{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DeriveAnyClass      #-}
{-# LANGUAGE TemplateHaskell     #-}
{-# LANGUAGE TypeOperators       #-}

{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

{-# HLINT ignore "Redundant ^." #-}

module ZkFold.Base.Protocol.IVC.Internal where

import           Control.DeepSeq                            (NFData)
import           Control.Lens                               ((^.))
import           Control.Lens.Combinators                   (makeLenses)
import           Data.Functor.Rep                           (Representable (..))
import           Data.Type.Equality                         (type (~))
import           Data.Zip                                   (Zip (..), unzip)
import           GHC.Generics                               (Generic, U1, (:*:))
import           Prelude                                    (Show, const, ($))

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Algebra.Basic.Number           (KnownNat, type (+))
import           ZkFold.Base.Algebra.Polynomials.Univariate (PolyVec)
import           ZkFold.Base.Data.Vector                    (Vector, singleton)
import           ZkFold.Base.Protocol.IVC.Accumulator       hiding (pi)
import qualified ZkFold.Base.Protocol.IVC.AccumulatorScheme as Acc
import           ZkFold.Base.Protocol.IVC.AccumulatorScheme (AccumulatorScheme, accumulatorScheme)
import           ZkFold.Base.Protocol.IVC.Commit            (HomomorphicCommit)
import           ZkFold.Base.Protocol.IVC.CommitOpen
import           ZkFold.Base.Protocol.IVC.FiatShamir
import           ZkFold.Base.Protocol.IVC.NARK              (NARKInstanceProof (..), NARKProof (..))
import           ZkFold.Base.Protocol.IVC.Oracle
import           ZkFold.Base.Protocol.IVC.Predicate         (Predicate (..), predicate)
import           ZkFold.Base.Protocol.IVC.RecursiveFunction
import           ZkFold.Base.Protocol.IVC.SpecialSound      (SpecialSoundProtocol (..), specialSoundProtocol,
                                                             specialSoundProtocol')
import           ZkFold.Base.Protocol.IVC.StepFunction      (StepFunction)
import           ZkFold.Symbolic.Compiler                   (ArithmeticCircuit)
import           ZkFold.Symbolic.Data.FieldElement          (FieldElement)
import           ZkFold.Symbolic.Interpreter                (Interpreter)

-- | The recursion circuit satisfiability proof.
data IVCProof k c f
    = IVCProof
    { forall (k :: Natural) (c :: Type -> Type) f.
IVCProof k c f -> Vector k (c f)
_proofX :: Vector k (c f)
    -- ^ The commitment to the witness of the recursion circuit satisfiability proof.
    , forall (k :: Natural) (c :: Type -> Type) f.
IVCProof k c f -> Vector k [f]
_proofW :: Vector k [f]
    -- ^ The witness of the recursion circuit satisfiability proof.
    } deriving ((forall x. IVCProof k c f -> Rep (IVCProof k c f) x)
-> (forall x. Rep (IVCProof k c f) x -> IVCProof k c f)
-> Generic (IVCProof k c f)
forall (k :: Natural) (c :: Type -> Type) f x.
Rep (IVCProof k c f) x -> IVCProof k c f
forall (k :: Natural) (c :: Type -> Type) f x.
IVCProof k c f -> Rep (IVCProof k c f) x
forall x. Rep (IVCProof k c f) x -> IVCProof k c f
forall x. IVCProof k c f -> Rep (IVCProof k c f) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall (k :: Natural) (c :: Type -> Type) f x.
IVCProof k c f -> Rep (IVCProof k c f) x
from :: forall x. IVCProof k c f -> Rep (IVCProof k c f) x
$cto :: forall (k :: Natural) (c :: Type -> Type) f x.
Rep (IVCProof k c f) x -> IVCProof k c f
to :: forall x. Rep (IVCProof k c f) x -> IVCProof k c f
GHC.Generics.Generic, Int -> IVCProof k c f -> ShowS
[IVCProof k c f] -> ShowS
IVCProof k c f -> String
(Int -> IVCProof k c f -> ShowS)
-> (IVCProof k c f -> String)
-> ([IVCProof k c f] -> ShowS)
-> Show (IVCProof k c f)
forall (k :: Natural) (c :: Type -> Type) f.
(Show f, Show (c f)) =>
Int -> IVCProof k c f -> ShowS
forall (k :: Natural) (c :: Type -> Type) f.
(Show f, Show (c f)) =>
[IVCProof k c f] -> ShowS
forall (k :: Natural) (c :: Type -> Type) f.
(Show f, Show (c f)) =>
IVCProof k c f -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall (k :: Natural) (c :: Type -> Type) f.
(Show f, Show (c f)) =>
Int -> IVCProof k c f -> ShowS
showsPrec :: Int -> IVCProof k c f -> ShowS
$cshow :: forall (k :: Natural) (c :: Type -> Type) f.
(Show f, Show (c f)) =>
IVCProof k c f -> String
show :: IVCProof k c f -> String
$cshowList :: forall (k :: Natural) (c :: Type -> Type) f.
(Show f, Show (c f)) =>
[IVCProof k c f] -> ShowS
showList :: [IVCProof k c f] -> ShowS
Show, IVCProof k c f -> ()
(IVCProof k c f -> ()) -> NFData (IVCProof k c f)
forall (k :: Natural) (c :: Type -> Type) f.
(NFData f, NFData (c f)) =>
IVCProof k c f -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall (k :: Natural) (c :: Type -> Type) f.
(NFData f, NFData (c f)) =>
IVCProof k c f -> ()
rnf :: IVCProof k c f -> ()
NFData)

makeLenses ''IVCProof

noIVCProof :: forall k c f .
    ( KnownNat k
    , AdditiveMonoid (c f)
    , AdditiveMonoid f
    ) => IVCProof k c f
noIVCProof :: forall (k :: Natural) (c :: Type -> Type) f.
(KnownNat k, AdditiveMonoid (c f), AdditiveMonoid f) =>
IVCProof k c f
noIVCProof = Vector k (c f) -> Vector k [f] -> IVCProof k c f
forall (k :: Natural) (c :: Type -> Type) f.
Vector k (c f) -> Vector k [f] -> IVCProof k c f
IVCProof ((Rep (Vector k) -> c f) -> Vector k (c f)
forall a. (Rep (Vector k) -> a) -> Vector k a
forall (f :: Type -> Type) a.
Representable f =>
(Rep f -> a) -> f a
tabulate ((Rep (Vector k) -> c f) -> Vector k (c f))
-> (Rep (Vector k) -> c f) -> Vector k (c f)
forall a b. (a -> b) -> a -> b
$ c f -> Zp k -> c f
forall a b. a -> b -> a
const c f
forall a. AdditiveMonoid a => a
zero) ((Rep (Vector k) -> [f]) -> Vector k [f]
forall a. (Rep (Vector k) -> a) -> Vector k a
forall (f :: Type -> Type) a.
Representable f =>
(Rep f -> a) -> f a
tabulate ((Rep (Vector k) -> [f]) -> Vector k [f])
-> (Rep (Vector k) -> [f]) -> Vector k [f]
forall a b. (a -> b) -> a -> b
$ [f] -> Zp k -> [f]
forall a b. a -> b -> a
const [f]
forall a. AdditiveMonoid a => a
zero)

-- | The current result of recursion together with the first iteration flag,
-- the corresponding accumulator, and the recursion circuit satisfiability proof.
data IVCResult k i c f
    = IVCResult
    { forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
IVCResult k i c f -> i f
_z     :: i f
    , forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
IVCResult k i c f -> Accumulator k (RecursiveI i) c f
_acc   :: Accumulator k (RecursiveI i) c f
    , forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
IVCResult k i c f -> IVCProof k c f
_proof :: IVCProof k c f
    } deriving ((forall x. IVCResult k i c f -> Rep (IVCResult k i c f) x)
-> (forall x. Rep (IVCResult k i c f) x -> IVCResult k i c f)
-> Generic (IVCResult k i c f)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f x.
Rep (IVCResult k i c f) x -> IVCResult k i c f
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f x.
IVCResult k i c f -> Rep (IVCResult k i c f) x
forall x. Rep (IVCResult k i c f) x -> IVCResult k i c f
forall x. IVCResult k i c f -> Rep (IVCResult k i c f) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f x.
IVCResult k i c f -> Rep (IVCResult k i c f) x
from :: forall x. IVCResult k i c f -> Rep (IVCResult k i c f) x
$cto :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f x.
Rep (IVCResult k i c f) x -> IVCResult k i c f
to :: forall x. Rep (IVCResult k i c f) x -> IVCResult k i c f
GHC.Generics.Generic, Int -> IVCResult k i c f -> ShowS
[IVCResult k i c f] -> ShowS
IVCResult k i c f -> String
(Int -> IVCResult k i c f -> ShowS)
-> (IVCResult k i c f -> String)
-> ([IVCResult k i c f] -> ShowS)
-> Show (IVCResult k i c f)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
(Show f, Show (i f), Show (c f)) =>
Int -> IVCResult k i c f -> ShowS
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
(Show f, Show (i f), Show (c f)) =>
[IVCResult k i c f] -> ShowS
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
(Show f, Show (i f), Show (c f)) =>
IVCResult k i c f -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
(Show f, Show (i f), Show (c f)) =>
Int -> IVCResult k i c f -> ShowS
showsPrec :: Int -> IVCResult k i c f -> ShowS
$cshow :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
(Show f, Show (i f), Show (c f)) =>
IVCResult k i c f -> String
show :: IVCResult k i c f -> String
$cshowList :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
(Show f, Show (i f), Show (c f)) =>
[IVCResult k i c f] -> ShowS
showList :: [IVCResult k i c f] -> ShowS
Show, IVCResult k i c f -> ()
(IVCResult k i c f -> ()) -> NFData (IVCResult k i c f)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
(NFData f, NFData (i f), NFData (c f)) =>
IVCResult k i c f -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
(NFData f, NFData (i f), NFData (c f)) =>
IVCResult k i c f -> ()
rnf :: IVCResult k i c f -> ()
NFData)

makeLenses ''IVCResult

type IVCAssumptions ctx0 ctx1 algo d k a i p c f =
    ( RecursivePredicateAssumptions algo d k a i p c
    , KnownNat (d+1)
    , k ~ 1
    , Zip i
    , Field f
    , HashAlgorithm algo f
    , RandomOracle algo f f
    , RandomOracle algo (i f) f
    , RandomOracle algo (c f) f
    , HomomorphicCommit [f] (c f)
    , Scale a f
    , Scale a (PolyVec f (d+1))
    , Scale f (c f)
    , ctx0 ~ Interpreter a
    , RecursiveFunctionAssumptions algo d a i c (FieldElement ctx0) ctx0
    , ctx1 ~ ArithmeticCircuit a (RecursiveI i :*: RecursiveP d k i p c) U1
    , RecursiveFunctionAssumptions algo d a i c (FieldElement ctx1) ctx1
    )

-- | Create the first IVC result
--
-- It differs from the rest of the iterations as we don't have anything accumulated just yet.
ivcSetup :: forall ctx0 ctx1 algo d k a i p c . IVCAssumptions ctx0 ctx1 algo d k a i p c a
    => StepFunction a i p
    -> i a
    -> p a
    -> IVCResult k i c a
ivcSetup :: forall {k} (ctx0 :: (Type -> Type) -> Type)
       (ctx1 :: (Type -> Type) -> Type) (algo :: k) (d :: Natural)
       (k :: Natural) a (i :: Type -> Type) (p :: Type -> Type)
       (c :: Type -> Type).
IVCAssumptions ctx0 ctx1 algo d k a i p c a =>
StepFunction a i p -> i a -> p a -> IVCResult k i c a
ivcSetup StepFunction a i p
f i a
z0 p a
witness =
    let
        p :: Predicate a i p
        p :: Predicate a i p
p = StepFunction a i p -> Predicate a i p
forall a (i :: Type -> Type) (p :: Type -> Type).
PredicateAssumptions a i p =>
StepFunction a i p -> Predicate a i p
predicate i f -> p f -> i f
StepFunction a i p
f

        z1 :: i a
        z1 :: i a
z1 = Predicate a i p -> i a -> p a -> i a
forall a (i :: Type -> Type) (p :: Type -> Type).
Predicate a i p -> i a -> p a -> i a
predicateEval Predicate a i p
p i a
z0 p a
witness

        pRec :: Predicate a (RecursiveI i) (RecursiveP d k i p c)
        pRec :: Predicate a (RecursiveI i) (RecursiveP d k i p c)
pRec = forall (algo :: k) (d :: Natural) (k2 :: Natural) a
       (i :: Type -> Type) (p :: Type -> Type) (c :: Type -> Type)
       (ctx0 :: (Type -> Type) -> Type) (ctx1 :: (Type -> Type) -> Type).
(RecursivePredicateAssumptions algo d k2 a i p c,
 ctx0 ~ Interpreter a,
 RecursiveFunctionAssumptions algo d a i c (FieldElement ctx0) ctx0,
 ctx1
 ~ ArithmeticCircuit a (RecursiveI i :*: RecursiveP d k2 i p c) U1,
 RecursiveFunctionAssumptions
   algo d a i c (FieldElement ctx1) ctx1) =>
RecursiveFunction algo d k2 a i p c
-> Predicate a (RecursiveI i) (RecursiveP d k2 i p c)
forall {k1} (algo :: k1) (d :: Natural) (k2 :: Natural) a
       (i :: Type -> Type) (p :: Type -> Type) (c :: Type -> Type)
       (ctx0 :: (Type -> Type) -> Type) (ctx1 :: (Type -> Type) -> Type).
(RecursivePredicateAssumptions algo d k2 a i p c,
 ctx0 ~ Interpreter a,
 RecursiveFunctionAssumptions algo d a i c (FieldElement ctx0) ctx0,
 ctx1
 ~ ArithmeticCircuit a (RecursiveI i :*: RecursiveP d k2 i p c) U1,
 RecursiveFunctionAssumptions
   algo d a i c (FieldElement ctx1) ctx1) =>
RecursiveFunction algo d k2 a i p c
-> Predicate a (RecursiveI i) (RecursiveP d k2 i p c)
recursivePredicate @algo (RecursiveFunction algo d k a i p c
 -> Predicate a (RecursiveI i) (RecursiveP d k i p c))
-> RecursiveFunction algo d k a i p c
-> Predicate a (RecursiveI i) (RecursiveP d k i p c)
forall a b. (a -> b) -> a -> b
$ forall (algo :: k) (d :: Natural) (k2 :: Natural) a
       (i :: Type -> Type) (p :: Type -> Type) (c :: Type -> Type).
(PredicateAssumptions a i p, FunctorAssumptions c,
 KnownNat (d - 1), KnownNat (d + 1), KnownNat (k2 - 1), KnownNat k2,
 Zip i) =>
StepFunction a i p -> RecursiveFunction algo d k2 a i p c
forall {k1} (algo :: k1) (d :: Natural) (k2 :: Natural) a
       (i :: Type -> Type) (p :: Type -> Type) (c :: Type -> Type).
(PredicateAssumptions a i p, FunctorAssumptions c,
 KnownNat (d - 1), KnownNat (d + 1), KnownNat (k2 - 1), KnownNat k2,
 Zip i) =>
StepFunction a i p -> RecursiveFunction algo d k2 a i p c
recursiveFunction @algo i f -> p f -> i f
StepFunction a i p
StepFunction (BaseField ctx) i p
f
    in
        i a
-> Accumulator k (RecursiveI i) c a
-> IVCProof k c a
-> IVCResult k i c a
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
i f
-> Accumulator k (RecursiveI i) c f
-> IVCProof k c f
-> IVCResult k i c f
IVCResult i a
z1 (forall (d :: Natural) (k :: Natural) a (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) f.
(KnownNat (d + 1), KnownNat (k - 1), KnownNat k, Representable i,
 HomomorphicCommit [f] (c f), Ring f, Scale a f) =>
Predicate a i p -> Accumulator k i c f
emptyAccumulator @d Predicate a (RecursiveI i) (RecursiveP d k i p c)
pRec) IVCProof k c a
forall (k :: Natural) (c :: Type -> Type) f.
(KnownNat k, AdditiveMonoid (c f), AdditiveMonoid f) =>
IVCProof k c f
noIVCProof

ivcProve :: forall ctx0 ctx1 algo d k a i p c . IVCAssumptions ctx0 ctx1 algo d k a i p c a
    => StepFunction a i p
    -> IVCResult k i c a
    -> p a
    -> IVCResult k i c a
ivcProve :: forall {k} (ctx0 :: (Type -> Type) -> Type)
       (ctx1 :: (Type -> Type) -> Type) (algo :: k) (d :: Natural)
       (k :: Natural) a (i :: Type -> Type) (p :: Type -> Type)
       (c :: Type -> Type).
IVCAssumptions ctx0 ctx1 algo d k a i p c a =>
StepFunction a i p -> IVCResult k i c a -> p a -> IVCResult k i c a
ivcProve StepFunction a i p
f IVCResult k i c a
res p a
witness =
    let
        p :: Predicate a i p
        p :: Predicate a i p
p = StepFunction a i p -> Predicate a i p
forall a (i :: Type -> Type) (p :: Type -> Type).
PredicateAssumptions a i p =>
StepFunction a i p -> Predicate a i p
predicate i f -> p f -> i f
StepFunction a i p
f

        z' :: i a
        z' :: i a
z' = Predicate a i p -> i a -> p a -> i a
forall a (i :: Type -> Type) (p :: Type -> Type).
Predicate a i p -> i a -> p a -> i a
predicateEval Predicate a i p
p (IVCResult k i c a
resIVCResult k i c a -> Getting (i a) (IVCResult k i c a) (i a) -> i a
forall s a. s -> Getting a s a -> a
^.Getting (i a) (IVCResult k i c a) (i a)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f
       (f :: Type -> Type).
Functor f =>
(i f -> f (i f)) -> IVCResult k i c f -> f (IVCResult k i c f)
z) p a
witness

        pRec :: Predicate a (RecursiveI i) (RecursiveP d k i p c)
        pRec :: Predicate a (RecursiveI i) (RecursiveP d k i p c)
pRec = forall (algo :: k) (d :: Natural) (k2 :: Natural) a
       (i :: Type -> Type) (p :: Type -> Type) (c :: Type -> Type)
       (ctx0 :: (Type -> Type) -> Type) (ctx1 :: (Type -> Type) -> Type).
(RecursivePredicateAssumptions algo d k2 a i p c,
 ctx0 ~ Interpreter a,
 RecursiveFunctionAssumptions algo d a i c (FieldElement ctx0) ctx0,
 ctx1
 ~ ArithmeticCircuit a (RecursiveI i :*: RecursiveP d k2 i p c) U1,
 RecursiveFunctionAssumptions
   algo d a i c (FieldElement ctx1) ctx1) =>
RecursiveFunction algo d k2 a i p c
-> Predicate a (RecursiveI i) (RecursiveP d k2 i p c)
forall {k1} (algo :: k1) (d :: Natural) (k2 :: Natural) a
       (i :: Type -> Type) (p :: Type -> Type) (c :: Type -> Type)
       (ctx0 :: (Type -> Type) -> Type) (ctx1 :: (Type -> Type) -> Type).
(RecursivePredicateAssumptions algo d k2 a i p c,
 ctx0 ~ Interpreter a,
 RecursiveFunctionAssumptions algo d a i c (FieldElement ctx0) ctx0,
 ctx1
 ~ ArithmeticCircuit a (RecursiveI i :*: RecursiveP d k2 i p c) U1,
 RecursiveFunctionAssumptions
   algo d a i c (FieldElement ctx1) ctx1) =>
RecursiveFunction algo d k2 a i p c
-> Predicate a (RecursiveI i) (RecursiveP d k2 i p c)
recursivePredicate @algo (RecursiveFunction algo d k a i p c
 -> Predicate a (RecursiveI i) (RecursiveP d k i p c))
-> RecursiveFunction algo d k a i p c
-> Predicate a (RecursiveI i) (RecursiveP d k i p c)
forall a b. (a -> b) -> a -> b
$ forall (algo :: k) (d :: Natural) (k2 :: Natural) a
       (i :: Type -> Type) (p :: Type -> Type) (c :: Type -> Type).
(PredicateAssumptions a i p, FunctorAssumptions c,
 KnownNat (d - 1), KnownNat (d + 1), KnownNat (k2 - 1), KnownNat k2,
 Zip i) =>
StepFunction a i p -> RecursiveFunction algo d k2 a i p c
forall {k1} (algo :: k1) (d :: Natural) (k2 :: Natural) a
       (i :: Type -> Type) (p :: Type -> Type) (c :: Type -> Type).
(PredicateAssumptions a i p, FunctorAssumptions c,
 KnownNat (d - 1), KnownNat (d + 1), KnownNat (k2 - 1), KnownNat k2,
 Zip i) =>
StepFunction a i p -> RecursiveFunction algo d k2 a i p c
recursiveFunction @algo i f -> p f -> i f
StepFunction a i p
StepFunction (BaseField ctx) i p
f

        input :: RecursiveI i a
        input :: RecursiveI i a
input = i a -> a -> RecursiveI i a
forall (i :: Type -> Type) f. i f -> f -> RecursiveI i f
RecursiveI (IVCResult k i c a
resIVCResult k i c a -> Getting (i a) (IVCResult k i c a) (i a) -> i a
forall s a. s -> Getting a s a -> a
^.Getting (i a) (IVCResult k i c a) (i a)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f
       (f :: Type -> Type).
Functor f =>
(i f -> f (i f)) -> IVCResult k i c f -> f (IVCResult k i c f)
z) (forall (algo :: k) x a. RandomOracle algo x a => x -> a
forall {k} (algo :: k) x a. RandomOracle algo x a => x -> a
oracle @algo (AccumulatorInstance k (RecursiveI i) c a -> a)
-> AccumulatorInstance k (RecursiveI i) c a -> a
forall a b. (a -> b) -> a -> b
$ IVCResult k i c a
resIVCResult k i c a
-> Getting
     (Accumulator k (RecursiveI i) c a)
     (IVCResult k i c a)
     (Accumulator k (RecursiveI i) c a)
-> Accumulator k (RecursiveI i) c a
forall s a. s -> Getting a s a -> a
^.Getting
  (Accumulator k (RecursiveI i) c a)
  (IVCResult k i c a)
  (Accumulator k (RecursiveI i) c a)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f
       (f :: Type -> Type).
Functor f =>
(Accumulator k (RecursiveI i) c f
 -> f (Accumulator k (RecursiveI i) c f))
-> IVCResult k i c f -> f (IVCResult k i c f)
accAccumulator k (RecursiveI i) c a
-> Getting
     (AccumulatorInstance k (RecursiveI i) c a)
     (Accumulator k (RecursiveI i) c a)
     (AccumulatorInstance k (RecursiveI i) c a)
-> AccumulatorInstance k (RecursiveI i) c a
forall s a. s -> Getting a s a -> a
^.Getting
  (AccumulatorInstance k (RecursiveI i) c a)
  (Accumulator k (RecursiveI i) c a)
  (AccumulatorInstance k (RecursiveI i) c a)
forall (k :: Natural) (i1 :: Type -> Type) (c1 :: Type -> Type) f1
       (i2 :: Type -> Type) (c2 :: Type -> Type) (f2 :: Type -> Type).
Functor f2 =>
(AccumulatorInstance k i1 c1 f1
 -> f2 (AccumulatorInstance k i2 c2 f1))
-> Accumulator k i1 c1 f1 -> f2 (Accumulator k i2 c2 f1)
x)

        messages :: Vector k [a]
        messages :: Vector k [a]
messages = IVCResult k i c a
resIVCResult k i c a
-> Getting (IVCProof k c a) (IVCResult k i c a) (IVCProof k c a)
-> IVCProof k c a
forall s a. s -> Getting a s a -> a
^.Getting (IVCProof k c a) (IVCResult k i c a) (IVCProof k c a)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f
       (f :: Type -> Type).
Functor f =>
(IVCProof k c f -> f (IVCProof k c f))
-> IVCResult k i c f -> f (IVCResult k i c f)
proofIVCProof k c a
-> Getting (Vector k [a]) (IVCProof k c a) (Vector k [a])
-> Vector k [a]
forall s a. s -> Getting a s a -> a
^.Getting (Vector k [a]) (IVCProof k c a) (Vector k [a])
forall (k :: Natural) (c :: Type -> Type) f (f :: Type -> Type).
Functor f =>
(Vector k [f] -> f (Vector k [f]))
-> IVCProof k c f -> f (IVCProof k c f)
proofW

        commits :: Vector k (c a)
        commits :: Vector k (c a)
commits = IVCResult k i c a
resIVCResult k i c a
-> Getting (IVCProof k c a) (IVCResult k i c a) (IVCProof k c a)
-> IVCProof k c a
forall s a. s -> Getting a s a -> a
^.Getting (IVCProof k c a) (IVCResult k i c a) (IVCProof k c a)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f
       (f :: Type -> Type).
Functor f =>
(IVCProof k c f -> f (IVCProof k c f))
-> IVCResult k i c f -> f (IVCResult k i c f)
proofIVCProof k c a
-> Getting (Vector k (c a)) (IVCProof k c a) (Vector k (c a))
-> Vector k (c a)
forall s a. s -> Getting a s a -> a
^.Getting (Vector k (c a)) (IVCProof k c a) (Vector k (c a))
forall (k :: Natural) (c :: Type -> Type) f (c :: Type -> Type)
       (f :: Type -> Type).
Functor f =>
(Vector k (c f) -> f (Vector k (c f)))
-> IVCProof k c f -> f (IVCProof k c f)
proofX

        narkIP :: NARKInstanceProof k (RecursiveI i) c a
        narkIP :: NARKInstanceProof k (RecursiveI i) c a
narkIP = RecursiveI i a
-> NARKProof k c a -> NARKInstanceProof k (RecursiveI i) c a
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
i f -> NARKProof k c f -> NARKInstanceProof k i c f
NARKInstanceProof RecursiveI i a
input (Vector k (c a) -> Vector k [a] -> NARKProof k c a
forall (k :: Natural) (c :: Type -> Type) f.
Vector k (c f) -> Vector k [f] -> NARKProof k c f
NARKProof Vector k (c a)
commits Vector k [a]
messages)

        accScheme :: AccumulatorScheme d k (RecursiveI i) c a
        accScheme :: AccumulatorScheme d k (RecursiveI i) c a
accScheme = forall (algo :: k) (d :: Natural) (k2 :: Natural) a
       (i :: Type -> Type) (p :: Type -> Type) (c :: Type -> Type) f.
(KnownNat (d - 1), KnownNat (d + 1), Representable i, Zip i,
 HashAlgorithm algo f, RandomOracle algo f f,
 RandomOracle algo (i f) f, RandomOracle algo (c f) f,
 HomomorphicCommit [f] (c f), Field f, Scale a f,
 Scale a (PolyVec f (d + 1)), Scale f (c f)) =>
Predicate a i p -> AccumulatorScheme d k2 i c f
forall {k1} (algo :: k1) (d :: Natural) (k2 :: Natural) a
       (i :: Type -> Type) (p :: Type -> Type) (c :: Type -> Type) f.
(KnownNat (d - 1), KnownNat (d + 1), Representable i, Zip i,
 HashAlgorithm algo f, RandomOracle algo f f,
 RandomOracle algo (i f) f, RandomOracle algo (c f) f,
 HomomorphicCommit [f] (c f), Field f, Scale a f,
 Scale a (PolyVec f (d + 1)), Scale f (c f)) =>
Predicate a i p -> AccumulatorScheme d k2 i c f
accumulatorScheme @algo @d Predicate a (RecursiveI i) (RecursiveP d k i p c)
pRec

        (Accumulator k (RecursiveI i) c a
acc', Vector (d - 1) (c a)
pf) = AccumulatorScheme d k (RecursiveI i) c a
-> Accumulator k (RecursiveI i) c a
-> NARKInstanceProof k (RecursiveI i) c a
-> (Accumulator k (RecursiveI i) c a, Vector (d - 1) (c a))
forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (c :: Type -> Type) f.
AccumulatorScheme d k i c f
-> Accumulator k i c f
-> NARKInstanceProof k i c f
-> (Accumulator k i c f, Vector (d - 1) (c f))
Acc.prover AccumulatorScheme d k (RecursiveI i) c a
accScheme (IVCResult k i c a
resIVCResult k i c a
-> Getting
     (Accumulator k (RecursiveI i) c a)
     (IVCResult k i c a)
     (Accumulator k (RecursiveI i) c a)
-> Accumulator k (RecursiveI i) c a
forall s a. s -> Getting a s a -> a
^.Getting
  (Accumulator k (RecursiveI i) c a)
  (IVCResult k i c a)
  (Accumulator k (RecursiveI i) c a)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f
       (f :: Type -> Type).
Functor f =>
(Accumulator k (RecursiveI i) c f
 -> f (Accumulator k (RecursiveI i) c f))
-> IVCResult k i c f -> f (IVCResult k i c f)
acc) NARKInstanceProof k (RecursiveI i) c a
narkIP

        payload :: RecursiveP d k i p c a
        payload :: RecursiveP d k i p c a
payload = p a
-> Vector k (c a)
-> AccumulatorInstance k (RecursiveI i) c a
-> a
-> Vector (d - 1) (c a)
-> RecursiveP d k i p c a
forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) f.
p f
-> Vector k (c f)
-> AccumulatorInstance k (RecursiveI i) c f
-> f
-> Vector (d - 1) (c f)
-> RecursiveP d k i p c f
RecursiveP p a
witness Vector k (c a)
commits (IVCResult k i c a
resIVCResult k i c a
-> Getting
     (Accumulator k (RecursiveI i) c a)
     (IVCResult k i c a)
     (Accumulator k (RecursiveI i) c a)
-> Accumulator k (RecursiveI i) c a
forall s a. s -> Getting a s a -> a
^.Getting
  (Accumulator k (RecursiveI i) c a)
  (IVCResult k i c a)
  (Accumulator k (RecursiveI i) c a)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f
       (f :: Type -> Type).
Functor f =>
(Accumulator k (RecursiveI i) c f
 -> f (Accumulator k (RecursiveI i) c f))
-> IVCResult k i c f -> f (IVCResult k i c f)
accAccumulator k (RecursiveI i) c a
-> Getting
     (AccumulatorInstance k (RecursiveI i) c a)
     (Accumulator k (RecursiveI i) c a)
     (AccumulatorInstance k (RecursiveI i) c a)
-> AccumulatorInstance k (RecursiveI i) c a
forall s a. s -> Getting a s a -> a
^.Getting
  (AccumulatorInstance k (RecursiveI i) c a)
  (Accumulator k (RecursiveI i) c a)
  (AccumulatorInstance k (RecursiveI i) c a)
forall (k :: Natural) (i1 :: Type -> Type) (c1 :: Type -> Type) f1
       (i2 :: Type -> Type) (c2 :: Type -> Type) (f2 :: Type -> Type).
Functor f2 =>
(AccumulatorInstance k i1 c1 f1
 -> f2 (AccumulatorInstance k i2 c2 f1))
-> Accumulator k i1 c1 f1 -> f2 (Accumulator k i2 c2 f1)
x) a
forall a. MultiplicativeMonoid a => a
one Vector (d - 1) (c a)
pf

        protocol :: FiatShamir k (RecursiveI i) (RecursiveP d k i p c) c [a] [a] a
        protocol :: FiatShamir k (RecursiveI i) (RecursiveP d k i p c) c [a] [a] a
protocol = forall (algo :: k) (k2 :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) m o f.
(KnownNat k2, HashAlgorithm algo f, RandomOracle algo f f,
 RandomOracle algo (i f) f, RandomOracle algo (c f) f) =>
CommitOpen k2 i p c m o f -> FiatShamir k2 i p c m o f
forall {k1} (algo :: k1) (k2 :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) m o f.
(KnownNat k2, HashAlgorithm algo f, RandomOracle algo f f,
 RandomOracle algo (i f) f, RandomOracle algo (c f) f) =>
CommitOpen k2 i p c m o f -> FiatShamir k2 i p c m o f
fiatShamir @algo (CommitOpen k (RecursiveI i) (RecursiveP d k i p c) c [a] [a] a
 -> FiatShamir k (RecursiveI i) (RecursiveP d k i p c) c [a] [a] a)
-> CommitOpen k (RecursiveI i) (RecursiveP d k i p c) c [a] [a] a
-> FiatShamir k (RecursiveI i) (RecursiveP d k i p c) c [a] [a] a
forall a b. (a -> b) -> a -> b
$ SpecialSoundProtocol
  k (RecursiveI i) (RecursiveP d k i p c) [a] [a] a
-> CommitOpen k (RecursiveI i) (RecursiveP d k i p c) c [a] [a] a
forall m (c :: Type -> Type) f (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) o.
HomomorphicCommit m (c f) =>
SpecialSoundProtocol k i p m o f -> CommitOpen k i p c m o f
commitOpen (SpecialSoundProtocol
   k (RecursiveI i) (RecursiveP d k i p c) [a] [a] a
 -> CommitOpen k (RecursiveI i) (RecursiveP d k i p c) c [a] [a] a)
-> SpecialSoundProtocol
     k (RecursiveI i) (RecursiveP d k i p c) [a] [a] a
-> CommitOpen k (RecursiveI i) (RecursiveP d k i p c) c [a] [a] a
forall a b. (a -> b) -> a -> b
$ forall (d :: Natural) a (i :: Type -> Type) (p :: Type -> Type).
(KnownNat (d + 1), Arithmetic a, Representable i,
 Representable p) =>
Predicate a i p -> SpecialSoundProtocol 1 i p [a] [a] a
specialSoundProtocol @d Predicate a (RecursiveI i) (RecursiveP d k i p c)
pRec

        (Vector k [a]
messages', Vector k (c a)
commits') = Vector k ([a], c a) -> (Vector k [a], Vector k (c a))
forall a b. Vector k (a, b) -> (Vector k a, Vector k b)
forall (f :: Type -> Type) a b. Unzip f => f (a, b) -> (f a, f b)
unzip (Vector k ([a], c a) -> (Vector k [a], Vector k (c a)))
-> Vector k ([a], c a) -> (Vector k [a], Vector k (c a))
forall a b. (a -> b) -> a -> b
$ FiatShamir k (RecursiveI i) (RecursiveP d k i p c) c [a] [a] a
-> RecursiveI i a
-> RecursiveP d k i p c a
-> a
-> Natural
-> Vector k ([a], c a)
forall (k :: Natural) (i :: Type -> Type) (p :: Type -> Type) m o
       f.
SpecialSoundProtocol k i p m o f -> i f -> p f -> f -> Natural -> m
prover FiatShamir k (RecursiveI i) (RecursiveP d k i p c) c [a] [a] a
protocol RecursiveI i a
input RecursiveP d k i p c a
payload a
forall a. AdditiveMonoid a => a
zero Natural
0

        ivcProof :: IVCProof k c a
        ivcProof :: IVCProof k c a
ivcProof = Vector k (c a) -> Vector k [a] -> IVCProof k c a
forall (k :: Natural) (c :: Type -> Type) f.
Vector k (c f) -> Vector k [f] -> IVCProof k c f
IVCProof Vector k (c a)
commits' Vector k [a]
messages'
    in
        i a
-> Accumulator k (RecursiveI i) c a
-> IVCProof k c a
-> IVCResult k i c a
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
i f
-> Accumulator k (RecursiveI i) c f
-> IVCProof k c f
-> IVCResult k i c f
IVCResult i a
z' Accumulator k (RecursiveI i) c a
acc' IVCProof k c a
ivcProof

ivcVerify :: forall ctx0 ctx1 algo d k a i p c f . IVCAssumptions ctx0 ctx1 algo d k a i p c f
    => StepFunction a i p
    -> IVCResult k i c f
    -> ((Vector k (c f), [f]), (Vector k (c f), c f))
ivcVerify :: forall {k} (ctx0 :: (Type -> Type) -> Type)
       (ctx1 :: (Type -> Type) -> Type) (algo :: k) (d :: Natural)
       (k :: Natural) a (i :: Type -> Type) (p :: Type -> Type)
       (c :: Type -> Type) f.
IVCAssumptions ctx0 ctx1 algo d k a i p c f =>
StepFunction a i p
-> IVCResult k i c f
-> ((Vector k (c f), [f]), (Vector k (c f), c f))
ivcVerify StepFunction a i p
f IVCResult k i c f
res =
    let
        pRec :: Predicate a (RecursiveI i) (RecursiveP d k i p c)
        pRec :: Predicate a (RecursiveI i) (RecursiveP d k i p c)
pRec = forall (algo :: k) (d :: Natural) (k2 :: Natural) a
       (i :: Type -> Type) (p :: Type -> Type) (c :: Type -> Type)
       (ctx0 :: (Type -> Type) -> Type) (ctx1 :: (Type -> Type) -> Type).
(RecursivePredicateAssumptions algo d k2 a i p c,
 ctx0 ~ Interpreter a,
 RecursiveFunctionAssumptions algo d a i c (FieldElement ctx0) ctx0,
 ctx1
 ~ ArithmeticCircuit a (RecursiveI i :*: RecursiveP d k2 i p c) U1,
 RecursiveFunctionAssumptions
   algo d a i c (FieldElement ctx1) ctx1) =>
RecursiveFunction algo d k2 a i p c
-> Predicate a (RecursiveI i) (RecursiveP d k2 i p c)
forall {k1} (algo :: k1) (d :: Natural) (k2 :: Natural) a
       (i :: Type -> Type) (p :: Type -> Type) (c :: Type -> Type)
       (ctx0 :: (Type -> Type) -> Type) (ctx1 :: (Type -> Type) -> Type).
(RecursivePredicateAssumptions algo d k2 a i p c,
 ctx0 ~ Interpreter a,
 RecursiveFunctionAssumptions algo d a i c (FieldElement ctx0) ctx0,
 ctx1
 ~ ArithmeticCircuit a (RecursiveI i :*: RecursiveP d k2 i p c) U1,
 RecursiveFunctionAssumptions
   algo d a i c (FieldElement ctx1) ctx1) =>
RecursiveFunction algo d k2 a i p c
-> Predicate a (RecursiveI i) (RecursiveP d k2 i p c)
recursivePredicate @algo (RecursiveFunction algo d k a i p c
 -> Predicate a (RecursiveI i) (RecursiveP d k i p c))
-> RecursiveFunction algo d k a i p c
-> Predicate a (RecursiveI i) (RecursiveP d k i p c)
forall a b. (a -> b) -> a -> b
$ forall (algo :: k) (d :: Natural) (k2 :: Natural) a
       (i :: Type -> Type) (p :: Type -> Type) (c :: Type -> Type).
(PredicateAssumptions a i p, FunctorAssumptions c,
 KnownNat (d - 1), KnownNat (d + 1), KnownNat (k2 - 1), KnownNat k2,
 Zip i) =>
StepFunction a i p -> RecursiveFunction algo d k2 a i p c
forall {k1} (algo :: k1) (d :: Natural) (k2 :: Natural) a
       (i :: Type -> Type) (p :: Type -> Type) (c :: Type -> Type).
(PredicateAssumptions a i p, FunctorAssumptions c,
 KnownNat (d - 1), KnownNat (d + 1), KnownNat (k2 - 1), KnownNat k2,
 Zip i) =>
StepFunction a i p -> RecursiveFunction algo d k2 a i p c
recursiveFunction @algo i f -> p f -> i f
StepFunction a i p
StepFunction (BaseField ctx) i p
f

        input :: RecursiveI i f
        input :: RecursiveI i f
input = i f -> f -> RecursiveI i f
forall (i :: Type -> Type) f. i f -> f -> RecursiveI i f
RecursiveI (IVCResult k i c f
resIVCResult k i c f -> Getting (i f) (IVCResult k i c f) (i f) -> i f
forall s a. s -> Getting a s a -> a
^.Getting (i f) (IVCResult k i c f) (i f)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f
       (f :: Type -> Type).
Functor f =>
(i f -> f (i f)) -> IVCResult k i c f -> f (IVCResult k i c f)
z) (forall (algo :: k) x a. RandomOracle algo x a => x -> a
forall {k} (algo :: k) x a. RandomOracle algo x a => x -> a
oracle @algo (AccumulatorInstance k (RecursiveI i) c f -> f)
-> AccumulatorInstance k (RecursiveI i) c f -> f
forall a b. (a -> b) -> a -> b
$ IVCResult k i c f
resIVCResult k i c f
-> Getting
     (Accumulator k (RecursiveI i) c f)
     (IVCResult k i c f)
     (Accumulator k (RecursiveI i) c f)
-> Accumulator k (RecursiveI i) c f
forall s a. s -> Getting a s a -> a
^.Getting
  (Accumulator k (RecursiveI i) c f)
  (IVCResult k i c f)
  (Accumulator k (RecursiveI i) c f)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f
       (f :: Type -> Type).
Functor f =>
(Accumulator k (RecursiveI i) c f
 -> f (Accumulator k (RecursiveI i) c f))
-> IVCResult k i c f -> f (IVCResult k i c f)
accAccumulator k (RecursiveI i) c f
-> Getting
     (AccumulatorInstance k (RecursiveI i) c f)
     (Accumulator k (RecursiveI i) c f)
     (AccumulatorInstance k (RecursiveI i) c f)
-> AccumulatorInstance k (RecursiveI i) c f
forall s a. s -> Getting a s a -> a
^.Getting
  (AccumulatorInstance k (RecursiveI i) c f)
  (Accumulator k (RecursiveI i) c f)
  (AccumulatorInstance k (RecursiveI i) c f)
forall (k :: Natural) (i1 :: Type -> Type) (c1 :: Type -> Type) f1
       (i2 :: Type -> Type) (c2 :: Type -> Type) (f2 :: Type -> Type).
Functor f2 =>
(AccumulatorInstance k i1 c1 f1
 -> f2 (AccumulatorInstance k i2 c2 f1))
-> Accumulator k i1 c1 f1 -> f2 (Accumulator k i2 c2 f1)
x)

        messages :: Vector k [f]
        messages :: Vector k [f]
messages = IVCResult k i c f
resIVCResult k i c f
-> Getting (IVCProof k c f) (IVCResult k i c f) (IVCProof k c f)
-> IVCProof k c f
forall s a. s -> Getting a s a -> a
^.Getting (IVCProof k c f) (IVCResult k i c f) (IVCProof k c f)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f
       (f :: Type -> Type).
Functor f =>
(IVCProof k c f -> f (IVCProof k c f))
-> IVCResult k i c f -> f (IVCResult k i c f)
proofIVCProof k c f
-> Getting (Vector k [f]) (IVCProof k c f) (Vector k [f])
-> Vector k [f]
forall s a. s -> Getting a s a -> a
^.Getting (Vector k [f]) (IVCProof k c f) (Vector k [f])
forall (k :: Natural) (c :: Type -> Type) f (f :: Type -> Type).
Functor f =>
(Vector k [f] -> f (Vector k [f]))
-> IVCProof k c f -> f (IVCProof k c f)
proofW

        commits :: Vector k (c f)
        commits :: Vector k (c f)
commits = IVCResult k i c f
resIVCResult k i c f
-> Getting (IVCProof k c f) (IVCResult k i c f) (IVCProof k c f)
-> IVCProof k c f
forall s a. s -> Getting a s a -> a
^.Getting (IVCProof k c f) (IVCResult k i c f) (IVCProof k c f)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f
       (f :: Type -> Type).
Functor f =>
(IVCProof k c f -> f (IVCProof k c f))
-> IVCResult k i c f -> f (IVCResult k i c f)
proofIVCProof k c f
-> Getting (Vector k (c f)) (IVCProof k c f) (Vector k (c f))
-> Vector k (c f)
forall s a. s -> Getting a s a -> a
^.Getting (Vector k (c f)) (IVCProof k c f) (Vector k (c f))
forall (k :: Natural) (c :: Type -> Type) f (c :: Type -> Type)
       (f :: Type -> Type).
Functor f =>
(Vector k (c f) -> f (Vector k (c f)))
-> IVCProof k c f -> f (IVCProof k c f)
proofX

        accScheme :: AccumulatorScheme d k (RecursiveI i) c f
        accScheme :: AccumulatorScheme d k (RecursiveI i) c f
accScheme = forall (algo :: k) (d :: Natural) (k2 :: Natural) a
       (i :: Type -> Type) (p :: Type -> Type) (c :: Type -> Type) f.
(KnownNat (d - 1), KnownNat (d + 1), Representable i, Zip i,
 HashAlgorithm algo f, RandomOracle algo f f,
 RandomOracle algo (i f) f, RandomOracle algo (c f) f,
 HomomorphicCommit [f] (c f), Field f, Scale a f,
 Scale a (PolyVec f (d + 1)), Scale f (c f)) =>
Predicate a i p -> AccumulatorScheme d k2 i c f
forall {k1} (algo :: k1) (d :: Natural) (k2 :: Natural) a
       (i :: Type -> Type) (p :: Type -> Type) (c :: Type -> Type) f.
(KnownNat (d - 1), KnownNat (d + 1), Representable i, Zip i,
 HashAlgorithm algo f, RandomOracle algo f f,
 RandomOracle algo (i f) f, RandomOracle algo (c f) f,
 HomomorphicCommit [f] (c f), Field f, Scale a f,
 Scale a (PolyVec f (d + 1)), Scale f (c f)) =>
Predicate a i p -> AccumulatorScheme d k2 i c f
accumulatorScheme @algo @d Predicate a (RecursiveI i) (RecursiveP d k i p c)
pRec

        protocol :: FiatShamir k (RecursiveI i) (RecursiveP d k i p c) c [f] [f] f
        protocol :: FiatShamir k (RecursiveI i) (RecursiveP d k i p c) c [f] [f] f
protocol = forall (algo :: k) (k2 :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) m o f.
(KnownNat k2, HashAlgorithm algo f, RandomOracle algo f f,
 RandomOracle algo (i f) f, RandomOracle algo (c f) f) =>
CommitOpen k2 i p c m o f -> FiatShamir k2 i p c m o f
forall {k1} (algo :: k1) (k2 :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) m o f.
(KnownNat k2, HashAlgorithm algo f, RandomOracle algo f f,
 RandomOracle algo (i f) f, RandomOracle algo (c f) f) =>
CommitOpen k2 i p c m o f -> FiatShamir k2 i p c m o f
fiatShamir @algo (CommitOpen k (RecursiveI i) (RecursiveP d k i p c) c [f] [f] f
 -> FiatShamir k (RecursiveI i) (RecursiveP d k i p c) c [f] [f] f)
-> CommitOpen k (RecursiveI i) (RecursiveP d k i p c) c [f] [f] f
-> FiatShamir k (RecursiveI i) (RecursiveP d k i p c) c [f] [f] f
forall a b. (a -> b) -> a -> b
$ SpecialSoundProtocol
  k (RecursiveI i) (RecursiveP d k i p c) [f] [f] f
-> CommitOpen k (RecursiveI i) (RecursiveP d k i p c) c [f] [f] f
forall m (c :: Type -> Type) f (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) o.
HomomorphicCommit m (c f) =>
SpecialSoundProtocol k i p m o f -> CommitOpen k i p c m o f
commitOpen (SpecialSoundProtocol
   k (RecursiveI i) (RecursiveP d k i p c) [f] [f] f
 -> CommitOpen k (RecursiveI i) (RecursiveP d k i p c) c [f] [f] f)
-> SpecialSoundProtocol
     k (RecursiveI i) (RecursiveP d k i p c) [f] [f] f
-> CommitOpen k (RecursiveI i) (RecursiveP d k i p c) c [f] [f] f
forall a b. (a -> b) -> a -> b
$ forall (d :: Natural) a (i :: Type -> Type) (p :: Type -> Type) f.
(KnownNat (d + 1), Representable i, Ring f, Scale a f) =>
Predicate a i p -> SpecialSoundProtocol 1 i p [f] [f] f
specialSoundProtocol' @d Predicate a (RecursiveI i) (RecursiveP d k i p c)
pRec
    in
        ( FiatShamir k (RecursiveI i) (RecursiveP d k i p c) c [f] [f] f
-> RecursiveI i f
-> Vector 1 (Vector k ([f], c f))
-> Vector (1 - 1) f
-> (Vector k (c f), [f])
forall (k :: Natural) (i :: Type -> Type) (p :: Type -> Type) m o
       f.
SpecialSoundProtocol k i p m o f
-> i f -> Vector k m -> Vector (k - 1) f -> o
verifier FiatShamir k (RecursiveI i) (RecursiveP d k i p c) c [f] [f] f
protocol RecursiveI i f
input (Vector k ([f], c f) -> Vector 1 (Vector k ([f], c f))
forall a. a -> Vector 1 a
singleton (Vector k ([f], c f) -> Vector 1 (Vector k ([f], c f)))
-> Vector k ([f], c f) -> Vector 1 (Vector k ([f], c f))
forall a b. (a -> b) -> a -> b
$ Vector k [f] -> Vector k (c f) -> Vector k ([f], c f)
forall a b. Vector k a -> Vector k b -> Vector k (a, b)
forall (f :: Type -> Type) a b. Zip f => f a -> f b -> f (a, b)
zip Vector k [f]
messages Vector k (c f)
commits) Vector 0 f
Vector (1 - 1) f
forall a. AdditiveMonoid a => a
zero
        , AccumulatorScheme d k (RecursiveI i) c f
-> Accumulator k (RecursiveI i) c f -> (Vector k (c f), c f)
forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (c :: Type -> Type) f.
AccumulatorScheme d k i c f
-> Accumulator k i c f -> (Vector k (c f), c f)
Acc.decider AccumulatorScheme d k (RecursiveI i) c f
accScheme (IVCResult k i c f
resIVCResult k i c f
-> Getting
     (Accumulator k (RecursiveI i) c f)
     (IVCResult k i c f)
     (Accumulator k (RecursiveI i) c f)
-> Accumulator k (RecursiveI i) c f
forall s a. s -> Getting a s a -> a
^.Getting
  (Accumulator k (RecursiveI i) c f)
  (IVCResult k i c f)
  (Accumulator k (RecursiveI i) c f)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f
       (f :: Type -> Type).
Functor f =>
(Accumulator k (RecursiveI i) c f
 -> f (Accumulator k (RecursiveI i) c f))
-> IVCResult k i c f -> f (IVCResult k i c f)
acc)
        )