Module CsharpminorIterproof


Require Import Coqlib Util.
Require Import Maps.
Require Import Integers.
Require Import Values.
Require Import Memory.
Require Import AdomLib.
Require Import Utf8.
Require Import AST.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Behaviors.
Require Import Csharpminor.
Require Import CsharpminorLogic.
Require Import CsharpminorIter.
Require Import AlarmMon.
Require Import AbMemSignatureCsharpminor.

Section PROG.

Variable (unroll: nat).
Variable (prog: program).
Let ge := Genv.globalenv prog.

Lemma forall_exists {T: Type} (P : TProp) : (∀ t : T, ¬ P t) ∨ ∃ t : T, P t.
Proof.
destruct (Classical_Prop.classic (ex P)); eauto. Qed.

Lemma eval_expr_dec:
  ∀ e t m exp,
    (∃ v, eval_expr ge e t m exp v) \/ (∀ v, ~eval_expr ge e t m exp v).
Proof.
  intros.
  edestruct Classical_Prop.classic.
  left. apply H.
  right. repeat intro. eauto.
Qed.

Lemma eval_exprlist_dec:
  ∀ e t m expl,
    (∃ vl, eval_exprlist ge e t m expl vl) \/
    (∀ vl, ~eval_exprlist ge e t m expl vl).
Proof.
  induction expl; intros. repeat econstructor.
  destruct IHexpl as [[vl Hvl]|].
  edestruct eval_expr_dec as [[v Hv]|].
  repeat econstructor; eauto.
  right. repeat intro. inv H0. intuition eauto.
  right. repeat intro. inv H0. intuition eauto.
Qed.

Section ABMEM.

Variable abstate abstate_iter: Type.

Variable abmem : mem_dom abstate abstate_iter.
Existing Instance abmem.

Variable mem_gamma : gamma_op abstate concrete_state.
Existing Instance mem_gamma.

Variable mem_gamma_iter : gamma_op abstate_iter concrete_state.
Existing Instance mem_gamma_iter.

Variable mem_spec : mem_dom_spec ge abmem mem_gamma mem_gamma_iter.

Lemma type_check_expr_sound :
  ∀ t e s m (ab: abstate),
    ((t, e) :: s, m) ∈ γ ab
    ∀ ty exp,
      type_check_expr ty exp ab = (tt, nil) →
      ∃ ev v,
        v ∈ (eval_expr ge e t m expeventval_match ge ev ty).
Proof.
  intros t e s m ab Gamma ty exp.
  unfold type_check_expr.
  destruct ty; try discriminate; intros NE;
  match type of NE with
  | noerror ?exp ?ab = _ =>
    generalize (noerror_sound ge exp ab); rewrite NE; clear NE; intros NE
  end.
  destruct (forall_existsi, Vint ieval_expr ge e t m exp)) as [ NV | (i & Hi) ];
    [
      destruct (NE None); econstructor; eauto;
      intros v H H0; inv H; simpl in *; eq_some_inv; subst;
      destruct v1; (elim (H0 eq_refl) || (eelim (NV); eauto; repeat econstructor (eauto)))
    |].
  repeat (econstructor (eauto)).
  destruct (forall_existsi, Vfloat ieval_expr ge e t m exp)) as [ NV | (i & Hi) ];
    [
      destruct (NE None); econstructor; eauto;
      intros v H H0; inv H; simpl in *; eq_some_inv; subst;
      destruct v1; (elim (H0 eq_refl) || (eelim (NV); eauto; repeat econstructor (eauto)))
    |].
  repeat (econstructor (eauto)).
  destruct (forall_existsi, Vlong ieval_expr ge e t m exp)) as [ NV | (i & Hi) ];
    [
      destruct (NE None); econstructor; eauto;
      intros v H H0; inv H; simpl in *; eq_some_inv; subst;
      destruct v1; (elim (H0 eq_refl) || (eelim (NV); eauto; repeat econstructor (eauto)))
    |].
  repeat (econstructor (eauto)).
  destruct (forall_existsi, Vsingle ieval_expr ge e t m exp)) as [ NV | (i & Hi) ];
    [
      destruct (NE None); econstructor; eauto;
      intros v H H0; inv H; simpl in *; eq_some_inv; subst;
      destruct v1; (elim (H0 eq_refl) || (eelim (NV); eauto; repeat econstructor (eauto)))
    |].
  repeat (econstructor (eauto)).
Qed.

Lemma fold_left2_bind_mono {A B C} (f: CABalarm_mon C) {ka kb ma} :
  (∀ x y z w, ka x (y :: z) ≠ (w, nil)) →
  (∀ x y z w, kb x (y :: z) ≠ (w, nil)) →
  ∀ mb c d,
    fold_left2q a b, do c <- q; f c a b) ka kb ma mb c = (d, nil) →
    snd c = nil.
Proof.
  intros Hka Hkb.
  induction ma as [ | a ma IH ]; intros [ | b mb ] ( c & [ | ? ? ]) d H;
  simpl in H; eq_some_inv; subst.
  - reflexivity.
  - elim (Hkb _ _ _ _ H).
  - elim (Hkb _ _ _ _ H).
  - elim (Hka _ _ _ _ H).
  - elim (Hka _ _ _ _ H).
  - specialize (IH _ _ _ H).
    destruct (f c a b). simpl in *; subst; eauto.
  - specialize (IH _ _ _ H).
    destruct (f c a b). simpl in *; subst; eq_some_inv.
Qed.

Lemma type_check_list_sound:
  ∀ t e s m (ab: abstate),
    ((t, e) :: s, m) ∈ γ ab
    ∀ targs eargs,
      type_check_list targs eargs ab = (tt, nil) →
      ∃ args vargs,
        args ∈ (eval_exprlist ge e t m eargseventval_list_match ge vargs targs).
Proof.
  intros t e s m ab G targs.
  induction targs as [ | ty targs IH ]; intros [ | exp eargs ];
  unfold type_check_list; simpl; intros H; subst; eq_some_inv.
  - exists nil, nil. split; constructor.
  - generalize (type_check_expr_sound t e s m ab G ty exp).
    destruct (type_check_expr _ _ _) as ( () & [ | ? ? ]).
    intros X; destruct (X eq_refl) as ( ev &v & Hv & Hev); clear X.
    specialize (IH eargs H). clear H.
    destruct IH as (args & vargs & Hargs & Hvargs).
    exists (v :: args), (ev :: vargs). split; constructor; auto.
    exfalso.
    generalizeX Y, fold_left2_bind_mono _ X Y _ _ _ H).
    refineX, _ (X _ _)); discriminate.
Qed.

