From 8b1bceea0e4c26f039ffd1f125013fcc6001b9b4 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Wed, 20 May 2026 19:51:09 +0100
Subject: [PATCH] chore(machine-readable): correct STATE.a2ml proof-status lie
 (Refs standards#134)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

`STATE.a2ml` claimed:

  # No active blockers. Formal proofs FULLY CLOSED (67 Qed, 0 Admitted).

This was wrong on both axes:

- `formal/Semantics.v::preservation` carries `Qed.` but `coqc` 8.18.0
  rejects it with "Attempt to save an incomplete proof (there are
  remaining open goals)" — the proof never actually closed. PR#92
  (MERGED) marked it `Admitted.` to restore CI green; PR#102 (OPEN)
  reduces the open-goal count from 910 to ~29 via the standard
  remember-cfg preservation pattern. So there's at least 1 Admitted,
  not 0.
- `src/formal/Ephapax/Formal/RegionLinear.idr::regionSafetyExtract` /
  `noGCExtract` are vacuous tautological wrappers (body is the input
  unchanged: `= ne` / `= (ne, lc)`). ROADMAP citing them as
  "regionSafetyTheorem"/"noGCTheorem" complete is overstated. The
  honest E3 (region no-escape) and E4 (no-runtime-GC) obligations are
  stated in `src/abi/Ephapax/ABI/Invariants.idr` (the Rust/SPARK seam
  landed via PR#95-MERGED).

This change updates STATE.a2ml to reflect actual proof state:
- `phase`, `next_action`, `last_action`, `updated` brought to 2026-05-20.
- `@blockers` block now lists the residual proof debt accurately:
  Semantics.v preservation Admitted (with handoff doc pointer), vacuous
  RegionLinear wrappers, and the E1–E6 invariant register from the new
  ABI seam.

No source/proof changes; this is purely the machine-readable artefact
catching up to the actual code state (which the human-readable docs —
ROADMAP, PROOF-NEEDS, RUST-SPARK-STANCE — already reflect after the
2026-05-20 batch of #92/#95/#102).

Refs standards#134 (NOT Closes — joint-close on agreement).

🤖 Generated with [Claude Code](https://claude.com/claude-code)
---
 .machine_readable/6a2/STATE.a2ml | 25 +++++++++++++++++++++----
 1 file changed, 21 insertions(+), 4 deletions(-)

diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml
index 9f725d0d..8d19f51d 100644
--- a/.machine_readable/6a2/STATE.a2ml
+++ b/.machine_readable/6a2/STATE.a2ml
@@ -6,11 +6,28 @@
 
 @state(version="2.0"):
 phase: "implementation"
-next_action: "Wire real PipeWire session through type checker (PipeWire Proving Ground)"
-last_action: "Standardized to RSR 2026 with v2 STATE format and 6a2 alignment"
-updated: 2026-04-23T13:00:00Z
+next_action: "Close residual ~29 open goals in formal/Semantics.v preservation theorem (see formal/PRESERVATION-HANDOFF.md for per-case checklist)"
+last_action: "Rust/SPARK ABI seam landed (PR#95); preservation proof now Admitted with honest open-goal count after 910 -> 29 reduction (PR#102)"
+updated: 2026-05-20T19:00:00Z
 
 @blockers:
-# No active blockers. Formal proofs FULLY CLOSED (67 Qed, 0 Admitted).
+# Formal proofs NOT fully closed (earlier "FULLY CLOSED (67 Qed, 0 Admitted)"
+# claim was wrong — `coqc` 8.18.0 rejects `Qed.` on preservation).
+#   - formal/Semantics.v `preservation`: Admitted (down from 910 to ~29 open
+#     goals via remember-cfg pattern, PR#102). The prior in-file `Qed.` was
+#     rejected with "Attempt to save an incomplete proof"; the build-oracle
+#     is now source of truth. PR#92 marked it Admitted and reverted PR#87's
+#     propagated "Qed, closed 2026-04-27" claim from ROADMAP+PROOF-NEEDS.
+#   - src/formal/Ephapax/Formal/RegionLinear.idr `regionSafetyExtract` /
+#     `noGCExtract`: vacuous wrappers (body is the input unchanged); ROADMAP
+#     citing them as "regionSafetyTheorem"/"noGCTheorem" complete is
+#     overstated. Honest E3/E4 obligations stated in src/abi/Ephapax/ABI/
+#     Invariants.idr (PR#95-MERGED).
+#   - src/abi/Ephapax/ABI/Invariants.idr E1-E6: E1 (preservation) OWED;
+#     E2 (linear consumption) PARTIAL (head form discharged via
+#     splitLinearCoverage PR#85); E3 (region no-escape) PARTIAL (narrow
+#     form discharged via noEscapeTheorem); E4 (no-runtime-GC) OWED;
+#     E5 (WASM compilation) OWED; E6 (IR lowering) OWED.
+# Estate proof-debt arm: standards#134 (OPEN).
 @end
 @end