Module Octagons

Require Import Utf8.
Require Import Reals.
Require Import IdealExpr.
Require Import AbIdealNonrel.
Require Import ZArith.
Require Import Coqlib.
Require Import Integers.
Require Import AdomLib.
Require Import AbIdealEnv ShareTree Util TreeAl.
Require Import FloatLib.
Require Import LinearQuery AbLinearize.
Require Import ZIntervals FloatIntervals IdealIntervals.
Require Import FactMsgHelpers.
Require Import ToString.

Local Existing Instance fitv_gamma_oR.
Local Existing Instance fitv_gamma_R.

Inductive ovar :=
| ovPlus (v:var)
| ovMinus (v:var).

Instance ovar_tostring {_:ToString var}: ToString ovar :=
  fun x =>
    match x with
    | ovPlus x => ("+"++to_string x)%string
    | ovMinus x => ("-"++to_string x)%string
    end.

Definition oρ (ρ : var -> ideal_num) (x:ovar) : option R :=
  match x with
  | ovPlus x => rρ ρ x
  | ovMinus x => option_map Ropp (rρ ρ x)
  end.

Definition ovar_opp (x:ovar) : ovar :=
  match x with
  | ovPlus v => ovMinus v
  | ovMinus v => ovPlus v
  end.

Lemma ovar_opp_opp:
  ∀ ρ v x, oρ ρ v = Some (-x) <-> oρ ρ (ovar_opp v) = Some x.

Module ovar_EQ <: TYPE_EQ
    with Definition s := ovar
    with Definition t := (var * (unit + unit))%type.

  Definition s := ovar.
  Definition t := (var * (unit + unit))%type.

  Definition t_of_s (x:s) : t :=
    match x with
    | ovPlus x => (x, inl tt)
    | ovMinus x => (x, inr tt)
    end.

  Definition s_of_t (x:t) : s :=
    match x with
    | (x, inl _) => ovPlus x
    | (x, inr _) => ovMinus x
    end.

  Lemma s_of_t_of_s : forall x : s, s_of_t (t_of_s x) = x.

  Lemma t_of_s_of_t: forall x : t, t_of_s (s_of_t x) = x.

  Instance eq : EqDec s.
End ovar_EQ.

Module SUU := SumShareTree(UnitShareTree)(UnitShareTree).
Module PTSUU := ProdShareTree(T)(SUU).
Module To := BijShareTree(ovar_EQ)(PTSUU).
Module Top := ShareTree_Properties(To).
Module Too := ProdShareTree(To)(To).
Module Toop := ShareTree_Properties(Too).

Instance ovar_eq : EqDec ovar := To.elt_eq.

Definition fin_float := {f:float | is_finite f = true}.

Definition proj_fin_float (f:fin_float) : float := proj1_sig f.
Coercion proj_fin_float : fin_float >-> float.
Lemma proj_fin_float_finite :
  ∀ (f:fin_float), is_finite f = true.
Hint Resolve proj_fin_float_finite.

Instance fin_float_eqdec : EqDec fin_float.

Definition fin_float_of_float (f:float) : option fin_float :=
  match is_finite f with
  | true => fun EQ => Some (exist _ f EQ)
  | false => fun _ => None
  end eq_refl.

Lemma fin_float_of_float_correct:
  ∀ f f',
    fin_float_of_float f = Some f' ->
    is_finite f = true /\ f = f'.

Ltac destruct_fin_float_of_float :=
  match goal with
  | |- context [fin_float_of_float ?F] =>
    let H := fresh "FFOF" in
    assert (H:=fin_float_of_float_correct F);
    destruct (fin_float_of_float F);
    [specialize (H _ eq_refl)|clear H]
  end.

Definition t := Too.t fin_float.
Definition iter_t := (t * Too.t unit)+⊥.

Instance t_tostring {_:ToString var}: ToString t :=
  fun x =>
    (Too.fold (fun acc xy (b:fin_float) =>
       let '(x, y) := xy in
       acc ++ "[" ++ to_string x ++ to_string (ovar_opp y) ++ "<=" ++ to_string (b:float)++"]")
       x "{" ++ "}")%string.

Instance octitert_tostring {_:ToString var} : ToString iter_t :=
  to_string ∘ (fmap fst).

Instance ogamma: gamma_op t (var -> ideal_num) :=
  fun ab ρ =>
    ∀ x y b, Too.get (x, y) ab = Some b ->
    ∃ xv yv, oρ ρ x = Some xv /\ oρ ρ y = Some yv /\ (xv-yv <= b).

Instance ogamma_it_0: gamma_op (t * Too.t unit) (var -> ideal_num) :=
  γ ∘ fst.


Definition bound_leb (b1 b2:option fin_float) : bool :=
  match b2, b1 with
  | None, _ => true
  | _, None => false
  | Some (exist b2' _), Some (exist b1' _) =>
    if Fleb b1' b2' then true else false
  end.

