Current Behavior
The formal model in src/proof.rs proves that migration steps, rollback, and
kernel install preserve bootability. These proofs assume
kernel_install_dispatches_hooks as a static boolean axiom: either the hook
exists or it does not.
In reality, the hook's existence is dynamic state that changes with package
install/uninstall. The model cannot prove that arbitrary orderings of
install, uninstall, and migrate produce safe states, because it does not
model those transitions.
The Gap
The model lacks state transitions for:
- install_package: hook appears, plugins appear
- uninstall_package: hook disappears, plugins disappear
These interact with the permanent layout change from migrate. The unsafe
sequence (install, migrate, uninstall, kernel update) is not representable
in the current model.
kernel_install_dispatches_hooks should be mutable system state (set by
install_package/migrate, cleared by uninstall_package) rather than a static
axiom. The model should then prove that every reachable state after
migration either has the hook present or refuses kernel installs.
Context
The most critical unsafe sequence (issue #17: kernel installs after package
removal on migrated systems) is being addressed in v0.4.0 by making migrate
write the hook instead of the RPM owning it. That code fix makes the hook
persist after removal, closing the practical gap.
This issue tracks the remaining formal gap: the model should be extended to
cover package lifecycle transitions so the safety of arbitrary orderings is
proven, not just believed.
Scope
Current Behavior
The formal model in src/proof.rs proves that migration steps, rollback, and
kernel install preserve bootability. These proofs assume
kernel_install_dispatches_hooks as a static boolean axiom: either the hook
exists or it does not.
In reality, the hook's existence is dynamic state that changes with package
install/uninstall. The model cannot prove that arbitrary orderings of
install, uninstall, and migrate produce safe states, because it does not
model those transitions.
The Gap
The model lacks state transitions for:
These interact with the permanent layout change from migrate. The unsafe
sequence (install, migrate, uninstall, kernel update) is not representable
in the current model.
kernel_install_dispatches_hooks should be mutable system state (set by
install_package/migrate, cleared by uninstall_package) rather than a static
axiom. The model should then prove that every reachable state after
migration either has the hook present or refuses kernel installs.
Context
The most critical unsafe sequence (issue #17: kernel installs after package
removal on migrated systems) is being addressed in v0.4.0 by making migrate
write the hook instead of the RPM owning it. That code fix makes the hook
persist after removal, closing the practical gap.
This issue tracks the remaining formal gap: the model should be extended to
cover package lifecycle transitions so the safety of arbitrary orderings is
proven, not just believed.
Scope
package_not_installed produces an unsafe kernel install
close the gap in the model