From d5c2cf92885e4f12d1bcde9c2bc09af8ddbbdf38 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 27 May 2026 09:29:09 +0100 Subject: [PATCH] =?UTF-8?q?docs+annotate:=20Filesystem=20cluster=20?= =?UTF-8?q?=E2=80=94=2026=20inline=20AXIOM:=20+=208=20=C2=A7(d)=20DEBT=20e?= =?UTF-8?q?ntries=20(Phase=202c)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- docs/proof-debt.md | 110 +++++++++++++++++++++++++- proofs/coq/filesystem/FilesystemCNO.v | 12 +++ proofs/lean4/FilesystemCNO.lean | 18 +++++ 3 files changed, 137 insertions(+), 3 deletions(-) diff --git a/docs/proof-debt.md b/docs/proof-debt.md index 848921c..8cde855 100644 --- 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 index f8d81f8..19e2f8e 100644 --- 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 index ef8d4aa..122c700 100644 --- 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 -/