From 09a9310b877c5032146a6e73b59fcef9bda71e5e Mon Sep 17 00:00:00 2001 From: jadep Date: Thu, 6 Oct 2016 13:47:48 -0400 Subject: Moved PointEncoding out of Spec --- src/Spec/PointEncoding.v | 432 ----------------------------------------------- 1 file changed, 432 deletions(-) delete mode 100644 src/Spec/PointEncoding.v (limited to 'src/Spec') diff --git a/src/Spec/PointEncoding.v b/src/Spec/PointEncoding.v deleted file mode 100644 index 92ba91a6d..000000000 --- a/src/Spec/PointEncoding.v +++ /dev/null @@ -1,432 +0,0 @@ -Require Import Coq.ZArith.ZArith. -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 Crypto.Tactics.VerdiTactics. -Require Import Crypto.Util.Option. -Require Import Crypto.Util.NatUtil. -Require Import Crypto.Util.WordUtil. -Require Import Crypto.Util.FixCoqMistakes. -Require Crypto.Encoding.PointEncodingPre. - -(* This file should fill in the following context variables from EdDSARepChange.v - Eenc := encode_point - Proper_Eenc := Proper_encode_point - Edec := Fdecode_point (notation) - eq_enc_E_iff := Fdecode_encode_iff - EToRep := point_phi - Ahomom := point_phi_homomorphism - ERepEnc := Kencode_point - ERepEnc_correct := Kencode_point_correct - Proper_ERepEnc := Proper_Kencode_point - ERepDec := Kdecode_point - ERepDec_correct := Kdecode_point_correct -*) - -Section PointEncoding. - Context {b : nat} {m : Z} {Fa Fd : F m} {prime_m : Znumtheory.prime m} - {bound_check : (Z.to_nat m < 2 ^ b)%nat}. - - 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). - - Import Morphisms. - Lemma Proper_encode_point : Proper (E.eq ==> Logic.eq) encode_point. - Proof. - repeat intro. - eapply @E.Proper_coordinates in H; eauto using F.field_modulo, F.eq_dec. - cbv [encode_point]. - remember (E.coordinates x) as cx; destruct cx as [cx1 cy1]. - remember (E.coordinates y) as cy; destruct cy as [cx2 cy2]. - inversion H; cbv [fst snd] in *. - cbv [Tuple.fieldwise'] in *. - repeat f_equal; auto. - Qed. - - Section RepChange. - Context {K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv} - `{Kfield:@Algebra.field K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv} - {Keq_dec:Decidable.DecidableRel Keq}. - Context {phi:F m->K} {phi_homomorphism : @Algebra.Ring.is_homomorphism - (F m) eq F.one F.add F.mul - K Keq Kone Kadd Kmul phi}. - Context {Ka Kd : K} {phi_a : Keq (phi Fa) Ka} {phi_d : Keq (phi Fd) Kd}. - Context {Ksign : K -> bool} {Kenc : K -> word b} - {Ksign_correct : forall x, sign x = Ksign (phi x)} - {Kenc_correct : forall x, Fencode x = Kenc (phi x)}. - - Notation KonCurve := (@Pre.onCurve _ Keq Kone Kadd Kmul Ka Kd). - Context {Kpoint} {Kcoord_to_point : forall P, KonCurve P -> Kpoint} - {Kpoint_to_coord : Kpoint -> (K * K)}. - Context {Kp2c_c2p : forall P pf, Tuple.fieldwise (n := 2) Keq (Kpoint_to_coord (Kcoord_to_point P pf)) P}. - 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}. - - Context {Fprm:@E.twisted_edwards_params (F m) eq F.zero F.one F.add F.mul Fa Fd}. - Context {Kprm:@E.twisted_edwards_params K Keq Kzero Kone Kadd Kmul Ka Kd}. - Context {phi_bijective : forall x y, Keq (phi x) (phi y) <-> x = y}. - - Lemma phi_onCurve : forall x y, - eq (F.add (F.mul Fa (F.mul x x)) (F.mul y y)) - (F.add F.one (F.mul (F.mul Fd (F.mul x x)) (F.mul y y))) <-> - Keq (Kadd (Kmul Ka (Kmul (phi x) (phi x))) (Kmul (phi y) (phi y))) - (Kadd Kone (Kmul (Kmul Kd (Kmul (phi x) (phi x))) (Kmul (phi y) (phi y)))). - Proof. - intros. - rewrite <-phi_a, <-phi_d. - rewrite <-Algebra.Ring.homomorphism_one. - rewrite <-!Algebra.Ring.homomorphism_mul. - rewrite <-!Algebra.Ring.homomorphism_add. - rewrite phi_bijective. - reflexivity. - Qed. - - Definition point_phi (P : Fpoint) : Kpoint. - Proof. - destruct P as [[fx fy]]. - apply (Kcoord_to_point (phi fx, phi fy)). - apply phi_onCurve; auto. - Defined. - - Lemma Proper_point_phi : Proper (E.eq ==> Kpoint_eq) point_phi. - Proof. - repeat intro. - apply Kpoint_eq_correct; cbv [point_phi]. - destruct x, y. - repeat break_let. - rewrite !Kp2c_c2p. - apply E.Proper_coordinates in H; cbv [E.coordinates proj1_sig] in H. - inversion H; econstructor; cbv [Tuple.fieldwise' fst snd] in *; subst; - reflexivity. - Qed. - - Notation Fpoint_add := (@E.add _ _ _ _ _ _ _ _ _ _ (F.field_modulo m) _ Fa Fd _). - Definition Fdecode (w : word b) : option (F m) := - let z := Z.of_N (wordToN w) in - if Z_lt_dec z m then Some (F.of_Z m z) else None. - - Context {Kpoint_add_correct : forall P Q, Kpoint_eq - (point_phi (Fpoint_add P Q)) - (Kpoint_add (point_phi P) (point_phi Q))}. - Context {Kdec : word b -> option K} {Ksqrt : K -> K}. - Context {Proper_Ksqrt : Proper (Keq ==> Keq) Ksqrt} - {Proper_Ksign : Proper (Keq ==> eq) Ksign} - {Proper_Kenc : Proper (Keq ==> eq) Kenc}. - Context {phi_decode : forall w, - 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}. - - Lemma point_phi_homomorphism: @Algebra.Group.is_homomorphism - Fpoint E.eq Fpoint_add - Kpoint Kpoint_eq Kpoint_add point_phi. - Proof. - econstructor; intros; auto using Kpoint_add_correct. - apply Proper_point_phi. - Qed. - - Definition Kencode_point (P : Kpoint) := - let '(x,y) := Kpoint_to_coord P in WS (Ksign x) (Kenc y). - - Lemma Kencode_point_correct : forall P : Fpoint, - encode_point P = Kencode_point (point_phi P). - Proof. - cbv [encode_point Kencode_point point_phi]; intros. - destruct P as [[fx fy]]; cbv [E.coordinates proj1_sig]. - break_match. - match goal with - H: Kpoint_to_coord (Kcoord_to_point (?x, ?y) ?pf) = (_,_) |- _ => let A := fresh "H" in - pose proof (Kp2c_c2p (x,y) pf) as A; rewrite Heqp in A; - inversion A; cbv [fst snd Tuple.fieldwise'] in * end. - f_equal; rewrite ?H0, ?H1; auto. - Qed. - - Lemma Proper_Kencode_point : Proper (Kpoint_eq ==> Logic.eq) Kencode_point. - Proof. - repeat intro; cbv [Kencode_point]. - apply Kpoint_eq_correct in H. - simpl in H. - destruct (Kpoint_to_coord x). - destruct (Kpoint_to_coord y). - simpl in H; destruct H. - f_equal; auto. - Qed. - - - Definition Kcoordinates_from_y sign_bit (y : K) : option (K * K) := - let x2 := @E.solve_for_x2 _ Kone Ksub Kmul Kdiv Ka Kd y in - let x := Ksqrt x2 in - if Keq_dec (Kmul x x) x2 - then - let p := (if Bool.eqb sign_bit (Ksign x) then x else Kopp x, y) in - if (PointEncodingPre.F_eqb x Kzero && sign_bit)%bool - then None - else Some p - else None. - - Definition Kdecode_coordinates (w : word (S b)) : option (K * K) := - option_rect (fun _ => option (K * K)) - (Kcoordinates_from_y (whd w)) - None - (Kdec (wtl w)). - - Lemma onCurve_eq : forall x y, - Keq (Kadd (Kmul Ka (Kmul x x)) (Kmul y y)) - (Kadd Kone (Kmul (Kmul Kd (Kmul x x)) (Kmul y y))) -> - @Pre.onCurve _ Keq Kone Kadd Kmul Ka Kd (x,y). - Proof. - tauto. - Qed. - - Definition Kpoint_from_xy (xy : K * K) : option Kpoint := - let '(x,y) := xy in - match Decidable.dec (Keq (Kadd (Kmul Ka (Kmul x x)) (Kmul y y)) - (Kadd Kone (Kmul (Kmul Kd (Kmul x x)) (Kmul y y)))) with - | left A => Some (Kcoord_to_point (x,y) (onCurve_eq x y A)) - | right _ => None - end. - - Definition Kdecode_point (w : word (S b)) : option Kpoint := - option_rect (fun _ => option Kpoint) Kpoint_from_xy None (Kdecode_coordinates w). - - Definition Fencoding : Encoding.CanonicalEncoding (F m) (word b). - Proof. - eapply Encoding.Build_CanonicalEncoding with (enc := Fencode) (dec := Fdecode); - cbv [Fencode Fdecode]; intros. - + assert (0 < m)%Z as m_pos by (ZUtil.Z.prime_bound). - pose proof (F.to_Z_range x m_pos). - rewrite !wordToN_NToWord_idempotent by (apply bound_check_nat_N; - transitivity (Z.to_nat m); auto; apply Z2Nat.inj_lt; omega). - rewrite Z2N.id by omega. - rewrite F.of_Z_to_Z. - break_if; auto; omega. - + break_if; auto; try discriminate. - inversion H; subst. clear H. - rewrite F.to_Z_of_Z. - rewrite Z.mod_small by (split; try omega; auto using N2Z.is_nonneg). - rewrite N2Z.id. - apply NToWord_wordToN. - Defined. - - Lemma Fdecode_encode_iff P_ P : Fencode P = P_ <-> Fdecode P_ = Some P. - Proof. - pose proof (@Encoding.encoding_canonical _ _ Fencoding). - pose proof (@Encoding.encoding_valid _ _ Fencoding). - cbv [Encoding.dec Encoding.enc Fencoding] in *. - split; intros; subst; auto. - Qed. - - Lemma option_rect_shuffle : - forall {X A B C D} (x : X) - (EQD : D -> D -> Prop) (EQC : C -> C -> Prop) - {EquivC : Equivalence EQD} {EquivC : Equivalence EQC} - (ab : A -> B) (bc : B -> option C) (dc : D -> option C) (ad : A -> D) - {Proper_dc : Proper (EQD==>option_eq EQC) dc} - (oa : X -> option A) (od : X -> option D), - (forall x : X, option_eq EQD (option_map ad (oa x)) (od x)) -> - (forall x : A, option_eq EQC (dc (ad x)) (bc (ab x))) -> - option_eq EQC - (option_rect (fun _ => option C) (fun x: D => dc x) None (od x)) - (option_rect (fun _ => option C) (fun x : A => bc (ab x)) None (oa x)). - Proof. - cbv; intros. - specialize (H x). - destruct (oa x) as [a |]; [ | repeat break_match; reflexivity || discriminate]. - destruct (od x) as [d |]; [ | contradiction ]. - pose proof (H0 a). - assert (option_eq EQC (dc d) (dc (ad a))) by (apply Proper_dc; symmetry; auto). - cbv [option_eq] in *. - repeat break_match; try tauto; try reflexivity; try discriminate; - etransitivity; eauto. - Qed. - - Notation Fdecode_coordinates :=( @PointEncodingPre.point_dec_coordinates - _ eq F.zero F.one F.opp F.sub F.mul F.div - _ Fa Fd _ Fsqrt Fencoding sign). - Notation Fdecode_point := (@PointEncodingPre.point_dec - _ eq F.zero F.one F.opp F.add F.sub F.mul F.div - _ Fa Fd _ Fsqrt Fencoding sign). - - Lemma phi_solve_for_x2 : forall x : F m, - Keq (@E.solve_for_x2 _ Kone Ksub Kmul Kdiv Ka Kd (phi x)) - (phi (@E.solve_for_x2 _ F.one F.sub F.mul F.div Fa Fd x)). - Proof. - intros. - cbv [E.solve_for_x2]. - rewrite Algebra.Field.homomorphism_div by apply E.a_d_y2_nonzero. - rewrite !Algebra.Ring.homomorphism_sub. - rewrite !Algebra.Ring.homomorphism_mul. - rewrite Algebra.Ring.homomorphism_one. - rewrite phi_a, phi_d. - reflexivity. - Qed. - - Lemma option_map_option_rect : forall {A B C} (g : B -> C) (f : A -> option B) o, - option_map g (option_rect (fun _ : option A => _) f None o) = - option_rect (fun _ : option A => _) - (fun x => option_map g (f x)) None o. - Proof. - intros. cbv [option_rect option_map]. - repeat (break_match; try discriminate); congruence. - Qed. - - Notation Fcoordinates_from_y := - (@PointEncodingPre.coord_from_y - _ eq F.zero F.one F.opp F.sub F.mul F.div - _ Fa Fd Fsqrt sign). - - Definition coord_phi (p : F m* F m) := let '(x, y) := p in (phi x, phi y). - - Lemma Kcoordinates_from_y_correct : forall sign_bit y, - option_eq (Tuple.fieldwise (n := 2) Keq) - (Kcoordinates_from_y sign_bit (phi y)) - (option_map coord_phi (Fcoordinates_from_y sign_bit y)). - Proof. - cbv [Kcoordinates_from_y PointEncodingPre.coord_from_y]. - intros. - match goal with - |- option_eq _ _ (option_map ?f (if ?A - then (if ?B then None else Some ?xy) - else None)) => - transitivity (if A then (if B then None else Some (f xy)) else None); - [ | repeat (break_if; auto; try discriminate); reflexivity] - end. - match goal with - |- option_eq _ (if Keq_dec ?ka ?kb then _ else _) - (if F.eq_dec ?fa ?fb then _ else _) => - destruct (Keq_dec ka kb) as [keq | keq]; - rewrite phi_solve_for_x2, <-phi_sqrt, <-Algebra.Ring.homomorphism_mul in keq; - rewrite phi_bijective in keq; - destruct (F.eq_dec fa fb); try congruence; try reflexivity - end. - clear keq e. - match goal with - |- option_eq _ (if ?A then _ else _) (if ?B then _ else _) => assert (A = B) - end. - { - destruct (sign_bit); rewrite ?Bool.andb_true_r, ?Bool.andb_false_r; auto. - cbv [PointEncodingPre.F_eqb]. - pose proof (@Algebra.Ring.homomorphism_is_homomorphism _ _ _ _ _ _ _ _ _ _ _ phi_homomorphism). - pose proof (@Algebra.Group.homomorphism_id _ _ _ _ _ _ _ _ _ _ _ _ _ H). - match goal with |- (if ?x then _ else _) = _ => destruct x as [keq | keq] end; - rewrite phi_solve_for_x2, <-phi_sqrt, <-H0 in keq; - rewrite phi_bijective in keq; cbv [F.zero]; break_if; try congruence; reflexivity. - } - rewrite H. - break_if; try reflexivity. - econstructor; cbv [coord_phi Tuple.fieldwise' fst snd]; try reflexivity. - rewrite Ksign_correct, !phi_sqrt, !phi_solve_for_x2. - break_if; rewrite ?Algebra.Ring.homomorphism_opp, ?phi_sqrt, ?phi_solve_for_x2; - reflexivity. - Qed. - - Global Instance Proper_solve_for_x2 : forall {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv a d} - {Ffield : @Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}, - Proper (Feq==>Feq) (@E.solve_for_x2 F Fone Fsub Fmul Fdiv a d) | 0. - Proof. - repeat intro; subst. - cbv [E.solve_for_x2]. - rewrite H. reflexivity. - Qed. - - Lemma Proper_Kcoordinates_from_y : - Proper (eq==>Keq ==> option_eq (Tuple.fieldwise (n := 2) Keq)) Kcoordinates_from_y. - Proof. - repeat intro; subst. - cbv [Kcoordinates_from_y]. - match goal with |- option_eq _ (if ?A then _ else _) (if ?B then _ else _) => - destruct A as [keq | keq]; rewrite H0 in keq; - destruct B; try congruence; try reflexivity end. - destruct y; rewrite ?Bool.andb_true_r, ?Bool.andb_false_r; - break_if; repeat break_if; - rewrite ?@PointEncodingPre.F_eqb_iff, <-?@PointEncodingPre.F_eqb_false, - ?Bool.eqb_true_iff, ?Bool.eqb_false_iff in *; try discriminate; try reflexivity; - repeat match goal with - | H : appcontext[E.solve_for_x2 x0] |- _ => rewrite H0 in H; - congruence end; - simpl; rewrite H0; intuition reflexivity. - Qed. - - Lemma Kdecode_coordinates_correct : forall w, - option_eq (Tuple.fieldwise (n := 2) Keq) - (Kdecode_coordinates w) - (option_map coord_phi (Fdecode_coordinates w)). - Proof. - intros; cbv [Kdecode_coordinates point_phi PointEncodingPre.point_dec_coordinates]. - rewrite option_map_option_rect. - eapply option_rect_shuffle with (EQD := Keq). - + apply Algebra.monoid_Equivalence. - + apply (@Tuple.Equivalence_fieldwise K _ _ 2). - + apply Proper_Kcoordinates_from_y; auto. - + cbv [Encoding.dec Fencoding]. - apply phi_decode. - + apply Kcoordinates_from_y_correct. - Qed. - - Lemma Kpoint_from_xy_correct : forall xy, - option_eq Kpoint_eq - (Kpoint_from_xy (coord_phi xy)) - (option_map point_phi (PointEncodingPre.point_from_xy xy)). - Proof. - intros; cbv [Kpoint_from_xy PointEncodingPre.point_from_xy coord_phi]. - destruct xy as [x y]. - pose proof (phi_onCurve x y). - repeat break_match; try tauto; try reflexivity. - simpl. - apply Kpoint_eq_correct. - rewrite !Kp2c_c2p. - reflexivity. - Qed. - - Lemma Proper_Kpoint_from_xy : - Proper (Tuple.fieldwise (n := 2) Keq ==> option_eq Kpoint_eq) Kpoint_from_xy. - Proof. - repeat intro; cbv [Kpoint_from_xy]. - destruct x as [x1 y1]. - destruct y as [x2 y2]. - cbv [Tuple.tuple' Tuple.fieldwise Tuple.fieldwise' fst snd] in *. - destruct H. - break_match. { - pose proof k as k'. - rewrite H, H0 in k'. - break_match; try congruence. - simpl. apply Kpoint_eq_correct. - repeat ( break_match; - match goal with - H: Kpoint_to_coord (Kcoord_to_point (?x, ?y) ?pf) = (_,_) |- _ => let A := fresh "H" in - pose proof (Kp2c_c2p (x,y) pf) as A; rewrite H in A; - inversion A; cbv [fst snd Tuple.fieldwise'] in * end; - intuition; - repeat match goal with H : Keq _ _ |- _ => rewrite H end; try reflexivity). - } { - pose proof n as k'. - rewrite H, H0 in k'. - break_match; congruence. - } - Qed. - - Lemma Kdecode_point_correct : forall w, - option_eq Kpoint_eq (Kdecode_point w) (option_map point_phi (Fdecode_point w)). - Proof. - intros; cbv [Kdecode_point PointEncodingPre.point_dec]. - rewrite option_map_option_rect. - eapply option_rect_shuffle with (EQD := Tuple.fieldwise (n := 2) Keq). - + apply Tuple.Equivalence_fieldwise. - + auto. - + apply Proper_Kpoint_from_xy. - + intros. symmetry. apply Kdecode_coordinates_correct. - + intros. apply Kpoint_from_xy_correct. - Qed. - - End RepChange. - -End PointEncoding. \ No newline at end of file -- cgit v1.2.3