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        // L9: Added Unshared->Cleaned transition for cleanup from
28        // partially-initialized state (e.g., error during namespace setup).
29        matches!(
30            (self, next),
31            (Uninitialized, Unshared)
32                | (Unshared, Entered)
33                | (Unshared, Cleaned)
34                | (Entered, Cleaned)
35                | (Uninitialized, Uninitialized)
36                | (Unshared, Unshared)
37                | (Entered, Entered)
38                | (Cleaned, Cleaned)
39        )
40    }
41
42    fn is_terminal(&self) -> bool {
43        matches!(self, NamespaceState::Cleaned)
44    }
45}
46
47#[cfg(test)]
48mod tests {
49    use super::*;
50
51    #[test]
52    fn test_valid_transitions() {
53        assert!(NamespaceState::Uninitialized.can_transition_to(&NamespaceState::Unshared));
54        assert!(NamespaceState::Unshared.can_transition_to(&NamespaceState::Entered));
55        assert!(NamespaceState::Entered.can_transition_to(&NamespaceState::Cleaned));
56    }
57
58    #[test]
59    fn test_unshared_to_cleaned() {
60        // L9: Cleanup from partially-initialized state
61        assert!(NamespaceState::Unshared.can_transition_to(&NamespaceState::Cleaned));
62    }
63
64    #[test]
65    fn test_invalid_transitions() {
66        // Cannot skip states
67        assert!(!NamespaceState::Uninitialized.can_transition_to(&NamespaceState::Entered));
68        assert!(!NamespaceState::Uninitialized.can_transition_to(&NamespaceState::Cleaned));
69
70        // Cannot go backwards
71        assert!(!NamespaceState::Entered.can_transition_to(&NamespaceState::Unshared));
72        assert!(!NamespaceState::Cleaned.can_transition_to(&NamespaceState::Entered));
73    }
74
75    #[test]
76    fn test_terminal_state() {
77        assert!(!NamespaceState::Uninitialized.is_terminal());
78        assert!(!NamespaceState::Unshared.is_terminal());
79        assert!(!NamespaceState::Entered.is_terminal());
80        assert!(NamespaceState::Cleaned.is_terminal());
81    }
82}
nucleus/isolation/state.rs

nucleus/isolation/
state.rs
