aver::ir::interval

Struct Interval

pub struct Interval {
    pub lo: Bound,
    pub hi: Bound,
}

Expand description

A constant integer interval [lo, hi] over the extended integers. Produced by interval_of_invariant from a refinement predicate and propagated bottom-up through an operation body by the abstract interpreter in classify_op.

Fields§

§lo: Bound§hi: Bound

Implementations§

Source §

impl Interval

Source

pub fn unbounded() -> Interval

The whole extended integer line — the conservative “I know nothing” answer the analysis returns whenever it declines.

Source

pub fn point(k: i128) -> Interval

A single point [k, k].

Source

pub fn ge(k: i128) -> Interval

[k, +inf] — the over-approximation of n >= k.

Source

pub fn le(k: i128) -> Interval

[-inf, k] — the over-approximation of n <= k.

Source

pub fn between(lo: i128, hi: i128) -> Interval

[lo, hi] from two literal bounds.

Source

pub fn intersect(self, other: Interval) -> Interval

Intersection — used to combine the conjuncts of a compound Bool.and guard into a single two-sided interval.

Source

pub fn hull(self, other: Interval) -> Interval

Convex hull (worst-case widening join) — the merge operator for control-flow joins and the per-value worst accumulator the general range pass uses. If either operand escapes i64, so does the hull, keeping the headroom verdict sound. Public mirror of the crate-private join free fn so the bare-i64 consumer (outside this module) can widen without re-deriving the rule.

Source

pub fn fits_i64(self) -> bool

true when both bounds are finite and within the i64 range. This is the headroom test: an intermediate whose interval fits_i64 cannot overflow a raw i64 before the smart constructor’s guard re-validates it.

Source

pub fn contains_point(self, k: i128) -> bool

true when the constant k provably lies within [lo, hi]. Used by the carrier-i64 eligibility tightening: a BARE record constructor outside the smart-ctor whose carrier-field argument is a literal in the proven interval is SAFE (it cannot smuggle an out-of-bound / i64-overflowing value past the gate), so it does not demote the carrier. A non-literal argument (or a literal outside the interval) is ungated and DOES demote. Bound::le is module-private, so this containment test must live here.

Source

pub fn widen(self, next: Interval) -> Interval

Standard interval widening ∇. An endpoint that moved OUTWARD between the previous iterate self and the next iterate next jumps to the matching infinity; a stable or inward-moving endpoint is kept (as the enclosing bound of the two). ENLARGING-ONLY: the result is always a superset of next, so widening can never make an interval too narrow (soundness preserved — only precision is lost). It is the termination operator for the bare-i64 interval fixpoint: a genuinely-unbounded endpoint reaches ±inf in one widen step, capping the chain height.

Bound::le is module-private, so this MUST live in interval.rs.

Source

pub fn add(self, other: Interval) -> Interval

Saturating interval addition. (Inherent, not std::ops::Add: the operation saturates rather than panicking, so the std trait would carry the wrong contract.)

Source

pub fn sub(self, other: Interval) -> Interval

Saturating interval subtraction (a - b = a + (-b), with the endpoints flipped so lo stays the lower bound).

Source

pub fn mul(self, other: Interval) -> Interval

Saturating interval multiplication. The product range is the min/max over the four endpoint products, which is the standard sound interval-arithmetic rule and handles negative operands.