Merge branch 'main' into vlasin-monorepo-refactor

symbolic-base/src/ZkFold/Base/Protocol/Protostar/Commit.hs

@@ -12,6 +12,7 @@ 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
@@ -76,6 +77,7 @@ instance
     , SymbolicData (Point c)
     , Context (Point c) ~ ctx
     , PedersonSetup (Point c)
+    , Layout (Point c) ~ Vector n
     ) => HomomorphicCommit (FieldElement ctx) (FieldElement ctx) (Point c) where
     hcommit r b = let (g, h) = pedersonGH @(Point c)
                    in scale b g + scale r h

symbolic-base/src/ZkFold/Base/Protocol/Protostar/Fold.hs

@@ -163,6 +163,12 @@ 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)
     => Acc.AccumulatorScheme i f c m ctx a
     => y

symbolic-base/src/ZkFold/Symbolic/Algorithms/Hash/MiMC.hs

@@ -11,7 +11,7 @@ import           Prelude                                        hiding (Eq (..),
 
 import           ZkFold.Base.Algebra.Basic.Class
 import           ZkFold.Base.Data.Package                       (unpacked)
-import           ZkFold.Base.Data.Vector                        (fromVector)
+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,11 +39,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 .
+hash :: forall context x a size .
     ( Symbolic context
     , SymbolicData x
     , BaseField context ~ a
     , Context x ~ context
     , Support x ~ Proxy context
+    , Layout x ~ Vector size
     ) => x -> FieldElement context
 hash = mimcHashN mimcConstants (zero :: a) . fromVector . fmap FieldElement . unpacked . flip pieces Proxy

symbolic-base/src/ZkFold/Symbolic/Compiler.hs

@@ -45,13 +45,14 @@ forceOne r = fromCircuitF r (\fi -> for fi $ \i -> constraint (\x -> x i - one)
 solder ::
     forall a c f ni .
     ( KnownNat ni
-    , ni ~ TypeSize (Support f)
     , c ~ ArithmeticCircuit a (Vector ni)
     , 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))
 solder f = pieces f (restore @(Support f) $ const inputC)
     where
@@ -61,7 +62,6 @@ solder f = pieces f (restore @(Support f) $ const inputC)
 compileForceOne ::
     forall a c f y ni .
     ( KnownNat ni
-    , ni ~ TypeSize (Support f)
     , c ~ ArithmeticCircuit a (Vector ni)
     , Arithmetic a
     , Binary a
@@ -74,14 +74,16 @@ compileForceOne ::
     , 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
     ) => 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
-    , ni ~ TypeSize (Support f)
     , c ~ ArithmeticCircuit a (Vector ni)
     , SymbolicData f
     , Context f ~ c
@@ -92,14 +94,16 @@ compile ::
     , 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
     ) => 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
-    , ni ~ TypeSize (Support f)
     , c ~ ArithmeticCircuit a (Vector ni)
     , FromJSON a
     , ToJSON a
@@ -108,6 +112,8 @@ compileIO ::
     , SymbolicData (Support f)
     , Context (Support f) ~ c
     , Support (Support f) ~ Proxy c
+    , Layout f ~ Vector (TypeSize f)
+    , Layout (Support f) ~ Vector ni
     ) => FilePath -> f -> IO ()
 compileIO scriptFile f = do
     let ac = optimize (solder @a f) :: c (Vector (TypeSize f))

symbolic-base/src/ZkFold/Symbolic/Data/Class.hs

@@ -32,12 +32,14 @@ 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 (Vector (TypeSize x))
+    pieces :: x -> Support x -> Context x (Layout x)
 
     -- | Restores `x` from the circuit's outputs.
-    restore :: (Support x -> Context x (Vector (TypeSize x))) -> x
+    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
@@ -78,6 +80,8 @@ instance
     , 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
@@ -98,6 +102,9 @@ instance
     , 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))
@@ -122,6 +129,10 @@ instance
     , 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))
@@ -150,6 +161,11 @@ instance
     , 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))
@@ -165,6 +181,7 @@ instance
     , 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
@@ -178,6 +195,7 @@ 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
     restore f x = restore (f . (x,))

symbolic-base/src/ZkFold/Symbolic/Data/Conditional.hs

@@ -7,7 +7,7 @@ import           Data.Type.Equality              (type (~))
 import           GHC.Generics                    (Par1 (Par1))
 
 import           ZkFold.Base.Algebra.Basic.Class
-import           ZkFold.Base.Data.Vector         (zipWithM)
+import           ZkFold.Base.Data.Vector         (Vector, zipWithM)
 import           ZkFold.Symbolic.Class
 import           ZkFold.Symbolic.Data.Bool       (Bool (Bool), BoolType)
 import           ZkFold.Symbolic.Data.Class
