module ZkFold.Base.Protocol.IVC.CommitOpen where

import           Data.Zip                              (zipWith)
import           Prelude                               hiding (Num (..), length, pi, tail, zipWith, (&&))

import           ZkFold.Base.Algebra.Basic.Class       (AdditiveGroup (..))
import           ZkFold.Base.Data.Vector               (Vector)
import           ZkFold.Base.Protocol.IVC.Commit       (HomomorphicCommit (hcommit))
import           ZkFold.Base.Protocol.IVC.SpecialSound (SpecialSoundProtocol (..))

type CommitOpen k i p c m o f = SpecialSoundProtocol k i p (m, c f) (Vector k (c f), o) f

commitOpen :: HomomorphicCommit m (c f) => SpecialSoundProtocol k i p m o f -> CommitOpen k i p c m o f
commitOpen :: 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 {i f -> p f -> i f
i f -> p f -> f -> Natural -> m
i f -> Vector k m -> Vector (k - 1) f -> o
input :: i f -> p f -> i f
prover :: i f -> p f -> f -> Natural -> m
verifier :: i f -> Vector k m -> Vector (k - 1) f -> o
input :: forall (k :: Natural) (i :: Type -> Type) (p :: Type -> Type) m o
       f.
SpecialSoundProtocol k i p m o f -> i f -> p f -> i f
prover :: 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
verifier :: 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
..} =
    let
        prover' :: i f -> p f -> f -> Natural -> (m, c f)
prover' i f
pi0 p f
w f
r Natural
i =
            let m :: m
m = i f -> p f -> f -> Natural -> m
prover i f
pi0 p f
w f
r Natural
i
            in (m
m, m -> c f
forall a c. HomomorphicCommit a c => a -> c
hcommit m
m)

        verifier' :: i f -> Vector k (m, c f) -> Vector (k - 1) f -> (Vector k (c f), o)
verifier' i f
pi Vector k (m, c f)
pms Vector (k - 1) f
rs =
            let ms :: Vector k m
ms = ((m, c f) -> m) -> Vector k (m, c f) -> Vector k m
forall a b. (a -> b) -> Vector k a -> Vector k b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (m, c f) -> m
forall a b. (a, b) -> a
fst Vector k (m, c f)
pms
                cs :: Vector k (c f)
cs = ((m, c f) -> c f) -> Vector k (m, c f) -> Vector k (c f)
forall a b. (a -> b) -> Vector k a -> Vector k b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (m, c f) -> c f
forall a b. (a, b) -> b
snd Vector k (m, c f)
pms
            in ((c f -> c f -> c f)
-> Vector k (c f) -> Vector k (c f) -> Vector k (c f)
forall a b c.
(a -> b -> c) -> Vector k a -> Vector k b -> Vector k c
forall (f :: Type -> Type) a b c.
Zip f =>
(a -> b -> c) -> f a -> f b -> f c
zipWith (-) ((m -> c f) -> Vector k m -> Vector k (c f)
forall a b. (a -> b) -> Vector k a -> Vector k b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap m -> c f
forall a c. HomomorphicCommit a c => a -> c
hcommit Vector k m
ms) Vector k (c f)
cs, i f -> Vector k m -> Vector (k - 1) f -> o
verifier i f
pi Vector k m
ms Vector (k - 1) f
rs)
    in
        (i f -> p f -> i f)
-> (i f -> p f -> f -> Natural -> (m, c f))
-> (i f
    -> Vector k (m, c f) -> Vector (k - 1) f -> (Vector k (c f), o))
-> SpecialSoundProtocol k i p (m, c f) (Vector k (c f), o) f
forall (k :: Natural) (i :: Type -> Type) (p :: Type -> Type) m o
       f.
(i f -> p f -> i f)
-> (i f -> p f -> f -> Natural -> m)
-> (i f -> Vector k m -> Vector (k - 1) f -> o)
-> SpecialSoundProtocol k i p m o f
SpecialSoundProtocol i f -> p f -> i f
input i f -> p f -> f -> Natural -> (m, c f)
prover' i f -> Vector k (m, c f) -> Vector (k - 1) f -> (Vector k (c f), o)
verifier'