Require Export Memory. Require Export Memory_hypotheses. (* First-fit allocator *) Load param. Section Alloc. Variable reqsize : int. Variable m : mem. Variable initial_freelist : list (block * int). Record find_free_block_found_block : Set := make_find_free_block_found_block { find_free_block_found_block_block : block; find_free_block_found_block_offset : int; find_free_block_found_block_size : int }. Record find_free_block_body_param : Set := make_find_free_block_body_param { find_free_block_freelist_block : block; find_free_block_freelist_offset : int; find_free_block_result : option find_free_block_found_block }. Section Find_free_block. Definition find_free_block_body p0 := match p0 with | Some p => match load Mint32 m (find_free_block_freelist_block p) (signed (find_free_block_freelist_offset p)) with | Some (Vint i) => (negb (eq i zero), None) | Some (Vptr b i) => match load Mint32 m b (signed (sub i four)) with | Some (Vint v) => if cmp Cle reqsize (v) then (false, Some (make_find_free_block_body_param (find_free_block_freelist_block p) (find_free_block_freelist_offset p) (Some (make_find_free_block_found_block b i (v))) )) else (true, Some (make_find_free_block_body_param b i (find_free_block_result p) )) | _ => (true, None) end | _ => (true, None) end | _ => (true, None) end. Variable whatever_happens_on_freelist_head : block -> int -> Prop. Record find_free_block_body_further_param : Set := make_find_free_block_body_further_param { find_free_block_freelist : list (block * int); find_free_block_before_freelist : list (block * int) }. Record find_free_block_body_invariants (p : find_free_block_body_param) (q : find_free_block_body_further_param) : Prop := find_free_block_body_invariants_intro { find_free_block_freelist_hyp : chain m (find_free_block_freelist_block p) (find_free_block_freelist_offset p) (find_free_block_freelist q); (* needed for termination *) find_free_block_freelist_block_header : forall b i, member (b, i) (find_free_block_freelist q) -> exists vi, Some (Vint vi) = load Mint32 m b (signed (sub i four)); (* needed for history *) find_free_block_before_freelist_hyp : initial_freelist = find_free_block_before_freelist q ++ find_free_block_freelist q; find_free_block_freelist_mem : whatever_happens_on_freelist_head (find_free_block_freelist_block p) (find_free_block_freelist_offset p) \/ member (find_free_block_freelist_block p, find_free_block_freelist_offset p) (find_free_block_before_freelist q) }. Lemma find_free_block_body_invariants_false : forall l q, find_free_block_freelist q = l -> forall p, find_free_block_body_invariants p q -> forall p', (false, Some p') = find_free_block_body (Some p) -> find_free_block_body_invariants p' q /\ exists r, Some r = find_free_block_result p' /\ exists l', l = (find_free_block_found_block_block r, find_free_block_found_block_offset r) :: l' /\ Some (Vint (find_free_block_found_block_size r)) = load Mint32 m (find_free_block_found_block_block r) (signed (sub (find_free_block_found_block_offset r) four)). Proof. (* induction l. *) destruct l as [ | r0 l'0]. intros q Hq p Hp p' Hp'. inversion Hp. rewrite Hq in *. inversion find_free_block_freelist_hyp0. subst b i. generalize Hp'. unfold find_free_block_body. rewrite <- H. discriminate 1. intros q Hq p Hp p' Hp'. inversion Hp. rewrite Hq in *. inversion find_free_block_freelist_hyp0. subst b i r0 l. generalize Hp'. unfold find_free_block_body. rewrite <- H3. case_eq (load Mint32 m b' (signed (sub i' four))); try (intros; discriminate). destruct v; try (intros; discriminate). intros Hi. case_eq (cmp Cle reqsize ( i)); try (intros; discriminate). injection 2; intros; subst p'. rewrite <- Hq in *. split. apply find_free_block_body_invariants_intro; simpl. eauto. assumption. eauto. simpl. assumption. exists (make_find_free_block_found_block b' i' i). split. simpl; trivial. exists l'0. eauto. Qed. Lemma find_free_block_body_invariants_true : forall l q, find_free_block_freelist q = l -> forall p, find_free_block_body_invariants p q -> forall p', (true, Some p') = find_free_block_body (Some p) -> exists l', l = (find_free_block_freelist_block p', find_free_block_freelist_offset p') :: l' /\ find_free_block_body_invariants p' (make_find_free_block_body_further_param l' (find_free_block_before_freelist q ++ (find_free_block_freelist_block p', find_free_block_freelist_offset p') :: nil)). Proof. destruct l as [|r0 l'0]. intros q Hq p Hp p' Hp'. inversion Hp. rewrite Hq in *. inversion find_free_block_freelist_hyp0. subst b i. generalize Hp'. unfold find_free_block_body. rewrite <- H. discriminate 1. intros q Hq p Hp p' Hp'. inversion Hp. rewrite Hq in *. inversion find_free_block_freelist_hyp0. subst b i l'0 r0. generalize Hp'. unfold find_free_block_body. rewrite <- H3. case_eq (load Mint32 m b' (signed (sub i' four))); try (intros; discriminate). destruct v; try (intros; discriminate). intros Hi. case_eq (cmp Cle reqsize i); try (intros; discriminate). injection 2; intros; subst p'. simpl. exists l. split. trivial. apply find_free_block_body_invariants_intro; simpl. assumption. intros; eauto. rewrite app_ass. simpl. auto. right. apply member_app_right. auto. Qed. Lemma find_free_block_loop_arg_not_none : forall p0 p'0, Loop.loop_prop find_free_block_body p0 p'0 -> p0 = None -> False. Proof. induction 1. intros; subst. discriminate. intros. subst. injection H. auto. Qed. Theorem find_free_block_loop_none : forall p0 p'0, Loop.loop_prop find_free_block_body p0 p'0 -> forall p, Some p = p0 -> p'0 = None -> forall q, find_free_block_body_invariants p q -> forall b i, member (b, i) (find_free_block_freelist q) -> forall v, Some (Vint v) = load Mint32 m b (signed (sub i four)) -> cmp Clt v reqsize = true. Proof. induction 1. intros p ? ? q Hpq b i Hmem v Hv. subst. generalize H. unfold find_free_block_body. inversion Hpq. inversion find_free_block_freelist_hyp0. subst b0 i0. rewrite <- H3. intros ?. rewrite <- H0 in Hmem. inversion Hmem. subst b0 i0. rewrite <- H1. case_eq (load Mint32 m b' (signed (sub i' four))); try (intros; discriminate). destruct v0; try (intros; discriminate). case (cmp Cle reqsize (i0)); intros; discriminate. intros p ? ? q Hpq b i Hmem v Hv. subst a a''. generalize H. unfold find_free_block_body. inversion Hpq. inversion find_free_block_freelist_hyp0. subst b0 i0. rewrite <- H4. intros; discriminate. subst b0 i0. rewrite <- H2. case_eq (load Mint32 m b' (signed (sub i' four))). destruct v0. injection 2; intros; subst a'; destruct (find_free_block_loop_arg_not_none H0 (refl_equal _)). case_eq (cmp Cle reqsize ( i0)). intros; discriminate. intro Hlt. injection 2; intros; subst a'. symmetry in H. destruct (find_free_block_body_invariants_true (refl_equal _) Hpq H). simpl in H6. invall. assert (l = x). congruence. subst x. rewrite <- H1 in Hmem. inversion Hmem. subst b i l0. assert (v = i0). congruence. subst i0. apply le_false_lt_true. assumption. subst a l0. eapply IHloop_prop. reflexivity. auto. eassumption. simpl. eassumption. assumption. injection 2; intros; subst a'. destruct (find_free_block_loop_arg_not_none H0 (refl_equal _)). injection 2; intros; subst a'. destruct (find_free_block_loop_arg_not_none H0 (refl_equal _)). injection 2; intros; subst a'. destruct (find_free_block_loop_arg_not_none H0 (refl_equal _)). Qed. Theorem find_free_block_loop_some : forall p0 p'0, Loop.loop_prop find_free_block_body p0 p'0 -> forall p, Some p = p0 -> forall p', Some p' = p'0 -> forall q, find_free_block_body_invariants p q -> exists r, Some r = find_free_block_result p' /\ member (find_free_block_found_block_block r, find_free_block_found_block_offset r) (find_free_block_freelist q) /\ exists q', find_free_block_body_invariants p' q' /\ exists rq, find_free_block_freelist q' = (find_free_block_found_block_block r, find_free_block_found_block_offset r) :: rq /\ Some (Vint (find_free_block_found_block_size r)) = load Mint32 m (find_free_block_found_block_block r) (signed (sub (find_free_block_found_block_offset r) four)) /\ cmp Cle reqsize (find_free_block_found_block_size r) = true. Proof. induction 1. intros p ? p' ? q Hpq . subst. generalize H. unfold find_free_block_body. inversion Hpq. inversion find_free_block_freelist_hyp0. subst b i. rewrite <- H3. intros; discriminate. subst b i. rewrite <- H1. case_eq (load Mint32 m b' (signed (sub i' four))); try (intros; discriminate). destruct v; try (intros; discriminate). intro Hi. case_eq (cmp Cle reqsize ( i)); try (intros; discriminate). injection 2; intros; subst p'. exists (make_find_free_block_found_block b' i' i). split. simpl; trivial. split. simpl; auto. exists q. split. eapply find_free_block_body_invariants_intro; simpl; eauto. exists l. split. auto. simpl. eauto. intros p ? p' ? q Hpq. subst a a''. generalize H. unfold find_free_block_body. inversion Hpq. inversion find_free_block_freelist_hyp0. subst b i. rewrite <- H4. intros; discriminate. subst b i. rewrite <- H2. case_eq (load Mint32 m b' (signed (sub i' four))). destruct v. injection 2; intros; subst a'; destruct (find_free_block_loop_arg_not_none H0 (refl_equal _)). case (cmp Cle reqsize ( i)). intros; discriminate. injection 2; intros; subst a'. symmetry in H. destruct (find_free_block_body_invariants_true (refl_equal _) Hpq H). simpl in H6. invall. assert (l = x). congruence. subst x. destruct (IHloop_prop _ (refl_equal _) _ (refl_equal _) _ H8). invall. eapply ex_intro. split. eassumption. split. simpl in H9. auto. eapply ex_intro. split. eassumption. eapply ex_intro. split. eassumption. split; assumption. injection 2; intros; subst a'. destruct (find_free_block_loop_arg_not_none H0 (refl_equal _)). injection 2; intros; subst a'. destruct (find_free_block_loop_arg_not_none H0 (refl_equal _)). injection 2; intros; subst a'. destruct (find_free_block_loop_arg_not_none H0 (refl_equal _)). Qed. (* Termination *) Theorem find_free_block_loop_terminates : forall l q, find_free_block_freelist q = l -> forall p, find_free_block_body_invariants p q -> Loop.loop_term find_free_block_body (Some p). Proof. induction l. inversion 2. case_eq (find_free_block_body (Some p)). intros b o Hbo. generalize Hbo. unfold find_free_block_body at 1. rewrite H in find_free_block_freelist_hyp0. inversion find_free_block_freelist_hyp0. subst b0 i. rewrite <- H1. simpl. injection 1; intros; subst b o. eapply Loop.loop_term_interrupt. eassumption. inversion 2. case_eq (find_free_block_body (Some p)). intros b o Hbo. generalize Hbo. unfold find_free_block_body at 1. rewrite H in find_free_block_freelist_hyp0. inversion find_free_block_freelist_hyp0. subst l a i b0. rewrite <- H5. destruct (find_free_block_freelist_block_header H0 (b := b') (i := i')). rewrite H. auto. rewrite <- H1. case_eq (cmp Cle reqsize ( x)). intro Hle. injection 1; intros; subst b o. eapply Loop.loop_term_interrupt. eassumption. intro Hnle. injection 1; intros; subst b o. symmetry in Hbo. destruct (find_free_block_body_invariants_true (refl_equal _) H0 Hbo). simpl in H2. invall. assert (x0 = l0). congruence. subst x0. eapply Loop.loop_term_continue. eauto. eapply IHl. 2 : eassumption. simpl; trivial. Qed. End Find_free_block. Variable p' : find_free_block_body_param. Definition alloc_block := match find_free_block_result p' with | Some r => if eq (find_free_block_found_block_size r) reqsize then match load Mint32 m (find_free_block_found_block_block r) (signed (find_free_block_found_block_offset r)) with | Some v => match store Mint32 m (find_free_block_freelist_block p') (signed (find_free_block_freelist_offset p')) v with | Some m' => Some (m', (find_free_block_found_block_block r, find_free_block_found_block_offset r)) | _ => None end | _ => None end else if eq (find_free_block_found_block_size r) (add reqsize four) then match load Mint32 m (find_free_block_found_block_block r)(signed (find_free_block_found_block_offset r)) with | Some v => match store Mint32 m (find_free_block_freelist_block p') (signed (find_free_block_freelist_offset p')) v with | Some m1 => match store Mint32 m1 (find_free_block_found_block_block r) (signed (add (find_free_block_found_block_offset r) reqsize)) (Vint zero) with | Some m' => Some (m', (find_free_block_found_block_block r, find_free_block_found_block_offset r)) | _ => None end | _ => None end | _ => None end else let newsize := sub (find_free_block_found_block_size r) (add reqsize four) in match store Mint32 m (find_free_block_found_block_block r) (signed (find_free_block_found_block_offset r)) (Vint newsize) with | Some m1 => match store Mint32 m1 (find_free_block_found_block_block r) (signed (add (find_free_block_found_block_offset r) newsize)) (Vint (find_free_block_found_block_size r)) with | Some m' => Some (m', (find_free_block_found_block_block r, add (find_free_block_found_block_offset r) (add newsize four))) | _ => None end | _ => None end | _ => None end. Variable heap : block. Variable r : find_free_block_found_block. Hypothesis Hr : Some r = find_free_block_result p'. Variable q' : find_free_block_body_further_param. Hypothesis Hq' : find_free_block_body_invariants (fun b _ => b <> heap) p' q'. Variable rq : list (block * int). Hypothesis Hrq : find_free_block_freelist q' = (find_free_block_found_block_block r, find_free_block_found_block_offset r) :: rq . Hypothesis Hsize : Some (Vint (find_free_block_found_block_size r)) = load Mint32 m (find_free_block_found_block_block r) (signed (sub (find_free_block_found_block_offset r) four)). Lemma Hmem__0 : member (find_free_block_found_block_block r, find_free_block_found_block_offset r) initial_freelist. inversion Hq'. rewrite find_free_block_before_freelist_hyp0. apply member_app_right. rewrite Hrq. auto. Qed. Hypothesis Hsize_le : cmp Cle reqsize (find_free_block_found_block_size r) = true. Hypothesis reqsize_nonnull : cmp Clt zero reqsize = true. Hypothesis four_divides_reqsize : four_divides reqsize. Variable hs : int. Variable he : int. Variable blocklist : list int. Hypothesis Hblock : block_description_from_to m heap hs he blocklist. Hypothesis Hfreelist_block : forall a i, member (a, i) initial_freelist -> a = heap. Hypothesis Hfreelist_offset : forall a i, member (a, i) initial_freelist -> member i blocklist. Hypothesis Hfreelist_headers : forall i, member (heap, i) initial_freelist -> forall v, Some (Vint v) = load Mint32 m heap (signed (sub i four)) -> v = Size_header v. Hypothesis Hfreelist_sizes_not_null : forall i, member (heap, i) initial_freelist -> forall v, Some (Vint v) = load Mint32 m heap (signed (sub i four)) -> v <> zero. Lemma alloc_block_runs_well : {m' : _ & {b : _ & {o : _ | Some (m', (b, o)) = alloc_block}}}. Proof. generalize Hmem__0. intro Hmem. generalize (lt_is_signed_lt reqsize_nonnull). change (signed zero) with 0. intro H_reqsize_pos. assert (find_free_block_found_block_size r <> zero) as Hblocksize_nonzero. intro. rewrite H in Hsize_le. destruct (@int_lt_irrefl_1 zero). repeat int_le_lt_trans_tac; auto. assert (cmp Cle zero (sub (find_free_block_found_block_size r) one) = true) as Hblocksize_p_nonneg. eapply lt_is_le_p. repeat int_le_lt_trans_tac; auto. case_eq alloc_block. destruct p. destruct p. intros. repeat esplit; eauto. intro Hnone. apply False_rect. inversion Hq'. rewrite Hrq in find_free_block_freelist_hyp0. inversion find_free_block_freelist_hyp0. subst. generalize Hnone. unfold alloc_block. rewrite <- Hr. assert (exists x, Some x = load Mint32 m (find_free_block_found_block_block r) (signed (find_free_block_found_block_offset r))) as H. inversion H5. subst b i rq. eapply ex_intro; eauto. subst b i rq. eapply ex_intro; eauto. destruct H as [f H]. case_eq (eq (find_free_block_found_block_size r) reqsize). intro Heq_reqsize. rewrite <- H. case_eq (store Mint32 m (find_free_block_freelist_block p') (signed (find_free_block_freelist_offset p')) f). intros; discriminate. intro Habs. intros _. destruct (valid_access_store m Mint32 (find_free_block_freelist_block p') (signed (find_free_block_freelist_offset p')) f). eapply load_valid_access. eauto. discr. intro Hneq_reqsize. generalize (neq_bool_neq_prop Hneq_reqsize). intro Hneq_reqsize_prop. assert (cmp Clt reqsize (find_free_block_found_block_size r) = true) as Hsize_lt. apply lt_is_le_neq. assumption. auto. generalize (lt_is_le_p Hsize_lt). intro Hsize_le_p. assert (find_free_block_found_block_block r = heap) as Hfound_heap. eapply Hfreelist_block. eassumption. assert (member (find_free_block_found_block_offset r) blocklist) as Hfound_blocklist. eapply Hfreelist_offset. eassumption. rewrite Hfound_heap in *. generalize (nonempty_block_right Hblock Hfound_blocklist Hsize). intro Hp_le_ps_1. rewrite <- (Hfreelist_headers Hmem Hsize) in Hp_le_ps_1. generalize (Hp_le_ps_1 Hblocksize_nonzero). clear Hp_le_ps_1. intro Hp_le_ps. rewrite sub_add_opp in Hp_le_ps. rewrite add_assoc in Hp_le_ps. rewrite <- sub_add_opp in Hp_le_ps. generalize (plus_positive Hp_le_ps Hblocksize_p_nonneg). intro Hsum. case_eq (eq (find_free_block_found_block_size r) (add reqsize four)). intro Heq4. rewrite <- H. case_eq (store Mint32 m (find_free_block_freelist_block p') (signed (find_free_block_freelist_offset p')) f). intros m1 Hm1. case_eq ( store Mint32 m1 heap (signed (add (find_free_block_found_block_offset r) reqsize)) (Vint zero) ). intros; discriminate. intro Habs. intros _. destruct (valid_access_store m1 Mint32 heap (signed (add (find_free_block_found_block_offset r) reqsize)) (Vint zero)). eapply store_valid_access_1. eassumption. eapply block_description_valid. eassumption. eapply Hfreelist_offset. eassumption. eauto. intro Hnull. rewrite <- (Hfreelist_headers Hmem Hsize) in Hnull. rewrite Hnull in Hsize_le. contradiction. apply mod4_sym. apply modulo_four_four_divides_add. assumption. apply signed_le_is_le. rewrite add_signed. rewrite signed_repr. omega. generalize (signed_range (find_free_block_found_block_offset r)). intros [lo hi]. split. eapply Zle_trans. eassumption. omega. apply Zle_trans with (signed (find_free_block_found_block_offset r) + signed (sub (find_free_block_found_block_size r) one)). generalize (le_is_signed_le Hsize_le_p). omega. rewrite <- Hsum. generalize (signed_range (add (find_free_block_found_block_offset r) (sub (find_free_block_found_block_size r) one))); omega. apply modulo_four_le_m1_left. apply mod4_add. auto. eapply mod4_trans. apply four_divides_reqsize. apply mod4_sym. apply four_divides_size_header. rewrite <- (Hfreelist_headers Hmem Hsize) . rewrite sub_add_opp. rewrite add_assoc. rewrite <- sub_add_opp. apply signed_le_is_le. rewrite add_signed. rewrite Hsum. rewrite signed_repr. generalize (le_is_signed_le Hsize_le_p). omega. generalize (signed_range (find_free_block_found_block_offset r)). intros [lo hi]. split. omega. apply Zle_trans with (signed (find_free_block_found_block_offset r) + signed (sub (find_free_block_found_block_size r) one)). generalize (le_is_signed_le Hsize_le_p). omega. rewrite <- Hsum. generalize (signed_range (add (find_free_block_found_block_offset r) (sub (find_free_block_found_block_size r) one))); omega. discr. intros Habs _. destruct (valid_access_store m Mint32 (find_free_block_freelist_block p') (signed (find_free_block_freelist_offset p')) f). eapply load_valid_access. eauto. discr. intro Hneq4. generalize (neq_bool_neq_prop Hneq4). intro Hneq4_prop. destruct (modulo_four_le_eq_or_next (a := reqsize) (b := find_free_block_found_block_size r)). eapply mod4_trans. apply four_divides_reqsize. apply mod4_sym. rewrite (Hfreelist_headers Hmem Hsize) . apply four_divides_size_header. assumption. congruence. invall. destruct (modulo_four_le_eq_or_next (a := add reqsize four) (b := find_free_block_found_block_size r)). apply mod4_sym. eapply mod4_trans. rewrite (Hfreelist_headers Hmem Hsize) . apply four_divides_size_header. eapply mod4_trans. apply mod4_sym. apply four_divides_reqsize. apply modulo_four_four_divides_add. apply four_divides_four. assumption. congruence. invall. generalize (minus_positive (int_le_trans (int_le_lt_weak reqsize_nonnull) H0) H6). intro Hsub_pos. generalize (minus_bounded (int_le_trans (int_le_lt_weak reqsize_nonnull) H0) H6). intro Hsub_bound. case_eq ( store Mint32 m heap (signed (find_free_block_found_block_offset r)) (Vint (sub (find_free_block_found_block_size r) (add reqsize four)))). intros m1 Hm1. case_eq ( store Mint32 m1 heap (signed (add (find_free_block_found_block_offset r) (sub (find_free_block_found_block_size r) (add reqsize four)))) (Vint (find_free_block_found_block_size r))) ; try (intros; discriminate). intros Habs _. destruct (valid_access_store m1 Mint32 heap (signed (add (find_free_block_found_block_offset r) (sub (find_free_block_found_block_size r) (add reqsize four)))) (Vint (find_free_block_found_block_size r)) ). eapply store_valid_access_1. eauto. eapply block_description_valid. eassumption. eapply Hfreelist_offset. eassumption. eauto. rewrite <- (Hfreelist_headers Hmem Hsize). assumption. apply mod4_sym. apply modulo_four_four_divides_add. unfold four_divides. eapply mod4_trans. eapply modulo_four_four_divides_sub. unfold four_divides. eapply mod4_trans. apply mod4_sym. apply modulo_four_four_divides_add. apply four_divides_four. apply four_divides_reqsize. rewrite (Hfreelist_headers Hmem Hsize) . apply four_divides_size_header. eapply bounded_add_left. assumption. eapply lt_is_le_p. eapply lt_is_le_neq. eassumption. rewrite sub_add_opp. intro Habs_calc. generalize (add_zero_recip_l Habs_calc). change zero with (neg zero). intro Hneg. generalize (neg_inj Hneg). rewrite <- (sub_idem four). rewrite sub_add_opp. clear Hneg. clear Habs_calc. rewrite <- (add_commut (neg four)). intro Habs_calc. generalize (add_reg_r Habs_calc). intros; subst reqsize. discriminate. rewrite (Hfreelist_headers Hmem Hsize) . rewrite add_commut. rewrite <- sub_add_l. rewrite add_commut. eapply nonempty_block_right. eassumption. assumption. assumption. rewrite <-(Hfreelist_headers Hmem Hsize) ; assumption. rewrite sub_add_opp. rewrite sub_add_opp. rewrite add_assoc. eapply bounded_add_right. rewrite <- sub_add_opp. assumption. rewrite <- sub_add_opp. rewrite <- sub_add_opp. rewrite <- (Hfreelist_headers Hmem Hsize) . destruct (modulo_four_le_eq_or_next (a := (sub (find_free_block_found_block_size r) (add reqsize four))) (b := (find_free_block_found_block_size r))). eapply modulo_four_four_divides_sub. apply four_divides_add_four. apply four_divides_reqsize. assumption. cut (reqsize = neg four). intro ; subst reqsize; discriminate. rewrite sub_add_opp in e. generalize (add_zero_recip_l e). change zero with (neg zero). intro Habs_calc. generalize (neg_inj Habs_calc). clear Habs_calc. change zero with (sub four four). rewrite sub_add_opp. rewrite add_commut. intro Habs_calc. generalize (add_reg_l Habs_calc). tauto. invall. assumption. rewrite <- add_assoc. rewrite <- sub_add_opp. apply modulo_four_le_m1_left. apply modulo_four_four_divides_add. apply four_divides_size_header. eapply nonempty_block_right. eassumption. assumption. assumption. rewrite <- (Hfreelist_headers Hmem Hsize) ; assumption. discr. intro Habs. destruct (valid_access_store m Mint32 heap (signed (find_free_block_found_block_offset r)) (Vint (sub (find_free_block_found_block_size r) (add reqsize four)))). eapply load_valid_access. eauto. discr. Defined. Variable m' : mem. Variable fb : block. Variable fo : int. Hypothesis Hm' : Some (m', (fb, fo)) = alloc_block. Theorem alloc_invariant_heap_cells : forall i, member i blocklist -> (find_free_block_freelist_block p' = heap -> i <> find_free_block_freelist_offset p') -> i <> find_free_block_found_block_offset r -> forall v, Some (Vint v) = load Mint32 m heap (signed (sub i four)) -> forall x, modulo_four x i -> cmp Cle (sub i four) x = true -> cmp Cle x (sub (add i (Size_header v)) four) = true -> load Mint32 m heap (signed x) = load Mint32 m' heap (signed x). Proof. generalize Hmem__0. intro Hmem. generalize (lt_is_signed_lt reqsize_nonnull). change (signed zero) with 0. intro H_reqsize_pos. assert (find_free_block_found_block_size r <> zero) as Hblocksize_nonzero. intro. rewrite H in Hsize_le. destruct (@int_lt_irrefl_1 zero). repeat int_le_lt_trans_tac; auto. assert (cmp Cle zero (sub (find_free_block_found_block_size r) one) = true) as Hblocksize_p_nonneg. eapply lt_is_le_p. repeat int_le_lt_trans_tac; auto. intros i Hi_mem Hi_not_freelist Hi_not_found v Hv x Hx_mod4 Hx_lo Hx_hi. generalize Hm'. unfold alloc_block. inversion Hq'. rewrite Hrq in find_free_block_freelist_hyp0. inversion find_free_block_freelist_hyp0. subst. rewrite <- Hr. assert (exists x, Some x = load Mint32 m (find_free_block_found_block_block r) (signed (find_free_block_found_block_offset r))) as H. inversion H5. subst b i0 rq. eapply ex_intro; eauto. subst b i0 rq. eapply ex_intro; eauto. destruct H as [f H]. generalize (Hfreelist_block Hmem). intro Hfound_heap. generalize (Hfreelist_offset Hmem). intro Hfound_offset. rewrite Hfound_heap in *. generalize (block_description_disjoint Hi_mem Hfound_offset Hi_not_found Hblock Hv Hsize). rewrite <- (Hfreelist_headers Hmem Hsize). intros [Hi_found_disj]. case_eq (eq (find_free_block_found_block_size r) reqsize). intro Heq_reqsize. generalize (eq_bool_eq_prop Heq_reqsize). intro. subst reqsize. rewrite <- H. case_eq (store Mint32 m (find_free_block_freelist_block p') (signed (find_free_block_freelist_offset p')) f); try (intros; discriminate). intros m1 Hm1. injection 1; intros; subst m' fb fo. symmetry. inversion find_free_block_freelist_mem0. eapply load_store_other. eassumption. left; auto. generalize (Hfreelist_block (member_app_left H1 _)). intro Hheap. rewrite Hheap in *. generalize (Hfreelist_offset (member_app_left H1 _)). intro Hfmem. generalize (Hi_not_freelist (refl_equal _)). intro Hdiff. generalize (block_header Hblock Hfmem). intros [v0 Hv0]. generalize (block_description_disjoint Hi_mem Hfmem Hdiff Hblock Hv Hv0). intros [Hdisj]. symmetry. eapply get_set_int32_indep. eauto. intro Habs. subst x. apply Hdisj with (find_free_block_freelist_offset p'). assumption. eapply int_le_trans. eassumption. eapply modulo_four_le_m1_right. eapply mod4_trans. eapply modulo_four_four_divides_sub. apply four_divides_four. eapply modulo_four_four_divides_add. apply four_divides_size_header. eapply int_le_trans. eapply block_header_end_after_block_start. eassumption. assumption. eapply block_header_end_before_block_end. eassumption. assumption. assumption. eapply int_le_trans. eapply block_header_end_after_block_start. eassumption. assumption. eapply nonempty_block_left. eassumption. assumption. eassumption. rewrite <- (Hfreelist_headers (member_app_left H1 _) Hv0) . intro. destruct (Hfreelist_sizes_not_null (member_app_left H1 _) Hv0). assumption. eapply nonempty_block_right. eassumption. assumption. eassumption. rewrite <- (Hfreelist_headers (member_app_left H1 _) Hv0) . intro. destruct (Hfreelist_sizes_not_null (member_app_left H1 _) Hv0). assumption. eapply mod4_trans. eapply block_description_modulo_four. eassumption. assumption. eexact Hi_mem. apply mod4_sym. assumption. intro Hneq_reqsize. generalize (neq_bool_neq_prop Hneq_reqsize). intro Hneq_reqsize_prop. assert (cmp Clt reqsize (find_free_block_found_block_size r) = true) as Hsize_lt. apply lt_is_le_neq. assumption. auto. generalize (lt_is_le_p Hsize_lt). intro Hsize_le_p. generalize (nonempty_block_right Hblock Hfound_offset Hsize). intro Hp_le_ps_1. rewrite <- (Hfreelist_headers Hmem Hsize) in Hp_le_ps_1. generalize (Hp_le_ps_1 Hblocksize_nonzero). clear Hp_le_ps_1. intro Hp_le_ps. rewrite sub_add_opp in Hp_le_ps. rewrite add_assoc in Hp_le_ps. rewrite <- sub_add_opp in Hp_le_ps. generalize (plus_positive Hp_le_ps Hblocksize_p_nonneg). intro Hsum. case_eq (eq (find_free_block_found_block_size r) (add reqsize four)). intro Heq4. rewrite <- H. case_eq (store Mint32 m (find_free_block_freelist_block p') (signed (find_free_block_freelist_offset p')) f); try (intros; discriminate). intros m1 Hm1. case_eq ( store Mint32 m1 heap (signed (add (find_free_block_found_block_offset r) reqsize)) (Vint zero) ) ; try (intros; discriminate). intros m2 Hm2. injection 1; intros; subst m' fb fo. apply trans_equal with (load Mint32 m1 heap (signed x)). symmetry. inversion find_free_block_freelist_mem0. eapply load_store_other. eassumption. left; auto. generalize (Hfreelist_block (member_app_left H0 _)). intro Hheap. rewrite Hheap in *. generalize (Hfreelist_offset (member_app_left H0 _)). intro Hfmem. generalize (Hi_not_freelist (refl_equal _)). intro Hdiff. generalize (block_header Hblock Hfmem). intros [v0 Hv0]. generalize (block_description_disjoint Hi_mem Hfmem Hdiff Hblock Hv Hv0). intros [Hdisj]. symmetry. eapply get_set_int32_indep. eauto. intro Habs. subst x. apply Hdisj with (find_free_block_freelist_offset p'). assumption. eapply int_le_trans. eassumption. eapply modulo_four_le_m1_right. eapply mod4_trans. eapply modulo_four_four_divides_sub. apply four_divides_four. eapply modulo_four_four_divides_add. apply four_divides_size_header. eapply int_le_trans. eapply block_header_end_after_block_start. eassumption. assumption. eapply block_header_end_before_block_end. eassumption. assumption. assumption. eapply int_le_trans. eapply block_header_end_after_block_start. eassumption. assumption. eapply nonempty_block_left. eassumption. assumption. eassumption. rewrite <- (Hfreelist_headers (member_app_left H0 _) Hv0) . intro. destruct (Hfreelist_sizes_not_null (member_app_left H0 _) Hv0). assumption. eapply nonempty_block_right. eassumption. assumption. eassumption. rewrite <- (Hfreelist_headers (member_app_left H0 _) Hv0) . intro. destruct (Hfreelist_sizes_not_null (member_app_left H0 _) Hv0). assumption. eapply mod4_trans. eapply block_description_modulo_four. eassumption. assumption. eexact Hi_mem. apply mod4_sym. assumption. eapply get_set_int32_indep. eauto. intro Habs. subst x. apply Hi_found_disj with (add (find_free_block_found_block_offset r) reqsize). assumption. eapply int_le_trans. eassumption. eapply modulo_four_le_m1_right. eapply mod4_trans. eapply modulo_four_four_divides_sub. apply four_divides_four. eapply modulo_four_four_divides_add. apply four_divides_size_header. eapply int_le_trans. eapply block_header_end_after_block_start. eassumption. assumption. eapply block_header_end_before_block_end. eassumption. assumption. assumption. eapply int_le_trans. eapply block_header_end_after_block_start. eassumption. assumption. eapply int_le_trans. eapply nonempty_block_left. eassumption. assumption. eassumption. rewrite <- (Hfreelist_headers Hmem Hsize) . assumption. eapply bounded_add_left. apply int_le_lt_weak; assumption. eassumption. rewrite (Hfreelist_headers Hmem Hsize) . rewrite sub_add_opp. rewrite <- add_assoc. rewrite <- sub_add_opp. eapply nonempty_block_right. eassumption. assumption. eauto. rewrite <- (Hfreelist_headers Hmem Hsize) . assumption. rewrite sub_add_opp. rewrite add_assoc. rewrite <- sub_add_opp. eapply bounded_add_right. apply int_le_lt_weak; assumption. eassumption. rewrite (Hfreelist_headers Hmem Hsize) . rewrite sub_add_opp. rewrite <- add_assoc. rewrite <- sub_add_opp. eapply nonempty_block_right. eassumption. assumption. eauto. rewrite <- (Hfreelist_headers Hmem Hsize) . assumption. apply mod4_sym. eapply mod4_trans. eassumption. eapply mod4_trans. apply (block_description_modulo_four Hblock Hi_mem Hfound_offset). apply modulo_four_four_divides_add. apply four_divides_reqsize. intro Hneq4. generalize (neq_bool_neq_prop Hneq4). intro Hneq4_prop. destruct (modulo_four_le_eq_or_next (a := reqsize) (b := find_free_block_found_block_size r)). eapply mod4_trans. apply four_divides_reqsize. apply mod4_sym. rewrite (Hfreelist_headers Hmem Hsize) . apply four_divides_size_header. assumption. congruence. invall. destruct (modulo_four_le_eq_or_next (a := add reqsize four) (b := find_free_block_found_block_size r)). apply mod4_sym. eapply mod4_trans. rewrite (Hfreelist_headers Hmem Hsize) . apply four_divides_size_header. eapply mod4_trans. apply mod4_sym. apply four_divides_reqsize. apply modulo_four_four_divides_add. apply four_divides_four. assumption. congruence. invall. generalize (minus_positive (int_le_trans (int_le_lt_weak reqsize_nonnull) H0) H6). intro Hsub_pos. generalize (minus_bounded (int_le_trans (int_le_lt_weak reqsize_nonnull) H0) H6). intro Hsub_bound. assert (cmp Cle (sub (find_free_block_found_block_size r) (add reqsize four)) (sub (find_free_block_found_block_size r) one) = true ) as Hsub_bound_p. eapply lt_is_le_p. eapply lt_is_le_neq. eassumption. rewrite sub_add_opp. intro Habs. generalize (add_zero_recip_l Habs). change zero with (neg zero). clear Habs. intro Habs. generalize (neg_inj Habs). clear Habs. change zero with (sub four four). rewrite sub_add_opp. rewrite add_commut. intro Habs. generalize (add_reg_l Habs). clear Habs. intro Habs. rewrite Habs in *; discriminate. case_eq ( store Mint32 m heap (signed (find_free_block_found_block_offset r)) (Vint (sub (find_free_block_found_block_size r) (add reqsize four)))); try (intros; discriminate). intros m1 Hm1. case_eq ( store Mint32 m1 heap (signed (add (find_free_block_found_block_offset r) (sub (find_free_block_found_block_size r) (add reqsize four)))) (Vint (find_free_block_found_block_size r))) ; try (intros; discriminate). intros m2 Hm2. injection 1; intros; subst m' fb fo. apply trans_equal with (load Mint32 m1 heap (signed x)). eapply get_set_int32_indep. eauto. intro Habs. subst x. apply Hi_found_disj with (find_free_block_found_block_offset r). assumption. eapply int_le_trans. eassumption. eapply modulo_four_le_m1_right. eapply mod4_trans. eapply modulo_four_four_divides_sub. apply four_divides_four. eapply modulo_four_four_divides_add. apply four_divides_size_header. eapply int_le_trans. eapply block_header_end_after_block_start. eassumption. assumption. eapply block_header_end_before_block_end. eassumption. assumption. assumption. eapply int_le_trans. eapply block_header_end_after_block_start. eassumption. assumption. eapply nonempty_block_left. eassumption. assumption. eassumption. rewrite <- (Hfreelist_headers Hmem Hsize) . assumption. rewrite (Hfreelist_headers Hmem Hsize) . eapply nonempty_block_right. eassumption. assumption. eauto. rewrite <- (Hfreelist_headers Hmem Hsize) . assumption. apply mod4_sym. eapply mod4_trans. eassumption. apply (block_description_modulo_four Hblock Hi_mem Hfound_offset). eapply get_set_int32_indep. eauto. intro Habs. subst x. apply Hi_found_disj with (add (find_free_block_found_block_offset r) (sub (find_free_block_found_block_size r) (add reqsize four))). assumption. eapply int_le_trans. eassumption. eapply modulo_four_le_m1_right. eapply mod4_trans. eapply modulo_four_four_divides_sub. apply four_divides_four. eapply modulo_four_four_divides_add. apply four_divides_size_header. eapply int_le_trans. eapply block_header_end_after_block_start. eassumption. assumption. eapply block_header_end_before_block_end. eassumption. assumption. assumption. eapply int_le_trans. eapply block_header_end_after_block_start. eassumption. assumption. eapply int_le_trans. eapply nonempty_block_left. eassumption. assumption. eassumption. rewrite <- (Hfreelist_headers Hmem Hsize) . assumption. eapply bounded_add_left. assumption. eexact Hsub_bound_p. rewrite (Hfreelist_headers Hmem Hsize) . rewrite sub_add_opp. rewrite <- add_assoc. rewrite <- sub_add_opp. eapply nonempty_block_right. eassumption. assumption. eauto. rewrite <- (Hfreelist_headers Hmem Hsize) . assumption. rewrite <- (add_commut (find_free_block_found_block_size r)). rewrite sub_add_l. rewrite <- (add_commut (find_free_block_found_block_offset r)). eapply bounded_add_right. assumption. assumption. rewrite (Hfreelist_headers Hmem Hsize) . rewrite sub_add_opp. rewrite <- add_assoc. rewrite <- sub_add_opp. eapply nonempty_block_right. eassumption. assumption. eauto. rewrite <- (Hfreelist_headers Hmem Hsize) . assumption. apply mod4_sym. eapply mod4_trans. eassumption. eapply mod4_trans. apply (block_description_modulo_four Hblock Hi_mem Hfound_offset). apply modulo_four_four_divides_add. unfold four_divides. eapply mod4_trans. eapply modulo_four_four_divides_sub. unfold four_divides. eapply mod4_trans. apply mod4_sym. eapply modulo_four_four_divides_add. apply four_divides_four. apply four_divides_reqsize. rewrite (Hfreelist_headers Hmem Hsize) . apply four_divides_size_header. Qed. Theorem alloc_invariant_blocks : forall b, b <> heap -> b <> find_free_block_freelist_block p' -> forall c o, load c m b (signed o) = load c m' b (signed o). Proof. generalize Hmem__0. intro Hmem. intros b Hb_not_in_heap Hb_not_freelist_block c o. generalize Hm'. unfold alloc_block. inversion Hq'. rewrite Hrq in find_free_block_freelist_hyp0. inversion find_free_block_freelist_hyp0. subst. rewrite <- Hr. assert (exists x, Some x = load Mint32 m (find_free_block_found_block_block r) (signed (find_free_block_found_block_offset r))) as H. inversion H5. subst b0 i rq. eapply ex_intro; eauto. subst b0 i rq. eapply ex_intro; eauto. destruct H as [f H]. generalize (Hfreelist_block Hmem). intro Hfound_heap. generalize (Hfreelist_offset Hmem). intro Hfound_offset. rewrite Hfound_heap in *. case (eq (find_free_block_found_block_size r) reqsize). rewrite <- H. case_eq (store Mint32 m (find_free_block_freelist_block p') (signed (find_free_block_freelist_offset p')) f); try (intros; discriminate). intros m1 Hm1. injection 1; intros; subst m' fb fo. symmetry. eapply load_store_other. eassumption. left; auto. case (eq (find_free_block_found_block_size r) (add reqsize four)). rewrite <- H. case_eq (store Mint32 m (find_free_block_freelist_block p') (signed (find_free_block_freelist_offset p')) f); try (intros; discriminate). intros m1 Hm1. case_eq ( store Mint32 m1 heap (signed (add (find_free_block_found_block_offset r) reqsize)) (Vint zero) ) ; try (intros; discriminate). intros m2 Hm2. injection 1; intros; subst m' fb fo. apply trans_equal with (load c m1 b (signed o)). symmetry. eapply load_store_other. eassumption. left; auto. symmetry. eapply load_store_other. eassumption. left; auto. case_eq ( store Mint32 m heap (signed (find_free_block_found_block_offset r)) (Vint (sub (find_free_block_found_block_size r) (add reqsize four)))); try (intros; discriminate). intros m1 Hm1. case_eq ( store Mint32 m1 heap (signed (add (find_free_block_found_block_offset r) (sub (find_free_block_found_block_size r) (add reqsize four)))) (Vint (find_free_block_found_block_size r))) ; try (intros; discriminate). intros m2 Hm2. injection 1; intros; subst m' fb fo. apply trans_equal with (load c m1 b (signed o)). symmetry. eapply load_store_other. eassumption. left; auto. symmetry. eapply load_store_other. eassumption. left; auto. Qed. Variable rd : val. Variable roots : list (list (option (block * int))). Hypothesis Hroots : all_roots m rd roots. Variable pl : list (list (block * int)). Hypothesis Hpl : root_position_list m rd pl. Hypothesis roots_not_in_heap : forall rb ro, member (rb, ro) (flatten pl) -> rb <> heap. Hypothesis roots_not_in_freelist : forall rb ro, member (rb, ro) (flatten pl) -> rb <> find_free_block_freelist_block p'. Hypothesis freelist_not_accessible : forall b o, member (b, o) initial_freelist -> forall phi, realize_path m rd phi (Some (b, o)) -> False. Hypothesis accessible_in_heap : forall phi b o, realize_path m rd phi (Some (b, o)) -> b = heap. Hypothesis accessible_in_blocklist : forall phi b o, realize_path m rd phi (Some (b, o)) -> member o blocklist. Hypothesis closure_size_not_null : forall o, member o blocklist -> forall v, Some (Vint v ) = load Mint32 m heap (signed (sub o four)) -> Kind_header v = KIND_CLOSURE -> Size_header v = zero -> False. Theorem old_paths_get_new_paths : forall phi dest, realize_path m rd phi dest -> realize_path m' rd phi dest. Proof. generalize Hmem__0. intro Hmem. intros phi dest Hpath. eapply realize_path_invar_by_path; try eassumption. (* root positions *) intros. eapply alloc_invariant_blocks; eauto. (* blocks well sized *) intros p0 b0 i0 Hpath0 v0 Hv0. eapply int_le_trans. eapply block_header_end_after_block_start. eassumption. eauto. eapply block_header_end_before_block_end. eassumption. eauto. replace heap with b0. assumption. eauto. (* closures not zero-sized *) intros p0 b0 i0 Hpath0 v0 Hv0 Hkin Hsiz. eapply closure_size_not_null with i0 v0. eauto. replace heap with b0. eauto. eauto. assumption. assumption. (* same values *) intros p0 b0 i0 Hpath0 v0 Hv0 x xlo xhi x_mod4. inversion Hq'. replace b0 with heap. eapply alloc_invariant_heap_cells with i0 v0. eauto. intros Hfree Habs. inversion find_free_block_freelist_mem0. contradiction. eapply freelist_not_accessible with (find_free_block_freelist_block p') (find_free_block_freelist_offset p') p0. rewrite find_free_block_before_freelist_hyp0. apply member_app_left; auto. rewrite Hfree. rewrite <- Habs. replace heap with b0. assumption. eauto. intro Habs. eapply freelist_not_accessible with (find_free_block_found_block_block r) (find_free_block_found_block_offset r) p0. assumption. rewrite (Hfreelist_block Hmem). rewrite <- Habs. replace heap with b0. assumption. eauto. replace heap with b0; eauto. apply mod4_sym; auto. assumption. assumption. symmetry. eauto. Qed. Theorem new_paths_get_old_paths : forall phi dest, realize_path m' rd phi dest -> realize_path m rd phi dest. Proof. generalize Hmem__0. intro Hmem. intros phi dest Hpath. eapply realize_path_invar_by_path_recip; try eassumption. (* root positions *) intros. eapply alloc_invariant_blocks; eauto. (* exists header in "from" memory *) intros. destruct (block_header Hblock (accessible_in_blocklist H)). generalize (accessible_in_heap H). intros; subst. eapply ex_intro; eauto. (* blocks well sized *) intros p0 b0 i0 Hpath0 v0 Hv0. eapply int_le_trans. eapply block_header_end_after_block_start. eassumption. eauto. eapply block_header_end_before_block_end. eassumption. eauto. replace heap with b0. assumption. eauto. (* closures not zero-sized *) intros p0 b0 i0 Hpath0 v0 Hv0 Hkin Hsiz. eapply closure_size_not_null with i0 v0. eauto. replace heap with b0. eauto. eauto. assumption. assumption. (* same values *) intros p0 b0 i0 Hpath0 v0 Hv0 x xlo xhi x_mod4. inversion Hq'. replace b0 with heap. eapply alloc_invariant_heap_cells with i0 v0. eauto. intros Hfree Habs. inversion find_free_block_freelist_mem0. contradiction. eapply freelist_not_accessible with (find_free_block_freelist_block p') (find_free_block_freelist_offset p') p0. rewrite find_free_block_before_freelist_hyp0. apply member_app_left; auto. rewrite Hfree. rewrite <- Habs. replace heap with b0. assumption. eauto. intro Habs. eapply freelist_not_accessible with (find_free_block_found_block_block r) (find_free_block_found_block_offset r) p0. assumption. rewrite (Hfreelist_block Hmem). rewrite <- Habs. replace heap with b0. assumption. eauto. replace heap with b0; eauto. apply mod4_sym; auto. assumption. assumption. symmetry. eauto. Qed. (* What about block description and freelist ? *) Section Exact_size. Hypothesis Hexact_size : reqsize = find_free_block_found_block_size r. Lemma Hexact_size_bool : eq (find_free_block_found_block_size r) reqsize = true. Proof eq_prop_eq_bool (sym_equal Hexact_size). Theorem exact_size_block_description : block_description_from_to m' heap hs he blocklist. Proof. generalize (Hmem__0). intro Hmem. generalize Hm'. unfold alloc_block. rewrite <- Hr. rewrite Hexact_size_bool. inversion Hq'. rewrite Hrq in find_free_block_freelist_hyp0. inversion find_free_block_freelist_hyp0. subst. assert (exists x, Some x = load Mint32 m (find_free_block_found_block_block r) (signed (find_free_block_found_block_offset r))) as H. inversion H5. subst b i rq. eapply ex_intro; eauto. subst b i rq. eapply ex_intro; eauto. destruct H as [f H]. generalize (Hfreelist_block Hmem). intro Hfound_heap. generalize (Hfreelist_offset Hmem). intro Hfound_offset. rewrite <- H. case_eq (store Mint32 m (find_free_block_freelist_block p') (signed (find_free_block_freelist_offset p')) f); try (intros; discriminate). intros m1 Hm1. injection 1; intros; subst fb fo. inversion find_free_block_freelist_mem0. (* easy case : not in heap *) eapply block_description_invar_outside. eassumption. subst m'. symmetry. eassumption. assumption. (* difficult case : in heap *) rewrite H2 in *. generalize (Hfreelist_block (member_app_left H0 _)). intro Hfree_heap. generalize (Hfreelist_offset (member_app_left H0 _)). intro Hfree_offset. rewrite Hfree_heap in *. rewrite Hfound_heap in *. eapply block_description_same_headers_inv. eassumption. intros b Hb. destruct (eq_dec b (find_free_block_found_block_offset r)). subst b. (* HERE *) destruct (eq_dec b (find_free_block_freelist_offset p')). subst b. symmetry. eapply get_set_int32_indep. symmetry; eexact Hm1. rewrite sub_add_opp. intro Habs. generalize (add_zero_recip_l (sym_equal Habs)). inversion 1. apply mod4_sym. apply modulo_four_four_divides_sub. apply four_divides_four. symmetry. rewrite <- H2. eapply alloc_invariant_heap_cells. eexact Hb. intros; assumption. exists h. assert (exists x, Some x = load Mint32 m (find_free_block_found_block_block r) (signed (find_free_block_found_block_offset r))) as H. subst b i0 rq. eapply ex_intro; eauto. subst b i0 rq. eapply ex_intro; eauto. destruct H as [f H]. generalize (Hfreelist_block Hmem). intro Hfound_heap. generalize (Hfreelist_offset Hmem). intro Hfound_offset. rewrite Hfound_heap in *. generalize (block_description_disjoint Hi_mem Hfound_offset Hi_not_found Hblock Hv Hsize). rewrite <- (Hfreelist_headers Hmem Hsize). intros [Hi_found_disj]. End Exact_size. Section Quasi_exact_size. End Quasi_exact_size. Section Different_size. End Different_size. End Alloc.