Module interval_replay 

Independent range-safety checker for analog netlist claims — the trust core of the analog lane’s RangeCertificate, in the same spirit as this crate’s PR/RUP checker: a small, dependency-free replay the certificate producer cannot influence.

The compiler (one crate over) claims per-node voltage bounds for a mapped analog dataflow. This module re-derives those bounds from the declared input boxes by DIRECTED-OUTWARD-ROUNDED f64 interval arithmetic — after every interval operation each endpoint is bumped one ULP outward (next_down/next_up), so the replayed interval SOUNDLY contains every exactly- computed value regardless of intermediate rounding — and checks, fail-closed:

1. Honesty — the replayed interval of every node is contained in the node’s CLAIMED interval (a claim tighter than reality is rejected);
2. No clipping — every claimed interval lies within the usable rail half-span;
3. No starvation — every node’s claimed full scale clears the noise floor by the demanded dynamic-range ratio (a signal whose whole range drowns in noise is a gain-scheduling bug, not a small signal).

Any NaN or infinity anywhere — inputs, weights, claims, replay — rejects the certificate. No solver, no bignum, no imports beyond std. Trust this file, not the producer.

Structs

RangeClaim

The claim under judgment: declared math-domain input boxes, per-net power-of-two scales, claimed VOLT-domain per-node bounds, and the physical envelope they must respect.

Enums

RCell

The neutral cell vocabulary the checker replays. Mirrors (but does not import) the analog lane’s tile set; the producer converts its netlist into this form to be judged.

RSrc

An operand of a replayed cell: a plane input, a prior cell’s net, or a programmed constant.

Functions

check_integrator_claim

Replay a MULTI-STATE INTEGRATOR claim: the cells run once per frame over the held state vector (starting inside the init boxes); outs[s] gives state s’s next value. The claim’s input boxes must contain every frame’s state vector (the trajectory hull), and the per-node claims must contain the per-frame hulls, inside the rails / above the noise floor.

check_range_claim

Replay the claim and judge it. true iff every check passes; ANY malformation (arity mismatch, dangling reference, non-finite number, inverted interval) is false — fail-closed.

check_reduction_claim

Replay a STREAMED-REDUCTION claim: the same cells run once per frame with input 0 the element box and input 1 the carried accumulator (starting at init); the claim’s per-node bounds must contain the HULL of every frame’s replayed bounds, the claim’s input-1 box must contain the whole accumulator trajectory, and every claimed bound must respect the rails and the noise floor. Fail-closed on any malformation, divergence, or a frame count of zero.