Coq: Initial register values are not reflected in the generated coq code

[maxkurze1]

If I am using the register <id> : <typ> = <exp> syntax to initialize a register with a certain value, the generated coq code will still use 0 as the initial register state.

For example, the following sail code:

default Order dec
$include <prelude.sail>

register SOME_REG    : bits(32) = 0x00000003
register ANOTHER_REG : bits(16) = 0x1234
register IDK         : bits( 5) = 0b10101

generates a coq definition like this:

Definition initial_regstate : regstate :=
{| IDK := ('b"00000")  : mword 5;
   ANOTHER_REG := (Ox"0000")  : mword 16;
   SOME_REG := (Ox"00000000")  : mword 32 |}.

Sadly, the initial values from the sail definition completely vanish inside the generated coq.

If this behavior is intentional, is there any other way to get access to these init-expressions inside coq? And if it is not intentional, how would I go about fixing it?

[bacam]

I think you might be using an old version of Sail? They were added in 2ed35c6f4 shortly before the release of 0.17.1.

(Also, I should warn you that we're going to change the representation of registers and sequential register state in Coq soon, although probably not until after the next release.)

[maxkurze1]

I am a bit embarrassed now, you are right, I was using the older 0.16 version from the nix package repo. I am probably going to commit a version bump there. Thanks for the advice.

Regarding this incoming change, is there a place to find more information about it?

[bacam]

Regarding this incoming change, is there a place to find more information about it?

Not really, although there is some code for it in https://github.com/bacam/sail/tree/newregstate and https://github.com/rems-project/coq-sail/tree/newregstate. Some major points are:

• Registers are represented essentially by an enumeration rather than strings.
• Each register is associated with a type (currently by a GADT-like type parameter on the register type because we think that it might have some advantages when working with extracted OCaml, but some disadvantages in Coq might end up outweighing this).
• The monad the definitions are in uses these types at register read and write, rather than a generic register value type.
• The sequential state is now a map rather than a giant record (which avoids efficiency problems with the coq-record-update package).

[maxkurze1]

Thank you.