META.a2ml

# SPDX-License-Identifier: PMPL-1.0-or-later
# META.a2ml — Project meta-information
# Converted from META.scm on 2026-03-21

[metadata]
project = "affinescript"
author = "Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"
license = "PMPL-1.0-or-later"
standard = "RSR 2026"

# ──────────────────────────────────────────────────────────────────────────────
# Architecture Decision Records
# ──────────────────────────────────────────────────────────────────────────────
# ADRs are numbered sequentially and never renumbered. Superseded ADRs remain
# in place with status = "superseded" and a pointer to the replacement.
# Added 2026-04-10 during Track F1 (Idris2 Solo-core formalisation) — the
# formal-verification track surfaced three decisions about the QTT type system
# that were previously implicit.

[[adr]]
id = "ADR-001"
status = "accepted"
date = "2026-04-10"
title = "Split-Γ is the canonical presentation of the QTT type system"
context = """
The Idris2 Solo-core formalisation (docs/academic/formal-verification/solo-core/)
revealed that docs/spec.md §3.6 presents typing rules against a shared Γ
(writing e.g. T-App with both premises typed under the same Γ), while
lib/quantity.ml runs a post-hoc usage walk that accumulates per-variable
usage summed across subterms. The literature-standard QTT presentation
(Atkey 2018, Granule, Idris2 core) uses explicit context splitting
  Γ = Γ₁ + q·Γ₂
at every eliminator position.

Both forms are extensionally equivalent for the Solo core (same programs
accepted/rejected). The difference is purely presentational.
"""
decision = """
Split-Γ is canonical. The spec, the formalisation, and all future
documentation present typing rules in split-Γ form. The post-hoc usage walk
in lib/quantity.ml is an equivalent implementation strategy, documented as
such in a comment, not the definition of the type system.
"""
consequences = """
- docs/spec.md §3.6 is rewritten to show explicit context splitting (~30-60 LOC).
- lib/quantity.ml gets a header comment explaining that its flat walk is an
  equivalent implementation of the split-Γ rules, with a pointer to this ADR.
- The Idris2 formalisation's Typing.idr (which uses split-Γ) becomes the
  mechanised witness of the spec — no translation layer required.
- Progress + preservation proofs can proceed in textbook form.
- Dependability gain: one source of truth. The spec-vs-impl gap (the failure
  mode flagged in Track B's audit of TYPECHECKER-COMPLETION.md) cannot
  structurally hide in this part of the system.
- Interop gain: the spec becomes citable and legible to anyone with QTT
  background (Atkey, Idris2, Granule, Quill readers).
- Reader-tax cost: split-Γ notation is heavier than shared-Γ for newcomers.
  Mitigated by surface-language tutorials keeping informal shared-Γ intuition
  while the spec remains the formal reference.
"""

[[adr]]
id = "ADR-002"
status = "accepted"
date = "2026-04-10"
title = "Let rule scales value context by binder quantity (QTT-orthodox)"
context = """
During the Decision-2 audit of docs/spec.md T-Let against lib/typecheck.ml
and lib/quantity.ml, the current implementation was found to handle Let
unsoundly:

- lib/typecheck.ml:631-665 (ExprLet) does zero quantity handling — pure
  HM-style inference with let-generalisation, quantities entirely absent.
- lib/quantity.ml:251-253 (ExprLet in infer_usage_expr) does a flat walk
  that sums e1's and e2's usages without scaling e1 by the binder's quantity.

This is equivalent to the rule
  Γ₁ ⊢ e1 : A    (Γ₂, x:A) ⊢ e2 : B
  ─────────────────────────────────
            Γ₁ + Γ₂ ⊢ let x = e1 in e2 : B
rather than the QTT-orthodox
  Γ₁ ⊢ e1 : A    (Γ₂, x:^q A) ⊢ e2 : B
  ─────────────────────────────────────
         q·Γ₁ + Γ₂ ⊢ let x :^q = e1 in e2 : B

Two concrete soundness bugs follow:

BUG-001 (high severity — linear-value smuggling):
  let x :ω = linear_resource() in use_x_once(x)
  Current impl accepts; QTT-correct form rejects (e1's Γ must be scaled by
  ω, so any Γ₁ containing a linear variable becomes ill-formed).

BUG-002 (medium severity — erasure failure):
  let x :0 = expensive_proof_term() in body_not_using_x
  Current impl evaluates e1 and consumes its resources; QTT-correct form
  scales e1's Γ by 0, producing the zero context, which means e1 can be
  erased at runtime.

BUG-001 is a soundness hole that defeats the point of affine types in any
program where ω-binders and linear values coexist.
"""
decision = """
The Let rule in both the spec and the implementation scales the value
context by the binder's quantity. T-Let becomes:

  Γ₁ ⊢ e1 : A    (Γ₂, x:^q A) ⊢ e2 : B
  ─────────────────────────────────────
         q·Γ₁ + Γ₂ ⊢ let x :^q = e1 in e2 : B

Unannotated Let defaults to q = ω (matching current behaviour for all
existing unannotated code — so the fix is non-breaking for the common case).
"""
consequences = """
- lib/quantity.ml ExprLet case grows a scale-by-q step before summing
  into the outer context (~10 LOC).
- lib/typecheck.ml ExprLet case threads quantities (folded into Track A3
  which is already rewriting quantity flow through typecheck.ml).
- docs/spec.md T-Let rule is rewritten to show the scaling explicitly.
- Two regression tests added as Track A2 fixtures covering BUG-001 and
  BUG-002.
- The Idris2 formalisation (Typing.idr THLet) already assumes the scaled
  form — no rework there.
- Users who had previously (accidentally) relied on the unsound behaviour
  to duplicate linear values through ω-lets will now get a compile error.
  Expected blast radius: near-zero because affine enforcement was never
  wired in the first place (see ADR-001 rationale).
"""

