proved most of point encoding admits, fixed some build system issues (dead imports of PointFormats and Galois things)

5 files changed, 105 insertions, 9 deletions

diff --git a/src/Encoding/EncodingTheorems.v b/src/Encoding/EncodingTheorems.v
new file mode 100644
index 000000000..f53ad0319
--- /dev/null
+++ b/src/Encoding/EncodingTheorems.v
@@ -0,0 +1,14 @@
+Require Import Crypto.Spec.Encoding.
+
+Section EncodingTheorems.
+  Context {A B : Type} {E : encoding of A as B}.
+  
+  Lemma encoding_inj : forall x y, enc x = enc y -> x = y.
+  Proof.
+    intros.
+    assert (dec (enc x) = dec (enc y)) as dec_enc_eq by (f_equal; auto).
+    do 2 rewrite encoding_valid in dec_enc_eq.
+    inversion dec_enc_eq; auto.
+  Qed.
+
+End EncodingTheorems.
diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v
index 889b4fa3d..fe0398ff4 100644
--- a/src/ModularArithmetic/PrimeFieldTheorems.v
+++ b/src/ModularArithmetic/PrimeFieldTheorems.v
@@ -197,6 +197,24 @@ Section VariousModPrime.
   Proof.
     intros; field. (* TODO: Warning: Collision between bound variables ... *)
   Qed.
+ 
+  Lemma F_eq_opp_zero : forall x : F q, 2 < q -> (x = opp x <-> x = 0).
+  Proof.
+    split; intro A.
+    + pose proof (F_opp_spec x) as opp_spec.
+      rewrite <- A in opp_spec.
+      replace (x + x) with (ZToField 2 * x) in opp_spec by ring.
+      apply Fq_mul_zero_why in opp_spec.
+      destruct opp_spec as [eq_2_0 | ?]; auto.
+      apply F_eq in eq_2_0.
+      rewrite FieldToZ_ZToField in eq_2_0.
+      replace (FieldToZ 0) with 0%Z in eq_2_0 by auto.
+      replace (2 mod q) with 2 in eq_2_0; try discriminate.
+      symmetry; apply Z.mod_small; omega.
+    + subst.
+      rewrite <- (F_opp_spec 0) at 1.
+      ring.
+  Qed.
 
   Lemma euler_criterion_F : forall (a : F q) (q_odd : 2 < q) (a_nonzero : a <> 0),
     (a ^ (Z.to_N (q / 2)) = 1) <-> isSquare a.
diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v
index 47d772a65..04e6a5fc2 100644
--- a/src/Spec/Ed25519.v
+++ b/src/Spec/Ed25519.v
@@ -4,7 +4,6 @@ Require Import Crypto.Spec.Encoding Crypto.Spec.PointEncoding.
 Require Import Crypto.Spec.EdDSA.
 Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems.
-Require Import Crypto.Curves.PointFormats.
 Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil Crypto.Util.NumTheoryUtil.
 Require Import Bedrock.Word.
 Require Import VerdiTactics.
diff --git a/src/Spec/PointEncoding.v b/src/Spec/PointEncoding.v
index 84cbc1af2..ea662a6b7 100644
--- a/src/Spec/PointEncoding.v
+++ b/src/Spec/PointEncoding.v
@@ -1,9 +1,8 @@
 Require Import ZArith.ZArith Zpower ZArith Znumtheory.
 Require Import NPeano NArith.
-Require Import Crypto.Spec.Encoding.
+Require Import Crypto.Spec.Encoding Crypto.Encoding.EncodingTheorems.
 Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems.
-Require Import Crypto.Curves.PointFormats.
 Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil Crypto.Util.NumTheoryUtil.
 Require Import Bedrock.Word.
 Require Import VerdiTactics.
@@ -39,14 +38,71 @@ Definition point_dec (w : word (S sz)) : option point :=
   end.
 
 Lemma y_decode : forall p, dec (wtl (point_enc p)) = Some (snd (proj1_sig p)).
