proofs(coq): re-verify 0 admits/0 real gaps; fix build+verify from clean

Verified the Coq proof tree with coqc + Print Assumptions under Coq 8.18.0:
the full _CoqProject (11 files) compiles with zero admit/Admitted/Axiom
markers. obliterate_overwrites_all_blocks and overwrite_pass_equalizes_storage
are 'Closed under the global context'; single_op_reversible,
operation_sequence_reversible, copy_file_reversible, mkdir_two_dirs_reversible
and obliterate_not_injective depend only on standard functional_extensionality.
The historically-tracked '1 real gap' and the three 2026-06-02 admits
(#56/#57/#58) are all closed. Remaining assumptions are standard/justified:
functional_extensionality (stdlib) + is_empty_dir_dec (justified classical),
Agda funext (structural).

Build/tooling fixes (both failed from a clean checkout):
- just build-coq and scripts/verify-proofs.sh compiled an incomplete file
  subset (missing filesystem_composition.v etc.), so posix_errors.v failed
  with 'Cannot find a physical path bound to logical path
  filesystem_composition'. Both now compile the full _CoqProject chain in
  dependency order and mkdir -p extracted before extraction.v, matching the
  validation.yml CI oracle.
- verify-proofs.sh: fixed two latent set -e bugs that aborted before any test
  ran — ((VAR++)) counters (first bump from 0 returns exit 1) replaced with
  assignment form; per-test cd side effects isolated via subshell.
- gitignore proofs/coq/.lia.cache (Coq Lia build artifact).

Docs reconciled to 0 real gaps (live docs only; dated audit snapshots left as
records): PROOF_HOLES_AUDIT.md, README.adoc, FAQ.adoc, CLAUDE.md,
docs/wiki/{Verification-Status,For-Developers}.md, ROADMAP.adoc,
docs/ROADMAP_TO_V1.md, STATE.a2ml, methodology.a2ml, CHANGELOG.adoc.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01KfgJznd6jzSeDYsSXGAXkU

Author: claude

.machine_readable/6a2/STATE.a2ml

@@ -71,28 +71,33 @@ tasks-completed = [
 ]
 
 [coq-proof-status]
-admitted = 3
+admitted = 0
 axioms-justified = 1
 admitted-detail = """
-3 Admitted markers as of 2026-06-02 post-PR #55 design-gap surfacing:
-
-  1. mkdir_two_dirs_reversible (filesystem_composition.v:697) — non-LIFO
-     sequence reversal; not derivable from two_op_sequence_reversible as
-     stated. Tracked as #56 (restate as LIFO sequence).
-
-  2. overwrite_pass_equalizes_storage (rmo_operations.v:422) — model gap.
-     Needs Hgeom strengthening or conclusion relaxation. Tracked as #57.
-
-  3. obliterate_not_injective (rmo_operations.v:535) — downstream of #57;
-     reconnects once #57 closes. Tracked as #58.
-
-The prior single_op_reversible OpRmdir admit (declared 2026-04-19) was
-Qed-closed by PR #67 (2026-06-01) via OpMkdirWithPerms +
-OpCreateFileWithPerms constructor-variant approach — zero new axioms.
+0 Admitted markers. Re-verified 2026-07-16 with `coqc` + `Print Assumptions`
+under Coq 8.18.0: the full _CoqProject (11 files) compiles with zero
+admit/Admitted/Axiom markers. The 3 admits recorded here on 2026-06-02 are all
+now Qed-closed:
+
+  1. mkdir_two_dirs_reversible (filesystem_composition.v:681, now an Example)
+     — CLOSED (#56); Print Assumptions: functional_extensionality_dep only.
+
+  2. overwrite_pass_equalizes_storage (rmo_operations.v:398) — CLOSED (#57);
+     Print Assumptions: Closed under the global context (zero axioms).
+
+  3. obliterate_not_injective (rmo_operations.v:530) — CLOSED (#58);
+     Print Assumptions: functional_extensionality_dep only.
+
+The single_op_reversible OpRmdir model-permission admit (declared 2026-04-19)
+was Qed-closed via OpMkdirWithPerms + OpCreateFileWithPerms constructor variants
+— zero new axioms. The 1 real gap the audit historically tracked
+(obliterate_overwrites_all_blocks) is CLOSED: Print Assumptions reports Closed
+under the global context. Remaining Coq assumptions: functional_extensionality_dep
+(stdlib standard) + is_empty_dir_dec (1 justified classical).
 """
 axiom-detail = "is_empty_dir_dec: Filesystem = Path -> option FSNode is infinite-domain; universal quantification over all paths is not constructively decidable. Migration: switch to FMaps.t FSNode."
-proof-debt-items-closed = [1, 2]
-proof-debt-open = [3]
+proof-debt-items-closed = [1, 2, 3]
+proof-debt-open = []
 
 [dogfooding-status]
 # Section present per CRG v2.0 schema. Honest disclosure follows.

.machine_readable/bot_directives/methodology.a2ml

@@ -98,7 +98,7 @@ constraints = [
   "Lean -> Rust correspondence is property-tested only (~85% confidence), NOT mechanised — closing this is the critical-path blocker to v1.0.0",
   "Elixir NIF build is broken — impl/elixir/ is reference-only; do not block work on it",
   "BEAM daemon is designed but not implemented — no current SNIF carrier",
-  "Coq has 1 remaining real proof gap: obliterate_overwrites_all_blocks (mechanical induction over overwrite passes) — see docs/PROOF_HOLES_AUDIT.md",
+  "Coq has 0 remaining real proof gaps: obliterate_overwrites_all_blocks is CLOSED (Print Assumptions: Closed under the global context, re-verified 2026-07-16 under Coq 8.18.0) — see docs/PROOF_HOLES_AUDIT.md",
   "Agda has 1 structural axiom (funext) — provable in cubical Agda, intentional in intensional TT",
   "Coq has 1 justified decidability axiom (is_empty_dir_dec) — infinite-domain Filesystem = Path -> option FSNode; switching to FMaps.t FSNode is the documented migration",
   "RMO (GDPR / secure deletion) primitives are stubs in impl/rust-cli/src/commands/secure_deletion.rs — proofs exist for the model, runtime does not yet bind to them",

CHANGELOG.adoc

@@ -17,6 +17,44 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Full POSIX shell compliance (subset)
 - RMO (Remove-Match-Obliterate) proofs for GDPR compliance
 
+=== Verified — 2026-07-16
+
+==== Proofs
+- Coq proof-debt re-verified to **0 admits / 0 real gaps** under Coq
+  8.18.0. The full `_CoqProject` (11 files) compiles with no
+  `admit`/`Admitted`/`Axiom` markers. `Print Assumptions` on the
+  load-bearing theorems: `obliterate_overwrites_all_blocks` and
+  `overwrite_pass_equalizes_storage` are *Closed under the global
+  context* (zero axioms); `single_op_reversible`,
+  `operation_sequence_reversible`, `copy_file_reversible`,
+  `mkdir_two_dirs_reversible`, `obliterate_not_injective` depend only on
+  the standard `functional_extensionality_dep`. The historically-tracked
+  "1 real gap" (`obliterate_overwrites_all_blocks`) and the three
+  2026-06-02 admits (#56/#57/#58) are all closed. Remaining assumptions
+  are standard/justified: Coq `functional_extensionality` (stdlib) +
+  `is_empty_dir_dec` (justified classical), Agda `funext` (structural).
+  Docs reconciled: `PROOF_HOLES_AUDIT.md`, `README.adoc`, `FAQ.adoc`,
+  `CLAUDE.md`, `docs/wiki/`, `ROADMAP*.{adoc,md}`,
+  `.machine_readable/6a2/STATE.a2ml`, `bot_directives/methodology.a2ml`.
+
+=== Fixed — 2026-07-16
+
+==== Build / tooling
+- `just build-coq` and `scripts/verify-proofs.sh` now succeed from a
+  clean checkout. Both previously compiled an incomplete file subset
+  (missing `filesystem_composition.v` and others), so `posix_errors.v`
+  failed with "Cannot find a physical path bound to logical path
+  filesystem_composition"; both now compile the full `_CoqProject`
+  chain in dependency order and `mkdir -p extracted` before
+  `extraction.v` (the gitignored output dir), matching the CI oracle in
+  `validation.yml`.
+- `scripts/verify-proofs.sh`: fixed two latent `set -e` bugs that
+  aborted the script before any test ran — `((VAR++))` counters
+  (post-increment returns the pre-value, so the first bump from 0
+  yields exit status 1) replaced with assignment form; and per-test
+  `cd` side effects that leaked between tests are now isolated by
+  running each test command in a subshell.
+
 === Added — 2026-06-02
 
 ==== Implementation

CLAUDE.md

@@ -86,7 +86,7 @@ The Rust CLI is a functional interactive shell with these features:
 
 - 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)
-- 3 proof holes remaining: 1 real gap (Coq `obliterate_overwrites_all_blocks`), 1 justified axiom (Coq `is_empty_dir_dec` — infinite-domain decidability), 1 structural axiom (Agda `funext` — standard in intensional TT) — see `docs/PROOF_HOLES_AUDIT.md`
+- 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.md`
 - 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)
 
@@ -95,7 +95,7 @@ The Rust CLI is a functional interactive shell with these features:
 ### Critical Priority
 
 1. **No mechanized Lean -> Rust correspondence** — testing only, ~85% confidence
-2. **1 real proof gap** remaining (Coq `obliterate_overwrites_all_blocks` — mechanical induction over overwrite passes), plus 2 documented axioms (1 justified decidability + 1 structural funext) — see `docs/PROOF_HOLES_AUDIT.md`
+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.md`
 3. **NOT production-ready** — research prototype only
 
 ### High Priority
@@ -191,7 +191,7 @@ valence-shell/
     mcp/                # MCP server bindings
   proofs/
     lean4/              # Primary proof source (101 theorems)
-    coq/                # CIC proofs + extraction (131 theorems, 3 admits in extraction.v)
+    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)
@@ -326,7 +326,7 @@ MPL-2.0 (Palimpsest License)
 
 ---
 
-**Last Updated**: 2026-06-01 (drift reconcile: 32 src files / 21,331 LoC, 3 proof holes per audit, 478 theorem candidates, 7 fuzz targets)
+**Last Updated**: 2026-07-16 (Coq proof-debt re-verified: 0 admits / 0 real gaps under Coq 8.18.0; 2 justified/structural axioms remain. Prior 2026-06-01 drift reconcile: 32 src files / 21,331 LoC, 478 theorem candidates, 7 fuzz targets)
 **Version**: see `CHANGELOG.md` (release history) and `impl/rust-cli/Cargo.toml` `[package].version` (semver pin)
 **Status**: Advanced research prototype — NOT production-ready
 **Tests**: 736 passing, 0 failures, 14 ignored

FAQ.adoc

@@ -86,8 +86,9 @@ deep-audit inventory in `docs/audits/2026-06-01-deep-audit.adoc`.
 What is solid:
 
 * The 6-system proofs of the model-layer operations. ~478 theorem candidates;
-  1 real gap remaining (Coq `obliterate_overwrites_all_blocks`) + 2 documented
-  axioms (1 justified decidability + 1 structural funext).
+  0 real gaps (Coq `obliterate_overwrites_all_blocks` CLOSED, re-verified
+  2026-07-16 via `Print Assumptions` under Coq 8.18.0) + 2 documented axioms
+  (1 justified decidability + 1 structural funext).
 * The Rust CLI. 736 tests passing, 0 failures, 7 fuzz targets, working shell
   surface (pipelines, redirections, here-docs, job control, variables, control
   structures, glob, quoting).
@@ -116,12 +117,12 @@ plus the Idris2 ABI layer, distributed as:
 |===
 |System |Count |Notes
 |Lean 4 |101 |Primary source of truth
-|Coq |131 |Includes `extraction.v` — 3 admits remaining
+|Coq |131 |Includes `extraction.v` — 0 admits (re-verified 2026-07-16, Coq 8.18.0)
 |Isabelle/HOL |76 |Cross-validation
 |Agda |85 |3 postulates remaining (including funext)
 |Mizar |63 |Set-theoretic foundation
 |Z3 SMT |125 asserts |Automated decision procedures
-|Idris2 (ABI + filesystem) |~22 |2 holes + 10 partial markers
+|Idris2 (ABI + filesystem) |~22 |0 holes, 0 partials, 2 primitive-eq axioms (closed #151/#152)
 |===
 
 If you see a stale number elsewhere in the repo, please file an issue —
@@ -178,8 +179,8 @@ Valence-shell follows the estate boundary-convention policy
 (`feedback_estate_boundary_conventions`):
 
 * In-process FFI (Rust ↔ C) — Zig scaffolding in `impl/zig/`.
-* Formal ABI / proof carrier — Idris2 in `proofs/idris2/` (~22 theorems, 2 holes,
-  10 partial markers per issue #42).
+* Formal ABI / proof carrier — Idris2 in `proofs/idris2/` (~22 theorems, 0 holes,
+  0 partial markers, 2 primitive-eq axioms; closed via #151/#152, builds under `--total`).
 * BEAM ↔ native — would use SNIFs; not currently wired (BEAM daemon is
   designed but not implemented).
 * Compile target / typed-wasm — not currently a target.

Justfile

@@ -15,13 +15,22 @@ build-all: build-coq build-lean4 build-agda build-isabelle build-mizar build-idr
 verify-all:
     @./scripts/verify-proofs.sh
 
-# Build Coq proofs
+# Build Coq proofs (full _CoqProject chain, in dependency order)
 build-coq:
     @echo "Building Coq proofs..."
-    cd proofs/coq && coqc filesystem_model.v
-    cd proofs/coq && coqc file_operations.v
-    cd proofs/coq && coqc posix_errors.v
-    cd proofs/coq && coqc extraction.v
+    # extraction.v writes to extracted/filesystem.ml; the dir is gitignored, so create it.
+    cd proofs/coq && mkdir -p extracted
+    cd proofs/coq && coqc -R . ValenceShell filesystem_model.v
+    cd proofs/coq && coqc -R . ValenceShell file_operations.v
+    cd proofs/coq && coqc -R . ValenceShell file_content_operations.v
+    cd proofs/coq && coqc -R . ValenceShell copy_move_operations.v
+    cd proofs/coq && coqc -R . ValenceShell symlink_operations.v
+    cd proofs/coq && coqc -R . ValenceShell permission_operations.v
+    cd proofs/coq && coqc -R . ValenceShell filesystem_composition.v
+    cd proofs/coq && coqc -R . ValenceShell filesystem_equivalence.v
+    cd proofs/coq && coqc -R . ValenceShell posix_errors.v
+    cd proofs/coq && coqc -R . ValenceShell rmo_operations.v
+    cd proofs/coq && coqc -R . ValenceShell extraction.v
     @echo "✓ Coq proofs compiled"
 
 # Build Lean 4 proofs
@@ -68,7 +77,8 @@ verify-idris2: build-idris2
 # Extract Coq to OCaml
 extract:
     @echo "Extracting Coq to OCaml..."
-    cd proofs/coq && coqc extraction.v
+    # extraction.v writes to extracted/filesystem.ml; the dir is gitignored, so create it.
+    cd proofs/coq && mkdir -p extracted && coqc extraction.v
     @echo "✓ OCaml code extracted"
 
 # Build OCaml FFI (legacy)

README.adoc

@@ -42,7 +42,7 @@ Valence Shell is a formally verified shell with proven reversibility guarantees.
 == Formal Verification
 * [x] Formally Proven Reversibility: `rmdir(mkdir(p, fs)) = fs`
 * [x] Polyglot Verification: 6 proof systems (Coq, Lean 4, Agda, Isabelle, Mizar, Z3)
-* [x] ~478 Theorem Candidates: Proven across different logical foundations (1 real gap, 1 justified axiom, 1 structural axiom remain — see `docs/PROOF_HOLES_AUDIT.md`)
+* [x] ~478 Theorem Candidates: Proven across different logical foundations (0 real gaps; 1 justified axiom + 1 structural axiom remain — see `docs/PROOF_HOLES_AUDIT.md`)
 * [x] Content Operations: File read/write with proven reversibility
 * [x] MAA Framework: Mutually Assured Accountability with audit trails
 
@@ -358,8 +358,8 @@ Valence Shell sits inside a three-layer architecture; the other two layers are u
 * If preconditions hold, `write(p, old, write(p, new, fs)) = fs`
 * Operations on `p1` don't affect `p2` (when `p1 ≠ p2`)
 * Composition: sequences of operations reverse correctly
-* ~478 theorem candidates proven across 6 verification systems (1 real gap + 2 axioms remain — see `docs/PROOF_HOLES_AUDIT.md`)
-* 2026-06-02 snapshot: 4 admits in `proofs/coq/rmo_operations.v` are annotated with explicit obligations; Idris2 0.8.0 keyword/parse fixes landed alongside (#112/#113/#115/#117) and the build oracle is strict (#118).
+* ~478 theorem candidates proven across 6 verification systems (0 real gaps; 2 justified/structural axioms remain — see `docs/PROOF_HOLES_AUDIT.md`)
+* 2026-07-16 re-verification: `proofs/coq/` compiles with **0 admits** under Coq 8.18.0; `Print Assumptions` on the load-bearing theorems reports *Closed under the global context* or dependence only on standard `functional_extensionality`. Idris2 0.8.0 keyword/parse fixes landed earlier (#112/#113/#115/#117), the build oracle is strict (#118), and the Idris2 layer is hole-free (#151/#152).
 
 === ❌ What Is NOT Guaranteed
 
@@ -604,7 +604,7 @@ See link:LICENSE[LICENSE] for full text.
 
 **Made with ❤️ by humans and AI, for humans who value formal correctness.**
 
-**Status**: Advanced Research Prototype (v0.9.0) | **RSR**: PLATINUM (105/100) | **Proofs**: ~478 theorem candidates (1 real gap remaining) | **Tests**: 736 passing
+**Status**: Advanced Research Prototype (v0.9.0) | **RSR**: PLATINUM (105/100) | **Proofs**: ~478 theorem candidates (0 real gaps; 2 justified axioms) | **Tests**: 736 passing
 
 [.text-center]
 _"Every operation reversible. Every claim proven. Every contributor valued."_

ROADMAP.adoc

@@ -106,8 +106,9 @@ Hard requirements before any v1.0 claim:
 
 * [ ] Mechanized Lean → Rust correspondence (currently property testing
   only, ~85% confidence).
-* [ ] Close all real gaps in `docs/PROOF_HOLES_AUDIT.md` (post-2026-04
-  sweep: 1 real gap, 1 justified axiom, 1 structural).
+* [x] Close all real gaps in `docs/PROOF_HOLES_AUDIT.md` — **DONE**
+  (re-verified 2026-07-16 under Coq 8.18.0): 0 real gaps; 1 justified axiom
+  (`is_empty_dir_dec`) + 1 structural (`funext`) remain.
 * [ ] CRG v2.0 grade B: 6+ diverse external targets, issues fed back.
   See audit `=== External validation` section for the proposed diverse-6
   shape.