the-q 0.1.0

//! The crate's edges: `f64` in, `f64` out, `Display`, `serde`.
//!
//! # The trusted boundary
//!
//! Exactly two functions in this crate touch a float, and both are at the edge:
//!
//! * [`f64_decompose`] pulls the IEEE-754 binary64 fields out of a `f64`. It is
//!   `external_body`, because Verus has no model of `f64::to_bits`. Everything
//!   downstream of it is ordinary verified integer arithmetic: the conversion of
//!   `(sign, mantissa, exponent)` into a rational, and the rounding of that
//!   rational. The *only* assumption is that the triple denotes the float.
//! * [`to_f64`] serves display and DTO use only. It is `external_body`. Its
//!   output must not return into `Rat` arithmetic. Such a round trip silently
//!   reintroduces every `f64` problem this crate removes.
//!
//! `TRUSTED.md` enumerates both, with their assumed specifications and the
//! differential tests that back them.
//!
//! # Why the input path is exact
//!
//! An `f64` *is* a rational: `±m · 2^e` with a 53-bit `m`. `from_f64_dir`
//! therefore does no floating-point reasoning. It builds `m / 2^-e` (or
//! `m · 2^e` over `1`) as integers. It then hands the pair to the same verified
//! rounding function that every arithmetic operation uses.

use verus_builtin_macros::verus;

#[allow(unused_imports)]
use verus_builtin::*;
#[allow(unused_imports)]
use vstd::prelude::*;

#[allow(unused_imports)]
use crate::model::*;
#[allow(unused_imports)]
use crate::round::*;
use crate::types::{Dir, Rat};

