feat: Allow array of fields on public output #131

erhant · 2024-06-19T18:16:38Z

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

Resolves Array as public output #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

mimoo · 2024-06-19T22:23:20Z

src/circuit_writer/mod.rs

+                TyKind::Field => {
+                    circuit_writer.add_public_outputs(1, typ.span);
+                }
+                TyKind::Array(_, len) => {


I don't think this is correct as this won't work if you have [T; len] for T a different type than Field.

I think a quick fix here could be to match for TyKind::Array(TyKind::Field, len) or to actually recurse and figure out the real size (akin to the size_of function), but this would be out of the scope of this issue and perhaps a tad more complicated :o

erhant · 2024-06-19T22:31:37Z

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 · 2024-06-19T22:35:10Z

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 · 2024-06-19T22:37:18Z

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 · 2024-06-20T00:33:32Z

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 · 2024-06-20T08:01:16Z

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 · 2024-06-20T09:00:46Z

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

mimoo · 2024-06-20T15:54:42Z

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

mimoo · 2024-06-20T16:01:04Z

examples/fixture/asm/r1cs/public_output_array.asm

+2 == (v_3 + v_4) * (1)
+v_5 == (v_3 + v_4) * (v_3)
+v_3 + v_4 + 6 == (v_1) * (1)
+v_5 == (v_2) * (1)


^ this last constraint seems really useless, we should optimize that, I'll create an issue :)

Do you mean the second constraint should be instead
v_2 = (v_3 + v_4) * (v_3)?

v_1 and v_2 are the outputs and they have to be constrained

yeah! v_2 == (v_3 + v_4) * v_3 would have been better. But I don't think we should look to create such optimization, because an optimization pass that would do inlining would easily inline the last constraint

erhant · 2024-06-20T16:45:50Z

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 · 2024-06-20T16:57:28Z

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 · 2024-06-20T17:06:24Z

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?

src/backends/kimchi/mod.rs

mimoo

thanks so much for the PR :) !!

erhant added 2 commits June 19, 2024 21:11

allow array of fields on public output

4a4fb69

remove comment / log and redundant clones

c879418

mimoo reviewed Jun 19, 2024

View reviewed changes

allow only fields and bools for the array output

3aa65fb

mimoo reviewed Jun 20, 2024

View reviewed changes

public output respects the size of returned type

6d7f689

use BTreeMap instead of HashMap for Kimchi public outputs

30f31ab

mimoo reviewed Jun 20, 2024

View reviewed changes

src/backends/kimchi/mod.rs Outdated Show resolved Hide resolved

use educe(PartialOrd) instead of impl

f6a563d

mimoo approved these changes Jun 21, 2024

View reviewed changes

mimoo merged commit 96cd1f1 into zksecurity:main Jun 21, 2024
1 check passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: Allow array of fields on public output #131

feat: Allow array of fields on public output #131

erhant commented Jun 19, 2024 •

edited

Loading

mimoo Jun 19, 2024

erhant commented Jun 19, 2024

erhant commented Jun 19, 2024

erhant commented Jun 19, 2024

mimoo commented Jun 20, 2024 •

edited

Loading

erhant commented Jun 20, 2024

erhant commented Jun 20, 2024

mimoo commented Jun 20, 2024

mimoo Jun 20, 2024

katat Jun 20, 2024

mimoo Jun 21, 2024

erhant commented Jun 20, 2024 •

edited

Loading

erhant commented Jun 20, 2024 •

edited

Loading

erhant commented Jun 20, 2024

mimoo left a comment

feat: Allow array of fields on public output #131

feat: Allow array of fields on public output #131

Conversation

erhant commented Jun 19, 2024 • edited Loading

mimoo Jun 19, 2024

Choose a reason for hiding this comment

erhant commented Jun 19, 2024

erhant commented Jun 19, 2024

erhant commented Jun 19, 2024

mimoo commented Jun 20, 2024 • edited Loading

erhant commented Jun 20, 2024

erhant commented Jun 20, 2024

mimoo commented Jun 20, 2024

mimoo Jun 20, 2024

Choose a reason for hiding this comment

katat Jun 20, 2024

Choose a reason for hiding this comment

mimoo Jun 21, 2024

Choose a reason for hiding this comment

erhant commented Jun 20, 2024 • edited Loading

erhant commented Jun 20, 2024 • edited Loading

erhant commented Jun 20, 2024

mimoo left a comment

Choose a reason for hiding this comment

erhant commented Jun 19, 2024 •

edited

Loading

mimoo commented Jun 20, 2024 •

edited

Loading

erhant commented Jun 20, 2024 •

edited

Loading

erhant commented Jun 20, 2024 •

edited

Loading