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!