Implemented subtraction mod q as as (sub a b = sub (add a (2*q)) b) to avoid unsigned integer underflow. Also changed rep in Specific proofs so that it is PseudoMersenneBaseRep.rep rather than ModularBaseSystem.rep; these are equivalent but the first is the abstraction level we want.

6 files changed, 116 insertions, 22 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v
index 2bfcdcf0b..f294591eb 100644
--- a/src/ModularArithmetic/ModularBaseSystem.v
+++ b/src/ModularArithmetic/ModularBaseSystem.v
@@ -25,6 +25,9 @@ Section PseudoMersenneBase.
 
   Definition mul (us vs : digits) := reduce (BaseSystem.mul ext_base us vs).
 
+  Definition sub (xs : digits) (xs_0_mod : (BaseSystem.decode base xs) mod modulus = 0) (us vs : digits) :=
+      BaseSystem.sub (add xs us) vs.
+
 End PseudoMersenneBase.
 
 Section CarryBasePow2.
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v
index f93534a99..981680b4a 100644
--- a/src/ModularArithmetic/ModularBaseSystemOpt.v
+++ b/src/ModularArithmetic/ModularBaseSystemOpt.v
@@ -71,6 +71,13 @@ Ltac construct_params prime_modulus len k :=
   | abstract apply prime_modulus
   | abstract brute_force_indices lw].
 
+Definition construct_mul2modulus {m} (prm : PseudoMersenneBaseParams m) : digits :=  
+  match limb_widths with
+  | nil => nil
+  | x :: tail =>
+      2 ^ (x + 1) - (2 * c) :: map (fun w => 2 ^ (w + 1) - 2) tail
+  end.
+
 Ltac subst_precondition := match goal with
   | [H : ?P, H' : ?P -> _ |- _] => specialize (H' H); clear H
 end.
@@ -81,13 +88,13 @@ Ltac kill_precondition H :=
 
 Ltac compute_formula :=
   match goal with
-  | [H : _ -> _ -> rep _ ?result |- rep _ ?result] => kill_precondition H; compute_formula
-  | [H : _ -> rep _ ?result |- rep _ ?result] => kill_precondition H; compute_formula
-  | [H : @rep ?M ?P _ ?result |- @rep ?M ?P _ ?result] =>
+  | [H : _ -> _ -> PseudoMersenneBaseRep.rep _ ?result |- PseudoMersenneBaseRep.rep _ ?result] => kill_precondition H; compute_formula
+  | [H : _ -> PseudoMersenneBaseRep.rep _ ?result |- PseudoMersenneBaseRep.rep _ ?result] => kill_precondition H; compute_formula
+  | [H : @PseudoMersenneBaseRep.rep ?M ?P _ ?result |- @PseudoMersenneBaseRep.rep ?M ?P _ ?result] =>
     let m := fresh "m" in set (m := M) in H at 1; change M with m at 1;
     let p := fresh "p" in set (p := P) in H at 1; change P with p at 1;
     let r := fresh "r" in set (r := result) in H |- *;
-    cbv -[m p r rep] in H;
+    cbv -[m p r PseudoMersenneBaseRep.rep] in H;
     repeat rewrite ?Z.mul_1_r, ?Z.add_0_l, ?Z.add_assoc, ?Z.mul_assoc in H;
     exact H
   end.
@@ -230,7 +237,7 @@ Section Carries.
 End Carries.
 
 Section Addition.
-  Context `{prm : PseudoMersenneBaseParams}.
+  Context `{prm : PseudoMersenneBaseParams} {sc : SubtractionCoefficient modulus prm}.
 
   Definition add_opt_sig (us vs : T) : { b : digits | b = add us vs }.
   Proof.
@@ -246,18 +253,48 @@ Section Addition.
     : add_opt us vs = add us vs
     := proj2_sig (add_opt_sig us vs).
 
