Follow-up to PR #62 (crash-consistency keystone). See docs/THEORY-CRASH-CONSISTENCY.adoc § Frontier B and docs/POSIX-2024-NOTES.md.
Three classes the current model does not cover
- Sub-second mtime (
struct timespec in stat). Crash between mtime write and data write can leave mtime ahead of data. Keystone model has no clock; needs (Filesystem, Clock) pair.
copy_file_range(2). Linux: reflink branch (atomic) vs fallback loop (non-atomic per-chunk). Modelling must expose the distinction.ioctl(FICLONE) / FICLONERANGE. Reflink semantics — two-filesystem transition (source + destination), source unaffected.
Proposed approach
Extend the Op inductive with clone, copy_range, touch_mtime. Extend Filesystem to { tree : Path → Option FSNode, clock : Time }. Re-prove the keystone for each constructor.
Tier: S (Foundational gap, POSIX-2024-conformance critical).
Follow-up to PR #62 (crash-consistency keystone). See
docs/THEORY-CRASH-CONSISTENCY.adoc§ Frontier B anddocs/POSIX-2024-NOTES.md.Three classes the current model does not cover
struct timespecinstat). Crash between mtime write and data write can leave mtime ahead of data. Keystone model has no clock; needs(Filesystem, Clock)pair.copy_file_range(2). Linux: reflink branch (atomic) vs fallback loop (non-atomic per-chunk). Modelling must expose the distinction.ioctl(FICLONE)/FICLONERANGE. Reflink semantics — two-filesystem transition (source + destination), source unaffected.Proposed approach
Extend the
Opinductive withclone,copy_range,touch_mtime. ExtendFilesystemto{ tree : Path → Option FSNode, clock : Time }. Re-prove the keystone for each constructor.Tier: S (Foundational gap, POSIX-2024-conformance critical).