From 51dee0768145fb3c61e413e4487d673c6aa0891b Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:11:16 +0000 Subject: [PATCH 01/10] fix(lean4): make RmdirPrecondition inhabited; record 2026-11-09 proof ground truth isEmptyDir quantified over ancestors (child.isPrefixOf p) instead of descendants. The parent always exists, so RmdirPrecondition was uninhabited and every Lean theorem assuming it was vacuous, including the composition theorems for any sequence containing mkdir or rmdir. Flip the prefix test to match the Coq and Isabelle models. Add PreconditionWitnesses: one inhabitant per operation precondition plus reversible (.mkdirOp ["a"]) emptyFS, so a future edit that empties a precondition fails the build. Make CI build every Lean library that compiles, by name; a bare `lake build` only built FilesystemModel. Record a re-run of every prover leg against PROOF-POLICY in docs/audits/2026-11-09-proof-ground-truth.adoc, refresh the PROOF-NEEDS reproduction block that the mathesis census reads, and correct the claim that Coq is_empty_dir_dec is an Axiom: it is a Theorem proved with Classical.classic. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDjNR1ZoYKEPxSKE2nq --- .github/workflows/rust-cli.yml | 10 +- CLAUDE.md | 2 +- PROOF-NEEDS.adoc | 59 ++++- .../audits/2026-11-09-proof-ground-truth.adoc | 244 ++++++++++++++++++ proofs/lean4/FilesystemModel.lean | 7 +- proofs/lean4/PreconditionWitnesses.lean | 55 ++++ proofs/lean4/lakefile.lean | 6 +- 7 files changed, 376 insertions(+), 7 deletions(-) create mode 100644 docs/audits/2026-11-09-proof-ground-truth.adoc create mode 100644 proofs/lean4/PreconditionWitnesses.lean diff --git a/.github/workflows/rust-cli.yml b/.github/workflows/rust-cli.yml index 0c9abfaa..b5018e42 100644 --- a/.github/workflows/rust-cli.yml +++ b/.github/workflows/rust-cli.yml @@ -86,7 +86,15 @@ jobs: - name: Build Lean proofs working-directory: proofs/lean4 - run: lake build + # A bare `lake build` builds only the default target (FilesystemModel), + # so the other libraries were never checked here. Build every library + # that compiles on v4.34.1, by name. FileContentOperations, + # RMOOperations, CopyMoveOperations and PermissionOperations do not + # build (see lakefile.lean); they are open work, not silently green. + run: | + lake build FilesystemModel FileOperations FilesystemComposition \ + FilesystemEquivalence SymlinkOperations Extraction \ + CrashConsistency PathTraversal PreconditionWitnesses - name: Check for proof completeness working-directory: proofs/lean4 diff --git a/CLAUDE.md b/CLAUDE.md index 3189566c..1da924e3 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -108,7 +108,7 @@ Grade 2 or Grade 1 obligation. - 21,331 lines of Rust across 32 source files (`find impl/rust-cli/src -name '*.rs' | wc -l`; `wc -l` aggregate, measured 2026-06-01) - ~478 theorem candidates across 6 proof systems + Idris2 ABI layer (per issue #42 deep-audit inventory, 2026-06-01) -- 2 proof holes remaining, **0 real gaps**: 1 justified axiom (Coq `is_empty_dir_dec` — infinite-domain decidability), 1 structural axiom (Agda `funext` — standard in intensional TT). The former real gap (Coq `obliterate_overwrites_all_blocks`) is CLOSED — re-verified 2026-07-16 via `Print Assumptions` (*Closed under the global context*) under Coq 8.18.0 — see `docs/PROOF_HOLES_AUDIT.adoc` +- 2 proof holes remaining, **0 real gaps**: 1 justified classical dependency (Coq `is_empty_dir_dec` — a `Theorem` proved with `Classical.classic` and `ClassicalEpsilon`, not a custom `Axiom`; corrected 2026-11-09), 1 structural axiom (Agda `funext` — standard in intensional TT). The former real gap (Coq `obliterate_overwrites_all_blocks`) is CLOSED — re-verified 2026-07-16 via `Print Assumptions` (*Closed under the global context*) under Coq 8.18.0 — see `docs/PROOF_HOLES_AUDIT.adoc` - Idris2 ABI layer: **0 proof holes** (all closed 2026-07-01, issue #151 root — builds under `--total`), 0 `partial` markers, 2 registered primitive-eq axioms (`axStringEqRefl`, `axBits8EqRefl`; gated by `.github/scripts/check-idris2-believe-me.sh`) - 7 fuzz targets in `impl/rust-cli/fuzz/fuzz_targets/` (parser, arith, job-spec, signal-parse, path-ops, glob-expansion, state-machine) diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index e41ea5c3..9e7e187b 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -12,7 +12,60 @@ cross-system witness matrix) and *docs/PROOF-OPEN-FRONTIER.adoc* (every valuable but unproven theorem, with tractability classification). ____ -=== Reproduction state (2026-11-01) +=== Reproduction state (2026-11-09) + +Every leg was re-run on `main` at `2d798b8`. Full record, with tool versions, +digests and the policy reading: `docs/audits/2026-11-09-proof-ground-truth.adoc`. +Status words are PROOF-POLICY §5; grades are §8. + +[cols="2,2,6",options="header"] +|=== +| Leg | Status | Evidence + +| Agda (theory source) +| `OPEN` under §2.1 +| 9/9 modules check with plain `agda` (2.7.0.1, stdlib 2.2); 9/9 fail under +`--safe --without-K --cubical-compatible` (`funext` postulate). No theory +theorem reaches `PWG-3`; all are `ungraded`. `IsEmptyDir` lacks its emptiness field + +| Lean (recheck leg) +| target-only, `AGDA-PENDING` +| Lean 4.34.1: 8 libraries + `model_oracle` + the new `PreconditionWitnesses` +build; `FileContentOperations`, `RMOOperations`, `CopyMoveOperations`, +`PermissionOperations` do not. `RmdirPrecondition` was uninhabited (ancestor/descendant +prefix reversed in `isEmptyDir`), making every theorem that assumed it vacuous; +fixed 2026-11-09 and guarded by `PreconditionWitnesses` + +| Rocq/Coq (recheck leg) +| target-only, `AGDA-PENDING` +| Coq 8.18.0: 11/11 files build; 133 theorems, 98 closed under the global +context, 35 on standard-library axioms only (funext 30, `classic` 6, +`constructive_indefinite_description` 6). No custom `Axiom` + +| Z3 (§4 exception, unrecorded) +| `ASSUMED` +| Z3 4.8.12: all 5 files axiomatic; `filesystem_operations` is circular, +`symlink_operations` proves nothing + +| Idris2 (engineering/ABI) +| `PROVEN-WITH-AXIOMS` +| Idris2 0.8.0: 5/5 modules under `--total`; 2 registered primitive-eq axioms + +| Isabelle, Mizar +| unchecked +| not run this round (Isabelle server unavailable; Mizar installer not +permitted in the audit session) + +| Rust +| `TESTED`; Creusot/Pearlite and Verus `OPEN` +| `cargo test`: 827 passed, 0 failed, 15 ignored. No Creusot, Pearlite or +Verus contracts exist +|=== + +The toolchains above were installed outside Guix for this audit; each is an +open §6 `deviation`, listed in the audit record. + +=== Reproduction state (2026-11-01, superseded by 2026-11-09) This file records what is *needed*; this block records what has actually been *run*. The full receipt is @@ -68,7 +121,7 @@ Z3) + 1 ABI-stub tier (Idris2) |`+proofs/agda/FilesystemModel.agda:161-162+` |Standard intensional-TT axiom; provable under `+--cubical+` -|Coq |`+Axiom is_empty_dir_dec+` (justified) +|Coq |`+is_empty_dir_dec+` (a `Theorem` proved by `Classical.classic`; corrected 2026-11-09, it is not an `Axiom`) |`+proofs/coq/posix_errors.v+` |Infinite-domain universal quantification |Coq |(closed) `+mkdir_two_dirs_reversible+` @@ -387,7 +440,7 @@ theorem in this repo establishes that bytes are absent from a device. The three Coq admits (#56 / #57 / #58) closed in the 2026-06-02 PM session bring the Coq layer to *zero `+Admitted+` markers* — only the -single justified `+Axiom is_empty_dir_dec+` remains. +single justified classical theorem `+is_empty_dir_dec+` remains (not an `Axiom`; corrected 2026-11-09). `+obliterate_not_injective+` — the formal grounding for the "`mathematically irreversible secure deletion`" marketing claim — is now soundly proven (under the strengthened `+block_overwritten+`-aware diff --git a/docs/audits/2026-11-09-proof-ground-truth.adoc b/docs/audits/2026-11-09-proof-ground-truth.adoc new file mode 100644 index 00000000..ed5bffc0 --- /dev/null +++ b/docs/audits/2026-11-09-proof-ground-truth.adoc @@ -0,0 +1,244 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell += Proof ground truth and PROOF-POLICY conformance, 2026-11-09 +:toc: macro + +This record re-runs every prover leg in `proofs/` on `main` at `2d798b8`. It then +reads the results, and the merged route plan +(`docs/plans/VSH-ROUTE-PLAN-2026-11-04.adoc`), against the estate proof policy +(`hyperpolymath/standards` `3-practice/PROOF-POLICY.adoc`, rulings 2026-10-26, +2026-11-04 and 2026-11-07). Status words are the policy's closed vocabulary +(§5). Grades are Proof Witness Grades (§8) and always carry the `PWG-` prefix. + +toc::[] + +== 1. Summary + +* *One real soundness defect was found and is fixed in this change.* In Lean, + `RmdirPrecondition` was uninhabited: `isEmptyDir` quantified over ancestors + (`child.isPrefixOf p`) instead of descendants, and the parent always exists. + Every Lean theorem with that hypothesis was vacuous. That covers + `rmdir_removes_path`, `rmdir_mkdir_reversible`, `rmdirPreservesEquiv`, and, + through `reversible (.mkdirOp p)`, which needs `RmdirPrecondition` after the + mkdir, every composition theorem on a sequence containing mkdir or rmdir. The + Rocq/Coq and Isabelle definitions have the correct direction. Section 3.1 has + the evidence. +* *No theory theorem in this repository reaches `PWG-3`.* The Agda tree does + not check under the §2.1 invocation (`--safe --without-K + --cubical-compatible`), because of the `funext` postulate. By §8, every theory + theorem here is `ungraded`. The census: 0 of 9 Agda modules check under §2.1, + so 0 theorems are at `PWG-3` or better. +* The existing Lean and Coq proofs are *target-only evidence* under §3, because + no Agda proof is yet `PROVEN`, so the statements cannot be compared. Their + correspondence state is `AGDA-PENDING` (§2.2). +* The Z3 leg is `ASSUMED` at best (§5: a direct SMT run with no certificate), + and two of its five files prove nothing. +* Idris2 (the engineering/ABI leg, §1) builds under `--total`: + `PROVEN-WITH-AXIOMS`, with the 2 registered primitive-equality axioms. +* The Rust suite is green: 827 passed, 0 failed, 15 ignored, across 23 test + binaries. No Creusot, Pearlite or Verus contract exists yet (§1.2), so the Rust + implementation leg is `OPEN`. +* The merged route plan disagrees with the policy in six places (section 5). + Those need owner rulings before the implementation session starts. + +== 2. Toolchains used + +None of these came from the Guix manifest or a container. They were installed +for this audit, so each is a §6 *deviation*. These records cover this audit +session only. CI lanes that install provers outside Guix still need their own +records (section 5, gap G-6). + +[cols="2,2,4,2",options="header"] +|=== +|Leg |Tool and version |Source and digest |State + +|Lean |Lean 4.34.1 (commit `5045d00`) |release archive +`lean.tar.zst`, sha256 `47bf4bbd78f70c2e9670598ab7124d92b6efb7330ff33e5fbb4030f6fd72e4e4` +|`open` +|Rocq/Coq |Coq 8.18.0 |Ubuntu apt package |`open` +|Agda |Agda 2.7.0.1, standard library 2.2 (rev `6cd04e46`) |release +archive `agda.tar.xz`, sha256 +`975b515a14877ab6bce5bfc641e16c4a3ee52ca5d7f846577dee80aa2145db8a`; stdlib from +git |`open` +|Z3 |Z3 4.8.12 |Ubuntu apt package |`open` +|Idris2 |Idris2 0.8.0 |built from source, rev `15a3e4e7` |`open` +|Mizar |— |the archive was downloaded (sha256 +`2ca6aa03a8a19aa1d96e4d80c15e32b59bd789c9aff7b0ca9168834c468e8637`) but the +session's permission policy refused running its installer. *Not run.* |`open` +|Isabelle |— |the distribution server returned HTTP 503. *Not run.* |`open` +|=== + +== 3. Results per leg + +[cols="2,3,3,2",options="header"] +|=== +|Leg |What ran |Result |Status (§5) and correspondence (§2.2) + +|Agda, theory source (§1) |all 9 modules, plain `agda`, and again under +`agda --safe --without-K --cubical-compatible` |plain: 9/9 check. §2.1: 9/9 +fail with `Cannot postulate funext with safe flag` +(`FilesystemModel.agda:178-179`). `IsEmptyDir` has only an `isDir` field: the +emptiness half of the precondition is missing, so the Agda rmdir precondition is +weaker than the Coq and Lean ones |`OPEN` under §2.1. Every theory theorem is +`ungraded` + +|Lean, recheck leg |`lake build` per library, 12 libraries plus +`model_oracle` |8 libraries and the oracle build. `FileContentOperations` +(line 292, application type mismatch), `RMOOperations` (172, simp failed), +`CopyMoveOperations` (19, unknown namespace `Valence.Filesystem`) and +`PermissionOperations` (28, instance synthesis failed) do not build. No `sorry` +and no `axiom`. `RmdirPrecondition` uninhabited (3.1, fixed here) |kernel-checked +where it builds; *target-only*, `AGDA-PENDING` + +|Rocq/Coq, recheck leg |all 11 `_CoqProject` files; `Print Assumptions` on all +133 theorems |all build. 98 are *closed under the global context*. 35 use +standard-library axioms only: `functional_extensionality_dep` (30), +`Classical_Prop.classic` (6), `ClassicalEpsilon.constructive_indefinite_description` +(6). No custom `Axiom`. The 6 classical theorems are `is_empty_dir_dec`, which +is a `Theorem` proved by excluded middle and is not an axiom as `CLAUDE.md` and +`PROOF-NEEDS.adoc` said, and five `safe_rmdir_*` / `safe_mkdir_rmdir_reversible` +lemmas that use it. `rmdir_precondition` is inhabited: a witness on `mkdir ["a"] +empty_fs` is closed under the global context |`PROVEN` / `PROVEN-WITH-AXIOMS` as a +target; *target-only*, `AGDA-PENDING` + +|Z3 / SMT, §4 exception |each of the 5 files, one process each |`filesystem_operations.smt2` +asserts the reversibility "theorem" as an axiom (line 65) and then shows its +negation `unsat`, which is circular. `symlink_operations.smt2` has one `sat` +check and negates no goal. The other three return `unsat` from asserted, +unverified definitional axioms over uninterpreted functions |`ASSUMED` (no +certificate). No §4 exception note exists beside the files + +|Idris2, engineering/ABI (§1) |`idris2 --build valence-shell.ipkg` |5/5 modules +under `--total`. The `believe_me` gate passes: 2 occurrences, 2 registered +axioms (`axStringEqRefl`, `axBits8EqRefl`) |`PROVEN-WITH-AXIOMS` + +|Isabelle |not run (server 503) |— |supplementary evidence only under §3; +unchecked + +|Mizar |not run (permission refused) |— |unchecked; needs a §4 exception +record or archival + +|Rust implementation (§1.2) |`cargo test` in `impl/rust-cli` |827 passed, 0 +failed, 15 ignored, 23 binaries |`TESTED`. Creusot/Pearlite and Verus: no +contracts, `OPEN` +|=== + +=== 3.1 The Lean `RmdirPrecondition` defect + +Before this change: + +[source,lean] +---- +def isEmptyDir (p : Path) (fs : Filesystem) : Prop := + isDirectory p fs ∧ + ∀ child : Path, child.isPrefixOf p → child ≠ p → ¬pathExists child fs +---- + +`parentPath p` is a proper prefix of `p` and, by the `parentWritable` field, it +exists. The following theorem was checked against the unfixed file under Lean +4.34.1 (axioms: `propext`, `Classical.choice`, `Quot.sound`): + +[source,lean] +---- +theorem rmdir_precondition_uninhabited (p : Path) (fs : Filesystem) : + ¬ RmdirPrecondition p fs +---- + +The fix flips the prefix test to `p.isPrefixOf child`. The Coq +(`path_prefix p child`) and Isabelle (`prefix p child`) models already had this +direction. After the fix: + +* All 8 Lean libraries that built before still build, and so does + `model_oracle`. No proof depended on the vacuity. Two of the affected theorems + (`rmdir_removes_path`, `rmdir_mkdir_reversible`) never used the hypothesis; + they were true but could not be applied to any state. +* The uninhabitedness proof no longer typechecks. +* The new library `PreconditionWitnesses` exhibits an inhabitant of every + precondition (mkdir, rmdir, createFile, deleteFile, symlink) and of + `reversible (.mkdirOp ["a"]) emptyFS`. Its axioms are `propext` and + `Quot.sound` at most. A future edit that empties a precondition now fails the + build. + +=== 3.2 Related findings, not fixed here + +* *CI built almost none of the Lean tree.* `rust-cli.yml` ran a bare + `lake build`, which builds only the default target (`FilesystemModel`), and + `lean-verification.yml` builds only `Extraction` and `model_oracle`. This + change makes `rust-cli.yml` build the 8 working libraries plus + `PreconditionWitnesses` by name. +* *The extracted model does not check emptiness.* `Extraction.isEmptyDirBool` + is "simplified: just check if it's a directory", and no theorem links it to + `isEmptyDir`. The Lean oracle that the Rust differential tests drive therefore + allows rmdir of a non-empty directory. This is a spec/executable gap at the + oracle seam. +* *Agda `IsEmptyDir` is a stub* (see the table). Removing `funext` (route plan + P5) should also complete this record. +* *Mizar proofs look unfinished.* For example + `copy_move_operations.miz:200-201` discharges a reversibility equation with + `by A1`, the bare precondition. This cannot be confirmed without running the + checker. + +== 4. Reflection in mathesis + +`hyperpolymath/mathesis` builds its catalogue with `scripts/census/*`, and the +catalogue says it must never be edited by hand. Its census finds this repo's +proof-status file by the pattern `PROOF-STATUS*|PROOF-NEEDS*|proof-debt*`; here +that file is `PROOF-NEEDS.adoc`. The current catalogue row reads `axioms 1, holes +5, status_doc PROOF-NEEDS.adoc`. This change updates `PROOF-NEEDS.adoc` with the +2026-11-09 reproduction block. The row refreshes the next time mathesis reruns +its census. That rerun happens in another repository and is not done by this +change. + +== 5. Route plan against PROOF-POLICY + +The plan merged in #222 predates the 2026-11-07 Rust ruling. In places it also +departs from the 2026-10-26 theory mapping. Each gap below needs an owner ruling +before session 1 runs. + +[cols="1,4,4",options="header"] +|=== +|Gap |Plan says |Policy says + +|G-1 |OD-0/OD-1: Lean is the canonical FinFS spec; Agda is the second witness +|§1/§3: Agda is the source of truth for theory; Rocq and Lean are recheck legs, +Dedukti transport first + +|G-2 |OD-2/P6/P9: Aeneas spike to prove the Rust core refines the Lean spec; +`#print axioms` allow-list includes Aeneas library axioms |§1.2: Rust is +verified with Creusot/Pearlite and Verus by default. §4.1: Aeneas only where +Rust implements an Agda theorem; its Lean backend needs Mathlib (ruled out), so +the Rust-to-model row is `ASSUMED` + +|G-3 |P5 and the session-1 provisioner: Agda 2.6.4.3 with `--no-libraries`; +`--safe --without-K` only |§2.1: `--safe --without-K --cubical-compatible`, with +version and stdlib pinned per commit + +|G-4 |G6: "≥2 independent CI-gated provers plus the oracle", using the #221 +lower-case ledger words |§8: grades derived from receipts; a leg counts only when +kernel-checked *and* `RECONCILED`; §5 upper-case vocabulary + +|G-5 |Isabelle and Mizar "unchecked until archived"; Z3 counted as a prover |§3: +Isabelle is supplementary only. §4: Z3 and Mizar need recorded exception notes, +and SMT without a certificate is `ASSUMED` + +|G-6 |Session-1 provisioner installs from elan, opam, apt and release archives +|§6: Guix manifest or container, otherwise a `deviation` record in the +proof-status file and the installing workflow +|=== + +The plan also writes "Coq" where the estate now writes "Rocq". That is wording +only. + +== 6. What this change does + +* `proofs/lean4/FilesystemModel.lean`: the `isEmptyDir` fix. +* `proofs/lean4/PreconditionWitnesses.lean` (new) and its `lean_lib` entry. +* `.github/workflows/rust-cli.yml`: build the 8 working Lean libraries and the + witnesses by name. +* `PROOF-NEEDS.adoc`: the 2026-11-09 reproduction block; the `is_empty_dir_dec` + row corrected from axiom to classical theorem. +* `CLAUDE.md`: the same correction. +* This record. + +It does not change the route plan. The six gaps in section 5 wait for owner +rulings. diff --git a/proofs/lean4/FilesystemModel.lean b/proofs/lean4/FilesystemModel.lean index 4238aec7..a7701513 100644 --- a/proofs/lean4/FilesystemModel.lean +++ b/proofs/lean4/FilesystemModel.lean @@ -66,9 +66,14 @@ def parentExists (p : Path) (fs : Filesystem) : Prop := def hasWritePermission (p : Path) (fs : Filesystem) : Prop := ∃ node, fs p = some node ∧ node.permissions.writable = true +-- `p` is a directory with no strict descendants: every path that has `p` as a +-- proper prefix is absent. Before 2026-11-09 the prefix test ran the other way +-- (`child.isPrefixOf p`), quantifying over ancestors. The parent always exists, +-- so `RmdirPrecondition` was uninhabited and every theorem assuming it was +-- vacuous. Regression witness: `rmdir_pre_inhabited` in PreconditionWitnesses. def isEmptyDir (p : Path) (fs : Filesystem) : Prop := isDirectory p fs ∧ - ∀ child : Path, child.isPrefixOf p → child ≠ p → ¬pathExists child fs + ∀ child : Path, p.isPrefixOf child → child ≠ p → ¬pathExists child fs -- Basic Lemmas diff --git a/proofs/lean4/PreconditionWitnesses.lean b/proofs/lean4/PreconditionWitnesses.lean new file mode 100644 index 00000000..513e7d7e --- /dev/null +++ b/proofs/lean4/PreconditionWitnesses.lean @@ -0,0 +1,55 @@ +-- SPDX-License-Identifier: MPL-2.0 +/- Valence Shell - precondition non-vacuity witnesses (Lean 4) + + Every reversibility theorem here has the shape `Pre p fs → op⁻¹ (op p fs) = fs`. + If `Pre` is uninhabited the theorem is vacuously true and says nothing. + This module exhibits one concrete state for each operation's precondition, + so a future edit that makes a precondition empty fails the build. + + Added 2026-11-09 after `RmdirPrecondition` was found to be uninhabited + (`isEmptyDir` quantified over ancestors instead of descendants). Audit: + docs/audits/2026-11-09-proof-ground-truth.adoc. +-/ +import FilesystemModel +import FileOperations +import SymlinkOperations +import FilesystemComposition + +namespace PreconditionWitnesses + +theorem mkdir_pre_inhabited : MkdirPrecondition ["a"] emptyFS := + ⟨by simp [pathExists, emptyFS], ⟨_, rfl⟩, ⟨_, rfl⟩, ⟨_, rfl, rfl⟩⟩ + +theorem rmdir_pre_inhabited : RmdirPrecondition ["a"] (mkdir ["a"] emptyFS) := by + refine ⟨⟨defaultPerms, by simp [mkdir, fsUpdate]⟩, + ⟨⟨defaultPerms, by simp [mkdir, fsUpdate]⟩, ?_⟩, + ⟨⟨FSNodeType.directory, defaultPerms⟩, + by simp [mkdir, fsUpdate, parentPath, emptyFS], rfl⟩, + by simp [rootPath]⟩ + intro child hpre hne ⟨node, hn⟩ + match child, hpre, hne, hn with + | [], h, _, _ => simp at h + | [c], h, hne, _ => + simp [List.isPrefixOf] at h; subst h; exact hne rfl + | _ :: _ :: _, _, _, hn => + simp [mkdir, fsUpdate, emptyFS] at hn + +theorem createFile_pre_inhabited : CreateFilePrecondition ["a"] emptyFS := + ⟨by simp [pathExists, emptyFS], ⟨_, rfl⟩, ⟨_, rfl⟩, ⟨_, rfl, rfl⟩⟩ + +theorem deleteFile_pre_inhabited : + DeleteFilePrecondition ["a"] (createFile ["a"] emptyFS) := + ⟨⟨defaultPerms, by simp [createFile, fsUpdate]⟩, + ⟨⟨FSNodeType.directory, defaultPerms⟩, + by simp [createFile, fsUpdate, parentPath, emptyFS], rfl⟩⟩ + +theorem symlink_pre_inhabited : SymlinkPrecondition ["a"] emptyFS := + ⟨by simp [pathExists, emptyFS], ⟨_, rfl⟩, ⟨_, rfl⟩, ⟨_, rfl, rfl⟩⟩ + +-- `reversible (.mkdirOp p)` needs `RmdirPrecondition` after the mkdir, so it was +-- also uninhabited before the fix. This makes the composition theorems for +-- sequences that contain mkdir non-vacuous. +theorem mkdir_reversible_inhabited : reversible (.mkdirOp ["a"]) emptyFS := + ⟨mkdir_pre_inhabited, rmdir_pre_inhabited, trivial⟩ + +end PreconditionWitnesses diff --git a/proofs/lean4/lakefile.lean b/proofs/lean4/lakefile.lean index a6b9b5d7..64e807ad 100644 --- a/proofs/lean4/lakefile.lean +++ b/proofs/lean4/lakefile.lean @@ -4,7 +4,7 @@ -- Last verified working: Lean 4 v4.34.1 (2026-10-02) -- Builds clean: FilesystemModel, FileOperations, FilesystemComposition, -- FilesystemEquivalence, SymlinkOperations, Extraction, CrashConsistency, --- PathTraversal, model_oracle. +-- PathTraversal, PreconditionWitnesses, model_oracle. -- Do NOT build (already broken on v4.12.0, not port regressions): -- FileContentOperations, RMOOperations, CopyMoveOperations, -- PermissionOperations. @@ -58,6 +58,10 @@ lean_lib CrashConsistency where lean_lib PathTraversal where srcDir := "." +-- Non-vacuity witnesses: one inhabitant per operation precondition. +lean_lib PreconditionWitnesses where + srcDir := "." + -- Executable model oracle: drives the proven model for differential testing -- against the Rust implementation. Build: `lake build model_oracle`. lean_exe model_oracle where From 5bd68d1e3900d7f69fe571a6417fcf7e8018d528 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:20:23 +0000 Subject: [PATCH 02/10] docs(audit): record Idris2 holes outside the ledger and the census believe_me classification Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDjNR1ZoYKEPxSKE2nq --- docs/audits/2026-11-09-proof-ground-truth.adoc | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/docs/audits/2026-11-09-proof-ground-truth.adoc b/docs/audits/2026-11-09-proof-ground-truth.adoc index ed5bffc0..e76a2b48 100644 --- a/docs/audits/2026-11-09-proof-ground-truth.adoc +++ b/docs/audits/2026-11-09-proof-ground-truth.adoc @@ -173,6 +173,18 @@ direction. After the fix: oracle seam. * *Agda `IsEmptyDir` is a stub* (see the table). Removing `funext` (route plan P5) should also complete this record. +* *Three Idris2 holes sit outside the proof ledger.* The mathesis hole scanner + (`scripts/census/proof-holes.sh`) finds `?fieldsAlignedProof`, + `?exampleFieldsAligned` and `?offsetInBoundsProof` in + `alkahest-shell-transmuter/src/abi/Layout.idr` (lines 140, 161, 178). + `PROOF-NEEDS.adoc` and `CLAUDE.md` count only `proofs/idris2/`, so they report + zero Idris2 holes. `offsetInBounds` is also unprovable as stated: it quantifies + over every `Field`, not only the fields of the layout. +* *The census and the ledger classify `believe_me` differently.* mathesis counts + the 2 registered primitive-equality axioms as `hole`; this repo registers them + as axioms. Its row today reads axioms 1 (Agda `funext`), holes 5 (those 3 plus + the 2 `believe_me`), policy 9 (Agda files without `--safe`). A local scan of this + branch gives the same counts, so this change leaves the row as it is. * *Mizar proofs look unfinished.* For example `copy_move_operations.miz:200-201` discharges a reversibility equation with `by A1`, the bare precondition. This cannot be confirmed without running the From b8e4c7f7b16890141c5a3a66c114c12c5b532dd2 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:40:06 +0000 Subject: [PATCH 03/10] feat(agda): check the Agda tree under --safe --without-K --cubical-compatible MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Owner ruling 2026-11-09: Agda is the theory source of truth here, per standards PROOF-POLICY §1. Make the tree meet the canonical invocation. - Remove the funext postulate. Whole-filesystem equalities are now pointwise (_≗_); every former `funext helper` proof was already pointwise inside, so no theorem loses content. Composition gets fsUpdate-cong, applyOp-cong and applySequence-cong. - Remove K: clauses that matched refl on `p ≡ p` now use fsUpdate-at. - Complete IsEmptyDir with noChildren (no strict descendant exists), using a prefix relation in the descendant direction, as in Coq and the fixed Lean model. - Add PreconditionWitnesses (one inhabitant per precondition) and All.agda (the import cone CI checks). - Add .github/workflows/agda.yml: Agda 2.7.0.1 release archive, digest-checked, and agda-stdlib v2.2 at a pinned commit (a recorded §6 deviation), a no-postulate/no-pragma guard, an All.agda coverage guard, then the canonical check. All 10 modules check (exit 0). The 190 warnings are all UnsupportedIndexedMatch from matching stdlib Dec, which only matters under Cubical Agda; recorded in VERIFICATION.adoc. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDjNR1ZoYKEPxSKE2nq --- .github/workflows/agda.yml | 100 ++++++++++++++++++++++ CLAUDE.md | 19 +++-- EXPLAINME.adoc | 10 +-- PROOF-NEEDS.adoc | 20 +++-- docs/PROOF_HOLES_AUDIT.adoc | 5 ++ proofs/agda/All.agda | 16 ++++ proofs/agda/CopyMoveOperations.agda | 31 +++---- proofs/agda/FileContentOperations.agda | 25 +++--- proofs/agda/FileOperations.agda | 26 ++---- proofs/agda/FilesystemComposition.agda | 40 ++++++--- proofs/agda/FilesystemEquivalence.agda | 9 +- proofs/agda/FilesystemModel.agda | 57 ++++++------- proofs/agda/PermissionOperations.agda | 19 +++-- proofs/agda/PreconditionWitnesses.agda | 66 +++++++++++++++ proofs/agda/README.adoc | 32 +++---- proofs/agda/RMOOperations.agda | 3 +- proofs/agda/SymlinkOperations.agda | 20 ++--- proofs/agda/VERIFICATION.adoc | 113 ++++++++++++------------- 18 files changed, 395 insertions(+), 216 deletions(-) create mode 100644 .github/workflows/agda.yml create mode 100644 proofs/agda/All.agda create mode 100644 proofs/agda/PreconditionWitnesses.agda diff --git a/.github/workflows/agda.yml b/.github/workflows/agda.yml new file mode 100644 index 00000000..6a7e9198 --- /dev/null +++ b/.github/workflows/agda.yml @@ -0,0 +1,100 @@ +# SPDX-License-Identifier: MPL-2.0 +# Agda is the theory source of truth (standards PROOF-POLICY §1). This lane +# checks every module through proofs/agda/All.agda under the canonical +# invocation (§2.1): --safe --without-K --cubical-compatible. +# +# PROOF-POLICY §6 deviation (state: open). The toolchain is not installed from +# the Guix manifest or a container, because this repository has neither for +# Agda yet. Leg: Agda theory source. Tool: Agda 2.7.0.1 upstream release +# archive, sha256 975b515a14877ab6bce5bfc641e16c4a3ee52ca5d7f846577dee80aa2145db8a; +# agda-stdlib tag v2.2 at commit 6cd04e46e5f8c740a5ec584a108bbb3380fa92d7. +# The run asserts both and fails on a mismatch. Also recorded in PROOF-NEEDS.adoc. +name: Agda proofs + +on: + push: + branches: [main] + paths: + - 'proofs/agda/**' + - '.github/workflows/agda.yml' + pull_request: + paths: + - 'proofs/agda/**' + - '.github/workflows/agda.yml' + +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +permissions: + contents: read + +jobs: + check: + name: Agda (--safe --without-K --cubical-compatible) + runs-on: ubuntu-latest + timeout-minutes: 30 + env: + AGDA_VERSION: 2.7.0.1 + AGDA_SHA256: 975b515a14877ab6bce5bfc641e16c4a3ee52ca5d7f846577dee80aa2145db8a + STDLIB_TAG: v2.2 + STDLIB_COMMIT: 6cd04e46e5f8c740a5ec584a108bbb3380fa92d7 + steps: + - name: Checkout code + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v4 + + - name: Install Agda (pinned release, digest-checked) + run: | + set -euo pipefail + curl -sSfL -o agda.tar.xz \ + "https://github.com/agda/agda/releases/download/v${AGDA_VERSION}/Agda-v${AGDA_VERSION}-linux.tar.xz" + echo "${AGDA_SHA256} agda.tar.xz" | sha256sum -c - + mkdir -p "$HOME/agda" + tar -xJf agda.tar.xz -C "$HOME/agda" + echo "$HOME/agda/Agda-v${AGDA_VERSION}/bin" >> "$GITHUB_PATH" + echo "Agda_datadir=$HOME/agda/Agda-v${AGDA_VERSION}/data" >> "$GITHUB_ENV" + + - name: Install agda-stdlib (pinned commit) + run: | + set -euo pipefail + git clone --depth 1 --branch "${STDLIB_TAG}" https://github.com/agda/agda-stdlib.git "$HOME/agda-stdlib" + got="$(git -C "$HOME/agda-stdlib" rev-parse HEAD)" + if [ "$got" != "${STDLIB_COMMIT}" ]; then + echo "::error::agda-stdlib ${STDLIB_TAG} is ${got}, expected ${STDLIB_COMMIT}"; exit 1 + fi + mkdir -p "$HOME/.agda" + echo "$HOME/agda-stdlib/standard-library.agda-lib" > "$HOME/.agda/libraries" + + - name: Assert Agda version + run: | + set -euo pipefail + ver="$(agda --version | head -n1)" + echo "$ver" + case "$ver" in + *"version ${AGDA_VERSION}"*) : ;; + *) echo "::error::expected Agda ${AGDA_VERSION}, got: $ver"; exit 1 ;; + esac + + - name: No postulates or escape pragmas + working-directory: proofs/agda + run: | + set -euo pipefail + if grep -nE '^[[:space:]]*postulate|TERMINATING|NON_TERMINATING|NO_POSITIVITY_CHECK|NO_UNIVERSE_CHECK' *.agda; then + echo "::error::postulate or escape pragma found"; exit 1 + fi + + - name: Every module is imported by All.agda + working-directory: proofs/agda + run: | + set -euo pipefail + missing=0 + for f in *.agda; do + m="${f%.agda}" + [ "$m" = "All" ] && continue + grep -qx "import ${m}" All.agda || { echo "::error::${m} is not imported by All.agda"; missing=1; } + done + exit "$missing" + + - name: Check All.agda under the estate invocation + working-directory: proofs/agda + run: agda --safe --without-K --cubical-compatible All.agda diff --git a/CLAUDE.md b/CLAUDE.md index 1da924e3..5080d6da 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -59,9 +59,10 @@ the same change as that file. Which verifier carries which obligation: only where Rust implements a theorem proved in Agda. * *Ada code* → SPARK (none in this repo). * *APIs, ABIs, wire formats, engineering properties* → Idris2 (`proofs/idris2/`). -* *Theory* → Agda as the source of truth, rechecked in Rocq and Lean. This repo's - theory rows are currently Coq/Lean-sourced, which is the reverse of that order; see - `docs/audits/2026-11-01-assurance-boundary-audit.adoc` AP-3. +* *Theory* → Agda as the source of truth, rechecked in Rocq and Lean. Owner + ruling 2026-11-09 adopts this order here: the Agda tree is the source and checks + under the canonical invocation; the existing Lean and Rocq proofs are target-only + evidence until compared (`docs/audits/2026-11-09-proof-ground-truth.adoc`). * Isabelle/Mizar/Z3 are §4 exceptions and need a recorded exception note. Status vocabulary is closed (`PROOF-POLICY` §5): `proven`, @@ -108,7 +109,7 @@ Grade 2 or Grade 1 obligation. - 21,331 lines of Rust across 32 source files (`find impl/rust-cli/src -name '*.rs' | wc -l`; `wc -l` aggregate, measured 2026-06-01) - ~478 theorem candidates across 6 proof systems + Idris2 ABI layer (per issue #42 deep-audit inventory, 2026-06-01) -- 2 proof holes remaining, **0 real gaps**: 1 justified classical dependency (Coq `is_empty_dir_dec` — a `Theorem` proved with `Classical.classic` and `ClassicalEpsilon`, not a custom `Axiom`; corrected 2026-11-09), 1 structural axiom (Agda `funext` — standard in intensional TT). The former real gap (Coq `obliterate_overwrites_all_blocks`) is CLOSED — re-verified 2026-07-16 via `Print Assumptions` (*Closed under the global context*) under Coq 8.18.0 — see `docs/PROOF_HOLES_AUDIT.adoc` +- 2 proof holes remaining, **0 real gaps**: 1 justified classical dependency (Coq `is_empty_dir_dec` — a `Theorem` proved with `Classical.classic` and `ClassicalEpsilon`, not a custom `Axiom`; corrected 2026-11-09), 0 Agda postulates (the structural `funext` was removed 2026-11-09: filesystem equality is now pointwise and the tree checks under `--safe --without-K --cubical-compatible`). The former real gap (Coq `obliterate_overwrites_all_blocks`) is CLOSED — re-verified 2026-07-16 via `Print Assumptions` (*Closed under the global context*) under Coq 8.18.0 — see `docs/PROOF_HOLES_AUDIT.adoc` - Idris2 ABI layer: **0 proof holes** (all closed 2026-07-01, issue #151 root — builds under `--total`), 0 `partial` markers, 2 registered primitive-eq axioms (`axStringEqRefl`, `axBits8EqRefl`; gated by `.github/scripts/check-idris2-believe-me.sh`) - 7 fuzz targets in `impl/rust-cli/fuzz/fuzz_targets/` (parser, arith, job-spec, signal-parse, path-ops, glob-expansion, state-machine) @@ -117,7 +118,7 @@ Grade 2 or Grade 1 obligation. ### Critical Priority 1. **No mechanized Lean -> Rust correspondence** — `argued` + `tested-only`, never `proven`; the v1.0 blocker -2. **0 real proof gaps** — the former Coq `obliterate_overwrites_all_blocks` gap is CLOSED (re-verified 2026-07-16, *Closed under the global context*); 2 documented axioms remain (1 justified decidability + 1 structural funext) — see `docs/PROOF_HOLES_AUDIT.adoc` +2. **0 real proof gaps** — the former Coq `obliterate_overwrites_all_blocks` gap is CLOSED (re-verified 2026-07-16, *Closed under the global context*); 1 documented classical dependency remains (Coq `is_empty_dir_dec`; the Agda `funext` postulate was removed 2026-11-09) — see `docs/PROOF_HOLES_AUDIT.adoc` 3. **NOT production-ready** — research prototype only ### High Priority @@ -184,10 +185,10 @@ deep-audit session). The corresponding Phase 4C design docs under ### Technology Stack **Formal Verification (6 systems)**: -- Lean 4 — primary source of truth +- Agda — theory source of truth (owner ruling 2026-11-09) +- Lean 4 — recheck leg; also the executable model oracle - Coq — CIC foundation, extraction to OCaml - Isabelle/HOL — cross-validation -- Agda — intensional type theory - Mizar — set theory foundation - Z3 SMT — automated verification @@ -212,9 +213,9 @@ valence-shell/ zig/ # Zig FFI scaffolding mcp/ # MCP server bindings proofs/ - lean4/ # Primary proof source (101 theorems) + lean4/ # Lean recheck leg + executable model oracle (101 theorems) coq/ # CIC proofs + extraction (131 theorems, 0 admits — re-verified 2026-07-16, Coq 8.18.0) - agda/ # Type theory proofs (85 theorems, 3 postulates including funext) + agda/ # Theory source of truth (owner ruling 2026-11-09); 10 modules, 0 postulates, --safe --without-K --cubical-compatible isabelle/ # HOL proofs (76 theorems) mizar/ # Set theory proofs (63 theorems) z3/ # SMT proofs (125 asserts) diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index c176f0a5..c693135d 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -111,11 +111,11 @@ reproduce. Absence of a tool is an open obligation, not a passing leg | `proofs/lean4/FilesystemModel.lean`, `FileOperations.lean`, `FilesystemComposition.lean` | Independent restatement, *not* a translation of the Coq term, so it is not mathesis grade 2; the Lean model is also separately typed -| Same theorems restated in Agda -| proven-with-postulates (reproduced 2026-11-01) -| `agda --library-file= .agda`, Agda 2.6.4.3 + stdlib 2.1.1 *and* 2.7.0.1 + stdlib 2.2: 9/9 modules type-check -| `proofs/agda/` (all nine modules; `postulate funext` at `FilesystemModel.agda:179`) -| One postulate (`funext`), no holes -- but *not* the estate invocation. `--safe` reports `Cannot postulate funext with safe flag`; `--without-K` reports `Cannot eliminate reflexive equation p = p ... K has been disabled`. So this row is reproduced under a waiver, is not mathesis grade 3, and the waiver must be recorded beside the artefact per PROOF-POLICY §4. See the audit's AP-6 and its verification round +| Same theorems in Agda (the theory source since the 2026-11-09 owner ruling) +| proven (2026-11-09) +| `agda --safe --without-K --cubical-compatible All.agda`, Agda 2.7.0.1 + stdlib v2.2: 10/10 modules; CI `.github/workflows/agda.yml` +| `proofs/agda/` (ten modules via `All.agda`) +| No postulates, no holes, the estate invocation. Filesystem equality is pointwise (`_≗_`). Grade `PWG-3` is derived from the CI receipt on the merge head, not asserted here. See `docs/audits/2026-11-09-proof-ground-truth.adoc` | Same theorems restated in Isabelle / Mizar / Z3 | proven-with-postulates (Isabelle) / open (Mizar) / Z3: reproduced for 4 of 5 files, `open` for `symlink_operations.smt2` diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index 9e7e187b..9a4b0e03 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -22,11 +22,15 @@ Status words are PROOF-POLICY §5; grades are §8. |=== | Leg | Status | Evidence -| Agda (theory source) -| `OPEN` under §2.1 -| 9/9 modules check with plain `agda` (2.7.0.1, stdlib 2.2); 9/9 fail under -`--safe --without-K --cubical-compatible` (`funext` postulate). No theory -theorem reaches `PWG-3`; all are `ungraded`. `IsEmptyDir` lacks its emptiness field +| Agda (theory source, owner ruling 2026-11-09) +| `PROVEN`; `PWG-3` once CI is green on the merge head +| On `main` (2d798b8): 9/9 failed `--safe --without-K --cubical-compatible` +(`funext` postulate, K-dependent clauses), and `IsEmptyDir` lacked its +emptiness field. Fixed in PR #223: equalities are pointwise (`_≗_`), no +postulates, `IsEmptyDir` complete, non-vacuity witnesses added; 10/10 +modules check through `All.agda` under that invocation (Agda 2.7.0.1, stdlib +v2.2) and CI checks it (`.github/workflows/agda.yml`). §6 `deviation` +(open): Agda comes from the upstream release archive, digest-checked, not Guix | Lean (recheck leg) | target-only, `AGDA-PENDING` @@ -117,9 +121,9 @@ Z3) + 1 ABI-stub tier (Idris2) [width="100%",cols="25%,25%,25%,25%",options="header",] |=== |Layer |Item |Location |Nature -|Agda |`+postulate funext+` -|`+proofs/agda/FilesystemModel.agda:161-162+` |Standard intensional-TT -axiom; provable under `+--cubical+` +|Agda |(closed 2026-11-09) `+postulate funext+` +|`+proofs/agda/FilesystemModel.agda+` |Removed: filesystem equality is +now pointwise, so no extensionality is needed |Coq |`+is_empty_dir_dec+` (a `Theorem` proved by `Classical.classic`; corrected 2026-11-09, it is not an `Axiom`) |`+proofs/coq/posix_errors.v+` |Infinite-domain universal quantification diff --git a/docs/PROOF_HOLES_AUDIT.adoc b/docs/PROOF_HOLES_AUDIT.adoc index 764a547d..e896e5f0 100644 --- a/docs/PROOF_HOLES_AUDIT.adoc +++ b/docs/PROOF_HOLES_AUDIT.adoc @@ -1,6 +1,11 @@ == Proof Holes Audit - Valence Shell ____ +*SUPERSEDED IN PART 2026-11-09.* The Agda `funext` postulate is gone and the +Agda tree now checks under `--safe --without-K --cubical-compatible`; the Lean +`RmdirPrecondition` was found uninhabited and fixed. Current state: +`docs/audits/2026-11-09-proof-ground-truth.adoc`. + *CORRECTED 2026-11-01.* This file records the state as believed on 2026-07-16. It has since been measured and parts of it were wrong. When the Agda tree was first actually compiled (Agda 2.7.0.1 + stdlib 2.2, then 2.6.4.3 + stdlib 2.1.1), diff --git a/proofs/agda/All.agda b/proofs/agda/All.agda new file mode 100644 index 00000000..f521f376 --- /dev/null +++ b/proofs/agda/All.agda @@ -0,0 +1,16 @@ +{-# OPTIONS --safe --without-K --cubical-compatible #-} +-- SPDX-License-Identifier: MPL-2.0 +-- Every Agda module in this tree. CI checks this file under the estate +-- invocation (PROOF-POLICY §2.1); a module not imported here is not checked. +module All where + +import FilesystemModel +import FileOperations +import SymlinkOperations +import PermissionOperations +import FilesystemComposition +import FilesystemEquivalence +import CopyMoveOperations +import FileContentOperations +import RMOOperations +import PreconditionWitnesses diff --git a/proofs/agda/CopyMoveOperations.agda b/proofs/agda/CopyMoveOperations.agda index 47c1200d..32a85193 100644 --- a/proofs/agda/CopyMoveOperations.agda +++ b/proofs/agda/CopyMoveOperations.agda @@ -1,3 +1,4 @@ +{-# OPTIONS --safe --without-K --cubical-compatible #-} -- SPDX-License-Identifier: MPL-2.0 {- Valence Shell - Copy and Move Operations in Agda @@ -22,7 +23,7 @@ open import Data.Bool using (Bool; true; false; if_then_else_) open import Data.Product using (_×_; _,_; proj₁; proj₂; ∃; ∃-syntax) open import Data.Maybe using (Maybe; just; nothing) open import Data.String using (String) -open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym; trans; subst) +open import Relation.Binary.PropositionalEquality using (_≡_; _≗_; refl; cong; sym; trans; subst) open import Relation.Nullary using (¬_; Dec; yes; no) open import Data.Empty using (⊥; ⊥-elim) open import Data.Unit using (⊤; tt) @@ -100,11 +101,11 @@ moveFile-nothing-eq src dst fs h with fs src -- moveFile is reversible: moving back restores the original filesystem moveFile-reversible : ∀ src dst fs → movePrecondition src dst fs → - moveFile dst src (moveFile src dst fs) ≡ fs -moveFile-reversible src dst fs ((node , hsrc) , not-dst , parent-ex , notEq , rest) = - trans (cong (λ t → moveFile dst src t) (moveFile-just-eq src dst fs node hsrc)) - (trans (moveFile-just-eq dst src fs1 node fs1-dst) - (funext fs2-is-fs)) + moveFile dst src (moveFile src dst fs) ≗ fs +moveFile-reversible src dst fs ((node , hsrc) , not-dst , parent-ex , notEq , rest) p' = + trans (cong (λ t → moveFile dst src t p') (moveFile-just-eq src dst fs node hsrc)) + (trans (cong (λ g → g p') (moveFile-just-eq dst src fs1 node fs1-dst)) + (fs2-is-fs p')) where fs1 : Filesystem fs1 = fsUpdate src nothing (fsUpdate dst (just node) fs) @@ -150,8 +151,8 @@ pathExists-not-nothing p fs (node , eq) = node , eq -- Double fsUpdate at same path: second write wins fsUpdate-overwrite : ∀ p v1 v2 fs → - fsUpdate p v2 (fsUpdate p v1 fs) ≡ fsUpdate p v2 fs -fsUpdate-overwrite p v1 v2 fs = funext helper + fsUpdate p v2 (fsUpdate p v1 fs) ≗ fsUpdate p v2 fs +fsUpdate-overwrite p v1 v2 fs = helper where helper : ∀ p' → fsUpdate p v2 (fsUpdate p v1 fs) p' ≡ fsUpdate p v2 fs p' helper p' = case-split (p path-≟ p') @@ -167,8 +168,8 @@ fsUpdate-overwrite p v1 v2 fs = funext helper -- fsUpdate p nothing fs ≡ fs when fs p ≡ nothing (path didn't exist) fsUpdate-nothing-noop : ∀ p fs → ¬ pathExists p fs → - fsUpdate p nothing fs ≡ fs -fsUpdate-nothing-noop p fs notExists = funext helper + fsUpdate p nothing fs ≗ fs +fsUpdate-nothing-noop p fs notExists = helper where helper : ∀ p' → fsUpdate p nothing fs p' ≡ fs p' helper p' with p path-≟ p' @@ -230,11 +231,11 @@ copyFile-same-content src dst fs ((perms , hsrc) , _) = -- Theorem: copy is reversible by deleting destination copyFile-reversible : ∀ src dst fs → copyFilePrecondition src dst fs → - deleteFile dst (copyFile src dst fs) ≡ fs -copyFile-reversible src dst fs ((perms , hsrc) , not-dst , _) = - trans (cong (λ t → deleteFile dst t) (copyFile-just src dst fs (mkFSNode File perms) hsrc)) - (trans (fsUpdate-overwrite dst (just (mkFSNode File perms)) nothing fs) - (fsUpdate-nothing-noop dst fs not-dst)) + deleteFile dst (copyFile src dst fs) ≗ fs +copyFile-reversible src dst fs ((perms , hsrc) , not-dst , _) p' = + trans (cong (λ t → deleteFile dst t p') (copyFile-just src dst fs (mkFSNode File perms) hsrc)) + (trans (fsUpdate-overwrite dst (just (mkFSNode File perms)) nothing fs p') + (fsUpdate-nothing-noop dst fs not-dst p')) -- ============================================================================ -- Move Operation Theorems diff --git a/proofs/agda/FileContentOperations.agda b/proofs/agda/FileContentOperations.agda index aca4840b..9011f2ce 100644 --- a/proofs/agda/FileContentOperations.agda +++ b/proofs/agda/FileContentOperations.agda @@ -1,3 +1,4 @@ +{-# OPTIONS --safe --without-K --cubical-compatible #-} {- SPDX-License-Identifier: MPL-2.0 -} {- Valence Shell - File Content Operations (Agda) @@ -25,7 +26,7 @@ open import Data.Bool using (Bool; true; false; if_then_else_) open import Data.Nat using (ℕ) open import Data.Product using (_×_; _,_; ∃; ∃-syntax) open import Relation.Binary.PropositionalEquality - using (_≡_; refl; sym; trans; cong; inspect; [_]) + using (_≡_; _≗_; refl; sym; trans; cong; inspect; [_]) open import Relation.Nullary using (¬_; Dec; yes; no) open import Data.Empty using (⊥-elim) @@ -172,8 +173,8 @@ writeFileReversible : ∀ (p : Path) (fs : FilesystemWithContent) (oldContent newContent : FileContent) → WriteFilePrecondition p fs → readFile p fs ≡ just oldContent → - writeFile p oldContent (writeFile p newContent fs) ≡ fs -writeFileReversible p fs oldContent newContent pre hold = funext helper + writeFile p oldContent (writeFile p newContent fs) ≗ fs +writeFileReversible p fs oldContent newContent pre hold = helper where helper : ∀ p' → writeFile p oldContent (writeFile p newContent fs) p' ≡ fs p' helper p' = case-split (p path-≟ p') @@ -204,8 +205,8 @@ writeFileIndependence p1 p2 content fs p1≢p2 = -- Last write wins: writing c2 after c1 at the same path = writing c2 directly writeFileLastWriteWins : ∀ (p : Path) (fs : FilesystemWithContent) (c1 c2 : FileContent) → - writeFile p c2 (writeFile p c1 fs) ≡ writeFile p c2 fs -writeFileLastWriteWins p fs c1 c2 = funext helper + writeFile p c2 (writeFile p c1 fs) ≗ writeFile p c2 fs +writeFileLastWriteWins p fs c1 c2 = helper where helper : ∀ p' → writeFile p c2 (writeFile p c1 fs) p' ≡ writeFile p c2 fs p' helper p' = case-split (p path-≟ p') @@ -226,9 +227,9 @@ writeFileLastWriteWins p fs c1 c2 = funext helper writeFileCommute : ∀ (p1 p2 : Path) (fs : FilesystemWithContent) (c1 c2 : FileContent) → ¬ (p1 ≡ p2) → - writeFile p1 c1 (writeFile p2 c2 fs) ≡ + writeFile p1 c1 (writeFile p2 c2 fs) ≗ writeFile p2 c2 (writeFile p1 c1 fs) -writeFileCommute p1 p2 fs c1 c2 p1≢p2 = funext helper +writeFileCommute p1 p2 fs c1 c2 p1≢p2 = helper where p2≢p1 : ¬ (p2 ≡ p1) p2≢p1 = λ e → p1≢p2 (sym e) @@ -263,8 +264,8 @@ writeFileCommute p1 p2 fs c1 c2 p1≢p2 = funext helper writeFileSameContent : ∀ (p : Path) (content : FileContent) (fs : FilesystemWithContent) → WriteFilePrecondition p fs → readFile p fs ≡ just content → - writeFile p content fs ≡ fs -writeFileSameContent p content fs pre hold = funext helper + writeFile p content fs ≗ fs +writeFileSameContent p content fs pre hold = helper where helper : ∀ p' → writeFile p content fs p' ≡ fs p' helper p' = case-split (p path-≟ p') @@ -299,10 +300,10 @@ restoreFileState state fs = -- Capturing then restoring is identity for writable files captureRestoreIdentity : ∀ (p : Path) (fs : FilesystemWithContent) → WriteFilePrecondition p fs → - restoreFileState (captureFileState p fs) fs ≡ fs + restoreFileState (captureFileState p fs) fs ≗ fs captureRestoreIdentity p fs hpre with readFile p fs | inspect (readFile p) fs ... | just content | [ eq ] = writeFileSameContent p content fs hpre eq -... | nothing | _ = refl +... | nothing | _ = λ _ → refl -- ============================================================================ -- Integration with MAA Framework @@ -337,7 +338,7 @@ modificationReversible : ∀ (mrec : FileModificationRecord) (fs : FilesystemWit WriteFilePrecondition (FileModificationRecord.modPath mrec) fs → readFile (FileModificationRecord.modPath mrec) fs ≡ just (FileModificationRecord.modOldContent mrec) → - reverseModification mrec (applyModification mrec fs) ≡ fs + reverseModification mrec (applyModification mrec fs) ≗ fs modificationReversible mrec fs hpre hold = writeFileReversible (FileModificationRecord.modPath mrec) diff --git a/proofs/agda/FileOperations.agda b/proofs/agda/FileOperations.agda index b7d64f2a..ae4162c7 100644 --- a/proofs/agda/FileOperations.agda +++ b/proofs/agda/FileOperations.agda @@ -1,3 +1,4 @@ +{-# OPTIONS --safe --without-K --cubical-compatible #-} {- Valence Shell - File Operations (Agda) Extension of filesystem model to include file operations. @@ -10,7 +11,7 @@ open import FilesystemModel open import Data.Maybe using (just; nothing) open import Data.Product using (_×_; _,_) open import Relation.Nullary using (¬_; Dec; yes; no) -open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans) +open import Relation.Binary.PropositionalEquality using (_≡_; _≗_; refl; sym; trans) -- File Operations @@ -33,32 +34,21 @@ deleteFile p fs = fsUpdate p nothing fs -- Postcondition Theorems createFile-creates-file : ∀ p fs → CreateFilePrecondition p fs → isFile p (createFile p fs) -createFile-creates-file p fs pre with p path-≟ p -... | yes refl = defaultPerms , refl -... | no p≢p = ⊥-elim (p≢p refl) - where - open import Data.Empty using (⊥-elim) +createFile-creates-file p fs pre = defaultPerms , fsUpdate-at p _ _ createFile-path-exists : ∀ p fs → CreateFilePrecondition p fs → pathExists p (createFile p fs) -createFile-path-exists p fs pre with p path-≟ p -... | yes refl = mkFSNode File defaultPerms , refl -... | no p≢p = ⊥-elim (p≢p refl) - where - open import Data.Empty using (⊥-elim) +createFile-path-exists p fs pre = mkFSNode File defaultPerms , fsUpdate-at p _ _ deleteFile-removes-path : ∀ p fs → DeleteFilePrecondition p fs → ¬ pathExists p (deleteFile p fs) -deleteFile-removes-path p fs pre (node , eq) with p path-≟ p -... | yes refl = nothing≢just eq -... | no p≢p = ⊥-elim (p≢p refl) - where - open import Data.Empty using (⊥-elim) +deleteFile-removes-path p fs pre (node , eq) = + nothing≢just (trans (sym (fsUpdate-at p nothing _)) eq) -- File Reversibility Theorem createFile-deleteFile-reversible : ∀ p fs → CreateFilePrecondition p fs → - deleteFile p (createFile p fs) ≡ fs -createFile-deleteFile-reversible p fs pre = funext helper + deleteFile p (createFile p fs) ≗ fs +createFile-deleteFile-reversible p fs pre = helper where open import Data.Empty using (⊥-elim) diff --git a/proofs/agda/FilesystemComposition.agda b/proofs/agda/FilesystemComposition.agda index c5b7309e..c50ea983 100644 --- a/proofs/agda/FilesystemComposition.agda +++ b/proofs/agda/FilesystemComposition.agda @@ -1,3 +1,4 @@ +{-# OPTIONS --safe --without-K --cubical-compatible #-} {- Valence Shell - Filesystem Composition (Agda) Composition theorems for filesystem operations @@ -11,7 +12,7 @@ open import Data.List using (List; []; _∷_; reverse; map; _++_) open import Data.Maybe using (just; nothing) open import Data.Product using (_×_; _,_) open import Relation.Nullary using (Dec; yes; no) -open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong) +open import Relation.Binary.PropositionalEquality using (_≡_; _≗_; refl; sym; trans; cong) open import Data.Empty using (⊥-elim) -- Operation type @@ -56,6 +57,17 @@ applySequence-append : ∀ xs ys fs → applySequence-append [] ys fs = refl applySequence-append (x ∷ xs) ys fs = applySequence-append xs ys (applyOp x fs) +-- Operations and sequences respect pointwise equality +applyOp-cong : ∀ op {fs₁ fs₂} → fs₁ ≗ fs₂ → applyOp op fs₁ ≗ applyOp op fs₂ +applyOp-cong (mkdirOp p) h = fsUpdate-cong p _ h +applyOp-cong (rmdirOp p) h = fsUpdate-cong p _ h +applyOp-cong (createFileOp p) h = fsUpdate-cong p _ h +applyOp-cong (deleteFileOp p) h = fsUpdate-cong p _ h + +applySequence-cong : ∀ ops {fs₁ fs₂} → fs₁ ≗ fs₂ → applySequence ops fs₁ ≗ applySequence ops fs₂ +applySequence-cong [] h = h +applySequence-cong (op ∷ ops) h = applySequence-cong ops (applyOp-cong op h) + -- Precondition opPrecondition : Operation → Filesystem → Set opPrecondition (mkdirOp p) fs = MkdirPrecondition p fs @@ -95,8 +107,8 @@ HasDefaultFilePerms p fs = fs p ≡ just (mkFSNode File defaultPerms) rmdir-mkdir-reversible : ∀ (p : Path) (fs : Filesystem) → RmdirPrecondition p fs → HasDefaultDirPerms p fs → - applyOp (mkdirOp p) (applyOp (rmdirOp p) fs) ≡ fs -rmdir-mkdir-reversible p fs pre hperms = funext helper + applyOp (mkdirOp p) (applyOp (rmdirOp p) fs) ≗ fs +rmdir-mkdir-reversible p fs pre hperms = helper where helper : ∀ p' → mkdir p (rmdir p fs) p' ≡ fs p' helper p' = case-split (p path-≟ p') @@ -112,8 +124,8 @@ rmdir-mkdir-reversible p fs pre hperms = funext helper deleteFile-createFile-reversible : ∀ (p : Path) (fs : Filesystem) → DeleteFilePrecondition p fs → HasDefaultFilePerms p fs → - applyOp (createFileOp p) (applyOp (deleteFileOp p) fs) ≡ fs -deleteFile-createFile-reversible p fs pre hperms = funext helper + applyOp (createFileOp p) (applyOp (deleteFileOp p) fs) ≗ fs +deleteFile-createFile-reversible p fs pre hperms = helper where helper : ∀ p' → createFile p (deleteFile p fs) p' ≡ fs p' helper p' = case-split (p path-≟ p') @@ -146,7 +158,7 @@ record ReversibleDP (op : Operation) (fs : Filesystem) : Set where -- Single operation reversibility (with default-perms constraint) singleOpReversible : ∀ (op : Operation) (fs : Filesystem) → ReversibleDP op fs → - applyOp (reverseOp op) (applyOp op fs) ≡ fs + applyOp (reverseOp op) (applyOp op fs) ≗ fs singleOpReversible (mkdirOp p) fs rev = mkdir-rmdir-reversible p fs (ReversibleDP.precondition rev) singleOpReversible (rmdirOp p) fs rev with ReversibleDP.permsWitness rev @@ -169,10 +181,12 @@ data AllReversibleDP : List Operation → Filesystem → Set where -- Main composition theorem (with default-perms constraint) operationSequenceReversible : ∀ (ops : List Operation) (fs : Filesystem) → AllReversibleDP ops fs → - applySequence (reverseSequence ops) (applySequence ops fs) ≡ fs -operationSequenceReversible [] fs nilReversibleDP = refl -operationSequenceReversible (op ∷ ops) fs (consReversibleDP {op} {ops} {fs} rev revRest) = - trans (applySequence-append (reverseSequence ops) (reverseOp op ∷ []) (applySequence ops (applyOp op fs))) - (trans (cong (λ x → applyOp (reverseOp op) x) - (operationSequenceReversible ops (applyOp op fs) revRest)) - (singleOpReversible op fs rev)) + applySequence (reverseSequence ops) (applySequence ops fs) ≗ fs +operationSequenceReversible [] fs nilReversibleDP p' = refl +operationSequenceReversible (op ∷ ops) fs (consReversibleDP {op} {ops} {fs} rev revRest) p' = + trans (cong (λ g → g p') + (applySequence-append (reverseSequence ops) (reverseOp op ∷ []) + (applySequence ops (applyOp op fs)))) + (trans (applyOp-cong (reverseOp op) + (operationSequenceReversible ops (applyOp op fs) revRest) p') + (singleOpReversible op fs rev p')) diff --git a/proofs/agda/FilesystemEquivalence.agda b/proofs/agda/FilesystemEquivalence.agda index 3d9d3c4f..a4987f4d 100644 --- a/proofs/agda/FilesystemEquivalence.agda +++ b/proofs/agda/FilesystemEquivalence.agda @@ -1,3 +1,4 @@ +{-# OPTIONS --safe --without-K --cubical-compatible #-} {- Valence Shell - Filesystem Equivalence (Agda) Equivalence relations on filesystems and proofs that operations @@ -14,7 +15,7 @@ open import Data.Maybe using (Maybe; just; nothing) open import Data.Product using (_×_; _,_) open import Data.List using (List; []; _∷_) open import Relation.Nullary using (Dec; yes; no) -open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong) +open import Relation.Binary.PropositionalEquality using (_≡_; _≗_; refl; sym; trans; cong) -- Filesystem Equivalence @@ -123,14 +124,12 @@ equivSubstitution = applyOpPreservesEquiv reversibleCreatesEquiv : ∀ (op : Operation) (fs : Filesystem) → ReversibleDP op fs → applyOp (reverseOp op) (applyOp op fs) ≈ fs -reversibleCreatesEquiv op fs rev p = - cong (λ x → x p) (singleOpReversible op fs rev) +reversibleCreatesEquiv op fs rev = singleOpReversible op fs rev sequenceReversibleEquiv : ∀ (ops : List Operation) (fs : Filesystem) → AllReversibleDP ops fs → applySequence (reverseSequence ops) (applySequence ops fs) ≈ fs -sequenceReversibleEquiv ops fs hrev p = - cong (λ x → x p) (operationSequenceReversible ops fs hrev) +sequenceReversibleEquiv ops fs hrev = operationSequenceReversible ops fs hrev -- CNO Connection via Equivalence diff --git a/proofs/agda/FilesystemModel.agda b/proofs/agda/FilesystemModel.agda index bcd3dc09..65349abe 100644 --- a/proofs/agda/FilesystemModel.agda +++ b/proofs/agda/FilesystemModel.agda @@ -1,3 +1,4 @@ +{-# OPTIONS --safe --without-K --cubical-compatible #-} {- Valence Shell - Filesystem Model (Agda) A formal model of POSIX-like filesystem operations for proving @@ -15,10 +16,8 @@ open import Data.Maybe using (Maybe; just; nothing) open import Data.Bool using (Bool; true; false) open import Data.Product using (_×_; ∃; _,_; proj₁; proj₂) open import Relation.Nullary using (¬_; Dec; yes; no) -open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong; subst) +open import Relation.Binary.PropositionalEquality using (_≡_; _≗_; refl; sym; trans; cong; subst) open import Function using (_∘_) -open import Axiom.Extensionality.Propositional using (Extensionality) -open import Agda.Primitive using (lzero) open import Data.Empty using (⊥-elim) -- Path Model @@ -86,12 +85,18 @@ parentExists p fs = pathExists (parentPath p) fs hasWritePermission : Path → Filesystem → Set hasWritePermission p fs = ∃ λ node → (fs p ≡ just node) × (Permissions.writable (FSNode.permissions node) ≡ true) --- Note: isEmptyDir would require additional path prefix predicate --- Simplified version for now +-- `xs ⊑ ys`: xs is a prefix of ys (component-wise). +data _⊑_ : Path → Path → Set where + ⊑-[] : ∀ {ys} → [] ⊑ ys + ⊑-∷ : ∀ {x xs ys} → xs ⊑ ys → (x ∷ xs) ⊑ (x ∷ ys) + +-- A directory is empty when no strict descendant exists. The prefix runs +-- from p to the child (descendants), matching Coq `is_empty_dir` and the +-- Lean model after its 2026-11-09 fix. record IsEmptyDir (p : Path) (fs : Filesystem) : Set where field isDir : isDirectory p fs - -- In full version: no children exist + noChildren : ∀ child → p ⊑ child → ¬ (child ≡ p) → ¬ pathExists child fs -- Basic Lemmas pathExists-emptyFS-root : pathExists rootPath emptyFS @@ -128,6 +133,12 @@ fsUpdate-other p p' n fs p≢p' with p path-≟ p' ... | yes p≡p' = ⊥-elim (p≢p' p≡p') ... | no _ = refl +-- fsUpdate respects pointwise equality of the filesystem it updates +fsUpdate-cong : ∀ p n {fs₁ fs₂} → fs₁ ≗ fs₂ → fsUpdate p n fs₁ ≗ fsUpdate p n fs₂ +fsUpdate-cong p n h p' with p path-≟ p' +... | yes _ = refl +... | no _ = h p' + -- mkdir: Create a directory record MkdirPrecondition (p : Path) (fs : Filesystem) : Set where field @@ -151,32 +162,20 @@ rmdir p fs = fsUpdate p nothing fs -- Postcondition Theorems mkdir-creates-directory : ∀ p fs → MkdirPrecondition p fs → isDirectory p (mkdir p fs) -mkdir-creates-directory p fs pre with p path-≟ p -... | yes refl = defaultPerms , refl -... | no p≢p = ⊥-elim (p≢p refl) - where - open import Data.Empty using (⊥-elim) +mkdir-creates-directory p fs pre = defaultPerms , fsUpdate-at p _ fs mkdir-path-exists : ∀ p fs → MkdirPrecondition p fs → pathExists p (mkdir p fs) -mkdir-path-exists p fs pre with p path-≟ p -... | yes refl = mkFSNode Directory defaultPerms , refl -... | no p≢p = ⊥-elim (p≢p refl) - where - open import Data.Empty using (⊥-elim) +mkdir-path-exists p fs pre = mkFSNode Directory defaultPerms , fsUpdate-at p _ fs rmdir-removes-path : ∀ p fs → RmdirPrecondition p fs → ¬ pathExists p (rmdir p fs) -rmdir-removes-path p fs pre (node , eq) with p path-≟ p -... | yes refl = nothing≢just eq -... | no p≢p = ⊥-elim (p≢p refl) - where - open import Data.Empty using (⊥-elim) +rmdir-removes-path p fs pre (node , eq) = + nothing≢just (trans (sym (fsUpdate-at p nothing fs)) eq) --- AXIOM: Functional extensionality at level 0. --- Uses stdlib's canonical Extensionality type (Axiom.Extensionality.Propositional). --- Consistent with standard Agda type theory; provable under --cubical. --- See also: HoTT Book, Axiom 2.9.3. -postulate - funext : Extensionality lzero lzero +-- Filesystem equality is pointwise (`_≗_`): two filesystems are equal when +-- they agree on every path. This needs no function extensionality, so the +-- module checks under `--safe --without-K --cubical-compatible`. (Until +-- 2026-11-09 these theorems were stated with `_≡_` on functions and closed +-- with a postulated `funext`.) -- Helper: from ¬ pathExists, derive fs p ≡ nothing not-path-exists-nothing : ∀ {p : Path} {fs : Filesystem} → @@ -189,8 +188,8 @@ not-path-exists-nothing {p} {fs} notEx with fs p mkdir-rmdir-reversible : ∀ p fs → MkdirPrecondition p fs → - rmdir p (mkdir p fs) ≡ fs -mkdir-rmdir-reversible p fs pre = funext helper + rmdir p (mkdir p fs) ≗ fs +mkdir-rmdir-reversible p fs pre = helper where open import Data.Empty using (⊥-elim) diff --git a/proofs/agda/PermissionOperations.agda b/proofs/agda/PermissionOperations.agda index 8b0ff3bd..8d4d6e9d 100644 --- a/proofs/agda/PermissionOperations.agda +++ b/proofs/agda/PermissionOperations.agda @@ -1,3 +1,4 @@ +{-# OPTIONS --safe --without-K --cubical-compatible #-} {- SPDX-License-Identifier: MPL-2.0 -} {- Valence Shell - Permission Operations (Agda) @@ -15,7 +16,7 @@ open import Data.Nat using (ℕ) open import Data.Bool using (Bool; true; false) open import Relation.Nullary using (¬_; Dec; yes; no) open import Data.Empty using (⊥-elim) -open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong; subst) +open import Relation.Binary.PropositionalEquality using (_≡_; _≗_; refl; sym; trans; cong; subst) -- ============================================================================ -- Extended Types for Permission/Ownership @@ -107,8 +108,8 @@ chmod-other p p' m fs p≢p' with p pathExt-≟ p' -- chmod is reversible — restoring old mode restores fs chmod-reversible : ∀ p fs oldMode newMode → (hold : ∃ λ node → (fs p ≡ just node) × (FSNodeExt.mode node ≡ oldMode)) → - chmod p oldMode (chmod p newMode fs) ≡ fs -chmod-reversible p fs oldMode newMode (node , hnode , hmode) = funext helper + chmod p oldMode (chmod p newMode fs) ≗ fs +chmod-reversible p fs oldMode newMode (node , hnode , hmode) = helper where node-modes : Mode → FSNodeExt node-modes m = mkFSNodeExt (FSNodeExt.nodeType node) m (FSNodeExt.owner node) @@ -130,8 +131,8 @@ chmod-reversible p fs oldMode newMode (node , hnode , hmode) = funext helper -- chmod to same mode is identity chmod-same-mode : ∀ p fs m → (hold : ∃ λ node → (fs p ≡ just node) × (FSNodeExt.mode node ≡ m)) → - chmod p m fs ≡ fs -chmod-same-mode p fs m (node , hnode , hmode) = funext helper + chmod p m fs ≗ fs +chmod-same-mode p fs m (node , hnode , hmode) = helper where node-modes : Mode → FSNodeExt node-modes md = mkFSNodeExt (FSNodeExt.nodeType node) md (FSNodeExt.owner node) @@ -184,8 +185,8 @@ chown-other p p' o fs p≢p' with p pathExt-≟ p' -- chown is reversible — restoring old owner restores fs chown-reversible : ∀ p fs oldOwner newOwner → (hold : ∃ λ node → (fs p ≡ just node) × (FSNodeExt.owner node ≡ oldOwner)) → - chown p oldOwner (chown p newOwner fs) ≡ fs -chown-reversible p fs oldOwner newOwner (node , hnode , howner) = funext helper + chown p oldOwner (chown p newOwner fs) ≗ fs +chown-reversible p fs oldOwner newOwner (node , hnode , howner) = helper where node-owners : Ownership → FSNodeExt node-owners o = mkFSNodeExt (FSNodeExt.nodeType node) (FSNodeExt.mode node) o @@ -207,8 +208,8 @@ chown-reversible p fs oldOwner newOwner (node , hnode , howner) = funext helper -- chown to same owner is identity chown-same-owner : ∀ p fs o → (hold : ∃ λ node → (fs p ≡ just node) × (FSNodeExt.owner node ≡ o)) → - chown p o fs ≡ fs -chown-same-owner p fs o (node , hnode , howner) = funext helper + chown p o fs ≗ fs +chown-same-owner p fs o (node , hnode , howner) = helper where node-owners : Ownership → FSNodeExt node-owners ow = mkFSNodeExt (FSNodeExt.nodeType node) (FSNodeExt.mode node) ow diff --git a/proofs/agda/PreconditionWitnesses.agda b/proofs/agda/PreconditionWitnesses.agda new file mode 100644 index 00000000..40892b41 --- /dev/null +++ b/proofs/agda/PreconditionWitnesses.agda @@ -0,0 +1,66 @@ +{-# OPTIONS --safe --without-K --cubical-compatible #-} +-- SPDX-License-Identifier: MPL-2.0 +{- Valence Shell - precondition non-vacuity witnesses (Agda) + + Every reversibility theorem has the shape `Pre p fs → op⁻¹ (op p fs) ≗ fs`. + If `Pre` is uninhabited the theorem says nothing. This module exhibits one + concrete state per precondition, so an edit that empties a precondition + fails the check. Mirrors proofs/lean4/PreconditionWitnesses.lean. + Added 2026-11-09; see docs/audits/2026-11-09-proof-ground-truth.adoc. +-} + +module PreconditionWitnesses where + +open import FilesystemModel +open import FileOperations +open import SymlinkOperations +open import Data.List using (List; []; _∷_) +open import Data.Maybe using (just; nothing) +open import Data.Product using (_,_) +open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans) +open import Relation.Nullary using (¬_) + +a : Path +a = "a" ∷ [] + +mkdir-pre-inhabited : MkdirPrecondition a emptyFS +mkdir-pre-inhabited = record + { notExists = λ { (_ , ()) } + ; parent-path-exists = mkFSNode Directory defaultPerms , refl + ; parentIsDir = defaultPerms , refl + } + +-- The emptiness field is the one that was missing before 2026-11-09. +rmdir-pre-inhabited : RmdirPrecondition a (mkdir a emptyFS) +rmdir-pre-inhabited = record + { isDir = defaultPerms , fsUpdate-at a _ emptyFS + ; isEmpty = record + { isDir = defaultPerms , fsUpdate-at a _ emptyFS + ; noChildren = no-children + } + ; notRoot = λ () + } + where + no-children : ∀ child → a ⊑ child → ¬ (child ≡ a) → ¬ pathExists child (mkdir a emptyFS) + no-children (.("a") ∷ []) (⊑-∷ ⊑-[]) ne _ = ne refl + no-children (.("a") ∷ y ∷ ys) (⊑-∷ ⊑-[]) _ (node , eq) = + nothing≢just (trans (sym (fsUpdate-other a ("a" ∷ y ∷ ys) (just (mkFSNode Directory defaultPerms)) emptyFS λ ())) eq) + +createFile-pre-inhabited : CreateFilePrecondition a emptyFS +createFile-pre-inhabited = record + { notExists = λ { (_ , ()) } + ; parent-path-exists = mkFSNode Directory defaultPerms , refl + ; parentIsDir = defaultPerms , refl + } + +deleteFile-pre-inhabited : DeleteFilePrecondition a (createFile a emptyFS) +deleteFile-pre-inhabited = record + { deletedIsFile = defaultPerms , fsUpdate-at a _ emptyFS } + +symlink-pre-inhabited : SymlinkPrecondition a emptyFS +symlink-pre-inhabited = record + { notExists = λ { (_ , ()) } + ; parent-path-exists = mkFSNode Directory defaultPerms , refl + ; parentIsDir = defaultPerms , refl + ; parentWritable = mkFSNode Directory defaultPerms , refl , refl + } diff --git a/proofs/agda/README.adoc b/proofs/agda/README.adoc index 4cffa210..7204d5c2 100644 --- a/proofs/agda/README.adoc +++ b/proofs/agda/README.adoc @@ -2,10 +2,9 @@ // Copyright (c) Jonathan D.A. Jewell = proofs/agda/ — Agda Filesystem Proofs (Intensional Type Theory) -Agda (intensional dependent type theory) cross-validates the -filesystem reversibility theorems against the primary Lean 4 source -of truth (`../lean4/`). Agda's intensional treatment of equality -provides a different lens than Lean's HoTT-flavoured framework. +Agda is the theory source of truth for the filesystem reversibility +theorems (owner ruling 2026-11-09, per `standards` PROOF-POLICY §1). The Lean 4 +(`../lean4/`) and Rocq (`../coq/`) trees are recheck legs. == Files @@ -22,6 +21,8 @@ provides a different lens than Lean's HoTT-flavoured framework. | `PermissionOperations.agda` | chmod/chown bit-preservation. | `SymlinkOperations.agda` | Symlink creation + traversal. | `RMOOperations.agda` | Remove-Match-Obliterate (GDPR-relevant). +| `PreconditionWitnesses.agda` | One inhabitant per operation precondition (non-vacuity). +| `All.agda` | Imports every module; the file CI checks. |=== Manifest: @@ -33,31 +34,24 @@ Manifest: ```bash cd proofs/agda -agda --library-file=.agda-lib --library=valence-shell FilesystemModel.agda # single module -agda --library-file=.agda-lib --library=valence-shell CopyMoveOperations.agda # transitive +agda --safe --without-K --cubical-compatible All.agda ``` -All nine modules type-check this way under Agda 2.6.4.3 + stdlib 2.1.1 and under -Agda 2.7.0.1 + stdlib 2.2. - -*Waiver (see `VERIFICATION.adoc`).* The estate invocation is -`agda --safe --without-K --cubical-compatible`, and this tree does **not** meet -it: `--safe` reports `Cannot postulate funext with safe flag` and `--without-K` -reports `Cannot eliminate reflexive equation p = p of type List String because K -has been disabled`. The commands above are therefore the *unflagged* invocation, -used under a recorded waiver. Do not add `--safe` or `--without-K` to them until -those two obstacles are discharged. +This is the estate invocation (PROOF-POLICY §2.1). It checks all ten modules +under Agda 2.7.0.1 + agda-stdlib v2.2; CI runs the same command +(`.github/workflows/agda.yml`). See `VERIFICATION.adoc` for the receipt. == Conventions -* Status under PROOF-POLICY §5 is `proven-with-postulates` (one postulate: - `funext` in `FilesystemModel`) -- the waiver above is why it is not `proven`. +* Status under PROOF-POLICY §5 is `PROVEN`: no postulates, no escape pragmas. +* Filesystem equality is pointwise (`_≗_`), so no function extensionality is + needed. * PascalCase module names; one module per file. * No `.agdai` interface artefacts in tree (cached locally, not committed). == See also * `../README.md` — overall proof-stack design -* `../lean4/README.adoc` — primary source of truth +* `../lean4/README.adoc` — Lean recheck leg * `../../docs/PROOF_HOLES_AUDIT.adoc` — proof-debt status across all systems diff --git a/proofs/agda/RMOOperations.agda b/proofs/agda/RMOOperations.agda index f20c8f81..06198631 100644 --- a/proofs/agda/RMOOperations.agda +++ b/proofs/agda/RMOOperations.agda @@ -1,3 +1,4 @@ +{-# OPTIONS --safe --without-K --cubical-compatible #-} -- SPDX-License-Identifier: MPL-2.0 {- Valence Shell - RMO (Remove / Match / Obliterate) operations in Agda @@ -29,7 +30,7 @@ open import Data.List using (List; []; _∷_; length; map) open import Data.Bool using (Bool; true; false; if_then_else_) open import Data.Product using (_×_; _,_; proj₁; proj₂; ∃; ∃-syntax) open import Data.Maybe using (Maybe; just; nothing) -open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym; trans; subst) +open import Relation.Binary.PropositionalEquality using (_≡_; _≗_; refl; cong; sym; trans; subst) open import Relation.Nullary using (¬_; Dec; yes; no) open import Data.Empty using (⊥; ⊥-elim) open import Data.List.Properties using (length-map) diff --git a/proofs/agda/SymlinkOperations.agda b/proofs/agda/SymlinkOperations.agda index 34695e8a..57c437ff 100644 --- a/proofs/agda/SymlinkOperations.agda +++ b/proofs/agda/SymlinkOperations.agda @@ -1,3 +1,4 @@ +{-# OPTIONS --safe --without-K --cubical-compatible #-} {- Valence Shell - Symlink Operations (Agda) Abstract model of symbolic link creation and removal. @@ -11,7 +12,7 @@ open import FilesystemModel open import Data.Maybe using (just; nothing) open import Data.Product using (_×_; _,_) open import Relation.Nullary using (¬_; Dec; yes; no) -open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans) +open import Relation.Binary.PropositionalEquality using (_≡_; _≗_; refl; sym; trans) -- Preconditions for creating a symlink record SymlinkPrecondition (p : Path) (fs : Filesystem) : Set where @@ -31,22 +32,15 @@ unlink p fs = fsUpdate p nothing fs -- Postcondition Lemmas symlink-creates-path : ∀ p fs → SymlinkPrecondition p fs → pathExists p (symlink p fs) -symlink-creates-path p fs pre with p path-≟ p -... | yes refl = mkFSNode File defaultPerms , refl -... | no p≢p = ⊥-elim (p≢p refl) - where - open import Data.Empty using (⊥-elim) +symlink-creates-path p fs pre = mkFSNode File defaultPerms , fsUpdate-at p _ _ unlink-removes-path : ∀ p fs → pathExists p fs → ¬ pathExists p (unlink p fs) -unlink-removes-path p fs (node , eq) with p path-≟ p -... | yes refl = λ () -... | no p≢p = ⊥-elim (p≢p refl) - where - open import Data.Empty using (⊥-elim) +unlink-removes-path p fs _ (node , eq) = + nothing≢just (trans (sym (fsUpdate-at p nothing fs)) eq) -- Reversibility Theorem -symlink-unlink-reversible : ∀ p fs → SymlinkPrecondition p fs → unlink p (symlink p fs) ≡ fs -symlink-unlink-reversible p fs pre = funext helper +symlink-unlink-reversible : ∀ p fs → SymlinkPrecondition p fs → unlink p (symlink p fs) ≗ fs +symlink-unlink-reversible p fs pre = helper where helper : ∀ p' → unlink p (symlink p fs) p' ≡ fs p' helper p' = case-split (p path-≟ p') diff --git a/proofs/agda/VERIFICATION.adoc b/proofs/agda/VERIFICATION.adoc index 51116998..b620c7e1 100644 --- a/proofs/agda/VERIFICATION.adoc +++ b/proofs/agda/VERIFICATION.adoc @@ -1,72 +1,65 @@ = Agda proof verification record :toc: preamble -This file is the receipt that `standards/3-practice/PROOF-POLICY.adoc` §4 asks for: -the invocation, the exact versions, the result, and the *waiver* that records why -this artefact does not yet meet the estate invocation. +This file is the receipt that `standards/3-practice/PROOF-POLICY.adoc` §2.1 and +§8 ask for: the invocation, the exact versions, the flags in force, the import +cone and the result. Owner ruling 2026-11-09: Agda is this repository's theory +source of truth; Lean and Rocq are recheck legs. -== What was run +== What was run (2026-11-09) -[cols="3,1,1",options="header"] +[cols="3,2",options="header"] |=== -| Invocation | Agda 2.6.4.3 + stdlib 2.1.1 | Agda 2.7.0.1 + stdlib 2.2 +| Invocation | Agda 2.7.0.1 + agda-stdlib v2.2 (`6cd04e46`) -| `agda --library-file= --library=valence-shell .agda`, all nine modules -| 9/9 type-check | 9/9 type-check - -| same, plus `--safe` -| rejected | rejected - -| same, plus `--without-K` -| rejected | rejected - -| same, plus `--cubical-compatible` -| rejected | rejected +| `agda --safe --without-K --cubical-compatible All.agda` +| exit 0; all 10 modules checked |=== -Modules: `FilesystemModel`, `FileOperations`, `SymlinkOperations`, -`PermissionOperations`, `FilesystemComposition`, `FilesystemEquivalence`, -`CopyMoveOperations`, `FileContentOperations`, `RMOOperations`. - -== The two rejections, verbatim - -[source] ----- -FilesystemModel.agda:179,3-38 -Cannot postulate funext with safe flag -when scope checking the declaration - funext : Extensionality lzero lzero ----- - -[source] ----- -FilesystemModel.agda:155,11-15 -I'm not sure if there should be a case for the constructor refl, -because I get stuck when trying to solve the following unification -problems (inferred index ≟ expected index): - p ≟ p -Possible reason why unification failed: - Cannot eliminate reflexive equation p = p of type List String - because K has been disabled. ----- - -The first is `postulate funext` in `FilesystemModel`. The second is *not* about -`funext`: any case split on `Dec (p ≡ p)` needs K, because Agda cannot eliminate -the reflexive equation on `List String` without it. Every `... | yes refl` clause -over `p path-≟ p` depends on that, so removing the postulate alone would not make -`--without-K` pass. - -== Status and waiver - -* Status under PROOF-POLICY §5: `proven-with-postulates`. -* Status under mathesis §5: *Claimed / reproduced*, **not** grade 3. -* Waiver: this artefact is checked with the unflagged `agda` invocation because the - two blockers above are proof-engineering work, not documentation work. The waiver - expires when either (a) `funext` is discharged (state whole-filesystem - reversibility pointwise, or move the tree to a `--cubical` build), or (b) the path - decision is threaded through the operations instead of being re-asked with - `p ≟ p` at each site. Until then, no claim in this repository may say the Agda - layer is checked under `--safe --without-K --cubical-compatible`. +Import cone (`All.agda`): `FilesystemModel`, `FileOperations`, +`SymlinkOperations`, `PermissionOperations`, `FilesystemComposition`, +`FilesystemEquivalence`, `CopyMoveOperations`, `FileContentOperations`, +`RMOOperations`, `PreconditionWitnesses`. Each file also carries +`{-# OPTIONS --safe --without-K --cubical-compatible #-}`. No `postulate` and +no escape pragma remains; CI (`.github/workflows/agda.yml`) rejects either. + +Toolchain digest: Agda release archive sha256 +`975b515a14877ab6bce5bfc641e16c4a3ee52ca5d7f846577dee80aa2145db8a`. It is +installed from the upstream archive, not Guix: an open §6 `deviation`, +recorded in the workflow and in `PROOF-NEEDS.adoc`. + +== What changed to get there + +* *`funext` removed.* Whole-filesystem equalities are now pointwise + (`_≗_`). Every former `funext helper` proof was already pointwise inside, + so the theorems keep their content and lose the postulate. Composition uses + two new congruence lemmas, `fsUpdate-cong` and `applyOp-cong` / + `applySequence-cong`. +* *K removed.* Clauses that matched `refl` on `p ≡ p` (from `p path-≟ p`) + now use `fsUpdate-at`, which needs no K. +* *`IsEmptyDir` completed.* It had only an `isDir` field. It now also has + `noChildren`: no strict descendant (`p ⊑ child`, `child ≢ p`) exists. The + descendant direction matches Coq and the fixed Lean model. +* *Non-vacuity witnesses.* `PreconditionWitnesses` gives an inhabitant of the + mkdir, rmdir, createFile, deleteFile and symlink preconditions. + +== Warnings + +The check prints `UnsupportedIndexedMatch` warnings. They come from matching +`yes` / `no` on the standard library's `Dec`, whose `Reflects` index +needs constructor injectivity that Cubical Agda does not support. The +consequence is that these functions would not compute under cubical +transport. Nothing here is used from Cubical Agda, so they do not affect the +result. Removing them means replacing `Dec` with a non-indexed decision +type throughout; that is recorded as optional clean-up, not done. + +== Status + +* PROOF-POLICY §5: `PROVEN` for every theorem in the cone. +* PROOF-POLICY §8: `PWG-3` once this check runs green in CI on the current + head (receipts are per commit). No recheck leg counts yet: the Lean and Rocq + statements have not been compared with these (§2.2 `AGDA-VERIFIED`, legs + `BRIDGE-PENDING`). == History From 34e92356831136a5dfb7b8ca1f79060c14eebf9b Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:44:07 +0000 Subject: [PATCH 04/10] chore(proofs): archive Isabelle and Mizar; make the Z3 checks non-circular MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Owner ruling 2026-11-09. Isabelle and Mizar move to archive/proofs/ (kept, never deleted). Neither had a CI lane or a checked run; under PROOF-POLICY Isabelle is supplementary only and Mizar is a §4 exception. archive/proofs/README.adoc maps all 139 archived theorems to successors by name: 103 name an Agda successor, 29 only a Lean or Rocq one, 2 are only related, and 6 are Mizar set-theory helpers that need none. Every consumer is updated in the same change: both Justfiles, scripts/verify-proofs.sh and scripts/validate-with-echidna.sh. build-agda now runs the canonical invocation on All.agda. Z3: filesystem_operations.smt2 asserted each theorem as an axiom before checking it, and symlink_operations.smt2 never negated a goal. Both now define the operations as array stores, check non-vacuity (sat) and negate every goal (unsat). Dropping a precondition yields sat, so the encoding separates true from false statements. The other three files keep their axiomatic encoding with a §4 note saying so. verify-z3.sh carries the new exact result sequences; all five pass. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDjNR1ZoYKEPxSKE2nq --- .machine_readable/contractiles/Justfile | 34 +-- CLAUDE.md | 12 +- CONTRIBUTING.adoc | 7 +- EXPLAINME.adoc | 23 +- Justfile | 34 +-- REVIEW.adoc | 5 + archive/proofs/README.adoc | 173 +++++++++++ .../proofs}/isabelle/CopyMoveOperations.thy | 0 .../isabelle/FileContentOperations.thy | 0 .../proofs}/isabelle/FileOperations.thy | 0 .../isabelle/FilesystemComposition.thy | 0 .../isabelle/FilesystemEquivalence.thy | 0 .../proofs}/isabelle/FilesystemModel.thy | 0 .../proofs}/isabelle/PermissionOperations.thy | 0 .../proofs}/isabelle/README.adoc | 0 .../proofs}/isabelle/RMO_Operations.thy | 0 {proofs => archive/proofs}/isabelle/ROOT | 0 .../proofs}/isabelle/SymlinkOperations.thy | 0 {proofs => archive/proofs}/mizar/.gitignore | 0 {proofs => archive/proofs}/mizar/README.adoc | 0 .../proofs}/mizar/copy_move_operations.miz | 0 .../proofs}/mizar/file_content_operations.miz | 0 .../proofs}/mizar/file_operations.miz | 0 .../proofs}/mizar/filesystem_composition.miz | 0 .../proofs}/mizar/filesystem_equivalence.miz | 0 .../proofs}/mizar/filesystem_model.miz | 0 .../proofs}/mizar/permission_operations.miz | 0 .../proofs}/mizar/rmo_operations.miz | 0 .../proofs}/mizar/symlink_operations.miz | 0 proofs/README.adoc | 24 +- proofs/z3/README.adoc | 2 +- proofs/z3/copy_move_operations.smt2 | 8 + proofs/z3/filesystem_operations.smt2 | 283 ++++++++---------- proofs/z3/permission_operations.smt2 | 8 + proofs/z3/rmo_operations.smt2 | 8 + proofs/z3/symlink_operations.smt2 | 104 ++++--- scripts/validate-with-echidna.sh | 16 +- scripts/verify-proofs.sh | 33 +- scripts/verify-z3.sh | 4 +- 39 files changed, 444 insertions(+), 334 deletions(-) create mode 100644 archive/proofs/README.adoc rename {proofs => archive/proofs}/isabelle/CopyMoveOperations.thy (100%) rename {proofs => archive/proofs}/isabelle/FileContentOperations.thy (100%) rename {proofs => archive/proofs}/isabelle/FileOperations.thy (100%) rename {proofs => archive/proofs}/isabelle/FilesystemComposition.thy (100%) rename {proofs => archive/proofs}/isabelle/FilesystemEquivalence.thy (100%) rename {proofs => archive/proofs}/isabelle/FilesystemModel.thy (100%) rename {proofs => archive/proofs}/isabelle/PermissionOperations.thy (100%) rename {proofs => archive/proofs}/isabelle/README.adoc (100%) rename {proofs => archive/proofs}/isabelle/RMO_Operations.thy (100%) rename {proofs => archive/proofs}/isabelle/ROOT (100%) rename {proofs => archive/proofs}/isabelle/SymlinkOperations.thy (100%) rename {proofs => archive/proofs}/mizar/.gitignore (100%) rename {proofs => archive/proofs}/mizar/README.adoc (100%) rename {proofs => archive/proofs}/mizar/copy_move_operations.miz (100%) rename {proofs => archive/proofs}/mizar/file_content_operations.miz (100%) rename {proofs => archive/proofs}/mizar/file_operations.miz (100%) rename {proofs => archive/proofs}/mizar/filesystem_composition.miz (100%) rename {proofs => archive/proofs}/mizar/filesystem_equivalence.miz (100%) rename {proofs => archive/proofs}/mizar/filesystem_model.miz (100%) rename {proofs => archive/proofs}/mizar/permission_operations.miz (100%) rename {proofs => archive/proofs}/mizar/rmo_operations.miz (100%) rename {proofs => archive/proofs}/mizar/symlink_operations.miz (100%) diff --git a/.machine_readable/contractiles/Justfile b/.machine_readable/contractiles/Justfile index 51427221..74ac85b2 100644 --- a/.machine_readable/contractiles/Justfile +++ b/.machine_readable/contractiles/Justfile @@ -8,7 +8,7 @@ default: @just --list # Build all proofs across all systems -build-all: build-coq build-lean4 build-agda build-isabelle build-mizar build-idris2 +build-all: build-coq build-lean4 build-agda build-idris2 @echo "✓ All proofs built" # Verify all proofs @@ -34,21 +34,11 @@ build-lean4: # Build Agda proofs build-agda: @echo "Building Agda proofs..." - cd proofs/agda && agda FilesystemModel.agda - cd proofs/agda && agda FileOperations.agda - @echo "✓ Agda proofs type-checked" - -# Build Isabelle proofs -build-isabelle: - @echo "Building Isabelle proofs..." - cd proofs/isabelle && isabelle build -D . - @echo "✓ Isabelle proofs verified" - -# Build Mizar proofs (requires Mizar setup) -build-mizar: - @echo "Building Mizar proofs..." - cd proofs/mizar && mizf filesystem_model.miz || echo "⚠ Mizar not configured" - cd proofs/mizar && mizf file_operations.miz || echo "⚠ Mizar not configured" + cd proofs/agda && agda --safe --without-K --cubical-compatible All.agda + @echo "✓ Agda proofs checked (estate invocation, all modules)" + +# Isabelle and Mizar were archived to archive/proofs/ on 2026-11-09 (owner +# ruling; see archive/proofs/README.adoc). They have no build recipe. # Requires Idris2 0.8.0. Install via: # nix-shell -p idris2 # recommended for reproducibility @@ -236,8 +226,8 @@ ci: clean build-all verify-all test-all stats: @echo "=== Valence Shell Statistics ===" @echo "" - @echo "Proof Code (Coq/Lean/Agda/Isabelle/Mizar):" - @find proofs -name "*.v" -o -name "*.lean" -o -name "*.agda" -o -name "*.thy" -o -name "*.miz" 2>/dev/null | xargs wc -l 2>/dev/null | tail -1 || echo " 0 total" + @echo "Proof Code (Agda/Rocq/Lean; Isabelle and Mizar archived):" + @find proofs -name "*.v" -o -name "*.lean" -o -name "*.agda" 2>/dev/null | xargs wc -l 2>/dev/null | tail -1 || echo " 0 total" @echo "" @echo "Zig FFI Code:" @find impl/zig -name "*.zig" 2>/dev/null | xargs wc -l 2>/dev/null | tail -1 || echo " 0 total" @@ -269,7 +259,7 @@ watch: echidna-verify: @if command -v echidna &> /dev/null; then \ echo "Running ECHIDNA multi-prover verification..."; \ - echidna verify --all --targets coq,lean4,agda,isabelle,mizar; \ + echidna verify --all --targets coq,lean4,agda; \ else \ echo "⚠ ECHIDNA not installed. Using built-in verification."; \ just verify-all; \ @@ -292,7 +282,7 @@ certify: "version": "${VERSION}", "generated": "${TIMESTAMP}", "prover": "valence-shell", - "proof_systems": ["coq", "lean4", "agda", "isabelle", "mizar", "z3"], + "proof_systems": ["coq", "lean4", "agda", "z3"], "verified_properties": [ { "theorem": "mkdir_rmdir_reversible", @@ -340,8 +330,6 @@ certify: - Coq (primary) - Lean 4 (cross-verification) - Agda (dependent types) - - Isabelle/HOL (classical logic) - - Mizar (mathematical proofs) - Z3 (SMT verification) ### Key Theorems Verified @@ -388,8 +376,6 @@ help: @echo " just build-coq - Build Coq proofs" @echo " just build-lean4 - Build Lean 4 proofs" @echo " just build-agda - Build Agda proofs" - @echo " just build-isabelle - Build Isabelle proofs" - @echo " just build-mizar - Build Mizar proofs" @echo " just build-idris2 - Build Idris2 proofs" @echo " just verify-idris2 - Build + hole-count Idris2 proofs" @echo "" diff --git a/CLAUDE.md b/CLAUDE.md index 5080d6da..d7c93c53 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -63,7 +63,8 @@ the same change as that file. Which verifier carries which obligation: ruling 2026-11-09 adopts this order here: the Agda tree is the source and checks under the canonical invocation; the existing Lean and Rocq proofs are target-only evidence until compared (`docs/audits/2026-11-09-proof-ground-truth.adoc`). -* Isabelle/Mizar/Z3 are §4 exceptions and need a recorded exception note. +* Z3 is a §4 exception; its notes are recorded in each `.smt2` header. Isabelle and + Mizar were archived unchecked to `archive/proofs/` (owner ruling 2026-11-09). Status vocabulary is closed (`PROOF-POLICY` §5): `proven`, `proven-with-postulates`, `argued`, `tested-only`, `open`. Every obligation's status @@ -188,9 +189,8 @@ deep-audit session). The corresponding Phase 4C design docs under - Agda — theory source of truth (owner ruling 2026-11-09) - Lean 4 — recheck leg; also the executable model oracle - Coq — CIC foundation, extraction to OCaml -- Isabelle/HOL — cross-validation -- Mizar — set theory foundation -- Z3 SMT — automated verification +- Z3 SMT — automated checks (ASSUMED under PROOF-POLICY §5) +- Isabelle/HOL and Mizar — archived unchecked 2026-11-09 (`archive/proofs/`) **Runtime**: - Rust — primary shell implementation (`impl/rust-cli/`) @@ -216,9 +216,7 @@ valence-shell/ lean4/ # Lean recheck leg + executable model oracle (101 theorems) coq/ # CIC proofs + extraction (131 theorems, 0 admits — re-verified 2026-07-16, Coq 8.18.0) agda/ # Theory source of truth (owner ruling 2026-11-09); 10 modules, 0 postulates, --safe --without-K --cubical-compatible - isabelle/ # HOL proofs (76 theorems) - mizar/ # Set theory proofs (63 theorems) - z3/ # SMT proofs (125 asserts) + z3/ # SMT checks (ASSUMED; 2 files definitional, 3 axiomatic) idris2/ # ABI carrier (0 holes, 0 partials, 2 primitive-eq axioms) docs/ # Design docs, roadmaps, PROOF_HOLES_AUDIT.adoc audits/ # Deep-audit log (per estate standards) diff --git a/CONTRIBUTING.adoc b/CONTRIBUTING.adoc index 8cec6510..bb5544bd 100644 --- a/CONTRIBUTING.adoc +++ b/CONTRIBUTING.adoc @@ -24,9 +24,7 @@ perimeters: *Who*: Project maintainers with formal methods expertise *Files*: - `+proofs/coq/*.v+` - Coq proofs - `+proofs/lean4/*.lean+` - -Lean 4 proofs - `+proofs/agda/*.agda+` - Agda proofs - -`+proofs/isabelle/*.thy+` - Isabelle proofs - `+proofs/mizar/*.miz+` - -Mizar proofs - `+impl/ocaml/filesystem_ffi.ml+` - FFI layer +Lean 4 proofs - `+proofs/agda/*.agda+` - Agda proofs (theory source) - `+impl/ocaml/filesystem_ffi.ml+` - FFI layer *Requirements*: - Formal verification expertise - Proof assistant proficiency - Security review process - Maintainer approval required @@ -86,7 +84,7 @@ Matters`" Bash *Full Development* (to modify proofs): - Coq 8.18+ - Lean 4.3+ - Agda -2.6.4+ - Isabelle 2024 - Z3 4.12+ - Just (command runner) - Nix +2.7.0.1 with agda-stdlib v2.2 - Z3 4.8+ - Just (command runner) - Nix (recommended for reproducible builds) ==== Setup Instructions @@ -276,7 +274,6 @@ just verify-proofs just build-coq just build-lean4 just build-agda -just build-isabelle ---- ==== Implementation Testing diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index c693135d..23d8afc5 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -15,7 +15,9 @@ claims, and the second is a count of *candidates*, not of proved theorems. **Evidence**: `impl/rust-cli/` is where the tests live (`cargo test --all-features`); the -proof trees are `proofs/{coq,lean4,agda,idris2,isabelle,mizar,z3}/`. The Coq +proof trees are `proofs/{agda,coq,lean4,idris2,z3}/` (Agda is the theory source since the +2026-11-09 owner ruling; Isabelle and Mizar were archived to `archive/proofs/` the +same day). The Coq tree alone declares 133 `Theorem`/`Lemma` commands and contains no `admit`/`Admitted`. @@ -33,7 +35,8 @@ code, and no percentage is quoted for that correspondence: it is `argued` plus **Evidence**: `proofs/coq/filesystem_model.v:207` (`mkdir_rmdir_reversible`), with the same property restated in `proofs/lean4/FilesystemModel.lean`, `proofs/agda/FilesystemModel.agda`, -`proofs/isabelle/`, `proofs/mizar/` and `proofs/z3/`. The composition lemma is +and `proofs/z3/` (the Isabelle and Mizar restatements are archived in +`archive/proofs/`). The composition lemma is `proofs/coq/filesystem_composition.v:352` (`operation_sequence_reversible`). **Caveat**: this is a theorem about an abstract `Filesystem` function, not about @@ -117,11 +120,11 @@ reproduce. Absence of a tool is an open obligation, not a passing leg | `proofs/agda/` (ten modules via `All.agda`) | No postulates, no holes, the estate invocation. Filesystem equality is pointwise (`_≗_`). Grade `PWG-3` is derived from the CI receipt on the merge head, not asserted here. See `docs/audits/2026-11-09-proof-ground-truth.adoc` -| Same theorems restated in Isabelle / Mizar / Z3 -| proven-with-postulates (Isabelle) / open (Mizar) / Z3: reproduced for 4 of 5 files, `open` for `symlink_operations.smt2` -| `isabelle build -D .`; `mizf` (failure-swallowing target); z3-solver 5.3.3, one process per file, parsing each `(check-sat)` -| `proofs/isabelle/`, `proofs/mizar/`, `proofs/z3/` -| §4 exceptions to PROOF-POLICY §1 with no recorded exception note yet; the Mizar target ends in `|| echo`, so a failing Mizar build is not distinguishable from a pass +| Same theorems restated in Z3 (Isabelle and Mizar archived 2026-11-09) +| Z3: ASSUMED (no proof certificate) +| `scripts/verify-z3.sh`, exact result sequence per file +| `proofs/z3/` (`archive/proofs/` for Isabelle and Mizar) +| §4 exception notes are now recorded in each `.smt2` header. `filesystem_operations` and `symlink_operations` were rewritten on 2026-11-09 to define the operations as array `store`s and negate each goal; the other three still rest on asserted axioms. Isabelle and Mizar were never CI-checked and are archived, unchecked, with a successor map | Sandbox path normalisation never escapes the root | proven (model) / tested-only (code) @@ -180,7 +183,7 @@ reproduce. Absence of a tool is an open obligation, not a passing leg == Dogfooded Across The Account -Uses polyglot formal verification stack (Coq + Lean 4 + Agda + Isabelle + Mizar + Z3). Same pattern across: +Uses a multi-prover stack (Agda as theory source, Rocq and Lean 4 as recheck legs, Idris2 for the ABI, Z3 as a supplementary check). Same pattern across: - https://github.com/hyperpolymath/absolute-zero[absolute-zero] — Compositional algebra with CNO (Certified Null Operation) theory - https://github.com/hyperpolymath/proven-servers[proven-servers] — Protocol verification (Idris2 ABI) - https://github.com/hyperpolymath/burble[burble] — Telecom control plane (Lean 4 core) @@ -231,9 +234,7 @@ All share: *Multiple proof systems for cross-validation, honest status reporting | `proofs/agda/` | Agda proofs: ~700 lines. Intensional type theory foundation. -| `proofs/isabelle/` | Isabelle/HOL proofs: ~650 lines. Higher-order logic approach. - -| `proofs/mizar/` | Mizar proofs: ~400 lines. Tarski-Grothendieck set theory. +| `archive/proofs/` | Isabelle/HOL and Mizar trees, archived unchecked on 2026-11-09, with a theorem-by-theorem successor map. | `proofs/z3/` | Z3 SMT proofs: ~150 lines. Automated first-order logic verification. diff --git a/Justfile b/Justfile index c801fac3..780b0980 100644 --- a/Justfile +++ b/Justfile @@ -11,7 +11,7 @@ default: @just --list # Build all proofs across all systems -build-all: build-coq build-lean4 build-agda build-isabelle build-mizar build-idris2 +build-all: build-coq build-lean4 build-agda build-idris2 @echo "✓ All proofs built" # Verify all proofs @@ -59,21 +59,11 @@ test-correspondence-model: build-model-oracle # Build Agda proofs build-agda: @echo "Building Agda proofs..." - cd proofs/agda && agda FilesystemModel.agda - cd proofs/agda && agda FileOperations.agda - @echo "✓ Agda proofs type-checked" - -# Build Isabelle proofs -build-isabelle: - @echo "Building Isabelle proofs..." - cd proofs/isabelle && isabelle build -D . - @echo "✓ Isabelle proofs verified" - -# Build Mizar proofs (requires Mizar setup) -build-mizar: - @echo "Building Mizar proofs..." - cd proofs/mizar && mizf filesystem_model.miz || echo "⚠ Mizar not configured" - cd proofs/mizar && mizf file_operations.miz || echo "⚠ Mizar not configured" + cd proofs/agda && agda --safe --without-K --cubical-compatible All.agda + @echo "✓ Agda proofs checked (estate invocation, all modules)" + +# Isabelle and Mizar were archived to archive/proofs/ on 2026-11-09 (owner +# ruling; see archive/proofs/README.adoc). They have no build recipe. # Requires Idris2 0.8.0. Install via: # nix-shell -p idris2 # recommended for reproducibility @@ -271,8 +261,8 @@ ci: clean build-all verify-all test-all stats: @echo "=== Valence Shell Statistics ===" @echo "" - @echo "Proof Code (Coq/Lean/Agda/Isabelle/Mizar):" - @find proofs -name "*.v" -o -name "*.lean" -o -name "*.agda" -o -name "*.thy" -o -name "*.miz" 2>/dev/null | xargs wc -l 2>/dev/null | tail -1 || echo " 0 total" + @echo "Proof Code (Agda/Rocq/Lean; Isabelle and Mizar archived):" + @find proofs -name "*.v" -o -name "*.lean" -o -name "*.agda" 2>/dev/null | xargs wc -l 2>/dev/null | tail -1 || echo " 0 total" @echo "" @echo "Zig FFI Code:" @find impl/zig -name "*.zig" 2>/dev/null | xargs wc -l 2>/dev/null | tail -1 || echo " 0 total" @@ -304,7 +294,7 @@ watch: echidna-verify: @if command -v echidna &> /dev/null; then \ echo "Running ECHIDNA multi-prover verification..."; \ - echidna verify --all --targets coq,lean4,agda,isabelle,mizar; \ + echidna verify --all --targets coq,lean4,agda; \ else \ echo "⚠ ECHIDNA not installed. Using built-in verification."; \ just verify-all; \ @@ -327,7 +317,7 @@ certify: "version": "${VERSION}", "generated": "${TIMESTAMP}", "prover": "valence-shell", - "proof_systems": ["coq", "lean4", "agda", "isabelle", "mizar", "z3"], + "proof_systems": ["coq", "lean4", "agda", "z3"], "verified_properties": [ { "theorem": "mkdir_rmdir_reversible", @@ -375,8 +365,6 @@ certify: - Coq (primary) - Lean 4 (cross-verification) - Agda (dependent types) - - Isabelle/HOL (classical logic) - - Mizar (mathematical proofs) - Z3 (SMT verification) ### Key Theorems Verified @@ -423,8 +411,6 @@ help: @echo " just build-coq - Build Coq proofs" @echo " just build-lean4 - Build Lean 4 proofs" @echo " just build-agda - Build Agda proofs" - @echo " just build-isabelle - Build Isabelle proofs" - @echo " just build-mizar - Build Mizar proofs" @echo " just build-idris2 - Build Idris2 proofs" @echo " just verify-idris2 - Build + hole-count Idris2 proofs" @echo "" diff --git a/REVIEW.adoc b/REVIEW.adoc index 3e670e2b..68335127 100644 --- a/REVIEW.adoc +++ b/REVIEW.adoc @@ -1,5 +1,10 @@ == Valence Shell - One-Day Sprint Review +NOTE: *Historical record (2025-11-22), not current status.* Its claims that the +theorems are "proven" in five systems were never CI-checked for Isabelle or Mizar; +both trees were archived unchecked on 2026-11-09. Current state: +`docs/audits/2026-11-09-proof-ground-truth.adoc`. + *Date*: 2025-11-22 *Type*: Autonomous polyglot verification development ''''' diff --git a/archive/proofs/README.adoc b/archive/proofs/README.adoc new file mode 100644 index 00000000..25f3f3a1 --- /dev/null +++ b/archive/proofs/README.adoc @@ -0,0 +1,173 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell += Archived proof trees: Isabelle/HOL and Mizar +:toc: preamble + +These trees moved here from `proofs/isabelle/` and `proofs/mizar/` on 2026-11-09, +by owner ruling (see `docs/audits/2026-11-09-proof-ground-truth.adoc`). They are +kept, never deleted. + +*Why.* Under the estate proof policy (`hyperpolymath/standards` +`3-practice/PROOF-POLICY.adoc`) Agda is the theory source, rechecked in Rocq and +Lean. Isabelle is supplementary evidence only (§3) and Mizar is a §4 exception. +Neither could be run in the 2026-11-09 audit (Isabelle's distribution server was +unavailable; Mizar's installer was not permitted in the session), and neither had +a CI lane. They are *unchecked*: nothing below says these files were ever accepted +by their checker. + +*What still uses them.* Nothing. The Justfiles, `scripts/verify-proofs.sh` and +`scripts/validate-with-echidna.sh` were updated in the same change. + +== Successor map + +Each row names the archived theorem and the theorem that carries the same claim +today. Matching is *by name* (case, `_` and `-` ignored; Mizar's `Th_` prefix +dropped), so a match says where to look, not that the two statements were +compared. Statement comparison is the §2.2 reconciliation work and is open. The +Agda column is the source of truth; `lean:` and `rocq:` are recheck legs. + +[cols="1,2,3,5",options="header"] +|=== +|Prover |File |Archived theorem |Successor +|isabelle |`CopyMoveOperations.thy` |`copy_file_creates_destination` |agda:copyFile-creates-destination lean:copyFile_creates_destination rocq:copy_file_creates_destination +|isabelle |`CopyMoveOperations.thy` |`copy_file_preserves_source` |agda:copyFile-preserves-source lean:copyFile_preserves_source rocq:copy_file_preserves_source +|isabelle |`CopyMoveOperations.thy` |`copy_file_same_content` |agda:copyFile-same-content lean:copyFile_same_content rocq:copy_file_same_content +|isabelle |`CopyMoveOperations.thy` |`copy_file_reversible` |agda:copyFile-reversible lean:copyFile_reversible rocq:copy_file_reversible +|isabelle |`CopyMoveOperations.thy` |`move_creates_destination` |lean:move_creates_destination rocq:move_creates_destination +|isabelle |`CopyMoveOperations.thy` |`move_removes_source` |lean:move_removes_source rocq:move_removes_source +|isabelle |`CopyMoveOperations.thy` |`move_preserves_content` |lean:move_preserves_content rocq:move_preserves_content +|isabelle |`CopyMoveOperations.thy` |`move_reversible` |lean:move_reversible rocq:move_reversible +|isabelle |`CopyMoveOperations.thy` |`copy_preserves_other_paths` |lean:copy_preserves_other_paths rocq:copy_preserves_other_paths +|isabelle |`CopyMoveOperations.thy` |`move_preserves_other_paths` |lean:move_preserves_other_paths rocq:move_preserves_other_paths +|isabelle |`CopyMoveOperations.thy` |`copy_then_move` |lean:copy_then_move rocq:copy_then_move +|isabelle |`FileContentOperations.thy` |`read_file_preserves_fs` |agda:readFilePreservesFs lean:readFilePreservesFs rocq:read_file_preserves_fs +|isabelle |`FileContentOperations.thy` |`write_file_reversible` |agda:writeFileReversible lean:writeFileReversible rocq:write_file_reversible +|isabelle |`FileContentOperations.thy` |`write_file_independence` |agda:writeFileIndependence lean:writeFileIndependence rocq:write_file_independence +|isabelle |`FileContentOperations.thy` |`write_file_last_write_wins` |agda:writeFileLastWriteWins lean:writeFileLastWriteWins rocq:write_file_last_write_wins +|isabelle |`FileContentOperations.thy` |`write_file_commute` |agda:writeFileCommute lean:writeFileCommute rocq:write_file_commute +|isabelle |`FileContentOperations.thy` |`create_file_empty_content` |lean:createFileEmptyContent rocq:create_file_empty_content +|isabelle |`FileContentOperations.thy` |`capture_restore_identity` |agda:captureRestoreIdentity lean:captureRestoreIdentity rocq:capture_restore_identity +|isabelle |`FileContentOperations.thy` |`modification_reversible` |agda:modificationReversible lean:modificationReversible rocq:modification_reversible +|isabelle |`FileOperations.thy` |`create_file_creates_file` |agda:createFile-creates-file lean:createFile_creates_file rocq:create_file_creates_file +|isabelle |`FileOperations.thy` |`create_file_path_exists` |agda:createFile-path-exists lean:createFile_path_exists rocq:create_file_path_exists +|isabelle |`FileOperations.thy` |`delete_file_removes_path` |agda:deleteFile-removes-path lean:deleteFile_removes_path rocq:delete_file_removes_path +|isabelle |`FileOperations.thy` |`create_file_delete_file_reversible` |agda:createFile-deleteFile-reversible lean:createFile_deleteFile_reversible +|isabelle |`FileOperations.thy` |`create_file_preserves_other_paths` |agda:createFile-preserves-other-paths lean:createFile_preserves_other_paths rocq:create_file_preserves_other_paths +|isabelle |`FileOperations.thy` |`create_file_preserves_directories` |lean:createFile_preserves_directories rocq:create_file_preserves_directories +|isabelle |`FileOperations.thy` |`mkdir_preserves_files` |lean:mkdir_preserves_files rocq:mkdir_preserves_files +|isabelle |`FileOperations.thy` |`rmdir_mkdir_reversible` |agda:rmdir-mkdir-reversible lean:rmdir_mkdir_reversible +|isabelle |`FileOperations.thy` |`delete_file_create_file_reversible` |agda:deleteFile-createFile-reversible lean:deleteFile_createFile_reversible +|isabelle |`FileOperations.thy` |`file_isolation` |agda:file-isolation lean:file_isolation rocq:file_isolation +|isabelle |`FilesystemComposition.thy` |`apply_sequence_append` |agda:applySequence-append lean:applySequence_append +|isabelle |`FilesystemComposition.thy` |`single_mkdir_reversible` |lean:singleMkdirReversible rocq:single_mkdir_reversible +|isabelle |`FilesystemComposition.thy` |`single_create_file_reversible` |lean:singleCreateFileReversible rocq:single_create_file_reversible +|isabelle |`FilesystemComposition.thy` |`operation_sequence_reversible` |agda:operationSequenceReversible lean:operationSequenceReversible rocq:operation_sequence_reversible +|isabelle |`FilesystemEquivalence.thy` |`fs_equiv_refl` |agda:fsEquivRefl lean:fsEquivRefl rocq:fs_equiv_refl +|isabelle |`FilesystemEquivalence.thy` |`fs_equiv_sym` |agda:fsEquivSym lean:fsEquivSym rocq:fs_equiv_sym +|isabelle |`FilesystemEquivalence.thy` |`fs_equiv_trans` |agda:fsEquivTrans lean:fsEquivTrans rocq:fs_equiv_trans +|isabelle |`FilesystemEquivalence.thy` |`fs_equiv_is_equivalence` |agda:fsEquivIsEquivalence lean:fsEquivIsEquivalence rocq:fs_equiv_is_equivalence +|isabelle |`FilesystemEquivalence.thy` |`mkdir_preserves_equiv` |agda:mkdirPreservesEquiv lean:mkdirPreservesEquiv rocq:mkdir_preserves_equiv +|isabelle |`FilesystemEquivalence.thy` |`rmdir_preserves_equiv` |agda:rmdirPreservesEquiv lean:rmdirPreservesEquiv rocq:rmdir_preserves_equiv +|isabelle |`FilesystemEquivalence.thy` |`create_file_preserves_equiv` |agda:createFilePreservesEquiv lean:createFilePreservesEquiv rocq:create_file_preserves_equiv +|isabelle |`FilesystemEquivalence.thy` |`delete_file_preserves_equiv` |agda:deleteFilePreservesEquiv lean:deleteFilePreservesEquiv rocq:delete_file_preserves_equiv +|isabelle |`FilesystemEquivalence.thy` |`apply_op_preserves_equiv` |agda:applyOpPreservesEquiv lean:applyOpPreservesEquiv rocq:apply_op_preserves_equiv +|isabelle |`FilesystemEquivalence.thy` |`equiv_substitution` |agda:equivSubstitution lean:equivSubstitution rocq:equiv_substitution +|isabelle |`FilesystemEquivalence.thy` |`reversible_creates_equiv` |agda:reversibleCreatesEquiv lean:reversibleCreatesEquiv rocq:reversible_creates_equiv +|isabelle |`FilesystemEquivalence.thy` |`sequence_reversible_equiv` |agda:sequenceReversibleEquiv lean:sequenceReversibleEquiv rocq:sequence_reversible_equiv +|isabelle |`FilesystemEquivalence.thy` |`cno_identity_element` |agda:cnoIdentityElement lean:cnoIdentityElement rocq:cno_identity_element +|isabelle |`FilesystemEquivalence.thy` |`sequence_cno_identity` |agda:sequenceCnoIdentity lean:sequenceCnoIdentity rocq:sequence_cno_identity +|isabelle |`FilesystemEquivalence.thy` |`equiv_cong_apply_op` |agda:equivCongApplyOp lean:equivCongApplyOp rocq:equiv_cong_apply_op +|isabelle |`FilesystemEquivalence.thy` |`ops_equiv_refl` |agda:opsEquivRefl lean:opsEquivRefl rocq:ops_equiv_refl +|isabelle |`FilesystemEquivalence.thy` |`ops_equiv_sym` |agda:opsEquivSym lean:opsEquivSym rocq:ops_equiv_sym +|isabelle |`FilesystemModel.thy` |`path_exists_empty_fs_root` |agda:pathExists-emptyFS-root lean:pathExists_emptyFS_root rocq:path_exists_empty_fs_root +|isabelle |`FilesystemModel.thy` |`not_path_exists_empty_fs` |lean:not_pathExists_emptyFS rocq:not_path_exists_empty_fs +|isabelle |`FilesystemModel.thy` |`mkdir_creates_directory` |agda:mkdir-creates-directory lean:mkdir_creates_directory rocq:mkdir_creates_directory +|isabelle |`FilesystemModel.thy` |`mkdir_path_exists` |agda:mkdir-path-exists lean:mkdir_path_exists rocq:mkdir_path_exists +|isabelle |`FilesystemModel.thy` |`rmdir_removes_path` |agda:rmdir-removes-path lean:rmdir_removes_path rocq:rmdir_removes_path +|isabelle |`FilesystemModel.thy` |`mkdir_rmdir_reversible` |agda:mkdir-rmdir-reversible lean:mkdir_rmdir_reversible rocq:mkdir_rmdir_reversible +|isabelle |`FilesystemModel.thy` |`mkdir_preserves_other_paths` |agda:mkdir-preserves-other-paths lean:mkdir_preserves_other_paths rocq:mkdir_preserves_other_paths +|isabelle |`FilesystemModel.thy` |`rmdir_preserves_other_paths` |agda:rmdir-preserves-other-paths lean:rmdir_preserves_other_paths rocq:rmdir_preserves_other_paths +|isabelle |`FilesystemModel.thy` |`mkdir_parent_still_exists` |lean:mkdir_parent_still_exists rocq:mkdir_parent_still_exists +|isabelle |`PermissionOperations.thy` |`chmod_reversible` |agda:chmod-reversible lean:chmod_reversible rocq:chmod_reversible +|isabelle |`PermissionOperations.thy` |`chmod_same_mode` |agda:chmod-same-mode lean:chmod_same_mode rocq:chmod_same_mode +|isabelle |`PermissionOperations.thy` |`chmod_commute` |lean:chmod_commute rocq:chmod_commute +|isabelle |`PermissionOperations.thy` |`chmod_preserves_other` |agda:chmod-preserves-other lean:chmod_preserves_other rocq:chmod_preserves_other +|isabelle |`PermissionOperations.thy` |`chown_reversible` |agda:chown-reversible lean:chown_reversible rocq:chown_reversible +|isabelle |`PermissionOperations.thy` |`chown_same_owner` |agda:chown-same-owner lean:chown_same_owner rocq:chown_same_owner +|isabelle |`PermissionOperations.thy` |`chmod_chown_commute` |lean:chmod_chown_commute rocq:chmod_chown_commute +|isabelle |`PermissionOperations.thy` |`chown_preserves_other` |agda:chown-preserves-other lean:chown_preserves_other rocq:chown_preserves_other +|isabelle |`RMO_Operations.thy` |`obliterate_removes_path` |agda:obliterate-removes-path lean:obliterate_removes_path rocq:obliterate_removes_path +|isabelle |`RMO_Operations.thy` |`obliterate_removes_mapping` |agda:obliterate-removes-mapping lean:obliterate_removes_mapping rocq:obliterate_removes_mapping +|isabelle |`RMO_Operations.thy` |`obliterate_not_injective` |lean:obliterate_not_injective rocq:obliterate_not_injective +|isabelle |`RMO_Operations.thy` |`obliterate_preserves_other_paths` |agda:obliterate-preserves-other-paths lean:obliterate_preserves_other_paths rocq:obliterate_preserves_other_paths +|isabelle |`RMO_Operations.thy` |`obliterate_preserves_other_mappings` |rocq:obliterate_preserves_other_mappings +|isabelle |`RMO_Operations.thy` |`obliterate_leaves_no_trace` |lean:obliterate_leaves_no_trace rocq:obliterate_leaves_no_trace +|isabelle |`SymlinkOperations.thy` |`symlink_creates_path` |agda:symlink-creates-path lean:symlink_creates_path rocq:symlink_creates_path +|isabelle |`SymlinkOperations.thy` |`unlink_removes_path` |agda:unlink-removes-path lean:unlink_removes_path rocq:unlink_removes_path +|isabelle |`SymlinkOperations.thy` |`symlink_unlink_reversible` |agda:symlink-unlink-reversible lean:symlink_unlink_reversible rocq:symlink_unlink_reversible +|mizar |`copy_move_operations.miz` |`Th_copy_creates_destination` |agda:copyFile-creates-destination (name differs: copy/copyFile) +|mizar |`copy_move_operations.miz` |`Th_copy_preserves_source` |agda:copyFile-preserves-source (name differs) +|mizar |`copy_move_operations.miz` |`Th_copy_same_content` |agda:copyFile-same-content (name differs) +|mizar |`copy_move_operations.miz` |`Th_copy_reversible` |agda:copyFile-reversible (name differs) +|mizar |`copy_move_operations.miz` |`Th_move_creates_destination` |lean:move_creates_destination rocq:move_creates_destination +|mizar |`copy_move_operations.miz` |`Th_move_removes_source` |lean:move_removes_source rocq:move_removes_source +|mizar |`copy_move_operations.miz` |`Th_move_preserves_content` |lean:move_preserves_content rocq:move_preserves_content +|mizar |`copy_move_operations.miz` |`Th_move_reversible` |lean:move_reversible rocq:move_reversible +|mizar |`copy_move_operations.miz` |`Th_copy_preserves_other_paths` |lean:copy_preserves_other_paths rocq:copy_preserves_other_paths +|mizar |`copy_move_operations.miz` |`Th_move_preserves_other_paths` |lean:move_preserves_other_paths rocq:move_preserves_other_paths +|mizar |`copy_move_operations.miz` |`Th_copy_then_move` |lean:copy_then_move rocq:copy_then_move +|mizar |`file_content_operations.miz` |`Th_read_file_preserves_fs` |agda:readFilePreservesFs lean:readFilePreservesFs rocq:read_file_preserves_fs +|mizar |`file_content_operations.miz` |`Th_write_file_reversible` |agda:writeFileReversible lean:writeFileReversible rocq:write_file_reversible +|mizar |`file_content_operations.miz` |`Th_write_file_independence` |agda:writeFileIndependence lean:writeFileIndependence rocq:write_file_independence +|mizar |`file_content_operations.miz` |`Th_write_file_last_write_wins` |agda:writeFileLastWriteWins lean:writeFileLastWriteWins rocq:write_file_last_write_wins +|mizar |`file_content_operations.miz` |`Th_write_file_commute` |agda:writeFileCommute lean:writeFileCommute rocq:write_file_commute +|mizar |`file_content_operations.miz` |`Th_capture_restore_identity` |agda:captureRestoreIdentity lean:captureRestoreIdentity rocq:capture_restore_identity +|mizar |`file_content_operations.miz` |`Th_modification_reversible` |agda:modificationReversible lean:modificationReversible rocq:modification_reversible +|mizar |`file_operations.miz` |`CreateFileCreatesFile` |agda:createFile-creates-file lean:createFile_creates_file rocq:create_file_creates_file +|mizar |`file_operations.miz` |`CreateFilePathExists` |agda:createFile-path-exists lean:createFile_path_exists rocq:create_file_path_exists +|mizar |`file_operations.miz` |`DeleteFileRemovesPath` |agda:deleteFile-removes-path lean:deleteFile_removes_path rocq:delete_file_removes_path +|mizar |`file_operations.miz` |`CreateFileDeleteFileReversible` |agda:createFile-deleteFile-reversible lean:createFile_deleteFile_reversible +|mizar |`file_operations.miz` |`FileIsolation` |agda:file-isolation lean:file_isolation rocq:file_isolation +|mizar |`filesystem_composition.miz` |`SingleOpReversible` |agda:singleOpReversible lean:singleOpReversible rocq:single_op_reversible +|mizar |`filesystem_composition.miz` |`OperationSequenceReversible` |agda:operationSequenceReversible lean:operationSequenceReversible rocq:operation_sequence_reversible +|mizar |`filesystem_composition.miz` |`ReversibleCreatesCNO` |lean:reversibleCreatesCNO rocq:reversible_creates_CNO +|mizar |`filesystem_equivalence.miz` |`FsEquivRefl` |agda:fsEquivRefl lean:fsEquivRefl rocq:fs_equiv_refl +|mizar |`filesystem_equivalence.miz` |`FsEquivSym` |agda:fsEquivSym lean:fsEquivSym rocq:fs_equiv_sym +|mizar |`filesystem_equivalence.miz` |`FsEquivTrans` |agda:fsEquivTrans lean:fsEquivTrans rocq:fs_equiv_trans +|mizar |`filesystem_equivalence.miz` |`FsEquivIsEquivalence` |agda:fsEquivIsEquivalence lean:fsEquivIsEquivalence rocq:fs_equiv_is_equivalence +|mizar |`filesystem_equivalence.miz` |`MkdirPreservesEquiv` |agda:mkdirPreservesEquiv lean:mkdirPreservesEquiv rocq:mkdir_preserves_equiv +|mizar |`filesystem_equivalence.miz` |`RmdirPreservesEquiv` |agda:rmdirPreservesEquiv lean:rmdirPreservesEquiv rocq:rmdir_preserves_equiv +|mizar |`filesystem_equivalence.miz` |`CreateFilePreservesEquiv` |agda:createFilePreservesEquiv lean:createFilePreservesEquiv rocq:create_file_preserves_equiv +|mizar |`filesystem_equivalence.miz` |`DeleteFilePreservesEquiv` |agda:deleteFilePreservesEquiv lean:deleteFilePreservesEquiv rocq:delete_file_preserves_equiv +|mizar |`filesystem_equivalence.miz` |`ApplyOpPreservesEquiv` |agda:applyOpPreservesEquiv lean:applyOpPreservesEquiv rocq:apply_op_preserves_equiv +|mizar |`filesystem_equivalence.miz` |`EquivSubstitution` |agda:equivSubstitution lean:equivSubstitution rocq:equiv_substitution +|mizar |`filesystem_equivalence.miz` |`ReversibleCreatesEquiv` |agda:reversibleCreatesEquiv lean:reversibleCreatesEquiv rocq:reversible_creates_equiv +|mizar |`filesystem_equivalence.miz` |`CnoIdentityElement` |agda:cnoIdentityElement lean:cnoIdentityElement rocq:cno_identity_element +|mizar |`filesystem_equivalence.miz` |`EquivCongApplyOp` |agda:equivCongApplyOp lean:equivCongApplyOp rocq:equiv_cong_apply_op +|mizar |`filesystem_equivalence.miz` |`OpsEquivRefl` |agda:opsEquivRefl lean:opsEquivRefl rocq:ops_equiv_refl +|mizar |`filesystem_equivalence.miz` |`OpsEquivSym` |agda:opsEquivSym lean:opsEquivSym rocq:ops_equiv_sym +|mizar |`filesystem_model.miz` |`LemmaMembershipUnion` |none needed: Mizar set-theory encoding helper +|mizar |`filesystem_model.miz` |`LemmaMembershipSingleton` |none needed: Mizar set-theory encoding helper +|mizar |`filesystem_model.miz` |`LemmaNonMembershipSingleton` |none needed: Mizar set-theory encoding helper +|mizar |`filesystem_model.miz` |`LemmaSubsetSelf` |none needed: Mizar set-theory encoding helper +|mizar |`filesystem_model.miz` |`LemmaSubsetUnion` |none needed: Mizar set-theory encoding helper +|mizar |`filesystem_model.miz` |`LemmaSubsetDifference` |none needed: Mizar set-theory encoding helper +|mizar |`filesystem_model.miz` |`MAAReversibility` |related, not equivalent: agda:operationSequenceReversible +|mizar |`permission_operations.miz` |`Th_chmod_reversible` |agda:chmod-reversible lean:chmod_reversible rocq:chmod_reversible +|mizar |`permission_operations.miz` |`Th_chmod_same_mode` |agda:chmod-same-mode lean:chmod_same_mode rocq:chmod_same_mode +|mizar |`permission_operations.miz` |`Th_chmod_preserves_other` |agda:chmod-preserves-other lean:chmod_preserves_other rocq:chmod_preserves_other +|mizar |`permission_operations.miz` |`Th_chown_reversible` |agda:chown-reversible lean:chown_reversible rocq:chown_reversible +|mizar |`permission_operations.miz` |`Th_chown_same_owner` |agda:chown-same-owner lean:chown_same_owner rocq:chown_same_owner +|mizar |`permission_operations.miz` |`Th_chown_preserves_other` |agda:chown-preserves-other lean:chown_preserves_other rocq:chown_preserves_other +|mizar |`permission_operations.miz` |`Th_chmod_chown_commute` |lean:chmod_chown_commute rocq:chmod_chown_commute +|mizar |`rmo_operations.miz` |`Th_obliterate_removes_path` |agda:obliterate-removes-path lean:obliterate_removes_path rocq:obliterate_removes_path +|mizar |`rmo_operations.miz` |`Th_obliterate_removes_mapping` |agda:obliterate-removes-mapping lean:obliterate_removes_mapping rocq:obliterate_removes_mapping +|mizar |`rmo_operations.miz` |`Th_obliterate_not_reversible` |related, not equivalent: rocq:obliterate_not_injective; idris2 ObliterationProof +|mizar |`rmo_operations.miz` |`Th_obliterate_preserves_other_paths` |agda:obliterate-preserves-other-paths lean:obliterate_preserves_other_paths rocq:obliterate_preserves_other_paths +|mizar |`rmo_operations.miz` |`Th_obliterate_leaves_no_trace` |lean:obliterate_leaves_no_trace rocq:obliterate_leaves_no_trace +|mizar |`symlink_operations.miz` |`Th_symlink_creates_path` |agda:symlink-creates-path lean:symlink_creates_path rocq:symlink_creates_path +|mizar |`symlink_operations.miz` |`Th_unlink_removes_path` |agda:unlink-removes-path lean:unlink_removes_path rocq:unlink_removes_path +|mizar |`symlink_operations.miz` |`Th_symlink_unlink_reversible` |agda:symlink-unlink-reversible lean:symlink_unlink_reversible rocq:symlink_unlink_reversible +|=== + +Counts: 139 theorems; 103 name an Agda successor; 29 name only a Lean or Rocq successor; 2 are only related; 6 are Mizar encoding helpers with no counterpart needed. diff --git a/proofs/isabelle/CopyMoveOperations.thy b/archive/proofs/isabelle/CopyMoveOperations.thy similarity index 100% rename from proofs/isabelle/CopyMoveOperations.thy rename to archive/proofs/isabelle/CopyMoveOperations.thy diff --git a/proofs/isabelle/FileContentOperations.thy b/archive/proofs/isabelle/FileContentOperations.thy similarity index 100% rename from proofs/isabelle/FileContentOperations.thy rename to archive/proofs/isabelle/FileContentOperations.thy diff --git a/proofs/isabelle/FileOperations.thy b/archive/proofs/isabelle/FileOperations.thy similarity index 100% rename from proofs/isabelle/FileOperations.thy rename to archive/proofs/isabelle/FileOperations.thy diff --git a/proofs/isabelle/FilesystemComposition.thy b/archive/proofs/isabelle/FilesystemComposition.thy similarity index 100% rename from proofs/isabelle/FilesystemComposition.thy rename to archive/proofs/isabelle/FilesystemComposition.thy diff --git a/proofs/isabelle/FilesystemEquivalence.thy b/archive/proofs/isabelle/FilesystemEquivalence.thy similarity index 100% rename from proofs/isabelle/FilesystemEquivalence.thy rename to archive/proofs/isabelle/FilesystemEquivalence.thy diff --git a/proofs/isabelle/FilesystemModel.thy b/archive/proofs/isabelle/FilesystemModel.thy similarity index 100% rename from proofs/isabelle/FilesystemModel.thy rename to archive/proofs/isabelle/FilesystemModel.thy diff --git a/proofs/isabelle/PermissionOperations.thy b/archive/proofs/isabelle/PermissionOperations.thy similarity index 100% rename from proofs/isabelle/PermissionOperations.thy rename to archive/proofs/isabelle/PermissionOperations.thy diff --git a/proofs/isabelle/README.adoc b/archive/proofs/isabelle/README.adoc similarity index 100% rename from proofs/isabelle/README.adoc rename to archive/proofs/isabelle/README.adoc diff --git a/proofs/isabelle/RMO_Operations.thy b/archive/proofs/isabelle/RMO_Operations.thy similarity index 100% rename from proofs/isabelle/RMO_Operations.thy rename to archive/proofs/isabelle/RMO_Operations.thy diff --git a/proofs/isabelle/ROOT b/archive/proofs/isabelle/ROOT similarity index 100% rename from proofs/isabelle/ROOT rename to archive/proofs/isabelle/ROOT diff --git a/proofs/isabelle/SymlinkOperations.thy b/archive/proofs/isabelle/SymlinkOperations.thy similarity index 100% rename from proofs/isabelle/SymlinkOperations.thy rename to archive/proofs/isabelle/SymlinkOperations.thy diff --git a/proofs/mizar/.gitignore b/archive/proofs/mizar/.gitignore similarity index 100% rename from proofs/mizar/.gitignore rename to archive/proofs/mizar/.gitignore diff --git a/proofs/mizar/README.adoc b/archive/proofs/mizar/README.adoc similarity index 100% rename from proofs/mizar/README.adoc rename to archive/proofs/mizar/README.adoc diff --git a/proofs/mizar/copy_move_operations.miz b/archive/proofs/mizar/copy_move_operations.miz similarity index 100% rename from proofs/mizar/copy_move_operations.miz rename to archive/proofs/mizar/copy_move_operations.miz diff --git a/proofs/mizar/file_content_operations.miz b/archive/proofs/mizar/file_content_operations.miz similarity index 100% rename from proofs/mizar/file_content_operations.miz rename to archive/proofs/mizar/file_content_operations.miz diff --git a/proofs/mizar/file_operations.miz b/archive/proofs/mizar/file_operations.miz similarity index 100% rename from proofs/mizar/file_operations.miz rename to archive/proofs/mizar/file_operations.miz diff --git a/proofs/mizar/filesystem_composition.miz b/archive/proofs/mizar/filesystem_composition.miz similarity index 100% rename from proofs/mizar/filesystem_composition.miz rename to archive/proofs/mizar/filesystem_composition.miz diff --git a/proofs/mizar/filesystem_equivalence.miz b/archive/proofs/mizar/filesystem_equivalence.miz similarity index 100% rename from proofs/mizar/filesystem_equivalence.miz rename to archive/proofs/mizar/filesystem_equivalence.miz diff --git a/proofs/mizar/filesystem_model.miz b/archive/proofs/mizar/filesystem_model.miz similarity index 100% rename from proofs/mizar/filesystem_model.miz rename to archive/proofs/mizar/filesystem_model.miz diff --git a/proofs/mizar/permission_operations.miz b/archive/proofs/mizar/permission_operations.miz similarity index 100% rename from proofs/mizar/permission_operations.miz rename to archive/proofs/mizar/permission_operations.miz diff --git a/proofs/mizar/rmo_operations.miz b/archive/proofs/mizar/rmo_operations.miz similarity index 100% rename from proofs/mizar/rmo_operations.miz rename to archive/proofs/mizar/rmo_operations.miz diff --git a/proofs/mizar/symlink_operations.miz b/archive/proofs/mizar/symlink_operations.miz similarity index 100% rename from proofs/mizar/symlink_operations.miz rename to archive/proofs/mizar/symlink_operations.miz diff --git a/proofs/README.adoc b/proofs/README.adoc index c1df6fd4..42baff5e 100644 --- a/proofs/README.adoc +++ b/proofs/README.adoc @@ -1,5 +1,11 @@ == Valence Shell Formal Proofs +NOTE: *2026-11-09.* Agda (`agda/`) is the theory source of truth, checked under +`--safe --without-K --cubical-compatible`; Rocq (`coq/`) and Lean (`lean4/`) are +recheck legs. The Isabelle and Mizar trees were archived, unchecked, to +`../archive/proofs/` (with a successor map). Statements below about "5 proof +assistants" predate that. Current state: `../docs/audits/2026-11-09-proof-ground-truth.adoc`. + This directory contains formal proofs of filesystem operations across *5 different proof assistants*, establishing the MAA (Mutually Assured Accountability) framework with polyglot verification. @@ -139,23 +145,9 @@ agda FilesystemModel.agda # Produces: FilesystemModel.agdai ---- -==== Isabelle/HOL - -[source,bash] ----- -cd proofs/isabelle -isabelle build -D . -# Or: isabelle jedit FilesystemModel.thy ----- +==== Isabelle/HOL and Mizar -==== Mizar - -[source,bash] ----- -cd proofs/mizar -mizf filesystem_model.miz -# Produces verification output ----- +Archived on 2026-11-09; see `../archive/proofs/README.adoc`. === What This Enables diff --git a/proofs/z3/README.adoc b/proofs/z3/README.adoc index fa8c43a4..b54d4757 100644 --- a/proofs/z3/README.adoc +++ b/proofs/z3/README.adoc @@ -4,7 +4,7 @@ Z3 (SMT-LIB v2 scripts) provides automated verification for the filesystem operation invariants. Unlike the interactive proof systems -(Lean 4 / Coq / Agda / Isabelle) and the structural foundation (Mizar), +(Agda, the theory source, and the Lean 4 / Rocq recheck legs), Z3 discharges decidable fragments via SAT-modulo-theories solving. == Files diff --git a/proofs/z3/copy_move_operations.smt2 b/proofs/z3/copy_move_operations.smt2 index 1d275347..2700c218 100644 --- a/proofs/z3/copy_move_operations.smt2 +++ b/proofs/z3/copy_move_operations.smt2 @@ -1,4 +1,12 @@ ; SPDX-License-Identifier: MPL-2.0 +; +; PROOF-POLICY §4 exception note (2026-11-09). Tool: Z3. The operations here +; are uninterpreted functions characterised by *asserted* axioms, so an `unsat` +; result shows the theorem follows from those axioms, not that the axioms match +; the Agda model (the theory source, proofs/agda) or the Rust code. Status under +; §5: ASSUMED. The definitional array encoding used in filesystem_operations.smt2 +; and symlink_operations.smt2 is the pattern to port this file to. +; ; Valence Shell - Copy and Move Operations in Z3/SMT-LIB ; ; This module formalizes copy and move (rename) operations diff --git a/proofs/z3/filesystem_operations.smt2 b/proofs/z3/filesystem_operations.smt2 index 5d87172b..57f31546 100644 --- a/proofs/z3/filesystem_operations.smt2 +++ b/proofs/z3/filesystem_operations.smt2 @@ -1,164 +1,141 @@ -; Valence Shell - Z3 SMT Encoding -; Filesystem operations with reversibility properties +; SPDX-License-Identifier: MPL-2.0 +; Valence Shell - Z3 SMT encoding of the core filesystem operations ; -; This encoding allows automated verification of theorems using Z3 SMT solver +; PROOF-POLICY §4 exception note. Obligation: the mkdir/rmdir and +; createFile/deleteFile reversibility, postcondition, independence and +; composition properties, on a finite-map model. Tool: Z3 (SMT, theory of +; arrays + datatypes). Why: these are quantifier-free array identities that an +; SMT solver decides automatically; the theory source of truth is the Agda tree +; (proofs/agda), and this file is a supplementary automated check. Status under +; §5: ASSUMED, because a direct SMT run without a proof certificate is not a +; kernel-checked witness. +; +; Encoding (rewritten 2026-11-09). The previous version declared the operations +; as uninterpreted functions and *asserted* each theorem as an axiom before +; "checking" it, which was circular. Here every operation is *defined*: a +; filesystem is an array from paths to entries, and each operation is a +; `store`. Each theorem query asserts the hypotheses and the *negation* of the +; goal; `unsat` means no counterexample exists in the theory of arrays. Nothing +; about the operations is assumed. +; +; Abstraction: entries carry the node type only (no permissions, no content). +; The Agda model carries permissions; reversibility of rmdir/deleteFile there +; needs the original node to have default permissions, which this encoding +; makes trivially true by omitting them. +; +; Expected result sequence (scripts/verify-z3.sh): +; sat, sat, unsat x 9 +; The two `sat` results are non-vacuity checks: the mkdir and rmdir +; preconditions are satisfiable, so the theorems below are not vacuous. (set-logic ALL) -(set-option :produce-models true) - -; ===== Sorts ===== (declare-sort Path 0) -(declare-sort Filesystem 0) -(declare-sort FSNode 0) - -; ===== Filesystem Operations ===== - -(declare-fun mkdir (Path Filesystem) Filesystem) -(declare-fun rmdir (Path Filesystem) Filesystem) -(declare-fun create-file (Path Filesystem) Filesystem) -(declare-fun delete-file (Path Filesystem) Filesystem) - -; ===== Preconditions ===== - -(declare-fun path-exists (Path Filesystem) Bool) -(declare-fun parent-path (Path) Path) -(declare-fun parent-exists (Path Filesystem) Bool) -(declare-fun is-directory (Path Filesystem) Bool) -(declare-fun is-file (Path Filesystem) Bool) -(declare-fun is-empty-dir (Path Filesystem) Bool) -(declare-fun has-write-permission (Path Filesystem) Bool) - -(declare-fun mkdir-precondition (Path Filesystem) Bool) -(declare-fun rmdir-precondition (Path Filesystem) Bool) -(declare-fun create-file-precondition (Path Filesystem) Bool) -(declare-fun delete-file-precondition (Path Filesystem) Bool) - -; Define preconditions -(assert (forall ((p Path) (fs Filesystem)) - (= (mkdir-precondition p fs) - (and (not (path-exists p fs)) - (parent-exists p fs) - (is-directory (parent-path p) fs) - (has-write-permission (parent-path p) fs))))) - -(assert (forall ((p Path) (fs Filesystem)) - (= (rmdir-precondition p fs) - (and (is-directory p fs) - (is-empty-dir p fs) - (has-write-permission (parent-path p) fs))))) - -(assert (forall ((p Path) (fs Filesystem)) - (= (create-file-precondition p fs) - (and (not (path-exists p fs)) - (parent-exists p fs) - (has-write-permission (parent-path p) fs))))) - -(assert (forall ((p Path) (fs Filesystem)) - (= (delete-file-precondition p fs) - (and (is-file p fs) - (has-write-permission (parent-path p) fs))))) - -; ===== Main Reversibility Theorems ===== - -; Theorem: mkdir/rmdir reversibility -(assert (forall ((p Path) (fs Filesystem)) - (=> (mkdir-precondition p fs) - (= (rmdir p (mkdir p fs)) fs)))) - -; Theorem: create-file/delete-file reversibility -(assert (forall ((p Path) (fs Filesystem)) - (=> (create-file-precondition p fs) - (= (delete-file p (create-file p fs)) fs)))) - -; ===== Postcondition Properties ===== - -; mkdir creates directory -(assert (forall ((p Path) (fs Filesystem)) - (=> (mkdir-precondition p fs) - (is-directory p (mkdir p fs))))) - -; rmdir removes path -(assert (forall ((p Path) (fs Filesystem)) - (=> (rmdir-precondition p fs) - (not (path-exists p (rmdir p fs)))))) - -; create-file creates file -(assert (forall ((p Path) (fs Filesystem)) - (=> (create-file-precondition p fs) - (is-file p (create-file p fs))))) - -; delete-file removes path -(assert (forall ((p Path) (fs Filesystem)) - (=> (delete-file-precondition p fs) - (not (path-exists p (delete-file p fs)))))) - -; ===== Independence Properties ===== - -; Operations on different paths don't interfere -(declare-fun path-eq (Path Path) Bool) - -(assert (forall ((p1 Path) (p2 Path) (fs Filesystem)) - (=> (and (not (path-eq p1 p2)) - (mkdir-precondition p1 fs)) - (= (path-exists p2 fs) - (path-exists p2 (mkdir p1 fs)))))) - -(assert (forall ((p1 Path) (p2 Path) (fs Filesystem)) - (=> (and (not (path-eq p1 p2)) - (rmdir-precondition p1 fs)) - (= (path-exists p2 fs) - (path-exists p2 (rmdir p1 fs)))))) - -; ===== Composition Properties ===== - -; Two-operation reversibility -(assert (forall ((p1 Path) (p2 Path) (fs Filesystem)) - (=> (and (mkdir-precondition p1 fs) - (mkdir-precondition p2 (mkdir p1 fs))) - (= (rmdir p2 (rmdir p1 (mkdir p2 (mkdir p1 fs)))) fs)))) - -; Three-operation reversibility -(assert (forall ((p1 Path) (p2 Path) (p3 Path) (fs Filesystem)) - (=> (and (mkdir-precondition p1 fs) - (mkdir-precondition p2 (mkdir p1 fs)) - (mkdir-precondition p3 (mkdir p2 (mkdir p1 fs)))) - (= (rmdir p3 (rmdir p2 (rmdir p1 - (mkdir p3 (mkdir p2 (mkdir p1 fs)))))) fs)))) - -; ===== CNO (Certified Null Operation) Properties ===== - -; Reversible operation followed by its reverse is identity -(assert (forall ((p Path) (fs Filesystem)) - (=> (mkdir-precondition p fs) - (= (rmdir p (mkdir p fs)) fs)))) - -(assert (forall ((p Path) (fs Filesystem)) - (=> (create-file-precondition p fs) - (= (delete-file p (create-file p fs)) fs)))) - -; ===== Queries and Checks ===== - -; Check satisfiability - should be SAT if theorems are consistent +(declare-datatype NodeType ((File) (Directory))) +(declare-datatype Entry ((Absent) (Present (kind NodeType)))) +(define-sort FS () (Array Path Entry)) + +; Parent of a path; uninterpreted, so every result holds for any parent function. +(declare-fun parent (Path) Path) +; `(child-of c p)`: c is a strict descendant of p; uninterpreted, but strict. +(declare-fun child-of (Path Path) Bool) +(assert (forall ((p Path)) (not (child-of p p)))) + +(define-fun exists-at ((p Path) (fs FS)) Bool (not (= (select fs p) Absent))) +(define-fun is-dir ((p Path) (fs FS)) Bool (= (select fs p) (Present Directory))) +(define-fun is-file ((p Path) (fs FS)) Bool (= (select fs p) (Present File))) + +(define-fun mkdir ((p Path) (fs FS)) FS (store fs p (Present Directory))) +(define-fun rmdir ((p Path) (fs FS)) FS (store fs p Absent)) +(define-fun create-file ((p Path) (fs FS)) FS (store fs p (Present File))) +(define-fun delete-file ((p Path) (fs FS)) FS (store fs p Absent)) + +(define-fun mkdir-pre ((p Path) (fs FS)) Bool + (and (not (exists-at p fs)) (is-dir (parent p) fs))) +(define-fun rmdir-pre ((p Path) (fs FS)) Bool + (and (is-dir p fs) + (forall ((c Path)) (=> (child-of c p) (not (exists-at c fs)))))) +(define-fun create-file-pre ((p Path) (fs FS)) Bool + (and (not (exists-at p fs)) (is-dir (parent p) fs))) +(define-fun delete-file-pre ((p Path) (fs FS)) Bool (is-file p fs)) + +(declare-const p Path) +(declare-const p1 Path) +(declare-const p2 Path) +(declare-const p3 Path) +(declare-const fs FS) + +; ===== Non-vacuity (expected: sat, sat) ===== + +(push) +(assert (mkdir-pre p fs)) +(check-sat) +(pop) + +(push) +(assert (rmdir-pre p fs)) +(check-sat) +(pop) + +; ===== Reversibility (expected: unsat x 4) ===== + +(push) +(assert (mkdir-pre p fs)) +(assert (not (= (rmdir p (mkdir p fs)) fs))) +(check-sat) +(pop) + +(push) +(assert (rmdir-pre p fs)) +(assert (not (= (mkdir p (rmdir p fs)) fs))) +(check-sat) +(pop) + +(push) +(assert (create-file-pre p fs)) +(assert (not (= (delete-file p (create-file p fs)) fs))) (check-sat) +(pop) + +(push) +(assert (delete-file-pre p fs)) +(assert (not (= (create-file p (delete-file p fs)) fs))) +(check-sat) +(pop) + +; ===== Postconditions (expected: unsat x 2) ===== -; Get a model (example filesystem state) -; (get-model) +(push) +(assert (not (is-dir p (mkdir p fs)))) +(check-sat) +(pop) -; Check specific instances (push) -(declare-const test-path Path) -(declare-const test-fs Filesystem) -(assert (mkdir-precondition test-path test-fs)) -(assert (not (= (rmdir test-path (mkdir test-path test-fs)) test-fs))) -(check-sat) ; Should be UNSAT - proves the theorem +(assert (exists-at p (rmdir p fs))) +(check-sat) (pop) -; Summary: -; This SMT encoding formalizes filesystem operations in first-order logic -; Z3 can automatically verify: -; ✓ Reversibility theorems -; ✓ Postcondition properties -; ✓ Independence of operations -; ✓ Composition correctness -; ✓ CNO identity properties +; ===== Independence (expected: unsat) ===== + +(push) +(assert (not (= p1 p2))) +(assert (not (= (select (mkdir p1 fs) p2) (select fs p2)))) +(check-sat) +(pop) + +; ===== Composition, undone in reverse order (expected: unsat x 2) ===== + +(push) +(assert (mkdir-pre p1 fs)) +(assert (mkdir-pre p2 (mkdir p1 fs))) +(assert (not (= (rmdir p1 (rmdir p2 (mkdir p2 (mkdir p1 fs)))) fs))) +(check-sat) +(pop) + +(push) +(assert (mkdir-pre p1 fs)) +(assert (mkdir-pre p2 (mkdir p1 fs))) +(assert (mkdir-pre p3 (mkdir p2 (mkdir p1 fs)))) +(assert (not (= (rmdir p1 (rmdir p2 (rmdir p3 (mkdir p3 (mkdir p2 (mkdir p1 fs)))))) fs))) +(check-sat) +(pop) diff --git a/proofs/z3/permission_operations.smt2 b/proofs/z3/permission_operations.smt2 index a5c17d76..0a53cca2 100644 --- a/proofs/z3/permission_operations.smt2 +++ b/proofs/z3/permission_operations.smt2 @@ -1,4 +1,12 @@ ; SPDX-License-Identifier: MPL-2.0 +; +; PROOF-POLICY §4 exception note (2026-11-09). Tool: Z3. The operations here +; are uninterpreted functions characterised by *asserted* axioms, so an `unsat` +; result shows the theorem follows from those axioms, not that the axioms match +; the Agda model (the theory source, proofs/agda) or the Rust code. Status under +; §5: ASSUMED. The definitional array encoding used in filesystem_operations.smt2 +; and symlink_operations.smt2 is the pattern to port this file to. +; ; Valence Shell - Permission Operations in Z3/SMT-LIB ; ; Formalizes chmod and chown as reversible operations. diff --git a/proofs/z3/rmo_operations.smt2 b/proofs/z3/rmo_operations.smt2 index 9fdd3a13..4a3482d3 100644 --- a/proofs/z3/rmo_operations.smt2 +++ b/proofs/z3/rmo_operations.smt2 @@ -1,4 +1,12 @@ ; SPDX-License-Identifier: MPL-2.0 +; +; PROOF-POLICY §4 exception note (2026-11-09). Tool: Z3. The operations here +; are uninterpreted functions characterised by *asserted* axioms, so an `unsat` +; result shows the theorem follows from those axioms, not that the axioms match +; the Agda model (the theory source, proofs/agda) or the Rust code. Status under +; §5: ASSUMED. The definitional array encoding used in filesystem_operations.smt2 +; and symlink_operations.smt2 is the pattern to port this file to. +; ; Valence Shell - RMO (Remove-Match-Obliterate) Operations in Z3/SMT-LIB ; ; This module formalizes the logical block-mapping model of secure deletion. diff --git a/proofs/z3/symlink_operations.smt2 b/proofs/z3/symlink_operations.smt2 index 05a14234..ead3762e 100644 --- a/proofs/z3/symlink_operations.smt2 +++ b/proofs/z3/symlink_operations.smt2 @@ -1,65 +1,73 @@ ; SPDX-License-Identifier: MPL-2.0 -; Valence Shell - Symlink Operations in Z3/SMT-LIB +; Valence Shell - Z3 SMT encoding of symlink creation and removal ; -; Abstract model of symbolic link creation and removal. -; A symlink is represented as a file node with default permissions; -; the target path is modeled externally. +; PROOF-POLICY §4 exception note. Obligation: symlink/unlink reversibility and +; postconditions on a finite-map model. Tool: Z3 (theory of arrays + +; datatypes). Why: quantifier-free array identities an SMT solver decides +; automatically; the theory source of truth is proofs/agda/SymlinkOperations.agda. +; Status under §5: ASSUMED (no proof certificate). +; +; Rewritten 2026-11-09. The previous version had one `(check-sat)` that +; returned `sat` and never negated a goal, so it proved nothing; it also +; asserted `symlink p fs = fs-update p node fs` for *every* node, forcing all +; updates at a path to coincide. Here symlink and unlink are defined as +; `store`s, and each theorem query asserts the negated goal. +; +; As in the Agda model, a symlink is a file-typed node; the target is not +; modelled. +; +; Expected result sequence (scripts/verify-z3.sh): sat, unsat x 4 (set-logic ALL) -(set-option :produce-models true) - -; ===== Sorts ===== (declare-sort Path 0) -(declare-sort Filesystem 0) -(declare-sort FSNode 0) - -; ===== Core Predicates/Functions ===== - -(declare-fun path-exists (Path Filesystem) Bool) -(declare-fun parent-path (Path) Path) -(declare-fun parent-exists (Path Filesystem) Bool) -(declare-fun is-directory (Path Filesystem) Bool) -(declare-fun has-write-permission (Path Filesystem) Bool) -(declare-fun fs-update (Path FSNode Filesystem) Filesystem) -(declare-fun fs-delete (Path Filesystem) Filesystem) -(declare-fun fs-get (Filesystem Path) FSNode) +(declare-datatype NodeType ((File) (Directory))) +(declare-datatype Entry ((Absent) (Present (kind NodeType)))) +(define-sort FS () (Array Path Entry)) -; ===== Symlink Operations ===== +(declare-fun parent (Path) Path) -(declare-fun symlink-precondition (Path Filesystem) Bool) -(declare-fun symlink (Path Filesystem) Filesystem) -(declare-fun unlink (Path Filesystem) Filesystem) +(define-fun exists-at ((p Path) (fs FS)) Bool (not (= (select fs p) Absent))) +(define-fun is-dir ((p Path) (fs FS)) Bool (= (select fs p) (Present Directory))) -(assert (forall ((p Path) (fs Filesystem)) - (= (symlink-precondition p fs) - (and (not (path-exists p fs)) - (parent-exists p fs) - (is-directory (parent-path p) fs) - (has-write-permission (parent-path p) fs))))) +(define-fun symlink ((p Path) (fs FS)) FS (store fs p (Present File))) +(define-fun unlink ((p Path) (fs FS)) FS (store fs p Absent)) -; symlink modeled as fs-update with a fresh node -(assert (forall ((p Path) (node FSNode) (fs Filesystem)) - (= (symlink p fs) (fs-update p node fs)))) +(define-fun symlink-pre ((p Path) (fs FS)) Bool + (and (not (exists-at p fs)) (is-dir (parent p) fs))) -; unlink modeled as fs-delete -(assert (forall ((p Path) (fs Filesystem)) - (= (unlink p fs) (fs-delete p fs)))) +(declare-const p Path) +(declare-const q Path) +(declare-const fs FS) -; ===== Axioms ===== - -(assert (forall ((p Path) (node FSNode) (fs Filesystem)) - (path-exists p (fs-update p node fs)))) - -(assert (forall ((p Path) (fs Filesystem)) - (not (path-exists p (fs-delete p fs))))) +; Non-vacuity: the precondition is satisfiable (expected: sat) +(push) +(assert (symlink-pre p fs)) +(check-sat) +(pop) -; ===== Reversibility Theorem ===== +; symlink then unlink restores the filesystem (expected: unsat) +(push) +(assert (symlink-pre p fs)) +(assert (not (= (unlink p (symlink p fs)) fs))) +(check-sat) +(pop) -(assert (forall ((p Path) (fs Filesystem) (node FSNode)) - (=> (symlink-precondition p fs) - (= (unlink p (symlink p fs)) fs)))) +; symlink creates the path (expected: unsat) +(push) +(assert (not (exists-at p (symlink p fs)))) +(check-sat) +(pop) -; ===== Check ===== +; unlink removes the path (expected: unsat) +(push) +(assert (exists-at p (unlink p fs))) +(check-sat) +(pop) +; symlink leaves other paths alone (expected: unsat) +(push) +(assert (not (= p q))) +(assert (not (= (select (symlink p fs) q) (select fs q)))) (check-sat) +(pop) diff --git a/scripts/validate-with-echidna.sh b/scripts/validate-with-echidna.sh index 152757a2..204352bf 100755 --- a/scripts/validate-with-echidna.sh +++ b/scripts/validate-with-echidna.sh @@ -128,20 +128,8 @@ verify_file "Agda: FilesystemComposition" "proofs/agda/FilesystemComposition.a verify_file "Agda: FilesystemEquivalence" "proofs/agda/FilesystemEquivalence.agda" "agda" echo "" -# ─── Step 4: Verify Isabelle proofs ─── -echo "── Step 4: Isabelle/HOL Proofs ──" -verify_file "Isabelle: FilesystemModel" "proofs/isabelle/FilesystemModel.thy" "isabelle" -verify_file "Isabelle: FileOperations" "proofs/isabelle/FileOperations.thy" "isabelle" -verify_file "Isabelle: FilesystemComposition" "proofs/isabelle/FilesystemComposition.thy" "isabelle" -verify_file "Isabelle: FilesystemEquivalence" "proofs/isabelle/FilesystemEquivalence.thy" "isabelle" -echo "" - -# ─── Step 5: Verify Mizar proofs ─── -echo "── Step 5: Mizar Proofs ──" -verify_file "Mizar: filesystem_model" "proofs/mizar/filesystem_model.miz" "mizar" -verify_file "Mizar: file_operations" "proofs/mizar/file_operations.miz" "mizar" -verify_file "Mizar: filesystem_composition" "proofs/mizar/filesystem_composition.miz" "mizar" -echo "" +# Isabelle and Mizar were archived to archive/proofs/ on 2026-11-09 (owner +# ruling); they are not validated here. Steps 4 and 5 were removed. # ─── Step 6: Verify Z3 SMT proofs ─── echo "── Step 6: Z3 SMT Proofs ──" diff --git a/scripts/verify-proofs.sh b/scripts/verify-proofs.sh index 43ed6036..e80a06a9 100755 --- a/scripts/verify-proofs.sh +++ b/scripts/verify-proofs.sh @@ -144,10 +144,8 @@ echo "" # Agda Verification if check_command agda; then log_info "Agda detected" - run_test "Agda: FilesystemModel.agda" \ - "cd proofs/agda && agda FilesystemModel.agda" - run_test "Agda: FileOperations.agda" \ - "cd proofs/agda && agda FileOperations.agda" + run_test "Agda: All.agda (--safe --without-K --cubical-compatible)" \ + "cd proofs/agda && agda --safe --without-K --cubical-compatible All.agda" else log_skip "Agda not installed" ((TOTAL_TESTS += 2)) @@ -156,31 +154,8 @@ fi echo "" -# Isabelle Verification -if check_command isabelle; then - log_info "Isabelle/HOL detected" - run_test "Isabelle: FilesystemModel.thy" \ - "cd proofs/isabelle && isabelle build -D ." -else - log_skip "Isabelle not installed" - TOTAL_TESTS=$((TOTAL_TESTS + 1)) - SKIPPED_TESTS=$((SKIPPED_TESTS + 1)) -fi - -echo "" - -# Mizar Verification -if check_command mizf; then - log_info "Mizar detected" - run_test "Mizar: filesystem_model.miz" \ - "cd proofs/mizar && mizf filesystem_model.miz" - run_test "Mizar: file_operations.miz" \ - "cd proofs/mizar && mizf file_operations.miz" -else - log_skip "Mizar not installed (complex setup required)" - ((TOTAL_TESTS += 2)) - ((SKIPPED_TESTS += 2)) -fi +# Isabelle and Mizar were archived to archive/proofs/ on 2026-11-09 and are +# not verified here (see archive/proofs/README.adoc). echo "" diff --git a/scripts/verify-z3.sh b/scripts/verify-z3.sh index 49682c5d..70490b84 100755 --- a/scripts/verify-z3.sh +++ b/scripts/verify-z3.sh @@ -50,11 +50,11 @@ verify_file() { # These sequences are part of the checked proof contract. Consistency queries # intentionally return sat; theorem queries assert the negation and must be # unsat. Any unknown, missing result, extra result, or parse error fails. -verify_file proofs/z3/filesystem_operations.smt2 "sat,unsat" +verify_file proofs/z3/filesystem_operations.smt2 "sat,sat,unsat,unsat,unsat,unsat,unsat,unsat,unsat,unsat,unsat" verify_file proofs/z3/copy_move_operations.smt2 "unsat,unsat,unsat,unsat,unsat,unsat,unsat,unsat,unsat,unsat,unsat" verify_file proofs/z3/permission_operations.smt2 "unsat,unsat,unsat,unsat,unsat" verify_file proofs/z3/rmo_operations.smt2 "unsat,unsat,unsat,unsat" -verify_file proofs/z3/symlink_operations.smt2 "sat" +verify_file proofs/z3/symlink_operations.smt2 "sat,unsat,unsat,unsat,unsat" # Positive failure control: demonstrate that the result validator rejects a # satisfiable counterexample when a theorem query is expected to be unsat. From 97db7f9373e661ea600b86b2e2f34ff39b5bb9c7 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:47:06 +0000 Subject: [PATCH 05/10] docs(plan): record owner rulings OD-30 to OD-34 (proof-policy conformance) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - OD-30: Agda is the canonical theory spec; Rocq and Lean are recheck legs. The Lean FinFS keeps its role as the executable oracle. - OD-31: Rust is verified with Creusot, Pearlite and Verus on vsh-core. Aeneas becomes an optional, labelled side lane that never gates or grades anything (its Rust-to-model row is ASSUMED). - OD-32: funext removed by pointwise equality (done in this PR), plus a Dedukti transport experiment for mathesis and echidna. - OD-33: Isabelle and Mizar archived; Z3 kept with §4 notes (done here). - OD-34: G6 counts Proof Witness Grades from CI receipts. - Toolchains outside Guix carry §6 deviation records. The new section names every part of the plan each ruling supersedes. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDjNR1ZoYKEPxSKE2nq --- CLAUDE.md | 8 ++- .../audits/2026-11-09-proof-ground-truth.adoc | 11 ++-- docs/plans/VSH-ROUTE-PLAN-2026-11-04.adoc | 63 +++++++++++++++++++ 3 files changed, 75 insertions(+), 7 deletions(-) diff --git a/CLAUDE.md b/CLAUDE.md index d7c93c53..1c2ee68a 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -54,9 +54,11 @@ The Rust CLI is a functional interactive shell with these features: normative for this repository; this section is a short map for agents and changes in the same change as that file. Which verifier carries which obligation: -* *Rust code* → Creusot, on the code itself (no Creusot contracts exist in - `impl/rust-cli/` yet). Kani is the standing exception for `unsafe`/FFI seams; Aeneas - only where Rust implements a theorem proved in Agda. +* *Rust code* → Creusot with Pearlite contracts, and Verus (ruling 2026-11-07), on + the code itself; no contracts exist in `impl/rust-cli/` yet. Kani is the standing + exception for `unsafe`/FFI seams. Aeneas runs only as an optional, labelled side + lane (route plan OD-31): it never gates or grades anything, and its Rust-to-model + row is `ASSUMED`. * *Ada code* → SPARK (none in this repo). * *APIs, ABIs, wire formats, engineering properties* → Idris2 (`proofs/idris2/`). * *Theory* → Agda as the source of truth, rechecked in Rocq and Lean. Owner diff --git a/docs/audits/2026-11-09-proof-ground-truth.adoc b/docs/audits/2026-11-09-proof-ground-truth.adoc index e76a2b48..fdf499f1 100644 --- a/docs/audits/2026-11-09-proof-ground-truth.adoc +++ b/docs/audits/2026-11-09-proof-ground-truth.adoc @@ -204,8 +204,11 @@ change. == 5. Route plan against PROOF-POLICY The plan merged in #222 predates the 2026-11-07 Rust ruling. In places it also -departs from the 2026-10-26 theory mapping. Each gap below needs an owner ruling -before session 1 runs. +departs from the 2026-10-26 theory mapping. The owner ruled on every gap below on +2026-11-09 (route plan OD-30 to OD-34): G-1 Agda canonical; G-2 Creusot/Pearlite and +Verus, with Aeneas as an optional side lane; G-3 the canonical invocation, now met; +G-4 G6 by Proof Witness Grade; G-5 Isabelle and Mizar archived, Z3 kept with §4 +notes; G-6 deviation records. [cols="1,4,4",options="header"] |=== @@ -252,5 +255,5 @@ only. * `CLAUDE.md`: the same correction. * This record. -It does not change the route plan. The six gaps in section 5 wait for owner -rulings. +The owner rulings of 2026-11-09 are recorded in the route plan (OD-30 to OD-34), and +the follow-up commits on this PR carry them out (section 7). diff --git a/docs/plans/VSH-ROUTE-PLAN-2026-11-04.adoc b/docs/plans/VSH-ROUTE-PLAN-2026-11-04.adoc index 96d4eff2..b39e1eea 100644 --- a/docs/plans/VSH-ROUTE-PLAN-2026-11-04.adoc +++ b/docs/plans/VSH-ROUTE-PLAN-2026-11-04.adoc @@ -23,6 +23,8 @@ Review findings at that level of detail are recorded here as gate requirements a *Revision 2026-11-05:* this revision adds the symlink-escape failure (j) found in review. It also scopes G6, defines nested-root locking, makes the G5 write alphabet finite, and builds P5 on the Agda tree that #221 repaired. +*Revision 2026-11-09:* owner rulings OD-30 to OD-34 bring the plan into line with the estate proof policy (`hyperpolymath/standards` `3-practice/PROOF-POLICY.adoc`). Where they conflict with anything below, the 2026-11-09 rulings win. The section "Owner rulings (2026-11-09)" lists each superseded part. Ground truth for the same day: `docs/audits/2026-11-09-proof-ground-truth.adoc`. + *How the evidence was gathered:* * An ultracode workflow ran 50 agents, all of which completed: @@ -51,6 +53,67 @@ Review findings at that level of detail are recorded here as gate requirements a |— |Commit this plan and open a draft PR. Wait for the owner's go before running the implementation workflows. |This document. |=== +== Owner rulings (2026-11-09) + +These rulings follow a re-run of every prover leg against PROOF-POLICY (rulings +2026-10-26, 2026-11-04 and 2026-11-07). They supersede the parts of this plan named +in the right-hand column. + +[cols="1,4,5",options="header"] +|=== +|# |Ruling |Supersedes, and what changes + +|*OD-30* |*Agda is the canonical theory spec.* Rocq and Lean are recheck legs: Dedukti +transport first, hand re-proof as fallback, each leg recorded as "transported" or +"re-proved" (policy §1, §3). This is the elegant arm (E 9 / D 7). +|OD-0 and OD-1 ("one canonical spec in Lean", "Agda as second witness"). FinFS is +written in Agda first. The Lean FinFS keeps one engineering role: the executable model +oracle that the Rust differential tests drive. The existing Lean and Rocq theorems +are target-only evidence (§3) until each is compared with its Agda statement (§2.2). +P5 is done: the Agda tree checks under the canonical invocation (`b8e4c7f`). + +|*OD-31* |*Rust is verified with Creusot, Pearlite and Verus* on `vsh-core` (policy +§1.2). *Aeneas runs as an optional side lane*, labelled as such: it never gates a +session, never counts toward a grade or G6, and records two rows per §4.1, the model +theorem (`PROVEN`) and the Rust-to-model correspondence (`ASSUMED`; its Lean backend +needs Mathlib). +|OD-2, P6 and P9 (Aeneas as the refinement route), G9. G9 becomes "Creusot/Pearlite +and Verus contracts on `vsh-core` prove `step` and `inverse` meet the Agda-derived +specification for the declared op set". The Aeneas spike keeps its kill rule but moves +to the side lane. *Lightweight release, heavy development*: contracts are ghost code +erased at compile time, so the shipped binary should not grow. Session 1 tests that +claim by building `vsh-core` with and without contracts and comparing the artefacts; +until then it is a design intent, not a result. + +|*OD-32* |*Agda `funext` removed by pointwise equality* (elegant arm, E 9 / D 8), +plus a Dedukti transport experiment whose findings feed mathesis and echidna. +|P5 ("K-free refactor", "fallback: builtins-only mirror"). Done in this PR: no +postulates, `IsEmptyDir` completed, CI lane `.github/workflows/agda.yml`. The +Dedukti findings are recorded in `docs/audits/2026-11-09-proof-ground-truth.adoc`. + +|*OD-33* |*Archive Isabelle and Mizar now; keep Z3 with §4 notes and fix its broken +files* (E 8 / D 8). +|OD-1 and P10 ("archive only once G6 holds without them"). Done in this PR: +`archive/proofs/` with a 139-theorem successor map; all consumers updated. Coq +(Rocq) is *not* archived: it is a recheck leg under the policy, not an archival +candidate. + +|*OD-34* |*G6 counts Proof Witness Grades, not prover tallies.* A theory theorem +counts toward G6 at `PWG-2i` or better: the Agda proof checks under §2.1 and at +least one recheck leg is kernel-checked *and* `RECONCILED` (§2.2, §8). Grades are +derived from CI receipts, never asserted. Engineering statements (Idris2) and Rust +contracts are not graded; they count as their own rows. +|OD-22 and G6 ("≥2 independent CI-gated provers plus the oracle"; the #221 ledger +words). MANIFEST statuses use the policy §5 vocabulary (`PROVEN`, +`PROVEN-WITH-AXIOMS`, `TESTED`, `ASSUMED`, `OPEN`). Z3 rows are `ASSUMED` and never +count toward G6. + +|— |*Toolchains outside Guix carry a §6 deviation record* in `PROOF-NEEDS.adoc` and +in the installing workflow, naming the leg, tool, version, digest, reason and state. +|The session-1 provisioner (Phase 0). It installs the pinned versions *and* writes +the deviation records; a lane that installs a prover without one fails review. +|=== + *Why proof-first still fixes runtime holes first.* The proof-first architect's own thesis orders the work as "holes come first (rungs 0–1), wiring next (CI lanes before claims), features last". It also argues that the drift guard and the WAL are _proof-necessary_: they discharge, at runtime, the one hypothesis a refinement proof cannot cover, namely that the real OS state equals the abstract state. So the Rust hole fixes (Phase 1) are part of the spine, not a departure from it. They also touch disjoint files from the Lean work (Phase 2), so the two run in parallel and the proofs are not held up. ''''' From 38b947f42a64f202ae4c37c9f8ceed6e1c83856a Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:51:01 +0000 Subject: [PATCH 06/10] fix: address SonarCloud and review findings on the proof-ground-truth PR - agda.yml: pin curl redirects to HTTPS (--proto '=https' --tlsv1.2, SonarCloud S6506) and prefix globs with ./ (S6573). - Negative witnesses in Lean and Agda: RmdirPrecondition rejects a directory that has a child. Weakening isEmptyDir to True now breaks the Lean build (checked by mutation). - CLAUDE.md: scope the "0 real gaps" metric to escape hatches and point at the audit for open proof work. - PROOF-NEEDS.adoc: is_empty_dir_dec depends on both Classical_Prop.classic and ClassicalEpsilon.constructive_indefinite_description. - Audit: record filesystem well-formedness (parent of an existing path is a directory) as an invariant for the Agda FinFS spec rather than a Lean-only rmdir precondition. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDjNR1ZoYKEPxSKE2nq --- .github/workflows/agda.yml | 8 ++++---- CLAUDE.md | 2 +- PROOF-NEEDS.adoc | 2 +- docs/audits/2026-11-09-proof-ground-truth.adoc | 7 +++++++ proofs/agda/PreconditionWitnesses.agda | 10 ++++++++++ proofs/lean4/PreconditionWitnesses.lean | 9 +++++++++ 6 files changed, 32 insertions(+), 6 deletions(-) diff --git a/.github/workflows/agda.yml b/.github/workflows/agda.yml index 6a7e9198..7cbbcfbb 100644 --- a/.github/workflows/agda.yml +++ b/.github/workflows/agda.yml @@ -46,7 +46,7 @@ jobs: - name: Install Agda (pinned release, digest-checked) run: | set -euo pipefail - curl -sSfL -o agda.tar.xz \ + curl --proto '=https' --tlsv1.2 -sSfL -o agda.tar.xz \ "https://github.com/agda/agda/releases/download/v${AGDA_VERSION}/Agda-v${AGDA_VERSION}-linux.tar.xz" echo "${AGDA_SHA256} agda.tar.xz" | sha256sum -c - mkdir -p "$HOME/agda" @@ -79,7 +79,7 @@ jobs: working-directory: proofs/agda run: | set -euo pipefail - if grep -nE '^[[:space:]]*postulate|TERMINATING|NON_TERMINATING|NO_POSITIVITY_CHECK|NO_UNIVERSE_CHECK' *.agda; then + if grep -nE '^[[:space:]]*postulate|TERMINATING|NON_TERMINATING|NO_POSITIVITY_CHECK|NO_UNIVERSE_CHECK' ./*.agda; then echo "::error::postulate or escape pragma found"; exit 1 fi @@ -88,8 +88,8 @@ jobs: run: | set -euo pipefail missing=0 - for f in *.agda; do - m="${f%.agda}" + for f in ./*.agda; do + m="$(basename "$f" .agda)" [ "$m" = "All" ] && continue grep -qx "import ${m}" All.agda || { echo "::error::${m} is not imported by All.agda"; missing=1; } done diff --git a/CLAUDE.md b/CLAUDE.md index 1c2ee68a..0eeb44ba 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -112,7 +112,7 @@ Grade 2 or Grade 1 obligation. - 21,331 lines of Rust across 32 source files (`find impl/rust-cli/src -name '*.rs' | wc -l`; `wc -l` aggregate, measured 2026-06-01) - ~478 theorem candidates across 6 proof systems + Idris2 ABI layer (per issue #42 deep-audit inventory, 2026-06-01) -- 2 proof holes remaining, **0 real gaps**: 1 justified classical dependency (Coq `is_empty_dir_dec` — a `Theorem` proved with `Classical.classic` and `ClassicalEpsilon`, not a custom `Axiom`; corrected 2026-11-09), 0 Agda postulates (the structural `funext` was removed 2026-11-09: filesystem equality is now pointwise and the tree checks under `--safe --without-K --cubical-compatible`). The former real gap (Coq `obliterate_overwrites_all_blocks`) is CLOSED — re-verified 2026-07-16 via `Print Assumptions` (*Closed under the global context*) under Coq 8.18.0 — see `docs/PROOF_HOLES_AUDIT.adoc` +- Proof-hole count (Coq/Agda escape hatches only; *not* a measure of open proof work, which is listed in `docs/audits/2026-11-09-proof-ground-truth.adoc`, e.g. the Lean oracle/spec emptiness mismatch and the four Lean libraries that do not build): **0 real gaps**: 1 justified classical dependency (Coq `is_empty_dir_dec` — a `Theorem` proved with `Classical.classic` and `ClassicalEpsilon`, not a custom `Axiom`; corrected 2026-11-09), 0 Agda postulates (the structural `funext` was removed 2026-11-09: filesystem equality is now pointwise and the tree checks under `--safe --without-K --cubical-compatible`). The former real gap (Coq `obliterate_overwrites_all_blocks`) is CLOSED — re-verified 2026-07-16 via `Print Assumptions` (*Closed under the global context*) under Coq 8.18.0 — see `docs/PROOF_HOLES_AUDIT.adoc` - Idris2 ABI layer: **0 proof holes** (all closed 2026-07-01, issue #151 root — builds under `--total`), 0 `partial` markers, 2 registered primitive-eq axioms (`axStringEqRefl`, `axBits8EqRefl`; gated by `.github/scripts/check-idris2-believe-me.sh`) - 7 fuzz targets in `impl/rust-cli/fuzz/fuzz_targets/` (parser, arith, job-spec, signal-parse, path-ops, glob-expansion, state-machine) diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index 9a4b0e03..c436d788 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -125,7 +125,7 @@ Z3) + 1 ABI-stub tier (Idris2) |`+proofs/agda/FilesystemModel.agda+` |Removed: filesystem equality is now pointwise, so no extensionality is needed -|Coq |`+is_empty_dir_dec+` (a `Theorem` proved by `Classical.classic`; corrected 2026-11-09, it is not an `Axiom`) +|Coq |`+is_empty_dir_dec+` (a `Theorem`, not an `Axiom`; corrected 2026-11-09). It depends on two standard-library axioms: `Classical_Prop.classic` and `ClassicalEpsilon.constructive_indefinite_description` |`+proofs/coq/posix_errors.v+` |Infinite-domain universal quantification |Coq |(closed) `+mkdir_two_dirs_reversible+` diff --git a/docs/audits/2026-11-09-proof-ground-truth.adoc b/docs/audits/2026-11-09-proof-ground-truth.adoc index fdf499f1..35e877d2 100644 --- a/docs/audits/2026-11-09-proof-ground-truth.adoc +++ b/docs/audits/2026-11-09-proof-ground-truth.adoc @@ -173,6 +173,13 @@ direction. After the fix: oracle seam. * *Agda `IsEmptyDir` is a stub* (see the table). Removing `funext` (route plan P5) should also complete this record. +* *No model states filesystem well-formedness.* Nothing in the Lean, Agda or Coq + model says that the parent of an existing path is a directory, so a state where + `["a"]` is a file and `["a","b"]` is a directory is admitted (raised in review on + #223). This is an invariant of the whole model, not a precondition of one + operation, so it belongs in the Agda FinFS spec (route plan OD-30), with each + operation proved to preserve it, and is then carried to the recheck legs. Adding + it to the Lean rmdir alone would make the three models disagree. * *Three Idris2 holes sit outside the proof ledger.* The mathesis hole scanner (`scripts/census/proof-holes.sh`) finds `?fieldsAlignedProof`, `?exampleFieldsAligned` and `?offsetInBoundsProof` in diff --git a/proofs/agda/PreconditionWitnesses.agda b/proofs/agda/PreconditionWitnesses.agda index 40892b41..d3d4fe02 100644 --- a/proofs/agda/PreconditionWitnesses.agda +++ b/proofs/agda/PreconditionWitnesses.agda @@ -64,3 +64,13 @@ symlink-pre-inhabited = record ; parentIsDir = defaultPerms , refl ; parentWritable = mkFSNode Directory defaultPerms , refl , refl } + +-- Negative control: a directory with a child does not satisfy the precondition. +-- Guards against a weakening of `IsEmptyDir` that `rmdir-pre-inhabited` alone +-- would not catch. +rmdir-pre-rejects-nonempty : + ¬ RmdirPrecondition a (mkdir ("a" ∷ "b" ∷ []) (mkdir a emptyFS)) +rmdir-pre-rejects-nonempty pre = + IsEmptyDir.noChildren (RmdirPrecondition.isEmpty pre) + ("a" ∷ "b" ∷ []) (⊑-∷ ⊑-[]) (λ ()) + (_ , fsUpdate-at ("a" ∷ "b" ∷ []) _ (mkdir a emptyFS)) diff --git a/proofs/lean4/PreconditionWitnesses.lean b/proofs/lean4/PreconditionWitnesses.lean index 513e7d7e..c36a271d 100644 --- a/proofs/lean4/PreconditionWitnesses.lean +++ b/proofs/lean4/PreconditionWitnesses.lean @@ -34,6 +34,15 @@ theorem rmdir_pre_inhabited : RmdirPrecondition ["a"] (mkdir ["a"] emptyFS) := b | _ :: _ :: _, _, _, hn => simp [mkdir, fsUpdate, emptyFS] at hn +-- Negative control: a directory with a child does not satisfy the precondition. +-- Guards against a weakening of `isEmptyDir` that `rmdir_pre_inhabited` alone +-- would not catch. +theorem rmdir_pre_rejects_nonempty : + ¬ RmdirPrecondition ["a"] (mkdir ["a", "b"] (mkdir ["a"] emptyFS)) := by + intro h + exact h.isEmpty.2 ["a", "b"] (by simp [List.isPrefixOf]) (by simp) + ⟨⟨FSNodeType.directory, defaultPerms⟩, by simp [mkdir, fsUpdate]⟩ + theorem createFile_pre_inhabited : CreateFilePrecondition ["a"] emptyFS := ⟨by simp [pathExists, emptyFS], ⟨_, rfl⟩, ⟨_, rfl⟩, ⟨_, rfl, rfl⟩⟩ From 0439301e396b50baa4a0a9859c7c5a36943b9955 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:53:46 +0000 Subject: [PATCH 07/10] docs(experiment): Dedukti transport of the Agda proofs to Rocq/Lean Owner ruling OD-32 asked for an experiment on the PROOF-POLICY "transport first" route. Result: it does not work today. - Agda2Dedukti is built on a 2021 Agda fork with no --cubical-compatible, so it cannot read modules written to the canonical invocation, and it predates agda-stdlib 2.x. - Lambdapi's Rocq export drops rewrite rules. A minimal encoding whose proof needs a definition to compute is accepted by lambdapi and by dk check, and rejected by coqc after export. - Lambdapi 4.0.0 has no Lean export. Dedukti works as an independent kernel. The experiment records three options for mathesis and echidna (rules as equations, rules as definitions, a modern Agda front end), all untried. The audit gains a section 7 summarising the follow-up work on this PR. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDjNR1ZoYKEPxSKE2nq --- PROOF-NEEDS.adoc | 4 +- .../audits/2026-11-09-proof-ground-truth.adoc | 33 +++++ .../2026-11-09-dedukti-transport/Nat.lp | 20 +++ .../2026-11-09-dedukti-transport/README.adoc | 135 ++++++++++++++++++ .../2026-11-09-dedukti-transport/lambdapi.pkg | 3 + 5 files changed, 194 insertions(+), 1 deletion(-) create mode 100644 docs/experiments/2026-11-09-dedukti-transport/Nat.lp create mode 100644 docs/experiments/2026-11-09-dedukti-transport/README.adoc create mode 100644 docs/experiments/2026-11-09-dedukti-transport/lambdapi.pkg diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index c436d788..27fdde6a 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -67,7 +67,9 @@ Verus contracts exist |=== The toolchains above were installed outside Guix for this audit; each is an -open §6 `deviation`, listed in the audit record. +open §6 `deviation`, listed in the audit record. The Dedukti experiment adds two more, +Lambdapi 4.0.0 and Dedukti, both from opam on an OCaml 4.14.2 switch (`open`; see +`docs/experiments/2026-11-09-dedukti-transport/`). === Reproduction state (2026-11-01, superseded by 2026-11-09) diff --git a/docs/audits/2026-11-09-proof-ground-truth.adoc b/docs/audits/2026-11-09-proof-ground-truth.adoc index 35e877d2..7ddbd3be 100644 --- a/docs/audits/2026-11-09-proof-ground-truth.adoc +++ b/docs/audits/2026-11-09-proof-ground-truth.adoc @@ -264,3 +264,36 @@ only. The owner rulings of 2026-11-09 are recorded in the route plan (OD-30 to OD-34), and the follow-up commits on this PR carry them out (section 7). + +== 7. Follow-up after the owner rulings (same day, same PR) + +[cols="2,5",options="header"] +|=== +|Ruling |What was done, with the check that shows it + +|OD-30, OD-32: Agda canonical, `funext` removed +|All 10 Agda modules check under `agda --safe --without-K --cubical-compatible +All.agda` (Agda 2.7.0.1, agda-stdlib v2.2): no postulates, no escape pragmas. +Filesystem equality is pointwise (`_≗_`). `IsEmptyDir` now has its emptiness field. +Positive and negative precondition witnesses exist in Agda and Lean; weakening the +Lean `isEmptyDir` to `True` breaks the build. New CI lane: `.github/workflows/agda.yml`. + +|OD-33: Isabelle and Mizar archived; Z3 fixed +|`archive/proofs/` holds both trees with a successor map for all 139 theorems. The +two broken Z3 files now define their operations as array `store`s, check +non-vacuity (`sat`) and negate each goal (`unsat`); dropping a precondition gives +`sat`. `scripts/verify-z3.sh` passes all five files. + +|OD-32: Dedukti transport experiment +|`docs/experiments/2026-11-09-dedukti-transport/`. Transport to Rocq or Lean does not +work today: Agda2Dedukti has no `--cubical-compatible` and predates agda-stdlib 2.x; +Lambdapi's Rocq export drops rewrite rules, so a computed proof is rejected by +`coqc`; Lambdapi 4.0.0 has no Lean export. Dedukti itself checks the same encoding. +The recheck legs are therefore "re-proved", not "transported", for now. +|=== + +The mathesis hole scanner (`scripts/census/proof-holes.sh`) on this branch now +reports 0 axioms, 5 holes and 0 policy violations, down from 1, 5 and 9. The 5 holes +are the 3 `alkahest-shell-transmuter` Idris2 holes and the 2 registered `believe_me` +axioms. The census still counts the archived `.thy` files as Isabelle, because it +does not exclude `archive/`; that is a change for mathesis, not this repository. diff --git a/docs/experiments/2026-11-09-dedukti-transport/Nat.lp b/docs/experiments/2026-11-09-dedukti-transport/Nat.lp new file mode 100644 index 00000000..a347e942 --- /dev/null +++ b/docs/experiments/2026-11-09-dedukti-transport/Nat.lp @@ -0,0 +1,20 @@ +// SPDX-License-Identifier: MPL-2.0 +// Minimal Agda-style encoding: a type of types, naturals, addition by +// rewrite rules (how Agda2Dedukti encodes pattern-matching definitions), +// propositional equality, and a theorem whose proof needs the rules to fire. +constant symbol Univ : TYPE; +injective symbol El : Univ → TYPE; + +constant symbol Nat : Univ; +constant symbol zero : El Nat; +constant symbol succ : El Nat → El Nat; + +symbol add : El Nat → El Nat → El Nat; +rule add zero $n ↪ $n +with add (succ $m) $n ↪ succ (add $m $n); + +constant symbol Eq : El Nat → El Nat → Univ; +constant symbol refl : Π x, El (Eq x x); + +// Needs `add (succ zero) zero ↪ succ zero` to type-check. +symbol one_plus_zero : El (Eq (add (succ zero) zero) (succ zero)) ≔ refl (succ zero); diff --git a/docs/experiments/2026-11-09-dedukti-transport/README.adoc b/docs/experiments/2026-11-09-dedukti-transport/README.adoc new file mode 100644 index 00000000..38b8a6d5 --- /dev/null +++ b/docs/experiments/2026-11-09-dedukti-transport/README.adoc @@ -0,0 +1,135 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell += Experiment: can the Agda proofs be transported to Rocq and Lean through Dedukti? +:toc: preamble + +*Date:* 2026-11-09. *Asked by:* the owner, with route-plan ruling OD-32. +*Why:* `hyperpolymath/standards` PROOF-POLICY §2 says each Agda theorem is rechecked +in Rocq and Lean "transport first": carry the Agda proof term across through +Dedukti/Lambdapi, and only fall back to re-proving by hand. This experiment asks +whether that route works today for a tree like `proofs/agda/`, and what mathesis +and echidna would need to make it work. + +== Result in one paragraph + +Transport to Rocq or Lean does not work today, for three independent reasons. Two +of them are measured, and the third is measured on a minimal stand-in. (1) The +only Agda-to-Dedukti translator, Agda2Dedukti, is built on a 2021 Agda fork that has +no `--cubical-compatible` option, so it cannot read any module written to the +estate's canonical invocation, and it predates the agda-stdlib 2.x that such modules +import. (2) Lambdapi, the hub, exports to Rocq only by *dropping rewrite rules*, +and rewrite rules are how a Dedukti encoding of Agda represents every +pattern-matching definition. A proof that relies on a definition computing is then +rejected by Rocq. (3) Lambdapi 4.0.0 has no Lean export at all. Dedukti itself, +however, checked the same encoding without trouble. So Dedukti is usable *today* +as an independent checking kernel, but not as a bridge to Rocq or Lean. + +== Toolchain + +[cols="2,3",options="header"] +|=== +|Tool |Version and source +|Lambdapi |4.0.0, opam (`opam install lambdapi`), OCaml 4.14.2 switch +|Dedukti (`dk`) |opam (`opam install dedukti`), same switch +|Rocq/Coq |8.18.0, Ubuntu package +|Agda2Dedukti |`Deducteam/Agda2Dedukti` master `c7c7d67` (2022-01-24); *not built*, see below +|=== + +All were installed for this experiment outside Guix: a PROOF-POLICY §6 deviation, +recorded here and in `PROOF-NEEDS.adoc`. + +== Finding 1: Agda2Dedukti cannot read our modules + +Measured from the source, not by running the tool: + +* `stack.yaml` pins the Agda fork `Deducteam/agda` at `b026db1`, branch `to_dk`, + whose `Agda.cabal` says version `2.6.3`: a development snapshot from before the + 2.6.3 release, on the Stackage LTS 18.21 resolver (GHC 8.10). +* That fork's option parser (`src/full/Agda/Interaction/Options/Base.hs`) has + `--safe` and `--without-K` but *no* `--cubical-compatible`. Agda added that flag + in the 2.6.3 release (`CHANGELOG.md` at `v2.6.3`). Every module in `proofs/agda/` + starts with `{-# OPTIONS --safe --without-K --cubical-compatible #-}`, so the + translator's Agda rejects them before translation. +* Our tree imports agda-stdlib v2.2, which states "tested using Agda 2.7.0 and + 2.7.0.1". The translator's own README lists "correct errors when translating the + standard library" as open work. + +Building the translator was not attempted. The session's safety policy refused to +compile an unvetted external repository, and the measured facts above already +decide the question for this tree. + +== Finding 2: Lambdapi's Rocq export drops rewrite rules + +`Nat.lp` (in this directory) is a minimal stand-in for the Agda encoding: +naturals, addition defined by two rewrite rules (as Agda2Dedukti encodes +pattern-matching definitions), an equality type, and the theorem +`one_plus_zero : add (succ zero) zero = succ zero`, proved by `refl`. The proof +only type-checks if `add` computes. + +[source,shell] +---- +lambdapi check Nat.lp # accepted +lambdapi export -o dk Nat.lp > Nat.dk && dk check Nat.dk +# [SUCCESS] Nat.dk was successfully checked. +lambdapi export -o raw_coq Nat.lp > Nat.v +# [Nat.lp:12:0-13:39] Command not translated. <- the rewrite rules +coqc Nat.v +# Error: The term "refl (succ zero)" has type "El (Eq (succ zero) (succ zero))" +# while it is expected to have type "El (Eq (add (succ zero) zero) (succ zero))". +---- + +The exported Rocq file declares `add` as an `Axiom` with no equations, so the +definitional step the proof relies on is gone. (Lambdapi's documentation says the +same: `raw_coq` and `stt_coq` accept only `require`, `open`, `symbol` and `rule`, +and ignore rules. `stt_coq` additionally assumes a simple-type-theory encoding, which +Agda's dependent type theory is not.) A side observation: `raw_coq` does not rename +identifiers that are reserved in Rocq; a symbol named `Set` makes `coqc` fail to +parse, so the stand-in uses `Univ`. + +Nearly every proof in `proofs/agda/` depends on reduction in exactly this way +(`fsUpdate` unfolding, `refl` on computed values), so this blocks transport of the +tree even once Finding 1 is fixed. + +== Finding 3: no Lean export + +Lambdapi 4.0.0's `export -o` accepts `lp`, `raw_dk`, `dk`, `raw_coq` and `stt_coq` +(from `lambdapi export --help`). There is no Lean target. A Lean exporter appears +only in an open Lambdapi pull request. + +== What this means + +* *For this repository.* The recheck legs (OD-30) are "re-proved", not + "transported", for now, and the ledger must say so (§2). Dedukti can still be + added as an extra kernel check later: it is independent of Agda's kernel, but it + is not a Rocq or Lean leg and does not count toward `PWG-2i`. +* *For PROOF-POLICY and mathesis.* "Transport first" is currently unreachable for + any repository that follows the policy's own §2.1 invocation. The policy, or the + mathesis architecture note, should say so explicitly, so that repositories do not + wait on a route that cannot run. Mathesis census rows could carry a + `transport: blocked (agda2dedukti pre-cubical-compatible)` note until it changes. +* *For echidna.* Its exchange layer speaks Dedukti, so it can already use `dk` as an + independent checker. To carry Agda proofs on to Rocq or Lean, the exchange needs + one of three things, in order of effort. None of the three was tried in this + experiment; they are design options for mathesis and echidna to evaluate. + . *Rules as equations.* Export each rewrite rule `l ↪ r` as an axiom + `∀ x̄, l = r` and turn each conversion step in the proof term into an explicit + rewrite (`eq_rect`) on it. Rocq and Lean then check the proof, but the rule + axioms join the trust base, so the leg is at best `PROVEN-WITH-AXIOMS` and is + recorded as "transported, with rule axioms". This is the route mathesis could + adopt soonest. + . *Rules as definitions.* Recognise rule sets that are the clauses of a + terminating function and emit them as a `Fixpoint` / `def` with pattern + matching, so conversion still holds and no axiom is added. This is the + elegant result, but it needs a termination and coverage argument per definition + (Agda already has one; it would have to be carried along). + . *A modern Agda front end.* Port Agda2Dedukti, or write a successor, against + Agda 2.7 and agda-stdlib 2.x with `--cubical-compatible` support. Without it, + neither of the above has an input. + +== Reproduce + +From this directory, with Lambdapi and Dedukti on `PATH` and Rocq installed, run the +four commands in Finding 2. Lambdapi 4.0.0 prints progress lines ("Start +checking …", with colour codes) on standard output, so filter them out of the exported +file before `dk check`, for example with `grep -v checking`. The `lambdapi.pkg` file +makes this directory a Lambdapi package. diff --git a/docs/experiments/2026-11-09-dedukti-transport/lambdapi.pkg b/docs/experiments/2026-11-09-dedukti-transport/lambdapi.pkg new file mode 100644 index 00000000..bc93f5bf --- /dev/null +++ b/docs/experiments/2026-11-09-dedukti-transport/lambdapi.pkg @@ -0,0 +1,3 @@ +# SPDX-License-Identifier: MPL-2.0 +package_name = vshexp +root_path = vshexp From 5b62887799cbbba157dfe3eb19fad5ea78465e7e Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:22:21 +0000 Subject: [PATCH 08/10] docs: clear two Hypatia text-match alerts - FilesystemModel.agda: the historical note no longer uses the word "postulated" (no postulate exists; CSA001 matched the comment). - Dedukti experiment README: name the Agda fork's option parser by its Haskell module rather than a src/full/ path that does not exist in this tree (SD022). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDjNR1ZoYKEPxSKE2nq --- docs/experiments/2026-11-09-dedukti-transport/README.adoc | 2 +- proofs/agda/FilesystemModel.agda | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/experiments/2026-11-09-dedukti-transport/README.adoc b/docs/experiments/2026-11-09-dedukti-transport/README.adoc index 38b8a6d5..05e41913 100644 --- a/docs/experiments/2026-11-09-dedukti-transport/README.adoc +++ b/docs/experiments/2026-11-09-dedukti-transport/README.adoc @@ -45,7 +45,7 @@ Measured from the source, not by running the tool: * `stack.yaml` pins the Agda fork `Deducteam/agda` at `b026db1`, branch `to_dk`, whose `Agda.cabal` says version `2.6.3`: a development snapshot from before the 2.6.3 release, on the Stackage LTS 18.21 resolver (GHC 8.10). -* That fork's option parser (`src/full/Agda/Interaction/Options/Base.hs`) has +* That fork's option parser (Haskell module `Agda.Interaction.Options.Base`) has `--safe` and `--without-K` but *no* `--cubical-compatible`. Agda added that flag in the 2.6.3 release (`CHANGELOG.md` at `v2.6.3`). Every module in `proofs/agda/` starts with `{-# OPTIONS --safe --without-K --cubical-compatible #-}`, so the diff --git a/proofs/agda/FilesystemModel.agda b/proofs/agda/FilesystemModel.agda index 65349abe..8030949a 100644 --- a/proofs/agda/FilesystemModel.agda +++ b/proofs/agda/FilesystemModel.agda @@ -175,7 +175,7 @@ rmdir-removes-path p fs pre (node , eq) = -- they agree on every path. This needs no function extensionality, so the -- module checks under `--safe --without-K --cubical-compatible`. (Until -- 2026-11-09 these theorems were stated with `_≡_` on functions and closed --- with a postulated `funext`.) +-- with an assumed function-extensionality axiom.) -- Helper: from ¬ pathExists, derive fs p ≡ nothing not-path-exists-nothing : ∀ {p : Path} {fs : Filesystem} → From 1f570a37fe1bc305fdd606a35ec14d0c87d51365 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:43:11 +0000 Subject: [PATCH 09/10] fix: address the second CodeRabbit review on the proof-ground-truth PR Archive consumers that were missed: - impl/rust-cli proof_refs, explain and help now point Isabelle entries at archive/proofs/ and label them "archived, unchecked". - ffi/rust no longer lists Isabelle or Mizar files as evidence. - README.adoc and FAQ.adoc drop the removed build-isabelle/build-mizar recipes; the report generator gets a historical-template banner. - `just certify` no longer claims "256 theorems across 6 systems", "100% precondition checking" or Zig memory safety; it points to the ledger and the audit instead. Agda CI: - Drop the grep for postulates and pragmas; `--safe` already rejects them (checked: "Cannot use TERMINATING pragma with safe flag"). - The All.agda coverage check now finds nested modules and accepts `open import` and trailing whitespace. Checked against six cases, including a missing import, a nested module and a name-prefix match. - PreconditionWitnesses: ReversibleDP (mkdirOp a) emptyFS is inhabited. Docs: - Archive successor count: 102 Agda (not 103), 29, 2, 6 = 139. - Audit: Coq already has a partial well_formed invariant (parents exist, not parents-are-directories). - Ledger, PROOF-NEEDS Z3 row, CLAUDE.md system count, Agda stdlib registration step, Lean and Z3 README source-of-truth references. - Z3 note: the queries are quantified, so termination is not guaranteed by a decision procedure; verify-z3.sh times out unknowns (run: 25 ms). - Dedukti experiment: use `--verbose 0` (checked: clean output, warning on stderr) and warn that dk check accepts an empty file. - verify-proofs.sh counts one skipped Agda check, not three. cargo test: 827 passed, 0 failed, 15 ignored (rust-cli); ffi/rust 24 passed. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDjNR1ZoYKEPxSKE2nq --- .github/workflows/agda.yml | 19 ++++------- CLAUDE.md | 2 +- EXPLAINME.adoc | 2 +- FAQ.adoc | 5 ++- Justfile | 16 ++++----- PROOF-NEEDS.adoc | 8 +++-- README.adoc | 4 +-- archive/proofs/README.adoc | 9 +++-- .../audits/2026-11-09-proof-ground-truth.adoc | 10 +++--- .../2026-11-09-dedukti-transport/README.adoc | 16 +++++---- ffi/rust/src/lib.rs | 6 ---- ffi/rust/src/verification.rs | 11 ------- impl/rust-cli/src/commands.rs | 7 ++-- impl/rust-cli/src/help.rs | 2 +- impl/rust-cli/src/proof_refs.rs | 33 ++++++++++--------- proofs/README.adoc | 4 +-- proofs/agda/PreconditionWitnesses.agda | 11 +++++++ proofs/agda/README.adoc | 11 +++++++ proofs/lean4/README.adoc | 14 ++++---- proofs/z3/README.adoc | 3 +- proofs/z3/filesystem_operations.smt2 | 10 ++++-- scripts/generate-verification-report.sh | 17 ++++++---- scripts/verify-proofs.sh | 3 +- 23 files changed, 124 insertions(+), 99 deletions(-) diff --git a/.github/workflows/agda.yml b/.github/workflows/agda.yml index 7cbbcfbb..f1002e81 100644 --- a/.github/workflows/agda.yml +++ b/.github/workflows/agda.yml @@ -75,24 +75,19 @@ jobs: *) echo "::error::expected Agda ${AGDA_VERSION}, got: $ver"; exit 1 ;; esac - - name: No postulates or escape pragmas - working-directory: proofs/agda - run: | - set -euo pipefail - if grep -nE '^[[:space:]]*postulate|TERMINATING|NON_TERMINATING|NO_POSITIVITY_CHECK|NO_UNIVERSE_CHECK' ./*.agda; then - echo "::error::postulate or escape pragma found"; exit 1 - fi - + # Postulates and escape pragmas need no separate grep: `--safe` (below) + # rejects `postulate`, TERMINATING, NO_POSITIVITY_CHECK and the rest. - name: Every module is imported by All.agda working-directory: proofs/agda run: | set -euo pipefail missing=0 - for f in ./*.agda; do - m="$(basename "$f" .agda)" + while IFS= read -r f; do + m="${f#./}"; m="${m%.agda}"; m="${m//\//.}" [ "$m" = "All" ] && continue - grep -qx "import ${m}" All.agda || { echo "::error::${m} is not imported by All.agda"; missing=1; } - done + grep -Eq "^[[:space:]]*(open[[:space:]]+)?import[[:space:]]+${m//./\\.}([[:space:]]|\$)" All.agda \ + || { echo "::error::${m} is not imported by All.agda"; missing=1; } + done < <(find . -name '*.agda' -not -path './_build/*' | sort) exit "$missing" - name: Check All.agda under the estate invocation diff --git a/CLAUDE.md b/CLAUDE.md index 0eeb44ba..906494bf 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -187,7 +187,7 @@ deep-audit session). The corresponding Phase 4C design docs under ### Technology Stack -**Formal Verification (6 systems)**: +**Formal Verification (4 active systems; Isabelle/HOL and Mizar archived)**: - Agda — theory source of truth (owner ruling 2026-11-09) - Lean 4 — recheck leg; also the executable model oracle - Coq — CIC foundation, extraction to OCaml diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index 23d8afc5..7f0fc4d8 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -121,7 +121,7 @@ reproduce. Absence of a tool is an open obligation, not a passing leg | No postulates, no holes, the estate invocation. Filesystem equality is pointwise (`_≗_`). Grade `PWG-3` is derived from the CI receipt on the merge head, not asserted here. See `docs/audits/2026-11-09-proof-ground-truth.adoc` | Same theorems restated in Z3 (Isabelle and Mizar archived 2026-11-09) -| Z3: ASSUMED (no proof certificate) +| argued (the ledger word for PROOF-POLICY §5 `ASSUMED`: a direct SMT run with no proof certificate) | `scripts/verify-z3.sh`, exact result sequence per file | `proofs/z3/` (`archive/proofs/` for Isabelle and Mizar) | §4 exception notes are now recorded in each `.smt2` header. `filesystem_operations` and `symlink_operations` were rewritten on 2026-11-09 to define the operations as array `store`s and negate each goal; the other three still rest on asserted axioms. Isabelle and Mizar were never CI-checked and are archived, unchecked, with a successor map diff --git a/FAQ.adoc b/FAQ.adoc index f305638a..67d8ef94 100644 --- a/FAQ.adoc +++ b/FAQ.adoc @@ -67,9 +67,8 @@ just verify-proofs # Or per-system just build-coq # produces .vo certificates just build-lean4 # compiles to executable -just build-agda # type-checks, generates interface files -just build-isabelle # builds heap image -just build-mizar # set-theoretic foundation +just build-agda # type-checks All.agda under --safe --without-K --cubical-compatible +# Isabelle and Mizar are archived (archive/proofs/README.adoc has the successor map) just build-z3 # SMT SAT/UNSAT queries ---- diff --git a/Justfile b/Justfile index 780b0980..c80a53d1 100644 --- a/Justfile +++ b/Justfile @@ -362,10 +362,10 @@ certify: to ensure correctness of filesystem operations. ### Proof Systems Used - - Coq (primary) - - Lean 4 (cross-verification) - - Agda (dependent types) - - Z3 (SMT verification) + - Agda (theory source of truth) + - Rocq/Coq and Lean 4 (recheck legs) + - Z3 (SMT checks; ASSUMED, no proof certificate) + - Isabelle/HOL and Mizar: archived unchecked (archive/proofs/) ### Key Theorems Verified @@ -374,10 +374,10 @@ certify: 3. **operation_sequence_reversible** - Operation sequences can be undone 4. **transaction_atomicity** - Transactions maintain ACID properties - ### Total Coverage - - 256 theorems verified across 6 proof systems - - 100% precondition checking for all filesystem operations - - Memory safety verified via Zig implementation + ### Coverage + This certificate asserts no theorem count or percentage. Current coverage, + with each obligation's status, is in EXPLAINME.adoc#proof-ledger and + docs/audits/2026-11-09-proof-ground-truth.adoc. EOF diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index 27fdde6a..0365bc5e 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -46,10 +46,12 @@ fixed 2026-11-09 and guarded by `PreconditionWitnesses` context, 35 on standard-library axioms only (funext 30, `classic` 6, `constructive_indefinite_description` 6). No custom `Axiom` -| Z3 (§4 exception, unrecorded) +| Z3 (§4 exception) | `ASSUMED` -| Z3 4.8.12: all 5 files axiomatic; `filesystem_operations` is circular, -`symlink_operations` proves nothing +| Z3 4.8.12. On `main`: all 5 files axiomatic, `filesystem_operations` circular, +`symlink_operations` proving nothing, no exception notes. In PR #223: those two files +define their operations as array `store`s, check non-vacuity and negate each goal; +all 5 carry a §4 note; `scripts/verify-z3.sh` passes. Still `ASSUMED` (no certificate) | Idris2 (engineering/ABI) | `PROVEN-WITH-AXIOMS` diff --git a/README.adoc b/README.adoc index f9752e13..3c715bb2 100644 --- a/README.adoc +++ b/README.adoc @@ -201,8 +201,8 @@ just verify-proofs # Build specific proof system just build-coq # Coq proofs just build-lean4 # Lean 4 proofs -just build-agda # Agda proofs -just build-isabelle # Isabelle proofs +just build-agda # Agda proofs (theory source) +# Isabelle and Mizar are archived: see archive/proofs/README.adoc # Show available commands just --list diff --git a/archive/proofs/README.adoc b/archive/proofs/README.adoc index 25f3f3a1..57bfb340 100644 --- a/archive/proofs/README.adoc +++ b/archive/proofs/README.adoc @@ -15,8 +15,11 @@ unavailable; Mizar's installer was not permitted in the session), and neither ha a CI lane. They are *unchecked*: nothing below says these files were ever accepted by their checker. -*What still uses them.* Nothing. The Justfiles, `scripts/verify-proofs.sh` and -`scripts/validate-with-echidna.sh` were updated in the same change. +*What still uses them.* Nothing checks them. The Justfiles, `scripts/verify-proofs.sh` +and `scripts/validate-with-echidna.sh` no longer run them. The shell's proof +references (`impl/rust-cli/src/proof_refs.rs`) point here and label the Isabelle +entries "archived, unchecked". The FFI verification suite (`ffi/rust`) no longer lists +them as evidence. == Successor map @@ -170,4 +173,4 @@ Agda column is the source of truth; `lean:` and `rocq:` are recheck legs. |mizar |`symlink_operations.miz` |`Th_symlink_unlink_reversible` |agda:symlink-unlink-reversible lean:symlink_unlink_reversible rocq:symlink_unlink_reversible |=== -Counts: 139 theorems; 103 name an Agda successor; 29 name only a Lean or Rocq successor; 2 are only related; 6 are Mizar encoding helpers with no counterpart needed. +Counts: 139 theorems; 102 name an Agda successor; 29 name only a Lean or Rocq successor; 2 are only related (one of them names an Agda theorem); 6 are Mizar encoding helpers with no counterpart needed. diff --git a/docs/audits/2026-11-09-proof-ground-truth.adoc b/docs/audits/2026-11-09-proof-ground-truth.adoc index 7ddbd3be..1103cce4 100644 --- a/docs/audits/2026-11-09-proof-ground-truth.adoc +++ b/docs/audits/2026-11-09-proof-ground-truth.adoc @@ -173,10 +173,12 @@ direction. After the fix: oracle seam. * *Agda `IsEmptyDir` is a stub* (see the table). Removing `funext` (route plan P5) should also complete this record. -* *No model states filesystem well-formedness.* Nothing in the Lean, Agda or Coq - model says that the parent of an existing path is a directory, so a state where - `["a"]` is a file and `["a","b"]` is a directory is admitted (raised in review on - #223). This is an invariant of the whole model, not a precondition of one +* *No model requires the parent of an existing path to be a directory.* Coq has a + partial invariant, `well_formed` (`filesystem_composition.v:437`: every existing + non-root path has an existing parent), used by several composition theorems. It + does not say the parent is a directory, and Lean and Agda have no invariant at + all, so a state where `["a"]` is a file and `["a","b"]` is a directory is admitted + (raised in review on #223). This is an invariant of the whole model, not a precondition of one operation, so it belongs in the Agda FinFS spec (route plan OD-30), with each operation proved to preserve it, and is then carried to the recheck legs. Adding it to the Lean rmdir alone would make the three models disagree. diff --git a/docs/experiments/2026-11-09-dedukti-transport/README.adoc b/docs/experiments/2026-11-09-dedukti-transport/README.adoc index 05e41913..37393d8b 100644 --- a/docs/experiments/2026-11-09-dedukti-transport/README.adoc +++ b/docs/experiments/2026-11-09-dedukti-transport/README.adoc @@ -69,10 +69,10 @@ only type-checks if `add` computes. [source,shell] ---- lambdapi check Nat.lp # accepted -lambdapi export -o dk Nat.lp > Nat.dk && dk check Nat.dk +lambdapi export --verbose 0 -o dk Nat.lp > Nat.dk && dk check Nat.dk # [SUCCESS] Nat.dk was successfully checked. -lambdapi export -o raw_coq Nat.lp > Nat.v -# [Nat.lp:12:0-13:39] Command not translated. <- the rewrite rules +lambdapi export --verbose 0 -o raw_coq Nat.lp > Nat.v +# [Nat.lp:13:0-14:39] Command not translated. <- the rewrite rules (on stderr) coqc Nat.v # Error: The term "refl (succ zero)" has type "El (Eq (succ zero) (succ zero))" # while it is expected to have type "El (Eq (add (succ zero) zero) (succ zero))". @@ -129,7 +129,9 @@ only in an open Lambdapi pull request. == Reproduce From this directory, with Lambdapi and Dedukti on `PATH` and Rocq installed, run the -four commands in Finding 2. Lambdapi 4.0.0 prints progress lines ("Start -checking …", with colour codes) on standard output, so filter them out of the exported -file before `dk check`, for example with `grep -v checking`. The `lambdapi.pkg` file -makes this directory a Lambdapi package. +four commands in Finding 2. Keep `--verbose 0`: without it Lambdapi 4.0.0 prints +progress lines ("Start checking …", with colour codes) on standard output, into the +exported file, and `dk check` then rejects it. With it, the exported files are clean and +the "Command not translated" warning goes to standard error. Check that `Nat.dk` is not +empty before trusting a `dk check` success: an empty file also checks. The +`lambdapi.pkg` file makes this directory a Lambdapi package. diff --git a/ffi/rust/src/lib.rs b/ffi/rust/src/lib.rs index 13f85c95..84b40862 100644 --- a/ffi/rust/src/lib.rs +++ b/ffi/rust/src/lib.rs @@ -259,8 +259,6 @@ impl FfiContext { /// - Z3: proofs/z3/copy_move_operations.smt2 /// - Lean4: proofs/lean4/CopyMoveOperations.lean /// - Agda: proofs/agda/CopyMoveOperations.agda - /// - Isabelle: proofs/isabelle/CopyMoveOperations.thy - /// - Mizar: proofs/mizar/copy_move_operations.miz pub fn copy_file(&mut self, src: &str, dst: &str) -> FfiResult<()> { let src_path = self.resolve_path(src)?; let dst_path = self.resolve_path(dst)?; @@ -289,8 +287,6 @@ impl FfiContext { /// - Z3: proofs/z3/copy_move_operations.smt2 /// - Lean4: proofs/lean4/CopyMoveOperations.lean /// - Agda: proofs/agda/CopyMoveOperations.agda - /// - Isabelle: proofs/isabelle/CopyMoveOperations.thy - /// - Mizar: proofs/mizar/copy_move_operations.miz pub fn move_path(&mut self, src: &str, dst: &str) -> FfiResult<()> { let src_path = self.resolve_path(src)?; let dst_path = self.resolve_path(dst)?; @@ -358,8 +354,6 @@ impl FfiContext { /// - Coq: proofs/coq/rmo_operations.v /// - Lean4: proofs/lean4/RMOOperations.lean /// - Agda: proofs/agda/RMOOperations.agda - /// - Isabelle: proofs/isabelle/RMO_Operations.thy - /// - Mizar: proofs/mizar/rmo_operations.miz /// - Z3: proofs/z3/rmo_operations.smt2 pub fn obliterate(&mut self, path: &str) -> FfiResult<()> { let full_path = self.resolve_path(path)?; diff --git a/ffi/rust/src/verification.rs b/ffi/rust/src/verification.rs index 07d1fe72..4893dc18 100644 --- a/ffi/rust/src/verification.rs +++ b/ffi/rust/src/verification.rs @@ -122,8 +122,6 @@ impl VerificationSuite { "proofs/coq/filesystem_model.v", "proofs/lean4/FilesystemModel.lean", "proofs/agda/FilesystemModel.agda", - "proofs/isabelle/FilesystemModel.thy", - "proofs/mizar/filesystem_model.miz", "proofs/z3/filesystem_operations.smt2", ]; @@ -173,8 +171,6 @@ impl VerificationSuite { "proofs/coq/file_operations.v", "proofs/lean4/FileOperations.lean", "proofs/agda/FileOperations.agda", - "proofs/isabelle/FileOperations.thy", - "proofs/mizar/file_operations.miz", "proofs/z3/filesystem_operations.smt2", ]; @@ -220,8 +216,6 @@ impl VerificationSuite { let locations = vec![ "proofs/coq/file_content_operations.v", - "proofs/isabelle/FileContentOperations.thy", - "proofs/mizar/file_content_operations.miz", ]; let test_path = "verify_write.txt"; @@ -281,8 +275,6 @@ impl VerificationSuite { "proofs/z3/copy_move_operations.smt2", "proofs/lean4/CopyMoveOperations.lean", "proofs/agda/CopyMoveOperations.agda", - "proofs/isabelle/CopyMoveOperations.thy", - "proofs/mizar/copy_move_operations.miz", ]; let src_path = "verify_copy_src.txt"; @@ -331,8 +323,6 @@ impl VerificationSuite { "proofs/z3/copy_move_operations.smt2", "proofs/lean4/CopyMoveOperations.lean", "proofs/agda/CopyMoveOperations.agda", - "proofs/isabelle/CopyMoveOperations.thy", - "proofs/mizar/copy_move_operations.miz", ]; let src_path = "verify_move_src.txt"; @@ -400,7 +390,6 @@ impl VerificationSuite { "proofs/coq/filesystem_model.v", "proofs/lean4/FilesystemModel.lean", "proofs/agda/FilesystemModel.agda", - "proofs/isabelle/FilesystemModel.thy", ]; // Create two separate files diff --git a/impl/rust-cli/src/commands.rs b/impl/rust-cli/src/commands.rs index 95342b58..0760f045 100644 --- a/impl/rust-cli/src/commands.rs +++ b/impl/rust-cli/src/commands.rs @@ -2325,11 +2325,14 @@ pub fn explain_command(cmd: &crate::parser::Command, state: &ShellState) -> Resu // Full proof references if let Some(ref proof) = proof_ref { - println!(" {}", "Verification (6 systems):".bright_yellow().bold()); + println!(" {}", "Proof references:".bright_yellow().bold()); println!(" Coq: {}", proof.coq_location); println!(" Lean 4: {}", proof.lean_location); println!(" Agda: {}", proof.agda_location); - println!(" Isabelle: {}", proof.isabelle_location); + println!( + " Isabelle: {} (archived, unchecked)", + proof.isabelle_location + ); println!(); } diff --git a/impl/rust-cli/src/help.rs b/impl/rust-cli/src/help.rs index 30604a27..a9ab6f5c 100644 --- a/impl/rust-cli/src/help.rs +++ b/impl/rust-cli/src/help.rs @@ -208,7 +208,7 @@ impl HelpEntry { output.push_str(&format!(" Lean 4: {}\n", proof_ref.lean_location)); output.push_str(&format!(" Agda: {}\n", proof_ref.agda_location)); output.push_str(&format!( - " Isabelle: {}\n\n", + " Isabelle: {} (archived, unchecked)\n\n", proof_ref.isabelle_location )); } diff --git a/impl/rust-cli/src/proof_refs.rs b/impl/rust-cli/src/proof_refs.rs index f8279c22..8f19bbc2 100644 --- a/impl/rust-cli/src/proof_refs.rs +++ b/impl/rust-cli/src/proof_refs.rs @@ -87,7 +87,7 @@ impl ProofReference { /// in Coq, Lean 4, Agda, and Isabelle. pub fn format_full(&self) -> String { format!( - "{}\n {}\n Coq: {}\n Lean 4: {}\n Agda: {}\n Isabelle: {}", + "{}\n {}\n Coq: {}\n Lean 4: {}\n Agda: {}\n Isabelle: {} (archived, unchecked)", self.theorem.bright_cyan().bold(), self.description.bright_black(), self.coq_location, @@ -107,7 +107,7 @@ pub const MKDIR_RMDIR_REVERSIBLE: ProofReference = ProofReference { coq_location: "proofs/coq/filesystem_model.v:L45-L62", lean_location: "proofs/lean4/FilesystemModel.lean:L38-L52", agda_location: "proofs/agda/FilesystemModel.agda:L41-L58", - isabelle_location: "proofs/isabelle/FilesystemModel.thy:L35-L50", + isabelle_location: "archive/proofs/isabelle/FilesystemModel.thy:L35-L50", description: "rmdir(mkdir(path, fs)) = fs when preconditions hold", }; @@ -120,7 +120,7 @@ pub const CREATE_DELETE_REVERSIBLE: ProofReference = ProofReference { coq_location: "proofs/coq/file_operations.v:L32-L48", lean_location: "proofs/lean4/FileOperations.lean:L28-L42", agda_location: "proofs/agda/FileOperations.agda:L30-L45", - isabelle_location: "proofs/isabelle/FileOperations.thy:L25-L40", + isabelle_location: "archive/proofs/isabelle/FileOperations.thy:L25-L40", description: "delete_file(create_file(path, fs)) = fs when preconditions hold", }; @@ -133,7 +133,7 @@ pub const WRITE_FILE_REVERSIBLE: ProofReference = ProofReference { coq_location: "proofs/coq/file_content_operations.v:L67-L85", lean_location: "proofs/lean4/FileContentOperations.lean:L58-L74", agda_location: "proofs/agda/FileContentOperations.agda:L62-L78", - isabelle_location: "proofs/isabelle/FileContentOperations.thy:L55-L72", + isabelle_location: "archive/proofs/isabelle/FileContentOperations.thy:L55-L72", description: "write_file(path, old, write_file(path, new, fs)) = fs", }; @@ -146,7 +146,7 @@ pub const COMPOSITION_REVERSIBLE: ProofReference = ProofReference { coq_location: "proofs/coq/filesystem_composition.v:L28-L52", lean_location: "proofs/lean4/FilesystemComposition.lean:L24-L45", agda_location: "proofs/agda/FilesystemComposition.agda:L26-L48", - isabelle_location: "proofs/isabelle/FilesystemComposition.thy:L22-L42", + isabelle_location: "archive/proofs/isabelle/FilesystemComposition.thy:L22-L42", description: "apply_sequence(reverse(ops), apply_sequence(ops, fs)) = fs", }; @@ -159,7 +159,7 @@ pub const COPY_FILE_REVERSIBLE: ProofReference = ProofReference { coq_location: "proofs/coq/copy_move_operations.v:L148", lean_location: "proofs/lean4/CopyMoveOperations.lean:L101", agda_location: "proofs/agda/CopyMoveOperations.agda:L95", - isabelle_location: "proofs/isabelle/CopyMoveOperations.thy:L90", + isabelle_location: "archive/proofs/isabelle/CopyMoveOperations.thy:L90", description: "deleteFile(copyFile(src, dst, fs)) = fs when preconditions hold", }; @@ -172,7 +172,7 @@ pub const MOVE_REVERSIBLE: ProofReference = ProofReference { coq_location: "proofs/coq/copy_move_operations.v:L239", lean_location: "proofs/lean4/CopyMoveOperations.lean:L156", agda_location: "proofs/agda/CopyMoveOperations.agda:L150", - isabelle_location: "proofs/isabelle/CopyMoveOperations.thy:L145", + isabelle_location: "archive/proofs/isabelle/CopyMoveOperations.thy:L145", description: "move(dst, src, move(src, dst, fs)) = fs when preconditions hold", }; @@ -185,7 +185,7 @@ pub const SYMLINK_UNLINK_REVERSIBLE: ProofReference = ProofReference { coq_location: "proofs/coq/symlink_operations.v:L45", lean_location: "proofs/lean4/SymlinkOperations.lean:L45", agda_location: "proofs/agda/SymlinkOperations.agda:L42", - isabelle_location: "proofs/isabelle/SymlinkOperations.thy:L40", + isabelle_location: "archive/proofs/isabelle/SymlinkOperations.thy:L40", description: "unlink(symlink(path, fs)) = fs when preconditions hold", }; @@ -197,7 +197,7 @@ pub const CHMOD_REVERSIBLE: ProofReference = ProofReference { coq_location: "proofs/coq/permission_operations.v:L67", lean_location: "proofs/lean4/PermissionOperations.lean:L52", agda_location: "proofs/agda/PermissionOperations.agda:L70", - isabelle_location: "proofs/isabelle/PermissionOperations.thy:L67", + isabelle_location: "archive/proofs/isabelle/PermissionOperations.thy:L67", description: "chmod(old_mode, chmod(new_mode, path, fs)) = fs when preconditions hold", }; @@ -209,7 +209,7 @@ pub const CHOWN_REVERSIBLE: ProofReference = ProofReference { coq_location: "proofs/coq/permission_operations.v:L149", lean_location: "proofs/lean4/PermissionOperations.lean:L135", agda_location: "proofs/agda/PermissionOperations.agda:L119", - isabelle_location: "proofs/isabelle/PermissionOperations.thy:L166", + isabelle_location: "archive/proofs/isabelle/PermissionOperations.thy:L166", description: "chown(old_uid/gid, chown(new_uid/gid, path, fs)) = fs when preconditions hold", }; @@ -223,7 +223,7 @@ pub const VARIABLE_ASSIGNMENT_REVERSIBLE: ProofReference = ProofReference { coq_location: "proofs/coq/environment_model.v:pending", lean_location: "proofs/lean4/EnvironmentModel.lean:pending", agda_location: "proofs/agda/EnvironmentModel.agda:pending", - isabelle_location: "proofs/isabelle/EnvironmentModel.thy:pending", + isabelle_location: "archive/proofs/isabelle/EnvironmentModel.thy:pending", description: "set(name, old, set(name, new, env)) = env (pre-state capture)", }; @@ -236,7 +236,7 @@ pub const HARDWARE_ERASE_IRREVERSIBLE: ProofReference = ProofReference { coq_location: "proofs/coq/rmo_operations.v:L45-L68", lean_location: "proofs/lean4/RMOOperations.lean:L52-L73", agda_location: "proofs/agda/RMOOperations.agda:L48-L70", - isabelle_location: "proofs/isabelle/RMOOperations.thy:L44-L65", + isabelle_location: "archive/proofs/isabelle/RMOOperations.thy:L44-L65", description: "∀ fs device. ¬∃ op. apply(op, hardware_erase(device, fs)) = fs", }; @@ -250,7 +250,7 @@ pub const OBLITERATE_IRREVERSIBLE: ProofReference = ProofReference { coq_location: "proofs/coq/rmo_operations.v:L70-L95", lean_location: "proofs/lean4/RMOOperations.lean:L75-L98", agda_location: "proofs/agda/RMOOperations.agda:L72-L96", - isabelle_location: "proofs/isabelle/RMOOperations.thy:L67-L89", + isabelle_location: "archive/proofs/isabelle/RMOOperations.thy:L67-L89", description: "∀ fs file. ¬∃ op. apply(op, obliterate(file, fs)) = fs", }; @@ -295,9 +295,12 @@ pub fn print_verification_summary() { ); println!(" 2. {} - Dependent Type Theory", "Lean 4".bright_cyan()); println!(" 3. {} - Intensional Type Theory", "Agda".bright_cyan()); - println!(" 4. {} - Higher-Order Logic", "Isabelle/HOL".bright_cyan()); println!( - " 5. {} - Tarski-Grothendieck Set Theory", + " 4. {} - Higher-Order Logic (archived 2026-11-09, unchecked)", + "Isabelle/HOL".bright_cyan() + ); + println!( + " 5. {} - Tarski-Grothendieck Set Theory (archived 2026-11-09, unchecked)", "Mizar".bright_cyan() ); println!(" 6. {} - SMT Automated Verification", "Z3".bright_cyan()); diff --git a/proofs/README.adoc b/proofs/README.adoc index 42baff5e..400629ea 100644 --- a/proofs/README.adoc +++ b/proofs/README.adoc @@ -141,8 +141,8 @@ lake build [source,bash] ---- cd proofs/agda -agda FilesystemModel.agda -# Produces: FilesystemModel.agdai +agda --safe --without-K --cubical-compatible All.agda +# Checks every module (interface files go under _build/, not committed) ---- ==== Isabelle/HOL and Mizar diff --git a/proofs/agda/PreconditionWitnesses.agda b/proofs/agda/PreconditionWitnesses.agda index d3d4fe02..7b31c61b 100644 --- a/proofs/agda/PreconditionWitnesses.agda +++ b/proofs/agda/PreconditionWitnesses.agda @@ -14,6 +14,7 @@ module PreconditionWitnesses where open import FilesystemModel open import FileOperations open import SymlinkOperations +open import FilesystemComposition open import Data.List using (List; []; _∷_) open import Data.Maybe using (just; nothing) open import Data.Product using (_,_) @@ -74,3 +75,13 @@ rmdir-pre-rejects-nonempty pre = IsEmptyDir.noChildren (RmdirPrecondition.isEmpty pre) ("a" ∷ "b" ∷ []) (⊑-∷ ⊑-[]) (λ ()) (_ , fsUpdate-at ("a" ∷ "b" ∷ []) _ (mkdir a emptyFS)) + +-- The composition theorems quantify over `ReversibleDP`; this shows the +-- record is inhabited, so `operationSequenceReversible` is not vacuous for a +-- sequence containing mkdir (its reverse precondition is the rmdir one). +mkdir-reversibleDP-inhabited : ReversibleDP (mkdirOp a) emptyFS +mkdir-reversibleDP-inhabited = record + { precondition = mkdir-pre-inhabited + ; reversePrecondition = rmdir-pre-inhabited + ; permsWitness = mkdirPerms refl + } diff --git a/proofs/agda/README.adoc b/proofs/agda/README.adoc index 7204d5c2..4b425c6c 100644 --- a/proofs/agda/README.adoc +++ b/proofs/agda/README.adoc @@ -32,6 +32,17 @@ Manifest: == Build +`valence-shell.agda-lib` depends on `standard-library`, so Agda must know where +agda-stdlib v2.2 lives. Register it once (CI does the same): + +```bash +git clone --depth 1 --branch v2.2 https://github.com/agda/agda-stdlib.git ~/agda-stdlib +mkdir -p ~/.agda +echo ~/agda-stdlib/standard-library.agda-lib >> ~/.agda/libraries +``` + +Then check every module: + ```bash cd proofs/agda agda --safe --without-K --cubical-compatible All.agda diff --git a/proofs/lean4/README.adoc b/proofs/lean4/README.adoc index a7aa9e33..ec43a493 100644 --- a/proofs/lean4/README.adoc +++ b/proofs/lean4/README.adoc @@ -1,11 +1,13 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell -= proofs/lean4/ — Lean 4 Filesystem Proofs (Primary Source of Truth) - -Lean 4 (dependent type theory) is the **primary source of truth** for -the valence-shell formal specs (per `../../CLAUDE.md` "Technology -Stack"). The other proof systems (Coq, Agda, Isabelle, Mizar, Z3 SMT) -cross-validate; the parent `../README.md` discusses why polyglot. += proofs/lean4/ — Lean 4 Filesystem Proofs (Recheck Leg and Model Oracle) + +Since the 2026-11-09 owner ruling, Agda (`../agda/`) is the theory source of truth +(standards PROOF-POLICY §1). This Lean tree is a *recheck leg*: its theorems are +target-only evidence until each is compared with its Agda statement. It is also the +executable model oracle (`model_oracle`) that the Rust differential tests drive. +Rocq (`../coq/`) is the other recheck leg; Z3 is a supplementary SMT check; Isabelle +and Mizar are archived (`../../archive/proofs/`). == Files diff --git a/proofs/z3/README.adoc b/proofs/z3/README.adoc index b54d4757..c7b1f3c8 100644 --- a/proofs/z3/README.adoc +++ b/proofs/z3/README.adoc @@ -66,6 +66,7 @@ sweep. == See also * `../README.md` — overall proof-stack design -* `../lean4/README.adoc` — primary source of truth (interactive) +* `../agda/README.adoc` — theory source of truth (owner ruling 2026-11-09) +* `../lean4/README.adoc` — Lean recheck leg and executable model oracle * `../coq/README.adoc` — interactive CIC foundation * `../../docs/PROOF_HOLES_AUDIT.adoc` — proof-debt status diff --git a/proofs/z3/filesystem_operations.smt2 b/proofs/z3/filesystem_operations.smt2 index 57f31546..1ffb6ab7 100644 --- a/proofs/z3/filesystem_operations.smt2 +++ b/proofs/z3/filesystem_operations.smt2 @@ -4,9 +4,13 @@ ; PROOF-POLICY §4 exception note. Obligation: the mkdir/rmdir and ; createFile/deleteFile reversibility, postcondition, independence and ; composition properties, on a finite-map model. Tool: Z3 (SMT, theory of -; arrays + datatypes). Why: these are quantifier-free array identities that an -; SMT solver decides automatically; the theory source of truth is the Agda tree -; (proofs/agda), and this file is a supplementary automated check. Status under +; arrays + datatypes). Why: the goals are array identities an SMT solver checks +; automatically; the theory source of truth is the Agda tree (proofs/agda), and this +; file is a supplementary automated check. The queries are *not* quantifier-free: +; the strictness assertion on `child-of` and the `forall` in `rmdir-pre` add +; quantifiers, so termination is not guaranteed by a decision procedure. Z3 4.8.12 +; returns every expected result in well under a second, and scripts/verify-z3.sh +; fails any `unknown` or timeout (30 s), so a non-terminating query cannot pass. Status under ; §5: ASSUMED, because a direct SMT run without a proof certificate is not a ; kernel-checked witness. ; diff --git a/scripts/generate-verification-report.sh b/scripts/generate-verification-report.sh index 6b87629e..e5bfd771 100755 --- a/scripts/generate-verification-report.sh +++ b/scripts/generate-verification-report.sh @@ -14,6 +14,11 @@ echo "Generating Verification Coverage Report..." cat > "$REPORT_FILE" << 'EOF' # Verification Coverage Report +> **Historical template (milestone M14), not current status.** The current proof +> ledger is `EXPLAINME.adoc#proof-ledger` and +> `docs/audits/2026-11-09-proof-ground-truth.adoc`. Isabelle and Mizar were archived +> unchecked on 2026-11-09 (`archive/proofs/`) and are not listed below. + **Generated**: $(date -u +"%Y-%m-%d %H:%M:%S UTC") **Version**: 0.14.0 **Phase**: M14 Complete - Conditionals & Logical Operators @@ -38,7 +43,7 @@ along with property-based test coverage for each proven theorem. ## Core Filesystem Operations ### mkdir Operation -- ✅ **Proven**: `mkdir_rmdir_reversible` (Lean 4, Coq, Agda, Isabelle, Mizar) +- ✅ **Proven**: `mkdir_rmdir_reversible` (Lean 4, Coq, Agda) - 🔗 **Implemented**: `impl/rust-cli/src/commands.rs:mkdir()` - 🧪 **Tested**: `prop_mkdir_rmdir_reversible` (1000+ iterations) - **Status**: ✅ COMPLETE @@ -60,19 +65,19 @@ pub fn mkdir(state: &mut ShellState, path: &str, quiet: bool) -> Result<()> { ``` ### rmdir Operation -- ✅ **Proven**: `mkdir_rmdir_reversible` (Lean 4, Coq, Agda, Isabelle, Mizar) +- ✅ **Proven**: `mkdir_rmdir_reversible` (Lean 4, Coq, Agda) - 🔗 **Implemented**: `impl/rust-cli/src/commands.rs:rmdir()` - 🧪 **Tested**: `prop_mkdir_rmdir_reversible` (1000+ iterations) - **Status**: ✅ COMPLETE ### touch (create_file) Operation -- ✅ **Proven**: `create_delete_file_reversible` (Lean 4, Coq, Agda, Isabelle) +- ✅ **Proven**: `create_delete_file_reversible` (Lean 4, Coq, Agda) - 🔗 **Implemented**: `impl/rust-cli/src/commands.rs:touch()` - 🧪 **Tested**: `prop_create_delete_file_reversible` (1000+ iterations) - **Status**: ✅ COMPLETE ### rm (delete_file) Operation -- ✅ **Proven**: `create_delete_file_reversible` (Lean 4, Coq, Agda, Isabelle) +- ✅ **Proven**: `create_delete_file_reversible` (Lean 4, Coq, Agda) - 🔗 **Implemented**: `impl/rust-cli/src/commands.rs:rm()` - 🧪 **Tested**: `prop_create_delete_file_reversible` (1000+ iterations) - **Status**: ✅ COMPLETE @@ -82,13 +87,13 @@ pub fn mkdir(state: &mut ShellState, path: &str, quiet: bool) -> Result<()> { ## Composition & Equivalence ### Operation Sequences -- ✅ **Proven**: `operation_sequence_reversible` (Lean 4, Coq, Agda, Isabelle) +- ✅ **Proven**: `operation_sequence_reversible` (Lean 4, Coq, Agda) - 🔗 **Implemented**: `impl/rust-cli/src/state.rs` (undo/redo stack) - 🧪 **Tested**: `prop_sequence_reversible`, `prop_composition_correctness` - **Status**: ✅ COMPLETE ### Filesystem Equivalence -- ✅ **Proven**: `fs_equiv_refl/sym/trans` (Lean 4, Coq, Agda, Isabelle) +- ✅ **Proven**: `fs_equiv_refl/sym/trans` (Lean 4, Coq, Agda) - 🔗 **Implemented**: `impl/rust-cli/src/state.rs` (equivalence via snapshots) - 🧪 **Tested**: `prop_equivalence_reflexive` - **Status**: ✅ COMPLETE diff --git a/scripts/verify-proofs.sh b/scripts/verify-proofs.sh index e80a06a9..a3ae4209 100755 --- a/scripts/verify-proofs.sh +++ b/scripts/verify-proofs.sh @@ -148,8 +148,7 @@ if check_command agda; then "cd proofs/agda && agda --safe --without-K --cubical-compatible All.agda" else log_skip "Agda not installed" - ((TOTAL_TESTS += 2)) - ((SKIPPED_TESTS += 2)) + ((TOTAL_TESTS += 1)) fi echo "" From dfae63c7685115cc745529b8c5e4efcc4c086142 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:45:35 +0000 Subject: [PATCH 10/10] test(proofs): negative Z3 check for non-empty rmdir; Agda sequence witness MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - filesystem_operations.smt2: a directory with an existing strict descendant does not satisfy rmdir-pre (unsat). Mutation check: with the emptiness conjunct removed from rmdir-pre, this query turns sat and verify-z3.sh fails. - PreconditionWitnesses.agda: AllReversibleDP (mkdirOp a ∷ []) emptyFS is inhabited, so operationSequenceReversible has a non-empty instance. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDjNR1ZoYKEPxSKE2nq --- proofs/agda/PreconditionWitnesses.agda | 5 +++++ proofs/z3/filesystem_operations.smt2 | 11 ++++++++++- scripts/verify-z3.sh | 2 +- 3 files changed, 16 insertions(+), 2 deletions(-) diff --git a/proofs/agda/PreconditionWitnesses.agda b/proofs/agda/PreconditionWitnesses.agda index 7b31c61b..56a38ad7 100644 --- a/proofs/agda/PreconditionWitnesses.agda +++ b/proofs/agda/PreconditionWitnesses.agda @@ -85,3 +85,8 @@ mkdir-reversibleDP-inhabited = record ; reversePrecondition = rmdir-pre-inhabited ; permsWitness = mkdirPerms refl } + +-- A one-step sequence satisfies `AllReversibleDP`, so +-- `operationSequenceReversible` has a non-empty instance. +mkdir-sequence-reversibleDP : AllReversibleDP (mkdirOp a ∷ []) emptyFS +mkdir-sequence-reversibleDP = consReversibleDP mkdir-reversibleDP-inhabited nilReversibleDP diff --git a/proofs/z3/filesystem_operations.smt2 b/proofs/z3/filesystem_operations.smt2 index 1ffb6ab7..76bd1155 100644 --- a/proofs/z3/filesystem_operations.smt2 +++ b/proofs/z3/filesystem_operations.smt2 @@ -28,7 +28,7 @@ ; makes trivially true by omitting them. ; ; Expected result sequence (scripts/verify-z3.sh): -; sat, sat, unsat x 9 +; sat, sat, unsat x 10 ; The two `sat` results are non-vacuity checks: the mkdir and rmdir ; preconditions are satisfiable, so the theorems below are not vacuous. @@ -81,6 +81,15 @@ (check-sat) (pop) +; Negative control: a directory with an existing strict descendant does not +; satisfy rmdir-pre (expected: unsat). +(push) +(assert (child-of p1 p)) +(assert (exists-at p1 fs)) +(assert (rmdir-pre p fs)) +(check-sat) +(pop) + ; ===== Reversibility (expected: unsat x 4) ===== (push) diff --git a/scripts/verify-z3.sh b/scripts/verify-z3.sh index 70490b84..31310c56 100755 --- a/scripts/verify-z3.sh +++ b/scripts/verify-z3.sh @@ -50,7 +50,7 @@ verify_file() { # These sequences are part of the checked proof contract. Consistency queries # intentionally return sat; theorem queries assert the negation and must be # unsat. Any unknown, missing result, extra result, or parse error fails. -verify_file proofs/z3/filesystem_operations.smt2 "sat,sat,unsat,unsat,unsat,unsat,unsat,unsat,unsat,unsat,unsat" +verify_file proofs/z3/filesystem_operations.smt2 "sat,sat,unsat,unsat,unsat,unsat,unsat,unsat,unsat,unsat,unsat,unsat" verify_file proofs/z3/copy_move_operations.smt2 "unsat,unsat,unsat,unsat,unsat,unsat,unsat,unsat,unsat,unsat,unsat" verify_file proofs/z3/permission_operations.smt2 "unsat,unsat,unsat,unsat,unsat" verify_file proofs/z3/rmo_operations.smt2 "unsat,unsat,unsat,unsat"