Make use of new conditional_subtract

4 files changed, 31 insertions, 42 deletions

diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Definition.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Definition.v
index caddbd7c0..b59b6018c 100644
--- a/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Definition.v
+++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Definition.v
@@ -25,7 +25,7 @@ Section WordByWordMontgomery.
     {add : forall {n}, T n -> T n -> T (S n)} (* joins carry *)
     {add' : forall {n}, T (S n) -> T n -> T (S (S n))} (* joins carry *)
     {drop_high : T (S (S R_numlimbs)) -> T (S R_numlimbs)} (* drops the highest limb *)
-    {conditional_subtract : T (S R_numlimbs) -> T R_numlimbs} (* computes [arg - N] if [R <= arg], and drops high bit *)
+    {conditional_sub : T (S R_numlimbs) -> T R_numlimbs} (* computes [arg - N] if [R <= arg], and drops high bit *)
     (N : T R_numlimbs).
 
   (* Recurse for a as many iterations as A has limbs, varying A := A, S := 0, r, bounds *)
@@ -65,7 +65,7 @@ Section WordByWordMontgomery.
       := snd (redc_loop A_numlimbs (A, zero (1 + R_numlimbs))).
 
     Definition redc : T R_numlimbs
-      := conditional_subtract pre_redc.
+      := conditional_sub pre_redc.
   End loop.
 End WordByWordMontgomery.
 
diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v
index 86c72e728..2a9e179a3 100644
--- a/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v
+++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v
@@ -48,9 +48,9 @@ Section WordByWordMontgomery.
     (N : T R_numlimbs) (Npos : positive) (Npos_correct: eval N = Z.pos Npos)
     (small_N : small N)
     (N_lt_R : eval N < R)
-    {conditional_subtract : T (S R_numlimbs) -> T R_numlimbs} (* computes [arg - N] if [N <= arg], and drops high bit *)
-    {eval_conditional_subtract : forall v, small v -> 0 <= eval v < eval N + R -> eval (conditional_subtract v) = eval v + if R <=? eval v then -eval N else 0}
-    {small_conditional_subtract : forall v, small v -> 0 <= eval v < eval N + R -> small (conditional_subtract v)}
+    {conditional_sub : T (S R_numlimbs) -> T R_numlimbs} (* computes [arg - N] if [N <= arg], and drops high bit *)
+    {eval_conditional_sub : forall v, small v -> 0 <= eval v < eval N + R -> eval (conditional_sub v) = eval v + if R <=? eval v then -eval N else 0}
+    {small_conditional_sub : forall v, small v -> 0 <= eval v < eval N + R -> small (conditional_sub v)}
     (B : T R_numlimbs)
     (B_bounds : 0 <= eval B < R)
     (small_B : small B)
@@ -66,7 +66,7 @@ Section WordByWordMontgomery.
                  | apply small_drop_high
                  | apply small_zero
                  | apply small_scmul
-                 | apply small_conditional_subtract
+                 | apply small_conditional_sub
                  | apply Z_mod_lt
                  | rewrite Z.mul_split_mod
                  | progress destruct_head' and
@@ -82,7 +82,7 @@ Section WordByWordMontgomery.
        eval_add'
        eval_scmul
        eval_drop_high
-       eval_conditional_subtract
+       eval_conditional_sub
        using (repeat autounfold with word_by_word_montgomery; t_small)
     : push_eval.
 
@@ -239,7 +239,7 @@ Section WordByWordMontgomery.
   Local Notation redc_body := (@redc_body T (@divmod) r R_numlimbs scmul add add' drop_high N B k).
   Local Notation redc_loop := (@redc_loop T (@divmod) r R_numlimbs scmul add add' drop_high N B k).
   Local Notation pre_redc A := (@pre_redc T zero (@divmod) r R_numlimbs scmul add add' drop_high N _ A B k).
-  Local Notation redc A := (@redc T zero (@divmod) r R_numlimbs scmul add add' drop_high conditional_subtract N _ A B k).
+  Local Notation redc A := (@redc T zero (@divmod) r R_numlimbs scmul add add' drop_high conditional_sub N _ A B k).
 
   Section body.
     Context (pred_A_numlimbs : nat)
@@ -473,7 +473,7 @@ Section WordByWordMontgomery.
     pose proof (@small_pre_redc _ A small_A).
     pose proof (@pre_redc_bound _ A small_A).
     unfold redc.
-    rewrite eval_conditional_subtract by t_small.
+    rewrite eval_conditional_sub by t_small.
     break_innermost_match; Z.ltb_to_lt; omega.
   Qed.
 
@@ -485,7 +485,7 @@ Section WordByWordMontgomery.
     pose proof (@small_pre_redc _ A small_A).
     pose proof (@pre_redc_bound _ A small_A).
     unfold redc.
-    rewrite eval_conditional_subtract by t_small.
+    rewrite eval_conditional_sub by t_small.
     break_innermost_match; Z.ltb_to_lt; try omega.
   Qed.
 
@@ -497,6 +497,6 @@ Section WordByWordMontgomery.
     pose proof (@small_pre_redc _ A small_A).
     pose proof (@pre_redc_bound _ A small_A).
     unfold redc.
-    apply small_conditional_subtract; [ apply small_pre_redc | .. ]; auto; omega.
+    apply small_conditional_sub; [ apply small_pre_redc | .. ]; auto; omega.
   Qed.
 End WordByWordMontgomery.
diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v
index a5aefd821..8335cbb39 100644
--- a/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v
+++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v
@@ -24,12 +24,8 @@ Section WordByWordMontgomery.
   Local Notation scmul := (@scmul (Z.pos r)).
   Local Notation add' := (fun n => @add (Z.pos r) (S n) n (S n)).
   Local Notation add := (fun n => @add (Z.pos r) n n n).
-  (*****************************************************************************************)
-  (** TODO(jadep) FIXME: Fill these in, replacing [Axiom] with [Local Notation] *)
-  Local Notation conditional_subtract_cps := (@drop_high_cps R_numlimbs).
-  (*Axiom conditional_subtract_cps : T (S R_numlimbs) -> forall {cpsT}, (T R_numlimbs -> cpsT) -> cpsT *)(* computes [arg - N] if [R <= arg], and drops high bit *)
-  Axiom conditional_subtract : T (S R_numlimbs) -> T R_numlimbs (* computes [arg - N] if [R <= arg], and drops high bit *).
-  (*****************************************************************************************)
+  Local Notation conditional_sub_cps := (fun V => @conditional_sub_cps (Z.pos r) _ (Z.pos r - 1) V N _).
+  Local Notation conditional_sub := (fun V => @conditional_sub (Z.pos r) _ (Z.pos r - 1) V N).
 
   Definition redc_body_no_cps (B : T R_numlimbs) (k : Z) {pred_A_numlimbs} (A_S : T (S pred_A_numlimbs) * T (S R_numlimbs))
     : T pred_A_numlimbs * T (S R_numlimbs)
@@ -40,7 +36,7 @@ Section WordByWordMontgomery.
   Definition pre_redc_no_cps {A_numlimbs} (A : T A_numlimbs) (B : T R_numlimbs) (k : Z) : T (S R_numlimbs)
     := @pre_redc T (@zero) (@divmod) r R_numlimbs (@scmul) add add' (@drop_high (S R_numlimbs)) N _ A B k.
   Definition redc_no_cps {A_numlimbs} (A : T A_numlimbs) (B : T R_numlimbs) (k : Z) : T R_numlimbs
-    := @redc T (@zero) (@divmod) r R_numlimbs (@scmul) add add' (@drop_high (S R_numlimbs)) conditional_subtract N _ A B k.
+    := @redc T (@zero) (@divmod) r R_numlimbs (@scmul) add add' (@drop_high (S R_numlimbs)) conditional_sub N _ A B k.
 
   Definition redc_body_cps {pred_A_numlimbs} (A : T (S pred_A_numlimbs)) (B : T R_numlimbs) (k : Z) (S' : T (S R_numlimbs))
              {cpsT} (rest : T pred_A_numlimbs * T (S R_numlimbs) -> cpsT)
@@ -65,7 +61,7 @@ Section WordByWordMontgomery.
       := redc_loop_cps A_numlimbs (fun '(A, S') => rest S') (A, zero).
 
     Definition redc_cps (rest : T R_numlimbs -> cpsT) : cpsT
-      := pre_redc_cps (fun v => conditional_subtract_cps v rest).
+      := pre_redc_cps (fun v => conditional_sub_cps v rest).
   End loop.
 
   Definition redc_body {pred_A_numlimbs} (A : T (S pred_A_numlimbs)) (B : T R_numlimbs) (k : Z) (S' : T (S R_numlimbs))
diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v
index 780a5de60..9787f9c34 100644
--- a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v
+++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v
@@ -43,6 +43,7 @@ Section WordByWordMontgomery.
           (small_N : small N)
           (small_B : small B)
           (N_nonzero : eval N <> 0)
+          (N_mask : Tuple.map (Z.land (Z.pos r - 1)) N = N)
           (k_correct : k * eval N mod r = (-1) mod r).
   Let R : positive := match (Z.pos r ^ Z.of_nat R_numlimbs)%Z with
                       | Z.pos R => R
@@ -67,24 +68,16 @@ Section WordByWordMontgomery.
     intros; apply Saturated.small_add; auto; lia.
   Qed.
 
-
-  (*****************************************************************************************)
-  (** TODO(jadep) FIXME: Fill these in, replacing [Axiom] with [Local Notation] *)
-  Local Notation conditional_subtract_cps := (@drop_high_cps R_numlimbs).
-  (*Axiom conditional_subtract_cps : T (S R_numlimbs) -> forall {cpsT}, (T R_numlimbs -> cpsT) -> cpsT *)(* computes [arg - N] if [R <= arg], and drops high bit *)
-  Local Notation conditional_subtract := conditional_subtract.
-  Axiom conditional_subtract_cps_id : forall v cpsT f, @conditional_subtract_cps v cpsT f = f (@conditional_subtract _ v).
-  Axiom eval_conditional_subtract
-    : forall v : T (S R_numlimbs),
-      small v ->
-      0 <= eval v < eval N + Z.pos R ->
-      eval (conditional_subtract v) = eval v + (if Z.pos R <=? eval v then - eval N else 0).
-  Axiom small_conditional_subtract
-    : forall v : T (S R_numlimbs),
-      small v ->
-      0 <= eval v < eval N + Z.pos R ->
-      small (conditional_subtract v).
-  (*****************************************************************************************)
+  Local Notation conditional_sub_cps := (fun V : T (S R_numlimbs) => @conditional_sub_cps (Z.pos r) _ (Z.pos r - 1) V N _).
+  Local Notation conditional_sub := (fun V : T (S R_numlimbs) => @conditional_sub (Z.pos r) _ (Z.pos r - 1) V N).
+  Local Notation eval_conditional_sub' := (fun V small_V V_bound => @eval_conditional_sub (Z.pos r) (Zorder.Zgt_pos_0 _) _ (Z.pos r - 1) V N small_V small_N N_mask V_bound).
+  Local Lemma eval_conditional_sub
+    : forall v, small v -> 0 <= eval v < eval N + R -> eval (conditional_sub v) = eval v + if R <=? eval v then -eval N else 0.
+  Proof. rewrite R_correct; exact eval_conditional_sub'. Qed.
+  Local Notation small_conditional_sub' := (fun V small_V V_bound => @small_conditional_sub (Z.pos r) (Zorder.Zgt_pos_0 _) _ (Z.pos r - 1) V N small_V small_N N_mask V_bound).
+  Local Lemma small_conditional_sub
+    : forall v : T (S R_numlimbs), small v -> 0 <= eval v < eval N + R -> small (conditional_sub v).
+  Proof. rewrite R_correct; exact small_conditional_sub'. Qed.
 
   Local Lemma A_bound : 0 <= eval A < Z.pos r ^ Z.of_nat A_numlimbs.
   Proof. apply eval_small; auto; lia. Qed.
@@ -121,13 +114,13 @@ Section WordByWordMontgomery.
   Local Notation redc := (@redc r R_numlimbs N A_numlimbs A B k).
 
   Definition redc_no_cps_bound : 0 <= eval redc_no_cps < R
-    := @redc_bound T (@eval) (@zero) (@divmod) r r_big R R_numlimbs R_correct (@small) eval_zero small_zero eval_div eval_mod small_div (@scmul) eval_scmul small_scmul (@add) eval_add small_add (@add') eval_add' small_add' drop_high eval_drop_high small_drop_high N Npos Npos_correct small_N N_lt_R conditional_subtract eval_conditional_subtract B B_bound small_B ri k A_numlimbs A small_A A_bound.
+    := @redc_bound T (@eval) (@zero) (@divmod) r r_big R R_numlimbs R_correct (@small) eval_zero small_zero eval_div eval_mod small_div (@scmul) eval_scmul small_scmul (@add) eval_add small_add (@add') eval_add' small_add' drop_high eval_drop_high small_drop_high N Npos Npos_correct small_N N_lt_R conditional_sub eval_conditional_sub B B_bound small_B ri k A_numlimbs A small_A A_bound.
   Definition redc_no_cps_mod_N
     : (eval redc_no_cps) mod (eval N) = (eval A * eval B * ri^(Z.of_nat A_numlimbs)) mod (eval N)
-    := @redc_mod_N T (@eval) (@zero) (@divmod) r r_big R R_numlimbs R_correct (@small) eval_zero small_zero eval_div eval_mod small_div (@scmul) eval_scmul small_scmul (@add) eval_add small_add (@add') eval_add' small_add' drop_high eval_drop_high small_drop_high N Npos Npos_correct small_N N_lt_R conditional_subtract eval_conditional_subtract B B_bound small_B ri ri_correct k k_correct A_numlimbs A small_A A_bound.
+    := @redc_mod_N T (@eval) (@zero) (@divmod) r r_big R R_numlimbs R_correct (@small) eval_zero small_zero eval_div eval_mod small_div (@scmul) eval_scmul small_scmul (@add) eval_add small_add (@add') eval_add' small_add' drop_high eval_drop_high small_drop_high N Npos Npos_correct small_N N_lt_R conditional_sub eval_conditional_sub B B_bound small_B ri ri_correct k k_correct A_numlimbs A small_A A_bound.
   Definition small_redc_no_cps
     : small redc_no_cps
-    := @small_redc T (@eval) (@zero) (@divmod) r r_big R R_numlimbs R_correct (@small) eval_zero small_zero eval_div eval_mod small_div (@scmul) eval_scmul small_scmul (@add) eval_add small_add (@add') eval_add' small_add' drop_high eval_drop_high small_drop_high N Npos Npos_correct small_N N_lt_R conditional_subtract small_conditional_subtract B B_bound small_B ri k A_numlimbs A small_A A_bound.
+    := @small_redc T (@eval) (@zero) (@divmod) r r_big R R_numlimbs R_correct (@small) eval_zero small_zero eval_div eval_mod small_div (@scmul) eval_scmul small_scmul (@add) eval_add small_add (@add') eval_add' small_add' drop_high eval_drop_high small_drop_high N Npos Npos_correct small_N N_lt_R conditional_sub small_conditional_sub B B_bound small_B ri k A_numlimbs A small_A A_bound.
 
   Lemma redc_body_cps_id pred_A_numlimbs (A' : T (S pred_A_numlimbs)) (S' : T (S R_numlimbs)) {cpsT} f
     : @redc_body_cps pred_A_numlimbs A' B k S' cpsT f = f (redc_body A' B k S').
@@ -158,7 +151,7 @@ Section WordByWordMontgomery.
   Proof.
     unfold redc, redc_cps.
     etransitivity; rewrite pre_redc_cps_id; [ | reflexivity ];
-      rewrite ?conditional_subtract_cps_id;
+      autorewrite with uncps;
       reflexivity.
   Qed.
 
@@ -193,7 +186,7 @@ Section WordByWordMontgomery.
   Proof.
     unfold redc, redc_no_cps, redc_cps, Abstract.Dependent.Definition.redc.
     rewrite pre_redc_cps_id, pre_redc_cps_id_no_cps.
-    rewrite conditional_subtract_cps_id; reflexivity.
+    autorewrite with uncps; reflexivity.
   Qed.
 
   Lemma redc_bound : 0 <= eval redc < R.