[[adr]]
id = "ADR-003"
status = "accepted"
date = "2026-04-10"
title = "Evaluation order is strict CBV, left-to-right, for all n-ary forms"
context = """
During the Decision-3 audit of lib/interp.ml for the Track F1 Step relation,
the evaluator was found to be internally inconsistent about evaluation order
of n-ary expression forms.

- ExprBinary (lib/interp.ml:135-138) is explicitly left-to-right:
    let* left_val = eval env left in
    let* right_val = eval env right in
    eval_binop op left_val right_val
- ExprApp args (:130), ExprTuple (:144), ExprArray (:148) all delegate to
  eval_list, which is implemented with List.fold_right:
    and eval_list env exprs =
      List.fold_right (fun expr acc ->
        let* vals = acc in
        let* v = eval env expr in
        Ok (v :: vals)
      ) exprs (Ok [])
  OCaml is strict, so in f (fold_right f [a;b;c] init) the innermost
  application runs first — eval env c is forced before eval env b before
  eval env a. Net result: right-to-left.

This was almost certainly unintentional; nothing currently depends on the
order because affine enforcement was never wired. However:

- The WASM and Julia backends will naturally generate left-to-right code,
  producing cross-backend semantic divergence for any program with effectful
  or resource-consuming arguments.
- The effect system (70% complete per STATE.a2ml) would observe handler
  ordering tied to evaluation order, making this a latent soundness hazard.
- A Track F1 Step relation defined in textbook CBV left-to-right form would
  disagree with the interpreter, requiring a non-standard right-to-left
  presentation or a proof of order-independence (which is false in general
  for effectful languages).
"""
decision = """
All n-ary expression forms evaluate their subterms strict left-to-right.
This applies to: application arguments, tuples, arrays, record fields,
function calls in all positions.

lib/interp.ml eval_list is fixed to left-to-right:
  and eval_list env exprs =
    let rec loop acc = function
      | [] -> Ok (List.rev acc)
      | e :: rest ->
        let* v = eval env e in
        loop (v :: acc) rest
    in
    loop [] exprs

Track F1's Step relation uses the standard CBV left-to-right presentation
  e1 → e1'  ⟹  e1 e2 → e1' e2       (reduce function first)
  e2 → e2'  ⟹  v1 e2 → v1 e2'       (then argument, only once function is a value)
with the symmetric congruences for pairs, tuples, etc.
"""
consequences = """
- lib/interp.ml eval_list is replaced (~6 LOC diff).
- docs/spec.md gains (or receives an edit to) an explicit operational
  semantics section stating strict CBV, left-to-right.
- A regression test lands in Track A2 exercising a program whose output
  depends on left-to-right evaluation (e.g. a tuple of two side-effecting
  calls that mutate a shared counter).
- WASM, Julia, and the effect system all become consistent with the
  interpreter by default — no backend fix required.
- Track F1 can proceed on its current footing to mechanise Step and the
  progress/preservation proofs without author input.
- Existing programs are unaffected unless they rely on observable right-
  to-left evaluation of tuple/arg components. The interpreter is the only
  place that did this, and nobody has filed a bug, so blast radius is
  expected to be zero.
"""

