Add RecursiveCircuit

[arnaucube]

The RecursiveCircuit verifies N proofs of itself (N=arity), together with the logic defined at the InnerCircuit (in our case, used for the MainPodCircuit logic).

The arity defines the maximum amount of proofs of itself that the RecursiveCircuit verifies. When arity>1, using the RecursiveCircuit has the shape of a tree of the same arity.

                     π_root
                       ▲
               ┌───────┴────────┐
               │RecursiveCircuit│
               └─▲───▲───▲────▲─┘
         ┌───────┘  ┌┘   └┐   └──────┐
         │π''_1     │ ... │     π''_N│
┌────────┴───────┐ ┌┴┐┌─┐┌┴┐ ┌───────┴────────┐
│RecursiveCircuit│ │.││.││.│ │RecursiveCircuit│
└──▲─────────▲───┘ └─┘└─┘└─┘ └──▲─────────▲───┘
   │         │                  │         │
  π_1  ...  π_N               π'_1 ...  π'_N

where
N: arity of the RecursiveCircuit
π_i: plonky2 proof of the RecursiveCircuit

In the direction of #174 .

[arnaucube]

(rebased to latest main branch changes & improved tests)

[ed255]

I've done an initial review. I haven't reviewed the tests properly yet.

[ed255]

These public inputs are built like this:
[inner_circuit_public, circuit_digest, constants_sigmas_cap].
We should do two things here:

1. If the selectors_targ=true, then circuit_digest, constants_sigmas_cap from the proof should be equal to the values in verifier_data_targ. Or maybe we skip the conditional part and just connect, beacuse the dummy proof may use the same verifier data?
2. Extract the inner_circuit_public and that's collected and passed to I::build

[ed255]

1. If the `selectors_targ=true`, then `circuit_digest, constants_sigmas_cap` from the proof should be equal to the values in `verifier_data_targ`.  Or maybe we skip the conditional part and just connect, beacuse the dummy proof may use the same verifier data?

I learned that this is already being done through the combination of

builder.add_verifier_data_public_inputs()

and

builder.conditionally_verify_cyclic_proof_or_dummy()

https://github.com/0xPolygonZero/plonky2/blob/6a2c1b47b7b00864c2b65a44c18099b0152f550e/plonky2/src/recursion/cyclic_recursion.rs#L114-L117

[ed255]

I think we need a new method to return the public inputs so that we can pass them from InnerCircuit to RecursiveCircuit.
For example something like this:

pub trait InnerCircuit: Clone {
    type InputTarget: Flattenable;

    fn public_inputs(&self) -> Self::InputTarget;

[arnaucube]

yes, I've opened the issue #208 to tackle this

[ed255]

I think we should add a verify function, because the verification of this proof is not just calling the plonky2 method, but we also need to check that the expected verifier_data is in the public inputs.

[arnaucube]

Agree, but probably this verify function will include also the logic to check the validity of the verifier_data, right? I would propose to map it into a separate issue for the entire task (which includes implementing one of the approaches that you described in the hackmd of the 'recursion family framework').

[ed255]

The verifier_data must be equal to the one calculated via:

let circuit_data = RecursiveCircuit::<I>::circuit_data(&params, &inner_params)?;
let verifier_data = circuit_data.verifier_data();

That's the case if we consider a circuit that verifies itself. If the verifier data in the public inputs is not the verifier data of the outer circuit then it's not a circuit that verifies itself.