Require Import
  Utf8 String Coqlib Integers ArithLib AdomLib ToString FastArith.

Require Import
  ZIntervals AbIdealNonrel IdealExpr ZCongruences_defs
  AbIdealEnv IdealBoxDomain Util.

Definition extern_top (ab:zcongr) : zcongr+⊤ :=
  if Nfasteqb ab.(zc_mod) F1 then All else Just ab.

Definition intern_top (ab:zcongr+⊤) : zcongr :=
  match ab with
  | All => top
  | Just ab => ab
  end.

Abstract Operators.

Program Definition zc_const (z: Zfast) : zcongr := ZC z F0 _.
Lemma zc_const_sound:
  ∀ (n:Z), n ∈ γ (zc_const n).

Definition zc_true : zcongr := zc_const F1.
Definition zc_false: zcongr := zc_const F0.
Definition zc_bool (b: bool) : zcongr := if b then zc_true else zc_false.

Lemma zc_bool_sound b : ((if b return Zfast then F1 else F0):Z) ∈ γ(zc_bool b).

Program Definition zc_add (plus: Zfast → Zfast → Zfast) (x y: zcongr) : zcongr :=
  let m := Nfastgcd x.(zc_mod) y.(zc_mod) in
  let r := plus x.(zc_rem) y.(zc_rem) in
  ZC (if Nfasteqb m F0 then r else Zfastmod r m) m _.

Lemma zc_add_sound (plus: Zfast → Zfast → Zfast) (x y: zcongr) (i j: Z) :
  (∀ n u u' v v', u ≡ u' [n] → v ≡ v' [n] → plus u v ≡ plus u' v' [n]) →
  γ x i → γ y j → γ (zc_add plus x y) (plus i j:Z).

Program Definition zc_neg x :=
  ZC (if Nfasteqb x.(zc_mod) F0 then Zfastopp x.(zc_rem)
      else Zfastmod (Zfastopp x.(zc_rem)) x.(zc_mod))
     x.(zc_mod) _.

Lemma zc_neg_sound x (i:Z) :
  γ x i → γ (zc_neg x) (-i).

Program Definition zc_mul (x y: zcongr) : zcongr :=
  let g1 := Nfastgcd (Zfastabs x.(zc_rem)) x.(zc_mod) in
  let g2 := Nfastgcd (Nfastmul g1 y.(zc_mod))
                     (Nfastmul (Zfastabs y.(zc_rem)) x.(zc_mod))
  in
  let r := Zfastmul x.(zc_rem) y.(zc_rem) in
  ZC (if Nfasteqb g2 F0 then r else Zfastmod r g2) g2 _.

Lemma zc_mul_sound x y (i j:Z) :
  γ x i → γ y j → γ (zc_mul x y) (i * j).

Program Definition zc_quot_pos (x: zcongr) (y: Nfast) : zcongr :=
  match divide (Nfast_of_Zfast (Zfastabs x.(zc_rem))) y,
        divide x.(zc_mod) y with
  | true, true =>
    {| zc_rem := Zfastdiv x.(zc_rem) y ; zc_mod := Nfastdiv x.(zc_mod) y |}
  | _, _ => ⊤
  end.

Lemma zc_quot_pos_sound x y (i:Z) :
  γ x i → γ (zc_quot_pos x (N.pos y)) (i ÷ Zpos y).

Program Definition zc_div_pos (x: zcongr) (y: Nfast) : zcongr :=
  match divide x.(zc_mod) y with
  | true => {| zc_rem := Zfastdiv x.(zc_rem) y;
               zc_mod := Nfastdiv x.(zc_mod) y |}
  | _ => top
  end.

Lemma zc_div_pos_sound x y (i:Z) :
  γ x i → γ (zc_div_pos x (N.pos y)) (i / Zpos y).

Definition zc_quot (x y: zcongr) : zcongr+⊥ :=
  if Nfasteqb y.(zc_mod) F0
  then match Zfastcompare y.(zc_rem) F0 with
       | Eq => Bot
       | Lt => NotBot (zc_neg (zc_quot_pos x (Nfast_of_Zfast (Zfastopp y.(zc_rem)))))
       | Gt => NotBot (zc_quot_pos x (Nfast_of_Zfast (y.(zc_rem))))
       end
  else top.


Lemma zc_quot_sound x y (i j:Z) :
  γ x i → γ y j → j <> 0 -> γ (zc_quot x y) (i ÷ j).

