Add nonzero synthesis

2 files changed, 13 insertions, 1 deletions

diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v
index 3959fb4f5..d1221d006 100644
--- a/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v
+++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v
@@ -97,6 +97,10 @@ Section WordByWordMontgomery.
     := sub_cps zero A rest.
   Definition opp (A : T R_numlimbs) : T R_numlimbs
     := opp_cps A id.
+  Definition nonzero_cps (A : T R_numlimbs) {cpsT} (f : Z -> cpsT) : cpsT
+    := @nonzero_cps R_numlimbs A cpsT f.
+  Definition nonzero (A : T R_numlimbs) : Z
+    := nonzero_cps A id.
 End WordByWordMontgomery.
 
-Hint Opaque redc pre_redc redc_body redc_loop add sub opp : uncps.
+Hint Opaque redc pre_redc redc_body redc_loop add sub opp nonzero : uncps.
diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v
index a053e8106..f36f55a0f 100644
--- a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v
+++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v
@@ -316,6 +316,14 @@ Section WordByWordMontgomery.
     Lemma eval_opp_mod_N : eval opp mod eval N = (-eval Av) mod eval N.
     Proof. t. Qed.
   End add_sub.
+
+  Section nonzero.
+    Lemma nonzero_cps_id Av {cpsT} f : @nonzero_cps R_numlimbs Av cpsT f = f (@nonzero R_numlimbs Av).
+    Proof. unfold nonzero, nonzero_cps; autorewrite with uncps; reflexivity. Qed.
+
+    Lemma eval_nonzero Av : small Av -> @nonzero R_numlimbs Av = 0 <-> eval Av = 0.
+    Proof. apply eval_nonzero. Qed.
+  End nonzero.
 End WordByWordMontgomery.
 
 Hint Rewrite redc_body_cps_id redc_loop_cps_id pre_redc_cps_id redc_cps_id add_cps_id sub_cps_id opp_cps_id : uncps.