module ZkFold.Base.Protocol.ARK.Protostar.Permutation where

import           Data.Zip                                        (Zip (..))
import           Numeric.Natural                                 (Natural)
import           Prelude                                         hiding (Num (..), zipWith, (!!), (^))

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Algebra.Basic.Permutations          (Permutation, applyPermutation)
import           ZkFold.Base.Algebra.Polynomials.Multivariate    (Polynomial', var)
import           ZkFold.Base.Data.Vector                         (Vector)
import           ZkFold.Base.Protocol.ARK.Protostar.SpecialSound (SpecialSoundProtocol (..), SpecialSoundTranscript)
import           ZkFold.Symbolic.Compiler                        (Arithmetic)

data ProtostarPermutation (n :: Natural)

instance Arithmetic f => SpecialSoundProtocol f (ProtostarPermutation n) where
    type Witness f (ProtostarPermutation n)         = Vector n f
    -- ^ w in the paper
    type Input f (ProtostarPermutation n)           = Permutation n
    -- ^ \sigma in the paper
    type ProverMessage t (ProtostarPermutation n)   = Vector n t
    -- ^ same as Witness
    type VerifierMessage t (ProtostarPermutation n) = ()

    type Dimension (ProtostarPermutation n)         = n
    type Degree (ProtostarPermutation n)            = 1

    rounds :: ProtostarPermutation n -> Natural
    rounds :: ProtostarPermutation n -> Natural
rounds ProtostarPermutation n
_ = Natural
1

    prover :: ProtostarPermutation n
           -> Witness f (ProtostarPermutation n)
           -> Input f (ProtostarPermutation n)
           -> SpecialSoundTranscript f (ProtostarPermutation n)
           -> ProverMessage f (ProtostarPermutation n)
    prover :: ProtostarPermutation n
-> Witness f (ProtostarPermutation n)
-> Input f (ProtostarPermutation n)
-> SpecialSoundTranscript f (ProtostarPermutation n)
-> ProverMessage f (ProtostarPermutation n)
prover ProtostarPermutation n
_ Witness f (ProtostarPermutation n)
w Input f (ProtostarPermutation n)
_ SpecialSoundTranscript f (ProtostarPermutation n)
_ = Witness f (ProtostarPermutation n)
ProverMessage f (ProtostarPermutation n)
w

    verifier' :: ProtostarPermutation n
              -> Input f (ProtostarPermutation n)
              -> SpecialSoundTranscript Natural (ProtostarPermutation n)
              -> Vector (Dimension (ProtostarPermutation n)) (Polynomial' f)
    verifier' :: ProtostarPermutation n
-> Input f (ProtostarPermutation n)
-> SpecialSoundTranscript Natural (ProtostarPermutation n)
-> Vector (Dimension (ProtostarPermutation n)) (Polynomial' f)
verifier' ProtostarPermutation n
_ Input f (ProtostarPermutation n)
sigma [(ProverMessage Natural (ProtostarPermutation n)
w, VerifierMessage Natural (ProtostarPermutation n)
_)] = (Polynomial' f -> Polynomial' f -> Polynomial' f)
-> Vector n (Polynomial' f)
-> Vector n (Polynomial' f)
-> Vector n (Polynomial' f)
forall a b c.
(a -> b -> c) -> Vector n a -> Vector n b -> Vector n c
forall (f :: Type -> Type) a b c.
Zip f =>
(a -> b -> c) -> f a -> f b -> f c
zipWith (-) (Permutation n
-> Vector n (Polynomial' f) -> Vector n (Polynomial' f)
forall (n :: Natural) a. Permutation n -> Vector n a -> Vector n a
applyPermutation Permutation n
Input f (ProtostarPermutation n)
sigma Vector n (Polynomial' f)
wX) Vector n (Polynomial' f)
wX
      where wX :: Vector n (Polynomial' f)
wX = (Natural -> Polynomial' f)
-> Vector n Natural -> Vector n (Polynomial' f)
forall a b. (a -> b) -> Vector n a -> Vector n b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Natural -> Polynomial' f
forall c i j.
Polynomial c i j =>
i -> P c i j (Map i j) [(c, M i j (Map i j))]
var Vector n Natural
ProverMessage Natural (ProtostarPermutation n)
w
    verifier' ProtostarPermutation n
_ Input f (ProtostarPermutation n)
_ SpecialSoundTranscript Natural (ProtostarPermutation n)
_ = [Char] -> Vector n (Polynomial' f)
forall a. HasCallStack => [Char] -> a
error [Char]
"Invalid transcript"


    verifier :: ProtostarPermutation n
             -> Input f (ProtostarPermutation n)
             -> SpecialSoundTranscript f (ProtostarPermutation n)
             -> Bool
    verifier :: ProtostarPermutation n
-> Input f (ProtostarPermutation n)
-> SpecialSoundTranscript f (ProtostarPermutation n)
-> Bool
verifier ProtostarPermutation n
_ Input f (ProtostarPermutation n)
sigma [(ProverMessage f (ProtostarPermutation n)
w, VerifierMessage f (ProtostarPermutation n)
_)] = Permutation n -> Vector n f -> Vector n f
forall (n :: Natural) a. Permutation n -> Vector n a -> Vector n a
applyPermutation Permutation n
Input f (ProtostarPermutation n)
sigma Vector n f
ProverMessage f (ProtostarPermutation n)
w Vector n f -> Vector n f -> Bool
forall a. Eq a => a -> a -> Bool
== Vector n f
ProverMessage f (ProtostarPermutation n)
w
    verifier ProtostarPermutation n
_ Input f (ProtostarPermutation n)
_     SpecialSoundTranscript f (ProtostarPermutation n)
_        = [Char] -> Bool
forall a. HasCallStack => [Char] -> a
error [Char]
"Invalid transcript"