Module AbVarExpEq

Require Import ToString Coqlib Utf8 Maps ShareTree Sets Util.
Require Import AdomLib.
Require Import IdealExpr AbIdealEnv.
Require Import Integers ZIntervals.
Require Import Hash FastArith.
Require Import FactMsgHelpers.

Module MVar := T.

Module SVar <: SET with Definition elt := var := Tree2Set(MVar).
Module SVarO := SetOp(SVar).

Module HExp_Cells <: Hashable.
  Definition t := iexpr.
  Definition eq : Util.EqDec t := _.
  Definition hash : hashable t := _.
  Definition bits := F8.
End HExp_Cells.
Module MExp := Hashtable HExp_Cells.

Module SExp <: SET with Definition elt := iexpr := Tree2Set(MExp).
Module SExpO := SetOp(SExp).

Module MExp_Properties := Tree_Properties(MExp).

Fixpoint iexpr_free_vars_acc (e:iexpr) (acc:SVar.t) : SVar.t :=
  match e with
  | IEvar _ x => SVar.add x acc
  | IEconst _ | IEZitv _ => acc
  | IEunop _ e => iexpr_free_vars_acc e acc
  | IEbinop _ e1 e2 => iexpr_free_vars_acc e1 (iexpr_free_vars_acc e2 acc)
  end.

Lemma iexpr_free_vars_acc_iff:
  ∀ e acc x,
    SVar.mem x (iexpr_free_vars_acc e acc) <->
    SVar.mem x acc \/ SVar.mem x (iexpr_free_vars_acc e SVar.empty).

Lemma eval_iexpr_upd_free_acc:
  ∀ x ρ n v e,
    eval_iexpr ρ e v ->
  ∀ acc,
    ~SVar.mem x (iexpr_free_vars_acc e acc) ->
    eval_iexpr (upd ρ x n) e v.

Definition iexpr_free_vars (e:iexpr) : SVar.t :=
  iexpr_free_vars_acc e SVar.empty.

Lemma eval_iexpr_upd_free:
  ∀ x ρ n v e,
    ~SVar.mem x (iexpr_free_vars e) ->
    eval_iexpr ρ e v ->
    eval_iexpr (upd ρ x n) e v.

Fixpoint iexpr_is_free (e:iexpr) (y:var) : bool :=
  match e with
  | IEvar _ x => if eq_dec y x then true else false
  | IEconst _ | IEZitv _ => false
  | IEunop _ e => iexpr_is_free e y
  | IEbinop _ e1 e2 =>
    iexpr_is_free e1 y || iexpr_is_free e2 y
  end.

Lemma iexpr_is_free_iexpr_free_vars:
  ∀ e y,
    SVar.mem y (iexpr_free_vars e) ->
    iexpr_is_free e y.

Fixpoint ite_iexpr_free_vars_acc (e:ite_iexpr) (acc:SVar.t) : SVar.t :=
  match e with
  | Leaf e => iexpr_free_vars_acc e acc
  | Ite c et ef =>
    iexpr_free_vars_acc c
      (ite_iexpr_free_vars_acc et
         (ite_iexpr_free_vars_acc ef acc))
  end.

Lemma ite_iexpr_free_vars_acc_iff:
  ∀ e acc x,
    SVar.mem x (ite_iexpr_free_vars_acc e acc) <->
    SVar.mem x acc \/ SVar.mem x (ite_iexpr_free_vars_acc e SVar.empty).

Lemma eval_ite_iexpr_upd_free_acc:
  ∀ x ρ n v e,
    eval_ite_iexpr ρ e v ->
  ∀ acc,
    ~SVar.mem x (ite_iexpr_free_vars_acc e acc) ->
    eval_ite_iexpr (upd ρ x n) e v.

Definition ite_iexpr_free_vars (e:ite_iexpr) : SVar.t :=
  ite_iexpr_free_vars_acc e SVar.empty.

Lemma eval_ite_iexpr_upd_free:
  ∀ x ρ n v e,
    ~SVar.mem x (ite_iexpr_free_vars e) ->
    eval_ite_iexpr ρ e v ->
    eval_ite_iexpr (upd ρ x n) e v.

Definition max_eq_sz : Z := 30.
Definition max_fact_sz : Z := 10.
Opaque max_eq_sz.
Opaque max_fact_sz.

