fix(codegen): close #556 — async CPS table-miss loud-fail fence (#596)

## Summary

T0 operational-soundness fence (sibling of the just-closed #554).
`gen_function` previously fell through to synchronous `gen_expr`
whenever the ADR-013 async CPS transform did not fire — **even for an
`Async` fn whose async-call result is consumed by a continuation**. That
silently ran the continuation against an unsettled `Thenable` handle: a
wrong runtime value, no diagnostic.

## Fix

A precise loud-fail guard in `lib/codegen.ml::gen_function`: fail with
`UnsupportedFeature` when an `Async` fn performs an async call
**consumed by a continuation** that cannot be CPS-lowered
(`thenableThen` not importable / unrecognised shape / effect side-table
miss), while still lowering the **sound** shapes:
- the `let r = <async-call>; <cont>` base case (transformed as before),
- the bare tail-return-`Thenable` pass-through (#205 convergence
protocol — the host awaits the handle),
- an `Async` fn that performs no async call at all.

This mirrors the #555/#566 "fail loud, never silent" fence already in
the same file. The narrow guard was deliberate: the broader
`fn_is_async`-only guard would have wrongly rejected the valid
`tests/codegen/http_thenable_skeleton.affine` pass-through (verified —
all 7 existing async fixtures still compile).

## Tests

New `E2E Async Fence (#556)` group:
- `async_sync_fallback.affine` → loud `UnsupportedFeature` (negative)
- `async_passthrough_thenable.affine` → still compiles (no
over-rejection)
- `async_no_boundary.affine` → still compiles (no over-rejection)

Full suite **454/454 green**.

Closes #556

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

Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

lib/codegen.ml

@@ -2772,6 +2772,23 @@ let is_async_prim_call (e : expr) : bool =
 let mentions_async_prim (e : expr) : bool =
   Effect_sites.exists_call Effect_sites.is_async_call e
 
+(** ADR-013 / #556. An `Async` fn that the CPS transform did NOT recognise
+    is SOUND to lower synchronously in exactly one shape: its async boundary
+    is a bare tail call whose `Thenable` result flows straight out as the
+    return value (the #205 convergence protocol — the host, not the guest,
+    awaits the handle; e.g. `tests/codegen/http_thenable_skeleton.affine`).
+    Any other un-transformed `Async` body runs a continuation against an
+    unsettled handle, the silent miscompile #556 closes. Recognise the safe
+    pass-through: after peeling trivial block / `return` wrappers the tail is
+    itself an async-primitive call. *)
+let is_async_passthrough (body : expr) : bool =
+  let rec tail = function
+    | ExprBlock { blk_stmts = []; blk_expr = Some e } -> tail e
+    | ExprReturn (Some e) -> tail e
+    | e -> e
+  in
+  is_async_prim_call (tail body)
+
 (** Async-fn body recogniser (ADR-013 #225). Returns
     [Some (pre, binder, async_call, cont)] iff the body is, after
     trivial-block unwrapping, a sequence of zero or more simple
@@ -3013,6 +3030,30 @@ let gen_function (ctx : context) (fd : fn_decl) : (context * func) result =
     match async_base with
     | Some (pre, binder, call, cont, tt_idx) ->
       gen_async_base_case ctx_with_params pre binder call cont tt_idx
+    | None when fn_is_async fd
+                && mentions_async_prim body_expr
+                && not (is_async_passthrough body_expr) ->
+      (* #556: this `Async` fn performs an async call whose result is
+         consumed by a continuation, but the CPS transform did not fire
+         (`thenableThen` not importable on this backend, the body is not the
+         recognised `let r = <async-call>; <cont>` base case, or the effect
+         side-table missed the call site). Lowering it synchronously would
+         run the continuation against an UNSETTLED handle — a silent wrong
+         result. Fail loudly instead; the bare tail-return-`Thenable`
+         pass-through (#205) is still lowered by the `Some`/`gen_expr` arms.
+         This back-ports the #555/#566 "fail loud, never silent" fence to the
+         async path. *)
+      Error (UnsupportedFeature
+        (Printf.sprintf
+          "async function `%s` performs an async call whose result is used \
+           by a continuation, but it could not be lowered to the WASM CPS \
+           form (ADR-013): the `thenableThen` host import is not in scope, \
+           the body is not the recognised `let r = <async-call>; <cont>` \
+           base case, or the effect side-table missed this call site \
+           (Refs #556); lowering it synchronously would run the \
+           continuation before the async result settles. Use `--interp` / \
+           `-i`, or a backend where `thenableThen` is importable."
+          fd.fd_name.name))
     | None -> gen_expr ctx_with_params body_expr
   in
 

test/e2e/fixtures/async_no_boundary.affine

@@ -0,0 +1,15 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2026 hyperpolymath
+//
+// Issue #556 regression fixture (POSITIVE / no-over-rejection). `noop` is
+// declared `Async` but performs no async call at all, so there is no
+// continuation to mis-order — synchronous lowering is correct and must not
+// trip the #556 fence (the guard keys on an actual async-prim call, not the
+// effect row alone).
+fn noop(u: Int) -> Int / { Async } {
+  return u + 1;
+}
+
+fn main() -> Int {
+  return noop(7);
+}

test/e2e/fixtures/async_passthrough_thenable.affine

@@ -0,0 +1,17 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2026 hyperpolymath
+//
+// Issue #556 regression fixture (POSITIVE / no-over-rejection). `launch` is
+// `Async` but its async call is in TAIL position — the `Thenable` handle
+// flows straight out as the return value (the #205 convergence protocol; the
+// host, not the guest, awaits it). This is sound to lower synchronously and
+// must keep compiling: the #556 fence must NOT reject the pass-through shape.
+extern fn fetchHandle(u: Int) -> Int / { Async };
+
+fn launch(u: Int) -> Int / { Async } {
+  fetchHandle(u)
+}
+
+fn main() -> Int {
+  return 0;
+}

test/e2e/fixtures/async_sync_fallback.affine

@@ -0,0 +1,20 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2026 hyperpolymath
+//
+// Issue #556 regression fixture (NEGATIVE). `get` is declared `Async` and
+// performs an async call (`getThenable`) whose result is consumed by a
+// continuation (`h + 0`), but the core-WASM CPS transform cannot fire here
+// (`thenableThen` is not importable). Lowering it synchronously would run
+// the continuation against an UNSETTLED handle — the silent miscompile #556
+// closes. The backend must now fail loudly with an UnsupportedFeature error.
+extern fn getThenable(u: Int) -> Int / { Async };
+
+fn get(u: Int) -> Int / { Async } {
+  let bumped = u + 1;
+  let h = getThenable(bumped);
+  return h + 0;
+}
+
+fn main() -> Int {
+  return get(7);
+}

test/test_e2e.ml

@@ -2268,6 +2268,50 @@ let handler_fence_tests = [
   Alcotest.test_case "deno-esm: handle → loud failure"            `Quick test_handle_deno_loud_fail;
 ]
 
+(* ============================================================================
+   Issue #556: async CPS table-miss loud-fail fence
+   ============================================================================
+
+   gen_function previously fell through to synchronous `gen_expr` whenever the
+   ADR-013 CPS transform did not fire — even for an `Async` fn that performs an
+   async call whose result is consumed by a continuation. That silently ran the
+   continuation against an unsettled `Thenable` handle (a wrong value, no
+   diagnostic). The fence makes that case fail loudly, while still lowering the
+   sound shapes: the `let r = <async-call>; <cont>` base case (transformed), the
+   bare tail-return-`Thenable` pass-through (#205 convergence protocol), and an
+   `Async` fn that performs no async call at all. *)
+
+let test_async_wasm_loud_fail () =
+  match run_wasm_pipeline (fixture "async_sync_fallback.affine") with
+  | Ok _ ->
+      Alcotest.fail
+        "expected UnsupportedFeature for an un-lowerable async-consuming fn \
+         on core-WASM (Refs #556); got Ok — silent synchronous fallback has \
+         regressed"
+  | Error msg ->
+      Alcotest.(check bool) "error names the async fence" true
+        (contains_str "async function" msg)
+
+let test_async_passthrough_still_compiles () =
+  (* Tail-return-Thenable pass-through (#205): sound to lower synchronously;
+     the fence must not over-reject it. *)
+  match run_wasm_pipeline (fixture "async_passthrough_thenable.affine") with
+  | Error msg -> Alcotest.failf "async pass-through should compile, got: %s" msg
+  | Ok _ -> ()
+
+let test_async_no_boundary_still_compiles () =
+  (* `Async` row but no async call ⇒ no continuation to mis-order; must
+     compile (the guard keys on an actual async-prim call, not the row). *)
+  match run_wasm_pipeline (fixture "async_no_boundary.affine") with
+  | Error msg -> Alcotest.failf "async-rowed fn with no async call should compile, got: %s" msg
+  | Ok _ -> ()
+
+let async_fence_tests = [
+  Alcotest.test_case "wasm: async-consuming fn → loud UnsupportedFeature" `Quick test_async_wasm_loud_fail;
+  Alcotest.test_case "wasm: tail-return-Thenable pass-through compiles"   `Quick test_async_passthrough_still_compiles;
+  Alcotest.test_case "wasm: async row without async call compiles"        `Quick test_async_no_boundary_still_compiles;
+]
+
 (* ============================================================================
    Section: Stage 7 — typed-wasm Ownership Verifier (Tw_verify)
    ============================================================================
@@ -5414,6 +5458,7 @@ let tests =
     ("E2E LSP Phase D", lsp_phase_d_tests);
     ("E2E Try/Catch/Finally", try_catch_tests);
     ("E2E Handler Fence (#555)", handler_fence_tests);
+    ("E2E Async Fence (#556)", async_fence_tests);
     ("E2E Ownership Verify", tw_verify_tests);
     ("E2E Cmd Linearity", cmd_linear_tests);
     ("E2E Boundary Verify", tw_interface_tests);