vstd_extra/external/
cmp.rs

1// SPDX-License-Identifier: MPL-2.0
2//! Specifications for the free comparison functions missing from `vstd`.
3use vstd::{prelude::*, std_specs::cmp::OrdSpec};
4
5use core::cmp::Ordering;
6
7verus! {
8
9/// Returns `y` when it compares less than `x`, and returns `x` otherwise.
10pub open spec fn spec_ord_min<T: Ord>(x: T, y: T) -> T {
11    match y.cmp_spec(&x) {
12        Ordering::Less => y,
13        Ordering::Equal => x,
14        Ordering::Greater => x,
15    }
16}
17
18/// Returns `x` when `y` compares less than it, and returns `y` otherwise.
19pub open spec fn spec_ord_max<T: Ord>(x: T, y: T) -> T {
20    match y.cmp_spec(&x) {
21        Ordering::Less => x,
22        Ordering::Equal => y,
23        Ordering::Greater => y,
24    }
25}
26
27/// Returns the minimum, choosing the first argument when they compare equal.
28/// See [`std::cmp::min`](https://doc.rust-lang.org/std/cmp/fn.min.html).
29#[verifier::when_used_as_spec(spec_ord_min)]
30pub assume_specification<T: Ord>[ core::cmp::min ](x: T, y: T) -> (ret: T)
31    ensures
32        T::obeys_cmp_spec() ==> ret == spec_ord_min(x, y),
33;
34
35/// Returns the maximum, choosing the second argument when they compare equal.
36/// See [`std::cmp::max`](https://doc.rust-lang.org/std/cmp/fn.max.html).
37#[verifier::when_used_as_spec(spec_ord_max)]
38pub assume_specification<T: Ord>[ core::cmp::max ](x: T, y: T) -> (ret: T)
39    ensures
40        T::obeys_cmp_spec() ==> ret == spec_ord_max(x, y),
41;
42
43} // verus!
vstd_extra/external/cmp.rs

vstd_extra/external/
cmp.rs
