$$
\def\Fq{{\mathbb{F}_q}}
\def\Ftwo{{\mathbb{F}_2}}
\def\Zp{{\mathbb{Z}_p}}
\def\Zbin{{\mathbb{Z}_{2^m}}}
\def\thin{{\thinspace}}
\def\Byte{{\mathbb{B}}}
\def\Bit{{\{0, 1\}}}
\def\typecolon{\mathbin{\large :}}
\def\neg{{\text{-}}}
\def\constb{{\textbf{const }}}
\def\as{{\textbf{ as }}}
\def\msb{{\textsf{msb}}}
\def\if{{\text{if }}}
\def\ifb{{\textbf{if } \hspace{1pt}}}
\def\bi{{\ \ }}
\def\hso{{\hspace{1pt}}}
\def\Function{{\textbf{Function: }}}
\def\init{{\textsf{init}}}
\def\for{{\textbf{for }}}
\def\foreach{{\textbf{for each }}}
\def\bcolon{{\hspace{1pt} \textbf{:}}}
\def\state{{\textsf{state}}}
\def\xor{\oplus_\text{xor}}
\def\bit{{\textsf{bit}}}
\def\bits{{\textsf{bits}}}
\def\line#1{{{\small \rm \rlap{#1.}\hphantom{10.}} \ \ }}
\def\while{{\textbf{while }}}
\def\pluseq{\mathrel{+}=}
\def\return{{\textbf{return }}}
\def\else{{\textbf{else}}}
\def\len{{\textbf{len}}}
\def\preimage{{\textsf{preimage}}}
\def\DomainTag{{\text{DomainTag}}}
\def\Arity{{\text{Arity}}}
\def\HashType{{\text{HashType}}}
\def\MerkleTree{{\text{MerkleTree}}}
\def\ConstInputLen{{\text{ConstInputLen}}}
\def\Mds{{\mathcal{M}}}
\def\la{{\langle}}
\def\ra{{\rangle}}
\def\do{{\textbf{do }}}
\def\timesb{{\textbf{ times}}}
\def\RC{{\text{RoundConstants}}}
\def\push{{\textbf{.push}}}
\def\dotprod{{{\boldsymbol\cdot} \hso}}
\def\row{{\textsf{row}}}
\def\acc{{\textsf{acc}}}
\def\push{{\textbf{.push}}}
\def\extend{{\textbf{.extend}}}
\def\reverse{{\textbf{reverse}}}
\def\MdsInv{{\mathcal{M}^{\text{-} 1}}}
\def\deq{\overset{\diamond}=}
\def\alloc{{\textsf{alloc}}}
\def\allocpub{{\textsf{alloc_pub}}}
\def\bitlen{{\textbf{bitlen}}}
\def\typecolon{\mathbin{\large :}}
\def\CommDOld{{\text{CommDOld}}}
\def\CommDNew{{\text{CommDNew}}}
\def\CommROld{{\text{CommROld}}}
\def\CommRNew{{\text{CommRNew}}}
\def\Hs{{\textbf{Hs}}}
\def\pub{{\text{pub}}}
\def\priv{{\text{priv}}}
\def\lebitsgadget{{\textsf{le_bits_gadget}}}
\def\poseidongadget{{\textsf{poseidon_gadget}}}
$$

# Empty-Sector-Update Circuit Spec (Nov-2021)

## Notation and Constants

### General

$[n]$
The set containing the first $n$ unsigned integers $(0, 1, \ldots, n - 1)$.

$i \in [n]$
Indicates that $i$ is an index pointing to an element in an array of $n$ elements; equivalent to $i \in \mathbb{Z}$ where $0 \leq i < n$.

$x \typecolon \text{SomeType}^{[n]}$
Indicates that the value $x$ is an array of length $n$ where each element of the array is of type $\text{SomeType}$.

$x \typecolon \Fq$
Indicates that $x$ is a prime field element, specifically an element of BLS12-381's scalar field having modulus $q$.

$(a_0, \ldots, a_{n - 1})$
An array of $n$ elements.

$\boldsymbol{a}[i \hso \textbf{..} \hso j]$
A slice $(a_i, \ldots, a_{j - 1})$ of the array $\boldsymbol{a} = (a_0, \ldots, a_{n - 1})$.

### Configuration Parameters

$\text{SectorNodes} \in \{2^{30}, 2^{31}\}$
The number of nodes in the sector; allowed sector sizes are 32GiB and 64GiB.

$k \in [P]$
The index of the partition in the sector for which a proof is being generated.

$h \in \Hs$
The number of high bits taken from each challenge's [little-endian] binary representation. Filecoin currently defaults to using $h = 10$.

