$$
\def\deq{\overset{\diamond}=}
\def\alloc{{\textsf{alloc}}}
\def\bitlen{{\textbf{bitlen}}}
\def\Fq{{\mathbb{F}_q}}
\def\line#1{{{\small \rm \rlap{#1.}\hphantom{10.}} \ \ }}
\def\typecolon{\mathbin{\large :}}
$$

# CC-Sector Update Circuit

## General Notation

$\Fq$
A prime field element (i.e. an integer $\text{mod } q$). Filecoin uses the BLS12-381 scalar field as its prime field.

$\Fq|_{\{0, 1\}}$
A field element whose value is constrained to either $0$ or $1$.

$\Fq^{[n]}$
An array containing $n$ field elements.

$x \typecolon \Fq$
A variable $x$ which has type $\Fq$.

$(x_1, x_2)$
An array containing two values.

$0\text{..}n$
The range of values $(0, 1, \ldots, n - 1)$.

$\text{arr}[m\text{..}n]$
A slice (subarray) of an array $\text{arr}$ containing the values $(\text{arr}[m], \text{arr}[m + 1], \ldots, \text{arr}[n - 1])$.

$y \deq \textsf{some_gadget}(\ldots)$
Denotes $y$ as a being a value allocated in a constraint system by a gadget $\textsf{some_gadget}$.

## Circuit Notation and Constants

$N = \begin{cases} 2^{30} & \text{if sector-size} = 32\ \text{GiB} \\ 2^{31} & \text{otherwise if sector-size} = 64\ \text{GiB}
\end{cases}$
The number of nodes per sector.

$C = 2200$
The number of challenges per sector (one proof is generated for per update CC-sector).

$c \in 0\text{..}N$
A Merkle challenge (i.e. the index of a node in a sector of size $N$). There are $C$ number of challenges $c_i$ generated per proof.

$\rho \typecolon \Fq$
A random value generated for each challenge $c$.

