Require Import Loop.
Require Export List_addons.
Load param.

Require Memory_abstract.

Require Export AST.
Require Export Values.
Require Export Mem.

Require Export Int_addons.

(* We do not care about whether equality on values is decidable.
   We just check equality between some kinds of values : integers, pointers. *)

Lemma eq_ptr : forall (bi bi' : block * int), {bi = bi'} + {bi <> bi'}.

Proof.
intros.
decide equality.
apply eq_dec.
apply Z_eq_dec.
Defined.

Lemma eq_optptr : forall (bi bi' : option (block * int)), {bi = bi'} + {bi <> bi'}.
Proof.
intros.
decide equality.
apply eq_ptr.
Defined.

Lemma eq_vptr : forall a b o, {a = Vptr b o} + {a = Vptr b o -> False}.

Proof.
destruct a; try (right; discriminate 1).
intro b0.
destruct (Z_eq_dec b b0).
intros o.
destruct (eq_dec i o).
left; congruence.
right; congruence.
right; congruence.
Defined.

Lemma eq_int : forall a i, {a = Vint i} + {a = Vint i -> False}.

Proof.
destruct a; try (right; discriminate 1).
intro b0.
destruct (eq_dec i b0).
left; congruence.
right; congruence.
Defined.

(* Access theorems *)

(*
Lemma get_int32_inv : forall m b,
(min_signed <= low_bound m b /\ high_bound m b <= max_signed) ->
forall i v,
Some v = load Mint32 m b (signed i) ->
cmp Cle i (add i three) = true.

Proof.
intros m b [Hb_lo Hb_hi] i v Hb.
symmetry in Hb.
destruct (load_inv _ _ _ _ _ Hb) as [Hv_acc ?]; subst.
destruct Hv_acc as [Hvb ? ? ?].
simpl in * |-.
apply signed_le_is_le.
rewrite add_signed.
change (signed three) with 3.
rewrite signed_repr; omega.
Qed.
*)

Lemma get_set_int32_indep : forall m m' b i v,
Some m' = store Mint32 m b (signed i) v ->
forall i', i <> i' -> modulo_four i i' ->
load Mint32 m b (signed i') = load Mint32 m' b (signed i').
Proof.
intros m m' b i v Hm' i' Hneq Hmod4.
symmetry.
eapply load_store_other.
eauto.
right.
eapply modulo_four_disjoint_blocks; eauto.
Qed.

(* Allocation *)

Lemma load_alloc_other_2 : forall m m' a b sp, 
alloc m a b = (m', sp) ->
forall q, q <> sp -> 
forall i chunk,
load chunk m q i = load chunk m' q i.
Proof.
intros m m' a b sp Hm' q Hq i chunk.
case_eq (load chunk m' q i).
intros v Hv.
generalize (load_valid_access _ _ _ _ _ Hv).
intros Hvalid'.
destruct (valid_access_alloc_inv _ _ _ _ _ Hm' _ _ _  Hvalid') as [Hvalid | [Habs ?]];
try contradiction.
generalize (valid_access_load _ _ _ _ Hvalid).
intros [v0 Hv0].
generalize (load_alloc_other _ _ _ _ _ Hm' _ _ _ _ Hv0).
intros; congruence.
intro.
case_eq (load chunk m q i); auto.
intros v Hv.
generalize (load_alloc_other _ _ _ _ _ Hm' _ _ _ _ Hv).
intros ; discr.
Qed.

Lemma load_alloc_other_3 : forall m m' a b sp, 
alloc m a b = (m', sp) ->
forall q, sp <> q -> 
forall i chunk,
load chunk m q i = load chunk m' q i.
Proof.
intros.
eapply load_alloc_other_2.
eassumption.
intro; congruence.
Qed.



(* Idea : represent, as a middle level, the list of the blocks
   to describe the memory state. *)

Definition size_mask := repr (Z_of_bits wordsize (fun z => andb (zle 2 z) (zle z (Z_of_nat wordsize - 3)))).

Definition Size_header h := and h size_mask.

Lemma four_divides_size_mask_0 : size_mask = mul four (shru size_mask two).
reflexivity.
Qed.

Lemma mul_four_shl_two : forall x, mul four x = shl x two.
intro x.
rewrite mul_commut.
rewrite shl_mul_two_p.
reflexivity.
Qed.

Lemma bitwise_binop_false:
  forall f,
  (forall a, f a a = false) ->
  forall x,
  bitwise_binop f x x = zero.
Proof.
  unfold bitwise_binop; intros.
  transitivity (repr (Z_of_bits wordsize (bits_of_Z wordsize 0))).
  decEq. 
  apply Z_of_bits_exten; intros.
  rewrite H.
  rewrite bits_of_Z_zero.
  trivial.
  reflexivity.
Qed.

Theorem xor_idem: forall x, xor x x = zero.
Proof.
  assert (forall b, xorb b b = false).
    destruct b; reflexivity.
  exact (bitwise_binop_false H).
Qed.

Lemma four_divides_and_zero : forall x, four_divides x -> and x three = zero.
Proof.
intros x Hx.
inversion Hx.
subst.
rewrite sub_zero_l in H ; subst.
rewrite mul_four_shl_two.
change three with (xor mone (shl mone two)).
rewrite and_xor_distrib.
rewrite and_mone.
rewrite and_shl.
rewrite and_mone.
apply xor_idem.
Qed.

Lemma and_four_mone : forall x, x = or (and x three) (and x (shl mone two)).
intro.
rewrite <- and_or_distrib.
replace (or three (shl mone two)) with mone.
rewrite and_mone.
trivial.
symmetry.
eapply trans_equal.
compute.
match goal with |- mkint ?x ?y = _ => change (mkint x y) with (repr x) end.
reflexivity.
unfold mone.
eapply eqm_samerepr.
unfold eqm.
unfold eqmod.
exists 1; reflexivity.
Qed.

Lemma and_zero_four_divides_0 : forall x, and x three = zero -> x = and x (shl mone two).
Proof.
intros x Hx.
pattern x at 1.
rewrite (and_four_mone x).
rewrite Hx.
rewrite or_commut.
rewrite or_zero.
trivial.
Qed.

Lemma and_zero_four_divides : forall x, and x three = zero -> four_divides x.
intros x.
change three with (sub four one).
generalize (modu_and x four two (refl_equal _)).
intro Hmodu.
rewrite <- Hmodu.
intro Hx.
generalize (modu_divu_Euclid x four (four_not_zero)).
rewrite Hx.
rewrite add_zero.
rewrite mul_commut.
pattern x at 1.
rewrite <- (sub_zero_l x).
intro.
unfold four_divides.
eapply mod4_intro.
eassumption.
Qed.

Lemma four_divides_size_header : forall h, four_divides (Size_header h).
Proof.
unfold Size_header.
intro h.
apply and_zero_four_divides.
rewrite and_assoc.
change (and size_mask three) with zero.
apply and_zero.
Qed.

Hint Resolve four_divides_size_header.

(* Put aside some lemmas about Size_header *)

Lemma size_header_nonnegative : forall h, cmp Cle zero (Size_header h) = true.
Admitted.

Lemma size_header_le_size_mask : forall h, cmp Cle (Size_header h) size_mask = true.
Admitted.

Lemma nonnegative_le_size_mask_size_header : forall s, cmp Cle zero s = true -> cmp Cle s size_mask = true -> four_divides s ->
s = Size_header s.
Admitted.

Section Description.
Variable m : mem.

Section Description_with_heap_included.

Variable heap : block.

Lemma member_block : forall l i j, member (i, j) (map (fun j0 : int => (heap, j0)) l) -> i = heap.
induction l; inversion 1; eauto.
Qed .

Lemma member_offset_to_block : forall l i, member i l -> member (heap, i) (map (fun j0 : int => (heap, j0)) l).
Proof.
induction 1; simpl; eauto.
Qed .

Lemma member_block_to_offset : forall l i j, member (i, j) (map (fun j0 : int => (heap, j0)) l) -> member j l.
Proof.
induction l; inversion 1; eauto.
Qed .

Corollary member_block_to_offset_2 :
forall l i j, member (i, j) (map (fun j0 : int => (heap, j0)) l) -> i = heap /\ member j l.
Proof.
intros.
split.
eapply member_block.
eassumption.
eapply member_block_to_offset.
eassumption.
Qed.

Inductive well_formed_from_to : int -> int -> Prop :=
| well_formed_end : forall he, well_formed_from_to he he
| well_formed_block : forall he n, (n = he -> False) ->
  forall v, Some (Vint v) = load Mint32 m heap (signed n) -> 
  (Size_header v <> zero -> forall x, modulo_four x n -> cmp Cle (add n four) x = true ->
    cmp Cle x (add n (Size_header v)) = true ->
    valid_access m Mint32 heap (signed x)) -> 
  cmp Cle n (add n three) = true ->
  cmp Cle (add n three) (add (add n (Size_header v)) three) = true -> 
  cmp Cle (add (add n (Size_header v)) three) (sub he one) = true ->
  well_formed_from_to (add (add n (Size_header v)) four) he -> well_formed_from_to n he.
Hint Constructors well_formed_from_to.

Inductive block_description_from_to : int -> int -> list int -> Prop :=
| block_description_end : forall he, block_description_from_to he he nil
| block_description_block : forall he n, (n = he -> False) ->
  forall v, Some (Vint v) = load Mint32 m heap (signed n) -> 
  (Size_header v <> zero -> forall x, modulo_four x n -> cmp Cle (add n four) x = true ->
    cmp Cle x (add n (Size_header v)) = true ->
    valid_access m Mint32 heap (signed x)) ->   
  cmp Cle n (add n three) = true ->
  cmp Cle (add n three) (add (add n (Size_header v)) three) = true -> 
  cmp Cle (add (add n (Size_header v)) three) (sub he one) = true ->
  forall l, block_description_from_to (add (add n (Size_header v)) four) he l -> block_description_from_to n he (cons (add n four) l).

Hint Constructors block_description_from_to.

Lemma block_description_from_to_func : forall n p l1,
block_description_from_to n p l1 -> forall l2, block_description_from_to n p l2 -> l1 = l2.

Proof.
induction 1; inversion 1; try congruence.
f_equal; apply IHblock_description_from_to; congruence.
Qed.

Lemma block_description_well_formed :
forall n p l, block_description_from_to n p l -> well_formed_from_to n p.

Proof.
induction 1 ; eauto.
Qed.

Lemma block_description_heap_nonempty : forall l n p, block_description_from_to n p l -> forall b, member b l ->
n = p -> False.
Proof.
intro l.
case l.
inversion 2.
inversion 1.
auto.
Qed.

Section From_properties.

Lemma well_formed_modulo_four : forall n p, well_formed_from_to n p -> modulo_four n p.
Proof.
induction 1; eauto.
eapply mod4_trans.
eapply modulo_four_four_divides_add.
eapply four_divides_size_header.
eapply mod4_trans.
eapply modulo_four_four_divides_add.
apply four_divides_four.
subst.
eassumption.
Qed.

Lemma from_heap_end_or_int : forall n p,
well_formed_from_to n p ->
(n = p -> False) ->
cmp Cle n (add n three) = true.
Proof.
intros n p Hn Hneq.
destruct Hn.
congruence.
assumption.
Qed.

Corollary from_before_heap_end : forall n p, well_formed_from_to n p ->
(n = p -> False) ->
cmp Cle n (sub p one) = true.
Proof.
intros n p Hn Hneq.
inversion Hn.
congruence.
subst.
eapply int_le_trans.
eapply from_heap_end_or_int; eassumption.
int_le_lt_trans_tac; eauto.
Qed.

Corollary well_formed_max : forall h,
well_formed_from_to (repr max_signed) h -> 
h = repr max_signed.
Proof.
 intros h Hmax.
 inversion Hmax; auto.
 subst.
 apply max_supremum.
 generalize (from_heap_end_or_int Hmax H).
 intro Hre.
 destruct three_not_zero.
 eapply add_zero_recip_l.
 apply int_le_antisym.
 apply max_upper_bound.
 assumption.
Qed.

Lemma well_formed_le_next_3 : forall n p,
well_formed_from_to n p ->
(n = p -> False) ->
forall v, Some (Vint v) = load Mint32 m heap (signed n) ->
(add (add n (Size_header v)) four = p -> False) ->
cmp Clt (add (add n (Size_header v)) three) (add (add n (Size_header v)) four) = true.

Proof.
intros n p Hn Hn_neq_p v Hv Hv_neq_p.
inversion Hn  as [ | ? ? ? v0 ? ? ? ? Hend].
contradiction.
subst.
replace v0 with v in * ; try congruence.
change four with (add three one).
rewrite <- add_assoc.
destruct (not_le_s_is_max (add (add n (Size_header v)) three)) as [ | e].
apply lt_is_le_neq.
auto.
intro Habs.
apply one_not_zero.
eapply add_zero_recip_l.
symmetry.
eassumption.
rewrite e in Hend.
generalize (max_supremum Hend).
intros Hmax.
destruct Hv_neq_p.
rewrite <- (sub_add_id p one).
change four with (add three one).
rewrite <- add_assoc.
f_equal.
congruence.
Qed.

End From_properties.

Section Block_description_properties.

Lemma block_description_modulo_four_hs : forall b l, member b l ->
forall  n p, block_description_from_to n p l -> modulo_four b n.
Proof.
induction 1.
inversion 1.
apply mod4_sym.
apply modulo_four_four_divides_add.
apply four_divides_four.
inversion 1.
subst.
eapply mod4_trans.
eapply IHmember.
eassumption.
apply mod4_sym.
eapply mod4_trans.
eapply modulo_four_four_divides_add.
eapply four_divides_size_header.
eapply modulo_four_four_divides_add.
apply four_divides_four.
Qed.

Corollary block_description_modulo_four : forall n p l, block_description_from_to n p l ->
forall b, member b l -> forall b', member b' l -> modulo_four b b'.
Proof.
intros.
eapply mod4_trans.
eapply block_description_modulo_four_hs.
eassumption.
eassumption.
apply mod4_sym.
eapply block_description_modulo_four_hs.
eassumption.
eassumption.
Qed.

Lemma block_description_tail : forall n p l, block_description_from_to n p l ->
forall l1 l2 b, l = l1 ++ (b :: l2) -> block_description_from_to (sub b four) p (b :: l2).
Proof.
induction 1.

intro l1; case l1; simpl; inversion 1.

intros l1 l2 b.
case l1.
simpl.
injection 1; intros; subst.
rewrite add_sub_id.
eapply block_description_block; (eassumption || reflexivity).
intros i l0.
simpl.
injection 1; intros; subst.
eapply IHblock_description_from_to.
reflexivity.
Qed.

Corollary block_well_formed : forall n p l, block_description_from_to n p l ->
forall b, member b l -> well_formed_from_to (sub b four) p.
Proof.
induction 1.
inversion 1.
inversion 1.
subst.
rewrite add_sub_id.
eapply well_formed_block.
eassumption.
eassumption.
assumption.
assumption.
assumption.
assumption.
eapply block_description_well_formed; eauto.
subst.
eauto.
Qed.

Lemma heap_end_four_forbidden : forall n p l,
block_description_from_to n p l ->
member (add p four) l -> False.
Proof.
induction 1.
inversion 1.
intros Hnhe.
case (member_which_dec eq_dec Hnhe).
intro e.
generalize (add_reg_r e).
congruence.
intro; eauto.
Qed.

Lemma min_forbidden_2 : forall p l, block_description_from_to (repr min_signed) p l ->
(     cmp Cle (repr max_signed) (sub p one) = true)
-> l = nil.
Proof.
intros p l Hp Hle.
generalize (max_supremum Hle).
rewrite <- min_minus_one_is_max.
repeat rewrite sub_add_opp.
intro Habs.
generalize (add_reg_r Habs).
intro Heq.
inversion Hp; congruence.
Qed.

Lemma block_header : forall n p l, block_description_from_to n p l ->
forall b, member b l -> {v | Some (Vint v) = load Mint32 m heap (signed (sub b four))}.
Proof.
intros n p l Hblock_desc b Hb.
case_eq (load Mint32 m heap (signed (sub b four))).
intros v Hv.
destruct v; try (
 apply False_rect; 
 induction Hblock_desc;
 inversion Hb;
 subst;
 try rewrite add_sub_id in *;
 congruence
).
exists i; trivial.
intro H.
apply False_rect.
induction Hblock_desc;
inversion Hb;
subst;
try rewrite add_sub_id in *;
congruence.
Defined.

Definition block_header_weak n p l (H : block_description_from_to n p l) i :=
 match member_dec eq_dec l i with
 | left Hmem => let (h, _) := block_header H Hmem in h
 | _ => zero
 end.


Lemma block_header_weak_prop : forall n p l (H : block_description_from_to n p l),
forall l0, block_description_from_to n p l0 ->
forall b, member b l0 ->
Some (Vint (block_header_weak H b)) = load Mint32 m heap (signed (sub b four)).
Proof.
unfold block_header_weak.
intros.
destruct (member_dec eq_dec l b).
 destruct (block_header H m0).
 assumption.
generalize (block_description_from_to_func H H0).
congruence.
Qed.


Lemma block_header_end_before_block_end : forall n p l, block_description_from_to n p l ->
forall b, member b l -> forall v, Some (Vint v) = load Mint32 m heap (signed (sub b four)) ->
cmp Cle (sub b one) (sub (add b (Size_header v)) one) = true.
Proof.
induction 1.
inversion 1.
inversion 1.
subst.
rewrite add_sub_id.
intros.
subst.
rewrite sub_add_opp.
rewrite add_assoc.
rewrite <- sub_add_opp.
change (sub four  one) with three.
rewrite add_assoc.
rewrite (add_commut four).
rewrite sub_add_opp.
rewrite add_assoc.
rewrite add_assoc.
rewrite <- sub_add_opp.
change (sub four  one) with three.
rewrite <- add_assoc.
congruence.
subst.
eauto.
Qed.

Lemma next_well_formed : forall n p l, block_description_from_to n p l ->
forall b, member b l -> forall v, Some (Vint v) = load Mint32 m heap (signed (sub b four)) ->
well_formed_from_to (add b (Size_header v)) p.
Proof.
induction 1.
inversion 1.
inversion 1.
subst.
rewrite add_sub_id.
intros.
subst.
rewrite add_assoc.
rewrite (add_commut four).
rewrite <- add_assoc.
apply block_description_well_formed with l.
congruence.
subst.
eauto.
Qed.

Lemma block_end_before_heap_end : forall n p l, block_description_from_to n p l ->
forall b, member b l -> forall v,
Some (Vint v) = load Mint32 m heap (signed (sub b four)) ->
cmp Cle (sub (add b (Size_header v)) one) (sub p one) = true.
Proof.
induction 1.
inversion 1.
inversion 1.
subst.

intros v0.
rewrite add_sub_id.
intros.
rewrite (add_commut n).
rewrite add_assoc.
rewrite sub_add_l.
change (sub four one) with three.
rewrite add_commut.
assert (v = v0).
congruence.
subst.
eauto.

subst.
intros.
eauto.
Qed.

Corollary block_header_end_before_heap_end : forall n p l, block_description_from_to n p l ->
forall b, member b l ->
cmp Cle (sub b one) (sub p one) = true.
Proof.
intros n p l Hnl b Hb.
destruct (block_header Hnl Hb) as [h Hh].
eapply int_le_trans.
eapply block_header_end_before_block_end.
eassumption.
assumption.
eassumption.
eapply block_end_before_heap_end.
eassumption.
assumption.
assumption.
Qed.

Lemma nonempty_block_left : forall n p l, block_description_from_to n p l ->
forall b, member b l -> forall v, 
Some (Vint v) = load Mint32 m heap (signed (sub b four)) ->
(Size_header v = zero -> False) ->
cmp Cle (sub b one) b = true.
Proof.
intros n p l Hnl b.
pattern b at 4.
rewrite <- (sub_add_id b one).
induction Hnl.
inversion 1.
inversion 1.
rewrite add_sub_id.
subst.
intros v0 Hv0.
replace v0 with v in *; [|congruence].
intro Hsize_not_null.
apply int_le_lt_weak.
assert (cmp Clt (sub (add n four) one) (sub (add (add n (Size_header v)) four) one) = true) as Hlt.
 apply lt_is_le_neq.
 rewrite sub_add_opp.
 rewrite add_assoc.
 rewrite <- sub_add_opp.
 change (sub four one) with three.
 rewrite sub_add_opp.
 rewrite add_assoc.
 rewrite <- sub_add_opp.
 change (sub four one) with three.
 assumption.
 rewrite sub_add_opp.
 rewrite sub_add_opp.
 intro Habs.
 generalize (add_reg_r Habs).
 intro Habs2.
 generalize (add_reg_r Habs2).
 pattern n at 1.
 rewrite <- (add_zero n).
 intro Habs3.
 generalize (add_reg_l (sym_equal Habs3)).
 assumption.
exact (lt_step Hlt).

subst.
intros; eapply IHHnl; eauto.
Qed.

Lemma nonempty_block_right : forall n p l, block_description_from_to n p l ->
forall b, member b l -> forall v,
Some (Vint v) = load Mint32 m heap (signed (sub b four)) ->
(Size_header v = zero -> False) ->
cmp Cle b (sub (add b (Size_header v)) one) = true.
Proof.
intros n l p Hnl b.
pattern b at 3.
rewrite <- (sub_add_id b one).
induction Hnl.
inversion 1.
inversion 1.
rewrite add_sub_id.
subst.
intros v0 Hv0.
replace v0 with v in *; [|congruence].
intro Hsize_not_null.
assert (cmp Clt (sub (add n four) one) (sub (add (add n (Size_header v)) four) one) = true) as Hlt.
 apply lt_is_le_neq.
 rewrite sub_add_opp.
 rewrite add_assoc.
 rewrite <- sub_add_opp.
 change (sub four one) with three.
 rewrite sub_add_opp.
 rewrite add_assoc.
 rewrite <- sub_add_opp.
 change (sub four one) with three.
 assumption.
 rewrite sub_add_opp.
 rewrite sub_add_opp.
 intro Habs.
 generalize (add_reg_r Habs).
 intro Habs2.
 generalize (add_reg_r Habs2).
 pattern n at 1.
 rewrite <- (add_zero n).
 intro Habs3.
 generalize (add_reg_l (sym_equal Habs3)).
 assumption.
rewrite (add_assoc n four).
rewrite (add_commut four).
rewrite <- add_assoc.
apply (lt_is_le_s Hlt).

subst.
intros; eapply IHHnl; eauto.
Qed.

Lemma block_start_after_heap_start : forall n p l, block_description_from_to n p l ->
forall b, member b l -> cmp Cle n (sub b four) = true.
Proof.
induction 1.
inversion 1.
inversion 1.
subst.
rewrite add_sub_id.
apply int_le_refl.
auto.

subst.
assert (well_formed_from_to n he) as Hn.
 eapply block_description_well_formed.
 eapply block_description_block; (eassumption || reflexivity).
generalize (from_heap_end_or_int Hn H).
intro.
case (not_le_s_is_max (add (add n (Size_header v)) three)) .
rewrite add_assoc.
rewrite add_assoc.
rewrite add_assoc.
change (add three one) with four.
rewrite <- add_assoc.
rewrite <- add_assoc.
intros.
eapply int_le_trans.
eassumption.
int_le_lt_trans_tac.
int_le_lt_trans_tac.
eapply IHblock_description_from_to; eauto.
intros Hmax.
assert (l = nil).
eapply min_forbidden_2.
rewrite <- max_plus_one_is_min.
rewrite <- Hmax.
rewrite add_assoc.
change (add three one) with four.
eassumption.
rewrite <- Hmax.
assumption.
subst.
match goal with H : member _ nil |- _ => inversion H end.
Qed.

Corollary block_header_end_after_block_start : forall n p l, block_description_from_to n p l ->
forall b, member b l ->
cmp Cle (sub b four) (sub b one) = true.
Proof.
induction 1; inversion 1; subst.
 rewrite add_sub_id.
 rewrite <- Hcalc.
 rewrite add_sub_id.
 assumption.
eapply IHblock_description_from_to; eauto.
Qed.

Corollary block_start_before_heap_end : forall n p l, block_description_from_to n p l ->
forall b, member b l ->
cmp Cle (sub b four) (sub p one) = true.
Proof.
intros n p l H b Hb.
destruct (block_header H Hb).
eapply int_le_trans.
eapply block_header_end_after_block_start; eauto.
eapply block_header_end_before_heap_end; eauto.
Qed.

Lemma block_description_head : forall n p l, block_description_from_to n p l ->
forall l1 l2 b, l = l1 ++ (b :: l2) -> block_description_from_to n (sub b four) l1.
Proof.
induction 1.

intro l1; case l1; simpl; inversion 1.

intros l1 l2 b.
case l1.
simpl.
injection 1; intros; subst.
rewrite add_sub_id.
eauto.
intros i l0.
simpl.
injection 1; intros; subst.
assert (member b (l0 ++ b :: l2)) as Hb.
 apply member_app_right.
 auto.
generalize (block_description_heap_nonempty H5 Hb).
intro Hnext_false.
assert (well_formed_from_to n he) as Hinit.
 eapply well_formed_block.
 assumption.
 eassumption.
 assumption.
 assumption.
 assumption.
 assumption.
 eapply block_description_well_formed; eassumption.
generalize (well_formed_le_next_3 Hinit H H0 Hnext_false).
intro Hlt.
assert (n = sub b four -> False).
intro Habs.
apply int_lt_irrefl_1 with (sub b four).
eapply int_le_lt_trans.
eapply int_le_refl.
symmetry.
eexact Habs.
eapply int_le_lt_trans.
eassumption.
eapply int_le_lt_trans.
eassumption.
eapply int_lt_le_trans.
eassumption.
eapply block_start_after_heap_start.
eassumption.
assumption.
eapply block_description_block.
assumption.
eassumption.
assumption.
assumption.
assumption.
case (eq_dec (add (add n (Size_header v)) four) (sub b four)).
intro.
change three with (sub four one).
rewrite add_commut.
rewrite <- sub_add_l.
rewrite add_commut.
rewrite e.
auto.
intro Hneq.
eapply int_le_trans.
eapply int_le_lt_weak.
eassumption.
apply (lt_is_le_p).
apply lt_is_le_neq.
eapply block_start_after_heap_start.
eassumption.
assumption.
assumption.

eapply IHblock_description_from_to.
reflexivity.
Qed.

Theorem block_description_sorted : forall n p l,
block_description_from_to n p l ->
sorted (fun p q => cmp Clt (sub p four) (sub q four) = true) l.
Proof.
 induction 1.
 auto.
 case_eq l.
 auto.
 intros i l0 ?.
 subst.
 apply sorted_S.
 rewrite add_sub_id.
 eapply int_lt_le_trans.
 apply lt_is_le_neq.
 eassumption.
 intros.
 apply three_not_zero.
 eapply add_zero_recip_l.
 eauto.
 int_le_lt_trans_tac.
 apply int_le_trans with (add (add n (Size_header v)) four).
 change four with (add three one).
 rewrite <- add_assoc.
 destruct (not_le_s_is_max (add (add n (Size_header v)) three)) as [|e].
 auto.
 cut (i::l0 = nil).
 discriminate 1.
 eapply min_forbidden_2.
 rewrite <- max_plus_one_is_min.
 rewrite <- e.
 rewrite add_assoc.
 change (add three one) with four.
 eauto.
 rewrite <- e.
 auto.
 eapply block_start_after_heap_start.
 eauto.
 auto.
 auto.
Qed.

Corollary block_description_no_duplicates : forall n p l,
block_description_from_to n p l ->
no_duplicates l.
Proof.
induction 1.
 auto.
apply no_duplicates_cons; auto.
intro Hmem.
destruct (@int_lt_irrefl_1 (sub (add n four) four)).
assert (block_description_from_to n he ((add n four :: nil) ++ l)).
 simpl.
 eauto.
pose (ord := fun i j => cmp Clt (sub i four) (sub j four) = true).
assert (forall a b, ord a b -> forall c, ord b c -> ord a c) as ord_trans.
 unfold ord; intros; repeat int_le_lt_trans_tac.
apply (sorted_app ord_trans (l1 := add n four :: nil) (l2 := l)).
eapply block_description_sorted.
 eassumption.
auto.
assumption.
Qed.

Lemma block_description_disjoint_aux : forall l b2, member b2 l -> forall b1,
forall n p, block_description_from_to n p (b1::l) ->
forall v1, 
Some (Vint v1) = load Mint32 m heap (signed (sub b1 four)) ->
forall v2, 
Some (Vint v2) = load Mint32 m heap (signed (sub b2 four)) ->
disjoint_intervals
 (sub b1 four) (sub (add b1 (Size_header v1)) one)
 (sub b2 four) (sub (add b2 (Size_header v2)) one).

Proof.
intros l b2 Hmemb2 b1 n p Hblock v1 Hv1 v2 Hv2.
inversion Hblock.
subst.
rewrite add_sub_id in *.
match goal with Hblock_next: block_description_from_to _ _ l |- _ =>
inversion Hblock_next end.
subst.
inversion Hmemb2.
subst.
generalize (well_formed_le_next_3 (block_description_well_formed Hblock) H1 H2 H).
intro Hlt.
apply disjoint_indep.
eapply int_lt_le_trans.
rewrite <- (add_commut four).
rewrite add_assoc.
rewrite (add_commut four).
rewrite sub_add_opp.
rewrite add_assoc.
rewrite <- sub_add_opp.
change (sub four ( one)) with three.
replace v with v1 in *; [|congruence].
eexact Hlt.
match goal with |- _ _ ?x _ = _ =>
rewrite <- (add_sub_id x four) end.
inversion Hmemb2.
auto.
match goal with Hblock_next : block_description_from_to _ _ (_::l0) |- _ =>
generalize (block_description_sorted Hblock_next) end.
intros Hsorted.
generalize (head_minimal (fun a b Hab c Hbc => int_lt_le_trans Hab (int_le_lt_weak Hbc)) Hsorted).
intros Hmin.
eapply int_le_lt_weak.
eapply Hmin.
reflexivity.
auto.
Qed.

Corollary block_description_disjoint : forall l b1, member b1 l ->
forall b2, member b2 l -> (b1 = b2 -> False) ->
forall n p, block_description_from_to n p l -> 
forall v1, 
Some (Vint v1) = load Mint32 m heap (signed (sub b1 four)) ->
forall v2, 
Some (Vint v2) = load Mint32 m heap (signed (sub b2 four)) ->
disjoint_intervals
 (sub b1 four) (sub (add b1 (Size_header v1)) one)
 (sub b2 four) (sub (add b2 (Size_header v2)) one).

Proof.
induction 1.
inversion 1.
intros ; contradiction (refl_equal b1).
subst.
intros.
eapply block_description_disjoint_aux ; eauto.

inversion 1.
subst.
intros.
apply disjoint_sym.
eapply block_description_disjoint_aux; eauto.

subst.
inversion 2.
intros.
subst.
eapply IHmember ; eauto.
Qed.

Corollary block_description_data_header_disjoint : forall n p l, block_description_from_to n p l -> 
forall b, member b l ->
forall v,
Some (Vint v) = load Mint32 m heap (signed (sub b four)) ->
(Size_header v = zero -> False) ->
forall x, cmp Cle b x = true -> cmp Cle x (sub (add b (Size_header v)) four) = true ->
forall b', member b' l -> x <> sub b' four.
Proof.
intros n p l Hl b Hb v Hv Hsize x xlo xhi b' Hb' Habs.
subst.
destruct (block_header Hl Hb') as [v' Hv'].
destruct (eq_dec b b') as [Heq | Hneq].
 subst.
 destruct four_not_zero.
 rewrite <- (neg_neg four).
 rewrite <- (neg_neg zero).
 f_equal.
 rewrite neg_zero.
 apply add_zero_recip_l with b'.
 rewrite <- sub_add_opp.
 apply int_le_antisym.
 eapply int_le_trans.
 eapply block_header_end_after_block_start.
  eassumption.
  assumption.
 eapply nonempty_block_left; eauto.
 assumption.
destruct (block_description_disjoint Hb Hb' Hneq Hl Hv Hv') as [H].
apply H with (sub b' four).
   eapply int_le_trans.
    eapply block_header_end_after_block_start; eauto.
   eapply int_le_trans.
    eapply nonempty_block_left; eauto.
   eassumption.
  eapply int_le_trans.
   eassumption.
  eapply modulo_four_le_m1_right.
  eapply modulo_four_four_divides_add.
   auto.
  pattern b at 1.
  rewrite <- (sub_add_id b one).
  eapply lt_is_le_s.
  eapply lt_is_le_neq.
   eapply block_header_end_before_block_end; eauto.
  rewrite sub_add_opp.
  rewrite sub_add_opp.
  rewrite <- (add_commut (Size_header v)).
  rewrite add_assoc.
  intro Habs.
  generalize (add_zero_recip_r (sym_equal Habs)).
  assumption.
 auto.
eapply int_le_trans.
 eapply block_header_end_after_block_start; eauto.
eapply block_header_end_before_block_end; eauto.
Qed.  

Theorem block_description_merge : forall n i l1, block_description_from_to n i l1 -> forall p l2,
block_description_from_to i p l2 -> (n = i \/ (n <> p /\ cmp Cle (sub i one) (sub p one) = true)) ->
block_description_from_to n p (l1 ++ l2).
Proof.
induction 1.
 intros; simpl; assumption.
intros p l2 Hl2.
inversion_clear 1 as [? | [Hn_diff_p Hhe_le_p]]; try contradiction.
simpl.
eapply block_description_block; try eassumption.
 repeat int_le_lt_trans_tac.
destruct (eq_dec he p) as [ ? | n0].
 subst.
 inversion Hl2; try congruence.
 subst.
 rewrite <- app_nil_end.
 assumption.
eapply IHblock_description_from_to.
 assumption.
right.
split.
 intro Habs.
 subst.
 destruct n0.
 apply add_reg_r with (neg one).
 rewrite <- sub_add_opp.
 rewrite <- sub_add_opp.
 apply int_le_antisym.
  assumption.
 rewrite <- Hcalc.
 rewrite add_sub_id.
 assumption.
assumption.
Qed.

Opaque cmp.

Theorem block_description_split : forall n p l0, block_description_from_to n p l0 -> forall i, 
member (add i four) l0 ->
exists l1, block_description_from_to n i l1 /\ exists l2', block_description_from_to i p (add i four :: l2') /\ 
l0 = l1 ++ (add i four :: l2') /\ (n = i \/ (n <> p /\ cmp Cle (sub i one) (sub p one) = true)).
Proof.
induction 1.
 inversion 1.
intros i Hi.
destruct (eq_dec i n).
 subst.
 exists (@nil int).
 split.
  auto.
 exists l.
 split.
  eapply block_description_block; (eassumption || reflexivity).
 split.
  simpl; trivial.
 left.
 trivial.
simple inversion Hi.
 generalize (list_inj H6).
 intros [Hi_n ?].
 destruct n0.
 eapply add_reg_r; eauto.
intros Hmem.
injection H7; intros; subst.
destruct (IHblock_description_from_to _ Hmem).
invall.
subst.
exists (add n four :: x).
split.
 eapply block_description_block.
  eauto.
  eassumption.
  assumption.
  assumption.
  assumption.
 destruct (eq_dec (add (add n (Size_header v)) four) i).
  subst.
  rewrite sub_add_opp.
  rewrite (add_assoc (add n (Size_header v)) four).
  rewrite <- sub_add_opp.
  change (sub four one) with three.
  auto.
  inversion H11.
   contradiction.
  invall.
  eapply int_le_trans.
  eapply int_le_lt_weak.
  eapply lt_step.
  eapply lt_is_le_neq.
  eassumption.
  rewrite <- Hcalc.
  intro Habs.
  generalize (add_reg_r Habs).
  rewrite <- (add_sub_id (add n (Size_header v)) four).
  rewrite sub_add_opp.
  rewrite sub_add_opp.
  clear Habs.
  intro Habs.
  generalize (add_reg_r Habs).
  assumption.
  rewrite add_assoc.
  change (add three one) with four.
  eapply from_before_heap_end.
  eapply block_description_well_formed; eauto.
  assumption.
 assumption.
exists x0.
split.
 assumption.
split.
 simpl.
 trivial.
right.
split.
 assumption.
inversion H11.
 subst.
 rewrite sub_add_opp.
 rewrite add_assoc.
 rewrite <- sub_add_opp.
 change (sub four one) with three.
 assumption.
subst.
invall.
assumption.
Qed.

Theorem block_description_split_strong : forall n p l0, block_description_from_to n p l0 -> forall i l1 l2', 
l0 = l1 ++ (add i four :: l2') ->
block_description_from_to n i l1 /\ block_description_from_to i p (add i four :: l2') /\ 
  (n = i \/ (n <> p /\ cmp Cle (sub i one) (sub p one) = true)).
Proof.
induction 1.
 intros; destruct l1; discriminate.
intros i l1 l2 Hi.
destruct (eq_dec i n).
 subst.
 destruct l1.
  split.
   auto.
  split.
   simpl in Hi.
   injection Hi.
   intros; subst.
   eapply block_description_block; (eassumption || reflexivity).
  auto.
 simpl in Hi.
 injection Hi.
 intros; subst.
 assert (block_description_from_to n he (add n four :: l1 ++ add n four :: l2)) as Hgeneral.
  eapply block_description_block; (eassumption || reflexivity).
 generalize (block_description_sorted Hgeneral).
 intro Hsorted.
 destruct (@int_lt_irrefl_1 (sub (add n four) four)).
 refine (head_minimal _ Hsorted _ _).
 intros; repeat int_le_lt_trans_tac.
 reflexivity.
 apply member_app_right; auto.
destruct l1.
simpl in Hi.
generalize (list_inj Hi).
 intros [Hi_n ?].
 destruct n0.
 eapply add_reg_r; eauto.
simpl in Hi.
injection Hi; intros; subst.
destruct (IHblock_description_from_to _ _ _ (refl_equal _)).
invall.
split.
 eapply block_description_block.
  eauto.
  eassumption.
  assumption.
  assumption.
  assumption.
 destruct (eq_dec (add (add n (Size_header v)) four) i).
  subst.
  rewrite sub_add_opp.
  rewrite (add_assoc (add n (Size_header v)) four).
  rewrite <- sub_add_opp.
  change (sub four one) with three.
  auto.
  inversion H9.
   contradiction.
  invall.
  eapply int_le_trans.
  eapply int_le_lt_weak.
  eapply lt_step.
  eapply lt_is_le_neq.
  eassumption.
  rewrite <- Hcalc.
  intro Habs.
  generalize (add_reg_r Habs).
  rewrite <- (add_sub_id (add n (Size_header v)) four).
  rewrite sub_add_opp.
  rewrite sub_add_opp.
  clear Habs.
  intro Habs.
  generalize (add_reg_r Habs).
  assumption.
  rewrite add_assoc.
  change (add three one) with four.
  eapply from_before_heap_end.
  eapply block_description_well_formed; eauto.
  assumption.
 assumption.
split.
 assumption.
right.
split.
 assumption.
inversion H9.
 subst.
 rewrite sub_add_opp.
 rewrite add_assoc.
 rewrite <- sub_add_opp.
 change (sub four one) with three.
 assumption.
invall.
assumption.
Qed.

Corollary block_description_explicit_split : forall l2 n p l1, block_description_from_to n p (l1 ++ l2) -> 
exists i, block_description_from_to n i l1 /\ block_description_from_to i p l2 /\ (n = i \/ (n <> p /\ cmp Cle (sub i one) (sub p one) = true)).
Proof.
destruct l2.
 intros.
 rewrite <- app_nil_end in H.
 exists p.
 split.
  assumption.
 split.
  auto.
 destruct (eq_dec n p).
  auto.
 right; auto.
intros.
rewrite <- (sub_add_id i four) in H.
rewrite <- (sub_add_id i four).
exists (sub i four).
eapply block_description_split_strong.
 eassumption.
trivial.
Qed.

Lemma block_description_valid : forall n p l, block_description_from_to n p l ->
forall b, member b l ->
forall v, Some (Vint v) = load Mint32 m heap (signed (sub b four)) ->
Size_header v <> zero ->
forall x, modulo_four x b ->
cmp Cle b x = true ->
cmp Cle x (sub (add b (Size_header v)) four) = true ->
valid_access m Mint32 heap (signed x).
Proof.
induction 1.
 inversion 1.
inversion 1.
subst.
intros v0 Hv0.
replace v0 with v in *. 
 intros Hv_not_null x Hmod4.
 rewrite add_assoc.
 rewrite (add_commut four).
 rewrite <- add_assoc.
 rewrite add_sub_id.
 apply H1.
  assumption.
  rewrite <- (add_sub_id n four).
  apply mod4_sym.
  eapply mod4_trans.
  eapply modulo_four_four_divides_sub.
   apply four_divides_four.
  apply mod4_sym.
  assumption.
 rewrite add_sub_id in Hv0; congruence.
subst.
apply IHblock_description_from_to.
assumption.
Qed.
  

End Block_description_properties.

Section Block_description_ascending_loop.

Variable p : int.

Let body (k : int * list int) :=
let (n, l) := k in
if eq_dec n p
then (false, (n, l))
else match 
 load Mint32 m heap (signed n)
with
| Some (Vint v) => let o := add (add n (Size_header v)) four in
  (true, (o, (l ++ (add n four::nil))))
| _ => (false, k)
end.

Let body_extensive : forall n l n' l' b, body (n, l) = (b, (n', l')) ->
exists l'', l' = l ++ l''.
Proof.
unfold body.
introvars.
destruct (eq_dec n p).
injection 1;intros ; subst; exists (nil (A := int));apply app_nil_end.
case (load Mint32 m heap (signed n)); try (injection 1; intros; subst; 
 exists (nil (A := int)); apply app_nil_end

).
destruct v;
injection 1; intros; subst; try (
 exists (nil (A := int)); apply app_nil_end
).
exists (add n four :: nil).
auto.
Qed.


Let loop_extensive : forall a a', loop_prop body a a' ->
forall n l, a = (n, l) -> forall n' l', a' = (n', l') ->
exists l'', l' = l ++ l''.
Proof.
induction 1.
intros n l ?.
subst.
intros n' l' ?.
subst.
eapply body_extensive; eauto.
genclear H.
destruct a'.
intro Hbody.
destruct a.
generalize (body_extensive Hbody).
intros [l'' Hl''].
injection 1.
intros.
subst.
generalize (IHloop_prop i (l1 ++ l'') (refl_equal _) n' l' (refl_equal _)).
intros [l''0 Hl''0].
exists (l'' ++ l''0).
rewrite <- app_ass.
auto.
Qed.

Let loop_correct : forall a a', loop_prop body a a' ->
forall n l, a =(n, l) -> forall n' l', a' = (n', l') -> 
well_formed_from_to n p -> 
forall l'', l' = l ++ l'' ->
block_description_from_to n p l''.
Proof.
induction 1.
intros n l ? n' l' ?.
genclear H.
unfold body.
subst.
destruct (eq_dec n p).
injection 1.
intros ? ? ; subst.
intros _.
intros l'' Hl''.
replace l'' with (nil (A := int)).
auto.
symmetry.
eapply app_fix_left.
eauto.
case_eq (load Mint32 m heap (signed n)).
destruct v; try (discriminate 2 || (
intro;
intros _;
inversion 1; [
contradiction |
discr])).
intros ? _; inversion 1; [contradiction | discr].

intros n l ?.
subst.
intros n' l' ?.
subst.
destruct a'.
genclear H.
unfold body.
destruct (eq_dec n p).
discriminate 1.
case_eq (load Mint32 m heap (signed n)); [|discriminate 2].
destruct v; try discriminate 2.
intros Hv.
injection 1.
intros.
subst.
generalize (loop_extensive H0 (refl_equal _) (refl_equal _)).
intros [l''0 Hl''0].
rewrite app_ass in Hl''0.
simpl in Hl''0.
generalize (app_reg_l Hl''0).
intro.
subst.
inversion H3.
contradiction.
subst.
replace i0 with v in * ; [| try congruence].
eapply block_description_block.
eassumption.
eassumption.
assumption.
eassumption.
eassumption.
eassumption.
eapply IHloop_prop.
reflexivity.
reflexivity.
assumption.
rewrite app_ass.
trivial.
Qed.

Let loop_terminates : forall n, well_formed_from_to n p ->
forall l, loop_term body (n, l).
induction 1.
intro.
eapply loop_term_interrupt.
unfold body.
destruct (eq_dec he he).
reflexivity.
congruence.

intro l.
eapply loop_term_continue.
unfold body.
destruct (eq_dec n he).
contradiction.
rewrite<- H0.
reflexivity.
subst.
auto.
Qed.

Theorem describe_blocks_strong : forall n, well_formed_from_to n p ->
{l | block_description_from_to n p l}.
Proof.
intros n Hn.
generalize (loop (loop_terminates Hn nil)).
intros [[? l] Hl].
generalize (loop_correct Hl (refl_equal _) (refl_equal _) Hn).
simpl.
intro H.
generalize (H l (refl_equal _)).
intro.
exists l ; trivial.
Defined.

Definition describe_blocks n (h : well_formed_from_to n p) :=
let (l, _) := describe_blocks_strong h in l.

Proposition describe_blocks_prop : forall n (h : well_formed_from_to n p),
block_description_from_to n p (describe_blocks h).
Proof.
unfold describe_blocks.
introvars.
destruct (describe_blocks_strong h).
auto.
Qed.

End Block_description_ascending_loop.

End Description_with_heap_included.

End Description.

(* Thanks (or because of ?) the memory model, writing outside the heap might be expressed without
interval problems. Let's see whether it's true. *)

Lemma block_description_samesize_inv : forall m heap n p l,
block_description_from_to m heap n p l ->
forall m' heap',
(forall b, member b l -> exists v', Some (Vint v') = load Mint32 m' heap' (signed (sub b four))) ->
(forall b, member b l ->
forall v, Some (Vint v) = load Mint32 m heap (signed (sub b four)) ->
forall v', Some (Vint v') = load Mint32 m' heap' (signed (sub b four)) ->
Size_header v = Size_header v') ->
(* new condition arises here *)
(forall b, member b l -> forall v, Some (Vint v) = load Mint32 m heap (signed (sub b four)) -> Size_header v <> zero -> forall x, modulo_four x b -> cmp Cle b x = true -> cmp Cle x (sub (add b (Size_header v)) four) = true -> valid_access m' Mint32 heap' (signed x)) ->
block_description_from_to m' heap' n p l.
Proof.
induction 1.
intros; apply block_description_end.
subst.
intros m' heap' Hheader_m'_ex Hheader_size_inv Hvalid.
generalize (Hheader_m'_ex _ (member_head _ _)).
intros [v' Hv'].
rewrite <- (add_sub_id n four) in H0.
rewrite (Hheader_size_inv _ (member_head _ _) _ H0 _ Hv') in *.
eapply block_description_block.
assumption.
rewrite add_sub_id in Hv'.
eassumption.
intros.
eapply Hvalid.
 apply member_head.
 eauto.
 rewrite (Hheader_size_inv _ (member_head _ _) _ H0 _ Hv').
 assumption.
 eapply mod4_trans.
  eassumption.
 apply modulo_four_four_divides_add.
 apply four_divides_four.
 assumption.
 rewrite add_assoc.
 rewrite (add_commut four).
 rewrite <- add_assoc.
 rewrite add_sub_id.
 rewrite (Hheader_size_inv _ (member_head _ _) _ H0 _ Hv'). 
 assumption.
 assumption.
 assumption.
 assumption.
eapply IHblock_description_from_to.
intros; eapply Hheader_m'_ex; eauto.
intros.
eapply Hheader_size_inv.
eapply member_tail.
eassumption.
assumption.
assumption.
intros; eauto.
Qed.

Corollary block_description_same_headers_inv : forall m heap n p l,
block_description_from_to m heap n p l ->
forall m' heap',
(forall b, member b l -> load Mint32 m' heap' (signed (sub b four)) = load Mint32 m heap (signed (sub b four))) ->
(forall b, member b l -> forall v, Some (Vint v) = load Mint32 m heap (signed (sub b four)) -> Size_header v <> zero -> forall x, modulo_four x b -> cmp Cle b x = true -> cmp Cle x (sub (add b (Size_header v)) four) = true -> valid_access m' Mint32 heap' (signed x)) ->
block_description_from_to m' heap' n p l.
Proof.
intros m heap n p l Hblock m' heap' Hm' Hvalid.
eapply block_description_samesize_inv.
 eassumption.
 intros b Hb.
 destruct (block_header Hblock Hb) as [v Hv].
 exists v.
 rewrite Hv.
 symmetry.
 eauto.
intros b Hb v Hv v' Hv'.
rewrite <- (Hm' _ Hb) in Hv.
congruence.
assumption.
Qed.

Corollary block_description_ext_heap_zone : forall m heap n p l,
block_description_from_to m heap n p l ->
forall m' heap',
(forall x c, load c m heap (signed x) = load c m' heap' (signed x)) ->
block_description_from_to m' heap' n p l.
Proof.
intros m heap n p l Hblock m' heap' Hext.
eapply block_description_samesize_inv.
eassumption.
intros b Hb.
destruct (block_header Hblock Hb) as [v Hv].
exists v.
rewrite Hv.
eauto.
intros ? ? ?;
rewrite <- Hext; intros; congruence.
intros b Hb.
generalize (block_description_valid Hblock Hb).
intros Hvalid v Hv Hnz x Hmod4 xlo xhi.
generalize (Hvalid _ Hv Hnz _ Hmod4 xlo xhi).
intros Hxv.
destruct (valid_access_load _ _ _ _ Hxv).
eapply load_valid_access.
rewrite <- Hext.
eauto.
Qed.

Corollary block_description_invar_outside : forall m b heap, b <> heap ->
forall c o v m', Some m' = store c m b o v -> 
forall n p l, block_description_from_to m heap n p l ->
block_description_from_to m' heap n p l.

Proof.
intros m b heap b_neq_heap c o v m' Hm' n p l Hblock.
eapply block_description_ext_heap_zone.
eassumption.
intros.
symmetry.
eapply load_store_other.
eauto.
left; congruence.
Qed.

(* To express the fact that two memories have the same values in a zone,
   better use load than direct access to the contents *)

(* No need.
Lemma block_description_ext_heap_zone_but_in_heap : forall m,
(forall b, valid_block m b -> min_signed <= low_bound m b /\ high_bound m b <= max_signed) ->
forall heap n p l,
block_description_from_to m heap n p l ->
forall m' heap',
(forall x, cmp Cle n x = true -> cmp Cle x (sub p one) = true -> 
forall c, load c m heap (signed x) = load c m' heap' (signed x)) ->

block_description_from_to m' heap' n p l.

Proof.
 intros m Hm_valid heap n p l.
 induction 1 as [ | he n Hn v Hv s Hs Hs_div Hle Hbd l Hl IHblock ].
 intros; eapply block_description_end; eauto.
 assert (block_description_from_to m heap n he (add n four :: l)) as Hn_prev.
 eapply block_description_block ; eauto.
 subst.
 intros m' heap' Hext.
 eapply block_description_block.
 assumption.
 eapply trans_equal.
 eexact Hv.
 apply Hext.
 auto.
 eapply int_le_trans.
 eapply get_int32_inv; eauto.
 int_le_lt_trans_tac.
 assumption.
 reflexivity. 
 assumption.
 assumption.
 assumption.
 inversion Hl.
 apply block_description_end.
 subst.
 eapply IHblock.
 intros x xlo xhi c.
 apply Hext.
 eapply int_le_trans.
 eapply get_int32_inv; eauto.
 int_le_lt_trans_tac.
 eapply int_le_trans.
 eapply int_le_lt_weak.
 eapply well_formed_le_next_3.
 eapply block_description_well_formed.
 eexact Hn_prev.
 assumption.
 assumption.
 assumption.
 assumption.
 assumption.
Qed.
*)

Lemma block_description_same_sizes_head : forall n p b l m heap, block_description_from_to m heap n p (b::l) ->
forall m' heap', block_description_from_to m' heap' n p (b::l) ->
forall v, Some (Vint v) = load Mint32 m heap (signed (sub b four))  ->
forall v', Some (Vint v') = load Mint32 m' heap' (signed (sub b four)) ->
Size_header v = Size_header v'.
Proof.
introvars.
intro Hm.
introvars.
intro Hm'.
inversion Hm.
inversion Hm'.
subst.
rewrite add_sub_id.
intros v1 Hv1.
replace v1 with v in *; [|congruence].
intros v' Hv'.
replace v0 with v' in *; [|congruence].
inversion H9.
inversion H20.
subst.
apply add_reg_l with n.
apply add_reg_r with four.
congruence.
congruence.
inversion H20.
congruence.
subst.
generalize (list_inj H33).
intros [? ?].
apply add_reg_l with n.
apply add_reg_r with four.
apply add_reg_r with four.
congruence.
Qed.

Corollary block_description_same_sizes : forall n l m heap p, block_description_from_to m heap n p l ->
forall m' heap', block_description_from_to m' heap' n p l ->
forall b, member b l ->
forall v, Some (Vint v) = load Mint32 m heap (signed (sub b four))  ->
forall v', Some (Vint v') = load Mint32 m' heap' (signed (sub b four)) ->
Size_header v = Size_header v'.
Proof.
induction 1.
inversion 2.
intros m' heap' Hm'.
inversion Hm'.
subst.
assert (block_description_from_to m heap n he (add n four :: l))
as Hm.
 eapply block_description_block.
 assumption.
 eassumption.
 assumption.
 assumption.
 assumption.
 assumption.
 assumption.
intros b Hmem v1 Hv1 v' Hv'.
inversion Hmem.
subst.
intros; eapply block_description_same_sizes_head.
eexact Hm.
eexact Hm'.
assumption.
assumption.
subst.
cut (Size_header v = Size_header v0).
intro Hbegin.
rewrite Hbegin in IHblock_description_from_to.
eapply IHblock_description_from_to; eauto.
eapply block_description_same_sizes_head.
eexact Hm.
eexact Hm'.
rewrite add_sub_id.
assumption.
rewrite add_sub_id.
assumption.
Qed.

Definition kind_mask := repr 3.

Definition Kind_header h := and h kind_mask.
Definition KIND_RAWDATA := zero.
Definition KIND_PTRDATA := one.
Definition KIND_CLOSURE := two.

Lemma kind_rawdata_neq_ptrdata : KIND_RAWDATA = KIND_PTRDATA -> False.
Proof.
inversion 1.
Qed.

Lemma kind_ptrdata_neq_closure : KIND_PTRDATA = KIND_CLOSURE -> False.
Proof.
inversion 1.
Qed.

Lemma kind_closure_neq_rawdata : KIND_CLOSURE = KIND_RAWDATA -> False.
Proof.
inversion 1.
Qed.

Inductive val_is_pointer_or_dumb : val -> option (block * int) -> Prop :=
| val_is_pointer : forall b i, val_is_pointer_or_dumb (Vptr b i) (Some (b, i))
| val_is_dumb : val_is_pointer_or_dumb (Vint zero) None.

Inductive val_is_pointer_or_dumb_desc : val -> Prop :=
| val_is_pointer_desc : forall b i, val_is_pointer_or_dumb_desc (Vptr b i)
| val_is_dumb_desc : val_is_pointer_or_dumb_desc (Vint zero).

Hint Constructors val_is_pointer_or_dumb val_is_pointer_or_dumb_desc.

Lemma val_is_pointer_or_dumb_func : forall v bi, val_is_pointer_or_dumb v bi ->
forall bi', val_is_pointer_or_dumb v bi' -> bi = bi'.
Proof.
induction 1; inversion 1; eauto.
Qed.

Lemma val_is_pointer_or_dumb_inj : forall v bi, val_is_pointer_or_dumb v bi ->
forall v', val_is_pointer_or_dumb v' bi -> v = v'.
Proof.
induction 1; inversion 1; eauto.
Qed.

Lemma val_is_pointer_or_dumb_describes : forall v bi, val_is_pointer_or_dumb v bi ->
val_is_pointer_or_dumb_desc v.
Proof.
induction 1; eauto.
Qed.

Lemma construct_val_is_pointer_or_dumb : forall v, val_is_pointer_or_dumb_desc v ->
{bi | val_is_pointer_or_dumb v bi}.
Proof.
intros v Hv.
destruct v ; try (apply False_rect; inversion Hv ; fail).
destruct (eq_dec i zero).
  subst; exists (None (A := (block * int))); auto.
 apply False_rect; inversion Hv; congruence.
exists (Some (b, i)); auto. 
Defined .

Hint Resolve val_is_pointer_or_dumb_func val_is_pointer_or_dumb_describes.

Definition construct_val_is_pointer_or_dumb_recip_weak m :=
match m with
  | None => Vint zero
  | Some (b, i) => Vptr b i
end.

Lemma val_is_pointer_or_dumb_recip : forall b, val_is_pointer_or_dumb (construct_val_is_pointer_or_dumb_recip_weak b) b.
Proof.
destruct b as [[? ?] | ]; simpl; auto.
Qed.

Section Pointers.

Variable m : mem.

Section Pointer_list_block.

Variable heap : block.
Variable b : int.

Section Pointer_list.

Variable until : int.

Inductive pointer_list : int -> list (option (block * int)) -> Prop :=
| pointer_list_end : forall i, i = until -> pointer_list i nil
| pointer_list_cont : forall i, (i = until -> False) -> forall v,
  Some v = load Mint32 m heap (signed i) -> forall l, pointer_list (sub i four) l ->
  forall p, val_is_pointer_or_dumb v p -> pointer_list i (p::l).

Hint Constructors pointer_list.

Lemma pointer_list_func : forall i l1, pointer_list i l1 -> forall l2, pointer_list i l2 -> l1 = l2.
induction 1.
inversion 1.
auto.
contradiction.
inversion 1.
contradiction.
subst.
replace v0 with v in *; [|congruence].
f_equal; eauto.
Qed.

Lemma pointer_list_i_func : forall i1 l, pointer_list i1 l -> forall i2, pointer_list i2 l -> i1 = i2.
induction 1.
 inversion 1.
 congruence.
inversion 1.
subst.
apply add_reg_r with (neg four).
rewrite <- sub_add_opp.
eapply IHpointer_list.
rewrite <- sub_add_opp.
assumption.
Qed.

Inductive pointer_list_desc : int -> Prop :=
| pointer_list_desc_end : forall i, i = until -> pointer_list_desc i
| pointer_list_desc_cont : forall i, (i = until -> False) -> 
  forall v, Some v = load Mint32 m heap (signed i) ->
    val_is_pointer_or_dumb_desc v ->
pointer_list_desc (sub i four) ->
pointer_list_desc i.

Hint Constructors pointer_list_desc.

Lemma pointer_list_describes : forall i l, pointer_list i l -> pointer_list_desc i.
Proof.
induction 1; eauto.
Qed.

Hint Resolve pointer_list_describes.

Lemma pointer_list_desc_exists : forall i, pointer_list_desc i -> exists l, pointer_list i l.
Proof.
induction 1.
exists (@nil (option (block * int))); auto.
inversion IHpointer_list_desc as [l ?].
generalize (construct_val_is_pointer_or_dumb H1).
intros [v2 ?].
exists (v2 :: l); eauto.
Qed.

Hint Resolve pointer_list_desc_exists.

Section Pointer_list_loop.

(* To be redone soon.

Let body (a : int * list int) := let (i, l) := a in
if eq_dec i until then (false, (i, l)) else
match get_int32 i m with
| Some v => (true, (sub i four, l ++ (v :: nil)))
| None => (false, (i, l))
end.

Let body_extensive : forall n l n' l' b, body (n, l) = (b, (n', l')) ->
exists l'', l' = l ++ l''.
unfold body.
introvars.
case (eq_dec n until).
injection 2.
intros ; subst.
exists (nil (A := int)).
apply app_nil_end.
case (get_int32 n m).
injection 2.
intros ; subst.
exists (i::nil).
auto.
injection 2.
intros ; subst.
exists (nil (A:=int)).
apply app_nil_end.
Qed.

Let loop_extensive : forall a a', loop_prop body a a' -> 
forall n l, a = (n, l) -> forall n' l', a' = (n', l') ->
exists l'', l' = l ++ l''.
induction 1.
intros n l ? n' l' ? ; subst.
eapply body_extensive; eauto.
intros n l ? n' l' ? ; subst.
destruct a'.
generalize (body_extensive H).
intros [l'' Hl''].
subst.
generalize (IHloop_prop _ _ (refl_equal _) _ _ (refl_equal _)).
intros [l''0 Hl''0].
subst.
exists (l'' ++ l''0).
apply app_ass.
Qed.

Let loop_correct : forall a a', loop_prop body a a' ->
forall n l, a =(n, l) -> forall n' l', a' = (n', l') -> 
pointer_list_desc n ->
(* (exists l'', pointer_list n l'') ->  *)
forall l'', l' = l ++ l'' ->
pointer_list n l''.
induction 1.
intros n l ? n' l' ? ; subst.
genclear H.
unfold body.
case (eq_dec n until).
intro.
subst.
injection 1.
intro.
subst l'.
intro.
intros _.
intros l'' Hl''.
generalize (app_fix_left Hl'').
intro.
subst l''.
apply pointer_list_end.
auto.
intro Hneq.
case_eq (get_int32 n m).
discriminate 2.
intros ? ? Hdesc.
destruct (pointer_list_desc_exists Hdesc) as [l'' Hl''].
inversion Hl''.
contradiction.
discr.

intros n l ? n' l' ? Hdesc.
destruct (pointer_list_desc_exists Hdesc) as [l'' Hl''].
subst.
genclear H.
unfold body.
case (eq_dec n until).
discriminate 2.
intro Hneq.
inversion Hl''.
contradiction.
subst.
rewrite <- H1.
injection 1.
intro.
subst.
generalize (loop_extensive H0 (refl_equal _) (refl_equal _)).
intros [l''0 Hl''0].
subst.
intros l''1.
rewrite app_ass.
simpl.
intro Hl''1.
generalize (app_reg_l Hl''1).
intro.
subst.
eapply pointer_list_cont.
assumption.
assumption.
eapply IHloop_prop.
reflexivity.
reflexivity.
eauto.
auto.
Qed.

Let loop_terminates : forall n, 
(* (exists l, pointer_list n l) -> *)
pointer_list_desc n ->
forall l0, loop_term body (n, l0).
intros n Hdesc.
induction Hdesc.
(* [l Hl]. induction Hl. *)
intro l0.
eapply loop_term_interrupt.
unfold body.
case (eq_dec i until).
intros _ ; reflexivity.
intro ; contradiction.
intro l0.
eapply loop_term_continue.
unfold body.
case (eq_dec i until).
intro ; contradiction.
intros _.
rewrite <- H0.
reflexivity.
auto.
Qed.
*)

Theorem construct_pointer_list : forall n,
pointer_list_desc n ->
{l | pointer_list n l}.
Admitted.
(*
Proof.
intros n Hn.
generalize (loop (loop_terminates Hn nil)).
intros [[? l] Hl].
generalize (loop_correct Hl (refl_equal _) (refl_equal _) Hn (refl_equal _)).
intro.
exists l ; auto.
Defined.
*)


End Pointer_list_loop.

End Pointer_list.

Hint Constructors pointer_list pointer_list_desc.
Hint Resolve pointer_list_describes pointer_list_desc_exists.

Inductive pointer_list_block : list (option (block * int)) -> Prop := 
| pointer_list_block_rawdata : forall v, Some (Vint v) = load Mint32 m heap (signed (sub b four)) ->
  Kind_header v = KIND_RAWDATA -> pointer_list_block nil
| pointer_list_block_ptrdata : forall v, Some (Vint v) = load Mint32 m heap (signed (sub b four)) ->
  Kind_header v = KIND_PTRDATA -> forall l,
  pointer_list (sub b four) (sub (add b (Size_header v)) four) l ->
  pointer_list_block l
| pointer_list_block_closure : forall v, Some (Vint v) = load Mint32 m heap (signed (sub b four)) ->
  Kind_header v = KIND_CLOSURE -> 
  (Size_header v = zero -> False) ->
  forall l,
  pointer_list b (sub (add b (Size_header v)) four) l ->
  pointer_list_block l.

Hint Constructors pointer_list_block.

Lemma pointer_list_block_func : forall l1, pointer_list_block l1 -> forall l2, pointer_list_block l2 ->
l1 = l2.
Proof.
inversion 1 as [v Hv Hk | v Hv Hk m1 Hm1 | v Hv Hk Hs m2 Hm2]; subst;
inversion 1 as [v' Hv' Hk' | v' Hv' Hk' m1' Hm1' | v' Hv' Hk' Hs' m2' Hm2']; subst;
auto ; replace v' with v in * ; try congruence.
destruct (kind_rawdata_neq_ptrdata); congruence.
destruct (kind_closure_neq_rawdata); congruence.
destruct (kind_rawdata_neq_ptrdata); congruence.
eapply pointer_list_func; eauto.
destruct (kind_ptrdata_neq_closure); congruence.
destruct (kind_closure_neq_rawdata); congruence.
destruct (kind_ptrdata_neq_closure); congruence.
eapply pointer_list_func; eauto.
Qed.

Inductive pointer_list_block_desc : Prop := 
| pointer_list_block_desc_rawdata : forall v, Some (Vint v) = load Mint32 m heap (signed (sub b four)) ->
  Kind_header v = KIND_RAWDATA -> pointer_list_block_desc
| pointer_list_block_desc_ptrdata : forall v, Some (Vint v) = load Mint32 m heap (signed (sub b four)) ->
  Kind_header v = KIND_PTRDATA ->
  pointer_list_desc (sub b four) (sub (add b (Size_header v)) four) ->
  pointer_list_block_desc
| pointer_list_block_desc_closure : forall v, Some (Vint v) = load Mint32 m heap (signed (sub b four)) ->
  Kind_header v = KIND_CLOSURE ->
  (Size_header v = zero -> False) -> 
  pointer_list_desc b (sub (add b (Size_header v)) four) ->
  pointer_list_block_desc.

Hint Constructors pointer_list_block_desc.

Lemma pointer_list_block_describes : forall l,
pointer_list_block l -> pointer_list_block_desc.
Proof.
induction 1; eauto.
Qed.

Lemma pointer_list_block_desc_exists : pointer_list_block_desc ->
exists l, pointer_list_block l.
Proof.
induction 1; eauto.
destruct (pointer_list_desc_exists H1) as [x Hx];exists x; eauto.
destruct (pointer_list_desc_exists H2) as [x Hx];exists x; eauto.
Qed.

(* This lemma is important. It allows "hiding" the list in Prop. *)

Lemma construct_pointer_list_block : 
pointer_list_block_desc -> {pl | pointer_list_block pl}.
Proof.
intro Hptr.
case_eq (load Mint32 m heap (signed (sub b four))).
intros v Hv.
destruct v; try (
 apply False_rect; inversion Hptr; discr
).
destruct (eq_dec (Kind_header i) KIND_RAWDATA).
exists (nil (A := option (block * int))).
eapply pointer_list_block_rawdata.
eauto.
assumption.
destruct (eq_dec (Kind_header i) KIND_PTRDATA).
assert (pointer_list_desc (sub b four) (sub (add b (Size_header i)) four)).
inversion Hptr; try congruence.
destruct kind_ptrdata_neq_closure; congruence.
destruct (construct_pointer_list H).
exists x.
eapply pointer_list_block_ptrdata.
eauto.
assumption.
assumption.
assert (
  pointer_list_desc b (sub (add b (Size_header i)) four) ).
inversion Hptr; try congruence.
destruct (construct_pointer_list H).
exists x.
inversion Hptr; try congruence.
eapply pointer_list_block_closure; eauto.
congruence.
intros.
apply False_rect.
inversion Hptr; discr.
Defined.

End Pointer_list_block.

Inductive good_pointers_from_block_list l : Prop :=
| good_pointers_from_block_list_intro :
   (forall b i, member (b, i) l -> pointer_list_block_desc b i) ->
   (forall b i, member (b, i) l -> forall pl, pointer_list_block b i pl ->
     forall p q, member (Some (p, q)) pl -> member (p, q) l) ->
   good_pointers_from_block_list l.

Inductive good_pointers_from_to heap n p : Prop :=
| good_pointers_from_to_intro : (forall l, block_description_from_to m heap n p l ->
  good_pointers_from_block_list (map (fun i => (heap, i)) l)) ->
  @good_pointers_from_to heap n p.

Hint Constructors good_pointers_from_block_list good_pointers_from_to.

Lemma good_pointers_from_to_intro_weak heap n p :
forall l, block_description_from_to m heap n p l ->
good_pointers_from_block_list (map (fun i => (heap, i)) l) ->
good_pointers_from_to heap n p.
Proof.
intros.
apply good_pointers_from_to_intro.
intros.
rewrite (block_description_from_to_func H1 H).
assumption.
Qed.

Hint Resolve good_pointers_from_to_intro_weak.

Theorem children_strong : forall l, (forall b i, member (b, i) l -> pointer_list_block_desc b i) ->
{c | forall b i, member (b, i) l -> pointer_list_block b i (c (b, i))}.
intros l H.
refine (exist _ (fun bi : block * int =>
let (b, i) := bi in
match member_dec eq_ptr l (b, i)
with 
left m0 => match construct_pointer_list_block (H _ _ m0)
with exist l _ => l end
| _ => nil
end) _).
intros b i Hbi.
destruct (member_dec eq_ptr l (b, i)).
destruct (construct_pointer_list_block (H _  _ m0)).
auto.
contradiction.
Defined.

End Pointers.

Section Roots.
Variable m : mem.

(*
Inductive chain : int -> list int -> Prop :=
| chain_nil : forall r, r = zero -> chain r nil
| chain_cons : forall r, (r = zero -> False) ->
forall v, Some v = get_int32 r m -> forall l, chain v l -> chain r (r::l).

Hint Constructors chain.
*)

Section All_roots.

Section Root_list.

Variable r : block.

Inductive root_list : int -> int -> list (option (block * int)) -> Prop :=
| root_list_zero : forall n, n = zero -> forall i, root_list n i nil
| root_list_nonzero : forall n, (n = zero -> False) ->
  forall i, cmp Cle (sub i four) i = true ->
  forall bv, Some bv = load Mint32 m r (signed i) ->
  forall bv', val_is_pointer_or_dumb bv bv' ->
  forall l, root_list (sub n one) (add i four) l ->
  root_list n i (bv'::l).

Lemma root_list_func : forall n i l, root_list n i l ->
forall l2, root_list n i l2 -> l = l2.
Proof.
induction 1; inversion 1; try congruence.
subst; f_equal; eauto.
replace bv0 with bv in *; try congruence; eauto.
Qed.

Inductive root_list_desc : int -> int -> Prop :=
| root_list_desc_zero : forall n, n = zero -> forall i, root_list_desc n i
| root_list_desc_nonzero : forall n, (n = zero -> False) ->
  forall i, cmp Cle (sub i four) i = true ->
  forall vb, Some vb = load Mint32 m r (signed i) ->
  val_is_pointer_or_dumb_desc vb ->
  root_list_desc (sub n one) (add i four) ->
  root_list_desc n i.

Hint Constructors root_list_desc root_list.

Lemma root_list_describes : forall n i l, root_list n i l -> root_list_desc n i.
Proof.
induction 1; eauto.
Qed.

Hint Resolve root_list_describes.

Lemma root_list_desc_exists : forall n i, root_list_desc n i -> exists l,
root_list n i l.
Proof.
induction 1; eauto ; inversion IHroot_list_desc as [l0 Hl0].
destruct (construct_val_is_pointer_or_dumb H2) as [v Hv].
exists (v :: l0); eauto.
Qed.


Section Root_list_loop.

(*
Let body (a : (int * int) * list int) :=
let (ni, l) := a in
let (n, i) := ni in
if eq_dec n zero
then (false, a)
else match get_int32 i m with
| Some v => (true, ((sub n one, add i four), if eq_dec v zero then l else l ++ (v :: nil)))
| None => (false, a)
end.

Let body_extensive : forall ni l ni' l' b, body (ni, l) = (b, (ni', l')) ->
exists l'', l' = l ++ l''.
unfold body.
introvars.
destruct ni as [n i].
case (eq_dec n zero).
injection 2.
intros; subst.
exists (nil (A := int)).
apply app_nil_end.
case (get_int32 i m).
intros i0.
case (eq_dec i0 zero).
injection 3.
intros; subst.
exists (nil (A := int)).
apply app_nil_end.
injection 3.
intros ; subst.
exists (i0 :: nil).
auto.
injection 2.
intros ; subst.
exists (nil (A := int)).
apply app_nil_end.
Qed.

Corollary loop_extensive :  forall a a', loop_prop body a a' -> 
forall n l, a = (n, l) -> forall n' l', a' = (n', l') ->
exists l'', l' = l ++ l''.
induction 1.
destruct a.
destruct a'.
generalize (body_extensive H).
intros [l'' Hl''].
injection 1.
injection 3.
intros.
subst.
subst.
exists l''; auto.

destruct a.
destruct a'.
generalize (body_extensive H).
intros [l'' Hl''].
subst.
injection 1.
intros.
subst.
generalize (IHloop_prop _ _ (refl_equal _) _ _ (refl_equal _)).
intros [l''0 Hl''0].
subst.
exists (l'' ++ l''0).
apply app_ass.
Qed.

Let loop_correct : forall a a', loop_prop body a a' ->
forall n i l, a =((n, i), l) -> forall ni' l', a' = (ni', l') -> 
root_list_desc n i -> 
forall l'', l' = l ++ l'' ->
root_list n i l''.
induction 1.
introvars.
intro.
subst.
introvars.
intro.
subst.
intro Hex.
genclear H.
unfold body.
case (eq_dec n zero).
intro.
injection 1.
intro; subst.
intro ; subst.
intros l'' Hl''.
generalize (app_fix_left Hl'').
intro; subst l''.
apply root_list_zero.
auto.
intro.
generalize (root_list_desc_exists Hex).
intros [? H]. 
inversion H.
contradiction.
subst.
rewrite <- H2.
discriminate 1.
subst.
rewrite <- H2.
discriminate 1.

introvars.
intro.
subst.
introvars.
intro.
subst.
intro Hex.
genclear H.
unfold body.
case (eq_dec n zero).
discriminate 2.
intro.
generalize (root_list_desc_exists Hex).
intros [? H]. 
inversion H.
contradiction.
subst.
rewrite <- H3.
destruct (eq_dec v zero).
contradiction.
injection 1.
intro ; subst.
generalize (loop_extensive H0 (refl_equal _) (refl_equal _)).
intros [l'' Hl''].
subst l'.
intros l''0.
rewrite app_ass.
simpl.
intro Hl''0.
generalize (app_reg_l Hl''0).
clear Hl''0.
intro.
subst.
eapply root_list_nonzero_normal_root; auto.
eapply IHloop_prop.
reflexivity.
reflexivity.
eauto.
auto.

subst.
rewrite <- H3.
case (eq_dec zero zero).
intros _.
injection 1.
intro.
subst.
intros l'' Hl''.
subst.
eapply root_list_nonzero_dumb_root; auto.
eapply IHloop_prop.
reflexivity.
reflexivity.
eauto.
auto.
intro; contradiction (refl_equal zero).
Qed.

Let loop_terminates : forall n i, root_list_desc n i ->
forall l0, loop_term body ((n, i), l0).
intros n i Hdesc.
induction Hdesc.
intros.
eapply loop_term_interrupt.
unfold body.
case (eq_dec n zero).
intros _ ; reflexivity.
intros ; contradiction.
intros l0.
eapply loop_term_continue.
unfold body.
case (eq_dec n zero).
intros ; contradiction.
intros _.
rewrite <- H1.
reflexivity.
auto.

intros l0.
eapply loop_term_continue.
unfold body.
case (eq_dec n zero).
intros ; contradiction.
intros _.
rewrite <- H1.
reflexivity.
auto.
Qed.

*)
Theorem construct_root_list : forall n i,
root_list_desc n i ->
{l | root_list n i l}.
Admitted.
(*

Proof.
intros n i Hex.
generalize (loop (loop_terminates Hex nil)).
intros [[ni l'] Hl].
generalize (loop_correct Hl (refl_equal _) (refl_equal _) Hex (refl_equal _)).
intros ; exists l'; auto.
Defined.
*)

End Root_list_loop.

End Root_list.

Hint Constructors root_list root_list_desc.
Hint Resolve root_list_describes.

Inductive all_roots : val -> list (list (option (block * int))) -> Prop :=
| all_roots_zero : all_roots (Vint zero) nil
| all_roots_nonzero : forall r d,
  cmp Cle d (add d four) = true ->
  forall n, Some (Vint n) = load Mint32 m r (signed (add d four)) ->
  forall l, root_list r n (add (add d four) four) l ->
  forall v', Some v' = load Mint32 m r (signed d) ->
    forall l', all_roots v' l' ->
  all_roots (Vptr r d) (l :: l').

Lemma all_roots_func : forall v l, all_roots v l ->
forall l2, all_roots v l2 -> l = l2.
Proof.
induction 1.
inversion 1.
auto.
inversion 1.
subst.
f_equal.
eapply root_list_func ; eauto.
congruence.
eapply IHall_roots; eauto.
congruence.
Qed.

Hint Constructors all_roots.

Inductive all_roots_desc : val -> Prop :=
| all_roots_desc_zero : all_roots_desc (Vint zero)
| all_roots_desc_nonzero : forall r d,
  cmp Cle d (add d four) = true ->
  forall n, Some (Vint n) = load Mint32 m r (signed (add d four)) ->
  root_list_desc r n (add (add d four) four) ->
  forall v', Some v' = load Mint32 m r (signed d) ->
    all_roots_desc v' ->
  all_roots_desc (Vptr r d).

Hint Constructors all_roots_desc.

Lemma all_roots_describes : forall v l, all_roots v l -> all_roots_desc v.
induction 1; eauto.
Qed.

Section All_roots_loop.

(*
Let all_roots_succ : forall r, 
all_roots_desc r ->
(r = zero -> False) -> {r' |
prod (Some r' = get_int32 r m) 
(all_roots_desc r')}.
Proof.
intros r Hex Hnz.
case_eq (get_int32 r m).
intros r' Hr'.
exists r'.
split.
trivial.
inversion Hex.
contradiction.
subst.
congruence.
intro Habs.
apply False_rect.
inversion Hex.
contradiction.
discr.
Defined.

Let all_roots_root_list : forall r,
(all_roots_desc r) ->
(r = zero -> False) ->
{l | root_list r l}.
Proof.
intros.
eapply construct_root_list.
inversion H.
contradiction.
subst.
auto.
Defined.

Let body (a : (list int * {r | all_roots_desc r})) :=
match a with
| pair l0 rH =>
  match rH with
  | exist r Hr =>
    match eq_dec r zero with
    | left _ => (false, a)
    | right Hnz =>
      match all_roots_root_list Hr Hnz with
      | exist l _ =>
        match all_roots_succ Hr Hnz with
        | exist r' Hr'0 =>
          match Hr'0 with
          | pair _ Hr' => (true, pair (l0 ++ l) (exist _ r' Hr'))
          end
        end
      end
    end
  end
end.

Let body_extensive : forall l0 r0 b l' r'0,
body (pair l0 r0) = (b, pair l' r'0) ->
exists l'', l' = l0 ++ l''.
Proof.
unfold body.
introvars.
destruct r0 as [r Hr].
case (eq_dec r zero).
intro Hzero.
injection 1.
intros ; subst.
exists (nil (A := int)).
apply app_nil_end.
intro Hnz.
destruct (all_roots_root_list Hr Hnz) as [l Hl].
destruct (all_roots_succ Hr Hnz) as [r' [Hr'_def Hr']].
injection 1.
intros ; subst.
exists l; auto.
Qed.

Let loop_extensive : forall a a', loop_prop body a a' ->
forall l0 r0, a = pair l0 r0 ->
forall l' r'0, a' = pair l' r'0 ->
exists l'', l' = l0 ++ l''.
Proof.
induction 1.
introvars.
intro.
subst.
introvars.
intro.
subst.
generalize (body_extensive H).
intros [l'' Hl''].
subst.
exists l''; auto.

introvars.
intro.
subst.
introvars.
intro.
subst.
destruct a' as [l'0 Hl'0].
generalize (body_extensive H).
intros [l'' Hl''].
subst.
generalize (IHloop_prop _ _ (refl_equal _) _ _ (refl_equal _)).
intros [l''0 Hl''0].
subst.
exists (l'' ++ l''0).
apply app_ass.
Qed.

Let loop_correct : forall a a', loop_prop body a a' ->
forall l r Hr,  a = pair l (exist _ r Hr) ->
forall l' r'H', a' = pair l' r'H' ->
forall l'', l' = l ++ l'' ->
all_roots r l''.
Proof.
induction 1.
introvars.
intro.
subst.
introvars.
intro.
subst.
genclear H.
unfold body.
case (eq_dec r zero).
intro Hz.
injection 1.
intro ; subst.
intro ; subst.
intros l'' Hl''.
generalize (app_fix_left Hl'').
intro ; subst l''.
apply all_roots_zero.
auto.
intro Hnz.
destruct (all_roots_root_list Hr Hnz) as [l0 Hl0].
destruct (all_roots_succ Hr Hnz) as [r' [Hr'_def Hr']].
discriminate 1.


introvars.
intro.
subst.
introvars.
intro.
subst.
genclear H.
unfold body.
case (eq_dec r zero).
intro Hz.
discriminate 1.
intro Hnz.
destruct (all_roots_root_list Hr Hnz) as [l0 Hl0].
destruct (all_roots_succ Hr Hnz) as [r' [Hr'_def Hr']].
injection 1.
intro.
subst.
generalize (loop_extensive H0 (refl_equal _) (refl_equal _)).
intros [l'' Hl''].
subst.
intros l''0.
rewrite app_ass.
intro Hl''0.
generalize (app_reg_l Hl''0).
intro.
subst.
eapply all_roots_nonzero.
assumption.
assumption.
eassumption.
generalize (IHloop_prop _ _ _ (refl_equal _) _ _ (refl_equal _)).
intro IH.
generalize (IH _ (refl_equal _)).
auto.
Qed.

Let loop_terminates : forall a, loop_term body a.
Proof.
destruct a as [l0 [r Hr]].
genclear l0.
generalize Hr.
induction Hr.
intros Hr0 l0.
eapply loop_term_interrupt.
unfold body.
case (eq_dec r zero).
intros _ ; reflexivity.
intro ; contradiction.
intros Hr0 l0.
case_eq (eq_dec r zero).
intro ; contradiction.
intros Hnz HHnz.
case_eq (all_roots_root_list Hr0 Hnz).
intros l1 Hl1 HHl1.
case_eq (all_roots_succ Hr0 Hnz).
intros r'0 [Hr'0_def Hr'0] HHr'0.
eapply loop_term_continue.
unfold body.
rewrite HHnz.
rewrite HHl1.
rewrite HHr'0.
reflexivity.
replace r' with r'0 in IHHr; [ | congruence].
eapply IHHr.
Qed.
*)

Theorem construct_all_roots : forall v,
(all_roots_desc v) -> {l | all_roots v l}.
Admitted.
(*
Proof.
intros r Hr.
generalize (loop (loop_terminates (pair nil (exist _ r Hr)))).
intros [[l [? ?]] Hl].
exists l.
eapply loop_correct.
eassumption.
reflexivity.
reflexivity.
reflexivity.
Defined.
*)

End All_roots_loop.

Inductive root_list_position_list : block -> int -> int -> list (block * int) -> Prop :=
| root_list_pl_zero : forall n, n = zero -> forall r i, root_list_position_list r n i nil
| root_list_pl_nonzero : forall n, (n = zero -> False) ->
  forall i, cmp Cle (sub i four) i = true ->
  forall r l, root_list_position_list r (sub n one) (add i four) l ->
  root_list_position_list r n i ((r, i)::l).

Inductive root_position_list : val -> list (list (block * int)) -> Prop :=
| root_pl_zero : root_position_list (Vint zero) nil
| root_pl_nonzero : forall r i,
  cmp Cle i (add i four) = true ->
  forall n, Some (Vint n) = load Mint32 m r (signed (add i four)) ->
  forall l, root_list_position_list r n (add (add i four) four) l ->
  forall v', Some v' = load Mint32 m r (signed i) ->
  forall l', root_position_list v' l' ->
  root_position_list (Vptr r i) (((r, i) :: (r, add i four) :: l) :: l').

Hint Constructors root_list_position_list root_position_list.

Lemma root_list_position_list_func : forall r n i l, root_list_position_list r n i l ->
forall l', root_list_position_list r n i l' -> l = l'.
Proof.
induction 1; inversion 1; try congruence; f_equal; subst; eauto.
Qed.

Lemma root_list_position_list_n_inj : forall r n i l,root_list_position_list r n i l ->
forall n', root_list_position_list r n' i l -> n = n'.
Proof.
induction 1.
 inversion 1.
 congruence.
inversion 1.
subst.
apply add_reg_r with (neg one).
rewrite <- sub_add_opp.
rewrite <- sub_add_opp.
eauto.
Qed.

Lemma root_position_list_func : forall v l, root_position_list v l ->
forall l', root_position_list v l' -> l = l'.
Proof.
induction 1; inversion 1; try congruence.
subst.
f_equal.
 f_equal.
 f_equal.
 eapply root_list_position_list_func; eauto.
 congruence.
eapply IHroot_position_list; eauto.
congruence.
Qed.

Lemma root_list_desc_root_position_list : forall r n i, root_list_desc r n i ->
exists l, root_list_position_list r n i l.
Proof.
induction 1.
exists (@nil (block * int)); eauto.
 inversion IHroot_list_desc as [l Hl].
 exists ((r, i)::l); eauto.
Qed.

Lemma all_roots_desc_root_position_list : forall v, all_roots_desc v ->
exists l, root_position_list v l.
Proof.
induction 1.
exists (@nil (list (block * int))); eauto.
inversion IHall_roots_desc as [l' Hl'].
generalize (root_list_desc_root_position_list H1).
intros [l Hl].
exists (((r, d) :: (r, add d four) :: l) :: l'); eauto.
Qed.

Lemma root_list_desc_root_position_list_constr : forall r n i, root_list_desc r n i ->
{l | root_list_position_list r n i l}.
Admitted.

Lemma all_roots_desc_root_position_list_constr : forall v, all_roots_desc v ->
{l | root_position_list v l}.
Admitted.

End All_roots.

End Roots.

Section Data_at_rootpos.

Lemma root_list_root_position_list_value_prop :
forall m r n i, root_list_desc m r n i ->
forall lp, root_list_position_list r n i lp ->
forall b j, member (b, j) lp -> exists v, Some v = load Mint32 m b (signed j).
Proof.
induction 1.
subst.
inversion 1.
inversion 1.
congruence.
inversion 1.
contradiction.
subst.
inversion 1.
subst.
eapply ex_intro; eauto.
subst.
eauto.
Qed.

Corollary root_list_root_position_list_value :
forall m r n i, root_list_desc m r n i ->
forall lp, root_list_position_list r n i lp ->
forall b j, member (b, j) lp -> {v | Some v = load Mint32 m b (signed j)}.
Proof.
intros m r n i Hl lp Hlp b j Hb.
case_eq (load Mint32 m b (signed j)).
intros; eapply exist; eauto.
intro.
eapply False_rect.
destruct (root_list_root_position_list_value_prop Hl Hlp Hb).
discr.
Defined.

Lemma all_roots_root_position_list_value_prop :
forall m rd, all_roots_desc m rd ->
forall lp, root_position_list m rd lp ->
forall b j, member (b, j) (flatten lp) -> exists v, Some v = load Mint32 m b (signed j).
Proof.
induction 1.
inversion 1.
inversion 1.
inversion 1.
subst.
unfold flatten.
intros b j Hb.
destruct (member_or Hb) as [ Hb' | ].
inversion Hb' as [ | ? Hb''].
subst.
eapply ex_intro; eauto.
subst.
inversion Hb''.
subst.
eapply ex_intro; eauto.
subst.
eapply root_list_root_position_list_value_prop; try eassumption.
congruence.
subst.
eapply IHall_roots_desc; try eassumption.
congruence.
Qed.

Corollary all_roots_root_position_list_value :
forall m rd, all_roots_desc m rd ->
forall lp, root_position_list m rd lp ->
forall b j, member (b, j) (flatten lp) -> {v | Some v = load Mint32 m b (signed j)}.
Proof.
intros m rd Hrd lp Hlp b j Hbj.
case_eq (load Mint32 m b (signed j)).
intros; eapply exist; eauto.
intro; eapply False_rect.
destruct (all_roots_root_position_list_value_prop Hrd Hlp Hbj).
discr.
Defined.

End Data_at_rootpos.

Section Invariant_positions.

Lemma root_list_invar : forall m r n i l, root_list m r n i l ->
forall lp, root_list_position_list r n i lp ->
forall m',
(forall b i, member (b, i) lp -> load Mint32 m b (signed i) = load Mint32 m' b (signed i)) ->
root_list m' r n i l.
Proof.
induction 1.
intros; eapply root_list_zero; eauto.

intros.
inversion H4.
contradiction.
subst.
eapply root_list_nonzero; auto.
eapply trans_equal.
eexact H1.
apply H5.
auto.
assumption.
eapply IHroot_list.
eassumption.
intros ? ? ?.
apply H5.
auto.
Qed.


Lemma root_position_list_invar : forall m v l, root_position_list m v l ->
forall m',
(forall b i, member (b, i) (flatten l) -> load Mint32 m b (signed i) = load Mint32 m' b (signed i)) ->
root_position_list m' v l.
Proof.
induction 1.
intros.
eapply root_pl_zero; eauto.
intros.
eapply root_pl_nonzero; eauto.
rewrite H0.
apply H4.
simpl.
auto.
transitivity (Some v').
reflexivity.
rewrite H2.
apply H4.
simpl.
auto.
eapply IHroot_position_list.
intros b i0 Hb.
apply H4.
unfold flatten.
eapply member_app_right; eauto.
Qed.

Lemma all_roots_invar : forall m v l, all_roots m v l ->
forall lp, root_position_list m v lp ->
forall m',
(forall b i, member (b, i) (flatten lp) -> load Mint32 m b (signed i) = load Mint32 m' b (signed i)) ->
all_roots m' v l.
Proof.
induction 1.
intros; eapply all_roots_zero; eauto.
intros lp Hlp m' Hm'.
inversion Hlp.
subst.
eapply all_roots_nonzero.
assumption.
eapply trans_equal.
eexact H0.
apply Hm'.
simpl; auto.
eapply root_list_invar.
eassumption.
replace n0 with n in *; [|congruence].
eassumption.
intros b i Hb.
apply Hm'.
unfold flatten; eapply member_app_left; eauto.
eapply trans_equal.
eexact H2.
apply Hm'.
simpl; auto.
replace v'0 with v' in *; [|congruence].
eapply IHall_roots.
eassumption.
intros b i Hb.
apply Hm'.
unfold flatten; eapply member_app_right; eauto.
Qed.

Corollary all_roots_invar_recip : forall m v l, all_roots m v l ->
forall m' lp, root_position_list m' v lp ->
(forall b i, member (b, i) (flatten lp) -> load Mint32 m b (signed i) = load Mint32 m' b (signed i)) ->
all_roots m' v l.
Proof.
intros.
eapply all_roots_invar.
eassumption.
eapply root_position_list_invar.
eassumption.
intros; symmetry; eauto.
assumption.
Qed.

End Invariant_positions.

Section Invariant_values_at_positions.

Lemma root_list_position_list_values_invar : forall r n i lp, root_list_position_list r n i lp ->
forall m l, root_list m r n i l ->
forall m', root_list m' r n i l ->
forall b i, member (b, i) lp -> load Mint32 m b (signed i) = load Mint32 m' b (signed i).

Proof.
induction 1.
 inversion 3.
simple inversion 1; subst.
 contradiction.
intros until 3.
intro Hbv.
inversion 2.
subst.
inversion 1.
 subst.
 generalize (val_is_pointer_or_dumb_inj Hbv).
 clear Hbv.
 intros Heq.
 match goal with Hv : val_is_pointer_or_dumb _ _ |- _ =>
   generalize (Heq _ Hv) end.
 intros ; congruence.
subst.
eauto.
Qed.

Lemma root_list_n_inj : forall m r n i l, root_list m r n i l ->
forall m' n2, root_list m' r n2 i l -> n = n2.
Proof.
induction 1.
 inversion 1.
 congruence.
inversion 1.
 subst.
 apply add_reg_r with (neg one).
 rewrite <- sub_add_opp.
 rewrite <- sub_add_opp.
 eauto.
Qed.

Lemma root_position_list_values_invar : 
  forall m v l, all_roots m v l ->
    forall lp, root_position_list m v lp ->
      forall m',  all_roots m' v l ->
        root_position_list m' v lp ->
        forall b i, member (b, i) (flatten lp) -> load Mint32 m b (signed i) = load Mint32 m' b (signed i).

Proof.
induction 1.
 inversion 1.
 inversion 2.
inversion 1.
subst.
inversion 1.
subst.
inversion 1.
subst.
generalize (root_list_n_inj H1 H17).
intro; subst.
inversion 1.
subst.
generalize (root_list_position_list_n_inj H9 H23).
intro; subst.
replace v'1 with v' in *.
 unfold flatten.
 intros b i Hbi.
 generalize (member_or Hbi).
 clear Hbi.
 intro Hbi.
 inversion Hbi as [Hbi_left | Hbi_right].
  inversion Hbi_left.
   subst.
   congruence.
  subst. 
  inversion H13.
   subst.
   congruence.
  subst.
  eapply root_list_position_list_values_invar.
     eassumption.
    replace n with n1 in *.
     eassumption.
    congruence.
   congruence.
  assumption.
 eapply IHall_roots.
    replace v' with v'0.
     eassumption.
    congruence.
   assumption.
  replace v' with v'2.
   eassumption.
  congruence.
 assumption. 
inversion H12.
 subst.
 inversion H25.
 subst.
 congruence.
subst. 
inversion H25.
subst.
congruence.
Qed.

End  Invariant_values_at_positions.


Section Path.

Record path : Set := mkPath {
 root_list_number : nat;
 root_number : nat;
 pointer_chain : list nat
}.

Section Realize_path.

Variable m : mem.

Inductive find_root_list : nat -> block -> int -> block -> int -> Prop :=
| find_root_list_O : forall p q, find_root_list O p q p q
| find_root_list_S : forall b i c j,
  Some (Vptr c j) = load Mint32 m b (signed i) -> forall n d k, find_root_list n c j d k ->
  find_root_list (S n) b i d k.

Hint Constructors find_root_list.

Lemma find_root_list_func : forall n b i d k, find_root_list n b i d k ->
forall d2 k2, find_root_list n b i d2 k2 -> (d = d2 /\ k = k2).
Proof.
induction 1.
inversion 1.
auto.
inversion 1.
subst.
eapply IHfind_root_list.
congruence.
Qed.

Lemma find_root_list_thm_recip : forall n b i d k, find_root_list n b i d k ->
forall l, all_roots m (Vptr b i) l ->
exists lk, find_in_list l n lk /\
exists num, Some (Vint num) = load Mint32 m d (signed (add k four)) /\ root_list m d num (add (add k four) four) lk.
induction 1.
inversion 1.
subst.
esplit.
split.
 eauto.
esplit.
split.
eassumption.
assumption.

inversion 1.
subst.
replace v' with (Vptr c j) in *; [|congruence].
destruct (IHfind_root_list _ H9) as [lk [Hl ?]].
subst.
esplit.
split.
 eauto.
assumption.
Qed.

Lemma find_root_list_thm : forall l n lk, find_in_list l n lk -> forall b i,
  all_roots m (Vptr b i) l ->
exists d, exists k, find_root_list n b i d k /\ 
exists num, Some (Vint num) = load Mint32 m d (signed (add k four)) /\ root_list m d num (add (add k four) four) lk.
Proof.
induction 1.
 inversion 1.
 subst.
 esplit.
 esplit.
 split.
  eauto.
 esplit.
 split.
  eassumption.
 assumption.
inversion 1.
subst.
inversion H9.
 subst.
 inversion H.
subst.
generalize (IHfind_in_list _ _ H9).
intros [d0 [k [Hd0k ?]]].
esplit.
esplit.
split; try eassumption.
eauto.
Qed.

Lemma find_root_list_root_position_list_thm : forall n b i d k, find_root_list n b i d k ->
forall l, root_position_list m (Vptr b i) l -> exists lk,
find_in_list l n ((d, k) :: (d, add k four) :: lk) /\
forall v, Some (Vint v) = load Mint32 m d (signed (add k four)) ->
root_list_position_list d v (add (add k four) four) lk.
Proof.
induction 1.
inversion 1.
subst.
exists l0.
split.
auto.
intros; congruence.

inversion 1.
subst.
replace v' with (Vptr c j) in *; [|congruence].
destruct (IHfind_root_list _ H9) as [lk [Hl Hpl]].
subst.
exists lk.
split.
auto.
auto.
Qed.

Inductive find_root : nat -> int -> block -> int -> option (block * int) -> Prop :=
| find_root_number_O : forall n, (n = zero -> False) ->
  forall r d pv, Some pv = load Mint32 m r (signed d) ->
    forall v, val_is_pointer_or_dumb pv v ->
  find_root O n r d v
| find_root_number_S : forall n, (n = zero -> False) ->
  forall k r d pv, find_root k (sub n one) r (add d four) pv ->
  find_root (S k) n r d pv.

Lemma find_root_func : forall k n r d pv, find_root k n r d pv ->
forall p2v2, find_root k n r d p2v2 -> (pv = p2v2).
Proof.
induction 1.
inversion 1.
subst; eauto.
replace pv0 with pv in *; try congruence; eauto.
inversion 1.
subst.
eapply IHfind_root; congruence.
Qed.

Lemma find_root_thm : forall n r d l,
root_list m r n d l ->
forall bi k, find_in_list l k bi ->
find_root k n r d bi.
Proof.
induction 1.
inversion 1.
inversion 1.
subst.
eapply find_root_number_O.
assumption.
eassumption.
assumption.
subst.
generalize (IHroot_list _ _ H9).
intros Hk.
apply find_root_number_S.
assumption.
assumption.
Qed.

Lemma find_root_thm_recip : forall k n r d pv,
find_root k n r d pv -> forall l,
root_list m r n d l ->
find_in_list l k pv.
Proof.
induction 1.
inversion 1.
contradiction.
subst.
replace pv with bv in *; [ | congruence].
replace bv' with v in *; eauto.
inversion 1.
contradiction.
subst.
generalize (IHfind_root _ H6).
auto.
Qed.

Section Find_pointer.

Variable b : block.

Section Find_pointer_from.

Variable l : int.

Inductive find_pointer_from : nat -> int -> option (block * int) -> Prop :=
| find_pointer_O : forall i, (i = l -> False) ->
  forall pv, Some pv = load Mint32 m b (signed i) -> 
  forall opv, val_is_pointer_or_dumb pv opv ->
  find_pointer_from O i opv
| find_pointer_S : forall i, (i = l -> False) ->
  forall n pv, find_pointer_from n (sub i four) pv ->
  find_pointer_from (S n) i pv.

Lemma find_pointer_from_func : forall n i pv,
find_pointer_from n i pv -> forall p2v2, find_pointer_from n i p2v2 ->
(pv = p2v2).
Proof.
induction 1; inversion 1; try congruence; subst; eauto.
replace pv with pv0 in *; try congruence; eauto.
Qed.

Lemma find_pointer_from_thm : forall i k,
pointer_list m b l i k ->
forall n pv, find_in_list k n pv ->
find_pointer_from n i pv.
Proof.
induction 1.
 inversion 1.
inversion 1.
 subst.
 eapply find_pointer_O.
   assumption.
  eassumption.
 assumption.
subst.
generalize (IHpointer_list _ _ H8).
intros Hn.
apply find_pointer_S.
 assumption.
assumption.
Qed.

Lemma find_pointer_from_thm_recip :
forall n i pv, find_pointer_from n i pv ->
forall k, pointer_list m b l i k ->
find_in_list k n pv.
Proof.
induction 1.
 inversion 1.
  contradiction.
 subst.
 replace pv with v in *; [|congruence].
 replace opv with p in *; [ |eapply val_is_pointer_or_dumb_func; eauto].
 auto.
inversion 1.
 contradiction.
subst.
apply find_in_list_S.
eapply IHfind_pointer_from.
assumption.
Qed.

End Find_pointer_from.

Inductive find_pointer : nat -> int -> option (block * int) -> Prop :=
| find_pointer_ptrdata : forall i v, Some (Vint v) = load Mint32 m b (signed (sub i four)) ->
  Kind_header v = KIND_PTRDATA ->
  forall n pw, find_pointer_from (sub i four) n (sub (add i (Size_header v)) four) pw ->
  find_pointer n i pw
| find_pointer_closure : forall i v, Some (Vint v) = load Mint32 m b (signed (sub i four)) ->
  Kind_header v = KIND_CLOSURE ->
  forall n pw, find_pointer_from i n (sub (add i (Size_header v)) four) pw ->
  find_pointer n i pw.

Lemma find_pointer_func : forall n i pw, find_pointer n i pw ->
forall p2w2, find_pointer n i p2w2 -> (pw = p2w2).
Proof.
induction 1.
inversion 1.
subst.
eapply find_pointer_from_func; eauto.
congruence.
destruct (kind_ptrdata_neq_closure); congruence.

inversion 1.
destruct (kind_ptrdata_neq_closure); congruence.
eapply find_pointer_from_func; eauto.
congruence.
Qed.

Lemma find_pointer_thm_recip : forall n i pw, find_pointer n i pw ->
forall l, pointer_list_block m b i l -> find_in_list l n pw.
Proof.
induction 1.
inversion 1.
destruct (kind_rawdata_neq_ptrdata); congruence.
subst.
eapply find_pointer_from_thm_recip.
eassumption.
congruence.
destruct (kind_ptrdata_neq_closure); congruence.
inversion 1.
destruct (kind_closure_neq_rawdata); congruence.
destruct (kind_ptrdata_neq_closure); congruence.
eapply find_pointer_from_thm_recip.
eassumption.
congruence.
Qed.

Lemma find_pointer_thm : forall i l, pointer_list_block m b i l ->
  forall n pw, find_in_list l n pw -> find_pointer n i pw.
Proof.
induction 1.
 inversion 1.
intros.
eapply find_pointer_ptrdata.
 eassumption.
 assumption.
 eapply find_pointer_from_thm; eauto.
intros.
eapply find_pointer_closure.
eassumption.
assumption.
eapply find_pointer_from_thm; eauto.
Qed.

End Find_pointer.

Inductive follow_pointer_chain : option (block * int) -> list nat -> option (block * int) -> Prop :=
| follow_pointer_chain_nil : forall bi, follow_pointer_chain bi nil bi
| follow_pointer_chain_cons : forall b n i cj, find_pointer b n i cj ->
  forall l dk, follow_pointer_chain cj l dk -> follow_pointer_chain (Some (b, i)) (n::l) dk.

Hint Constructors follow_pointer_chain.

Lemma follow_pointer_chain_func : forall bi l pv,
follow_pointer_chain bi l pv ->
forall p2v2, follow_pointer_chain bi l p2v2 -> (pv = p2v2).
Proof.
induction 1; inversion 1; eauto.
subst; eapply IHfollow_pointer_chain; eauto.
generalize (find_pointer_func H H7).
intros.
subst; eassumption.
Qed.

Lemma follow_pointer_chain_app_elim : forall l1 bi l2 pv,
follow_pointer_chain bi (l1 ++ l2) pv ->
exists p15v15, (follow_pointer_chain bi l1 p15v15 /\ follow_pointer_chain p15v15 l2 pv).
induction l1; simpl.
intros.
exists bi.
split; auto.
inversion 1.
subst.
generalize (IHl1 _ _ _ H5).
intros [p15v15 [Hleft Hright]].
exists p15v15.
split; eauto.
Qed.

Lemma follow_pointer_chain_app_intro : forall bi l1 p15v15,
follow_pointer_chain bi l1 p15v15 ->
forall l2 pv,
follow_pointer_chain p15v15 l2 pv ->
follow_pointer_chain bi (l1 ++ l2) pv.
Proof.
induction 1; simpl; auto.
intros.
eapply follow_pointer_chain_cons; eauto.
Qed.

Lemma follow_pointer_chain_valid : forall heap n p, good_pointers_from_to m heap n p ->
forall l, block_description_from_to m heap n p l ->
forall bi nl cj, follow_pointer_chain bi nl cj -> (forall b i,
bi = Some (b, i) -> (b = heap /\ member i l)) -> forall c j, cj = Some (c, j) -> (c = heap /\ member j l).
Proof.
introvars.
intros Hgp l Hl.
inversion Hgp as [Hgp1].
generalize (Hgp1 l Hl).
intros [Hgp_wf Hgp_ptr].
induction 1.
auto.
intros Hbi.
apply IHfollow_pointer_chain.
generalize (Hbi _ _ (refl_equal _)).
intros [Hb Hi].
subst.
generalize (member_offset_to_block heap Hi).
intro Hi2.
generalize (Hgp_wf heap i Hi2). 
intro Hdesc_i.
generalize (construct_pointer_list_block Hdesc_i).
intros [pl Hpl].
intros; subst.
generalize (Hgp_ptr _ _ Hi2 _ Hpl _ _ (find_in_list_member (find_pointer_thm_recip H Hpl))).
intros H_3.
split.
eapply member_block; eauto.
eapply member_block_to_offset; eauto.
Qed.

Inductive realize_path :
 val ->
 (path) -> 
 (option (block * int)) ->
 Prop :=
| realize_path_intro : forall r d p qv r0 d0, find_root_list p.(root_list_number) r d r0 d0 ->
  forall n, Some (Vint n) = load Mint32 m r0  (signed (add d0 four)) ->
  forall b0u0, find_root p.(root_number) n r0 (add (add d0 four) four) b0u0 ->
  follow_pointer_chain b0u0 p.(pointer_chain) qv ->
  realize_path (Vptr r d) p qv.

Lemma realize_path_func : forall rd p qv,
realize_path rd p qv -> forall q2v2, realize_path rd p q2v2 -> (qv = q2v2).
Proof.
induction 1; inversion 1.
subst.
eapply follow_pointer_chain_func.
eassumption.
replace b0u0 with b0u1.
  assumption.
eapply find_root_func.
 eassumption.
assert (r0 = r2 /\ d0 = d2). 
 eapply find_root_list_func ; eauto.
invall.
subst.
congruence.
Qed.

Lemma all_roots_thm : forall rd l, all_roots m rd l -> forall bi, member bi (flatten l) ->
exists p, realize_path rd p bi.
Proof.
induction 1.
 inversion 1.
simpl.
intros bi Hbi.
generalize (member_or Hbi).
intros [Hmem | Hmem].
 inversion H1.
  subst.
  inversion Hmem.
 subst.
 generalize (member_find_in_list Hmem).
 intros [n0 Hn0].
 generalize (find_root_thm H1 Hn0).
 intros Hk.
 refine (ex_intro _ (mkPath _ _ _) _).
 eapply realize_path_intro.
    simpl.
    eapply find_root_list_O.
   eassumption.
  simpl.
  eassumption.
 simpl.
 eapply follow_pointer_chain_nil.
subst.
generalize (IHall_roots _ Hmem).
intros [[root_list_num root_num ptr_chain] Hrealize].
inversion Hrealize.
subst.
exists (mkPath (S (root_list_num)) root_num ptr_chain).
eapply realize_path_intro; simpl.
   eapply find_root_list_S; eauto.
  eassumption.
 eassumption.
eassumption.
Qed.


End Realize_path.

Section Invariant_paths.

(*
Inductive find_root_list : nat -> int -> int -> Prop :=
| find_root_list_O : forall i, (i = zero -> False) -> find_root_list O i i
| find_root_list_S : forall i, (i = zero -> False) -> forall j,
  Some j = get_int32 i m -> forall n k, find_root_list n j k -> find_root_list (S n) i k.
*)

Lemma find_root_list_invar : forall m n r d k e, find_root_list m n r d k e ->
forall l, root_position_list m (Vptr r d) l ->
forall m',
(forall b i, member (b, i) (flatten l) -> 
load Mint32 m b (signed i) = load Mint32 m' b (signed i)) ->
find_root_list m' n r d k e.
Proof.
induction 1.
 intros; eapply find_root_list_O; eauto.
intros l Hl m' Hm'.
eapply find_root_list_S.
 eapply trans_equal.
  eexact H.
 apply Hm'.
 inversion Hl.
 simpl; auto.
inversion Hl.
subst.
eapply IHfind_root_list with l'.
 congruence.
intros; eapply Hm'; eauto.
unfold flatten; eapply member_app_right; eauto.
Qed.

Corollary find_root_list_invar_recip : forall m n r d k e, find_root_list m n r d k e ->
forall m' l, root_position_list m' (Vptr r d) l ->
(forall b i, member (b, i) (flatten l) -> 
load Mint32 m' b (signed i) = load Mint32 m b (signed i)) ->
find_root_list m' n r d k e.
Proof.
intros.
eapply find_root_list_invar.
eassumption.
eapply root_position_list_invar.
eassumption.
intros; eauto.
intros; symmetry; eauto.
Qed.

Lemma find_root_invar : forall m n r k i sj, find_root m n k r i sj ->
forall l, root_list_position_list r k i l ->
forall m',
(forall b i, member (b, i) l -> 
load Mint32 m b (signed i) = load Mint32 m' b (signed i)) ->
find_root m' n k r i sj.
Proof.
induction 1.
 intros; eapply find_root_number_O; eauto.
 rewrite H0.
 eapply H3; eauto.
 inversion H2.
  contradiction.
 auto.
intros.
eapply find_root_number_S.
 assumption.
inversion H1.
 contradiction.
subst.
eapply IHfind_root.
 eassumption.
intros; eapply H2.
apply member_tail; eassumption.
Qed.

Section Invariant_chain.

Variable m : mem.
Variable heap : block.

Variable m' : mem.

Lemma find_pointer_from_invar : forall until n i pk, find_pointer_from m heap until n i pk ->
cmp Cle until i = true ->
cmp Cle i (add i three) = true ->
modulo_four i until ->
(forall x, cmp Cle (add until four) x = true -> cmp Cle x i = true -> 
modulo_four x i ->
load Mint32 m heap (signed x) = load Mint32 m' heap (signed x)) ->
find_pointer_from m' heap until n i pk.
Proof.
induction 1.
 intros Hle Hhi Hmod4 Hm'.
 eapply find_pointer_O.
   assumption.
  eapply trans_equal. 
   eexact H0.
  apply Hm'.
    destruct (modulo_four_le_eq_or_next (mod4_sym Hmod4) Hle) as [? | [? [? [? ?]]]].
     congruence.
    assumption.
   auto.
  auto.
 assumption.
intros Hle Hhi Hmod4 Hm'.
eapply find_pointer_S.
 assumption.
destruct (modulo_four_le_eq_or_next (mod4_sym Hmod4) Hle) as [? | [? [? [? ?]]]].
 congruence.
eapply IHfind_pointer_from.
   assumption.
  eapply four_three_left.
  rewrite sub_add_id.
  assumption.
 rewrite <- (sub_zero_l until).
 eapply mod4_sub.
  assumption.
 auto.
intros x xlo xhi x_mod4.
apply Hm'.
  assumption.
 int_le_lt_trans_tac.
 assumption.
eapply mod4_trans.
 eexact x_mod4.
apply modulo_four_four_divides_sub.
unfold four_divides; auto.
Qed.

Lemma pointer_list_invar : forall until i l, pointer_list m heap until i l ->
cmp Cle until i = true ->
cmp Cle i (add i three) = true ->
modulo_four i until ->
(forall x, cmp Cle (add until four) x = true -> cmp Cle x i = true -> modulo_four i x ->
load Mint32 m heap (signed x) = load Mint32 m' heap (signed x)) ->
pointer_list m' heap until i l.
Proof.
induction 1.
 intros Hle Hhi Hmod4 Hm'.
 eapply pointer_list_end.
 assumption.
intros Hle Hhi Hmod4 Hm'.
destruct (modulo_four_le_eq_or_next (mod4_sym Hmod4) Hle) as [? | [? [? [? ?]]]].
 congruence.
eapply pointer_list_cont.
   assumption.
  eapply trans_equal.
   eexact H0.
  apply Hm'.
    assumption.
   auto.
  auto.
 eapply IHpointer_list.
    assumption.
   eapply four_three_left.
   rewrite sub_add_id.
   assumption.
  rewrite <- (sub_zero_l until).
  eapply mod4_sub.
   assumption.
  auto.
 intros x xlo xhi x_mod4.
 apply Hm'.
   assumption.
  int_le_lt_trans_tac.
  assumption.
 eapply mod4_trans.
  apply mod4_sym.
  eapply modulo_four_four_divides_sub.
  apply four_divides_four.
 assumption.
assumption.
Qed.

Lemma pointer_list_invar_by_suffix : forall l s, is_suffix_of s l ->
forall until i, pointer_list m heap until i l ->
pointer_list m' heap until i l ->
forall j, pointer_list m heap until j s ->
pointer_list m' heap until j s.
Proof.
induction 1.
 intros.
 replace j with i; auto.
 eapply pointer_list_i_func.
  eexact H.
  assumption.
inversion 1.
subst.
inversion 1.
subst.
intros.
eapply IHis_suffix_of.
 eassumption.
 eassumption.
 assumption.
Qed.

Variables n p : int.

Variable l : list int.
Hypothesis Hl : block_description_from_to m heap n p l.

Hypothesis Hgp : good_pointers_from_to m heap n p.

Hypothesis Hm'_header : forall b, member b l -> exists v',
Some (Vint v') = load Mint32 m' heap (signed (sub b four)).

Hypothesis Hm'_kind : forall b, member b l ->
forall v, Some (Vint v) = load Mint32 m heap (signed (sub b four)) ->
forall v', Some (Vint v') = load Mint32 m' heap (signed (sub b four)) ->
Kind_header v = Kind_header v'.

Hypothesis Hm'_size : forall b, member b l ->
forall v, Some (Vint v) = load Mint32 m heap (signed (sub b four)) ->
forall v', Some (Vint v') = load Mint32 m' heap (signed (sub b four)) ->
Size_header v = Size_header v'.

Hypothesis Hm'_data : forall b, member b l ->
forall v, Some (Vint v) = load Mint32 m heap (signed (sub b four)) ->
(Size_header v = zero -> False) ->
forall x, cmp Cle b x = true -> cmp Cle x (sub (add b (Size_header v)) four) = true ->
modulo_four b x ->
load Mint32 m heap (signed x) = load Mint32 m' heap (signed x).

Lemma find_pointer_invar : forall b, member b l -> forall n pi, find_pointer m heap n b pi ->
find_pointer m' heap n b pi.
Proof.
intros b Hb.
generalize (Hm'_header Hb).
intros [v' Hv'].
inversion Hgp as [Hgp2].
destruct (Hgp2 _ Hl) as [Hdesc Hptr].
generalize (Hdesc _ _ (member_map Hb (fun i0 => (heap, i0)))).
intro Hdesc_b.
inversion 1.
 subst.
 inversion Hdesc_b.
   destruct (kind_rawdata_neq_ptrdata); congruence.
  replace v0 with v in * ; [| congruence].
  inversion H5.
   subst.
   genclear H6.
   rewrite sub_add_opp.
   rewrite sub_add_opp.
   intro Habs.
   generalize (add_reg_r Habs).
   intro Habs2.
   generalize (add_zero_recip_l Habs2).
   intro Habs3.
   rewrite Habs3 in H2.
   rewrite add_zero in H2.
   inversion H2.
    congruence.
   congruence.
  subst.
  assert (Size_header v = zero -> False) as Hblock_nonempty.
   intro Habs.
   apply H6.
   f_equal.
   rewrite Habs.
   apply add_zero.
  destruct (modulo_four_le_eq_or_next_2 (a := sub b four) (b := add b (Size_header v)))
as [ e | [? [? [? ?]]]].
     eapply mod4_trans.
      apply modulo_four_four_divides_sub.
      unfold four_divides; auto.
     apply modulo_four_four_divides_add.
     eapply four_divides_size_header.
    eapply int_le_trans.
     eapply block_header_end_after_block_start; eauto.
    eapply block_header_end_before_block_end; eauto.
   rewrite sub_add_id in e.
   symmetry in e.
   generalize (add_zero_recip_l e).
   intro; contradiction.
  rewrite sub_add_id in *.
  eapply find_pointer_ptrdata.
    eassumption.
   rewrite <- H1.
   symmetry.
   eapply Hm'_kind; eauto.
  rewrite <- (Hm'_size Hb H0 Hv').
  eapply find_pointer_from_invar.
      assumption.
     assumption.
    rewrite Hcalc.
    assumption.
   apply mod4_sub.
    apply mod4_sym.
    apply modulo_four_four_divides_add.
    eapply four_divides_size_header.
   auto.
  intros x xlo xhi x_mod4.
  eapply Hm'_data.
        eassumption.
       eassumption.
      eassumption.
    rewrite <- (sub_add_id b four).
    assumption.
   assumption.
  apply mod4_sym.
  eapply mod4_trans.
   eassumption.
  eapply mod4_trans.
   eapply modulo_four_four_divides_sub.
   unfold four_divides; eauto.
  apply mod4_sym.
  eapply modulo_four_four_divides_add.
  eapply four_divides_size_header.
 destruct (kind_ptrdata_neq_closure); congruence.
subst.
inversion Hdesc_b.
destruct (kind_closure_neq_rawdata); congruence.
destruct (kind_ptrdata_neq_closure); congruence.
replace v0 with v in * ; [|try congruence].
inversion H6.
subst i.
genclear H7.
rewrite sub_add_opp.
rewrite add_assoc.
intro Habs.
generalize (add_zero_recip_l Habs).
rewrite <- (sub_idem four).
rewrite sub_add_opp.
intro Habs2.
generalize (add_reg_r Habs2).
intro Habs3.
rewrite Habs3 in H2.
rewrite add_sub_id in H2.
inversion H2.
congruence.
congruence.
subst.
assert (Size_header v = four -> False) as Hblock_nonempty.
 intro Habs.
 apply H7.
 pattern b at 2.
 rewrite <- (add_sub_id b four).
 f_equal.
 f_equal.
 assumption.
destruct (modulo_four_le_eq_or_next_2 (a := b) (b := add b (Size_header v)))
as [ e | [? [? [? ?]]]].
   apply modulo_four_four_divides_add.
   eapply four_divides_size_header.
  eapply nonempty_block_right; eauto.
 generalize (add_reg_l e).
 intro; congruence.
eapply find_pointer_closure.
  eassumption.
 rewrite <- H1.
 symmetry.
 eapply Hm'_kind; eauto.
rewrite <- (Hm'_size Hb H0 Hv').
eapply find_pointer_from_invar.
    assumption.
   assumption.
  rewrite Hcalc.
  assumption.
 eapply mod4_trans.
 apply modulo_four_four_divides_sub.
  apply four_divides_four.
 apply mod4_sym.
 apply modulo_four_four_divides_add.
 apply four_divides_size_header.
intros x xlo xhi x_mod4.
eapply Hm'_data.
      eassumption.
    eassumption.
   assumption.
  eapply int_le_trans with (add b four).
   assumption.
  assumption.
 assumption.
apply mod4_sym.
eapply mod4_trans.
 eassumption.
eapply mod4_trans.
 eapply modulo_four_four_divides_sub.
 unfold four_divides; eauto.
apply mod4_sym.
eapply modulo_four_four_divides_add.
eapply four_divides_size_header; eauto.
Qed.

Lemma pointer_list_block_invar :
forall b, member b l -> forall l0, pointer_list_block m heap b l0 ->
pointer_list_block m' heap b l0.
Proof.
intros b Hb.
generalize (Hm'_header Hb).
intros [v' Hv'].

inversion 1.
subst.
eapply pointer_list_block_rawdata.
eassumption.
rewrite <- H1.
symmetry.
eapply Hm'_kind.
eassumption.
assumption.
assumption.

subst.
eapply pointer_list_block_ptrdata.
eassumption.
rewrite <- H1.
symmetry.
eapply Hm'_kind.
eassumption.
assumption.
assumption.
rewrite <- (Hm'_size Hb H0 Hv').
inversion H2.
subst.
eapply pointer_list_end.
assumption.
subst.
assert (Size_header v = zero -> False) as Hblock_nonempty.
 intro Habs.
 apply H3.
 f_equal.
 rewrite Habs.
 apply add_zero.
destruct (modulo_four_le_eq_or_next_2 (a := sub b four) (b := add b (Size_header v)))
as [ e | [? [? [? ?]]]].
eapply mod4_trans.
apply modulo_four_four_divides_sub.
unfold four_divides.
auto.
apply modulo_four_four_divides_add.
eapply four_divides_size_header.
eapply int_le_trans.
eapply block_header_end_after_block_start; eauto.
eapply block_header_end_before_block_end; eauto.
rewrite sub_add_id in e.
symmetry in e.
generalize (add_zero_recip_l e).
intro; contradiction.
rewrite sub_add_id in *.
eapply pointer_list_invar.
assumption.
assumption.
rewrite Hcalc.
assumption.
apply mod4_sub.
apply mod4_sym.
apply modulo_four_four_divides_add.
eapply four_divides_size_header.
auto.
rewrite sub_add_id.
intros x xlo xhi x_mod4.
eapply Hm'_data.
eassumption.
eassumption.
assumption.
assumption.
assumption.
eapply mod4_trans.
eapply modulo_four_four_divides_add.
eapply four_divides_size_header.
eapply mod4_trans.
apply mod4_sym.
eapply modulo_four_four_divides_sub.
apply four_divides_four.
eassumption.

subst.
eapply pointer_list_block_closure.
eassumption.
rewrite <- H1.
symmetry.
eapply Hm'_kind; eauto.
rewrite <- (Hm'_size Hb H0 Hv').
assumption.
rewrite <- (Hm'_size Hb H0 Hv').
inversion H3.
eapply pointer_list_end.
assumption.
subst.
assert (Size_header v = four -> False) as Hblock_nonempty.
 intro Habs.
 apply H4.
 pattern b at 2.
 rewrite <- (add_sub_id b four).
 f_equal.
 f_equal.
 assumption.
destruct (modulo_four_le_eq_or_next_2 (a := b) (b := add b (Size_header v)))
as [ e | [? [? [? ?]]]].
apply modulo_four_four_divides_add.
eapply four_divides_size_header.
eapply nonempty_block_right.
eassumption.
assumption.
assumption.
assumption.

generalize (add_reg_l e).
intro; congruence.
eapply pointer_list_invar.
assumption.
assumption.
rewrite Hcalc.
assumption.
eapply mod4_trans.
apply modulo_four_four_divides_sub.
unfold four_divides.
auto.
apply mod4_sym.
apply modulo_four_four_divides_add.
eapply four_divides_size_header.
intros x xlo xhi x_mod4.
eapply Hm'_data.
eassumption.
eassumption.
assumption.
eapply int_le_trans.
eexact H8.
eassumption.
assumption.
eapply mod4_trans.
eapply modulo_four_four_divides_add.
eapply four_divides_size_header.
eapply mod4_trans.
apply mod4_sym.
eapply modulo_four_four_divides_sub.
apply four_divides_four.
eassumption.
Qed.

Lemma good_pointers_from_to_invar : good_pointers_from_to m' heap n p.
Proof.
assert (block_description_from_to m' heap n p l).
 eapply block_description_samesize_inv.
 eassumption.
 assumption.
 assumption.
 auto.
(* validity *)
intros b Hb v Hv Hnz x Hxmod4 xlo xhi.
generalize (block_description_valid Hl Hb Hv Hnz Hxmod4 xlo xhi).
intro Hvalid.
destruct (valid_access_load _ _ _ _ Hvalid).
eapply load_valid_access.
rewrite <- (Hm'_data Hb Hv Hnz xlo xhi (mod4_sym Hxmod4)).
eassumption.

apply good_pointers_from_to_intro.
intros l0 Hl0.
rewrite (block_description_from_to_func Hl0 H).
clear l0 Hl0.
inversion Hgp.
destruct (H0 _ Hl) as [Hheaders Hptr].
apply good_pointers_from_block_list_intro.
 intros b i Hbi.
 generalize (construct_pointer_list_block (Hheaders _ _ Hbi)).
 intros [pl Hpl].
 replace b with heap in *.
  eapply pointer_list_block_describes.
  eapply pointer_list_block_invar.
   eapply member_block_to_offset; eauto.
  eassumption.
 symmetry; eapply member_block; eauto.
intros b i Hbi pl' Hpl'.
generalize (construct_pointer_list_block (Hheaders _ _ Hbi)).
intros [pl Hpl]. 
replace b with heap in *.
 replace pl' with pl in *.
  intros; eauto.
 eapply pointer_list_block_func.
  eapply pointer_list_block_invar.
   eapply member_block_to_offset; eassumption.
  assumption.
 assumption.
symmetry; eapply member_block; eauto.
Qed .

Corollary follow_pointer_chain_invar : forall bi lp b'i', 
follow_pointer_chain m bi lp b'i' ->
(forall b i, bi = Some (b, i) -> (b = heap /\ member i l)) ->
follow_pointer_chain m' bi lp b'i'.
Proof.
induction 1.
 intro.
 eapply follow_pointer_chain_nil.
intros Hbi.
generalize (Hbi _ _ (refl_equal _)).
intros [Hb_heap Hi_mem].
subst.
eapply follow_pointer_chain_cons.
eapply find_pointer_invar.
  assumption.
 eassumption.
eapply IHfollow_pointer_chain.
inversion Hgp as [Hgp0].
generalize (Hgp0 _ Hl).
intros [Hgp1 Hgp2].
subst.
generalize (member_offset_to_block heap Hi_mem).
intros Hi2.
generalize (Hgp1 _ _ Hi2).
intro Hdesc.
generalize (construct_pointer_list_block Hdesc).
intros [pl Hpl].
generalize (find_pointer_thm_recip H Hpl).
intros Hj.
intros ; subst.
generalize (Hgp2 _ _  Hi2 _ Hpl _ _ (find_in_list_member Hj)).
intros Hc.
split.
 eapply member_block; eauto.
eapply member_block_to_offset; eauto.
Qed.



Variable rd : val.
Hypothesis Hroots : all_roots_desc m rd.
Hypothesis good_roots : forall l0, all_roots m rd l0 -> forall r' d', member (Some (r', d')) (flatten l0) -> 
(r' = heap /\ member d' l).

Hypothesis Hm'_roots : forall pl, root_position_list m rd pl -> forall p i, member (p, i) (flatten pl) ->
load Mint32 m p (signed i) = load Mint32 m' p (signed i).

Lemma realize_path_invar : forall p qi, realize_path m rd p qi -> realize_path m' rd p qi.
Proof.
inversion Hroots.
 subst.
 intros p0 qi Hpi.
 inversion Hpi.
subst.
inversion 1.
destruct (all_roots_desc_root_position_list Hroots).
destruct (find_root_list_root_position_list_thm H7 H13) as [lr0 [Heq Hpl]].
subst.
eapply realize_path_intro.
   eapply find_root_list_invar.
     eassumption.
    eassumption.
   intros b i0 Hb.
   eapply Hm'_roots.
    eassumption.
   assumption.
  eapply trans_equal.
   eexact H8.
  eapply Hm'_roots.
   eassumption.
  eapply member_flatten_intro.
   eapply find_in_list_member.
   eassumption.
  auto.
 eapply find_root_invar.
   eassumption.
  eapply Hpl.
  assumption.
 intros b i0 Hb.
 eapply Hm'_roots.
  eassumption.
 eapply member_flatten_intro.
  eapply find_in_list_member.
  eassumption.
 auto.
eapply follow_pointer_chain_invar.
 assumption.
destruct (construct_all_roots Hroots).
intros; subst.
eapply good_roots.
 eassumption.
destruct (find_root_list_thm_recip H7 a) as [lr2 [Hx [? [? ?]]]].
subst.
eapply member_flatten_intro.
 eapply find_in_list_member.
 eassumption.
eapply find_in_list_member.
eapply find_root_thm_recip.
 eassumption.
congruence.
Qed.


End Invariant_chain.


Lemma find_pointer_invar_recip
       (m : mem) (heap : block) (m' : mem) (n p : int) (l : list int)
       (H : block_description_from_to m heap n p l)
       (H0 : good_pointers_from_to m heap n p)
       (H1 : forall b : int,
        member b l ->
        exists v' : int,
          Some (Vint v') = load Mint32 m' heap (signed (sub b four)))
       (H2 : forall b : int,
        member b l ->
        forall v : int,
        Some (Vint v) = load Mint32 m heap (signed (sub b four)) ->
        forall v' : int,
        Some (Vint v') = load Mint32 m' heap (signed (sub b four)) ->
        Kind_header v = Kind_header v')
       (H3 : forall b : int,
        member b l ->
        forall v : int,
        Some (Vint v) = load Mint32 m heap (signed (sub b four)) ->
        forall v' : int,
        Some (Vint v') = load Mint32 m' heap (signed (sub b four)) ->
        Size_header v = Size_header v')
       (H4 : forall b : int,
        member b l ->
        forall v : int,
        Some (Vint v) = load Mint32 m heap (signed (sub b four)) ->
        (Size_header v = zero -> False) ->
        forall x : int,
        cmp Cle b x = true ->
        cmp Cle x (sub (add b (Size_header v)) four) = true ->
        modulo_four b x ->
        load Mint32 m heap (signed x) = load Mint32 m' heap (signed x)) 
       (b : int)
       (H7 : member b l)
       (n0 : nat) (p0i : option (block * int))
       (H8 : find_pointer m' heap n0 b p0i)
 :
    find_pointer m heap n0 b p0i.

Proof.
intros.
eapply find_pointer_invar.
        eapply block_description_samesize_inv.
          eassumption.
         eassumption.
        assumption.
(* validity *)
intros b0 Hb0 v Hv Hnz x Hxmod4 xlo xhi.
generalize (block_description_valid H Hb0 Hv Hnz Hxmod4 xlo xhi).
intro Hvalid.
destruct (valid_access_load _ _ _ _ Hvalid).
eapply load_valid_access.
rewrite <- (H4 _ Hb0 _ Hv Hnz _ xlo xhi (mod4_sym Hxmod4)).
eassumption.


       eapply good_pointers_from_to_invar.
            eassumption.
           assumption.
          assumption.
         assumption.
        assumption.
       assumption.
      intros.
      eapply ex_set_prop.
      eapply block_header.
        eassumption.
       assumption.
      intros; symmetry.
      eapply H2; eassumption.
     intros; symmetry.
     eapply H3; eassumption.    
    intros b0 Hb0 v' Hv'.
    destruct (block_header H Hb0) as [v Hv].     
    rewrite <- (H3 _ Hb0 _ Hv  _ Hv').
    intros; symmetry; eauto.
  assumption.
 assumption.
Qed.

Lemma follow_pointer_chain_invar_recip :

 forall (m : mem) (heap : block) (m' : mem) (n p : int) (l : list int),
       block_description_from_to m heap n p l ->
       good_pointers_from_to m heap n p ->
       (forall b : int,
        member b l ->
        exists v' : int,
          Some (Vint v') = load Mint32 m' heap (signed (sub b four))) ->
       (forall b : int,
        member b l ->
        forall v : int,
        Some (Vint v) = load Mint32 m heap (signed (sub b four)) ->
        forall v' : int,
        Some (Vint v') = load Mint32 m' heap (signed (sub b four)) ->
        Kind_header v = Kind_header v') ->
       (forall b : int,
        member b l ->
        forall v : int,
        Some (Vint v) = load Mint32 m heap (signed (sub b four)) ->
        forall v' : int,
        Some (Vint v') = load Mint32 m' heap (signed (sub b four)) ->
        Size_header v = Size_header v') ->
       (forall b : int,
        member b l ->
        forall v : int,
        Some (Vint v) = load Mint32 m heap (signed (sub b four)) ->
        (Size_header v = zero -> False) ->
        forall x : int,
        cmp Cle b x = true ->
        cmp Cle x (sub (add b (Size_header v)) four) = true ->
        modulo_four b x ->
        load Mint32 m heap (signed x) = load Mint32 m' heap (signed x)) ->
       forall (bi : option (block * int)) (lp : list nat) (b'i' : option (block * int)),
       follow_pointer_chain m' bi lp b'i' ->
       (forall b i, bi = Some (b, i) -> b = heap /\ member i l) ->
       follow_pointer_chain m bi lp b'i'.

Proof.
intros.
eapply follow_pointer_chain_invar.
        eapply block_description_samesize_inv.
          eassumption.
         eassumption.
        assumption.
(* validity *)
intros b0 Hb0 v Hv Hnz x Hxmod4 xlo xhi.
generalize (block_description_valid H Hb0 Hv Hnz Hxmod4 xlo xhi).
intro Hvalid.
destruct (valid_access_load _ _ _ _ Hvalid).
eapply load_valid_access.
rewrite <- (H4 _ Hb0 _ Hv Hnz _ xlo xhi (mod4_sym Hxmod4)).
eassumption.


       eapply good_pointers_from_to_invar.
             eassumption.
            assumption.
           assumption.
          assumption.
         assumption.
        assumption.

      intros.
      eapply ex_set_prop.
      eapply block_header.
        eassumption.
       assumption.
      intros; symmetry.
      eapply H2; eauto.
     intros; symmetry.
     eapply H3; eauto.
    intros b0 Hb0 v' Hv'.
    destruct (block_header H Hb0) as [v Hv].
    rewrite <- (H3 _ Hb0 _ Hv _ Hv').
    intros; symmetry.
    eapply H4; eauto.
   assumption.
  assumption.

Qed.

Lemma realize_path_invar_recip 

     : forall (m : mem) (heap : block) (m' : mem) (n p : int) (l : list int),
       block_description_from_to m heap n p l ->
       good_pointers_from_to m heap n p ->
       (forall b : int,
        member b l ->
        exists v' : int,
          Some (Vint v') = load Mint32 m' heap (signed (sub b four))) ->
       (forall b : int,
        member b l ->
        forall v : int,
        Some (Vint v) = load Mint32 m heap (signed (sub b four)) ->
        forall v' : int,
        Some (Vint v') = load Mint32 m' heap (signed (sub b four)) ->
        Kind_header v = Kind_header v') ->
       (forall b : int,
        member b l ->
        forall v : int,
        Some (Vint v) = load Mint32 m heap (signed (sub b four)) ->
        forall v' : int,
        Some (Vint v') = load Mint32 m' heap (signed (sub b four)) ->
        Size_header v = Size_header v') ->
       (forall b : int,
        member b l ->
        forall v : int,
        Some (Vint v) = load Mint32 m heap (signed (sub b four)) ->
        (Size_header v = zero -> False) ->
        forall x : int,
        cmp Cle b x = true ->
        cmp Cle x (sub (add b (Size_header v)) four) = true ->
        modulo_four b x ->
        load Mint32 m heap (signed x) = load Mint32 m' heap (signed x)) ->
       forall (rd : val),
       all_roots_desc m rd ->
       (forall l0 : list (list (option (block * int))),
        all_roots m rd l0 ->
        forall (r' : block) (d' : int),
        member (Some (r', d')) (flatten l0) -> r' = heap /\ member d' l) ->
       (forall pl : list (list (block * int)),
        root_position_list m rd pl ->
        forall (p0 : block) (i : int),
        member (p0, i) (flatten pl) ->
        load Mint32 m p0 (signed i) = load Mint32 m' p0 (signed i)) ->
       forall (p0 : path) (qi : option (block * int)),
       realize_path m' rd p0 qi -> realize_path m rd p0 qi
.

Proof.
intros.
eapply realize_path_invar.
          eapply block_description_samesize_inv.
            eassumption.
           eassumption.
          assumption.
(* validity *)
intros b0 Hb0 v Hv Hnz x Hxmod4 xlo xhi.
generalize (block_description_valid H Hb0 Hv Hnz Hxmod4 xlo xhi).
intro Hvalid.
destruct (valid_access_load _ _ _ _ Hvalid).
eapply load_valid_access.
rewrite <- (H4 _ Hb0 _ Hv Hnz _ xlo xhi (mod4_sym Hxmod4)).
eassumption.


         eapply good_pointers_from_to_invar.
               eassumption.
              assumption.
             assumption.
            assumption.
           assumption.
          assumption.

        intros.
        eapply ex_set_prop.
        eapply block_header.
         eassumption.
        assumption.
       intros; symmetry.
       eapply H2; eassumption.
      intros; symmetry.
      eapply H3; eassumption.
     intros b0 Hb0 v' Hv'.
     destruct (block_header H Hb0) as [v Hv].
     rewrite <- (H3 _ Hb0 _ Hv _ Hv').
     intros; symmetry.
     eapply H4; eassumption.

   destruct (construct_all_roots H5).
   destruct (all_roots_desc_root_position_list H5).
   eapply all_roots_describes.
   eapply all_roots_invar.
     eassumption.
    eassumption.
   apply H7.
   assumption.
  destruct (construct_all_roots H5).
  destruct (all_roots_desc_root_position_list H5).
  assert (all_roots m' rd x).
   eapply all_roots_invar; eauto.
  intros l0 Hl0.
  rewrite (all_roots_func Hl0 H10).
  apply H6.
  assumption.
 destruct (construct_all_roots H5).
 destruct (all_roots_desc_root_position_list H5).
 assert (root_position_list m' rd x0).
  eapply root_position_list_invar; eauto.
 intros l0 Hl0.
 rewrite (root_position_list_func Hl0 H10).
 intros; symmetry; eauto.
assumption.
Qed.

End Invariant_paths.

(* Used abstraction (Memory_abstract, for Mark_abstract algorithm) *)

Definition extra_mask := repr (Z_of_bits wordsize (fun z => (zle (Z_of_nat wordsize - 2) z))).

Definition Extra_header h := and h extra_mask.

Lemma header_decomp : forall h,
h = or (Extra_header h) (or (Size_header h) (Kind_header h)).
Proof.
unfold Extra_header.
unfold Size_header.
unfold Kind_header.
intro.
rewrite <- and_or_distrib.
rewrite <- and_or_distrib.
replace (or extra_mask (or size_mask kind_mask)) with mone.
symmetry.
apply and_mone.
unfold mone.
symmetry.
eapply trans_equal.
compute.
match goal with |- mkint ?x ?y = _ => change (mkint x y) with (repr x) end.
reflexivity.
eapply eqm_samerepr.
unfold eqm.
unfold eqmod.
exists 1; reflexivity.
Qed.

Record memory_param : Set := make_memory_param {
  memory_heap : block;
  memory_hs : int;
  memory_he : int;
  memory_rd : val
}.

Record used_abstraction_param : Set := make_used_abstraction_param {
  used_blocklist : list int;
  used_sizes : int -> int;
  used_kinds : int -> int;
  used_extra_zero : bool;
  used_rawdata : int -> val;
  used_children : option (block * int) -> list (option (block * int));
  used_rootpos : list (list (block * int));
  used_roots : list (list (option (block * int)))
}.

Record used_abstraction (m : mem) (mp : memory_param) (p : used_abstraction_param) : Prop := used_abstraction_intro {
  used_heap_hyp : block_description_from_to m (memory_heap mp) (memory_hs mp) (memory_he mp) (used_blocklist p);
  used_sizes_hyp : forall i, member i (used_blocklist p) -> forall v, Some (Vint v) = load Mint32 m (memory_heap mp) (signed (sub i four)) ->
    Size_header v = used_sizes p i;
  used_kinds_hyp : forall i, member i (used_blocklist p) -> forall v, Some (Vint v) = load Mint32 m (memory_heap mp) (signed (sub i four)) ->
    Kind_header v = used_kinds p i;
  used_extra_zero_hyp : used_extra_zero p = true -> forall i, member i (used_blocklist p) -> forall v, Some (Vint v) = load Mint32 m (memory_heap mp) (signed (sub i four)) ->
    Extra_header v = zero;
  used_rawdata_hyp : forall i, member i (used_blocklist p) -> used_kinds p i = KIND_RAWDATA -> (used_sizes p i = zero -> False) -> forall x,
    cmp Cle i x = true -> cmp Cle x (sub (add i (used_sizes p i)) four) = true ->
    modulo_four x i -> load Mint32 m (memory_heap mp) (signed x) = Some (used_rawdata p x);
  used_children_hyp : forall b, member b (used_blocklist p) -> pointer_list_block m (memory_heap mp) b (used_children p (Some (memory_heap mp, b)));
  used_children_are_blocks : forall b, member b (used_blocklist p) -> forall cb co, member (Some (cb, co)) (used_children p (Some (memory_heap mp, b))) ->
    (cb = memory_heap mp /\ member co (used_blocklist p));
  used_children_none : used_children p None = nil;
  used_rootpos_hyp : root_position_list m (memory_rd mp) (used_rootpos p);
  used_roots_hyp : all_roots m (memory_rd mp) (used_roots p);
  used_roots_are_blocks : forall r' d', member (Some (r', d')) (flatten (used_roots p)) -> (r' = memory_heap mp /\ member d' (used_blocklist p));
  used_rootpos_not_in_heap : forall b i, member (b, i) (flatten (used_rootpos p)) -> b <> (memory_heap mp)
}.

Hint Resolve
  used_heap_hyp
  used_sizes_hyp
  used_kinds_hyp
  used_extra_zero_hyp
  used_rawdata_hyp
  used_children_hyp used_children_are_blocks
  used_rootpos_hyp
  used_roots_hyp used_roots_are_blocks used_rootpos_not_in_heap.

Lemma used_abstraction_used_extra_zero_weak : 
  forall m mp up, used_abstraction m mp up ->
    used_abstraction m mp (make_used_abstraction_param
      (used_blocklist up) (used_sizes up) (used_kinds up) false (used_rawdata up) (used_children up) (used_rootpos up) (used_roots up))
.
Proof.
inversion 1.
apply used_abstraction_intro; try assumption.
discriminate 1.
Qed.

Lemma used_extra_zero_used_abstraction :
  forall m mp up, used_abstraction m mp up ->
    (forall i, member i (used_blocklist up) -> forall v, Some (Vint v) = load Mint32 m (memory_heap mp) (signed (sub i four)) ->  Extra_header v = zero) ->
    used_abstraction m mp (make_used_abstraction_param
      (used_blocklist up) (used_sizes up) (used_kinds up) true (used_rawdata up) (used_children up) (used_rootpos up) (used_roots up)).
Proof.
inversion 1.
intro.
apply used_abstraction_intro; try assumption.
intros _ ; assumption.
Qed.

Notation blocklist_hyp := used_heap_hyp (only parsing).

Lemma used_good_pointers : forall m mp up, used_abstraction m mp up ->
good_pointers_from_to m (memory_heap mp) (memory_hs mp) (memory_he mp).
Proof.
inversion 1.
eapply good_pointers_from_to_intro.
intros l Hl.
replace l with (used_blocklist up).
 eapply good_pointers_from_block_list_intro.
  intros b i Hbi.
  generalize (member_block Hbi).
  intros; subst.
  generalize (member_block_to_offset Hbi).
  intro Hi.
  eapply pointer_list_block_describes.
  eauto.
 intros b i Hbi pl Hpl p q Hpq.
 generalize (member_block Hbi).
 intros; subst.
 generalize (member_block_to_offset Hbi).
 intro Hi.
 replace pl with (used_children up (Some (memory_heap mp, i))) in *.
  generalize (used_children_are_blocks H Hi Hpq).
  intros [? Hq]; subst.
  eapply member_offset_to_block.
  assumption.
 eapply pointer_list_block_func; eauto.
eapply block_description_from_to_func; eauto. 
Qed.


Inductive used_follow p : option (block * int) -> list nat -> option (block * int) -> Prop :=
| used_follow_nil : forall a, used_follow p a nil a
| used_follow_cons : forall a n b, find_in_list (used_children p a) n b -> forall l c, used_follow p b l c -> used_follow p a (n::l) c
.

Hint Constructors used_follow.

Lemma used_follow_app_elim : forall p l1 bi l2 pv,
used_follow p bi (l1 ++ l2) pv ->
exists p15v15, (used_follow p bi l1 p15v15 /\ used_follow p p15v15 l2 pv).
induction l1; simpl.
intros.
exists bi.
split; auto.
inversion 1.
subst.
generalize (IHl1 _ _ _ H5).
intros [p15v15 [Hleft Hright]].
exists p15v15.
split; eauto.
Qed.

Lemma used_follow_app_intro : forall p bi l1 p15v15,
used_follow p bi l1 p15v15 ->
forall l2 pv,
used_follow p p15v15 l2 pv ->
used_follow p bi (l1 ++ l2) pv.
Proof.
induction 1; simpl; auto.
intros.
eapply used_follow_cons; eauto.
Qed.


Lemma kind_values : forall m mp p, used_abstraction m mp p -> forall i, member i (used_blocklist p) ->
  used_kinds p i = KIND_RAWDATA \/ used_kinds p i = KIND_PTRDATA \/ used_kinds p i = KIND_CLOSURE.
Proof.
introvars.
intros Hused i Hi.
generalize (used_children_hyp Hused Hi).
inversion 1.
 rewrite <- (used_kinds_hyp Hused Hi H1).
 auto.
rewrite <- (used_kinds_hyp Hused Hi H0); auto.
rewrite <- (used_kinds_hyp Hused Hi H0); auto.
Qed.

Lemma closure_not_null : forall m mp p, used_abstraction m mp p -> forall i, member i (used_blocklist p) ->
used_kinds p i = KIND_CLOSURE -> used_sizes p i <> zero.
Proof.
introvars.
intros Hused i Hi.
generalize (used_children_hyp Hused Hi).
inversion 1.
 rewrite <- (used_kinds_hyp Hused Hi H1).
 intros Hkind.
 rewrite Hkind in H2; inversion H2.
subst.
 rewrite <- (used_kinds_hyp Hused Hi H0).
 intros Hkind.
 rewrite Hkind in H1; inversion H1.
intros.
rewrite <- (used_sizes_hyp Hused Hi H0).
assumption.
Qed.

Definition used_valid (mp : memory_param) (p : used_abstraction_param) (bi : option (block * int)) := match bi with
| None => false
| Some (b, i) => if Z_eq_dec b (memory_heap mp) then if member_dec eq_dec (used_blocklist p) i then true else false else false
end.

Property Hvalid : forall mp p bi, (used_valid mp p bi = true <-> (exists i, bi = Some (memory_heap mp, i) /\ member i (used_blocklist p))).
unfold used_valid.
intros mp p bi.
destruct bi as [[b i] | bi].
 destruct (Z_eq_dec b (memory_heap mp)).
  destruct (member_dec eq_dec (used_blocklist p) i).
   split; auto.
   intros.
   exists i; split; congruence.
  split.
   discriminate 1.
  intros [? [? ?]]; congruence.
 split.
  discriminate 1.
 intros [? [? ?]]; congruence.
split; intros; invall; discriminate.
Qed.

Property Hvalid_bool_prop : forall mp p k, used_valid mp p k = true -> (exists i, k = Some (memory_heap mp, i) /\ member i (used_blocklist p)).
intros mp p k Hk.
destruct (Hvalid mp p k).
eauto.
Qed.

Lemma i_mem : forall l j ,
  member j l -> forall (h : block), member (Some (h, j)) (map (fun j0 : int => Some (h, j0)) l).
Proof.
 induction 1; simpl; eauto.
Qed.

Property Hvalid_bool_prop2 : forall mp p k, used_valid mp p k = true ->
  member k (map (fun j0 : int => Some (memory_heap mp, j0)) (used_blocklist p)).
Proof.
 introvars.
 intro Hused.
 generalize (Hvalid_bool_prop Hused).
 intros [i [? Hmem]].
 subst.
 apply i_mem.
 assumption.
Qed.

Property Hvalid_prop_bool : forall mp p k i, k = Some (memory_heap mp, i) -> member i (used_blocklist p) -> used_valid mp p k = true.
intros mp p k i Hk Hmem.
destruct (Hvalid mp p k) as [h1 h2].
subst.
apply h2.
eapply ex_intro.
split.
reflexivity.
assumption.
Qed.

Definition used_raw p (bi : option (block * int)) : bool :=
  match bi with
    | Some (h, j) => eq (used_kinds p j) KIND_RAWDATA
    | _ => false
  end.

Theorem used_raw_prop_bool : 
    forall m mp p, used_abstraction m mp p -> forall b, member b (used_blocklist p) -> 
      forall v, Some (Vint v) = load Mint32 m (memory_heap mp) (signed (sub b four)) -> Kind_header v = KIND_RAWDATA ->
        used_raw p (Some (memory_heap mp, b)) = true.
Proof.
introvars.
intro Hused.
intros b Hb v Hv Hkind.
unfold used_raw.
rewrite <- (used_kinds_hyp Hused Hb Hv).
apply eq_prop_eq_bool.
assumption.
Qed.

Theorem used_raw_bool_prop :    forall m mp p, used_abstraction m mp p -> 
 forall b, member b (used_blocklist p) -> 
used_raw p (Some (memory_heap mp, b)) = true -> forall v, Some (Vint v) = load Mint32 m (memory_heap mp) (signed (sub b four)) -> Kind_header v = KIND_RAWDATA.
Proof.
 introvars.
 intro Hused.
intros b Hb Hkind v Hv.
unfold used_raw in Hkind.
rewrite <- (used_kinds_hyp Hused Hb Hv) in Hkind.
apply eq_bool_eq_prop.
assumption.
Qed.

Lemma follow_pointer_chain_thm_recip : forall m mp p, used_abstraction m mp p ->
forall a l b, follow_pointer_chain m a l b -> (a = None \/ used_valid mp p a = true) ->
used_follow p a l b /\ (b = None \/ used_valid mp p b = true).
Proof.
intros m mp p Hm.
induction 1.
 intros; split; auto.
inversion 1.
 discriminate.
generalize (Hvalid_bool_prop H2).
intros [i0 [Hinj Hmem]].
injection Hinj; intros; subst.
cut (
  used_follow p cj l dk /\
  (dk = None \/ used_valid mp p dk = true)
).
intros [Hused Hdk].
split ; auto.
eapply used_follow_cons.
  eapply find_pointer_thm_recip.
  eassumption.
 auto.
 assumption.
apply IHfollow_pointer_chain.
destruct cj; auto.
right. 
destruct p0.
generalize (find_in_list_member (find_pointer_thm_recip H (used_children_hyp Hm Hmem))).
intro Hmemc.
generalize (used_children_are_blocks Hm Hmem Hmemc).
intros [? Hmemc2].
subst.
eapply Hvalid_prop_bool.
reflexivity.
assumption.
Qed.

Lemma follow_pointer_chain_thm : forall m mp p, used_abstraction m mp p ->
forall a l b, used_follow p a l b -> (a = None \/ used_valid mp p a = true) ->
follow_pointer_chain m a l b /\ (b = None \/ used_valid mp p b = true).
Proof.
intros m mp p Hm.
induction 1.
 intros; split; auto.
 apply follow_pointer_chain_nil.
inversion 1.
 subst.
 rewrite (used_children_none Hm) in H.
 inversion H.
generalize (Hvalid_bool_prop H2).
intros [i0 [Hinj Hmem]].
subst.
cut (
  follow_pointer_chain m b l c /\
  (c = None \/ used_valid mp p c = true)
).
intros [Hused Hdk].
split ; auto.
eapply follow_pointer_chain_cons.
  eapply find_pointer_thm.
  eapply used_children_hyp.
  eassumption.
  assumption.
  eassumption.
 assumption.
apply IHused_follow.
destruct b; auto.
right. 
destruct p0.
generalize (find_in_list_member H).
intro Hmemc.
generalize (used_children_are_blocks Hm Hmem Hmemc).
intros [? Hmemc2].
subst.
eapply Hvalid_prop_bool.
reflexivity.
assumption.
Qed.

Inductive used_realize_path (up : used_abstraction_param) (p : path) (bi : option (block * int)) : Prop :=
| used_realize_path_intro : forall rl,
  find_in_list (used_roots up) (root_list_number p) rl ->
  forall r, find_in_list rl (root_number p) r ->
    used_follow up r (pointer_chain p) bi ->
    used_realize_path up p bi.

Hint Constructors used_realize_path.

Lemma realize_path_thm : forall m mp up, used_abstraction m mp up ->
forall p bi, used_realize_path up p bi ->
  realize_path m (memory_rd mp) p bi.
Proof.
intros m mp up Hm.
inversion Hm. 
intros p bi Hpath.
inversion Hpath.
inversion used_roots_hyp0.
 rewrite <- H4 in H.
 inversion H.
rewrite <- H2 in *.
generalize (find_root_list_thm H used_roots_hyp0).
intros [d0 [k [Hd0 [num [Hnum Hrl]]]]].
generalize (find_root_thm Hrl H0).
intro Hr.
assert (r = None \/ used_valid mp up r = true).
destruct r.
 right.
 destruct p0.
 generalize (used_roots_are_blocks Hm (member_flatten_intro (find_in_list_member H) (find_in_list_member H0))).
 intros [? Hi_mem].
 subst.
 eapply Hvalid_prop_bool.
 reflexivity.
 assumption.
auto.
generalize (follow_pointer_chain_thm Hm H1 H9).
intros [? _].
eapply realize_path_intro; eassumption.
Qed.

Lemma realize_path_thm_recip : forall m mp up, used_abstraction m mp up ->
forall p bi, realize_path m (memory_rd mp) p bi ->
used_realize_path up p bi.
Proof.
intros m mp up Hm.
inversion Hm. 
intros p bi Hpath.
inversion Hpath.
subst.
rewrite <- H in *.
generalize (find_root_list_thm_recip H0 used_roots_hyp0).
intros [lk [Hfind [num [Hnum Hlk]]]].
replace num with n in *; [|congruence].
generalize (find_root_thm_recip H2 Hlk).
intro Hb0u0.
assert (b0u0 = None \/ used_valid mp up b0u0 = true).
destruct b0u0.
 right.
 destruct p0.
 generalize (used_roots_are_blocks Hm (member_flatten_intro (find_in_list_member Hfind) (find_in_list_member Hb0u0))).
 intros [? Hi_mem].
 subst.
 eapply Hvalid_prop_bool.
 reflexivity.
 assumption.
auto.
generalize (follow_pointer_chain_thm_recip Hm H3 H4).
intros [? _].
eapply used_realize_path_intro; eassumption.
Qed.

(* Finally, two memories with the same used_abstraction params have the same paths. *)

Theorem used_abstraction_paths_inv : forall mp up m m', used_abstraction m mp up -> used_abstraction m' mp up ->
forall p bi, realize_path m (memory_rd mp) p bi -> realize_path m' (memory_rd mp) p bi.
Proof.
intros.
eapply realize_path_thm.
 eassumption.
eapply realize_path_thm_recip.
 2 : eassumption.
assumption.
Qed.

(* More precisely, what does the abstract path realization exactly depend on ? *)

Theorem used_follow_invar : forall up p l q,
used_follow up p l q ->
forall up', 
(forall o, used_children up o = used_children up' o) ->
used_follow up' p l q.
Proof.
induction 1.
 intros; auto.
intros.
eapply used_follow_cons.
rewrite <- H1.
eassumption.
eauto.
Qed.

Theorem used_abstraction_invar : forall up up', 
used_roots up = used_roots up' ->
(forall o, used_children up o = used_children up' o) ->
forall p bi, used_realize_path up p bi ->
used_realize_path up' p bi.
Proof.
intros.
inversion H1.
eapply used_realize_path_intro.
 rewrite <- H.
 eassumption.
eassumption.
eapply used_follow_invar.
 eassumption.
assumption.
Qed.

Section Used_abstraction_init.

Variable m : mem.
Variable mp : memory_param.

Hypothesis Hwf : well_formed_from_to m (memory_heap mp) (memory_hs mp) (memory_he mp).

Let l := describe_blocks Hwf.

Let Hl := describe_blocks_prop Hwf.

Hypothesis Hgp : good_pointers_from_to m (memory_heap mp) (memory_hs mp) (memory_he mp).

Let children_strong_2 : {f | forall b, member b l ->
pointer_list_block m (memory_heap mp) b (f (Some (memory_heap mp, b)))}.

Proof.
destruct (children_strong (m := m) (l := map (fun i0 => (memory_heap mp, i0)) l)) as [c Hc].
 inversion Hgp as [Hgp0].
 generalize (Hgp0 _ Hl).
 intros [Hgp1 Hgp2].
 assumption.
exists (fun bi => match bi with Some bi' => c bi' | None => nil end). 
intros.
eapply Hc.
apply member_offset_to_block.
assumption.
Defined.

Let children := let (c, _) := children_strong_2 in c.

Let Hchildren : forall b, member b l ->
pointer_list_block m (memory_heap mp) b (children (Some (memory_heap mp, b))).
unfold children; destruct children_strong_2; auto.
Qed.

Hypothesis Hall_roots : all_roots_desc m (memory_rd mp).

Let roots := let (l, _) := construct_all_roots Hall_roots in l.

Let Hroots : all_roots m (memory_rd mp) roots.
unfold roots; destruct (construct_all_roots Hall_roots); auto.
Qed.

Let rootpos := let (l, _) := all_roots_desc_root_position_list_constr Hall_roots in l.

Let Hrootpos : root_position_list m (memory_rd mp) rootpos.
unfold rootpos; destruct (all_roots_desc_root_position_list_constr); auto.
Qed.

Hypothesis roots_are_blocks : forall l0, block_description_from_to m (memory_heap mp) (memory_hs mp) (memory_he mp) l0 ->
forall roots0, all_roots m (memory_rd mp) roots0 -> forall r' d', member (Some (r', d')) (flatten roots0) ->
(r' = memory_heap mp /\ member d' l0).

Hypothesis rootpos_not_in_heap :
forall rp, root_position_list m (memory_rd mp) rp ->
forall b i, member (b, i) (flatten rp) -> b <> (memory_heap mp).


Let p := make_used_abstraction_param 
  l
  (fun i => Size_header (block_header_weak Hl i))
  (fun i => Kind_header (block_header_weak Hl i))
  false
  (fun i => match load Mint32 m (memory_heap mp) (signed i) with None => Vundef | Some v => v end)
  children
  rootpos
  roots
.

Let Hp :used_abstraction m mp p.
Proof.
unfold p.
eapply used_abstraction_intro.

(* block description *)
 assumption.

(* sizes *)
simpl.
intros.
rewrite <- (block_header_weak_prop Hl Hl H) in H0.
congruence.

(* kinds *)
simpl.
intros.
rewrite <- (block_header_weak_prop Hl Hl H) in H0.
congruence.

(* extra zero *)
discriminate 1.

(* raw data *)
unfold used_sizes.
unfold used_rawdata.
unfold used_kinds.
unfold used_blocklist.
intros i Hi.
generalize (block_header_weak_prop Hl Hl Hi).
intro Hh.
intros Hkind Hsize_not_null x xlo xhi x_mod4.
generalize (block_description_valid Hl Hi Hh Hsize_not_null x_mod4 xlo xhi).
intro Hvx.
generalize (valid_access_load _ _ _ _ Hvx).
intros [v Hv].
rewrite Hv.
trivial.

(* children *)
assumption.

(* children in block header *)
simpl.
inversion Hgp as [Hgp1].
generalize (Hgp1 _ Hl).
intros [? Hgp2].
intros b Hb cb co Hcbco.
eapply member_block_to_offset_2.
eapply Hgp2.
eapply member_offset_to_block.
eexact Hb.
eapply Hchildren.
assumption.
assumption.

(* children none *)
reflexivity.

(* root position list *)
assumption.

(* all roots *)
assumption.

(* roots are blocks *)
simpl.
intros.
eapply roots_are_blocks.
 assumption.
 eassumption.
 assumption.

(* rootpos not in heap *)
simpl.
apply rootpos_not_in_heap.
assumption.

Qed.

Definition construct_used_abstraction := exist _ p Hp.

End Used_abstraction_init.

Section Used_abstraction.

Variable m : mem.
Variable mp : memory_param.
Variable up : used_abstraction_param.

Hypothesis Hup : used_abstraction m mp up.


Theorem used_make_abstract_path : forall bi, Memory_abstract.used (used_valid mp up) (flatten (used_roots up)) (used_children up) (used_raw up) bi ->
exists p, used_realize_path up p bi.
Proof.
simple induction 1.
intros.
generalize (member_flatten_elim H0).
intros [l0 [Hl0_roots Hn_l0]].
generalize (member_find_in_list Hl0_roots).
intros [rlnum Hrlnum].
generalize (member_find_in_list Hn_l0).
intros [rnum Hrnum].
refine (ex_intro _ (mkPath _ _ _) _).
eapply used_realize_path_intro; simpl.
 eassumption.
 eassumption.
 eauto.
intros k Hkused.
intros Hpath.
intros n Hn.
destruct (Hpath) as [p Hp].
destruct p as [root_list_num root_num ptr_chain].
inversion Hp.
subst.
generalize (Memory_abstract.used_valid Hkused).
intro Hk_valid.
inversion Hn.
generalize (member_find_in_list H4).
intros [n0 Hn0].
exists (mkPath root_list_num root_num (ptr_chain ++ (n0 :: nil))).
eapply used_realize_path_intro; eauto.
simpl.
eapply used_follow_app_intro; eauto.
Qed.

Corollary used_make_path : forall bi, Memory_abstract.used (used_valid mp up) (flatten (used_roots up)) (used_children up) (used_raw up) bi ->
exists p, realize_path m (memory_rd mp) p bi.
Proof.
intros bi Hbi.
generalize (used_make_abstract_path Hbi).
intros [p Hp].
exists p.
eapply realize_path_thm; eassumption.
Qed.


Lemma used_follow_used : forall bi l b'i', used_follow up bi l b'i' ->
(b'i' = None -> False) ->
Memory_abstract.used (used_valid mp up) (flatten (used_roots up)) (used_children up) (used_raw up) bi ->
Memory_abstract.used (used_valid mp up) (flatten (used_roots up)) (used_children up) (used_raw up) b'i'.
Proof.
induction 1.
auto.
intros Hnz Ha.
eapply IHused_follow.
assumption.
eapply Memory_abstract.used_child.
eassumption.
assert (used_follow up a (n :: nil) b).
 eauto.
generalize (Memory_abstract.used_valid Ha).
intros Ha_valid.
generalize (follow_pointer_chain_thm Hup H1 (or_intror _ Ha_valid)).
intros [? Hb].
generalize (follow_pointer_chain_thm Hup H0 Hb).
intros [? Hc].
inversion Hc.
 contradiction.
eapply Memory_abstract.points_to_intro.
case_eq (used_raw up a); auto.
intro Habs.
generalize (Hvalid_bool_prop Ha_valid).
intros [i [? Hi]].
subst.
generalize (used_children_hyp Hup Hi).
inversion 1.
 rewrite <- H6 in H.
 inversion H.
subst.
rewrite (used_raw_bool_prop Hup Hi Habs H6) in H7.
inversion H7.
subst.
rewrite (used_raw_bool_prop Hup Hi Habs H6) in H7.
inversion H7.
eapply find_in_list_member.
eassumption.
inversion Hb; auto.
subst.
inversion H3.
congruence.
Qed.

Corollary abstract_path_used : forall p bi,used_realize_path up p bi -> (bi = None -> False) ->
 Memory_abstract.used (used_valid mp up) (flatten (used_roots up)) (used_children up) (used_raw up) bi.
Proof.
inversion 1.
subst.
intros Hnz.
eapply used_follow_used.
eassumption.
assumption.
destruct r.
 destruct p0.
 generalize (used_roots_are_blocks Hup (member_flatten_intro (find_in_list_member H0) (find_in_list_member H1))).
 intros [? Hi].
 subst.
 eapply Memory_abstract.used_root.
  eapply member_flatten_intro.
   eapply find_in_list_member.
   eassumption.
  eapply find_in_list_member.
  eassumption.
 eapply Hvalid_prop_bool.
  reflexivity.
 assumption.
generalize (follow_pointer_chain_thm Hup H2 (or_introl _ (refl_equal _))).
intros [Hf ?].
inversion Hf.
congruence.
Qed.

Corollary path_used : forall p bi, realize_path m (memory_rd mp) p bi -> (bi = None -> False) ->
 Memory_abstract.used (used_valid mp up) (flatten (used_roots up)) (used_children up) (used_raw up) bi.
Proof.
intros p bi Hp Hbi.
eapply abstract_path_used.
 eapply realize_path_thm_recip; eassumption.
assumption.
Qed.
  

End Used_abstraction.

(* Paths are invariant if the data of the accessible blocks are unchanged,
   independently on the block structure *)

Lemma find_pointer_from_invar_by_path :
forall m m' r0d0,
       (forall p b i, realize_path m r0d0 p (Some (b, i)) -> forall v, Some (Vint v) = load Mint32 m b (signed (sub i four)) ->
        forall x, cmp Cle (sub i four) x = true -> cmp Cle x (sub (add i (Size_header v)) four) = true ->
        modulo_four i x -> load Mint32 m b (signed x) = load Mint32 m' b (signed x)) ->
       forall p b i, realize_path m r0d0 p (Some (b, i)) ->
       forall v, Some (Vint v) = load Mint32 m b (signed (sub i four))  ->
       forall d, cmp Cle (sub i four) d = true -> modulo_four i d -> forall d' n b'i',
       find_pointer_from m b d n d' b'i' -> 
       modulo_four d d' ->
       cmp Cle d d' = true ->
       cmp Cle d' (sub (add i (Size_header v)) four) = true ->
       find_pointer_from m' b d n d' b'i'.

Proof.
intros m m' r0d0 Hmem p b i Hpath v Hv d Hi_le_d Hmod4_b_d d' n b'i' Hptr.
induction Hptr.
intros.
eapply find_pointer_O.
assumption.
eapply trans_equal.
eexact H0.
eapply Hmem.
eexact Hpath.
eassumption.
int_le_lt_trans_tac.
assumption.
assumption.
eapply mod4_trans.
eassumption.
assumption.
assumption.
intros.
eapply find_pointer_S.
assumption.
destruct (modulo_four_le_eq_or_next (a := d) (b := i0)).
assumption.
assumption.
congruence.
invall.
apply IHHptr.
eapply mod4_trans.
eassumption.
apply mod4_sym.
apply modulo_four_four_divides_sub.
unfold four_divides; auto.
assumption.
eapply int_le_trans.
eassumption.
assumption.
Qed.


Corollary find_pointer_invar_by_path : 
forall m m' r0d0,
       (forall p b i, realize_path m r0d0 p (Some (b, i)) -> forall v, Some (Vint v) = load Mint32 m b (signed (sub i four)) ->
         cmp Cle (sub i four) (sub (add i (Size_header v)) one) = true)  ->
       (forall p b i, realize_path m r0d0 p (Some (b, i)) -> forall v, Some (Vint v) = load Mint32 m b (signed (sub i four)) ->
         Kind_header v = KIND_CLOSURE -> Size_header v = zero -> False)  ->
       (forall p b i, realize_path m r0d0 p (Some (b, i)) -> forall v, Some (Vint v) = load Mint32 m b (signed (sub i four)) ->
        forall x, cmp Cle (sub i four) x = true -> cmp Cle x (sub (add i (Size_header v)) four) = true ->
        modulo_four i x -> load Mint32 m b (signed x) = load Mint32 m' b (signed x)) ->


       forall p b i, realize_path m r0d0 p (Some (b, i)) ->

       forall n b'i', find_pointer m b n i b'i' ->
       find_pointer m' b n i b'i' .

Proof.
intros m m' r0d0 Hsle Hclosure_nonzero Hmem p b i Hpath n b'i' Hptr.
destruct Hptr.
eapply find_pointer_ptrdata.
eapply trans_equal.
eexact H.
eapply Hmem.
eexact Hpath.
eassumption.
auto.
apply modulo_four_le_m1_left.
eapply mod4_trans.
eapply modulo_four_four_divides_sub.
unfold four_divides; auto.
eapply modulo_four_four_divides_add; eauto.
eapply Hsle; eauto.
eapply mod4_sym.
eapply modulo_four_four_divides_sub.
unfold four_divides; auto.
assumption.
eapply find_pointer_from_invar_by_path.
eassumption.
eassumption.
eassumption.
auto.
apply mod4_sym.
apply modulo_four_four_divides_sub.
unfold four_divides; auto.
assumption.
apply mod4_sub; auto.
apply modulo_four_four_divides_add.
eauto.
apply modulo_four_le_m1_left.
eapply mod4_trans.
apply modulo_four_four_divides_sub.
unfold four_divides; auto.
apply modulo_four_four_divides_add.
eauto.
eapply Hsle; eauto.
auto.

destruct (modulo_four_le_eq_or_next_2 (a:= sub i four) (b := add i (Size_header v))).
eapply mod4_trans.
apply modulo_four_four_divides_sub.
unfold four_divides; auto.
apply modulo_four_four_divides_add.
eauto.
eapply Hsle; eauto. (* eauto ? *)
destruct (Hclosure_nonzero _ _ _ Hpath _ H H0).
apply add_zero_recip_l with i.
rewrite sub_add_id in *.
congruence.
rewrite sub_add_id in *.
invall.
eapply find_pointer_closure.
eapply trans_equal.
eexact H.
eapply Hmem.
eexact Hpath.
eassumption.
auto.
eapply modulo_four_le_m1_left.
eapply mod4_trans.
apply modulo_four_four_divides_sub.
unfold four_divides; auto.
apply modulo_four_four_divides_add.
eauto.
eapply Hsle; eauto. (* eauto ? *)
apply mod4_sym.
eapply modulo_four_four_divides_sub.
unfold four_divides; eauto.
assumption.
eapply find_pointer_from_invar_by_path.
eassumption.
eassumption.
eassumption.

eassumption.
auto.
assumption.
apply mod4_sym.
eapply mod4_trans.
apply modulo_four_four_divides_sub.
unfold four_divides; auto.
apply mod4_sym.
apply modulo_four_four_divides_add.
eauto.
apply modulo_four_le_m1_left.
apply modulo_four_four_divides_add.
eauto.
assumption.
auto.
Qed.

Corollary follow_pointer_chain_invar_by_path : 
forall m m' r0d0,
       (forall p b i, realize_path m r0d0 p (Some (b, i)) -> forall v, Some (Vint v) = load Mint32 m b (signed (sub i four)) ->
         cmp Cle (sub i four) (sub (add i (Size_header v)) one) = true)  ->
       (forall p b i, realize_path m r0d0 p (Some (b, i)) -> forall v, Some (Vint v) = load Mint32 m b (signed (sub i four)) ->
         Kind_header v = KIND_CLOSURE -> Size_header v = zero -> False)  ->
       (forall p b i, realize_path m r0d0 p (Some (b, i)) -> forall v, Some (Vint v) = load Mint32 m b (signed (sub i four)) ->
        forall x, cmp Cle (sub i four) x = true -> cmp Cle x (sub (add i (Size_header v)) four) = true ->
        modulo_four i x -> load Mint32 m b (signed x) = load Mint32 m' b (signed x)) ->
forall bi l b'i',
follow_pointer_chain m bi l b'i' -> 
forall p, realize_path m r0d0 p bi ->
follow_pointer_chain m' bi l b'i'.
Proof.
intros m m' r0d0 Hsle Hclosure_nonzero Hmem bi l b'i' Hptr.
induction Hptr.
intros.
apply follow_pointer_chain_nil.
intros p Hp.
inversion Hp.
eapply follow_pointer_chain_cons.
eapply find_pointer_invar_by_path.
eassumption.
assumption.
assumption.
eassumption.
eassumption.
eapply IHHptr.
rewrite <- H4.
subst p0 qv.
eapply (realize_path_intro (m := m) (r := r) (d := d) (p := mkPath (root_list_number p) (root_number p) (pointer_chain p ++ n :: nil) )); simpl.
eassumption.
eassumption.
eassumption.
eapply follow_pointer_chain_app_intro.
eassumption.
eapply follow_pointer_chain_cons.
eassumption.
apply follow_pointer_chain_nil.
Qed.

Corollary realize_path_invar_by_path :

forall m m' r0d0,

forall lp, root_position_list m r0d0 lp ->
(forall b i, member (b, i) (flatten lp) -> load Mint32 m b (signed i) = load Mint32 m' b (signed i)) ->

       (forall p b i, realize_path m r0d0 p (Some (b, i)) -> forall v, Some (Vint v) = load Mint32 m b (signed (sub i four)) ->
         cmp Cle (sub i four) (sub (add i (Size_header v)) one) = true)  ->
       (forall p b i, realize_path m r0d0 p (Some (b, i)) -> forall v, Some (Vint v) = load Mint32 m b (signed (sub i four)) ->
         Kind_header v = KIND_CLOSURE -> Size_header v = zero -> False)  ->
       (forall p b i, realize_path m r0d0 p (Some (b, i)) -> forall v, Some (Vint v) = load Mint32 m b (signed (sub i four)) ->
        forall x, cmp Cle (sub i four) x = true -> cmp Cle x (sub (add i (Size_header v)) four) = true ->
        modulo_four i x -> load Mint32 m b (signed x) = load Mint32 m' b (signed x)) ->

forall bi p, realize_path m r0d0 p bi -> realize_path m' r0d0 p bi.

intros m m' r0d0 lp Hlp Hrootpos Hsle Hclosure_nonzero Hmem bi p Hpath.
inversion Hpath.
subst.
destruct (find_root_list_root_position_list_thm H Hlp) as [lr0 [Heq Hpl]].
subst.
eapply realize_path_intro.
eapply find_root_list_invar.
eassumption.
eassumption.
assumption.
eapply trans_equal.
eexact H0.
eapply Hrootpos.
eapply member_flatten_intro.
 eapply find_in_list_member.
 eassumption.
auto.
eapply find_root_invar.
eassumption.
eauto.
intros b1 i1 Hb1.
eapply Hrootpos.
eapply member_flatten_intro.
 eapply find_in_list_member.
 eassumption.
auto.
eapply follow_pointer_chain_invar_by_path.
eassumption.
assumption.
assumption.
assumption.
eapply (realize_path_intro (m := m) (r := r) (d := d) (p := mkPath (root_list_number p) (root_number p) nil )); simpl.
eassumption.
eassumption.
eassumption.
apply follow_pointer_chain_nil.
Qed.

(* Reciprocal theorems, starting from the hypotheses on the "before" memory *)

Lemma find_pointer_from_invar_by_path_recip :
forall m m' r0d0,

       (forall p b i, realize_path m r0d0 p (Some (b, i)) -> forall v, Some (Vint v) = load Mint32 m b (signed (sub i four)) ->
        forall x, cmp Cle (sub i four) x = true -> cmp Cle x (sub (add i (Size_header v)) four) = true ->
        modulo_four i x -> load Mint32 m b (signed x) = load Mint32 m' b (signed x)) ->
       forall p b i, realize_path m r0d0 p (Some (b, i)) ->
       forall v, Some (Vint v) = load Mint32 m b (signed (sub i four))  ->
       forall d, cmp Cle (sub i four) d = true -> modulo_four i d -> forall d' n b'i',
       find_pointer_from m' b d n d' b'i' -> 
       modulo_four d d' ->
       cmp Cle d d' = true ->
       cmp Cle d' (sub (add i (Size_header v)) four) = true ->
       find_pointer_from m b d n d' b'i'.
Proof.
intros m m' r0d0 Hmem p b i Hpath v Hv d Hb_le_d Hmod4_b_d d' n b'i' Hptr.
induction Hptr.
intros.
eapply find_pointer_O.
assumption.
eapply trans_equal.
eexact H0.
symmetry.
eapply Hmem.
eexact Hpath.
eassumption.
int_le_lt_trans_tac.
assumption.
assumption.
eapply mod4_trans; eauto.
assumption.

intros.
eapply find_pointer_S.
assumption.
destruct (modulo_four_le_eq_or_next (a := d) (b := i0)).
assumption.
assumption.
congruence.
invall.
apply IHHptr.
eapply mod4_trans.
eassumption.
apply mod4_sym.
apply modulo_four_four_divides_sub.
unfold four_divides; auto.
assumption.
eapply int_le_trans.
eassumption.
assumption.
Qed.

(* Here I need the block headers to be well defined in the "from" memory. *)

Corollary find_pointer_invar_by_path_recip : 

forall m m' r0d0,


        (forall p b i, realize_path m r0d0 p (Some (b, i)) -> exists v, Some (Vint v) = load Mint32 m b (signed (sub i four)))  ->  

       (forall p b i, realize_path m r0d0 p (Some (b, i)) -> forall v, Some (Vint v) = load Mint32 m b (signed (sub i four)) ->
         cmp Cle (sub i four) (sub (add i (Size_header v)) one) = true)  ->
       (forall p b i, realize_path m r0d0 p (Some (b, i)) -> forall v, Some (Vint v) = load Mint32 m b (signed (sub i four)) ->
         Kind_header v = KIND_CLOSURE -> Size_header v = zero -> False)  ->
       (forall p b i, realize_path m r0d0 p (Some (b, i)) -> forall v, Some (Vint v) = load Mint32 m b (signed (sub i four)) ->
        forall x, cmp Cle (sub i four) x = true -> cmp Cle x (sub (add i (Size_header v)) four) = true ->
        modulo_four i x -> load Mint32 m b (signed x) = load Mint32 m' b (signed x)) ->


       forall p b i, realize_path m r0d0 p (Some (b, i)) ->

       forall n b'i', find_pointer m' b n i b'i' ->
       find_pointer m b n i b'i' .

Proof.
intros m m' r0d0 Hheader  Hsle Hclosure_nonzero Hmem p b i Hpath n b'i' Hptr.
destruct (Hheader _ _ _ Hpath) as [vb Hvb].  
destruct Hptr.
 
assert (Some (Vint v) = load Mint32 m b (signed (sub i four))).
 rewrite H.
 symmetry.
 eapply Hmem.
 eexact Hpath.
 eassumption.
 auto.
 eapply modulo_four_le_m1_left.
 eapply mod4_trans.
 eapply modulo_four_four_divides_sub.
 unfold four_divides; eauto.
 apply modulo_four_four_divides_add.
 eauto.
 eapply Hsle; eauto.
 apply mod4_sym.
 eapply modulo_four_four_divides_sub. unfold four_divides; eauto.
clear vb Hvb.
eapply find_pointer_ptrdata.
eassumption.
assumption.
eapply find_pointer_from_invar_by_path_recip.
eassumption.
eassumption.
eassumption.
auto.
apply mod4_sym.
apply modulo_four_four_divides_sub.
unfold four_divides; auto.
assumption.
apply mod4_sub; auto.
apply modulo_four_four_divides_add.
eauto.
apply modulo_four_le_m1_left.
eapply mod4_trans.
apply modulo_four_four_divides_sub.
unfold four_divides; auto.
apply modulo_four_four_divides_add.
eauto.
eapply Hsle; eauto.
auto.

assert (Some (Vint v) = load Mint32 m b (signed (sub i four))).
 rewrite H.
 symmetry.
 eapply Hmem.
 eexact Hpath.
 eassumption.
 auto.
 eapply modulo_four_le_m1_left.
 eapply mod4_trans.
 eapply modulo_four_four_divides_sub.
 unfold four_divides; eauto.
 apply modulo_four_four_divides_add.
 eauto.
 eapply Hsle; eauto.
 apply mod4_sym.
 eapply modulo_four_four_divides_sub. unfold four_divides; eauto.
clear vb Hvb.
destruct (modulo_four_le_eq_or_next_2 (a:= sub i four) (b := add i (Size_header v))).
eapply mod4_trans.
apply modulo_four_four_divides_sub.
unfold four_divides; auto.
apply modulo_four_four_divides_add.
eauto.
eapply Hsle; eauto. (*  eauto ? *)
destruct (Hclosure_nonzero _ _ _ Hpath _ H2 H0).
apply add_zero_recip_l with i.
rewrite sub_add_id in *.
congruence.
rewrite sub_add_id in *.
invall.
eapply find_pointer_closure.
eassumption.
assumption.
eapply find_pointer_from_invar_by_path_recip.
eassumption.
eassumption.
eassumption.
eassumption.
auto.
assumption.
apply mod4_sym.
eapply mod4_trans.
apply modulo_four_four_divides_sub.
unfold four_divides; auto.
apply mod4_sym.
apply modulo_four_four_divides_add.
eauto.
apply modulo_four_le_m1_left.
apply modulo_four_four_divides_add.
eauto.
assumption.
auto.
Qed.

Corollary follow_pointer_chain_invar_by_path_recip : 

forall m m' r0d0,
       (forall p b i, realize_path m r0d0 p (Some (b, i)) -> exists v, Some (Vint v) = load Mint32 m b (signed (sub i four)))  ->

       (forall p b i, realize_path m r0d0 p (Some (b, i)) -> forall v, Some (Vint v) = load Mint32 m b (signed (sub i four)) ->
         cmp Cle (sub i four) (sub (add i (Size_header v)) one) = true)  ->
       (forall p b i, realize_path m r0d0 p (Some (b, i)) -> forall v, Some (Vint v) = load Mint32 m b (signed (sub i four)) ->
         Kind_header v = KIND_CLOSURE -> Size_header v = zero -> False)  ->
       (forall p b i, realize_path m r0d0 p (Some (b, i)) -> forall v, Some (Vint v) = load Mint32 m b (signed (sub i four)) ->
        forall x, cmp Cle (sub i four) x = true -> cmp Cle x (sub (add i (Size_header v)) four) = true ->
        modulo_four i x -> load Mint32 m b (signed x) = load Mint32 m' b (signed x)) ->
forall bi l b'i',
follow_pointer_chain m' bi l b'i' -> 
forall p, realize_path m r0d0 p bi ->
follow_pointer_chain m bi l b'i'.


Proof.
intros m m' r0d0 Hheader Hsle Hclosure_nonzero Hmem bi l b'i' Hptr.
induction Hptr.
intros.
apply follow_pointer_chain_nil.
intros p Hp.
inversion Hp.
subst.
destruct (Hheader _ _ _ Hp) as [vi Hvi].
eapply follow_pointer_chain_cons.
eapply find_pointer_invar_by_path_recip.
eassumption.
eassumption.
assumption.
eassumption.
eassumption.
eassumption.
eapply IHHptr.
eapply (realize_path_intro (m := m) (r := r) (d := d) (p := mkPath (root_list_number p) (root_number p) (pointer_chain p ++ n :: nil))); simpl.
eassumption.
eassumption.
eassumption.
eapply follow_pointer_chain_app_intro.
eassumption.
eapply follow_pointer_chain_cons.
eapply find_pointer_invar_by_path_recip.
eassumption.
assumption.
assumption.
eassumption.
eassumption.
eassumption.
apply follow_pointer_chain_nil.
Qed.

Corollary realize_path_invar_by_path_recip :


forall m m' r0d0,

forall lp, root_position_list m r0d0 lp ->
(forall b i, member (b, i) (flatten lp) -> load Mint32 m b (signed i) = load Mint32 m' b (signed i)) ->

       (forall p b i, realize_path m r0d0 p (Some (b, i)) -> exists v, Some (Vint v) = load Mint32 m b (signed (sub i four)))  -> 

       (forall p b i, realize_path m r0d0 p (Some (b, i)) -> forall v, Some (Vint v) = load Mint32 m b (signed (sub i four)) ->
         cmp Cle (sub i four) (sub (add i (Size_header v)) one) = true)  ->
       (forall p b i, realize_path m r0d0 p (Some (b, i)) -> forall v, Some (Vint v) = load Mint32 m b (signed (sub i four)) ->
         Kind_header v = KIND_CLOSURE -> Size_header v = zero -> False)  ->
       (forall p b i, realize_path m r0d0 p (Some (b, i)) -> forall v, Some (Vint v) = load Mint32 m b (signed (sub i four)) ->
        forall x, cmp Cle (sub i four) x = true -> cmp Cle x (sub (add i (Size_header v)) four) = true ->
        modulo_four i x -> load Mint32 m b (signed x) = load Mint32 m' b (signed x)) ->

forall bi p, realize_path m' r0d0 p bi -> realize_path m r0d0 p bi.

Proof.
intros m m' r0d0 lp Hlp Hrootpos Hheader Hsle Hclosure_nonzero Hmem bi p Hpath.
inversion Hpath.
assert (root_position_list m' r0d0 lp) as H'.
 eapply root_position_list_invar.
 eassumption.
 assumption.
subst.
destruct (find_root_list_root_position_list_thm H H') as [lr0 [Heq Hpl]].
subst.
eapply realize_path_intro.
eapply find_root_list_invar.
eassumption.
eassumption.
intros; symmetry; eauto.
eapply trans_equal.
eexact H0.
symmetry.
eapply Hrootpos.
eapply member_flatten_intro.
 eapply find_in_list_member.
  eassumption.
 auto.
eapply find_root_invar.
eassumption.
eauto.
intros b1 i1 Hb1.
symmetry.
eapply Hrootpos.
eapply member_flatten_intro.
 eapply find_in_list_member.
  eassumption.
 auto.
eapply follow_pointer_chain_invar_by_path_recip.
eassumption.
assumption.
assumption.
eassumption.
eassumption.
eapply (realize_path_intro (m := m) (r := r) (d := d) (p := mkPath (root_list_number p) (root_number p) nil )); simpl.
eapply find_root_list_invar.
eassumption.
eassumption.
intros; symmetry; eauto.
eapply trans_equal.
eexact H0.
symmetry.
eapply Hrootpos.
eapply member_flatten_intro.
 eapply find_in_list_member.
  eassumption.
 auto.
eapply find_root_invar.
eassumption.
eauto.
intros b1 i1 Hb1.
symmetry.
eapply Hrootpos.
eapply member_flatten_intro.
 eapply find_in_list_member.
  eassumption.
 auto.
apply follow_pointer_chain_nil.
Qed.

End Path.


Section Chain.

(* for the freelist -- and maybe the roots too *)

Inductive chain (m : mem) : block -> int -> list (block * int) -> Prop :=
| chain_end : forall b i, Some (Vint zero) = load Mint32 m b (signed i) ->
  chain m b i nil
| chain_cont : forall b i b' i', Some (Vptr b' i') = load Mint32 m b (signed i) ->
  forall l, chain m b' i' l -> chain m b i ((b', i') :: l)
.

Hint Constructors chain.

Lemma chain_func : forall m b i l, chain m b i l -> forall l', chain m b i l' -> l = l'.
Proof.
induction 1; inversion 1; try congruence.
subst.
f_equal.
 congruence.
eapply IHchain.
congruence.
Qed.

Lemma chain_tail : forall l1 b i b' i' l2 m, chain m b i (l1 ++ (b', i') :: l2) -> chain m b' i' l2.
Proof.
induction l1; simpl.
 inversion 1; auto.
inversion 1.
subst.
eapply IHl1.
eassumption.
Qed.

Lemma chain_not_mem_0 : forall l1 b i l2 m, chain m b i (l1 ++ (b, i) :: l2) -> False.
Proof.
intros.
generalize (chain_tail H).
intro H0.
generalize (chain_func H H0).
intro Habs.
cut (length (l1 ++ (b, i) :: l2) = length l2).
 rewrite app_length.
 simpl.
 omega.
rewrite Habs.
trivial.
Qed.

Corollary chain_not_mem : forall l b i m, chain m b i l -> member (b, i) l -> False.
intros.
destruct (member_extract H0).
invall.
subst.
eapply chain_not_mem_0; eassumption.
Qed.

Lemma chain_no_duplicates : forall m b i l, chain m b i l -> no_duplicates l.
Proof.
induction 1.
 auto.
apply no_duplicates_cons.
intros; eapply chain_not_mem; eauto.
assumption.
Qed.

Inductive chain_until (m : mem) (until_block : block) (until_off : int) :
   block -> int -> list (block * int) -> Prop :=
| chain_until_end : chain_until m until_block until_off until_block until_off nil
| chain_until_cont : forall b i, (b, i) <> (until_block, until_off) -> forall b' i',
  Some (Vptr b' i') = load Mint32 m b (signed i) ->
    forall l', chain_until m until_block until_off b' i' l' ->
      chain_until m until_block until_off b i ((b', i'):: l')
.

Lemma chain_until_func m until_block until_off : forall b i l, chain_until m until_block until_off b i l ->
forall l2, chain_until m until_block until_off b i l2 -> l = l2.
Proof.
induction 1.
 inversion 1.
  auto.
 congruence.
inversion 1.
 congruence.
subst.
replace b'0 with b' in *.
replace i'0 with i' in *.
f_equal.
 eauto.
congruence.
congruence.
Qed.

Lemma chain_until_func_2 m until_block until_off b i l : chain_until m until_block until_off b i l ->
forall until_block_2 until_off_2, chain_until m until_block_2 until_off_2 b i l ->
until_block = until_block_2 /\ until_off = until_off_2.
Proof.
induction 1.
 inversion 1.
 auto.
inversion 1.
subst.
eauto.
Qed.

Lemma chain_until_last_mem  m until_block until_off : forall b i l, chain_until m until_block until_off b i l ->
(b, i) = (until_block, until_off) \/ member (until_block, until_off) l.
Proof.
induction 1.
 auto.
right.
inversion IHchain_until.
 injection H2; intros; subst; auto.
auto.
Qed.

Hint Constructors chain_until.

Lemma chain_until_closed : forall m ub uo b o l, chain_until m ub uo b o l ->
Some (Vint zero) = load Mint32 m ub (signed uo) ->
chain m b o l.
Proof.
induction 1; intros; eauto.
Qed.

Lemma chain_explicit_split : forall l1 m b i l2, chain m b i (l1 ++ l2) ->
exists b', exists i', 
chain_until m b' i' b i l1 /\ chain m b' i' l2.
Proof.
induction l1.
 simpl.
 intros.
 exists b.
 exists i.
 split;  auto.
simpl.
inversion 1.
subst.
destruct (IHl1 _ _ _ _ H5).
invall.
exists x.
exists x0.
split.
apply chain_until_cont.
 intro.
 injection H1; intros; subst.
 generalize (chain_func H2 H).
 intro Habs.
 assert (length l2 = S (length l1 + length l2)).
  pattern l2 at 1.
  rewrite Habs.
  simpl.
  rewrite app_length.
  auto.
 omega.
 assumption.
 assumption.
 assumption.
Qed.

Lemma chain_split : forall l m b i, chain m b i l -> forall b' i', 
(b, i) = (b', i') \/ member (b', i') l ->
exists l1, exists l2, l = l1 ++ l2 /\ chain_until m b' i' b i l1 /\ chain m b' i' l2.
Proof.
induction 1.
 inversion 1.
  injection H1; intros; subst.
  exists (@nil (block * int)).
  exists (@nil (block * int)).
  split.
   reflexivity.
  split.
   auto.
  auto.
 inversion H1.
intros b'0 i'0.
destruct (eq_optptr (Some (b, i)) (Some (b'0, i'0))).
 injection e; intros; subst.
 exists (@nil (block * int)).
 exists ((b', i') :: l).
 split.
  simpl; trivial.  
 split; auto.
inversion 1.
 congruence.
destruct (eq_optptr (Some (b, i)) (Some (b', i'))).
 injection e.
 intros; subst.
 assert (chain m b' i' ((b', i')::l)).
  auto.
 change ((b', i') :: l) with (nil ++ (b', i') :: l) in H3.
 destruct (chain_not_mem_0 H3).
assert ((b, i) <> (b', i')).
 congruence.
destruct (eq_optptr (Some (b', i')) (Some (b'0, i'0))).
 injection e.
 intros; subst.
 exists ((b'0, i'0) :: nil).
 exists l.
 split.
   simpl.
   auto.
 split.
  auto.
 assumption.
assert ((b', i') <> (b'0, i'0)).
 congruence.
inversion H2.
 subst.
 congruence.
subst.
generalize (IHchain _ _ (or_intror _ H6)).
intros [l1 [l2 [Hl [Hl1 Hl2 ]]]].
subst.
exists ((b', i')::l1).
exists l2.
split.
 trivial.
split; auto.
 apply chain_until_cont.
  congruence.
  auto.
  auto.
Qed.

Lemma chain_merge : forall l1 m b i b' i', chain_until m b' i' b i l1 ->
forall l2, chain m b' i' l2 ->
chain m b i (l1 ++ l2).
Proof.
induction 1.
 simpl; auto.
intros l2 Hl2.
simpl.
apply chain_cont.
 assumption.
eauto.
Qed.

Lemma chain_until_invar : forall m1 b' i' b i l, chain_until m1 b' i' b i l ->
forall m2, (forall c j, (c, j) <> (b', i') -> ( (c, j) = (b, i) \/  member (c, j) l) ->
load Mint32 m1 c (signed j) = load Mint32 m2 c (signed j)) ->
chain_until m2 b' i' b i l.
Proof.
induction 1.
 intros; auto.
intros m2 Hm2.
apply chain_until_cont.
  assumption.
 rewrite <- Hm2.
  assumption.
 auto.
auto.
eapply IHchain_until.
intros c j Hdiff.
inversion 1.
 injection H3; intros; subst.
 eapply Hm2.
 assumption.
 auto.
eapply Hm2.
 assumption.
auto.
Qed.

Lemma chain_invar : forall m1 b i l, chain m1 b i l ->
forall m2, (forall c j, (c, j) = (b, i) \/ member (c, j) l ->
load Mint32 m1 c (signed j) = load Mint32 m2 c (signed j)) ->
chain m2 b i l.
Proof.
induction 1.
 intros.
 apply chain_end.
 rewrite <- H0.
 assumption.
 auto.
intros m2 Hm2.
apply chain_cont.
 rewrite <- Hm2.
 assumption.
 auto.
eapply IHchain.
inversion 1.
 injection H2; intros; subst.
 eapply Hm2.
 auto.
eauto.
Qed.

End Chain.