Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[feat] update docs #211

Merged
merged 3 commits into from
Nov 3, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -66,3 +66,5 @@ jobs:

- name: Run cargo audit
uses: actions-rs/audit-check@v1
with:
token: ${{ secrets.GITHUB_TOKEN }}
578 changes: 56 additions & 522 deletions halo2-base/README.md

Large diffs are not rendered by default.

8 changes: 2 additions & 6 deletions halo2-base/src/gates/flex_gate/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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);
Expand Down
34 changes: 25 additions & 9 deletions halo2-base/src/gates/range/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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();
Expand All @@ -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,
Expand Down Expand Up @@ -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>,
Expand Down Expand Up @@ -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>,
Expand Down Expand Up @@ -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;
Expand Down
10 changes: 9 additions & 1 deletion halo2-base/src/safe_types/bytes.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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>,
Expand Down
8 changes: 8 additions & 0 deletions halo2-base/src/safe_types/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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>,
Expand All @@ -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>,
Expand Down
6 changes: 6 additions & 0 deletions halo2-ecc/src/fields/vector.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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>,
Expand Down Expand Up @@ -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>,
Expand Down
2 changes: 0 additions & 2 deletions halo2-ecc/src/secp256k1/tests/ecdsa_tests.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,3 @@
#![allow(non_snake_case)]
use crate::ff::Field as _;
use crate::halo2_proofs::{
arithmetic::CurveAffine,
halo2curves::secp256k1::{Fq, Secp256k1Affine},
Expand Down
Loading