Completed encoding reorganization; factored sign_bit out of PointEncodings and finished encoding admits.

9 files changed, 232 insertions, 124 deletions

diff --git a/_CoqProject b/_CoqProject
index b6f056b3e..1046bef3c 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -8,6 +8,7 @@ src/CompleteEdwardsCurve/ExtendedCoordinates.v
 src/CompleteEdwardsCurve/Pre.v
 src/Encoding/EncodingTheorems.v
 src/Encoding/ModularWordEncodingPre.v
+src/Encoding/ModularWordEncodingTheorems.v
 src/Encoding/PointEncodingPre.v
 src/ModularArithmetic/ExtendedBaseVector.v
 src/ModularArithmetic/FField.v
diff --git a/src/Encoding/ModularWordEncodingPre.v b/src/Encoding/ModularWordEncodingPre.v
index 272748103..cb2f5a045 100644
--- a/src/Encoding/ModularWordEncodingPre.v
+++ b/src/Encoding/ModularWordEncodingPre.v
@@ -38,16 +38,42 @@ Section ModularWordEncodingPre.
     omega.
   Qed.
 
+  (* TODO: move to WordUtil *)
+  Lemma wordToN_NToWord_idempotent : forall sz n, (n < Npow2 sz)%N ->
+    wordToN (NToWord sz n) = n.
+  Proof.
+    intros.
+    rewrite wordToN_nat, NToWord_nat.
+    rewrite wordToNat_natToWord_idempotent; rewrite Nnat.N2Nat.id; auto.
+  Qed.
+
+  (* TODO: move to WordUtil *)
+  Lemma NToWord_wordToN : forall sz w, NToWord sz (wordToN w) = w.
+  Proof.
+    intros.
+    rewrite wordToN_nat, NToWord_nat, Nnat.Nat2N.id.
+    apply natToWord_wordToNat.
+  Qed.
+
   Lemma Fm_encoding_valid : forall x, Fm_dec (Fm_enc x) = Some x.
   Proof.
     unfold Fm_dec, Fm_enc; intros.
     pose proof (FieldToZ_range x m_pos).
-    rewrite wordToN_nat, NToWord_nat.
-    rewrite wordToNat_natToWord_idempotent by
-      (rewrite Nnat.N2Nat.id; apply bound_check_N).
-    rewrite Nnat.N2Nat.id, Z2N.id by omega.
+    rewrite wordToN_NToWord_idempotent by apply bound_check_N.
+    rewrite Z2N.id by omega.
     rewrite ZToField_idempotent.
     break_if; auto; omega.
   Qed.
 
+  Lemma Fm_encoding_canonical : forall w x, Fm_dec w = Some x -> Fm_enc x = w.
+  Proof.
+    unfold Fm_dec, Fm_enc; intros ? ? dec_Some.
+    break_if; [ | congruence ].
+    inversion dec_Some.
+    rewrite FieldToZ_ZToField.
+    rewrite Z.mod_small by (pose proof (N2Z.is_nonneg (wordToN w)); try omega).
+    rewrite N2Z.id.
+    apply NToWord_wordToN.
+  Qed.
+
 End ModularWordEncodingPre.
