Module PolAdomZ

This module implements the AbIdealEnv.ab_ideal_env interface of abtract domains on ideal numbers.

Require Import ZArith_base.
Require CExprPedraZ.
Import NumC ProgVar Itv.
Require Import AdomLib Util FastArith.
Require Import IdealExpr.
Require Import IdealIntervals ZIntervals.
Require Import AbIdealEnv.
Require Import FactMsgHelpers.
Require Import String.
Require Import ToString.
Require Import CellEncoding.

Instance v2p : injection var positive :=
  fun vg => Pos.pred (match vg with Real x => xO (inj x) | Ghost x => xI x end).

Instance p2v : injection positive var :=
  fun p =>
    match Pos.succ p with
    | xO x => Real (inj x)
    | xI x => Ghost x
    | xH => Ghost xH
    end.

Instance BIJ : bijection v2p p2v.
Proof.
  split; intros; unfold inj, p2v, v2p.
  - rewrite Pos.succ_pred. destruct a. rewrite forward. auto. auto.
    destruct a; discriminate.
  - destruct (Pos.succ b) eqn:EQ.
    rewrite <- EQ. apply Pos.pred_succ.
    rewrite backward, <- EQ. apply Pos.pred_succ.
    destruct b; discriminate.
Qed.

Local Open Scope Z_scope.

Local Notation zmemT := (Mem.t ZNum.t).

Definition liftN (dummy: ZNum.t) (n: ideal_num): ZNum.t
  := match n with
         | INf _ => dummy
         | INz z => z
     end.

Definition liftRho (rho: var -> ideal_num) (dummy: ZNum.t): zmemT
  := fun x => liftN dummy (rho (p2v x)).

Definition cmpTrans : Integers.comparison -> CExprPedraZ.Cmp.t
  := fun cmp =>
       match cmp with
       | Integers.Ceq => CExprPedraZ.Cmp.Eq
       | Integers.Cne => CExprPedraZ.Cmp.Neq
       | Integers.Clt => CExprPedraZ.Cmp.Lt
       | Integers.Cle => CExprPedraZ.Cmp.Le
       | Integers.Cgt => CExprPedraZ.Cmp.Gt
       | Integers.Cge => CExprPedraZ.Cmp.Ge
       end.

Import Datatypes.
Lemma CmpTransTrue : forall (cmp : Integers.comparison),
                   forall z1 z2 : Z,
                     Zcmp cmp z1 z2 = true -> CExprPedraZ.Cmp.denote (cmpTrans cmp) z1 z2.
Proof.
  intros cmp z1 z2 hyp.
  assert (fact : match z1 ?= z2 with
                   | Eq => z1 = z2
                   | Lt => z1 < z2
                   | Gt => z1 > z2
                 end).
  apply Zcompare_elim; trivial.
  destruct cmp; simpl; simpl in hyp; destruct (z1 ?= z2);
  try discriminate; try assumption.
  intro contr.
  subst.
  apply Z.lt_irrefl in fact.
  contradiction.
  intro contr.
  subst.
  apply Z.gt_lt in fact.
  apply Z.lt_irrefl in fact.
  contradiction.
  subst.
  apply Z.le_refl.
  apply Z.lt_le_incl.
  assumption.
  apply Z.gt_lt in fact.
  assumption.
  subst.
  apply Z.le_refl.
  apply Z.gt_lt in fact.
  apply Z.lt_le_incl in fact.
  assumption.
Qed.

Lemma CmpTransFalse : forall (cmp: Integers.comparison),
                      forall z1 z2 : Z,
                        Zcmp cmp z1 z2 = false ->
                        ~ CExprPedraZ.Cmp.denote (cmpTrans cmp) z1 z2.