@@ -27,7 +27,7 @@ gif b x y = bool y x b
 (?) :: Conditional b a => b -> a -> a -> a
 (?) = gif
 
-instance (SymbolicData x, Context x ~ c, Symbolic c) => Conditional (Bool c) x where
+instance (SymbolicData x, Context x ~ c, Symbolic c, Layout x ~ Vector n) => 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

symbolic-base/src/ZkFold/Symbolic/Data/Ed25519.hs

@@ -101,6 +101,7 @@ instance
     , SymbolicData (Point curve)
     , Context (Point curve) ~ ctx
     , bits ~ NumberOfBits (S.BaseField ctx)
+    , Layout (Point curve) ~ V.Vector n
     ) => Scale (FieldElement ctx) (Point curve) 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)

symbolic-base/src/ZkFold/Symbolic/Data/Eq/Structural.hs

@@ -1,8 +1,11 @@
-{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 module ZkFold.Symbolic.Data.Eq.Structural where
 
 import           Data.Proxy                 (Proxy (..))
+import           Data.Traversable           (Traversable)
+import           Data.Zip                   (Zip)
 import           Prelude                    (type (~))
 
 import           ZkFold.Symbolic.Class
@@ -18,6 +21,8 @@ instance
     , Context x ~ c
     , Support x ~ Proxy c
     , Symbolic c
+    , Zip (Layout x)
+    , Traversable (Layout x)
     ) => Eq (Bool c) (Structural x) where
 
     Structural x == Structural y =

symbolic-base/src/ZkFold/Symbolic/Data/Maybe.hs

@@ -41,8 +41,8 @@ nothing
     .  Symbolic c
     => SymbolicData x
     => c ~ Context x
-    => k ~ TypeSize 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))
 
@@ -52,7 +52,7 @@ fromMaybe
     => Ring (c (Vector 1))
     => SymbolicData x
     => Context x ~ c
-    => 1 ~ TypeSize x
+    => Layout x ~ Vector 1
     => x
     -> Maybe c x
     -> x
@@ -74,6 +74,7 @@ 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
@@ -82,13 +83,13 @@ instance
     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))
 
-maybe :: forall a b c .
-    (Symbolic c, SymbolicData b, Context b ~ c) =>
+maybe :: forall a b c n .
+    (Symbolic c, SymbolicData b, Context b ~ c, Layout b ~ Vector n) =>
     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)) =>
+    (Symbolic c, SymbolicData a, Context a ~ c, Support a ~ Proxy c, KnownNat (TypeSize a), Layout a ~ Vector (TypeSize a)) =>
     Haskell.Foldable t =>
     (a -> Bool c) -> t a -> Maybe c a
 find p = let n = nothing in

symbolic-base/src/ZkFold/Symbolic/Data/Ord.hs

@@ -20,7 +20,7 @@ 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          (unsafeToVector)
+import           ZkFold.Base.Data.Vector          (Vector, unsafeToVector)
 import           ZkFold.Symbolic.Class            (Symbolic (BaseField, symbolicF), symbolic2F)
 import           ZkFold.Symbolic.Data.Bool        (Bool (..))
 import           ZkFold.Symbolic.Data.Class
@@ -70,6 +70,7 @@ instance
     , Context x ~ c
     , Support x ~ Proxy c
     , TypeSize x ~ 1
+    , Layout x ~ Vector 1
     ) => Ord (Bool c) (Lexicographical x) where
 
     x <= y = y >= x
@@ -86,7 +87,7 @@ instance
 
 getBitsBE ::
   forall c x .
-  (Symbolic c, SymbolicData x, Context x ~ c, Support x ~ Proxy c, TypeSize x ~ 1) =>
+  (Symbolic c, SymbolicData x, Context x ~ c, Support x ~ Proxy c, Layout x ~ Vector 1) =>
   x -> c (V.Vector (NumberOfBits (BaseField c)))
 -- ^ @getBitsBE x@ returns a list of circuits computing bits of @x@, eldest to
 -- youngest.

symbolic-examples/src/ZkFold/Symbolic/Examples.hs

@@ -38,14 +38,15 @@ data ExampleOutput where
 exampleOutput ::
   forall i_n o_n c f.
   ( KnownNat i_n
-  , i_n ~ TypeSize (Support f)
   , SymbolicData f
   , c ~ C (Vector i_n)
   , Context f ~ c
   , TypeSize f ~ o_n
   , SymbolicData (Support f)
   , Context (Support f) ~ c
   , Support (Support f) ~ Proxy c
+  , Layout f ~ Vector o_n
+  , Layout (Support f) ~ Vector i_n
   ) => f -> ExampleOutput
 exampleOutput = ExampleOutput @i_n @o_n . const . compile