diff --git a/src/Encoding/ModularWordEncodingTheorems.v b/src/Encoding/ModularWordEncodingTheorems.v
new file mode 100644
index 000000000..83f199d90
--- /dev/null
+++ b/src/Encoding/ModularWordEncodingTheorems.v
@@ -0,0 +1,89 @@
+Require Import Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
+Require Import Coq.Numbers.Natural.Peano.NPeano.
+Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
+Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
+Require Import Bedrock.Word.
+Require Import Crypto.Tactics.VerdiTactics.
+Require Import Crypto.Spec.Encoding.
+Require Import Crypto.Spec.ModularWordEncoding.
+
+
+Local Open Scope F_scope.
+
+Section SignBit.
+  Context {m : Z} {prime_m : prime m} {two_lt_m : (2 < m)%Z} {sz : nat} {bound_check : (Z.to_nat m < 2 ^ sz)%nat}.
+  Lemma m_pos : (0 < m)%Z.
+  Proof.
+    apply prime_ge_2 in prime_m; omega.
+  Qed.
+
+  Arguments modular_word_encoding {m} {sz} m_pos bound_check.
+  Let Fm_encoding := modular_word_encoding m_pos bound_check.
+
+  Definition sign_bit (x : F m) :=
+  match (@enc _ _ Fm_encoding x) with
+    | Word.WO => false
+    | Word.WS b _ w' => b
+  end.
+
+  Lemma sign_bit_parity : forall x, sign_bit x = Z.odd x.
+  Proof.
+    unfold sign_bit; intros.
+    unfold Fm_encoding, enc, modular_word_encoding, Fm_enc.
+    pose proof (shatter_word (NToWord sz (Z.to_N x))) as shatter.
+    case_eq sz; intros; subst; rewrite shatter.
+    + pose proof (prime_ge_2 m prime_m).
+      simpl in bound_check.
+      assert (m < 1)%Z by (apply Z2Nat.inj_lt; try omega; assumption).
+      omega.
+    + pose proof (FieldToZ_range x m_pos).  
+      destruct (FieldToZ x); auto.
+      - destruct p; auto.
+      - pose proof (Pos2Z.neg_is_neg p); omega.
+   Qed.
+
+  Lemma sign_bit_zero : sign_bit 0 = false.
+  Proof.
+    rewrite sign_bit_parity; auto.
+  Qed.
+
+  (* TODO : move to ZUtil *)
+  Lemma Z_odd_mod : forall a b, (b <> 0)%Z ->
+    Z.odd (a mod b) = if Z.odd b then xorb (Z.odd a) (Z.odd (a / b)) else Z.odd a.
+  Proof.
+    intros.
+    rewrite Zmod_eq_full by assumption.
+    rewrite <-Z.add_opp_r, Z.odd_add, Z.odd_opp, Z.odd_mul.
+    break_if; rewrite ?Bool.andb_true_r, ?Bool.andb_false_r; auto using Bool.xorb_false_r.
+  Qed.
+
+  (* TODO : move to ModularArithmeticTheorems *)
+  Lemma F_FieldToZ_add_opp : forall x : F m, x <> 0 -> (FieldToZ x + FieldToZ (opp x) = m)%Z.
+  Proof.
+    intros.
+    rewrite FieldToZ_opp.
+    rewrite Z_mod_nz_opp_full, mod_FieldToZ; try omega.
+    rewrite mod_FieldToZ.
+    replace 0%Z with (@FieldToZ m 0) by auto.
+    intro false_eq.
+    rewrite <-F_eq in false_eq.
+    congruence.
+  Qed.
+
+  Lemma sign_bit_opp : forall (x : F m), x <> 0 -> negb (sign_bit x) = sign_bit (opp x).
+  Proof.
+    intros.
+    pose proof sign_bit_zero as sign_zero.
+    rewrite !sign_bit_parity in *.
+    pose proof (F_opp_spec x) as opp_spec_x.
+    apply F_eq in opp_spec_x.
+    rewrite FieldToZ_add in opp_spec_x.
+    rewrite <-opp_spec_x, Z_odd_mod in sign_zero by omega.
+    replace (Z.odd m) with true in sign_zero by (destruct (ZUtil.prime_odd_or_2 m prime_m); auto || omega).
+    rewrite Z.odd_add, F_FieldToZ_add_opp, Z.div_same, Bool.xorb_true_r in sign_zero by assumption || omega.
+    apply Bool.xorb_eq.
+    rewrite <-Bool.negb_xorb_l.
+    assumption.
+  Qed.
+
+End SignBit.
\ No newline at end of file
diff --git a/src/Encoding/PointEncodingPre.v b/src/Encoding/PointEncodingPre.v
index b7e907e10..9b65d9819 100644
--- a/src/Encoding/PointEncodingPre.v
+++ b/src/Encoding/PointEncodingPre.v
@@ -5,16 +5,21 @@ Require Import Crypto.Encoding.EncodingTheorems.
 Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
 Require Import Bedrock.Word.
