Merge pull request #227 from zkFold/hov-migrate-ed25519

Symbolic Ed25519

bench/BenchDiv.hs

@@ -36,8 +36,6 @@ divisionCircuit
     => KnownRegisterSize r
     => rs ~ NumberOfRegisters (Zp p) n r
     => KnownNat rs
-    => KnownNat (rs - 1)
-    => KnownNat (rs + rs)
     => PrimeField (Zp p)
     => IO (UInt n r (ArithmeticCircuit (Zp p)), UInt n r (ArithmeticCircuit (Zp p)))
 divisionCircuit = do
@@ -57,8 +55,6 @@ benchOps
     => KnownRegisterSize r
     => rs ~ NumberOfRegisters (Zp p) n r
     => KnownNat rs
-    => KnownNat (rs - 1)
-    => KnownNat (rs + rs)
     => Benchmark
 benchOps = env (divisionCircuit @n @p @r) $ \ ~ac ->
     bench ("Dividing UInts of size " <> show (value @n)) $ nf (\(a, b) -> (evalUInt a, evalUInt b)) ac

src/ZkFold/Base/Algebra/EllipticCurve/Ed25519.hs

@@ -12,11 +12,12 @@ import           ZkFold.Base.Algebra.EllipticCurve.Class
 
 -- | The Ed25519 curve used in EdDSA signature scheme.
 -- @c@ represents the "computational context" used to store and perform operations on curve points.
+-- @r@ represents the register size
 --
-data Ed25519 c
+data Ed25519 c r
 
 -- | 2^252 + 27742317777372353535851937790883648493 is the order of the multiplicative group in Ed25519
--- with the generator point defined below in @instance EllipticCurve (Ed25519 Void Void)@
+-- with the generator point defined below in @instance EllipticCurve (Ed25519 Void r)@
 --
 type Ed25519_Scalar = 7237005577332262213973186563042994240857116359379907606001950938285454250989
 instance Prime Ed25519_Scalar
@@ -29,9 +30,9 @@ instance Prime Ed25519_Base
 -- | The purely mathematical implementation of Ed25519.
 -- It is available for use as-is and serves as "backend" for the @UInt 256 (Zp p)@ implementation as well.
 --
-instance EllipticCurve (Ed25519 Void) where
-    type BaseField (Ed25519 Void) = Zp Ed25519_Base
-    type ScalarField (Ed25519 Void) = Zp Ed25519_Scalar
+instance EllipticCurve (Ed25519 Void r) where
+    type BaseField (Ed25519 Void r) = Zp Ed25519_Base
+    type ScalarField (Ed25519 Void r) = Zp Ed25519_Scalar
 
     inf = Inf
 
@@ -46,25 +47,25 @@ instance EllipticCurve (Ed25519 Void) where
     mul = pointMul
 
 
-ed25519Add :: Point (Ed25519 Void) -> Point (Ed25519 Void) -> Point (Ed25519 Void)
+ed25519Add :: Point (Ed25519 Void r) -> Point (Ed25519 Void r) -> Point (Ed25519 Void r)
 ed25519Add p Inf = p
 ed25519Add Inf q = q
 ed25519Add (Point x1 y1) (Point x2 y2) = Point x3 y3
     where
-        d :: BaseField (Ed25519 Void)
+        d :: BaseField (Ed25519 Void r)
         d = negate $ toZp 121665 // toZp 121666
 
-        a :: BaseField (Ed25519 Void)
+        a :: BaseField (Ed25519 Void r)
         a = negate $ toZp 1
 
         x3 = (x1 * y2 + y1 * x2) // (toZp 1 + d * x1 * x2 * y1 * y2)
         y3 = (y1 * y2 - a * x1 * x2) // (toZp 1 - d * x1 * x2 * y1 * y2)
 
-ed25519Double :: Point (Ed25519 Void) -> Point (Ed25519 Void)
+ed25519Double :: Point (Ed25519 Void r) -> Point (Ed25519 Void r)
 ed25519Double Inf = Inf
 ed25519Double (Point x y) = Point x3 y3
     where
