(** 
 RAMANANANDRO Tahina
 Ecole Normale Superieure
 Paris, France

 The Gallium Project
 Institut National de Recherche en Informatique & Automatique
 Rocquencourt, France

 * Abstract marking algorithm

 The abstract marking algorithm is correct and complete
 whenever it terminates, regardless of the addressing
 space.
*)

Load param.

Require Export Memory_abstract.
Require Export Loop.

(** ** The marking algorithm *)

Section Mark.

Inductive color : Set := | Black | Gray | White.

Variable A : Set.
Variable valid : A -> bool.
Variable eq_A_dec : forall a b : A, {a = b} + {a <> b}.
Variable first_gray : (A -> color) -> option A.
Hypothesis Hfirst_gray_some : forall col a, first_gray col = Some a -> (valid a = true /\ col a = Gray).
Hypothesis Hfirst_gray_none : forall col, first_gray col = None -> forall a : A, valid a = true -> col a = Gray -> False.

Variable B : Set.
Variable cache_is_full : B -> bool.
Variable push : B -> B.
Variable pop : B -> B.

Definition cache_push (a : A) overflow cache cache_full :=
if cache_is_full cache_full
then ((true, cache), cache_full)
else ((overflow, a::cache), push cache_full).

Definition set_color (a : A) (c : color) (col : A -> color) :=
(fun x => if eq_A_dec x a then c else col x)
.

Variable (children : A -> list A) .
Variable raw : A -> bool.

Definition mark_block
 (col : A -> color) (overflow : bool) (cache : list A) (cache_full : B)
 (a : A)
:
 (A -> color) * ((bool * list A) * B)
:=
 if valid a then match col a with
 | White =>
   if raw a
   then (set_color a Black col, ((overflow, cache), cache_full))
   else (set_color a Gray col, cache_push a overflow cache cache_full)
 | _ => (col, ((overflow, cache), cache_full))
 end else (col, ((overflow, cache), cache_full))
.

Definition cache_pop
 (col : A -> color) (overflow : bool) (cache : list A) (cache_full : B)
:
 ((option A * list A) * B)
:=
 match cache with
 | nil =>
   if overflow
   then match first_gray col with
   | Some a => ((Some a, cache), cache_full)
   | _ => ((None, cache), cache_full)
   end
   else ((None, cache), cache_full)
 | cons a m => ((Some a, m), pop cache_full)
 end
.

Fixpoint mark_list
 (col : A -> color) (overflow : bool) (cache : list A) (cache_full : B)
 (l : list A) {struct l}
:
 (A -> color) * ((bool * list A) * B)
:=
 match l with
 | nil => (col, ((overflow, cache), cache_full))
 | cons a m => 
   match mark_block col overflow cache cache_full a with
   | (col2, ((overflow2, cache2), cache_full_2)) => mark_list col2 overflow2 cache2 cache_full_2 m
   end
 end
.

Lemma mark_list_app : forall l1 l2 col overflow cache cache_full,
  mark_list col overflow cache cache_full (l1 ++ l2) =
  match mark_list col overflow cache cache_full l1 with
    (col1, ((overflow1, cache1), cache_full_1)) =>
    mark_list col1 overflow1 cache1 cache_full_1 l2
  end.
Proof.
induction l1; simpl.
 auto.
intros.
destruct (mark_block col overflow cache cache_full a).
destruct p.
destruct p.
auto.
Qed.


(*
 
 Mark_gray is a loop that could be written followingly in OCaml :

 let rec mark_gray col overflow cache =
 begin match cache_pop col overflow cache with
 | (Some a, cache1) ->
   begin match
    mark_list (set_color a Black col) overflow cache1 (children a)
   with
   | (col2, (overflow2, ( cache2 ))) ->
     mark_gray col2 overflow2 cache2    
   end
 | (None, cache2) => (col, (overflow, ( cache2 )))
 end

 It defines a loop that does not structurally terminate.
 So we have to induce over an ad-hoc predicate.

*)

Inductive mark_gray_term (col : A -> color) (overflow : bool) (cache : list A) (cache_full : B) : Prop :=
| Mark_gray_base : forall cache1 cache_full_1,
   ((None, cache1), cache_full_1) = cache_pop col overflow cache cache_full ->
   mark_gray_term col overflow cache cache_full
| Mark_gray_call1 : forall a cache1 cache_full_1, 
   ((Some a, cache1), cache_full_1) = cache_pop col overflow cache cache_full ->
   forall col2 overflow2 cache2 cache_full_2,
   (col2, ((overflow2, cache2), cache_full_2)) = mark_list (set_color a Black col) overflow cache1 cache_full_1 (children a) ->
   mark_gray_term col2 overflow2 cache2 cache_full_2 ->
   mark_gray_term col overflow cache cache_full
.

Hint Constructors mark_gray_term.

(*

The Mark_gray loop has to be defined as a predicate to allow easier reasoning
about it, and to prevent the user from having to cope with the Gallina term,
in particular the refined parts given in proof mode.

However, it is not enough, as one still wants to extract the algorithm for
the loop.

*)

Inductive mark_gray_prop : (A -> color) -> bool -> list A -> B -> (A -> color) -> bool -> list A -> B -> Prop :=
| mark_gray_prop_O : forall col overflow cache cache_full cache2 cache_full_2,
  ((None, cache2), cache_full_2) = cache_pop col overflow cache cache_full ->
  mark_gray_prop col overflow cache cache_full col overflow cache2 cache_full_2
| mark_gray_prop_S : forall col overflow cache cache_full a cache1 cache_full_1,
  ((Some a, cache1), cache_full_1) = cache_pop col overflow cache cache_full ->
  forall col2 overflow2 cache2 cache_full_2,
  (col2, ((overflow2, cache2), cache_full_2)) = mark_list (set_color a Black col) overflow cache1 cache_full_1 (children a) ->
  forall col3 overflow3 cache3 cache_full_3,
  mark_gray_prop col2 overflow2 cache2 cache_full_2 col3 overflow3 cache3 cache_full_3 ->
  mark_gray_prop col overflow cache cache_full col3 overflow3 cache3 cache_full_3
.

Hint Constructors mark_gray_prop.

(* It is safe to show that this predicate is functional. *)

Lemma mark_gray_prop_func : forall col overflow cache cache_full col2 overflow2 cache2 cache_full_2,
mark_gray_prop col overflow cache cache_full col2 overflow2 cache2 cache_full_2 ->
forall col3 overflow3 cache3 cache_full_3,
mark_gray_prop col overflow cache cache_full col3 overflow3 cache3 cache_full_3 ->
col2 = col3 /\ overflow2 = overflow3 /\ cache2 = cache3 /\ cache_full_2 = cache_full_3.

Proof.
intros col overflow cache cache_full col2 overflow2 cache2 cache_full_2 H.
induction H. (* mark_gray_prop *)
 (* case O *)
 intros.
 inversion H0 ; subst. (* mark_gray_prop *)
  (* case O *)
  rewrite <- H in H1.
  injection H1 ; auto.
  (* case S *)
  rewrite <- H in  H1.
  discriminate.
 (* case S *)
 intros.
 inversion H2 ; subst. (* mark_gray_prop *)
  (* case O *)
  rewrite <- H3 in H.
  discriminate.
  (* case S *)
  rewrite <- H3 in H.
  injection H ; intros ; subst.
  rewrite <- H0 in H4.
  injection H4 ; intros ; subst.
  apply IHmark_gray_prop ; auto.
