diff --git a/noir-examples/noir-r1cs-test-programs/range-check-mixed-bases/Nargo.toml b/noir-examples/noir-r1cs-test-programs/range-check-mixed-bases/Nargo.toml new file mode 100644 index 000000000..92c044bfe --- /dev/null +++ b/noir-examples/noir-r1cs-test-programs/range-check-mixed-bases/Nargo.toml @@ -0,0 +1,6 @@ +[package] +name = "main" +type = "bin" +authors = [""] + +[dependencies] diff --git a/noir-examples/noir-r1cs-test-programs/range-check-mixed-bases/Prover.toml b/noir-examples/noir-r1cs-test-programs/range-check-mixed-bases/Prover.toml new file mode 100644 index 000000000..369ec53c8 --- /dev/null +++ b/noir-examples/noir-r1cs-test-programs/range-check-mixed-bases/Prover.toml @@ -0,0 +1,2 @@ +x = 2 +y = 2410 diff --git a/noir-examples/noir-r1cs-test-programs/range-check-mixed-bases/src/main.nr b/noir-examples/noir-r1cs-test-programs/range-check-mixed-bases/src/main.nr new file mode 100644 index 000000000..aa53eeacc --- /dev/null +++ b/noir-examples/noir-r1cs-test-programs/range-check-mixed-bases/src/main.nr @@ -0,0 +1,3 @@ +fn main(x: Field, y: Field) -> pub u16 { + (x as u16) + (y as u16) +} diff --git a/noir-examples/noir-r1cs-test-programs/range-check-u16/Nargo.toml b/noir-examples/noir-r1cs-test-programs/range-check-u16/Nargo.toml new file mode 100644 index 000000000..92c044bfe --- /dev/null +++ b/noir-examples/noir-r1cs-test-programs/range-check-u16/Nargo.toml @@ -0,0 +1,6 @@ +[package] +name = "main" +type = "bin" +authors = [""] + +[dependencies] diff --git a/noir-examples/noir-r1cs-test-programs/range-check-u16/Prover.toml b/noir-examples/noir-r1cs-test-programs/range-check-u16/Prover.toml new file mode 100644 index 000000000..87cf3b090 --- /dev/null +++ b/noir-examples/noir-r1cs-test-programs/range-check-u16/Prover.toml @@ -0,0 +1 @@ +x = 2222 diff --git a/noir-examples/noir-r1cs-test-programs/range-check-u16/src/main.nr b/noir-examples/noir-r1cs-test-programs/range-check-u16/src/main.nr new file mode 100644 index 000000000..b4f772cab --- /dev/null +++ b/noir-examples/noir-r1cs-test-programs/range-check-u16/src/main.nr @@ -0,0 +1 @@ +fn main(x: u16) { } diff --git a/noir-examples/noir-r1cs-test-programs/range-check-u8/Nargo.toml b/noir-examples/noir-r1cs-test-programs/range-check-u8/Nargo.toml new file mode 100644 index 000000000..92c044bfe --- /dev/null +++ b/noir-examples/noir-r1cs-test-programs/range-check-u8/Nargo.toml @@ -0,0 +1,6 @@ +[package] +name = "main" +type = "bin" +authors = [""] + +[dependencies] diff --git a/noir-examples/noir-r1cs-test-programs/range-check-u8/Prover.toml b/noir-examples/noir-r1cs-test-programs/range-check-u8/Prover.toml new file mode 100644 index 000000000..407de3068 --- /dev/null +++ b/noir-examples/noir-r1cs-test-programs/range-check-u8/Prover.toml @@ -0,0 +1 @@ +x = 2 diff --git a/noir-examples/noir-r1cs-test-programs/range-check-u8/src/main.nr b/noir-examples/noir-r1cs-test-programs/range-check-u8/src/main.nr new file mode 100644 index 000000000..3824f3262 --- /dev/null +++ b/noir-examples/noir-r1cs-test-programs/range-check-u8/src/main.nr @@ -0,0 +1 @@ +fn main(x: u8) { } diff --git a/noir-r1cs-logup/src/digits.rs b/noir-r1cs-logup/src/digits.rs index c2995f3b5..cfff83f1c 100644 --- a/noir-r1cs-logup/src/digits.rs +++ b/noir-r1cs-logup/src/digits.rs @@ -1,26 +1,35 @@ -use acir::{AcirField, FieldElement}; -use crate::{compiler::R1CS, solver::WitnessBuilder}; +use { + crate::{compiler::R1CS, solver::WitnessBuilder}, + acir::{AcirField, FieldElement}, + serde::{Deserialize, Serialize}, +}; -/// Allocates witnesses for the digital decomposition of the given witnesses into its digits in the -/// given bases. A log base is specified for each digit (permitting mixed base decompositions). The -/// order of bases is little-endian. Witnesses are grouped by digital place, in the order of the bases, -/// where each group of witnesses is in 1:1 correspondence with witnesses_to_decompose. -#[derive(Debug, Clone)] +/// Allocates witnesses for the digital decomposition of the given witnesses +/// into its digits in the given bases. A log base is specified for each digit +/// (permitting mixed base decompositions). The order of bases is little-endian. +/// Witnesses are grouped by digital place, in the order of the bases, +/// where each group of witnesses is in 1:1 correspondence with +/// witnesses_to_decompose. +#[derive(Debug, Clone, Serialize, Deserialize, PartialEq)] pub(crate) struct DigitalDecompositionWitnesses { /// The log base of each digit (in little-endian order) - pub log_bases: Vec, + pub log_bases: Vec, /// The number of witnesses to decompose pub num_witnesses_to_decompose: usize, /// Witness indices of the values to be decomposed - pub witnesses_to_decompose: Vec, + pub witnesses_to_decompose: Vec, /// The index of the first witness written to - pub first_witness_idx: usize, + pub first_witness_idx: usize, /// The number of witnesses written to - pub num_witnesses: usize, + pub num_witnesses: usize, } impl DigitalDecompositionWitnesses { - pub fn new(next_witness_idx: usize, log_bases: Vec, witnesses_to_decompose: Vec) -> Self { + pub fn new( + next_witness_idx: usize, + log_bases: Vec, + witnesses_to_decompose: Vec, + ) -> Self { let num_witnesses_to_decompose = witnesses_to_decompose.len(); let digital_decomp_length = log_bases.len(); Self { @@ -32,9 +41,10 @@ impl DigitalDecompositionWitnesses { } } - /// Returns the witness index of the `value_offset`-th witness of the `digit_place`-th digit. - /// Note that `value_offset` is the index of the witness in the original list of witnesses (not - /// itself a witness index). + /// Returns the witness index of the `value_offset`-th witness of the + /// `digit_place`-th digit. Note that `value_offset` is the index of the + /// witness in the original list of witnesses (not itself a witness + /// index). pub fn get_digit_witness_index(&self, digit_place: usize, value_offset: usize) -> usize { debug_assert!(digit_place < self.log_bases.len()); debug_assert!(value_offset < self.num_witnesses_to_decompose); @@ -43,27 +53,41 @@ impl DigitalDecompositionWitnesses { /// Solve for the witness values allocated to the digital decomposition. pub fn solve(&self, witness: &mut [FieldElement]) { - self.witnesses_to_decompose.iter().enumerate().for_each(|(i, value_witness_idx)| { - let value = witness[*value_witness_idx]; - let digits = decompose_into_digits(value, &self.log_bases); - digits.iter().enumerate().for_each(|(digit_place, digit_value)| { - witness[self.first_witness_idx + digit_place * self.witnesses_to_decompose.len() + i] = *digit_value; + self.witnesses_to_decompose + .iter() + .enumerate() + .for_each(|(i, value_witness_idx)| { + let value = witness[*value_witness_idx]; + let digits = decompose_into_digits(value, &self.log_bases); + digits + .iter() + .enumerate() + .for_each(|(digit_place, digit_value)| { + witness[self.first_witness_idx + + digit_place * self.witnesses_to_decompose.len() + + i] = *digit_value; + }); }); - }); } } -/// Adds the witnesses and constraints for the digital decomposition of the given witnesses in a -/// mixed base decomposition (see [DigitalDecompositionWitnesses]). Does NOT add constraints for -/// range checking the digits - this is left to the caller (as sometimes these range checks are -/// obviated e.g. by later lookups, as in the case of the binop codes). +/// Adds the witnesses and constraints for the digital decomposition of the +/// given witnesses in a mixed base decomposition (see +/// [DigitalDecompositionWitnesses]). Does NOT add constraints for +/// range checking the digits - this is left to the caller (as sometimes these +/// range checks are obviated e.g. by later lookups, as in the case of the binop +/// codes). pub(crate) fn add_digital_decomposition( r1cs: &mut R1CS, log_bases: Vec, witnesses_to_decompose: Vec, ) -> DigitalDecompositionWitnesses { let next_witness_idx = r1cs.num_witnesses(); - let dd_struct = DigitalDecompositionWitnesses::new(next_witness_idx, log_bases.clone(), witnesses_to_decompose); + let dd_struct = DigitalDecompositionWitnesses::new( + next_witness_idx, + log_bases.clone(), + witnesses_to_decompose, + ); r1cs.add_witness_builder(WitnessBuilder::DigitalDecomposition(dd_struct.clone())); // Add the constraints for the digital recomposition let mut digit_multipliers = vec![FieldElement::one()]; @@ -71,23 +95,30 @@ pub(crate) fn add_digital_decomposition( let multiplier = *digit_multipliers.last().unwrap() * FieldElement::from(1u64 << *log_base); digit_multipliers.push(multiplier); } - dd_struct.witnesses_to_decompose.iter().enumerate().for_each(|(i, value)| { - let mut recomp_summands = vec![]; - digit_multipliers.iter().enumerate().for_each(|(digit_place, digit_multiplier)| { - let digit_witness = dd_struct.get_digit_witness_index(digit_place, i); - recomp_summands.push((FieldElement::from(*digit_multiplier), digit_witness)); + dd_struct + .witnesses_to_decompose + .iter() + .enumerate() + .for_each(|(i, value)| { + let mut recomp_summands = vec![]; + digit_multipliers + .iter() + .enumerate() + .for_each(|(digit_place, digit_multiplier)| { + let digit_witness = dd_struct.get_digit_witness_index(digit_place, i); + recomp_summands.push((FieldElement::from(*digit_multiplier), digit_witness)); + }); + r1cs.matrices.add_constraint( + &[(FieldElement::one(), r1cs.witness_one())], + &[(FieldElement::one(), *value)], + &recomp_summands, + ); }); - r1cs.matrices.add_constraint( - &[(FieldElement::one(), r1cs.witness_one())], - &[(FieldElement::one(), *value)], - &recomp_summands, - ); - }); dd_struct } -/// Compute a mixed-base decomposition of a field element into its digits, using the given log bases. -/// Decomposition is little-endian. +/// Compute a mixed-base decomposition of a field element into its digits, using +/// the given log bases. Decomposition is little-endian. /// Panics if the value provided can not be represented in the given bases. pub(crate) fn decompose_into_digits( value: FieldElement, @@ -96,7 +127,8 @@ pub(crate) fn decompose_into_digits( let num_digits = log_bases.len(); let mut digits = vec![FieldElement::zero(); num_digits]; let value_bits = field_to_le_bits(value); - // Grab the bits of the element that we need for each digit, and turn them back into field elements. + // Grab the bits of the element that we need for each digit, and turn them back + // into field elements. let mut start_bit = 0; for digit_idx in 0..num_digits { let log_base = log_bases[digit_idx]; @@ -106,7 +138,10 @@ pub(crate) fn decompose_into_digits( start_bit += log_base; } let remaining_bits = &value_bits[start_bit..]; - assert!(remaining_bits.iter().all(|&bit| !bit), "Higher order bits are not zero"); + assert!( + remaining_bits.iter().all(|&bit| !bit), + "Higher order bits are not zero" + ); digits } @@ -120,8 +155,9 @@ pub(crate) fn field_to_le_bits(value: FieldElement) -> Vec { .collect() } -/// Given the binary representation of a field element in little-endian order, convert it to a field -/// element. The input is padded to the next multiple of 8 bits. +/// Given the binary representation of a field element in little-endian order, +/// convert it to a field element. The input is padded to the next multiple of 8 +/// bits. pub(crate) fn le_bits_to_field(bits: &[bool]) -> FieldElement { let next_multiple_of_8 = bits.len().div_ceil(8) * 8; let padding_amt = next_multiple_of_8 - bits.len(); diff --git a/noir-r1cs/src/digits.rs b/noir-r1cs/src/digits.rs new file mode 100644 index 000000000..699150087 --- /dev/null +++ b/noir-r1cs/src/digits.rs @@ -0,0 +1,205 @@ +use { + crate::{noir_to_r1cs::NoirToR1CSCompiler, r1cs_solver::WitnessBuilder, FieldElement}, + ark_ff::{BigInteger, One, PrimeField, Zero}, + serde::{Deserialize, Serialize}, +}; + +/// Allocates witnesses for the digital decomposition of the given witnesses +/// into its digits in the given bases. A log base is specified for each digit +/// (permitting mixed base decompositions). The order of bases is little-endian. +/// Witnesses are grouped by digital place, in the order of the bases, +/// where each group of witnesses is in 1:1 correspondence with +/// witnesses_to_decompose. +#[derive(Debug, Clone, Serialize, Deserialize, PartialEq)] +pub(crate) struct DigitalDecompositionWitnesses { + /// The log base of each digit (in little-endian order) + pub log_bases: Vec, + /// The number of witnesses to decompose + pub num_witnesses_to_decompose: usize, + /// Witness indices of the values to be decomposed + pub witnesses_to_decompose: Vec, + /// The index of the first witness written to + pub first_witness_idx: usize, + /// The number of witnesses written to + pub num_witnesses: usize, +} + +impl DigitalDecompositionWitnesses { + pub fn new( + next_witness_idx: usize, + log_bases: Vec, + witnesses_to_decompose: Vec, + ) -> Self { + let num_witnesses_to_decompose = witnesses_to_decompose.len(); + let digital_decomp_length = log_bases.len(); + Self { + log_bases, + num_witnesses_to_decompose, + witnesses_to_decompose, + first_witness_idx: next_witness_idx, + num_witnesses: digital_decomp_length * num_witnesses_to_decompose, + } + } + + /// Returns the witness index of the `value_offset`-th witness of the + /// `digit_place`-th digit. Note that `value_offset` is the index of the + /// witness in the original list of witnesses (not itself a witness + /// index). + pub fn get_digit_witness_index(&self, digit_place: usize, value_offset: usize) -> usize { + debug_assert!(digit_place < self.log_bases.len()); + debug_assert!(value_offset < self.num_witnesses_to_decompose); + self.first_witness_idx + digit_place * self.num_witnesses_to_decompose + value_offset + } + + /// Solve for the witness values allocated to the digital decomposition. + pub fn solve(&self, witness: &mut [Option]) { + self.witnesses_to_decompose + .iter() + .enumerate() + .for_each(|(i, value_witness_idx)| { + let value = witness[*value_witness_idx].unwrap(); + let digits = decompose_into_digits(value, &self.log_bases); + digits + .iter() + .enumerate() + .for_each(|(digit_place, digit_value)| { + witness[self.first_witness_idx + + digit_place * self.witnesses_to_decompose.len() + + i] = Some(*digit_value); + }); + }); + } +} + +/// Adds the witnesses and constraints for the digital decomposition of the +/// given witnesses in a mixed base decomposition (see +/// [DigitalDecompositionWitnesses]). Does NOT add constraints for +/// range checking the digits - this is left to the caller (as sometimes these +/// range checks are obviated e.g. by later lookups, as in the case of the binop +/// codes). +pub(crate) fn add_digital_decomposition( + r1cs_compiler: &mut NoirToR1CSCompiler, + log_bases: Vec, + witnesses_to_decompose: Vec, +) -> DigitalDecompositionWitnesses { + let next_witness_idx = r1cs_compiler.num_witnesses(); + let dd_struct = DigitalDecompositionWitnesses::new( + next_witness_idx, + log_bases.clone(), + witnesses_to_decompose, + ); + r1cs_compiler.add_witness_builder(WitnessBuilder::DigitalDecomposition(dd_struct.clone())); + // Add the constraints for the digital recomposition + let mut digit_multipliers = vec![FieldElement::one()]; + for log_base in log_bases[..log_bases.len() - 1].iter() { + let multiplier = *digit_multipliers.last().unwrap() * FieldElement::from(1u64 << *log_base); + digit_multipliers.push(multiplier); + } + dd_struct + .witnesses_to_decompose + .iter() + .enumerate() + .for_each(|(i, value)| { + let mut recomp_summands = vec![]; + digit_multipliers + .iter() + .enumerate() + .for_each(|(digit_place, digit_multiplier)| { + let digit_witness = dd_struct.get_digit_witness_index(digit_place, i); + recomp_summands.push((FieldElement::from(*digit_multiplier), digit_witness)); + }); + r1cs_compiler.r1cs.add_constraint( + &[(FieldElement::one(), r1cs_compiler.witness_one())], + &[(FieldElement::one(), *value)], + &recomp_summands, + ); + }); + dd_struct +} + +/// Compute a mixed-base decomposition of a field element into its digits, using +/// the given log bases. Decomposition is little-endian. +/// Panics if the value provided can not be represented in the given bases. +pub(crate) fn decompose_into_digits( + value: FieldElement, + log_bases: &Vec, +) -> Vec { + let num_digits = log_bases.len(); + let mut digits = vec![FieldElement::zero(); num_digits]; + let value_bits = field_to_le_bits(value); + // Grab the bits of the element that we need for each digit, and turn them back + // into field elements. + let mut start_bit = 0; + for digit_idx in 0..num_digits { + let log_base = log_bases[digit_idx]; + let digit_bits = &value_bits[start_bit..start_bit + log_base]; + let digit_value = le_bits_to_field(digit_bits); + digits[digit_idx] = digit_value; + start_bit += log_base; + } + let remaining_bits = &value_bits[start_bit..]; + assert!( + remaining_bits.iter().all(|&bit| !bit), + "Higher order bits are not zero" + ); + digits +} + +/// Decomposes a field element into its bits, in little-endian order. +pub(crate) fn field_to_le_bits(value: FieldElement) -> Vec { + value.into_bigint().to_bits_le() +} + +/// Given the binary representation of a field element in little-endian order, +/// convert it to a field element. The input is padded to the next multiple of 8 +/// bits. +pub(crate) fn le_bits_to_field(bits: &[bool]) -> FieldElement { + let next_multiple_of_8 = bits.len().div_ceil(8) * 8; + let padding_amt = next_multiple_of_8 - bits.len(); + let mut padded_bits_le = vec![false; next_multiple_of_8]; + padded_bits_le[..(next_multiple_of_8 - padding_amt)].copy_from_slice(bits); + let be_byte_vec: Vec = padded_bits_le + .chunks(8) + .map(|chunk_in_bits| { + chunk_in_bits + .iter() + .enumerate() + .fold(0u8, |acc, (i, bit)| acc | ((*bit as u8) << i)) + }) + .rev() + .collect(); + FieldElement::from_be_bytes_mod_order(&be_byte_vec) +} + +#[cfg(test)] +#[test] +fn test_decompose_into_digits() { + let value = FieldElement::from(3 + 2u32 * 256 + 1u32 * 256 * 256); + let log_bases = vec![8, 8, 4]; + let digits = decompose_into_digits(value, &log_bases); + assert_eq!(digits.len(), log_bases.len()); + assert_eq!(digits[0], FieldElement::from(3u32)); + assert_eq!(digits[1], FieldElement::from(2u32)); + assert_eq!(digits[2], FieldElement::from(1u32)); +} + +#[cfg(test)] +#[test] +fn test_field_to_le_bits() { + let value = FieldElement::from(5u32); + let bits = field_to_le_bits(value); + assert_eq!(bits.len(), 256); + assert_eq!(bits[0], true); + assert_eq!(bits[1], false); + assert_eq!(bits[2], true); + assert_eq!(bits[254], false); + assert_eq!(bits[255], false); +} + +#[cfg(test)] +#[test] +fn test_le_bits_to_field() { + let bits = vec![true, false, true, false, false]; + let value = le_bits_to_field(&bits); + assert_eq!(value.into_bigint().0[0], 5); +} diff --git a/noir-r1cs/src/lib.rs b/noir-r1cs/src/lib.rs index 22bedb699..75bd51438 100644 --- a/noir-r1cs/src/lib.rs +++ b/noir-r1cs/src/lib.rs @@ -1,5 +1,6 @@ #![doc = include_str!("../README.md")] #![allow(missing_docs)] +mod digits; mod file; mod gnark_config; mod interner; @@ -9,6 +10,7 @@ mod noir_to_r1cs; mod noir_witness; mod r1cs; mod r1cs_solver; +mod range_check; mod rom; mod skyscraper; mod sparse_matrix; diff --git a/noir-r1cs/src/noir_to_r1cs.rs b/noir-r1cs/src/noir_to_r1cs.rs index e58006462..58045b5ec 100644 --- a/noir-r1cs/src/noir_to_r1cs.rs +++ b/noir-r1cs/src/noir_to_r1cs.rs @@ -2,12 +2,18 @@ use { crate::{ memory::{MemoryBlock, MemoryOperation}, r1cs_solver::{ConstantTerm, SumTerm, WitnessBuilder}, + range_check::add_range_checks, rom::add_rom_checking, utils::noir_to_native, FieldElement, NoirElement, R1CS, }, acir::{ - circuit::{opcodes::BlockType, Circuit, Opcode}, + circuit::{ + opcodes::{ + BlackBoxFuncCall, BlockType, ConstantOrWitnessEnum as ConstantOrACIRWitness, + }, + Circuit, Opcode, + }, native_types::{Expression, Witness as NoirWitness}, }, anyhow::{bail, Result}, @@ -210,6 +216,10 @@ impl NoirToR1CSCompiler { // Read-only memory blocks (used for building the memory lookup constraints at // the end) let mut memory_blocks: BTreeMap = BTreeMap::new(); + // Mapping the log of the range size k to the vector of witness indices that + // are to be constrained within the range [0..2^k]. + // These will be digitally decomposed into smaller ranges, if necessary. + let mut range_checks: BTreeMap> = BTreeMap::new(); for opcode in &circuit.opcodes { match opcode { @@ -294,6 +304,39 @@ impl NoirToR1CSCompiler { block.operations.push(op); } + Opcode::BlackBoxFuncCall(black_box_func_call) => match black_box_func_call { + BlackBoxFuncCall::RANGE { + input: function_input, + } => { + let input = function_input.input(); + let num_bits = function_input.num_bits(); + let input_witness = match input { + ConstantOrACIRWitness::Constant(_) => { + panic!( + "We should never be range-checking a constant value, as this \ + should already be done by the noir-ACIR compiler" + ); + } + ConstantOrACIRWitness::Witness(witness) => { + self.fetch_r1cs_witness_index(witness) + } + }; + println!( + "RANGE CHECK of witness {} to {} bits", + input_witness, num_bits + ); + // Add the entry into the range blocks. + range_checks + .entry(num_bits) + .or_default() + .push(input_witness); + } + + _ => { + unimplemented!("Other black box function: {:?}", black_box_func_call); + } + }, + op => bail!("Unsupported Opcode {op}"), } } @@ -310,6 +353,10 @@ impl NoirToR1CSCompiler { // Not supported yet. } }); + + // Perform all range checks + add_range_checks(self, range_checks); + Ok(()) } } diff --git a/noir-r1cs/src/r1cs_solver.rs b/noir-r1cs/src/r1cs_solver.rs index 6b3f9e36e..66a8bbb40 100644 --- a/noir-r1cs/src/r1cs_solver.rs +++ b/noir-r1cs/src/r1cs_solver.rs @@ -1,5 +1,6 @@ use { crate::{ + digits::DigitalDecompositionWitnesses, utils::{noir_to_native, serde_ark, serde_ark_option}, FieldElement, }, @@ -22,6 +23,13 @@ pub struct ConstantTerm(pub usize, #[serde(with = "serde_ark")] pub FieldElement #[derive(Debug, Clone, PartialEq, Serialize, Deserialize)] pub struct WitnessCoefficient(#[serde(with = "serde_ark")] pub FieldElement, pub usize); +#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)] +pub struct ProductLinearTerm( + pub usize, + #[serde(with = "serde_ark")] pub FieldElement, + #[serde(with = "serde_ark")] pub FieldElement, +); + #[derive(Debug, Clone, PartialEq, Serialize, Deserialize)] /// Indicates how to solve for a collection of R1CS witnesses in terms of /// earlier (i.e. already solved for) R1CS witnesses and/or ACIR witness values. @@ -56,6 +64,16 @@ pub enum WitnessBuilder { /// The inverse of the value at a specified witness index /// (witness index, operand witness index) Inverse(usize, usize), + /// Products with linear operations on the witness indices. + /// Fields are ProductLinearOperation(witness_idx, (index, a, b), (index, c, + /// d)) such that we wish to compute (ax + b) * (cx + d). + ProductLinearOperation(usize, ProductLinearTerm, ProductLinearTerm), + /// For solving for the denominator of a lookup (non-indexed). + /// Field are (witness index, sz_challenge, (value_coeff, value)). + LogUpDenominator(usize, usize, WitnessCoefficient), + /// Builds the witnesses values required for the mixed base digital + /// decomposition of other witness values. + DigitalDecomposition(DigitalDecompositionWitnesses), } impl WitnessBuilder { @@ -64,6 +82,7 @@ impl WitnessBuilder { pub fn num_witnesses(&self) -> usize { match self { WitnessBuilder::MultiplicitiesForRange(_, range_size, _) => *range_size, + WitnessBuilder::DigitalDecomposition(dd_struct) => dd_struct.num_witnesses, _ => 1, } } @@ -79,6 +98,9 @@ impl WitnessBuilder { WitnessBuilder::IndexedLogUpDenominator(start_idx, ..) => *start_idx, WitnessBuilder::Challenge(start_idx) => *start_idx, WitnessBuilder::Inverse(start_idx, _) => *start_idx, + WitnessBuilder::LogUpDenominator(start_idx, ..) => *start_idx, + WitnessBuilder::ProductLinearOperation(start_idx, ..) => *start_idx, + WitnessBuilder::DigitalDecomposition(dd_struct) => dd_struct.first_witness_idx, } } @@ -168,6 +190,26 @@ impl WitnessBuilder { WitnessBuilder::Challenge(witness_idx) => { witness[*witness_idx] = Some(transcript.draw_challenge()); } + WitnessBuilder::LogUpDenominator( + witness_idx, + sz_challenge, + WitnessCoefficient(value_coeff, value), + ) => { + witness[*witness_idx] = Some( + witness[*sz_challenge].unwrap() - (*value_coeff * witness[*value].unwrap()), + ); + } + WitnessBuilder::ProductLinearOperation( + witness_idx, + ProductLinearTerm(x, a, b), + ProductLinearTerm(y, c, d), + ) => { + witness[*witness_idx] = + Some((*a * witness[*x].unwrap() + *b) * (*c * witness[*y].unwrap() + *d)); + } + WitnessBuilder::DigitalDecomposition(dd_struct) => { + dd_struct.solve(witness); + } } } } diff --git a/noir-r1cs/src/range_check.rs b/noir-r1cs/src/range_check.rs new file mode 100644 index 000000000..086599539 --- /dev/null +++ b/noir-r1cs/src/range_check.rs @@ -0,0 +1,240 @@ +use { + crate::{ + digits::add_digital_decomposition, + noir_to_r1cs::NoirToR1CSCompiler, + r1cs_solver::{ProductLinearTerm, SumTerm, WitnessBuilder, WitnessCoefficient}, + FieldElement, + }, + ark_ff::{One, Zero}, + std::{collections::BTreeMap, ops::Neg}, +}; + +const NUM_WITNESS_THRESHOLD_FOR_LOOKUP_TABLE: usize = 5; +pub const NUM_BITS_THRESHOLD_FOR_DIGITAL_DECOMP: u32 = 8; + +/// Add witnesses and constraints that ensure that the values of the witness +/// belong to a range 0..2^k (for some k). If k is larger than +/// `NUM_BITS_THRESHOLD_FOR_DIGITAL_DECOMP`, then a digital decomposition is +/// performed: witnesses are allocated for the digits of the decomposition, a +/// constraint is added that enforces the correctness of the digital +/// decomposition, and then the digits themselves are range checked. +/// `range_checks` is a map from the number of bits k to the vector of witness +/// indices that are to be constrained within the range [0..2^k]. +pub(crate) fn add_range_checks( + r1cs: &mut NoirToR1CSCompiler, + range_checks: BTreeMap>, +) { + // Do a pass through everything that needs to be range checked, + // decomposing each value into digits that are at most + // [NUM_BITS_THRESHOLD_FOR_DIGITAL_DECOMP] and creating a map + // `atomic_range_blocks` of each `num_bits` from 1 to the + // NUM_BITS_THRESHOLD_FOR_DIGITAL_DECOMP (inclusive) to the vec of witness + // indices that are constrained to that range. + + // Mapping the log of the range size k to the vector of witness indices that + // are to be constrained within the range [0..2^k]. + // The witnesses of all small range op codes are added to this map, along with + // witnesses of digits for digital decompositions of larger range checks. + let mut atomic_range_checks: Vec>> = + vec![vec![vec![]]; NUM_BITS_THRESHOLD_FOR_DIGITAL_DECOMP as usize + 1]; + + range_checks + .into_iter() + .for_each(|(num_bits, values_to_lookup)| { + if num_bits > NUM_BITS_THRESHOLD_FOR_DIGITAL_DECOMP { + let num_big_digits = num_bits / NUM_BITS_THRESHOLD_FOR_DIGITAL_DECOMP; + let logbase_of_remainder_digit = num_bits % NUM_BITS_THRESHOLD_FOR_DIGITAL_DECOMP; + let mut log_bases = + vec![NUM_BITS_THRESHOLD_FOR_DIGITAL_DECOMP as usize; num_big_digits as usize]; + if logbase_of_remainder_digit != 0 { + log_bases.push(logbase_of_remainder_digit as usize); + } + let dd_struct = + add_digital_decomposition(r1cs, log_bases.clone(), values_to_lookup.clone()); + + // Add the witness indices for the digits to the atomic range checks + dd_struct + .log_bases + .iter() + .enumerate() + .map(|(digit_place, log_base)| { + ( + *log_base as u32, + (0..dd_struct.num_witnesses_to_decompose) + .map(|i| dd_struct.get_digit_witness_index(digit_place, i)) + .collect::>(), + ) + }) + .for_each(|(log_base, digit_witnesses)| { + atomic_range_checks[log_base as usize].push(digit_witnesses); + }); + } else { + atomic_range_checks[num_bits as usize].push(values_to_lookup); + } + }); + + // For each of the atomic range checks, add the range check constraints. + // Use logup if the range is large; otherwise use a naive range check. + atomic_range_checks + .iter() + .enumerate() + .for_each(|(num_bits, all_values_to_lookup)| { + let values_to_lookup = all_values_to_lookup + .iter() + .flat_map(|v| v.iter()) + .copied() + .collect::>(); + if values_to_lookup.len() > NUM_WITNESS_THRESHOLD_FOR_LOOKUP_TABLE { + add_range_check_via_lookup(r1cs, num_bits as u32, &values_to_lookup); + } else { + values_to_lookup.iter().for_each(|value| { + add_naive_range_check(r1cs, num_bits as u32, *value); + }) + } + }); +} + +/// Helper function which computes all the terms of the summation for +/// each side (LHS and RHS) of the log-derivative multiset check. +/// +/// Checks that both sums (LHS and RHS) are equal at the end. +fn add_range_check_via_lookup( + r1cs_compiler: &mut NoirToR1CSCompiler, + num_bits: u32, + values_to_lookup: &[usize], +) { + // Add witnesses for the multiplicities + let wb = WitnessBuilder::MultiplicitiesForRange( + r1cs_compiler.num_witnesses(), + 1 << num_bits, + values_to_lookup.into(), + ); + let multiplicities_first_witness = r1cs_compiler.add_witness_builder(wb); + // Sample the Schwartz-Zippel challenge for the log derivative + // multiset check. + let sz_challenge = + r1cs_compiler.add_witness_builder(WitnessBuilder::Challenge(r1cs_compiler.num_witnesses())); + + // Compute all the terms in the summation for multiplicity/(X - table_value) + // for each table value. + let table_summands = (0..(1 << num_bits)) + .map(|table_value| { + let table_denom = add_lookup_factor( + r1cs_compiler, + sz_challenge, + FieldElement::from(table_value as u64), + r1cs_compiler.witness_one(), + ); + let multiplicity_witness = multiplicities_first_witness + table_value; + SumTerm( + None, + r1cs_compiler.add_product(table_denom, multiplicity_witness), + ) + }) + .collect(); + let sum_for_table = r1cs_compiler.add_sum(table_summands); + // Compute all the terms in the summation for 1/(X - witness_value) for each + // witness value. + let witness_summands = values_to_lookup + .iter() + .map(|value| { + let witness_idx = + add_lookup_factor(r1cs_compiler, sz_challenge, FieldElement::one(), *value); + SumTerm(None, witness_idx) + }) + .collect(); + let sum_for_witness = r1cs_compiler.add_sum(witness_summands); + // Check that these two sums are equal. + r1cs_compiler.r1cs.add_constraint( + &[ + (FieldElement::one(), sum_for_table), + (FieldElement::one().neg(), sum_for_witness), + ], + &[(FieldElement::one(), r1cs_compiler.witness_one())], + &[(FieldElement::zero(), r1cs_compiler.witness_one())], + ); +} + +/// Helper function that computes the LogUp denominator either for +/// the table values: (X - t_j), or for the witness values: +/// (X - w_i). Computes the inverse and also checks that this is +/// the appropriate inverse. +pub(crate) fn add_lookup_factor( + r1cs_compiler: &mut NoirToR1CSCompiler, + sz_challenge: usize, + value_coeff: FieldElement, + value_witness: usize, +) -> usize { + let denom_wb = WitnessBuilder::LogUpDenominator( + r1cs_compiler.num_witnesses(), + sz_challenge, + WitnessCoefficient(value_coeff, value_witness), + ); + let denominator = r1cs_compiler.add_witness_builder(denom_wb); + r1cs_compiler.r1cs.add_constraint( + &[ + (FieldElement::one(), sz_challenge), + (FieldElement::one().neg() * value_coeff, value_witness), + ], + &[(FieldElement::one(), r1cs_compiler.witness_one())], + &[(FieldElement::one(), denominator)], + ); + let inverse = r1cs_compiler.add_witness_builder(WitnessBuilder::Inverse( + r1cs_compiler.num_witnesses(), + denominator, + )); + r1cs_compiler.r1cs.add_constraint( + &[(FieldElement::one(), denominator)], + &[(FieldElement::one(), inverse)], + &[(FieldElement::one(), r1cs_compiler.witness_one())], + ); + inverse +} + +/// A naive range check helper function, computing the +/// $\prod_{i = 0}^{range}(a - i) = 0$ to check whether a witness found at +/// `index_witness`, which is $a$, is in the $range$, which is `num_bits`. +fn add_naive_range_check( + r1cs_compiler: &mut NoirToR1CSCompiler, + num_bits: u32, + index_witness: usize, +) { + let mut current_product_witness = index_witness; + (1..(1 << num_bits) - 1).for_each(|index: u32| { + let next_product_witness = + r1cs_compiler.add_witness_builder(WitnessBuilder::ProductLinearOperation( + r1cs_compiler.num_witnesses(), + ProductLinearTerm( + current_product_witness, + FieldElement::one(), + FieldElement::zero(), + ), + ProductLinearTerm( + index_witness, + FieldElement::one(), + FieldElement::from(index).neg(), + ), + )); + r1cs_compiler.r1cs.add_constraint( + &[(FieldElement::one(), current_product_witness)], + &[ + (FieldElement::one(), index_witness), + (FieldElement::from(index).neg(), r1cs_compiler.witness_one()), + ], + &[(FieldElement::one(), next_product_witness)], + ); + current_product_witness = next_product_witness; + }); + + r1cs_compiler.r1cs.add_constraint( + &[(FieldElement::one(), current_product_witness)], + &[ + (FieldElement::one(), index_witness), + ( + FieldElement::from((1 << num_bits) - 1 as u32).neg(), + r1cs_compiler.witness_one(), + ), + ], + &[(FieldElement::zero(), r1cs_compiler.witness_one())], + ); +} diff --git a/noir-r1cs/src/test_functions.rs b/noir-r1cs/src/test_functions.rs index 938c63c29..39fc2c37a 100644 --- a/noir-r1cs/src/test_functions.rs +++ b/noir-r1cs/src/test_functions.rs @@ -1,3 +1,4 @@ +use crate::range_check::NUM_BITS_THRESHOLD_FOR_DIGITAL_DECOMP; #[cfg(test)] use { crate::{utils::file_io::deserialize_witness_stack, NoirProofScheme}, @@ -45,3 +46,49 @@ fn test_read_only_memory() { "../noir-examples/noir-r1cs-test-programs/read-only-memory/target/main.gz", ); } + +#[test] +// Test a direct range check (i.e. without a digital decomposition) +fn test_atomic_range_check() { + assert!(8 <= NUM_BITS_THRESHOLD_FOR_DIGITAL_DECOMP); + test_compiler( + "../noir-examples/noir-r1cs-test-programs/range-check-u8/target/main.json", + "../noir-examples/noir-r1cs-test-programs/range-check-u8/target/main.gz", + ); +} + +#[test] +// Test a range check that requires a digital decomposition +fn test_digital_decomposition_u16() { + assert!(16 > NUM_BITS_THRESHOLD_FOR_DIGITAL_DECOMP); + test_compiler( + "../noir-examples/noir-r1cs-test-programs/range-check-u16/target/main.json", + "../noir-examples/noir-r1cs-test-programs/range-check-u16/target/main.gz", + ); +} + +#[test] +// Test a range check that requires a digital decomposition mixed bases +// The program compiles to the following ACIR: +// BrilligCall +// RANGE CHECK of witness 1 to 238 bits +// RANGE CHECK of witness 2 to 16 bits +// BrilligCall +// RANGE CHECK of witness 7 to 17 bits +// .. +// + The 238 bit range check is done using a digital decomposition using 29 +// base-2^8 digits and one +// base-2^6 digit. +// + The 16 bit range check is done using a digital decomposition using 2 +// base-2^8 digits. +// + The 17 bit range check is done using a digital decomposition using 2 +// base-2^8 digits and one +// base-2^1 digit. +// Note that the range check of the base-2^1 digit will be done using a direct +// ("naive") range check. +fn test_mixed_base_range_check() { + test_compiler( + "../noir-examples/noir-r1cs-test-programs/range-check-mixed-bases/target/main.json", + "../noir-examples/noir-r1cs-test-programs/range-check-mixed-bases/target/main.gz", + ); +}