//! The one arithmetic step of a residual refinement (`WIR1`,
//! `extensions/staged-delivery.md` Appendix A.1): `clamp(pred + r·q, lo, hi)`, as the
//! direct decode ran it. A decode steps through the integer operator set's E9
//! (`wai_ops::stage::residual_step`; K29 holds its 32-bit form to it); this step is
//! test-only (`legacy_int`), the reference the differential holds that one to.
//!
//! Self-contained (`core` only), so the model checker (`wai-verify`, harness
//! `step_in_range`) proves it as the decoder runs it: for every `r` the rANS decoder
//! can return (`[−2^31, 2^31 − 1]`, the bypass saturates there), every step
//! `q ∈ [1, 65535]` and every prediction in the element's range, no operation
//! overflows and the result is in the range.

/// The u8 element range.
pub const U8_RANGE: (i64, i64) = (0, 255);
/// The i16 element range.
pub const I16_RANGE: (i64, i64) = (-32768, 32767);

/// `clamp(pred + r·q, lo, hi)`. With `|r| ≤ 2^31`, `1 ≤ q < 2^16` and `|pred| < 2^16`,
/// `|r·q| < 2^47`, so every step fits `i64`; outside those bounds the sum saturates
/// before the clamp, so the function is total for every input.
pub fn step(pred: i64, r: i64, q: i64, lo: i64, hi: i64) -> i64 {
    pred.saturating_add(r.saturating_mul(q)).clamp(lo, hi.max(lo))
}

/// `step_in_range`: for every `r` the rANS decoder returns, every step `q` in
/// `1..=65535`, both element ranges and every prediction in the range, `pred + r·q`
/// fits `i64` without saturating, and the step is that sum clamped to the range. So a
/// build with overflow checks and one without compute the same element.
#[cfg(kani)]
#[kani::proof]
fn step_in_range() {
    let r: i64 = kani::any();
    kani::assume(r >= -(1i64 << 31) && r < (1i64 << 31));
    let q: i64 = kani::any();
    kani::assume((1..=65_535).contains(&q));
    let wide: bool = kani::any();
    let (lo, hi) = if wide { I16_RANGE } else { U8_RANGE };
    let pred: i64 = kani::any();
    kani::assume(pred >= lo && pred <= hi);
    let exact = r.checked_mul(q).and_then(|m| pred.checked_add(m));
    kani::assert(exact.is_some(), "pred + r·q fits i64");
    let v = step(pred, r, q, lo, hi);
    kani::assert(v >= lo && v <= hi, "the element is in its range");
    kani::assert(Some(v) == exact.map(|e| e.clamp(lo, hi)), "the step is the exact sum, clamped");
    kani::cover!(v == lo, "the clamp's floor is reached");
    kani::cover!(v == hi, "the clamp's ceiling is reached");
}