-  Lemma add_opt_rep:
-    forall (u v : T) (x y : F modulus), rep u x -> rep v y -> rep (add_opt u v) (x + y)%F.
+  Lemma add_opt_rep: forall (u v : T) (x y : F modulus),
+    PseudoMersenneBaseRep.rep u x -> PseudoMersenneBaseRep.rep v y ->
+    PseudoMersenneBaseRep.rep (add_opt u v) (x + y)%F.
   Proof.
     intros.
     rewrite add_opt_correct.
-    auto using add_rep.
+    auto using PseudoMersenneBaseRep.add_rep.
   Qed.
 
 End Addition.
 
+Section Subtraction.
+  Context `{prm : PseudoMersenneBaseParams} {sc : SubtractionCoefficient modulus prm}.
+
+  Definition sub_opt_sig (us vs : T) : { b : digits | b = sub coeff coeff_mod us vs }.
+  Proof.
+    eexists.
+    cbv [BaseSystem.add ModularBaseSystem.sub BaseSystem.sub].
+    reflexivity.
+  Defined.
+
+  Definition sub_opt (us vs : T) : digits
+    := Eval cbv [proj1_sig sub_opt_sig] in proj1_sig (sub_opt_sig us vs).
+
+  Definition sub_opt_correct us vs
+    : sub_opt us vs = sub coeff coeff_mod us vs
+    := proj2_sig (sub_opt_sig us vs).
+
+  Lemma sub_opt_rep: forall (u v : T) (x y : F modulus),
+    PseudoMersenneBaseRep.rep u x -> PseudoMersenneBaseRep.rep v y ->
+    PseudoMersenneBaseRep.rep (sub_opt u v) (x - y)%F.
+  Proof.
+    intros.
+    rewrite sub_opt_correct.
+    change (sub coeff coeff_mod) with PseudoMersenneBaseRep.sub.
+    apply PseudoMersenneBaseRep.sub_rep; auto using coeff_length.
+  Qed.
+
+End Subtraction.
+
 Section Multiplication.
-  Context `{prm : PseudoMersenneBaseParams}
+  Context `{prm : PseudoMersenneBaseParams} {sc : SubtractionCoefficient modulus prm}
     (* allows caller to precompute k and c *)
     (k_ c_ : Z) (k_subst : k = k_) (c_subst : c = c_).
   Definition mul_bi'_step
@@ -397,11 +434,13 @@ Section Multiplication.
     := proj2_sig (mul_opt_sig us vs).
 
   Lemma mul_opt_rep:
-    forall (u v : T) (x y : F modulus), rep u x -> rep v y -> rep (mul_opt u v) (x * y)%F.
+    forall (u v : T) (x y : F modulus), PseudoMersenneBaseRep.rep u x -> PseudoMersenneBaseRep.rep v y ->
+    PseudoMersenneBaseRep.rep (mul_opt u v) (x * y)%F.
   Proof.
     intros.
     rewrite mul_opt_correct.
-    auto using mul_rep.
+    change mul with PseudoMersenneBaseRep.mul.
+    auto using PseudoMersenneBaseRep.mul_rep.
   Qed.
 
   Definition carry_mul_opt 
@@ -412,13 +451,13 @@ Section Multiplication.
 
   Lemma carry_mul_opt_correct
     : forall (is : list nat) (us vs : list Z) (x  y: F modulus),
-      rep us x -> rep vs y ->
+      PseudoMersenneBaseRep.rep us x -> PseudoMersenneBaseRep.rep vs y ->
       (forall i : nat, In i is -> i < length base)%nat ->
       length (mul_opt us vs) = length base ->
-      rep (carry_mul_opt is us vs) (x*y)%F.
+      PseudoMersenneBaseRep.rep (carry_mul_opt is us vs) (x*y)%F.
   Proof.
     intros is us vs x y; intros.
     change (carry_mul_opt _ _ _) with (carry_sequence_opt_cps c_ is (mul_opt us vs)).
     apply carry_sequence_opt_cps_rep, mul_opt_rep; auto.
   Qed.
-End Multiplication.
+End Multiplication.
\ No newline at end of file
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index 2989bfa12..d9f1bd393 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -48,15 +48,20 @@ Section PseudoMersenneProofs.
     subst; auto.
   Qed.
 
-  Lemma sub_rep : forall u v x y, u ~= x -> v ~= y -> BaseSystem.sub u v ~= (x-y)%F.
+  Lemma sub_rep : forall c c_0modq, (length c <= length base)%nat ->
+    forall u v x y, u ~= x -> v ~= y -> 
+    ModularBaseSystem.sub c c_0modq u v ~= (x-y)%F.
   Proof.
-    autounfold; intuition. {
+    autounfold; unfold ModularBaseSystem.sub; intuition. {
       rewrite sub_length_le_max.
+      case_max; try rewrite Max.max_r; try omega.
+      rewrite add_length_le_max.
       case_max; try rewrite Max.max_r; omega.
     }
     unfold decode in *; unfold BaseSystem.decode in *.
-    rewrite sub_rep.
-    rewrite ZToField_sub.
+    rewrite BaseSystemProofs.sub_rep, BaseSystemProofs.add_rep.
+    rewrite ZToField_sub, ZToField_add, ZToField_mod.
+    rewrite c_0modq, F_add_0_l.
     subst; auto.
   Qed.
 
diff --git a/src/ModularArithmetic/PseudoMersenneBaseRep.v b/src/ModularArithmetic/PseudoMersenneBaseRep.v
index 2cc12b933..c16cc8d38 100644
--- a/src/ModularArithmetic/PseudoMersenneBaseRep.v
+++ b/src/ModularArithmetic/PseudoMersenneBaseRep.v
@@ -23,7 +23,14 @@ Class RepZMod (modulus : Z) := {
   mul_rep : forall u v x y, rep u x -> rep v y -> rep (mul u v) (x*y)%F
 }.
 
-Instance PseudoMersenneBase m (prm : PseudoMersenneBaseParams m) : RepZMod m := {
+Class SubtractionCoefficient (m : Z) (prm : PseudoMersenneBaseParams m) := {
+  coeff : BaseSystem.digits;
+  coeff_length : (length coeff <= length PseudoMersenneBaseParamProofs.base)%nat;
+  coeff_mod: (BaseSystem.decode PseudoMersenneBaseParamProofs.base coeff) mod m = 0
+}.
+
+Instance PseudoMersenneBase m (prm : PseudoMersenneBaseParams m) (sc : SubtractionCoefficient m prm)
+: RepZMod m := {
   T := list Z;
   encode := ModularBaseSystem.encode;
   decode := ModularBaseSystem.decode;
@@ -35,8 +42,8 @@ Instance PseudoMersenneBase m (prm : PseudoMersenneBaseParams m) : RepZMod m :=
   add := BaseSystem.add;
   add_rep := ModularBaseSystemProofs.add_rep;
 
-  sub := BaseSystem.sub;
-  sub_rep := ModularBaseSystemProofs.sub_rep;
+  sub := ModularBaseSystem.sub coeff coeff_mod;
+  sub_rep := ModularBaseSystemProofs.sub_rep coeff coeff_mod coeff_length;
 
   mul := ModularBaseSystem.mul;
   mul_rep := ModularBaseSystemProofs.mul_rep
diff --git a/src/Specific/GF1305.v b/src/Specific/GF1305.v
index 9d11cf8e1..b004a60d1 100644
--- a/src/Specific/GF1305.v
+++ b/src/Specific/GF1305.v
@@ -2,6 +2,7 @@ Require Import Crypto.ModularArithmetic.ModularBaseSystem.
 Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt.
 Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
 Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs.
+Require Import Crypto.ModularArithmetic.PseudoMersenneBaseRep.
 Require Import Coq.Lists.List Crypto.Util.ListUtil.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
 Require Import Crypto.Tactics.VerdiTactics.
@@ -19,6 +20,12 @@ Instance params1305 : PseudoMersenneBaseParams modulus.
   construct_params prime_modulus 5%nat 130.
 Defined.
 
+Definition mul2modulus := Eval compute in (construct_mul2modulus params1305).
+
+Instance subCoeff : SubtractionCoefficient modulus params1305.
+  apply Build_SubtractionCoefficient with (coeff := mul2modulus); cbv; auto.
+Defined.
+
 (* END PseudoMersenneBaseParams instance construction. *)
 
 (* Precompute k and c *)
@@ -38,7 +45,7 @@ Lemma GF1305Base26_mul_reduce_formula :
                       -> rep ls (f*g)%F}.
 Proof.
   eexists; intros ? ? Hf Hg.
-  pose proof (carry_mul_opt_correct k_ c_ (eq_refl k_) (eq_refl c_) [0;4;3;2;1;0]_ _ _ _ Hf Hg) as Hfg.
+  pose proof (carry_mul_opt_correct k_ c_ (eq_refl k) (eq_refl c_) [0;4;3;2;1;0]_ _ _ _ Hf Hg) as Hfg.
   compute_formula.
 Defined.
 
@@ -51,4 +58,17 @@ Proof.
   eexists; intros ? ? Hf Hg.
   pose proof (add_opt_rep _ _ _ _ Hf Hg) as Hfg.
   compute_formula.
+Defined.
+
+Lemma GF25519Base25Point5_sub_formula :
+  forall f0 f1 f2 f3 f4 f5 f6 f7 f8 f9
+    g0 g1 g2 g3 g4 g5 g6 g7 g8 g9,
+    {ls | forall f g, rep [f0;f1;f2;f3;f4;f5;f6;f7;f8;f9] f
+                   -> rep [g0;g1;g2;g3;g4;g5;g6;g7;g8;g9] g
+                   -> rep ls (f - g)%F}.
+Proof.
+  eexists.
+  intros f g Hf Hg.
+  pose proof (sub_opt_rep _ _ _ _ Hf Hg) as Hfg.
+  compute_formula.
 Defined.
\ No newline at end of file
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index 1f6be80cc..b01e6280e 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -2,6 +2,7 @@ Require Import Crypto.ModularArithmetic.ModularBaseSystem.
 Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt.
 Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
 Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs.
+Require Import Crypto.ModularArithmetic.PseudoMersenneBaseRep.
 Require Import Coq.Lists.List Crypto.Util.ListUtil.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
 Require Import Crypto.Tactics.VerdiTactics.
@@ -19,6 +20,12 @@ Instance params25519 : PseudoMersenneBaseParams modulus.
   construct_params prime_modulus 10%nat 255.
 Defined.
 
+Definition mul2modulus := Eval compute in (construct_mul2modulus params25519).
+
+Instance subCoeff : SubtractionCoefficient modulus params25519.
+  apply Build_SubtractionCoefficient with (coeff := mul2modulus); cbv; auto.
+Defined.
+
 (* END PseudoMersenneBaseParams instance construction. *)
 
 (* Precompute k and c *)
@@ -61,4 +68,17 @@ Proof.
   intros f g Hf Hg.
   pose proof (add_opt_rep _ _ _ _ Hf Hg) as Hfg.
   compute_formula.
+Defined.
+
+Lemma GF25519Base25Point5_sub_formula :
+  forall f0 f1 f2 f3 f4 f5 f6 f7 f8 f9
+    g0 g1 g2 g3 g4 g5 g6 g7 g8 g9,
+    {ls | forall f g, rep [f0;f1;f2;f3;f4;f5;f6;f7;f8;f9] f
+                   -> rep [g0;g1;g2;g3;g4;g5;g6;g7;g8;g9] g
+                   -> rep ls (f - g)%F}.
+Proof.
+  eexists.
+  intros f g Hf Hg.
+  pose proof (sub_opt_rep _ _ _ _ Hf Hg) as Hfg.
+  compute_formula.
 Defined.
\ No newline at end of file