the_q/
types.rs

1//! The `Rat` value type, the rounding-direction enum, and the width budget.
2//!
3//! The representation is private to this module. Every public constructor
4//! establishes the invariant, every operation preserves it, and downstream
5//! callers inspect values through [`Rat::numerator`] and [`Rat::denominator`].
6
7use verus_builtin_macros::verus;
8
9#[allow(unused_imports)]
10use verus_builtin::*;
11#[allow(unused_imports)]
12use vstd::prelude::*;
13
14verus! {
15
16/// The magnitude budget, `2^62 − 1`: the largest under which
17/// `num1·den2 ± num2·den1 < 2^125` fits `i128`.
18pub const MAX_MAG: i64 = 4611686018427387903;  // 2^62 - 1
19
20/// The largest decimal exponent accepted by `crate::q::Rat::from_decimal`.
21///
22/// `10^18 < 2^62 - 1 <= 10^19`. Eighteen places is therefore the last count
23/// whose scale factor is itself representable.
24pub const MAX_DEC_PLACES: u8 = 18;
25
26/// The largest scale (digits after the point) a `rust_decimal::Decimal`
27/// carries. `crate::convert::from_decimal128_dir` accepts exactly the domain
28/// `Decimal` itself guarantees: `scale() <= MAX_DECIMAL_SCALE` and
29/// `|mantissa()| <= MAX_DECIMAL_MANTISSA`.
30pub const MAX_DECIMAL_SCALE: u32 = 28;
31
32/// `2^96 - 1`, the largest magnitude a `rust_decimal::Decimal` mantissa
33/// carries (a 96-bit unsigned integer with the sign held separately).
34pub const MAX_DECIMAL_MANTISSA: i128 = 79228162514264337593543950335;
35
36/// Rounding direction for the operations that can round.
37///
38/// `Down` and `Up` are *directed*: they bracket the exact value (R2). This
39/// bracketing lets [`crate::interval::QI`] be built without any new proofs.
40/// `Nearest` (ties to even) is the default for the plain operations.
41#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
42pub enum Dir {
43    /// Round toward `-inf`: the result is `<=` the exact value.
44    Down,
45    /// Round toward `+inf`: the result is `>=` the exact value.
46    Up,
47    /// Round to the nearest grid point; ties go to the even numerator.
48    Nearest,
49}
50
51/// A bounded rational `num / den`: canonical (`den > 0`, `gcd(|num|, den) == 1`)
52/// and bounded (`|num|, den <= MAX_MAG`), so structural equality is value
53/// equality and `Eq`/`Hash` derive safely. `Ord` is hand-written by
54/// cross-multiplication. The fields are private:
55///
56/// ```compile_fail
57/// use the_q::Rat;
58/// let _ = Rat { num: 1, den: 2 };
59/// ```
60///
61/// ```compile_fail
62/// use the_q::Rat;
63/// let mut r = Rat::one();
64/// r.den = 0;
65/// ```
66#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
67pub struct Rat {
68    /// The numerator. Coprime to `den`; `|num| <= MAX_MAG`.
69    num: i64,
70    /// The denominator. Strictly positive; `den <= MAX_MAG`.
71    den: i64,
72}
73
74impl Rat {
75    /// The numerator, as an unbounded integer.
76    pub closed spec fn n(self) -> int {
77        self.num as int
78    }
79
80    /// The denominator, as an unbounded integer.
81    pub closed spec fn d(self) -> int {
82        self.den as int
83    }
84
85    /// Ghost-only constructor used by public specifications. Its closed body
86    /// keeps the crate-private representation out of public open contracts.
87    pub closed spec fn from_raw_spec(num: i64, den: i64) -> Rat {
88        Rat { num, den }
89    }
90
91    /// Exposes the modeled components of [`Rat::from_raw_spec`] without
92    /// exposing the representation fields themselves.
93    pub proof fn lemma_from_raw_spec_components(num: i64, den: i64)
94        ensures
95            Rat::from_raw_spec(num, den).n() == num as int,
96            Rat::from_raw_spec(num, den).d() == den as int,
97    {
98        reveal(Rat::from_raw_spec);
99        reveal(Rat::n);
100        reveal(Rat::d);
101    }
102
103    /// Two rationals with identical abstract components are the same value.
104    pub proof fn lemma_extensional(a: Rat, b: Rat)
105        requires
106            a.n() == b.n(),
107            a.d() == b.d(),
108        ensures
109            a == b,
110    {
111        reveal(Rat::n);
112        reveal(Rat::d);
113    }
114
115    /// Internal representation constructor. Callers must establish any
116    /// well-formedness property required by their public contract.
117    pub(crate) fn from_raw_parts(num: i64, den: i64) -> (r: Rat)
118        ensures
119            r == Rat::from_raw_spec(num, den),
120            r.n() == num as int,
121            r.d() == den as int,
122    {
123        proof {
124            reveal(Rat::from_raw_spec);
125            reveal(Rat::n);
126            reveal(Rat::d);
127        }
128        Rat { num, den }
129    }
130
131    /// The numerator of the canonical representation. Always coprime to
132    /// [`Rat::denominator`].
133    ///
134    /// ```
135    /// use the_q::Rat;
136    ///
137    /// let r = Rat::new(-3, 6).unwrap();
138    /// assert_eq!(r.numerator(), -1);
139    /// assert_eq!(r.denominator(), 2);
140    /// ```
141    pub fn numerator(&self) -> (r: i64)
142        ensures r as int == self.n(),
143    {
144        self.num
145    }
146
147    /// The denominator of the canonical representation. Always `>= 1`.
148    ///
149    /// ```
150    /// use the_q::Rat;
151    ///
152    /// let r = Rat::new(3, 6).unwrap();
153    /// assert_eq!(r.denominator(), 2);
154    /// assert_eq!(Rat::one().denominator(), 1);
155    /// ```
156    pub fn denominator(&self) -> (r: i64)
157        ensures r as int == self.d(),
158    {
159        self.den
160    }
161}
162
163} // verus!
the_q/types.rs

the_q/
types.rs