$\bitlen(\text{digest}) = \bitlen(\Fq) = \left\lceil \log_2(q) \right\rceil = 255$
The bit-length of a Poseidon digest. Our Poseidon hash function is instantiated over a $\approx$ 256-bit field (BLS12-381's scalar field $\Fq$), thus targets a security level of 128 bits. $q$ is the Poseidon field modulus.

$\bitlen(c) = \log_2(N) = \begin{cases}30 & \text{if sector-size is 32GiB} \\ 31 & \text{otherwise if sector-size is 64GiB}\end{cases}$
The bit-length of a challenge $c$. Each challenge $c$ is the index of a node in a sector $c \in 0\text{..}N$.

$\left\lfloor\bitlen(\text{digest}) \over \bitlen(c)\right\rfloor = \left\lfloor{255 \over \log_2(N)}\right\rfloor = 8$
The number of challenges generated using a single Poseidon digest, i.e. the $j^{th}$ digest is used to generate the challenges $(c_{j8}, c_{j8 + 1}, \ldots, c_{j8 + 7})$.

$C/8 = 275$
The number of Poseidon digests required to generate $C$ number of challenges, i.e. a single Poseidon digest generates $8$ of the required $C = 2200$ challenges.

$\boldsymbol{H} = \left(2^7, 2^8, 2^9, 2^{10}, 2^{11}, 2^{12}\right)$
An array containing the possible values of $H$.

$H \in \boldsymbol{H}$
Specifies the number of bits extracted from a challenge $c$'s binary representation $\text{c_bits}$ and appended onto $\text{CommDNew}$ to generate the preimage for $c$'s random value $\rho$. $H$ is chosen from $\boldsymbol{H}$ using the $\text{HSelect}$ public-input.

$\text{HSelect} \typecolon \Fq \in \{2^0, 2^1, 2^2, 2^3, 2^4, 2^5\}$
Selects $H \in \boldsymbol{H}$ via $H = \boldsymbol{H}[\log_2(\text{HSelect})]$. Note that each possible value of $\text{HSelect}$ has either no bits set or exactly one bit set, thus $\log_2(\text{HSelect})$ is a unique integer in $0\text{..}6$. Within the circuit we allocate $\textsf{HSelect}$ as 6 bits $\text{h_select_bits}$ and extract the $\log_2(H)$ high bits from each challenge $c$ using the linear combination $c * \sum_{k \in 0\text{..}6} \text{h_select_bits}[k] * 2^{\log_2(N) - \log_2(\boldsymbol{H}[k])}$.

$\text{CommDNew} \typecolon \Fq$
Commitment to the sector's plaintext data after updating; the root of $\text{TreeDNew}$.

$\text{CommROld}, \text{CommRNew} \typecolon \Fq$
Commitments to the replicated sector before and after updating; $\text{CommR} = \textsf{poseidon}_2((\text{CommC}, \text{CommRLast}))$.

$\text{CommRLastOld}, \text{CommRLastNew} \typecolon \Fq$
Roots of the sector's $\text{TreeR}$ trees before and after updating.

$\text{CommC} \typecolon \Fq$
The original/unupdated sector's $\text{CommC}$. Note that $\text{CommC}$ is not changed when updating a CC-sector.

$\text{TreeDNewProof}_c \typecolon \textsf{struct } \Big\{ \thinspace\text{leaf} \typecolon \Fq,\ \text{path} \typecolon {\Fq^{[1]}}^{[\log_2(N)]} \thinspace \Big\}$
$\text{TreeROldProof}_c, \text{TreeRNewProof}_c \typecolon \textsf{struct } \Big\{ \thinspace\text{leaf} \typecolon \Fq,\ \text{path} \typecolon {\Fq^{[7]}}^{[\log_8(N)]} \thinspace \Big\}$
Three Merkle proofs (1 bintree, 2 octtree) are generated for each challenge $c$: one in $\text{TreeDNew}$, one in $\text{TreeROld}$, and one in $\text{TreeRNew}$. The $\text{leaf}$ field is the Merkel challenge $c$'s (leaf) label. The field $\text{path}$ is the Merkle path generated for $c$.

## Summary

Generate $C$ number of challenges using $C/8$ Poseidon digests, i.e. one digest generates $8$ challenges.
$$
\forall j \in 0\text{..}C/8: \text{digest}_j = \text{poseidon}((\text{CommDNew}, j))
$$

Each challenge is a $\log_2(N)$-bit unsigned integer, thus split each digest into $8$, $\log_2(N)$-bit, partitions interpreting each as the little-endian bits of a challenge $c$.
$$
\forall i \in 0\text{..}8: c_{8j + i} = \text{digest}_j[\log_2(N)i \text{..} \log_2(N)(i + 1)] \textsf{ as } \Fq
$$

Isolate the most-significant $H$ bits of $c$ denoted $\text{c_high}$ where $H$ is chosen from $\boldsymbol{H}$ using the public input bit-array $\text{HSelect}$. Calculate each challenge's random value $\rho$ using $\text{c_high}$.
$$
\rho_c = \text{poseidon}((\text{poseideon}(\text{CommDNew}, \text{CommROld}), \text{c_high}))
$$

Verify each challenge $c$'s Merkle proofs in $\text{TreeDNew}$, $\text{TreeROld}$, and $\text{TreeRNew}$ (i.e. the trees built over the new plaintext data, old replica, and new replica).

Verify each $c$'s new replica label $R_c^\ast$ using $c$'s old replica label $R_c$, new plaintext label $D_c^\ast$, and $\rho_c$.
$$
R_c^\ast = R_c + D_c^\ast \rho_c
$$

## Circuit

**Public Inputs:** $\text{CommDNew}, \text{CommROld}, \text{CommRNew}, \text{HSelect}$

**Private Inputs:** $\text{CommC}, \text{CommRLastOld}, \text{CommRLastNew}, \forall c \in (c_1, \ldots, c_{2200}): \text{TreeDNewProof}_c, \text{TreeROldProof}_c, \text{TreeRNewProof}_c$

$\overline{\underline{\textbf{Circuit:}\ \text{SDR CC-Sector Update} \ \ }}$
$\line{1} \text{comm_d_new} \deq \textsf{alloc_pub}(\text{CommDNew}_\text{pub})$
$\line{2} \text{comm_r_old} \deq \textsf{alloc_pub}(\text{CommROld}_\text{pub})$
$\line{3} \text{comm_r_new} \deq \textsf{alloc_pub}(\text{CommRNew}_\text{pub})$
$\line{4} \phi \typecolon \Fq \deq \textsf{poseidon_gadget}_2((\text{comm_d_new}, \text{comm_r_old}))$
$\line{5} \text{h_select} \deq \textsf{alloc_pub}(\text{HSelect}_\text{pub})$
$\line{6} \text{h_select_bits} \typecolon {\Fq|_{\{0, 1\}}}^{[6]} \deq \textsf{le_bits_gadget}(\text{h_select}, 6)$

$\line{7} \text{comm_c} \deq \alloc(\text{CommC}_\text{priv})$
$\line{8} \text{comm_r_last_old} \deq \alloc(\text{CommRLastOld}_\text{priv})$
$\line{9} \text{comm_r_last_new} \deq \alloc(\text{CommRLastNew}_\text{priv})$

**TODO:** do we need to prove $\text{CommRLastOld}$ using $\text{CommROld}$?
$\line{10} \text{comm_r_old_calc} \typecolon \Fq \deq \textsf{poseidon_gadget}_2((\text{comm_c}, \text{comm_r_last_old}))$
$\line{11} \textsf{assert_eq}(\text{comm_r_old_calc}, \text{comm_r_old})$

$\line{10} \text{comm_r_new_calc} \typecolon \Fq \deq \textsf{poseidon_gadget}_2((\text{comm_c}, \text{comm_r_last_new}))$
$\line{11} \textsf{assert_eq}(\text{comm_r_new_calc}, \text{comm_r_new})$

$\line{12} \textbf{for } j \in 0\text{..}C/8 \hspace{1pt}{:}$
$\line{13} \quad j \overset{\diamond}= \alloc(j)$
$\line{14} \quad \text{digest} \typecolon \Fq \deq \textsf{poseidon_gadget}_2((\text{comm_r_new}, j))$
$\line{15} \quad \text{digest_bits} \typecolon {\Fq|_{\{0, 1\}}}^{[8\log_2(N)]} \deq \textsf{le_bits_gadget}(\text{digest}, 8 \log_2(N))$

$\line{16} \quad \textbf{for } i \in 0\text{..}8\hspace{1pt}{:}$
$\line{17} \quad\quad \text{c_bits} \typecolon {\Fq|_{\{0, 1\}}}^{[\log_2(N)]} = \text{digest_bits}[\log_2(N)i\text{..}\log_2(N)(i + 1)]$
$\line{18} \quad\quad \text{c_high} \deq \textsf{lc_gadget}(\sum_{k \in 0\text{..}6} \text{h_select_bits}[k] * (\text{c_bits} \gg (\log_2(N) - \log_2(\boldsymbol{H}[k]))))$
$\line{19} \quad\quad \rho \typecolon \Fq \deq \textsf{poseidon_gadget}_2((\phi, \text{c_high}))$

$\line{20} \quad\quad (\text{label_d_new}, \text{path_d_new}) \deq \textsf{alloc_bintree_proof}(\text{TreeDNewProof}_{c, \hspace{1pt} \text{priv}})$
$\line{21} \quad\quad (\text{label_r_old}, \text{path_r_old}) \deq \textsf{alloc_octtree_proof}(\text{TreeROldProof}_{c, \hspace{1pt} \text{priv}})$
$\line{22} \quad\quad (\text{label_r_new}, \text{path_r_new}) \deq \textsf{alloc_octtree_proof}(\text{TreeRNewProof}_{c, \hspace{1pt} \text{priv}})$

$\line{23} \quad\quad \text{comm_d_new_calc} \deq \textsf{bintree_root_gadget}(\text{c_bits}, \text{label_d_new}, \text{path_d_new})$
$\line{24} \quad\quad \text{comm_r_last_old_calc} \deq \textsf{octtree_root_gadget}(\text{c_bits}, \text{label_r_old}, \text{path_r_old})$
$\line{25} \quad\quad \text{comm_r_last_new_calc} \deq \textsf{octtree_root_gadget}(\text{c_bits}, \text{label_r_new}, \text{path_r_new})$

$\line{26} \quad\quad \textsf{assert_eq}(\text{comm_d_new_calc}, \text{comm_d_new})$
$\line{27} \quad\quad \textsf{assert_eq}(\text{comm_r_last_old_calc}, \text{comm_r_last_old})$
$\line{28} \quad\quad \textsf{assert_eq}(\text{comm_r_last_new_calc}, \text{comm_r_last_new})$

$\line{29} \quad\quad \text{rho_label_d_new} \deq \textsf{mul_gadget}(\rho, \text{label_d_new})$
$\line{30} \quad\quad \text{label_r_new_calc} \deq \textsf{add_gadget}(\text{label_r_old}, \text{rho_label_d_new})$
$\line{31} \quad\quad \textsf{assert_eq}(\text{label_r_new_calc}, \text{label_r_new})$

## Gadgets

$\textsf{alloc}(x)$ allocates $x$ in the constraint-system and does not add constraints.

$\textsf{alloc_pub}(x)$ makes one public and one private allocation in the constraint-system and adds one constraint asserting equality between the two.

$\textsf{alloc_bintree_proof/alloc_octtree_proof}(\text{leaf}, \text{path})$ allocate a challenge $c$'s Merkle leaf label and its Merkle path elements and doe not add constraints to the constraint system.

$\textsf{assert_eq}(x, y)$ adds one constraint asserting the equality $x == y$.

$\textsf{add_gadget}(x, y)$ allocates the sum $x + y$ and adds one constraint asserting the correctness of the allocated value.

$\textsf{mul_gadget}(x, y)$ allocates the product $x * y$ and adds one constraint asserting the correctness of the allocated value.

$\textsf{lc_gadget}(\sum_{i} \text{const}_i * \text{prev_alloc_value}_i)$ makes one allocation for the output of the linear combination ("lc") and adds one constraint asserting that the allocated value is consistent with the sum of (scaled) previously allocated values. Note that each constant $\text{const}_i$ is unallocated.

$\textsf{poseidon_gadget}_2((x, y))$ calculates the arity-2 Poseidon digest of the preimage array $(x, y)$.

$\textsf{le_bits_gadget}(x, n)$ allocates $x$ as $n$ bits in the constraint system, i.e. makes $n$ allocations, add a boolean constraint for each allocated bit, and adds $1$ constraint asserting that the allocated bits are the correct binary representation for $x$: $\textsf{assert_eq}(\sum_{i \in 0\text{..}n} 2^i * \text{bits}[i], x)$.

$\textsf{bintree_root_gadget/octtree_root_gadget}(\text{c_bits}, \text{leaf}, \text{path})$ calculates the root of a Merkle bintree/octtree given a challenge $c$'s Merkle leaf label and Merkle path. Bintrees use arity-2 SHA256 and octtrees use arity-8 Poseidon.

## Circuit (Updated)

$\textbf{const } \text{P} = 16$
$\textbf{const } \text{A} = 128$
$\textbf{const } \text{C} = 86$
$\textbf{const } \textbf{Hs} = (7, 8, 9, 10, 11, 12)$
$\textbf{const } \text{PartitionTreeHeight} = \log_2(\text{P}) = 4$
$\textbf{const } \text{ApexTreeHeight} = \log_2(\text{A}) = 7$

$\textbf{config } \text{SectorSize} \in \{32\ \text{GiB}, 64\ \text{GiB}\}$
$\textbf{config } k \in 0\text{..}\text{P}$
$\textbf{config } \text{HsIndex} \in \{0, 1, 2, 3, 4, 5\}$

$\textbf{type } \text{TreeD} = \text{BinTree}$

$\textbf{type } \text{TreeR} = \begin{cases}
\text{OctTree} & \text{if } \text{SectorSize} = 32\ \text{GiB} \\
\text{OctBinTree} & \text{if } \text{SectorSize} = 64\ \text{GiB} \\
\end{cases}$

$\text{Nodes} = \begin{cases}
2^{30} & \text{if } \text{SectorSize} = 32\ \text{Gib} \\
2^{31} & \text{if } \text{SectorSize} = 64\ \text{Gib}
\end{cases}$

$\textbf{input } \text{R}_\text{old} \in \Fq^{[\text{Nodes}]}$
$\textbf{input } \text{D}_\text{new} \in \Fq^{[\text{Nodes}]}$
$\textbf{input } \text{R}_\text{new} \in \Fq^{[\text{Nodes}]}$

$\text{ChallengeBits} = \log_2(\text{Nodes})$
$\text{PartitionBits} = \log_2(\text{P})$
$\text{RandChallengeBits} = \text{ChallengeBits} - \text{PartitionBits}$

$\text{HSelect} = 2^{\text{HsIndex}}$
$\text{H} = \textbf{Hs}[\text{HsIndex}] = \textbf{Hs}[\log_2(\text{HSelect})]$

$\text{TreeROld} = \text{TreeR}(\text{R}_\text{old})$
$\text{TreeDNew} = \text{TreeD}(\text{D}_\text{new})$
$\text{TreeRNew} = \text{TreeR}(\text{R}_\text{new})$

$\text{CommROld} = \text{TreeROld}\text{.root}$
$\text{CommDNew} = \text{TreeDNew}\text{.root}$
$\text{CommRNew} = \text{TreeRNew}\text{.root}$

$\text{TreeDHeight} = \log_2(\text{Nodes})$

$\text{TreeRHeight} = \begin{cases}
\log_8(\text{Nodes}) & \text{if } \text{SectorSize} = 32\ \text{GiB} \\
\log_8(\text{Nodes} / 2) + 1 & \text{if } \text{SectorSize} = 64\ \text{GiB}
\end{cases}$

$\text{ApexRootsRow} = \text{TreeDHeight} - \text{PartitionTreeHeight}$
$\text{ApexLeafsRow} = \text{ApexRootsRow} - \text{ApexTreeHeight}$

$\text{ApexLeafs} = \text{TreeD}[\text{ApexLeafsRow}][k * \text{A} \text{..} (k + 1) * \text{A}]$
$\text{ApexTree} = \text{TreeD}(\text{ApexLeafs})$
$\text{ApexRoots} = \text{TreeD}[\text{ApexRootsRow}]$
$\text{ApexRoot} = \text{ApexRoots}[k] = \text{ApexTree}\text{.root}$

$\text{PartitionBits} = ((k \gg i) \wedge 1 \mid i \in \log_2(\text{P})) = \textbf{le_bits}(k)$
$\text{PartitionPath} = (\text{TreeD}_\text{new}[\text{ApexRootsRow} + i][(k \gg i) + j] \mid i \in 0\text{..}\text{ApexTreeHeight}, j = \begin{cases} 1 & \text{if } \textbf{is_even}(k \gg i) \\ -1 & \text{if } \textbf{is_odd}(k \gg i) \end{cases}) = \text{TreeDNewProof}_c[\text{TreeDHeight} - \text{PartitionTreeHeight}\text{..}]$

$\text{PubInputs} = (k, \text{CommROld}, \text{CommDNew}, \text{CommRNew}, \text{HSelect})$
$\text{PrivInputs} = (\text{CommC}, \text{RootROld}, \text{RootRNew}, \textbf{ApexLeafs}, \textbf{ChallengeProofs})$

$\overline{\underline{\textbf{Circuit:}\ \text{SDR Empty Sector Update} \ \ }}$
$\line{1} \text{k} \deq \textsf{alloc_pub}(k_\text{pub})$
$\line{2} \text{comm_r_old} \deq \textsf{alloc_pub}(\text{CommROld}_\text{pub})$
$\line{3} \text{comm_d_new} \deq \textsf{alloc_pub}(\text{CommDNew}_\text{pub})$
$\line{4} \text{comm_r_new} \deq \textsf{alloc_pub}(\text{CommRNew}_\text{pub})$
$\line{5} \text{h_select} \deq \textsf{alloc_pub}(\text{HSelect}_\text{pub})$

$\line{6} \text{k_bits} \deq \textsf{le_bits_gadget}(\text{k}, 255)[\text{..}\log_2(P)]$
$\line{7} \text{h_select_bits} \deq \textsf{le_bits_gadget}(\text{h_select}, 255)[\text{..}6]$
$\line{8} \text{phi} \deq \textsf{poseidon_gadget}((\text{comm_d_new}, \text{comm_r_old}))$

$\line{9} \text{comm_c} \deq \textsf{alloc}(\text{CommC}_\text{priv})$
$\line{10} \text{root_r_old} \deq \textsf{alloc}(\text{RootROld}_\text{priv})$
$\line{11} \text{root_r_new} \deq \textsf{alloc}(\text{RootRNew}_\text{priv})$
$\line{12} \text{apex_leafs}: \Fq^{[\text{A}]} \deq (\textsf{alloc}(\text{apex_leaf}) \mid \text{apex_leaf} \in \text{ApexLeafs}_\text{priv})$
$\line{13} \text{partition_path}: {\Fq^{[1]}}^{[\text{PartitionTreeHeight}]} \deq ((\textsf{alloc}(\text{el})) \mid \text{el} \in \text{PartitionPath}_\text{priv})$

$\line{14} \text{comm_r_old_calc} \deq \textsf{poseidon_gadget}((\text{comm_c}, \text{root_r_old}))$
$\line{15} \textsf{assert_eq}(\text{comm_r_old_calc}, \text{comm_r_old})$
$\line{16} \text{comm_r_new_calc} \deq \textsf{poseidon_gadget}((\text{comm_c}, \text{root_r_new}))$
$\line{17} \textsf{assert_eq}(\text{comm_r_new_calc}, \text{comm_r_new})$

$\line{18} \text{apex_tree}: (\Fq^{[\text{A}]}, \Fq^{[A / 2]}, \ldots, \Fq^{[1]}) \deq \textsf{bin_tree_gadget}(\text{apex_leafs})$
$\line{19} \text{apex_root} = \text{apex_tree}[\text{ApexTreeHeight}][0]$
$\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})$

