(* * Seplog is an implementation of separation logic (an extension of Hoare * logic by John C. Reynolds, Peter W. O'Hearn, and colleagues) in the * Coq proof assistant (version 8, http://coq.inria.fr) together with a * sample verification of the heap manager of the Topsy operating system * (version 2, http://www.topsy.net). More information is available at * http://web.yl.is.s.u-tokyo.ac.jp/~affeldt/seplog. * * Copyright (c) 2005 Reynald Affeldt and Nicolas Marti * * This program is free software; you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by * the Free Software Foundation; either version 2 of the License, or * (at your option) any later version. * * This program is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU General Public License for more details. * * You should have received a copy of the GNU General Public License * along with this program; if not, write to the Free Software * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA *) Load seplog_header. Require Import topsy_hm. Open Local Scope vc_scope. Open Local Scope Z_scope. (* Allocation *) Definition findFree (size: nat) (entry fnd sz stts:var.v) := entry <- (var_e hmStart); stts <-* (entry -.> status); fnd <- (int_e 0); (while' ((var_e entry =/= null) &&& (var_e fnd =/= (int_e 1))) (TT) ( stts <-* (entry -.> status); (ENTRYSIZE entry sz); (ifte ((var_e stts == Free) &&& (var_e sz >>= nat_e size)) thendo fnd <- (int_e 1) elsedo (entry <-* (entry -.> next))) )). Definition LEFTOVER : nat := 8%nat. Definition compact (cptr :var.v) (nptr: var.v) (stts : var.v) := while' (var_e cptr =/= null) (TT) ( stts <-* (cptr -.> status); (*current status*) ifte (var_e stts == Free) thendo ( (* la on sait qu'on est sur un bloc Free (donc pas le dernier) *) nptr <-* (cptr -.> next); (*address of next block*) (while' ((var_e nptr =/= null)) (TT) ( (* la on sait que le prochain bloc n'est a l'adresse nil = on est pas sur le bloc de fin (on le savait deja par le ifte) *) (stts <-* (nptr -.> status)); (ifte (var_e stts == Free) thendo ( stts <-* (nptr -.> next); (cptr -.> next) *<- (var_e stts); nptr <- (var_e stts) ) elsedo (nptr <- null)) ) ) ) elsedo (skip'); cptr <-* (cptr -.> next) (* move to next block *) ). (* entry contains the address of a free entry, size is the size we want to allocated *) Definition split (entry:var.v) (size:nat) (cptr sz:var.v) := ENTRYSIZE entry sz; ifte ((var_e sz) >>= ((nat_e size) +e (nat_e LEFTOVER) +e (nat_e 2%nat))) thendo ( cptr <- (var_e entry) +e (nat_e 2%nat) +e (nat_e size); sz <-* (entry -.> next); (cptr -.> next) *<- (var_e sz); (cptr -.> status) *<- Free; (entry -.> next) *<- (var_e cptr) ) elsedo ( skip' ); (entry -.> status) *<- Allocated. Definition HM_ALLOCFAILED := (int_e 0%Z). Definition HM_ALLOCOK := (int_e 1%Z). Definition hmAlloc (result:var.v) (size: nat) (entry:var.v) (*(adr: loc)*) (cptr fnd stts nptr sz:var.v) := (* entry <- (nat_e adr); cette instruction ne sert a rien*) result <- null; (findFree size entry fnd sz stts); (ifte ((var_e entry) == null) thendo ( (* tmp <- (var_e adr);*) cptr <- (var_e hmStart); (compact cptr nptr stts); (findFree size entry fnd sz stts) ) elsedo ( skip' )); (ifte ((var_e entry) == null) thendo ( result <- HM_ALLOCFAILED ) elsedo ( (split entry size cptr sz); result <- (var_e entry) +e (nat_e 2%nat) )). Close Local Scope vc_scope. Close Local Scope Z_scope. (* hmAlloc Specification *) Definition hmAlloc_specif := forall result adr sizex x size entry cptr fnd stts nptr sz lx, length lx = sizex -> (var.set (hmStart::result::entry::cptr::fnd::stts::nptr::sz::nil)) -> adr > 0 -> sizex > 0 -> size > 0 -> {{fun s => fun h => exists l1, Heap_List l1 adr 0 s h /\ In (x,sizex,Allocated) l1 /\ (ArrayI (x + 2) lx ** TT) s h /\ eval (var_e hmStart) s = eval (nat_e adr) s }} proj_cmd (hmAlloc result size entry cptr fnd stts nptr sz) {{ fun s => fun h => (exists l2, exists y, y > 0 /\ eval (var_e result) s = Z_of_nat (y+2) /\ (exists size'', size'' >= size /\ Heap_List l2 adr 0 s h /\ In (x,sizex,Allocated) l2 /\ (ArrayI (x + 2) lx ** TT) s h /\ In (y,size'',Allocated) l2 /\ x <> y)) \/ (exists l2, eval (var_e result) s = 0%Z /\ Heap_List l2 adr 0 s h /\ In (x,sizex,Allocated) l2) }}. Definition findFree_specif := forall adr entry fnd sz stts size sizex x result lx, length lx = sizex -> size > 0 -> sizex > 0 -> adr > 0 -> var.set (hmStart::entry::fnd::sz::stts::result::nil) -> {{fun s => fun h =>exists l1, Heap_List l1 adr 0 s h /\ In (x,sizex,Allocated) l1 /\ (ArrayI (x + 2) lx ** TT) s h /\ eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s }} proj_cmd (findFree size entry fnd sz stts) {{fun s => fun h => exists l1, Heap_List l1 adr 0 s h /\ In (x,sizex,Allocated) l1 /\ (ArrayI (x + 2) lx ** TT) s h /\ eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ ( (exists finded_free_block, exists size'', size'' >= size /\ In (finded_free_block,size'',Free) l1 /\ eval (var_e entry) s = (Z_of_nat finded_free_block) /\ finded_free_block > 0) \/ (eval (var_e entry) s = eval null s) )}}. Lemma findFree_verif : findFree_specif. unfold findFree_specif. do 10 intro. intro NEW. intros. unfold findFree. simpl. apply semax_assign_var_e'' with (fun s => fun h =>exists l1, Heap_List l1 adr 0 s h /\ In (x,sizex,Allocated) l1 /\ (ArrayI (x + 2) lx ** TT) s h /\ eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e entry) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s ). Resolve_assign_var. inversion_clear H3 as [l]. decompose [and] H4; clear H4. exists l. split. Resolve_simpl1. split; auto. split. eapply sep.con_inde_store. apply H5. intros. eapply ArrayI_inde_store. apply H4. trivial. split. Resolve_simpl1. split. Resolve_simpl1. Resolve_simpl1. apply semax_assign_var_lookup_backwards'' with (fun s => fun h =>exists l1, Heap_List l1 adr 0 s h /\ In (x,sizex,Allocated) l1 /\ (ArrayI (x + 2) lx ** TT) s h /\ eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e entry) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ (exists status, (status = Allocated \/ status = Free) /\ eval (var_e stts) s = eval status s /\ exists size, In (adr,size,status) l1) ). red. simpl. intros. inversion_clear H3 as [l]. decompose [and] H4; clear H4. inversion H3. subst l. simpl in H6. contradiction. inversion H4. subst next hd_adr startl endl s0 h0. exists hd_expr. eapply Heap_List_var_lookup_status. apply H3. rewrite <- H17. simpl. left. intuition. auto. red. exists l. split. rewrite <- H17. eapply Heap_List_inde_store with s. eapply Heap_List_suiv with (h1 := h1) (h2 := h2). Disjoint_heap. Equal_heap. auto. intuition. auto. auto. auto. auto. split; auto. split. eapply sep.con_inde_store. apply H5. intros. eapply ArrayI_inde_store. apply H12. trivial. split. Resolve_simpl1. split. Resolve_simpl1. split. Resolve_simpl1. exists hd_expr. split. auto. split. Resolve_simpl1. inversion_clear H11. subst hd_expr. trivial. subst hd_expr. trivial. exists hd_size. subst l. auto with *. intros. inversion_clear H13 as [l1]. decompose [and] H18; clear H18. exists l1. split. eapply Heap_List_heap_equal. apply heap.equal_sym. apply H12. auto. split; auto. split. eapply sep.con_inde_store. eapply ArrayITT_heap_cong. apply H12. apply H19. intros. eapply ArrayI_inde_store. apply H18. trivial. auto. apply semax_assign_var_e'' with (fun s => fun h => exists l1, Heap_List l1 adr 0 s h /\ In (x,sizex,Allocated) l1 /\ (ArrayI (x+2) lx ** TT) s h /\ eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e entry) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ eval (var_e fnd) s = eval (nat_e 0) s /\ (exists status, (status = Allocated \/ status = Free) /\ eval (var_e stts) s = eval status s /\ exists size', In (adr,size',status) l1) ). red. simpl. intros . inversion_clear H3 as [l]. decompose [and] H4; clear H4. inversion_clear H11. decompose [and] H4; clear H4. inversion_clear H13. red. exists l. split. eapply Heap_List_inde_store. apply H3. split; auto. split. Resolve_simpl1. split. Resolve_simpl1. split. Resolve_simpl1. split. Resolve_simpl1. split. Resolve_simpl1. exists x0. split; auto. split. inversion_clear H10. subst x0. Resolve_simpl1. subst x0. Resolve_simpl1. exists x1. auto. apply semax_while' with (fun s => fun h =>exists l1, Heap_List l1 adr 0 s h /\ In (x,sizex,Allocated) l1 /\ (ArrayI (x+2) lx ** TT) s h /\ eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ ( (* soit le bloc est trouve *) (eval (var_e fnd) s = eval (nat_e 1) s /\ exists bloc_adr, eval (var_e entry) s = eval (nat_e bloc_adr) s /\ bloc_adr > 0 /\ (* eval (var_e tmp2) s = eval Free s /\ *) exists size', In (bloc_adr,size',Free) l1 /\ size' >= size ) \/ (* soit on ne l'a pas trouve et on continu de chercher *) (eval (var_e fnd) s = eval (nat_e 0) s /\ exists bloc_adr, eval (var_e entry) s = eval (nat_e bloc_adr) s /\ bloc_adr > 0 /\ exists status, (status = Allocated \/ status = Free) /\ (* eval (var_e tmp2) s = eval status s /\ *) exists size', In (bloc_adr,size',status) l1) \/ (* soit on a fini la recherche sans trouver *) (eval (var_e entry) s = eval null s) \/ (* soit on en est arrive au dernier tail-bloc ... et la ca sent la fin *) (eval (var_e fnd) s = eval (nat_e 0) s /\ exists bloc_adr, eval (var_e entry) s = eval (nat_e bloc_adr) s /\ bloc_adr > 0 /\ (Heap_List l1 adr bloc_adr ** Heap_List nil bloc_adr 0) s h ) ) ). (* on ressere a gauche du while *) red. intuition. inversion_clear H3 as [l]. exists l. decompose [and] H4; clear H4. split; auto. split; auto. split; auto. split; auto. split; auto. right. left. split; auto. exists adr. split; auto. split; auto. inversion_clear H12. exists x0. intuition. apply semax_strengthen_pre with (fun s => fun h => exists l1, Heap_List l1 adr 0 s h /\ In (x,sizex,Allocated) l1 /\ (ArrayI (x+2) lx ** TT) s h /\ eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ ( (eval (var_e fnd) s = eval (nat_e 0) s /\ exists bloc_adr, eval (var_e entry) s = eval (nat_e bloc_adr) s /\ bloc_adr > 0 /\ exists status, (status = Allocated \/ status = Free) /\ (*eval (var_e tmp2) s = eval status s /\*) exists size', In (bloc_adr,size',status) l1) \/ (eval (var_e fnd) s = eval (nat_e 0) s /\ exists bloc_adr, eval (var_e entry) s = eval (nat_e bloc_adr) s /\ bloc_adr > 0 /\ (Heap_List l1 adr bloc_adr ** Heap_List nil bloc_adr 0) s h ) ) ). red. simpl. intros. decompose [and] H3; clear H3. inversion_clear H4 as [l]. generalize (andb_prop _ _ H5); intro X; inversion_clear X. generalize (negb_true_is_false _ H4). generalize (negb_true_is_false _ H6). clear H4 H6; intros. unfold eqb in H4; unfold eqb in H6. generalize (Zeq_bool_false (eval (var_e entry) s) (eval null s)); intro X; inversion_clear X. generalize (H7 H6); intros; clear H7 H8 H6. generalize (Zeq_bool_false (eval (var_e fnd) s) (eval (int_e 1%Z) s)); intro X; inversion_clear X. generalize (H6 H4); intros; clear H7 H4 H6. exists l. decompose [and] H3; clear H3. inversion_clear H13. intuition. inversion_clear H3. intuition. inversion_clear H12. intuition. intuition. (* on est dans le while *) apply semax_assign_var_lookup_backwards'' with (fun s => fun h =>exists l1, Heap_List l1 adr 0 s h /\ In (x,sizex,Allocated) l1 /\ (ArrayI (x+2) lx ** TT) s h /\ eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ ( (eval (var_e fnd) s = eval (nat_e 0) s /\ exists bloc_adr, eval (var_e entry) s = eval (nat_e bloc_adr) s /\ bloc_adr > 0 /\ exists status, (status = Allocated \/ status = Free) /\ eval (var_e stts) s = eval status s /\ exists size', In (bloc_adr,size',status) l1) \/ (eval (var_e fnd) s = eval (nat_e 0) s /\ exists bloc_adr, eval (var_e entry) s = eval (nat_e bloc_adr) s /\ bloc_adr > 0 /\ (Heap_List l1 adr bloc_adr ** Heap_List nil bloc_adr 0) s h /\ eval (var_e stts) s = eval Allocated s) ) ). red. simpl. intros. inversion_clear H3 as [l]. decompose [and] H4; clear H4. inversion_clear H10. inversion_clear H4. inversion_clear H10. decompose [and] H4; clear H4. inversion_clear H13. decompose [and] H4; clear H4. inversion_clear H13. exists x1. eapply Heap_List_var_lookup_status. apply H3. apply H4. auto. red. exists l. split. apply Heap_List_inde_store with s. auto. split; auto. split. Resolve_simpl1. split. Resolve_simpl1. split. Resolve_simpl1. left. split. Resolve_simpl1. exists x0. split. Resolve_simpl1. split; auto. exists x1. split; auto. split. Resolve_simpl1. inversion_clear H11. subst x1. auto. subst x1. auto. exists x2. auto. intros. inversion_clear H14 as [l1]. decompose [and] H15; clear H15. exists l1. split. eapply Heap_List_heap_equal. apply heap.equal_sym. apply H13. auto. split; auto. split; auto. eapply ArrayITT_heap_cong. apply H13. auto. split; auto. split; auto. inversion_clear H21. decompose [and] H15; clear H15. left. auto. inversion_clear H15. inversion_clear H21. decompose [and] H15; clear H15. right. split; auto. exists x3. split; auto. split; auto. split. Decompose_sepcon H22 h01 h02. exists h01; exists h02. split. Disjoint_heap. split. eapply heap.equal_trans with h0. Equal_heap. Equal_heap. auto. auto. inversion_clear H4. inversion_clear H10. decompose [and] H4; clear H4. Decompose_sepcon H13 h1 h2. inversion_clear H15. clear H14. simpl in H18. Decompose_sepcon H18 h21 h22. Decompose_sepcon H20 h221 h222. red in H23. exists Allocated. Compose_sepcon h21 (heap.union h221 h1). eapply mapsto_equiv. apply H15. simpl. unfold status. rewrite H10. intuition. intuition. Intro_sepimp h'21 h'. red. exists l. split. apply Heap_List_inde_store with s. assert (heap.equal h h'). assert (heap.equal h'21 h21). eapply singleton_equal. apply H24. apply H15. simpl. unfold status. rewrite H10. intuition. intuition. Equal_heap. eapply Heap_List_heap_equal. apply heap.equal_sym; apply H26. auto. split; auto. split. assert (heap.equal h h'). assert (heap.equal h'21 h21). eapply singleton_equal. apply H24. apply H15. simpl. unfold status. rewrite H10. intuition. intuition. Equal_heap. eapply ArrayITT_heap_cong. apply H26. Resolve_simpl1. split. Resolve_simpl1. split. Resolve_simpl1. right. split. Resolve_simpl1. exists x0. split. Resolve_simpl1. split; auto. split. assert (heap.equal h'21 h21). eapply singleton_equal. apply H24. apply H15. simpl. unfold status. rewrite H10. intuition. intuition. Compose_sepcon h1 (heap.union h21 h221). apply Heap_List_inde_store with s. auto. apply Heap_List_inde_store with s. eapply Heap_List_last. auto. apply H16. auto. simpl. Compose_sepcon h21 h221. auto. Compose_sepcon h221 heap.emp. auto. red; apply heap.equal_refl. Resolve_simpl1. inversion H14. apply semax_seq with (fun s => fun h =>exists l1, Heap_List l1 adr 0 s h /\ In (x,sizex,Allocated) l1 /\ (ArrayI (x+2) lx ** TT) s h /\ eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ ( (eval (var_e fnd) s = eval (nat_e 0) s /\ exists bloc_adr, eval (var_e entry) s = eval (nat_e bloc_adr) s /\ bloc_adr > 0 /\ exists status, (status = Allocated \/ status = Free) /\ eval (var_e stts) s = eval status s /\ exists size', In (bloc_adr,size',status) l1 /\ eval (var_e sz) s = Z_of_nat size') \/ (eval (var_e fnd) s = eval (nat_e 0) s /\ exists bloc_adr, eval (var_e entry) s = eval (nat_e bloc_adr) s /\ bloc_adr > 0 /\ (Heap_List l1 adr bloc_adr ** Heap_List nil bloc_adr 0) s h /\ eval (var_e stts) s = eval Allocated s /\ eval (var_e sz) s = 0%Z) ) ). apply semax_assign_var_lookup_backwards'' with (fun s => fun h =>exists l1, Heap_List l1 adr 0 s h /\ In (x,sizex,Allocated) l1 /\ (ArrayI (x+2) lx ** TT) s h /\ eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ ( (eval (var_e fnd) s = eval (nat_e 0) s /\ exists bloc_adr, eval (var_e entry) s = eval (nat_e bloc_adr) s /\ bloc_adr > 0 /\ exists status, (status = Allocated \/ status = Free) /\ eval (var_e stts) s = eval status s /\ exists size', In (bloc_adr,size',status) l1 /\ eval (var_e sz) s = Z_of_nat (bloc_adr + 2 + size')) \/ (eval (var_e fnd) s = eval (nat_e 0) s /\ exists bloc_adr, eval (var_e entry) s = eval (nat_e bloc_adr) s /\ bloc_adr > 0 /\ (Heap_List l1 adr bloc_adr ** Heap_List nil bloc_adr 0) s h /\ eval (var_e stts) s = eval Allocated s /\ eval (var_e sz) s = 0%Z) ) ). red. simpl. intros. inversion_clear H3 as [l]. decompose [and] H4; clear H4. inversion_clear H10. inversion_clear H4. inversion_clear H10. decompose [and] H4; clear H4. inversion_clear H13. decompose [and] H4; clear H4. inversion_clear H15. exists (nat_e (x0 + 2 + x2)). eapply Heap_List_var_lookup_next. apply H3. apply H4. intuition. red. exists l. split. apply Heap_List_inde_store with s; auto. split; auto. split. Resolve_simpl1. split. Resolve_simpl1. split. Resolve_simpl1. left. split. Resolve_simpl1. exists x0. split. Resolve_simpl1. split; auto. exists x1. split; auto. split. inversion_clear H11. subst x1. Resolve_simpl1. subst x1. Resolve_simpl1. exists x2. split; auto. Resolve_simpl1. intros. inversion_clear H15. decompose [and] H16; clear H16. exists x3. split. eapply Heap_List_heap_equal. apply heap.equal_sym. apply H13. auto. split; auto. split; auto. eapply ArrayITT_heap_cong. apply H13. auto. split; auto. split; auto. inversion_clear H22. left; auto. inversion_clear H16. inversion_clear H22. decompose [and] H16; clear H16. right. split; auto. exists x4. split; auto. split; auto. split. Decompose_sepcon H23 h01 h02. exists h01; exists h02. split. Disjoint_heap. split. apply heap.equal_trans with h0. Equal_heap. Equal_heap. auto. auto. decompose [and] H4; clear H4. inversion_clear H10. decompose [and] H4; clear H4. Decompose_sepcon H11 h1 h2. inversion_clear H16. clear H15; subst next. simpl in H19. Decompose_sepcon H19 h21 h22. Decompose_sepcon H20 h221 h222. red in H23. exists (nat_e 0). Compose_sepcon h221 (heap.union h21 h1). eapply mapsto_equiv. apply H20. simpl. unfold next. rewrite H10. intuition. intuition. Intro_sepimp h'221 h'. red. exists l. split. apply Heap_List_inde_store with s. assert (heap.equal h h'). assert (heap.equal h'221 h221). eapply singleton_equal. apply H24. apply H20. simpl. unfold status. rewrite H10. intuition. intuition. Equal_heap. eapply Heap_List_heap_equal. apply heap.equal_sym; apply H26. auto. split; auto. split. assert (heap.equal h h'). assert (heap.equal h'221 h221). eapply singleton_equal. apply H24. apply H20. simpl. unfold status. rewrite H10. intuition. intuition. Equal_heap. eapply ArrayITT_heap_cong. apply H26. Resolve_simpl1. split. Resolve_simpl1. split. Resolve_simpl1. right. split. Resolve_simpl1. exists x0. split. Resolve_simpl1. split; auto. split. assert (heap.equal h'221 h221). eapply singleton_equal. apply H24. apply H20. simpl. unfold status. rewrite H10. intuition. intuition. Compose_sepcon h1 (heap.union h21 h221). apply Heap_List_inde_store with s. auto. apply Heap_List_inde_store with s. eapply Heap_List_last. auto. intuition. auto. simpl. Compose_sepcon h21 h221. auto. Compose_sepcon h221 heap.emp. auto. red; apply heap.equal_refl. split. Resolve_simpl1. Resolve_simpl1. inversion H15. apply semax_assign_var_e'' with (fun s => fun h =>exists l1, Heap_List l1 adr 0 s h /\ In (x,sizex,Allocated) l1 /\ (ArrayI (x+2) lx ** TT) s h /\ eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ ( (eval (var_e fnd) s = eval (nat_e 0) s /\ exists bloc_adr, eval (var_e entry) s = eval (nat_e bloc_adr) s /\ bloc_adr > 0 /\ exists status, (status = Allocated \/ status = Free) /\ eval (var_e stts) s = eval status s /\ exists size', In (bloc_adr,size',status) l1 /\ eval (var_e sz) s = Z_of_nat size') \/ (eval (var_e fnd) s = eval (nat_e 0) s /\ exists bloc_adr, eval (var_e entry) s = eval (nat_e bloc_adr) s /\ bloc_adr > 0 /\ (Heap_List l1 adr bloc_adr ** Heap_List nil bloc_adr 0) s h /\ eval (var_e stts) s = eval Allocated s /\ eval (var_e sz) s = (0 - 2 - (Z_of_nat (bloc_adr)))%Z) ) ). red. intros. simpl in H3. inversion_clear H3 as [l]. decompose [and] H4; clear H4. red. exists l. split. eapply Heap_List_inde_store. apply H3. split; auto. split. Resolve_simpl1. split. simpl. Resolve_simpl1. split. simpl. Resolve_simpl1. inversion_clear H10. inversion_clear H4. inversion_clear H10. decompose [and] H4; clear H4. inversion_clear H13. decompose [and] H4; clear H4. inversion_clear H15. decompose [and] H4; clear H4. left. split. simpl. Resolve_simpl1. exists x0. split. simpl. Resolve_simpl1. split; auto. exists x1. split; auto. split. simpl. inversion_clear H11. subst x1. Resolve_simpl1. subst x1. Resolve_simpl1. exists x2. split; auto. simpl. Resolve_simpl1. rewrite H15; rewrite H10. assert (2 = Z_of_nat 2)%Z. intuition. rewrite H4; clear H4. rewrite <- inj_minus1. rewrite <- inj_minus1. intuition. intuition. intuition. inversion_clear H4. inversion_clear H10. decompose [and] H4; clear H4. right. split. simpl. Resolve_simpl1. exists x0. split. simpl. Resolve_simpl1. split; auto. split. Resolve_simpl1. split. simpl. Resolve_simpl1. assert (exists d, eval (var_e sz) (store.update sz (eval ((var_e sz -e var_e entry) -e int_e 2%Z) s) s) = d). exists (eval (var_e sz) (store.update sz (eval ((var_e sz -e var_e entry) -e int_e 2%Z) s) s)). auto. inversion_clear H4. rewrite H14. simpl in H14. rewrite H15 in H14; rewrite H10 in H14. rewrite <- H14. Resolve_simpl1. assert ( - Z_of_nat x0 - 2 = - 2 - Z_of_nat x0)%Z. intuition. assert (forall x1 x2, x1 = x2 -> 0 - x1 = 0 - x2)%Z. intuition. generalize (H16 _ _ H4). intuition. apply semax_ifte. apply semax_assign_var_e'. red. intros. simpl. inversion_clear H3. simpl in H5. generalize (Zgt_cases 0 (store.lookup sz s)); intro. rewrite H5 in H3. clear H5. inversion_clear H4 as [l]. decompose [and] H5; clear H5. simpl in H9; simpl in H8. red. exists l. split. Resolve_simpl1. split. auto. split. Resolve_simpl1. split. Resolve_simpl1. split. Resolve_simpl1. inversion_clear H11. inversion_clear H5. inversion_clear H11. decompose [and] H5; clear H5. inversion_clear H14. decompose [and] H5; clear H5. inversion_clear H16. decompose [and] H5; clear H5. simpl in H16. rewrite H16 in H3. assert (forall x, (0 > Z_of_nat x)%Z -> 0 > x). intuition. generalize (H5 _ H3); intro. inversion H17. inversion_clear H5. inversion_clear H11. decompose [and] H5; clear H5. right. simpl in H11; simpl in H14; simpl in H10. split. Resolve_simpl1. exists x0. split. Resolve_simpl1. split; auto. split. Resolve_simpl1. split. Resolve_simpl1. Resolve_simpl1. apply semax_skip'. red. intros. inversion_clear H3. simpl in H5. generalize (Zgt_cases 0 (store.lookup sz s)); intros. rewrite H5 in H3; clear H5. inversion_clear H4 as [l]. decompose [and] H5; clear H5. simpl in H9; simpl in H8. inversion_clear H11. simpl in H5. decompose [and] H5; clear H5. inversion_clear H11. decompose [and] H5; clear H5. inversion_clear H14. decompose [and] H5; clear H5. inversion_clear H16. decompose [and] H5; clear H5. exists l. split; auto. split; auto. split; auto. split; auto. split; auto. left. split; auto. exists x0. split; auto. split; auto. exists x1. split; auto. split; auto. exists x2. split; auto. inversion_clear H5. inversion_clear H11. decompose [and] H5; clear H5. assert (eval (var_e sz) s = store.lookup sz s). intuition. rewrite H5 in H16; clear H5. rewrite H16 in H3. assert ( 0 - 2 - Z_of_nat x0 = 0 - (2 + Z_of_nat x0))%Z. intuition. rewrite H5 in H3. assert (2 + Z_of_nat x0 > 0)%Z. intuition. assert (forall x, x > 0 -> 0 > 0 - x)%Z. intuition. generalize (H17 (2 + Z_of_nat x0)%Z H15); intro. assert (forall x, ~(0 > x /\ 0 <= x)%Z). intuition. red in H19. assert ((0 > 0 - (2 + Z_of_nat x0))%Z /\ (0 <= 0 - (2 + Z_of_nat x0))%Z). intuition. generalize (H19 (0 - (2 + Z_of_nat x0))%Z H20). intuition. apply semax_ifte. apply semax_assign_var_e'. red. simpl. intros. inversion_clear H3. generalize (andb_prop _ _ H5); intros; clear H5. inversion_clear H3. unfold eqb in H5. generalize (Zeq_bool_true _ _ H5); intro; clear H5. red. inversion_clear H4 as [l]. decompose [and] H5; clear H5. exists l. split. Resolve_simpl1. split; auto. split. Resolve_simpl1. split. Resolve_simpl1. split. Resolve_simpl1. inversion_clear H12. decompose [and] H5; clear H5. inversion_clear H12. decompose [and] H5; clear H5. inversion_clear H15. decompose [and] H5; clear H5. inversion_clear H17. decompose [and] H5; clear H5. left. split. Resolve_simpl1. exists x0. split. Resolve_simpl1. split; auto. exists x2. split. inversion_clear H13. subst x1. rewrite H16 in H3. simpl in H3. inversion H3. subst x1. auto. generalize (Zge_cases (store.lookup sz s) (Z_of_nat size)); intro. rewrite H6 in H5. rewrite H17 in H5. intuition. inversion_clear H5. inversion_clear H12. decompose [and] H5; clear H5. generalize (Zge_cases (store.lookup sz s) (Z_of_nat size)); intro. rewrite H6 in H5. rewrite H17 in H5. assert (0 < Z_of_nat size)%Z. intuition. assert (forall x, ~(0 < x /\ 0 >= x)%Z). intuition. red in H18. generalize (H18 (Z_of_nat size)%Z); intro. intuition. apply semax_assign_var_lookup_backwards'. red. simpl. intros. inversion_clear H3. inversion_clear H4 as [l]. decompose [and] H3; clear H3. inversion_clear H11. inversion_clear H3. inversion_clear H11. decompose [and] H3; clear H3. inversion_clear H14. decompose [and] H3; clear H3. inversion_clear H16. decompose [and] H3; clear H3. exists (nat_e (x0 + 2 + x2)). eapply Heap_List_var_lookup_next. apply H4. apply H14. simpl; auto. red. exists l. split. Resolve_simpl1. split; auto. split. Resolve_simpl1. split. Resolve_simpl1. split. Resolve_simpl1. generalize (list_split' l x0 x2 x1 H14); intro. inversion_clear H3 as [l1]. inversion_clear H17 as [l2]. generalize H4; intro. rewrite H3 in H17. generalize (Heap_List_split' l1 (((x0, x2, x1) :: nil) ++ l2) adr s h H1); intro X; inversion_clear X. generalize (H18 H17); clear H19 H17 H18; intro. inversion_clear H17. Decompose_sepcon H18 h1 h2. assert (x3 > 0). eapply Heap_List_start_pos. apply H21. inversion_clear H21. subst x3. subst next. induction l2. right. right. right. split. Resolve_simpl1. exists (x0 + 2 + x2). split. simpl. Resolve_simpl1. split. omega. eapply sep.con_inde_store with s. Compose_sepcon' (heap.union h1 h3) h4. rewrite H3. simpl. assert (x0 + 2 + x2 > 0). omega. generalize (Heap_List_split l1 ((x0, x2, x1) :: nil) adr (x0 + 2 + x2) s (heap.union h1 h3) H1 H21); intro X; inversion_clear X. apply H26 ; clear H26 H25. exists x0. Compose_sepcon h1 h3. auto. eapply Heap_List_suiv with (h1:= h3) (h2 := heap.emp). Disjoint_heap. Equal_heap. auto. intuition. auto. auto. auto. eapply Heap_List_trans. auto. auto. red; apply heap.equal_refl. auto. intros. Resolve_simpl1. intros. Resolve_simpl1. clear IHl2. induction a. induction a. right. left. split. Resolve_simpl1. exists (x0 + 2 + x2). split. Resolve_simpl1. split. omega. exists b. inversion_clear H29. split; auto. exists b0. subst a. rewrite H3. intuition. intros. inversion_clear H17. decompose [and] H18; clear H18. exists x3. split. eapply Heap_List_heap_equal. apply heap.equal_sym. apply H3. auto. split; auto. split. eapply ArrayITT_heap_cong. apply H3. auto. split; auto. split; auto. inversion_clear H24. left; auto. inversion_clear H18. inversion_clear H23. right. left. split; auto. inversion_clear H23. right; right; left. auto. inversion_clear H18. inversion_clear H24. inversion_clear H18. inversion_clear H25. right; right; right. split; auto. exists x4. split; auto. split; auto. Decompose_sepcon H26 h01 h02. exists h01; exists h02. split. Disjoint_heap. split. apply heap.equal_trans with h0. Equal_heap. Equal_heap. auto. inversion_clear H3. inversion_clear H11. decompose [and] H3; clear H3. Decompose_sepcon H12 h1 h2. inversion_clear H18. simpl in H21. Decompose_sepcon H21 h21 h22. Decompose_sepcon H24 h221 h222. red in H27. subst next. exists (nat_e 0). Compose_sepcon (h221) (heap.union h1 h21). eapply mapsto_equiv. apply H24. simpl. unfold next. rewrite H11. intuition. intuition. Intro_sepimp h'221 h'. assert (heap.equal h221 h'221). eapply singleton_equal. apply H24. apply H26. simpl; unfold next; rewrite H11; intuition. intuition. red. exists l. split. assert (heap.equal h h'). Equal_heap. eapply Heap_List_heap_equal. apply heap.equal_sym. apply H30. Resolve_simpl1. split; auto. split. assert (heap.equal h h'). Equal_heap. eapply ArrayITT_heap_cong. apply H30. Resolve_simpl1. split. Resolve_simpl1. split. Resolve_simpl1. right; right; left. Resolve_simpl1. inversion H17. red. simpl. intros. inversion_clear H3. inversion_clear H4 as [l]. exists l. split; intuition. inversion_clear H11. decompose [and] H9; clear H9. inversion_clear H14. inversion_clear H9. left. exists x0. exists x1. intuition. generalize (andb_false_elim _ _ H5); intro X; inversion_clear X. generalize (negb_false_is_true _ H10); intro. right. generalize (Zeq_bool_true _ _ H12). intuition. generalize (negb_false_is_true _ H10); intro. rewrite H9 in H12. generalize (Zeq_bool_true _ _ H12). intuition. generalize (andb_false_elim _ _ H5); intro X; inversion_clear X. generalize (negb_false_is_true _ H9); intro. right. generalize (Zeq_bool_true _ _ H12). intuition. generalize (negb_false_is_true _ H9); intro. unfold eqb in H12. rewrite H10 in H12. generalize (Zeq_bool_true _ _ H12). intuition. Qed. Definition compact_specif:= forall adr cptr nptr stts size sizex x result entry lx, length lx = sizex -> size > 0 -> sizex > 0 -> adr > 0 -> var.set (hmStart::entry::cptr::nptr::stts::result::nil) -> {{fun s => fun h =>exists l1, Heap_List l1 adr 0 s h /\ In (x,sizex,Allocated) l1 /\ eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ eval (var_e cptr) s = eval (nat_e adr) s /\ (ArrayI (x+2) lx ** TT) s h}} proj_cmd (compact cptr nptr stts) {{fun s => fun h => exists l1, Heap_List l1 adr 0 s h /\ In (x,sizex,Allocated) l1 /\ eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ (ArrayI (x+2) lx ** TT) s h}}. Lemma compact_verif : compact_specif. unfold compact_specif. do 10 intro. intro lx_length. intros. unfold compact. simpl. apply semax_while' with (fun s => fun h =>exists l, Heap_List l adr 0 s h /\ In (x,sizex,Allocated) l /\ (ArrayI (x+2) lx ** TT) s h /\ eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ (exists bloc_adr, eval (var_e cptr) s = Z_of_nat bloc_adr /\ ( (exists bloc_size, exists bloc_type, exists l1, exists l2, l = (l1 ++ ((bloc_adr, bloc_size, bloc_type)::nil) ++ l2)) \/ ((Heap_List l adr bloc_adr ** Heap_List nil bloc_adr 0) s h) \/ (bloc_adr = 0) ) ) ). red. simpl. intros. inversion_clear H3 as [l]. decompose [and] H4; clear H4. exists l. split; auto. split; auto. split; auto. split; auto. split; auto. inversion H3. subst l. simpl in H6; contradiction. inversion H4. subst startl endl s0 h0. subst next hd_adr. exists adr. split; auto. left. exists hd_size; exists hd_expr. exists (@nil (loc * nat * expr)); exists tl. simpl. auto. apply semax_strengthen_pre with (fun s => fun h =>exists l, Heap_List l adr 0 s h /\ In (x,sizex,Allocated) l /\ (ArrayI (x+2) lx ** TT) s h /\ eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ (exists bloc_adr, eval (var_e cptr) s = Z_of_nat bloc_adr /\ ( (exists bloc_size, exists bloc_type, exists l1, exists l2, l = (l1 ++ ((bloc_adr, bloc_size, bloc_type)::nil) ++ l2)) \/ ((Heap_List l adr bloc_adr ** Heap_List nil bloc_adr 0) s h) ) ) ). red. simpl; intros. inversion_clear H3. generalize (negb_true_is_false _ H5); clear H5; intro. unfold eqb in H3. generalize (Zeq_bool_false (store.lookup cptr s) 0); intro X; inversion_clear X. generalize (H5 H3); clear H3 H5 H6; intros. inversion_clear H4 as [l]. decompose [and] H5; clear H5. inversion_clear H11. inversion_clear H5. exists l. intuition. inversion_clear H5. inversion_clear H11. inversion_clear H5 as [l1]. inversion_clear H11 as [l2]. exists x0; split; auto. left. exists x1; exists x2. exists l1; exists l2; auto. exists x0; split; auto. subst x0. rewrite H10 in H3. tauto. apply semax_assign_var_lookup_backwards'' with (fun s => fun h =>exists l, Heap_List l adr 0 s h /\ In (x,sizex,Allocated) l /\ (ArrayI (x+2) lx ** TT) s h /\ eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ (exists bloc_adr, eval (var_e cptr) s = Z_of_nat bloc_adr /\ ( (exists bloc_size, exists bloc_type, exists l1, exists l2, l = (l1 ++ ((bloc_adr, bloc_size, bloc_type)::nil) ++ l2)/\ eval (var_e stts) s = eval bloc_type s) \/ ((Heap_List l adr bloc_adr ** Heap_List nil bloc_adr 0) s h /\ eval (var_e stts) s = eval Allocated s) ) ) ). red. simpl. intros. inversion_clear H3 as [l]. decompose [and] H4; clear H4. inversion_clear H10. inversion_clear H4. inversion_clear H10. inversion_clear H4. inversion_clear H10. inversion_clear H4 as [l1]. inversion_clear H10 as [l2]. exists x2. eapply Heap_List_var_lookup_status. apply H3. rewrite H4. apply in_or_app. right. simpl; left; intuition. auto. red. exists l. split. Resolve_simpl1. split; auto. split. Resolve_simpl1. split. Resolve_simpl1. split. Resolve_simpl1. exists x0. split. Resolve_simpl1. left. exists x1; exists x2; exists l1; exists l2. split. auto. Resolve_simpl1. rewrite H4 in H3. generalize (Heap_List_split' l1 ((x0, x1, x2) :: l2) adr s h H1); intro X; inversion_clear X. generalize (H10 H3); clear H3 H10 H11; intros. inversion_clear H3. Decompose_sepcon H10 h1 h2. inversion_clear H13. inversion_clear H15. subst x2. simpl. auto. subst x2. simpl. auto. intros. inversion_clear H11. decompose [and] H12; clear H12. inversion_clear H18. inversion_clear H12. exists x3. split. eapply Heap_List_heap_equal. apply heap.equal_sym. apply H10. auto. split; auto. split; auto. eapply ArrayITT_heap_cong. apply H10. auto. split; auto. split; auto. exists x4. split; auto. inversion_clear H18. auto. inversion_clear H12. right. split. Decompose_sepcon H18 h01 h02. exists h01; exists h02. split. Disjoint_heap. split. apply heap.equal_trans with h0. Equal_heap. Equal_heap. auto. auto. Decompose_sepcon H4 h1 h2. inversion_clear H13. clear H12. subst next. exists Allocated. simpl in H16. Decompose_sepcon H16 h21 h22. Decompose_sepcon H17 h221 h222. red in H20. Compose_sepcon h21 (heap.union h1 h221). eapply mapsto_equiv. apply H13. simpl. rewrite H9. auto with *. trivial. Intro_sepimp h'21 h'. red. exists l. split. eapply Heap_List_inde_store with s. assert (heap.equal h'21 h21). eapply singleton_equal. apply H21. apply H13. simpl. rewrite H9. auto with *. trivial. assert (heap.equal h' h). Equal_heap. eapply Heap_List_heap_equal. apply H24. auto. split; auto. split. assert (heap.equal h'21 h21). eapply singleton_equal. apply H21. apply H13. simpl. rewrite H9. auto with *. trivial. assert (heap.equal h' h). Equal_heap. eapply ArrayITT_heap_cong with h. apply heap.equal_sym. auto. Resolve_simpl1. split. Resolve_simpl1. split. Resolve_simpl1. exists x0. split. Resolve_simpl1. right. split. Compose_sepcon h1 (heap.union h'21 h221). eapply Heap_List_inde_store with s. auto. eapply Heap_List_inde_store with s. eapply (Heap_List_last). auto. intuition. auto. simpl. Compose_sepcon h'21 h221. eapply mapsto_equiv. apply H21. simpl. rewrite H9. auto with *. trivial. Compose_sepcon h221 heap.emp. auto. red; apply heap.equal_refl. Resolve_simpl1. inversion H12. apply semax_seq with (fun s => fun h =>exists l, Heap_List l adr 0 s h /\ In (x,sizex,Allocated) l /\ (ArrayI (x+2) lx ** TT) s h /\ eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ (exists bloc_adr, eval (var_e cptr) s = Z_of_nat bloc_adr /\ ( (exists bloc_size, exists bloc_type, exists l1, exists l2, l = (l1 ++ ((bloc_adr, bloc_size, bloc_type)::nil) ++ l2)) \/ ((Heap_List l adr bloc_adr ** Heap_List nil bloc_adr 0) s h ) ) ) ). apply semax_ifte. apply semax_strengthen_pre with (fun s => fun h =>exists l, Heap_List l adr 0 s h /\ In (x,sizex,Allocated) l /\ (ArrayI (x+2) lx ** TT) s h /\ eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ (exists bloc_adr, eval (var_e cptr) s = Z_of_nat bloc_adr /\ ( (exists bloc_size, exists l1, exists l2, l = (l1 ++ ((bloc_adr, bloc_size, Free)::nil) ++ l2)) ) ) ). red. simpl; intros. inversion_clear H3. unfold eqb in H5. generalize (Zeq_bool_true _ _ H5); clear H5; intros. inversion_clear H4 as [l]. decompose [and] H5; clear H5. inversion_clear H11. inversion_clear H5. inversion_clear H11. exists l. intuition. inversion_clear H5. inversion_clear H11. exists x0. split; auto. exists x1. inversion_clear H5 as [l1]. inversion_clear H11 as [l2]. exists l1; exists l2. inversion_clear H5. rewrite H11 in H4. generalize (Heap_List_split' l1 ((x0, x1, x2) :: l2) adr s h H1); intro X; inversion_clear X. generalize (H5 H4); clear H4 H5 H13; intros. inversion_clear H4. Decompose_sepcon H5 h1 h2. inversion_clear H15. subst x3 next. inversion_clear H17. subst x2. rewrite H12 in H3. simpl in H3. inversion H3. subst x2. auto. auto. inversion_clear H5. rewrite H12 in H3. inversion H3. apply semax_assign_var_lookup_backwards'' with (fun s => fun h =>exists l, Heap_List l adr 0 s h /\ In (x,sizex,Allocated) l /\ (ArrayI (x+2) lx ** TT) s h /\ eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ (exists bloc_adr, eval (var_e cptr) s = Z_of_nat bloc_adr /\ ( (exists bloc_size, exists l1, exists l2, l = (l1 ++ ((bloc_adr, bloc_size, Free)::nil) ++ l2) /\ eval (var_e nptr) s = eval (nat_e (bloc_adr + 2 + bloc_size)) s) ) ) ). red. simpl; intros. inversion_clear H3 as [l]. decompose [and] H4; clear H4. inversion_clear H10. inversion_clear H4. inversion_clear H10. inversion_clear H4 as [l1]. inversion_clear H10 as [l2]. exists (nat_e (x0 + 2 + x1)). eapply Heap_List_var_lookup_next. apply H3. rewrite H4. apply in_or_app. right. simpl; left; intuition. auto. red. exists l. split. Resolve_simpl1. split; auto. split. Resolve_simpl1. split. Resolve_simpl1. split. Resolve_simpl1. exists x0. split. Resolve_simpl1. exists x1. exists l1; exists l2. split; auto. Resolve_simpl1. intros. inversion_clear H11. inversion_clear H12. exists x2. split. eapply (Heap_List_heap_equal). apply heap.equal_sym. apply H10. auto. inversion_clear H13. inversion_clear H14. split; auto. split. eapply ArrayITT_heap_cong. apply H10. auto. auto. apply semax_while' with (fun s => fun h =>exists l, Heap_List l adr 0 s h /\ In (x,sizex,Allocated) l /\ (ArrayI (x+2) lx ** TT) s h /\ eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ (exists bloc_adr, eval (var_e cptr) s = Z_of_nat bloc_adr /\ ( (exists bloc_size, exists l1, exists l2, l = (l1 ++ ((bloc_adr, bloc_size, Free)::nil) ++ l2) /\ eval (var_e nptr) s = eval (nat_e (bloc_adr + 2 + bloc_size)) s) \/ (exists bloc_size, exists bloc_size2, exists l1, exists l2, l = (l1 ++ ((bloc_adr, bloc_size, Free)::(bloc_adr + 2 + bloc_size, bloc_size2, Allocated)::nil) ++ l2) /\ eval (var_e nptr) s = eval null s) \/ (exists bloc_size, exists l1, l = (l1 ++ ((bloc_adr, bloc_size, Free)::nil)) /\ eval (var_e nptr) s = eval null s) ) ) ). red. simpl; intros. inversion_clear H3 as [l]. decompose [and] H4; clear H4. inversion_clear H10. inversion_clear H4. inversion_clear H10. inversion_clear H4 as [l1]. inversion_clear H10 as [l2]. decompose [and] H4; clear H4. exists l. intuition. exists x0. split; auto. left. exists x1. exists l1; exists l2. auto. apply semax_strengthen_pre with (fun s => fun h =>exists l, Heap_List l adr 0 s h /\ In (x,sizex,Allocated) l /\ (ArrayI (x+2) lx ** TT) s h /\ eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ (exists bloc_adr, eval (var_e cptr) s = Z_of_nat bloc_adr /\ ( (exists bloc_size, exists l1, exists l2, l = (l1 ++ ((bloc_adr, bloc_size, Free)::nil) ++ l2) /\ eval (var_e nptr) s = eval (nat_e (bloc_adr + 2 + bloc_size)) s) ))). red. simpl. intros. inversion_clear H3. unfold eqb in H5. generalize (negb_true_is_false _ H5); clear H5; intro. generalize (Zeq_bool_false (store.lookup nptr s) 0); intro X; inversion_clear X. generalize (H5 H3); clear H3 H5 H6; intro. inversion_clear H4 as [l]. decompose [and] H5; clear H5. inversion_clear H11. inversion_clear H5. exists l. split; auto. split; auto. split; auto. split; auto. split; auto. exists x0. split; auto. inversion_clear H11. auto. inversion_clear H5. inversion_clear H11. inversion_clear H5. inversion_clear H11. inversion_clear H5. tauto. inversion_clear H11. inversion_clear H5. inversion_clear H11. tauto. apply semax_assign_var_lookup_backwards'' with (fun s => fun h =>exists l, Heap_List l adr 0 s h /\ In (x,sizex,Allocated) l /\ (ArrayI (x+2) lx ** TT) s h /\ eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ (exists bloc_adr, eval (var_e cptr) s = Z_of_nat bloc_adr /\ ( (exists bloc_size, exists bloc_size2, exists l1, exists l2, l = (l1 ++ ((bloc_adr, bloc_size, Free)::(bloc_adr + 2 + bloc_size, bloc_size2, Free)::nil) ++ l2) /\ eval (var_e nptr) s = eval (nat_e (bloc_adr + 2 + bloc_size)) s /\ eval (var_e stts) s = eval Free s) \/ (exists bloc_size, exists bloc_size2, exists l1, exists l2, l = (l1 ++ ((bloc_adr, bloc_size, Free)::(bloc_adr + 2 + bloc_size, bloc_size2, Allocated)::nil) ++ l2) /\ eval (var_e nptr) s = eval (nat_e (bloc_adr + 2 + bloc_size)) s /\ eval (var_e stts) s = eval Allocated s) \/ (exists bloc_size, exists l1, l = (l1 ++ ((bloc_adr, bloc_size, Free)::nil)) /\ eval (var_e nptr) s = eval (nat_e (bloc_adr + 2 + bloc_size)) s /\ eval (var_e stts) s = eval Allocated s) ) ) ). red. simpl; intros. inversion_clear H3 as [l]. decompose [and] H4; clear H4. inversion_clear H10. inversion_clear H4. inversion_clear H10. inversion_clear H4 as [l1]. inversion_clear H10 as [l2]. inversion_clear H4. induction l2. exists Allocated. rewrite H10 in H3. generalize (Heap_List_split' l1 ((x0, x1, Free) :: nil) adr s h H1); intro X; inversion_clear X. generalize H3; intro HL. generalize (H4 H3); clear H12 H3 H4; intros. inversion_clear H3. Decompose_sepcon H4 h1 h2. inversion_clear H14. inversion_clear H21. subst next0 x2 next. simpl in H24. Decompose_sepcon H24 h41 h42. Compose_sepcon h41 (heap.union h42 (heap.union h3 h1)). eapply mapsto_equiv. apply H18. simpl. rewrite H11. auto with *. trivial. Intro_sepimp h'41 h'. assert (heap.equal h'41 h41). eapply singleton_equal. apply H25. apply H18. simpl. rewrite H11. auto with *. trivial. assert (heap.equal h' h). Equal_heap. red. exists l. split. eapply Heap_List_heap_equal. apply H28. rewrite H10. Resolve_simpl1. split; auto. split. eapply ArrayITT_heap_cong. apply heap.equal_sym. apply H28. Resolve_simpl1. split. Resolve_simpl1. split. Resolve_simpl1. exists x0. split. Resolve_simpl1. right; right. exists x1. exists l1. split; auto. split. Resolve_simpl1. Resolve_simpl1. inversion H14. clear IHl2. induction a; induction a. exists b. rewrite H10 in H3. generalize (Heap_List_split' l1 ((x0, x1, Free) :: (a, b0, b) :: l2) adr s h H1); intro X; inversion_clear X. generalize (H4 H3); clear H4 H12; intros. inversion_clear H4. Decompose_sepcon H12 h1 h2. inversion_clear H15. subst x2 next. inversion_clear H22. subst next a. simpl in H26. rewrite sep.con_assoc_equiv in H26. rewrite sep.con_assoc_equiv in H26. Decompose_sepcon H26 h51 h52. Compose_sepcon h51 (heap.union h52 (heap.union h6 (heap.union h3 h1))). eapply mapsto_equiv. apply H23. simpl. rewrite H11. auto with *. trivial. Intro_sepimp h'51 h'. assert (heap.equal h'51 h51). eapply singleton_equal. apply H29. apply H23. simpl. rewrite H11. auto with *. trivial. assert (heap.equal h' h). Equal_heap. red. exists l. split. eapply Heap_List_heap_equal. apply H32. rewrite H10. Resolve_simpl1. split; auto. split. eapply ArrayITT_heap_cong. apply heap.equal_sym. apply H32. Resolve_simpl1. split. Resolve_simpl1. split. Resolve_simpl1. exists x0. split. Resolve_simpl1. inversion_clear H19. subst b. right; left. exists x1; exists b0. exists l1; exists l2. split; auto. split. Resolve_simpl1. Resolve_simpl1. subst b. left. exists x1; exists b0. exists l1; exists l2. split; auto. split. Resolve_simpl1. Resolve_simpl1. apply semax_ifte. apply semax_strengthen_pre with (fun s => fun h =>exists l, Heap_List l adr 0 s h /\ In (x,sizex,Allocated) l /\ (ArrayI (x+2) lx ** TT) s h /\ eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ (exists bloc_adr, eval (var_e cptr) s = Z_of_nat bloc_adr /\ (exists bloc_size, exists bloc_size2, exists l1, exists l2, l = (l1 ++ ((bloc_adr, bloc_size, Free)::(bloc_adr + 2 + bloc_size, bloc_size2, Free)::nil) ++ l2) /\ eval (var_e nptr) s = eval (nat_e (bloc_adr + 2 + bloc_size)) s /\ eval (var_e stts) s = eval Free s) )). red. simpl; intros. inversion_clear H3. unfold eqb in H5. generalize (Zeq_bool_true _ _ H5); clear H5; intros. inversion_clear H4 as [l]. decompose [and] H5; clear H5. inversion_clear H11. inversion_clear H5. exists l. split; auto. split; auto. split; auto. split; auto. split; auto. exists x0. split; auto. inversion_clear H11. auto. inversion_clear H5. inversion_clear H11. inversion_clear H5. inversion_clear H11. inversion_clear H5. decompose [and] H11; clear H11. rewrite H14 in H3. inversion H3. inversion_clear H11. inversion_clear H5. decompose [and] H11; clear H11. rewrite H14 in H3. inversion H3. apply semax_assign_var_lookup_backwards'' with (fun s => fun h =>exists l, Heap_List l adr 0 s h /\ In (x,sizex,Allocated) l /\ (ArrayI (x+2) lx ** TT) s h /\ eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ (exists bloc_adr, eval (var_e cptr) s = Z_of_nat bloc_adr /\ (exists bloc_size, exists bloc_size2, exists l1, exists l2, l = (l1 ++ ((bloc_adr, bloc_size, Free)::(bloc_adr + 2 + bloc_size, bloc_size2, Free)::nil) ++ l2) /\ eval (var_e nptr) s = eval (nat_e (bloc_adr + 2 + bloc_size)) s /\ eval (var_e stts) s = eval (nat_e (bloc_adr + 2 + bloc_size + 2 + bloc_size2)) s) )). red. simpl; intros. inversion_clear H3 as [l]. decompose [and] H4; clear H4. inversion_clear H10. inversion_clear H4. inversion_clear H10. inversion_clear H4. inversion_clear H10 as [l1]. inversion_clear H4 as [l2]. decompose [and] H10; clear H10. exists (nat_e (x0 + 2 + x1 + 2 + x2)). eapply Heap_List_var_lookup_next. apply H3. rewrite H4. apply in_or_app. right. simpl. right; left. intuition. auto. red. exists l. split. Resolve_simpl1. split; auto. split. Resolve_simpl1. split. Resolve_simpl1. split. Resolve_simpl1. exists x0. split. Resolve_simpl1. exists x1; exists x2. exists l1; exists l2. split; auto. split. Resolve_simpl1. Resolve_simpl1. intros. inversion_clear H11. inversion_clear H14. decompose [and] H15; clear H15. exists x3; split. eapply Heap_List_heap_equal. apply heap.equal_sym. apply H10. auto. split; auto. split. eapply ArrayITT_heap_cong. apply H10. auto. auto. apply semax_assign_lookup_expr_backwards'' with (fun s => fun h =>exists l, Heap_List l adr 0 s h /\ In (x,sizex,Allocated) l /\ (ArrayI (x+2) lx ** TT) s h /\ eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ (exists bloc_adr, eval (var_e cptr) s = Z_of_nat bloc_adr /\ (exists bloc_size, exists l1, exists l2, l = (l1 ++ ((bloc_adr, bloc_size, Free)::nil) ++ l2) /\ eval (var_e stts) s = eval (nat_e (bloc_adr + 2 + bloc_size)) s) )). red. simpl; intros. inversion_clear H3 as [l]. decompose [and] H4; clear H4. inversion_clear H10. inversion_clear H4. inversion_clear H10. inversion_clear H4. inversion_clear H10 as [l1]. inversion_clear H4 as [l2]. decompose [and] H10; clear H10. subst l. exists (nat_e (x0 + 2 + x1)). generalize (Compaction l1 l2 x0 x1 x2 adr s h H1 H3); intro. Decompose_sepcon H4 h1 h2. Compose_sepcon h1 h2. eapply mapsto_equiv. apply H10. simpl. rewrite H9. trivial. trivial. Intro_sepimp h'1 h'. red in H15. generalize (H15 h'1); clear H15; intros. assert (heap.disjoint h2 h'1 /\ (nat_e x0 +e int_e 1%Z |-> nat_e (x0 + x1 + 4 + x2)) s h'1). split. auto. eapply mapsto_equiv. apply H16. simpl. rewrite H9. trivial. simpl. rewrite H13. assert (x0 + 2 + x1 + 2 + x2 = x0 + x1 + 4 + x2). omega. rewrite H18; auto. generalize (H15 H18 h' H17); clear H15 H18; intro. exists (l1 ++ ((x0, x1 + 2 + x2, Free) :: nil) ++ l2). split; auto. split. apply in_or_app. generalize (in_app_or _ _ _ H6); intro. inversion_clear H18. left; auto. simpl in H19. inversion_clear H19. inversion H18. inversion_clear H18. inversion H19. right; simpl; right; auto. split. eapply Data_destructive_update_inv. generalize (Heap_List_block_pos _ _ _ _ _ _ _ H3 H6); intro. intuition. apply H5. apply H4. apply H11. apply H10. eapply mapsto_equiv. apply H16. simpl. unfold next. intuition. intuition. Disjoint_heap. Equal_heap. generalize (in_app_or _ _ _ H6); intro X; inversion_clear X. generalize (Heap_List_block_block_pos l1 (((x0, x1 + 2 + x2, Free) :: nil) ++ l2) adr s h' x sizex Allocated x0 (x1 + 2 + x2) Free H1 H15 H18); intros. simpl in H19. intuition. rewrite lx_length. right. simpl. assert (1 = Z_of_nat 1)%Z. intuition. rewrite H20; clear H20. rewrite <- inj_plus. assert (forall x y, x >= y -> (Z_of_nat x >= Z_of_nat y)%Z). intuition. apply H20. omega. simpl in H18. inversion_clear H18. inversion H19. inversion_clear H19. inversion H18. rewrite ass_app in H15. generalize (Heap_List_block_block_pos (l1 ++ (((x0, x1 + 2 + x2, Free) :: nil))) l2 adr s h' x0 (x1 + 2 + x2) Free x sizex Allocated H1 H15); intros. assert ( In (x0, x1 + 2 + x2, Free) (l1 ++ (x0, x1 + 2 + x2, Free) :: nil)). intuition. generalize (H19 H20 H18); intros. assert (forall x y, x < y -> (Z_of_nat x < Z_of_nat y)%Z). intuition. left. simpl. assert (1 = Z_of_nat 1)%Z. intuition. rewrite H23; clear H23. rewrite <- inj_plus. apply H22. omega. split; auto. split; auto. exists x0. split; auto. exists (x1 + 2 + x2). exists l1; exists l2. split; auto. rewrite H13. auto with *. apply semax_assign_var_e'. red. simpl; intros. red. inversion_clear H3 as [l]. decompose [and] H4; clear H4. exists l. split. Resolve_simpl1. split; auto. split. Resolve_simpl1. split. Resolve_simpl1. split. Resolve_simpl1. inversion_clear H10. inversion_clear H4. exists x0. split. Resolve_simpl1. inversion_clear H10. inversion_clear H4 as [l1]. inversion_clear H10 as [l2]. inversion_clear H4. left. exists x1. exists l1; exists l2. split; auto. Resolve_simpl1. apply semax_strengthen_pre with (fun s => fun h =>exists l, Heap_List l adr 0 s h /\ In (x,sizex,Allocated) l /\ (ArrayI (x+2) lx ** TT) s h /\ eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ (exists bloc_adr, eval (var_e cptr) s = Z_of_nat bloc_adr /\ ( (exists bloc_size, exists bloc_size2, exists l1, exists l2, l = (l1 ++ ((bloc_adr, bloc_size, Free)::(bloc_adr + 2 + bloc_size, bloc_size2, Allocated)::nil) ++ l2) /\ eval (var_e nptr) s = eval (nat_e (bloc_adr + 2 + bloc_size)) s /\ eval (var_e stts) s = eval Allocated s) \/ (exists bloc_size, exists l1, l = (l1 ++ ((bloc_adr, bloc_size, Free)::nil)) /\ eval (var_e nptr) s = eval (nat_e (bloc_adr + 2 + bloc_size)) s /\ eval (var_e stts) s = eval Allocated s) ) ) ). red. simpl; intros. inversion_clear H3. unfold eqb in H5. generalize (Zeq_bool_false (store.lookup stts s) 1); intro X; inversion_clear X. generalize (H3 H5); clear H5 H3 H6; intros. inversion_clear H4 as [l]. decompose [and] H5; clear H5. inversion_clear H11. inversion_clear H5. exists l. split; auto. split; auto. split; auto. split; auto. split; auto. exists x0. split; auto. inversion_clear H11. inversion_clear H5. inversion_clear H11. inversion_clear H5. inversion_clear H11. decompose [and] H5; clear H5. tauto. inversion_clear H5. left; auto. right; auto. apply semax_assign_var_e'. red. simpl; intros. red. inversion_clear H3 as [l]. decompose [and] H4; clear H4. inversion_clear H10. inversion_clear H4. exists l. split. Resolve_simpl1. split; auto. split. Resolve_simpl1. split. Resolve_simpl1. split. Resolve_simpl1. exists x0. split. Resolve_simpl1. inversion_clear H10. right. left. inversion_clear H4. inversion_clear H10. inversion_clear H4 as [l1]. inversion_clear H10 as [l2]. decompose [and] H4; clear H4. exists x1; exists x2. exists l1; exists l2. split; auto. Resolve_simpl1. right; right. inversion_clear H4. inversion_clear H10 as [l1]. decompose [and] H4; clear H4. exists x1. exists l1. split; auto. Resolve_simpl1. red. simpl. intros. inversion_clear H3. generalize (negb_false_is_true _ H5); clear H5; intro. unfold eqb in H3. generalize (Zeq_bool_true _ _ H3); clear H3; intro. inversion_clear H4 as [l]. decompose [and] H5; clear H5. inversion_clear H11. inversion_clear H5. inversion_clear H11. inversion_clear H5. inversion_clear H11. inversion_clear H5. inversion_clear H11. inversion_clear H5. rewrite H3 in H12. assert (0 = Z_of_nat 0)%Z. trivial. rewrite H5 in H12. generalize (Z_of_nat_inj _ _ H12); intro. assert (~(0 = x0 + 2 + x1)). omega. tauto. inversion_clear H5. inversion_clear H11. inversion_clear H5. inversion_clear H11 as [l1]. inversion_clear H5 as [l2]. decompose [and] H11; clear H11. exists l. intuition. exists x0. split; auto. left. exists x1. exists Free. exists l1; exists ((x0 + 2 + x1, x2, Allocated) :: l2). auto. inversion_clear H11. inversion_clear H5. inversion_clear H11. exists l. intuition. exists x0. split; auto. left. exists x1; exists Free. exists x2; exists (@nil (loc * nat * expr)). trivial. apply semax_skip'. red. simpl; intros. inversion_clear H3. inversion_clear H4 as [l]. decompose [and] H3; clear H3. inversion_clear H11. inversion_clear H3. exists l. split; auto. split; auto. split; auto. split; auto. split; auto. exists x0; split; auto. inversion_clear H11. left. inversion_clear H3. inversion_clear H11. inversion_clear H3. inversion_clear H11. inversion_clear H3. exists x1; exists x2; exists x3; exists x4. auto. inversion_clear H3. right; auto. apply semax_assign_var_lookup_backwards'. red. simpl. intros. inversion_clear H3 as [l]. decompose [and] H4; clear H4. inversion_clear H10. inversion_clear H4. inversion_clear H10. inversion_clear H4. inversion_clear H10. inversion_clear H4 as [l1]. inversion_clear H10 as [l2]. exists (nat_e (x0 + 2 + x1)). eapply Heap_List_var_lookup_next. apply H3. rewrite H4. apply in_or_app. right; simpl; left; intuition. auto. red. exists l. split. Resolve_simpl1. split; auto. split. Resolve_simpl1. split. Resolve_simpl1. split. Resolve_simpl1. exists (x0 + 2 + x1). split. Resolve_simpl1. induction l2. right. left. rewrite H4 in H3. generalize (Heap_List_split' l1 ((x0,x1,x2)::nil) adr s h H1); intro X; inversion_clear X. generalize (H10 H3); clear H3 H11 H10; intros. inversion_clear H3. Decompose_sepcon H10 h1 h2. inversion_clear H13. subst x3 next. Compose_sepcon (heap.union h1 h3) h4. eapply Heap_List_inde_store with s. rewrite H4. assert (x0 + 2 + x1 > 0). omega. generalize (Heap_List_split l1 ((x0,x1,x2)::nil) adr (x0 + 2 + x1) s (heap.union h1 h3) H1 H13); intro X; inversion_clear X. apply H17; clear H13 H17 H16. exists x0. Compose_sepcon h1 h3. auto. eapply Heap_List_suiv with (h1 := h3) (h2 := heap.emp). Disjoint_heap. Equal_heap. auto. intuition. auto. auto. auto. eapply Heap_List_trans. omega. trivial. red; apply heap.equal_refl. eapply Heap_List_inde_store with s. auto. clear IHl2. induction a; induction a. left. exists b0; exists b; exists (l1 ++ (x0, x1, x2)::nil); exists l2. rewrite H4 in H3. generalize (Heap_List_split' l1 ((x0,x1,x2)::(a, b0, b)::l2) adr s h H1); intro X; inversion_clear X. generalize (H10 H3); clear H3 H11 H10; intro. inversion_clear H3. Decompose_sepcon H10 h1 h2. inversion_clear H13. subst x3 next. inversion_clear H20. subst a. rewrite H4. rewrite app_ass. simpl. trivial. intros. inversion_clear H11. decompose [and] H12; clear H12. exists x3. split. eapply Heap_List_heap_equal. apply heap.equal_sym. apply H10. auto. split; auto. split; auto. eapply ArrayITT_heap_cong. apply H10. auto. split; auto. split; auto. inversion_clear H18. inversion_clear H12. exists x4. split; auto. inversion_clear H18. auto. inversion_clear H12. right; left. Decompose_sepcon H18 h01 h02. exists h01; exists h02. split. Disjoint_heap. split. apply heap.equal_trans with h0. Equal_heap. Equal_heap. auto. auto. exists (nat_e 0). Decompose_sepcon H4 h1 h2. inversion_clear H13. subst next; clear H12. simpl in H16. Decompose_sepcon H16 h21 h22. Decompose_sepcon H17 h221 h222. red in H20. Compose_sepcon h221 (heap.union h21 h1). eapply mapsto_equiv. apply H17. simpl. rewrite H9. trivial. trivial. Intro_sepimp h'221 h'. red. assert (heap.equal h'221 h221). eapply singleton_equal. apply H21. apply H17. simpl. rewrite H9. trivial. trivial. assert (heap.equal h' h). Equal_heap. exists l. split. eapply Heap_List_heap_equal. apply H24. Resolve_simpl1. split; auto. split. eapply ArrayITT_heap_cong. apply heap.equal_sym. apply H24. Resolve_simpl1. split. Resolve_simpl1. split. Resolve_simpl1. exists 0. split. Resolve_simpl1. right. right. auto. inversion H12. red. simpl. intros. inversion_clear H3. generalize (negb_false_is_true _ H5); clear H5; intro. unfold eqb in H3. generalize (Zeq_bool_true _ _ H3); clear H3; intro. inversion_clear H4 as [l]. decompose [and] H5; clear H5. inversion_clear H11. inversion_clear H5. assert (0 = Z_of_nat 0)%Z. trivial. rewrite H3 in H10. rewrite H5 in H10. clear H5. generalize (Z_of_nat_inj _ _ H10); intro; subst x0. inversion_clear H11. inversion_clear H5. inversion_clear H11. inversion_clear H5 as [l1]. inversion_clear H11 as [l2]. rewrite H5 in H4. generalize (Heap_List_split' l1 ((0,x0,x1)::l2) adr s h H1); intro X; inversion_clear X. generalize (H11 H4); clear H4 H12 H11; intro. inversion_clear H4. Decompose_sepcon H11 h1 h2. inversion_clear H14. subst x2 next. inversion_clear H19. inversion_clear H5. Decompose_sepcon H11 h1 h2. inversion_clear H14. inversion H16. inversion H13. exists l. tauto. Qed. Definition split_specif := forall adr cptr sz size tmp sizex x result entry lx, length lx = sizex -> size > 0 -> sizex > 0 -> adr > 0 -> var.set (hmStart::entry::cptr::sz::tmp::result::nil) -> {{fun s => fun h => eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ (exists finded_free_block, exists size'', exists l2, size'' >= size /\ In (finded_free_block,size'',Free) l2 /\ eval (var_e entry) s = (Z_of_nat finded_free_block) /\ finded_free_block > 0 /\ Heap_List l2 adr 0 s h /\ In (x,sizex,Allocated) l2 /\ (ArrayI (x+2) lx ** TT) s h /\ finded_free_block <> x) }} proj_cmd (split entry size cptr sz) {{fun s => fun h => (exists l1, exists y, y > 0 /\ eval (var_e entry) s = Z_of_nat (y) /\ (exists size'', size'' >= size /\ Heap_List l1 adr 0 s h /\ In (x,sizex,Allocated) l1 /\ (ArrayI (x+2) lx ** TT) s h /\ In (y,size'',Allocated) l1 /\ y <> x))}}. Lemma split_verif : split_specif. unfold split_specif. do 10 intro. intro ArrayI_inv. intros. unfold split. simpl. apply semax_seq with (fun s => fun h => eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ (exists finded_free_block, exists size'', exists l2, size'' >= size /\ In (finded_free_block,size'',Free) l2 /\ eval (var_e entry) s = (Z_of_nat finded_free_block) /\ finded_free_block > 0 /\ Heap_List l2 adr 0 s h /\ In (x,sizex,Allocated) l2 /\ finded_free_block <> x /\ eval (var_e sz) s = Z_of_nat (size'') /\ (ArrayI (x+2) lx ** TT) s h )). apply semax_assign_var_lookup_backwards'' with (fun s => fun h => eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ (exists finded_free_block, exists size'', exists l2, size'' >= size /\ In (finded_free_block,size'',Free) l2 /\ eval (var_e entry) s = (Z_of_nat finded_free_block) /\ finded_free_block > 0 /\ Heap_List l2 adr 0 s h /\ In (x,sizex,Allocated) l2 /\ finded_free_block <> x /\ eval (var_e sz) s = Z_of_nat (finded_free_block + 2 + size'') /\ (ArrayI (x+2) lx ** TT) s h )). red. simpl. intros. decompose [and] H3; clear H3. inversion_clear H7. inversion_clear H3. inversion_clear H5 as [l]. decompose [and] H3; clear H3. exists (nat_e (x0 + 2 + x1)). eapply Heap_List_var_lookup_next. apply H10. apply H8. simpl. auto. red. split. Resolve_simpl1. split. Resolve_simpl1. exists x0. exists x1. exists l. split; auto. split; auto. split. Resolve_simpl1. split; auto. split. Resolve_simpl1. split; auto. split; auto. split. Resolve_simpl1. Resolve_simpl1. intros. decompose [and] H13; clear H13. inversion_clear H18. inversion_clear H13. inversion_clear H16. decompose [and] H13; clear H13. split; auto. split; auto. exists x2. exists x3; exists x4. split; auto. split; auto. split; auto. split; auto. split. eapply Heap_List_heap_equal. apply heap.equal_sym. apply H3. auto. split; auto. split; auto. split; auto. eapply ArrayITT_heap_cong; [apply H3 | auto]. apply semax_assign_var_e'' with (fun s => fun h => eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ (exists finded_free_block, exists size'', exists l2, size'' >= size /\ In (finded_free_block,size'',Free) l2 /\ eval (var_e entry) s = (Z_of_nat finded_free_block) /\ finded_free_block > 0 /\ Heap_List l2 adr 0 s h /\ In (x,sizex,Allocated) l2 /\ finded_free_block <> x /\ eval (var_e sz) s = Z_of_nat (size'') /\ (ArrayI (x+2) lx ** TT) s h )). red. simpl. intros. decompose [and] H3; clear H3. inversion_clear H7. inversion_clear H3. inversion_clear H5 as [l]. decompose [and] H3; clear H3. red. split. Resolve_simpl1. split. Resolve_simpl1. exists x0. exists x1. exists l. split; auto. split; auto. split. Resolve_simpl1. split; auto. split. Resolve_simpl1. split; auto. split; auto. split. Resolve_simpl1. simpl. rewrite H13; rewrite H7. rewrite <- inj_minus1. assert (2 = Z_of_nat 2)%Z. intuition. rewrite H3. rewrite <- inj_minus1. intuition. intuition. intuition. Resolve_simpl1. apply semax_ifte. apply semax_assign_var_e'. red. simpl. intros. inversion_clear H3. decompose [and] H4; clear H4. inversion_clear H8. inversion_clear H4. inversion_clear H6 as [l]. decompose [and] H4; clear H4. rewrite H14 in H5. generalize (Zgt_cases 0 (Z_of_nat x1)); intro. rewrite H5 in H4. assert (0 < Z_of_nat x1)%Z. intuition. assert (forall x, ( 0 < x) -> (0 > x) -> False)%Z. intuition. generalize (H17 (Z_of_nat x1) H15 H4). intuition. apply semax_skip'. red. intuition. apply semax_seq with (fun s => fun h => (exists l1, exists y, y > 0 /\ eval (var_e entry) s = Z_of_nat (y) /\ (exists size'', size'' >= size /\ Heap_List l1 adr 0 s h /\ In (x,sizex,Allocated) l1 /\ In (y,size'',Free) l1 /\ y <> x) /\ (ArrayI (x+2) lx ** TT) s h )). apply semax_ifte. apply semax_assign_var_e'' with (fun s => fun h => eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ (exists finded_free_block, exists size'', exists l2, size'' >= size /\ In (finded_free_block,size'',Free) l2 /\ eval (var_e entry) s = (Z_of_nat finded_free_block) /\ finded_free_block > 0 /\ Heap_List l2 adr 0 s h /\ In (x,sizex,Allocated) l2 /\ finded_free_block <> x /\ eval (var_e sz) s = Z_of_nat (size'') /\ eval (var_e cptr) s = eval ((var_e entry +e nat_e 2) +e nat_e size) s /\ (Z_of_nat size'' >= Z_of_nat size + 8 + 2)%Z /\ (ArrayI (x+2) lx ** TT) s h )). red. simpl. intros. inversion_clear H3. decompose [and] H4; clear H4. inversion_clear H8. inversion_clear H4. inversion_clear H6 as [l]. decompose [and] H4; clear H4. rewrite H14 in H5. generalize (Zge_cases (Z_of_nat x1) (Z_of_nat size + 8 + 2)); intro. rewrite H5 in H4. clear H5. red. split. Resolve_simpl1. split. Resolve_simpl1. exists x0. exists x1. exists l. split; auto. split; auto; split. Resolve_simpl1. split; auto; split. Resolve_simpl1. split; auto. split; auto. split. Resolve_simpl1. split. Resolve_simpl1. simpl. rewrite H8. symmetry. cut (store.lookup entry (store.update cptr (Z_of_nat x0 + 2 + Z_of_nat size)%Z s) = Z_of_nat x0). intuition. Resolve_simpl1. split; auto. Resolve_simpl1. apply semax_assign_var_lookup_backwards'' with (fun s => fun h => eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ (exists finded_free_block, exists size'', exists l2, size'' >= size /\ In (finded_free_block,size'',Free) l2 /\ eval (var_e entry) s = (Z_of_nat finded_free_block) /\ finded_free_block > 0 /\ Heap_List l2 adr 0 s h /\ In (x,sizex,Allocated) l2 /\ finded_free_block <> x /\ eval (var_e sz) s = Z_of_nat (finded_free_block + 2 + size'') /\ eval (var_e cptr) s = eval ((var_e entry +e nat_e 2) +e nat_e size) s /\ (Z_of_nat size'' >= Z_of_nat size + 8 + 2)%Z /\ (ArrayI (x+2) lx ** TT) s h )). red. simpl. intros. inversion_clear H3. inversion_clear H5. inversion_clear H6. inversion_clear H5. inversion_clear H6 as [l]. decompose [and] H5; clear H5. exists (nat_e (x0 + 2 + x1)). eapply Heap_List_var_lookup_next. apply H10. apply H8. simpl. auto. red. split. Resolve_simpl1. split. Resolve_simpl1. exists x0; exists x1; exists l. split; auto. split; auto. split. Resolve_simpl1. split; auto. split. Resolve_simpl1. split; auto. split; auto. split. Resolve_simpl1. auto. rewrite <- store.lookup_update. rewrite <- store.lookup_update. rewrite H14. split; auto. split; auto. Resolve_simpl1. Resolve_var_neq. Resolve_var_neq. intros. decompose [and] H16; clear H16. inversion_clear H21. inversion_clear H16. inversion_clear H19. decompose [and] H16; clear H16. split; auto. split; auto. exists x2; exists x3; exists x4. split; auto. split; auto. split; auto. split; auto. split. eapply Heap_List_heap_equal. apply heap.equal_sym. apply H5. auto. split; auto. split; auto. split; auto. split; auto. split; auto. eapply ArrayITT_heap_cong; [apply H5 | auto]. apply semax_strengthen_pre with (fun s => fun h => eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ (exists finded_free_block, exists size'', exists l1, exists l2, size'' >= size /\ eval (var_e entry) s = (Z_of_nat finded_free_block) /\ finded_free_block > 0 /\ Heap_List (l1 ++ ((finded_free_block,size'',Free)::nil) ++ l2) adr 0 s h /\ (In (x,sizex,Allocated) l1 \/ In (x,sizex,Allocated) l2) /\ finded_free_block <> x /\ eval (var_e sz) s = Z_of_nat (finded_free_block + 2 + size'') /\ eval (var_e cptr) s = eval ((var_e entry +e nat_e 2) +e nat_e size) s /\ (Z_of_nat size'' >= Z_of_nat size + 8 + 2)%Z /\ (ArrayI (x+2) lx ** TT) s h )). red. simpl. intros. decompose [and] H3; clear H3. inversion_clear H7. inversion_clear H3. inversion_clear H5 as [l]. decompose [and] H3; clear H3. split; auto. split; auto. exists x0. exists x1. generalize (list_split' l x0 x1 Free H8); intro. inversion_clear H3 as [l1]. inversion_clear H16 as [l2]. exists l1; exists l2. split; auto. split; auto. split; auto. split; rewrite H3 in H10; auto. split. rewrite H3 in H11. simpl in H11. generalize (in_app_or _ _ _ H11); intro X; inversion_clear X. left; auto. simpl in H16. inversion_clear H16. inversion H18. right; auto. split; auto. apply semax_seq with ( fun s0 => fun h0 => exists e'' : expr, ((cptr -.> status |-> e'') ** ((cptr -.> status |-> Free) -* (fun (s1 : store.s) (h1 : heap.h) => exists e''0 : expr, ((entry -.> next |-> e''0) ** ((entry -.> next |-> var_e cptr) -* (fun (s : store.s) (h : heap.h) => exists l1 : list (loc * nat * expr), (exists y : nat, y > 0 /\ eval (var_e entry) s = Z_of_nat y /\ (exists size'' : nat, size'' >= size /\ Heap_List l1 adr 0 s h /\ In (x, sizex, Allocated) l1 /\ In (y, size'', Free) l1 /\ y <> x) /\ (ArrayI (x+2) lx ** TT) s h )))) s1 h1))) s0 h0 ). apply semax_assign_lookup_expr_backwards'. red. simpl. intros. decompose [and] H3; clear H3. inversion_clear H7 as [finded_free_block]. inversion_clear H3 as [size'']. inversion_clear H5 as [l1]. inversion_clear H3 as [l2]. decompose [and] H5; clear H5. assert (exists size1, size'' = size + 2 + size1). assert (size'' >= size + 8 + 2). omega. exists (size'' - 2 - size). omega. inversion_clear H5 as [size2]. rewrite H15 in H9. generalize (Splitting l1 l2 finded_free_block size size2 s h adr H1 H9); intro. inversion_clear H5. exists x0. Decompose_sepcon H17 h1 h2. Compose_sepcon h1 h2. eapply mapsto_equiv. apply H17. simpl. rewrite H13. unfold next. rewrite H8. assert (2 = Z_of_nat 2)%Z. trivial. assert (1 = Z_of_nat 1)%Z. trivial. rewrite H19; rewrite H21. clear H19 H21. repeat rewrite <- inj_plus. auto with *. trivial. Intro_sepimp h'1 h'. assert ((ArrayI (x+2) lx ** TT) s h'). eapply Data_destructive_update_inv. intuition. apply H16. apply H5. apply H18. apply H17. eapply mapsto_equiv. apply H21. simpl. simpl. rewrite H13. rewrite H8. unfold next. assert (2 = Z_of_nat 2)%Z. trivial. rewrite H23; clear H23. assert (1 = Z_of_nat 1)%Z. trivial. rewrite H23; clear H23. repeat rewrite <- inj_plus. intuition. simpl. assert (store.lookup sz s = eval (nat_e (finded_free_block + 2 + size'')) s). apply H12. apply H23. Disjoint_heap. Equal_heap. inversion_clear H10. generalize (Heap_List_block_block_pos l1 ((finded_free_block, size + 2 + size2, Free) :: l2) adr s h x sizex Allocated finded_free_block (size + 2 + size2) Free H1 H9 H23); intros. simpl in H10. intuition. rewrite ArrayI_inv. right. simpl. assert (forall x y, x >= y -> (Z_of_nat x >= Z_of_nat y)%Z). intuition. apply H24. omega. generalize (Heap_List_block_block_pos (l1 ++ (finded_free_block, size + 2 + size2, Free)::nil) l2 adr s h finded_free_block (size + 2 + size2) Free x sizex Allocated H1); intros. rewrite app_ass in H10. simpl in H10. intuition. assert (In (finded_free_block, size + 2 + size2, Free) (l1 ++ (finded_free_block, size + 2 + size2, Free) :: nil)). apply in_or_app. right; simpl; auto. left. generalize (H24 H10 H23); intros. simpl. assert (forall x y, x < y -> (Z_of_nat x < Z_of_nat y)%Z). intuition. apply H26. omega. generalize H23; intro ArrayI_in_h'; clear H23. red in H20. assert (heap.disjoint h2 h'1 /\ (nat_e (finded_free_block + 3 + size)|-> nat_e (finded_free_block + 4 + size + size2)) s h'1). split; auto. eapply mapsto_equiv. apply H21. simpl. rewrite H13. unfold next. rewrite H8. assert (2 = Z_of_nat 2)%Z. trivial. assert (1 = Z_of_nat 1)%Z. trivial. rewrite H23; rewrite H24. clear H23 H24. repeat rewrite <- inj_plus. auto with *. simpl. rewrite H12. rewrite H15. auto with *. generalize (H20 h'1 H23 h' H22); clear H20; intros. inversion_clear H20. Decompose_sepcon H24 h1' h2'. exists x1. Compose_sepcon h1' h2'. eapply mapsto_equiv. apply H24. simpl. rewrite H13. rewrite H8; unfold status. assert (2 = Z_of_nat 2)%Z. trivial. rewrite H26; clear H26. repeat rewrite <- inj_plus. auto with *. auto. Intro_sepimp h1'' h2''. assert ((ArrayI (x+2) lx ** TT) s h2''). eapply Data_destructive_update_inv. intuition. apply ArrayI_in_h'. apply H20. apply H25. apply H24. eapply mapsto_equiv. apply H28. simpl. simpl. rewrite H13. rewrite H8. unfold status. assert (2 = Z_of_nat 2)%Z. trivial. rewrite H30; clear H30. repeat rewrite <- inj_plus. intuition. intuition. Disjoint_heap. Equal_heap. inversion_clear H10. generalize (Heap_List_block_block_pos l1 ((finded_free_block, size + 2 + size2, Free) :: l2) adr s h x sizex Allocated finded_free_block (size + 2 + size2) Free H1 H9 H30); intros. simpl in H10. intuition. rewrite ArrayI_inv. right. simpl. assert (forall x y, x >= y -> (Z_of_nat x >= Z_of_nat y)%Z). intuition. apply H23. omega. generalize (Heap_List_block_block_pos (l1 ++ (finded_free_block, size + 2 + size2, Free)::nil) l2 adr s h finded_free_block (size + 2 + size2) Free x sizex Allocated H1); intros. rewrite app_ass in H10. simpl in H10. intuition. assert (In (finded_free_block, size + 2 + size2, Free) (l1 ++ (finded_free_block, size + 2 + size2, Free) :: nil)). apply in_or_app. right; simpl; auto. left. generalize (H23 H10 H30); intros. simpl. assert (forall x y, x < y -> (Z_of_nat x < Z_of_nat y)%Z). intuition. apply H34. omega. generalize H30; intro ArrayI_in_h2''; clear H30 ArrayI_in_h'. red in H27. assert (heap.disjoint h2' h1'' /\(nat_e (finded_free_block + 2 + size) |-> Free) s h1''). split; auto. eapply mapsto_equiv. apply H28. simpl. rewrite H13. rewrite H8. unfold status. assert (2 = Z_of_nat 2)%Z. trivial. rewrite H30; clear H30. repeat rewrite <- inj_plus. auto with *. auto. generalize (H27 h1'' H30 h2'' H29); clear H27; intros. inversion_clear H27. exists x2. Decompose_sepcon H31 h2''1 h2''2. Compose_sepcon h2''1 h2''2. eapply mapsto_equiv. apply H31. simpl. rewrite H8. unfold next. assert (1 = Z_of_nat 1)%Z. trivial. rewrite H33; clear H33. repeat rewrite <- inj_plus. auto with *. auto. Intro_sepimp h3 h4. red in H34. assert (heap.disjoint h2''2 h3 /\ (nat_e (finded_free_block + 1)|-> nat_e (finded_free_block + 2 + size)) s h3 ). split; auto. eapply mapsto_equiv. apply H35. simpl. rewrite H8. assert (1 = Z_of_nat 1)%Z. trivial. unfold next. rewrite H37; clear H37. repeat rewrite <- inj_plus. auto with *. simpl. rewrite H13. rewrite H8. assert (2 = Z_of_nat 2)%Z. trivial. rewrite H37; clear H37. repeat rewrite <- inj_plus. auto with *. generalize (H34 h3 H37 h4 H36); clear H34; intros. exists (l1 ++ ((finded_free_block, size, Free) :: (finded_free_block + 2 + size, size2, Free) :: nil) ++ l2). exists finded_free_block. split; auto. split; auto. split. exists size. split; auto. split; auto. split. apply in_or_app. inversion_clear H10. left; auto. right. simpl. right; right. auto. intuition. eapply Data_destructive_update_inv. intuition. apply ArrayI_in_h2''. apply H27. apply H32. apply H31. eapply mapsto_equiv. apply H35. simpl. rewrite H8. unfold next. assert (1 = Z_of_nat 1)%Z. trivial. rewrite H38; clear H38. repeat rewrite <- inj_plus. intuition. intuition. Disjoint_heap. Equal_heap. inversion_clear H10. generalize (Heap_List_block_block_pos l1 ((finded_free_block, size + 2 + size2, Free) :: l2) adr s h x sizex Allocated finded_free_block (size + 2 + size2) Free H1 H9 H38); intros. simpl in H10. intuition. rewrite ArrayI_inv. right. simpl. assert (forall x y, x >= y -> (Z_of_nat x >= Z_of_nat y)%Z). intuition. apply H37. omega. generalize (Heap_List_block_block_pos (l1 ++ (finded_free_block, size + 2 + size2, Free)::nil) l2 adr s h finded_free_block (size + 2 + size2) Free x sizex Allocated H1); intros. rewrite app_ass in H10. simpl in H10. intuition. assert (In (finded_free_block, size + 2 + size2, Free) (l1 ++ (finded_free_block, size + 2 + size2, Free) :: nil)). apply in_or_app. right; simpl; auto. left. generalize (H37 H10 H38); intros. simpl. assert (forall x y, x < y -> (Z_of_nat x < Z_of_nat y)%Z). intuition. apply H44. omega. apply semax_seq with ( fun s0 => fun h0 => exists e'' : expr, ((entry -.> next |-> e'') ** ((entry -.> next |-> var_e cptr) -* (fun (s : store.s) (h : heap.h) => exists l1 : list (loc * nat * expr), (exists y : nat, y > 0 /\ eval (var_e entry) s = Z_of_nat y /\ (exists size'' : nat, size'' >= size /\ Heap_List l1 adr 0 s h /\ In (x, sizex, Allocated) l1 /\ In (y, size'', Free) l1 /\ y <> x) /\ (ArrayI (x+2) lx ** TT) s h )))) s0 h0 ). apply semax_assign_lookup_expr_backwards' . red. intuition. apply semax_assign_lookup_expr_backwards' . red. intuition. eapply semax_skip'. red. simpl; intros. inversion_clear H3. decompose [and] H4; clear H4. inversion_clear H8. inversion_clear H4. inversion_clear H6 as [l]. decompose [and] H4; clear H4. exists l. exists x0. split; auto. split; auto. split. exists x1. split; auto. auto. apply semax_assign_lookup_expr_backwards' . red. simpl. intros. inversion_clear H3 as [l]. inversion_clear H4. decompose [and] H3; clear H3. inversion_clear H5. decompose [and] H3; clear H3. generalize (list_split' l x0 x1 Free H10); intro. inversion_clear H3 as [l1]. inversion_clear H11 as [l2]. rewrite H3 in H7. rewrite H3 in H9. generalize (Change_Status_Allocated l1 l2 x0 x1 adr s h H1 H9); intros. Decompose_sepcon H11 h1 h2. exists Free. Compose_sepcon h1 h2. eapply mapsto_equiv. apply H13. simpl. rewrite H6. intuition. intuition. Intro_sepimp h'1 h'. red in H16. assert (h2 # h'1 /\ (nat_e x0 |-> Allocated) s h'1). split. Disjoint_heap. eapply mapsto_equiv. apply H17. simpl; rewrite H6. intuition. intuition. generalize (H16 h'1 H19 h' H18); clear H16 H19; intros. exists (l1 ++ ((x0, x1, Allocated) :: nil) ++ l2). exists x0. split; auto. split; auto. exists x1. split; auto. split; auto. split. generalize (in_app_or _ _ _ H7); intro X; inversion_clear X. apply in_or_app. left; auto. simpl in H19. intuition. inversion H20. split. eapply Data_destructive_update_inv. intuition. apply H8. apply H11. auto. apply H13. eapply mapsto_equiv. apply H17. simpl; rewrite H6. intuition. intuition. auto. Disjoint_heap. Equal_heap. rewrite ArrayI_inv. generalize (in_app_or _ _ _ H7); intro. inversion_clear H19. generalize (Heap_List_split' l1 (((x0, x1, Allocated) :: nil) ++ l2) adr s h' H1); intro X; inversion_clear X. generalize (H19 H16); intro X; inversion_clear X; clear H19 H21. Decompose_sepcon H22 h1' h2'. generalize (Heap_List_block_end_pos l1 adr x2 x sizex Allocated s h1' H1 (Heap_List_start_pos _ _ _ _ H24) H21 H20); intros. right. simpl. assert (forall x y, x >= y -> (Z_of_nat x >= Z_of_nat y)%Z). intuition. apply H25. inversion_clear H24. subst next x2. omega. simpl in H20. inversion_clear H20. inversion H19. generalize (Heap_List_split' l1 (((x0, x1, Allocated) :: nil) ++ l2) adr s h' H1); intro X; inversion_clear X. generalize (H20 H16); intro X; inversion_clear X; clear H20 H21. Decompose_sepcon H22 h1' h2'. inversion_clear H24. generalize (Heap_List_block_pos l2 next x sizex Allocated s h4 H31 H19); intros. left. simpl. assert (forall x y, x < y -> (Z_of_nat x < Z_of_nat y)%Z). intuition. apply H32. omega. split. apply in_or_app. right; auto. apply in_or_app. left; auto. auto with *. trivial. Qed. Lemma hmAlloc_verif : hmAlloc_specif. unfold hmAlloc_specif. do 12 intro. intro lx_length. intros. unfold hmAlloc. simpl. (*******************************************) apply semax_assign_var_e'' with (fun s => fun h =>exists l1, Heap_List l1 adr 0 s h /\ In (x,sizex,Allocated) l1 /\ (ArrayI (x+2) lx ** TT) s h /\ eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s ). Resolve_assign_var. inversion_clear H3 as [l]. decompose [and] H4; clear H4. exists l. split. eapply Heap_List_inde_store. apply H3. split; auto. split. Resolve_simpl1. split. Resolve_simpl1. Resolve_simpl1. (*******************************************) (* Le Resultat du premier Find Free *) apply semax_seq with (fun s => fun h => exists l1, Heap_List l1 adr 0 s h /\ In (x,sizex,Allocated) l1 /\ (ArrayI (x+2) lx ** TT) s h /\ eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ ( (exists finded_free_block, exists size'', size'' >= size /\ In (finded_free_block,size'',Free) l1 /\ eval (var_e entry) s = (Z_of_nat finded_free_block) /\ finded_free_block > 0) \/ (eval (var_e entry) s = eval null s) )). assert (var.set (hmStart::entry::fnd::sz::stts::result::nil)). simpl. simpl in H. intuition. generalize (findFree_verif adr entry fnd sz stts size sizex x result lx lx_length H2 H1 H0 H3). intros. unfold findFree in H4; simpl in H4. apply H4. (*********************************) (* Si on trouve pas -> compact puis findfree *) apply semax_seq with (fun s => fun h => exists l1, Heap_List l1 adr 0 s h /\ In (x,sizex,Allocated) l1 /\ (ArrayI (x+2) lx ** TT) s h /\ eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ ( (exists finded_free_block, exists size'', size'' >= size /\ In (finded_free_block,size'',Free) l1 /\ eval (var_e entry) s = (Z_of_nat finded_free_block) /\ finded_free_block > 0) \/ (eval (var_e entry) s = eval null s) )). (* Est-ce qu'on a trouve ? *) apply semax_ifte. (*********************) (* non *) (* on peut eliminer le premier cas *) apply semax_strengthen_pre with (fun s => fun h =>exists l1, Heap_List l1 adr 0 s h /\ In (x,sizex,Allocated) l1 /\ (ArrayI (x+2) lx ** TT) s h /\ eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s ). red. simpl. intros. decompose [and] H3; clear H3. unfold eqb in H5. generalize (Zeq_bool_true _ _ H5); intro; clear H5. inversion_clear H4 as [l]. decompose [and] H5; clear H5. inversion_clear H11. inversion_clear H5. inversion_clear H10. decompose [and] H5; clear H5. assert (0%Z = Z_of_nat 0)%Z. trivial. rewrite H5 in H3. clear H5. rewrite H3 in H11. generalize (Z_of_nat_inj _ _ H11); intro. subst x0. inversion H14. exists l. auto. apply semax_assign_var_e'' with (fun s => fun h => exists l1, Heap_List l1 adr 0 s h /\ In (x,sizex,Allocated) l1 /\ (ArrayI (x+2) lx ** TT) s h /\ eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ eval (var_e cptr) s = eval (nat_e adr) s ). red. Resolve_assign_var. inversion_clear H3 as [l]. decompose [and] H4; clear H4. exists l. split. Resolve_simpl1. split; auto. split. Resolve_simpl1. split. Resolve_simpl1. split. Resolve_simpl1. Resolve_simpl1. (* la post cond de compact *) apply semax_seq with (fun s => fun h =>exists l1, Heap_List l1 adr 0 s h /\ In (x,sizex,Allocated) l1 /\ eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ (ArrayI (x+2) lx ** TT) s h ). (* pour matcher le preconde compact *) apply semax_strengthen_pre with (fun (s : store.s) (h : heap.h) => exists l1 : list (loc * nat * expr), Heap_List l1 adr 0 s h /\ In (x, sizex, Allocated) l1 /\ eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ eval (var_e cptr) s = eval (nat_e adr) s /\ (ArrayI (x+2) lx ** TT) s h). red. intuition. inversion_clear H3 as [l]. exists l. intuition. (* le compact *) assert (var.set (hmStart::entry::cptr::nptr::stts::result::nil)). simpl; simpl in H; intuition. generalize (compact_verif adr cptr nptr stts size sizex x result entry lx lx_length H2 H1 H0 H3). intros. unfold compact in H4; simpl in H4. simpl. apply H4. (* match la precond de finFree *) apply semax_strengthen_pre with (fun (s : store.s) (h : heap.h) => exists l1 : list (loc * nat * expr), Heap_List l1 adr 0 s h /\ In (x, sizex, Allocated) l1 /\ (ArrayI (x+2) lx ** TT) s h /\ eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s). red. intros. inversion_clear H3 as [l]. exists l. intuition. (* le findfree *) assert (var.set (hmStart::entry::fnd::sz::stts::result::nil)). simpl. simpl in H. intuition. generalize (findFree_verif adr entry fnd sz stts size sizex x result lx lx_length H2 H1 H0 H3). intros. unfold findFree in H4; simpl in H4. apply H4. (* oui *) apply semax_skip'. red. simpl; intros. inversion_clear H3. simpl in H4. unfold eqb in H4. generalize (Zeq_bool_false (store.lookup entry s) 0 ); intro X; inversion_clear X. generalize (H3 H5); clear H6 H3 H5; intro. inversion_clear H4 as [l]. decompose [and] H5; clear H5. inversion_clear H11. inversion_clear H5. inversion_clear H10. decompose [and] H5; clear H5. exists l. split; auto. split; auto. split; auto. split; auto. split; auto. left. exists x0; exists x1. split; auto. intuition. (***********************************) (* Est-ce qu'on a trouve ? *) apply semax_ifte. (*********************) (* non *) apply semax_assign_var_e'. red. simpl. intros. inversion_clear H3. unfold eqb in H5. generalize (Zeq_bool_true _ _ H5); intro. inversion_clear H4 as [l]. decompose [and] H6; clear H6. inversion_clear H12. inversion_clear H6. inversion_clear H11. inversion_clear H6. decompose [and] H12; clear H12. rewrite H3 in H14. assert (0%Z = Z_of_nat 0)%Z. intuition. rewrite H12 in H14. generalize (Z_of_nat_inj _ _ H14); intro. subst x0. inversion_clear H15. red. right. exists l. split. simpl. Resolve_simpl1. split. eapply Heap_List_inde_store. apply H4. auto. (* oui *) (* dans ce cas seul le premier cas est vrai *) apply semax_strengthen_pre with (fun s => fun h => eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ (exists finded_free_block, exists size'', exists l2, size'' >= size /\ In (finded_free_block,size'',Free) l2 /\ eval (var_e entry) s = (Z_of_nat finded_free_block) /\ finded_free_block > 0 /\ Heap_List l2 adr 0 s h /\ In (x,sizex,Allocated) l2 /\ (ArrayI (x+2) lx ** TT) s h) ). red. simpl. intros. decompose [and] H3; clear H3. simpl in H5; unfold eqb in H5. generalize (Zeq_bool_false (store.lookup entry s) 0); intro X; inversion_clear X. generalize (H3 H5); clear H5 H3 H6; intros. inversion_clear H4 as [l]. decompose [and] H5; clear H5. split; auto. split; auto. inversion_clear H11. inversion_clear H5. inversion_clear H10. decompose [and] H5; clear H5. exists x0. exists x1. exists l. split; auto. split; auto. contradiction. apply semax_strengthen_pre with (fun s => fun h => eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ (exists finded_free_block, exists size'', exists l2, size'' >= size /\ In (finded_free_block,size'',Free) l2 /\ eval (var_e entry) s = (Z_of_nat finded_free_block) /\ finded_free_block > 0 /\ Heap_List l2 adr 0 s h /\ In (x,sizex,Allocated) l2 /\ finded_free_block <> x /\ (ArrayI (x+2) lx ** TT) s h) ). red. simpl. intros. decompose [and] H3; clear H3. inversion_clear H7. inversion_clear H3. inversion_clear H5 as [l]. decompose [and] H3; clear H3. split; auto. split; auto. exists x0; exists x1. exists l. split; auto. split; auto. split; auto. split; auto. split; auto. split; auto. split. red; intros. generalize (list_split' l x0 x1 Free H8); intro. generalize (list_split' l x sizex Allocated H11); intro. inversion_clear H12 as [l1x0]. inversion_clear H15 as [l2x0]. inversion_clear H14 as [l1x]. inversion_clear H15 as [l2x]. generalize (H10); intro. rewrite H12 in H15. generalize (H10); intro. rewrite H14 in H16. generalize (Heap_List_split' l1x0 (((x0, x1, Free) :: nil) ++ l2x0) adr s h H0); intro X; inversion_clear X. generalize (Heap_List_split' l1x (((x, sizex, Allocated) :: nil) ++ l2x) adr s h H0); intro X; inversion_clear X. clear H20 H18. generalize (H17 H15); intro; clear H15 H17. generalize (H19 H16); intro; clear H19 H16. inversion_clear H18. inversion_clear H15. Decompose_sepcon H16 h1 h2. Decompose_sepcon H17 h'1 h'2. subst x0. simpl in H20; simpl in H23. inversion_clear H20. subst x2. inversion_clear H23. subst x3. Decompose_sepcon H28 h31 h32. Decompose_sepcon H34 h51 h52. simpl in H28. simpl in H36. Decompose_sepcon H36 h511 h512. Decompose_sepcon H28 h311 h312. assert (heap.lookup x h = Some (eval Allocated s)). eapply heap.lookup_equal. apply heap.equal_sym. assert (heap.equal h (heap.union h511 (heap.union h512 (heap.union h52 (heap.union h6 h'1))))). clear H18. Equal_heap. apply H45. assert (heap.lookup x (heap.union h511 (heap.union h512 (heap.union h52 (heap.union h6 h'1)))) = Some (eval Allocated s)). apply heap.lookup_union. Disjoint_heap. red in H39. inversion_clear H39. inversion_clear H45. eapply heap.lookup_equal with (heap.singleton x0 (eval Allocated s)). simpl. simpl in H39. rewrite (Z_of_nat2loc) in H39. injection H39; intro; subst x0. eapply heap.equal_sym. eapply heap.equal_trans with (heap.singleton x (eval Allocated s)). auto. assert (heap.lookup x h = Some (eval Free s)). eapply heap.lookup_equal. apply heap.equal_sym. assert (heap.equal h (heap.union h311 (heap.union h312 (heap.union h32 (heap.union h4 h1))))). clear H21. Equal_heap. apply H45. assert (heap.lookup x (heap.union h311 (heap.union h312 (heap.union h32 (heap.union h4 h1)))) = Some (eval Free s)). apply heap.lookup_union. Disjoint_heap. red in H42. inversion_clear H42. inversion_clear H45. eapply heap.lookup_equal with (heap.singleton x0 (eval Free s)). Equal_heap. simpl in H42. rewrite (Z_of_nat2loc) in H42. injection H42; intro; subst x0. apply heap.lookup_singleton. intuition. auto. simpl. apply heap.equal_refl. auto. simpl in H39. rewrite Z_of_nat2loc in H39. injection H39; intro; subst x0. apply heap.lookup_singleton. auto. auto. red in H39. red in H42. inversion_clear H42. simpl in H47; inversion_clear H47. inversion_clear H39. simpl in H47; inversion_clear H47. rewrite Z_of_nat2loc in H42; rewrite Z_of_nat2loc in H39. rewrite H42 in H39. injection H39; intro; subst x2; clear H39. injection H42; intro; subst x0; clear H42. assert (A1: h311 +++ (h312 +++ h32 +++ h4 +++ h1) === h). clear H21. Equal_heap. assert (A2: h511 +++ (h512 +++ h52 +++ h6 +++ h'1) === h). clear H18 A1. Equal_heap. assert (A3: heap.lookup x h311 = Some 1%Z). apply (heap.lookup_equal (heap.singleton x 1%Z) h311). Equal_heap. apply heap.lookup_singleton. assert (A4: heap.lookup x h511 = Some 0%Z). apply (heap.lookup_equal (heap.singleton x 0%Z) h511). Equal_heap. apply heap.lookup_singleton. assert (A5: heap.lookup x h = Some 1%Z). apply (heap.lookup_equal (h311 +++ (((h312 +++ h32) +++ h4) +++ h1)) h A1). apply heap.lookup_union. Disjoint_heap. auto. assert (A6: heap.lookup x h = Some 0%Z). apply (heap.lookup_equal (h511 +++ (h512 +++ h52 +++ h6 +++ h'1)) h A2). apply heap.lookup_union. Disjoint_heap. auto. rewrite A5 in A6. inversion A6. auto. auto. auto. auto. (* on matche la precond de split *) apply semax_strengthen_pre with (fun (s : store.s) (h : heap.h) => eval (var_e hmStart) s = eval (nat_e adr) s /\ eval (var_e result) s = eval null s /\ (exists finded_free_block : nat, (exists size'' : nat, (exists l2 : list (nat * nat * expr), size'' >= size /\ In (finded_free_block, size'', Free) l2 /\ eval (var_e entry) s = Z_of_nat finded_free_block /\ finded_free_block > 0 /\ Heap_List l2 adr 0 s h /\ In (x, sizex, Allocated) l2 /\ (ArrayI (x+2) lx ** TT) s h /\ finded_free_block <> x)))). red. intros. decompose [and] H3; clear H3. inversion_clear H7. inversion_clear H3. inversion_clear H5. decompose [and] H3; clear H3. split; auto. split; auto. exists x0; exists x1; exists x2. intuition. (* on split *) apply semax_seq with (fun s => fun h => (exists l1, exists y, y > 0 /\ eval (var_e entry) s = Z_of_nat (y) /\ (exists size'', size'' >= size /\ Heap_List l1 adr 0 s h /\ In (x,sizex,Allocated) l1 /\ (ArrayI (x+2) lx ** TT) s h /\ In (y,size'',Allocated) l1 /\ y <> x))). assert (var.set (hmStart :: entry :: cptr :: sz :: stts :: result :: nil)). simpl in H; simpl; intuition. generalize (split_verif adr cptr sz size stts sizex x result entry lx lx_length H2 H1 H0 H3); intros. unfold split in H4. simpl in H4. simpl. apply H4. apply semax_assign_var_e'. red. intros. inversion_clear H3 as [l]. inversion_clear H4. decompose [and] H3; clear H3. inversion_clear H7. decompose [and] H3; clear H3. red. left. exists l. exists x0. split; auto. split. simpl. simpl in H5. Resolve_simpl1. simpl in H6; rewrite H6. assert (2%Z = Z_of_nat 2). intuition. rewrite H3. rewrite inj_plus. auto. exists x1. split; auto. split. eapply Heap_List_inde_store. apply H8. split; auto. split. Resolve_simpl1. auto. Qed.