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
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80

// #![allow(unused_imports)]
// #![allow(unused_attributes)]
use builtin::*;
use builtin_macros::*;
use vstd::map::*;
use vstd::modes::*;
use vstd::multiset::*;
use vstd::pervasive::*;
use vstd::seq::*;

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

use crate::common::framework::environment_s::*;
use crate::common::native::io_s::*;
use crate::services::RSL::app_state_machine::*;

verus! {
    pub type OperationNumber = int;

    pub struct Ballot {
        pub seqno : int,
        pub proposer_id : int,
    }

    pub struct Request {
        pub client : AbstractEndPoint,
        pub seqno : int,
        pub request : AppMessage,
    }

    pub struct Reply {
        pub client : AbstractEndPoint,
        pub seqno : int,
        pub reply : AppMessage,
    }

    pub type RequestBatch = Seq<Request>;

    pub type ReplyCache = Map<AbstractEndPoint, Reply>;

    pub struct Vote {
        pub max_value_bal : Ballot,
        pub max_val : RequestBatch,
    }

    pub type Votes = Map<OperationNumber, Vote>;

    pub struct LearnerTuple {
        pub received_2b_message_senders:Set<AbstractEndPoint>, 
        pub candidate_learned_value:RequestBatch,
    }

    pub type LearnerState = Map<OperationNumber, LearnerTuple>;

    pub open spec fn BalLt(ba:Ballot, bb:Ballot) -> bool
    {
        ||| ba.seqno < bb.seqno
        ||| (ba.seqno == bb.seqno && ba.proposer_id < bb.proposer_id)
    }

    pub open spec fn BalLeq(ba:Ballot, bb:Ballot) -> bool
    {
        ||| ba.seqno < bb.seqno
        ||| (ba.seqno == bb.seqno && ba.proposer_id <= bb.proposer_id)
    }

    pub proof fn lemma_BalLtMiddle(ba:Ballot, bb:Ballot)
        requires 
            !BalLt(ba, bb),
            ba != bb,
        ensures
            BalLt(bb, ba),
    {

    }

    pub struct ClockReading {
        pub t:int
    }
}