1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
//! # `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.
//!
//! ## 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`], 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.
// Verus's surface language does not accept compound-assignment operators or
// `RangeInclusive::contains` in exec code, and the inherent `Rat::add`/`Rat::mul`
// names are deliberate (the operator traits delegate to them and are not
// callable from verified code).
// Verus's macro machinery.
use verus_builtin as _;
use vstd as _;
pub use ;
pub use ;
pub use ;
pub use QI;
pub use ;