verus! {

/// The IEEE-754 binary64 decomposition of a finite float: `(negative,
/// mantissa, exponent)` denoting `(-1)^negative · mantissa · 2^exponent`.
///
/// `None` for NaN and the infinities.
///
/// **TRUSTED** (`external_body`). Verus has no model of `f64::to_bits`. The
/// correspondence between the returned triple and the float's real value is
/// therefore an assumption. `TRUSTED.md` lists it, and differential tests check
/// it against `malachite-q`'s exact `Rational::try_from(f64)`.
#[verifier::external_body]
pub fn f64_decompose(v: f64) -> (r: Option<(bool, u64, i32)>)
    ensures
        r.is_some() ==> {
            let t = r.unwrap();
            &&& t.1 <= 9007199254740992u64  // 2^53
            &&& -1074 <= t.2 <= 971
        },
{
    let bits: u64 = v.to_bits();
    let neg: bool = (bits >> 63) != 0;
    let raw_exp: u64 = (bits >> 52) & 0x7ff;
    let frac: u64 = bits & 0x000f_ffff_ffff_ffff;
    if raw_exp == 0x7ff {
        // NaN or +/- infinity.
        return None;
    }
    if raw_exp == 0 {
        // Subnormal (and zero): value == frac * 2^-1074.
        Some((neg, frac, -1074))
    } else {
        // Normal: value == (2^52 + frac) * 2^(raw_exp - 1075).
        Some((neg, frac + 0x0010_0000_0000_0000u64, raw_exp as i32 - 1075))
    }
}

/// Convert an `f64` to a `Rat`, rounding in direction `dir`.
///
/// Returns `None` on NaN, on either infinity, and on `|v| > 2^61`. The
/// specification explicitly permits a restriction of the magnitude.
///
/// Below `2^-62` in magnitude, the value is under the finest grid this crate
/// uses. The result is then the appropriate endpoint of that first grid cell:
/// `0` for `Nearest`, and the neighbouring `±2^-61` for the directed modes,
/// which stay on their side of the value.
///
/// **The postcondition here is weak, because the trusted boundary shows
/// through.** Verus has no model of `f64`, so no postcondition here mentions
/// `v`'s value at all. R2 and R3 *against the float* are not statable, and thus
/// not provable. Everything downstream of the decomposition is provable, and it
/// lives on [`from_parts_dir`]. This function is a two-line composition of that
/// one. The rounding contract is the contract of [`from_parts_dir`] plus
/// [`f64_decompose`]'s assumption from `TRUSTED.md`.
pub fn from_f64_dir(v: f64, dir: Dir) -> (r: Option<Rat>)
    ensures
        r.is_some() ==> r.unwrap().wf(),
{
    match f64_decompose(v) {
        None => None,
        Some((neg, mant, e)) => from_parts_dir(neg, mant, e, dir),
    }
}

/// The exact numerator of the value an IEEE-754 decomposition denotes:
/// `(-1)^neg · mant · 2^e`, with the `2^e` folded in when `e >= 0`.
pub open spec fn parts_num(neg: bool, mant: u64, e: i32) -> int {
    let m = if neg {
        -(mant as int)
    } else {
        mant as int
    };
    if e >= 0 {
        m * pow2(e as nat)
    } else {
        m
    }
}

/// The exact denominator of the same value, always positive.
pub open spec fn parts_den(e: i32) -> int {
    if e >= 0 {
        1int
    } else {
        pow2((-e) as nat)
    }
}

/// The verified core of [`from_f64_dir`]: an IEEE-754 decomposition to a `Rat`,
/// rounded in direction `dir`.
///
/// **The contract lives here.** `from_f64_dir` states no contract, because
/// nothing in Verus relates an `f64` to a rational. That correspondence is the
/// single assumption [`f64_decompose`] carries. Everything *downstream* of the
/// triple is ordinary integer arithmetic, as the module header states. This
/// separate function makes that claim checkable rather than a comment.
///
/// The postcondition is the strongest available. It pins the result to
/// `round_frac` applied to the exact decomposed rational, which fixes the result
/// completely. R2 and R3 against that rational follow from
/// `round::lemma_r2_directed` and `round::lemma_r3_error`. (These two names
/// carry no intra-doc links: items inside `verus!` are not resolvable targets
/// from another module.) The postconditions below restate R2 and R3, so callers
/// do not re-derive them.
///
/// One postcondition covers all three branches. It covers the sub-grid branch as
/// well, whose denominator `2^s` with `s > 124` is past what `round_frac_exec`
/// accepts. `round::lemma_round_frac_subgrid` closes that gap.
///
/// # The domain is checked at run time as well as proved
///
/// A *verified* caller discharges the `requires` below, and
/// [`f64_decompose`]'s postcondition matches it exactly. `from_f64_dir`
/// therefore gets it at no cost. The `requires` is ghost: `cargo build` erases
/// it, so it binds no caller outside a `verus!` block, and this function is
/// `pub`. An unverified caller that passes `mant` above `2^53` otherwise reaches
/// `mant · 2^e` with `e` up to `64` and overflows `i128`. That overflow is
/// silent in any dependent crate built with the default
/// `overflow-checks = false`. The body therefore re-checks the same bounds first
/// and returns `None`. The check costs one comparison on a path that already
/// branches, and it makes the function total for every caller, not only for the
/// callers Verus sees.
pub fn from_parts_dir(neg: bool, mant: u64, e: i32, dir: Dir) -> (r: Option<Rat>)
    requires
        mant <= 9007199254740992u64,
        -1074 <= e <= 971,
    ensures
        r.is_some() ==> r.unwrap().wf(),
        // The value pin, over the *decomposed* rational.
        r.is_some() ==> r.unwrap() == round_frac(parts_num(neg, mant, e), parts_den(e), dir),
        // R2 and R3, guarded on `!saturated`, exactly as the crate's rounding
        // contract is scoped. This function discharges the guard for every
        // value it accepts rather than assumes it. It returns `None` above
        // `2^61`, so every value with a result is far inside the ceiling.
        r.is_some() ==> !saturated(parts_num(neg, mant, e), parts_den(e)),
        (r.is_some() && dir == Dir::Down) ==> q_le_frac(
            r.unwrap(),
            parts_num(neg, mant, e),
            parts_den(e),
        ),
        (r.is_some() && dir == Dir::Up) ==> q_ge_frac(
            r.unwrap(),
            parts_num(neg, mant, e),
            parts_den(e),
        ),
        r.is_some() ==> within_error_bound(
            r.unwrap(),
            parts_num(neg, mant, e),
            parts_den(e),
        ),
        // Completeness: the documented magnitude restriction is the *only*
        // reason this returns `None`.
        r.is_none() ==> abs_int(parts_num(neg, mant, e)) > pow2(61) * parts_den(e),
{
    // The `requires` above, enforced for callers Verus never sees. This branch
    // is dead under verification. The postconditions below are therefore
    // unweakened by it.
    if mant > 9007199254740992u64 || e < -1074 || e > 971 {
        return None;
    }
    if mant == 0 {
        proof {
            if e >= 0 {
                assert(parts_num(neg, mant, e) == 0) by (nonlinear_arith)
                    requires
                        parts_num(neg, mant, e) == 0 * pow2(e as nat),
                ;
            }
            assert(parts_den(e) > 0) by {
                lemma_pow2_pos((-e) as nat);
            }
            lemma_r2_r3_directed(parts_num(neg, mant, e), parts_den(e), dir);
        }
        return Some(Rat::zero());
    }
    proof {
        lemma_pow2_61();
        lemma_pow2_62();
        lemma_pow2_124();
        lemma_pow2_126();
    }
    if e >= 0 {
        proof {
            lemma_pow2_pos(e as nat);
            // `|±mant · 2^e| == mant · 2^e`. Every branch below needs this
            // fact. It is a fact about `abs_int` of a product, so it is
            // established here rather than assumed inside a nonlinear block.
            let m = if neg {
                -(mant as int)
            } else {
                mant as int
            };
            lemma_abs_mul_pos(m, pow2(e as nat));
            assert(abs_int(m) == mant as int);
            assert(abs_int(parts_num(neg, mant, e)) == (mant as int) * pow2(e as nat));
        }
        if e > 64 {
            proof {
                // `mant >= 1` and `e >= 65`, so the value is at least `2^65`.
                // The postcondition needs a *strict* excess over `2^61`, so the
                // proof goes through `2^62`. Monotonicity alone gives only
                // `<=`.
                lemma_pow2_mono(62nat, e as nat);
                lemma_pow2_pos(61nat);
                lemma_pow2_pos(e as nat);
                assert(pow2(62) == 2 * pow2(61));
                assert(abs_int(parts_num(neg, mant, e)) >= pow2(e as nat))
                    by (nonlinear_arith)
                    requires
                        abs_int(parts_num(neg, mant, e)) == (mant as int) * pow2(e as nat),
                        mant >= 1,
                        pow2(e as nat) > 0,
                ;
                assert(parts_den(e) == 1);
                assert(abs_int(parts_num(neg, mant, e)) > pow2(61) * parts_den(e))
                    by (nonlinear_arith)
                    requires
                        abs_int(parts_num(neg, mant, e)) >= pow2(e as nat),
                        pow2(62) <= pow2(e as nat),
                        pow2(62) == 2 * pow2(61),
                        pow2(61) > 0,
                        parts_den(e) == 1,
                ;
            }
            return None;
        }
        let p: i128 = pow2_i128(e as u32);
        proof {
            // mant <= 2^53 and p == 2^e <= 2^64, so the product is at most
            // 2^117, far inside i128.
            lemma_pow2_mono(e as nat, 64nat);
            lemma_pow2_64();
            assert((mant as int) * (p as int) <= 9007199254740992int
                * 18446744073709551616int) by (nonlinear_arith)
                requires
                    0 <= mant <= 9007199254740992int,
                    0 < p <= 18446744073709551616int,
            ;
        }
        let mag: i128 = (mant as i128) * p;
        proof {
            assert(abs_int(parts_num(neg, mant, e)) == mag as int) by (nonlinear_arith)
                requires
                    abs_int(parts_num(neg, mant, e)) == (mant as int) * pow2(e as nat),
                    mag as int == (mant as int) * (p as int),
                    p as int == pow2(e as nat),
            ;
        }
        if mag > 2305843009213693952i128 {
            // > 2^61
            return None;
        }
        let n: i128 = if neg {
            0 - mag
        } else {
            mag
        };
        proof {
            assert(pow2(0) == 1);
            // `-(mant · 2^e) == (-mant) · 2^e`. The code applies the sign to
            // the product, and the spec applies it to the mantissa.
            assert(-((mant as int) * pow2(e as nat)) == (-(mant as int)) * pow2(e as nat))
                by (nonlinear_arith);
            assert(n as int == parts_num(neg, mant, e));
            assert(parts_den(e) == 1);
            // Inside `2^61`, so nowhere near the `2^62 - 1` ceiling.
            assert(!saturated(n as int, 1int)) by (nonlinear_arith)
                requires
                    abs_int(n as int) <= pow2(61),
                    max_mag() == pow2(62) - 1,
                    pow2(62) == 2 * pow2(61),
                    pow2(61) > 0,
            ;
            lemma_r2_r3_directed(n as int, 1int, dir);
        }
        Some(round_frac_exec(n, 1, dir))
    } else if e >= -124 {
        let s: u32 = (0 - e) as u32;
        let d: i128 = pow2_i128(s);
        let n: i128 = if neg {
            0 - (mant as i128)
        } else {
            mant as i128
        };
        proof {
            // d == 2^s with s <= 124, which is exactly the denominator bound
            // `round_frac_exec` asks for. Also, |n| <= 2^53 is far below the
            // numerator bound.
            lemma_pow2_mono(s as nat, 124nat);
            lemma_pow2_124();
            lemma_pow2_126();
            lemma_pow2_pos(s as nat);
            assert(n as int == parts_num(neg, mant, e));
            assert(d as int == parts_den(e));
            // `|n| <= 2^53 <= max_mag <= max_mag · d`, since `d >= 1`. The
            // proof runs on the literals. The mantissa bound is already a
            // literal, so there is no `pow2(53)` to pin.
            assert(abs_int(n as int) <= max_mag() * (d as int)) by (nonlinear_arith)
                requires
                    abs_int(n as int) <= 9007199254740992int,
                    max_mag() == pow2(62) - 1,
                    pow2(62) == 4611686018427387904int,
                    d as int >= 1,
            ;
            lemma_r2_r3_directed(n as int, d as int, dir);
        }
        Some(round_frac_exec(n, d, dir))
    } else {
        // |v| <= 2^53 · 2^-125 == 2^-72, strictly inside the first grid cell of
        // width 2^-61. `round_frac` therefore lands on that cell's endpoint.
        // `tiny` returns that endpoint, by `lemma_round_frac_subgrid`.
        proof {
            // `s` is ghost-only here. This branch computes nothing. It only
            // shows that `tiny` returns the value `round_frac` produces.
            let s = (-e) as nat;
            let n = parts_num(neg, mant, e);
            let d = parts_den(e);
            assert(d == pow2(s));
            lemma_pow2_pos(s);
            lemma_pow2_mono(125nat, s);
            lemma_pow2_125();
            // |n|·2^62 <= 2^53 · 2^62 == 2^115 < 2^125 <= d. The proof runs on
            // the literals rather than through a `pow2(53) + pow2(62)`
            // addition lemma. `2^53` is already a literal here, as the
            // mantissa bound in the precondition, and `2^62`/`2^125` are
            // pinned. Nothing remains to add.
            assert(abs_int(n) * pow2(62) <= 9007199254740992int
                * 4611686018427387904int) by (nonlinear_arith)
                requires
                    abs_int(n) <= 9007199254740992int,
                    pow2(62) == 4611686018427387904int,
            ;
            assert(abs_int(n) * pow2(62) < d) by (nonlinear_arith)
                requires
                    abs_int(n) * pow2(62) <= 9007199254740992int * 4611686018427387904int,
                    pow2(125) == 42535295865117307932921825928971026432int,
                    pow2(125) <= d,
            ;
            assert(abs_int(n) >= 1);
            assert(n != 0);
            assert((n > 0) == !neg);
            // `magnitude_fits`, and hence `!saturated`, comes back out of the
            // subgrid lemma. That lemma cannot reach `round_frac` without a
            // proof of `magnitude_fits` first. A re-derivation here duplicates
            // the same `nonlinear_arith` block in a second file.
            lemma_round_frac_subgrid(n, d, dir);
            lemma_r2_r3_directed(n, d, dir);
        }
        Some(tiny(neg, dir))
    }
}

/// The result for a value whose magnitude is strictly below `2^-62`: the
/// correct endpoint of the first dyadic cell.
///
/// The postcondition pins the result to `round::subgrid_endpoint`.
/// `round::lemma_round_frac_subgrid` proves that this endpoint is the value
/// `round_frac` produces. That equality lets `from_parts_dir` state one
/// postcondition covering this branch as well as the two branches that go
/// through the rounder.
///
/// This function builds the pair directly rather than through `Rat::new`.
/// `Rat::new` returns an `Option` and needs a canonical-form uniqueness argument
/// to recover the exact representation from `q_is`. `gcd(1, 2^61) == 1` is a
/// one-line discharge of I1, and nothing remains to reduce.
pub fn tiny(neg: bool, dir: Dir) -> (r: Rat)
    ensures
        r.wf(),
        r == crate::round::subgrid_endpoint(!neg, dir),
{
    let eps_den: i64 = 2305843009213693952;  // 2^61
    proof {
        lemma_max_mag_pow2();
        lemma_pow2_61();
        lemma_pow2_62();
        // I1 for the two endpoints: `gcd(±1, 2^61)` is between 1 and 1.
        crate::gcd::lemma_gcd_pos(1nat, 2305843009213693952nat);
        crate::gcd::lemma_gcd_le(1nat, 2305843009213693952nat);
    }
    match dir {
        Dir::Nearest => Rat::zero(),
        Dir::Down => {
            if neg {
                Rat { num: -1, den: eps_den }
            } else {
                Rat::zero()
            }
        },
        Dir::Up => {
            if neg {
                Rat::zero()
            } else {
                Rat { num: 1, den: eps_den }
            }
        },
    }
}

/// Convert a `Rat` to the nearest `f64`.
///
/// **TRUSTED** (`external_body`), and **display/DTO only**. This function hands
/// a number to a JSON encoder. A Verus proof of its float rounding therefore
/// costs more effort than it returns. The result must not return into `Rat`
/// arithmetic.
///
/// Accuracy: three roundings occur (numerator, denominator, quotient). The
/// result is therefore within about `3·2^-53` relative of the true value. The
/// differential test suite pins this at 4 ulp against `malachite-q`.
#[verifier::external_body]
pub fn to_f64(q: Rat) -> f64 {
    (q.num as f64) / (q.den as f64)
}

} // verus!

