Filecoin — PoREP circuit introduction
The logic related to PoREP circuits is in the storage-proofs / src / porep / stacked / circuit / directory. The 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 <rod@vagg.org>
Date: Fri Mar 20 22:30:18 2020 +1100feat(filecoin-proofs): expose filecoin_proofs::pad_reader
As long as the SDR algorithm remains unchanged, the general circuit logic will not change significantly. The code framework of the entire PoREP circuit is shown below:
Speaking from StackedCircuit.
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: JubjubEngine, H: 'static + Hasher, G: 'static + Hasher> {
params: &'a E::Params,
public_params: <StackedDrg<'a, H, G> as ProofScheme<'a>>::PublicParams,
replica_id: Option<H::Domain>,
comm_d: Option<G::Domain>,
comm_r: Option<H::Domain>,
comm_r_last: Option<H::Domain>,
comm_c: Option<H::Domain>,proofs: Vec<Proof<H, G>>,
}
among them
- 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 copy 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 data after encoding
- comm_c-Root of the octree of column hash result
- proofs-Challenge the corresponding proof circuit
The construction of the entire circuit begins with the StackedCircuit’s synthesize interface function.
impl<'a, H: Hasher, G: Hasher> Circuit<Bls12> for StackedCircuit<'a, Bls12, H, G> {
fn synthesize<CS: ConstraintSystem<Bls12>>(self, cs: &mut CS) -> Result<(), SynthesisError> {The whole synthesize function divides the circuit into two parts: 1 / tree root check circuit 2 / challenged node information proof circuit. The root check 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 that comm_c and comm_r_last can correctly calculate comm_r.
Challenge node proof circuit
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,
)?;
}The small circuit of each challenge node is represented by the Proof structure (storage-proofs / src / porep / stacked / circuit / params.rs).
pub struct Proof<H: Hasher, G: Hasher> {
pub comm_d_proof: InclusionPath<Bls12, G, typenum::U2>,
pub comm_r_last_proof: InclusionPath<Bls12, H, typenum::U8>,
pub replica_column_proof: ReplicaColumnProof<H>,
pub labeling_proofs: Vec<(usize, LabelingProof)>,
pub encoding_proof: EncodingProof,
}Proof structure is relatively clear, including:
- comm_d_proof-Merkle tree proof of original data
- encoding_proof-Encoding result proof
- comm_r_last_proof-Merkle tree proof of Encoding result
- labeling_proofs-Labeling calculation proof
- replica_column_proof-column hash calculation proof
Proof’s synthesize function constructs the proof above.
Merkle tree proof circuit for raw data
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 an 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<Bls12>>(
self,
cs: CS,
params: &<Bls12 as JubjubEngine>::Params,
root: num::AllocatedNum<Bls12>,
leaf: num::AllocatedNum<Bls12>,
) -> Result<(), SynthesisError> {
let InclusionPath { auth_path, .. } = self;let root = Root::from_allocated::<CS>(root);
let value = Root::from_allocated::<CS>(leaf);
PoRCircuit::<U, Bls12, H>::synthesize(cs, params, value, auth_path, root, true)
}
It can be found that all circuits that prove Retrieval are realized through PoRCircuit. In other words, the current PoR is realized through the Merkle tree. PoRCircuit circuit is defined in storage-proofs / src /gadgets / por.rs. PoRCircuit’s circuit is to combine leaf node and path information to see if the root that is “computed” at the end is consistent with the provided root.
Labeling Proof circuit
The proof circuit for 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,
)?;
}Labeling result data of a node on a certain layer can be obtained by replica_column_proof.c_x.get_node_at_layer (layer). The calculation circuit of Labeling is realized by the synthesize function of the LabelingProof structure:
pub fn synthesize<CS: ConstraintSystem<Bls12>>(
self,
mut cs: CS,
params: &<Bls12 as JubjubEngine>::Params,
replica_id: &[Boolean],
exp_encoded_node: &num::AllocatedNum<Bls12>,
) -> 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 are sha256 calculations of the node data of the parents. constraint :: equal is to confirm whether the “calculated” node data is consistent with the provided node data.
Encoding proof circuit
Encoding calculation is to encode the node data of the last layer and the original data. The calculation method of Encoding is the addition of large numbers. The specific calculation is in storage-proofs / src / gadgets / encode.rs.
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, Encoding’s circuit verification process first calculates Labeling, and then performs Encoding calculation on comm_d_leaf to determine whether the result is consistent with comm_r_last_data_leaf.
Merkle Tree Proof of Encoding Results
The Merkle tree proof circuit proof similar to the original data proves that comm_r_last_data_leaf is on the comm_r_last Merkle tree. It’s just 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,
)?;Column hash proof circuit
The proof circuit of the Column hash is realized by the Synthesize of the 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 that the Column information of the challenge node is processed first, and then the Column information of the base and exp dependent nodes are processed separately:
// 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)?;
}
In other words, the proof circuit consists of 15 ColumnProof subcircuits. ColumnProof is defined in storage-proofs / src / porep / stacked / circuit / column_proof.rs.
pub struct ColumnProof<H: Hasher> {
column: Column,
inclusion_path: InclusionPath<Bls12, H, typenum::U8>,
}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);
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 if this result is equal to leaf_num. Also check if this leaf_num is on the comm_c Merkle tree.
So far, the whole picture of the whole circuit has appeared:
Public input of the circuit
The public input of the entire PoREP circuit is implemented by StackedCompound’s generate_public_inputs function, which is specifically implemented in the file storage-proofs / src / porep / stacked / circuit / proof.rs.
fn generate_public_inputs(
pub_in: &<StackedDrg<H, G> as ProofScheme>::PublicInputs,
pub_params: &<StackedDrg<H, G> as ProofScheme>::PublicParams,
k: Option<usize>,
) -> Result<Vec<Fr>> {Where k is the number of the parition. For the 32G Sector, there are a total of 9 Paritition.
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 proof of existence corresponding to comm_d
At present, PoRCompound only uses the path information of the Merkle tree as public input.
inputs.extend(PoRCompound::<H, typenum::U2>::generate_public_inputs(
&pub_inputs,
&por_params,
k,
)?);Challenge a series of comm_c existence proofs
Note that the calculation of comm_d is a binary tree, and the calculation 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)?);
}
Proof of existence of comm_r_last corresponding to the challenge
inputs.extend(generate_inclusion_inputs(challenge)?);To sum up:
PoREP’s circuit validates the Sector’s calculation process, from Labeling, Encoding to Column Hash. Note that in the case where 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 has the path information of each Merkle tree.
