# Module ZCongruences

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).
Proof.
intros. exists 0. simpl. Psatz.lia. Qed.

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).
Proof.
destruct b; exists 0; reflexivity. Qed.

Program Definition zc_add (plus: ZfastZfastZfast) (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 _.
Next Obligation.
fastunwrap. destruct N.gcd. discriminate. apply Z_mod_lt. auto. Qed.

Lemma zc_add_sound (plus: ZfastZfastZfast) (x y: zcongr) (i j: Z) :
(∀ n u u' v v', uu' [n] → vv' [n] → plus u vplus u' v' [n]) →
γ x i → γ y j → γ (zc_add plus x y) (plus i j:Z).
Proof.
destruct x as [[xr] [xm] ?]. destruct y as [[yr] [ym] ?]. simpl.
intros [p Hp] [q Hq]. simpl in Hp, Hq. unfold zc_gamma. simpl. fastunwrap. subst.
destruct (N.eqb_spec (N.gcd xm ym) 0).
- apply N.gcd_eq_0 in e. destruct e. subst. exists 0. ring_simplify.
f_equal; f_equal; f_equal; ring.
- eapply congr_trans, congr_mod_compat. 2:Psatz.lia.
rewrite Ngcd_is_Zgcd. apply COMPAT; (eapply congr_divide; [eexists; reflexivity|]).
apply Zgcd_divides_l. apply Zgcd_divides_r.
Qed.

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) _.
Next Obligation.
fastunwrap. destruct (x.(zc_mod)) as [[]]. discriminate. apply Z_mod_lt. auto.
Qed.

Lemma zc_neg_sound x (i:Z) :
γ x i → γ (zc_neg x) (-i).
Proof.
intros. unfold zc_neg, zc_gamma in *. simpl in *. fastunwrap.
destruct (x.(zc_mod)) as [[]]. apply congr_neg_compat, H.
simpl. eapply congr_trans, congr_mod_compat. 2:Psatz.lia.
apply congr_neg_compat. auto.
Qed.

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 _.
Next Obligation.
fastunwrap. rewrite (proj2 (N.eqb_neq _ _)) by Psatz.lia.
apply Z_mod_lt. Psatz.lia.
Qed.

Lemma zc_mul_sound x y (i j:Z) :
γ x i → γ y j → γ (zc_mul x y) (i * j).
Proof.
unfold zc_mul.
destruct x as [[xr] [xm]], y as [[yr] [ym]]. simpl. intros [qx Hx] [qy Hy].
unfold zc_gamma. simpl in *. fastunwrap.
set (m := N.gcd (N.gcd (Z.abs_N xr) xm * ym) (Z.abs_N yr * xm)).
assert (m | (xr*yr - i*j)).
{ subst m xr yr.
replace ((i + qx * (Z.of_N xm)) * (j + qy * (Z.of_N ym)) - i * j)
with (((j+qy*ym)*xm)*qx + ((i+qx*xm)*qy-xm*qx*qy)*ym) by (fastunwrap; ring).
fastunwrap.
rewrite !Ngcd_is_Zgcd, !N2Z.inj_mul, !Ngcd_is_Zgcd by Psatz.lia.
replace (Z.of_N xm) with (Z.of_N (Z.abs_N xm)) by (destruct xm; auto).
rewrite <- N2Z.inj_mul, <- Zabs2N.inj_mul, !N2Z.inj_abs_N, Z.gcd_abs_l, Z.gcd_abs_r.
fastunwrap. replace (Z.abs (Z.of_N xm)) with (Z.of_N xm) by Psatz.lia.
eapply Z.divide_mul_l, Zgcd_divides_r.
eapply Z.divide_trans, Z.mul_divide_mono_r, Z.divide_sub_r. apply Zgcd_divides_l.
apply Z.divide_mul_l, Zgcd_divides_l.
apply Z.divide_mul_l, Z.divide_mul_l, Zgcd_divides_r. }
destruct (N.eqb_spec m 0).
- rewrite e in *. apply Z.divide_0_l in H. exists 0. simpl. Psatz.lia.
- eapply congr_trans, congr_mod_compat. 2:Psatz.lia.
destruct H as [q H]. exists q. fastunwrap. Psatz.lia.
Qed.

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.
Next Obligation.
symmetry in Heq_anonymous, Heq_anonymous0.
apply divide_ok in Heq_anonymous. apply divide_ok in Heq_anonymous0.
fastunwrap. rewrite Z2N.id in Heq_anonymous by Psatz.lia.
pose proof (zc_rem_itv x). destruct (zc_mod x) as [[]].
rewrite N.div_0_l in H; discriminate. specialize (H0 eq_refl). destruct H0.
destruct y as [[|y]]. discriminate. split.
- apply Z_div_le with (c:=Npos y) in H0. rewrite Z.div_0_l in H0.
auto. discriminate. reflexivity.
- rewrite N2Z.inj_abs_N in Heq_anonymous.
apply -> Z.divide_abs_r in Heq_anonymous. destruct Heq_anonymous, Heq_anonymous0.
simpl in *. rewrite N2Z.inj_gt, N2Z.inj_div in *.
simpl in *. rewrite H2, H3 in *. clear H2 p H3 x.
rewrite !Z.div_mul in * by discriminate.
eapply Zmult_lt_reg_r; eauto. reflexivity.
Qed.

Lemma zc_quot_pos_sound x y (i:Z) :
γ x i → γ (zc_quot_pos x (N.pos y)) (i ÷ Zpos y).
Proof.
unfold zc_quot_pos.
generalize (zc_quot_pos_obligation_1 x (N.pos y)).
repeat match goal with
| |- context [divide ?a ?b] =>
pose proof divide_ok a b; destruct (divide a b)
end; intros; try apply top_correct.
simpl. unfold zc_gamma. simpl. clear a.
destruct H as [? _], H0 as [? _]. specialize (H eq_refl). specialize (H0 eq_refl).
fastunwrap. rewrite Z2N.id in H by Psatz.lia.
rewrite N2Z.inj_abs_N in H. apply -> Z.divide_abs_r in H.
destruct H1 as [q Hq]. exists q.
assert (Z.pos y | i).
{ replace i with (x.(zc_rem) - q*x.(zc_mod)) by Psatz.lia.
apply Z.divide_sub_r, Z.divide_mul_r; auto. }
rewrite Hq. rewrite Z.quot_div_exact by easy.
destruct H1. subst i.
rewrite Z_div_plus_full_l, Z_div_mult_full, N2Z.inj_div by discriminate.
rewrite Z.divide_div_mul_exact. auto. discriminate. auto.
Qed.

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.
Next Obligation.
pose proof (zc_rem_itv x). destruct (zc_mod x) as [[]].
rewrite N.div_0_l in H; discriminate. destruct y as [[|y]]. discriminate.
specialize (H0 eq_refl). destruct H0.
symmetry in Heq_anonymous. apply divide_ok in Heq_anonymous.
split.
- apply Z_div_le with (c:=N.pos y) in H0. rewrite Z.div_0_l in H0.
auto. discriminate. reflexivity.
- destruct Heq_anonymous. fastunwrap.
rewrite N2Z.inj_gt, N2Z.inj_div, H2 in *. clear H2 p.
simpl in *. rewrite !Z.div_mul in * by discriminate.
eapply Zmult_lt_reg_r with (p:=Z.pos y). reflexivity.
pose proof (Zmod_eq (zc_rem x) (Z.pos y) eq_refl).
pose proof (Z_mod_lt (zc_rem x) (Z.pos y) eq_refl).
omega.
Qed.

