Require Export Marksweep_concrete.
Require Mark_abstract_finite.

Load param.

Lemma size_header_color_white_inv : forall i,
Size_header (or i COLOR_WHITE) = Size_header i.
Proof.
unfold COLOR_WHITE.
intros.
rewrite or_zero.
auto.
Qed.

Lemma size_header_color_black_inv :forall i,
Size_header (or i COLOR_BLACK) = Size_header i.
Proof.
unfold Size_header.
intro i.
rewrite and_commut.
rewrite and_or_distrib.
change (and size_mask COLOR_BLACK) with zero.
rewrite or_zero.
apply and_commut.
Qed.

Lemma size_header_color_gray_inv :forall i,
Size_header (or i COLOR_GRAY) = Size_header i.
Proof.
unfold Size_header.
intro i.
rewrite and_commut.
rewrite and_or_distrib.
change (and size_mask COLOR_GRAY) with zero.
rewrite or_zero.
apply and_commut.
Qed.

Corollary size_header_color_inv : forall c,
(c = COLOR_WHITE \/ c = COLOR_BLACK \/ c = COLOR_GRAY) ->
forall i, Size_header (or i c) = Size_header i.
Proof.
simple inversion 1.
intros; subst; apply size_header_color_white_inv.
simple inversion 1.
intros; subst; apply size_header_color_black_inv.
intros; subst; apply size_header_color_gray_inv.
Qed.

Lemma kind_header_color_white_inv : forall i,
Kind_header (or i COLOR_WHITE) = Kind_header i.
Proof.
unfold COLOR_WHITE.
intros.
rewrite or_zero.
auto.
Qed.

Lemma kind_header_color_black_inv :forall i,
Kind_header (or i COLOR_BLACK) = Kind_header i.
Proof.
unfold Kind_header.
intro i.
rewrite and_commut.
rewrite and_or_distrib.
change (and three COLOR_BLACK) with zero.
rewrite or_zero.
apply and_commut.
Qed.

Lemma kind_header_color_gray_inv :forall i,
Kind_header (or i COLOR_GRAY) = Kind_header i.
Proof.
unfold Kind_header.
intro i.
rewrite and_commut.
rewrite and_or_distrib.
change (and three COLOR_GRAY) with zero.
rewrite or_zero.
apply and_commut.
Qed.

Corollary kind_header_color_inv : forall c,
(c = COLOR_WHITE \/ c = COLOR_BLACK \/ c = COLOR_GRAY) ->
forall i, Kind_header (or i c) = Kind_header i.
Proof.
simple inversion 1.
intros; subst; apply kind_header_color_white_inv.
simple inversion 1.
intros; subst; apply kind_header_color_black_inv.
intros; subst; apply kind_header_color_gray_inv.
Qed.

Lemma color_header_white_var : forall i,
Color_header i = COLOR_WHITE -> forall c,
 (c = COLOR_BLACK \/ c = COLOR_GRAY) ->
Color_header (or i c) = c.
Proof.
intros i.
unfold Color_header.
intros Hi c Hc.
rewrite and_commut.
rewrite and_or_distrib.
rewrite and_commut.
rewrite Hi.
unfold COLOR_WHITE.
rewrite or_commut.
rewrite or_zero.
inversion Hc; subst; reflexivity.
Qed.

Lemma color_header_gray_var : forall i,
Color_header i = COLOR_GRAY -> 
Color_header (or i COLOR_BLACK) = COLOR_BLACK.
Proof.
intros i.
unfold Color_header.
intros Hi.
rewrite and_commut.
rewrite and_or_distrib.
rewrite and_commut.
rewrite Hi.
reflexivity.
Qed.

Lemma and_or_abs_0 :
  forall x y,
  and (or y x) x = and x x.
Proof.
  intros; unfold and, or, bitwise_binop.
  decEq. repeat rewrite unsigned_repr; auto with ints.
  apply Z_of_bits_exten; intros.
  repeat rewrite bits_of_Z_of_bits; auto.
  destruct (bits_of_Z wordsize (unsigned x) z);
  destruct (bits_of_Z wordsize (unsigned y) z );
  trivial.
Qed. (* inspired from Integers.add_or_distrib. *)

Corollary and_or_abs :
forall x y,
 and (or y x) x = x.
Proof.
 intros.
 rewrite and_or_abs_0.
 apply and_idem.
Qed.

Corollary color_header_set_black : forall i,
Color_header (or i COLOR_BLACK) = COLOR_BLACK.
Proof.
unfold Color_header.
intros i.
change color_mask with COLOR_BLACK.
apply and_or_abs.
Qed.

Lemma block_description_change_color_inv : 
forall c, (c = COLOR_WHITE \/ c = COLOR_BLACK \/ c = COLOR_GRAY) ->
forall b l, member b l -> forall m heap n p,
block_description_from_to m heap n p l ->
forall v, Some (Vint v) = load Mint32 m heap (signed (sub b four)) ->
forall m', Some m' = store Mint32 m heap (signed (sub b four)) (Vint (or v c)) ->
block_description_from_to m' heap n p l.

Proof.
intros c Hc b l Hbl m heap n p Hm v Hv m' Hm'.
generalize (load_valid_access _ _ _ _ _ (sym_equal Hv)).
intros Hvalid.
inversion Hvalid.
eapply block_description_samesize_inv.
eassumption.
intros b0 Hb0.
destruct (block_header Hm Hb0).
destruct (eq_dec b b0).
subst.
exists (or v c).
symmetry.
change (Vint (or v c)) with (Val.load_result Mint32 (Vint (or v c))).
eapply load_store_same.
eauto.
exists x.
rewrite e.
eapply get_set_int32_indep; eauto.
repeat rewrite sub_add_opp.
intro.
destruct n0.
eapply add_reg_r; eauto.
apply mod4_sub; auto.
eapply block_description_modulo_four; eauto.

