sail-to-lean: Add support to memory

[ineol]

This is a prerequisite for properly fixing #939.

A good candidate would be to have the SequentialState.mem field be a Std.HashMap Nat UInt8

[javra]

Is Nat the right semantics or do we have to restrict the "address space"?

[bacam]

The memory interface in Sail uses bitvectors for physical addresses, FWIW.

[tobiasgrosser]

LNSym did the same, AFAIU.

[ineol]

The memory interface in Sail uses bitvectors for physical addresses, FWIW.

But it's Nat's in the Coq (sequential) state, right?

In State_monad.v:

Module NMap := FMapAVL.Make(OrderedTypeEx.N_as_OT).
Definition Memstate : Type := NMap.t memory_byte.

[bacam]

But it's Nat's in the Coq (sequential) state, right?

Yes, it is there. With the new concurrency interface the model's type is passed down (and I think Thibaut's sequential interpretation uses that directly, even though the Sail interface requires a function to embed it in a bitvector). It probably doesn't make much difference for us at the moment.