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

use builtin::*;
use builtin_macros::*;
use vstd::{map::*, modes::*, prelude::*, seq::*, seq_lib::*, *};
use vstd::{set::*, set_lib::*};
use crate::protocol::RSL::distributed_system::*;
use crate::protocol::RSL::constants::*;
use crate::protocol::RSL::types::*;
use crate::protocol::RSL::election::*;
use crate::protocol::RSL::common_proof::assumptions::*;
use crate::protocol::RSL::common_proof::constants::*;

use crate::common::logic::temporal_s::*;
use crate::common::logic::heuristics_i::*;
use crate::common::framework::environment_s::*;
use crate::common::framework::environment_s::LEnvStep;
use crate::common::native::io_s::*;
use crate::common::collections::maps2::*;

verus!{
    // #[verifier::external_body]
    pub proof fn lemma_RemoveAllSatisfiedRequestsInSequenceProducesSubsequence(
        s_:Seq<Request>, 
        s:Seq<Request>, 
        r:Request
    )
        requires s_ == RemoveAllSatisfiedRequestsInSequence(s, r)
        ensures  forall |x:Request| s_.contains(x) ==> s.contains(x)
        decreases s.len()
    {
        if s.len() > 0 && !RequestsMatch(s[0], r)
        {
            let s_prev = s.drop_first();
            let s_prev_ = RemoveAllSatisfiedRequestsInSequence(s_prev, r);
            lemma_RemoveAllSatisfiedRequestsInSequenceProducesSubsequence(
                RemoveAllSatisfiedRequestsInSequence(s_prev, r), s_prev, r);
            assert(forall |x:Request| s_prev_.contains(x) ==> s_prev.contains(x));
            assert(forall |x:Request| s_prev.contains(x) ==> s.contains(x));
            assert(forall |x:Request| s_.contains(x) ==> s.contains(x));
        } else if s.len() > 0 && RequestsMatch(s[0], r){
            assert(s_ == RemoveAllSatisfiedRequestsInSequence(s.drop_first(), r));
            assume(s.drop_first().len() < s.len());
            lemma_RemoveAllSatisfiedRequestsInSequenceProducesSubsequence(s_, s.drop_first(), r);
            assert(forall |x:Request| s_.contains(x) ==> s.drop_first().contains(x));
            assert(forall |x:Request| s_.contains(x) ==> s.contains(x));
        } else {
            assert(forall |x:Request| s_.contains(x) ==> s.contains(x));
        }
    }

    pub proof fn lemma_RemoveExecutedRequestBatchProducesSubsequence(
        s_:Seq<Request>, 
        s:Seq<Request>, 
        batch:RequestBatch
    )
        requires s_ == RemoveExecutedRequestBatch(s, batch)
        ensures  forall |x:Request| s_.contains(x) ==> s.contains(x)
        decreases batch.len()
    {
        if batch.len() > 0
        {
            let s__ = RemoveAllSatisfiedRequestsInSequence(s, batch[0]);
            lemma_RemoveAllSatisfiedRequestsInSequenceProducesSubsequence(s__, s, batch[0]);
            lemma_RemoveExecutedRequestBatchProducesSubsequence(s_, s__, batch.drop_first());
        }
    }
}