docs+annotate: Filesystem cluster — 26 inline AXIOM: + 8 §(d) DEBT entries (Phase 2c)

hyperpolymath · claude · hyperpolymath · commit d5c2cf92885e · 2026-05-27T09:29:09.000+01:00
Phase 2c of the standards#203 trusted-base rollout. Largest single cluster: Coq + Lean Filesystem (34 markers total — 13 Coq + 21 Lean). Coq side (13 markers, classifications from #58 Phase 1 triage): - 8 §(c) AXIOM inline annotations: - L96 fs_eq_dec (treat as §(c) until property-test budget lands; promote to §(b)) - L104 mkdir_rmdir_inverse, L114 create_unlink_inverse, L124 read_write_identity, L130 chmod_identity, L136 chown_identity, L142 rename_identity, L147 rename_inverse — POSIX-semantics specifications. - 5 §(d) DEBT entries (no inline; enumerated in docs/proof-debt.md): mkdir_not_identity (L300), write_different_not_identity (L316), transaction_cno (L397), mkdir_idempotent (L421), snapshot_restore_identity (L453). All DISCHARGE candidates in #58. Lean side (21 markers, new Phase 2c triage): - 18 §(c) AXIOM inline annotations: - 10 POSIX primitives (mkdir/rmdir/create/unlink/readFile/writeFile/ stat/chmod/chown/rename) — opaque ops. - 6 POSIX semantics axioms (mirror Coq §(c)). - 2 snapshot primitives (snapshot, restore) — opaque ops. - 3 §(d) DEBT entries (mirror Coq DISCHARGE): mkdir_not_identity (L233), snapshot_restore_identity (L288), mkdir_idempotent (L309). `docs/proof-debt.md`: - New "Phase 2c triage — Lean Filesystem cluster" section with full per-marker tables (primitives / semantics / snapshot / discharge). - §(d) DEBT bucket gains 8 new Filesystem entries (5 Coq + 3 Lean), each with owner + INDEFINITE deadline. - "Lean — pending triage" count updates from 49 → 28. Verification: `check-trusted-base.sh` now reports 88/129 undocumented (down from 122 after #61, 123 after #60). Delta of 34 matches the cluster size exactly. 0 Filesystem-specific errors remain. Refs standards#203, #58, #60, #61. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
diff --git a/docs/proof-debt.md b/docs/proof-debt.md
@@ -45,6 +45,58 @@ First cluster: `proofs/lean4/LambdaCNO.lean` (3 axioms).
 The two §(c) entries are annotated inline with `-- AXIOM:` leading
 comments. The §(d) entry below has an owner + deadline.
 
+## Phase 2c triage — Lean Filesystem cluster (2026-05-27)
+
+Second Lean cluster: `proofs/lean4/FilesystemCNO.lean` (21 axioms).
+
+### POSIX primitive operations (§(c) AXIOM — opaque ops, 10)
+
+| Line | Identifier | Disposition | Justification |
+|-----:|------------|-------------|---------------|
+|  56  | `mkdir`     | §(c) AXIOM | Opaque POSIX primitive — no executable body in the model. |
+|  60  | `rmdir`     | §(c) AXIOM | Opaque POSIX primitive. |
+|  64  | `create`    | §(c) AXIOM | Opaque POSIX primitive. |
+|  68  | `unlink`    | §(c) AXIOM | Opaque POSIX primitive. |
+|  72  | `readFile`  | §(c) AXIOM | Opaque POSIX primitive. |
+|  76  | `writeFile` | §(c) AXIOM | Opaque POSIX primitive. |
+|  80  | `stat`      | §(c) AXIOM | Opaque POSIX primitive. |
+|  84  | `chmod`     | §(c) AXIOM | Opaque POSIX primitive. |
+|  88  | `chown`     | §(c) AXIOM | Opaque POSIX primitive. |
+|  92  | `rename`    | §(c) AXIOM | Opaque POSIX primitive. |
+
+### POSIX semantics specifications (§(c) AXIOM — mirror Coq, 6)
+
+| Line | Identifier | Disposition |
+|-----:|------------|-------------|
+|  98  | `mkdir_rmdir_inverse`  | §(c) AXIOM (mirrors Coq) |
+| 104  | `create_unlink_inverse`| §(c) AXIOM (mirrors Coq) |
+| 109  | `read_write_identity`  | §(c) AXIOM (mirrors Coq) |
+| 115  | `chmod_identity`       | §(c) AXIOM (mirrors Coq) |
+| 121  | `rename_identity`      | §(c) AXIOM (mirrors Coq) |
+| 126  | `rename_inverse`       | §(c) AXIOM (mirrors Coq) |
+
+### Snapshot primitives (§(c) AXIOM — opaque ops, 2)
+
+| Line | Identifier | Disposition |
+|-----:|------------|-------------|
+| 281  | `snapshot` | §(c) AXIOM (opaque snapshot primitive) |
+| 285  | `restore`  | §(c) AXIOM (opaque restore primitive) |
+
+### Discharge candidates (§(d) DEBT — 3)
+
+These claim provable existence / equality facts that should follow
+from the §(c) primitives once the model is concretely defined. They
+need a discharge PR — see §(d) DEBT below.
+
+| Line | Identifier | Disposition | Plan |
+|-----:|------------|-------------|------|
+| 233  | `mkdir_not_identity`         | §(d) DEBT | Existence proof; exhibit one concrete `fs` lacking the path. |
+| 288  | `snapshot_restore_identity`  | §(d) DEBT | Composite theorem; derivable from `snapshot`/`restore` once a concrete snapshot model lands. |
+| 309  | `mkdir_idempotent`           | §(d) DEBT | Follows from `mkdir_rmdir_inverse` family with stronger repeat-mkdir semantics. |
+
+All 18 §(c) entries above are annotated inline with `-- AXIOM:`
+leading comments.
+
 ## (a) DISCHARGE backlog (Coq, 17)
 
 Provable propositions currently stated as `Axiom`. Enumerated in
