diff --git a/bench/BenchDiv.hs b/bench/BenchDiv.hs index cd52e14bf..6cfbc2602 100644 --- a/bench/BenchDiv.hs +++ b/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 diff --git a/src/ZkFold/Base/Algebra/EllipticCurve/Ed25519.hs b/src/ZkFold/Base/Algebra/EllipticCurve/Ed25519.hs index 5ed4a8bf2..df44b3c1e 100644 --- a/src/ZkFold/Base/Algebra/EllipticCurve/Ed25519.hs +++ b/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) diff --git a/src/ZkFold/Symbolic/Data/Ed25519.hs b/src/ZkFold/Symbolic/Data/Ed25519.hs index 3a2700b62..c354a1cc7 100644 --- a/src/ZkFold/Symbolic/Data/Ed25519.hs +++ b/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,31 +64,14 @@ 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 @@ -129,7 +79,7 @@ instance (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 diff --git a/src/ZkFold/Symbolic/Data/UInt.hs b/src/ZkFold/Symbolic/Data/UInt.hs index 182ca4236..c6bad0bf3 100644 --- a/src/ZkFold/Symbolic/Data/UInt.hs +++ b/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 diff --git a/tests/Tests/UInt.hs b/tests/Tests/UInt.hs index 933791f9c..248b1f1b8 100644 --- a/tests/Tests/UInt.hs +++ b/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