Proof.
  intros cmp z1 z2 hyp contr.
  assert (fact : match z1 ?= z2 with
                 | Eq => z1 = z2
                 | Lt => z1 < z2
                 | Gt => z1 > z2
                 end).
  apply Zcompare_elim; trivial.
  destruct cmp; simpl in hyp; simpl in contr; destruct (z1 ?= z2); try discriminate.
  subst.
  apply Z.lt_irrefl in fact.
  contradiction.
  subst.
  apply Z.gt_lt, Z.lt_irrefl in fact.
  contradiction.
  contradiction (contr fact).
  subst.
  apply Z.lt_irrefl in contr.
  contradiction.
  apply Z.lt_asymm in contr.
  apply Z.gt_lt in fact.
  contradiction (contr fact).
  apply Z.gt_lt in fact.
  apply Zle_lt_or_eq in contr.
  destruct contr.
  apply (Z.lt_trans z1 z2 z1) in fact.
  apply Z.lt_irrefl in fact.
  contradiction.
  assumption.
  subst.
  apply Z.lt_irrefl in fact.
  contradiction.
  subst.
  apply Z.lt_irrefl in contr.
  contradiction.
  apply (Z.lt_trans z1 z2 z1) in contr.
  apply Z.lt_irrefl in contr.
  contradiction.
  assumption.
  apply Zlt_not_le in fact.
  contradiction (fact contr).
Qed.

Lemma CmpTransPreservation : forall (cmp: Integers.comparison) (z1 z2 : Z),
                               (if Zcmp cmp z1 z2 return Zfast then F1 else F0) =
                               ((if CExprPedraZ.Cmp.dec (cmpTrans cmp) z1 z2 then 1 else 0):Zfast).
Proof.
  intros cmp z1 z2.
  assert (fact1 := CmpTransTrue cmp z1 z2).
  assert (fact2 := CmpTransFalse cmp z1 z2).
  destruct (Zcmp cmp z1 z2);
  destruct (CExprPedraZ.Cmp.dec (cmpTrans cmp) z1 z2).
  reflexivity.
  contradiction n. apply fact1; reflexivity.
  refine (match fact2 _ d with end). reflexivity.
  reflexivity.
Qed.

Definition ItvTrSpec (i1: zitv) (i2: ZItv.t): Prop
  := forall z: Z.t, γ i1 z <-> ZItv.sat i2 z.

Definition itvTr (i1: zitv): {i2: ZItv.t | ItvTrSpec i1 i2}.
  refine (
      match i1
            return {i2: ZItv.t | ItvTrSpec i1 i2}
      with
        | ZITV z1 z2 =>
          exist _ (proj1_sig (ZItv.mk (ZItv.Closed z1) (ZItv.Closed z2))) _
      end);
  unfold ItvTrSpec;
  intro z;
  split;
  intro h;
  simpl; try easy.
  - destruct (ZNum.ltLeDec z2 z1) as [h1|h1].
    + assert (h2 := h1).
      apply Zlt_not_le in h2.
      destruct h2.
      apply Z.le_trans with (m := z);
        apply h.
    + simpl.
      assumption.
  - simpl in h.
    destruct (ZNum.ltLeDec z2 z1) as [h1|h1].
    + destruct h.
    + simpl in h.
      assumption.
Defined.

