Skip to content

Latest commit

 

History

History
268 lines (230 loc) · 13.3 KB

File metadata and controls

268 lines (230 loc) · 13.3 KB

AffineScript Ecosystem, Spine, and the typed-wasm Contract

Important

This document defines the spine (the macro-stage structure of the language build-out), the actual AffineScript ↔ typed-wasm contract, the satellite registry, and the INT-01..12 integration roadmap. It is authoritative for those four things; for per-feature readiness see CAPABILITY-MATRIX.adoc. Reconstructed 2026-05-19 from issues #128/#135, #175–183, #215, #225, #228, #177, #234, #235 and the hyperpolymath/typed-wasm repo (LEVEL-STATUS v1.5). It supersedes any informally-referenced prior "Stage A–E ledger" — that ledger was cited by multiple issues but was never committed; this is its authoritative materialisation.

The spine

Two distinct things have been called "the spine"; this document keeps them separate.

The implementation spine (compiler files)

The set of compiler modules that the affine discipline is threaded through, end to end. Any change to the affine/borrow/quantity/codegen contract touches all of them in lock-step:

lib/ast.ml, lib/parser.mly, lib/quantity.ml, lib/typecheck.ml, lib/borrow.ml, lib/interp.ml, lib/codegen.ml, lib/codegen_gc.ml, lib/tw_interface.ml, lib/tw_verify.ml, lib/julia_codegen.ml, lib/formatter.ml, lib/json_output.ml, lib/linter.ml, test/e2e/fixtures/, docs/spec.md.

The macro-stage spine (A–E)

The language build-out proceeds in five macro stages. These definitions are established by this document (the prior ledger was never committed).

Stage Scope Status Evidence / exit criterion

A

Core affine spine: QTT semiring wired into the CLI pipeline; affine types + linear arrows enforced; BUG-001..005 closed (Manhattan/Track-A recovery).

CLOSED

affine-types = wired-and-reachable, linear-arrows = enforced in STATE.a2ml; BUG-001..005 closed-bug records.

B

Grammar conformance + conflict elimination: ADR-009 conformance, the #215 conflict-family workstream, ADR-012 ("grammar changes are correctness assertions").

CLOSED

#215 closed with an owner-ratified ADR-012 disposition: families A/C/D/F + the EXTERN bug fixed on correctness grounds (#216/#217/#219/#222/#223); family B (return/resume, #224) shipped as a correctness change, conflict-count-neutral. The residual ~68 S/R + state-401 R/R are intentional WON’T-FIX: Menhir resolves them correctly, the full gate proves every accepted parse is the intended one, and removing them is the systemic precedence/left-factoring contortion (estate-wide blast radius, cosmetic-only payoff) ADR-012 forbids. Closure is by disclosure, not surgery: just build masks the benign notices but prints the count + correctness proof + ADR pointer; just build-loud / dune build reveal all (policy: docs/specs/SETTLED-DECISIONS.adoc "Parser-Conflict Disclosure"). Do not reopen residual-conflict elimination — it is settled won’t-fix.

C

Standard library AOT: every stdlib file compiles resolve→typecheck→codegen, gated in CI.

CLOSED 2026-05-18

19/19 stdlib files; test/test_stdlib_aot.ml; issues #128/#135.

D