Lemma zc_div_pos_sound x y (i:Z) :
γ x i → γ (zc_div_pos x (N.pos y)) (i / Zpos y).
Proof.
unfold zc_div_pos. generalize (zc_div_pos_obligation_1 x (N.pos y)).
repeat match goal with
| |- context [divide ?a ?b] =>
pose proof divide_ok a b; destruct (divide a b)
end; intros; try apply top_correct.
destruct x as [[xr] [xm]]. destruct H0 as [q Hq]. unfold zc_gamma. simpl in *. subst.
clear a. destruct H as [? _]. specialize (H eq_refl).
exists q. destruct H. rewrite N2Z.inj_div, H. simpl.
rewrite Z_div_mult_full by discriminate. rewrite Z.mul_assoc.
Qed.

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 jj <> 0 -> γ (zc_quot x y) (i ÷ j).
Proof.
unfold zc_quot. fastunwrap. destruct y as [[yr] [ym]].
simpl. destruct ym. 2:intros; apply top_correct. simpl.
unfold zc_gamma; simpl; intros. destruct H0.
assert (j = yr) by Psatz.lia. clear H0. subst.
destruct yr as [|y'|y']; fastunwrap.
- simpl. auto.
- apply zc_quot_pos_sound. auto.
- unfold Z.compare.
change (Z.neg y') with (-Z.pos y'). rewrite Zquot.Zquot_opp_r.
apply zc_neg_sound, zc_quot_pos_sound. auto.
Qed.

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).
Proof.
unfold zc_shl. destruct y as [[yr] [ym]]. destruct ym; auto; simpl.
2:intros; apply top_correct. fastunwrap.
intros K H. apply congr_0_eq in H. subst.
destruct yr as [|y'|y']. exact K.
- simpl zc_rem. fastunwrap. rewrite !Z.shiftl_mul_pow2, Z.mul_1_l by Psatz.lia.
apply zc_mul_sound, zc_const_sound. auto.
- simpl zc_rem. fastunwrap.
rewrite !Z.shiftl_div_pow2, N.shiftl_mul_pow2, N.mul_1_l by Psatz.lia.
simpl. rewrite <- Pos2Z.inj_pow_pos. apply zc_div_pos_sound, K.
Qed.

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).
Proof.
unfold zc_shr. destruct y as [[yr] [ym]]. destruct ym; auto; simpl.
2:intros; apply top_correct. fastunwrap.
intros K H. apply congr_0_eq in H. subst.
destruct yr as [|y'|y']. exact K.
- simpl zc_rem. fastunwrap.
rewrite !Z.shiftr_div_pow2, N.shiftl_mul_pow2, N.mul_1_l by Psatz.lia.
simpl. rewrite <- Pos2Z.inj_pow_pos. apply zc_div_pos_sound, K.
- simpl zc_rem. fastunwrap. rewrite !Z.shiftr_mul_pow2, Z.mul_1_l by Psatz.lia.
apply zc_mul_sound, zc_const_sound. auto.
Qed.

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 _.
Next Obligation.
fastunwrap. destruct N.gcd. discriminate. apply Z_mod_lt. auto. Qed.

Lemma zc_remainder_sound x y (i j:Z) :
j <> 0 -> γ x i → γ y j → γ (zc_remainder x y) (Z.rem i j).
Proof.
unfold zc_remainder.
destruct y as [[yr] [ym]], x as [[xr] [xm]]. simpl. intros Hj [qx Hx] [qy Hy]. simpl in *.
destruct (Nfasteqb ym F0 && divide xr (Zfastabs yr) &&
divide xm (Zfastabs yr)) eqn:?.
{ rewrite !Bool.andb_true_iff in Heqb. fastunwrap. destruct Heqb as [[??]?].
apply N.eqb_eq in H. subst ym. apply divide_ok in H0. apply divide_ok in H1.
fastunwrap. rewrite N2Z.inj_abs_N, Z.divide_abs_l in *.
exists 0. simpl. erewrite (proj2 (Z.rem_divide _ _ Hj)). auto.
replace i with (i + qx * xm - qx * xm) by ring.
replace j with yr in * by Psatz.lia. clear Hy zc_rem_itv.
apply Z.divide_sub_r. subst xr. auto. apply Z.divide_mul_r. auto. }
unfold zc_gamma. simpl. fastunwrap. set (m:=N.gcd xm (N.gcd ym (Z.abs_N yr))).
assert (m|xr - Z.rem i j).
{ subst m xr yr. rewrite Z.rem_eq by auto.
replace (i + qx * (Z.of_N xm) - (i - j * (i ÷ j)))
with (Z.of_N xm * qx + ((j + qy * ym) * (i ÷ j) - ym * (qy * (i ÷ j)))) by ring.
fastunwrap. rewrite !Ngcd_is_Zgcd, N2Z.inj_abs_N, Z.gcd_abs_r.
apply Z.divide_mul_l, Zgcd_divides_l.
eapply Zdivides_trans, Z.divide_mul_l, Zgcd_divides_r. apply Zgcd_divides_r.
eapply Zdivides_trans, Z.divide_mul_l, Zgcd_divides_l. apply Zgcd_divides_r. }
destruct m.
apply Z.divide_0_l in H. exists 0. simpl. Psatz.lia.
eapply congr_trans, congr_mod_compat, eq_refl.
destruct H as [q H]. exists q. simpl in *. Psatz.lia.
Qed.

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.
Proof.
simpl. destruct a; simpl.
- replace (Pos.ldiff a a) with 0%N by (symmetry; apply (N.ldiff_diag (N.pos a))).
exists 0%N. auto.
- induction a; simpl.
+ simpl. replace (Pos.ldiff a a) with 0%N by (symmetry; apply (N.ldiff_diag (N.pos a))).
exists 1%N. auto.
+ assert (∀ x, Z.neg (N.succ_pos (Pos.Nsucc_double x)) = -2*x-2)%Z.
{ intros []. auto. simpl. intro. rewrite Pos.add_1_r. auto. }
rewrite H.
destruct IHa as [k Hk]. exists (k+1)%N.
destruct Pos.ldiff. auto. simpl. zify; omega.
+ exists 1%N. auto.
- exists 0%N. auto.
Qed.

