vstd_extra/
arithmetic.rs

1use vstd::arithmetic::div_mod::*;
2use vstd::arithmetic::mul::*;
3use vstd::{pervasive::trigger, 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
100broadcast group group_arithmetic_lemmas {
101    lemma_nat_align_up_sound,
102    lemma_nat_align_down_sound,
103}
104
105} // verus!
vstd_extra/arithmetic.rs

vstd_extra/
arithmetic.rs
