Arkworks adapter for Groth16 Backend (#701)

* csv -> qap * load from csv * works but for what * roll back to beginning * Revert "works but for what" This reverts commit b1fc5b5. * Revert "load from csv" This reverts commit 015a1b8. * Revert "csv -> qap" This reverts commit d4700e6. * arkworks-adapter-init * more examples * bugfix + linear exponentiation example * minor refactor * reorg * reorg * clippy * readd winterfell * added readme to the adapter * Update README.md * make clippy happy * extract_witness_from_arkworks_cs more clear * almost all reviews done * remove unnecessary "1" * get rid of unecessary "1"s * failing test * Add docs to "arkworks_cs_to_lambda_cs" * add move test utils to correct place + #[cfg(test)] --------- Co-authored-by: Mauro Toscano <[email protected]> Co-authored-by: Diego K <[email protected]>
lambdaclass · Jan 5, 2024 · 5f3ffd2 · 5f3ffd2
1 parent 86c7efa
commit 5f3ffd2
Show file tree

Hide file tree

Showing 14 changed files with 606 additions and 119 deletions.
diff --git a/Cargo.toml b/Cargo.toml
@@ -1,5 +1,6 @@
 [workspace]
-members = ["math", "crypto", "gpu", "benches", "provers/plonk", "provers/stark", "provers/cairo", "provers/groth16", "examples/merkle-tree-cli", "examples/prove-miden", "winterfell_adapter"]
+
+members = ["math", "crypto", "gpu", "benches", "provers/plonk", "provers/stark", "provers/cairo", "provers/groth16", "provers/groth16/arkworks-adapter", "examples/merkle-tree-cli", "examples/prove-miden", "winterfell_adapter"]
 exclude = ["ensure-no_std"]
 resolver = "2"
 

diff --git a/provers/groth16/README.md b/provers/groth16/README.md
@@ -1,3 +1,3 @@
 # Lambdaworks Groth16 Prover
 
-An incomplete and unoptimized implementation of the [Groth16](https://eprint.iacr.org/2016/260) protocol.
+An under-optimized implementation of [Groth16](https://eprint.iacr.org/2016/260) protocol.
diff --git a/provers/groth16/arkworks-adapter/Cargo.toml b/provers/groth16/arkworks-adapter/Cargo.toml
@@ -0,0 +1,19 @@
+[package]
+name = "arkworks_adapter"
+version.workspace = true
+edition.workspace = true
+license.workspace = true
+repository.workspace = true
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+lambdaworks-math = { path = "../../../math" }
+lambdaworks-groth16 = { path = "../" }
+ark-r1cs-std = { version = "^0.3.1"}
+ark-bls12-381 = { version = "0.4.0"}
+ark-ff = { version = "^0.4.2" }
+ark-relations = { version = "^0.4.0" }
+ark-serialize = {version = "0.4.2"}
+num-bigint = { version = "0.4", default-features = false }
+rand = "0.8.5"
diff --git a/provers/groth16/arkworks-adapter/README.md b/provers/groth16/arkworks-adapter/README.md
@@ -0,0 +1,84 @@
+# Arkworks Adapter for Lambdaworks Groth16 Backend
+
+This crate enables circuits written in Arkworks to be proven / verified via Lambdaworks Groth16 backend.
+
+Crate exposes [to_lambda](./src/lib.rs#to_lambda) function for <b><span style="color: #57a14d">ConstraintSystemRef</span></b> type of Arkworks, which is expected to carry all constraints, witnesses, and public variable assignments:
+
+```rust
+pub fn to_lambda<F: PrimeField>(cs: &ConstraintSystemRef<F>) -> (QuadraticArithmeticProgram, Vec<FrElement>)
+```
+
+It returns a Lambdaworks-compatible QAP struct alongside variable assignments. Please note that public variable assignments are bundled with witnesses, and this vector of field elements is called **witness** alltogether.
+
+```rust
+let (qap, w) = to_lambda(&cs);
+```
+
+After this point, typical steps of Groth16 can be performed using Lamdaworks: setup, prove, verify
+
+```rust
+let (pk, vk) = setup(&qap);
+
+let proof = Prover::prove(&w, &qap, &pk);
+
+let public_inputs = &w[..qap.num_of_public_inputs];
+let accept = verify(&vk, &proof, public_inputs);
+
+assert!(accept);
+```
+
+## Full Example
+
+A linear exponentiation example on BLS12-381 can be found here.
+Please check [integration_tests.rs](./src/integration_tests.rs) for more examples.
+
+```rust
+
+use crate::to_lambda;
+use ark_bls12_381::Fr;
+use ark_relations::{lc, r1cs::ConstraintSystem, r1cs::Variable};
+use lambdaworks_groth16::{setup, verify, Prover};
+use rand::Rng;
+
+// ...
+// ...
+
+let mut rng = rand::thread_rng();
+let x = rng.gen::<u64>();
+let exp = rng.gen::<u8>();
+
+// Define the circuit using Arkworks
+
+let cs = ConstraintSystem::<Fr>::new_ref();
+
+let x = Fr::from(x);
+let mut _x = cs.new_witness_variable(|| Ok(x)).unwrap();
+
+let mut acc = Fr::from(x);
+let mut _acc = cs.new_witness_variable(|| Ok(x)).unwrap();
+
+for _ in 0..exp - 1 {
+	acc *= x;
+	let _new_acc = cs.new_witness_variable(|| Ok(acc)).unwrap();
+	cs.enforce_constraint(lc!() + _acc, lc!() + _x, lc!() + _new_acc)
+		.unwrap();
+	_acc = _new_acc;
+}
+
+let _out = cs.new_input_variable(|| Ok(acc)).unwrap();
+cs.enforce_constraint(lc!() + _out, lc!() + Variable::One, lc!() + _acc)
+	.unwrap();
+
+// Make Lambdaworks-compatible
+let (qap, w) = to_lambda(&cs);
+
+// Use Lambdaworks Groth16 backend
+
+let (pk, vk) = setup(&qap);
+
+let proof = Prover::prove(&w, &qap, &pk);
+
+let public_inputs = &w[..qap.num_of_public_inputs];
+let accept = verify(&vk, &proof, public_inputs);
+assert!(accept);
+```
diff --git a/provers/groth16/arkworks-adapter/src/integration_tests.rs b/provers/groth16/arkworks-adapter/src/integration_tests.rs
@@ -0,0 +1,195 @@
+use crate::arkworks_cs_to_lambda_cs;
+use ark_bls12_381::Fr;
+use ark_relations::{lc, r1cs::ConstraintSystem, r1cs::Variable};
+use lambdaworks_groth16::{setup, verify, Prover, QuadraticArithmeticProgram};
+use rand::Rng;
+
+#[test]
+fn pinocchio_paper_example() {
+    /*
+        pub inp a, b, c, d
+        pub out result
+        sig e
+
+        c * d = e
+        (a + b) + e = result
+    */
+    let cs = ConstraintSystem::<Fr>::new_ref();
+
+    let _a = Fr::from(1555);
+    let _b = Fr::from(25555);
+    let _c = Fr::from(35555);
+    let _d = Fr::from(45555);
+
+    let a = cs.new_input_variable(|| Ok(_a)).unwrap();
+    let b = cs.new_input_variable(|| Ok(_b)).unwrap();
+    let c = cs.new_input_variable(|| Ok(_c)).unwrap();
+    let d = cs.new_input_variable(|| Ok(_d)).unwrap();
+
+    let e = cs.new_witness_variable(|| Ok(_c * _d)).unwrap();
+    cs.enforce_constraint(lc!() + c, lc!() + d, lc!() + e)
+        .unwrap();
+
+    let result = cs.new_input_variable(|| Ok(_c * _d * (_a + _b))).unwrap();
+
+    cs.enforce_constraint(lc!() + a + b, lc!() + e, lc!() + result)
+        .unwrap();
+
+    let lambda_cs = arkworks_cs_to_lambda_cs(&cs);
+
+    let qap = QuadraticArithmeticProgram::from_r1cs(lambda_cs.constraints);
+
+    let (pk, vk) = setup(&qap);
+
+    let accept = verify(
+        &vk,
+        &Prover::prove(&lambda_cs.witness, &qap, &pk),
+        &lambda_cs.witness[..qap.num_of_public_inputs],
+    );
+    assert!(accept);
+}
+
+#[test]
+fn vitalik_example() {
+    /*
+        pub out ~out
+        sig x, sym_1, y, sym_2
+
+        x * x = sym_1;
+        sym_1 * x = y;
+        (y + x) * 1 = sym_2
+        (sym_2 + 5) * 1 = ~out
+    */
+    let cs = ConstraintSystem::<Fr>::new_ref();
+
+    //["0x1", "0x3", "0x23", "0x9", "0x1b", "0x1e"]
+    let _x = Fr::from(3);
+    let _sym_1 = Fr::from(9);
+    let _y = Fr::from(27);
+    let _sym_2 = Fr::from(30);
+
+    let _out = Fr::from(35);
+
+    let x = cs.new_witness_variable(|| Ok(_x)).unwrap();
+    let sym_1 = cs.new_witness_variable(|| Ok(_sym_1)).unwrap();
+    let y = cs.new_witness_variable(|| Ok(_y)).unwrap();
+    let sym_2 = cs.new_witness_variable(|| Ok(_sym_2)).unwrap();
+
+    let out = cs.new_input_variable(|| Ok(_out)).unwrap();
+
+    cs.enforce_constraint(lc!() + x, lc!() + x, lc!() + sym_1)
+        .unwrap();
+    cs.enforce_constraint(lc!() + sym_1, lc!() + x, lc!() + y)
+        .unwrap();
+    cs.enforce_constraint(lc!() + y + x, lc!() + Variable::One, lc!() + sym_2)
+        .unwrap();
+    cs.enforce_constraint(
+        lc!() + sym_2 + (Fr::from(5), Variable::One),
+        lc!() + Variable::One,
+        lc!() + out,
+    )
+    .unwrap();
+
+    let lambda_cs = arkworks_cs_to_lambda_cs(&cs);
+
+    let qap = QuadraticArithmeticProgram::from_r1cs(lambda_cs.constraints);
+
+    let (pk, vk) = setup(&qap);
+
+    let accept = verify(
+        &vk,
+        &Prover::prove(&lambda_cs.witness, &qap, &pk),
+        &lambda_cs.witness[..qap.num_of_public_inputs],
+    );
+    assert!(accept);
+}
+
+#[test]
+fn failing_vitalik() {
+    // Same circuit as vitalik_example, but with an incorrect witness assignment.
+    let cs = ConstraintSystem::<Fr>::new_ref();
+
+    //["0x1", "0x3", "0x23", "0x9", "0x1b", "0x1e"]
+    let _x = Fr::from(3);
+    let _sym_1 = Fr::from(10); // should be have been 9
+    let _y = Fr::from(27);
+    let _sym_2 = Fr::from(30);
+
+    let _out = Fr::from(35);
+
+    let x = cs.new_witness_variable(|| Ok(_x)).unwrap();
+    let sym_1 = cs.new_witness_variable(|| Ok(_sym_1)).unwrap();
+    let y = cs.new_witness_variable(|| Ok(_y)).unwrap();
+    let sym_2 = cs.new_witness_variable(|| Ok(_sym_2)).unwrap();
+
+    let out = cs.new_input_variable(|| Ok(_out)).unwrap();
+
+    cs.enforce_constraint(lc!() + x, lc!() + x, lc!() + sym_1)
+        .unwrap();
+    cs.enforce_constraint(lc!() + sym_1, lc!() + x, lc!() + y)
+        .unwrap();
+    cs.enforce_constraint(lc!() + y + x, lc!() + Variable::One, lc!() + sym_2)
+        .unwrap();
+    cs.enforce_constraint(
+        lc!() + sym_2 + (Fr::from(5), Variable::One),
+        lc!() + Variable::One,
+        lc!() + out,
+    )
+    .unwrap();
+
+    let lambda_cs = arkworks_cs_to_lambda_cs(&cs);
+
+    let qap = QuadraticArithmeticProgram::from_r1cs(lambda_cs.constraints);
+
+    let (pk, vk) = setup(&qap);
+
+    let accept = verify(
+        &vk,
+        &Prover::prove(&lambda_cs.witness, &qap, &pk),
+        &lambda_cs.witness[..qap.num_of_public_inputs],
+    );
+    assert!(!accept);
+}
+
+#[test]
+fn exponentiation_example() {
+    /*
+        Generates a "linear exponentiation" circuit with a random base and a random exponent.
+        Only the output ~out is public input.
+    */
+    let cs = ConstraintSystem::<Fr>::new_ref();
+
+    let mut rng = rand::thread_rng();
+    let x = rng.gen::<u64>();
+    let exp = rng.gen::<u8>(); // Bigger data types take too much time for a test
+
+    let x = Fr::from(x);
+    let mut _x = cs.new_witness_variable(|| Ok(x)).unwrap();
+
+    let mut acc = Fr::from(x);
+    let mut _acc = cs.new_witness_variable(|| Ok(x)).unwrap();
+
+    for _ in 0..exp - 1 {
+        acc *= x;
+        let _new_acc = cs.new_witness_variable(|| Ok(acc)).unwrap();
+        cs.enforce_constraint(lc!() + _acc, lc!() + _x, lc!() + _new_acc)
+            .unwrap();
+        _acc = _new_acc;
+    }
+
+    let _out = cs.new_input_variable(|| Ok(acc)).unwrap();
+    cs.enforce_constraint(lc!() + _out, lc!() + Variable::One, lc!() + _acc)
+        .unwrap();
+
+    let lambda_cs = arkworks_cs_to_lambda_cs(&cs);
+
+    let qap = QuadraticArithmeticProgram::from_r1cs(lambda_cs.constraints);
+
+    let (pk, vk) = setup(&qap);
+
+    let proof = Prover::prove(&lambda_cs.witness, &qap, &pk);
+
+    let public_inputs = &lambda_cs.witness[..qap.num_of_public_inputs];
+    let accept = verify(&vk, &proof, public_inputs);
+    assert!(accept);
+}