Lemma lor_opp:
∀ a, a = 0 \/ ∃ (k:N), Z.lor a (-a) = -2^k.
Proof.
intros. destruct a. auto.
right. apply lor_pos_neg.
right. rewrite Z.lor_comm. apply lor_pos_neg.
Qed.

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 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) _.
Next Obligation.
fastunwrap.
match goal with
| |- context [Z.lor (?unknown0) (-?unknown0)] => set (unknown:=unknown0) in *
end.
change (0 <= Z.land (Z.land (zc_rem x) (zc_rem y))
(-1- Z.lor unknown (- unknown))
< Z.of_N (Z.abs_N (Z.lor unknown (- unknown)))).
rewrite N2Z.inj_abs_N.
destruct (lor_opp unknown) as [|[k Hk]]. rewrite H0 in H. discriminate.
rewrite Hk, Z.abs_neq'; rewrite Z.opp_involutive.
2:apply Z.pow_nonneg; Psatz.lia.
set (rem := Z.land (Z.land (zc_rem x) (zc_rem y)) (-1--2 ^ k)).
assert (0 <= rem).
{ apply Z.land_nonneg. right.
assert (0 < 2 ^ k) by (apply Z.pow_pos_nonneg; fastunwrap; Psatz.lia).
Psatz.lia. }
split. auto. fastunwrap. destruct (Z_lt_dec 0 rem).
2:replace rem with 0 by omega; apply Z.pow_pos_nonneg; Psatz.lia.
apply Z.log2_lt_cancel. rewrite Z.log2_pow2 by Psatz.lia.
apply Z.bit_log2 in l. unfold rem at 1 in l.
fastunwrap. replace (-1 - - 2 ^ Z.of_N k) with (Z.lnot (-1*2^Z.of_N k)) in l
by (unfold Z.lnot; omega).
apply Z.nle_gt. intro.
rewrite Z.land_spec, Bool.andb_true_iff, Z.lnot_spec, <- Z.shiftl_mul_pow2,
Z.shiftl_spec, Int.Ztestbit_m1 in l
by (Psatz.lia || apply Z.log2_nonneg).
easy.
Qed.

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 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) _.
Next Obligation.
match goal with
| |- context [Z.lor (?unknown0) (-?unknown0)] => set (unknown:=unknown0) in *
end.
change (0 <= Z.land (Z.lor (zc_rem x) (zc_rem y))
(-1- Z.lor unknown (- unknown))
< Z.of_N (Z.abs_N (Z.lor unknown (- unknown)))).
destruct (lor_opp unknown) as [|[k Hk]]. rewrite H0 in H. discriminate.
rewrite Hk, N2Z.inj_abs_N, Z.abs_neq'; rewrite Z.opp_involutive.
2:apply Z.pow_nonneg; Psatz.lia.
set (rem := Z.land (Z.lor (zc_rem x) (zc_rem y)) (-1 - - 2 ^ k)).
assert (0 <= rem).
{ apply Z.land_nonneg. right.
assert (0 < 2 ^ k) by (apply Z.pow_pos_nonneg; fastunwrap; Psatz.lia).
Psatz.lia. }
split. auto. fastunwrap. destruct (Z_lt_dec 0 rem).
2:replace rem with 0 by omega; apply Z.pow_pos_nonneg; Psatz.lia.
apply Z.log2_lt_cancel. rewrite Z.log2_pow2 by Psatz.lia.
apply Z.bit_log2 in l. unfold rem at 1 in l.
fastunwrap. replace (-1 - - 2 ^ Z.of_N k) with (Z.lnot (-1*2^Z.of_N k)) in l
by (unfold Z.lnot; omega).
apply Z.nle_gt. intro.
rewrite Z.land_spec, Bool.andb_true_iff, Z.lnot_spec, <- Z.shiftl_mul_pow2,
Z.shiftl_spec, Int.Ztestbit_m1 in l
by (Psatz.lia || apply Z.log2_nonneg).
easy.
Qed.

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 modu := Zfastlor unknown (Zfastopp unknown) in
let rem := Zfastland (Zfastlxor x.(zc_rem) y.(zc_rem)) (Zfastsub Fm1 modu) in
ZC rem (Zfastabs modu) _.
Next Obligation.
match goal with
| |- context [Z.lor (?unknown0) (-?unknown0)] => set (unknown:=unknown0) in *
end.
change (0 <= Z.land (Z.lxor (zc_rem x) (zc_rem y))
(-1- Z.lor unknown (- unknown))
< Z.of_N (Z.abs_N (Z.lor unknown (- unknown)))).
destruct (lor_opp unknown) as [|[k Hk]]. rewrite H0 in H. discriminate.
rewrite Hk, N2Z.inj_abs_N, Z.abs_neq'; rewrite Z.opp_involutive. 2:apply Z.pow_nonneg; Psatz.lia.
set (rem := Z.land (Z.lxor (zc_rem x) (zc_rem y)) (-1 - - 2 ^ k)).
assert (0 <= rem).
{ apply Z.land_nonneg. right.
assert (0 < 2 ^ k) by (apply Z.pow_pos_nonneg; fastunwrap; Psatz.lia).
Psatz.lia. }
split. auto. fastunwrap. destruct (Z_lt_dec 0 rem).
2:replace rem with 0 by omega; apply Z.pow_pos_nonneg; Psatz.lia.
apply Z.log2_lt_cancel. rewrite Z.log2_pow2 by Psatz.lia.
apply Z.bit_log2 in l. unfold rem at 1 in l.
fastunwrap. replace (-1 - - 2 ^ Z.of_N k) with (Z.lnot (-1*2^Z.of_N k)) in l
by (unfold Z.lnot; omega).
apply Z.nle_gt. intro.
rewrite Z.land_spec, Bool.andb_true_iff, Z.lnot_spec, <- Z.shiftl_mul_pow2,
Z.shiftl_spec, Int.Ztestbit_m1 in l
by (Psatz.lia || apply Z.log2_nonneg).
easy.
Qed.

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
| 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 <- xy; 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 :=

