Support R1CS #52

katat · 2024-04-26T04:15:31Z

snarkjs testing workflow

Here are the commands to verify the whole process.

# create new noname package. this will create a new folder test, containing the noname code.
cargo run new -p test

# trigger the noname run subcommand to generate .r1cs and .wtns binary files
cargo run run --backend r1cs --path test --private-inputs '{"yy": "1"}' --public-inputs '{"xx": "2"}'

# check the consistency between the witness and r1cs constraints via snarkjs
snarkjs wchk test/output.r1cs test/output.wtns


# for generating a proof and verify with it via snarkjs
snarkjs powersoftau new bls12-381 12 pot12_0000.ptau -v
snarkjs powersoftau contribute pot12_0000.ptau pot12_0001.ptau --name="First contribution" -v
snarkjs powersoftau prepare phase2 pot12_0001.ptau pot12_final.ptau -v
snarkjs groth16 setup test/output.r1cs pot12_final.ptau test_0000.zkey
snarkjs zkey contribute test_0000.zkey test_0001.zkey --name="1st Contributor Name" -v
snarkjs zkey export verificationkey test_0001.zkey verification_key.json
snarkjs groth16 prove test_0001.zkey test/output.wtns proof.json public.json
snarkjs groth16 verify verification_key.json public.json proof.json


# at the end, it should display "snarkJS: OK!"

Missing meta data

It currently doesn't store the number of outputs and private inputs to the r1cs file.
Maybe we can shift and have the backend store the public outputs and private inputs?
Either we can pass these meta data from the circuit writer or from within backend. The latter approach seems cleaner.

witness data arrangement

snarkjs expect the public inputs are arranged at first. This is crucial for generating the correct proving index.
Make sure the public inputs are always arranged at first (relating to how the new vars are recorded in witness_vars)

constraint public inputs / outputs

in kimchi backend, it needs to add constraints that will be cancelled by the verifier.
research: it seems we don't need to do this in r1cs as long as the public inputs can be correctly recognized from the witness data

Implement finalize_circuit interface

what do we need to check before finalizing it?

mimoo

This looks really great! I left you a few comments. But the important ones:

did we forget to constrain the returned CellVars with the public output CellVars o_O? https://zksecurity.github.io/noname/public-outputs.html doesn't even mention it ;_;
it'd be nice to document the snarkjs expected serialization for .r1cs and .witness, maybe in the book?
I don't think we should use a hashmap for the symbolic witness vector, I think we can simplify that a lot

src/tests/examples.rs

src/backends/r1cs/mod.rs

mimoo · 2024-04-26T22:23:52Z

src/backends/r1cs/mod.rs

+        var
+    }
+
+    fn add_constant(


add_constant doesn't make sense in r1cs, I guess we should discuss in #34 how we can remove it

src/backends/r1cs/mod.rs

src/backends/r1cs/builtin.rs

src/backends/r1cs/mod.rs

mimoo · 2024-05-01T09:27:38Z

src/backends/r1cs/mod.rs

+        let c = LinearCombination {
+            terms: Some(HashMap::from_iter(vec![(res, one)])),
+            constant: None,
+        };


LinearCombination::from_var(res) would be cleaner

implemented from_vars :D

src/backends/r1cs/mod.rs

src/cli/cmd_build_and_check.rs

mimoo · 2024-05-03T15:09:44Z

src/backends/r1cs/mod.rs

+        }
+    }
+
+    // todo: how can we create this r1cs backend with different associated field types, but still using the same backend implementation? using macro?


I don't think you need to use macro, you could just have a R1CS struct generic on the prime, and then instantiate it in two different backends.

src/backends/r1cs/mod.rs

mimoo · 2024-05-03T15:16:28Z

src/backends/r1cs/mod.rs

+        // generate witness through witness vars vector
+        let mut witness = self.witness_vars.iter().enumerate().map(|(index, val)| {
+            self.compute_val(witness_env, val, index)
+        }).collect::<crate::error::Result<Vec<Fr>>>()?;


wait so, my understanding is that either the public_output values are Value::PublicOutput(None), in which case it will crash. Or they are set, in which case they will be calculated correctly at this point.

If the circuit is finalized, they should be set, so we shouldn't have to compute them after no (which is what you do after)?

The public output cell is replaced in the finalize_circuit:

noname/src/backends/r1cs/mod.rs

Lines 215 to 221 in 77e4409

for (pub_var, ret_var) in cvars.clone().iter().zip(returned_cells.unwrap()) {

// replace the computation of the public output vars with the actual variables being returned here

let var_idx = pub_var.idx().unwrap();

let prev = &self.witness_vars[var_idx];

assert!(matches!(prev, Value::PublicOutput(None)));

self.witness_vars[var_idx] = Value::PublicOutput(Some(ret_var));

}

