Coq: re-verify 0 real gaps + fix build/verify from clean; add just run launcher (#164)

Two outstanding items, both verified with the actual toolchain.

## 1. Coq proof stack — re-verified 0 admits / 0 real gaps (Coq 8.18.0)

The full `_CoqProject` (11 files) compiles with **zero
`admit`/`Admitted`/`Axiom`** markers. `Print Assumptions` on the
load-bearing theorems:

| Theorem | Assumptions |
|---------|-------------|
| `obliterate_overwrites_all_blocks` | **Closed under the global
context** (zero axioms) |
| `overwrite_pass_equalizes_storage` (#57) | **Closed under the global
context** |
| `single_op_reversible` / `operation_sequence_reversible` /
`copy_file_reversible` / `mkdir_two_dirs_reversible` (#56) /
`obliterate_not_injective` (#58) | `functional_extensionality_dep` only
|

The historically-tracked "1 real gap" 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).
**Net: 2 documented axioms, 0 real gaps.**

Docs reconciled (live docs only; dated audit snapshots left as records):
`PROOF_HOLES_AUDIT.md`, `README.adoc`, `FAQ.adoc`, `CLAUDE.md`,
`docs/wiki/`, `ROADMAP*.{adoc,md}`, `STATE.a2ml`, `methodology.a2ml`,
`CHANGELOG.adoc`.

## 2. Coq build/verify entry points — fixed to work 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 order and `mkdir -p extracted` before
`extraction.v`, matching the `validation.yml` CI oracle.
- `scripts/verify-proofs.sh`: fixed two latent `set -e` bugs that
aborted before any test ran — `((VAR++))` counters (first bump from 0
returns exit 1) → assignment form; per-test `cd` leaks → each command
runs in a subshell. Script now runs end-to-end (exit 0).
- gitignore `proofs/coq/.lia.cache`.

## 3. Launcher — add `just run` / `just launch`

The user-facing launcher was missing (no `run`/`setup`/`install`
recipe), and `QUICKSTART-USER.adoc` was an unfilled template promising
recipes that didn't exist.

- Added `just run *ARGS` (alias `just launch`): builds and starts the
interactive `vsh` shell, passing args through. **Verified end-to-end:**
`just run --version` → `vsh 0.9.0` (exit 0); REPL banner starts; `just
run <script>` executes and exits 0.
- Rewrote `QUICKSTART-USER.adoc` to the real flow — every `just` command
it cites is a real recipe (verified via `just --show`).

**Scope note:** full alignment to the external *launcher standard*
(`hyperpolymath/standards`) is not attempted — that repo is outside this
session's GitHub scope. This adds a real, verified launch entry point
consistent with what the quickstart already promised;
standard-conformance can follow when the standard is readable.

## Validation
- `coqc -R . ValenceShell` on all 11 files: clean; `Print Assumptions`
as tabulated.
- `just build-coq` and `scripts/verify-proofs.sh` from a cleaned tree:
exit 0.
- `just run --version`, `just run <script>`: exit 0 with correct output.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

https://claude.ai/code/session_01KfgJznd6jzSeDYsSXGAXkU

---------

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

.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,59 @@ 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
 
+=== Added — 2026-07-16
+
+==== Launcher
+- `just run` (alias `just launch`) — the user-facing launcher for the `vsh`
+  shell, previously missing. Builds and starts the interactive REPL; passes
+  extra arguments through to the binary (`just run --version`,
+  `just run script.vsh`). Verified end-to-end: `--version` prints `vsh 0.9.0`
+  (exit 0), the REPL banner starts interactively, and script execution runs and
+  exits 0.
+- `QUICKSTART-USER.adoc` rewritten from the unfilled RSR template to the real,
+  working flow — it no longer references non-existent recipes (`just setup`,
+  `just uninstall`, `just stapeln-run`, `just install --portable`); every `just`
+  command it now cites is a real recipe (verified via `just --show`). Uninstall
+  documents the honest `cargo uninstall vsh` path.
+
+=== 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

@@ -4,6 +4,9 @@
 # Default recipe - show available commands
 import? "contractile.just"
 
+# `just launch` is a synonym for `just run` (launch the vsh shell)
+alias launch := run
+
 default:
     @just --list
 
@@ -15,13 +18,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 +80,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)
@@ -113,6 +126,14 @@ test-cli:
     cd impl/rust-cli && cargo test
     @echo "✓ Rust CLI tests passed"
 
+# Launch the interactive vsh shell (the primary deliverable). Extra args pass
+# through to the binary:
+#   just run              # start the interactive REPL
+#   just run --version    # print version and exit
+#   just run script.vsh   # run a script
+run *ARGS:
+    cd impl/rust-cli && cargo run -- {{ARGS}}
+
 # Build all FFI layers
 build-ffi: build-ffi-zig build-ffi-ocaml
     @echo "✓ All FFI layers built"