// ---------------------------------------------------------------------------
// Display and serde. Outside the verified region, thin and total.
// ---------------------------------------------------------------------------

#[cfg_attr(verus_keep_ghost, verifier::external)]
impl core::fmt::Display for Rat {
    /// `"num/den"`, always in canonical form. The string is thus a faithful and
    /// unambiguous rendering of the value.
    fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
        write!(f, "{}/{}", self.num, self.den)
    }
}

/// Serialise as the `(num, den)` integer pair.
///
/// This round-trips **exactly**, which no `f64` encoding does. The
/// deserialiser re-canonicalises through [`Rat::new`]. A hand-written or
/// corrupted payload therefore produces an error instead of a `Rat` that
/// violates the type invariant.
#[cfg(feature = "serde")]
#[cfg_attr(verus_keep_ghost, verifier::external)]
impl serde::Serialize for Rat {
    fn serialize<S: serde::Serializer>(&self, s: S) -> Result<S::Ok, S::Error> {
        use serde::ser::SerializeTuple;
        let mut t = s.serialize_tuple(2)?;
        t.serialize_element(&self.num)?;
        t.serialize_element(&self.den)?;
        t.end()
    }
}

#[cfg(feature = "serde")]
#[cfg_attr(verus_keep_ghost, verifier::external)]
impl<'de> serde::Deserialize<'de> for Rat {
    fn deserialize<D: serde::Deserializer<'de>>(d: D) -> Result<Rat, D::Error> {
        use serde::de::Error;
        let (num, den) = <(i64, i64) as serde::Deserialize>::deserialize(d)?;
        Rat::new(num, den).ok_or_else(|| {
            D::Error::custom("the-q: (num, den) pair is not a representable rational")
        })
    }
}

