diff --git a/symbolic-base/src/ZkFold/Base/Data/Vector.hs b/symbolic-base/src/ZkFold/Base/Data/Vector.hs index daa5990ac..04277ea46 100644 --- a/symbolic-base/src/ZkFold/Base/Data/Vector.hs +++ b/symbolic-base/src/ZkFold/Base/Data/Vector.hs @@ -9,6 +9,7 @@ import Control.Monad.State.Strict (runState, state) import Data.Aeson (ToJSON (..)) import Data.Distributive (Distributive (..)) import Data.Foldable (fold) +import Data.Functor.Classes (Show1) import Data.Functor.Rep (Representable (..), collectRep, distributeRep, mzipRep, pureRep) import Data.These (These (..)) import qualified Data.Vector as V @@ -20,7 +21,7 @@ import GHC.IsList (IsList (..)) import Prelude hiding (concat, drop, head, length, mod, negate, replicate, sum, tail, take, unzip, zip, zipWith, (*), (+), (-)) import System.Random (Random (..)) -import Test.QuickCheck (Arbitrary (..)) +import Test.QuickCheck (Arbitrary (..), Arbitrary1 (..), arbitrary1) import ZkFold.Base.Algebra.Basic.Class import ZkFold.Base.Algebra.Basic.Field @@ -29,7 +30,7 @@ import ZkFold.Base.Data.ByteString (Binary (..)) import ZkFold.Prelude (length) newtype Vector (size :: Natural) a = Vector {toV :: V.Vector a} - deriving (Show, Eq, Functor, Foldable, Traversable, Generic, NFData, Ord) + deriving (Show, Show1, Eq, Functor, Foldable, Traversable, Generic, NFData, Ord) -- helper knownNat :: forall size n . (KnownNat size, Integral n) => n @@ -173,7 +174,10 @@ instance Unzip (Vector size) where unzip v = (fst <$> v, snd <$> v) instance (Arbitrary a, KnownNat size) => Arbitrary (Vector size a) where - arbitrary = sequenceA (pureRep arbitrary) + arbitrary = arbitrary1 + +instance KnownNat size => Arbitrary1 (Vector size) where + liftArbitrary = sequenceA . pureRep instance (Random a, KnownNat size) => Random (Vector size a) where random = runState (sequenceA (pureRep (state random))) diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonk.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonk.hs index 03c4a7147..e68c0a799 100644 --- a/symbolic-base/src/ZkFold/Base/Protocol/Plonk.hs +++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonk.hs @@ -6,6 +6,7 @@ module ZkFold.Base.Protocol.Plonk ( ) where import Data.Binary (Binary) +import Data.Functor.Classes (Show1) import Data.Functor.Rep (Rep) import Data.Kind (Type) import Data.Word (Word8) @@ -17,7 +18,6 @@ import Test.QuickCheck (Arbitrary import ZkFold.Base.Algebra.Basic.Class (AdditiveGroup) import ZkFold.Base.Algebra.Basic.Number import ZkFold.Base.Algebra.EllipticCurve.Class (EllipticCurve (..), Pairing, PointCompressed) -import ZkFold.Base.Data.Vector (Vector (..)) import ZkFold.Base.Protocol.NonInteractiveProof import ZkFold.Base.Protocol.Plonk.Prover (plonkProve) import ZkFold.Base.Protocol.Plonk.Verifier (plonkVerify) @@ -32,31 +32,32 @@ import ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal {-| Based on the paper https://eprint.iacr.org/2019/953.pdf -} -data Plonk p (i :: Natural) (n :: Natural) (l :: Natural) curve1 curve2 transcript = Plonk { +data Plonk p i (n :: Natural) l curve1 curve2 transcript = Plonk { omega :: ScalarField curve1, k1 :: ScalarField curve1, k2 :: ScalarField curve1, - ac :: ArithmeticCircuit (ScalarField curve1) p (Vector i) (Vector l), + ac :: ArithmeticCircuit (ScalarField curve1) p i l, x :: ScalarField curve1 } fromPlonkup :: - ( KnownNat i - , Arithmetic (ScalarField c1) + ( Arithmetic (ScalarField c1) , Binary (ScalarField c1) , Binary (Rep p) + , Binary (Rep i) + , Ord (Rep i) ) => Plonkup p i n l c1 c2 ts -> Plonk p i n l c1 c2 ts fromPlonkup Plonkup {..} = Plonk { ac = desugarRanges ac, ..} toPlonkup :: Plonk p i n l c1 c2 ts -> Plonkup p i n l c1 c2 ts toPlonkup Plonk {..} = Plonkup {..} -instance (Show (ScalarField c1), Arithmetic (ScalarField c1), KnownNat l, KnownNat i) => Show (Plonk p i n l c1 c2 t) where +instance (Show1 l, Show (Rep i), Show (ScalarField c1), Ord (Rep i)) => Show (Plonk p i n l c1 c2 t) where show Plonk {..} = "Plonk: " ++ show omega ++ " " ++ show k1 ++ " " ++ show k2 ++ " " ++ show (acOutput ac) ++ " " ++ show ac ++ " " ++ show x -instance ( KnownNat i, Arithmetic (ScalarField c1) - , Binary (ScalarField c1), Binary (Rep p) +instance ( Arithmetic (ScalarField c1), Binary (ScalarField c1) + , Binary (Rep p), Binary (Rep i), Ord (Rep i) , Arbitrary (Plonkup p i n l c1 c2 t)) => Arbitrary (Plonk p i n l c1 c2 t) where arbitrary = fromPlonkup <$> arbitrary @@ -69,6 +70,7 @@ instance forall p i n l c1 c2 (ts :: Type) core . , Input (Plonkup p i n l c1 c2 ts) ~ PlonkupInput l c1 , Proof (Plonkup p i n l c1 c2 ts) ~ PlonkupProof c1 , KnownNat n + , Foldable l , Ord (BaseField c1) , AdditiveGroup (BaseField c1) , Pairing c1 c2 diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonk/Prover.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonk/Prover.hs index 53afe5984..12841bc7e 100644 --- a/symbolic-base/src/ZkFold/Base/Protocol/Plonk/Prover.hs +++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonk/Prover.hs @@ -15,7 +15,7 @@ import ZkFold.Base.Algebra.Basic.Class import ZkFold.Base.Algebra.Basic.Number (KnownNat, Natural, value) import ZkFold.Base.Algebra.EllipticCurve.Class (EllipticCurve (..), PointCompressed, compress) import ZkFold.Base.Algebra.Polynomials.Univariate hiding (qr) -import ZkFold.Base.Data.Vector (fromVector, (!!)) +import ZkFold.Base.Data.Vector ((!!)) import ZkFold.Base.Protocol.NonInteractiveProof import ZkFold.Base.Protocol.Plonkup (with4n6) import ZkFold.Base.Protocol.Plonkup.Input @@ -32,6 +32,7 @@ import ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal plonkProve :: forall p i n l c1 c2 ts core . ( KnownNat n + , Foldable l , Ord (BaseField c1) , AdditiveGroup (BaseField c1) , Arithmetic (ScalarField c1) @@ -61,7 +62,7 @@ plonkProve PlonkupProverSetup {..} w2X = with4n6 @n $ polyVecInLagrangeBasis omega w2 :: PlonkupPolyExtended n c1 w3X = with4n6 @n $ polyVecInLagrangeBasis omega w3 :: PlonkupPolyExtended n c1 - pi = toPolyVec @_ @n $ fromList $ fromVector (negate <$> wPub) + pi = toPolyVec @_ @n $ fromList $ foldMap (\x -> [negate x]) wPub piX = with4n6 @n $ polyVecInLagrangeBasis omega pi :: PlonkupPolyExtended n c1 -- Round 1 diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonk/Verifier.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonk/Verifier.hs index ba809bb43..e70aed795 100644 --- a/symbolic-base/src/ZkFold/Base/Protocol/Plonk/Verifier.hs +++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonk/Verifier.hs @@ -14,7 +14,6 @@ import ZkFold.Base.Algebra.Basic.Class import ZkFold.Base.Algebra.Basic.Number (KnownNat, Natural, value) import ZkFold.Base.Algebra.EllipticCurve.Class import ZkFold.Base.Algebra.Polynomials.Univariate hiding (qr) -import ZkFold.Base.Data.Vector (fromVector) import ZkFold.Base.Protocol.NonInteractiveProof hiding (verify) import ZkFold.Base.Protocol.Plonkup.Input import ZkFold.Base.Protocol.Plonkup.Internal @@ -25,6 +24,7 @@ import ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal plonkVerify :: forall p i n l c1 c2 ts . ( KnownNat n + , Foldable l , Pairing c1 c2 , Ord (BaseField c1) , AdditiveGroup (BaseField c1) @@ -103,7 +103,7 @@ plonkVerify -- Step 7: Compute public polynomial evaluation pi_xi = with4n6 @n $ polyVecInLagrangeBasis @(ScalarField c1) @n @(PlonkupPolyExtendedLength n) omega - (toPolyVec $ fromList $ fromVector (negate <$> wPub)) + (toPolyVec $ fromList $ foldMap (\x -> [negate x]) wPub) `evalPolyVec` xi -- Step 8: Compute the public table commitment diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup.hs index 4df11fea5..3f5ad1f90 100644 --- a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup.hs +++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup.hs @@ -7,7 +7,7 @@ module ZkFold.Base.Protocol.Plonkup ( Plonkup (..) ) where -import Data.Functor.Rep (Representable) +import Data.Functor.Rep (Rep, Representable) import Data.Word (Word8) import Prelude hiding (Num (..), div, drop, length, replicate, sum, take, (!!), (/), (^)) @@ -29,10 +29,12 @@ import ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal {-| Based on the paper https://eprint.iacr.org/2022/086.pdf -} instance forall p i n l c1 c2 ts core. - ( KnownNat i - , KnownNat n - , KnownNat l + ( KnownNat n , Representable p + , Representable i + , Representable l + , Foldable l + , Ord (Rep i) , Ord (BaseField c1) , AdditiveGroup (BaseField c1) , Pairing c1 c2 diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Input.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Input.hs index 2acf90140..de4f98316 100644 --- a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Input.hs +++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Input.hs @@ -2,24 +2,25 @@ module ZkFold.Base.Protocol.Plonkup.Input where -import Prelude hiding (Num (..), drop, length, sum, take, (!!), (/), (^)) +import Data.Function (($)) +import Data.Functor (Functor, (<$>)) +import Data.Functor.Classes (Show1) +import Data.List ((++)) import Test.QuickCheck (Arbitrary (..)) +import Text.Show (Show, show) import ZkFold.Base.Algebra.Basic.Class -import ZkFold.Base.Algebra.Basic.Number import ZkFold.Base.Algebra.EllipticCurve.Class (EllipticCurve (..)) -import ZkFold.Base.Data.Vector (Vector (..), unsafeToVector) -import ZkFold.Prelude (take) import ZkFold.Symbolic.Compiler () -newtype PlonkupInput l c = PlonkupInput { unPlonkupInput :: Vector l (ScalarField c) } +newtype PlonkupInput l c = PlonkupInput { unPlonkupInput :: l (ScalarField c) } -instance Show (ScalarField c) => Show (PlonkupInput l c) where +instance (Show1 l, Show (ScalarField c)) => Show (PlonkupInput l c) where show (PlonkupInput v) = "Plonkup Input: " ++ show v -instance (KnownNat l, Arbitrary (ScalarField c)) => Arbitrary (PlonkupInput l c) where - arbitrary = do - PlonkupInput . unsafeToVector . take (value @l) <$> arbitrary +instance (Arbitrary (l (ScalarField c))) => Arbitrary (PlonkupInput l c) where + arbitrary = PlonkupInput <$> arbitrary -plonkupVerifierInput :: Field (ScalarField c) => Vector l (ScalarField c) -> PlonkupInput l c -plonkupVerifierInput input = PlonkupInput $ fmap negate input +plonkupVerifierInput :: + (Functor l, Field (ScalarField c)) => l (ScalarField c) -> PlonkupInput l c +plonkupVerifierInput input = PlonkupInput $ negate <$> input diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Internal.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Internal.hs index 29fe31240..6d3d2d96a 100644 --- a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Internal.hs +++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Internal.hs @@ -3,9 +3,9 @@ module ZkFold.Base.Protocol.Plonkup.Internal where -import Data.Binary (Binary) import Data.Constraint (withDict) import Data.Constraint.Nat (plusNat, timesNat) +import Data.Functor.Classes (Show1) import Data.Functor.Rep (Rep) import Prelude hiding (Num (..), drop, length, sum, take, (!!), (/), (^)) @@ -14,7 +14,6 @@ import Test.QuickCheck (Arbitrary import ZkFold.Base.Algebra.Basic.Number import ZkFold.Base.Algebra.EllipticCurve.Class (EllipticCurve (..)) import ZkFold.Base.Algebra.Polynomials.Univariate (PolyVec) -import ZkFold.Base.Data.Vector (Vector (..)) import ZkFold.Base.Protocol.Plonkup.Utils import ZkFold.Symbolic.Compiler () import ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal @@ -24,11 +23,11 @@ import ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal Additionally, we don't want this library to depend on Cardano libraries. -} -data Plonkup p (i :: Natural) (n :: Natural) (l :: Natural) curve1 curve2 transcript = Plonkup { +data Plonkup p i (n :: Natural) l curve1 curve2 transcript = Plonkup { omega :: ScalarField curve1, k1 :: ScalarField curve1, k2 :: ScalarField curve1, - ac :: ArithmeticCircuit (ScalarField curve1) p (Vector i) (Vector l), + ac :: ArithmeticCircuit (ScalarField curve1) p i l, x :: ScalarField curve1 } @@ -37,20 +36,18 @@ type PlonkupPermutationSize n = 3 * n -- The maximum degree of the polynomials we need in the protocol is `4 * n + 5`. type PlonkupPolyExtendedLength n = 4 * n + 6 - with4n6 :: forall n {r}. KnownNat n => (KnownNat (4 * n + 6) => r) -> r with4n6 f = withDict (timesNat @4 @n) (withDict (plusNat @(4 * n) @6) f) type PlonkupPolyExtended n c = PolyVec (ScalarField c) (PlonkupPolyExtendedLength n) -instance (Show (ScalarField c1), Arithmetic (ScalarField c1), KnownNat l, KnownNat i) => Show (Plonkup p i n l c1 c2 t) where +instance (Show (ScalarField c1), Show (Rep i), Show1 l, Ord (Rep i)) => Show (Plonkup p i n l c1 c2 t) where show Plonkup {..} = "Plonkup: " ++ show omega ++ " " ++ show k1 ++ " " ++ show k2 ++ " " ++ show (acOutput ac) ++ " " ++ show ac ++ " " ++ show x instance - ( KnownNat i, KnownNat n, KnownNat l - , Arithmetic (ScalarField c1), Arbitrary (ScalarField c1), Binary (ScalarField c1) - , Binary (Rep p) + ( KnownNat n, Arithmetic (ScalarField c1), Arbitrary (ScalarField c1) + , Arbitrary (ArithmeticCircuit (ScalarField c1) p i l) ) => Arbitrary (Plonkup p i n l c1 c2 t) where arbitrary = do ac <- arbitrary diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/LookupConstraint.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/LookupConstraint.hs index c20ba6204..7fff28e2f 100644 --- a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/LookupConstraint.hs +++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/LookupConstraint.hs @@ -1,17 +1,21 @@ +{-# LANGUAGE UndecidableInstances #-} + module ZkFold.Base.Protocol.Plonkup.LookupConstraint where import Data.Binary (Binary) import Data.ByteString (ByteString) +import Data.Functor.Rep (Rep) import Prelude hiding (Num (..), drop, length, sum, take, (!!), (/), (^)) import Test.QuickCheck (Arbitrary (..)) import ZkFold.Base.Data.ByteString (toByteString) -import ZkFold.Base.Data.Vector (Vector) import ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal -newtype LookupConstraint i a = LookupConstraint { lkVar :: SysVar (Vector i) } - deriving (Show, Eq) +newtype LookupConstraint i a = LookupConstraint { lkVar :: SysVar i } + +deriving instance Show (Rep i) => Show (LookupConstraint i a) +deriving instance Eq (Rep i) => Eq (LookupConstraint i a) instance (Arbitrary a, Binary a) => Arbitrary (LookupConstraint i a) where arbitrary = LookupConstraint . NewVar . toByteString @a <$> arbitrary diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/PlonkConstraint.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/PlonkConstraint.hs index 3caa71180..4993634e1 100644 --- a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/PlonkConstraint.hs +++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/PlonkConstraint.hs @@ -9,13 +9,13 @@ import Data.Containers.ListUtils (nubOrd) import Data.Eq (Eq (..)) import Data.Function (($), (.)) import Data.Functor ((<$>)) +import Data.Functor.Rep (Rep) import Data.List (find, head, map, permutations, sort, (!!), (++)) import Data.Map (Map) import qualified Data.Map as Map import Data.Maybe (Maybe (..), fromMaybe, mapMaybe) import Data.Ord (Ord) import GHC.IsList (IsList (..)) -import GHC.TypeNats (KnownNat) import Numeric.Natural (Natural) import Test.QuickCheck (Arbitrary (..)) import Text.Show (Show) @@ -24,7 +24,6 @@ import ZkFold.Base.Algebra.Basic.Class import ZkFold.Base.Algebra.Polynomials.Multivariate (Poly, evalMonomial, evalPolynomial, polynomial, var, variables) import ZkFold.Base.Data.ByteString (toByteString) -import ZkFold.Base.Data.Vector (Vector) import ZkFold.Prelude (length, take) import ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal @@ -34,13 +33,15 @@ data PlonkConstraint i a = PlonkConstraint , qr :: a , qo :: a , qc :: a - , x1 :: Var a (Vector i) - , x2 :: Var a (Vector i) - , x3 :: Var a (Vector i) + , x1 :: Var a i + , x2 :: Var a i + , x3 :: Var a i } - deriving (Show, Eq) -instance (Ord a, Arbitrary a, Binary a, KnownNat i) => Arbitrary (PlonkConstraint i a) where +deriving instance (Show a, Show (Rep i)) => Show (PlonkConstraint i a) +deriving instance (Eq a, Eq (Rep i)) => Eq (PlonkConstraint i a) + +instance (Ord a, Arbitrary a, Binary a, Ord (Rep i)) => Arbitrary (PlonkConstraint i a) where arbitrary = do qm <- arbitrary ql <- arbitrary @@ -49,10 +50,10 @@ instance (Ord a, Arbitrary a, Binary a, KnownNat i) => Arbitrary (PlonkConstrain qc <- arbitrary let arbitraryNewVar = SysVar . NewVar . toByteString @a <$> arbitrary xs <- sort <$> replicateM 3 arbitraryNewVar - let x1 = xs !! 0; x2 = xs !! 1; x3 = xs !! 2 + let x1 = head xs; x2 = xs !! 1; x3 = xs !! 2 return $ PlonkConstraint qm ql qr qo qc x1 x2 x3 -toPlonkConstraint :: forall a i . (Ord a, FiniteField a, KnownNat i) => Poly a (Var a (Vector i)) Natural -> PlonkConstraint i a +toPlonkConstraint :: forall a i . (Ord a, FiniteField a, Ord (Rep i)) => Poly a (Var a i) Natural -> PlonkConstraint i a toPlonkConstraint p = let xs = Just <$> toList (variables p) perms = nubOrd $ map (take 3) $ permutations $ case length xs of @@ -61,12 +62,12 @@ toPlonkConstraint p = 2 -> [Nothing] ++ xs ++ xs _ -> xs ++ xs - getCoef :: Map (Maybe (Var a (Vector i))) Natural -> a + getCoef :: Map (Maybe (Var a i)) Natural -> a getCoef m = case find (\(_, as) -> m == Map.mapKeys Just as) (toList p) of Just (c, _) -> c _ -> zero - getCoefs :: [Maybe (Var a (Vector i))] -> Maybe (PlonkConstraint i a) + getCoefs :: [Maybe (Var a i)] -> Maybe (PlonkConstraint i a) getCoefs [a, b, c] = do let xa = [(a, 1)] xb = [(b, 1)] @@ -89,7 +90,7 @@ toPlonkConstraint p = [] -> toPlonkConstraint zero _ -> head $ mapMaybe getCoefs perms -fromPlonkConstraint :: (Ord a, Field a, KnownNat i) => PlonkConstraint i a -> Poly a (Var a (Vector i)) Natural +fromPlonkConstraint :: (Ord a, Field a, Ord (Rep i)) => PlonkConstraint i a -> Poly a (Var a i) Natural fromPlonkConstraint (PlonkConstraint qm ql qr qo qc a b c) = let xa = var a xb = var b diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/PlonkupConstraint.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/PlonkupConstraint.hs index 287edb93d..b4d0ea1a3 100644 --- a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/PlonkupConstraint.hs +++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/PlonkupConstraint.hs @@ -1,18 +1,17 @@ module ZkFold.Base.Protocol.Plonkup.PlonkupConstraint where +import Data.Functor.Rep (Rep) import Prelude hiding (Num (..), drop, length, replicate, sum, take, (!!), (/), (^)) import ZkFold.Base.Algebra.Basic.Class -import ZkFold.Base.Algebra.Basic.Number -import ZkFold.Base.Data.Vector (Vector) import ZkFold.Base.Protocol.Plonkup.LookupConstraint (LookupConstraint (..)) import ZkFold.Base.Protocol.Plonkup.PlonkConstraint (PlonkConstraint (..), toPlonkConstraint) import ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal data PlonkupConstraint i a = ConsPlonk (PlonkConstraint i a) | ConsLookup (LookupConstraint i a) | ConsExtra -getPlonkConstraint :: (Ord a, FiniteField a, KnownNat i) => PlonkupConstraint i a -> PlonkConstraint i a +getPlonkConstraint :: (Ord a, FiniteField a, Ord (Rep i)) => PlonkupConstraint i a -> PlonkConstraint i a getPlonkConstraint (ConsPlonk c) = c getPlonkConstraint _ = toPlonkConstraint zero @@ -20,17 +19,17 @@ isLookupConstraint :: FiniteField a => PlonkupConstraint i a -> a isLookupConstraint (ConsLookup _) = one isLookupConstraint _ = zero -getA :: forall a i . (Ord a, FiniteField a, KnownNat i) => PlonkupConstraint i a -> Var a (Vector i) +getA :: forall a i . (Ord a, FiniteField a, Ord (Rep i)) => PlonkupConstraint i a -> Var a i getA (ConsPlonk c) = x1 c getA (ConsLookup c) = SysVar $ lkVar c -getA ConsExtra = x1 (toPlonkConstraint @a zero) +getA ConsExtra = x1 (toPlonkConstraint zero) -getB :: forall a i . (Ord a, FiniteField a, KnownNat i) => PlonkupConstraint i a -> Var a (Vector i) +getB :: forall a i . (Ord a, FiniteField a, Ord (Rep i)) => PlonkupConstraint i a -> Var a i getB (ConsPlonk c) = x2 c getB (ConsLookup c) = SysVar $ lkVar c -getB ConsExtra = x2 (toPlonkConstraint @a zero) +getB ConsExtra = x2 (toPlonkConstraint zero) -getC :: forall a i . (Ord a, FiniteField a, KnownNat i) => PlonkupConstraint i a -> Var a (Vector i) +getC :: forall a i . (Ord a, FiniteField a, Ord (Rep i)) => PlonkupConstraint i a -> Var a i getC (ConsPlonk c) = x3 c getC (ConsLookup c) = SysVar $ lkVar c -getC ConsExtra = x3 (toPlonkConstraint @a zero) +getC ConsExtra = x3 (toPlonkConstraint zero) diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Prover.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Prover.hs index fb711cdf5..dd3d74765 100644 --- a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Prover.hs +++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Prover.hs @@ -18,7 +18,7 @@ import ZkFold.Base.Algebra.Basic.Class import ZkFold.Base.Algebra.Basic.Number (KnownNat, Natural, value) import ZkFold.Base.Algebra.EllipticCurve.Class (EllipticCurve (..), PointCompressed, compress) import ZkFold.Base.Algebra.Polynomials.Univariate hiding (qr) -import ZkFold.Base.Data.Vector (fromVector, (!!)) +import ZkFold.Base.Data.Vector ((!!)) import ZkFold.Base.Protocol.NonInteractiveProof import ZkFold.Base.Protocol.Plonkup.Input import ZkFold.Base.Protocol.Plonkup.Internal (PlonkupPolyExtended, PlonkupPolyExtendedLength) @@ -35,6 +35,7 @@ import ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal plonkupProve :: forall p i n l c1 c2 ts core . ( KnownNat n , KnownNat (PlonkupPolyExtendedLength n) + , Foldable l , Ord (BaseField c1) , AdditiveGroup (BaseField c1) , Arithmetic (ScalarField c1) @@ -64,7 +65,9 @@ plonkupProve PlonkupProverSetup {..} w2X = polyVecInLagrangeBasis omega w2 :: PlonkupPolyExtended n c1 w3X = polyVecInLagrangeBasis omega w3 :: PlonkupPolyExtended n c1 - pi = toPolyVec @_ @n $ fromList $ fromVector (negate <$> wPub) + -- Is this really correct? + -- How is \(n\) related to the length of public input? + pi = toPolyVec @_ @n $ fromList $ foldMap (\x -> [negate x]) wPub piX = polyVecInLagrangeBasis omega pi :: PlonkupPolyExtended n c1 -- Round 1 diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Relation.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Relation.hs index 387f2097c..6f0ebb37f 100644 --- a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Relation.hs +++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Relation.hs @@ -4,16 +4,16 @@ module ZkFold.Base.Protocol.Plonkup.Relation where -import Data.Binary (Binary) import Data.Bool (bool) import Data.Constraint (withDict) import Data.Constraint.Nat (timesNat) -import Data.Functor.Rep (Rep, Representable) +import Data.Foldable (toList) +import Data.Functor.Rep (Rep, Representable, tabulate) import Data.Map (elems) import qualified Data.Map.Monoidal as M import Data.Maybe (fromJust) import qualified Data.Set as S -import GHC.IsList (IsList (..)) +import GHC.IsList (fromList) import Prelude hiding (Num (..), drop, length, replicate, sum, take, (!!), (/), (^)) import Test.QuickCheck (Arbitrary (..)) @@ -23,7 +23,6 @@ import ZkFold.Base.Algebra.Basic.Number import ZkFold.Base.Algebra.Basic.Permutations (Permutation, fromCycles, mkIndexPartition) import ZkFold.Base.Algebra.Polynomials.Multivariate (evalMonomial, evalPolynomial, var) import ZkFold.Base.Algebra.Polynomials.Univariate (PolyVec, toPolyVec) -import ZkFold.Base.Data.Vector (Vector, fromVector) import ZkFold.Base.Protocol.Plonkup.Internal (PlonkupPermutationSize) import ZkFold.Base.Protocol.Plonkup.LookupConstraint (LookupConstraint (..)) import ZkFold.Base.Protocol.Plonkup.PlonkConstraint (PlonkConstraint (..), toPlonkConstraint) @@ -42,8 +41,8 @@ data PlonkupRelation p i n l a = PlonkupRelation , qK :: PolyVec a n , t :: PolyVec a n , sigma :: Permutation (3 * n) - , witness :: p a -> Vector i a -> (PolyVec a n, PolyVec a n, PolyVec a n) - , pubInput :: p a -> Vector i a -> Vector l a + , witness :: p a -> i a -> (PolyVec a n, PolyVec a n, PolyVec a n) + , pubInput :: p a -> i a -> l a } instance Show a => Show (PlonkupRelation p i n l a) where @@ -59,29 +58,26 @@ instance Show a => Show (PlonkupRelation p i n l a) where ++ show sigma instance - ( KnownNat i - , KnownNat n + ( KnownNat n , KnownNat (PlonkupPermutationSize n) - , KnownNat l , Representable p - , Arbitrary a + , Representable i + , Representable l + , Foldable l + , Ord (Rep i) , Arithmetic a - , Binary a - , Binary (Rep p) + , Arbitrary (ArithmeticCircuit a p i l) ) => Arbitrary (PlonkupRelation p i n l a) where arbitrary = fromJust . toPlonkupRelation <$> arbitrary -toPlonkupRelation :: forall i p n l a . - KnownNat i - => KnownNat n - => KnownNat l - => Representable p - => Arithmetic a - => ArithmeticCircuit a p (Vector i) (Vector l) - -> Maybe (PlonkupRelation p i n l a) +toPlonkupRelation :: + forall i p n l a . + ( KnownNat n, Arithmetic a, Ord (Rep i) + , Representable p, Representable i, Representable l, Foldable l + ) => ArithmeticCircuit a p i l -> Maybe (PlonkupRelation p i n l a) toPlonkupRelation ac = let xPub = acOutput ac - pubInputConstraints = map var (fromVector xPub) + pubInputConstraints = map var (toList xPub) plonkConstraints = map (evalPolynomial evalMonomial (var . SysVar)) (elems (acSystem ac)) rs = map toConstant $ M.keys $ acRange ac -- TODO: We are expecting at most one range. @@ -92,7 +88,7 @@ toPlonkupRelation ac = xLookup = concatMap S.toList $ M.elems (acRange ac) -- The total number of constraints in the relation. - n' = acSizeN ac + value @l + length xLookup + n' = acSizeN ac + length (tabulate @l id) + length xLookup plonkupSystem = concat [ map (ConsPlonk . toPlonkConstraint) (pubInputConstraints ++ plonkConstraints) diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Setup.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Setup.hs index 4a2779372..e2436c66c 100644 --- a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Setup.hs +++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Setup.hs @@ -3,7 +3,7 @@ module ZkFold.Base.Protocol.Plonkup.Setup where -import Data.Functor.Rep (Representable) +import Data.Functor.Rep (Rep, Representable) import Data.Maybe (fromJust) import qualified Data.Vector as V import GHC.IsList (IsList (..)) @@ -61,10 +61,12 @@ instance ++ show commitments plonkupSetup :: forall i p n l c1 c2 ts core. - ( KnownNat i - , KnownNat l - , KnownNat n + ( KnownNat n , Representable p + , Representable i + , Representable l + , Foldable l + , Ord (Rep i) , Arithmetic (ScalarField c1) , Pairing c1 c2 , CoreFunction c1 core) => Plonkup p i n l c1 c2 ts -> PlonkupSetup p i n l c1 c2 diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Verifier.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Verifier.hs index 4651fa736..d637b8f27 100644 --- a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Verifier.hs +++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Verifier.hs @@ -16,7 +16,6 @@ import ZkFold.Base.Algebra.Basic.Class import ZkFold.Base.Algebra.Basic.Number (KnownNat, Natural, value) import ZkFold.Base.Algebra.EllipticCurve.Class import ZkFold.Base.Algebra.Polynomials.Univariate hiding (qr) -import ZkFold.Base.Data.Vector (fromVector) import ZkFold.Base.Protocol.NonInteractiveProof hiding (verify) import ZkFold.Base.Protocol.Plonkup.Input import ZkFold.Base.Protocol.Plonkup.Internal @@ -28,6 +27,7 @@ import ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal plonkupVerify :: forall p i n l c1 c2 ts . ( KnownNat n , KnownNat (PlonkupPolyExtendedLength n) + , Foldable l , Pairing c1 c2 , Ord (BaseField c1) , AdditiveGroup (BaseField c1) @@ -106,7 +106,7 @@ plonkupVerify -- Step 7: Compute public polynomial evaluation pi_xi = polyVecInLagrangeBasis @(ScalarField c1) @n @(PlonkupPolyExtendedLength n) omega - (toPolyVec $ fromList $ fromVector (negate <$> wPub)) + (toPolyVec $ fromList $ foldMap (\x -> [negate x]) wPub) `evalPolyVec` xi -- Step 8: Compute the public table commitment diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Witness.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Witness.hs index 7dffe586f..63dba3db9 100644 --- a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Witness.hs +++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Witness.hs @@ -2,22 +2,24 @@ module ZkFold.Base.Protocol.Plonkup.Witness where -import Prelude hiding (Num (..), drop, length, sum, take, (!!), (/), (^)) -import Test.QuickCheck (Arbitrary (..)) +import Control.Applicative ((<*>)) +import Data.Functor ((<$>)) +import Data.Functor.Classes (Show1) +import Data.List ((++)) +import Test.QuickCheck (Arbitrary (..), Arbitrary1, arbitrary1) +import Text.Show (Show, show) -import ZkFold.Base.Algebra.Basic.Number (KnownNat) import ZkFold.Base.Algebra.EllipticCurve.Class (EllipticCurve (..)) -import ZkFold.Base.Data.Vector (Vector) data PlonkupWitnessInput p i c = PlonkupWitnessInput { payloadInput :: p (ScalarField c) - , witnessInput :: Vector i (ScalarField c) + , witnessInput :: i (ScalarField c) } -instance (Show (ScalarField c), Show (p (ScalarField c))) +instance (Show1 p, Show1 i, Show (ScalarField c)) => Show (PlonkupWitnessInput p i c) where show (PlonkupWitnessInput p v) = "Plonkup Witness Input: " ++ show p ++ ", " ++ show v -instance (KnownNat i, Arbitrary (ScalarField c), Arbitrary (p (ScalarField c))) +instance (Arbitrary1 p, Arbitrary1 i, Arbitrary (ScalarField c)) => Arbitrary (PlonkupWitnessInput p i c) where - arbitrary = PlonkupWitnessInput <$> arbitrary <*> arbitrary + arbitrary = PlonkupWitnessInput <$> arbitrary1 <*> arbitrary1 diff --git a/symbolic-base/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit/Instance.hs b/symbolic-base/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit/Instance.hs index a03dde46f..9792df719 100644 --- a/symbolic-base/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit/Instance.hs +++ b/symbolic-base/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit/Instance.hs @@ -99,7 +99,7 @@ createRangeConstraint (FieldElement x) a = FieldElement $ fromCircuitF x (\ (Par return v -- TODO: make it more readable -instance (FiniteField a, Haskell.Eq a, Show a, Show (o (Var a i)), Haskell.Ord (Rep i), Show (Var a i), Show (Rep i)) => Show (ArithmeticCircuit a p i o) where +instance (Show a, Show (o (Var a i)), Show (Var a i), Show (Rep i), Haskell.Ord (Rep i)) => Show (ArithmeticCircuit a p i o) where show r = "ArithmeticCircuit { acSystem = " ++ show (acSystem r) ++ "\n, acRange = " ++ show (acRange r) ++ "\n, acOutput = " ++ show (acOutput r) diff --git a/symbolic-base/test/Tests/NonInteractiveProof.hs b/symbolic-base/test/Tests/NonInteractiveProof.hs index 7fcda0081..35c73aab7 100644 --- a/symbolic-base/test/Tests/NonInteractiveProof.hs +++ b/symbolic-base/test/Tests/NonInteractiveProof.hs @@ -6,13 +6,16 @@ module Tests.NonInteractiveProof (specNonInteractiveProof) where import Data.ByteString (ByteString) +import Data.Functor.Classes (Show1 (..)) import Data.Typeable (Proxy (..), Typeable, typeRep) import GHC.Generics (U1 (..)) import Prelude hiding (Fractional (..), Num (..), length) import Test.Hspec (describe, hspec, it) -import Test.QuickCheck (Arbitrary, Testable (property), arbitrary, withMaxSuccess) +import Test.QuickCheck (Arbitrary (..), Arbitrary1 (..), Testable (property), + withMaxSuccess) import ZkFold.Base.Algebra.EllipticCurve.BLS12_381 +import ZkFold.Base.Data.Vector (Vector) import ZkFold.Base.Protocol.KZG (KZG) import ZkFold.Base.Protocol.NonInteractiveProof (HaskellCore, NonInteractiveProof (..)) import ZkFold.Base.Protocol.Plonk (Plonk) @@ -35,9 +38,13 @@ specNonInteractiveProof' = hspec $ do instance Arbitrary (U1 a) where arbitrary = return U1 +instance Show1 U1 where + liftShowsPrec _ _ = showsPrec +instance Arbitrary1 U1 where + liftArbitrary _ = return U1 specNonInteractiveProof :: IO () specNonInteractiveProof = do specNonInteractiveProof' @(KZG BLS12_381_G1 BLS12_381_G2 32) @HaskellCore - specNonInteractiveProof' @(Plonk U1 1 32 2 BLS12_381_G1 BLS12_381_G2 ByteString) @HaskellCore - specNonInteractiveProof' @(Plonkup U1 1 32 2 BLS12_381_G1 BLS12_381_G2 ByteString) @HaskellCore + specNonInteractiveProof' @(Plonk U1 (Vector 1) 32 (Vector 2) BLS12_381_G1 BLS12_381_G2 ByteString) @HaskellCore + specNonInteractiveProof' @(Plonkup U1 (Vector 1) 32 (Vector 2) BLS12_381_G1 BLS12_381_G2 ByteString) @HaskellCore diff --git a/symbolic-base/test/Tests/Plonkup.hs b/symbolic-base/test/Tests/Plonkup.hs index a71d865b9..4caf531eb 100644 --- a/symbolic-base/test/Tests/Plonkup.hs +++ b/symbolic-base/test/Tests/Plonkup.hs @@ -9,16 +9,19 @@ import Control.Monad (forM_, ret import Data.Bool (Bool) import Data.ByteString (ByteString) import Data.Eq (Eq (..)) +import Data.Foldable (Foldable, toList) import Data.Function (($)) -import Data.Functor.Rep (Representable) +import Data.Functor.Classes (Show1 (..)) +import Data.Functor.Rep (Rep, Representable) import Data.Int (Int) import Data.List (head, sort) import Data.Ord (Ord) import GHC.Generics (U1 (..)) -import GHC.IsList (IsList (..)) +import GHC.IsList (IsList (fromList)) import System.IO (IO) import Test.Hspec import Test.QuickCheck +import Text.Show (showsPrec) import ZkFold.Base.Algebra.Basic.Class import ZkFold.Base.Algebra.Basic.Field (fromZp) @@ -27,7 +30,7 @@ import ZkFold.Base.Algebra.EllipticCurve.BLS12_381 (BLS12_381_ import ZkFold.Base.Algebra.EllipticCurve.Class (EllipticCurve (..)) import ZkFold.Base.Algebra.Polynomials.Multivariate as PM import ZkFold.Base.Algebra.Polynomials.Univariate -import ZkFold.Base.Data.Vector (Vector, fromVector) +import ZkFold.Base.Data.Vector (Vector) import ZkFold.Base.Protocol.NonInteractiveProof (HaskellCore, setupProve) import ZkFold.Base.Protocol.Plonkup hiding (omega) import ZkFold.Base.Protocol.Plonkup.PlonkConstraint @@ -53,21 +56,23 @@ problematicPolynomials = , polynomial [(one, M $ fromList [(SysVar (NewVar "v1"), 1), (ConstVar one, 1)])] ] -propPlonkConstraintConversion :: (Ord a, FiniteField a) => PlonkConstraint 1 a -> Bool +propPlonkConstraintConversion :: (Ord a, FiniteField a) => PlonkConstraint (Vector 1) a -> Bool propPlonkConstraintConversion p = toPlonkConstraint (fromPlonkConstraint p) == p -propPlonkupRelationHolds :: forall p i n l a . (KnownNat n, Arithmetic a) => PlonkupRelation p i n l a -> p a -> Vector i a -> Bool +propPlonkupRelationHolds :: + forall p i n l a . (Foldable l, KnownNat n, Arithmetic a) => + PlonkupRelation p i n l a -> p a -> i a -> Bool propPlonkupRelationHolds PlonkupRelation {..} p w = let (w1, w2, w3) = witness p w - pub = negate $ toPolyVec $ fromList $ fromVector $ pubInput p w + pub = negate $ toPolyVec $ fromList $ toList $ pubInput p w in qL .*. w1 + qR .*. w2 + qO .*. w3 + qM .*. w1 .*. w2 + qC + pub == zero propSortByListIsCorrect :: Ord a => [a] -> Bool propSortByListIsCorrect xs = sortByList xs (sort xs) == sort xs propPlonkPolyEquality :: forall p i n l - . (Representable p, KnownNat i, KnownNat n, KnownNat l) + . (Representable p, KnownNat n, Representable i, Representable l, Foldable l, Ord (Rep i)) => Plonkup p i n l BLS12_381_G1 BLS12_381_G2 ByteString -> PlonkupWitnessInput p i BLS12_381_G1 -> PlonkupProverSecret BLS12_381_G1 @@ -80,7 +85,7 @@ propPlonkPolyEquality plonk witness secret pow = in p `evalPolyVec` (omega ^ fromZp pow) == zero propPlonkGrandProductIsCorrect :: forall p i n l - . (Representable p, KnownNat i, KnownNat n, KnownNat l) + . (Representable p, KnownNat n, Representable i, Representable l, Foldable l, Ord (Rep i)) => Plonkup p i n l BLS12_381_G1 BLS12_381_G2 ByteString -> PlonkupWitnessInput p i BLS12_381_G1 -> PlonkupProverSecret BLS12_381_G1 @@ -91,7 +96,7 @@ propPlonkGrandProductIsCorrect plonk witness secret = in head (toList $ fromPolyVec grandProduct1) == one propPlonkGrandProductEquality :: forall p i n l - . (Representable p, KnownNat i, KnownNat n, KnownNat l) + . (Representable p, KnownNat n, Representable i, Representable l, Foldable l, Ord (Rep i)) => Plonkup p i n l BLS12_381_G1 BLS12_381_G2 ByteString -> PlonkupWitnessInput p i BLS12_381_G1 -> PlonkupProverSecret BLS12_381_G1 @@ -113,7 +118,7 @@ propPlonkGrandProductEquality plonk witness secret pow = in p `evalPolyVec` (omega ^ fromZp pow) == zero propLookupPolyEquality :: forall p i n l - . (Representable p, KnownNat i, KnownNat n, KnownNat l) + . (Representable p, KnownNat n, Representable i, Representable l, Foldable l, Ord (Rep i)) => Plonkup p i n l BLS12_381_G1 BLS12_381_G2 ByteString -> PlonkupWitnessInput p i BLS12_381_G1 -> PlonkupProverSecret BLS12_381_G1 @@ -127,7 +132,7 @@ propLookupPolyEquality plonk witness secret pow = in p `evalPolyVec` (omega ^ fromZp pow) == zero propLookupGrandProductIsCorrect :: forall p i n l - . (Representable p, KnownNat i, KnownNat n, KnownNat l) + . (Representable p, KnownNat n, Representable i, Representable l, Foldable l, Ord (Rep i)) => Plonkup p i n l BLS12_381_G1 BLS12_381_G2 ByteString -> PlonkupWitnessInput p i BLS12_381_G1 -> PlonkupProverSecret BLS12_381_G1 @@ -138,7 +143,7 @@ propLookupGrandProductIsCorrect plonk witness secret = in z2X `evalPolyVec` omega == one propLookupGrandProductEquality :: forall p i n l - . (Representable p, KnownNat i, KnownNat n, KnownNat l) + . (Representable p, KnownNat n, Representable i, Representable l, Foldable l, Ord (Rep i)) => Plonkup p i n l BLS12_381_G1 BLS12_381_G2 ByteString -> PlonkupWitnessInput p i BLS12_381_G1 -> PlonkupProverSecret BLS12_381_G1 @@ -155,7 +160,7 @@ propLookupGrandProductEquality plonk witness secret pow = in p `evalPolyVec` (omega ^ fromZp pow) == zero propLinearizationPolyEvaluation :: forall p i n l - . (Representable p, KnownNat i, KnownNat n, KnownNat l) + . (Representable p, KnownNat n, Representable i, Representable l, Foldable l, Ord (Rep i)) => Plonkup p i n l BLS12_381_G1 BLS12_381_G2 ByteString -> PlonkupWitnessInput p i BLS12_381_G1 -> PlonkupProverSecret BLS12_381_G1 @@ -167,6 +172,10 @@ propLinearizationPolyEvaluation plonk witness secret = instance Arbitrary (U1 a) where arbitrary = return U1 +instance Arbitrary1 U1 where + liftArbitrary _ = return U1 +instance Show1 U1 where + liftShowsPrec _ _ = showsPrec specPlonkup :: IO () specPlonkup = hspec $ do @@ -176,22 +185,22 @@ specPlonkup = hspec $ do it "handcrafted polynomials do not cause exceptions " $ forM_ problematicPolynomials $ \p -> fromPlonkConstraint (toPlonkConstraint @(ScalarField BLS12_381_G1) p) `shouldBe` p it "'ConstVar a' does not cause exceptions " $ - property $ \v -> fromPlonkConstraint (toPlonkConstraint @(ScalarField BLS12_381_G1) @1 (var $ ConstVar v)) == var (ConstVar v) + property $ \v -> fromPlonkConstraint (toPlonkConstraint @(ScalarField BLS12_381_G1) @(Vector 1) (var $ ConstVar v)) == var (ConstVar v) describe "Sort by list is correct" $ do it "should hold" $ property $ propSortByListIsCorrect @Int describe "Plonkup relation" $ do - it "should hold" $ property $ propPlonkupRelationHolds @U1 @2 @32 @3 @(ScalarField BLS12_381_G1) + it "should hold" $ property $ propPlonkupRelationHolds @U1 @(Vector 2) @32 @(Vector 3) @(ScalarField BLS12_381_G1) describe "Plonk polynomials equality" $ do - it "should hold" $ property $ propPlonkPolyEquality @U1 @1 @32 @2 + it "should hold" $ property $ propPlonkPolyEquality @U1 @(Vector 1) @32 @(Vector 2) describe "Plonk grand product correctness" $ do - it "should hold" $ property $ withMaxSuccess 10 $ propPlonkGrandProductIsCorrect @U1 @1 @32 @2 + it "should hold" $ property $ withMaxSuccess 10 $ propPlonkGrandProductIsCorrect @U1 @(Vector 1) @32 @(Vector 2) describe "Plonkup grand product equality" $ do - it "should hold" $ property $ withMaxSuccess 10 $ propPlonkGrandProductEquality @U1 @1 @32 @2 + it "should hold" $ property $ withMaxSuccess 10 $ propPlonkGrandProductEquality @U1 @(Vector 1) @32 @(Vector 2) describe "Lookup polynomials equality" $ do - it "should hold" $ property $ withMaxSuccess 10 $ propLookupPolyEquality @U1 @1 @32 @2 + it "should hold" $ property $ withMaxSuccess 10 $ propLookupPolyEquality @U1 @(Vector 1) @32 @(Vector 2) describe "Lookup grand product correctness" $ do - it "should hold" $ property $ withMaxSuccess 10 $ propLookupGrandProductIsCorrect @U1 @1 @32 @2 + it "should hold" $ property $ withMaxSuccess 10 $ propLookupGrandProductIsCorrect @U1 @(Vector 1) @32 @(Vector 2) describe "Lookup grand product equality" $ do - it "should hold" $ property $ withMaxSuccess 10 $ propLookupGrandProductEquality @U1 @1 @32 @2 + it "should hold" $ property $ withMaxSuccess 10 $ propLookupGrandProductEquality @U1 @(Vector 1) @32 @(Vector 2) describe "Linearization polynomial in the challenge point" $ do - it "evaluates to zero" $ property $ withMaxSuccess 10 $ propLinearizationPolyEvaluation @U1 @1 @32 @2 + it "evaluates to zero" $ property $ withMaxSuccess 10 $ propLinearizationPolyEvaluation @U1 @(Vector 1) @32 @(Vector 2)