Module VCGen

Require Import ProductProof.
Import Utf8.
Import Coqlib.
Import Maps.
Import Util.
Import Extra.
Import Product.
Import Sexpr Sylvie.

Definition OK_inj {T} {a b: T} (H: Errors.OK a = Errors.OK b) : a = b :=
  let 'eq_refl := H in eq_refl.

Lemma In_filter {A} (f: A → bool) (m: list A) (x: A) :
  In x m → reflect (In x (filter f m)) (f x).
Proof.
  intros IN.
  generalize (filter_In f x m). intros ().
  case (f _); intros X Y; constructor.
  apply Y; auto.
  intros K. specialize (X K). hsplit. apply diff_false_true. assumption.
Qed.

Lemma in_rev_map_o {X Y} (f: X → option Y) (xs: list X) y :
  In y (rev_map_o f xs) ↔ In (Some y) (map f xs).
Proof.
  cut (In y (rev_map_o f xs) ↔ In (Some y) (map f xs) ∨ In y nil). intuition.
  unfold rev_map_o.
  generalize (@nil Y).
  elim xs; clear xs. intuition.
  intros x xs IH acc. simpl.
  rewrite IH. clear IH.
  split. intros (). auto.
  case (f x). intros ? [ -> | ? ]; auto. auto.
  intros [ [ -> | ? ] | ? ]. right; left; auto. auto.
  right. case (f x); simpl; auto.
Qed.

Section REGISTER.

Context (reg: Type).
Context (reg_dec : EqDec reg).
Variable (reg_max: reg → reg → reg).
Variable reg_succ: reg → reg.
Variable (reg_le: reg → reg → Prop).
Hypothesis reg_le_refl : ∀ x, reg_le x x.
Hypothesis reg_le_trans : ∀ x y z, reg_le x y → reg_le y z → reg_le x z.
Hypothesis reg_max_le : ∀ x y z, reg_le z x ∨ reg_le z y → reg_le z (reg_max x y).
Hypothesis reg_succ_le_ne : ∀ x y, reg_le x y → x ≠ reg_succ y.

Let assign := assign' reg_dec reg_max reg_succ.
Let simplify := simplify reg_dec reg_max reg_succ.

Lemma simplify_is_true fs sp vp ε a :
  simplify a = True →
  eval_assertion _ fs sp vp ε a.
Proof.
  intros H.
  apply (simplify_correct _ reg_max reg_succ reg_le reg_le_refl reg_le_trans reg_max_le reg_succ_le_ne fs sp a vp ε).
  fold simplify. rewrite H. exact I.
Qed.

Definition wp (e: edge reg) (k: option bool) (a: assertion reg) : assertion reg :=
  match e with
  | Egoto _ => a
  | Ebranch cond args _ _ =>
    match k with
    | Some b =>
      let pre := Assert (oper (Op.Ocmp cond) (List.map Reg args)) in
      match b with
      | true => Implies pre a
      | false => Implies (Negate pre) a
      end
    | None => a
    end
  | Eop dst (Operation op) args _ => assign dst (oper op (List.map Reg args)) a
  | Eop dst Havoc _ _ =>
    if is_free' _ dst a
    then ForAll dst a
    else a
  | Estop => True
  end.

Section SOUNDNESS.

Import Values.

Context (find_symbol: AST.ident → option block) (sp: val) (valid_pointer: block → Z → bool) (fn: function reg).

Let step := step reg_dec find_symbol sp valid_pointer fn.
Let eval_assertion := eval_assertion reg_dec find_symbol sp valid_pointer.

Definition step_exit_compat (e: edge reg) (pc: node) k : Prop :=
  match e with
  | Ebranch _ _ t f =>
    if Pos.eqb t f
    then pc = t ∧ k = None
    else (pc = t ∧ k = Some true) ∨ (pc = f ∧ k = Some false)
  | Eop _ _ _ i
  | Egoto i => pc = i ∧ k = None
  | Estop => False
  end.

Definition State_inj {π ϱ π' ϱ'} (H: @State reg π ϱ = State π' ϱ') : π = π' ∧ ϱ = ϱ' :=
  let 'eq_refl := H in conj eq_refl eq_refl.

Definition Run_inj {a b: rstate reg} (H: Run a = Run b) : a = b :=
  let 'eq_refl := H in eq_refl.

Definition Run_neq_Stop {a: rstate reg} (P: Prop) (H: Run a = Stop _) : P :=
  let 'eq_refl := H in I.

Lemma step_has_exit_compat π ϱ π' ϱ' :
  step (Run (State π ϱ)) (Run (State π' ϱ')) →
  ∃ e k,
    (fn_code fn) ! π = Some e ∧ step_exit_compat e π' k.
Proof.
  simpl. case ((fn_code fn) ! _). 2: intros ().
  intros e STEP. exists e. revert STEP.
  case e; clear e; intros; hsplit;
  repeat match goal with
  | H : Run _ = Run _ |- _ => apply Run_inj, State_inj in H; hsplit
  | H : Run _ = Stop _ |- _ => exact (Run_neq_Stop _ H)
  | H : match ?x with _ => _ end |- _ => destruct x; hsplit
  end;
  subst; simpl; vauto.
  case Pos.eqb_spec; case b; vauto.
Qed.

Lemma map_o_eval_sexpr_map (ε: env reg) args :
  map_o (eval_sexpr find_symbol sp valid_pointer ε) (map Reg args) = Some (map ε args).
Proof.
  elim args; clear args.
  reflexivity.
  intros r args IH. simpl. rewrite IH. reflexivity.
Qed.

Lemma wp_sound pc e k a ε pc' ε' :
  (fn_code fn) ! pc = Some e →
  eval_assertion ε (wp e k a) →
  step (Run (State pc ε)) (Run (State pc' ε')) →
  step_exit_compat e pc' k →
  eval_assertion ε' a.
Proof.
  simpl. intros He. rewrite He.
  destruct e; simpl; intros PRE STEP Hk;
  hsplit;
  repeat match goal with
  | H : Run _ = _ |- _ => inversion H; clear H
  | o: operation |- _ => destruct o as [ | o ]; hsplit
  | H: upd_spec ?f ?r ?v ?f' |- _ => assert (eq_env f' (upd f r v)) by exact H; clear H
  | H: eq_env _ _ |- _ =>
    let X := fresh in
    let X' := fresh in
    pose proof (λ a, proj1 (eval_assertion_m reg_dec find_symbol sp H valid_pointer a)) as X;
    pose proof (λ a, proj2 (eval_assertion_m reg_dec find_symbol sp H valid_pointer a)) as X';
    clear H;
    fold eval_assertion in X;
    fold eval_assertion in X'
  end;
  subst;
  auto.
  - (* cond *)
    revert Hk. case Pos.eqb_spec.
    intros EQ (? & ->). auto.
    intros NE [ (? & ->) | (? & ->) ];
    destruct b; try congruence;
    red in PRE; simpl in PRE;
    rewrite map_o_eval_sexpr_map in PRE; simpl in PRE;
    rewrite STEP in PRE.
    specialize (PRE eq_refl); auto.
    assert (Vfalse ≠ Vtrue) as K by discriminate.
    specialize (PRE (λ H, K (some_eq_inv H))). auto.
  - (* havoc *)
    red in PRE. simpl in PRE. fold (eval_assertion) in PRE.
    destruct (is_free' _ _ _) eqn: FREE.
    + red in PRE. simpl in *.
      fold eval_assertion in PRE. auto.
    + generalize (eval_assertion_is_free reg_dec find_symbol sp _ _ FREE valid_pointer ε v).
      intuition.
  - (* op *)
    match goal with H : _ |- _ => apply H; clear H end.
    eapply eval_assertion_assign'; try eassumption.
    rewrite oper_eval. clear -STEP.
    simpl. rewrite map_o_eval_sexpr_map.
    exact STEP.
Qed.

End SOUNDNESS.

Context (c: code reg).

Context (annot: PTree.t (list (decoration reg))).

Definition get_invariant (pc: node) : list (assertion reg) :=
  match annot ! pc with
  | None => nil
  | Some a => rev_map_o (λ d, match d with Invariant i => Some i | Assertion _ => None end) a
  end.

Inductive vc_for_case_t : Type :=
| VC_norec (inv: list (assertion reg)) (a: assertion reg)
| VC_rec (a: assertion reg).

Definition vc_for_case pc d : vc_for_case_t :=
  match get_invariant pc, d with
  | nil, (Invariant a | Assertion a)
  | _, Invariant a =>
    VC_rec a
  | inv, Assertion a =>
    VC_norec inv a
  end.

Definition not_nil {A} (m: list A) : Prop :=
  match m with
  | nil => False | _ => Logic .True
  end.

Definition not_nil_inv {A} (m: list A) :
  not_nil m →
  ∃ a m', m = a :: m' :=
  match m with
  | nil => False_ind _
  | a :: m' => λ _, ex_intro _ a (ex_intro _ m' eq_refl)
  end.

