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

use builtin::*;
use builtin_macros::*;
use vstd::seq::*;

use vstd::{set::*, set_lib::*};

verus! {
    // pub open spec fn CountMatchesInSeq<T, F: spec_fn(T) -> bool>(s: Seq<T>, f: F) -> nat
    // {
    //     if s.len() == 0 {
    //         0
    //     } else {
    //         CountMatchesInSeq(s.subrange(1, s.len() as int), f) + if f(s.index(0)) { 1 as nat } else { 0 as nat }
    //     }
    // }

    pub open spec fn CountMatchesInSeq<T>(s: Seq<T>, f: spec_fn(T) -> bool) -> nat
        decreases s.len()
    {
        if s.len() == 0 {
            0
        } else {
            CountMatchesInSeq(s.subrange(1, s.len() as int), f) + if f(s.index(0)) { 1 as nat } else { 0 as nat }
        }
    }

    pub open spec fn IsNthHighestValueInSequence(v:int, s:Seq<int>, n:int) -> bool
    {
        &&& 0 < n < s.len()
        &&& s.contains(v)
        &&& CountMatchesInSeq(s, |x:int| x > v) < n
        &&& CountMatchesInSeq(s, |x:int| x >= v) >= n
    }

}