$\index_l: [\lfloor N_\nodes / 2^l \rfloor] \equiv [\len(\BinTree\dot\layer_l)]$ The index of a node in a $\BinTree$ layer $l$. The leftmost node in a tree has $\index_l = 0$. For each tree layer $l$ (excluding the root layer) a Merkle proof verifier calculates the label of the node at $\index_l$ from a single Merkle proof path element $\BinTreeProof_c\dot\path[l - 1] \thin$.
BinTreeProofs
The method $\BinTree\dot\createproof$ is used to create a Merkle proof for a challenge node $c$.
Line 5: Calculates the node index in layer $l$ of the node that the verifier calculated using the previous lath element (or the $\BinTreeProof_c\dot\leaf$ if $l = 0$). Note that $c \gg l \equiv \lfloor c / 2^l \rfloor \thin$.
OctTreeProofs
The method $\OctTree\dot\createproof$ is used to create a Merkle proof for a challenge node $c$.
Additional Notation:
$\index_l: [\lfloor N_\nodes / 8^l \rfloor] \equiv [\len(\OctTree\dot\layer_l)]$ The index of a node in an $\OctTree$ layer $l$. The leftmost node in a tree has $\index_l = 0$. For each tree layer $l$ (excluding the root layer) a Merkle proof verifier calculates the label of the node at $\index_l$ from a single Merkle proof path element $\OctTreeProof_c\dot\path[l - 1] \thin$.
$\textsf{first\_sibling}_l \thin, \textsf{last\_sibling}: [\lfloor N_\nodes / 8^l \rfloor]$ The node indexes in tree layer $l$ of the first and last nodes in this layer's Merkle path element's siblings array $\OctTreeProof_c\dot\path[l]\dot\siblings \thin$.
Line 5: Calculates the node index in layer $l$ of the node that the verifier calculated themselves using the previous path element (or $\OctTreeProof_c\dot\leaf$ if $l = 0$). Note that $c \gg (3 * l) \equiv \lfloor c / 8^l \rfloor \thin$.
Line 7-8: Calculates the indexes in tree layer $l$ of the first and last (both inclusive) Merkle hash inputs for layer $l$'s path element.
Line 9: Copies the 7 Merkle hash inputs that will be in layer $l$'s path element $\OctTreeProof\dot\path[l]\dot\siblings \thin$.
Proof Root Validation
The functions $\bintreeproofisvalid$ and $\octtreeproofisvalid$ are used to verify that a $\BinTreeProof\dot\path$ or an $\OctTreeProof\dot\path$ hash to the root found in the Merkle proof $\BinTreeProof\dot\root$ and $\OctTreeProof\dot\root$ respectively.
Note that these functions do not verify that a $\BinTreeProof\dot\path$ or an $\OctTreeProof\dot\path$ correspond to the expected Merkle challenge $c$. To verify that a proof path is consistent with $c$, see the psuedocode functions $\calculatebintreechallenge$ and $\calculateocttreechallenge$.
The function $\octtreeproofisvalid$ can receive as the type of its $\proof$ argument either an $\OctTreeProof$ or $\ColumnProof$ (a $\ColumnProof$ is just an $\OctTreeProof$ with an adjoined field $\column$, $\ColumnProof_c \equiv \OctTreeProof_c \cup \column_c \thin$).
Given a Merkle path $\path$ in a $\BinTree$ or $\OctTree$, $\calculatebintreechallenge$ and $\calculateocttreechallenge$ calculate the Merkle challenge $c$ for which the Merkle proof $\path$ was generated.
Given a Merkle challenge $c$ and its path in a $\BinTree$ or $\OctTree$, the concatentation of the $\missing$ bits (or octal digits) in the Merkle path is the little-endian binary (or octal) representation of the integer $c \thin$:
$\path = \BinTreeProof\dot\path$$\path = \OctTreeProof\dot\path$ The $\path$ argument is the path field of a $\BinTreeProof$ or $\OctTreeProof$.
$c: \NodeIndex$ The challenge corresponding to $\path$.
$l \in [\BinTreeDepth]$$l \in [\OctTreeDepth]$ A path element's layer in a Merkle tree (the layer in the tree that contains the path elements $\siblings$). Layer $l = 0$ is the leaves layer of the tree. Here, values for $l$ do not include the root layer $l \neq \BinTreeDepth, \OctTreeDepth \thin$.
Filecoin utilizes the topological properties of depth robust graphs (DRG's) to build a sequential and regeneration resistant encoding scheme. We stack $N_\layers$ of DRG's, each containing $N_\nodes$ nodes, on top of one another and connect each adjacent pair of DRG layers via the edges of bipartite expander. The source layer of each expander is the DRG at layer $l$ and the sink layer is the DRG at layer $l + 1$. The resulting graph is termed a Stacked-DRG.
For every node $v \in [N_\nodes]$ in the DRG at layer $l \in [N_\layers]$, we generate $d_\drg$ number of DRG parent for $v$ in layer $l$. DRG parents are generated using the Bucket Sampling algorithm. For every node $v$ in layers $l > 0$ we generate $d_\exp$ number of expander parents for $v$ where the parents are in layer $l - 1$. Expander parents are generated using a psuedorandom permutation (PRP) $\pi: [N_\nodes] \rightarrow [N_\nodes]$ which maps a node in the DRG layer $l$ to a node in the the DRG layer $l - 1$. The psudeorandom permutation is generated using a $N_\feistelrounds$-round Feistel network whose round function is the keyed hash function $\Blake$, where round keys are specified by the constant $\FeistelKeys$.
DRG
The function $\getdrgparents$ are used to generate a node $v$'s DRG parents in the Stacked-DRG layer $l_v \thin$. The set of DRG parents returned for $v$ is the same for all PoRep's of the same PoRep version $\PorepID$.
$v, u: \NodeIndex$ DRG child and parent node indexes respectively. A DRG child and its parents are in the same Stacked-DRG layer $l$.
$\mathbf{u}_\drg: \NodeIndex^{[d_\drg]}$ The set of $v$'s DRG parents.
$v_\meta, u_\meta: [d_\meta * N_\nodes]$ The indexes of $v$ and $u$ in the metagraph.
$\rng_{\PorepID, v}$ The RNG used to sample $v$'s DRG parents. The RNG is seeded with the same bytes $\DrgSeed_{\PorepID, v}$ every time $\getdrgparents$ is called for node $v$ from a PoRep having version $\PorepID$.
$x \xleftarrow[\rng]{} S$ Samples $x$ uniformly from $S$ using the seeded $\rng$.
$b: [1, N_\buckets + 1]$ The Bucket Sampling bucket index. Bucket indexes start at 1.
$\dist_{\min, b}$$\dist_{\max, b}$ The minimum and maximum parent distances in bucket $b$.
$\dist_{u_\meta}$ The distance $u_\meta$ is from $v_\meta$ in the metagraph.
The function $\getexpparents$ is used to generate a node $v$'s expander parents in the Stacked-DRG layer $l_v - 1 \thin$. The set of expander parents returned for a node $v$ is the same for all PoRep's of the same version $\PorepID$.
$v, u: \NodeIndex$ Expander child and parent node indexes respectively. Each expander parent $u$ is in the Staked-DRG layer $l - 1$ that precedes the child node $v$'s layer $l$.
$\mathbf{u}_\exp: \NodeIndex^{[d_\exp]}$ The set of $v$'s expander parents.
$e_l \thin, e_{l - 1}: \ExpEdgeIndex$ The index of an expander edge in the child $v$'s layer $l$ and the parent $u$'s layer $l - 1$ respectively. An expander edge connects edge indexes $(e_{l - 1}, e_l)$ in adjacent Stacked-DRG layers.
The function $\feistel$ runs an $N_\feistelrounds$ round Feistel network as a psuedorandom permutation (PRP) over the set of expander edges $[d_\exp * N_\nodes] = [2^{33}]$ in a Stacked-DRG layer.
$\input, \output$ The Feistel network's input and output blocks respectively. The $\input$ argument and the returned $\output$ are guaranteed to be valid $\u{33}$ expander edge indexes, however their intermediate values may be $\u{34}$.
$\u{64}_{(17)}$ An unsigned 64-bit integer whose lowest 17 bits are utilized. The integer's 17 least significant bits are used and may be $0$ or $1$, while the integer's 47 most significant bits are $0$ and are not used.
$\left_r, \right_r$ The left and right halves of round $r$'s input block.
$\left_{r + 1}, \right_{r + 1}$ The left and right halves of the next round's $r + 1$ input block.
$\FeistelKeys_\PorepID$ Is the set of constant round keys associated with the PoRep version $\PorepID$ that called $\feistel$.
$\key_r$ Round $r$'s key.
$\digestright$ The $\ell_\mask^\bit = 17$ least significant bits of a round's Blake2b $\digest$.
Line 1: Loops forever until the $\textsf{return}$ statement is reached (loops until $\output$ is a valid $\ExpEdgeIndex$).
Lines 13-14: Checks if $\output$ is a valid $\ExpEdgeIndex$ (true iff. the most-significant bit, the 34th bit, is 0), otherwise the Feistel network is rerun.
Line 15: Signifies that the next Feistel network's input has it's most-significant, its 34th bit, set to 1 (as opposed to the argument $\input: \ExpEdgeIndex \equiv \u{64}_{(33)}$, which does not have its 34th bit set).
All Parents
The function $\getallparents$ returns a node $v$'s set of DRG parents concatenated with its set of expander parents. The set of parents returned for $v$ is the same across all PoRep's of the same PoRep version $\PorepID$.
The labeling function for every node in a Stacked-DRG is $\Sha{254}$ producing a 254-bit field element $\Fqsafe$. A unique preimage is derived for each node-layer tuple $(v, l)$ in replica $\ReplicaID$'s Stacked-DRG.
The labeling preimage for the first node $v_0 = 0$ in every Stacked-DRG layer $l \in [N_\layers]$ for a replica $\ReplicaID$ is defined:
The function $\textsf{generate\_labels}$ describes how every Stacked-DRG node is labeled for a replica. Nodes in the first layer $l_0 = 0$ are labeled using only DRG parents' labels, nodes in every subsequent layers $l > 0$ are labeled using both their DRG and expander parents' labels. The first node $v_0$ in every layer is not labeled using parents.
Additional Notation:
$\Labels_R$ Denotes that $\Labels$ is the labeling for a single replica $R$.
$l_0 = 0$ The constant $l_0$ is used to signify the first Stacked-DRG layer.
$l_v$ The Stacked-DRG layer in which a node $v$ resides.
$\Label_{v, l_v}$ The label of node $v$ in the Stacked-DRG layer $l_v$.
$u_{\langle \drg | \exp \rangle}$ Denotes that parent $u$ may be a DRG or expander parent.
$\Label_{u_\drg}$ The label of a DRG parent (in $v$'s layer $l$).
$\Label_u \equiv \or{\Label_{u_\drg, l_v}}{\Label_{u_\exp, l_v - 1}}$ The label of either a DRG or expander parent (in layer $l$ or $l - 1$ respectively).
Lines 4-6: Label the remaining Stacked-DRG layers.
The function $\labelwithdrgparents$ is used to label a node $v$ in the first Stacked-DRG layer $l_0 = 0 \thin$.
The label of each node $v$ in $l_0$ is dependent on the labels of $v$'s DRG parents (where $v$'s DRG parents are in layer $l_v = l_0 \thin$. $v$'s DRG parents always come from the node range $[v]$ in layer $l_v$, thus we pass in the argument $\Labels[l_0][..v]$ which contains the label of every node up to $v$ in $l_0 \thin$. $\Labels[l_0][..v]$ is guaranteed to be labeled up to node $v$ because $\labelwithdrgparents$ is called sequentially for each node $v \in [N_\nodes] \thin$.
The function $\labelwithallparents$ is used to label a node $v$ in all layers other than the first Stacked-DRG layer $l_v > 0 \thin$.
The label of a node $v$ in layers $l_v > 0$ is dependent on both the labels of $v$'s DRG and expander parents. $\labelwithallparents$ takes the argument $\Labels[l_v][..v]$ (the current layer $l_v$ being labeled, contains labels up to node $v$) to retrieve the labels of $v$'s DRG parents and the argument $\Labels[l_v - 1]$ (the previous layer's labels) to retrieve the labels of $v$'s expander parents.
The column commitment process is used commit to a replica's labeling $\Labels$. The column commitment $\CommC$ is generated by building an $\TreeC: \OctTree$ over the labeling matrix $\Labels$ and taking the tree's root.
To build a tree over the matrix $\Labels$ we hash each of its $N_\nodes$ number of columns (where each column contains $N_\layers$ number of $\Label$'s) using the hash function $\Poseidon_{11}$ producing $N_\nodes$ number of column digests. The $i^{th}$ column digest is the $i^{th}$ leaf in $\TreeC$.
Encoding is the process by which a sector $D: \Safe^{[N_\nodes]}$ is transformed into its encoding $R: \Fqsafe^{[N_\nodes]}$. The encoding function is node-wise prime field addition $\oplus$, where "node-wise" means that every distinct $\Safe$ slice $D_i \in D$ is discretely encoded.
$D$ is viewed as an array of $N_\nodes$ distinct byte arrays $D_i: \Safe$. Sector preprocessing ensures that each $D_i$ is a valid $\Safe$ (represents a valid 254-bit or less field element $\Fqsafe)$.
A unique encoding key $K$ is derived for every distinct $\ReplicaID$ via the PoRep labeling process producing $\Labels$. Each $D_i \in D$ is encoded by a distinct encoding key $K_i \in K$, where $K_i$ is $i^{th}$ node's label in the last Stacked-DRG layer.
$D$ is encoded into $R$ via node-wise field addition. Each $D_i \in D$ is interpreted as a field element and encoded into $R_i$ by adding $K_i$ to $D_i$. The resulting array of field elements produced via field addition is the encoding $R$ of $D$.
Replication is the entire process by which a sector $D$ is uniquely encoded into a replica $R$. Replication encompasses Stacked-DRG labeling, encoding $D$ into $R$, and the generation of trees $\TreeC$ over $\Labels$ and $\TreeR$ over $R$.
A miner derives a unique $\ReplicaID$ for each $R$ using the commitment to the replica's sector $\CommD = \TreeD\dot\root \thin$ (where $\TreeD$ is build over the nodes of the unencoded sector $D$ associated with $R \thin$).
Given a sector $D$ and its commitment $\CommD$, replication proceeds as follows:
Generate the $R$'s unique $\ReplicaID$.
Generate $\Labels$ from $\ReplicaID$, thus deriving the key $K$ that encodes $D$ into $R$.
Generate $\TreeC$ over the columns of $\Labels$ via the column commitment process.
Encode $D$ into $R$ using the encoding key $K$.
Generate a $\TreeR: \OctTree$ over the replica $R$.
Commit to $R$ and its associated labeling $\Labels$ via the commitment $\CommCR$.
The function $\replicate$ runs the entire replication process for a sector $D$.
The function $\createreplicaid$ describes how a miner having the ID $\ProverID$ is able to generate a $\ReplicaID$ for a replica $R$ of sector $D$, where $D$ has a unique ID $\SectorID$ and commitment $\CommD$. The prover uses a unique random value $\R_\ReplicaID$ for each $\ReplicaID$ generated.
A sector $D$ is constructed from Filecoin client data where the aggregating of client data of has been preprocessed/bit-padded such that two zero bits are placed between each distinct 254-bit slice of client data. This padding process results in a sector $D$ such that every 256-bit slice represents a valid 254-bit field element $\Safe \thin$.
A Merkle tree $\TreeD: \BinTree$ is constructed for sector $D$ whose leaves are the 256-bit slices $D_i: \Safe \in D \thin$.
A PoRep prover generates a $\PorepPartitionProof_k$ for each partition $k$ in a replica $R$'s batch of PoRep proofs. Each partition proof is generated for $N_{\porepchallenges / k}$ number of challenges, the challenge set $\PorepChallenges_{R, k}$ (each partition proof's challenge set is specific to the replica $R$ and partition $k$).
A single partition proof generated by a PoRep prover shows that:
The prover knows a valid Merkle path for $c$ in $\TreeD$ that is consistent with the public $\CommD$.
The prover knows valid Merkle paths for $c$ in trees $\TreeC$ and $\TreeR$ which are consistent with the committed to $\CommCR$.
The prover knows $c$'s labeling in each Stacked-DRG layer $\Column_c = \ColumnProof_c\dot\column \thin$ by hashing $\Column_c$ into a leaf in $\TreeC$ that is consistent with $\CommCR$.
For each layer $l$ in the Stacked-DRG, the prover knows $c$'s labeling preimage $\ParentLabels$ (taken from the columns in $\ParentColumnProofs$), such that the parent labels are consistent with $\CommCR$.
The prover knows the key $K_c$ used to encode $D_c$ into $R_c$ (where $D_c$, $K_c$, and $R_c$ were already shown to be consistent with the commitments $\CommD$ and $\CommCR$).
$\createlabel_\V$ Designates the function $\createlabel$ as being used by a PoRep verifier $\V$.
$c: \NodeIndex \setminus 0$ The node index of a PoRep challenge. The first node 0 is never challenged in PoRep proofs.
$d = \big[ \tern{l_c = 0}{d_\drg}{d_\total \big]}$ The number of parents that challenge $c$ has (where $c$ is in the layer $l_c$).
$\Label_{c, l}^\dagger: \Fqsafe$ The label of the challenge node $c$ in layer $l$ calculated from the unverified $\ParentColumnProofs^\dagger$.
$\Label_{u_\exp, l - 1}: \Fqsafe$ The label of challenge $c$'s expander parent $u_\exp$ in layer $l - 1$. Expander parents come from the layer prior to $c$'s layer $l$.
$p_\drg \in [d_\drg]$ $p\total \in [d\total]$ The index of a parent in $c$'s parent arrays $\mathbf{u}_\drg$ and $\mathbf{u}_\total$ respectively.
$u_\drg, u_\exp: \NodeIndex$ The node index of a DRG or expander graph parent for $c$.
$\parentlabels': \Label^{[N_\parentlabels]}$ The set of parent labels repeated until its length is $N_\parentlabels$.
$\PorepPartitionProof_{R, k}$ The $k^{th}$ PoRep partition proof generated for the replica $R$.
$\treedleaf_{\auxb, c}$ The circuit value for a challenge $c$'s leaf in $\TreeD$.
$\calculatedcommd_{\auxb, c}$ The circuit value calculated for $\CommD$ using challenge $c$'s $\TreeDProof_c$.
$\column_{[\auxb], u}$ The array circuit values representing a parent $u$ of challenge $c$'s label in each Stacked-DRG layer.
$\parentcolumns_{[[\auxb]], \mathbf{u}_\total}$ An array of an array of circuit values, the allocated column for each parent $u \in \mathbf{u}_\total \thin$.
$l_c$ The challenge $c$'s layer in the Stacked-DRG.
$\parentlabelsbits_{[[\auxb + \constb, \lebytes]]}$ An array where each element is a parent $u$'s label, an array of allocated and unallocated bits $_{[\auxb + \constb]}$ having $\lebytes$ bit order.
$\calculatedlabel_{\auxb, c, l}$ The label calculated for challenge $c$ in residing in layer $l$.
Lines 9-10: Computes $\CommCR^\dagger$ within the circuit from the witnessed commitments and assert that $\CommCR^\dagger$ is equal to the public input $\CommCR$.
Lines 15-16: Adds the packed challenge $c$ as a public input, used when calculating each challenge $c$'s column within the circuit.
Lines 17-19: Verifies $c$'s $\TreeDProof_c$ by computing $\CommD_c^\dagger$ within the circuit and asserting that it is equal to the public input $\CommD$.
Lines 20-26: Allocates each of $c$'s parent's $u \in \mathbf{u}_\total$ label and checks that $u$'s $\ColumnProof_u$ is consistent with the previously verified $\CommC^\dagger \mapsto \CommC \thin$.
Lines 27-44: Calculates challenge $c$'s label in each Stacked-DRG layer $l$ within the circuit using each parent's allocated column.
Lines 45-46: Verifies that $c$'s $\TreeRProof_c$ is consistent with the previously verified $\CommR^\dagger \mapsto \CommR$.
Lines 47-48: Checks that the calculated encoding key $K_c^\dagger$ for $c$ encodes the previously verified sector and replica tree leaves $D_c^\dagger \mapsto D_c$ into $R_c^\dagger \mapsto R_c$.
Lines 49-51: Verifies $c$'s $\ColumnProof_c$ against the previously verified $\CommC$.
PoSt Challenges
The function $\getpostchallenge$ is used to derive a Merkle challenge for a Winning or Window PoSt proof.
$\R_{\postchallenges, \batch \thin \aww}$ A random value used to derive the challenge set for each of a PoSt prover's partition proofs in their current Winning or Window PoSt proof batch.
$\SectorID$ The ID for the sector $D$ associated with the replica $R$ for which this Merkle challemnge is being generated.
$\challengeindex_\batch$ The unique index of a Merkle challenge across all PoSt partition proofs that a PoSt prover is generating. For all partition proofs in the same PoSt batch, every Merkle challenge across all replicas will have a unique $\challengeindex_\batch \thin$.
$\nreplicas_k$ The number of distinct replicas that the prover has for this PoSt partition proof.
$\replicaindex_k$ $\replicaindex_\batch$ The index of a challenged replica $R$ in a partition $k$'s partition proof and the index of the challenged replica across all partition proofs that a prover is generating for batch.
$\challengeindex_R$ $\challengeindex_\batch$ The index of a Merkle challenge in a challenged replica $R$ and the index of the Merkle challenge across all partition proofs that a prover is generating for batch.
$\TreeR_R, \CommC_R, \CommCR_R, \TreeRProofs_R$ The subscript $_R$ denotes each of these values as being for the replica $R$ which is distinct within the prover's PoSt batch.
$\ell_\pad$ The number of non-distinct $\PostReplicaProof{\bf \sf s}$ that are added as padding to a PoSt prover's final partition proof in a batch.
Lines 13-15: If the prover does not have enough replicas to fill an entire PoSt partition proof, pad the partition proof with copies of the last distinct replica's $\PostReplicaProof_R \thin$.
$k: N_{\postpartitions / \batch, \P \thin \aww}$ The number of partitions in a Winning or Window PoSt batch is dependent on the length of the PoSt prover $\P$'s replica set.
$\nreplicas_k$ The number of distinct replicas that the prover has for this PoSt partition proof.
$\replicaindex_k$$\replicaindex_\batch$ The index of a challenged replica $R$ in a partition $k$'s partition proofs in a PoSt prover's batch.
$\challengeindex_R$$\challengeindex_\batch$ The index of a Merkle challenge in a challenged replica $R$ and the index of the Merkle challenge across all partition proofs in a PoSt prover's batch.
Line 13: The dagger is removed from $\CommR^\dagger$ (producing $\CommR$) because $\CommR^\dagger$ was verified to be consistent with the committed to $\CommCR$ (Line 8).
PoSt Circuit
The function $\createpostcircuit$ is used to instantiate a Winning or Window PoSt circuit.
Addional Notation:
$\PostPartitionProof_{k \thin \aww}$ The partition-$k$ proof in a PoSt prover's Winning or Window PoSt batch. $\PostPartitionProof_k$ Contains any padded $\PostReplicaProof{\bf \sf s}$.
$\TreeR_R, \CommC_R, \CommCR_R$ Each $\PostReplica_R \in \PostReplicas_{\P \thin \aww}$ represents a unique replica $R$ in the batch denoted by the subscript $_R \thin$.
$\TreeRProofs_R$ Each $\TreeRProofs$ is for a distinct replica $R$, denoted by the subscript $_R \thin$, in a PoSt batch.
The function $\bintreerootgadget$ calculates and returns a $\BinTree$ Merkle root from an allocated leaf $\leaf_\auxb$ and an unallocated Merkle $\path$. Both the leaf and path are from a Merkle challenge $c$'s proof $\BinTreeProof_c$, where $\path = \BinTreeProof_c\dot\path \thin$.
The gadget adds one public input to the constraint system for the packed Merkle proof path bits $\pathbits_\auxle$ which are the binary representation of the $c$'s DRG node-index $\llcorner c \lrcorner_{2, \Le} \equiv \pathbits_\auxle \thin$).
Line 9: A public input is added to $\cs$ for the Merkle challenge $c$ corresponding to the Merkle path which was used to calculate the returned root.
Line 10: The final value for $\curr_\auxb$ is the Merkle root calculated from $\leaf_\auxb$ and $\path$.
OctTree Root Gadget
The function $\octtreerootgadget$ calculates and returns an $\OctTree$ Merkle root from an allocated leaf $\leaf_\auxb$ and an unallocated Merkle $\path$. Both the leaf and path are from a Merkle challenge $c$'s proof $\OctTreeProof_c$, where $\path = \OctTreeProof_c\dot\path \thin$.
The gadget adds one public input to the constraint system for the packed Merkle proof path bits $\pathbits_\auxle$ which are the binary representation of the $c$'s DRG node-index $\llcorner c \lrcorner_{2, \Le} \equiv \pathbits_\auxle \thin$).
Note that the constant $3 = \log_2(8)$, the number of bits required to represent an index in the 8-element Merkle hash $\inputs$ array, is used at various times in the following algorithm.
Line 1: Not a reallocation of $\leaf_\auxb$ within $\cs$, but is an in-memory copy.
Lines 4-8: Witnesses the 3-bit missing index for each path element. The first iteration $i = 0$ corresponds to the least significant bit in $\missing$.
Lines 9-12: Witnesses each path element's 7 Merkle hash inputs (the exlucded 8-th Merkle hash input is the calculated hash input $\curr_\auxb$ for this tree depth).
Line 13: Creates the Merkle hash inputs array by inserting $\curr$ into $\siblings$ at index $\missing$.
Line 14: Hashes the 8 Merkle hash inputs.
Line 16: Adds the challenge $c$ as a public input.
Line 17: Returns the calculated root.
Encoding Gadget
The function $\encodegadget$ runs the $\encode$ function within a circuit. Used to encode $\unencoded_{\auxb, v}$ (node $v$'s sector data $D_v$) into $\encoded_{\auxb, v}$ (the replica node $R_v$) given an allocated encoding key $\key_{\auxb, v}$ ($K_v$).
The function $\createlabelgadget$ is used to label a node $\node$ in the Stacked-DRG layer $\layerindex$ given the node's expanded parent labels $\parentlabels$.
$\replicaid_{[\auxb + \constb, \lebytes]}$ The allocated bits (and constant zero bit(s)) representing a $\ReplicaID$.
$\layerindex_{[\auxb, \Le]}$ The allocated bits representing a layer $l \in [N_\layers]$ as an unsigned 32-bit integer.
$\node_{[\auxb, \Le]}$ A node index $v \in [N_\nodes]$ allocated as 64 bits.
$\parentlabels_{[[\auxb + \constb, \lebytes]]}$ An array containing $N_\parentlabels$ allocated bit arrays, where each bit array is the label of one of $\node$'s parents.
Lines 4-5: The constant $256 = \ell_\block^\bit \thin$.
Lines 5-6: These are not reallocations.
Lines 6-7: The labeling function is $\Sha{254}$ not $\Sha{256}$.
Lines 6,9: The constant $254 = \ell_{\Fq, \safe}^\bit \thin$.
Little-Endian Bits Gadget
The function $\lebitsgadget$ receives a value $\value$ allocated within a constraint system $\cs$ and reallocates it as its $n$-bit little-endian binary representation.
Note that the number of bits returned must be at least the number of bits required to represent $\value$: $0 < \lceil \log_2(\value\dot\int) \rceil \leq n \thin$.
Line 2: This will pad $n - \lceil \log_2(\value\dot\int) \rceil$ zero bits onto the most significant end of $\llcorner \int \lrcorner_{2, \Le} \thin$.
Pack Bits as Input Gadget
The function $\packbitsasinputgadget$ receives an array of $n$ allocated little-endian bits $\bits_{[\auxb, \Le]}$, where $0 < n \leq \ell_\Fqsafe^\bit \thin$, and creates the field element $\packed$ whose little-endian binary representation is that of $\bits$. The gadget adds one public input $\packed_\pubb$ to the constraint system for the created field element.
The $\pickgadget$ is used to choose one of two allocated values, $\x$ and $\y$, based upon the value of a binary condition $\bit$.
If $\bit$ is set, the gadget will reallocate and return $\x$, otherwise if $\bit$ is not set, the gadget will reallocate and return $\y$.
The $\pickgadget$, when given two allocated values $\x, \y \in \Fq$ and an allocated boolean constrained value $\bit \in \Bit$, outputs the allocated value $\pick \in \{ \x, \y \}$ and adds the $\RCS$ quadratic constraint:
$\bi (\y - \x) * (\bit) = (\y - \pick)$
This table shows that for $\bit \in \Bit$ and $\x, \y \in \Fq$ that the constraint is satisfied for the outputted values of $\pick$.
The $\insertgadget{2}$ inserts $\value$ into an array $\arr$ at index $\index$ and returns the inserted array of reallocated elements.
The gadget receives an array containing one allocated element $\arr[0]$ and a second allocated value $\value$ and returns the two element array containing the reallocations of the two values where the index of the reallocated $\value$ is at the index $\index$ argument in the returned 2-element array.
The function $\insertgadget{8}$ inserts a value $\value$ into an array of 7 elements $\arr$ at index in the 8 element array given by $\indexbits$. The values returned in the 8-element array are reallocations of $\arr$ and $\value$.
Note that the length of the $\indexbits$ argument is $3 = \log_2(8)$ bits, which is the number of bits required to represent an index in an array of 8 elements.
Additional Notation:
$\arr'$ The inserted array containing 8 reallocated values, the elements of the uninserted array $\arr$ and the insertion value $\value$.
$\nor_{\auxb \thin (b_0, b_1)}$ Set to true if neither $\indexbits[0]$ nor $\indexbits[1]$ are $1$.
$\and_{\auxb \thin (b_0, b_1)}$ Set to true if both $\indexbits[0]$ and $\indexbits[1]$ are $1$.
The pick for the $i^{th}$ element of the inserted array based upon the value of the first bit (least-significant), first and second bits, and the first, second and third bits respectively.
For ease of notation the subscripts $_\auxb$ and $_\aap$ are left off everywhere except in the function signature and when allocating of a value within the circuit.
The function $\andgadget$ returns an allocated bit $1$ if both allocated bit arguments $\x$ and $\y$ are $1$ and returns the allocated bit $0$ otherwise.
The $\RCS$ quadratic constraint that is added by the $\andgadget$, when applied to two boolean constrained values $\x, \y \in \Bit$ and outputting a third boolean constrained value $\and \in \Bit$, is:
$\bi (\x) * (\y) = (\and)$
This table shows the satisfiablilty of the constraint for all values of $\x, \y \in \Bit$ and corresponding outputted values of $\and \in \Bit$.
The function $\norgadget$ returns an allocated bit $1$ if both allocated bit arguments $\x$ and $\y$ are $0$ and returns the allocated bit $0$ otherwise.
The $\RCS$ quadratic constraint that is added by $\norgadget$, when applied to two boolean constrained values $\x, \y \in \Bit$ and outputting a third boolean constrained value $\nor \in \Bit$, is:
$\bi (1 - \x) * (1 - \y) = (\nor)$
The following table shows the satisfiablilty of the constraint for all values of $\x, \y \in \Bit$ and corresponding outputted values for $\nor \in \Bit$.