Qed.

(* The following definition is twofold : not only does it provide the algorithm
   for the Mark_gray loop ready for extraction, but it also states that the
   termination predicate suffices to show the existence of "images" for the
   arguments provided in the "functional" predicate. *)


(* The termination condition is necessary *)

Lemma mark_gray_prop_term : forall col overflow cache cache_full col2 overflow2 cache2 cache_full_2,
mark_gray_prop col overflow cache cache_full col2 overflow2 cache2 cache_full_2 ->
mark_gray_term col overflow cache cache_full.

Proof.
induction 1 ; eauto.
Qed.


Section Mark_gray.

Let body k := match k with
| (col, ((overflow, cache), cache_full)) =>
  match cache_pop col overflow cache cache_full with
  | ((Some a, cache1), cache_full_1) =>
    match mark_list (set_color a Black col) overflow cache1 cache_full_1 (children a) with
    | (col2, ((overflow2, cache2), cache_full_2)) =>
      (true, (col2, ((overflow2, cache2), cache_full_2)))
    end
  | ((None, cache1), cache_full_1) => (false, (col, ((overflow, cache1), cache_full_1)))
  end
end.

Definition mark_gray_body := body.

Let loop_correct : forall k k', loop_prop body k k' ->
forall col overflow cache cache_full, k = (col, ((overflow, cache), cache_full)) ->
forall col' overflow' cache' cache_full', k' = (col', ((overflow', cache'), cache_full')) ->
mark_gray_prop col overflow cache cache_full col' overflow' cache' cache_full'.
Proof.
induction 1.
introvars.
intro.
subst.
introvars.
intro.
subst.
genclear H.
unfold body.
case_eq (cache_pop col overflow cache cache_full).
intros [o cache1] cache_full_1 Hcache_pop.
case_eq o.
intros a ?.
subst.
case_eq (mark_list (set_color a Black col) overflow cache1 cache_full_1 (children a)).
intros col2 [[overflow2 cache2] cache_full_2] Hmark_list.
discriminate 1.
intro.
subst.
injection 1; intros; subst.
eauto.
introvars.
intro.
subst.
introvars.
intro.
subst.
genclear H.
unfold body.
case_eq (cache_pop col overflow cache cache_full).
intros [o cache1] cache_full_1 Hcache_pop.
case_eq o.
intros a ?.
subst.
case_eq (mark_list (set_color a Black col) overflow cache1 cache_full_1 (children a)).
intros col2 [[overflow2 cache2] cache_full_2] Hmark_list.
injection 1; intros; subst.
generalize (IHloop_prop _ _ _ _ (refl_equal _)
_ _ _ _ (refl_equal _)).
intro.
eauto.
discriminate 2.
Qed.

Corollary mark_gray_body_loop_correct : forall col overflow cache cache_full col' overflow' cache' cache_full',
loop_prop mark_gray_body (col, ((overflow, cache), cache_full)) (col', ((overflow', cache'), cache_full')) ->
mark_gray_prop col overflow cache cache_full col' overflow' cache' cache_full'.
Proof.
intros.
eapply loop_correct.
 eassumption.
 auto.
 auto.
Qed.

Let loop_terminates : forall col overflow cache cache_full,
mark_gray_term col overflow cache cache_full ->
loop_term body (col, ((overflow, cache), cache_full)).
Proof.
induction 1.
eapply loop_term_interrupt.
unfold body.
rewrite <- H.
reflexivity.
eapply loop_term_continue.
unfold body.
rewrite <- H.
rewrite <- H0.
reflexivity.
assumption.
Qed.

Corollary mark_gray_body_loop_complete : forall col overflow cache cache_full col' overflow' cache' cache_full',
mark_gray_prop col overflow cache cache_full col' overflow' cache' cache_full' ->
loop_prop mark_gray_body (col, ((overflow, cache), cache_full)) (col', ((overflow', cache'), cache_full')).
Proof.
introvars.
intro Hm.
generalize (mark_gray_prop_term Hm).
intro Hterm.
generalize (loop_terminates Hterm).
intros Hterml.
generalize (loop Hterml).
intros [[col'' [[overflow'' cache''] cache_full'']] H''].
generalize (mark_gray_body_loop_correct H'').
intro Hm''.
generalize (mark_gray_prop_func Hm Hm'').
intros; invall; subst;assumption.
Qed.

Definition mark_gray col overflow cache cache_full :
 mark_gray_term col overflow cache cache_full ->
 {col2 : _ & {overflow2 : _ & {cache2 : _ & {cache_full_2 : _ |
  mark_gray_prop col overflow cache cache_full col2 overflow2 cache2 cache_full_2}}}}.

Proof.
introvars.
intro Hmark.
generalize (loop (loop_terminates Hmark)).
intros [ [col2 [[overflow2 cache2] cache_full_2]] Hloop].
exists col2.
exists overflow2.
exists cache2.
exists cache_full_2.
eapply loop_correct; eauto.
Defined.

End Mark_gray.

(* Now we package everything. *)

Variable roots : list A.

Definition gc_mark_term cache_full :=
  forall col2 overflow2 cache2 cache_full_2,
  (col2, ((overflow2, cache2), cache_full_2)) = mark_list (fun _ => White) false nil cache_full roots ->
  mark_gray_term col2 overflow2 cache2 cache_full_2
.

Inductive gc_mark_prop cache_full col3 overflow3 cache3 cache_full_3 : Prop :=
| gc_mark_prop_intro :
  forall col2 overflow2 cache2 cache_full_2,
  (col2, ((overflow2, cache2), cache_full_2)) = mark_list (fun _ => White) false nil cache_full roots ->
  mark_gray_prop col2 overflow2 cache2 cache_full_2 col3 overflow3 cache3 cache_full_3 ->
  @gc_mark_prop cache_full col3 overflow3 cache3 cache_full_3.

Lemma gc_mark_prop_func : forall cache_full col3 overflow3 cache3 cache_full_3 col4 overflow4 cache4 cache_full_4,
gc_mark_prop cache_full col3 overflow3 cache3 cache_full_3 ->
gc_mark_prop cache_full col4 overflow4 cache4 cache_full_4 ->
col3 = col4 /\ overflow3 = overflow4 /\ cache3 = cache4 /\ cache_full_3 = cache_full_4.

Proof.
simple inversion 1.
simple inversion 3.
match goal with [H : context [mark_list] |- _ ] => rewrite <- H end.
injection 1 ; intros ; subst ; eapply mark_gray_prop_func ; eauto.
Qed.

Lemma gc_mark_prop_term : forall cache_full col3 overflow3 cache3 cache_full_3,
gc_mark_prop cache_full col3 overflow3 cache3 cache_full_3 -> gc_mark_term cache_full.

Proof.
inversion 1.
unfold gc_mark_term.
introvars.
match goal with [H : context [mark_list] |- _ ] => rewrite <- H end.
injection 1 ; intros ; subst ;
eapply mark_gray_prop_term ; eauto.
Qed.

Definition gc_mark cache_full : gc_mark_term cache_full -> {col3 : _ & {overflow3 : _ & {cache3 : _ & {cache_full_3 | 
gc_mark_prop cache_full col3 overflow3 cache3 cache_full_3}}}}.

