diff options
author | Andres Erbsen <andreser@mit.edu> | 2016-10-27 10:12:54 -0400 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2016-11-04 00:27:28 -0400 |
commit | 6498b3808c81eeb19f5b1b3a3c8797c1c4adc83a (patch) | |
tree | 9566a90388fb9ebb4280d03edb2035f6c91976e5 /src | |
parent | da89fd027e7fc9339cb3f637edf47f6a74c7d589 (diff) |
put EdDSA encoding sign bit at the MSB
Diffstat (limited to 'src')
-rw-r--r-- | src/Encoding/PointEncoding.v | 27 | ||||
-rw-r--r-- | src/Encoding/PointEncodingPre.v | 45 | ||||
-rw-r--r-- | src/Experiments/Ed25519.v | 4 | ||||
-rw-r--r-- | src/Spec/Ed25519.v | 9 | ||||
-rw-r--r-- | src/Util/WordUtil.v | 7 |
5 files changed, 59 insertions, 33 deletions
diff --git a/src/Encoding/PointEncoding.v b/src/Encoding/PointEncoding.v index f2139ff28..1160ed83a 100644 --- a/src/Encoding/PointEncoding.v +++ b/src/Encoding/PointEncoding.v @@ -3,7 +3,7 @@ Require Import Coq.Numbers.Natural.Peano.NPeano. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. Require Import Crypto.Spec.CompleteEdwardsCurve. Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. -Require Import Bedrock.Word. +Require Import Bedrock.Word Crypto.Util.WordUtil. Require Import Crypto.Tactics.VerdiTactics. Require Import Crypto.Util.Option. Require Import Crypto.Util.NatUtil. @@ -30,14 +30,16 @@ Section PointEncoding. {two_lt_m : (2 < m)%Z} {bound_check : (Z.to_nat m < 2 ^ b)%nat}. - Definition sign (x : F m) : bool := Z.testbit (F.to_Z x) 0. + Local Infix "++" := Word.combine. + Local Notation bit b := (Word.WS b Word.WO : Word.word 1). + Definition sign (x : F m) : bool := Z.testbit (F.to_Z x) 0. Definition Fencode (x : F m) : word b := NToWord b (Z.to_N (F.to_Z x)). Let Fpoint := @E.point (F m) Logic.eq F.one F.add F.mul Fa Fd. Definition encode_point (P : Fpoint) := - let '(x,y) := E.coordinates P in WS (sign x) (Fencode y). + let '(x,y) := E.coordinates P in Fencode y ++ bit (sign x). Import Morphisms. Lemma Proper_encode_point : Proper (E.eq ==> Logic.eq) encode_point. @@ -69,7 +71,6 @@ Section PointEncoding. {Kcoord_to_point : @E.point K Keq Kone Kadd Kmul Ka Kd -> Kpoint} {Kpoint_to_coord : Kpoint -> (K * K)}. Context {Kp2c_c2p : forall pt : E.point, Tuple.fieldwise (n := 2) Keq (Kpoint_to_coord (Kcoord_to_point pt)) (E.coordinates pt)}. - Check Kp2c_c2p. Context {Kpoint_eq : Kpoint -> Kpoint -> Prop} {Kpoint_add : Kpoint -> Kpoint -> Kpoint}. Context {Kpoint_eq_correct : forall p q, Kpoint_eq p q <-> Tuple.fieldwise (n := 2) Keq (Kpoint_to_coord p) (Kpoint_to_coord q)} {Kpoint_eq_Equivalence : Equivalence Kpoint_eq}. @@ -135,7 +136,7 @@ Section PointEncoding. Qed. Definition Kencode_point (P : Kpoint) := - let '(x,y) := Kpoint_to_coord P in WS (Ksign x) (Kenc y). + let '(x,y) := Kpoint_to_coord P in (Kenc y) ++ bit (Ksign x). Lemma Kencode_point_correct : forall P : Fpoint, encode_point P = Kencode_point (point_phi P). @@ -148,7 +149,9 @@ Section PointEncoding. pose proof (Kp2c_c2p x) as A; rewrite Heqp in A; inversion A; cbv [fst snd Tuple.fieldwise'] in * end. cbv [E.coordinates E.ref_phi proj1_sig] in *. - f_equal; rewrite ?H0, ?H1; auto. + apply (f_equal2 (fun a b => a ++ b)); + try apply (f_equal2 (fun a b => WS a b)); + rewrite ?H0, ?H1; auto. Qed. Lemma Proper_Kencode_point : Proper (Kpoint_eq ==> Logic.eq) Kencode_point. @@ -159,7 +162,9 @@ Section PointEncoding. destruct (Kpoint_to_coord x). destruct (Kpoint_to_coord y). simpl in H; destruct H. - f_equal; auto. + apply (f_equal2 (fun a b => a ++ b)); + try apply (f_equal2 (fun a b => WS a b)); + rewrite ?H0, ?H1; auto. Qed. @@ -174,11 +179,11 @@ Section PointEncoding. else Some p else None. - Definition Kdecode_coordinates (w : word (S b)) : option (K * K) := + Definition Kdecode_coordinates (w : word (b + 1)) : option (K * K) := option_rect (fun _ => option (K * K)) - (Kcoordinates_from_y (whd w)) + (Kcoordinates_from_y (wlast w)) None - (Kdec (wtl w)). + (Kdec (winit w)). Lemma onCurve_eq : forall x y, Keq (Kadd (Kmul Ka (Kmul x x)) (Kmul y y)) @@ -196,7 +201,7 @@ Section PointEncoding. | right _ => None end. - Definition Kdecode_point (w : word (S b)) : option Kpoint := + Definition Kdecode_point (w : word (b+1)) : option Kpoint := option_rect (fun _ => option Kpoint) Kpoint_from_xy None (Kdecode_coordinates w). Definition Fencoding : Encoding.CanonicalEncoding (F m) (word b). diff --git a/src/Encoding/PointEncodingPre.v b/src/Encoding/PointEncodingPre.v index 71b239698..8a0d4c849 100644 --- a/src/Encoding/PointEncodingPre.v +++ b/src/Encoding/PointEncodingPre.v @@ -3,7 +3,7 @@ Require Import Coq.Numbers.Natural.Peano.NPeano. Require Import Coq.Program.Equality. Require Import Crypto.CompleteEdwardsCurve.Pre. Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. -Require Import Bedrock.Word. +Require Import Bedrock.Word Crypto.Util.WordUtil. Require Import Crypto.Encoding.ModularWordEncodingTheorems. Require Import Crypto.Util.ZUtil. Require Import Crypto.Algebra. @@ -39,7 +39,6 @@ Section PointEncodingPre. Local Notation point := (@E.point F eq one add mul a d). Local Notation onCurve := (@onCurve F eq one add mul a d). Local Notation solve_for_x2 := (@E.solve_for_x2 F one sub mul div a d). - Check PrimeFieldTheorems.F.sqrt_5mod8_correct. Context {sz : nat} (sz_nonzero : (0 < sz)%nat). Context {sqrt : F -> F} {Proper_sqrt : Proper (eq ==>eq) sqrt} @@ -92,10 +91,10 @@ Section PointEncodingPre. apply E.solve_correct; eassumption. Qed. - Definition point_enc_coordinates (p : (F * F)) : Word.word (S sz) := let '(x,y) := p in - Word.WS (sign_bit x) (enc y). + Definition point_enc_coordinates (p : (F * F)) : Word.word (sz+1) := let '(x,y) := p in + combine (enc y) (WS (sign_bit x) WO). - Let point_enc (p : point) : Word.word (S sz) := point_enc_coordinates (E.coordinates p). + Let point_enc (p : point) : Word.word (sz+1) := point_enc_coordinates (E.coordinates p). Definition coord_from_y sign (y : F) : option (F * F) := let x2 := solve_for_x2 y in @@ -108,8 +107,8 @@ Section PointEncodingPre. else Some p else None. - Definition point_dec_coordinates (w : word (S sz)) : option (F * F) := - option_rect (fun _ => _) (coord_from_y (whd w)) None (dec (wtl w)). + Definition point_dec_coordinates (w : word (sz+1)) : option (F * F) := + option_rect (fun _ => _) (coord_from_y (wlast w)) None (dec (winit w)). (* Definition of product equality parameterized over equality of underlying types *) Definition prod_eq {A B} eqA eqB (x y : (A * B)) := let (xA,xB) := x in let (yA,yB) := y in @@ -247,9 +246,13 @@ Section PointEncodingPre. | right _ => None end. - Definition point_dec (w : word (S sz)) : option point := + Definition point_dec (w : word (sz+1)) : option point := option_rect (fun _ => option point) point_from_xy None (point_dec_coordinates w). + Lemma bool_neq_negb x y : x <> y <-> x = negb y. + destruct x, y; split; (discriminate||tauto). + Qed. + Lemma point_coordinates_encoding_canonical : forall w p, option_eq (Tuple.fieldwise (n := 2) eq) (point_dec_coordinates w) (Some p) -> point_enc_coordinates p = w. @@ -279,15 +282,19 @@ Section PointEncodingPre. Bool.eq_true_not_negb, Bool.not_false_is_true, encoding_canonical] end; - try solve [apply enc_canonical_equiv; rewrite Heqo; auto]; + rewrite combine_winit_wlast; split; + try apply (f_equal2 (fun a b => WS a b)); + try solve + [ trivial + | apply enc_canonical_equiv; rewrite Heqo; auto]; erewrite <-sign_bit_subst by eassumption. - { rewrite <-sign_bit_opp - by (intro A; apply F_eqb_iff in A; congruence). - auto using Bool.eq_true_not_negb. } - { rewrite <-sign_bit_opp - by (intro A; apply sign_bit_zero in A; congruence). - apply Bool.negb_false_iff, Bool.not_false_is_true. - auto. } + { intuition. } + { apply bool_neq_negb in Heqb0. rewrite <-sign_bit_opp. + { congruence. } + { rewrite Bool.andb_false_iff in *. + unfold not; intro Hx; destruct Heqb; + [apply F_eqb_iff in Hx; congruence + |rewrite (sign_bit_zero _ Hx) in *; simpl negb in *; congruence]. } } Qed. Lemma inversion_point_dec : forall w x, @@ -311,9 +318,11 @@ Section PointEncodingPre. auto using inversion_point_dec. Qed. - Lemma y_decode : forall p, dec (wtl (point_enc_coordinates p)) = Some (snd p). + + Lemma y_decode : forall p, dec (winit (point_enc_coordinates p)) = Some (snd p). Proof. intros; destruct p. cbv [point_enc_coordinates wtl snd]. + rewrite winit_combine. exact (encoding_valid _). Qed. @@ -372,6 +381,7 @@ Section PointEncodingPre. rewrite zero_square in *. assert (sqrt (solve_for_x2 y) == 0) by (rewrite solve_correct; tauto). rewrite !sign_bit_zero by (tauto || eauto). + rewrite wlast_combine. rewrite Bool.andb_false_r, Bool.eqb_reflx. apply option_coordinates_eq_iff; split; try reflexivity. etransitivity; eauto. @@ -388,6 +398,7 @@ Section PointEncodingPre. rewrite H0, zero_square in sqrt_square. rewrite Ring.zero_product_iff_zero_factor in sqrt_square. tauto. } Unfocus. + rewrite wlast_combine. break_if; [ | apply eqb_sign_opp_r in Heqb]; try (apply option_coordinates_eq_iff; split; try reflexivity); try eapply sign_match with (y := solve_for_x2 y); eauto; diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v index 36af82937..56d8112bd 100644 --- a/src/Experiments/Ed25519.v +++ b/src/Experiments/Ed25519.v @@ -1357,7 +1357,7 @@ Lemma eq_enc_E_iff : forall (P_ : Word.word b) (P : E), Option.option_eq CompleteEdwardsCurveTheorems.E.eq (Edec P_) (Some P). Proof. cbv [Eenc]. - eapply @PointEncoding.encode_point_decode_point_iff; try (exact iff_equivalence || exact curve_params); []. + eapply (@PointEncoding.encode_point_decode_point_iff (b-1)); try (exact iff_equivalence || exact curve_params); []. intros. apply (@PrimeFieldTheorems.F.sqrt_5mod8_correct GF25519.modulus _ eq_refl Fsqrt_minus1 Fsqrt_minus1_correct). eexists. @@ -1397,7 +1397,7 @@ Let verify_correct : (* Eenc := *) Eenc (* Senc := *) Senc (* prm := *) ed25519 - (* Proper_Eenc := *) PointEncoding.Proper_encode_point + (* Proper_Eenc := *) (PointEncoding.Proper_encode_point (b:=b-1)) (* Edec := *) Edec (* eq_enc_E_iff := *) eq_enc_E_iff (* Sdec := *) Sdec diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index a8e95cf9d..d6873607f 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.v @@ -61,12 +61,15 @@ Section Ed25519. (F.of_Z q 15112221349535400772501151409588531511454012693041857206046113283949847762202, F.of_Z q 4 / F.of_Z q 5). - Definition Fencode {b : nat} {m} : F m -> Word.word b := + Local Infix "++" := Word.combine. + Local Notation bit b := (Word.WS b Word.WO : Word.word 1). + + Definition Fencode {len} {m} : F m -> Word.word len := fun x : F m => (Word.NToWord _ (BinIntDef.Z.to_N (F.to_Z x))). Definition sign (x : F q) : bool := BinIntDef.Z.testbit (F.to_Z x) 0. Definition Eenc : E -> Word.word b := fun P => - let '(x,y) := E.coordinates P in Word.WS (sign x) (Fencode y). - Definition Senc : Fl -> Word.word b := Fencode. + let '(x,y) := E.coordinates P in Fencode (len:=b-1) y ++ bit (sign x). + Definition Senc : Fl -> Word.word b := Fencode (len:=b). (* TODO(andreser): prove this after we have fast scalar multplication *) Axiom B_order_l : CompleteEdwardsCurveTheorems.E.eq (BinInt.Z.to_nat l * B)%E E.zero. diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v index fd2e5e098..7a856f1e9 100644 --- a/src/Util/WordUtil.v +++ b/src/Util/WordUtil.v @@ -311,3 +311,10 @@ Proof. Admitted. Hint Rewrite @wordToN_wor using word_util_arith : push_wordToN. Hint Rewrite <- @wordToN_wor using word_util_arith : pull_wordToN. + +Axiom wlast : forall sz, word (sz+1) -> bool. Arguments wlast {_} _. +Axiom winit : forall sz, word (sz+1) -> word sz. Arguments winit {_} _. +Axiom combine_winit_wlast : forall {sz} a b (c:word (sz+1)), + @combine sz a 1 b = c <-> a = winit c /\ b = (WS (wlast c) WO). +Axiom winit_combine : forall sz a b, @winit sz (combine a b) = a. +Axiom wlast_combine : forall sz a b, @wlast sz (combine a (WS b WO)) = b.
\ No newline at end of file |