Try   HackMD

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

Notation and Constants

General

[n]
The set containing the first
n
unsigned integers
(0,1,,n1)
.

i[n]
Indicates that
i
is an index pointing to an element in an array of
n
elements; equivalent to
iZ
where
0i<n
.

x:SomeType[n]
Indicates that the value
x
is an array of length
n
where each element of the array is of type
SomeType
.

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

(a0,,an1)
An array of
n
elements.

\boldsymbola[i..j]
A slice
(ai,,aj1)
of the array
\boldsymbola=(a0,,an1)
.

Configuration Parameters

SectorNodes{230,231}
The number of nodes in the sector; allowed sector sizes are 32GiB and 64GiB.

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

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

Constants

const A=128
The number of apex-leafs per partition.

const ApexLeafBits,ApexTreeHeight=log2(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).

const ApexLeafOffset=NodeBits(PartitionBits+ApexLeafBits)
The position in a
TreeDNew
Merkle proof which contains an apex-leaf.

const C=86
The number of challenges per partition.

const ChallengesPerPRF=log2(q)RandChallengeBits=9
The maximum number of challenges which can be derived from a single Poseidon digest when Poseidon is used as a pseudorandom function (PRF).
log2(q)=254
is the number of fully utilized bits in a field element
Fq
.

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

const h_index=Hs.index_of(h)
The index of the configuration parameter
h
in
Hs
.

const h_select=2h_index
An integer which encodes
h_index
.

const h_select_bits:{0,1}[len(Hs)]=le_bits(h_select)
The binary representation of
h_select
. Note that exactly one bit in
h_select_bits
is set which gives the index (
h_index
) of the chosen
h
in
Hs
.

const k_and_h_select=k(h_selectPartitionBits)
A packed integer containing
k
and
h_select
.

const k_and_h_select_bits:{0,1}[PartitionBits+len(Hs)]=k_bitsh_select_bits=le_bits(k_and_h_select)
The binary representation of
k_and_h_select
. The first bit is the least-significant of
k_bits
and last bit is the most-significant of
h_select
.

const k_bits:{0,1}[PartitionBits]=le_bits(k)
The binary representation of the chosen partition-index
k
.