Proof.
intros cache_full H.
refine (
 let ml0 := mark_list _ _ _ _ _ in
 match ml0 as ml return (ml = ml0 -> _) with
 | (_, ((_, _), _)) => fun Heq =>
   match mark_gray (H _ _ _ _ Heq) with
   | (existT col3 (existT overflow3 (existT cache3 (exist cache_full_3 _)))) => _ (* proof_obligation *)
   end
 end (refl_equal _)
).
exists col3.
exists overflow3.
exists cache3.
exists cache_full_3.
eapply gc_mark_prop_intro ; eauto.
Defined.

Section Correctness.

(* The marking algorithm is correct : every accessible item is black *)

(* Whenever an invariant P is kept by mark_block,
   then P is also kept by mark_list. *)

Theorem mark_list_general : forall P : (A -> color) -> bool -> list A -> B -> Prop,
(forall col overflow cache cache_full a col2 overflow2 cache2 cache_full_2,
(col2, ((overflow2, cache2), cache_full_2)) = mark_block col overflow cache cache_full a ->
P col overflow cache cache_full -> P col2 overflow2 cache2 cache_full_2) ->
forall l col1 overflow1 cache1 cache_full_1 col3 overflow3 cache3 cache_full_3,
(col3, ((overflow3, cache3), cache_full_3)) = mark_list col1 overflow1 cache1 cache_full_1 l ->
P col1 overflow1 cache1 cache_full_1 ->
P col3 overflow3 cache3 cache_full_3.

Proof.
intros P HP.
induction l as [ | a] ; simpl. (* list *)
 (* case nil *)
 injection 1 ; intros ; subst ; auto.
 (* case cons *)
 intros col1 overflow1 cache1 cache_full_1.
 case_eq (mark_block col1 overflow1 cache1 cache_full_1 a).
 intros ? [[? ?] ?].
 intros.
 eapply IHl ; eauto.
Qed.

(* Color lemmas *)

Lemma set_color_variant : forall a c col, set_color a c col a = c.

Proof.
intros.
unfold set_color.
destruct (eq_A_dec a a).
 (* case = *)
 trivial.
 (* case <> *)
 contradiction (refl_equal a).
Qed.

Lemma set_color_invariant :
forall a c col x, x <> a -> set_color a c col x = col x.

Proof.
intros.
unfold set_color.
destruct (eq_A_dec x a).
 (* case = *)
 contradiction.
 (* case <> *)
 trivial.
Qed.

(* When the cache is popped, either it was empty, or it is removed one item. *)

Lemma cache_pop_which : forall col overflow cache cache_full cache2 cache_full_2 a,
((Some a, cache2), cache_full_2) = cache_pop col overflow cache cache_full ->
((cache = nil /\ cache2 = nil) \/ cache = a::cache2).

Proof.
introvars.
unfold cache_pop.
destruct cache. (* list *)
 (* case nil *)
 destruct overflow. (* bool *)
  (* case true *)
  case_eq (first_gray col) . (* first_gray *)
   (* case gray *)
   injection 2 ; intros ; subst ; auto.
   (* case no gray *)
   intros ; discriminate.
  (* case false *)
  intros ; discriminate.
 (* case cons *)
 injection 1 ; intros ; subst ; auto.
Qed.

(* The following lemmas prove the canonical invariant :
   no black object points to any white object *)
 
Lemma mark_block_invar :
 forall P col overflow cache cache_full a col2 overflow2 cache2 cache_full_2,
 (col2, ((overflow2, cache2), cache_full_2)) = mark_block col overflow cache cache_full a ->
 (forall s t, P s -> col s = Black -> points_to valid children raw s t -> col t = White -> False) ->
 forall s t, P s -> col2 s = Black -> points_to valid children raw s t -> col2 t = White -> False.

Proof.
unfold mark_block.
introvars.
case_eq (valid a). (* bool *)
intro Hvalid.
case_eq (col a). (* color *)
 (* case Black *)
 injection 2 ; intros ; subst ; eauto.
 (* case Gray *)
 injection 2 ; intros ; subst ; eauto.
 (* case White *)
 case_eq (raw a). (* bool *)
  (* case true *)
  unfold set_color at 1.
  injection 3.
  intros until 4; subst.
  inversion 4 ; subst.
  destruct (eq_A_dec t a).
   (* case = *)
   discriminate 1.
   (* case <> *)
   destruct (eq_A_dec s a).
    (* case = *)
    subst.
    discr.
    (* case <> *)
    eauto.
 (* case false *)
  unfold set_color.
  injection 3 ; intros ; subst.
  destruct (eq_A_dec t a).
   (* case = *)
   discriminate.
   (* case <> *)
   destruct (eq_A_dec s a).
    (* case = *)
    discriminate.
    (* case <> *)
    eauto.
(* case valid = false *)
injection 2; intros; subst; eauto.
Qed.

Lemma mark_list_invar :
 forall P l col overflow cache cache_full col2 overflow2 cache2 cache_full_2,
 (col2, ((overflow2, cache2), cache_full_2)) = mark_list col overflow cache cache_full l ->
 (forall s t, P s -> col s = Black -> points_to valid children raw s t -> col t = White -> False) ->
 forall s t, P s -> col2 s = Black -> points_to valid children raw s t -> col2 t = White -> False.

Proof (fun P => (mark_list_general (mark_block_invar (P := P)))).

(* A *valid* marked block is no longer white. *)

Lemma mark_block_no_white :
forall a,
valid a = true ->
forall col overflow cache cache_full col2 overflow2 cache2 cache_full_2,
(col2, ((overflow2, cache2), cache_full_2)) = mark_block col overflow cache cache_full a ->
col2 a = White -> False.

Proof.
unfold mark_block.
intros a Hvalid col.
case_eq (valid a); intro; try discr.
case_eq (col a). (* color *)
 (* case Black *)
 injection 2 ; intros ; subst ; discr.
 (* case Gray *)
 injection 2 ; intros ; subst ; discr.
 (* case White *)
 destruct (raw a). (* bool *)
  (* case true *)
  injection 2 ; intros until 4 ; subst.
  rewrite set_color_variant ;
  discriminate.
  (* case false *)
  injection 2 ; intros until 2 ; subst.
  rewrite set_color_variant.
  discriminate.
Qed.

(* Any non-white object still remains non-white. *)

Lemma mark_block_not_white_inv :
forall a0,
forall col overflow cache cache_full a col2 overflow2 cache2 cache_full_2,
(col2, ((overflow2, cache2), cache_full_2)) = mark_block col overflow cache cache_full a ->
(col a0 = White -> False) ->
col2 a0 = White -> False.

Proof.
introvars.
unfold mark_block.
case (valid a).
case_eq (col a). (* color *)
 (* case Black *)
 injection 2 ; intros ; subst ; contradiction.
 (* case Gray *)
 injection 2 ; intros ; subst ; contradiction.
 (* case White *)
 destruct (raw a). (* bool *)
  (* case true *)
  injection 2 ; intros until 4 ; subst.
  unfold set_color.
  destruct (eq_A_dec a0 a).
   (* case = *)
   intros ; discriminate.
   (* case <> *)
   auto.
  (* case false *)
  injection 2 ; intros until 2 ; subst.
  unfold set_color.
  destruct (eq_A_dec a0 a).
   (* case = *)
   intros ; discriminate.
   (* case <> *)
   auto.
injection 1; intros; subst; eauto.
Qed.

Lemma mark_list_not_white_inv :
forall a0,
forall l col overflow cache cache_full col2 overflow2 cache2 cache_full_2,
(col2, ((overflow2, cache2), cache_full_2)) = mark_list col overflow cache cache_full l ->
(col a0 = White -> False) ->
col2 a0 = White -> False.

