interp::run_observed reports to an Observe every value an operator forms under
one of §5's named intermediates (the keys of §8.5, Table 8.5-A), and every
producer-result element before its policy. run is run_observed with Quiet,
which compiles to nothing. gram and apply now form their epilogue through
rq_apply: their rq has no multiplier and no bias (a parse rule), so the
integers are the same.
bounds::Within is an observer that holds a run to a pass: every value must lie
in the interval the pass records for it, and every key must be one the node
records.
- Every golden decode (tests/goldens.rs) runs observed: every committed set's
decode stays inside its certified intervals.
- tests/trace.rs: hand-built graphs at the edge of acc64, one per operator
family, loaded through step 8 and run on inputs at their range ends and on
samples; softmax one past its widest spread, and elu with α = −2^63, are
refused at load.
- The photo witness, run observed, stays inside node 6's intervals, and its
accumulator with the bias attains convT.acc's upper end.
Co-Authored-By: Claude Opus 5.5 <[email protected]>
129cb11bb2