[[adr]]
id = "ADR-007"
status = "accepted"
date = "2026-04-10"
accepted = "2026-04-10"
title = "Surface syntax for quantity annotations: @linear/@erased/@unrestricted (primary) + :1/:0/:ω (sugar)"
context = """
The Track A audit on 2026-04-10 found that affine enforcement is wired
through the CLI (Quantity.check_program_quantities runs from
lib/typecheck.ml:1206 on every check/compile/eval invocation) but
**unreachable** from user programs because the surface syntax for declaring
quantity annotations on let-binders does not exist. Specifically:

- lib/ast.ml ExprLet and StmtLet have no quantity field. They carry
  el_mut/sl_mut, el_pat/sl_pat, el_ty/sl_ty, el_value/sl_value, el_body
  — no el_quantity. Only function `param` and `type_param` carry
  `p_quantity`/`tp_quantity`.
- lib/lexer.ml never emits ZERO/ONE tokens. Source `0` and `1` are lexed
  as `INT 0`/`INT 1`. The only quantity literal that round-trips through
  source today is `omega`/`ω` (lexer.ml:53 and lexer.ml:153 respectively).
- lib/parser.mly's `quantity` rule (lines 180-183) takes ZERO|ONE|OMEGA
  but only OMEGA is reachable from source. Even on function parameters,
  `:1` and `:0` annotations cannot be written.
- ADR-002 specifies the QTT-orthodox scaled Let rule (q·Γ₁ + Γ₂), which
  requires the binder to carry a quantity. Without surface syntax to
  attach one, the rule has no input to scale by, BUG-001 cannot be
  closed, and the headline affine-types feature remains theatre.

Surface syntax is a language-design decision, not an implementation
detail. The decision needs author input before any of items 1-6 in
[track-a-manhattan] proceed.
"""
options = """
Three candidate surface syntaxes are listed. None has been chosen.

# Option A — caret-quantity suffix on `let` keyword

  let^1 x = linear_resource() in use_x_once(x)
  let^0 _proof = expensive_term() in body
  let^ω y = pure_int() in use_y_many(y)

  Pros:
  - Visually parallel to T-Let's `let x :^q A` notation in QTT papers.
  - The `^` is currently unused in the lexer, so no disambiguation cost.
  - The annotation lives on the keyword, not the binder, which mirrors
    the type-theory framing where `q` parameterises the rule, not the
    variable.
  - Easy parser rule: LET (CARET quantity)? pat (COLON ty)? EQ value.

  Cons:
  - `^` is unfamiliar surface syntax for users coming from Rust/Idris2.
  - The `^` may collide with future bitwise-XOR or pow operators
    (currently OpBitXor exists in ast.ml but the lexer surface form is
    unclear).
  - Requires users to type a non-letter character on every annotation.

# Option B — colon-quantity prefix on the type ascription

  let x :1 :Int = linear_resource()
  let x :0 :Int = expensive_term()
  let x :ω :Int = pure_int()
  let x :1 = linear_resource()              # type inferred

  Pros:
  - Reuses the existing COLON token; no new operators needed.
  - Mirrors the function parameter syntax, which already accepts
    `qty? own? name COLON ty` (parser.mly:186).
  - Familiar to readers of Idris2 (`x : 1 A`) and Quantitative Type
    Theory papers.

  Cons:
  - Two consecutive colons looks awkward and may confuse readers
    expecting `::` (the path separator COLONCOLON token).
  - When the type is inferred (`let x :1 = e`), the parser needs
    one-token lookahead to distinguish `:1` (quantity) from `:Int`
    (type). This is a minor parser challenge but non-zero.
  - The lexer must additionally route `INT 0`/`INT 1` to ZERO/ONE in
    quantity position, which is context-sensitive lexing — best handled
    by accepting `INT 0|INT 1` directly in the parser's quantity rule
    instead, but that introduces a small grammar wart.

# Option C — annotation-style attribute before `let`

  @linear let x = linear_resource() in use_x_once(x)
  @erased let _proof = expensive_term() in body
  @unrestricted let y = pure_int() in use_y_many(y)
  let z = pure_int() in use_z(z)            # default = unrestricted

  Pros:
  - Reads naturally; `@linear` and `@erased` are self-documenting and
    require no quantity-theory background.
  - Trivially extensible to future modal annotations (e.g. `@borrowed`,
    `@owned`) without grammar changes.
  - Parser change is local: AT (ident) LET pat (COLON ty)? EQ value.
    No COLON disambiguation, no new operator tokens.
  - Aligns with the language-policy preference for descriptive names
    over symbolic ones (CLAUDE.md: "Always use descriptive variable
    names"; the same instinct applied to annotations).

  Cons:
  - Verbose. `@linear let x = ...` is six tokens vs `let^1 x = ...`'s
    four.
  - Diverges from the QTT mathematical notation, making it harder for
    paper-trained readers to map source to spec. Mitigation: spec.md
    can show both forms in parallel.
  - The `@` token is currently unused, so it's free, but introducing
    it for one feature creates pressure to use it for others (which
    may or may not be desirable depending on language direction).
  - Requires a small mapping table from attribute name to quantity
    value (`linear → QOne`, `erased → QZero`, `unrestricted → QOmega`).
"""
decision = """
Hybrid: Option C accepted as primary, Option B accepted as sugar.

Both surface syntaxes parse to the same internal representation.
Tutorials, error messages, IDE tooling, and the spec's prose all use
Option C. Option B remains legal for users porting from QTT papers or
who prefer the compact form. Option A is rejected outright.

# Primary surface form (Option C — what tutorials and error messages use)

  @linear        — used exactly once (QOne)
  @erased        — must not be used at runtime (QZero)
  @unrestricted  — any number of uses (QOmega), the default

Examples:
  @linear let x = linear_resource() in use_x_once(x)
  @erased let _proof = expensive_term() in body_not_using_proof
  @unrestricted let y = pure_int() in use_y_many(y)
  let z = pure_int() in use_z(z)            # default: @unrestricted

  fn consume(@linear x: Resource) -> Unit = release(x)
  fn weigh(@erased _proof: Even(n), n: Nat) -> Nat = n / 2

# Sugar surface form (Option B — accepted but not promoted)

  let x :1 :Resource = linear_resource() in use_x_once(x)
  let _proof :0 :Even(n) = expensive_term() in body
  let y :ω :Int = pure_int() in use_y_many(y)
  let z :Int = pure_int() in use_z(z)       # no quantity = @unrestricted

  fn consume(x :1: Resource) -> Unit = release(x)
  fn weigh(_proof :0: Even(n), n: Nat) -> Nat = n / 2

# Equivalence

  @linear        ≡  :1
  @erased        ≡  :0
  @unrestricted  ≡  :ω    (also: omitted entirely)

Both forms parse to the same `el_quantity = Some QOne | QZero | QOmega`
in lib/ast.ml. The compiler chooses the canonical form (Option C) when
emitting diagnostics, formatter output, and pretty-printed source. The
formatter rewrites Option B to Option C on `affinescript fmt`, with an
opt-out flag `--keep-quantity-sugar` for users who deliberately prefer
the compact form.

Rationale (decided per the standing priority order
dependability > security > interop > usability/accessibility/marketability
> performance > versatility > functional extension):

- Usability/accessibility/marketability beats consistency-with-papers
  in the priority order, so Option C must be the primary form a new
  user encounters in tutorials and error messages. A new user reading
  `@linear let x = e` can form a working hypothesis without consulting
  the spec. The same user looking at `let x :1 = e` has nothing to
  Google.
- However, the priority order does not require *exclusivity*. Accepting
  Option B as sugar costs ~15 LOC of parser surface area and one
  paragraph in the spec, and in return it:
  * Preserves consistency with the existing function-parameter syntax
    (which uses `qty? own? name COLON ty`), so the param-quantity gap
    closes with the *same* grammar production rather than a parallel
    one. Users learning the param syntax already see `:1` in the
    grammar; the sugar makes that knowledge transfer to let-binders.
  * Preserves citation isomorphism with QTT papers — anyone porting an
    Idris2 example or a Granule example can paste the numeric form
    directly without rewriting it.
  * Gives advanced users a denser form for code where annotations are
    frequent and English keywords would create visual noise.
- Compiler errors and source code share the C vocabulary regardless of
  which form the user wrote: "`@linear` binding 'x' used 2 times" reads
  cleanly without mental translation, even if the source was written
  as `:1`. The diagnostic always speaks the canonical form.
- Tutorials can be example-driven from the first runnable program with
  Option C; the QTT semiring and Option B sugar become optional
  advanced reading rather than a prerequisite for "hello world with
  affine types."
- The `@` namespace is now committed to AffineScript and may grow to
  cover additional modal annotations (e.g. `@total`, `@pure`,
  `@borrowed`, `@owned`) in future ADRs. This is an intentional
  reservation, not a side effect.
- The Rust/Linear-Haskell precedent is real: Rust ships affine
  semantics under approachable keywords and reaches a vastly larger
  audience than Linear Haskell, which exposes the type-theory
  machinery directly. AffineScript chooses Rust's marketing instinct
  for the primary form, while keeping Linear Haskell's notation
  available for users who already think in it.

# Style guide commitment

The spec commits explicitly to keeping both forms supported. Future
contributors proposing to drop Option B sugar must amend this ADR
rather than removing it silently. The recommended convention in
published AffineScript code is:

- New code: Option C (`@linear let x = e`).
- Code accompanying a paper: either form, author's choice.
- Auto-formatted code: Option C (formatter rewrites unless
  `--keep-quantity-sugar` is set).
- Generated code (compiler diagnostics, IDE quick-fixes, refactoring
  tools): Option C exclusively.

Rejected alternatives:

- Option A (`let^q x = e`): rejected. Lowest implementation cost but
  worst on the priority order — symbolic, opaque to non-TT readers,
  forecloses future use of `^` for bitwise XOR or exponentiation.
- Option B exclusively (without C): rejected for the same
  accessibility/adoption reasons that make C the primary form.
- Option C exclusively (without B sugar): considered and rejected. The
  marginal cost of accepting B is low (~15 LOC parser, one paragraph
  spec), and the benefit — closing the param-quantity gap with one
  grammar production and preserving paper-citation isomorphism — is
  worth the cost given the standing priority order's high weighting
  of interop alongside accessibility.
"""
consequences = """
- lib/ast.ml gains el_quantity / sl_quantity fields on ExprLet and
  StmtLet. ~10 modules pattern-matching on Let must be updated
  mechanically (typecheck, interp, codegen, codegen_gc, julia_codegen,
  formatter, sexpr_dump, json_output, linter, opt, desugar_traits).
- lib/lexer.ml gains an AT token for `@`. ~2 LOC.
- lib/token.ml gains the AT token kind. ~2 LOC.
- lib/parser.mly gains:
  * AT ident — a quantity_attr rule that maps `@linear`/`@erased`/
    `@unrestricted` to QOne/QZero/QOmega and rejects unknown attribute
    names with a parse error pointing at the documented set.
  * Optional quantity_attr prefix on let_decl, stmt_let, param, and
    lambda_param productions. ~15 LOC.
  * The existing numeric quantity rule (ZERO|ONE|OMEGA) gains INT 0
    and INT 1 as accepted lexemes (since the lexer emits INT not
    ZERO/ONE for `0` and `1`). This makes Option B sugar reachable
    from source on let-binders and params, in addition to type_params
    where it already worked. ~5 LOC.
  * Both productions resolve to the same el_quantity / sl_quantity /
    p_quantity slot — they are alternative concrete syntaxes for the
    identical abstract syntax.
- lib/quantity.ml ExprLet/StmtLet cases gain context scaling per
  ADR-002. ~25 LOC including a `scale_usage_by` helper.
- Error messages in lib/quantity.ml format_quantity_error are updated
  to use `@linear` / `@erased` / `@unrestricted` vocabulary instead of
  the show_quantity numeric forms.
- Regression fixtures land covering BOTH surface forms:
  * test/e2e/fixtures/bug_001_omega_let_smuggles_linear.affine — must
    be rejected (Option C form: `@unrestricted let x = ...`).
  * test/e2e/fixtures/bug_001_sugar_form.affine — must be rejected
    (Option B form: `let x :ω = ...`). Proves both surface forms are
    enforced through the same code path.
  * test/e2e/fixtures/affine_let_valid.affine — must pass (Option C).
  * test/e2e/fixtures/affine_let_valid_sugar.affine — must pass
    (Option B).
- docs/spec.md T-Let rule is rewritten to show the formal QTT notation
  alongside both surface forms (Option C primary, Option B sugar) so
  paper-trained readers and pedagogy-first readers both see their
  preferred presentation.
- docs/spec.md gains a "Surface syntax for quantity annotations"
  section documenting the equivalence table and the style-guide
  commitment from this ADR.
- BUG-002 (`:0` lets do not erase their RHS) closes in the same change,
  per ADR-002's consequence list.
- The affine-types feature flag in STATE.a2ml [features] flips from
  `wired-but-unreachable` to `wired-and-reachable` once the change
  lands.
- Future modal annotations (`@total`, `@pure`, `@borrowed`, `@owned`,
  etc.) inherit the same `@`-attribute parsing infrastructure for free.
- The formatter (lib/formatter.ml) gains a `--keep-quantity-sugar` flag
  that defaults to OFF (so default `affinescript fmt` rewrites Option
  B sugar to Option C primary). Users opting in retain their chosen
  form across format passes.
"""
references = [
  ".machine_readable/6a2/STATE.a2ml [track-a-manhattan]",
  ".machine_readable/6a2/STATE.a2ml [[open-bug]] BUG-001",
  ".machine_readable/6a2/STATE.a2ml [[open-bug]] BUG-002",
  ".machine_readable/6a2/META.a2ml [[adr]] ADR-002 (scaled Let rule)",
  "lib/ast.ml ExprLet (lines 105-111), StmtLet (lines 170-176)",
  "lib/lexer.ml (ZERO/ONE never emitted)",
  "lib/parser.mly quantity rule (lines 180-183)",
]

