the_q/exact.rs
1//! [`Exact`], a [`Rat`] wrapper whose arithmetic only ever returns a value
2//! that equals the true, unrounded result — or reports that it cannot.
3//!
4//! The Exact(Rat) is intended to be the most helpful and easy interface.
5//!
6//! `Rat::add`/`sub`/`mul`/`div` round silently once the exact result no
7//! longer fits the budget. On the exact path (no rounding at any step),
8//! `add` and `mul` are proven associative and distributive, and `add`/`mul`
9//! (with a nonnegative second factor) are proven monotone (`src/laws.rs`);
10//! off that path none of the three is guaranteed in general (`README.md`).
11//! `Exact` turns "did this operation leave the exact path?" into an explicit
12//! failure instead of a silent, unguaranteed answer, and the theorems below
13//! recover each property whenever every operation involved succeeded. Each
14//! theorem is one-directional: success of every step is sufficient, not
15//! claimed necessary — a computation that left the exact path could still
16//! happen to satisfy the same equation or inequality.
17//!
18//! ```
19//! use the_q::{Exact, ExactError, Rat};
20//!
21//! let half = Exact::new(Rat::new(1, 2).unwrap());
22//! let one = Exact::add(half, half).expect("1/2 + 1/2 is exact");
23//! assert_eq!(one.value(), Rat::new(1, 1).unwrap());
24//!
25//! // A sum whose reduced denominator would exceed the budget fails instead
26//! // of rounding silently.
27//! let a = Exact::new(Rat::new(1, 3_037_000_493).unwrap());
28//! let b = Exact::new(Rat::new(1, 3_037_000_499).unwrap());
29//! assert_eq!(Exact::add(a, b), Err(ExactError::Inexact));
30//!
31//! // A chain that stays on the exact path the whole way is genuinely
32//! // associative -- not approximately, exactly equal.
33//! let (x, y, z) = (
34//! Exact::new(Rat::new(1, 2).unwrap()),
35//! Exact::new(Rat::new(1, 3).unwrap()),
36//! Exact::new(Rat::new(1, 6).unwrap()),
37//! );
38//! let left = Exact::add(Exact::add(x, y).unwrap(), z).unwrap();
39//! let right = Exact::add(x, Exact::add(y, z).unwrap()).unwrap();
40//! assert_eq!(left.value(), right.value());
41//! ```
42
43use verus_builtin_macros::verus;
44
45#[allow(unused_imports)]
46use verus_builtin::*;
47#[allow(unused_imports)]
48use vstd::prelude::*;
49
50#[allow(unused_imports)]
51use crate::model::*;
52#[allow(unused_imports)]
53use crate::q::*;
54#[allow(unused_imports)]
55use crate::round::*;
56use crate::types::Rat;
57
58verus! {
59
60/// A [`Rat`] wrapper whose `add`/`sub`/`mul`/`div` succeed only when the
61/// result needs no rounding.
62///
63/// ```compile_fail
64/// use the_q::{Exact, Rat};
65/// let _ = Exact { value: Rat::one() };
66/// ```
67///
68/// ```compile_fail
69/// use the_q::{Exact, Rat};
70/// let mut e = Exact::new(Rat::one());
71/// e.value = Rat::zero();
72/// ```
73#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
74pub struct Exact {
75 pub(crate) value: Rat,
76}
77
78impl Exact {
79 /// The wrapped value, in specifications.
80 pub closed spec fn spec_value(self) -> Rat {
81 self.value
82 }
83
84 /// The type invariant: the wrapped [`Rat`] is well-formed. `Exact` adds
85 /// no invariant of its own; exactness is a property of *operations*, not
86 /// of a value in isolation.
87 pub open spec fn wf(self) -> bool {
88 self.spec_value().wf()
89 }
90
91 /// `r` denotes the exact sum `a + b`.
92 pub open spec fn spec_is_sum(r: Exact, a: Exact, b: Exact) -> bool {
93 q_is(r.spec_value(), add_n(a.spec_value(), b.spec_value()), prod_d(a.spec_value(), b.spec_value()))
94 }
95
96 /// `r` denotes the exact difference `a - b`.
97 pub open spec fn spec_is_difference(r: Exact, a: Exact, b: Exact) -> bool {
98 q_is(r.spec_value(), sub_n(a.spec_value(), b.spec_value()), prod_d(a.spec_value(), b.spec_value()))
99 }
100
101 /// `r` denotes the exact product `a * b`.
102 pub open spec fn spec_is_product(r: Exact, a: Exact, b: Exact) -> bool {
103 q_is(r.spec_value(), mul_n(a.spec_value(), b.spec_value()), prod_d(a.spec_value(), b.spec_value()))
104 }
105
106 /// `r` denotes the exact quotient `a / b`.
107 pub open spec fn spec_is_quotient(r: Exact, a: Exact, b: Exact) -> bool {
108 q_is(r.spec_value(), div_n(a.spec_value(), b.spec_value()), div_d(a.spec_value(), b.spec_value()))
109 }
110
111 /// Two `Exact` wrapping the same value are the same value.
112 pub proof fn lemma_extensional(a: Exact, b: Exact)
113 requires
114 a.spec_value() == b.spec_value(),
115 ensures
116 a == b,
117 {
118 reveal(Exact::spec_value);
119 }
120
121 /// Wraps an already-computed [`Rat`]. Always exact: it denotes itself.
122 ///
123 /// ```
124 /// use the_q::{Exact, Rat};
125 ///
126 /// let half = Exact::new(Rat::new(1, 2).unwrap());
127 /// assert_eq!(half.value(), Rat::new(1, 2).unwrap());
128 /// ```
129 pub fn new(value: Rat) -> (r: Exact)
130 requires
131 value.wf(),
132 ensures
133 r.wf(),
134 r.spec_value() == value,
135 {
136 Exact { value }
137 }
138
139 /// The wrapped value.
140 ///
141 /// ```
142 /// use the_q::{Exact, Rat};
143 ///
144 /// let e = Exact::new(Rat::new(3, 4).unwrap());
145 /// assert_eq!(e.value(), Rat::new(3, 4).unwrap());
146 /// ```
147 pub fn value(&self) -> (r: Rat)
148 ensures
149 r == self.spec_value(),
150 {
151 proof {
152 reveal(Exact::spec_value);
153 }
154 self.value
155 }
156
157 /// Whether the wrapped value is nonnegative.
158 ///
159 /// ```
160 /// use the_q::{Exact, Rat};
161 ///
162 /// assert!(Exact::new(Rat::new(1, 2).unwrap()).is_nonneg());
163 /// assert!(Exact::new(Rat::zero()).is_nonneg());
164 /// assert!(!Exact::new(Rat::new(-1, 2).unwrap()).is_nonneg());
165 /// ```
166 pub fn is_nonneg(&self) -> (r: bool)
167 requires
168 self.wf(),
169 ensures
170 r <==> self.spec_value().n() >= 0,
171 {
172 proof {
173 reveal(Exact::spec_value);
174 }
175 self.value.numerator() >= 0
176 }
177
178 /// `a <= b`.
179 ///
180 /// ```
181 /// use the_q::{Exact, Rat};
182 ///
183 /// let a = Exact::new(Rat::new(1, 3).unwrap());
184 /// let b = Exact::new(Rat::new(1, 2).unwrap());
185 /// assert!(Exact::le(a, b));
186 /// assert!(!Exact::le(b, a));
187 /// assert!(Exact::le(a, a));
188 /// ```
189 pub fn le(a: Exact, b: Exact) -> (r: bool)
190 requires
191 a.wf(),
192 b.wf(),
193 ensures
194 r <==> q_le(a.spec_value(), b.spec_value()),
195 {
196 proof {
197 reveal(Exact::spec_value);
198 }
199 Rat::le(a.value, b.value)
200 }
201
202 /// `a + b`, or `None` if the exact sum needs rounding.
203 ///
204 /// ```
205 /// use the_q::{Exact, Rat};
206 ///
207 /// let half = Exact::new(Rat::new(1, 2).unwrap());
208 /// let sum = Exact::checked_add(half, half).expect("1/2 + 1/2 is exact");
209 /// assert_eq!(sum.value(), Rat::new(1, 1).unwrap());
210 ///
211 /// // The reduced denominator of this sum is about 9.2e18, past the
212 /// // budget -- `None`, not a silently rounded answer.
213 /// let a = Exact::new(Rat::new(1, 3_037_000_493).unwrap());
214 /// let b = Exact::new(Rat::new(1, 3_037_000_499).unwrap());
215 /// assert_eq!(Exact::checked_add(a, b), None);
216 /// ```
217 pub fn checked_add(a: Exact, b: Exact) -> (r: Option<Exact>)
218 requires
219 a.wf(),
220 b.wf(),
221 ensures
222 r.is_some() <==> exact_path(
223 add_n(a.spec_value(), b.spec_value()),
224 prod_d(a.spec_value(), b.spec_value()),
225 ),
226 r.is_some() ==> r.unwrap().wf(),
227 r.is_some() ==> Exact::spec_is_sum(r.unwrap(), a, b),
228 {
229 proof {
230 reveal(Exact::spec_value);
231 lemma_op_widths(a.value, b.value);
232 crate::model::lemma_pow2_126();
233 }
234 if crate::round::exact_path_exec(add_n_exec(a.value, b.value), prod_d_exec(a.value, b.value)) {
235 Some(Exact { value: Rat::add(a.value, b.value) })
236 } else {
237 None
238 }
239 }
240
241 /// `a - b`, or `None` if the exact difference needs rounding.
242 ///
243 /// ```
244 /// use the_q::{Exact, Rat};
245 ///
246 /// let a = Exact::new(Rat::new(3, 4).unwrap());
247 /// let b = Exact::new(Rat::new(1, 4).unwrap());
248 /// let diff = Exact::checked_sub(a, b).expect("3/4 - 1/4 is exact");
249 /// assert_eq!(diff.value(), Rat::new(1, 2).unwrap());
250 /// ```
251 pub fn checked_sub(a: Exact, b: Exact) -> (r: Option<Exact>)
252 requires
253 a.wf(),
254 b.wf(),
255 ensures
256 r.is_some() <==> exact_path(
257 sub_n(a.spec_value(), b.spec_value()),
258 prod_d(a.spec_value(), b.spec_value()),
259 ),
260 r.is_some() ==> r.unwrap().wf(),
261 r.is_some() ==> Exact::spec_is_difference(r.unwrap(), a, b),
262 {
263 proof {
264 reveal(Exact::spec_value);
265 lemma_op_widths(a.value, b.value);
266 crate::model::lemma_pow2_126();
267 }
268 if crate::round::exact_path_exec(sub_n_exec(a.value, b.value), prod_d_exec(a.value, b.value)) {
269 Some(Exact { value: Rat::sub(a.value, b.value) })
270 } else {
271 None
272 }
273 }
274
275 /// `a * b`, or `None` if the exact product needs rounding.
276 ///
277 /// ```
278 /// use the_q::{Exact, Rat};
279 ///
280 /// let a = Exact::new(Rat::new(2, 3).unwrap());
281 /// let b = Exact::new(Rat::new(3, 4).unwrap());
282 /// let product = Exact::checked_mul(a, b).expect("(2/3) * (3/4) is exact");
283 /// assert_eq!(product.value(), Rat::new(1, 2).unwrap());
284 /// ```
285 pub fn checked_mul(a: Exact, b: Exact) -> (r: Option<Exact>)
286 requires
287 a.wf(),
288 b.wf(),
289 ensures
290 r.is_some() <==> exact_path(
291 mul_n(a.spec_value(), b.spec_value()),
292 prod_d(a.spec_value(), b.spec_value()),
293 ),
294 r.is_some() ==> r.unwrap().wf(),
295 r.is_some() ==> Exact::spec_is_product(r.unwrap(), a, b),
296 {
297 proof {
298 reveal(Exact::spec_value);
299 lemma_op_widths(a.value, b.value);
300 crate::model::lemma_pow2_126();
301 }
302 if crate::round::exact_path_exec(mul_n_exec(a.value, b.value), prod_d_exec(a.value, b.value)) {
303 Some(Exact { value: Rat::mul(a.value, b.value) })
304 } else {
305 None
306 }
307 }
308
309 /// `a / b`, or `None` if `b` is zero or the exact quotient needs rounding.
310 ///
311 /// ```
312 /// use the_q::{Exact, Rat};
313 ///
314 /// let a = Exact::new(Rat::new(1, 2).unwrap());
315 /// let b = Exact::new(Rat::new(1, 3).unwrap());
316 /// let quotient = Exact::checked_div(a, b).expect("(1/2) / (1/3) is exact");
317 /// assert_eq!(quotient.value(), Rat::new(3, 2).unwrap());
318 ///
319 /// // Division by zero is `None`, the same as any other operand that
320 /// // leaves the exact path -- `checked_div` does not distinguish the two
321 /// // causes (the `Result`-returning `div` does; see below).
322 /// assert_eq!(Exact::checked_div(a, Exact::new(Rat::zero())), None);
323 /// ```
324 pub fn checked_div(a: Exact, b: Exact) -> (r: Option<Exact>)
325 requires
326 a.wf(),
327 b.wf(),
328 ensures
329 b.spec_value().n() == 0 ==> r.is_none(),
330 b.spec_value().n() != 0 ==> (r.is_some() <==> exact_path(
331 div_n(a.spec_value(), b.spec_value()),
332 div_d(a.spec_value(), b.spec_value()),
333 )),
334 r.is_some() ==> b.spec_value().n() != 0,
335 r.is_some() ==> r.unwrap().wf(),
336 r.is_some() ==> Exact::spec_is_quotient(r.unwrap(), a, b),
337 {
338 proof {
339 reveal(Exact::spec_value);
340 }
341 if b.value.numerator() == 0 {
342 return None;
343 }
344 proof {
345 lemma_op_widths(a.value, b.value);
346 crate::model::lemma_pow2_126();
347 assert(b.value.n() > 0 ==> a.value.d() * b.value.n() > 0) by (nonlinear_arith)
348 requires
349 a.value.d() > 0,
350 ;
351 assert(b.value.n() < 0 ==> a.value.d() * b.value.n() < 0) by (nonlinear_arith)
352 requires
353 a.value.d() > 0,
354 ;
355 }
356 if crate::round::exact_path_exec(div_n_exec(a.value, b.value), div_d_exec(a.value, b.value)) {
357 Some(Exact { value: Rat::div(a.value, b.value) })
358 } else {
359 None
360 }
361 }
362}
363
364// ---------------------------------------------------------------------------
365// Theorems: associativity, distributivity, and monotonicity, each holding
366// whenever every `Exact` operation it names actually succeeded (sufficient,
367// not claimed necessary).
368// ---------------------------------------------------------------------------
369
370/// If `(a+b)+c` and `a+(b+c)` both succeeded exactly, they are equal.
371pub proof fn theorem_exact_add_associative(
372 a: Exact,
373 b: Exact,
374 c: Exact,
375 ab: Exact,
376 bc: Exact,
377 left: Exact,
378 right: Exact,
379)
380 requires
381 a.wf(),
382 b.wf(),
383 c.wf(),
384 ab.wf(),
385 bc.wf(),
386 left.wf(),
387 right.wf(),
388 Exact::spec_is_sum(ab, a, b),
389 Exact::spec_is_sum(bc, b, c),
390 Exact::spec_is_sum(left, ab, c),
391 Exact::spec_is_sum(right, a, bc),
392 ensures
393 left == right,
394{
395 crate::laws::lemma_add_assoc_exact_values(
396 a.spec_value(),
397 b.spec_value(),
398 c.spec_value(),
399 ab.spec_value(),
400 bc.spec_value(),
401 left.spec_value(),
402 right.spec_value(),
403 );
404 crate::laws::lemma_canonical_eq(left.spec_value(), right.spec_value());
405 Exact::lemma_extensional(left, right);
406}
407
408/// If `(a*b)*c` and `a*(b*c)` both succeeded exactly, they are equal.
409pub proof fn theorem_exact_mul_associative(
410 a: Exact,
411 b: Exact,
412 c: Exact,
413 ab: Exact,
414 bc: Exact,
415 left: Exact,
416 right: Exact,
417)
418 requires
419 a.wf(),
420 b.wf(),
421 c.wf(),
422 ab.wf(),
423 bc.wf(),
424 left.wf(),
425 right.wf(),
426 Exact::spec_is_product(ab, a, b),
427 Exact::spec_is_product(bc, b, c),
428 Exact::spec_is_product(left, ab, c),
429 Exact::spec_is_product(right, a, bc),
430 ensures
431 left == right,
432{
433 crate::laws::theorem_mul_associative_exact(
434 a.spec_value(),
435 b.spec_value(),
436 c.spec_value(),
437 ab.spec_value(),
438 bc.spec_value(),
439 left.spec_value(),
440 right.spec_value(),
441 );
442 crate::laws::lemma_canonical_eq(left.spec_value(), right.spec_value());
443 Exact::lemma_extensional(left, right);
444}
445
446/// If `bc = b+c`, `lhs = a*bc`, `ab = a*b`, `ac = a*c`, and `rhs = ab+ac` all
447/// succeeded exactly, then `lhs == rhs`: `a*(b+c) == a*b + a*c`.
448pub proof fn theorem_exact_distributive(
449 a: Exact,
450 b: Exact,
451 c: Exact,
452 bc: Exact,
453 lhs: Exact,
454 ab: Exact,
455 ac: Exact,
456 rhs: Exact,
457)
458 requires
459 a.wf(),
460 b.wf(),
461 c.wf(),
462 bc.wf(),
463 lhs.wf(),
464 ab.wf(),
465 ac.wf(),
466 rhs.wf(),
467 Exact::spec_is_sum(bc, b, c),
468 Exact::spec_is_product(lhs, a, bc),
469 Exact::spec_is_product(ab, a, b),
470 Exact::spec_is_product(ac, a, c),
471 Exact::spec_is_sum(rhs, ab, ac),
472 ensures
473 lhs == rhs,
474{
475 crate::laws::theorem_distributive_exact(
476 a.spec_value(),
477 b.spec_value(),
478 c.spec_value(),
479 bc.spec_value(),
480 lhs.spec_value(),
481 ab.spec_value(),
482 ac.spec_value(),
483 rhs.spec_value(),
484 );
485 crate::laws::lemma_canonical_eq(lhs.spec_value(), rhs.spec_value());
486 Exact::lemma_extensional(lhs, rhs);
487}
488
489/// If `a <= b` and `ac = a+c`, `bc = b+c` both succeeded exactly, then
490/// `ac <= bc`.
491pub proof fn theorem_exact_add_monotone(a: Exact, b: Exact, c: Exact, ac: Exact, bc: Exact)
492 requires
493 a.wf(),
494 b.wf(),
495 c.wf(),
496 ac.wf(),
497 bc.wf(),
498 q_le(a.spec_value(), b.spec_value()),
499 Exact::spec_is_sum(ac, a, c),
500 Exact::spec_is_sum(bc, b, c),
501 ensures
502 q_le(ac.spec_value(), bc.spec_value()),
503{
504 let av = a.spec_value();
505 let bv = b.spec_value();
506 let cv = c.spec_value();
507 let x = ac.spec_value();
508 let y = bc.spec_value();
509 crate::laws::theorem_add_monotone_exact(av, bv, cv);
510 crate::q::lemma_op_widths(av, cv);
511 crate::q::lemma_op_widths(bv, cv);
512 crate::interval::lemma_frac_chain_le(
513 x.n(),
514 x.d(),
515 add_n(av, cv),
516 prod_d(av, cv),
517 add_n(bv, cv),
518 prod_d(bv, cv),
519 y.n(),
520 y.d(),
521 );
522}
523
524/// If `a <= b`, `c >= 0`, and `ac = a*c`, `bc = b*c` both succeeded exactly,
525/// then `ac <= bc`.
526pub proof fn theorem_exact_mul_monotone_nonneg(a: Exact, b: Exact, c: Exact, ac: Exact, bc: Exact)
527 requires
528 a.wf(),
529 b.wf(),
530 c.wf(),
531 ac.wf(),
532 bc.wf(),
533 q_le(a.spec_value(), b.spec_value()),
534 c.spec_value().n() >= 0,
535 Exact::spec_is_product(ac, a, c),
536 Exact::spec_is_product(bc, b, c),
537 ensures
538 q_le(ac.spec_value(), bc.spec_value()),
539{
540 let av = a.spec_value();
541 let bv = b.spec_value();
542 let cv = c.spec_value();
543 let x = ac.spec_value();
544 let y = bc.spec_value();
545 crate::laws::theorem_mul_monotone_nonneg_exact(av, bv, cv);
546 crate::q::lemma_op_widths(av, cv);
547 crate::q::lemma_op_widths(bv, cv);
548 crate::interval::lemma_frac_chain_le(
549 x.n(),
550 x.d(),
551 mul_n(av, cv),
552 prod_d(av, cv),
553 mul_n(bv, cv),
554 prod_d(bv, cv),
555 y.n(),
556 y.d(),
557 );
558}
559
560} // verus!
561
562// ---------------------------------------------------------------------------
563// The ergonomic `Result` layer. Plain Rust, not proof-carrying: it only
564// re-packages the verified `checked_*` primitives above into a friendlier
565// error type, and (for `div`) checks the zero divisor before calling in so
566// the two failure causes are distinguishable.
567// ---------------------------------------------------------------------------
568
569/// Why an [`Exact`] operation could not return a value.
570#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
571pub enum ExactError {
572 /// The exact result does not fit the budget: it would have to round.
573 Inexact,
574 /// The divisor was zero.
575 DivisionByZero,
576}
577
578#[cfg_attr(verus_keep_ghost, verifier::external)]
579impl core::fmt::Display for ExactError {
580 fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
581 f.write_str(match self {
582 ExactError::Inexact => "the-q: exact result would need rounding",
583 ExactError::DivisionByZero => "the-q: division by zero",
584 })
585 }
586}
587
588#[cfg_attr(verus_keep_ghost, verifier::external)]
589impl std::error::Error for ExactError {}
590
591#[cfg_attr(verus_keep_ghost, verifier::external)]
592impl Exact {
593 /// `a + b`, or [`ExactError::Inexact`] if the exact sum needs rounding.
594 ///
595 /// ```
596 /// use the_q::{Exact, ExactError, Rat};
597 ///
598 /// let half = Exact::new(Rat::new(1, 2).unwrap());
599 /// assert_eq!(Exact::add(half, half).unwrap().value(), Rat::new(1, 1).unwrap());
600 ///
601 /// let a = Exact::new(Rat::new(1, 3_037_000_493).unwrap());
602 /// let b = Exact::new(Rat::new(1, 3_037_000_499).unwrap());
603 /// assert_eq!(Exact::add(a, b), Err(ExactError::Inexact));
604 /// ```
605 pub fn add(a: Exact, b: Exact) -> Result<Exact, ExactError> {
606 Exact::checked_add(a, b).ok_or(ExactError::Inexact)
607 }
608
609 /// `a - b`, or [`ExactError::Inexact`] if the exact difference needs
610 /// rounding.
611 ///
612 /// ```
613 /// use the_q::{Exact, Rat};
614 ///
615 /// let a = Exact::new(Rat::new(3, 4).unwrap());
616 /// let b = Exact::new(Rat::new(1, 4).unwrap());
617 /// assert_eq!(Exact::sub(a, b).unwrap().value(), Rat::new(1, 2).unwrap());
618 /// ```
619 pub fn sub(a: Exact, b: Exact) -> Result<Exact, ExactError> {
620 Exact::checked_sub(a, b).ok_or(ExactError::Inexact)
621 }
622
623 /// `a * b`, or [`ExactError::Inexact`] if the exact product needs
624 /// rounding.
625 ///
626 /// ```
627 /// use the_q::{Exact, Rat};
628 ///
629 /// let a = Exact::new(Rat::new(2, 3).unwrap());
630 /// let b = Exact::new(Rat::new(3, 4).unwrap());
631 /// assert_eq!(Exact::mul(a, b).unwrap().value(), Rat::new(1, 2).unwrap());
632 /// ```
633 pub fn mul(a: Exact, b: Exact) -> Result<Exact, ExactError> {
634 Exact::checked_mul(a, b).ok_or(ExactError::Inexact)
635 }
636
637 /// `a / b`, or [`ExactError::DivisionByZero`] / [`ExactError::Inexact`].
638 ///
639 /// ```
640 /// use the_q::{Exact, ExactError, Rat};
641 ///
642 /// let a = Exact::new(Rat::new(1, 2).unwrap());
643 /// let b = Exact::new(Rat::new(1, 3).unwrap());
644 /// assert_eq!(Exact::div(a, b).unwrap().value(), Rat::new(3, 2).unwrap());
645 ///
646 /// assert_eq!(
647 /// Exact::div(a, Exact::new(Rat::zero())),
648 /// Err(ExactError::DivisionByZero),
649 /// );
650 /// ```
651 pub fn div(a: Exact, b: Exact) -> Result<Exact, ExactError> {
652 if b.value().numerator() == 0 {
653 return Err(ExactError::DivisionByZero);
654 }
655 Exact::checked_div(a, b).ok_or(ExactError::Inexact)
656 }
657}