Architecture Decision Records
Each ADR records a decision a future session could otherwise reverse or relitigate: the rationale, the rejected alternatives, and a "Revisit if" clause that distinguishes legitimate reconsideration from drift. Read the relevant ADR before changing anything it covers.
Layer taxonomy
ADRs are tagged by layer (see ../../ROADMAP.md):
- K — kernel (semantic); near-permanent; deep review required to change
- C — compiler / methodology; stable statements, evolving implementations
- S — surface (liquid); experimental; cheap to write/delete
Recent culls:
- ADR-0003 (own-the-runtime) and ADR-0004 (calculated-VM-canonical) → deleted, subsumed by ADR-0016 (two-hop architecture). See 0016 for the current position.
- ADRs 0010–0014 (per-machine K3 calculations) → collapsed into ADR-0017 (K3 retrospective). The five were execution records; the retrospective preserves the load-bearing insights (composition map, methodology, shared-Value equality). The proofs themselves remain in
effectrow-oracle/oracle-lean/Bang/Calc*.lean.- ADRs 0005 and 0007 → rewritten as kernel-layer semantic principles (glyph specifics moved to the liquid surface layer; filenames refreshed).
The index below is GENERATED from each ADR's frontmatter by
tools/gen-adr-index.py(runjust adr-index). Do not hand-edit between the markers — edit the ADR's frontmatter and regenerate.just adr-checkfails the build if it drifts. Layer tags (K/C/P) live in each ADR's**Layer**bullet, not this table. Format: lightweight MADR; Status ∈ {Proposed, Accepted, Superseded, Deprecated}.
| # | Status | Title | Summary | Supersedes / Superseded-by | Amends / Amended-by | Resolves | Depends-on |
|---|---|---|---|---|---|---|---|
| 0001 | Accepted | Effect rows are idempotent sets (a join-semilattice), modeled as Finset | Effect rows are idempotent sets (a join-semilattice), modeled as Finset. | — / — | — / — | — | — |
| 0002 | Accepted | Verify the reference in Lean 4 + Mathlib, not F* | Verify the reference in Lean 4 + Mathlib, not F* (agent-maintainable proofs). | — / — | — / — | — | — |
| 0005 | Accepted | Reactivity is an operator distinction, not a separate kernel form | Reactivity is an operator distinction, not a separate kernel form (semantic; surface glyph liquid). | — / — | — / — | — | — |
| 0006 | Accepted | Capture is explicit and tracked; no implicit lexical closure | Capture is explicit and tracked; no implicit lexical closure. | — / — | — / — | — | — |
| 0007 | Accepted | Force is always explicit; grouping ≠ forcing; operator precedence is global | Force is always explicit; grouping ≠ forcing; operator precedence is global (semantic; glyph liquid). | — / — | — / — | — | — |
| 0008 | Accepted | The definitional eval is a fuel-bounded free-monad interpreter; handlers are a deep fold | The definitional eval is a fuel-bounded free-monad interpreter; handlers are a deep fold. | — / — | — / — | — | — |
| 0009 | Accepted | The calculated VM is extrinsic and grown one constructor at a time, starting from an arithmetic kernel | The calculated VM is extrinsic and grown one constructor at a time, from an arithmetic kernel. | — / — | — / — | — | — |
| 0015 | Accepted | Continuation reification — a flat generalised-continuation machine (CalcReify); multi-shot / non-tail handlers | Continuation reification — a flat generalised-continuation machine (CalcReify); CalcReifySim bisimulation paused per 0016 (the LR subsumes the goal). | — / — | — / 0051 | — | — |
| 0016 | Accepted | Two-hop architecture: graded-CBPV reference, CalcVM executable spec, abstract proof target | The two-hop architecture keeps the graded-CBPV reference and CalcVM executable spec, with checked forward simulation into a project abstract target; ADR-0059 separately selects Wasm 3.0 as the product target, and ADR-0110 keeps its concrete emitter on an independent differential-evidence edge. | 0003, 0004 / — | — / 0110 | — | 0001, 0002, 0015 |
| 0017 | Accepted | K3 calculated-machine retrospective (supersedes ADRs 0010–0014) | K3 calculated-machine retrospective — composition-mechanism map + methodology; replaces the five per-machine ADRs. | 0010, 0011, 0012, 0013, 0014 / — | — / — | — | 0009, 0008 |
| 0018 | Accepted | Effect-row algebra — lacks-constrained row quantifiers (set discipline) | Effect-row algebra extended with lacks-constrained row quantifiers (set discipline); enables no_accidental_handling. | — / — | — / — | — | 0001, 0016 |
| 0019 | Accepted | Typing context split — Finsupp grade-vector + ambient type context | Typing context split into a Finsupp grade-vector + ambient type context; enables the resource-enforcing rules. | — / — | — / 0020 | Q3, Q10 | 0001, 0016 |
| 0020 | Accepted | De Bruijn indices for the term representation | De Bruijn indices for the term representation — dissolves the named-encoding side-conditions; amends 0019's context split. | — / — | 0019 / — | Q10, Q11 | 0019 |
| 0021 | Accepted | Effect/grade typing corrections surfaced by the STD block | Effect/grade typing corrections surfaced by the STD block — makes preservation/progress/type_safety provable; advances Q4. | — / — | — / — | — | 0019, 0020 |
| 0022 | Proposed | Effect operations: the up rule, operation signatures, and label-discharging handle | Effect operations: up rule + EffSig signatures + label-discharging handle; makes effect-soundness non-vacuous (D3 superseded by 0023). | — / — | — / — | Q4, Q5 | 0018, 0019, 0020, 0021 |
| 0023 | Accepted | The CK machine: deep handlers, and why progress needs a stack | CK machine for deep handlers — Source.step becomes config-level (EvalCtx × Comp); throws discards the captured continuation. | — / — | — / 0045 | Q4, Q5, Q6, Q13 | 0020, 0021, 0022 |
| 0024 | Accepted | Abstraction-safety: no_accidental_handling is correct-by-construction in a label-indexed machine | Abstraction-safety: no_accidental_handling restated faithfully + proven — correct-by-construction in the label-indexed machine. Closes the ◊2 gate. | — / — | — / 0045 | — | 0018, 0023 |
| 0025 | Accepted | Resumptive state handlers: the CK machine keeps the continuation, and the closed focus dissolves the grade tension | Resumptive state handler: dispatch keeps the captured continuation + reinstalls a deep state ℓ s' frame; the closed focus dissolves the grade tension. | — / — | — / — | Q12 | 0023, 0020 |
| 0026 | Accepted | Correctness is a dispatched ladder; the kernel defines semantics, checkers are a pluggable layer | Correctness is a dispatched ladder (verified > tested > unsafe); the kernel defines semantics, checkers are a pluggable layer. Resolves the proof-power dial. | — / — | — / 0040 | — | 0016, 0024 |
| 0027 | Accepted | Polymorphism is staged: monomorphic v1 → Hindley-Milner → System F (+ effect-row + grade) | Polymorphism is staged: monomorphic v1 → Hindley-Milner → System F + effect-row + grade variables. | — / — | — / — | Q17 | 0026, 0001 |
| 0028 | Accepted | Verified core + tested superset: the stratification principle (tooling · language · the meta-circular evaluator) | Verified core + tested superset, separated by an explicit seam — at three levels (correctness · tooling · language total/partial). | — / — | — / — | — | 0026, 0027, 0002 |
| 0029 | Accepted | Iso-recursive ADTs (sum + product + μ) for the data layer | Iso-recursive ADTs (sum + product + μ with fold/unfold); inductive only; μ-vars ≠ polymorphism. | — / — | — / — | Q18 | 0027, 0026, 0028 |
| 0030 | Accepted | STM enters as a transactional handler in v1; privilege is concurrency-only | STM enters v1 as a transactional handler — NO new kernel primitive; privilege (shared heap) is concurrency-only and deferred. | — / — | — / — | — | 0025, 0023, 0001, 0018, 0026, 0016 |
| 0031 | Accepted | CalcVM resumptive state: evalD threads a store and services ops inline; the machine RESUMES with a non-discarding OP (shape A stays, one-shot) | CalcVM resumptive state: evalD threads a label-keyed store servicing ops inline; the machine RESUMES with a non-discarding OP (shape A stays). | — / — | — / — | — | 0025, 0030, 0023, 0016 |
| 0032 | Accepted | group_recovers RETIRED — rollback is a handler mechanism, not an effect-algebra inverse | group_recovers RETIRED — the rollback law is false-as-≈, vacuous, and redundant; v1 rollback is the txn handler. Supersedes 0018's group-row. | — / — | — / — | Q8 | 0018, 0030, 0031, 0001 |
| 0033 | Accepted | The LR relations are indexed by the effect row ε (faithful Biernacki τ/ε) | The LR relations are indexed by the effect row ε (faithful Biernacki τ/ε); a faithful tightening of the Phase-A stub. | — / — | — / — | — | 0021, 0023, 0016 |
| 0034 | Accepted | lr_fundamental is the env-closed (open-term) fundamental theorem; the bare c c is its Γ=[] corollary | lr_fundamental amended to the env-closed (open-term) form; the bare c c becomes its Γ=[] corollary lr_fundamental_closed. | — / — | — / — | — | 0033, 0023, 0016 |
| 0035 | Accepted | Biorthogonal LR for equivalence (◊4); annotated simulation for compilation (◊5) | Biorthogonal LR proves ◊4's contextual-equivalence theorems; AsmFX-style annotated simulation is the method for ◊5's compile_forward_sim. | — / — | — / — | — | 0016, 0033, 0034 |
| 0036 | Accepted | LR closed-value carrier: enforced at Krel/Srel quantification, not EnvRel alone | LR closed-value carrier enforced at Krel/Srel quantification (not EnvRel alone); unblocks closeC_subst_comm + the binder cases. | — / — | — / — | — | 0034, 0033, 0025, 0030, 0016 |
| 0037 | Accepted | Abstract model fights for correctness; implementation fights for performance under contract (+ the shared-nothing concurrency invariant) | Abstract model fights for correctness; implementation for performance under contract; the concurrency runtime is shared-nothing. | — / — | — / — | — | 0016, 0035, 0030, 0026, 0028 |
| 0038 | Accepted | CBPV arrow observation in the biorthogonal LR: peeling Krel(arr) + returner-restricted empty-stack adequacy | CBPV computation-typed arrows in the LR: a PEELING/existential Krel arrow clause + returner-restricted empty-stack adequacy. | — / — | — / — | — | 0034, 0036, 0033, 0035, 0016 |
| 0039 | Accepted | ◊4 split: LR foundation lands for the non-▷ fragment; the ▷-subsystem (μ + resumptive handlers) → ◊4.5 | ◊4 split — the LR foundation lands sorry-free for the non-▷ fragment; the cohesive ▷-subsystem (μ · up · resumptive handlers) defers to ◊4.5. | — / — | — / 0041 | — | 0038, 0036, 0034, 0033, 0035, 0030, 0016 |
| 0040 | Accepted | Laws as first-class algebraic interfaces; proof-first discharge (amends ADR-0026) | Surface laws are first-class, enforced algebraic interfaces; discharge is proof-first → test → assert. Amends 0026's test-default. | — / — | 0026 / — | Q19 | 0026, 0027, 0029, 0016 |
| 0041 | Accepted | ◊4.5: the LR's recursive fragment requires a ▷ (later) modality | ◊4.5 — the LR's recursive fragment (μ · up · resumptive handlers) requires a ▷ (later) modality; build-proven + literature-confirmed. | — / — | 0039 / — | — | 0039, 0038, 0036, 0035, 0034, 0033 |
| 0042 | Accepted | The ADR decided-ledger is generated from frontmatter (drift unrepresentable) | The ADR index + resolved-questions ledger is GENERATED from per-ADR frontmatter; onboarding consults the generated ledger before opening a design question. | — / — | — / — | — | 0026 |
| 0043 | Accepted | ◊4.5b: scoped-seam for nested-wrapping-handler resumption (the lr_sound moat scope) | ◊4.5b's resume-through-a-wrap edge is excluded by a scoped seam (the NoWrapMiss primitive is landed); the cheap typed-CrelK close (Architecture D) was build-probed NO-GO (no KrelS⇒HasStack bridge — the LR is one-way), so the ADR-0026 tested-descent seam is the verified-final answer for this edge. | — / — | — / 0045, 0050 | — | 0041, 0039, 0026, 0025, 0023 |
| 0044 | Accepted | Dynamic vs lexical handler dispatch (v1 stays dynamic; named handlers a recorded future) | v1 keeps DYNAMIC handler dispatch (splitAt outward search; ADR-0023/0024). Lexical/named handlers (capability-targeted, à la Koka named handlers / Lexa tunneling) are NOT adopted but recorded as a future direction: they would dissolve the ADR-0043 resume-through-a-wrap edge and turn the verification seam into a per-handler USER CHOICE — at the cost of a second dispatch path whose library-encodability (vs a 6th primitive) is unverified. | — / — | — / 0045, 0052 | — | 0043, 0024, 0023, 0016, 0001 |
| 0045 | Accepted | Pivot to a typed logical relation + static/capability dispatch | bang-lang pivots from an UNTYPED-dynamic kernel to a TYPED logical relation + STATIC (capability) handler dispatch. The ADR-0043 resume-through-a-wrap edge is an ARTIFACT of dynamic dispatch, not a fundamental limit: a static-link kernel dissolves it (build-gated). The pivot stays inside graded CBPV (Levy already types the CK machine), is bounded (LR changes only its index set; dispatch is a perform-semantics swap, no 6th primitive), build-confirmed to preserve set-rows (no ordered evidence / no rank-2 polymorphism), and demotes dynamic dispatch to a tested shell macro. | — / — | 0043, 0044, 0023, 0024 / 0050 | — | 0016, 0043, 0044, 0001 |
| 0046 | Accepted | The surface architecture: a canonical explicit core + an inference-bridged sugar surface | bang has TWO syntaxes for ONE core. The CANONICAL CORE is fully explicit — every label/capability, grade, effect row, and type spelled out — ergonomic to the machine; it is where the semantics and the proofs live, and it is a first-class WRITABLE surface (not a hidden IR). The SUGAR SURFACE (the "language API") omits what can be inferred; ergonomic to humans and agents. A deterministic ELABORATOR bridges them by inference. The surface has no semantics of its own — its meaning IS its elaboration to the core; you verify the small core once, the surface is correct-by-elaboration. The elaborator is tested-not-verified (shell), differential-tested against the core. Load-bearing constraint: inference is a deterministic function or a LOUD ERROR — never a guess — so every surface program elaborates to a UNIQUE core term (no ambiguity). North-star: infer as much as possible. | — / — | — / — | — | 0026, 0045, 0016, 0007 |
| 0047 | Accepted | The sugar surface: dialects + user-extensible macros, one mechanism, safe by core-recheck | The sugar surface (ADR-0046's "language API") is a layer of DETERMINISTIC ELABORATORS to the canonical core. ONE mechanism serves both DIALECTS (curated sugar bundles — v1 ships a single C-like one, in the Rust/Zig/Gleam family) and USER MACROS (ad-hoc, post-v1). Safe by construction: the core RE-CHECKS every elaboration, so untrusted user sugar can produce at-worst a wrong-but-core-checked program, never an unverified one; and the lexical-capability discipline (ADR-0045) gives effect-hygiene for free. The load-bearing cost is AMBIGUITY DETECTION — every surface program has a UNIQUE elaboration or a LOUD ERROR, never a silent pick. v1 ships a fixed C-like dialect (ambiguity = an unambiguous grammar, easy); user-extensible sugar is post-v1, and the cheapest way to keep it unambiguous is keyword-led macros. | — / — | — / — | — | 0046, 0045, 0026 |
| 0048 | Accepted | The library tiering: Frontend / Core / Backend, a dependency V with an apex | Make the architectural seams VISIBLE in the module structure. The Bang library tiers into three namespaces — Bang.Frontend (the human/agent edge: surface, elaborator, the writable NamedCore IR, tooling; tested-not-verified), Bang.Core (semantics + IR + proofs; the single source of truth), Bang.Backend (the machine edge: CalcVM + the verified WASM compiler) — plus an APEX (Spec/Audit/Distribution) that aggregates across all three. The dependency rule is a V, not a line: data FLOWS Frontend → Core → Backend (text → IR → WASM), but DEPENDENCIES point inward at Core (Frontend → Core ← Backend); Core imports nothing outward. A fitness function (tools/arch-check.sh) enforces this as a TESTED rung — direction drift is a build failure. Rollout is seam-first: Bang.Frontend is established now (NamedCore); the physical move of the existing flat modules is DEFERRED until they are green again (the ADR-0045 pivot left them build-red; moving red files is unverifiable churn), and the Core-internal sweep waits for lr_sound. | — / — | — / — | — | 0046, 0047, 0026, 0016 |
| 0049 | Accepted | Capability-safety diagnostics via the lexical-well-capped (LW) pass, not typing-rule fusion | Capability errors (a perform cap ℓ op's cap resolves to a handler of the wrong label/kind) are reported by a label+kind-aware checking pass over the EXISTING LW machinery (CapResolvesKind/handlesOp/staticSplit), which already computes the exact mismatch decidably and carries the (cap, ℓ, op) triple a sharp message needs. We do NOT fuse cap-resolution into the core typing rule HasCTy.perform (approach "A"): it is HARD (~200–300 LOC, breaks the cap-irrelevance principle, risks the axiom-clean STD block), buys no diagnostic power the LW lacks ("A forces B anyway"), and contradicts the field's universal practice of keeping handler RESOLUTION a separate lexical pass (Zhang-Myers, Effekt, Koka). HasCTy.perform stays cap-irrelevant; the diagnostic richness lives in the separate LW pass — the kernel-minimal / shell-rich stratification (ADR-0026, kernel-shell-library). | — / — | — / — | — | 0045, 0026, 0044, 0046 |
| 0050 | Accepted | The LR handler-arm cancellation is build-refuted; v1 ships LR seam-5 | The env cap-shift cancellation that the 3 crelK_fund handler arms (compatK_handle{Throws,State,Transaction}) need is BUILD-REFUTED. Its U-clause reduces to a config-simulation (handleF h :: K, shiftCap c) ≈ (K, c) that walls at the state/txn resume. Root cause: this is a bang-SPECIFIC artifact of the de-Bruijn cap representation (ADR-0046) — crossing a handle SHIFTS caps (Val.shiftCap); Biernacki's named-handler n-free never has this obligation, so there is no proof to inherit. Both attempted carriers — A (LR LWStack-fold, the operator's committed route) and B (standalone config-simulation) — share this ONE wall. v1 ships the LR with the 3 arms as ADR-0043 seam descents (seam-5); the real 5→2/full close is a REPRESENTATION change (absolute/level caps, or named handlers ADR-0044) deferred to a feasibility spike. | — / — | 0043, 0045 / 0052, 0053 | — | 0043, 0044, 0045, 0046 |
| 0051 | Accepted | The CalcReify → Bahr–Hutton 2022 monadic recast is NO-GO (renames, does not dissolve) | Recasting CalcReify's fuel-indexed forward bisimulation into the Bahr–Hutton 2022 Monadic Compiler Calculation frame (partiality/Delay monad + step-indexed strong bisimilarity) does NOT dissolve the open perf_outcome_mono gate — it RENAMES it. The 2022 frame gets its key monotonicity (~idown) FREE from coinduction; bang's index is EAGER fuel, so the matching obligation is the opposite direction (upward, f ≤ f' ⇒ outcome preserved), must be EARNED, and the deep case (a performing resumed body under handleC, deep re-handling) is a genuine bisimulation knot the single-monad paper never confronts. The shallow leg is already bind_mono (the paper's bind-cong specialised to the ret leg — bang has it). No usable coinductive Delay/Partial exists in Mathlib (only propositional Part/PFun); a faithful port is prohibitive infra for zero buy on the gate. Keep bang's eager Comp + Nat fuel + RelV. Re-open ONLY if genuine divergence (the Div fragment) enters CalcReify. Bonus: perf_outcome_mono was never a Lean statement (only a doc-name in 0015 / k2-playbook / a CalcReifySim comment); formalized for the first time in the spike (scratch/archive/MonadicRecast.lean, PerfOutcomeMono). | — / — | 0015 / — | — | 0015, 0016 |
| 0052 | Accepted | bang's effect dispatch is LEXICAL; the CalcVM reference re-derives cap-keyed (route B) | The kernel (ADR-0045 static/cap dispatch) and the CalcVM reference evalD (ADR-0023 dynamic/nearest-label) build-provenly DISAGREE on a well-typed same-label-shadowing program: handle (state 1 10) (handle (state 1 20) (perform cap=1 1 "get")) gives kernel 10 (cap=1 names the OUTER handler, lexical) but evalD 20 (nearest-label, dynamic) — both rfl. The witness is well-TYPED (not just well-capped): handleState's subsumption premise e ≤ labelEff ℓ ⊔ φ admits a handler over a body that doesn't use ℓ, so same-label nesting types. DECISION: bang's effect dispatch is LEXICAL — the kernel (ADR-0045's cap dispatch) is canonical; evalD is the stale dynamic half left over from before the typed-static pivot. Route B: re-derive evalD (+ unwindFind/compile/exec) cap-keyed to match the kernel — full generality, no seam, return-only/vacuous handlers retained. Sequence B AFTER the absolute-caps migration (ADR-0053): cap-keying evalD against de-Bruijn caps then re-doing it for absolute caps is wasted work. Rejected: (A) CalcVM-seam — ships a KNOWN machine≠kernel divergence (the diff-test Agree asserts one v from both, UNSATISFIABLE on shadow programs → not diff-testable → strictly weaker than the LR seam-5, which has exec as oracle); (C-new=relevance typing) — a labelEff ℓ ≤ e premise forbids the divergence by construction but also kills return-only handlers (handle (throws 0) (ret 7), a deliberate + tested feature; the effect row cannot distinguish "ℓ handled below" from "ℓ unused" — both ⊥); (C-new=scope-tracking) — a true narrow rule needs an in-scope-label set threaded through 12 rules + ~134 Metatheory + the FROZEN Spec (large, re-freeze). | — / — | 0044, 0050 / — | — | 0023, 0044, 0045, 0050 |
| 0053 | Superseded | Absolute (root-level) caps dissolve the shift wall; LR seam 5→2 | GO on absolute/level caps — the perform cap is a ROOT-LEVEL (from the program root / stack bottom; lvl=0 = outermost handler), NOT a de-Bruijn outward index. Crossing a handle does NOT shift the cap (Comp.subst leaves it unchanged), which dissolves the de-Bruijn shift wall (ADR-0050) BY CONSTRUCTION: closeC_handle* rewrite to the UNSHIFTED closeC δ M, so the 3 crelK_fund handler arms close on their LANDED compatK_handle* cores — LR seam 5→2 (only hcatch + :1801 remain as ADR-0043 descents). Runtime dispatch resolves the level via absSplit K cap = staticSplit K (handlerCount K - 1 - cap) (the conversion modulus self-adjusts under stack mutation — the +1 the shift threaded is absorbed). The WC/LWT/progress cap-resolution re-keys to absResolvesKind; the WC keystone (WCComp.shiftCap_insert general-Δ insert) reformulation is the one kernel-engineer-paired 2c piece still seamed. Frozen-statement-free for the 5→2. Supersedes ADR-0050's "defer the representation fix." | — / 0054 | 0050 / — | — | 0045, 0046, 0050 |
| 0054 | Accepted | Handler reference by generative IDENTITY (re-base as data), not an integer cap | Reverse ADR-0053's absolute caps (build-verified UNSOUND: a first-class thunk that locally handles its own effect, forced under an unrelated handler, mis-dispatches its own perform to the outer handler — a well-typed, LWConfig-valid program evaluating to a wrong-typed value). Root cause is structural: a SINGLE INTEGER cap cannot be both migration-stable and shift-free, and closeC ≡ Comp.subst couples them (a substitution-time shift for migration soundness re-shifts closeC_handle* = the ADR-0050 LR wall). Fix (deep-research-grounded, Lexa/Effekt/Koka): the perform's handler reference is a generative IDENTITY (a fresh label/capability travelling WITH the thunk), and any handler-crossing re-base is carried as explicit DATA on the value, not proof-internal index arithmetic. Identity-as-value needs NO 6th primitive (a label/capability is an ordinary value; handler already primitive) — refining ADR-0044's hesitation. Keep the step-indexed LR (route B, Effekt System Ξ shows lexical capability-passing admits a closeable LR); Leroy forward-simulation (Lexa, no LR) is a recorded alternative. First-class-thunk escape is ruled out by the EXISTING LWT non-escape gate (preservation_returnEscape), not by second-class thunks. Representation redesign in SHAPE (Core/Syntax + VM dispatch re-derivation); replaces an unsound kernel, not an upgrade. | 0053 / — | — / — | — | 0044, 0045, 0046, 0050, 0052, 0053, 0016 |
| 0055 | Accepted | Global-fresh capability identity (reverse Fork-ii's handlerCount) | ADR-0054 fixed the representation (handler reference = a capability VALUE, dispatched by identity match) but left the identity-MINTING scheme open and chose Fork-ii: identity = handlerCount K at install (depth-from-root, NO Config counter). Build-verified this session that depth-based minting admits a cross-extent collision: a capability that escapes its (popped) handler, then is forced under a FRESH handler installed at the SAME depth, resolves to that same-depth impostor instead of being stuck. Witness progB (re-handled escape) → done reading the wrong handler's state; progB' (direct-force escape, no re-handler) → stuck. The inc-4 metatheory (preservation/progress/type_safety) remains SOUND — it proves no-stuck, which progB (done) does not violate — but capability resolution-transparency (a cap names ITS handler, not a same-typed impostor) is NOT achieved, and NonEscape-as-FocusResolves ("the cap resolves to something") is too weak: the collision makes it satisfiable for a genuinely-escaping program. This is the long-flagged WC keystone-2c, now concretely witnessed. Fix: mint identity from a monotonic Config counter (global-fresh / gensym) — never reused, so no two handlers ever share an identity → an escaped cap resolves to ITS handler or to NOTHING (stuck, fail-loud); collisions become UNREPRESENTABLE and NonEscape's simple form becomes adequate. Reverses Fork-ii's "no Config counter" simplicity bet, which this finding build-refuted. | — / — | — / — | — | 0054, 0030, 0023 |
| 0056 | Accepted | The capability-escape soundness gap (the ⊥-row gate does NOT rule out escape) | ADR-0054 asserted "first-class-thunk escape is ruled out by the EXISTING LWT non-escape gate (preservation_returnEscape), NOT by second-class thunks." That assumption is machine-checked FALSE (inc-5, B2): a capability can escape its handler and get STUCK even in a well-typed-at-⊥, VcapFree program, because typing is by LABEL (ℓ) but dispatch is by IDENTITY (n) — the ⊥-row gate is label-based and cannot see the identity-escape. Witness progB (the DiagonalFalsifyProbe diagonal_is_false, axiom-clean): HasConfigTy (0,[],progB) ⊥ (F 1 unit) ∧ VcapFree progB ∧ ¬ NonEscape (0,[],progB) ∧ Source.eval progB = .stuck. So the inc-5 diagonal (HasConfigTy ⊥ ∧ VcapFree → NonEscape) — the source-level soundness payoff — is FALSE, and the language is unsound as it stands (a well-typed source program gets stuck). This is the WC keystone-2c, only HALF-solved: ADR-0055 global-fresh fixed the collision (wrong-handler resolution), but the escape (cap → nothing → stuck) remains. The fix requires a real non-escape discipline. DECISION: explore the design space first (operator ruling, 2026-06-26) before committing — same approach as the ADR-0053→0054 pivot. | — / — | — / — | — | — |
| 0057 | Accepted | The non-escape discipline: answer-type label-freedom at the kernel (B-occ) | ADR-0056 recorded that the language is unsound — a capability can escape its handler and | — / — | — / — | — | 0056, 0055, 0054, 0030, 0027, 0023 |
| 0058 | Accepted | The CrelK Canonical wall is a frozen-signature artifact; route 1 (carry the real counter) deletes it | The binary-LR Canonical wall (task #33) — closing crelK_fund's ret case, hence | — / — | — / — | — | 0016, 0050, 0052, 0055 |
| 0059 | Accepted | Compile to Wasm 3.0 with a grade-directed pluggable backend (refines ADR-0016's WasmFX-primary target) | Stack switching did NOT land in Wasm 3.0** (Sept 2025 standardized WasmGC, exception | — / — | — / 0110 | — | 0016, 0058, 0001, 0052 |
| 0060 | Accepted | Cap-non-escape soundness via grade-driven liveness; commit the grade rig to NoZeroDivisors + ZeroSumFree + Nontrivial | The diagonal's last obligation wsCfg_step (the WScfg preservation that closes | — / — | — / — | — | 0054, 0055, 0001, 0016 |
| 0061 | Accepted | The soundness-diagonal invariant: typeless → graded + stratified-fresh | The non-escape soundness diagonal (Bang/Model.lean, inc-5) preserves an internal config invariant WScfg across Source.step; reachability + WScfg ⟹ FocusResolves then gives NonEscape for the initial config (the sole inc-4 carried obligation). WScfg carried TYPELESS liveness (LWSC/LWSK) + the ids-only freshness WellCounted (StackBelow), which discard two facts the preservation needs, leaving wsCfg_step with 3 un-closable sorries. (1) The typed GRADE: LWSC's storage q is a free ∃, so a typed-DEAD capability is NOT forced dormant — the 4 elimination walls (letC/app/case/split) of the ⊥-row return-escape and the REDUCE dead-arg cannot close (spike #48 build-PROVED this: the value-layer B-occ technique works but WALLS at eliminations; escapeB_app in Bang/Witness/BoccRegress.lean:145 is the machine-checked falsity that typeless B-occ blinds at the arrow/eliminator). (2) Cap-id FRESHNESS over STORED caps: StackBelow bounds only handleF FRAME ids < g, never the caps stored in letF/appF frames, so the POP-tail (popping handleF g' must leave the tail's caps ≠ g') is unprovable though TRUE by global-fresh monotone minting (ADR-0055). DECISION: regrade WScfg to carry GRADED liveness LWSCg/LWSKg (gate b && decide(q≠0) tied to the typed binder grade, projecting to the typeless layer by forgetting the grade) PLUS a STRATIFIED capability-freshness conjunct FreshCfg = CapsBelow (ids + stored caps < g) ∧ a focus-cap bound ∧ StratFresh (everything below each handleF n is < n). The grade closes the eliminations (dead intermediate ⇒ gate-dormant ⇒ stack-independent) + the REDUCE dead-arg; StratFresh closes the POP-tail; the POP-focus rides B-occ over the grade. Result: type_safety reduces to a single sorry on DISPATCH (#35, the resumption-multiplicity grading). | — / — | — / — | — | 0060, 0055, 0057, 0054, 0023 |
| 0062 | Accepted | Multi-shot resumption is ω-graded by construction; the affine fragment is gradeable | The "grade the resumption" frontier (task #35) asks what multiplicity grade r a handler frame carries for how many times it invokes its captured continuation. Decision: record the resumption grade as a stack-grade homomorphism gradeOf : Stack → (Mult, *, 1) with resumeMult (throws=0, state/transaction=1) read off dispatchOn's reinstall behaviour. QTT's {0,1,ω} trichotomy settles it: 0 = *-zero (throws — frame absent), 1 = *-unit (one-shot — transparent, vanishes), ω = *-top (multi-shot — absorbing). bang's built-in handlers are all affine (throws zero-shot, state/transaction one-shot; genuine multi-shot lives only in CalcReify). So multi-shot resumption is ω-graded BY CONSTRUCTION — a closed mathematical boundary (Cousot POPL'24 Th II.3.9: no finite variant for unbounded invocation; = the non-idempotence 1+1=ω), NOT an open sorry. The affine fragment is gradeable by reflexivity (one_mul) — engineering, not research. Declines the transfer-function-grade escape hatch (Ivašković FSCD'20) that would recover finite multi-shot grades, because it abandons the scalar QTT the rest of the system is built on (let-rule (q_or_1 q2)•γ₁ + γ₂, F q A returner grade) for a construct the built-in handlers — and the WasmFX target (ADR-0035) for the affine fragment — do not use. | — / — | — / — | — | 0054, 0035, 0030, 0023 |
| 0063 | Accepted | Capability escape is a defined fail-loud for v1; scoped-cap types deferred post-v1 | The inc-5 diagonal HasConfigTy ([],c) → NonEscape ([],c) — the derivation that makes | — / — | — / — | — | 0016, 0001, 0055 |
| 0064 | Accepted | Regrade WScfg to a carrier-indexed liveness invariant (LiveCapsResolveV/C/K), derived coherent from typing | The diagonal's preservation obligation wsCfg_step was carried by a typeless | — / — | — / — | — | — |
| 0065 | Accepted | Arithmetic & comparisons as base-type δ-rules (Comp.binop) — pure, ⊥-row | Integer arithmetic (+ − × ÷) and comparisons (< ==) enter the kernel as pure base-type δ-rules via ONE new computation form Comp.binop : BinOp → Val → Val → Comp, ⊥-row typed. Comparisons return Bool = 1+1 (a sum), so if is surface sugar over case. A δ-rule is NOT a sixth computational primitive — invariant #5 governs effect/computation structure, not base-type operations. | — / — | — / — | — | 0029, 0020, 0007 |
| 0066 | Accepted | Surface type system — a bidirectional checker targeting the kernel HasCTy (tested-superset, grades-deferred) | The surface gains a TYPE LAYER — a bidirectional type-checker (check ⇐ / synth ⇒) over the surface AST that produces typing conforming to the kernel's graded HasVTy/HasCTy relation. The relation stays the single source of truth; the checker is an ALGORITHM in the TESTED superset (its soundness vs HasCTy is differential-tested, not proven in v1). v1 checks type structure + effect rows; grades default to ω (grade-checking is a separable refinement). Unblocks #5 (effect-typed signatures), #24 (lawful algebra — type-directed operator resolution), #21 (scoped capability types). | — / — | — / — | — | 0019, 0020, 0028, 0029 |
| 0067 | Accepted | Integer semantics: unbounded ℤ in v1 — width is a verified optimization behind the oracle | v1 Int denotes unbounded ℤ — the oracle's existing δ-rule (ADR-0065 Comp.binop over Lean Int) IS the spec, so the decision costs zero proof rework. Overflow is never undefined (vacuous under ℤ; binding on any future width). Width, if ever introduced, enters through the ORACLE via a new K-ADR — never backend-decided. The Wasm model's misnamed i32 constructor is renamed; real-Wasm emission (post-v1) ships bignum first, i64 as a later verified optimization. | — / — | — / — | Q25 | 0065, 0016 |
| 0068 | Accepted | Surface trait/impl wiring — tested-rung ceiling for source laws, structural keying, resolution as elaboration | The #24 parser↔Trait↔checker wiring, three decisions: (1) a law parsed from SOURCE lands on the tested rung by construction in v1 (decidable predicate over kernel runs, checked sample, rung DISPLAYED) — the verified rung stays Lean-level; a later meta-elaborator lifts the ceiling without syntax changes. (2) Instances are keyed on STRUCTURAL types (impl Add for (Int, Int)) — nominal keying arrives with #23. (3) Operator resolution is a type-directed ELABORATION pass over a decl-prelude program (Prog = decls + body) behind a NEW typed entry point; the untyped path is untouched. | — / — | — / — | — | 0040, 0066, 0029, 0067 |
| 0069 | Accepted | Surface data declarations — named constructors as transparent sugar over sums · products · μ | Recursive data surfaces as data declarations in the Prog prelude (data IntList = Nil | Cons(Int, IntList)): constructors are TRANSPARENT sugar over the kernel's existing sums/products/μ (right-nested sum by decl order, k-ary product payload, uniform fold-wrap), aliases are STRUCTURAL not nominal (consistent with ADR-0068 keying; nominal identity deferred to #23-proper), and the feature lives on the TYPED path only (ctor intro + named match need the decl env; the untyped path fail-louds). Recursive FUNCTIONS are out of scope — a separate bullet (fix + Div row). | — / — | — / — | — | 0029, 0068, 0066 |
| 0070 | Accepted | Surface named capabilities — with H as h in e + h.op, exposing the kernel cap the ambient forms already use | Named capabilities surface the cap VALUE the kernel already binds at every handler (ADR-0054/0055): with state 1 as h in e binds h : Cap state to the installed handler's cap, and h.get / h.put(v) perform on THAT cap. The ambient forms (get, state s in e) stay as sugar for the single-instance common case — they resolve an implicit sentinel cap. The win is MULTIPLE COEXISTING INSTANCES (two state cells) and capability-PASSING (h is a first-class value), neither expressible with the nearest-sentinel ambient form. Correction to the issue framing: both forms dispatch by IDENTITY (lexical) — bang has no dynamic/nearest-label dispatch (ADR-0052); "ambient" here means implicit-cap-resolution, NOT dynamic dispatch. | — / — | — / 0072 | — | 0054, 0055, 0052, 0068 |
| 0071 | Accepted | Rule-table Pratt parser — reify the grammar so parser · spec · tree-sitter generate from one root | Adopt the Cheng-Parreaux (ECOOP'26) rule-table Pratt architecture for the surface parser: reify operator precedence as binding-power DATA and keyword-led constructs as first-class parsing RULES, so one Pratt-shaped loop consults the reified rules — and the SAME rule values generate the grammar spec (railroad + precedence table) and the tree-sitter grammar. Staged: (①) replace the fixed 4-level precedence chain with one binding-power loop over a reified operator table; (②) reify keyword-led rules; (③) generate the language.md grammar section (#38); (④) whitespace-insensitivity + bang fmt (Q24) fall out. The parser stays TOTAL (fuel-driven) so demo #guards reduce under rfl. | — / — | — / — | — | 0068, 0069, 0070 |
| 0072 | Accepted | Named-capability syntax: drop with, fold the binder into the effect forms (state 5 as h in e) | Revise the named-capability surface syntax from ADR-0070's with <kind> as h in b to an optional as <ident> binder on the EXISTING per-effect forms: state <init> [as h] in <body> · handle [as h] <body> · atomically [as h] <body>. The with keyword is removed. Reads more naturally (the awkward two-keyword run-on becomes a binder on a form the user already knows) AND is grammar-regular (it folds into the already-reified state/handle/atomically rules instead of a bespoke keyword-pair construct — dissolving the hardest ②b case, ADR-0071). Surface-only: identical lowering, no kernel/semantics/proof/AST change. | — / — | 0070 / — | — | 0070, 0071 |
| 0073 | Accepted | Recursion: let rec surface + Div-row typing; μ-encoding preferred (no new primitive), fix-primitive fallback; TCO deferred | Recursion enters as a surface let rec construct that the checker recognizes and types with Div in the effect row (the stratification seam made real — general recursion is the descent into the fuel-bounded fragment). MECHANISM: prefer a μ-types LIBRARY ENCODING of the fixpoint (no new kernel primitive — invariant #5 holds; the recursion spike #42 confirmed the kernel has the pieces: iso-recursive μ + thunks + arrows), gated on checker completeness (#45) which currently blocks the higher-order payload the encoding needs; a minimal fix kernel primitive is the FALLBACK if the encoding proves too fiddly to type/lower. v1 recursion runs under Source.eval's existing fuel (deep recursion → outOfFuel); TCO is a DEFERRED verified machine optimization (invariant #7), unified with resumption grades (Q27/#17). Resolves Q28. | — / — | — / — | Q28 | 0029, 0028, 0065 |
| 0074 | Accepted | Strings: String = List Char verified spec, Char = a code point; packed runtime + normalization deferred behind the oracle | String is the inductive spec List Char, Char a Unicode code point (a distinct type over Int, refined once Q31 lands). All string operations are TOTAL structural folds (certified ⊥ by #47) — CORRECT and slow first (invariant #7). It is LIBRARY code over the kernel (rides data + Int; invariant #5 — no 6th primitive); only surface string/char literals need parser support. A packed UTF-8 runtime representation is DEFERRED — a later compiled OPTIMIZATION differentially-bridged to the List Char ORACLE (the exact ADR-0067 Int-spec-behind-the-oracle move). Unicode normalization + grapheme clusters are DEFERRED as documented non-features (not silent gaps). | — / — | — / — | — | 0067, 0069 |
| 0075 | Accepted | Polymorphism = a tested checker/elaborator over the monomorphic verified kernel (elaborate-to-mono); bidirectional inference with annotation-required decidability descent; row-polymorphism first-class | Polymorphism is realized as inference + elaboration in the CHECKER (a tested superset), NOT as a System F kernel — generic surface code ELABORATES to MONOMORPHIC kernel terms (monomorphization / dictionary-passing), so the verified kernel (Source.eval/HasCTy/soundness) stays UNTOUCHED, census-stable (the ADR-0026 stratification: verified core + tested superset, seam = elaboration). Type establishment is BIDIRECTIONAL and stratified by DECIDABILITY: HM-INFERRED where decidable (no annotation) → ANNOTATION-CHECKED where inference is undecidable (higher-rank / dependent — the user gives the intended type, checking is decidable) → ASSERTED/postulated (can't check — the escape hatch). Decidability is the invariant: an un-annotated undecidable term is a TYPE ERROR, never an unsound guess — the annotation is the explicit-descent marker (the type-system analog of Div). Row-polymorphism (over effect rows, and eventually grades — ADR-0027) is first-class from the first bite. | — / — | — / — | — | 0027, 0026 |
| 0076 | Accepted | Language tooling by construction: modules elaborate to the flat kernel · the compiler is a queryable content-addressed service · incremental compilation falls out of immutability + purity (the constraints are generative) | The stdlib forces namespacing → a MODULE SYSTEM → multi-module BUILD TOOLS + an LSP. Three decisions, pinned early because retrofitting is expensive: (1) modules are a FRONTEND feature that ELABORATES to the flat kernel (invariant #5, same elaborate-away move as polymorphism/ADR-0075 and the injected prelude — the kernel stays flat, 5-primitive, untouched); (2) the compiler is a QUERYABLE SERVICE — the LSP + build tool are VIEWS over its analyses, NOT parallel type-checkers (a second checker is a single-source-of-truth violation that can DISAGREE with the compiler); (3) the module dependency graph is an ACYCLIC, GENERATED DAG (bang dogfoods its own arch-check V-structure + generated import-graph discipline). LOAD-BEARING RATIONALE — the operator's thesis: bang's core constraints (immutability · purity · ADTs · laws) ARE exactly the invariants that content-addressed incremental tooling REQUIRES, so the tooling falls out BY CONSTRUCTION. Immutability ⟹ stable content hashes ⟹ Merkle-DAG staleness ⟹ incremental compilation that is CORRECT BY CONSTRUCTION (a silently-stale cache is UNREPRESENTABLE — the hash IS the dependency check). Purity ⟹ memoized queries (Salsa-style). The constraints are generative. | — / — | — / — | — | 0026, 0075, 0001 |
| 0077 | Accepted | Documentation architecture: product vs project docs, placed by (audience × temporality) — a doc's home, lifecycle, and maintenance rung follow from its coordinate | Documentation is placed on two axes — audience (consumer/user vs contributor/agent-builder) × temporality (a timeless snapshot vs time-indexed work). PRODUCT docs = consumer × snapshot: the artifact as-it-is, ideally GENERATED from code (can't drift), publishable (docs/reference/language.md, PRD, README, ONBOARDING). PROJECT docs = contributor × time-indexed, sub-split by TENSE: DONE (immutable — CHANGELOG, ADRs = a past decision + rationale, git history), NOW (volatile — CONTEXT, active paths/), NEXT (revisable — ROADMAP, the OKF question ledger, project-roadmap). A doc's (audience, tense) coordinate determines its home, lifecycle, and maintenance rung. Conflating coordinates (a "future feature" line in the product reference, a "current status" line in a timeless doc) is a category error that drifts. This makes EXPLICIT the taxonomy already implicit in the repo's doc-discipline rules. | — / — | — / — | — | 0076, 0026 |
| 0078 | Accepted | Knowledge is git-native (agent-visible, generated + validated); GitHub Issues is the PM layer; a gh-bridge resolves issue-edges into the tie-graph — one graph, two well-chosen stores, no third tool | DOCS stay git-native (the OKF question ledger + ADRs + notes, in the main repo) because the top priority is AI-agent-visibility — an agent reads the repo directly; git files are diffable, PR-reviewed, generated-from-frontmatter, and coupled with the code. A hosted docs tool (Linear/Notion/Jira) would take docs OFF git and regress that priority. GitHub Issues is the PM layer — already in use, excellent GraphQL/REST/gh API, integrates with the repo (PR-closes-issue, #N linkification), and fits the project's scale (Linear/Jira are team-velocity tools = ahead of need; the repo already retired issues-as-files TO GitHub). The two stores are unified NOT by moving one into the other but by a gh-BRIDGE: the OKF see-also: ["#44"] issue-edges are resolved via gh (validate the issue exists, pull its live title/status, render it in the tie-graph) — one queryable graph (questions ↔ ADRs ↔ issues) from two well-chosen stores + a thin bridge. The anti-tangle principle: the tangle risk is a THIRD tool; the fix is the bridge, not replacement. | — / — | — / — | — | 0076, 0077 |
| 0079 | Accepted | Generic (parameterized) data types elaborate to the monomorphic kernel — each concrete instantiation monomorphizes to a closed ADR-0069 μ; annotation-driven introduction | Parameterized data declarations (data List a = Nil | Cons(a, List a)) are realized by the SAME elaborate-to-mono move as the rest of polymorphism (ADR-0075): a generic decl gives POLYMORPHIC constructors (Nil : ∀a. List a, Cons : ∀a. a → List a → List a) that ride the HM generalize/instantiate machinery (ADR-0075/the IVTy·ICTy re-rep), and each DISTINCT concrete instantiation monomorphizes to a closed ADR-0069 μ (List Int ↦ μX. Unit + (Int × X), args substituted for params, self-reference → the μ-bound var). The kernel / Source.eval / HasCTy NEVER see a type variable (invariant #5, kernel untouched). Surface: type params on data + Ty.tApp name args (type application). Constructor INTRODUCTION is ANNOTATION-DRIVEN (check-mode from an annotation or let rec signature drives the concrete element type down through the structure); an un-annotated generic ctor in synth position FAILS LOUD ("annotate") — the ADR-0075 annotation-checked tier. Generic-match binders are derived from the concrete scrutinee μ (unrollMu + navigate). Additive: non-parameterized data decls keep the byte-identical monomorphic path. | — / — | — / — | — | 0069, 0075 |
| 0080 | Accepted | Bounded generic functions monomorphize per concrete carrier — the dict-vs-mono fork resolved for MONOMORPHIZATION; carrier fixed annotation-driven | A BOUNDED generic function (fn fold(xs) : List a -> a where Monoid a = …) is realized by the SAME elaborate-to-mono move as the rest of polymorphism (ADR-0075): at each concrete use (fold xs : Int) the carrier a is fixed, the Trait a instance is resolved, and the instance's ops are SPLICED into a concrete let rec that kernel-typechecks and runs. This RESOLVES the ADR-0075/PATH-polymorphism bite-2 fork for MONOMORPHIZATION (Rust/MLton) over dictionary-passing (Haskell): it is consistent with bite-1's monoData and the raw-splice trait model (ADR-0068/0079), needs no runtime dictionary, and bang is whole-program elaborate-to-mono. The kernel / Source.eval / HasCTy NEVER see a bound or a type variable (invariant #5, kernel untouched, census byte-identical). Surface: a top-level fn name(params) : declaredTy where Trait tyVar = body decl + nullary trait ops (fn empty() -> Self). Traits stay Self-based (ADR-0068) — the bound Monoid a means "the carrier a implements Monoid" (Self = a); no trait type-parameter syntax is added. The carrier is fixed annotation-driven (ADR-0079): v1 requires the declared result type to BE the bound var (the fold shape … -> a), so the call-result annotation gives the carrier; a MISSING instance ⟹ a loud type error. LAWS are preserved unchanged (ADR-0068 tested rung). Only the CONSUMING half is in scope (fold/sum match on Cons/Nil); a bounded function that CONSTRUCTS generic data hits the #55 annotation-driven-intro wall (ADR-0079), deferred. | — / — | — / — | — | 0075, 0079, 0068, 0069, 0073 |
| 0081 | Accepted | Annotation-free generic-data introduction — a generic constructor is a polymorphic function; its instantiation is inferred from field types by HM over a template μ | Generic-data INTRODUCTION becomes annotation-free (lifting ADR-0079's staged annotation-driven limitation, the #50-successor #55). A generic constructor IS a polymorphic function (Some : ∀a. a → Option a); in SYNTH position the checker INFERS its instantiation from the FIELD types via ordinary HM (the IVTy/ICTy machinery), NOT via monoData. Mechanism: the constructor carries a template μ (params left as markers .tVar (paramBase+i)); embVInst mints a FRESH hole per marker when the annotation is embedded; unifying the field expressions against the hole-carrying μ SOLVES the instantiation — concrete at a concrete use, a let-generalized hole inside a polymorphic function body. This is real HM over generic data; monoData/Source.eval/HasCTy/kernel stay UNTOUCHED (elaborate-to-mono). It unifies the annotation-driven (ADR-0079 check-mode) and annotation-free (synth-mode) paths into ONE mechanism. | — / — | — / — | — | 0079, 0075 |
| 0082 | Accepted | Higher-kinded types (Functor/Monad) elaborate to the monomorphic kernel — kinds-as-arity, decidable HK-unification by constructor-injectivity, monomorphize-per-constructor (NOT dict-passing) | Higher-kinded types (trait Functor f, trait Monad m; type variables ranging over CONSTRUCTORS, f : Type→Type) are realized by the SAME elaborate-to-mono move as the rest of polymorphism (ADR-0075/0079/0080): the kernel never learns about kinds, ∀-variables, or type-constructors-as-values. A higher-kinded use is monomorphized at each concrete CONSTRUCTOR (the bite-2 bfnWrapper move, keyed on a constructor name instead of a resolved carrier type). Kinds are tracked as ARITY (a Nat per type variable — a degenerate kind), reusing bite-1's constructor-param count; an explicit Kind inductive is DEFERRED (needed only for higher-order kinds / monad transformers, not for Functor/Monad). Higher-kinded UNIFICATION is decidable by constructor-injectivity decomposition (f a ~ Option Int ⇒ f:=Option, a:=Int) — inside the Miller pattern fragment, available for free because bang has no type families (no reducing type synonyms); anything outside it (f a ~ Int) is an ANNOTATION-required descent, never an unsound guess (the ADR-0075 decidability invariant). Traits gain a constructor-kinded, APPLIED Self (f a = Self a) and POLYMORPHIC methods (fmap : ∀a b. (a→b) → f a → f b), composing bite-0 generalize/instantiate with bite-2 monomorphize-per-carrier. This does NOT re-open the ADR-0080 dict-vs-mono fork: HKT is additive to monomorphization; dict-passing is pulled only by separate compilation or first-class existential constructors, neither present in v1 (bang is whole-program, no existentials). The kernel / Source.eval / HasCTy stay UNTOUCHED, census byte-identical. | — / — | — / — | — | 0075, 0079, 0080, 0068, 0069, 0073 |
| 0083 | Accepted | Option/Result are universal prelude types; Either IS the built-in binary sum (not a nominal type); the first witnessed isomorphisms | Now that generic data (ADR-0079) + annotation-free introduction (ADR-0081) are in, the universal generic types are promoted to the INJECTED PRELUDE (the opt-out module, Q34): data Option a = None | Some(a) and data Result e a = Err(e) | Ok(a), filtered per-name like Str/Char (zero runtime fuel — data decls are elaboration-only). Either is NOT a nominal data type — it IS the built-in binary sum e + a: Left/Right/match are already RESERVED surface primitives (ADR/#53), so a nominal data Either = Left | Right COLLIDES and breaks the sum corpus; one-construct-per-problem ⟹ Either = the sum, and the isomorphism conversions bridge Result/Option to it. Seven functions (mapOption, mapResult, bimap, and the four iso conversions) are injected CONDITIONALLY — only when the program mentions the name (surfUsesVar) — so existing fuel-bounded #guards are UNCHANGED. The four ISO round-trips (from∘to = id) are the FIRST WITNESSED ISOMORPHISMS (Q41's witnessed rung), property-tested through Source.eval. Kernel/HasCTy/census UNTOUCHED (frontend leaf). | — / — | — / — | — | 0079, 0081, 0068, 0074 |
| 0084 | Proposed | Networking is a typed effect + handler, gated on user-defined effects (#44); real sockets deferred to the backend | The web-server northstar demands networking. Q39 frames it as a typed {Net} effect (listen/accept/read/write) realized by a swappable handler — capability-secured, effect-tracked, mock-for-tests/real-for-prod. VERIFIED FROM CODE: the kernel Handler (Bang/Core/IR.lean) is a CLOSED triple (state/throws/transaction) with operations HARDCODED in handlesOp/dispatchOn — there is no general handler carrying user op-clauses + a reified continuation. So a genuine {Net} effect (its own ops) REQUIRES user-defined effects (#44) as a hard KERNEL prerequisite (#44 = L, weeks, spine-touching, ~424 Handler-match sites, ripples to the calc machine/LR/soundness/backend per invariant #4). {Net} is a small INSTANCE of #44, not a peer. The achievable-now slice is a mock/simulated handler on the pure Source.eval (no syscalls); real sockets need the FFI seam (Q37) + compiled backend (◊5+). Decision: name B (genuine {Net} via #44) as the correct answer; ship A (a "net-shaped" demonstrator over the existing state handler — zero kernel change, honestly labelled a demo, ops are get/put) as the cheap near-term slice; gate B on #44; defer D (real sockets) to ◊5+; REJECT C (a bespoke | net kernel constructor — spends #44's full ripple to buy one hardcoded effect, violating invariant #5's "generalize, don't special-case"). | — / — | — / — | — | 0030, 0063, 0070 |
| 0085 | Proposed | User-defined effects: a general custom handler ALONGSIDE the built-in triple (coexist, one-shot v1) | #44 (user-defined effects — the moat: "paradigm and runtime are values") is blocked at the KERNEL, not the surface — the Handler type is a CLOSED triple (state/throws/transaction, Bang/Core/IR.lean) with operations hardcoded in handlesOp/dispatchOn. The performer side is ALREADY general (perform/up routes through EffSig.opArg/opRes — any label, any op; EffSig already IS the user-effect interface), so #44 is a HANDLER-side generalization. Decision: COEXIST — add a fourth Handler.custom : Label → Val → (OpId → Option Comp) constructor ALONGSIDE the three built-ins, NOT collapse them into instances of it; scope v1 to ONE-SHOT tail-resumptive clauses (multi-shot deferred to Q22/Q27). Coexist QUARANTINES the soundness risk behind the constructor seam (the project's own stratification principle): the trusted-three (preservation/progress/type_safety) can stay axiom-clean because their frozen statements are CONSTRUCTOR-AGNOSTIC (no Spec.lean statement changes — the ripple is ~424 ADDITIVE proof cases, not a re-freeze), and any gap that won't close lives in the NEW custom cases WITHOUT regressing the built-ins' clean census. Rejected: INSTANCES (Option A — one custom ctor, the three derived from it) — truer to minimality but routes the currently-CLEAN trusted-three THROUGH unproven general-handler soundness, risking a census regression; kept as a LATER census-preserving refactor once the general soundness + multi-shot grade (Q27) are settled. The single riskiest obligation is invariant #4 — the calculated-machine re-derivation (generalize SStore/THeap → a param store, DERIVE the custom evalD/compile/exec arm), entangled with the route-B metatheory TAIL (ADR-0052's core LANDED — see Amendment 2026-07-08; U5b-handler completeness + the binary-LR re-index + the coherence-layer generalization remain). | — / — | — / — | — | 0022, 0023, 0025, 0052, 0054, 0055, 0063, 0070 |
| 0086 | Accepted | compile_forward_sim re-freeze: VcapFree + CustomFree premises (true-but-unprovable, made provable) | The ◊5 headline compile_forward_sim (Spec.lean:292) quantifies over RAW Comp with no premise, and the #16 completeness spine (the converse-of-run_evalD bridge, origin/inc6-u5b2) proved its only known proof architecture CANNOT reach two program classes the statement includes: (i) non-VcapFree programs (a buried never-forced vcap completes in the kernel while failing the FreshCfg the evalD-bridge needs — machine-checked, scratch/VcapFreeRefute.lean) and (ii) Handler.custom-containing programs (evalD custom = none by ADR-0085 Stage-1, while the kernel and the WASM machine both handle custom generically). Both witnesses ALSO machine-check that the headline is TRUE on those classes (both sides complete identically, all rfl) — so this is "premise an unprovable true statement," NOT "repair a false one." Decision (operator ruling 2026-07-09, option a2): re-freeze compile_forward_sim with BOTH premises — VcapFree c → CustomFree c → … — making the headline provable sorryAx-ZERO from the banked spine. Both premises are vacuously true for every elaborator-produced program (the elaborator emits vvar not vcap; no surface form produces custom until ADR-0085 Stage 7), so the product-facing meaning of ◊5 is unchanged. CustomFree is TEMPORARY scaffolding: ADR-0085 Stage 4 (the derived custom machine arm) DROPS it — a premise-drop is a consumer-safe strengthening. VcapFree persists until raw vcap becomes untypeable (#21 scoped capability types), after which it is derivable. Rejected: (a1) VcapFree-only (same re-freeze ritual, strictly weaker endpoint — the custom arm stays a sorryAx); (b) no re-freeze (the heart-of-the-contribution headline stays flagged until the full #44 metatheory arc); proving the unpremised form (no known architecture; the bridge NEEDS FreshCfg, witness-refuted derivable). | — / — | — / — | — | 0016, 0035, 0052, 0063, 0085 |
| 0087 | Accepted | #44 Stage 2′: finite clause representation — enumerability by construction dissolves the capsH wall | The #44 arc is blocked at ADR-0085's Stage-2 finding: making Handler.custom dispatch real regresses the clean CalcVM coherence headlines because capsH : Handler → List (Nat × Label) must BOUND a config's capabilities, and the coexist rep's clause map is an opaque OpId → Option Comp whose caps cannot be collected (the domain is not enumerable; capsH (.custom …) = [] is currently sound ONLY by Stage-1 inertness). ADR-0085 sketched the fix as a THREADED well-formedness invariant ("custom clauses are VcapFree") through CapLabelCoh/FreshCfg/the machine proofs. This ADR proposes the stronger move: change the representation — Handler.custom : Label → Val → List (OpId × Comp) → Handler (a finite association list) — making cap-enumeration STRUCTURAL. capsH's custom arm becomes clauses.flatMap (capsC ∘ ·.2) — total, honest, compositional — so CapLabelCoh/FreshCfg statements do not change and gain no premise: clause caps are bounded by the SAME machinery as every other cap, and the clean headlines stay clean by construction rather than by a side condition. The finite rep also matches the surface (an effect declaration and a handle … with { … } block are syntactically finite clause lists), makes handlesOp a decidable lookup, gives renameH/substFrom/shiftFrom an ordinary .map traversal, and eases Stage-3 typing (pointwise over the list). Cost: rebase the banked Stage-2 semantics (origin/gh44s2, one ~180-line WIP commit) from function-application dispatch to list lookup, and give up infinite op families — which EffSig-declared effects never produce (an effect decl is finite by construction). Rejected: (a) the threaded VcapFree-clause invariant (detection where construction is available: every machine theorem gains a premise + a preservation-lemma surface, violating the make-illegal-states-unrepresentable principle); (b) a subtype/bundled rep {cl // ∀ op c, cl op = some c → VcapFree c} (carries dependent proof obligations through every construction site for less than the list buys). Probe-first before the arc commits (falsifiable rungs below). | — / — | — / — | — | 0085, 0086, 0055, 0063 |
| 0088 | Accepted | #48 effectful recursion: row-carrying recursive thunk type, row DECLARED not inferred | A let rec body currently cannot carry ANY latent effect — the μ-encoded knot's type recTy = μX. Thunk(X → T) forces the recursive thunk PURE (tThunk ⟹ ⊥), so the #45 fold-payload check (φ' ⊆ φ, φ=⊥) REJECTS a body that raises, touches state, or calls a Div helper (#48; found in #47's soundness audit, case ⑤). This is sound-by-rejection but a T1-ergonomics completeness gap: a recursive parser that performs, or a recursive fold calling a partial helper, cannot be written. Decision: implement #46 Option B as a row-carrying recursive thunk type — recTy = μX. Thunk_ρ(X → T ! ρ) — with ρ DECLARED in the let rec type annotation (let rec f : Int -> Int ! {throws} = …), never inferred by fixpoint. The body checks against declared ρ (φ_body ⊆ ρ — the #45 arm generalizes from φ=⊥ to φ=ρ); inner self-calls type at ρ (retiring Option A's inner-⊥ under-approximation); the effective knot row stays ρ ∪ (structOK ? ∅ : {Div}) so #47's termination certification keeps eliminating Div orthogonally. Elaborator-only (elaborate-to-mono, ADR-0075 pattern): the kernel, census, and frozen statements are untouched. Rejected: fixpoint row inference (implicit where explicit is available — violates the agent-first lens and the config-explicit-at-boundaries principle; more machinery for a worse contract), and effect-polymorphic recursion (needs #56's full Rémy treatment; nothing v1 writes requires it). | — / — | — / — | — | 0073, 0074, 0019, 0020, 0075 |
| 0089 | Accepted | Package layout mirrors the stratification — multi-package Lake workspace | The repo has outgrown "one lib + a CLI": the tested superset now spans a parser/elaborator/formatter frontend, a REPL-bearing CLI, a witness layer (differential fuzz #14, outcome-oracle #54), and non-Lean tooling — while the verified spine stays the proof-budget core. The stratification seam (verified core / tested superset, ADR-0026/0028) is currently enforced one rung DOWN the derivation ladder: tools/arch-check.sh tests that Bang/Frontend has fan-in 0 from the spine. Decision: restructure into a multi-package Lake workspace whose dependency arrows ARE the stratification — bang-spine (Core+Backend+Meta+Spec+Audit, the only Mathlib consumer) ← bang-frontend ← bang-witness, with the bang exe atop frontend — so a spine module importing the frontend becomes UNBUILDABLE (a require-cycle error), not merely a red script. Module NAMES do not change (imports stay Bang.Core.…/Bang.Frontend.…), so the churn is lakefile surgery + CI/cache plumbing, not an import rewrite. Crucially rejected as insufficient: splitting into multiple lean_libs inside one package — Lake resolves imports package-wide regardless of lib membership, so that split is organizational cosmetics at the same enforcement rung we already occupy. Also rejected: multi-REPO split (kills the shared proof context, atomic cross-strata commits, and the single just verify gate for zero added enforcement over a workspace). Timing: entry-gated on the #44 rung-2 landing — the spine is mid-surgery (feat-44-rung2); restructuring under it would force a rebase across a package boundary. | — / — | — / — | — | 0026, 0028, 0016 |
| 0090 | Accepted | #58 formatter multi-line layout — ride Lean's Std.Format Wadler engine, zero-config | The v1 canonical formatter (Bang/Frontend/Format.lean, #58) is FLAT (single-line): it prints one deterministic line per Surf/Ty/Decl/Prog, with minimal-parenthesization driven by the shared opInfo precedence table (ADR-0071) and two corpus #guard laws (roundTripsOn = the AST never changes; idempotentOn = fmt-of-fmt is a no-op). Multi-line/wrapped layout was left open. This ADR settles HOW multi-line layout is added. Decision: build the layout on Lean's host Std.Format — a Wadler Doc algebra (group/nest/line/align/fill, pretty (width := 120)) already in the toolchain — rather than hand-roll a second Wadler kernel (option B) or adopt the Final Pretty Printer's extensible-monadic architecture (option C, whose novelty — proportional fonts, interactive presentations, Web — is orthogonal to bang's monospace-.bang-file target). The printer stays ZERO-CONFIG (one fixed width constant, no user knobs — the gofmt/dart_style/black consensus, and the generative constraint that gives a canonical formatter its whole value). The two existing laws EXTEND unchanged: roundTripsOn/idempotentOn are stated over the parsed Prog, independent of whether the printed text is one line or many, so multi-line output must still satisfy both #guards. examples/ are NOT reformatted by this ADR (the corpus's teaching role — hand-written idiomatic style — is preserved; a corpus entry is verbatim source, and reformatting it would destroy the very variety the round-trip #guards exercise). CLI -w/in-place is DEFERRED to a follow-up (the #58 CLI half wires bang fmt to stdout first). Rejected: (B) hand-rolled Wadler kernel — a second layout engine beside Std.Format, violating one-construct-per-problem, buying #guard-able Doc laws bang doesn't need on a fan-in-0 leaf; (C) Final Pretty Printer — pays for extensibility bang's target makes moot; (biparsers/FliPpr, rung 3) — solve EXACT printing (recover source text), the deliberate opposite of bang's CANONICAL printing, at the cost of a full Pratt-parser rewrite. Layout engine is the recommendation; the width VALUE (survey recommends 80/2-space) is a preference the operator rules. | — / — | — / — | — | 0046, 0071 |
| 0091 | Accepted | #50: structOK multi-arg certification — single-fixed-slot descent | structOK (#47) certifies single-arg structural recursion as total (⊥-row, no Div); multi-arg/accumulator recursion — the shape the tokenizer dogfood deliberately AVOIDED (ce6d738) — still conservatively types Div even when descent is plainly structural. The design note (docs/notes/structok-multiarg-design.md, code-grounded at TypeCheck.lean:1608-1662/:1728-1734/:1690-1694, gap verified LIVE against fresh main) surfaces a genuine fork. Decision: (A) single-fixed-slot descent — exactly ONE designated argument position, the SAME slot at every recursive call site, must be a strict data subterm at each call; all other slots (accumulators) ride free. Covers both corpus shapes (curried accumulator, tuple accumulator) at cost proportional to the existing checker (~55 lines generalized pair→n-indexed list + the shadowing-arm port). Soundness posture preserved by construction: the check is n copies of the already-sound bare-variable single-slot rule, and fixing ONE slot across all call sites forecloses the one known break (two per-site measures each idle on the other's turn); false-certification stays impossible, not merely unlikely. The five adversarial guards port to curried/tupled form as the regression corpus. Rejected: (B) full lexicographic descent — no corpus example needs it, real annotation/inference cost, cuts against the ADR-0088 explicit-over-inferred precedent; NOT foreclosed ((A) is (B) with slot-list length 1 — layer it later if a genuine zip/merge-shaped two-structural-argument case surfaces). (C) numeric well-founded measures — out of scope, tracked behind Q31. | — / — | — / — | — | 0073, 0088 |
| 0092 | Accepted | #44 Stage 3: typing user-defined effects — program-derived EffSig + the typed custom-handle rule | Stage 2 landed custom dispatch census-clean (6413281), but custom is still UNTYPED: no HasCTy rule mentions it, and the typed trusted-three stay clean only via vacuity (HasStack.concat_custom_absurd — a custom frame cannot sit on a typed stack). Stage 3 makes user effects TYPEABLE. The grounding fact that shapes everything: the kernel metatheory is already parametric in [EffSig Eff Mult] and the performer side (perform/up via EffSig.opArg/opRes) is already fully general (ADR-0085's own finding) — so op typing needs NO new kernel mechanism. Decision: (D1) user effect declarations allocate labels deterministically in the elaborator (ℓ ≥ 4, decl order — the four built-ins keep 0–3; the kernel is label-agnostic, Label = Nat, zero kernel change); (D2) the elaborator CONSTRUCTS the concrete EffSig instance from the program's effect decls (finite-map opArg/opRes over the declared ops) — the typed judgment runs at the program-derived instance, so the parametric soundness theorems apply to user effects BY INSTANTIATION, not by new proof; (D3) one new typed rule, handle-custom, mirroring the three built-in handle rules: clauses typed pointwise over the finite list (body : opRes ! φ under param + arg bindings, one-shot tail-resumptive), the B-occ anti-escape premise (¬ LabelOccurs ℓ A) carried verbatim; v1 types the READ-ONLY-param form only; (D4) the vacuous custom arms in preservation/progress become REAL additive arms (the ADR-0085 additive-ripple pattern; frozen statements untouched), probe-first per the ADR-0087 rung discipline — the preservation-of-dispatch slice is the bet. Deferred, named: (D5) the param-UPDATE protocol (put-like ops mutating the carried param — ADR-0087 §Open-questions; semantics not yet landed either, deferred with ADR-0085's Stage-4/first-class-k note; read-like user effects (Net/read, ADR-0084's motivating case) do not need it). Rejected: a universal open EffSig instance keyed by runtime maps (loses by-construction totality of op signatures; the program-derived instance is total over declared ops by construction), and typing custom via a NEW judgment separate from HasCTy (two judgments for one problem — the coexist seam already quarantines risk at the constructor, not the judgment). | — / — | — / — | — | 0085, 0087, 0022, 0046, 0054, 0055 |
| 0093 | Accepted | Module system v1: file-modules, qualified-by-default imports, elaborate-to-flat | Q34's revisit signal has fired — the dogfood arc reached multi-file need (a JSON parser wanting the tokenizer's machinery; the operator names modules as the pending blocker for real projects). The ARCHITECTURE is already pinned (ADR-0076, Accepted: modules elaborate to the FLAT kernel · the compiler is a queryable service · the module DAG is acyclic + generated); this ADR decides Q34's v1 SURFACE forks inside those pins. Decision: (D1) one module = one FILE — import tokenizer resolves tokenizer.bang relative to the importing file (then a project root); the module's name IS its filename, no module header, no blocks; (D2) qualified access by default (tokenizer.lex input) + EXPLICIT selective use tokenizer (lex, Token) — no glob/open-all import exists (implicit namespace pollution is the anti-agent-first move; a use collision is a LOUD error, ADR-0046); (D3, operator-amended 2026-07-09) declarations are PRIVATE by default; pub marks a declaration exported (riding the Rust convention — the dominant pattern-match for exactly this semantics). Private-by-default is the consistent agent-first choice: the module's interface is DECLARED at the definition site, nothing exports by accident, and use/qualified access can only name what the author deliberately revealed (the Q34 interface-reveal lesson, made structural); (D4) semantics = whole-program elaboration: imports parse + merge with name-qualification at the Surf level, THEN the existing single-program pipeline runs unchanged — the kernel never learns modules exist (the ADR-0075/0088/0091 elaborate-away move, fourth application); import cycles are a loud error (the 0076 DAG pin); the prelude stays the one always-open implicit module. Q38 posture (deliberate): v1 mints NO new interface construct — a module is a file, not a signature; the module≟trait≟effect unification stress-test stays fully open for Stage 7, when the effect declaration surface (ADR-0092/0085-D4) either converges with trait syntax or diverges-documented. Deferred per Q34's own sequencing: the stdlib partition (prelude scales for now), the hashing boundary + incremental build, the LSP query surface (its non-deferrable prerequisite — spans in the checker — already landed via #52/#59). Rejected: module blocks (Lean-style module { } — nesting no v1 program needs; not foreclosed, a file is trivially one block); glob imports (use tokenizer * — resolution becomes context-dependent, breaking both ADR-0046 determinism and agent pattern-matching); an export (…) LIST as the visibility mechanism (a second place to look — the def site should carry its own visibility; kept conceivable as future sugar over pub); default-PUBLIC (the draft's original D3, operator-rejected — exports-by-accident and an undeclared interface). | — / — | — / — | — | 0076, 0075, 0046 |
| 0094 | Accepted | Environment semantics in the machine layer; the substitution spec stays | #61's measured cliff (per-step Comp.subst at ~1 ms/step — O(knot-body-size) per unfold; docs/notes/hang-61-diagnosis.md) is a reduction-STRATEGY cost, not an encoding bug, so the fix is representational: introduce an environment/closure representation in the calculated-machine layer (evalD → exec), leaving Source.eval unchanged as the substitution SPEC (option A1 of docs/notes/envsem-survey.md). evalD_agrees_source is re-proven as the substitution↔environment correspondence (the PLFA γ≈ₑσ pattern — mechanized prior art, not an invention); the machine gains one variable environment ρ + closure values alongside the untouched effect stores (SStore/THeap are effect-state, not var-env); bang run's default flips to the compiled engine so real programs hit the fast path while the oracle stays the slow, simple reference. The whole ~1900-occurrence substitution proof spine (Soundness 427 · both LRs 453 · Freshness 103) is preserved, not rebased — that asymmetry is the argument. Predicted gain: ~10⁴–10⁵× on the per-step constant (survey §5); the cliff dissolves, it isn't softened. Rejected: (B) env semantics in the spec — discards the paid-for substitution metatheory bang already owns (CakeML never paid it, so its day-one envs prove nothing for us) and blurs invariant #4's spec/machine split; (C) explicit-substitution calculus λσ — imports a known SN-failure hazard to solve a perf problem envs solve cleanly; (E) hash-consing — shares subterms but the reducer still walks O(body) per step. (D) thunk-sharing at the knot is DEFERRED as the fallback stopgap, not rejected — named cost: memoized force breaks step-monotonicity, owing backward simulation (PureCake §5.4), so it is small–medium, not small; if A lands, skip D entirely. | — / — | — / — | — | 0016, 0035 |
| 0095 | Accepted | #44 Stage 7: the handler surface — handle … with syntax, the Q38 posture, and the clause calling convention | Stages 1–6 landed the kernel arc for user-defined effects (Handler.custom rep, one-shot dispatch, the typed custom-handle rule, and the trusted-three census clean through soundness — ADR-0085/0092, ADR-0085 §Stage-6 STATUS MET). What remains is Stage 7: the surface a user writes and the end-to-end bang eval that lowers it. The effect Name { op : A -> B } half of the declaration surface already landed at Stage 3 (ADR-0092 §Status D1/D2 EXECUTED 844931f+88e0f55); this ADR decides the handle … with half. It is also the stress-test the operator deferred Q38 TO (ADR-0093 §Q38-posture: "module-as-file deliberately left no construct to collide with it … run the stress-test THEN") and the decision issue #78 was parked TO (the trait-ops calling-convention fork). Five decisions, each operator-ruled: (D1) the concrete handle e with Name { op(arg) => body } syntax — the Flix/Effekt method-impl clause shape (def op(args, resume) = body), recommended over the Koka match-arm and OCaml exception-style forms because it (a) is syntactically identical to a trait impl (serving Q38 for free), (b) degrades to v1's ret-shape/one-shot constraint by treating resume as an implicitly-tail-called bound name, and (c) grows to multi-shot by loosening the TYPING rule, not changing the surface (rq38 §1 degradation verdict) — amended D1a (2026-07-10): the handled body names the capability via a REQUIRED explicit as h binder, handle e with Name as h { … }, scoping over the body (the ADR-0070 state … as name precedent; implicit-lowercase rejected — silently-shadowing nested same-effect handlers — and the optional-default sugar deferred as purely additive), with the decl-order-dependent label resolved at elaboration into a slot on the Surf constructor so lowering stays ElabEnv-free; (D2) the Q38 posture — a SEPARATE handle construct now, NOT syntactic convergence with trait/impl, per the taxonomy's "unify the MACHINERY, keep the surfaces separate until this stress-test rules" (laws-taxonomy §5 caveat) and the census finding that every unification pays at the implementation layer, not the interface (rq38 §2); the interface ALREADY unifies in bang's glossary, so convergence buys nothing and costs the binding-time knob; (D3) the clause calling convention — effects are CURRIED (op(x) => body is sugar for a curried clause, op performed as $cap.op arg curried), decided ONCE with #78's tuple-vs-curried finding in view; the existing trait ops (tuple-style fn eq(a,b), stranger-test-2 §S3 papercut) DIVERGE-documented in v1 and are flagged for convergence to curried in a follow-up (#78 option B), NOT retrofitted here; (D4) the ret-shape restriction (ADR-0092 §D3-as-landed: v1 clause bodies are ret w) surfaces as a SPECIFIC diagnostic ("clause body must be a ret-shape value in v1; compute-then-return needs binop typing (ADR-0065) + grade surfacing (Q27)") naming the exact entry gate, NOT a bare type error; (D5) resume's surface spelling — IMPLICIT tail-resume in v1 (a clause body that is ret w resumes with w; no resume binder needed), with resume RESERVED as a binder name so the explicit resume(w) form and the eventual multi-shot first-class k (Q22/Q27) slot in without a surface break. What Stage 7 does NOT do (explicitly scoped out): the IO prong is ADR-0084's own unit (unblocked BY this stage, not part of it); multi-shot / first-class k stays Q22/Q27 (v1 one-shot pin, ADR-0085 D2); param-UPDATE (put-like clauses) stays ADR-0092 D5 / ADR-0087 §Open-questions; op-name namespacing end-to-end (Net.read dissolving the builtin-name reservation) is named by ADR-0092 §Status as Q34/Q38 module-interface work and rides the module system, not the handler surface. Rejected: the Koka match-arm form (handle(e){ op(x) -> body } — reads as exception-handling, obscures the interface-impl framing that serves Q38); the OCaml effect Op k -> form (exposes k as a first-class binder v1 cannot honor one-shot, and reads as exception matching); syntactic convergence of handle with trait impl in v1 (the taxonomy's implementation-layer-pays finding says the interface unification is free and the surface convergence is the untested claim — this ADR keeps them separate to KEEP the stress-test honest, not to foreclose it); tuple-style effect clauses matching today's trait ops (would double down on the #78/stranger-test-2 §S3 inconsistency the language should shed, not entrench); an explicit-k binder in v1 (ADR-0085 D2 one-shot pin means a visible k would over-promise a control the kernel cannot deliver). | — / — | — / — | — | 0085, 0092, 0093, 0070 |
| 0096 | Accepted | The LR id-uniqueness (freshness) carrier — the item-1 SKIP-relocation wall | The last proof-layer wall gating lr_fundamental/lr_fundamental_closed (and one of lr_sound's two residuals) is the krelS_splitAtId_decomp SKIP-arm resume relocation (BinaryLR.lean:1030, task #29 item 1). Machine-characterized on krnl3's feat-lr-final-wall @ 2b0948e: the relocation is a config-append INVERSE that needs splitAtId cfg₁.1 nid = none — an id-uniqueness/freshness fact — where the captured continuation cfg₁.1 = Kᵢ ++ reinstall :: Ki' has Kᵢ UNIVERSALLY quantified (any captured continuation). Both viable routes need it: the self-recursive strip (route B) and the un-append (route A). Route A elaborates and terminates (AppendInvWF.lean) but is answer-type-refuted at its last obligation (Dⱼ = Dᵢ fails at P=[]: Dᵢ=X vs Dⱼ=F qᵣ Aᵣ); the caller-discharge of a uniqueness premise (route B′) is refuted because the LR is freshness-free BY DESIGN — ADR-0058 route-1 dissolved Canonical/CapsBelow/run_bump, so no WellCounted/FreshCfg carrier is in scope to discharge it. The carrier that must be RE-INTRODUCED already half-exists: CrelK/KrelS ALREADY thread the real fresh-id counter g internally (ADR-0058 route-1 landed), and the kernel ALREADY has the exact well-formedness predicate (StackBelow g K, Invariants.lean:39, axiom-clean) and its consequences (splitAtId_fresh, stackBelow_splitAtId, wellCounted_reachable). What is MISSING is the assertion tying g to the stacks: StackBelow g K₁ ∧ StackBelow g K₂. THE REACHING TEST (machine-decided, da03e68 witness pair BWitnessUniqueInResume.lean, axiom-clean [propext]) narrows the shape space to a def-change: the strip's needed fact lives on the resume conjunct's captured continuation Kᵢ, which KrelS binds UNIVERSALLY — strip_mislocates_when_nid_in_prefix refutes reaching it from a top-level premise (a concrete Kᵢ = [handleF nid _] mislocates the split), while strip_with_fact confirms the strip closes once the fact IS on Kᵢ. So the pure top-level shapes are REFUTED: (ii) a lemma-chain premise and (iii) a consumer-side side judgment both CANNOT reach the bound Kᵢ and are struck. The surviving shapes both put the fact inside KrelS: (i′) a KrelS def-invariant on the two stack args (the recursive resume-conjunct hyp KrelS m … g Kᵢ Kᵢ' then propagates StackBelow g Kᵢ for free — self-propagating, matches the WellCounted precedent), or (i″) a fresh premise directly on the resume conjunct (surgical, but the discharge threads at every producer). RECOMMEND shape (i′) for its self-propagation — re-introduces only the fact, not the machinery (no Canonical, no run_bump, no faked counter), and forces no frozen-statement change (the Spec.lean lr_* statements never mention g/KrelS/the carrier). The proof-layer close is ready to consume (strip_with_fact + the banked KrelS_length_eq); the cost is the FROZEN DEF-block change (LR.lean:1131) rippling to the ~20 krelS_* eq-lemmas, self-propagating so each intro maintains it inductively. Load-bearing honest correction to the task-#29 census claim: the carrier closes lr_fundamental + lr_fundamental_closed (census 18→20), NOT lr_sound — lr_sound carries a SECOND, independent residual (the Q22 reshape↔raw-focus bridge, Spec.lean:252), and the stackBelow_handlerCount_of_hasStack obligation the carrier would impose on krelS_refl at lr_sound's g := handlerCount C instantiation is UNPROVABLE from HasStack alone (FreshCarrierDischargeProbe.lean) — that IS the Q22 seam. So lr_sound's third shed needs Q22 co-resolved; 18→21 is only reachable if this ADR is landed together with the Q22 bridge, not by the carrier alone. PARK priced: ship v1 with the three lr_* flagged; the ◊4 binary-LR paper (docs/papers/binary-lr-skeleton.md) becomes a CPP-framed "machine-checked LR construction + the seam analysis" with lr_fundamental a single named residual — honest, publishable now, but the POPL/ICFP "closed contextual-equivalence result" claim stays out of reach. | — / — | — / — | — | 0058, 0055, 0057, 0016 |
| 0097 | Accepted | Deriving handlers: Eq/Ord as a structural fold over the ADR-0069 μ-sum-of-products | A data Foo = … deriving (Eq, Ord) clause runs an elaboration-level handler | — / — | — / — | — | 0068, 0069, 0079 |
| 0098 | Accepted | The prelude is a real Prelude.bang module, auto-used | Issue #106 (operator-ruled 2026-07-11, unblocked same day when #97 item-3 turned out | — / — | — / — | — | 0093, 0074, 0079, 0081, 0046 |
| 0099 | Accepted | Constructors are type-namespaced — bare names resolve when unambiguous in scope | A data constructor's true identity is (dataName, ctorName), not ctorName alone | — / — | — / — | — | 0069, 0079, 0093, 0098 |
| 0100 | Accepted | G1 compute-then-return clause bodies ship as a tested-superset feature (the kernel carve-out is refuted) | A ⊥-row COMPUTING custom-handler clause body (compute-then-return, e.g. | — / — | — / — | — | 0065, 0092, 0095, 0026, 0028 |
| 0101 | Accepted | Concurrency model: scheduler-as-handler; components/threads are backends, not the model | Concurrency is an ORDINARY effect (a conc/Sched row label) and a scheduler is a | — / — | — / — | — | 0007, 0016, 0059, 0030, 0001, 0018 |
| 0102 | Accepted | Mutual let rec … and …: H2 tuple-of-thunks μ-knot (#97 item 2) | let rec f : T1 = e1 and g : T2 = e2 … in body generalizes ADR-0073's single-function | — / — | — / — | — | 0073, 0091, 0071 |
| 0103 | Accepted | ∀-generalization for bound-free self-recursive generics: a call-site-monomorphization pre-pass (the List-family door) | A bound-free self-recursive generic (length : List a -> Int, the whole List family: | — / — | — / — | — | 0075, 0080, 0079, 0073, 0069 |
| 0104 | Accepted | Host IO as effects + handlers, driven by an environment seam with record/replay conformance | Host IO (Console, Clock now; Fs, Net later) is an ORDINARY effect in the row, | — / — | — / — | — | 0084, 0092, 0095, 0093, 0094, 0063, 0101, 0016, 0059 |
| 0105 | Accepted | effect_sound trace semantics: the runtime live-bound (Q14 ruling) | effect_sound (Bang/Spec.lean:191, a ◊2-block soundness theorem) was flagged with three | — / — | — / — | — | — |
| 0106 | Accepted | trait-op name-call dispatch (#78 operator ruling) | #78 (trait ops were operator-dispatch-ONLY — env.insts consulted exclusively at | — / — | — / — | — | 0005, 0006 |
| 0107 | Accepted | effect-row reuse: subeffecting at reuse sites, open-row ascription deferred (#94) | #94 (unifyRow's single-shared-row-var "first cut" rejected reusing ONE | — / — | — / — | — | 0001, 0018 |
| 0108 | Accepted | Contributor reference and onboarding contract | The contributor-reference system optimizes first for a general language implementer, while branching into specialist human and agent routes; uses one public Vocs site with a curated product/contributor split and keeps volatile work state repo-only; ships deterministic caption-led generated media with transcripts and reduced-motion fallbacks, without requiring narration; and teaches one journey through two fixtures — a tiny thunk/force precursor followed by the logger-counting handler example. These choices settle Plan 014 Phase 0 and make Phase 1 executable. | — / — | — / — | — | 0077, 0078 |
| 0109 | Accepted | Page manifest is the publication and navigation authority | One schema-validated page manifest defines the public Vocs publication map and generated navigation; Vocs, repository-page projection, tour generation, and route checks consume one compiled site model. Volatile current-work pages remain repository-only links, and displayed evidence status resolves from serialized Phase 2 facts rather than styling or copied labels. | — / — | — / — | — | 0077, 0078, 0108 |
| 0110 | Accepted | Preserve the Wasm proof-model to concrete-emitter boundary | Route B preserves an explicit boundary between the project-defined Wasm-oriented abstract machine proved by compile_forward_sim and the separately implemented concrete WasmGC/WAT emitter. The product target remains Wasm 3.0, while emitted modules earn differential evidence from real-engine execution rather than inheriting the abstract model's theorem evidence. | — / — | 0016, 0059 / — | — | 0016, 0035, 0059 |
Resolved questions (derived from ADR Resolves: fields)
| Question | Resolved by |
|---|---|
| Q3 | 0019 |
| Q4 | 0022, 0023 |
| Q5 | 0022, 0023 |
| Q6 | 0023 |
| Q8 | 0032 |
| Q10 | 0019, 0020 |
| Q11 | 0020 |
| Q12 | 0025 |
| Q13 | 0023 |
| Q17 | 0027 |
| Q18 | 0029 |
| Q19 | 0040 |
| Q25 | 0067 |
| Q28 | 0073 |
Canonical exemplar
Read 0016-two-hop-architecture-calcvm-and-wasmfx.md first when writing
a new ADR. It exhibits the format we want: Context (1-3 paragraphs),
Decision (concrete + actionable), Why this model (numbered list of
reasons), What it commits to (the consequences), Consequences for other
ADRs (subsumptions/deletions), Rejected alternatives (each with "why
not"), Revisit if (the legitimate reconsideration triggers).
Template stub: adr-template.md in this directory (or copy 0016 and edit).
When to write an ADR
- The choice is reversible by a future session — without an ADR, they WILL reverse it.
- The "why" is non-obvious from the code alone.
- Rejected alternatives are worth recording (saves re-thinking).
- The decision spans multiple files / subsystems.
Skip ADRs for: bug fixes, refactors that don't change semantics, formatting, typo fixes. Those go in commit messages.