AGENTS.md — read this first

What BANG is

A small language whose paradigm and runtime are values, not language features. The kernel is thunks + effects + STM; everything else (mutability, IO, async, actors, signals) is ordinary library code over it. Programs are descriptions until forced with $ (ADR-0007; ! is actor-send); a function's paradigm is which effects are in its row; a program's runtime is a handler installed at the use site.

First time in this repo? Read ONBOARDING.md for setup + a tighter reference index.

Reference index

This file is the always-loaded core: invariants, glossary, architecture-in-force, verify-command. Everything else is on-demand — consult the relevant doc when its trigger arises.

Architecture in force (third design revision)

Two-hop verified compilation per ADR-0016 as revised by ADR-0059:

  source → graded-CBPV semantics → CalcVM (Bahr-Hutton) → project Wasm-oriented abstract machine
  graded-CBPV Comp → separate WasmGC/WAT emitter → Wasmtime differential tests

The CalcVM is the executable spec; Wasm 3.0 is the product target (ADR-0059: grade-directed lowering — pure→native, abort→exceptions, tail→direct call, general→the GC-frame-chain runtime, the one pluggable slot where WasmFX switch/resume becomes a fast-path once standardized; stack switching did NOT land in Wasm 3.0). The CalcVM→Wasm hop is proven by annotated forward simulation (compile_forward_sim, ADR-0035) only against the project Wasm-oriented abstract machine — NOT the concrete WAT emitter, official Wasm semantics, or the biorthogonal/Benton–Hur LR, which proves ◊4 contextual equivalence (a separate theorem, the binary LR). Concrete emission is differentially tested; ADR-0110 preserves the open proof link. ADRs 0003 and 0004 were deleted, subsumed by 0016. See CONTEXT.md for where the implementation stands; docs/notes/k3-historical-status.md for what the K3 work taught (preserved as input to the graded-CBPV port at ◊3).

The stratification principle (the load-bearing mental model)

One shape governs the whole project: a verified core + a tested superset, separated by an explicit, type-visible seam. It recurs at three levels (ADR-0026 / ADR-0028):

level         verified core              tested superset             seam
──────────────────────────────────────────────────────────────────────────────────
correctness   verified (proof)           tested · unsafe             the ADR-0026 ladder
tooling       Lean (kernel·CalcVM·       surface · runtime           typed AST + differential test
              compiler·LR)               (diff-tested vs Lean)
language      total fragment             Div fragment                the EFFECT ROW (Div = descent)
              (⊥-row, System F)          (fuel-bounded, Turing-compl.)

Descent (verified → tested) is always explicit and marked, never silent. The expensive proof budget is spent only on the verified core; the superset rides differential-testing + fuel. (Source.eval's fuel-bounded interpretation of the partial Comp already demonstrates the language-level seam — a total prover interpreting a Turing-complete object language.)

Invariants — never break these

1. Proof rides the reference. Anything that runs is either exec itself or differential-tested against it. Never ship an execution path with no oracle behind it.
2. Effect rows are sets — idempotent, union = join. Never ordered, never a multiset. (ADR-0001) Post-Q1: [Lattice Eff] [OrderBot Eff] (ADR-0018).
3. STM is the only privileged kernel primitive. Everything else is effect + handler. (design doc; preserved by ADR-0016.) ADR-0030: privilege is concurrency-only — single-threaded STM is a transactional handler, so v1 ships STM as a handler; the privileged shared-heap form returns with concurrency (post-v1). STM stays a named member of the five (below), unused-as-privileged in v1.
4. The machine is an output of the calculation, never hand-designed. Calculate, don't verify-after-the-fact. (ADR-0016, formerly ADR-0004)
5. Kernel stays at five primitives: thunk · force · effect rows · handlers · STM. Adding a sixth is a spec change requiring an ADR.
6. No implicit capture; reactivity is the operator, not a keyword. (ADR-0005, ADR-0006)
7. Performance is second-class. Optimize only where it touches the user; a slow correct path beats a fast unverified one.
8. Effect TS is not the target. The calculated VM is canonical; Wasm 3.0 is the product target. The checked simulation reaches the project abstract target, while the separate concrete emitter is differentially tested. WasmFX is a future fast path for the post-v1 general-resumption slot. (ADR-0016 as revised by ADR-0059 and amended by ADR-0110; supersedes ADR-0003)

Do NOT

• add a kernel primitive · make rows ordered · reintroduce sig · add implicit lexical capture
• hand-design the VM, then justify a compiler against it
• optimize speculatively, or add a feature the spec's Non-Features section forbids
• prove most-generality (MGU) for unification — soundness is the contract; MGU goes to the differential test

Ubiquitous language (glossary)

Doc discipline

• History lives in git, not in docs. When a fact is no longer current (e.g., "K3 was in progress until the pivot"), the commit history preserves it. Docs describe present state. Past-tense narrative belongs in commit messages or docs/notes/<topic>-historical-*.md for genuine archival value.
• Genuine design decisions that future sessions might reverse → ADR in docs/decisions/. ADRs record the alternative considered AND rejected with rationale (not just the chosen path). ADRs are forks-in-the-road, not changelogs.
• Volatile state (current position, active path, blockers) → CONTEXT.md or paths/PATH-*.md.
• Always-useful (invariants, glossary, architecture-in-force) → here (CLAUDE.md). Every token in this file is loaded into every session; bloat is expensive.
• On-demand reference → docs/notes/* indexed in the Reference Index above.
• Before grilling or opening a design question, read the generated decided-ledger (docs/decisions/README.md) — a question with an ADR is closed, not open. grep docs/decisions/ first. The ledger is generated from each ADR's frontmatter (just adr-index); just adr-check keeps it ≡ the ADRs + OPEN_QUESTIONS (ADR-0042).

How to verify (the cheapest orientation)

nix develop          # ENTER THE DEV SHELL FIRST — bare `lake`/`just`/`node` are NOT on PATH
just verify          # selfcheck (Node) + lake build + tools/audit.sh
# or piecemeal:
just check FILE      # fast single-file Lean error check
just build           # one lake build Bang bang + full library/runner warning ratchet  (cold: minutes)
just audit           # bash tools/audit.sh
just burndown        # Phase B sorry/axiom counts per module
just axioms          # lake env lean Bang/Audit.lean — #print axioms per theorem

First lake build pulls Mathlib via lake exe cache get (network; minutes). Green means: lake build succeeds without exceeding the module/category warning budget, axiom set per headline theorem ⊆ {propext, Classical.choice, Quot.sound}. If you can express a new invariant as a runnable check, do that instead of writing it in prose — checkable beats described.

Gate-traps (cause false-greens): read errors via lake build exit code or grep -E "error" — plain grep "error:" MISSES error(lean.unknownIdentifier):; gate sorries via #print axioms / just axioms, NEVER grep sorry (false-positive on comment prose, false-negative on transitive deps). Gate the COMMITTED sha on a clean tree — never an agent's summary or a dirty worktree.

When you make a decision

If you make a choice that a future session could reasonably reverse or relitigate, write an ADR in docs/decisions/ (copy the format of an existing one; 0016 is a good exemplar). Record the rationale and the rejected alternatives, not just the choice. Anti-drift is mostly anti-reversion, and reversion happens when the "why" is missing.