zkFold / zkfold-base

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

Add separate "witness layout" for `List`-like datatypes #295

Open TurtlePU opened 1 month ago

TurtlePU commented 1 month ago

Symbolic List, as designed, requires a separate list (Haskell's []) of witnesses to function properly. The problem is, we cannot write a good SymbolicData instance for List as defined currently; however, this can be solved by the following additions:

class (HApplicative c, Package c) => Symbolic c where
  type BaseField c :: Type
+ type WitnessField c :: Type -- for circuits, this is Witness type from MonadCircuit

+ witness :: c f -> f (WitnessField c)
  ...

class SymbolicData d where
  type Context d :: (Type -> Type) -> Type
  type Support d :: Type
  type Layout d :: Type -> Type -- old layout functor
+ type Payload d :: Type -> Type -- new witness functor

- pieces :: d -> Support d -> Context d (Layout d)
+ pieces :: Context d ~ c => d -> Support d -> (c (Layout d), Payload d (Witness c))
- restore :: (Support d -> Context d (Layout d)) -> d
+ restore :: Context d ~ c => (Support d -> (c (Layout d), Payload d (Witness c))) -> d

-data ArithmeticCircuit a i o = ArithmeticCircuit {
+data ArithmeticCircuit a p i o = ArithmeticCircuit {
  acSystem :: Map ByteString (Constraint a i),
  acRange :: Map (SysVar i) a,
- acWitness :: Map ByteString (i a -> Map ByteString a -> a),
+ acWitness :: Map ByteString (p a -> i a -> Map ByteString a -> a),
  acOutput :: o (Var a i)
  }

Setting Payload for lists of type x to be a Stream :.: (Layout x :*: Payload x) (where Stream is an infinite list with Rep Stream = Natural), we get a SymbolicData instance for Lists. Note that the signature for compile function stays (almost) the same: we only need to provide a correct parameter for p, which is Payload (Support f).

Subtasks:

TurtlePU commented 1 month ago

While this is great, there's still room for improvement: notably, when we run the circuit, the Layout and Payload part have to be provided separately, and this looks like a possible source of mistakes.

vlasin commented 1 month ago

Agree with the change to ArithmeticCircuit. Would it be better to make the payload a part of the context?

- pieces :: d -> Support d -> Context d (Layout d)
+ pieces :: Context d ~ c => d -> Support d -> c (Layout d) (Payload d)
- restore :: (Support d -> Context d (Layout d)) -> d
+ restore :: Context d ~ c => (Support d -> c (Layout d) (Payload d)) -> d
TurtlePU commented 1 month ago

Agree with the change to ArithmeticCircuit. Would it be better to make the payload a part of the context?

The "modes" of payload do not agree, sadly: arithmetic circuit is contravariant with respect to payload, while in pieces/restore it has to be covariant