Require Arith. Require Omega. Require machine. Require axioms. Require traux. Require jsize. Require invar. Require induction. Require lemmas. Require java. (* need virtab_size_four *) Section allocinv. Hint ofType : axioms := Constructors ofType. Hint ptr : axioms := Constructors ptr. Hint ofmem : axioms := Constructors ofmem. Hint jsize : axioms := Constructors jsize. Definition new_simple_ofType [s:state'] [T:javasimpletype][SZ:nat][jsz:(jsize T SZ)] [e:exp][t:type] : Prop := (ofType s e t) \/ t=jlong \/ t=jfloat \/ t=jdouble. Definition new_simple_ptr [s:state'] [T:javasimpletype][SZ:nat][jsz:(jsize T SZ)] [s2 := (allocate_simple_type T SZ jsz s)] [e:exp][r:rorw][t:type] : Prop := ((ptr s e r t)\/(e=(rega_of' s2) /\ t=T /\ r=rw)). Definition new_simple_ofmem [s:state'] [T:javasimpletype][SZ:nat][jsz:(jsize T SZ)] [s2 := (allocate_simple_type T SZ jsz s)] [m:mem] : Prop := ( (e:exp)(r:rorw)(t:type)(sz:nat) (new_simple_ptr s T SZ jsz e r t) -> (jsize t sz) -> (new_simple_ofType s T SZ jsz (seln sz m e) t) ) /\ ( (a:exp)(t:javatype) (new_simple_ofType s T SZ jsz a (jarray t)) -> (nonnull a) -> (sel4 m (plus a (4))) = (sel4 (mem_of' s) (plus a (4))) ) /\ ( ((e:exp; r:rorw; t:type)(sz: nat) (new_simple_ptr s T SZ jsz e r t) -> (jsize t sz) -> (addr sz m e)) ). Lemma simple_newptr_equal_or_apart : (s:state') (T:javasimpletype)(SZ:nat)(jsz:(jsize T SZ)) (invariant s) -> (e1,e2:exp; RW:rorw; T1,T2:type; SZ1,SZ2:nat) (new_simple_ptr s T SZ jsz e1 rw T1) ->(jsize T1 SZ1) ->(new_simple_ptr s T SZ jsz e2 RW T2) ->(jsize T2 SZ2) ->e1=e2/\rw=RW/\T1=T2\/(apart e1 SZ1 e2 SZ2). Proof. Unfold new_simple_ptr. Intros. Unfold_invar H. Decompose [and or] H0; Decompose [and or] H2; EAuto. Right. Rewrite H11. Unfold rega_of' allocate_simple_type machine_state_of. Fold (machine_state_of s). Rewrite H10 in H3. Rewrite (jsize_unique ? ? ? H3 jsz). EApply allocate_addr_apart; EAuto. Rewrite_4or8 SZ; Auto with arith. Rewrite_4or8 SZ1; Auto with arith. Right. Rewrite H10. Unfold rega_of' allocate_simple_type machine_state_of. Fold (machine_state_of s). Rewrite H8 in H1. Rewrite (jsize_unique ? ? ? H1 jsz). Apply apart_sym. EApply allocate_addr_apart; EAuto. Rewrite_4or8 SZ; Auto with arith. Rewrite_4or8 SZ2; Auto with arith. Left. Rewrite H10; Rewrite H13. Rewrite H15. Rewrite H8; Rewrite H11. Auto. Qed. Lemma allocate_simple_type_effects : (s:state')(T:javasimpletype) (SZ:nat)(jsz:(jsize T SZ)) (invariant s) -> [s2 := (allocate_simple_type T SZ jsz s)] ( (e:exp; t:type)(ofType s2 e t)-> (new_simple_ofType s T SZ jsz e t) ) /\ ( (e:exp; r:rorw; t:type)(ptr s2 e r t)-> (new_simple_ptr s T SZ jsz e r t) ) /\ ( (m:mem)(ofmem s2 m)-> (new_simple_ofmem s T SZ jsz m) ). Proof. Intros. Apply ofType_ptr_ofmem_simul_ind; Unfold new_simple_ofmem new_simple_ofType new_simple_ptr; EAuto with axioms; Intros. NewDestruct H2; EAuto with axioms. Discriminate_some3. NewDestruct H1; EAuto with axioms. Discriminate_some3. Decompose [and] H4. Unfold sel4. EAuto with axioms. Decompose [and] H4. Unfold sel8. EAuto with axioms. Simpl in H0. Decompose [and or] H0. Discriminate H2. EAuto with axioms. Simpl in H0. Decompose [and or] H0. Discriminate H2. EAuto with axioms. Decompose [or] H1; Try Discriminate_something. EAuto with axioms. Decompose [or] H1; Try Discriminate_something. EAuto with axioms. Decompose [or] H2; Try Discriminate_something. EAuto with axioms. Decompose [or] H2; Try Discriminate_something. EAuto with axioms. Decompose [or] H1; Try Discriminate_something. EAuto with axioms. Decompose [and] H3. Decompose [or] H1; Try Discriminate_something. Rewrite (H9 A T0) in H6; EAuto. Unfold_invar H. EAuto with axioms. Decompose [or] H1; Try Discriminate_something. EAuto with axioms. Simpl in H0. Decompose [and or] H0. Rewrite H4; EAuto. EAuto with axioms. (* Now the ofmem cases *) Decompose [and] H6. Split; [Intros | Split; Intros]. Unfold_invar H. Unfold upd4. Decompose [and or] (simple_newptr_equal_or_apart s T SZ jsz H ADDR e r T0 t (4) sz H1 H2 H8 H11). Rewrite H18. Rewrite H20 in H2. Rewrite (jsize_unique ? ? ? H11 H2). Rewrite updn_seln; EAuto. Rewrite H20 in H4; Assumption. Rewrite updn_seln_apart; EAuto. Unfold sel4 upd4. NewDestruct H8; [Idtac | Discriminate_some3]. Assert (ptr s (plus a (4)) ro jint); [EAuto with axioms | Idtac]. Assert (new_simple_ptr s T SZ jsz (plus a (4)) ro jint); [Unfold new_simple_ptr; EAuto | Idtac]. Decompose [and or] (simple_newptr_equal_or_apart s T SZ jsz H ADDR (plus a (4)) ro T0 jint (4) (4) H1 H2 H13 szint). Discriminate H14. Rewrite updn_seln_apart; EAuto. Unfold upd4. Apply addr_updn; EAuto. (* an entirely similar case for (8) *) Decompose [and] H6. Split; [Intros | Split; Intros]. Unfold_invar H. Unfold upd8. Decompose [and or] (simple_newptr_equal_or_apart s T SZ jsz H ADDR e r T0 t (8) sz H1 H2 H8 H11). Rewrite H18. Rewrite H20 in H2. Rewrite (jsize_unique ? ? ? H11 H2). Rewrite updn_seln; EAuto. Rewrite H20 in H4; Assumption. Rewrite updn_seln_apart; EAuto. Unfold sel4 upd8. NewDestruct H8; [Idtac | Discriminate_some3]. Assert (ptr s (plus a (4)) ro jint); [EAuto with axioms | Idtac]. Assert (new_simple_ptr s T SZ jsz (plus a (4)) ro jint); [Unfold new_simple_ptr; EAuto | Idtac]. Decompose [and or] (simple_newptr_equal_or_apart s T SZ jsz H ADDR (plus a (4)) ro T0 jint (8) (4) H1 H2 H13 szint). Discriminate H14. Rewrite updn_seln_apart; EAuto. Unfold upd8. Apply addr_updn; EAuto. (* Finally the case of last_alloc *) Unfold_invar H. Split; [Intros | Split; Intros]. Decompose [and or] H4. Unfold s2 last_alloc_of allocate_simple_type. Rewrite allocate_alias; EAuto. Left. Rewrite_4or8 sz; EAuto with axioms. Rewrite H7. Case T; EAuto with axioms. Unfold s2 last_alloc_of allocate_simple_type. Unfold sel4. Rewrite allocate_alias; EAuto. NewDestruct H4; [Idtac | Discriminate_some3]. EAuto with axioms. Decompose [and or] H4. Unfold s2 last_alloc_of allocate_simple_type. EApply allocate_preserves; EAuto. Rewrite H8. Unfold s2 last_alloc_of allocate_simple_type rega_of' machine_state_of. Fold (machine_state_of s). Rewrite H7 in H6. Rewrite (jsize_unique ? ? ? H6 jsz). EApply allocate_works; EAuto. Qed. Lemma allocate_simple_type_effects_ptr : (s:state')(T:javasimpletype) (SZ:nat)(jsz:(jsize T SZ)) (invariant s) -> [s2 := (allocate_simple_type T SZ jsz s)] (e:exp; r:rorw; t:type)(ptr s2 e r t)-> (new_simple_ptr s T SZ jsz e r t). Proof. Intros until s2. EApply proj1. EApply proj2. Unfold s2. EApply allocate_simple_type_effects. Assumption. Qed. Lemma allocate_simple_type_respects : (s:state')(T:javasimpletype) (SZ:nat)(jsz:(jsize T SZ)) (invariant s) -> [s2 := (allocate_simple_type T SZ jsz s)] (invariant s2). Proof. Intros. Unfold_invar H. Unfold_invar_Goal. Intros. Assert (new_simple_ptr s T SZ jsz E RW T0); [EApply allocate_simple_type_effects_ptr; EAuto | Idtac]. Unfold s2 mem_of' allocate_simple_type machine_state_of. Fold (machine_state_of s). Unfold new_simple_ptr in H7. Decompose [and or] H7. EApply allocate_preserves; EAuto. Rewrite H9. Unfold rega_of' allocate_simple_type machine_state_of. Fold (machine_state_of s). Rewrite H8 in H4; Rewrite (jsize_unique ? ? ? H4 jsz). EApply allocate_works; EAuto. Intros. Unfold s2 in H4. Unfold s2 in H7. (* tried: EApply simple_newptr_equal_or_apart; EAuto. EApply allocate_simple_type_effects_ptr; EAuto. EExact H3. get: Error: w_Unify *) EApply simple_newptr_equal_or_apart with T:=T SZ:=SZ jsz:=jsz; EAuto; EApply allocate_simple_type_effects_ptr; EAuto. Intros. Unfold mem_of' s2 allocate_simple_type machine_state_of. Fold (machine_state_of s). EApply allocate_preserves. EAuto. Intros. Assert (new_simple_ptr s T SZ jsz e rw T0); [EApply allocate_simple_type_effects_ptr; EAuto | Idtac]. Unfold new_simple_ptr in H7. Decompose [and or] H7. EAuto. EApply apart_sym. Rewrite H9. Unfold rega_of' allocate_simple_type machine_state_of. Rewrite H8 in H6. Rewrite (jsize_unique ? ? ? H6 jsz). EApply allocate_addr_apart; EAuto. Rewrite_4or8 SZ; Omega. Generalize (virtab_size_four C); Intro. Omega. Replace (mem_of' s2) with (last_alloc_of s2). EAuto with axioms. Reflexivity. Qed. (***) (* Now jinstof *) (***) Definition new_jinstof_ofType [s:state'] [C:exp] [s2 := (allocate_jinstof C s)] [e:exp][t:type] : Prop := (ofType s e t) \/ (e=(rega_of' s2) /\ (EX D:exp | (jextends C D) /\ t=(jinstof D))) \/ (e=(loc_of_virtab C) /\ (EX D:exp | (jextends C D) /\ t=(jvirtab D))) \/ t=jclassdesc \/ (EX SIG:exp | t=(jimplof SIG)) \/ t=jlong \/ t=jfloat \/ t=jdouble. Definition new_jinstof_ptr [s:state'] [C:exp] [s2 := (allocate_jinstof C s)] [e:exp][r:rorw][t:type] : Prop := (ptr s e r t)\/ (r=rw /\ (EX OFF:nat | (EX T:javatype | (jifield C OFF T) /\ t=T /\ e=(plus (rega_of' s2) OFF)))) \/ (r=ro /\ e=(rega_of' s2) /\ (EX D:exp | (jextends C D) /\ t=(jvirtab D))) \/ (r=ro /\ e=(loc_of_virtab C) /\ t=jclassdesc) \/ (r=ro /\ (EX OFF:nat | (EX SIG:exp | (jvmethod C OFF SIG) /\ e=(plus (loc_of_virtab C) OFF) /\ t=(jimplof SIG)))). Definition new_jinstof_ofmem [s:state'] [C:exp] [s2 := (allocate_jinstof C s)] [m:mem] : Prop := ( (e:exp)(r:rorw)(t:type)(sz:nat) (new_jinstof_ptr s C e r t) -> (jsize t sz) -> (new_jinstof_ofType s C (seln sz m e) t) ) /\ ( (a:exp)(t:javatype) (new_jinstof_ofType s C a (jarray t)) -> (nonnull a) -> (sel4 m (plus a (4))) = (sel4 (mem_of' s) (plus a (4))) ) /\ ( ((e:exp; r:rorw; t:type)(sz: nat) (new_jinstof_ptr s C e r t) -> (jsize t sz) -> (addr sz m e)) ). Hints Unfold new_jinstof_ofType new_jinstof_ptr new_jinstof_ofmem : temp1. Hints Resolve virtab_size_good : java1. Hints Resolve jextends_transitive : java1. Hints Resolve jextends_reflexive : java1. Hints Resolve jvmethod_extends : java1. Hints Resolve jifield_extends : java1. Hints Resolve virtab_size_four : java1. Hints Resolve instance_size_four : java1. Hints Resolve field_size_good : java1. Lemma allocate_jinstof_upd_addr : (s:state')(C:exp) [s' := (allocate (size_of_instance C) (machine_state_of s))] (addr (4) (mem_of s') (rega_of s')). Proof. Intros. Replace (rega_of s') with (plus (0) (rega_of s')); Try Reflexivity. Unfold s'. EApply addr_closed. EApply allocate_works. Simpl. EApply instance_size_four. Qed. Lemma new_jinstof_ptr_equal_or_apart : (s:state') (C:exp) (invariant s) -> (e1,e2:exp; RW:rorw; T1,T2:type; SZ1,SZ2:nat) (new_jinstof_ptr s C e1 rw T1) ->(jsize T1 SZ1) ->(new_jinstof_ptr s C e2 RW T2) ->(jsize T2 SZ2) ->e1=e2/\rw=RW/\T1=T2\/(apart e1 SZ1 e2 SZ2). Proof. Unfold new_jinstof_ptr. Intros. Unfold_invar H. LetTac s' := (allocate (size_of_instance C) (machine_state_of s)). Decompose [and or ex] H0; Decompose [and or ex] H2; Clear H0 H2; Try Discriminate_something. (* two old ptrs *) EAuto. (* old ptr and field *) Right. Assert (apart e1 SZ1 (rega_of' (allocate_jinstof C s)) (size_of_instance C)). Replace (rega_of' (allocate_jinstof C s)) with (rega_of s'); Try Reflexivity. Unfold s'; EApply allocate_addr_apart; EAuto. Generalize (instance_size_four C); Omega. Rewrite_4or8 SZ1; Omega. Rewrite H12 in H3. Rewrite H14. Generalize (field_size_good ? ? ? ? H11 H3). Generalize H0; Clear H0. Unfold apart. Rewrite_4or8 SZ2; Intros; Omega. (* old and jvirtab *) Right. EApply apart_extend_right. Rewrite H10. Replace (rega_of' (allocate_jinstof C s)) with (rega_of s'); Try Reflexivity. Unfold s'; EApply allocate_addr_apart. Generalize (instance_size_four C); Omega. Rewrite_4or8 SZ1; Omega. EAuto. Rewrite H14 in H3; Rewrite (jsize_unique ? ? ? H3 (szvirtab x)). EAuto with java1. (* old and jclassdesc *) Right. EApply apart_extend_right. Rewrite H11; EAuto. Rewrite H13 in H3; Rewrite (jsize_unique ? ? ? H3 szcdesc). EAuto with java1. (* old and jimplof *) Right. Rewrite H12. EApply apart_shift_right. EAuto. Rewrite H14 in H3; Rewrite (jsize_unique ? ? ? H3 (szjimplof x0)). EAuto with java1. Rewrite_4or8 SZ2; Omega. (* field and old *) Right. EApply apart_sym. Rewrite H13. EApply apart_shift_right. Replace (rega_of' (allocate_jinstof C s)) with (rega_of s'); Try Reflexivity. Unfold s'; EApply allocate_addr_apart. Generalize (instance_size_four C); Omega. Rewrite_4or8 SZ2; Omega. EAuto. Rewrite H11 in H1. EAuto with java1. Rewrite_4or8 SZ1; Omega. (* field and field *) Rewrite H11 in H1. Rewrite H17. Rewrite H15 in H3. Rewrite H13. Generalize (fields_equal_or_apart ? ? ? ? ? ? ? H10 H14 H1 H3). Intros [(eq1,eq2)|apart1]. Left. Rewrite H12. Rewrite H15; Rewrite H11; Rewrite eq2. Rewrite eq1. Repeat Split; Trivial. Right. EApply apart_move_both; EAuto. (* field and virtab *) Right. Rewrite H13. Rewrite H12. Rewrite H17 in H3; Rewrite (jsize_unique ? ? ? H3 (szvirtab x1)). Generalize (jifield_four ? ? ? H10). Unfold apart. Intros. Omega. (* field and classdesc *) Right. EApply apart_sym. Rewrite H14; Rewrite H13. EApply apart_shift_right. Replace (rega_of' (allocate_jinstof C s)) with (rega_of s'); Try Reflexivity. Unfold s'; EApply allocate_addr_apart. Generalize (instance_size_four C); Omega. Rewrite_4or8 SZ2; Omega. Replace (loc_of_virtab C) with (plus (0) (loc_of_virtab C)); Try Reflexivity. EApply addr_closed. EAuto. Rewrite H16 in H3; Rewrite (jsize_unique ? ? ? H3 szcdesc). Simpl. EAuto with java1. Rewrite H11 in H1. EAuto with java1. Rewrite_4or8 SZ1; Omega. (* field and jimplof *) Right. EApply apart_sym. Rewrite H15; Rewrite H13. EApply apart_shift_right. Replace (rega_of' (allocate_jinstof C s)) with (rega_of s'); Try Reflexivity. Unfold s'; EApply allocate_addr_apart. Generalize (instance_size_four C); Omega. Rewrite_4or8 SZ2; Omega. Rewrite plus_sym. EApply addr_closed. EAuto. Rewrite H17 in H3; Rewrite (jsize_unique ? ? ? H3 (szjimplof x2)). EAuto with java1. Rewrite H11 in H1. EAuto with java1. Rewrite_4or8 SZ1; Omega. Qed. Lemma allocate_jinstof_effects_ptr : (s:state') (C:exp) (invariant s) -> [s2 := (allocate_jinstof C s)] (e:exp; r:rorw; t:type)(ptr s2 e r t)-> (new_jinstof_ptr s C e r t). Proof. Intros. Elim H0 using ptr_etc_ind with P:=(new_jinstof_ofType s C) P1:=(new_jinstof_ofmem s C); Try Solve [Unfold new_jinstof_ofmem new_jinstof_ofType new_jinstof_ptr; EAuto with axioms]; Intros. (* ext *) Unfold new_jinstof_ofType in H3. Decompose [and or ex] H3; EAuto with axioms temp1; Try Discriminate_something. Injection H7; Intro. Rewrite <- H5 in H6. EAuto 8 with java1 temp1. (* jarrObject *) Unfold new_jinstof_ofType in H2. Decompose [and or ex] H2; EAuto with axioms temp1; Try Discriminate_something. (* ty4 *) Unfold sel4. Unfold new_jinstof_ofmem in H5; Decompose [and] H5; EAuto. (* ty8 *) Unfold sel8. Unfold new_jinstof_ofmem in H5; Decompose [and] H5; EAuto. (* hyp_jinstof *) Simpl in H1. Decompose [and or] H1; EAuto with axioms temp1. Right. Injection H5; Intro. Rewrite H4. Rewrite H2. EAuto with java1. (* hyp_jarray *) Simpl in H1. Decompose [and or] H1; EAuto with axioms temp1. Discriminate H5. (* ptrvirtab *) Unfold new_jinstof_ofType in H2. Decompose [and or ex] H2; EAuto with axioms temp1; Try Discriminate_something. Right. Right; Left. Injection H7; Intro. Rewrite <- H5 in H6. EAuto. (* ptrcdesc *) Unfold new_jinstof_ofType in H2. Decompose [and or ex] H2; EAuto with axioms temp1; Try Discriminate_something. Right. Right; Right; Left. Auto. (* instFld *) Unfold new_jinstof_ofType in H3. Decompose [and or ex] H3; EAuto with axioms temp1; Try Discriminate_something. Injection H8; Intro eq1; Rewrite <- eq1 in H7. Rewrite H5. EAuto 10 with java1 temp1. (* ptrvmethod *) Unfold new_jinstof_ofType in H3. Decompose [and or ex] H3; EAuto with axioms temp1; Try Discriminate_something. Injection H7; Intro eq1; Rewrite <- eq1 in H6. Rewrite H5. EAuto 12 with java1 temp1. (* arrLen *) Unfold new_jinstof_ofType in H2. Decompose [and or ex] H2; EAuto with axioms temp1; Try Discriminate_something. (* arrElem *) Unfold new_jinstof_ofType in H2. Decompose [and or ex] H2; EAuto with axioms temp1; Try Discriminate_something. Unfold new_jinstof_ofmem in H4; Decompose [and] H4. Left. Unfold_invar H. EApply arrElem; EAuto. Rewrite <- H11 with t:=T; EAuto. (* ptrvirtabarr *) Unfold new_jinstof_ofType in H2. Decompose [and or ex] H2; EAuto with axioms temp1; Try Discriminate_something. (* hyp_simple_type *) Simpl in H1. Decompose [and or] H1; Try Discriminate_something. EAuto with axioms temp1. (* ofmem4 *) Unfold new_jinstof_ofmem in H7. Decompose [and] H7; Clear H7. Split; [Intros | Split; Intros]. Generalize (new_jinstof_ptr_equal_or_apart ? ? H ? ? ? ? ? ? ? H2 H3 H7 H9). Intro Q; Decompose [and or] Q. Unfold upd4. Rewrite <- H15 in H9. Rewrite (jsize_unique ? ? ? H9 H3). Rewrite <- H13. Rewrite updn_seln. Rewrite <- H15; EAuto. EAuto. Unfold upd4. Rewrite updn_seln_apart; EAuto. (* should be tabbed... *) Unfold sel4 upd4. Rewrite updn_seln_apart; EAuto. Unfold new_jinstof_ofType in H7; Decompose [and or ex] H7; Try Discriminate_something. Unfold new_jinstof_ptr in H2; Decompose [and or ex] H2; Try Discriminate_something. Unfold_invar H. Elim H16 with 1:= H13 2:=H3 3:=(arrLen ? ? ? H12 H9) 4:=szint. Intros (x,(y,z)); Discriminate_something. Trivial. EApply apart_sym. Rewrite H17. Replace (rega_of' (allocate_jinstof C s)) with (rega_of (allocate (size_of_instance C) (machine_state_of s))); Try Reflexivity. Assert (apart (plus a (4)) (4) (rega_of (allocate (size_of_instance C) (machine_state_of s))) (size_of_instance C)). EApply allocate_addr_apart; EAuto. Generalize (instance_size_four C); Intro. Omega. Unfold_invar H. EAuto with axioms. Rewrite H15 in H3. Generalize (field_size_good ? ? ? ? H14 H3). Generalize H16. Generalize (size_of_instance C). Intro. Generalize (rega_of (allocate n (machine_state_of s))). Intro m. Clear H3 H16 H17 H15 H14 x0 H13 H12 H9 H7 t0 H11 H10 H8 H6 H5 H4 H2 H1 T E ADDR M H0 t r e s2 H C s. Unfold apart; Intro. Decompose [and or] H16; Clear H16. Left; Omega. Right; Omega. Unfold upd4. EApply addr_updn; EAuto. (* ofmem8 *) Unfold new_jinstof_ofmem in H7. Decompose [and] H7; Clear H7. Split; [Intros | Split; Intros]. Generalize (new_jinstof_ptr_equal_or_apart ? ? H ? ? ? ? ? ? ? H2 H3 H7 H9). Intro Q; Decompose [and or] Q. Unfold upd8. Rewrite <- H15 in H9. Rewrite (jsize_unique ? ? ? H9 H3). Rewrite <- H13. Rewrite updn_seln. Rewrite <- H15; EAuto. EAuto. Unfold upd8. Rewrite updn_seln_apart; EAuto. (* should be tabbed... *) Unfold sel4 upd8. Rewrite updn_seln_apart; EAuto. Unfold new_jinstof_ofType in H7; Decompose [and or ex] H7; Try Discriminate_something. Unfold new_jinstof_ptr in H2; Decompose [and or ex] H2; Try Discriminate_something. Unfold_invar H. Elim H16 with 1:= H13 2:=H3 3:=(arrLen ? ? ? H12 H9) 4:=szint. Intros (x,(y,z)); Discriminate_something. Trivial. EApply apart_sym. Rewrite H17. Replace (rega_of' (allocate_jinstof C s)) with (rega_of (allocate (size_of_instance C) (machine_state_of s))); Try Reflexivity. Assert (apart (plus a (4)) (4) (rega_of (allocate (size_of_instance C) (machine_state_of s))) (size_of_instance C)). EApply allocate_addr_apart; EAuto. Generalize (instance_size_four C); Intro. Omega. Unfold_invar H. EAuto with axioms. Rewrite H15 in H3. Generalize (field_size_good ? ? ? ? H14 H3). Generalize H16. Generalize (size_of_instance C). Intro. Generalize (rega_of (allocate n (machine_state_of s))). Intro m. Clear H3 H16 H17 H15 H14 x0 H13 H12 H9 H7 t0 H11 H10 H8 H6 H5 H4 H2 H1 T E ADDR M H0 t r e s2 H C s. Unfold apart; Intro. Decompose [and or] H16; Clear H16. Left; Omega. Right; Omega. Unfold upd8. EApply addr_updn; EAuto. (* hyp_ofmem *) Clear H0 e r t. Unfold s2; Clear s2. Unfold last_alloc_of allocate_jinstof. Unfold astargetsb4 bgetsn mem_of rega_of regb_of. LetTac s' := (allocate (size_of_instance C) (machine_state_of s)). Fold (mem_of s'). Fold (rega_of s'). Unfold_invar H. Unfold new_jinstof_ofmem. Split; [Intros | Split; Intros]. Unfold new_jinstof_ptr in H4. Decompose [and or ex] H4; Clear H4. Unfold new_jinstof_ofType. Left. Unfold upd4. Rewrite updn_seln_apart. Unfold s'. Rewrite allocate_alias; EAuto. Rewrite_4or8 sz; EAuto with axioms. Replace (rega_of s') with (plus (0) (rega_of s')); Try Reflexivity. Unfold s'. EApply addr_closed. EApply allocate_works. Simpl. EApply instance_size_four. EApply apart_sym. Assert (apart e sz (rega_of s') (size_of_instance C)). Unfold s'. EApply allocate_addr_apart. Generalize (instance_size_four C); Omega. Rewrite_4or8 sz; Omega. Unfold_invar H; EAuto. Generalize (instance_size_four C); Intro. Unfold apart in H4; Unfold apart. Omega. Unfold upd4. Rewrite H9; Rewrite H9 in H6. Rewrite H11. Rewrite updn_seln_apart. Unfold s'. Rewrite plus_sym. Replace (rega_of' (allocate_jinstof C s)) with (rega_of (allocate (size_of_instance C) (machine_state_of s))); Try Reflexivity. Rewrite allocate_zeros. Case x0; EAuto with temp1 axioms. Destruct j; EAuto 10 with temp1 axioms. EApply field_size_good; EAuto. Replace (rega_of s') with (plus (0) (rega_of s')); Try Reflexivity. Unfold s'. EApply addr_closed. EApply allocate_works. Simpl. EApply instance_size_four. Replace (rega_of' (allocate_jinstof C s)) with (rega_of s'); Try Reflexivity. Generalize (jifield_four ? ? ? H8). Unfold apart; Omega. Rewrite H7; Rewrite H11. Unfold upd4. Unfold new_jinstof_ofType. Right; Right; Left. Split; [Idtac | EAuto]. Rewrite H11 in H6; Rewrite (jsize_unique ? ? ? H6 (szvirtab ?)). Rewrite updn_seln; EAuto. Replace (rega_of' (allocate_jinstof C s)) with (plus (0) (rega_of s')); Try Reflexivity. Unfold s'. EApply addr_closed. EApply allocate_works. Simpl. EApply instance_size_four. EAuto 6 with temp1. EAuto 8 with temp1. (* now the *second* part of hyp_ofmem... *) Unfold new_jinstof_ofType in H4. Decompose [and or ex] H4; Clear H4; Try Discriminate_something. Unfold sel4 upd4. Rewrite updn_seln_apart. Unfold s'. Rewrite allocate_alias; EAuto with axioms. Replace (rega_of s') with (plus (0) (rega_of s')); Try Reflexivity. Unfold s'. EApply addr_closed. EApply allocate_works. Simpl. EApply instance_size_four. EApply apart_sym. Assert (apart (plus a (4)) (4) (rega_of s') (size_of_instance C)). Unfold s'. EApply allocate_addr_apart; EAuto with axioms. Generalize (instance_size_four C); Omega. Generalize (instance_size_four C). Unfold apart in H4. Unfold apart. Omega. (* Now, finally, the third part of hyp_ofmem *) Unfold new_jinstof_ptr in H4; Decompose [and or ex] H4; Clear H4. Unfold upd4; EApply addr_updn. Replace (rega_of s') with (plus (0) (rega_of s')); Try Reflexivity. Unfold s'. EApply addr_closed. EApply allocate_works. Simpl. EApply instance_size_four. Unfold s'. EApply allocate_preserves. EAuto. Unfold upd4; EApply addr_updn. Unfold s'; EApply allocate_jinstof_upd_addr. Rewrite H11. Rewrite H9 in H6. Rewrite plus_sym; EApply addr_closed. Replace (rega_of' (allocate_jinstof C s)) with (rega_of s'); Try Reflexivity. Unfold s'; EApply allocate_works. EAuto with java1. Unfold upd4; EApply addr_updn; [ Unfold s'; EApply allocate_jinstof_upd_addr | Idtac]. Rewrite H7. Replace (rega_of' (allocate_jinstof C s)) with (plus (0) (rega_of s')); Try Reflexivity. EApply addr_closed. Unfold s'; EApply allocate_works. Rewrite H11 in H6; Rewrite (jsize_unique ? ? ? H6 (szvirtab x)); Simpl; EAuto with java1. Unfold upd4; EApply addr_updn; [ Unfold s'; EApply allocate_jinstof_upd_addr | Idtac]. Rewrite H8. Replace (loc_of_virtab C) with (plus (0) (loc_of_virtab C)); Try Reflexivity. EApply addr_closed. Unfold s'; EApply allocate_preserves. EAuto. Rewrite H10 in H6; Rewrite (jsize_unique ? ? ? H6 szcdesc); EAuto with java1. Unfold upd4; EApply addr_updn; [ Unfold s'; EApply allocate_jinstof_upd_addr | Idtac]. Rewrite H9; Rewrite plus_sym. EApply addr_closed. Unfold s'; EApply allocate_preserves. EAuto. Rewrite H11 in H6; Rewrite (jsize_unique ? ? ? H6 (szjimplof x0)). EAuto with java1. Qed. Lemma allocate_jinstof_respects : (s:state') (C:exp) (invariant s) -> [s2 := (allocate_jinstof C s)] (invariant s2). Proof. Intros. Unfold_invar H. Unfold_invar_Goal; Intros. Assert (new_jinstof_ptr s C E RW T); [ EApply allocate_jinstof_effects_ptr; EAuto | Idtac]. LetTac s' := (allocate (size_of_instance C) (machine_state_of s)). Replace (mem_of' s2) with (updn (4) (mem_of s') (rega_of s') (loc_of_virtab C)); Try Reflexivity. EApply addr_updn; [Unfold s'; EApply allocate_jinstof_upd_addr; EAuto | Idtac]. Unfold new_jinstof_ptr in H7; Decompose [and or ex] H7; Clear H7. Unfold s'; EApply allocate_preserves; EAuto. Rewrite H12; Rewrite H10 in H4. Rewrite plus_sym; EApply addr_closed. Replace (rega_of' (allocate_jinstof C s)) with (rega_of s'); Try Reflexivity. Unfold s'; EApply allocate_works; EAuto. EAuto with java1. Rewrite H8; Rewrite H12 in H4. Replace (rega_of' (allocate_jinstof C s)) with (plus (0) (rega_of s')); Try Reflexivity. EApply addr_closed. Unfold s'; EApply allocate_works; EAuto. Simpl; Rewrite (jsize_unique ? ? ? H4 (szvirtab x)). EAuto with java1. Rewrite H9; Rewrite H11 in H4. Replace (loc_of_virtab C) with (plus (0) (loc_of_virtab C)); Try Reflexivity. EApply addr_closed. Unfold s'; EApply allocate_preserves; EAuto. Simpl; Rewrite (jsize_unique ? ? ? H4 szcdesc). EAuto with java1. Rewrite H10; Rewrite H12 in H4. Rewrite plus_sym; EApply addr_closed. Unfold s'; EApply allocate_preserves; EAuto. Rewrite (jsize_unique ? ? ? H4 (szjimplof x0)). EAuto with java1. (*two pointers apart*) Assert (new_jinstof_ptr s C e1 rw T1); [ EApply allocate_jinstof_effects_ptr; EAuto | Idtac]. Assert (new_jinstof_ptr s C e2 RW T2); [ EApply allocate_jinstof_effects_ptr; EAuto | Idtac]. EApply new_jinstof_ptr_equal_or_apart; EAuto. (* addr virtab *) LetTac s' := (allocate (size_of_instance C) (machine_state_of s)). Replace (mem_of' s2) with (updn (4) (mem_of s') (rega_of s') (loc_of_virtab C)); Try Reflexivity. EApply addr_updn; [Unfold s'; EApply allocate_jinstof_upd_addr; EAuto | Idtac]. Unfold s'; EApply allocate_preserves; EAuto. (* apart virtab *) Assert (new_jinstof_ptr s C e rw T); [ EApply allocate_jinstof_effects_ptr; EAuto | Idtac]. Unfold new_jinstof_ptr in H7; Decompose [and or ex] H7; Clear H7; Try Discriminate_something. EAuto. Rewrite H12. EApply apart_sym. EApply apart_shift_right. LetTac s' := (allocate (size_of_instance C) (machine_state_of s)). Replace (rega_of' (allocate_jinstof C s)) with (rega_of s'); Try Reflexivity. Unfold s'; EApply allocate_addr_apart; EAuto. Generalize (instance_size_four C); Omega. Generalize (virtab_size_four C0); Omega. Rewrite H10 in H6. EAuto with java1. Rewrite_4or8 SZ; Omega. Replace (mem_of' s2) with (last_alloc_of s2); Try Reflexivity. EAuto with axioms. Qed. (***) (* Now jarray *) (***) Definition new_jarray_ofType [s:state'] [T:javatype][SZ:nat][jsz:(jsize T SZ)][n:nat] [a' := (rega_of (allocate (plus (mult n SZ) (8)) (machine_state_of s)))] [e:exp][t:type] : Prop := (ofType s e t) \/ (e=a' /\ t=(jarray T)) \/ (e=a' /\ t=(jinstof _4java4lang6Object_C)) \/ (e=(loc_of_virtab _4java4lang6Object_C) /\ t=(jvirtab _4java4lang6Object_C)) \/ t=jclassdesc \/ (EX SIG:exp | t=(jimplof SIG)) \/ t=jlong \/ t=jfloat \/ t=jdouble. Definition new_jarray_ptr [s:state'] [T:javatype][SZ:nat][jsz:(jsize T SZ)][n:nat] [a' := (rega_of (allocate (plus (mult n SZ) (8)) (machine_state_of s)))] [s2 := (allocate_jarray T SZ jsz n s)] [e:exp][r:rorw][t:type] : Prop := (ptr s e r t)\/ (r=ro /\ e=a' /\ t=(jvirtab _4java4lang6Object_C)) \/ (r=ro /\ e=(loc_of_virtab _4java4lang6Object_C) /\ t=jclassdesc) \/ (r=ro /\ (EX OFF:nat | (EX SIG:exp | (jvmethod _4java4lang6Object_C OFF SIG) /\ e=(plus (loc_of_virtab _4java4lang6Object_C) OFF) /\ t=(jimplof SIG)))) \/ (r=ro /\ e=(plus a' (4)) /\ t=jint) \/ (r=rw /\ t=T /\ (EX IDX:nat | (lt IDX n) /\ e=(plus a' (plus (mult IDX SZ) (8))))). Definition new_jarray_ofmem [s:state'] [T:javatype][SZ:nat][jsz:(jsize T SZ)][n:nat] [a' := (rega_of (allocate (plus (mult n SZ) (8)) (machine_state_of s)))] [m:mem] : Prop := ( (e:exp)(r:rorw)(t:type)(sz:nat) (new_jarray_ptr s T SZ jsz n e r t) -> (jsize t sz) -> (new_jarray_ofType s T SZ jsz n (seln sz m e) t) ) /\ ( (a:exp)(t:javatype) (ofType s a (jarray t)) -> (nonnull a) -> (sel4 m (plus a (4))) = (sel4 (mem_of' s) (plus a (4))) ) /\ ( (sel4 m (plus a' (4))) = n ) /\ ( ((e:exp; r:rorw; t:type)(sz: nat) (new_jarray_ptr s T SZ jsz n e r t) -> (jsize t sz) -> (addr sz m e)) ). Lemma new_jarray_ptr_equal_or_apart : (s:state') (T:javatype)(SZ:nat)(jsz:(jsize T SZ))(n:nat) (invariant s) -> (e1,e2:exp; RW:rorw; T1,T2:type; SZ1,SZ2:nat) (new_jarray_ptr s T SZ jsz n e1 rw T1) ->(jsize T1 SZ1) ->(new_jarray_ptr s T SZ jsz n e2 RW T2) ->(jsize T2 SZ2) ->e1=e2/\rw=RW/\T1=T2\/(apart e1 SZ1 e2 SZ2). Proof. Unfold new_jarray_ptr. Intros. Unfold_invar H. Decompose [and or ex] H0; Try Discriminate_something; Decompose [and or ex] H2; Clear H0 H2. (* both old *) EAuto. (* old and virtab *) Right. Rewrite H11. EApply allocate_addr_apart_extend; EAuto. LetTac dumb := (mult n SZ); Omega. Rewrite_4or8 SZ1; Omega. LetTac dumb := (mult n SZ); Rewrite_4or8 SZ2; Omega. (* old and classdesc *) Rewrite H10. Right. EApply apart_extend_right; EAuto. Rewrite H13 in H3; Rewrite (jsize_unique ? ? ? H3 szcdesc). EAuto with java1. (* old and jimplof *) Right. Rewrite H12. EApply apart_shift_right; EAuto. Rewrite H14 in H3; Rewrite (jsize_unique ? ? ? H3 (szjimplof x0)). EAuto with java1. Rewrite_4or8 SZ2; Omega. (* old and arrlen *) Right. Rewrite H10. EApply apart_shift_right. EApply allocate_addr_apart; EAuto. LetTac dumb := (mult n SZ); Omega. Rewrite_4or8 SZ1; Omega. Rewrite H13 in H3; Rewrite (jsize_unique ? ? ? H3 szint). LetTac dumb := (mult n SZ); Omega. Rewrite_4or8 SZ2; Omega. (* old and arrelem *) Right. Rewrite H14. EApply apart_shift_right. EApply allocate_addr_apart; EAuto. LetTac dumb := (mult n SZ); Omega. Rewrite_4or8 SZ1; Omega. Rewrite H10 in H3; Rewrite (jsize_unique ? ? ? H3 jsz). Rewrite_4or8 SZ; Omega. Rewrite_4or8 SZ2; Omega. (* arrElem and old *) Right. Rewrite H13. EApply apart_sym. EApply apart_shift_right. EApply allocate_addr_apart; EAuto. LetTac dumb := (mult n SZ); Omega. Rewrite_4or8 SZ2; Omega. Rewrite H8 in H1; Rewrite (jsize_unique ? ? ? H1 jsz). Rewrite_4or8 SZ; Omega. Rewrite_4or8 SZ1; Omega. (* arrElem and virtab *) Right. Rewrite H13; Rewrite H14. Rewrite H8 in H1; Rewrite (jsize_unique ? ? ? H1 jsz). Rewrite H16 in H3; Rewrite (jsize_unique ? ? ? H3 (szvirtab _4java4lang6Object_C)). Unfold apart. Rewrite_4or8 SZ; Omega. (* arrelem and jclassdesc *) Right. Rewrite H13; Rewrite H11. EApply apart_sym. EApply apart_shift_right. EApply allocate_addr_apart. LetTac dumb := (mult n SZ); Omega. Rewrite_4or8 SZ2; Omega. Replace (loc_of_virtab _4java4lang6Object_C) with (plus (0) (loc_of_virtab _4java4lang6Object_C)); Try Reflexivity. EApply addr_closed; EAuto. Rewrite H16 in H3; Rewrite (jsize_unique ? ? ? H3 szcdesc). Simpl; EAuto with java1. Rewrite H8 in H1; Rewrite (jsize_unique ? ? ? H1 jsz). Rewrite_4or8 SZ; Omega. Rewrite_4or8 SZ1; Omega. (* arrelem and jimplof *) Right. Rewrite H13; Rewrite H15. EApply apart_sym. EApply apart_shift_right. EApply allocate_addr_apart. LetTac dumb := (mult n SZ); Omega. Rewrite_4or8 SZ2; Omega. Rewrite plus_sym. EApply addr_closed; EAuto. Rewrite H17 in H3; Rewrite (jsize_unique ? ? ? H3 (szjimplof x1)). EAuto with java1. Rewrite H8 in H1; Rewrite (jsize_unique ? ? ? H1 jsz). Rewrite_4or8 SZ; Omega. Rewrite_4or8 SZ1; Omega. (* arrelem and arrlen *) Right. Rewrite H11; Rewrite H13. Rewrite H8 in H1; Rewrite (jsize_unique ? ? ? H1 jsz). Rewrite H16 in H3; Rewrite (jsize_unique ? ? ? H3 szint). LetTac a :=(rega_of (allocate (plus (mult n SZ) (8)) (machine_state_of s))). Unfold apart. Rewrite_4or8 SZ; Omega. (* arrelem and arrelem *) Rewrite H14; Rewrite H11; Rewrite H8. Rewrite H11 in H3; Rewrite (jsize_unique ? ? ? H3 jsz). Rewrite H8 in H1; Rewrite (jsize_unique ? ? ? H1 jsz). Assert (e1=e2 \/ (apart e1 SZ e2 SZ)). Unfold exp; Unfold apart. Rewrite H13; Rewrite H17. LetTac a := (rega_of (allocate (plus (mult n SZ) (8)) (machine_state_of s))). Clear H1 H3 H17 H11 H14 H13 H8 H10 H H9 H7 H5 H6 H4 SZ2 SZ1 T2 T1 RW. Decompose [sumbool sumor] (lt_eq_lt_dec x x0). Right; Left. Rewrite_4or8 SZ; Omega. Left; Rewrite b; Trivial. Right; Right. Rewrite_4or8 SZ; Omega. Elim H0; Auto. Qed. Hints Unfold new_jarray_ofType new_jarray_ptr new_jarray_ofmem : temp2. Hints Resolve no_object_fields : java1. Lemma allocate_jarray_upd_addr : (s:state') (SZ:nat)(n:nat) [s' := (allocate (plus (mult n SZ) (8)) (machine_state_of s))] (addr (4) (mem_of s') (rega_of s')). Proof. Intros. Replace (rega_of s') with (plus (0) (rega_of s')); Try Reflexivity. Unfold s'. EApply addr_closed. EApply allocate_works. Clear s'. LetTac dumb := (mult n SZ); Omega. Qed. Lemma allocate_jarray_upd_upd_addr : (s:state') (SZ:nat)(n:nat) [s' := (allocate (plus (mult n SZ) (8)) (machine_state_of s))] (addr (4) (mem_of s') (plus (rega_of s') (4))). Proof. Intros. Rewrite plus_sym. Unfold s'. EApply addr_closed. EApply allocate_works. Clear s'. LetTac dumb := (mult n SZ); Omega. Qed. Lemma allocate_works_extend : (n:nat)(s:state)(m:nat) [s2:=(allocate n s)] (le m n) -> (addr m (mem_of s2) (rega_of s2)). Proof. Intros. Replace (rega_of s2) with (plus (0) (rega_of s2)); Try Reflexivity. EApply addr_closed. Unfold s2; EApply allocate_works. Simpl; Assumption. Qed. Lemma allocate_jarray_effects_ptr : (s:state') (T:javatype)(SZ:nat)(jsz:(jsize T SZ))(n:nat) (invariant s) -> [s2 := (allocate_jarray T SZ jsz n s)] (e:exp; r:rorw; t:type)(ptr s2 e r t)-> (new_jarray_ptr s T SZ jsz n e r t). Proof. Intros. Elim H0 using ptr_etc_ind with P:=(new_jarray_ofType s T SZ jsz n) P1:=(new_jarray_ofmem s T SZ jsz n); Try Solve [Unfold new_jarray_ofmem new_jarray_ofType new_jarray_ptr; EAuto with axioms]; Intros. (* ext *) Unfold new_jarray_ofType in H3; Decompose [and or ex] H3; Clear H3; EAuto with temp2 axioms; Try Discriminate_something. Injection H6; Intro. Rewrite H3 in H1. Rewrite (no_object_super D); EAuto. Rewrite H5. EAuto 6 with temp2. (*jarrObject*) Unfold new_jarray_ofType in H2; Decompose [and or ex] H2; Clear H2; EAuto with temp2 axioms; Try Discriminate_something. Rewrite H3. EAuto 6 with temp2. (* ty4 *) Unfold new_jarray_ofmem in H5; Decompose [and] H5; Clear H5. Unfold sel4; EAuto. (* ty8 *) Unfold new_jarray_ofmem in H5; Decompose [and] H5; Clear H5. Unfold sel8; EAuto. (* hyp_jinstof *) Simpl in H1. Decompose [and or] H1; Try Discriminate_something. EAuto with temp2 axioms. (* hyp_jarray *) Simpl in H1. Decompose [and or] H1; Clear H1. Rewrite H2; Rewrite H5. EAuto with temp2. EAuto with temp2 axioms. (* ptrvirtab *) Unfold new_jarray_ofType in H2; Decompose [and or ex] H2; Clear H2; EAuto with temp2 axioms; Try Discriminate_something. Injection H6; Intro eq1; Rewrite eq1. EAuto 6 with temp2. (* ptrcdesc *) Unfold new_jarray_ofType in H2; Decompose [and or ex] H2; Clear H2; EAuto with temp2 axioms; Try Discriminate_something. Rewrite H3. EAuto 7 with temp2. (* instFld *) Unfold new_jarray_ofType in H3; Decompose [and or ex] H3; Clear H3; EAuto with temp2 axioms; Try Discriminate_something. Injection H7; Intro eq1; Rewrite eq1 in H1. ElimType False; EAuto with java1. (* ptrvmethod *) Unfold new_jarray_ofType in H3; Decompose [and or ex] H3; Clear H3; EAuto with temp2 axioms; Try Discriminate_something. Rewrite H4. Injection H6; Intro eq1; Rewrite eq1 in H1. EAuto 11 with temp2. (* arrLen *) Unfold new_jarray_ofType in H2; Decompose [and or ex] H2; Clear H2; EAuto with temp2 axioms; Try Discriminate_something. Rewrite H4. EAuto 9 with temp2. (* arrElem *) Unfold new_jarray_ofType in H2; Decompose [and or ex] H2; Clear H2; EAuto with temp2 axioms; Try Discriminate_something. (* old *) Unfold new_jarray_ofmem in H4; Decompose [and] H4; Clear H4. Rewrite H10 with t:=T0 in H7; EAuto. Unfold new_jarray_ptr; Left. EApply arrElem; EAuto. Unfold_invar H; EAuto. (* new *) Rewrite H8. Injection H10; Intro eq1; Rewrite eq1; Rewrite eq1 in H6. Rewrite (jsize_unique ? ? ? H6 jsz). Unfold new_jarray_ofmem in H4; Decompose [and] H4; Clear H4. Rewrite H8 in H7. Rewrite H9 in H7; EAuto. EAuto 11 with temp2. (* ptrvirtabarr *) Unfold new_jarray_ofType in H2; Decompose [and or ex] H2; Clear H2; EAuto with temp2 axioms; Try Discriminate_something. Rewrite H4. EAuto 6 with temp2. (* hyp_simple_type *) Simpl in H1. Decompose [and or] H1; Try Discriminate_something. EAuto with temp2 axioms. (* ofmem4 *) Unfold new_jarray_ofmem in H7. Decompose [and] H7; Clear H7. Split; [Intros | Split; [Intros | Split; Intros]]. Generalize (new_jarray_ptr_equal_or_apart ? ? ? ? ? H ? ? ? ? ? ? ? H2 H3 H7 H11). Intro Q. Decompose [and or] Q. Unfold upd4. Rewrite <- H16 in H11. Rewrite (jsize_unique ? ? ? H11 H3). Rewrite <- H14. Rewrite updn_seln. Rewrite <- H16; EAuto. EAuto. Unfold upd4. Rewrite updn_seln_apart; EAuto. (*ofmem4 part 2 *) Unfold upd4 sel4. Rewrite updn_seln_apart; EAuto. Assert (new_jarray_ptr s T SZ jsz n (plus a (4)) ro jint); [ EAuto with temp2 axioms | Idtac]. Generalize (new_jarray_ptr_equal_or_apart ? ? ? ? ? H ? ? ? ? ? ? ? H2 H3 H13 szint). Intro Q; Decompose [and or] Q; Try Discriminate_something. Assumption. (* ofmem4 part 3 *) Unfold upd4 sel4. Rewrite updn_seln_apart; EAuto. LetTac a' := (rega_of (allocate (plus (mult n SZ) (8)) (machine_state_of s))). Assert (new_jarray_ptr s T SZ jsz n (plus a' (4)) ro jint); [ Unfold a'; EAuto 9 with temp2 axioms | Idtac]. Generalize (new_jarray_ptr_equal_or_apart ? ? ? ? ? H ? ? ? ? ? ? ? H2 H3 H7 szint). Intro Q; Decompose [and or] Q; Try Discriminate_something. Assumption. (* ofmem4 part 4 *) Unfold upd4. EApply addr_updn; EAuto. (*ofmem8*) Unfold new_jarray_ofmem in H7. Decompose [and] H7; Clear H7. Split; [Intros | Split; [Intros | Split; Intros]]. Generalize (new_jarray_ptr_equal_or_apart ? ? ? ? ? H ? ? ? ? ? ? ? H2 H3 H7 H11). Intro Q. Decompose [and or] Q. Unfold upd8. Rewrite <- H16 in H11. Rewrite (jsize_unique ? ? ? H11 H3). Rewrite <- H14. Rewrite updn_seln. Rewrite <- H16; EAuto. EAuto. Unfold upd8. Rewrite updn_seln_apart; EAuto. (*ofmem4 part 2 *) Unfold upd8 sel4. Rewrite updn_seln_apart; EAuto. Assert (new_jarray_ptr s T SZ jsz n (plus a (4)) ro jint); [ EAuto with temp2 axioms | Idtac]. Generalize (new_jarray_ptr_equal_or_apart ? ? ? ? ? H ? ? ? ? ? ? ? H2 H3 H13 szint). Intro Q; Decompose [and or] Q; Try Discriminate_something. Assumption. (* ofmem4 part 3 *) Unfold upd8 sel4. Rewrite updn_seln_apart; EAuto. LetTac a' := (rega_of (allocate (plus (mult n SZ) (8)) (machine_state_of s))). Assert (new_jarray_ptr s T SZ jsz n (plus a' (4)) ro jint); [ Unfold a'; EAuto 9 with temp2 axioms | Idtac]. Generalize (new_jarray_ptr_equal_or_apart ? ? ? ? ? H ? ? ? ? ? ? ? H2 H3 H7 szint). Intro Q; Decompose [and or] Q; Try Discriminate_something. Assumption. (* ofmem4 part 4 *) Unfold upd8. EApply addr_updn; EAuto. (* hyp_ofmem *) Clear H0 t r e. Unfold_invar H. Simpl. LetTac s' := (allocate (plus (mult n SZ) (8)) (machine_state_of s)). Unfold upd4. Split; [Intros | Split; [Intros | Split; Intros]]. (* part 1 *) Unfold new_jarray_ptr in H4; Decompose [and or ex] H4; Clear H4. Rewrite updn_seln_apart. Rewrite updn_seln_apart. Unfold s'. Rewrite allocate_alias. Generalize H6. Rewrite_4or8 sz; EAuto with temp2 axioms. EAuto. Unfold s'; EApply allocate_jarray_upd_addr. EApply apart_sym. Unfold s'. EApply allocate_addr_apart_extend; EAuto. Clear s'; LetTac dumb := (mult n SZ); Omega. Rewrite_4or8 sz; Omega. Clear s'; LetTac dumb := (mult n SZ); Omega. EApply addr_updn. Unfold s'; EApply allocate_jarray_upd_addr. Unfold s'; EApply allocate_jarray_upd_upd_addr. EApply apart_sym. EApply apart_shift_right. Unfold s'; EApply allocate_addr_apart. Clear s'; LetTac dumb := (mult n SZ); Omega. Rewrite_4or8 sz; Omega. EAuto. Clear s'; LetTac dumb := (mult n SZ); Omega. Omega. (* part 1, jvirtab *) Rewrite updn_seln_apart. Rewrite H10 in H6; Rewrite (jsize_unique ? ? ? H6 (szvirtab _4java4lang6Object_C)). Rewrite H8. Rewrite updn_seln. Rewrite H10. EAuto 7 with temp2. Unfold s'; EApply allocate_works_extend. Clear s'; LetTac dumb := (mult n SZ); Omega. EApply addr_updn. Unfold s'; EApply allocate_jarray_upd_addr. Unfold s'; EApply allocate_jarray_upd_upd_addr. Rewrite H8. Rewrite H10 in H6; Rewrite (jsize_unique ? ? ? H6 (szvirtab _4java4lang6Object_C)). Unfold s'; Unfold apart; Omega. (* part 1, jclassdesc *) Rewrite updn_seln_apart. Rewrite updn_seln_apart. Unfold s'. Rewrite allocate_alias. Rewrite H7; Rewrite H10. Rewrite H10 in H6; Rewrite (jsize_unique ? ? ? H6 szcdesc). EAuto 7 with temp2. Rewrite H7. Rewrite H10 in H6; Rewrite (jsize_unique ? ? ? H6 szcdesc). Replace (loc_of_virtab _4java4lang6Object_C) with (plus (0) (loc_of_virtab _4java4lang6Object_C)); Try Reflexivity. EApply addr_closed; Simpl; EAuto with java1. Unfold s'; EApply allocate_jarray_upd_addr. EApply apart_sym. Unfold s'. EApply allocate_addr_apart_extend; EAuto. Clear s'; LetTac dumb := (mult n SZ); Omega. Rewrite_4or8 sz; Omega. Clear s'; LetTac dumb := (mult n SZ); Omega. Rewrite H7. Rewrite H10 in H6; Rewrite (jsize_unique ? ? ? H6 szcdesc). Replace (loc_of_virtab _4java4lang6Object_C) with (plus (0) (loc_of_virtab _4java4lang6Object_C)); Try Reflexivity. EApply addr_closed; Simpl; EAuto with java1. EApply addr_updn. Unfold s'; EApply allocate_jarray_upd_addr. Unfold s'; EApply allocate_jarray_upd_upd_addr. EApply apart_sym. EApply apart_shift_right. Unfold s'; EApply allocate_addr_apart. Clear s'; LetTac dumb := (mult n SZ); Omega. Rewrite_4or8 sz; Omega. Rewrite H7. Rewrite H10 in H6; Rewrite (jsize_unique ? ? ? H6 szcdesc). Replace (loc_of_virtab _4java4lang6Object_C) with (plus (0) (loc_of_virtab _4java4lang6Object_C)); Try Reflexivity. EApply addr_closed; Simpl; EAuto with java1. Clear s'; LetTac dumb := (mult n SZ); Omega. Omega. (* part 1, jimplof *) Rewrite updn_seln_apart. Rewrite updn_seln_apart. Unfold s'. Rewrite allocate_alias. Rewrite H9; Rewrite H11. Rewrite H11 in H6; Rewrite (jsize_unique ? ? ? H6 (szjimplof x0)). EAuto 10 with temp2. Rewrite H9. Rewrite H11 in H6; Rewrite (jsize_unique ? ? ? H6 (szjimplof x0)). Rewrite plus_sym. EApply addr_closed; Simpl; EAuto with java1. Unfold s'; EApply allocate_jarray_upd_addr. EApply apart_sym. Unfold s'. EApply allocate_addr_apart_extend; EAuto. Clear s'; LetTac dumb := (mult n SZ); Omega. Rewrite_4or8 sz; Omega. Clear s'; LetTac dumb := (mult n SZ); Omega. Rewrite H9. Rewrite H11 in H6; Rewrite (jsize_unique ? ? ? H6 (szjimplof x0)). Rewrite plus_sym. EApply addr_closed; Simpl; EAuto with java1. EApply addr_updn. Unfold s'; EApply allocate_jarray_upd_addr. Unfold s'; EApply allocate_jarray_upd_upd_addr. EApply apart_sym. EApply apart_shift_right. Unfold s'; EApply allocate_addr_apart. Clear s'; LetTac dumb := (mult n SZ); Omega. Rewrite_4or8 sz; Omega. Rewrite H9. Rewrite H11 in H6; Rewrite (jsize_unique ? ? ? H6 (szjimplof x0)). Rewrite plus_sym. EApply addr_closed; Simpl; EAuto with java1. Clear s'; LetTac dumb := (mult n SZ); Omega. Omega. (* part 1, arrLen *) Rewrite H10 in H6; Rewrite (jsize_unique ? ? ? H6 szint). Rewrite H7; Rewrite H10. Rewrite updn_seln. EAuto with temp2 axioms. EApply addr_updn. Unfold s'; EApply allocate_jarray_upd_addr. Rewrite plus_sym; EApply addr_closed. Unfold s'; EApply allocate_works. Clear s'; LetTac dumb := (mult n SZ); Omega. (* part 1, arrelem *) Rewrite H7 in H6; Rewrite (jsize_unique ? ? ? H6 jsz). Rewrite H11; Rewrite H7. Rewrite updn_seln_apart. Rewrite updn_seln_apart. Replace (allocate (plus (mult n SZ) (8)) (machine_state_of s)) with s'; Try Reflexivity. Rewrite (plus_sym (rega_of s')). Unfold s'; Rewrite allocate_zeros. Pattern 2 T; Case T; EAuto with temp2 axioms. Intro j. Case j; EAuto 10 with temp2 axioms. Rewrite_4or8 SZ; Omega. Unfold s'; EApply allocate_jarray_upd_addr. Unfold s'; Clear s'. LetTac dumb := (mult x SZ). Unfold apart. Omega. EApply addr_updn. Unfold s'; EApply allocate_jarray_upd_addr. Rewrite plus_sym; EApply addr_closed. Unfold s'; EApply allocate_works. Clear s'; LetTac dumb := (mult n SZ); Omega. Unfold s'; Clear s'. LetTac dumb := (mult x SZ). Unfold apart. Omega. (* whew. part 2 *) Unfold sel4. Rewrite updn_seln_apart. Rewrite updn_seln_apart. Unfold s'. Rewrite allocate_alias. Reflexivity. EAuto with axioms. Unfold s'; EApply allocate_jarray_upd_addr. EApply apart_sym. Unfold s'. EApply allocate_addr_apart_extend; EAuto. Clear s'; LetTac dumb := (mult n SZ); Omega. Clear s'; LetTac dumb := (mult n SZ); Omega. EAuto with axioms. EApply addr_updn. Unfold s'; EApply allocate_jarray_upd_addr. Unfold s'; EApply allocate_jarray_upd_upd_addr. EApply apart_sym. EApply apart_shift_right. Unfold s'; EApply allocate_addr_apart. Clear s'; LetTac dumb := (mult n SZ); Omega. Omega. EAuto with axioms. Clear s'; LetTac dumb := (mult n SZ); Omega. Omega. (* part 3 *) Replace (allocate (plus (mult n SZ) (8)) (machine_state_of s)) with s'; Try Reflexivity. Unfold sel4. Rewrite updn_seln. Reflexivity. EApply addr_updn. Unfold s'; EApply allocate_jarray_upd_addr. Unfold s'; EApply allocate_jarray_upd_upd_addr. (* part 4 *) EApply addr_updn. EApply addr_updn. Unfold s'; EApply allocate_jarray_upd_addr. Unfold s'; EApply allocate_jarray_upd_upd_addr. EApply addr_updn. Unfold s'; EApply allocate_jarray_upd_addr. Unfold new_jarray_ptr in H4; Decompose [and or ex] H4; Clear H4. Unfold s'; EApply allocate_preserves; EAuto. Rewrite H8. Rewrite H10 in H6; Rewrite (jsize_unique ? ? ? H6 (szvirtab _4java4lang6Object_C)). Unfold s'; EApply allocate_works_extend. Clear s'; LetTac dumb := (mult n SZ); Omega. Replace e with (plus (0) e); Try Reflexivity. Rewrite H7. EApply addr_closed. Unfold s'; EApply allocate_preserves. EAuto. Rewrite H10 in H6; Rewrite (jsize_unique ? ? ? H6 szcdesc). Simpl; EAuto with java1. Rewrite H9. Rewrite plus_sym. EApply addr_closed. Unfold s'; EApply allocate_preserves. EAuto. Rewrite H11 in H6; Rewrite (jsize_unique ? ? ? H6 (szjimplof x0)). EAuto with java1. Rewrite H7. Rewrite plus_sym. EApply addr_closed. Unfold s'; EApply allocate_works. Rewrite H10 in H6; Rewrite (jsize_unique ? ? ? H6 szint). Clear s'; LetTac dumb := (mult n SZ); Omega. Rewrite H11. Rewrite plus_sym. EApply addr_closed. Unfold s'; EApply allocate_works. Rewrite H7 in H6; Rewrite (jsize_unique ? ? ? H6 jsz). Rewrite_4or8 SZ; Omega. Qed. Lemma allocate_jarray_respects : (s:state') (T:javatype)(SZ:nat)(jsz:(jsize T SZ))(n:nat) (invariant s) -> [s2 := (allocate_jarray T SZ jsz n s)] (invariant s2). Proof. Intros. Unfold_invar H. Unfold_invar_Goal; Intros. Assert (new_jarray_ptr s T SZ jsz n E RW T0); [ EApply allocate_jarray_effects_ptr; EAuto | Idtac]. LetTac s' := (allocate (plus (mult n SZ) (8)) (machine_state_of s)). LetTac m := (updn (4) (updn (4) (mem_of s') (rega_of s') (loc_of_virtab _4java4lang6Object_C)) (plus (rega_of s') (4)) n). Replace (mem_of' s2) with m; Try Reflexivity. Unfold m. EApply addr_updn. EApply addr_updn. Unfold s'; EApply allocate_jarray_upd_addr. Unfold s'; EApply allocate_jarray_upd_upd_addr. EApply addr_updn. Unfold s'; EApply allocate_jarray_upd_addr. Unfold new_jarray_ptr in H7; Decompose [and or ex] H7; Clear H7. Unfold s'; EApply allocate_preserves; EAuto. Rewrite H9. Rewrite H11 in H4; Rewrite (jsize_unique ? ? ? H4 (szvirtab _4java4lang6Object_C)). Unfold s'; EApply allocate_works_extend. Clear m s'; LetTac dumb := (mult n SZ); Omega. Replace E with (plus (0) E); Try Reflexivity. Rewrite H8. EApply addr_closed. Unfold s'; EApply allocate_preserves. EAuto. Rewrite H11 in H4; Rewrite (jsize_unique ? ? ? H4 szcdesc). Simpl; EAuto with java1. Rewrite H10. Rewrite plus_sym. EApply addr_closed. Unfold s'; EApply allocate_preserves. EAuto. Rewrite H12 in H4; Rewrite (jsize_unique ? ? ? H4 (szjimplof x0)). EAuto with java1. Rewrite H8. Rewrite plus_sym. EApply addr_closed. Unfold s'; EApply allocate_works. Rewrite H11 in H4; Rewrite (jsize_unique ? ? ? H4 szint). Clear m s'; LetTac dumb := (mult n SZ); Omega. Rewrite H12. Rewrite plus_sym. EApply addr_closed. Unfold s'; EApply allocate_works. Rewrite H8 in H4; Rewrite (jsize_unique ? ? ? H4 jsz). Rewrite_4or8 SZ; Omega. (* part 2 *) Assert (new_jarray_ptr s T SZ jsz n e1 rw T1); [ EApply allocate_jarray_effects_ptr; EAuto | Idtac]. Assert (new_jarray_ptr s T SZ jsz n e2 RW T2); [ EApply allocate_jarray_effects_ptr; EAuto | Idtac]. EApply new_jarray_ptr_equal_or_apart with T:=T SZ:=SZ; EAuto. (* part 3 *) LetTac s' := (allocate (plus (mult n SZ) (8)) (machine_state_of s)). LetTac m := (updn (4) (updn (4) (mem_of s') (rega_of s') (loc_of_virtab _4java4lang6Object_C)) (plus (rega_of s') (4)) n). Replace (mem_of' s2) with m; Try Reflexivity. Unfold m. EApply addr_updn. EApply addr_updn. Unfold s'; EApply allocate_jarray_upd_addr. Unfold s'; EApply allocate_jarray_upd_upd_addr. EApply addr_updn. Unfold s'; EApply allocate_jarray_upd_addr. Unfold s'. EApply allocate_preserves. EAuto. (* part 4 *) Assert (new_jarray_ptr s T SZ jsz n e rw T0); [ EApply allocate_jarray_effects_ptr; EAuto | Idtac]. Unfold new_jarray_ptr in H7; Decompose [and or ex] H7; Clear H7; Try Discriminate_something. EAuto. Rewrite H12. EApply apart_sym. EApply apart_shift_right. EApply allocate_addr_apart. LetTac dumb:=(mult n SZ); Omega. Generalize (virtab_size_four C); Omega. EAuto. Rewrite H8 in H6; Rewrite (jsize_unique ? ? ? H6 jsz). Rewrite_4or8 SZ; Omega. Rewrite_4or8 SZ0; Omega. (* part 5 *) Replace (mem_of' s2) with (last_alloc_of s2); Try Reflexivity. EAuto with axioms. Qed. End allocinv.