[[adr]]
id = "ADR-008"
status = "accepted"
date = "2026-04-11"
title = "Effect invocation uses direct call syntax — no 'perform' keyword"
context = """
Algebraic effects require a syntax for invoking an effect operation at a
call site. Two candidates exist in the literature:

1. Direct call: `Http.get(url)` — the effect operation looks like a
   namespaced function call. The effect is declared in the return type
   annotation (`-> T / Http, Async`) not at each call site.

2. Explicit perform: `perform Http.get(url)` — the keyword makes the
   effectful nature of the call visible at every use site. Used by Koka
   (earlier versions) and some effect-system research languages.

The AffineScript DESIGN-VISION.adoc already shows direct call style in its
effect examples. The decision needed to be made explicit so the conformance
suite, parser, and documentation are unambiguous.
"""
decision = """
Effect operations are invoked with direct call syntax. No `perform` keyword.

  fn fetch_user(id: Int) -> User / Http, Async {
    let resp = Http.get("/users/" ++ show(id))
    Async.await(resp.json())
  }

The effect is declared once — in the return type annotation (`/ Http, Async`).
The call sites are plain calls. The type signature is the contract; the call
site is just a call.
"""
consequences = """
- The conformance suite, parser, and spec must not admit or require `perform`.
- Effect operation calls are syntactically indistinguishable from regular
  function calls; the distinction is entirely in the type system.
- Error messages for unhandled effects reference the return type annotation,
  not a `perform` site.
- This is consistent with the ergonomics goal: effect-heavy code does not
  accumulate keyword noise at every call site.
- Face parsers (Python-face, JS-face) can map `async/await` to the Async
  effect without introducing a `perform` concept — `await` desugars to
  `Async.await(...)`, which is a direct call.
"""
references = [
  "docs/DESIGN-VISION.adoc (effect examples)",
  "docs/specs/effects.md",
]

[[adr]]
id = "ADR-009"
status = "accepted"
date = "2026-04-11"
title = "The conformance suite is authoritative — parser must conform to spec"
context = """
The conformance suite (test/conformance/) contains valid AffineScript programs
drawn from the spec. As of 2026-04-11, 8 of 12 valid conformance tests fail
to parse. The three categories of failure are:

1. Uppercase type names — `Int`, `String`, `Bool`, `Option` are written in
   the spec with PascalCase. The parser's `ident` rule accepts only lowercase,
   so `Int` fails to parse as a type name.

2. ML-style enum syntax — the spec's enum declaration syntax does not match
   what the parser accepts.

3. Effect op type parameters — the spec includes type parameters on effect
   operations; the parser does not support them.

Two possible authorities: the spec (conformance suite) or the parser
(current implementation).
"""
decision = """
The spec is authoritative. The parser must conform to the spec. This is
consistent with the standing estate-wide rule: 'Language scope lives in a
written thesis. Thesis authoritative, code must conform. If disagreement,
code is wrong.'

Specific required changes:
1. Parser must accept PascalCase type names (`Int`, `String`, `Bool`, user-
   defined types). The type name namespace is PascalCase; value names remain
   camelCase/snake_case. This also fixes the conformance suite failure where
   effect and enum type names could not be written.
2. Parser must accept the spec's enum declaration syntax (to be confirmed
   against spec and fixed accordingly).
3. Parser must support type parameters on effect operations.

The target is 12/12 conformance suite passing.
"""
consequences = """
- lib/lexer.ml and lib/parser.mly are updated to accept PascalCase type names.
- The `ident` vs `type_ident` distinction is formalised in the grammar:
  `ident` = lowercase-leading (values, variables, functions)
  `type_ident` = uppercase-leading (types, effects, enums, type aliases)
- lib/parser.mly enum and effect rules are audited against spec and fixed.
- 12/12 conformance tests pass. The conformance suite becomes a live
  regression suite — any future parser change that breaks a conformance test
  is a bug, not a spec disagreement.
- All fixture files under test/e2e/fixtures/ that use lowercase type names
  (e.g. `type point = ...`) are reviewed; lowercase type aliases remain valid
  (they are value-level names) but builtin types (`int` written lowercase)
  are normalised to PascalCase.
- Error messages and diagnostics use PascalCase type names consistently.
"""
references = [
  "test/conformance/",
  "lib/lexer.ml",
  "lib/parser.mly",
  "docs/spec.md",
]

