Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Question Regarding rootC Selection in Proof Aggregation #71

Open
kiwi202202 opened this issue Jul 31, 2024 · 0 comments
Open

Question Regarding rootC Selection in Proof Aggregation #71

kiwi202202 opened this issue Jul 31, 2024 · 0 comments

Comments

@kiwi202202
Copy link

After running buildsetup in zkevm-proverjs, I noticed the following code segment in the build/proof/recursive2.circom file:

    component vA = StarkVerifier(); // include "recursive1.verifier.circom";
    ...
    component isOneBatchA = IsZero();
    isOneBatchA.in  <== a_publics[43] - a_publics[16] - 1;
    component a_muxRootC = MultiMux1(4);
    a_muxRootC.c[0] <== rootC;
    a_muxRootC.c[1] <== rootCSingle;
    a_muxRootC.s <== isOneBatchA.out;

    for (var i=0; i<4; i++) {
        vA.publics[44+i] <== rootC[i];
    }
    vA.rootC <== a_muxRootC.out;

In this code, a choice is made between a hard-coded rootCSingle and an input rootC based on whether it is verifying a recursive1 proof or a recursive2 proof. My concern is whether there could be any issues when using rootC. Specifically, if the rootC circuit does not correctly execute the STARK verification process for two recursive1/recursive2 proofs (maybe less constraints, despite having the same shape as a normal recursive2 circuit), it could lead to potential vulnerabilities.

The above-mentioned StarkVerifier uses the code from build/proof/recursive1.circom, as shown below:

template StarkVerifier() {
    signal input publics[48]; // constant polynomials
    signal input root1[4]; // Merkle tree root of the evaluations of all trace polynomials
    signal input root2[4]; // Merkle tree root of the evaluations of polynomials h1 and h2 used for the plookup
    signal input root3[4]; // Merkle tree root of the evaluations of the grand product polynomials (Z) 
    signal input root4[4]; // Merkle tree root of the evaluations of the quotient Q1 and Q2 polynomials

    // Notice that root2 and root3 can be zero depending on the STARK being verified 


    signal input rootC[4]; // Merkle tree root of the evaluations of constant polynomials

Compared to the build/proof/recursive1.circom which uses the dynamic StarkVerifier template, the rootC is hard-coded in the build/proof/c12a.verifier.circom file to ensure verification of a "correctly executed c12a process" circuit:

template StarkVerifier() {
    signal input publics[44]; // constant polynomials
    signal input root1[4]; // Merkle tree root of the evaluations of all trace polynomials
    signal input root2[4]; // Merkle tree root of the evaluations of polynomials h1 and h2 used for the plookup
    signal input root3[4]; // Merkle tree root of the evaluations of the grand product polynomials (Z) 
    signal input root4[4]; // Merkle tree root of the evaluations of the quotient Q1 and Q2 polynomials

    // Notice that root2 and root3 can be zero depending on the STARK being verified 

    signal rootC[4] <== [18013726111668493315,7128019730232301670,1786599658476827655,13745530316764869768 ]; // Merkle tree root of the evaluations of constant polynomials

I would like to understand whether the dynamic input rootC in recursive2.circom might introduce any issues, and if there are any approaches to ensure the security and correctness of this proof aggregation.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant