Skip to content

Commit

Permalink
Update range check (#132)
Browse files Browse the repository at this point in the history 
* feat: update `rangeCheckChip`

* feat: add printing

* feat: add `N_BYTES` generic to `MerkleSumTree`, `MstInclusionCircuit`, `SolvencyCircuit` and `Snapshot`

* fix: modified logic of range chip

* fix: `RangeCheckChip` config in syntesize

* test: add integration test for range check

* chore: move `enable_constant` out of poseidon chip

It doesn't change anything, but I think it's clearer to define all the column configuration within the `configure` function of the circuit

* fix: remove unnecessary selector

* chore: update printing

* fix: minor

* fix: clearer constraint on `zs` length equal to `N_BYTES + 1`

* test: fix

* chore: naming

* benches: update
  • Loading branch information
@enricobottazzi
enricobottazzi authored Aug 11, 2023
1 parent 38997c8 commit 56f28ee
Show file tree
Hide file tree
Showing 26 changed files with 868 additions and 915 deletions.
5 changes: 3 additions & 2 deletions backend/examples/verify_inclusion.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,14 +29,15 @@ where
fn main() {
const LEVELS: usize = 4;
const N_ASSETS: usize = 2;
const N_BYTES: usize = 8;

let ptau_path = "./ptau/hermez-raw-11";
let signature_csv_path = "./examples/signatures.csv";
let entry_csv_path = "../zk_prover/src/merkle_sum_tree/csv/entry_16.csv";

// CEX Generate the Merkle Sum Tree and then initialize the circuit.
// Note that `signature_csv` is empty because this is only needed to generate π of Solvency, which is not the case here.
let snapshot = Snapshot::<LEVELS, N_ASSETS>::new(
let snapshot = Snapshot::<LEVELS, N_ASSETS, N_BYTES>::new(
&entry_csv_path,
&signature_csv_path,
"Summa proof of solvency for CryptoExchange".to_string(),
Expand Down Expand Up @@ -83,7 +84,7 @@ fn main() {
generate_leaf_hash::<N_ASSETS>(user_name.clone(), balances_usize.clone())
);

let mst_inclusion_circuit = MstInclusionCircuit::<LEVELS, N_ASSETS>::init_empty();
let mst_inclusion_circuit = MstInclusionCircuit::<LEVELS, N_ASSETS, N_BYTES>::init_empty();

// The CEX can serve the params and vk by using the get_trusted_setup_for_mst_inclusion() method from the snapshot instance, as shown below:
// let (params, _, vk) = snapshot.get_trusted_setup_for_mst_inclusion();
Expand Down
27 changes: 15 additions & 12 deletions backend/src/apis/snapshot.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,8 +22,8 @@ use summa_solvency::{

use crate::apis::csv_parser::parse_signature_csv;

pub struct Snapshot<const LEVELS: usize, const N_ASSETS: usize> {
mst: MerkleSumTree<N_ASSETS>,
pub struct Snapshot<const LEVELS: usize, const N_ASSETS: usize, const N_BYTES: usize> {
mst: MerkleSumTree<N_ASSETS, N_BYTES>,
proof_of_address_ownership: AddressOwnershipProof,
trusted_setup: [SetupArtifcats; 2], // the first trusted setup relates to MstInclusionCircuit, the second related to SolvencyCircuit
}
Expand Down Expand Up @@ -87,7 +87,8 @@ impl AddressOwnershipProof {
}
}

impl<const LEVELS: usize, const N_ASSETS: usize> Snapshot<LEVELS, N_ASSETS>
impl<const LEVELS: usize, const N_ASSETS: usize, const N_BYTES: usize>
Snapshot<LEVELS, N_ASSETS, N_BYTES>
where
[usize; N_ASSETS + 1]: Sized,
[usize; 2 * (1 + N_ASSETS)]: Sized,
Expand All @@ -97,13 +98,13 @@ where
signature_csv_path: &str,
message: String,
params_path: &str,
) -> Result<Snapshot<LEVELS, N_ASSETS>, Box<dyn std::error::Error>> {
) -> Result<Snapshot<LEVELS, N_ASSETS, N_BYTES>, Box<dyn std::error::Error>> {
let (addresses, signatures) = parse_signature_csv(signature_csv_path).unwrap();

let mst: MerkleSumTree<N_ASSETS> = MerkleSumTree::<N_ASSETS>::new(entry_csv_path).unwrap();
let mst = MerkleSumTree::<N_ASSETS, N_BYTES>::new(entry_csv_path).unwrap();

let mst_inclusion_circuit = MstInclusionCircuit::<LEVELS, N_ASSETS>::init_empty();
let solvency_circuit = SolvencyCircuit::<N_ASSETS>::init_empty();
let mst_inclusion_circuit = MstInclusionCircuit::<LEVELS, N_ASSETS, N_BYTES>::init_empty();
let solvency_circuit = SolvencyCircuit::<N_ASSETS, N_BYTES>::init_empty();

// get k from ptau file name
let parts: Vec<&str> = params_path.split("-").collect();
Expand Down Expand Up @@ -140,7 +141,7 @@ where
yul_output_path: &str,
sol_output_path: &str,
) -> Result<(), Box<dyn std::error::Error>> {
let _deployment_code = gen_evm_verifier_shplonk::<SolvencyCircuit<N_ASSETS>>(
let _deployment_code = gen_evm_verifier_shplonk::<SolvencyCircuit<N_ASSETS, N_BYTES>>(
&self.trusted_setup[1].0,
&self.trusted_setup[1].2,
vec![1 + N_ASSETS],
Expand All @@ -157,7 +158,7 @@ where
asset_contract_addresses: Vec<String>,
asset_sums: [Fp; N_ASSETS],
) -> Result<(SolvencyProof, Vec<String>), &'static str> {
let circuit = SolvencyCircuit::<N_ASSETS>::init(self.mst.clone(), asset_sums);
let circuit = SolvencyCircuit::<N_ASSETS, N_BYTES>::init(self.mst.clone(), asset_sums);

let calldata = gen_proof_solidity_calldata(
&self.trusted_setup[1].0,
Expand All @@ -178,7 +179,8 @@ where
&self,
user_index: usize,
) -> Result<MstInclusionProof, &'static str> {
let circuit = MstInclusionCircuit::<LEVELS, N_ASSETS>::init(self.mst.clone(), user_index);
let circuit =
MstInclusionCircuit::<LEVELS, N_ASSETS, N_BYTES>::init(self.mst.clone(), user_index);

let proof = full_prover(
&self.trusted_setup[0].0,
Expand Down Expand Up @@ -212,12 +214,13 @@ mod tests {

const N_ASSETS: usize = 2;
const LEVELS: usize = 4;
const N_BYTES: usize = 8;

fn initialize_snapshot() -> Snapshot<LEVELS, N_ASSETS> {
fn initialize_snapshot() -> Snapshot<LEVELS, N_ASSETS, N_BYTES> {
let entry_csv = "../zk_prover/src/merkle_sum_tree/csv/entry_16.csv";
let signature_csv = "src/apis/csv/signatures.csv";

Snapshot::<LEVELS, N_ASSETS>::new(
Snapshot::<LEVELS, N_ASSETS, N_BYTES>::new(
entry_csv,
signature_csv,
"Summa proof of solvency for CryptoExchange".to_string(),
Expand Down
6 changes: 3 additions & 3 deletions zk_prover/README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ To build, test and print the circuits, execute

```
cargo build
cargo test --release --features dev-graph -- --nocapture
cargo test --release --features dev-graph
```
## Documentation

Expand Down Expand Up @@ -79,13 +79,13 @@ For Merkle Sum Tree Proof of Inclusion circuit

| VK Gen | Pk Gen | Proof Generation | Proof Verification | Proof Size (bytes) |
| ------------------ | ------------------- | ------------------- | ------------------- | ------------------ |
| 176.05 ms | 122.75 ms | 473.98 ms | 3.8 ms | 1856 |
| 176.05 ms | 122.75 ms | 473.98 ms | 3.8 ms | 1632 |

For Proof of Solvency circuit

| VK Gen | Pk Gen | Proof Generation | Proof Verification | Proof Size (bytes) |
| ------ | ------ | ---------------- | ------------------ | ------------------ |
| 63.22 ms | 27.075 ms | 133.82 ms | 3.4476 ms | 1760 (-36.05%) |
| 63.22 ms | 27.075 ms | 133.82 ms | 3.4476 ms | 1760 |

Gas cost to verify proof of solvency

Expand Down
35 changes: 18 additions & 17 deletions zk_prover/benches/full_solvency_flow.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ const SAMPLE_SIZE: usize = 10;
const LEVELS: usize = 15;
const N_ASSETS: usize = 2;
const PATH_NAME: &str = "two_assets";
const N_BYTES: usize = 8;

fn build_mstree(_c: &mut Criterion) {
let mut criterion = Criterion::default().sample_size(SAMPLE_SIZE);
Expand All @@ -34,15 +35,15 @@ fn build_mstree(_c: &mut Criterion) {

criterion.bench_function(&bench_name, |b| {
b.iter(|| {
MerkleSumTree::<N_ASSETS>::new(&csv_file).unwrap();
MerkleSumTree::<N_ASSETS, N_BYTES>::new(&csv_file).unwrap();
})
});
}

fn verification_key_gen_mst_inclusion_circuit(_c: &mut Criterion) {
let mut criterion = Criterion::default().sample_size(SAMPLE_SIZE);

let empty_circuit = MstInclusionCircuit::<LEVELS, N_ASSETS>::init_empty();
let empty_circuit = MstInclusionCircuit::<LEVELS, N_ASSETS, N_BYTES>::init_empty();

let (params, _, _) = generate_setup_artifacts(13, None, empty_circuit.clone()).unwrap();

Expand All @@ -60,7 +61,7 @@ fn verification_key_gen_mst_inclusion_circuit(_c: &mut Criterion) {
fn proving_key_gen_mst_inclusion_circuit(_c: &mut Criterion) {
let mut criterion = Criterion::default().sample_size(SAMPLE_SIZE);

let empty_circuit = MstInclusionCircuit::<LEVELS, N_ASSETS>::init_empty();
let empty_circuit = MstInclusionCircuit::<LEVELS, N_ASSETS, N_BYTES>::init_empty();

let (params, _, vk) = generate_setup_artifacts(13, None, empty_circuit.clone()).unwrap();

Expand All @@ -78,7 +79,7 @@ fn proving_key_gen_mst_inclusion_circuit(_c: &mut Criterion) {
fn generate_zk_proof_mst_inclusion_circuit(_c: &mut Criterion) {
let mut criterion = Criterion::default().sample_size(SAMPLE_SIZE);

let empty_circuit = MstInclusionCircuit::<LEVELS, N_ASSETS>::init_empty();
let empty_circuit = MstInclusionCircuit::<LEVELS, N_ASSETS, N_BYTES>::init_empty();

let (params, pk, vk) = generate_setup_artifacts(13, None, empty_circuit).unwrap();

Expand All @@ -87,10 +88,10 @@ fn generate_zk_proof_mst_inclusion_circuit(_c: &mut Criterion) {
PATH_NAME, PATH_NAME, LEVELS
);

let merkle_sum_tree = MerkleSumTree::<N_ASSETS>::new(&csv_file).unwrap();
let merkle_sum_tree = MerkleSumTree::<N_ASSETS, N_BYTES>::new(&csv_file).unwrap();

// Only now we can instantiate the circuit with the actual inputs
let circuit = MstInclusionCircuit::<LEVELS, N_ASSETS>::init(merkle_sum_tree, 0);
let circuit = MstInclusionCircuit::<LEVELS, N_ASSETS, N_BYTES>::init(merkle_sum_tree, 0);

let bench_name = format!(
"generate zk proof - tree of 2 power of {} entries with {} assets mst inclusion circuit",
Expand All @@ -106,7 +107,7 @@ fn generate_zk_proof_mst_inclusion_circuit(_c: &mut Criterion) {
fn verify_zk_proof_mst_inclusion_circuit(_c: &mut Criterion) {
let mut criterion = Criterion::default().sample_size(SAMPLE_SIZE);

let empty_circuit = MstInclusionCircuit::<LEVELS, N_ASSETS>::init_empty();
let empty_circuit = MstInclusionCircuit::<LEVELS, N_ASSETS, N_BYTES>::init_empty();

let (params, pk, vk) = generate_setup_artifacts(13, None, empty_circuit).unwrap();

Expand All @@ -115,10 +116,10 @@ fn verify_zk_proof_mst_inclusion_circuit(_c: &mut Criterion) {
PATH_NAME, PATH_NAME, LEVELS
);

let merkle_sum_tree = MerkleSumTree::<N_ASSETS>::new(&csv_file).unwrap();
let merkle_sum_tree = MerkleSumTree::<N_ASSETS, N_BYTES>::new(&csv_file).unwrap();

// Only now we can instantiate the circuit with the actual inputs
let circuit = MstInclusionCircuit::<LEVELS, N_ASSETS>::init(merkle_sum_tree, 0);
let circuit = MstInclusionCircuit::<LEVELS, N_ASSETS, N_BYTES>::init(merkle_sum_tree, 0);

let proof = full_prover(&params, &pk, circuit.clone(), circuit.instances());

Expand All @@ -138,7 +139,7 @@ fn verify_zk_proof_mst_inclusion_circuit(_c: &mut Criterion) {
fn verification_key_gen_solvency_circuit(_c: &mut Criterion) {
let mut criterion = Criterion::default().sample_size(SAMPLE_SIZE);

let empty_circuit = SolvencyCircuit::<N_ASSETS>::init_empty();
let empty_circuit = SolvencyCircuit::<N_ASSETS, N_BYTES>::init_empty();

let (params, _, _) = generate_setup_artifacts(11, None, empty_circuit.clone()).unwrap();

Expand All @@ -156,7 +157,7 @@ fn verification_key_gen_solvency_circuit(_c: &mut Criterion) {
fn proving_key_gen_solvency_circuit(_c: &mut Criterion) {
let mut criterion = Criterion::default().sample_size(SAMPLE_SIZE);

let empty_circuit = SolvencyCircuit::<N_ASSETS>::init_empty();
let empty_circuit = SolvencyCircuit::<N_ASSETS, N_BYTES>::init_empty();

let (params, _, vk) = generate_setup_artifacts(11, None, empty_circuit.clone()).unwrap();

Expand All @@ -174,7 +175,7 @@ fn proving_key_gen_solvency_circuit(_c: &mut Criterion) {
fn generate_zk_proof_solvency_circuit(_c: &mut Criterion) {
let mut criterion = Criterion::default().sample_size(SAMPLE_SIZE);

let empty_circuit = SolvencyCircuit::<N_ASSETS>::init_empty();
let empty_circuit = SolvencyCircuit::<N_ASSETS, N_BYTES>::init_empty();

let (params, pk, vk) = generate_setup_artifacts(11, None, empty_circuit).unwrap();

Expand All @@ -183,12 +184,12 @@ fn generate_zk_proof_solvency_circuit(_c: &mut Criterion) {
PATH_NAME, PATH_NAME, LEVELS
);

let merkle_sum_tree = MerkleSumTree::<N_ASSETS>::new(&csv_file).unwrap();
let merkle_sum_tree = MerkleSumTree::<N_ASSETS, N_BYTES>::new(&csv_file).unwrap();

let asset_sums = merkle_sum_tree.root().balances.map(|x| x + Fp::from(1));

// Only now we can instantiate the circuit with the actual inputs
let circuit = SolvencyCircuit::<N_ASSETS>::init(merkle_sum_tree, asset_sums);
let circuit = SolvencyCircuit::<N_ASSETS, N_BYTES>::init(merkle_sum_tree, asset_sums);

let bench_name = format!(
"generate zk proof - tree of 2 power of {} entries with {} assets solvency circuit",
Expand All @@ -204,7 +205,7 @@ fn generate_zk_proof_solvency_circuit(_c: &mut Criterion) {
fn verify_zk_proof_solvency_circuit(_c: &mut Criterion) {
let mut criterion = Criterion::default().sample_size(SAMPLE_SIZE);

let empty_circuit = SolvencyCircuit::<N_ASSETS>::init_empty();
let empty_circuit = SolvencyCircuit::<N_ASSETS, N_BYTES>::init_empty();

let (params, pk, vk) = generate_setup_artifacts(11, None, empty_circuit).unwrap();

Expand All @@ -213,12 +214,12 @@ fn verify_zk_proof_solvency_circuit(_c: &mut Criterion) {
PATH_NAME, PATH_NAME, LEVELS
);

let merkle_sum_tree = MerkleSumTree::<N_ASSETS>::new(&csv_file).unwrap();
let merkle_sum_tree = MerkleSumTree::<N_ASSETS, N_BYTES>::new(&csv_file).unwrap();

let asset_sums = merkle_sum_tree.root().balances.map(|x| x + Fp::from(1));

// Only now we can instantiate the circuit with the actual inputs
let circuit = SolvencyCircuit::<N_ASSETS>::init(merkle_sum_tree, asset_sums);
let circuit = SolvencyCircuit::<N_ASSETS, N_BYTES>::init(merkle_sum_tree, asset_sums);

let proof = full_prover(&params, &pk, circuit.clone(), circuit.instances());

Expand Down
Binary file modified zk_prover/prints/mst-inclusion-layout.png
View file
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Binary file added zk_prover/prints/range-check-layout.png
View file
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
2 changes: 1 addition & 1 deletion zk_prover/src/chips/mod.rs
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
pub mod less_than;
pub mod merkle_sum_tree;
pub mod overflow;
pub mod poseidon;
pub mod range;
3 changes: 0 additions & 3 deletions zk_prover/src/chips/overflow/mod.rs
View file

This file was deleted.

Loading

0 comments on commit 56f28ee

Please sign in to comment.