Add documentation for all debug_asserts (#40)

feat: add documentation for all debug_asserts

halo2-base/src/gates/flex_gate.rs

@@ -1100,7 +1100,7 @@ impl<F: ScalarField> GateInstructions<F> for GateChip<F> {
     ///
     /// Assumes `range_bits >= number of bits in a`.
     /// * `a`: [QuantumCell] of the value to convert
-    /// * `range_bits`: range of bits needed to represent `a`
+    /// * `range_bits`: range of bits needed to represent `a`. Assumes `range_bits > 0`.
     fn num_to_bits(
         &self,
         ctx: &mut Context<F>,

halo2-base/src/gates/range.rs

@@ -441,8 +441,8 @@ pub struct RangeChip<F: ScalarField> {
     pub gate: GateChip<F>,
     /// Defines the number of bits represented in the lookup table [0,2<sup>lookup_bits</sup>).
     pub lookup_bits: usize,
-    /// [Vec] of 'limbs' represented as [QuantumCell] that divide the underlying scalar field element into sections smaller than lookup_bits.
-    /// * This allows range checks on field elements that are larger than the maximum value of the lookup table.
+    /// [Vec] of powers of `2 ** lookup_bits` represented as [QuantumCell::Constant].
+    /// These are precomputed and cached as a performance optimization for later limb decompositions. We precompute up to the higher power that fits in `F`, which is `2 ** ((F::CAPACITY / lookup_bits) * lookup_bits)`.
     pub limb_bases: Vec<QuantumCell<F>>,
 }
 
@@ -453,7 +453,7 @@ impl<F: ScalarField> RangeChip<F> {
     pub fn new(strategy: RangeStrategy, lookup_bits: usize) -> Self {
         let limb_base = F::from(1u64 << lookup_bits);
         let mut running_base = limb_base;
-        let num_bases = F::NUM_BITS as usize / lookup_bits;
+        let num_bases = F::CAPACITY as usize / lookup_bits;
         let mut limb_bases = Vec::with_capacity(num_bases + 1);
         limb_bases.extend([Constant(F::one()), Constant(running_base)]);
         for _ in 2..=num_bases {
@@ -494,13 +494,16 @@ impl<F: ScalarField> RangeInstructions<F> for RangeChip<F> {
 
     /// Checks and constrains that `a` lies in the range [0, 2<sup>range_bits</sup>).
     ///
-    /// This is done by decomposing `a` into `k` limbs, where `k = (range_bits + lookup_bits - 1) / lookup_bits`.
+    /// This is done by decomposing `a` into `k` limbs, where `k = ceil(range_bits / lookup_bits)`.
     /// Each limb is constrained to be within the range [0, 2<sup>lookup_bits</sup>).
     /// The limbs are then combined to form `a` again with the last limb having `rem_bits` number of bits.
     ///
     /// * `a`: [AssignedValue] value to be range checked
     /// * `range_bits`: number of bits in the range
     /// * `lookup_bits`: number of bits in the lookup table
+    ///
+    /// # Assumptions
+    /// * `ceil(range_bits / lookup_bits) * lookup_bits <= F::CAPACITY`
     fn range_check(&self, ctx: &mut Context<F>, a: AssignedValue<F>, range_bits: usize) {
         // the number of limbs
         let k = (range_bits + self.lookup_bits - 1) / self.lookup_bits;
@@ -585,10 +588,13 @@ impl<F: ScalarField> RangeInstructions<F> for RangeChip<F> {
 
     /// Constrains whether `a` is in `[0, b)`, and returns 1 if `a` < `b`, otherwise 0.
     ///
-    /// Assumes that`a` and `b` are known to have <= num_bits bits.
     /// * a: first [QuantumCell] to compare
     /// * b: second [QuantumCell] to compare
     /// * num_bits: number of bits to represent the values
+    ///
+    /// # Assumptions
+    /// * `a` and `b` are known to have `<= num_bits` bits.
+    /// * (`ceil(num_bits / lookup_bits) + 1) * lookup_bits <= F::CAPACITY`
     fn is_less_than(
         &self,
         ctx: &mut Context<F>,

halo2-base/src/utils.rs

@@ -184,7 +184,8 @@ pub fn fe_to_biguint<F: ScalarField>(fe: &F) -> BigUint {
 
 /// Converts a [BigPrimeField] element into a [BigInt] element by sending `fe` in `[0, F::modulus())` to
 /// ```
-/// fe < F::modulus() / 2 ? fe : fe - F::modulus()
+/// fe,                 if fe < F::modulus() / 2
+/// fe - F::modulus(),  otherwise
 /// ```
 pub fn fe_to_bigint<F: BigPrimeField>(fe: &F) -> BigInt {
     // TODO: `F` should just have modulus as lazy_static or something

halo2-ecc/src/bigint/add_no_carry.rs

@@ -1,33 +1,35 @@
 use super::{CRTInteger, OverflowInteger};
 use halo2_base::{gates::GateInstructions, utils::ScalarField, Context};
+use itertools::Itertools;
 use std::cmp::max;
 
+/// # Assumptions
+/// * `a, b` have same number of limbs
 pub fn assign<F: ScalarField>(
     gate: &impl GateInstructions<F>,
     ctx: &mut Context<F>,
     a: &OverflowInteger<F>,
     b: &OverflowInteger<F>,
 ) -> OverflowInteger<F> {
-    debug_assert_eq!(a.limbs.len(), b.limbs.len());
-
     let out_limbs = a
         .limbs
         .iter()
-        .zip(b.limbs.iter())
+        .zip_eq(b.limbs.iter())
         .map(|(&a_limb, &b_limb)| gate.add(ctx, a_limb, b_limb))
         .collect();
 
     OverflowInteger::construct(out_limbs, max(a.max_limb_bits, b.max_limb_bits) + 1)
 }
 
+/// # Assumptions
+/// * `a, b` have same number of limbs
 // pass by reference to avoid cloning the BigInt in CRTInteger, unclear if this is optimal
 pub fn crt<F: ScalarField>(
     gate: &impl GateInstructions<F>,
     ctx: &mut Context<F>,
     a: &CRTInteger<F>,
     b: &CRTInteger<F>,
 ) -> CRTInteger<F> {
-    debug_assert_eq!(a.truncation.limbs.len(), b.truncation.limbs.len());
     let out_trunc = assign::<F>(gate, ctx, &a.truncation, &b.truncation);
     let out_native = gate.add(ctx, a.native, b.native);
     let out_val = &a.value + &b.value;

halo2-ecc/src/bigint/big_is_equal.rs

@@ -1,22 +1,25 @@
 use super::{CRTInteger, OverflowInteger};
 use halo2_base::{gates::GateInstructions, utils::ScalarField, AssignedValue, Context};
+use itertools::Itertools;
 
 /// Given OverflowInteger<F>'s `a` and `b` of the same shape,
 /// returns whether `a == b`.
+///
+/// # Assumptions:
+/// * `a, b` have the same number of limbs.
+/// * The number of limbs is nonzero.
 pub fn assign<F: ScalarField>(
     gate: &impl GateInstructions<F>,
     ctx: &mut Context<F>,
     a: &OverflowInteger<F>,
     b: &OverflowInteger<F>,
 ) -> AssignedValue<F> {
-    let k = a.limbs.len();
-    debug_assert_eq!(k, b.limbs.len());
-    debug_assert_ne!(k, 0);
+    debug_assert!(!a.limbs.is_empty());
 
     let mut a_limbs = a.limbs.iter();
     let mut b_limbs = b.limbs.iter();
     let mut partial = gate.is_equal(ctx, *a_limbs.next().unwrap(), *b_limbs.next().unwrap());
-    for (&a_limb, &b_limb) in a_limbs.zip(b_limbs) {
+    for (&a_limb, &b_limb) in a_limbs.zip_eq(b_limbs) {
         let eq_limb = gate.is_equal(ctx, a_limb, b_limb);
         partial = gate.and(ctx, eq_limb, partial);
     }

halo2-ecc/src/bigint/big_is_zero.rs

@@ -1,7 +1,10 @@
 use super::{CRTInteger, OverflowInteger};
 use halo2_base::{gates::GateInstructions, utils::ScalarField, AssignedValue, Context};
 
-/// assume you know that the limbs of `a` are all in [0, 2^{a.max_limb_bits})
+/// # Assumptions
+/// * `a` has nonzero number of limbs
+/// * The limbs of `a` are all in [0, 2<sup>a.max_limb_bits</sup>)
+/// * a.limbs.len() * 2<sup>a.max_limb_bits</sup> ` is less than modulus of `F`
 pub fn positive<F: ScalarField>(
     gate: &impl GateInstructions<F>,
     ctx: &mut Context<F>,
@@ -15,14 +18,16 @@ pub fn positive<F: ScalarField>(
     gate.is_zero(ctx, sum)
 }
 
-// given OverflowInteger<F> `a`, returns whether `a == 0`
+/// Given OverflowInteger<F> `a`, returns whether `a == 0`
+///
+/// # Assumptions
+/// * `a` has nonzero number of limbs
 pub fn assign<F: ScalarField>(
     gate: &impl GateInstructions<F>,
     ctx: &mut Context<F>,
     a: &OverflowInteger<F>,
 ) -> AssignedValue<F> {
-    let k = a.limbs.len();
-    debug_assert_ne!(k, 0);
+    debug_assert!(!a.limbs.is_empty());
 
     let mut a_limbs = a.limbs.iter();
     let mut partial = gate.is_zero(ctx, *a_limbs.next().unwrap());

halo2-ecc/src/bigint/carry_mod.rs

@@ -18,7 +18,10 @@ use std::{cmp::max, iter};
 // `out.native = (a (mod modulus)) % (native_modulus::<F>)`
 // We constrain `a = out + modulus * quotient` and range check `out` and `quotient`
 //
-// Assumption: the leading two bits (in big endian) are 1, and `abs(a) <= 2^{n * k - 1 + F::NUM_BITS - 2}` (A weaker assumption is also enough, but this is good enough for forseeable use cases)
+// Assumption: the leading two bits (in big endian) are 1,
+/// # Assumptions
+/// * abs(a) <= 2<sup>n * k - 1 + F::NUM_BITS - 2</sup> (A weaker assumption is also enough, but this is good enough for forseeable use cases)
+/// * `native_modulus::<F>` requires *exactly* `k = a.limbs.len()` limbs to represent
 
 // This is currently optimized for limbs greater than 64 bits, so we need `F` to be a `BigPrimeField`
 // In the future we'll need a slightly different implementation for limbs that fit in 32 or 64 bits (e.g., `F` is Goldilocks)

halo2-ecc/src/bigint/check_carry_mod_to_zero.rs

@@ -43,7 +43,7 @@ pub fn crt<F: BigPrimeField>(
     // we need to constrain that `sum_i quot_vec[i] * 2^{n*i} = quot_native` in `F`
     let (quot_val, _out_val) = a.value.div_mod_floor(modulus);
 
-    // only perform safety checks in display mode so we can turn them off in production
+    // only perform safety checks in debug mode
     debug_assert_eq!(_out_val, BigInt::zero());
     debug_assert!(quot_val.abs() < (BigInt::one() << quot_max_bits));
 

halo2-ecc/src/bigint/mul_no_carry.rs

@@ -1,6 +1,11 @@
 use super::{CRTInteger, OverflowInteger};
 use halo2_base::{gates::GateInstructions, utils::ScalarField, Context, QuantumCell::Existing};
 
+/// # Assumptions
+/// * `a` and `b` have the same number of limbs `k`
+/// * `k` is nonzero
+/// * `num_limbs_log2_ceil = log2_ceil(k)`
+/// * `log2_ceil(k) + a.max_limb_bits + b.max_limb_bits <= F::NUM_BITS as usize - 2`
 pub fn truncate<F: ScalarField>(
     gate: &impl GateInstructions<F>,
     ctx: &mut Context<F>,

halo2-ecc/src/bigint/scalar_mul_and_add_no_carry.rs

@@ -5,9 +5,15 @@ use halo2_base::{
     Context,
     QuantumCell::Constant,
 };
+use itertools::Itertools;
 use std::cmp::max;
 
 /// compute a * c + b = b + a * c
+///
+/// # Assumptions
+/// * `a, b` have same number of limbs
+/// * Number of limbs is nonzero
+/// * `c_log2_ceil = log2_ceil(c)` where `c` is the BigUint value of `c_f`
 // this is uniquely suited for our simple gate
 pub fn assign<F: ScalarField>(
     gate: &impl GateInstructions<F>,
@@ -17,12 +23,10 @@ pub fn assign<F: ScalarField>(
     c_f: F,
     c_log2_ceil: usize,
 ) -> OverflowInteger<F> {
-    debug_assert_eq!(a.limbs.len(), b.limbs.len());
-
     let out_limbs = a
         .limbs
         .iter()
-        .zip(b.limbs.iter())
+        .zip_eq(b.limbs.iter())
         .map(|(&a_limb, &b_limb)| gate.mul_add(ctx, a_limb, Constant(c_f), b_limb))
         .collect();
 

halo2-ecc/src/bigint/select.rs

@@ -1,19 +1,22 @@
 use super::{CRTInteger, OverflowInteger};
 use halo2_base::{gates::GateInstructions, utils::ScalarField, AssignedValue, Context};
+use itertools::Itertools;
 use std::cmp::max;
 
+/// # Assumptions
+/// * `a, b` have same number of limbs
+/// * Number of limbs is nonzero
 pub fn assign<F: ScalarField>(
     gate: &impl GateInstructions<F>,
     ctx: &mut Context<F>,
     a: OverflowInteger<F>,
     b: OverflowInteger<F>,
     sel: AssignedValue<F>,
 ) -> OverflowInteger<F> {
-    debug_assert_eq!(a.limbs.len(), b.limbs.len());
     let out_limbs = a
         .limbs
         .into_iter()
-        .zip(b.limbs.into_iter())
+        .zip_eq(b.limbs)
         .map(|(a_limb, b_limb)| gate.select(ctx, a_limb, b_limb, sel))
         .collect();
 

halo2-ecc/src/bigint/sub.rs

@@ -5,8 +5,11 @@ use halo2_base::{
     AssignedValue, Context,
     QuantumCell::{Constant, Existing, Witness},
 };
+use itertools::Itertools;
 
-/// Should only be called on integers a, b in proper representation with all limbs having at most `limb_bits` number of bits
+/// # Assumptions
+/// * Should only be called on integers a, b in proper representation with all limbs having at most `limb_bits` number of bits
+/// * `a, b` have same nonzero number of limbs
 pub fn assign<F: ScalarField>(
     range: &impl RangeInstructions<F>,
     ctx: &mut Context<F>,
@@ -17,12 +20,11 @@ pub fn assign<F: ScalarField>(
 ) -> (OverflowInteger<F>, AssignedValue<F>) {
     debug_assert!(a.max_limb_bits <= limb_bits);
     debug_assert!(b.max_limb_bits <= limb_bits);
-    debug_assert_eq!(a.limbs.len(), b.limbs.len());
     let k = a.limbs.len();
     let mut out_limbs = Vec::with_capacity(k);
 
     let mut borrow: Option<AssignedValue<F>> = None;
-    for (&a_limb, &b_limb) in a.limbs.iter().zip(b.limbs.iter()) {
+    for (&a_limb, &b_limb) in a.limbs.iter().zip_eq(b.limbs.iter()) {
         let (bottom, lt) = match borrow {
             None => {
                 let lt = range.is_less_than(ctx, a_limb, b_limb, limb_bits);

halo2-ecc/src/bigint/sub_no_carry.rs

@@ -1,18 +1,20 @@
 use super::{CRTInteger, OverflowInteger};
 use halo2_base::{gates::GateInstructions, utils::ScalarField, Context};
+use itertools::Itertools;
 use std::cmp::max;
 
+/// # Assumptions
+/// * `a, b` have same number of limbs
 pub fn assign<F: ScalarField>(
     gate: &impl GateInstructions<F>,
     ctx: &mut Context<F>,
     a: &OverflowInteger<F>,
     b: &OverflowInteger<F>,
 ) -> OverflowInteger<F> {
-    debug_assert_eq!(a.limbs.len(), b.limbs.len());
     let out_limbs = a
         .limbs
         .iter()
-        .zip(b.limbs.iter())
+        .zip_eq(b.limbs.iter())
         .map(|(&a_limb, &b_limb)| gate.sub(ctx, a_limb, b_limb))
         .collect();
 

halo2-ecc/src/ecc/fixed_base.rs

@@ -50,7 +50,7 @@ where
 }
 
 // computes `[scalar] * P` on y^2 = x^3 + b where `P` is fixed (constant)
-// - `scalar` is represented as a reference array of `AssignedCell`s
+// - `scalar` is represented as a non-empty reference array of `AssignedValue`s
 // - `scalar = sum_i scalar_i * 2^{max_bits * i}`
 // - an array of length > 1 is needed when `scalar` exceeds the modulus of scalar field `F`
 // assumes:
@@ -261,6 +261,9 @@ where
     chip.sum::<C>(ctx, sm.iter())
 }
 
+/// # Assumptions
+/// * `points.len() = scalars.len()`
+/// * `scalars[i].len() = scalars[j].len()` for all `i,j`
 pub fn msm_par<F, FC, C>(
     chip: &EccChip<F, FC>,
     builder: &mut GateThreadBuilder<F>,

halo2-ecc/src/ecc/pippenger.rs

@@ -143,7 +143,11 @@ where
     (acc, rand_point)
 }
 
-/// Currently does not support if the final answer is actually the point at infinity
+/// Currently does not support if the final answer is actually the point at infinity (meaning constraints will fail in that case)
+///
+/// # Assumptions
+/// * `points.len() == scalars.len()`
+/// * `scalars[i].len() == scalars[j].len()` for all `i, j`
 pub fn multi_exp<F: PrimeField, FC, C>(
     chip: &FC,
     ctx: &mut Context<F>,
@@ -202,7 +206,11 @@ where
 /// Multi-thread witness generation for multi-scalar multiplication.
 /// Should give exact same circuit as `multi_exp`.
 ///
-/// Currently does not support if the final answer is actually the point at infinity
+/// Currently does not support if the final answer is actually the point at infinity (meaning constraints will fail in that case)
+///
+/// # Assumptions
+/// * `points.len() == scalars.len()`
+/// * `scalars[i].len() == scalars[j].len()` for all `i, j`
 pub fn multi_exp_par<F: PrimeField, FC, C>(
     chip: &FC,
     // these are the "threads" within a single Phase

halo2-ecc/src/fields/fp.rs

@@ -290,6 +290,8 @@ impl<'range, F: PrimeField, Fp: PrimeField> FieldChip<F> for FpChip<'range, F, F
         )
     }
 
+    /// # Assumptions
+    /// * `max_bits` in `(n * (k - 1), n * k]`
     fn range_check(
         &self,
         ctx: &mut Context<F>,
@@ -301,7 +303,6 @@ impl<'range, F: PrimeField, Fp: PrimeField> FieldChip<F> for FpChip<'range, F, F
         debug_assert!(max_bits > n * (k - 1) && max_bits <= n * k);
         let last_limb_bits = max_bits - n * (k - 1);
 
-        #[cfg(debug_assertions)]
         debug_assert!(a.value.bits() as usize <= max_bits);
 
         // range check limbs of `a` are in [0, 2^n) except last limb should be in [0, 2^last_limb_bits)

hashes/zkevm-keccak/src/util/constraint_builder.rs

@@ -53,7 +53,7 @@ impl<F: FieldExt> BaseConstraintBuilder<F> {
 
     pub(crate) fn validate_degree(&self, degree: usize, name: &'static str) {
         if self.max_degree > 0 {
-            debug_assert!(
+            assert!(
                 degree <= self.max_degree,
                 "Expression {} degree too high: {} > {}",
                 name,