### Constants

$\constb A = 128$
The number of apex-leafs per partition.

$\constb \text{ApexLeafBits}, \text{ApexTreeHeight} = \log_2(A) = 7$
The number of bits required to specify the index of an apex-leaf; equivalently the height of each partition's apex-tree, i.e. each apex-tree contains $8 = 7 + 1$ rows (including leafs and root).

$\constb \text{ApexLeafOffset} = \text{NodeBits} - (\text{PartitionBits} + \text{ApexLeafBits})$
The position in a $\text{TreeDNew}$ Merkle proof which contains an apex-leaf.

$\constb C = 86$
The number of challenges per partition.

$\constb \text{ChallengesPerPRF} = \left\lfloor{\lfloor \log_2(q) \rfloor \over \text{RandChallengeBits}}\right\rfloor = 9$
The maximum number of challenges which can be derived from a single Poseidon digest when Poseidon is used as a pseudorandom function (PRF). $\lfloor \log_2(q) \rfloor = 254$ is the number of fully utilized bits in a field element $\Fq$.

$\constb \Hs = (7, 8, 9, 10, 11, 12)$
An array containing the allowed values for $h$.

$\constb \text{h_index} = \Hs\textsf{.index_of}(h)$
The index of the configuration parameter $h$ in $\Hs$.

$\constb \text{h_select} = 2^{\text{h_index}}$
An integer which encodes $\text{h_index}$.

$\constb \text{h_select_bits} \typecolon \Bit^{[\len(\Hs)]} = \textsf{le_bits}(\text{h_select})$
The binary representation of $\text{h_select}$. Note that exactly one bit in $\text{h_select_bits}$ is set which gives the index ($\text{h_index}$) of the chosen $h$ in $\Hs$.

$\constb \text{k_and_h_select} = k \vee (\text{h_select} \ll \text{PartitionBits})$
A packed integer containing $k$ and $\text{h_select}$.

$\constb \text{k_and_h_select_bits} \typecolon \Bit^{[\text{PartitionBits} + \len(\Hs)]} = \text{k_bits} \mathbin{\Vert} \text{h_select_bits} = \textsf{le_bits}(\text{k_and_h_select})$
The binary representation of $\text{k_and_h_select}$. The first bit is the least-significant of $\text{k_bits}$ and last bit is the most-significant of $\text{h_select}$.

$\constb \text{k_bits} \typecolon \Bit^{[\text{PartitionBits}]} = \textsf{le_bits}(k)$
The binary representation of the chosen partition-index $k$.

$\constb \text{NodeBits} = \log_2(\text{SectorNodes}) = \begin{cases}30 & \text{32GiB sector-size} \\ 31 & \text{64GiB sector-size}\end{cases}$
The number of bits required to specify the index of a node in a sector.

$\constb P = 16$
The number of partitions per sector.

$\constb \text{PartitionBits}, \text{PartitionTreeHeight} = \log_2(P) = 4$
The number of bits required to specify a partition-index $k \in [P]$; equivalently the height of the top of a sector's $\text{TreeDNew}$ (starting at the tree row containing $P$ number of nodes and continuing upwards until the tree's root $\text{CommDNew}$ is reached).

$\constb \text{PartitionNodes} = {\text{SectorNodes} \over P} = \begin{cases}2^{26} & \text{32GiB sector-size} \\ 2^{27} & \text{64GiB sector-size}\end{cases}$
The number of nodes in each partition of a sector.

$\constb \text{PRFsPerPartition} = \left\lceil {C \over \text{ChallengesPerPRF}} \right\rceil = 10$
The number of calls to the Poseidon-PRF required to generate a partition's $C$ challenges.

$\constb \text{RandChallengeBits} = \log_2(\text{PartitionNodes}) = \text{NodeBits} - \text{PartitionBits}$
The number of random bits generated per challenge; equivalently the number of bits required to specify the index of a node in a partition. Note that during challenge generation for a partition $k$, all challenge's will fall within the $k^{th}$ partition of the sector, i.e. the first $\text{RandChallengeBits}$ bits of each challenge are randomly chosen and the last $\text{PartitionBits}$ bits of each challenge are the same.

$\constb \text{TreeDHeight} = \log_2(\text{SectorNodes})$
$\constb \text{TreeRHeight} = \log_8(\text{SectorNodes})$
The heights of trees that have been generated over a sector of values. $\text{TreeD}$'s are arity-2 and use $\text{Sha256}$, whereas $\text{TreeR}$'s are arity-8 and use $\text{Poseidon}$. Note that adding 1 to a tree's height (for the leafs) $\text{height} + 1$ gives the number of "rows" in the tree.

