the Nim and Haskell circuit input generators produces the same input

This commit is contained in:
Balazs Komuves 2023-11-23 14:39:20 +01:00
parent 9e61c14e5d
commit 950d6c9df9
No known key found for this signature in database
GPG Key ID: F63B7AEF18435562
14 changed files with 277 additions and 81 deletions

View File

@ -3,3 +3,4 @@
dist
dist-newstyle
*.json
json/

View File

@ -4,16 +4,27 @@ module Main where
import Slot
import Sampling
mySlotCfg :: SlotConfig
mySlotCfg = MkSlotCfg
{ _cellSize = 128
, _nCells = 1024
, _nSamples = 10
, _dataSrc = FakeData 12345
smallSlotCfg :: SlotConfig
smallSlotCfg = MkSlotCfg
{ _cellSize = 128
, _blockSize = 4096
, _nCells = 256
, _nSamples = 5
, _dataSrc = FakeData 12345
}
bigSlotCfg :: SlotConfig
bigSlotCfg = MkSlotCfg
{ _cellSize = 2048
, _blockSize = 65536
, _nCells = 512
, _nSamples = 5
, _dataSrc = FakeData 666
}
main :: IO ()
main = do
let slotCfg = mySlotCfg
circomMainComponentV1 slotCfg "slot_main.circom"
samplingTest slotCfg "input_example.json"
let slotCfg = smallSlotCfg
let entropy = 1234567 :: Entropy
circomMainComponentV1 slotCfg "./json/slot_main.circom"
samplingTest slotCfg entropy "./json/input_example.json"

View File

@ -0,0 +1,17 @@
module Misc where
--------------------------------------------------------------------------------
import Data.Bits
--------------------------------------------------------------------------------
-- | Smallest integer @k@ such that @2^k@ is larger or equal to @n@
ceilingLog2 :: Integer -> Int
ceilingLog2 0 = 0
ceilingLog2 n = 1 + go (n-1) where
go 0 = -1
go k = 1 + go (shiftR k 1)
--------------------------------------------------------------------------------

View File

@ -5,7 +5,7 @@ module Poseidon2
( Fr
, sponge1 , sponge2
, calcMerkleRoot , calcMerkleTree
, MerkleTree(..) , depthOf , merkleRootOf
, MerkleTree(..) , depthOf , merkleRootOf , treeBottomLayer
, MerkleProof(..) , extractMerkleProof , extractMerkleProof_ , reconstructMerkleRoot
, compressPair, keyedCompressPair
, permutation

View File

@ -10,7 +10,7 @@
-- if it's an even node (2 children)
--
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE BangPatterns, StrictData #-}
module Poseidon2.Merkle where
--------------------------------------------------------------------------------
@ -54,6 +54,9 @@ depthOf :: MerkleTree -> Int
depthOf (MkMerkleTree outer) = b-a where
(a,b) = bounds outer
treeBottomLayer :: MerkleTree -> [Fr]
treeBottomLayer (MkMerkleTree arr) = elems (arr!0)
{-
calcMerkleTree' :: [Fr] -> [[Fr]]
calcMerkleTree' = go where
@ -66,7 +69,7 @@ calcMerkleTree' = go where
calcMerkleTree' :: [Fr] -> [[Fr]]
calcMerkleTree' input =
case input of
[] -> error "calcMerkleRoot: input is empty"
[] -> error "calcMerkleTree': input is empty"
[z] -> [[keyedCompression (nodeKey BottomLayer OddNode) z 0]]
zs -> go layerFlags zs
where

View File

@ -1,4 +1,5 @@
{-# LANGUAGE BangPatterns, StrictData #-}
module Sampling where
--------------------------------------------------------------------------------
@ -6,6 +7,8 @@ module Sampling where
import Control.Monad
import System.IO
import qualified Data.ByteString as B
import Poseidon2
import Slot
@ -13,9 +16,8 @@ import qualified ZK.Algebra.Curves.BN128.Fr.Mont as Fr
--------------------------------------------------------------------------------
samplingTest :: SlotConfig -> FilePath -> IO ()
samplingTest slotCfg fpath = do
let entropy = 123456789 :: Fr
samplingTest :: SlotConfig -> Entropy -> FilePath -> IO ()
samplingTest slotCfg entropy fpath = do
input <- calculateCircuitInput slotCfg entropy
exportCircuitInput fpath input
@ -34,10 +36,11 @@ sampleCellIndex cfg entropy slotRoot counter = fromInteger idx where
--------------------------------------------------------------------------------
data CircuitInput = MkInput
{ _entropy :: Entropy -- ^ public input
, _slotRoot :: Hash -- ^ public input
, _cellData :: [[Fr]] -- ^ private input
, _merklePaths :: [[Fr]] -- ^ private input
{ _entropy :: Entropy -- ^ public input
, _slotRoot :: Hash -- ^ public input
, _cellsPerSlot :: Int -- ^ public input
, _cellData :: [[Fr]] -- ^ private input
, _merklePaths :: [[Fr]] -- ^ private input
}
deriving Show
@ -45,15 +48,17 @@ data CircuitInput = MkInput
calculateCircuitInput :: SlotConfig -> Entropy -> IO CircuitInput
calculateCircuitInput slotCfg entropy = do
slotTree <- calcSlotTree slotCfg
let slotRoot = merkleRootOf slotTree
let idxs = [ sampleCellIndex slotCfg entropy slotRoot j | j <- [1..(_nSamples slotCfg)] ]
let !slotRoot = slotTreeRoot slotTree
let !idxs = [ sampleCellIndex slotCfg entropy slotRoot j | j <- [1..(_nSamples slotCfg)] ]
cellData <- forM idxs $ \idx -> (cellDataToFieldElements <$> loadCellData slotCfg idx)
let merklePaths = [ extractMerkleProof_ slotTree idx | idx <- idxs ]
let !merklePaths = [ extractCellProof slotCfg slotTree idx | idx <- idxs ]
return $ MkInput
{ _entropy = entropy
, _slotRoot = slotRoot
, _cellData = cellData
, _merklePaths = merklePaths
{ _entropy = entropy
, _slotRoot = slotRoot
, _cellsPerSlot = _nCells slotCfg
, _cellData = cellData
, _merklePaths = merklePaths
}
-- | Export the inputs of the storage proof circuits in JSON format,
@ -65,8 +70,9 @@ calculateCircuitInput slotCfg entropy = do
exportCircuitInput :: FilePath -> CircuitInput -> IO ()
exportCircuitInput fpath input = do
h <- openFile fpath WriteMode
hPutStrLn h $ "{ \"entropy\": " ++ show (show (_entropy input))
hPutStrLn h $ ", \"slotRoot\": " ++ show (show (_slotRoot input))
hPutStrLn h $ "{ \"entropy\": " ++ show (show (_entropy input))
hPutStrLn h $ ", \"slotRoot\": " ++ show (show (_slotRoot input))
hPutStrLn h $ ", \"nCells\": " ++ show (show (_cellsPerSlot input))
hPutStrLn h $ ", \"cellData\": "
hPrintListOfLists h ((map.map) show $ _cellData input)
hPutStrLn h $ ", \"merklePaths\": "

View File

@ -1,10 +1,12 @@
{-# LANGUAGE BangPatterns, StrictData #-}
module Slot where
--------------------------------------------------------------------------------
import Data.Bits
import Data.Word
import Data.Array
import Data.ByteString (ByteString)
import qualified Data.ByteString as B
@ -14,12 +16,30 @@ import Control.Monad
import System.IO
import Poseidon2
import Misc
--------------------------------------------------------------------------------
type Seed = Int
type CellIdx = Int
type Hash = Fr
type Seed = Int
type CellIdx = Int
type BlockIdx = Int
type Hash = Fr
newtype CellData = CellData { fromCellData :: ByteString }
newtype BlockData = BlockData { fromBlockData :: ByteString }
instance Show CellData where show (CellData bs) = "CellData<" ++ show (B.length bs) ++ ">"
instance Show BlockData where show (BlockData bs) = "BlockData<" ++ show (B.length bs) ++ ">"
mkCellData :: SlotConfig -> ByteString -> CellData
mkCellData cfg bs = if B.length bs == _cellSize cfg
then CellData bs
else error $ "mkCellData: invalid cell size: " ++ show (B.length bs)
mkBlockData :: SlotConfig -> ByteString -> BlockData
mkBlockData cfg bs = if B.length bs == _blockSize cfg
then BlockData bs
else error $ "mkBlockData: invalid block size: " ++ show (B.length bs)
data DataSource
= SlotFile FilePath
@ -27,20 +47,33 @@ data DataSource
deriving Show
data SlotConfig = MkSlotCfg
{ _cellSize :: Int -- ^ cell size in bytes
, _nCells :: Int -- ^ number of cells per slot (should be power of two)
, _nSamples :: Int -- ^ how many cells we sample
, _dataSrc :: DataSource -- ^ slot data source
{ _cellSize :: Int -- ^ cell size in bytes (eg. 2048)
, _blockSize :: Int -- ^ block size in bytes (eg. 65536)
, _nCells :: Int -- ^ number of cells per slot (should be power of two)
, _nSamples :: Int -- ^ how many cells we sample
, _dataSrc :: DataSource -- ^ slot data source
}
deriving Show
cellsPerBlock :: SlotConfig -> Int
cellsPerBlock cfg = case divMod (_blockSize cfg) (_cellSize cfg) of
(q,0) -> if q>1 then q else error "cells per block must be at least 2"
_ -> error "block size is not divisible by the cell size"
blocksPerSlot :: SlotConfig -> Int
blocksPerSlot cfg = case divMod (_nCells cfg) (cellsPerBlock cfg) of
(q,0) -> if q>1 then q else error "blocks per slot must be at least 2"
_ -> error "slot size is not divisible by the block size"
-- | Example slot configuration
exSlotCfg :: SlotConfig
exSlotCfg = MkSlotCfg
{ _cellSize = 256
, _nCells = 1024
, _nSamples = 20
, _dataSrc = FakeData 12345
{ _cellSize = 256
, _blockSize = 4096
, _nCells = 1024
, _nSamples = 20
, _dataSrc = FakeData 12345
}
fieldElemsPerCell :: SlotConfig -> Int
@ -68,15 +101,24 @@ circomMainComponentV1 slotCfg circomFile = do
--------------------------------------------------------------------------------
-- * load data
genFakeCell :: SlotConfig -> Seed -> CellIdx -> ByteString
genFakeCell cfg seed1 seed2 = B.pack list where
list = go (_cellSize cfg) 1
go :: Int -> Int -> [Word8]
genFakeCell :: SlotConfig -> Seed -> CellIdx -> CellData
genFakeCell cfg seed idx = (mkCellData cfg $ B.pack list) where
list = go (fromIntegral $ _cellSize cfg) 1
seed1 = fromIntegral seed :: Word64
seed2 = fromIntegral idx :: Word64
go :: Word64 -> Word64 -> [Word8]
go 0 _ = []
go cnt state = fromIntegral state' : go (cnt-1) state' where
state' = state*state + seed1*state + (seed2 + 17)
loadCellData :: SlotConfig -> CellIdx -> IO ByteString
genFakeBlock :: SlotConfig -> Seed -> BlockIdx -> BlockData
genFakeBlock cfg seed blockIdx = (mkBlockData cfg $ B.concat$ map fromCellData cells) where
k = cellsPerBlock cfg
a = k * blockIdx
b = k * (blockIdx + 1) - 1
cells = [ genFakeCell cfg seed j | j<-[a..b] ]
loadCellData :: SlotConfig -> CellIdx -> IO CellData
loadCellData cfg idx = case _dataSrc cfg of
FakeData seed -> return $ genFakeCell cfg seed idx
SlotFile fname -> do
@ -84,10 +126,21 @@ loadCellData cfg idx = case _dataSrc cfg of
hSeek h AbsoluteSeek (fromIntegral (_cellSize cfg) * fromIntegral idx)
bs <- B.hGet h (_cellSize cfg)
hClose h
return bs
return (mkCellData cfg bs)
loadBlockData :: SlotConfig -> BlockIdx -> IO BlockData
loadBlockData cfg idx = case _dataSrc cfg of
FakeData seed -> return $ genFakeBlock cfg seed idx
SlotFile fname -> do
h <- openBinaryFile fname ReadMode
hSeek h AbsoluteSeek (fromIntegral (_blockSize cfg) * fromIntegral idx)
bs <- B.hGet h (_blockSize cfg)
hClose h
return (mkBlockData cfg bs)
--------------------------------------------------------------------------------
{-
calcSlotTree :: SlotConfig -> IO MerkleTree
calcSlotTree cfg = calcMerkleTree <$> calcCellHashes cfg
@ -96,17 +149,106 @@ calcCellHashes cfg = do
forM [0..(_nCells cfg - 1)] $ \idx -> do
cell <- loadCellData cfg idx
return (hashCell cell)
-}
--------------------------------------------------------------------------------
{-
-- | Split bytestring into smaller pieces
-- | Split bytestring into smaller pieces, no padding
splitByteString :: Int -> ByteString -> [ByteString]
splitByteString k = go where
go bs
| B.null bs = []
| otherwise = B.take k bs : go (B.drop k bs)
-}
splitBlockToCells :: SlotConfig -> BlockData -> [CellData]
splitBlockToCells cfg (BlockData blockdata) =
map CellData (splitByteString (_cellSize cfg) blockdata)
calcBlockTree :: SlotConfig -> BlockIdx -> IO MerkleTree
calcBlockTree cfg idx = do
block <- loadBlockData cfg idx
let cells = splitBlockToCells cfg block
let cellHashes = map (hashCell cfg) cells
let tree = calcMerkleTree cellHashes
return tree
calcAllBlockTrees :: SlotConfig -> IO (Array Int MerkleTree)
calcAllBlockTrees cfg
= listArray (0,n-1) <$> (forM [0..n-1] $ \idx -> calcBlockTree cfg idx)
where
n = blocksPerSlot cfg
--------------------------------------------------------------------------------
data SlotTree = MkSlotTree
{ _miniTrees :: Array Int MerkleTree -- ^ block trees
, _bigTree :: MerkleTree -- ^ the tree over the block hashes
}
slotTreeRoot :: SlotTree -> Hash
slotTreeRoot = merkleRootOf . _bigTree
calcSlotTree :: SlotConfig -> IO SlotTree
calcSlotTree cfg = do
minitrees <- calcAllBlockTrees cfg
let bigtree = calcMerkleTree $ map merkleRootOf $ elems minitrees
return $ MkSlotTree minitrees bigtree
extractCellProof :: SlotConfig -> SlotTree -> CellIdx -> [Hash]
extractCellProof cfg slotTree cellIdx = final where
(blockIdx, withinBlockIdx) = cellIdx `divMod` (cellsPerBlock cfg)
blockTree = (_miniTrees slotTree) ! blockIdx
proof1 = extractMerkleProof blockTree withinBlockIdx
proof2 = extractMerkleProof (_bigTree slotTree) blockIdx
final = _merklePath proof1 ++ _merklePath proof2
checkCellProof :: SlotConfig -> SlotTree -> CellIdx -> Hash -> [Hash] -> Bool
checkCellProof cfg slotTree cellIdx cellHash path
| logK + logM /= length path = error "checkCellProof: incorrect Merkle path length"
| 2^logK /= k = error "checkCellProof: non-power-of-two number of cells per blocks"
| otherwise = reSlotHash == slotTreeRoot slotTree
where
k = cellsPerBlock cfg
m = blocksPerSlot cfg
logK = ceilingLog2 (fromIntegral k)
logM = ceilingLog2 (fromIntegral m)
blockIdx = shiftR cellIdx logK
inBlockCellIdx = cellIdx .&. (k-1)
smallProof = MkMerkleProof
{ _leafIndex = inBlockCellIdx
, _leafData = cellHash
, _merklePath = take logK path
, _dataSize = k
}
bigProof = MkMerkleProof
{ _leafIndex = blockIdx
, _leafData = blockHash
, _merklePath = drop logK path
, _dataSize = m
}
blockHash = reconstructMerkleRoot smallProof
reSlotHash = reconstructMerkleRoot bigProof
--------------------------------------------------------------------------------
-- | Hash a cell
hashCell :: SlotConfig -> CellData -> Hash
hashCell cfg (CellData rawdata)
| B.length rawdata /= _cellSize cfg = error "hashCell: invalid cell data size"
| otherwise = hashCell_ rawdata
hashCell_ :: ByteString -> Hash
hashCell_ rawdata = sponge2 (cellDataToFieldElements $ CellData rawdata)
--------------------------------------------------------------------------------
-- | A 31-byte long chunk
newtype Chunk
= Chunk ByteString
deriving Show
-- | Split bytestring into samller pieces, applying the @10*@ padding strategy.
--
@ -114,33 +256,32 @@ splitByteString k = go where
-- number (in the interval @[0..k-1]@) of @0x00@ bytes to be a multiple of the
-- given chunk length
--
padAndSplitByteString :: Int -> ByteString -> [ByteString]
padAndSplitByteString :: Int -> ByteString -> [Chunk]
padAndSplitByteString k orig = go (B.snoc orig 0x01) where
go bs
| m == 0 = []
| m < k = [B.append bs (B.replicate (k-m) 0x00)]
| otherwise = B.take k bs : go (B.drop k bs)
| m < k = [Chunk $ B.append bs (B.replicate (k-m) 0x00)]
| otherwise = (Chunk $ B.take k bs) : go (B.drop k bs)
where
m = B.length bs
-- | Chunk a ByteString into a sequence of field elements
cellDataToFieldElements :: ByteString -> [Fr]
cellDataToFieldElements rawdata = map chunkToField pieces where
cellDataToFieldElements :: CellData -> [Fr]
cellDataToFieldElements (CellData rawdata) = map chunkToField pieces where
chunkSize = 31
pieces = padAndSplitByteString chunkSize rawdata
-- | Hash a cell
hashCell :: ByteString -> Hash
hashCell rawdata = sponge2 (cellDataToFieldElements rawdata)
chunkToField :: ByteString -> Fr
chunkToField chunk
| B.length chunk <= 31 = fromInteger (chunkToIntegerLE chunk)
| otherwise = error "chunkToField: chunk is too big (expecting at most 31 bytes)"
chunkToField :: Chunk -> Fr
chunkToField chunk@(Chunk bs)
| l == 31 = fromInteger (chunkToIntegerLE chunk)
| l < 31 = error "chunkToField: chunk is too small (expecting exactly 31 bytes)"
| l > 31 = error "chunkToField: chunk is too big (expecting exactly 31 bytes)"
where
l = B.length bs
-- | Interpret a ByteString as an integer (little-endian)
chunkToIntegerLE :: ByteString -> Integer
chunkToIntegerLE chunk = go (B.unpack chunk) where
chunkToIntegerLE :: Chunk -> Integer
chunkToIntegerLE (Chunk chunk) = go (B.unpack chunk) where
go [] = 0
go (w:ws) = fromIntegral w + shiftL (go ws) 8

View File

@ -52,7 +52,7 @@ testVectorsHash = do
forM_ [0..80] $ \n -> do
let input = map fromIntegral [1..n] :: [Word8]
let bs = B.pack input
putStrLn $ "hash of [1.." ++ show n ++ "] :: [Byte] = " ++ show (hashCell bs)
putStrLn $ "hash of [1.." ++ show n ++ "] :: [Byte] = " ++ show (hashCell_ bs)
--------------------------------------------------------------------------------
@ -71,7 +71,7 @@ testVectorsMerkle = do
forM_ [0..80] $ \n -> do
let input = map fromIntegral [1..n] :: [Word8]
let bs = B.pack input
let flds = cellDataToFieldElements bs
let flds = cellDataToFieldElements (CellData bs)
putStrLn $ "Merkle root of [1.." ++ show n ++ "] :: [Byte] = " ++ show (calcMerkleRoot flds)
--------------------------------------------------------------------------------

View File

@ -33,15 +33,16 @@ Library
random >= 1.1 && < 1.5,
zikkurat-algebra == 0.0.1
Exposed-Modules: Poseidon2
Sampling
Exposed-Modules: Sampling
Slot
TestVectors
Poseidon2
Poseidon2.Example
Poseidon2.Merkle
Poseidon2.Permutation
Poseidon2.RoundConsts
Poseidon2.Sponge
Misc
TestVectors
Default-Language: Haskell2010
Default-Extensions: CPP, BangPatterns

View File

@ -1,3 +1,4 @@
.DS_Store
testmain
*.json
*.json
json/

View File

@ -17,10 +17,10 @@ func extractLowBits[n: static int]( A: BigInt[n], k: int): uint64 =
assert( k>0 and k<=64 )
var r : uint64 = 0
for i in 0..<k:
let b = bit[n](A, n-1-i) # it's BIG-ENDIAN (wtf)
let b = bit[n](A, i) # NOTE: the docunmentation seems to lie about the conventions here....
let y = uint64(b)
if (y != 0):
r = bitor( r, 1'u64 shl y )
r = bitor( r, 1'u64 shl i )
return r
func extractLowBits(fld: F, k: int): uint64 =

View File

@ -12,24 +12,39 @@ import blocks
#
const exSlotCfg =
SlotConfig( nCells: 1024
, nSamples: 20
SlotConfig( nCells: 256 # 1024
, nSamples: 5 # 20
, dataSrc: DataSource(kind: FakeData, seed: 12345)
)
#-------------------------------------------------------------------------------
{.overflowChecks: off.}
func genFakeCell(cfg: SlotConfig, seed1: Seed, seed2: CellIdx): Cell =
func genFakeCell(cfg: SlotConfig, seed: Seed, idx: CellIdx): Cell =
let seed1 : uint64 = uint64(seed)
let seed2 : uint64 = uint64(idx)
var cell : seq[byte] = newSeq[byte](cellSize)
var state : int64 = 0
var state : uint64 = 1
for i in 0..<cellSize:
state = state*state + seed1*state + (seed2 + 17)
cell[i] = byte(state)
return cell
#[
--
-- the Haskell version, for reference:
--
genFakeCell :: SlotConfig -> Seed -> CellIdx -> CellData
genFakeCell cfg seed idx = (mkCellData cfg $ B.pack list) where
list = go (fromIntegral $ _cellSize cfg) 1
seed1 = fromIntegral seed :: Word64
seed2 = fromIntegral idx :: Word64
go :: Word64 -> Word64 -> [Word8]
go 0 _ = []
go cnt state = fromIntegral state' : go (cnt-1) state' where
state' = state*state + seed1*state + (seed2 + 17)
]#
#-------------------------------------------------------------------------------
proc loadCellData*(cfg: SlotConfig, idx: CellIdx): Cell =

View File

@ -48,8 +48,8 @@ when isMainModule:
# testAllMerkleProofs(20)
let fakedata = DataSource(kind: FakeData, seed: 12345)
let slotcfg = SlotConfig( nCells: 128, nSamples: 3, dataSrc: fakedata)
let slotcfg = SlotConfig( nCells: 256, nSamples: 5, dataSrc: fakedata)
let entropy = toF( 1234567 )
let prfInput = generateProofInput(slotcfg, entropy)
exportProofInput( "foo.json" , prfInput )
exportProofInput( "json/foo.json" , prfInput )

View File

@ -8,8 +8,8 @@ export types
#-------------------------------------------------------------------------------
const cellSize* : int = 2048 # size of the cells we prove
const blockSize* : int = 65536 # size of the network block
const cellSize* : int = 128 # 2048 # size of the cells we prove
const blockSize* : int = 4096 # 65536 # size of the network block
const cellsPerBlock* : int = blockSize div cellSize