Enum FactKind 

pub enum FactKind {
    ValueRange {
        lo: i64,
        hi: i64,
    },
    ShiftBound {
        bound: u32,
    },
    DivisorNonZero,
    InBoundsAccess {
        access_width: u32,
    },
    SelectTotality,
    MemoryDisjointness {
        other_value_id: u32,
    },
}

The fact kinds of encoding schema v1, in silicon-payoff order (the numbers are the on-wire kind bytes; 0x00 is deliberately unassigned so a zeroed buffer never parses as a fact).

Variants

ValueRange

0x01 — the value is within [lo, hi], signed, inclusive both ends (drives the dead-clamp elision, the gust_mix shape).

Fields

lo: i64

hi: i64

ShiftBound

0x02 — the shift amount is < bound (bare lsl/lsr, no mask).

Fields

bound: u32

DivisorNonZero

0x03 — the divisor is never zero (the div/rem trap guard is dead).

InBoundsAccess

0x04 — the address plus an access_width-byte access stays within linear-memory bounds (the bounds check is dead).

Fields

access_width: u32

SelectTotality

0x05 — both select arms are safe to evaluate: branchless IT lowering is admissible (pairs with VCR-SEL-004).

MemoryDisjointness

0x06 — this address and the one produced by other_value_id (same function) never alias: values may stay in registers across the store.

Fields

other_value_id: u32

Trait Implementations

impl Clone for FactKind

fn clone(&self) -> FactKind

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Copy for FactKind

impl Debug for FactKind

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

Formats the value using the given formatter.

impl Eq for FactKind

impl PartialEq for FactKind

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

Tests for self and other values to be equal, and is used by ==.

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

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for FactKind