So actually they can be calculated directly via this line of code, and the following lines from generate_witness are not necessary any more:

noname/src/backends/r1cs/mod.rs

Lines 266 to 269 in 77e4409

for var in &self.public_outputs {

let val = self.compute_var(witness_env, *var)?;

witness[var.index] = val;

}

maybe my reasoning in the below comment makes sense?

mimoo · 2024-05-03T15:17:33Z

src/backends/r1cs/mod.rs

+        // so we need to compute them separately
+        for var in &self.public_outputs {
+            let val = self.compute_var(witness_env, *var)?;
+            witness[var.index] = val;


so I think this is unnecessary, I guess you can quickly check this by checking if the public_output.no leads to the same witness with this line or without (or if the witness verifies without this line)

OK so thinking more about it, I think I understand why I did this in noname (I really should have documented that).

I think it I compute the public output before everything else, it might end up recursing A LOT as it needs to compute the whole main function to compute the value of the public output. So by deferring we can just make use of the cache to compute the public output and avoid recursing. (I think we should add a comment to explain that in both kimchi and R1CS if we do this ^^)

so in the map above, I think we should just insert 0s if it's a publicoutput, otherwise call compute_val. Then we do that loop here^

wdyt?

it might end up recursing A LOT as it needs to compute the whole main function to compute the value of the public output

Because there will be caches created for most of vars when the calculation of the public output triggers the chain of calculations, does that mean the performance gain actually isn't that much for deferring these output calculation until the end of witness generation?

If so, maybe it is simpler to just remove the following code(the redundant calculation), so we can avoid a bit of this intricated assumption?

noname/src/backends/r1cs/mod.rs

Lines 262 to 267 in 6c99128

// The original vars of public outputs are not part of the constraints

// so we need to compute them separately

for var in &self.public_outputs {

let val = self.compute_var(witness_env, *var)?;

witness[var.index] = val;

}

no I think we should def defer the computation, as the compute_val will recurse too much otherwise (it would be fine if the implementation was not recursive or didn't use too much memory, but atm it doesn't make sense to not defer IMO).

Because at the point where we call it there is no cache yet (you can probably see that by step debugging with that change)

src/backends/r1cs/mod.rs

mimoo

Everything looks great, besides the public output computation not being deferred. So I think this is approvable now :) feel free to merge and fix things later!

mimoo · 2024-05-06T07:49:30Z

src/witness.rs

@@ -21,7 +20,7 @@ where
 {
    pub var_values: HashMap<String, Vec<F>>,

-    pub cached_values: HashMap<CellVar, F>,


note that this change is a tiny bit annoying because we're exposing usize to the frontend, which for the frontend doesn't mean much. IMO we should try to keep exposing CellVar, especially as we might make future changes that might expose a different CellVar depending on the backend.

I've looked a bit more at the implementation of the compute_val and I think we could call compute_var instead (by recreating a CellVar potentially, or storing a CellVar in the right place instead of a usize.

Also I'm not sure I understand why compute_var and compute_val return an Result :D it looks like it's only for the public output case, but I'm wondering if we can actually reach that path.

Anyway it's not really related to this PR at this point.

mimoo · 2024-05-06T08:02:44Z

src/backends/r1cs/mod.rs

+        }
+
+        // check if every cell vars end up being a cell var in the circuit or public output
+        for index in 0..self.witness_vars.len() {


dangerous! always use iterators (for witness_var in &self.witness_vars)

katat · 2024-05-07T02:04:09Z

Updated to defer the output calculation and optimize the circuit finalization.

katat force-pushed the rebase/basic-constraints-r1cs branch 3 times, most recently from 739b5fa to 207636f Compare April 29, 2024 04:19

katat changed the base branch from rebase/basic-constraints to main May 1, 2024 04:39

katat force-pushed the rebase/basic-constraints-r1cs branch from 1fc6da1 to 74944e6 Compare May 1, 2024 04:40

katat added 5 commits May 1, 2024 12:42

fix: avoid the associated type PrettyField that relies on kimchi lib.

7412f85

Add R1CS bls12_381 backend

da6be3d

Apply same set of tests to r1cs backend

316a2cf

Add SnarkjsExporter to generate .r1cs and .wtns files in snarkjs format

a150531

Update noname run command to generate circuit and witness

239ae52

katat force-pushed the rebase/basic-constraints-r1cs branch from 74944e6 to 239ae52 Compare May 1, 2024 04:45

mimoo reviewed May 1, 2024

View reviewed changes

katat added 8 commits May 2, 2024 14:39

remove the use of option in lc

4409086

refactor witness_var interface

f25236a

refactor witness vars in r1cs to vector

f785e3d

fix: witness map

a81b687

add compute_val to simplify computation for symbolic vars

530d2b4

fix docs

34308da

add impls for lc

77e4409

update cmd

d760fe2