Merge and refactor of GF25519

3 files changed, 6 insertions, 7 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index 7efccbade..0a7070922 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -94,7 +94,9 @@ Section PseudoMersenneProofs.
     replace (2^k) with ((2^k - c) + c) by ring.
     rewrite Z.mul_add_distr_r.
     rewrite Zplus_mod.
-    rewrite <- modulus_pseudomersenne.
+    unfold c.
+    rewrite Z.sub_sub_distr, Z.sub_diag.
+    simpl.
     rewrite Z.mul_comm.
     rewrite mod_mult_plus; auto using modulus_nonzero.
     rewrite <- Zplus_mod; auto.
@@ -379,7 +381,7 @@ Section CarryProofs.
       rewrite Z.mul_comm.
       rewrite Z.mul_assoc.
       rewrite <- Z.pow_add_r by (apply log_cap_nonneg || apply sum_firstn_limb_widths_nonneg).
-      rewrite <- k_matches_limb_widths.
+      unfold k.
       replace (length limb_widths) with (S (pred (length base))) by
         (subst; rewrite <- base_length; apply NPeano.Nat.succ_pred; omega).
       rewrite sum_firstn_succ with (x:= log_cap (pred (length base))) by
diff --git a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
index 93e6bc1f0..0a58c81d2 100644
--- a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
+++ b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
@@ -121,7 +121,6 @@ Section PseudoMersenneBaseParamProofs.
 
   Lemma k_nonneg : 0 <= k.
   Proof.
-    rewrite <- k_matches_limb_widths.
     apply sum_firstn_limb_widths_nonneg.
   Qed.
 
diff --git a/src/ModularArithmetic/PseudoMersenneBaseParams.v b/src/ModularArithmetic/PseudoMersenneBaseParams.v
index 09f4bc68e..3914d6219 100644
--- a/src/ModularArithmetic/PseudoMersenneBaseParams.v
+++ b/src/ModularArithmetic/PseudoMersenneBaseParams.v
@@ -12,11 +12,9 @@ Class PseudoMersenneBaseParams (modulus : Z) := {
   limb_widths_good : forall i j, (i + j < length limb_widths)%nat ->
     sum_firstn limb_widths (i + j) <=
     sum_firstn limb_widths i + sum_firstn limb_widths j;
-  k : Z;
-  c : Z;
-  k_matches_limb_widths : sum_firstn limb_widths (length limb_widths) = k;
-  modulus_pseudomersenne : modulus = 2^k - c;
   prime_modulus : Znumtheory.prime modulus;
+  k := sum_firstn limb_widths (length limb_widths);
+  c := 2 ^ k - modulus;
   limb_widths_match_modulus : forall i j,
     (i < length limb_widths)%nat ->
     (j < length limb_widths)%nat ->