This document describes the storage proof system for the Codex 2023 Q4 MVP.
README.md- this documentcircuit/- the proof circuit (circomcode)reference/haskell/- Haskell reference implementation of the proof input generationreference/nim/proof_input/- Nim reference implementation of the proof input generationreference/nim/testvectors/- Nim script to generate test vectors for Poseidon2 sponge hashtest/- tests for (some parts of the) circuit (using ther1cs-solvertool)workflow/- description and script for the full proof workflow
We assume that a user dataset is split into nSlots number of (not necessarily
uniformly sized) "slots" of size slotSize, for example 10 GB or 100 GB or even
1,000 GB (for the MVP we may chose a smaller sizes). The slots of the same dataset
are spread over different storage nodes, but a single storage node can hold several
slots (of different sizes, and belonging to different datasets). The slots themselves
can be optionally erasure coded, but this does not change the proof system, only
the robustness of it.
We assume the slots are split into nCells number of fixed, uniformly sized
"cells" of size cellSize, for example 2048 bytes. Note that nCells can
depend on the particular slot. For the initial version, we assume
that these numbers are powers of two (especially nCells). Worst case we
can just pad the data to achieve this (it probably makes more sense to pad
before the erasure coding, even though this increases the computational cost).
Note that we can simply calculate:
nCells = slotSize / cellSize
We hash each cell independently, using the sponge construction with Poseidon2 (see below for details).
The cells are then organized to blockSize = 64kb blocks, each block containing
blockSize / cellSize = 32 cells. This is for compatibility with the networking
layer, which use larger (right now 64kb) blocks. For each block, we compute a
block hash by building a depth 5 = log2(32) complete Merkle tree, using again
Poseidon2 hash, with the Merkle tree conventions described below.
Then on the set of of block hashes in a slot (we have slotSize / blockSize many
ones), we build another (big) Merkle tree, whose root will identify the slot,
which we call the the "slot root", and is denoted by slotRoot.
Then for a given dataset, containing several slots, we can build a third binary
Merkle tree on the top of its slot roots, resulting in the "dataset root" (note:
this is not the same as the SHA256 hash associated with the original dataset
uploaded by the user). Grafting these Merkle trees together we get a big dataset
Merkle tree; however one should be careful about the padding conventions
(it makes sense to construct the dataset-level Merkle tree separately, as nSlots
may not be a power of two, and later maybe nCells and nBlocks won't be
power-of-two either).
The dataset root is a commitment to the whole (erasure coded) dataset, and will be posted on-chain, to ensure that the nodes really store its data and not something else. Optionally, the slot roots can be posted on-chain, but this seems to be somewhat wasteful.
For the MVP we will use the Poseidon2 hash function, specialized to state size
t = 3 field elements, and to the alt-bn128 elliptic curve's scalar field, which
has size
r = 21888242871839275222246405745257275088548364400416034343698204186575808495617
For more details about this curve, see BN254 For The Rest Of Us.
Remark: we have 2^253 < r < 2^254.
For more details about the Poseidon2 hash, see
Poseidon2 hash works not over sequence of bytes, but field elements. Hence we need to convert the data to be hashed to a sequence of field elements.
Note that the field size is approximately 254 bits, so a field element can store
31 bytes of data but cannot store 32 bytes. Hence we have to split up our data
into 31 bytes "hash chunks", then encode these as field elements. We will use
little-endian byte convention to get from 31 bytes to the standard form of
a field element, that is, the 31 little-endian bytes encode the number a
where 0 <= a < 2^248 < r < 2^254 is the standard representation of a field element.
For padding the last field element use the so-called 10* strategy: That means
always append a single 0x01 byte, and then pad with the minimum number
of zero bytes so that the final padded length is a multiple of 31.
It's probably better to choose the standard representation of field elements, because most standard tools like circom use that; even though choosing the Montgomery form would be a tiny bit more efficient (but the difference is very small, the hashing will dominate the costs anyway).
Poseidon2 offers essentially two API functions: a so called compression function which takes 2 field elements and returns 1; this can be used to build binary Merkle trees. And a more complex sponge construction for linear hashing, which can hash an arbitrary sequence of field elements into a single (or several) field element(s).
The sponge can have versions with different "rate" parameters, and the compression function is more generally a parametric family of functions, which I call a keyed compression function.
While we could always use a Merkle tree instead of the sponge, in the sponge
construction we can use rate = 2 with a target of 128-bit security level, which
in practice means twice as fast; so we should use that for hashing the cells.
Conventions to decide:
- padding (especially important for
rate > 1) - conversion from bytes to field elements (see above)
- initialization vector
We propose again the padding strategy 10* (but here we are talking about field
elements, not bytes!), and an initialization vector (0,0,domSep) where domSep
(short for "domain separation"), the initial value for the "capacity" part of the
sponge, is defined as
domSep := 2^64 + 256*t + rate
Parameters should be set based on bechmarks and other external constraints, but already we can have some preliminary targets. If we use a slot Merkle tree of depth between 16-32, and sponge hash with a rate of 2, then the Merkle inclusion proof cost will be approximately in balance with the cell hashing cost if the cell size is 1024-2048 bytes (34-67 field elements).
If we use 2048 byte cells, then nCells = 8192*8192 = 2^26 gives a slot size
of 128 Gb, which looks like a good compromise target slot size (we don't want
it to be too small, because then the number of slot proofs per node will be
too big; but we don't want it to be too big either, because that's inflexible).
The maximum slot size with cell size of 2048 and a depth of 32 (corresponding
to 2D erasure code is of size 2^16 x 2^16, see below) is 2^(32+11) = 2^43 = 8 Tb.
We need to use 2D erasure coding inside a slot, because while 1D would be better,
the required K,N parameters of the EC would be too big. Furthermore, we don't
want too big storage overhead, so the idea is to use K ~= 2/3 * N
(with N being a power of two). With such a setting, we can store the
original K x K matrix and the small (N-K) x (N-K) matrix, and reconstruct
the rest real-time. This particular parameter setting gives us a storage overhead
of 25% (of course we can tune the parameters, this is just an example).
Note that the EC rate does not affect the proof system itself, only the required number of samples to achieve a given target detection probability.
With the above setting (EC rate = 2/3), we need 117 samples to achieve 6 nines
of detection probability. Sampling a single 2048 cell with sponge rate 2
means approx 34 Poseidon2 permutation calls, while computing the root of
a depth 26 Merkle path is another 26 such calls. Finally computing the index
needs 2 calls and an extra cost similar to approx 3 calls, so we have about
65 calls per sample, each about 250 constraints. So in total we have about
117 * 65 * 250 ~= 1.9 million constraints, or equivalent to hashing about
235 kb of data with a binary Merkle tree or with a sponge of rate 1.
Given a slot of a dataset, we want to check nSamples randomly selected
cells, to see whether they are still stored by the node. We expect nSamples
to be in the range 20-200.
To be able to do this, we need to compute:
- the indices of the selected cells (or Merkle leaves)
- the hashes of the selected cells
- the Merkle paths from these hashes up to the slot root (Merkle proofs)
- the number of cells in the slot (this is because of our particular Merkle tree construction, but we will need it anyway to compute the indices)
- the (single) Merkle path from the slot root to the dataset root.
To be able to sample randomly, we need some external source of entropy; for
this, presumably a block hash of some public blockchain (eg. Ethereum) will
be used. It can be convenient to have the entropy in the form a field element;
for this we can simply take the block hash modulo r. While this gives a
somewhat non-uniform probability distribution, in practice this should not
cause any issue. Alternatively, we could just keep 31 bytes of the block hash and
interpret it as a field element, giving 248 bits of uniform entropy.
We propose the following function to compute the indices of the selected cells:
idx = H( entropy | slotRoot | counter ) `mod` nCells
where counter iterates over the range [1..nSamples], H is our hash
function (right now Poseidon2 sponge with rate = 2 and 10* padding strategy),
and | denotes concatenation (in this case the input is just 3 field elements).
For the MVP, we build a monolithic circuit / R1CS instance for proving all the samples in single slot; then use Groth16 to prove it.
Public inputs:
- dataset root
- slot index within the dataset
- entropy (public randomness)
Private inputs:
- the slot root
- number of cells in the slot
- the number of slots in the dataset
- the underlying data of the cells, as sequences of field elements
- the Merkle paths from the leaves (the cell hashes) to the slot root
- the Merkle path from the slot root to the dataset root
Computation:
- compute the cell indices from the slot root and the entropy
- compute the cell hashes from the cell data
- from the cell hashes, using the provided Merkle paths, recompute the slot root
- compare the reconstructed slot root to the slot root given as private input
- from the slot root, using the provided Merkle path, recompute and check the dataset root
Note that given the index of a leaf, we can compute the left-right zig-zag of the corresponding Merkle path, simply by looking at the binary decomposition. So the Merkle paths will only consist lists of hashes.
We use the same "safe" Merkle tree construction across the codebase. This uses a "keyed compression function", where the key depends on:
- whether we are in the bottommost layer or not
- whether the node we are dealing with has 1 or 2 children (odd or even node)
These are two bits, encoded as numbers in the set {0,1,2,3} (the lowest bit is
1 if it's the bottom layer, 0 otherwise; the next bit is 1 if it's an odd node,
0 if even node). Furthermore:
- in case of an odd node with leaf
x, we apply the compression to the pair(x,0) - in case of a singleton input (the whole Merkle tree is built on a single field element), we also apply one compression
- the keyed compression is defined as applying the permutation to the triple
(x,y,key), and extracting the first component of the resulting triple
In case of SHA256, we could use a compression functions of the form
SHA256(x|y|key), where x,y are 32 byte long hashes, and key is a single
byte. Since SHA256 already does some padding internally, this has the same
cost as computing just SHA256(x|y).
The networking layer uses 64kb "blocks", while the proof layer uses 2kb "cells". To make these compatible, the way we define a hash of a 64kb block is:
- split the 64kb data into 32 smaller 2kb cells;
- hash these cells (with Poseidon2 sponge, rate=2, and
10*padding); - build a depth 5 complete binary Merkle tree on those hashes, with the above conventions. The resulting Merkle root will be the hash of the 64kb block.
Then we build a big Merkle tree on these block hashes, again with the above conventions, resulting in the slot root.