Fixpoint iexprTr (ie : iexpr) : CExprPedraZ.Expr.t
  := match ie with
       | IEvar INTz x => CExprPedraZ.Expr.Evar (v2p x)
       | IEvar INTf x => CExprPedraZ.Expr.Eunknown
       | IEconst (INz z) => CExprPedraZ.Expr.Econst z
       | IEconst _ => CExprPedraZ.Expr.Eunknown
       | IEZitv itv => CExprPedraZ.Expr.Eitv (proj1_sig (itvTr itv))
       | IEunop op ie' =>
         let e' := iexprTr ie' in
         match op with
           | IOneg => CExprPedraZ.Expr.Eunop CExprPedraZ.Expr.Oneg e'
           | IOnot => CExprPedraZ.Expr.Eunop CExprPedraZ.Expr.Onot e'
           | _ => CExprPedraZ.Expr.Eunknown
         end
       | IEbinop op ie1 ie2 =>
         let e1 := iexprTr ie1 in
         let e2 := iexprTr ie2 in
         match op with
           | IOadd => CExprPedraZ.Expr.Ebinop CExprPedraZ.Expr.Oadd e1 e2
           | IOsub => CExprPedraZ.Expr.Ebinop CExprPedraZ.Expr.Osub e1 e2
           | IOmul => CExprPedraZ.Expr.Ebinop CExprPedraZ.Expr.Omul e1 e2
           | IOdiv => CExprPedraZ.Expr.Ebinop CExprPedraZ.Expr.Odiv e1 e2
           | IOmod => CExprPedraZ.Expr.Ebinop CExprPedraZ.Expr.Omod e1 e2
           | IOand => CExprPedraZ.Expr.Ebinop CExprPedraZ.Expr.Oand e1 e2
           | IOor => CExprPedraZ.Expr.Ebinop CExprPedraZ.Expr.Oor e1 e2
           | IOxor => CExprPedraZ.Expr.Ebinop CExprPedraZ.Expr.Oxor e1 e2
           | IOshl => CExprPedraZ.Expr.Ebinop CExprPedraZ.Expr.Oshl e1 e2
           | IOshr => CExprPedraZ.Expr.Ebinop CExprPedraZ.Expr.Oshr e1 e2
           | IOcmp c => CExprPedraZ.Expr.Ebinop (CExprPedraZ.Expr.Ocmp (cmpTrans c)) e1 e2
           | _ => CExprPedraZ.Expr.Eunknown
         end
     end.

Lemma IExprTrPreservationInF :
  forall (ie : iexpr) (m : var -> ideal_num) (f: Floats.float),
    eval_iexpr m ie (INf f) -> iexprTr ie = CExprPedraZ.Expr.Eunknown.
Proof.
  intros ie m f hyp.
  induction ie; inversion hyp; subst.
  - destruct i; reflexivity || inversion H3.
  - reflexivity.
  - destruct i; reflexivity || inversion H3.
  - destruct i; reflexivity || inversion H5.
Qed.

Lemma IExprTrPreservationInZ :
  forall (ie : iexpr) (m : var -> ideal_num) (z : Z) (dummy : Z),
    eval_iexpr m ie (INz z) -> CExprPedraZ.Expr.denote (liftRho m dummy) (iexprTr ie) z.
Proof.
  intros ie m z dummy.
  revert z.
  induction ie; intros zz hyp; inversion hyp; subst.
  - destruct i; [|inversion H3].
    constructor.
    unfold liftRho.
    rewrite BIJ.(@forward _ _ _ _), H1.
    reflexivity.
  - constructor.
  - constructor. destruct itvTr. apply i, H1.
  - destruct n as [|[]]; [inversion H3|].
    + constructor.
    + destruct i; simpl; try constructor.
      * apply CExprPedraZ.Expr.EvalEunop with (z1 := x).
        apply IHie.
        assumption.
        inversion H3.
        constructor.
      * apply CExprPedraZ.Expr.EvalEunop with (z1 := x).
        apply IHie.
        assumption.
        inversion H3.
        constructor.
  - destruct n1 as [|[]].
    inversion H5.
    constructor.
    destruct n2 as [|[]].
    inversion H5.
    destruct i; simpl; try constructor;
    apply CExprPedraZ.Expr.EvalEbinop with (z1 := x) (z2 := x0);
    try (apply IHie1; assumption) || (apply IHie2; assumption);
    inversion H5;
    try constructor.
    assumption.
    assumption.
    rewrite CmpTransPreservation in H6. inversion H6.
    constructor.
Qed.

Lemma IExprTrPreservation :
  forall (dummy : Z) (ie : iexpr) (m : var -> ideal_num) (n : ideal_num),
    eval_iexpr m ie n -> CExprPedraZ.Expr.denote (liftRho m dummy) (iexprTr ie) (liftN dummy n).
Proof.
  intros dummy ie m n hyp.
  destruct n as [f|[z]].
  replace (iexprTr ie) with CExprPedraZ.Expr.Eunknown.
  constructor.
  symmetry.
  apply IExprTrPreservationInF with (m := m) (f := f).
  assumption.
  apply IExprTrPreservationInZ.
  assumption.
