Not quite done with WordUtil lemmas.

1 files changed, 96 insertions, 13 deletions

diff --git a/src/Encoding/PointEncoding.v b/src/Encoding/PointEncoding.v
index b005ce3df..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.
@@ -15,7 +15,7 @@ Require Crypto.Encoding.PointEncodingPre.
    Eenc := encode_point
    Proper_Eenc := Proper_encode_point
    Edec := Fdecode_point (notation)
-   eq_enc_E_iff := Fdecode_encode_iff
+   eq_enc_E_iff := encode_point_decode_point_iff
    EToRep := point_phi
    Ahomom := point_phi_homomorphism
    ERepEnc := Kencode_point
@@ -27,16 +27,19 @@ Require Crypto.Encoding.PointEncodingPre.
 
 Section PointEncoding.
   Context {b : nat} {m : Z} {Fa Fd : F m} {prime_m : Znumtheory.prime m}
+          {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.
@@ -68,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}.
 
@@ -122,7 +124,8 @@ Section PointEncoding.
                 option_eq Keq (option_map phi (Fdecode w)) (Kdec w)}.
     Context {Fsqrt : F m -> F m}
             {phi_sqrt : forall x, Keq (phi (Fsqrt x)) (Ksqrt (phi x))}
-            {Fsqrt_square : forall x root, eq x (F.mul root root) -> eq (Fsqrt x) root}.
+            {Fsqrt_square : forall x root, eq x (F.mul root root) ->
+                                        eq (F.mul (Fsqrt x) (Fsqrt x)) x}.
 
     Lemma point_phi_homomorphism: @Algebra.Monoid.is_homomorphism
                                     Fpoint E.eq Fpoint_add
@@ -133,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).
@@ -146,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.
@@ -157,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.
 
 
@@ -172,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))
@@ -194,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).
@@ -434,6 +441,82 @@ Section PointEncoding.
       + intros. apply Kpoint_from_xy_correct.
     Qed.
 
+    Lemma sign_zero : forall x, x = F.zero -> sign x = false.
+    Proof.
+      intros; subst.
+      reflexivity.
+    Qed.
+
+    Lemma sign_negb : forall x : F m, x <> F.zero ->
+                                      negb (sign x) = sign (F.opp x).
+    Proof.
+      intros.
+      cbv [sign].
+      rewrite !Z.bit0_odd.
+      rewrite F.to_Z_opp.
+      rewrite F.eq_to_Z_iff in H.
+      replace (@F.to_Z m F.zero) with 0%Z in H by reflexivity.
+      rewrite Z.mod_opp_l_nz by (solve [ZUtil.Z.prime_bound] ||
+                                   rewrite F.mod_to_Z; auto).
+      rewrite F.mod_to_Z.
+      rewrite Z.odd_sub.
+      destruct (ZUtil.Z.prime_odd_or_2 m prime_m) as [? | m_odd];
+        [ omega | rewrite m_odd].
+      rewrite <-Bool.xorb_true_l; auto.
+    Qed.
+
+    Lemma Eeq_point_eq : forall x y : option E.point,
+        option_eq E.eq x y <->
+        option_eq
+          (@PointEncodingPre.point_eq _ eq F.one F.add F.mul Fa Fd) x y.
+    Proof.
+      intros.
+      cbv [option_eq E.eq PointEncodingPre.point_eq
+                     PointEncodingPre.prod_eq]; repeat break_match;
+        try reflexivity.
+      cbv [E.coordinates].
+      subst.
+      rewrite Heqp1, Heqp0.
+      cbv [Tuple.fieldwise Tuple.fieldwise' fst snd].
+      tauto.
+    Qed.
+    
+    Lemma enc_canonical_equiv : forall (x_enc : word b) (x : F m),
+      option_eq eq (Fdecode x_enc) (Some x) ->
+      Fencode x = x_enc.
+    Proof.
+      intros.
+      cbv [option_eq] in *.
+      break_match; try discriminate.
+      subst.
+      apply (@Encoding.encoding_canonical _ _ Fencoding).
+      auto.
+    Qed.
+
+    Lemma encode_point_decode_point_iff : forall P_ P,
+      encode_point P = P_ <->
+      Option.option_eq E.eq (Fdecode_point P_) (Some P).
+    Proof.
+      pose proof (@PointEncodingPre.point_encoding_canonical
+                    _ eq F.zero F.one F.opp F.add F.sub F.mul F.div
+                    _ Fa Fd _ Fsqrt Fencoding enc_canonical_equiv
+                    sign sign_zero sign_negb
+                 ) as Hcanonical.
+      let A := fresh "H" in
+      match type of Hcanonical with
+        ?P -> _ => assert P as A by congruence;
+                     specialize (Hcanonical A); clear A end.
+      intros.
+      rewrite Eeq_point_eq.
+      split; intros; subst.
+      { apply PointEncodingPre.point_encoding_valid;
+          auto using sign_zero, sign_negb;
+          congruence. }
+      { apply Hcanonical.
+        cbv [option_eq PointEncodingPre.point_eq PointEncodingPre.prod_eq] in H |- *.
+        break_match; congruence. }
+    Qed.
+
   End RepChange.
 
 End PointEncoding.