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

use crate::protocol::RSL::configuration::*;
use crate::protocol::RSL::parameters::*;
use builtin::*;
use builtin_macros::*;
use vstd::prelude::verus;
use vstd::*;

verus! {
    pub struct LConstants {
        pub config:LConfiguration,
        pub params:LParameters,
    }

    pub struct LReplicaConstants {
        pub my_index:int,
        pub all:LConstants,
    }

    pub open spec fn LReplicaConstantsValid(c:LReplicaConstants) -> bool
    {
        0 <= c.my_index < c.all.config.replica_ids.len()
    }
}