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
138
139
140
141

use builtin::*;
use builtin_macros::*;
use vstd::{map::*, modes::*, prelude::*, seq::*, seq_lib::*, *};
use vstd::{set::*, set_lib::*};
// use crate::protocol::RSL::configuration::*;
// use crate::protocol::RSL::constants::*;
// use crate::protocol::RSL::broadcast::*;
// use crate::protocol::RSL::environment::*;
use crate::common::framework::environment_s::*;
use crate::common::native::io_s::*;
use crate::protocol::RSL::types::*;
use crate::services::RSL::app_state_machine::*;

use crate::implementation::common::marshalling::*;

verus! {
    pub type CAppState = u64;

    pub open spec fn CAppStateIsAbstractable(s:&CAppState) -> bool {
        true
    }

    pub open spec fn CAppStateIsValid(s:&CAppState) -> bool {
        true
    }

    pub open spec fn AbstractifyCAppStateToAppState(s:&CAppState) -> AppState
        recommends CAppStateIsAbstractable(s)
    {
        *s
    }

    // #[derive(Clone, PartialEq)]
    // pub enum CAppMessage {
    //     CAppIncrement{},
    //     CAppReply{
    //         response:u64,
    //     },
    //     CAppInvalid{},
    // }

    define_enum_and_derive_marshalable! {
        #[derive(Clone, PartialEq, Eq, Hash)]
        pub enum CAppMessage {
            #[tag = 0]
            CAppIncrement,
            #[tag = 1]
            CAppReply { #[o=o0]response: u64 },
            #[tag = 2]
            CAppInvalid,
        }
        [rlimit attr = verifier::rlimit(25)]
    }

    impl CAppMessage {

        pub fn clone_up_to_view(&self) -> (res: CAppMessage)
            ensures res@ == self@
        {
            match self {
                CAppMessage::CAppIncrement {} => CAppMessage::CAppIncrement {},
                CAppMessage::CAppReply { response } => CAppMessage::CAppReply { response: *response },
                CAppMessage::CAppInvalid {} => CAppMessage::CAppInvalid {},
            }
        }

        pub open spec fn abstractable(&self) -> bool {
            true
        }

        pub open spec fn valid(&self) -> bool {
            self.abstractable()
        }

        pub open spec fn view(&self) -> AppMessage
            recommends
                self.abstractable()
        {
            match self {
                CAppMessage::CAppIncrement{} => AppMessage::AppIncrementRequest{},
                CAppMessage::CAppReply{response} => AppMessage::AppIncrementReply{response: *response},
                CAppMessage::CAppInvalid{} => AppMessage::AppInvalidReply{},
            }
        }

        pub proof fn view_equal_spec()
            ensures forall |x: &CAppMessage, y: &CAppMessage| #[trigger] x.view_equal(y) <==> x@ == y@
        {
            assert forall |x: &CAppMessage, y: &CAppMessage|
            #[trigger] x.view_equal(y) <==> x@ == y@ by
            {
            match (x, y) {
                (CAppMessage::CAppIncrement {  }, CAppMessage::CAppIncrement { }) => {},
                (CAppMessage::CAppReply { response:r1 }, CAppMessage::CAppReply { response:r2 }) => {},
                (CAppMessage::CAppInvalid {  }, CAppMessage::CAppInvalid {  }) => {},
                _ => {
                assert(!x.view_equal(y) && x@ != y@);
                }
            }
            }
        }
    }

    pub fn CAppStateInit() -> (s:CAppState)
        ensures
            CAppStateIsAbstractable(&s),
            AbstractifyCAppStateToAppState(&s) == AppInitialize(),
    {
        0 
    }

    pub fn CappendIncrImpl(v:&u64) -> (rc:u64)
            requires 0 <= *v <= 0xffff_ffff_ffff_ffff
            ensures rc == CappedIncr(*v)
        {
            if (*v == 0xffff_ffff_ffff_ffff) {
                // return v;
                *v
            } else {
                // return v + 1;
                v + 1
            }
        }

    pub fn HandleAppRequest(appState:&CAppState, request:&CAppMessage) -> (rc:(CAppState, CAppMessage))
        requires
            CAppStateIsAbstractable(appState),
            request.abstractable(),
        ensures
            CAppStateIsAbstractable(&rc.0),
            rc.1.abstractable(),
            AppHandleRequest(AbstractifyCAppStateToAppState(appState), request.view()) ==
            (AbstractifyCAppStateToAppState(&rc.0), rc.1.view())
    {
        match request {
            CAppMessage::CAppIncrement {} => {(CappendIncrImpl(appState), CAppMessage::CAppReply{response: CappendIncrImpl(appState)})},
            _ => {(*appState, CAppMessage::CAppInvalid{})}
        }
    }

}