From f1ef056a7a153931c7f05c126742d941d0908d25 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 25 Apr 2016 23:04:13 -0400 Subject: consolidate and rename Edwards curve lemmas --- src/Specific/Ed25519.v | 54 ++++++++++++++------------------------------------ 1 file changed, 15 insertions(+), 39 deletions(-) (limited to 'src/Specific') diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index f02c24ffb..f8fb5aad7 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -87,33 +87,9 @@ Axiom decode_scalar : word b -> option N. Local Existing Instance Ed25519.FlEncoding. Axiom decode_scalar_correct : forall x, decode_scalar x = option_map (fun x : F (Z.of_nat Ed25519.l) => Z.to_N x) (dec x). -Local Infix "==?" := point_eqb (at level 70) : E_scope. +Local Infix "==?" := E.point_eqb (at level 70) : E_scope. Local Infix "==?" := ModularArithmeticTheorems.F_eq_dec (at level 70) : F_scope. -Program Definition negate (P:point) : point := let '(x, y) := proj1_sig P in (opp x, y). -Next Obligation. -Proof. - pose (proj2_sig P) as H; rewrite <-Heq_anonymous in H; simpl in H. - rewrite F_square_opp; trivial. -Qed. - -Definition point_sub P Q := (P + negate Q)%E. -Infix "-" := point_sub : E_scope. - -Lemma negate_zero : negate zero = zero. -Proof. - pose proof @F_opp_0. - unfold negate, zero; eapply point_eq'; congruence. -Qed. - -Lemma negate_add : forall P Q, negate (P + Q)%E = (negate P + negate Q)%E. Admitted. - -Lemma negate_scalarMult : forall n P, negate (scalarMult n P) = scalarMult n (negate P). -Proof. - pose proof negate_add; pose proof negate_zero. - induction n; simpl; intros; congruence. -Qed. - Axiom solve_for_R : forall A B C, (A ==? B + C)%E = (B ==? A - C)%E. Local Notation "'(' X ',' Y ',' Z ',' T ')'" := (mkExtended X Y Z T). @@ -127,13 +103,13 @@ Proof. repeat rewrite ?F_div_opp_1, ?F_mul_opp_l, ?F_square_opp; trivial. Admitted. -Axiom negateExtended_correct : forall P, negate (unExtendedPoint P) = unExtendedPoint (negateExtended P). +Axiom negateExtended_correct : forall P, E.opp (unExtendedPoint P) = unExtendedPoint (negateExtended P). Local Existing Instance PointEncoding. -Axiom decode_point_eq : forall (P_ Q_ : word (S (b-1))) (P Q:point), dec P_ = Some P -> dec Q_ = Some Q -> weqb P_ Q_ = (P ==? Q)%E. +Axiom decode_point_eq : forall (P_ Q_ : word (S (b-1))) (P Q:E.point), dec P_ = Some P -> dec Q_ = Some Q -> weqb P_ Q_ = (P ==? Q)%E. -Lemma decode_test_encode_test : forall S_ X, option_rect (fun _ : option point => bool) - (fun S : point => (S ==? X)%E) false (dec S_) = weqb S_ (enc X). +Lemma decode_test_encode_test : forall S_ X, option_rect (fun _ : option E.point => bool) + (fun S : E.point => (S ==? X)%E) false (dec S_) = weqb S_ (enc X). Proof. intros. destruct (dec S_) eqn:H. @@ -146,13 +122,13 @@ Qed. Definition enc' : F q * F q -> word (S (b - 1)). Proof. intro x. - let enc' := (eval hnf in (@enc (@point curve25519params) _ _)) in + let enc' := (eval hnf in (@enc (@E.point curve25519params) _ _)) in match (eval cbv [proj1_sig] in (fun pf => enc' (exist _ x pf))) with | (fun _ => ?enc') => exact enc' end. Defined. -Definition enc'_correct : @enc (@point curve25519params) _ _ = (fun x => enc' (proj1_sig x)) +Definition enc'_correct : @enc (@E.point curve25519params) _ _ = (fun x => enc' (proj1_sig x)) := eq_refl. Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x := let y := x in f y. @@ -276,13 +252,13 @@ Proof. [ reflexivity | .. ] end. set_evars. - rewrite<- point_eqb_correct. - rewrite solve_for_R; unfold point_sub. - rewrite negate_scalarMult. + rewrite<- E.point_eqb_correct. + rewrite solve_for_R; unfold E.sub. + rewrite E.opp_mul. let p1 := constr:(scalarMultM1_rep eq_refl) in let p2 := constr:(unifiedAddM1_rep eq_refl) in repeat match goal with - | |- context [(_ * negate ?P)%E] => + | |- context [(_ * E.opp ?P)%E] => rewrite <-(unExtendedPoint_mkExtendedPoint P); rewrite negateExtended_correct; rewrite <-p1 @@ -336,7 +312,7 @@ Proof. reflexivity. } Unfocus. - cbv [mkExtendedPoint zero mkPoint]. + cbv [mkExtendedPoint E.zero]. unfold proj1_sig at 1 2 3 5 6 7 8. rewrite B_proj. @@ -369,7 +345,7 @@ Proof. reflexivity. } Unfocus. - cbv iota beta delta [point_dec_coordinates sign_bit dec FqEncoding modular_word_encoding CompleteEdwardsCurveTheorems.solve_for_x2 sqrt_mod_q]. + cbv iota beta delta [point_dec_coordinates sign_bit dec FqEncoding modular_word_encoding E.solve_for_x2 sqrt_mod_q]. etransitivity. Focus 2. { @@ -484,8 +460,8 @@ Proof. unfold curve25519params, q. (* TODO: do we really wanna do it here? *) rewrite (rep2F_F2rep 0%F). rewrite (rep2F_F2rep 1%F). - match goal with |- context [?x] => match x with (fst (proj1_sig B)) => idtac x; rewrite (rep2F_F2rep x) end end. - match goal with |- context [?x] => match x with (snd (proj1_sig B)) => idtac x; rewrite (rep2F_F2rep x) end end. + match goal with |- context [?x] => match x with (fst (proj1_sig B)) => rewrite (rep2F_F2rep x) end end. + match goal with |- context [?x] => match x with (snd (proj1_sig B)) => rewrite (rep2F_F2rep x) end end. rewrite !FRepMul_correct. repeat match goal with |- appcontext [ ?E ] => match E with (rep2F ?x, rep2F ?y, rep2F ?z, rep2F ?t) => -- cgit v1.2.3