Definition zc_backward_sub res l r :=

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+⊤).
Next Obligation.
fastunwrap. destruct N.gcd. discriminate. apply Z_mod_lt. auto. Qed.

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)))
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.
Next Obligation.
repeat match goal with
| |- context [Z.lor (?x) (-?x)] =>
try (unfold x; fail 1); let u := fresh "z" in set (u:=x) in *
end.
destruct (lor_opp z2) as [|[k Hk]]. rewrite H0 in H. discriminate.
rewrite Hk, N2Z.inj_abs_N, Z.abs_neq'; rewrite Z.opp_involutive. 2:apply Z.pow_nonneg; Psatz.lia.
match goal with |- context [0 <= ?rem'] => set (rem := rem') end.
assert (0 <= rem).
{ apply Z.land_nonneg. right.
assert (0 < 2 ^ k) by (apply Z.pow_pos_nonneg; fastunwrap; Psatz.lia).
change (0 <= -1 + 2 ^ k). Psatz.lia. }
split. auto. fastunwrap. destruct (Z_lt_dec 0 rem).
2:replace rem with 0 by omega; apply Z.pow_pos_nonneg; Psatz.lia.
apply Z.log2_lt_cancel. rewrite Z.log2_pow2 by Psatz.lia.
apply Z.bit_log2 in l. unfold rem at 1 in l.
fastunwrap. assert (-1 + 2 ^ Z.of_N k = Z.lnot (-1*2^Z.of_N k)) by (unfold Z.lnot; omega).
simpl Z.add in H1. rewrite H1 in l.
apply Z.nle_gt. intro.
rewrite Z.land_spec, Bool.andb_true_iff, Z.lnot_spec, <- Z.shiftl_mul_pow2,
Z.shiftl_spec, Int.Ztestbit_m1 in l
by (Psatz.lia || apply Z.log2_nonneg).
easy.
Qed.

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))
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.
Next Obligation.
repeat match goal with
| |- context [Z.lor (?x) (-?x)] =>
try (unfold x; fail 1); let u := fresh "z" in set (u:=x) in *
end.
destruct (lor_opp z2) as [|[k Hk]]. rewrite H0 in H. discriminate.
rewrite Hk, N2Z.inj_abs_N, Z.abs_neq'; rewrite Z.opp_involutive. 2:apply Z.pow_nonneg; Psatz.lia.
match goal with |- context [0 <= ?rem'] => set (rem := rem') end.
assert (0 <= rem).
{ apply Z.land_nonneg. right.
assert (0 < 2 ^ k) by (apply Z.pow_pos_nonneg; fastunwrap; Psatz.lia).
change (0 <= -1 + 2 ^ k). Psatz.lia. }
split. auto. fastunwrap. destruct (Z_lt_dec 0 rem).
2:replace rem with 0 by omega; apply Z.pow_pos_nonneg; Psatz.lia.
apply Z.log2_lt_cancel. rewrite Z.log2_pow2 by Psatz.lia.
apply Z.bit_log2 in l. unfold rem at 1 in l.
fastunwrap. assert (-1 + 2 ^ Z.of_N k = Z.lnot (-1*2^Z.of_N k)) by (unfold Z.lnot; omega).
simpl Z.add in H1. rewrite H1 in l.
apply Z.nle_gt. intro.
rewrite Z.land_spec, Bool.andb_true_iff, Z.lnot_spec, <- Z.shiftl_mul_pow2,
Z.shiftl_spec, Int.Ztestbit_m1 in l
by (Psatz.lia || apply Z.log2_nonneg).
easy.
Qed.

Definition zc_backward_binop op res l r :=
match op with
| 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).
Proof.
intros. destruct (lor_opp a) as [|[k Hk]].
- exists 0. auto.
- rewrite Hk. exists (-Z.shiftr a k).
apply Z.bits_inj'. intros. fastunwrap.
rewrite Z.mul_opp_opp, <- Z.shiftl_mul_pow2, Z.shiftl_spec by Psatz.lia.
destruct (Z_lt_dec (n-Z.of_N k) 0). 2:rewrite Z.shiftr_spec; f_equal; Psatz.lia.
rewrite Z.testbit_neg_r with (n:=n-Z.of_N k) by omega.
apply (f_equal (fun a => Z.testbit a n)) in Hk.
replace (-2^Z.of_N k) with (-1*2^Z.of_N k) in Hk by ring.
rewrite <- Z.shiftl_mul_pow2, Z.lor_spec, Z.shiftl_spec,
Z.testbit_neg_r with (n:=n-Z.of_N k) in Hk by (zify; omega).
destruct (Z.testbit a n); easy.
Qed.

