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
Not a bug report — a pointer to an experiment the paper suggests, shared here because the
paperrepo 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:
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;FileExistsErrorrouted as L-Raise);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