const NodeBits=log2(SectorNodes)={3032GiB sector-size3164GiB sector-size
The number of bits required to specify the index of a node in a sector.

const P=16
The number of partitions per sector.

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

const PartitionNodes=SectorNodesP={22632GiB sector-size22764GiB sector-size
The number of nodes in each partition of a sector.

const PRFsPerPartition=CChallengesPerPRF=10
The number of calls to the Poseidon-PRF required to generate a partition's
C
challenges.

const RandChallengeBits=log2(PartitionNodes)=NodeBitsPartitionBits
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
kth
partition of the sector, i.e. the first
RandChallengeBits
bits of each challenge are randomly chosen and the last
PartitionBits
bits of each challenge are the same.

const TreeDHeight=log2(SectorNodes)
const TreeRHeight=log8(SectorNodes)

The heights of trees that have been generated over a sector of values.
TreeD
's are arity-2 and use
Sha256
, whereas
TreeR
's are arity-8 and use
Poseidon
. Note that adding 1 to a tree's height (for the leafs)
height+1
gives the number of "rows" in the tree.

Old and New Sectors

Dold:Fq[SectorNodes]
An empty sector of data input to SDR-PoRep. Note that
Dnew
is not used by the empty-sector-update proof.

Rold:Fq[SectorNodes]
The replica of
Dold
output by SDR-PoRep.

Dnew:Fq[SectorNodes]
The data which is replacing the empty sector data
Dold
.

Rnew:Fq[SectorNodes]
The encoding of the new data
Dnew
.

Old and New Merkle Trees and Commitments

TreeROld=OctTree::from_leaves(Rold)
An arity-8 Merkle tree built over the replica
Rold
output by running SDR-PoRep on an empty sector
Dold
.

TreeDNew=BinTree::from_leaves(Dnew)
An arity-2 Merkle tree built over the data
Dnew
which is replacing that of the old empty sector
Dold
.

TreeRNew=OctTree::from_leaves(Rnew)
An arity-8 Merkle tree built over the empty-sector-update encoding
Rnew
of the new sector data
Dnew
.

CommROld:Fq=Poseidon((CommC,TreeROld.root))
CommDNew:Fq=TreeDNew.root

CommRNew:Fq=Poseidon((CommC,TreeRNew.root))

Commitments to three Merkle trees. Note that
CommC
is a commitment which was generated by SDR-PoRep when encoding
Dold
into
Rold
.

Merkle Proofs

struct BinTreeProof {
leaf:Fq,

path:Fq[TreeDHeight],

}

Arity-2 Merkle proof type.

struct OctTreeProof {
leaf:Fq,

path:Fq[7][TreeRHeight],

}

Arity-8 Merkle proof type.

Empty-Sector-Update Proof

struct PartitionProof {
ChallengeProofs,

ApexLeafs,

}

Represents an empty-sector-update proof. One
PartitionProof
is generated for each partition
k
of an updated sector, thus
P
number of
PartitionProof
's are generated per updated sector.
C
number of challenges are generated per partition, thus each
PartitionProof
contains
C
number of
ChallengeProof
's.

struct ChallengeProof {
proof_r_old:OctTreeProof,

proof_d_new:BinTreeProof,

proof_r_new:OctTreeProof,

}

Three Merkle proofs are generated per challenge, one for each of the trees
TreeROld
,
TreeDNew
, and
TreeRNew
.

ChallengeProofs:ChallengeProof[C]
Denotes all Merkle proofs generated for a partition.

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

ApexLeafs:Fq[A]=TreeDNew.rowApexLeafsOffset[kA..(k+1)A]
The
kth
partition's apex-leafs, i.e. the
kth
chunk of
A
nodes from the
TreeDNew
row containing
PA
values.

TreeDNew, Apex-Tree, and Partition-Tree

ApexTree and
PartitionTree
are sub-trees of a sector's
TreeDNew
. Each
TreeDNew
has exactly one
PartitionTree
(the top 5 rows of
TreeDNew
) and
P
unique
ApexTree
's (one for each partition). The root of the
kth
partition's
ApexTree
is the
kth
leaf in
PartitionTree
.

Each Merkle challenge is the index of a node in a sector, thus challenges are either 30 or 31 bits (32GiB sectors contain

230 nodes, 64GiB sectors contain
231
nodes).

Partition Trees

The last

PartitionBits=log2(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

TreeDNew Merkle proof validation to hash from a partition's apex-root up to
TreeDNew.root
.

The top

4+1=5 rows of
TreeDNew
are a sub-tree (of height 4) called
PartitionTree
whose leafs are a sector's apex-roots and whose root is
TreeDNew.root
.

Apex Trees

The

ApexLeafBits=log2(A)=7 bits preceding a challenge's partition bits represent the index of the challenge's apex-leaf in the partition's
ApexLeafs
.

Apex-leaf bits are used during

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

ApexLeafOffset=NodeBits(PartitionBits+ApexLeafBits) bits, are used during
TreeDNew
Merkle proof validation to hash from the challenge's leaf in
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
SectorNodes=230
or
231
number nodes) by calling Poseidon-PRF (128-bit security level, prime field
Fq
, arity-2, width-3, see Poseidon-PRF gadget for domain separation tag)
PRFsPerPartition=10
number of times to generate the binary representation of each of the partition's challenges.

The preimage for each

j[PRFsPerPartition] call to Poseidon-PRF in a partition is the concatenation of the unique identifier
CommRNew
associated with the updated sector and the unique index of the PRF call in the sector
PRFsPerPartitionk+j
.

The number of fully utilized bits in a Poseidon digest is

q=254; if a sector partition contains
PartitionNodes=226
(32GiB sector-size) or
227
(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
ChallengesPerPRF=25426=25427=9
. We denote
RandChallengeBits=log2(PartitionNodes)=26
or
27
as the number of bits taken from a PRF digest for each challenge.

The

jth chunk of
ChallengesPerPRF
challenges
(c0,,c8)
for partition
k[P]
is generated as follows:

digest:Fq=PoseidonPRF((CommRNew,PRFsPerPartitionk+j))c0=le_bits(digest)[0RandChallengeBits..1RandChallengeBits]c8=le_bits(digest)[8RandChallengeBits..9RandChallengeBits]

A challenge

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

Phi, Rho, and Labeling

We assign a value

phi for each updated sector:
phi=PoseidonPRF((CommDNew,CommROld))
where
CommROld
is a commitment to the empty sector's SDR replica and
CommDNew
is a commitment to the new data which will overwrite the empty sector.

The Empty-Sector-Update algorithm takes a configuration parameter

hHs which specifies the number of high (i.e. most-significant) bits taken from each challenge's
ci
binary representation denoted
highi
:
i[PC]:highi=ci(log2(SectorNodes)h)
note that
PC
is the total number of challenges per sector.

For each challenge

ci, a value
rhoi
is computed from the challenge's
h
high bits
highi
and the sector's
phi
.
i[PC]:rhoi=PoseidonPRF((phi,highi))

rhoi is used to compute the encoding of the
ith
node's new data, see Old and New Sectors for notation.
Rnew[i]=Rold[i]+Dnew[i]rhoi

Circuit

Notation

a:Fq=alloc(x)
Denotes that
a
is an allocated value in R1CS having the value
x
, where
x
is an unallocated value.

a:Fq=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.

F2
A boolean constrained BLS12-381 scalar field element allocated in R1CS.

Implementation

Circuit: SDR Empty Sector Update  
#  Public-inputs

1.10.  comm_r_old=alloc_pub(CommROldpub)

2.10.  comm_d_new=alloc_pub(CommDNewpub)

3.10.  comm_r_new=alloc_pub(CommRNewpub)

#  Unpack k and h_select from their packed public-input
4.10.  k_and_h_select=alloc_pub(k_and_h_selectpub)

5.10.  k_and_h_select_bits:F2[PartitionBits+len(Hs)] =le_bits_gadget(k_and_h_select)

6.10.  k_bits:F2[PartitionBits]=k_and_h_select_bits[..PartitionBits]

7.10.  h_select_bits:F2[len(Hs)]=k_and_h_select_bits[PartitionBits..]

8.10.  k=lc_gadget(i[PartitionBits]2ik_bits[i])# 2i is an unallocated constant

#  Compute phi for this sector
9.10.  phi=poseidon_prf_gadget((comm_d_new,comm_r_old))

#  Verify the roots of TreeROld and TreeRNew against public commitments
10.10.  comm_c=alloc(CommCpriv)

11.10.  root_r_old=alloc(RootROldpriv)

12.10.  root_r_new=alloc(RootRNewpriv)

13.10.  comm_r_old_calc=poseidon_gadget((comm_c,root_r_old))

14.10.  comm_r_new_calc=poseidon_gadget((comm_c,root_r_new))

15.10.  assert_eq(comm_r_old_calc,comm_r_old)

16.10.  assert_eq(comm_r_new_calc,comm_r_new)

#  Verify the witnessed apex-leafs against the public commitment CommDNew
17.10.  apex_leafs:Fq[ApexLeafs]=(alloc(ApexLeafspriv[i])i[ApexLeafs])

18.10.  apex_root=apex_root_gadget(apex_leafs)

19.10.  partition_path:Fq[PartitionTreeHeight]=(alloc(PartitionPathpriv[i])i[PartitionTreeHeight])

20.10.  comm_d_new_calc=bintree_root_gadget(k_bits,apex_root,partition_path)

21.10.  assert_eq(comm_d_new_calc,comm_d_new)

#  Generate this partition's challenges
22.10.  rand_challenge_bits:F2[RandChallengeBits][C]=gen_challenge_bits_gadget(comm_r_new,k)

#  Verify each challenge's Merkle proofs
23.10.  for i[C]:

24.10.  (proof_r_old,proof_d_new,proof_r_new)ChallengeProofspriv[i]

  # Get this challenge's binary representation
25.10.  challenge_sans_partition_bits:F2[RandChallengeBits]=rand_challenge_bits[i]

26.10.  challenge_bits:F2[NodeBits]=challenge_sans_partition_bitsk_bits

  # Calculate this challenge's encoding
27.10.  high=get_high_bits_gadget(challenge_bits,h_select_bits)

28.10.  rho=poseidon_prf_gadget((phi,high))

29.10.  leaf_r_old=alloc(proof_r_old.leaf)

30.10.  leaf_d_new=alloc(proof_d_new.leaf)

31.10.  leaf_d_new_rho=mul_gadget(rho,leaf_d_new)

32.10.  leaf_r_new=add_gadget(leaf_r_old,leaf_d_new_rho)

  # Get this challenge's apex-leaf from the array of validated apex-leafs
33.10.  apex_leaf_bits:F2[ApexLeafBits]=challenge_sans_partition_bits[ApexLeafOffset..]

34.10.  apex_leaf=select_gadget(apex_leafs,apex_leaf_bits)

  # Verify this challenge's TreeDNew Merkle proof up to the apex-leaf
35.10.  below_apex_leaf_bits:F2[ApexLeafOffset]=challenge_sans_partition_bits[..ApexLeafOffset]

36.10.  below_apex_leaf_path:Fq[ApexLeafOffset]=(alloc(proof_d_new.path[i])i[ApexLeafOffset])

37.10.  apex_leaf_calc:Fq=bintree_root_gadget(

71.10.  below_apex_leaf_bits,

72.10.  leaf_d_new,

73.10.  below_apex_leaf_path,

74.10.  )

38.10.  assert_eq(apex_leaf_calc,apex_leaf)

  # Verify this challenge's TreeROld Merkle proof
39.10.  path_r_old:Fq[7][TreeRHeight]=((alloc(proof_r_old.path[h][s])s[7])h[TreeRHeight])

40.10.  root_r_old_calc=octtree_root_gadget(challenge_bits,leaf_r_old,path_r_old)

41.10.  assert_eq(root_r_old_calc,root_r_old)

  # Verify this challenge's TreeRNew Merkle proof
42.10.  path_r_new:Fq[7][TreeRHeight]=((alloc(proof_r_new.path[h][s])s[7])h[TreeRHeight])

43.10.  root_r_new_calc=bintree_root_gadget(challenge_bits,leaf_r_new,path_r_new)

44.10.  assert_eq(root_r_new_calc,root_r_new)

Gadgets

add_gadget(x:Fq,y:Fq)Fq
Allocates and returns the value
z=x+y
and adds the R1CS constraint
(x+y)(1)=z
.

mul_gadget(x:Fq,y:Fq)Fq
Allocates and returns the value
z=xy
and adds the R1CS constraint
(x)(y)=z
.

lc_gadget(c1x1++cnxn)Fq
Allocates and returns the evaluation
y
of the provided linear-combination; each
xi
is a value allocated in R1CS and each
ci
is an unallocated constant by which
xi
is scaled. This gadget adds the R1CS constraint
(c1x1++cnxn)(1)=y
.

sum_gadget((x1,,xn))Fq
Allocates and returns the the sum of the array of allocated values
(x1,,xn)
. Equivalent to calling
lc_gadget(i[n]1xi)
.

le_bits_gadget(x:Fq)F2[n]
Allocates and returns the little-endian binary representation of the allocated value
x
. This gadget allocates
n
boolean constrained values
(b0,,bn1)
in R1CS (adding one boolean constraint per bit) and adds the constraint
(20b0++2n1bn1)(1)=x
where each
2i
is an unallocated constant.

Poseidon and Poseidon-PRF

poseidon_gadget(preimage:Fq[2])Fq
Given an allocated array of two field elements (
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
2arity1=3
and the remaining two elements of the initial state are
preimage
.

poseidon_prf_gadget(preimage:Fq[2])Fq
Uses Poseidon as a pseudorandom function (PRF). This gadget is identical to
poseidon_gadget
except that here we use a "custom" Poseidon domain separation tag of
240
.

Apex-Root

Creates an arity-2 SHA256 Merkle tree in R1CS from the leafs

apex_leafs and returns the root as an allocated value.

Gadget: apex_root_gadget(apex_leafs:Fq[A])Fq
1.10.  row=apex_leafs

2.10.  while len(row)>1\boldsymbol:

3.10.  row:Fq[len(row)/2]=(sha256_gadget((row[2i],values[2i+1]))i[len(row)/2])

4.10.  return row[0]

Challenge Generation

Generates

C random challenges for partition
k
of the updated sector corresponding to
CommRNew
.

Gadget: gen_challenge_bits_gadget(comm_r_new:Fq,k:Fq)F2[RandChallengeBits][C]
1.10.  rand_challenge_bits:F2[RandChallengeBits][C]=( )

2.10.  for i[PRFsPerPartition]\boldsymbol:

3.10.  digest_index=lc_gadget(PRFsPerPartitionk+iR1CS.one)# PRFsPerPartition and i are unallocated constants

4.10.  digest=poseidon_prf_gadget((comm_r_new,digest_index))

5.10.  digest_bits:F2[255]=le_bits_gadget(digest)# 255=log2(q) is the bit-length of Fq

  # Chunk digest_bits by challenge (chunks of size RandChallengeBits)

6.10.  for j[ChallengesPerPRF]\boldsymbol:

7.10.  challenge_bits:F2[RandChallengeBits]=digest_bits[jRandChallengeBits..(j+1)RandChallengeBits]

8.10.  rand_challenge_bits.push(challenge_bits)

#  Truncate the return value because the last PRF adds more challenges than necessary

9.10.  return rand_challenge_bits[..C]

Get Challenge High Bits

Returns the

h high bits of
challenge_bits
, allocated as a single field element, where
h
is chosen from
Hs
via
h_select_bits
.

Gadget: get_high_bits_gadget(challenge_bits:F2[NodeBits],h_select_bits:F2[len(Hs)])Fq
1.10.  scaled_highs:Fq[len(Hs)]=( )

2.10.  for (h,h_select_bit)zip(Hs,h_select_bits)\boldsymbol:

  # Pack the h high bits of challenge_bits into a single Fq

3.10.  high_bits=challenge_bits[NodeBitsh..]

4.10.  high=lc_gadget(i[h]2ihigh_bits[i])# Note: 2i is an unallocated constant

  # Scale by 0 or 1

5.10.  high_or_zero=mul_gadget(high,h_select_bit)

6.10.  scaled_highs.push(high_or_zero)

#  The sum of the scaled values is the selected high value

7.10.  selected_high=sum_gadget(scaled_highs)

8.10.  return selected_high