// ---------------------------------------------------------------------------
// The extended `Q`: Display, FromStr and serde (issue #26 §8)
//
// All three share one spelling, rather than two spellings that can drift:
//
//     nan   inf   -inf   >max   <-max
//
// The saturation spellings are not readable as numbers. A numeral for `PosSat`
// is wrong in either direction. The value is finite, so `inf` is wrong. The
// value is also unknown, so `4611686018427387903` is worse: it claims an exact
// value that the type explicitly does not have.
// ---------------------------------------------------------------------------

/// The spelling of `Q::PosSat` in `Display`, `FromStr` and serde.
const POS_SAT_STR: &str = ">max";
/// The spelling of `Q::NegSat`.
const NEG_SAT_STR: &str = "<-max";
/// The spelling of `Q::PosInf`.
const POS_INF_STR: &str = "inf";
/// The spelling of `Q::NegInf`.
const NEG_INF_STR: &str = "-inf";
/// The spelling of `Q::Nan`.
const NAN_STR: &str = "nan";

#[cfg_attr(verus_keep_ghost, verifier::external)]
impl core::fmt::Display for crate::ext::Q {
    /// `"num/den"` for a number, and the fixed spelling above for each special.
    ///
    /// Every output round-trips through [`FromStr`](core::str::FromStr).
    fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
        match self {
            crate::ext::Q::Number(x) => write!(f, "{}", x),
            crate::ext::Q::PosSat => f.write_str(POS_SAT_STR),
            crate::ext::Q::NegSat => f.write_str(NEG_SAT_STR),
            crate::ext::Q::PosInf => f.write_str(POS_INF_STR),
            crate::ext::Q::NegInf => f.write_str(NEG_INF_STR),
            crate::ext::Q::Nan => f.write_str(NAN_STR),
        }
    }
}

