put EdDSA encoding sign bit at the MSB

5 files changed, 59 insertions, 33 deletions

diff --git a/src/Encoding/PointEncoding.v b/src/Encoding/PointEncoding.v
index f2139ff28..1160ed83a 100644
--- a/src/Encoding/PointEncoding.v
+++ b/src/Encoding/PointEncoding.v
@@ -3,7 +3,7 @@ Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
 Require Import Crypto.Spec.CompleteEdwardsCurve.
 Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
-Require Import Bedrock.Word.
+Require Import Bedrock.Word Crypto.Util.WordUtil.
 Require Import Crypto.Tactics.VerdiTactics.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.NatUtil.
@@ -30,14 +30,16 @@ Section PointEncoding.
           {two_lt_m : (2 < m)%Z}
           {bound_check : (Z.to_nat m < 2 ^ b)%nat}.
 
-  Definition sign (x : F m) : bool := Z.testbit (F.to_Z x) 0.
+  Local Infix "++" := Word.combine.
+  Local Notation bit b := (Word.WS b Word.WO : Word.word 1).
 
+  Definition sign (x : F m) : bool := Z.testbit (F.to_Z x) 0.
   Definition Fencode (x : F m) : word b := NToWord b (Z.to_N (F.to_Z x)).
 
   Let Fpoint := @E.point (F m) Logic.eq F.one F.add F.mul Fa Fd.
 
   Definition encode_point (P : Fpoint) :=
-    let '(x,y) := E.coordinates P in WS (sign x) (Fencode y).
+    let '(x,y) := E.coordinates P in Fencode y ++ bit (sign x).
 
   Import Morphisms.
   Lemma Proper_encode_point : Proper (E.eq ==> Logic.eq) encode_point.
@@ -69,7 +71,6 @@ Section PointEncoding.
             {Kcoord_to_point : @E.point K Keq Kone Kadd Kmul Ka Kd  -> Kpoint}
             {Kpoint_to_coord : Kpoint -> (K * K)}.
     Context {Kp2c_c2p : forall pt : E.point, Tuple.fieldwise (n := 2) Keq (Kpoint_to_coord (Kcoord_to_point pt)) (E.coordinates pt)}.
-        Check Kp2c_c2p.
     Context {Kpoint_eq : Kpoint -> Kpoint -> Prop} {Kpoint_add : Kpoint -> Kpoint -> Kpoint}.
     Context {Kpoint_eq_correct : forall p q, Kpoint_eq p q <-> Tuple.fieldwise (n := 2) Keq (Kpoint_to_coord p) (Kpoint_to_coord q)} {Kpoint_eq_Equivalence : Equivalence Kpoint_eq}.
 
@@ -135,7 +136,7 @@ Section PointEncoding.
     Qed.
 
     Definition Kencode_point (P : Kpoint) :=
-      let '(x,y) := Kpoint_to_coord P in WS (Ksign x) (Kenc y).
+      let '(x,y) := Kpoint_to_coord P in (Kenc y) ++ bit (Ksign x).
 
     Lemma Kencode_point_correct : forall P : Fpoint,
         encode_point P = Kencode_point (point_phi P).
