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
type Input f (ProtostarPermutation n) = Permutation n
type ProverMessage t (ProtostarPermutation n) = Vector n t
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"