### Old and New Sectors

$D_\text{old} \typecolon \Fq^{[\text{SectorNodes}]}$
An empty sector of data input to SDR-PoRep. Note that $D_\text{new}$ is not used by the empty-sector-update proof.

$R_\text{old} \typecolon \Fq^{[\text{SectorNodes}]}$
The replica of $D_\text{old}$ output by SDR-PoRep.

$D_\text{new} \typecolon \Fq^{[\text{SectorNodes}]}$
The data which is replacing the empty sector data $D_\text{old}$.

$R_\text{new} \typecolon \Fq^{[\text{SectorNodes}]}$
The encoding of the new data $D_\text{new}$.

### Old and New Merkle Trees and Commitments

$\text{TreeROld} = \text{OctTree}\textsf{::from_leaves}(R_\text{old})$
An arity-8 Merkle tree built over the replica $R_\text{old}$ output by running SDR-PoRep on an empty sector $D_\text{old}$.

$\text{TreeDNew} = \text{BinTree}\textsf{::from_leaves}(D_\text{new})$
An arity-2 Merkle tree built over the data $D_\text{new}$ which is replacing that of the old empty sector $D_\text{old}$.

$\text{TreeRNew} = \text{OctTree}\textsf{::from_leaves}(R_\text{new})$
An arity-8 Merkle tree built over the empty-sector-update encoding $R_\text{new}$ of the new sector data $D_\text{new}$.

$\text{CommROld} \typecolon \Fq = \text{Poseidon}((\text{CommC}, \text{TreeROld}\textsf{.root}))$
$\text{CommDNew} \typecolon \Fq = \text{TreeDNew}\textsf{.root}$
$\text{CommRNew} \typecolon \Fq = \text{Poseidon}((\text{CommC}, \text{TreeRNew}\textsf{.root}))$
Commitments to three Merkle trees. Note that $\text{CommC}$ is a commitment which was generated by SDR-PoRep when encoding $D_\text{old}$ into $R_\text{old}$.

### Merkle Proofs

$\textbf{struct } \text{BinTreeProof}\ \{$
$\quad \textsf{leaf} \typecolon \Fq,$
$\quad \textsf{path} \typecolon \Fq^{[\text{TreeDHeight}]},$
$\}$
Arity-2 Merkle proof type.

$\textbf{struct } \text{OctTreeProof}\ \{$
$\quad \textsf{leaf} \typecolon \Fq,$
$\quad \textsf{path} \typecolon {\Fq^{[7]}}^{[\text{TreeRHeight}]},$
$\}$
Arity-8 Merkle proof type.

### Empty-Sector-Update Proof

$\textbf{struct}\ \text{PartitionProof}\ \{$
$\quad \text{ChallengeProofs},$
$\quad \text{ApexLeafs},$
$\}$
Represents an empty-sector-update proof. One $\text{PartitionProof}$ is generated for each partition $k$ of an updated sector, thus $P$ number of $\text{PartitionProof}$'s are generated per updated sector. $C$ number of challenges are generated per partition, thus each $\text{PartitionProof}$ contains $C$ number of $\text{ChallengeProof}$'s.

$\textbf{struct } \text{ChallengeProof}\ \{$
$\quad \textsf{proof_r_old} \typecolon \text{OctTreeProof},$
$\quad \textsf{proof_d_new} \typecolon \text{BinTreeProof},$
$\quad \textsf{proof_r_new} \typecolon \text{OctTreeProof},$
$\}$
Three Merkle proofs are generated per challenge, one for each of the trees $\text{TreeROld}$, $\text{TreeDNew}$, and $\text{TreeRNew}$.

$\text{ChallengeProofs} \typecolon \text{ChallengeProof}^{[C]}$
Denotes all Merkle proofs generated for a partition.

