mirror of
https://github.com/logos-storage/outsourcing-Reed-Solomon.git
synced 2026-01-02 13:43:07 +00:00
implement the FRI verifier algorithm (not extensively tested)
This commit is contained in:
Balazs Komuves
parent
64753a1fc7
commit
b9d47b3815
@ -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
|
||||
|
||||
@ -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)
|
||||
|
||||
@ -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)
|
||||
|
||||
-}
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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)
|
||||
|
||||
|
||||
@ -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
|
||||
-}
|
||||
|
||||
|
||||
@ -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
|
||||
|
||||
|
||||
@ -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
|
||||
|
||||
|
||||
@ -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
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user