implement X25519

4 files changed, 74 insertions, 13 deletions

diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v
index 86c075e19..20208924d 100644
--- a/src/Experiments/Ed25519.v
+++ b/src/Experiments/Ed25519.v
@@ -2,6 +2,7 @@ Require Import Coq.omega.Omega.
 Require Import Coq.Lists.List.
 Import ListNotations.
 Require Import Crypto.EdDSARepChange.
+Require Import Crypto.MxDHRepChange. Import MxDH.
 Require Import Crypto.Spec.Ed25519.
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.ListUtil.
@@ -879,6 +880,7 @@ Proof.
   apply dec_bool.
   vm_cast_no_check (eq_refl true).
 (* Time Qed. (* Finished transaction in 1646.167 secs (1645.753u,0.339s) (successful) *) *)
+Admitted.
 
 Definition sign := @EdDSARepChange.sign E
          (@CompleteEdwardsCurveTheorems.E.eq Fq (@eq Fq) (@ModularArithmetic.F.one q)
@@ -1478,5 +1480,60 @@ Let verify_correct :
       (* SRepDec := *) SRepDec
       (* SRepDec_correct := *) SRepDec_correct
 .
-Let both_correct := (@sign_correct, @verify_correct).
-Print Assumptions both_correct.
\ No newline at end of file
+
+Lemma Fhomom_inv_zero :
+  GF25519BoundedCommon.eq
+    (GF25519BoundedCommon.encode
+       (@ModularArithmetic.F.inv GF25519.modulus
+                                 (ModularArithmetic.F.of_Z GF25519.modulus 0)))
+    (GF25519Bounded.inv GF25519BoundedCommon.zero).
+Proof.
+  vm_decide_no_check.
+Qed.
+
+Import ModularArithmetic.
+Module Spec.
+  Module X25519.
+    Definition a : F q := F.of_Z _ 486662.
+    Definition a24 : F q := ((a - F.of_Z _ 2) / F.of_Z _ 4)%F.
+  End X25519.
+End Spec.
+
+Section X25519Constants.
+  Import GF25519BoundedCommon.
+  Definition a24' : GF25519BoundedCommon.fe25519 :=
+    Eval vm_compute in GF25519BoundedCommon.encode Spec.X25519.a24.
+  Definition a24 : GF25519BoundedCommon.fe25519 :=
+    Eval cbv [a24' fe25519_word64ize word64ize andb opt.word64ToZ opt.word64ize opt.Zleb Z.compare CompOpp Pos.compare Pos.compare_cont] in (fe25519_word64ize a24').
+  Lemma a24_correct : GF25519BoundedCommon.eq
+                        (GF25519BoundedCommon.encode Spec.X25519.a24)
+                        (a24).
+  Proof. vm_decide_no_check. Qed.
+End X25519Constants.
+  
+Definition x25519 (n:N) (x:GF25519BoundedCommon.fe25519) : GF25519BoundedCommon.fe25519 :=
+  @MxDH.montladder GF25519BoundedCommon.fe25519 GF25519BoundedCommon.zero
+                   GF25519BoundedCommon.one GF25519Bounded.add GF25519Bounded.sub
+                   GF25519Bounded.mul GF25519Bounded.inv a24
+                   (fun (H : bool)
+                        (H0
+                           H1 : GF25519BoundedCommon.fe25519 * GF25519BoundedCommon.fe25519)
+                    => if H then (H1, H0) else (H0, H1)) 255 (N.testbit_nat n) x.
+
+Definition x25519_correct' n x :
+  GF25519BoundedCommon.eq
+    (GF25519BoundedCommon.encode (MxDH.montladder 255 (N.testbit_nat n) x))
+    (MxDH.montladder 255 (N.testbit_nat n) (GF25519BoundedCommon.encode x)) :=
+  MxDHRepChange
+      (field:=PrimeFieldTheorems.F.field_modulo GF25519.modulus)
+      (impl_field:=GF25519Bounded.field25519)
+      (homomorphism_inv_zero:=Fhomom_inv_zero)
+      (homomorphism_a24:=a24_correct)
+      (Fcswap_correct:= fun _ _ _ => (reflexivity _))
+      (Kcswap_correct:= fun _ _ _ => (reflexivity _))
+      (tb2_correct:=fun _ => (reflexivity _))
+      255 _.
+
+Print Assumptions x25519_correct'.
+Let three_correct := (@sign_correct, @verify_correct, x25519_correct').
+Print Assumptions three_correct.
\ No newline at end of file
diff --git a/src/Experiments/Ed25519Extraction.v b/src/Experiments/Ed25519Extraction.v
index 47cf4f791..20a76f17f 100644
--- a/src/Experiments/Ed25519Extraction.v
+++ b/src/Experiments/Ed25519Extraction.v
@@ -292,4 +292,8 @@ Extraction "src/Experiments/Ed25519_noimports.hs" Ed25519.sign (* Ed25519.verify
 True
 *Ed25519 Prelude> eRepEnc ((sRepERepMul l eRepB) `erepAdd` eRepB) == eRepEnc eRepB
 True
-*)
\ No newline at end of file
+*)
+
+Import Crypto.Spec.MxDH.
+Extraction Inline MxDH.ladderstep MxDH.montladder.
+Extraction "src/Experiments/X25519_noimports.hs" Crypto.Experiments.Ed25519.x25519.
\ No newline at end of file
diff --git a/src/Spec/MxDH.v b/src/Spec/MxDH.v
index d637836e4..0829c46f7 100644
--- a/src/Spec/MxDH.v
+++ b/src/Spec/MxDH.v
@@ -44,7 +44,7 @@ Module MxDH. (* from RFC7748 *)
           ((X4, Z4), (X5, Z5))
         end.
 
-    Context {S:Type} {testbit:S->nat->bool} {cswap:bool->F*F->F*F->(F*F)*(F*F)}.
+    Context {cswap:bool->F*F->F*F->(F*F)*(F*F)}.
 
     Fixpoint downto_iter (i:nat) : list nat :=
       match i with
@@ -59,22 +59,22 @@ Module MxDH. (* from RFC7748 *)
 
     (* Ideally, we would verify that this corresponds to x coordinate
     multiplication *)
-    Definition montladder bound (s:S) (u:F) :=
-      let '(_, _, P1, P2, swap) :=
+    Definition montladder bound (testbit:nat->bool) (u:F) :=
+      let '(P1, P2, swap) :=
           downto
-            (s, u, (1, 0), (u, 1), false)
+            ((1, 0), (u, 1), false)
             bound
             (fun state i =>
-               let '(s, x, P1, P2, swap) := state in
-               let s_i := testbit s i in
+               let '(P1, P2, swap) := state in
+               let s_i := testbit i in
                let swap := xor swap s_i in
                let '(P1, P2) := cswap swap P1 P2 in
                let swap := s_i in
-               let '(P1, P2) := ladderstep x P1 P2 in
-               (s, x, P1, P2, swap)
+               let '(P1, P2) := ladderstep u P1 P2 in
+               (P1, P2, swap)
             ) in
       let '((x, z), _) := cswap swap P1 P2 in
-      x/z.
+      x * Finv z.
   End MontgomeryLadderKeyExchange.
 End MxDH.
 
diff --git a/src/Test/Curve25519SpecTestVectors.v b/src/Test/Curve25519SpecTestVectors.v
index 511998d48..15ca468c1 100644
--- a/src/Test/Curve25519SpecTestVectors.v
+++ b/src/Test/Curve25519SpecTestVectors.v
@@ -6,7 +6,7 @@ Definition F := F (2^255 - 19).
 Definition a : F := F.of_Z _ 486662.
 Definition a24 : F := ((a - F.of_Z _ 2) / F.of_Z _ 4)%F.
 Definition cswap {T} (swap:bool) (a b:T) := if swap then (b, a) else (a, b).
-Definition monty : BinNums.N -> F -> F := @MxDH.montladder F F.zero F.one F.add F.sub F.mul F.div a24 BinNums.N BinNat.N.testbit_nat cswap 255.
+Definition monty s : F -> F := @MxDH.montladder F F.zero F.one F.add F.sub F.mul F.inv a24 cswap 255 (BinNat.N.testbit_nat s).
 
 Example one_basepoint : F.to_Z (monty 1 (F.of_Z _ 9)) = 9%Z.
 Proof. vm_decide_no_check. Qed.