Proof (fun a0 => mark_list_general (mark_block_not_white_inv (a0 := a0))).

Lemma mark_list_no_white :
forall l x,
member x l ->
forall col overflow cache cache_full col2 overflow2 cache2 cache_full_2,
(col2, ((overflow2, cache2), cache_full_2)) = mark_list col overflow cache cache_full l ->
valid x = true ->
col2 x  = White -> False.

Proof.
induction 1 ; simpl ; introvars. (* member *)
 (* case head *)
 case_eq (mark_block col overflow cache cache_full x) ;
 intros col1 p ;
 destruct p as [[overflow1 cache1] cache_full_1] ;
 intros.
 eapply mark_list_not_white_inv ; eauto.
 intros.
 eapply mark_block_no_white ; eauto.
 (* case tail *)
 case_eq (mark_block col overflow cache cache_full a) ;
 intros col1 p ;
 destruct p as [[overflow1 cache1] cache_full_1] ;
 intros.
 eapply IHmember ; eauto.
Qed.

Lemma mark_gray_not_white_inv :
forall col overflow cache cache_full col2 overflow2 cache2 cache_full_2,
mark_gray_prop col overflow cache cache_full col2 overflow2 cache2 cache_full_2 ->
forall x,
(col x = White -> False) ->
col2 x = White -> False.

Proof.
induction 1. (* mark_gray_prop *)
 (* case O *)
 contradiction.
 (* case S *)
 intros.
 eapply IHmark_gray_prop ; eauto.
 (* col2 x = White -> False *)
 intros.
 eapply mark_list_not_white_inv ; eauto.
 (* set_color a Black col x = White -> False *)
 unfold set_color.
 match goal with [ |- context [(eq_A_dec x ?b)] ] => case (eq_A_dec x b) end ; intros.
  (* case = *)
  discriminate.
  (* case <> *)
  auto.
Qed.

Lemma mark_gray_invar : 
forall col overflow cache cache_full col2 overflow2 cache2 cache_full_2,
mark_gray_prop col overflow cache cache_full col2 overflow2 cache2 cache_full_2 ->
(forall s t, col s = Black -> points_to valid children raw s t -> col t = White -> False) ->
forall s t, col2 s = Black -> points_to valid children raw s t -> col2 t = White -> False.

Proof.
induction 1 as [ | ? ? ? ? a] ; eauto. (* mark_gray_prop *)
(* case S *)
inversion 3.
intros. eapply IHmark_gray_prop ; eauto.
intros s0 t0.
inversion 2. intros.
destruct (eq_A_dec s0 a).
  (* case = *)
  subst.
  eapply mark_list_no_white ; eauto.
  (* case <> *)
  eapply (mark_list_invar (P := fun x => x <> a)) ; eauto.
  unfold set_color.
  intros s1 t1.
  case (eq_A_dec s1 a).
   (* case = *)
   intros ; contradiction.
   (* case <> *) 
   inversion 4.
   case (eq_A_dec t1 a) ; eauto.
   intros ; discriminate.
Qed.

(* Conversely, if a white object before marking is no longer white,
   then it is valid. *)

Lemma mark_block_changed_valid :
forall a col overflow cache cache_full col2 overflow2 cache2 cache_full_2,
(col2, ((overflow2, cache2), cache_full_2)) = mark_block col overflow cache cache_full a ->
col a = White ->
(col2 a = White -> False) ->
valid a = true.
Proof.
introvars.
unfold mark_block.
case_eq (valid a); auto.
injection 2; intros; subst; contradiction.
Qed.

Corollary mark_block_changed_valid_inv : 
forall col overflow cache cache_full a col2 overflow2 cache2 cache_full_2,
(col2, ((overflow2, cache2), cache_full_2)) = mark_block col overflow cache cache_full a ->
(forall x, (col x = White -> False) -> valid x = true) ->
forall x, (col2 x = White -> False) -> valid x = true.
Proof.
introvars.
unfold mark_block.
case_eq (valid a).
intro.
case_eq (col a).
injection 2; intros; subst; auto.
injection 2; intros; subst; auto.
case (raw a);
injection 2.
intros until 5; subst; unfold set_color.
intro x.
destruct (eq_A_dec x a).
congruence.
intros; eauto.
intros until 3; subst; unfold set_color.
intro x.
destruct (eq_A_dec x a).
congruence.
intros; eauto.
injection 2; intros; subst; eauto.
Qed.

Corollary mark_list_changed_valid_inv :
forall l col overflow cache cache_full col2 overflow2 cache2 cache_full_2,
(col2, ((overflow2, cache2), cache_full_2)) = mark_list col overflow cache cache_full l ->
(forall x, (col x = White -> False) -> valid x = true) ->
forall x, (col2 x = White -> False) -> valid x = true.

Proof (mark_list_general mark_block_changed_valid_inv).

(* Cache is valid *)
Lemma mark_block_cache_valid :
forall col overflow cache cache_full a col2 overflow2 cache2 cache_full_2,
(col2, ((overflow2, cache2), cache_full_2)) = mark_block col overflow cache cache_full a ->
(forall x, member x cache -> valid x = true) ->
forall x, member x cache2 -> valid x = true.
Proof.
introvars.
unfold mark_block.
case_eq (valid a).
intro.
case (col a).
injection 1; intros; subst; eauto.
injection 1; intros; subst; eauto.
case (raw a).
injection 1; intros; subst; eauto.
unfold cache_push.
case (cache_is_full cache_full); injection 1.
 intros ; subst; auto.
 intros until 5; intros x Hmem; subst.
 inversion Hmem; auto.
 injection 2; intros; subst; eauto.
Qed.

Corollary mark_list_cache_valid :
forall l col overflow cache cache_full col2 overflow2 cache2 cache_full_2,
(col2, ((overflow2, cache2), cache_full_2)) = mark_list col overflow cache cache_full l ->
(forall x, member x cache -> valid x = true) ->
forall x, member x cache2 -> valid x = true.

Proof (mark_list_general mark_block_cache_valid).


Lemma cache_pop_valid_elem : forall col overflow cache cache_full a cache2 cache_full_2,
((Some a, cache2), cache_full_2) = cache_pop col overflow cache cache_full ->
(forall x, member x cache -> valid x = true) ->
valid a = true.

Proof.
unfold cache_pop.
introvars.
case cache.
case overflow.
case_eq (first_gray col).
 intros a0 Ha0.
 destruct (Hfirst_gray_some Ha0) as [Hvalid ?].
 injection 1; intros; subst; auto.
intros; discriminate.
discriminate 1.
injection 1.
intros.
subst.
eauto.
Qed.

Lemma cache_pop_valid_cache : forall col overflow cache cache_full a cache2 cache_full_2,
((a, cache2), cache_full_2) = cache_pop col overflow cache cache_full ->
(forall x, member x cache -> valid x = true) ->
forall x, member x cache2 -> valid x = true.

Proof.
unfold cache_pop.
introvars.
case cache.
case overflow.
case (first_gray col).
injection 1; intros; subst; eauto.
injection 1; intros; subst; eauto.
injection 1; intros; subst; eauto.
injection 1; intros; subst; eauto.
Qed.

Corollary mark_gray_cache_valid :
 forall col overflow cache cache_full col2 overflow2 cache2 cache_full_2,
 mark_gray_prop col overflow cache cache_full col2 overflow2 cache2 cache_full_2 ->