-        a :: BaseField (Ed25519 Void)
+        a :: BaseField (Ed25519 Void r)
         a = negate $ toZp 1
 
         x3 = 2 * x * y // (a * x * x + y * y)

src/ZkFold/Symbolic/Data/Ed25519.hs

@@ -7,9 +7,9 @@
 module ZkFold.Symbolic.Data.Ed25519  where
 
 import           Control.Applicative                       ((<*>))
+import           Control.DeepSeq                           (NFData)
 import           Data.Functor                              ((<$>))
-import           Data.Void                                 (Void)
-import           Prelude                                   (type (~), ($), (.))
+import           Prelude                                   (type (~), ($))
 import qualified Prelude                                   as P
 
 import           ZkFold.Base.Algebra.Basic.Class
@@ -28,61 +28,28 @@ import           ZkFold.Symbolic.Data.Combinators
 import           ZkFold.Symbolic.Data.Conditional
 import           ZkFold.Symbolic.Data.Eq
 import           ZkFold.Symbolic.Data.UInt
-import           ZkFold.Symbolic.Interpreter
-
-zpToEd :: (Symbolic (Interpreter (Zp p))) => Point (Ed25519 (Interpreter (Zp p))) -> Point (Ed25519 Void)
-zpToEd Inf         = Inf
-zpToEd (Point x y) = Point (toZp . toConstant $ x) (toZp . toConstant $ y)
-
-edToZp :: (Symbolic (Interpreter (Zp p))) => Point (Ed25519 Void) -> Point (Ed25519 (Interpreter (Zp p)))
-edToZp Inf         = Inf
-edToZp (Point x y) = Point (fromConstant . fromZp $ x) (fromConstant . fromZp $ y)
-
--- | Ed25519 with @UInt 256 (Zp p)@ as computational backend
---
-instance (Symbolic  (Interpreter (Zp p))) => EllipticCurve (Ed25519 (Interpreter (Zp p))) where
-    type BaseField (Ed25519 (Interpreter (Zp p))) = UInt 256 Auto (Interpreter (Zp p))
-    type ScalarField (Ed25519 (Interpreter (Zp p))) = UInt 256 Auto (Interpreter (Zp p))
-
-    inf = Inf
-
-    gen = Point
-            (fromConstant (15112221349535400772501151409588531511454012693041857206046113283949847762202 :: Natural))
-            (fromConstant (46316835694926478169428394003475163141307993866256225615783033603165251855960 :: Natural))
-
-    -- | Addition casts point coordinates to @Zp Ed25519_Base@ and adds them as if they were points on @Ed25519 Void@
-    --
-    add p1 p2 = edToZp $ add (zpToEd p1) (zpToEd p2)
-
-    -- | Multiplication casts point coordinates to @Zp Ed25519_Base@ and scale factor to @Zp Ed25519_Scalar@,
-    --   then scales the point as if it were a point on @Ed25519 Void@
-    --
-    mul s p = edToZp @p $ mul (toZp . toConstant $ s) (zpToEd @p p)
 
 instance
     ( Symbolic c
-    , SymbolicData c (UInt 256 Auto c)
-    , AdditiveMonoid (UInt 256 Auto c)
-    , Eq (Bool c) (UInt 256 Auto c)
+    , KnownRegisterSize rs
     , S.BaseField c ~ a
-    , r ~ NumberOfRegisters a 256 Auto
+    , r ~ NumberOfRegisters a 256 rs
     , KnownNat r
-    , 1 <= r
-    ) => SymbolicData c (Point (Ed25519 c)) where
+    ) => SymbolicData c (Point (Ed25519 c rs)) where
 
-    type Support c (Point (Ed25519 c)) = Support c (UInt 256 Auto c)
-    type TypeSize c (Point (Ed25519 c)) = TypeSize c (UInt 256 Auto c) + TypeSize c (UInt 256 Auto c)
+    type Support c (Point (Ed25519 c rs)) = Support c (UInt 256 rs c)
+    type TypeSize c (Point (Ed25519 c rs)) = TypeSize c (UInt 256 rs c) + TypeSize c (UInt 256 rs c)
 
     -- (0, 0) is never on a Twisted Edwards curve for any curve parameters.
     -- We can encode the point at infinity as (0, 0), therefore.