Base-language soundness + ecosystem connective tissue: CORE-01 borrow Phase-3 (#177); the INT-01..12 integration roadmap; the satellite registry made real; #228/ADR-014 module-qualified paths (estate port unblocker).

ACTIVE — current frontier

This stage. Substrate = INT-01..04 + CORE-01.

E

typed-wasm convergence hardening (the transition runway): the AffineScript↔typed-wasm contract widened from L7+L10 toward full L1–6/L13–16 emitted-wasm enforcement; estate-wide re-validation (#235); effect-threaded async-boundary recogniser (#234); the #225/#160 convergence ABI matured to "shared with Ephapax".

planned

Begins when D’s substrate (INT-01..04, CORE-01) is closed; ends at a stable, multi-producer typed-wasm convergence ABI.

The transition the mandate refers to — "end of E into typed-wasm" — is not a hand-off into a different project. It is the point at which AffineScript’s emitted typed-wasm satisfies enough of the hyperpolymath/typed-wasm level discipline that the separate typed-wasm verifier accepts AffineScript output on the same footing as the other producers (ephapax). See the contract below.

The actual AffineScript ↔ typed-wasm contract

Important

typed-wasm is a separate, language-agnostic compilation target with its own repository (hyperpolymath/typed-wasm), its own Idris2 proofs, its own ReScript surface, its own Rust verifier crate, and its own other producers (notably hyperpolymath/ephapax). AffineScript compiles to plain WASM, typed-wasm, Deno-ESM, and ~22 other targets; typed-wasm is one of them. Multiple languages target typed-wasm. These are meaningfully separated and must stay so. Do not collapse "AffineScript" and "typed-wasm" in any doc.

The contract is narrower than older prose claimed and is exactly this:

  1. Carrier. AffineScript emits ordinary WASM/WASM-GC. The typed-wasm discipline rides on it via the affinescript.ownership custom section (per-function param ownership kinds: 0=Unrestricted, 1=Linear, 2=SharedBorrow, 3=ExclBorrow) plus the affinescript.tea_layout section where a TEA bridge is involved.

  2. Producer side (in this repo). lib/codegen.ml (QTT pass) enforces the discipline on the source; lib/tw_interface.ml performs cross-module boundary verification (verify-boundary CALLEE CALLER, LinearImportCalledMultiple, LinearImportDroppedOnSomePath); lib/tw_verify.ml re-checks the emitted module post-codegen.

  3. Spec / verifier side (separate repo). hyperpolymath/typed-wasm v1.5 carries the L1–L16 Idris2 proofs and crates/typed-wasm-verify (Rust), a faithful port of the OCaml reference here. The OCaml files remain the spec of record until the cross-compat suite is supplemented with real AffineScript-emitted fixtures (typed-wasm "C5.1", deferred).

  4. Coverage today. Emitted-wasm enforcement is Level 7 (aliasing)
    Level 10 (linearity)
    , plus Level 13 (module isolation, negative form)Tw_verify.verify_module_isolation rejects a module that owns linear memory yet also imports a memory/table (carrier-free; no ownership-section ABI change). L1–6, L14–16 (region schema, session protocols, resource capabilities, agent choreography) remain proven at the spec level but not enforced on AffineScript-emitted wasm: they require a new carrier section (region/type-schema or capability data), which is a multi-producer ABI change coordinated with hyperpolymath/typed-wasm + ephapax — not made unilaterally here. Further widening + INT-12 is the rest of Stage E.

  5. Other producers. ephapax (src/ephapax-wasm) already emits the same affinescript.ownership section and exposes the verifier via ephapax compile --verify-ownership. Any change to the section format is a multi-producer ABI change and must be coordinated with typed-wasm (Refs the typed-wasm repo), not made unilaterally here.

Satellite registry (truthed)

Satellite Reality Notes

affinescript-dom

reconciler (compiles)

INT-08 (#183): src/dom.as (non-parsing 39-line stub) renamed to canonical src/dom.affine and replaced with a real VDOM + render + mount + minimal-mutation reconciler that compiles end-to-end. Runtime gated on #255 (pre-existing wasm loop-codegen defect).

affinescript-pixijs

skeleton

Migration-prerequisite scaffold (#56).

affinescript-vite

scaffold

Build-tool integration shell.

affinescript-deno-test

works

Smoke-test harness used by the Deno-ESM target.

affinescript-tea

runtime

INT-07 (#182): real host-side TEA runtime + run loop (TeaApp: load/init/dispatch/model/setScreen/run, parseTeaLayout). Generic over affinescript.tea_layout; enforces the Linear-msg invariant; reuses the INT-02 loader. 9 Deno tests vs the canonical affinescript tea-bridge + a re-entrancy fixture.

affinescript-dom-loader

scaffold

Was imaginary until #175. INT-02 (#179) builds the host-agnostic loader. Blocks INT-05/08/11.

affinescript-cadre

scaffold

Was imaginary until #175. Router/navigation satellite (internal lib/tea_router.ml contract exists).

affinescriptiser, road-skate

adjunct

In-tree tooling/experiments; not part of the integration critical path.

packages/affine-js / -ts / -res / -vscode

works

affine-js SAT-02 fixed by INT-02 (#179): host-agnostic loader (loader.js) — Deno/Node/browser parity, multi-namespace import object, affinescript.ownership accessor.

Integration roadmap — INT-01..12

Critical path: INT-01..INT-04 are substrate and block most satellites. Filed sub-issues are children of #175; severity/blocked-by also in TECH-DEBT.adoc.

ID Item Issue Status

INT-01

Cross-module WASM import emission (the substrate)

#178

use Mod::{fn}/::* PROVEN+locked (deno link harness); use Mod;/as + Mod.fn(x) qualified-value path WIRED+locked (parse-boundary lowering; 4 hermetic tests). Distinct parser follow-up: Mod::fn(x) in expr position

INT-02

Host-agnostic loader bridge (affinescript-dom-loader)

#179

loader in packages/affine-js (SAT-02 fixed; Deno/Node/browser parity, multi-namespace import object, ownership-section accessor). PROVEN
regression-locked:
14 unit tests via pinned deno task test (was flag-fragile — no run task) + tests/modules/loader-bridge/ drives the real loader API over genuine compiler-emitted cross-module wasm (readBytes+buildImportObject link CrossCallee.consume(42)=42; parseOwnershipSection reads a real Linear-param entry) — closes INT-01 ↔ INT-02. S1; unblocks INT-05/08/11. The affinescript-dom-loader satellite shell is downstream.

INT-03

WASI preview2 / host I/O beyond stdout

#180

S1, ADR-015 ACCEPTED (owner-chosen full WASM Component-Model re-target). Staged S1..S6; legacy preview1 stdout path is the default until S6 (reversible-in-progress). S2 toolchain provisioned (#251). S3 DONE: tools/componentize.sh wraps the emitted core module into a valid WASI-0.2 component via the fetch-pinned preview1→preview2 reactor adapter (wasmtime v44.0.1, sha256-verified); the affinescript.ownership section is proven to SURVIVE the wrap; tests/componentize/smoke.sh gates it (SKIP-safe without the toolchain). Codegen UNCHANGED — core preview1 stays the default (reversible). S4a (clock) + S4b (env_count, arg_count) DONE: builtins lower to on-demand wasi_snapshot_preview1.* imports (Effect_sites pre-scan, canonical-order indexing through ctx.wasi_func_indices; zero impact on units that don’t use them; verified with a multi-import combo regression). Component path bridges to wasi:clocks/wasi:cli. Real-host main-invoke deferred to S6 (WIT export-lifting / wasi:cli/run command shape). String accessors (env_at/arg_at) gated on a byte-level wasm-IR extension (I32Load8U/I32Store8 absent today) — tracked as the next slice before/with S5 filesystem. WIT world of record: wit/affinescript.wit

INT-04

Publish compiler + runtime to JSR (then npm)

#181

runtime packaging READY (affine-js + affinescript-tea JSR dry-run green; manual-only publish-jsr.yml; docs/PACKAGING.adoc). INT-01 dep cleared. NOT published (owner-gated: needs explicit go + JSR/npm auth). Compiler-binary distribution = design fork #260

INT-05

Loader-driven multi-module app bundling

ledger-only

planned (blocked by INT-02)

INT-06

Server-side runtime profile (on INT-03 WASI p2)

ledger-only

planned (blocked by INT-03)

INT-07

affinescript-tea runtime satellite

#182

runtime + run loop shipped (TeaApp/parseTeaLayout, Linear-msg enforced); INT-01 dep cleared (#253). Router/nav = separate INT-09

INT-08

DOM reconciler in affinescript-dom

#183

reconciler implemented + compiles (resolve→typecheck→codegen→wasm); .as.affine corrected. INT-02 dep cleared. Runtime BLOCKED by #255 (wasm loop-codegen defect, pre-existing)

INT-09

affinescript-cadre router/navigation runtime

ledger-only

planned (blocked by INT-07)

INT-10

LSP distribution (affinescript-lsp)

#282

unblocked — distribution decided (ADR-019: Releases + thin Deno/JSR shim, #260). Consumes the shim once #260 S2/S3 land

INT-11

Browser host parity (DOM loader + reconciler end-to-end)

ledger-only

planned (blocked by INT-02/08)

INT-12

typed-wasm convergence: AffineScript-emitted fixtures into the typed-wasm cross-compat suite (closes the Stage-E runway)

ledger-only

planned (Stage E; coordinates with hyperpolymath/typed-wasm C5.1)

INT-05/06/09/10/11/12 are ledger-only (defined here, not yet filed as issues) by deliberate choice: they are unblocked only after their substrate lands, and filing them now would create stale critical-path noise. They are filed when their blocker closes.

See also

  • CAPABILITY-MATRIX.adoc — authoritative per-feature readiness.

  • TECH-DEBT.adoc — the coordination ledger.

  • RESCRIPT-ELIMINATION.adoc — the estate ReScript-surface elimination ledger (#229), the spine’s estate-port arm.

  • hyperpolymath/typed-wasm LEVEL-STATUS.md — the target spec & proofs.

  • hyperpolymath/ephapax — the other typed-wasm producer.