IVC compiler

symbolic-base/src/ZkFold/Base/Protocol/IVC/AlgebraicMap.hs

@@ -20,6 +20,7 @@ import           ZkFold.Base.Data.Vector                             (Vector)
 import           ZkFold.Base.Protocol.IVC.Predicate                  (Predicate (..))
 import           ZkFold.Symbolic.Compiler
 import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal
+import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Var      (NewVar (..), SysVar (..))
 import           ZkFold.Symbolic.Data.Eq
 
 -- | Algebraic map of @a@.
@@ -41,18 +42,18 @@ algebraicMap :: forall d k a i p f .
     -> [f]
 algebraicMap Predicate {..} pi pm _ pad = padDecomposition pad f_sps_uni
     where
-        sys :: [PM.Poly a (SysVar i) Natural]
+        sys :: [ACConstraint a i]
         sys = M.elems (acSystem predicateCircuit)
 
         witness :: Map ByteString f
         witness = M.fromList $ zip (keys $ acWitness predicateCircuit) (V.head pm)
 
-        varMap :: SysVar i -> f
+        varMap :: ACSysVar i -> f
         varMap (InVar inV)            = index pi inV
         varMap (NewVar (EqVar newV))  = M.findWithDefault zero newV witness
         varMap (NewVar (FoldVar _ _)) = P.error "unexpected FOLD constraint"
 
-        f_sps :: Vector (d+1) [PM.Poly a (SysVar i) Natural]
+        f_sps :: Vector (d+1) [ACConstraint a i]
         f_sps = degreeDecomposition @d $ sys
 
         f_sps_uni :: Vector (d+1) [f]

symbolic-base/src/ZkFold/Base/Protocol/Plonkup/LookupConstraint.hs

