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 CsharpminorLogic.
Require Import CsharpminorIter.
Require Import AlarmMon.
Require Import AbMemSignatureCsharpminor.
Import Csharpminorannot.

Lemma eval_exprlist_snoc {F V} (ge: Genv.t F V) e t m args vargs :
  eval_exprlist ge e t m args vargs ->
  forall a v, eval_expr ge e t m a v ->
              eval_exprlist ge e t m (args ++ a :: nil) (vargs ++ v :: nil).
Proof.
induction 1; vauto. Qed.

Section PROG.

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

Lemma forall_exists {T: Type} (P : T → Prop) : (∀ 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.

Variables L abstate abstate_iter: Type.

Variable abmem : mem_dom L 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 L 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 log,
      type_check_expr L ty exp ab = (tt, (nil, log)) →
      ∃ ev v,
        v ∈ (eval_expr ge e t m (expr_erase exp) ∩ eventval_match ge ev ty).
Proof.
  intros t e s m ab Gamma ty exp log.
  unfold type_check_expr.
  destruct ty; try discriminate; intros NE;
  match type of NE with
  | noerror _ ?exp ?ab = _ =>
    generalize (noerror_sound L ge exp ab); rewrite NE; clear NE; intros NE
  end.
  destruct (forall_exists (λ i, Vint i ∈ eval_expr ge e t m (expr_erase 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_exists (λ i, Vfloat i ∈ eval_expr ge e t m (expr_erase 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_exists (λ i, Vlong i ∈ eval_expr ge e t m (expr_erase 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_exists (λ i, Vsingle i ∈ eval_expr ge e t m (expr_erase 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: C → A → B → alarm_mon L C) {ka kb ma} :
  (∀ x y z w k, ka x (y :: z) ≠ (w, (nil, k))) →
  (∀ x y z w k, kb x (y :: z) ≠ (w, (nil, k))) →
  ∀ mb c d e,
    fold_left2 (λ q a b, do c <- q; f c a b) ka kb ma mb c = (d, (nil, e)) →
    fst (snd c) = nil.
Proof.
  intros Hka Hkb.
  induction ma as [ | a ma IH ]; intros [ | b mb ] ( c & ([ | ? ? ], log)) d e 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) as (?, (?,?)). simpl in *; subst; eauto.
  - specialize (IH _ _ _ _ H).
    destruct (f c a b) as (?, (?,?)). 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 log,
      type_check_list L targs eargs ab = (tt, (nil, log)) →
      ∃ args vargs,
        args ∈ (eval_exprlist ge e t m (List.map expr_erase eargs) ∩ eventval_list_match ge vargs targs).
Proof.
  intros t e s m ab G targs.
  unfold type_check_list. simpl.
  generalize (@nil L) at 3.
  induction targs as [ | ty targs IH ]; intros gol [ | exp eargs ] log;
  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 log H). clear H.
    destruct IH as (args & vargs & Hargs & Hvargs).
    exists (v :: args), (ev :: vargs). split; constructor; auto.
    exfalso.
    generalize (λ X Y, fold_left2_bind_mono _ X Y _ _ _ _ H).
    refine (λ X, _ (X _ _)); discriminate.
Qed.

Lemma ab_builtin_sound:
  ∀ s m (ab: abstate), (s, m) ∈ γ ab ->
  ∀ ef x args ab' log, ab_builtin L ef x args ab = (ab', (nil, log)) ->
                   (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 (List.map expr_erase 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 L 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_exists (λ x,
        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 (expr_erase 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 L 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_exists (λ x,
                    let '(addr, arg, b, i, g, v) := x in
                    args = addr :: arg :: nil ∧
                    eval_expr ge e t m (expr_erase addr) (Vptr b i) ∧
                    Genv.find_symbol ge g = Some b ∧
                    eval_expr ge e t m (expr_erase arg) v ∧
                    (if Senv.block_is_volatile ge b
                     then ∃ v', eventval_match ge v' (type_of_chunk chunk) (Val.load_result chunk v)
                     else ∃ m', 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 L _ e x ab).
    simpl in H0. rewrite H0 in A.
    destruct (eval_expr_dec e' t m (expr_erase 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 L _ 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 (expr_erase 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 L _ sz al e e0 ab).
    simpl in H0. rewrite H0 in A.
    destruct (eval_expr_dec e' t m (expr_erase e)) as [[varg0 VARG0]|].
    destruct (eval_expr_dec e' t m (expr_erase 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 ((b0 ≠ b ∨ Int.unsigned i0 = Int.unsigned i
            ∨ Int.unsigned i0 + sz <= Int.unsigned i
            ∨ Int.unsigned i + sz <= Int.unsigned i0) \/
           ~(b0 ≠ b ∨ Int.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' X. inv X. 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 (() & ([ | ? ? ], log')).
    2: destruct x; simpl in *; eq_some_inv;
    destruct (assign _ _ _ _) as (?, (?,?)); simpl in *; eq_some_inv.
    intros X; specialize (X log' eq_refl).
    destruct X as (ev & v & Hv & Hev).
    destruct x as [ x | ]; simpl in *;
    (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 L ge x earg ab).
    destruct (assign _ _ _ _) as (?, (?,?)); eq_some_inv; subst.
    intros H1. eapply (H1 (Some _)).
    econstructor; eauto. now intros; determ.
    eq_some_inv; subst; 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 log H0. apply am_bind_case.
    intros; eq_some_inv; subst; eauto.
    intros; eq_some_inv.
    intros () log NOERR log' ?. eq_some_inv. subst.
    assert (exists vargs, eval_exprlist ge e t m (List.map expr_erase args) vargs) as VARGS.
    {
      revert log NOERR.
      induction args as [ | a args IH ] using rev_ind.
      vauto.
      rewrite am_fold_app. apply am_bind_case.
      intros; eq_some_inv; subst; eauto.
      intros; eq_some_inv.
      intros () log Hargs. specialize (IH log Hargs).
      unfold am_fold. simpl.
      generalize (noerror_sound L ge a ab). destruct (noerror _ _) as (u & ([ | ], ?)).
      2: discriminate.
      intros NE ?; eq_some_inv; subst.
      destruct (forall_exists (λ v, v ∈ eval_expr ge e t m (expr_erase 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).
      rewrite map_app. apply eval_exprlist_snoc; eassumption.
    }
    destruct VARGS as (vargs & VARGS). exists vargs. split. exact VARGS.
    split.
    exists nil, Vundef, m. vauto.
    intros tr vres m' X. inv X. 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 L (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 (ab1 ⊔ ab2) 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 L 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 (ab1 ⊔ ab2) 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 L 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 (a ⊔ a0); auto.
  destruct H as [? | []]. auto.
  destruct H as [[] | ?]. auto.
  destruct H as [[]|[]].
Qed.

Hypothesis iter_function_ok:
  ∀ sig name fundef rettemp args i o log,
    iter_function sig name fundef rettemp args i = (o, (nil, log)) ->
  ∀ le mem, pred_of_ab (NotBot i) le mem ->
    ∃ vargs,
      eval_exprlist ge env le mem (List.map expr_erase 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 L (@outcome abstate).
Variable low:abstate +⊥.

Hypothesis it_ok:
  ∀ ab o log,
    it ab = (o, (nil, log)) ->
    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 log,
    pfp_widen L fuel f x y = (o, (nil, log)) ->
    ∃ x0, f x0 = (o, (nil, log)) /\
          γ (y, x) ⊆ γ x0 /\
          γ o.(onormal) ⊆ γ x0.
Proof.
  induction fuel; simpl; intros.
  - destruct (f x) as (?, (?,?)). 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 log,
    pfp_narrow L it low n ab = (o, (nil, log)) ->
    (∀ o' log, ab = (o', (nil, log)) -> is_invariant o') ->
    is_invariant o.
Proof.
  induction n; intros. eapply H0; eauto. simpl in H.
  destruct @is_bot in H. eapply H0; eauto.
  destruct ab as [o' ([|],?)];
    destruct (it (low ⊔ o'.(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. exact (H0 _ _ eq_refl).
    eapply hoare_stmt_post_impl, hoare_stmt_pre_impl, it_ok, eqo''; auto.
    apply join_pred_of_ab.
  - eauto.
  - 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 log, pfp L it low = (o, (nil, log)) -> 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 abstate → alarm_mon L (@outcome abstate).
Variable body: stmt.

Hypothesis it_ok:
  ∀ ab o log,
    it ab = (o, (nil, log)) ->
    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 L 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 (a0 ⊑ a1) eqn:?; congruence.
Qed.

Lemma pfp_widen_goto_ok:
  ∀ fuel f x y o log,
    pfp_widen_goto L fuel f x y = (o, (nil, log)) ->
    ∃ x0, f x0 = (o, (nil, log)) /\ incl_goto o.(ogoto) x0.
Proof.
  Opaque widen_goto. induction fuel; simpl; intros.
  - destruct (f x) as (?, (?,?)). 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 log,
    pfp_narrow_goto L it n ab = (o, (nil, log)) ->
    (∀ o' log, ab = (o', (nil, log)) -> is_goto_invariant o') ->
    is_goto_invariant o.
Proof.
  induction n; intros. eapply H0; eauto. simpl in H.
  destruct (leb_goto L ((fst ab).(ogoto)) bot_goto) eqn:?.
  eapply H0; eauto.
  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 log, pfp_goto L it = (o, (nil, log)) -> 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 log,
    iter L unroll iter_function rettemp inormal igoto s = (o, (nil, log)) ->
    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 log,
    iter_switch L unroll iter_function rettemp islong inormal
                idefault iprev igoto e lbl_s = (o, (nil, log)) ->
    hoare_lbl_stmt prog env
                   (fun n le mem =>
                      eval_expr ge env le mem (expr_erase 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 log H. unfold iter. simpl. apply am_bind_case.
    intros; eq_some_inv; subst; eauto.
    intros; eq_some_inv.
    intros out log OUT log' eq. inv eq.
    assert (A:=assign_sound L ge i e inormal). rewrite OUT in A.
    destruct (eval_expr_dec env le mem (expr_erase 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 log H. unfold iter. simpl. apply am_bind_case.
    intros; eq_some_inv; subst; eauto.
    intros; eq_some_inv.
    intros out log OUT log' eq. inv eq.
    assert (S:=store_sound L ge a m e e0 inormal). rewrite OUT in S.
    destruct (eval_expr_dec env le mem (expr_erase e)) as [[v Hv]|].
    destruct (eval_expr_dec env le mem (expr_erase 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 log H. unfold iter, bind_normal_outcome.
    apply am_bind_case.
    intros; eq_some_inv; subst; eauto.
    intros; eq_some_inv.
    intros out1 log OUT1 log' eq. inv eq.
    revert log OUT1. apply am_bind_case.
    intros; eq_some_inv; subst; eauto.
    intros; eq_some_inv.
    intros out2 log OUT1 log' OUT2.
    assert (D:=deref_fun_sound L ge e inormal). rewrite OUT1 in D.
    destruct (eval_expr_dec env le mem (expr_erase 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.
      clear log.
      revert log' out1 OUT2. induction (rev out2). contradiction.
      unfold fold_right.
      apply am_bind_case.
      intros; eq_some_inv; subst; eauto.
      intros; eq_some_inv.
      intros out1 log OUT1.
      apply am_bind_case.
      intros; eq_some_inv; subst; eauto.
      intros; eq_some_inv.
      intros out3 log' OUT3.
      intros log'' out4 eq. simpl in eq. eq_some_inv. 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 log H. apply am_bind_case.
    intros; eq_some_inv; subst; eauto.
    intros; eq_some_inv.
    intros out1 log OUT1 log' 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 log H. unfold iter.
    apply am_bind_case.
    intros; eq_some_inv; subst; eauto.
    intros; eq_some_inv.
    intros out1 log OUT1.
    apply am_bind_case.
    intros; eq_some_inv; subst; eauto.
    intros; eq_some_inv.
    intros out2 log' OUT2 log'' eq. simpl in eq. eq_some_inv. 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 log H. unfold iter.
    apply am_bind_case.
    intros; eq_some_inv; subst; eauto.
    intros; eq_some_inv.
    intros [out1t out1f] log1 OUT1.
    apply am_bind_case.
    intros; eq_some_inv; subst; eauto.
    intros; eq_some_inv.
    intros out2 log2 OUT2.
    apply am_bind_case.
    intros; eq_some_inv; subst; eauto.
    intros; eq_some_inv.
    intros out3 log3 OUT3 log4.
    intros eq. simpl in eq. eq_some_inv. 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 L ge e inormal). rewrite OUT1 in A.
      destruct (eval_expr_dec env le mem (expr_erase e)) as [[v Hv]|].
      assert ((exists b, Val.bool_of_val v b) \/ (∀ b, ~Val.bool_of_val v b)).
      { clear. destruct v; try now (right; repeat intro; inv H). 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 log H. unfold iter.
    revert inormal igoto o. generalize (unroll_call_lookup s unroll).
    induction n; intros inormal igoto o.
    + apply am_bind_case.
      intros; eq_some_inv; subst; eauto.
      intros; eq_some_inv.
      intros out log OUT log' eq. simpl in eq. eq_some_inv. subst. simpl.
      eapply hoare_Sloop_unstable, pfp_ok, OUT. eauto.
    + apply am_bind_case.
      intros; eq_some_inv; subst; eauto.
      intros; eq_some_inv.
      intros out1 log1 OUT1.
      destruct out1.(onormal) eqn:E.
      * intros logr Hr; inv Hr. clear IHn. simpl.
        eapply hoare_Sloop, hoare_stmt_post_impl, IHs, OUT1; auto.
        rewrite E. contradiction.
      * apply am_bind_case.
        intros; eq_some_inv; subst; eauto.
        intros; eq_some_inv.
        intros out2 log2 OUT2.
        intros logr Hr; inv Hr. simpl.
        eapply hoare_loop_pre_unroll; eapply hoare_stmt_post_impl.
        5: eapply 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 log H. unfold iter.
    apply am_bind_case.
    intros; eq_some_inv; subst; eauto.
    intros; eq_some_inv.
    intros out log OUT log'.
    intros eq. simpl in eq. eq_some_inv. 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 log H. unfold iter.
    apply am_bind_case.
    intros; eq_some_inv; subst; eauto.
    intros; eq_some_inv.
    intros out1 log1 OUT1 log1' OUT1'.
    eapply hoare_Sswitch, hoare_lbl_stmt_pre_impl, IHlbl_s, OUT1'; eauto.
    intros. destruct inormal. contradiction.
    revert log1 OUT1. apply am_bind_case.
    intros; eq_some_inv; subst; eauto.
    intros; eq_some_inv.
    intros out2 log2 OUT2 log2' OUT2'.
    assert (N:=noerror_sound L ge (Eunop (if b then Cminor.Onegl else Cminor.Onegint) e) x). rewrite OUT2 in N.
    destruct (eval_expr_dec env le mem (expr_erase e)) as [[v Hv]|].
    assert ((∃ n, Switch.switch_argument b v n) \/ (∀ n, ~Switch.switch_argument b v n)).
    { clear; 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 log2' 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 log2' OUT2'. apply am_bind_case.
        intros; eq_some_inv; subst; eauto.
        intros; eq_some_inv.
        intros [outt outf] log OUT.
        assert (A:=assume_sound L 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 log H. unfold iter. apply am_bind_case.
    intros; eq_some_inv; subst; eauto.
    intros; eq_some_inv.
    intros out log OUT ? eq; simpl in eq; eq_some_inv; subst.
    assert (P:=pop_frame_sound L ge o rettemp inormal). rewrite OUT in P.
    assert ((∃ v, match o with
                  | Some a => eval_expr (Genv.globalenv prog) env le mem (expr_erase a) v
                  | None => v = Vundef
                  end) \/
            (∃ a, o = Some a /\ ∀ v, ~eval_expr (Genv.globalenv prog) env le mem (expr_erase a) v)).
    { destruct o. destruct (eval_expr_dec env le mem (expr_erase 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 log H. unfold iter_switch.
    apply am_bind_case.
    intros; eq_some_inv; subst; eauto.
    intros; eq_some_inv.
    intros [icase' idefault'] log1 OUT1.
    apply am_bind_case.
    intros; eq_some_inv; subst; eauto.
    intros; eq_some_inv.
    intros out2 log2 OUT2.
    apply am_bind_case.
    intros; eq_some_inv; subst; eauto.
    intros; eq_some_inv.
    intros out3 log3 OUT3 ?.
    intros eq. simpl in eq. eq_some_inv. subst.
    destruct o; revert log1 OUT1.
    + apply am_bind_case.
      intros; eq_some_inv; subst; eauto.
      intros; eq_some_inv.
      intros out4 log4 OUT4 ?.
      intros eq. simpl in eq. eq_some_inv. 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 log4 OUT4. apply am_bind_case.
        intros; eq_some_inv; subst; eauto.
        intros; eq_some_inv.
        intros [icase idummy] log OUT ? eq. simpl in eq. eq_some_inv. subst.
        assert (A:=assume_sound L 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 v b H H0. destruct islong.
        inv H0. inv H9. inv H4. inv H10. determ.
        unfold Val.cmpl, Val.cmpl_bool, Int64.cmp in H4. rewrite Int64.eq_true in H4.
        eq_some_inv. hsplit. subst. eq_some_inv. subst. inv H. auto.
        inv H0. inv H9. inv H4. determ. inv H10.
        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. eq_some_inv. 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 log,
    iter_function L unroll fuel sig name fundef rettemp args i = (o, (nil, log)) ->
  ∀ 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 (List.map expr_erase 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.
  revert log.
  destruct fundef.
  - apply am_bind_case.
    intros; eq_some_inv; subst; eauto.
    intros; eq_some_inv.
    intros out1 log1 OUT1.
    apply am_bind_case.
    intros; eq_some_inv; subst; eauto.
    intros; eq_some_inv.
    intros out2 log2 OUT2.
    apply am_bind_case.
    intros; eq_some_inv; subst; eauto.
    intros; eq_some_inv.
    intros out3 log3 OUT3.
    apply am_bind_case.
    intros; eq_some_inv; subst; eauto.
    intros; eq_some_inv.
    intros out4 log4 OUT4.
    apply am_bind_case.
    intros; eq_some_inv; subst; eauto.
    intros; eq_some_inv.
    intros out5 log5 OUT5.
    apply am_bind_case.
    intros; eq_some_inv; subst; eauto.
    intros; eq_some_inv.
    intros out6 log6 OUT6.
    apply am_bind_case.
    intros; eq_some_inv; subst; eauto.
    intros; eq_some_inv.
    intros out7 log7 OUT7.
    apply am_bind_case.
    intros; eq_some_inv; subst; eauto.
    intros; eq_some_inv.
    intros out8 log8 OUT8.
    intros ? eq. simpl in eq. eq_some_inv. 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 L 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 (List.map expr_erase 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, H0.
        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 H0. specialize (H0 eq_refl lbl).
        rewrite PTree.gcombine in H0 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 L 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 H0. eauto.
      econstructor. eexists. split. eauto. split. auto.
      intros. determ. destruct H0. eauto.
    + destruct (P None), stk as [|[env le]].
      destruct H as (? & ? & ? & ->).
      econstructor. eexists. split. eauto. split. auto.
      intros. destruct H0. eauto.
      econstructor. eexists. split. eauto. split. auto.
      intros. destruct H0. 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) ->
  ∀ log, iter_program L unroll prog = (tt, (nil, log)) ->
  False.
Proof.
  intros tr TR.
  unfold iter_program.
  apply am_bind_case.
  intros; eq_some_inv; subst; eauto.
  intros; eq_some_inv.
  intros init log INIT.
  pose proof (init_mem_sound L 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.
    intros; eq_some_inv; subst; eauto.
    intros; eq_some_inv.
    intros Hf.
    apply am_bind_case.
    intros; eq_some_inv; subst; eauto.
    intros; eq_some_inv.
    intros finish log' FINISH log'' _.
    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.
Generated by coq2html