From 4a2c65e57a107545654c2ae815efd734ca7d8321 Mon Sep 17 00:00:00 2001 From: jadep Date: Wed, 15 Jun 2016 18:00:35 -0400 Subject: PseudoMersenneBaseRep.mul now carries by default (made possible by strictly base-length digit vectors) --- src/Specific/GF1305.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Specific/GF1305.v') diff --git a/src/Specific/GF1305.v b/src/Specific/GF1305.v index b004a60d1..31dee21f3 100644 --- a/src/Specific/GF1305.v +++ b/src/Specific/GF1305.v @@ -45,7 +45,7 @@ Lemma GF1305Base26_mul_reduce_formula : -> rep ls (f*g)%F}. Proof. eexists; intros ? ? Hf Hg. - pose proof (carry_mul_opt_correct k_ c_ (eq_refl k) (eq_refl c_) [0;4;3;2;1;0]_ _ _ _ Hf Hg) as Hfg. + pose proof (carry_mul_opt_rep k_ c_ (eq_refl k) (eq_refl c_) _ _ _ _ Hf Hg) as Hfg. compute_formula. Defined. -- cgit v1.2.3 From d81a299db761650b6c9405cd19335cb54ea0b2ad Mon Sep 17 00:00:00 2001 From: jadep Date: Fri, 17 Jun 2016 23:49:41 -0400 Subject: Canonicalization is now automated in GF25519 and added to GF1305. --- src/ModularArithmetic/ModularBaseSystemOpt.v | 92 +++++++++++----------------- src/Specific/GF1305.v | 37 ++++++++--- src/Specific/GF25519.v | 54 ++++------------ 3 files changed, 76 insertions(+), 107 deletions(-) (limited to 'src/Specific/GF1305.v') diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index 8ac8c95c5..c0e942ece 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -30,6 +30,9 @@ Definition map_opt {A B} := Eval compute in @map A B. Definition full_carry_chain_opt := Eval compute in @full_carry_chain. Definition length_opt := Eval compute in length. Definition base_opt := Eval compute in @base. +Definition max_ones_opt := Eval compute in @max_ones. +Definition max_bound_opt := Eval compute in @max_bound. +Definition minus_opt := Eval compute in minus. Definition Let_In {A P} (x : A) (f : forall y : A, P y) := let y := x in f y. @@ -80,6 +83,10 @@ Definition construct_mul2modulus {m} (prm : PseudoMersenneBaseParams m) : digits 2 ^ (x + 1) - (2 * c) :: map (fun w => 2 ^ (w + 1) - 2) tail end. +Ltac compute_preconditions := + cbv; intros; repeat match goal with H : _ \/ _ |- _ => + destruct H; subst; [ congruence | ] end; (congruence || omega). + Ltac subst_precondition := match goal with | [H : ?P, H' : ?P -> _ |- _] => specialize (H' H); clear H end. @@ -97,8 +104,7 @@ Ltac compute_formula := let p := fresh "p" in set (p := P) in H at 1; change P with p at 1; let r := fresh "r" in set (r := result) in H |- *; cbv -[m p r PseudoMersenneBaseRep.rep] in H; - repeat rewrite ?Z.mul_1_r, ?Z.add_0_l, ?Z.add_assoc, ?Z.mul_assoc in H; - exact H + repeat rewrite ?Z.mul_1_r, ?Z.add_0_l, ?Z.add_assoc, ?Z.mul_assoc in H end. Section Carries. @@ -181,7 +187,7 @@ Section Carries. change (LHS = Let_In (nth_default_opt 0%Z b i) RHSf). change Z.shiftl with Z_shiftl_opt. change (-1) with (Z_opp_opt 1). - change Z.add with Z_add_opt at 8 12 20 24. + change Z.add with Z_add_opt at 5 9 17 21. reflexivity. Defined. @@ -536,62 +542,31 @@ Section Multiplication. End Multiplication. +Record freezePreconditions {modulus} (prm : PseudoMersenneBaseParams modulus) 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)))) < max_bound 0 + 1; + c_reduce2 : c <= max_bound 0 - c; + two_pow_k_le_2modulus : 2 ^ k <= 2 * modulus +}. +Local Hint Resolve lt_1_length_base int_width_pos int_width_compat c_pos + c_reduce1 c_reduce2 two_pow_k_le_2modulus. + Section Canonicalization. Context `{prm : PseudoMersenneBaseParams} {sc : SubtractionCoefficient modulus prm} (* allows caller to precompute k and c *) (k_ c_ : Z) (k_subst : k = k_) (c_subst : c = c_) - (lt_1_length_base : (1 < length base)%nat) - {int_width} (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)))) < max_bound 0 + 1) - (c_reduce2 : c <= max_bound 0 - c) - (two_pow_k_le_2modulus : 2 ^ k <= 2 * modulus). - - Definition max_ones_opt := Eval compute in max_ones. - Definition max_bound_opt := Eval compute in max_bound. - Definition minus_opt := Eval compute in minus. - - Definition isFull'_opt_sig (us : T) full i : - { b : bool | b = isFull' us full i }. - Proof. - eexists. - cbv [isFull']. - change max_bound with max_bound_opt. - rewrite c_subst. - change Z.sub with Z_sub_opt. - reflexivity. - Defined. - - Definition isFull'_opt (us : T) full i: bool - := Eval cbv [proj1_sig isFull'_opt_sig] in proj1_sig (isFull'_opt_sig us full i). - - Definition isFull'_opt_correct us full i: isFull'_opt us full i = isFull' us full i := - proj2_sig (isFull'_opt_sig us full i). - - Definition and_term_opt_sig (us : list Z) : { b : Z | b = and_term us }. - Proof. - eexists. - cbv [and_term isFull]. - change length with length_opt. - rewrite <-isFull'_opt_correct. - change max_ones with max_ones_opt. - change @base with base_opt. - change minus with minus_opt. - reflexivity. - Defined. - - Definition and_term_opt (us : digits) : Z - := Eval cbv [proj1_sig and_term_opt_sig] in proj1_sig (and_term_opt_sig us). - - Definition and_term_opt_correct us : and_term_opt us = and_term us := - proj2_sig (and_term_opt_sig us). + {int_width} (preconditions : freezePreconditions prm int_width). Definition modulus_digits_opt_sig : { b : digits | b = modulus_digits }. Proof. eexists. cbv beta iota delta [modulus_digits modulus_digits' app]. - change max_bound with max_bound_opt. + change @max_bound with max_bound_opt. rewrite c_subst. change length with length_opt. change minus with minus_opt. @@ -646,13 +621,14 @@ Section Canonicalization. rewrite <-carry_full_3_opt_cps_correct with (f := RHSf). cbv beta iota delta [and_term isFull isFull']. change length with length_opt. - change max_bound with max_bound_opt. + change @max_bound with max_bound_opt. rewrite c_subst. - change max_ones with max_ones_opt. + change @max_ones with max_ones_opt. change @base with base_opt. change minus with minus_opt. - rewrite <-modulus_digits_opt_correct. change @map with @map_opt. + change Z.sub with Z_sub_opt at 1. + rewrite <-modulus_digits_opt_correct. reflexivity. Defined. @@ -664,20 +640,23 @@ Section Canonicalization. := proj2_sig (freeze_opt_sig us). Lemma freeze_opt_canonical: forall us vs x, - @pre_carry_bounds _ _ int_width us -> rep us x -> - @pre_carry_bounds _ _ int_width vs -> rep vs x -> + @pre_carry_bounds _ _ int_width us -> PseudoMersenneBaseRep.rep us x -> + @pre_carry_bounds _ _ int_width vs -> PseudoMersenneBaseRep.rep vs x -> freeze_opt us = freeze_opt vs. Proof. intros. rewrite !freeze_opt_correct. + change PseudoMersenneBaseRep.rep with rep in *. eapply freeze_canonical with (B := int_width); eauto. Qed. - Lemma freeze_opt_preserves_rep : forall us x, rep us x -> rep (freeze_opt us) x. + Lemma freeze_opt_preserves_rep : forall us x, PseudoMersenneBaseRep.rep us x -> + PseudoMersenneBaseRep.rep (freeze_opt us) x. Proof. intros. rewrite freeze_opt_correct. - eauto using freeze_preserves_rep. + change PseudoMersenneBaseRep.rep with rep in *. + eapply freeze_preserves_rep; eauto. Qed. Lemma freeze_opt_spec : forall us vs x, rep us x -> rep vs x -> @@ -686,7 +665,6 @@ Section Canonicalization. (PseudoMersenneBaseRep.rep (freeze_opt us) x /\ freeze_opt us = freeze_opt vs). Proof. split; eauto using freeze_opt_canonical. - change PseudoMersenneBaseRep.rep with rep. auto using freeze_opt_preserves_rep. Qed. diff --git a/src/Specific/GF1305.v b/src/Specific/GF1305.v index 31dee21f3..02ef714d9 100644 --- a/src/Specific/GF1305.v +++ b/src/Specific/GF1305.v @@ -15,6 +15,7 @@ Local Open Scope Z. Definition modulus : Z := 2^130 - 5. Lemma prime_modulus : prime modulus. Admitted. +Definition int_width := 32%Z. Instance params1305 : PseudoMersenneBaseParams modulus. construct_params prime_modulus 5%nat 130. @@ -26,16 +27,22 @@ Instance subCoeff : SubtractionCoefficient modulus params1305. apply Build_SubtractionCoefficient with (coeff := mul2modulus); cbv; auto. Defined. +Definition freezePreconditions1305 : freezePreconditions params1305 int_width. +Proof. + constructor; compute_preconditions. +Defined. + (* END PseudoMersenneBaseParams instance construction. *) (* Precompute k and c *) Definition k_ := Eval compute in k. Definition c_ := Eval compute in c. +Definition c_subst : c = c_ := eq_refl c_. (* Makes Qed not take forever *) Opaque Z.shiftr Pos.iter Z.div2 Pos.div2 Pos.div2_up Pos.succ Z.land Z.of_N Pos.land N.ldiff Pos.pred_N Pos.pred_double Z.opp Z.mul Pos.mul - Let_In digits Z.add Pos.add Z.pos_sub. + Let_In digits Z.add Pos.add Z.pos_sub andb Z.eqb Z.ltb. Local Open Scope nat_scope. Lemma GF1305Base26_mul_reduce_formula : @@ -45,8 +52,9 @@ Lemma GF1305Base26_mul_reduce_formula : -> rep ls (f*g)%F}. Proof. eexists; intros ? ? Hf Hg. - pose proof (carry_mul_opt_rep k_ c_ (eq_refl k) (eq_refl c_) _ _ _ _ Hf Hg) as Hfg. + pose proof (carry_mul_opt_rep k_ c_ (eq_refl k) c_subst _ _ _ _ Hf Hg) as Hfg. compute_formula. + exact Hfg. Defined. Lemma GF1305Base26_add_formula : @@ -58,17 +66,30 @@ Proof. eexists; intros ? ? Hf Hg. pose proof (add_opt_rep _ _ _ _ Hf Hg) as Hfg. compute_formula. + exact Hfg. Defined. -Lemma GF25519Base25Point5_sub_formula : - forall f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 - g0 g1 g2 g3 g4 g5 g6 g7 g8 g9, - {ls | forall f g, rep [f0;f1;f2;f3;f4;f5;f6;f7;f8;f9] f - -> rep [g0;g1;g2;g3;g4;g5;g6;g7;g8;g9] g +Lemma GF1305Base26_sub_formula : + forall f0 f1 f2 f3 f4 g0 g1 g2 g3 g4, + {ls | forall f g, rep [f0;f1;f2;f3;f4] f + -> rep [g0;g1;g2;g3;g4] g -> rep ls (f - g)%F}. Proof. eexists. intros f g Hf Hg. pose proof (sub_opt_rep _ _ _ _ Hf Hg) as Hfg. compute_formula. -Defined. \ No newline at end of file + exact Hfg. +Defined. + +Lemma GF1305Base26_freeze_formula : + forall f0 f1 f2 f3 f4, + {ls | forall x, rep [f0;f1;f2;f3;f4] x + -> rep ls x}. +Proof. + eexists. + intros x Hf. + pose proof (freeze_opt_preserves_rep _ c_subst freezePreconditions1305 _ _ Hf) as Hfreeze_rep. + compute_formula. + exact Hfreeze_rep. +Defined. diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 2ec338625..8ee9b25d8 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -16,6 +16,7 @@ Local Open Scope Z. Definition modulus : Z := 2^255 - 19. Lemma prime_modulus : prime modulus. Admitted. +Definition int_width := 32%Z. Instance params25519 : PseudoMersenneBaseParams modulus. construct_params prime_modulus 10%nat 255. @@ -27,31 +28,18 @@ Instance subCoeff : SubtractionCoefficient modulus params25519. apply Build_SubtractionCoefficient with (coeff := mul2modulus); cbv; auto. Defined. +Definition freezePreconditions25519 : freezePreconditions params25519 int_width. +Proof. + constructor; compute_preconditions. +Defined. + (* END PseudoMersenneBaseParams instance construction. *) (* Precompute k and c *) Definition k_ := Eval compute in k. Definition c_ := Eval compute in c. -Definition base_ := Eval compute in base. -Definition limb_widths_ := Eval compute in limb_widths. - Definition c_subst : c = c_ := eq_refl c_. -Lemma c_reduce1 : (c * Z.ones (32 - log_cap (pred (length base))) < max_bound 0 + 1)%Z. -Proof. - cbv; congruence. -Qed. - -Lemma c_reduce2 : c <= max_bound 0 - c. -Proof. - cbv; congruence. -Qed. - -Lemma two_pow_k_le_2modulus : (2 ^ k <= 2 * modulus)%Z. -Proof. - cbv; congruence. -Qed. - (* Makes Qed not take forever *) Opaque Z.shiftr Pos.iter Z.div2 Pos.div2 Pos.div2_up Pos.succ Z.land Z.of_N Pos.land N.ldiff Pos.pred_N Pos.pred_double Z.opp Z.mul Pos.mul @@ -68,6 +56,7 @@ Proof. eexists; intros ? ? Hf Hg. pose proof (carry_mul_opt_rep k_ c_ (eq_refl k_) c_subst _ _ _ _ Hf Hg) as Hfg. compute_formula. + exact Hfg. Time Defined. Extraction "/tmp/test.ml" GF25519Base25Point5_mul_reduce_formula. @@ -88,6 +77,7 @@ Proof. intros f g Hf Hg. pose proof (add_opt_rep _ _ _ _ Hf Hg) as Hfg. compute_formula. + exact Hfg. Defined. Lemma GF25519Base25Point5_sub_formula : @@ -101,6 +91,7 @@ Proof. intros f g Hf Hg. pose proof (sub_opt_rep _ _ _ _ Hf Hg) as Hfg. compute_formula. + exact Hfg. Defined. Lemma GF25519Base25Point5_freeze_formula : @@ -110,35 +101,14 @@ Lemma GF25519Base25Point5_freeze_formula : Proof. eexists. intros x Hf. - assert (1 < length base)%nat as lt_1_length_base by (cbv; repeat constructor). - assert (0 < 32)%Z by omega. - assert (forall w : Z, In w limb_widths -> (w <= 32)%Z) by - (cbv [limb_widths params25519 limb_widths_from_len In]; intros w w_cases; - repeat (destruct w_cases as [ ? | w_cases]; [ subst; omega | ]); exfalso; assumption). - assert (0 < c)%Z by (change c with c_; cbv; congruence). - pose proof c_reduce1. - pose proof c_reduce2. - pose proof two_pow_k_le_2modulus. - pose proof (@freeze_opt_preserves_rep modulus params25519 subCoeff c_ (eq_refl c_) lt_1_length_base 32) as Hfreeze_rep. - repeat match goal with H : ?P, H' : ?P -> _ |- _ => specialize (H' H) end. - specialize (Hfreeze_rep _ _ Hf). - change ModularBaseSystem.rep with rep in Hfreeze_rep. - match goal with H : @rep ?M ?P (?f ?l) ?result |- _ => - let m := fresh "m" in - set (m := M) in H at 1; change M with m in |- * at 1; - (let p := fresh "p" in - set (p := P) in H at 1; change P with p in |- * at 1; - (let r := fresh "r" in - set (r := result) in H |- *)) - end. - cbv [freeze_opt] in Hfreeze_rep. - cbv [carry_full_3_opt_cps] in Hfreeze_rep. - cbv -[m p r rep] in Hfreeze_rep. + pose proof (freeze_opt_preserves_rep _ c_subst freezePreconditions25519 _ _ Hf) as Hfreeze_rep. + compute_formula. exact Hfreeze_rep. Defined. (* Uncomment the below to see pretty-printed freeze function *) (* +Set Printing Depth 1000. Local Transparent Let_In. Infix "<<" := Z.shiftr (at level 50). Infix "&" := Z.land (at level 50). -- cgit v1.2.3