Module MemoryMachine

Require Import Coqlib.
Require Import Maps.
Require Import Ast.
Require Import Integers.
Require Import Pointers.
Require Import Values.
Require Import Mem.
Require Import Events.
Require Import Globalenvs.
Require Import Op.
Require Import Registers.
Require Import Libtactics.
Require Import INJECT.
Require Import Utils.
Require Import TSOmachine.
Require Import Classical.
Require Import Relations.
Require Import Permissions Emem.

Record mem : Type := MEM {
  mem_rtl :> Mem.mem;
  perms :> perm_map
}.


Inductive mem_step t : mem -> mem_event -> mem -> Prop :=
  | mem_step_perm: forall m d d' ev
    (ESD:perm_step t d ev d'),
    mem_step t (MEM m d) (MEperm ev) (MEM m d')
  | mem_step_localstore: forall m p v m' d (released:bool) d'
    (ESS:store_ptr Mint32 m p v = Some m')
    (ESD:d p = HiddenBy t)
    (ESP:if released then release t d d' else d=d')
    (ESWF1: wf_val v)
    (ESWF2: wf_ptr p),
    mem_step t (MEM m d) (MEwrite released Local p v) (MEM m' d')
  | mem_step_localload: forall m p v d inbuf
    (ESL:load_ptr Mint32 m p = Some v)
    (ESP:readable_perm d p t)
    (ESWF1: wf_val v)
    (ESWF2: wf_ptr p),
    mem_step t (MEM m d) (MEread Local inbuf p v) (MEM m d)
  | mem_step_store: forall m p v m' d (released:bool) d'
    (ESS:store_ptr Mint32 m p v = Some m')
    (ESD: check_perm_store t d' Global p)
    (ESP:if released then release t d d' else d=d')
    (ESWF1: wf_val v)
    (ESWF2: wf_ptr p),
    mem_step t (MEM m d) (MEwrite released Global p v) (MEM m' d')
  | mem_step_load: forall m p v d inbuf
    (ESL:load_ptr Mint32 m p = Some v)
    (ESD:forall t', d p = HiddenBy t' -> t=t')
    (ESWF1: wf_val v)
    (ESWF2: wf_ptr p),
    mem_step t (MEM m d) (MEread Global inbuf p v) (MEM m d)
  | mem_step_rmw : forall m m' p v instr (r:bool) d d'
    (LD: load_ptr Mint32 m p = Some v)
    (STO: store_ptr Mint32 m p (rmw_instr_semantics instr v) = Some m')
    (ESP:if r then release t d d' else d=d')
    (ESD:d' p = empty_perm)
    (ESWF1: wf_val v)
    (ESWF2: wf_ptr p)
    (ESWF3: wf_rmw instr),
    mem_step t (MEM m d) (MErmw r p v instr) (MEM m' d')
  | mem_step_alloc: forall m p i k m' d
    (ESF: range_has_store_perm t d (p,i))
    (ESL:alloc_ptr (p,i) k m = Some m'),
    mem_step t (MEM m d) (MEalloc p i k) (MEM m' d)
  | mem_step_free: forall m p k m' d n
    (ESA: range_allocated (p,n) k m)
    (ESWF: range_has_store_perm t d (p,n))
    (ESL:free_ptr p k m = Some m'),
    mem_step t (MEM m d) (MEfree p k) (MEM m' d).