tla-rs 0.1.0

Rust implementation of the IronFleet verified distributed systems framework
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

use crate::protocol::common::upper_bound::*;
use vstd::prelude::*;

verus! {
    pub enum CUpperBound {
        CUpperBoundFinite { n: int },
        CUpperBoundInfinite,
    }

    impl CUpperBound {
        pub open spec fn valid(self) -> bool {
            match self {
                CUpperBound::CUpperBoundFinite { n } => true,
                CUpperBound::CUpperBoundInfinite => true,
            }
        }

        pub open spec fn abstractable(self) -> bool {
            true
        }

        pub open spec fn view(self) -> UpperBound {
            match self {
                CUpperBound::CUpperBoundFinite { n } => UpperBound::UpperBoundFinite { n },
                CUpperBound::CUpperBoundInfinite => UpperBound::UpperBoundInfinite{},
            }
        }

        pub open spec fn CLeqUpperBound(x: int, u:CUpperBound) -> bool {
            match u {
                CUpperBound::CUpperBoundFinite{n} => x<= n,
                CUpperBound::CUpperBoundInfinite => true
            }
        }

    }
}