@@ -85,6 +137,38 @@ no longer in §(d).
   - **Deadline**: INDEFINITE (blocked on `SetCategory` instance —
     universe-polymorphism scaffolding precondition).
 
+- `proofs/coq/filesystem/FilesystemCNO.v:300` — `mkdir_not_identity`
+  - **Owner**: @hyperpolymath
+  - **Plan**: existence proof; exhibit one concrete `fs` lacking the
+    path. Triaged DISCHARGE in #58.
+  - **Deadline**: INDEFINITE (small proof; awaits a discharge PR).
+
+- `proofs/coq/filesystem/FilesystemCNO.v:316` — `write_different_not_identity`
+  - **Owner**: @hyperpolymath
+  - **Plan**: existence proof; exhibit one concrete content mismatch.
+    Triaged DISCHARGE in #58.
+  - **Deadline**: INDEFINITE.
+
+- `proofs/coq/filesystem/FilesystemCNO.v:397` — `transaction_cno`
+  - **Owner**: @hyperpolymath
+  - **Plan**: composite theorem; derivable from primitive `_inverse`
+    axioms once a `transaction` definition is in place. Triaged
+    DISCHARGE in #58.
+  - **Deadline**: INDEFINITE (blocked on `transaction` definition).
+
+- `proofs/coq/filesystem/FilesystemCNO.v:421` — `mkdir_idempotent`
+  - **Owner**: @hyperpolymath
+  - **Plan**: follows from `mkdir_rmdir_inverse` family + stronger
+    repeat-mkdir semantics. Triaged DISCHARGE in #58.
+  - **Deadline**: INDEFINITE.
+
+- `proofs/coq/filesystem/FilesystemCNO.v:453` — `snapshot_restore_identity`
+  - **Owner**: @hyperpolymath
+  - **Plan**: composite theorem; derivable from primitive `_identity`
+    / `_inverse` axioms once a snapshot model lands. Triaged DISCHARGE
+    in #58.
+  - **Deadline**: INDEFINITE.
+
 ### Lean — provable, awaiting proof
 
 - `proofs/lean4/LambdaCNO.lean:183` — `subst_closed_term`
@@ -95,11 +179,31 @@ no longer in §(d).
   - **Deadline**: INDEFINITE (no proof-PR scheduled yet — provable;
     awaits Lean-side discharge push).
 
+- `proofs/lean4/FilesystemCNO.lean:233` — `mkdir_not_identity`
+  - **Owner**: @hyperpolymath
+  - **Plan**: existence proof; exhibit one concrete `fs` lacking the
+    path. Mirrors Coq site at `FilesystemCNO.v:300`.
+  - **Deadline**: INDEFINITE.
+
+- `proofs/lean4/FilesystemCNO.lean:288` — `snapshot_restore_identity`
+  - **Owner**: @hyperpolymath
+  - **Plan**: composite theorem; derivable from `snapshot`/`restore`
+    primitives once a concrete snapshot model is in place. Mirrors
+    Coq site at `FilesystemCNO.v:453`.
+  - **Deadline**: INDEFINITE.
+
+- `proofs/lean4/FilesystemCNO.lean:309` — `mkdir_idempotent`
+  - **Owner**: @hyperpolymath
+  - **Plan**: follows from `mkdir_rmdir_inverse` + stronger
+    repeat-mkdir semantics. Mirrors Coq site at `FilesystemCNO.v:421`.
+  - **Deadline**: INDEFINITE.
+
 ### Lean — pending triage
 
