wai-verify includes staged/predict.rs and staged/wir1_arith.rs, whose
harnesses prove: step_in_range (for every residual the rANS decoder returns,
every step q and both element ranges, pred + r*q fits i64 and the element is
that sum clamped), up2_bounded (the half-pel prediction lies between the
neighbours it reads, odd output sizes included), rdiv_matches_spec (rdiv is
the rounding half away from zero, stated by inequalities rather than a second
division) and rate_index_in_bounds (every output sample's indices are source
samples, for every channel). The last two are nonlinear and hold over the
bounded windows their docs state; each harness's cover is reached.
rdiv and the rate indices move from i128/u128 to checked 64-bit arithmetic,
which is total for every input and gives the same values for every shape a
WIR1 payload allows; the corpus and the goldens are unchanged.
The CHANGELOG gains the staged-delivery subsection.
Co-Authored-By: Claude Opus 5.5 <[email protected]>
ea174e7a6f