Definition bound_min (b1 b2:option fin_float) : option fin_float :=
  if bound_leb b1 b2 then b1 else b2.

Lemma bound_min_either:
  ∀ b1 b2 (P:option fin_float -> Prop),
    (P b1) -> (P b2) -> (P (bound_min b1 b2)).

Lemma reduct_rule_1:
  ∀ x y z (f1 f2:fin_float),
    (x - y <= f1) -> (y - z <= f2) ->
    let b := Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP f1 f2 in
    is_finite b = true ->
    (x - z <= b).

Definition half : float :=
  match Float.exact_inverse (BofZ 53 1024 eq_refl eq_refl 2) as x
        return match x with Some _ => float | None => True end
  with
  | Some x => x
  | None => I
  end.

Lemma half_half: (half:R) = 1/2.

Opaque Bmult.

Lemma reduct_rule_2:
  ∀ x y (f1 f2:fin_float),
    (2 * x <= f1) -> (- 2 * y <= f2) ->
    let b := Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP f1 f2 in
    let b := Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_UP half b in
    is_finite b = true ->
    (x - y <= b).

Definition reduce_diag (x0 x:t) : t+⊥.
refine (
  let handle_bound (f:fin_float) :=
      match Bcompare _ _ f Float.zero with
      | None => None
      | Some Lt => Some false
      | Some Eq => None
      | Some Gt => Some true
      end
  in
  let diffDiag :=
      To.shcombine_diff
        (fun k x0 x =>
           match x0, x with
           | None, None => None
           | Some _, None => None
           | None, Some x =>
             if Top.is_empty x then None
             else
               match To.get k x with
               | None => Some true
               | Some f => handle_bound f
               end
           | Some x0, Some x =>
             if Top.is_empty x then None
             else
               match To.get k x0, To.get k x with
               | None, None => None
               | Some _, None => Some true
               | None, Some f => handle_bound f
               | Some f0, Some f =>
                 if fin_float_eqdec f f0 then None
                 else handle_bound f
               end
           end)
        _ x0 x
  in
  To.fold
    (fun oct k (b:bool) =>
       if b then
         do oct <- oct;
         ret (Too.set (k, k) (exist _ Float.zero eq_refl) oct)
       else Bot)
    diffDiag (NotBot x)).

Lemma reduce_diag_correct:
  ∀ x0 x ρ, ρ ∈ γ x -> ρ ∈ γ (reduce_diag x0 x).


Definition otop (c:query_chan): (t * messages_chan)+⊥ :=
  NotBot (Too.empty _, List.nil).

Lemma otop_correct:
  ∀ c ρ, ρ ∈ γ c -> ρ ∈ γ (otop c).


