nucleus/isolation/
state.rs

1use crate::error::StateTransition;
2
3/// Namespace lifecycle state machine matching Nucleus_Isolation_NamespaceLifecycle.tla
4///
5/// State transitions:
6/// uninitialized -> unshared -> entered -> cleaned
7///
8/// Properties verified by TLA+ model:
9/// - isolation_integrity: Once entered, can only move to entered or cleaned
10/// - cleanup_happens: If entered, eventually cleaned
11#[derive(Debug, Clone, Copy, PartialEq, Eq)]
12pub enum NamespaceState {
13    /// Initial state before namespace creation
14    Uninitialized,
15    /// Namespaces created via unshare(2)
16    Unshared,
17    /// Process entered the namespaces
18    Entered,
19    /// Namespaces cleaned up
20    Cleaned,
21}
22
23impl StateTransition for NamespaceState {
24    fn can_transition_to(&self, next: &NamespaceState) -> bool {
25        use NamespaceState::*;
26
27        matches!(
28            (self, next),
29            (Uninitialized, Unshared)
30                | (Unshared, Entered)
31                | (Entered, Cleaned)
32                | (Uninitialized, Uninitialized)
33                | (Unshared, Unshared)
34                | (Entered, Entered)
35                | (Cleaned, Cleaned)
36        )
37    }
38
39    fn is_terminal(&self) -> bool {
40        matches!(self, NamespaceState::Cleaned)
41    }
42}
43
44#[cfg(test)]
45mod tests {
46    use super::*;
47
48    #[test]
49    fn test_valid_transitions() {
50        assert!(NamespaceState::Uninitialized.can_transition_to(&NamespaceState::Unshared));
51        assert!(NamespaceState::Unshared.can_transition_to(&NamespaceState::Entered));
52        assert!(NamespaceState::Entered.can_transition_to(&NamespaceState::Cleaned));
53    }
54
55    #[test]
56    fn test_invalid_transitions() {
57        // Cannot skip states
58        assert!(!NamespaceState::Uninitialized.can_transition_to(&NamespaceState::Entered));
59        assert!(!NamespaceState::Uninitialized.can_transition_to(&NamespaceState::Cleaned));
60        assert!(!NamespaceState::Unshared.can_transition_to(&NamespaceState::Cleaned));
61
62        // Cannot go backwards
63        assert!(!NamespaceState::Entered.can_transition_to(&NamespaceState::Unshared));
64        assert!(!NamespaceState::Cleaned.can_transition_to(&NamespaceState::Entered));
65    }
66
67    #[test]
68    fn test_terminal_state() {
69        assert!(!NamespaceState::Uninitialized.is_terminal());
70        assert!(!NamespaceState::Unshared.is_terminal());
71        assert!(!NamespaceState::Entered.is_terminal());
72        assert!(NamespaceState::Cleaned.is_terminal());
73    }
74}
nucleus/isolation/state.rs

nucleus/isolation/
state.rs
