vstd_extra/temporal_logic/
defs.rs

1// Copyright 2022 VMware, Inc.
2// SPDX-License-Identifier: MIT
3#![allow(unused_imports)]
4use vstd::prelude::*;
5
6verus! {
7
8#[verifier::ext_equal]
9pub struct Execution<T> {
10    pub nat_to_state: spec_fn(nat) -> T,
11}
12
13impl<T> Execution<T> {
14    pub open spec fn head(self) -> T {
15        (self.nat_to_state)(0)
16    }
17
18    pub open spec fn head_next(self) -> T {
19        (self.nat_to_state)(1)
20    }
21
22    pub open spec fn suffix(self, pos: nat) -> Self {
23        Execution { nat_to_state: |i: nat| (self.nat_to_state)(i + pos) }
24    }
25}
26
27#[verifier::ext_equal]
28#[verifier(reject_recursive_types(T))]
29pub struct StatePred<T> {
30    pub pred: spec_fn(T) -> bool,
31}
32
33impl<T> StatePred<T> {
34    pub open spec fn new(pred: spec_fn(T) -> bool) -> Self {
35        StatePred { pred: pred }
36    }
37
38    pub open spec fn as_fn(self) -> spec_fn(T) -> bool {
39        self.pred
40    }
41
42    pub open spec fn apply(self, state: T) -> bool {
43        (self.pred)(state)
44    }
45
46    pub open spec fn and(self, other: Self) -> Self {
47        StatePred::new(|s| self.apply(s) && other.apply(s))
48    }
49
50    pub open spec fn or(self, other: Self) -> Self {
51        StatePred::new(|s| self.apply(s) || other.apply(s))
52    }
53
54    pub open spec fn implies(self, other: Self) -> Self {
55        StatePred::new(|s| self.apply(s) ==> other.apply(s))
56    }
57
58    pub open spec fn not(self) -> Self {
59        StatePred::new(|s| !self.apply(s))
60    }
61
62    pub open spec fn state_forall<A>(a_to_state_pred: spec_fn(A) -> StatePred<T>) -> StatePred<T> {
63        StatePred::new(|s| forall|a| #[trigger] a_to_state_pred(a).apply(s))
64    }
65
66    pub open spec fn state_exists<A>(a_to_state_pred: spec_fn(A) -> StatePred<T>) -> StatePred<T> {
67        StatePred::new(|s| exists|a| #[trigger] a_to_state_pred(a).apply(s))
68    }
69
70    pub open spec fn absorb<A>(
71        a_to_state_pred: spec_fn(A) -> StatePred<T>,
72        state_pred: StatePred<T>,
73    ) -> spec_fn(A) -> StatePred<T> {
74        |a: A| a_to_state_pred(a).and(state_pred)
75    }
76}
77
78#[verifier::ext_equal]
79#[verifier(reject_recursive_types(T))]
80pub struct ActionPred<T> {
81    pub pred: spec_fn(T, T) -> bool,
82}
83
84impl<T> ActionPred<T> {
85    pub open spec fn new(pred: spec_fn(T, T) -> bool) -> Self {
86        ActionPred { pred: pred }
87    }
88
89    pub open spec fn as_fn(self) -> spec_fn(T, T) -> bool {
90        self.pred
91    }
92
93    pub open spec fn apply(self, state: T, state_prime: T) -> bool {
94        (self.pred)(state, state_prime)
95    }
96}
97
98#[verifier::ext_equal]
99#[verifier(reject_recursive_types(T))]
100pub struct TempPred<T> {
101    pub pred: spec_fn(Execution<T>) -> bool,
102}
103
104impl<T> TempPred<T> {
105    pub open spec fn new(pred: spec_fn(Execution<T>) -> bool) -> Self {
106        TempPred { pred: pred }
107    }
108
109    pub open spec fn satisfied_by(self, execution: Execution<T>) -> bool {
110        (self.pred)(execution)
111    }
112
113    // We specify all infix operators for temporal logic as TempPred methods to aid readability
114    /// `/\` for temporal predicates in TLA+ (i.e., `&&` in Verus).
115    pub open spec fn and(self, other: Self) -> Self {
116        TempPred::new(|ex: Execution<T>| self.satisfied_by(ex) && other.satisfied_by(ex))
117    }
118
119    /// `\/` for temporal predicates in TLA+ (i.e., `||` in Verus).
120    pub open spec fn or(self, other: Self) -> Self {
121        TempPred::new(|ex: Execution<T>| self.satisfied_by(ex) || other.satisfied_by(ex))
122    }
123
124    // `=>` for temporal predicates in TLA+ (i.e., `==>` in Verus).
125    pub open spec fn implies(self, other: Self) -> Self {
126        TempPred::new(|ex: Execution<T>| self.satisfied_by(ex) ==> other.satisfied_by(ex))
127    }
128
129    // `~>` for temporal predicates in TLA+.
130    // Returns a temporal predicate that is satisfied
131    // iff it is always the case that `self` getting satisfied implies `other` eventually getting satisfied.
132    //
133    // Defined in 3.2.3.
134    // |ex| forall |i: nat| self.satisfied_by(ex.suffix(i)) ==> exists |j: nat| other.satisfied_by(ex.suffix(i + j))
135    pub open spec fn leads_to(self, other: Self) -> Self {
136        always(self.implies(eventually(other)))
137    }
138
139    /// `|=` for temporal predicates in TLA+.
140    pub open spec fn entails(self, other: Self) -> bool {
141        valid(self.implies(other))
142    }
143}
144
145pub open spec fn lift_state<T>(state_pred: StatePred<T>) -> TempPred<T> {
146    TempPred::new(|ex: Execution<T>| state_pred.apply(ex.head()))
147}
148
149pub open spec fn lift_state_prime<T>(state_pred: StatePred<T>) -> TempPred<T> {
150    TempPred::new(|ex: Execution<T>| state_pred.apply(ex.head_next()))
151}
152
153pub open spec fn lift_action<T>(action_pred: ActionPred<T>) -> TempPred<T> {
154    TempPred::new(|ex: Execution<T>| action_pred.apply(ex.head(), ex.head_next()))
155}
156
157// `[]` for temporal predicates in TLA+.
158// Returns a temporal predicate that is satisfied iff `temp_pred` is satisfied on every suffix of the execution.
159//
160// Defined in 3.1.
161pub open spec fn always<T>(temp_pred: TempPred<T>) -> TempPred<T> {
162    TempPred::new(|ex: Execution<T>| forall|i: nat| #[trigger] temp_pred.satisfied_by(ex.suffix(i)))
163}
164
165// `<>` for temporal predicates in TLA+.
166// Returns a temporal predicate that is satisfied iff `temp_pred` is satisfied on at least one suffix of the execution.
167//
168// Defined in 3.2.1.
169pub open spec fn eventually<T>(temp_pred: TempPred<T>) -> TempPred<T> {
170    TempPred::new(|ex: Execution<T>| exists|i: nat| #[trigger] temp_pred.satisfied_by(ex.suffix(i)))
171}
172
173// `'` (prime) for temporal predicates in TLA+.
174// Returns a temporal predicate that is satisfied iff `temp_pred` is satisfied on the suffix execution starting from the next state.
175pub open spec fn later<T>(temp_pred: TempPred<T>) -> TempPred<T> {
176    TempPred::new(|ex: Execution<T>| temp_pred.satisfied_by(ex.suffix(1)))
177}
178
179/// `~` for temporal predicates in TLA+ (i.e., `!` in Verus).
180pub open spec fn not<T>(temp_pred: TempPred<T>) -> TempPred<T> {
181    TempPred::new(|ex: Execution<T>| !temp_pred.satisfied_by(ex))
182}
183
184/// `\A` for temporal predicates in TLA+ (i.e., `forall` in Verus).
185pub open spec fn tla_forall<T, A>(a_to_temp_pred: spec_fn(A) -> TempPred<T>) -> TempPred<T> {
186    TempPred::new(|ex: Execution<T>| forall|a: A| #[trigger] a_to_temp_pred(a).satisfied_by(ex))
187}
188
189/// `\E` for temporal predicates in TLA+ (i.e., `exists` in Verus).
190pub open spec fn tla_exists<T, A>(a_to_temp_pred: spec_fn(A) -> TempPred<T>) -> TempPred<T> {
191    TempPred::new(|ex: Execution<T>| exists|a: A| #[trigger] a_to_temp_pred(a).satisfied_by(ex))
192}
193
194// |ex| temp_pred.satisfied_by(ex) ==> forall |i: nat| temp_pred.satisfied_by(ex.suffix(i))
195pub open spec fn stable<T>(temp_pred: TempPred<T>) -> TempPred<T> {
196    //TempPred::new(|ex: Execution<T>| temp_pred.implies(always(temp_pred)).satisfied_by(ex))
197    temp_pred.implies(always(temp_pred))
198}
199
200// Returns a state predicate that is satisfied
201// iff `action_pred` can be satisfied by any possible following state and the current state
202//
203// enabled() is used for checking whether a particular action is enabled at this **state**
204//
205// Note: it says whether the action *can possibly* happen, rather than whether the action *actually does* happen!
206pub open spec fn enabled<T>(action_pred: ActionPred<T>) -> StatePred<T> {
207    StatePred::new(|s: T| exists|s_prime: T| #[trigger] action_pred.apply(s, s_prime))
208}
209
210// Returns a temporal predicate that is satisfied
211// iff `always(lift_state(enabled(action_pred)))` getting satisfied leads to `lift_action(action_pred)` getting satisfied.
212//
213// It says whether it is *always* the case that if the action is *always* enabled, the action *eventually* happens.
214//
215// Defined in 5.3 in a different form.
216// We can prove the two forms are the same:
217//    []E(A) ~> A
218// == []([]E(A) => <>A)
219// == [](~[]E(A) \/ <>A)
220// == [](~~<>~E(A) \/ <>A)  <--- apply always_to_eventually
221// == [](<>~E(A) \/ <>A)
222// == []<>(~E(A) \/ A)      <--- apply eventually_or
223// == []<>~E(A) \/ []<>A    <--- apply always_eventually_distrib
224// == []<>A \/ []<>~E(A)
225pub open spec fn weak_fairness<T>(action_pred: ActionPred<T>) -> TempPred<T> {
226    always(lift_state(enabled(action_pred))).leads_to(lift_action(action_pred))
227}
228
229// `|=` for temporal predicates in TLA+.
230// Returns true iff `temp_pred` is satisfied by all possible executions (behaviors).
231//
232// Defined in 3.3.
233pub open spec fn valid<T>(temp_pred: TempPred<T>) -> bool {
234    forall|ex: Execution<T>| temp_pred.satisfied_by(ex)
235}
236
237pub open spec fn true_pred<T>() -> TempPred<T> {
238    TempPred::new(|_ex: Execution<T>| true)
239}
240
241pub open spec fn false_pred<T>() -> TempPred<T> {
242    TempPred::new(|_ex: Execution<T>| false)
243}
244
245pub open spec fn lift_state_forall<T, A>(a_to_state_pred: spec_fn(A) -> StatePred<T>) -> TempPred<
246    T,
247> {
248    lift_state(StatePred::state_forall(a_to_state_pred))
249}
250
251pub open spec fn lift_state_exists<T, A>(a_to_state_pred: spec_fn(A) -> StatePred<T>) -> TempPred<
252    T,
253> {
254    lift_state(StatePred::state_exists(a_to_state_pred))
255}
256
257} // verus!
vstd_extra/temporal_logic/defs.rs

vstd_extra/temporal_logic/
defs.rs
