$$ \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 ![](https://i.imgur.com/UffNh5W.png) $\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). ![](https://i.imgur.com/e1a0NGm.png) ### 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}$
Last changed by  
 
Jake

Read more

Synth-PoRep Spec

$$ \def\C{\text{C}} \def\Csyn{\text{C}^{\text{syn}}} \def\N{\text{N}} \def\Nsyn{\text{N}^\text{syn}} \def\Ch{\text{Ch}} \def\csyn_#1{c^\text{syn}_{#1}} \def\Bit{{0, 1}} \def\par{\mathbin\Vert} \def\TreeD{\text{TreeD}}

3/10/2023
PLONK Arithmetization

$$ \def\Zp{{\mathbb{Z}_p}} \def\F{{\mathbb{F}}} \def\Bit{{{0, 1}}} \def\PI{{\textsf{PI}}} \def\bold#1{\boldsymbol{#1}} \def\stop{{\rlap{\quad.}\hphantom{}}} \def\qed{{\rlap{\quad \tiny\blacksquare}\hphantom{}}} \def\par{{\thinspace {\parallel} \thinspace}} \def\hso{{\hspace{1pt}}}

10/7/2022
Halo2 Circuits

Groth16 Uses R1CS Arithmetization R1CS encodes an arithmetic computation (addition and multiplication). $\text{Public Inputs: } (1, x_1, \dots, x_m)$ $\text{Private Inputs: } (x_{m + 1}, \dots, x_n)$ $\text{Constraints: }(A_1B_1 = C_1, \dots, A_kB_k = C_k)$ Variables $x_i$ are stored in two vectors (public and private). A constraint is a degree-1 or degree-2 polynomial equation: $\text{polynomial}_A * \text{polynomial}_B = \text{polynomial}_C$

10/7/2022
Circuit-Efficient Labeling

During sealing, we perform a labeling function for each node in each layer (sha256 of a 20-block preimage). let label = sha256([ replica_id, // 0.5 blocks layer_index, // 0.25 blocks node, // 0.25 blocks parent_1_label, // 0.5 blocks ..., parent_37_label, // 0.5 blocks ]);

9/10/2022
Read more from Jake
Published on HackMD