Definition zc_shl (x y: zcongr) : zcongr :=
  if Nfasteqb y.(zc_mod) F0
  then match Zfastcompare y.(zc_rem) F0 with
       | Eq => x
       | Gt => zc_mul x (zc_const (Zfastshl F1 y.(zc_rem)))
       | Lt => zc_div_pos x (Nfastshl F1 (Nfast_of_Zfast (Zfastopp y.(zc_rem))))
       end
  else top.

Lemma zc_shl_sound x y (i j:Z) :
  γ x i → γ y j → γ (zc_shl x y) (Z.shiftl i j).

Definition zc_shr (x y: zcongr) : zcongr :=
  if Nfasteqb y.(zc_mod) F0
  then match Zfastcompare y.(zc_rem) F0 with
       | Eq => x
       | Lt => zc_mul x (zc_const (Zfastshr F1 y.(zc_rem)))
       | Gt => zc_div_pos x (Nfastshl F1 (Nfast_of_Zfast y.(zc_rem)))
       end
  else top.

Lemma zc_shr_sound x y (i j:Z) :
  γ x i → γ y j → γ (zc_shr x y) (Z.shiftr i j).

Program Definition zc_remainder (x y: zcongr) : zcongr :=
  let y' := Zfastabs y.(zc_rem) in
  if Nfasteqb y.(zc_mod) F0 && divide x.(zc_rem) y' && divide x.(zc_mod) y'
  then zc_const F0
  else
    let m := Nfastgcd x.(zc_mod) (Nfastgcd y.(zc_mod) (Zfastabs y.(zc_rem))) in
    ZC (if Nfasteqb m F0 then x.(zc_rem) else Zfastmod x.(zc_rem) m) m _.

Lemma zc_remainder_sound x y (i j:Z) :
  j <> 0 -> γ x i → γ y j → γ (zc_remainder x y) (Z.rem i j).

Definition zc_cmp_eq (b: bool) (x y: zcongr) : zcongr :=
  match Nfasteqb x.(zc_mod) F0, Nfasteqb y.(zc_mod) F0 with
  | true, true => zc_bool (Bool.eqb b (Zfasteqb x.(zc_rem) y.(zc_rem)))
  | true, false =>
    if divide (Zfastsub x.(zc_rem) y.(zc_rem)) y.(zc_mod) then top
    else zc_bool (negb b)
  | fase, true =>
    if divide (Zfastsub x.(zc_rem) y.(zc_rem)) x.(zc_mod) then top
    else zc_bool (negb b)
  | false, false =>
top
  end.

Definition zc_cmp (cmp: comparison) (x y: zcongr) : zcongr :=
  match cmp with
  | Ceq => zc_cmp_eq true x y
  | Cne => zc_cmp_eq false x y
  | _ =>
    top
  end.

Definition zc_forward_unop op (x:zcongr+⊤) : zcongr+⊤ :=
  match op with
  | IOneg => match x with All => All | Just x => Just (zc_neg x) end
  | IOnot => extern_top (zc_add Zfastsub (zc_const (Fm1)) (intern_top x))
  | IOnegf | IOabsf | IOsingleoffloat | IOzoffloat | IOfloatofz | IOsingleofz
    => All
  end.

Definition zc_backward_unop op (ab:zcongr+⊤) : zcongr+⊤ :=
  match op with
  | IOneg => match ab with All => All | Just ab => Just (zc_neg ab) end
  | IOnot => extern_top (zc_add Zfastsub (zc_const F1) (intern_top ab))
  | _ => top
  end.

Lemma lor_pos_neg:
  ∀ a, ∃ (k:N), Z.lor (Z.pos a) (Z.neg a) = -2^k.

Lemma lor_opp:
  ∀ a, a = 0 \/ ∃ (k:N), Z.lor a (-a) = -2^k.

Program Definition zc_forward_and x y :=
  let maskx := Zfastlor x.(zc_mod) (Zfastopp x.(zc_mod)) in
  let masky := Zfastlor y.(zc_mod) (Zfastopp y.(zc_mod)) in
  let unknownx := Zfastlor maskx x.(zc_rem) in
  let unknowny := Zfastlor masky y.(zc_rem) in
  let unknowndirect := Zfastlor maskx masky in
  let unknown := Zfastland (Zfastland unknownx unknowny) unknowndirect in
  let modu := Zfastlor unknown (Zfastopp unknown) in
  let rem := Zfastland (Zfastland x.(zc_rem) y.(zc_rem)) (Zfastsub Fm1 modu) in
  ZC rem (Zfastabs modu) _.

