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
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137

use builtin::*;
use builtin_macros::*;
use crate::implementation::common::function::*;
use vstd::prelude::*;
use vstd::slice::*;
use crate::verus_extra::seq_lib_v::*;
use crate::common::native::io_s::*;
use crate::protocol::RSL::environment::*;
use crate::implementation::RSL::{replicaimpl_class::*, cmessage::*, cbroadcast::*, replicaimpl_delivery::*, netrsl_i::*, ReplicaImpl::*};
use vstd::{map::*, modes::*, prelude::*, seq::*, seq_lib::*, *};
use vstd::{set::*, set_lib::*};

verus!{

    pub fn replica_next_process_packet_invalid(r:&mut ReplicaImpl, netc:&mut NetClient, pkt:CPacket)
    {

    }

    #[verifier(external_body)]
    pub fn replica_next_process_packet_request(r:&mut ReplicaImpl, netc:&mut NetClient, pkt:CPacket) -> (ok:bool)
    {   
        let outpackets = CReplica::CReplicaNextProcessRequest(&mut r.replica, pkt);
        let ok = deliver_outbound_packets(r, netc, &outpackets);
        ok
    }

    #[verifier(external_body)]
    pub fn replica_next_process_packet_1a(r:&mut ReplicaImpl, netc:&mut NetClient, pkt:CPacket) -> (ok:bool)
    {   
        let outpackets = CReplica::CReplicaNextProcess1a(&mut r.replica, pkt);
        let ok = deliver_outbound_packets(r, netc, &outpackets);
        ok
    }

    #[verifier(external_body)]
    pub fn replica_next_process_packet_1b(r:&mut ReplicaImpl, netc:&mut NetClient, pkt:CPacket) -> (ok:bool)
    {   
        let outpackets = CReplica::CReplicaNextProcess1b(&mut r.replica, pkt);
        let ok = deliver_outbound_packets(r, netc, &outpackets);
        ok
    }

    #[verifier(external_body)]
    pub fn replica_next_process_packet_starting_phase2(r:&mut ReplicaImpl, netc:&mut NetClient, pkt:CPacket) -> (ok:bool)
    {   
        let outpackets = CReplica::CReplicaNextProcessStartingPhase2(&mut r.replica, pkt);
        let ok = deliver_outbound_packets(r, netc, &outpackets);
        ok
    }

    #[verifier(external_body)]
    pub fn replica_next_process_packet_2a(r:&mut ReplicaImpl, netc:&mut NetClient, pkt:CPacket) -> (ok:bool)
    {   
        let outpackets = CReplica::CReplicaNextProcess2a(&mut r.replica, pkt);
        let ok = deliver_outbound_packets(r, netc, &outpackets);
        ok
    }

    #[verifier(external_body)]
    pub fn replica_next_process_packet_2b(r:&mut ReplicaImpl, netc:&mut NetClient, pkt:CPacket) -> (ok:bool)
    {   
        let outpackets = CReplica::CReplicaNextProcess2b(&mut r.replica, pkt);
        let ok = deliver_outbound_packets(r, netc, &outpackets);
        ok
    }

    #[verifier(external_body)]
    pub fn replica_next_process_packet_reply(r:&mut ReplicaImpl, netc:&mut NetClient, pkt:CPacket) -> (ok:bool)
    {   
        let outpackets = CReplica::CReplicaNextProcessReply(&mut r.replica, pkt);
        let ok = deliver_outbound_packets(r, netc, &outpackets);
        ok
    }

    #[verifier(external_body)]
    pub fn replica_next_process_packet_appstate_request(r:&mut ReplicaImpl, netc:&mut NetClient, pkt:CPacket) -> (ok:bool)
    {   
        let outpackets = CReplica::CReplicaNextProcessAppStateRequest(&mut r.replica, pkt);
        let ok = deliver_outbound_packets(r, netc, &outpackets);
        ok
    }

    #[verifier(external_body)]
    pub fn replica_next_process_packet_appstate_supply(r:&mut ReplicaImpl, netc:&mut NetClient, pkt:CPacket) -> (ok:bool)
    {   
        let outpackets = CReplica::CReplicaNextProcessAppStateSupply(&mut r.replica, pkt);
        let ok = deliver_outbound_packets(r, netc, &outpackets);
        ok
    }

    #[verifier(external_body)]
    pub fn replica_next_process_packet_without_reading_clock(r:&mut ReplicaImpl, netc:&mut NetClient, pkt:CPacket) -> (ok:bool)
    {
        let mut ok = true;
        match pkt.msg {
            CMessage::CMessageInvalid{} => {
                // ok = true
            }
            CMessage::CMessageRequest{seqno_req, ..} => {
                // println!("receive request");
                ok = replica_next_process_packet_request(r, netc, pkt);
            }
            CMessage::CMessage1a{bal_1a} => {
                println!("receive 1a");
                ok = replica_next_process_packet_1a(r, netc, pkt);
            }
            CMessage::CMessage1b{bal_1b, log_truncation_point, ..} => {
                println!("receive 1b");
                ok = replica_next_process_packet_1b(r, netc, pkt);
            }
            CMessage::CMessageStartingPhase2{bal_2, logTruncationPoint_2} => {
                println!("receive starting phase 2");
                ok = replica_next_process_packet_starting_phase2(r, netc, pkt);
            }
            CMessage::CMessage2a{bal_2a, opn_2a, ..} => {
                // println!("receive 2a");
                ok = replica_next_process_packet_2a(r, netc, pkt);
            }
            CMessage::CMessage2b{bal_2b, opn_2b, ..} => {
                // println!("receive 2b");
                ok = replica_next_process_packet_2b(r, netc, pkt);
            }
            CMessage::CMessageReply{seqno_reply, ..} => {
                ok = replica_next_process_packet_reply(r, netc, pkt);
            }
            CMessage::CMessageAppStateRequest{bal_state_req, opn_state_req} => {
                ok = replica_next_process_packet_appstate_request(r, netc, pkt);
            }
            CMessage::CMessageAppStateSupply{bal_state_supply, opn_state_supply, ..} => {
                ok = replica_next_process_packet_appstate_supply(r, netc, pkt);
            }
            _ => {}
        }
        ok
    }
}