diff options
| -rw-r--r-- | src/Experiments/Ed25519.v | 92 | ||||
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystem.v | 16 | ||||
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemOpt.v | 26 | ||||
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 32 | ||||
| -rw-r--r-- | src/Specific/GF1305.v | 2 | ||||
| -rw-r--r-- | src/Specific/GF25519.v | 6 |
6 files changed, 84 insertions, 90 deletions
diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v index aa5c5c5ca..84b8cb113 100644 --- a/src/Experiments/Ed25519.v +++ b/src/Experiments/Ed25519.v @@ -31,14 +31,6 @@ Definition feSign (f : GF25519BoundedCommon.fe25519) : bool := let '(x9, x8, x7, x6, x5, x4, x3, x2, x1, x0) := (x : GF25519.fe25519) in BinInt.Z.testbit x0 0. -Definition freezePre : - @ModularBaseSystemProofs.FreezePreconditions - GF25519.modulus GF25519.params25519 GF25519.int_width. -Proof. - pose proof GF25519.freezePreconditions25519 as A. - inversion A; econstructor; eauto. -Defined. - Definition a : GF25519BoundedCommon.fe25519 := Eval vm_compute in GF25519BoundedCommon.encode a. Definition d : GF25519BoundedCommon.fe25519 := @@ -399,24 +391,34 @@ Proof. f_equal. Qed. -Lemma nth_default_B_compat : forall i, +Lemma nth_default_freeze_input_bound_compat : forall i, + (nth_default 0 PseudoMersenneBaseParams.limb_widths i < + GF25519.freeze_input_bound)%Z. +Proof. + pose proof GF25519.freezePreconditions25519. + intros. + destruct (lt_dec i (length PseudoMersenneBaseParams.limb_widths)). + { apply ModularBaseSystemProofs.B_compat. + rewrite nth_default_eq. + auto using nth_In. } + { rewrite nth_default_out_of_bounds by omega. + cbv; congruence. } +Qed. +(* +Lemma nth_default_int_width_compat : forall i, (nth_default 0 PseudoMersenneBaseParams.limb_widths i < GF25519.int_width)%Z. Proof. - assert (@ModularBaseSystemProofs.FreezePreconditions - GF25519.modulus GF25519.params25519 - GF25519.int_width) by - (let A := fresh "H" in - pose proof GF25519.freezePreconditions25519 as A; - inversion A; econstructor; eauto). - intros. - destruct (lt_dec i (length PseudoMersenneBaseParams.limb_widths)). - { apply ModularBaseSystemProofs.B_compat. - rewrite nth_default_eq. - auto using nth_In. } - { rewrite nth_default_out_of_bounds by omega. - cbv; congruence. } + pose proof GF25519.freezePreconditions25519. + intros. + destruct (lt_dec i (length PseudoMersenneBaseParams.limb_widths)). + { apply ModularBaseSystemProofs.int_width_compat. + rewrite nth_default_eq. + auto using nth_In. } + { rewrite nth_default_out_of_bounds by omega. + cbv; congruence. } Qed. +*) Lemma minrep_freeze : forall x, Pow2Base.bounded @@ -436,12 +438,7 @@ Lemma minrep_freeze : forall x, (ModularBaseSystem.encode x))) = 0%Z. Proof. - assert (@ModularBaseSystemProofs.FreezePreconditions - GF25519.modulus GF25519.params25519 - GF25519.int_width) - by (let A := fresh "H" in - pose proof GF25519.freezePreconditions25519 as A; - inversion A; econstructor; eauto). + pose proof GF25519.freezePreconditions25519. intros. match goal with |- appcontext [ModularBaseSystem.freeze _ ?x] => @@ -455,15 +452,17 @@ Proof. eapply Z.lt_le_trans; [ solve [intuition eauto] | ]. match goal with |- appcontext [if ?a then _ else _] => destruct a end. { apply Z.pow_le_mono_r; try omega. - apply Z.lt_le_incl, nth_default_B_compat. } - { transitivity (2 ^ (Z.pred GF25519.int_width))%Z. + apply Z.lt_le_incl. + apply nth_default_freeze_input_bound_compat. } + { transitivity (2 ^ (Z.pred GF25519.freeze_input_bound))%Z. { apply Z.pow_le_mono; try omega. - apply Z.lt_le_pred. - apply nth_default_B_compat. } + apply Z.lt_le_pred. + apply nth_default_freeze_input_bound_compat. } { rewrite Z.shiftr_div_pow2 by (auto using Pow2BaseProofs.nth_default_limb_widths_nonneg, PseudoMersenneBaseParamProofs.limb_widths_nonneg). - rewrite <- Z.pow_sub_r by (try omega; split; auto using Pow2BaseProofs.nth_default_limb_widths_nonneg, PseudoMersenneBaseParamProofs.limb_widths_nonneg, Z.lt_le_incl, nth_default_B_compat). - replace (2 ^ GF25519.int_width)%Z - with (2 ^ (Z.pred GF25519.int_width + 1))%Z by (f_equal; omega). + rewrite <- Z.pow_sub_r by (try omega; split; auto using Pow2BaseProofs.nth_default_limb_widths_nonneg, PseudoMersenneBaseParamProofs.limb_widths_nonneg, Z.lt_le_incl, nth_default_freeze_input_bound_compat). + replace (2 ^ GF25519.freeze_input_bound)%Z + with (2 ^ (Z.pred GF25519.freeze_input_bound + 1))%Z + by (f_equal; omega). rewrite Z.pow_add_r by (omega || (cbv; congruence)). rewrite <-Zplus_diag_eq_mult_2. match goal with |- (?a <= ?a + ?b - ?c)%Z => @@ -561,7 +560,7 @@ Proof. { cbv [ZNWord]. do 2 apply f_equal. subst w. - pose proof freezePre. + pose proof GF25519.freezePreconditions25519. match goal with |- appcontext [GF25519.freeze ?x ] => let A := fresh "H" in @@ -625,11 +624,11 @@ Lemma initial_bounds : forall x n, nth_default 0 (Tuple.to_list (length PseudoMersenneBaseParams.limb_widths) (GF25519BoundedCommon.proj1_fe25519 x)) n < - 2 ^ GF25519.int_width - + 2 ^ GF25519.freeze_input_bound - (if eq_nat_dec n 0%nat then 0 else - Z.shiftr (2 ^ GF25519.int_width) + Z.shiftr (2 ^ GF25519.freeze_input_bound) (nth_default 0 PseudoMersenneBaseParams.limb_widths (pred n))))%Z. Proof. @@ -673,7 +672,7 @@ Proof. rewrite !Z.bit0_odd. rewrite <-@Pow2BaseProofs.parity_decode with (limb_widths := PseudoMersenneBaseParams.limb_widths) by (auto using PseudoMersenneBaseParamProofs.limb_widths_nonneg, Tuple.length_to_list; cbv; congruence). - pose proof freezePre. + pose proof GF25519.freezePreconditions25519. match goal with H : _ = GF25519.freeze ?u |- _ => let A := fresh "H" in let B := fresh "H" in pose proof (ModularBaseSystemProofs.freeze_rep u x) as A; @@ -702,14 +701,14 @@ Proof. repeat match goal with |- appcontext[GF25519.freeze ?x] => remember (GF25519.freeze x) end. assert (Tuple.fieldwise (n := 10) eq f f0). - { pose proof freezePre. + { pose proof GF25519.freezePreconditions25519. match goal with H1 : _ = GF25519.freeze ?u, H2 : _ = GF25519.freeze ?v |- _ => let A := fresh "H" in let HP := fresh "H" in let HQ := fresh "H" in pose proof (ModularBaseSystemProofs.freeze_canonical - (freeze_pre := freezePre) u v _ _ eq_refl eq_refl); + (freeze_pre := GF25519.freezePreconditions25519) u v _ _ eq_refl eq_refl); match type of A with ?P -> ?Q -> _ => assert P as HP by apply initial_bounds; assert Q as HQ by apply initial_bounds end; @@ -748,7 +747,7 @@ Qed. Lemma Proper_feEnc : Proper (GF25519BoundedCommon.eq ==> eq) feEnc. Proof. - pose proof freezePre. + pose proof GF25519.freezePreconditions25519. repeat intro; cbv [feEnc]. rewrite !GF25519Bounded.pack_correct, !GF25519Bounded.freeze_correct. rewrite !GF25519.freeze_correct, !ModularBaseSystemOpt.freeze_opt_correct @@ -760,7 +759,8 @@ Proof. let HP := fresh "H" in let HQ := fresh "H" in pose proof (ModularBaseSystemProofs.freeze_canonical - (freeze_pre := freezePre) x y (ModularBaseSystem.decode x) + (freeze_pre := GF25519.freezePreconditions25519) + x y (ModularBaseSystem.decode x) (ModularBaseSystem.decode y) eq_refl eq_refl); match type of A with ?P -> ?Q -> _ => assert P as HP by apply initial_bounds; @@ -1258,14 +1258,14 @@ Qed. Lemma bounded_by_encode_freeze : forall x, ModularBaseSystemProofs.bounded_by (ModularBaseSystem.encode x) - (ModularBaseSystemProofs.freeze_input_bounds (B := GF25519.int_width)). + (ModularBaseSystemProofs.freeze_input_bounds (B := GF25519.freeze_input_bound)). Proof. Admitted. Lemma bounded_by_freeze : forall x, ModularBaseSystemProofs.bounded_by (GF25519BoundedCommon.fe25519WToZ x) - (ModularBaseSystemProofs.freeze_input_bounds (B := GF25519.int_width)). + (ModularBaseSystemProofs.freeze_input_bounds (B := GF25519.freeze_input_bound)). Admitted. Lemma sqrt_correct : forall x : ModularArithmetic.F.F q, @@ -1288,7 +1288,7 @@ Proof. rewrite ModularBaseSystemProofs.encode_rep. symmetry. eapply @ModularBaseSystemProofs.sqrt_5mod8_correct; - eauto using freezePre, ModularBaseSystemProofs.encode_rep, bounded_by_freeze, bounded_by_encode_freeze; + eauto using GF25519.freezePreconditions25519, ModularBaseSystemProofs.encode_rep, bounded_by_freeze, bounded_by_encode_freeze; match goal with | |- appcontext[GF25519Bounded.powW ?a ?ch] => let A := fresh "H" in diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v index 6df49173e..9d7ce7c1f 100644 --- a/src/ModularArithmetic/ModularBaseSystem.v +++ b/src/ModularArithmetic/ModularBaseSystem.v @@ -83,10 +83,10 @@ Section ModularBaseSystem. Definition eq (x y : digits) : Prop := decode x = decode y. - Definition freeze B (x : digits) : digits := - from_list (freeze B [[x]]) (length_freeze length_to_list). + Definition freeze int_width (x : digits) : digits := + from_list (freeze int_width [[x]]) (length_freeze length_to_list). - Definition eqb B (x y : digits) : bool := fieldwiseb Z.eqb (freeze B x) (freeze B y). + Definition eqb int_width (x y : digits) : bool := fieldwiseb Z.eqb (freeze int_width x) (freeze int_width y). (* Note : both of the following square root definitions will produce garbage output if the input is not square mod [modulus]. The caller should either provably only call them with square input, @@ -95,10 +95,10 @@ Section ModularBaseSystem. (chain_correct : fold_chain 0%N N.add chain (1%N :: nil) = Z.to_N (modulus / 4 + 1)) (x : digits) : digits := pow x chain. - Definition sqrt_5mod8 B powx powx_squared (chain : list (nat * nat)) + Definition sqrt_5mod8 int_width powx powx_squared (chain : list (nat * nat)) (chain_correct : fold_chain 0%N N.add chain (1%N :: nil) = Z.to_N (modulus / 8 + 1)) (sqrt_minus1 x : digits) : digits := - if eqb B powx_squared x then powx else mul sqrt_minus1 powx. + if eqb int_width powx_squared x then powx else mul sqrt_minus1 powx. Import Morphisms. Global Instance eq_Equivalence : Equivalence eq. @@ -106,9 +106,9 @@ Section ModularBaseSystem. split; cbv [eq]; repeat intro; congruence. Qed. - Definition select B (b : Z) (x y : digits) := - add (map (Z.land (neg B b)) x) - (map (Z.land (neg B (Z.lxor b 1))) x). + Definition select int_width (b : Z) (x y : digits) := + add (map (Z.land (neg int_width b)) x) + (map (Z.land (neg int_width (Z.lxor b 1))) x). Context {target_widths} (target_widths_nonneg : forall x, In x target_widths -> 0 <= x) (bits_eq : sum_firstn limb_widths (length limb_widths) = diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index d302f83a8..155698e56 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -905,30 +905,15 @@ Section Conversion. End Conversion. -Section with_base. - Context {modulus} (prm : PseudoMersenneBaseParams modulus). - Local Notation base := (Pow2Base.base_from_limb_widths limb_widths). - Local Notation log_cap i := (nth_default 0 limb_widths i). - - Record freezePreconditions int_width := - mkFreezePreconditions { - lt_1_length_base : (1 < length base)%nat; - int_width_pos : 0 < int_width; - int_width_compat : forall w, In w limb_widths -> w < int_width; - c_pos : 0 < c; - c_reduce1 : c * (Z.ones (int_width - log_cap (pred (length base)))) < 2 ^ log_cap 0; - c_reduce2 : c < 2 ^ log_cap 0 - c; - two_pow_k_le_2modulus : 2 ^ k <= 2 * modulus - }. -End with_base. -Local Hint Resolve lt_1_length_base int_width_pos int_width_compat c_pos - c_reduce1 c_reduce2 two_pow_k_le_2modulus. +Local Hint Resolve lt_1_length_limb_widths int_width_pos B_pos B_compat + c_reduce1 c_reduce2. Section Canonicalization. Context `{prm : PseudoMersenneBaseParams} {sc : SubtractionCoefficient} (* allows caller to precompute k and c *) (k_ c_ : Z) (k_subst : k = k_) (c_subst : c = c_) - {int_width} (preconditions : freezePreconditions prm int_width). + {int_width freeze_input_bound} + (preconditions : FreezePreconditions freeze_input_bound int_width). Local Notation digits := (tuple Z (length limb_widths)). Definition carry_full_3_opt_cps_sig @@ -1072,7 +1057,8 @@ Section SquareRoots. Section SquareRoot5mod8. Context {ec : ExponentiationChain (modulus / 8 + 1)}. Context (sqrt_m1 : digits) (sqrt_m1_correct : rep (mul sqrt_m1 sqrt_m1) (F.opp 1%F)). - Context {int_width} (preconditions : freezePreconditions prm int_width). + Context {int_width freeze_input_bound} + (preconditions : FreezePreconditions freeze_input_bound int_width). Definition sqrt_5mod8_opt_sig (powx powx_squared us : digits) : { vs : digits | diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 59a6f33db..197a0dca6 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -521,16 +521,18 @@ End CarryProofs. Hint Rewrite @length_carry_and_reduce @length_carry : distr_length. -Class FreezePreconditions `{prm : PseudoMersenneBaseParams} B := +Class FreezePreconditions `{prm : PseudoMersenneBaseParams} B int_width := { lt_1_length_limb_widths : (1 < length limb_widths)%nat; + int_width_pos : 0 < int_width; + B_le_int_width : B <= int_width; B_pos : 0 < B; B_compat : forall w, In w limb_widths -> w < B; (* on the first reduce step, we add at most one bit of width to the first digit *) c_reduce1 : c * ((2 ^ B) >> nth_default 0 limb_widths (pred (length limb_widths))) <= 2 ^ (nth_default 0 limb_widths 0); (* on the second reduce step, we add at most one bit of width to the first digit, and leave room to carry c one more time after the highest bit is carried *) - c_reduce2 : c <= 2 ^ (nth_default 0 limb_widths 0) - c + c_reduce2 : c <= 2 ^ (nth_default 0 limb_widths 0) - c; }. Section CanonicalizationProofs. @@ -940,8 +942,14 @@ Section CanonicalizationProofs. congruence. Qed. + Lemma int_width_compat : forall x, In x limb_widths -> x < int_width. + Proof. + intros. apply B_compat in H. + eapply Z.lt_le_trans; eauto using B_le_int_width. + Qed. + Lemma minimal_rep_freeze : forall u, initial_bounds u -> - minimal_rep (freeze B u). + minimal_rep (freeze int_width u). Proof. repeat match goal with | |- _ => progress (cbv [freeze ModularBaseSystemList.freeze]) @@ -952,12 +960,12 @@ Section CanonicalizationProofs. | |- _ => apply conditional_subtract_lt_modulus | |- _ => apply conditional_subtract_modulus_preserves_bounded | |- bounded _ (carry_full _) => apply bounded_iff - | |- _ => solve [auto using Z.lt_le_incl, B_pos, B_compat, lt_1_length_limb_widths, length_carry_full, length_to_list] + | |- _ => solve [auto using Z.lt_le_incl, int_width_pos, int_width_compat, lt_1_length_limb_widths, length_carry_full, length_to_list] end. Qed. Lemma freeze_decode : forall u, - BaseSystem.decode base (to_list _ (freeze B u)) mod modulus = + BaseSystem.decode base (to_list _ (freeze int_width u)) mod modulus = BaseSystem.decode base (to_list _ u) mod modulus. Proof. repeat match goal with @@ -967,7 +975,7 @@ Section CanonicalizationProofs. | |- _ => rewrite Z.mod_add by (pose proof prime_modulus; prime_bound) | |- _ => rewrite to_list_from_list | |- _ => rewrite conditional_subtract_modulus_spec by - auto using Z.lt_le_incl, B_pos, B_compat, lt_1_length_limb_widths, length_carry_full, length_to_list, ge_modulus_01 + (auto using Z.lt_le_incl, int_width_pos, int_width_compat, lt_1_length_limb_widths, length_carry_full, length_to_list, ge_modulus_01) end. rewrite !decode_mod_Fdecode by auto using length_carry_full, length_to_list. cbv [carry_full]. @@ -986,7 +994,7 @@ Section CanonicalizationProofs. rewrite from_list_to_list; reflexivity. Qed. - Lemma freeze_rep : forall u x, rep u x -> rep (freeze B u) x. + Lemma freeze_rep : forall u x, rep u x -> rep (freeze int_width u) x. Proof. cbv [rep]; intros. apply F.eq_to_Z_iff. @@ -997,7 +1005,7 @@ Section CanonicalizationProofs. Lemma freeze_canonical : forall u v x y, rep u x -> rep v y -> initial_bounds u -> initial_bounds v -> - (x = y <-> fieldwise Logic.eq (freeze B u) (freeze B v)). + (x = y <-> fieldwise Logic.eq (freeze int_width u) (freeze int_width v)). Proof. intros; apply bounded_canonical; auto using freeze_rep, minimal_rep_freeze. Qed. @@ -1022,7 +1030,7 @@ Section SquareRootProofs. Lemma eqb_true_iff : forall u v x y, bounded_by u freeze_input_bounds -> bounded_by v freeze_input_bounds -> - u ~= x -> v ~= y -> (x = y <-> eqb B u v = true). + u ~= x -> v ~= y -> (x = y <-> eqb int_width u v = true). Proof. cbv [eqb freeze_input_bounds]. intros. rewrite fieldwiseb_fieldwise by (apply Z.eqb_eq). @@ -1031,10 +1039,10 @@ Section SquareRootProofs. Lemma eqb_false_iff : forall u v x y, bounded_by u freeze_input_bounds -> bounded_by v freeze_input_bounds -> - u ~= x -> v ~= y -> (x <> y <-> eqb B u v = false). + u ~= x -> v ~= y -> (x <> y <-> eqb int_width u v = false). Proof. intros. - case_eq (eqb B u v). + case_eq (eqb int_width u v). + rewrite <-eqb_true_iff by eassumption; split; intros; congruence || contradiction. + split; intros; auto. @@ -1069,7 +1077,7 @@ Section SquareRootProofs. bounded_by powx_squared freeze_input_bounds -> ModularBaseSystem.eq powx (pow u chain) -> ModularBaseSystem.eq powx_squared (mul powx powx) -> - (sqrt_5mod8 B powx powx_squared chain chain_correct sqrt_m1 u) ~= F.sqrt_5mod8 (decode sqrt_m1) x. + (sqrt_5mod8 int_width powx powx_squared chain chain_correct sqrt_m1 u) ~= F.sqrt_5mod8 (decode sqrt_m1) x. Proof. cbv [sqrt_5mod8 F.sqrt_5mod8]. intros. diff --git a/src/Specific/GF1305.v b/src/Specific/GF1305.v index 72184cf07..d31a2319f 100644 --- a/src/Specific/GF1305.v +++ b/src/Specific/GF1305.v @@ -44,7 +44,7 @@ Instance carryChain : CarryChain limb_widths. contradiction H. Defined. -Definition freezePreconditions1305 : freezePreconditions params1305 int_width. +Definition freezePreconditions1305 : FreezePreconditions int_width int_width. Proof. constructor; compute_preconditions. Defined. diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 16ce7a545..0a487b1e2 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -22,7 +22,8 @@ Local Open Scope Z. Definition modulus : Z := Eval compute in 2^255 - 19. Lemma prime_modulus : prime modulus. Admitted. -Definition int_width := 32%Z. +Definition int_width := 64%Z. +Definition freeze_input_bound := 32%Z. Instance params25519 : PseudoMersenneBaseParams modulus. construct_params prime_modulus 10%nat 255. @@ -46,7 +47,7 @@ Instance carryChain : CarryChain limb_widths. contradiction H. Defined. -Definition freezePreconditions25519 : freezePreconditions params25519 int_width. +Definition freezePreconditions25519 : FreezePreconditions freeze_input_bound int_width. Proof. constructor; compute_preconditions. Defined. @@ -584,7 +585,6 @@ Proof. exact (proj2_sig (eqb_sig f' g')). Qed. -Print sqrt_5mod8_opt. Definition sqrt_sig (powf powf_squared f : fe25519) : { f' : fe25519 | f' = sqrt_5mod8_opt (int_width := int_width) k_ c_ sqrt_m1 powf powf_squared f}. Proof. |