the-q

Bounded rational arithmetic with verified directed rounding, in Rust, proven in Verus.

use the_q::Rat;

let reliability = Rat::from_decimal(85, 2).unwrap();   // 0.85, exactly — 17/20
let weight      = Rat::from_decimal(3, 1).unwrap();    // 0.3,  exactly — 3/10
let combined    = Rat::mul(reliability, weight);       // 51/200, exactly
assert_eq!(combined.to_string(), "51/200");

Rat and Q

Rat is num / den in two i64 fields, always canonical (den > 0, gcd(|num|, den) == 1) and always bounded (|num|, den <= 2^62 − 1). It is Copy, 128 bits, no heap, Send + Sync. The fields are private; every Rat a caller can hold came from a constructor and satisfies the invariant.

Rat is exact whenever the exact result fits the budget and rounded when it does not. It is partial: Rat::new(_, 0) is None; Rat::div(x, 0) and Rat::zero().recip() panic (a precondition under Verus, a runtime check with a message for everyone else); and an exact result above the budget saturates to ±(2^62 − 1), which the checked_* variants report as None and the plain operations do not.

Q makes every one of those cases a value:

pub enum Q {
    Number(Rat),
    PosSat, NegSat,   // magnitude exceeds the budget; sign known
    PosInf, NegInf,   // exactly infinite
    Nan,              // no information
}

Every operation on Q — arithmetic, comparison, the folds, every root and transcendental — is total: it returns a value in the type and never panics.

use the_q::{Q, Rat, MAX_MAG};

assert_eq!(Q::div(Q::one(), Q::zero()), Q::PosInf);
assert_eq!(Q::div(Q::zero(), Q::zero()), Q::Nan);
let m = Q::Number(Rat::new(MAX_MAG, 1).unwrap());
assert!(Q::add(m, m).is_saturated());

Three deliberate choices, each different from IEEE 754:

• PosSat denotes the finite reals above the budget, not infinity. So Number(0) * PosSat == Number(0), and there is no is_finite().
• The order is total: Nan == Nan, and Nan sorts last. Q can be a map key. Outside Number the order is on representations, not values.
• min/max/clamp propagate Nan, so a fold of Q::min is not iter().min().

The rounding contract

When an exact result does not fit, it snaps to a dyadic grid chosen per magnitude: with k = bitlen(floor(|x|)), the grid step is 2^-(62-k), capped at 2^-61. Ties go to even. Proven, for every operation:

R3 is absolute below 1. A result near 1 carries ~61 significant bits; a result near 2^-40 carries ~21; below 2^-62 a value rounds to zero. This is the single most important thing to know before using the crate for small quantities, and it governs every accuracy figure below. If small values matter, scale the problem.

Limits

Not associative. add and mul are commutative with rounding. They are associative and distributive only on the exact path (no intermediate rounds), and that is proven. The general failure is bounded: |((a+b)+c) − (a+(b+c))| ≤ 4 · 2^-61 · m for any bound m ≥ 1 on the partial sums, and |((a·b)·c) − (a·(b·c))| ≤ 6 · 2^-61 on [0, 1].

Not globally monotone. R4 holds on each grid, not across the representable/rounded boundary. Counterexample (tests/adversarial.rs):

u = 2 / (2^61 + 1)              representable, returned exactly
v = u · (1 + 1/(2^62 − 2))      a hair larger, not representable
round_down(v) = 2^-61  <  u = round_down(u)       though u < v

The cause is that round has no single codomain: a representable input is returned from the whole bounded-denominator set, an unrepresentable one is snapped to the far coarser dyadic subgrid. Projection onto any one fixed set would be monotone. Fixing it means either always snapping, which discards exactness, or a Stern–Brocot floor onto the full set, which is the harder proof. The crate does neither; if you iterate a rounded projection to a fixed point, know this.

Saturation is a choice. Some exact results above 2^62 − 1 do have a Rat within 2^-61 (saturation::lemma_saturation_is_a_choice exhibits one). R3 is scoped below the ceiling to keep one clean boundary, and results above it saturate. Rat::new also returns None for an i64 pair that is already reduced but over budget; Rat::new_rounded is total in the numerator.

API

Constructors: zero, one, neg_one, from_int, new, new_rounded, from_decimal, convert::from_f64_dir.

Arithmetic: add, sub, mul, div (nearest, ties to even); *_dir (explicit direction); checked_* (None on saturation, and on a zero divisor for checked_div); neg, abs, recip, min, max, clamp (exact); pow_u32 (a fold of mul).

Comparison: compare, eq_q, lt, le, gt, ge, Ord/PartialOrd — exact, total. Predicates: is_zero, is_one, signum, in_unit_interval.

N-ary (nary): sum, product, weighted_mean — fixed left folds, so results are bit-reproducible across machines and threads.

Intervals (interval::QI): new (panics on lo > hi), checked_new, add, sub, mul, neg, hull, contains, width (rounded up; Q::PosSat when too wide to represent), checked_width. Enclosure is proven for every sign pattern.

Exact (exact::Exact): a Rat wrapper whose add, sub, mul, div succeed only when the result needs no rounding, returning Result<Exact, ExactError> (Inexact, or DivisionByZero for div) the moment it would leave that path — checked_* variants return Option instead. Unlike Rat::checked_*, which is None only on saturation, Exact's checked_* is None on any rounding, saturating or not. Associativity, distributivity, and monotonicity, absent in general once rounding happens (see Limits above), hold for a chain of Exact operations whenever every operation in the chain succeeded — sufficient, not claimed necessary (theorem_exact_add_associative, theorem_exact_mul_associative, theorem_exact_distributive, theorem_exact_add_monotone, theorem_exact_mul_monotone_nonneg).

