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

use vstd::map::*;
use vstd::modes::*;
use vstd::multiset::*;
use vstd::seq::*;
use vstd::set::*;

use vstd::pervasive::*;
use builtin::*;
use builtin_macros::*;

verus! {
    pub type AppState = u64;

    pub enum AppMessage {
        AppIncrementRequest{},
        AppIncrementReply{
            response : u64,
        },
        AppInvalidReply{},
    }

    pub open spec fn AppInitialize() -> AppState
    {
        0
    }

    pub open spec fn CappedIncr(v:u64) -> u64
    {
        if v == 0xffff_ffff_ffff_ffff {
            v 
        } else {
            (v + 1) as u64
        }
    }

    pub open spec fn AppHandleRequest(m:AppState, request:AppMessage) -> (AppState, AppMessage)
    {
        if request is AppIncrementRequest {
            (CappedIncr(m), AppMessage::AppIncrementReply{response:CappedIncr(m)})
        } else {
            (m, AppMessage::AppInvalidReply{})
        }
    }
}