Require Arith.
Require Omega.

Require machine.
Require trref.
Require axioms.
Require traux.
Require invar.
Require induction.
Require upd_resp.
Require allocinv.
Require start.
Require java. (* Need instance_size_four for duplicating allocate_jinstof
  * in the reference system *)

Section main.

(* First, all reachable states satisfy the invariant.
First we need that silly transitions preserve the invariant *)

(* These from upd_resp *)
Hints Resolve same_pseudo_preserves_ptr same_pseudo_preserves_ofmem
  : same_pseudo.

Lemma same_pseudo_same_mem_preserves_invar :
  (r:rep)(l:mem)(m:mem)
  (a1,b1:exp)(h1:hist)(a2,b2:exp)(h2:hist)
  [ms := (mkstate a1 b1 m h1)][ms2 := (mkstate a2 b2 m h2)]
  [s := (mkstate' ms r l)][s2 := (mkstate' ms2 r l)]
  (invariant s) -> (invariant s2).
Proof.
Intros until s2.
Unfold s s2 ms ms2.
Clear s s2 ms ms2.
Intros.
Unfold_invar H.
Unfold_invar_Goal; EAuto with same_pseudo.
Qed.


Lemma trAux_preserves_invariant :
  (s:state')(invariant s) ->
  (s':state')(trAux s s') ->
  (invariant s').
Proof.
Intros.
Generalize H; Clear H.
NewInduction H0; Try
  (Intros invar; Unfold s in invar; Unfold agetsb bgetsa agetsn bgetsn 
   agetsaplusb agetsbstar4 agetsbstar8;
   EApply same_pseudo_same_mem_preserves_invar; EAuto).
(* the upd cases *)
  Intro; Unfold s in H0; Unfold astargetsb4.
  Unfold upd4.
  Replace (mem_of s) with (mem_of' (mkstate' s r l)); Try Reflexivity.
  Replace r with (rep_of (mkstate' s r l)); Try Reflexivity.
  Replace l with (last_alloc_of (mkstate' s r l)); Try Reflexivity.
  Inversion_clear H.
  EApply upd_respects; EAuto.

  Intro; Unfold s in H0; Unfold astargetsb8.
  Unfold upd8.
  Replace (mem_of s) with (mem_of' (mkstate' s r l)); Try Reflexivity.
  Replace r with (rep_of (mkstate' s r l)); Try Reflexivity.
  Replace l with (last_alloc_of (mkstate' s r l)); Try Reflexivity.
  Inversion_clear H.
  EApply upd_respects; EAuto.

(*the alloc cases*)
    
  Intro.
  EApply allocate_jinstof_respects; EAuto.

  Intro.
  EApply allocate_jarray_respects; EAuto.

  Intro.
  EApply allocate_simple_type_respects; EAuto.
Qed.


Lemma reachable_implies_invariant :
  (s:state')(invariant s) ->
  (s':state')(reachable_from s s') ->
  (invariant s').
Proof.
Intros.
NewInduction H0.
  Assumption.

  EApply trAux_preserves_invariant; EAuto.
Qed.


Hint trRef_star : temp := Constructors trRef_star.
Hint trRef : temp := Constructors trRef.

Lemma invariant_implies_sound : 
  (s:state')(invariant s) ->
  (s':state')(trAux s s') ->
  (trRef_star (machine_state_of s) (machine_state_of s')).
Proof.
Intros.
Unfold_invar H.
NewInduction H0; 
    Unfold machine_state_of s; Auto with temp;
    Try (Solve [Inversion_clear H0; EAuto with temp]). (* safexx cases *)
(* allocate_jinstof *)
  Unfold allocate_jinstof.
  EApply trans.
    EApply onestep.  
    EApply trRef_allocate.

    EApply trans.
      EApply onestep.
      EApply trRef_bgetsn.

      EApply onestep.
      EApply trRef_astargetsb4.
      LetTac ss := (allocate (size_of_instance C)
           (machine_state_of (mkstate' (mkstate a b m h) r l))).
      Change (addr (4) (mem_of ss) (rega_of ss)).
      Replace (rega_of ss) with (plus (0) (rega_of ss)); Try Reflexivity.
      EApply addr_closed.
        Unfold ss; EApply allocate_works.

        Unfold plus.
        Apply instance_size_four.

(* allocate_jarray *)
  Unfold allocate_jarray.
  EApply trans. EApply onestep; EApply trRef_allocate 
      with n:=(plus (mult n SZ) (8)).
  EApply trans. EApply onestep; EApply trRef_bgetsn 
      with n:=(loc_of_virtab _4java4lang6Object_C).
  EApply trans. EApply onestep; EApply trRef_astargetsb4.
    LetTac ss := (allocate (plus (mult n SZ) (8))
         (mkstate a b m h)).
    Change (addr (4) (mem_of ss) (rega_of ss)).
    Replace (rega_of ss) with (plus (0) (rega_of ss)); Try Reflexivity.
    EApply addr_closed.
      Unfold ss; EApply allocate_works.
  
      Clear ss.
      LetTac silly := (mult n SZ).
      Omega.  
    
  EApply trans. EApply onestep; EApply trRef_bgetsn with n:=(4).
  EApply trans. EApply onestep; EApply trRef_agetsaplusb.
  EApply trans. EApply onestep; EApply trRef_bgetsn.
  EApply trans. EApply onestep; EApply trRef_astargetsb4.
    LetTac ss := (allocate (plus (mult n SZ) (8))
         (mkstate a b m h)).
    Change (addr (4) 
        (updn (4) (mem_of ss) (rega_of ss) 
           (loc_of_virtab _4java4lang6Object_C))
        (plus (rega_of ss) (4))).
    EApply addr_updn.
      Replace (rega_of ss) with (plus (0) (rega_of ss)); Try Reflexivity.
      EApply addr_closed.
        Unfold ss; EApply allocate_works.
  
        Clear ss.
        LetTac silly := (mult n SZ).
        Omega.  

      Rewrite plus_sym.
      EApply addr_closed.
        Unfold ss; EApply allocate_works.
    
        Clear ss.
        LetTac silly := (mult n SZ).
        Omega.  
  
  EAuto with temp.      

(*finally allocate_simple_type*)
  Unfold allocate_simple_type.
  EApply trans. EApply onestep; EApply trRef_allocate.
  EAuto with temp.
Qed.


Theorem main : (EX start_state : state' | 
  (s:state')(reachable_from start_state s) ->
  (s':state')(trAux s s') ->
  (trRef_star (machine_state_of s) (machine_state_of s'))).
Proof.
Exists start_state.
Intros.
Apply invariant_implies_sound; Auto.
EApply reachable_implies_invariant; EAuto.
Exact invariant_start_state.
Qed.

End main.