-49 Lean axioms remain to be triaged (FilesystemCNO 21, QuantumCNO 14,
-StatMech 14). Triage planned in cluster-sized PRs through
-2026-06 — see this file's status block at the bottom.
+28 Lean axioms remain to be triaged (QuantumCNO 14, StatMech 14;
+Lambda and Filesystem clusters done in Phase 2a/2c). Triage planned
+in cluster-sized PRs through 2026-06 — see this file's status block
+at the bottom.
 
 ### Idris2 — pending triage
 
diff --git a/proofs/coq/filesystem/FilesystemCNO.v b/proofs/coq/filesystem/FilesystemCNO.v
@@ -93,6 +93,10 @@ Parameter rename : Path -> Path -> Filesystem -> Filesystem.
 (** ** Filesystem State Equality *)
 
 (** Two filesystems are equal if they have the same structure and content *)
+(* AXIOM: fs_eq_dec; decidable equality over opaque FileContent — currently
+   §(c) NECESSARY AXIOM; promote to §(b) TRUSTED with property-test budget
+   when a concrete FileContent type lands. See docs/proof-debt.md and
+   docs/proof-debt-triage.md row FilesystemCNO.v:96. *)
 Axiom fs_eq_dec : forall (fs1 fs2 : Filesystem), {fs1 = fs2} + {fs1 <> fs2}.
 
 (** Filesystem equality is an equivalence relation *)
