From b9d47b3815ad665d352dfdde0ffe086ca85a2df2 Mon Sep 17 00:00:00 2001 From: Balazs Komuves Date: Sun, 12 Oct 2025 22:40:18 +0200 Subject: [PATCH] implement the FRI verifier algorithm (not extensively tested) --- reference/src/FRI/Prover.hs | 59 +-- reference/src/FRI/Types.hs | 40 ++- reference/src/FRI/Verifier.hs | 376 +++++++++++++++++++- reference/src/Field/Goldilocks/Extension.hs | 2 +- reference/src/Hash/Duplex/Monad.hs | 3 + reference/src/Hash/Merkle.hs | 52 ++- reference/src/Misc.hs | 90 ++++- reference/src/NTT/Poly.hs | 2 +- reference/src/testMain.hs | 10 +- 9 files changed, 588 insertions(+), 46 deletions(-) diff --git a/reference/src/FRI/Prover.hs b/reference/src/FRI/Prover.hs index 74bef8a..0528af8 100644 --- a/reference/src/FRI/Prover.hs +++ b/reference/src/FRI/Prover.hs @@ -11,6 +11,8 @@ import Data.Word import Control.Monad.IO.Class import System.Random +import Text.Show.Pretty + import Field.Goldilocks ( F ) import Field.Goldilocks.Extension ( FExt , scl ) import Field.Encode @@ -49,7 +51,7 @@ encodeAndProveFRI friConfig@(MkFriConfig{..}) dataMatrix = absorb finalPoly -- absorb the final final polynomial MkPoW powWitness powResponse <- performGrinding friGrindingBits -- do the grinding queryIndices <- generateQueryIndices nn friNQueryRounds -- generate query indices - let queries = map (singleQueryRound phases) queryIndices -- execute the query rounds + queries <- liftIO $ mapM (singleQueryRound phases) queryIndices -- execute the query rounds -- only for debugging purposes let challenges = MkFriChallenges @@ -99,27 +101,42 @@ encodeAndProveFRI friConfig@(MkFriConfig{..}) dataMatrix = dataCoset = MkCoset (powSubgroup ldeSubgroup expFactor) shift expFactor = exp2_ rsRateBits - singleQueryRound :: [CommitPhaseData] -> Idx -> FriQueryRound - singleQueryRound phases queryIdx = result where - initialProof = extractMerkleProof' friMerkleCapSize matrixTree $ fullDomainIndexMapFwd friRSConfig queryIdx - result = MkFriQueryRound - { queryRow = _leafData initialProof - , queryInitialTreeProof = _merklePath initialProof - , querySteps = go phases queryIdx - } + singleQueryRound :: [CommitPhaseData] -> Idx -> IO FriQueryRound + singleQueryRound phases queryIdx + | initialSanityOK = do + steps <- go phases queryIdx + return $ MkFriQueryRound + { queryRow = _leafData initialProof + , queryInitialTreeProof = _merklePath initialProof + , querySteps = steps + } + | otherwise = do + -- pPrint initialProof + fail "initial tree Merkle proof check failed" + where + initialProof = extractMerkleProof' friMerkleCapSize matrixTree $ fullDomainIndexMapFwd friRSConfig queryIdx + initialSanityOK = checkMerkleCapProof (extractMerkleCap friMerkleCapSize matrixTree) initialProof - go :: [CommitPhaseData] -> Idx -> [FriQueryStep] - go [] _ = [] - go (MkCommitPhaseData{..} : rest) idx = thisStep : go rest idx' where - intArity = exp2_ commitPhaseArity - domainSize' = Prelude.div (cosetSize commitPhaseDomain) intArity -- N/K - idx' = Prelude.mod idx domainSize' -- idx' = idx mod (N/K) - proof = extractMerkleProof' friMerkleCapSize commitPhaseMerkleTree idx' - cosetValues = elems (_leafData proof) - thisStep = MkFriQueryStep - { queryEvals = cosetValues - , queryMerklePath = _merklePath proof - } + go :: [CommitPhaseData] -> Idx -> IO [FriQueryStep] + go [] _ = return [] + go (MkCommitPhaseData{..} : rest) idx + | sanityOK = do + restSteps <- go rest idx' + return (thisStep : restSteps) + | otherwise = do + -- pPrint proof + fail "commit phase Merkle proof sanity check failed" + where + intArity = exp2_ commitPhaseArity + domainSize' = Prelude.div (cosetSize commitPhaseDomain) intArity -- N/K + idx' = Prelude.mod idx domainSize' -- idx' = idx mod (N/K) + proof = extractMerkleProof' friMerkleCapSize commitPhaseMerkleTree idx' + sanityOK = checkMerkleCapProof (extractMerkleCap friMerkleCapSize commitPhaseMerkleTree) proof + cosetValues = elems (_leafData proof) + thisStep = MkFriQueryStep + { queryEvals = cosetValues + , queryMerklePath = _merklePath proof + } -------------------------------------------------------------------------------- -- * Grinding diff --git a/reference/src/FRI/Types.hs b/reference/src/FRI/Types.hs index 93e80b1..b9076e5 100644 --- a/reference/src/FRI/Types.hs +++ b/reference/src/FRI/Types.hs @@ -94,6 +94,24 @@ instance Binary ReductionStrategy where instance FieldEncode ReductionStrategy where fieldEncode = fieldEncode . fromReductionStrategy +-- | Computes the sizes of the commit phase committed vectors + the size of the final polynomial +computeCommitPhaseFullSizes :: RSConfig -> ReductionStrategy -> ( [Log2] , Log2 ) +computeCommitPhaseFullSizes rsConfig (MkRedStrategy arities) = go (rsEncodedSize rsConfig) arities where + go :: Log2 -> [Log2] -> ( [Log2] , Log2 ) + go logN [] = ( [] , logN ) + go logN (a:as) = let ( sizes , final ) = go (logN-a) as + in ( logN : sizes , final ) + +-- | As the leafs of the commit phase Merkle trees are in fact \"folding cosets\", +-- the actual Merkle trees are smaller (less leaves) +computeCommitPhaseMerkleSizes :: RSConfig -> ReductionStrategy -> ( [Log2] , Log2 ) +computeCommitPhaseMerkleSizes rsConfig (MkRedStrategy arities) = go (rsEncodedSize rsConfig) arities where + go logN [] = ( [] , logN ) + go logN (a:as) = let ( sizes , final ) = go (logN-a) as + in ( logN-a : sizes , final ) + +-------------------------------------------------------------------------------- + -- | FRI configuration data FriConfig = MkFriConfig { friRSConfig :: RSConfig -- ^ Reed-Solomon configuration @@ -140,16 +158,6 @@ instance FieldEncode FriConfig where -------------------------------------------------------------------------------- -data FriChallenges = MkFriChallenges - { friAlpha :: FExt -- ^ column linear combination coefficient - , friBetas :: [FExt] -- ^ folding step betas - , friGrindResponse :: F -- ^ the PoW response (computed via Fiat-Shamir), which should have predetermined bit patterns - , friQueryIndices :: [Int] -- ^ query indices - } - deriving (Eq,Show) - --------------------------------------------------------------------------------- - data ReductionStrategyParams = MkRedStratPars { redStoppingDegree :: Log2 -- ^ stopping degree , redFoldingArity :: Log2 -- ^ default folding arity @@ -172,6 +180,17 @@ findReductionStrategy (MkRedStratPars{..}) (MkRSConfig{..}) = MkRedStrategy $ wo -------------------------------------------------------------------------------- +-- | Only used in the verifier (but for debugging purposes only, also in the prover...) +data FriChallenges = MkFriChallenges + { friAlpha :: FExt -- ^ column linear combination coefficient + , friBetas :: [FExt] -- ^ folding step betas + , friGrindResponse :: F -- ^ the PoW response (computed via Fiat-Shamir), which should have predetermined bit patterns + , friQueryIndices :: [Int] -- ^ query indices + } + deriving (Eq,Show) + +-------------------------------------------------------------------------------- + data FriQueryStep = MkFriQueryStep { queryEvals :: [FExt] , queryMerklePath :: RawMerklePath @@ -195,6 +214,7 @@ data FriProof = MkFriProof deriving (Eq,Show) ---------------------------------------- +-- binary instances friProofSizeInBytes :: FriProof -> Int friProofSizeInBytes friProof = fromIntegral $ L.length (encode friProof) diff --git a/reference/src/FRI/Verifier.hs b/reference/src/FRI/Verifier.hs index e00ee46..a743d5d 100644 --- a/reference/src/FRI/Verifier.hs +++ b/reference/src/FRI/Verifier.hs @@ -1,4 +1,5 @@ + {-# LANGUAGE RecordWildCards, StrictData #-} module FRI.Verifier where @@ -9,9 +10,12 @@ import Data.Bits import Data.Word import Control.Monad +import Control.Monad.Except +import Control.Monad.Trans ( lift ) +import Control.Monad.IO.Class ( liftIO ) -import Field.Goldilocks ( F ) -import Field.Goldilocks.Extension ( FExt , scl ) +import Field.Goldilocks ( F , theMultiplicativeGenerator ) +import Field.Goldilocks.Extension ( FExt , scl , inj ) import Field.Encode import NTT @@ -27,15 +31,265 @@ import FRI.Types -------------------------------------------------------------------------------- -verifyFRI :: MerkleCap -> FriProof -> DuplexIO Bool -verifyFRI matrixCap friProof@(MkFriProof{..}) = do +data FriVerifierKey = MkFriVerifierKey + { vkeyFriConfig :: FriConfig + , vkeyMatrixCap :: MerkleCap + } + deriving (Eq,Show) - challenges <- computeFriChallenges matrixCap friProof +-------------------------------------------------------------------------------- - duplexPPrint "verifier challenges" challenges +type Msg = String - return False +indent :: String -> String +indent = unlines . map (" " ++) . lines +prefixErrorMsg :: MonadError Msg m => Msg -> m a -> m a +prefixErrorMsg prefix action = catchError action handler where + handler msg = throwError (prefix ++ ":\n" ++ indent msg) + +unlessEqual :: (Eq a, Show a, MonadError Msg m) => a -> a -> (String -> String -> Msg) -> m () +unlessEqual x y mkMsg = if x == y + then return () + else throwError $ mkMsg (show x) (show y) + +failUnless :: MonadError Msg m => Bool -> Msg -> m () +failUnless ok msg = case ok of + True -> return () + False -> throwError msg + +-------------------------------------------------------------------------------- + +liftToExceptT :: MonadError e m => Either e a -> m a +liftToExceptT ei = case ei of + Left err -> throwError err + Right yyy -> return yyy + +liftToExceptDuplexIO :: ExceptT e IO a -> ExceptT e (DuplexT IO) a +liftToExceptDuplexIO = mapExceptT ioToDuplexIO + +-------------------------------------------------------------------------------- + +verifyFRI :: FriVerifierKey -> FriProof -> DuplexIO Bool +verifyFRI friVKey friProof = do + ei <- runExceptT (verifyFRI' friVKey friProof) + case ei of + Left msg -> do + liftIO $ putStrLn msg + return False + Right () -> return True + +verifyFRI' :: FriVerifierKey -> FriProof -> ExceptT Msg (DuplexT IO) () +verifyFRI' friVKey@(MkFriVerifierKey{..}) friProof@(MkFriProof{..}) = do + + -- check the proof shape + prefixErrorMsg "proof shape check failed" $ liftToExceptDuplexIO $ checkProofShape vkeyFriConfig friProof + let MkFriConfig{..} = vkeyFriConfig + + -- compute challenges + challenges <- lift $ computeFriChallenges vkeyMatrixCap friProof + {- duplexPPrint "verifier challenges" challenges -} + + -- check proof-of-work grinding + unless (checkGrindBits friGrindingBits (friGrindResponse challenges)) $ throwError "grinding challenge didn't pass" + + -- check the query rounds + liftToExceptDuplexIO $ + safeZipWithM_ (checkQueryRound friVKey challenges friProof) + (friQueryIndices challenges) proofQueryRounds + + return () + +-------------------------------------------------------------------------------- + +-- | Checks the \"initial tree proof\" (in Plonky2 lingo), and returns combined value +-- (initial \"upstream\" value) +checkInitialTreeProof :: FriVerifierKey -> FExt -> Idx -> FriQueryRound -> ExceptT String IO FExt +checkInitialTreeProof (MkFriVerifierKey{..}) alpha queryIdx (MkFriQueryRound{..}) = do + let merkleProof = MkMerkleProof + { _leafIndex = fullDomainIndexMapFwd (friRSConfig vkeyFriConfig) queryIdx + , _leafData = queryRow + , _merklePath = queryInitialTreeProof + , _dataSize = exp2_ (rsEncodedSize $ friRSConfig vkeyFriConfig) + } + let m = friNColumns vkeyFriConfig + failUnless (m == length queryRow) $ "row length doesn't equal the expected" + failUnless (checkMerkleCapProof vkeyMatrixCap merkleProof) $ "initial tree Merkle proof failed" + let alphas = powersOf m alpha + let combined = sum (safeZipWith scl (elems queryRow) alphas) + return combined + +-------------------------------------------------------------------------------- + +checkQueryRound :: FriVerifierKey -> FriChallenges -> FriProof -> Idx -> FriQueryRound -> ExceptT String IO () +checkQueryRound vkey@(MkFriVerifierKey{..}) challenges theFriProof iniQueryIdx queryRound@(MkFriQueryRound{..}) = do + + -- check the initial tree proof, and calculate the corresponding value + iniUpstreamValue <- checkInitialTreeProof vkey (friAlpha challenges) iniQueryIdx queryRound + + let MkFriConfig{..} = vkeyFriConfig + let arities = fromReductionStrategy friReductionStrategy + + let steps = + [ MkStepInfo + { stepArity = arity + , stepBeta = beta + , stepTreeCap = cap + , stepEvals = queryEvals friQueryStep + , stepMerklePath = queryMerklePath friQueryStep + } + + | (arity, beta, friQueryStep, cap) <- safeZip4 + arities + (friBetas challenges) + querySteps + (proofCommitPhaseCaps theFriProof) + ] + + let iniArity = myHead arities + let iniTreeCfg = MkTreeCfg + { _treeSize = rsEncodedSize friRSConfig - iniArity + , _cosetSize = iniArity + } + let initialStepState = MkStepState + { stateFullSize = rsEncodedSize friRSConfig + , stateShift = theMultiplicativeGenerator + , stateQueryIdx = iniQueryIdx + , stateQueryValue = iniUpstreamValue + } + + finalState <- foldM checkQueryStep initialStepState steps + let loc = stateEvalLocation finalState + let polyVal = polyEvalAt (proofFinalPoly theFriProof) (inj loc) + unlessEqual polyVal (stateQueryValue finalState) $ \a b -> + "final polynomial evaluation " ++ a ++ " does not match final downstream value " ++ b + + -- fail "checkQueryRound: not yet fully implemented" + return () + +-------------------------------------------------------------------------------- + +-- | Note: treeSize + cosetSize = vector size (because the tree is over the cosets) +data TreeCfg = MkTreeCfg + { _treeSize :: Log2 -- ^ log size of the tree (whose leafs are cosets) + , _cosetSize :: Log2 -- ^ size of the cosets + } + deriving (Eq,Show) + +data TreePos = MkTreePos + { posLeafIdx :: Int -- ^ which leaf of the commit phase tree (which is over cosets) + , posCosetOfs :: Int -- ^ which point within the coset + } + deriving (Eq,Show) + +-- we use natural indexing +-- upstream coset: { 0 , T , 2T , ... (K-1)T } where T = treeSize (note: K*T = subgroup size) +naturalIdxToTreePos :: TreeCfg -> Idx -> TreePos +naturalIdxToTreePos (MkTreeCfg treeSize arity) naturalIdx + | naturalIdx < 0 = error "naturalIdxToTreePos: negative input index" + | naturalIdx >= nn = error "naturalIdxToTreePos: out of range" + | otherwise = MkTreePos leafIdx cosetOfs + where + kk = exp2_ arity + mm = exp2_ treeSize + nn = exp2_ (treeSize + arity) + leafIdx = Prelude.mod naturalIdx mm -- leafIdx < treeSize + cosetOfs = Prelude.div naturalIdx mm -- cosetOfs < cosetSize + +naturalIdxToFoldingCoset :: F -> TreeCfg -> Idx -> Coset F +naturalIdxToFoldingCoset shift treeCfg@(MkTreeCfg{..}) naturalIdx = MkCoset cosetSubgroup offset where + MkTreePos{..} = naturalIdxToTreePos treeCfg naturalIdx + fineSubgroup = getSubgroup (_treeSize + _cosetSize) + cosetSubgroup = getSubgroup _cosetSize + offset = shift * pow_ (subgroupGen fineSubgroup) (posLeafIdx) + +-------------------------------------------------------------------------------- + +data StepInfo = MkStepInfo + { stepArity :: Log2 -- ^ folding arity + , stepBeta :: FExt -- ^ folding coeff + , stepTreeCap :: MerkleCap -- ^ commit phase Merkle cap + , stepEvals :: [FExt] -- ^ coset evals (from the FRI proof) + , stepMerklePath :: RawMerklePath -- ^ coset Merkle proof (from the FRI proof) + } + deriving Show + +data StepState = MkStepState + { stateFullSize :: Log2 -- ^ size of the vector (note: the Merkle tree is smaller as the leaves are cosets!) + , stateShift :: F -- ^ the global shift accumulates while folding + , stateQueryIdx :: Idx -- ^ current query index + , stateQueryValue :: FExt -- ^ corresponding evaluation + } + deriving Show + +stateEvalLocation :: StepState -> F +stateEvalLocation (MkStepState{..}) + = stateShift + * pow_ (subgroupGen subgroup) stateQueryIdx + where + subgroup = getSubgroup stateFullSize + +-- we use natural indexing +-- upstream coset: { 0 , T , 2T , ... (K-1)T } where T = treeSize (note: K*T = subgroup size) +checkQueryStep :: StepState -> StepInfo -> ExceptT String IO StepState +checkQueryStep upstream@(MkStepState{..}) (MkStepInfo{..}) = do + + let upstreamIdx = stateQueryIdx + let treeCfg = MkTreeCfg { _treeSize = stateFullSize - stepArity , _cosetSize = stepArity } + let treePos = naturalIdxToTreePos treeCfg stateQueryIdx + let downstreamIdx = posLeafIdx treePos + + let foldingCoset = naturalIdxToFoldingCoset stateShift treeCfg stateQueryIdx + let inverseDFT = polyCoeffArray $ cosetINTTExt foldingCoset (listToArray stepEvals) + + let betas = powersOf (exp2_ stepArity) stepBeta + let downstreamValue = sum $ safeZipWith (*) betas (elems inverseDFT) + +{- + liftIO $ do + debugPrint "upstreamIdx" upstreamIdx + debugPrint "downstreamIdx" downstreamIdx + debugPrint "treeCfg" treeCfg + debugPrint "treePos" treePos + debugPrint "evals" stepEvals + debugPrint "upstreamValue" stateQueryValue + -- debugPrint "inverseDFT" inverseDFT + debugPrint "downtreamValue" downstreamValue +-} + + unless (stateQueryValue == stepEvals !! (posCosetOfs treePos)) $ do + throwError "upstream evaluation value does not match" + + let merkleProof = MkMerkleProof + { _leafIndex = downstreamIdx -- "accidentally" this is the same + , _leafData = stepEvals + , _merklePath = stepMerklePath + , _dataSize = exp2_ (stateFullSize - stepArity) + } + unless (checkMerkleCapProof stepTreeCap merkleProof) $ do + throwError "coset evaluation Merkle proof failed" + + return $ MkStepState + { stateFullSize = stateFullSize - stepArity + , stateShift = pow_ stateShift (exp2_ stepArity) + , stateQueryIdx = downstreamIdx + , stateQueryValue = downstreamValue + } + + +-------------------------------------------------------------------------------- + +{- +data FriChallenges = MkFriChallenges + { friAlpha :: FExt -- ^ column linear combination coefficient + , friBetas :: [FExt] -- ^ folding step betas + , friGrindResponse :: F -- ^ the PoW response (computed via Fiat-Shamir), which should have predetermined bit patterns + , friQueryIndices :: [Int] -- ^ query indices + } + deriving (Eq,Show) +-} + +-- | This is straightforward enough: Reproduce the Fiat-Shamir challenges from the proof computeFriChallenges :: MerkleCap -> FriProof -> DuplexIO FriChallenges computeFriChallenges matrixCap (MkFriProof{..}) = do @@ -66,3 +320,111 @@ computeFriChallenges matrixCap (MkFriProof{..}) = do nn = exp2_ (rsDataSize + rsRateBits) -------------------------------------------------------------------------------- + +-- | Checks if the \"shape\" of the proof (sizes of lists, arrays, Merkle caps, +-- Merkle paths, etc etc) is the expected one +-- +checkProofShape :: FriConfig -> FriProof -> ExceptT String IO () +checkProofShape expectedFriConfig@(MkFriConfig{..}) (MkFriProof{..}) = + + do + -- check some global stuff + failUnless configMatches $ "FRI configuration of the proof does not match the expected one" + + unlessEqual friNQueryRounds (length proofQueryRounds) $ \a b -> + "number of query rounds in the proof " ++ a ++ " does match the expected " ++ b + + unlessEqual (length proofCommitPhaseCaps) numberOfFolds $ \a b -> + "number of commit phase Merkle caps " ++ a ++ " does not match the expected " ++ b + + unlessEqual (polySize proofFinalPoly) (exp2_ expectedFinalPolyLogDegree) $ \a b -> + "final polynomial size " ++ a ++ " does not match the expected " ++ b + + failUnless merkleCapSizes $ "commit phase Merkle cap sizes do not match the expected one" + +{- + failUnless configMatches $ "FRI configuration of the proof does not match the expected one" + failUnless numberOfRounds $ "number of query rounds in the proof does match the expected one" + failUnless nCommitPhases $ "number of commit phase Merkle caps does not match the expected one" + failUnless finalPolySize $ "final polynomial size does not match the expected" + failUnless merkleCapSizes $ "commit phase Merkle cap sizes do not match the expected one" +-} + + -- check query rounds + safeFlippedZipWithM_ [0..friNQueryRounds-1] proofQueryRounds $ \i queryRound@(MkFriQueryRound{..}) -> do + prefixErrorMsg ("in query round #" ++ show i) $ do + + -- check opened row length + unlessEqual (arrayLength queryRow) (friNColumns) $ \a b -> + "opened row size " ++ a ++ " does not match the expected " ++ b + + -- check initial tree Merkle proof path length + unlessEqual (rawMerklePathLength2 queryInitialTreeProof) (rsEncodedSize friRSConfig - friMerkleCapSize) $ \a b -> + "initial tree Merkle path length " ++ a ++ " does not match the expected " ++ b + + -- check query steps + let (treeSizes, _finalPolyLogSize) = computeCommitPhaseMerkleSizes friRSConfig friReductionStrategy + + let nsteps = length arities + + safeFlippedZipWith4M_ [0..nsteps-1] arities treeSizes querySteps $ \j arity treeSize queryStep@(MkFriQueryStep{..}) -> do + prefixErrorMsg ("in query step #" ++ show j) $ do + + -- check opened folding coset size + unlessEqual (length queryEvals) (exp2_ arity) $ \a b -> + "coset evaluation size " ++ a ++ " does not match the expected one " ++ b + + -- check coset Merkle proof path length + unlessEqual (rawMerklePathLength2 queryMerklePath) (treeSize - friMerkleCapSize) $ \a b -> + "Merkle path length " ++ a ++ " does not match the expected one " ++ b + + where + MkRSConfig{..} = friRSConfig + MkRedStrategy arities = friReductionStrategy + numberOfFolds = length arities + expectedFinalPolyLogDegree = rsDataSize - sum arities + + configMatches = expectedFriConfig == proofFriConfig + numberOfRounds = friNQueryRounds == length proofQueryRounds + nCommitPhases = length proofCommitPhaseCaps == numberOfFolds + finalPolySize = polySize proofFinalPoly == exp2_ expectedFinalPolyLogDegree + merkleCapSizes = and [ merkleCapSize cap == exp2_ friMerkleCapSize | cap <- proofCommitPhaseCaps ] + +{- + +-- RECALL THE FOLLOWING DEFINITIONS: + +data FriConfig = MkFriConfig + { friRSConfig :: RSConfig -- ^ Reed-Solomon configuration + , friNColumns :: Int -- ^ number of columns (batch FRI width) + , friMerkleCapSize :: Log2 -- ^ size of the Merkle caps + , friReductionStrategy :: ReductionStrategy -- ^ folding arities + , friNQueryRounds :: Int -- ^ number of query rounds + , friGrindingBits :: Log2 -- ^ grinding hardness + } + +data FriQueryStep = MkFriQueryStep + { queryEvals :: [FExt] + , queryMerklePath :: RawMerklePath + } + deriving (Eq,Show) + +data FriQueryRound = MkFriQueryRound + { queryRow :: FRow + , queryInitialTreeProof :: RawMerklePath + , querySteps :: [FriQueryStep] + } + deriving (Eq,Show) + +data FriProof = MkFriProof + { proofFriConfig :: FriConfig -- ^ the FRI configuration + , proofCommitPhaseCaps :: [MerkleCap] -- ^ commit phase Merkle caps + , proofFinalPoly :: Poly FExt -- ^ the final polynomial in coefficient form + , proofQueryRounds :: [FriQueryRound] -- ^ query rounds + , proofPowWitness :: F -- ^ witness showing that the prover did PoW + } + deriving (Eq,Show) + +-} + +-------------------------------------------------------------------------------- diff --git a/reference/src/Field/Goldilocks/Extension.hs b/reference/src/Field/Goldilocks/Extension.hs index f4bc930..288181c 100644 --- a/reference/src/Field/Goldilocks/Extension.hs +++ b/reference/src/Field/Goldilocks/Extension.hs @@ -33,7 +33,7 @@ instance Binary F2 where get = F2 <$> get <*> get instance Show F2 where - show (F2 r i) = "[ " ++ show r ++ " + j * " ++ show i ++ " ]" + show (F2 r i) = "(" ++ show r ++ " + j * " ++ show i ++ ")" instance Num F2 where fromInteger = inj . fromIntegral diff --git a/reference/src/Hash/Duplex/Monad.hs b/reference/src/Hash/Duplex/Monad.hs index 8c2fb09..f72e2e4 100644 --- a/reference/src/Hash/Duplex/Monad.hs +++ b/reference/src/Hash/Duplex/Monad.hs @@ -65,6 +65,9 @@ type DuplexIO a = DuplexT IO a instance MonadIO (DuplexT IO) where liftIO action = DuplexT (liftIO action) +ioToDuplexIO :: IO a -> DuplexIO a +ioToDuplexIO = liftIO + duplexPutStrLn :: String -> DuplexIO () duplexPutStrLn s = DuplexT (liftIO $ putStrLn s) diff --git a/reference/src/Hash/Merkle.hs b/reference/src/Hash/Merkle.hs index a392356..57161b0 100644 --- a/reference/src/Hash/Merkle.hs +++ b/reference/src/Hash/Merkle.hs @@ -14,7 +14,7 @@ Conventions: -} -{-# LANGUAGE StrictData #-} +{-# LANGUAGE StrictData, RecordWildCards #-} module Hash.Merkle where -------------------------------------------------------------------------------- @@ -25,6 +25,8 @@ import Data.Bits import Control.Monad import Data.Binary +import Text.Show.Pretty + import Field.Goldilocks import Field.Goldilocks.Extension ( FExt , F2(..) ) import Field.Encode @@ -143,6 +145,12 @@ newtype RawMerklePath fromRawMerklePath :: RawMerklePath -> [Digest] fromRawMerklePath (MkRawMerklePath ds) = ds +rawMerklePathLength :: RawMerklePath -> Int +rawMerklePathLength (MkRawMerklePath ds) = length ds + +rawMerklePathLength2 :: RawMerklePath -> Log2 +rawMerklePathLength2 path = Log2 (rawMerklePathLength path) + instance Binary RawMerklePath where put = putSmallList . fromRawMerklePath get = MkRawMerklePath <$> getSmallList @@ -179,6 +187,34 @@ extractMerkleProof' (Log2 capDepth) tree@(MkMerkleTree outer leaves) idx = MkMer -------------------------------------------------------------------------------- +checkMerkleRootProof :: FieldEncode a => Digest -> MerkleProof a -> Bool +checkMerkleRootProof root proof = reconstructMerkleRoot proof == root + +checkMerkleCapProof :: FieldEncode a => MerkleCap -> MerkleProof a -> Bool +-- checkMerkleCapProof = error "checkMerkleCapProof: not yet implemented" +checkMerkleCapProof (MkMerkleCap cap) (MkMerkleProof{..}) = result where + + result = go _dataSize _leafIndex (hashAny _leafData) (fromRawMerklePath _merklePath) layerFlags + + capSize = arraySize cap + + go :: Int -> Int -> Digest -> [Digest] -> [LayerFlag] -> Bool + go n j hash [] _layerFlags = if n /= capSize + then error "checkMerkleCapProof: fatal error: cap size doesn't match" + else (hash == cap!j) + go n j hash (sibling:siblings') (layerf:layerfs') = go n' j' hash' siblings' layerfs' + where + j' = shiftR j 1 + n' = shiftR (n+1) 1 + jparity = j .&. 1 + oddflag = if (j+1 == n) && (jparity == 0) then OddNode else EvenNode + key = nodeKey layerf oddflag + hash' = case jparity of + 0 -> keyedCompress theHashFunction key hash sibling + 1 -> keyedCompress theHashFunction key sibling hash + +-------------------------------------------------------------------------------- + calcMerkleTree' :: [Digest] -> [Array Int Digest] calcMerkleTree' input = case input of @@ -310,3 +346,17 @@ calcMerkleCap :: FieldEncode a => Log2 -> [a] -> MerkleCap calcMerkleCap capDepth = calcMerkleCap' capDepth . map hashAny -------------------------------------------------------------------------------- + +{- +exLeaves :: [[F]] +exLeaves = [ leaf (fromInteger i) | i<-[1..8] ] where + leaf :: F -> [F] + leaf i = [ 10*i , 10*i+1 , 10*i+2 ] + +exTree = calcMerkleTree exLeaves +exCap = extractMerkleCap (Log2 1) exTree +exIdx = 2 +exProof = extractMerkleProof' (Log2 1) exTree exIdx +exSanity = checkMerkleCapProof exCap exProof +-} + diff --git a/reference/src/Misc.hs b/reference/src/Misc.hs index 630068e..5cf62dd 100644 --- a/reference/src/Misc.hs +++ b/reference/src/Misc.hs @@ -1,4 +1,5 @@ +{-# LANGUAGE ScopedTypeVariables #-} module Misc where -------------------------------------------------------------------------------- @@ -23,6 +24,9 @@ debug_ x y = trace (">>> " ++ show x) y debug :: Show a => String -> a -> b -> b debug n x y = trace (">>> " ++ n ++ " = " ++ show x) y +debugPrint :: Show a => String -> a -> IO () +debugPrint n x = putStrLn ("> " ++ n ++ " = " ++ show x) + -------------------------------------------------------------------------------- -- * Integers @@ -47,13 +51,19 @@ newtype Log2 deriving (Eq,Ord,Show,Num) fromLog2 :: Log2 -> Int -fromLog2 (Log2 k) = k +fromLog2 (Log2 k) + | k >=0 = k + | otherwise = error "fromLog2: negative exponent" exp2 :: Log2 -> Integer -exp2 (Log2 k) = shiftL 1 k +exp2 (Log2 k) + | k >= 0 = shiftL 1 k + | otherwise = error "exp2: negative exponent" exp2_ :: Log2 -> Int -exp2_ (Log2 k) = shiftL 1 k +exp2_ (Log2 k) + | k >= 0 = shiftL 1 k + | otherwise = error "exp2_: negative exponent" -- | Smallest integer @k@ such that @2^k@ is larger or equal to @n@ ceilingLog2 :: Integer -> Log2 @@ -79,12 +89,33 @@ exactLog2__ = exactLog2_ . fromIntegral -------------------------------------------------------------------------------- -- * Lists +-- | just to avoid the annoying GHC warning +myHead :: [a] -> a +myHead (x:_) = x +myHead [] = error "myHead: empty list" + safeZipWith :: (a -> b -> c) -> [a] -> [b] -> [c] safeZipWith f = go where go [] [] = [] go (x:xs) (y:ys) = f x y : go xs ys go _ _ = error "safeZipWith: incompatible lengths" +safeZipWith3 :: (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d] +safeZipWith3 f = go where + go [] [] [] = [] + go (x:xs) (y:ys) (z:zs) = f x y z : go xs ys zs + go _ _ _ = error "safeZipWith3: incompatible lengths" + +safeZipWith4 :: (a -> b -> c -> d -> e) -> [a] -> [b] -> [c] -> [d] -> [e] +safeZipWith4 f = go where + go [] [] [] [] = [] + go (x:xs) (y:ys) (z:zs) (w:ws) = f x y z w : go xs ys zs ws + go _ _ _ _ = error "safeZipWith4: incompatible lengths" + +safeZip = safeZipWith (,) +safeZip3 = safeZipWith3 (,,) +safeZip4 = safeZipWith4 (,,,) + interleave :: [a] -> [a] -> [a] interleave (x:xs) (y:ys) = x:y:interleave xs ys interleave [] [] = [] @@ -102,6 +133,59 @@ nubOrd = worker Set.empty where | Set.member x s = worker s xs | otherwise = x : worker (Set.insert x s) xs +-------------------------------------------------------------------------------- +-- * Monads + +-- WTF, this is not in @base@ but 'Maybe' is?! +instance MonadFail (Either String) where + fail = Left + +safeZipWithM :: forall m a b c. MonadFail m => (a -> b -> m c) -> [a] -> [b] -> m [c] +safeZipWithM f xs ys = go xs ys where + go :: [a] -> [b] -> m [c] + go (x:xs) (y:ys) = do + z <- f x y + zs <- go xs ys + return (z:zs) + go [] [] = return [] + go _ _ = fail "safeZipWithM: incompatible input sizes" + +safeZipWith3M :: MonadFail m => (a -> b -> c -> m d) -> [a] -> [b] -> [c] -> m [d] +safeZipWith3M f xs ys zs = go xs ys zs where + go (x:xs) (y:ys) (z:zs) = do + w <- f x y z + ws <- go xs ys zs + return (w:ws) + go [] [] [] = return [] + go _ _ _ = fail "safeZipWith3M: incompatible input sizes" + +safeZipWith4M :: MonadFail m => (a -> b -> c -> d -> m e) -> [a] -> [b] -> [c] -> [d] -> m [e] +safeZipWith4M f xs ys zs us = go xs ys zs us where + go (x:xs) (y:ys) (z:zs) (u:us) = do + w <- f x y z u + ws <- go xs ys zs us + return (w:ws) + go [] [] [] [] = return [] + go _ _ _ _ = fail "safeZipWith4M: incompatible input sizes" + +safeZipWithM_ :: MonadFail m => (a -> b -> m c) -> [a] -> [b] -> m () +safeZipWithM_ f xs ys = void (safeZipWithM f xs ys) + +safeZipWith3M_ :: MonadFail m => (a -> b -> c -> m d) -> [a] -> [b] -> [c] -> m () +safeZipWith3M_ f xs ys zs = void (safeZipWith3M f xs ys zs) + +safeZipWith4M_ :: MonadFail m => (a -> b -> c -> d -> m e) -> [a] -> [b] -> [c] -> [d] -> m () +safeZipWith4M_ f xs ys zs us = void (safeZipWith4M f xs ys zs us) + +safeFlippedZipWithM_ :: MonadFail m => [a] -> [b] -> (a -> b -> m c) -> m () +safeFlippedZipWithM_ xs ys f = safeZipWithM_ f xs ys + +safeFlippedZipWith3M_ :: MonadFail m => [a] -> [b] -> [c] -> (a -> b -> c -> m d) -> m () +safeFlippedZipWith3M_ xs ys zs f = safeZipWith3M_ f xs ys zs + +safeFlippedZipWith4M_ :: MonadFail m =>[a] -> [b] -> [c] -> [d] -> (a -> b -> c -> d -> m e) -> m () +safeFlippedZipWith4M_ xs ys zs us f = safeZipWith4M_ f xs ys zs us + -------------------------------------------------------------------------------- -- * Arrays diff --git a/reference/src/NTT/Poly.hs b/reference/src/NTT/Poly.hs index ceac044..3676a7c 100644 --- a/reference/src/NTT/Poly.hs +++ b/reference/src/NTT/Poly.hs @@ -57,7 +57,7 @@ polyDegree (Poly arr) = worker d0 where | arr!d /= 0 = d | otherwise = worker (d-1) --- | Size of the polynomial +-- | Size of the polynomial (can be larger than @degree + 1@, if the some top coefficients are zeros) polySize :: (Eq a, Num a) => Poly a -> Int polySize (Poly p) = arraySize p diff --git a/reference/src/testMain.hs b/reference/src/testMain.hs index f816626..8f9169c 100644 --- a/reference/src/testMain.hs +++ b/reference/src/testMain.hs @@ -84,6 +84,7 @@ main = do printSeparator setStdGen (mkStdGen 1337) -- make it deterministic + -- setStdGen (mkStdGen 133756) justPrint friConfig printSeparator @@ -97,7 +98,12 @@ main = do putStrLn $ "size of the serialized proof = " ++ show (L.length lbs) putStrLn $ "could serialize proof and then load back unchanged = " ++ show (friProof == friProof') --- ok <- runDuplexIO_ (verifyFRI (_ldeCommitment commits) friProof) --- putStrLn $ "verify FRI succeed = " ++ show ok + let vkey = MkFriVerifierKey + { vkeyFriConfig = friConfig + , vkeyMatrixCap = _ldeCommitment commits + } + + ok <- runDuplexIO_ (verifyFRI vkey friProof) + putStrLn $ "verify FRI succeed = " ++ show ok --------------------------------------------------------------------------------