Require Arith.
Require machine.
Require axioms.


Section traux.

(*** pseudo-external functions ***)

Definition allocate_jinstof_rep : exp -> state' -> rep :=
  [C:exp][s:state'][ms := (machine_state_of s)][r := (rep_of s)]
  [a := (rega_of (allocate (size_of_instance C) ms))]
  (consrep repval a (jinstof C) r).
Definition allocate_jinstof : exp -> state' -> state' :=
  [C:exp][s:state'][ms:=(machine_state_of s)]
  [ms':=(astargetsb4
    (bgetsn 
     (allocate (size_of_instance C) ms)
     (loc_of_virtab C) ))]
  (mkstate' ms'  
   (allocate_jinstof_rep C s)
   (mem_of ms')).

Definition allocate_jarray_rep :=
  [T:javatype][SZ:nat][jsz:(jsize T SZ)][n:nat][s:state']
  [ms := (machine_state_of s)][r := (rep_of s)]
  [a := (rega_of (allocate (plus (mult n SZ) (8)) ms))]
  (consrep repval a (jarray T) r). 
Definition allocate_jarray :=
  [T:javatype][SZ:nat][jsz:(jsize T SZ)]
  [n:nat][s:state'][ms:=(machine_state_of s)]
  [ms' := (astargetsb4
    (bgetsn
     (agetsaplusb
      (bgetsn
       (astargetsb4 
        (bgetsn 
         (allocate (plus (mult n SZ) (8)) ms)
         (loc_of_virtab _4java4lang6Object_C)))
       (4)))
     n))]
  (mkstate' ms'
   (allocate_jarray_rep T SZ jsz n s)
   (mem_of ms')).

Definition allocate_simple_type_rep :=
  [T:javasimpletype][SZ:nat][jsz:(jsize T SZ)]
  [s:state'][ms := (machine_state_of s)][r := (rep_of s)]
  [a := (rega_of (allocate SZ ms))]
  (consrep repptr a T r).
Definition allocate_simple_type :=
  [T:javasimpletype][SZ:nat][jsz:(jsize T SZ)]
  [s:state'][ms:=(machine_state_of s)]
  (mkstate' (allocate SZ ms) 
    (allocate_simple_type_rep T SZ jsz s)
    (mem_of (allocate SZ ms))).



Inductive trAux : state' -> state' -> Prop :=
    trAux_agetsb : (a,b:exp)(m:mem)(h:hist)(r:rep)(l:mem)
      [s:=(mkstate a b m h)]
      (trAux (mkstate' s r l) (mkstate' (agetsb s) r l))
  | trAux_bgetsa : (a,b:exp)(m:mem)(h:hist)(r:rep)(l:mem)
      [s:=(mkstate a b m h)]
      (trAux (mkstate' s r l) (mkstate' (bgetsa s) r l))
  | trAux_agetsn : (a,b:exp)(m:mem)(h:hist)(r:rep)(l:mem)
      [s:=(mkstate a b m h)]
      (n:exp)
      (trAux (mkstate' s r l) (mkstate' (agetsn s n) r l))
  | trAux_bgetsn : (a,b:exp)(m:mem)(h:hist)(r:rep)(l:mem)
      [s:=(mkstate a b m h)]
      (n:exp)
      (trAux (mkstate' s r l) (mkstate' (bgetsn s n) r l))
  | trAux_agetsaplusb : (a,b:exp)(m:mem)(h:hist)(r:rep)(l:mem)
      [s:=(mkstate a b m h)]
      (trAux (mkstate' s r l) (mkstate' (agetsaplusb s) r l))
(***
  | trAux_agetsaminusb : (a,b:exp)(m:mem)(h:hist)(r:rep)
      [s:=(mkstate a b m h)]
      (trAux (mkstate' s r) (mkstate' (agetsaminusb s) r))
***)

  | trAux_read4 : (a,b:exp)(m:mem)(h:hist)(r:rep)(l:mem)
      [s:=(mkstate a b m h)]
      (saferd4 (mkstate' s r l) b) ->
      (trAux (mkstate' s r l) (mkstate' (agetsbstar4 s) r l))
  | trAux_read8 : (a,b:exp)(m:mem)(h:hist)(r:rep)(l:mem)
      [s:=(mkstate a b m h)]
      (saferd8 (mkstate' s r l) b) ->
      (trAux (mkstate' s r l) (mkstate' (agetsbstar8 s) r l))
  | trAux_write4 : (a,b:exp)(m:mem)(h:hist)(r:rep)(l:mem)
      [s:=(mkstate a b m h)]
      (safewr4 (mkstate' s r l) a b) ->
      (trAux (mkstate' s r l) (mkstate' (astargetsb4 s) r l))
  | trAux_write8 : (a,b:exp)(m:mem)(h:hist)(r:rep)(l:mem)
      [s:=(mkstate a b m h)]
      (safewr8 (mkstate' s r l) a b) ->
      (trAux (mkstate' s r l) (mkstate' (astargetsb8 s) r l))
  | trAux_alloc_jinstof : (a,b:exp)(m:mem)(h:hist)(r:rep)(l:mem)
      [s:=(mkstate a b m h)]
      (C:exp)
      (trAux (mkstate' s r l) 
             (allocate_jinstof C (mkstate' s r l)))
  | trAux_alloc_jarray : (a,b:exp)(m:mem)(h:hist)(r:rep)(l:mem)
      [s:=(mkstate a b m h)]
      (T:javatype)(SZ:nat)(jsz:(jsize T SZ))(n:nat)
      (trAux (mkstate' s r l) 
             (allocate_jarray T SZ jsz n (mkstate' s r l)))
  | trAux_alloc_simple_type : (a,b:exp)(m:mem)(h:hist)(r:rep)(l:mem)
      [s:=(mkstate a b m h)]
      (T:javasimpletype)(SZ:nat)(jsz:(jsize T SZ))
      (trAux (mkstate' s r l) 
             (allocate_simple_type T SZ jsz (mkstate' s r l))).



Inductive reachable_from [s:state'] : state' -> Prop :=
    self_reachable : (reachable_from s s)
  | trAux_reachable : (s',s'':state')
      (reachable_from s s') ->
      (trAux s' s'') ->
      (reachable_from s s'').


End traux.