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
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
#[crate::check_module(crate)]
#[declare_types(u32)]
#[allow(dead_code)]
mod my_mod {
#[declare]
const ZERO: u32 = 0;
/// We can't use numeric operators (<=, >, +, etc) in code that
/// the solver sees, so we declare these functions to stand in for
/// them.
#[declare]
fn le(a: u32, b: u32) -> bool {
a <= b
}
#[define]
fn lt(a: u32, b: u32) -> bool
{
le(a,b) && a != b
}
#[define]
fn ge(a: u32, b: u32) -> bool
{
le(b,a)
}
#[define]
fn gt(a: u32, b: u32) -> bool
{
ge(a,b) && a != b
}
/// The 'dec' function subtracts one from a u32, or returns ZERO
/// if the argument was already ZERO.
///
/// 'inc' and 'dec' form the basic interface to u32 that we will
/// use to write functions over u32 that the solver understands.
#[declare]
fn dec(a: u32) -> u32 {
if a == 0 {
0
} else {
a - 1
}
}
/// The 'inc' function adds one to a u32.
#[declare]
fn inc(a: u32) -> u32 {
a + 1
}
// This axiom over inc and dec is what allows us to verify the
// add_zeros annotation later.
#[assume]
fn inc_dec() -> bool {
forall(|a: u32| {
implies(
a != ZERO,
inc(dec(a)) == a
)
})
}
/// 'add' is a recursively-defined function that the solver
/// understands. The solver can use the function body to
/// inductively verify annotations on 'add'.
///
/// When 'add' is used in other verification conditions, the
/// solver will treat it as uninterpreted and assume
/// previously-verified annotations as axioms.
#[define]
#[recursive]
fn add(a: u32, b: u32) -> u32
{
if a == ZERO {
b
} else {
inc(
add(dec(a), b)
)
}
}
// This annotation is verified with respect to the function body
// of 'add'.
#[annotate(add(a,b) => c)]
fn add_zeros() -> bool {
implies(a == ZERO, b == c)
&& implies(b == ZERO, a == c)
}
// This condition can be verified only because we have declared
// the 'add_zeros' annotation above.
#[verify]
fn simple_zeros() -> bool {
add(ZERO, ZERO) == ZERO
}
// The following annotation does not verify under the current
// assumptions. What axioms on 'ZERO' and 'le' are needed to fix
// it?
// #[annotate(add)]
// fn add_monotonic() -> bool {
// |a: u32, b: u32|
// |c: u32|
// le(a,c) && le(a,b)
// }
}