(*
 *  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.

(* Deallocation *)

(* cette fonction apporte un probleme:

    on peut remplace le flag du dernier bloc par Free,
    donc si apres il est precede par un bloc Free et qu'on compacte -> on pert de la place allouable *)
(* Original version form topsy => probleme (c.f. space06 paper) *)
Definition hmFree (address: loc) (entry: var.v) (addressEntry: var.v) (tmp: var.v) (result: var.v) :=
entry <- (var_e hmStart);
addressEntry <- ((nat_e address) -e (int_e 2%Z));
while' ((var_e entry =/= null) &&& (var_e entry =/= var_e addressEntry)) (TT) (
   tmp <-* (entry -.> next);
   entry <- (var_e tmp)
);
ifte (var_e entry =/= null) thendo (
   (entry -.> status) *<- Free;
   result <- HM_FREEOK
) elsedo (
   result <- HM_FREEFAILED
).

(* Version corrigee *)
(* Corrected Version *)
Definition hmFree' (address: loc) (entry: var.v) (addressEntry: var.v) (tmp: var.v) (result: var.v) :=
entry <- (var_e hmStart);
addressEntry <- ((nat_e address) -e (int_e 2%Z));

while' ((var_e entry =/= null) &&& (var_e entry =/= var_e addressEntry)) (TT) (
   tmp <-* (entry -.> next);
   entry <- (var_e tmp)
);

ifte (var_e entry =/= null) thendo (
   tmp <-* (entry -.> next);
   ifte (var_e tmp =/= null) thendo (
                    (entry -.> status) *<- Free;
                    result <- HM_FREEOK
   ) elsedo ( result <- HM_FREEFAILED)
) elsedo (
   result <- HM_FREEFAILED
).


Close Local Scope vc_scope.
Close Local Scope Z_scope.


(* hmFree *)