-Admitted.
+Proof.
+  intros.
+  destruct p as [[x y] onCurve_p]; simpl.
+  exact (encoding_valid y).
+Qed.
+
+
+Lemma wordToN_enc_neq_opp : forall x, x <> 0 -> (wordToN (enc (opp x)) <> wordToN (enc x))%N.
+Proof.
+  intros x x_nonzero.
+  intro false_eq.
+  apply x_nonzero.
+  apply F_eq_opp_zero; try apply two_lt_q.
+  apply wordToN_inj in false_eq.
+  apply encoding_inj in false_eq.
+  auto.
+Qed.
+
+Lemma sign_bit_opp_negb : forall x, x <> 0 -> negb (sign_bit x) = sign_bit (opp x).
+Proof.
+  intros x x_nonzero.
+  unfold sign_bit.
+  rewrite <- N.leb_antisym.
+  rewrite N.ltb_compare, N.leb_compare.
+  rewrite F_opp_involutive.
+  case_eq (wordToN (enc x) ?= wordToN (enc (opp x)))%N; auto.
+  intro wordToN_enc_eq.
+  pose proof (wordToN_enc_neq_opp x x_nonzero).
+  apply N.compare_eq_iff in wordToN_enc_eq.
+  congruence.
+Qed.
+
+Lemma sign_bit_opp : forall x y, y <> 0 ->
+  (sign_bit x <> sign_bit y <-> sign_bit x = sign_bit (opp y)).
+Proof.
+  split; intro sign_mismatch; case_eq (sign_bit x); case_eq (sign_bit y);
+    try congruence; intros y_sign x_sign; rewrite <- sign_bit_opp_negb in * by auto;
+    rewrite y_sign, x_sign in *; reflexivity || discriminate.
+Qed.
+
+Lemma sign_bit_squares : forall x y, y <> 0 -> x ^ 2 = y ^ 2 ->
+  sign_bit x = sign_bit y -> x = y.
+Proof.
+  intros ? ? y_nonzero squares_eq sign_match.
+  destruct (sqrt_solutions _ _ squares_eq) as [? | eq_opp]; auto.
+  assert (sign_bit x = sign_bit (opp y)) as sign_mismatch by (f_equal; auto).
+  apply sign_bit_opp in sign_mismatch; auto.
+  congruence.
+Qed.
 
 Lemma sign_bit_match : forall x x' y : F q, onCurve (x, y) -> onCurve (x', y) ->
   sign_bit x = sign_bit x' -> x = x'.
-Admitted.
-
-Lemma sign_bit_opp : forall x y, sign_bit x <> sign_bit y -> sign_bit x = sign_bit (opp y).
-Admitted.
+Proof.
+  intros ? ? ? onCurve_x onCurve_x' sign_match.
+  apply solve_correct in onCurve_x.
+  apply solve_correct in onCurve_x'.
+  destruct (F_eq_dec x' 0).
+  + subst.
+    rewrite Fq_pow_zero in onCurve_x' by congruence.
+    rewrite <- onCurve_x' in *.
+    eapply Fq_root_zero; eauto.
+  + apply sign_bit_squares; auto.
+    rewrite onCurve_x, onCurve_x'.
+    reflexivity.
+Qed.
 
 Lemma point_encoding_valid : forall p, point_dec (point_enc p) = Some p.
 Proof.
@@ -68,6 +124,13 @@ Proof.
     f_equal.
     apply sign_bit_opp in Heqb.
     apply (sign_bit_match _ _ y); auto.
+    intro eq_zero.
+    apply 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.
+    apply Fq_root_zero in onCurve_p.
+    rewrite onCurve_p in Heqb; auto.
 Qed.
 
 Instance point_encoding : encoding of point as (word (S sz)) := {
@@ -76,4 +139,6 @@ Instance point_encoding : encoding of point as (word (S sz)) := {
   encoding_valid := point_encoding_valid
 }.
 
+Print Assumptions point_encoding.
+
 End PointEncoding.
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index e716cd244..516efd8b2 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -1,5 +1,5 @@
 Require Import ModularArithmetic.PrimeFieldTheorems.
-Require Import Galois.BaseSystem Galois.ModularBaseSystem.
+Require Import BaseSystem ModularBaseSystem.
 Require Import List Util.ListUtil.
 Import ListNotations.
 Require Import ZArith.ZArith Zpower ZArith Znumtheory.