@@ -101,6 +105,8 @@ Notation "fs1 =fs= fs2" := (fs1 = fs2) (at level 70).
 (** ** Operation Axioms *)
 
 (** mkdir followed by rmdir is identity (if directory doesn't exist initially) *)
+(* AXIOM: mkdir_rmdir_inverse; POSIX-semantics specification (model-layer);
+   §(c) per docs/proof-debt.md. *)
 Axiom mkdir_rmdir_inverse :
   forall (p : Path) (fs : Filesystem),
     (* Precondition: p doesn't exist *)
@@ -111,6 +117,7 @@ Axiom mkdir_rmdir_inverse :
     rmdir p (mkdir p fs) =fs= fs.
 
 (** create followed by unlink is identity (if file doesn't exist initially) *)
+(* AXIOM: create_unlink_inverse; POSIX-semantics specification; §(c) per docs/proof-debt.md. *)
 Axiom create_unlink_inverse :
   forall (p : Path) (fs : Filesystem),
     (* Precondition: p doesn't exist *)
@@ -121,29 +128,34 @@ Axiom create_unlink_inverse :
     unlink p (create p fs) =fs= fs.
 
 (** read followed by write is identity (preserves filesystem) *)
+(* AXIOM: read_write_identity; POSIX-semantics specification; §(c) per docs/proof-debt.md. *)
 Axiom read_write_identity :
   forall (p : Path) (fs : Filesystem) (content : FileContent),
     read_file p fs = Some content ->
     write_file p content fs =fs= fs.
 
 (** chmod to current permissions is identity *)
+(* AXIOM: chmod_identity; POSIX-semantics specification; §(c) per docs/proof-debt.md. *)
 Axiom chmod_identity :
   forall (p : Path) (fs : Filesystem) (meta : FileMetadata),
     stat p fs = Some meta ->
     chmod p (permissions meta) fs =fs= fs.
 
 (** chown to current owner is identity *)
+(* AXIOM: chown_identity; POSIX-semantics specification; §(c) per docs/proof-debt.md. *)
 Axiom chown_identity :
   forall (p : Path) (fs : Filesystem) (meta : FileMetadata),
     stat p fs = Some meta ->
     chown p (owner meta) fs =fs= fs.
 
 (** rename to same path is identity *)
+(* AXIOM: rename_identity; POSIX-semantics specification; §(c) per docs/proof-debt.md. *)
 Axiom rename_identity :
   forall (p : Path) (fs : Filesystem),
     rename p p fs =fs= fs.
 
 (** rename A to B followed by rename B to A is identity *)
+(* AXIOM: rename_inverse; POSIX-semantics specification; §(c) per docs/proof-debt.md. *)
 Axiom rename_inverse :
   forall (p1 p2 : Path) (fs : Filesystem),
     p1 <> p2 ->
diff --git a/proofs/lean4/FilesystemCNO.lean b/proofs/lean4/FilesystemCNO.lean
@@ -52,61 +52,77 @@ abbrev Filesystem : Type := List FileEntry
 /-! ## Filesystem Operations -/
 
 /-- Create directory -/
+-- AXIOM: mkdir; opaque POSIX primitive op; §(c) per docs/proof-debt.md.
 axiom mkdir : Path → Filesystem → Filesystem
 
 /-- Remove directory -/
+-- AXIOM: rmdir; opaque POSIX primitive op; §(c) per docs/proof-debt.md.
 axiom rmdir : Path → Filesystem → Filesystem
 
 /-- Create file -/
+-- AXIOM: create; opaque POSIX primitive op; §(c) per docs/proof-debt.md.
 axiom create : Path → Filesystem → Filesystem
 
 /-- Delete file -/
+-- AXIOM: unlink; opaque POSIX primitive op; §(c) per docs/proof-debt.md.
 axiom unlink : Path → Filesystem → Filesystem
 
 /-- Read file content -/
+-- AXIOM: readFile; opaque POSIX primitive op; §(c) per docs/proof-debt.md.
 axiom readFile : Path → Filesystem → Option FileContent
 
 /-- Write file content -/
+-- AXIOM: writeFile; opaque POSIX primitive op; §(c) per docs/proof-debt.md.
 axiom writeFile : Path → FileContent → Filesystem → Filesystem
 
 /-- Get file metadata -/
+-- AXIOM: stat; opaque POSIX primitive op; §(c) per docs/proof-debt.md.
 axiom stat : Path → Filesystem → Option FileMetadata
 
 /-- Change permissions -/
+-- AXIOM: chmod; opaque POSIX primitive op; §(c) per docs/proof-debt.md.
 axiom chmod : Path → PermSet → Filesystem → Filesystem
 
 /-- Change owner -/
+-- AXIOM: chown; opaque POSIX primitive op; §(c) per docs/proof-debt.md.
 axiom chown : Path → Nat → Filesystem → Filesystem
 
 /-- Rename/move file -/
+-- AXIOM: rename; opaque POSIX primitive op; §(c) per docs/proof-debt.md.
 axiom rename : Path → Path → Filesystem → Filesystem
 
 /-! ## Operation Axioms -/
 
 /-- mkdir followed by rmdir is identity -/
+-- AXIOM: mkdir_rmdir_inverse; POSIX-semantics specification (mirrors Coq); §(c) per docs/proof-debt.md.
 axiom mkdir_rmdir_inverse (p : Path) (fs : Filesystem) :
   -- Precondition: p doesn't exist
   rmdir p (mkdir p fs) = fs
 
 /-- create followed by unlink is identity -/
+-- AXIOM: create_unlink_inverse; POSIX-semantics specification (mirrors Coq); §(c) per docs/proof-debt.md.
 axiom create_unlink_inverse (p : Path) (fs : Filesystem) :
   unlink p (create p fs) = fs
 
 /-- read followed by write is identity -/
+-- AXIOM: read_write_identity; POSIX-semantics specification (mirrors Coq); §(c) per docs/proof-debt.md.
 axiom read_write_identity (p : Path) (fs : Filesystem) (content : FileContent) :
   readFile p fs = some content →
   writeFile p content fs = fs
 
 /-- chmod to current permissions is identity -/
+-- AXIOM: chmod_identity; POSIX-semantics specification (mirrors Coq); §(c) per docs/proof-debt.md.
 axiom chmod_identity (p : Path) (fs : Filesystem) (meta : FileMetadata) :
   stat p fs = some meta →
   chmod p meta.permissions fs = fs
 
 /-- rename to same path is identity -/
+-- AXIOM: rename_identity; POSIX-semantics specification (mirrors Coq); §(c) per docs/proof-debt.md.
 axiom rename_identity (p : Path) (fs : Filesystem) :
   rename p p fs = fs
 
 /-- rename A to B followed by rename B to A is identity -/
+-- AXIOM: rename_inverse; POSIX-semantics specification (mirrors Coq); §(c) per docs/proof-debt.md.
 axiom rename_inverse (p1 p2 : Path) (fs : Filesystem) :
   p1 ≠ p2 →
   rename p2 p1 (rename p1 p2 fs) = fs
@@ -261,9 +277,11 @@ example (p : Path) :
 /-! ## Snapshot and Restore -/
 
 /-- Snapshot operation -/
+-- AXIOM: snapshot; opaque snapshot primitive; §(c) per docs/proof-debt.md.
 axiom snapshot : Filesystem → Filesystem
 
 /-- Restore from snapshot -/
+-- AXIOM: restore; opaque restore primitive; §(c) per docs/proof-debt.md.
 axiom restore : Filesystem → Filesystem → Filesystem
 
 /-- snapshot followed by restore is identity -/
