Fixed Encoding/PointEncodingTheorems; imports had been deleted, but for some reason I wasn't affected. Also updated the same file to use E module.

1 files changed, 41 insertions, 23 deletions

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)) <? wordToN (enc x))%N.
-Definition point_enc (p : point) : word (S sz) := let '(x,y) := proj1_sig p in
+Definition point_enc (p : E.point) : word (S sz) := let '(x,y) := proj1_sig p in
   WS (sign_bit x) (enc y).
 Definition point_dec_coordinates (w : word (S sz)) : option (F q * F q) :=
   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
       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.