(forall x, member x cache -> valid x = true) ->
forall x, member x cache2 -> valid x = true.

Proof.
induction 1.
intros.
eapply cache_pop_valid_cache.
eassumption.
auto.
auto.
intro Hcache.
apply IHmark_gray_prop.
intros ; eapply mark_list_cache_valid.
eassumption.
intros.
eapply cache_pop_valid_cache.
eassumption.
auto.
auto.
auto.
Qed.

Lemma mark_gray_changed_valid_inv :
 forall col overflow cache cache_full col2 overflow2 cache2 cache_full_2,
 mark_gray_prop col overflow cache cache_full col2 overflow2 cache2 cache_full_2 ->
(forall x, member x cache -> valid x = true) ->
(forall x, (col x = White -> False) -> valid x = true) ->
forall x, (col2 x = White -> False) -> valid x = true.
Proof.
induction 1; auto.
intros Hvalid Hcol.
apply IHmark_gray_prop.
intros.
eapply mark_list_cache_valid.
eassumption.
intros.
eapply cache_pop_valid_cache.
eassumption.
auto.
auto.
auto.
intros.
eapply mark_list_changed_valid_inv; eauto.
intro x0.
unfold set_color.
destruct (eq_A_dec x0 a).
subst.
intro.
eapply cache_pop_valid_elem.
eassumption.
auto.
apply Hcol.
Qed.

(* If there is no overflow, then all the gray items are in the cache. *)

Lemma mark_block_all_gray_in_cache : 
forall col overflow cache cache_full a col2 overflow2 cache2 cache_full_2,
(col2, ((overflow2, cache2), cache_full_2)) = mark_block col overflow cache cache_full a ->
(overflow = false -> forall x, col x = Gray -> member x cache) ->
overflow2 = false -> forall x, col2 x = Gray -> member x cache2.

Proof.
unfold mark_block.
introvars.
case (valid a); [ | (injection 1; intros; subst; eauto)];
case_eq (col a). (* color *)
 (* case Black *)
 injection 2 ; intros ; subst ; eauto.
 (* case Gray *)
 injection 2 ; intros ; subst ; eauto.
 (* case White *)
 case (raw a). (* bool *)
  (* case true *)
  unfold set_color.
  injection 2 ; intros until 6.
  intro.
  subst.
  destruct (eq_A_dec x a) ; intros.
   (* case = *)
   discriminate.
   (* case <> *)
   eauto.
  (* case false *)
  injection 2.
  unfold cache_push.
  case (cache_is_full cache_full); injection 1.
   (* case true *)
   intros ; subst ; discriminate.
   (* case false *)
   intros until 6; subst.
   unfold set_color.
   subst.
   intro.
   destruct (eq_A_dec x a) ;subst ; eauto.
Qed.

Lemma mark_list_all_gray_in_cache : 
forall l col overflow cache cache_full col2 overflow2 cache2 cache_full_2,
(col2, ((overflow2, cache2), cache_full_2)) = mark_list col overflow cache cache_full l ->
(overflow = false -> forall x, col x = Gray -> member x cache) ->
overflow2 = false -> forall x, col2 x = Gray -> member x cache2.

Proof (mark_list_general mark_block_all_gray_in_cache).

(* After the Mark_gray loop, there are no more Gray objects. *)

Lemma mark_gray_no_gray :
 forall col overflow cache cache_full col2 overflow2 cache2 cache_full_2,
 mark_gray_prop col overflow cache cache_full col2 overflow2 cache2 cache_full_2 ->
 (overflow = false -> forall x, col x = Gray -> member x cache) ->
 (forall x, member x cache -> valid x = true) ->
 (forall x, (col x = White -> False) -> valid x = true) ->
 forall x, col2 x = Gray -> False.

Proof.
induction 1. (* mark_gray_prop *)
 (* case O *)
 match goal with [ H : context [cache_pop] |- _ ] => genclear H end.
 unfold cache_pop.
 destruct cache. (* list *)
  (* case nil *)
  destruct overflow. (* bool *)
   (* case true *)
   case_eq (first_gray col). 
    (* case gray *)
    intros ; discriminate.
    (* case no gray *)
   intro f_n.
   generalize (Hfirst_gray_none f_n).
   intro f.
   injection 1.
   intros ? ? _ _ Hvalid x Hcol.
   subst.
   eapply f.
   2 : eexact Hcol.
   eapply Hvalid.
   rewrite Hcol.
   discriminate 1.
   (* case false *)
   injection 1.
   intros ; subst.
   eapply member_nil; eauto.
  (* case cons *)
  intros ; discriminate.
 (* case S *)
 intros ? Hcache_valid Hvalid x ?. 
 eapply IHmark_gray_prop ; eauto.
 intros.
 eapply mark_list_all_gray_in_cache ; eauto.
 match goal with [ H : context [cache_pop] |- _ ] => genclear H end.
 unfold cache_pop.
 destruct cache as [ | a0 ]. (* list *)
  (* case nil *)
  destruct overflow ; intros ; discriminate.
  (* case cons *)
  injection 1 ; intros until 4 ; subst ; eauto.
  intro x1.
  unfold set_color.
  destruct (eq_A_dec x1 a0).
   (* case = *)
   intros ; discriminate.
   (* case <> *)
   intros ; eauto.
   apply member_step with a0 ; eauto.
  intros; eapply mark_list_cache_valid; eauto.
  intros; eapply cache_pop_valid_cache; eauto.
  intros ; eapply mark_list_changed_valid_inv; eauto.
  unfold set_color.
  intro x1.
  destruct (eq_A_dec x1 a).
  intros _.
  subst.
  eapply cache_pop_valid_elem; eauto.
 eauto.
Qed.

Theorem gc_mark_no_gray :
 forall cache_full col2 overflow2 cache2 cache_full_2,
 gc_mark_prop cache_full col2 overflow2 cache2 cache_full_2 ->
 forall x, col2 x = Gray -> False.

Proof.
inversion 1.
intros ; eapply mark_gray_no_gray ; eauto.
intros; eapply mark_list_all_gray_in_cache ; eauto.
simpl ; intros ; discriminate.
intros ; eapply mark_list_cache_valid; eauto.
intros; eapply mark_list_changed_valid_inv ; eauto.
Qed.

Lemma gc_mark_invar  :
 forall cache_full col2 overflow2 cache2 cache_full_2,
 gc_mark_prop cache_full col2 overflow2 cache2 cache_full_2 ->
 forall s t, col2 s = Black -> points_to valid children raw s t -> col2 t = White -> False.

Proof.
inversion 1.
intros.
eapply mark_gray_invar; eauto.
intros.
eapply (mark_list_invar (P := fun _ => True)); eauto.
simpl ; intros ; discriminate.
Qed.

Lemma gc_mark_valid_roots_not_white :
 forall cache_full col2 overflow2 cache2 cache_full_2,
 gc_mark_prop cache_full col2 overflow2 cache2 cache_full_2 ->
 forall x, member x roots -> valid x = true -> col2 x = White -> False.

Proof.
inversion 1.
intros.
eapply (mark_gray_not_white_inv) ; eauto.
intros.
eapply (mark_list_no_white) ; eauto.
Qed.

(* Finally... *)

Theorem gc_mark_correct :
 forall cache_full col2 overflow2 cache2 cache_full_2,
 gc_mark_prop cache_full col2 overflow2 cache2 cache_full_2 ->
 forall x, used valid roots children raw x -> col2 x = White -> False.

