Struct IsLtSubAir

pub struct IsLtSubAir {
    pub bus: VariableRangeCheckerBus,
    pub max_bits: usize,
    pub decomp_limbs: usize,
}

This is intended for use as a SubAir, not as a standalone Air.

This SubAir constrains the boolean equal to 1 iff x < y, assuming the two numbers both have a max number of bits, given by max_bits. The SubAir compares the numbers by decomposing y - x - 1 + 2^max_bits into limbs of size bus.range_max_bits, and interacts with a VariableRangeCheckerBus to range check the decompositions.

The SubAir will own auxilliary columns to store the decomposed limbs. The number of limbs is max_bits.div_ceil(bus.range_max_bits).

The expected max constraint degree of eval is deg(count) + max(1, deg(x), deg(y))

N.B.: AssertLtSubAir could be implemented by directly passing through to IsLtSubAir with out = AB::Expr::ONE. The only additional constraint in this air is assert_bool(io.out). However since both Airs are fundamental and the constraints are simple, we opt to keep the two versions separate.

Fields

bus: VariableRangeCheckerBus

The bus for sends to range chip

max_bits: usize

The maximum number of bits for the numbers to compare Soundness requirement: max_bits <= 29 max_bits > 29 doesn’t work: the approach is to decompose and range check y - x - 1 + 2^max_bits is non-negative. This requires 2^{max_bits+1} < |F|. When F::bits() = 31, this implies max_bits <= 29.

decomp_limbs: usize

decomp_limbs = max_bits.div_ceil(bus.range_max_bits).

Implementations

impl IsLtSubAir

pub fn new(bus: VariableRangeCheckerBus, max_bits: usize) -> Self

pub fn range_max_bits(&self) -> usize

pub fn when_transition(self) -> IsLtWhenTransitionAir

pub fn eval_range_checks<AB: InteractionBuilder>( &self, builder: &mut AB, lower_decomp: &[AB::Var], count: impl Into<AB::Expr>, )

Trait Implementations

impl Clone for IsLtSubAir

fn clone(&self) -> IsLtSubAir

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for IsLtSubAir

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<AB: InteractionBuilder> SubAir<AB> for IsLtSubAir

type AirContext<'a> = (IsLessThanIo<<AB as AirBuilder>::Expr>, &'a [<AB as AirBuilder>::Var]) where AB::Expr: 'a, AB::Var: 'a, AB: 'a

Type to define the context, typically in terms of AB::Expr that are needed to define the SubAir’s constraints.

fn eval<'a>( &'a self, builder: &'a mut AB, (io, lower_decomp): (IsLessThanIo<AB::Expr>, &'a [AB::Var]), )

where AB::Var: 'a, AB::Expr: 'a,

impl<F: Field> TraceSubRowGenerator<F> for IsLtSubAir

type TraceContext<'a> = (&'a VariableRangeCheckerChip, u32, u32)

(range_checker, x, y)

type ColsMut<'a> = (&'a mut [F], &'a mut F)

(lower_decomp, out)

fn generate_subrow<'a>( &'a self, (range_checker, x, y): (&'a VariableRangeCheckerChip, u32, u32), (lower_decomp, out): (&'a mut [F], &'a mut F), )

Only use this when count != 0.

impl Copy for IsLtSubAir