From 728f19637d39edd1c3ec93a5278159778c55b4e5 Mon Sep 17 00:00:00 2001
From: Brian W Bush <code@functionally.io>
Date: Sun, 29 Dec 2024 13:12:58 -0700
Subject: [PATCH 1/3] Implemented mapping to curve via try and increment.

---
 src/Crypto.lean                        |  6 +++
 src/Crypto/EllipticCurve.lean          |  7 ++-
 src/Crypto/EllipticCurve/HTC.lean      | 32 ++++++++++++
 src/Crypto/EllipticCurve/HTC/Test.lean | 71 ++++++++++++++++++++++++++
 src/Crypto/EllipticCurve/VRF.lean      |  7 +++
 src/Crypto/Field.lean                  |  8 +++
 src/Crypto/Field/Fp.lean               | 20 ++++++++
 7 files changed, 149 insertions(+), 2 deletions(-)
 create mode 100644 src/Crypto/EllipticCurve/HTC.lean
 create mode 100644 src/Crypto/EllipticCurve/HTC/Test.lean
 create mode 100644 src/Crypto/EllipticCurve/VRF.lean
 create mode 100644 src/Crypto/Field.lean

diff --git a/src/Crypto.lean b/src/Crypto.lean
index b7e33bc..11c10a6 100644
--- a/src/Crypto.lean
+++ b/src/Crypto.lean
@@ -1,4 +1,5 @@
 
+import Crypto.Field
 import Crypto.Field.Fp
 import Crypto.Field.Fp.Test
 
@@ -20,12 +21,17 @@ import Crypto.EllipticCurve.ECDSA.Test
 import Crypto.EllipticCurve.ECIES
 import Crypto.EllipticCurve.ECIES.Test
 
+import Crypto.EllipticCurve.HTC
+import Crypto.EllipticCurve.HTC.Test
+
 import Crypto.EllipticCurve.Schnorr
 import Crypto.EllipticCurve.Schnorr.Test
 
 import Crypto.EllipticCurve.TSS
 import Crypto.EllipticCurve.TSS.Test
 
+import Crypto.EllipticCurve.VRF
+
 import Crypto.Hash
 import Crypto.Hash.Test
 
diff --git a/src/Crypto/EllipticCurve.lean b/src/Crypto/EllipticCurve.lean
index e7ea94c..8114458 100644
--- a/src/Crypto/EllipticCurve.lean
+++ b/src/Crypto/EllipticCurve.lean
@@ -33,6 +33,9 @@ namespace EllipticCurve
   def wellFormed' (ec : EllipticCurve F) : Bool :=
     4 * ec.a^3 + 27 * ec.b^2 != 0
 
+  def residue (ec : EllipticCurve F) (x : F) : F :=
+    x^3 + ec.a * x + ec.b
+
 
   inductive Point (ec : EllipticCurve F) where
   | mk : F → F → Point ec
@@ -54,11 +57,11 @@ namespace EllipticCurve
 
     def onCurve : Point (ec : EllipticCurve F) → Prop
     | Point.infinity => True
-    | Point.mk x y => y^2 = x^3 + ec.a * x + ec.b
+    | Point.mk x y => y^2 = residue ec x
 
     def onCurve' : Point (ec : EllipticCurve F) → Bool
     | Point.infinity => true
-    | Point.mk x y => y^2 == x^3 + ec.a * x + ec.b
+    | Point.mk x y => y^2 == residue ec x
 
   end Point
 