Qed.

Definition A: Type
  := CExprPedraZ.AbDom.A.

Definition B: Type
  := var -> ideal_num.

Definition gamma: A -> B -> Prop
  := fun ab rho => CExprPedraZ.AbDom.gamma ab (liftRho rho ZNum.z).

Instance PolGammaOp: gamma_op A B := gamma.

Lemma gamma_monotone: forall (ab1:A*query_chan) (ab2: A) (rho:B),
                        CExprPedraZ.AbDom.leb (fst ab1) ab2 = true ->
                        γ ab1 rho -> gamma ab2 rho.
Proof.
  unfold gamma.
  intros ab1 ab2 h rho [H _]. revert H.
  apply CExprPedraZ.AbDom.gamma_monotone.
  assumption.
Qed.

Lemma gamma_top: forall x: B, gamma CExprPedraZ.AbDom.top x.
Proof.
  unfold gamma.
  intro x.
  generalize (liftRho x ZNum.z).
  apply CExprPedraZ.AbDom.gamma_top.
Qed.

Lemma join_sound: forall (ab1 ab2: A*query_chan) (chan:query_chan) (x: B),
    γ ab1 x \/ γ ab2 x -> γ chan x ->
    γ (CExprPedraZ.AbDom.join (fst ab1) (fst ab2)) x.
Proof.
  intros ab1 ab2 chan x H _.
  destruct H as [[]|[]];
    apply CExprPedraZ.AbDom.join_sound;
    [left|right];
    assumption.
Qed.

Definition ItvConvSpec (i1: ZItv.t) (i2: zitv+⊤+⊥): Prop
  := forall z: BinInt.Z, ZItv.sat i1 z -> γ i2 z.

Definition itvConv (i1: ZItv.t): {i2: zitv+⊤+⊥ | ItvConvSpec i1 i2}.
  refine (
      match i1
            return {i2: zitv+⊤+⊥ | ItvConvSpec i1 i2}
      with
        | ZItv.Bot => exist _ Bot _
        | ZItv.NotBot low up pfi1 =>
          match low
                  return forall pf: ZItv.BndOk low up,
                           {i2: zitv+⊤+⊥ | ItvConvSpec (ZItv.NotBot low up pf) i2}
          with
            | ZItv.Infty => fun pfl => exist _ (NotBot All) _
            | ZItv.Open b1 =>
              fun pfl =>
                match up
                      return forall pf: ZItv.BndOk (ZItv.Open b1) up,
                               {i2: zitv+⊤+⊥ |
                                ItvConvSpec (ZItv.NotBot (ZItv.Open b1) up pf) i2}
                with
                  | ZItv.Infty => fun pfu => exist _ (NotBot All) _
                  | ZItv.Open b2
                  | ZItv.Closed b2 =>
                    fun pfu => exist _ (AdomLib.NotBot (Just (ZITV b1 b2))) _
                end pfl
            | ZItv.Closed b1 =>
              fun pfl =>
                match up
                      return forall pf: ZItv.BndOk (ZItv.Closed b1) up,
                               {i2: zitv+⊤+⊥ |
                                ItvConvSpec (ZItv.NotBot (ZItv.Closed b1) up pf) i2}
                with
                  | ZItv.Infty => fun pfu => exist _ (NotBot All) _
                  | ZItv.Open b2
                  | ZItv.Closed b2 =>
                    fun pfu => exist _ (NotBot (Just (ZITV b1 b2))) _
                end pfl
          end pfi1
      end);
  unfold ItvConvSpec;
  intros z h;
  simpl;
  match goal with
    | |- γ All z => constructor
    | _ => idtac
  end;
  simpl;
  unfold ZItv.sat, ZItv.satLower, ZItv.satUpper in h;
  match goal with
    | h: False |- False => destruct h
    | _ => idtac
  end; auto.
  - split; apply Zlt_le_weak, h.
  - split;
    [apply Zlt_le_weak|idtac];
    apply h.
  - split;
    [idtac|apply Zlt_le_weak];
    apply h.
