No-False gate hardening, D0/D0b status sync, and the W0 wave (E0/E1 holes, probes, aLib conformer)

.github/workflows/coq-build.yml

@@ -116,6 +116,13 @@ jobs:
           coqc --version
           coq_makefile --help 2>&1 | head -1 || true
 
+      - name: No-False gate scanner self-test
+        working-directory: formal
+        # Fixtures for the gate's scanners: split bypass flags, split
+        # declarations, nested Module qualification, and (using the Coq just
+        # installed) the census of results in ":"-sealed modules.
+        run: bash scripts/test-no-false-gate.sh
+
       - name: Build formal/ via coq_makefile (the merge-oracle command)
         working-directory: formal
         run: |
@@ -129,38 +136,11 @@ jobs:
 
       - name: No-False gate (D0/D0b, owner-ratified 2026-11-05)
         working-directory: formal
-        run: |
-          # The build is axiom-free: no `Admitted.` and no `Axiom` /
-          # `Parameter` in any `_CoqProject` file. While a refuted
-          # statement was `Admitted`, the build could derive `False`
-          # (see docs/reports/2026-11-04-v2-survey, F0/F1). Assuming
-          # Coq's own consistency, an axiom-free build cannot.
-          set -euo pipefail
-          FILES=$(grep -E '\.v$' _CoqProject)
-          if grep -nE '^[[:space:]]*(Admitted\.|Axiom[[:space:]]|Parameter[[:space:]])' $FILES; then
-            echo "no-False gate: Admitted/Axiom/Parameter found above -> FAIL"
-            exit 1
-          fi
-          # Every headline and refutation must be closed under the global
-          # context; any `Axioms:` block fails the gate.
-          OUT=$(coqtop -R . Ephapax 2>&1 <<'EOF2'
-          From Ephapax Require Import Semantics Semantics_L1 TypingL2.
-          From Ephapax Require Import Counterexample Counterexample_StepPop Counterexample_PreservationL1.
-          Print Assumptions Counterexample.preservation_false.
-          Print Assumptions Counterexample_StepPop.step_pop_disjoint_from_type_l1_FALSE.
-          Print Assumptions Counterexample_PreservationL1.preservation_l1_FALSE.
-          Print Assumptions preservation_l2_via_l1.
-          Print Assumptions preservation_l2_app_eff_beta_linear.
-          Print Assumptions preservation_l2_app_eff_beta_ground_nonlinear.
-          EOF2
-          )
-          echo "$OUT" | tail -60
-          if echo "$OUT" | grep -qE '^Axioms:|Error'; then
-            echo "no-False gate: a printed result depends on an axiom, or coqtop errored -> FAIL"
-            exit 1
-          fi
-          test "$(echo "$OUT" | grep -c 'Closed under the global context')" -eq 6
-          echo "no-False gate: PASS (0 Admitted, 0 Axiom, 6/6 closed)"
+        # Comment-aware token scan, kernel-bypass scan, a Print Assumptions
+        # census of every named result (the six headlines must be present),
+        # and an independent coqchk recheck of the compiled libraries. See the
+        # header of formal/scripts/no-false-gate.sh for the exact claim.
+        run: bash scripts/no-false-gate.sh
 
   # Always-on aggregator. This is the ONLY job listed in the Base ruleset's
   # required_status_checks rule (#244). If detect-relevant-changes determined

.machine_readable/6a2/STATE.a2ml

@@ -8,10 +8,10 @@
 # current_* fields below supersede the 2026-06 journal text and the dated
 # owner-directive snapshot; see CLAUDE.md and PROOF-NEEDS.adoc for policy.
 phase: "implementation"
