Trait halo2_base::gates::range::RangeInstructions

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> { ... }
}

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

Required Associated Types

type Gate: GateInstructions<F>

The type of Gate used within the instructions.

Required Methods

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

Returns the type of gate used.

fn lookup_bits(&self) -> usize

Returns the number of bits the lookup table represents.

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

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

Inputs:

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

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

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

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.

• 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_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.

• a: AssignedValue value to check
• b: upper bound expressed as a BigUint value

Assumptions

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

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.

• a: AssignedValue value to check
• b: upper bound as u64 value

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.

• a: AssignedValue value to check
• b: upper bound as BigUint value

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

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

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

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

Object Safety

This trait is not object safe.

Implementors

impl<F: ScalarField> RangeInstructions<F> for RangeChip<F>

type Gate = GateChip<F>