Skip to content

Commit

Permalink
refactor: use instance value for checking 0 instead of 'constrain_con…
Browse files Browse the repository at this point in the history 
…stan' method
  • Loading branch information
@sifnoc
sifnoc committed Mar 13, 2024
1 parent 88e797e commit 5c2bf13
Show file tree
Hide file tree
Showing 4 changed files with 101 additions and 31 deletions.
25 changes: 20 additions & 5 deletions kzg_prover/src/chips/range/range_check.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ use crate::chips::range::utils::decompose_fp_to_byte_pairs;
use halo2_proofs::arithmetic::Field;
use halo2_proofs::circuit::{AssignedCell, Region, Value};
use halo2_proofs::halo2curves::bn256::Fr as Fp;
use halo2_proofs::plonk::{Advice, Column, ConstraintSystem, Error, Expression, Fixed};
use halo2_proofs::plonk::{Advice, Column, ConstraintSystem, Error, Expression, Fixed, Instance};
use halo2_proofs::poly::Rotation;
use std::fmt::Debug;

Expand All @@ -12,6 +12,8 @@ use std::fmt::Debug;
/// # Fields
///
/// * `zs`: Four advice columns - contain the truncated right-shifted values of the element to be checked
/// * `z0`: An advice column - for storing the zero value from the instance column
/// * `instance`: An instance column - zero value provided to the circuit
///
/// # Assumptions
///
Expand All @@ -21,6 +23,8 @@ use std::fmt::Debug;
#[derive(Debug, Copy, Clone)]
pub struct RangeCheckU64Config {
zs: [Column<Advice>; 4],
z0: Column<Advice>,
instance: Column<Instance>,
}