$\text{PartitionPath} \typecolon \Fq^{[\text{PartitionTreeHeight}]} = \text{ChallengeProof}\textsf{.proof_d_new}\textsf{.path}[\text{RandChallengeBits} \textbf{..}]$
Denotes the final portion of all $\text{TreeDNew}$ Merkle proofs (starting from the partition's apex-root and continuing upwards until $\text{TreeDNew}\text{.root}$ is reached) generated for this partition. Note a partition's $\text{PartitionPath}$ is constant for all challenges in a partition, thus $\text{ChallengeProof}$ may correspond to any challenge in a partition.

$\text{ApexLeafs} \typecolon \Fq^{[A]} = \text{TreeDNew}\textsf{.row}_{\text{ApexLeafsOffset}}[kA \hso \textbf{..} (k + 1)A]$
The $k^{th}$ partition's apex-leafs, i.e. the $k^{th}$ chunk of $A$ nodes from the $\text{TreeDNew}$ row containing $P*A$ values.

## TreeDNew, Apex-Tree, and Partition-Tree


$\text{ApexTree}$ and $\text{PartitionTree}$ are sub-trees of a sector's $\text{TreeDNew}$. Each $\text{TreeDNew}$ has exactly one $\text{PartitionTree}$ (the top 5 rows of $\text{TreeDNew}$) and $P$ unique $\text{ApexTree}$'s (one for each partition). The root of the $k^{th}$ partition's $\text{ApexTree}$ is the $k^{th}$ leaf in $\text{PartitionTree}$.

Each Merkle challenge is the index of a node in a sector, thus challenges are either 30 or 31 bits (32GiB sectors contain $2^{30}$ nodes, 64GiB sectors contain $2^{31}$ nodes).

### Partition Trees

The last $\text{PartitionBits} = \log_2(P) = 4$ bits of a challenge represent the challenge's partition-index $k$. All challenges in a partition have the same partition bits.

Partition bits are used during $\text{TreeDNew}$ Merkle proof validation to hash from a partition's apex-root up to $\text{TreeDNew}\textsf{.root}$.

The top $4 + 1 = 5$ rows of $\text{TreeDNew}$ are a sub-tree (of height 4) called $\text{PartitionTree}$ whose leafs are a sector's apex-roots and whose root is $\text{TreeDNew}\textsf{.root}$.

### Apex Trees

The $\text{ApexLeafBits} = \log_2(A) = 7$ bits preceding a challenge's partition bits represent the index of the challenge's apex-leaf in the partition's $\text{ApexLeafs}$.

Apex-leaf bits are used during $\text{TreeDNew}$ Merkle proof validation to hash from a challenge's apex-leaf up to the partition's apex-root.

### Below Apex Leafs

All challenge bits which precede the apex-leaf bits, i.e. the challenge's first $\text{ApexLeafOffset} = \text{NodeBits} - (\text{PartitionBits} + \text{ApexLeafBits})$ bits, are used during $\text{TreeDNew}$ Merkle proof validation to hash from the challenge's leaf in $\text{TreeDNew}$ up to the challenge's apex-leaf.

## Randomness Generation

### Challenge Generation

Challenge generation is the process by which we generate $C = 86$ challenges per partition in an updated sector (of $\text{SectorNodes} = 2^{30}$ or $2^{31}$ number nodes) by calling Poseidon-PRF (128-bit security level, prime field $\Fq$, arity-2, width-3, see [Poseidon-PRF gadget](#Poseidon-and-Poseidon-PRF) for domain separation tag) $\text{PRFsPerPartition} = 10$ number of times to generate the binary representation of each of the partition's challenges.

The preimage for each $j \in [\text{PRFsPerPartition}]$ call to Poseidon-PRF in a partition is the concatenation of the unique identifier $\text{CommRNew}$ associated with the updated sector and the unique index of the PRF call in the sector $\text{PRFsPerPartition} * k + j$.

The number of fully utilized bits in a Poseidon digest is $\lfloor q \rfloor = 254$; if a sector partition contains $\text{PartitionNodes} = 2^{26}$ (32GiB sector-size) or $2^{27}$ (64GiB sector-size) nodes (where $P = 16$ is the number of partitions per sector), then the number of challenge generated from each PRF digest is $\text{ChallengesPerPRF} = \left\lfloor {254 \over 26} \right\rfloor = \left\lfloor {254 \over 27} \right\rfloor = 9$. We denote $\text{RandChallengeBits} = \log_2(\text{PartitionNodes}) = 26$ or $27$ as the number of bits taken from a PRF digest for each challenge.

The $j^{th}$ chunk of $\text{ChallengesPerPRF}$ challenges $(c_0, \ldots, c_8)$ for partition $k \in [P]$ is generated as follows:

$$
\eqalign{
& \text{digest} \typecolon \Fq = \text{PoseidonPRF}((\text{CommRNew}, \text{PRFsPerPartition} * k + j)) \\
& c_0 = \textsf{le_bits}(\text{digest})[0 * \text{RandChallengeBits} \hso \textbf{..} \hso 1 * \text{RandChallengeBits}] \\
& \quad \vdots \\
& c_8 = \textsf{le_bits}(\text{digest})[8 * \text{RandChallengeBits} \hso \textbf{..} \hso 9 * \text{RandChallengeBits}] \\
}
$$

A challenge $c \in [\text{PartitionNodes}]$ is an index of a node in a partition of $\text{PartitionNodes}$ number of nodes; appending the little-endian binary representation of the partition-index $k \in [P]$ onto $c$'s binary representation $\textsf{le_bits}(c) \mathbin{\Vert} \textsf{le_bits}(k)$ yields the challenge's node-index across all nodes in the sector.

### Phi, Rho, and Labeling

We assign a value $\text{phi}$ for each updated sector:
$$
\text{phi} = \text{PoseidonPRF}((\text{CommDNew}, \text{CommROld}))
$$ where $\text{CommROld}$ is a commitment to the empty sector's SDR replica and $\text{CommDNew}$ is a commitment to the new data which will overwrite the empty sector.

The Empty-Sector-Update algorithm takes a configuration parameter $h \in \Hs$ which specifies the number of high (i.e. most-significant) bits taken from each challenge's $c_i$ binary representation denoted $\text{high}_i$:
$$
\forall i \in [P * C]: \text{high}_i = c_i \gg (\log_2(\text{SectorNodes}) - h)
$$ note that $P * C$ is the total number of challenges per sector.

For each challenge $c_i$, a value $\text{rho}_i$ is computed from the challenge's $h$ high bits $\text{high}_i$ and the sector's $\text{phi}$.
$$
\forall i \in [P * C]: \text{rho}_i = \text{PoseidonPRF}((\text{phi}, \text{high}_i))
$$

$\text{rho}_i$ is used to compute the encoding of the $i^{th}$ node's new data, see [Old and New Sectors](#Old-and-New-Sectors) for notation.
$$
R_\text{new}[i] = \text{R}_\text{old}[i] + D_\text{new}[i] * \text{rho}_i
$$

## Circuit

### Notation

$a \typecolon \Fq \deq \textsf{alloc}(x)$
Denotes that $a$ is an allocated value in R1CS having the value $x$, where $x$ is an unallocated value.

$a \typecolon \Fq \deq \textsf{alloc_pub}(x)$
Denotes that $a$ is an allocated value in R1CS and is a public-input. The prover assigns the value of $a$ in R1CS to that of $x$, where $x$ is an unallocated value.

$\Fq$
A BLS12-381 scalar field element allocated in R1CS.

$\Ftwo$
A boolean constrained BLS12-381 scalar field element allocated in R1CS.

### Implementation

$\overline{\underline{\textbf{Circuit:}\ \text{SDR Empty Sector Update} \ \ }}$
$\textbf{#}\ \ \text{Public-inputs}$
$\line{1} \text{comm_r_old} \deq \allocpub(\CommROld_\pub)$
$\line{2} \text{comm_d_new} \deq \allocpub(\CommDNew_\pub)$
$\line{3} \text{comm_r_new} \deq \allocpub(\CommRNew_\pub)$

$\textbf{#}\ \ \text{Unpack k and h_select from their packed public-input}$
$\line{4} \text{k_and_h_select} \deq \allocpub(\text{k_and_h_select}_\pub)$
$\line{5} \text{k_and_h_select_bits} \typecolon \Ftwo^{[\text{PartitionBits} + \len(\Hs)]} \ \deq \lebitsgadget(\text{k_and_h_select})$
$\line{6} \text{k_bits} \typecolon \Ftwo^{[\text{PartitionBits}]} = \text{k_and_h_select_bits}[\textbf{..} \text{PartitionBits}]$
$\line{7} \text{h_select_bits} \typecolon \Ftwo^{[\len(\Hs)]} = \text{k_and_h_select_bits}[\text{PartitionBits}\textbf{..}]$
$\line{8} \text{k} \deq \textsf{lc_gadget}(\sum_{i \in [\text{PartitionBits}]} 2^i * \text{k_bits}[i]) \quad\quad\quad \textbf{#}\ 2^i \text{ is an unallocated constant}$

$\textbf{#}\ \ \text{Compute phi for this sector}$
$\line{9} \text{phi} \deq \textsf{poseidon_prf_gadget}((\text{comm_d_new}, \text{comm_r_old}))$

$\textbf{#}\ \ \text{Verify the roots of TreeROld and TreeRNew against public commitments}$
$\line{10} \text{comm_c} \deq \alloc(\text{CommC}_\priv)$
$\line{11} \text{root_r_old} \deq \alloc(\text{RootROld}_\priv)$
$\line{12} \text{root_r_new} \deq \alloc(\text{RootRNew}_\priv)$
$\line{13} \text{comm_r_old_calc} \deq \poseidongadget((\text{comm_c}, \text{root_r_old}))$
$\line{14} \text{comm_r_new_calc} \deq \poseidongadget((\text{comm_c}, \text{root_r_new}))$
$\line{15} \textsf{assert_eq}(\text{comm_r_old_calc}, \text{comm_r_old})$
$\line{16} \textsf{assert_eq}(\text{comm_r_new_calc}, \text{comm_r_new})$

$\textbf{#}\ \ \text{Verify the witnessed apex-leafs against the public commitment CommDNew}$
$\line{17} \text{apex_leafs} \typecolon \Fq^{[\text{ApexLeafs}]} \deq (\alloc(\text{ApexLeafs}_\priv[i]) \mid i \in [\text{ApexLeafs}])$
$\line{18} \text{apex_root} \deq \textsf{apex_root_gadget}(\text{apex_leafs})$
$\line{19} \text{partition_path} \typecolon \Fq^{[\text{PartitionTreeHeight}]} \deq (\textsf{alloc}(\text{PartitionPath}_\text{priv}[i]) \mid i \in [\text{PartitionTreeHeight}])$
$\line{20} \text{comm_d_new_calc} \deq \textsf{bintree_root_gadget}(\text{k_bits}, \text{apex_root}, \text{partition_path})$
$\line{21} \textsf{assert_eq}(\text{comm_d_new_calc}, \text{comm_d_new})$

$\textbf{#}\ \ \text{Generate this partition's challenges}$
$\line{22} \text{rand_challenge_bits} \typecolon {\Ftwo^{[\text{RandChallengeBits}]}}^{[C]} \deq \textsf{gen_challenge_bits_gadget}(\text{comm_r_new}, \text{k})$

$\textbf{#}\ \ \text{Verify each challenge's Merkle proofs}$
$\line{23} \for i \in [C]\bcolon$
$\line{24} \quad (\text{proof_r_old}, \text{proof_d_new}, \text{proof_r_new}) \leftarrow \text{ChallengeProofs}_\priv[i]$

$\quad\quad \ \ \textbf{#}\ \text{Get this challenge's binary representation}$
$\line{25} \quad \text{challenge_sans_partition_bits} \typecolon \Ftwo^{[\text{RandChallengeBits}]} = \text{rand_challenge_bits}[i]$
$\line{26} \quad \text{challenge_bits} \typecolon \Ftwo^{[\text{NodeBits}]} = \text{challenge_sans_partition_bits} \mathbin{\Vert} \text{k_bits}$

$\quad\quad\ \ \textbf{#}\ \text{Calculate this challenge's encoding}$
$\line{27} \quad \text{high} \deq \textsf{get_high_bits_gadget}(\text{challenge_bits}, \text{h_select_bits})$
$\line{28} \quad \text{rho} \deq \textsf{poseidon_prf_gadget}((\text{phi}, \text{high}))$
$\line{29} \quad \text{leaf_r_old} \deq \alloc(\text{proof_r_old}\textsf{.leaf})$
$\line{30} \quad \text{leaf_d_new} \deq \alloc(\text{proof_d_new}\textsf{.leaf})$
$\line{31} \quad \text{leaf_d_new_rho} \deq \textsf{mul_gadget}(\text{rho}, \text{leaf_d_new})$
$\line{32} \quad \text{leaf_r_new} \deq
\textsf{add_gadget}(\text{leaf_r_old}, \text{leaf_d_new_rho})$

$\quad\quad\ \ \textbf{#}\ \text{Get this challenge's apex-leaf from the array of validated apex-leafs}$
$\line{33} \quad \text{apex_leaf_bits} \typecolon \Ftwo^{[\text{ApexLeafBits}]} = \text{challenge_sans_partition_bits}[\text{ApexLeafOffset} \hso \textbf{..}]$
$\line{34} \quad \text{apex_leaf} \deq \textsf{select_gadget}(\text{apex_leafs}, \text{apex_leaf_bits})$

$\quad\quad\ \ \textbf{#}\ \text{Verify this challenge's TreeDNew Merkle proof up to the apex-leaf}$
$\line{35} \quad \text{below_apex_leaf_bits} \typecolon \Ftwo^{[\text{ApexLeafOffset}]} = \text{challenge_sans_partition_bits}[\textbf{..} \hso \text{ApexLeafOffset}]$
$\line{36} \quad \text{below_apex_leaf_path} \typecolon \Fq^{[\text{ApexLeafOffset}]} \deq (\textsf{alloc}(\text{proof_d_new}\textsf{.path}[i]) \mid i \in [\text{ApexLeafOffset}])$
$\line{37} \quad \text{apex_leaf_calc} \typecolon \Fq \deq \textsf{bintree_root_gadget}($
$\phantom{\line{71}\quad} \quad \text{below_apex_leaf_bits},$
$\phantom{\line{72}\quad} \quad \text{leaf_d_new},$
$\phantom{\line{73}\quad} \quad \text{below_apex_leaf_path},$
$\phantom{\line{74}\quad})$
$\line{38} \quad \textsf{assert_eq}(\text{apex_leaf_calc}, \text{apex_leaf})$

$\quad\quad\ \ \textbf{#}\ \text{Verify this challenge's TreeROld Merkle proof}$
$\line{39} \quad \text{path_r_old} \typecolon {\Fq^{[7]}}^{[\text{TreeRHeight}]} \deq ((\alloc(\text{proof_r_old}\textsf{.path}[h][s]) \mid s \in [7]) \mid h \in [\text{TreeRHeight}])$
$\line{40} \quad \text{root_r_old_calc} \deq \textsf{octtree_root_gadget}(\text{challenge_bits}, \text{leaf_r_old}, \text{path_r_old})$
$\line{41} \quad \textsf{assert_eq}(\text{root_r_old_calc}, \text{root_r_old})$

$\quad\quad\ \ \textbf{#}\ \text{Verify this challenge's TreeRNew Merkle proof}$
$\line{42} \quad \text{path_r_new} \typecolon {\Fq^{[7]}}^{[\text{TreeRHeight}]} \deq ((\alloc(\text{proof_r_new}\textsf{.path}[h][s]) \mid s \in [7]) \mid h \in [\text{TreeRHeight}])$
$\line{43} \quad \text{root_r_new_calc} \deq \textsf{bintree_root_gadget}(\text{challenge_bits}, \text{leaf_r_new}, \text{path_r_new})$
$\line{44} \quad \textsf{assert_eq}(\text{root_r_new_calc}, \text{root_r_new})$

## Gadgets

$\textsf{add_gadget}(x \typecolon \Fq, y \typecolon \Fq) \rightarrow \Fq$
Allocates and returns the value $z = x + y$ and adds the R1CS constraint $(x + y) * (1) = z$.

$\textsf{mul_gadget}(x \typecolon \Fq, y \typecolon \Fq) \rightarrow \Fq$
Allocates and returns the value $z = x * y$ and adds the R1CS constraint $(x) * (y) = z$.

$\textsf{lc_gadget}(c_1x_1 + \ldots + c_nx_n) \rightarrow \Fq$
Allocates and returns the evaluation $y$ of the provided linear-combination; each $x_i$ is a value allocated in R1CS and each $c_i$ is an unallocated constant by which $x_i$ is scaled. This gadget adds the R1CS constraint $(c_1x_1 + \ldots + c_nx_n) * (1) = y$.

$\textsf{sum_gadget}((x_1, \ldots, x_n)) \rightarrow \Fq$
Allocates and returns the the sum of the array of allocated values $(x_1, \ldots, x_n)$. Equivalent to calling $\textsf{lc_gadget}(\sum_{i \in [n]} 1 * x_i)$.

$\textsf{le_bits_gadget}(x \typecolon \Fq) \rightarrow \Ftwo^{[n]}$
Allocates and returns the little-endian binary representation of the allocated value $x$. This gadget allocates $n$ boolean constrained values $(b_0, \ldots, b_{n - 1})$ in R1CS (adding one boolean constraint per bit) and adds the constraint $(2^0b_0 + \ldots + 2^{n - 1}b_{n - 1}) * (1) = x$ where each $2^i$ is an unallocated constant.

### Poseidon and Poseidon-PRF

$\textsf{poseidon_gadget}(\text{preimage} \typecolon \Fq^{[2]}) \rightarrow \Fq$
Given an allocated array of two field elements ($\text{preimage}$) computes the Poseidon digest (width-3) of the preimage in R1CS and returns the allocated digest. This gadget uses the Poseidon "Merkle Tree arity-2" domain separation tag, i.e. the first field element of the width-3 initial state is $2^\text{arity} - 1 = 3$ and the remaining two elements of the initial state are $\text{preimage}$.

$\textsf{poseidon_prf_gadget}(\text{preimage} \typecolon \Fq^{[2]}) \rightarrow \Fq$
Uses Poseidon as a pseudorandom function (PRF). This gadget is identical to $\textsf{poseidon_gadget}$ except that here we use a "custom" Poseidon domain separation tag of $2^{40}$.

### Apex-Root

Creates an arity-2 SHA256 Merkle tree in R1CS from the leafs $\text{apex_leafs}$ and returns the root as an allocated value.

$\overline{\underline{\textbf{Gadget:}\ \textsf{apex_root_gadget}(\text{apex_leafs} \typecolon \Fq^{[A]}) \rightarrow \Fq}}$
$\line{1} \text{row} = \text{apex_leafs}$
$\line{2} \textbf{while } \len(\text{row}) > 1 \boldsymbol{:}$
$\line{3} \quad \text{row} \typecolon \Fq^{[\len(\text{row}) / 2]} \deq (\textsf{sha256_gadget}((\text{row}[2i], \text{values}[2i + 1])) \mid i \in [\len(\text{row}) / 2])$
$\line{4} \textbf{return } \text{row}[0]$

### Challenge Generation

Generates $C$ random challenges for partition $k$ of the updated sector corresponding to $\text{CommRNew}$.

$\overline{\underline{\textbf{Gadget:}\ \textsf{gen_challenge_bits_gadget}(\text{comm_r_new} \typecolon \Fq, k \typecolon \Fq) \rightarrow {\Ftwo^{[\text{RandChallengeBits}]}}^{[C]}}}$
$\line{1} \text{rand_challenge_bits} \typecolon {\Ftwo^{[\text{RandChallengeBits}]}}^{[C]} = (\ )$
$\line{2} \textbf{for } i \in [\text{PRFsPerPartition}] \boldsymbol{:}$
$\line{3} \quad \text{digest_index} \deq \textsf{lc_gadget}(\text{PRFsPerPartition} * k + i * \text{R1CS}\textsf{.one}) \quad\quad \textbf{#}\ \text{PRFsPerPartition}\ \text{and}\ i\ \text{are unallocated constants}$
$\line{4} \quad \text{digest} \deq \textsf{poseidon_prf_gadget}((\text{comm_r_new}, \text{digest_index}))$
$\line{5} \quad \text{digest_bits} \typecolon \Ftwo^{[255]} \deq \textsf{le_bits_gadget}(\text{digest}) \quad\quad \textbf{#}\ 255 = \lceil\log_2(q)\rceil\ \text{is the bit-length of } \Fq$
$\quad\quad\ \ \textbf{#}\ \text{Chunk digest_bits by challenge (chunks of size RandChallengeBits)}$
$\line{6} \quad \textbf{for } j \in [\text{ChallengesPerPRF}] \boldsymbol{:}$
$\line{7} \quad\quad \text{challenge_bits} \typecolon \Ftwo^{[\text{RandChallengeBits}]} = \text{digest_bits}[j * \text{RandChallengeBits} \textbf{..} \hso (j + 1)\text{RandChallengeBits}]$
$\line{8} \quad\quad \text{rand_challenge_bits}\textsf{.push}(\text{challenge_bits})$
$\textbf{#}\ \ \text{Truncate the return value because the last PRF adds more challenges than necessary}$
$\line{9} \textbf{return } \text{rand_challenge_bits}[\textbf{..} \hso C]$

### Get Challenge High Bits

Returns the $h$ high bits of $\text{challenge_bits}$, allocated as a single field element, where $h$ is chosen from $\Hs$ via $\text{h_select_bits}$.

$\overline{\underline{\textbf{Gadget:}\ \textsf{get_high_bits_gadget}(\text{challenge_bits} \typecolon \Ftwo^{[\text{NodeBits}]}, \text{h_select_bits} \typecolon \Ftwo^{[\len(\Hs)]}) \rightarrow \Fq}}$
$\line{1} \text{scaled_highs} \typecolon \Fq^{[\len(\Hs)]} = (\ )$
$\line{2} \textbf{for } (h, \text{h_select_bit}) \in \textbf{zip}(\Hs, \text{h_select_bits}) \boldsymbol{:}$
$\quad\quad\ \ \textbf{#}\ \text{Pack the } h \text{ high bits of challenge_bits into a single } \Fq$
$\line{3} \quad \text{high_bits} = \text{challenge_bits}[\text{NodeBits} - h \hso \textbf{..}]$
$\line{4} \quad \text{high} \deq \textsf{lc_gadget}(\sum_{i \in [h]} 2^i * \text{high_bits}[i]) \quad\quad\quad \textbf{#}\ \text{Note: } 2^i \text{ is an unallocated constant}$
$\quad\quad\ \ \textbf{#}\ \text{Scale by } 0 \text{ or } 1$
$\line{5} \quad \text{high_or_zero} \deq \textsf{mul_gadget}(\text{high}, \text{h_select_bit})$
$\line{6} \quad \text{scaled_highs}\textsf{.push}(\text{high_or_zero})$
$\textbf{#}\ \ \text{The sum of the scaled values is the selected high value}$
$\line{7} \text{selected_high} \deq \textsf{sum_gadget}(\text{scaled_highs})$
$\line{8} \textbf{return } \text{selected_high}$