Filecoin - PoREP Circuit Introduction

The logic related to the PoREP circuit is in the storage-proofs/src/porep/stacked/circuit/ directory. Rust-fil-proofs code is updated relatively quickly. The last commit information of the code used in this article is as follows:

 commit 14870d715f1f6019aba3f72772659e38184378bf
Author: Rod Vagg
Date: Fri Mar 20 22:30:18 2020 +1100
    feat(filecoin-proofs): expose filecoin_proofs::pad_reader

As long as the SDR algorithm remains unchanged, the general circuit logic will not change much. For those who are not familiar with the SDR algorithm, you can take a look at:

Filecoin - Why is SDR so slow?

The code framework of the entire PoREP circuit is shown in the figure below:

Let’s start with StackedCircuit.

StackedCircuit is the overall circuit of PoREP. StackedCircuit is defined in storage-proofs/src/porep/stacked/circuit/proof.rs.

 pub struct StackedCircuit<'a, e:="" h:="" static="" g:="" hasher=""> {
params: &'a E::Params,
    public_params:<StackedDrg<'a, g="">as ProofScheme<'a>>::PublicParams,
replica_id: Option
comm_d: Option
comm_r: Option
comm_r_last: Option
comm_c: Option
proofs: Vec<Proof
}

in

• params - JubjubEngine related parameters,

• public_params - StackedDrg (deep robust graph) related parameters, including the parameters of the graph itself and the number of challenges.

• replica_id - Sector replication id

• comm_d – the root of the binary tree of the original data

• comm_r - hash result of comm_r_last and comm_c

• comm_r_last - the root of the octree of the encoded data

• comm_c - the root of the octree of column hash results

• proofs - proof circuit corresponding to the challenge

The construction of the entire circuit starts with the synthesize interface function of StackedCircuit.

 impl<'a, h:="" g:="" hasher=""> Circuit
    fn synthesize<CS: ConstraintSystem

The entire synthesize function divides the circuit into two parts: 1/ tree root verification circuit 2/ challenge node information proof circuit. The tree root verification circuit is relatively simple and easy to understand. Apply for replica_id_bits, comm_d, comm_r, comm_r_last and comm_c variables, and verify whether comm_c and comm_r_last can correctly calculate comm_r.

When the sector size is 32G, the number of challenges is 144. In other words, the entire challenge node proof circuit consists of 144 small circuits.

 for (i, proof) in proofs.into_iter().enumerate() {
proof.synthesize(
                &mut cs.namespace(|| format!("challenge_{}", i)),
&self.params,
                public_params.layer_challenges.layers(),
&comm_d_num,
&comm_c_num,
                &comm_r_last_num,
                &replica_id_bits,
)?;
}

A small circuit for each challenge node, represented by a Proof structure (storage-proofs/src/porep/stacked/circuit/params.rs).

 pub struct Proof
    pub comm_d_proof: InclusionPath
    pub comm_r_last_proof: InclusionPath
    pub replica_column_proof: ReplicaColumnProof
    pub labeling_proofs: Vec<(usize,>,
    pub encoding_proof: EncodingProof,
}

The structure of Proof is relatively clear, including:

• comm_d_proof - Merkle tree proof of the original data

• encoding_proof - Encoding result proof

• comm_r_last_proof - Merkle tree proof of encoding result

• labeling_proofs - Labeling computational proofs

• replica_column_proof - proof of calculation of column hash

Proof's synthesize function constructs the proof above.

The Merkle tree proof circuit of the original data proves that the node of comm_d_leaf is on the Merkle tree with comm_d as the root.

 let comm_d_leaf = comm_d_proof.alloc_value(cs.namespace(|| "comm_d_leaf"))?;
comm_d_proof.synthesize(
    cs.namespace(|| "comm_d_inclusion"),
params,
comm_d.clone(),
comm_d_leaf.clone(),
)?;

Where comm_d_leaf is a variable in the circuit. comm_d_proof is the InclusionPath structure, defined in storage-proofs/src/porep/stacked/circuit/params.rs. The core logic of the InclusionPath circuit is in the synthesize function:

 pub fn synthesize<CS: ConstraintSystem
self,
cs: CS,
params: &
root: num::AllocatedNum
leaf: num::AllocatedNum
) -> Result<(), synthesiserror=""> {
    let InclusionPath { auth_path, .. } = self;
    let root = Root::from_allocated::
    let value = Root::from_allocated::
PoRCircuit::
}

It can be found that all the circuits for proof retrieval are implemented through PoRCircuit. In other words, the current PoR is implemented through the Merkle tree. The PoRCircuit circuit is defined in storage-proofs/src/gadgets/por.rs. The PoRCircuit circuit combines the leaf node and path information to check whether the final "calculated" root is consistent with the provided root. You can check the specific related logic by yourself.

The proof circuit of Labeling calculation is to prove that a certain node is calculated correctly according to the SDR algorithm.

 for (layer, proof) in labeling_proofs.into_iter() {
    let raw = replica_column_proof.c_x.get_node_at_layer(layer);
let labeled_node =
         num::AllocatedNum::alloc(cs.namespace(|| format!("label_node_{}", layer)), || {
                    raw.map(Into::into)
                        .ok_or_else(|| SynthesisError::AssignmentMissing)
})?;
proof.synthesize(
         cs.namespace(|| format!("labeling_proof_{}", layer)),
params,
replica_id,
&labeled_node,
)?;
}

The result data of Labeling of a node on a certain layer can be obtained through replica_column_proof.c_x.get_node_at_layer(layer). The calculation circuit of Labeling is implemented by the synthesize function of the LabelingProof structure:

 pub fn synthesize<CS: ConstraintSystem
