Require Arith.
Require machine.
Require axioms.

Section invar.

Definition ptr_addr [s:state'] : Prop :=
  (E:exp)(RW:rorw)(T:type)(SZ:nat)  (*  (M:mem)  *)
  (jsize T SZ) ->
  (ptr s E RW T) ->
(*  (ofmem s M) -> *)
  (addr SZ (mem_of' s) E).

Definition ptr_rw_equal_or_apart [s:state'] : Prop :=
  (e1,e2:exp)(RW:rorw)(T1,T2:type)(SZ1,SZ2:nat)
  (ptr s e1 rw T1) -> 
  (jsize T1 SZ1) ->
  (ptr s e2 RW T2) ->
  (jsize T2 SZ2) ->
  ((e1=e2)/\(rw=RW)/\(T1=T2)) \/
  (apart e1 SZ1 e2 SZ2).

Definition virtab_addr [s:state'] : Prop :=
  (C:exp)(addr (size_of_virtab C) (mem_of' s) (loc_of_virtab C)).

Definition ptr_rw_virtab_apart [s:state'] : Prop :=
  (e:exp)(T:type)(SZ:nat)(C:exp)
  (ptr s e rw T) -> 
  (jsize T SZ) ->
  (apart e SZ (loc_of_virtab C) (size_of_virtab C)).


Definition ofmem_own_mem [s:state'] : Prop :=
  (ofmem s (mem_of' s)).  

Definition invariant [s:state'] : Prop :=
  (ptr_addr s) /\ 
    (ptr_rw_equal_or_apart s) /\ 
    (virtab_addr s) /\
    (ptr_rw_virtab_apart s) /\
    (ofmem_own_mem s).


End invar.


Tactic Definition Unfold_invar H :=
  Generalize H;
  Cbv Delta [invariant ptr_addr ptr_rw_equal_or_apart
    virtab_addr ptr_rw_virtab_apart ofmem_own_mem] in H;
  Decompose [and] H;
  Clear H;
  Intro H.

Tactic Definition Unfold_invar_Goal :=
  Cbv Delta [invariant ptr_addr ptr_rw_equal_or_apart
    virtab_addr ptr_rw_virtab_apart ofmem_own_mem];
  Split; [Idtac | Split; [Idtac | Split; [Idtac | Split]]].