Definition vc_for_case_ind (P: _ → _ → _ → Prop) :
  ∀ pc,
    (∀ d a, get_invariant pc = nil ∧ d = Assertion a ∨ d = Invariant a → P pc d (VC_rec a)) →
    (∀ a, not_nil (get_invariant pc) → P pc (Assertion a) (VC_norec (get_invariant pc) a)) →
    ∀ d, P pc d (vc_for_case pc d).
Proof.
  intros pc Hrec Hnorec d. specialize (Hrec d).
  unfold vc_for_case.
  destruct (get_invariant _);
    destruct d; simpl in *; auto.
Qed.

Import Errors.
Open Scope error_monad_scope.

Section PRED.
Context (predecessors : PTree.t (list (node * option bool))).
Context (ep_annot: Sexpr.assertion reg → Sexpr.assertion reg).

Fixpoint vc_for (pc: node) (d: Product.decoration reg) (acc: list (Sexpr.assertion reg)) (fuel: nat) {struct fuel} : Errors.res (list (Sexpr.assertion reg)) :=
  match fuel with
  | O => Error (msg "vc_for: Dame más gasolina")
  | S fuel' =>
    match vc_for_case pc d with
    | VC_rec a =>
      let acc := if (pc =? 1)%positive then ep_annot (match d with Invariant a | Assertion a => a end) :: acc else acc in
      match predecessors ! pc with
      | (None | Some nil) =>
        OK acc
      | Some pre =>
        let f p :=
            let '(pc', k) := p in
            match c ! pc' with
            | None => Error (msg "vc_for: no edge")
            | Some i =>
              let a' := wp i k a in
              OK (pc', Assertion a')
            end
        in
        match pre with
        | p :: nil =>
          do (pc', a) <- f p;
          if match a with Assertion a' =>
                          eq_dec True (simplify a')
                     | _ => false end
          then OK acc
          else
          vc_for pc' a acc fuel'
        | _ =>
        List.fold_left
          (λ res p,
           do res <- res;
           do (pc', a) <- f p;
           vc_for pc' a res fuel'
          )
          pre
          (OK acc)
        end
      end
    | VC_norec inv a =>
      OK (with_precondition inv a :: acc)
    end
  end.

Definition doit' fuel :
  Errors.res (list (node * Sexpr.assertion reg)) :=
  PTree.fold
    (λ res pc dec,
     List.fold_left
       (λ res d,
        do res <- res;
        do a <- vc_for pc d nil fuel;
        OK (rev_map_app (pair pc) a res)
       )
       dec
       res
    )
    annot
    (OK nil).

Let ghost_insert (pc: node) (d: decoration reg) (g: hashmap _) :=
  match d with Invariant _ => g | Assertion a => PTree.set pc (a :: g pc) g end.

Lemma ghost_insert_get pc d g pc' :
  (ghost_insert pc d g) pc' = if peq pc' pc then match d with Invariant _ => g pc | Assertion a => a :: g pc end else g pc'.
Proof.
  unfold ghost_insert. case d. case peq; congruence.
  intros a. unfold ptree_get_all. rewrite PTree.gsspec. case peq; auto.
Qed.

Fixpoint vc_for_ghost (pc: node) (d: Product.decoration reg) (acc: list (Sexpr.assertion reg)) (g: hashmap (Sexpr.assertion reg)) (fuel: nat) {struct fuel} : Errors.res (list (Sexpr.assertion reg) * hashmap (Sexpr.assertion reg)) :=
  match fuel with
  | O => Error (msg "vc_for_ghost: Dame más gasolina")
  | S fuel' =>
    match vc_for_case pc d with
    | VC_rec a =>
      let acc := if (pc =? 1)%positive then ep_annot (match d with Invariant a | Assertion a => a end) :: acc else acc in
      match predecessors ! pc with
      | (None | Some nil) =>
        OK (acc, ghost_insert pc d g)
      | Some pre =>
        let f p :=
            let '(pc', k) := p in
            match c ! pc' with
            | None => Error (msg "vc_for_ghost: no edge")
            | Some i =>
              let a' := wp i k a in
              OK (pc', Assertion a')
            end
        in
        match pre with
        | p :: nil =>
          do (pc', a) <- f p;
          if match a with Assertion a' =>
                          eq_dec True (simplify a')
                     | _ => false end
          then OK (acc, ghost_insert pc d g)
          else
            (do res <- vc_for_ghost pc' a acc g fuel';
             let '(acc, g) := res in
             OK (acc, ghost_insert pc d g))
        | _ =>
          do res <-
        List.fold_left
          (λ (res: Errors.res (list _ * hashmap _)) p,
           do res <- res;
           let '(acc, g) := res in
           do (pc', a) <- f p;
           vc_for_ghost pc' a acc g fuel'
          )
          pre
          (OK (acc, g));
            let '(acc, g) := res in
            OK (acc, ghost_insert pc d g)
        end
      end
    | VC_norec inv a =>
      OK (with_precondition inv a :: acc, ghost_insert pc d g)
    end
  end.

Definition doit'_ghost_aux pc fuel :=
    (λ res d,
     do res <- res;
     let '(acc, g) := res in
     do a <- vc_for_ghost pc d nil g fuel;
     let '(a, g) := a in
     OK (rev_map_app (pair pc) a acc, g)
    ).

Definition doit'_ghost fuel :
  Errors.res (list (node * Sexpr.assertion reg) * hashmap (Sexpr.assertion reg)) :=
  PTree.fold (λ res pc deco, List.fold_left (doit'_ghost_aux pc fuel) deco res)
    annot
    (OK (nil, PTree.empty _)).

Lemma doit'_ghost_intro fuel (P : _ → Prop) :
  (∀ m,
      (∀ pc deco d, annot ! pc = Some deco → In d deco → In (pc, d) m) →
      (∀ pc d, In (pc, d) m → ∃ deco, annot ! pc = Some deco ∧ In d deco) →
      P (List.fold_left (λ res pc_d, let '(pc, d) := pc_d in doit'_ghost_aux pc fuel res d) m (OK (nil, PTree.empty _)))) →
  P (doit'_ghost fuel).
Proof.
  intros H.
  specialize (H (flat_map (λ pc_deco, let '(pc, deco) := pc_deco in map (pair pc) deco) (PTree.elements annot))).
  eapply eq_ind.
  apply H; clear.
  intros pc deco d H0 H1.
  rewrite in_flat_map. exists (pc, deco). split.
  apply PTree.elements_correct; auto.
  apply in_map; auto.
  intros pc d. rewrite in_flat_map. intros ().
  intros (pc', deco'). intros [H H']. rewrite in_map_iff in H'.
  destruct H' as (d' & ? & H'). eq_some_inv. subst pc' d'.
  apply PTree.elements_complete in H. eauto.
  clear.
  unfold doit'_ghost.
  rewrite PTree.fold_spec.
  generalize (PTree.elements annot).
  intros m. elim m using rev_ind; clear m.
  reflexivity.
  intros (pc, deco) m IH.
  rewrite flat_map_app.
  rewrite ! fold_left_app, <- IH. clear IH.
  simpl. rewrite app_nil_r.
  elim deco using rev_ind; clear deco. reflexivity.
  intros d deco IH. rewrite map_app, ! fold_left_app. simpl.
  rewrite IH. reflexivity.
Qed.

Lemma vc_for_has_ghost pc d acc fuel res :
  vc_for pc d acc fuel = OK res →
  ∀ g, ∃ g', vc_for_ghost pc d acc g fuel = OK (res, g').
Proof.
  revert pc d acc res.
  elim fuel; clear fuel.
  discriminate.
  intros fuel IH.
  intros pc d acc res.
  unfold vc_for, vc_for_ghost.
  case vc_for_case.
  - intros inv a H g. apply OK_inj in H. rewrite H. vauto.
  - intros a.
    set (acc' := if (pc =? 1)%positive then ep_annot match d with Invariant a | Assertion a => a end :: acc else acc).
    fold vc_for. fold vc_for_ghost.
    destruct (predecessors ! pc) as [ [ | (pc', k) [ | x pre ] ] | ].
    + intros H; apply OK_inj in H. intros g; eexists; apply f_equal; apply f_equal2; auto.
    + destruct (c ! pc') as [ e | ]. 2: discriminate.
      simpl.
      case proj_sumbool. intros H; apply OK_inj in H; intros g; eexists. repeat f_equal; auto.
      intros H g. specialize (IH _ _ _ _ H g). destruct IH as (g' & G).
      rewrite G. simpl. eauto.
    + generalize ((pc', k) :: x :: pre). clear pc' k x pre.
      intros pre. revert acc acc' res.
      elim pre using rev_ind; clear pre.
      * intros acc acc' res.
        intros H. apply OK_inj in H. intros g; eexists. simpl. apply f_equal, f_equal2; auto.
      * intros (pc', k) pre IH' acc acc' res.
        setoid_rewrite fold_left_app. simpl.
        destruct (c ! pc') as [ e | ].
        2: intros H; monadInv H; discriminate.
        intros H g. specialize (IH' acc). fold acc' in IH'.
        destruct (fold_left _ pre (OK acc')) as [ acc'' | ] eqn: X. 2: discriminate. simpl in H.
        specialize (IH' _ X). destruct (IH' g) as [ g' G ]. clear IH' X.
        destruct (fold_left _ _ _) as [ (acc''' & g'') | ]. 2: discriminate. simpl in *.
        apply OK_inj in G. inv G.
        specialize (IH _ _ _ _ H g''). destruct IH as (g' & G'). rewrite G'. simpl. eauto.
    + intros H; apply OK_inj in H; intros g; eexists; repeat f_equal; auto.
Qed.

Lemma doit'_has_ghost fuel res :
  doit' fuel = OK res →
  ∃ g, doit'_ghost fuel = OK (res, g).
Proof.
  set (f res pc dec := fold_left (λ res d, do res <- res; do a <- vc_for pc d nil fuel; OK (rev_map_app (pair pc) a res)) dec res).
  change (PTree.fold f annot (OK nil) = OK res → ∃ g, PTree.fold (λ res pc deco, List.fold_left (doit'_ghost_aux pc fuel) deco res) annot (OK (nil, PTree.empty _)) = OK (res, g)).
  rewrite ! PTree.fold_spec.
  revert res.
  generalize (PTree.elements annot).
  intros ann. elim ann using rev_ind; clear ann.
  - intros res H; apply OK_inj in H; subst res. vauto.
  - intros (pc, deco) ann IH res.
    setoid_rewrite fold_left_app. simpl.
    destruct (fold_left _ ann (OK nil)) as [ m | e ].
    + specialize (IH _ eq_refl). destruct IH as (g & IH). rewrite IH. clear IH.
      revert res. elim deco using rev_ind; clear deco.
      * intros res H; apply OK_inj in H; subst m. vauto.
      * intros d deco IH res.
        unfold f. setoid_rewrite fold_left_app. simpl.
        fold (f (OK m) pc deco).
        destruct (f (OK m) pc _) as [ res' | e ]. 2: discriminate.
        specialize (IH _ eq_refl). destruct IH as (g' & IH).
        rewrite IH. clear IH. simpl. intros H.
        generalize (vc_for_has_ghost pc d nil fuel).
        destruct (vc_for _ _ _ _). 2: discriminate.
        apply OK_inj in H. subst res. intros H. specialize (H _ eq_refl g').
        destruct H as (g'' & H).
        eexists. rewrite H. reflexivity.
    + intros K. exfalso. clear - K. revert e K. elim deco; clear deco.
      discriminate. intros d deco. exact id.
Qed.

Definition ghost_rel (g g': hashmap (Sexpr.assertion reg)) : Prop :=
  ∀ x y, In x (g y) → In x (g' y).

Infix "<<" := ghost_rel (at level 50).

Import RelationClasses.
Instance ghost_rel_refl : Reflexive ghost_rel.
Proof.
intros g x y; exact id. Qed.

Instance ghost_rel_trans : Transitive ghost_rel.
Proof.
intros α β γ L R x y H. apply R, L, H. Qed.

Lemma ghost_insert_mono pc d g : g << ghost_insert pc d g.
Proof.
  intros x y H.
  rewrite ghost_insert_get. case peq.
  intros ->. case d; simpl; auto.
  intros _. exact H.
Qed.

Lemma vc_for_ghost_mono pc d acc g fuel res g' :
  vc_for_ghost pc d acc g fuel = OK (res, g') →
  g << g' ∧ (∀ vc, In vc acc → In vc res).
Proof.
  revert pc d acc g res g'.
  elim fuel; clear fuel. discriminate.
  intros fuel IH pc d acc g res g'.
  unfold vc_for_ghost.
  case vc_for_case.
  - intros inv a H; apply OK_inj in H. inv H.
    split. apply ghost_insert_mono.
    clear. intros vc H. right. exact H.
  - intros a.
    set (acc' := if (pc =? 1)%positive then ep_annot match d with Invariant a | Assertion a => a end :: acc else acc).
    destruct (predecessors ! pc) as [ [ | (pc', k) [ | x pre ] ] | ].
    + intros H; apply OK_inj in H. inv H. split.
      apply ghost_insert_mono.
      case (_ =? _)%positive; simpl; auto.
    + destruct (c ! pc') as [ e | ]. 2: discriminate.
      fold (vc_for_ghost). simpl.
      case proj_sumbool.
      * intros H; apply OK_inj in H; inv H.
        split. apply ghost_insert_mono.
        case (_ =? _)%positive; simpl; auto.
      * specialize (IH pc' (Assertion (wp e k a)) acc' g).
        destruct (vc_for_ghost _ _ _ _ _) as [ (res', g'') | err ]. 2: discriminate.
        specialize (IH _ _ eq_refl). simpl. intros H; apply OK_inj in H. inv H.
        destruct IH as [IH IH'].
        split.
        transitivity g''; auto using ghost_insert_mono.
        intros vc H. apply IH'. clear -H.
        subst acc'. destruct (_ =? _)%positive; simpl; auto.
    + generalize ((pc', k) :: x :: pre). clear pc' k x pre.
      intros pre. revert acc acc' g res g'.
      elim pre using rev_ind; clear pre.
      * intros acc acc' g res g'. simpl.
        intros H. apply OK_inj in H. inv H.
        split. apply ghost_insert_mono.
        case (_ =? _)%positive; simpl; auto.
      * intros (pc', k) pre IH' acc acc' g res g'. rewrite fold_left_app.
        fold (vc_for_ghost) in *. simpl.
        destruct (c ! pc') as [ e | ].
        {
          intros H. specialize (IH' acc g). fold acc' in IH'.
          destruct (fold_left _ pre _) as [ (acc'' & g'') | ] eqn: X. 2: discriminate.
          simpl in H.
          setoid_rewrite X in IH'.
          specialize (IH' _ _ eq_refl). destruct IH' as [IH' IH''].
          specialize (IH pc' (Assertion (wp e k a)) acc'' g'').
          destruct (vc_for_ghost _) as [ (acc''' & g''') | err ]. 2: discriminate. simpl in *. apply OK_inj in H. inv H.
          specialize (IH _ _ eq_refl). destruct IH as [IH IH_].
          split.
          etransitivity. exact IH'.
          clear -IH.
          intros x y. rewrite ! ghost_insert_get.
          (case peq; [ intros ->; case d; simpl; intuition | auto ]).
          auto.
        }
        {
          intros K. exfalso. clear -K. revert K.
          destruct (fold_left _ _ _) as [ (?, ?) | ? ]; discriminate.
        }
    + intros H; apply OK_inj in H. inv H. split. apply ghost_insert_mono.
      case (_ =? _)%positive; simpl; auto.
Qed.

Lemma in_hashmap_insert {X} a pc (g: hashmap X) :
  In a ((PTree.set pc (a :: g pc) g : hashmap X) pc).
Proof.
  unfold ptree_get_all. rewrite PTree.gss. left. reflexivity.
Qed.

Lemma vc_for_ghost_has_vc pc a acc g fuel res g' :
  vc_for_ghost pc (Assertion a) acc g fuel = OK (res, g') →
  In a (g' pc).
Proof.
  case fuel; clear fuel. discriminate. intros fuel.
  simpl. case vc_for_case.
  - intros inv a' H; apply OK_inj in H; inv H. apply in_hashmap_insert.
  - intros a'.
    destruct (predecessors ! _) as [ [ | (pc'' & k) [ | x pre ] ] | ].
    + intros H; apply OK_inj in H; inv H. apply in_hashmap_insert.
    + destruct (c ! _). 2: discriminate. simpl.
      case proj_sumbool.
      intros H; apply OK_inj in H; inv H. apply in_hashmap_insert.
      destruct (vc_for_ghost _) as [ (?, ?) | ]. 2: discriminate.
      simpl. intros H; apply OK_inj in H; inv H. apply in_hashmap_insert.
    + destruct (fold_left _ _ _) as [ (?, ?) | ]. 2: discriminate.
      simpl. intros H; apply OK_inj in H; inv H. apply in_hashmap_insert.
    + intros H; apply OK_inj in H; inv H. apply in_hashmap_insert.
Qed.

Definition trivial_or_in (a: Sexpr.assertion reg) (m: list _) :=
  simplify a = True ∨ In a m.

Lemma make_predecessors_correct :
  ∀ π e π' k,
    c ! π = Some e →
    step_exit_compat e π' k →
    ∃ m, (make_predecessors c) ! π' = Some m ∧ In (π, k) m.
Proof.
  unfold make_predecessors.
  apply PTree_Properties.fold_rec.
  - intros m m' a H H0 π e π' k H1 H2. eapply H0; eauto. rewrite H; assumption.
  - intros π e π' k. rewrite PTree.gempty. intro; eq_some_inv.
  - intros c' pred pc v H Hpc IH π e π' k.
    rewrite PTree.gsspec. case peq.
    + intros ? ?; eq_some_inv; subst v pc.
      revert e Hpc. intros (); simpl.
      * intros i Hpc (-> & ->).
        rewrite PTree.gss. vauto2.
      * intros cond args t f Hpc.
        case Pos.eqb_spec. intros ->. intros (-> & ->). rewrite PTree.gss. vauto2.
        intros Htf. intros [ (-> & ->) | (-> & ->) ];
          repeat (repeat rewrite PTree.gss; repeat rewrite PTree.gso by auto);
          vauto2.
      * intros dst op args i Hpc (-> & ->). rewrite PTree.gss. vauto2.
      * intros _ ().
    + intros NE Hold CPT.
      specialize (IH _ _ _ _ Hold CPT).
      destruct IH as (m & Hπ' & Hm).
      destruct (successors _) as [ | α [ | β [ | γ ? ] ] ]; vauto.
      * rewrite PTree.gsspec; case peq. 2: vauto.
        intros ->. eexists. split. vauto. right.
        unfold ptree_get_all. unfold node in *. rewrite Hπ'. exact Hm.
      * case Pos.eqb_spec.
        intros ->. rewrite PTree.gsspec. case peq. 2: vauto.
          intros ->. eexists. split. vauto. right.
          unfold ptree_get_all. unfold node in *. rewrite Hπ'. exact Hm.
        intros NE'. rewrite PTree.gsspec. case peq.
          intros ->. eexists. split. vauto. right.
          unfold ptree_get_all, node in *. rewrite PTree.gso; auto. rewrite Hπ'. exact Hm.
          intros NE''.
            rewrite PTree.gsspec. case peq. 2: vauto.
            intros ->. eexists. split. vauto. right.
            unfold ptree_get_all, node in *. rewrite Hπ'. exact Hm.
Qed.

Lemma make_predecessors_complete :
  ∀ π' m,
    (make_predecessors c) ! π' = Some m →
    ∀ π k, In (π, k) m →
           ∃ e, c ! π = Some e ∧ step_exit_compat e π' k.
Proof.
  unfold make_predecessors.
  apply PTree_Properties.fold_rec.
  - intros m m' a H H0 π' m0 H1 π k H2. edestruct H0; eauto. hsplit. rewrite H in *. vauto.
  - intros π' m. rewrite PTree.gempty. intro; eq_some_inv.
  - intros m a pc v Hmk Hck IH π' pred Hpred π k' Hk'.
    unfold ptree_get_all in Hpred.
    destruct v; simpl in *; rewrite ? PTree.gsspec in Hpred.
    * destruct peq. subst. eq_some_inv. subst.
      destruct Hk'. eq_some_inv. subst.
      eexists. split. apply PTree.gss. vauto.
      specialize (IH i). destruct (a ! i) as [ m' | ] eqn: Hm'.
      specialize (IH _ Hm' _ _ H). hsplit. rewrite PTree.gso. vauto. congruence.
      elim H.
      destruct (IH _ _ Hpred _ _ Hk'). rewrite PTree.gso. vauto. intuition congruence.
    * revert Hpred.
      case Pos.eqb_spec. intros ->.
      rewrite PTree.gsspec. case peq. intros ->. intro; eq_some_inv; subst pred.
      destruct Hk'. eq_some_inv. subst.
      eexists. split. apply PTree.gss. simpl. rewrite Pos.eqb_refl. vauto.
      specialize (IH f). destruct (a ! f) as [ m' | ] eqn: Hm'. 2: intuition.
      specialize (IH _ Hm' _ _ H). hsplit. rewrite PTree.gso. vauto. congruence.
      intros NE Hpred.
      destruct (IH _ _ Hpred _ _ Hk'). rewrite PTree.gso. vauto. intuition congruence.
      intros NE. rewrite peq_false by auto.
      rewrite PTree.gsspec. case peq. intros -> ?; eq_some_inv; subst pred.
      destruct Hk' as [? | Hk']. eq_some_inv. subst.
      eexists. split. apply PTree.gss. simpl. rewrite (proj2 (Pos.eqb_neq _ _) NE). vauto.
      specialize (IH f). destruct (a ! f) as [ m' | ] eqn: Hm'. 2: intuition.
      specialize (IH _ Hm' _ _ Hk'). hsplit. rewrite PTree.gso. vauto. congruence.
      intros NE'. rewrite PTree.gsspec. case peq. intros -> ?; eq_some_inv; subst pred.
      destruct Hk' as [? | Hk']. eq_some_inv. subst.
      eexists. split. apply PTree.gss. simpl. rewrite (proj2 (Pos.eqb_neq _ _) NE). vauto.
      specialize (IH t). destruct (a ! t) as [ m' | ] eqn: Hm'. 2: intuition.
      specialize (IH _ Hm' _ _ Hk'). hsplit. rewrite PTree.gso. vauto. congruence.
      intros NE'' Hpred.
      destruct (IH _ _ Hpred _ _ Hk'). rewrite PTree.gso. vauto. hsplit. congruence.
    * destruct peq. subst. eq_some_inv. subst.
      destruct Hk'. eq_some_inv. subst.
      eexists. split. apply PTree.gss. simpl. vauto.
      specialize (IH i). destruct (a ! i) as [ m' | ] eqn: Hm'. 2: intuition.
      specialize (IH _ Hm' _ _ H). hsplit. rewrite PTree.gso. vauto. congruence.
      destruct (IH _ _ Hpred _ _ Hk'). rewrite PTree.gso. vauto. intuition congruence.
    * destruct (IH _ _ Hpred _ _ Hk'); hsplit. rewrite PTree.gso. vauto. congruence.
Qed.

Hypothesis predecessors_correct :
  ∀ π e π' k,
    c ! π = Some e →
    step_exit_compat e π' k →
    ∃ m, predecessors ! π' = Some m ∧ In (π, k) m.

Hypothesis predecessors_complete :
  ∀ π' m,
    predecessors ! π' = Some m →
    ∀ π k, In (π, k) m →
           ∃ e, c ! π = Some e ∧ step_exit_compat e π' k.

Lemma not_nil_rev_ind {X} (P: list X → Prop) :
  ∀ x m,
    (P (x :: nil)) →
    (∀ z m', P m' → P (m' ++ z :: nil)) →
    P (x :: m).
Proof.
  clear.
  intros x m Hbase Hind.
  set (Q n := P (x :: n)).
  fold (Q m).
  elim m using rev_ind; clear m. exact Hbase.
  intros y m REC.
  exact (Hind y _ REC).
Qed.

Lemma step_exit_compat_inj e pc' k k' :
  step_exit_compat e pc' k →
  step_exit_compat e pc' k' →
  k' = k.
Proof.
  clear.
  destruct e; simpl; try intuition congruence.
  case Pos.eqb_spec; intuition congruence.
Qed.

Lemma vc_for_ghost_step pc deco acc g fuel acc' g' :
  vc_for_ghost pc deco acc g fuel = OK (acc', g') →
  ∀ π e k π',
    get_invariant π' = nil →
    c ! π = Some e →
    step_exit_compat e π' k →
    ∀ a,
      In a (g' π') →
      ¬ In a (g π') →
      trivial_or_in (wp e k a) (g' π).
Proof.
  Opaque Pos.eqb.
  revert pc deco acc g acc' g'.
  elim fuel; clear fuel. discriminate.
  intros fuel IH.
  intros pc deco acc g acc' g'.
  unfold vc_for_ghost. fold vc_for_ghost.
  apply vc_for_case_ind.
  - intros d a H.
    destruct (predecessors ! pc) as [ [ | (pc', k') [ | x pre ] ] | ] eqn: Hpre.
    + intros K; apply OK_inj, pair_eq_inv in K; destruct K as [<- <-].
      destruct H as [ [ H -> ] | -> ]. 2: intuition.
      simpl. intros π e k π' H0 H1 H2 a'.
      unfold ptree_get_all. rewrite PTree.gso. intuition.
      intros ->.
      destruct (predecessors_correct _ _ _ _ H1 H2) as (pre & Hpre' & K).
      rewrite Hpre in Hpre'. eq_some_inv. subst pre. exact K.
    + destruct (c ! pc') as [ e' | ] eqn: He'. 2: discriminate. simpl.
      destruct (proj_sumbool _) eqn: Htrivial.
      * clear IH.
        intros K; apply OK_inj, pair_eq_inv in K; destruct K as [<- <-].
        destruct H as [ [ H -> ] | -> ]. 2: intuition. simpl.
        intros π e k π' H0 H1 H2 a'.
        unfold ptree_get_all. rewrite ! PTree.gsspec. case peq. 2: intuition.
        intros -> [ <- | IN ]. 2: intuition.
        intros _. destruct (predecessors_correct _ _ _ _ H1 H2) as (pre & Hpre' & K).
        rewrite Hpre' in Hpre. eq_some_inv. subst pre.
        destruct K as [ K | () ]. eq_some_inv. subst pc' k'.
        rewrite He' in H1. eq_some_inv. subst e'.
        left. symmetry. apply eq_dec_eq, Htrivial.
      * destruct (vc_for_ghost _ _ _ _ _) as [(?, ?)|] eqn: REC. 2: discriminate.
        specialize (IH _ _ _ _ _ _ REC).
        intros K; apply OK_inj, pair_eq_inv in K; destruct K as [<- <-].
        intros π e k π' H0 H1 H2 a'.
        destruct H as [ [ H -> ] | -> ]; simpl. 2: eauto.
        unfold ptree_get_all. rewrite PTree.gsspec. case peq.
        { intros ->. intros [ <- | IN ].
          destruct (predecessors_correct _ _ _ _ H1 H2) as (pre & Hpre' & K).
          rewrite Hpre' in Hpre. eq_some_inv. subst pre.
          destruct K as [ K | () ]. eq_some_inv. subst pc' k'.
          rewrite He' in H1. eq_some_inv. subst e'.
          apply vc_for_ghost_has_vc in REC.
          intros NI. right. rewrite PTree.gsspec. case peq. intros ->. intuition. intros _. exact REC.
          intros NI. specialize (IH _ _ _ _ H0 H1 H2 a' IN NI). clear IN NI.
          destruct IH as [IH|IH]. left; exact IH. right.
          rewrite PTree.gsspec. case peq. intros ->. right. exact IH. intros _. exact IH. }
        { intros NE IN NI. specialize (IH _ _ _ _ H0 H1 H2 a' IN NI). clear IN NI.
          destruct IH as [IH|IH]. left; exact IH. right.
          rewrite PTree.gsspec. case peq. intros ->. right. exact IH. intros _. exact IH. }

    + intros REC'.
      match type of REC' with appcontext[ fold_left ?f _ ?a ] =>
                             set (func := f); set (rec := a); fold func in REC'; fold rec in REC' end.
      destruct (fold_left func _ rec) as [(acc'', g'')|] eqn: REC. 2: discriminate.
      apply OK_inj, pair_eq_inv in REC'.
      destruct REC' as [<- <-].
      intros π e k π' Hinv He Hk.
      revert Hpre REC.
      generalize (x :: pre). clear x pre. intros pre Hpre REC.
      intros a' Hag' Hag.
      assert ((d = Assertion a' ∧ pc = π') ∨ (In a' (g'' π'))) as D.
      { clear - Hag'.
        destruct d as [ d | d ]; simpl in *. eauto.
        revert Hag'.
        unfold ptree_get_all at 1. rewrite PTree.gsspec. case peq.
        intros ->. intros [<- | Hag' ]; eauto. eauto. }
      clear Hag'.
      destruct D as [ D | D ].
      {
        destruct D as [ X Y ].
        rewrite X in *; clear X.
        rewrite Y in *; clear Y.
        generalize (predecessors_correct _ _ _ _ He Hk).
        intros (m & Hm & Hπk). rewrite Hpre in Hm. eq_some_inv.
        subst m.
        cut (∃ (h h': hashmap _) vcs vcs',
                vc_for_ghost π (Assertion (wp e k a')) vcs h fuel = OK (vcs', h') ∧ h' << g'').
        intros (h & h' & vcs & vcs' & REC' & MONO).
        apply vc_for_ghost_has_vc in REC'.
        right. simpl.
        unfold ptree_get_all at 1. rewrite PTree.gsspec. case peq.
        intros ->; right; apply MONO, REC'.
        intros; apply MONO, REC'.

        destruct H as [ [ _ Y ] | H ]. 2: discriminate.
        inversion Y; clear Y; subst a'.
        clear Hpre Hk Hinv IH.
        revert He REC Hπk.
        generalize ((pc', k') :: pre). clear pc' k' pre.
        intros pre.
        revert acc'' g''.
        elim pre using rev_ind; clear pre.
        - simpl; intuition.
        - intros (pc', k') pre IH.
          intros acc' g'' He.
          rewrite fold_left_app. simpl.
          destruct (fold_left _ _ _) as [(vcs',g')|] eqn: Y. 2: discriminate.
          intros REC. rewrite in_app.
          intros [ IN | [?|()] ].
          + specialize (IH _ _ He eq_refl IN).
            revert REC.
            simpl.
            destruct (c ! pc') eqn: He'. 2: discriminate. simpl.
            destruct (vc_for_ghost _ _ _ _ _) as [(?, ?)|] eqn: REC. 2: discriminate.
            intros K; apply OK_inj, pair_eq_inv in K; destruct K as [-> ->].
            destruct IH as (h & h'' & vcs & vcs'' & IH' & MONO).
            apply vc_for_ghost_mono in REC. destruct REC as [REC _].
            eauto 10 using ghost_rel_trans.
          + clear IH.
            eq_some_inv. subst π k.
            revert REC. simpl. rewrite He. simpl.
            eauto 12 using ghost_rel_refl.
      }

      cut (∃ q (h h': hashmap _) vcs vcs' deco, In q ((pc', k') :: pre) ∧
                     In a' (h' π') ∧ ¬ In a' (h π') ∧
                     vc_for_ghost (fst q) deco vcs h fuel = OK (vcs', h') ∧ h' << g'').
      intros (q & h & h' & vcs & vcs' & deco' & Hq & Hh' & Hh & REC' & MONO).
      specialize (IH _ _ _ _ _ _ REC' _ _ _ _ Hinv He Hk _ Hh' Hh).
      destruct IH as [ IH | IH ]. left; exact IH. right.
      destruct d as [ d | d ]; simpl.
      apply MONO, IH.
      unfold ptree_get_all at 1. rewrite PTree.gsspec. case peq.
      intros ->; right; apply MONO, IH.
      intros _; apply MONO, IH.

      { revert REC.
        revert acc'' g'' D.
        apply not_nil_rev_ind.
        - intros acc' g' Hag'. simpl.
          destruct (predecessors_complete _ _ Hpre _ _ (or_introl _ eq_refl))
            as (e' & He' & He'k).
         rewrite He'. simpl.
         destruct (vc_for_ghost _ _ _ _ _) as [(acc'',g'')|] eqn: REC. 2: discriminate.
         intros K; apply OK_inj, pair_eq_inv in K; destruct K as [<- <-].
         exists (pc', k'). eauto 12 using ghost_rel_refl.

        - intros (pc'', k'') pre' IH'.
          intros acc'' g'' Hag'.
          rewrite fold_left_app. simpl.
          destruct (fold_left _ _ _) as [(vcs',g')|] eqn: Y. 2: discriminate.
          specialize (λ U, IH' _ _ U eq_refl).
          simpl.
          destruct (c ! pc'') eqn: He'. 2: discriminate. simpl.
          destruct (vc_for_ghost _ _ _ _ _) as [(?, ?)|] eqn: REC. 2: discriminate.
          intros K; apply OK_inj, pair_eq_inv in K; destruct K as [-> ->].
          case (in_dec eq_dec a' (g' π')).
          + intros IN. specialize (IH' IN).
            destruct IH' as (q & h & h'' & vcs & vcs'' & deco' & Hq & Hh' & Hh & IH' & MONO).
            eexists q, h, h'', vcs, vcs'', deco'.
            split. rewrite in_app. eauto. split. assumption.
            split. assumption. split. assumption.
            eapply ghost_rel_trans. eassumption.
            apply vc_for_ghost_mono in REC. apply REC.
          + intros NI.
            eexists (pc'', k''), g', g'', vcs', acc'', (Assertion _).
            split. rewrite in_app; right; left; reflexivity.
            split. assumption. split. assumption.
            split. eassumption. apply ghost_rel_refl.
      }

    + clear IH.
      intros K; apply OK_inj, pair_eq_inv in K; destruct K as [<- <-].
      destruct H as [ [ H -> ] | -> ]. 2: intuition.
      intros π e k π' H0 H1 H2 a'. simpl.
      unfold ptree_get_all. rewrite PTree.gso. intuition.
      destruct (predecessors_correct _ _ _ _ H1 H2) as (pre & Hpre' & K).
      congruence.
  - intros a' Hpc. apply not_nil_inv in Hpc.
    destruct Hpc as (i & inv & Hpc).
    intros K; apply OK_inj, pair_eq_inv in K; destruct K as [<- <-].
    simpl.
    intros π e k π' H H0 H1 a.
    unfold ptree_get_all. rewrite PTree.gso. 2: congruence. intuition.
Qed.

End PRED.

Definition doit (ep_annot: list (Sexpr.assertion reg)) fuel :=
  let pred := make_predecessors c in
  let epa := with_precondition ep_annot in
  do vc <- doit' pred epa fuel;
  OK (List.filter (λ a, if eq_dec True (simplify (snd a)) then false else true) vc).

Lemma doit_doit' ep_annot fuel :
  doit ep_annot fuel = OK nil →
  let pred := make_predecessors c in
  let epa := with_precondition ep_annot in
  ∃ vcs,
    doit' pred epa fuel = OK vcs ∧
    ∀ vc, In vc vcs → simplify (snd vc) = True.
Proof.
  unfold doit.
  case doit'. 2: discriminate.
  intros vcs. intros EQ. apply OK_inj in EQ.
  exists vcs. split. exact eq_refl.
  intros vc IN. generalize (In_filter (λ a, if eq_dec True (simplify (snd a)) then false else true) _ _ IN).
  rewrite EQ. clear EQ. intros H. apply reflect_iff in H. revert H.
  case eq_dec. auto. intros _ (). intros _ K; elim (K eq_refl).
Qed.

Section CORRECT.

  Context
          (epa: list (Sexpr.assertion reg))
          (fuel: nat).

  Definition garland_annot (garland: hashmap _) : Prop :=
    ∀ n a, In a (get_assertions annot n) → In a (garland n).

  Definition garland_invariant (garland: hashmap _) : Prop :=
    ∀ n, get_invariant n ≠ nil →
         ∀ a, In a (garland n) → simplify (with_precondition (get_invariant n) a) = True.

  Definition garland_init (garland: hashmap _) : Prop :=
    match get_invariant xH with
    | nil => ∀ a, In a (garland xH) → simplify (with_precondition epa a) = True
    | inv => ∀ a, In a inv → simplify (with_precondition epa a) = True
    end.

  Definition garland_step (garland: hashmap (Sexpr.assertion reg)) : Prop :=
    ∀ π e π' k,
      c ! π = Some e →
      step_exit_compat e π' k →
      ∀ a, In a match get_invariant π' with nil => garland π' | inv => inv end → trivial_or_in (wp e k a) (garland π).

  Lemma in_get_invariant a pc :
    In a (get_invariant pc) →
    ∃ deco, annot ! pc = Some deco ∧ In (Invariant a) deco.
Proof.
    unfold get_invariant. destruct (annot ! _). 2: intros ().
    rewrite in_rev_map_o, in_map_iff.
    intros (). intros [ i | x ] [H H']; eq_some_inv. subst. eauto.
  Qed.

  Lemma zcorrect :
    doit epa fuel = Errors.OK nil →
    ∃ garland: hashmap (Sexpr.assertion reg),
      garland ∈ (garland_annot ∩ garland_invariant ∩ garland_init ∩ garland_step).
Proof.
    Opaque Pos.eqb.
    intros H. apply doit_doit' in H.
    destruct H as (vcs & H & Hvcs').
    assert (∀ pc vc, In (pc, vc) vcs → simplify vc = True) as Hvcs by (intros pc vc; exact (Hvcs' (pc, vc))).
    clear Hvcs'.
    apply doit'_has_ghost in H.
    destruct H as (g & H).
    assert (garland_invariant g) as g_invariant.
    {
      intros n A a Ha.
      cut (∃ pc, In (pc, with_precondition (get_invariant n) a) vcs). intros (). intros pc. apply Hvcs.
      clear Hvcs.
      revert H n A a Ha.
      apply doit'_ghost_intro.
      intros m _ _. revert vcs g.
      elim m using rev_ind; clear m.
      intros vcs g H; apply OK_inj, pair_eq_inv in H. destruct H as (H & <-).
      intros n _ a. unfold ptree_get_all. rewrite PTree.gempty. intros ().
      intros (pc, d) m IH vcs g.
      rewrite fold_left_app. simpl.
      destruct (fold_left _ _ _) as [ (vcs', g') | ? ]. 2: discriminate.
      specialize (IH _ _ eq_refl).
      simpl. destruct (vc_for_ghost _ _ _ _ _ _ _) as [ (vcs'', g'') | ] eqn: H. 2: discriminate.
      intros K; apply OK_inj, pair_eq_inv in K. destruct K as [ <- -> ].
      intros n A a Ha.
      specialize (IH n A).
      rewrite rev_map_app_correct. setoid_rewrite in_app. setoid_rewrite <- in_rev.
      setoid_rewrite in_map_iff.
      cut (In (with_precondition (get_invariant n) a) vcs'' ∨ In a ((g': hashmap _) n)).
      { clear -IH. intros (). eauto. intros IN. destruct (IH _ IN). eauto. }
      clear IH.
      revert H.
      generalize (@nil (Sexpr.assertion reg)). intros acc H.
      revert pc d acc g' vcs'' g H Ha.
      elim fuel; clear fuel. discriminate.
      intros fuel IH' pc d acc g' vcs g.
      unfold vc_for_ghost. apply vc_for_case_ind.
      + intros d' a' H.
        destruct (_ ! _) as [ [ | (pc', k) [| x pre ] ] | ].
        * intros K; apply OK_inj, pair_eq_inv in K. destruct K as [<- <-].
          destruct H as [ [H ->] | -> ].
          unfold ptree_get_all. rewrite PTree.gso. auto. congruence.
          auto.
        * destruct (c ! pc') as [ e | ]. 2: discriminate.
          simpl.
          case proj_sumbool.
          { intros K; apply OK_inj, pair_eq_inv in K. destruct K as [<- <-].
            destruct H as [ [H ->] | -> ].
            unfold ptree_get_all. rewrite PTree.gso. auto. congruence. auto. }
          fold (vc_for_ghost (make_predecessors c) (with_precondition epa) pc' (Assertion (wp e k a'))).
          specialize (IH' pc' (Assertion (wp e k a')) (if (pc =? 1)%positive then with_precondition epa match d' with Invariant a | Assertion a => a end :: acc else acc) g').
          destruct (vc_for_ghost _ _ _ _ _ _ _) as [ (vcs'', g'') | ]. 2: discriminate.
          specialize (IH' _ _ eq_refl).
          intros K. apply OK_inj, pair_eq_inv in K. destruct K as [<- <-].
          destruct H as [ [H ->] | -> ].
          unfold ptree_get_all. rewrite PTree.gso. 2: congruence.
          intros Ha. destruct IH'; eauto. auto.
        * generalize ((pc', k) :: x :: pre). clear pc' k x pre.
          fold (vc_for_ghost (make_predecessors c) (with_precondition epa)).
          intros pre. revert vcs g.
          elim pre using rev_ind; clear pre.
          intros vcs g.
          simpl. intros K; apply OK_inj, pair_eq_inv in K. destruct K as [<- <-].
          destruct H as [ [H ->] | -> ].
          unfold ptree_get_all. rewrite PTree.gso. auto. congruence. auto.

          intros (pc', k) pre IH vcs g.
          rewrite fold_left_app. simpl.
          destruct (fold_left _ _ _) as [ (vcs'', g'') | ]. 2: discriminate.
          simpl.
          destruct (c ! _). 2: discriminate.
          simpl.
          specialize (IH' pc' (Assertion (wp e k a')) vcs'' g'').
          simpl in IH. specialize( IH _ _ eq_refl).
          destruct (vc_for_ghost _ _ _ _ _ _ _) as [ (vcs''', g''') |] eqn: REC. 2: discriminate.
          specialize (IH' _ _ eq_refl).
          apply vc_for_ghost_mono in REC.
          intros K; apply OK_inj, pair_eq_inv in K. destruct K as [<- <-].
          destruct H as [ [H ->] | -> ]. revert IH.
          unfold ptree_get_all. assert (n ≠ pc) by congruence. rewrite ! PTree.gso; auto.
          intros IH Ha. destruct IH'; auto. destruct IH; auto.
          left. apply REC. auto.
          intros Ha. destruct IH'; auto. destruct IH; auto.
          left. apply REC. auto.
        * intros K; apply OK_inj, pair_eq_inv in K. destruct K as [ <- <- ].
          destruct H as [ [H ->] | -> ]; auto.
          unfold ptree_get_all. rewrite PTree.gso. 2: congruence. auto.

      + intros a' Hinv H. apply OK_inj, pair_eq_inv in H. destruct H as [<- <- ].
        unfold ptree_get_all. rewrite PTree.gsspec. destruct peq. subst.
        intros [ -> | Ha ]. simpl. auto. right. auto.
        right. auto.
    }

    exists g.
    split. split. split.

    - clear -H. unfold garland_annot.
      intros n a Ha.
      assert (∃ deco, annot ! n = Some deco ∧ In (Assertion a) deco) as Ha'.
      { revert Ha. clear.
        unfold get_assertions, ptree_get_all. rewrite in_rev_map_o, in_map_iff.
        intros (). intros (); intros; hsplit; eq_some_inv. subst.
        destruct (annot ! _). eauto. eelim in_nil; eauto.
      } clear Ha.
      destruct Ha' as (deco & Hdeco & Ha).
      revert H.
      apply doit'_ghost_intro.
      intros m H _.
      specialize (H _ _ _ Hdeco Ha). revert H. clear.
      revert vcs g.
      elim m using rev_ind; clear m. intros _ _ ().
      intros (pc, d) m IH vcs g IN.
      rewrite fold_left_app. simpl.
      destruct (fold_left _ _ _) as [ (vcs', g') | ]. 2: discriminate.
      rewrite in_app in IN; destruct IN as [ IN | [ H | () ] ].
      specialize (IH _ _ IN eq_refl).
      simpl.
      generalize (vc_for_ghost_mono (make_predecessors c) (with_precondition epa) pc d nil g' fuel).
      case vc_for_ghost. 2: discriminate.
      intros (vcs'', g'') H. specialize (H _ _ eq_refl).
      intros K; apply OK_inj in K. inv K. apply H, IH.
      inv H. simpl.
      generalize (vc_for_ghost_has_vc (make_predecessors c) (with_precondition epa) n a nil g' fuel).
      case (vc_for_ghost _). 2: discriminate.
      intros (?, ?) IN. specialize (IN _ _ eq_refl). intros H; apply OK_inj in H. inv H. exact IN.

    - assumption.

    - red.
      cut ((get_invariant xH = nil ∧ ∀ a, In a (g xH) → ∃ pc, In (pc, with_precondition epa a) vcs) ∨
           (not_nil (get_invariant xH) ∧ ∀ a, In a (get_invariant xH) → ∃ pc, In (pc, with_precondition epa a) vcs)).
      { clear -Hvcs.
        intros (). intros (). intros -> H a Ha. destruct (H a Ha). eauto.
        intros (). intros NN. apply not_nil_inv in NN. hsplit. rewrite NN.
        intros H b Ha. destruct (H _ Ha). eauto. }
      clear Hvcs g_invariant.
      destruct (get_invariant _) as [ | i inv ] eqn:Hi; [ left | right ].
      + split. reflexivity.
        revert vcs g H.
        apply doit'_ghost_intro.
        intros m _ _.
        elim m using rev_ind; clear m.
        intros vcs g K.
        apply OK_inj, pair_eq_inv in K. destruct K as [<- <-]. simpl. intros _ ().
        intros (pc, d) m IH vcs g.
        rewrite fold_left_app. simpl.
        destruct (fold_left _ _ _) as [(vcs', g') | ]. 2: discriminate.
        specialize (IH _ _ eq_refl). simpl.
        destruct (vc_for_ghost _ _ _ _ _ _ _ ) as [(vcs'', g'') | ] eqn: REC. 2: discriminate.
        intros K; apply OK_inj, pair_eq_inv in K. destruct K as [<- <-].
        intros a Ha.
        cut (In (with_precondition epa a) vcs'' ∨ In a ((g': hashmap _) xH)).
        { clear -IH. intros (); intros H; [ | destruct (IH _ H) ];
                       eexists; rewrite rev_map_app_correct, in_app; eauto.
          left. rewrite <- in_rev, in_map_iff. eauto. }
        clear IH vcs'.
        revert REC Ha.
        revert g' vcs'' g''.
        generalize (@nil (Sexpr.assertion reg)).
        revert pc d.
        elim fuel; clear fuel. discriminate.
        intros fuel IH pc d acc g vcs' g'.
        unfold vc_for_ghost. apply vc_for_case_ind.
        * {
          intros d' a' H.
          destruct (_ ! _) as [ [ | (pc', k) [ | x pre ] ] | ].
          - intros K; apply OK_inj, pair_eq_inv in K. destruct K as [<- <-].
            destruct H as [ [H ->] | -> ].
            unfold ptree_get_all. rewrite PTree.gsspec. case peq.
            intros <-. rewrite Pos.eqb_refl.
            intros [ <- | IN ]. left; left; reflexivity. auto. auto. auto.
          - destruct (_ ! _). 2: discriminate.
            fold (vc_for_ghost (make_predecessors c) (with_precondition epa)).
            simpl. destruct proj_sumbool.
            intros K; apply OK_inj, pair_eq_inv in K. destruct K as [<- <-].
            destruct H as [ [H ->] | -> ].
            unfold ptree_get_all. rewrite PTree.gsspec. case peq.
            intros <-. rewrite Pos.eqb_refl.
            intros [ <- | IN ]. left; left; reflexivity. auto. auto. auto.
            specialize (IH pc' (Assertion (wp e k a')) (if (pc =? 1)%positive then with_precondition epa match d' with Invariant a | Assertion a => a end :: acc else acc) g).
            destruct (vc_for_ghost _ _ _ _ _ _ _) as [(vcs'', g'')|] eqn: REC. 2: discriminate.
            intros K; apply OK_inj, pair_eq_inv in K. destruct K as [<- <-].
            specialize (IH _ _ eq_refl).
            destruct H as [ [H ->] | -> ].
            unfold ptree_get_all. rewrite PTree.gsspec. case peq.
            intros <-. rewrite Pos.eqb_refl in REC.
            apply vc_for_ghost_mono in REC.
            intros [ <- | IN ]. left. apply REC. left; reflexivity. auto. auto. auto.
          - destruct (fold_left _ _ _) as [(vc''', g''')|] eqn: REC. 2: discriminate.
            intros K; apply OK_inj, pair_eq_inv in K. destruct K as [<- <-].
            revert vc''' g''' REC.
            fold (vc_for_ghost (make_predecessors c) (with_precondition epa)).
            generalize ((pc', k) :: x :: pre). clear pc' k x pre.
            intros pre. elim pre using rev_ind; clear pre.
            + intros vcs g'.
              intros K; apply OK_inj, pair_eq_inv in K. destruct K as [<- <-].
              destruct H as [ [H ->] | -> ].
              unfold ptree_get_all. rewrite PTree.gsspec. case peq.
              intros <-. rewrite Pos.eqb_refl.
              intros [ <- | IN ]. left; left; reflexivity. auto. auto. auto.
            + intros (pc', k) pre IH' vcs g'.
              rewrite fold_left_app.
              simpl.
              destruct (fold_left _ _ _) as [(vcs'', g'')|]. 2: discriminate.
              specialize (IH' _ _ eq_refl).
              simpl. destruct (_ ! _). 2: discriminate.
              simpl. intros REC.
              specialize (IH _ _ _ _ _ _ REC).
              apply vc_for_ghost_mono in REC.
              destruct H as [ [H ->] | -> ].
              * revert IH'.
                unfold ptree_get_all. rewrite ! PTree.gsspec. case peq.
                intros <- IH'.
                intros [ <- | IN ].
                destruct IH'; auto. left; reflexivity.
                left. apply REC. auto.
                destruct (IH IN). auto.
                destruct IH'. right. auto. left. apply REC; auto. auto.
                intros n IH' Ha.
                destruct (IH Ha). auto.
                destruct IH'; auto. left. apply REC. auto.
              * intros Ha; destruct (IH Ha); auto.
                destruct IH'; auto.
                left; apply REC; auto.
          - intros K; apply OK_inj, pair_eq_inv in K. destruct K as [<- <-].
            destruct H as [ [H ->] | -> ].
            unfold ptree_get_all. rewrite PTree.gsspec. case peq.
            intros <-. rewrite Pos.eqb_refl.
            intros [ <- | IN ]. left; left; reflexivity. auto. auto. auto.
          }
        * intros a' H REC.
          apply OK_inj, pair_eq_inv in REC. destruct REC as [<- <-].
          unfold ptree_get_all. rewrite PTree.gso. auto.
          intros <-. rewrite Hi in H. exact H.

      + split. exact I.
        intros a.
        rewrite <- Hi. intros X.
        clear i inv Hi.
        destruct (in_get_invariant _ _ X) as (deco & Hdeco & Hi).
        
        revert H deco Hdeco Hi.
        apply doit'_ghost_intro.
        intros m H _.
        intros H0 deco Hdeco Hi.
        specialize (H _ _ _ Hdeco Hi). clear deco Hdeco Hi.
        revert vcs g H0 H.
        elim m using rev_ind; clear m.
        intros ? ? _ ().
        intros (pc, d) m IH vcs g.
        rewrite fold_left_app. simpl.
        destruct (fold_left _ _ _) as [(vcs', g')|]. 2: discriminate.
        specialize (IH _ _ eq_refl). simpl.
        destruct (vc_for_ghost _ _ _ _ _ _ _) as [(vcs'', g'')|] eqn: R. 2: discriminate.
        intros K; apply OK_inj, pair_eq_inv in K. destruct K as [<- <-].
        rewrite in_app. intros [ IN | [ ? | () ] ].
        specialize (IH IN). destruct IH as (pc' & IH).
        apply vc_for_ghost_mono in R.
        exists pc'. rewrite rev_map_app_correct.
        apply in_app; right. exact IH.
        eq_some_inv; subst.
        clear IH.
        exists xH. rewrite rev_map_app_correct, in_app. left.
        rewrite <- in_rev. apply in_map.
        revert R.
        case fuel; clear fuel. discriminate.
        intros fuel. unfold vc_for_ghost.
        fold (vc_for_ghost (make_predecessors c) (with_precondition epa)).
        unfold vc_for_case.
        destruct (get_invariant _). destruct X.
        destruct (_ ! _) as [ [ | (pc', k) [ | x pre ] ] | ].
        * intros K; apply OK_inj, pair_eq_inv in K. destruct K as [<- <-].
          rewrite Pos.eqb_refl; left; reflexivity.
        * destruct (_ ! _). 2: discriminate.
          rewrite Pos.eqb_refl.
          simpl. destruct proj_sumbool.
          intros K; apply OK_inj, pair_eq_inv in K. destruct K as [<- <-]. left; reflexivity.
          destruct (vc_for_ghost _ _ _ _ _ _ _) as [(vcs''', g''')|] eqn: REC. 2: discriminate.
          intros K; apply OK_inj, pair_eq_inv in K. destruct K as [<- <-].
          apply vc_for_ghost_mono in REC. apply REC; left; reflexivity.
        * destruct (fold_left _ _ _) as [(vc''', g''')|] eqn: REC. 2: discriminate.
          intros K; apply OK_inj, pair_eq_inv in K. destruct K as [<- <-].
          revert REC.
          rewrite Pos.eqb_refl.
          revert vc''' g'''.
          generalize ((pc', k) :: x :: pre). clear pc' k x pre.
          intros pre. elim pre using rev_ind; clear pre.
          clear.
          intros vcs g.
          intros K; apply OK_inj, pair_eq_inv in K. destruct K as [<- <-]. left; reflexivity.
          intros (pc', k) pre IH vcs g.
          rewrite fold_left_app.
          simpl.
          destruct (fold_left _ _ _) as [(vcs'', g'')|]. 2: discriminate.
          simpl. destruct (_ ! _). 2: discriminate.
          intros REC. simpl in REC. apply vc_for_ghost_mono in REC.
          apply REC, (IH _ _ eq_refl).
        * rewrite Pos.eqb_refl. intros K; apply OK_inj, pair_eq_inv in K.
          destruct K as [<- <-]; left; reflexivity.

    - clear g_invariant Hvcs.
      revert vcs g H.
      apply doit'_ghost_intro.
      intros m Hannot _.
      intros vcs g H π e π' k H0 H1 a H2.
      assert (match get_invariant π' with nil => In a (g π') | inv => In a inv ∧ In (π', Invariant a) m end) as Ha.
      generalize (in_get_invariant a π').
      destruct (get_invariant π'). auto.
      intros X; destruct (X H2) as (deco & Hdeco & Ha). eauto.
      clear Hannot H2.
      revert vcs g H π e π' k H0 H1 a Ha.
      elim m using rev_ind; clear m.
      intros vcs g K; apply OK_inj, pair_eq_inv in K; destruct K as [<- <-].
      intros π e π' k He Hek a Ha. exfalso.
      destruct get_invariant. unfold ptree_get_all in Ha. rewrite PTree.gempty in Ha. exact Ha.
      intuition.
      intros (pc, deco) ann IH vcs g. rewrite fold_left_app. simpl.
      destruct (fold_left _ ann _) as [ (acc, g') | ] eqn: X. 2: discriminate.
      specialize (IH acc g' X). clear X. simpl.
      destruct (vc_for_ghost _ _ _ _ _ _ _) as [(acc', g'')|] eqn: REC. 2: discriminate.
      intros K; apply OK_inj, pair_eq_inv in K; destruct K as [<- <-].
      intros π e π' k H0 H1 a Ha.
      destruct (get_invariant π') as [ | i inv ] eqn: Hi.
      + specialize (IH _ _ _ _ H0 H1 a). rewrite Hi in IH.
        destruct (in_dec eq_dec a ((g' :hashmap _) π')) as [IN | NI].
        specialize (IH IN). destruct IH as [IH|IH]. left; exact IH.
        right. apply vc_for_ghost_mono in REC. apply REC, IH.
        clear IH.
        eauto using vc_for_ghost_step, make_predecessors_correct, make_predecessors_complete.

      + destruct Ha as [ Hai Ha ].
        rewrite in_app in Ha. destruct Ha as [ Ha | [ Ha | () ] ].
        * specialize (IH π e π' k H0 H1 a). rewrite Hi in IH.
          specialize (IH (conj Hai Ha)).
          destruct IH. left; assumption.
          right.
          apply vc_for_ghost_mono in REC. apply REC. assumption.
        * { eq_some_inv; hsplit; subst pc deco.
            clear IH.
            revert REC. case fuel; clear fuel. discriminate.
            intros fuel.
            unfold vc_for_ghost.
            fold (vc_for_ghost (make_predecessors c) (with_precondition epa)).
            unfold vc_for_case.
            rewrite Hi.
            destruct (make_predecessors_correct _ _ _ _ H0 H1) as (pre & Hpre & He).
            rewrite Hpre.
            destruct pre as [ | (pc', k') [ | x pre ] ].
            - elim He.
            - destruct He as [ He | () ]. eq_some_inv. subst pc' k'.
              rewrite H0. simpl.
              destruct (proj_sumbool _) eqn: H.
              intros K; apply OK_inj, pair_eq_inv in K; destruct K as [<- <-].
              left. symmetry; apply eq_dec_eq, H.
              destruct (vc_for_ghost _ _ _ _ _ _ _) as [(?, ?) |] eqn: REC. 2: discriminate.
              apply vc_for_ghost_has_vc in REC.
              intros K; apply OK_inj, pair_eq_inv in K; destruct K as [<- <-].
              right. exact REC.
            - clear Hpre.
              revert He.
              generalize ((pc', k') :: x :: pre). clear pc' k' x pre.
              intros m.
              revert acc' g''.
              elim m using rev_ind; clear m.
              intros _ _ ().
              intros (pc', k') m IH acc'' g'' IN.
              rewrite in_app in IN.
              rewrite fold_left_app. simpl.
              destruct (fold_left _ _ _) as [(acc''',g''')|]. 2: discriminate.
              simpl. destruct (c ! pc') eqn: Hpc'. 2: discriminate.
              simpl.
              destruct (vc_for_ghost _ _ _ _ _ _ _) as [(?, ?) |] eqn: REC. 2: discriminate.
              intros K; apply OK_inj, pair_eq_inv in K; destruct K as [<- <-].
              simpl in IH.
              destruct IN as [IN | [IN | () ]].
              specialize (IH _ _ IN eq_refl).
              destruct IH as [IH|IH]. left; exact IH. right.
              apply vc_for_ghost_mono in REC. apply REC, IH.
              eq_some_inv; subst pc' k'.
              apply vc_for_ghost_has_vc in REC.
              right. congruence.
          }
  Qed.

  Theorem correct :
    doit epa fuel = Errors.OK nil →
    ∀ fs sp perm,
    well_annotated_function _ fs sp perm (Function c xH)
                            (get_assertions annot)
                            (pre_of_assertion_list _ fs sp perm epa).
Proof.
    intros OK fs sp perm.
    destruct (zcorrect OK) as (garland & ((Hannot & Hinvariant) & Hinit) & Hstep).
    apply (invariant_weaken (well_annotated_state reg_dec fs sp perm garland)).
    - intros (). 2: exact id.
      intros [π ϱ] H a Ha; apply H, Hannot, Ha.
    - apply invariant_ind.
      + intros s ([π ϱ] & -> & ? & PRE). simpl in *. subst π.
        intros a Ha.
        specialize (Hinvariant xH). red in Hinit.
        destruct (get_invariant _).
        * specialize (Hinit a Ha).
          apply (simplify_is_true fs sp perm ϱ) in Hinit.
          apply eval_with_precondition in Hinit; assumption.
        * eapply (simplify_is_true fs sp perm ϱ) in Hinvariant; eauto. 2: intro; eq_some_inv.
          apply eval_with_precondition in Hinvariant. assumption.
          intros i H. specialize (Hinit i H).
          apply (simplify_is_true fs sp perm ϱ) in Hinit.
          apply eval_with_precondition in Hinit; assumption.

      + intros (). 2: easy.
        intros [π ϱ] REACH WAS (). 2: repeat intro; exact I.
        intros [π' ϱ'] STEP.
        generalize (step_has_exit_compat _ _ _ _ _ _ _ _ STEP).
        intros (e & k & He & Hk). simpl in He.
        intros a; simpl. intros Ha.
        generalize (Hstep _ _ _ _ He Hk). clear Hstep.
        assert (∀ a, trivial_or_in (wp e k a) (garland π) → eval_assertion reg_dec fs sp perm ϱ' a)
          as Hcut.
        {
          intros a' [ WP | WP ];
          [ apply (simplify_is_true fs sp perm ϱ) in WP |
            specialize (WAS _ WP); simpl in WAS ];
          eapply wp_sound; try eassumption; exact He.
        }
        specialize (Hinvariant π'). destruct (get_invariant _).
        auto.
        intros H.
        eapply (simplify_is_true fs sp perm ϱ') in Hinvariant; eauto. 2: intro; eq_some_inv.
        apply eval_with_precondition in Hinvariant. assumption.
        auto.
  Qed.

End CORRECT.

End REGISTER.
Generated by coq2html