Require Arith.
Require PolyList.

Require machine.
Require axioms.
Require invar.
Require induction.
Require jsize.
Require lemmas.
Require java.

Section start.

Definition alloc_virtabs_mem : mem :=
  (fold_right
      [C:exp][m:mem](brute_alloc (size_of_virtab C) m (loc_of_virtab C))
      empty
      list_of_classes).

Definition start_mem : mem :=
  (fold_right
      [pair:exp*javatype][m:mem](updn (jsize_of (Snd pair)) 
          (brute_alloc (jsize_of (Snd pair)) m (Fst pair))
          (Fst pair) Null)
      alloc_virtabs_mem
      list_of_staticptrs).

Hints Resolve brute_alloc_addr brute_alloc_preserves addr_updn : temp.

Lemma addr_virtab_start_mem : (C:exp)
  (addr (size_of_virtab C) start_mem (loc_of_virtab C)).
Proof.
Intros.
Unfold start_mem.
Elim list_of_staticptrs.
  Simpl.
  Unfold alloc_virtabs_mem.
  Generalize (all_classes_in_list C); Intro.
  Decompose [and ex] H. 
  Rewrite H0.  
  Rewrite H3.
  Generalize H1; Clear H1.
  Clear H H0 H3.
  Elim list_of_classes. 
    Contradiction. 

    Intros.
    Simpl in H1.
    Decompose [or] H1.
      Rewrite H0.
      Simpl.
      EAuto with temp.

      Simpl.
      EAuto with temp.

  Intros.
  Simpl.
  EAuto with temp.
Qed.

Lemma addr_staticptr_start_mem_lemma : (E:exp)(T:javatype)
  (l:(list (exp*javatype)))
  (In (E,T) l) ->
  (addr (jsize_of T)
      (fold_right
      [pair:exp*javatype][m:mem](updn (jsize_of (Snd pair)) 
          (brute_alloc (jsize_of (Snd pair)) m (Fst pair))
          (Fst pair) Null)
      alloc_virtabs_mem
      l) E).
Proof.
Intros until l.
Elim l.
  Contradiction.

  Intros.
  Simpl in H0.
  Decompose [or] H0.
    Rewrite H1.  
    Simpl.
    EAuto with temp.

    Simpl.
    EAuto with temp.
Qed.


Lemma addr_staticptr_start_mem : (E:exp)(T:javatype)
  (given_staticptr E T) ->
  (SZ:nat)(jsize T SZ) ->
  (addr SZ start_mem E).
Proof.
Intros.
Rewrite (jsize_unique ? ? ? H0 (jsize_lemma T)).
Unfold start_mem.
Generalize (all_staticptrs_in_list E T H).
Elim list_of_staticptrs.
  Contradiction.

  Intros.  
  Simpl in H2.
  Decompose [or] H2.
    Rewrite H3.  
    Simpl.
    EAuto with temp.

    Simpl.
    EAuto with temp.
Qed.

  
Lemma double_or_lemma : (A,B,C,D:Prop)
  A\/B ->
  A\/C ->
  (A->D)->
  (B->C->D)->
   D.
Proof.
Tauto.
Qed.

Hints Resolve apart_sym : temp.

Lemma null_staticptr_start_mem : (E:exp)(T:javatype)
  (given_staticptr E T) ->
  (SZ:nat)(jsize T SZ) ->
  (seln SZ start_mem E)=Null.
