Crate the_q 

the-q — verified bounded rational arithmetic

Rat is num / den in two i64 fields, canonical (den > 0, gcd(|num|, den) == 1) and bounded (|num|, den <= 2^62 - 1). Arithmetic is exact when the exact result fits and rounded to a proven contract when it does not; every intermediate is i128 and cannot overflow.

use the_q::{Dir, Rat};

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

// Directed modes bracket the exact value.
let a = Rat::new(1, 3).unwrap();
assert!(Rat::le(Rat::mul_dir(a, a, Dir::Down), Rat::mul_dir(a, a, Dir::Up)));

Rat is partial: Rat::new(_, 0) is None, Rat::div(x, 0) panics, and an over-budget result saturates. Q makes each of those a value and is total: every operation on every input returns a Q and nothing panics.

use the_q::{Q, Rat};

assert_eq!(Q::div(Q::one(), Q::zero()), Q::PosInf);
assert_eq!(Q::div(Q::zero(), Q::zero()), Q::Nan);
assert_eq!(Q::checked_div(Q::one(), Q::zero()), None);

// Overflow is reported, and is distinct from division by zero.
let m = Q::Number(Rat::new(the_q::MAX_MAG, 1).unwrap());
let over = Q::add(m, m);
assert!(over.is_saturated() && !over.is_infinite());
assert_eq!(over.to_string(), ">max");

// Saturation denotes finite reals, so this is exact where `0 * inf` is not.
assert_eq!(Q::mul(Q::zero(), Q::PosSat), Q::zero());
assert_eq!(Q::mul(Q::zero(), Q::PosInf), Q::Nan);

// The order is total; `Nan` sorts last. Selection propagates `Nan`, so a
// fold of `Q::min` is not `iter().min()`.
let mut v = vec![Q::Nan, Q::PosInf, Q::zero(), Q::NegInf];
v.sort();
assert_eq!(v, vec![Q::NegInf, Q::zero(), Q::PosInf, Q::Nan]);
assert_eq!(Q::min(Q::Nan, Q::one()), Q::Nan);

Limits

• The rounding bound 2^-61 · max(1, |exact|) is absolute below 1.
• With rounding, add and mul are commutative but not associative; associativity holds on the exact path and the defect is bounded.
• Rounding is monotone on each grid, not across the representable/rounded boundary. README.md has the counterexample.
• Transcendentals are exact at rational points only where a proof says so: log2 at 2^k, log10 at 10^k (both signs), sqrt of a perfect square, exp(0), ln(1). cbrt(8) and exp2(3) are a hair off the integer, inside the measured bounds.
• Q is not a semiring: add/mul are commutative unconditionally, but associative, distributive and monotone only on the all-Number exact path — every failure past it has a counterexample in tests/q_laws.rs. Q::div(a, b) == Q::mul(a, Q::recip(b)) fails in six cells. See VERIFICATION.md’s V11 for what is proven instead: containment of the special-value propagation tables against an independent ghost model.

Verification and API stability

Proofs are in the source inside verus! blocks; cargo verus verify checks them, cargo build erases them. VERIFICATION.md maps the obligations, TRUSTED.md lists the three trusted functions.

Rat, Q, Dir, interval::QI, Exact, their operations and constructors, and nary follow semver. Other public items (gcd, model, round, lipschitz, fx, and executable helpers such as round::round_frac_exec_with_gcd) are public because Verus’s visibility rules require it and may change shape in patch releases.

Re-exports

pub use convert::ParseQError;

pub use convert::from_decimal128_dir;

pub use convert::from_decimal128_exact;

pub use convert::from_f64_dir;

pub use convert::from_ratio128_dir;

pub use convert::from_ratio128_exact;

pub use convert::q_from_f64;

pub use convert::to_f64;

pub use convert::exact_from_big_rational;

pub use convert::exact_from_num_rational_i64;

pub use convert::from_big_rational_dir;

pub use convert::from_big_rational_exact;

pub use convert::from_num_rational_i64_dir;

pub use convert::from_num_rational_i64_exact;

pub use convert::q_from_big_rational;

pub use convert::q_from_num_rational_i64;

pub use convert::exact_from_bigdecimal;

pub use convert::from_bigdecimal_dir;

pub use convert::from_bigdecimal_exact;

pub use convert::q_from_bigdecimal;

pub use convert::exact_from_bigint;

pub use convert::from_bigint_dir;

pub use convert::from_bigint_exact;

pub use convert::q_from_bigint;

pub use convert::exact_from_fixed;

pub use convert::from_fixed_dir;

pub use convert::from_fixed_exact;

pub use convert::q_from_fixed;

pub use convert::exact_from_rust_decimal;

pub use convert::from_rust_decimal_dir;

pub use convert::q_from_rust_decimal;

pub use exact::Exact;

pub use exact::ExactError;

pub use ext::Q;

pub use ext::Sign;

pub use interval::QI;

pub use types::Dir;

pub use types::MAX_DEC_PLACES;

pub use types::MAX_DECIMAL_MANTISSA;

pub use types::MAX_DECIMAL_SCALE;

pub use types::MAX_MAG;

pub use types::Rat;

Modules

convert

The crate’s edges: f64 in and out, Display, FromStr, serde.

denote

The true-value model behind issue #26 §2, and the containment obligation from issue #28: {x ⊕ y : x ∈ ⟦a⟧, y ∈ ⟦b⟧} ⊆ ⟦op(a, b)⟧ for every Q operation.

exact

Exact, a Rat wrapper whose arithmetic only ever returns a value that equals the true, unrounded result — or reports that it cannot.

ext

The extended Q: a Rat, or an explicit non-representable state.

fx

Fixed-point kernel for exp and ln.

gcd

Verified greatest common divisor (V5).

interval

QI, a closed rational interval on the directed rounding modes.

laws

Algebraic laws (V6).

laws_q

Algebraic laws for Q (issue #26 §5/§10.3, the V6 gap this crate’s laws never closed at the Q level: grep -n "Q::" src/laws.rs was empty before this file).

lipschitz

Error-propagation (Lipschitz) lemmas (V7), the layer under interval arithmetic and the accumulation bounds.

model

The ghost model Rat is specified against: spec/proof code only.

nary

N-ary helpers (V8): sum, product, weighted_mean.

q

The public Rat API: constructors, arithmetic, comparison, predicates.

round

The rounding contract R1–R4 (V4) and the single canonicalising entry point every arithmetic operation uses, round_frac_exec.

saturation

The scoping of the rounding contract at the magnitude ceiling, as one lemma.

soundness

Issue #28: the containment obligation for crate::ext::Q::add, proven against crate::denote’s ghost XR model, restricted to the special-value propagation cells — at least one operand is not a Number.

soundness_div

Issue #28: the containment obligation for crate::ext::Q::div, proven against crate::denote’s ghost XR model. Same scope discipline as soundness.rs/soundness_mul.rs: Number × Number is excluded (R1–R4’s job), including its zero-divisor sub-case.

soundness_mul

Issue #28: the containment obligation for crate::ext::Q::mul, proven against crate::denote’s ghost XR model. Same scope discipline as soundness.rs: Number × Number -> Number (or -> Sat) is excluded, governed instead by the already-proven rounding contract (R1–R4).

transcendental

Roots and transcendental functions on Q.

types

The Rat value type, the rounding-direction enum, and the width budget.