$$$$

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

Notation and Constants

General

$[n]$
The set containing the first

$n$ unsigned integers

$(0,1,\dots ,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\le i<n$.

$x:{\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:{\mathbb{F}}_q$
Indicates that

$x$ is a prime field element, specifically an element of BLS12-381's scalar field having modulus

$q$.

$(a_0,\dots ,a_{n-1})$
An array of

$n$ elements.

$\mathit{a}[i\mathbf{\text{..}}j]$
A slice

$(a_i,\dots ,a_{j-1})$ of the array

$\mathit{a}=(a_0,\dots ,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 \mathbf{\text{Hs}}$
The number of high bits taken from each challenge's [little-endian] binary representation. Filecoin currently defaults to using

$h=10$.

Constants

$\mathbf{\text{const }}A=128$
The number of apex-leafs per partition.

$\mathbf{\text{const }}\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).

$\mathbf{\text{const }}\text{ApexLeafOffset}=\text{NodeBits}-(\text{PartitionBits}+\text{ApexLeafBits})$
The position in a

$\text{TreeDNew}$ Merkle proof which contains an apex-leaf.

$\mathbf{\text{const }}C=86$
The number of challenges per partition.

$\mathbf{\text{const }}\text{ChallengesPerPRF}=\lfloor \frac{\lfloor {\log }_2(q)\rfloor }{\text{RandChallengeBits}}\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

${\mathbb{F}}_q$.

$\mathbf{\text{const }}\mathbf{\text{Hs}}=(7,8,9,10,11,12)$
An array containing the allowed values for

$h$.

$\mathbf{\text{const }}\text{h\_index}=\mathbf{\text{Hs}}\mathsf{\text{.index\_of}}(h)$
The index of the configuration parameter

$h$ in

$\mathbf{\text{Hs}}$.

$\mathbf{\text{const }}\text{h\_select}=2^{\text{h\_index}}$
An integer which encodes

$\text{h\_index}$.

$\mathbf{\text{const }}\text{h\_select\_bits}:{\{0,1\}}^{[\mathbf{\text{len}}(\mathbf{\text{Hs}})]}=\mathsf{\text{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

$\mathbf{\text{Hs}}$.

$\mathbf{\text{const }}\text{k\_and\_h\_select}=k\vee (\text{h\_select}\ll \text{PartitionBits})$
A packed integer containing

$k$ and

$\text{h\_select}$.

$\mathbf{\text{const }}\text{k\_and\_h\_select\_bits}:{\{0,1\}}^{[\text{PartitionBits}+\mathbf{\text{len}}(\mathbf{\text{Hs}})]}=\text{k\_bits}\Vert \text{h\_select\_bits}=\mathsf{\text{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}$.

$\mathbf{\text{const }}\text{k\_bits}:{\{0,1\}}^{[\text{PartitionBits}]}=\mathsf{\text{le\_bits}}(k)$
The binary representation of the chosen partition-index

$k$.

$\mathbf{\text{const }}\text{NodeBits}={\log }_2(\text{SectorNodes})=\{\begin{array}{ll}30& \text{32GiB sector-size}\\ 31& \text{64GiB sector-size}\end{array}$
The number of bits required to specify the index of a node in a sector.

$\mathbf{\text{const }}P=16$
The number of partitions per sector.

$\mathbf{\text{const }}\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).

$\mathbf{\text{const }}\text{PartitionNodes}=\frac{\text{SectorNodes}}{P}=\{\begin{array}{ll}{2}^{26}& \text{32GiB sector-size}\\ 2^{27}& \text{64GiB sector-size}\end{array}$
The number of nodes in each partition of a sector.

$\mathbf{\text{const }}\text{PRFsPerPartition}=\lceil \frac{C}{\text{ChallengesPerPRF}}\rceil =10$
The number of calls to the Poseidon-PRF required to generate a partition's

$C$ challenges.

$\mathbf{\text{const }}\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.

$\mathbf{\text{const }}\text{TreeDHeight}={\log }_2(\text{SectorNodes})$

$\mathbf{\text{const }}\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}}:{{\mathbb{F}}_q}^{[\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}}:{{\mathbb{F}}_q}^{[\text{SectorNodes}]}$
The replica of

$D_{\text{old}}$ output by SDR-PoRep.

$D_{\text{new}}:{{\mathbb{F}}_q}^{[\text{SectorNodes}]}$
The data which is replacing the empty sector data

$D_{\text{old}}$.

$R_{\text{new}}:{{\mathbb{F}}_q}^{[\text{SectorNodes}]}$
The encoding of the new data

$D_{\text{new}}$.

Old and New Merkle Trees and Commitments

$\text{TreeROld}=\text{OctTree}\mathsf{\text{::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}\mathsf{\text{::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}\mathsf{\text{::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}:{\mathbb{F}}_q=\text{Poseidon}((\text{CommC},\text{TreeROld}\mathsf{\text{.root}}))$

$\text{CommDNew}:{\mathbb{F}}_q=\text{TreeDNew}\mathsf{\text{.root}}$

$\text{CommRNew}:{\mathbb{F}}_q=\text{Poseidon}((\text{CommC},\text{TreeRNew}\mathsf{\text{.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

$\mathbf{\text{struct }}\text{BinTreeProof}\{$

$\mathsf{\text{leaf}}:{\mathbb{F}}_q,$

$\mathsf{\text{path}}:{{\mathbb{F}}_q}^{[\text{TreeDHeight}]},$

$\}$
Arity-2 Merkle proof type.

$\mathbf{\text{struct }}\text{OctTreeProof}\{$

$\mathsf{\text{leaf}}:{\mathbb{F}}_q,$

$\mathsf{\text{path}}:{{{\mathbb{F}}_q}^{[7]}}^{[\text{TreeRHeight}]},$

$\}$
Arity-8 Merkle proof type.

Empty-Sector-Update Proof

$\mathbf{\text{struct}}\text{PartitionProof}\{$

$\text{ChallengeProofs},$

$\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.

$\mathbf{\text{struct }}\text{ChallengeProof}\{$

$\mathsf{\text{proof\_r\_old}}:\text{OctTreeProof},$

$\mathsf{\text{proof\_d\_new}}:\text{BinTreeProof},$

$\mathsf{\text{proof\_r\_new}}:\text{OctTreeProof},$

$\}$
Three Merkle proofs are generated per challenge, one for each of the trees

$\text{TreeROld}$,

$\text{TreeDNew}$, and

$\text{TreeRNew}$.

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

$\text{PartitionPath}:{{\mathbb{F}}_q}^{[\text{PartitionTreeHeight}]}=\text{ChallengeProof}\mathsf{\text{.proof\_d\_new}}\mathsf{\text{.path}}[\text{RandChallengeBits}\mathbf{\text{..}}]$
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}:{{\mathbb{F}}_q}^{[A]}=\text{TreeDNew}{\mathsf{\text{.row}}}_{\text{ApexLeafsOffset}}[kA\mathbf{\text{..}}(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\ast 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}\mathsf{\text{.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}\mathsf{\text{.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

${\mathbb{F}}_q$, arity-2, width-3, see Poseidon-PRF gadget 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}\ast 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}=\lfloor \frac{254}{26}\rfloor =\lfloor \frac{254}{27}\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,\dots ,c_8)$ for partition

$k\in [P]$ is generated as follows:

$$\begin{array}{rl}& \text{digest}:{\mathbb{F}}_q=\text{PoseidonPRF}((\text{CommRNew},\text{PRFsPerPartition}\ast k+j))\\ & c_0=\mathsf{\text{le\_bits}}(\text{digest})[0\ast \text{RandChallengeBits}\mathbf{\text{..}}1\ast \text{RandChallengeBits}]\\ & ⋮\\ & c_8=\mathsf{\text{le\_bits}}(\text{digest})[8\ast \text{RandChallengeBits}\mathbf{\text{..}}9\ast \text{RandChallengeBits}]\end{array}$$

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

$\mathsf{\text{le\_bits}}(c)\Vert \mathsf{\text{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 \mathbf{\text{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$:

$$\mathrm{\forall }i\in [P\ast C]:{\text{high}}_i=c_i\gg ({\log }_2(\text{SectorNodes})-h)$$ note that

$P\ast 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}$.

$$\mathrm{\forall }i\in [P\ast 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 for notation.

$$R_{\text{new}}[i]={\text{R}}_{\text{old}}[i]+D_{\text{new}}[i]\ast {\text{rho}}_i$$

Circuit

Notation

$a:{\mathbb{F}}_q\stackrel{\diamond }{=}\mathsf{\text{alloc}}(x)$
Denotes that

$a$ is an allocated value in R1CS having the value

$x$, where

$x$ is an unallocated value.

$a:{\mathbb{F}}_q\stackrel{\diamond }{=}\mathsf{\text{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.

${\mathbb{F}}_q$
A BLS12-381 scalar field element allocated in R1CS.

${\mathbb{F}}_2$
A boolean constrained BLS12-381 scalar field element allocated in R1CS.

Implementation

$\stackrel{―}{\underset{―}{\mathbf{\text{Circuit:}}\text{SDR Empty Sector Update}}}$

$\mathbf{\text{\#}}\text{Public-inputs}$

$1.\phantom{10.}\text{comm\_r\_old}\stackrel{\diamond }{=}\mathsf{\text{alloc\_pub}}({\text{CommROld}}_{\text{pub}})$

$2.\phantom{10.}\text{comm\_d\_new}\stackrel{\diamond }{=}\mathsf{\text{alloc\_pub}}({\text{CommDNew}}_{\text{pub}})$

$3.\phantom{10.}\text{comm\_r\_new}\stackrel{\diamond }{=}\mathsf{\text{alloc\_pub}}({\text{CommRNew}}_{\text{pub}})$

$\mathbf{\text{\#}}\text{Unpack k and h\_select from their packed public-input}$

$4.\phantom{10.}\text{k\_and\_h\_select}\stackrel{\diamond }{=}\mathsf{\text{alloc\_pub}}({\text{k\_and\_h\_select}}_{\text{pub}})$

$5.\phantom{10.}\text{k\_and\_h\_select\_bits}:{{\mathbb{F}}_2}^{[\text{PartitionBits}+\mathbf{\text{len}}(\mathbf{\text{Hs}})]}\stackrel{\diamond }{=}\mathsf{\text{le\_bits\_gadget}}(\text{k\_and\_h\_select})$

$6.\phantom{10.}\text{k\_bits}:{{\mathbb{F}}_2}^{[\text{PartitionBits}]}=\text{k\_and\_h\_select\_bits}[\mathbf{\text{..}}\text{PartitionBits}]$

$7.\phantom{10.}\text{h\_select\_bits}:{{\mathbb{F}}_2}^{[\mathbf{\text{len}}(\mathbf{\text{Hs}})]}=\text{k\_and\_h\_select\_bits}[\text{PartitionBits}\mathbf{\text{..}}]$

$8.\phantom{10.}\text{k}\stackrel{\diamond }{=}\mathsf{\text{lc\_gadget}}(\sum _{i\in [\text{PartitionBits}]}{2}^i\ast \text{k\_bits}[i])\mathbf{\text{\#}}{2}^i\text{ is an unallocated constant}$

$\mathbf{\text{\#}}\text{Compute phi for this sector}$

$9.\phantom{10.}\text{phi}\stackrel{\diamond }{=}\mathsf{\text{poseidon\_prf\_gadget}}((\text{comm\_d\_new},\text{comm\_r\_old}))$

$\mathbf{\text{\#}}\text{Verify the roots of TreeROld and TreeRNew against public commitments}$

$10.\phantom{10.}\text{comm\_c}\stackrel{\diamond }{=}\mathsf{\text{alloc}}({\text{CommC}}_{\text{priv}})$

$11.\phantom{10.}\text{root\_r\_old}\stackrel{\diamond }{=}\mathsf{\text{alloc}}({\text{RootROld}}_{\text{priv}})$

$12.\phantom{10.}\text{root\_r\_new}\stackrel{\diamond }{=}\mathsf{\text{alloc}}({\text{RootRNew}}_{\text{priv}})$

$13.\phantom{10.}\text{comm\_r\_old\_calc}\stackrel{\diamond }{=}\mathsf{\text{poseidon\_gadget}}((\text{comm\_c},\text{root\_r\_old}))$

$14.\phantom{10.}\text{comm\_r\_new\_calc}\stackrel{\diamond }{=}\mathsf{\text{poseidon\_gadget}}((\text{comm\_c},\text{root\_r\_new}))$

$15.\phantom{10.}\mathsf{\text{assert\_eq}}(\text{comm\_r\_old\_calc},\text{comm\_r\_old})$

$16.\phantom{10.}\mathsf{\text{assert\_eq}}(\text{comm\_r\_new\_calc},\text{comm\_r\_new})$

$\mathbf{\text{\#}}\text{Verify the witnessed apex-leafs against the public commitment CommDNew}$

$17.\phantom{10.}\text{apex\_leafs}:{{\mathbb{F}}_q}^{[\text{ApexLeafs}]}\stackrel{\diamond }{=}(\mathsf{\text{alloc}}({\text{ApexLeafs}}_{\text{priv}}[i])\mid i\in [\text{ApexLeafs}])$

$18.\phantom{10.}\text{apex\_root}\stackrel{\diamond }{=}\mathsf{\text{apex\_root\_gadget}}(\text{apex\_leafs})$

$19.\phantom{10.}\text{partition\_path}:{{\mathbb{F}}_q}^{[\text{PartitionTreeHeight}]}\stackrel{\diamond }{=}(\mathsf{\text{alloc}}({\text{PartitionPath}}_{\text{priv}}[i])\mid i\in [\text{PartitionTreeHeight}])$

$20.\phantom{10.}\text{comm\_d\_new\_calc}\stackrel{\diamond }{=}\mathsf{\text{bintree\_root\_gadget}}(\text{k\_bits},\text{apex\_root},\text{partition\_path})$

$21.\phantom{10.}\mathsf{\text{assert\_eq}}(\text{comm\_d\_new\_calc},\text{comm\_d\_new})$

$\mathbf{\text{\#}}\text{Generate this partition's challenges}$

$22.\phantom{10.}\text{rand\_challenge\_bits}:{{{\mathbb{F}}_2}^{[\text{RandChallengeBits}]}}^{[C]}\stackrel{\diamond }{=}\mathsf{\text{gen\_challenge\_bits\_gadget}}(\text{comm\_r\_new},\text{k})$

$\mathbf{\text{\#}}\text{Verify each challenge's Merkle proofs}$

$23.\phantom{10.}\mathbf{\text{for }}i\in [C]\mathbf{\text{:}}$

$24.\phantom{10.}(\text{proof\_r\_old},\text{proof\_d\_new},\text{proof\_r\_new})\leftarrow {\text{ChallengeProofs}}_{\text{priv}}[i]$

$\mathbf{\text{\#}}\text{Get this challenge's binary representation}$

$25.\phantom{10.}\text{challenge\_sans\_partition\_bits}:{{\mathbb{F}}_2}^{[\text{RandChallengeBits}]}=\text{rand\_challenge\_bits}[i]$

$26.\phantom{10.}\text{challenge\_bits}:{{\mathbb{F}}_2}^{[\text{NodeBits}]}=\text{challenge\_sans\_partition\_bits}\Vert \text{k\_bits}$

$\mathbf{\text{\#}}\text{Calculate this challenge's encoding}$

$27.\phantom{10.}\text{high}\stackrel{\diamond }{=}\mathsf{\text{get\_high\_bits\_gadget}}(\text{challenge\_bits},\text{h\_select\_bits})$

$28.\phantom{10.}\text{rho}\stackrel{\diamond }{=}\mathsf{\text{poseidon\_prf\_gadget}}((\text{phi},\text{high}))$

$29.\phantom{10.}\text{leaf\_r\_old}\stackrel{\diamond }{=}\mathsf{\text{alloc}}(\text{proof\_r\_old}\mathsf{\text{.leaf}})$

$30.\phantom{10.}\text{leaf\_d\_new}\stackrel{\diamond }{=}\mathsf{\text{alloc}}(\text{proof\_d\_new}\mathsf{\text{.leaf}})$

$31.\phantom{10.}\text{leaf\_d\_new\_rho}\stackrel{\diamond }{=}\mathsf{\text{mul\_gadget}}(\text{rho},\text{leaf\_d\_new})$

$32.\phantom{10.}\text{leaf\_r\_new}\stackrel{\diamond }{=}\mathsf{\text{add\_gadget}}(\text{leaf\_r\_old},\text{leaf\_d\_new\_rho})$

$\mathbf{\text{\#}}\text{Get this challenge's apex-leaf from the array of validated apex-leafs}$

$33.\phantom{10.}\text{apex\_leaf\_bits}:{{\mathbb{F}}_2}^{[\text{ApexLeafBits}]}=\text{challenge\_sans\_partition\_bits}[\text{ApexLeafOffset}\mathbf{\text{..}}]$

$34.\phantom{10.}\text{apex\_leaf}\stackrel{\diamond }{=}\mathsf{\text{select\_gadget}}(\text{apex\_leafs},\text{apex\_leaf\_bits})$

$\mathbf{\text{\#}}\text{Verify this challenge's TreeDNew Merkle proof up to the apex-leaf}$

$35.\phantom{10.}\text{below\_apex\_leaf\_bits}:{{\mathbb{F}}_2}^{[\text{ApexLeafOffset}]}=\text{challenge\_sans\_partition\_bits}[\mathbf{\text{..}}\text{ApexLeafOffset}]$

$36.\phantom{10.}\text{below\_apex\_leaf\_path}:{{\mathbb{F}}_q}^{[\text{ApexLeafOffset}]}\stackrel{\diamond }{=}(\mathsf{\text{alloc}}(\text{proof\_d\_new}\mathsf{\text{.path}}[i])\mid i\in [\text{ApexLeafOffset}])$

$37.\phantom{10.}\text{apex\_leaf\_calc}:{\mathbb{F}}_q\stackrel{\diamond }{=}\mathsf{\text{bintree\_root\_gadget}}($

$\phantom{71.\phantom{10.}}\text{below\_apex\_leaf\_bits},$

$\phantom{72.\phantom{10.}}\text{leaf\_d\_new},$

$\phantom{73.\phantom{10.}}\text{below\_apex\_leaf\_path},$

$\phantom{74.\phantom{10.}})$

$38.\phantom{10.}\mathsf{\text{assert\_eq}}(\text{apex\_leaf\_calc},\text{apex\_leaf})$

$\mathbf{\text{\#}}\text{Verify this challenge's TreeROld Merkle proof}$

$39.\phantom{10.}\text{path\_r\_old}:{{{\mathbb{F}}_q}^{[7]}}^{[\text{TreeRHeight}]}\stackrel{\diamond }{=}((\mathsf{\text{alloc}}(\text{proof\_r\_old}\mathsf{\text{.path}}[h][s])\mid s\in [7])\mid h\in [\text{TreeRHeight}])$

$40.\phantom{10.}\text{root\_r\_old\_calc}\stackrel{\diamond }{=}\mathsf{\text{octtree\_root\_gadget}}(\text{challenge\_bits},\text{leaf\_r\_old},\text{path\_r\_old})$

$41.\phantom{10.}\mathsf{\text{assert\_eq}}(\text{root\_r\_old\_calc},\text{root\_r\_old})$

$\mathbf{\text{\#}}\text{Verify this challenge's TreeRNew Merkle proof}$

$42.\phantom{10.}\text{path\_r\_new}:{{{\mathbb{F}}_q}^{[7]}}^{[\text{TreeRHeight}]}\stackrel{\diamond }{=}((\mathsf{\text{alloc}}(\text{proof\_r\_new}\mathsf{\text{.path}}[h][s])\mid s\in [7])\mid h\in [\text{TreeRHeight}])$

$43.\phantom{10.}\text{root\_r\_new\_calc}\stackrel{\diamond }{=}\mathsf{\text{bintree\_root\_gadget}}(\text{challenge\_bits},\text{leaf\_r\_new},\text{path\_r\_new})$

$44.\phantom{10.}\mathsf{\text{assert\_eq}}(\text{root\_r\_new\_calc},\text{root\_r\_new})$

Gadgets

$\mathsf{\text{add\_gadget}}(x:{\mathbb{F}}_q,y:{\mathbb{F}}_q)\to {\mathbb{F}}_q$
Allocates and returns the value

$z=x+y$ and adds the R1CS constraint

$(x+y)\ast (1)=z$.

$\mathsf{\text{mul\_gadget}}(x:{\mathbb{F}}_q,y:{\mathbb{F}}_q)\to {\mathbb{F}}_q$
Allocates and returns the value

$z=x\ast y$ and adds the R1CS constraint

$(x)\ast (y)=z$.

$\mathsf{\text{lc\_gadget}}(c_1{x}_1+\dots +c_n{x}_n)\to {\mathbb{F}}_q$
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_1{x}_1+\dots +c_n{x}_n)\ast (1)=y$.

$\mathsf{\text{sum\_gadget}}((x_1,\dots ,x_n))\to {\mathbb{F}}_q$
Allocates and returns the the sum of the array of allocated values

$(x_1,\dots ,x_n)$. Equivalent to calling

$\mathsf{\text{lc\_gadget}}(\sum _{i\in [n]}1\ast x_i)$.

$\mathsf{\text{le\_bits\_gadget}}(x:{\mathbb{F}}_q)\to {{\mathbb{F}}_2}^{[n]}$
Allocates and returns the little-endian binary representation of the allocated value

$x$. This gadget allocates

$n$ boolean constrained values

$(b_0,\dots ,b_{n-1})$ in R1CS (adding one boolean constraint per bit) and adds the constraint

$(2^0{b}_0+\dots +2^{n-1}{b}_{n-1})\ast (1)=x$ where each

$2^i$ is an unallocated constant.

Poseidon and Poseidon-PRF

$\mathsf{\text{poseidon\_gadget}}(\text{preimage}:{{\mathbb{F}}_q}^{[2]})\to {\mathbb{F}}_q$
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}$.

$\mathsf{\text{poseidon\_prf\_gadget}}(\text{preimage}:{{\mathbb{F}}_q}^{[2]})\to {\mathbb{F}}_q$
Uses Poseidon as a pseudorandom function (PRF). This gadget is identical to

$\mathsf{\text{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.

$\stackrel{―}{\underset{―}{\mathbf{\text{Gadget:}}\mathsf{\text{apex\_root\_gadget}}(\text{apex\_leafs}:{{\mathbb{F}}_q}^{[A]})\to {\mathbb{F}}_q}}$

$1.\phantom{10.}\text{row}=\text{apex\_leafs}$

$2.\phantom{10.}\mathbf{\text{while }}\mathbf{\text{len}}(\text{row})>1\mathbf{:}$

$3.\phantom{10.}\text{row}:{{\mathbb{F}}_q}^{[\mathbf{\text{len}}(\text{row})/2]}\stackrel{\diamond }{=}(\mathsf{\text{sha256\_gadget}}((\text{row}[2i],\text{values}[2i+1]))\mid i\in [\mathbf{\text{len}}(\text{row})/2])$

$4.\phantom{10.}\mathbf{\text{return }}\text{row}[0]$

Challenge Generation

Generates

$C$ random challenges for partition

$k$ of the updated sector corresponding to

$\text{CommRNew}$.

$\stackrel{―}{\underset{―}{\mathbf{\text{Gadget:}}\mathsf{\text{gen\_challenge\_bits\_gadget}}(\text{comm\_r\_new}:{\mathbb{F}}_q,k:{\mathbb{F}}_q)\to {{{\mathbb{F}}_2}^{[\text{RandChallengeBits}]}}^{[C]}}}$

$1.\phantom{10.}\text{rand\_challenge\_bits}:{{{\mathbb{F}}_2}^{[\text{RandChallengeBits}]}}^{[C]}=()$

$2.\phantom{10.}\mathbf{\text{for }}i\in [\text{PRFsPerPartition}]\mathbf{:}$

$3.\phantom{10.}\text{digest\_index}\stackrel{\diamond }{=}\mathsf{\text{lc\_gadget}}(\text{PRFsPerPartition}\ast k+i\ast \text{R1CS}\mathsf{\text{.one}})\mathbf{\text{\#}}\text{PRFsPerPartition}\text{and}i\text{are unallocated constants}$

$4.\phantom{10.}\text{digest}\stackrel{\diamond }{=}\mathsf{\text{poseidon\_prf\_gadget}}((\text{comm\_r\_new},\text{digest\_index}))$

$5.\phantom{10.}\text{digest\_bits}:{{\mathbb{F}}_2}^{[255]}\stackrel{\diamond }{=}\mathsf{\text{le\_bits\_gadget}}(\text{digest})\mathbf{\text{\#}}255=\lceil {\log }_2(q)\rceil \text{is the bit-length of }{\mathbb{F}}_q$

$\mathbf{\text{\#}}\text{Chunk digest\_bits by challenge (chunks of size RandChallengeBits)}$

$6.\phantom{10.}\mathbf{\text{for }}j\in [\text{ChallengesPerPRF}]\mathbf{:}$

$7.\phantom{10.}\text{challenge\_bits}:{{\mathbb{F}}_2}^{[\text{RandChallengeBits}]}=\text{digest\_bits}[j\ast \text{RandChallengeBits}\mathbf{\text{..}}(j+1)\text{RandChallengeBits}]$

$8.\phantom{10.}\text{rand\_challenge\_bits}\mathsf{\text{.push}}(\text{challenge\_bits})$

$\mathbf{\text{\#}}\text{Truncate the return value because the last PRF adds more challenges than necessary}$

$9.\phantom{10.}\mathbf{\text{return }}\text{rand\_challenge\_bits}[\mathbf{\text{..}}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

$\mathbf{\text{Hs}}$ via

$\text{h\_select\_bits}$.

$\stackrel{―}{\underset{―}{\mathbf{\text{Gadget:}}\mathsf{\text{get\_high\_bits\_gadget}}(\text{challenge\_bits}:{{\mathbb{F}}_2}^{[\text{NodeBits}]},\text{h\_select\_bits}:{{\mathbb{F}}_2}^{[\mathbf{\text{len}}(\mathbf{\text{Hs}})]})\to {\mathbb{F}}_q}}$

$1.\phantom{10.}\text{scaled\_highs}:{{\mathbb{F}}_q}^{[\mathbf{\text{len}}(\mathbf{\text{Hs}})]}=()$

$2.\phantom{10.}\mathbf{\text{for }}(h,\text{h\_select\_bit})\in \mathbf{\text{zip}}(\mathbf{\text{Hs}},\text{h\_select\_bits})\mathbf{:}$

$\mathbf{\text{\#}}\text{Pack the }h\text{ high bits of challenge\_bits into a single }{\mathbb{F}}_q$

$3.\phantom{10.}\text{high\_bits}=\text{challenge\_bits}[\text{NodeBits}-h\mathbf{\text{..}}]$

$4.\phantom{10.}\text{high}\stackrel{\diamond }{=}\mathsf{\text{lc\_gadget}}(\sum _{i\in [h]}{2}^i\ast \text{high\_bits}[i])\mathbf{\text{\#}}\text{Note: }{2}^i\text{ is an unallocated constant}$

$\mathbf{\text{\#}}\text{Scale by }0\text{ or }1$

$5.\phantom{10.}\text{high\_or\_zero}\stackrel{\diamond }{=}\mathsf{\text{mul\_gadget}}(\text{high},\text{h\_select\_bit})$

$6.\phantom{10.}\text{scaled\_highs}\mathsf{\text{.push}}(\text{high\_or\_zero})$

$\mathbf{\text{\#}}\text{The sum of the scaled values is the selected high value}$

$7.\phantom{10.}\text{selected\_high}\stackrel{\diamond }{=}\mathsf{\text{sum\_gadget}}(\text{scaled\_highs})$

$8.\phantom{10.}\mathbf{\text{return }}\text{selected\_high}$