-next_action: "Owner-approved L1/L2 soundness redesign: preserve the legacy five-Qed counterexample and durable Admitted; do not prove the refuted step_pop_disjoint_from_type_l1 or preservation_l1 statements; do not claim unconditional L2 preservation. First classify each exact obligation under hyperpolymath/mathesis/estate-mathematical-architecture and standards/3-practice/PROOF-POLICY.adoc. Grade 3 is Agda-only; current Coq witnesses are not Grade 3, and Ephapax-specific engineering claims map to Idris2 unless an implementation-independent Agda theory statement is explicitly defined. Update the proof ledger after policy resolution; no proof build was run in this environment."
+next_action: "Owner-approved L1/L2 soundness redesign: preserve the legacy five-Qed counterexample; do not prove the refuted step_pop_disjoint_from_type_l1 or preservation_l1 statements; do not claim unconditional L2 preservation. First classify each exact obligation under hyperpolymath/mathesis/estate-mathematical-architecture and standards/3-practice/PROOF-POLICY.adoc. Grade 3 is Agda-only; current Coq witnesses are not Grade 3, and Ephapax-specific engineering claims map to Idris2 unless an implementation-independent Agda theory statement is explicitly defined. Update the proof ledger after policy resolution; no proof build was run in this environment."
 last_action: "Proof + stdlib wave 2026-06-01 → 02 landed (13 PRs): canonical-forms L1 modality-polymorphic (#274, P43, 7 lemmas axiom-free, prerequisite for progress_l1/P42); Print Assumptions audit framework across L1 + L3 keystones (#270, closes P10/P32); step_pop_disjoint_from_type_l1 stated + EASY cases Qed-closed (#280, P06, HARD cases blocked on #240/#241/#242); Rust↔Coq is_linear_ty truth-table mechanical assertion (#273, P28); OwnershipKind from_byte/to_byte round-trip (#277, P59, typed-wasm ADR-0002 carrier handshake); 4 stdlib DB-theory additions — Transactions as linear scopes (#275, D04), Allen's interval algebra (#272, D11), MessageHandle as linear typestate (#279, D17), monoidal aggregates (#281, D18); doc truth-restore + banned-preservation framing buried (#263); cluster-D L3/L4 status meander (#278); Track C panic-attack triage (#271); coq-build noble apt CI fix (#282, unblocks ~5 PRs); R5b standards SHA bump (#276). Plus CHANGELOG sync (#283). Build oracle clean across all 12 .v files. Print Assumptions: canonical_*_l1_m + most new lemmas zero-axiom; expected residuals (preservation_l1, region_liveness_at_split_l1_gen, region_shrink_preserves_typing_l1_gen_m) tracked. Stages 2-4 (#240/#241/#242) still un-touched. Wiki Proof-status.md refreshed 2026-06-02. | INFRA (2026-06-24, non-proof track): governance docs landed (#314 — CODEOWNERS/GOVERNANCE.adoc/MAINTAINERS.adoc); standards reusable-workflow pins remediated (#315) and current at d135b05 (#316); Hypatia neurosymbolic gate now active and reporting 37 pre-existing findings (5 crit / 7 high / 25 med) — triage handed off (docs/governance/HYPATIA-HANDOFF.md), standards visibility patch drafted-not-applied. No .v files touched; no proof-state change."
 current_last_action: "2026-11-01 proof-honesty audit: updated local status surfaces, retained all proof terms, and recorded Mathesis Grade 3/standards mapping without promoting Coq evidence to Grade 3. No Coq build run; coqc unavailable."
-current_proof_boundary: "Legacy preservation is refuted and its Admitted is durable; step_pop_disjoint_from_type_l1 and modality-polymorphic preservation_l1 are refuted as stated; no unconditional preservation_l2 theorem is declared; preserve all Coq regressions."
+current_proof_boundary: "Legacy preservation is refuted; step_pop_disjoint_from_type_l1 and modality-polymorphic preservation_l1 are refuted as stated; no unconditional preservation_l2 theorem is declared; preserve all Coq regressions."
 current_grade_target: "Mathesis Grade 3 requested but not claimed. Grade 3 requires local Agda checking; current regressions are Coq. Standards proof policy maps repo-specific engineering claims to Idris2 unless an implementation-independent Agda theory statement is explicitly identified."
 proof_policy_sources: ["https://github.com/hyperpolymath/mathesis/blob/main/estate-mathematical-architecture", "https://github.com/hyperpolymath/standards/blob/main/3-practice/PROOF-POLICY.adoc"]
 proof_status_source: "PROOF-NEEDS.adoc + EXPLAINME.adoc proof ledger"
@@ -61,11 +61,6 @@ updated: 2026-11-01
 #     and their at_pre helpers are Qed but support legacy-preservation
 #     closure attempts that are now ruled out. Retained for diagnostic
 #     value; no new lemmas in this class.
-#   - formal/Semantics_L1.v `preservation_l1`: stated `forall m`; body
-#     Admitted (lambda-rigidity gap, closes at Phase D / L2 effect-typed
-#     TFun per PRESERVATION-DESIGN.md §5.1). 5 inner `admit.` cases
-#     (3 distinct structural blockers + 2 mechanical mirrors) covered
-#     by 3 outer Admitted markers. Zero new debt introduced post-L2.
 #   - formal/Semantics_L1.v `preservation_l3`: Qed, both modes, slice 4
 #     of L3 wiring landed 2026-05-27 (PR #196).
 #   - formal/TypingL1.v: m-indexed (`has_type_l1 m R G e T R' G'`),
