halo2_base::gates::range

Trait RangeInstructions

Source
pub trait RangeInstructions<F: ScalarField> {
    type Gate: GateInstructions<F>;

    // Required methods
    fn gate(&self) -> &Self::Gate;
    fn lookup_bits(&self) -> usize;
    fn range_check(
        &self,
        ctx: &mut Context<F>,
        a: AssignedValue<F>,
        range_bits: usize,
    );
    fn check_less_than(
        &self,
        ctx: &mut Context<F>,
        a: impl Into<QuantumCell<F>>,
        b: impl Into<QuantumCell<F>>,
        num_bits: usize,
    );
    fn is_less_than(
        &self,
        ctx: &mut Context<F>,
        a: impl Into<QuantumCell<F>>,
        b: impl Into<QuantumCell<F>>,
        num_bits: usize,
    ) -> AssignedValue<F>;

    // Provided methods
    fn check_less_than_safe(
        &self,
        ctx: &mut Context<F>,
        a: AssignedValue<F>,
        b: u64,
    ) { ... }
    fn check_big_less_than_safe(
        &self,
        ctx: &mut Context<F>,
        a: AssignedValue<F>,
        b: BigUint,
    )
       where F: BigPrimeField { ... }
    fn is_less_than_safe(
        &self,
        ctx: &mut Context<F>,
        a: AssignedValue<F>,
        b: u64,
    ) -> AssignedValue<F> { ... }
    fn is_big_less_than_safe(
        &self,
        ctx: &mut Context<F>,
        a: AssignedValue<F>,
        b: BigUint,
    ) -> AssignedValue<F>
       where F: BigPrimeField { ... }
    fn div_mod(
        &self,
        ctx: &mut Context<F>,
        a: impl Into<QuantumCell<F>>,
        b: impl Into<BigUint>,
        a_num_bits: usize,
    ) -> (AssignedValue<F>, AssignedValue<F>)
       where F: BigPrimeField { ... }
    fn div_mod_var(
        &self,
        ctx: &mut Context<F>,
        a: impl Into<QuantumCell<F>>,
        b: impl Into<QuantumCell<F>>,
        a_num_bits: usize,
        b_num_bits: usize,
    ) -> (AssignedValue<F>, AssignedValue<F>)
       where F: BigPrimeField { ... }
    fn get_last_bit(
        &self,
        ctx: &mut Context<F>,
        a: AssignedValue<F>,
        limb_bits: usize,
    ) -> AssignedValue<F> { ... }
}
Expand description

Trait that implements methods to constrain a field element number x is within a range of bits.

Required Associated Types§

Source

type Gate: GateInstructions<F>

The type of Gate used within the instructions.

Required Methods§

Source

fn gate(&self) -> &Self::Gate

Returns the type of gate used.

Source

fn lookup_bits(&self) -> usize

Returns the number of bits the lookup table represents.

Source

fn range_check( &self, ctx: &mut Context<F>, a: AssignedValue<F>, range_bits: usize, )

Checks and constrains that a lies in the range [0, 2range_bits).

Inputs:

  • a: AssignedValue value to be range checked
  • range_bits: number of bits in the range
Source

fn check_less_than( &self, ctx: &mut Context<F>, a: impl Into<QuantumCell<F>>, b: impl Into<QuantumCell<F>>, num_bits: usize, )

Constrains that ‘a’ is less than ‘b’.

Assumes that a and b have bit length <= num_bits bits.

Note: This may fail silently if a or b have more than num_bits.

  • a: QuantumCell value to check
  • b: upper bound expressed as a QuantumCell
  • num_bits: number of bits used to represent the values of a and b
Source

fn is_less_than( &self, ctx: &mut Context<F>, a: impl Into<QuantumCell<F>>, b: impl Into<QuantumCell<F>>, num_bits: usize, ) -> AssignedValue<F>

Constrains whether a is in [0, b), and returns 1 if a < b, otherwise 0.

Assumes thata 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

Provided Methods§

Source

fn check_less_than_safe( &self, ctx: &mut Context<F>, a: AssignedValue<F>, b: u64, )

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.

§Assumptions
  • ceil(b.bits() / lookup_bits) * lookup_bits <= F::CAPACITY
Source

fn check_big_less_than_safe( &self, ctx: &mut Context<F>, a: AssignedValue<F>, b: BigUint, )
where F: BigPrimeField,

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.

§Assumptions
  • ceil(b.bits() / lookup_bits) * lookup_bits <= F::CAPACITY
Source

fn is_less_than_safe( &self, ctx: &mut Context<F>, a: AssignedValue<F>, b: u64, ) -> AssignedValue<F>

Performs a range check that a has at most ceil(bit_length(b) / lookup_bits) * lookup_bits and then returns whether a is in [0,b).

Returns 1 if a < b, otherwise 0.

Source

fn is_big_less_than_safe( &self, ctx: &mut Context<F>, a: AssignedValue<F>, b: BigUint, ) -> AssignedValue<F>
where F: BigPrimeField,

Performs a range check that a has at most ceil(b.bits() / lookup_bits) * lookup_bits bits and then returns whether a is in [0,b).

Returns 1 if a < b, otherwise 0.

For the current implementation using is_less_than, we require ceil(b.bits() / lookup_bits) + 1 < F::NUM_BITS / lookup_bits

Source

fn div_mod( &self, ctx: &mut Context<F>, a: impl Into<QuantumCell<F>>, b: impl Into<BigUint>, a_num_bits: usize, ) -> (AssignedValue<F>, AssignedValue<F>)
where F: BigPrimeField,

Constrains and returns (c, r) such that a = b * c + r.

  • 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
Source

fn div_mod_var( &self, ctx: &mut Context<F>, a: impl Into<QuantumCell<F>>, b: impl Into<QuantumCell<F>>, a_num_bits: usize, b_num_bits: usize, ) -> (AssignedValue<F>, AssignedValue<F>)
where F: BigPrimeField,

Constrains and returns (c, r) such that a = b * c + r.

Assumes: that b != 0. that a has <= a_num_bits bits. that b has <= b_num_bits bits.

Note: Let X = 2 ** b_num_bits Write a = a1 * X + a0 and c = c1 * X + c0 If we write b * c0 + r = d1 * X + d0 then b * c + r = (b * c1 + d1) * X + d0

  • a: QuantumCell value to divide
  • b: QuantumCell value to divide by
  • 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
Source

fn get_last_bit( &self, ctx: &mut Context<F>, a: AssignedValue<F>, limb_bits: usize, ) -> AssignedValue<F>

Constrains and returns the last bit of the value of a.

Assume a has been range checked already to limb_bits bits.

  • a: AssignedValue value to get the last bit of
  • limb_bits: number of bits in a limb

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors§