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

bug: baby-snark and_gate test fails #957

Closed
erhant opened this issue Jan 11, 2025 · 2 comments
Closed

bug: baby-snark and_gate test fails #957

erhant opened this issue Jan 11, 2025 · 2 comments

Comments

@erhant
Copy link
Contributor

erhant commented Jan 11, 2025

Hi, the and_gate test at https://github.com/lambdaclass/lambdaworks/blob/main/examples/baby-snark/tests/integration_tests.rs#L35 uses a witness [1, 1, 1] with public [1] which passes, but if we have [0, 0, 0] with public [0] it fails.

Full code:

#[test]
fn and_gate() {
    let u = vec![
        i64_vec_to_field(&[-1, 2, 0, 0]),
        i64_vec_to_field(&[-1, 0, 2, 0]),
        i64_vec_to_field(&[-1, 0, 0, 2]),
        i64_vec_to_field(&[-1, 2, 2, -4]),
    ];

    let witness = i64_vec_to_field(&[0, 0, 0]);
    let public = i64_vec_to_field(&[0]);

    test_integration(u, witness, public)
}
@nicole-graus
Copy link
Contributor

Hi! Thanks for your comment. In the code you are showing, the variable public cannot be 0, it must be 1, because it is the first element of the input that the prover receives. In the Baby Snark paper you can find a detailed explanation (in section 3).

Here we leave a short explanation:

In the code you show, the first row of the matrix $U$ ensures that the first input of the And Gate is a boolean. If we call $a = (1, x_1, x_2, y)$, then the matrix equation $Ua \circ Ua = 1$ implies that $(-1 \cdot 1 + 2 \cdot x_1 + 0 \cdot x_2 + 0 \cdot y)^2 = 1$ (looking only at the first row of the resulting matrix). Now this last equation works as a constraint for $x_1$ to be a boolean only if the first element of $w$ is 1. Because if so, we have:
$(-1 + 2 \cdot x_1 )^2 = 1$.
Then, $2 \cdot x_1 - 1 = 1 \text{ or } -1$.
So, $x_1 = 1 \text{ or } 0$. That is $x_1$, the first input of the And, is a boolean.
If the variable public were 0 as you propose, then the first row equation would be $(2 \cdot x_1)^2 = 1$
which doesn't imply that $x_1$ is $1$ or $0$.

Anyway, we did a small PR adding a check in the prover and documentation explaining this so there is no confusion.

Feel free to ask if something wasn't clear enough!

@erhant
Copy link
Contributor Author

erhant commented Jan 14, 2025

Ah my bad, I thought witness itself included the public part for some reason (coming from Circom world) so I guessed it had to be a, b, c 😅

Anyway, we did a small #960 adding a check in the prover and documentation explaining this so there is no confusion.

Good idea!

Thanks for the explanation, closing this issue.

@erhant erhant closed this as completed Jan 14, 2025
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

2 participants