diff --git a/src/Crypto/EllipticCurve/HTC.lean b/src/Crypto/EllipticCurve/HTC.lean
new file mode 100644
index 0000000..2b6a9ee
--- /dev/null
+++ b/src/Crypto/EllipticCurve/HTC.lean
@@ -0,0 +1,32 @@
+import Crypto.EllipticCurve
+import Crypto.Field
+
+open Crypto.Field
+
+
+namespace Crypto.EllipticCurve.HTC
+
+
+variable {ec : EllipticCurve F}
+
+[∀ i, OfNat F i]
+[DecidableEq F]
+[Add F]
+[Mul F]
+[Pow F Nat]
+[Sqrt F]
+
+
+namespace MapToCurve
+
+  partial def tryAndIncrement (x : F) : Point ec :=
+    let y2 : F := residue ec x
+    let y : F := Sqrt.sqrt y2
+    if y^2 = y2
+      then Point.mk x y
+      else tryAndIncrement (x + 1)
+
+end MapToCurve
+
+
+end Crypto.EllipticCurve.HTC
diff --git a/src/Crypto/EllipticCurve/HTC/Test.lean b/src/Crypto/EllipticCurve/HTC/Test.lean
new file mode 100644
index 0000000..ec52b01
--- /dev/null
+++ b/src/Crypto/EllipticCurve/HTC/Test.lean
@@ -0,0 +1,71 @@
+import Crypto.EllipticCurve
+import Crypto.EllipticCurve.HTC
+import Crypto.EllipticCurve.SECG.Secp256k1
+import Crypto.Field.Fp
+import LSpec
+
+open Crypto
+open Crypto.EllipticCurve.HTC
+open Crypto.Field
+open LSpec
+
+
+namespace Crypto.EllipticCurve.HTC.Test
+
+
+-- https://asecuritysite.com/hash/hash_to_ecc
+
+abbrev p1 := 43
+abbrev F1 := Fp p1
+def hasSqrt1 : Fp.Is3Mod4 p1 := rfl
+instance iSqrt1 : Sqrt F1 := Fp.iSqrt3Mod4 hasSqrt1
+def ec1 : EllipticCurve (Fp p1) := ⟨ 0, 7 ⟩
+
+abbrev p2 := 10099
+abbrev F2 := Fp p2
+def hasSqrt2 : Fp.Is3Mod4 p2 := rfl
+instance iSqrt2 : Sqrt F2 := Fp.iSqrt3Mod4 hasSqrt2
+def ec2 : EllipticCurve (Fp p2) := ⟨ 0, 7 ⟩
+
+abbrev p := Secp256k1.p
+abbrev F := Secp256k1.F
+theorem hasSqrt : Fp.Is3Mod4 p := rfl
+instance iSqrt : Sqrt F := Fp.iSqrt3Mod4 hasSqrt
+def ec := Secp256k1.curve
+
+instance : SlimCheck.Shrinkable F where
+  shrink _ := []
+
+instance : SlimCheck.SampleableExt F :=
+  SlimCheck.SampleableExt.mkSelfContained
+    $ do
+      let x ← (Fp.randFp : Rand F)
+      pure x
+
+#lspec group "Map to point"
+  $ group "tryAndIncrement"
+    (
+      test "y^2=x^3+7, p = 43, x = 10" (
+        let expected : EllipticCurve.Point ec1 := EllipticCurve.Point.mk 12 31
+        MapToCurve.tryAndIncrement 10 = expected
+      )
+    $ test "y^2=x^3+7, p = 43, x = 12" (
+        let expected : EllipticCurve.Point ec1 := EllipticCurve.Point.mk 12 31
+        MapToCurve.tryAndIncrement 12 = expected
+      )
+    $ test "y^2=x^3+7, p = 10099, x = 1032" (
+        let expected : EllipticCurve.Point ec2 := EllipticCurve.Point.mk 1036 1112
+        MapToCurve.tryAndIncrement 1032 = expected
+      )
+    $ test "y^2=x^3+7, p = 10099, x = 1030" (
+        let expected : EllipticCurve.Point ec2 := EllipticCurve.Point.mk 1036 1112
+        MapToCurve.tryAndIncrement 1032 = expected
+      )
+    $ check "On curve" (
+        ∀ x : F,
+        let actual : EllipticCurve.Point ec := MapToCurve.tryAndIncrement x
+        EllipticCurve.Point.onCurve' actual
+      )
+    )
+
+end Crypto.EllipticCurve.HTC.Test
diff --git a/src/Crypto/EllipticCurve/VRF.lean b/src/Crypto/EllipticCurve/VRF.lean
new file mode 100644
index 0000000..3f5f07e
--- /dev/null
+++ b/src/Crypto/EllipticCurve/VRF.lean
@@ -0,0 +1,7 @@
+import Crypto.EllipticCurve
+
+
+namespace Crypto.EllipticCurve.VRF
+
+
+end Crypto.EllipticCurve.VRF
diff --git a/src/Crypto/Field.lean b/src/Crypto/Field.lean
new file mode 100644
index 0000000..6d1685c
--- /dev/null
+++ b/src/Crypto/Field.lean
@@ -0,0 +1,8 @@
+namespace Crypto.Field
+
+
+class Sqrt (F : Type) where
+  sqrt : F → F
+
+
+end Crypto.Field
diff --git a/src/Crypto/Field/Fp.lean b/src/Crypto/Field/Fp.lean
index 8cc0b2f..35f694d 100644
--- a/src/Crypto/Field/Fp.lean
+++ b/src/Crypto/Field/Fp.lean
@@ -1,3 +1,4 @@
+import Crypto.Field
 import Mathlib.Control.Random
 
 