Defined.
Definition get_itv: iexpr -> A -> iitv+⊤+⊥
  := fun e ab =>
       match iexpr_ty e with
         | INTz =>
           let e' := iexprTr e in
           match proj1_sig (itvConv (CExprPedraZ.AbDom.get_itv e' ab)) with
             | Bot => Bot
             | NotBot (Just itv) => NotBot (Just (Az itv))
             | NotBot All => NotBot All
           end
         | INTf => NotBot All
       end.

Lemma get_itv_correct: forall (e: iexpr) (rho: B) (ab: A),
                         gamma ab rho ->
                         (eval_iexpr rho e) ⊆ γ (get_itv e ab).
Proof.
  simpl.
  intros e rho ab hab i h.
  unfold get_itv.
  pose proof (iexpr_ty_correct _ _ _ h). destruct H. 2:constructor.
  assert (pfe := IExprTrPreservation ZNum.z e).
  destruct (itvConv (CExprPedraZ.AbDom.get_itv (iexprTr e) ab)) as [x pfx].
  simpl.
  unfold ItvConvSpec in pfx.
    destruct x as [|[]].
    + apply pfx with (z := i).
      apply CExprPedraZ.AbDom.get_itv_correct with (rho := liftRho rho 0).
      assumption.
      apply pfe with (n := INz i).
      assumption.
    + exact I.
    + simpl.
      apply pfx.
      apply CExprPedraZ.AbDom.get_itv_correct with (rho := liftRho rho 0).
      assumption.
      apply pfe with (n := INz i).
      assumption.
Qed.

Definition propagateBot : A -> A+⊥ :=
  fun ab => if CExprPedraZ.AbDom.isBottom ab then Bot else NotBot ab.

Lemma propagateBot_correct : forall (ab : A) (m : B),
                               m ∈ γ ab <-> m ∈ γ (propagateBot ab).
Proof.
  intros ab m. simpl.
  split.
  - intro hyp.
    unfold propagateBot.
    assert (pf := CExprPedraZ.AbDom.isBottom_correct ab).
    destruct (CExprPedraZ.AbDom.isBottom ab).
    apply pf with (m := liftRho m ZNum.z).
    reflexivity.
    assumption.
    assumption.
  - assert (pf := CExprPedraZ.AbDom.isBottom_correct ab).
    unfold propagateBot.
    destruct (CExprPedraZ.AbDom.isBottom ab).
    intro contr.
    destruct contr.
    intro h.
    assumption.
Qed.

Definition assume : iexpr -> bool -> A * query_chan -> A+⊥
  := fun e b ab => propagateBot (CExprPedraZ.AbDom.assume (iexprTr e) b (fst ab)).

Lemma assume_correct: forall (c: iexpr) (rho: B) (ab: A * query_chan) (b: bool),
                        rho ∈ γ ab ->
                        eval_iexpr rho c (INz (if b then F1 else F0)) ->
                        rho ∈ γ (assume c b ab).
Proof.
  intros e rho ab b hab hc.
  unfold assume.
  simpl.
  apply propagateBot_correct.
  apply CExprPedraZ.AbDom.assume_correct.
  apply hab.
  destruct b.
  apply IExprTrPreservation with (n := INz 1), hc.
  apply IExprTrPreservation with (n := INz 0), hc.
Qed.

Definition assign: var -> iexpr -> A * query_chan -> query_chan -> A+⊥
  := fun x e ab _ => propagateBot (CExprPedraZ.AbDom.assign (v2p x) (iexprTr e) (fst ab)).

Lemma assign_correct: forall (x: var) (e: iexpr) (ρ: var -> ideal_num)
                             (n: ideal_num) (ab: A*query_chan) (c:query_chan),
                        γ ab ρ -> γ c (upd ρ x n) -> eval_iexpr ρ e n ->
                        γ (assign x e ab c) (upd ρ x n).
Proof.
  simpl. unfold PolGammaOp.
  intros x e rho n ab c [h1 _] _ h2.
  unfold assign.
  assert (pf := CExprPedraZ.AbDom.assign_correct).
  specialize (pf (v2p x) (iexprTr e) (liftRho rho 0) (liftN 0 n) (fst ab) h1
                 (IExprTrPreservation _ _ _ _ h2)).
  apply propagateBot_correct. simpl.

  assert (pfm : forall x0, Mem.assign (v2p x) (liftN 0 n) (liftRho rho 0) x0 =
                          liftRho (upd rho x n) ZNum.z x0).
  intro x0.
  unfold Mem.assign, upd, liftRho, liftN.
  destruct (eq_dec (p2v x0) x) as [eqx | eqx].
    subst. rewrite BIJ.(@backward _ _ _ _).
    destruct (PVar.eq_dec x0 x0) as [eq0 | eq0]. reflexivity. congruence.
    destruct (PVar.eq_dec (v2p x) x0).
    subst x0. rewrite BIJ.(@forward _ _ _ _) in eqx. congruence.
    reflexivity.

  revert pf.
  generalize (CExprPedraZ.AbDom.assign (v2p x) (iexprTr e) (fst ab)).
  intros ab' pfab'.
  eapply CExprPedraZ.AbDom.gamma_ext.
  reflexivity.
  symmetry. auto.
  assumption.
Qed.

Definition forget: var -> A * query_chan -> query_chan -> A+⊥
  := fun x ab _ =>
       propagateBot (CExprPedraZ.AbDom.project (fst ab) (v2p x)).

Lemma forget_correct: forall (x: var) (ρ: var -> ideal_num)
                             (n: ideal_num) (ab: A * query_chan) (c:query_chan),
                        γ ab ρ -> γ c (upd ρ x n) ->
                        γ (forget x ab c) (upd ρ x n).
Proof.
  intros x rho n ab c [h1 _] _.
  unfold forget.
  simpl.
  assert (pf := CExprPedraZ.AbDom.project_correct).
  specialize (pf (fst ab) (v2p x) (liftRho rho 0) (liftN 0 n)).
  apply propagateBot_correct.
  simpl. unfold PolGammaOp.

  assert (pfm : forall x0, Mem.assign (v2p x) (liftN 0 n) (liftRho rho 0) x0 =
                          liftRho (upd rho x n) ZNum.z x0).
  intro x0.
  unfold Mem.assign, upd, liftRho, liftN.
  destruct (eq_dec (p2v x0) x) as [eqx | eqx].
    subst. rewrite BIJ.(@backward _ _ _ _).
    destruct (PVar.eq_dec x0 x0) as [eq0 | eq0]. reflexivity. congruence.
    destruct (PVar.eq_dec (v2p x) x0). subst.
    rewrite BIJ.(@forward _ _ _ _) in eqx. congruence. reflexivity.

  eapply CExprPedraZ.AbDom.gamma_ext.
  reflexivity.
  symmetry. auto.
  apply pf.
  assumption.
Qed.

Global Instance to_string: ToString A
  := fun p => CExprPedraZ.AbDom.pr p.

Definition enrich_qchan (ab:A) (c:query_chan) : query_chan :=
  {| get_var_ty := c.(get_var_ty);
     AbIdealEnv.get_itv expr :=
       match c.(AbIdealEnv.get_itv) expr, get_itv expr ab with
         | NotBot (Just (Az i1)), NotBot (Just (Az i2)) =>
           fmap (@Just _ ∘ Az) (i1 ⊓ i2)
         | NotBot (Just (Af i1)), NotBot (Just (Af i2)) =>
           fmap (@Just _ ∘ Af) (i1 ⊓ i2)
         | NotBot All, NotBot ab | NotBot ab, NotBot All => NotBot ab
         | _, _ => Bot
       end;
     get_congr := c.(get_congr);
     get_eq_expr := c.(get_eq_expr);
     linearize_expr := c.(linearize_expr) |}.

Lemma enrich_qchan_correct :
  forall chan ab ρ,
    ρ ∈ γ chan -> ρ ∈ γ ab -> ρ ∈ γ (enrich_qchan ab chan).
Proof.
  intros chan ab ρ H H0. constructor.
  - intros. apply H.
  - intros. simpl.
    destruct H. specialize (get_itv_correct0 _ _ H1). destruct AbIdealEnv.get_itv. contradiction.
    pose proof (get_itv_correct _ _ _ H0 _ H1).
    destruct x as [|[]], (get_itv e ab) as [|[|[]]], a; auto; try contradiction.
    eapply botbind_spec; eauto. intros. apply H2. apply meet_correct; eauto.
    apply botbind_spec with f1; eauto. apply meet_correct; eauto.
  - intros. apply H. auto.
  - intros. apply H. auto.
  - intros. eapply H; eauto.
Qed.

Global Instance PolAbIdealEnv: ab_ideal_env A (A+⊥) :=
  { id_gamma := PolGammaOp;
    id_top c := NotBot (CExprPedraZ.AbDom.top, nil);
    id_join x y c := NotBot (CExprPedraZ.AbDom.join (fst x) (fst y), nil);
    id_init_iter := id;
    id_widen x y c :=
      let w :=
          match x with
          | Bot => fmap fst y
          | NotBot x =>
            match y with
            | Bot => NotBot x
            | NotBot y =>
              NotBot (CExprPedraZ.AbDom.join x
                       (CExprPedraZ.AbDom.widen x
                         (CExprPedraZ.AbDom.join x (fst y))))
            end
          end
      in
      (w, do w <- w; ret (w, nil));
    assign x e ab c := fmap (fun ab => (ab, nil)) (assign x e ab c);
    forget x ab c := fmap (fun ab => (ab, nil)) (forget x ab c);
    process_msg m ab :=
      match m with
        | Fact_msg e b =>
          do res <- assume_unfold
                      (J:=fun x y => NotBot (CExprPedraZ.AbDom.join x y))
                      assume e b ab;
          ret (res, (m::nil)%list)
        | Known_value_msg x (INz v) =>
          do res <-
             propagateBot (TrustedPedraZ.FullDom.assume
                             (ASCond.ZCond .Atom NumC.Eq (ASTerm.ZTerm.Var (v2p x))
                                                 (ASTerm.ZTerm.Cte v))
                             (fst ab));
          ret (res, (m::nil)%list)
        | _ => ret (fst ab, (m::nil)%list)
      end;
    enrich_query_chan ab c := enrich_qchan ab c }.
Proof.
- intros. split. apply CExprPedraZ.AbDom.gamma_top. constructor.
- intros. eapply gamma_monotone. 2:eauto. apply H.
- intros. split. eapply join_sound; eauto. constructor.
- auto.
- intros. destruct ab1. contradiction. destruct ab2.
  + split. auto. split. auto. constructor.
  + split. eapply CExprPedraZ.AbDom.join_sound. auto.
    split. eapply CExprPedraZ.AbDom.join_sound. auto.
    constructor.
- intros. eapply botbind_spec, assign_correct; eauto. intros. split. eauto. constructor.
- intros. eapply botbind_spec, forget_correct; eauto. intros. split. eauto. constructor.
- intros. destruct m; try (split; [apply H|constructor; [auto|constructor]]).
  + eapply botbind_spec. intros. split. eauto. constructor. auto. constructor.
    apply assume_unfold_correct; eauto.
    intros. eapply CExprPedraZ.AbDom.join_sound. auto.
    intros. eapply assume_correct; auto.
  + destruct i; try (split; [apply H|constructor; [auto|constructor]]).
    eapply botbind_spec. intros. split. eauto. constructor. auto. constructor.
    apply propagateBot_correct, TrustedPedraZ.FullDom.assume_correct, H.
    simpl. unfold liftRho, liftN. rewrite BIJ.(@forward _ _ _ _), H0. auto.
- intros. apply enrich_qchan_correct; auto.
Defined.
Generated by coq2html