automation_structures/
value_eq.rs

1//! Executable equality adapters whose contracts are tied to Verus equality.
2
3use vstd::prelude::*;
4
5verus! {
6
7/// Executable equality for values used by generic verified carriers.
8pub trait ValueEq: Sized {
9    /// Compare two values using the equality seen by specifications.
10    fn value_eq(&self, other: &Self) -> (equal: bool)
11        ensures equal == (*self == *other);
12}
13
14impl ValueEq for u64 {
15    fn value_eq(&self, other: &Self) -> (equal: bool) {
16        *self == *other
17    }
18}
19
20impl ValueEq for usize {
21    fn value_eq(&self, other: &Self) -> (equal: bool) {
22        *self == *other
23    }
24}
25
26impl ValueEq for (usize, usize, u64) {
27    fn value_eq(&self, other: &Self) -> (equal: bool) {
28        self.0 == other.0 && self.1 == other.1 && self.2 == other.2
29    }
30}
31
32}

automation_structures/value_eq.rs

automation_structures/
value_eq.rs