+Require Import Crypto.Encoding.ModularWordEncodingTheorems.
 Require Import Crypto.Tactics.VerdiTactics.
+Require Import Crypto.Util.ZUtil.
 
-Require Import Crypto.Spec.Encoding Crypto.Spec.ModularArithmetic.
+Require Import Crypto.Spec.Encoding Crypto.Spec.ModularWordEncoding Crypto.Spec.ModularArithmetic.
 
 Local Open Scope F_scope.
 
 Section PointEncoding.
   Context {prm: TwistedEdwardsParams} {sz : nat} {sz_nonzero : (0 < sz)%nat}
-   {FqEncoding : encoding of F q as word sz} {q_5mod8 : (q mod 8 = 5)%Z}
-   {sqrt_minus1_valid : (@ZToField q 2 ^ Z.to_N (q / 4)) ^ 2 = opp 1}.
+   {bound_check : (Z.to_nat q < 2 ^ sz)%nat} {q_5mod8 : (q mod 8 = 5)%Z}
+   {sqrt_minus1_valid : (@ZToField q 2 ^ Z.to_N (q / 4)) ^ 2 = opp 1}
+   {FqEncoding : encoding of (F q) as (word sz)}
+   {sign_bit : F q -> bool} {sign_bit_zero : sign_bit 0 = false}
+   {sign_bit_opp : forall x, x <> 0 -> negb (sign_bit x) = sign_bit (opp x)}.
   Existing Instance prime_q.
 
   Add Field Ffield : (@Ffield_theory q _)
@@ -58,12 +63,6 @@ Section PointEncoding.
     ring.
   Qed.
 
-  Let sign_bit (x : F CompleteEdwardsCurve.q) :=
-    match (enc x) with
-      | Word.WO => false
-      | Word.WS b _ w' => b
-    end.
-
   Definition point_enc_coordinates (p : (F q * F q)) : Word.word (S sz) := let '(x,y) := p in
     Word.WS (sign_bit x) (enc y).
 
@@ -94,22 +93,21 @@ Section PointEncoding.
     break_if; [ congruence | ]. 
     break_if; inversion_Some_eq; auto using solve_onCurve, solve_opp_onCurve.
   Qed.