/// Helper chip that verfiies that the element witnessed in a given cell lies within the u64 range.
Expand All @@ -36,7 +40,7 @@ pub struct RangeCheckU64Config {
///
/// z | zs[0] | zs[1] | zs[2] | zs[3] |
/// --------- | ---------- | ---------- | ---------- | ---------- |
/// 0x1f2f3f4f5f6f7f8f | 0x1f2f3f4f5f6f | 0x1f2f3f4f | 0x1f2f | 0x00 |
/// 0x1f2f3f4f5f6f7f8f | 0x1f2f3f4f5f6f | 0x1f2f3f4f | 0x1f2f | 0x00 |
///
/// Column zs[0], at offset 0, contains the truncated right-shifted value z - ks[0] / 2^16 (shift right by 16 bits) where ks[0] is the 0-th decomposition big-endian of the element to be checked
/// Column zs[1], at offset 0, contains the truncated right-shifted value zs[0] - ks[1] / 2^16 (shift right by 16 bits) where ks[1] is the 1-th decomposition big-endian of the element to be checked
Expand All @@ -52,7 +56,7 @@ pub struct RangeCheckU64Config {
/// zs[i] - 2^16⋅zs[i+1] = ks[i] ∈ range_u16
///
/// 3.
/// zs[3] == 0
/// zs[3] == z0
#[derive(Debug, Clone)]
pub struct RangeCheckU64Chip {
config: RangeCheckU64Config,
Expand All @@ -69,6 +73,8 @@ impl RangeCheckU64Chip {
meta: &mut ConstraintSystem<Fp>,
z: Column<Advice>,
zs: [Column<Advice>; 4],
z0: Column<Advice>,
instance: Column<Instance>,
range_u16: Column<Fixed>,
) -> RangeCheckU64Config {
// Constraint that the difference between the element to be checked and the 0-th truncated right-shifted value of the element to be within the range.
Expand Down Expand Up @@ -106,7 +112,7 @@ impl RangeCheckU64Chip {
);
}

RangeCheckU64Config { zs }
RangeCheckU64Config { zs, z0, instance }
}

/// Assign the truncated right-shifted values of the element to be checked to the corresponding columns zs at offset 0 starting from the element to be checked.
Expand Down Expand Up @@ -146,8 +152,17 @@ impl RangeCheckU64Chip {
zs.push(z.clone());
}

// Assign zero to z0 from the instance
let z0 = region.assign_advice_from_instance(
|| "assign zero to z0",
self.config.instance,
0,
self.config.z0,
0,
)?;

// Constrain the final running sum output to be zero.
region.constrain_constant(zs[3].cell(), Fp::from(0))?;
region.constrain_equal(zs[3].cell(), z0.cell())?;

Ok(())
}
Expand Down
21 changes: 15 additions & 6 deletions kzg_prover/src/chips/range/tests.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -130,7 +130,13 @@ impl Circuit<Fp> for TestCircuit {

let add_selector = meta.selector();

let range_check_config = RangeCheckU64Chip::configure(meta, c, zs, range_u16);
let instance = meta.instance_column();
meta.enable_equality(instance);

let z0 = meta.advice_column();
meta.enable_equality(z0);

let range_check_config = RangeCheckU64Chip::configure(meta, c, zs, z0, instance, range_u16);

let addchip_config = AddChip::configure(meta, a, b, c, add_selector);

Expand Down Expand Up @@ -213,7 +219,7 @@ mod testing {
let b = Fp::from(1);

let circuit = TestCircuit { a, b };
let prover = MockProver::run(k, &circuit, vec![]).unwrap();
let prover = MockProver::run(k, &circuit, vec![vec![Fp::zero()]]).unwrap();
prover.assert_satisfied();
}

Expand All @@ -231,16 +237,19 @@ mod testing {
let b = Fp::from(2);

let circuit = TestCircuit { a, b };
let invalid_prover = MockProver::run(k, &circuit, vec![]).unwrap();
let invalid_prover = MockProver::run(k, &circuit, vec![vec![Fp::zero()]]).unwrap();
assert_eq!(
invalid_prover.verify(),
Err(vec![
VerifyFailure::Permutation {
column: (Any::Fixed, 1).into(),
location: FailureLocation::OutsideRegion { row: 0 }
column: (Any::advice(), 6).into(),
location: FailureLocation::InRegion {
region: (2, "Perform range check on c").into(),
offset: 0
}
},
VerifyFailure::Permutation {
column: (Any::advice(), 6).into(),
column: (Any::advice(), 7).into(),
location: FailureLocation::InRegion {
region: (2, "Perform range check on c").into(),
offset: 0
Expand Down
74 changes: 58 additions & 16 deletions kzg_prover/src/circuits/tests.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,8 @@ mod test {
let (entries, circuit, pk, _, params) =
set_up::<9, N_USERS, N_CURRENCIES, NoRangeCheckConfig<N_CURRENCIES, N_USERS>>(path);

let (_, advice_polys, omega) = full_prover(&params, &pk, circuit.clone(), &[vec![]]);
let (_, advice_polys, omega) =
full_prover(&params, &pk, circuit.clone(), &[vec![Fp::zero()]]);

// Select the first user balance polynomial for the example
let f_poly = advice_polys.advice_polys.get(1).unwrap();
Expand Down Expand Up @@ -138,11 +139,31 @@ mod test {
UnivariateGrandSumConfig<N_CURRENCIES, N_USERS>,
>::init(entries.to_vec());

let valid_prover = MockProver::run(K, &circuit, vec![vec![]]).unwrap();
let valid_prover = MockProver::run(K, &circuit, vec![vec![Fp::zero()]]).unwrap();

assert_eq!(valid_prover.verify_par(), Ok(()))
}

#[test]
fn test_invalid_instance_value_univariate_grand_sum_prover() {
let path = "../csv/entry_16.csv";

let mut entries: Vec<Entry<N_CURRENCIES>> = vec![Entry::init_empty(); N_USERS];
let mut cryptos = vec![Cryptocurrency::init_empty(); N_CURRENCIES];
parse_csv_to_entries::<&str, N_CURRENCIES>(path, &mut entries, &mut cryptos).unwrap();

let circuit = UnivariateGrandSum::<
N_USERS,
N_CURRENCIES,
UnivariateGrandSumConfig<N_CURRENCIES, N_USERS>,
>::init(entries.to_vec());

let valid_prover = MockProver::run(K, &circuit, vec![vec![Fp::one()]]).unwrap();

let invalid_result = valid_prover.verify_par().unwrap_err()[0].to_string();
assert!(invalid_result.contains("Equality constraint not satisfied"));
}

#[test]
fn test_valid_univariate_grand_sum_full_prover() {
let path = "../csv/entry_16.csv";
Expand All @@ -165,7 +186,7 @@ mod test {
// The Custodian generates the ZK-SNARK Halo2 proof that commits to the user entry values in advice polynomials
// and also range-checks the user balance values
let (zk_snark_proof, advice_polys, omega) =
full_prover(&params, &pk, circuit.clone(), &[vec![]]);
full_prover(&params, &pk, circuit.clone(), &[vec![Fp::zero()]]);

// Both the Custodian and the Verifier know what column range are the balance columns
// (The first column is the user IDs)
Expand Down Expand Up @@ -211,7 +232,12 @@ mod test {

// 2. Verification phase
// The Verifier verifies the ZK proof
assert!(full_verifier(&params, &vk, &zk_snark_proof, &[vec![]]));
assert!(full_verifier(
&params,
&vk,
&zk_snark_proof,
&[vec![Fp::zero()]]
));

// The Verifier is able to independently extract the omega from the verification key
let omega = pk.get_vk().get_domain().get_omega();
Expand Down Expand Up @@ -278,7 +304,7 @@ mod test {
// 1. Proving phase
// The Custodian generates the ZK proof
let (zk_snark_proof, advice_polys, omega) =
full_prover(&params, &pk, circuit.clone(), &[vec![]]);
full_prover(&params, &pk, circuit.clone(), &[vec![Fp::zero()]]);

// The Custodian creates a KZG batch proof of the 4th user ID & balances inclusion
let user_index = 3_u16;
Expand All @@ -303,7 +329,12 @@ mod test {

// 2. Verification phase
// The Verifier verifies the ZK proof
assert!(full_verifier(&params, &vk, &zk_snark_proof, &[vec![]]));
assert!(full_verifier(
&params,
&vk,
&zk_snark_proof,
&[vec![Fp::zero()]]
));

// The Verifier is able to independently extract the omega from the verification key
let omega = pk.get_vk().get_domain().get_omega();
Expand Down Expand Up @@ -349,7 +380,7 @@ mod test {
// The Custodian generates the ZK-SNARK Halo2 proof that commits to the user entry values in advice polynomials
// and also range-checks the user balance values
let (zk_snark_proof, advice_polys, _) =
full_prover(&params, &pk, circuit.clone(), &[vec![]]);
full_prover(&params, &pk, circuit.clone(), &[vec![Fp::zero()]]);

// Both the Custodian and the Verifier know what column range are the balance columns
// (The first column is the user IDs)
Expand All @@ -373,7 +404,12 @@ mod test {

// 2. Verification phase
// The Verifier verifies the ZK proof
assert!(full_verifier(&params, &vk, &zk_snark_proof, &[vec![]]));
assert!(full_verifier(
&params,
&vk,
&zk_snark_proof,
&[vec![Fp::zero()]]
));

// The Custodian communicates the (invalid) polynomial length to the Verifier
let invalid_poly_length = 2 ^ u64::from(K) - 1;
Expand Down Expand Up @@ -413,28 +449,34 @@ mod test {
UnivariateGrandSumConfig<N_CURRENCIES, N_USERS>,
>::init(entries.to_vec());

let invalid_prover = MockProver::run(K, &circuit, vec![vec![]]).unwrap();
let invalid_prover = MockProver::run(K, &circuit, vec![vec![Fp::zero()]]).unwrap();

assert_eq!(
invalid_prover.verify(),
Err(vec![
VerifyFailure::Permutation {
column: (Any::Fixed, 0).into(),
location: FailureLocation::OutsideRegion { row: 65536 }
column: (Any::advice(), 6).into(),
location: FailureLocation::InRegion {
region: (2, "Perform range check on balance 0 of user 0").into(),
offset: 0
}
},
VerifyFailure::Permutation {
column: (Any::Fixed, 0).into(),
location: FailureLocation::OutsideRegion { row: 65539 }
column: (Any::advice(), 7).into(),
location: FailureLocation::InRegion {
region: (2, "Perform range check on balance 0 of user 0").into(),
offset: 0
}
},
VerifyFailure::Permutation {
column: (Any::advice(), 6).into(),
column: (Any::advice(), 11).into(),
location: FailureLocation::InRegion {
region: (2, "Perform range check on balance 0 of user 0").into(),
region: (5, "Perform range check on balance 1 of user 1").into(),
offset: 0
}
},
VerifyFailure::Permutation {
column: (Any::advice(), 10).into(),
column: (Any::advice(), 12).into(),
location: FailureLocation::InRegion {
region: (5, "Perform range check on balance 1 of user 1").into(),
offset: 0
Expand Down
12 changes: 8 additions & 4 deletions kzg_prover/src/circuits/univariate_grand_sum.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -84,6 +84,9 @@ where
// Create an empty array of range check configs
let mut range_check_configs = Vec::with_capacity(N_CURRENCIES);

let instance = meta.instance_column();
meta.enable_equality(instance);

for item in balances.iter().take(N_CURRENCIES) {
let z = *item;
// Create 4 advice columns for each range check chip
Expand All @@ -93,14 +96,15 @@ where
meta.enable_equality(*column);
}

let range_check_config = RangeCheckU64Chip::configure(meta, z, zs, range_u16);
let z0 = meta.advice_column();
meta.enable_equality(z0);

let range_check_config =
RangeCheckU64Chip::configure(meta, z, zs, z0, instance, range_u16);

range_check_configs.push(range_check_config);
}

let instance = meta.instance_column();
meta.enable_equality(instance);

Self {
username,
balances,
Expand Down

0 comments on commit 5c2bf13

Please sign in to comment.