Interval (arrayjit.Ir.Interval)

Interval (min/max) lattice shared between the per-tensor bounds summaries stored on Tnode.t and the interval_of analysis over Low_level.scalar_t. See docs/proposals/interval-analysis-scalar-t.md. This is deliberately the single module defining the bounds record and its operations (binding constraint 9 of the proposal): Tnode stores plain t values; Low_level extends them with a symbol environment and source tracking.

Invariants.

Outwardness: lo and hi always bound every possible (machine) value from below resp. above. Every arithmetic rule either produces exactly-representable endpoints or nudges the computed endpoints outward (see round_out), so ordering-based folds are sound without an exactness requirement (binding constraint 6: "exact endpoints or outward rounding at every operation").
NaN-freedom: a non-top interval asserts the value cannot be NaN. Any rule whose result may be NaN returns top. lo = nan never occurs.
integral asserts every possible machine value is a mathematical integer (note that every float of magnitude >= 2^53 is an integer, so integrality survives float rounding).
exact asserts the endpoints represent the true bounds exactly; in particular abs endpoint < 2^53 when integral (strict: 2^53 + 1 rounds to 2^53, binding constraint 6). Equality/singleton folds additionally require exact: two distinct integers above 2^53 may round to the same float.

type t = {

lo : Base.float;
hi : Base.float;
integral : Base.bool;
exact : Base.bool;

}

val t_of_sexp : Sexplib0.Sexp.t -> t

val sexp_of_t : t -> Sexplib0.Sexp.t

val compare : t -> t -> Base.int

val equal : t -> t -> Base.bool

val top : t

val is_top : t -> Base.bool

val exact_int_cutoff : float

Strict exact-integer cutoff: 2^53. Values with abs v < exact_int_cutoff read from integer storage convert to float exactly.

val endpoint_exact : Base.Float.t -> Base.bool

val point : Base.Float.t -> t

Constructs the singleton interval of a float value. NaN gives top; infinities give non-exact singletons (they never participate in folds).

val of_int : int -> t

val of_int_range : int -> int -> t

of_int_range lo hi is the interval of integers between lo and hi inclusive; requires lo <= hi.

val round_out : t -> t

Nudges endpoints outward by two ulps to absorb the round-to-nearest error of endpoint arithmetic (one ulp would do for a single operation; two is safety margin). Used whenever an arithmetic rule cannot guarantee exactly-representable endpoints, preserving the outwardness invariant.

val join : t -> t -> t

Lattice join (convex hull).

val inter : t -> t -> t

Lattice meet over the value sets; endpoint selection only, no arithmetic. The result can be empty (lo > hi) if the inputs are disjoint -- callers intersect facts known to hold simultaneously, so this does not arise for sound inputs.

val is_within : outer:t -> t -> Base.bool

Value-set containment: every value admitted by inner is admitted by outer. Used to validate proposals against settled bounds. Conservative: outward-rounded inner endpoints can only cause false rejections, never false acceptance.

val value_fits : t -> Base.Float.t -> Base.bool

Whether the single (machine) value v is admitted.

val is_singleton : t -> Base.bool

Truthiness

A derived view, not a lattice facet (see the proposal). Sound w.r.t. both the C emitters (!= 0, &&, ternary) and Ops.interpret_*: non-top intervals are NaN-free, so the C-vs-OCaml NaN divergences cannot arise on decided inputs.

val definitely_false : t -> Base.bool

val definitely_true : t -> Base.bool

Machine ranges of precisions

val dtype_range : Ops.prec -> t

The interval of all values representable (and thus of any machine result) at an integer precision; top for float and opaque-data precisions. Note the int64/uint64 upper endpoints round outward (2^63 - 1 is not a float) and are marked non-exact.

val float_exact_int_limit : Ops.prec -> float option

The largest magnitude up to which a float precision represents every integer exactly. bfloat16 has 7 mantissa bits, hence 256 -- not fp16's 2048 (binding constraint 5; witness: 257 is unrepresentable in bfloat16). fp8 is conservatively 8 (covers both e4m3 and e5m2).