-    pieces Inf         = hliftA2 V.append <$> pieces (zero :: UInt 256 Auto c) <*> pieces (zero :: UInt 256 Auto c)
+    pieces Inf         = hliftA2 V.append <$> pieces (zero :: UInt 256 rs c) <*> pieces (zero :: UInt 256 rs c)
     pieces (Point x y) = hliftA2 V.append <$> pieces x <*> pieces y
 
-    restore f = bool @(Bool c) @(Point (Ed25519 c)) (Point x y) Inf ((x == zero) && (y == zero))
+    restore f = bool @(Bool c) @(Point (Ed25519 c rs)) (Point x y) Inf ((x == zero) && (y == zero))
         where
             (x, y) = restore f
 
-instance (Symbolic c, Eq (Bool c) (BaseField (Ed25519 c))) => Eq (Bool c) (Point (Ed25519 c)) where
+instance (Symbolic c, Eq (Bool c) (BaseField (Ed25519 c r))) => Eq (Bool c) (Point (Ed25519 c r)) where
     Inf == Inf                     = true
     Inf == _                       = false
     _ == Inf                       = false
@@ -97,39 +64,22 @@ instance (Symbolic c, Eq (Bool c) (BaseField (Ed25519 c))) => Eq (Bool c) (Point
 --
 instance
     ( Symbolic c
-    , SymbolicData c (UInt 256 Auto c)
-    , AdditiveGroup (UInt 256 Auto c)
-    , AdditiveGroup (UInt 512 Auto c)
-    , Extend (UInt 256 Auto c) (UInt 512 Auto c)
-    , Shrink (UInt 512 Auto c) (UInt 256 Auto c)
-    , Eq (Bool c) (UInt 512 Auto c)
-    , BitState ByteString 256 c
-    , Eq (Bool c) (UInt 256 Auto c)
-    , FromConstant Natural (UInt 256 Auto c)
-    , FromConstant Natural (UInt 512 Auto c)
-    , EuclideanDomain (UInt 512 Auto c)
-    , S.BaseField c ~ a
-    , r256 ~ NumberOfRegisters a 256 Auto
-    , KnownNat r256
-    , KnownNat (r256 + r256)
-    , 1 <= r256
-    , r512 ~ NumberOfRegisters a 512 Auto
-    , 1 <= r512
-    , KnownNat r512
-    , KnownNat (r512 + (r512 + r512))
-    , Iso (UInt 256 Auto c) (ByteString 256 c)
-    ) => EllipticCurve (Ed25519 c)  where
-
-    type BaseField (Ed25519 c) = UInt 256 Auto c
-    type ScalarField (Ed25519 c) = UInt 256 Auto c
+    , KnownRegisterSize rs
+    , KnownNat (NumberOfRegisters (S.BaseField c) 256 rs)
+    , KnownNat (NumberOfRegisters (S.BaseField c) 512 rs)
+    , NFData (c (V.Vector (NumberOfRegisters (S.BaseField c) 512 rs)))
+    ) => EllipticCurve (Ed25519 c rs)  where
+
+    type BaseField (Ed25519 c rs) = UInt 256 rs c
+    type ScalarField (Ed25519 c rs) = UInt 256 rs c
 
     inf = Inf
 
     gen = Point
             (fromConstant (15112221349535400772501151409588531511454012693041857206046113283949847762202 :: Natural))
             (fromConstant (46316835694926478169428394003475163141307993866256225615783033603165251855960 :: Natural))
 
-    add x y = bool @(Bool c) @(Point (Ed25519 c)) (acAdd25519 x y) (acDouble25519 x) (x == y)
+    add x y = bool @(Bool c) @(Point (Ed25519 c rs)) (acAdd25519 x y) (acDouble25519 x) (x == y)
 
     -- pointMul uses natScale which converts the scale to Natural.
     -- We can't convert arithmetic circuits to Natural, so we can't use pointMul either.
@@ -140,118 +90,112 @@ instance
             bits = from sc
 
 acAdd25519
-    :: forall c
+    :: forall c rs
     .  Symbolic c