@@ -99,11 +94,11 @@ updated: 2026-11-01
 
 @artifacts:
 # Layered files on main (post-slice-4 + Phase A):
-#   formal/Counterexample.v   — 5 Qed lemmas; preservation FALSE
+#   formal/Counterexample.v   — preservation FALSE
 #   formal/Echo.v             — L3 calculus, K-free, 12 Qed
 #   formal/Modality.v         — L2 thin poset, all Qed
 #   formal/TypingL1.v         — m-indexed has_type_l1 + Echo/Observe rules
-#   formal/Semantics_L1.v     — 26 Qed, 3 outer Admitted (5 inner admit.)
+#   formal/Semantics_L1.v
 #   formal/TypingL2.v         — L2_lift_l1 + T_App_L2_Eff +
 #                                preservation_l2_via_l1 (Phase D slice 4 partial)
 #   formal/L4.v               — ProgramMode labelling discipline (Phase A)

0-AI-MANIFEST.a2ml

@@ -24,7 +24,7 @@ These 7 A2ML files MUST exist in `.machine_readable/6a2/` directory ONLY:
 
 ## CORE INVARIANTS
 
-1. **Formal Proof Integrity** — Coq proofs are layered per the four-layer redesign (`formal/PRESERVATION-DESIGN.md`). The legacy `preservation` in `Semantics.v` is provably FALSE per `Counterexample.v` (5 Qed lemmas) and remains `Admitted`. The L1 preservation chain (`Semantics_L1.v`) is in flight; explicit `Admitted` / `admit.` / `Axiom` sites are enumerated by `file:line` in `docs/proof-debt.adoc` per the standards#203 trusted-base reduction policy. Idris2 source has no `believe_me` / `assert_total` / `sorry`. ANY new escape hatch must be enumerated in `docs/proof-debt.adoc` before the trusted-base CI check will pass.
+1. **Formal Proof Integrity** — Coq proofs are layered per the four-layer redesign (`formal/PRESERVATION-DESIGN.md`). The legacy `preservation` in `Semantics.v` is provably FALSE per `Counterexample.v`. Explicit `Admitted` / `admit.` / `Axiom` sites are enumerated by `file:line` in `docs/proof-debt.adoc` per the standards#203 trusted-base reduction policy. Idris2 source has no `believe_me` / `assert_total` / `sorry`.
 2. **Dyadic Separation** - The boundary between affine and linear types must be strictly enforced.
 3. **SPDX Headers** - All source files MUST carry `SPDX-License-Identifier: MPL-2.0`.
 // Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>

CHANGELOG.adoc

@@ -4,6 +4,33 @@ All notable changes to Ephapax are documented here.
 
 === https://github.com/hyperpolymath/ephapax/compare/v0.8.0...HEAD[Unreleased]
 
