Require Arith.
Require machine.

(*** The reference transition system ***)

Section trref.

Inductive trRef : state -> state -> Prop :=
    trRef_agetsb : (s:state)
      (trRef s (agetsb s))
  | trRef_bgetsa : (s:state)
      (trRef s (bgetsa s))
  | trRef_agetsbstar4 : (s:state)
      (addr (4) (mem_of s) (regb_of s)) ->
      (trRef s (agetsbstar4 s))
  | trRef_agetsbstar8 : (s:state)
      (addr (8) (mem_of s) (regb_of s)) ->
      (trRef s (agetsbstar8 s))
  | trRef_astargetsb4 : (s:state)
      (addr (4) (mem_of s) (rega_of s)) -> 
      (trRef s (astargetsb4 s))
  | trRef_astargetsb8 : (s:state)
      (addr (8) (mem_of s) (rega_of s)) -> 
      (trRef s (astargetsb8 s))
  | trRef_agetsn : (s:state)
      (n:exp)
      (trRef s (agetsn s n))
  | trRef_bgetsn : (s:state)
      (n:exp)
      (trRef s (bgetsn s n))
  | trRef_agetsaplusb : (s:state)
      (trRef s (agetsaplusb s))
(*  | trRef_agetsaminusb : (a,b:nat)(m:mem)(h:hist)[s:=(mkstate a b m h)]
      (trRef s (agetsaminusb s))
*)
(***
  | trRef_agetsnewn : (a,b:nat)(m:mem)(h:hist)[s:=(mkstate a b m h)]
      (n,x:nat)
      (new m x n) ->
      (trRef s (agetsnewn s n x))
***)
  | trRef_allocate : (s:state)
      (n:nat)
      (trRef s (allocate n s))
.

Inductive trRef_star : state -> state -> Prop :=
    refl : (s:state)(trRef_star s s)
  | trans : (s1,s2,s3:state)
      (trRef_star s1 s2) ->
      (trRef_star s2 s3) ->
      (trRef_star s1 s3)
  | onestep : (s1,s2:state)
      (trRef s1 s2) -> 
      (trRef_star s1 s2).

End trref.