zkFold / zkfold-base

ZkFold's Base library
https://zkfold.io
MIT License
14 stars 6 forks source link

Add structured input to `ArithmeticCircuit`. #117

Closed echatav closed 2 months ago

echatav commented 4 months ago

With structured inputs and outputs, we may sketch definitions of circuits and circuit combinators.


data ArithmeticCircuit i o a = ArithmeticCircuit
  { acConstraints :: Set (Polynomial' a)
  , acValues :: Map Natural a
  , acOutputs :: o Natural
  }

compile
  :: ( Eq a
     , VectorSpace a i
     , Traversable i
     , Functor o
     , Foldable o
     , FunctionSpace (ArithmeticCircuit i Identity a) f
     , i ~ InputSpace (ArithmeticCircuit i Identity a) f
     , o ~ OutputSpace (ArithmeticCircuit i Identity a) f
     )
  => f -> ArithmeticCircuit i o a
compile f = optimize (solder (uncurryV f (desolder idCircuit)))

instance (Eq a, o ~ U1) => Monoid (ArithmeticCircuit i o a) where
  mempty = ArithmeticCircuit mempty mempty mempty
instance (Eq a, o ~ U1) => Semigroup (ArithmeticCircuit i o a) where
  ArithmeticCircuit c1 v1 o1 <> ArithmeticCircuit c2 v2 o2 =
    ArithmeticCircuit (c1 <> c2) (v1 <> v2) (o1 <> o2)

-- | `ArithmeticCircuit`s will maintain the invariant that
-- the input variables are 0,..,i-1
acInputs :: forall a i. (VectorSpace a i, Traversable i) => i Natural
acInputs =
  let
    ai = errorV @a @i "acInputs"
    plusPlus _ = do
      s <- get
      modify (1 +)
      return s
  in
    evalState (traverse plusPlus ai) 0

idCircuit :: forall a i. (Eq a, VectorSpace a i, Traversable i) => ArithmeticCircuit i i a
idCircuit = mempty { acOutputs = acInputs @a @i }

acWitness :: Foldable i => ArithmeticCircuit i o a -> i a -> Map Natural a
acWitness circuit ias =
    let
      oldValues = acValues circuit
      insertVal vals ia = do
        s <- get
        modify (1 +)
        return (Map.insert s ia vals)
    in
      evalState (foldM insertVal oldValues ias) 0

instance (Eq a, VectorSpace a i, Foldable i)
  => FromConstant a (ArithmeticCircuit i Identity a) where
    fromConstant a =
        let
          ai = errorV @a @i "ArithmeticCircuit fromConstant"
          newVar = fromIntegral (length ai)
        in
          ArithmeticCircuit
            { acConstraints = mempty
            , acValues = Map.singleton newVar a
            , acOutputs = Identity newVar
            }

solder
  :: (Eq a, Functor o, Foldable o)
  => o (ArithmeticCircuit i Identity a)
  -> ArithmeticCircuit i o a
solder circuits =
  (fold (fmap (\circuit -> circuit{acOutputs = U1}) circuits))
    { acOutputs = fmap (runIdentity . acOutputs) circuits }

desolder
  :: Functor o
  => ArithmeticCircuit i o a
  -> o (ArithmeticCircuit i Identity a)
desolder circuit =
    fmap (\output -> circuit{acOutputs = Identity output}) (acOutputs circuit)

optimize :: ArithmeticCircuit i o a -> ArithmeticCircuit i o a
optimize = id

errorV :: VectorSpace a v => String -> v a
errorV = pureV . error
echatav commented 4 months ago

@vks4git Here's a sketch with both parametrized inputs & outputs.

TurtlePU commented 2 months ago

Maybe we can close this in favor of #159?

echatav commented 2 months ago

Close in favor of #159