+==== v2 plan rungs E0 + E1 in the Rust implementation (2026-11-09)
+
+* *E0, holes first* (gate `+src/ephapax-cli/tests/linearity_holes.rs+`):
+a `+let!+` of any type, and any linear-typed binding, may not be used
+twice; `+Ty::is_linear+` takes the join over products, sums, tuples and
+lists (a deliberate, conservative divergence from Coq `+is_linear_ty+`,
+recorded in `+docs/coq-rust-bridge/is_linear_ty.adoc+`); a closure may
+not consume a captured linear value; a borrow of a linear value may not
+be dereferenced into an owned value; a pattern wildcard over a linear
+component and a duplicate pattern binder are rejected; tuple/list
+projection that would discard a linear component is rejected; recursive
+`+data+` is the named `+DesugarError::RecursiveType+` instead of a stack
+overflow. Pair destructuring now lowers to a core `+match+`.
+* *E1, fail loudly* (gate `+src/ephapax-cli/tests/fail_loud.rs+`):
+`+perform+`/`+handle+` are a `+CodegenError+` (no module is written, and
+`+check+` reports the same error); raw variadic `+__ffi+` is rejected
+(`+RawFfiNotSupported+`), so typed `+extern+` is the only FFI path and
+the import index space is contiguous. The interpreter does not bind typed
+`+extern+` declarations: calling one fails with an unbound-variable error
+even with `+-L+`; `+@total+`, `+@pure+` and
+`+@comptime+` are a parse error (`+AnnotationNotEnforced+`); `+-O+` above 0
+and `+--mode+` are rejected; `+--debug+` now adds the `+ephapax.debug.mode+`
+section as well as writing the source map. `+stdlib/Coproc.eph+` and
+`+conformance/valid/ffi_basic.eph+` were migrated to typed `+extern+`
+blocks; the interpreter's `+-L+` FFI loader no longer has a reachable
+caller.
+
 ==== Governance, CI & security-scan infrastructure (2026-06-24)
 
 * *Governance model formalised* (PR #314): added `+.github/CODEOWNERS+`

CLAUDE.md

@@ -109,8 +109,10 @@ redesign and state sound replacement theorems, not to prove refuted ones.
 > `…_stmt : Prop`, refuted by `Counterexample_StepPop.v` and
 > `Counterexample_PreservationL1.v`. While they were `Admitted`, the build
 > could derive `False`. `formal/` now has **0 `Admitted` and 0 `Axiom`**,
-> and CI's no-False gate (`coq-build.yml`) blocks any new
-> `Admitted`/`Axiom`/`Parameter`. The fence below is unchanged in spirit:
+> and CI's no-False gate (`formal/scripts/no-false-gate.sh`, run by
+> `coq-build.yml`) fails on any assumption vernacular or `admit` outside
+> comments, on any kernel-check bypass, on any named result not closed under
+> the global context, and on any Ephapax axiom that `coqchk` finds. The fence below is unchanged in spirit:
 > never try to prove a refuted statement.
 
 > The guardrails below protect pinned counterexamples and the false
@@ -202,13 +204,17 @@ them if asked; if asked anyway, push back and link this section.
    prove it locally and report its assumptions and regressions.
 
 4. **DO follow estate proofing and grading policy.** Consult
-   `hyperpolymath/mathesis/estate-mathematical-architecture` for grades
-   and `hyperpolymath/standards/3-practice/PROOF-POLICY.adoc` for prover
-   mapping. Mathesis Grade 3 specifically requires a local Agda proof;
-   Coq `Qed` is Coq evidence, not Grade 3. Standards maps
-   Ephapax-specific engineering claims to Idris2 unless an
-   implementation-independent theory statement is explicitly defined.
-   Do not assign a Grade 3 label until that classification and exact
+   `hyperpolymath/standards/3-practice/PROOF-POLICY.adoc` for prover
+   mapping and for Proof Witness Grades (§8, which supersedes the grades in
+   the mathesis brief). `PWG-3` requires a local Agda proof checked with
+   `agda --safe --without-K --cubical-compatible`; Coq `Qed` is Coq
+   evidence, not `PWG-3`, and counts as a recheck leg only once an Agda
+   source exists and the statements are `RECONCILED`. Always write the
+   `PWG-` prefix. Owner ruling 2026-11-09: the soundness statements
+   (calculus, progress, preservation, L1–L4 obligations, refutations) are
+   *theory*, with an Agda source of truth; the Idris2 ABI and the Rust
+   implementation stay engineering.
+   Do not assign a PWG until that classification and exact
    statement correspondence are recorded in `EXPLAINME.adoc` and
    `PROOF-NEEDS.adoc`.
 

Cargo.toml

@@ -57,11 +57,11 @@ ephapax-meta = { path = "src/ephapax-meta" }
 ephapax-vram-cache = { path = "src/ephapax-vram-cache" }
 
 # Sibling-repo crates.
-# NOTE: rev pin is the post-merge SHA of typed-wasm#65 on
-# `hyperpolymath/typed-wasm:origin/main` (renames the custom section
-# `affinescript.ownership` → `typedwasm.ownership`). This is the
-# canonical C7 pin (cf. CHANGELOG.md "Added" / "C7 (#72)"). Re-bump
-# only if a newer `typed-wasm-verify` API change is needed.
+# NOTE: rev pin is the merge commit of typed-wasm#203 (2026-07-07,
+# per-module split + `tw link`, #140), checked 2026-11-09. It postdates
+# typed-wasm#65, which renamed the custom section `affinescript.ownership`
+# → `typedwasm.ownership`. Re-bump only when a newer `typed-wasm-verify`
+# API change is needed, and update this comment with the new PR.
 typed-wasm-verify = { git = "https://github.com/hyperpolymath/typed-wasm", rev = "5d67603852098561d5f4e967f6d0bdf3d3e10a16", features = ["unstable-l2"] }
 
 # External dependencies