Fixpoint iexpr_subst (e:iexpr) (x:var) (e':iexpr) : iexpr.
refine (match e as ee return ee = e -> _ with
    | IEvar _ x' => fun _ => if eq_dec x x' then e' else e
    | IEconst _ | IEZitv _ => fun _ => e
    | IEunop op e1 => fun _ =>
      let e1' := iexpr_subst e1 x e' in
      ifeq e1' == e1 then e else IEunop op e1'
    | IEbinop op e1 e2 => fun _ =>
      let e1' := iexpr_subst e1 x e' in
      let e2' := iexpr_subst e2 x e' in
      ifeq e1' == e1 then
        ifeq e2' == e2 then e else IEbinop op e1' e2'
      else IEbinop op e1' e2'
  end eq_refl).

Lemma iexpr_subst_eval:
  ∀ ρ v e, eval_iexpr ρ e v ->
  ∀ x e', eval_iexpr ρ e' (ρ x) ->
          eval_iexpr ρ (iexpr_subst e x e') v.

Lemma iexpr_subst_free:
  ∀ e x e', ~SVar.mem x (iexpr_free_vars e') ->
  ∀ y, SVar.mem y (iexpr_free_vars (iexpr_subst e x e')) ->
       x ≠ y /\
       (SVar.mem y (iexpr_free_vars e) \/
        SVar.mem y (iexpr_free_vars e')).

Fixpoint ite_iexpr_subst (e:ite_iexpr) (x:var) (e':iexpr) : ite_iexpr.
refine (match e as ee return ee = e -> _ with
    | Leaf e1 => fun _ =>
      let e1' := iexpr_subst e1 x e' in
      ifeq e1' == e1 then e else Leaf e1'
    | Ite c e1 e2 => fun _ =>
      let c' := iexpr_subst c x e' in
      let e1' := ite_iexpr_subst e1 x e' in
      let e2' := ite_iexpr_subst e2 x e' in
      ifeq c' == c then
        ifeq e1' == e1 then
          ifeq e2' == e2 then e else Ite c' e1' e2'
        else Ite c' e1' e2'
      else Ite c' e1' e2'
  end eq_refl).

Lemma ite_iexpr_subst_eval:
  ∀ ρ v e, eval_ite_iexpr ρ e v ->
  ∀ x e', eval_iexpr ρ e' (ρ x) ->
          eval_ite_iexpr ρ (ite_iexpr_subst e x e') v.

Lemma ite_iexpr_subst_free:
  ∀ e x e', ~SVar.mem x (iexpr_free_vars e') ->
  ∀ y, SVar.mem y (ite_iexpr_free_vars (ite_iexpr_subst e x e')) ->
       x ≠ y /\
       (SVar.mem y (ite_iexpr_free_vars e) \/
        SVar.mem y (iexpr_free_vars e')).

Record t0 :=
  { eqs : MVar.t ite_iexpr;
    eqs_free : MVar.t SVar.t;
    facts : MExp.t bool;
    facts_free : MVar.t SExp.t
  }.
Record t0_inv (ab:t0) : Prop :=
  { eqs_free_correct :
      ∀ x e, MVar.get x ab.(eqs) = Some e ->
      ∀ y, SVar.mem y (ite_iexpr_free_vars e) ->
      ∃ s, MVar.get y ab.(eqs_free) = Some s /\ SVar.mem x s;
    facts_free_correct :
      ∀ e b, MExp.get e ab.(facts) = Some b ->
      ∀ y, SVar.mem y (iexpr_free_vars e) ->
      ∃ s, MVar.get y ab.(facts_free) = Some s /\ SExp.mem e s }.

Definition t := {ab: t0 | t0_inv ab}.

Record gamm0 (ab:t0) (ρ:var -> ideal_num) : Prop :=
  { eqs_gamm :
      ∀ x e, MVar.get x ab.(eqs) = Some e -> eval_ite_iexpr ρ e (ρ x);
    facts_gamm :
      ∀ e b, MExp.get e ab.(facts) = Some b ->
             eval_iexpr ρ e (INz (if b then F1 else F0)) }.
Instance gamm0' : gamma_op t0 (var -> ideal_num) := gamm0.

Instance gamm : gamma_op t (var -> ideal_num) :=
  fun ab => gamm0 (proj1_sig ab).

Definition enrich_qchan (ab:t) (c:query_chan) : query_chan :=
  {| get_var_ty := c.(get_var_ty);
     get_itv := c.(get_itv);
     get_congr := c.(get_congr);
     get_eq_expr x := MVar.get x (proj1_sig ab).(eqs);
     linearize_expr := c.(linearize_expr) |}.

Lemma enrich_qchan_correct:
  ∀ ρ ab c, ρ ∈ γ ab -> ρ ∈ γ c -> ρ ∈ γ (enrich_qchan ab c).

Definition remove_eq (x:var) (e:ite_iexpr) (ab:t0) : t0 :=
  {| eqs := MVar.remove x ab.(eqs);
     eqs_free :=
       SVar.fold (fun x' free =>
                    match MVar.get_set x' free with
                      | (None, _) => free
                      | (Some s, setter) => setter (SVar.rem x s)
                    end)
                 (ite_iexpr_free_vars e) ab.(eqs_free);
     facts := ab.(facts); facts_free := ab.(facts_free)
  |}.

Lemma remove_eq_inv:
  ∀ x e ab,
    t0_inv ab ->
    MVar.get x ab.(eqs) = Some e ->
    t0_inv (remove_eq x e ab).

Lemma remove_eq_get:
  ∀ x e ab y, MVar.get y (remove_eq x e ab).(eqs) =
     if eq_dec y x then None else MVar.get y ab.(eqs).

Lemma remove_eq_gamm0:
  ∀ x e ab ρ, ρ ∈ γ ab -> ρ ∈ γ (remove_eq x e ab).

Definition unfree_eq (x:var) (ab:t0) (x':var) (e':iexpr) : t0 :=
  match MVar.get_set x ab.(eqs) with
  | (Some e, setter) =>
    let newe := ite_iexpr_subst e x' e' in
    if Z.leb (ite_iexpr_sz newe) max_eq_sz then
      let free :=
          match MVar.get_set x' ab.(eqs_free) with
          | (None, _) => ab.(eqs_free)
          | (Some s, setter) => setter (SVar.rem x s)
          end
      in
      let free :=
          SVar.fold
            (fun y free =>
               let '(o, setter) := MVar.get_set y free in
               setter
                 (SVar.add x match o with None => SVar.empty | Some s => s end))
            (iexpr_free_vars e') free
      in
      {| eqs := setter newe; eqs_free := free;
         facts := ab.(facts); facts_free := ab.(facts_free)
      |}
    else remove_eq x e ab
  | (None, _) => ab
  end.

Lemma unfree_eq_inv:
  ∀ ab x x' e',
    ~SVar.mem x' (iexpr_free_vars e') ->
    t0_inv ab ->
    t0_inv (unfree_eq x ab x' e').

Lemma unfree_eq_gamm0:
  ∀ x ab x' e' ρ,
    ρ ∈ γ ab ->
    eval_iexpr ρ e' (ρ x') ->
    ρ ∈ γ (unfree_eq x ab x' e').

Lemma unfree_eq_get:
  ∀ ab x x' e' y,
    match MVar.get y (unfree_eq x ab x' e').(eqs) with
    | None => MVar.get y ab.(eqs) = None \/ x = y
    | Some e =>
      if eq_dec x y then
        ∃ ee, MVar.get x ab.(eqs) = Some ee /\
              e = ite_iexpr_subst ee x' e'
      else MVar.get y ab.(eqs) = Some e
    end.

Definition forget0_eqs (x:var) (e:option iexpr) (ab:t0) : t0 :=
  match MVar.get x ab.(eqs_free) with
  | None => ab
  | Some s =>
    let ab := SVar.fold
       (fun x' ab =>
          match e with
          | Some e => unfree_eq x' ab x e
          | _ =>
            match MVar.get x' ab.(eqs) with
            | Some e' => remove_eq x' e' ab
            | None => ab
            end
          end) s ab
    in
    {| eqs := ab.(eqs); eqs_free := MVar.remove x ab.(eqs_free);
       facts := ab.(facts); facts_free := ab.(facts_free) |}
  end.

Lemma forget0_eqs_inv:
  ∀ ab x e,
    t0_inv ab ->
    match e with
    | Some e => ~SVar.mem x (iexpr_free_vars e)
    | _ => True
    end ->
    t0_inv (forget0_eqs x e ab).

Lemma forget0_eqs_gamm0:
  ∀ x e ab ρ,
    ρ ∈ γ ab ->
    match e with
    | Some e => eval_iexpr ρ e (ρ x)
    | None => True
    end ->
    ρ ∈ γ (forget0_eqs x e ab).

Definition remove_fact (e:iexpr) (ab:t0) : t0 :=
  {| facts := MExp.remove e ab.(facts);
     facts_free :=
       SVar.fold (fun x' free =>
                    match MVar.get_set x' free with
                    | (None, _) => free
                    | (Some s, setter) => setter (MExp.remove e s)
                    end)
              (iexpr_free_vars e) ab.(facts_free);
         eqs := ab.(eqs); eqs_free := ab.(eqs_free)
  |}.

Lemma remove_fact_inv:
  ∀ ab p, t0_inv ab -> t0_inv (remove_fact p ab).

Lemma remove_fact_gamm0:
  ∀ ab ρ e, ρ ∈ γ ab -> ρ ∈ γ (remove_fact e ab).

Lemma remove_fact_get:
  ∀ e ab ee, MExp.get ee (remove_fact e ab).(facts) =
     if eq_dec ee e then None else MExp.get ee ab.(facts).

Definition try_add_fact_aux (e:iexpr) (b:bool) (ab:t0) : t0+⊥ :=
  if iexpr_det e && Z.leb (iexpr_sz e) max_fact_sz then
    match MExp.get_set e ab.(facts) with
      | (None, setter) =>
        NotBot
          {| eqs := ab.(eqs); eqs_free := ab.(eqs_free);
             facts := setter b;
             facts_free :=
               SVar.fold
                 (fun x' free =>
                    let '(o, setter) := MVar.get_set x' free in
                    setter
                      (SExp.add e
                        (match o with
                         | None => SExp.empty
                         | Some s => s
                         end)))
                 (iexpr_free_vars e) ab.(facts_free)
          |}
      | (Some b', _) =>
        if Bool.eqb b b' then NotBot ab else Bot
    end
  else NotBot ab.

Lemma try_add_fact_aux_inv:
  ∀ e f ab ab',
    t0_inv ab ->
    try_add_fact_aux e f ab = NotBot ab' ->
    t0_inv ab'.

Lemma try_add_fact_aux_gamm0:
  ∀ e (b:bool) ρ ab,
    ρ ∈ γ ab ->
    eval_iexpr ρ e (INz (if b then F1 else F0)) ->
    ρ ∈ γ (try_add_fact_aux e b ab).

Definition unfree_fact (e:iexpr) (ab:t0) (x':var) (e':iexpr) : t0+⊥ :=
  match MExp.get e ab.(facts) with
  | Some b =>
    let newe := iexpr_subst e x' e' in
    try_add_fact_aux newe b (remove_fact e ab)
  | None => NotBot (remove_fact e ab)
  end.

Lemma unfree_fact_inv:
  ∀ ab e x' e' ab',
    t0_inv ab ->
    unfree_fact e ab x' e' = NotBot ab' ->
    t0_inv ab'.

Lemma unfree_fact_gamm0:
  ∀ e ab x' e' ρ,
    ρ ∈ γ ab ->
    eval_iexpr ρ e' (ρ x') ->
    ρ ∈ γ (unfree_fact e ab x' e').

Lemma unfree_fact_get:
  ∀ ab e x' e' ab' ee,
    unfree_fact e ab x' e' = NotBot ab' ->
    match MExp.get ee ab'.(facts) with
    | None => MExp.get ee ab.(facts) = None \/ e = ee
    | Some b =>
      ee = iexpr_subst e x' e' /\ MExp.get e ab.(facts) = Some b \/
      MExp.get ee ab.(facts) = Some b /\ (ee ≠ e \/ ~SVar.mem x' (iexpr_free_vars e))
    end.

Definition forget0_facts (x:var) (e:option iexpr) (ab:t0) : t0+⊥ :=
  match MVar.get x ab.(facts_free) with
  | None => NotBot ab
  | Some s =>
    do ab <-
      SExp.fold (fun f ab =>
                   do ab <- ab;
                   match e with
                   | Some e => unfree_fact f ab x e
                   | None => ret (remove_fact f ab)
                   end)
        s (NotBot ab);
    ret {| eqs := ab.(eqs); eqs_free := ab.(eqs_free);
           facts := ab.(facts); facts_free := MVar.remove x ab.(facts_free) |}
  end.

Lemma forget0_facts_inv:
  ∀ ab x e ab',
    t0_inv ab ->
    match e with
    | Some e => ~SVar.mem x (iexpr_free_vars e)
    | _ => True
    end ->
    forget0_facts x e ab = NotBot ab' ->
    t0_inv ab'.

Lemma forget0_facts_gamm0:
  ∀ x e ab ρ,
    ρ ∈ γ ab ->
    match e with
    | Some e => eval_iexpr ρ e (ρ x)
    | None => True
    end ->
    ρ ∈ γ (forget0_facts x e ab).

Definition forget0 (x:var) (ab:t0) : t0+⊥ :=
  let e := MVar.get x ab.(eqs) in
  let e' :=
    match e with
    | Some (Leaf e) => if iexpr_is_free e x then None else Some e
    | _ => None
    end
  in
  let ab := match e with None => ab | Some e => remove_eq x e ab end in
  forget0_facts x e' (forget0_eqs x e' ab).

Lemma forget0_inv:
  ∀ ab x ab', t0_inv ab ->
              forget0 x ab = NotBot ab' ->
              t0_inv ab'.

Lemma forget0_gamm0:
  ∀ x ab ρ,
    ρ ∈ γ ab ->
    ρ ∈ γ (forget0 x ab).

Lemma eqs_free_forget0_facts:
  ∀ x e ab ab',
    forget0_facts x e ab = NotBot ab' ->
    ab'.(eqs_free) = ab.(eqs_free).

Lemma eqs_forget0_facts:
  ∀ x e ab ab',
    forget0_facts x e ab = NotBot ab' ->
    ab'.(eqs) = ab.(eqs).

Lemma eqs_forget0_eqs:
  ∀ x e ab x' e',
    MVar.get x' (forget0_eqs x e ab).(eqs) = Some e' ->
    ∃ e', MVar.get x' ab.(eqs) = Some e'.

Lemma forget0_gamm0_upd:
  ∀ x ρ n ab,
    t0_inv ab ->
    ρ ∈ γ ab ->
    (upd ρ x n) ∈ γ (forget0 x ab).

Definition forget (x:var) (ab:t * query_chan) (chan:query_chan): (t * messages_chan)+⊥.
refine
  (match forget0 x (proj1_sig (fst ab)) as ab return _ = ab -> _ with
   | NotBot ab => fun EQ => NotBot (exist _ ab _, nil)
   | Bot => fun _ => Bot
   end eq_refl).

Lemma forget_correct :
  ∀ x ρ n ab chan, ρ ∈ γ ab -> (upd ρ x n) ∈ γ chan ->
                   (upd ρ x n) ∈ γ (forget x ab chan).

Definition try_add_eq (x:var) (e:iexpr) (ab:t0) : t0 :=
  if Z.leb (iexpr_sz e) max_eq_sz then
    match MVar.get_set x ab.(eqs) with
    | (None, setter) =>
      {| eqs := setter (Leaf e);
         eqs_free :=
           SVar.fold
             (fun x' free =>
                let '(o, setter') := MVar.get_set x' free in
                setter' (SVar.add x (match o with
                                     | None => SVar.empty
                                     | Some s => s
                                     end)))
             (iexpr_free_vars e) ab.(eqs_free);
         facts := ab.(facts); facts_free := ab.(facts_free) |}
    | (Some _, _) => ab
    end
  else ab.

Lemma try_add_eq_inv:
  ∀ ab x e, t0_inv ab -> t0_inv (try_add_eq x e ab).

Lemma try_add_eq_gamm0:
  ∀ x e ρ ab,
    ρ ∈ γ ab -> eval_iexpr ρ e (ρ x) -> t0_inv ab ->
    ρ ∈ γ (try_add_eq x e ab).

Opaque try_add_eq.

Definition assign (x:var) (e:iexpr) (ab:t * query_chan) (chan:query_chan):
  (t * messages_chan)+⊥.
refine
  (if
    match e with
    | IEvar _ x' => if eq_dec x x' then true else false
    | _ => false
    end
  then NotBot (fst ab, nil)
  else
    let e :=
      if iexpr_is_free e x then
        match MVar.get x (proj1_sig (fst ab)).(eqs) with
        | Some (Leaf e') =>
          if iexpr_is_free e' x then None else Some (iexpr_subst e x e')
        | _ => None
        end
      else
        Some e
    in
    let e := do e <- e; if iexpr_det e then Some e else None in
    match e with
    | None => forget x ab chan
    | Some e =>
      match forget0 x (proj1_sig (fst ab)) as ab return ab = _ -> (t * messages_chan)+⊥ with
      | Bot => fun _ => Bot
      | NotBot ab => fun EQ =>
        let ab := try_add_eq x e ab in
        NotBot (exist _ ab _, nil)
      end eq_refl
    end).

Lemma assign_correct:
  ∀ x e ρ n ab chan,
    ρ ∈ γ ab -> (upd ρ x n) ∈ γ chan ->
    n ∈ eval_iexpr ρ e ->
    (upd ρ x n) ∈ γ (assign x e ab chan).

Definition try_add_fact (e:iexpr) (b:bool) (ab:t) : t+⊥.
refine
  (let H := _ in
   match e with
   | IEconst _ => NotBot ab
   | _ =>
     match try_add_fact_aux e b (proj1_sig ab) as ab' return _ = ab' -> _ with
     | NotBot ab => fun EQ => NotBot (exist _ ab (H ab EQ))
     | Bot => fun _ => Bot
     end eq_refl
   end).

Lemma try_add_fact_gamm:
  ∀ e (b:bool) ρ ab,
    ρ ∈ γ ab -> eval_iexpr ρ e (INz (if b then F1 else F0)) ->
    ρ ∈ γ (try_add_fact e b ab).

Definition assume0 (e:iexpr) (b:bool) (ab:t0) : t0 :=
  match e with
  | IEbinop (IOcmp Ceq) (IEvar _ x) e'
  | IEbinop (IOcmp Ceq) e' (IEvar _ x) =>
    if b then try_add_eq x e' ab
    else ab
  | IEbinop (IOcmp Cne) (IEvar _ x) e'
  | IEbinop (IOcmp Cne) e' (IEvar _ x) =>
    if b then ab
    else try_add_eq x e' ab
  | _ => ab
  end.

Lemma assume0_inv:
  ∀ e b ab, t0_inv ab -> t0_inv (assume0 e b ab).

Lemma assume0_gamm0:
  ∀ c ρ ab (b:bool) v, t0_inv ab -> ρ ∈ γ ab -> v <> 0 ->
    (INz (if b return Zfast then v else F0)) ∈ eval_iexpr ρ c ->
    ρ ∈ γ (assume0 c b ab).

Definition assume (e:iexpr) (b:bool) (ab:t * query_chan): t+⊥.
refine (
  let '(e, b') := simplify_bool_expr e (snd ab) return t+⊥ in
  do ab <- try_add_fact e (xorb b b') (fst ab);
  NotBot (exist _ (assume0 e (xorb b b') (proj1_sig ab)) _)).

Lemma assume_correct :
  ∀ e ρ ab (b:bool), ρ ∈ γ ab ->
    (INz (if b then F1 else F0)) ∈ eval_iexpr ρ e ->
    ρ ∈ γ (assume e b ab).

Lemma ite_iexpr_eqdec : ∀ (e1 e2:ite_iexpr), {e1 = e2} + {e1 <> e2}.

Definition leb (ab1:t * query_chan) (ab2:t) : bool.
refine (
  let ab1 := proj1_sig (fst ab1) in
  let ab2 := proj1_sig ab2 in
  MVar.shforall2 (fun _ e1' e2' =>
                    match e1', e2' with
                    | _, None => true
                    | None, _ => false
                    | Some e1, Some e2 =>
                      if ite_iexpr_eqdec e1 e2 then true else false
                    end)
              _ ab1.(eqs) ab2.(eqs) &&
  MExp.shforall2 (fun _ f1 f2 =>
                    match f1, f2 with
                    | _, None => true
                    | None, _ => false
                    | Some b1, Some b2 => Bool.eqb b1 b2
                    end)
                       _ ab1.(facts) ab2.(facts)).

Lemma leb_correct:
  ∀ ab1 ab2 ρ, leb ab1 ab2 = true -> ρ ∈ γ ab1 -> ρ ∈ γ ab2.

Definition top (chan:query_chan) : (t * messages_chan)+⊥.
refine (
    NotBot (exist _
                  {| eqs := MVar.empty _; eqs_free := MVar.empty _;
                     facts := MExp.empty _; facts_free := MVar.empty _
                  |} _, nil)).

Lemma top_correct:
  ∀ chan ρ, ρ ∈ γ chan -> ρ ∈ γ (top chan).

Definition join0_cond (widen:bool) (ab1:t0) (ab2:t0) : option (iexpr * bool).
refine (
  if widen then None
  else
    let candidates :=
      MExp.shcombine_diff (fun e ob1 ob2 =>
        match ob1, ob2 with
        | None, _ | _, None => None
        | Some b1, Some b2 =>
          if xorb b1 b2 then ob1 else None
        end)
        _ ab1.(facts) ab2.(facts)
    in
    MExp.fold (fun acc e b =>
      match acc with
      | Some eb => Some eb
      | None => Some (e, b)
      end) candidates None).

Lemma join0_cond_correct :
  ∀ w ab1 ab2 ρ e b,
    join0_cond w ab1 ab2 = Some (e, b) ->
    (ρ ∈ γ ab1 -> eval_iexpr ρ e (INz (if b then F1 else F0))) /\
    (ρ ∈ γ ab2 -> eval_iexpr ρ e (INz (if negb b then F1 else F0))).

Definition join0_eqs (w:bool) (ab1:t0) (ab2:t0) (ab:t0) : t0.
refine(
  match join0_cond w ab1 ab2 with
  | Some (cond, swap) =>
    let diffs :=
      MVar.shcombine_diff (fun _ e1 e2 =>
        match e1, e2 with
        | Some e1, None => Some (e1, false)
        | Some e1, Some e2 =>
          if ite_iexpr_eqdec e1 e2 then None
          else
            if Z.leb (ite_iexpr_sz (Ite cond e1 e2)) max_eq_sz then Some (e2, true)
            else None
        | _, _ => None
        end)
        _ ab1.(eqs) ab2.(eqs)
    in
    let cond_free := iexpr_free_vars cond in
    let free :=
      MVar.fold (fun free x eb =>
        match eb with
        | (e, false) =>
          SVar.fold (fun x' free =>
            match MVar.get_set x' free with
            | (None, _) => free
            | (Some s, setter) => setter (SVar.rem x s)
            end)
            (ite_iexpr_free_vars e) free
        | (e, true) =>
          SVar.fold (fun x' free =>
            let '(o, setter) := MVar.get_set x' free in
            setter
              (SVar.add x
                (match o with
                 | None => SVar.empty
                 | Some s => s
                 end)))
            (ite_iexpr_free_vars_acc e cond_free) free
        end) diffs ab1.(eqs_free)
    in
    {| eqs :=
         MVar.shcombine (fun _ e1 e2 =>
           match e1, e2 with
           | None, _ | _, None => None
           | Some e1, Some e2 =>
             if ite_iexpr_eqdec e1 e2 then Some e1
             else
               let e' :=
                 if swap then Ite cond e1 e2
                 else Ite cond e2 e1
               in
               if Z.leb (ite_iexpr_sz e') max_eq_sz then Some e'
               else None
           end) _ ab1.(eqs) ab2.(eqs);
       eqs_free := free;
       facts := ab.(facts);
       facts_free := ab.(facts_free)
    |}
  | None =>
    let diffs :=
      MVar.shcombine_diff (fun _ e1 e2 =>
        match e1, e2 with
        | Some e1, None => Some e1
        | Some e1, Some e2 =>
          if ite_iexpr_eqdec e1 e2 then None
          else Some e1
        | _, _ => None
        end)
        _ ab1.(eqs) ab2.(eqs)
    in
    let free :=
      MVar.fold (fun free x e1 =>
        SVar.fold (fun x' free =>
          match MVar.get_set x' free with
          | (None, _) => free
          | (Some s, setter) => setter (SVar.rem x s)
          end)
          (ite_iexpr_free_vars e1) free)
        diffs ab1.(eqs_free)
    in
    {| eqs :=
         MVar.shcombine (fun _ e1' e2' =>
           match e1', e2' with
           | None, _ | _, None => None
           | Some e1, Some e2 =>
             if ite_iexpr_eqdec e1 e2 then e1'
             else None
           end) _ ab1.(eqs) ab2.(eqs);
       eqs_free := free;
       facts := ab.(facts);
       facts_free := ab.(facts_free)
    |}
  end);
  abstract (destruct v; auto; destruct ite_iexpr_eqdec; congruence).

Lemma join0_eqs_correct :
  ∀ w ab1 ab2 ab,
    t0_inv ab1 -> t0_inv ab2 -> t0_inv ab ->
    t0_inv (join0_eqs w ab1 ab2 ab) /\
    ∀ ρ, ρ ∈ (γ ab1 ∪ γ ab2) ->
         ρ ∈ γ ab ->
         ρ ∈ γ (join0_eqs w ab1 ab2 ab).

Definition join0_facts (ab1:t0) (ab2:t0) (ab:t0) : t0.
refine (
  let diffs :=
    MExp.shcombine_diff (fun _ ob1 ob2 =>
      match ob1, ob2 with
      | Some _, None => Some tt
      | Some b1, Some b2 => if xorb b1 b2 then Some tt else None
      | _, _ => None
      end)
      _ ab1.(facts) ab2.(facts)
  in
  let free :=
    SExp.fold (fun e free =>
      SVar.fold (fun x' free =>
        match MVar.get_set x' free with
        | (None, _) => free
        | (Some s, setter) => setter (SExp.rem e s)
        end)
        (iexpr_free_vars e) free)
      diffs ab1.(facts_free)
  in
  {| facts :=
       MExp.shcombine (fun _ ob1 ob2 =>
         match ob1, ob2 with
         | None, _ | _, None => None
         | Some b1, Some b2 => if xorb b1 b2 then None else ob1
         end) _ ab1.(facts) ab2.(facts);
     facts_free := free;
     eqs := ab.(eqs);
     eqs_free := ab.(eqs_free)
  |});
  abstract (destruct v as [[]|]; auto; simpl; congruence).

Lemma join0_facts_correct :
  ∀ ab1 ab2 ab,
    t0_inv ab1 -> t0_inv ab2 -> t0_inv ab ->
    t0_inv (join0_facts ab1 ab2 ab) /\
    ∀ ρ, ρ ∈ (γ ab1 ∪ γ ab2) ->
         ρ ∈ γ ab ->
         ρ ∈ γ (join0_facts ab1 ab2 ab).

Definition join0_aux (w:bool) (ab1:t0) (ab2:t0) : t0 :=
  let ab :=
    {| eqs := MVar.empty _; eqs_free := MVar.empty _;
       facts := MExp.empty _; facts_free := MVar.empty _ |}
  in
  let ab := join0_eqs w ab1 ab2 ab in
  let ab := join0_facts ab1 ab2 ab in
  {| eqs := ab.(eqs); eqs_free := ab.(eqs_free);
     facts := ab.(facts); facts_free := ab.(facts_free) |}.

Lemma join0_aux_correct :
  ∀ ab1 ab2 w,
    t0_inv ab1 -> t0_inv ab2 ->
    t0_inv (join0_aux w ab1 ab2) /\
    ∀ ρ, ρ ∈ (γ ab1 ∪ γ ab2) ->
         ρ ∈ γ (join0_aux w ab1 ab2).

Program Instance join0 : join_op t t := join0_aux false.
Program Definition widen0 : t -> t -> t := join0_aux true.

Definition join (ab1:t * query_chan) (ab2:t * query_chan) (chan:query_chan) :
  (t * messages_chan)+⊥ :=
  NotBot ((fst ab1) ⊔ (fst ab2), nil).

Lemma join_correct :
  ∀ ab1 ab2 chan ρ,
    ρ ∈ γ ab1 \/ ρ ∈ γ ab2 -> ρ ∈ γ chan ->
    ρ ∈ γ (join ab1 ab2 chan).

Definition widen (ab1:t+⊥) (ab2:(t * query_chan)+⊥) (chan:query_chan+⊥) :
  t+⊥ * (t * messages_chan)+⊥ :=
  let w :=
      match ab1 with
      | Bot => do (ab2, _) <- ab2; ret ab2
      | NotBot ab1 =>
        match ab2 with
        | Bot => NotBot ab1
        | NotBot (ab2, _) => NotBot (widen0 ab1 ab2)
        end
      end
  in
  (w, do w <- w; ret (w, nil)).

Lemma widen_incr :
  ∀ ab1 ab2 chan ρ,
    ρ ∈ γ ab1 -> ρ ∈ γ chan ->
    ρ ∈ γ (widen ab1 ab2 chan).

Program Instance abVarExpEq_env : ab_ideal_env t (t+⊥) :=
  {| id_leb := leb;
     id_top := top;
     id_join := join;
     id_init_iter := id;
     id_widen := widen;
     assign := assign;
     forget := forget;
     enrich_query_chan := enrich_qchan;
     process_msg m ab :=
       match m return _ with
       | Fact_msg e b =>
         do res <- assume_unfold assume e b ab;
         ret (res, m::nil)
       | _ => ret (fst ab, m::nil)
       end |}.

Instance abVarExpEq_env_tostring
  {_:ToString var} {_:ToString (MVar.t ite_iexpr)} : ToString t :=
  fun x =>
    (MExp.fold (fun acc e b =>
                  acc ++ "[" ++
                  to_string e ++ "↦" ++
                  (if b:bool then "true" else "false") ++ "]")
               (proj1_sig x).(facts)
               "{" ++ "}"
               ++
    to_string (proj1_sig x).(eqs))%string.