nucleus/filesystem/
state.rs

1use crate::error::StateTransition;
2
3/// Filesystem lifecycle state machine matching Nucleus_Filesystem_FilesystemLifecycle.tla
4///
5/// State transitions:
6/// unmounted -> mounted -> populated -> pivoted -> unmounted_final
7///
8/// Properties verified by TLA+ model:
9/// - context_isolation: Once pivoted, can only move to pivoted or unmounted_final
10/// - ephemeral_guarantee: unmounted_final is terminal and stable
11/// - mount_ordering: populated can only transition to pivoted or unmounted_final
12#[derive(Debug, Clone, Copy, PartialEq, Eq)]
13pub enum FilesystemState {
14    /// Initial state - no filesystem mounted
15    Unmounted,
16    /// tmpfs mounted
17    Mounted,
18    /// Context files populated
19    Populated,
20    /// Root switched via pivot_root
21    Pivoted,
22    /// Final cleanup - terminal state
23    UnmountedFinal,
24}
25
26impl StateTransition for FilesystemState {
27    fn can_transition_to(&self, next: &FilesystemState) -> bool {
28        use FilesystemState::*;
29
30        matches!(
31            (self, next),
32            (Unmounted, Mounted)
33                | (Mounted, Populated)
34                | (Populated, Pivoted)
35                | (Mounted, Unmounted)
36                | (Populated, Unmounted)
37                | (Pivoted, UnmountedFinal)
38                | (Unmounted, Unmounted)
39                | (Mounted, Mounted)
40                | (Populated, Populated)
41                | (Pivoted, Pivoted)
42                | (UnmountedFinal, UnmountedFinal)
43        )
44    }
45
46    fn is_terminal(&self) -> bool {
47        matches!(self, FilesystemState::UnmountedFinal)
48    }
49}
50
51#[cfg(test)]
52mod tests {
53    use super::*;
54
55    #[test]
56    fn test_valid_transitions() {
57        assert!(FilesystemState::Unmounted.can_transition_to(&FilesystemState::Mounted));
58        assert!(FilesystemState::Mounted.can_transition_to(&FilesystemState::Populated));
59        assert!(FilesystemState::Populated.can_transition_to(&FilesystemState::Pivoted));
60        assert!(FilesystemState::Pivoted.can_transition_to(&FilesystemState::UnmountedFinal));
61    }
62
63    #[test]
64    fn test_invalid_transitions() {
65        // Cannot skip states
66        assert!(!FilesystemState::Unmounted.can_transition_to(&FilesystemState::Populated));
67        assert!(!FilesystemState::Mounted.can_transition_to(&FilesystemState::Pivoted));
68
69        // Cannot go backwards
70        assert!(!FilesystemState::Pivoted.can_transition_to(&FilesystemState::Populated));
71        assert!(!FilesystemState::UnmountedFinal.can_transition_to(&FilesystemState::Pivoted));
72    }
73
74    #[test]
75    fn test_terminal_state() {
76        assert!(!FilesystemState::Unmounted.is_terminal());
77        assert!(!FilesystemState::Mounted.is_terminal());
78        assert!(!FilesystemState::Populated.is_terminal());
79        assert!(!FilesystemState::Pivoted.is_terminal());
80        assert!(FilesystemState::UnmountedFinal.is_terminal());
81    }
82
83    #[test]
84    fn test_cleanup_transitions() {
85        // BUG-10: Mounted and Populated must be able to transition to Unmounted (cleanup)
86        assert!(
87            FilesystemState::Mounted.can_transition_to(&FilesystemState::Unmounted),
88            "Mounted must be able to transition back to Unmounted for cleanup"
89        );
90        assert!(
91            FilesystemState::Populated.can_transition_to(&FilesystemState::Unmounted),
92            "Populated must be able to transition back to Unmounted for cleanup"
93        );
94    }
95}
nucleus/filesystem/state.rs

nucleus/filesystem/
state.rs