$\line{22} \text{rand_bits}: {{\Fq|_{\{0, 1\}}}^{[\text{RandChallengeBits}]}}^{[\text{C}]} \deq \textsf{gen_challenge_bits_gadget}(\text{comm_r_new}, \text{k})$
$\line{23} \textbf{for } \text{c_rand_bits} \in \text{rand_bits}:$
$\line{24} \quad \text{c_high_and_zeros}: \Fq^{[6]} = ()$
$\line{25} \quad \textbf{for } h, \text{h_select_bit} \in \textbf{zip}(\textbf{Hs}, \text{h_select_bits}):$
$\line{26} \quad\quad \text{c_high_bits} = \text{c_rand_bits}[\text{RandChallengeBits} - h\text{..}]$
$\line{27} \quad\quad \text{c_high} \deq \textsf{lc_gadget}(\sum_{i \in 0\text{..}h} 2^i * \text{c_high_bits}[i])$
$\line{28} \quad\quad \text{c_high_or_zero} \deq \textsf{mul_gadget}(\text{h_select_bit}, \text{c_high})$
$\line{29} \quad\quad \text{c_high_and_zeros}\text{.}\textbf{push}(\text{c_high_or_zero})$
$\line{30} \quad \text{c_high_selected} \deq \textsf{lc_gadget}(\sum_{i \in 0\text{..}6} \text{c_high_and_zeros}[i])$
$\line{31} \quad \text{rho} \deq \textsf{poseidon_gadget}((\text{phi}, \text{c_high_selected}))$