intros b0 Hb0 v0 Hv0 v' Hv'.
destruct (eq_dec b b0).
replace v0 with v in *; [ | congruence].
subst.
generalize (load_store_same _ _ _ _ _ _ (sym_equal Hm')).
simpl.
intro.
replace v' with (or v c); [ | congruence].
symmetry; eapply size_header_color_inv; eauto.

assert (load Mint32 m heap (signed (sub b0 four)) = load Mint32 m' heap (signed (sub b0 four))).
 eapply get_set_int32_indep; eauto.
 repeat rewrite sub_add_opp.
 intro.
 destruct n0.
 eapply add_reg_r; eauto.
 apply mod4_sub; auto.
 eapply block_description_modulo_four; eauto.
congruence.

(* validity *)
intros.
eapply store_valid_access_1.
 eauto.
eapply block_description_valid; eauto.
Qed.

Module Marksweep_theorems (MP : Marksweep_parameters) (MH : Marksweep_hypotheses).

Export MH.

Module MA := Marksweep_algorithms MP MH.
Export MA.

Section Cache_invar.
Variable m : mem.

Lemma cache_invar_0 : forall i0 l, pointer_list m gray_cache_block (sub zero four) i0 l ->
forall i, i0 = sub i four ->
((i = zero -> False) -> cmp Cle zero (sub i four) = true) ->
modulo_four i zero ->
forall m',
((i = zero -> False) -> forall x, cmp Cle zero x = true -> cmp Cle x (sub i four) = true -> 
modulo_four x zero ->
load Mint32 m gray_cache_block (signed x) = load Mint32 m' gray_cache_block (signed x)) ->
pointer_list m' gray_cache_block (sub zero four) (sub i four) l.
Proof.
induction 1.
intros; apply pointer_list_end; congruence.

intros i1 Hi1.
subst.
intros Hcond Hmod4 m' Hm'.
assert (i1 = zero -> False).
 intro.
 destruct H.
 f_equal.
 assumption.
eapply pointer_list_cont.
assumption.
eapply trans_equal.
eexact H0.
apply Hm'.
assumption.
eapply Hcond; eauto.
auto.
eapply mod4_trans.
eapply modulo_four_four_divides_sub; eauto.
apply four_divides_four.
assumption.
destruct (modulo_four_le_eq_or_next (a := zero) (b := sub i1 four))
 as [? | [? [? [? ?]]]].
apply mod4_sym.
eapply mod4_trans.
eapply modulo_four_four_divides_sub.
unfold four_divides; auto.
assumption.
eauto.
eapply IHpointer_list.
trivial.
intro ; congruence.
eapply mod4_trans.
eapply modulo_four_four_divides_sub.
unfold four_divides; auto.
assumption.
intro ; congruence.

eapply IHpointer_list.
trivial.
intros _ ; assumption.
eapply mod4_trans.
eapply modulo_four_four_divides_sub.
unfold four_divides; auto.
assumption.
intros _ x xlo xhi x_mod4.
apply Hm'.
assumption.
assumption.
eapply int_le_trans.
eexact xhi.
assumption.
assumption.
assumption.
Qed.

Corollary cache_invar : forall i l, pointer_list m gray_cache_block (sub zero four) (sub i four) l ->
((i = zero -> False) -> cmp Cle zero (sub i four) = true) ->
modulo_four i zero ->
forall m',
((i = zero -> False) -> forall x, cmp Cle zero x = true -> cmp Cle x (sub i four) = true -> 
modulo_four x zero ->
load Mint32 m gray_cache_block (signed x) = load Mint32 m' gray_cache_block (signed x)) ->
pointer_list m' gray_cache_block (sub zero four) (sub i four) l.

Proof (fun _ _ H => cache_invar_0 H (refl_equal _)).

(* NOTE : better use cache_invar than pointer_list_invar in these cases *)

End Cache_invar.

Record marksweep_invariants   (m : mem) (mp : memory_param) (up : used_abstraction_param) (gp : gc_invariants_param) : Prop :=
marksweep_invariants_intro {

 marksweep_gc_inv : gc_invariants m mp up gp;

 gray_cache_offset_not_in_heap : gray_cache_offset_block <> (memory_heap mp);
 gray_cache_overflow_not_in_heap : gray_cache_overflow_block <> (memory_heap mp);
 gray_cache_not_in_heap : gray_cache_block <> (memory_heap mp);

 gray_cache_overflow_rootpos_indep : forall b i, member (b, i) (flatten (used_rootpos up)) -> b <> gray_cache_overflow_block;
 gray_cache_rootpos_indep : forall b i, member (b, i) (flatten (used_rootpos up)) -> b <> gray_cache_block;
 gray_cache_offset_rootpos_indep : forall b i, member (b, i) (flatten (used_rootpos up)) -> b <> gray_cache_offset_block;

 gray_cache_valid : valid_block m gray_cache_block;
 gray_cache_low_bound : low_bound m gray_cache_block <= 0;
 gray_cache_high_bound : signed GRAY_CACHE_SIZE <= high_bound m gray_cache_block

}.

Record mark_abstraction_param : Set := make_mark_abstraction_param {
(* gray_cache_overflow_value : int; *)
 gray_cache_overflow_bool : bool;
 gray_cache_offset_value : int; (* which will also play the role of marksweep_cache_full *)
 marksweep_col : option (block * int) -> Mark_abstract.color;
 marksweep_cache : list (option (block * int))
}.

Definition marksweep_cache_is_full i := eq i GRAY_CACHE_SIZE.
Definition marksweep_cache_full_push i := add i four.
Definition marksweep_cache_full_pop i := sub i four.

Record mark_abstraction
  (m : mem) (mp : memory_param) (up : used_abstraction_param) (gp : gc_invariants_param) (p : mark_abstraction_param) : Prop :=
 mark_abstraction_intro
 {

 (* what really changes *)

(*  gray_cache_overflow_defined : Some (Vint (gray_cache_overflow_value p)) = load Mint32 m gray_cache_overflow_block 0; *)
  gray_cache_overflow_defined : Some (Vint (if gray_cache_overflow_bool p then one else zero)) = load Mint32 m gray_cache_overflow_block 0;

 gray_cache_offset_defined : Some (Vint (gray_cache_offset_value p)) = load Mint32 m gray_cache_offset_block 0;
 gray_cache_offset_lower_bounded : cmp Cle zero (gray_cache_offset_value p) = true;
 gray_cache_offset_higher_bounded : cmp Cle (gray_cache_offset_value p) GRAY_CACHE_SIZE = true;
 gray_cache_offset_modulo_four : modulo_four zero (gray_cache_offset_value p);

 col_black_a_c : forall b, member b (used_blocklist up) ->
 marksweep_col p (Some (memory_heap mp, b)) = Mark_abstract.Black -> forall v, Some (Vint v) = load Mint32 m (memory_heap mp) (signed (sub b four)) -> Color_header v = COLOR_BLACK;

 col_black_c_a : forall b, member b (used_blocklist up) ->
 forall v, Some (Vint v) = load Mint32 m (memory_heap mp) (signed (sub b four)) -> Color_header v = COLOR_BLACK -> marksweep_col p (Some (memory_heap mp, b)) = Mark_abstract.Black;

 col_gray_a_c : forall b, member b (used_blocklist up) ->
 marksweep_col p (Some (memory_heap mp, b)) = Mark_abstract.Gray -> forall v, Some (Vint v) = load Mint32 m (memory_heap mp) (signed (sub b four)) -> Color_header v = COLOR_GRAY;

 col_gray_c_a : forall b, member b (used_blocklist up) ->
 forall v, Some (Vint v) = load Mint32 m (memory_heap mp) (signed (sub b four)) -> Color_header v = COLOR_GRAY -> marksweep_col p (Some (memory_heap mp, b)) = Mark_abstract.Gray;

 col_white_a_c : forall b, member b (used_blocklist up) ->
 marksweep_col p (Some (memory_heap mp, b)) = Mark_abstract.White -> forall v, Some (Vint v) = load Mint32 m (memory_heap mp) (signed (sub b four)) -> Color_header v = COLOR_WHITE;

 col_white_c_a : forall b, member b (used_blocklist up) ->
 forall v, Some (Vint v) = load Mint32 m (memory_heap mp) (signed (sub b four)) -> Color_header v = COLOR_WHITE -> marksweep_col p (Some (memory_heap mp, b)) = Mark_abstract.White;

(* and the cache, hum ! *)
 cache_abstraction : pointer_list m gray_cache_block (sub zero four) (sub (gray_cache_offset_value p) four) (marksweep_cache p);

 (* further invariants to read the cache *)
 cache_elements_in_heap : forall b i, member (Some (b, i)) (marksweep_cache p) -> b = memory_heap mp;
 cache_elements_in_blocklist : forall b i, member (Some (b, i)) (marksweep_cache p) -> member i (used_blocklist up);
 cache_elements_not_null : member None (marksweep_cache p) -> False;

 (* further invariants for cache_pop not to pop raw elements *)
 cache_elements_not_raw : forall bi, member bi (marksweep_cache p) -> used_raw up bi = false;
 gray_elements_not_raw : forall bi, marksweep_col p bi = Mark_abstract.Gray -> used_raw up bi = false

}.

Hint Constructors marksweep_invariants mark_abstraction.
Hint Resolve
 marksweep_gc_inv
 gray_cache_offset_not_in_heap gray_cache_overflow_not_in_heap gray_cache_not_in_heap
 gray_cache_overflow_rootpos_indep gray_cache_rootpos_indep gray_cache_offset_rootpos_indep 
 gray_cache_valid gray_cache_low_bound gray_cache_high_bound
 gray_cache_overflow_defined gray_cache_offset_defined gray_cache_offset_lower_bounded gray_cache_offset_higher_bounded gray_cache_offset_modulo_four
 col_black_a_c col_black_c_a col_gray_a_c col_gray_c_a col_white_a_c col_white_c_a cache_abstraction
 cache_elements_in_heap cache_elements_in_blocklist cache_elements_not_null
 cache_elements_not_raw gray_elements_not_raw
.

Section Mark.

Variable mp : memory_param.
Variable gp : gc_invariants_param.

Section Gc_mark_body.

Variable up : used_abstraction_param.
Hypothesis up_extra_zero_false : used_extra_zero up = false.

(* Marksweep invariants and allocation *)
Section Mark_abstraction_alloc.
Variables a b : Z.
Variables m m' : mem.
Variable sp : block.
Hypothesis Hm' : alloc m a b = (m', sp).
Variable p : mark_abstraction_param.
Hypothesis Hm0 : marksweep_invariants m mp up gp.
Hypothesis Hm : mark_abstraction m mp up gp p.

Lemma alloc_gray_cache_overflow_indep : 
sp <> gray_cache_overflow_block.
Proof.
intro Habs.
subst.
generalize (gray_cache_overflow_defined Hm).
intro.
absurd (valid_block m gray_cache_overflow_block).
eapply fresh_block_alloc; eauto.
eapply valid_access_valid_block.
eapply load_valid_access.
symmetry.
eassumption.
Qed.

Lemma alloc_gray_cache_offset_indep :
sp <> gray_cache_offset_block.
Proof.
intro Habs.
subst.
absurd (valid_block m gray_cache_offset_block).
eapply fresh_block_alloc; eauto.
eapply valid_access_valid_block.
eapply load_valid_access.
symmetry.
eauto.
Qed.

Lemma alloc_gray_cache_indep :
sp <> gray_cache_block.
Proof.
intro Habs.
subst.
absurd (valid_block m gray_cache_block).
eapply fresh_block_alloc; eauto.
eauto.
Qed.

Lemma alloc_heap_start_indep :
sp <> heap_start_block.
Proof.
intro Habs.
subst.
absurd (valid_block m heap_start_block).
eapply fresh_block_alloc; eauto.
eapply valid_access_valid_block.
eapply load_valid_access.
symmetry.
eauto.
Qed.

Lemma alloc_heap_end_indep :
sp <> heap_end_block.
Proof.
intro Habs.
subst.
absurd (valid_block m heap_end_block).
eapply fresh_block_alloc; eauto.
eapply valid_access_valid_block.
eapply load_valid_access.
symmetry.
eauto.
Qed.

Lemma alloc_heap_indep :
sp <> memory_heap mp.
Proof.
intros Habs.
subst.
absurd (valid_block m (memory_heap mp)).
eapply fresh_block_alloc; eauto.
eauto.
Qed.

Lemma alloc_rootpos_indep :
forall r d, member (r, d) (flatten (used_rootpos up)) ->
sp <> r.
Proof.
intros r d Hrd Habs.
subst.
inversion Hm0.
inversion marksweep_gc_inv0.
inversion gc_used_hyp0.
destruct (all_roots_root_position_list_value (all_roots_describes used_roots_hyp) used_rootpos_hyp Hrd).
absurd (valid_block m r).
eapply fresh_block_alloc; eauto.
eapply valid_access_valid_block.
eapply load_valid_access.
symmetry.
eassumption.
Qed.

Lemma alloc_freelist_indep : 
sp <> freelist_head_block.
Proof.
intro Habs.
subst.
absurd (valid_block m freelist_head_block).
eapply fresh_block_alloc; eauto.
eapply valid_access_valid_block.
eapply load_valid_access.
symmetry.
eauto.
Qed.


Hint Resolve alloc_gray_cache_offset_indep alloc_gray_cache_overflow_indep alloc_gray_cache_indep
alloc_heap_start_indep alloc_heap_end_indep alloc_heap_indep alloc_rootpos_indep alloc_freelist_indep.


Theorem alloc_marksweep_invariants : marksweep_invariants m' mp up gp.
inversion Hm0.
inversion marksweep_gc_inv0.
inversion gc_used_hyp0.
apply marksweep_invariants_intro ; 
try (try rewrite <- (load_alloc_other_2 Hm'); auto).
apply gc_invariants_intro ;
try (try rewrite <- (load_alloc_other_2 Hm'); auto).
apply used_abstraction_intro ; try assumption;
try rewrite <- (load_alloc_other_2 Hm').

(* block_description_from_to *)
eapply block_description_samesize_inv.
eassumption.
intros b0 Hb0.
destruct (block_header used_heap_hyp Hb0); eapply ex_intro; eauto.
rewrite <- (load_alloc_other_3 Hm'); eauto.
(* same sizes *)
intros b0 Hb0.
rewrite <- (load_alloc_other_3 Hm').
intros; congruence.
eauto.
(* valid access *)
intros.
eapply valid_access_alloc_other.
eauto.
eapply block_description_valid; eauto.

(* sizes *)
intros b0 Hb0.
rewrite <- (load_alloc_other_3 Hm').
intros; eapply used_sizes_hyp; eauto.
eauto.

(* kinds *)
intros b0 Hb0.
rewrite <- (load_alloc_other_3 Hm').
intros; eapply used_kinds_hyp; eauto.
eauto.

(* extra zero : don't care *)
rewrite up_extra_zero_false.
discriminate 1.

(* raw data *)
intros.
rewrite <- (load_alloc_other_3 Hm').
intros; eapply used_rawdata_hyp; eauto.
eauto.

(* pointer_list_block (children) *)
intros b0 Hb0.
eapply pointer_list_block_invar.
eassumption.
intros b1 Hb1.
destruct (block_header used_heap_hyp Hb1); eapply ex_intro; eauto.
rewrite <- (load_alloc_other_3 Hm'); eauto.
intros b1 Hb1.
rewrite <- (load_alloc_other_3 Hm').
intros; congruence.
eauto.
intros b1 Hb1.
rewrite <- (load_alloc_other_3 Hm').
intros; congruence.
eauto.
intros.
rewrite <- (load_alloc_other_3 Hm').
intros; congruence.
eauto.
assumption.
eauto.

(* root positions *)
eapply root_position_list_invar.
eauto.
intros.
eapply load_alloc_other_3.
eassumption.
eauto.

(* all roots *)
eapply all_roots_invar.
eassumption.
eassumption.
intros b0 i Hb0.
eapply load_alloc_other_3.
eassumption.
eauto.

(* valid heap *)
eapply valid_block_alloc; eauto.

(* valid cache *)
eapply valid_block_alloc; eauto.

(* cache low bound *)
rewrite (low_bound_alloc _ _ _ _ _ Hm').
destruct (zeq gray_cache_block sp).
destruct alloc_gray_cache_indep.
auto.
eauto.

(* cache high bound *)
rewrite (high_bound_alloc _ _ _ _ _ Hm').
destruct (zeq gray_cache_block sp).
destruct alloc_gray_cache_indep.
auto.
eauto.
Qed.

Theorem alloc_mark_abstraction :
mark_abstraction m' mp up gp p.
Proof.
inversion Hm.
inversion Hm0.
inversion marksweep_gc_inv0.
inversion gc_used_hyp0.
apply mark_abstraction_intro ; 
try (rewrite <- (load_alloc_other_2 Hm'); [| auto]);
try assumption.

intros until 2; rewrite <- (load_alloc_other_2 Hm'); [| auto]; intros; eapply col_black_a_c0; eassumption.
intros until 1; introvars; rewrite <- (load_alloc_other_2 Hm'); [| auto] ; intros; eapply col_black_c_a0; eassumption.
intros until 2; rewrite <- (load_alloc_other_2 Hm'); [| auto]; intros; eapply col_gray_a_c0; eassumption.
intros until 1; introvars; rewrite <- (load_alloc_other_2 Hm'); [| auto]; intros; eapply col_gray_c_a0; eassumption.
intros until 2; rewrite <- (load_alloc_other_2 Hm'); [| auto] ; intros; eapply col_white_a_c0; eassumption.
intros until 1; introvars; rewrite <- (load_alloc_other_2 Hm'); [| auto]; intros; eapply col_white_c_a0; eassumption.

eapply cache_invar.
 eassumption.
   intro.
   apply modulo_four_le_m1_left.
    assumption.
    apply lt_is_le_p.
    apply lt_is_le_neq; auto.
 apply mod4_sym; auto.
intros; apply (load_alloc_other_2 Hm'); auto.
Qed.


(* So, what to do when this block is freed ? *)

Variables m'' m''' : mem.
Hypothesis Hm''0 : marksweep_invariants m'' mp up gp.

Theorem free_marksweep_invariants : marksweep_invariants (free m'' sp) mp up gp.
Proof.
inversion Hm''0.
inversion marksweep_gc_inv0.
inversion gc_used_hyp0.

eapply marksweep_invariants_intro ; try
(try rewrite load_free; auto).

eapply gc_invariants_intro; try
(try rewrite load_free; auto).

eapply used_abstraction_intro ; 
try (rewrite load_free; [| auto]);
try assumption.

(* block_description_from_to *)
eapply block_description_samesize_inv.
eassumption.
intros b0 Hb0.
destruct (block_header used_heap_hyp Hb0); eapply ex_intro; eauto.
rewrite load_free; eauto.
(* same sizes *)
intros b0 Hb0.
rewrite load_free.
intros; congruence.
eauto.
(* valid access *)
intros.
eapply valid_access_free_1.
eapply block_description_valid; eauto.
auto.

(* sizes *)
intros i Hi v.
rewrite load_free.
intros; eapply used_sizes_hyp; eauto.
eauto.

(* kinds *)
intros i Hi v.
rewrite load_free.
intros; eapply used_kinds_hyp; eauto.
eauto.

(* extra zero : don't care *)
rewrite up_extra_zero_false.
discriminate 1.

(* raw data *)
intros.
rewrite load_free.
intros; eapply used_rawdata_hyp; eauto.
eauto.

(* pointer_list_block *)
intros b0 Hb0.
eapply pointer_list_block_invar.
eassumption.
intros b1 Hb1.
destruct (block_header used_heap_hyp Hb1); eapply ex_intro; eauto.
rewrite load_free; eauto.
intros b1 Hb1.
rewrite load_free.
intros; congruence.
eauto.
intros b1 Hb1.
rewrite load_free.
intros; congruence.
eauto.
intros.
rewrite load_free.
intros; congruence.
eauto.
assumption.
eauto.


(* root positions *)
eapply root_position_list_invar.
eauto.
intros b0 i Hb0.
symmetry.
eapply load_free.
intro.
destruct (alloc_rootpos_indep Hb0).
auto.

(* all roots *)
eapply all_roots_invar.
eassumption.
eassumption.
intros b0 i Hb0.
symmetry.
eapply load_free.
intro.
destruct (alloc_rootpos_indep Hb0).
auto.

(* cache low bound *)
rewrite low_bound_free; eauto.

(* cache high bound *)
rewrite high_bound_free; eauto.
Qed.

Variable p'' : mark_abstraction_param.
Hypothesis Hm'' : mark_abstraction m'' mp up gp p''.


Theorem free_mark_abstraction :
mark_abstraction (free m'' sp) mp up gp p''.
Proof.
inversion Hm''.
inversion Hm''0.
inversion marksweep_gc_inv0.
inversion gc_used_hyp0.
apply mark_abstraction_intro ; 
try (rewrite load_free; [|auto]); try assumption.

intros until 2; rewrite load_free; [|auto]; intros; eapply col_black_a_c0; eassumption.
intros until 1; introvars; rewrite load_free; [|auto]; intros; eapply col_black_c_a0; eassumption.
intros until 2; rewrite load_free; [|auto]; intros; eapply col_gray_a_c0; eassumption.
intros until 1; introvars; rewrite load_free; [|auto]; intros; eapply col_gray_c_a0; eassumption.
intros until 2; rewrite load_free; [|auto]; intros; eapply col_white_a_c0; eassumption.
intros until 1; introvars; rewrite load_free; [|auto]; intros; eapply col_white_c_a0; eassumption.

eapply cache_invar.
 eassumption.
   intro.
   apply modulo_four_le_m1_left.
    assumption.
    apply lt_is_le_p.
    apply lt_is_le_neq; auto.
 apply mod4_sym; auto.
intros; symmetry; apply load_free; auto.
Qed.


End Mark_abstraction_alloc.

Section Mark_block_body.

Variable m : mem.
Variable p : mark_abstraction_param.

Hypothesis initial_state0 : marksweep_invariants m mp up gp.
Hypothesis initial_state : mark_abstraction m mp up gp p.

Variable bi : option (block * int).

Hypothesis bi_in_heap_1 : forall b i, bi = Some (b, i) -> b = memory_heap mp.
Hypothesis bi_in_heap_2 : forall b i, bi = Some (b, i) -> member i (used_blocklist up).

Definition mark_block_body_simplified_access :=
  match bi with
    | None => Some m
    | Some (b, i) =>
      match load Mint32 m b (signed (sub i four)) with
        | Some (Vint header) =>    
          if (negb (eq (Color_header header) COLOR_WHITE))
            then Some m
            else if eq (Kind_header header) KIND_RAWDATA
              then store Mint32 m b (signed (sub i four)) (Vint (or header COLOR_BLACK))
              else match store Mint32 m b (signed (sub i four)) (Vint (or header COLOR_GRAY)) with
                     | None => None 
                     | Some m1 =>
                       match load Mint32 m gray_cache_offset_block 0 with
                         | Some (Vint cache) =>
                           if eq cache GRAY_CACHE_SIZE
                             then store Mint32 m1 gray_cache_overflow_block 0 (Vint one) 
                             else match store Mint32 m1 gray_cache_block (signed cache) (Vptr b i) with
                                    | Some m2 =>
                                      store Mint32 m2 gray_cache_offset_block 0 (Vint (add cache four))
                                    | None => None 
                                  end
                         | _ => None
                       end
                   end
        | _ => None
      end
  end.

Theorem mark_block_body_simplified_access_equiv : mark_block_body m bi = mark_block_body_simplified_access.
Proof.
unfold mark_block_body.
unfold mark_block_body_simplified_access.
destruct bi as [p0 | ]; [ | auto ].
destruct p0.
generalize (bi_in_heap_1 (refl_equal _)).
intro ; subst.
generalize (bi_in_heap_2 (refl_equal _)).
intro Hi.
destruct (block_header (used_heap_hyp (gc_used_hyp (marksweep_gc_inv initial_state0))) Hi) as [v Hv].
rewrite <- Hv.
case (negb (eq (Color_header v) COLOR_WHITE)); auto.
case (eq (Kind_header v) KIND_RAWDATA); auto.
case_eq (store Mint32 m (memory_heap mp) (signed (sub i four)) (Vint (or v COLOR_GRAY))); [ | auto ].
intros m1 Hm1.
rewrite (load_store_other _ _ _ _ _ _ Hm1).
case (load Mint32 m gray_cache_offset_block 0); auto.
left; eauto.
Qed.

Theorem mark_block_body_runs_well : {m' | mark_block_body m bi = Some m'}.
Proof.
rewrite mark_block_body_simplified_access_equiv.
case_eq mark_block_body_simplified_access.
intros ; eapply exist; eauto.
intro Habs.
eapply False_rect.
genclear Habs.
unfold mark_block_body_simplified_access.
destruct bi as [p0 | ] ; try discriminate 1.
destruct p0 as [ b i ].
generalize (bi_in_heap_1 (refl_equal _)).
intro ; subst.
generalize (bi_in_heap_2 (refl_equal _)).
intro Hi.
destruct (block_header (used_heap_hyp (gc_used_hyp (marksweep_gc_inv initial_state0))) Hi) as [v Hv].
rewrite <- Hv.
rewrite <- (gray_cache_offset_defined initial_state).
case (negb (eq (Color_header v) COLOR_WHITE)); try discriminate 1.
case (eq (Kind_header v) KIND_RAWDATA).
unfold store.
generalize (load_valid_access _ _ _ _ _ (sym_equal Hv)).
intro Hvalid_heap.
destruct (in_bounds m Mint32 (memory_heap mp) (signed (sub i four))) ; intros; congruence.
case_eq (store Mint32 m (memory_heap mp) (signed (sub i four)) (Vint (or v COLOR_GRAY))).
intros m1 Hm1.
case_eq (eq (gray_cache_offset_value p) GRAY_CACHE_SIZE).
intro Hfull.
unfold store.
generalize (load_valid_access _ _ _ _ _ (sym_equal (gray_cache_overflow_defined initial_state))).
intro Hvalid_gco.
generalize (store_valid_access_1 _ _ _ _ _ _ Hm1 _ _ _ Hvalid_gco).
destruct (in_bounds m1 Mint32 gray_cache_overflow_block 0) ; intros; congruence.
intro Hnot_full.
case_eq (store Mint32 m1 gray_cache_block (signed (gray_cache_offset_value p)) (Vptr (memory_heap mp) i)).
intros m2 Hm2.
unfold store.
generalize (load_valid_access _ _ _ _ _ (sym_equal (gray_cache_offset_defined initial_state))).
intro Hvalid_gcof.
generalize (store_valid_access_1 _ _ _ _ _ _ Hm1 _ _ _ Hvalid_gcof).
intro Hvalid_gcof1.
generalize (store_valid_access_1 _ _ _ _ _ _ Hm2 _ _ _ Hvalid_gcof1).
intro.
destruct (in_bounds m2 Mint32 gray_cache_offset_block 0); intros; congruence.
(* the most difficult : cache valid. *)
generalize (neq_bool_neq_prop Hnot_full).
intro Hcache_not_full.
destruct (modulo_four_le_eq_or_next (a := gray_cache_offset_value p) (b := GRAY_CACHE_SIZE)).
eapply mod4_sym.
eapply mod4_trans.
eapply four_divides_gray_cache_size.
eapply gray_cache_offset_modulo_four.
eassumption.
eauto.
contradiction.
invall.
assert (valid_access m Mint32 gray_cache_block (signed (gray_cache_offset_value p))) as Hvalid.
 apply valid_access_intro.
 eauto.
 eapply Zle_trans.
 eauto.
 change 0 with (signed zero).
 eauto.
 change (size_chunk Mint32) with (signed four).
 rewrite <- plus_positive.
 eapply Zle_trans.
 eapply le_is_signed_le.
 eassumption.
 eauto.
 assumption.
 reflexivity.
generalize (store_valid_access_1 _ _ _ _ _ _ Hm1 _ _ _ Hvalid).
intro Hvalid1.
unfold store.
destruct (in_bounds m1 Mint32 gray_cache_block (signed (gray_cache_offset_value p))); intros; congruence.

(* then, the last case : white *)
unfold store.
generalize (load_valid_access _ _ _ _ _ (sym_equal Hv)).
intro Hvalid.
destruct (in_bounds m Mint32 (memory_heap mp) (signed (sub i four))); intros; congruence.

Defined.

Variable m' : mem.
Hypothesis Hm' : mark_block_body m bi = Some m'.

Theorem mark_block_body_valid_block_invar : forall b', valid_block m b' -> valid_block m' b'.
Proof.
intro.
genclear Hm'.
unfold mark_block_body.
destruct bi; try (intros; replace m' with m ; congruence).
destruct p0.
destruct (load Mint32 m b (signed (sub i four))); try (intros; discriminate).
destruct v ; try (intros; discriminate).
destruct (negb (eq (Color_header i0) COLOR_WHITE)); try (intros; replace m' with m ; congruence).
destruct (eq (Kind_header i0) KIND_RAWDATA).
intros; eapply store_valid_block_1; eauto.
case_eq (store Mint32 m b (signed (sub i four)) (Vint (or i0 COLOR_GRAY)));
try (intros; discriminate).
intros m1 Hm1.
destruct (load Mint32 m1 gray_cache_offset_block 0); try (intros; discriminate).
destruct v; try (intros; discriminate).
destruct (eq i1 GRAY_CACHE_SIZE).
intros; repeat ( eapply store_valid_block_1; eauto).
case_eq (store Mint32 m1 gray_cache_block (signed i1) (Vptr b i)); try (intros; discriminate).
intros; repeat ( eapply store_valid_block_1; eauto).
Qed.

Theorem mark_block_body_valid_access_invar : forall c b' i', valid_access m c b' i' -> valid_access m' c b' i'.
Proof.
intro.
genclear Hm'.
unfold mark_block_body.
destruct bi; try (intros; replace m' with m ; congruence).
destruct p0.
destruct (load Mint32 m b (signed (sub i four))); try (intros; discriminate).
destruct v ; try (intros; discriminate).
destruct (negb (eq (Color_header i0) COLOR_WHITE)); try (intros; replace m' with m ; congruence).
destruct (eq (Kind_header i0) KIND_RAWDATA).
intros; eapply store_valid_access_1; eauto.
case_eq (store Mint32 m b (signed (sub i four)) (Vint (or i0 COLOR_GRAY)));
try (intros; discriminate).
intros m1 Hm1.
destruct (load Mint32 m1 gray_cache_offset_block 0); try (intros; discriminate).
destruct v; try (intros; discriminate).
destruct (eq i1 GRAY_CACHE_SIZE).
intros; repeat ( eapply store_valid_access_1; eauto).
case_eq (store Mint32 m1 gray_cache_block (signed i1) (Vptr b i)); try (intros; discriminate).
intros; repeat ( eapply store_valid_access_1; eauto).
Qed.

Proposition mark_block_body_invariant_blocks :
forall x,
x <> gray_cache_block ->
x <> memory_heap mp ->
x <> gray_cache_offset_block ->
x <> gray_cache_overflow_block ->
forall c i, load c m x i = load c m' x i.
Proof.
intros x Hx_not_in_cache Hx_not_in_heap Hx_not_in_cache_offset Hx_not_in_cache_overflow.
genclear Hm'.
rewrite mark_block_body_simplified_access_equiv.
unfold mark_block_body_simplified_access.
destruct bi ; try (intros; congruence).
destruct p0.
generalize (bi_in_heap_1 (refl_equal _)).
intro ; subst.
generalize (bi_in_heap_2 (refl_equal _)).
intro Hi.
destruct (block_header (used_heap_hyp (gc_used_hyp (marksweep_gc_inv initial_state0))) Hi) as [v Hv].
rewrite <- Hv.
rewrite <- (gray_cache_offset_defined initial_state).
case (negb (eq (Color_header v) COLOR_WHITE)); try (intros; congruence).
case (eq (Kind_header v) KIND_RAWDATA).
 intro Hm'.
 intros.
 symmetry.
 eapply load_store_other.
 eassumption.
 auto.
case_eq (store Mint32 m (memory_heap mp) (signed (sub i four)) (Vint (or v COLOR_GRAY)));
try (intros; discriminate).
intros m1 Hm1.
case (eq (gray_cache_offset_value p) GRAY_CACHE_SIZE).
 intros Hm'.
 intros.
 symmetry.
 eapply trans_equal.
  eapply load_store_other.
  eassumption.
  auto.
 eapply load_store_other.
 eassumption.
 auto.
case_eq (store Mint32 m1 gray_cache_block (signed (gray_cache_offset_value p)) (Vptr (memory_heap mp) i));
try (intros; discriminate).
intros m2 Hm2 Hm'.
intros.
symmetry.
eapply trans_equal.
 eapply load_store_other.
 eassumption.
 auto.
eapply trans_equal.
 eapply load_store_other.
 eassumption.
 auto.
eapply load_store_other.
eassumption.
auto.
Qed.

Proposition mark_block_body_header_change : forall i,
bi = Some (memory_heap mp, i) -> forall v, Some (Vint v) = load Mint32 m (memory_heap mp) (signed (sub i four)) ->
  load Mint32 m' (memory_heap mp) (signed (sub i four)) = Some (Vint (
    if (negb (eq (Color_header v) COLOR_WHITE))
      then v
      else if eq (Kind_header v) KIND_RAWDATA
        then (or v COLOR_BLACK)
        else (or v COLOR_GRAY)
  )).
Proof.
intros i Hi v Hv.
genclear Hm'.
rewrite mark_block_body_simplified_access_equiv.
unfold mark_block_body_simplified_access.
subst.
rewrite <- Hv.
case (negb (eq (Color_header v) COLOR_WHITE)).
congruence.
case (eq (Kind_header v) KIND_RAWDATA).
intro Hm'.
rewrite (load_store_same _ _ _ _ _ _ Hm').
reflexivity.
case_eq (store Mint32 m (memory_heap mp) (signed (sub i four)) (Vint (or v COLOR_GRAY)));
try (intros; discriminate).
intros m1 Hm1.
rewrite <- (gray_cache_offset_defined initial_state).
case (eq (gray_cache_offset_value p) GRAY_CACHE_SIZE).
 intro Hm'.
 rewrite (load_store_other _ _ _ _ _ _ Hm'); eauto.
 rewrite (load_store_same _ _ _ _ _ _ Hm1).
 reflexivity.
 left ; intro; destruct (gray_cache_overflow_not_in_heap initial_state0); congruence.
case_eq (store Mint32 m1 gray_cache_block (signed (gray_cache_offset_value p)) (Vptr (memory_heap mp) i));
try (intros; discriminate). 
intros m2 Hm2.
intros Hm'.
rewrite (load_store_other _ _ _ _ _ _ Hm').
rewrite (load_store_other _ _ _ _ _ _ Hm2).
rewrite (load_store_same _ _ _ _ _ _ Hm1).
reflexivity.
left; intro; destruct (gray_cache_not_in_heap initial_state0); congruence.
left; intro; destruct (gray_cache_offset_not_in_heap initial_state0); congruence.
Qed.

Corollary mark_block_body_kind_and_size_invar : forall i v v', bi = Some (memory_heap mp, i) ->
Some (Vint v) = load Mint32 m (memory_heap mp) (signed (sub i four)) ->
Some (Vint v') = load Mint32 m' (memory_heap mp) (signed (sub i four)) ->
Kind_header v' = Kind_header v /\ Size_header v' = Size_header v.
Proof.
intros i v v' Hbi Hv Hv'.
rewrite (mark_block_body_header_change Hbi Hv) in Hv'.
injection Hv'.
intros ; subst.
case (negb (eq (Color_header v) COLOR_WHITE)); auto.
case (eq (Kind_header v) KIND_RAWDATA) ; split. 
apply kind_header_color_inv; auto.
apply size_header_color_inv; auto.
apply kind_header_color_inv; auto.
apply size_header_color_inv; auto.
Qed.

Lemma mark_block_body_other_blocks_invar : forall i, bi = Some (memory_heap mp, i) ->
forall i', (i = i' -> False) -> modulo_four i i' ->
load Mint32 m (memory_heap mp) (signed (sub i' four)) =
load Mint32 m' (memory_heap mp) (signed (sub i' four)).

Proof.
intros i Hbi i' Hdiff Hi_mod.
assert (sub i four <> sub i' four).
 repeat rewrite sub_add_opp.
 intro Habs.
 destruct Hdiff.
 eapply add_reg_r; eauto.
assert (modulo_four (sub i four) (sub i' four)).
 eapply mod4_sub; eauto.
genclear Hm'.
rewrite mark_block_body_simplified_access_equiv.
unfold mark_block_body_simplified_access.
subst.
generalize (bi_in_heap_2 (refl_equal _)).
intro Hi.
destruct (block_header (used_heap_hyp (gc_used_hyp (marksweep_gc_inv initial_state0))) Hi) as [v Hv].
rewrite <- Hv.
rewrite <- (gray_cache_offset_defined initial_state).
case (negb (eq (Color_header v) COLOR_WHITE)); try (intros; congruence).
case (eq (Kind_header v) KIND_RAWDATA).
 intro Hm'.
 eapply get_set_int32_indep ; try symmetry ; eauto.
case_eq (store Mint32 m (memory_heap mp) (signed (sub i four)) (Vint (or v COLOR_GRAY)));
try (intros; discriminate).
intros m1 Hm1.
case (eq (gray_cache_offset_value p) GRAY_CACHE_SIZE).
 intros Hm'.
 eapply trans_equal.
 eapply get_set_int32_indep; try symmetry; eauto.
 symmetry.
 eapply load_store_other.
 eassumption.
 left; intro ; destruct (gray_cache_overflow_not_in_heap initial_state0); eauto.
case_eq (store Mint32 m1 gray_cache_block (signed (gray_cache_offset_value p)) (Vptr (memory_heap mp) i));
try (intros; discriminate).
intros m2 Hm2 Hm'.
eapply trans_equal.
eapply get_set_int32_indep; try symmetry; eauto.
symmetry.
eapply trans_equal.
eapply load_store_other.
 eassumption.
 left; intro; destruct (gray_cache_offset_not_in_heap initial_state0); eauto.
eapply load_store_other.
eassumption.
left; intro; destruct (gray_cache_not_in_heap initial_state0); eauto.
Qed.

Corollary mark_block_body_blocks_exist : 
forall i', member i' (used_blocklist up) -> exists v', Some (Vint v') = load Mint32 m' (memory_heap mp) (signed (sub i' four)).
Proof.
intros i' Hi'.
destruct (block_header (used_heap_hyp (gc_used_hyp (marksweep_gc_inv initial_state0))) Hi') as [v' Hv'].
case_eq bi.

destruct p0.
intro Hbi.
generalize (bi_in_heap_1 Hbi).
intro ; subst b.
generalize (bi_in_heap_2 Hbi).
intro Hi.
destruct (eq_dec i i').
subst i'.
generalize (mark_block_body_header_change Hbi Hv').
intro; eapply ex_intro; eauto.
rewrite <- (mark_block_body_other_blocks_invar Hbi n).
eapply ex_intro; eauto.
eapply block_description_modulo_four.
eapply used_heap_hyp; eauto.
assumption.
assumption.
intro ; subst.
simpl in Hm'.
eapply ex_intro. 
injection Hm'; intros; subst; eauto.
Qed.

Corollary mark_block_body_kind_invar : 
forall i', member i' (used_blocklist up) -> forall v,
Some (Vint v) = load Mint32 m (memory_heap mp) (signed (sub i' four)) ->
forall v', Some (Vint v') = load Mint32 m' (memory_heap mp) (signed (sub i' four)) ->
Kind_header v = Kind_header v'.
Proof.
intros i' Hi' v Hv v' Hv'.
case_eq bi.

destruct p0.
intro Hbi.
generalize (bi_in_heap_1 Hbi).
intro ; subst b.
generalize (bi_in_heap_2 Hbi).
intro Hi.
destruct (eq_dec i i').
subst i'.
generalize (mark_block_body_kind_and_size_invar Hbi Hv Hv').
inversion 1; auto.
rewrite <- (mark_block_body_other_blocks_invar Hbi n) in Hv'.
congruence.
eapply block_description_modulo_four.
eapply used_heap_hyp; eauto.
assumption.
assumption.
intro ; subst.
simpl in Hm'.
congruence.
Qed.


Corollary mark_block_body_size_invar : 
forall i', member i' (used_blocklist up) -> forall v,
Some (Vint v) = load Mint32 m (memory_heap mp) (signed (sub i' four)) ->
forall v', Some (Vint v') = load Mint32 m' (memory_heap mp) (signed (sub i' four)) ->
Size_header v = Size_header v'.
Proof.
intros i' Hi' v Hv v' Hv'.
case_eq bi.

destruct p0.
intro Hbi.
generalize (bi_in_heap_1 Hbi).
intro ; subst b.
generalize (bi_in_heap_2 Hbi).
intro Hi.
destruct (eq_dec i i').
subst i'.
generalize (mark_block_body_kind_and_size_invar Hbi Hv Hv').
inversion 1; auto.
rewrite <- (mark_block_body_other_blocks_invar Hbi n) in Hv'.
congruence.
eapply block_description_modulo_four.
eapply used_heap_hyp; eauto.
assumption.
assumption.
intro ; subst.
simpl in Hm'.
congruence.
Qed.

Corollary mark_block_body_block_description_invar : 
block_description_from_to m' (memory_heap mp) (memory_hs mp) (memory_he mp) (used_blocklist up).
Proof.
eapply block_description_samesize_inv.
eapply used_heap_hyp; eauto.
apply mark_block_body_blocks_exist; auto.
apply mark_block_body_size_invar.
intros; apply mark_block_body_valid_access_invar. 
eapply block_description_valid; eauto.
eapply used_heap_hyp; eauto.
Qed.

Lemma mark_block_body_invar_data : 
forall b', member b' (used_blocklist up) ->
forall v', Some (Vint v') = load Mint32 m (memory_heap mp) (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 (memory_heap mp) (signed x) = load Mint32 m' (memory_heap mp) (signed x).
Proof.
intros b' Hb' v' Hv' Hb'nonempty x xlo xhi Hx_mod4.
case_eq bi.
destruct p0.
intro Hbi.
generalize (bi_in_heap_1 Hbi).
intro ; subst b.
generalize (bi_in_heap_2 Hbi).
intro Hi.
destruct (block_header (used_heap_hyp (gc_used_hyp (marksweep_gc_inv initial_state0))) Hi) as [v Hv].
rewrite <- (add_sub_id x four).
eapply mark_block_body_other_blocks_invar.
eassumption.
rewrite <- (sub_add_id i four).
intro Habs.
symmetry in Habs.
generalize (add_reg_r Habs).
cut (x <> sub i four).
auto.
eapply block_description_data_header_disjoint.
eapply used_heap_hyp; eauto.
eexact Hb'.
eassumption.
assumption.
assumption.
assumption.
assumption.
eapply mod4_trans.
eapply block_description_modulo_four.
eapply used_heap_hyp; eauto.
assumption.
eexact Hb'.
eapply mod4_trans.
eassumption.
apply modulo_four_four_divides_add.
exact four_divides_four.
intro ; subst. 
simpl in Hm'; congruence.

Qed.

Theorem mark_block_body_same_low_bounds : forall b', low_bound m b' = low_bound m' b'.
Proof.
intro.
genclear Hm'.
unfold mark_block_body.
destruct bi; try (intros; congruence).
destruct p0.
destruct (load Mint32 m b (signed (sub i four))); try (intros; discriminate).
destruct v ; try (intros; discriminate).
destruct (negb (eq (Color_header i0) COLOR_WHITE)); try (intros; congruence).
destruct (eq (Kind_header i0) KIND_RAWDATA).
symmetry; eapply low_bound_store; eauto.
case_eq (store Mint32 m b (signed (sub i four)) (Vint (or i0 COLOR_GRAY)));
try (intros; discriminate).
intros m1 Hm1.
destruct (load Mint32 m1 gray_cache_offset_block 0); try (intros; discriminate).
destruct v; try (intros; discriminate).
destruct (eq i1 GRAY_CACHE_SIZE).
intro Hm'.
symmetry.
eapply trans_equal; eapply low_bound_store; eauto.
case_eq (store Mint32 m1 gray_cache_block (signed i1) (Vptr b i)); try (intros; discriminate).
intros m2 Hm2 Hm'.
symmetry.
eapply trans_equal. 
eapply trans_equal; eapply low_bound_store; eauto.
eapply low_bound_store; eauto.
Qed.

Theorem mark_block_body_same_high_bounds : forall b', high_bound m b' = high_bound m' b'.
Proof.
intro.
genclear Hm'.
unfold mark_block_body.
destruct bi; try (intros; congruence).
destruct p0.
destruct (load Mint32 m b (signed (sub i four))); try (intros; discriminate).
destruct v ; try (intros; discriminate).
destruct (negb (eq (Color_header i0) COLOR_WHITE)); try (intros; congruence).
destruct (eq (Kind_header i0) KIND_RAWDATA).
symmetry; eapply high_bound_store; eauto.
case_eq (store Mint32 m b (signed (sub i four)) (Vint (or i0 COLOR_GRAY)));
try (intros; discriminate).
intros m1 Hm1.
destruct (load Mint32 m1 gray_cache_offset_block 0); try (intros; discriminate).
destruct v; try (intros; discriminate).
destruct (eq i1 GRAY_CACHE_SIZE).
intro Hm'.
symmetry.
eapply trans_equal; eapply high_bound_store; eauto.
case_eq (store Mint32 m1 gray_cache_block (signed i1) (Vptr b i)); try (intros; discriminate).
intros m2 Hm2 Hm'.
symmetry.
eapply trans_equal. 
eapply trans_equal; eapply high_bound_store; eauto.
eapply high_bound_store; eauto.
Qed.

Theorem mark_block_body_final_gc_state : marksweep_invariants m' mp up gp.
inversion initial_state0.
inversion initial_state.
inversion marksweep_gc_inv0.
inversion gc_used_hyp0.
apply marksweep_invariants_intro; try (
try rewrite <- mark_block_body_invariant_blocks; eauto
).
apply gc_invariants_intro; try (
try rewrite <- mark_block_body_invariant_blocks; eauto
).
apply used_abstraction_intro; try assumption.

(* block description *)
apply mark_block_body_block_description_invar.

(* sizes *)
intros b Hb v' Hv'.
destruct (block_header used_heap_hyp Hb) as [v Hv].
rewrite <- (mark_block_body_size_invar Hb Hv Hv').
intros; eapply used_sizes_hyp; eassumption.

(* kinds *)
intros b Hb v' Hv'.
destruct (block_header used_heap_hyp Hb) as [v Hv].
rewrite <- (mark_block_body_kind_invar Hb Hv Hv').
intros; eapply used_kinds_hyp; eassumption.

(* extra zero : don't care *)
rewrite up_extra_zero_false.
discriminate 1.

(* raw data *)
intros i Hi.
destruct (block_header used_heap_hyp Hi) as [v Hv].
intros Hk Hs x xlo xhi x_mod4.
generalize Hs xhi.
rewrite <- (used_sizes_hyp _ Hi _ Hv).
intros H_not_null xhi2.
rewrite <- (mark_block_body_invar_data Hi Hv H_not_null xlo xhi2 (mod4_sym x_mod4)).
eapply used_rawdata_hyp; eassumption.

(* pointer list block *)
intros b Hb.
eapply pointer_list_block_invar;try eassumption.
intros ; eapply mark_block_body_blocks_exist; eauto.
intros; eapply mark_block_body_kind_invar; eauto.
intros; eapply mark_block_body_size_invar; eauto.
intros; eapply mark_block_body_invar_data; eauto.
eauto.

(* root positions *)
eapply root_position_list_invar; try eassumption.
intros; symmetry;
rewrite mark_block_body_invariant_blocks; eauto.

(* all roots *)
eapply all_roots_invar.
eassumption.
eassumption.
intros; symmetry;
rewrite mark_block_body_invariant_blocks; eauto.

(* valid heap *)
eapply mark_block_body_valid_block_invar; eauto.

(* valid gray cache *)
eapply mark_block_body_valid_block_invar; eauto.

(* cache low bound *)
rewrite <- mark_block_body_same_low_bounds; eauto.

(* cache high bound *)
rewrite <- mark_block_body_same_high_bounds; eauto.

Qed.

Definition mark_block_post_param := 
let (col', occ) :=
Mark_abstract.mark_block (used_valid mp up) eq_optptr marksweep_cache_is_full marksweep_cache_full_push (used_raw up) (marksweep_col p) (gray_cache_overflow_bool p) (marksweep_cache p) (gray_cache_offset_value p) bi in
let (oc, cache_full') := occ in
let (overflow', cache') := oc in
  make_mark_abstraction_param
  overflow'
  cache_full'
  col'
  cache'.

Let p' := mark_block_post_param.

Theorem mark_block_body_final_state :
mark_abstraction m' mp up gp p'.
Proof.
unfold p'.
unfold mark_block_post_param.
generalize Hm'.
rewrite mark_block_body_simplified_access_equiv.
unfold mark_block_body_simplified_access.
unfold Mark_abstract.mark_block.
inversion initial_state0.
inversion marksweep_gc_inv0.
inversion gc_used_hyp0.
inversion initial_state.
case_eq bi.

(* case valid *)
destruct p0.
intro Hbi.
generalize (bi_in_heap_1 Hbi).
intro ; subst b.
generalize (bi_in_heap_2 Hbi).
intro Hi.
destruct (block_header used_heap_hyp Hi) as [v Hv].
rewrite <- Hv.
rewrite <- gray_cache_offset_defined0.
generalize (Hvalid_prop_bool (mp := mp) (refl_equal _) Hi).
intro Hvalid.
rewrite Hvalid.
case_eq (eq (Color_header v) COLOR_WHITE) ; simpl.
(* case white *)
intro Hwhite_bool.
generalize (eq_bool_eq_prop Hwhite_bool).
intro Hwhite_prop.
generalize (col_white_c_a0 _ Hi _ Hv Hwhite_prop).
intro Hwhite_abs.
rewrite Hwhite_abs.
rewrite <- (used_kinds_hyp _ Hi _ Hv).
case_eq (eq (Kind_header v) KIND_RAWDATA).
(* case raw *)
intro Hraw_bool.
generalize (eq_bool_eq_prop Hraw_bool).
intro Hraw_prop.
generalize (used_raw_prop_bool gc_used_hyp0 Hi Hv Hraw_prop).
intro Hraw_abs.
(* rewrite Hraw_abs. *)
intro Hm'0.
apply mark_abstraction_intro; simpl; try assumption.
rewrite (load_store_other _ _ _ _ _ _ Hm'0).
auto.
left; eauto.
rewrite (load_store_other _ _ _ _ _ _ Hm'0); auto.
intros b Hb.
unfold Mark_abstract.set_color.
destruct (eq_optptr (Some (memory_heap mp, b)) (Some (memory_heap mp, i)))
as [Heq | Hneq ].
injection Heq.
intros ? _ ; subst b.
intros v'.
rewrite (mark_block_body_header_change Hbi Hv).
rewrite Hwhite_bool; simpl.
rewrite Hraw_bool; simpl.
injection 1; intro; subst v'.
apply color_header_white_var.
assumption.
auto.
assert (b <> i) as Hneq2.
 intro ; congruence.
intros Hcol_abs v0.
rewrite <- (mark_block_body_other_blocks_invar Hbi).
intro ; eapply col_black_a_c0 ; eassumption.
congruence.
eapply block_description_modulo_four; eassumption.
intros b Hb.
unfold Mark_abstract.set_color.
destruct (eq_optptr (Some (memory_heap mp, b)) (Some (memory_heap mp, i)))
as [ | Hneq ]; auto.
assert (b <> i) as Hneq2.
 intro ; congruence.
intros v0.
rewrite <- (mark_block_body_other_blocks_invar Hbi).
intros ; eapply col_black_c_a0 ; eassumption.
congruence.
eapply block_description_modulo_four; eassumption.
intros b Hb.
unfold Mark_abstract.set_color.
destruct (eq_optptr (Some (memory_heap mp, b)) (Some (memory_heap mp, i)))
as [Heq | Hneq ] ; try (intros; discriminate).
assert (b <> i) as Hneq2.
 intro ; congruence.
intros Hcol_abs v0.
rewrite <- (mark_block_body_other_blocks_invar Hbi).
intro ; eapply col_gray_a_c0 ; eassumption.
congruence.
eapply block_description_modulo_four; eassumption.
intros b Hb.
unfold Mark_abstract.set_color.
destruct (eq_optptr (Some (memory_heap mp, b)) (Some (memory_heap mp, i)))
as [ Heq | Hneq ].
injection Heq; intro; subst b.
intro v0.
rewrite (mark_block_body_header_change Hbi Hv).
rewrite Hwhite_bool; simpl.
rewrite Hraw_bool; simpl.
injection 1; intro; subst v0.
rewrite (color_header_white_var Hwhite_prop).
inversion 1.
auto.
assert (b <> i) as Hneq2.
 intro ; congruence.
intros v0.
rewrite <- (mark_block_body_other_blocks_invar Hbi).
intros ; eapply col_gray_c_a0 ; eassumption.
congruence.
eapply block_description_modulo_four; eassumption.
intros b Hb.
unfold Mark_abstract.set_color.
destruct (eq_optptr (Some (memory_heap mp, b)) (Some (memory_heap mp, i)))
as [Heq | Hneq ] ; try (intros; discriminate).
assert (b <> i) as Hneq2.
 intro ; congruence.
intros Hcol_abs v0.
rewrite <- (mark_block_body_other_blocks_invar Hbi).
intro ; eapply col_white_a_c0 ; eassumption.
congruence.
eapply block_description_modulo_four; eassumption.
intros b Hb.
unfold Mark_abstract.set_color.
destruct (eq_optptr (Some (memory_heap mp, b)) (Some (memory_heap mp, i)))
as [ Heq | Hneq ].
injection Heq; intro; subst b.
intro v0.
rewrite (mark_block_body_header_change Hbi Hv).
rewrite Hwhite_bool; simpl.
rewrite Hraw_bool; simpl.
injection 1; intro; subst v0.
rewrite (color_header_white_var Hwhite_prop).
inversion 1.
auto.
assert (b <> i) as Hneq2.
 intro ; congruence.
intros v0.
rewrite <- (mark_block_body_other_blocks_invar Hbi).
intros ; eapply col_white_c_a0 ; eassumption.
congruence.
eapply block_description_modulo_four; eassumption.
(* and the cache... *)
(* eapply pointer_list_invar. # nope. try cache_invar instead *)
eapply cache_invar.
    eassumption.
   intro.
   apply modulo_four_le_m1_left.
    assumption.
    apply lt_is_le_p.
    apply lt_is_le_neq; auto.
 apply mod4_sym; auto.
intros; symmetry; apply (load_store_other _ _ _ _ _ _ Hm'0); auto.
(* no gray object raw *)
intros bi0.
unfold Mark_abstract.set_color.
destruct (eq_optptr bi0 (Some (memory_heap mp, i))).
 discriminate 1.
intros; eapply gray_elements_not_raw0; eauto.

(* case not raw *)
intro Hnot_raw_bool.
generalize (neq_bool_neq_prop Hnot_raw_bool).
intro Hnot_raw_prop.
(*
case_eq (used_raw up (Some (memory_heap mp, i))).
 intro Habs.
 generalize (used_raw_bool_prop gc_used_hyp0 Hi Habs Hv).
 intro ; contradiction.
intro Hnot_used_raw.
*)
case_eq (store Mint32 m (memory_heap mp) (signed (sub i four)) (Vint (or v COLOR_GRAY))); try (intros; discriminate).
intros m1 Hm1.
unfold Mark_abstract.cache_push.
unfold marksweep_cache_is_full.
case_eq (eq (gray_cache_offset_value p) GRAY_CACHE_SIZE).
(* case cache full *)
intro Hfull_prop.
generalize (eq_bool_eq_prop Hfull_prop).
intro Hfull_bool.
intro Hm'0.
apply mark_abstraction_intro; simpl; try assumption.
rewrite (load_store_same _ _ _ _ _ _ Hm'0).
reflexivity.
rewrite (load_store_other _ _ _ _ _ _ Hm'0); auto.
rewrite (load_store_other _ _ _ _ _ _ Hm1); auto.
intros b Hb.
unfold Mark_abstract.set_color.
destruct (eq_optptr (Some (memory_heap mp, b)) (Some (memory_heap mp, i)))
as [Heq | Hneq ] ; try (intros; discriminate).
assert (b <> i) as Hneq2.
 intro ; congruence.
intros Hcol_abs v0.
rewrite <- (mark_block_body_other_blocks_invar Hbi).
intro ; eapply col_black_a_c0 ; eassumption.
congruence.
eapply block_description_modulo_four; eassumption.
intros b Hb.
unfold Mark_abstract.set_color.
destruct (eq_optptr (Some (memory_heap mp, b)) (Some (memory_heap mp, i)))
as [ Heq | Hneq ].
injection Heq; intro; subst b.
intro v0.
rewrite (mark_block_body_header_change Hbi Hv).
rewrite Hwhite_bool; simpl.
rewrite Hnot_raw_bool; simpl.
injection 1; intro; subst v0.
rewrite (color_header_white_var Hwhite_prop).
inversion 1.
auto.
assert (b <> i) as Hneq2.
 intro ; congruence.
intros v0.
rewrite <- (mark_block_body_other_blocks_invar Hbi).
intros ; eapply col_black_c_a0 ; eassumption.
congruence.
eapply block_description_modulo_four; eassumption.
intros b Hb.
unfold Mark_abstract.set_color.
destruct (eq_optptr (Some (memory_heap mp, b)) (Some (memory_heap mp, i)))
as [Heq | Hneq ].
injection Heq.
intros ? _ ; subst b.
intros v'.
rewrite (mark_block_body_header_change Hbi Hv).
rewrite Hwhite_bool; simpl.
rewrite Hnot_raw_bool; simpl.
injection 1; intro; subst v'.
apply color_header_white_var.
assumption.
auto.
assert (b <> i) as Hneq2.
 intro ; congruence.
intros Hcol_abs v0.
rewrite <- (mark_block_body_other_blocks_invar Hbi).
intro ; eapply col_gray_a_c0 ; eassumption.
congruence.
eapply block_description_modulo_four; eassumption.
intros b Hb.
unfold Mark_abstract.set_color.
destruct (eq_optptr (Some (memory_heap mp, b)) (Some (memory_heap mp, i)))
as [ | Hneq ]; auto.
assert (b <> i) as Hneq2.
 intro ; congruence.
intros v0.
rewrite <- (mark_block_body_other_blocks_invar Hbi).
intros ; eapply col_gray_c_a0 ; eassumption.
congruence.
eapply block_description_modulo_four; eassumption.
intros b Hb.
unfold Mark_abstract.set_color.
destruct (eq_optptr (Some (memory_heap mp, b)) (Some (memory_heap mp, i)))
as [Heq | Hneq ] ; try (intros; discriminate).
assert (b <> i) as Hneq2.
 intro ; congruence.
intros Hcol_abs v0.
rewrite <- (mark_block_body_other_blocks_invar Hbi).
intro ; eapply col_white_a_c0 ; eassumption.
congruence.
eapply block_description_modulo_four; eassumption.
intros b Hb.
unfold Mark_abstract.set_color.
destruct (eq_optptr (Some (memory_heap mp, b)) (Some (memory_heap mp, i)))
as [ Heq | Hneq ].
injection Heq; intro; subst b.
intro v0.
rewrite (mark_block_body_header_change Hbi Hv).
rewrite Hwhite_bool; simpl.
rewrite Hnot_raw_bool; simpl.
injection 1; intro; subst v0.
rewrite (color_header_white_var Hwhite_prop).
inversion 1.
auto.
assert (b <> i) as Hneq2.
 intro ; congruence.
intros v0.
rewrite <- (mark_block_body_other_blocks_invar Hbi).
intros ; eapply col_white_c_a0 ; eassumption.
congruence.
eapply block_description_modulo_four; eassumption.
(* and the cache... *)
(* eapply pointer_list_invar. # nope. try cache_invar instead *)
eapply cache_invar.
    eassumption.
   intro.
   apply modulo_four_le_m1_left.
    assumption.
    apply lt_is_le_p.
    apply lt_is_le_neq; auto.
   auto.
 auto.
 apply mod4_sym; auto.
intros; symmetry.
eapply trans_equal.
apply (load_store_other _ _ _ _ _ _ Hm'0).
auto.
apply (load_store_other _ _ _ _ _ _ Hm1).
auto.
(* no gray elements raw *)
intros b0.
unfold Mark_abstract.set_color.
destruct (eq_optptr b0 (Some (memory_heap mp, i))).
 idtac. 
subst.
intros.
case_eq (used_raw up (Some (memory_heap mp, i))); try auto.
intro Habs.
generalize (used_raw_bool_prop gc_used_hyp0 Hi Habs Hv).
intro ; contradiction.
 intros; eapply gray_elements_not_raw0; eauto.

(* case cache not full *)
intro Hnot_full_bool.
generalize (neq_bool_neq_prop Hnot_full_bool).
intro Hnot_full_prop.
unfold marksweep_cache_full_push.
destruct (modulo_four_le_eq_or_next (a := gray_cache_offset_value p) (b := GRAY_CACHE_SIZE)).
apply mod4_sym.
eapply mod4_trans.
apply four_divides_gray_cache_size.
assumption.
assumption.
contradiction.
invall.
case_eq (store Mint32 m1 gray_cache_block (signed (gray_cache_offset_value p)) (Vptr (memory_heap mp) i)); try (intros ; discriminate).
intros m2 Hm2.
intros Hm'0.
apply mark_abstraction_intro.
simpl; rewrite (load_store_other _ _ _ _ _ _ Hm'0); auto.
rewrite (load_store_other _ _ _ _ _ _ Hm2); auto.
rewrite (load_store_other _ _ _ _ _ _ Hm1); auto.
simpl.
unfold marksweep_cache_full_push.
rewrite (load_store_same _ _ _ _ _ _ Hm'0).
reflexivity.
match goal with |- cmp Cle zero ?j = _ => change j with (add (gray_cache_offset_value p) four) end.
int_le_lt_trans_tac.
assumption.
match goal with |- cmp Cle ?j _ = _ => change j with (add (gray_cache_offset_value p) four) end.
assumption.
simpl.
eapply mod4_trans.
eassumption.
apply modulo_four_four_divides_add.
apply four_divides_four.
simpl.
intros b Hb.
unfold Mark_abstract.set_color.
destruct (eq_optptr (Some (memory_heap mp, b)) (Some (memory_heap mp, i)))
as [Heq | Hneq ] ; try (intros; discriminate).
assert (b <> i) as Hneq2.
 intro ; congruence.
intros Hcol_abs v0.
rewrite <- (mark_block_body_other_blocks_invar Hbi).
intro ; eapply col_black_a_c0 ; eassumption.
congruence.
eapply block_description_modulo_four; eassumption.
simpl; intros b Hb.
unfold Mark_abstract.set_color.
destruct (eq_optptr (Some (memory_heap mp, b)) (Some (memory_heap mp, i)))
as [ Heq | Hneq ].
injection Heq; intro; subst b.
intro v0.
rewrite (mark_block_body_header_change Hbi Hv).
rewrite Hwhite_bool; simpl.
rewrite Hnot_raw_bool; simpl.
injection 1; intro; subst v0.
rewrite (color_header_white_var Hwhite_prop).
inversion 1.
auto.
assert (b <> i) as Hneq2.
 intro ; congruence.
intros v0.
rewrite <- (mark_block_body_other_blocks_invar Hbi).
intros ; eapply col_black_c_a0 ; eassumption.
congruence.
eapply block_description_modulo_four; eassumption.
simpl;intros b Hb.
unfold Mark_abstract.set_color.
destruct (eq_optptr (Some (memory_heap mp, b)) (Some (memory_heap mp, i)))
as [Heq | Hneq ].
injection Heq.
intros ? _ ; subst b.
intros v'.
rewrite (mark_block_body_header_change Hbi Hv).
rewrite Hwhite_bool; simpl.
rewrite Hnot_raw_bool; simpl.
injection 1; intro; subst v'.
apply color_header_white_var.
assumption.
auto.
assert (b <> i) as Hneq2.
 intro ; congruence.
intros Hcol_abs v0.
rewrite <- (mark_block_body_other_blocks_invar Hbi).
intro ; eapply col_gray_a_c0 ; eassumption.
congruence.
eapply block_description_modulo_four; eassumption.
simpl;intros b Hb.
unfold Mark_abstract.set_color.
destruct (eq_optptr (Some (memory_heap mp, b)) (Some (memory_heap mp, i)))
as [ | Hneq ]; auto.
assert (b <> i) as Hneq2.
 intro ; congruence.
intros v0.
rewrite <- (mark_block_body_other_blocks_invar Hbi).
intros ; eapply col_gray_c_a0 ; eassumption.
congruence.
eapply block_description_modulo_four; eassumption.
simpl;intros b Hb.
unfold Mark_abstract.set_color.
destruct (eq_optptr (Some (memory_heap mp, b)) (Some (memory_heap mp, i)))
as [Heq | Hneq ] ; try (intros; discriminate).
assert (b <> i) as Hneq2.
 intro ; congruence.
intros Hcol_abs v0.
rewrite <- (mark_block_body_other_blocks_invar Hbi).
intro ; eapply col_white_a_c0 ; eassumption.
congruence.
eapply block_description_modulo_four; eassumption.
simpl;intros b Hb.
unfold Mark_abstract.set_color.
destruct (eq_optptr (Some (memory_heap mp, b)) (Some (memory_heap mp, i)))
as [ Heq | Hneq ].
injection Heq; intro; subst b.
intro v0.
rewrite (mark_block_body_header_change Hbi Hv).
rewrite Hwhite_bool; simpl.
rewrite Hnot_raw_bool; simpl.
injection 1; intro; subst v0.
rewrite (color_header_white_var Hwhite_prop).
inversion 1.
auto.
assert (b <> i) as Hneq2.
 intro ; congruence.
intros v0.
rewrite <- (mark_block_body_other_blocks_invar Hbi).
intros ; eapply col_white_c_a0 ; eassumption.
congruence.
eapply block_description_modulo_four; eassumption.
(* and the cache... *)
simpl.
eapply pointer_list_cont.
rewrite add_sub_id.
intro Habs.
apply (@int_lt_irrefl_1 zero).
eapply int_le_lt_trans.
eassumption.
rewrite Habs.
reflexivity.
rewrite add_sub_id.
rewrite (load_store_other _ _ _ _ _ _ Hm'0).
rewrite (load_store_same _ _ _ _ _ _ Hm2).
simpl.
reflexivity.
auto.
rewrite add_sub_id.
(* eapply pointer_list_invar. # nope. try cache_invar instead *)
eapply cache_invar.
    eassumption.
   intro.
   apply modulo_four_le_m1_left.
    assumption.
    apply lt_is_le_p.
    apply lt_is_le_neq; auto.
   apply mod4_sym; assumption.
intros; symmetry.
eapply trans_equal.
apply (load_store_other _ _ _ _ _ _ Hm'0).
auto.
eapply trans_equal.
apply (load_store_other _ _ _ _ _ _ Hm2).
right.
left.
change (size_chunk Mint32) with (signed four).
destruct (modulo_four_le_eq_or_next (a := x) (b := sub (gray_cache_offset_value p) four)).
eapply mod4_trans.
eassumption.
apply mod4_sym.
eapply mod4_trans.
apply modulo_four_four_divides_sub.
apply four_divides_four.
apply mod4_sym; auto.
assumption.
subst x.
rewrite <- plus_positive.
rewrite sub_add_id.
auto.
rewrite sub_add_id.
eapply int_le_trans.
eapply modulo_four_le_m1_right.
eassumption.
apply lt_is_le_p.
apply lt_is_le_neq.
assumption.
congruence.
apply int_le_lt_weak.
eapply lt_step_p.
apply lt_is_le_neq.
eassumption.
congruence.
reflexivity.
invall.
rewrite <- plus_positive.
apply le_is_signed_le.
int_le_lt_trans_tac.
eapply int_le_trans.
eapply modulo_four_le_m1_right.
eassumption.
apply lt_is_le_p.
apply lt_is_le_neq.
assumption.
congruence.
apply int_le_lt_weak.
eapply lt_step_p.
apply lt_is_le_neq.
eassumption.
congruence.
assumption.
reflexivity.
apply (load_store_other _ _ _ _ _ _ Hm1).
auto.
auto.

simpl.
auto.
simpl.
 inversion 1.
  auto.
 eauto.
simpl.
inversion 1.
 auto.
eauto.
simpl.
inversion 1.
subst.
eapply cache_elements_not_null0; eauto.

simpl.
inversion 1.
 subst.
 case_eq (used_raw up (Some (memory_heap mp, i))); try auto.
 intro Habs.
 generalize (used_raw_bool_prop gc_used_hyp0 Hi Habs Hv).
 intros; contradiction.
subst.
eapply cache_elements_not_raw0; eauto.

simpl.
unfold Mark_abstract.set_color.
intros bi0.
destruct (eq_optptr bi0 (Some (memory_heap mp, i))).
 intros.
 subst.
 case_eq (used_raw up (Some (memory_heap mp, i))); try auto.
 intro Habs.
 generalize (used_raw_bool_prop gc_used_hyp0 Hi Habs Hv).
 intros; contradiction.
intros; eapply gray_elements_not_raw0; eauto.

(* case not white *)
intro H_not_white.
injection 1; intro; subst m'.
case_eq (marksweep_col p (Some (memory_heap mp, i))).
auto.
auto.
intro Hwhite.
generalize (col_white_a_c0 _ Hi Hwhite _ Hv).
intro Habs.
generalize (eq_prop_eq_bool Habs).
intro  ; congruence.

(* case not valid *)
intro ; injection 1; intro ; subst.
unfold used_valid.
auto.
Qed.

End Mark_block_body.

Section Mark_block.

Variable m : mem.
Variable p : mark_abstraction_param.

Hypothesis initial_state0 : marksweep_invariants m mp up gp.
Hypothesis initial_state : mark_abstraction m mp up gp p.

Variable bi : option (block * int).

Hypothesis bi_in_heap_1 : forall b i, bi = Some (b, i) -> b = memory_heap mp.
Hypothesis bi_in_heap_2 : forall b i, bi = Some (b, i) -> member i (used_blocklist up).

Theorem mark_block_runs_well : {m' | mark_block m bi = Some m'}.
Proof.
unfold mark_block.
case_eq (alloc m 0 0).
intros m0 sp Hm0.
cut {m1 | mark_block_body m0 bi = Some m1}.
destruct 1 as [m1 Hm1].
exists (free m1 sp).
rewrite Hm1.
trivial.
eapply mark_block_body_runs_well.
  eapply alloc_marksweep_invariants.
  eassumption.
  assumption.
eapply alloc_mark_abstraction.
eassumption.
assumption.
eassumption.
assumption.
assumption.
Defined.

Variable m' : mem.
Hypothesis Hm' : Some m' = mark_block m bi.

Theorem mark_block_final_gc_state : 
marksweep_invariants m' mp up gp.
Proof. 
 generalize Hm'.
 unfold mark_block.
 case_eq (alloc m 0 0); try (intros; discriminate).
 intros m0 sp Hm0.
 case_eq (mark_block_body m0 bi); try (intros; discriminate).
 intros m1 Hm1.
 injection 1; intros; subst.
 assert (marksweep_invariants m0 mp up gp).
  eapply alloc_marksweep_invariants.
   eassumption.
  assumption.
 assert (mark_abstraction m0 mp up gp p).
  eapply alloc_mark_abstraction.
  eassumption.
  assumption.
  assumption.
 eapply free_marksweep_invariants.
  eassumption.
  assumption.
 eapply mark_block_body_final_gc_state.
 eassumption.
 eassumption.
 eassumption.
 assumption.
 assumption.
Qed.


Theorem mark_block_final_state : 
  mark_abstraction m' mp up gp (mark_block_post_param p bi).
Proof. 
 generalize Hm'.
 unfold mark_block.
 case_eq (alloc m 0 0); try (intros; discriminate).
 intros m0 sp Hm0.
 case_eq (mark_block_body m0 bi); try (intros; discriminate).
 intros m1 Hm1.
 injection 1; intros; subst.
 assert (marksweep_invariants m0 mp up gp).
  eapply alloc_marksweep_invariants.
   eassumption.
  assumption.
 assert (mark_abstraction m0 mp up gp p).
  eapply alloc_mark_abstraction.
  eassumption.
  assumption.
  assumption.
 eapply free_mark_abstraction.
  eassumption.
  assumption.
  eassumption.
 eapply mark_block_body_final_gc_state.
  eassumption.
  eassumption.
  eassumption.
  assumption.
  assumption.
 eapply mark_block_body_final_state.
 eassumption.
 eassumption.
 eassumption.
 assumption.
 assumption.
Qed.

Proposition mark_block_invariant_blocks :
forall x,
(forall m0 sp, alloc m 0 0 = (m0, sp) -> sp <> x) ->
x <> gray_cache_block ->
x <> memory_heap mp ->
x <> gray_cache_offset_block ->
x <> gray_cache_overflow_block ->
forall c i, load c m x i = load c m' x i.
Proof.
intros.
generalize Hm'.
unfold mark_block.
case_eq (alloc m 0 0); try (intros; discriminate).
intros m0 sp Hm0.
case_eq (mark_block_body m0 bi); try (intros; discriminate).
intros m1 Hm1.
injection 1; intros; subst.
eapply trans_equal.
 eapply load_alloc_other_3.
 eassumption.
 eauto.
generalize (alloc_marksweep_invariants Hm0 initial_state0).
intros Hm0gc.
generalize (alloc_mark_abstraction Hm0 initial_state0 initial_state).
intro Hm0abs.
eapply trans_equal.
 eapply mark_block_body_invariant_blocks. 
  assumption.
  eassumption.
  eassumption.
  assumption.
  eassumption.
  assumption.
  assumption.
  assumption.
  assumption.
symmetry.
eapply load_free.
intro.
subst.
destruct (H _ _ Hm0).
trivial.
Qed.

Lemma mark_block_other_blocks_invar : forall i, bi = Some (memory_heap mp, i) ->
forall i', (i = i' -> False) -> modulo_four i i' ->
load Mint32 m (memory_heap mp) (signed (sub i' four)) =
load Mint32 m' (memory_heap mp) (signed (sub i' four)).
Proof.
intros.
generalize Hm'.
unfold mark_block.
case_eq (alloc m 0 0); try (intros; discriminate).
intros m0 sp Hm0.
case_eq (mark_block_body m0 bi); try (intros; discriminate).
intros m1 Hm1.
injection 1; intros; subst.
eapply trans_equal.
 eapply load_alloc_other_3.
 eassumption.
 eapply alloc_heap_indep.
 eassumption.
 assumption.
generalize (alloc_marksweep_invariants Hm0 initial_state0).
intros Hm0gc.
generalize (alloc_mark_abstraction Hm0 initial_state0 initial_state).
intro Hm0abs.
eapply trans_equal.
 eapply mark_block_body_other_blocks_invar.
  assumption.
  eassumption.
  eassumption.
  assumption.
  eassumption.
  reflexivity.
  assumption.
  assumption.
symmetry.
generalize (mark_block_body_final_gc_state Hm0gc Hm0abs bi_in_heap_1 bi_in_heap_2 Hm1).
intro Hm1gc.
generalize (mark_block_body_final_state Hm0gc Hm0abs bi_in_heap_1 bi_in_heap_2 Hm1).
intro Hm1abs.
eapply load_free.
intro.
subst.
destruct (alloc_heap_indep Hm0 ).
assumption.
trivial.
Qed.


End Mark_block.

Definition mark_list_post_param p l := 
let (col', occ) :=
Mark_abstract.mark_list (used_valid mp up) eq_optptr marksweep_cache_is_full marksweep_cache_full_push (used_raw up) (marksweep_col p) (gray_cache_overflow_bool p) (marksweep_cache p) (gray_cache_offset_value p) l in
let (oc, cache_full') := occ in
let (overflow', cache') := oc in
  make_mark_abstraction_param
  overflow'
  cache_full'
  col'
  cache'.

Fixpoint mark_list_post_param_2 p l {struct l} :=
match l with
| nil => p
| a::q => @mark_list_post_param_2 (mark_block_post_param p a) q
end.

(*
Lemma mark_block_overflow_true_is_true : forall col overflow cache cache_full bi0 
col' overflow' cache' cache_full',
(col', ((overflow', cache'), cache_full')) = Mark_abstract.mark_block (used_valid mp up) eq_optptr marksweep_cache_is_full marksweep_cache_full_push (used_raw up) 
col overflow cache cache_full bi0 ->
overflow = true ->
overflow' = true.
intros.
subst.
generalize H.
unfold Mark_abstract.mark_block.
 destruct (used_valid mp up bi0); try congruence.
 destruct (col bi0); try congruence.
 destruct (used_raw up bi0); try congruence.
 unfold Mark_abstract.cache_push.
 destruct (marksweep_cache_is_full cache_full); try congruence.
Qed.

Corollary mark_list_overflow_true_is_true : forall l col overflow cache cache_full
col' overflow' cache' cache_full',
(col', ((overflow', cache'), cache_full')) = Mark_abstract.mark_list (used_valid mp up) eq_optptr marksweep_cache_is_full marksweep_cache_full_push (used_raw up) 
col overflow cache cache_full l ->
overflow = true ->
overflow' = true.
Proof Mark_abstract.mark_list_general (mark_block_overflow_true_is_true).

Corollary mark_block_overflow_false_was_false : forall col overflow cache cache_full bi0 
col' overflow' cache' cache_full',
(col', ((overflow', cache'), cache_full')) = Mark_abstract.mark_block (used_valid mp up) eq_optptr marksweep_cache_is_full marksweep_cache_full_push (used_raw up) 
col overflow cache cache_full bi0 ->
overflow' = false ->
overflow = false.
Proof.
intros.
destruct overflow.
 generalize (mark_block_overflow_true_is_true H (refl_equal _)).
 intros; discr.
auto.
Qed.

Corollary mark_list_overflow_false_was_false : forall l col overflow cache cache_full
col' overflow' cache' cache_full',
(col', ((overflow', cache'), cache_full')) = Mark_abstract.mark_list (used_valid mp up) eq_optptr marksweep_cache_is_full marksweep_cache_full_push (used_raw up) 
col overflow cache cache_full l ->
overflow' = false ->
overflow = false.
Proof.
intros.
destruct overflow.
 generalize (mark_list_overflow_true_is_true H (refl_equal _)).
 intros; discr.
auto.
Qed.
*)

Lemma mark_list_post_param_equiv : forall l p,
mark_list_post_param p l = mark_list_post_param_2 p l.
Proof.
induction l.
 simpl.
 intros.
 unfold mark_list_post_param.
 unfold Mark_abstract.mark_list.
 simpl.
 destruct p; auto.
simpl.
intro p.
rewrite <- IHl.
unfold mark_list_post_param.
simpl.
unfold mark_block_post_param.
destruct (Mark_abstract.mark_block (used_valid mp up) eq_optptr
              marksweep_cache_is_full marksweep_cache_full_push 
              (used_raw up) (marksweep_col p)
              (gray_cache_overflow_bool p) 
              (marksweep_cache p) (gray_cache_offset_value p) a ).
destruct p0.
destruct p0.
simpl.
trivial.
Qed.


Section Find_first_gray_block.

Section Abstract_first_gray.

Variable col : option (block * int) -> Mark_abstract.color.

Fixpoint first_gray_from_list l {struct l} : option int :=
match l with
  | a::q =>
    match col (Some (memory_heap mp, a)) with
      | Mark_abstract.Gray => Some a
      | _ => first_gray_from_list q
    end
  | _ => None
end.

Lemma first_gray_some_mem : forall l a, first_gray_from_list l = Some a -> member a l.
induction l; simpl.
 intros; discriminate.
intro a0; destruct (col (Some (memory_heap mp, a))); try (injection 1; intros; subst); auto.
Qed.

Lemma first_gray_some_col : forall l a, first_gray_from_list l = Some a -> col (Some (memory_heap mp, a)) = Mark_abstract.Gray.
Proof.
induction l; simpl.
 intros; discriminate.
intros a0.
case_eq (col (Some (memory_heap mp, a))); try (injection 2; intros; subst); auto.
Qed.

Lemma first_gray_none_no_gray : forall l, first_gray_from_list l = None -> forall a, member a l -> col (Some (memory_heap mp, a)) = Mark_abstract.Gray -> False.
Proof.
induction l; simpl.
 inversion 2.
case_eq (col (Some (memory_heap mp, a))); try (intros; discriminate);
 inversion 3 ; intros; subst; try discr; eauto.
Qed.

Definition first_gray :=
  match first_gray_from_list (used_blocklist up) with
    | Some i => Some (Some (memory_heap mp, i))
    | None => None
  end.

Theorem Hfirst_gray_some : forall a, first_gray = Some a -> used_valid mp up a = true /\ col a = Mark_abstract.Gray.

Proof.
 unfold first_gray.
 case_eq (first_gray_from_list (used_blocklist up)); try (intros; discriminate).
 intros i Hi.
 injection 1; intros; subst.
 split.
  unfold used_valid.
  destruct (Z_eq_dec (memory_heap mp) (memory_heap mp)); try congruence.
  destruct (member_dec eq_dec (used_blocklist up) i); auto.
  destruct f.
  apply first_gray_some_mem.
  assumption.
 eapply first_gray_some_col.
 eassumption.
Qed.


Theorem Hfirst_gray_none : first_gray = None -> forall a, used_valid mp up a = true -> col a = Mark_abstract.Gray -> False.

Proof.
unfold first_gray.
intro Hnone.
unfold used_valid.
destruct a; try (intros; discriminate).
destruct p.
destruct (Z_eq_dec b (memory_heap mp)); try (intros; discriminate).
destruct (member_dec eq_dec (used_blocklist up) i); try (intros; discriminate).
intros _ ?.
subst.
eapply first_gray_none_no_gray; eauto.
destruct (first_gray_from_list (used_blocklist up)); auto; discriminate.
Qed.

Corollary first_gray_no_some_none : first_gray = Some None -> False.
Proof.
intro Habs.
generalize (Hfirst_gray_some Habs).
intros [? ?]; discriminate.
Qed.

Lemma first_gray_in_heap : forall a b, first_gray = Some (Some (a, b)) -> a = memory_heap mp.
unfold first_gray.
destruct (first_gray_from_list (used_blocklist up)); congruence.
Qed.

Lemma first_gray_in_blocklist : forall a b, first_gray = Some (Some (a, b)) -> member b (used_blocklist up).
unfold first_gray.
case_eq (first_gray_from_list (used_blocklist up)); try (intros; discriminate).
injection 2; intros; subst.
eapply first_gray_some_mem; eauto.
Qed.

End Abstract_first_gray.

Variable m : mem.
Variable p : mark_abstraction_param .
Hypothesis Hgc : gc_invariants m mp up gp.
Hypothesis Habs : mark_abstraction m mp up gp  p.

Lemma find_first_gray_block_from_list_c_a_some : 
forall l hs, block_description_from_to m (memory_heap mp) hs (memory_he mp) l ->
(forall i, member i l -> member i (used_blocklist up)) ->
forall q r, Loop.loop_prop (find_first_gray_block_body m (memory_heap mp) (memory_he mp)) (Some q) (Some r) ->
find_first_gray_block_scan q = hs ->
forall b i, find_first_gray_block_result r = Vptr b i ->
first_gray_from_list (marksweep_col p) l = Some i.
Proof.
induction l.
 inversion 1.
 subst.
 simpl.
 intro Hl.
 inversion 1.
  subst.
  intros.
  generalize H1.
  unfold find_first_gray_block_body.
  rewrite (eq_prop_eq_bool H2).
  injection 1; intros; subst.
  discriminate.
 subst.
 intros.
 generalize  H1.
 unfold find_first_gray_block_body.
 rewrite (eq_prop_eq_bool H3).
 intros; discriminate.
inversion 1.  
subst.
intro Hl.
inversion 1.
 intros.
 subst.
 generalize H1.
 unfold find_first_gray_block_body.
 rewrite (neq_prop_neq_bool H2).
 rewrite <- H3.
 case_eq (eq (Color_header v) COLOR_GRAY). 
  injection 2; intros; subst.
  simpl.
  rewrite <- (add_sub_id (find_first_gray_block_scan q) four) in H3.
  rewrite (col_gray_c_a Habs (Hl _ (member_head _ _)) H3 (eq_bool_eq_prop H7)).
 simpl in H12.
 congruence.
 intros; discriminate.
intros.
subst.
simpl.
generalize H1.
unfold find_first_gray_block_body.
rewrite (neq_prop_neq_bool H2).
rewrite <- H3.
case_eq (eq (Color_header v) COLOR_GRAY); try (intros; discriminate).
injection 2; intros; subst.
case_eq (marksweep_col p (Some (memory_heap mp, add (find_first_gray_block_scan q) four))).
 intro.
 eapply IHl.
 eassumption.
 intros; eauto.
 eassumption.
 simpl.
 trivial.
 eassumption.
 intro Habsurd.
 rewrite <- (add_sub_id (find_first_gray_block_scan q) four) in H3.
 generalize (col_gray_a_c Habs (Hl _ (member_head _ _)) Habsurd H3).
 intro Habsurdos.
 generalize (eq_prop_eq_bool Habsurdos); intros; discr.
 intros; eauto. 
Qed.


Corollary first_gray_c_a_some : 
forall q r, Loop.loop_prop (find_first_gray_block_body m (memory_heap mp) (memory_he mp)) (Some q) (Some r) ->
find_first_gray_block_scan q = memory_hs mp ->
forall b i, find_first_gray_block_result r = Vptr b i ->
first_gray (marksweep_col p) = Some (Some (memory_heap mp, i)).
Proof.
intros.
cut (first_gray_from_list (marksweep_col p) (used_blocklist up) = Some i).
intro Hrew.
unfold first_gray.
rewrite Hrew.
trivial.
eapply find_first_gray_block_from_list_c_a_some.
 eapply used_heap_hyp; eauto.
 trivial.
 eassumption.
 assumption.
 eassumption.
Qed.


Lemma find_first_gray_block_from_list_a_c_none : 
forall l hs, block_description_from_to m (memory_heap mp) hs (memory_he mp) l ->
(forall i, member i l -> member i (used_blocklist up)) ->
first_gray_from_list (marksweep_col p) l = None ->
forall q r, Loop.loop_prop (find_first_gray_block_body m (memory_heap mp) (memory_he mp)) (Some q) (Some r) ->
find_first_gray_block_scan q = hs ->
find_first_gray_block_result r = Vint zero.
Proof.
induction l.
 inversion 1.
 subst.
 simpl.
 inversion 3.
  subst.
  intro.
  generalize H3.
  unfold find_first_gray_block_body.
  rewrite (eq_prop_eq_bool H4).
  injection 1 ; intros; subst; simpl; auto.
 intro.
 subst.
 generalize H3.
 unfold find_first_gray_block_body.
 rewrite (eq_prop_eq_bool H7).
 intros; discriminate.
inversion 1.  
subst.
intro Hl.
intros Hi.
inversion 1.
 intros.
 subst.
 generalize H1.
 unfold find_first_gray_block_body.
 rewrite (neq_prop_neq_bool H2).
 rewrite <- H3.
 case_eq (eq (Color_header v) COLOR_GRAY).
  intro Hgray.
  generalize Hi.
  simpl.
  rewrite <- (add_sub_id (find_first_gray_block_scan q) four) in H3.
  rewrite (col_gray_c_a Habs (Hl _ (member_head _ _)) H3 (eq_bool_eq_prop Hgray)).
  intros; discriminate.
 intros; discriminate.
intros.
subst.
generalize H1.
unfold find_first_gray_block_body.
rewrite (neq_prop_neq_bool H2).
rewrite <- H3.
case_eq (eq (Color_header v) COLOR_GRAY); try (intros; discriminate).
injection 2; intros; subst.
generalize Hi.
simpl.
case_eq (marksweep_col p (Some (memory_heap mp, add (find_first_gray_block_scan q) four))).
 intros; eauto.
 intro Habsurd.
 rewrite <- (add_sub_id (find_first_gray_block_scan q) four) in H3.
 generalize (col_gray_a_c Habs (Hl _ (member_head _ _)) Habsurd H3).
 intro Habsurdos.
 generalize (eq_prop_eq_bool Habsurdos); intros; discr.
 intros; eauto. 
Qed.

Corollary first_gray_a_c_none : 
forall q r, Loop.loop_prop (find_first_gray_block_body m (memory_heap mp) (memory_he mp)) (Some q) (Some r) ->
find_first_gray_block_scan q = memory_hs mp ->
first_gray (marksweep_col p) = None ->
find_first_gray_block_result r = Vint zero.
Proof.
intros.
cut (first_gray_from_list (marksweep_col p) (used_blocklist up) = None).
intro Hrew.
eapply find_first_gray_block_from_list_a_c_none.
 eapply used_heap_hyp; eauto.
 trivial.
 assumption.
 eassumption.
 assumption.
generalize H1.
unfold first_gray.
destruct (first_gray_from_list (marksweep_col p) (used_blocklist up)); congruence.
Qed.

Lemma find_first_gray_block_from_list_c_a_none : 
forall l hs, block_description_from_to m (memory_heap mp) hs (memory_he mp) l ->
(forall i, member i l -> member i (used_blocklist up)) ->
forall q r, Loop.loop_prop (find_first_gray_block_body m (memory_heap mp) (memory_he mp)) (Some q) (Some r) ->
find_first_gray_block_scan q = hs ->
find_first_gray_block_result r = Vint zero ->
first_gray_from_list (marksweep_col p) l = None.
Proof.
induction l.
 inversion 1.
 subst.
 simpl.
 auto.
inversion 1.  
subst.
intro Hl.
inversion 1.
 intros.
 subst.
 generalize H1.
 unfold find_first_gray_block_body.
 rewrite (neq_prop_neq_bool H2).
 rewrite <- H3.
 case_eq (eq (Color_header v) COLOR_GRAY). 
  injection 2; intros; subst; discriminate.
 intros; discriminate.
intros.
subst.
simpl.
generalize H1.
unfold find_first_gray_block_body.
rewrite (neq_prop_neq_bool H2).
rewrite <- H3.
case_eq (eq (Color_header v) COLOR_GRAY); try (intros; discriminate).
injection 2; intros; subst.
case_eq (marksweep_col p (Some (memory_heap mp, add (find_first_gray_block_scan q) four))).
 intros; eauto.
 intro Habsurd.
 rewrite <- (add_sub_id (find_first_gray_block_scan q) four) in H3.
 generalize (col_gray_a_c Habs (Hl _ (member_head _ _)) Habsurd H3).
 intro Habsurdos.
 generalize (eq_prop_eq_bool Habsurdos); intros; discr.
 intros; eauto. 
Qed.


Corollary first_gray_c_a_none : 
forall q r, Loop.loop_prop (find_first_gray_block_body m (memory_heap mp) (memory_he mp)) (Some q) (Some r) ->
find_first_gray_block_scan q = memory_hs mp ->
find_first_gray_block_result r = Vint zero ->
first_gray (marksweep_col p) = None.
Proof.
intros.
cut (first_gray_from_list (marksweep_col p) (used_blocklist up) = None).
intro Hrew.
unfold first_gray.
rewrite Hrew.
trivial.
eapply find_first_gray_block_from_list_c_a_none.
 eapply used_heap_hyp; eauto.
 trivial.
 eassumption.
 assumption.
 eassumption.
Qed.


Lemma find_first_gray_block_from_list_a_c_some : 
forall l hs, block_description_from_to m (memory_heap mp) hs (memory_he mp) l ->
(forall i, member i l -> member i (used_blocklist up)) ->
forall i, first_gray_from_list (marksweep_col p) l = Some i ->
forall q r, Loop.loop_prop (find_first_gray_block_body m (memory_heap mp) (memory_he mp)) (Some q) (Some r) ->
find_first_gray_block_scan q = hs ->
find_first_gray_block_result r = Vptr (memory_heap mp) i.
Proof.
induction l.
 inversion 1.
 subst.
 simpl.
 intros; discriminate.
inversion 1.  
subst.
intro Hl.
intros i Hi.
inversion 1.
 intros.
 subst.
 generalize H1.
 unfold find_first_gray_block_body.
 rewrite (neq_prop_neq_bool H2).
 rewrite <- H3.
 case_eq (eq (Color_header v) COLOR_GRAY). 
  injection 2; intros; subst.
  simpl.
  f_equal.
  generalize Hi.
  simpl.
  rewrite <- (add_sub_id (find_first_gray_block_scan q) four) in H3.
  rewrite (col_gray_c_a Habs (Hl _ (member_head _ _)) H3 (eq_bool_eq_prop H7)).
  congruence.
 intros; discriminate.
intros.
subst.
generalize H1.
unfold find_first_gray_block_body.
rewrite (neq_prop_neq_bool H2).
rewrite <- H3.
case_eq (eq (Color_header v) COLOR_GRAY); try (intros; discriminate).
injection 2; intros; subst.
generalize Hi.
simpl.
case_eq (marksweep_col p (Some (memory_heap mp, add (find_first_gray_block_scan q) four))).
 intros.
 eapply IHl.
 eassumption.
 intros; eauto.
 assumption.
 eassumption.
 simpl.
 trivial.
 intro Habsurd.
 rewrite <- (add_sub_id (find_first_gray_block_scan q) four) in H3.
 generalize (col_gray_a_c Habs (Hl _ (member_head _ _)) Habsurd H3).
 intro Habsurdos.
 generalize (eq_prop_eq_bool Habsurdos); intros; discr.
 intros; eauto. 
Qed.

Corollary first_gray_a_c_some : 
forall q r, Loop.loop_prop (find_first_gray_block_body m (memory_heap mp) (memory_he mp)) (Some q) (Some r) ->
find_first_gray_block_scan q = memory_hs mp ->
forall b i, first_gray (marksweep_col p) = Some (Some (b, i)) ->
find_first_gray_block_result r = Vptr (memory_heap mp) i.
Proof.
intros.
cut (first_gray_from_list (marksweep_col p) (used_blocklist up) = Some i).
intro Hrew.
eapply find_first_gray_block_from_list_a_c_some.
 eapply used_heap_hyp; eauto.
 trivial.
 assumption.
 eassumption.
 assumption.
generalize H1.
unfold first_gray.
destruct (first_gray_from_list (marksweep_col p) (used_blocklist up)); congruence.
Qed.

(* Termination *)
Lemma find_first_gray_block_from_list_term : 
forall l hs, block_description_from_to m (memory_heap mp) hs (memory_he mp) l ->
(forall i, member i l -> member i (used_blocklist up)) ->
forall q, find_first_gray_block_scan q = hs ->
Loop.loop_term (find_first_gray_block_body m (memory_heap mp) (memory_he mp)) (Some q).
Proof.
induction l.
 inversion 1.
 subst.
 simpl.
 intros.
 eapply Loop.loop_term_interrupt.
 unfold find_first_gray_block_body.
 rewrite (eq_prop_eq_bool H1).
 reflexivity.
inversion 1.  
subst.
intro Hl.
intros q Hq.
subst.
case_eq (eq (Color_header v) COLOR_GRAY).
 intro Hgray.
 eapply Loop.loop_term_interrupt.
 unfold find_first_gray_block_body.
 rewrite (neq_prop_neq_bool H2).
 rewrite <- H3.
 rewrite Hgray.
 reflexivity.
intro Hnogray.
eapply Loop.loop_term_continue.
 unfold find_first_gray_block_body.
 rewrite (neq_prop_neq_bool H2).
 rewrite <- H3.
 rewrite Hnogray.
 reflexivity.
eauto.
Qed.

Corollary first_gray_term : 
forall q, 
find_first_gray_block_scan q = memory_hs mp ->
Loop.loop_term (find_first_gray_block_body m (memory_heap mp) (memory_he mp)) (Some q).
Proof.
intros.
eapply find_first_gray_block_from_list_term.
 eapply used_heap_hyp; eauto.
 trivial.
 assumption.
Qed.

End Find_first_gray_block.

Section Cache_pop.

Variable m : mem.
Variable p : mark_abstraction_param .
Hypothesis Hgc : marksweep_invariants m mp up gp.
Hypothesis Habs : mark_abstraction m mp up gp  p.

Theorem cache_pop_exists : exists r, exists m',
  cache_pop (memory_heap mp) (memory_hs mp) (memory_he mp) m r m'.
Proof.
unfold cache_pop.
inversion Hgc.
inversion marksweep_gc_inv0.
inversion gc_used_hyp0.
inversion Habs.
inversion cache_abstraction0.
 subst.
 repeat rewrite sub_add_opp in H1.
 rewrite <- gray_cache_offset_defined0.
 rewrite (eq_prop_eq_bool (add_reg_r H1)).
 rewrite <- gray_cache_overflow_defined0.
 destruct (gray_cache_overflow_bool p).
  simpl.
  destruct (Loop.loop (first_gray_term marksweep_gc_inv0 (q := make_find_first_gray_block_param (memory_hs mp) Vundef) (refl_equal _))).
  destruct x.
   destruct f.
   case_eq (first_gray (marksweep_col p)).
    destruct o.
     destruct p0.
     intros Hfirst.
     generalize (first_gray_a_c_some marksweep_gc_inv0 Habs l (refl_equal _) Hfirst).
     simpl.
     intro Hres.
     subst.
     exists (Some (Vptr (memory_heap mp) i)).
     exists m.
     split ; auto.
     exists Vundef.
     exists find_first_gray_block_scan0.
     exists (Vptr (memory_heap mp) i).
     auto.
    intro Habsurd.
    destruct (first_gray_no_some_none Habsurd).
   intros Hfirst.
   generalize (first_gray_a_c_none marksweep_gc_inv0 Habs l (refl_equal _) Hfirst).
   simpl.
   intro; subst.
   exists (@None val).
   exists m.
   split; auto.
   exists Vundef.
   exists find_first_gray_block_scan0.
   exists (Vint zero).
   simpl; auto.
  destruct (find_first_gray_block_loop_res_some l); auto.
 simpl.
 repeat esplit; eauto.
subst. 
rewrite <- gray_cache_offset_defined0.
case_eq (eq (gray_cache_offset_value p) zero).
 intro Heq.
 generalize (eq_bool_eq_prop Heq).
 intros; congruence.
 intros _.
 rewrite <- H1.
 destruct (
   valid_access_store m Mint32 gray_cache_offset_block 0 (Vint (sub (gray_cache_offset_value p) four))
   (load_valid_access _ _ _ _ _ (sym_equal gray_cache_offset_defined0))
 ) as [m' Hm'].
 rewrite Hm'.
 repeat esplit; eauto.
Qed.

Variable m' : mem.
Variable r : option val.
Hypothesis Hm' : cache_pop (memory_heap mp) (memory_hs mp) (memory_he mp) m r m'.

Theorem cache_pop_final_gc_state : marksweep_invariants m' mp up gp.
Proof.
inversion Hgc.
inversion marksweep_gc_inv0.
inversion gc_used_hyp0.
inversion Habs.

generalize Hm'.
unfold cache_pop.
rewrite <- gray_cache_offset_defined0.
case_eq (eq (gray_cache_offset_value p) zero).
 intro Hzero.
 inversion 1.
 subst.
 assumption.
intro Hnz.
inversion cache_abstraction0.
 subst.
 repeat rewrite sub_add_opp in H1.
 generalize (eq_prop_eq_bool (add_reg_r H1)); intro; discr.
subst.
rewrite <- H1.
case_eq (store Mint32 m gray_cache_offset_block 0 (Vint (sub (gray_cache_offset_value p) four))); try (intros; contradiction).
intros m1 Hm1.
intros [? ?]; subst.
apply marksweep_invariants_intro; try (
  try rewrite (load_store_other _ _ _ _ _ _ Hm1); auto
).
 apply gc_invariants_intro; try (
   try rewrite (load_store_other _ _ _ _ _ _ Hm1); auto
   ).
 apply used_abstraction_intro;
  try rewrite (load_store_other _ _ _ _ _ _ Hm1); try assumption.

(* block description *)
eapply block_description_invar_outside.
2 : eauto.
auto.
auto.

(* sizes *)
 intros i Hi v0.
 rewrite (load_store_other _ _ _ _ _ _ Hm1);  [|auto];
 intros; eapply used_sizes_hyp; eauto.

(* kinds *)
 intros i Hi v0.
 rewrite (load_store_other _ _ _ _ _ _ Hm1);  [|auto];
 intros; eapply used_kinds_hyp; eauto.

(* extra zero : don't care *)
rewrite up_extra_zero_false.
discriminate 1.

(* raw data *)
intros.
rewrite (load_store_other _ _ _ _ _ _ Hm1);  [|auto];
intros; eapply used_rawdata_hyp; eauto.

(* pointer list block *)
intros.
eapply pointer_list_block_invar.
 eassumption.
 intros.
  destruct (block_header used_heap_hyp H5).
  rewrite (load_store_other _ _ _ _ _ _ Hm1).
  esplit; eauto.
 auto.
  intros until 2; intro; rewrite (load_store_other _ _ _ _ _ _ Hm1).
   congruence.
  auto.
  intros until 2; intro; rewrite (load_store_other _ _ _ _ _ _ Hm1).
   congruence.
  auto.
  intros until 6; rewrite (load_store_other _ _ _ _ _ _ Hm1); auto.
  assumption.
 eauto.

(* root positions *)
 eapply root_position_list_invar.
  eassumption.
  intros; symmetry; eapply load_store_other; eauto.

(* all roots *)
 eapply all_roots_invar.
  eassumption.
  eassumption.
 intros; rewrite (load_store_other _ _ _ _ _ _ Hm1); auto.
 left; eauto.

(* valid heap *)
  eapply store_valid_block_1;  eassumption.

(* valid gray cache *)
  eapply store_valid_block_1;  eassumption.

(* gray cache low bound *)
 rewrite (low_bound_store _ _ _ _ _ _ Hm1); eassumption.

(* gray cache high bound *)
 rewrite (high_bound_store _ _ _ _ _ _ Hm1); eassumption.
Qed. 

Definition cache_pop_post_param :=
  let (k, cache_full') :=
    Mark_abstract.cache_pop (first_gray) marksweep_cache_full_pop (marksweep_col p) (gray_cache_overflow_bool p) (marksweep_cache p) (gray_cache_offset_value p) in
let (_, cache') := k in
    make_mark_abstraction_param
    (gray_cache_overflow_bool p)
    cache_full'
    (marksweep_col p)
    cache'
.

Theorem cache_pop_final_state : mark_abstraction m' mp up gp cache_pop_post_param.
Proof.
inversion Hgc.
inversion marksweep_gc_inv0.
inversion gc_used_hyp0.
inversion Habs.

generalize Hm'.
unfold cache_pop.
unfold cache_pop_post_param.
unfold Mark_abstract.cache_pop.
rewrite <- gray_cache_offset_defined0.
inversion cache_abstraction0.
 subst.
 repeat rewrite sub_add_opp in H1.
 generalize (add_reg_r H1).
 intro Hzero.
 rewrite (eq_prop_eq_bool Hzero).
 intros [? _].
 subst.
 case_eq (gray_cache_overflow_bool p).
  intro Hoverflow.
  destruct (first_gray (marksweep_col p)).
   rewrite H; rewrite <- Hoverflow.
   destruct p; assumption.
  rewrite H; rewrite <- Hoverflow.
  destruct p; assumption.
 intro Hfalse.
 rewrite <- Hfalse; rewrite H.
 destruct p; assumption.
simpl.
replace (eq (gray_cache_offset_value p) zero) with false.
subst.
rewrite <- H1.
case_eq (  store Mint32 m gray_cache_offset_block 0
       (Vint (sub (gray_cache_offset_value p) four))
);
try (intros; contradiction).
intros m1 Hm1.
intros [_ ?]; subst.
unfold marksweep_cache_full_pop.
assert (cmp Cle zero( sub (gray_cache_offset_value p) four) = true).
 eapply modulo_four_le_m1_left.
 auto.
 apply lt_is_le_p.
 apply lt_is_le_neq.
 assumption.
 congruence.
Opaque cmp.
apply mark_abstraction_intro; simpl;
  try assumption; try
  (rewrite (load_store_other _ _ _ _ _ _ Hm1); [|auto]; assumption).
rewrite (load_store_same _ _ _ _ _ _ Hm1);simpl;trivial.
eapply int_le_trans.
eapply modulo_four_le_m1_right.
eassumption.
apply lt_is_le_p.
apply lt_is_le_neq.
assumption.
congruence.
eapply int_le_trans.
eapply int_le_lt_weak.
eapply lt_step_p.
eapply lt_is_le_neq.
eassumption.
congruence.
assumption.
apply mod4_sym.
apply four_divides_sub_four.
unfold four_divides.
apply mod4_sym.
auto.

intros until 2; intro; rewrite (load_store_other _ _ _ _ _ _ Hm1); [|auto];
simpl; intros; eapply col_black_a_c0; eassumption.

intros until 1; intro; rewrite (load_store_other _ _ _ _ _ _ Hm1); [|auto].
simpl;intros; eapply col_black_c_a0; eassumption.


intros until 2; intro; rewrite (load_store_other _ _ _ _ _ _ Hm1); [|auto].
simpl; intros; eapply col_gray_a_c0; eassumption.

intros until 1; intro; rewrite (load_store_other _ _ _ _ _ _ Hm1); [|auto].
simpl;intros; eapply col_gray_c_a0; eassumption.


intros until 2; intro; rewrite (load_store_other _ _ _ _ _ _ Hm1); [|auto].
simpl; intros; eapply col_white_a_c0; eassumption.

intros until 1; intro; rewrite (load_store_other _ _ _ _ _ _ Hm1); [|auto].
simpl;intros; eapply col_white_c_a0; eassumption.

simpl.
eapply cache_invar.
 eassumption.
 intro Hnz2.
 eapply modulo_four_le_m1_left.
  apply mod4_sym.
  apply four_divides_sub_four.
  unfold four_divides.  
  apply mod4_sym.
 auto.
 apply lt_is_le_p.
 apply lt_is_le_neq.
 assumption.
 congruence.
  apply four_divides_sub_four.
  unfold four_divides.  
  apply mod4_sym.
 auto.

intros; symmetry; eapply load_store_other; eauto.
simpl.
intros; eapply cache_elements_in_heap0.
rewrite <- H; eauto.
intros; eapply cache_elements_in_blocklist0.
rewrite <- H; eauto.
simpl.
intros; eapply cache_elements_not_null0.
rewrite <- H; eauto.

simpl.
intros; eapply cache_elements_not_raw0.
rewrite <- H; eauto.


symmetry.
apply neq_prop_neq_bool.
congruence.
Qed.



Theorem cache_pop_value_none : r = None -> (* exists k1, exists k2,  *)
  Mark_abstract.cache_pop (first_gray) marksweep_cache_full_pop (marksweep_col p) (gray_cache_overflow_bool p) (marksweep_cache p) (gray_cache_offset_value p) = 
   (None, marksweep_cache p, gray_cache_offset_value p).
Proof.

inversion Hgc.
inversion marksweep_gc_inv0.
inversion gc_used_hyp0.
inversion Habs.

intro.
subst.

generalize Hm'.
unfold cache_pop.
unfold Mark_abstract.cache_pop.
rewrite <- gray_cache_offset_defined0.
inversion cache_abstraction0.
 subst.
 repeat rewrite sub_add_opp in H1.
 generalize (add_reg_r H1).
 intro Hzero.
 rewrite (eq_prop_eq_bool Hzero).
 intros [_ Hres].
 genclear Hres.
 rewrite <- gray_cache_overflow_defined0.
 case_eq (gray_cache_overflow_bool p).
  simpl.
  intros.
  invall.
  destruct x1; try (intros; discriminate).
  genclear H4.
  case_eq (eq i zero); try (intros; discriminate).
  intros Hz _.
  rewrite (eq_bool_eq_prop Hz) in H3.
  rewrite (first_gray_c_a_none marksweep_gc_inv0 Habs H3).
  reflexivity.
  trivial.
  trivial.
 intros;  reflexivity.
subst.
case_eq (eq (gray_cache_offset_value p) zero).
 intro Hz.
 generalize (eq_bool_eq_prop Hz).
 intros; congruence.
intro.
rewrite <- H1.
destruct (store Mint32 m gray_cache_offset_block 0 (Vint (sub (gray_cache_offset_value p) four)));
intros; invall; (discriminate || contradiction).
Qed.

Opaque used_raw.

Theorem cache_pop_value_some : forall v, r = Some v -> exists o, exists k1, exists k2, 
    Mark_abstract.cache_pop (first_gray) marksweep_cache_full_pop (marksweep_col p) (gray_cache_overflow_bool p) (marksweep_cache p) (gray_cache_offset_value p) = (Some (Some (memory_heap mp, o)), k1, k2) /\
    v = Vptr (memory_heap mp) o /\
    member o (used_blocklist up) /\
    used_raw up (Some (memory_heap mp, o)) = false.
Proof.

inversion Hgc.
inversion marksweep_gc_inv0.
inversion gc_used_hyp0.
inversion Habs.

intros ? ?; subst.

generalize Hm'.
unfold cache_pop.
unfold Mark_abstract.cache_pop.
rewrite <- gray_cache_offset_defined0.
inversion cache_abstraction0.
 subst.
 repeat rewrite sub_add_opp in H1.
 generalize (add_reg_r H1).
 intro Hzero.
 rewrite (eq_prop_eq_bool Hzero).
 intros [_ Hres].
 genclear Hres.
 rewrite <- gray_cache_overflow_defined0.
 case_eq (gray_cache_overflow_bool p).
  simpl.
  intros.
  invall.
  case_eq (first_gray (marksweep_col p)).
   intros o Ho.
   destruct o.
   destruct p0.
    generalize (first_gray_a_c_some marksweep_gc_inv0 Habs H3 (refl_equal _) Ho).
    simpl.
    generalize (first_gray_in_heap Ho).
    intros; subst.
    injection H4; intros; subst.
    repeat eapply ex_intro.
    split.
    reflexivity.
    split.
     auto.
    split.
     eapply first_gray_in_blocklist.
     eassumption.
    eapply gray_elements_not_raw0.
    destruct (Hfirst_gray_some Ho);assumption.
   destruct (first_gray_no_some_none Ho).
  intro Hnone.
  generalize (first_gray_a_c_none marksweep_gc_inv0 Habs H3 (refl_equal _) Hnone).
  simpl.
  intros; subst.
  discriminate.
 simpl.
 intros; discriminate.
subst.
case_eq (eq (gray_cache_offset_value p) zero).
 intro Hz.
 generalize (eq_bool_eq_prop Hz).
 intros; congruence.
intro.
rewrite <- H1.
destruct (store Mint32 m gray_cache_offset_block 0 (Vint (sub (gray_cache_offset_value p) four)));
try (intros; contradiction).
intros [Hinj ?]; subst.
injection Hinj; intros; subst.
destruct p0.
 destruct p0.
 rewrite <- H in cache_elements_in_heap0.
 generalize (cache_elements_in_heap0 b i (member_head _ _)).
 intros; subst.
 repeat esplit.
 inversion H4.
 trivial.
 eapply cache_elements_in_blocklist0.
 rewrite <- H.
 eapply member_head; eauto.
eapply cache_elements_not_raw0.
rewrite <- H.
auto.

destruct cache_elements_not_null0.
rewrite <- H; auto.

Qed.

End Cache_pop.

Section Set_black.

Variable m : mem.
Variable p : mark_abstraction_param .
Hypothesis Hgc : marksweep_invariants m mp up gp.
Hypothesis Habs : mark_abstraction m mp up gp  p.

Variable i : int.
Hypothesis Hi : member i (used_blocklist up).

Variable v : int.
Hypothesis Hv : Some (Vint v) = load Mint32 m (memory_heap mp) (signed (sub i four)).

Lemma set_black_exists : exists m',
  store Mint32 m (memory_heap mp) (signed (sub i four)) (Vint (or v COLOR_BLACK)) = Some m'.
Proof.
  destruct (block_header (used_heap_hyp (gc_used_hyp (marksweep_gc_inv Hgc))) Hi).
  eapply valid_access_store.
  eapply load_valid_access.
  eauto.
Qed.

Variable m' : mem.
Hypothesis Hm' : store Mint32 m (memory_heap mp) (signed (sub i four)) (Vint (or v COLOR_BLACK)) = Some m'.

Theorem set_black_final_gc_state : marksweep_invariants m' mp up gp.
inversion Hgc.
inversion marksweep_gc_inv0.
inversion gc_used_hyp0.
inversion Habs.

apply marksweep_invariants_intro; try (
  try rewrite (load_store_other _ _ _ _ _ _ Hm'); auto
).
 apply gc_invariants_intro; try (
   try rewrite (load_store_other _ _ _ _ _ _ Hm'); auto
   ).
 apply used_abstraction_intro; try assumption;
  try (rewrite (load_store_other _ _ _ _ _ _ Hm'); [|auto]; assumption).

(* block description *)
eapply block_description_change_color_inv.
4 : eassumption.
4 : symmetry; eassumption.
auto.
assumption.
assumption.

(* sizes *)
intros b Hb v0.
destruct (eq_dec b i).
 subst.
 rewrite (load_store_same _ _ _ _ _ _ Hm').
 simpl.
 injection 1; intro; subst.
 rewrite size_header_color_inv.
 eapply used_sizes_hyp; eauto.
 auto.
 rewrite <- (get_set_int32_indep (sym_equal Hm')).
 intros; eapply used_sizes_hyp; eauto.
 repeat rewrite sub_add_opp.
 intro Habsurd. 
 generalize (add_reg_r Habsurd); congruence.
 apply mod4_sub.
 eapply block_description_modulo_four; eassumption.
 auto.

(* kinds *)
intros b Hb v0.
destruct (eq_dec b i).
 subst.
 rewrite (load_store_same _ _ _ _ _ _ Hm').
 simpl.
 injection 1; intro; subst.
 rewrite kind_header_color_inv.
 eapply used_kinds_hyp; eauto.
 auto.
 rewrite <- (get_set_int32_indep (sym_equal Hm')).
 intros; eapply used_kinds_hyp; eauto.
 repeat rewrite sub_add_opp.
 intro Habsurd. 
 generalize (add_reg_r Habsurd); congruence.
 apply mod4_sub.
 eapply block_description_modulo_four; eassumption.
 auto.

(* extra zero : don't care *)
rewrite up_extra_zero_false.
discriminate 1.

(* raw data *)
  intros.
  rewrite <- (used_rawdata_hyp _ H H0 H1 _ H2 H3 H4).
  symmetry.
  eapply get_set_int32_indep.
  eauto.
  intro Habsurd.
  subst.
  destruct (eq_dec i0 i).
  subst.
  eapply four_not_zero.
  rewrite <- (neg_neg four).
  change zero with (neg zero).
  f_equal.
  apply add_zero_recip_l with i.
  rewrite <- sub_add_opp.
  eapply int_le_antisym.
  eapply int_le_trans.
   eapply block_header_end_after_block_start.
   eassumption.
   assumption.
  eapply nonempty_block_left.
   eassumption.
   assumption.
   eassumption.
   idtac.
   rewrite (used_sizes_hyp _ Hi _ Hv).
   assumption.
  assumption.
  destruct (block_header used_heap_hyp H) as [v0 Hv0].
  rewrite <- (used_sizes_hyp _ H _ Hv0) in *.
  generalize (block_description_disjoint  H Hi n used_heap_hyp Hv0 Hv).
  intros [Hdisj].
  apply Hdisj with (sub i four); try assumption.
  eapply int_le_trans.
  eapply block_header_end_after_block_start; eassumption.
  eapply int_le_trans.
  eapply nonempty_block_left;  eassumption.
  assumption.
  eapply int_le_trans.
  eassumption.
  eapply modulo_four_le_m1_right.
  eapply modulo_four_four_divides_add.
  apply four_divides_size_header.
  eapply nonempty_block_right; eassumption.
  auto.
  eapply int_le_trans.
  eapply block_header_end_after_block_start; eassumption.
  eapply block_header_end_before_block_end; eassumption.
  eapply mod4_trans.
  eapply modulo_four_four_divides_sub.
  apply four_divides_four.
  eapply mod4_trans.
  eapply block_description_modulo_four; eassumption.
  apply mod4_sym; assumption.

(* pointer list block *)
intros.
eapply pointer_list_block_invar.
 eassumption.
 intros.
  destruct (eq_dec b0 i).
  subst.
  esplit.
  rewrite (load_store_same _ _ _ _ _ _ Hm').
  simpl.
  reflexivity.
  destruct (block_header used_heap_hyp H0).
  rewrite <- (get_set_int32_indep (sym_equal Hm')).
  esplit; eauto.
  repeat rewrite sub_add_opp.
  intro Habsurd.
  generalize (add_reg_r Habsurd).
  congruence.
  apply mod4_sub.
  eapply block_description_modulo_four; eauto.
  auto.
  intros until 2; intro.
  destruct (eq_dec b0 i).
   subst; intros.
   replace v0 with v.
   replace v' with (or v COLOR_BLACK).
   symmetry.
   apply kind_header_color_inv.
   auto.
   rewrite (load_store_same _ _ _ _ _ _ Hm') in H2.
   simpl in H2. congruence.
   congruence.
  rewrite <- (get_set_int32_indep (sym_equal Hm')).   
  intros; congruence.
  repeat rewrite sub_add_opp.
  intro Habsurd.
  generalize (add_reg_r Habsurd).
  congruence.
  apply mod4_sub.
  eapply block_description_modulo_four; eauto.
  auto.
  intros until 2; intro.
  destruct (eq_dec b0 i).
   subst; intros.
   replace v0 with v.
   replace v' with (or v COLOR_BLACK).
   symmetry.
   apply size_header_color_inv.
   auto.
   rewrite (load_store_same _ _ _ _ _ _ Hm') in H2.
   simpl in H2. congruence.
   congruence.
  rewrite <- (get_set_int32_indep (sym_equal Hm')).   
  intros; congruence.
  repeat rewrite sub_add_opp.
  intro Habsurd.
  generalize (add_reg_r Habsurd).
  congruence.
  apply mod4_sub.
  eapply block_description_modulo_four; eauto.
  auto.

  intros.
  eapply get_set_int32_indep.
  eauto.
  intro Habsurd.
  subst.
  destruct (eq_dec b0 i).
  subst.
  eapply four_not_zero.
  rewrite <- (neg_neg four).
  change zero with (neg zero).
  f_equal.
  apply add_zero_recip_l with i.
  rewrite <- sub_add_opp.
  eapply int_le_antisym.
  eapply int_le_trans.
   eapply block_header_end_after_block_start.
   eassumption.
   assumption.
  eapply nonempty_block_left.
   eassumption.
   assumption.
   eassumption.
   assumption.
  assumption.
  generalize (block_description_disjoint  H0 Hi n used_heap_hyp H1 Hv).
  intros [Hdisj].
  apply Hdisj with (sub i four); try assumption.
  eapply int_le_trans.
  eapply block_header_end_after_block_start; eassumption.
  eapply int_le_trans.
  eapply nonempty_block_left; eassumption.
  assumption.
  eapply int_le_trans.
  eassumption.
  eapply modulo_four_le_m1_right.
  eapply modulo_four_four_divides_add.
  apply four_divides_size_header.
  eapply nonempty_block_right; eassumption.
  auto.
  eapply int_le_trans.
  eapply block_header_end_after_block_start; eassumption.
  eapply block_header_end_before_block_end; eassumption.
  eapply mod4_trans.
  eapply modulo_four_four_divides_sub.
  apply four_divides_four.
  eapply mod4_trans.
  eapply block_description_modulo_four; eassumption.
  assumption.

 assumption.
 eauto.

(* root positions *)
 eapply root_position_list_invar.
  eassumption.
  intros; symmetry; eapply load_store_other; eauto.

(* all roots *)
 eapply all_roots_invar.
  eassumption.
  eassumption.
 intros; rewrite (load_store_other _ _ _ _ _ _ Hm'); auto.
 left; eauto.

(* valid heap *)
 eapply store_valid_block_1; eassumption.

(* valid cache *)
  eapply store_valid_block_1;  eassumption.

(* cache low bound *)
 rewrite (low_bound_store _ _ _ _ _ _ Hm'); eassumption.

(* cache high bound *)
 rewrite (high_bound_store _ _ _ _ _ _ Hm'); eassumption.

Qed.

Definition set_black_post_param := make_mark_abstraction_param
 (gray_cache_overflow_bool p)
 (gray_cache_offset_value p)
 (Mark_abstract.set_color eq_optptr (Some (memory_heap mp, i)) Mark_abstract.Black (marksweep_col p))
 (marksweep_cache p).

Opaque cmp used_raw.
Theorem set_black_final_state : mark_abstraction m' mp up gp set_black_post_param.
inversion Hgc.
inversion marksweep_gc_inv0.
inversion gc_used_hyp0.
inversion Habs.

unfold set_black_post_param.

Opaque cmp.
apply mark_abstraction_intro; simpl; try assumption;
  try (rewrite (load_store_other _ _ _ _ _ _ Hm'); [|auto]; assumption).

unfold Mark_abstract.set_color.
intros b Hb col v0.
destruct (eq_optptr (Some (memory_heap mp, b)) (Some (memory_heap mp, i))).
 injection e; intro; subst.
 rewrite (load_store_same _ _ _ _ _ _ Hm');simpl;trivial.
 injection 1; intros; subst.
 apply color_header_set_black.
 rewrite <- (get_set_int32_indep (sym_equal Hm') (i' := sub b four)).
 intros; eapply col_black_a_c0; eassumption.
 repeat rewrite sub_add_opp.
 intro Habsurd.
 generalize (add_reg_r Habsurd).
 congruence.
 apply mod4_sub.
 eapply block_description_modulo_four; eassumption.
 auto.

unfold Mark_abstract.set_color.
intros b Hb v0.
destruct (eq_optptr (Some (memory_heap mp, b)) (Some (memory_heap mp, i))); auto.
 rewrite <- (get_set_int32_indep (sym_equal Hm') (i' := sub b four)).
 intros; eapply col_black_c_a0; eassumption.
 repeat rewrite sub_add_opp.
 intro Habsurd.
 generalize (add_reg_r Habsurd).
 congruence.
 apply mod4_sub.
 eapply block_description_modulo_four; eassumption.
 auto.

unfold Mark_abstract.set_color.
intros b Hb col v0.
destruct (eq_optptr (Some (memory_heap mp, b)) (Some (memory_heap mp, i))); try discriminate.
 rewrite <- (get_set_int32_indep (sym_equal Hm') (i' := sub b four)).
 intros; eapply col_gray_a_c0; eassumption.
 repeat rewrite sub_add_opp.
 intro Habsurd.
 generalize (add_reg_r Habsurd).
 congruence.
 apply mod4_sub.
 eapply block_description_modulo_four; eassumption.
 auto.

unfold Mark_abstract.set_color.
intros b Hb v0.
destruct (eq_optptr (Some (memory_heap mp, b)) (Some (memory_heap mp, i))).
 injection e; intro; subst.
 rewrite (load_store_same _ _ _ _ _ _ Hm');simpl;trivial.
 injection 1; intro; subst.
 rewrite color_header_set_black.
 inversion 1.
 rewrite <- (get_set_int32_indep (sym_equal Hm') (i' := sub b four)).
 intros; eapply col_gray_c_a0; eassumption.
 repeat rewrite sub_add_opp.
 intro Habsurd.
 generalize (add_reg_r Habsurd).
 congruence.
 apply mod4_sub.
 eapply block_description_modulo_four; eassumption.
 auto.

unfold Mark_abstract.set_color.
intros b Hb col v0.
destruct (eq_optptr (Some (memory_heap mp, b)) (Some (memory_heap mp, i))); try discriminate.
 rewrite <- (get_set_int32_indep (sym_equal Hm') (i' := sub b four)).
 intros; eapply col_white_a_c0; eassumption.
 repeat rewrite sub_add_opp.
 intro Habsurd.
 generalize (add_reg_r Habsurd).
 congruence.
 apply mod4_sub.
 eapply block_description_modulo_four; eassumption.
 auto.

unfold Mark_abstract.set_color.
intros b Hb v0.
destruct (eq_optptr (Some (memory_heap mp, b)) (Some (memory_heap mp, i))).
 injection e; intro; subst.
 rewrite (load_store_same _ _ _ _ _ _ Hm');simpl;trivial.
 injection 1; intro; subst.
 rewrite color_header_set_black.
 inversion 1.
 rewrite <- (get_set_int32_indep (sym_equal Hm') (i' := sub b four)).
 intros; eapply col_white_c_a0; eassumption.
 repeat rewrite sub_add_opp.
 intro Habsurd.
 generalize (add_reg_r Habsurd).
 congruence.
 apply mod4_sub.
 eapply block_description_modulo_four; eassumption.
 auto.

eapply cache_invar.
eassumption.
intro Hnz.
eapply modulo_four_le_m1_left.
assumption.
eapply lt_is_le_p.
eapply lt_is_le_neq.
assumption.
congruence.
apply mod4_sym; auto.

intros.
symmetry.
apply (load_store_other _ _ _ _ _ _ Hm').
auto.

intros bi.
unfold Mark_abstract.set_color.
destruct (eq_optptr bi (Some (memory_heap mp, i))).
 discriminate 1.
intros; eapply gray_elements_not_raw; eauto.
Qed.

End Set_black.

Section Mark_children.

Variable i : int.
Hypothesis Hi : member i (used_blocklist up).
Hypothesis Hnot_raw : used_raw up (Some (memory_heap mp, i)) = false.

Let firstfield := if (eq (used_kinds up i) KIND_CLOSURE) then four else zero.

Lemma mark_children_exists_partial : 
forall l, is_suffix_of l (used_children up (Some (memory_heap mp, i))) ->
forall m j ap, pointer_list m (memory_heap mp) (add (sub i four) firstfield) j l ->
marksweep_invariants m mp up gp ->
mark_abstraction m mp up gp ap ->
exists p', Loop.loop_prop (mark_children_body (memory_heap mp) i firstfield) 
  (Some (make_mark_children_body_param m (add (sub j i) four))) (Some p') /\
  let m' := mark_children_body_mem p' in
    marksweep_invariants m' mp up gp /\
    mark_abstraction m' mp up gp (mark_list_post_param ap l)
  .

Proof.
induction l.
 inversion 2.
 subst.
 intros.
 eapply ex_intro.
 split.
  eapply Loop.loop_prop_interrupt.
  unfold mark_children_body.
  Opaque eq load store. simpl.
  rewrite <- sub_add_l.
  rewrite <- sub_add_l.
  rewrite <- sub_add_l.
  rewrite (add_commut i).
  rewrite add_sub_id.
  rewrite add_sub_id.
  case_eq (eq firstfield firstfield).
   intros; reflexivity.
  intro Habsurd.
  destruct (neq_bool_neq_prop Habsurd).
  trivial.
 unfold mark_list_post_param.
 unfold Mark_abstract.mark_list.
 simpl.
 split; destruct ap; auto.
inversion 2.
subst.
(* some intermediate lemmata *)
inversion 1.
inversion 1.
inversion marksweep_gc_inv0.
inversion gc_used_hyp0.
assert (member a (used_children up (Some (memory_heap mp, i)))).
 eapply suffix_member.
  eassumption.
 auto.
assert (
 bi_in_heap_1 : forall b i0, a = Some (b, i0) -> b = memory_heap mp
).
 intros; subst.
 inversion H7; subst. (* val_is_pointer_or_dumb *)
 generalize (used_children_are_blocks _ Hi _ _ H5).
 inversion 1; auto.
assert (
  bi_in_heap_2 : forall b i0, a = Some (b, i0) -> member i0 (used_blocklist up) 
).
 intros; subst.
 inversion H7; subst. (* val_is_pointer_or_dumb *)
 generalize (used_children_are_blocks _ Hi _ _ H5).
 inversion 1; auto.
case_eq (mark_children_body (memory_heap mp) i firstfield (Some (make_mark_children_body_param m (add (sub j i) four)))).
intros bo op Hbop.
generalize Hbop.
unfold mark_children_body at 1.
simpl.
case_eq (eq (add (sub j i) four) firstfield).
 intro Habsurd.
 generalize (eq_bool_eq_prop Habsurd).
 clear Habsurd.
 intro Habsurd.
 rewrite <- Habsurd in *.
 destruct H3.
 rewrite <- sub_add_l.
 rewrite <- add_assoc.
 rewrite add_sub_id.
 rewrite add_commut.
 rewrite sub_add_id.
 trivial.
intros _.
rewrite add_sub_id.
rewrite add_commut.
rewrite sub_add_id.
rewrite <- H4.
generalize (mark_block_runs_well H1 H2 bi_in_heap_1 bi_in_heap_2).
intros [m' Hm'].
replace (
  match v with
     | Vundef => None (A:=mem)
     | Vint _ => mark_block m None
     | Vfloat _ => None (A:=mem)
     | Vptr bl of => mark_block m (Some (bl, of))
     end
) with (Some m').
 injection 1; intros; subst.
 symmetry in Hm'.
 generalize (mark_block_final_gc_state H1 H2 bi_in_heap_1 bi_in_heap_2 Hm').
 intro Hm'gc.
 generalize (mark_block_final_state H1 H2 bi_in_heap_1 bi_in_heap_2 Hm').
 intro Hm'u.
 inversion Hm'gc.
 inversion marksweep_gc_inv1.
 inversion gc_used_hyp1.
 inversion Hm'u.
 destruct (IHl (suffix_cons H) m' (sub j four)(mark_block_post_param ap a) ) as [p' [Hp' [Hp'1 Hp'2]]];
  try assumption.
  generalize (used_children_hyp _ Hi).
  inversion 1; subst.
   generalize (used_raw_prop_bool gc_used_hyp0 Hi H10 H11).
   intros; discr.
   generalize H6.
   unfold firstfield.
   rewrite <- (used_kinds_hyp _ Hi _ H9).
   rewrite H10.
   simpl.
   rewrite add_zero.
   apply (pointer_list_invar_by_suffix (suffix_cons H) H11 (m' := m')).
   generalize (used_children_hyp0 _ Hi).
   inversion 1; subst.
    generalize (used_raw_prop_bool gc_used_hyp1 Hi H14 H15).
    intros; discr.
    generalize H15.
    rewrite (used_sizes_hyp _ Hi _ H9).
    rewrite (used_sizes_hyp0 _ Hi _ H13).
    trivial.
   rewrite (used_kinds_hyp0 _ Hi _ H13) in H14.
   rewrite (used_kinds_hyp _ Hi _ H9) in H10.
   rewrite H14 in H10.
   inversion H10.
  generalize H6.
  unfold firstfield.
  rewrite <- (used_kinds_hyp _ Hi _ H9).
  rewrite H10.
  simpl.
  rewrite sub_add_id.
  apply (pointer_list_invar_by_suffix (suffix_cons H) H12 (m' := m')).
  generalize (used_children_hyp0 _ Hi).
  inversion 1; subst.
    generalize (used_raw_prop_bool gc_used_hyp1 Hi H15 H16).
    intros; discr.
   rewrite (used_kinds_hyp0 _ Hi _ H14) in H15.
   rewrite (used_kinds_hyp _ Hi _ H9) in H10.
   rewrite H15 in H10.
   inversion H10.
  generalize H17.
  rewrite (used_sizes_hyp _ Hi _ H9).
  rewrite (used_sizes_hyp0 _ Hi _ H14).
  trivial.
 eapply ex_intro.
 split.
  eapply Loop.loop_prop_continue.
  eassumption.
  rewrite <- sub_add_l in Hp'.
  rewrite sub_add_id in Hp'.
  eassumption.
 split.
  assumption.
 rewrite mark_list_post_param_equiv.
 simpl.
 rewrite <- mark_list_post_param_equiv.
 assumption.
inversion H7; subst; auto.
Qed.


Corollary mark_children_exists_0 : 
forall m ap,
marksweep_invariants m mp up gp ->
mark_abstraction m mp up gp ap ->
exists p', Loop.loop_prop (mark_children_body (memory_heap mp) i firstfield) 
  (Some (make_mark_children_body_param m (used_sizes up i))) (Some p') /\
  let m' := mark_children_body_mem p' in
    marksweep_invariants m' mp up gp /\
    mark_abstraction m' mp up gp (mark_list_post_param ap (used_children up (Some (memory_heap mp, i)))).
Proof.
intros m ap Hm_gc Hm_a.
inversion Hm_gc.
inversion marksweep_gc_inv0.
inversion gc_used_hyp0.
inversion Hm_a.
generalize (used_children_hyp _ Hi).
inversion 1; subst.
  generalize (used_raw_prop_bool gc_used_hyp0 Hi H1 H2).
  intros; discr.
 assert (Hff : firstfield = zero).
  unfold firstfield.
  rewrite <- (used_kinds_hyp _ Hi _ H0).
  rewrite H1.
  reflexivity.
 destruct (mark_children_exists_partial (is_suffix_of_id _) (m := m) (j := (sub (add i (Size_header v)) four)) (ap := ap))
 as [p' [Hp' [Hm'gc Hm'a]]] ; try assumption.
  rewrite Hff. 
  rewrite add_zero.
  assumption.
 exists p'.    
 split.
  rewrite <- (used_sizes_hyp _ Hi _ H0).
  generalize Hp'.
  rewrite <- sub_add_l.
  rewrite sub_add_id.
  rewrite add_commut.
  rewrite add_sub_id.
  trivial.
 split; auto.
assert (Hff : firstfield = four).
 unfold firstfield.
 rewrite <- (used_kinds_hyp _ Hi _ H0).
 rewrite H1.
 reflexivity.
destruct (mark_children_exists_partial (is_suffix_of_id _) (m := m) (j := (sub (add i (Size_header v)) four)) (ap := ap))
as [p' [Hp' [Hm'gc Hm'a]]] ; try assumption.
 rewrite Hff. 
 rewrite sub_add_id.
 assumption.
exists p'.    
split.
 rewrite <- (used_sizes_hyp _ Hi _ H0).
 generalize Hp'.
 rewrite <- sub_add_l.
 rewrite sub_add_id.
 rewrite add_commut.
 rewrite add_sub_id.
 trivial.
split; auto.
Qed.

Corollary mark_children_exists : 
forall m ap,
marksweep_invariants m mp up gp ->
mark_abstraction m mp up gp ap ->
exists p', Loop.loop_prop (mark_children_body (memory_heap mp) i firstfield) 
  (Some (make_mark_children_body_param m (used_sizes up i))) (Some p').
Proof.
intros.
destruct (mark_children_exists_0 (m := m) (ap := ap)); try
 assumption; invall; eapply ex_intro; eassumption.
Qed.


Corollary mark_children_final_gc_state :
forall m ap,
marksweep_invariants m mp up gp ->
mark_abstraction m mp up gp ap ->
forall p', Loop.loop_prop (mark_children_body (memory_heap mp) i firstfield) 
  (Some (make_mark_children_body_param m (used_sizes up i))) (Some p') ->
    marksweep_invariants (mark_children_body_mem p') mp up gp.
Proof.
intros.
destruct (mark_children_exists_0 (m := m) (ap := ap)); try
 assumption.
simpl in H2; invall.
generalize (Loop.loop_functional H1 H3).
intros; congruence.
Qed.

Corollary mark_children_final_state :
forall m ap,
marksweep_invariants m mp up gp ->
mark_abstraction m mp up gp ap ->
forall p', Loop.loop_prop (mark_children_body (memory_heap mp) i firstfield) 
  (Some (make_mark_children_body_param m (used_sizes up i))) (Some p') ->
    mark_abstraction (mark_children_body_mem p') mp up gp (mark_list_post_param ap (used_children up (Some (memory_heap mp, i)))).
Proof.
intros.
destruct (mark_children_exists_0 (m := m) (ap := ap)); try
 assumption.
simpl in H2; invall.
generalize (Loop.loop_functional H1 H3).
intros; congruence.
Qed.

End Mark_children.

Section Mark_gray_body.


Variable m : mem.
Variable p : mark_abstraction_param .
Hypothesis Hgc : marksweep_invariants m mp up gp.
Hypothesis Habs : mark_abstraction m mp up gp  p.

Theorem mark_gray_body_exists : exists b, exists m',
  mark_gray_body_2 (memory_heap mp) (memory_hs mp) (memory_he mp) m b m'.
Proof.
unfold mark_gray_body_2.
generalize (cache_pop_exists Hgc Habs).
intros [r [m1 Hm1]].
generalize (cache_pop_final_gc_state Hgc Habs Hm1).
intro Hm1gc.
generalize (cache_pop_final_state Hgc Habs Hm1).
intro Hm1abs.
case_eq r.
 inversion Hm1abs.
 inversion Hm1gc.
 inversion marksweep_gc_inv0.
 inversion gc_used_hyp0.
 intros blof ? ; subst.
 unfold mark_gray_body_middle.
 generalize (cache_pop_value_some Hgc Habs Hm1 (refl_equal _)).
 intros [o [k1 [k2 [Hcc [? [Hmem Hnot_raw]]]]]].
 subst.
 generalize (block_header used_heap_hyp Hmem).
 intros [header Hheader].
 generalize (set_black_exists Hm1gc Hmem header).
 intros [m2 Hm2].
 generalize (set_black_final_gc_state Hm1gc Hm1abs Hmem Hheader Hm2). 
 intros Hm2gc.
 generalize (set_black_final_state Hm1gc Hm1abs Hmem Hm2). 
 intros Hm2abs.
 generalize (mark_children_exists Hmem Hnot_raw Hm2gc Hm2abs).
 intros [p' Hp'].
 destruct p'.
 repeat esplit.
  eassumption.
 simpl.
 split.
  reflexivity.
 rewrite <- Hheader.
 rewrite Hm2.
 esplit.
 rewrite (used_kinds_hyp _ Hmem _ Hheader).
 rewrite (used_sizes_hyp _ Hmem _ Hheader).
 eexact Hp'.
intros; subst.
repeat esplit.
 eassumption.
simpl.
split; reflexivity.
Qed.

Variable b : bool.
Variable m' : mem.
Hypothesis Hm' :   mark_gray_body_2 (memory_heap mp) (memory_hs mp) (memory_he mp) m b m'.

Lemma mark_gray_body_final_gc_state : marksweep_invariants m' mp up gp.
Proof.
unfold mark_gray_body_2 in Hm'.
inversion Hm' as [m1 [r [Hm1 Hr]]].
generalize (cache_pop_final_gc_state Hgc Habs Hm1).
intro Hm1gc.
generalize (cache_pop_final_state Hgc Habs Hm1).
intro Hm1abs.
destruct r.
 inversion Hr as [? Hm'0].
 subst.
 generalize Hm'0.
 unfold mark_gray_body_middle.
 destruct v; try contradiction.
 case_eq (load Mint32 m1 b (signed (sub i four))); try contradiction.
 destruct v ; try contradiction.
 case_eq (store Mint32 m1 b (signed (sub i four)) (Vint (or i0 COLOR_BLACK)));
 try contradiction.
 intros m2 Hm2 Hi0 [n Hn].
 generalize (cache_pop_value_some Hgc Habs Hm1 (refl_equal _)).
 intros [o [k1 [k2 [Hcc [Heq [Hmem Hnot_raw]]]]]].
 injection Heq; intros; subst.
 symmetry in Hi0.
 generalize (set_black_final_gc_state Hm1gc Hm1abs Hmem Hi0 Hm2). 
 intros Hm2gc.
 generalize (set_black_final_state Hm1gc Hm1abs Hmem Hm2). 
 intros Hm2abs.
 rewrite (used_kinds_hyp (gc_used_hyp (marksweep_gc_inv Hm1gc)) Hmem Hi0) in Hn.
 rewrite (used_sizes_hyp (gc_used_hyp (marksweep_gc_inv Hm1gc)) Hmem Hi0) in Hn.
 exact (mark_children_final_gc_state Hmem Hnot_raw Hm2gc Hm2abs Hn).
invall; congruence.
Qed.

Definition mark_gray_body_post_param :=
let (_, cocc) :=
Mark_abstract.mark_gray_body (used_valid mp up) eq_optptr first_gray marksweep_cache_is_full marksweep_cache_full_push marksweep_cache_full_pop (used_children up) (used_raw up) (marksweep_col p, (gray_cache_overflow_bool p, marksweep_cache p, gray_cache_offset_value p)) in
let (col', occ) := cocc in
let (oc, cache_full') := occ in
let (overflow', cache') := oc in
  make_mark_abstraction_param
  overflow'
  cache_full'
  col'
  cache'.

Lemma mark_gray_body_final_state : mark_abstraction m' mp up gp mark_gray_body_post_param.
Proof.
unfold mark_gray_body_2 in Hm'.
inversion Hm' as [m1 [r [Hm1 Hr]]].
generalize (cache_pop_final_gc_state Hgc Habs Hm1).
intro Hm1gc.
generalize (cache_pop_final_state Hgc Habs Hm1).
intro Hm1abs.
destruct r.
 inversion Hr as [? Hm'0].
 subst.
 generalize Hm'0.
 unfold mark_gray_body_middle.
 destruct v; try contradiction.
 case_eq (load Mint32 m1 b (signed (sub i four))); try contradiction.
 destruct v ; try contradiction.
 case_eq (store Mint32 m1 b (signed (sub i four)) (Vint (or i0 COLOR_BLACK)));
 try contradiction.
 intros m2 Hm2 Hi0 [n Hn].
 generalize (cache_pop_value_some Hgc Habs Hm1 (refl_equal _)).
 intros [o [k1 [k2 [Hcc [Heq [Hmem Hnot_raw]]]]]].
 injection Heq; intros; subst.
 symmetry in Hi0.
 generalize (set_black_final_gc_state Hm1gc Hm1abs Hmem Hi0 Hm2). 
 intros Hm2gc.
 generalize (set_black_final_state Hm1gc Hm1abs Hmem Hm2). 
 intros Hm2abs.
 rewrite (used_kinds_hyp (gc_used_hyp (marksweep_gc_inv Hm1gc)) Hmem Hi0) in Hn.
 rewrite (used_sizes_hyp (gc_used_hyp (marksweep_gc_inv Hm1gc)) Hmem Hi0) in Hn.
 generalize (mark_children_final_state Hmem Hnot_raw Hm2gc Hm2abs Hn).
 simpl.
 replace  (mark_list_post_param (set_black_post_param (cache_pop_post_param p) o)
        (used_children up (Some (memory_heap mp, o))))
  with mark_gray_body_post_param.
  tauto.
 unfold mark_gray_body_post_param.
 unfold Mark_abstract.mark_gray_body.
 unfold cache_pop_post_param.
 unfold set_black_post_param.
 unfold mark_list_post_param.
 simpl.
 rewrite Hcc.
 simpl.
 destruct (
           Mark_abstract.mark_list (used_valid mp up) eq_optptr
          marksweep_cache_is_full marksweep_cache_full_push 
          (used_raw up)
          (Mark_abstract.set_color eq_optptr (Some (memory_heap mp, o))
             Mark_abstract.Black (marksweep_col p))
          (gray_cache_overflow_bool p) k1 k2
          (used_children up (Some (memory_heap mp, o)))
 ).
 destruct p0.
 destruct p0.
 reflexivity.
inversion Hr.
subst.
generalize Hm1abs.
unfold cache_pop_post_param.
unfold mark_gray_body_post_param.
unfold Mark_abstract.mark_gray_body.
generalize (cache_pop_value_none Hgc Habs Hm1 (refl_equal _)).
intros Hk.
rewrite Hk.
trivial.
Qed.

Lemma mark_gray_body_final_bool_state : 
let (b', cocc) :=
Mark_abstract.mark_gray_body (used_valid mp up) eq_optptr first_gray marksweep_cache_is_full marksweep_cache_full_push marksweep_cache_full_pop (used_children up) (used_raw up) (marksweep_col p, (gray_cache_overflow_bool p, marksweep_cache p, gray_cache_offset_value p)) in
b = b'.
Proof.
unfold mark_gray_body_2 in Hm'.
inversion Hm' as [m1 [r [Hm1 Hr]]].
generalize (cache_pop_final_gc_state Hgc Habs Hm1).
intro Hm1gc.
generalize (cache_pop_final_state Hgc Habs Hm1).
intro Hm1abs.
unfold Mark_abstract.mark_gray_body.
destruct r.
 inversion Hr as [? Hm'0].
 subst.
 generalize Hm'0.
 unfold mark_gray_body_middle.
 destruct v; try contradiction.
 case_eq (load Mint32 m1 b (signed (sub i four))); try contradiction.
 destruct v ; try contradiction.
 case_eq (store Mint32 m1 b (signed (sub i four)) (Vint (or i0 COLOR_BLACK)));
 try contradiction.
 intros m2 Hm2 Hi0 [n Hn].
 generalize (cache_pop_value_some Hgc Habs Hm1 (refl_equal _)).
 intros [o [k1 [k2 [Hcc [Heq [Hmem Hnot_raw]]]]]].
 injection Heq; intros; subst.
 rewrite Hcc.
 destruct (
           Mark_abstract.mark_list (used_valid mp up) eq_optptr
             marksweep_cache_is_full marksweep_cache_full_push 
             (used_raw up)
             (Mark_abstract.set_color eq_optptr (Some (memory_heap mp, o))
                Mark_abstract.Black (marksweep_col p))
             (gray_cache_overflow_bool p) k1 k2
             (used_children up (Some (memory_heap mp, o))) 
 ).
 destruct p0.
 destruct p0.
 reflexivity.
inversion Hr.
subst.
unfold cache_pop_post_param.
unfold mark_gray_body_post_param.
unfold Mark_abstract.mark_gray_body.
generalize (cache_pop_value_none Hgc Habs Hm1 (refl_equal _)).
intros Hk.
rewrite Hk.
trivial.
Qed.

End Mark_gray_body. 

Section Mark_gray_if_terminates.

Theorem mark_gray_exists_cond :
  forall k k', Loop.loop_prop (
    Mark_abstract.mark_gray_body (used_valid mp up) eq_optptr first_gray marksweep_cache_is_full marksweep_cache_full_push marksweep_cache_full_pop (used_children up) (used_raw up)
  ) k k' ->
  forall p m,
    marksweep_invariants m mp up gp -> mark_abstraction m mp up gp p ->
    k = (marksweep_col p, (gray_cache_overflow_bool p, marksweep_cache p, gray_cache_offset_value p)) ->
    exists m', Loop.genloop_prop (
      mark_gray_body_2 (memory_heap mp) (memory_hs mp) (memory_he mp)
    ) m m'.
Proof.
induction 1.
 intros p m Hgc Habs ?.
 subst.
 generalize (mark_gray_body_exists Hgc Habs).
 intros [b [m' Hm']].
 generalize (mark_gray_body_final_bool_state Hgc Habs Hm').
 rewrite H.
 intros ; subst.
 esplit.
 eapply Loop.genloop_prop_interrupt.
 eassumption.
intros p m Hgc Habs ?.
subst.
generalize (mark_gray_body_exists Hgc Habs).
intros [b [m' Hm']].
generalize (mark_gray_body_final_bool_state Hgc Habs Hm').
rewrite H.
intros ; subst.
generalize (mark_gray_body_final_gc_state Hgc Habs Hm').
intros Hm'gc.
generalize (mark_gray_body_final_state Hgc Habs Hm').
unfold mark_gray_body_post_param.
rewrite H.
destruct a'.
destruct p0.
destruct p0.
intro Hm'abs.
generalize (IHloop_prop _ _ Hm'gc Hm'abs (refl_equal _)).
intros [m'0 Hm'0].
esplit.
eapply Loop.genloop_prop_continue.
 eassumption.
eassumption.
Qed.


Theorem mark_gray_final_gc_state :
  forall m m', Loop.genloop_prop (
    mark_gray_body_2 (memory_heap mp) (memory_hs mp) (memory_he mp)
  ) m m' ->
  forall p,
    marksweep_invariants m mp up gp -> mark_abstraction m mp up gp p
    ->
    marksweep_invariants m' mp up gp.
Proof.
induction 1.
 intros p Hgc Habs.
 eapply mark_gray_body_final_gc_state; eassumption.
intros p Hgc Habs.
eapply IHgenloop_prop.
 eapply mark_gray_body_final_gc_state; eassumption.
 eapply mark_gray_body_final_state; eassumption.
Qed.

Definition mark_gray_post_param p p' :=
  Mark_abstract.mark_gray_prop (used_valid mp up) eq_optptr first_gray marksweep_cache_is_full marksweep_cache_full_push marksweep_cache_full_pop (used_children up) (used_raw up)
  (marksweep_col p) (gray_cache_overflow_bool p) (marksweep_cache p) (gray_cache_offset_value p)
  (marksweep_col p') (gray_cache_overflow_bool p') (marksweep_cache p') (gray_cache_offset_value p').

Lemma mark_gray_post_param_functional p p'1 p'2 :
  mark_gray_post_param p p'1 -> mark_gray_post_param p p'2 ->
  p'1 = p'2.
Proof.
 unfold mark_gray_post_param.
 intros p.
 destruct p'1.
 destruct p'2.
 simpl.
 intros Hp'1 Hp'2.
 generalize (Mark_abstract.mark_gray_prop_func Hp'1 Hp'2).
 intros; invall; congruence.
Qed.

Definition mark_gray_post_param_2 p p' :=
  Loop.loop_prop
  (Mark_abstract.mark_gray_body (used_valid mp up) eq_optptr first_gray
    marksweep_cache_is_full marksweep_cache_full_push
    marksweep_cache_full_pop (used_children up) (used_raw up))
  (marksweep_col p,
    (gray_cache_overflow_bool p, marksweep_cache p,
      gray_cache_offset_value p))
  (marksweep_col p',
    (gray_cache_overflow_bool p', marksweep_cache p',
      gray_cache_offset_value p')).

Lemma mark_gray_post_param_is_param2 p p' :
  mark_gray_post_param p p' -> mark_gray_post_param_2 p p'.
Proof.
unfold mark_gray_post_param.
unfold mark_gray_post_param_2.
intros.
apply  Mark_abstract.mark_gray_body_loop_complete.
assumption.
Qed.

Lemma mark_gray_post_param2_is_param p p' :
  mark_gray_post_param_2 p p' -> mark_gray_post_param p p'.
Proof.
unfold mark_gray_post_param.
unfold mark_gray_post_param_2.
intros.
apply  Mark_abstract.mark_gray_body_loop_correct.
assumption.
Qed.
  
Lemma mark_gray_post_param_exists :
  forall m m', Loop.genloop_prop (
    mark_gray_body_2 (memory_heap mp) (memory_hs mp) (memory_he mp)
  ) m m' ->
  forall p,
    marksweep_invariants m mp up gp -> mark_abstraction m mp up gp p
    ->
    exists p',
      mark_gray_post_param p p'.
Proof.
induction 1.
 intros p Hgc Habs.
 generalize (mark_gray_body_final_gc_state Hgc Habs H).
 intros Ha'gc.
 generalize (mark_gray_body_final_state Hgc Habs H).
 unfold mark_gray_body_post_param.
 intros Ha'abs.
 generalize (mark_gray_body_final_bool_state Hgc Habs H).
 intros Ha'bool.
 exists (mark_gray_body_post_param p).
 unfold mark_gray_post_param.
 unfold mark_gray_body_post_param.
 eapply Mark_abstract.mark_gray_body_loop_correct.
 eapply Loop.loop_prop_interrupt.
 destruct (
  Mark_abstract.mark_gray_body (used_valid mp up) eq_optptr first_gray
  marksweep_cache_is_full marksweep_cache_full_push
  marksweep_cache_full_pop (used_children up) (used_raw up)
  (marksweep_col p,
   (gray_cache_overflow_bool p, marksweep_cache p,
    gray_cache_offset_value p))
 ).
 destruct p0.
 destruct p0.
 destruct p0.
 simpl.
 congruence.
intros p Hgc Habs.   
generalize (mark_gray_body_final_gc_state Hgc Habs H).
intros Ha'gc.
generalize (mark_gray_body_final_state Hgc Habs H).
unfold mark_gray_body_post_param.
intros Ha'abs.
generalize (mark_gray_body_final_bool_state Hgc Habs H).
intros Ha'bool.
generalize (IHgenloop_prop _ Ha'gc Ha'abs).
intros [p' Hp'].
exists p'.
unfold mark_gray_post_param.
eapply Mark_abstract.mark_gray_body_loop_correct.
 case_eq (
     Mark_abstract.mark_gray_body (used_valid mp up) eq_optptr first_gray
     marksweep_cache_is_full marksweep_cache_full_push
     marksweep_cache_full_pop (used_children up) (used_raw up)
     (marksweep_col p,
     (gray_cache_overflow_bool p, marksweep_cache p,
     gray_cache_offset_value p))
 ).
 intros b p0 Hb.
 destruct p0. 
 destruct p0.
 destruct p0.
 rewrite Hb in *.
 subst.
eapply Loop.loop_prop_continue.
 rewrite Hb.
 reflexivity.
unfold mark_gray_post_param in Hp'.
simpl in Hp'.
apply Mark_abstract.mark_gray_body_loop_complete.
assumption.
Qed.

Theorem mark_gray_final_state :
  forall m  m', Loop.genloop_prop (
      mark_gray_body_2 (memory_heap mp) (memory_hs mp) (memory_he mp)
    ) m m' ->
  forall p,
    marksweep_invariants m mp up gp -> mark_abstraction m mp up gp p ->
    forall p',
      mark_gray_post_param p p' ->
      mark_abstraction m' mp up gp p'.
Proof.
induction 1.
 intros p Hgc Habs p'.
 unfold mark_gray_post_param.
 intros Hp'.
 generalize (Mark_abstract.mark_gray_body_loop_complete Hp').
 intro Hp'loop.
 generalize (mark_gray_body_final_gc_state Hgc Habs H).
 intros Hm'gc.
 generalize (mark_gray_body_final_state Hgc Habs H).
 intros Hm'abs.
 generalize (mark_gray_body_final_bool_state Hgc Habs H).
 intros Hm'b.
 inversion Hp'loop; subst.
  unfold mark_gray_body_post_param in Hm'abs.
  rewrite H0 in Hm'abs.
  destruct p'; assumption.
 rewrite H0 in Hm'b.
 discriminate.
intros p Hgc Habs p'.
unfold mark_gray_post_param.
intros Hp'.
generalize (Mark_abstract.mark_gray_body_loop_complete Hp').
intro Hp'loop.
generalize (mark_gray_body_final_gc_state Hgc Habs H).
intros Hm'gc.
generalize (mark_gray_body_final_state Hgc Habs H).
intros Hm'abs.
generalize (mark_gray_body_final_bool_state Hgc Habs H).
intros Hm'b.
inversion Hp'loop; subst.
 rewrite H1 in Hm'b.
 discriminate.
eapply IHgenloop_prop.
  assumption.
 eassumption.
unfold mark_gray_body_post_param.
rewrite H1.
destruct a'0.
destruct p0.
destruct p0.
unfold mark_gray_post_param.
simpl.
eapply Mark_abstract.mark_gray_body_loop_correct.
assumption.
Qed.

End Mark_gray_if_terminates.

Section Mark_all_roots.

Section Mark_root_list.

Variable r : block.

Opaque load store alloc free mark_block_body.

Lemma mark_root_list_terminates : forall l m n d, root_list m r n d l ->
forall p, marksweep_invariants m mp up gp -> mark_abstraction m mp up gp p ->
(forall pl, root_list_position_list r n d pl -> forall i, member i pl -> member i (flatten (used_rootpos up))) ->
(forall s, member s l -> member s (flatten (used_roots up))) ->
Loop.loop_term mark_root_list_body (Some (make_mark_root_list_param m n r d)).
Proof.
induction l. (* because m changes over time *)
 inversion 1.
 subst.
 intros p Hinv Habstr Hrootpos Hroot.
 eapply Loop.loop_term_interrupt.
 unfold mark_root_list_body.
 simpl.
 reflexivity.
inversion 1.
subst.
intros p Hinv Habstr Hrootpos Hroot.
case_eq (mark_root_list_body (Some (make_mark_root_list_param m n r d))).
intros bf pf Hpf.
generalize Hpf.
unfold mark_root_list_body at 1; simpl.
case_eq (eq n zero).
 intro Heq; generalize (eq_bool_eq_prop Heq); intros; contradiction.
intros ?.
rewrite <- H4.
rewrite (val_is_pointer_or_dumb_constructs_some H7).
assert (forall (b : block) (i : int), a = Some (b, i) -> b = memory_heap mp) as Ha_heap.
  intros; subst;
  generalize (Hroot (Some (b, i)) (member_head _ _));
  intro Hmem;
  generalize (used_roots_are_blocks (gc_used_hyp (marksweep_gc_inv Hinv)) Hmem);
  tauto.
assert (forall (b : block) (i : int),
     a = Some (b, i) -> member i (used_blocklist up)) as Ha_mem.
  intros; subst;
  generalize (Hroot (Some (b, i)) (member_head _ _));
  intro Hmem;
  generalize (used_roots_are_blocks (gc_used_hyp (marksweep_gc_inv Hinv)) Hmem);
  tauto.
destruct (mark_block_runs_well Hinv Habstr Ha_heap Ha_mem) as [m' Hm'].
rewrite Hm'.
injection 1.
intros; subst.
eapply Loop.loop_term_continue.
 eassumption.
generalize (root_list_describes H).
intro Hdesc.
generalize (root_list_desc_root_position_list Hdesc).
intros [pl0 Hpl0].
inversion Hpl0.
 contradiction.
subst.
symmetry in Hm'.
generalize (mark_block_final_gc_state Hinv Habstr Ha_heap Ha_mem Hm').
intro Hm'inv.
generalize (mark_block_final_state Hinv Habstr Ha_heap Ha_mem Hm').
intro Hm'abstr.
eapply IHl.
    eapply root_list_invar.
      eassumption.
     eassumption.
    intros b i Hbi.
    assert (member (b, i) (flatten (used_rootpos up))).
     eapply Hrootpos.
      eassumption.
     auto.
    eapply mark_block_invariant_blocks.
             assumption.
            eassumption.
           eassumption.
          assumption.
         assumption.
        intros.
        eapply alloc_rootpos_indep; eauto.
       eapply gray_cache_rootpos_indep; eauto.
      eapply used_rootpos_not_in_heap; eauto.
     eapply gray_cache_offset_rootpos_indep; eauto.
    eapply gray_cache_overflow_rootpos_indep; eauto.
   assumption.
  eassumption.
 intros pl2 Hpl2.
 replace pl2 with l0.
  intros; eauto.
 eapply root_list_position_list_func; eauto.
intros; eauto.
Qed. 

Corollary mark_root_list_exists : forall l m n d, root_list m r n d l ->
forall p, marksweep_invariants m mp up gp -> mark_abstraction m mp up gp p ->
(forall pl, root_list_position_list r n d pl -> forall i, member i pl -> member i (flatten (used_rootpos up))) ->
(forall s, member s l -> member s (flatten (used_roots up))) ->
exists p', Loop.loop_prop mark_root_list_body (Some (make_mark_root_list_param m n r d)) (Some p').
Proof.
intros l m n d Hl p Hgc Habs Hrootpos Hroots.
generalize (mark_root_list_terminates Hl Hgc Habs Hrootpos Hroots).
intro Hterm.
generalize (Loop.loop Hterm).
intros [a' Ha'].
destruct a'.
 esplit; eassumption.
destruct (mark_root_list_res_some Ha' (refl_equal _)).
Qed.

Lemma mark_root_list_final_gc_state : 
forall l m n d, root_list m r n d l ->
forall p, marksweep_invariants m mp up gp -> mark_abstraction m mp up gp p ->
(forall pl, root_list_position_list r n d pl -> forall i, member i pl -> member i (flatten (used_rootpos up))) ->
(forall s, member s l -> member s (flatten (used_roots up))) ->
forall rp',
Loop.loop_prop mark_root_list_body (Some (make_mark_root_list_param m n r d)) (Some rp') ->
marksweep_invariants (mark_root_list_mem rp') mp up gp.
Proof.
induction l. (* because m changes over time *)
 inversion 1.
 subst.
 intros p Hinv Habstr Hrootpos Hroot.
 inversion 1.
  subst.
  generalize H1.
  unfold mark_root_list_body.
  simpl.
  injection 1; intros; subst.
  simpl.
  assumption.
 subst.
 generalize H1.
 unfold mark_root_list_body.
 simpl.
 discriminate 1.
inversion 1.
subst.
intros p Hinv Habstr Hrootpos Hroot.
case_eq (mark_root_list_body (Some (make_mark_root_list_param m n r d))).
intros bf pf Hpf.
generalize Hpf.
unfold mark_root_list_body at 1; simpl.
case_eq (eq n zero).
 intro Heq; generalize (eq_bool_eq_prop Heq); intros; contradiction.
intros ?.
rewrite <- H4.
rewrite (val_is_pointer_or_dumb_constructs_some H7).
assert (forall (b : block) (i : int), a = Some (b, i) -> b = memory_heap mp) as Ha_heap.
  intros; subst;
  generalize (Hroot (Some (b, i)) (member_head _ _));
  intro Hmem;
  generalize (used_roots_are_blocks (gc_used_hyp (marksweep_gc_inv Hinv)) Hmem);
  tauto.
assert (forall (b : block) (i : int),
     a = Some (b, i) -> member i (used_blocklist up)) as Ha_mem.
  intros; subst;
  generalize (Hroot (Some (b, i)) (member_head _ _));
  intro Hmem;
  generalize (used_roots_are_blocks (gc_used_hyp (marksweep_gc_inv Hinv)) Hmem);
  tauto.
destruct (mark_block_runs_well Hinv Habstr Ha_heap Ha_mem) as [m' Hm'].
rewrite Hm'.
injection 1.
intros until 2; subst.
inversion 1.
 subst.
 discr.
subst.
rewrite Hpf in H5.
injection H5.
intros ; subst.
generalize (root_list_describes H).
intro Hdesc.
generalize (root_list_desc_root_position_list Hdesc).
intros [pl0 Hpl0].
inversion Hpl0.
 contradiction.
subst.
symmetry in Hm'.
generalize (mark_block_final_gc_state Hinv Habstr Ha_heap Ha_mem Hm').
intro Hm'inv.
generalize (mark_block_final_state Hinv Habstr Ha_heap Ha_mem Hm').
intro Hm'abstr.
eapply IHl.
    eapply root_list_invar.
      eassumption.
     eassumption.
    intros b i Hbi.
    assert (member (b, i) (flatten (used_rootpos up))).
     eapply Hrootpos.
      eassumption.
     auto.
    eapply mark_block_invariant_blocks.
             assumption.
            eassumption.
           eassumption.
          assumption.
          eassumption.
        intros.
        eapply alloc_rootpos_indep; eauto.
       eapply gray_cache_rootpos_indep; eauto.
      eapply used_rootpos_not_in_heap; eauto.
     eapply gray_cache_offset_rootpos_indep; eauto.
    eapply gray_cache_overflow_rootpos_indep; eauto.
   assumption.
  eassumption.
 intros pl2 Hpl2.
 replace pl2 with l0.
  intros; eauto.
 eapply root_list_position_list_func; eauto.
intros; eauto.
assumption.
Qed.

Lemma mark_root_list_final_state : 
forall l m n d, root_list m r n d l ->
forall p, marksweep_invariants m mp up gp -> mark_abstraction m mp up gp p ->
(forall pl, root_list_position_list r n d pl -> forall i, member i pl -> member i (flatten (used_rootpos up))) ->
(forall s, member s l -> member s (flatten (used_roots up))) ->
forall rp',
Loop.loop_prop mark_root_list_body (Some (make_mark_root_list_param m n r d)) (Some rp') ->
mark_abstraction (mark_root_list_mem rp') mp up gp (mark_list_post_param_2 p l).
Proof.
induction l. (* because m changes over time *)
 inversion 1.
 subst.
 intros p Hinv Habstr Hrootpos Hroot.
 inversion 1.
  subst.
  generalize H1.
  unfold mark_root_list_body.
  simpl.
  injection 1; intros; subst.
  simpl.  
  assumption.
 subst.
 generalize H1.
 unfold mark_root_list_body.
 simpl.
 discriminate 1.
inversion 1.
subst.
intros p Hinv Habstr Hrootpos Hroot.
case_eq (mark_root_list_body (Some (make_mark_root_list_param m n r d))).
intros bf pf Hpf.
generalize Hpf.
unfold mark_root_list_body at 1; simpl.
case_eq (eq n zero).
 intro Heq; generalize (eq_bool_eq_prop Heq); intros; contradiction.
intros ?.
rewrite <- H4.
rewrite (val_is_pointer_or_dumb_constructs_some H7).
assert (forall (b : block) (i : int), a = Some (b, i) -> b = memory_heap mp) as Ha_heap.
  intros; subst;
  generalize (Hroot (Some (b, i)) (member_head _ _));
  intro Hmem;
  generalize (used_roots_are_blocks (gc_used_hyp (marksweep_gc_inv Hinv)) Hmem);
  tauto.
assert (forall (b : block) (i : int),
     a = Some (b, i) -> member i (used_blocklist up)) as Ha_mem.
  intros; subst;
  generalize (Hroot (Some (b, i)) (member_head _ _));
  intro Hmem;
  generalize (used_roots_are_blocks (gc_used_hyp (marksweep_gc_inv Hinv)) Hmem);
  tauto.
destruct (mark_block_runs_well Hinv Habstr Ha_heap Ha_mem) as [m' Hm'].
rewrite Hm'.
injection 1.
intros until 2; subst.
inversion 1.
 subst.
 discr.
subst.
rewrite Hpf in H5.
injection H5.
intros ; subst.
generalize (root_list_describes H).
intro Hdesc.
generalize (root_list_desc_root_position_list Hdesc).
intros [pl0 Hpl0].
inversion Hpl0.
 contradiction.
subst.
symmetry in Hm'.
generalize (mark_block_final_gc_state Hinv Habstr Ha_heap Ha_mem Hm').
intro Hm'inv.
generalize (mark_block_final_state Hinv Habstr Ha_heap Ha_mem Hm').
intro Hm'abstr.
eapply IHl.
    eapply root_list_invar.
      eassumption.
     eassumption.
    intros b i Hbi.
    assert (member (b, i) (flatten (used_rootpos up))).
     eapply Hrootpos.
      eassumption.
     auto.
    eapply mark_block_invariant_blocks.
             assumption.
            eassumption.
           eassumption.
          assumption.
          eassumption.
        intros.
        eapply alloc_rootpos_indep; eauto.
       eapply gray_cache_rootpos_indep; eauto.
      eapply used_rootpos_not_in_heap; eauto.
     eapply gray_cache_offset_rootpos_indep; eauto.
    eapply gray_cache_overflow_rootpos_indep; eauto.
   assumption.
  eassumption.
 intros pl2 Hpl2.
 replace pl2 with l0.
  intros; eauto.
 eapply root_list_position_list_func; eauto.
intros; eauto.
assumption.
Qed.

End Mark_root_list.

Lemma mark_all_roots_terminates_0 : forall l m v, all_roots m v l ->
forall p, marksweep_invariants m mp up gp -> mark_abstraction m mp up gp p ->
(forall pl, root_position_list m v pl -> forall i, member i (flatten pl) -> member i (flatten (used_rootpos up))) ->
(forall s, member s l -> member s (used_roots up)) ->
Loop.genloop_term mark_all_roots_body (make_mark_all_roots_param v m).
Proof.
induction l.
 inversion 1.
 subst.
 intros p Hgc Habs _ _.
 subst.
 eapply Loop.genloop_term_interrupt.
 eapply mark_all_roots_body_end.
 unfold mark_all_roots_body_before.
 simpl.
 reflexivity.
inversion 1.
subst.
intros p Hgc Habs Hpl Hs.
subst.
generalize (all_roots_desc_root_position_list (all_roots_describes H)).
intros [l0 Hl0].
inversion Hl0.
subst.
replace n0 with n in *; [|congruence].
replace v'0 with v' in *; [|congruence].
assert (
   forall pl : list (block * int),
   root_list_position_list r n (add (add d four) four) pl ->
   forall i : block * int,
   member i pl -> member i (flatten (used_rootpos up))
).
 intros pl0 Hpl0.
 replace pl0 with l1 in *.
 intros.
 eapply Hpl.
 eassumption.
 eapply member_flatten_intro.
 eapply member_head.
 auto.
 eapply root_list_position_list_func.
 eassumption.
 assumption.
assert (
 forall s : option (block * int),
 member s a -> member s (flatten (used_roots up))

).
 intros.
 eapply member_flatten_intro.
 2 : eassumption.
 eapply Hs.
 auto.
assert (
   Loop.loop_term mark_root_list_body
     (Some
        (make_mark_root_list_param m n r
           (add (add d four) four)))
).
 eapply mark_root_list_terminates; eassumption.
generalize (Loop.loop H11).
intros [a' Ha'].
destruct a' ; try destruct (mark_root_list_res_some Ha' (refl_equal _)).
assert (marksweep_invariants (mark_root_list_mem m0) mp up gp).
 eapply mark_root_list_final_gc_state; eassumption.
assert (mark_abstraction (mark_root_list_mem m0) mp up gp (mark_list_post_param_2 p a)).
 eapply mark_root_list_final_state; eassumption.
inversion Hgc.
inversion marksweep_gc_inv0.
inversion gc_used_hyp0.
inversion H13.
inversion marksweep_gc_inv1.
inversion gc_used_hyp1.
generalize (root_position_list_values_invar used_roots_hyp used_rootpos_hyp used_roots_hyp0 used_rootpos_hyp0).
intros Hinv.
eapply Loop.genloop_term_continue.
 eapply mark_all_roots_body_cont.
   unfold mark_all_roots_body_before.
   simpl.
   rewrite <- H3.
   reflexivity.
  simpl.
  eassumption.
 unfold mark_all_roots_body_after.
 simpl.
 rewrite <- Hinv.
 rewrite <- H6.
 reflexivity.
 eapply Hpl.
 eassumption.
 eapply member_flatten_intro.
 apply member_head.
 auto.
eapply IHl.
 eapply all_roots_invar.
 eassumption.
 eassumption.
 intros.
 eapply Hinv.
 eapply Hpl.
 eassumption.
 unfold flatten.
 apply member_app_right.
 assumption.
assumption.
eassumption.
intros.
replace pl with l' in *.
eapply Hpl.
eassumption.
unfold flatten.
fold flatten.
apply member_app_right.
assumption.
symmetry.
eapply root_position_list_func.
eassumption.
eapply root_position_list_invar.
eassumption.
intros.
eapply Hinv.
eapply Hpl.
eassumption.
unfold flatten.
fold flatten.
apply member_app_right.
assumption.
intros.
eauto.
Qed.
 
Corollary mark_all_roots_terminates : forall m p, marksweep_invariants m mp up gp -> mark_abstraction m mp up gp p ->
{p2 | Loop.genloop_prop mark_all_roots_body (make_mark_all_roots_param (memory_rd mp) m) p2}.
Proof.
intros.
eapply all_roots_loop.
eapply mark_all_roots_terminates_0.
eapply used_roots_hyp.
eauto.
assumption.
eassumption.
intros.
replace (used_rootpos up) with pl.
assumption.
eapply root_position_list_func.
eassumption.
eapply used_rootpos_hyp; eauto.
trivial.
Defined.

Lemma mark_all_roots_final_gc_state_0 : forall ap ap',
Loop.genloop_prop mark_all_roots_body ap ap' ->
forall l m v p, all_roots m v l ->
marksweep_invariants m mp up gp -> mark_abstraction m mp up gp p ->
(forall pl, root_position_list m v pl -> forall i, member i (flatten pl) -> member i (flatten (used_rootpos up))) ->
(forall s, member s l -> member s (used_roots up)) ->
mark_all_roots_mem ap = m ->
mark_all_roots_root ap = v ->
marksweep_invariants (mark_all_roots_mem ap') mp up gp.
Proof.
induction 1.
 inversion H.
 subst.
 generalize H0.
 unfold mark_all_roots_body_before.
 destruct (mark_all_roots_root a); try (intros; discriminate).
 destruct (eq i zero); try (intros; discriminate). 
 injection 1; intros; subst.
 assumption.
inversion H. 
subst.
generalize H1.
unfold mark_all_roots_body_before.
case_eq (mark_all_roots_root a); try (intros; discriminate).
 intros i ?.
 destruct (eq i zero); intros; discriminate.
intros b i Hbi.
case_eq (
 load Mint32 (mark_all_roots_mem a) b
       (signed (add i four))
); try (intros; discriminate).
destruct v; try (intros; discriminate).
intros Hval.
injection 1.
intros ? ? l m v p Hl Hgc Habs Hpl Hs ? ?; subst.
clear H4.
inversion Hl.
subst.
generalize (all_roots_desc_root_position_list (all_roots_describes Hl)).
intros [l1 Hl1].
inversion Hl1.
subst.
replace n0 with n in *; [|congruence].
replace v'0 with v' in *; [|congruence].
assert (
   forall pl : list (block * int),
   root_list_position_list b n (add (add i four) four) pl ->
   forall j : block * int,
   member j pl -> member j (flatten (used_rootpos up))
).
 intros pl0 Hpl0.
 replace pl0 with l in *.
 intros.
 eapply Hpl.
 eassumption.
 eapply member_flatten_intro.
 eapply member_head.
 auto.
 eapply root_list_position_list_func.
 eassumption.
 assumption.
assert (
 forall s : option (block * int),
 member s l0 -> member s (flatten (used_roots up))
).
 intros.
 eapply member_flatten_intro.
 2 : eassumption.
 eapply Hs.
 auto.
simpl in H3.
simpl in H2.
replace i0 with n in *; [ | congruence ].
assert (marksweep_invariants (mark_root_list_mem rp''0) mp up gp).
 eapply mark_root_list_final_gc_state; eassumption.
assert (mark_abstraction (mark_root_list_mem rp''0) mp up gp (mark_list_post_param_2 p l0)).
 eapply mark_root_list_final_state; eassumption.
generalize H3.
unfold mark_all_roots_body_after.
simpl.
case_eq (
 load Mint32 (mark_root_list_mem rp''0) b (signed i) 
) ; try (intros; discriminate).
injection 2. 
clear H19.
intros; subst.
inversion Hgc.
inversion marksweep_gc_inv0.
inversion gc_used_hyp0.
inversion H15.
inversion marksweep_gc_inv1.
inversion gc_used_hyp1.
generalize (root_position_list_values_invar used_roots_hyp used_rootpos_hyp used_roots_hyp0 used_rootpos_hyp0).
intros Hinv.
replace v with v' in *.
eapply IHgenloop_prop.
7 : simpl; reflexivity.
6 : simpl; reflexivity.
eapply all_roots_invar.
 eassumption.
 eassumption.
 intros.
 eapply Hinv.
 eapply Hpl.
 eassumption.
 unfold flatten.
 apply member_app_right.
 assumption.
assumption.
eassumption.
intros.
replace pl with l'0 in *.
eapply Hpl.
eassumption.
unfold flatten.
fold flatten.
apply member_app_right.
assumption.
symmetry.
eapply root_position_list_func.
eassumption.
eapply root_position_list_invar.
eassumption.
intros.
eapply Hinv.
eapply Hpl.
eassumption.
unfold flatten.
fold flatten.
apply member_app_right.
assumption.
intros.
eauto.
cut (Some v' = Some v).
congruence.
eapply trans_equal.
eassumption.
eapply trans_equal.
2 : eassumption.
eapply Hinv.
eapply Hpl.
eassumption.
eapply member_flatten_intro.
eapply member_head.
auto.
Qed.

Corollary mark_all_roots_final_gc_state : forall ap' m p,
Loop.genloop_prop mark_all_roots_body (make_mark_all_roots_param (memory_rd mp) m) ap' ->
marksweep_invariants m mp up gp -> mark_abstraction m mp up gp p ->
marksweep_invariants (mark_all_roots_mem ap') mp up gp.
Proof.
intros.
eapply mark_all_roots_final_gc_state_0.
eassumption.
eapply used_roots_hyp.
eauto.
assumption.
eassumption.
intros.
replace (used_rootpos up) with pl.
assumption.
eapply root_position_list_func.
eassumption.
eapply used_rootpos_hyp; eauto.
trivial.
simpl.
trivial.
simpl.
trivial.
Qed.

Lemma mark_list_post_param_2_app : forall l1 p l2,
mark_list_post_param_2 p (l1 ++ l2) = mark_list_post_param_2 (mark_list_post_param_2 p l1) l2.
Proof.
induction l1; simpl.
 trivial.
intros.
apply IHl1.
Qed.

Lemma mark_all_roots_final_state_0 : forall ap ap',
Loop.genloop_prop mark_all_roots_body ap ap' ->
forall l m v p, all_roots m v l ->
marksweep_invariants m mp up gp -> mark_abstraction m mp up gp p ->
(forall pl, root_position_list m v pl -> forall i, member i (flatten pl) -> member i (flatten (used_rootpos up))) ->
(forall s, member s l -> member s (used_roots up)) ->
mark_all_roots_mem ap = m ->
mark_all_roots_root ap = v ->
mark_abstraction (mark_all_roots_mem ap') mp up gp
(mark_list_post_param_2 p (flatten l))
.
Proof.
induction 1.
 inversion H.
 subst.
 generalize H0.
 unfold mark_all_roots_body_before.
 destruct (mark_all_roots_root a); try (intros; discriminate).
 destruct (eq i zero); try (intros; discriminate). 
 injection 1; intros; subst.
 inversion H4.
 subst.
 simpl.
 assumption.
inversion H. 
subst.
generalize H1.
unfold mark_all_roots_body_before.
case_eq (mark_all_roots_root a); try (intros; discriminate).
 intros i ?.
 destruct (eq i zero); intros; discriminate.
intros b i Hbi.
case_eq (
 load Mint32 (mark_all_roots_mem a) b
       (signed (add i four))
); try (intros; discriminate).
destruct v; try (intros; discriminate).
intros Hval.
injection 1.
intros ? ? l m v p Hl Hgc Habs Hpl Hs ? ?; subst.
clear H4.
inversion Hl.
subst.
generalize (all_roots_desc_root_position_list (all_roots_describes Hl)).
intros [l1 Hl1].
inversion Hl1.
subst.
replace n0 with n in *; [|congruence].
replace v'0 with v' in *; [|congruence].
assert (
   forall pl : list (block * int),
   root_list_position_list b n (add (add i four) four) pl ->
   forall j : block * int,
   member j pl -> member j (flatten (used_rootpos up))
).
 intros pl0 Hpl0.
 replace pl0 with l in *.
 intros.
 eapply Hpl.
 eassumption.
 eapply member_flatten_intro.
 eapply member_head.
 auto.
 eapply root_list_position_list_func.
 eassumption.
 assumption.
assert (
 forall s : option (block * int),
 member s l0 -> member s (flatten (used_roots up))
).
 intros.
 eapply member_flatten_intro.
 2 : eassumption.
 eapply Hs.
 auto.
simpl in H3.
simpl in H2.
replace i0 with n in *; [ | congruence ].
assert (marksweep_invariants (mark_root_list_mem rp''0) mp up gp).
 eapply mark_root_list_final_gc_state; eassumption.
assert (mark_abstraction (mark_root_list_mem rp''0) mp up gp (mark_list_post_param_2 p l0)).
 eapply mark_root_list_final_state; eassumption.
generalize H3.
unfold mark_all_roots_body_after.
simpl.
case_eq (
 load Mint32 (mark_root_list_mem rp''0) b (signed i) 
) ; try (intros; discriminate).
injection 2. 
clear H19.
intros; subst.
inversion Hgc.
inversion marksweep_gc_inv0.
inversion gc_used_hyp0.
inversion H15.
inversion marksweep_gc_inv1.
inversion gc_used_hyp1.
generalize (root_position_list_values_invar used_roots_hyp used_rootpos_hyp used_roots_hyp0 used_rootpos_hyp0).
intros Hinv.
replace v with v' in *.
rewrite mark_list_post_param_2_app.
eapply IHgenloop_prop.
7 : simpl; reflexivity.
6 : simpl; reflexivity.
eapply all_roots_invar.
 eassumption.
 eassumption.
 intros.
 eapply Hinv.
 eapply Hpl.
 eassumption.
 unfold flatten.
 apply member_app_right.
 assumption.
assumption.
eassumption.
intros.
replace pl with l'0 in *.
eapply Hpl.
eassumption.
unfold flatten.
fold flatten.
apply member_app_right.
assumption.
symmetry.
eapply root_position_list_func.
eassumption.
eapply root_position_list_invar.
eassumption.
intros.
eapply Hinv.
eapply Hpl.
eassumption.
unfold flatten.
fold flatten.
apply member_app_right.
assumption.
intros.
eauto.
cut (Some v' = Some v).
congruence.
eapply trans_equal.
eassumption.
eapply trans_equal.
2 : eassumption.
eapply Hinv.
eapply Hpl.
eassumption.
eapply member_flatten_intro.
eapply member_head.
auto.
Qed.


Corollary mark_all_roots_final_state : forall ap' m p,
Loop.genloop_prop mark_all_roots_body (make_mark_all_roots_param (memory_rd mp) m) ap' ->
marksweep_invariants m mp up gp -> mark_abstraction m mp up gp p ->
mark_abstraction (mark_all_roots_mem ap') mp up gp
(mark_list_post_param_2 p (flatten (used_roots up)))
.
Proof.
intros.
eapply mark_all_roots_final_state_0.
eassumption.
eapply used_roots_hyp.
eauto.
assumption.
eassumption.
intros.
replace (used_rootpos up) with pl.
assumption.
eapply root_position_list_func.
eassumption.
eapply used_rootpos_hyp; eauto.
trivial.
trivial.
trivial.
Qed.

End Mark_all_roots.

End Gc_mark_body.

Variable up : used_abstraction_param.
Hypothesis up_extra_zero_true : used_extra_zero up = true.

Variable m : mem.
Hypothesis Hm : marksweep_invariants m mp up gp.

Hypothesis gray_cache_offset_valid : valid_access m Mint32 gray_cache_offset_block 0.
Hypothesis gray_cache_overflow_valid : valid_access m Mint32 gray_cache_overflow_block 0.

Definition m2_ex :
{m2 : _ & {m1 : _ |
Some m1 = store Mint32 m gray_cache_offset_block 0 (Vint zero) /\
Some m2 = store Mint32 m1 gray_cache_overflow_block 0 (Vint zero)
}}.
Proof.
case_eq (store Mint32 m gray_cache_offset_block 0 (Vint zero)).
intros m1 Hm1.
case_eq (store Mint32 m1 gray_cache_overflow_block 0 (Vint zero)).
intros m2 Hm2.
repeat esplit.
eauto.
intro Habs.
apply False_rect.
generalize (store_valid_access_1 _ _ _ _ _ _ Hm1 _ _ _ gray_cache_overflow_valid).
intro Hm1valid.
generalize (valid_access_store _ _ _ _ (Vint zero) Hm1valid).
intros; invall; congruence.
intro Habs.
apply False_rect.
generalize (valid_access_store _ _ _ _ (Vint zero) gray_cache_offset_valid).
intros; invall; congruence.
Defined.

Let m1 := let (_, H) := m2_ex in let (m1, _) := H in m1.

Let m2 := let (m2, _) := m2_ex in m2.

Let Hm1 : Some m1 = store Mint32 m gray_cache_offset_block 0 (Vint zero).
Proof.
destruct m2_ex.
destruct s.
invall.
assumption.
Qed.

Let Hm2 : Some m2 = store Mint32 m1 gray_cache_overflow_block 0 (Vint zero).
Proof.
destruct m2_ex.
destruct s.
invall.
assumption.
Qed.

Lemma m2_gray_cache_offset_block :
load Mint32 m2 gray_cache_offset_block 0 = Some (Vint zero).
Proof.
symmetry in Hm2.
rewrite (load_store_other _ _ _ _ _ _ Hm2).
symmetry in Hm1.
apply (load_store_same _ _ _ _ _ _ Hm1).
auto.
Qed.

Lemma m2_gray_cache_overflow_block :
load Mint32 m2 gray_cache_overflow_block 0 = Some (Vint zero).
Proof.
symmetry in Hm2.
apply (load_store_same _ _ _ _ _ _ Hm2).
Qed.

Lemma m2_other : forall b c i, b <> gray_cache_offset_block -> b <> gray_cache_overflow_block ->
load c m2 b i = load c m b i.
Proof.
intros.
symmetry in Hm2.
rewrite (load_store_other _ _ _ _ _ _ Hm2).
symmetry in Hm1.
apply (load_store_other _ _ _ _ _ _ Hm1).
auto.
auto.
Qed.

Lemma m2_initial_gc_state : marksweep_invariants m2 mp up gp.
Proof.
inversion Hm.
inversion marksweep_gc_inv0.
inversion gc_used_hyp0.
eapply marksweep_invariants_intro; try eassumption.
eapply gc_invariants_intro; try eassumption.
rewrite m2_other; auto.
rewrite m2_other; auto.
eapply used_abstraction_intro; try eassumption.
eapply block_description_ext_heap_zone.
eassumption.
intros.
symmetry.
eapply m2_other.
auto.
auto.
intros i ? v.
rewrite m2_other.
genclear v.
genclear H.
genclear i.
assumption.
auto.
auto.
intros i ? v.
rewrite m2_other.
genclear v.
genclear H.
genclear i.
assumption.
auto.
auto.
intros ? i ? v.
rewrite m2_other.
genclear v.
genclear H0.
genclear i.
genclear H.
assumption.
auto.
auto.
intros.
rewrite m2_other.
eauto.
auto.
auto.
intros.
eapply pointer_list_block_invar.
eassumption.
intros b0 Hb0.
rewrite m2_other.
eapply ex_set_prop.
eapply block_header.
eassumption.
assumption.
auto.
auto.
intros b0 Hb0.
rewrite m2_other.
intros; congruence.
auto.
auto.
intros b0 Hb0.
rewrite m2_other.
intros; congruence.
auto.
auto.
intros.
symmetry.
apply m2_other.
auto.
auto.
auto.
auto.
eapply root_position_list_invar.
eassumption.
intros b i Hbi.
symmetry.
apply m2_other.
eauto.
eauto.
eapply all_roots_invar.
eassumption.
eassumption.
intros b i Hbi.
symmetry.
apply m2_other.
eauto.
eauto.
eapply store_valid_block_1.
eauto.
eapply store_valid_block_1.
eauto.
assumption.
rewrite m2_other.
assumption.
auto.
auto.
eapply store_valid_block_1.
eauto.
eapply store_valid_block_1.
eauto.
assumption.
rewrite (low_bound_store _ _ _ _ _ _ (sym_equal Hm2)).
rewrite (low_bound_store _ _ _ _ _ _ (sym_equal Hm1)).
assumption.
rewrite (high_bound_store _ _ _ _ _ _ (sym_equal Hm2)).
rewrite (high_bound_store _ _ _ _ _ _ (sym_equal Hm1)).
assumption.
Qed.

Let p := make_mark_abstraction_param
 false zero (fun _ => Mark_abstract.White) nil.

Lemma m2_initial_state : mark_abstraction m2 mp up gp p.
Proof.
inversion Hm.
inversion marksweep_gc_inv0.
inversion gc_used_hyp0.
unfold p.
eapply mark_abstraction_intro; simpl; try trivial.
symmetry.
apply m2_gray_cache_overflow_block.
symmetry.
apply m2_gray_cache_offset_block.
intros; discriminate.
intros b Hb v Hv.
rewrite m2_other in Hv.
generalize (used_extra_zero_hyp up_extra_zero_true _ Hb _ Hv).
intro Habs.
rewrite Habs.
inversion 1.
auto.
auto.
intros; discriminate.
intros b Hb v Hv.
rewrite m2_other in Hv.
generalize (used_extra_zero_hyp up_extra_zero_true _ Hb _ Hv).
intro Habs.
rewrite Habs.
inversion 1.
auto.
auto.
intros b Hb _ v Hv.
eapply used_extra_zero_hyp.
assumption.
eassumption.
eapply trans_equal.
eassumption.
apply m2_other.
auto.
auto.
eapply pointer_list_end.
trivial.
inversion 1.
inversion 1.
inversion 1.
inversion 1.
discriminate 1.
Qed.

Definition p'_exists : {p' : _ | Mark_abstract.gc_mark_prop (used_valid mp up) eq_optptr (first_gray up) marksweep_cache_is_full marksweep_cache_full_push marksweep_cache_full_pop (used_children up) (used_raw up) (flatten (used_roots up)) zero
  (marksweep_col p') (gray_cache_overflow_bool p') (marksweep_cache p') (gray_cache_offset_value p')}.
Proof.
assert (
  exists lA, forall a, used_valid mp up a = true -> member a lA
) as HlA.
exists (List.map (fun i => Some (memory_heap mp, i)) (used_blocklist up)).
intros a Ha.
generalize (Hvalid_bool_prop Ha).
intros [i [? Hi]].
subst.
change (Some (memory_heap mp, i)) with ((fun i0 => Some (memory_heap mp, i0)) i).
apply member_map.
assumption.
generalize (Mark_abstract_finite.gc_mark_finite
  eq_optptr
  (@Hfirst_gray_some up)
  marksweep_cache_is_full
  marksweep_cache_full_push
  marksweep_cache_full_pop
  (used_children up)
  (used_raw up)
  (flatten (used_roots up))
  HlA
  zero
).
intros [col [overflow [cache [cache_full H]]]].  
exists (make_mark_abstraction_param overflow cache_full col cache).
simpl.
assumption.
Defined.

Let p' := let (p', _) := p'_exists in p'.

Let Hp' : Mark_abstract.gc_mark_prop (used_valid mp up) eq_optptr (first_gray up) marksweep_cache_is_full marksweep_cache_full_push marksweep_cache_full_pop (used_children up) (used_raw up) (flatten (used_roots up)) zero
  (marksweep_col p') (gray_cache_overflow_bool p') (marksweep_cache p') (gray_cache_offset_value p').
Proof.
destruct p'_exists.
assumption.
Qed.

Let up0 :=
  (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))
.

Lemma Hup0 : used_extra_zero up0 = false.
Proof.
reflexivity.
Qed.

Lemma m2_initial_gc_state0 :
  marksweep_invariants m2 mp up0 gp.
Proof.
generalize m2_initial_gc_state.
inversion 1.
inversion marksweep_gc_inv0.
eapply marksweep_invariants_intro; try eassumption.
eapply gc_invariants_intro; try eassumption.
unfold up0.
eapply used_abstraction_used_extra_zero_weak.
assumption.
Qed.

Lemma m2_initial_state0 :
  mark_abstraction m2 mp up0 gp p.
Proof.
generalize m2_initial_state.
inversion 1.
unfold up0.
eapply mark_abstraction_intro; simpl; try eassumption.
Qed.

Lemma m3_exists_0 : exists m3 : _,
  gc_mark_body (memory_heap mp) (memory_hs mp) (memory_he mp) m2 (memory_rd mp) m3 /\
  marksweep_invariants m3 mp up0 gp /\
  mark_abstraction m3 mp up0 gp p'
.
Proof.
inversion Hp'.
generalize (mark_all_roots_terminates Hup0 m2_initial_gc_state0 m2_initial_state0).
intros [p2 Hp2].
generalize (mark_all_roots_final_gc_state Hup0 Hp2 m2_initial_gc_state0 m2_initial_state0).
intros Hp2inv.
generalize (mark_all_roots_final_state Hup0 Hp2 m2_initial_gc_state0 m2_initial_state0).
intros Hp2abstr.
generalize (Mark_abstract.mark_gray_body_loop_complete H0).
intro Hloop.
var (mark_list_post_param_2 up0 p (flatten (used_roots up0))).
generalize H1.
rewrite <- mark_list_post_param_equiv.
unfold mark_list_post_param.
simpl.
change (used_valid mp up0) with (used_valid mp up).
change (used_raw up0) with (used_raw up).
rewrite <- H.
intro.
subst.
rewrite <- H2 in Hp2abstr.
generalize (mark_gray_exists_cond
  Hup0 
  Hloop
  Hp2inv
  Hp2abstr
  (refl_equal _)
).
intros [m' Hm'].
generalize (mark_gray_final_gc_state Hup0 Hm' Hp2inv Hp2abstr).
intros Hm'gc.
generalize (mark_gray_final_state Hup0 Hm' Hp2inv Hp2abstr H0).
intros Hm'abstr.
exists m'.
split.
2 : auto.
unfold gc_mark_body.
exists p2.
split.
assumption.
eapply (Loop.genloop_implies (@mark_gray_body_2_is_body (memory_heap mp) (memory_hs mp) (memory_he mp))).
assumption.
Qed.

Lemma m3_exists : { m3 : _ |
  gc_mark_body (memory_heap mp) (memory_hs mp) (memory_he mp) m2 (memory_rd mp) m3
}.
Proof.
apply gc_mark_body_dec.
generalize m3_exists_0.
intros.
invall.
esplit.
eassumption.
Defined.

Let m3 := let (m3, _) := m3_exists in m3.

Let Hm3 :   gc_mark_body (memory_heap mp) (memory_hs mp) (memory_he mp) m2 (memory_rd mp) m3.
Proof.
destruct m3_exists.
assumption.
Qed.

Lemma Hm3gc :   marksweep_invariants m3 mp up0 gp.
Proof.
generalize (m3_exists_0).
intros.
invall.
generalize (gc_mark_body_func Hm3 H).
intros; congruence.
Qed.


Lemma Hm3abs :     mark_abstraction m3 mp up0 gp p'.
Proof.
generalize (m3_exists_0).
intros.
invall.
generalize (gc_mark_body_func Hm3 H).
intros; congruence.
Qed.

Lemma m3_final : gc_mark (memory_heap mp) (memory_hs mp) (memory_he mp) m (memory_rd mp) m3.
unfold gc_mark.
exists m1.
split.
assumption.
exists m2.
split.
assumption.
assumption.
Qed.

Theorem m3_used_dec : forall i, (* member i (used_blocklist up) -> *)
{Memory_abstract.used (used_valid mp up) (flatten (used_roots up)) (used_children up) (used_raw up) i} +
{Memory_abstract.used (used_valid mp up) (flatten (used_roots up)) (used_children up) (used_raw up) i -> False} .
Proof.
intros.
eapply (Mark_abstract.used_excluded_middle (eq_A_dec := eq_optptr) (@Hfirst_gray_some up) (@Hfirst_gray_none up)).
eapply Mark_abstract.gc_mark_prop_term.
eassumption.
Defined.

Theorem m3_used_black : forall i, member i (used_blocklist up) ->
Memory_abstract.used (used_valid mp up) (flatten (used_roots up)) (used_children up) (used_raw up) (Some (memory_heap mp, i)) ->
forall v, Some (Vint v) = load Mint32 m3 (memory_heap mp) (signed (sub i four)) ->
  Extra_header v = COLOR_BLACK.
Proof.
intros.
eapply col_black_a_c.
 eexact Hm3abs.
 eexact H.
eapply (Mark_abstract.gc_mark_used_black (eq_A_dec := eq_optptr) (@Hfirst_gray_some up) (@Hfirst_gray_none up)).
 eassumption.
 assumption.
assumption.
Qed.

Theorem m3_not_used_white : forall i, member i (used_blocklist up) ->
(Memory_abstract.used (used_valid mp up) (flatten (used_roots up)) (used_children up) (used_raw up) (Some (memory_heap mp, i)) -> False) ->
forall v, Some (Vint v) = load Mint32 m3 (memory_heap mp) (signed (sub i four)) ->
  Extra_header v = COLOR_WHITE.
Proof.
intros.
eapply col_white_a_c.
 eexact Hm3abs.
 eexact H.
eapply (Mark_abstract.gc_mark_not_used_white (eq_A_dec := eq_optptr) (@Hfirst_gray_some up) (@Hfirst_gray_none up)).
 eassumption.
 assumption.
assumption.
Qed.

Theorem m3_used :
forall i, member i (used_blocklist up) ->
Memory_abstract.used (used_valid mp up) (flatten (used_roots up)) (used_children up) (used_raw up) (Some (memory_heap mp, i)) ->
Some (Vint (or COLOR_BLACK (or (used_sizes up i) (used_kinds up i)))) = load Mint32 m3 (memory_heap mp) (signed (sub i four)).
Proof.
intros i Hi Hused.
generalize Hm3gc.
inversion 1.
inversion marksweep_gc_inv0.
inversion gc_used_hyp0.
generalize (block_header used_heap_hyp Hi).
intros [v Hv].
rewrite <- Hv.
f_equal.
f_equal.
rewrite <- (m3_used_black Hi Hused Hv).
change (used_sizes up) with (used_sizes up0).
change (used_kinds up) with (used_kinds up0).
rewrite <- (used_sizes_hyp _ Hi _ Hv).
rewrite <- (used_kinds_hyp _ Hi _ Hv).
symmetry.
apply header_decomp.
Qed.

Theorem m3_not_used :
forall i, member i (used_blocklist up) ->
(Memory_abstract.used (used_valid mp up) (flatten (used_roots up)) (used_children up) (used_raw up) (Some (memory_heap mp, i)) -> False) ->
Some (Vint (or COLOR_WHITE (or (used_sizes up i) (used_kinds up i)))) = load Mint32 m3 (memory_heap mp) (signed (sub i four)).
Proof.
intros i Hi Hused.
generalize Hm3gc.
inversion 1.
inversion marksweep_gc_inv0.
inversion gc_used_hyp0.
generalize (block_header used_heap_hyp Hi).
intros [v Hv].
rewrite <- Hv.
f_equal.
f_equal.
rewrite <- (m3_not_used_white Hi Hused Hv).
change (used_sizes up) with (used_sizes up0).
change (used_kinds up) with (used_kinds up0).
rewrite <- (used_sizes_hyp _ Hi _ Hv).
rewrite <- (used_kinds_hyp _ Hi _ Hv).
symmetry.
apply header_decomp.
Qed.

End Mark.

Section Sweep.



Variable heap : block.
Variables hs he : int.

Record sweep_invariants_param : Set := make_sweep_invariants_param { 
  sweep_invar_blocklist_before : list int;
  sweep_invar_blocklist_after : list int
}  .


Record sweep_invariants (p : sweep_loop_body_param) (ip : sweep_invariants_param) : Prop := sweep_invariants_intro {
  sweep_last_nonempty_offset_defined_valid_access :
   valid_access (sweep_mem p) Mint32 (sweep_last_nonempty_block p) (signed (sweep_last_nonempty_offset p));
  sweep_last_nonempty_lt_empty :
    sweep_last_nonempty_block p = heap ->
    sweep_prev_is_free p = true ->
    sweep_last_is_empty p = true ->
    cmp Clt (sweep_last_nonempty_offset p) (sub (sweep_last_offset p) four) = true;
  sweep_last_nonempty_offset_hyp :
   sweep_last_nonempty_block p = heap ->
   sweep_scan_ptr_offset p <> he ->
   cmp Clt (sweep_last_nonempty_offset p) (sweep_scan_ptr_offset p) = true;
  sweep_last_nonempty_modulo_four :
    sweep_last_nonempty_block p = heap ->
    modulo_four (sweep_last_nonempty_offset p) (sweep_scan_ptr_offset p);
  sweep_prev_empty_hyp :
   sweep_prev_is_free p = true ->
   sweep_last_is_empty p = true ->
   sweep_last_offset p = sweep_scan_ptr_offset p;
  sweep_prev_nonempty_offset_hyp :
    sweep_prev_is_free p = true ->
    sweep_last_is_empty p = false ->
    sweep_last_offset p = sweep_last_nonempty_offset p;
  sweep_prev_nonempty_block_hyp :
    sweep_prev_is_free p = true ->
    sweep_last_is_empty p = false ->
    sweep_last_nonempty_block p = heap;
  sweep_last_nonempty_non_empty :
    sweep_last_nonempty_block p = heap ->
    forall v, Some (Vint v) = load Mint32 (sweep_mem p) heap (signed (sub (sweep_last_nonempty_offset p) four)) ->
      Size_header v <> zero;
  sweep_last_empty_empty :
    sweep_last_is_empty p = true ->
    Some (Vint zero) = load Mint32 (sweep_mem p) heap (signed (sub (sweep_last_offset p) four));

  sweep_invar_blocklist_hyp_1 : sweep_prev_is_free p = false -> block_description_from_to (sweep_mem p) heap hs he (sweep_invar_blocklist_before ip ++ sweep_invar_blocklist_after ip);
  sweep_invar_blocklist_hyp_2 : sweep_prev_is_free p = true -> block_description_from_to (sweep_mem p) heap hs he (sweep_invar_blocklist_before ip ++ (sweep_last_nonempty_offset p) :: sweep_invar_blocklist_after ip);
  sweep_invar_blocklist_end : block_description_from_to (sweep_mem p) heap (sweep_scan_ptr_offset p) he (sweep_invar_blocklist_after ip)
(*  sweep_invar_blocklist_junction : hs = sweep_scan_ptr_offset p \/  hs <> he /\ cmp Cle (sub (sweep_scan_ptr_offset p) one) (sub he one) = true *)
}.

Hint Constructors sweep_invariants.

(*
Lemma sweep_invar_blocklist_hyp_1 p ip : sweep_invariants p ip ->
sweep_prev_is_free p = false ->
block_description_from_to (sweep_mem p) heap hs he (sweep_invar_blocklist_before ip ++ sweep_invar_blocklist_after ip).
Proof.
inversion 1; intros; eapply block_description_merge; eauto.
Qed.

Lemma sweep_invar_blocklist_hyp_2 p ip : sweep_invariants p ip ->
sweep_prev_is_free p = true ->
block_description_from_to (sweep_mem p) heap hs he (sweep_invar_blocklist_before ip ++ sweep_last_nonempty_offset p :: sweep_invar_blocklist_after ip).
Proof.
inversion 1; intros; eapply block_description_merge.
 eauto.
pattern (sweep_last_nonempty_offset p) at -1.
rewrite <- (sub_add_id (sweep_last_nonempty_offset p) four).
eapply block_description_block.
 
; eauto.
Qed.
*)

(*
Section Properties.

Opaque cmp.

Theorem sweep_loop_body_invar : forall p ip, sweep_invariants p ip ->
forall b p', (b, Some p') = sweep_loop_body heap he (Some p) ->
exists ip', sweep_invariants p' ip' /\ (b = true -> length (sweep_invar_blocklist_after ip) = S (length (sweep_invar_blocklist_after ip'))).
Proof.
inversion 1.
intros b p' Hp'.
generalize Hp'.
unfold sweep_loop_body.
case_eq (eq (sweep_scan_ptr_offset p) he).
 injection 2; intros; subst; eapply ex_intro; split; eauto.
 intros; discriminate.
intro Hnend_bool.
generalize (neq_bool_neq_prop Hnend_bool).
intro Hnend.
inversion sweep_invar_blocklist_end0.
 contradiction.
subst.
case_eq (load Mint32 (sweep_mem p) heap (signed (sweep_scan_ptr_offset p))); try (intros; discriminate).
destruct v0; try (intros; discriminate).
intros Hi.
case_eq (eq (Color_header i) COLOR_WHITE).
 intro Hwhite_bool.
 generalize (eq_bool_eq_prop Hwhite_bool).
 intro Hwhite.
 case_eq (sweep_prev_is_free p).
  intro Hprev_is_free.
  rewrite Hprev_is_free in *.
  rewrite <- (sub_add_id (sweep_last_nonempty_offset p) four) in sweep_invar_blocklist_hyp_4.
  generalize (block_description_split_strong (sweep_invar_blocklist_hyp_4 (refl_equal _)) (refl_equal _)).
  intro.
  invall.
  case_eq (load Mint32 (sweep_mem p) heap (signed (sub (sweep_last_offset p) four))); try (intros; discriminate).
  destruct v0; try (intros; discriminate).
  intros Hi0.
  case_eq (store Mint32 (sweep_mem p) heap (signed (sub (sweep_last_offset p) four)) (Vint (add i0 (add (Size_header i) four)))); try (intros; discriminate).
  intros m1 Hm1.
  case_eq (sweep_last_is_empty p).
   intro Hlast_empty.
   rewrite Hlast_empty in *.
   generalize  (sweep_prev_empty_hyp0 (refl_equal _) (refl_equal _)).
   intro sweep_prev_empty_hyp1. 
   rewrite sweep_prev_empty_hyp1 in *.
   case_eq (store Mint32 m1 (sweep_last_nonempty_block p) (signed (sweep_last_nonempty_offset p)) (Vptr heap (sweep_scan_ptr_offset p)));
    try (intros; discriminate).
   intros m' Hm'.
   injection 1; intros; subst.
   exists (make_sweep_invariants_param (sweep_invar_blocklist_before ip) l).
   split.
    apply sweep_invariants_intro.
          simpl.
         eapply store_valid_access_1.
          eassumption.
         eapply store_valid_access_1.
          eassumption.
         eapply load_valid_access.
         eauto.
        simpl.
        intros; discriminate.
        simpl.
        intros _ Hdiff.
        inversion H9.
         subst.
         rewrite add_assoc in Hdiff.
         congruence.
        subst.
        eapply int_le_lt_trans.
         eassumption.
        change four with (add three one).
        rewrite <- add_assoc.
        rewrite <- add_assoc.
        eapply int_le_lt_trans.
         eassumption.
        replace i with v in *; [ | congruence].
        eapply lt_step.
         eapply lt_is_le_neq.
          eassumption.
         rewrite <- Hcalc.
         intro Habs.
         destruct H8.
         rewrite <- (sub_add_id he four).
         f_equal.
         apply add_reg_r with three.
         assumption.
        simpl.
        rewrite <- add_assoc.
        intros _.
        eapply mod4_trans.
        apply modulo_four_four_divides_add.
        apply four_divides_size_header.
        apply modulo_four_four_divides_add.
        apply four_divides_four.
       simpl. discriminate 2.
      simpl. trivial.
     simpl. trivial.
     simpl. intros _ v0 Hv0.
     assert (i0 = zero).
      generalize (sweep_last_empty_empty0 (refl_equal _)).
      intro.
      congruence.
     subst.
     rewrite add_commut in Hm1.
     rewrite add_zero in Hm1.
     assert (v0 = add (Size_header i) four).
      destruct (zeq (sweep_last_nonempty_block p) heap).
       subst.
       rewrite <- (get_set_int32_indep (sym_equal Hm')) in Hv0.
       rewrite (load_store_same _ _ _ _ _ _ Hm1) in Hv0.
       simpl in Hv0.
       injection Hv0.
       auto.
       intro Habs.
       destruct (int_lt_irrefl_0 (sweep_last_nonempty_lt_empty0 (refl_equal _) (refl_equal _) (refl_equal _))).
       rewrite <- sweep_prev_empty_hyp1.
       rewrite sweep_prev_empty_hyp1.
       trivial.
      eapply mod4_trans.
      eapply sweep_last_nonempty_modulo_four0.
      trivial.
      apply mod4_sym.
      eapply modulo_four_four_divides_sub.
      apply four_divides_four; auto.
     rewrite (load_store_other _ _ _ _ _ _ Hm') in Hv0.
     rewrite (load_store_same _ _ _ _ _ _ Hm1) in Hv0.
     simpl in Hv0.
     injection Hv0.
     auto.
     left; auto.
     subst.
    

Focus 2.
simpl.
discriminate 1.

Focus 2.
simpl.
discriminate 1.

Focus 2.
simpl.
intros _.
eapply block_description_merge.
      eapply block_description_samesize_inv.
        eassumption.
       intros b Hb.
       destruct (block_header H7 Hb) as [h Hh].
       exists h.
       rewrite Hh.
       symmetry.
       destruct (zeq (sweep_last_nonempty_block p) heap).
        rewrite e in *.
        eapply trans_equal.
        symmetry.
        eapply get_set_int32_indep.
         eauto.
         intro Habs.
         
         
       
         

        
         (* valid access on last offset *) assumption.

Section Case_loop.

Theorem sweep_loop_body_block_description_invar : forall l,
block_description_from_to (sweep_mem p) sweep_scan_block (sweep_scan_ptr_offset p) sweep_scan_end_offset l ->
sweep_loop_body sweep_scan_block sweep_scan_end_offset (Some p) = (true, Some p') ->
exists a, exists q, l = a :: q /\
block_description_from_to (sweep_mem p') sweep_scan_block (sweep_scan_ptr_offset p') sweep_scan_end_offset q.
Admitted.

End Case_loop.

End Properties.

Section Termination.

Theorem sweep_loop_body_terminates : forall l p,
  block_description_from_to (sweep_mem p) sweep_scan_block (sweep_scan_ptr_offset p) sweep_scan_end_offset l ->
  (eq (sweep_freelist_init p) zero = false -> sweep_last_free_block_block p = sweep_scan_block) -> 
  (eq (sweep_freelist_init p) zero = false -> exists v, Some (Vint v) = load Mint32 (sweep_mem p) sweep_scan_block (signed (sub (sweep_last_free_block_offset p) four))) -> 
  Loop.loop_term (sweep_loop_body sweep_scan_block sweep_scan_end_offset) (Some p).
Proof.
induction l.
 intro p.
 inversion 1.
 subst.
 intros.
 eapply Loop.loop_term_interrupt.
 unfold sweep_loop_body.
 case_eq (eq (sweep_scan_ptr_offset p) (sweep_scan_ptr_offset p)).
  intro ; reflexivity.
 intro Hneq_bool.
 destruct (neq_bool_neq_prop Hneq_bool).
 trivial.
intros p Hp Hlfb Hlfb_ex.
inversion Hp.
subst.
case_eq (eq (sweep_scan_ptr_offset p) sweep_scan_end_offset).
 intro Habs.
 generalize (eq_bool_eq_prop Habs).
 intros; congruence.
intro H_neq_bool.
case_eq (sweep_loop_body sweep_scan_block sweep_scan_end_offset (Some p)).
intros bo op Hbop.
generalize Hbop.
intro Hbop2.
unfold sweep_loop_body in Hbop2.
genclear Hbop2.
rewrite H_neq_bool.
rewrite <- H2.
case_eq (eq (Color_header v) COLOR_WHITE).
 intro Hwhite_bool.
 case_eq (
    if eq (sweep_freelist_init p) zero
      then false
      else eq (sweep_scan_ptr_offset p) (sweep_end_last_free_block_offset p)
 ).
  case_eq (eq (sweep_freelist_init p) zero) ; try (intros; discriminate).
  intros eq_sweep_init eq_is_last_free_block.
  generalize (Hlfb eq_sweep_init).
  intro His_scan_block.
  rewrite His_scan_block.
  generalize (Hlfb_ex eq_sweep_init).
  intros [v' Hv'].
  rewrite <- Hv'.
  case_eq (store Mint32 (sweep_mem p) sweep_scan_block (signed (sub (sweep_last_free_block_offset p) four))
  

 
 Focus 2.
 intro Hnonwhite.
 case_eq (store Mint32 (sweep_mem p) sweep_scan_block (signed (sweep_scan_ptr_offset p)) (Vint (and v (not COLOR_BLACK)))).
  intros m' Hm'.
  refine ((fun Hm'0 : sweep_loop_body sweep_scan_block sweep_scan_end_offset (Some p) = (true, Some _) => _) _).
  Focus 2.
  unfold sweep_loop_body.
  rewrite H_neq_bool.
  rewrite <- H2.
  rewrite Hnonwhite.
  rewrite Hm'.
  reflexivity.
  Focus 2.
  eapply Loop.loop_term_continue.
   eassumption.
   eapply IHl.
  Print Implicit sweep_loop_body_block_description_invar.
   generalize (sweep_loop_body_block_description_invar Hp Hm'0).
   intros [a [q [Hinj Hblock]]]; congruence.


   apply 
   simpl.
   
 auto.

End Termination.
*)

End Sweep.

End Marksweep_theorems.