@@ -135,4 +136,23 @@ instance : HDiv (Fp p) (NonZeroFp p) (Fp p) where
   hDiv x y := x * y.inverse
 
 
+namespace Fp
+
+  def isSquare (x : Fp p) : Prop :=
+    match x^((p - 1) / 2) with
+    | Fp.mkUnsafe 0 => True
+    | Fp.mkUnsafe 1 => True
+    | _             => False
+
+  def Is3Mod4 (p : Nat) : Prop := p % 4 = 3
+
+  -- FIXME: Add a comprehensive set of instances.
+  instance iSqrt3Mod4 {p : Nat} (_ : Fp.Is3Mod4 p) : Sqrt (Fp p) where
+    sqrt (x : Fp p) :=
+      let c1 : Nat := (p + 1) / 4
+      x^c1
+
+end Fp
+
+
 end Crypto.Field

From d0ccb5146373d530644c64d682c33c869402940b Mon Sep 17 00:00:00 2001
From: Brian W Bush <code@functionally.io>
Date: Sun, 29 Dec 2024 14:21:49 -0700
Subject: [PATCH 2/3] Implemented ECVRF

---
 src/Crypto/EllipticCurve/HTC/Test.lean |  6 ++---
 src/Crypto/EllipticCurve/VRF.lean      | 32 ++++++++++++++++++++++++++
 src/Crypto/Field/Fp.lean               |  2 +-
 3 files changed, 36 insertions(+), 4 deletions(-)

diff --git a/src/Crypto/EllipticCurve/HTC/Test.lean b/src/Crypto/EllipticCurve/HTC/Test.lean
index ec52b01..c881448 100644
--- a/src/Crypto/EllipticCurve/HTC/Test.lean
+++ b/src/Crypto/EllipticCurve/HTC/Test.lean
@@ -18,19 +18,19 @@ namespace Crypto.EllipticCurve.HTC.Test
 abbrev p1 := 43
 abbrev F1 := Fp p1
 def hasSqrt1 : Fp.Is3Mod4 p1 := rfl
-instance iSqrt1 : Sqrt F1 := Fp.iSqrt3Mod4 hasSqrt1
+instance iSqrt1 : Sqrt F1 := Fp.instSqrt3Mod4 hasSqrt1
 def ec1 : EllipticCurve (Fp p1) := ⟨ 0, 7 ⟩
 
 abbrev p2 := 10099
 abbrev F2 := Fp p2
 def hasSqrt2 : Fp.Is3Mod4 p2 := rfl