val at_prec : Ops.prec -> t -> t

at_prec prec iv makes iv valid for the machine value of an expression computed at (or converted into) precision prec.

Integer precisions: a provably-in-range exact integral interval passes through; anything else falls back to dtype_range -- out-of-range casts wrap (binding constraint 5), and in particular a lower bound that could cross zero at an unsigned precision widens to the full unsigned range rather than being trusted (binding constraint 7: the "crosses zero" rule, implemented as widening instead of an assert so it stays sound if an emitter ever produces such arithmetic). Note dtype_range is also correct for the float-to-integer conversions C leaves undefined out of range: all supported backends produce some value of the type.
Float precisions: integrality and endpoint exactness survive only within the precision's exact-integer range (proposal lattice rules); everything else is top -- genuinely float computations never fold (Phase A policy), and float rounding could otherwise move machine values past real-arithmetic endpoints.
Void_prec/Uint4x32_prec: top.

Endpoint arithmetic

All rules take machine-valid operand intervals and return the real-arithmetic result interval; callers apply at_prec to account for the precision the operation actually computes in. Rules requiring finite endpoints return top otherwise (this also excludes operands that may be NaN, per the NaN-freedom invariant: top in, top out).

val all_finite : Base.Float.t Base.List.t -> bool

val arith_result : t -> t -> Base.Float.t -> Base.Float.t -> t

val add : t -> t -> t

val sub : t -> t -> t

val mul : t -> t -> t

val div : t -> t -> t

Division: top when the divisor interval contains 0 (or anything is unbounded); real-endpoint quotients otherwise, never exact (integer division truncates and float division rounds; the result is only used through at_prec, which widens integer-precision consumers to the dtype range since integral is cleared).

val mod_ : t -> t -> t

Modulo, proposal rule: divisor an exact positive integral singleton c and a non-negative integral argument give [0, min (hi, c-1)]; anything else is top (avoids the C remainder sign traps).

val max_ : t -> t -> t

val min_ : t -> t -> t

val relu : t -> t

ReLU: fmax(0, x) maps NaN to 0 in C, and Ops.interpret_unop agrees, so even a top argument yields a genuine lower bound of 0.

val neg : t -> t

val trunc : t -> t

Truncation toward zero; monotone, exactly representable when the argument endpoint is.

val satur01 : t -> t

Saturation to [0, 1]: monotone clamping. top arguments stay top: the OCaml interpreter returns NaN for NaN (C's fmax/fmin chain would give a number), so a possibly-NaN argument admits no codomain bound valid on all execution paths.

val exp_like : t -> t

Codomain bound for Exp/Exp2: non-negative. NaN maps to NaN, so top stays top.

val abs_le_1 : t -> t

Codomain bound for Sin/Cos/Tanh_approx: [-1, 1] (libm and the GPU intrinsics respect it); NaN maps to NaN, so top stays top.

val sqrt_ : t -> t

Codomain bound for Sqrt: requires a provably non-negative argument (else NaN is possible).

val bool_range : t

The [0, 1]-valued operations (comparisons, And/Or, Not): sound for any operands including NaN (all emitters produce 0 or 1).

val true_ : t

val false_ : t

Comparison folding

Decisions rely on the outwardness invariant; equality-true additionally requires exact singletons (binding constraint 6). NaN safety: a possibly-NaN operand implies a top interval whose infinite endpoints never satisfy the strict inequalities, so a fold-to-true never fires on possibly-NaN operands; fold-to-false agrees with NaN comparison semantics (false) in both C and the OCaml interpreter.

val cmplt_decides : t -> t -> bool option

Whether a < b is decided: Some true/Some false/None.

val cmpeq_decides : t -> t -> bool option

Whether a = b is decided. True requires both to be the same exact singleton; false requires disjointness (sound outward).