vstd_extra/
arithmetic.rs

1use vstd::arithmetic::div_mod::*;
2use vstd::arithmetic::mul::*;
3use vstd::prelude::*;
4
5verus! {
6
7pub open spec fn nat_align_down(x: nat, align: nat) -> nat
8    recommends
9        align > 0,
10{
11    (x - x % align) as nat
12}
13
14pub open spec fn nat_align_up(x: nat, align: nat) -> nat
15    recommends
16        align > 0,
17{
18    if x % align == 0 {
19        x
20    } else {
21        nat_align_down(x, align) + align
22    }
23}
24
25pub broadcast proof fn lemma_nat_align_up_sound(x: nat, align: nat)
26    requires
27        align > 0,
28    ensures
29        #[trigger] nat_align_up(x, align) >= x,
30        nat_align_up(x, align) % align == 0,
31        forall|n: nat| n >= x && #[trigger] (n % align) == 0 ==> n >= nat_align_up(x, align),
32        nat_align_up(x, align) - x < align,
33{
34    if x % align == 0 {
35    } else {
36        let down = nat_align_down(x, align);
37        lemma_fundamental_div_mod(x as int, align as int);
38        lemma_mul_is_commutative(align as int, x as int / align as int);
39        lemma_mod_multiples_basic(x as int / align as int, align as int);
40        lemma_mod_add_multiples_vanish(down as int, align as int);
41    }
42
43    assert forall|n: nat| n >= x && (#[trigger] (n % align)) == 0 implies n >= nat_align_up(
44        x,
45        align,
46    ) by {
47        if x % align == 0 {
48        } else {
49            lemma_mul_is_commutative(align as int, x as int / align as int);
50
51            lemma_fundamental_div_mod(n as int, align as int);
52            if n < nat_align_up(x, align) {
53                let q_n = n as int / align as int;
54                let q_x = x as int / align as int;
55                lemma_mul_is_distributive_add(align as int, q_x, 1);
56                if q_n >= q_x + 1 {
57                    lemma_mul_inequality(q_x + 1, q_n, align as int);
58                    lemma_mul_is_commutative(align as int, q_n);
59                }
60                lemma_mul_inequality(q_n, q_x, align as int);
61                lemma_mul_is_commutative(align as int, q_n);
62            }
63        }
64    }
65}
66
67pub broadcast proof fn lemma_nat_align_down_sound(x: nat, align: nat)
68    requires
69        align > 0,
70    ensures
71        #[trigger] nat_align_down(x, align) <= x,
72        nat_align_down(x, align) % align == 0,
73        forall|n: nat| n <= x && #[trigger] (n % align) == 0 ==> n <= nat_align_down(x, align),
74        x - nat_align_down(x, align) < align,
75{
76    lemma_fundamental_div_mod(x as int, align as int);
77    let q_x = x as int / align as int;
78    lemma_mod_multiples_basic(q_x, align as int);
79    lemma_mul_is_commutative(align as int, q_x);
80
81    assert forall|n: nat| n <= x && #[trigger] (n % align) == 0 implies n <= nat_align_down(
82        x,
83        align,
84    ) by {
85        if n > nat_align_down(x, align) && n % align == 0 {
86            lemma_fundamental_div_mod(n as int, align as int);
87            let q_n = n as int / align as int;
88            if q_n <= q_x {
89                lemma_mul_inequality(q_n, q_x, align as int);
90                lemma_mul_is_commutative(align as int, q_n);
91            } else {
92                lemma_mul_inequality(q_x + 1, q_n, align as int);
93                lemma_mul_is_commutative(align as int, q_n);
94                lemma_mul_is_distributive_add(align as int, q_x, 1);
95            }
96        }
97    }
98}
99
100/// When `k2` is a multiple of `k1`, aligning to the coarser `k2` gives a
101/// value at most `nat_align_down(x, k1)`: the `k2`-boundary is also a
102/// `k1`-boundary, and it is the largest such boundary ≤ x.
103pub proof fn lemma_nat_align_down_monotone(x: nat, k1: nat, k2: nat)
104    requires
105        k1 > 0,
106        k2 > 0,
107        k2 % k1 == 0,
108    ensures
109        nat_align_down(x, k2) <= nat_align_down(x, k1),
110        nat_align_down(x, k2) % k1 == 0,
111{
112    lemma_nat_align_down_sound(x, k1);
113    lemma_nat_align_down_sound(x, k2);
114    let a = nat_align_down(x, k2) as int;
115    let q = a / k2 as int;
116    let r = k2 as int / k1 as int;
117    lemma_fundamental_div_mod(a, k2 as int);
118    lemma_fundamental_div_mod(k2 as int, k1 as int);
119    assert(k2 as int == r * k1 as int);
120    lemma_mul_is_associative(q, r, k1 as int);
121    lemma_mod_multiples_basic(q * r, k1 as int);
122}
123
124/// The finer-aligned block `[align_down(x,k1), align_down(x,k1)+k1)` fits
125/// inside the coarser-aligned block `[align_down(x,k2), align_down(x,k2)+k2)`
126/// when `k1` divides `k2`.
127pub proof fn lemma_nat_align_down_within_block(x: nat, k1: nat, k2: nat)
128    requires
129        k1 > 0,
130        k2 > 0,
131        k2 % k1 == 0,
132    ensures
133        nat_align_down(x, k1) + k1 <= nat_align_down(x, k2) + k2,
134{
135    lemma_nat_align_down_sound(x, k1);
136    lemma_nat_align_down_sound(x, k2);
137    lemma_nat_align_down_monotone(x, k1, k2);
138    let a1 = nat_align_down(x, k1) as int;
139    let a2 = nat_align_down(x, k2) as int;
140    let q1 = a1 / k1 as int;
141    let q2 = a2 / k1 as int;
142    lemma_fundamental_div_mod(a1, k1 as int);
143    lemma_fundamental_div_mod(a2, k1 as int);
144    lemma_nat_align_down_monotone(x, k1, k2);
145    lemma_mul_is_distributive_sub(k1 as int, q1, q2);
146    lemma_mul_is_commutative(k1 as int, q1);
147    lemma_mul_is_commutative(k1 as int, q2);
148    lemma_mul_is_commutative(k1 as int, q1 - q2);
149    let qk = k2 as int / k1 as int;
150    lemma_fundamental_div_mod(k2 as int, k1 as int);
151    lemma_mul_is_commutative(k1 as int, qk);
152    if q1 - q2 >= qk {
153        lemma_mul_inequality(qk, q1 - q2, k1 as int);
154        lemma_mul_is_commutative(k1 as int, q1 - q2);
155    } else {
156        lemma_mul_inequality(q1 - q2 + 1, qk, k1 as int);
157        lemma_mul_is_commutative(k1 as int, q1 - q2 + 1);
158        lemma_mul_is_distributive_add(k1 as int, q1 - q2, 1 as int);
159        lemma_mul_is_commutative(k1 as int, q1 - q2);
160    }
161}
162
163broadcast group group_arithmetic_lemmas {
164    lemma_nat_align_up_sound,
165    lemma_nat_align_down_sound,
166}
167
168} // verus!
vstd_extra/arithmetic.rs

vstd_extra/
arithmetic.rs