/// Why a string could not be parsed as a [`Q`](crate::ext::Q).
#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
pub enum ParseQError {
    /// The input matched no special spelling and was not of the form
    /// `int` or `int/int`.
    Malformed,
    /// A numeral did not fit an `i64`.
    IntOverflow,
    /// The denominator was zero.
    ///
    /// The parser rejects this input rather than maps it to a special.
    /// `Q::new(1, 0)` is `PosInf`, because *a computation* divides by zero and
    /// the result must be some value. In an input stream, `"1/0"` is instead a
    /// malformed numeral, and silent acceptance hides the typo that produces
    /// it. `Display` never emits a zero denominator, so the rejection costs no
    /// round-trip.
    ZeroDenominator,
    /// The pair does not reduce to a value inside the width budget.
    OutOfBudget,
}

#[cfg_attr(verus_keep_ghost, verifier::external)]
impl core::fmt::Display for ParseQError {
    fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
        f.write_str(match self {
            ParseQError::Malformed => "the-q: not a rational or a recognised special",
            ParseQError::IntOverflow => "the-q: numeral does not fit an i64",
            ParseQError::ZeroDenominator => "the-q: denominator is zero",
            ParseQError::OutOfBudget => "the-q: value is outside the width budget",
        })
    }
}

impl std::error::Error for ParseQError {}

