Trait ConstraintBuilder

Source

pub trait ConstraintBuilder {
    type Expr: SetElement;
    type Ideal: Ideal;
    type FqIdeal: Ideal;

    // Required methods
    fn assert_in_ideal(&mut self, expr: Self::Expr, ideal: &Self::Ideal);
    fn assert_zero(&mut self, expr: Self::Expr);
    fn assert_in_fq_ideal(
        &mut self,
        prime_idx: usize,
        expr: Self::Expr,
        ideal: &Self::FqIdeal,
    );
}

Expand description

The abstract interface to constraint building logic. In essence it allows to create constraints modulo ideals.

Required Associated Types§

Source

type Expr: SetElement

The expressions the constraint builder operates on. It is opaque from the PoV of an AIR: arithmetic operations on it are provided by the expression config passed to Uair::constrain_general alongside the builder.

Source

type Ideal: Ideal

The type of ideals used by the constraint builder.

Source

type FqIdeal: Ideal

Ideals living over $F_{q_i}[X]$ for the prime tuple declared by the surrounding UairSignature::primes. A single ConstraintBuilder shares one runtime type for all primes; the prime index is passed at the call site via ConstraintBuilder::assert_in_fq_ideal. Builders that don’t care about $F_q[X]$-constraints (counters, collectors, etc.) set this to ImpossibleIdeal.

Required Methods§

Source

fn assert_in_ideal(&mut self, expr: Self::Expr, ideal: &Self::Ideal)

Add a constraint saying that expr belongs to the ideal ideal.

Source

fn assert_zero(&mut self, expr: Self::Expr)

Add a constraint saying that expr is equal to zero which is the same as saying that expr belongs to the zero ideal.

Source

fn assert_in_fq_ideal( &mut self, prime_idx: usize, expr: Self::Expr, ideal: &Self::FqIdeal, )

Add a constraint saying that expr, after coefficient-wise reduction mod $q_{\text{prime_index}}$ (the paper’s $\phi_{q_i}$), belongs to the $F_{q_i}[X]$-ideal ideal.

prime_idx indexes into UairSignature::primes and must be a valid index for any UAIR that calls this method.

§Ordering convention

The order of constraints within each family must be stable across constrain_general calls, so count_constraints / count_constraint_degrees / IdealCollector::{ideals, fq_ideals} line up per family.

§Scope: projections of f_0 only

expr is built only from the $Q[X]$-typed up/down rows passed to Uair::constrain_general — i.e. the projection $\phi_{q_i}(\hat f_0)$ of the single integer trace. There is no separate $\hat f_i$ witness typed natively in $F_{q_i}[X]$; $\phi_{q_i}$ is applied by the PIOP layer at prove/verify time.