From 0b22eb729a738daaa9837acd3f0643aed642d873 Mon Sep 17 00:00:00 2001 From: jadep Date: Mon, 3 Oct 2016 17:56:30 -0400 Subject: Wrote proofs necessary to fill in all point-encoding related context variables in EdDSARepChange.v --- src/Encoding/PointEncodingPre.v | 175 ++++++++++++++++++++-------------------- 1 file changed, 89 insertions(+), 86 deletions(-) (limited to 'src/Encoding') diff --git a/src/Encoding/PointEncodingPre.v b/src/Encoding/PointEncodingPre.v index 00fb98133..3c3075d4f 100644 --- a/src/Encoding/PointEncodingPre.v +++ b/src/Encoding/PointEncodingPre.v @@ -5,13 +5,14 @@ Require Import Crypto.CompleteEdwardsCurve.Pre. Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. Require Import Bedrock.Word. Require Import Crypto.Encoding.ModularWordEncodingTheorems. -Require Import Crypto.Tactics.VerdiTactics. Require Import Crypto.Util.ZUtil. Require Import Crypto.Algebra. Require Import Crypto.Spec.Encoding Crypto.Spec.ModularWordEncoding Crypto.Spec.ModularArithmetic. Require Import Crypto.Util.Notations. +Require Import Crypto.Util.Tactics. +Require Import Crypto.Tactics.VerdiTactics. Require Export Crypto.Util.FixCoqMistakes. Generalizable All Variables. @@ -39,7 +40,7 @@ Section PointEncodingPre. Context {sz : nat} (sz_nonzero : (0 < sz)%nat). Context {sqrt : F -> F} (sqrt_square : forall x root, x == (root ^2) -> sqrt x == root) - (sqrt_subst : forall x y, x == y -> sqrt x == sqrt y). + (sqrt_subst : forall x y, x == y -> sqrt x == sqrt y). Context (FEncoding : canonical encoding of F as (word sz)). Context {sign_bit : F -> bool} (sign_bit_zero : forall x, x == 0 -> Logic.eq (sign_bit x) false) (sign_bit_opp : forall x, x !== 0 -> Logic.eq (negb (sign_bit x)) (sign_bit (opp x))) @@ -89,19 +90,19 @@ Section PointEncodingPre. Let point_enc (p : point) : Word.word (S sz) := point_enc_coordinates (E.coordinates p). - Definition point_dec_coordinates (w : Word.word (S sz)) : option (F * F) := - match dec (Word.wtl w) with - | None => None - | Some y => let x2 := solve_for_x2 y in - let x := sqrt x2 in - if eq_dec (x ^ 2) x2 - then - let p := (if Bool.eqb (whd w) (sign_bit x) then x else opp x, y) in - if (andb (F_eqb x 0) (whd w)) - then None (* special case for 0, since its opposite has the same sign; if the sign bit of 0 is 1, produce None.*) - else Some p - else None - end. + Definition coord_from_y sign (y : F) : option (F * F) := + let x2 := solve_for_x2 y in + let x := sqrt x2 in + if eq_dec (mul x x) x2 + then + let p := (if Bool.eqb sign (sign_bit x) then x else opp x, y) in + if (F_eqb x zero && sign)%bool + then None + 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 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 @@ -209,7 +210,7 @@ Section PointEncodingPre. option_coordinates_eq q r -> option_coordinates_eq p r. Proof. unfold option_coordinates_eq, option_eq; intros. - repeat break_match; subst; congruence || eauto using prod_eq_trans. + repeat break_match; subst; try destruct p,q; congruence || eauto using prod_eq_trans. Qed. Lemma prod_eq_sym : forall p q, prod_eq eq eq p q -> prod_eq eq eq q p. @@ -223,7 +224,7 @@ Section PointEncodingPre. option_coordinates_eq q p. Proof. unfold option_coordinates_eq, option_eq; intros. - repeat break_match; subst; congruence || eauto using prod_eq_sym; intuition. + repeat break_match; subst; try destruct p; congruence || eauto using prod_eq_sym; intuition. Qed. Opaque option_coordinates_eq option_point_eq point_eq option_eq prod_eq. @@ -232,59 +233,56 @@ Section PointEncodingPre. Ltac congruence_option_coord := exfalso; eauto using option_coordinates_eq_NS. - Lemma point_dec_coordinates_onCurve : forall w p, option_coordinates_eq (point_dec_coordinates w) (Some p) -> onCurve p. + Lemma onCurve_eq : forall x y, + eq (add (mul a (mul x x)) (mul y y)) + (add one (mul (mul d (mul x x)) (mul y y))) -> + @Pre.onCurve _ eq one add mul a d (x,y). Proof. - unfold point_dec_coordinates; intros. - edestruct dec; [ | congruence_option_coord ]. - break_if; [ | congruence_option_coord]. - break_if; [ congruence_option_coord | ]. - repeat match goal with [H: _ = _ :> Decidable _ |- _ ] => clear H end. - apply E.solve_correct in e. - break_if; eapply prod_eq_onCurve; - eauto using inversion_option_coordinates_eq, solve_onCurve, solve_opp_onCurve. + tauto. Qed. - Definition point_dec' w p : option point := - match (option_coordinates_eq_dec (point_dec_coordinates w) (Some p)) with - | left EQ => Some (exist _ p (point_dec_coordinates_onCurve w p EQ)) - | right _ => None (* this case is never reached *) + Definition point_from_xy (xy : F * F) : option point := + let '(x,y) := xy in + match Decidable.dec (eq (add (mul a (mul x x)) (mul y y)) + (add one (mul (mul d (mul x x)) (mul y y)))) with + | left A => Some (exist _ (x,y) (onCurve_eq x y A)) + | right _ => None end. Definition point_dec (w : word (S sz)) : option point := - match point_dec_coordinates w with - | Some p => point_dec' w p - | None => None - end. + option_rect (fun _ => option point) point_from_xy None (point_dec_coordinates w). Lemma point_coordinates_encoding_canonical : forall w p, point_dec_coordinates w = Some p -> point_enc_coordinates p = w. Proof. - unfold point_dec_coordinates, point_enc_coordinates; intros ? ? coord_dec_Some. - case_eq (dec (wtl w)); [ intros ? dec_Some | intros dec_None; rewrite dec_None in *; congruence ]. - destruct p. - rewrite (shatter_word w). - f_equal; rewrite dec_Some in *; - do 2 (break_if; try congruence); inversion coord_dec_Some; subst. - + destruct (eq_dec (sqrt (solve_for_x2 f1)) 0) as [sqrt_0 | ?]. - - break_if; rewrite sign_bit_zero in * by (assumption || (rewrite sqrt_0; ring)); - auto using Bool.eqb_prop. - apply F_eqb_iff in sqrt_0. - rewrite sqrt_0 in *. - destruct (whd w); inversion Heqb0; auto. - - break_if. - symmetry; auto using Bool.eqb_prop. - rewrite <- sign_bit_opp by assumption. - destruct (whd w); inversion Heqb0; break_if; auto. - + inversion coord_dec_Some; subst. - auto using encoding_canonical. + repeat match goal with + | |- _ => progress cbv [point_dec_coordinates option_rect + point_enc_coordinates coord_from_y] in * + | |- _ => progress intros + | |- _ => progress rewrite ?Bool.andb_true_r, + ?Bool.andb_false_r, ?Bool.eqb_false_iff in * + | |- _ => rewrite <-sign_bit_opp + by ((rewrite <-F_eqb_iff; congruence) || + (intro A; specialize (sign_bit_zero _ A); congruence)) + | p : F * F |- _ => destruct p + | |- _ => break_match; try discriminate + | H : Some _ = Some _ |- _ => inversion H; subst; clear H + | w : word (S sz) |- WS _ _ = ?w => rewrite (shatter_word w); + f_equal + | |- sign_bit _ = whd ?w => destruct (whd w) + | |- negb _ = false => apply Bool.negb_false_iff + | |- _ => solve [auto using Bool.eqb_prop, + Bool.eq_true_not_negb, + Bool.not_false_is_true, encoding_canonical] + end. Qed. Lemma inversion_point_dec : forall w x, point_dec w = Some x -> point_dec_coordinates w = Some (E.coordinates x). Proof. - unfold point_dec, E.coordinates; intros. + unfold point_dec, E.coordinates, point_from_xy, option_rect; intros. break_match; [ | congruence]. - unfold point_dec' in *; break_match; [ | congruence]. + destruct p. break_match; [ | congruence ]. match goal with [ H : Some _ = Some _ |- _ ] => inversion H end. reflexivity. Qed. @@ -302,9 +300,11 @@ Section PointEncodingPre. exact (encoding_valid _). Qed. - Lemma F_eqb_false : forall x y, x !== y -> F_eqb x y = false. + Lemma F_eqb_false : forall x y, x !== y <-> F_eqb x y = false. Proof. - intros; unfold F_eqb; destruct (eq_dec x y); congruence. + intros; unfold F_eqb; destruct (eq_dec x y). + + split; intuition eauto; try discriminate. + + tauto. Qed. Lemma eqb_sign_opp_r : forall x y, (y !== 0) -> @@ -333,7 +333,7 @@ Section PointEncodingPre. option_coordinates_eq (point_dec_coordinates (point_enc_coordinates p)) (Some p). Proof. intros [x y] onCurve_p. - unfold point_dec_coordinates. + unfold point_dec_coordinates, point_from_xy, coord_from_y, option_rect. rewrite y_decode. cbv [whd point_enc_coordinates snd]. pose proof (square_sqrt (solve_for_x2 y) x) as solve_sqrt_ok. @@ -353,7 +353,7 @@ Section PointEncodingPre. apply option_coordinates_eq_iff; split; try reflexivity. transitivity (sqrt (x ^2)); auto. apply (sqrt_square); reflexivity. - + rewrite F_eqb_false, Bool.andb_false_l by (rewrite sqrt_square; [ | eauto]; assumption). + + rewrite (proj1 (F_eqb_false _ 0)), Bool.andb_false_l by (rewrite sqrt_square; [ | eauto]; assumption). 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; @@ -362,37 +362,40 @@ Section PointEncodingPre. assumption. Qed. -Lemma point_dec'_valid : forall p q, option_coordinates_eq (Some q) (Some (proj1_sig p)) -> - option_point_eq (point_dec' (point_enc_coordinates (proj1_sig p)) q) (Some p). -Proof. - unfold point_dec'; intros. - break_match. - + f_equal. - apply option_point_eq_iff. - destruct p as [ [ ? ? ] ? ]; simpl in *. - assumption. - + exfalso; apply n. - eapply option_coordinates_eq_trans; [ | eauto using option_coordinates_eq_sym ]. - apply point_encoding_coordinates_valid. - apply (proj2_sig p). -Qed. - Lemma point_encoding_valid : forall p, option_point_eq (point_dec (point_enc p)) (Some p). Proof. - intros. - unfold point_dec. - replace (point_enc p) with (point_enc_coordinates (proj1_sig p)) by reflexivity. - break_match. - + eapply (point_dec'_valid p). - rewrite <-Heqo. - apply point_encoding_coordinates_valid. - apply (proj2_sig p). - + exfalso. - eapply option_coordinates_eq_NS. - pose proof (point_encoding_coordinates_valid _ (proj2_sig p)). - rewrite Heqo in *. - eassumption. + repeat match goal with + | |- _ => progress (cbv [point_dec point_enc E.coordinates + option_rect point_from_xy]; intros) + | |- _ => progress simpl proj1_sig in * + | p : point |- _ => destruct p + | p : F * F |- _ => destruct p + | |- appcontext[proj1_sig (exist ?a ?b ?c)] => + progress replace (proj1_sig (exist a b c)) with b by reflexivity + | |- _ => break_match + | |- _ => split + | |- option_point_eq _ _ => apply option_point_eq_iff + | |- option_coordinates_eq _ _ => apply option_coordinates_eq_iff + | H : a * ?x^2 + ?y^2 == 1 + d * ?x^2 * ?y^2 |- _ => + unique pose proof (point_encoding_coordinates_valid (_,_) H) + | Hpq : point_dec_coordinates (point_enc_coordinates ?p) = Some ?q, + Hp : option_coordinates_eq + (point_dec_coordinates (point_enc_coordinates ?p)) (Some ?p) + |- _ => unique assert (option_coordinates_eq (Some q) (Some p)) + by (rewrite Hpq in Hp; auto) + | H : option_coordinates_eq (Some ?p) (Some ?q) |- _ => + apply option_coordinates_eq_iff in H; destruct H; + (assumption || (symmetry; assumption)) + end. + exfalso. + apply n. + apply option_coordinates_eq_iff in H1; destruct H1. + rewrite H1, H2; assumption. + + + rewrite Heqo in H0. + congruence_option_coord. Qed. End PointEncodingPre. -- cgit v1.2.3