[[adr]]
id = "ADR-010"
status = "accepted"
date = "2026-04-11"
title = "Face-aware error formatting is a first-class toolchain concern"
context = """
AffineScript supports syntactic face layers (Python-face, JS-face,
pseudocode-face, canonical AffineScript) that allow developers to write
AffineScript using familiar surface syntax from other languages. The compiler
pipeline forks only at the parser; everything downstream (type checker,
codegen) is shared and operates on the canonical AST.

Without face-aware error formatting, a developer writing Python-face
AffineScript receives type errors expressed in canonical AffineScript
syntax — terms and constructs they have deliberately not learned yet. This
shatters the face illusion at the worst possible moment (when the developer
is stuck and needs help) and is a direct contradiction of the adoption goal.
"""
decision = """
Face-aware error formatting is a first-class toolchain concern, not an
afterthought. It is implemented as a formatting layer between the compiler
and the terminal, not inside the compiler itself.

Architecture:
  compiler (emits errors in canonical AST terms)
      ↓
  face-aware error formatter   ← separate concern, swappable
      ↓
  terminal / IDE / LSP

The compiler's error representation is canonical and face-agnostic. The
formatter receives: (error, active-face) → formatted error string.

Each face provides an error vocabulary mapping:
  canonical term → face term
  e.g. (python-face) "affine binding" → "single-use variable"
  e.g. (js-face) "Option[T]" → "T | null"  [with note: 'use .unwrap_or()']

Error source spans are always reported in the face's syntax, not canonical
AffineScript syntax, since the user's file is written in the face.
"""
consequences = """
- The compiler's error types carry enough information for the formatter to
  reconstruct face-appropriate messages. No compiler internals leak face
  knowledge.
- Each face ships with an error vocabulary file (part of the face definition).
- The toolchain (CLI, LSP server, playground) passes the active face to the
  formatter. The formatter is the single point of face-awareness for errors.
- A developer on Python-face who hits a linearity violation sees:
    Error: single-use variable 'x' used twice
      → line 7, in greet
  not:
    Error: affine binding 'x' used 2 times (quantity violation: QOne, found 2)
- The face formatter is versioned alongside the face. When a face is
  deprecated, its error formatter is deprecated with it.
- The IDE/LSP integration carries face information in the project config so
  hover types, completions, and inline errors all speak the face's vocabulary.
- This is a design commitment, not an immediate implementation task. The
  canonical compiler error representation must be designed with this
  formatability requirement in mind from the start.
"""
references = [
  "docs/DESIGN-VISION.adoc (faces section)",
  "docs/specs/faces.adoc",
]

[[adr]]
id = "ADR-011"
status = "accepted"
date = "2026-05-17"
title = "Stdlib namespace model: real modules with qualified paths"
context = """
The AffineScript stdlib was never compiled through the static
resolve → typecheck → codegen pipeline as a coherent unit (issue #128).
Its core files (prelude, option, result, collections, string, io,
testing, effects, math, traits) are interpreter-era code: a flat global
namespace with no `module`/`use`/`open`, and conflicting duplicate
definitions across files — `prelude.affine` and `option.affine` both
define `is_some`/`unwrap`/`map`/… with *incompatible* signatures
(`prelude.map(arr, f)` vs `option.map(f, opt)`). Commit b895374 seeded
`Some/None/Ok/Err` as builtins to make `string.affine` resolve
standalone, a band-aid that entrenches the flat namespace.

Issue #132 required a single ruling — real modules vs intentionally
flat-and-deduplicated — because #133 (dedup), #135 (whole-stdlib
compile), #137 (multi-module integration test) and #138 (band-aid
removal) all branch on it.

The compiler already has the machinery: the grammar accepts
`module X;`, `use path;` and `::`-qualified paths; `module_loader.ml`
resolves module paths to files with search paths, nested modules and
caching; and the *newer* stdlib files (Core, Crypto, Ajv, Sqlite,
Grammy, Deno, Network, Vscode, VscodeLanguageClient) already declare
`module X;` and use qualified constructors (`Ordering::Less` in
traits.affine). Only the legacy core files are flat.
"""
decision = """
The stdlib uses **real modules with qualified paths**, not a flat
de-duplicated prelude.

- Every `stdlib/*.affine` declares `module <Name>;` and is addressed by
  its module path.
- Cross-file use is explicit: `use option::{Option, Some, None};` /
  qualified references `Result::unwrap`.
- There is exactly one canonical definition per name, owned by its
  module. The `prelude`/`option`/`result` overlaps are resolved by
  giving each name a single owning module and having the others `use`
  it (no duplicate, signature-divergent copies).
- A minimal, explicit prelude module may re-export the few universally
  needed names (`Option`, `Result`, `Some`, `None`, `Ok`, `Err`); it
  contains *re-exports*, not independent redefinitions.
- The b895374 seeded builtins are removed once resolution flows through
  the module path (tracked by #138); they are not load-bearing.

This is the path consistent with the machinery the compiler and the
newer stdlib already use; it makes the AOT pipeline exercise real
cross-module resolution, which is the actual #128 objective.
"""
consequences = """
- #133 removes the duplicate/conflicting prelude/option/result defs by
  assigning each name one owning module; non-owners `use` it.
- #135 brings the legacy core files under `module`/`use` as it makes
  each compile through resolve → typecheck → codegen.
- #137 (multi-module integration test) is meaningful: it exercises
  several modules `use`d together, which the flat model could not test.
- #138 can delete the seeded-builtins band-aid once the prelude
  re-export module exists and resolution uses it.
- Slightly more up-front import wiring than a flat prelude, but it is
  the model the language already commits to elsewhere (ADR pointer:
  newer stdlib + `module_loader.ml`), so no new compiler design debt.
- This decision is settled; do not reopen without amending this ADR.
"""
references = [
  "https://github.com/hyperpolymath/affinescript/issues/128",
  "https://github.com/hyperpolymath/affinescript/issues/132",
  "docs/history/MODULE-SYSTEM-PROGRESS.md (2026-05-17 decision section)",
  "lib/module_loader.ml",
  "lib/parser.mly (module_decl / import_decl / COLONCOLON)",
]