#[cfg_attr(verus_keep_ghost, verifier::external)]
impl core::str::FromStr for crate::ext::Q {
    type Err = ParseQError;

    /// Parses every spelling [`Display`](core::fmt::Display) produces. The
    /// round-trip is therefore total over all six states.
    ///
    /// The specials match **case-insensitively**, as `f64::from_str` does. IEEE
    /// 754 is this type's reference model, and acceptance of `"NaN"` alongside
    /// `"nan"` costs nothing. Surrounding whitespace is **rejected**, as
    /// `i64::from_str` rejects it. A parser that silently trims also silently
    /// accepts `"1 / 2"` in a data file.
    ///
    /// A bare integer (`"5"`) is accepted as well as a ratio (`"5/1"`). The
    /// bare form is unambiguous, and it is the human spelling.
    fn from_str(s: &str) -> Result<Self, ParseQError> {
        use crate::ext::Q;

        if s.eq_ignore_ascii_case(NAN_STR) {
            return Ok(Q::Nan);
        }
        if s.eq_ignore_ascii_case(POS_INF_STR) {
            return Ok(Q::PosInf);
        }
        if s.eq_ignore_ascii_case(NEG_INF_STR) {
            return Ok(Q::NegInf);
        }
        // The saturation spellings contain no letters, so the case-insensitive
        // comparison is only for uniformity of treatment.
        if s.eq_ignore_ascii_case(POS_SAT_STR) {
            return Ok(Q::PosSat);
        }
        if s.eq_ignore_ascii_case(NEG_SAT_STR) {
            return Ok(Q::NegSat);
        }

        let (num_str, den_str) = match s.split_once('/') {
            Some((n, d)) => (n, d),
            None => (s, "1"),
        };
        // `split_once` on `"//"` yields `("", "/")`, and on `"1/2/3"` yields
        // `("1", "2/3")`. Both inputs fail here, which is the intent.
        let num: i64 = parse_i64(num_str)?;
        let den: i64 = parse_i64(den_str)?;
        if den == 0 {
            return Err(ParseQError::ZeroDenominator);
        }
        match crate::types::Rat::new(num, den) {
            Some(x) => Ok(Q::Number(x)),
            None => Err(ParseQError::OutOfBudget),
        }
    }
}

