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
#[allow(unused_imports)]
use super::prelude::*;
verus! {
/// This function computes the minimum of two given integers.
pub open spec fn min(x: int, y: int) -> int {
if x <= y {
x
} else {
y
}
}
/// This function computes the maximum of two given integers.
pub open spec fn max(x: int, y: int) -> int {
if x >= y {
x
} else {
y
}
}
/// This function computes the maximum of three given integers.
pub open spec fn max3(x: int, y: int, z: int) -> int {
if x < y {
max(y, z)
} else {
max(x, z)
}
}
/// This function converts the given integer `x` to a natural number
/// by returning 0 when `x` is negative and `x` otherwise.
pub open spec fn clip(x: int) -> nat {
if x < 0 {
0
} else {
x as nat
}
}
/// This function computes the absolute value of a given integer.
pub open spec fn abs(x: int) -> nat {
if x < 0 {
-x as nat
} else {
x as nat
}
}
/// This function adds two integers together. It's sometimes
/// useful as a substitute for `+` in triggers that feature
/// function invocations, since mathematical operators can't be
/// mixed with function invocations in triggers.
pub open spec fn add(x: int, y: int) -> int {
x + y
}
/// This function subtracts two integers. It's sometimes useful as
/// a substitute for `-` in triggers that feature function
/// invocations, since mathematical operators can't be mixed with
/// function invocations in triggers.
pub open spec fn sub(x: int, y: int) -> int {
x - y
}
/// This function divides two integers. It's sometimes useful as a
/// substitute for `/` in triggers that feature function
/// invocations, since mathematical operators can't be mixed with
/// function invocations in triggers.
pub open spec fn div(x: int, y: int) -> int {
x / y
}
} // verus!