{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeOperators       #-}

module ZkFold.Base.Protocol.Protostar.RecursiveCircuit where

import           GHC.Generics                                          (Par1 (..), U1 (..), type (:.:) (..), (:*:) (..))
import           Prelude                                               hiding (Num (..), drop, head, replicate, take,
                                                                        zipWith)

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Algebra.Basic.Number                      (KnownNat, type (+), type (-), value)
import           ZkFold.Base.Data.ByteString                           (Binary)
import           ZkFold.Base.Data.Vector                               (Vector, unsafeToVector)
import           ZkFold.Base.Protocol.Protostar.ArithmetizableFunction (ArithmetizableFunction (ArithmetizableFunction))
import           ZkFold.Base.Protocol.Protostar.Commit                 (HomomorphicCommit)
import           ZkFold.Base.Protocol.Protostar.CommitOpen             (CommitOpen (..))
import           ZkFold.Base.Protocol.Protostar.FiatShamir             (FiatShamir (..))
import           ZkFold.Base.Protocol.Protostar.IVC                    (IVCResult, ivcVerify)
import           ZkFold.Prelude                                        (replicate)
import           ZkFold.Symbolic.Class
import           ZkFold.Symbolic.Compiler
import           ZkFold.Symbolic.Data.Class                            (SymbolicData (..))
import           ZkFold.Symbolic.Data.FieldElement                     (FieldElement (..))
import           ZkFold.Symbolic.Data.Input                            (SymbolicInput)
import           ZkFold.Symbolic.Interpreter                           (Interpreter (..))

-- | 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`.
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
protostar :: forall f (i :: Type -> Type) m c (d :: Natural) (k :: Natural) a
       (payload :: Type -> Type) (input :: Type -> Type)
       (output :: Type -> Type) (nx :: Natural) (nu :: Natural)
       (ctx :: (Type -> Type) -> Type).
(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' :: (Type -> Type) -> Type).
 Symbolic ctx' =>
 Vector nx (FieldElement ctx')
 -> Vector nu (FieldElement ctx') -> Vector nx (FieldElement ctx'))
-> ArithmeticCircuit a payload input output
protostar forall (ctx' :: (Type -> Type) -> Type).
Symbolic ctx' =>
Vector nx (FieldElement ctx')
-> Vector nu (FieldElement ctx') -> Vector nx (FieldElement ctx')
func =
    let
        -- The numeric interpretation of the function `f`.
        stepFunction :: Vector nx a -> Vector nu a -> Vector nx a
        stepFunction :: Vector nx a -> Vector nu a -> Vector nx a
stepFunction Vector nx a
x' Vector nu a
u' =
            let x :: Vector nx (FieldElement (Interpreter a))
x = a -> FieldElement (Interpreter a)
forall a b. FromConstant a b => a -> b
fromConstant (a -> FieldElement (Interpreter a))
-> Vector nx a -> Vector nx (FieldElement (Interpreter a))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector nx a
x' :: Vector nx (FieldElement (Interpreter a))
                u :: Vector nu (FieldElement (Interpreter a))
u = a -> FieldElement (Interpreter a)
forall a b. FromConstant a b => a -> b
fromConstant (a -> FieldElement (Interpreter a))
-> Vector nu a -> Vector nu (FieldElement (Interpreter a))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector nu a
u' :: Vector nu (FieldElement (Interpreter a))
            in Par1 a -> a
forall p. Par1 p -> p
unPar1 (Par1 a -> a)
-> (FieldElement (Interpreter a) -> Par1 a)
-> FieldElement (Interpreter a)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Interpreter a Par1 -> Par1 a
forall {k} (a :: k) (f :: k -> Type). Interpreter a f -> f a
runInterpreter (Interpreter a Par1 -> Par1 a)
-> (FieldElement (Interpreter a) -> Interpreter a Par1)
-> FieldElement (Interpreter a)
-> Par1 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FieldElement (Interpreter a) -> Interpreter a Par1
forall (c :: (Type -> Type) -> Type). FieldElement c -> c Par1
fromFieldElement (FieldElement (Interpreter a) -> a)
-> Vector nx (FieldElement (Interpreter a)) -> Vector nx a
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector nx (FieldElement (Interpreter a))
-> Vector nu (FieldElement (Interpreter a))
-> Vector nx (FieldElement (Interpreter a))
forall (ctx' :: (Type -> Type) -> Type).
Symbolic ctx' =>
Vector nx (FieldElement ctx')
-> Vector nu (FieldElement ctx') -> Vector nx (FieldElement ctx')
func Vector nx (FieldElement (Interpreter a))
x Vector nu (FieldElement (Interpreter a))
u

        -- The step circuit for the recursion implements the function `F(x, u, y) = f(x, u) - y`.
        -- Here `x` and `u` are the private inputs and `y` is the public input.
        stepCircuit :: ArithmeticCircuit a (Vector nx :*: Vector nu) (Vector nx) U1
        stepCircuit :: ArithmeticCircuit a (Vector nx :*: Vector nu) (Vector nx) U1
stepCircuit =
            (forall x.
 (:*:) (Vector nx) (Vector nu) x
 -> (:*:) (Vector nx :.: Par1) (Vector nu :.: Par1) x)
-> ArithmeticCircuit
     a ((Vector nx :.: Par1) :*: (Vector nu :.: Par1)) (Vector nx) U1
-> ArithmeticCircuit a (Vector nx :*: Vector nu) (Vector nx) U1
forall (p :: Type -> Type) (q :: Type -> Type) a
       (i :: Type -> Type) (o :: Type -> Type).
(Representable p, Representable q) =>
(forall x. q x -> p x)
-> ArithmeticCircuit a p i o -> ArithmeticCircuit a q i o
hpmap (\(Vector nx x
x :*: Vector nu x
u) -> Vector nx (Par1 x) -> (:.:) (Vector nx) Par1 x
forall k2 k1 (f :: k2 -> Type) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1 (x -> Par1 x
forall p. p -> Par1 p
Par1 (x -> Par1 x) -> Vector nx x -> Vector nx (Par1 x)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector nx x
x) (:.:) (Vector nx) Par1 x
-> (:.:) (Vector nu) Par1 x
-> (:*:) (Vector nx :.: Par1) (Vector nu :.: Par1) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: Vector nu (Par1 x) -> (:.:) (Vector nu) Par1 x
forall k2 k1 (f :: k2 -> Type) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1 (x -> Par1 x
forall p. p -> Par1 p
Par1 (x -> Par1 x) -> Vector nu x -> Vector nu (Par1 x)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector nu x
u)) (ArithmeticCircuit
   a ((Vector nx :.: Par1) :*: (Vector nu :.: Par1)) (Vector nx) U1
 -> ArithmeticCircuit a (Vector nx :*: Vector nu) (Vector nx) U1)
-> ArithmeticCircuit
     a ((Vector nx :.: Par1) :*: (Vector nu :.: Par1)) (Vector nx) U1
-> ArithmeticCircuit a (Vector nx :*: Vector nu) (Vector nx) U1
forall a b. (a -> b) -> a -> b
$
            (forall x. Vector nx x -> (:*:) U1 (Vector nx :.: Par1) x)
-> ArithmeticCircuit
     a
     ((Vector nx :.: Par1) :*: (Vector nu :.: Par1))
     (U1 :*: (Vector nx :.: Par1))
     U1
-> ArithmeticCircuit
     a ((Vector nx :.: Par1) :*: (Vector nu :.: Par1)) (Vector nx) U1
forall (i :: Type -> Type) (j :: Type -> Type) (o :: Type -> Type)
       a (p :: Type -> Type).
(Representable i, Representable j, Ord (Rep j), Functor o) =>
(forall x. j x -> i x)
-> ArithmeticCircuit a p i o -> ArithmeticCircuit a p j o
hlmap (\Vector nx x
x -> U1 x
forall k (p :: k). U1 p
U1 U1 x -> (:.:) (Vector nx) Par1 x -> (:*:) U1 (Vector nx :.: Par1) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: Vector nx (Par1 x) -> (:.:) (Vector nx) Par1 x
forall k2 k1 (f :: k2 -> Type) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1 (x -> Par1 x
forall p. p -> Par1 p
Par1 (x -> Par1 x) -> Vector nx x -> Vector nx (Par1 x)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector nx x
x)) (ArithmeticCircuit
   a
   ((Vector nx :.: Par1) :*: (Vector nu :.: Par1))
   (U1 :*: (Vector nx :.: Par1))
   U1
 -> ArithmeticCircuit
      a ((Vector nx :.: Par1) :*: (Vector nu :.: Par1)) (Vector nx) U1)
-> ArithmeticCircuit
     a
     ((Vector nx :.: Par1) :*: (Vector nu :.: Par1))
     (U1 :*: (Vector nx :.: Par1))
     U1
-> ArithmeticCircuit
     a ((Vector nx :.: Par1) :*: (Vector nu :.: Par1)) (Vector nx) U1
forall a b. (a -> b) -> a -> b
$
            forall a y (p :: Type -> Type) (i :: Type -> Type)
       (q :: Type -> Type) (j :: Type -> Type) s f
       (c0 :: (Type -> Type) -> Type) (c1 :: (Type -> Type) -> Type).
(CompilesWith c0 s f, c0 ~ ArithmeticCircuit a p i,
 Representable p, Representable i, RestoresFrom c1 y,
 c1 ~ ArithmeticCircuit a q j, Binary a, Binary (Rep p),
 Binary (Rep i), Ord (Rep i)) =>
(c0 (Layout f) -> c1 (Layout y))
-> (forall x. p x -> i x -> (Payload s x, Layout s x)) -> f -> y
compileWith @a ArithmeticCircuit
  a
  ((Vector nx :.: Par1) :*: (Vector nu :.: Par1))
  U1
  (Vector nx :.: Par1)
-> ArithmeticCircuit
     a
     ((Vector nx :.: Par1) :*: (Vector nu :.: Par1))
     (U1 :*: (Vector nx :.: Par1))
     U1
ArithmeticCircuit
  a
  ((Vector nx :.: Par1) :*: (Vector nu :.: Par1))
  U1
  (Layout
     (Vector
        nx
        (FieldElement
           (ArithmeticCircuit
              a ((Vector nx :.: Par1) :*: (Vector nu :.: Par1)) U1))
      -> Vector
           nu
           (FieldElement
              (ArithmeticCircuit
                 a ((Vector nx :.: Par1) :*: (Vector nu :.: Par1)) U1))
      -> Vector
           nx
           (FieldElement
              (ArithmeticCircuit
                 a ((Vector nx :.: Par1) :*: (Vector nu :.: Par1)) U1))))
-> ArithmeticCircuit
     a
     ((Vector nx :.: Par1) :*: (Vector nu :.: Par1))
     (U1 :*: (Vector nx :.: Par1))
     (Layout
        (ArithmeticCircuit
           a
           ((Vector nx :.: Par1) :*: (Vector nu :.: Par1))
           (U1 :*: (Vector nx :.: Par1))
           U1))
forall a (p :: Type -> Type) (i :: Type -> Type)
       (o :: Type -> Type).
(Arithmetic a, Binary a, Binary (Rep p), Binary (Rep i),
 Binary (Rep o), Ord (Rep i), Ord (Rep o), NFData (Rep i),
 NFData (Rep o), Representable i, Representable o, Foldable o) =>
ArithmeticCircuit a p i o -> ArithmeticCircuit a p (i :*: o) U1
guessOutput (\((:.:) (Vector nx) Par1 x
x :*: (:.:) (Vector nu) Par1 x
u) U1 x
U1 ->
                    ( Vector nx (U1 x) -> (:.:) (Vector nx) U1 x
forall k2 k1 (f :: k2 -> Type) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1 ([U1 x] -> Vector nx (U1 x)
forall (size :: Natural) a. [a] -> Vector size a
unsafeToVector ([U1 x] -> Vector nx (U1 x)) -> [U1 x] -> Vector nx (U1 x)
forall a b. (a -> b) -> a -> b
$ Natural -> U1 x -> [U1 x]
forall a. Natural -> a -> [a]
replicate (forall (n :: Natural). KnownNat n => Natural
value @nx) U1 x
forall k (p :: k). U1 p
U1) (:.:) (Vector nx) U1 x
-> (:*:) (Vector nu :.: U1) U1 x
-> (:*:) (Vector nx :.: U1) ((Vector nu :.: U1) :*: U1) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: Vector nu (U1 x) -> (:.:) (Vector nu) U1 x
forall k2 k1 (f :: k2 -> Type) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1 ([U1 x] -> Vector nu (U1 x)
forall (size :: Natural) a. [a] -> Vector size a
unsafeToVector ([U1 x] -> Vector nu (U1 x)) -> [U1 x] -> Vector nu (U1 x)
forall a b. (a -> b) -> a -> b
$ Natural -> U1 x -> [U1 x]
forall a. Natural -> a -> [a]
replicate (forall (n :: Natural). KnownNat n => Natural
value @nx) U1 x
forall k (p :: k). U1 p
U1) (:.:) (Vector nu) U1 x -> U1 x -> (:*:) (Vector nu :.: U1) U1 x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: U1 x
forall k (p :: k). U1 p
U1
                    , (:.:) (Vector nx) Par1 x
x (:.:) (Vector nx) Par1 x
-> (:*:) (Vector nu :.: Par1) U1 x
-> (:*:) (Vector nx :.: Par1) ((Vector nu :.: Par1) :*: U1) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: (:.:) (Vector nu) Par1 x
u (:.:) (Vector nu) Par1 x -> U1 x -> (:*:) (Vector nu :.: Par1) U1 x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: U1 x
forall k (p :: k). U1 p
U1)
                ) Vector
  nx
  (FieldElement
     (ArithmeticCircuit
        a ((Vector nx :.: Par1) :*: (Vector nu :.: Par1)) U1))
-> Vector
     nu
     (FieldElement
        (ArithmeticCircuit
           a ((Vector nx :.: Par1) :*: (Vector nu :.: Par1)) U1))
-> Vector
     nx
     (FieldElement
        (ArithmeticCircuit
           a ((Vector nx :.: Par1) :*: (Vector nu :.: Par1)) U1))
forall (ctx' :: (Type -> Type) -> Type).
Symbolic ctx' =>
Vector nx (FieldElement ctx')
-> Vector nu (FieldElement ctx') -> Vector nx (FieldElement ctx')
func

        -- Protostar IVC takes an arithmetizable function as input.
        af :: ArithmetizableFunction a (Vector nx) (Vector nu)
        af :: ArithmetizableFunction a (Vector nx) (Vector nu)
af = (Vector nx a -> Vector nu a -> Vector nx a)
-> ArithmeticCircuit a (Vector nx :*: Vector nu) (Vector nx) U1
-> ArithmetizableFunction a (Vector nx) (Vector nu)
forall a (i :: Type -> Type) (p :: Type -> Type).
(i a -> p a -> i a)
-> ArithmeticCircuit a (i :*: p) i U1
-> ArithmetizableFunction a i p
ArithmetizableFunction Vector nx a -> Vector nu a -> Vector nx a
stepFunction ArithmeticCircuit a (Vector nx :*: Vector nu) (Vector nx) U1
stepCircuit

        -- The Fiat-Shamired commit-open special-sound protocol for the arithmetizable function
        fs :: FiatShamir (CommitOpen (ArithmetizableFunction a (Vector nx) (Vector nu)))
        fs :: FiatShamir
  (CommitOpen (ArithmetizableFunction a (Vector nx) (Vector nu)))
fs = CommitOpen (ArithmetizableFunction a (Vector nx) (Vector nu))
-> FiatShamir
     (CommitOpen (ArithmetizableFunction a (Vector nx) (Vector nu)))
forall a. a -> FiatShamir a
FiatShamir (ArithmetizableFunction a (Vector nx) (Vector nu)
-> CommitOpen (ArithmetizableFunction a (Vector nx) (Vector nu))
forall a. a -> CommitOpen a
CommitOpen ArithmetizableFunction a (Vector nx) (Vector nu)
af)

        -- The verification function for the IVC result object
        vf :: IVCResult f i m c d k -> ((f, i f, Vector (k-1) f, Vector k c, c), (Vector k c, c))
        vf :: IVCResult f i m c d k
-> ((f, i f, Vector (k - 1) f, Vector k c, c), (Vector k c, c))
vf = forall f (i :: Type -> Type) m c (d :: Natural) (k :: Natural) a.
AccumulatorScheme f i m c d k a =>
a
-> IVCResult f i m c d k
-> ((f, i f, Vector (k - 1) f, Vector k c, c), (Vector k c, c))
ivcVerify @f @i @m @c @d @k FiatShamir
  (CommitOpen (ArithmetizableFunction a (Vector nx) (Vector nu)))
fs

        -- -- TODO: the circuit functors must be adjusted for better usability
        circuit :: ArithmeticCircuit a payload input output
circuit = forall a y f (c :: (Type -> Type) -> Type) s.
(CompilesWith c s f, RestoresFrom c y, Layout y ~ Layout f,
 c ~ ArithmeticCircuit a (Payload s) (Layout s)) =>
f -> y
compile @a IVCResult f i m c d k
-> ((f, i f, Vector (k - 1) f, Vector k c, c), (Vector k c, c))
IVCResult
  (FieldElement
     (ArithmeticCircuit
        a
        (Payload
           (IVCResult
              (FieldElement (ArithmeticCircuit a payload input))
              (Vector nx)
              [FieldElement (ArithmeticCircuit a payload input)]
              (FieldElement (ArithmeticCircuit a payload input))
              d
              k)
         :*: U1)
        (Layout
           (IVCResult
              (FieldElement
                 (ArithmeticCircuit
                    a
                    (Payload
                       (IVCResult
                          (FieldElement (ArithmeticCircuit a payload input))
                          (Vector nx)
                          [FieldElement (ArithmeticCircuit a payload input)]
                          (FieldElement (ArithmeticCircuit a payload input))
                          d
                          k)
                     :*: U1)
                    input))
              (Vector nx)
              [FieldElement
                 (ArithmeticCircuit
                    a
                    (Payload
                       (IVCResult
                          (FieldElement (ArithmeticCircuit a payload input))
                          (Vector nx)
                          [FieldElement (ArithmeticCircuit a payload input)]
                          (FieldElement (ArithmeticCircuit a payload input))
                          d
                          k)
                     :*: U1)
                    input)]
              (FieldElement
                 (ArithmeticCircuit
                    a
                    (Payload
                       (IVCResult
                          (FieldElement (ArithmeticCircuit a payload input))
                          (Vector nx)
                          [FieldElement (ArithmeticCircuit a payload input)]
                          (FieldElement (ArithmeticCircuit a payload input))
                          d
                          k)
                     :*: U1)
                    input))
              d
              k)
         :*: U1)))
  (Vector nx)
  [FieldElement
     (ArithmeticCircuit
        a
        (Payload
           (IVCResult
              (FieldElement (ArithmeticCircuit a payload input))
              (Vector nx)
              [FieldElement (ArithmeticCircuit a payload input)]
              (FieldElement (ArithmeticCircuit a payload input))
              d
              k)
         :*: U1)
        (Layout
           (IVCResult
              (FieldElement
                 (ArithmeticCircuit
                    a
                    (Payload
                       (IVCResult
                          (FieldElement (ArithmeticCircuit a payload input))
                          (Vector nx)
                          [FieldElement (ArithmeticCircuit a payload input)]
                          (FieldElement (ArithmeticCircuit a payload input))
                          d
                          k)
                     :*: U1)
                    input))
              (Vector nx)
              [FieldElement
                 (ArithmeticCircuit
                    a
                    (Payload
                       (IVCResult
                          (FieldElement (ArithmeticCircuit a payload input))
                          (Vector nx)
                          [FieldElement (ArithmeticCircuit a payload input)]
                          (FieldElement (ArithmeticCircuit a payload input))
                          d
                          k)
                     :*: U1)
                    input)]
              (FieldElement
                 (ArithmeticCircuit
                    a
                    (Payload
                       (IVCResult
                          (FieldElement (ArithmeticCircuit a payload input))
                          (Vector nx)
                          [FieldElement (ArithmeticCircuit a payload input)]
                          (FieldElement (ArithmeticCircuit a payload input))
                          d
                          k)
                     :*: U1)
                    input))
              d
              k)
         :*: U1))]
  (FieldElement
     (ArithmeticCircuit
        a
        (Payload
           (IVCResult
              (FieldElement (ArithmeticCircuit a payload input))
              (Vector nx)
              [FieldElement (ArithmeticCircuit a payload input)]
              (FieldElement (ArithmeticCircuit a payload input))
              d
              k)
         :*: U1)
        (Layout
           (IVCResult
              (FieldElement
                 (ArithmeticCircuit
                    a
                    (Payload
                       (IVCResult
                          (FieldElement (ArithmeticCircuit a payload input))
                          (Vector nx)
                          [FieldElement (ArithmeticCircuit a payload input)]
                          (FieldElement (ArithmeticCircuit a payload input))
                          d
                          k)
                     :*: U1)
                    input))
              (Vector nx)
              [FieldElement
                 (ArithmeticCircuit
                    a
                    (Payload
                       (IVCResult
                          (FieldElement (ArithmeticCircuit a payload input))
                          (Vector nx)
                          [FieldElement (ArithmeticCircuit a payload input)]
                          (FieldElement (ArithmeticCircuit a payload input))
                          d
                          k)
                     :*: U1)
                    input)]
              (FieldElement
                 (ArithmeticCircuit
                    a
                    (Payload
                       (IVCResult
                          (FieldElement (ArithmeticCircuit a payload input))
                          (Vector nx)
                          [FieldElement (ArithmeticCircuit a payload input)]
                          (FieldElement (ArithmeticCircuit a payload input))
                          d
                          k)
                     :*: U1)
                    input))
              d
              k)
         :*: U1)))
  d
  k
-> ((FieldElement
       (ArithmeticCircuit
          a
          (Payload
             (IVCResult
                (FieldElement (ArithmeticCircuit a payload input))
                (Vector nx)
                [FieldElement (ArithmeticCircuit a payload input)]
                (FieldElement (ArithmeticCircuit a payload input))
                d
                k)
           :*: U1)
          (Layout
             (IVCResult
                (FieldElement
                   (ArithmeticCircuit
                      a
                      (Payload
                         (IVCResult
                            (FieldElement (ArithmeticCircuit a payload input))
                            (Vector nx)
                            [FieldElement (ArithmeticCircuit a payload input)]
                            (FieldElement (ArithmeticCircuit a payload input))
                            d
                            k)
                       :*: U1)
                      input))
                (Vector nx)
                [FieldElement
                   (ArithmeticCircuit
                      a
                      (Payload
                         (IVCResult
                            (FieldElement (ArithmeticCircuit a payload input))
                            (Vector nx)
                            [FieldElement (ArithmeticCircuit a payload input)]
                            (FieldElement (ArithmeticCircuit a payload input))
                            d
                            k)
                       :*: U1)
                      input)]
                (FieldElement
                   (ArithmeticCircuit
                      a
                      (Payload
                         (IVCResult
                            (FieldElement (ArithmeticCircuit a payload input))
                            (Vector nx)
                            [FieldElement (ArithmeticCircuit a payload input)]
                            (FieldElement (ArithmeticCircuit a payload input))
                            d
                            k)
                       :*: U1)
                      input))
                d
                k)
           :*: U1)),
     Vector
       nx
       (FieldElement
          (ArithmeticCircuit
             a
             (Payload
                (IVCResult
                   (FieldElement (ArithmeticCircuit a payload input))
                   (Vector nx)
                   [FieldElement (ArithmeticCircuit a payload input)]
                   (FieldElement (ArithmeticCircuit a payload input))
                   d
                   k)
              :*: U1)
             (Layout
                (IVCResult
                   (FieldElement
                      (ArithmeticCircuit
                         a
                         (Payload
                            (IVCResult
                               (FieldElement (ArithmeticCircuit a payload input))
                               (Vector nx)
                               [FieldElement (ArithmeticCircuit a payload input)]
                               (FieldElement (ArithmeticCircuit a payload input))
                               d
                               k)
                          :*: U1)
                         input))
                   (Vector nx)
                   [FieldElement
                      (ArithmeticCircuit
                         a
                         (Payload
                            (IVCResult
                               (FieldElement (ArithmeticCircuit a payload input))
                               (Vector nx)
                               [FieldElement (ArithmeticCircuit a payload input)]
                               (FieldElement (ArithmeticCircuit a payload input))
                               d
                               k)
                          :*: U1)
                         input)]
                   (FieldElement
                      (ArithmeticCircuit
                         a
                         (Payload
                            (IVCResult
                               (FieldElement (ArithmeticCircuit a payload input))
                               (Vector nx)
                               [FieldElement (ArithmeticCircuit a payload input)]
                               (FieldElement (ArithmeticCircuit a payload input))
                               d
                               k)
                          :*: U1)
                         input))
                   d
                   k)
              :*: U1))),
     Vector
       (k - 1)
       (FieldElement
          (ArithmeticCircuit
             a
             (Payload
                (IVCResult
                   (FieldElement (ArithmeticCircuit a payload input))
                   (Vector nx)
                   [FieldElement (ArithmeticCircuit a payload input)]
                   (FieldElement (ArithmeticCircuit a payload input))
                   d
                   k)
              :*: U1)
             (Layout
                (IVCResult
                   (FieldElement
                      (ArithmeticCircuit
                         a
                         (Payload
                            (IVCResult
                               (FieldElement (ArithmeticCircuit a payload input))
                               (Vector nx)
                               [FieldElement (ArithmeticCircuit a payload input)]
                               (FieldElement (ArithmeticCircuit a payload input))
                               d
                               k)
                          :*: U1)
                         input))
                   (Vector nx)
                   [FieldElement
                      (ArithmeticCircuit
                         a
                         (Payload
                            (IVCResult
                               (FieldElement (ArithmeticCircuit a payload input))
                               (Vector nx)
                               [FieldElement (ArithmeticCircuit a payload input)]
                               (FieldElement (ArithmeticCircuit a payload input))
                               d
                               k)
                          :*: U1)
                         input)]
                   (FieldElement
                      (ArithmeticCircuit
                         a
                         (Payload
                            (IVCResult
                               (FieldElement (ArithmeticCircuit a payload input))
                               (Vector nx)
                               [FieldElement (ArithmeticCircuit a payload input)]
                               (FieldElement (ArithmeticCircuit a payload input))
                               d
                               k)
                          :*: U1)
                         input))
                   d
                   k)
              :*: U1))),
     Vector
       k
       (FieldElement
          (ArithmeticCircuit
             a
             (Payload
                (IVCResult
                   (FieldElement (ArithmeticCircuit a payload input))
                   (Vector nx)
                   [FieldElement (ArithmeticCircuit a payload input)]
                   (FieldElement (ArithmeticCircuit a payload input))
                   d
                   k)
              :*: U1)
             (Layout
                (IVCResult
                   (FieldElement
                      (ArithmeticCircuit
                         a
                         (Payload
                            (IVCResult
                               (FieldElement (ArithmeticCircuit a payload input))
                               (Vector nx)
                               [FieldElement (ArithmeticCircuit a payload input)]
                               (FieldElement (ArithmeticCircuit a payload input))
                               d
                               k)
                          :*: U1)
                         input))
                   (Vector nx)
                   [FieldElement
                      (ArithmeticCircuit
                         a
                         (Payload
                            (IVCResult
                               (FieldElement (ArithmeticCircuit a payload input))
                               (Vector nx)
                               [FieldElement (ArithmeticCircuit a payload input)]
                               (FieldElement (ArithmeticCircuit a payload input))
                               d
                               k)
                          :*: U1)
                         input)]
                   (FieldElement
                      (ArithmeticCircuit
                         a
                         (Payload
                            (IVCResult
                               (FieldElement (ArithmeticCircuit a payload input))
                               (Vector nx)
                               [FieldElement (ArithmeticCircuit a payload input)]
                               (FieldElement (ArithmeticCircuit a payload input))
                               d
                               k)
                          :*: U1)
                         input))
                   d
                   k)
              :*: U1))),
     FieldElement
       (ArithmeticCircuit
          a
          (Payload
             (IVCResult
                (FieldElement (ArithmeticCircuit a payload input))
                (Vector nx)
                [FieldElement (ArithmeticCircuit a payload input)]
                (FieldElement (ArithmeticCircuit a payload input))
                d
                k)
           :*: U1)
          (Layout
             (IVCResult
                (FieldElement
                   (ArithmeticCircuit
                      a
                      (Payload
                         (IVCResult
                            (FieldElement (ArithmeticCircuit a payload input))
                            (Vector nx)
                            [FieldElement (ArithmeticCircuit a payload input)]
                            (FieldElement (ArithmeticCircuit a payload input))
                            d
                            k)
                       :*: U1)
                      input))
                (Vector nx)
                [FieldElement
                   (ArithmeticCircuit
                      a
                      (Payload
                         (IVCResult
                            (FieldElement (ArithmeticCircuit a payload input))
                            (Vector nx)
                            [FieldElement (ArithmeticCircuit a payload input)]
                            (FieldElement (ArithmeticCircuit a payload input))
                            d
                            k)
                       :*: U1)
                      input)]
                (FieldElement
                   (ArithmeticCircuit
                      a
                      (Payload
                         (IVCResult
                            (FieldElement (ArithmeticCircuit a payload input))
                            (Vector nx)
                            [FieldElement (ArithmeticCircuit a payload input)]
                            (FieldElement (ArithmeticCircuit a payload input))
                            d
                            k)
                       :*: U1)
                      input))
                d
                k)
           :*: U1))),
    (Vector
       k
       (FieldElement
          (ArithmeticCircuit
             a
             (Payload
                (IVCResult
                   (FieldElement (ArithmeticCircuit a payload input))
                   (Vector nx)
                   [FieldElement (ArithmeticCircuit a payload input)]
                   (FieldElement (ArithmeticCircuit a payload input))
                   d
                   k)
              :*: U1)
             (Layout
                (IVCResult
                   (FieldElement
                      (ArithmeticCircuit
                         a
                         (Payload
                            (IVCResult
                               (FieldElement (ArithmeticCircuit a payload input))
                               (Vector nx)
                               [FieldElement (ArithmeticCircuit a payload input)]
                               (FieldElement (ArithmeticCircuit a payload input))
                               d
                               k)
                          :*: U1)
                         input))
                   (Vector nx)
                   [FieldElement
                      (ArithmeticCircuit
                         a
                         (Payload
                            (IVCResult
                               (FieldElement (ArithmeticCircuit a payload input))
                               (Vector nx)
                               [FieldElement (ArithmeticCircuit a payload input)]
                               (FieldElement (ArithmeticCircuit a payload input))
                               d
                               k)
                          :*: U1)
                         input)]
                   (FieldElement
                      (ArithmeticCircuit
                         a
                         (Payload
                            (IVCResult
                               (FieldElement (ArithmeticCircuit a payload input))
                               (Vector nx)
                               [FieldElement (ArithmeticCircuit a payload input)]
                               (FieldElement (ArithmeticCircuit a payload input))
                               d
                               k)
                          :*: U1)
                         input))
                   d
                   k)
              :*: U1))),
     FieldElement
       (ArithmeticCircuit
          a
          (Payload
             (IVCResult
                (FieldElement (ArithmeticCircuit a payload input))
                (Vector nx)
                [FieldElement (ArithmeticCircuit a payload input)]
                (FieldElement (ArithmeticCircuit a payload input))
                d
                k)
           :*: U1)
          (Layout
             (IVCResult
                (FieldElement
                   (ArithmeticCircuit
                      a
                      (Payload
                         (IVCResult
                            (FieldElement (ArithmeticCircuit a payload input))
                            (Vector nx)
                            [FieldElement (ArithmeticCircuit a payload input)]
                            (FieldElement (ArithmeticCircuit a payload input))
                            d
                            k)
                       :*: U1)
                      input))
                (Vector nx)
                [FieldElement
                   (ArithmeticCircuit
                      a
                      (Payload
                         (IVCResult
                            (FieldElement (ArithmeticCircuit a payload input))
                            (Vector nx)
                            [FieldElement (ArithmeticCircuit a payload input)]
                            (FieldElement (ArithmeticCircuit a payload input))
                            d
                            k)
                       :*: U1)
                      input)]
                (FieldElement
                   (ArithmeticCircuit
                      a
                      (Payload
                         (IVCResult
                            (FieldElement (ArithmeticCircuit a payload input))
                            (Vector nx)
                            [FieldElement (ArithmeticCircuit a payload input)]
                            (FieldElement (ArithmeticCircuit a payload input))
                            d
                            k)
                       :*: U1)
                      input))
                d
                k)
           :*: U1))))
vf
    in ArithmeticCircuit a payload input output
circuit