Prototype of the §6.7 substrate route: coeffects as Wasm (component) imports

[inso1337]

Not a bug report — a pointer to an experiment the paper suggests, shared here because the paper repo has issues and discussions disabled. Feel free to close after reading (or convert to a discussion if you enable them).

§6.7 of the paper sketches the substrate route: an embedder that "bounds a component to the dependencies it declares … as a WebAssembly module receives its imports from its embedder at instantiation." I built a small working prototype of exactly that:

https://github.com/inso1337/cordis-wasm — a Python/wasmtime host runtime where:

• a component's coeffect specification d is its Wasm import section (and, in the component-model variant, the WIT interfaces its world imports);
• its provision p is its exports; confinement (Def 48) is the sandbox; the L-Begin gate is the linker refusing to instantiate with unresolved imports;
• the §4.3 lifecycle runs with physical inertia: activation is an exported activate_step() iterator, a Wasm call can't be preempted, so only the landing alternative of L-Divert exists; divert at iteration boundaries gives partial rollback;
• failure follows the paper (Inactive(ξ) withheld until explicit retry) rather than the JS runtime's retry-on-target-change;
• the §6.1 boundary is demonstrated against the real filesystem (acquisitions reverted on unload, emissions surviving, a real FileExistsError routed as L-Raise);
• guests in WAT, AssemblyScript, and Python (componentize-py) run under the unchanged runtime — the "meta-framework, any language" ambition as passing tests.

Each demo asserts specific theorems/definitions from the paper (Thm 63 ordering, LIFO recovery, staged provisions, etc.), so it doubles as a small executable check of the calculus against a substrate the paper only sketches. If any of it is useful as a reference for §6.7 or future work, it's MIT.

🤖 Generated with Claude Code