-instance iSqrt2 : Sqrt F2 := Fp.iSqrt3Mod4 hasSqrt2
+instance iSqrt2 : Sqrt F2 := Fp.instSqrt3Mod4 hasSqrt2
 def ec2 : EllipticCurve (Fp p2) := ⟨ 0, 7 ⟩
 
 abbrev p := Secp256k1.p
 abbrev F := Secp256k1.F
 theorem hasSqrt : Fp.Is3Mod4 p := rfl
-instance iSqrt : Sqrt F := Fp.iSqrt3Mod4 hasSqrt
+instance iSqrt : Sqrt F := Fp.instSqrt3Mod4 hasSqrt
 def ec := Secp256k1.curve
 
 instance : SlimCheck.Shrinkable F where
diff --git a/src/Crypto/EllipticCurve/VRF.lean b/src/Crypto/EllipticCurve/VRF.lean
index 3f5f07e..17c4391 100644
--- a/src/Crypto/EllipticCurve/VRF.lean
+++ b/src/Crypto/EllipticCurve/VRF.lean
@@ -1,7 +1,39 @@
 import Crypto.EllipticCurve
 
+open Crypto.EllipticCurve
+open Crypto.Field
+
 
 namespace Crypto.EllipticCurve.VRF
 
+variable {α : Type}
+variable {p : Nat}
+variable {ec : EllipticCurve (Fp p)}
+
+structure Proof (g : Group ec) where
+  output : Point ec
+  challenge : Fp g.n
+  response : Fp g.n
+deriving Repr, DecidableEq, BEq, Inhabited
+
+variable {g : EllipticCurve.Group ec}
+
+def prove [RandomGen gen] [Monad m] (htc : Point ec → α → Point ec) (commit : Point ec → Point ec → Point ec → Point ec → Fp g.n) (kp : Group.KeyPair g) (x : α) : RandGT gen m (Proof g) :=
+  do
+    let H := htc kp.pub x
+    let Z := kp.prv * H
+    let r ← Random.random
+    let RB := r * g.G
+    let RH := r * g.G
+    let c := commit H Z RB RH
+    let s := r + kp.prv * c
+    pure ⟨ Z , c , s ⟩
+
+def verify (htc : Point ec → α → Point ec) (commit : Point ec → Point ec → Point ec → Point ec → Fp g.n) (pk : Group.PubKey g) (x : α) : Proof g → Bool
+| ⟨ Z , c , s ⟩ => let H := htc pk.pub x
+                   let RB := s * g.G - c * pk.pub
+                   let RH := s * H - c * Z
+                   c = commit H Z RB RH
+
 
 end Crypto.EllipticCurve.VRF
diff --git a/src/Crypto/Field/Fp.lean b/src/Crypto/Field/Fp.lean
index 35f694d..c9a1ffb 100644
--- a/src/Crypto/Field/Fp.lean
+++ b/src/Crypto/Field/Fp.lean
@@ -147,7 +147,7 @@ namespace Fp
   def Is3Mod4 (p : Nat) : Prop := p % 4 = 3
 
   -- FIXME: Add a comprehensive set of instances.
-  instance iSqrt3Mod4 {p : Nat} (_ : Fp.Is3Mod4 p) : Sqrt (Fp p) where
+  instance instSqrt3Mod4 {p : Nat} (_ : Fp.Is3Mod4 p) : Sqrt (Fp p) where
     sqrt (x : Fp p) :=
       let c1 : Nat := (p + 1) / 4
       x^c1

From b2a6e5760104f3fb542306456ade31dbc0fd2beb Mon Sep 17 00:00:00 2001
From: Brian W Bush <code@functionally.io>
Date: Sun, 29 Dec 2024 15:55:05 -0700
Subject: [PATCH 3/3] Tested ECVRF

---
 src/Crypto.lean                        |  1 +
 src/Crypto/EllipticCurve/HTC/Test.lean | 35 ++++++++-------
 src/Crypto/EllipticCurve/VRF.lean      |  2 +-
 src/Crypto/EllipticCurve/VRF/Test.lean | 62 ++++++++++++++++++++++++++
 src/Crypto/Serial.lean                 |  2 +-
 5 files changed, 83 insertions(+), 19 deletions(-)
 create mode 100644 src/Crypto/EllipticCurve/VRF/Test.lean

