Require Arith.
Require PolyList.
Require machine.
Require axioms.

Section java.

(* Consistency guarantees: assumptions about the outside
   information *)

(* need in allocinv.v *)
Axiom jextends_reflexive : (C:exp)
  (jextends C C).

Axiom jextends_transitive : (C,D,E:exp)
  (jextends C D) ->
  (jextends D E) ->
  (jextends C E).

Axiom jifield_extends : (C,D:exp)(OFF:nat)(T:javatype)
  (jextends C D) ->
  (jifield D OFF T) ->
  (jifield C OFF T).

Axiom jvmethod_extends : (C,D:exp)(OFF:nat)(SIG:exp)
  (jextends C D) ->
  (jvmethod D OFF SIG) ->
  (jvmethod C OFF SIG).

Axiom field_size_good : (C:exp)(OFF:nat)(T:javatype)(SZ:nat)
  (jifield C OFF T) ->
  (jsize T SZ) ->
  (le (plus OFF SZ) (size_of_instance C)).

Axiom jifield_four : (C:exp)(OFF:nat)(T:javatype)
  (jifield C OFF T) ->
  (le (4) OFF).

Axiom virtab_size_good : (C:exp)(OFF:nat)(SIG:exp)
  (jvmethod C OFF SIG) ->
  (le (plus OFF (4)) (size_of_virtab C)).

Axiom virtab_size_four : (C:exp)
  (le (4) (size_of_virtab C)).

Axiom fields_equal_or_apart : (C:exp)
  (OFF1,OFF2:nat)(T1,T2:javatype)(SZ1,SZ2:nat)
  (jifield C OFF1 T1) ->
  (jifield C OFF2 T2) ->
  (jsize T1 SZ1) ->
  (jsize T2 SZ2) ->
  (OFF1=OFF2 /\ T1=T2)\/(apart OFF1 SZ1 OFF2 SZ2).

Axiom no_object_super : (D:exp)
  (jextends _4java4lang6Object_C D) ->
  D = _4java4lang6Object_C.

Axiom no_object_fields : (OFF:nat)(T:javatype)
  (jifield _4java4lang6Object_C OFF T) ->
  False.


(* this one also in allocinv.v *)
Axiom instance_size_four : (C:exp)
  (le (4) (size_of_instance C)).




(* need in start.v *)

Axiom all_classes_in_list : (C:exp)(EX D:exp | (In D list_of_classes) /\
  (size_of_virtab C)=(size_of_virtab D) /\ 
  (loc_of_virtab C)=(loc_of_virtab D)).

Axiom all_staticptrs_in_list : (E:exp)(T:javatype)
  (given_staticptr E T) ->
  (In (E,T) list_of_staticptrs).

Axiom list_all_staticptrs : (E:exp)(T:javatype)
  (In (E,T) list_of_staticptrs) ->
  (given_staticptr E T).  

Axiom staticptr_equal_or_apart : (E1,E2:exp)(T1,T2:javatype)(SZ1,SZ2:nat)
  (given_staticptr E1 T1) ->
  (jsize T1 SZ1) ->
  (given_staticptr E2 T2) ->
  (jsize T2 SZ2) ->
  (E1=E2 /\ T1=T2) \/ (apart E1 SZ1 E2 SZ2).

Axiom staticptr_virtab_apart : (E:exp)(T:javatype)(SZ:nat)(C:exp)
  (given_staticptr E T) ->
  (jsize T SZ) ->
  (apart E SZ (loc_of_virtab C) (size_of_virtab C)).

End java.