From dabd1cb20aa5b5ab3d433d6ac0cbf6684b5c7283 Mon Sep 17 00:00:00 2001 From: jadep Date: Wed, 25 May 2016 13:33:51 -0400 Subject: Fixed Encoding/PointEncodingTheorems; imports had been deleted, but for some reason I wasn't affected. Also updated the same file to use E module. --- src/Encoding/PointEncodingTheorems.v | 64 +++++++++++++++++++++++------------- 1 file changed, 41 insertions(+), 23 deletions(-) (limited to 'src/Encoding') diff --git a/src/Encoding/PointEncodingTheorems.v b/src/Encoding/PointEncodingTheorems.v index 2713bd063..ccea1d81b 100644 --- a/src/Encoding/PointEncodingTheorems.v +++ b/src/Encoding/PointEncodingTheorems.v @@ -1,3 +1,15 @@ +Require Import Coq.ZArith.ZArith Coq.ZArith.Znumtheory. +Require Import Coq.Numbers.Natural.Peano.NPeano. +Require Import Coq.Program.Equality. +Require Import Crypto.Encoding.EncodingTheorems. +Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. +Require Import Bedrock.Word. +Require Import Crypto.Tactics.VerdiTactics. + +Require Import Crypto.Spec.Encoding Crypto.Spec.ModularArithmetic Crypto.Spec.CompleteEdwardsCurve. + +Local Open Scope F_scope. Section PointEncoding. Context {prm: CompleteEdwardsCurve.TwistedEdwardsParams} {sz : nat} @@ -16,12 +28,12 @@ Section PointEncoding. Definition sqrt_valid (a : F q) := ((sqrt_mod_q a) ^ 2 = a)%F. - Lemma solve_sqrt_valid : forall (p : point), - sqrt_valid (solve_for_x2 (snd (proj1_sig p))). + Lemma solve_sqrt_valid : forall (p : E.point), + sqrt_valid (E.solve_for_x2 (snd (proj1_sig p))). Proof. intros. destruct p as [[x y] onCurve_xy]; simpl. - rewrite (solve_correct x y) in onCurve_xy. + rewrite (E.solve_correct x y) in onCurve_xy. rewrite <- onCurve_xy. unfold sqrt_valid. eapply sqrt_mod_q_valid; eauto. @@ -29,31 +41,31 @@ Section PointEncoding. Grab Existential Variables. eauto. Qed. - Lemma solve_onCurve: forall (y : F q), sqrt_valid (solve_for_x2 y) -> - onCurve (sqrt_mod_q (solve_for_x2 y), y). + Lemma solve_onCurve: forall (y : F q), sqrt_valid (E.solve_for_x2 y) -> + E.onCurve (sqrt_mod_q (E.solve_for_x2 y), y). Proof. intros. unfold sqrt_valid in *. - apply solve_correct; auto. + apply E.solve_correct; auto. Qed. - Lemma solve_opp_onCurve: forall (y : F q), sqrt_valid (solve_for_x2 y) -> - onCurve (opp (sqrt_mod_q (solve_for_x2 y)), y). + Lemma solve_opp_onCurve: forall (y : F q), sqrt_valid (E.solve_for_x2 y) -> + E.onCurve (opp (sqrt_mod_q (E.solve_for_x2 y)), y). Proof. intros y sqrt_valid_x2. unfold sqrt_valid in *. - apply solve_correct. + apply E.solve_correct. rewrite <- sqrt_valid_x2 at 2. ring. Qed. Definition sign_bit (x : F q) := (wordToN (enc (opp x)) None - | Some y => let x2 := solve_for_x2 y in + | Some y => let x2 := E.solve_for_x2 y in let x := sqrt_mod_q x2 in if F_eq_dec (x ^ 2) x2 then @@ -62,16 +74,16 @@ Definition point_dec_coordinates (w : word (S sz)) : option (F q * F q) := else None end. -Definition point_dec (w : word (S sz)) : option point := +Definition point_dec (w : word (S sz)) : option E.point := match dec (wtl w) with | None => None - | Some y => let x2 := solve_for_x2 y in + | Some y => let x2 := E.solve_for_x2 y in let x := sqrt_mod_q x2 in match (F_eq_dec (x ^ 2) x2) with | right _ => None | left EQ => if Bool.eqb (whd w) (sign_bit x) - then Some (mkPoint (x, y) (solve_onCurve y EQ)) - else Some (mkPoint (opp x, y) (solve_opp_onCurve y EQ)) + then Some (exist _ (x, y) (solve_onCurve y EQ)) + else Some (exist _ (opp x, y) (solve_opp_onCurve y EQ)) end end. @@ -135,12 +147,12 @@ Proof. congruence. Qed. -Lemma sign_bit_match : forall x x' y : F q, onCurve (x, y) -> onCurve (x', y) -> +Lemma sign_bit_match : forall x x' y : F q, E.onCurve (x, y) -> E.onCurve (x', y) -> sign_bit x = sign_bit x' -> x = x'. Proof. intros ? ? ? onCurve_x onCurve_x' sign_match. - apply solve_correct in onCurve_x. - apply solve_correct in onCurve_x'. + apply E.solve_correct in onCurve_x. + apply E.solve_correct in onCurve_x'. destruct (F_eq_dec x' 0). + subst. rewrite Fq_pow_zero in onCurve_x' by congruence. @@ -160,8 +172,8 @@ Proof. unfold sqrt_valid in *. destruct p as [[x y] onCurve_p]. simpl in *. - destruct (F_eq_dec ((sqrt_mod_q (solve_for_x2 y)) ^ 2) (solve_for_x2 y)); intuition. - break_if; f_equal; apply point_eq. + destruct (F_eq_dec ((sqrt_mod_q (E.solve_for_x2 y)) ^ 2) (E.solve_for_x2 y)); intuition. + break_if; f_equal; apply E.point_eq. + rewrite Bool.eqb_true_iff in Heqb. pose proof (solve_onCurve y solve_sqrt_valid_p). f_equal. @@ -172,7 +184,7 @@ Proof. apply sign_bit_opp in Heqb. apply (sign_bit_match _ _ y); auto. intro eq_zero. - apply solve_correct in onCurve_p. + apply E.solve_correct in onCurve_p. rewrite eq_zero in *. rewrite Fq_pow_zero in solve_sqrt_valid_p by congruence. rewrite <- solve_sqrt_valid_p in onCurve_p. @@ -180,10 +192,16 @@ Proof. rewrite onCurve_p in Heqb; auto. Qed. -Instance point_encoding : canonical encoding of point as (word (S sz)) := { +(* Waiting on canonicalization *) +Lemma point_encoding_canonical : forall (x_enc : word (S sz)) (x : E.point), +point_dec x_enc = Some x -> point_enc x = x_enc. +Admitted. + +Instance point_encoding : canonical encoding of E.point as (word (S sz)) := { enc := point_enc; dec := point_dec; - encoding_valid := point_encoding_valid + encoding_valid := point_encoding_valid; + encoding_canonical := point_encoding_canonical }. End PointEncoding. -- cgit v1.2.3