Proof.
induction 2 ; intros. (* used *)
 (* case root *)
 eapply gc_mark_valid_roots_not_white ; eauto.
 (* case child *)
 eapply gc_mark_invar ; eauto.
 match goal with [ |- context [col2 ?k] ] => case_eq (col2 k) end ; intros ; eauto. (* color *)
  (* case Gray *)
  apply False_rect.
  eapply gc_mark_no_gray ; eauto.
  (* case White *)
  contradiction.
Qed.

End Correctness.

Section Completeness.

(* gc_mark is complete : any non-used object is white. *)

Section Gray_cache.

(* Push and pop keep the following invariant : every element of the cache is gray *)

Lemma cache_push_gray : forall col a cache cache_full o0 o cache2 cache_full_2,
((o, cache2), cache_full_2) = cache_push a o0 cache cache_full ->
col a = Gray ->
(forall x, member x cache -> col x = Gray) ->
forall x, member x cache2 -> col x = Gray.

Proof.
introvars.
unfold cache_push.
case (cache_is_full cache_full); injection 1. (* bool *)
 (* case true *)
 intros ; subst ; eauto.
 (* case <> *)
 intros until 5 ; subst.
 inversion 1 ; subst ; eauto.
Qed.

Lemma mark_block_gray_cache col overflow cache cache_full a col2 overflow2 cache2 cache_full_2
 :
 (col2, ((overflow2, cache2), cache_full_2)) = mark_block  col overflow cache cache_full a ->
 (forall x, member x cache -> col x = Gray) ->
 forall x, member x cache2 -> col2 x = Gray.

Proof.
unfold mark_block.
introvars.
case (valid a); [| injection 1; intros; subst; auto].
case_eq (col a). (* color *)
 (* case Black *)
 injection 2 ; intros ; subst ; eauto.
 (* case Gray *)
 injection 2 ; intros ; subst ; eauto.
 (* case White *)
 destruct (raw a). (* bool *)
  (* case true *)
  injection 2 ; intros until 5 ; subst.
  unfold set_color.
  intros.
  destruct (eq_A_dec x a).
   (* case = *)
   subst.
   assert (col a = Gray).
   eauto.
   discr.
   (* case <> *)
   eauto.
  (* case false *)
  var (cache_push a overflow cache cache_full).
  injection 2.
  intros.
  subst.
  eapply cache_push_gray ; eauto.
   (* set_color a Gray col a = Gray *)
   apply set_color_variant.
   (* forall x1, member x1 cache -> set_color a Gray col x1 = Gray *)
   intro x3; intros.
   unfold set_color.
   destruct (eq_A_dec x3 a) ; auto.
Qed.

Lemma mark_list_gray_cache :
forall l col overflow cache cache_full
col2 o2 cache2 cache_full_2,
(col2, ((o2, cache2), cache_full_2)) = mark_list col overflow cache cache_full l ->
(forall x, member x cache -> col x = Gray) ->
forall x, member x cache2 -> col2 x = Gray.

Proof (mark_list_general mark_block_gray_cache).

(* Whenever the cache is popped, we get a gray object *)

Lemma cache_pop_gray_elem : forall col overflow cache cache_full cache2 cache_full_2 a,
((Some a, cache2), cache_full_2) = cache_pop col overflow cache cache_full ->
(forall x, member x cache -> col x = Gray) ->
col a = Gray.

Proof.
introvars.
unfold cache_pop.
destruct cache. (* list *)
 (* case nil *)
 destruct overflow. (* bool *)
  (* case true *)
  case_eq (first_gray col).
   (* case gray *)
   intros a0 Ha0.
   generalize (Hfirst_gray_some Ha0).
   intros [? ?].
   injection 1 ; intros ; subst ; trivial.
   (* case no gray *)
   intros ; discriminate.
  (* case false *)
  intros ; discriminate.
 (* case cons *)
 injection 1 ; intros ; subst ; eauto.
Qed.

Lemma cache_pop_gray_cache : forall col overflow cache cache_full cache2 cache_full_2 w,
((w, cache2), cache_full_2) = cache_pop col overflow cache cache_full ->
(forall x, member x cache -> col x = Gray) ->
forall x, member x cache2 -> col x = Gray.

Proof.
introvars.
unfold cache_pop.
destruct cache. (* list *)
 (* case nil *)
 destruct overflow. (* bool *)
  (* case true *)
  destruct (first_gray col) as [s | ].
   (* case gray *)
   injection 1 ; intros ; subst ; eauto.
   (* case no gray *)
   injection 1 ; intros ; subst ; eauto.
  (* case false *)
  injection 1 ; intros ; subst ; eauto.
 (* case cons *)
  injection 1 ; intros ; subst ; eauto.
Qed.

End Gray_cache.

Section Gray_not_raw.

(* no gray element is raw *)

Lemma set_color_black_gray_not_raw :
forall col,
(forall x, col x = Gray -> raw x = false) ->
forall a x, set_color a Black col x = Gray -> raw x = false.

Proof.
intros until 1.
introvars.
unfold set_color.
destruct (eq_A_dec x a) ; eauto.
discriminate 1.
Qed.

Lemma mark_block_gray_not_raw
 (col : A -> color) (overflow : bool) (cache : list A) cache_full
 (a : A)
 (col2 : A -> color) 
 (overflow2 : bool)
 (cache2 : list A)
 cache_full_2
 :
 (col2, ((overflow2, cache2), cache_full_2)) = mark_block  col overflow cache cache_full a ->
 (forall x, col x = Gray -> raw x = false) ->
 forall x, col2 x = Gray -> raw x = false.

Proof.
unfold mark_block.
introvars.
case (valid a); [|injection 1; intros; subst; auto].
case_eq (col a). (* color *)
 (* case Black *)
 injection 2 ; intros ; subst ; eauto.
 (* case Gray *)
 injection 2 ; intros ; subst ; eauto.
 (* case White *)
 case_eq (raw a). (* bool *)
  (* case true *)
  injection 3 ; intros until 5 ; subst ; eauto.
  apply set_color_black_gray_not_raw ; auto.
  (* case false *)
  injection 3 ; intros until 3 ; subst ; eauto.
  intro x.
  unfold set_color.
  destruct (eq_A_dec x a) ; subst ; auto.
Qed.

Lemma mark_list_gray_not_raw :
forall l col overflow cache cache_full
col2 o2 cache2 cache_full_2,
(col2, ((o2, cache2), cache_full_2)) = mark_list col overflow cache cache_full l ->
(forall x, col x = Gray -> raw x = false) ->
forall x, col2 x = Gray -> raw x = false.

Proof (mark_list_general mark_block_gray_not_raw).

Lemma mark_gray_gray_not_raw :
forall col overflow cache cache_full col2 overflow2 cache2 cache_full_2,
mark_gray_prop col overflow cache cache_full col2 overflow2 cache2 cache_full_2 ->
(forall x, col x = Gray -> raw x = false) ->
forall x, col2 x = Gray -> raw x = false.

Proof.
induction 1 ; eauto.
intros ; eapply IHmark_gray_prop ; eauto ; intros ; eapply mark_list_gray_not_raw ; eauto.
apply set_color_black_gray_not_raw ; auto.
Qed.

End Gray_not_raw.


Section Cache_no_duplicates.

(* The cache has no duplicate items : an object is never
   pushed twice.

   This section requires the cache to always contain gray
   objects. *)

