plonky2/recursion/
cyclic_recursion.rs

1#![allow(clippy::int_plus_one)] // Makes more sense for some inequalities below.
2
3#[cfg(not(feature = "std"))]
4use alloc::vec::Vec;
5
6use anyhow::{ensure, Result};
7
8use crate::field::extension::Extendable;
9use crate::hash::hash_types::{HashOut, HashOutTarget, MerkleCapTarget, RichField};
10use crate::hash::merkle_tree::MerkleCap;
11use crate::iop::target::{BoolTarget, Target};
12use crate::plonk::circuit_builder::CircuitBuilder;
13use crate::plonk::circuit_data::{
14    CommonCircuitData, VerifierCircuitTarget, VerifierOnlyCircuitData,
15};
16use crate::plonk::config::{AlgebraicHasher, GenericConfig};
17use crate::plonk::proof::{ProofWithPublicInputs, ProofWithPublicInputsTarget};
18use crate::util::serialization::{Buffer, IoResult, Read, Write};
19
20impl<C: GenericConfig<D>, const D: usize> VerifierOnlyCircuitData<C, D> {
21    fn from_slice(slice: &[C::F], common_data: &CommonCircuitData<C::F, D>) -> Result<Self>
22    where
23        C::Hasher: AlgebraicHasher<C::F>,
24    {
25        // The structure of the public inputs is `[..., circuit_digest, constants_sigmas_cap]`.
26        let cap_len = common_data.config.fri_config.num_cap_elements();
27        let len = slice.len();
28        ensure!(len >= 4 + 4 * cap_len, "Not enough public inputs");
29        let constants_sigmas_cap = MerkleCap(
30            (0..cap_len)
31                .map(|i| HashOut {
32                    elements: core::array::from_fn(|j| slice[len - 4 * (cap_len - i) + j]),
33                })
34                .collect(),
35        );
36        let circuit_digest =
37            HashOut::from_partial(&slice[len - 4 - 4 * cap_len..len - 4 * cap_len]);
38
39        Ok(Self {
40            circuit_digest,
41            constants_sigmas_cap,
42        })
43    }
44}
45
46impl VerifierCircuitTarget {
47    pub fn to_bytes(&self) -> IoResult<Vec<u8>> {
48        let mut buffer = Vec::new();
49        buffer.write_target_merkle_cap(&self.constants_sigmas_cap)?;
50        buffer.write_target_hash(&self.circuit_digest)?;
51        Ok(buffer)
52    }
53
54    pub fn from_bytes(bytes: Vec<u8>) -> IoResult<Self> {
55        let mut buffer = Buffer::new(&bytes);
56        let constants_sigmas_cap = buffer.read_target_merkle_cap()?;
57        let circuit_digest = buffer.read_target_hash()?;
58        Ok(Self {
59            constants_sigmas_cap,
60            circuit_digest,
61        })
62    }
63
64    fn from_slice<F: RichField + Extendable<D>, const D: usize>(
65        slice: &[Target],
66        common_data: &CommonCircuitData<F, D>,
67    ) -> Result<Self> {
68        let cap_len = common_data.config.fri_config.num_cap_elements();
69        let len = slice.len();
70        ensure!(len >= 4 + 4 * cap_len, "Not enough public inputs");
71        let constants_sigmas_cap = MerkleCapTarget(
72            (0..cap_len)
73                .map(|i| HashOutTarget {
74                    elements: core::array::from_fn(|j| slice[len - 4 * (cap_len - i) + j]),
75                })
76                .collect(),
77        );
78        let circuit_digest = HashOutTarget {
79            elements: core::array::from_fn(|i| slice[len - 4 - 4 * cap_len + i]),
80        };
81
82        Ok(Self {
83            circuit_digest,
84            constants_sigmas_cap,
85        })
86    }
87}
88
89impl<F: RichField + Extendable<D>, const D: usize> CircuitBuilder<F, D> {
90    /// If `condition` is true, recursively verify a proof for the same circuit as the one we're
91    /// currently building. Otherwise, verify `other_proof_with_pis`.
92    ///
93    /// For a typical IVC use case, `condition` will be false for the very first proof in a chain,
94    /// i.e. the base case.
95    ///
96    /// Note that this does not enforce that the inner circuit uses the correct verification key.
97    /// This is not possible to check in this recursive circuit, since we do not know the
98    /// verification key until after we build it. Verifiers must separately call
99    /// `check_cyclic_proof_verifier_data`, in addition to verifying a recursive proof, to check
100    /// that the verification key matches.
101    ///
102    /// WARNING: Do not register any public input after calling this! TODO: relax this
103    pub fn conditionally_verify_cyclic_proof<C: GenericConfig<D, F = F>>(
104        &mut self,
105        condition: BoolTarget,
106        cyclic_proof_with_pis: &ProofWithPublicInputsTarget<D>,
107        other_proof_with_pis: &ProofWithPublicInputsTarget<D>,
108        other_verifier_data: &VerifierCircuitTarget,
109        common_data: &CommonCircuitData<F, D>,
110    ) -> Result<()>
111    where
112        C::Hasher: AlgebraicHasher<F>,
113    {
114        let verifier_data = self
115            .verifier_data_public_input
116            .clone()
117            .expect("Must call add_verifier_data_public_inputs before cyclic recursion");
118
119        if let Some(existing_common_data) = self.goal_common_data.as_ref() {
120            assert_eq!(existing_common_data, common_data);
121        } else {
122            self.goal_common_data = Some(common_data.clone());
123        }
124
125        let inner_cyclic_pis = VerifierCircuitTarget::from_slice::<F, D>(
126            &cyclic_proof_with_pis.public_inputs,
127            common_data,
128        )?;
129        // Connect previous verifier data to current one. This guarantees that every proof in the cycle uses the same verifier data.
130        self.connect_hashes(
131            inner_cyclic_pis.circuit_digest,
132            verifier_data.circuit_digest,
133        );
134        self.connect_merkle_caps(
135            &inner_cyclic_pis.constants_sigmas_cap,
136            &verifier_data.constants_sigmas_cap,
137        );
138
139        // Verify the cyclic proof if `condition` is set to true, otherwise verify the other proof.
140        self.conditionally_verify_proof::<C>(
141            condition,
142            cyclic_proof_with_pis,
143            &verifier_data,
144            other_proof_with_pis,
145            other_verifier_data,
146            common_data,
147        );
148
149        // Make sure we have every gate to match `common_data`.
150        for g in &common_data.gates {
151            self.add_gate_to_gate_set(g.clone());
152        }
153
154        Ok(())
155    }
156
157    pub fn conditionally_verify_cyclic_proof_or_dummy<C: GenericConfig<D, F = F> + 'static>(
158        &mut self,
159        condition: BoolTarget,
160        cyclic_proof_with_pis: &ProofWithPublicInputsTarget<D>,
161        common_data: &CommonCircuitData<F, D>,
162    ) -> Result<()>
163    where
164        C::Hasher: AlgebraicHasher<F>,
165    {
166        let (dummy_proof_with_pis_target, dummy_verifier_data_target) =
167            self.dummy_proof_and_vk::<C>(common_data)?;
168        self.conditionally_verify_cyclic_proof::<C>(
169            condition,
170            cyclic_proof_with_pis,
171            &dummy_proof_with_pis_target,
172            &dummy_verifier_data_target,
173            common_data,
174        )?;
175        Ok(())
176    }
177}
178
179/// Additional checks to be performed on a cyclic recursive proof in addition to verifying the proof.
180/// Checks that the purported verifier data in the public inputs match the real verifier data.
181pub fn check_cyclic_proof_verifier_data<
182    F: RichField + Extendable<D>,
183    C: GenericConfig<D, F = F>,
184    const D: usize,
185>(
186    proof: &ProofWithPublicInputs<F, C, D>,
187    verifier_data: &VerifierOnlyCircuitData<C, D>,
188    common_data: &CommonCircuitData<F, D>,
189) -> Result<()>
190where
191    C::Hasher: AlgebraicHasher<F>,
192{
193    let pis = VerifierOnlyCircuitData::<C, D>::from_slice(&proof.public_inputs, common_data)?;
194    ensure!(verifier_data.constants_sigmas_cap == pis.constants_sigmas_cap);
195    ensure!(verifier_data.circuit_digest == pis.circuit_digest);
196
197    Ok(())
198}
199
200#[cfg(test)]
201mod tests {
202    #[cfg(not(feature = "std"))]
203    use alloc::vec;
204
205    use anyhow::Result;
206
207    use crate::field::extension::Extendable;
208    use crate::field::types::{Field, PrimeField64};
209    use crate::gates::noop::NoopGate;
210    use crate::hash::hash_types::{HashOutTarget, RichField};
211    use crate::hash::hashing::hash_n_to_hash_no_pad;
212    use crate::hash::poseidon::{PoseidonHash, PoseidonPermutation};
213    use crate::iop::witness::{PartialWitness, WitnessWrite};
214    use crate::plonk::circuit_builder::CircuitBuilder;
215    use crate::plonk::circuit_data::{CircuitConfig, CommonCircuitData};
216    use crate::plonk::config::{AlgebraicHasher, GenericConfig, PoseidonGoldilocksConfig};
217    use crate::recursion::cyclic_recursion::check_cyclic_proof_verifier_data;
218    use crate::recursion::dummy_circuit::cyclic_base_proof;
219
220    // Generates `CommonCircuitData` usable for recursion.
221    fn common_data_for_recursion<
222        F: RichField + Extendable<D>,
223        C: GenericConfig<D, F = F>,
224        const D: usize,
225    >() -> CommonCircuitData<F, D>
226    where
227        C::Hasher: AlgebraicHasher<F>,
228    {
229        let config = CircuitConfig::standard_recursion_config();
230        let builder = CircuitBuilder::<F, D>::new(config);
231        let data = builder.build::<C>();
232        let config = CircuitConfig::standard_recursion_config();
233        let mut builder = CircuitBuilder::<F, D>::new(config);
234        let proof = builder.add_virtual_proof_with_pis(&data.common);
235        let verifier_data =
236            builder.add_virtual_verifier_data(data.common.config.fri_config.cap_height);
237        builder.verify_proof::<C>(&proof, &verifier_data, &data.common);
238        let data = builder.build::<C>();
239
240        let config = CircuitConfig::standard_recursion_config();
241        let mut builder = CircuitBuilder::<F, D>::new(config);
242        let proof = builder.add_virtual_proof_with_pis(&data.common);
243        let verifier_data =
244            builder.add_virtual_verifier_data(data.common.config.fri_config.cap_height);
245        builder.verify_proof::<C>(&proof, &verifier_data, &data.common);
246        while builder.num_gates() < 1 << 12 {
247            builder.add_gate(NoopGate, vec![]);
248        }
249        builder.build::<C>().common
250    }
251
252    /// Uses cyclic recursion to build a hash chain.
253    /// The circuit has the following public input structure:
254    /// - Initial hash (4)
255    /// - Output for the tip of the hash chain (4)
256    /// - Chain length, i.e. the number of times the hash has been applied (1)
257    /// - VK for cyclic recursion (?)
258    #[test]
259    fn test_cyclic_recursion() -> Result<()> {
260        const D: usize = 2;
261        type C = PoseidonGoldilocksConfig;
262        type F = <C as GenericConfig<D>>::F;
263
264        let config = CircuitConfig::standard_recursion_config();
265        let mut builder = CircuitBuilder::<F, D>::new(config);
266        let one = builder.one();
267
268        // Circuit that computes a repeated hash.
269        let initial_hash_target = builder.add_virtual_hash();
270        builder.register_public_inputs(&initial_hash_target.elements);
271        let current_hash_in = builder.add_virtual_hash();
272        let current_hash_out =
273            builder.hash_n_to_hash_no_pad::<PoseidonHash>(current_hash_in.elements.to_vec());
274        builder.register_public_inputs(&current_hash_out.elements);
275        let counter = builder.add_virtual_public_input();
276
277        let mut common_data = common_data_for_recursion::<F, C, D>();
278        let verifier_data_target = builder.add_verifier_data_public_inputs();
279        common_data.num_public_inputs = builder.num_public_inputs();
280
281        let condition = builder.add_virtual_bool_target_safe();
282
283        // Unpack inner proof's public inputs.
284        let inner_cyclic_proof_with_pis = builder.add_virtual_proof_with_pis(&common_data);
285        let inner_cyclic_pis = &inner_cyclic_proof_with_pis.public_inputs;
286        let inner_cyclic_initial_hash = HashOutTarget::try_from(&inner_cyclic_pis[0..4]).unwrap();
287        let inner_cyclic_latest_hash = HashOutTarget::try_from(&inner_cyclic_pis[4..8]).unwrap();
288        let inner_cyclic_counter = inner_cyclic_pis[8];
289
290        // Connect our initial hash to that of our inner proof. (If there is no inner proof, the
291        // initial hash will be unconstrained, which is intentional.)
292        builder.connect_hashes(initial_hash_target, inner_cyclic_initial_hash);
293
294        // The input hash is the previous hash output if we have an inner proof, or the initial hash
295        // if this is the base case.
296        let actual_hash_in =
297            builder.select_hash(condition, inner_cyclic_latest_hash, initial_hash_target);
298        builder.connect_hashes(current_hash_in, actual_hash_in);
299
300        // Our chain length will be inner_counter + 1 if we have an inner proof, or 1 if not.
301        let new_counter = builder.mul_add(condition.target, inner_cyclic_counter, one);
302        builder.connect(counter, new_counter);
303
304        builder.conditionally_verify_cyclic_proof_or_dummy::<C>(
305            condition,
306            &inner_cyclic_proof_with_pis,
307            &common_data,
308        )?;
309
310        let cyclic_circuit_data = builder.build::<C>();
311
312        let mut pw = PartialWitness::new();
313        let initial_hash = [F::ZERO, F::ONE, F::TWO, F::from_canonical_usize(3)];
314        let initial_hash_pis = initial_hash.into_iter().enumerate().collect();
315        pw.set_bool_target(condition, false)?;
316        pw.set_proof_with_pis_target::<C, D>(
317            &inner_cyclic_proof_with_pis,
318            &cyclic_base_proof(
319                &common_data,
320                &cyclic_circuit_data.verifier_only,
321                initial_hash_pis,
322            ),
323        )?;
324        pw.set_verifier_data_target(&verifier_data_target, &cyclic_circuit_data.verifier_only)?;
325        let proof = cyclic_circuit_data.prove(pw)?;
326        check_cyclic_proof_verifier_data(
327            &proof,
328            &cyclic_circuit_data.verifier_only,
329            &cyclic_circuit_data.common,
330        )?;
331        cyclic_circuit_data.verify(proof.clone())?;
332
333        // 1st recursive layer.
334        let mut pw = PartialWitness::new();
335        pw.set_bool_target(condition, true)?;
336        pw.set_proof_with_pis_target(&inner_cyclic_proof_with_pis, &proof)?;
337        pw.set_verifier_data_target(&verifier_data_target, &cyclic_circuit_data.verifier_only)?;
338        let proof = cyclic_circuit_data.prove(pw)?;
339        check_cyclic_proof_verifier_data(
340            &proof,
341            &cyclic_circuit_data.verifier_only,
342            &cyclic_circuit_data.common,
343        )?;
344        cyclic_circuit_data.verify(proof.clone())?;
345
346        // 2nd recursive layer.
347        let mut pw = PartialWitness::new();
348        pw.set_bool_target(condition, true)?;
349        pw.set_proof_with_pis_target(&inner_cyclic_proof_with_pis, &proof)?;
350        pw.set_verifier_data_target(&verifier_data_target, &cyclic_circuit_data.verifier_only)?;
351        let proof = cyclic_circuit_data.prove(pw)?;
352        check_cyclic_proof_verifier_data(
353            &proof,
354            &cyclic_circuit_data.verifier_only,
355            &cyclic_circuit_data.common,
356        )?;
357
358        // Verify that the proof correctly computes a repeated hash.
359        let initial_hash = &proof.public_inputs[..4];
360        let hash = &proof.public_inputs[4..8];
361        let counter = proof.public_inputs[8];
362        let expected_hash: [F; 4] = iterate_poseidon(
363            initial_hash.try_into().unwrap(),
364            counter.to_canonical_u64() as usize,
365        );
366        assert_eq!(hash, expected_hash);
367
368        cyclic_circuit_data.verify(proof)
369    }
370
371    fn iterate_poseidon<F: RichField>(initial_state: [F; 4], n: usize) -> [F; 4] {
372        let mut current = initial_state;
373        for _ in 0..n {
374            current = hash_n_to_hash_no_pad::<F, PoseidonPermutation<F>>(&current).elements;
375        }
376        current
377    }
378}
plonky2/recursion/cyclic_recursion.rs

plonky2/recursion/
cyclic_recursion.rs
