vstd/math.rs
1#[allow(unused_imports)]
2use super::prelude::*;
3
4verus! {
5
6/// This function computes the minimum of two given integers.
7pub open spec fn min(x: int, y: int) -> int {
8 if x <= y {
9 x
10 } else {
11 y
12 }
13}
14
15/// This function computes the maximum of two given integers.
16pub open spec fn max(x: int, y: int) -> int {
17 if x >= y {
18 x
19 } else {
20 y
21 }
22}
23
24/// This function computes the maximum of three given integers.
25pub open spec fn max3(x: int, y: int, z: int) -> int {
26 if x < y {
27 max(y, z)
28 } else {
29 max(x, z)
30 }
31}
32
33/// This function converts the given integer `x` to a natural number
34/// by returning 0 when `x` is negative and `x` otherwise.
35pub open spec fn clip(x: int) -> nat {
36 if x < 0 {
37 0
38 } else {
39 x as nat
40 }
41}
42
43/// This function computes the absolute value of a given integer.
44pub open spec fn abs(x: int) -> nat {
45 if x < 0 {
46 -x as nat
47 } else {
48 x as nat
49 }
50}
51
52/// This function adds two integers together. It's sometimes
53/// useful as a substitute for `+` in triggers that feature
54/// function invocations, since mathematical operators can't be
55/// mixed with function invocations in triggers.
56pub open spec fn add(x: int, y: int) -> int {
57 x + y
58}
59
60/// This function subtracts two integers. It's sometimes useful as
61/// a substitute for `-` in triggers that feature function
62/// invocations, since mathematical operators can't be mixed with
63/// function invocations in triggers.
64pub open spec fn sub(x: int, y: int) -> int {
65 x - y
66}
67
68/// This function divides two integers. It's sometimes useful as a
69/// substitute for `/` in triggers that feature function
70/// invocations, since mathematical operators can't be mixed with
71/// function invocations in triggers.
72pub open spec fn div(x: int, y: int) -> int {
73 x / y
74}
75
76} // verus!