Lemma mark_block_no_dupl (col : A -> color) (overflow : bool) (cache : list A) cache_full
 (a : A)
 (col2 : A -> color) 
 (overflow2 : bool)
 (cache2 : list A)
 cache_full_2
 :
 (col2, ((overflow2, cache2), cache_full_2)) = mark_block col overflow cache cache_full a ->
 ((forall x, member x cache -> col x = Gray) /\ no_duplicates cache) ->
 ((forall x, member x cache2 -> col2 x = Gray) /\ no_duplicates cache2).

Proof.
inversion 2.
split.
 (* gray cache *)
 intros.
 eapply (mark_block_gray_cache) ; eauto.
 (* no duplicates *)
 match goal with [ _ : context [mark_block] |- _ ] => genclear H end.
 unfold mark_block.
 case (valid a); [|injection 1; intros; subst; trivial].
 case_eq (col a). (* color *)
  (* case Black *)
  injection 2 ; intros ; subst ; trivial.
  (* case Gray *)
  injection 2 ; intros ; subst ; trivial.
  (* case White *)
  destruct (raw a). (* bool *)
   (* case true *)
   injection 2 ; intros ; subst ; auto.
   (* case false *)
   unfold cache_push.
   case (cache_is_full cache_full) ; injection 2; intros; subst; eauto.
    apply no_duplicates_cons.
    intros.
    assert (col a = Gray).
    eauto.
    discr.
    auto.
Qed.

(* HERE *)

Corollary mark_list_no_dupl_0 :
forall l col overflow cache cache_full
col2 o2 cache2 cache_full_2,
(col2, ((o2, cache2), cache_full_2)) = mark_list col overflow cache cache_full l ->
((forall x, member x cache -> col x = Gray) /\ no_duplicates cache) ->
((forall x, member x cache2 -> col2 x = Gray) /\ no_duplicates cache2).

Proof (mark_list_general mark_block_no_dupl).

Corollary mark_list_no_dupl :
forall l col overflow cache cache_full
col2 o2 cache2 cache_full_2,
(col2, ((o2, cache2), cache_full_2)) = mark_list col overflow cache cache_full l ->
(forall x, member x cache -> col x = Gray) ->
no_duplicates cache ->
no_duplicates cache2.

Proof.
introvars.
intros Hmark_list Hno_gray Hno_dupl.
generalize (mark_list_no_dupl_0 Hmark_list (conj Hno_gray Hno_dupl)).
inversion 1 ; eauto.
Qed.

Lemma cache_pop_no_dupl : forall col overflow cache cache_full cache2 cache_full_2 w,
((w, cache2), cache_full_2) = cache_pop col overflow cache cache_full ->
no_duplicates cache ->
no_duplicates cache2.

Proof.
introvars.
unfold cache_pop.
destruct cache. (* list *)
 (* case nil *)
 destruct overflow. (* bool *)
  (* case true *)
   destruct (first_gray col).
  (* case gray *)
    injection 1 ; intros ; subst ; eauto.
   (* case no gray *)
   injection 1 ; intros ; subst ; eauto.
  (* case false *)
   injection 1 ; intros ; subst ; eauto.
 (* case cons *)
 injection 1 ; intros ; subst ; eauto.
Qed.

Lemma cache_pop_not_mem : forall col overflow cache cache_full cache2 cache_full_2 a,
((Some a, cache2), cache_full_2) = cache_pop col overflow cache cache_full ->
no_duplicates cache ->
member a cache2 -> False.

Proof.
introvars.
unfold cache_pop.
destruct cache. (* list *)
 (* case nil *)
 destruct overflow. (* bool *)
  (* case true *)
  destruct (first_gray col).
   (* case gray *)
   injection 1 ; intros until 3 ; subst ; inversion 2.
   (* case no gray *)
   intros ;discriminate.
  (* case false *)
  intros ; discriminate.
 (* case cons *)
 injection 1 ; intros until 3 ; subst.
 inversion 1 ; intros ; contradiction.
Qed.

End Cache_no_duplicates.

(* When the color of an object changes through marking a list of objects,
   then the object was necessary in the list. *)

Lemma mark_list_changed : forall l col overflow cache cache_full col2 overflow2 cache2 cache_full_2,
(col2, ((overflow2, cache2), cache_full_2)) = mark_list col overflow cache cache_full l ->
forall x, col x = White -> (col2 x = White -> False) -> member x l.

Proof.
induction l ; simpl. (* list *)
 (* case nil *)
 injection 1 ; intros ; subst ; contradiction.
 (* case cons *)
 unfold mark_block.
 introvars.
 case (valid a).
 case_eq (col a) ;eauto. (* color *)
 (* case White *)
 unfold set_color.
 intros until 3.
 destruct (eq_A_dec x a) ; subst ; intros ; eauto.
 (* case <> *)
 destruct (raw a) ; intros ; apply member_tail. (* list *)
  (* case nil *)
  eapply IHl ; eauto.
  simpl.
  destruct (eq_A_dec x a) ; eauto.
  contradiction.
  (* case cons *)

  destruct (cache_push a overflow cache cache_full) as [[? ?] ?].
  eapply IHl ; eauto.
  simpl ; destruct (eq_A_dec x a) ; auto.
  contradiction.
(* case not valid *)
eauto.
Qed.

(* Then, when marking the list of the children of a non-white object, the
   invariant "non-white objects are used" is kept. *)

Lemma mark_list_used : forall a col overflow cache cache_full col2 overflow2 cache2 cache_full_2,
(col2, ((overflow2, cache2), cache_full_2)) = mark_list col overflow cache cache_full (children a) ->
(col a = White -> False) ->
raw a = false ->
(forall x, (col x = White -> False) -> used valid roots children raw x) ->
forall x, (col2 x = White -> False) -> used valid roots children raw x.

Proof.
intros until 3.
intro Hcol.
intros.
destruct (eq_A_dec x a) ; subst ; eauto.
 (* case <> *)
 case_eq (col x) ; intros ; eauto. (* color *)
  (* case Black *)
  eapply Hcol ; eauto ; intros ; discr.
  (* case Gray *)
  eapply Hcol ; eauto ; intros ; discr.
  (* case White *)
  eapply used_child ; eauto.
  eapply points_to_intro ; eauto.
  eapply (mark_list_changed) ; eauto.
 (* valid *)
 eapply mark_list_changed_valid_inv.
 eassumption.
 intros.
 eapply (used_valid (A := A)).
 eapply Hcol.
 assumption.
 assumption.
Qed.

(* The Mark_gray loop also keeps this invariant. *)

Lemma mark_gray_used : forall col overflow cache cache_full col2 overflow2 cache2 cache_full_2,
mark_gray_prop col overflow cache cache_full col2 overflow2 cache2 cache_full_2 ->
(forall x, member x cache -> col x = Gray) ->
(forall x, col x = Gray -> raw x = false) ->
no_duplicates cache ->
(forall x, (col x = White -> False) -> used valid roots children raw x) ->
forall x, (col2 x = White -> False) -> used valid roots children raw x.

