feat: Allow array of fields on public output

[erhant]

Here is my humble attempt at #130. I have added a test & it seems to compile & pass.

• Resolves #130
• Changes type of public outputs within generate_witness of Kimchi backend to use BTreeMap instead of HashMap to guarantee ordering at the final output

[erhant]

I tried the following circuit:

fn main(pub public_input: Bool, private_input: Bool) -> [Bool; 3] {
    // constants
    let xx = false && false;
    assert(!xx);

    // private input must be true
    let yy = private_input && true;
    assert(!yy);

    // public input must be false
    let zz = public_input && true;
    assert(zz);

    return [!yy, yy, zz];
}

with commands:

cargo run test -p examples/bool_output_array.no --public-inputs '{"public_input": true}' --private-inputs '{"private_input": false}' --backend kimchi-vesta

cargo run test -p examples/bool_output_array.no --public-inputs '{"public_input": true}' --private-inputs '{"private_input": false}' --backend r1cs-bls12-381

and it seems to compile fine! The outputs are:

@ noname.0.7.0

DoubleGeneric<1>
DoubleGeneric<1>
DoubleGeneric<1>
DoubleGeneric<1>
DoubleGeneric<1,0,-1,0,-1>
DoubleGeneric<0,0,-1,1>
DoubleGeneric<1>
DoubleGeneric<1,0,-1,0,-1>
DoubleGeneric<0,0,-1,1>
DoubleGeneric<1>
DoubleGeneric<1,1>
DoubleGeneric<1,0,-1,0,1>
DoubleGeneric<1,0,0,0,-1>
DoubleGeneric<1,0,0,0,-1>
DoubleGeneric<1,1>
DoubleGeneric<1,0,-1,0,1>
DoubleGeneric<1,-1>
DoubleGeneric<1,-1>
DoubleGeneric<1,-1>
(0,0) -> (16,0)
(1,0) -> (17,0)
(2,0) -> (18,0)
(3,0) -> (4,0) -> (5,0) -> (13,0) -> (18,1)
(4,2) -> (5,1)
(5,2) -> (6,0)
(7,0) -> (8,0) -> (10,0) -> (14,0) -> (17,1)
(7,2) -> (8,1)
(8,2) -> (9,0)
(10,1) -> (11,0)
(11,2) -> (12,0)
(14,1) -> (15,0)
(15,2) -> (16,1)

and

@ noname.0.7.0

v_5 == (v_4) * (v_4 + -1)
0 == (v_5) * (1)
v_7 == (v_6) * (v_6 + -1)
0 == (v_7) * (1)
1 == (-1 * v_6 + 1) * (1)
1 == (v_4) * (1)
-1 * v_6 + 1 == (v_1) * (1)
v_6 == (v_2) * (1)
v_4 == (v_3) * (1)

Will try with a custom type in a moment!

[erhant]

struct Thing {
    xx: Field,
    yy: Field,
}

fn main(pub xx: Field, pub yy: Field) -> [Thing; 2] {
    let thing1 = Thing {
        xx: 1,
        yy: 2,
    };
    let thing2 = Thing {
        xx: 3,
        yy: 4,
    };
    let things = [thing1, thing2];

    assert_eq(things[0].xx, xx);
    assert_eq(things[1].yy, yy);

    return things;
}

this one works as well^

[erhant]

Have to admit that by "work" I only mean it compiles & a proof is generated and verified, not sure if there are some soundness on the backend side errors due to the way this is implemented 🤔

[mimoo]

So Bool will work because a Bool is essentially a Field underneath it. Your second example should not work properly because it will allocate only 2 Fields when it should actually allocate 4 Fields (unless I'm missing something). This should be visible with a debug output (altho I think we don't have labels for r1cs, but the debug output of kimchi might show it better).

Can you post the r1cs debut output just for completeness as a comment here :D?

[erhant]

So Bool will work because a Bool is essentially a Field underneath it.

ah indeed!

Can you post the r1cs debut output just for completeness as a comment here :D?

I dont know if I was dreaming yesterday (it was kinda late), but today I got the error:

Error:   × Looks like something went wrong in constraint-generation
    ╭─[examples/types_array_output.no:14:1]
 14 │     };
 15 │     let things = [thing1, thing2];
    ·                  ────────┬───────
    ·                          ╰── here
 16 │     
    ╰────
  help: the public output cannot contain constants

After changing the circuit as below:

  struct Thing {
    xx: Field,
    yy: Field,
}

fn main(pub xx: Field, pub yy: Field) -> [Thing; 2] {
    let thing1 = Thing {
        xx: xx,
        yy: 1 + yy,
    };
    let thing2 = Thing {
        xx: 1 + xx,
        yy: yy,
    };
    let things = [thing1, thing2];

    assert_eq(things[0].xx, xx);
    assert_eq(things[1].yy, yy);

    return things;
}

the resulting R1CS is:

@ noname.0.7.0

v_3 == (v_3) * (1)
v_4 == (v_4) * (1)
v_3 == (v_1) * (1)
v_4 + 1 == (v_2) * (1)

Indeed it is not sized properly, and a test shows that only the fields of thing1 are included in the output. I will try to tackle it 🙏🏻

[erhant]

Indeed recursing into items was a bit too much, I've added a check to only allow Field and Bool for now.

[mimoo]

there's also a sizeof or size_of function somewhere, do you think you could just use that to make it work with everything?

[erhant]

there's also a sizeof or size_of function somewhere, do you think you could just use that to make it work with everything?

yea that seems to solve things (just pushed), I simply get the size of the returned type and add that many public outputs to the circuit.

However, there is still the issue of order of the public outputs during tests, it appears to be randomly shuffled (?) everytime, I will write a separate test for this real quick.

[erhant]

However, there is still the issue of order of the public outputs during tests, it appears to be randomly shuffled (?) everytime, I will write a separate test for this real quick.

The issue seems to be about Kimchi backend, not R1CS. I further found the reason why, its this here: https://github.com/zksecurity/noname/blob/main/src/backends/kimchi/mod.rs#L428

Iterating the hashmap does not guarantee order, so testing the public outputs randomly fails.

[erhant]

I made it use BTreeMap instead, which guarantees order; I made the ordering respect the index of the cell only, I think that is alright?