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

use builtin::*;
use builtin_macros::*;
use vstd::*;
use vstd::seq::*;
use crate::protocol::RSL::types::*;
use crate::protocol::RSL::message::*;
use crate::common::framework::environment_s::*;
use crate::common::native::io_s::*;

verus! {
    pub type RslEnvironment = LEnvironment<AbstractEndPoint, RslMessage>;
    pub type RslPacket = LPacket<AbstractEndPoint, RslMessage>;
    pub type RslIo = LIoOp<AbstractEndPoint, RslMessage>;

    pub open spec fn ConcatenatePaxosIos(s:Seq<Seq<RslIo>>) -> Seq<RslIo>
        decreases s.len()
    {
        if s.len() == 0 {
            Seq::empty()
        } else {
            s[0] + ConcatenatePaxosIos(s.subrange(1, s.len() as int))
        }
    }
}