@@ -148,7 +149,9 @@ Section PointEncoding.
       pose proof (Kp2c_c2p x) as A; rewrite Heqp in A;
         inversion A; cbv [fst snd Tuple.fieldwise'] in * end.
       cbv [E.coordinates E.ref_phi proj1_sig] in *.
-      f_equal; rewrite ?H0, ?H1; auto.
+      apply (f_equal2 (fun a b => a ++ b));
+        try apply (f_equal2 (fun a b => WS a b));
+        rewrite ?H0, ?H1; auto.
     Qed.
 
     Lemma Proper_Kencode_point : Proper (Kpoint_eq ==> Logic.eq) Kencode_point.
@@ -159,7 +162,9 @@ Section PointEncoding.
       destruct (Kpoint_to_coord x).
       destruct (Kpoint_to_coord y).
       simpl in H; destruct H.
-      f_equal; auto.
+      apply (f_equal2 (fun a b => a ++ b));
+        try apply (f_equal2 (fun a b => WS a b));
+        rewrite ?H0, ?H1; auto.
     Qed.
 
 
@@ -174,11 +179,11 @@ Section PointEncoding.
           else Some p
       else None.
 
-    Definition Kdecode_coordinates (w : word (S b)) : option (K * K) :=
+    Definition Kdecode_coordinates (w : word (b + 1)) : option (K * K) :=
       option_rect (fun _ => option (K * K))
-                  (Kcoordinates_from_y (whd w))
+                  (Kcoordinates_from_y (wlast w))
                   None
-                  (Kdec (wtl w)).
+                  (Kdec (winit w)).
 
     Lemma onCurve_eq : forall x y,
       Keq (Kadd (Kmul Ka (Kmul x x)) (Kmul y y))
@@ -196,7 +201,7 @@ Section PointEncoding.
         | right _ => None
       end.
 
-    Definition Kdecode_point (w : word (S b)) : option Kpoint :=
+    Definition Kdecode_point (w : word (b+1)) : option Kpoint :=
       option_rect (fun _ => option Kpoint) Kpoint_from_xy None (Kdecode_coordinates w).
 
     Definition Fencoding : Encoding.CanonicalEncoding (F m) (word b).
diff --git a/src/Encoding/PointEncodingPre.v b/src/Encoding/PointEncodingPre.v
index 71b239698..8a0d4c849 100644
--- a/src/Encoding/PointEncodingPre.v
+++ b/src/Encoding/PointEncodingPre.v
@@ -3,7 +3,7 @@ Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Coq.Program.Equality.
 Require Import Crypto.CompleteEdwardsCurve.Pre.
 Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
-Require Import Bedrock.Word.
+Require Import Bedrock.Word Crypto.Util.WordUtil.
 Require Import Crypto.Encoding.ModularWordEncodingTheorems.
 Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Algebra.
@@ -39,7 +39,6 @@ Section PointEncodingPre.
   Local Notation point := (@E.point F eq one add mul a d).
   Local Notation onCurve := (@onCurve F eq one add mul a d).
   Local Notation solve_for_x2 := (@E.solve_for_x2 F one sub mul div a d).
-  Check PrimeFieldTheorems.F.sqrt_5mod8_correct.
 
   Context {sz : nat} (sz_nonzero : (0 < sz)%nat).
   Context {sqrt : F -> F} {Proper_sqrt : Proper (eq ==>eq) sqrt}
@@ -92,10 +91,10 @@ Section PointEncodingPre.
     apply E.solve_correct; eassumption.
   Qed.
 
-  Definition point_enc_coordinates (p : (F * F)) : Word.word (S sz) := let '(x,y) := p in
-    Word.WS (sign_bit x) (enc y).
+  Definition point_enc_coordinates (p : (F * F)) : Word.word (sz+1) := let '(x,y) := p in
+    combine (enc y) (WS (sign_bit x) WO).
 
-  Let point_enc (p : point) : Word.word (S sz) := point_enc_coordinates (E.coordinates p).
+  Let point_enc (p : point) : Word.word (sz+1) := point_enc_coordinates (E.coordinates p).
 
   Definition coord_from_y sign (y : F) : option (F * F) :=
     let x2 := solve_for_x2 y in
@@ -108,8 +107,8 @@ Section PointEncodingPre.
         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 point_dec_coordinates (w : word (sz+1)) : option (F * F) :=
+    option_rect (fun _ => _) (coord_from_y (wlast w)) None (dec (winit 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
@@ -247,9 +246,13 @@ Section PointEncodingPre.
       | right _ => None
     end.
 
-  Definition point_dec (w : word (S sz)) : option point :=
+  Definition point_dec (w : word (sz+1)) : option point :=
     option_rect (fun _ => option point) point_from_xy None (point_dec_coordinates w).
 
+  Lemma bool_neq_negb x y : x <> y <-> x = negb y.
+    destruct x, y; split; (discriminate||tauto).
+  Qed.
+
   Lemma point_coordinates_encoding_canonical : forall w p,
     option_eq (Tuple.fieldwise (n := 2) eq) (point_dec_coordinates w) (Some p) ->
     point_enc_coordinates p = w.
@@ -279,15 +282,19 @@ Section PointEncodingPre.
                             Bool.eq_true_not_negb,
                             Bool.not_false_is_true, encoding_canonical]
            end;
-      try solve [apply enc_canonical_equiv; rewrite Heqo; auto];
+      rewrite combine_winit_wlast; split;
+        try apply (f_equal2 (fun a b => WS a b));
+        try solve
+            [ trivial
+            | apply enc_canonical_equiv; rewrite Heqo; auto];
         erewrite <-sign_bit_subst by eassumption.
-    { rewrite <-sign_bit_opp
-        by (intro A; apply F_eqb_iff in A; congruence).
-      auto using Bool.eq_true_not_negb. }
-    { rewrite <-sign_bit_opp
-        by (intro A; apply sign_bit_zero in A; congruence).
-      apply Bool.negb_false_iff, Bool.not_false_is_true.
-      auto. }
+    { intuition. }
+    { apply bool_neq_negb in Heqb0. rewrite <-sign_bit_opp.
+      { congruence. }
+      { rewrite Bool.andb_false_iff in *.
+        unfold not; intro Hx; destruct Heqb;
+          [apply F_eqb_iff in Hx; congruence
+          |rewrite (sign_bit_zero _ Hx) in *; simpl negb in *; congruence]. } }
   Qed.
 
   Lemma inversion_point_dec : forall w x,
@@ -311,9 +318,11 @@ Section PointEncodingPre.
     auto using inversion_point_dec.
   Qed.
 
-  Lemma y_decode : forall p, dec (wtl (point_enc_coordinates p)) = Some (snd p).
+
+  Lemma y_decode : forall p, dec (winit (point_enc_coordinates p)) = Some (snd p).
   Proof.
     intros; destruct p. cbv [point_enc_coordinates wtl snd].
+    rewrite winit_combine.
     exact (encoding_valid _).
   Qed.
 
@@ -372,6 +381,7 @@ Section PointEncodingPre.
       rewrite zero_square in *.
       assert (sqrt (solve_for_x2 y) == 0) by (rewrite solve_correct; tauto).
       rewrite !sign_bit_zero by (tauto || eauto).
+      rewrite wlast_combine.
       rewrite Bool.andb_false_r, Bool.eqb_reflx.
       apply option_coordinates_eq_iff; split; try reflexivity.
       etransitivity; eauto.
@@ -388,6 +398,7 @@ Section PointEncodingPre.
         rewrite H0, zero_square in sqrt_square.
         rewrite Ring.zero_product_iff_zero_factor in sqrt_square.
         tauto. } Unfocus.
+      rewrite wlast_combine.
       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;
diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v
index 36af82937..56d8112bd 100644
--- a/src/Experiments/Ed25519.v
+++ b/src/Experiments/Ed25519.v
@@ -1357,7 +1357,7 @@ Lemma eq_enc_E_iff : forall (P_ : Word.word b) (P : E),
  Option.option_eq CompleteEdwardsCurveTheorems.E.eq (Edec P_) (Some P).
 Proof.
   cbv [Eenc].
-  eapply @PointEncoding.encode_point_decode_point_iff; try (exact iff_equivalence || exact curve_params); [].
+  eapply (@PointEncoding.encode_point_decode_point_iff (b-1)); try (exact iff_equivalence || exact curve_params); [].
   intros.
   apply (@PrimeFieldTheorems.F.sqrt_5mod8_correct GF25519.modulus _ eq_refl Fsqrt_minus1 Fsqrt_minus1_correct).
   eexists.
@@ -1397,7 +1397,7 @@ Let verify_correct :
       (* Eenc := *) Eenc
       (* Senc := *) Senc
       (* prm := *) ed25519
-      (* Proper_Eenc := *) PointEncoding.Proper_encode_point
+      (* Proper_Eenc := *) (PointEncoding.Proper_encode_point (b:=b-1))
       (* Edec := *) Edec
       (* eq_enc_E_iff := *) eq_enc_E_iff
       (* Sdec := *) Sdec
diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v
index a8e95cf9d..d6873607f 100644
--- a/src/Spec/Ed25519.v
+++ b/src/Spec/Ed25519.v
@@ -61,12 +61,15 @@ Section Ed25519.
     (F.of_Z q 15112221349535400772501151409588531511454012693041857206046113283949847762202,
      F.of_Z q 4 / F.of_Z q 5).
 
-  Definition Fencode {b : nat} {m} : F m -> Word.word b :=
+  Local Infix "++" := Word.combine.
+  Local Notation bit b := (Word.WS b Word.WO : Word.word 1).
+
+  Definition Fencode {len} {m} : F m -> Word.word len :=
     fun x : F m => (Word.NToWord _ (BinIntDef.Z.to_N (F.to_Z x))).
   Definition sign (x : F q) : bool := BinIntDef.Z.testbit (F.to_Z x) 0.
   Definition Eenc : E -> Word.word b := fun P =>
-    let '(x,y) := E.coordinates P in Word.WS (sign x) (Fencode y).
-  Definition Senc : Fl -> Word.word b := Fencode.
+    let '(x,y) := E.coordinates P in Fencode (len:=b-1) y ++ bit (sign x).
+  Definition Senc : Fl -> Word.word b := Fencode (len:=b).
 
   (* TODO(andreser): prove this after we have fast scalar multplication *)
   Axiom B_order_l : CompleteEdwardsCurveTheorems.E.eq (BinInt.Z.to_nat l * B)%E E.zero.
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
index fd2e5e098..7a856f1e9 100644
--- a/src/Util/WordUtil.v
+++ b/src/Util/WordUtil.v
@@ -311,3 +311,10 @@ Proof.
 Admitted.
 Hint Rewrite @wordToN_wor using word_util_arith : push_wordToN.
 Hint Rewrite <- @wordToN_wor using word_util_arith : pull_wordToN.
+
+Axiom wlast : forall sz, word (sz+1) -> bool. Arguments wlast {_} _.
+Axiom winit : forall sz, word (sz+1) -> word sz. Arguments winit {_} _.
+Axiom combine_winit_wlast : forall {sz} a b (c:word (sz+1)),
+    @combine sz a 1 b = c <-> a = winit c /\ b = (WS (wlast c) WO).
+Axiom winit_combine : forall sz a b, @winit sz (combine a b) = a.
+Axiom wlast_combine : forall sz a b, @wlast sz (combine a (WS b WO)) = b.
\ No newline at end of file