From a1f9d9ee2c662790b43bf56df58121a390efbe7c Mon Sep 17 00:00:00 2001 From: jadep Date: Fri, 15 Feb 2019 14:41:47 -0500 Subject: start adapting Montgomery to new glue code --- src/COperationSpecifications.v | 36 ++++++++++-------------------------- 1 file changed, 10 insertions(+), 26 deletions(-) (limited to 'src/COperationSpecifications.v') diff --git a/src/COperationSpecifications.v b/src/COperationSpecifications.v index e8ae7d11e..96e17a4b0 100644 --- a/src/COperationSpecifications.v +++ b/src/COperationSpecifications.v @@ -562,21 +562,9 @@ Module WordByWordMontgomery. End __. End WordByWordMontgomery. -(* Module BarrettReduction. Section __. - (** TODO(jadep, from jgross): Remove any of these not needed to state the spec *) - Context (k M muLow : Z) - (n nout : nat) - (k_bound : 2 <= k) - (M_pos : 0 < M) - (muLow_eq : muLow + 2 ^ k = 2 ^ (2 * k) / M) - (muLow_bounds : 0 <= muLow < 2 ^ k) - (M_bound1 : 2 ^ (k - 1) < M < 2 ^ k) - (M_bound2 : 2 * (2 ^ (2 * k) mod M) <= 2 ^ (k + 1) - (muLow + 2 ^ k)) - (Hn_nz : n <> 0%nat) - (n_le_k : Z.of_nat n <= k) - (Hnout : nout = 2%nat). + Context (k M : Z). Definition barrett_red_correct (barrett_red : Z -> Z -> Z) @@ -589,18 +577,14 @@ End BarrettReduction. Module MontgomeryReduction. Section __. - Context (N R N' R' : Z). + Context (N R R' : Z). Definition montred_correct - Context (T R R' N - Lemma montred'_correct lo_hi T (HT_range: 0 <= T < R * N) - (Hlo: fst lo_hi = T mod R) (Hhi: snd lo_hi = T / R): montred' lo_hi = (T * R') mod N. - Proof. - erewrite montred'_eq by eauto. - apply Z.equiv_modulo_mod_small; auto using reduce_via_partial_correct. - replace 0 with (Z.min 0 (R-N)) by (apply Z.min_l; omega). - apply reduce_via_partial_in_range; omega. - Qed. - - End MontgomeryReduction. -*) + (mont_red : Z -> Z -> Z) + := forall lo hi, + 0 <= lo < R + -> 0 <= hi < R + -> 0 <= lo + R * hi < R * N + -> mont_red lo hi = ((lo + R * hi) * R') mod N. + End __. +End MontgomeryReduction. -- cgit v1.2.3