diff options
author | jadep <jade.philipoom@gmail.com> | 2016-06-17 23:49:41 -0400 |
---|---|---|
committer | jadep <jade.philipoom@gmail.com> | 2016-06-17 23:49:41 -0400 |
commit | d81a299db761650b6c9405cd19335cb54ea0b2ad (patch) | |
tree | aa2e1e05ae07ceb5f928e62e6877b236ea25b1a2 /src/Specific | |
parent | 1f36ebc229080fb8edd8f7903cc0466395cbdd43 (diff) |
Canonicalization is now automated in GF25519 and added to GF1305.
Diffstat (limited to 'src/Specific')
-rw-r--r-- | src/Specific/GF1305.v | 37 | ||||
-rw-r--r-- | src/Specific/GF25519.v | 54 |
2 files changed, 41 insertions, 50 deletions
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). |