/// `i64::from_str`, with the overflow case distinguished from the malformed one.
///
/// The two cases stay separate. "The number is too big for this type" and "that
/// is not a number" call for different fixes. One combined error discards the
/// only information that distinguishes them.
///
/// The test is syntactic rather than a re-parse at a wider type. A re-parse as
/// `i128` misreports any well-formed numeral above `i128::MAX` as malformed. A
/// numeral is an optional sign followed by at least one ASCII digit. When the
/// input is a numeral and `i64` still rejects it, the only possible reason is
/// range.
#[cfg_attr(verus_keep_ghost, verifier::external)]
fn parse_i64(s: &str) -> Result<i64, ParseQError> {
    match s.parse::<i64>() {
        Ok(v) => Ok(v),
        Err(_) => {
            let digits = s.strip_prefix(['+', '-']).unwrap_or(s);
            if !digits.is_empty() && digits.bytes().all(|b| b.is_ascii_digit()) {
                Err(ParseQError::IntOverflow)
            } else {
                Err(ParseQError::Malformed)
            }
        }
    }
}

/// Serialise a number as the `(num, den)` pair and a special as its string.
///
/// This is the untagged shape from issue #26 §8, and it carries that section's
/// caveat: **it works only in self-describing formats.** The deserialiser asks
/// the format what kind of value comes next. Thus `bincode` and other
/// non-self-describing codecs fail at run time rather than at compile time.
/// Issue #26 §12 leaves the question "is a wire break acceptable?" open. If
/// non-self-describing formats must keep working, this shape becomes an
/// externally tagged representation, which breaks the existing `Rat` wire
/// format.
///
/// This shape leaves `Rat`'s own serde impl unchanged. A bare `Rat` still
/// round-trips exactly.
#[cfg(feature = "serde")]
#[cfg_attr(verus_keep_ghost, verifier::external)]
impl serde::Serialize for crate::ext::Q {
    fn serialize<S: serde::Serializer>(&self, s: S) -> Result<S::Ok, S::Error> {
        match self {
            crate::ext::Q::Number(x) => x.serialize(s),
            crate::ext::Q::PosSat => s.serialize_str(POS_SAT_STR),
            crate::ext::Q::NegSat => s.serialize_str(NEG_SAT_STR),
            crate::ext::Q::PosInf => s.serialize_str(POS_INF_STR),
            crate::ext::Q::NegInf => s.serialize_str(NEG_INF_STR),
            crate::ext::Q::Nan => s.serialize_str(NAN_STR),
        }
    }
}

#[cfg(feature = "serde")]
#[cfg_attr(verus_keep_ghost, verifier::external)]
impl<'de> serde::Deserialize<'de> for crate::ext::Q {
    fn deserialize<D: serde::Deserializer<'de>>(d: D) -> Result<Self, D::Error> {
        struct V;

        impl<'de> serde::de::Visitor<'de> for V {
            type Value = crate::ext::Q;

            fn expecting(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
                f.write_str(
                    "a [num, den] pair or one of \"nan\", \"inf\", \"-inf\", \">max\", \"<-max\"",
                )
            }

