tla-rs 0.1.0

Rust implementation of the IronFleet verified distributed systems framework
1
2
3
4
5
6
7
8
9
10

use vstd::prelude::*;
use vstd::seq::*;

verus! {
    #[verifier::opaque]
    pub open spec fn SeqIsUnique<T>(s: Seq<T>) -> bool {
        forall |i: int, j: int| #![trigger s[i], s[j]]
            0 <= i < s.len() && 0 <= j < s.len() && s[i] == s[j] ==> i == j
    }
}