Definition join0 (x y:t) : t.
refine (Too.shcombine
          (fun vab (xb yb:option fin_float) =>
             let lt (xb':fin_float) xb yb (y:t) :=
               let '(va, vb) := vab in
               let yb' : option fin_float :=
                 do bndA <- Too.get (va, ovar_opp va) y;
                 do bndB <- Too.get (ovar_opp vb, vb) y;
                 let bnd:float := Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP
                                  (bndA:fin_float) (bndB:fin_float) in
                 let bnd:float := Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_UP
                                        half bnd in
                 fin_float_of_float bnd
               in
               if bound_leb yb yb' then yb
               else match yb' with
                    | None => None
                    | Some yb' => if Fleb yb' xb' then xb else Some yb'
                    end
             in
             match xb, yb with
             | None, None => None
             | Some xb', None => lt xb' xb yb y
             | None, Some yb' => lt yb' yb xb x
             | Some xb', Some yb' =>
               match Bcompare _ _ xb' yb' with
               | None => None
               | Some Eq => xb
               | Some Lt => lt xb' xb yb y
               | Some Gt => lt yb' yb xb x
               end
             end)
          _ x y).

Definition join0_correct :
  ∀ x y, (γ x ∪ γ y) ⊆ γ (join0 x y).

Definition get_join_diffs (x y:t) : list (ovar * fin_float * fin_float) *
                                    list (ovar * fin_float * fin_float).
refine(
    let m := To.shcombine_diff (fun v x' y' =>
      do x' <- x'; do x' <- To.get (ovar_opp v) x';
      do y' <- y'; do y' <- To.get (ovar_opp v) y';
      match Bcompare _ _ (x':fin_float) (y':fin_float) with
      | Some Lt => ret (true, x', y')
      | Some Gt => ret (false, x', y')
      | _ => None
      end) _ x y
    in
    To.fold (fun l v t =>
       let '(lt, gt) := l in
       let '(cmp, x', y') := t in
       if cmp:bool then ((v, x', y')::lt, gt) else (lt, (v, x', y')::gt))
      m (nil, nil)).

Lemma get_join_diffs_correct:
  ∀ x y llt lgt v bndx bndy,
    get_join_diffs x y = (llt, lgt) ->
    In (v, bndx, bndy) llt \/ In (v, bndx, bndy) lgt ->
  ∀ ρ,
    (ρ ∈ γ x -> ∃ xv, oρ ρ v = Some xv /\ 2*xv <= bndx) /\
    (ρ ∈ γ y -> ∃ xv, oρ ρ v = Some xv /\ 2*xv <= bndy).

Definition finish_join (r:t)
           (l:list (ovar * fin_float * fin_float) * list (ovar * fin_float * fin_float)) : t :=
  let '(llt, lgt) := l in
  List.fold_left (fun (r:t) (x:ovar * fin_float * fin_float) =>
    let '(a, bndxa, bndya) := x in
    List.fold_left (fun (r:t) (x:ovar * fin_float * fin_float) =>
      let '(b, bndxb, bndyb) := x in
      let bndx := Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP bndxa bndxb in
      let bndx := Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_UP half bndx in
      let bndx := fin_float_of_float bndx in
      let bndy := Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP bndya bndyb in
      let bndy := Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_UP half bndy in
      let bndy := fin_float_of_float bndy in
      let bnd := if bound_leb bndx bndy then bndy else bndx in
      let '(bnd0, setter) := Too.get_set (a, ovar_opp b) r in
      if bound_leb bnd0 bnd then r
      else match bnd with
           | None => r
           | Some bnd =>
             let r := setter bnd in
             Too.set (b, ovar_opp a) bnd r
           end)
     llt r)
    lgt r.

Lemma finish_join_correct:
  ∀ lgt llt r ρ,
  ((∀ v (bndx bndy:fin_float), In (v, bndx, bndy) llt \/ In (v, bndx, bndy) lgt ->
      ∃ xv, oρ ρ v = Some xv /\ 2*xv <= bndx) \/
   (∀ v (bndx bndy:fin_float), In (v, bndx, bndy) llt \/ In (v, bndx, bndy) lgt ->
      ∃ xv, oρ ρ v = Some xv /\ 2*xv <= bndy)) ->
  ρ ∈ γ r ->
  ρ ∈ γ (finish_join r (llt, lgt)).

Definition ojoin (x:t * query_chan) (y:t * query_chan) (c:query_chan) :
  (t * messages_chan)+⊥ :=
  let r := join0 (fst x) (fst y) in
  let l := get_join_diffs (fst x) (fst y) in
  let r := finish_join r l in
  NotBot (r, List.nil).

Lemma ojoin_correct :
  forall x y c ρ,
    ρ ∈ γ x \/ ρ ∈ γ y -> ρ ∈ γ c ->
    ρ ∈ γ (ojoin x y c).


Definition oinit_iter (m:t+⊥) : iter_t :=
  do m <- m;
  let m :=
    Toop.filter (fun xy (b:fin_float) =>
                   let '(x, y) := xy in
                   if eq_dec x (ovar_opp y) then true
                   else
                     match Too.get (x, ovar_opp x) m, Too.get (ovar_opp y, y) m with
                     | None, _ | _, None => true
                     | Some f1, Some f2 =>
                       let b' := Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP
                                       (f1:fin_float) (f2:fin_float) in
                       let b' := Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_UP half b' in
                       negb (Fleb b' b)
                     end
                ) m
  in
  NotBot (m, Too.empty _).

Lemma oinit_iter_sound:
  ∀ m, γ m ⊆ γ (oinit_iter m).

Definition widen0 (it:t*Too.t unit) (m:t) : t.
refine (Too.shcombine
          (fun vab (itb mb:option fin_float) =>
             let '(va, vb) := vab in
             match itb, mb with
             | None, None => None
             | None, Some mb =>
               match Too.get vab (snd it) with
               | Some _ => None
               | None =>
                 match Too.get (va, ovar_opp va) (fst it), Too.get (ovar_opp vb, vb) (fst it) with
                 | None, _ | _, None => None
                 | Some bndA, Some bndB =>
                   let bnd := Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP bndA bndB in
                   let bnd := Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_UP half bnd in
                   if Fleb mb bnd then
                     if bound_leb (Too.get (va, ovar_opp va) m) (Some bndA) &&
                        bound_leb (Too.get (ovar_opp vb, vb) m) (Some bndB) then
                       None
                     else fin_float_of_float bnd
                   else None
                 end
               end
             | Some _, _ =>
               if bound_leb mb itb then itb
               else
                 do bndA <- Too.get (va, ovar_opp va) m;
                 do bndB <- Too.get (ovar_opp vb, vb) m;
                 let bnd := Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP
                                  (bndA:fin_float) (bndB:fin_float) in
                 let bnd := Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_UP half bnd in
                 let b := fin_float_of_float bnd in
                 if bound_leb b itb then itb else None
             end)
          _ (fst it) m).

Lemma widen0_incr:
  ∀ it m, γ it ⊆ γ (widen0 it m).

Definition record_widen_diffs (it:t*Too.t unit) (itnew:t) : Too.t unit.
refine(let diffs :=
           Too.shcombine_diff
             (fun v old new =>
                match old, new with
                | Some _, None => Some tt
                | _, _ => None
                end)
             _ (fst it) itnew
       in
       Too.fold (fun w v _ => Too.set v tt w) diffs (snd it)).

Definition finish_widen
           (r:t)
           (l:list (ovar * fin_float * fin_float) *
              list (ovar * fin_float * fin_float))
           (w:Too.t unit) : t :=
  let '(llt, lgt) := l in
  List.fold_left (fun (r:t) (x:ovar * fin_float * fin_float) =>
    let '(a, bndita, bndma) := x in
    List.fold_left (fun (r:t) (x:ovar * fin_float * fin_float) =>
      let '(b, bnditb, bndmb) := x in
      match Too.get (a, ovar_opp b) w with
      | Some _ => r
      | None =>
        match Too.get_set (a, ovar_opp b) r with
        | (Some _, _) => r
        | (None, setter) =>
          let bndit := Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP bndita bnditb in
          let bndit := Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_UP half bndit in
          let bndit := fin_float_of_float bndit in
          let bndm := Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP bndma bndmb in
          let bndm := Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_UP half bndm in
          let bndm := fin_float_of_float bndm in
          if bound_leb bndm bndit then
            match bndit with
            | Some bndit =>
              let r := setter bndit in
              Too.set (b, ovar_opp a) bndit r
            | None => r
            end
          else r
        end
      end)
     llt r)
  lgt r.

Lemma finish_widen_correct:
  ∀ lgt llt r w ρ,
  (∀ v (bndx bndy:fin_float), In (v, bndx, bndy) llt \/ In (v, bndx, bndy) lgt ->
   ∃ xv, oρ ρ v = Some xv /\ 2*xv <= bndx) ->
  ρ ∈ γ r ->
  ρ ∈ γ (finish_widen r (llt, lgt) w).

Definition widen_reduce_1 (y0 y:t) : t :=
  (To.fold
     (fun (y:t) c _ =>
        match To.get (ovar_opp c) y, To.get c y with
        | None, _ | _, None => y
        | Some aa, Some bb =>
          Toop.map_changed fin_float_eqdec
             (fun ab yb =>
                let '(a, b) := ab in
                let bound :=
                  do f1 <- To.get (ovar_opp a) aa;
                  do f2 <- To.get b bb;
                  fin_float_of_float (Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP
                                            (f1:fin_float) (f2:fin_float))
                in
                bound_min yb bound)
             y0 y
        end
     ) y y).

Lemma widen_reduce_1_correct:
  ∀ y0 y ρ, ρ ∈ γ y -> ρ ∈ γ (widen_reduce_1 y0 y).

Definition owiden (it:iter_t) (y:(t * query_chan)+⊥) (c:query_chan+⊥) :
  iter_t * ((t * messages_chan) +⊥) :=
  match it, y with
  | Bot, Bot => (oinit_iter Bot, Bot)
  | Bot, NotBot (y, _) => (oinit_iter (NotBot y), NotBot (y, nil))
  | NotBot it, Bot =>
    let w := widen_reduce_1 (Too.empty _) (fst it) in
    (NotBot it, do w <- reduce_diag (Too.empty _) w; ret (w, List.nil))
  | NotBot it, NotBot (y, _) =>
    let r := widen0 it y in
    let w := record_widen_diffs it r in
    let l := get_join_diffs (fst it) y in
    let r := finish_widen r l w in
    (NotBot (r,w),
     let r := widen_reduce_1 y r in
     do r <- reduce_diag y r; ret (r, nil))
  end.

Lemma owiden_incr:
  forall x y c ρ,
    ρ ∈ γ x -> ρ ∈ γ c ->
    ρ ∈ γ (owiden x y c).


Definition oleb (x:t * query_chan) (y:t) : bool.
refine (
  let x := fst x in
  Too.shforall2 (fun k (xff yff:option fin_float) =>
    match yff with
    | None => true
    | Some fy =>
      match xff with
      | None => false
      | Some fx => Fleb fx fy
      end ||
      let x' : option fin_float :=
        let '(A, B) := k in
        do bndA <- Too.get (A, ovar_opp A) x;
        do bndB <- Too.get (ovar_opp B, B) x;
        let b : float := Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP
                               (bndA:fin_float) (bndB:fin_float) in
        let b : float := Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_UP
                               half b in
        fin_float_of_float b
      in
      match x' with
      | None => false
      | Some fx' => Fleb fx' fy
      end
    end)
    _ x y).

Lemma oleb_correct:
  forall x y ρ,
    oleb x y = true ->
    ρ ∈ γ x ->
    ρ ∈ γ y.


Definition oforget0 (x:var) (ab:t) : t :=
  let ab := To.remove (ovPlus x) ab in
  let ab := To.remove (ovMinus x) ab in
  To.map1
    (fun ab =>
       let ab := To.remove (ovPlus x) ab in
       To.remove (ovMinus x) ab)
    ab.

Lemma oforget0_incl:
  ∀ x ab, γ ab ⊆ γ (oforget0 x ab).

Lemma oforget0_forget:
  ∀ x ab ρ n,
    ρ ∈ γ (oforget0 x ab) ->
    ρ+[x => n] ∈ γ (oforget0 x ab).

Definition oforget (x:var) (ab:t * query_chan) (c:query_chan) :
  (t * messages_chan)+⊥ :=
  NotBot (oforget0 x (fst ab), List.nil).

Lemma oforget_correct:
  forall x ρ n ab chan,
    ρ ∈ γ ab -> (ρ+[x => n]) ∈ γ chan ->
    (ρ+[x => n]) ∈ γ (oforget x ab chan).


Definition add_zerocycle (x:ovar) (ab:t) : t :=
  match Too.get_set (x, x) ab with
  | (None, setter) => setter (exist _ Float.zero eq_refl)
  | (Some v, setter) =>
    if Fleb Float.zero v then setter (exist _ Float.zero eq_refl)
    else ab
  end.

Lemma add_zerocycle_correct:
  ∀ x ab ρ xv,
    ρ ∈ γ ab ->
    oρ ρ x = Some xv ->
    ρ ∈ γ (add_zerocycle x ab).

Definition constraint_row := To.t fin_float.

Instance cr_tostring {_:ToString var} : ToString constraint_row :=
  fun x =>
    (To.fold (fun acc y (b:fin_float) =>
       acc ++ "[_" ++ to_string (ovar_opp y) ++ "<=" ++ to_string (b:float) ++"]")
       x "{" ++ "}")%string.

Definition constraints_row_valid (row:constraint_row) (ρ:var -> ideal_num) : ℘ R :=
  fun v =>
  ∀ x b, To.get x row = Some b ->
  ∃ xv, oρ ρ x = Some xv /\ (v-xv <= b).

Definition trim_constraints_row (a:ovar) (row:constraint_row) (ab:t) : constraint_row :=
  let mapa :=
      match To.get a ab with
      | None => To.empty _
      | Some mapa => mapa
      end
  in
  To.combine (fun old new => if bound_leb old new then None else new)
    mapa row.

Lemma trim_constraints_row_correct:
  ∀ a row ab ρ av,
    ρ ∈ γ ab ->
    constraints_row_valid row ρ av ->
    constraints_row_valid (trim_constraints_row a row ab) ρ av.

Definition reduce_constraints_row_step (row:constraint_row) (x:ovar) (ax:fin_float) (ab:t):
  constraint_row :=
  match To.get x ab with
  | None => row
  | Some mapx =>
    To.combine
      (fun (ay xy:option fin_float) =>
         let ay' :=
             match xy with
             | None => None
             | Some xy =>
               fin_float_of_float (
                   Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP ax xy)
             end
         in
         bound_min ay ay')
      row mapx
  end.

Lemma reduce_constraints_row_step_correct:
  ∀ row x (ax:fin_float) ab ρ v,
    ρ ∈ γ ab ->
    (∀ xv, oρ ρ x = Some xv -> (v - xv <= ax)) ->
    constraints_row_valid row ρ v ->
    constraints_row_valid (reduce_constraints_row_step row x ax ab) ρ v.

Definition reduce_constraints_row_final (row:constraint_row) (a:ovar) (ab:t):
  constraint_row:=
  let best_aa' :=
    T.fold (fun bnd z (azaz':option fin_float * option fin_float) =>
              match azaz' with
              | (Some az, Some az') =>
                bound_min bnd (
                  fin_float_of_float (
                      Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP az az'))
              | _ => bnd
              end)
    row (To.get (ovar_opp a) row)
  in
  match best_aa' with
  | None => row
  | Some best_aa' =>
    let row := To.set (ovar_opp a) best_aa' row in
    reduce_constraints_row_step row (ovar_opp a) best_aa' ab
  end.

Lemma reduce_constraints_row_final_correct:
  ∀ row a ab ρ av,
    ρ ∈ γ ab ->
    oρ ρ a = Some av ->
    constraints_row_valid row ρ av ->
    constraints_row_valid (reduce_constraints_row_final row a ab) ρ av.

Definition reduce_constraints_row (row:constraint_row) (a:ovar) (ab:t) : constraint_row :=
  let row :=
    To.fold (fun (acc:constraint_row) (x:ovar) (ax:fin_float) =>
               reduce_constraints_row_step acc x ax ab)
      row row
  in
  reduce_constraints_row_final row a ab.

Lemma reduce_constraints_row_correct:
  ∀ row a ab ρ v,
    ρ ∈ γ ab ->
    oρ ρ a = Some v ->
    constraints_row_valid row ρ v ->
    constraints_row_valid (reduce_constraints_row row a ab) ρ v.

Definition add_constraints_row_noreduce (a:ovar) (row:constraint_row) (ab:t) : t :=
  let ab := add_zerocycle a ab in
  let ab := add_zerocycle (ovar_opp a) ab in
  match To.get (ovar_opp a) ab with
  | None => ab
  | Some map_ya =>
    let ab :=
      To.fold (fun acc yopp (ya:fin_float) =>
        match To.get_set (ovar_opp yopp) acc with
        | (None, _) => acc
        | (Some map_yx, setter_yx) =>
          let '(map_yx, chgt) :=
            To.fold (fun (acc':To.t fin_float * bool) x (ax:fin_float) =>
              let '(map_yx, chgt) := acc' in
              let new :=
                fin_float_of_float (
                  Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP ya ax)
              in
              let (old, setter) := To.get_set x map_yx in
              if bound_leb old new then acc'
              else match new with
                   | None => acc'
                   | Some new => (setter new, true)
                   end) row (map_yx, false)
          in
          if chgt then (setter_yx map_yx) else acc
        end) map_ya ab
    in
    match To.get (ovar_opp a) ab with
    | None => ab
    | Some map_ya =>
      To.fold (fun acc x (ax:fin_float) =>
        match To.get_set (ovar_opp x) acc with
        | (None, _) => acc
        | (Some map_xoppyopp, setter_xoppyopp) =>
          let '(map_xoppyopp, chgt) :=
            To.fold (fun (acc':To.t fin_float * bool) yopp (ya:fin_float) =>
              let '(map_xoppyopp, chgt) := acc' in
              let new :=
                fin_float_of_float (
                  Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP ya ax)
              in
              let (old, setter) := To.get_set yopp map_xoppyopp in
              if bound_leb old new then acc'
              else match new with
                   | None => acc'
                   | Some new => (setter new, true)
                   end) map_ya (map_xoppyopp, false)
          in
          if chgt then (setter_xoppyopp map_xoppyopp) else acc
        end) row ab
    end
  end.

Lemma add_constraints_row_noreduce_correct:
  ∀ a row ab ρ av,
    oρ ρ a = Some av -> ρ ∈ γ ab ->
    constraints_row_valid row ρ av ->
    ρ ∈ γ (add_constraints_row_noreduce a row ab).

Definition add_constraints_row (a:ovar) (row:constraint_row) (ab:t) : t :=
  let row := trim_constraints_row a row ab in
  let row := reduce_constraints_row row a ab in
  let row := trim_constraints_row a row ab in
  add_constraints_row_noreduce a row ab.

Lemma add_constraints_row_correct :
  ∀ a row ab ρ av,
    oρ ρ a = Some av -> ρ ∈ γ ab ->
    constraints_row_valid row ρ av ->
    ρ ∈ γ (add_constraints_row a row ab).

Definition add_constraint_to_row (r:constraint_row) (y:ovar) (b:float) : constraint_row :=
  match fin_float_of_float b with
  | None => r
  | Some b => To.set y b r
  end.

Lemma add_constraint_to_row_correct:
  ∀ row b ρ y yv v,
    oρ ρ y = Some yv ->
    (RF_le (v - yv) b) ->
    constraints_row_valid row ρ v ->
    constraints_row_valid (add_constraint_to_row row y b) ρ v.

Fixpoint constraints_row_of_linear_expr (i:fitv) (terms:list (var * (fitv * fitv))) :
  constraint_row * constraint_row * fitv :=
  match terms with
  | nil => (To.empty _, To.empty _, FITV Float.zero Float.zero)
  | (y, (itvα, itvy)) :: q =>
    let iαy := mult_itv itvα itvy in
    let '(constr_p, constr_m, iq) :=
        constraints_row_of_linear_expr (add_itv iαy i) q
    in
    let i := add_itv iq i in
    let 'FITV xpy_a xpy_b :=
        add_itv (mult_itv (add_itv itvα (FITV one one)) itvy) i in
    let mone := Float.neg one in
    let 'FITV xmy_a xmy_b :=
        add_itv (mult_itv (add_itv itvα (FITV mone mone)) itvy) i in
    let constr_p := add_constraint_to_row constr_p (ovPlus y) xmy_b in
    let constr_m := add_constraint_to_row constr_m (ovMinus y) (Float.neg xmy_a) in
    let constr_p := add_constraint_to_row constr_p (ovMinus y) xpy_b in
    let constr_m := add_constraint_to_row constr_m (ovPlus y) (Float.neg xpy_a) in
    (constr_p, constr_m, add_itv iαy iq)
  end.

Transparent Float.zero Float.neg.

Lemma constraints_row_of_linear_expr_correct:
  ∀ terms x i constr_p constr_m iterms ρ,
    eval_linear_expr ρ (i, terms) x ->
    constraints_row_of_linear_expr i terms = (constr_p, constr_m, iterms) ->
    constraints_row_valid constr_p ρ x /\
    constraints_row_valid constr_m ρ (-x) /\
    eval_linear_expr ρ (FITV Float.zero Float.zero, terms) ⊆ γ iterms.

Definition meet_constraints_row (x y:constraint_row) : constraint_row :=
  To.combine bound_min x y.

Lemma meet_constraints_row_correct:
  ∀ x a b ρ,
    constraints_row_valid a ρ x ->
    constraints_row_valid b ρ x ->
    constraints_row_valid (meet_constraints_row a b) ρ x.

Fixpoint assume_linear_constraint (i:fitv) (terms:list (var * (fitv * fitv))) (ab:t) : t :=
  match terms with
  | nil => ab
  | (x, (itvα, itvx)) :: q =>
    if fitv_is_top i then ab
    else
      let ip := add_itv (mult_itv (add_itv itvα (FITV one one)) itvx) i in
      let '(constr_p0, constr_m0, iq) := constraints_row_of_linear_expr ip q in
      let ipq := add_itv ip iq in
      let 'FITV lx2 ux2 := add_itv ipq ipq in
      let constr_p0 := add_constraint_to_row constr_p0 (ovMinus x) ux2 in
      let constr_m0 := add_constraint_to_row constr_m0 (ovPlus x) (Float.neg lx2) in

      let im := add_itv (mult_itv (add_itv (opp_itv itvα) (FITV one one)) itvx)
                        (opp_itv i)
      in
      let qm := List.map (fun t =>
        let '(k, (itvα, itvk)) := t in (k, (opp_itv itvα, itvk))) q
      in
      let '(constr_p1, constr_m1, iq) := constraints_row_of_linear_expr im qm in
      let imq := add_itv im iq in
      let 'FITV lx2 ux2 := add_itv imq imq in
      let constr_p1 := add_constraint_to_row constr_p1 (ovMinus x) ux2 in
      let constr_m1 := add_constraint_to_row constr_m1 (ovPlus x) (Float.neg lx2) in

      let constr_p := meet_constraints_row constr_p0 constr_p1 in
      let ab := add_constraints_row (ovPlus x) constr_p ab in
      let constr_m := meet_constraints_row constr_m0 constr_m1 in
      let ab := add_constraints_row (ovMinus x) constr_m ab in

      let i := add_itv (mult_itv itvα itvx) i in
      assume_linear_constraint i q ab
  end.

Lemma assume_linear_constraint_correct:
  ∀ terms i ab ρ,
    ρ ∈ γ ab ->
    eval_linear_expr ρ (i, terms) 0 ->
    ρ ∈ γ (assume_linear_constraint i terms ab).

Definition msg_of_bnds
           (a b:option fin_float) (x:var)
           (ty:ideal_num_ty) (itv:iitv+⊤+⊥) : message+⊤+⊥ :=
  let a :=
    match a with
    | None => B754_infinity true
    | Some a => Float.neg (Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_UP half a)
    end
  in
  let b :=
    match b with
    | None => B754_infinity false
    | Some b => Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_UP half b
    end
  in
  do itv' <- fitv_of_iitv itv ⊓ Just (FITV a b);
  let itv' := NotBot (bind itv' (iitv_of_fitv ty)) in
  if itv ⊑ itv' return message+⊤+⊥ then NotBot All
  else match itv' ⊓ itv with
       | NotBot All => NotBot All
       | Bot => Bot
       | NotBot (Just itv') =>
         NotBot (Just (Broadcasted_msg (
           match IdealIntervals.singleton itv' with
           | Some v => Known_value_msg x v
           | None => Itv_msg x itv'
           end)))
       end.

Lemma msg_of_bnds_correct:
  ∀ (a b:option fin_float) x ty itv ρ xv,
    ρ x ∈ γ ty ->
    ρ x ∈ γ itv ->
    rρ ρ x = Some xv ->
    (∀ a', a = Some a' -> -2*xv <= a') ->
    (∀ b', b = Some b' -> 2*xv <= b') ->
    ρ ∈ γ (msg_of_bnds a b x ty itv).

Definition oprocess_msg (m:message) (ab0:t * query_chan) : (t * messages_chan)+⊥.
refine
  (match m with
  | Linear_zero_msg e =>
    let '(ab0, c) := ab0 in
    let ab := assume_linear_constraint (fst e) (T.elements (snd e)) ab0 in
    do ab <- reduce_diag ab0 ab;
    let diff :=
      To.shcombine_diff (fun x mapxy0 mapxy =>
        let a0 := do mapxy0 <- mapxy0; To.get (ovar_opp x) mapxy0 in
        let a := do mapxy <- mapxy; To.get (ovar_opp x) mapxy in
        match a0, a with
        | None, Some _ => a
        | Some a0', Some a' => if Fleb (a0':fin_float) (a':fin_float) then None else a
        | _, _ => None
        end) _
        ab0 ab
    in
    do msgs <-
      T.fold (fun acc x bnds =>
        match bnds with
        | (None, None) => acc
        | (a, b) =>
          match c.(get_var_ty) x with
          | Just ty =>
            let ichan := c.(get_itv) (IEvar ty x) in
            do m <- msg_of_bnds b a x ty ichan;
            match m with
            | All => acc
            | Just m => do acc <- acc; ret (m::acc)
            end
          | All => acc
          end
        end) diff (NotBot nil);
    ret (ab, m::msgs)
  | _ => NotBot (fst ab0, m::nil)
  end).

Lemma oprocess_msg_correct:
  ∀ m ρ ab,
    ρ ∈ γ ab -> ρ ∈ γ m ->
    ρ ∈ γ (oprocess_msg m ab).


Definition reduce_constraints_row_step_self (row:constraint_row) (x:ovar) (ab:t):
  constraint_row :=
  match To.get x row with
  | None => row
  | Some ax => reduce_constraints_row_step row x ax ab
  end.

Lemma reduce_constraints_row_step_self_correct:
  ∀ row x ab ρ v,
    ρ ∈ γ ab ->
    constraints_row_valid row ρ v ->
    constraints_row_valid (reduce_constraints_row_step_self row x ab) ρ v.

Definition oassign (x:var) (e0:iexpr) (ab0:t * query_chan) (c:query_chan) :
  (t * messages_chan)+⊥:=
  let e := (snd ab0).(linearize_expr) e0 in
  let ty := iexpr_ty e0 in
  match e with
  | None => oforget x ab0 c
  | Some e =>
    let ab0 := fst ab0 in
    let ab := oforget0 x ab0 in
    let '(constr_p, constr_m, i) :=
        constraints_row_of_linear_expr (fst e) (T.elements (snd e))
    in
    let i := add_itv (fst e) i in
    let ichan := c.(get_itv) (IEvar (iexpr_ty e0) x) in
    do i <-
      match fitv_of_iitv ichan with
      | All => NotBot i
      | Just i' => i' ⊓ i
      end;
    let 'FITV a b := add_itv i i in

    let constr_p := reduce_constraints_row_step_self constr_p (ovPlus x) ab0 in
    let constr_p := reduce_constraints_row_step_self constr_p (ovMinus x) ab0 in
    let x'mx : option fin_float := To.get (ovPlus x) constr_p in
    let x'px : option fin_float := To.get (ovMinus x) constr_p in
    let b' :=
      do x'mx <- x'mx;
      do x'px <- x'px;
      fin_float_of_float (Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP
                                (x'mx:fin_float) (x'px:fin_float))
    in
    let constr_p := T.remove x constr_p in
    let constr_p :=
      match bound_min (fin_float_of_float b) b' with
      | Some b => To.set (ovMinus x) b constr_p
      | _ => constr_p
      end
    in

    let ab := add_constraints_row (ovPlus x) constr_p ab in

    let constr_m := reduce_constraints_row_step_self constr_m (ovPlus x) ab0 in
    let constr_m := reduce_constraints_row_step_self constr_m (ovMinus x) ab0 in
    let mx'mx : option fin_float := To.get (ovPlus x) constr_m in
    let mx'px : option fin_float := To.get (ovMinus x) constr_m in
    let a' :=
      do mx'mx <- mx'mx;
      do mx'px <- mx'px;
      fin_float_of_float
        (Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP (mx'mx:fin_float) (mx'px:fin_float))
    in
    let constr_m := T.remove x constr_m in
    let constr_m :=
      match bound_min (fin_float_of_float (Float.neg a)) a' with
      | Some a => To.set (ovPlus x) a constr_m
      | _ => constr_m
      end
    in

    let ab := add_constraints_row (ovMinus x) constr_m ab in

    do ab <- reduce_diag ab0 ab;

    let a := Too.get (ovMinus x, ovPlus x) ab in
    let b := Too.get (ovPlus x, ovMinus x) ab in
    do msg <- msg_of_bnds a b x ty ichan;
    let msgs :=
      match msg with
      | All => nil
      | Just m => m::nil
      end
    in
    ret (ab, msgs)
  end.

Lemma oassign_correct:
  forall x e ρ n ab chan,
    ρ ∈ γ ab -> (ρ+[x => n]) ∈ γ chan ->
    n ∈ eval_iexpr ρ e ->
    (ρ+[x => n]) ∈ γ (oassign x e ab chan).

Program Instance oct_idenv : ab_ideal_env t iter_t :=
  {| id_leb := oleb;
     id_top := otop;
     id_join := ojoin;
     id_init_iter := oinit_iter;
     id_widen := owiden;
     assign := oassign;
     forget := oforget;
     enrich_query_chan ab c := c;
     process_msg := oprocess_msg |}.