Proof.
Intros.
Rewrite (jsize_unique ? ? ? H0 (jsize_lemma T)).
Unfold start_mem.
Generalize (all_staticptrs_in_list E T H).
Generalize (list_all_staticptrs).
Elim list_of_staticptrs.
  Contradiction.

  Intros. 
  NewDestruct a.
  Assert E=e/\T=j\/(apart E (jsize_of T) e (jsize_of j)).
    EApply staticptr_equal_or_apart; Try Prolog [jsize_lemma] 1.
    EApply H2; Simpl; Auto.
  Simpl in H3.
  EApply double_or_lemma.
    EExact H4.

    Decompose [or] H3.
      Injection H5; Auto.    
 
      Right; EExact H5.

    Intros (eq1,eq2). 
    Rewrite eq1; Rewrite eq2.
    Simpl.
    EApply updn_seln.    
    EAuto with temp.

    Intros.
    Simpl.
    Rewrite updn_seln_apart; EAuto with temp.
    Fold (jsize_of T).
    Fold (jsize_of j).
    Rewrite <- brute_alloc_alias.
      EApply H1; EAuto.
      Intros.
      EApply H2.
      Simpl.
      Auto.

      EApply addr_staticptr_start_mem_lemma.   
      Assumption.
Qed.

Definition start_state : state' :=
  (mkstate'
      (mkstate Null Null start_mem (nil ?))
      nilrep
      start_mem).


Hint ofType : axioms := Constructors ofType.
Hint ptr : axioms := Constructors ptr.
Hint ofmem : axioms := Constructors ofmem.
Hint jsize : axioms := Constructors jsize.


Definition start_ofType [e:exp][t:type] :=
   ((C:exp)(t=(jvirtab C) -> False)) /\
  ((e=Null) \/ (EX s:javasimpletype | t=s) \/ (t=jclassdesc)).
  
Definition start_ptr [e:exp][r:rorw][t:type] :=
    (EX s:javatype | r=rw /\ t=s /\ (given_staticptr e s)).

Definition start_ofmem [m:mem] :=
  ((e:exp)(r:rorw)(t:type)(sz:nat)
  (jsize t sz) ->
  (start_ptr e r t) ->
  (start_ofType (seln sz m e) t)) /\ 
  ((e:exp)(r:rorw)(t:type)(sz:nat)
  (jsize t sz) ->
  (start_ptr e r t) ->
  (addr sz m e)).


Lemma start_state_preds : 
  (
    (e:exp; t:type)(ofType start_state e t)->
    (start_ofType e t)    
  ) /\ (
    (e:exp; r:rorw; t:type)(ptr start_state e r t)->
    (start_ptr e r t)
  ) /\ (
    (m:mem)(ofmem start_state m)->
    (start_ofmem m)
  ).
Proof.
Apply ofType_ptr_ofmem_simul_ind;
  Unfold start_ofmem start_ofType start_ptr;
  Try (Split; [Solve [Intros; Discriminate_something] | EAuto with axioms]);
  Intros; EAuto with axioms.
  
  Decompose [and or] H1; Auto; Try Discriminate_something.
  Decompose [ex] H3; Discriminate_something.

  Decompose [and or] H0; Auto; Try Discriminate_something.
  Decompose [ex] H2; Discriminate_something.

  Decompose [and] H3.
  Unfold sel4.
  EAuto.

  Decompose [and] H3.
  Unfold sel8.
  EAuto.

  Contradiction.

  Contradiction.

(* ptr cases *)
  Decompose [and or] H0; Try Discriminate_something.  
    Rewrite H4 in H1; Inversion H1 using nonnull_null_inv.
    
    Decompose [ex] H3; Discriminate_something.

  Decompose [and] H0.  
  ElimType False; EAuto.

  Decompose [and or] H1; Try Discriminate_something.
    Rewrite H5 in H2; Inversion H2 using nonnull_null_inv.
    
    Decompose [ex] H4; Discriminate_something.

  Decompose [and] H1.
  ElimType False; EAuto.

  Decompose [and or] H0; Try Discriminate_something.
    Rewrite H4 in H1; Inversion H1 using nonnull_null_inv.

    Decompose [ex] H3; Discriminate_something.

  Decompose [and or] H0; Try Discriminate_something.
    Rewrite H8 in H3; Inversion H3 using nonnull_null_inv.

    Decompose [ex] H7; Discriminate_something.

  Decompose [and or] H0; Try Discriminate_something.
    Rewrite H4 in H1; Inversion H1 using nonnull_null_inv.

    Decompose [ex] H3; Discriminate_something.

  Contradiction.
  