-(*
-  Definition point_dec (w : word (S sz)) : option point.
-    case_eq (point_dec_coordinates w); intros; [ | apply None].
-    apply Some.
-    eapply mkPoint.
-    eapply point_dec_coordinates_onCurve; eauto.
-  Defined.
-*)
-  Lemma option_eq_dec : forall {A} (x y : option A), {x = y} + {x <> y}.
+
+  Lemma prod_eq_dec : forall {A} (A_eq_dec : forall a a' : A, {a = a'} + {a <> a'})
+   (x y : (A * A)), {x = y} + {x <> y}.
   Proof.
     decide equality.
-  Admitted.
+  Qed.
 
+  Lemma option_eq_dec : forall {A} (A_eq_dec : forall a a' : A, {a = a'} + {a <> a'})
+   (x y : option A), {x = y} + {x <> y}.
+  Proof.
+    decide equality.
+  Qed.
 
   Definition point_dec' w p : option E.point :=
-    match (option_eq_dec (point_dec_coordinates sign_bit w) (Some p)) with
+    match (option_eq_dec (prod_eq_dec F_eq_dec) (point_dec_coordinates sign_bit w) (Some p)) with
       | left EQ => Some (exist _ p (point_dec_coordinates_onCurve w p EQ))
       | right _ => None (* this case is never reached *)
     end.
@@ -120,38 +118,6 @@ Section PointEncoding.
     | None => None
     end.
 
-  Lemma enc_first_bit_opp : forall (x : F q), x <> 0 ->
-    match enc x with
-    | WO => True
-    | WS b n w => match enc (opp x) with
-                  | WO => False
-                  | WS b' _ _ => b' = negb b
-                  end
-    end.
-  Proof.
-  Admitted.
-
-  Lemma first_bit_zero : match enc 0 with
-    | WO => False
-    | WS b _ _ => b = false
-    end.
-  Admitted.
-
-  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.
-    pose proof (enc_first_bit_opp x x_nonzero).
-    pose proof (shatter_word (enc x)) as shatter_enc_x.
-    pose proof (shatter_word (enc (opp x))) as shatter_enc_opp.
-    destruct sz; try omega.
-    rewrite shatter_enc_x, shatter_enc_opp in *.
-    auto.
-  Qed.
-
-  Lemma Fq_encoding_canonical : forall w (n : F q), dec w = Some n -> enc n = w.
-  Admitted.
-
   (* TODO : move *)
   Lemma sqrt_mod_q_0 : forall x : F q, sqrt_mod_q x = 0 -> x = 0.
   Proof.
@@ -173,15 +139,6 @@ Section PointEncoding.
       rewrite ring_subst in *.
       apply Fq_1_neq_0; assumption.
   Qed.
-    
-  Lemma sign_bit_zero : sign_bit 0 = false.
-  Proof.
-    unfold sign_bit.
-    pose proof first_bit_zero.
-    destruct sz; try omega.
-    pose proof (shatter_word (enc 0)) as shatter_enc0.
-    simpl in shatter_enc0; rewrite shatter_enc0 in *; assumption.
-  Qed.
 
   Lemma point_coordinates_encoding_canonical : forall w p,
     point_dec_coordinates sign_bit w = Some p -> point_enc_coordinates p = w.
@@ -202,10 +159,10 @@ Section PointEncoding.
         discriminate.
       - break_if.
         symmetry; auto using Bool.eqb_prop.
-        rewrite <- sign_bit_opp_negb by auto.
+        rewrite <- sign_bit_opp by assumption.
         destruct (whd w); inversion Heqb0; break_if; auto.
     + inversion coord_dec_Some; subst.
-      auto using Fq_encoding_canonical.
+      auto using encoding_canonical.
 Qed.
 
   Lemma point_encoding_canonical : forall w x, point_dec w = Some x -> point_enc x = w.
@@ -238,7 +195,7 @@ Proof.
   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.
@@ -249,12 +206,13 @@ Proof.
   apply encoding_inj in false_eq.
   auto.
 Qed.
+*)
 
-Lemma sign_bit_opp : forall x y, y <> 0 ->
+Lemma sign_bit_opp_eq_iff : 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;
+    try congruence; intros y_sign x_sign; rewrite <- sign_bit_opp in * by auto;
     rewrite y_sign, x_sign in *; reflexivity || discriminate.
 Qed.
 
@@ -264,7 +222,7 @@ 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.
+  apply sign_bit_opp_eq_iff in sign_mismatch; auto.
   congruence.
 Qed.
 
@@ -283,9 +241,25 @@ Proof.
     rewrite onCurve_x, onCurve_x'.
     reflexivity.
 Qed.
-(*
-Lemma blah : forall x y, (F_eqb (sqrt_mod_q (solve_for_x2 y)) 0 && sign_bit x)%bool = true.
-*)
+
+(* TODO : move *)
+Lemma sqrt_mod_q_of_0 : @sqrt_mod_q q 0 = 0.
+Proof.
+  unfold sqrt_mod_q.
+  rewrite !Fq_pow_zero.
+  break_if; ring.
+
+  congruence.
+  intro false_eq.
+  SearchAbout Z.to_N.
+  rewrite <-(N2Z.id 0) in false_eq.
+  rewrite N2Z.inj_0 in false_eq.
+  pose proof (prime_ge_2 q prime_q).
+  apply Z2N.inj in false_eq; zero_bounds.
+  assert (0 < q / 8 + 1)%Z.
+  apply Z.add_nonneg_pos; zero_bounds.
+  omega.
+Qed.
 
 Lemma point_encoding_coordinates_valid : forall p, E.onCurve p ->
    point_dec_coordinates sign_bit (point_enc_coordinates p) = Some p.
@@ -294,37 +268,40 @@ Proof.
   unfold point_dec_coordinates.
   rewrite y_decode.
   pose proof (solve_sqrt_valid p onCurve_p) as solve_sqrt_valid_p.
-  unfold sqrt_valid in *.
   destruct p as [x y].
-  simpl in *.
-  destruct (F_eq_dec ((sqrt_mod_q (E.solve_for_x2 y)) ^ 2) (E.solve_for_x2 y)); intuition.
-  break_if; f_equal.
-  + case_eq (F_eqb (sqrt_mod_q (E.solve_for_x2 y)) 0); intros eqb_0.
-(*
-    SearchAbout F_eqb.
-
- [ | simpl in *; congruence].
-    
-
-
-    rewrite Bool.eqb_true_iff in Heqb.
-    pose proof (solve_onCurve y solve_sqrt_valid_p).
-    f_equal.
-    apply (sign_bit_match _ _ y); auto.
-  + rewrite Bool.eqb_false_iff in Heqb.
-    pose proof (solve_opp_onCurve y solve_sqrt_valid_p).
-    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.
-*)
-Admitted.
+  unfold sqrt_valid in *.
+  simpl.
+  replace (E.solve_for_x2 y) with (x ^ 2 : F q) in * by (apply E.solve_correct; assumption).
+  case_eq (F_eqb x 0); intro eqb_x_0.
+  + apply F_eqb_eq in eqb_x_0; rewrite eqb_x_0 in *.
+    rewrite !Fq_pow_zero, sqrt_mod_q_of_0, Fq_pow_zero by congruence.
+    rewrite if_F_eq_dec_if_F_eqb, sign_bit_zero. 
+    reflexivity.
+  + assert (sqrt_mod_q (x ^ 2) <> 0) by (intro false_eq; apply sqrt_mod_q_0 in false_eq;
+      apply Fq_root_zero in false_eq; rewrite false_eq, F_eqb_refl in eqb_x_0; congruence).
+    replace (F_eqb (sqrt_mod_q (x ^ 2)) 0) with false by (symmetry;
+        apply F_eqb_neq_complete; assumption).
+    break_if.
+    - simpl.
+      f_equal.
+      break_if.
+      * rewrite Bool.eqb_true_iff in Heqb.
+        pose proof (solve_onCurve y solve_sqrt_valid_p).
+        f_equal.
+        apply (sign_bit_match _ _ y); auto.
+        apply E.solve_correct in onCurve_p; rewrite onCurve_p in *.
+        assumption.
+      * rewrite Bool.eqb_false_iff in Heqb.
+        pose proof (solve_opp_onCurve y solve_sqrt_valid_p).
+        f_equal.
+        apply sign_bit_opp_eq_iff in Heqb; try assumption.
+        apply (sign_bit_match _ _ y); auto.
+        apply E.solve_correct in onCurve_p.
+        rewrite onCurve_p; auto.
+   - simpl in solve_sqrt_valid_p.
+     replace (E.solve_for_x2 y) with (x ^ 2 : F q) in * by (apply E.solve_correct; assumption).
+     congruence.
+Qed.
 
 Lemma point_dec'_valid : forall p,
   point_dec' (point_enc_coordinates (proj1_sig p)) (proj1_sig p) = Some p.
diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v
index 6543823cb..505797987 100644
--- a/src/Spec/Ed25519.v
+++ b/src/Spec/Ed25519.v
@@ -1,6 +1,7 @@
 Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
 Require Import Coq.Numbers.Natural.Peano.NPeano Coq.NArith.NArith.
 Require Import Crypto.Spec.PointEncoding Crypto.Spec.ModularWordEncoding.
+Require Import Crypto.Encoding.ModularWordEncodingTheorems.
 Require Import Crypto.Spec.EdDSA.
 Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems.
@@ -142,7 +143,11 @@ Proof.
   reflexivity.
 Qed.
 
-Definition PointEncoding := @point_encoding curve25519params (b - 1) FqEncoding.
+Lemma b_minus1_nonzero : 0 < b - 1. Proof. cbv. omega. Qed.
+
+Definition PointEncoding : encoding of E.point as (word b) :=
+  (@point_encoding _ _ b_minus1_nonzero b_valid q_5mod8 sqrt_minus1_valid FqEncoding
+  (@sign_bit _ prime_q two_lt_q _ b_valid) sign_bit_zero sign_bit_opp).
 
 Definition H : forall n : nat, word n -> word (b + b). Admitted.
 Definition B : E.point. Admitted. (* TODO: B = decodePoint (y=4/5, x="positive") *)
diff --git a/src/Spec/Encoding.v b/src/Spec/Encoding.v
index 9a2d5e5ed..17dcb4b3e 100644
--- a/src/Spec/Encoding.v
+++ b/src/Spec/Encoding.v
@@ -1,7 +1,8 @@
 Class Encoding (T B:Type) := {
   enc : T -> B ;
   dec : B -> option T ;
-  encoding_valid : forall x, dec (enc x) = Some x
+  encoding_valid : forall x, dec (enc x) = Some x ;
+  encoding_canonical : forall x_enc x, dec x_enc = Some x -> enc x = x_enc
 }.
 
 Notation "'encoding' 'of' T 'as' B" := (Encoding T B) (at level 50).
\ No newline at end of file
diff --git a/src/Spec/ModularWordEncoding.v b/src/Spec/ModularWordEncoding.v
index 9f7e3340b..262b1054d 100644
--- a/src/Spec/ModularWordEncoding.v
+++ b/src/Spec/ModularWordEncoding.v
@@ -25,7 +25,10 @@ Section ModularWordEncoding.
   Instance modular_word_encoding : encoding of F m as word sz := {
     enc := Fm_enc;
     dec := Fm_dec;
-    encoding_valid := @ModularWordEncodingPre.Fm_encoding_valid m sz m_pos bound_check
+    encoding_valid :=
+      @ModularWordEncodingPre.Fm_encoding_valid m sz m_pos bound_check;
+    encoding_canonical :=
+      @ModularWordEncodingPre.Fm_encoding_canonical m sz bound_check
   }.
 
 End ModularWordEncoding.
diff --git a/src/Spec/PointEncoding.v b/src/Spec/PointEncoding.v
index 1d79a018d..3668632f4 100644
--- a/src/Spec/PointEncoding.v
+++ b/src/Spec/PointEncoding.v
@@ -6,22 +6,21 @@ Require Crypto.ModularArithmetic.PrimeFieldTheorems.
 Require Bedrock.Word.
 Require Crypto.Tactics.VerdiTactics.
 Require Crypto.Encoding.PointEncodingPre.
-Obligation Tactic := eauto using PointEncodingPre.point_encoding_canonical.
+Obligation Tactic := eauto; exact PointEncodingPre.point_encoding_canonical.
 
-Require Import Crypto.Spec.Encoding Crypto.Spec.ModularArithmetic.
-Require Import Crypto.Spec.CompleteEdwardsCurve.
+Require Import Crypto.Spec.Encoding Crypto.Spec.ModularWordEncoding.
+Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.Spec.ModularArithmetic.
 
 Local Open Scope F_scope.
 
 Section PointEncoding.
-  Context {prm: CompleteEdwardsCurve.TwistedEdwardsParams} {sz : nat}
-   {FqEncoding : encoding of ModularArithmetic.F (CompleteEdwardsCurve.q) as Word.word sz}.
-
-  Definition sign_bit (x : F CompleteEdwardsCurve.q) :=
-    match (enc x) with
-      | Word.WO => false
-      | Word.WS b _ w' => b
-    end.
+  Context {prm: TwistedEdwardsParams} {sz : nat} {sz_nonzero : (0 < sz)%nat}
+   {bound_check : (BinInt.Z.to_nat q < NPeano.Nat.pow 2 sz)%nat} {q_5mod8 : (q mod 8 = 5)%Z}
+   {sqrt_minus1_valid : (@ZToField q 2 ^ BinInt.Z.to_N (q / 4)) ^ 2 = opp 1}
+   {FqEncoding : encoding of (F q) as (Word.word sz)}
+   {sign_bit : F q -> bool} {sign_bit_zero : sign_bit 0 = false}
+   {sign_bit_opp : forall x, x <> 0 -> negb (sign_bit x) = sign_bit (opp x)}.
+  Existing Instance prime_q.
 
   Definition point_enc (p : E.point) : Word.word (S sz) := let '(x,y) := proj1_sig p in
     Word.WS (sign_bit x) (enc y).
@@ -29,13 +28,20 @@ Section PointEncoding.
   Program Definition point_dec_with_spec :
     {point_dec : Word.word (S sz) -> option E.point
                | forall w x, point_dec w = Some x -> (point_enc x = w)
-               } := PointEncodingPre.point_dec.
-   
+               } := @PointEncodingPre.point_dec _ _ _ sign_bit.
+
   Definition point_dec := Eval hnf in (proj1_sig point_dec_with_spec).
 
