the-q 0.1.0

Verified bounded rational (Q) arithmetic with machine-checked directed rounding
Documentation 
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

//! The scoping of the rounding contract at the magnitude ceiling, as one lemma.
//!
//! R3 is stated under `!saturated(n, d)`: results above the ceiling saturate,
//! and `checked_*` reports them as `None`. The natural justification for that
//! scoping — that nothing representable is close enough up there, so the bound
//! is unachievable — is false. `lemma_saturation_is_a_choice` (no intra-doc
//! link: items inside `verus!` are not resolvable targets) exhibits a value
//! outside the ceiling that a well-formed `Rat` satisfies R3 for, so the strong
//! claim contradicts a machine-checked theorem rather than a comment.
//!
//! The module boundary is organisational, not load-bearing: the lemma verifies
//! cleanly from `model` under the pinned toolchain (issue #15), so it can be
//! folded back in.
//!
//! Excluding the region above the ceiling keeps R3 on one side of a clean
//! boundary and keeps `checked_*` honest. It is a choice, not a necessity.

use verus_builtin_macros::verus;

#[allow(unused_imports)]
use verus_builtin::*;
#[allow(unused_imports)]
use vstd::prelude::*;

#[allow(unused_imports)]
use crate::model::*;
#[allow(unused_imports)]
use crate::types::{MAX_MAG, Rat};

verus! {

/// Saturation is a **scoping choice, not a necessity**: there are values above
/// the magnitude ceiling that a well-formed `Rat` does satisfy R3 for.
///
/// The opposite claim — that nothing representable is close enough up there, so
/// the bound is unachievable — is false, and this lemma is the obligation that
/// contradicts it.
///
/// The witness is `n/d = MAX_MAG + 1/2` against `r = MAX_MAG/1`: the error is
/// exactly `1/2`, and R3 at this magnitude allows nearly `2`.
///
/// This is not an argument for widening the contract. Excluding the region
/// keeps R3 on one side of a clean boundary and keeps `checked_*` honest; it is
/// simply not forced.
pub proof fn lemma_saturation_is_a_choice()
    ensures
        !magnitude_fits(2 * max_mag() + 1, 2),
        (Rat { num: MAX_MAG, den: 1 }).wf(),
        within_error_bound(Rat { num: MAX_MAG, den: 1 }, 2 * max_mag() + 1, 2),
{
    let n = 2 * max_mag() + 1;
    let r = Rat { num: MAX_MAG, den: 1 };
    lemma_max_mag_pow2();
    // Resolve the field accesses on the struct literal before anything reasons
    // about them arithmetically.
    assert(r.n() == max_mag());
    assert(r.d() == 1);
    // I1: gcd(MAX_MAG, 1) unfolds to gcd(1, 0) == 1, so it needs two steps of
    // fuel — the definition recurses on the second argument.
    assert(gcd_int(r.num as int, r.den as int) == 1) by {
        reveal_with_fuel(gcd_nat, 3);
    }
    // Outside the ceiling: |n| == 2·MAX_MAG + 1 > MAX_MAG · 2.
    assert(!magnitude_fits(n, 2));
    // The error is one half, written division-free as |r.num·d − n·r.den| == 1.
    assert(r.n() * 2 - n * r.d() == -1);
    assert(abs_int(r.n() * 2 - n * r.d()) == 1);
    // R3 allows `r.den · max(d, |n|)` == 2·MAX_MAG + 1 == 2^63 − 1, against the
    // 2^61 the error costs.
    assert(max_int(2, abs_int(n)) == n);
    // `n == 2·max_mag() + 1 == 2·2^62 − 1`, and `2^61 < 2^62`, so the bound has
    // room to spare. Stated via monotonicity rather than by unfolding `pow2` up
    // to 63 — the high fuel that needs is enough to destabilise other proofs in
    // this module.
    lemma_pow2_pos(62nat);
    lemma_pow2_mono(61nat, 62nat);
}

} // verus!