|
| 1 | +// SPDX-License-Identifier: PMPL-1.0-or-later |
| 2 | +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> |
| 3 | + |
| 4 | += Async-over-WasmGC Convergence ABI |
| 5 | +Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 6 | +:toc: preamble |
| 7 | +:icons: font |
| 8 | +:sectnums: |
| 9 | + |
| 10 | +This document fixes the *shared async boundary protocol* for languages that |
| 11 | +target typed WasmGC through this repository — currently AffineScript and |
| 12 | +Ephapax (typed-wasm ADR-004). It is the convergence-ABI section asked for by |
| 13 | +typed-wasm#31, surfaced by AffineScript #225 / ADR-013. |
| 14 | + |
| 15 | +It is a *binary-level* contract only. It does not couple AffineScript to |
| 16 | +typed-wasm, nor constrain Ephapax's design. Each language keeps its own |
| 17 | +surface syntax and effect discipline; they agree only on what crosses the |
| 18 | +WASM boundary so a module compiled by one can interoperate with a host (or |
| 19 | +module) serving the other. |
| 20 | + |
| 21 | +== Problem |
| 22 | + |
| 23 | +The WASM boundary is synchronous and i32-only. An async host operation |
| 24 | +(e.g. `fetch`) cannot return its result across that boundary directly. A |
| 25 | +shared convention is needed so that both languages' backends — and any |
| 26 | +host that serves them — speak the same async protocol without per-language |
| 27 | +FFI shims. |
| 28 | + |
| 29 | +== The protocol |
| 30 | + |
| 31 | +=== Thenable handle (synchronous return) |
| 32 | + |
| 33 | +An async host import returns a *`Thenable` handle* (an `i32`) synchronously. |
| 34 | +The host registers the pending `Promise`/future in a per-instance handle |
| 35 | +table keyed by that `i32`. The handle is opaque to the guest. |
| 36 | + |
| 37 | +An async *guest* function likewise returns a `Thenable` handle representing |
| 38 | +its own eventual completion. The protocol therefore *composes up the call |
| 39 | +chain*: a backend may present a transparent value-returning surface (e.g. |
| 40 | +AffineScript ADR-013's CPS transform) by threading handles internally, with |
| 41 | +no JSPI and no stack switching. |
| 42 | + |
| 43 | +=== Continuation registration |
| 44 | + |
| 45 | +The guest registers a continuation with: |
| 46 | + |
| 47 | +---- |
| 48 | +thenableThen(handle: i32, closure: i32) -> i32 // returns a new Thenable |
| 49 | +---- |
| 50 | + |
| 51 | +`closure` is a function value in the *shared closure ABI*: |
| 52 | + |
| 53 | +[cols="1,3", options="header"] |
| 54 | +|=== |
| 55 | +| Offset | Field |
| 56 | + |
| 57 | +| `@0` | `i32` — function table index (`funcref` in the module's single |
| 58 | + indirect-call table; AffineScript: `__indirect_function_table`) |
| 59 | +| `@4` | `i32` — environment pointer (captured-locals block, fields at |
| 60 | + `i*4`); `0` when there are no captures |
| 61 | +|=== |
| 62 | + |
| 63 | +Continuation invocation, performed by the host on settlement, is an indirect |
| 64 | +call through that table with signature: |
| 65 | + |
| 66 | +---- |
| 67 | +(env_ptr: i32) -> i32 |
| 68 | +---- |
| 69 | + |
| 70 | +The settled value is *not* passed as an argument. The continuation obtains |
| 71 | +it by calling the result accessor (see <<settlement>>) keyed by the |
| 72 | +`Thenable` handle, which the backend captures into the continuation |
| 73 | +environment reachable through `env_ptr` (AffineScript: the handle is the |
| 74 | +sole live local at the async split, captured via the #199 closure env). |
| 75 | +This is the *accessor model* (ratified 2026-05-19, resolving an earlier |
| 76 | +two-arg `(env_ptr, settled)` ambiguity in favour of the accessor form that |
| 77 | +both the host re-entry primitive `#205` and AffineScript #225 PR 2 |
| 78 | +implement; see <<conformance>>). The result is the handle the continuation |
| 79 | +itself completes with (enabling chaining). |
| 80 | + |
| 81 | +NOTE: This is the *only* hard convergence requirement and it is *already |
| 82 | +satisfied on both sides*. AffineScript #199 marshals `[fnId@0, envPtr@4]` |
| 83 | +through `__indirect_function_table`. Ephapax `ephapax-wasm` emits a closure |
| 84 | +cell `[table_idx@0, env_ptr@4]` (8-byte `CLOSURE_SIZE`) called via |
| 85 | +`call_indirect` with `(env_ptr, param) -> i32`. These are byte-identical; |
| 86 | +no reconciliation is required. |
| 87 | + |
| 88 | +[[settlement]] |
| 89 | +=== Settlement re-entry and result read |
| 90 | + |
| 91 | +When the underlying `Promise`/future settles, the host re-enters the guest |
| 92 | +by invoking the registered continuation closure exactly once (with |
| 93 | +`env_ptr` only — the settled value is not an argument, per the accessor |
| 94 | +model above). The settled value is read by the guest via a result |
| 95 | +accessor: |
| 96 | + |
| 97 | +---- |
| 98 | +thenableResultJson(handle: i32) -> i32 // pointer to a UTF-8 JSON string |
| 99 | +---- |
| 100 | + |
| 101 | +A typed reader specialised to a known result shape MAY be used instead of |
| 102 | +the JSON accessor where the shape is fixed (AffineScript ADR-013 introduces |
| 103 | +a minimal typed `Response` reader); the JSON accessor remains the general |
| 104 | +fallback and the interop default. |
| 105 | + |
| 106 | +=== Reject / error shape |
| 107 | + |
| 108 | +A rejected/failed settlement is delivered, at the *host-JSON boundary*, as: |
| 109 | + |
| 110 | +---- |
| 111 | +{ "__error": "<message string>" } |
| 112 | +---- |
| 113 | + |
| 114 | +i.e. a JSON object carrying a single `__error` string field. This is the |
| 115 | +shared *boundary* envelope only. Each language maps it to its native error |
| 116 | +type on the guest side: AffineScript to its `Result`/`Option`-shaped reader, |
| 117 | +Ephapax to a sum-type injection (`inr` of its `[tag@0, value@4]` encoding). |
| 118 | +The boundary envelope is fixed; the guest-side mapping is each language's |
| 119 | +own concern and is explicitly *not* constrained here. |
| 120 | + |
| 121 | +=== Once-settle guarantee |
| 122 | + |
| 123 | +A `Thenable` settles *exactly once*. `thenableThen` fires its continuation |
| 124 | +*at most once*. Backends MUST assert this (double-resumption is a host |
| 125 | +contract violation, not a recoverable condition). This guarantee is what |
| 126 | +makes the protocol safe for linear/affine captures in a continuation |
| 127 | +environment: a captured linear value is consumed by exactly one resumption. |
| 128 | +It aligns directly with Ephapax's planned one-shot `resume(once)` |
| 129 | +restriction for linear-capturing handlers. |
| 130 | + |
| 131 | +== Convergence review (Ephapax co-stakeholder, typed-wasm#31) |
| 132 | + |
| 133 | +Reviewed against Ephapax's current `ephapax-wasm` lowering and effect |
| 134 | +system (`ephapax-syntax`/`ephapax-typing`, ADR-007..ADR-010). |
| 135 | + |
| 136 | +[cols="1,1,2", options="header"] |
| 137 | +|=== |
| 138 | +| Protocol element | Ephapax status | Divergence |
| 139 | + |
| 140 | +| Async lowering | None yet (`perform`/`handle` type-checked, emit |
| 141 | + `unreachable`) | None — adoption is purely additive |
| 142 | +| Closure ABI | cell `[table_idx@0, env_ptr@4]`, funcref table, general |
| 143 | + call `(env_ptr, param)->i32` | None — closure *cell* byte-identical to |
| 144 | + AffineScript #199. The async *continuation* call is the no-extra-arg |
| 145 | + form `(env_ptr)->i32` (accessor model); Ephapax's general |
| 146 | + `(env_ptr, param)->i32` is a superset, so the continuation simply uses |
| 147 | + the zero-param-after-env case. No reconciliation required. |
| 148 | +| Once-settle | Planned `resume(once)` for linear captures | None — |
| 149 | + aligned; protocol guarantee is a superset |
| 150 | +| Error shape | Native sum types (`inl`/`inr`, `[tag@0, value@4]`) | |
| 151 | + Reconciled: `{__error}` is the *boundary* envelope; guest-side maps to |
| 152 | + the native sum. No on-the-wire divergence. |
| 153 | +|=== |
| 154 | + |
| 155 | +*Conclusion: no divergence.* Because Ephapax has no async lowering yet, |
| 156 | +there is nothing to conflict with, and the one structural requirement (the |
| 157 | +closure ABI for continuations) already converges byte-identically with what |
| 158 | +Ephapax independently emits. The single representational choice — the |
| 159 | +reject envelope — is settled as a host-boundary convention with per-language |
| 160 | +guest mapping, constraining neither language's error model. |
| 161 | + |
| 162 | +[[conformance]] |
| 163 | +== Conformance — AffineScript (#225) |
| 164 | + |
| 165 | +The marry-up between this protocol and the AffineScript WasmGC backend. |
| 166 | +Each protocol element maps to a concrete implementation site so the two |
| 167 | +repositories can be cross-referenced section-for-section. (Reciprocal |
| 168 | +xref: AffineScript `docs/specs/async-on-wasm-cps.adoc`, ADR-013.) |
| 169 | + |
| 170 | +[cols="2,3,1", options="header"] |
| 171 | +|=== |
| 172 | +| Protocol element (this spec) | AffineScript site | Status |
| 173 | + |
| 174 | +| Thenable handle, sync return (<<_thenable_handle_synchronous_return>>) |
| 175 | + | `stdlib/Http.affine` `http_request_thenable -> Thenable`; transformed |
| 176 | + `Async` fn returns the `thenableThen` result handle |
| 177 | + | ✅ #225 PR 1–2 |
| 178 | + |
| 179 | +| `thenableThen(handle, closure) -> i32` (<<_continuation_registration>>) |
| 180 | + | `stdlib/Http.affine` `thenableThen(t, on_settle: fn(Unit)->Int) -> Int` |
| 181 | + | ✅ #225 PR 2 |
| 182 | + |
| 183 | +| Shared closure cell `[fnId@0, envPtr@4]` via the indirect-call table |
| 184 | + | #199 `ExprLambda` lowering, reused verbatim by the CPS transform |
| 185 | + (`lib/codegen.ml` `gen_async_base_case`); table exported as |
| 186 | + `__indirect_function_table` (root-cause fix, #225 PR 2 — the export |
| 187 | + was absent so the #199 ABI had only ever been static-verified) |
| 188 | + | ✅ #225 PR 2 |
| 189 | + |
| 190 | +| Continuation signature `(env_ptr)->i32`, accessor model |
| 191 | + | continuation is a zero-arg (post-env) `ExprLambda`; the captured |
| 192 | + `Thenable` handle is the sole live local at the async split |
| 193 | + | ✅ #225 PR 2 |
| 194 | + |
| 195 | +| Settled value via `thenableResultJson` / fixed-shape typed reader |
| 196 | + | minimal scalar accessor in PR 2; general typed `Response` reader in |
| 197 | + PR 3 (ADR-013 §Delivery-plan) |
| 198 | + | ◑ PR 2 scalar / PR 3 typed |
| 199 | + |
| 200 | +| `{ "__error": "<msg>" }` boundary envelope |
| 201 | + | host adapter rejects settle as `{__error}`; guest maps to |
| 202 | + `Result`/`Option` |
| 203 | + | ✅ #225 PR 1 |
| 204 | + |
| 205 | +| Once-settle / "Backends MUST assert this" |
| 206 | + | guest-side once-resumption guard global ⇒ `unreachable` trap on a |
| 207 | + second continuation entry (defence-in-depth over host single-fire) |
| 208 | + | ✅ #225 PR 2 |
| 209 | +|=== |
| 210 | + |
| 211 | +== Status |
| 212 | + |
| 213 | +ACCEPTED 2026-05-18 (co-stakeholder sign-off, typed-wasm#31 / PR #32). |
| 214 | + |
| 215 | +AMENDED 2026-05-19 (PR #32, pre-merge): the continuation signature is |
| 216 | +ratified as the *accessor model* `(env_ptr) -> i32` — the earlier |
| 217 | +two-argument `(env_ptr, settled) -> i32` wording is removed as an |
| 218 | +internal ambiguity. This matches the proven #205 re-entry primitive and |
| 219 | +AffineScript #225 PR 2, and does not change the Ephapax conclusion (the |
| 220 | +closure *cell* remains byte-identical; the continuation call is the |
| 221 | +no-extra-arg case of Ephapax's general `(env_ptr, param)->i32`). A |
| 222 | +`<<conformance>>` section was added recording the AffineScript marry-up. |
| 223 | + |
| 224 | +AffineScript side is proven end-to-end (#225 PR 1, merged: Thenable |
| 225 | +foundation + wasm e2e round-trip; PR 2 implements the transform proper |
| 226 | +against this amended signature). Ephapax side: adopt-when-implemented — |
| 227 | +this document is the contract its async lowering must meet (no |
| 228 | +divergence: the closure cell converges byte-identically). AffineScript |
| 229 | +#225 PR 2–4 proceed against this ratified protocol. |
| 230 | + |
| 231 | +== References |
| 232 | + |
| 233 | +* typed-wasm ADR-004 (`.machine_readable/6a2/META.a2ml`) — aggregate / |
| 234 | + convergence role |
| 235 | +* typed-wasm ADR-005 (this protocol; `.machine_readable/6a2/META.a2ml`) |
| 236 | +* typed-wasm#31 — convergence-ABI review issue |
| 237 | +* AffineScript: ADR-013 `docs/specs/async-on-wasm-cps.adoc`; #225 (this |
| 238 | + work), #160 (Http primitive), #199 (closure ABI), #205 (Thenable |
| 239 | + resolution), #226 (Deno-ESM, shipped) |
| 240 | +* Ephapax: `ephapax-wasm` closure codegen; `docs/specs/DESIGN-DECISIONS.adoc` |
| 241 | + ADR-007..ADR-010 (algebraic effects, one-shot continuations) |
0 commit comments