[[adr]]
id = "ADR-012"
status = "accepted"
date = "2026-05-18"
title = "Grammar changes are correctness assertions; parser-conflict disclosure"
context = """
The Menhir parser emitted a wall of "N shift/reduce conflicts were
arbitrarily resolved" notices. Issues #215/#218 set out to address the
real concern: a correct toolchain looking broken — acutely damaging when
correctness is the product. Two grammar changes were made along the way
(#222 record `#{ }`; #215 family B `return`/`resume` hoist). It became
necessary to state, permanently, *why* the grammar may change and how the
residual benign notices are handled — so that in the long term no one
mistakes either the changes or the remaining notices for sloppiness.
"""
decision = """
The grammar is changed only to make it assert something TRUE about the
language's semantics; it is never contorted to lower a cosmetic metric.

- `#{ }` records (#218): semantic — kills block-vs-record ambiguity and
  the struct-literal-in-scrutinee hazard by construction. Conflict-count
  fall was a consequence, not the reason.
- `return`/`resume` as diverging prefix expressions (#215 family B):
  semantic — `return e : Never`, never an operator operand;
  `(return a) + b` now needs explicit parens (a feature: post-divergence
  dead code made visible). NOT motivated by, and does NOT reduce, the
  conflict count (proven: 21->21 S/R states, net-neutral).
- Residual ~68 S/R + small R/R (incl. state 401, the block
  trailing-expr-vs-statement boundary): inherent LALR(1) artefacts that
  Menhir resolves CORRECTLY (257-case gate green). Eliminating them =
  systemic precedence/left-factoring surgery, estate-wide parse blast
  radius, cosmetic-only payoff = exactly the contortion this ADR
  forbids. Intentionally LEFT IN PLACE; documented won't-fix on #215.
- Disclosure: default `just build` MASKS these specific benign notices
  but prints the masked count + correctness proof + this ADR pointer +
  the exact reveal command (`just build-loud` /
  AFFINESCRIPT_SHOW_MENHIR_NOISE=1 / plain `dune build`). The
  parser-generator output is not suppressed at source (that would be
  risky change for a cosmetic end); the build is unchanged and fully
  transparent on demand. Masking is disclosure, not concealment.
"""
consequences = """
- Every grammar change in the history has a recorded semantic
  justification; none was made to chase a number.
- The residual notices are settled won't-fix — do not reopen as "bugs"
  without amending this ADR.
- Contributors see a calm, honest build; auditors see everything via
  one documented command.
- This decision is settled; do not reopen without amending this ADR.
"""
references = [
  "https://github.com/hyperpolymath/affinescript/issues/215",
  "https://github.com/hyperpolymath/affinescript/issues/218",
  "https://github.com/hyperpolymath/affinescript/pull/222",
  "docs/specs/SETTLED-DECISIONS.adoc (ADR-012 section)",
  "justfile (build / build-loud recipes)",
  "lib/parser.mly (expr_assign return/resume; record #{ )",
]

[[adr]]
id = "ADR-013"
status = "accepted"
date = "2026-05-18"
title = "Async on the WasmGC backend: transparent CPS continuation transform"
context = """
stdlib/Http.affine exposes one portable surface
`fetch(req) -> Response / { Net, Async }`. The Deno-ESM backend lowers
it to a direct `await` (#226, shipped). The WasmGC backend cannot:
extern calls are synchronous, the boundary is i32-only, and the
estate's async-over-wasm mechanism (#205) is callback-shaped
(`-> Thenable` + thenableThen/thenableResultJson). Issue #225 Option 2
(owner-chosen) requires one BYTE-IDENTICAL source surface on both
targets, so the wasm backend must hide the continuation plumbing.
typed-wasm is the shared convergence ABI (ADR-004); Ephapax is a
co-stakeholder for the async ABI.
"""
decision = """
On the WasmGC backend ONLY, functions whose effect row includes `Async`
are compiled via a selective continuation-passing (CPS) transform.
Pure / non-Async functions are untouched (no codegen or perf change).

- Each async boundary (call to an extern returning under /Async, or to
  another Async function) splits the body; code after it becomes a
  generated continuation function whose env is the live-local capture
  set, marshalled via the EXISTING #199 closure ABI
  ([fnId@0,envPtr@4] through __indirect_function_table).
- The split lowers to thenableThen(handle, <continuation-closure>) (the
  EXISTING #205 host->guest re-entry); the enclosing Async function
  itself returns a Thenable handle, so Thenable composes transparently
  up the call chain. At the host boundary the outermost Thenable is
  awaited. The programmer never sees Thenable — effect row is the
  abstraction, backend chooses the mechanism (as on the Deno side).
- New orchestration over three proven primitives (find_free_vars, #199
  closure ABI, #205 re-entry); NOT a new runtime, NOT JSPI (rejected),
  NOT a general delimited-continuation feature.

Correctness obligations (binding, pre-merge):
1. A linear/own local captured into a continuation is the borrow
   checker's single use; double-resumption impossible (Thenable settles
   once; thenableThen fires once — asserted).
2. Transform triggers iff Async in fd_eff; Net/other effects ride
   along; fd_is_async reused as predicate.
3. Response reconstruction uses a minimal typed reader (jsonField is
   insufficient for headers: [(String,String)]); general decode
   deferred to #161. No silent lossiness.
4. Full `dune test --force` (258) green at every commit; wasm e2e
   parity test mirrors tests/codegen-deno/http_fetch.*.
"""
consequences = """
- Single portable Http surface across Deno-ESM and WasmGC; #160 closes
  only when both targets are green (joint-close with #225).
- The Thenable-handle + thenableThen continuation protocol is the
  agreed async ABI for the typed-wasm convergence layer; Ephapax
  co-stakeholder review is required for the convergence-spec section.
- Delivered incrementally (4 PRs, each behind the 258 gate); scope is
  WasmGC Async functions only.
- This decision is settled; do not reopen without amending this ADR.
"""
references = [
  "https://github.com/hyperpolymath/affinescript/issues/225",
  "https://github.com/hyperpolymath/affinescript/issues/160",
  "https://github.com/hyperpolymath/affinescript/pull/226",
  "docs/specs/async-on-wasm-cps.adoc (full design)",
  "docs/specs/SETTLED-DECISIONS.adoc (ADR-013 section)",
  "lib/codegen.ml (find_free_vars; #199 closure ABI)",
  "stdlib/Vscode.affine + packages/affine-vscode/mod.js (#205 thenableThen)",
  "typed-wasm ADR-004 (convergence / aggregate library; Ephapax)",
]