Definition hmFree'_specif1 := forall adr sizex x y entry cptr nptr result status lx,  
  length lx = sizex ->
  (var.set (hmStart::entry::cptr::nptr::result::nil)) -> 
  adr > 0 -> sizex > 0 ->

  {{fun s => fun h => exists l1,  Heap_List l1 adr 0 s h /\ 
      In (x,sizex,status) l1 /\ 
      (ArrayI (x+2) lx ** TT) s h /\
      x<>y /\
      eval (var_e hmStart) s = eval (nat_e adr) s }}
  
  proj_cmd (hmFree' (y+2) entry cptr nptr result)
  
  {{ fun s => fun h => exists l2,  Heap_List l2 adr 0 s h /\ 
       In (x,sizex,status) l2 /\
      (ArrayI (x+2) lx ** TT) s h 
  }}.

Definition hmFree'_specif2 := forall adr sizex x entry cptr nptr result status,  
  (var.set (hmStart::entry::cptr::nptr::result::nil)) -> 
  adr > 0 -> sizex > 0 ->

  {{fun s => fun h => exists l1,  Heap_List l1 adr 0 s h /\ 
      In (x,sizex,status) l1 /\ 
      eval (var_e hmStart) s = eval (nat_e adr) s }}
  
  proj_cmd (hmFree' (x+2) entry cptr nptr result)
  
(* a modifier: trop dependant de l'implem *)

  {{ fun s => fun h => exists l2,  Heap_List l2 adr 0 s h /\ 
       In (x,sizex,Free) l2 
  }}.

Lemma hmFree'_verif1 : hmFree'_specif1.

unfold hmFree'_specif1.
unfold hmFree'.
do 10 intro.
intro lx_length.
intros.
simpl.

apply semax_assign_var_e'' with (fun s => fun h => exists l1,  Heap_List l1 adr 0 s h /\ 
      In (x,sizex,status) l1 /\ (ArrayI (x+2) lx ** TT) s h /\ x<>y /\
      eval (var_e hmStart) s = eval (nat_e adr) s /\ 
      eval (var_e entry) s = eval (nat_e adr) s
).
red.
intros.
inversion_clear H2 as [l].
decompose [and] H3; clear H3.
red.
exists l.
split.
Resolve_simpl1.
split; auto.
split.
Resolve_simpl1.
split; auto.
split.
simpl.
Resolve_simpl1.
simpl.
Resolve_simpl1.

apply semax_assign_var_e'' with (fun s => fun h => exists l1,  Heap_List l1 adr 0 s h /\ 
      In (x,sizex,status) l1 /\ (ArrayI (x+2) lx ** TT) s h /\ x<>y /\
      eval (var_e hmStart) s = eval (nat_e adr) s /\ 
      eval (var_e entry) s = eval (nat_e adr) s /\
      eval (var_e cptr) s =eval (nat_e y)  s
).
red.
intros.
inversion_clear H2 as [l].
decompose [and] H3; clear H3.
red.
exists l.
split.
Resolve_simpl1.
split; auto.
split.
Resolve_simpl1.
split; auto.
split.
simpl.
rewrite <- store.lookup_update; auto; Resolve_var_neq.
split.
simpl.
rewrite <- store.lookup_update; auto; Resolve_var_neq.
simpl.
Resolve_simpl1.
Presb_Z.

apply semax_while'' with (fun s => fun h => exists l1,  Heap_List l1 adr 0 s h /\ 
      In (x,sizex,status) l1 /\ (ArrayI (x+2) lx ** TT) s h /\ x<>y /\
      eval (var_e hmStart) s = eval (nat_e adr) s /\ 
      (exists bloc_adr,  eval (var_e entry) s =eval (nat_e (bloc_adr))  s /\

         (
          (* either entry is the null pointer (we haven't been able to find the bloc) *)
          (bloc_adr = 0) \/
          (* or it's the last one (previously hmFree vulnerability) *)
          (bloc_adr > 0 /\ ((Heap_List l1 adr bloc_adr) ** (Heap_List nil bloc_adr 0)) s h) \/
          (* or it's a bloc *)
          (bloc_adr > 0 /\ exists bloc_size, exists bloc_type, In (bloc_adr, bloc_size, bloc_type) l1)
         )
     ) /\
      eval (var_e cptr) s =eval (nat_e y)  s
).
red.

(* just to see if invariant seem correct *)
simpl.
intros.
inversion_clear H2 as [l].
decompose [and] H3; clear H3.
exists l.
split; auto.
split; auto.
split; auto.
split; auto.
split; auto.
split.
exists adr.
split; auto.
right; right.
split; auto.
inversion H2.
subst l.
simpl in H5; contradiction.
inversion H3.
subst startl endl s0 h0.
subst adr.
exists hd_size.
exists hd_expr.
intuition.
auto.

apply semax_assign_var_lookup_backwards'' with (fun s => fun h => exists l1,  Heap_List l1 adr 0 s h /\ 
      In (x,sizex,status) l1 /\ (ArrayI (x+2) lx ** TT) s h /\ x<>y /\
      eval (var_e hmStart) s = eval (nat_e adr) s /\ 
      eval (var_e cptr) s =eval (nat_e y)  s /\
      (exists bloc_adr,  eval (var_e entry) s =eval (nat_e (bloc_adr))  s /\
       bloc_adr <> y /\ 
         (
          (* or it's the last one (previously hmFree vulnerability) *)
          (bloc_adr > 0 /\ ((Heap_List l1 adr bloc_adr) ** (Heap_List nil bloc_adr 0)) s h /\
           eval (var_e nptr) s = eval null s) \/
          (* or it's a bloc *)
          (bloc_adr > 0 /\ exists bloc_size, exists bloc_type, In (bloc_adr, bloc_size, bloc_type) l1 /\
           eval (var_e nptr) s = eval (nat_e (bloc_adr + 2 + bloc_size)) s)
         )
     )
).
red.
simpl.
intros.
inversion_clear H2.
generalize (andb_prop _ _ H4); intro X; clear H4; inversion_clear X.
generalize (negb_true_is_false _ H2); intro; clear H2.
generalize (negb_true_is_false _ H4); intro; clear H4.
unfold eqb in H5; unfold eqb in H2.
generalize (Zeq_bool_false (store.lookup entry s) 0); intro X; inversion_clear X.
generalize (H4 H5); clear H5 H4 H6; intro.
generalize (Zeq_bool_false (store.lookup entry s) (store.lookup cptr s)); intro X; inversion_clear X.
generalize (H5 H2); clear H2 H5 H6; intro.
inversion_clear H3 as [l].
decompose [and] H5; clear H5.
inversion_clear H10.
decompose [and] H5; clear H5.
rewrite H10 in H4; rewrite H10 in H2; rewrite H12 in H2.
inversion_clear H11.
subst x0.
tauto.
inversion_clear H5.
decompose [and] H11; clear H11.
Decompose_sepcon H13 h1 h2.
inversion_clear H16.
clear H15 H18.
simpl in H19.
Decompose_sepcon H19 h21 h22.
Decompose_sepcon H20 h221 h222.
red in H23.
subst next.
exists (nat_e 0).
Compose_sepcon h221 (heap.union h21 h1).
eapply mapsto_equiv.
apply H20.
simpl.
rewrite H10; unfold next.
trivial.
trivial.
Intro_sepimp h'221 h'.
red.
exists l.
assert (heap.equal h'221 h221).
eapply singleton_equal.
apply H22.
apply H20.
simpl.
rewrite H10; unfold next.
trivial.
trivial.
assert (heap.equal h h').
Equal_heap.
split.
eapply Heap_List_heap_equal.
apply heap.equal_sym.
apply H26.
Resolve_simpl1.
split; auto.
split.
eapply ArrayITT_heap_cong.
apply H26.
Resolve_simpl1.
clear H26.
split; auto.
split.
Resolve_simpl1.
split.
Resolve_simpl1.
exists x0.
split.
Resolve_simpl1.
split; auto.
left.
split; auto.
split.
assert ((Heap_List l adr x0 ** Heap_List nil x0 0) s h').
Compose_sepcon h1 (heap.union h21 h'221).
auto.
eapply Heap_List_last.
auto.
intuition.
auto.
simpl.
Compose_sepcon h21 h'221.
auto.
Compose_sepcon h'221 heap.emp.
eapply mapsto_equiv.
apply H22.
simpl.
rewrite H10.
unfold next.
trivial.
trivial.
red; apply heap.equal_refl.
Resolve_simpl1.
Resolve_simpl1.
inversion H15.
inversion_clear H11.
inversion_clear H13.
inversion_clear H11.
exists (nat_e (x0 + 2 + x1)).
eapply Heap_List_var_lookup_next.
apply H3.
apply H13.
auto.
red.
exists l.
split.
Resolve_simpl1.
split; auto.
split.
Resolve_simpl1.
split; auto.
split.
Resolve_simpl1.
split.
Resolve_simpl1.
exists x0.
split.
Resolve_simpl1.
split; auto.
right.
split; auto.
exists x1.
exists x2.
split; auto.
Resolve_simpl1.

intros.
inversion_clear H14.
decompose [and] H15; clear H15.
exists x3.
split.
eapply Heap_List_heap_equal.
apply heap.equal_sym.
apply H11.
auto.
split; auto.
split.
eapply ArrayITT_heap_cong.
apply H11.
Resolve_simpl1.
split; auto.
split; auto.
split; auto.
inversion_clear H22.
inversion_clear H15.
inversion_clear H22.
exists x4.
split; auto.
split; auto.
inversion_clear H23.
inversion_clear H22.
inversion_clear H24.
left.
split; auto.
split.
Decompose_sepcon H22 h01 h02.
exists h01; exists h02.
split.
Disjoint_heap.
split.
apply heap.equal_trans with h0.
Equal_heap.
Equal_heap.
auto.
auto.
auto.

apply semax_assign_var_e'.
red.
simpl.
intros.
inversion_clear H2 as [l].
decompose [and] H3; clear H3.
inversion_clear H10.
decompose [and] H3; clear H3.
inversion_clear H12.
decompose [and] H3; clear H3.
red.
exists l.
split.
Resolve_simpl1.
split; auto.
split.
Resolve_simpl1.
split; auto.
split.
Resolve_simpl1.
split.
exists 0.
split.
Resolve_simpl1.
left; auto.
Resolve_simpl1.
inversion_clear H3.
inversion_clear H12.
inversion_clear H3.
inversion_clear H12.
red.
exists l.
split.
Resolve_simpl1.
split; auto.
split.
Resolve_simpl1.
split; auto.
split.
Resolve_simpl1.
split.
exists (x0 + 2 + x1).
split.
Resolve_simpl1.
right.
generalize (list_split' l x0 x1 x2 H3); intro.
inversion_clear H12 as [l1].
inversion_clear H14 as [l2].
rewrite H12 in H2.
generalize (Heap_List_split' l1 (((x0, x1, x2) :: nil) ++ l2) adr s h H0); intro X; inversion_clear X.
generalize (H14 H2); clear H2 H14 H15; intro X; inversion_clear X.
Decompose_sepcon H2 h1 h2.
induction l2.
simpl in H17.
inversion_clear H17.
subst x3; clear H22.
subst next.
left.
split.
omega.
Compose_sepcon (heap.union h1 h3) h4.
rewrite H12.
simpl.
eapply Heap_List_inde_store with s.
assert ((x0 + 2 + x1) > 0).
omega.
generalize (Heap_List_split l1 ((x0,x1,x2)::nil) adr  (x0 + 2 + x1) s (heap.union h1 h3) H0 H17); intro X; inversion_clear X. 
apply H21.
clear H20 H21. 
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.
Resolve_simpl1.
clear IHl2.
induction a.
induction a.
right.
simpl in H17.
inversion_clear H17.
subst x3.
subst next.
inversion_clear H24.
subst a.
split; auto.
exists b0; exists b.
rewrite H12.
apply in_or_app.
right.
apply in_or_app.
right.
auto with *.
Resolve_simpl1.

apply semax_ifte.

apply semax_assign_var_lookup_backwards'' with (fun s => fun h => exists l1 : list (loc * nat * expr),
         Heap_List l1 adr 0 s h /\
         In (x, sizex, status) l1 /\
         (ArrayI (x+2) lx ** TT) s h /\
         x <> y /\
         eval (var_e hmStart) s = eval (nat_e adr) s /\
         eval (var_e cptr) s = eval (nat_e y) s /\
         eval (var_e entry) s = eval (nat_e y) s /\

            ((y > 0 /\
             (Heap_List l1 adr y ** Heap_List nil y 0) s h /\
              eval (var_e nptr) s = eval null s
             ) \/
             (y > 0 /\
             (exists bloc_size : nat,
                (exists bloc_type : expr,
                   In (y, bloc_size, bloc_type) l1 /\
                   eval (var_e nptr) s = eval (nat_e (y + 2 + bloc_size)) s))))

).
red.
simpl.
intros.
inversion_clear H2.
inversion_clear H3.
generalize (negb_true_is_false _ H4); intro; clear H4.
unfold eqb in H5; unfold eqb in H3.
generalize (Zeq_bool_false (store.lookup entry s) 0); intro X; inversion_clear X.
generalize (H4 H3); clear H3 H4 H6; intro.
generalize (andb_false_elim _ _ H5); intro X; inversion_clear X.
generalize (negb_false_is_true _ H4); intro; clear H4.
rewrite (Zeq_bool_true _ _ H6) in H3.
tauto.
clear H5.
generalize (negb_false_is_true _ H4); intro; clear H4.
generalize (Zeq_bool_true _ _ H5); intros.
clear H5.
inversion_clear H2 as [l].
decompose [and] H5; clear H5.
inversion_clear H10.
decompose [and] H5; clear H5.
inversion_clear H11.
subst x0.
tauto.
inversion_clear H5.
inversion_clear H11.
Decompose_sepcon H13 h1 h2.
inversion_clear H16.
clear H18 H15.
subst next.
simpl in H19.
Decompose_sepcon H19 h21 h22.
Decompose_sepcon H19 h221 h222.
red in H22.
exists (nat_e 0).
Compose_sepcon h221 (heap.union h1 h21).
eapply mapsto_equiv.
apply H19.
simpl.
unfold next.
rewrite H10.
trivial.
trivial.
Intro_sepimp h'221 h'.
assert (heap.equal h221 h'221).
eapply singleton_equal.
apply H19.
apply H23.
simpl.
rewrite H10; unfold next; auto.
auto.
red.
assert (heap.equal h' h).
Equal_heap.
rewrite H12 in H4; rewrite H10 in H4.
rewrite <- H4.
generalize (Z_of_nat_inj _ _ H4); intros.
subst x0.
clear H4.
exists l.
split.
eapply Heap_List_heap_equal.
apply H26.
Resolve_simpl1.
split; auto.
split.
eapply ArrayITT_heap_cong.
apply heap.equal_sym.
apply H26.
Resolve_simpl1.
split; auto.
split.
Resolve_simpl1.
split.
Resolve_simpl1.
split.
Resolve_simpl1.
left.
split; auto.
split.
Compose_sepcon h1 (heap.union h21 h'221).
Resolve_simpl1.
eapply Heap_List_inde_store with s.
eapply Heap_List_last.
auto.
intuition.
auto.
simpl.
Compose_sepcon h21 h'221.
auto.
Compose_sepcon h'221 heap.emp.
eapply mapsto_equiv.
apply H23.
simpl.
rewrite H10; unfold next; auto.
auto.
red; apply heap.equal_refl.
Resolve_simpl1.
inversion H15.
inversion_clear H11.
inversion_clear H13.
inversion_clear H11.
exists (nat_e (x0 + 2 + x1)).
eapply Heap_List_var_lookup_next.
apply H2.
apply H13.
auto.
red.
rewrite H12 in H4; rewrite H10 in H4.
generalize (Z_of_nat_inj _ _ H4); intros.
subst x0.
clear H4.
exists l.
split.
Resolve_simpl1.
split; auto.
split.
Resolve_simpl1.
split; auto.
split.
Resolve_simpl1.
split.
Resolve_simpl1.
split.
Resolve_simpl1.
right.
split; auto.
exists x1.
exists x2.
split; auto.
Resolve_simpl1.

intros.
inversion_clear H14.
decompose [and] H15; clear H15.
exists x3.
split.
eapply Heap_List_heap_equal.
apply heap.equal_sym.
apply H11.
auto.
split; auto.
split.
eapply ArrayITT_heap_cong.
apply H11.
auto.
split; auto.
split; auto.
split; auto.
split; auto.
inversion_clear H23.
inversion_clear H15.
inversion_clear H23.
left.
split; auto.
split.
Decompose_sepcon H15 h01 h02.
exists h01; exists h02.
split.
Disjoint_heap.
split.
apply heap.equal_trans with h0.
Equal_heap.
Equal_heap.
auto.
auto.
auto.

apply semax_ifte.

apply semax_assign_lookup_expr_backwards'' with (fun s => fun h => exists l1 : list (loc * nat * expr),
         Heap_List l1 adr 0 s h /\
         In (x, sizex, status) l1 /\
         (ArrayI (x+2) lx ** TT) s h /\
         x <> y /\
         eval (var_e hmStart) s = eval (nat_e adr) s /\
         eval (var_e cptr) s = eval (nat_e y) s /\
         eval (var_e entry) s = eval (nat_e y) s /\
         y > 0 /\
         (exists bloc_size : nat,
                (exists bloc_type : expr,
                   In (y, bloc_size, bloc_type) l1 /\
                   eval (var_e nptr) s = eval (nat_e (y + 2 + bloc_size)) s))

).
red.
simpl.
intros.
inversion_clear H2.
generalize (negb_true_is_false _ H4); intro; clear H4.
unfold eqb in H2.
generalize (Zeq_bool_false (store.lookup nptr s) 0); intro X; inversion_clear X.
generalize (H4 H2); intro; clear H2 H4 H5.
inversion_clear H3 as [l].
decompose [and] H2; clear H2.
inversion_clear H12.
decompose [and] H2; clear H2.
tauto.
inversion_clear H2.
inversion_clear H12.
inversion_clear H2.
inversion_clear H12.
generalize (list_split' l y x0 x1 H2); intro.
inversion_clear H12 as [l1].
inversion_clear H14 as [l2].
rewrite H12 in H2.
rewrite H12 in H5.
rewrite H12 in H3.
exists x1.

generalize (Change_Status_Free' l1 l2 y x0 adr s h entry x1 H0 H3); intros.
simpl in H14.
generalize (H14 H10); clear H14; intros.
Decompose_sepcon H14 h1 h2.
Compose_sepcon h1 h2.
auto.
Intro_sepimp h'1 h'.
red in H18.
assert (h2 # h'1 /\ (entry -.> topsy_hm.status |-> Free) s h'1).
auto.
generalize (H18 h'1 H21 h' H20); clear H18 H21; intros.
exists (l1 ++ (y, x0, Free) :: l2).
split.
auto.
split.
generalize (in_app_or _ _ _ H5); intros.
inversion_clear H21.
apply in_or_app.
left; auto.
simpl in H22.
inversion_clear H22.
inversion H21.
subst x.
intuition.
apply in_or_app.
right.
simpl; right; auto.
split.
eapply Data_destructive_update_inv.
intuition.
apply H4.
apply H14.
auto.
apply H15.
apply H19.
Disjoint_heap.
Equal_heap.

simpl.
unfold topsy_hm.status.
rewrite H10.
simpl.

generalize (in_app_or _ _ _ H5); intro X; inversion_clear X.
generalize (Heap_List_block_block_pos l1 ((y, x0, Free) :: l2) adr s h' x sizex status y x0 Free H0 H18 H21); intro.
simpl in H22.
intuition.
right.
rewrite lx_length.
assert (Z_of_nat y + 0 = Z_of_nat y)%Z.
intuition.
rewrite H23.
assert (forall x y, x >= y -> (Z_of_nat x >= Z_of_nat y)%Z).
intuition.
apply (H25 y (x + 2 + sizex)).
omega.
simpl in H21.
inversion_clear H21.
injection H22; intros.
subst y.
intuition.
assert (In (y, x0, Free) (l1 ++ (y, x0, Free) :: nil)).
apply in_or_app.
right.
intuition.
generalize (Heap_List_block_block_pos  (l1 ++ ((y, x0, Free)::nil)) l2 adr s h' y x0 Free x sizex status  H0); intro.
rewrite app_ass in H23.
simpl in H23.
intuition.
left.
assert (forall x y, x < y -> (Z_of_nat x < Z_of_nat y)%Z).
intuition.
assert (Z_of_nat y + 0 = Z_of_nat y)%Z.
intuition.
rewrite H25.
apply H23.
omega.

split; auto.
split; auto.
split; auto.
split; auto.
split; auto.
exists x0; exists Free.
split.
apply in_or_app.
right.
simpl; left; auto.
auto.

apply semax_assign_var_e'.
red.
simpl.
intuition.
red.
inversion_clear H2 as [l].
decompose [and] H3; clear H3.
exists l.
split.
Resolve_simpl1.
split; auto.
Resolve_simpl1.

apply semax_assign_var_e'.
red.
simpl.
intuition.
red.
inversion_clear H3 as [l].
decompose [and] H2; clear H2.
exists l.
split.
Resolve_simpl1.
split; auto.
Resolve_simpl1.

apply semax_assign_var_e'.
red.
simpl.
intros.
decompose [and] H2;  clear H2.
generalize (negb_false_is_true _ H4); intro; clear H4.
unfold eqb in H6; unfold eqb in H2.
generalize (Zeq_bool_true _ _ H2); intro; clear H2.
inversion_clear H5 as [l].
decompose [and] H2; clear H2.
inversion_clear H10.
inversion_clear H2.
clear H6.
rewrite H10 in H3.
assert (x0 = 0).
assert (0%Z = Z_of_nat 0).
trivial.
rewrite H2 in H3.
generalize (Z_of_nat_inj _ _ H3); intro.
trivial.
subst x0.
inversion_clear H11.
red.
exists l.
split.
Resolve_simpl1.
split; auto.
Resolve_simpl1.
inversion_clear H2.
inversion_clear H6.
inversion H2.
inversion_clear H6.
inversion H2.
Qed.


Lemma hmFree'_verif2 : hmFree'_specif2.

unfold hmFree'_specif2.
unfold hmFree'.
intros.
simpl.

apply semax_assign_var_e'' with (fun s => fun h => exists l1,  Heap_List l1 adr 0 s h /\ 
      In (x,sizex,status) l1 /\
      eval (var_e hmStart) s = eval (nat_e adr) s /\ 
      eval (var_e entry) s = eval (nat_e adr) s
).
red.
intros.
inversion_clear H2 as [l].
decompose [and] H3; clear H3.
red.
exists l.
split.
Resolve_simpl1.
split; auto.
split; auto.
simpl.
Resolve_simpl1.
simpl.
Resolve_simpl1.

apply semax_assign_var_e'' with (fun s => fun h => exists l1,  Heap_List l1 adr 0 s h /\ 
      In (x,sizex,status) l1 /\
      eval (var_e hmStart) s = eval (nat_e adr) s /\ 
      eval (var_e entry) s = eval (nat_e adr) s /\
      eval (var_e cptr) s =eval (nat_e x)  s
).
red.
intros.
inversion_clear H2 as [l].
decompose [and] H3; clear H3.
red.
exists l.
split.
Resolve_simpl1.
split; auto.
split; auto.
simpl.
rewrite <- store.lookup_update; auto; Resolve_var_neq.
split.
simpl.
rewrite <- store.lookup_update; auto; Resolve_var_neq.
simpl.
Resolve_simpl1.
Presb_Z.

apply semax_while'' with (fun s h => exists l, Heap_List l adr 0 s h /\ 
      In (x,sizex,status) l /\
      eval (var_e hmStart) s = eval (nat_e adr) s /\ 
      eval (var_e cptr) s = eval (nat_e x)  s /\
      (exists bloc_adr, eval (var_e entry) s =eval (nat_e (bloc_adr))  s /\
         bloc_adr > 0 /\ 
         ( exists bloc_size, exists bloc_type,
           ((bloc_adr, bloc_size, bloc_type) = (x,sizex,status))
           \/
           (exists l1, exists l2, 
            (l = l1 ++ ((bloc_adr, bloc_size, bloc_type)::nil) ++ l2 /\ In (x,sizex,status) l2))         
        )       
    )  
).
red.
simpl.
intros.
inversion_clear H2 as [l].
decompose [and] H3; clear H3.
exists l.
intuition.
inversion H2.
subst l.
simpl in H5; inversion H5.
inversion H3.
subst startl endl s0 h0.
subst hd_adr.
subst next.
exists adr.
split; auto.
split; auto.
rewrite <- H15 in H5.
exists hd_size; exists hd_expr.
simpl in H5; inversion_clear H5.
left; auto.
right.
exists (@nil (loc * nat * expr)); exists tl.
simpl.
split; auto.


apply semax_strengthen_pre with (fun s h => exists l, Heap_List l adr 0 s h /\ 
      In (x,sizex,status) l /\
      eval (var_e hmStart) s = eval (nat_e adr) s /\ 
      eval (var_e cptr) s = eval (nat_e x)  s /\
      (exists bloc_adr, eval (var_e entry) s = eval (nat_e (bloc_adr))  s /\
         bloc_adr > 0 /\ 
         (exists bloc_size, exists bloc_type,
           (exists l1, exists l2, 
            (l = l1 ++ ((bloc_adr, bloc_size, bloc_type)::nil) ++ l2 /\ In (x,sizex,status) l2))
        )       
    )  
).
red.
simpl.
intros.
inversion_clear H2.
generalize (andb_prop _ _ H4); clear H4; intro X; inversion_clear X.
generalize (negb_true_is_false _ H4); clear H4; intro.
unfold eqb in H2; unfold eqb in H4.
generalize (Zeq_bool_false (store.lookup entry s) (store.lookup cptr s)); intro X; inversion_clear X.
generalize (H5 H4); clear H4 H5 H6; intro.
clear H2.
inversion_clear H3 as [l].
decompose [and] H2; clear H2.
inversion_clear H9.
decompose [and] H2; clear H2.
inversion_clear H11.
inversion_clear H2.
inversion_clear H9.
injection H2; intros; subst x0 x1 x2.
rewrite H7 in H4; rewrite H8 in H4.
tauto.
exists l.
intuition.
exists x0.
intuition.
exists x1.
exists x2.
trivial.

apply semax_assign_var_lookup_backwards'' with (fun s => fun h => exists l,  Heap_List l adr 0 s h /\ 
      In (x,sizex,status) l /\
      eval (var_e hmStart) s = eval (nat_e adr) s /\ 
      eval (var_e cptr) s =eval (nat_e x)  s /\
      (exists bloc_adr,  eval (var_e entry) s =eval (nat_e (bloc_adr))  s /\
         bloc_adr > 0 /\ 
         ( exists bloc_size, exists bloc_type, eval (var_e nptr) s = Z_of_nat (bloc_adr + 2 + bloc_size) /\
           (exists l1, exists l2, 
            (l = l1 ++ ((bloc_adr, bloc_size, bloc_type)::nil) ++ l2 /\ In (x,sizex,status) l2))         
        )       
    )  
).
red.
simpl.
intros.
inversion_clear H2 as [l].
decompose [and] H3; clear H3.
inversion_clear H8.
decompose [and] H3; clear H3.
inversion_clear H10.
inversion_clear H3.
inversion_clear H8 as [l1].
inversion_clear H3 as [l2].
inversion_clear H8.
exists (nat_e (x0 + 2 + x1)).
eapply Heap_List_var_lookup_next.
apply H2.
rewrite H3.
apply in_or_app.
right.
simpl.
left.
intuition.
auto.
red.
exists l.
split.
Resolve_simpl1.
split; auto.
split.
Resolve_simpl1.
split.
Resolve_simpl1.
exists x0.
split.
Resolve_simpl1.
split; auto.
exists x1; exists x2.
split.
Resolve_simpl1.
exists l1; exists l2.
auto.

intros.
inversion_clear H11.
decompose [and] H12; clear H12.
exists x3.
split.
eapply Heap_List_heap_equal.
apply heap.equal_sym.
apply H8.
auto.
auto.

apply semax_assign_var_e'.
simpl.
red.
simpl.
intros.
inversion_clear H2 as [l].
decompose [and] H3; clear H3.
inversion_clear H8.
decompose [and] H3; clear H3.
inversion_clear H10.
inversion_clear H3.
inversion_clear H8.
inversion_clear H10 as [l1].
inversion_clear H8 as [l2].
inversion_clear H10.
induction l2.
simpl in H11.
contradiction.
clear IHl2.
exists l.
split.
Resolve_simpl1.
split; auto.
split.
Resolve_simpl1.
split.
Resolve_simpl1.
induction a.
induction a.
exists (x0 + 2 + x1).
split.
Resolve_simpl1.
split.
omega.
exists b0; exists b.
simpl in H11.
inversion_clear H11.
injection H10.
intros.
subst b b0 a.
left; auto.
rewrite H8 in H2.
generalize (Heap_List_split' l1 ((x0, x1, x2) :: (x, sizex, status) :: l2) adr s h H0); intro X; inversion_clear X.
generalize (H11 H2); clear H2 H11 H12; intro.
inversion_clear H2.
Decompose_sepcon H11 h1 h2.
inversion_clear H14.
subst x3.
subst next.
inversion_clear H21.
subst x.
auto.
right.
exists (l1 ++ (x0,x1,x2) :: nil).
exists l2.
split.
rewrite H8.
rewrite H8 in H2.
generalize (Heap_List_split' l1 ((x0, x1, x2) :: (a, b0, b) :: l2) adr s h H0); intro X; inversion_clear X.
generalize (H11 H2); clear H2 H11 H12; intro.
inversion_clear H2.
Decompose_sepcon H11 h1 h2.
inversion_clear H14.
subst x3.
subst next.
inversion_clear H21.
subst a.
rewrite <- ass_app.
simpl.
auto.
auto.

apply semax_strengthen_pre with (fun s => fun h => exists l,  Heap_List l adr 0 s h /\ 
      In (x,sizex,status) l /\
      eval (var_e hmStart) s = eval (nat_e adr) s /\ 
      eval (var_e cptr) s =eval (nat_e x)  s /\
      eval (var_e entry) s = eval (nat_e x) s 
).
red.
simpl.
intros.
inversion_clear H2.
inversion_clear H3 as [l].
decompose [and] H2; clear H2.
inversion_clear H9.
decompose [and] H2; clear H2.
inversion_clear H11.
inversion_clear H2.
generalize (andb_false_elim _ _ H4); intro.
inversion_clear H2.
generalize (negb_false_is_true _ H11); clear H11; intro.
unfold eqb in H2.
rewrite (Zeq_bool_true _ _ H2) in H8.
assert (0%Z = Z_of_nat 0)%Z.
trivial.
rewrite H11 in H8; clear H11.
rewrite <- (Z_of_nat_inj _ _ H8) in H10; inversion H10.
generalize (negb_false_is_true _ H11); clear H11; intro.
unfold eqb in H2.
generalize (Zeq_bool_true _ _ H2); clear H2; intro.
rewrite H7 in H2; rewrite H8 in H2.
generalize (Z_of_nat_inj _ _ H2); intro X; subst x0; clear H2 H4.
exists l.
split; auto.

apply semax_ifte.

apply semax_assign_var_lookup_backwards'' with (fun s => fun h => exists l,  Heap_List l adr 0 s h /\ 
      In (x,sizex,status) l /\
      eval (var_e hmStart) s = eval (nat_e adr) s /\ 
      eval (var_e cptr) s =eval (nat_e x)  s /\
      eval (var_e entry) s = eval (nat_e x) s /\
      eval (var_e nptr) s = Z_of_nat (x + 2 + sizex)).
red.
simpl.
intros.
inversion_clear H2.
clear H4.
inversion_clear H3 as [l].
decompose [and] H2; clear H2.
exists (nat_e (x + 2 + sizex)).
eapply Heap_List_var_lookup_next.
apply H3.
apply H5.
auto.
red.
exists l.
split.
Resolve_simpl1.
split; auto.
split.
Resolve_simpl1.
split.
Resolve_simpl1.
split.
Resolve_simpl1.
Resolve_simpl1.

intros.
inversion_clear H7.
decompose [and] H9; clear H9.
exists x0.
split.
eapply Heap_List_heap_equal.
apply heap.equal_sym.
apply H2.
auto.
split; auto.

apply semax_ifte.

apply semax_assign_lookup_expr_backwards'' with (fun s => fun h => exists l,  Heap_List l adr 0 s h /\ 
      In (x,sizex,Free) l /\
      eval (var_e hmStart) s = eval (nat_e adr) s /\ 
      eval (var_e cptr) s =eval (nat_e x)  s /\
      eval (var_e entry) s = eval (nat_e x) s /\
      eval (var_e nptr) s = Z_of_nat (x + 2 + sizex)).
red.
simpl.
intros.
inversion_clear H2.
clear H4.
inversion_clear H3 as [l].
decompose [and] H2; clear H2.
exists status.
generalize (list_split' l x sizex status H5).
intros.
inversion_clear H2 as [l1].
inversion_clear H8 as [l2].
subst l.
generalize (Change_Status_Free' l1 l2 x sizex adr s h entry status H0 H3); intro X.
simpl in X.
generalize (X H7); clear X; intros.
Decompose_sepcon H2 h1 h2.
Compose_sepcon h1 h2.
auto.
Intro_sepimp h1' h'.
exists (l1 ++ (x, sizex, Free) :: l2).
split.
red in H12.
assert (heap.disjoint h2 h1' /\ (entry -.> topsy_hm.status |-> Free) s h1').
intuition.
apply (H12 h1' H15 h' H14).
intuition.

apply semax_assign_var_e'.
red.
simpl; intros.
inversion_clear H2 as [l].
decompose [and] H3; clear H3.
red.
exists l.
intuition.
Resolve_simpl1.

apply semax_assign_var_e'.
red.
simpl.
intros.
inversion_clear H2.
inversion_clear H3 as [l].
decompose [and] H2; clear H2.
generalize (negb_false_is_true _ H4); clear H4; intro.
unfold eqb in H2.
rewrite (Zeq_bool_true _ _ H2) in H10.
assert (0 = Z_of_nat 0)%Z.
trivial.
rewrite H4 in H10.
generalize (Z_of_nat_inj _ _ H10).
intuition.
assert (0 = x + 2 + sizex -> False).
omega.
contradiction.


apply semax_assign_var_e'.
red.
simpl.
intros.
inversion_clear H2.
inversion_clear H3 as [l].
decompose [and] H2; clear H2.
generalize (negb_false_is_true _ H4); clear H4; intro.
unfold eqb in H2.
rewrite (Zeq_bool_true _ _ H2) in H9.
assert (0 = Z_of_nat 0)%Z.
trivial.
rewrite H4 in H9.
rewrite <- (Z_of_nat_inj _ _ H9) in H6.
generalize (list_split' l 0 sizex status H6); intro.
inversion_clear H8.
inversion_clear H10.
rewrite H8 in H3.
generalize (Heap_List_split' x0 (((0, sizex, status) :: nil) ++ x1) adr s h H0); intro X; inversion_clear X.
generalize (H10 H3); clear H3 H10 H11.
intros.
inversion_clear H3.
Decompose_sepcon H10 h1 h2.
inversion_clear H13.
subst x2; inversion H18.
Qed.