ZkFold.Base.Protocol.Protostar.RecursiveCircuit

Documentation

protostar :: forall f i m c d k a payload input output nx nu ctx. (f ~ FieldElement ctx, i ~ Vector nx, m ~ [f], c ~ f, HomomorphicCommit m c, KnownNat (d - 1), KnownNat (d + 1), KnownNat k, KnownNat (k - 1), Binary a, Arithmetic a, KnownNat nx, KnownNat nu, ctx ~ ArithmeticCircuit a payload input, SymbolicInput (IVCResult f i m c d k), Context (IVCResult f i m c d k) ~ ctx, payload ~ (Payload (IVCResult f i m c d k) :*: U1), input ~ (Layout (IVCResult f i m c d k) :*: U1), output ~ (((Par1 :*: (Vector nx :.: Par1)) :*: ((Vector (k - 1) :.: Par1) :*: ((Vector k :.: Par1) :*: Par1))) :*: ((Vector k :.: Par1) :*: Par1))) => (forall ctx'. Symbolic ctx' => Vector nx (FieldElement ctx') -> Vector nu (FieldElement ctx') -> Vector nx (FieldElement ctx')) -> ArithmeticCircuit a payload input output

Takes a function f and returns a circuit C with input y and witness w. The circuit is such that `C(y, w) = 0` implies that `y = x(n)` for some positive n where `x(k+1) = f(x(k), u(k))` for all k and some u.