Require Export Memory.

(*
Time Fixpoint find_root_list_constr (m : mem) (n : nat)     (b : block) (i : int) {struct n} : option (block * int) :=
  match n with
    | O => Some (b, i)
    | S n' =>
      match load Mint32 m b (signed i) with
        | Some (Vptr c j) => find_root_list_constr m n'  c j 
          
        | _ => None
      end
  end.
*)

Section Find_root_list_constr.

Variable m : mem.

Let body k :=
  match k with
    | (S n', Some (b, i)) => 
      match load Mint32 m b (signed i) with
        | Some (Vptr c j) => (true, (n', Some (c, j)))
        | _ => (false, (S n', None))
      end
    | _ => (false, k)
  end.

Lemma loop_terminates : forall n bi, Loop.loop_term body (n, bi).
Proof.
unfold body.
induction n.
intros.
eapply Loop.loop_term_interrupt.
 reflexivity.
destruct bi.
 destruct p.
 case_eq (load Mint32 m b (signed i)).
 destruct v; try repeat (
   intro Hbi;
     eapply Loop.loop_term_interrupt;
       rewrite Hbi;
         reflexivity
 ).
 intro Hbi.
 eapply Loop.loop_term_continue.
 rewrite Hbi.
 reflexivity.
 eapply IHn.
 intro Hbi.
 eapply Loop.loop_term_interrupt.
 rewrite Hbi.
 reflexivity.
eapply Loop.loop_term_interrupt. 
reflexivity.
Qed.

Lemma loop_correct : forall k k',
  Loop.loop_prop body k k' ->
  forall n b i, k = (n, (Some (b, i))) ->
    forall b' i', k' = (O, Some (b', i')) ->
      find_root_list m n b i b' i'.
Proof.
induction 1; intros; subst; generalize H; unfold body; destruct n.
 injection 1; intros; subst.
 apply find_root_list_O.
 destruct (load Mint32 m b (signed i)); try (intros; discriminate).
 destruct v; intros; discriminate.
intros; discriminate.
case_eq (load Mint32 m b (signed i)); try (intros; discriminate).
destruct v; try (intros; discriminate).
injection 2; intros; subst.
eapply find_root_list_S.
symmetry.
eassumption.
eapply IHloop_prop.
reflexivity.
reflexivity.
Qed.

Lemma loop_complete : forall n b i b' i',
  find_root_list m n b i b' i' ->
  Loop.loop_prop body (n, (Some (b, i))) (O, Some (b', i')).
Proof.
induction 1.
 eapply Loop.loop_prop_interrupt.
 reflexivity.
eapply Loop.loop_prop_continue.
 unfold body.
 rewrite <- H.
 reflexivity.
eapply IHfind_root_list.
Qed.