# Library liblayers.simrel.MemWithData

# Memory with abstract data

## Base memory model

Class BaseMemoryModel :=

{

mem : Type;

base_mem_ops :> Mem.MemoryModelOps mem;

base_mem_prf :> Mem.MemoryModelX mem

}.

## Memory with data

Section MEM_WITH_DATA.

Context `{Hmem: BaseMemoryModel}.

Context (D: layerdata).

Definition mwd := (mem × D)%type.

We can now instantiate a memory model for mwd D, by using the
lens fst to lift the base memory model to such pairs.

Local Instance mwd_liftmem_ops: LiftMemoryModelOps (@fst mem D) :=

{

liftmem_empty := (Mem.empty, init_data)

}.

Local Instance mwd_liftmem_prf `{Mem.MemoryModelX}:

LiftMemoryModel (@fst mem D).

Proof.

split.

typeclasses eauto.

reflexivity.

Qed.

Global Instance mwd_ops: Mem.MemoryModelOps mwd | 5 := _.

Global Instance mwd_prf: Mem.MemoryModelX mwd | 5 := _.

End MEM_WITH_DATA.

The following rewriting rule is useful when using the lens_unfold
tactic to reduce Compcert memory operations applied to our composite
memory states.

Lemma mwd_same_context_mem_eq_data `{BaseMemoryModel} D (m1 m2: mwd D):

same_context (S := mwd D) fst m1 m2 ↔

snd m1 = snd m2.

Proof.

apply fst_same_context_eq_snd.

Qed.

Hint Rewrite @mwd_same_context_mem_eq_data using typeclasses eauto : lens_simpl.