Program Definition zc_forward_or x y :=
  let maskx := Zfastlor x.(zc_mod) (Zfastopp x.(zc_mod)) in
  let masky := Zfastlor y.(zc_mod) (Zfastopp y.(zc_mod)) in
  let unknownx := Zfastlor maskx (Zfastlnot x.(zc_rem)) in
  let unknowny := Zfastlor masky (Zfastlnot y.(zc_rem)) in
  let unknowndirect := Zfastlor maskx masky in
  let unknown := Zfastland (Zfastland unknownx unknowny) unknowndirect in
  let modu := Zfastlor unknown (Zfastopp unknown) in
  let rem := Zfastland (Zfastlor x.(zc_rem) y.(zc_rem)) (Zfastsub Fm1 modu) in
  ZC rem (Zfastabs modu) _.

Program Definition zc_forward_xor x y :=
  let maskx := Zfastlor x.(zc_mod) (Zfastopp x.(zc_mod)) in
  let masky := Zfastlor y.(zc_mod) (Zfastopp y.(zc_mod)) in
  let unknown := Zfastlor maskx masky in
  let modu := Zfastlor unknown (Zfastopp unknown) in
  let rem := Zfastland (Zfastlxor x.(zc_rem) y.(zc_rem)) (Zfastsub Fm1 modu) in
  ZC rem (Zfastabs modu) _.

Definition zc_forward_binop op (x y:zcongr+⊤) : zcongr+⊤+⊥ :=
  match op with
  | IOadd | IOsub | IOmul | IOdiv | IOshl | IOshr | IOmod | IOcmp _
  | IOand | IOor | IOxor =>
    let x := intern_top x in
    let y := intern_top y in
    match op with
    | IOadd => NotBot (extern_top (zc_add Zfastadd x y))
    | IOsub => NotBot (extern_top (zc_add Zfastsub x y))
    | IOmul => NotBot (extern_top (zc_mul x y))
    | IOdiv => fmap extern_top (zc_quot x y)
    | IOshl => NotBot (extern_top (zc_shl x y))
    | IOshr => NotBot (extern_top (zc_shr x y))
    | IOmod => NotBot (extern_top (zc_remainder x y))
    | IOcmp cmp => NotBot (extern_top (zc_cmp cmp x y))
    | IOand => NotBot (extern_top (zc_forward_and x y))
    | IOor => NotBot (extern_top (zc_forward_or x y))
    | IOxor => NotBot (extern_top (zc_forward_xor x y))
    | _ => top
    end
  | IOcmpf _ | IOaddf | IOsubf | IOmulf | IOdivf => top
  end.

Definition zc_bw_cmp (cmp: comparison) (res: zcongr) (x y: zcongr) : (zcongr+⊤ * zcongr+⊤)+⊥ :=
  if Nfasteqb res.(zc_mod) F0
  then let cmp := if Zfasteqb res.(zc_rem) F0 then negate_comparison cmp else cmp in
       match cmp with
       | Ceq => do z <- x ⊓ y; ret (extern_top z, extern_top z)
       | _ => ret (extern_top x, extern_top y)
       end
  else NotBot (extern_top x, extern_top y).

Definition zc_backward_add res l r :=
  NotBot (extern_top (zc_add Zfastsub res r), extern_top (zc_add Zfastsub res l)).

Definition zc_backward_sub res l r :=
  NotBot (extern_top (zc_add Zfastadd res r), extern_top (zc_add Zfastsub l res)).

Program Definition zc_backward_mod res (l r:zcongr) :=
  let m := Nfastgcd res.(zc_mod) (Nfastgcd r.(zc_mod) (Zfastabs r.(zc_rem))) in
  NotBot (
      extern_top (ZC (if Nfasteqb m F0 then res.(zc_rem)
                      else Zfastmod res.(zc_rem) m) m _),
      ⊤:zcongr+⊤).

Program Definition zc_backward_and_l res x y :=
  let maskres := Zfastlor res.(zc_mod) (Zfastopp res.(zc_mod)) in
  let maskx := Zfastlor x.(zc_mod) (Zfastopp x.(zc_mod)) in
  let masky := Zfastlor y.(zc_mod) (Zfastopp y.(zc_mod)) in
  let unknown0res :=
    Zfastlor (Zfastlor (res.(zc_rem)) (Zfastlnot y.(zc_rem)))
             (Zfastlor masky maskres)
  in
  let unknown0 := Zfastland unknown0res (Zfastlor maskx x.(zc_rem)) in
  let unknown1res := Zfastlor (Zfastlnot res.(zc_rem)) maskres in
  let unknown1 := Zfastland unknown1res (Zfastlor maskx (Zfastlnot x.(zc_rem))) in
  if Zfasteqb (Zfastlor unknown0 unknown1) Fm1 then
    let unknown := Zfastland unknown0 unknown1 in
    let modu := Zfastlor unknown (Zfastopp unknown) in
    let rem := Zfastland (Zfastland unknown0 (Zfastlnot unknown1)) (Zfastsub Fm1 modu) in
    NotBot (ZC rem (Zfastabs modu) _)
  else Bot.

