Struct AssertLtSubAir

pub struct AssertLtSubAir {
    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 that x < y when count != 0, assuming the two numbers both have a max number of bits, given by max_bits. The SubAir decomposes y - x - 1 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))

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 check that y-x-1 is non-negative. For a field with prime modular, this is equivalent to checking that y-x-1 is in the range [0, 2^max_bits - 1]. However, for max_bits > 29, if y is small enough and x is large enough, then y-x-1 is negative but can still be in the range due to the field size not being big enough.

decomp_limbs: usize

decomp_limbs = max_bits.div_ceil(bus.range_max_bits) is the number of limbs that y - x - 1 will be decomposed into.

Implementations

impl AssertLtSubAir

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

pub fn when_transition(self) -> AssertLtWhenTransitionAir

pub fn range_max_bits(&self) -> usize

Trait Implementations

impl Clone for AssertLtSubAir

fn clone(&self) -> AssertLtSubAir

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for AssertLtSubAir

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

Formats the value using the given formatter.

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

type AirContext<'a> = (AssertLessThanIo<<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): (AssertLessThanIo<AB::Expr>, &'a [AB::Var]), )

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

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

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

(range_checker, x, y)

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

lower_decomp

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

Should only be used when io.count != 0.

impl Copy for AssertLtSubAir