proofs: ground-truth audit, Lean vacuity fix, Agda under the estate invocation, archive Isabelle/Mizar, Z3 fixes

.github/workflows/agda.yml

@@ -0,0 +1,95 @@
+# 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 --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"
+          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
+
+      # 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
+          while IFS= read -r f; do
+            m="${f#./}"; m="${m%.agda}"; m="${m//\//.}"
+            [ "$m" = "All" ] && continue
+            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
+        working-directory: proofs/agda
+        run: agda --safe --without-K --cubical-compatible All.agda

.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

.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 ""

CLAUDE.md

@@ -54,15 +54,19 @@ 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. 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.
-* Isabelle/Mizar/Z3 are §4 exceptions and need a recorded exception note.
+* *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`).
+* 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
@@ -108,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 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`
+- 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)
 
@@ -117,7 +121,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
@@ -183,13 +187,12 @@ deep-audit session). The corresponding Phase 4C design docs under
 
 ### Technology Stack
 
-**Formal Verification (6 systems)**:
-- Lean 4 — primary source of truth
+**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
-- Isabelle/HOL — cross-validation
-- Agda — intensional type theory
-- 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/`)
@@ -212,12 +215,10 @@ 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)
-    isabelle/           # HOL proofs (76 theorems)
-    mizar/              # Set theory proofs (63 theorems)
-    z3/                 # SMT proofs (125 asserts)
+    agda/               # Theory source of truth (owner ruling 2026-11-09); 10 modules, 0 postulates, --safe --without-K --cubical-compatible
+    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)

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