Follow-up to PR #62 (crash-consistency keystone). See docs/THEORY-CRASH-CONSISTENCY.adoc § Frontier D.
Statement
Below the filesystem is the block device. A mkdir(2) the kernel reports as committed may still be in the drive's volatile write cache when power fails. The keystone presupposes write barriers (fsync, fdatasync, FUA) have done their job; if they haven't, the post-state observable to the next boot is neither the keystone's pre- nor post-state — it is a hardware-level torn state.
Proposed approach (modelling boundary, not proof obligation)
- Document the assumption explicitly: every modelled
FilesystemOp is followed by a barrier sufficient for durability before any subsequent op starts.
- Annotate ops in
proofs/lean4/FilesystemModel.lean with the barrier each one assumes (directory ops: fsync on parent; file ops: fsync on file and parent).
- Cross-check against the Rust implementation in
impl/rust/; file gap-tickets for any missing barrier call.
Why this is a boundary, not a proof
A proof system cannot promise what the firmware will do. The honest move is to state the boundary explicitly and audit the implementation against it.
Tier: S (Foundational gap, modelling-boundary class).
Follow-up to PR #62 (crash-consistency keystone). See
docs/THEORY-CRASH-CONSISTENCY.adoc§ Frontier D.Statement
Below the filesystem is the block device. A
mkdir(2)the kernel reports as committed may still be in the drive's volatile write cache when power fails. The keystone presupposes write barriers (fsync,fdatasync,FUA) have done their job; if they haven't, the post-state observable to the next boot is neither the keystone's pre- nor post-state — it is a hardware-level torn state.Proposed approach (modelling boundary, not proof obligation)
FilesystemOpis followed by a barrier sufficient for durability before any subsequent op starts.proofs/lean4/FilesystemModel.leanwith the barrier each one assumes (directory ops:fsyncon parent; file ops:fsyncon file and parent).impl/rust/; file gap-tickets for any missing barrier call.Why this is a boundary, not a proof
A proof system cannot promise what the firmware will do. The honest move is to state the boundary explicitly and audit the implementation against it.
Tier: S (Foundational gap, modelling-boundary class).