{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module ZkFold.Base.Protocol.Protostar.CommitOpen where import GHC.Generics import Prelude hiding (Eq (..), length, (&&), (/=), (==)) import ZkFold.Base.Data.ByteString import ZkFold.Base.Protocol.Protostar.Oracle import ZkFold.Base.Protocol.Protostar.SpecialSound (AlgebraicMap (..), SpecialSoundProtocol (..), SpecialSoundTranscript) import ZkFold.Prelude (length) import ZkFold.Symbolic.Data.Bool import ZkFold.Symbolic.Data.Eq data CommitOpen m c a = CommitOpen ([m] -> c) a instance RandomOracle a b => RandomOracle (CommitOpen m c a) b where oracle :: CommitOpen m c a -> b oracle (CommitOpen [m] -> c _ a a) = a -> b forall a b. RandomOracle a b => a -> b oracle a a data CommitOpenProverMessage m c = Commit c | Open [m] deriving (forall x. CommitOpenProverMessage m c -> Rep (CommitOpenProverMessage m c) x) -> (forall x. Rep (CommitOpenProverMessage m c) x -> CommitOpenProverMessage m c) -> Generic (CommitOpenProverMessage m c) forall x. Rep (CommitOpenProverMessage m c) x -> CommitOpenProverMessage m c forall x. CommitOpenProverMessage m c -> Rep (CommitOpenProverMessage m c) x forall a. (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a forall m c x. Rep (CommitOpenProverMessage m c) x -> CommitOpenProverMessage m c forall m c x. CommitOpenProverMessage m c -> Rep (CommitOpenProverMessage m c) x $cfrom :: forall m c x. CommitOpenProverMessage m c -> Rep (CommitOpenProverMessage m c) x from :: forall x. CommitOpenProverMessage m c -> Rep (CommitOpenProverMessage m c) x $cto :: forall m c x. Rep (CommitOpenProverMessage m c) x -> CommitOpenProverMessage m c to :: forall x. Rep (CommitOpenProverMessage m c) x -> CommitOpenProverMessage m c Generic instance (Binary c, Binary m) => Binary (CommitOpenProverMessage m c) where put :: CommitOpenProverMessage m c -> Put put (Commit c c) = Word8 -> Put putWord8 Word8 0 Put -> Put -> Put forall a. Semigroup a => a -> a -> a <> c -> Put forall t. Binary t => t -> Put put c c put (Open [m] msgs) = Word8 -> Put putWord8 Word8 1 Put -> Put -> Put forall a. Semigroup a => a -> a -> a <> [m] -> Put forall t. Binary t => t -> Put put [m] msgs get :: Get (CommitOpenProverMessage m c) get = do Word8 flag <- Get Word8 getWord8 if Word8 flag Word8 -> Word8 -> Bool forall b a. Eq b a => a -> a -> b == Word8 0 then c -> CommitOpenProverMessage m c forall m c. c -> CommitOpenProverMessage m c Commit (c -> CommitOpenProverMessage m c) -> Get c -> Get (CommitOpenProverMessage m c) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b <$> Get c forall t. Binary t => Get t get else if Word8 flag Word8 -> Word8 -> Bool forall b a. Eq b a => a -> a -> b == Word8 1 then [m] -> CommitOpenProverMessage m c forall m c. [m] -> CommitOpenProverMessage m c Open ([m] -> CommitOpenProverMessage m c) -> Get [m] -> Get (CommitOpenProverMessage m c) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b <$> Get [m] forall t. Binary t => Get t get else String -> Get (CommitOpenProverMessage m c) forall a. String -> Get a forall (m :: Type -> Type) a. MonadFail m => String -> m a fail (String "Binary (CommitOpenProverMessage t c a): unexpected flag " String -> String -> String forall a. Semigroup a => a -> a -> a <> Word8 -> String forall a. Show a => a -> String show Word8 flag) instance ( SpecialSoundProtocol f a , BoolType (VerifierOutput f a) , Eq (VerifierOutput f a) [c] , m ~ ProverMessage f a ) => SpecialSoundProtocol f (CommitOpen m c a) where type Witness f (CommitOpen m c a) = (Witness f a, [m]) type Input f (CommitOpen m c a) = Input f a type ProverMessage f (CommitOpen m c a) = CommitOpenProverMessage m c type VerifierMessage f (CommitOpen m c a) = VerifierMessage f a type VerifierOutput f (CommitOpen m c a) = VerifierOutput f a type Degree (CommitOpen m c a) = Degree a outputLength :: CommitOpen m c a -> Natural outputLength (CommitOpen [m] -> c _ a a) = forall f a. SpecialSoundProtocol f a => a -> Natural outputLength @f a a rounds :: CommitOpen m c a -> Natural rounds (CommitOpen [m] -> c _ a a) = forall f a. SpecialSoundProtocol f a => a -> Natural rounds @f a a Natural -> Natural -> Natural forall a. Num a => a -> a -> a + Natural 1 prover :: CommitOpen m c a -> Witness f (CommitOpen m c a) -> Input f (CommitOpen m c a) -> SpecialSoundTranscript f (CommitOpen m c a) -> ProverMessage f (CommitOpen m c a) prover (CommitOpen [m] -> c cm a a) (Witness f a w, [m] ms) Input f (CommitOpen m c a) i SpecialSoundTranscript f (CommitOpen m c a) ts | [(CommitOpenProverMessage m c, VerifierMessage f a)] -> Natural forall (t :: Type -> Type) a. Foldable t => t a -> Natural length SpecialSoundTranscript f (CommitOpen m c a) [(CommitOpenProverMessage m c, VerifierMessage f a)] ts Natural -> Natural -> Bool forall b a. Eq b a => a -> a -> b /= [m] -> Natural forall (t :: Type -> Type) a. Foldable t => t a -> Natural length [m] ms = String -> CommitOpenProverMessage m c forall a. HasCallStack => String -> a error String "Invalid transcript length" | [(CommitOpenProverMessage m c, VerifierMessage f a)] -> Natural forall (t :: Type -> Type) a. Foldable t => t a -> Natural length SpecialSoundTranscript f (CommitOpen m c a) [(CommitOpenProverMessage m c, VerifierMessage f a)] ts Natural -> Natural -> Bool forall a. Ord a => a -> a -> Bool < forall f a. SpecialSoundProtocol f a => a -> Natural rounds @f a a = c -> CommitOpenProverMessage m c forall m c. c -> CommitOpenProverMessage m c Commit (c -> CommitOpenProverMessage m c) -> c -> CommitOpenProverMessage m c forall a b. (a -> b) -> a -> b $ [m] -> c cm [forall f a. SpecialSoundProtocol f a => a -> Witness f a -> Input f a -> SpecialSoundTranscript f a -> ProverMessage f a prover @f a a Witness f a w Input f a Input f (CommitOpen m c a) i (SpecialSoundTranscript f a -> ProverMessage f a) -> SpecialSoundTranscript f a -> ProverMessage f a forall a b. (a -> b) -> a -> b $ [ProverMessage f a] -> [VerifierMessage f a] -> SpecialSoundTranscript f a forall a b. [a] -> [b] -> [(a, b)] zip [m] [ProverMessage f a] ms ([VerifierMessage f a] -> SpecialSoundTranscript f a) -> [VerifierMessage f a] -> SpecialSoundTranscript f a forall a b. (a -> b) -> a -> b $ ((CommitOpenProverMessage m c, VerifierMessage f a) -> VerifierMessage f a) -> [(CommitOpenProverMessage m c, VerifierMessage f a)] -> [VerifierMessage f a] forall a b. (a -> b) -> [a] -> [b] map (CommitOpenProverMessage m c, VerifierMessage f a) -> VerifierMessage f a forall a b. (a, b) -> b snd SpecialSoundTranscript f (CommitOpen m c a) [(CommitOpenProverMessage m c, VerifierMessage f a)] ts] | Bool otherwise = [m] -> CommitOpenProverMessage m c forall m c. [m] -> CommitOpenProverMessage m c Open [m] ms verifier :: CommitOpen m c a -> Input f (CommitOpen m c a) -> [ProverMessage f (CommitOpen m c a)] -> [f] -> VerifierOutput f (CommitOpen m c a) verifier (CommitOpen [m] -> c cm a a) Input f (CommitOpen m c a) i ((Open [m] ms):[ProverMessage f (CommitOpen m c a)] mss) (f _:[f] ts) = (m -> c) -> [m] -> [c] forall a b. (a -> b) -> [a] -> [b] map ([m] -> c cm ([m] -> c) -> (m -> [m]) -> m -> c forall b c a. (b -> c) -> (a -> b) -> a -> c . m -> [m] forall a. a -> [a] forall (f :: Type -> Type) a. Applicative f => a -> f a pure) [m] ms [c] -> [c] -> VerifierOutput f a forall b a. Eq b a => a -> a -> b == (CommitOpenProverMessage m c -> c) -> [CommitOpenProverMessage m c] -> [c] forall a b. (a -> b) -> [a] -> [b] map CommitOpenProverMessage m c -> c forall {m} {c}. CommitOpenProverMessage m c -> c f [ProverMessage f (CommitOpen m c a)] [CommitOpenProverMessage m c] mss VerifierOutput f a -> VerifierOutput f a -> VerifierOutput f a forall b. BoolType b => b -> b -> b && forall f a. SpecialSoundProtocol f a => a -> Input f a -> [ProverMessage f a] -> [f] -> VerifierOutput f a verifier @f a a Input f a Input f (CommitOpen m c a) i [m] [ProverMessage f a] ms [f] ts where f :: CommitOpenProverMessage m c -> c f (Commit c c) = c c f CommitOpenProverMessage m c _ = String -> c forall a. HasCallStack => String -> a error String "Invalid message" verifier CommitOpen m c a _ Input f (CommitOpen m c a) _ [ProverMessage f (CommitOpen m c a)] _ [f] _ = String -> VerifierOutput f a forall a. HasCallStack => String -> a error String "Invalid transcript" instance (AlgebraicMap f a, m ~ MapMessage f a) => AlgebraicMap f (CommitOpen m c a) where type MapInput f (CommitOpen m c a) = MapInput f a type MapMessage f (CommitOpen m c a) = CommitOpenProverMessage m c algebraicMap :: CommitOpen m c a -> MapInput f (CommitOpen m c a) -> [MapMessage f (CommitOpen m c a)] -> [f] -> f -> [f] algebraicMap (CommitOpen [m] -> c _ a a) MapInput f (CommitOpen m c a) i ((Open [m] ms):[MapMessage f (CommitOpen m c a)] _) [f] ts = forall f a. AlgebraicMap f a => a -> MapInput f a -> [MapMessage f a] -> [f] -> f -> [f] algebraicMap @f a a MapInput f a MapInput f (CommitOpen m c a) i [m] [MapMessage f a] ms [f] ts algebraicMap CommitOpen m c a _ MapInput f (CommitOpen m c a) _ [MapMessage f (CommitOpen m c a)] _ [f] _ = String -> f -> [f] forall a. HasCallStack => String -> a error String "CommitOpen algebraic map: invalid transcript" commits :: forall f a c m . SpecialSoundTranscript f (CommitOpen m c a) -> [c] commits :: forall f a c m. SpecialSoundTranscript f (CommitOpen m c a) -> [c] commits = ((CommitOpenProverMessage m c, VerifierMessage f a) -> c) -> [(CommitOpenProverMessage m c, VerifierMessage f a)] -> [c] forall a b. (a -> b) -> [a] -> [b] map (ProverMessage f (CommitOpen m c a), VerifierMessage f (CommitOpen m c a)) -> c (CommitOpenProverMessage m c, VerifierMessage f a) -> c f where f :: (ProverMessage f (CommitOpen m c a), VerifierMessage f (CommitOpen m c a)) -> c f :: (ProverMessage f (CommitOpen m c a), VerifierMessage f (CommitOpen m c a)) -> c f (Commit c c, VerifierMessage f (CommitOpen m c a) _) = c c f (ProverMessage f (CommitOpen m c a), VerifierMessage f (CommitOpen m c a)) _ = String -> c forall a. HasCallStack => String -> a error String "Invalid message" opening :: 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 :: 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 a' :: CommitOpen m c a a'@(CommitOpen [m] -> c _ a a) Witness f a w Input f a i SpecialSoundTranscript f (CommitOpen m c a) -> ProverMessage f (CommitOpen m c a) -> VerifierMessage f a challenge = let f :: ([m], [(CommitOpenProverMessage m c, VerifierMessage f a)]) -> Natural -> ([m], [(CommitOpenProverMessage m c, VerifierMessage f a)]) f ([m] ms, [(CommitOpenProverMessage m c, VerifierMessage f a)] ts) Natural _ = let rs :: [VerifierMessage f a] rs = (CommitOpenProverMessage m c, VerifierMessage f a) -> VerifierMessage f a forall a b. (a, b) -> b snd ((CommitOpenProverMessage m c, VerifierMessage f a) -> VerifierMessage f a) -> [(CommitOpenProverMessage m c, VerifierMessage f a)] -> [VerifierMessage f a] forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b <$> [(CommitOpenProverMessage m c, VerifierMessage f a)] ts tsA :: [(m, VerifierMessage f a)] tsA = [m] -> [VerifierMessage f a] -> [(m, VerifierMessage f a)] forall a b. [a] -> [b] -> [(a, b)] zip [m] ms [VerifierMessage f a] rs m :: ProverMessage f a m = forall f a. SpecialSoundProtocol f a => a -> Witness f a -> Input f a -> SpecialSoundTranscript f a -> ProverMessage f a prover @f a a Witness f a w Input f a i [(m, VerifierMessage f a)] SpecialSoundTranscript f a tsA c :: ProverMessage f (CommitOpen m c a) c = forall f a. SpecialSoundProtocol f a => a -> Witness f a -> Input f a -> SpecialSoundTranscript f a -> ProverMessage f a prover @f CommitOpen m c a a' (Witness f a w, [m] ms) Input f a Input f (CommitOpen m c a) i SpecialSoundTranscript f (CommitOpen m c a) [(CommitOpenProverMessage m c, VerifierMessage f a)] ts in ([m] ms [m] -> [m] -> [m] forall a. [a] -> [a] -> [a] ++ [m ProverMessage f a m], [(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] ++ [(ProverMessage f (CommitOpen m c a) CommitOpenProverMessage m c c, SpecialSoundTranscript f (CommitOpen m c a) -> ProverMessage f (CommitOpen m c a) -> VerifierMessage f a challenge SpecialSoundTranscript f (CommitOpen m c a) [(CommitOpenProverMessage m c, VerifierMessage f a)] ts ProverMessage f (CommitOpen m c a) c)]) in (([m], [(CommitOpenProverMessage m c, VerifierMessage f a)]) -> Natural -> ([m], [(CommitOpenProverMessage m c, VerifierMessage f a)])) -> ([m], [(CommitOpenProverMessage m c, VerifierMessage f a)]) -> [Natural] -> ([m], [(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 ([m], [(CommitOpenProverMessage m c, VerifierMessage f a)]) -> Natural -> ([m], [(CommitOpenProverMessage m c, VerifierMessage f a)]) f ([], []) [Natural 1 .. forall f a. SpecialSoundProtocol f a => a -> Natural rounds @f a a]