[[adr]]
id = "ADR-014"
status = "accepted"
date = "2026-05-19"
title = "Module-qualified type/effect path separator: both `.` and `::`, `::` canonical"
context = """
The type/effect grammar had NO module-qualified path production: a
qualified reference such as `Externs.Res` or `Externs.Net` was
unrepresentable in any type or effect position and failed with
`parse error` at the `.` (issue #228). An audit of the estate `.affine`
corpus (compiler-as-oracle, origin/main) found this the SINGLE dominant
fault estate-wide: 525 of ~1177 files fail to parse, qualified-path the
leading cause in every hand-written Frontier-playbook TS-port. ADR-011
already settled "real modules with qualified paths"; the consequence was
unspeakable because the grammar could not name a module-qualified
entity. Per ADR-012 (grammar changes are correctness assertions),
closing this is asserting a settled truth, not adding sugar. The
separator was the open, escalated language-design call: `module_path`
(parser.mly) uses DOT; `use`/value paths use COLONCOLON (ADR-011
`Result::unwrap`, `use option::{…}`); the estate corpus uses `.` for
qualified types.
"""
decision = """
Accept BOTH `.` and `::` (mixed permitted) as the module-qualified
type/effect path separator. `Pkg::Type` is the CANONICAL form
(consistent with ADR-011 value paths — one canonical separator
estate-wide long-term). `.` is tolerated and normalised to `::`.

Implementation (parser.mly, conflict-neutral):
- New `qualified_type_name` (>=2 `upper_ident` segments, right-recursive,
  `qsep = DOT | COLONCOLON`), folded into a single canonical `::`-joined
  ident string. Added to `type_expr_primary` (TyCon / TyApp via `[ ]`
  and `< >`) and `effect_term` (EffVar / EffCon).
- Because the qualified name is folded to one ident, downstream
  (resolve/typecheck/all codegens) sees a single ident and needs no
  change; the formatter prints the stored `::` form, so `.`→`::`
  normalisation is automatic with NO formatter change.
- Conflict-neutral by construction: it only adds DOT/COLONCOLON as
  lookahead after a type/effect-position `upper_ident`, where no reduce
  action previously existed (that void is precisely the
  `parse error at .` #228 reports). Measured: Menhir conflict states
  unchanged at 21 S/R + 1 R/R; item counts unchanged at 68 S/R / 7 R/R.
- Resolution of the qualified name against a real module is a separate
  concern (the parse gap is what #228 names); the grammar PR unblocks
  parsing — most of the 525 estate parse failures clear with zero
  consumer churn. Genuine ReScript-surface residue (#229) is tracked
  separately.
"""
consequences = """
- The estate `.affine` corpus parses without rewriting `.`→`::`; the
  formatter migrates to the `::` canonical form opportunistically.
- No estate consumer porting was needed for the grammar gap (rejected
  alternative: rewriting hundreds of files entrenches a workaround
  against the Frontier playbook).
- This decision is settled; do not reopen without amending this ADR.
  CORE-03 in docs/TECH-DEBT.adoc.
"""
references = [
  "https://github.com/hyperpolymath/affinescript/issues/228",
  "https://github.com/hyperpolymath/affinescript/issues/229",
  "lib/parser.mly (qualified_type_name; type_expr_primary; effect_term)",
  "docs/specs/SETTLED-DECISIONS.adoc (ADR-014 section)",
  "META.a2ml [[adr]] ADR-011 (real modules / qualified paths)",
  "META.a2ml [[adr]] ADR-012 (grammar changes are correctness assertions)",
]

[[adr]]
id = "ADR-015"
status = "accepted"
date = "2026-05-19"
title = "WASI Preview2 / WASM Component-Model migration (INT-03)"
context = """
lib/wasi_runtime.ml emits only `wasi_snapshot_preview1.fd_write` to
stdout (fd 1). There is no file, socket, environment, clock, or argv
access, so there is no server-side runtime profile (INT-06 is blocked)
and no real host I/O. INT-03 (#180) is the substrate fix. The owner was
asked (2026-05-19, AskUserQuestion one-way-door fork) to choose between
(a) expanding the preview1 import surface, (b) preview1 + an external
preview1->preview2 adapter as the run path, or (c) a full re-target to
the WebAssembly Component Model with WASI 0.2 (preview2). The owner
chose (c) — explicitly the largest, one-way, highest-blast-radius path.
"""
decision = """
Re-target the WASM output to the WebAssembly Component Model with WASI
0.2 (preview2) WIT worlds. Binding constraints:

- STAGED, non-breaking per slice; each slice is its own PR behind the
  full gate. The legacy core-wasm + preview1 stdout path stays the
  DEFAULT until the final slice flips it, so the migration is
  reversible while in progress even though the end-state is one-way.
- The `affinescript.ownership` custom section is a MULTI-PRODUCER ABI
  (shared with hyperpolymath/ephapax; the typed-wasm contract carrier,
  see docs/ECOSYSTEM.adoc). It MUST survive verbatim onto the
  component's embedded core module. Its format MUST NOT change here;
  any change is coordinated in hyperpolymath/typed-wasm, never made
  unilaterally for this migration.
- Only the `wasm`/`wasm-gc` target re-points. The 22+ source-to-source
  targets (Deno-ESM, Node-CJS, Julia, …) are unaffected.
- WIT world of record: `wit/affinescript.wit` — world
  `affinescript:cli/run` importing the `wasi:cli`, `wasi:clocks`,
  `wasi:filesystem`, and `wasi:sockets` 0.2 interfaces.

Staged plan (ledger INT-03; each row = one gated PR):
- S1 (this PR): ADR-015 + WIT world + staged plan + tooling-prerequisite
  + roadmap truthing. No codegen change.
- S2: toolchain provisioning — `wasm-tools` + `wasm-component-ld` (and
  `wac`) into guix.scm/flake.nix. ABSENT in the current toolchain ⇒ a
  HARD GATE on S3+: a component cannot be built or tested without them.
- S3: componentize on-ramp — codegen still emits core wasm; a
  post-codegen step wraps it with the standard preview1->preview2
  adapter into a component; ownership section survival asserted;
  wasmtime component-run smoke. Codegen unchanged ⇒ reversible.
- S4: native `wasi:clocks` + environment + argv via preview2 (wasmtime
  host-testable), replacing the preview1 shims behind the component path.
- S5: `wasi:filesystem` (open/read/write/close) — unblocks INT-06.
- S6: `wasi:sockets`; then flip the default wasm target to component
  and demote the preview1 stdout path to a named legacy target.
"""
consequences = """
- End-state is one-way (the component model becomes the canonical wasm
  target) but reversible-in-progress: preview1 retained through S5.
- S3..S6 are HARD-GATED on S2 (toolchain). Tracked as a follow-up
  issue; this is disclosed, not hidden.
- typed-wasm ownership-section ABI is unchanged; the coordination
  obligation with hyperpolymath/ephapax + hyperpolymath/typed-wasm is
  recorded and binding.
- Source-to-source targets are untouched; no estate consumer churn from
  this migration until S6, and even then only wasm-target consumers.
- This decision is settled; do not reopen without amending this ADR.
  Ledger INT-03 in docs/TECH-DEBT.adoc; roadmap in docs/ECOSYSTEM.adoc.
"""
references = [
  "https://github.com/hyperpolymath/affinescript/issues/180",
  "https://github.com/hyperpolymath/affinescript/issues/160",
  "https://github.com/hyperpolymath/affinescript/issues/225",
  "wit/affinescript.wit",
  "lib/wasi_runtime.ml",
  "lib/codegen.ml / lib/codegen_node.ml (wasm target)",
  "docs/specs/SETTLED-DECISIONS.adoc (ADR-015 section)",
  "docs/ECOSYSTEM.adoc (AffineScript <-> typed-wasm contract; INT-03)",
  "hyperpolymath/typed-wasm (multi-producer ownership-section ABI)",
  "WASI 0.2 / WebAssembly Component Model specification",
]

