[feat] update docs (#211)

* feat: update doc comments with function assumptions

* feat: update readme

* chore: fix CI

halo2-base/src/gates/flex_gate/mod.rs

@@ -57,7 +57,6 @@ impl<F: ScalarField> BasicGateConfig<F> {
     ///
     /// Assumes `phase` is in the range [0, MAX_PHASE).
     /// * `meta`: [ConstraintSystem] used for the gate
-    /// * `strategy`: The [GateStrategy] to use for the gate
     /// * `phase`: The phase to add the gate to
     pub fn configure(meta: &mut ConstraintSystem<F>, phase: u8) -> Self {
         let value = match phase {
@@ -118,10 +117,7 @@ impl<F: ScalarField> FlexGateConfig<F> {
     ///
     /// Assumes `num_advice` is a [Vec] of length [MAX_PHASE]
     /// * `meta`: [ConstraintSystem] of the circuit
-    /// * `strategy`: [GateStrategy] of the flex gate
-    /// * `num_advice`: Number of [Advice] [Column]s in each phase
-    /// * `num_fixed`: Number of [Fixed] [Column]s in each phase
-    /// * `circuit_degree`: Degree that expresses the size of circuit (i.e., 2^<sup>circuit_degree</sup> is the number of rows in the circuit)
+    /// * `params`: see [FlexGateConfigParams]
     pub fn configure(meta: &mut ConstraintSystem<F>, params: FlexGateConfigParams) -> Self {
         // create fixed (constant) columns and enable equality constraints
         let mut constants = Vec::with_capacity(params.num_fixed);
@@ -918,7 +914,7 @@ impl<F: ScalarField> Default for GateChip<F> {
 }
 
 impl<F: ScalarField> GateChip<F> {
-    /// Returns a new [GateChip] with the given [GateStrategy].
+    /// Returns a new [GateChip] with some precomputed values. This can be called out of circuit and has no extra dependencies.
     pub fn new() -> Self {
         let mut pow_of_two = Vec::with_capacity(F::NUM_BITS as usize);
         let two = F::from(2);

halo2-base/src/gates/range/mod.rs

@@ -52,12 +52,9 @@ impl<F: ScalarField> RangeConfig<F> {
     ///
     /// Panics if `lookup_bits` > 28.
     /// * `meta`: [ConstraintSystem] of the circuit
-    /// * `range_strategy`: [GateStrategy] of the range chip
-    /// * `num_advice`: Number of [Advice] [Column]s without lookup enabled in each phase
+    /// * `gate_params`: see [FlexGateConfigParams]
     /// * `num_lookup_advice`: Number of `lookup_advice` [Column]s in each phase
-    /// * `num_fixed`: Number of fixed [Column]s in each phase
     /// * `lookup_bits`: Number of bits represented in the LookUp table [0,2^lookup_bits)
-    /// * `circuit_degree`: Degree that expresses the size of circuit (i.e., 2^<sup>circuit_degree</sup> is the number of rows in the circuit)
     pub fn configure(
         meta: &mut ConstraintSystem<F>,
         gate_params: FlexGateConfigParams,
@@ -194,10 +191,13 @@ pub trait RangeInstructions<F: ScalarField> {
         num_bits: usize,
     );
 
-    /// Performs a range check that `a` has at most `bit_length(b)` bits and then constrains that `a` is less than `b`.
+    /// Performs a range check that `a` has at most `ceil(b.bits() / lookup_bits) * lookup_bits` bits and then constrains that `a` is less than `b`.
     ///
     /// * a: [AssignedValue] value to check
     /// * b: upper bound expressed as a [u64] value
+    ///
+    /// ## Assumptions
+    /// * `ceil(b.bits() / lookup_bits) * lookup_bits <= F::CAPACITY`
     fn check_less_than_safe(&self, ctx: &mut Context<F>, a: AssignedValue<F>, b: u64) {
         let range_bits =
             (bit_length(b) + self.lookup_bits() - 1) / self.lookup_bits() * self.lookup_bits();
@@ -206,10 +206,13 @@ pub trait RangeInstructions<F: ScalarField> {
         self.check_less_than(ctx, a, Constant(F::from(b)), range_bits)
     }
 
-    /// Performs a range check that `a` has at most `bit_length(b)` bits and then constrains that `a` is less than `b`.
+    /// Performs a range check that `a` has at most `ceil(b.bits() / lookup_bits) * lookup_bits` bits and then constrains that `a` is less than `b`.
     ///
     /// * a: [AssignedValue] value to check
     /// * b: upper bound expressed as a [BigUint] value
+    ///
+    /// ## Assumptions
+    /// * `ceil(b.bits() / lookup_bits) * lookup_bits <= F::CAPACITY`
     fn check_big_less_than_safe(&self, ctx: &mut Context<F>, a: AssignedValue<F>, b: BigUint)
     where
         F: BigPrimeField,
@@ -280,10 +283,14 @@ pub trait RangeInstructions<F: ScalarField> {
 
     /// Constrains and returns `(c, r)` such that `a = b * c + r`.
     ///
-    /// Assumes that `b != 0` and that `a` has <= `a_num_bits` bits.
     /// * a: [QuantumCell] value to divide
     /// * b: [BigUint] value to divide by
     /// * a_num_bits: number of bits needed to represent the value of `a`
+    ///
+    /// ## Assumptions
+    /// * `b != 0` and that `a` has <= `a_num_bits` bits.
+    /// * `a_num_bits <= F::CAPACITY = F::NUM_BITS - 1`
+    ///   * Unsafe behavior if `a_num_bits >= F::NUM_BITS`
     fn div_mod(
         &self,
         ctx: &mut Context<F>,
@@ -330,6 +337,10 @@ pub trait RangeInstructions<F: ScalarField> {
     /// * a_num_bits: number of bits needed to represent the value of `a`
     /// * b_num_bits: number of bits needed to represent the value of `b`
     ///
+    /// ## Assumptions
+    /// * `a_num_bits <= F::CAPACITY = F::NUM_BITS - 1`
+    /// * `b_num_bits <= F::CAPACITY = F::NUM_BITS - 1`
+    /// * Unsafe behavior if `a_num_bits >= F::NUM_BITS` or `b_num_bits >= F::NUM_BITS`
     fn div_mod_var(
         &self,
         ctx: &mut Context<F>,
@@ -426,8 +437,13 @@ pub struct RangeChip<F: ScalarField> {
 
 impl<F: ScalarField> RangeChip<F> {
     /// Creates a new [RangeChip] with the given strategy and lookup_bits.
-    /// * strategy: [GateStrategy] for advice values in this chip
-    /// * lookup_bits: number of bits represented in the lookup table [0,2<sup>lookup_bits</sup>)
+    /// * `lookup_bits`: number of bits represented in the lookup table [0,2<sup>lookup_bits</sup>)
+    /// * `lookup_manager`: a [LookupAnyManager] for each phase.
+    ///
+    /// **IMPORTANT:** It is **critical** that all `LookupAnyManager`s use the same [`SharedCopyConstraintManager`](crate::virtual_region::copy_constraints::SharedCopyConstraintManager)
+    /// as in your primary circuit builder.
+    ///
+    /// It is not advised to call this function directly. Instead you should call `BaseCircuitBuilder::range_chip`.
     pub fn new(lookup_bits: usize, lookup_manager: [LookupAnyManager<F, 1>; MAX_PHASE]) -> Self {
         let limb_base = F::from(1u64 << lookup_bits);
         let mut running_base = limb_base;

halo2-base/src/safe_types/bytes.rs

@@ -41,7 +41,15 @@ impl<F: ScalarField, const MAX_LEN: usize> VarLenBytes<F, MAX_LEN> {
         MAX_LEN
     }
 
-    /// Left pads the variable length byte array with 0s to the MAX_LEN
+    /// Left pads the variable length byte array with 0s to the `MAX_LEN`.
+    /// Takes a fixed length array `self.bytes` and returns a length `MAX_LEN` array equal to
+    /// `[[0; MAX_LEN - len], self.bytes[..len]].concat()`, i.e., we take `self.bytes[..len]` and
+    /// zero pad it on the left, where `len = self.len`
+    ///
+    /// Assumes `0 < self.len <= MAX_LEN`.
+    ///
+    /// ## Panics
+    /// If `self.len` is not in the range `(0, MAX_LEN]`.
     pub fn left_pad_to_fixed(
         &self,
         ctx: &mut Context<F>,

halo2-base/src/safe_types/mod.rs

@@ -259,6 +259,10 @@ impl<'a, F: ScalarField> SafeTypeChip<'a, F> {
     /// * inputs: Slice representing the byte array.
     /// * len: [AssignedValue]<F> witness representing the variable length of the byte array. Constrained to be `<= MAX_LEN`.
     /// * MAX_LEN: [usize] representing the maximum length of the byte array and the number of elements it must contain.
+    ///
+    /// ## Assumptions
+    /// * `MAX_LEN < u64::MAX` to prevent overflow (but you should never make an array this large)
+    /// * `ceil((MAX_LEN + 1).bits() / lookup_bits) * lookup_bits <= F::CAPACITY` where `lookup_bits = self.range_chip.lookup_bits`
     pub fn raw_to_var_len_bytes<const MAX_LEN: usize>(
         &self,
         ctx: &mut Context<F>,
@@ -275,6 +279,10 @@ impl<'a, F: ScalarField> SafeTypeChip<'a, F> {
     /// * inputs: Vector representing the byte array, right padded to `max_len`. See [VarLenBytesVec] for details about padding.
     /// * len: [AssignedValue]<F> witness representing the variable length of the byte array. Constrained to be `<= max_len`.
     /// * max_len: [usize] representing the maximum length of the byte array and the number of elements it must contain. We enforce this to be provided explictly to make sure length of `inputs` is determinstic.
+    ///
+    /// ## Assumptions
+    /// * `max_len < u64::MAX` to prevent overflow (but you should never make an array this large)
+    /// * `ceil((max_len + 1).bits() / lookup_bits) * lookup_bits <= F::CAPACITY` where `lookup_bits = self.range_chip.lookup_bits`
     pub fn raw_to_var_len_bytes_vec(
         &self,
         ctx: &mut Context<F>,

halo2-ecc/src/fields/vector.rs

@@ -245,6 +245,9 @@ where
         FieldVector(a.into_iter().map(|coeff| self.fp_chip.carry_mod(ctx, coeff)).collect())
     }
 
+    /// # Assumptions
+    /// * `max_bits <= n * k` where `n = self.fp_chip.limb_bits` and `k = self.fp_chip.num_limbs`
+    /// * `a[i].truncation.limbs.len() = self.fp_chip.num_limbs` for all `i = 0..a.len()`
     pub fn range_check<A>(
         &self,
         ctx: &mut Context<F>,
@@ -432,6 +435,9 @@ macro_rules! impl_field_ext_chip_common {
             self.0.carry_mod(ctx, a)
         }
 
+        /// # Assumptions
+        /// * `max_bits <= n * k` where `n = self.fp_chip.limb_bits` and `k = self.fp_chip.num_limbs`
+        /// * `a[i].truncation.limbs.len() = self.fp_chip.num_limbs` for all `i = 0..a.len()`
         fn range_check(
             &self,
             ctx: &mut Context<F>,

halo2-ecc/src/secp256k1/tests/ecdsa_tests.rs

@@ -1,5 +1,3 @@
-#![allow(non_snake_case)]
-use crate::ff::Field as _;
 use crate::halo2_proofs::{
     arithmetic::CurveAffine,
     halo2curves::secp256k1::{Fq, Secp256k1Affine},