mirror of
https://github.com/logos-storage/plonky2-verifier.git
synced 2026-01-02 13:53:07 +00:00
parsing verifier only circuit data works
This commit is contained in:
parent
b437f915e8
commit
f30bea78a4
84
Digest.hs
Normal file
84
Digest.hs
Normal file
@ -0,0 +1,84 @@
|
||||
|
||||
{-# LANGUAGE DeriveGeneric, OverloadedStrings #-}
|
||||
module Digest where
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
import Data.Array
|
||||
import Data.Word
|
||||
import Data.Bits
|
||||
|
||||
import GHC.Generics
|
||||
import Data.Aeson ( FromJSON(..) , ToJSON(..) , object , withObject , (.=) , (.:) )
|
||||
|
||||
import Goldilocks
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
type State = Array Int F
|
||||
|
||||
listToState' :: Int -> [F] -> State
|
||||
listToState' n = listArray (0,n-1)
|
||||
|
||||
listToState :: [F] -> State
|
||||
listToState = listToState' 12
|
||||
|
||||
zeroState' :: Int -> State
|
||||
zeroState' n = listToState' n (replicate n 0)
|
||||
|
||||
zeroState :: State
|
||||
zeroState = zeroState' 12
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
data Digest
|
||||
= MkDigest !F !F !F !F
|
||||
deriving (Eq,Show,Generic)
|
||||
|
||||
instance ToJSON Digest where
|
||||
toJSON (MkDigest a b c d) = object [ "elements" .= toJSON [a,b,c,d] ]
|
||||
|
||||
instance FromJSON Digest where
|
||||
parseJSON = withObject "Digest" $ \obj -> listToDigest <$> obj .: "elements"
|
||||
|
||||
zeroDigest :: Digest
|
||||
zeroDigest = MkDigest 0 0 0 0
|
||||
|
||||
extractDigest :: State -> Digest
|
||||
extractDigest state = case elems state of
|
||||
(a:b:c:d:_) -> MkDigest a b c d
|
||||
|
||||
extractCapacity :: State -> [F]
|
||||
extractCapacity state = case elems state of
|
||||
(_:_:_:_:_:_:_:_:a:b:c:d:[]) -> [a,b,c,d]
|
||||
|
||||
listToDigest :: [F] -> Digest
|
||||
listToDigest [a,b,c,d] = MkDigest a b c d
|
||||
|
||||
digestToList :: Digest -> [F]
|
||||
digestToList (MkDigest a b c d) = [a,b,c,d]
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
digestToWord64s :: Digest -> [Word64]
|
||||
digestToWord64s (MkDigest a b c d) = [ fromF a, fromF b, fromF c, fromF d]
|
||||
|
||||
digestToBytes :: Digest -> [Word8]
|
||||
digestToBytes = concatMap bytesFromWord64LE . digestToWord64s
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
bytesFromWord64LE :: Word64 -> [Word8]
|
||||
bytesFromWord64LE = go 0 where
|
||||
go 8 _ = []
|
||||
go !k !w = fromIntegral (w .&. 0xff) : go (k+1) (shiftR w 8)
|
||||
|
||||
bytesToWord64LE :: [Word8] -> Word64
|
||||
bytesToWord64LE = fromInteger . bytesToIntegerLE
|
||||
|
||||
bytesToIntegerLE :: [Word8] -> Integer
|
||||
bytesToIntegerLE = go where
|
||||
go [] = 0
|
||||
go (this:rest) = fromIntegral this + 256 * go rest
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
@ -18,6 +18,9 @@ import Text.Printf
|
||||
|
||||
import System.Random
|
||||
|
||||
import GHC.Generics
|
||||
import Data.Aeson ( ToJSON(..), FromJSON(..) )
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
type F = Goldilocks
|
||||
@ -81,10 +84,22 @@ rootsOfUnity = listArray (0,32) $ map toF
|
||||
|
||||
newtype Goldilocks
|
||||
= Goldilocks Integer
|
||||
deriving Eq
|
||||
deriving (Eq,Generic)
|
||||
|
||||
asInteger :: Goldilocks -> Integer
|
||||
asInteger (Goldilocks x) = x
|
||||
|
||||
instance Show Goldilocks where
|
||||
show (Goldilocks k) = printf "0x%016x" k
|
||||
-- show (Goldilocks x) = printf "0x%016x" x
|
||||
show (Goldilocks x) = show x
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
instance ToJSON Goldilocks where
|
||||
toJSON x = toJSON (asInteger x)
|
||||
|
||||
instance FromJSON Goldilocks where
|
||||
parseJSON o = mkGoldilocks <$> parseJSON o
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
|
||||
82
Hash.hs
82
Hash.hs
@ -8,63 +8,41 @@ import Data.Word
|
||||
import Data.Bits
|
||||
|
||||
import Goldilocks
|
||||
import Poseidon
|
||||
import Digest
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
type State = Array Int F
|
||||
-- | Poseidon sponge construction (rate=8, capacity=4) without padding.
|
||||
--
|
||||
-- Notes:
|
||||
--
|
||||
-- * Plonky2 to use the sponge in \"overwrite mode\"
|
||||
--
|
||||
-- * No padding is applied (inputs are expected to be fixed length)
|
||||
--
|
||||
sponge :: [F] -> Digest
|
||||
sponge = go zeroState where
|
||||
go !state [] = extractDigest state
|
||||
go !state xs = case splitAt 8 xs of
|
||||
(this,rest) -> go (permutation $ combine this state) rest
|
||||
combine xs arr = listToState $ xs ++ drop (length xs) (elems arr)
|
||||
|
||||
listToState' :: Int -> [F] -> State
|
||||
listToState' n = listArray (0,n-1)
|
||||
-- | Sponge with @10*1@ padding. The only place this is used is hashing
|
||||
-- the domain separator (which is empty by default)
|
||||
spongeWithPad :: [F] -> Digest
|
||||
spongeWithPad what = go zeroState (what ++ [1]) where
|
||||
go !state [] = extractDigest state
|
||||
go !state xs = case splitAt 8 xs of
|
||||
(this,rest) -> go (permutation $ combine this state) rest
|
||||
combine xs arr = let k = length xs in if k < 8
|
||||
then listToState $ xs ++ replicate (8-k-1) 0 ++ [1] ++ drop 8 (elems arr)
|
||||
else listToState $ xs ++ drop k (elems arr)
|
||||
|
||||
listToState :: [F] -> State
|
||||
listToState = listToState' 12
|
||||
|
||||
zeroState' :: Int -> State
|
||||
zeroState' n = listToState' n (replicate n 0)
|
||||
|
||||
zeroState :: State
|
||||
zeroState = zeroState' 12
|
||||
-- | Compression function for Merkle trees
|
||||
compress :: Digest -> Digest -> Digest
|
||||
compress x y = extractDigest $ permutation $ listToState s0 where
|
||||
s0 = digestToList x ++ digestToList y ++ [0,0,0,0]
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
data Digest
|
||||
= MkDigest !F !F !F !F
|
||||
deriving (Eq,Show)
|
||||
|
||||
zeroDigest :: Digest
|
||||
zeroDigest = MkDigest 0 0 0 0
|
||||
|
||||
extractDigest :: State -> Digest
|
||||
extractDigest state = case elems state of
|
||||
(a:b:c:d:_) -> MkDigest a b c d
|
||||
|
||||
listToDigest :: [F] -> Digest
|
||||
listToDigest [a,b,c,d] = MkDigest a b c d
|
||||
|
||||
digestToList :: Digest -> [F]
|
||||
digestToList (MkDigest a b c d) = [a,b,c,d]
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
digestToWord64s :: Digest -> [Word64]
|
||||
digestToWord64s (MkDigest a b c d) = [ fromF a, fromF b, fromF c, fromF d]
|
||||
|
||||
digestToBytes :: Digest -> [Word8]
|
||||
digestToBytes = concatMap bytesFromWord64LE . digestToWord64s
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
bytesFromWord64LE :: Word64 -> [Word8]
|
||||
bytesFromWord64LE = go 0 where
|
||||
go 8 _ = []
|
||||
go !k !w = fromIntegral (w .&. 0xff) : go (k+1) (shiftR w 8)
|
||||
|
||||
bytesToWord64LE :: [Word8] -> Word64
|
||||
bytesToWord64LE = fromInteger . bytesToIntegerLE
|
||||
|
||||
bytesToIntegerLE :: [Word8] -> Integer
|
||||
bytesToIntegerLE = go where
|
||||
go [] = 0
|
||||
go (this:rest) = fromIntegral this + 256 * go rest
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
@ -16,7 +16,7 @@ import Data.Array.IArray
|
||||
|
||||
import Goldilocks
|
||||
import Constants
|
||||
import Hash
|
||||
import Digest
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
|
||||
97
Types.hs
97
Types.hs
@ -1,18 +1,26 @@
|
||||
|
||||
{-# LANGUAGE StrictData #-}
|
||||
{-# LANGUAGE StrictData, DeriveGeneric, DeriveAnyClass #-}
|
||||
module Types where
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
import Data.Word
|
||||
|
||||
import Data.Aeson
|
||||
import GHC.Generics
|
||||
|
||||
import Goldilocks
|
||||
import Digest
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
type KeccakHash = [Word8]
|
||||
newtype KeccakHash
|
||||
= MkKeccakHash [Word8]
|
||||
deriving (Eq,Show,Generic)
|
||||
|
||||
type LookupTable = [(Word64,Word64)]
|
||||
newtype LookupTable
|
||||
= MkLookupTable [(Word64,Word64)]
|
||||
deriving (Eq,Show,Generic)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
@ -31,7 +39,7 @@ data CommonCircuitData = MkCommonCircuitData
|
||||
, circuit_num_lookup_selectors :: Int -- ^ The number of lookup selectors.
|
||||
, circuit_luts :: [LookupTable] -- ^ The stored lookup tables.
|
||||
}
|
||||
deriving (Eq,Show)
|
||||
deriving (Eq,Show,Generic)
|
||||
|
||||
data CircuitConfig = MkCircuitConfig
|
||||
{ cfg_num_wires :: Int -- ^ Number of wires available at each row. This corresponds to the "width" of the circuit, and consists in the sum of routed wires and advice wires.
|
||||
@ -45,42 +53,19 @@ data CircuitConfig = MkCircuitConfig
|
||||
, cfg_max_quotient_degree_factor :: Int -- ^ A cap on the quotient polynomial's degree factor.
|
||||
, cfg_fri_config :: FriConfig
|
||||
}
|
||||
deriving (Eq,Show)
|
||||
deriving (Eq,Show,Generic)
|
||||
|
||||
-- | The interval @[a,b)@ (inclusive on the left, exclusive on the right)
|
||||
data Range
|
||||
= MkRange Int Int
|
||||
deriving (Eq,Show)
|
||||
deriving (Eq,Show,Generic)
|
||||
|
||||
data SelectorsInfo = MkSelectorsInfo
|
||||
{ selector_indices :: [Int]
|
||||
, groups :: [Range]
|
||||
, selector_vector :: Maybe [Int]
|
||||
}
|
||||
deriving (Eq,Show)
|
||||
|
||||
data FriConfig = MkFrConfig
|
||||
{ fri_rate_bits :: Int -- ^ @rate = 2^{-rate_bits}@
|
||||
, fri_cap_height :: Int -- ^ Height of Merkle tree caps.
|
||||
, fri_proof_of_work_bits :: Int -- ^ Number of bits used for grinding.
|
||||
, fri_reduction_strategy :: FriReductionStrategy -- ^ The reduction strategy to be applied at each layer during the commit phase.
|
||||
, fri_num_query_rounds :: Int -- ^ Number of query rounds to perform.
|
||||
}
|
||||
deriving (Eq,Show)
|
||||
|
||||
data FriReductionStrategy
|
||||
= Fixed { arity_bits_seq :: [Int] }
|
||||
| ConstantArityBits { arity_bits :: Int , final_poly_bits :: Int }
|
||||
| MinSize { opt_max_arity_bits :: Maybe Int }
|
||||
deriving (Eq,Show)
|
||||
|
||||
data FriParams = MkFriParams
|
||||
{ fri_config :: FriConfig -- ^ User-specified FRI configuration.
|
||||
, fri_hiding :: Bool -- ^ Whether to use a hiding variant of Merkle trees (where random salts are added to leaves).
|
||||
, fri_degree_bits :: Int -- ^ The degree of the purported codeword, measured in bits.
|
||||
, fri_reduction_arity_bits :: [Int] -- ^ The arity of each FRI reduction step, expressed as the log2 of the actual arity.
|
||||
}
|
||||
deriving (Eq,Show)
|
||||
deriving (Eq,Show,Generic)
|
||||
|
||||
data Gate
|
||||
= ArithmeticGate { num_ops :: Int }
|
||||
@ -99,6 +84,56 @@ data Gate
|
||||
| RandomAccessGate { bits :: Int, num_copies :: Int, num_extra_constants :: Int }
|
||||
| ReducingGate { num_coeffs :: Int }
|
||||
| ReducingExtensionGate { num_coeffs :: Int }
|
||||
deriving (Eq,Show)
|
||||
deriving (Eq,Show,Generic)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
data FriConfig = MkFrConfig
|
||||
{ fri_rate_bits :: Int -- ^ @rate = 2^{-rate_bits}@
|
||||
, fri_cap_height :: Int -- ^ Height of Merkle tree caps.
|
||||
, fri_proof_of_work_bits :: Int -- ^ Number of bits used for grinding.
|
||||
, fri_reduction_strategy :: FriReductionStrategy -- ^ The reduction strategy to be applied at each layer during the commit phase.
|
||||
, fri_num_query_rounds :: Int -- ^ Number of query rounds to perform.
|
||||
}
|
||||
deriving (Eq,Show,Generic)
|
||||
|
||||
data FriReductionStrategy
|
||||
= Fixed { arity_bits_seq :: [Int] }
|
||||
| ConstantArityBits { arity_bits :: Int , final_poly_bits :: Int }
|
||||
| MinSize { opt_max_arity_bits :: Maybe Int }
|
||||
deriving (Eq,Show,Generic)
|
||||
|
||||
data FriParams = MkFriParams
|
||||
{ fri_config :: FriConfig -- ^ User-specified FRI configuration.
|
||||
, fri_hiding :: Bool -- ^ Whether to use a hiding variant of Merkle trees (where random salts are added to leaves).
|
||||
, fri_degree_bits :: Int -- ^ The degree of the purported codeword, measured in bits.
|
||||
, fri_reduction_arity_bits :: [Int] -- ^ The arity of each FRI reduction step, expressed as the log2 of the actual arity.
|
||||
}
|
||||
deriving (Eq,Show,Generic)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
newtype PublicInputs
|
||||
= MkPublicInputs [F]
|
||||
deriving (Eq,Show,Generic)
|
||||
|
||||
data VerifierCircuitData = MkVerifierCircuitData
|
||||
{ verifier_only :: VerifierOnlyCircuitData
|
||||
, verifier_common :: CommonCircuitData
|
||||
}
|
||||
deriving (Eq,Show,Generic)
|
||||
|
||||
newtype MerkleCap
|
||||
= MkMerkleCap [Digest]
|
||||
deriving (Eq,Show,Generic)
|
||||
|
||||
data VerifierOnlyCircuitData = MkVerifierOnlyCircuitData
|
||||
{ constants_sigmas_cap :: MerkleCap -- ^ commitment to list of constant polynomial and sigma polynomials
|
||||
, circuit_digest :: Digest -- ^ a digest of the "circuit" (i.e. the instance, minus public inputs), which can be used to seed Fiat-Shamir
|
||||
}
|
||||
deriving (Eq,Show,Generic,ToJSON,FromJSON)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
instance ToJSON MerkleCap where toJSON (MkMerkleCap caps) = toJSON caps
|
||||
instance FromJSON MerkleCap where parseJSON o = MkMerkleCap <$> parseJSON o
|
||||
|
||||
27
testmain.hs
Normal file
27
testmain.hs
Normal file
@ -0,0 +1,27 @@
|
||||
|
||||
module Main where
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
import Data.Aeson
|
||||
|
||||
import Types
|
||||
import Hash
|
||||
import Digest
|
||||
import Goldilocks
|
||||
|
||||
import qualified Data.ByteString.Char8 as B
|
||||
import qualified Data.ByteString.Lazy.Char8 as L
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
main = do
|
||||
let publicIO = MkPublicInputs [0, 1, 3736710860384812976]
|
||||
text_common <- L.readFile "json/fibonacci_common.json"
|
||||
text_proof <- L.readFile "json/fibonacci_proof.json"
|
||||
text_vkey <- L.readFile "json/fibonacci_vkey.json"
|
||||
|
||||
let Just vkey = decode text_vkey :: Maybe VerifierOnlyCircuitData
|
||||
print vkey
|
||||
putStrLn ""
|
||||
L.putStr (encode vkey)
|
||||
Loading…
x
Reference in New Issue
Block a user