            fn visit_str<E: serde::de::Error>(self, v: &str) -> Result<Self::Value, E> {
                use crate::ext::Q;
                // Exact match, not the case-insensitive `FromStr` spelling. A
                // wire format is machine-written. A case variant therefore
                // means an encoder disagrees with this one. The mismatch is
                // caught rather than absorbed.
                match v {
                    NAN_STR => Ok(Q::Nan),
                    POS_INF_STR => Ok(Q::PosInf),
                    NEG_INF_STR => Ok(Q::NegInf),
                    POS_SAT_STR => Ok(Q::PosSat),
                    NEG_SAT_STR => Ok(Q::NegSat),
                    _ => Err(E::custom("the-q: unrecognised special-value string")),
                }
            }

            fn visit_seq<A: serde::de::SeqAccess<'de>>(
                self,
                mut seq: A,
            ) -> Result<Self::Value, A::Error> {
                use serde::de::Error;
                let num: i64 = seq
                    .next_element()?
                    .ok_or_else(|| A::Error::custom("the-q: missing numerator"))?;
                let den: i64 = seq
                    .next_element()?
                    .ok_or_else(|| A::Error::custom("the-q: missing denominator"))?;
                if seq.next_element::<serde::de::IgnoredAny>()?.is_some() {
                    return Err(A::Error::custom("the-q: expected exactly two elements"));
                }
                // Re-canonicalises through `Rat::new`, exactly as `Rat`'s own
                // deserialiser does, so `[2, 4]` is accepted as `1/2`. A
                // payload that does not canonicalise is an error rather than a
                // saturation. On the wire, an unrepresentable pair means the
                // producer and this type disagree, and the error surfaces that
                // disagreement.
                crate::types::Rat::new(num, den)
                    .map(crate::ext::Q::Number)
                    .ok_or_else(|| {
                        A::Error::custom("the-q: (num, den) pair is not a representable rational")
                    })
            }
        }

        // `deserialize_any` is what confines this to self-describing formats.
        d.deserialize_any(V)
    }
}

// ---------------------------------------------------------------------------
// The f64 boundary for the extended type (issue #26 §8)
// ---------------------------------------------------------------------------

/// An `f64` as an extended `Q`, **total**.
///
/// This function claims the win §8 describes. [`from_f64_dir`] maps `NaN` and
/// both infinities to `None`, because `Rat` has nowhere to put them. The enum
/// does have a place for them, and the mapping is forced rather than chosen:
/// `f64::NAN → Nan`, `±f64::INFINITY → ±Inf`. Every `f64` therefore has an
/// image.
///
/// A finite `f64` outside the width budget saturates by sign. The only reason a
/// result is not a `Number` is thus a genuine non-representability, never a
/// missing case.
///
/// # Why there is no `to_f64` for this type
///
/// §8 omits it on purpose. `PosSat → f64::INFINITY` is wrong, because the value
/// is finite. `PosSat → 4.6e18` is worse, because it claims an exact magnitude
/// that the state explicitly does not have. `to_f64` stays defined only on
/// [`Rat`], where every value has a real answer.
///
/// # Trusted surface
///
/// This function uses the `f64` classification predicates (`is_nan`,
/// `is_infinite`, `is_sign_negative`), and Verus does not model them. The
/// function therefore sits outside the verified region alongside
/// [`f64_decompose`] and [`to_f64`]. It adds no new *numeric* assumption. The
/// value path still goes through `from_f64_dir`. This function contributes only
/// the three-way split on classes whose meaning IEEE-754 fixes unambiguously.
#[cfg_attr(verus_keep_ghost, verifier::external)]
pub fn q_from_f64(v: f64) -> crate::ext::Q {
    use crate::ext::Q;
    if v.is_nan() {
        return Q::Nan;
    }
    if v.is_infinite() {
        return if v.is_sign_negative() {
            Q::NegInf
        } else {
            Q::PosInf
        };
    }
    match from_f64_dir(v, crate::types::Dir::Nearest) {
        Some(x) => Q::Number(x),
        // Finite but outside the budget: saturate by sign rather than fail.
        // `v` is finite and non-representable, so it is genuinely large.
        None => {
            if v.is_sign_negative() {
                Q::NegSat
            } else {
                Q::PosSat
            }
        }
    }
}