Require Arith.
Require PolyList.

Require machine.

Section axioms.

Inductive javasimpletype : Set :=
    jbool    : javasimpletype
  | jchar    : javasimpletype
  | jbyte    : javasimpletype
  | jshort   : javasimpletype
  | jint     : javasimpletype
  | jlong    : javasimpletype
  | jfloat   : javasimpletype
  | jdouble  : javasimpletype.

Inductive javatype : Set :=
    fromsimple : javasimpletype -> javatype
  | jinstof : exp -> javatype
  | jarray : javatype -> javatype.

Inductive type : Set := 
    fromjavatype : javatype -> type
  | jclassdesc : type
  | jvirtab : exp -> type
  | jimplof : exp -> type.

Coercion fromsimple : javasimpletype >-> javatype.
Coercion fromjavatype : javatype >-> type.




(* outside information *)

(* From tcjaxioms: *)
Parameter given_staticptr : exp -> javatype -> Prop.
Parameter given_jclassdesc : exp -> Prop.
Parameter jifield : exp -> nat -> javatype -> Prop.
Parameter jvmethod : exp -> nat -> exp -> Prop.
Parameter jextends : exp -> exp -> Prop.
Parameter _4java4lang6Object_C : exp.

(* Also: *)
Parameter list_of_classes : (list exp).
Parameter list_of_staticptrs : (list (exp*javatype)).
Parameter size_of_instance : exp -> nat.
Parameter size_of_virtab : exp -> nat.
Parameter loc_of_virtab : exp -> nat. 




(*** state and pseudo-state ***)

Inductive repflag : Set :=
    repval : repflag
  | repptr : repflag.

Inductive rep : Set := 
    nilrep : rep
  | consrep : repflag -> exp -> javatype -> rep -> rep.

Fixpoint alloc_in [pv:repflag;h:exp;t:javatype;r:rep] : Prop :=
  Cases r of 
      nilrep => False
    | (consrep pv' h' t' r) => 
        (pv=pv' /\ h=h' /\ t=t') \/ (alloc_in pv h t r)
  end.

Record state' : Set := mkstate' {
  machine_state_of : state;
  rep_of : rep;
  last_alloc_of : mem
}.

Definition rega_of' [s:state'] : exp := (rega_of (machine_state_of s)).
Definition regb_of' [s:state'] : exp := (regb_of (machine_state_of s)).
Definition mem_of' [s:state'] : mem := (mem_of (machine_state_of s)).
Definition hist_of' [s:state'] : hist := (hist_of (machine_state_of s)).


(*** axioms ***)
(* Inductive predicates may be parameterized by state'.
   If so, there may be additional "hyp_" constructors
   which are allowed to refer to the state'.
   These will be the pathway for external functions to introduce
   new proofs of predicates. *)

Inductive rorw : Set :=
    ro : rorw
  | rw : rorw.

Inductive jsize : type -> nat -> Prop :=
    szbool : (jsize jbool (4))
  | szint : (jsize jint (4))
  | szbyte : (jsize jbyte (4))
  | szchar : (jsize jchar (4))
  | szshort : (jsize jshort (4))
  | szlong : (jsize jlong (8))
  | szfloat : (jsize jfloat (4))
  | szdouble : (jsize jdouble (8))
  | szcdesc : (jsize jclassdesc (4))  
  | szjinst : (C:exp)(jsize (jinstof C) (4)) 
  | szvirtab : (C:exp)(jsize (jvirtab C) (4))
  | szjimplof : (SIG:exp)(jsize (jimplof SIG) (4))
  | szjarr : (T:javatype)(jsize (jarray T) (4)).



