zksecurity / noname

Noname: a programming language to write zkapps
https://zksecurity.github.io/noname/
178 stars 44 forks source link

create a test to see if the verifier can insert anything in public output part of the public input and the proof still works #58

Open mimoo opened 4 months ago

mimoo commented 4 months ago

I suspect that we don't assert that the public output (part of the public input) is the same as the values returned by the main function.

Let's create a test to see if the verifier can insert anything in public output part of the public input and the proof still works

actually, not even proof, we should be able to test if a witness is correct without producing a proof. For kimchi we can use this: https://github.com/o1-labs/proof-systems/blob/master/kimchi/src/circuits/constraints.rs#L290

we should find a similar function for R1CS

katat commented 4 months ago

It is fine for kimchi.

In noname, it add a "half-constraint" when a new output is added.

https://github.com/zksecurity/noname/blob/b93d60453836523569cca7354541b0c449f0108c/src/backends/kimchi/mod.rs#L698-L703

Then this constraint will be cancelled by - public during verifying witness.

https://github.com/o1-labs/proof-systems/blob/b443013b9f6a2aa5e396b5d274b9899626fb850b/kimchi/src/circuits/polynomials/generic.rs#L300-L304

So if the verifier doesn't provide a correct public output value, that constraint won't be cancelled.

mimoo commented 4 months ago

ohh right! We use the permutation in kimchi to wire these (since we copy the returned var up there in that part of the public input, they will be wired automatically)

for R1CS it won't work though, so it'd be good to have a test there also that shows that fails until we fix it :D

mimoo commented 4 months ago

on double take, the check done by the verify function here is not enough, as it will always work (the public input cancels the public input). To make sure the permutation is the one that's doing the checking, we have to actually create a proof/verify

(or have a better witness verify function, which we don't have at the moment ^^ but maybe it might be a good idea as well, but in the respect of time we should probably just create a proof and verify)

mimoo commented 4 months ago

associated, this command indeed doesn't show any constraints OR wiring for the public output!

cargo run -- test --path examples/public_output.no --private-inputs '{"private_input": "1"}' --public-inputs '{"public_input": "1"}' --debug

result:

╭─────╮
│GATES│
╰─────╯

╭────────────────────────────────────────────────────────────────────────────────
│ GATE 0 - DoubleGeneric<1>
╭────────────────────────────────────────────────────────────────────────────────
│ FILE: examples/public_output.no
│────────────────────────────────────────────────────────────────────────────────
│ 1: fn main(pub public_input: Field, private_input: Field) -> Field {
│                ^^^^^^^^^^^^
╰────────────────────────────────────────────────────────────────────────────────
    ▲
    ╰── add public input

╭────────────────────────────────────────────────────────────────────────────────
│ GATE 1 - DoubleGeneric<1,1,-1,0,0,1>
╭────────────────────────────────────────────────────────────────────────────────
│ FILE: examples/public_output.no
│────────────────────────────────────────────────────────────────────────────────
│ 2:     let xx = private_input + public_input;
│                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
╰────────────────────────────────────────────────────────────────────────────────
    ▲
    ╰── add two variables together

╭────────────────────────────────────────────────────────────────────────────────
│ GATE 2 - DoubleGeneric<1,0,-1,0,6,1,0,0,0,-2>
╭────────────────────────────────────────────────────────────────────────────────
│ FILE: examples/public_output.no
│────────────────────────────────────────────────────────────────────────────────
│ 4:     let yy = xx + 6;
│                 ^^^^^^
╰────────────────────────────────────────────────────────────────────────────────
    ▲
    ╰── add a constant with a variable

╭──────╮
│WIRING│
╰──────╯

╭────────────────────────────────────────────────────────────────────────────────
│ FILE: examples/public_output.no
│────────────────────────────────────────────────────────────────────────────────
│ 1: fn main(pub public_input: Field, private_input: Field) -> Field {
│                ^^^^^^^^^^^^
╭────────────────────────────────────────────────────────────────────────────────
│ FILE: examples/public_output.no
│────────────────────────────────────────────────────────────────────────────────
│ 2:     let xx = private_input + public_input;
│                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
╰────────────────────────────────────────────────────────────────────────────────
(0,0) -> (1,1)

╭────────────────────────────────────────────────────────────────────────────────
│ FILE: examples/public_output.no
│────────────────────────────────────────────────────────────────────────────────
│ 2:     let xx = private_input + public_input;
│                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
╭────────────────────────────────────────────────────────────────────────────────
│ FILE: examples/public_output.no
│────────────────────────────────────────────────────────────────────────────────
│ 4:     let yy = xx + 6;
│                 ^^^^^^
╭────────────────────────────────────────────────────────────────────────────────
│ FILE: examples/public_output.no
│────────────────────────────────────────────────────────────────────────────────
│ 4:     let yy = xx + 6;
│                 ^^^^^^
╰────────────────────────────────────────────────────────────────────────────────
(1,2) -> (2,0) -> (2,3)