{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module ZkFold.Base.Protocol.Protostar.FiatShamir where import Data.ByteString (ByteString) import GHC.Generics import Prelude hiding (Bool (..), Eq (..), length) import qualified Prelude as P import ZkFold.Base.Data.ByteString (Binary (..)) import ZkFold.Base.Protocol.NonInteractiveProof (NonInteractiveProof (..), ToTranscript (..), challenge) import ZkFold.Base.Protocol.Protostar.CommitOpen import qualified ZkFold.Base.Protocol.Protostar.SpecialSound as SpS import ZkFold.Base.Protocol.Protostar.SpecialSound (SpecialSoundProtocol (..), SpecialSoundTranscript) import ZkFold.Symbolic.Data.Bool import ZkFold.Symbolic.Data.Eq data FiatShamir f a = FiatShamir a (SpS.Input f a) deriving (forall x. FiatShamir f a -> Rep (FiatShamir f a) x) -> (forall x. Rep (FiatShamir f a) x -> FiatShamir f a) -> Generic (FiatShamir f a) forall x. Rep (FiatShamir f a) x -> FiatShamir f a forall x. FiatShamir f a -> Rep (FiatShamir f a) x forall a. (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a forall f a x. Rep (FiatShamir f a) x -> FiatShamir f a forall f a x. FiatShamir f a -> Rep (FiatShamir f a) x $cfrom :: forall f a x. FiatShamir f a -> Rep (FiatShamir f a) x from :: forall x. FiatShamir f a -> Rep (FiatShamir f a) x $cto :: forall f a x. Rep (FiatShamir f a) x -> FiatShamir f a to :: forall x. Rep (FiatShamir f a) x -> FiatShamir f a Generic fsChallenge :: forall f a c m . Binary (SpS.Input f a) => Binary (VerifierMessage f a) => Binary c => Binary (ProverMessage f a) => m ~ ProverMessage f a => FiatShamir f (CommitOpen m c a) -> SpecialSoundTranscript f (CommitOpen m c a) -> ProverMessage f (CommitOpen m c a) -> VerifierMessage f a fsChallenge :: forall f a c m. (Binary (Input f a), Binary (VerifierMessage f a), Binary c, Binary (ProverMessage f a), m ~ ProverMessage f a) => FiatShamir f (CommitOpen m c a) -> SpecialSoundTranscript f (CommitOpen m c a) -> ProverMessage f (CommitOpen m c a) -> VerifierMessage f a fsChallenge (FiatShamir CommitOpen m c a _ Input f (CommitOpen m c a) ip) [] ProverMessage f (CommitOpen m c a) c = let r0 :: VerifierMessage f a r0 = forall ts a. FromTranscript ts a => ts -> a challenge @ByteString (ByteString -> VerifierMessage f a) -> ByteString -> VerifierMessage f a forall a b. (a -> b) -> a -> b $ Input f a -> ByteString forall ts a. ToTranscript ts a => a -> ts toTranscript Input f a Input f (CommitOpen m c a) ip :: VerifierMessage f a in forall ts a. FromTranscript ts a => ts -> a challenge @ByteString (ByteString -> VerifierMessage f a) -> ByteString -> VerifierMessage f a forall a b. (a -> b) -> a -> b $ VerifierMessage f a -> ByteString forall ts a. ToTranscript ts a => a -> ts toTranscript VerifierMessage f a r0 ByteString -> ByteString -> ByteString forall a. Semigroup a => a -> a -> a <> CommitOpenProverMessage m c -> ByteString forall ts a. ToTranscript ts a => a -> ts toTranscript ProverMessage f (CommitOpen m c a) CommitOpenProverMessage m c c fsChallenge FiatShamir f (CommitOpen m c a) _ ((ProverMessage f (CommitOpen m c a) _, VerifierMessage f (CommitOpen m c a) r) : [(ProverMessage f (CommitOpen m c a), VerifierMessage f (CommitOpen m c a))] _) ProverMessage f (CommitOpen m c a) c = forall ts a. FromTranscript ts a => ts -> a challenge @ByteString (ByteString -> VerifierMessage f a) -> ByteString -> VerifierMessage f a forall a b. (a -> b) -> a -> b $ VerifierMessage f a -> ByteString forall ts a. ToTranscript ts a => a -> ts toTranscript VerifierMessage f a VerifierMessage f (CommitOpen m c a) r ByteString -> ByteString -> ByteString forall a. Semigroup a => a -> a -> a <> CommitOpenProverMessage m c -> ByteString forall ts a. ToTranscript ts a => a -> ts toTranscript ProverMessage f (CommitOpen m c a) CommitOpenProverMessage m c c instance ( SpS.SpecialSoundProtocol f a , Binary (SpS.Input f a) , Binary (VerifierMessage f a) , VerifierMessage f a ~ f , ProverMessage f a ~ m , Binary c , Binary (ProverMessage f a) , BoolType (VerifierOutput f a) , Eq (VerifierOutput f a) [c] , VerifierOutput f a ~ P.Bool ) => NonInteractiveProof (FiatShamir f (CommitOpen m c a)) core where type Transcript (FiatShamir f (CommitOpen m c a)) = ByteString type SetupProve (FiatShamir f (CommitOpen m c a)) = FiatShamir f (CommitOpen m c a) type SetupVerify (FiatShamir f (CommitOpen m c a)) = FiatShamir f (CommitOpen m c a) type Witness (FiatShamir f (CommitOpen m c a)) = SpS.Witness f a type Input (FiatShamir f (CommitOpen m c a)) = (SpS.Input f a, [c]) type Proof (FiatShamir f (CommitOpen m c a)) = [ProverMessage f a] setupProve :: FiatShamir f (CommitOpen m c a) -> SetupProve (FiatShamir f (CommitOpen m c a)) setupProve FiatShamir f (CommitOpen m c a) x = SetupProve (FiatShamir f (CommitOpen m c a)) FiatShamir f (CommitOpen m c a) x setupVerify :: FiatShamir f (CommitOpen m c a) -> SetupVerify (FiatShamir f (CommitOpen m c a)) setupVerify FiatShamir f (CommitOpen m c a) x = SetupVerify (FiatShamir f (CommitOpen m c a)) FiatShamir f (CommitOpen m c a) x prove :: SetupProve (FiatShamir f (CommitOpen m c a)) -> Witness (FiatShamir f (CommitOpen m c a)) -> (Input (FiatShamir f (CommitOpen m c a)), Proof (FiatShamir f (CommitOpen m c a))) prove fs :: SetupProve (FiatShamir f (CommitOpen m c a)) fs@(FiatShamir CommitOpen m c a a Input f (CommitOpen m c a) ip) Witness (FiatShamir f (CommitOpen m c a)) w = let ([m] ms, SpecialSoundTranscript f (CommitOpen m c a) ts) = forall f a c m. (SpecialSoundProtocol f a, BoolType (VerifierOutput f a), Eq (VerifierOutput f a) [c], m ~ ProverMessage f a) => CommitOpen m c a -> Witness f a -> Input f a -> (SpecialSoundTranscript f (CommitOpen m c a) -> ProverMessage f (CommitOpen m c a) -> VerifierMessage f a) -> ([m], SpecialSoundTranscript f (CommitOpen m c a)) opening @f @a @c @m CommitOpen m c a a Witness f a Witness (FiatShamir f (CommitOpen m c a)) w Input f a Input f (CommitOpen m c a) ip (FiatShamir f (CommitOpen (ProverMessage f a) c a) -> SpecialSoundTranscript f (CommitOpen (ProverMessage f a) c a) -> ProverMessage f (CommitOpen (ProverMessage f a) c a) -> VerifierMessage f a forall f a c m. (Binary (Input f a), Binary (VerifierMessage f a), Binary c, Binary (ProverMessage f a), m ~ ProverMessage f a) => FiatShamir f (CommitOpen m c a) -> SpecialSoundTranscript f (CommitOpen m c a) -> ProverMessage f (CommitOpen m c a) -> VerifierMessage f a fsChallenge SetupProve (FiatShamir f (CommitOpen m c a)) FiatShamir f (CommitOpen (ProverMessage f a) c a) fs) in ((Input f a Input f (CommitOpen m c a) ip, forall f a c m. SpecialSoundTranscript f (CommitOpen m c a) -> [c] commits @f @a @c @m SpecialSoundTranscript f (CommitOpen m c a) ts), [m] Proof (FiatShamir f (CommitOpen m c a)) ms) verify :: SetupVerify (FiatShamir f (CommitOpen m c a)) -> Input (FiatShamir f (CommitOpen m c a)) -> Proof (FiatShamir f (CommitOpen m c a)) -> Bool verify fs :: SetupVerify (FiatShamir f (CommitOpen m c a)) fs@(FiatShamir CommitOpen m c a a Input f (CommitOpen m c a) _) (Input f a ip, [c] cs) Proof (FiatShamir f (CommitOpen m c a)) ms = let ts' :: [(CommitOpenProverMessage m c, VerifierMessage f a)] ts' = ([(CommitOpenProverMessage m c, VerifierMessage f a)] -> CommitOpenProverMessage m c -> [(CommitOpenProverMessage m c, VerifierMessage f a)]) -> [(CommitOpenProverMessage m c, VerifierMessage f a)] -> [CommitOpenProverMessage m c] -> [(CommitOpenProverMessage m c, VerifierMessage f a)] forall b a. (b -> a -> b) -> b -> [a] -> b forall (t :: Type -> Type) b a. Foldable t => (b -> a -> b) -> b -> t a -> b foldl (\[(CommitOpenProverMessage m c, VerifierMessage f a)] acc CommitOpenProverMessage m c c -> [(CommitOpenProverMessage m c, VerifierMessage f a)] acc [(CommitOpenProverMessage m c, VerifierMessage f a)] -> [(CommitOpenProverMessage m c, VerifierMessage f a)] -> [(CommitOpenProverMessage m c, VerifierMessage f a)] forall a. [a] -> [a] -> [a] ++ [(CommitOpenProverMessage m c c, FiatShamir f (CommitOpen (ProverMessage f a) c a) -> SpecialSoundTranscript f (CommitOpen (ProverMessage f a) c a) -> ProverMessage f (CommitOpen (ProverMessage f a) c a) -> VerifierMessage f a forall f a c m. (Binary (Input f a), Binary (VerifierMessage f a), Binary c, Binary (ProverMessage f a), m ~ ProverMessage f a) => FiatShamir f (CommitOpen m c a) -> SpecialSoundTranscript f (CommitOpen m c a) -> ProverMessage f (CommitOpen m c a) -> VerifierMessage f a fsChallenge SetupVerify (FiatShamir f (CommitOpen m c a)) FiatShamir f (CommitOpen (ProverMessage f a) c a) fs SpecialSoundTranscript f (CommitOpen (ProverMessage f a) c a) [(CommitOpenProverMessage m c, VerifierMessage f a)] acc ProverMessage f (CommitOpen (ProverMessage f a) c a) CommitOpenProverMessage m c c)]) [] ([CommitOpenProverMessage m c] -> [(CommitOpenProverMessage m c, VerifierMessage f a)]) -> [CommitOpenProverMessage m c] -> [(CommitOpenProverMessage m c, VerifierMessage f a)] forall a b. (a -> b) -> a -> b $ (c -> CommitOpenProverMessage m c) -> [c] -> [CommitOpenProverMessage m c] forall a b. (a -> b) -> [a] -> [b] map c -> CommitOpenProverMessage m c forall m c. c -> CommitOpenProverMessage m c Commit [c] cs ts :: [(CommitOpenProverMessage m c, VerifierMessage f a)] ts = [(CommitOpenProverMessage m c, VerifierMessage f a)] ts' [(CommitOpenProverMessage m c, VerifierMessage f a)] -> [(CommitOpenProverMessage m c, VerifierMessage f a)] -> [(CommitOpenProverMessage m c, VerifierMessage f a)] forall a. [a] -> [a] -> [a] ++ [([m] -> CommitOpenProverMessage m c forall m c. [m] -> CommitOpenProverMessage m c Open [m] Proof (FiatShamir f (CommitOpen m c a)) ms, FiatShamir f (CommitOpen (ProverMessage f a) c a) -> SpecialSoundTranscript f (CommitOpen (ProverMessage f a) c a) -> ProverMessage f (CommitOpen (ProverMessage f a) c a) -> VerifierMessage f a forall f a c m. (Binary (Input f a), Binary (VerifierMessage f a), Binary c, Binary (ProverMessage f a), m ~ ProverMessage f a) => FiatShamir f (CommitOpen m c a) -> SpecialSoundTranscript f (CommitOpen m c a) -> ProverMessage f (CommitOpen m c a) -> VerifierMessage f a fsChallenge SetupVerify (FiatShamir f (CommitOpen m c a)) FiatShamir f (CommitOpen (ProverMessage f a) c a) fs SpecialSoundTranscript f (CommitOpen (ProverMessage f a) c a) [(CommitOpenProverMessage m c, VerifierMessage f a)] ts' (ProverMessage f (CommitOpen (ProverMessage f a) c a) -> VerifierMessage f a) -> ProverMessage f (CommitOpen (ProverMessage f a) c a) -> VerifierMessage f a forall a b. (a -> b) -> a -> b $ [m] -> CommitOpenProverMessage m c forall m c. [m] -> CommitOpenProverMessage m c Open [m] Proof (FiatShamir f (CommitOpen m c a)) ms)] ([CommitOpenProverMessage m c] ri, [VerifierMessage f a] ci) = [(CommitOpenProverMessage m c, VerifierMessage f a)] -> ([CommitOpenProverMessage m c], [VerifierMessage f a]) forall a b. [(a, b)] -> ([a], [b]) unzip [(CommitOpenProverMessage m c, VerifierMessage f a)] ts in CommitOpen m c a -> Input (VerifierMessage f a) (CommitOpen m c a) -> [ProverMessage (VerifierMessage f a) (CommitOpen m c a)] -> [VerifierMessage f a] -> VerifierOutput (VerifierMessage f a) (CommitOpen m c a) forall f a. SpecialSoundProtocol f a => a -> Input f a -> [ProverMessage f a] -> [f] -> VerifierOutput f a verifier CommitOpen m c a a Input f a Input (VerifierMessage f a) (CommitOpen m c a) ip [ProverMessage (VerifierMessage f a) (CommitOpen m c a)] [CommitOpenProverMessage m c] ri [VerifierMessage f a] ci