@@ -11,8 +11,9 @@ import           Test.QuickCheck                                     (Arbitrary
 
 import           ZkFold.Base.Data.ByteString                         (toByteString)
 import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal
+import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Var      (NewVar (..), SysVar (..))
 
-newtype LookupConstraint i a = LookupConstraint { lkVar :: SysVar i }
+newtype LookupConstraint i a = LookupConstraint { lkVar :: ACSysVar i }
 
 deriving instance Show (Rep i) => Show (LookupConstraint i a)
 deriving instance Eq (Rep i) => Eq (LookupConstraint i a)

symbolic-base/src/ZkFold/Base/Protocol/Plonkup/PlonkConstraint.hs

@@ -26,17 +26,17 @@ import           ZkFold.Base.Algebra.Polynomials.Multivariate        (Poly, eval
 import           ZkFold.Base.Data.ByteString                         (toByteString)
 import           ZkFold.Prelude                                      (length, take)
 import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal
-import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Var      (toVar)
+import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Var
 
 data PlonkConstraint i a = PlonkConstraint
     { qm :: a
     , ql :: a
     , qr :: a
     , qo :: a
     , qc :: a
-    , x1 :: Var a i
-    , x2 :: Var a i
-    , x3 :: Var a i
+    , x1 :: ACVar a i
+    , x2 :: ACVar a i
+    , x3 :: ACVar a i
     }
 
 deriving instance (Show a, Show (Rep i)) => Show (PlonkConstraint i a)
@@ -54,7 +54,7 @@ instance (Ord a, Arbitrary a, Binary a, Ord (Rep i), Semiring a) => Arbitrary (P
         let x1 = head xs; x2 = xs !! 1; x3 = xs !! 2
         return $ PlonkConstraint qm ql qr qo qc x1 x2 x3
 
-toPlonkConstraint :: forall a i . (Ord a, FiniteField a, Ord (Rep i)) => Poly a (Var a i) Natural -> PlonkConstraint i a
+toPlonkConstraint :: forall a i . (Ord a, FiniteField a, Ord (Rep i)) => Poly a (ACVar a i) Natural -> PlonkConstraint i a
 toPlonkConstraint p =
     let xs    = Just <$> toList (variables p)
         perms = nubOrd $ map (take 3) $ permutations $ case length xs of
@@ -63,12 +63,12 @@ toPlonkConstraint p =
             2 -> [Nothing] ++ xs ++ xs
             _ -> xs ++ xs
 
-        getCoef :: Map (Maybe (Var a i)) Natural -> a
+        getCoef :: Map (Maybe (ACVar a i)) Natural -> a
         getCoef m = case find (\(_, as) -> m == Map.mapKeys Just as) (toList p) of
             Just (c, _) -> c
             _           -> zero
 
-        getCoefs :: [Maybe (Var a i)] -> Maybe (PlonkConstraint i a)
+        getCoefs :: [Maybe (ACVar a i)] -> Maybe (PlonkConstraint i a)
         getCoefs [a, b, c] = do
             let xa = [(a, 1)]
                 xb = [(b, 1)]
@@ -91,7 +91,7 @@ toPlonkConstraint p =
         [] -> toPlonkConstraint zero
         _  -> head $ mapMaybe getCoefs perms
 
-fromPlonkConstraint :: (Ord a, Field a, Ord (Rep i)) => PlonkConstraint i a -> Poly a (Var a i) Natural
+fromPlonkConstraint :: (Ord a, Field a, Ord (Rep i)) => PlonkConstraint i a -> Poly a (ACVar a i) Natural
 fromPlonkConstraint (PlonkConstraint qm ql qr qo qc a b c) =
     let xa = var a
         xb = var b

symbolic-base/src/ZkFold/Base/Protocol/Plonkup/PlonkupConstraint.hs

@@ -20,17 +20,17 @@ isLookupConstraint :: FiniteField a => PlonkupConstraint i a -> a
 isLookupConstraint (ConsLookup _) = one
 isLookupConstraint _              = zero
 
-getA :: forall a i . (Ord a, FiniteField a, Ord (Rep i)) => PlonkupConstraint i a -> Var a i
+getA :: forall a i . (Ord a, FiniteField a, Ord (Rep i)) => PlonkupConstraint i a -> ACVar a i
 getA (ConsPlonk c)  = x1 c
 getA (ConsLookup c) = toVar $ lkVar c
 getA ConsExtra      = x1 (toPlonkConstraint zero)
 
-getB :: forall a i . (Ord a, FiniteField a, Ord (Rep i)) => PlonkupConstraint i a -> Var a i
+getB :: forall a i . (Ord a, FiniteField a, Ord (Rep i)) => PlonkupConstraint i a -> ACVar a i
 getB (ConsPlonk c)  = x2 c
 getB (ConsLookup c) = toVar $ lkVar c
 getB ConsExtra      = x2 (toPlonkConstraint zero)
 
-getC :: forall a i . (Ord a, FiniteField a, Ord (Rep i)) => PlonkupConstraint i a -> Var a i
+getC :: forall a i . (Ord a, FiniteField a, Ord (Rep i)) => PlonkupConstraint i a -> ACVar a i
 getC (ConsPlonk c)  = x3 c
 getC (ConsLookup c) = toVar $ lkVar c
 getC ConsExtra      = x3 (toPlonkConstraint zero)

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

@@ -101,7 +101,7 @@ compileIO ::
   , SymbolicData f
   , Context f ~ c
   , Support f ~ s
-  , ToJSON (Layout f (Var a l))
+  , ToJSON (Layout f (ACVar a l))
   , SymbolicInput s
   , Context s ~ c
   , Layout s ~ l

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

@@ -2,8 +2,8 @@
 
 module ZkFold.Symbolic.Compiler.ArithmeticCircuit (
         ArithmeticCircuit,
+        ACVar,
         Constraint,
-        Var,
         witnessGenerator,
         -- high-level functions
         optimize,
@@ -68,7 +68,7 @@ import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Instance     ()
 import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal
 import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Map
 import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Optimization
-import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Var          (toVar)
+import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Var          (SysVar (..), toVar)
 import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Witness      (WitnessF)
 import           ZkFold.Symbolic.Data.Combinators                        (expansion)
 import           ZkFold.Symbolic.MonadCircuit                            (MonadCircuit (..))
@@ -140,7 +140,7 @@ acValue = exec
 -- TODO: Check that all arguments have been applied.
 acPrint ::
   (Arithmetic a, Binary a, Show a) =>
-  (Show (o (Var a U1)), Show (o a), Functor o) =>
+  (Show (o (ACVar a U1)), Show (o a), Functor o) =>
   ArithmeticCircuit a U1 U1 o -> IO ()
 acPrint ac = do
     let m = elems (acSystem ac)

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

@@ -0,0 +1,120 @@
+{-# LANGUAGE TypeOperators #-}
+
+module ZkFold.Symbolic.Compiler.ArithmeticCircuit.IVC where
+
+import           Control.Applicative                                 (Applicative (..))
+import           Control.Monad.State                                 (State)
+import           Data.ByteString                                     (ByteString)
+import           Data.Either                                         (Either (..))
+import           Data.Foldable                                       (Foldable (..))
+import           Data.Function                                       ((.))
+import           Data.Functor                                        (Functor (..))
+import           Data.Functor.Rep                                    (Rep)
+import           Data.List.Infinite                                  (Infinite)
+import           Data.Map.Lazy                                       (Map)
+import qualified Data.Map.Lazy                                       as M
+import           Data.Maybe                                          (fromJust)
+import           Data.Monoid                                         (Monoid (..))
+import           Data.Semigroup                                      (Semigroup (..))
+import           Data.Tuple                                          (uncurry)
+import           GHC.Generics                                        (Par1 (..), U1 (..), (:*:) (..), (:.:))
+import           Prelude                                             (error)
+
+import           ZkFold.Base.Algebra.Basic.Class
+import           ZkFold.Base.Control.HApplicative                    (HApplicative (..))
+import           ZkFold.Base.Data.ByteString                         (Binary, fromByteString)
+import           ZkFold.Symbolic.Class                               (Symbolic (..))
+import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal
+import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Var      (SysVar, Var)
+import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Witness  (WitnessF)
+import           ZkFold.Symbolic.Data.Bool                           (Bool)
+import           ZkFold.Symbolic.Data.Class                          (LayoutFunctor, PayloadFunctor)
+import           ZkFold.Symbolic.Data.Conditional                    (Conditional (..))
+import           ZkFold.Symbolic.Data.FieldElement                   (FieldElement (..))
+import           ZkFold.Symbolic.Data.Ord                            (Ord (..))
+
+data RangeEntry a v = RangeEntry
+  { reUpperBound :: a
+  , reRangedVars :: [v]
+  }
+
+type PCWitness v a p i = WitnessF a (Either (Rep p) (SysVar i v))
+
+data PrimitiveCircuit v a p i n o = PrimitiveCircuit
+  { pcSystem  :: [Constraint a i v]
+  , pcRange   :: [RangeEntry a (SysVar i v)]
+  , pcWitness :: Map v (PCWitness v a p i)
+  , pcPayload :: n (PCWitness v a p i)
+  , pcOutput  :: o (Var a i v)
+  }
+
+data RecursiveCircuit v a p i n o =
+  forall sp si it.
+  RecursiveCircuit
+  { rcStep :: PrimitiveCircuit v a sp (si :*: it) sp si
+  , rcBoot :: PrimitiveCircuit v a (p :*: sp) (i :*: si)
+                  (n :*: sp :*: (Infinite :.: it))
+                  (o :*: si :*: Par1)
+  }
+
+data FoldingCircuit a ext =
+  forall p l i.
+  FoldingCircuit
+  { fcLayoutStep  :: ArithmeticCircuit a p (l :*: i) l
+  , fcWitnessStep :: p (CircuitWitness a p (l :*: i))
+  , fcSeedPayload :: p (WitnessField ext)
+  , fcSeedLayout  :: ext l
+  , fcStream      :: Infinite (i (WitnessField ext))
+  , fcCount       :: FieldElement ext
+  , fcOutPayload  :: Map ByteString (ByteString -> Rep p)
+  , fcOutLayout   :: Map ByteString (ByteString -> Rep l)
+  }
+
+fromFold ::
+  ByteString -> CircuitFold a (ACVar a i) (CircuitWitness a p i) ->
+  FoldingCircuit a (ArithmeticCircuit a p i)
+fromFold fldID CircuitFold {..} = FoldingCircuit
+  { fcLayoutStep = foldStep
+  , fcWitnessStep = foldStepP
+  , fcSeedPayload = foldSeedP
+  , fcSeedLayout = emptyCircuit { acOutput = foldSeed }
+  , fcStream = foldStream
+  , fcCount = FieldElement emptyCircuit { acOutput = Par1 foldCount }
+  , fcOutPayload = M.singleton fldID (fromJust . fromByteString)
+  , fcOutLayout = M.singleton fldID (fromJust . fromByteString)
+  }
+
+instance Symbolic c => Semigroup (FoldingCircuit a c) where
+  FoldingCircuit _ _ sp sl s k op ol <> FoldingCircuit _ _ tp tl t l pp pl =
+    FoldingCircuit
+      { fcLayoutStep = error "TODO"
+      , fcWitnessStep = error "TODO"
+      , fcSeedPayload = sp :*: tp
+      , fcSeedLayout = hpair sl tl
+      , fcStream = liftA2 (:*:) s t
+      , fcCount = bool k l (k < l :: Bool c)
+      , fcOutPayload = fmap (Left .) op <> fmap (Right .) pp
+      , fcOutLayout = fmap (Left .) ol <> fmap (Right .) pl
+      }
+
+instance Symbolic c => Monoid (FoldingCircuit a c) where
+  mempty = FoldingCircuit
+    { fcLayoutStep = emptyCircuit
+    , fcWitnessStep = U1
+    , fcSeedPayload = U1
+    , fcSeedLayout = hunit
+    , fcStream = pure U1
+    , fcCount = zero
+    , fcOutPayload = M.empty
+    , fcOutLayout = M.empty
+    }
+
+recursiveCircuit ::
+  ArithmeticCircuit a p i o -> State [v] (RecursiveCircuit v a p i U1 o)
+recursiveCircuit = error "TODO"
+
+foldingCircuit ::
+  (Arithmetic a, Binary a, LayoutFunctor i, PayloadFunctor p) =>
+  Map ByteString (CircuitFold a (ACVar a i) (CircuitWitness a p i)) ->
+  FoldingCircuit a (ArithmeticCircuit a p i)
+foldingCircuit = foldMap (uncurry fromFold) . M.assocs

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

@@ -105,14 +105,14 @@ createRangeConstraint (FieldElement x) a = FieldElement $ fromCircuitF x (\ (Par
       return v
 
 -- TODO: make it more readable
-instance (Show a, Show (o (Var a i)), Show (Var a i), Show (Rep i), Haskell.Ord (Rep i)) => Show (ArithmeticCircuit a p i o) where
+instance (Show a, Show (o (ACVar a i)), Show (ACVar a i), Show (Rep i), Haskell.Ord (Rep i)) => Show (ArithmeticCircuit a p i o) where
     show r = "ArithmeticCircuit { acSystem = " ++ show (acSystem r)
                           ++ "\n, acRange = " ++ show (acRange r)
                           ++ "\n, acOutput = " ++ show (acOutput r)
                           ++ " }"
 
 -- TODO: add witness generation info to the JSON object
-instance (ToJSON a, ToJSON (o (Var a i)), ToJSONKey a, FromJSONKey (Var a i), ToJSON (Rep i)) => ToJSON (ArithmeticCircuit a p i o) where
+instance (ToJSON a, ToJSON (o (ACVar a i)), ToJSONKey a, FromJSONKey (ACVar a i), ToJSON (Rep i)) => ToJSON (ArithmeticCircuit a p i o) where
     toJSON r = object
         [
             "system" .= acSystem r,
@@ -121,7 +121,7 @@ instance (ToJSON a, ToJSON (o (Var a i)), ToJSONKey a, FromJSONKey (Var a i), To
         ]
 
 -- TODO: properly restore the witness generation function
-instance (FromJSON a, FromJSON (o (Var a i)), ToJSONKey (Var a i), FromJSONKey a, Haskell.Ord a, Haskell.Ord (Rep i), FromJSON (Rep i)) => FromJSON (ArithmeticCircuit a p i o) where
+instance (FromJSON a, FromJSON (o (ACVar a i)), ToJSONKey (ACVar a i), FromJSONKey a, Haskell.Ord a, Haskell.Ord (Rep i), FromJSON (Rep i)) => FromJSON (ArithmeticCircuit a p i o) where
     parseJSON =
         withObject "ArithmeticCircuit" $ \v -> do
             acSystem   <- v .: "system"