Enum ShapePredicate 

#[non_exhaustive]
pub enum ShapePredicate {
    AtLeast(u32),
    AtMost(u32),
    Exactly(u32),
    MultipleOf(u32),
    ModEquals {
        modulus: u32,
        remainder: u32,
    },
    AffineRange {
        scale: i64,
        offset: i64,
        min: i64,
        max: i64,
    },
    And(Box<ShapePredicate>, Box<ShapePredicate>),
    Or(Box<ShapePredicate>, Box<ShapePredicate>),
    Not(Box<ShapePredicate>),
}

Refinement predicate over a buffer’s element count (P-1.0-V3.1).

Represents a small grammar of constraints a BufferDecl author can attach. The validator (P-1.0-V3.2) checks each predicate against the program’s static count and the optimizer (P-1.0-V3.3) uses verified predicates to prove loop-bound and alignment invariants for vectorization.

None (the default) is “unconstrained”; existing programs keep their current behavior.

Variants (Non-exhaustive)

Non-exhaustive enums could have additional variants added in future. Therefore, when matching against variants of non-exhaustive enums, an extra wildcard arm must be added to account for any future variants.

AtLeast(u32)

count >= n. Holds when the runtime element count is at least n. Used to prove non-empty workgroup buffers and minimum vectorization tile sizes.

AtMost(u32)

count <= n. Holds when the count never exceeds n. Used to bound dispatch sizes and prevent oversized allocations.

Exactly(u32)

count == n. The strongest constraint; the count is fixed.

MultipleOf(u32)

count % n == 0. Used for alignment proofs (e.g. SIMD lanes).

ModEquals

count % modulus == remainder. Invalid modular forms evaluate false, so static validation catches impossible declarations.

Fields

modulus: u32

Divisor used by the modular equality.

remainder: u32

Required remainder. Must be less than modulus to match.

AffineRange

min <= count * scale + offset <= max, evaluated with wide arithmetic for frontend-derived affine constraints.

Fields

scale: i64

Multiplicative coefficient applied to count.

offset: i64

Constant term added after scaling.

min: i64

Inclusive lower bound for the affine expression.

max: i64

Inclusive upper bound for the affine expression.

And(Box<ShapePredicate>, Box<ShapePredicate>)

Conjunction of two predicates (p1 && p2). Both must hold.

Or(Box<ShapePredicate>, Box<ShapePredicate>)

Disjunction of two predicates (p1 || p2). Either may hold.

Not(Box<ShapePredicate>)

Negation of a predicate.

Implementations

impl ShapePredicate

pub fn holds(&self, count: u32) -> bool

Evaluate the predicate against a concrete count. Returns true when the predicate holds. P-1.0-V3.2 uses this from the validate() pass; P-1.0-V3.3 calls it from optimizer passes that need a yes/no proof.

pub fn evaluate(&self, count: u32) -> bool

Evaluate the predicate against a concrete count.

pub fn proves_non_empty(&self) -> bool

Whether this predicate proves that the count cannot be zero.

pub fn describe(&self) -> String

Human-readable form for error messages.

Trait Implementations

impl Clone for ShapePredicate

fn clone(&self) -> ShapePredicate

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ShapePredicate

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

Formats the value using the given formatter.

impl Eq for ShapePredicate

impl Hash for ShapePredicate

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for ShapePredicate

fn eq(&self, other: &ShapePredicate) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl StructuralPartialEq for ShapePredicate