diff --git a/src/Crypto.lean b/src/Crypto.lean
index 11c10a6..2cc5115 100644
--- a/src/Crypto.lean
+++ b/src/Crypto.lean
@@ -31,6 +31,7 @@ import Crypto.EllipticCurve.TSS
 import Crypto.EllipticCurve.TSS.Test
 
 import Crypto.EllipticCurve.VRF
+import Crypto.EllipticCurve.VRF.Test
 
 import Crypto.Hash
 import Crypto.Hash.Test
diff --git a/src/Crypto/EllipticCurve/HTC/Test.lean b/src/Crypto/EllipticCurve/HTC/Test.lean
index c881448..adf0455 100644
--- a/src/Crypto/EllipticCurve/HTC/Test.lean
+++ b/src/Crypto/EllipticCurve/HTC/Test.lean
@@ -13,8 +13,6 @@ open LSpec
 namespace Crypto.EllipticCurve.HTC.Test
 
 
--- https://asecuritysite.com/hash/hash_to_ecc
-
 abbrev p1 := 43
 abbrev F1 := Fp p1
 def hasSqrt1 : Fp.Is3Mod4 p1 := rfl
@@ -45,21 +43,24 @@ instance : SlimCheck.SampleableExt F :=
 #lspec group "Map to point"
   $ group "tryAndIncrement"
     (
-      test "y^2=x^3+7, p = 43, x = 10" (
-        let expected : EllipticCurve.Point ec1 := EllipticCurve.Point.mk 12 31
-        MapToCurve.tryAndIncrement 10 = expected
-      )
-    $ test "y^2=x^3+7, p = 43, x = 12" (
-        let expected : EllipticCurve.Point ec1 := EllipticCurve.Point.mk 12 31
-        MapToCurve.tryAndIncrement 12 = expected
-      )
-    $ test "y^2=x^3+7, p = 10099, x = 1032" (
-        let expected : EllipticCurve.Point ec2 := EllipticCurve.Point.mk 1036 1112
-        MapToCurve.tryAndIncrement 1032 = expected
-      )
-    $ test "y^2=x^3+7, p = 10099, x = 1030" (
-        let expected : EllipticCurve.Point ec2 := EllipticCurve.Point.mk 1036 1112
-        MapToCurve.tryAndIncrement 1032 = expected
+      group "https://asecuritysite.com/hash/hash_to_ecc"
+      (
+        test "y^2=x^3+7, p = 43, x = 10" (
+          let expected : EllipticCurve.Point ec1 := EllipticCurve.Point.mk 12 31
+          MapToCurve.tryAndIncrement 10 = expected
+        )
+      $ test "y^2=x^3+7, p = 43, x = 12" (
+          let expected : EllipticCurve.Point ec1 := EllipticCurve.Point.mk 12 31
+          MapToCurve.tryAndIncrement 12 = expected
+        )
+      $ test "y^2=x^3+7, p = 10099, x = 1032" (
+          let expected : EllipticCurve.Point ec2 := EllipticCurve.Point.mk 1036 1112
+          MapToCurve.tryAndIncrement 1032 = expected
+        )
+      $ test "y^2=x^3+7, p = 10099, x = 1030" (
+          let expected : EllipticCurve.Point ec2 := EllipticCurve.Point.mk 1036 1112
+          MapToCurve.tryAndIncrement 1032 = expected
+        )
       )
     $ check "On curve" (
         ∀ x : F,
diff --git a/src/Crypto/EllipticCurve/VRF.lean b/src/Crypto/EllipticCurve/VRF.lean
index 17c4391..8762246 100644
--- a/src/Crypto/EllipticCurve/VRF.lean
+++ b/src/Crypto/EllipticCurve/VRF.lean
@@ -24,7 +24,7 @@ def prove [RandomGen gen] [Monad m] (htc : Point ec → α → Point ec) (commit
     let Z := kp.prv * H
     let r ← Random.random
     let RB := r * g.G
-    let RH := r * g.G
+    let RH := r * H
     let c := commit H Z RB RH
     let s := r + kp.prv * c
     pure ⟨ Z , c , s ⟩
diff --git a/src/Crypto/EllipticCurve/VRF/Test.lean b/src/Crypto/EllipticCurve/VRF/Test.lean
new file mode 100644
index 0000000..f0e98f7
--- /dev/null
+++ b/src/Crypto/EllipticCurve/VRF/Test.lean
@@ -0,0 +1,62 @@
+import Crypto.EllipticCurve.HTC
+import Crypto.EllipticCurve.SECG.Secp256k1
+import Crypto.EllipticCurve.VRF
+import Crypto.Field.Fp
+import Crypto.Hash
+import Crypto.Serial
+import LSpec
+
+open Crypto.EllipticCurve
+open Crypto.Field
+open Crypto.CHash
+open LSpec
+
+
+namespace Crypto.EllipticCurve.VRF.Test
+
+abbrev p := Secp256k1.p
+abbrev F := Secp256k1.F
+theorem hasSqrt : Fp.Is3Mod4 p := rfl
+instance iSqrt : Sqrt F := Fp.instSqrt3Mod4 hasSqrt
+def g := Secp256k1
+def ec := Secp256k1.curve
+
+def pointToBytes : Point ec → ByteArray := Serial.natToBytes ∘ Fp.val ∘ Point.x
+
+def htc (X : Point ec) (m : Nat) : Point ec :=
+  let bs : ByteArray := (pointToBytes X).append (Serial.natToBytes m)
+  let bh : ByteArray := (Algorithm.SHA2_256.chash bs).data
+  let i := Serial.bytesToNat bh
+  let i' : F := Fp.mk i
+  HTC.MapToCurve.tryAndIncrement i'
+
+def commit (H Z RB RH : Point ec) : Fp Secp256k1.n :=
+  let bs : ByteArray :=
+    [H, Z, RB, RH].foldl
+      (fun acc x => acc.append $ pointToBytes x)
+      ByteArray.empty
+  let bh : ByteArray := (Algorithm.SHA2_256.chash bs).data
+  let i := Serial.bytesToNat bh
+  Fp.mk i
+
+structure TestCase where
+  message : Nat
+  pk : Group.PubKey g
+  proof : Proof g
+deriving Repr
+
+instance : SlimCheck.Shrinkable TestCase where
+  shrink _ := []
+
+instance : SlimCheck.SampleableExt TestCase :=
+  SlimCheck.SampleableExt.mkSelfContained
+    $ do
+      let kp ← (Random.random : Rand (Group.KeyPair g))
+      let m ← (Random.randBound Nat 0 1000000 ((Nat.zero_le 1000000)) : Rand Nat)
+      let proof ← (VRF.prove htc commit kp m : Rand (Proof g))
+      pure $ ⟨ m , kp.pubKey, proof ⟩
+
+#lspec check "ECVRF" (∀ tc : TestCase, verify htc commit tc.pk tc.message tc.proof)
+
+
+end Crypto.EllipticCurve.VRF.Test
diff --git a/src/Crypto/Serial.lean b/src/Crypto/Serial.lean
index d66a462..d24f078 100644
--- a/src/Crypto/Serial.lean
+++ b/src/Crypto/Serial.lean
@@ -80,7 +80,7 @@ namespace Serial
   def natToBytes : Nat → ByteArray :=
     ByteArray.mk ∘ Words.toWords
 
-  def BytesToNat : ByteArray → Nat
+  def bytesToNat : ByteArray → Nat
   | ⟨ x ⟩ =>  Words.fromWords x
 
   private def bytesToUInt32s (x : Array UInt8) : Array UInt32 :=