Mutual Inductive ofType [s:state'] : exp -> type -> Prop :=
    jintany : (E:exp)(ofType s E jint)
  | jbyteany : (E:exp)(ofType s E jbyte)
  | jcharany : (E:exp)(ofType s E jchar)
  | jshortany : (E:exp)(ofType s E jshort)
  | jboolany : (E:exp)(ofType s E jbool)
(*
  | jlongany : (E:exp)(ofType s E jlong)
  | jfloatany : (E:exp)(ofType s E jfloat)
  | jdoubleany : (E:exp)(ofType s E jdouble)
*)
  | of0i : (C:exp)(ofType s Null (jinstof C))
  | of0a : (T:javatype)(ofType s Null (jarray T))

  | ext : (E:exp)(C:exp)(D:exp)
      (jextends C D) -> 
      (ofType s E (jinstof C)) -> 
      (ofType s E (jinstof D)) 

  | jarrObject : (E:exp)(T:javatype)
      (ofType s E (jarray T)) ->
      (ofType s E (jinstof _4java4lang6Object_C))

  | ty4 : (M:mem)(ADDR:exp)(T:type)(RO:rorw)
      (ptr s ADDR RO T) -> 
      (jsize T (4)) -> 
      (ofmem s M) -> 
      (ofType s (sel4 M ADDR) T)
  | ty8 : (M:mem)(ADDR:exp)(T:type)(RO:rorw)
      (ptr s ADDR RO T) ->
      (jsize T (8)) -> 
      (ofmem s M) ->
      (ofType s (sel8 M ADDR) T)

  | given_jclassdesc_of : (E:exp) 
      (given_jclassdesc E) ->
      (ofType s E jclassdesc)

  | hyp_jinstof : (h:exp)(C:exp)
      (alloc_in repval h (jinstof C) (rep_of s)) -> 
      (ofType s h (jinstof C))

  | hyp_jarray : (h:exp)(T:javatype)
      (alloc_in repval h (jarray T) (rep_of s)) -> 
      (ofType s h (jarray T))

with ptr [s:state'] : exp -> rorw -> type -> Prop :=
    ptrvirtab : (E:exp)(C:exp)
      (ofType s E (jinstof C)) ->
      (nonnull E) ->
      (ptr s E ro (jvirtab C))
  | ptrcdesc : (E:exp)(C:exp) 
      (ofType s E (jvirtab C)) ->
      (ptr s E ro jclassdesc)
  | instFld : (OFF:nat)(T:javatype)(C:exp)(E:exp)
      (jifield C OFF T) -> 
      (ofType s E (jinstof C)) -> 
      (nonnull E) -> 
      (ptr s (plus E OFF) rw T)
  | ptrvmethod : (E:exp)(C:exp)(OFF:nat)(SIG:exp)
      (jvmethod C OFF SIG) -> 
      (ofType s E (jvirtab C)) -> 
      (ptr s (plus E OFF) ro (jimplof SIG))

  | arrLen : (A:exp)(T:javatype)
      (ofType s A (jarray T)) ->
      (nonnull A) -> 
      (ptr s (plus A (4)) ro jint)
  | arrElem : (A:exp)(T:javatype)(SZ:nat)(M:mem)(IDX:nat)
      (ofType s A (jarray T)) ->
      (ofmem s M) ->
      (nonnull A) ->
      (jsize T SZ) -> 
      (lt IDX (sel4 M (plus A (4)))) ->
      (ptr s (plus A (plus (mult IDX SZ) (8))) rw T)
  | ptrvirtabarr : (E:exp)(T:javatype)
      (ofType s E (jarray T)) -> 
      (nonnull E) ->
      (ptr s E ro (jvirtab _4java4lang6Object_C))

  | given_staticptr_ptr : (E:exp)(T:javatype)
      (given_staticptr E T) -> 
      (ptr s E rw T)
 
  | hyp_simple_type : (h:exp)(T:javasimpletype)
      (alloc_in repptr h T (rep_of s)) ->
      (ptr s h rw T)

with ofmem [s:state'] : mem -> Prop :=
    ofmem4 : (M:mem)(ADDR:exp)(E:exp)(T:type)
      (ptr s ADDR rw T) ->
      (jsize T (4)) ->
      (ofType s E T) ->
      (ofmem s M) ->
      (ofmem s (upd4 M ADDR E))
  | ofmem8 : (M:mem)(ADDR:exp)(E:exp)(T:type)
      (ptr s ADDR rw T) ->
      (jsize T (8)) ->
      (ofType s E T) ->
      (ofmem s M) ->
      (ofmem s (upd8 M ADDR E))
(* ofamem : (E:exp)(ofmem s (amem E)) *)

 | hyp_ofmem :
(* The hyp clauses come from the postconditions of external functions... *)
     (ofmem s (last_alloc_of s)). 



Inductive saferd4 [s:state'] : exp -> Prop :=
    rd4 : (ADDR:exp)(T:type)(RO:rorw)
      (ptr s ADDR RO T) ->
      (jsize T (4)) ->
      (saferd4 s ADDR).

Inductive safewr4 [s:state'] : exp -> exp -> Prop :=
    wr4 : (ADDR:exp)(T:type)(E:exp)
      (ptr s ADDR rw T) ->
      (jsize T (4)) ->
      (ofType s E T) ->
      (safewr4 s ADDR E).

Inductive saferd8 [s:state'] : exp -> Prop :=
    rd8 : (ADDR:exp)(T:type)(RO:rorw)
      (ptr s ADDR RO T) ->
      (jsize T (8)) ->
      (saferd8 s ADDR).

Inductive safewr8 [s:state'] : exp -> exp -> Prop :=
    wr8 : (ADDR:exp)(T:type)(E:exp)
      (ptr s ADDR rw T) ->
      (jsize T (8)) ->
      (ofType s E T) ->
      (safewr8 s ADDR E).



(* end of axioms *)

End axioms.