Require Arith.
Require PolyList.

Section machine.

(*** The machine ***)

(*** Expressions ***)

Definition exp : Set := nat.
Definition Null : exp := (0).
Inductive null : exp -> Prop :=
  zero_null : (null Null).
Inductive nonnull : exp -> Prop :=
  S_nonnull : (n:nat)(nonnull (S n)).

Derive Inversion_clear nonnull_null_inv with 
  (nonnull Null) Sort Prop.




(*** memory ***)

Parameter mem : Set.
Parameter empty : mem.
Parameter updn : nat -> mem -> exp -> exp -> mem.
Definition upd4 := (updn (4)).
Definition upd8 := (updn (8)).
Parameter seln : nat -> mem -> exp -> exp.
Definition sel4 := (seln (4)).
Definition sel8 := (seln (8)).
Parameter addr : nat -> mem -> exp -> Prop.
Parameter brute_alloc : nat -> mem -> exp -> mem.

Axiom updn_seln : (n:nat)(m:mem)(ADDR,E:exp)
  (addr n m ADDR) -> 
  (seln n (updn n m ADDR E) ADDR) = E.

Definition apart [e1:exp][n1:nat][e2:exp][n2:nat] : Prop :=
  ((lt e1 e2) /\ (le (plus n1 e1) e2)) \/
  ((lt e2 e1) /\ (le (plus n2 e2) e1)).

Axiom updn_seln_apart : (n1,n2:nat)(m:mem)(e1,e2:exp)(v:exp)
  (addr n1 m e1) -> 
  (apart e1 n1 e2 n2) -> 
  (seln n2 (updn n1 m e1 v) e2) =
    (seln n2 m e2).

Axiom addr_updn : (n1,n2:nat)(m:mem)(ADDR1,ADDR2,E:exp)
  (addr n2 m ADDR2) -> 
  (addr n1 m ADDR1) ->
  (addr n1 (updn n2 m ADDR2 E) ADDR1).

Axiom addr_closed : (n,o,k:nat)(m:mem)(a:exp)
  (addr n m a) ->
  (le (plus o k) n) ->
  (addr k m (plus o a)).

Axiom brute_alloc_addr : (n:nat)(m:mem)(a:exp)
  (addr n (brute_alloc n m a) a). 

Axiom brute_alloc_preserves : (n1,n2:nat)(m:mem)(a1,a2:exp)
  (addr n1 m a1) ->
  (addr n1 (brute_alloc n2 m a2) a1).

Axiom brute_alloc_alias : (n1,n2:nat)(m:mem)(a1,a2:nat)
  (addr n1 m a1) -> 
  (seln n1 m a1) = (seln n1 (brute_alloc n2 m a2) a1).

(*** history ***)

Inductive inst : Set :=
    read_inst : mem -> exp -> inst
  | write_inst : mem -> exp -> exp -> inst.

Definition hist := (list inst).



(*** state ***)

Record state : Set := mkstate {
  rega_of : exp;
  regb_of : exp;
  mem_of : mem;
  hist_of : hist
}.


(*** external functions ***)

Parameter allocate : nat -> state -> state.

Axiom allocate_works : (n:nat)(s:state)[s2:=(allocate n s)]
  (addr n (mem_of s2) (rega_of s2)).

Axiom allocate_zeros : (n1,n2:nat)(s:state)(o:nat)[s2:=(allocate n2 s)]
  (le (plus o n1) n2) ->
  (seln n1 (mem_of s2) (plus o (rega_of s2))) = Null.

Axiom allocate_new :  (n1,n2,o:nat)(s:state)[s2:=(allocate n2 s)]
(*  (le (plus o n1) n2) -> *)
  (lt o n2) ->
  (lt (0) n1) -> 
  (addr n1 (mem_of s) (plus o (rega_of s2)))->
  False.

Axiom allocate_preserves : (n1,n2:nat)(s:state)[s2:=(allocate n2 s)]
  (a:exp)(addr n1 (mem_of s) a) -> (addr n1 (mem_of s2) a).

Axiom allocate_alias : (n1,n2:nat)(s:state)[s2:=(allocate n2 s)]
  (a:exp)(addr n1 (mem_of s) a) -> 
  (seln n1 (mem_of s2) a) = (seln n1 (mem_of s) a).




(*** The machine transitions ***)

Definition agetsb [s : state] : state :=
  [a := (rega_of s)][b := (regb_of s)][m := (mem_of s)][h := (hist_of s)]
    (mkstate b b m h).

Definition bgetsa [s : state] : state :=
  [a := (rega_of s)][b := (regb_of s)][m := (mem_of s)][h := (hist_of s)]
    (mkstate a a m h).

(* requires (addr n m b) *)
Definition agetsbstar4 [s : state] : state :=
  [a := (rega_of s)][b := (regb_of s)][m := (mem_of s)][h := (hist_of s)]
    (mkstate (sel4 m b) b m (cons (read_inst m b) h)).
Definition agetsbstar8 [s : state] : state :=
  [a := (rega_of s)][b := (regb_of s)][m := (mem_of s)][h := (hist_of s)]
    (mkstate (sel8 m b) b m (cons (read_inst m b) h)).

(* requires (addr n m a) *)
Definition astargetsb4 [s : state] : state :=
  [a := (rega_of s)][b := (regb_of s)][m := (mem_of s)][h := (hist_of s)]
    (mkstate a b (upd4 m a b) (cons (write_inst m a b) h)).
Definition astargetsb8 [s : state] : state :=
  [a := (rega_of s)][b := (regb_of s)][m := (mem_of s)][h := (hist_of s)]
    (mkstate a b (upd8 m a b) (cons (write_inst m a b) h)).

(* requires (new m h) *)
(*
Definition agetsnewn [s : state] : nat -> nat -> state :=
  [home,sz:nat]
  [a := (rega_of s)][b := (regb_of s)][m := (mem_of s)][h := (hist_of s)]
    (mkstate (Nat home) b (alloc m home sz) 
      (cons (alloc_inst home sz) h)).
*)

Definition agetsn [s : state] : exp -> state :=
  [n:exp]
  [a := (rega_of s)][b := (regb_of s)][m := (mem_of s)][h := (hist_of s)]
    (mkstate n b m h).

Definition bgetsn [s : state] : exp -> state := 
  [n:exp]
  [a := (rega_of s)][b := (regb_of s)][m := (mem_of s)][h := (hist_of s)]
    (mkstate a n m h).

Definition agetsaplusb [s : state] : state :=
  [a := (rega_of s)][b := (regb_of s)][m := (mem_of s)][h := (hist_of s)]
    (mkstate (plus a b) b m h).

(***
Definition agetsaminusb [s : state] : state :=
  [a := (rega_of s)][b := (regb_of s)][m := (mem_of s)][h := (hist_of s)]
    (mkstate (minus a b) b m h).
***)

End machine.