fix(wasm): preserve extern expression stack types

.github/workflows/actions.lock

@@ -3,13 +3,6 @@
 # Docs: https://gh.io/actions-lockfile
 version: 'v0.0.2'
 workflows:
-    '.github/workflows/governance.yml': []
-    '.github/workflows/hypatia-scan.yml': []
-    '.github/workflows/label-triage.yml': []
-    '.github/workflows/labels.yml': []
-    '.github/workflows/mirror.yml': []
-    '.github/workflows/scorecard.yml': []
-    '.github/workflows/secret-scanner.yml': []
     '.github/workflows/abi-verify.yml':
         - 'actions/checkout@v7.0.1'
     '.github/workflows/codeql.yml':
@@ -20,14 +13,21 @@ workflows:
     '.github/workflows/ffi-seams.yml':
         - 'actions/checkout@v7.0.1'
         - 'mlugg/setup-zig@v2.2.1'
+    '.github/workflows/governance.yml': []
+    '.github/workflows/hypatia-scan.yml': []
     '.github/workflows/instant-sync.yml':
         - 'peter-evans/repository-dispatch@v4.0.1'
+    '.github/workflows/label-triage.yml': []
+    '.github/workflows/labels.yml': []
+    '.github/workflows/mirror.yml': []
     '.github/workflows/push-email-notify.yml':
-        - 'dawidd6/action-send-mail@v3.12.0'
+        - 'dawidd6/action-send-mail@v18'
     '.github/workflows/rust-ci.yml':
         - 'actions/checkout@v7.0.1'
         - 'dtolnay/rust-toolchain@v1'
         - 'swatinem/rust-cache@v2.9.2'
+    '.github/workflows/scorecard.yml': []
+    '.github/workflows/secret-scanner.yml': []
     '.github/workflows/status-gate.yml':
         - 'actions/checkout@v7.0.1'
         - 'dtolnay/rust-toolchain@v1'
@@ -38,9 +38,9 @@ dependencies:
         commit: 'sha1-3d3c42e5aac5ba805825da76410c181273ba90b1'
         owner_id: 44036562
         repo_id: 197814629
-    'dawidd6/action-send-mail@v3.12.0':
-        ref: 'v3.12.0'
-        commit: 'sha1-0bbdab096651ee93f37ec02383e088183d41ff0b'
+    'dawidd6/action-send-mail@v18':
+        ref: 'v18'
+        commit: 'sha1-94de994a9f6fffee200243214e17002e2920bb59'
         owner_id: 9713907
         repo_id: 222439721
     'dtolnay/rust-toolchain@v1':

.github/workflows/governance.yml

@@ -15,4 +15,4 @@ permissions:
 
 jobs:
   governance:
-    uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@84355587cb2a1f86e6882de83514a32db2646e7a
+    uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@6b38eb50104901e2fec80f9455a972bc3eced813

.github/workflows/hypatia-scan.yml

@@ -18,4 +18,4 @@ permissions:
 
 jobs:
   scan:
-    uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@84355587cb2a1f86e6882de83514a32db2646e7a
+    uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@6b38eb50104901e2fec80f9455a972bc3eced813

.github/workflows/instant-sync.yml

@@ -22,10 +22,13 @@ jobs:
     timeout-minutes: 5
     steps:
       - name: Trigger Propagation
-        if: ${{ secrets.FARM_DISPATCH_TOKEN != '' }}
+        id: propagate
+        if: ${{ env.FARM_DISPATCH_TOKEN != '' }}
         uses: peter-evans/repository-dispatch@v4.0.1
+        env:
+          FARM_DISPATCH_TOKEN: ${{ secrets.FARM_DISPATCH_TOKEN }}
         with:
-          token: ${{ secrets.FARM_DISPATCH_TOKEN }}
+          token: ${{ env.FARM_DISPATCH_TOKEN }}
           repository: hyperpolymath/.git-private-farm
           event-type: propagate
           client-payload: |-
@@ -37,6 +40,7 @@ jobs:
             }
 
       - name: Confirm
+        if: ${{ steps.propagate.outcome == 'success' }}
         run: echo "::notice::Propagation triggered for ${{ github.event.repository.name }}"
 
       - name: K9-SVC Validation

.github/workflows/mirror.yml

@@ -13,5 +13,5 @@ permissions:
 
 jobs:
   mirror:
-    uses: hyperpolymath/standards/.github/workflows/mirror-reusable.yml@84355587cb2a1f86e6882de83514a32db2646e7a
+    uses: hyperpolymath/standards/.github/workflows/mirror-reusable.yml@6b38eb50104901e2fec80f9455a972bc3eced813
     secrets: inherit

.github/workflows/rust-ci.yml

@@ -31,7 +31,7 @@ concurrency:
 
 jobs:
   rust-ci:
-    uses: hyperpolymath/standards/.github/workflows/rust-ci-reusable.yml@84355587cb2a1f86e6882de83514a32db2646e7a
+    uses: hyperpolymath/standards/.github/workflows/rust-ci-reusable.yml@6b38eb50104901e2fec80f9455a972bc3eced813
 
   no-default-features:
     name: Cargo build + test (ephapax-cli, --no-default-features)

.github/workflows/scorecard.yml

@@ -17,4 +17,4 @@ jobs:
       contents: read
       security-events: write
       id-token: write
-    uses: hyperpolymath/standards/.github/workflows/scorecard-reusable.yml@84355587cb2a1f86e6882de83514a32db2646e7a
+    uses: hyperpolymath/standards/.github/workflows/scorecard-reusable.yml@6b38eb50104901e2fec80f9455a972bc3eced813