+   Definition point_encoding_valid : forall p : E.point, point_dec (point_enc p) = Some p :=
+     @PointEncodingPre.point_encoding_valid _ _ sz_nonzero bound_check q_5mod8 sqrt_minus1_valid _ _ sign_bit_zero sign_bit_opp.
+
+   Definition point_encoding_canonical : forall x_enc x, point_dec x_enc = Some x -> point_enc x = x_enc :=
+     PointEncodingPre.point_encoding_canonical . 
+
   Instance point_encoding : encoding of E.point as (Word.word (S sz)) := {
     enc := point_enc;
     dec := point_dec;
-    encoding_valid := PointEncodingPre.point_encoding_valid
+    encoding_valid := point_encoding_valid;
+    encoding_canonical := point_encoding_canonical
   }.
 End PointEncoding.
\ No newline at end of file
diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v
index 320200218..d14e8ea30 100644
--- a/src/Specific/Ed25519.v
+++ b/src/Specific/Ed25519.v
@@ -123,7 +123,7 @@ Proof.
     apply weqb_true_iff in Heqb. subst. rewrite encoding_valid in H; discriminate. }
 Qed.
 
-Definition enc' : F q * F q -> word (S (b - 1)).
+Definition enc' : F q * F q -> word b.
 Proof.
   intro x.
   let enc' := (eval hnf in (@enc (@E.point curve25519params) _ _)) in
@@ -296,7 +296,7 @@ Proof.
   { do 2 (eapply option_rect_Proper_nd; [intro|reflexivity..]).
     symmetry; apply decode_test_encode_test.
   } Unfocus.
-
+  
   rewrite enc'_correct.
   cbv [unExtendedPoint unifiedAddM1 negateExtended scalarMultM1].
   (* Why does this take too long?
@@ -349,7 +349,7 @@ Proof.
     reflexivity. }
   Unfocus.
 
-  cbv iota beta delta [point_dec_coordinates sign_bit dec FqEncoding modular_word_encoding E.solve_for_x2 sqrt_mod_q].
+  cbv iota beta delta [point_dec_coordinates ModularWordEncodingTheorems.sign_bit dec FqEncoding modular_word_encoding E.solve_for_x2 sqrt_mod_q].
 
   etransitivity.
   Focus 2. {