From 380df8e086bffcaa5ebf56f1accb3f4ffbd19838 Mon Sep 17 00:00:00 2001 From: TurtlePU Date: Thu, 10 Oct 2024 04:59:53 +0300 Subject: [PATCH 1/4] removed TypeSize --- .../ZkFold/Base/Protocol/Protostar/Commit.hs | 9 +- .../ZkFold/Base/Protocol/Protostar/Fold.hs | 75 +++++---------- .../ZkFold/Symbolic/Algorithms/Hash/MiMC.hs | 9 +- symbolic-base/src/ZkFold/Symbolic/Compiler.hs | 84 +++++++++-------- .../Symbolic/Compiler/ArithmeticCircuit.hs | 7 +- .../Compiler/ArithmeticCircuit/Internal.hs | 28 +++++- .../src/ZkFold/Symbolic/Data/Bool.hs | 3 +- .../src/ZkFold/Symbolic/Data/ByteString.hs | 2 +- .../src/ZkFold/Symbolic/Data/Class.hs | 91 +++++-------------- .../src/ZkFold/Symbolic/Data/Combinators.hs | 6 +- .../src/ZkFold/Symbolic/Data/Conditional.hs | 28 ++++-- .../src/ZkFold/Symbolic/Data/Ed25519.hs | 35 ++++--- symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs | 12 +-- .../src/ZkFold/Symbolic/Data/Eq/Structural.hs | 4 +- .../src/ZkFold/Symbolic/Data/FieldElement.hs | 4 +- .../src/ZkFold/Symbolic/Data/List.hs | 3 +- .../src/ZkFold/Symbolic/Data/Maybe.hs | 39 ++++---- symbolic-base/src/ZkFold/Symbolic/Data/Ord.hs | 38 ++++---- .../src/ZkFold/Symbolic/Data/UInt.hs | 6 +- .../test/Tests/Arithmetization/Test1.hs | 10 +- .../test/Tests/Arithmetization/Test2.hs | 7 +- .../test/Tests/Arithmetization/Test3.hs | 7 +- .../test/Tests/Arithmetization/Test4.hs | 12 +-- symbolic-base/test/Tests/Blake2b.hs | 4 +- .../Cardano/Contracts/BatchTransfer.hs | 9 +- .../Cardano/Contracts/RandomOracle.hs | 4 +- .../ZkFold/Symbolic/Cardano/Types/Address.hs | 2 +- .../ZkFold/Symbolic/Cardano/Types/Input.hs | 12 +-- .../ZkFold/Symbolic/Cardano/Types/Output.hs | 10 +- .../Symbolic/Cardano/Types/OutputRef.hs | 2 +- .../Symbolic/Cardano/Types/Transaction.hs | 25 ++--- .../ZkFold/Symbolic/Cardano/Types/Value.hs | 6 +- .../ZkFold/Symbolic/Cardano/UPLC/Builtins.hs | 2 - .../src/ZkFold/Symbolic/Cardano/UPLC/Term.hs | 7 +- .../src/ZkFold/Symbolic/Cardano/UPLC/Type.hs | 7 +- symbolic-examples/bench/BenchCompiler.hs | 6 +- .../src/Examples/BatchTransfer.hs | 14 +-- .../src/ZkFold/Symbolic/Examples.hs | 41 +++++---- symbolic-examples/symbolic-examples.cabal | 1 + 39 files changed, 307 insertions(+), 364 deletions(-) diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Protostar/Commit.hs b/symbolic-base/src/ZkFold/Base/Protocol/Protostar/Commit.hs index 215e6c93d..30e99201f 100644 --- a/symbolic-base/src/ZkFold/Base/Protocol/Protostar/Commit.hs +++ b/symbolic-base/src/ZkFold/Base/Protocol/Protostar/Commit.hs @@ -1,18 +1,17 @@ -{-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module ZkFold.Base.Protocol.Protostar.Commit (Commit (..), HomomorphicCommit (..), PedersonSetup (..)) where import Data.Foldable (Foldable, toList) -import Prelude (type (~), zipWith, ($), (<$>)) +import Data.Functor.Rep (Representable) +import Prelude (Traversable, type (~), zipWith, ($), (<$>)) import ZkFold.Base.Algebra.Basic.Class import ZkFold.Base.Algebra.Basic.Number import ZkFold.Base.Algebra.EllipticCurve.BLS12_381 import ZkFold.Base.Algebra.EllipticCurve.Class as EC import ZkFold.Base.Algebra.EllipticCurve.Ed25519 -import ZkFold.Base.Data.Vector (Vector) import ZkFold.Base.Protocol.Protostar.Oracle import ZkFold.Symbolic.Class import ZkFold.Symbolic.Data.Class @@ -77,7 +76,9 @@ instance , SymbolicData (Point c) , Context (Point c) ~ ctx , PedersonSetup (Point c) - , Layout (Point c) ~ Vector n + , Layout (Point c) ~ l + , Representable l + , Traversable l ) => HomomorphicCommit (FieldElement ctx) (FieldElement ctx) (Point c) where hcommit r b = let (g, h) = pedersonGH @(Point c) in scale b g + scale r h diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Protostar/Fold.hs b/symbolic-base/src/ZkFold/Base/Protocol/Protostar/Fold.hs index 578c0da88..0f3c59cbf 100644 --- a/symbolic-base/src/ZkFold/Base/Protocol/Protostar/Fold.hs +++ b/symbolic-base/src/ZkFold/Base/Protocol/Protostar/Fold.hs @@ -9,17 +9,23 @@ module ZkFold.Base.Protocol.Protostar.Fold where import Control.DeepSeq (NFData) import Control.Lens ((^.)) +import Data.Binary (Binary) +import Data.Function ((.)) +import Data.Functor (fmap) +import Data.Functor.Rep (Representable) import Data.Kind (Type) import Data.Map.Strict (Map) import qualified Data.Map.Strict as M import Data.Proxy (Proxy) -import GHC.Generics (Generic, Par1) +import GHC.Generics (Generic, Par1 (..), U1 (..), type (:*:) (..), + type (:.:) (..)) import Prelude (type (~), ($), (<$>), (<*>)) import qualified Prelude as P import ZkFold.Base.Algebra.Basic.Class import ZkFold.Base.Algebra.Basic.Number import qualified ZkFold.Base.Algebra.Polynomials.Univariate as PU +import ZkFold.Base.Data.HFunctor (hmap) import ZkFold.Base.Data.Vector (Vector) import ZkFold.Base.Protocol.Protostar.Accumulator import qualified ZkFold.Base.Protocol.Protostar.AccumulatorScheme as Acc @@ -53,10 +59,10 @@ instance (Ring a, P.Ord key, KnownNat k) => Acc.LinearCombination (Map key a) (M linearCombination mx ma = M.unionWith (+) (P.flip PU.polyVecLinear zero <$> mx) (PU.polyVecConstant <$> ma) instance (Ring a, KnownNat n, KnownNat k) => Acc.LinearCombination (Vector n a) (Vector n (PU.PolyVec a k)) where - linearCombination mx ma = (+) <$> (P.flip PU.polyVecLinear zero <$> mx) <*> (PU.polyVecConstant <$> ma) + linearCombination mx ma = (+) . P.flip PU.polyVecLinear zero <$> mx <*> (PU.polyVecConstant <$> ma) instance (Ring a, KnownNat n) => Acc.LinearCombinationWith a (Vector n a) where - linearCombinationWith coeff a b = (+) <$> (P.fmap (coeff *) a) <*> b + linearCombinationWith coeff a b = (+) <$> P.fmap (coeff *) a <*> b type C n a = ArithmeticCircuit a (Vector n) (Vector n) @@ -82,7 +88,7 @@ toFS -> C n a -> Vector n (FieldElement ctx) -> FS_CM ctx n comm a -toFS ck rc v = FiatShamir (CommitOpen (hcommit ck) rc) v +toFS ck rc = FiatShamir (CommitOpen (hcommit ck) rc) -- No SymbolicData instances for data -- all protocols are one-round in case of arithmetic circuits, therefore we can replace lists with elements. @@ -94,7 +100,7 @@ ivcVerifier -> (a, (f, (f, f)), ((i, c, f, c, f), m)) -> Bool ctx ivcVerifier (i, pi_x, accTuple, acc'Tuple, pf) (a, ckTuple, dkTuple) - = (Acc.verifier @i @f @c @m @ctx @a i [pi_x] acc acc' [pf]) && (Acc.decider @i @f @c @m @ctx @a a ck dk) + = Acc.verifier @i @f @c @m @ctx @a i [pi_x] acc acc' [pf] && Acc.decider @i @f @c @m @ctx @a a ck dk where acc = let (x1, x2, x3, x4, x5) = accTuple in AccumulatorInstance x1 [x2] [x3] x4 x5 @@ -109,48 +115,14 @@ ivcVerifier (i, pi_x, accTuple, acc'Tuple, pf) (a, ckTuple, dkTuple) -- TODO: this is insane ivcVerifierAc - :: forall i f c m ctx a y typeSize ckSize dkSize accSize + :: forall i f c m ctx a y t . Symbolic ctx - => TypeSize y ~ 1 => SymbolicData i => SymbolicData f => SymbolicData c => SymbolicData m => SymbolicData a => SymbolicData y - => typeSize ~ ((TypeSize i - + (TypeSize c - + ((TypeSize i - + (TypeSize c + (TypeSize f + (TypeSize c + TypeSize f)))) - + ((TypeSize i - + (TypeSize c - + (TypeSize f + (TypeSize c + TypeSize f)))) - + TypeSize c)))) - + (TypeSize a - + ((TypeSize f + (TypeSize f + TypeSize f)) - + ((TypeSize i - + (TypeSize c + (TypeSize f + (TypeSize c + TypeSize f)))) - + TypeSize m)))) - => ckSize ~ (TypeSize f + (TypeSize f + TypeSize f)) - => dkSize ~ TypeSize a + ((TypeSize f + (TypeSize f + TypeSize f)) - + ((TypeSize i - + (TypeSize c + (TypeSize f + (TypeSize c + TypeSize f)))) - + TypeSize m)) - => accSize ~ (TypeSize i + (TypeSize c - + ((TypeSize i - + (TypeSize c + (TypeSize f + (TypeSize c + TypeSize f)))) - + ((TypeSize i - + (TypeSize c + (TypeSize f + (TypeSize c + TypeSize f)))) - + TypeSize c)))) - => KnownNat typeSize - => KnownNat dkSize - => KnownNat ckSize - => KnownNat accSize - => KnownNat (TypeSize i + (TypeSize c + (TypeSize f + (TypeSize c + TypeSize f)))) - => KnownNat (TypeSize i) - => KnownNat (TypeSize f) - => KnownNat (TypeSize c) - => KnownNat (TypeSize a) => Context i ~ ctx => Context f ~ ctx => Context c ~ ctx @@ -163,22 +135,23 @@ ivcVerifierAc => Support m ~ Proxy ctx => Support a ~ Proxy ctx => Support y ~ Proxy ctx - => Layout i ~ Vector (TypeSize i) - => Layout f ~ Vector (TypeSize f) - => Layout c ~ Vector (TypeSize c) - => Layout m ~ Vector (TypeSize m) - => Layout a ~ Vector (TypeSize a) - => Layout y ~ Vector (TypeSize y) - => ctx ~ ArithmeticCircuit a (Vector typeSize) + => Representable (Layout i) + => Representable (Layout c) + => Representable (Layout f) + => Representable (Layout a) + => Representable (Layout m) + => Layout y ~ Par1 + => t ~ ((i,c,(i,c,f,c,f),(i,c,f,c,f),c),(a,(f,f,f),(i,c,f,c,f),m),Proxy ctx) + => ctx ~ ArithmeticCircuit a (Layout t) => Acc.AccumulatorScheme i f c m ctx a => y ivcVerifierAc = compile (ivcVerifier @i @f @c @m @ctx @a) iterate :: forall ctx n comm a - . Symbolic ctx - => KnownNat n + . KnownNat n => Arithmetic a + => Binary a => Scale a (BaseField ctx) => FromConstant a (BaseField ctx) => Eq (Bool ctx) comm @@ -194,7 +167,7 @@ iterate => Scale (FieldElement ctx) comm => ctx ~ ArithmeticCircuit a (Vector n) => SPS.Input (FieldElement ctx) (C n a) ~ Vector n (FieldElement ctx) - => (Vector n (FieldElement ctx) -> Vector n (FieldElement ctx)) + => (forall c. (Symbolic c, BaseField c ~ a) => Vector n (FieldElement c) -> Vector n (FieldElement c)) -> Vector n a -> Natural -> ProtostarResult ctx n comm a @@ -204,7 +177,7 @@ iterate f i0 n = iteration n ck f ac i0_arith i0 initialAccumulator (Acc.KeyScal i0_arith = fromConstant <$> i0 ac :: C n a - ac = compile @a f + ac = hmap (fmap unPar1 . unComp1) $ hlmap ((:*: U1) . Comp1 . fmap Par1) (compile @a f) initE = hcommit ck $ replicate (SPS.outputLength @(FieldElement ctx) ac) (zero :: FieldElement ctx) diff --git a/symbolic-base/src/ZkFold/Symbolic/Algorithms/Hash/MiMC.hs b/symbolic-base/src/ZkFold/Symbolic/Algorithms/Hash/MiMC.hs index 7a3277847..6aedf7946 100644 --- a/symbolic-base/src/ZkFold/Symbolic/Algorithms/Hash/MiMC.hs +++ b/symbolic-base/src/ZkFold/Symbolic/Algorithms/Hash/MiMC.hs @@ -3,6 +3,7 @@ module ZkFold.Symbolic.Algorithms.Hash.MiMC where +import Data.Foldable (toList) import Data.List.NonEmpty (NonEmpty ((:|)), nonEmpty) import Data.Proxy (Proxy (..)) import Numeric.Natural (Natural) @@ -10,8 +11,8 @@ import Prelude hiding (Eq (..), (^), (||)) import ZkFold.Base.Algebra.Basic.Class +import ZkFold.Base.Data.HFunctor (hmap) import ZkFold.Base.Data.Package (unpacked) -import ZkFold.Base.Data.Vector (Vector, fromVector) import ZkFold.Symbolic.Algorithms.Hash.MiMC.Constants (mimcConstants) import ZkFold.Symbolic.Class import ZkFold.Symbolic.Data.Class @@ -39,12 +40,12 @@ mimcHashN xs k = go [zL, zR] -> mimcHash2 xs k zL zR (zL:zR:zs') -> go (mimcHash2 xs k zL zR : zs') -hash :: forall context x a size . +hash :: forall context x a . ( Symbolic context , SymbolicData x , BaseField context ~ a , Context x ~ context , Support x ~ Proxy context - , Layout x ~ Vector size + , Foldable (Layout x) ) => x -> FieldElement context -hash = mimcHashN mimcConstants (zero :: a) . fromVector . fmap FieldElement . unpacked . flip pieces Proxy +hash = mimcHashN mimcConstants (zero :: a) . fmap FieldElement . unpacked . hmap toList . flip pieces Proxy diff --git a/symbolic-base/src/ZkFold/Symbolic/Compiler.hs b/symbolic-base/src/ZkFold/Symbolic/Compiler.hs index 3109fa6b9..bd05040d7 100644 --- a/symbolic-base/src/ZkFold/Symbolic/Compiler.hs +++ b/symbolic-base/src/ZkFold/Symbolic/Compiler.hs @@ -14,14 +14,14 @@ import Data.Aeson (FromJSON, ToJSON) import Data.Binary (Binary) import Data.Function (const, (.)) import Data.Functor (($>)) +import Data.Functor.Rep (Rep, Representable) +import Data.Ord (Ord) import Data.Proxy (Proxy) import Data.Traversable (for) import Prelude (FilePath, IO, Monoid (mempty), Show (..), Traversable, putStrLn, type (~), ($), (++)) import ZkFold.Base.Algebra.Basic.Class -import ZkFold.Base.Algebra.Basic.Number -import ZkFold.Base.Data.Vector (Vector) import ZkFold.Prelude (writeFileJSON) import ZkFold.Symbolic.Class (Arithmetic, Symbolic (..)) import ZkFold.Symbolic.Compiler.ArithmeticCircuit @@ -43,80 +43,84 @@ forceOne r = fromCircuitF r (\fi -> for fi $ \i -> constraint (\x -> x i - one) -- | Arithmetizes an argument by feeding an appropriate amount of inputs. solder :: - forall a c f ni . - ( KnownNat ni - , c ~ ArithmeticCircuit a (Vector ni) + forall a c f s l . + ( c ~ ArithmeticCircuit a l , SymbolicData f , Context f ~ c - , SymbolicData (Support f) - , Context (Support f) ~ c - , Support (Support f) ~ Proxy c - , Layout f ~ Vector (TypeSize f) - , Layout (Support f) ~ Vector ni - ) => f -> c (Vector (TypeSize f)) + , Support f ~ s + , SymbolicData s + , Context s ~ c + , Support s ~ Proxy c + , Layout s ~ l + , Representable l + ) => f -> c (Layout f) solder f = pieces f (restore @(Support f) $ const inputC) where inputC = mempty { acOutput = acInput } -- | Compiles function `f` into an arithmetic circuit with all outputs equal to 1. compileForceOne :: - forall a c f y ni . - ( KnownNat ni - , c ~ ArithmeticCircuit a (Vector ni) + forall a c f s l y . + ( c ~ ArithmeticCircuit a l , Arithmetic a , Binary a , SymbolicData f , Context f ~ c - , SymbolicData (Support f) - , Context (Support f) ~ c - , Support (Support f) ~ Proxy c + , Support f ~ s + , SymbolicData s + , Context s ~ c + , Support s ~ Proxy c + , Layout s ~ l + , Representable l + , Binary (Rep l) + , Ord (Rep l) , SymbolicData y , Context y ~ c , Support y ~ Proxy c - , TypeSize f ~ TypeSize y - , Layout f ~ Vector (TypeSize y) - , Layout y ~ Vector (TypeSize y) - , Layout (Support f) ~ Vector ni + , Layout f ~ Layout y + , Traversable (Layout y) ) => f -> y compileForceOne = restore . const . optimize . forceOne . solder @a -- | Compiles function `f` into an arithmetic circuit. compile :: - forall a c f y ni . - ( KnownNat ni - , c ~ ArithmeticCircuit a (Vector ni) + forall a c f s l y . + ( c ~ ArithmeticCircuit a l , SymbolicData f , Context f ~ c - , SymbolicData (Support f) - , Context (Support f) ~ c - , Support (Support f) ~ Proxy c + , Support f ~ s + , SymbolicData s + , Context s ~ c + , Support s ~ Proxy c + , Layout s ~ l + , Representable l , SymbolicData y , Context y ~ c , Support y ~ Proxy c - , TypeSize f ~ TypeSize y - , Layout f ~ Vector (TypeSize y) - , Layout y ~ Vector (TypeSize y) - , Layout (Support f) ~ Vector ni + , Layout f ~ Layout y ) => f -> y compile = restore . const . optimize . solder @a -- | Compiles a function `f` into an arithmetic circuit. Writes the result to a file. compileIO :: - forall a c f ni . - ( KnownNat ni - , c ~ ArithmeticCircuit a (Vector ni) + forall a c f s l . + ( c ~ ArithmeticCircuit a l , FromJSON a , ToJSON a , SymbolicData f , Context f ~ c - , SymbolicData (Support f) - , Context (Support f) ~ c - , Support (Support f) ~ Proxy c - , Layout f ~ Vector (TypeSize f) - , Layout (Support f) ~ Vector ni + , Support f ~ s + , ToJSON (Layout f (Var a l)) + , SymbolicData s + , Context s ~ c + , Support s ~ Proxy c + , Layout s ~ l + , Representable l + , FromJSON (Rep l) + , ToJSON (Rep l) ) => FilePath -> f -> IO () compileIO scriptFile f = do - let ac = optimize (solder @a f) :: c (Vector (TypeSize f)) + let ac = optimize (solder @a f) :: c (Layout f) putStrLn "\nCompiling the script...\n" diff --git a/symbolic-base/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit.hs b/symbolic-base/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit.hs index c7302735e..0cd7b2667 100644 --- a/symbolic-base/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit.hs +++ b/symbolic-base/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit.hs @@ -1,10 +1,8 @@ -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE TypeOperators #-} - module ZkFold.Symbolic.Compiler.ArithmeticCircuit ( ArithmeticCircuit, ArithmeticCircuitTest(..), Constraint, + Var, witnessGenerator, -- high-level functions optimize, @@ -22,6 +20,7 @@ module ZkFold.Symbolic.Compiler.ArithmeticCircuit ( acValue, acPrint, -- Variable mapping functions + hlmap, mapVarArithmeticCircuit, -- Arithmetization type fields acWitness, @@ -53,7 +52,7 @@ import ZkFold.Prelude (length) import ZkFold.Symbolic.Compiler.ArithmeticCircuit.Instance () import ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal (Arithmetic, ArithmeticCircuit (..), Constraint, SysVar (..), Var (..), acInput, eval, eval1, exec, - exec1, witnessGenerator) + exec1, hlmap, witnessGenerator) import ZkFold.Symbolic.Compiler.ArithmeticCircuit.Map import ZkFold.Symbolic.Data.Combinators (expansion) import ZkFold.Symbolic.MonadCircuit (MonadCircuit (..)) diff --git a/symbolic-base/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit/Internal.hs b/symbolic-base/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit/Internal.hs index 5341e1122..331b20db3 100644 --- a/symbolic-base/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit/Internal.hs +++ b/symbolic-base/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit/Internal.hs @@ -15,6 +15,8 @@ module ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal ( -- variable getters acInput, getAllVars, + -- input mapping + hlmap, -- evaluation functions witnessGenerator, eval, @@ -45,7 +47,7 @@ import Prelude hiding (N import ZkFold.Base.Algebra.Basic.Class import ZkFold.Base.Algebra.Basic.Field (Zp) import ZkFold.Base.Algebra.Basic.Number -import ZkFold.Base.Algebra.Polynomials.Multivariate (Poly, evalMonomial, evalPolynomial, var) +import ZkFold.Base.Algebra.Polynomials.Multivariate (Poly, evalMonomial, evalPolynomial, var, mapVars) import ZkFold.Base.Control.HApplicative import ZkFold.Base.Data.HFunctor import ZkFold.Base.Data.Package @@ -94,6 +96,12 @@ deriving stock instance Eq (Rep i) => Eq (SysVar i) deriving stock instance Ord (Rep i) => Ord (SysVar i) deriving instance NFData (Rep i) => NFData (SysVar i) +imapSysVar :: + (Representable i, Representable j) => + (forall x. j x -> i x) -> SysVar i -> SysVar j +imapSysVar f (InVar r) = index (f (tabulate InVar)) r +imapSysVar _ (NewVar b) = NewVar b + data Var a i = SysVar (SysVar i) | ConstVar a @@ -109,6 +117,12 @@ deriving instance (NFData (Rep i), NFData a) => NFData (Var a i) instance FromConstant a (Var a i) where fromConstant = ConstVar +imapVar :: + (Representable i, Representable j) => + (forall x. j x -> i x) -> Var a i -> Var a j +imapVar f (SysVar s) = SysVar (imapSysVar f s) +imapVar _ (ConstVar c) = ConstVar c + ---------------------------------- Variables ----------------------------------- acInput :: Representable i => i (Var a i) @@ -127,6 +141,18 @@ indexW circuit inputs = \case (witnessGenerator circuit inputs !? newV) ConstVar cV -> cV +-------------------------------- "HProfunctor" --------------------------------- + +hlmap :: + (Representable i, Representable j, Ord (Rep j), Functor o) => + (forall x . j x -> i x) -> ArithmeticCircuit a i o -> ArithmeticCircuit a j o +hlmap f (ArithmeticCircuit s r w o) = ArithmeticCircuit + { acSystem = mapVars (imapSysVar f) <$> s + , acRange = r + , acWitness = (\g j p -> g (f j) p) <$> w + , acOutput = imapVar f <$> o + } + --------------------------- Symbolic compiler context -------------------------- crown :: ArithmeticCircuit a i g -> f (Var a i) -> ArithmeticCircuit a i f diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Bool.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Bool.hs index cb3962d4a..4ddaf1310 100644 --- a/symbolic-base/src/ZkFold/Symbolic/Data/Bool.hs +++ b/symbolic-base/src/ZkFold/Symbolic/Data/Bool.hs @@ -21,7 +21,6 @@ import qualified Prelude as Haskell import Text.Show (Show) import ZkFold.Base.Algebra.Basic.Class -import ZkFold.Base.Data.HFunctor (HFunctor) import ZkFold.Symbolic.Class import ZkFold.Symbolic.Data.Class (SymbolicData) import ZkFold.Symbolic.Interpreter (Interpreter (..)) @@ -66,7 +65,7 @@ deriving instance Show (c Par1) => Show (Bool c) instance {-# OVERLAPPING #-} (Eq a, MultiplicativeMonoid a) => Show (Bool (Interpreter a)) where show (fromBool -> x) = if x == one then "True" else "False" -deriving newtype instance HFunctor c => SymbolicData (Bool c) +deriving newtype instance SymbolicData (Bool c) instance Symbolic c => BoolType (Bool c) where true = Bool $ embed (Par1 one) diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/ByteString.hs b/symbolic-base/src/ZkFold/Symbolic/Data/ByteString.hs index 1d452d8d2..72988769b 100644 --- a/symbolic-base/src/ZkFold/Symbolic/Data/ByteString.hs +++ b/symbolic-base/src/ZkFold/Symbolic/Data/ByteString.hs @@ -68,7 +68,7 @@ deriving newtype instance SymbolicData (ByteString n c) deriving via (Structural (ByteString n c)) - instance (Symbolic c) => Eq (Bool c) (ByteString n c) + instance (Symbolic c, KnownNat n) => Eq (Bool c) (ByteString n c) instance ( Symbolic c diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Class.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Class.hs index 65a412bc3..f9738bb03 100644 --- a/symbolic-base/src/ZkFold/Symbolic/Data/Class.hs +++ b/symbolic-base/src/ZkFold/Symbolic/Data/Class.hs @@ -1,39 +1,32 @@ -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE NoStarIsType #-} -{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module ZkFold.Symbolic.Data.Class ( SomeData (..), SymbolicData (..), - typeSize ) where import Control.Applicative ((<*>)) -import Data.Function (const, flip, ($), (.)) +import Data.Function (flip, (.)) import Data.Functor ((<$>)) -import Data.Functor.Rep (Representable (tabulate)) +import Data.Functor.Rep (Representable (..)) import Data.Kind (Type) import Data.Type.Equality (type (~)) import Data.Typeable (Proxy (..), Typeable) -import GHC.Generics (Par1 (..)) +import GHC.Generics (U1 (..), (:*:) (..), (:.:) (..)) -import ZkFold.Base.Algebra.Basic.Field (fromZp) -import ZkFold.Base.Algebra.Basic.Number (KnownNat, Natural, type (*), type (+), value) +import ZkFold.Base.Algebra.Basic.Number (KnownNat) import ZkFold.Base.Control.HApplicative (HApplicative, hliftA2, hpure) -import ZkFold.Base.Data.HFunctor (HFunctor, hmap) -import ZkFold.Base.Data.Package (Package, packWith) -import qualified ZkFold.Base.Data.Vector as V +import ZkFold.Base.Data.HFunctor (hmap) +import ZkFold.Base.Data.Package (Package, pack) +import ZkFold.Base.Data.Product (fstP, sndP) import ZkFold.Base.Data.Vector (Vector) -- | A class for Symbolic data types. class SymbolicData x where type Context x :: (Type -> Type) -> Type type Support x :: Type - type TypeSize x :: Natural type Layout x :: Type -> Type - type Layout x = Vector (TypeSize x) -- | Returns the circuit that makes up `x`. pieces :: x -> Support x -> Context x (Layout x) @@ -41,36 +34,24 @@ class SymbolicData x where -- | Restores `x` from the circuit's outputs. restore :: (Support x -> Context x (Layout x)) -> x --- | Returns the number of finite field elements needed to describe `x`. -typeSize :: forall x . KnownNat (TypeSize x) => Natural -typeSize = value @(TypeSize x) - -- A wrapper for `SymbolicData` types. data SomeData c where SomeData :: (Typeable t, SymbolicData t, Context t ~ c) => t -> SomeData c -instance SymbolicData (c (Vector n)) where - type Context (c (Vector n)) = c - type Support (c (Vector n)) = Proxy c - type TypeSize (c (Vector n)) = n +instance SymbolicData (c (f :: Type -> Type)) where + type Context (c f) = c + type Support (c f) = Proxy c + type Layout (c f) = f pieces x _ = x restore f = f Proxy -instance HFunctor c => SymbolicData (c Par1) where - type Context (c Par1) = c - type Support (c Par1) = Proxy c - type TypeSize (c Par1) = 1 - - pieces = const . hmap (V.singleton . unPar1) - restore = hmap (Par1 . V.item) . ($ Proxy) - instance HApplicative c => SymbolicData (Proxy (c :: (Type -> Type) -> Type)) where type Context (Proxy c) = c type Support (Proxy c) = Proxy c - type TypeSize (Proxy c) = 0 + type Layout (Proxy c) = U1 - pieces _ _ = hpure V.empty + pieces _ _ = hpure U1 restore _ = Proxy instance @@ -79,17 +60,14 @@ instance , HApplicative (Context x) , Context x ~ Context y , Support x ~ Support y - , KnownNat (TypeSize x) - , Layout x ~ Vector (TypeSize x) - , Layout y ~ Vector (TypeSize y) ) => SymbolicData (x, y) where type Context (x, y) = Context x type Support (x, y) = Support x - type TypeSize (x, y) = TypeSize x + TypeSize y + type Layout (x, y) = Layout x :*: Layout y - pieces (a, b) = hliftA2 V.append <$> pieces a <*> pieces b - restore f = (restore (hmap V.take . f), restore (hmap V.drop . f)) + pieces (a, b) = hliftA2 (:*:) <$> pieces a <*> pieces b + restore f = (restore (hmap fstP . f), restore (hmap sndP . f)) instance ( SymbolicData x @@ -100,16 +78,11 @@ instance , Context y ~ Context z , Support x ~ Support y , Support y ~ Support z - , KnownNat (TypeSize x) - , KnownNat (TypeSize y) - , Layout x ~ Vector (TypeSize x) - , Layout y ~ Vector (TypeSize y) - , Layout z ~ Vector (TypeSize z) ) => SymbolicData (x, y, z) where type Context (x, y, z) = Context (x, (y, z)) type Support (x, y, z) = Support (x, (y, z)) - type TypeSize (x, y, z) = TypeSize (x, (y, z)) + type Layout (x, y, z) = Layout (x, (y, z)) pieces (a, b, c) = pieces (a, (b, c)) restore f = let (a, (b, c)) = restore f in (a, b, c) @@ -126,18 +99,11 @@ instance , Support w ~ Support x , Support x ~ Support y , Support y ~ Support z - , KnownNat (TypeSize w) - , KnownNat (TypeSize x) - , KnownNat (TypeSize y) - , Layout w ~ Vector (TypeSize w) - , Layout x ~ Vector (TypeSize x) - , Layout y ~ Vector (TypeSize y) - , Layout z ~ Vector (TypeSize z) ) => SymbolicData (w, x, y, z) where type Context (w, x, y, z) = Context (w, (x, y, z)) type Support (w, x, y, z) = Support (w, (x, y, z)) - type TypeSize (w, x, y, z) = TypeSize (w, (x, y, z)) + type Layout (w, x, y, z) = Layout (w, (x, y, z)) pieces (a, b, c, d) = pieces (a, (b, c, d)) restore f = let (a, (b, c, d)) = restore f in (a, b, c, d) @@ -157,44 +123,31 @@ instance , Support w ~ Support x , Support x ~ Support y , Support y ~ Support z - , KnownNat (TypeSize v) - , KnownNat (TypeSize w) - , KnownNat (TypeSize x) - , KnownNat (TypeSize y) - , Layout v ~ Vector (TypeSize v) - , Layout w ~ Vector (TypeSize w) - , Layout x ~ Vector (TypeSize x) - , Layout y ~ Vector (TypeSize y) - , Layout z ~ Vector (TypeSize z) ) => SymbolicData (v, w, x, y, z) where type Context (v, w, x, y, z) = Context (v, (w, x, y, z)) type Support (v, w, x, y, z) = Support (v, (w, x, y, z)) - type TypeSize (v, w, x, y, z) = TypeSize (v, (w, x, y, z)) + type Layout (v, w, x, y, z) = Layout (v, (w, x, y, z)) pieces (a, b, c, d, e) = pieces (a, (b, c, d, e)) - restore f = let (a, (b, c, d, e)) = restore f in (a, b, c, d, e) instance ( SymbolicData x , Package (Context x) - , KnownNat (TypeSize x) , KnownNat n - , Layout x ~ Vector (TypeSize x) ) => SymbolicData (Vector n x) where type Context (Vector n x) = Context x type Support (Vector n x) = Support x - type TypeSize (Vector n x) = n * TypeSize x + type Layout (Vector n x) = Vector n :.: Layout x - pieces xs i = packWith V.concat (flip pieces i <$> xs) - restore f = tabulate (\i -> restore (hmap ((V.!! fromZp i) . V.chunks @n) . f)) + pieces xs i = pack (flip pieces i <$> xs) + restore f = tabulate (\i -> restore (hmap (flip index i . unComp1) . f)) instance SymbolicData f => SymbolicData (x -> f) where type Context (x -> f) = Context f type Support (x -> f) = (x, Support f) - type TypeSize (x -> f) = TypeSize f type Layout (x -> f) = Layout f pieces f (x, i) = pieces (f x) i diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Combinators.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Combinators.hs index 29e1127d7..a39cad629 100644 --- a/symbolic-base/src/ZkFold/Symbolic/Data/Combinators.hs +++ b/symbolic-base/src/ZkFold/Symbolic/Data/Combinators.hs @@ -8,6 +8,7 @@ module ZkFold.Symbolic.Data.Combinators where import Control.Monad (mapM) import Data.Foldable (foldlM) +import Data.Functor.Rep (Representable, mzipRep) import Data.Kind (Type) import Data.List (find, splitAt) import Data.List.Split (chunksOf) @@ -17,7 +18,6 @@ import Data.Ratio ((%)) import Data.Traversable (Traversable, for) import Data.Type.Bool (If) import Data.Type.Ord -import qualified Data.Zip as Z import GHC.Base (const, return) import GHC.List (reverse) import GHC.TypeNats @@ -222,8 +222,8 @@ splitExpansion n1 n2 k = do . (`div` fromConstant @Natural (2 ^ n1)) . toConstant -runInvert :: (MonadCircuit i a m, Z.Zip f, Traversable f) => f i -> m (f i, f i) +runInvert :: (MonadCircuit i a m, Representable f, Traversable f) => f i -> m (f i, f i) runInvert is = do js <- for is $ \i -> newConstrained (\x j -> x i * x j) (\x -> let xi = x i in one - xi // xi) - ks <- for (Z.zip is js) $ \(i, j) -> newConstrained (\x k -> x i * x k + x j - one) (finv . ($ i)) + ks <- for (mzipRep is js) $ \(i, j) -> newConstrained (\x k -> x i * x k + x j - one) (finv . ($ i)) return (js, ks) diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Conditional.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Conditional.hs index 40c2ab947..dc5c319f8 100644 --- a/symbolic-base/src/ZkFold/Symbolic/Data/Conditional.hs +++ b/symbolic-base/src/ZkFold/Symbolic/Data/Conditional.hs @@ -1,17 +1,20 @@ -{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} module ZkFold.Symbolic.Data.Conditional where -import Data.Function (($)) -import Data.Type.Equality (type (~)) -import GHC.Generics (Par1 (Par1)) +import Control.Applicative (Applicative) +import Control.Monad.Representable.Reader (Representable, mzipWithRep) +import Data.Function (($)) +import Data.Traversable (Traversable, sequenceA) +import Data.Type.Equality (type (~)) +import GHC.Generics (Par1 (Par1)) import ZkFold.Base.Algebra.Basic.Class -import ZkFold.Base.Data.Vector (Vector, zipWithM) import ZkFold.Symbolic.Class -import ZkFold.Symbolic.Data.Bool (Bool (Bool), BoolType) +import ZkFold.Symbolic.Data.Bool (Bool (Bool), BoolType) import ZkFold.Symbolic.Data.Class -import ZkFold.Symbolic.MonadCircuit (newAssigned) +import ZkFold.Symbolic.MonadCircuit (newAssigned) class BoolType b => Conditional b a where -- | Properties: @@ -27,10 +30,17 @@ gif b x y = bool y x b (?) :: Conditional b a => b -> a -> a -> a (?) = gif -instance (SymbolicData x, Context x ~ c, Symbolic c, Layout x ~ Vector n) => Conditional (Bool c) x where +mzipWithMRep :: + (Representable f, Traversable f, Applicative m) => + (a -> b -> m c) -> f a -> f b -> m (f c) +mzipWithMRep f x y = sequenceA (mzipWithRep f x y) + +instance ( SymbolicData x, Context x ~ c, Symbolic c + , Representable (Layout x), Traversable (Layout x) + ) => Conditional (Bool c) x where bool x y (Bool b) = restore $ \s -> fromCircuit3F b (pieces x s) (pieces y s) $ \(Par1 c) -> - zipWithM $ \i j -> do + mzipWithMRep $ \i j -> do i' <- newAssigned (\w -> (one - w c) * w i) j' <- newAssigned (\w -> w c * w j) newAssigned (\w -> w i' + w j') diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Ed25519.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Ed25519.hs index 621e9d9e1..7a4e2d619 100644 --- a/symbolic-base/src/ZkFold/Symbolic/Data/Ed25519.hs +++ b/symbolic-base/src/ZkFold/Symbolic/Data/Ed25519.hs @@ -6,9 +6,7 @@ module ZkFold.Symbolic.Data.Ed25519 where -import Control.Applicative ((<*>)) import Control.DeepSeq (NFData, force) -import Data.Functor ((<$>)) import Prelude (type (~), ($)) import qualified Prelude as P @@ -17,7 +15,6 @@ import ZkFold.Base.Algebra.Basic.Field import ZkFold.Base.Algebra.Basic.Number import ZkFold.Base.Algebra.EllipticCurve.Class import ZkFold.Base.Algebra.EllipticCurve.Ed25519 -import ZkFold.Base.Control.HApplicative (hliftA2) import qualified ZkFold.Base.Data.Vector as V import qualified ZkFold.Symbolic.Class as S import ZkFold.Symbolic.Class (Symbolic) @@ -29,18 +26,15 @@ import ZkFold.Symbolic.Data.Conditional import ZkFold.Symbolic.Data.Eq import ZkFold.Symbolic.Data.FieldElement import ZkFold.Symbolic.Data.UInt +import Data.Functor.Rep (Representable) +import Data.Traversable (Traversable) -instance - ( Symbolic c - , S.BaseField c ~ a - , r ~ NumberOfRegisters a 256 'Auto - , KnownNat r - ) => SymbolicData (Point (Ed25519 c)) where +instance Symbolic c => SymbolicData (Point (Ed25519 c)) where type Context (Point (Ed25519 c)) = c type Support (Point (Ed25519 c)) = Support (UInt 256 'Auto c) - type TypeSize (Point (Ed25519 c)) = TypeSize (UInt 256 'Auto c) + TypeSize (UInt 256 'Auto c) + type Layout (Point (Ed25519 c)) = Layout (UInt 256 'Auto c, UInt 256 'Auto 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. @@ -49,8 +43,8 @@ instance -- It will need additional checks in pointDouble because of the denominator becoming zero, though. -- TODO: Think of a better solution -- - pieces Inf = hliftA2 V.append <$> pieces (zero :: UInt 256 'Auto c) <*> pieces (zero :: UInt 256 'Auto c) - pieces (Point x y) = hliftA2 V.append <$> pieces x <*> pieces y + pieces Inf = pieces (zero :: UInt 256 'Auto c, zero :: UInt 256 'Auto c) + pieces (Point x y) = pieces (x, y) restore f = Point x y where @@ -96,13 +90,16 @@ instance bits = from sc instance - ( Symbolic ctx - , EllipticCurve curve - , SymbolicData (Point curve) - , Context (Point curve) ~ ctx - , bits ~ NumberOfBits (S.BaseField ctx) - , Layout (Point curve) ~ V.Vector n - ) => Scale (FieldElement ctx) (Point curve) where + ( EllipticCurve c + , SymbolicData (Point c) + , l ~ Layout (Point c) + , Representable l + , Traversable l + , ctx ~ Context (Point c) + , Symbolic ctx + , a ~ S.BaseField ctx + , bits ~ NumberOfBits a + ) => Scale (FieldElement ctx) (Point c) where scale sc x = sum $ P.zipWith (\b p -> bool @(Bool ctx) zero p (isSet bits b)) [upper, upper -! 1 .. 0] (P.iterate (\e -> e + e) x) where diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs index 2a927380b..3be573540 100644 --- a/symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs +++ b/symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs @@ -7,8 +7,8 @@ module ZkFold.Symbolic.Data.Eq ( import Data.Bool (bool) import Data.Foldable (Foldable) +import Data.Functor.Rep (Representable, mzipRep, mzipWithRep) import Data.Traversable (Traversable, for) -import qualified Data.Zip as Z import Prelude (return, ($)) import qualified Prelude as Haskell @@ -33,14 +33,14 @@ instance Haskell.Eq a => Eq Haskell.Bool a where (==) = (Haskell.==) (/=) = (Haskell./=) -instance (Symbolic c, Haskell.Eq (BaseField c), Z.Zip f, Traversable f) +instance (Symbolic c, Haskell.Eq (BaseField c), Representable f, Traversable f) => Eq (Bool c) (c f) where x == y = let result = symbolic2F x y - (Z.zipWith (\i j -> bool zero one (i Haskell.== j))) + (mzipWithRep (\i j -> bool zero one (i Haskell.== j))) (\x' y' -> do - difference <- for (Z.zip x' y') $ \(i, j) -> + difference <- for (mzipRep x' y') $ \(i, j) -> newAssigned (\w -> w i - w j) (isZeros, _) <- runInvert difference return isZeros @@ -51,9 +51,9 @@ instance (Symbolic c, Haskell.Eq (BaseField c), Z.Zip f, Traversable f) x /= y = let result = symbolic2F x y - (Z.zipWith (\i j -> bool zero one (i Haskell./= j))) + (mzipWithRep (\i j -> bool zero one (i Haskell./= j))) (\x' y' -> do - difference <- for (Z.zip x' y') $ \(i, j) -> + difference <- for (mzipRep x' y') $ \(i, j) -> newAssigned (\w -> w i - w j) (isZeros, _) <- runInvert difference for isZeros $ \isZ -> diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Eq/Structural.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Eq/Structural.hs index 7813e0db9..1777f42ad 100644 --- a/symbolic-base/src/ZkFold/Symbolic/Data/Eq/Structural.hs +++ b/symbolic-base/src/ZkFold/Symbolic/Data/Eq/Structural.hs @@ -3,9 +3,9 @@ module ZkFold.Symbolic.Data.Eq.Structural where +import Data.Functor.Rep (Representable) import Data.Proxy (Proxy (..)) import Data.Traversable (Traversable) -import Data.Zip (Zip) import Prelude (type (~)) import ZkFold.Symbolic.Class @@ -21,7 +21,7 @@ instance , Context x ~ c , Support x ~ Proxy c , Symbolic c - , Zip (Layout x) + , Representable (Layout x) , Traversable (Layout x) ) => Eq (Bool c) (Structural x) where diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/FieldElement.hs b/symbolic-base/src/ZkFold/Symbolic/Data/FieldElement.hs index df28b43c5..693b00571 100644 --- a/symbolic-base/src/ZkFold/Symbolic/Data/FieldElement.hs +++ b/symbolic-base/src/ZkFold/Symbolic/Data/FieldElement.hs @@ -15,7 +15,7 @@ import qualified Prelude as Haskell import ZkFold.Base.Algebra.Basic.Class import ZkFold.Base.Algebra.Basic.Number -import ZkFold.Base.Data.HFunctor (HFunctor, hmap) +import ZkFold.Base.Data.HFunctor (hmap) import ZkFold.Base.Data.Par1 () import ZkFold.Base.Data.Vector (Vector, fromVector, unsafeToVector) import ZkFold.Symbolic.Class @@ -37,7 +37,7 @@ deriving stock instance Haskell.Ord (c Par1) => Haskell.Ord (FieldElement c) deriving newtype instance NFData (c Par1) => NFData (FieldElement c) -deriving newtype instance HFunctor c => SymbolicData (FieldElement c) +deriving newtype instance SymbolicData (FieldElement c) deriving newtype instance Symbolic c => Eq (Bool c) (FieldElement c) diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/List.hs b/symbolic-base/src/ZkFold/Symbolic/Data/List.hs index b09e212b7..8849cf51a 100644 --- a/symbolic-base/src/ZkFold/Symbolic/Data/List.hs +++ b/symbolic-base/src/ZkFold/Symbolic/Data/List.hs @@ -5,11 +5,10 @@ import Data.Kind (Type) import GHC.Generics (Par1) import Prelude (flip, undefined, (.)) -import ZkFold.Base.Data.Vector (Vector) import ZkFold.Symbolic.Data.Bool (Bool) import ZkFold.Symbolic.Data.Class -data List (context :: (Type -> Type) -> Type) x = List (context (Vector (TypeSize x))) (context Par1) +data List (context :: (Type -> Type) -> Type) x = List (context (Layout x)) (context Par1) emptyList :: List context x emptyList = undefined diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Maybe.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Maybe.hs index d1a9e714b..a2b206d33 100644 --- a/symbolic-base/src/ZkFold/Symbolic/Data/Maybe.hs +++ b/symbolic-base/src/ZkFold/Symbolic/Data/Maybe.hs @@ -8,14 +8,15 @@ module ZkFold.Symbolic.Data.Maybe ( ) where import Data.Function ((.)) +import Data.Functor.Rep (Representable, pureRep) import Data.Proxy (Proxy) +import Data.Traversable (Traversable) import GHC.Generics (Par1 (..)) import Prelude (foldr, type (~), ($)) import qualified Prelude as Haskell import ZkFold.Base.Algebra.Basic.Class -import ZkFold.Base.Algebra.Basic.Number -import ZkFold.Base.Control.HApplicative (HApplicative, hliftA2) +import ZkFold.Base.Control.HApplicative (HApplicative) import ZkFold.Base.Data.HFunctor (HFunctor, hmap) import qualified ZkFold.Base.Data.Vector as V import ZkFold.Base.Data.Vector (Vector) @@ -36,15 +37,11 @@ deriving stock instance (Haskell.Eq (context Par1), Haskell.Eq x) => Haskell.Eq just :: Symbolic c => x -> Maybe c x just = Maybe true -nothing - :: forall c x k - . Symbolic c - => SymbolicData x - => c ~ Context x - => KnownNat k - => Layout x ~ Vector k - => Maybe c x -nothing = Maybe false (let c = embed @c $ Haskell.pure @(Vector k) zero in restore (Haskell.const c)) +nothing :: + forall x c . + (SymbolicData x, Representable (Layout x), Context x ~ c, Symbolic c) => + Maybe c x +nothing = Maybe false (let c = embed @c $ pureRep zero in restore (Haskell.const c)) fromMaybe :: forall c x @@ -74,22 +71,24 @@ instance , SymbolicData x , Context x ~ c , Support x ~ Proxy c - , Layout x ~ Vector (TypeSize x) ) => SymbolicData (Maybe c x) where - type Context (Maybe c x) = c - type Support (Maybe c x) = Proxy c - type TypeSize (Maybe c x) = 1 + TypeSize x - pieces (Maybe (Bool h) t) i = hliftA2 (\(Par1 h') t' -> V.singleton h' `V.append` t') h (pieces t i) - restore f = Maybe (restore (hmap V.take . f)) (restore (hmap V.drop . f)) + type Context (Maybe c x) = Context (Bool c, x) + type Support (Maybe c x) = Support (Bool c, x) + type Layout (Maybe c x) = Layout (Bool c, x) + + pieces (Maybe b t) = pieces (b, t) + restore f = let (b, t) = restore f in Maybe b t -maybe :: forall a b c n . - (Symbolic c, SymbolicData b, Context b ~ c, Layout b ~ Vector n) => +maybe :: forall a b c . + (Symbolic c, SymbolicData b, Context b ~ c) => + (Representable (Layout b), Traversable (Layout b)) => b -> (a -> b) -> Maybe c a -> b maybe d h x@(Maybe _ v) = bool @(Bool c) d (h v) $ isNothing x find :: forall a c t . - (Symbolic c, SymbolicData a, Context a ~ c, Support a ~ Proxy c, KnownNat (TypeSize a), Layout a ~ Vector (TypeSize a)) => + (Symbolic c, SymbolicData a, Context a ~ c, Support a ~ Proxy c) => + (Representable (Layout a), Traversable (Layout a)) => Haskell.Foldable t => (a -> Bool c) -> t a -> Maybe c a find p = let n = nothing in diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Ord.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Ord.hs index dec66709e..72f99ffcf 100644 --- a/symbolic-base/src/ZkFold/Symbolic/Data/Ord.hs +++ b/symbolic-base/src/ZkFold/Symbolic/Data/Ord.hs @@ -1,27 +1,27 @@ -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE DerivingVia #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DerivingVia #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} module ZkFold.Symbolic.Data.Ord (Ord (..), Lexicographical (..), blueprintGE, bitwiseGE, bitwiseGT, getBitsBE) where import Control.Monad (foldM) import qualified Data.Bool as Haskell import Data.Data (Proxy (..)) -import Data.Foldable (Foldable, toList) +import Data.Foldable (Foldable, concatMap, toList) import Data.Function ((.)) -import Data.Functor ((<$>)) -import Data.List (map) +import Data.Functor (fmap, (<$>)) +import Data.Functor.Rep (Representable) +import Data.List (map, reverse) +import Data.Traversable (Traversable, traverse) import qualified Data.Zip as Z import GHC.Generics (Par1 (..)) import Prelude (type (~), ($)) import qualified Prelude as Haskell import ZkFold.Base.Algebra.Basic.Class -import ZkFold.Base.Data.HFunctor (hmap) -import qualified ZkFold.Base.Data.Vector as V -import ZkFold.Base.Data.Vector (Vector, unsafeToVector) -import ZkFold.Symbolic.Class (Symbolic (BaseField, symbolicF), symbolic2F) +import ZkFold.Symbolic.Class (Symbolic (..), symbolic2F) import ZkFold.Symbolic.Data.Bool (Bool (..)) import ZkFold.Symbolic.Data.Class import ZkFold.Symbolic.Data.Combinators (expansion) @@ -69,8 +69,8 @@ instance , SymbolicData x , Context x ~ c , Support x ~ Proxy c - , TypeSize x ~ 1 - , Layout x ~ Vector 1 + , Representable (Layout x) + , Traversable (Layout x) ) => Ord (Bool c) (Lexicographical x) where x <= y = y >= x @@ -87,15 +87,13 @@ instance getBitsBE :: forall c x . - (Symbolic c, SymbolicData x, Context x ~ c, Support x ~ Proxy c, Layout x ~ Vector 1) => - x -> c (V.Vector (NumberOfBits (BaseField c))) + (Symbolic c, SymbolicData x, Context x ~ c, Support x ~ Proxy c, Foldable (Layout x)) => + x -> c [] -- ^ @getBitsBE x@ returns a list of circuits computing bits of @x@, eldest to -- youngest. -getBitsBE x = - hmap (V.reverse . unsafeToVector) - $ symbolicF (pieces x Proxy) - (padBits n . map fromConstant . binaryExpansion . toConstant . V.item) - (expansion n . V.item) +getBitsBE x = symbolicF (pieces x Proxy) + (concatMap (reverse . padBits n . map fromConstant . binaryExpansion . toConstant)) + (fmap (concatMap reverse) . traverse (expansion n) . toList) where n = numberOfBits @(BaseField c) bitwiseGE :: forall c f . (Symbolic c, Z.Zip f, Foldable f) => c f -> c f -> Bool c diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/UInt.hs b/symbolic-base/src/ZkFold/Symbolic/Data/UInt.hs index e088edcbe..748d8d9aa 100644 --- a/symbolic-base/src/ZkFold/Symbolic/Data/UInt.hs +++ b/symbolic-base/src/ZkFold/Symbolic/Data/UInt.hs @@ -228,7 +228,9 @@ instance let rs = force $ addBit (r' + r') (value @n -! i -! 1) in bool @(Bool c) (q', rs) (q' + fromConstant ((2 :: Natural) ^ i), rs - d) (rs >= d) -instance (Symbolic c, KnownNat n, KnownRegisterSize r) => Ord (Bool c) (UInt n r c) where +instance ( Symbolic c, KnownNat n, KnownRegisterSize r + , KnownNat (NumberOfRegisters (BaseField c) n r) + ) => Ord (Bool c) (UInt n r c) where x <= y = y >= x x < y = y > x @@ -382,7 +384,7 @@ instance ) => Ring (UInt n r c) deriving via (Structural (UInt n rs c)) - instance (Symbolic c) => + instance (Symbolic c, KnownNat (NumberOfRegisters (BaseField c) n rs)) => Eq (Bool c) (UInt n rs c) -------------------------------------------------------------------------------- diff --git a/symbolic-base/test/Tests/Arithmetization/Test1.hs b/symbolic-base/test/Tests/Arithmetization/Test1.hs index 19429b379..a046e3cc5 100644 --- a/symbolic-base/test/Tests/Arithmetization/Test1.hs +++ b/symbolic-base/test/Tests/Arithmetization/Test1.hs @@ -1,10 +1,11 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} module Tests.Arithmetization.Test1 (specArithmetization1) where import Data.Binary (Binary) -import GHC.Generics (Par1 (unPar1)) +import GHC.Generics (Par1 (..), U1 (..), (:*:) (..)) import Numeric.Natural (Natural) import Prelude hiding (Bool, Eq (..), Num (..), not, replicate, (/), (>), (^), (||)) import qualified Prelude as Haskell @@ -12,7 +13,6 @@ import Test.Hspec import Test.QuickCheck import ZkFold.Base.Algebra.Basic.Class -import ZkFold.Base.Data.Vector (Vector, unsafeToVector) import ZkFold.Symbolic.Class (Symbolic) import ZkFold.Symbolic.Compiler import ZkFold.Symbolic.Data.Bool (Bool (..)) @@ -31,13 +31,13 @@ testFunc x y = g3 = c 2 // x in (g3 == y :: Bool c) ? g1 $ g2 -testResult :: forall a . Arithmetic a => ArithmeticCircuit a (Vector 2) Par1 -> a -> a -> Haskell.Bool -testResult r x y = fromConstant (unPar1 $ eval r (unsafeToVector [x, y])) Haskell.== +testResult :: forall a . Arithmetic a => ArithmeticCircuit a (Par1 :*: Par1 :*: U1) Par1 -> a -> a -> Haskell.Bool +testResult r x y = fromConstant (unPar1 $ eval r (Par1 x :*: Par1 y :*: U1)) Haskell.== testFunc @(Interpreter a) (fromConstant x) (fromConstant y) specArithmetization1 :: forall a . (Arithmetic a, Arbitrary a, Binary a, Show a) => Spec specArithmetization1 = do describe "Arithmetization test 1" $ do it "should pass" $ do - let ac = compile @a (testFunc @(ArithmeticCircuit a (Vector 2))) :: ArithmeticCircuit a (Vector 2) Par1 + let ac = compile @a testFunc property $ \x y -> testResult ac x y diff --git a/symbolic-base/test/Tests/Arithmetization/Test2.hs b/symbolic-base/test/Tests/Arithmetization/Test2.hs index c06f062f2..92ef7f9a2 100644 --- a/symbolic-base/test/Tests/Arithmetization/Test2.hs +++ b/symbolic-base/test/Tests/Arithmetization/Test2.hs @@ -4,7 +4,7 @@ module Tests.Arithmetization.Test2 (specArithmetization2) where import Data.Binary (Binary) -import GHC.Generics (Par1 (unPar1)) +import GHC.Generics (Par1 (..), U1 (..), (:*:) (..)) import Prelude hiding (Bool, Eq (..), Num (..), not, replicate, (/), (^), (||)) import qualified Prelude as Haskell @@ -13,7 +13,6 @@ import Test.QuickCheck (property) import ZkFold.Base.Algebra.Basic.Class (one) import ZkFold.Base.Algebra.EllipticCurve.BLS12_381 (Fr) -import ZkFold.Base.Data.Vector (Vector, unsafeToVector) import ZkFold.Symbolic.Class (Symbolic) import ZkFold.Symbolic.Compiler import ZkFold.Symbolic.Data.Bool (Bool (..), BoolType (..)) @@ -27,8 +26,8 @@ tautology x y = (x /= y) || (x == y) testTautology :: forall a . (Arithmetic a, Binary a) => a -> a -> Haskell.Bool testTautology x y = - let Bool (ac :: ArithmeticCircuit a (Vector 2) Par1) = compile @a (tautology @(ArithmeticCircuit a (Vector 2))) - b = unPar1 (eval ac (unsafeToVector [x, y])) + let Bool ac = compile @a tautology + b = unPar1 (eval ac (Par1 x :*: Par1 y :*: U1)) in b Haskell.== one specArithmetization2 :: Spec diff --git a/symbolic-base/test/Tests/Arithmetization/Test3.hs b/symbolic-base/test/Tests/Arithmetization/Test3.hs index a693e67c4..1e1f5e322 100644 --- a/symbolic-base/test/Tests/Arithmetization/Test3.hs +++ b/symbolic-base/test/Tests/Arithmetization/Test3.hs @@ -1,7 +1,9 @@ {-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} module Tests.Arithmetization.Test3 (specArithmetization3) where +import GHC.Generics (Par1 (..), U1 (..), (:*:) (..)) import Numeric.Natural (Natural) import Prelude hiding (Bool, Eq (..), Num (..), Ord (..), any, not, replicate, (/), (^), (||)) @@ -9,7 +11,6 @@ import Test.Hspec import ZkFold.Base.Algebra.Basic.Class (fromConstant) import ZkFold.Base.Algebra.Basic.Field (Zp) -import ZkFold.Base.Data.Vector (Vector, unsafeToVector) import ZkFold.Symbolic.Class (Symbolic) import ZkFold.Symbolic.Compiler import ZkFold.Symbolic.Data.Bool (Bool (..)) @@ -17,7 +18,7 @@ import ZkFold.Symbolic.Data.FieldElement (FieldElement) import ZkFold.Symbolic.Data.Ord ((<=)) import ZkFold.Symbolic.Interpreter (Interpreter (Interpreter)) -type R = ArithmeticCircuit (Zp 97) (Vector 2) +type R = ArithmeticCircuit (Zp 97) (Par1 :*: Par1 :*: U1) -- A comparison test testFunc :: Symbolic c => FieldElement c -> FieldElement c -> Bool c @@ -28,4 +29,4 @@ specArithmetization3 = do describe "Arithmetization test 3" $ do it "should pass" $ do let Bool r = compile @(Zp 97) (testFunc @R) :: Bool R - Bool (Interpreter (eval r (unsafeToVector [3, 5]))) `shouldBe` testFunc (fromConstant (3 :: Natural)) (fromConstant (5 :: Natural)) + Bool (Interpreter (eval r (Par1 3 :*: Par1 5 :*: U1))) `shouldBe` testFunc (fromConstant (3 :: Natural)) (fromConstant (5 :: Natural)) diff --git a/symbolic-base/test/Tests/Arithmetization/Test4.hs b/symbolic-base/test/Tests/Arithmetization/Test4.hs index 49c463c6b..10b376efc 100644 --- a/symbolic-base/test/Tests/Arithmetization/Test4.hs +++ b/symbolic-base/test/Tests/Arithmetization/Test4.hs @@ -1,9 +1,10 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} module Tests.Arithmetization.Test4 (specArithmetization4) where -import GHC.Generics (Par1 (unPar1)) +import GHC.Generics (Par1 (..), U1 (..), (:*:) (..)) import Prelude hiding (Bool, Eq (..), Num (..), Ord (..), (&&)) import qualified Prelude as Haskell import Test.Hspec (Spec, describe, it) @@ -12,7 +13,6 @@ import Test.QuickCheck (Testable (..), (== import ZkFold.Base.Algebra.Basic.Class (FromConstant (..), one, zero) import ZkFold.Base.Algebra.EllipticCurve.BLS12_381 (BLS12_381_G1) import ZkFold.Base.Algebra.EllipticCurve.Class (EllipticCurve (..)) -import qualified ZkFold.Base.Data.Vector as V import ZkFold.Symbolic.Class import ZkFold.Symbolic.Compiler (ArithmeticCircuit (..), compile, eval) import ZkFold.Symbolic.Data.Bool (Bool (..)) @@ -27,14 +27,14 @@ lockedByTxId targetValue inputValue = inputValue == fromConstant targetValue testSameValue :: F -> Haskell.Bool testSameValue targetValue = - let Bool ac = compile @F (lockedByTxId @F @(ArithmeticCircuit F (V.Vector 1)) targetValue) :: Bool (ArithmeticCircuit F (V.Vector 1)) - b = unPar1 (eval ac (V.singleton targetValue)) + let Bool ac = compile @F (lockedByTxId @F targetValue) :: Bool (ArithmeticCircuit F (Par1 :*: U1)) + b = unPar1 (eval ac (Par1 targetValue :*: U1)) in b Haskell.== one testDifferentValue :: F -> F -> Haskell.Bool testDifferentValue targetValue otherValue = - let Bool ac = compile @F (lockedByTxId @F @(ArithmeticCircuit F (V.Vector 1)) targetValue) :: Bool (ArithmeticCircuit F (V.Vector 1)) - b = unPar1 (eval ac (V.singleton otherValue)) + let Bool ac = compile @F (lockedByTxId @F targetValue) :: Bool (ArithmeticCircuit F (Par1 :*: U1)) + b = unPar1 (eval ac (Par1 otherValue :*: U1)) in b Haskell.== zero specArithmetization4 :: Spec diff --git a/symbolic-base/test/Tests/Blake2b.hs b/symbolic-base/test/Tests/Blake2b.hs index f62fc4790..982665c09 100644 --- a/symbolic-base/test/Tests/Blake2b.hs +++ b/symbolic-base/test/Tests/Blake2b.hs @@ -1,10 +1,12 @@ {-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE TypeOperators #-} module Tests.Blake2b where import Crypto.Hash.BLAKE2.BLAKE2b (hash) import qualified Data.ByteString.Internal as BI import Data.Data (Proxy (Proxy)) +import GHC.Generics (U1, (:*:)) import Numeric.Natural (Natural) import Prelude (Eq (..), IO, ($)) import Test.Hspec @@ -31,7 +33,7 @@ blake2bSimple = blake2bAC :: Spec blake2bAC = - let cs = compile blake2b_512 :: ByteString 512 (ArithmeticCircuit (Zp BLS12_381_Scalar) (Vector 8)) + let cs = compile blake2b_512 :: ByteString 512 (ArithmeticCircuit (Zp BLS12_381_Scalar) (Vector 8 :*: U1)) ac = pieces cs Proxy in it "simple test with cardano-crypto " $ acSizeN ac == 564239 diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Contracts/BatchTransfer.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Contracts/BatchTransfer.hs index 037c59144..3a068a533 100644 --- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Contracts/BatchTransfer.hs +++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Contracts/BatchTransfer.hs @@ -12,7 +12,7 @@ import ZkFold.Base.Algebra.Basic.Number (KnownNat) import ZkFold.Base.Data.Vector (Vector, fromVector, toVector) import ZkFold.Symbolic.Algorithms.Hash.MiMC import ZkFold.Symbolic.Cardano.Types -import ZkFold.Symbolic.Class (Symbolic) +import ZkFold.Symbolic.Class (Symbolic (BaseField)) import ZkFold.Symbolic.Data.Bool (BoolType (..), all) import ZkFold.Symbolic.Data.Class (SymbolicData (..)) import ZkFold.Symbolic.Data.Combinators @@ -29,7 +29,7 @@ verifySignature :: forall context . ( Symbolic context , SymbolicData (TxOut context) - , KnownNat (TypeSize (TxOut context)) + , KnownNat (NumberOfRegisters (BaseField context) 256 'Auto) ) => ByteString 224 context -> (TxOut context, TxOut context) -> ByteString 256 context -> Bool context verifySignature pub (pay, change) sig = (from sig * base) == (strictConv (fromFieldElement mimc) * from (extend pub :: ByteString 256 context)) where @@ -43,9 +43,8 @@ batchTransfer :: forall context. ( Symbolic context , SymbolicData (TxOut context) - , KnownNat (TypeSize (TxOut context)) - , KnownNat (TypeSize (SingleAsset context)) - , KnownNat (TypeSize (Value Tokens context)) + , KnownNat (NumberOfRegisters (BaseField context) 256 'Auto) + , KnownNat (NumberOfRegisters (BaseField context) 64 'Auto) ) => Tx context -> Vector 5 (TxOut context, TxOut context, ByteString 256 context)-> Bool context batchTransfer tx transfers = let -- Extract the payment credentials and verify the signatures diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Contracts/RandomOracle.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Contracts/RandomOracle.hs index 1ca272cc4..b6f8c70c4 100644 --- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Contracts/RandomOracle.hs +++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Contracts/RandomOracle.hs @@ -7,6 +7,7 @@ import Prelude hiding (Bool, Eq (..), all (&&), (*), (+), (==)) import ZkFold.Base.Algebra.Basic.Class +import ZkFold.Base.Algebra.Basic.Number (Log2) import ZkFold.Base.Data.Vector (Vector, (!!)) import ZkFold.Symbolic.Algorithms.Hash.MiMC (hash) import ZkFold.Symbolic.Cardano.Types @@ -23,7 +24,8 @@ type Tx context = Transaction 1 0 2 Tokens 1 () context randomOracle :: forall context . ( Symbolic context - , Bits (FieldElement context) ~ context (Vector 256) + , Bits (FieldElement context) ~ context (Vector 256) + , Log2 (Order (BaseField context)) ~ 255 ) => BaseField context -> Tx context -> FieldElement context -> Bool context randomOracle c tx w = let -- The secret key is correct diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Address.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Address.hs index b0b969b57..a4a7e7bf7 100644 --- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Address.hs +++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Address.hs @@ -33,6 +33,6 @@ deriving via (Structural (Address context)) instance HApplicative context => SymbolicData (Address context) where type Context (Address context) = Context (AddressType context, PaymentCredential context, StakingCredential context) type Support (Address context) = Support (AddressType context, PaymentCredential context, StakingCredential context) - type TypeSize (Address context) = TypeSize (AddressType context, PaymentCredential context, StakingCredential context) + type Layout (Address context) = Layout (AddressType context, PaymentCredential context, StakingCredential context) pieces (Address a b c) = pieces (a, b, c) restore f = let (a, b, c) = restore f in Address a b c diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Input.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Input.hs index 951d6f839..3f5e13025 100644 --- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Input.hs +++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Input.hs @@ -11,7 +11,7 @@ import ZkFold.Base.Algebra.Basic.Number import ZkFold.Symbolic.Cardano.Types.Address (Address) import ZkFold.Symbolic.Cardano.Types.Output (DatumHash, Output, txoAddress, txoDatumHash, txoTokens) import ZkFold.Symbolic.Cardano.Types.OutputRef (OutputRef) -import ZkFold.Symbolic.Cardano.Types.Value (SingleAsset, Value) +import ZkFold.Symbolic.Cardano.Types.Value (Value) import ZkFold.Symbolic.Class import ZkFold.Symbolic.Data.Class @@ -25,16 +25,10 @@ deriving instance , Haskell.Eq (Output tokens datum context) ) => Haskell.Eq (Input tokens datum context) -instance - ( Symbolic context - , KnownNat tokens - , KnownNat (TypeSize (OutputRef context)) - , KnownNat (TypeSize (SingleAsset context)) - , KnownNat (TypeSize (Value tokens context)) - ) => SymbolicData (Input tokens datum context) where +instance (Symbolic context, KnownNat tokens) => SymbolicData (Input tokens datum context) where type Context (Input tokens datum context) = Context (OutputRef context, Output tokens datum context) type Support (Input tokens datum context) = Support (OutputRef context, Output tokens datum context) - type TypeSize (Input tokens datum context) = TypeSize (OutputRef context, Output tokens datum context) + type Layout (Input tokens datum context) = Layout (OutputRef context, Output tokens datum context) pieces (Input a b) = pieces (a, b) restore f = let (a, b) = restore f in Input a b diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Output.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Output.hs index dd2cb1ad1..df79b1d10 100644 --- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Output.hs +++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Output.hs @@ -14,9 +14,10 @@ import ZkFold.Base.Algebra.Basic.Number import ZkFold.Symbolic.Cardano.Types.Address (Address) import ZkFold.Symbolic.Cardano.Types.Basic import ZkFold.Symbolic.Cardano.Types.Output.Datum -import ZkFold.Symbolic.Cardano.Types.Value (SingleAsset, Value) +import ZkFold.Symbolic.Cardano.Types.Value (Value) import ZkFold.Symbolic.Class import ZkFold.Symbolic.Data.Class +import ZkFold.Symbolic.Data.Combinators (NumberOfRegisters, RegisterSize (..)) import ZkFold.Symbolic.Data.Eq (Eq) import ZkFold.Symbolic.Data.Eq.Structural @@ -34,14 +35,12 @@ deriving instance instance ( Symbolic context - , KnownNat (TypeSize (Value tokens context)) - , KnownNat (TypeSize (SingleAsset context)) , KnownNat tokens ) => SymbolicData (Output tokens datum context) where type Context (Output tokens datum context) = Context (Address context, Value tokens context, DatumHash context) type Support (Output tokens datum context) = Support (Address context, Value tokens context, DatumHash context) - type TypeSize (Output tokens datum context) = TypeSize (Address context, Value tokens context, DatumHash context) + type Layout (Output tokens datum context) = Layout (Address context, Value tokens context, DatumHash context) pieces (Output a b c) = pieces (a, b, c) restore f = let (a, b, c) = restore f in Output a b c @@ -50,6 +49,5 @@ deriving via (Structural (Output tokens datum context)) instance ( Symbolic context , KnownNat tokens - , KnownNat (TypeSize (SingleAsset context)) - , KnownNat (TypeSize (Value tokens context)) + , KnownNat (NumberOfRegisters (BaseField context) 64 'Auto) ) => Eq (Bool context) (Output tokens datum context) diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/OutputRef.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/OutputRef.hs index 683a1bfcb..e75177db5 100644 --- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/OutputRef.hs +++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/OutputRef.hs @@ -27,7 +27,7 @@ deriving instance instance HApplicative context => SymbolicData (OutputRef context) where type Context (OutputRef context) = Context (TxRefId context, TxRefIndex context) type Support (OutputRef context) = Support (TxRefId context, TxRefIndex context) - type TypeSize (OutputRef context) = TypeSize (TxRefId context, TxRefIndex context) + type Layout (OutputRef context) = Layout (TxRefId context, TxRefIndex context) pieces (OutputRef a b) = pieces (a, b) restore f = let (a, b) = restore f in OutputRef a b diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Transaction.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Transaction.hs index 13b6139fb..eda4986a1 100644 --- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Transaction.hs +++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Transaction.hs @@ -2,17 +2,16 @@ module ZkFold.Symbolic.Cardano.Types.Transaction where -import Prelude hiding (Bool, Eq, length, splitAt, (*), (+)) -import qualified Prelude as Haskell +import Prelude hiding (Bool, Eq, length, splitAt, (*), (+)) +import qualified Prelude as Haskell import ZkFold.Base.Algebra.Basic.Number import ZkFold.Base.Data.Vector import ZkFold.Symbolic.Cardano.Types.Basic -import ZkFold.Symbolic.Cardano.Types.Input (Input) -import ZkFold.Symbolic.Cardano.Types.Output (Output) -import ZkFold.Symbolic.Cardano.Types.OutputRef (OutputRef) -import ZkFold.Symbolic.Cardano.Types.Value (SingleAsset, Value) -import ZkFold.Symbolic.Class (Symbolic) +import ZkFold.Symbolic.Cardano.Types.Input (Input) +import ZkFold.Symbolic.Cardano.Types.Output (Output) +import ZkFold.Symbolic.Cardano.Types.Value (Value) +import ZkFold.Symbolic.Class (Symbolic) import ZkFold.Symbolic.Data.Class data Transaction inputs rinputs outputs tokens mint datum context = Transaction { @@ -39,20 +38,10 @@ instance , KnownNat inputs , KnownNat outputs , KnownNat mint - , KnownNat (TypeSize (SingleAsset context)) - , KnownNat (TypeSize (UTCTime context)) - , KnownNat (TypeSize (OutputRef context)) - , KnownNat (TypeSize (Value tokens context)) - , KnownNat (TypeSize (Output tokens datum context)) - , KnownNat (TypeSize (Vector outputs (Output tokens datum context))) - , KnownNat (TypeSize (Input tokens datum context)) - , KnownNat (TypeSize (Vector inputs (Input tokens datum context))) - , KnownNat (TypeSize (Vector rinputs (Input tokens datum context))) - , KnownNat (TypeSize (Value mint context)) ) => SymbolicData (Transaction inputs rinputs outputs tokens mint datum context) where type Context (Transaction inputs rinputs outputs tokens mint datum context) = Context (Vector rinputs (Input tokens datum context), Vector inputs (Input tokens datum context), Vector outputs (Output tokens datum context), Value mint context, (UTCTime context, UTCTime context)) type Support (Transaction inputs rinputs outputs tokens mint datum context) = Support (Vector rinputs (Input tokens datum context), Vector inputs (Input tokens datum context), Vector outputs (Output tokens datum context), Value mint context, (UTCTime context, UTCTime context)) - type TypeSize (Transaction inputs rinputs outputs tokens mint datum context) = TypeSize (Vector rinputs (Input tokens datum context), Vector inputs (Input tokens datum context), Vector outputs (Output tokens datum context), Value mint context, (UTCTime context, UTCTime context)) + type Layout (Transaction inputs rinputs outputs tokens mint datum context) = Layout (Vector rinputs (Input tokens datum context), Vector inputs (Input tokens datum context), Vector outputs (Output tokens datum context), Value mint context, (UTCTime context, UTCTime context)) pieces (Transaction a b c d e) = pieces (a, b, c, d, e) restore f = let (a, b, c, d, e) = restore f in Transaction a b c d e diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Value.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Value.hs index dd5332bf3..3428f328d 100644 --- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Value.hs +++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Value.hs @@ -28,11 +28,7 @@ deriving instance (Haskell.Eq (ByteString 224 context), Haskell.Eq (ByteString 2 deriving instance (Haskell.Ord (ByteString 224 context), Haskell.Ord (ByteString 256 context), Haskell.Ord (UInt 64 Auto context)) => Haskell.Ord (Value n context) -deriving instance - ( Symbolic context - , KnownNat n - , KnownNat (TypeSize (SingleAsset context)) - ) => SymbolicData (Value n context) +deriving instance (Symbolic context, KnownNat n) => SymbolicData (Value n context) instance Symbolic context => Scale Natural (Value n context) where n `scale` Value v = Value $ fmap (\((pid, aname), q) -> ((pid, aname), n `scale` q)) v diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/UPLC/Builtins.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/UPLC/Builtins.hs index 47b9aace4..f08348517 100644 --- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/UPLC/Builtins.hs +++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/UPLC/Builtins.hs @@ -6,7 +6,6 @@ module ZkFold.Symbolic.Cardano.UPLC.Builtins where import Data.Typeable (Proxy (..), Typeable) import GHC.Generics (Par1) -import GHC.TypeLits (KnownNat) import Prelude (($)) import ZkFold.Base.Algebra.Basic.Class @@ -28,7 +27,6 @@ data BuiltinFunctions = instance ( Typeable c , S.SymbolicData (c Par1) - , KnownNat (S.TypeSize (c Par1)) , Semiring (c Par1) ) => PlutusBuiltinFunction c BuiltinFunctions where diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/UPLC/Term.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/UPLC/Term.hs index d9963986e..2077beb57 100644 --- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/UPLC/Term.hs +++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/UPLC/Term.hs @@ -2,11 +2,10 @@ module ZkFold.Symbolic.Cardano.UPLC.Term where -import Data.Maybe (fromJust) -import Data.Typeable (Typeable, cast, typeOf) +import Data.Maybe (fromJust) +import Data.Typeable (Typeable, cast, typeOf) import Prelude -import ZkFold.Base.Algebra.Basic.Number import ZkFold.Symbolic.Data.Class -- Based on the November 2022 UPLC spec @@ -16,7 +15,7 @@ data Term name fun c where Apply :: Term name fun c -> Term name fun c -> Term name fun c Force :: Term name fun c -> Term name fun c Delay :: Term name fun c -> Term name fun c - Constant :: (Eq x, Typeable x, SymbolicData x, Context x ~ c, KnownNat (TypeSize x)) => x -> Term name fun c + Constant :: (Eq x, Typeable x, SymbolicData x, Context x ~ c) => x -> Term name fun c Builtin :: fun -> Term name fun c Error :: Term name fun c diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/UPLC/Type.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/UPLC/Type.hs index 97b191dd6..5de5441f2 100644 --- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/UPLC/Type.hs +++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/UPLC/Type.hs @@ -4,11 +4,10 @@ module ZkFold.Symbolic.Cardano.UPLC.Type where -import Data.Typeable (Proxy (..), TypeRep, Typeable, typeOf) +import Data.Typeable (Proxy (..), TypeRep, Typeable, typeOf) import Prelude -import ZkFold.Base.Algebra.Basic.Number -import ZkFold.Symbolic.Data.Class (SymbolicData (..)) +import ZkFold.Symbolic.Data.Class (SymbolicData (..)) data SomeType c where NoType :: SomeType c @@ -37,7 +36,7 @@ instance Semigroup (SomeType c) where _ <> _ = error "Semigroup (SomeType a): constructor mismatch" data SomeSymbolic c where - SomeData :: (Typeable t, SymbolicData t, Context t ~ c, KnownNat (TypeSize t)) => Proxy t -> SomeSymbolic c + SomeData :: (Typeable t, SymbolicData t, Context t ~ c) => Proxy t -> SomeSymbolic c getType :: SomeSymbolic c -> TypeRep getType (SomeData t) = typeOf t diff --git a/symbolic-examples/bench/BenchCompiler.hs b/symbolic-examples/bench/BenchCompiler.hs index ecde3324a..11c157b32 100644 --- a/symbolic-examples/bench/BenchCompiler.hs +++ b/symbolic-examples/bench/BenchCompiler.hs @@ -9,17 +9,13 @@ import Data.Function (const, ($) import Data.Functor.Rep (Representable (..)) import Data.Semigroup ((<>)) import Data.String (String, fromString) -import Data.Type.Equality (type (~)) -import GHC.TypeNats (KnownNat) import System.IO (IO) import Test.Tasty.Bench import Test.Tasty.Golden (goldenVsString) import Text.Show (show) import ZkFold.Base.Algebra.Basic.Class (AdditiveMonoid, zero) -import ZkFold.Base.Data.Vector (Vector) import ZkFold.Symbolic.Compiler -import ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal (Var) import ZkFold.Symbolic.Examples metrics :: String -> ArithmeticCircuit a i o -> ByteString @@ -31,7 +27,7 @@ metrics name circuit = benchmark :: - (NFData a, AdditiveMonoid a, NFData (o (Var a i)), NFData (Rep i), i ~ Vector n_i, KnownNat n_i) => + (NFData a, AdditiveMonoid a, NFData (o (Var a i)), NFData (Rep i), Representable i) => String -> (() -> ArithmeticCircuit a i o) -> Benchmark benchmark name circuit = bgroup name [ bench "compilation" $ nf circuit () diff --git a/symbolic-examples/src/Examples/BatchTransfer.hs b/symbolic-examples/src/Examples/BatchTransfer.hs index 9519085f1..4b22c5d7f 100644 --- a/symbolic-examples/src/Examples/BatchTransfer.hs +++ b/symbolic-examples/src/Examples/BatchTransfer.hs @@ -1,18 +1,18 @@ module Examples.BatchTransfer (exampleBatchTransfer) where -import ZkFold.Base.Algebra.Basic.Number (KnownNat) +import GHC.TypeLits (KnownNat) + import ZkFold.Base.Data.Vector (Vector) -import ZkFold.Symbolic.Cardano.Contracts.BatchTransfer (Tokens, Tx, TxOut, batchTransfer) -import ZkFold.Symbolic.Cardano.Types (Bool, ByteString, Value) -import ZkFold.Symbolic.Cardano.Types.Value (SingleAsset) +import ZkFold.Symbolic.Cardano.Contracts.BatchTransfer (Tx, TxOut, batchTransfer) +import ZkFold.Symbolic.Cardano.Types (Bool, ByteString) import ZkFold.Symbolic.Class (Symbolic (..)) import ZkFold.Symbolic.Data.Class (SymbolicData (..)) +import ZkFold.Symbolic.Data.Combinators (NumberOfRegisters, RegisterSize (..)) exampleBatchTransfer :: ( Symbolic c , SymbolicData (TxOut c) - , KnownNat (TypeSize (TxOut c)) - , KnownNat (TypeSize (SingleAsset c)) - , KnownNat (TypeSize (Value Tokens c)) + , KnownNat (NumberOfRegisters (BaseField c) 64 'Auto) + , KnownNat (NumberOfRegisters (BaseField c) 256 'Auto) ) => Tx c -> Vector 5 (TxOut c, TxOut c, ByteString 256 c) -> Bool c exampleBatchTransfer = batchTransfer diff --git a/symbolic-examples/src/ZkFold/Symbolic/Examples.hs b/symbolic-examples/src/ZkFold/Symbolic/Examples.hs index fb4f25ccf..ff1fc3082 100644 --- a/symbolic-examples/src/ZkFold/Symbolic/Examples.hs +++ b/symbolic-examples/src/ZkFold/Symbolic/Examples.hs @@ -1,8 +1,12 @@ {-# LANGUAGE TypeOperators #-} +{-# OPTIONS_GHC -Wno-orphans #-} + module ZkFold.Symbolic.Examples (ExampleOutput (..), examples) where +import Control.DeepSeq (NFData) import Data.Function (const, ($), (.)) +import Data.Functor.Rep (Rep, Representable) import Data.Proxy (Proxy) import Data.String (String) import Data.Type.Equality (type (~)) @@ -17,38 +21,43 @@ import Examples.LEQ (exampleLEQ) import Examples.MiMCHash (exampleMiMC) import Examples.ReverseList (exampleReverseList) import Examples.UInt +import GHC.Generics (Par1, (:*:), (:.:)) import ZkFold.Base.Algebra.Basic.Field (Zp) -import ZkFold.Base.Algebra.Basic.Number (KnownNat) import ZkFold.Base.Algebra.EllipticCurve.BLS12_381 (BLS12_381_Scalar) -import ZkFold.Base.Data.Vector (Vector) import ZkFold.Symbolic.Compiler (ArithmeticCircuit, compile) +import ZkFold.Symbolic.Compiler.ArithmeticCircuit (Var) import ZkFold.Symbolic.Data.ByteString (ByteString) import ZkFold.Symbolic.Data.Class import ZkFold.Symbolic.Data.Combinators (RegisterSize (Auto)) -type C = ArithmeticCircuit (Zp BLS12_381_Scalar) +type A = Zp BLS12_381_Scalar +type C = ArithmeticCircuit A data ExampleOutput where - ExampleOutput - :: forall i_n o_n. KnownNat i_n - => (() -> C (Vector i_n) (Vector o_n)) - -> ExampleOutput + ExampleOutput :: + forall i o. (Representable i, NFData (Rep i), NFData (o (Var A i))) => + (() -> C i o) -> ExampleOutput exampleOutput :: - forall i_n o_n c f. - ( KnownNat i_n - , SymbolicData f - , c ~ C (Vector i_n) + forall i o c f. + ( SymbolicData f + , c ~ C i , Context f ~ c - , TypeSize f ~ o_n + , Layout f ~ o , SymbolicData (Support f) , Context (Support f) ~ c , Support (Support f) ~ Proxy c - , Layout f ~ Vector o_n - , Layout (Support f) ~ Vector i_n + , Layout (Support f) ~ i + , Representable i + , NFData (Rep i) + , NFData (o (Var A i)) ) => f -> ExampleOutput -exampleOutput = ExampleOutput @i_n @o_n . const . compile +exampleOutput = ExampleOutput @i @o . const . compile + +instance NFData a => NFData (Par1 a) +instance (NFData (f a), NFData (g a)) => NFData ((f :*: g) a) +instance NFData (f (g a)) => NFData ((f :.: g) a) examples :: [(String, ExampleOutput)] examples = @@ -65,7 +74,7 @@ examples = , ("UInt.StrictAdd.256.Auto", exampleOutput $ exampleUIntStrictAdd @256 @Auto) , ("UInt.StrictMul.512.Auto", exampleOutput $ exampleUIntStrictMul @512 @Auto) , ("UInt.DivMod.32.Auto", exampleOutput $ exampleUIntDivMod @32 @Auto) - , ("Reverse.32.3000", exampleOutput $ exampleReverseList @32 @(ByteString 3000 (C (Vector _)))) + , ("Reverse.32.3000", exampleOutput $ exampleReverseList @32 @(ByteString 3000 (C _))) , ("Fibonacci.100", exampleOutput $ exampleFibonacci 100) , ("MiMCHash", exampleOutput exampleMiMC) , ("SHA256.32", exampleOutput $ exampleSHA @32) diff --git a/symbolic-examples/symbolic-examples.cabal b/symbolic-examples/symbolic-examples.cabal index 5bdd23e8e..e461d9cba 100644 --- a/symbolic-examples/symbolic-examples.cabal +++ b/symbolic-examples/symbolic-examples.cabal @@ -102,6 +102,7 @@ library Examples.ReverseList Examples.UInt build-depends: + adjunctions, base, deepseq, symbolic-base, From d5168e4ba7eed0bf6a53ccf9fef282604a516a16 Mon Sep 17 00:00:00 2001 From: TurtlePU Date: Thu, 10 Oct 2024 02:17:08 +0000 Subject: [PATCH 2/4] stylish-haskell auto-commit --- .../Compiler/ArithmeticCircuit/Internal.hs | 7 +++--- .../src/ZkFold/Symbolic/Data/Ed25519.hs | 4 ++-- symbolic-examples/bench/BenchCompiler.hs | 22 +++++++++---------- 3 files changed, 17 insertions(+), 16 deletions(-) diff --git a/symbolic-base/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit/Internal.hs b/symbolic-base/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit/Internal.hs index 331b20db3..f876b3d8b 100644 --- a/symbolic-base/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit/Internal.hs +++ b/symbolic-base/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit/Internal.hs @@ -47,7 +47,8 @@ import Prelude hiding (N import ZkFold.Base.Algebra.Basic.Class import ZkFold.Base.Algebra.Basic.Field (Zp) import ZkFold.Base.Algebra.Basic.Number -import ZkFold.Base.Algebra.Polynomials.Multivariate (Poly, evalMonomial, evalPolynomial, var, mapVars) +import ZkFold.Base.Algebra.Polynomials.Multivariate (Poly, evalMonomial, evalPolynomial, mapVars, + var) import ZkFold.Base.Control.HApplicative import ZkFold.Base.Data.HFunctor import ZkFold.Base.Data.Package @@ -99,7 +100,7 @@ deriving instance NFData (Rep i) => NFData (SysVar i) imapSysVar :: (Representable i, Representable j) => (forall x. j x -> i x) -> SysVar i -> SysVar j -imapSysVar f (InVar r) = index (f (tabulate InVar)) r +imapSysVar f (InVar r) = index (f (tabulate InVar)) r imapSysVar _ (NewVar b) = NewVar b data Var a i @@ -120,7 +121,7 @@ instance FromConstant a (Var a i) where imapVar :: (Representable i, Representable j) => (forall x. j x -> i x) -> Var a i -> Var a j -imapVar f (SysVar s) = SysVar (imapSysVar f s) +imapVar f (SysVar s) = SysVar (imapSysVar f s) imapVar _ (ConstVar c) = ConstVar c ---------------------------------- Variables ----------------------------------- diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Ed25519.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Ed25519.hs index 7a4e2d619..2109743a3 100644 --- a/symbolic-base/src/ZkFold/Symbolic/Data/Ed25519.hs +++ b/symbolic-base/src/ZkFold/Symbolic/Data/Ed25519.hs @@ -7,6 +7,8 @@ module ZkFold.Symbolic.Data.Ed25519 where import Control.DeepSeq (NFData, force) +import Data.Functor.Rep (Representable) +import Data.Traversable (Traversable) import Prelude (type (~), ($)) import qualified Prelude as P @@ -26,8 +28,6 @@ import ZkFold.Symbolic.Data.Conditional import ZkFold.Symbolic.Data.Eq import ZkFold.Symbolic.Data.FieldElement import ZkFold.Symbolic.Data.UInt -import Data.Functor.Rep (Representable) -import Data.Traversable (Traversable) instance Symbolic c => SymbolicData (Point (Ed25519 c)) where diff --git a/symbolic-examples/bench/BenchCompiler.hs b/symbolic-examples/bench/BenchCompiler.hs index 11c157b32..64b1dd4ea 100644 --- a/symbolic-examples/bench/BenchCompiler.hs +++ b/symbolic-examples/bench/BenchCompiler.hs @@ -2,19 +2,19 @@ module Main where -import Control.DeepSeq (NFData, force) -import Control.Monad (return) -import Data.ByteString.Lazy (ByteString) -import Data.Function (const, ($)) -import Data.Functor.Rep (Representable (..)) -import Data.Semigroup ((<>)) -import Data.String (String, fromString) -import System.IO (IO) +import Control.DeepSeq (NFData, force) +import Control.Monad (return) +import Data.ByteString.Lazy (ByteString) +import Data.Function (const, ($)) +import Data.Functor.Rep (Representable (..)) +import Data.Semigroup ((<>)) +import Data.String (String, fromString) +import System.IO (IO) import Test.Tasty.Bench -import Test.Tasty.Golden (goldenVsString) -import Text.Show (show) +import Test.Tasty.Golden (goldenVsString) +import Text.Show (show) -import ZkFold.Base.Algebra.Basic.Class (AdditiveMonoid, zero) +import ZkFold.Base.Algebra.Basic.Class (AdditiveMonoid, zero) import ZkFold.Symbolic.Compiler import ZkFold.Symbolic.Examples From 96cf0b9caa952680d81c159e909d2fa6e609a0b2 Mon Sep 17 00:00:00 2001 From: TurtlePU Date: Thu, 10 Oct 2024 23:27:12 +0300 Subject: [PATCH 3/4] post-289 fixes --- symbolic-base/src/ZkFold/Base/Protocol/Protostar/Fold.hs | 8 +++++++- symbolic-base/src/ZkFold/Symbolic/Compiler.hs | 3 +++ .../Symbolic/Compiler/ArithmeticCircuit/Internal.hs | 3 ++- symbolic-examples/src/ZkFold/Symbolic/Examples.hs | 3 +++ 4 files changed, 15 insertions(+), 2 deletions(-) diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Protostar/Fold.hs b/symbolic-base/src/ZkFold/Base/Protocol/Protostar/Fold.hs index 0f3c59cbf..3c3305b53 100644 --- a/symbolic-base/src/ZkFold/Base/Protocol/Protostar/Fold.hs +++ b/symbolic-base/src/ZkFold/Base/Protocol/Protostar/Fold.hs @@ -12,10 +12,11 @@ import Control.Lens ((^.)) import Data.Binary (Binary) import Data.Function ((.)) import Data.Functor (fmap) -import Data.Functor.Rep (Representable) +import Data.Functor.Rep (Rep, Representable) import Data.Kind (Type) import Data.Map.Strict (Map) import qualified Data.Map.Strict as M +import Data.Ord (Ord) import Data.Proxy (Proxy) import GHC.Generics (Generic, Par1 (..), U1 (..), type (:*:) (..), type (:.:) (..)) @@ -140,6 +141,11 @@ ivcVerifierAc => Representable (Layout f) => Representable (Layout a) => Representable (Layout m) + => Ord (Rep (Layout i)) + => Ord (Rep (Layout c)) + => Ord (Rep (Layout f)) + => Ord (Rep (Layout a)) + => Ord (Rep (Layout m)) => Layout y ~ Par1 => t ~ ((i,c,(i,c,f,c,f),(i,c,f,c,f),c),(a,(f,f,f),(i,c,f,c,f),m),Proxy ctx) => ctx ~ ArithmeticCircuit a (Layout t) diff --git a/symbolic-base/src/ZkFold/Symbolic/Compiler.hs b/symbolic-base/src/ZkFold/Symbolic/Compiler.hs index bd05040d7..f82e41c12 100644 --- a/symbolic-base/src/ZkFold/Symbolic/Compiler.hs +++ b/symbolic-base/src/ZkFold/Symbolic/Compiler.hs @@ -53,6 +53,7 @@ solder :: , Support s ~ Proxy c , Layout s ~ l , Representable l + , Ord (Rep l) ) => f -> c (Layout f) solder f = pieces f (restore @(Support f) $ const inputC) where @@ -94,6 +95,7 @@ compile :: , Support s ~ Proxy c , Layout s ~ l , Representable l + , Ord (Rep l) , SymbolicData y , Context y ~ c , Support y ~ Proxy c @@ -116,6 +118,7 @@ compileIO :: , Support s ~ Proxy c , Layout s ~ l , Representable l + , Ord (Rep l) , FromJSON (Rep l) , ToJSON (Rep l) ) => FilePath -> f -> IO () diff --git a/symbolic-base/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit/Internal.hs b/symbolic-base/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit/Internal.hs index 939619558..4d89d09ee 100644 --- a/symbolic-base/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit/Internal.hs +++ b/symbolic-base/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit/Internal.hs @@ -77,6 +77,7 @@ deriving via (GenericSemigroupMonoid (ArithmeticCircuit a i o)) deriving via (GenericSemigroupMonoid (ArithmeticCircuit a i o)) instance (Ord (Rep i), o ~ U1) => Monoid (ArithmeticCircuit a i o) + instance (NFData a, NFData (o (Var a i)), NFData (Rep i)) => NFData (ArithmeticCircuit a i o) @@ -148,7 +149,7 @@ hlmap :: (forall x . j x -> i x) -> ArithmeticCircuit a i o -> ArithmeticCircuit a j o hlmap f (ArithmeticCircuit s r w o) = ArithmeticCircuit { acSystem = mapVars (imapSysVar f) <$> s - , acRange = r + , acRange = mapKeys (imapSysVar f) r , acWitness = (\g j p -> g (f j) p) <$> w , acOutput = imapVar f <$> o } diff --git a/symbolic-examples/src/ZkFold/Symbolic/Examples.hs b/symbolic-examples/src/ZkFold/Symbolic/Examples.hs index ff1fc3082..abc18eca3 100644 --- a/symbolic-examples/src/ZkFold/Symbolic/Examples.hs +++ b/symbolic-examples/src/ZkFold/Symbolic/Examples.hs @@ -30,6 +30,7 @@ import ZkFold.Symbolic.Compiler.ArithmeticCircuit (Var) import ZkFold.Symbolic.Data.ByteString (ByteString) import ZkFold.Symbolic.Data.Class import ZkFold.Symbolic.Data.Combinators (RegisterSize (Auto)) +import Data.Ord (Ord) type A = Zp BLS12_381_Scalar type C = ArithmeticCircuit A @@ -50,11 +51,13 @@ exampleOutput :: , Support (Support f) ~ Proxy c , Layout (Support f) ~ i , Representable i + , Ord (Rep i) , NFData (Rep i) , NFData (o (Var A i)) ) => f -> ExampleOutput exampleOutput = ExampleOutput @i @o . const . compile +-- | TODO: Maybe there is a better place for these orphans? instance NFData a => NFData (Par1 a) instance (NFData (f a), NFData (g a)) => NFData ((f :*: g) a) instance NFData (f (g a)) => NFData ((f :.: g) a) From de82b2c5d5db9eaa17b5b29f1d115d56fcf8fafa Mon Sep 17 00:00:00 2001 From: TurtlePU Date: Thu, 10 Oct 2024 20:30:23 +0000 Subject: [PATCH 4/4] stylish-haskell auto-commit --- symbolic-examples/src/ZkFold/Symbolic/Examples.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/symbolic-examples/src/ZkFold/Symbolic/Examples.hs b/symbolic-examples/src/ZkFold/Symbolic/Examples.hs index abc18eca3..f687403ea 100644 --- a/symbolic-examples/src/ZkFold/Symbolic/Examples.hs +++ b/symbolic-examples/src/ZkFold/Symbolic/Examples.hs @@ -7,6 +7,7 @@ module ZkFold.Symbolic.Examples (ExampleOutput (..), examples) where import Control.DeepSeq (NFData) import Data.Function (const, ($), (.)) import Data.Functor.Rep (Rep, Representable) +import Data.Ord (Ord) import Data.Proxy (Proxy) import Data.String (String) import Data.Type.Equality (type (~)) @@ -30,7 +31,6 @@ import ZkFold.Symbolic.Compiler.ArithmeticCircuit (Var) import ZkFold.Symbolic.Data.ByteString (ByteString) import ZkFold.Symbolic.Data.Class import ZkFold.Symbolic.Data.Combinators (RegisterSize (Auto)) -import Data.Ord (Ord) type A = Zp BLS12_381_Scalar type C = ArithmeticCircuit A