Incorporate all necessary types for zkFold Symbolic smart contracts into the `Symbolic` constraint

[vlasin]

We want a typical zkFold Symbolic smart contract to have the following signature: contract :: (Symbolic t, Arithmetic a) => t Tx a -> t Input a -> t Bool a

Here t could be the identity or ArithmeticCircuit, and a is the chosen finite field.

[vlasin]

@TurtlePU, could you please post your sketches here?

[TurtlePU]

So, after #123, we can view Symbolic datatypes as such:

• While running with Zp p as base — Vector typeSize (Zp p)
• While running with arithmetic circuits as base — ArithmeticCircuit typeSize (Zp p)

After replacing natural indexing with containers as is currently done in #121 and generalizing from Zp p to generic Arithmetic a, we get

• container a for pure backend
• ArithmeticCircuit container a for AC backend

This motivates introducing the following typeclass:

class Arithmetic a => Symbolic a t where
  unit :: t U1 a
  (**) :: t f a -> t g a -> t (f :*: g) a
  symbolic ::
    (SymbolicData a f, SymbolicData a g) =>
    (forall i m . MonadBlueprint i a m => f i -> m (g i)) ->
    (f a -> g a) -> t f a -> t g a

instance Arithmetic a => Symbolic a IdentityT -- pure backend
instance Arithmetic a => Symbolic a ArithmeticCircuit -- AC backend

So the user-end code will look like this:

instance Symbolic a t => AdditiveSemigroup (t (UInt n) a)

contract :: Symbolic a t => t Tx a -> t Input a -> t Bool a

~~With additional type synonyms we can get: type (~>) f g a t = t f a -> t g a type Contract f = forall a t. Symbolic a t => f a t contract :: Contract (Tx ~> Input ~> Bool) ~~

P.S. Also we maybe can add another backend for testing which runs blueprints inside Identity monad and checks if the result matches the one produced by the pure function

P.P.S. Also because of this maybe we can specify different backends for different proving schemes?.. (e.g. simple circuits, PLONKish constraints, lookup arguments etc.). This requires generalizing MonadBlueprint class over which kinds of constraints are available and propagate this change into this new Symbolic class

[TurtlePU]

Actually, there is also a useful typeclass hierarchy preceding Symbolic:

class HFunctor t where
  hmap :: (forall a . f a -> g a) -> t f a -> t g a

class HFunctor t => HApplicative t where
  hpure :: (forall a . f a) -> t f a
  hliftA2 :: (forall a . f a -> g a -> h a) -> t f a -> t g a -> t h a

class Elevator t where
  down :: Functor f => t (f :.: g) a -> f (t g a)
  up :: (Functor f, Foldable f) => f (t g a) -> t (f :.: g) a

class (Arithmetic a, HApplicative t, Elevator t) => Symbolic a t where
  lift :: (Functor f, Foldable f) => f a -> t f a
  symbolic ::
    (SymbolicData a f, SymbolicData a g) =>
    (forall i m . MonadBlueprint i a m => f i -> m (g i)) ->
    (f a -> g a) -> t f a -> t g a

[TurtlePU]

Migration plan

• [x] FFA: #210
• [x] ByteString: #225
• [x] UInt: #216
• [x] FieldElement: #211
• [x] Ed25519: #227
• [x] Cardano types (CtxCompilation, CtxEvaluation): #230
• [x] get rid of MonadBlueprint and move functions from ArithmeticCircuit.Combinators to relevant places of usage: #231
• [x] get rid of Sig-like type aliases: #234