The effect system can now discharge an effect, not only track one

ARCHITECTURE.md

@@ -7,7 +7,7 @@ text. It is the leverage the text-token floor denies the language track (see
 [IDEAL_AGENTIC_LANGUAGE.md](IDEAL_AGENTIC_LANGUAGE.md) for that analysis).
 
 > **Scope.** Everything below is implemented and test-covered in `prototype/`
-> (**1,094 tests** green) and scored in the sibling `agentic-eval` crate (80
+> (**1,107 tests** green) and scored in the sibling `agentic-eval` crate (80
 > tests, in the AetherShell repository and not verifiable from here). The one
 > deliberate non-feature is agent/swarm *execution* — see
 > [Honest boundaries](#honest-boundaries).
@@ -175,7 +175,7 @@ are **five independent Cargo workspaces**:
 | Path | Crate | Tests | Notes |
 |---|---|--:|---|
 | `RecursiveMachineIntelligence/` | `rmi` | 1,380 | The low-level neurosymbolic framework. Feature-gated (`cpu` / `gpu` / `cuda`); build with `--no-default-features --features cpu` for the portable set |
-| `prototype/` | `mage-prototype` | 1,094 | Compiler, evaluator, ABL, RAP server. Path-depends on `rmi` |
+| `prototype/` | `mage-prototype` | 1,107 | Compiler, evaluator, ABL, RAP server. Path-depends on `rmi` |
 | `ribosome/` | `ribosome` | 164 | The distributed build engine. Depends on nothing in this repository — see below |
 | `germline/` | `germline` | 112 | Model succession, handoff, fallback — the RSI control plane. Path-depends on `ribosome` |
 | `forge/` | `forge` | 52 | The package registry, and only that |

HANDOFF.md

@@ -15,7 +15,7 @@ run, and are pinned to their output. See "The example rewrite" below.
 
 | | |
 |---|---|
-| Tests | **2,802** — rmi 1,380 · prototype 1,094 · ribosome 164 · germline 112 · forge 52 |
+| Tests | **2,815** — rmi 1,380 · prototype 1,107 · ribosome 164 · germline 112 · forge 52 |
 | CUDA | **1,071 passing** on dual RTX 3090 Ti, driver 610.88 |
 | Warnings | 0 compiler, 0 clippy in the four owned crates (`rmi` keeps 2 — vendored) |
 | Vulnerabilities | 0 Rust across five lockfiles, 0 npm |
@@ -109,7 +109,7 @@ Six of the eleven — #5, #6, #7, #8, #9, #11 — are the same class: a bug that
 **typechecks and then does not evaluate**. `--check` cannot find these. Only
 `--eval` can, which is why the pin now runs it.
 
-Prototype tests **1,066 → 1,094**, all green.
+Prototype tests **1,066 → 1,107**, all green.
 
 ### And a twelfth, from this list itself
 
@@ -125,6 +125,40 @@ Surveyed first rather than assumed: every `guard` in the repository — two
 examples, four `prototype/examples/*.mg`, two parser tests — already returns
 explicitly, so nothing had come to depend on the fall-through.
 
+### And the effect system got its elimination rule
+
+`handle { … } with E { … }`. The gap this closes was the one left in the
+"found and left alone" list: effects could be declared, annotated, inferred,
+and enforced, but never *discharged*, so `/ audit` propagated outward forever.
+
+Three things landed together, because none of them is useful alone:
+
+- **Introduction.** `Audit.record(x)` performs the operation and puts `audit`
+  in the calling function's effect set. Before this an `effect` block declared
+  operations that no analysis attributed to anyone and that the evaluator
+  rejected with `unknown function` — a thirteenth bug of the familiar
+  typechecks-then-does-not-evaluate kind.
+- **Elimination.** `handle` removes the effect from the block it wraps, so a
+  function can be pure despite calling something effectful. The subtraction is
+  **per block, not per function**: an unhandled call sitting beside a handled
+  one still reports. Whatever the arm itself does is attributed honestly, so
+  handling `audit` by writing a file makes the handling function `/ fs`.
+- **Declaration.** An operation the effect does not declare is an error, and
+  so is an effect annotation naming nothing.
+  `/ nte` used to be accepted as a *different effect* from `/ net`, enforced
+  consistently and matching nothing — a typo invented an effect instead of
+  failing. The operation check was added after the first version of this
+  feature shipped it broken: the analysis attributes the effect from the
+  *receiver* alone, so `Audit.recrod(x)` counted as performing `audit`,
+  checked clean, and died at run time. Building the fix for a bug class is no
+  protection against writing another instance of it one level down.
+
+Handlers do not resume. An operation call dispatches to its arm and returns
+like an ordinary call, which is what a tree-walking evaluator can do without
+capturing continuations. Handlers are found **dynamically** (innermost wins)
+and evaluated **lexically** (the arm sees the scope the handler was written
+in), and both are tested.
+
 ### The examples are now pinned to their output, not to their exit status
 
 `check-examples.sh` used to record which examples typechecked. That bar was too
@@ -142,9 +176,6 @@ the answer. `--print` regenerates the block after an intentional change.
 
 ### Found and left alone
 
-- **There is no `handle` form.** `--check` reports `unresolved name: handle`.
-  Effects can be declared, annotated, inferred, and enforced, but never
-  *discharged* — the effect system has no elimination rule.
 - **`agent` and `unsafe` cannot be written as effect names**, because both lex
   as keywords: `/ agent` is a parse error. `rand` is not built in either — the
   built-in kind is `rng`, and anything else silently becomes `Effect::Custom`.

MEASUREMENTS.md

@@ -6,8 +6,8 @@ numbers are machine-dependent; the shapes (throughput, scaling) are not.
 
 Date: 2026-06-10. Build: `release` for perf, `cargo test` for functionality.
 
-> **Re-verified 2026-08-11** — all five crates tested: prototype **1,094**, rmi
-> **1,380**, ribosome **164**, germline **112**, forge **52** = **2,802 passing,
+> **Re-verified 2026-08-11** — all five crates tested: prototype **1,107**, rmi
+> **1,380**, ribosome **164**, germline **112**, forge **52** = **2,815 passing,
 > 0 failing, 0 warnings**. No figure below has regressed.
 >
 > *A measurement that was wrong.* `BuildReport::cache_hit_ratio` was
@@ -65,7 +65,7 @@ Date: 2026-06-10. Build: `release` for perf, `cargo test` for functionality.
 ### Test suites (all green)
 | Suite | Tests | Cmd |
 |---|---|---|
-| MAGE prototype | **1094 pass** (+2 ignored perf harnesses) | `cargo test` |
+| MAGE prototype | **1107 pass** (+2 ignored perf harnesses) | `cargo test` |
 | rmi (`cpu`) | **1380 pass** | `cargo test --no-default-features --features cpu` |
 | ribosome (build engine) | **164 pass** | `cargo test --manifest-path ribosome/Cargo.toml` |
 | germline (RSI control plane) | **112 pass** | `cargo test --manifest-path germline/Cargo.toml` |

ROADMAP.md

@@ -4,8 +4,8 @@
 > Each step is a concrete, testable increment.
 >
 > **Last verified: 2026-08-11** — all five crates built and tested: prototype
-> **1,094**, rmi **1,380**, ribosome **164**, germline **112**, forge **52** —
-> **2,802 tests, 0 failures, 0 warnings**. The crate count went from three to
+> **1,107**, rmi **1,380**, ribosome **164**, germline **112**, forge **52** —
+> **2,815 tests, 0 failures, 0 warnings**. The crate count went from three to
 > five when the build engine (step 148) and the RSI control plane (step 149)
 > were extracted from `forge`; the total is unchanged by those moves, and
 > `forge`'s 52 is what the registry alone measured before they were parked in

examples/effects-showcase/src/main.mg

@@ -8,8 +8,8 @@
 //   - where that is *enforced*: private functions infer their effects, public
 //     ones must declare them. The check is at the module boundary.
 //   - composition, both `/ io, net` and `/ io + net` (the parser takes either)
-//   - a custom effect: any name that is not built in becomes one
-//   - `effect` declarations
+//   - a custom effect, declared by an `effect` block
+//   - performing an operation, and `handle … with` to *discharge* the effect
 //   - `guard` for early exit, and `defer`
 //
 // The rule the checker enforces is *under*-declaration: a published function
@@ -18,20 +18,35 @@
 // description. Every claim in this file was checked by running
 // `mage-parse --check` on an edited copy, not by reading the compiler.
 //
-// Not shown, because it does not exist yet: effect *handlers*. There is no
-// `handle` form — `mage-parse --check` reports `unresolved name: handle`. An
-// effect can be declared, annotated, inferred, and enforced, but not discharged.
+// The elimination rule is `handle { … } with E { … }`: it removes an effect
+// from the block it wraps, so a function can be *pure* despite calling
+// something effectful. Handlers do not resume — an operation call dispatches to
+// its arm and returns like an ordinary call.
 //
 // Run:  forge run        (or:  mage-parse --eval src/main.mg main)
 
 // ── Declaring an effect ──────────────────────────────────────────────
 
 // An `effect` block names an effect and the operations that belong to it. The
 // trailing semicolon on each signature is required.
+//
+// A declaration is not optional: an effect annotation naming nothing is an
+// error. It used to be accepted, which meant `/ nte` was not a misspelling of
+// `/ net` but a silently different effect that matched nothing.
+//
+// The declaration is `Audit`, the annotation is `/ audit`. The two spellings
+// are matched case-insensitively.
 effect Audit {
-    fn record(entry: String);
+    fn record(entry: String) -> usize;
 }
 
+// `db` is a custom effect too — it is not one of the built-in kinds (`io`,
+// `net`, `fs`, `async`, `alloc`, `panic`, `ffi`, `env`, `time`, `gpu`, `npu`,
+// `llm`, `evolve`, `learn`, `rng` — see `Effect::from_name` in `hir.rs`). It
+// carries no operations, which is allowed: a bare `effect` block is how you
+// name an effect you only want to track, not perform through.
+effect Db {}
+
 // ── Pure core ────────────────────────────────────────────────────────
 
 // No annotation means no effects, and the checker holds this to it: calling
@@ -77,10 +92,8 @@ fn jitter() -> i32 / rng {
     17
 }
 
-// `db` is not one of the built-in effect kinds (`io`, `net`, `fs`, `async`,
-// `alloc`, `panic`, `ffi`, `env`, `time`, `gpu`, `npu`, `llm`, `evolve`,
-// `learn`, `rng` — see `Effect::from_name` in `hir.rs`). Any other name becomes
-// a custom effect and is tracked the same way, so the system is open, not fixed.
+// Custom effects propagate and are enforced exactly like built-in ones, so the
+// system is open rather than fixed.
 fn persist(record: String) -> usize / db {
     len(chars(record))
 }
@@ -128,6 +141,33 @@ fn audit(entry: String) -> String / db {
     f"audited {len(chars(entry))} chars"
 }
 
+// ── Performing an effect, and discharging it ─────────────────────────
+
+// `Audit.record(...)` *performs* the operation. That is what puts `audit` in
+// this function's effect set — the annotation is checked against it, not the
+// source of it.
+fn transcribe(entry: String) -> usize / audit {
+    Audit.record(entry)
+}
+
+// And here it is discharged. `handle { … } with Audit { … }` removes `audit`
+// from the block, so this function is **pure** even though `transcribe` is not:
+// `--check` reports `f summarize_audit: pure`.
+//
+// The subtraction is per-block, not per-function. A second, unhandled call to
+// `transcribe` outside this `handle` would still be reported — handling one
+// call does not launder the rest.
+//
+// Whatever the arm itself does is honestly attributed: make `record` call
+// `persist` and this function becomes `/ db`, because that is what it now
+// performs. A handler exchanges one effect for the effects of handling it.
+fn summarize_audit(entry: String) -> String {
+    val n = handle { transcribe(entry) } with Audit {
+        record(e) => len(chars(e))
+    }
+    f"recorded {n} chars"
+}
+
 // ── Entry point ──────────────────────────────────────────────────────
 
 // The union of everything reachable: `fs` and `net` from `check_host`, `time`
@@ -140,6 +180,7 @@ pub fn main() -> String / fs, net, time, rng, db {
     val health = check_host("up.example", "app.toml")
     val stamped = stamp("up.example")
     val logged = audit(health)
+    val transcribed = summarize_audit(health)
 
     val codes = [200, 404, 503]
     val report = map(codes, fn(code) => severity(code))
@@ -150,6 +191,7 @@ pub fn main() -> String / fs, net, time, rng, db {
             health,
             stamped,
             logged,
+            transcribed,
             join(report, "/"),
             summarize(codes),
         ],

prototype/src/ast.rs

@@ -284,6 +284,25 @@ pub enum Expr {
         scrutinee: Option<Box<Expr>>,
         arms: Vec<MatchArm>,
     },
+    /// `handle { body } with Audit { record(e) => … }` — the effect system's
+    /// elimination rule.
+    ///
+    /// Effects could be declared, annotated, inferred, and enforced, but never
+    /// *discharged*: there was no way to satisfy `/ audit` other than to keep
+    /// propagating it outward forever. This is what removes it. The handled
+    /// effect leaves the body's effect set; whatever the arms themselves do
+    /// takes its place, so handling `audit` by writing to a file is honestly
+    /// reported as `/ fs`.
+    ///
+    /// Handlers do not resume. An operation call dispatches to the matching arm
+    /// and returns its value like an ordinary call, which is what a
+    /// tree-walking evaluator can implement without capturing continuations.
+    Handle {
+        body: Block,
+        /// The declared `effect` block being discharged.
+        effect: String,
+        arms: Vec<HandlerArm>,
+    },
     Loop {
         body: Block,
     },
@@ -366,6 +385,18 @@ pub struct MatchArm {
     pub body: Expr,
 }
 
+/// One operation of a handled effect: `record(entry) => persist(entry)`.
+///
+/// The parameters are bare names rather than patterns. Their types come from
+/// the `effect` block's declaration of the operation, so writing them again
+/// here would be a second place for them to disagree.
+#[derive(Debug, Clone, Serialize, Deserialize)]
+pub struct HandlerArm {
+    pub op: String,
+    pub params: Vec<String>,
+    pub body: Expr,
+}
+
 #[derive(Debug, Clone, Serialize, Deserialize)]
 #[serde(tag = "type")]
 pub enum Pattern {