Polynomials, HTC, and ECVRF

src/Crypto.lean

@@ -1,6 +1,7 @@
 
 import Crypto.API
 
+import Crypto.Field
 import Crypto.Field.Fp
 import Crypto.Field.Fp.Test
 
@@ -22,12 +23,18 @@ 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.EllipticCurve.VRF.Test
+
 import Crypto.Hash
 import Crypto.Hash.Test
 

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
 

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

src/Crypto/EllipticCurve/HTC/Test.lean

@@ -0,0 +1,72 @@
+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
+
+
+abbrev p1 := 43
+abbrev F1 := Fp p1
+def hasSqrt1 : Fp.Is3Mod4 p1 := rfl
+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.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.instSqrt3Mod4 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"
+    (
+      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,
+        let actual : EllipticCurve.Point ec := MapToCurve.tryAndIncrement x
+        EllipticCurve.Point.onCurve' actual
+      )
+    )
+
+end Crypto.EllipticCurve.HTC.Test

src/Crypto/EllipticCurve/VRF.lean

@@ -0,0 +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 * H
+    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

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

src/Crypto/Field.lean

@@ -0,0 +1,8 @@
+namespace Crypto.Field
+
+
+class Sqrt (F : Type) where
+  sqrt : F → F
+
+
+end Crypto.Field

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 instSqrt3Mod4 {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

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 :=