Program Definition zc_backward_or_l res x y :=
  let maskres := Zfastlor res.(zc_mod) (Zfastopp res.(zc_mod)) in
  let maskx := Zfastlor x.(zc_mod) (Zfastopp x.(zc_mod)) in
  let masky := Zfastlor y.(zc_mod) (Zfastopp y.(zc_mod)) in
  let unknown1res :=
    Zfastlor (Zfastlor (Zfastlnot res.(zc_rem)) y.(zc_rem))
             (Zfastlor masky maskres)
  in
  let unknown1 := Zfastland unknown1res (Zfastlor maskx (Zfastlnot x.(zc_rem))) in
  let unknown0res := Zfastlor res.(zc_rem) maskres in
  let unknown0 := Zfastland unknown0res (Zfastlor maskx x.(zc_rem)) in
  if Zfasteqb (Zfastlor unknown0 unknown1) Fm1 then
    let unknown := Zfastland unknown0 unknown1 in
    let modu := Zfastlor unknown (Zfastopp unknown) in
    let rem := Zfastland (Zfastland unknown0 (Zfastlnot unknown1))
                         (Zfastsub Fm1 modu) in
    NotBot (ZC rem (Zfastabs modu) _)
  else
    Bot.

Definition zc_backward_binop op res l r :=
  match op with
  | IOadd => zc_backward_add res (intern_top l) (intern_top r)
  | IOsub => zc_backward_sub res (intern_top l) (intern_top r)
  | IOmod => zc_backward_mod res (intern_top l) (intern_top r)
  | IOand =>
    let l := intern_top l in let r := intern_top r in
    do l <- zc_backward_and_l res l r;
    do r <- zc_backward_and_l res r l;
    ret (extern_top l, extern_top r)
  | IOor =>
    let l := intern_top l in let r := intern_top r in
    do l <- zc_backward_or_l res l r;
    do r <- zc_backward_or_l res r l;
    ret (extern_top l, extern_top r)
  | IOxor =>
    let l := intern_top l in let r := intern_top r in
    NotBot (extern_top (zc_forward_xor res r),
            extern_top (zc_forward_xor res l))
  | IOcmp cmp =>
    zc_bw_cmp cmp res (intern_top l) (intern_top r)
  | _ => NotBot (top, top)
  end.

Lemma lor_div:
  ∀ a, (Z.lor a (-a)|a).

Lemma congr_testbit :
  ∀ a b c, a ≡ b [c] ->
  ∀ i, Z.testbit (Z.lor c (-c)) i = false ->
    Z.testbit a i = Z.testbit b i.

Lemma testbit_congr :
  ∀ a b c,
    (∀ i, 0 <= i -> Z.testbit (Z.lor c (-c)) i = false ->
          Z.testbit a i = Z.testbit b i) ->
    a ≡ b [-Z.lor c (-c)].

Lemma zc_forward_and_sound x y (x0 y0:Z) :
  γ x x0 → γ y y0 → γ (zc_forward_and x y) (Z.land x0 y0).

Lemma zc_forward_or_sound x y (x0 y0:Z) :
  γ x x0 → γ y y0 → γ (zc_forward_or x y) (Z.lor x0 y0).

Lemma zc_forward_xor_sound x y (x0 y0:Z) :
  γ x x0 → γ y y0 → γ (zc_forward_xor x y) (Z.lxor x0 y0).

Lemma zcmp_eq_spec i j : Zcmp Ceq i j = eqb true (i =? j).

Lemma zcmp_ne_spec i j : Zcmp Cne i j = eqb false (i =? j).

Lemma zc_cmp_eq_sound b x y (i j:Z) :
  i ∈ γ(x) → j ∈ γ(y) → ((if Bool.eqb b (i =? j) return Zfast then F1 else F0):Z) ∈ γ(zc_cmp_eq b x y).

Lemma zc_cmp_sound c x y (i j:Z) :
  γ x i → γ y j → γ (zc_cmp c x y) ((if Zcmp c i j return Zfast then F1 else F0):Z).

Instance zc_ideal_gamma : gamma_op zcongr ideal_num := fun ab x =>
  match x with INz z => (z:Z) ∈ γ ab | INf _ => False end.

