diff options
author | jadep <jadep@mit.edu> | 2019-03-12 17:00:26 -0400 |
---|---|---|
committer | jadephilipoom <jade.philipoom@gmail.com> | 2019-03-25 06:13:45 -0400 |
commit | 7a7c691aa341a25da3a0082bc72a56c149a08dd8 (patch) | |
tree | cbb54df3019c89b12f521a9adbf96d891723aeaf /src/Fancy/Montgomery256.v | |
parent | 44d7932acb4eb48e0c75497747c5e3bd203afc3d (diff) |
fix montgomery
Diffstat (limited to 'src/Fancy/Montgomery256.v')
-rw-r--r-- | src/Fancy/Montgomery256.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Fancy/Montgomery256.v b/src/Fancy/Montgomery256.v index 078cdd193..2c692fb30 100644 --- a/src/Fancy/Montgomery256.v +++ b/src/Fancy/Montgomery256.v @@ -31,7 +31,7 @@ Module Montgomery256. Lemma montred256_correct : COperationSpecifications.MontgomeryReduction.montred_correct N R R' (expr.Interp (@ident.gen_interp cast_oor) montred256). Proof. - apply montred_correct with (n:=2%nat) (nout:=2%nat) (machine_wordsize:=machine_wordsize) (N':=N'). + apply montred_correct with (n:=2%nat) (machine_wordsize:=machine_wordsize) (N':=N'). { lazy. reflexivity. } { apply montred256_eq. } Qed. @@ -39,10 +39,10 @@ Module Montgomery256. Lemma montred'_correct_specialized R' (R'_correct : Z.equiv_modulo N (R * R') 1) : forall (lo hi : Z), 0 <= lo < R -> 0 <= hi < R -> 0 <= lo + R * hi < R * N -> - MontgomeryReduction.montred' N R N' (Z.log2 R) 2 2 lo hi = ((lo + R * hi) * R') mod N. + MontgomeryReduction.montred' N R N' (Z.log2 R) lo hi = ((lo + R * hi) * R') mod N. Proof. intros. - apply MontgomeryReduction.montred'_correct with (T:=lo + R * hi) (R':=R'); + apply MontgomeryReduction.montred'_correct with (T:=lo + R * hi) (R':=R') (n:=2%nat); try match goal with | |- context[R'] => assumption | |- context [lo] => |