Lemma ab_builtin_sound:
  ∀ s m (ab: abstate), (s, m) ∈ γ ab ->
  ∀ ef x args ab', ab_builtin ef x args ab = (ab', nil) ->
                   (s = nil ->
                    args = nil /\
                    match ef with EF_external _ _ => True | _ => False end /\
                    ef_sig ef = mksignature nil (Some AST.Tint) cc_default) ->
    ∃ vargs,
      match s with
        | nil => vargs = nil
        | (t, e)::_ => eval_exprlist ge e t m args vargs
      end /\
      (∃ tr vres m', external_call ef ge vargs m tr vres m') /\
       ∀ tr vres m', external_call ef ge vargs m tr vres m' ->
         (match s with
           | nil => nil
           | (t, e) :: s' => (Cminor.set_optvar x vres t, e) :: s'
          end, m') ∈ γ ab' /\
         (s = nil -> ∃ r, vres = Vint r).
Proof.
  intros.
  destruct ef; simpl; try now inv H0.

    Ltac clarify :=
      repeat
        (match goal with
         | H : Senv.block_is_volatile _ _ = _ |- _ => rewrite H
         | H : Senv.find_symbol _ _ = _ |- _ => unfold Senv.find_symbol, Genv.to_senv in H
         end || determ).

  - (* EF_vload *)
    simpl in *.
    assert (A := ab_vload_sound ge x None chunk args ab). rewrite H0 in A.
    clear H0.
    destruct s as [ | (t,e) s ]. destruct (H1 eq_refl); hsplit; discriminate. clear H1.
    destruct (forall_existsx,
        let '(arg, g, b, i) := x in
        match chunk with Mint64 | Mfloat32 | Mfloat64 | Mint32 => True | _ => False end
        args = arg :: nil
        eval_expr ge e t m arg (Vptr b i) ∧
        Genv.find_symbol ge g = Some b
        (Senv.block_is_volatile ge b = false
         ∃ v, Mem.load chunk m b (Int.unsigned i) = Some v)
    )) as [ K | K ].
    { destruct (A None); econstructor; eauto.
      intros Hchunk tr vres g b ofs Hargs Hb Htr.
      destruct args as [ | arg [ | ? ? ] ]; try (destruct Hargs; fail).
      elim (K (arg, g, b, ofs)). repeat (refine (conj _ _); auto).
      intros Hvol. inv Htr. rewrite H0 in Hvol. congruence. eauto.
    }
    destruct K as ((((arg & g) & b) & i) & Hchunk & -> & Hbi & Hg & HL).
    exists (Vptr b i :: nil). split. vauto. split.
    + destruct (Senv.block_is_volatile ge b) eqn: Hvol.
      * set (k := match chunk with Mint8signed | Mint8unsigned | Mint16signed | Mint16unsigned | Mint32 | Many32 | Many64 => O | Mint64 => S O | Mfloat32 => S (S O) | Mfloat64 => S (S (S O)) end).
        eexists (match k with O => _ | S O => _ | S (S O) => _ | _ => _ end :: nil), (Val.load_result chunk match k with O => Vint Int.zero | S O => Vlong Int64.zero | S (S O) => Vsingle Floats.Float32.zero | _ => Vfloat Floats.Float.zero end), m.
        subst k. destruct chunk; econstructor; vauto; eq_some_inv; easy.
      * specialize (HL eq_refl). destruct HL as (v & HL).
        exists nil, v, m. vauto.
    + intros tr vres m' H1. inv H1. split. 2: discriminate.
      apply (A (Some _)).
      econstructor; eauto.
      intros Hchunk' tr0 vres0 g0 b0 ofs H1 H2 H3.
      inv H3; inv H7; clarify; try congruence; auto.
      destruct chunk; try easy; inv H8; eexists; (split; [ | split ] ); vauto; simpl; vauto; easy.

  - (* EF_vstore *)
    simpl in *.
    assert (A := ab_vstore_sound ge x None chunk args ab). rewrite H0 in A.
    clear H0.
    destruct s as [ | (t,e) s ].
    now destruct (H1 eq_refl); hsplit. clear H1.
    destruct (forall_existsx,
                    let '(addr, arg, b, i, g, v) := x in
                    args = addr :: arg :: nil
                    eval_expr ge e t m addr (Vptr b i) ∧
                    Genv.find_symbol ge g = Some b
                    eval_expr ge e t m arg v
                    (if Senv.block_is_volatile ge b
                     thenv', eventval_match ge v' (type_of_chunk chunk) (Val.load_result chunk v)
                     elsem', Mem.store chunk m b (Int.unsigned i) v = Some m')
             )) as [ K | K ].
    { destruct (A None); econstructor; eauto.
      intros ? g ? ? ? v.
      destruct args as [ | addr [ | arg' [ | ? ? ] ] ]; try (intros (); fail).
      intros [ -> K' ] G E VOL.
      elim (K (addr, arg, b, ofs, g, v)).
      repeat (apply conj; [ (assumption || reflexivity) | ]).
      inv VOL; clarify; vauto.
    }
    destruct K as ((((((addr & arg) & b) & ofs) & g) & v) & -> & Hvaddr & Hg & Hv & Hstore).
    exists ( Vptr b ofs :: v :: nil). split. vauto2.
    + destruct (Senv.block_is_volatile ge b) eqn: Hvol.
      * split.
        destruct Hstore as (v' & Hv').
        eexists (_ :: nil), Vundef, m. vauto.
        clear Hstore.
        intros tr vres m' H0. inv H0. inv H8. 2: congruence.
        split. 2: intro; eq_some_inv.
        apply (A (Some _)); clear A.
        econstructor; eauto.
        intros tr g0 b0 ofs0 arg0 v0 [ -> H4 ] H5 H6 H7.
        clarify; auto.
      * destruct Hstore as (m' & Hm').
        split.
        exists nil, Vundef, m'. vauto.
        split. 2: intro; eq_some_inv.
        apply (A (Some _)); clear A.
        econstructor; eauto.
        intros tr0 g0 b0 ofs0 arg0 v0 [ -> H2] H3 H4 H5.
        inv H0. inv H5; inv H12; clarify; intros; auto. congruence. determ. auto.
        repeat f_equal. congruence.

  - destruct args; try now inv H0.
    destruct args; try now inv H0.
    destruct s as [|[? e']]. destruct (H1 eq_refl). discriminate. clear H1.
    assert (A:=malloc_sound _ e x ab).
    simpl in H0. rewrite H0 in A.
    destruct (eval_expr_dec e' t m e) as [[varg VARG]|].
    destruct varg;
      try (destruct (A None); econstructor; eauto; intros; inv H2; determ; congruence).
    destruct (Mem.alloc m (-4) (Int.unsigned i)) eqn:?.
    destruct (Mem.store Mint32 m0 b (-4) (Vint i)) eqn:?.
    + refine (let A':=A _ _ in _).
      { econstructor. eauto.
        intros. inv H2. determ.
        replace b0 with b by congruence.
        replace m' with m1 by congruence. auto. }
      repeat (econstructor; try discriminate); eauto.
      intros. apply (A (Some _)).
      econstructor. eauto. inv H1.
      intros. determ. inv H2. repeat f_equal; congruence.
    + destruct (A None).
      econstructor; eauto. intros. inv H2. determ. congruence.
    + destruct (A None). econstructor. eauto.
      intros. edestruct H1; eauto.
  - destruct args; try now inv H0.
    destruct args; try now inv H0.
    destruct x; try now inv H0.
    assert (A:=free_sound _ e ab).
    simpl in H0. rewrite H0 in A.
    destruct s as [|[? e']]. destruct (H1 eq_refl). discriminate. clear H1.
    destruct (eval_expr_dec e' t m e) as [[varg VARG]|].
    destruct varg;
      try (destruct (A None); econstructor; eauto; intros; inv H2; determ; congruence).
    destruct (Mem.load Mint32 m b (Int.unsigned i - 4)) eqn:?.
    destruct v;
      try (destruct (A None); econstructor; eauto; intros; inv H2; determ; congruence).
    destruct (Z_gt_dec (Int.unsigned i0) 0).
    destruct (Mem.free m b (Int.unsigned i - 4) (Int.unsigned i + Int.unsigned i0)) eqn:?.
    + refine (let A':=A _ _ in _).
      { econstructor. eauto.
        intros. inv H2. determ. replace m' with m0 by congruence. auto. }
      repeat (econstructor; try discriminate); eauto.
      intros. apply (A (Some _)).
      econstructor. eauto. inv H1.
      intros. determ. inv H2. repeat f_equal; congruence.
    + destruct (A None).
      econstructor; eauto. intros. inv H2. determ. congruence.
    + destruct (A None).
      econstructor; eauto. intros. inv H2. determ.
      assert (i0 = sz) by congruence. subst. destruct n. auto.
    + destruct (A None).
      econstructor; eauto. intros. inv H2. determ. congruence.
    + destruct (A None). econstructor. eauto.
      intros. edestruct H1; eauto.
  - destruct args; try now inv H0.
    destruct args; try now inv H0.
    destruct args; try now inv H0.
    destruct x; try now inv H0.
    destruct s as [|[? e']]. destruct (H1 eq_refl). discriminate. clear H1.
    assert (A:=memcpy_sound _ sz al e e0 ab).
    simpl in H0. rewrite H0 in A.
    destruct (eval_expr_dec e' t m e) as [[varg0 VARG0]|].
    destruct (eval_expr_dec e' t m e0) as [[varg1 VARG1]|].
    destruct varg0;
      try (destruct (A None); econstructor; eauto; intros; inv H3; determ; congruence).
    destruct varg1;
      try (destruct (A None); econstructor; eauto; intros; inv H3; determ; congruence).
    destruct (Mem.loadbytes m b0 (Int.unsigned i0) sz) eqn:?.
    destruct (Mem.storebytes m b (Int.unsigned i) l) eqn:?.
    assert ((al = 1 ∨ al = 2 ∨ al = 4 ∨ al = 8) \/
            ~(al = 1 ∨ al = 2 ∨ al = 4 ∨ al = 8)) by omega.
    destruct H1.
    assert ((sz >= 0 /\ (al | sz) /\ (sz > 0 -> (al | Int.unsigned i0)) /\ (sz > 0 -> (al | Int.unsigned i))) \/
            ~(sz >= 0 /\ (al | sz) /\ (sz > 0 -> (al | Int.unsigned i0)) /\ (sz > 0 -> (al | Int.unsigned i))))
    by tauto.
    destruct H2.
    assert ((b0bInt.unsigned i0 = Int.unsigned i
            ∨ Int.unsigned i0 + sz <= Int.unsigned i
            ∨ Int.unsigned i + sz <= Int.unsigned i0) \/
           ~(b0bInt.unsigned i0 = Int.unsigned i
            ∨ Int.unsigned i0 + sz <= Int.unsigned i
            ∨ Int.unsigned i + sz <= Int.unsigned i0)) by tauto.
    destruct H3.
    + refine (let A':=A _ _ in _).
      { econstructor. eauto. intros. inv H6. determ. auto. }
      eexists. split. repeat econstructor; eauto.
      split. eexists. eexists. eexists.
      econstructor; eauto; try tauto.
      intros. split.
      apply (A (Some _)). econstructor. eauto. inv H4.
      intros. determ. inv H6. repeat f_equal; congruence.
      discriminate.
    + destruct (A None).
      econstructor; eauto. intros. inv H6. determ. congruence.
    + destruct (A None).
      econstructor; eauto. intros. inv H5. determ. destruct H2. auto.
    + destruct (A None).
      econstructor; eauto. intros. inv H4. destruct H1. auto.
    + destruct (A None).
      econstructor; eauto. intros. inv H3. determ. congruence.
    + destruct (A None).
      econstructor; eauto. intros. inv H3. determ. congruence.
    + destruct (A None). econstructor. eauto.
      intros. edestruct H1; eauto.
    + destruct (A None). econstructor. eauto.
      intros. edestruct H1; eauto.
  - (* EF_annot *)
    destruct s as [ | (t, e) s ]. specialize (H1 eq_refl). intuition. clear H1.
    generalize (type_check_list_sound t e s m _ H targs args).
    simpl in *.
    destruct x as [ x | ]. simpl in *. eq_some_inv.
    destruct (type_check_list _ _ _) as (() & [ | ? ? ]); simpl in *; eq_some_inv; subst.
    intros X; specialize (X eq_refl).
    destruct X as (vargs & evargs & Hv & Hev).
    exists vargs. split. exact Hv.
    split.
    eexists. exists Vundef. exists m.
    econstructor. exact Hev.
    intros tr vres m' H0. inv H0. simpl. split. easy. intro; eq_some_inv.
  - (* EF_annot_val *)
    destruct s as [ | (t, e) s ]. specialize (H1 eq_refl). intuition. clear H1.
    destruct args as [ | earg [ | ? ? ] ]; simpl in *; eq_some_inv.
    generalize (type_check_expr_sound t e s m _ H targ earg).
    destruct (type_check_expr _ _ _) as (() & [ | ? ? ]); destruct x as [ x | ];
    simpl in *; eq_some_inv; subst;
    [ | | destruct (assign _ _ _); eq_some_inv ];
    intros X; specialize (X eq_refl);
    destruct X as (ev & v & Hv & Hev);
    (exists (v :: nil); split; [ repeat (constructor (auto)) | split ];
            [ eexists _, v, m; econstructor; eauto |
              intros tr vres m' H1; inv H1; simpl; split; [ | intro; eq_some_inv ] ]).
    generalize (assign_sound ge x earg ab). rewrite H0.
    intros H1. eapply (H1 (Some _)).
    econstructor; eauto. now intros; determ.
    eauto.
  - (* EF_debug *)
    destruct s as [ | (t, e) s ]. specialize (H1 eq_refl). intuition. clear H1.
    destruct x as [ x | ]; simpl in *. eq_some_inv.
    revert H0. apply am_bind_case. discriminate.
    intros () NOERR ?; eq_some_inv. subst.
    assert (exists vargs, eval_exprlist ge e t m args vargs) as VARGS.
    {
      revert NOERR.
      induction args as [ | a args IH ] using rev_ind.
      vauto.
      rewrite am_fold_app. apply am_bind_case. discriminate.
      intros () Hargs. specialize (IH Hargs).
      unfold am_fold. simpl.
      generalize (noerror_sound ge a ab). destruct (noerror _ _) as (u & [ | ]).
      2: discriminate.
      intros NE ?; eq_some_inv; subst.
      destruct (forall_existsv, veval_expr ge e t m a)) as [ NV | (v & V) ];
        [
          destruct (NE None); econstructor; eauto;
          intros v V; elim (NV v V)
        | ].
      destruct IH as (vargs & IH).
      exists (vargs ++ v :: nil).
      clear -IH V.
      revert v V; induction IH; vauto.
    }
    destruct VARGS as (vargs & VARGS). exists vargs. split. exact VARGS.
    split.
    exists nil, Vundef, m. vauto.
    intros tr vres m' H0. inv H0. simpl. split. easy. intro; eq_some_inv.
Qed.

Section stmt_iterator_proof.

Variable iter_function:
  forall (sig:signature)
         (name: ident) (function:fundef) (rettemp:option ident)
         (args:list expr) (state:abstate), alarm_mon (abstate+⊥).
Variable rettemp: option ident.
Variable env : env.
Variable stk : list (temp_env * Csharpminor.env).

Definition pred_of_ab (ab:abstate+⊥) (le:temp_env) (mem:mem) : Prop :=
  ((le, env) :: stk, mem) ∈ γ ab.

Existing Instance join_mem_correct.

Lemma join_pred_of_ab:
  ∀ ab1 ab2 le mem,
    pred_of_ab ab1 le mem \/ pred_of_ab ab2 le mem ->
    pred_of_ab (ab1ab2) le mem.
Proof.
  unfold pred_of_ab. intros ab1 ab2 le mem; apply join_correct.
Qed.

Definition exit_pred_of_ab (ab:list (abstate+⊥)) (x:nat) : temp_env -> mem -> Prop :=
  pred_of_ab (nth x ab Bot).

Lemma join_exit_pred_of_ab:
  ∀ ab1 ab2 le mem x,
    exit_pred_of_ab ab1 x le mem \/ exit_pred_of_ab ab2 x le mem ->
    exit_pred_of_ab (join_exit ab1 ab2) x le mem.
Proof.
  intros ab1 ab2 le mem x. revert x ab1 ab2 le mem.
  induction x; destruct ab1, ab2;
    try (apply IHx; now auto);
    try (apply join_pred_of_ab; now auto);
    intros le mem [H|H];
    now auto || now destruct H.
Qed.

Definition ret_pred_of_ab (ab:abstate+⊥) (v:val) (mem:mem) : Prop :=
  match stk with
  | nil => (nil, mem) ∈ γ ab /\ ∃ r, v = Vint r
  | (le', e') :: stk' =>
    ((Cminor.set_optvar rettemp v le', e') :: stk', mem) ∈ γ ab
  end.

Lemma join_ret_pred_of_ab:
  ∀ ab1 ab2 v mem,
    ret_pred_of_ab ab1 v mem \/ ret_pred_of_ab ab2 v mem ->
    ret_pred_of_ab (ab1ab2) v mem.
Proof.
  unfold ret_pred_of_ab.
  intros ab1 ab2 v mem [AB|AB]; destruct stk as [|[le' e']].
  - destruct AB. split. apply join_correct. auto. auto.
  - apply join_correct. auto.
  - destruct AB. split. apply join_correct. auto. auto.
  - apply join_correct. auto.
Qed.

Definition goto_pred_of_ab (ab:PTree.t abstate) (lbl:ident): temp_env -> mem -> Prop :=
  pred_of_ab
    match ab!lbl with
      | Some a => NotBot a
      | None => Bot
    end.

Lemma join_goto_pred_of_ab:
  ∀ ab1 ab2 lbl le mem,
    goto_pred_of_ab ab1 lbl le mem \/ goto_pred_of_ab ab2 lbl le mem ->
    goto_pred_of_ab (join_goto ab1 ab2) lbl le mem.
Proof.
  unfold join_goto, goto_pred_of_ab. intros. rewrite PTree.gcombine by auto.
  destruct PTree.get, PTree.get.
  apply join_pred_of_ab in H. unfold join in H. simpl in H. destruct (aa0); auto.
  destruct H as [? | []]. auto.
  destruct H as [[] | ?]. auto.
  destruct H as [[]|[]].
Qed.

Hypothesis iter_function_ok:
  ∀ sig name fundef rettemp args i o,
    iter_function sig name fundef rettemp args i = (o, nil) ->
  ∀ le mem, pred_of_ab (NotBot i) le mem ->
    ∃ vargs,
      eval_exprlist ge env le mem args vargs /\
      funsig fundef = sig /\
      hoare_fun prog
                (fun vargs' mem' => vargs = vargs' /\ mem = mem')
                fundef
                (fun ret mem' =>
                   pred_of_ab o (Cminor.set_optvar rettemp ret le) mem').

Section pfp.

Variable igoto:PTree.t abstate.
Variable s:stmt.
Variable it:abstate +⊥ → alarm_mon (@outcome abstate).
Variable low:abstate +⊥.

Hypothesis it_ok:
  ∀ ab o,
    it ab = (o, nil) ->
    hoare_stmt prog env
               (pred_of_ab ab) (goto_pred_of_ab igoto)
               s
               (pred_of_ab o.(onormal)) (ret_pred_of_ab o.(oreturn))
               (exit_pred_of_ab o.(oexit)) (goto_pred_of_ab o.(ogoto)).

Lemma pfp_widen_ok:
  ∀ fuel f x y o,
    pfp_widen fuel f x y = (o, nil) ->
    ∃ x0, f x0 = (o, nil) /\
          γ (y, x) ⊆ γ x0 /\
          γ o.(onormal) ⊆ γ x0.
Proof.
  induction fuel; simpl; intros.
  - destruct (f x). discriminate.
  - pose proof leb_correct ((fst (f x)).(onormal)) x.
    destruct @leb.
    + rewrite H in H0. simpl in *. eexists. split; eauto. split; eauto. intro; apply proj2.
    + pose proof widen_incr y (fst (f x)).(onormal). destruct @widen.
      apply IHfuel in H. destruct H as (? & ? & ? & ?).
      eexists. split; eauto. split; eauto. intros. apply H2, H1, H4.
Qed.

Definition is_invariant o :=
  loop_unstable_invariant prog env
                          (fun le mem => pred_of_ab low le mem \/ pred_of_ab o.(onormal) le mem)
                          (pred_of_ab low) (goto_pred_of_ab igoto)
                          s
                          (ret_pred_of_ab o.(oreturn))
                          (exit_pred_of_ab o.(oexit)) (goto_pred_of_ab o.(ogoto)).

Lemma pfp_narrow_ok:
  ∀ n ab o,
    pfp_narrow it low n ab = (o, nil) ->
    (∀ o', ab = (o', nil) -> is_invariant o') ->
    is_invariant o.
Proof.
  induction n; intros. apply H0; auto. simpl in H.
  destruct @is_bot in H. apply H0; auto.
  destruct ab as [o' [|]];
    destruct (it (lowo'.(onormal))) as [o'' [|]] eqn:eqo'';
    simpl in H; rewrite eqo'' in H; simpl in H.
  - eapply IHn. eauto. intros. inv H1.
    eapply loop_unstable_invariant_seq. 3:now auto. apply H0, eq_refl.
    eapply hoare_stmt_post_impl, hoare_stmt_pre_impl, it_ok, eqo''; auto.
    apply join_pred_of_ab.
  - auto.
  - pose proof leb_correct o''.(onormal) o'.(onormal). destruct @leb. 2:discriminate.
    eapply IHn. eauto. intros. inv H2. eexists. split. exact (fun le mem H => H). split. auto.
    eapply hoare_stmt_post_impl, hoare_stmt_pre_impl, it_ok, eqo''; auto.
    intros. apply join_pred_of_ab. destruct H2. auto. right. apply H1; auto.
  - eapply IHn. eauto. discriminate.
Qed.

Lemma pfp_ok:
  ∀ o, pfp it low = (o, nil) -> is_invariant o.
Proof.
  unfold pfp. intros. apply pfp_narrow_ok in H. auto.
  intros. apply pfp_widen_ok in H0.
  destruct H0 as (? & ? & ? & ?). eexists. split. exact (fun le mem H => H). split. auto.
  eapply hoare_stmt_post_impl, hoare_stmt_pre_impl, it_ok, H0; auto.
  intros. destruct H3; auto. apply H1. split; auto. apply init_iter_correct, H3. apply H2, H3.
Qed.

End pfp.

Section pfp_goto.

Variable inormal:abstate+⊥.
Variable it:PTree.t abstatealarm_mon (@outcome abstate).
Variable body: stmt.

Hypothesis it_ok:
  ∀ ab o,
    it ab = (o, nil) ->
    hoare_stmt prog env
               (pred_of_ab inormal) (goto_pred_of_ab ab)
               body
               (pred_of_ab o.(onormal)) (ret_pred_of_ab o.(oreturn))
               (exit_pred_of_ab o.(oexit)) (goto_pred_of_ab o.(ogoto)).

Definition is_goto_invariant o :=
  ∃ inv,
    (∀ lbl le mem, (inv lbl le mem:Prop) -> goto_pred_of_ab o.(ogoto) lbl le mem) /\
    hoare_stmt prog env
               (pred_of_ab inormal) inv
               body
               (pred_of_ab o.(onormal)) (ret_pred_of_ab o.(oreturn))
               (exit_pred_of_ab o.(oexit)) inv.

Definition incl_goto (a b:PTree.t abstate) :=
  ∀ l,
    match a!l with
      | None => True
      | Some a' =>
        match b!l with
          | None => False
          | Some b' => γ a' ⊆ γ b'
        end
    end.

Lemma leb_goto_incl_goto:
  ∀ a b, leb_goto a b = true -> incl_goto a b.
Proof.
  intros.
  unfold leb_goto in H. rewrite PTree.bempty_correct in H.
  intro. specialize (H l).
  rewrite PTree.gcombine in H by easy.
  edestruct PTree.get; try easy.
  edestruct PTree.get; try easy.
  eapply leb_correct. destruct (a0a1) eqn:?; congruence.
Qed.

Lemma pfp_widen_goto_ok:
  ∀ fuel f x y o,
    pfp_widen_goto fuel f x y = (o, nil) ->
    ∃ x0, f x0 = (o, nil) /\ incl_goto o.(ogoto) x0.
Proof.
  Opaque widen_goto. induction fuel; simpl; intros.
  - destruct (f x). discriminate.
  - pose proof leb_goto_incl_goto ((fst (f x)).(ogoto)) x. destruct leb_goto.
    + rewrite H in H0. simpl in *. eauto.
    + destruct widen_goto. eauto.
Qed.

Lemma pfp_narrow_goto_ok:
  ∀ n ab o,
    pfp_narrow_goto it n ab = (o, nil) ->
    (∀ o', ab = (o', nil) -> is_goto_invariant o') ->
    is_goto_invariant o.
Proof.
  induction n; intros. apply H0; auto. simpl in H.
  destruct (leb_goto ((fst ab).(ogoto)) bot_goto) eqn:?.
  apply H0; auto.
  destruct ab as [o' [|]]; simpl in H;
  destruct (it o'.(ogoto)) as [o'' [|]] eqn:eqo'';
  simpl in H.
  - eapply IHn. eauto. intros.
    edestruct H0 as (inv & invle & INV). eauto. clear H0.
    inv H1. eexists. split.
    2:eapply hoare_stmt_post_impl, hoare_stmt_post_and, hoare_stmt_pre_impl, INV; eauto.
    5:eapply hoare_stmt_pre_impl, it_ok, eqo''.
    now intuition. now intuition. now intuition. now intuition. now auto.
    destruct 1. auto using join_pred_of_ab. now intuition.
  - inv H. eauto.
  - pose proof leb_goto_incl_goto o''.(ogoto) o'.(ogoto). clear Heqb. destruct leb_goto.
    2:discriminate.
    eapply IHn. eauto. intros. inv H2. eexists. split. eauto.
    eapply hoare_stmt_pre_impl, it_ok, eqo''; auto.
    intros. specialize (H1 eq_refl lbl). unfold goto_pred_of_ab in *.
    destruct PTree.get, PTree.get; try contradiction; auto. apply H1, H2.
  - eapply IHn. eauto. discriminate.
Qed.

Lemma pfp_goto_ok:
  ∀ o, pfp_goto it = (o, nil) -> is_goto_invariant o.
Proof.
  unfold pfp_goto. intros. apply pfp_narrow_goto_ok in H. auto.
  intros. apply pfp_widen_goto_ok in H0. destruct H0 as (? & ? & ?).
  exists (goto_pred_of_ab o'.(ogoto)). split. auto.
  eapply hoare_stmt_pre_impl, it_ok, H0. now auto.
  unfold goto_pred_of_ab, pred_of_ab. intros. specialize (H1 lbl).
  destruct PTree.get, PTree.get; try contradiction. apply H1, H2.
Qed.

End pfp_goto.

Lemma iter_ok:
  ∀ s inormal igoto o,
    iter unroll iter_function rettemp inormal igoto s = (o, nil) ->
    hoare_stmt prog env
               (pred_of_ab inormal) (goto_pred_of_ab igoto)
               s
               (pred_of_ab o.(onormal)) (ret_pred_of_ab o.(oreturn))
               (exit_pred_of_ab o.(oexit)) (goto_pred_of_ab o.(ogoto))
with iter_switch_ok:
  ∀ lbl_s islong inormal idefault iprev igoto e o,
    iter_switch unroll iter_function rettemp islong inormal
                idefault iprev igoto e lbl_s = (o, nil) ->
    hoare_lbl_stmt prog env
                   (fun n le mem =>
                      eval_expr ge env le mem e
                                (if islong then Vlong (Int64.repr n)
                                 else Vint (Int.repr n)) /\
                      pred_of_ab inormal le mem)
                   (pred_of_ab idefault) (pred_of_ab iprev)
                   (goto_pred_of_ab igoto)
                   lbl_s
                   (pred_of_ab o.(onormal)) (ret_pred_of_ab o.(oreturn))
                   (exit_pred_of_ab o.(oexit)) (goto_pred_of_ab o.(ogoto)).
Proof.
  2:destruct lbl_s; intros.
  destruct s; intros.
  - (* Sskip *)
    clear iter_ok iter_switch_ok.
    inv H. apply hoare_Sskip. auto.
  - (* Sset *)
    clear iter_ok iter_switch_ok.
    apply hoare_Sset. intros le mem AB.
    destruct inormal as [|inormal]. contradiction.
    revert H. unfold iter. simpl. apply am_bind_case. discriminate.
    intros out OUT eq. inv eq.
    assert (A:=assign_sound ge i e inormal). rewrite OUT in A.
    destruct (eval_expr_dec env le mem e) as [[v Hv]|].
    + eexists. split. eauto. apply (A (Some _)). econstructor; eauto. intros. determ. auto.
    + destruct (A None). econstructor; eauto. intros. edestruct H. eauto.
  - (* Sstore*)
    clear iter_ok iter_switch_ok.
    apply hoare_Sstore. intros le mem AB.
    destruct inormal as [|inormal]. contradiction.
    revert H. unfold iter. simpl. apply am_bind_case. discriminate.
    intros out OUT eq. inv eq.
    assert (S:=store_sound ge m e e0 inormal). rewrite OUT in S.
    destruct (eval_expr_dec env le mem e) as [[v Hv]|].
    destruct (eval_expr_dec env le mem e0) as [[v0 Hv0]|].
    destruct (Mem.storev m mem v v0) eqn:?.
    + eexists. eexists. eexists. split. eauto. split. eauto. split. eauto.
      apply (S (Some _)). econstructor; eauto. intros. determ. auto.
    + destruct (S None). econstructor; eauto. intros. determ. congruence.
    + destruct (S None). econstructor; eauto. intros. edestruct H. eauto.
    + destruct (S None). econstructor; eauto. intros. edestruct H. eauto.
  - (* Scall*)
    clear iter_ok iter_switch_ok.
    apply hoare_Scall. intros le mem AB.
    destruct inormal as [|inormal]. contradiction.
    revert H. unfold iter, bind_normal_outcome.
    apply am_bind_case. discriminate. intros out1 OUT1 eq. inv eq.
    revert OUT1. apply am_bind_case. discriminate. intros out2 OUT1 OUT2.
    assert (D:=deref_fun_sound ge e inormal). rewrite OUT1 in D.
    destruct (eval_expr_dec env le mem e) as [[vf Hvf]|].
    destruct (Genv.find_funct (Genv.globalenv prog) vf) eqn:?.
    destruct vf; try discriminate.
    destruct (Genv.invert_symbol ge b) eqn:?. apply Genv.invert_find_symbol in Heqo1.
    destruct (Int.eq_dec i Int.zero). subst i.
    + assert (In (i0,f) out2).
      { apply (D (Some _)). econstructor; eauto. intros. determ. auto. }
      rewrite <- fold_left_rev_right in OUT2.
      rewrite in_rev in H. clear OUT1 D.
      revert out1 OUT2. induction (rev out2). contradiction.
      unfold fold_right.
      apply am_bind_case. discriminate. intros out1 OUT1.
      apply am_bind_case. discriminate. intros out3 OUT3.
      intros out4 eq. simpl in eq. apply pair_eq_inv in eq. destruct eq. subst.
      destruct H.
      * subst. edestruct iter_function_ok as (vargs & VARGS & SIG & HOARE); eauto.
        eexists. eexists. eexists. split. eauto. split. eauto. split. eauto. split. eauto.
        eapply hoare_fun_post_impl, HOARE. eauto using join_pred_of_ab.
      * edestruct IHl0 as (vf & vargs & fd & EVAL & EVALS & FIND & SIG & HOARE); eauto.
        eexists. eexists. eexists. split. eauto. split. eauto. split. eauto. split. eauto.
        eapply hoare_fun_post_impl, HOARE. eauto using join_pred_of_ab.
    + destruct (D None). econstructor; eauto.
      intros. determ. congruence.
    + destruct (D None). econstructor; eauto.
      intros. apply Genv.find_invert_symbol in H1. determ. congruence.
    + destruct (D None). econstructor; eauto.
      intros. determ. subst. simpl in Heqo0.
      unfold ge in H0. destruct Int.eq_dec; try congruence.
    + destruct (D None). econstructor; eauto.
      intros. edestruct H; eauto.
  - (* Sbuiltin *)
    clear iter_ok iter_switch_ok.
    apply hoare_Sbuiltin. intros le mem AB.
    destruct inormal as [|inormal]. contradiction.
    unfold iter, bind_normal_outcome in H.
    revert H. apply am_bind_case. discriminate. intros out1 OUT1 eq. inv eq.
    edestruct ab_builtin_sound as (vargs & VARGS & exEXTCALL & EXTCALL); eauto. discriminate.
    eexists. split. apply VARGS. split. auto.
    eapply EXTCALL.
  - (* Sseq *)
    assert (IHs1:=iter_ok s1). assert (IHs2:=iter_ok s2).
    clear iter_ok iter_switch_ok.
    revert H. unfold iter.
    apply am_bind_case. discriminate. intros out1 OUT1.
    apply am_bind_case. discriminate. intros out2 OUT2.
    intros eq. simpl in eq. apply pair_eq_inv in eq. destruct eq. subst.
    eapply hoare_Sseq;
      [eapply hoare_stmt_post_impl, IHs1, OUT1 |
       eapply hoare_stmt_post_impl, IHs2, OUT2]; eauto.
    + eauto using join_ret_pred_of_ab.
    + eauto using join_exit_pred_of_ab.
    + eauto using join_goto_pred_of_ab.
    + eauto using join_ret_pred_of_ab.
    + eauto using join_exit_pred_of_ab.
    + eauto using join_goto_pred_of_ab.
  - (* Sifthenelse *)
    assert (IHs1:=iter_ok s1). assert (IHs2:=iter_ok s2).
    clear iter_ok iter_switch_ok.
    revert H. unfold iter.
    apply am_bind_case. discriminate. intros [out1t out1f] OUT1.
    apply am_bind_case. discriminate. intros out2 OUT2.
    apply am_bind_case. discriminate. intros out3 OUT3.
    intros eq. simpl in eq. apply pair_eq_inv in eq. destruct eq. subst.
    eapply hoare_Sifthenelse;
      [|eapply hoare_stmt_post_impl, IHs1, OUT2 |
        eapply hoare_stmt_post_impl, IHs2, OUT3]; eauto.
    + intros le mem AB. destruct inormal as [|inormal]. contradiction.
      assert (A:=assume_sound ge e inormal). rewrite OUT1 in A.
      destruct (eval_expr_dec env le mem e) as [[v Hv]|].
      assert ((exists b, Val.bool_of_val v b) \/ (∀ b, ~Val.bool_of_val v b)).
      { destruct v; try now (right; repeat intro; inv H0). repeat econstructor. }
      destruct H as [[b Hb]|].
      * eexists. eexists. split. eauto. split. eauto.
        assert (A':=fun cs => A (Some (b, cs))). clear A.
        destruct b; apply A'; (econstructor; [eauto|intros; determ; auto]).
      * destruct (A None). econstructor; eauto.
        intros. determ. edestruct H. eauto.
      * destruct (A None). econstructor; eauto.
        intros. edestruct H. eauto.
    + eauto using join_pred_of_ab.
    + eauto using join_ret_pred_of_ab.
    + eauto using join_exit_pred_of_ab.
    + eauto using join_goto_pred_of_ab.
    + eauto using join_pred_of_ab.
    + eauto using join_ret_pred_of_ab.
    + eauto using join_exit_pred_of_ab.
    + eauto using join_goto_pred_of_ab.
  - (* Sloop *)
    assert (IHs:=iter_ok s).
    clear iter_ok iter_switch_ok iter_function_ok.
    revert H. unfold iter.
    revert inormal igoto o. generalize (unroll_call_lookup s unroll).
    induction n; intros inormal igoto o.
    + apply am_bind_case; try discriminate.
      intros out OUT eq. inv eq. simpl. eapply hoare_Sloop_unstable, pfp_ok, OUT. auto.
    + apply am_bind_case. discriminate. intros out1 OUT1.
      destruct out1.(onormal) eqn:E.
      * intros Hr; inv Hr. clear IHn. simpl.
        eapply hoare_Sloop, hoare_stmt_post_impl, IHs, OUT1; auto.
        rewrite E. contradiction.
      * apply am_bind_case. discriminate. intros out2 OUT2.
        intros Hr; inv Hr. simpl.
        eapply hoare_loop_pre_unroll; eapply hoare_stmt_post_impl.
        5:apply IHs, OUT1; eauto.
        9:eapply hoare_stmt_pre_impl, IHn, OUT2; eauto.
        assert (IHnn:=IHn _ _ _ OUT2). clear IHn OUT2.
        intros. congruence.
        intros. apply join_ret_pred_of_ab. auto.
        intros. apply join_exit_pred_of_ab. auto.
        intros. apply join_goto_pred_of_ab. auto.
        auto.
        intros. apply join_ret_pred_of_ab. auto.
        intros. apply join_exit_pred_of_ab. auto.
        intros. apply join_goto_pred_of_ab. auto.
        contradiction.
  - (* Sblock *)
    assert (IHs:=iter_ok s).
    clear iter_ok iter_switch_ok.
    revert H. unfold iter.
    apply am_bind_case. discriminate. intros out OUT.
    intros eq. simpl in eq. apply pair_eq_inv in eq. destruct eq. subst.
    eapply hoare_Sblock, hoare_stmt_post_impl, IHs, OUT.
    + eauto using join_pred_of_ab.
    + auto.
    + intros [|x].
      intros le mem CS. apply join_pred_of_ab. destruct out.(oexit); auto.
      unfold oexit at 2. destruct out.(oexit), x; auto.
    + auto.
  - (* Sexit *)
    clear iter_ok iter_switch_ok.
    apply hoare_Sexit. inv H. simpl.
    clear; induction n; auto.
  - (* Sswitch *)
    assert (IHlbl_s:=iter_switch_ok l b).
    clear iter_ok iter_switch_ok.
    revert H. unfold iter.
    apply am_bind_case. discriminate. intros out1 OUT1 OUT1'.
    eapply hoare_Sswitch, hoare_lbl_stmt_pre_impl, IHlbl_s, OUT1'; eauto.
    intros. destruct inormal. contradiction.
    revert OUT1. apply am_bind_case. discriminate. intros out2 OUT2 OUT2'.
    assert (N:=noerror_sound ge (Eunop (if b then Cminor.Onegl else Cminor.Onegint) e) x). rewrite OUT2 in N.
    destruct (eval_expr_dec env le mem e) as [[v Hv]|].
    assert ((∃ n, Switch.switch_argument b v n) \/ (∀ n, ~Switch.switch_argument b v n)).
    { destruct b, v; try (left; eexists; constructor); right; intros n Hn; inv Hn. }
    destruct H0 as [[n Hn]|?].
    + eexists. eexists. split. eauto. split. eauto. split.
      * destruct Hn; rewrite ?Int.repr_unsigned, ?Int64.repr_unsigned; auto.
      * clear - mem_spec OUT2' Hv Hn H.
        revert x out1 OUT2' H. induction l; intros. inv OUT2'. auto.
        destruct o. 2:inv OUT2'; now eauto.
        simpl in OUT2', H0. destruct zeq. discriminate. pose proof (IHl x).
        destruct zlt. simpl in OUT2'. now eauto.
        destruct zlt. simpl in OUT2'. now eauto. simpl in OUT2'.
        revert OUT2'. apply am_bind_case. discriminate. intros [outt outf] OUT.
        assert (A:=assume_sound ge
          (if b then Ebinop (Cminor.Ocmpl Ceq) e (Econst (Olongconst (Int64.repr z)))
           else Ebinop (Cminor.Ocmp Ceq) e (Econst (Ointconst (Int.repr z)))) x).
        rewrite OUT in A.
        assert (((le, env) :: stk, mem) ∈ γ outf).
        { apply (A (Some (false, _))). econstructor; eauto.
          intros. destruct Hn.
          - inv H3. inv H10. inv H9. inv H4. inv H2. determ.
            unfold Val.cmp, Val.cmp_bool, Int.cmp in H4.
            pose proof (Int.eq_spec i (Int.repr z)). destruct Int.eq.
            subst i. rewrite Int.unsigned_repr in n0. congruence. omega.
            inv H4. auto.
          - inv H3. inv H9. inv H4. inv H10. determ. inv H4.
            pose proof (Int64.eq_spec i (Int64.repr z)). destruct Int64.eq.
            subst i. rewrite Int64.unsigned_repr in n0. congruence. omega.
            inv H2. auto. }
        destruct outf. contradiction. eauto.
    + destruct (N None). econstructor; eauto.
      intros. inv H1. determ.
      destruct b, v; inv H7; try congruence; edestruct H0; constructor.
    + destruct (N None). econstructor; eauto.
      intros. inv H1. edestruct H0. eauto.
  - (* Sreturn *)
    clear iter_ok iter_switch_ok. constructor.
    intros le mem AB. destruct inormal as [|inormal]. contradiction.
    revert H. unfold iter. apply am_bind_case. discriminate. intros out OUT eq. inv eq.
    assert (P:=pop_frame_sound ge o rettemp inormal). rewrite OUT in P.
    assert ((∃ v, match o with
                  | Some a => eval_expr (Genv.globalenv prog) env le mem a v
                  | None => v = Vundef
                  end) \/
            (∃ a, o = Some a /\ ∀ v, ~eval_expr (Genv.globalenv prog) env le mem a v)).
    { destruct o. destruct (eval_expr_dec env le mem e) as [[v Hv]|]; eauto. eauto. }
    destruct H as [(v & Hv)|(a & -> & H)].
    destruct (Mem.free_list mem (blocks_of_env env)) as [mem0|] eqn:MEM.
    + eexists. eexists. split. eauto. split. eauto. simpl.
      unfold ret_pred_of_ab, pred_of_ab in AB|-*. destruct stk as [|(le' & e')].
      { split. apply (P (Some _)). econstructor; eauto.
        simpl. intros. repeat f_equal. congruence.
        destruct rettemp as [[]|], v; eauto; destruct (P None);
        econstructor; eauto; simpl; intros; destruct o; determ; congruence. }
      { apply (P (Some _)). econstructor; eauto.
        simpl. intros. destruct o; determ; auto. repeat f_equal. congruence. }
    + destruct (P None). econstructor; eauto. congruence.
    + destruct (P None). econstructor; eauto. intros. edestruct H; eauto.
  - (* Slabel *)
    assert (IHs:=iter_ok s).
    clear iter_ok iter_switch_ok.
    eapply hoare_Slabel, hoare_stmt_pre_impl, IHs, H.
    + intros le mem HH. apply join_pred_of_ab. destruct HH; auto.
    + auto.
  - (* Sgoto *)
    clear iter_ok iter_switch_ok.
    eapply hoare_Sgoto. inv H. unfold ogoto at 1.
    destruct inormal as [|inormal]. contradiction.
    unfold goto_pred_of_ab. rewrite PTree.gss. auto.
  - (* LSnil *)
    clear iter_ok iter_switch_ok. inv H. subst.
    apply hoare_LSnil; eauto using join_pred_of_ab.
  - (* LScons *)
    assert (IHs:=iter_ok s). assert (IHlbl_s:=iter_switch_ok lbl_s islong).
    clear iter_ok iter_switch_ok.
    revert H. unfold iter_switch.
    apply am_bind_case. discriminate. intros [icase' idefault'] OUT1.
    apply am_bind_case. discriminate. intros out2 OUT2.
    apply am_bind_case. discriminate. intros out3 OUT3.
    intros eq. simpl in eq. apply pair_eq_inv in eq. destruct eq. subst.
    destruct o; revert OUT1.
    + apply am_bind_case. discriminate. intros out4 OUT4.
      intros eq. simpl in eq. apply triple_eq_inv in eq. destruct eq as [[? ?] _]. subst.
      econstructor;
        [eapply hoare_stmt_post_impl, hoare_stmt_pre_impl, IHs, OUT2 |
         eapply hoare_lbl_stmt_post_impl, IHlbl_s, OUT3]; eauto.
      * eauto using join_ret_pred_of_ab.
      * eauto using join_exit_pred_of_ab.
      * intros. apply join_goto_pred_of_ab. auto.
      * intros le mem [[EVAL AB]|AB]; apply join_pred_of_ab; auto.
        right.
        destruct inormal. contradiction.
        revert OUT4. apply am_bind_case. discriminate.
        intros [icase idummy] OUT eq. inv eq.
        assert (A:=assume_sound ge
          (if islong then Ebinop (Cminor.Ocmpl Ceq) e (Econst (Olongconst (Int64.repr z)))
           else Ebinop (Cminor.Ocmp Ceq) e (Econst (Ointconst (Int.repr z))))
          x (Some (true, ((le, env)::stk, mem)))).
        rewrite OUT in A. apply A.
        econstructor; eauto.
        intros. destruct islong.
        inv H1. inv H7. inv H2. inv H8. determ.
        unfold Val.cmpl, Val.cmpl_bool, Int64.cmp in H2. rewrite Int64.eq_true in H2.
        inv H2. inv H. auto.
        inv H1. inv H7. inv H2. inv H8. determ.
        unfold Val.cmp, Val.cmp_bool, Int.cmp in H. rewrite Int.eq_true in H. inv H. auto.
      * eauto using join_ret_pred_of_ab.
      * eauto using join_exit_pred_of_ab.
      * intros. apply join_goto_pred_of_ab. auto.
    + intros eq. simpl in eq. apply triple_eq_inv in eq. destruct eq as [[? ?] _]. subst.
      econstructor;
        [eapply hoare_stmt_post_impl, hoare_stmt_pre_impl, IHs, OUT2|
         eapply hoare_lbl_stmt_post_impl, hoare_lbl_stmt_pre_impl, IHlbl_s, OUT3]; eauto.
      * eauto using join_ret_pred_of_ab.
      * eauto using join_exit_pred_of_ab.
      * eauto using join_goto_pred_of_ab.
      * intros. apply join_pred_of_ab. intuition.
      * eauto using join_ret_pred_of_ab.
      * eauto using join_exit_pred_of_ab.
      * eauto using join_goto_pred_of_ab.
Qed.

End stmt_iterator_proof.

Lemma labels_stmt_ok:
  ∀ lbl s k,
    (labels_stmt s) ! lbl = Some tt ->
    ∃ sk, find_label lbl s k = Some sk
with labels_sl_ok:
  ∀ lbl sl k,
    (labels_sl sl) ! lbl = Some tt ->
    ∃ sk, find_label_ls lbl sl k = Some sk.
Proof.
{ destruct s; simpl; intros k Hlbl;
  try (rewrite PTree.gempty in Hlbl; discriminate);
  try (rewrite PTree.gcombine in Hlbl by auto).
  - destruct ((labels_stmt s1)!lbl) as [[]|] eqn:?.
    pose proof (labels_stmt_ok lbl s1 (Kseq s2 k)).
    edestruct H as [sk Hsk]; auto. rewrite Hsk. eauto.
    pose proof (labels_stmt_ok lbl s2 k).
    destruct ((labels_stmt s2)!lbl) as [[]|]. 2:discriminate.
    edestruct H as [sk Hsk]; auto. rewrite Hsk.
    destruct (find_label lbl s1 (Kseq s2 k)) as [[]|]; eauto.
  - destruct ((labels_stmt s1)!lbl) as [[]|] eqn:?.
    pose proof (labels_stmt_ok lbl s1 k).
    edestruct H as [sk Hsk]; auto. rewrite Hsk. eauto.
    pose proof (labels_stmt_ok lbl s2 k).
    destruct ((labels_stmt s2)!lbl) as [[]|]. 2:discriminate.
    edestruct H as [sk Hsk]; auto. rewrite Hsk.
    destruct (find_label lbl s1 k) as [[]|]; eauto.
  - eapply (labels_stmt_ok lbl s). auto.
  - eapply (labels_stmt_ok lbl s). auto.
  - eapply (labels_sl_ok lbl l). auto.
  - unfold ident_eq. rewrite PTree.gsspec in Hlbl.
    destruct peq. eauto.
    eapply (labels_stmt_ok lbl s). auto.
}
{ destruct sl; simpl.
  - rewrite PTree.gempty. discriminate.
  - rewrite PTree.gcombine by auto. intros.
    destruct ((labels_stmt s)!lbl) as [[]|] eqn:?.
    pose proof (labels_stmt_ok lbl s (Kseq (seq_of_lbl_stmt sl) k)).
    edestruct H0 as [sk Hsk]; auto. rewrite Hsk. eauto.
    pose proof (labels_sl_ok lbl sl k).
    destruct ((labels_sl sl)!lbl) as [[]|]. 2:discriminate.
    edestruct H0 as [sk Hsk]; auto. rewrite Hsk.
    destruct (find_label lbl s (Kseq (seq_of_lbl_stmt sl) k)) as [[]|]; eauto.
}
Qed.

Lemma iter_function_ok :
  ∀ fuel sig name fundef rettemp args i o,
    iter_function unroll fuel sig name fundef rettemp args i = (o, nil) ->
  ∀ stk mem,
    match stk with
      | nil => (nil, mem) ∈ γ i /\
               sig = (mksignature nil (Some AST.Tint) cc_default) /\
               match fundef with External (EF_external _ _) | Internal _ => True | _ => False end
               args = nil
      | (le, env)::stk => pred_of_ab env stk (NotBot i) le mem
    end ->
    ∃ vargs,
      match stk with
        | nil => vargs = nil
        | (le, env)::_ => eval_exprlist ge env le mem args vargs
      end /\
      funsig fundef = sig /\
      hoare_fun prog
                (fun vargs' mem' => vargs = vargs' /\ mem = mem')
                fundef
                (fun ret mem' =>
                   match stk with
                     | nil =>
                       (nil, mem') ∈ γ o /\ ∃ r, ret = Vint r
                     | (le, env)::stk =>
                       pred_of_ab env stk o (Cminor.set_optvar rettemp ret le) mem'
                   end).
Proof.
  induction fuel. discriminate.
  Opaque join. simpl. Transparent join.
  intros*. destruct signature_eq. 2:discriminate.
  destruct fundef.
  - apply am_bind_case. discriminate. intros out1 OUT1.
    apply am_bind_case. discriminate. intros out2 OUT2.
    apply am_bind_case. discriminate. intros out3 OUT3.
    apply am_bind_case. discriminate. intros out4 OUT4.
    apply am_bind_case. discriminate. intros out5 OUT5.
    apply am_bind_case. discriminate. intros out6 OUT6.
    apply am_bind_case. discriminate. intros out7 OUT7.
    apply am_bind_case. discriminate. intros out8 OUT8.
    intros eq. apply pair_eq_inv in eq. destruct eq. subst.
    destruct list_norepet_dec; inv OUT1.
    destruct list_norepet_dec; inv OUT2.
    destruct list_disjoint_dec; inv OUT3.
    destruct out5.(oexit) eqn:?; inv OUT6.
    intros.
    assert (P:=push_frame_sound ge f args i). rewrite OUT4 in P.
    destruct (Classical_Prop.classic
                (exists vargs,
                   match stk with
                     | nil => vargs = nil
                     | (le, env) :: _ => eval_exprlist ge env le mem args vargs
                   end)) as [[vargs VARGS]|].
    destruct (Classical_Prop.classic
                (exists mem1 env le,
                   alloc_variables empty_env mem f.(fn_vars) env mem1 /\
                   bind_parameters f.(fn_params) vargs (create_undef_temps f.(fn_temps)) = Some le)) as [(mem1 & env & le & ALLOC & BIND)|].
    + eexists. split. eauto. split. auto.
      apply hoare_Internal.
      intros ? ? [<- <-]. split. auto. split. auto. split. auto.
      eexists. eexists. eexists. split. eauto. split. eauto.
      edestruct pfp_goto_ok with (rettemp:=rettemp) (stk:=stk) as (inv & invle & INV); eauto.
      { intros. eapply iter_ok, H1.
        intros. eapply IHfuel with (stk:=(_, _)::_) in H3; eauto. }
      exists inv. split.
      { pose proof PTree.bempty_correct (PTree.combine
           (λ x y, match x with None => None | Some _ =>
            match y with
              | Some _ => None
              | None => Some tt
            end end) out5.(ogoto) (labels_stmt f.(fn_body))).
        destruct PTree.bempty. 2:discriminate.
        intros. apply proj1 in H1. specialize (H1 eq_refl lbl).
        rewrite PTree.gcombine in H1 by auto.
        destruct (out5.(ogoto) ! lbl) eqn:?.
        - destruct ((labels_stmt f.(fn_body)) ! lbl) eqn:?. destruct u.
          apply labels_stmt_ok with (k:=k) in Heqo0.
          destruct Heqo0 as [sk ->]. congruence. discriminate.
        - unfold goto_pred_of_ab in invle.
          specialize (invle _ _ _ H2). rewrite Heqo in invle. contradiction. }
      eapply hoare_stmt_post_impl, hoare_stmt_pre_impl, INV; auto.
      * { intros. destruct out5.(onormal). contradiction.
          assert (P':=pop_frame_sound ge None rettemp x). rewrite OUT8 in P'.
          destruct (Mem.free_list mem0 (blocks_of_env env)) eqn:?.
          - eexists. split. eauto.
            destruct stk as [|(le' & e')].
            + destruct (P' None). econstructor; eauto. simpl. congruence.
            + eapply join_pred_of_ab. right. apply (P' (Some _)).
              econstructor; eauto. simpl. intros. subst. determ. auto.
          - destruct (P' None). econstructor; eauto. congruence. }
      * unfold ret_pred_of_ab. intros v mem0.
        destruct stk as [|(le' & e')]. intros [? [? ?]]. split.
        apply join_correct. auto. eauto.
        auto using join_pred_of_ab.
      * rewrite Heql2. intros [] ? ? [].
      * { intros ? ? [<- <-]. destruct stk as [|(le & env0)].
          - destruct H as (? & ? & ?).
            eapply (P (Some _)). econstructor.
            eexists. split. eauto. split. auto.
            intros. subst. determ. auto.
          - eapply (P (Some _)). econstructor.
            eexists. split. eauto. split. auto. intros. determ. auto. }
    + destruct (P None), stk as [|[le env]].
      destruct H as (? & ? & ? & ->).
      econstructor. eexists. split. eauto. split. auto.
      intros. subst. destruct H1. eauto.
      econstructor. eexists. split. eauto. split. auto.
      intros. determ. destruct H1. eauto.
    + destruct (P None), stk as [|[env le]].
      destruct H as (? & ? & ? & ->).
      econstructor. eexists. split. eauto. split. auto.
      intros. destruct H1. eauto.
      econstructor. eexists. split. eauto. split. auto.
      intros. destruct H1. eauto.
  - intros. subst. destruct stk as [|[env le]].
    + destruct H0 as (? & ? & ? & ->).
      edestruct (ab_builtin_sound nil) as (vargs & -> & exEXTCALL & EXTCALL); eauto.
      eexists. split. eauto. split. eauto.
      apply hoare_External.
      intros vargs' mem' [<- <-]. split. auto.
      intros. edestruct EXTCALL; eauto.
    + edestruct ab_builtin_sound as (vargs & VARGS & exEXTCALL & EXTCALL); eauto.
      discriminate.
      eexists. split. apply VARGS. split. auto.
      apply hoare_External.
      intros vargs' mem' [<- <-]. split. auto.
      intros. edestruct EXTCALL; eauto.
Qed.

Theorem iter_program_sound:
  ∀ tr, program_behaves (semantics prog) (Goes_wrong tr) ->
  iter_program unroll prog = (tt, nil) ->
  False.
Proof.
  intros tr TR.
  unfold iter_program.
  eapply am_bind_case. discriminate. intros init INIT.
  pose proof (init_mem_sound ge (prog_defs prog)).
  rewrite INIT in H.
  destruct (Genv.alloc_globals ge Mem.empty (prog_defs prog)) eqn:?.
  - refine (let H' := H _ _ in _).
    exists prog. split. auto. split. auto.
    intro. rewrite Heqo. intro eq. inv eq. auto.
    destruct init as [|init]. contradiction.
    destruct (Genv.find_symbol (Genv.globalenv prog) (prog_main prog)) eqn:?. 2:discriminate.
    destruct (Genv.find_funct_ptr (Genv.globalenv prog) b) eqn:?. 2:discriminate.
    apply am_assert_spec. easy. intros Hf.
    eapply am_bind_case. discriminate. intros finish FINISH _.
    apply iter_function_ok with (stk:=nil) (mem:=m) in FINISH; eauto.
    destruct FINISH as (? & -> & SIG & HOARE).
    eapply hoare_prog; eauto.
    eapply hoare_fun_pre_impl, hoare_fun_post_impl, HOARE.
    simpl. now intuition. simpl. now intuition.
    split. auto. split. auto. split. now destruct f as [ f | () ]. auto.
  - destruct (H None).
    exists prog. split. auto. split. auto. intro. congruence.
Qed.

End ABMEM.

End PROG.