Lemma extern_top_correct_id:
  ∀ (ab:zcongr) (x:Z), x ∈ γ ab -> INz x ∈ γ (extern_top ab).

Lemma intern_top_correct_id:
  ∀ (ab:zcongr+⊤) (x:Z), INz x ∈ γ ab -> x ∈ γ (intern_top ab).

Lemma zc_forward_unop_sound op i a :
  γ a i → ∀ n, eval_iunop op i n → γ (zc_forward_unop op a) n.

Lemma zc_forward_binop_sound op :
  ∀ i a, γ a i →
  ∀ j b, γ b j →
  ∀ n, eval_ibinop op i j n →
       γ (zc_forward_binop op a b) n.

Lemma zc_backward_add_sound:
  ∀ i a, γ a i →
  ∀ j b, γ b j →
  ∀ res, γ res (i+j) ->
  γ (zc_backward_add res a b) (INz i, INz j).

Lemma zc_backward_sub_sound:
  ∀ i a, γ a i →
  ∀ j b, γ b j →
  ∀ res, γ res (i-j) ->
  γ (zc_backward_sub res a b) (INz i, INz j).

Lemma zc_backward_mod_sound:
  ∀ i a, γ a i →
  ∀ j b, j <> 0 -> γ b j →
  ∀ res, γ res (Z.rem i j) ->
  γ (zc_backward_mod res a b) (INz i, INz j).

Lemma zc_bw_cmp_sound c:
  ∀ i a, γ a i →
  ∀ j b, γ b j →
  ∀ res, γ res ((if Zcmp c i j then F1 else F0):Z) ->
  γ (zc_bw_cmp c res a b) (INz i, INz j).

Lemma zc_backward_and_l_sound:
  ∀ i a, γ a i →
  ∀ j b, γ b j →
  ∀ res, γ res (Z.land i j) ->
  γ (zc_backward_and_l res a b) i.

Lemma zc_backward_or_l_sound:
  ∀ i a, γ a i →
  ∀ j b, γ b j →
  ∀ res, γ res (Z.lor i j) ->
  γ (zc_backward_or_l res a b) i.

Lemma zc_backward_binop_sound op :
  ∀ i a, γ a i →
  ∀ j b, γ b j →
  ∀ n res, γ res n ->
  eval_ibinop op i j n →
  γ (zc_backward_binop op res a b) (i, j).

Definition enrich_query_chan fev (chan:query_chan) : query_chan :=
  {| get_var_ty := chan.(get_var_ty);
     get_itv := chan.(get_itv);
     get_congr expr :=
       do ab <- fev expr;
       meet (NotBot (intern_top ab)) (chan.(get_congr) expr);
     get_eq_expr := chan.(get_eq_expr);
     linearize_expr := chan.(linearize_expr) |}.

Instance zc_ideal_non_rel (_:unit) : ab_ideal_nonrel zcongr :=
  { widen := join
  ; const n := match n with INf _ => All | INz z => Just (zc_const z) end
  ; z_itv itv := All
  ; forward_unop op ab := NotBot (zc_forward_unop op ab)
  ; forward_binop op l r := zc_forward_binop op l r
  ; backward_unop op res ab := NotBot ab
  ; backward_binop op res l r :=
      match res with
        | All => top
        | Just res => zc_backward_binop op res l r
      end
  ; forward_var fev x ab c := NotBot ab
  ; backward_var fev AB bev var_ref x ab abenv :=
      do abenv' <- var_ref ab (fst abenv);
      match (snd abenv).(get_eq_expr) x with
      | Some (Leaf e) => bev e ab (abenv', snd abenv)
      | _ => NotBot abenv'
      end
  ; enrich_query_chan := enrich_query_chan
  ; process_msg fev TAB bev msg ab := NotBot (fst ab, msg::nil)
  ; assign_msgs x zc :=
      if Nfasteqb zc.(zc_mod) F0 then Known_value_msg x (INz zc.(zc_rem))::nil
      else if Nfasteqb zc.(zc_mod) F1 then nil
           else Congr_msg x zc::nil
  ; assume_msgs x zc_old zc :=
      if Nfasteqb zc.(zc_mod) F0 then Known_value_msg x (INz zc.(zc_rem))::nil
      else if Nfasteqb zc.(zc_mod) F1 then nil
           else Congr_msg x zc::nil
  }.

Instance zc_ideal_non_rel_correct : ab_ideal_nonrel_correct (zc_ideal_non_rel tt) _.

Definition t := @IdealBoxDomain.t zcongr.

Instance zcongr_ideal_env : ab_ideal_env t (t+⊥) :=
  ideal_box_domain _ zc_ideal_non_rel_correct.