An offset interval bounds the values an integer name can hold, derived through its single definitionssingle definition nanofilA single definition is a temporary with exactly one definition in its function: a parameter, a phi or an instruction. The reuse forms read relations only between such names (a flight and its base, a proof and the pointer it checked, a span test or limit and its pointer), and the single-definition invariant says those relations hold at run time wherever the definition dominates the running point., so that a flightflight nanofilA flight builds a pointer from two independent sources: flight(D, Op, Args, Lower) computes D's address with copy, add or sub over l values and pointer addresses, and takes its capability from the pointer Lower names, or none (pizlonate:flight_inst/2). Making the pair proves nothing about access; no check, getter, memory access or safepoint happens inside it.'s offset from its base is known to lie in [Lo, Hi]. At class w it bounds the signed word itself; at l it bounds some integer congruent to the value modulo 2^64, which is all address arithmetic needs.

• ir:offset_interval/8ir.ploffset_interval+Once, +V, +K, +Depth, -Lo, -Hi, +Memo₀, -Memoas above, with each name's interval (or none) memoised, so an offset whose terms share names (x = x + x, repeated) is walked once per name. walks a narrow ext or load, copy, and with a mask, urem, shl and mul by a constant, add, and sub of a constant (ir:op_interval/9ir.plop_interval/9not documented), memoised under a depth limit of 32. Validate.v: oi, offset_interval.

• Interval.v: iv, one constructor per clause; offset_interval_iv (every answer is derived) and iv_sound (a derived interval holds where the names it walks hold their definitions). Chain.v's interval_at applies it at a run's point.

• Readers: guard chainsguard chain nanofilA pointer's guard chain lists its bases with the offset of its address from each: P itself at i(0, 0), then each base B reached through single-definition add, sub and copy flights whose lower donor is their address operand, with an interval for P's address minus B's, modulo 2^64. P has the capability of every base on its chain., hence renew_ifrenew_if nanofilA renew whose bounds come from a guard: renew_if(Lo, Hi, Rights, Align) of [P, G] is exactly a check of P, but where the span test G passed it natively tests only the flags and alignment, and where G failed it runs the full check out of line. The validator accepts it through ir:guard_covers/5, following P's guard chain (ir:guard_chain/3). and the needneed nanofilA need is the validator's backward fact for check_ahead: need(B) = H at a point says every path from it reaches a raw heap access through a pointer of which B is an exact base, whose bytes reach B + H, and reaches it first: before any instruction that is not ahead-transparent, any poll edge, edge back or end, and before B is redefined. analysis.

The subtlety: Prolog's evaluation shows through. The memo keeps successes but not failures, and op_interval/9ir.plop_interval/9not documented commits after its heads; Validate.v copies both rather than the clauses' logical reading.

See rocq.md, Offset intervals.