From 7a7c691aa341a25da3a0082bc72a56c149a08dd8 Mon Sep 17 00:00:00 2001 From: jadep Date: Tue, 12 Mar 2019 17:00:26 -0400 Subject: fix montgomery --- src/Fancy/Montgomery256.v | 6 +++--- src/PushButtonSynthesis/MontgomeryReduction.v | 22 ++++++++-------------- 2 files changed, 11 insertions(+), 17 deletions(-) (limited to 'src') 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 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]. -- cgit v1.2.3