(* ofmem cases *)
  Decompose [and] H5; Clear H5.
  Split; Intros.
    Decompose [and ex] H8.
    Rewrite H9; Rewrite H9 in H5.
    Decompose [and ex] H0.
    Rewrite H11 in H1.
    Unfold upd4.
    Elim (staticptr_equal_or_apart e ADDR x x0 sz (4)); Auto.
      Intros (eq1,eq2).
      Rewrite eq1.  
      Rewrite <-eq2 in H1.
      Rewrite (jsize_unique ? ? ? H5 H1).   
      Rewrite updn_seln.
        Rewrite eq2; Rewrite <- H11.
        Assumption.

        EApply H7; EAuto.
        Rewrite H9 in H8; Rewrite eq1 in H8.
        EAuto.

      Intros.
      Rewrite updn_seln_apart; EAuto with temp.
      Unfold upd4.
      EApply addr_updn; EAuto.

(* similarly for (8) *)
  Decompose [and] H5; Clear H5.
  Split; Intros.
    Decompose [and ex] H8.
    Rewrite H9; Rewrite H9 in H5.
    Decompose [and ex] H0.
    Rewrite H11 in H1.
    Unfold upd8.
    Elim (staticptr_equal_or_apart e ADDR x x0 sz (8)); Auto.
      Intros (eq1,eq2).
      Rewrite eq1.  
      Rewrite <-eq2 in H1.
      Rewrite (jsize_unique ? ? ? H5 H1).   
      Rewrite updn_seln.
        Rewrite eq2; Rewrite <- H11.
        Assumption.

        EApply H7; EAuto.
        Rewrite H9 in H8; Rewrite eq1 in H8.
        EAuto.

      Intros.
      Rewrite updn_seln_apart; EAuto with temp.
      Unfold upd8.
      EApply addr_updn; EAuto.

(* Now last_alloc *)
  Unfold last_alloc_of start_state.
  Split; Intros.
    Decompose [ex and] H0.
    Split; Intros.
      Rewrite H1 in H3; Discriminate H3.

      Left.
      Rewrite H1 in H.
      EApply null_staticptr_start_mem; EAuto.

    Decompose [ex and] H0.
    Rewrite H1 in H.
    EApply addr_staticptr_start_mem; EAuto.
Qed.

Lemma start_state_ptr : 
    (e:exp; r:rorw; t:type)(ptr start_state e r t)->
    (start_ptr e r t).
Proof.
EApply proj1.
EApply proj2.
EExact start_state_preds.
Qed.

Lemma invariant_start_state : (invariant start_state).
Proof.
Unfold_invar_Goal; Intros.
  Assert H1 := (start_state_ptr ? ? ? H0).    
  Unfold start_ptr in H1.
  Decompose [ex and] H1.
  Rewrite H2 in H.
  EApply addr_staticptr_start_mem; EAuto.
  
  Assert H3 := (start_state_ptr ? ? ? H).    
  Unfold start_ptr in H3.
  Decompose [ex and] H3.
  Assert H8 := (start_state_ptr ? ? ? H1).    
  Unfold start_ptr in H8.
  Decompose [ex and] H8.
  Rewrite H4 in H0.
  Rewrite H6 in H2. 
  Elim (staticptr_equal_or_apart ? ? ? ? ? ? H7 H0 H11 H2); EAuto.
  Intros (eq1,eq2).
  Left. 
  Repeat Split; Auto.
  Rewrite H4.   
  Rewrite H6.
  Rewrite eq2.
  Reflexivity. 

  EApply addr_virtab_start_mem; EAuto.
  Assert H1 := (start_state_ptr ? ? ? H).    
  Unfold start_ptr in H1.
  Decompose [ex and] H1.
  Rewrite H2 in H0.
  EApply staticptr_virtab_apart; EAuto.

  Replace (mem_of' start_state) with (last_alloc_of start_state);
      [Idtac | Reflexivity].
  Constructor.
Qed.

End start.