Proof.
induction 1 as [| ? ? ? ? a] ; eauto.
intros until 4.
intro x.
case_eq (col x) ; eauto. (* color *)
 (* case Black *)
 intros.
 assert (col x = White -> False).
  intro ; discr.
 eauto.
 (* case Gray *)
 intros.
 assert (col x = White -> False).
  intro ; discr.
 eauto.
 (* case White *)
 assert (col a = Gray).
  eapply cache_pop_gray_elem ; eauto.
 assert (col a = White -> False).
  intro ; discr.
 assert (used valid roots children raw a) as Ha_used.
  eauto.
 destruct (eq_A_dec x a) ; subst ; eauto.
 (* case <> *)
 case_eq (col2 x) ; intros. (* color *)
   (* case Black *)
   eapply mark_list_used ; eauto.
    (* set_color a Black col a <> White *)
    rewrite set_color_variant ; intros ; discriminate.
    (* forall x0, set_color a Black col x0 <> White -> used x0 *)
    unfold set_color.
    intro x0.
    destruct (eq_A_dec x0 a) ; subst ; auto.
    (* col2 x <> White *)
    intro ; discr.
   (* case Gray *)
   eapply mark_list_used ; eauto.
    (* set_color a Black col a <> White *)
    rewrite set_color_variant ; intros ; discriminate.
    (* forall x0, set_color a Black col x0 <> White -> used x0 *)
    unfold set_color.
    intro x0.
    destruct (eq_A_dec x0 a) ; subst ; auto.
    (* col2 x <> White *)
    intro ; discr.
   (* case White *)
   assert (Hcache : cache = nil /\ cache1 = nil \/ cache = a::cache1).
    eapply cache_pop_which ; eauto.
   inversion Hcache.
    (* case cache = cache1 = nil *)
    invall.
    subst.
    eapply IHmark_gray_prop ; eauto.
     (* forall x0, member x0 cache2 -> col2 x0 = Gray *)
     intros ; eapply mark_list_gray_cache ; eauto.
     inversion 1.
     (* forall x0, col2 x0 = Gray -> raw x0 = false *)
     intro x0.
     intros.
     eapply mark_list_gray_not_raw ; eauto.
     apply set_color_black_gray_not_raw ; auto.
     (* no_duplicates cache2 *)
     eapply mark_list_no_dupl ; eauto.
     inversion 1.
     (* forall x0, col2 x0 <> White -> used x0 *)
     intros.
     eapply mark_list_used ; eauto.
      (* set_color a Black col a <> White *)
      rewrite set_color_variant ; intros ; discriminate.
      (* forall x1, set_color a Black col x1 <> White -> used x1 *)
      unfold set_color.
      intro x1.
      destruct (eq_A_dec x1 a) ; subst ; auto.
    (* case cache = a::cache1 *)
    subst.
    eapply IHmark_gray_prop ; eauto.
     (* forall x1, member x1 cache2 -> col2 x1 = Gray *)
     intros.
     eapply mark_list_gray_cache ; eauto.
     intro x1.
     unfold set_color.
     destruct (eq_A_dec x1 a) ; subst ; eauto.
      (* case = *)
      intros.
      apply False_rect.
      eapply no_duplicates_base ; eauto.
     (* forall x0, col2 x0 = Gray -> raw x0 = false *)
     intros.
     eapply mark_list_gray_not_raw ; eauto.
     apply set_color_black_gray_not_raw ; auto.
     (* no_duplicates cache2 *)
     eapply mark_list_no_dupl ; eauto.
      (* forall x0, member x0 cache1 -> set_color a Black col x0 = Gray *)
      intro x0.
      unfold set_color.
      destruct (eq_A_dec x0 a) ; subst ;eauto.
       (* case = *)
       intros.
       apply False_rect.
       eapply no_duplicates_base ; eauto.
     (* forall x0, col2 x0 <> White -> used x0 *)
     intros.
     eapply mark_list_used ; eauto.
      (* set_color a Black col a <> White *)
      rewrite set_color_variant ; intros ; discriminate.
      (* forall x0, set_color a Black col x0 <> White -> used x0 *)
      unfold set_color.
      intro x1.
      destruct (eq_A_dec x1 a) ; subst ; auto.
Qed.

(* Finally... *)

Theorem gc_mark_complete :
 forall cache_full col2 overflow2 cache2 cache_full_2,
 gc_mark_prop cache_full col2 overflow2 cache2 cache_full_2 ->
 forall x,
 (col2 x = White -> False) ->
 used valid roots children raw x.

Proof.
inversion 1 as [col0 overflow0 cache0 cache_full_0].
intros.
eapply mark_gray_used ; eauto.
 (* forall x0, member x0 cache0 -> col0 x0 = Gray *)
 intros.
 eapply mark_list_gray_cache ; eauto.
 inversion 1.
 (* forall x0, col0 x0 = Gray -> raw x0 = false *)
 intros.
 eapply mark_list_gray_not_raw ; eauto.
 simpl ; discriminate 1.
 (* no_duplicates cache0 *)
 eapply mark_list_no_dupl ; eauto.
 inversion 1.
 (* forall x0, col0 x0 <> White -> used x0 *)
 intros.
 eapply used_root.
 eapply mark_list_changed ; eauto.
(* valid root. *)
 eapply mark_list_changed_valid_inv.
 eassumption.
 simpl.
 intros; congruence.
 assumption.
Qed.

End Completeness.

Section Final.

(* Let's rewrite everything in terms of equivalences. *)

Variable x : A.
Variable cache_full_0 : B.
Variable col : A -> color.
Variable overflow : bool.
Variable cache : list A.
Variable cache_full : B.
(*
Hypothesis H : gc_mark_term.
Hypothesis Hcol : (col, (overflow, cache)) = gc_mark H.
*)
Hypothesis Hcol : gc_mark_prop cache_full_0 col overflow cache cache_full.

Theorem gc_mark_used_black : 
 (used valid roots children raw x -> col x = Black).

Proof.
case_eq (col x) ; eauto ; intros ; apply False_ind. (* color *)
 (* case Gray *)
 eapply gc_mark_no_gray ; eauto.
 (* case White *)
 eapply gc_mark_correct ; eauto.
Qed.

Theorem gc_mark_black_used : 
 (col x = Black -> used valid roots children raw x).

Proof.
 intros.
 eapply gc_mark_complete ; eauto.
 intros ; discr.
Qed.

Theorem gc_mark_not_used_white : 
 ((used valid roots children raw x -> False) -> col x = White).

Proof.
 case_eq (col x) ; auto ; intros ; apply False_ind. (* color *)
  (* case Black *)
  absurd (used valid roots children raw x) ; eauto.
  eapply gc_mark_complete ; eauto.
  intros ; discr.
  (* case Gray *)
  eapply gc_mark_no_gray ; eauto.
 (* <- *)
Qed.

Theorem gc_mark_white_not_used : 
 (col x = White -> (used valid roots children raw x -> False)).
Proof.
 intros.
 eapply gc_mark_correct ; eauto.
Qed.

End Final.

(* Finally again, it is possible to constructively decide
   whether an object is used or not, **assuming** that
   the marking process terminates, which depends on A.
*)

Definition used_excluded_middle : forall cache_full_0, gc_mark_term cache_full_0 -> forall x,
{used valid roots children raw x} + {used valid roots children raw x -> False}.

Proof.
intros ? H.
destruct (gc_mark H) as [col [overflow [cache [cache_full ?]]]].
intro.
case_eq (col x) ; intro. (* color *)
 (* case Black *)
 left.
 eapply gc_mark_black_used ; eauto.
 (* case Gray *)
 apply False_rect.
 eapply gc_mark_no_gray ; eauto.
 (* case White *)
 right.
 intros.
 eapply gc_mark_white_not_used ; eauto.
Defined.

End Mark.

Extraction NoInline set_color.


(* Recursive Extraction used_excluded_middle. *)