diff options
Diffstat (limited to 'src/Encoding/PointEncoding.v')
-rw-r--r-- | src/Encoding/PointEncoding.v | 109 |
1 files changed, 96 insertions, 13 deletions
diff --git a/src/Encoding/PointEncoding.v b/src/Encoding/PointEncoding.v index b005ce3df..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. @@ -15,7 +15,7 @@ Require Crypto.Encoding.PointEncodingPre. Eenc := encode_point Proper_Eenc := Proper_encode_point Edec := Fdecode_point (notation) - eq_enc_E_iff := Fdecode_encode_iff + eq_enc_E_iff := encode_point_decode_point_iff EToRep := point_phi Ahomom := point_phi_homomorphism ERepEnc := Kencode_point @@ -27,16 +27,19 @@ Require Crypto.Encoding.PointEncodingPre. Section PointEncoding. Context {b : nat} {m : Z} {Fa Fd : F m} {prime_m : Znumtheory.prime m} + {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. @@ -68,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}. @@ -122,7 +124,8 @@ Section PointEncoding. option_eq Keq (option_map phi (Fdecode w)) (Kdec w)}. Context {Fsqrt : F m -> F m} {phi_sqrt : forall x, Keq (phi (Fsqrt x)) (Ksqrt (phi x))} - {Fsqrt_square : forall x root, eq x (F.mul root root) -> eq (Fsqrt x) root}. + {Fsqrt_square : forall x root, eq x (F.mul root root) -> + eq (F.mul (Fsqrt x) (Fsqrt x)) x}. Lemma point_phi_homomorphism: @Algebra.Monoid.is_homomorphism Fpoint E.eq Fpoint_add @@ -133,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). @@ -146,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. @@ -157,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. @@ -172,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)) @@ -194,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). @@ -434,6 +441,82 @@ Section PointEncoding. + intros. apply Kpoint_from_xy_correct. Qed. + Lemma sign_zero : forall x, x = F.zero -> sign x = false. + Proof. + intros; subst. + reflexivity. + Qed. + + Lemma sign_negb : forall x : F m, x <> F.zero -> + negb (sign x) = sign (F.opp x). + Proof. + intros. + cbv [sign]. + rewrite !Z.bit0_odd. + rewrite F.to_Z_opp. + rewrite F.eq_to_Z_iff in H. + replace (@F.to_Z m F.zero) with 0%Z in H by reflexivity. + rewrite Z.mod_opp_l_nz by (solve [ZUtil.Z.prime_bound] || + rewrite F.mod_to_Z; auto). + rewrite F.mod_to_Z. + rewrite Z.odd_sub. + destruct (ZUtil.Z.prime_odd_or_2 m prime_m) as [? | m_odd]; + [ omega | rewrite m_odd]. + rewrite <-Bool.xorb_true_l; auto. + Qed. + + Lemma Eeq_point_eq : forall x y : option E.point, + option_eq E.eq x y <-> + option_eq + (@PointEncodingPre.point_eq _ eq F.one F.add F.mul Fa Fd) x y. + Proof. + intros. + cbv [option_eq E.eq PointEncodingPre.point_eq + PointEncodingPre.prod_eq]; repeat break_match; + try reflexivity. + cbv [E.coordinates]. + subst. + rewrite Heqp1, Heqp0. + cbv [Tuple.fieldwise Tuple.fieldwise' fst snd]. + tauto. + Qed. + + Lemma enc_canonical_equiv : forall (x_enc : word b) (x : F m), + option_eq eq (Fdecode x_enc) (Some x) -> + Fencode x = x_enc. + Proof. + intros. + cbv [option_eq] in *. + break_match; try discriminate. + subst. + apply (@Encoding.encoding_canonical _ _ Fencoding). + auto. + Qed. + + Lemma encode_point_decode_point_iff : forall P_ P, + encode_point P = P_ <-> + Option.option_eq E.eq (Fdecode_point P_) (Some P). + Proof. + pose proof (@PointEncodingPre.point_encoding_canonical + _ eq F.zero F.one F.opp F.add F.sub F.mul F.div + _ Fa Fd _ Fsqrt Fencoding enc_canonical_equiv + sign sign_zero sign_negb + ) as Hcanonical. + let A := fresh "H" in + match type of Hcanonical with + ?P -> _ => assert P as A by congruence; + specialize (Hcanonical A); clear A end. + intros. + rewrite Eeq_point_eq. + split; intros; subst. + { apply PointEncodingPre.point_encoding_valid; + auto using sign_zero, sign_negb; + congruence. } + { apply Hcanonical. + cbv [option_eq PointEncodingPre.point_eq PointEncodingPre.prod_eq] in H |- *. + break_match; congruence. } + Qed. + End RepChange. End PointEncoding. |