[[adr]]
id = "ADR-016"
status = "accepted"
date = "2026-05-19"
title = "Effect-threaded async-boundary detection (side-table; #234)"
context = """
The WasmGC CPS transform (ADR-013) detects the async boundary
*structurally*: a `let` whose RHS calls a primitive in a hardcoded set
`async_primitives = ["http_request_thenable"]` (lib/codegen.ml). This
was the deliberately-contained #225 PR3a scope. It is brittle: every
new async stdlib primitive must be added to the set, and a
user-defined `Async`-effecting function is invisible to it — blocking
the fully transparent ADR-013 surface for user async code. #234 asks
for the principled generalisation: the boundary is any call whose
effect row ⊇ `Async`. This requires per-call effect information at
codegen time. The AST (`lib/ast.ml`) carries no location or node id on
`ExprApp`, and the owner-chosen mechanism (AskUserQuestion
2026-05-19) is a typecheck→codegen side-table, NOT AST annotation.
"""
decision = """
Thread per-call-site effect rows from typecheck to codegen via a
*side-table*, keyed by a deterministic shared call-site numbering.

- *Keying.* A single shared traversal (new `lib/effect_sites.ml`)
  assigns every `ExprApp` an ordinal in a fixed pre-order walk of the
  program. Both typecheck and codegen obtain ordinals by calling the
  *same* function, so keys cannot drift. No AST shape change (the
  pipeline already threads one `prog` value through resolve →
  typecheck → borrow → quantity → codegen unmodified, but ordinals —
  not physical identity — are the contract, which is robust to any
  future node rebuild).
- *Producer.* `Typecheck.check_program` populates
  `(int, effect_row) Hashtbl.t` (call-site ordinal → resolved effect
  row, declared *and* inferred) and returns it in its result context.
- *Pipeline.* `bin/main.ml` threads the table into the codegen entry
  alongside `prog` (one extra argument; the existing source-to-source
  backends ignore it).
- *Consumer.* The CPS detector's boundary predicate becomes “the
  `let`-RHS call's effect row ⊇ `Async`” via a table lookup, replacing
  `is_async_prim_call`/`async_primitives`.
- *Fallback / safety.* If the table has no entry for a site (e.g. a
  pre-typecheck embedder path, or a synthesised node), codegen falls
  back to the structural recogniser. The hardcoded set is retired only
  once the table path is proven (final slice); over-conservative
  fallback is always sound (= today's behaviour).

Staged (ledger #234; each a gated PR, full `dune test --force` +
wasm e2e):
- S1 (this): ADR-016 + plan. No code change.
- S2: `lib/effect_sites.ml` shared numbering + typecheck builds &
  returns the side-table. NO codegen behaviour change (table built,
  unused) — pure, gate-neutral.
- S3: pipeline threads the table; codegen boundary predicate switches
  to the table with structural fallback; new e2e proving a
  *user-defined* `Async` fn triggers the transform (the payoff). All
  existing http_cps_* / http_response_reader stay green.
- S4: retire the hardcoded `async_primitives` set (fallback remains
  for table-miss only); doc truthing.
"""
consequences = """
- Generalises to user-defined `Async` functions; new async primitives
  need no codegen edit (closes the brittleness #234 names).
- One-way-ish: introduces a typecheck→codegen data channel (shared
  infra). Reversible per-slice (S2/S3 are additive; the structural
  recogniser stays as the sound fallback throughout).
- Source-to-source backends unaffected (they ignore the table arg).
- This decision is settled; do not reopen without amending this ADR.
  Ledger #234 / CORE-02 in docs/TECH-DEBT.adoc.
"""
references = [
  "https://github.com/hyperpolymath/affinescript/issues/234",
  "https://github.com/hyperpolymath/affinescript/issues/225",
  "docs/specs/async-on-wasm-cps.adoc (ADR-013)",
  "lib/codegen.ml (async_primitives / detect_async_base_case)",
  "lib/typecheck.ml (check_program)",
  "lib/effect_sites.ml (new; shared call-site numbering)",
  "docs/specs/SETTLED-DECISIONS.adoc (ADR-016 section)",
]

[[adr]]
id = "ADR-018"
status = "accepted"
date = "2026-05-19"
title = "No raw/FFI escape: typed `extern` is the only host bridge"
context = """
ReScript `%%raw("<host source>")` / `%raw` injects arbitrary untyped
host source. AffineScript's only host bridge is `extern fn` / `extern
type` (parser.mly extern_fn_decl/extern_type_decl, FnExtern body) —
typed, host-supplied, no body, no arbitrary-source escape. 14 estate
`%%raw` occurrences (#229 Tier-3, ESC-01 #245) had no clean target.
Escalated language-side — the bidirectional-evidence discipline of
ADR-014 / #228 and the affine spirit of explicit, typed boundaries.
(ADR-017 is the block-module disposition #262; this is ADR-018 because
main merged ADR-016 = effect-threaded async-boundary, #234.)
"""
decision = """
No raw escape — there is no `%%raw` analogue, by design. Typed `extern
fn` / `extern type` is the SOLE FFI surface. Every estate `%%raw` ports
to a typed `extern` whose signature states the host contract the raw
blob assumed implicitly; the host implementation moves to the
embedder/runtime shim. AffineScript will NOT gain an untyped
intrinsic/`extern raw` block: an arbitrary-source hole defeats
affine/effect tracking at the boundary where the guarantees matter most
— precisely what the type-and-effect discipline (and ADR-012) exists to
prevent. Doctrine decision: `extern` already exists, no compiler change;
it settles the #229 canonical-map target and the FFI stance.
"""
consequences = """
- A `%%raw` encoding genuine logic (not just a host call) is a design
  smell the port surfaces: re-express as real AffineScript + a typed
  `extern` for any true host primitive, never smuggled through.
- `%%raw`-bearing #229 files (idaptik Main/StartupError, parts of
  burble) port under this doctrine; per-file execution is #229 per-repo.
- No language/compiler change; no estate consumer churn from this ADR.
- Settled; do not reopen without amending. ESC-01 #245.
"""
references = [
  "https://github.com/hyperpolymath/affinescript/issues/245",
  "https://github.com/hyperpolymath/affinescript/issues/229",
  "lib/parser.mly (extern_fn_decl; extern_type_decl; FnExtern)",
  "docs/specs/SETTLED-DECISIONS.adoc (ADR-018 section)",
  "docs/RESCRIPT-ELIMINATION.adoc (#229 canonical map; Tier-3 ESC-01)",
  "META.a2ml [[adr]] ADR-012 (grammar changes are correctness assertions)",
]