(* Memory model used in the dynamic semantics of the back-end intermediate
   languages. Inspired by common/Mem.ma, adapted from Compcert *)

(* * This file develops the memory model that is used in the dynamic
  semantics of all the languages used in the compiler.
  It defines a type [mem] of memory states, the following 4 basic
  operations over memory states, and their properties:
- [load]: read a memory chunk at a given address;
- [store]: store a memory chunk at a given address;
- [alloc]: allocate a fresh memory block;
- [free]: invalidate a memory block.
*)

include "joint/BEValues.ma".
include "common/GenMem.ma".

definition bemem ≝ mem (mk_contentT beval BVundef).

axiom beloadv: ∀m:bemem. ∀ptr:pointer. option beval.
axiom bestorev: ∀m:bemem. ∀ptr:pointer. beval → option bemem.