Out: to_f64 (display only; see TRUSTED.md), Display (num/den), serde (feature-gated; encodes the exact pair).

Roots and transcendentals, on Q

sqrt, cbrt, hypot; exp, exp2, powf, pow_i32, ln, log2, log10, log; sin, cos, tan, asin, acos, atan, atan2; sinh, cosh, tanh; constants pi, e, ln2, ln10, half_pi. All total, all fixed-length series (termination is structural, cost is constant). They live on Q because none is rational-closed.

Domains: exp returns PosSat above x = 43.67 and 0 below −44; sin, cos, tan return Nan for |x| > 2^20; sqrt(PosSat) and ln(PosSat) are Nan because the image of the saturated region reaches back inside the budget.

Accuracy is measured, not proven. Two independent oracles were used — mpmath at 120 decimal digits, and exact rational series in Common Lisp carried to 2^-160 — and they agree with each other to better than 2^-98 on every function. Worst observed error over the sweeps (tests/transcendental.rs and scripts/accuracy/), in R3's own metric |got − true| / max(1, |true|):

Read the table with the R3 caveat above: these are absolute bounds below 1. asin(0.002) is 2^-53 relative; exp(−40) is 2^-3; exp(−44) is 0. tan near a pole inherits cos's absolute error divided by cos², so it is unbounded there. ln within 2^-8 of 1 keeps a small-denominator rational and is often far better than 2^-61 absolute, but not uniformly: 2^-52 relative at 1 ± 2^-24, 2^-124 at 1 ± 2^-60.

pi, e, ln2, ln10 are literals; each has a *_series derivation and a test that the two are bit-identical.

What is proven

1088 verified, 0 errors in CI; no assume, no admit; three external_body functions, enumerated in TRUSTED.md.

• V1 Every public operation preserves canonical form and the budget.
• V2 No panic, no overflow: every i128 intermediate is bounded. The 2^62 budget is exactly what makes cross-multiplied products fit.
• V3 Every result equals the exact rational model, stated division-free.
• V4 R1–R4 above, with the tighter nearest bound.
• V5 GCD correctness and termination.
• V6 Commutativity; exact-path associativity and distributivity; identity and involution laws; a total order agreeing with the value order.
• V7 Lipschitz bounds for add, mul, recip, div.
• V8 Accumulation bounds: sum and product within k · m · 2^-61 after k steps (product needs |factor| ≤ 1); weighted_mean's returned value within 8k · 2^-61 / δ when weights and values lie in [0, 1] and the exact weight sum is at least δ.
• V9 Q: totality, classification, total order, Nan absorption.
• V10 Transcendentals: totality and termination. isqrt is exactly the integer square root.
• The associativity bounds under Limits, interval enclosure, and the value pinning of every constructor including the f64 decomposition's integer core.

Not proven: the f64 decode/encode (trusted, tested); transcendental accuracy (measured, above); pow_u32's value (only its well-formedness); mul associativity outside [0, 1].

Testing

malachite-q is the oracle, as a dev-dependency only (scripts/check-no-lgpl.sh enforces this). tests/oracle.rs runs 20,000 random cases per operation per direction against R1–R3 plus every p/q with |p|, q ≤ 12; tests/bounds.rs checks R3's nearest bound, the weighted-mean bound and interval enclosure on random operands; tests/props.rs covers the invariant, the laws, and byte-identical results across eight threads; tests/adversarial.rs holds the budget edges and both counterexamples; tests/transcendental.rs carries the accuracy oracles. Overflow checks stay on in release.

Performance

cargo bench --bench arith: minimum of seven runs, overflow-checks = true. Linux 6.16 x86-64, rustc 1.96. The benchmark prints its own quality block; on this run control drift was 5.8% and the widest spread 137%, so treat the second digit as noise.

Those are exact-path costs. Rounding is the expensive path, and it is where the exact backend wins:

the-q plateaus once operands fill the budget; the exact backend grows without bound and is cheaper between roughly k = 8 and k = 2000. An 8-pair weighted_mean is 8.0 µs against 5.3 µs exact. Transcendentals: exp 0.6 µs, ln 1.5 µs, sqrt 11 µs, sin/cos 17–19 µs, atan 32 µs.

the-q is the right tool when memory must be flat, chains are long or unbounded, or the per-step error must be a proven number. For short exact computations use an exact rational; for speed use f64.

Verification

Specifications and proofs live in the source inside verus! blocks. cargo build compiles them with plain rustc; cargo verus verify checks them. VERIFICATION.md has the obligation map and reproduction steps; TRUSTED.md the three trusted functions; docs/SPEC.md the original specification with its six recorded departures.

Licence

Dual-licensed. Free under AGPL-3.0-or-later: use, modify, and redistribute freely, including as a network service, as long as you release your source under the same terms (AGPL-3.0-or-later section 13 — the network-use clause — applies to any service built on this crate, not only to redistributed binaries). If that obligation does not work for your use — most commercial and closed-source use — a separate commercial licence is available; contact the author for terms.

The LGPL-3.0-only oracle malachite-q is a dev-dependency only and never ships, so its terms do not apply to any release of this crate.