-    => AdditiveGroup (UInt 512 Auto c)
-    => EuclideanDomain (UInt 512 Auto c)
-    => Extend (UInt 256 Auto c) (UInt 512 Auto c)
-    => Shrink (UInt 512 Auto c) (UInt 256 Auto c)
-    => Eq (Bool c) (UInt 512 Auto c)
-    => KnownNat (TypeSize c (UInt 512 Auto c))
-    => Point (Ed25519 c)
-    -> Point (Ed25519 c)
-    -> Point (Ed25519 c)
+    => KnownRegisterSize rs
+    => KnownNat (NumberOfRegisters (S.BaseField c) 512 rs)
+    => NFData (c (V.Vector (NumberOfRegisters (S.BaseField c) 512 rs)))
+    => Point (Ed25519 c rs)
+    -> Point (Ed25519 c rs)
+    -> Point (Ed25519 c rs)
 acAdd25519 Inf q = q
 acAdd25519 p Inf = p
 acAdd25519 (Point x1 y1) (Point x2 y2) = Point (shrink x3) (shrink y3)
     where
         -- We will perform multiplications of UInts of up to n bits, therefore we need 2n bits to store the result.
         --
-        x1e, y1e, x2e, y2e :: UInt 512 Auto c
+        x1e, y1e, x2e, y2e :: UInt 512 rs c
         x1e = extend x1
         y1e = extend y1
         x2e = extend x2
         y2e = extend y2
 
-        m :: UInt 512 Auto c
+        m :: UInt 512 rs c
         m = fromConstant $ value @Ed25519_Base
 
-        plusM :: UInt 512 Auto c -> UInt 512 Auto c -> UInt 512 Auto c
+        plusM :: UInt 512 rs c -> UInt 512 rs c -> UInt 512 rs c
         plusM x y = (x + y) `mod` m
 
-        mulM :: UInt 512 Auto c -> UInt 512 Auto c -> UInt 512 Auto c
+        mulM :: UInt 512 rs c -> UInt 512 rs c -> UInt 512 rs c
         mulM x y = (x * y) `mod` m
 
