automation-structures 0.2.1

Reusable, formally specified building blocks for composing automation systems.
Documentation 
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

//! Executable equality adapters whose contracts are tied to Verus equality.

use vstd::prelude::*;

verus! {

/// Executable equality for values used by generic verified carriers.
pub trait ValueEq: Sized {
    /// Compare two values using the equality seen by specifications.
    fn value_eq(&self, other: &Self) -> (equal: bool)
        ensures equal == (*self == *other);
}

impl ValueEq for u64 {
    fn value_eq(&self, other: &Self) -> (equal: bool) {
        *self == *other
    }
}

impl ValueEq for usize {
    fn value_eq(&self, other: &Self) -> (equal: bool) {
        *self == *other
    }
}

impl ValueEq for (usize, usize, u64) {
    fn value_eq(&self, other: &Self) -> (equal: bool) {
        self.0 == other.0 && self.1 == other.1 && self.2 == other.2
    }
}

}