aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar jadep <jadep@mit.edu>2019-03-12 17:00:26 -0400
committerGravatar jadephilipoom <jade.philipoom@gmail.com>2019-03-25 06:13:45 -0400
commit7a7c691aa341a25da3a0082bc72a56c149a08dd8 (patch)
treecbb54df3019c89b12f521a9adbf96d891723aeaf /src
parent44d7932acb4eb48e0c75497747c5e3bd203afc3d (diff)
fix montgomery
Diffstat (limited to 'src')
-rw-r--r--src/Fancy/Montgomery256.v6
-rw-r--r--src/PushButtonSynthesis/MontgomeryReduction.v22
2 files changed, 11 insertions, 17 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] =>
diff --git a/src/PushButtonSynthesis/MontgomeryReduction.v b/src/PushButtonSynthesis/MontgomeryReduction.v
index a682aa227..73204eb53 100644
--- a/src/PushButtonSynthesis/MontgomeryReduction.v
+++ b/src/PushButtonSynthesis/MontgomeryReduction.v
@@ -42,7 +42,7 @@ Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBU
Local Opaque reified_montred_gen. (* needed for making [autorewrite] not take a very long time *)
Section rmontred.
- Context (N R N' : Z) (n nout : nat)
+ Context (N R N' : Z) (n : nat)
(machine_wordsize : Z).
Let value_range := r[0 ~> (2^machine_wordsize - 1)%Z]%zrange.
@@ -92,14 +92,12 @@ Section rmontred.
((R' =? 0)%Z, Pipeline.No_modular_inverse "R⁻¹ mod N" R N);
(negb ((R * R') mod N =? 1 mod N)%Z, Pipeline.Values_not_provably_equalZ "(R * R') mod N ≠ 1 mod N" ((R * R') mod N) (1 mod N));
(negb ((N * N') mod R =? (-1) mod R)%Z, Pipeline.Values_not_provably_equalZ "(N * N') mod R ≠ (-1) mod R" ((N * N') mod R) ((-1) mod R));
- (negb (nout =? 2)%nat, Pipeline.Values_not_provably_equalZ "nout ≠ 2" (Z.of_nat nout) 2);
- (negb (n =? 2)%nat, Pipeline.Values_not_provably_equalZ "n ≠ 2" (Z.of_nat n) 2);
(negb (2 ^ machine_wordsize =? R)%Z, Pipeline.Values_not_provably_equalZ "2^machine_wordsize ≠ R" (2^machine_wordsize) R);
((negb (0 <? N))%Z, Pipeline.Value_not_ltZ "N ≤ 0" 0 N);
((negb (N <? R))%Z, Pipeline.Value_not_ltZ "R ≤ N" R N);
((negb (0 <=? N'))%Z, Pipeline.Value_not_leZ "N' < 0" 0 N');
((negb (N' <? R))%Z, Pipeline.Value_not_ltZ "R ≤ N'" R N');
- ((negb (Z.of_nat n <=? machine_wordsize))%Z, Pipeline.Value_not_leZ "machine_wordsize < n" (Z.of_nat n) machine_wordsize)].
+ ((negb (2 <=? machine_wordsize))%Z, Pipeline.Value_not_leZ "machine_wordsize < 2" 2 machine_wordsize)].
Local Arguments Z.mul !_ !_.
Local Ltac use_curve_good_t :=
@@ -123,10 +121,8 @@ Section rmontred.
/\ EquivModulo.Z.equiv_modulo R (N * N') (-1)
/\ EquivModulo.Z.equiv_modulo N (R * R') 1
/\ n <> 0%nat
- /\ Z.of_nat n <= machine_wordsize
- /\ 2 ^ machine_wordsize = R
- /\ n = 2%nat
- /\ nout = 2%nat.
+ /\ 2 <= machine_wordsize
+ /\ 2 ^ machine_wordsize = R.
Proof using curve_good.
clear -curve_good.
cbv [check_args fold_right] in curve_good.
@@ -147,8 +143,6 @@ Section rmontred.
{ use_curve_good_t. }
{ use_curve_good_t. }
{ use_curve_good_t. }
- { use_curve_good_t. }
- { use_curve_good_t. }
Qed.
Definition montred
@@ -157,7 +151,7 @@ Section rmontred.
fancy_args (* fancy *)
possible_values
(reified_montred_gen
- @ GallinaReify.Reify N @ GallinaReify.Reify R @ GallinaReify.Reify N' @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify 2%nat @ GallinaReify.Reify 2%nat)
+ @ GallinaReify.Reify N @ GallinaReify.Reify R @ GallinaReify.Reify N' @ GallinaReify.Reify machine_wordsize)
(bound, (bound, tt))
bound.
@@ -178,13 +172,13 @@ Section rmontred.
| progress Z.rewrite_mod_small ].
Local Strategy -100 [montred]. (* needed for making Qed not take forever *)
+ Local Strategy -100 [montred' reified_montred_gen]. (* needed for making prove_correctness not take forever *)
Lemma montred_correct res (Hres : montred = Success res)
: montred_correct N R R' (expr.Interp (@ident.gen_interp cast_oor) res).
- Proof using n nout curve_good.
+ Proof using n curve_good.
cbv [montred_correct]; intros.
- rewrite <- MontgomeryReduction.montred'_correct with (R:=R) (N':=N') (Zlog2R:=machine_wordsize) (n:=n) (nout:=nout) (lo:=lo) (hi:=hi) by solve_montred_preconditions.
+ rewrite <- MontgomeryReduction.montred'_correct with (R:=R) (N':=N') (Zlog2R:=machine_wordsize) (n:=n) (lo:=lo) (hi:=hi) by solve_montred_preconditions.
prove_correctness' ltac:(fun _ => idtac) use_curve_good.
- { congruence. }
{ cbv [ZRange.type.base.option.is_bounded_by ZRange.type.base.is_bounded_by bound is_bounded_by_bool value_range upper lower].
rewrite Bool.andb_true_iff, !Z.leb_le. lia. }
{ cbv [ZRange.type.base.option.is_bounded_by ZRange.type.base.is_bounded_by bound is_bounded_by_bool value_range upper lower].