self,
mut cs: CS,
params: &
        replica_id: &[Boolean],
        exp_encoded_node: &num::AllocatedNum
    ) -> Result<(), synthesiserror=""> {
        let LabelingProof { node, parents } = self;
        let key = Self::create_label(
            cs.namespace(|| "create_label"),
params,
replica_id,
node,
parents,
)?;
// enforce equality
        constraint::equal(&mut cs, || "equality_key", &exp_encoded_node, &key);
Ok(())
}
}

The create_label function is composed of two circuits: create_label_circuit and sha256_circuit. In other words, these two circuits perform sha256 calculations on the dependent (parents) node data. constraint::equal is used to confirm whether the "calculated" node data is consistent with the provided node data.

The encoding calculation is to encode the node data of the last layer and the original data. The encoding calculation method is large number addition. The specific calculation is in the storage-proofs/src/gadgets/encode.rs file.

 encoding_proof.synthesize(
            cs.namespace(|| format!("encoding_proof_{}", layers)),
params,
replica_id,
            &comm_r_last_data_leaf,
&comm_d_leaf,
)?;

The entire Encoding proof circuit is implemented by the synthesize function of EncodingProof. Simply put, the Encoding circuit verification process first calculates Labeling, then performs Encoding calculation on comm_d_leaf, and determines whether the result is consistent with comm_r_last_data_leaf.

Similar to the Merkle tree proof circuit proof of the original data, it proves that comm_r_last_data_leaf is on the Merkle tree of comm_r_last. The only difference is that this tree is an octree.

 comm_r_last_proof.synthesize(
     cs.namespace(|| "comm_r_last_data_inclusion"),
params,
comm_r_last.clone(),
comm_r_last_data_leaf,
)?;

The proof circuit of Column hash is implemented by synthesize of ReplicaColumnProof structure, which is specifically defined in storage-proofs/src/porep/stacked/circuit/params.rs.

 replica_column_proof.synthesize(cs.namespace(|| "replica_column_proof"), params, comm_c)?;

The general logic is to process the Column information of the challenge node first, and then process the Column information of the base and exp dependent nodes respectively:

 // c_x
c_x.synthesize(cs.namespace(|| "c_x"), params, comm_c)?;
// drg parents
for (i, parent) in drg_parents.into_iter().enumerate() {
     parent.synthesize(cs.namespace(|| format!("drg_parent_{}", i)), params, comm_c)?;
}
// exp parents
for (i, parent) in exp_parents.into_iter().enumerate() {
     parent.synthesize(cs.namespace(|| format!("exp_parent_{}", i)), params, comm_c)?;
}

That is, the proof circuit consists of 15 ColumnProof subcircuits. ColumnProof is defined in storage-proofs/src/porep/stacked/circuit/column_proof.rs.

 pub struct ColumnProof
column: Column,
    inclusion_path: InclusionPath
}

The corresponding circuit generation logic is in the synthesize function of ColumnProof:

 let c_i = column.hash(cs.namespace(|| "column_hash"), params)?;
let leaf_num = inclusion_path.alloc_value(cs.namespace(|| "leaf"))?;
constraint::equal(&mut cs, || "enforce column_hash = leaf", &c_i, &leaf_num);
// TODO: currently allocating the leaf twice, inclusion path should take the already allocated leaf.
inclusion_path.synthesize(
    cs.namespace(|| "column_proof_all_inclusion"),
params,
comm_c.clone(),
leaf_num,
)?;

Column.hash calculates the hash result corresponding to Column. Check whether this result is equal to leaf_num. Also check whether this leaf_num is on the Merkle tree of comm_c.

So far, the full picture of the entire circuit has emerged:

The public input of the entire PoREP circuit is implemented by StackedCompound's generate_public_inputs function, which is specifically implemented in the storage-proofs/src/porep/stacked/circuit/proof.rs file.

 fn generate_public_inputs(
pub_in: &<StackedDrg
pub_params: &<StackedDrg
k: Option
) -> Result<Vec

Where k is the parition number. For a 32G sector, there are 9 paritions in total.

comm_d & comm_r

 let comm_d = pub_in.tau.as_ref().expect("missing tau").comm_d;
let comm_r = pub_in.tau.as_ref().expect("missing tau").comm_r;

Challenge the existence proof of comm_d

Currently, PoRCompound only uses the path information of the Merkle tree as public input.

 inputs.extend(PoRCompound::
&pub_inputs,
&por_params,
k,
)?);

Challenge the existence proof of a series of comm_c

Note that the computation of comm_d is a binary tree and the computation of comm_c is an octree.

 // c_x
inputs.extend(generate_inclusion_inputs(challenge)?);
// drg parents
let mut drg_parents = vec![0; graph.base_graph().degree()];
graph.base_graph().parents(challenge, &mut drg_parents)?;
for parent in drg_parents.into_iter() {
    inputs.extend(generate_inclusion_inputs(parent as usize)?);
}
// exp parents
let mut exp_parents = vec![0; graph.expansion_degree()];
graph.expanded_parents(challenge, &mut exp_parents);
for parent in exp_parents.into_iter() {
    inputs.extend(generate_inclusion_inputs(parent as usize)?);
}

Challenge the existence proof of comm_r_last

 inputs.extend(generate_inclusion_inputs(challenge)?);

Summarize:

PoREP's circuit verifies the calculation process of Sector, from Labeling, Encoding to Column Hash. Note that when the Sector size is 32G, the circuit includes the calculation of 144 challenge nodes. In addition to comm_d and comm_r, the corresponding public input of the circuit also includes the path information of each Merkle tree.