$$
\newcommand{\postwo}[0]{\text{Poseidon2}}
$$

# Proofs in Codex

We start by taking apart the code that builds general Merkle trees, and then looking into the bits that are specialized for proof trees - namely the `SlotBuilder` and the code that builds fine-grained, per-block "cell" trees.

## Building Merkle Trees

Our Merkle trees use leaf domain separation to avoid "second preimage" (or, more aptly named, ["node-as-leafs"](https://www.rareskills.io/post/merkle-tree-second-preimage-attack)) attacks. The code snippet which computes the nodes at height $k + 1$ from the nodes at height $k$ is shown below. Trees are built from the bottom (height $0$) up (height $=$ depth).

func merkleTreeWorker*[H, K](
  self: MerkleTree[H, K],
  xs: openArray[H],
  isBottomLayer: static bool): ?!seq[seq[H]] =

  let a = low(xs)
  let b = high(xs)
  let m = b - a + 1

  when not isBottomLayer:
    if m == 1:
      return success @[ @xs ]

  let halfn: int  = m div 2
  let n    : int  = 2 * halfn
  let isOdd: bool = (n != m)

  var ys: seq[H]
  if not isOdd:
    ys = newSeq[H](halfn)
  else:
    ys = newSeq[H](halfn + 1)

  for i in 0..<halfn:
    const key = when isBottomLayer: K.KeyBottomLayer else: K.KeyNone
    ys[i] = ? self.compress( xs[a + 2 * i], xs[a + 2 * i + 1], key = key )
  if isOdd:
    const key = when isBottomLayer: K.KeyOddAndBottomLayer else: K.KeyOdd
    ys[halfn] = ? self.compress( xs[n], self.zero, key = key )

  success @[ @xs ] & ? self.merkleTreeWorker(ys, isBottomLayer = false)

This starts with establishing the number of elements $m$[^1] in the array at height $k$, in lines $11$-$13$. If we only have one element at level $k$ and this is not the "bottom layer" (i.e., the set of nodes at height $0$), then we simply return `xs` as is. For a tree of depth $d$, I claim that this will only happen when $k = d$.

To see why, let $n_k$ be the number of nodes at height $k$ in the tree; i.e. $n_0$ is the number of leaf nodes. Now note that, at each call, `merkleTreeWorker` reduces the number of nodes to $n_{k+1} = \lceil n_k / 2 \rceil$. It does that in a sort of a funny way from lines $14$ to $22$ by taking the division floor and summing one if that is not an exact division (i.e., it takes the ceiling), but that is what it does.

This means that, in a bounded number of steps which is $O\left(\log n_0\right)$, we will get to a point where $n_j = 1$ for some $j \geq 0$. Once that happens, we have two possibilities:

1. $j = 0$. If $j = 0$, it means the tree has only one leaf node, and `isBottomLayer` will be false. This will cause the node to be compressed with zero (line $29$), and lead to a second call to `merkleTreeWorker` containing a single node. That call will put us in case $(2)$ below.
2. $j > 0$. If $j > 0$, then we are not at the bottom layer, and the condition in line $10$ will be triggered, returning the input itself and ending the construction.

In both cases, the condition in line $10$ is only triggered once we get to the tree's root, which by construction implies $k = d$. $_\blacksquare$

Note that `merkleTreeWorker` will build a sequence of sequences, where each sequence corresponds to the nodes at a given height. The sequence at position $0$, therefore, will contain the leaves, whereas the last sequence will contain a single node which is the root node.

## Building Proof Trees

As we have seen above, the Merkle tree construction relies on:

* a sequence of leaf elements $L = \{l_1, \cdots l_n\}$ drawn from some set $L \subset E$;
* a compression function $f : E^2 \longrightarrow E$;
* a special zero element $e_0 \in E$.

With proof trees, $E$ is the set of valid $\postwo$ hashes, and leaf nodes are the $\postwo$ hashes taken over block _cells_, which are subdivisions of blocks, over an entire slot. We currently use $2\text{kB}$ cells in $64\text{kB}$ blocks, meaning $32$ cells per block. For slots with $j$ blocks, then, we will have $32 \times j$ cells, or $32 \times j$ leaf nodes in the proof tree.

### Building a Full Proof Tree (Uploader)

The uploader; i.e., the node requesting storage, will need to build a full proof tree for its dataset.

The way this works is that uploaders build a subtree per slot, and then compose those into a larger tree which will ultimately yield the verification root -- the $\postwo$ hash of this tree-of-subtrees. This is all orchestrated within the `buildSlots` proc, listed below:

proc buildSlots*[T, H](self: SlotsBuilder[T, H]): Future[?!void] {.async.} =
  ## Build all slot trees and store them in the block store.
  ##

  logScope:
    cid         = self.manifest.treeCid
    blockCount  = self.manifest.blocksCount

  trace "Building slots"

  if self.slotRoots.len == 0:
    self.slotRoots = collect(newSeq):
      for i in 0..<self.manifest.numSlots:
        without slotRoot =? (await self.buildSlot(i)), err:
          error "Failed to build slot", err = err.msg, index = i
          return failure(err)
        slotRoot

  without tree =? self.buildVerifyTree(self.slotRoots) and root =? tree.root, err:
    error "Failed to build slot roots tree", err = err.msg
    return failure(err)

  if verifyTree =? self.verifyTree and verifyRoot =? verifyTree.root:
    if not bool(verifyRoot == root): # TODO: `!=` doesn't work for SecretBool
        return failure "Existing slots root doesn't match reconstructed root."

  self.verifiableTree = some tree

  success()

At a high level, we can see the slot subtrees being built in lines $13$ -- $17$, followed by the "tree-of-subtrees" in line $19$ which uses the slot roots as leaf nodes.

Finally, we have some funny-looking piece of code in lines $23$ -- $25$. The `if` statement in line $23$ will be triggered if only if we have `verifyTree` set _and_ that `verifyTree` has a computed root[^2]. To understand where such a tree might have been set, we need to look into `SlotBuilder.new`:

  if manifest.verifiable:
    if manifest.slotRoots.len == 0 or
      manifest.slotRoots.len != manifest.numSlots:
      return failure "Manifest is verifiable but slot roots are missing or invalid."

    let
      slotRoots = manifest.slotRoots.mapIt( (? it.fromSlotCid() ))
      tree = ? self.buildVerifyTree(slotRoots)
      expectedRoot = ? manifest.verifyRoot.fromVerifyCid()
      verifyRoot = ? tree.root

    if verifyRoot != expectedRoot:
      return failure "Existing slots root doesn't match reconstructed root."

    self.slotRoots = slotRoots
    self.verifiableTree = some tree

In essence, if `SlotBuilder` is instantiated with a verifiable manifest, it will build the top-level verification tree (the one that has the slot roots as leafs) and set it to `verifiableTree`, as well as the slot roots into `slotRoots`. This will make it so that `buildSlots`:

1. does not call `buildSlot` for each slot;
2. checks that the tree root obtained from the slot roots match what was supplied.

This is used by storage nodes when they attempt to fill a slot, as we will see later.

### Slot and Block Subtrees

Slot subtrees, as we have seen before, are built by calls to `buildSlot`, listed next:

proc buildSlot*[T, H](
  self: SlotsBuilder[T, H],
  slotIndex: Natural): Future[?!H] {.async.} =
  ## Build a slot tree and store the proofs in
  ## the block store.
  ##

  logScope:
    cid         = self.manifest.treeCid
    slotIndex   = slotIndex

  trace "Building slot tree"

  without tree =? (await self.buildSlotTree(slotIndex)) and
    treeCid =? tree.root.?toSlotCid, err:
    error "Failed to build slot tree", err = err.msg
    return failure(err)

  trace "Storing slot tree", treeCid, slotIndex, leaves = tree.leavesCount
  for i, leaf in tree.leaves:
    without cellCid =? leaf.toCellCid, err:
      error "Failed to get CID for slot cell", err = err.msg
      return failure(err)

    without proof =? tree.getProof(i) and
      encodableProof =? proof.toEncodableProof, err:
      error "Failed to get proof for slot tree", err = err.msg
      return failure(err)

    if err =? (await self.store.putCidAndProof(
      treeCid, i, cellCid, encodableProof)).errorOption:
      error "Failed to store slot tree", err = err.msg
      return failure(err)

  tree.root()

This is somewhat straightforward; it:

1. builds the slot subtree (lines $14$ -- $17$);
2. iterates through the leafs and queries the tree for their inclusion proofs (lines $25$ -- $28$);
3. stores those proofs into the blockstore (lines $30$ -- $33$).

Peeling another layer, we see that `buildSlotTree` (below) builds a tree from cell hashes. Those are not, however, hashes of individual cells as the code may lead you to believe.

proc buildSlotTree*[T, H](
  self: SlotsBuilder[T, H],
  slotIndex: Natural): Future[?!T] {.async.} =
  ## Build the slot tree from the block digest hashes
  ## and return the tree.

  without cellHashes =? (await self.getCellHashes(slotIndex)), err:
    error "Failed to select slot blocks", err = err.msg
    return failure(err)

  T.init(cellHashes)

Instead, if we look at `getCellHashes`:

proc getCellHashes*[T, H](
  self: SlotsBuilder[T, H],
  slotIndex: Natural): Future[?!seq[H]] {.async.} =
  ## Collect all the cells from a block and return
  ## their hashes.
  ##

  let
    treeCid = self.manifest.treeCid
    blockCount = self.manifest.blocksCount
    numberOfSlots = self.manifest.numSlots

  logScope:
    treeCid = treeCid
    origBlockCount = blockCount
    numberOfSlots = numberOfSlots
    slotIndex = slotIndex

  let hashes = collect(newSeq):
    for i, blkIdx in self.strategy.getIndicies(slotIndex):
      logScope:
        blkIdx = blkIdx
        pos = i

      trace "Getting block CID for tree at index"
      without (_, tree) =? (await self.buildBlockTree(blkIdx, i)) and
        digest =? tree.root, err:
        error "Failed to get block CID for tree at index", err = err.msg
        return failure(err)

      trace "Get block digest", digest = digest.toHex
      digest

  success hashes

We get a rather different story: it actually builds the subtrees for each individual block separately (lines $217$ -- $230$), leaning on the index strategy to figure out which blocks to fetch. Needless to say, misalignments in indexing strategies among clients, or among uploader and clients, will cause proofs to fail as roots won't match.

### Merkle Proofs

Next, we look into the code which actually generates Merkle proofs. This is provided in the `getProof` proc, listed next.

func getProof*[H, K](
  self: MerkleTree[H, K],
  index: int,
  proof: MerkleProof[H, K]): ?!void =
  let depth   = self.depth
  let nleaves = self.leavesCount

  if not (index >= 0 and index < nleaves):
    return failure "index out of bounds"

  var path : seq[H] = newSeq[H](depth)
  var k = index
  var m = nleaves
  for i in 0..<depth:
    let j = k xor 1
    path[i] = if (j < m): self.layers[i][j] else: self.zero
    k =  k      shr 1
    m = (m + 1) shr 1

  proof.index = index
  proof.path  = path
  proof.nleaves = nleaves
  proof.compress = self.compress

  success()

The main piece of `getProof` relies in the index of the leaf $k$ for which we want to obtain a proof, the total number $m$ of leaves, and the depth of the tree, $d$.

The loop in lines $14$--$18$ then iterates from the top (root) to the bottom of the tree. To understand what that code does, we have to recall how a Merkle proof works. An example of a Merkle tree with a highlighted proof is provided in Figure 1.


**Figure 1.** A Merkle proof.

Suppose we wanted to get the Merkle proof for node $010$. The idea here is that we traverse the path upwards from $010$ and, for each node we encounter, we obtain its sibling.

The key thing to note here is that the index of the leaf already encodes the path to the leaf in the binary tree. If we want to know the immediate sibling for node $010$, therefore, all we need to do is flip the least significant bit; i.e., the last part of the path, and we will get the index of the sibling ($011$), and that is exactly what line $15$ does.

Since our trees are not balanced, it may well be that the sibling does not exist. Recall that when building the tree we were adding a "virtual" zero-valued sibling to every node without siblings, and so that is what we do again here: if the sibling is missing (i.e., the index does not exist), we add zero to the path (line $16$).

Finally, we update $k$ so we move onto the next layer by dropping the last bit of the path (with a right shift of $1$ byte in line $17$), and compute the number of nodes in the layer above with the following update rule. If we had $m_k$ nodes at layer $k$, then $m_{k + 1} = \left\lfloor \frac{m_k + 1}{2} \right\rfloor$.

To understand why this works, note that $m_k$ is either an even number, at which point we will get $m_{k + 1} = m_k / 2$ from the formula above, or it is odd, at which point we will be getting $m_{k + 1} = \frac{m_k + 1}{2}$ which accounts for the "virtual" zero-valued node that exists at layer $k$.

### Verification of Inclusion Proofs

Haven't reviewed this piece of code yet.

## Single-Block Slots

The tree construction process detailed so far implies that, under certain circumstances, you may see some strange-looking trees being built. One case this is true is when parameters induce single-block slots. Assuming a block had $8$ cells for simplicity (it currently has $32$), the slot tree would look something like what is in Figure 2.

<center>
<img src="https://hackmd.io/_uploads/SJilwwrwC.png" width="80%">
</center>

**Figure 2.** Proof tree for a single-block slot.

As we can see, the slot-level tree in these cases will always be highly unbalanced. In particular, the first element of the proof path will be always zero-valued as the sibling node of the root of the slot tree will always be a padding node (i.e., zero-valued).

# Data Sampling

The sampling algorithm extracts $k_s$ Merkle proofs that run from an individual cell all the way to the dataset root. Merkle proofs are built in $3$ stages (block level, slot level, dataset level) and must all match up, i.e.:

* the cell-level Merkle proof must verify wrt the corresponding leaf in the block root;
* the block-level proof must verify wrt the block root, and;
* the slot-level proof must verify wrt the dataset root.

Another key aspect is the actual cell selection process, which relies on an _entropy_ parameter received as an external output.

The entropy is a $32$-byte, padded array, which is constructed by first taking a $32$-byte random input, which should be a block hash. For slot index $i \in \mathbb{N}$, we pick the hash of the $i^{th}$ block before the current. In solidity:

function _getChallenge(uint8 pointer) internal view returns (bytes32) {
  bytes32 hash = blockhash(block.number - 1 - pointer);
  assert(uint256(hash) != 0);
  return keccak256(abi.encode(hash));
}

We then flip the last byte of this array to zeroes using "double truncation": the array is truncated to `31` bytes, then back to `32`. The reason for this is because the curve we use is defined over a $254$-bit prime field, meaning that the last portion of the last byte needs to be removed or the field element will not be in canonical form. This is done both inside of contracts, as part of verifying proofs:

function _challengeToFieldElement(
  bytes32 challenge
) internal pure returns (uint256) {
  // use only 31 bytes of the challenge to ensure that it fits into the field
  bytes32 truncated = bytes32(bytes31(challenge));
  // convert from little endian to big endian
  bytes32 bigEndian = _byteSwap(truncated);
  // convert bytes to integer
  return uint256(bigEndian);
}

and at the client, as part of computing and submitting proofs:

proc getProofInput*[T, H](
  self: DataSampler[T, H],
  entropy: ProofChallenge,
  nSamples: Natural): Future[?!ProofInputs[H]] {.async.} =
  ## Generate proofs as input to the proving circuit.
  ##

  let
    entropy = H.fromBytes(
      array[31, byte].initCopyFrom(entropy[0..30])) # truncate to 31 bytes, otherwise it _might_ be greater than mod
  # ...

at the client, this $31$-byte array gets converted into a $254$-bit field element which is interpreted as a Poseidon2 hash in line $9$. The sampler then uses:

* the entropy as a $\postwo$ hash, computed above;
* the $\postwo$ hash of the slot (not block) root;
* the total number of samples we intend to draw;
* a sample index $j$, $1 \leq j \leq k_s$.

And generates a corresponding cell index as follows:

func cellIndex*(
  entropy: Poseidon2Hash,
  slotRoot: Poseidon2Hash,
  numCells: Natural, counter: Natural): Natural =
  let log2 = ceilingLog2(numCells)
  doAssert( 1 shl log2 == numCells , "`numCells` is assumed to be a power of two" )

  let hash = Sponge.digest( @[ entropy, slotRoot, counter.toF ], rate = 2 )
  return int( extractLowBits(hash, log2) )

The interesting bit is in lines $8$, which uses the entropy, the slot root, and the sample index $j$ to compute yet another $\postwo$ hash (using the sponge construction), and then extract the lowest $\log_2(j)$ bits (which ensures a number $\leq$ `numCells`) to use as random cell index for sample index $j$.

[^1]: This is an awkward piece of code as it assumes $a$ can be different from zero. If $a$ could not be different from zero, then we could simply have ```let m = xs.len```

[^2]: I do not know under which circumstances we can have a tree without a root set. I suspect the answer may be "never", and that the second check performed there is unnecessary.