Lemma congr_testbit :
∀ a b c, ab [c] ->
∀ i, Z.testbit (Z.lor c (-c)) i = false ->
Z.testbit a i = Z.testbit b i.
Proof.
intros a b c [q Hq] i Hi. subst b.
destruct (lor_opp c) as [|[k Hk]]. subst. f_equal. ring.
rewrite Hk in Hi.
replace (-2^k) with (-1*2^k) in Hi by ring.
rewrite <- Z.shiftl_mul_pow2 in Hi by (fastunwrap; Psatz.lia).
destruct (Z_lt_dec i k) as [Hi'|Hi'].
2:rewrite Z.shiftl_spec_high, Int.Ztestbit_m1 in Hi by (fastunwrap; Psatz.lia);
discriminate.
clear Hi.
pose proof (lor_div c). rewrite Hk in H. destruct H.
rewrite H, <- Z.mul_opp_comm, Z.mul_assoc, <- Z.shiftl_mul_pow2 by (fastunwrap; Psatz.lia).
pose proof Z.add_carry_bits a (Z.shiftl (q*-x) k) false.
destruct H0 as (d & ? & ? & ?).
simpl in H0. rewrite Z.add_0_r in H0. fastunwrap. rewrite H0. clear H0.
rewrite Z.lxor_assoc, Z.lxor_spec, <- (xorb_false_r (Z.testbit a i)) at 1. f_equal.
rewrite <- Zdiv2_div in H1.
clear Hk H. revert k i Hi' a d H1 H2.
induction k using N.peano_ind; intros.
- rewrite Z.testbit_neg_r; auto.
- refine (let H := IHk (Z.pred i) _ (Z.div2 a) (Z.div2 d) _ _ in _).
+ zify; omega.
+ rewrite H1 at 1.
rewrite !Z.div2_spec, Z.shiftr_lor, !Z.shiftr_land, Z.shiftr_lor,
Z.shiftr_shiftl_l, Z.sub_1_r, N2Z.inj_succ, Z.pred_succ by (zify; omega).
auto.
+ rewrite H1, Z.lor_spec, !Z.land_spec, Z.lor_spec, Z.shiftl_spec_low, H2,
andb_false_r, andb_false_l by Psatz.lia. auto.
+ rewrite Z.lxor_spec, Z.shiftl_spec_low by auto.
rewrite Z.lxor_spec, Z.shiftl_spec_low, Z.div2_spec in H by (zify; omega).
destruct i.
* rewrite H2. auto.
* rewrite H, Z.shiftr_spec at 1 by (zify; omega). f_equal. f_equal. omega.
* rewrite Z.testbit_neg_r; reflexivity.
Qed.

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) ->
ab [-Z.lor c (-c)].
Proof.
intros.
destruct (lor_opp c) as [|[k Hk]].
{ subst. replace b with a. apply congr_refl.
apply Z.bits_inj'. intros. apply H. auto. apply Z.bits_0. }
assert (∀ i, i < k -> Z.testbit a i = Z.testbit b i).
{ intros. destruct (Z_le_dec 0 i).
apply H. auto. rewrite Hk. replace (-2^k) with (-1*2^k) by ring.
rewrite <- Z.shiftl_mul_pow2, Z.shiftl_spec_low by (zify; omega). auto.
rewrite !Z.testbit_neg_r by omega; auto. }
clear H.
assert (∀ i, 0 <= i -> i < k -> Z.testbit (a-b) i = false).
{ intros i Hi Hi'. clear Hk.
pose proof Z.add_carry_bits a (Z.lnot b) true.
destruct H as (d & ? & ? & ?).
rewrite <- Z.div2_div in H1.
replace (a+Z.lnot b+Z.b2z true) with (a-b) in H by (unfold Z.lnot, Z.b2z; omega).
rewrite H, !Z.lxor_spec, Z.lnot_spec by omega.
rewrite H0, <- negb_xorb_r, xorb_nilpotent by auto.
replace (Z.testbit d i) with true. auto. clear H.
revert i Hi Hi' d a b H0 H1 H2. induction k using N.peano_ind.
- intros. fastunwrap. zify; omega.
- intros. destruct (Z_lt_dec 0 i). 2:rewrite <- H2; f_equal; omega. fastunwrap.
refine (let IHks := IHk (Z.pred i) _ _ (Z.div2 d) (Z.div2 a) (Z.div2 b) _ _ _ in _).
+ omega.
+ zify; omega.
+ intros. destruct (Z_lt_dec i0 0). rewrite !Z.testbit_neg_r; now auto.
rewrite !Z.div2_spec, !Z.shiftr_spec by omega. apply H0. zify; omega.
+ rewrite H1 at 1.
rewrite !Z.div2_spec, Z.shiftr_lor, !Z.shiftr_land, Z.shiftr_lor, Z.lnot_shiftr by omega. auto.
+ rewrite H1, Z.lor_spec, !Z.land_spec, Z.lor_spec, Z.lnot_spec, H0, H2, orb_negb_r,
orb_true_r by (zify; omega).
auto.
+ rewrite Z.div2_spec, Z.shiftr_spec in IHks by omega.
rewrite IHks. f_equal. omega. }
assert (Z.shiftl (Z.shiftr (a-b) k) k = a-b).
{ apply Z.bits_inj'. intros.
rewrite Z.shiftl_spec by auto.
destruct (Z_lt_dec n k).
- rewrite H, Z.testbit_neg_r by omega. auto.
- rewrite Z.shiftr_spec by omega. f_equal. ring. }
rewrite Z.shiftl_mul_pow2 in H1 by (fastunwrap; zify; omega).
exists (-Z.shiftr (a-b) k). rewrite Hk, Z.opp_involutive, <- Zopp_mult_distr_l, H1.
omega.
Qed.

Lemma zc_forward_and_sound x y (x0 y0:Z) :
γ x x0 → γ y y0 → γ (zc_forward_and x y) (Z.land x0 y0).
Proof.
intros Hx0 Hy0.
assert (Hx:=congr_testbit _ _ _ Hx0).
assert (Hy:=congr_testbit _ _ _ Hy0).
unfold zc_forward_and. fastunwrap.
set (maskx := Z.lor (Z.of_N x.(zc_mod)) (-Z.of_N x.(zc_mod))) in *.
set (masky := Z.lor (Z.of_N y.(zc_mod)) (-Z.of_N y.(zc_mod))) in *.
set (unknownx := Z.lor maskx x.(zc_rem)).
set (unknowny := Z.lor masky y.(zc_rem)).
set (unknown := Z.land (Z.land unknownx unknowny) unknowndirect).
set (modu := Z.lor unknown (-unknown)).
assert (modu <= 0).
{ unfold modu. destruct (lor_opp unknown) as [|[k Hk]]. rewrite H. compute. discriminate.
rewrite Hk. apply Z.opp_nonpos_nonneg, Z.pow_nonneg. omega. }
red. red. unfold zc_rem, zc_mod. fold (zc_rem x) (zc_rem y) (zc_mod x) (zc_mod y).
fastunwrap. rewrite N2Z.inj_abs_N, Z.abs_neq by auto. apply testbit_congr.
replace (-1-modu) with (Z.lnot modu) by (unfold Z.lnot; omega).
intros. unfold modu.
rewrite !Z.land_spec, Z.lnot_spec, H1, Bool.andb_true_r by auto.
rewrite Z.lor_spec, Bool.orb_false_iff in H1. destruct H1.
unfold unknown in H1. rewrite !Z.land_spec, !Bool.andb_false_iff in H1.
destruct H1 as [[]|].
- unfold unknownx in H1. rewrite Z.lor_spec, Bool.orb_false_iff in H1.
destruct H1. rewrite Hx, H3 by auto. auto.
- unfold unknowny in H1. rewrite Z.lor_spec, Bool.orb_false_iff in H1.
destruct H1. rewrite Hy, H3, !Bool.andb_false_r by auto. auto.
- unfold unknowndirect in H1. rewrite Z.lor_spec, Bool.orb_false_iff in H1.
destruct H1. rewrite Hx, Hy by auto. auto.
Qed.

Lemma zc_forward_or_sound x y (x0 y0:Z) :
γ x x0 → γ y y0 → γ (zc_forward_or x y) (Z.lor x0 y0).
Proof.
intros Hx0 Hy0.
assert (Hx:=congr_testbit _ _ _ Hx0).
assert (Hy:=congr_testbit _ _ _ Hy0).
unfold zc_forward_or. fastunwrap.
set (maskx := Z.lor (Z.of_N x.(zc_mod)) (-Z.of_N x.(zc_mod))) in *.
set (masky := Z.lor (Z.of_N y.(zc_mod)) (-Z.of_N y.(zc_mod))) in *.
set (unknownx := Z.lor maskx (Z.lnot x.(zc_rem))).
set (unknowny := Z.lor masky (Z.lnot y.(zc_rem))).
set (unknown := Z.land (Z.land unknownx unknowny) unknowndirect).
set (modu := Z.lor unknown (-unknown)).
assert (modu <= 0).
{ unfold modu. destruct (lor_opp unknown) as [|[k Hk]]. rewrite H. compute. discriminate.
rewrite Hk. apply Z.opp_nonpos_nonneg, Z.pow_nonneg. omega. }
red. red. unfold zc_rem, zc_mod. fold (zc_rem x) (zc_rem y) (zc_mod x) (zc_mod y).
fastunwrap. rewrite N2Z.inj_abs_N, Z.abs_neq by auto. apply testbit_congr.
replace (-1-modu) with (Z.lnot modu) by (unfold Z.lnot; omega).
intros. unfold modu.
rewrite Z.land_spec, !Z.lor_spec, Z.lnot_spec, H1, Bool.andb_true_r by auto.
rewrite Z.lor_spec, Bool.orb_false_iff in H1. destruct H1.
unfold unknown in H1. rewrite !Z.land_spec, !Bool.andb_false_iff in H1.
destruct H1 as [[]|].
- unfold unknownx in H1. rewrite Z.lor_spec, Z.lnot_spec, Bool.orb_false_iff, negb_false_iff in H1 by auto.
destruct H1. rewrite Hx, H3 by auto. auto.
- unfold unknowny in H1. rewrite Z.lor_spec, Z.lnot_spec, Bool.orb_false_iff, negb_false_iff in H1 by auto.
destruct H1. rewrite Hy, H3, !Bool.orb_true_r by auto. auto.
- unfold unknowndirect in H1. rewrite Z.lor_spec, Bool.orb_false_iff in H1.
destruct H1. rewrite Hx, Hy by auto. auto.
Qed.

Lemma zc_forward_xor_sound x y (x0 y0:Z) :
γ x x0 → γ y y0 → γ (zc_forward_xor x y) (Z.lxor x0 y0).
Proof.
intros Hx0 Hy0.
assert (Hx:=congr_testbit _ _ _ Hx0).
assert (Hy:=congr_testbit _ _ _ Hy0).
unfold zc_forward_xor. fastunwrap.
set (maskx := Z.lor (Z.of_N x.(zc_mod)) (-Z.of_N x.(zc_mod))) in *.
set (masky := Z.lor (Z.of_N y.(zc_mod)) (-Z.of_N y.(zc_mod))) in *.
set (modu := Z.lor unknown (-unknown)).
assert (modu <= 0).
{ unfold modu. destruct (lor_opp unknown) as [|[k Hk]]. rewrite H. compute. discriminate.
rewrite Hk. apply Z.opp_nonpos_nonneg, Z.pow_nonneg. omega. }
red. red. unfold zc_rem, zc_mod. fold (zc_rem x) (zc_rem y) (zc_mod x) (zc_mod y).
fastunwrap. rewrite N2Z.inj_abs_N, Z.abs_neq by auto. apply testbit_congr.
replace (-1-modu) with (Z.lnot modu) by (unfold Z.lnot; omega).
intros. unfold modu.
destruct (Z_le_dec 0 i). 2:rewrite !Z.testbit_neg_r by omega; auto.
rewrite Z.land_spec, !Z.lxor_spec, Z.lnot_spec, H1, Bool.andb_true_r by auto.
rewrite Z.lor_spec, Bool.orb_false_iff in H1. destruct H1.
unfold unknown in H1. rewrite Z.lor_spec, Bool.orb_false_iff in H1.
destruct H1. rewrite Hx, Hy by auto. auto.
Qed.

Lemma zcmp_eq_spec i j : Zcmp Ceq i j = eqb true (i =? j).
Proof.
simpl. rewrite Z.eqb_compare.
generalize (Zcompare_elim (i = j) (i < j) (i > j) i j id id id).
destruct (i ?= j); intuition.
Qed.

Lemma zcmp_ne_spec i j : Zcmp Cne i j = eqb false (i =? j).
Proof.
simpl. rewrite Z.eqb_compare.
generalize (Zcompare_elim (i = j) (i < j) (i > j) i j id id id).
destruct (i ?= j); intuition.
Qed.

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).
Proof.
unfold zc_cmp_eq.
intros I J.
destruct x as [[xr] [[|x']]];
destruct y as [[yr] [[|y']]];
try apply congr_0_eq in I;
try apply congr_0_eq in J;
simpl in *; subst.
- generalize (Z.eqb_spec xr yr). intros. rewrite Zfasteqb_Zeqb. apply zc_bool_sound.
- fastunwrap. pose proof divide_ok (xr-yr) (N.pos y').
destruct divide. apply top_correct.
destruct (Z.eqb_spec xr j). 2:apply zc_bool_sound. subst.
cut (false = true). discriminate.
apply H. destruct J as [q J]. simpl in J. exists (-q). simpl. Psatz.lia.
- fastunwrap. pose proof divide_ok (xr-yr) (N.pos x').
destruct divide. apply top_correct.
destruct (Z.eqb_spec i yr). 2:apply zc_bool_sound. subst.
cut (false = true). discriminate.
apply H. destruct I as [q I]. simpl in I. exists q. simpl. Psatz.lia.
- apply top_correct.
Qed.

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).
Proof.
intros I J.
destruct c; auto.
rewrite zcmp_eq_spec. apply zc_cmp_eq_sound; auto.
rewrite zcmp_ne_spec. apply zc_cmp_eq_sound; auto.
apply top_correct. apply top_correct. apply top_correct. apply top_correct.
Qed.

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).
Proof.
intros. unfold extern_top. fastunwrap.
destruct (N.eqb_spec ab.(zc_mod) 1); easy.
Qed.

Lemma intern_top_correct_id:
∀ (ab:zcongr+⊤) (x:Z), INz x ∈ γ ab -> x ∈ γ (intern_top ab).
Proof.
intros. destruct ab. apply top_correct. auto. Qed.

Lemma zc_forward_unop_sound op i a :
γ a i → ∀ n, eval_iunop op i n → γ (zc_forward_unop op a) n.
Proof.
destruct op; intros H n K; try (simpl; now auto); inv K.
- (* neg *) destruct a. auto. apply zc_neg_sound, H.
- (* not *)
replace (Z.lnot i0) with (- 1 - i0). unfold zc_forward_unop.
apply extern_top_correct_id.
apply zc_add_sound with (plus:=Zfastsub) (i:=-1), intern_top_correct_id, H.
apply congr_minus_compat. exists 0. auto.
unfold Z.lnot. omega.
Qed.

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.
Proof.
destruct op; intros i x X j y Y a H; unfold γ; simpl; auto; try apply top_correct;
inv H; try apply extern_top_correct_id;
apply intern_top_correct_id in X; apply intern_top_correct_id in Y.
apply zc_add_sound with (plus:=Zfastsub); auto. apply congr_minus_compat.
apply zc_mul_sound; auto.
eapply @botbind_spec with (A':=Z), zc_quot_sound; eauto.
intros. apply extern_top_correct_id, H.
apply zc_remainder_sound; auto.
apply zc_forward_and_sound; auto.
apply zc_forward_or_sound; auto.
apply zc_forward_xor_sound; auto.
apply zc_shl_sound; auto.
apply zc_shr_sound; auto.
pose proof zc_cmp_sound c _ _ _ _ X Y.
destruct Zcmp; apply extern_top_correct_id, H.
Qed.

∀ i a, γ a i
∀ j b, γ b j
∀ res, γ res (i+j) ->
γ (zc_backward_add res a b) (INz i, INz j).
Proof.
intros. split; simpl.
replace i with ((i+j)-j) by ring.
apply extern_top_correct_id, zc_add_sound with (plus:=Zfastsub); auto.
apply congr_minus_compat.
replace j with ((i+j)-i) by ring.
apply extern_top_correct_id, zc_add_sound with (plus:=Zfastsub); auto.
apply congr_minus_compat.
Qed.

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).
Proof.
intros. split; simpl.
replace i with ((i-j)+j) by ring.
apply congr_plus_compat.
replace j with (i-(i-j)) by ring.
apply extern_top_correct_id, zc_add_sound with (plus:=Zfastsub); auto.
apply congr_minus_compat.
Qed.

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).
Proof.
intros. split. 2:easy. simpl. apply extern_top_correct_id.
unfold zc_gamma. simpl.
set (m:=Nfastgcd (zc_mod res) (Nfastgcd (zc_mod b) (Zfastabs (zc_rem b)))).
fastunwrap.
destruct a as [[ar] [am]], b as [[br] [bm]], res as [[resr] [resm]], H, H1, H2.
simpl in *.
assert (m | i - Z.rem i j).
{ subst m br ar. fastunwrap.
rewrite !Ngcd_is_Zgcd, N2Z.inj_abs_N, Z.gcd_abs_r, Z.rem_eq,
eapply Z.divide_trans, Z.divide_mul_l. apply Zgcd_divides_r.
assert (j=j+x0*bm - x0*bm) by ring.
rewrite H at 2.
apply Z.divide_sub_r. apply Zgcd_divides_r. apply Z.divide_mul_r, Zgcd_divides_l. }
assert (m | Z.rem i j - resr).
{ subst m resr. fastunwrap. rewrite !Ngcd_is_Zgcd, N2Z.inj_abs_N, Z.gcd_abs_r.
apply Zdivide_opp_r, Z.divide_mul_r, Zgcd_divides_l. }
eapply Z.divide_add_r in H4. 2:apply H3.
replace (i - Z.rem i j + (Z.rem i j - resr)) with (i - resr) in H4 by ring.
destruct H4, m as [[]].
- simpl in H4. assert (i = resr) by omega. subst i. exists 0. simpl. omega.
- simpl. rewrite Z.mod_eq by easy. exists (- x2 - (resr/N.pos p)).
fastunwrap. Psatz.lia.
Qed.

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).
Proof.
unfold zc_bw_cmp. destruct res as [[res_rem] [[]]]; simpl. 2:split; apply extern_top_correct_id; auto.
intro RES.
assert (Zcmp c i j = negb (Zfasteqb res_rem F0)).
{ destruct RES. simpl in H1. fastunwrap. simpl. rewrite Z.mul_0_r, Z.add_0_r in H1.
destruct (Z.eqb_spec res_rem 0), Zcmp; subst; auto. discriminate. }
clear RES.
destruct c, Zfasteqb; (try now (split; apply extern_top_correct_id; auto));
simpl in H1; destruct (Z.compare_spec i j); try discriminate; subst;
(apply botbind_spec with j; [split; apply extern_top_correct_id; eauto|apply meet_correct; auto]).
Qed.

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.
Proof.
intros i x Hx0 j y Hy0 res Hres0.
assert (Hx:=congr_testbit _ _ _ Hx0).
assert (Hy:=congr_testbit _ _ _ Hy0).
assert (Hres:=congr_testbit _ _ _ Hres0).
unfold zc_backward_and_l. fastunwrap.
set (maskx := Z.lor (Z.of_N x.(zc_mod)) (-Z.of_N x.(zc_mod))) in *.
set (masky := Z.lor (Z.of_N y.(zc_mod)) (-Z.of_N y.(zc_mod))) in *.
set (maskres := Z.lor (Z.of_N res.(zc_mod)) (-Z.of_N res.(zc_mod))) in *.
set (unknown0res := Z.lor (Z.lor (zc_rem res) (Z.lnot (zc_rem y))) (Z.lor masky maskres)).
set (unknown0 := Z.land unknown0res (Z.lor maskx (zc_rem x))).
set (unknown1res := Z.lor (Z.lnot (zc_rem res)) maskres).
set (unknown1 := Z.land unknown1res (Z.lor maskx (Z.lnot (zc_rem x)))).
set (unknown := Z.land unknown0 unknown1).
assert (∀ n, 0 <= n -> Z.testbit unknown0 n = false -> Z.testbit i n = false).
{ intros. subst unknown0 unknown0res.
rewrite Z.land_spec, !Z.lor_spec, Z.lnot_spec, Bool.andb_false_iff, !Bool.orb_false_iff in H0 by omega.
destruct H0 as [[[] []]|[]].
- rewrite <- Hres, Z.land_spec, Bool.andb_false_iff, Hy in H0 by auto.
destruct H0. auto. rewrite H0 in H1. discriminate.
- rewrite <- Hx in H1 by auto. auto. }
assert (∀ n, 0 <= n -> Z.testbit unknown1 n = false -> Z.testbit i n = true).
{ intros. subst unknown1 unknown1res.
rewrite Z.land_spec, !Z.lor_spec, !Z.lnot_spec, Bool.andb_false_iff, !Bool.orb_false_iff in H1 by omega.
destruct H1 as [[]|[]].
- rewrite <- Hres, Z.land_spec, Bool.negb_false_iff in H1 by auto.
destruct (Z.testbit i n). auto. discriminate.
- rewrite <- Hx in H2 by auto.
destruct (Z.testbit i n). auto. discriminate. }
assert (Z.lor unknown0 unknown1 = -1).
{ apply Z.bits_inj'. intros.
rewrite Z.lor_spec, Int.Ztestbit_m1 by auto.
apply not_false_is_true. rewrite Bool.orb_false_iff. intro. destruct H2.
apply H in H2. apply H0 in H3. congruence. auto. auto. }
rewrite H1, Z.eqb_refl.
set (modu := Z.lor unknown (-unknown)).
assert (modu <= 0).
{ unfold modu. destruct (lor_opp unknown) as [|[k Hk]]. rewrite H2. compute. discriminate.
rewrite Hk. apply Z.opp_nonpos_nonneg, Z.pow_nonneg. omega. }
red. red. red. red. unfold zc_rem, zc_mod. fastunwrap.
rewrite N2Z.inj_abs_N, Z.abs_neq by auto. apply testbit_congr.
replace (-1 - modu) with (Z.lnot modu) by (unfold Z.lnot; omega).
intros. unfold modu.
rewrite !Z.land_spec, !Z.lnot_spec, H4 by auto.
rewrite Z.lor_spec, Bool.orb_false_iff in H4.
unfold unknown in H4. destruct H4.
rewrite Z.land_spec, Bool.andb_false_iff in H4. destruct H4.
- rewrite H, H4 by auto. auto.
- rewrite H0, H4 by auto.
apply (f_equal (fun n => Z.testbit n i0)) in H1.
rewrite Z.lor_spec, Int.Ztestbit_m1, Bool.orb_true_iff in H1 by auto.
destruct H1. rewrite H1. auto. congruence.
Qed.

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.
Proof.
intros i x Hx0 j y Hy0 res Hres0.
assert (Hx:=congr_testbit _ _ _ Hx0).
assert (Hy:=congr_testbit _ _ _ Hy0).
assert (Hres:=congr_testbit _ _ _ Hres0).
unfold zc_backward_or_l. fastunwrap.
set (maskx := Z.lor (Z.of_N x.(zc_mod)) (-Z.of_N x.(zc_mod))) in *.
set (masky := Z.lor (Z.of_N y.(zc_mod)) (-Z.of_N y.(zc_mod))) in *.
set (maskres := Z.lor (Z.of_N res.(zc_mod)) (-Z.of_N res.(zc_mod))) in *.
set (unknown1res := Z.lor (Z.lor (Z.lnot (zc_rem res)) (zc_rem y)) (Z.lor masky maskres)).
set (unknown1 := Z.land unknown1res (Z.lor maskx (Z.lnot (zc_rem x)))).
set (unknown0res := Z.lor (zc_rem res) maskres).
set (unknown0 := Z.land unknown0res (Z.lor maskx (zc_rem x))).
set (unknown := Z.land unknown0 unknown1).
assert (∀ n, 0 <= n -> Z.testbit unknown1 n = false -> Z.testbit i n = true).
{ intros. subst unknown1 unknown1res.
rewrite Z.land_spec, !Z.lor_spec, !Z.lnot_spec, Bool.andb_false_iff, !Bool.orb_false_iff in H0 by omega.
destruct H0 as [[[] []]|[]].
- rewrite <- Hres, Z.lor_spec, negb_false_iff, Bool.orb_true_iff, Hy in H0 by auto.
destruct H0. auto. rewrite H0 in H1. discriminate.
- rewrite <- Hx in H1 by auto. apply negb_false_iff. auto. }
assert (∀ n, 0 <= n -> Z.testbit unknown0 n = false -> Z.testbit i n = false).
{ intros. subst unknown0 unknown0res.
rewrite Z.land_spec, !Z.lor_spec, Bool.andb_false_iff, !Bool.orb_false_iff in H1 by omega.
destruct H1 as [[]|[]].
- rewrite <- Hres, Z.lor_spec in H1 by auto.
destruct (Z.testbit i n). discriminate. auto.
- rewrite <- Hx in H2 by auto. auto. }
assert (Z.lor unknown0 unknown1 = -1).
{ apply Z.bits_inj'. intros.
rewrite Z.lor_spec, Int.Ztestbit_m1 by auto.
apply not_false_is_true. rewrite Bool.orb_false_iff. intro. destruct H2.
apply H0 in H2. apply H in H3. congruence. auto. auto. }
rewrite H1, Z.eqb_refl.
set (modu := Z.lor unknown (-unknown)).
assert (modu <= 0).
{ unfold modu. destruct (lor_opp unknown) as [|[k Hk]]. rewrite H2. compute. discriminate.
rewrite Hk. apply Z.opp_nonpos_nonneg, Z.pow_nonneg. omega. }
red. red. red. red. unfold zc_rem, zc_mod. fastunwrap.
rewrite N2Z.inj_abs_N, Z.abs_neq by auto. apply testbit_congr.
replace (-1 - modu) with (Z.lnot modu) by (unfold Z.lnot; omega).
intros. unfold modu.
rewrite !Z.land_spec, !Z.lnot_spec, H4 by auto.
rewrite Z.lor_spec, Bool.orb_false_iff in H4.
unfold unknown in H4. destruct H4.
rewrite Z.land_spec, Bool.andb_false_iff in H4. destruct H4.
- rewrite H0, H4 by auto. auto.
- rewrite H, H4 by auto.
apply (f_equal (fun n => Z.testbit n i0)) in H1.
rewrite Z.lor_spec, Int.Ztestbit_m1, Bool.orb_true_iff in H1 by auto.
destruct H1. rewrite H1. auto. congruence.
Qed.

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).
Proof.
intros i x X j y Y n res RES H. inv H.
- eapply zc_backward_add_sound; auto using intern_top_correct_id.
- apply zc_backward_sub_sound; auto using intern_top_correct_id.
- split; apply top_correct.
- split; apply top_correct.
- apply zc_backward_mod_sound; auto using intern_top_correct_id.
- eapply botbind_spec with i1, zc_backward_and_l_sound; eauto using intern_top_correct_id.
intros. eapply botbind_spec with i2, zc_backward_and_l_sound; eauto using intern_top_correct_id.
intros. split; apply extern_top_correct_id; auto.
rewrite Z.land_comm. auto.
- eapply botbind_spec with i1, zc_backward_or_l_sound; eauto using intern_top_correct_id.
intros. eapply botbind_spec with i2, zc_backward_or_l_sound; eauto using intern_top_correct_id.
intros. split; apply extern_top_correct_id; auto.
rewrite Z.lor_comm. auto.
- split.
+ replace i1 with (Z.lxor (Z.lxor i1 i2) i2). apply extern_top_correct_id, zc_forward_xor_sound; auto using intern_top_correct_id.
rewrite Z.lxor_assoc, Z.lxor_nilpotent. apply Z.lxor_0_r.
+ replace i2 with (Z.lxor (Z.lxor i1 i2) i1). apply extern_top_correct_id, zc_forward_xor_sound; auto using intern_top_correct_id.
rewrite Z.lxor_comm, <- Z.lxor_assoc, Z.lxor_nilpotent. apply Z.lxor_0_l.
- split; apply top_correct.
- split; apply top_correct.
- apply zc_bw_cmp_sound; auto using intern_top_correct_id.
destruct Zcmp; auto.
- split; apply top_correct.
- split; apply top_correct.
- split; apply top_correct.
- split; apply top_correct.
- split; apply top_correct.
Qed.

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) _.
Proof.
split.
- simpl. intro. unfold join, join_top_res. rewrite zc_join_eq. auto.
- simpl. intro. unfold widen, join, join_top_res. rewrite zc_join_eq. auto.
- simpl. intro. unfold leb, zc_leb. fastunwrap. destruct (N.eqb_spec (zc_mod x) 0).
rewrite Z.eqb_refl. auto.
rewrite N.mod_same, Z.sub_diag by auto. auto.
- simpl. intros x y LE [f|z] G. exact G.
revert G. simpl. apply leb_correct; auto.
- intros x y [f|z]. destruct (xy); simpl; now intuition.
simpl. destruct (xy) eqn:?; simpl; auto. intro. apply join_correct in H.
rewrite Heqy0 in H. auto.
- simpl. intros x y [f|z]. destruct (xy); simpl; now intuition.
simpl. intros. apply meet_correct in H. destruct (xy); auto.
- intros x y [f|[z]]. destruct (widen x y); simpl; now intuition.
simpl. destruct (xy) eqn:?; simpl; auto. intro.
eapply or_introl with (B:=γ y z) in H.
apply join_correct in H. rewrite Heqy0 in H. auto.
- destruct n. constructor. exists 0. simpl. ring.
- easy.
- intros. eapply zc_forward_unop_sound; eauto.
- intros. eapply zc_forward_binop_sound; eauto.
- easy.
- intros. destruct res_ab. split; apply top_correct.
simpl backward_binop. eapply zc_backward_binop_sound, H2; auto.
- intros. simpl. auto.
- intros. simpl. eapply botbind_spec, H1, H3; auto. intros.
pose proof get_eq_expr_correct (proj2 H3) x.
destruct @get_eq_expr as [[]|]; try apply H4.
specialize (H5 _ eq_refl). inv H5. eapply H0; eauto. split. auto. apply H3.
- split; intros; try (apply H0; now auto).
eapply botbind_spec, H; eauto. intros. apply meet_correct. split.
apply intern_top_correct_id. destruct z. auto.
eapply get_congr_correct, H1. auto.
eapply linearize_expr_correct, H2. eauto. auto.
- split. apply H2. repeat constructor. auto.
- intros. unfold assign_msgs, zc_ideal_non_rel.
destruct v as [[rem] [[|[]]]]; repeat constructor; auto.
simpl. destructx), H. simpl in H. f_equal. destruct z.
f_equal. simpl in *. omega.
- intros. unfold assume_msgs, zc_ideal_non_rel.
destruct vNew as [[rem] [[|[]]]]; repeat constructor; auto.
simpl. destructx) as [|[]], H0. simpl in H0. f_equal. simpl in *. f_equal. omega.
Qed.

Definition t := @IdealBoxDomain.t zcongr.

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