-        d :: UInt 512 Auto c
+        d :: UInt 512 rs c
         d = fromConstant $ fromZp @Ed25519_Base $ (toZp (-121665) // toZp 121666)
 
-        x3n :: UInt 512 Auto c
+        x3n :: UInt 512 rs c
         x3n = (x1e `mulM` y2e) `plusM` (y1e `mulM` x2e)
 
-        x3d :: UInt 512 Auto c
+        x3d :: UInt 512 rs c
         x3d = one `plusM` (d `mulM` x1e `mulM` x2e `mulM` y1e `mulM` y2e)
 
         -- Calculate the modular inverse using Extended Euclidean algorithm
-        x3di :: UInt 512 Auto c
+        x3di :: UInt 512 rs c
         (x3di, _, _) = eea x3d m
 
-        x3 :: UInt 512 Auto c
+        x3 :: UInt 512 rs c
         x3 = x3n `mulM` x3di
 
-        y3n :: UInt 512 Auto c
+        y3n :: UInt 512 rs c
         y3n = (y1e `mulM` y2e) `plusM` (x1e `mulM` x2e)
 
-        y3d :: UInt 512 Auto c
+        y3d :: UInt 512 rs c
         y3d = one `plusM` ((m - d) `mulM` x1e `mulM` x2e `mulM` y1e `mulM` y2e)
 
         -- Calculate the modular inverse using Extended Euclidean algorithm
-        y3di :: UInt 512 Auto c
+        y3di :: UInt 512 rs c
         (y3di, _, _) = eea y3d m
 
-        y3 :: UInt 512 Auto c
+        y3 :: UInt 512 rs c
         y3 = y3n `mulM` y3di
 
 acDouble25519
-    :: forall c
+    :: forall c rs
     .  Symbolic c
-    => EuclideanDomain (UInt 512 Auto c)
-    => AdditiveGroup (UInt 512 Auto c)
-    => Extend (UInt 256 Auto c) (UInt 512 Auto c)
-    => Shrink (UInt 512 Auto c) (UInt 256 Auto c)
-    => Eq (Bool c) (UInt 512 Auto c)
-    => KnownNat (TypeSize c (UInt 512 Auto c))
-    => Point (Ed25519 c)
-    -> Point (Ed25519 c)
+    => KnownRegisterSize rs
+    => KnownNat (NumberOfRegisters (S.BaseField c) 512 rs)
+    => NFData (c (V.Vector (NumberOfRegisters (S.BaseField c) 512 rs)))
+    => Point (Ed25519 c rs)
+    -> Point (Ed25519 c rs)
 acDouble25519 Inf = Inf
 acDouble25519 (Point x1 y1) = Point (shrink x3) (shrink y3)
     where
         -- We will perform multiplications of UInts of up to n bits, therefore we need 2n bits to store the result.
         --
-        xe, ye :: UInt 512 Auto c
+        xe, ye :: UInt 512 rs c
         xe = extend x1
         ye = extend y1
 
-        m :: UInt 512 Auto c
+        m :: UInt 512 rs c
         m = fromConstant $ value @Ed25519_Base
 
-        plusM :: UInt 512 Auto c -> UInt 512 Auto c -> UInt 512 Auto c
+        plusM :: UInt 512 rs c -> UInt 512 rs c -> UInt 512 rs c
         plusM x y = (x + y) `mod` m
 
-        mulM :: UInt 512 Auto c -> UInt 512 Auto c -> UInt 512 Auto c
+        mulM :: UInt 512 rs c -> UInt 512 rs c -> UInt 512 rs c
         mulM x y = (x * y) `mod` m
 
-        x3n :: UInt 512 Auto c
+        x3n :: UInt 512 rs c
         x3n = (xe `mulM` ye) `plusM` (xe `mulM` ye)
 
-        x3d :: UInt 512 Auto c
+        x3d :: UInt 512 rs c
         x3d = ((m - one) `mulM` xe `mulM` xe) `plusM` (ye `mulM` ye)
 
         -- Calculate the modular inverse using Extended Euclidean algorithm
-        x3di :: UInt 512 Auto c
+        x3di :: UInt 512 rs c
         (x3di, _, _) = eea x3d m
 
-        x3 :: UInt 512 Auto c
+        x3 :: UInt 512 rs c
         x3 = x3n `mulM` x3di
 
-        y3n :: UInt 512 Auto c
+        y3n :: UInt 512 rs c
         y3n = (ye `mulM` ye) `plusM` (xe `mulM` xe)
 
-        y3d :: UInt 512 Auto c
+        y3d :: UInt 512 rs c
         y3d = (one + one) `plusM` (xe `mulM` xe) `plusM` ((m - one) `mulM` ye `mulM` ye)
 
         -- Calculate the modular inverse using Extended Euclidean algorithm
-        y3di :: UInt 512 Auto c
+        y3di :: UInt 512 rs c
         (y3di, _, _) = eea y3d m
 
-        y3 :: UInt 512 Auto c
+        y3 :: UInt 512 rs c
         y3 = y3n `mulM` y3di

src/ZkFold/Symbolic/Data/UInt.hs

@@ -200,14 +200,9 @@ instance
     ( Symbolic c
     , KnownNat n
     , KnownNat r
-    , KnownNat (r - 1)
-    , KnownNat (r + r)
     , KnownRegisterSize rs
     , r ~ NumberOfRegisters (BaseField c) n rs
     , NFData (c (Vector r))
-    , Ord (Bool c) (UInt n rs c)
-    , BitState ByteString n c
-    , Iso (ByteString n c) (UInt n rs c)
     ) => EuclideanDomain (UInt n rs c) where
     divMod numerator d = bool @(Bool c) (q, r) (zero, zero) (d == zero)
         where

tests/Tests/UInt.hs

@@ -66,11 +66,7 @@ specUInt'
     => r ~ NumberOfRegisters (Zp p) n rs
     => r2n ~ NumberOfRegisters (Zp p) (2 * n) rs
     => KnownNat r
-    => KnownNat (r + r)
     => KnownNat r2n
-    => KnownNat (r2n + r2n)
-    => KnownNat (r - 1)
-    => KnownNat (r2n - 1)
     => IO ()
 specUInt' = hspec $ do
     let n = value @n