.github/workflows/secret-scanner.yml

@@ -21,5 +21,5 @@ jobs:
       contents: read
       pull-requests: write
       actions: read
-    uses: hyperpolymath/standards/.github/workflows/secret-scanner-reusable.yml@84355587cb2a1f86e6882de83514a32db2646e7a
+    uses: hyperpolymath/standards/.github/workflows/secret-scanner-reusable.yml@6b38eb50104901e2fec80f9455a972bc3eced813
     secrets: inherit

CLAUDE.md

@@ -1,7 +1,5 @@
 <!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->
 <!-- Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
-<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->
-<!-- Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
 <!-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> -->
 <!-- Author: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
 
@@ -11,7 +9,7 @@
 
 **This repo is `hyperpolymath/ephapax`.** It is **NOT** `hyperpolymath/affinescript`.
 
-| | This repo | NOT this repo |
+| Criterion | This repo | NOT this repo |
 |---|---|---|
 | Name | **Ephapax** | AffineScript |
 | Path | `hyperpolymath/ephapax` | `hyperpolymath/affinescript` |

docs/proof-debt.adoc

@@ -1,7 +1,83 @@
 Copyright (c) Jonathan D.A. Jewell j.d.a.jewell@open.ac.uk
 SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) –>
 
-== Proof Debt — ephapax (SUPERSEDED — archaeology only)
+== Proof Debt — ephapax
+
+=== Current enforced inventory (2026-08-29)
+
+This section is the current inventory consumed by the trusted-base gate. The
+older closure plan below is retained only as labelled archaeology. A path being
+listed here means that its trust boundary is documented; it does *not* mean the
+obligation has been discharged.
+
+==== `+formal/Semantics.v:9258+` — legacy `+preservation+`
+
+* *Status*: one real outer `+Admitted.+`; not proved.
+* *Classification*: durable legacy counterexample boundary. The theorem as
+  originally stated is false, as demonstrated by the five `+Qed+` witnesses in
+  `+formal/Counterexample.v+`. It must not be presented as closable proof debt
+  without first replacing the false statement.
+* *Owner*: @hyperpolymath.
+* *Acceptance*: retain the counterexample regression and publish any replacement
+  theorem with its exact restricted boundary and zero hidden escape hatches.
+
+==== `+formal/Semantics_L1.v:3318+` — `+step_pop_disjoint_from_type_l1+`
+
+* *Status*: one internal `+admit.+` followed by one outer `+Admitted.+`; not
+  proved.
+* *Obligation*: establish region-count coherence when a congruence step exits a
+  region still required by a sibling's type. Ten former sub-cases are closed;
+  this is the one residual case.
+* *Obstacle*: the snapshot region environment and result type do not encode the
+  temporal distinction needed to show that the sibling's occurrence survives
+  the exit. The choreographic experiment in
+  `+formal/L1-ELIMINATOR-FORK.adoc+` showed that the first proposed formulation
+  relocates this obligation rather than discharging it.
+* *Owner*: @hyperpolymath.
+* *Plan and tracking*: continue the staged calculus work in issues #240, #241,
+  and #242; first require a coherent minimal counterexample/positive control,
+  then prove the supporting lemma without circularly assuming preservation.
+* *Acceptance*: `+Qed.+`, a clean `+Print Assumptions
+  step_pop_disjoint_from_type_l1.+`, and a regression showing that an invalid
+  region exit is rejected.
+
+==== `+formal/Semantics_L1.v:3337+` — `+preservation_l1+`
+
+* *Status*: one internal `+admit.+` followed by one outer `+Admitted.+`; not
+  proved.
+* *Dependency*: blocked by `+step_pop_disjoint_from_type_l1+` and the staged L2
+  restrictions tracked in issues #240, #241, and #242.
+* *Owner*: @hyperpolymath.
+* *Acceptance*: the theorem ends in `+Qed.+`, `+Print Assumptions
+  preservation_l1.+` reports no project escape hatch, and the complete Coq
+  build plus counterexample suite passes.
+
+==== `+idris2/src/Main.idr:22+` — global `+%default partial+`
+
+* *Status*: real module-wide Idris2 totality waiver; configured and compiled,
+  but neither totality-audited nor proved.
+* *Scope*: the affine front-end executable, including argument parsing, file
+  I/O orchestration, parser invocation, type checking, and emission.
+* *Owner*: @hyperpolymath.
+* *Plan and tracking*: issue #380. Audit each definition under
+  `+%default total+`; keep any unavoidable partiality narrowly attached to the
+  smallest I/O boundary with a stated precondition and failure result. This is
+  part of the Idris2 ABI trust boundary, so a global waiver is not an acceptable
+  final state.
+* *Acceptance*: a negative control demonstrates that Idris2 rejects a deliberately
+  non-total pure definition; the module builds under total-by-default checking;
+  every remaining local `+partial+` is individually documented and gated.
+
+=== Rust/Creusot verification boundary
+
+Ephapax contains proof-critical Rust but currently has no Creusot integration,
+contracts, reproducible solver setup, or hard verification gate. Issue #378 is
+the canonical closure record. Rust tests, Coq bridge tests, and typed-Wasm checks
+are valuable evidence, but they do not imply that Creusot obligations were
+generated or discharged. Until #378 is completed with its required failing
+positive control, the Rust implementation is *tested, not Creusot-proved*.
+
+=== Archived 2026-05-26 inventory (superseded)
 
 ____
 === 🛑 SUPERSEDED