planarian_txn/
machine.rs

1//! The journal state machine: which `TxnState` may follow which (§12).
2//! Pure; a Verus proof target (I12 paths, write-ahead ordering).
3
4use planarian_schema::{RecoveryStrategy, TxnState};
5use vstd::prelude::*;
6
7verus! {
8
9/// Whether a transaction with recovery strategy `strategy` may move from `from` to `to`.
10///
11/// Encodes §12 step 7 and the crash-recovery table:
12/// - Rejected/Cancelled only before any mutation.
13/// - `ReobserveOnly` never reverts and never publishes (Runtime outcomes never
14///   trigger generation reversion); it may commit from Activating (crash table).
15/// - Only generation operations pass through Published and Promoted.
16/// - The boot-only path (§12 step 7, §12f): Built → Publishing (journaled
17///   before the first boot mutation) → AwaitingBoot (a one-shot next-boot
18///   entry is armed) → Promoted (it booted and was admitted) or Reverted (it
19///   did not; the boot loader already fell back), or Reverting to withdraw the
20///   entry. From Publishing, a crash with no entry armed ends Rejected: the
21///   publication is all or nothing, so nothing was mutated.
22/// - Any state in which mutation may have happened can end in RecoveryFailed.
23pub open spec fn step_spec(from: TxnState, to: TxnState, strategy: RecoveryStrategy) -> bool {
24    let generation = strategy.reverts_generation();
25    let runtime = strategy == RecoveryStrategy::ReobserveOnly;
26    if from.terminal() {
27        false
28    } else {
29        match (from, to) {
30            (TxnState::Prepared, TxnState::Staged) => true,
31            (TxnState::Prepared, TxnState::Built) => true,
32            (TxnState::Prepared, TxnState::Activating) => true,
33            (TxnState::Staged, TxnState::Built) => true,
34            (TxnState::Staged, TxnState::Activating) => true,
35            (TxnState::Built, TxnState::Activating) => true,
36            (TxnState::Built, TxnState::Publishing) => generation,
37            (TxnState::Publishing, TxnState::AwaitingBoot) => generation,
38            (TxnState::Publishing, TxnState::Rejected(_)) => generation,
39            (TxnState::AwaitingBoot, TxnState::Promoted) => generation,
40            (TxnState::AwaitingBoot, TxnState::Reverting) => generation,
41            (TxnState::AwaitingBoot, TxnState::Reverted) => generation,
42            (_, TxnState::Rejected(_)) => from.pre_mutation(),
43            (_, TxnState::Cancelled(_)) => from.pre_mutation(),
44            (TxnState::Activating, TxnState::Checking) => true,
45            (TxnState::Activating, TxnState::Committed) => runtime,
46            (TxnState::Activating, TxnState::Reverting) => !runtime,
47            (TxnState::Checking, TxnState::Reverting) => !runtime,
48            (TxnState::Published, TxnState::Reverting) => !runtime,
49            (TxnState::Promoted, TxnState::Reverting) => !runtime,
50            (TxnState::Checking, TxnState::Committed) => runtime || strategy == RecoveryStrategy::UnbindDevice,
51            (TxnState::Checking, TxnState::Published) => generation,
52            (TxnState::Published, TxnState::Promoted) => generation,
53            (TxnState::Promoted, TxnState::Committed) => generation,
54            (TxnState::Reverting, TxnState::Reverted) => true,
55            (_, TxnState::RecoveryFailed) => !from.pre_mutation(),
56            _ => false,
57        }
58    }
59}
60
61pub fn step_allowed(from: &TxnState, to: &TxnState, strategy: RecoveryStrategy) -> (r: bool)
62    ensures
63        r == step_spec(*from, *to, strategy),
64{
65    let generation = match strategy {
66        RecoveryStrategy::RevertGeneration | RecoveryStrategy::RestoreSnapshotThenRevert => true,
67        _ => false,
68    };
69    let runtime = match strategy {
70        RecoveryStrategy::ReobserveOnly => true,
71        _ => false,
72    };
73    let device = match strategy {
74        RecoveryStrategy::UnbindDevice => true,
75        _ => false,
76    };
77    if from.is_terminal() {
78        return false;
79    }
80    match (from, to) {
81        (TxnState::Prepared, TxnState::Staged) => true,
82        (TxnState::Prepared, TxnState::Built) => true,
83        (TxnState::Prepared, TxnState::Activating) => true,
84        (TxnState::Staged, TxnState::Built) => true,
85        (TxnState::Staged, TxnState::Activating) => true,
86        (TxnState::Built, TxnState::Activating) => true,
87        (TxnState::Built, TxnState::Publishing) => generation,
88        (TxnState::Publishing, TxnState::AwaitingBoot) => generation,
89        (TxnState::Publishing, TxnState::Rejected(_)) => generation,
90        (TxnState::AwaitingBoot, TxnState::Promoted) => generation,
91        (TxnState::AwaitingBoot, TxnState::Reverting) => generation,
92        (TxnState::AwaitingBoot, TxnState::Reverted) => generation,
93        (_, TxnState::Rejected(_)) => from.is_pre_mutation(),
94        (_, TxnState::Cancelled(_)) => from.is_pre_mutation(),
95        (TxnState::Activating, TxnState::Checking) => true,
96        (TxnState::Activating, TxnState::Committed) => runtime,
97        (TxnState::Activating, TxnState::Reverting) => !runtime,
98        (TxnState::Checking, TxnState::Reverting) => !runtime,
99        (TxnState::Published, TxnState::Reverting) => !runtime,
100        (TxnState::Promoted, TxnState::Reverting) => !runtime,
101        (TxnState::Checking, TxnState::Committed) => runtime || device,
102        (TxnState::Checking, TxnState::Published) => generation,
103        (TxnState::Published, TxnState::Promoted) => generation,
104        (TxnState::Promoted, TxnState::Committed) => generation,
105        (TxnState::Reverting, TxnState::Reverted) => true,
106        (_, TxnState::RecoveryFailed) => !from.is_pre_mutation(),
107        _ => false,
108    }
109}
110
111/// How far a state is from the end: every allowed step lowers it.
112pub open spec fn rank(s: TxnState) -> nat {
113    match s {
114        TxnState::Prepared => 8,
115        TxnState::Staged => 7,
116        TxnState::Built => 6,
117        TxnState::Activating => 5,
118        TxnState::Checking => 4,
119        TxnState::Publishing => 4,
120        TxnState::Published => 3,
121        TxnState::AwaitingBoot => 3,
122        TxnState::Promoted => 2,
123        TxnState::Reverting => 1,
124        _ => 0,
125    }
126}
127
128/// I12, termination: every allowed step lowers the rank, so a transaction
129/// takes at most eight steps and never cycles.
130pub proof fn i12_steps_terminate(from: TxnState, to: TxnState, strategy: RecoveryStrategy)
131    requires
132        step_spec(from, to, strategy),
133    ensures
134        rank(to) < rank(from),
135{
136}
137
138/// I12, progress: from every state that is not terminal, a step to a
139/// terminal state is allowed: Cancelled before any mutation, RecoveryFailed
140/// after. So whoever holds the lease can always finish the transaction.
141pub proof fn i12_terminal_always_reachable(from: TxnState, strategy: RecoveryStrategy, by: planarian_schema::Actor)
142    requires
143        !from.terminal(),
144    ensures
145        from.pre_mutation() ==> step_spec(from, TxnState::Cancelled(by), strategy),
146        !from.pre_mutation() ==> step_spec(from, TxnState::RecoveryFailed, strategy),
147{
148}
149
150/// Terminal states have no successors.
151pub proof fn terminal_is_final(from: TxnState, to: TxnState, strategy: RecoveryStrategy)
152    requires
153        from.terminal(),
154    ensures
155        !step_spec(from, to, strategy),
156{
157}
158
159/// Rejected and Cancelled happen only before anything was mutated, or (for
160/// Rejected) from Publishing, whose all-or-nothing publication armed nothing.
161pub proof fn refusal_only_before_mutation(from: TxnState, to: TxnState, strategy: RecoveryStrategy)
162    requires
163        step_spec(from, to, strategy),
164        to is Rejected || to is Cancelled,
165    ensures
166        from.pre_mutation() || (from is Publishing && to is Rejected),
167{
168}
169
170/// Runtime operations never revert a generation and never publish (§12).
171pub proof fn runtime_never_reverts(from: TxnState, to: TxnState)
172    requires
173        step_spec(from, to, RecoveryStrategy::ReobserveOnly),
174    ensures
175        !(to is Reverting),
176        !(to is Published),
177        !(to is Promoted),
178{
179}
180
181/// Only generation operations publish a boot entry (also a one-shot one) or promote overrides.
182pub proof fn only_generations_publish(from: TxnState, to: TxnState, strategy: RecoveryStrategy)
183    requires
184        step_spec(from, to, strategy),
185        to is Published || to is Promoted || to is Publishing || to is AwaitingBoot,
186    ensures
187        strategy.reverts_generation(),
188{
189}
190
191/// A boot-only candidate is never live-activated: Publishing is journaled
192/// before any boot mutation (R01), AwaitingBoot is reached only through it,
193/// and left only for Promoted or a revert.
194pub proof fn boot_only_never_activates(from: TxnState, to: TxnState, strategy: RecoveryStrategy)
195    requires
196        step_spec(from, to, strategy),
197    ensures
198        to is Publishing ==> from is Built,
199        to is AwaitingBoot ==> from is Publishing,
200        from is Publishing ==> (to is AwaitingBoot || to is Rejected || to is RecoveryFailed),
201        from is AwaitingBoot ==> (to is Promoted || to is Reverting || to is Reverted || to is RecoveryFailed),
202{
203}
204
205/// A generation operation commits only after it was published and promoted.
206pub proof fn generations_commit_after_promotion(from: TxnState, strategy: RecoveryStrategy)
207    requires
208        step_spec(from, TxnState::Committed, strategy),
209        strategy.reverts_generation(),
210    ensures
211        from is Promoted,
212{
213}
214
215/// A short, stable name for a state (journal notes, crash points, catalog `path`).
216pub fn tag(s: &TxnState) -> &'static str {
217    match s {
218        TxnState::Prepared => "Prepared",
219        TxnState::Staged => "Staged",
220        TxnState::Built => "Built",
221        TxnState::Activating => "Activating",
222        TxnState::Checking => "Checking",
223        TxnState::Published => "Published",
224        TxnState::Publishing => "Publishing",
225        TxnState::AwaitingBoot => "AwaitingBoot",
226        TxnState::Promoted => "Promoted",
227        TxnState::Committed => "Committed",
228        TxnState::Reverting => "Reverting",
229        TxnState::Reverted => "Reverted",
230        TxnState::RecoveryFailed => "RecoveryFailed",
231        TxnState::Rejected(_) => "Rejected",
232        TxnState::Cancelled(_) => "Cancelled",
233    }
234}
235
236} // verus!
237
238#[cfg(test)]
239mod tests {
240    use super::*;
241    use planarian_schema::{Actor, RejectReason};
242
243    fn all() -> Vec<TxnState> {
244        vec![
245            TxnState::Prepared,
246            TxnState::Staged,
247            TxnState::Built,
248            TxnState::Activating,
249            TxnState::Checking,
250            TxnState::Published,
251            TxnState::Publishing,
252            TxnState::AwaitingBoot,
253            TxnState::Promoted,
254            TxnState::Committed,
255            TxnState::Reverting,
256            TxnState::Reverted,
257            TxnState::RecoveryFailed,
258            TxnState::Rejected(RejectReason::Stale),
259            TxnState::Cancelled(Actor::user(1000)),
260        ]
261    }
262
263    const STRATEGIES: [RecoveryStrategy; 4] = [
264        RecoveryStrategy::ReobserveOnly,
265        RecoveryStrategy::RevertGeneration,
266        RecoveryStrategy::UnbindDevice,
267        RecoveryStrategy::RestoreSnapshotThenRevert,
268    ];
269
270    /// Every non-terminal state has a path to a terminal state (the
271    /// reachability half of I12), for every strategy.
272    #[test]
273    fn terminal_reachable_from_every_state() {
274        for strategy in STRATEGIES {
275            for start in all().iter().filter(|s| !s.is_terminal()) {
276                let mut seen = vec![start.clone()];
277                let mut frontier = vec![start.clone()];
278                let mut reached = false;
279                while let Some(s) = frontier.pop() {
280                    for t in all() {
281                        if step_allowed(&s, &t, strategy) && !seen.contains(&t) {
282                            reached |= t.is_terminal();
283                            seen.push(t.clone());
284                            frontier.push(t);
285                        }
286                    }
287                }
288                // Published/Promoted exist only for generation operations; for the
289                // others those states are unreachable, so they need no exit.
290                let reachable_at_all = !matches!(start, TxnState::Published | TxnState::Promoted)
291                    || matches!(
292                        strategy,
293                        RecoveryStrategy::RevertGeneration | RecoveryStrategy::RestoreSnapshotThenRevert
294                    );
295                assert!(reached || !reachable_at_all, "{start:?} under {strategy:?} cannot terminate");
296            }
297        }
298    }
299
300    #[test]
301    fn terminal_states_are_final() {
302        for strategy in STRATEGIES {
303            for from in all().iter().filter(|s| s.is_terminal()) {
304                for to in all() {
305                    assert!(!step_allowed(from, &to, strategy));
306                }
307            }
308        }
309    }
310
311    #[test]
312    fn reobserve_only_never_reverts_or_publishes() {
313        let r = RecoveryStrategy::ReobserveOnly;
314        for from in all() {
315            assert!(!step_allowed(&from, &TxnState::Reverting, r));
316            assert!(!step_allowed(&from, &TxnState::Published, r));
317        }
318    }
319
320    #[test]
321    fn no_reject_after_mutation() {
322        for strategy in STRATEGIES {
323            for from in [TxnState::Activating, TxnState::Checking, TxnState::Reverting] {
324                assert!(!step_allowed(&from, &TxnState::Rejected(RejectReason::Stale), strategy));
325            }
326        }
327    }
328}
planarian_txn/machine.rs

planarian_txn/
machine.rs
