OCapN port + the compiler work it forced: interop to 24/24, plus ~185 core commits

.claude/rules/on-network.md

@@ -40,6 +40,46 @@ When encountering off-network state, ask:
 
 Every cell value must be a lattice element with a monotone merge. If you can't define a merge function, the value doesn't belong on the network yet — but that's a design signal, not a permanent excuse. Find the lattice.
 
+### ⚠ CHECK idempotence — do not document it (promoted 2026-08-05, 3 instances)
+
+> Read the *two kinds* subsection below with this one: idempotence is required of a JOIN cell, and four registered merges are deliberately not joins.
+
+`merge(x, x)` must equal `x`. This obligation was written in three ambient rule files and **enforced in none**, and the gap cost fourteen months.
+
+**The failure shape**: a merge that unions two collections with a bare `append`. `(merge x x)` returns twice x's elements, so the cell's lattice VALUE is stable while its REPRESENTATION grows on every write. Change-detection sees a change every round, dependents re-fire, and the network **never quiesces** — a HANG, not a wrong answer. Read cost grows with the representation too, so it accelerates.
+
+**Why it hides**: the merge's own comment usually asserts the property it violates. All three in-tree instances did — *"functionally equivalent to set-union for unique nogoods"*, *"the lattice is P(P(AssumptionId)) under set-union"*. The parenthetical does the work and nothing checks it.
+
+| instance | found by | consequence |
+|---|---|---|
+| `tagged-cell-merge` / `make-tagged-merge` | a 14-month hunt, at the wrong layer | union-type type-checker hang; also took the LSP down |
+| `nogood-merge` | `tests/test-merge-laws.rkt`, **first run** | live cell merge (`atms.rkt`), same latent hazard |
+| `merge-hasheq-list-append` | same run | its 3 cells turned out write-only; retired instead |
+
+**Do this**: add every new cell merge to the `MERGES` table in `tests/test-merge-laws.rkt` (24 covered of 29 registered). One `(E "name" fn samples)` row. Idempotence is checked unconditionally; `#:laws '(commutative associative)` is opt-IN, because several merges here are deliberately last-write-wins (`merge-hasheq-replace`). Pass an `equiv` when the carrier's representation is looser than its lattice value — a set carried as a list has an order set-union never claimed. A merge that is knowingly NOT a join (`merge-list-dedup-append`) is registered anyway and pinned as a known non-lattice, so the distinction stays visible instead of being omitted.
+
+**Debug rule**: a propagator network that will not quiesce is a merge that is not idempotent **until proven otherwise**. Check the carrier before the join. The union-type hang was filed as *"the `:type`-facet union join not reaching a fixpoint"* and the join was innocent — that framing sent it at the type-lattice/quantale work for over a year, and the fix was 8 lines in the cell.
+
+### The rule above is TOO STRONG: cells come in two kinds (2026-08-05)
+
+"Every cell value must be a lattice element with a monotone merge" is the ideal, and **four registered cell merges are not joins — three of them correctly**. Enumerated by `tests/test-merge-laws.rkt`:
+
+| merge | `merge(x,x)` | why non-idempotence is RIGHT |
+|---|---|---|
+| `add-usage` (`qtt.rkt`) | `(m1)+(m1) = (mw)` | semiring ADDITION. Using a linear resource twice makes it unrestricted — **idempotence would break QTT** |
+| `merge-list-append` (`relations.rkt` answer cell) | `(append x x)` | Rel T1 POL.1: solution sets are BAGS, multiplicity IS the derivation count — idempotence would break `solve` |
+| `warnings-facet-merge` | `(append x x)` | two identical warnings from two sites are two warnings |
+| `merge-hasheq-list-append` | grows | no defence; its cells were write-only, now retired |
+
+So the operative distinction is:
+
+- **JOIN cells** — idempotent. CALM-safe, order-independent, any scheduler.
+- **ACCUMULATOR cells** — not idempotent. Their correctness depends on a property **nothing checks**: that their writers never re-fire with a value already merged. That is a *scheduling* assumption smuggled into a *cell*, and it is exactly what `tagged-cell-merge` got wrong for fourteen months — an accumulator that believed it was a join.
+
+**When you write a non-idempotent merge, you owe the reason at the merge** (which semiring, which owner ruling), **and you owe a check that its writers are write-once**. `merge-fn-registry.rkt` cannot help: a domain name records WHICH lattice, never WHETHER it is one.
+
+**Fuel will not save you**: fuel is a FIRE-COUNT budget, decremented per propagator fired. It cannot bound the cost of ONE fire, so a single fire merging an unbounded value runs forever with fuel to spare. (Its `on-write-check` was also unreachable under speculation until 2026-08-05 — the hot fast path is gated on `(not under-speculation?)` and the slow path never consulted it.)
+
 ## Topology Requests for Dynamic Registration
 
 When a propagator discovers it needs infrastructure that doesn't exist yet (e.g., a table cell for an unregistered relation), it emits a topology request. The topology stratum (between BSP rounds) processes the request, allocates cells, updates registries. This is the CALM-safe protocol for structural mutation.

.claude/rules/prologos-syntax.md

@@ -85,6 +85,38 @@ it) and `=` never binds.
   ```
   Body at the **same** indent as `|` is a layout violation (currently produces a hard parser error; tracked in issue #27 for diagnostic improvement). Body indent must be **strictly greater than** the `|` column.
 
+- **Never write three-deep nested `match` as a single function body.** Three-deep nested `match` inside a single function body fails to elaborate at *import time* with "Unbound variable" errors in Prologos's current elaborator. The fix is mechanical: factor into a chain of single-match helpers. Each helper does one `match`, returns to the caller, the caller does the next `match`. Same semantics for the user, no elaborator failure. OCapN Phases 15 and 21 both shipped this workaround; codified after the second occurrence. Until the underlying elaborator bug is fixed, this is the safe pattern.
+  ```
+  ;; WRONG — fails at import time
+  defn pipeline-deliver [target args v]
+    match [lookup-actor target v]
+      | some _ -> send-only target args v
+      | none ->
+          match [lookup-promise target v]
+            | none -> v
+            | some pst ->
+                match pst
+                  | pst-unresolved msgs -> ...
+                  | _ -> v
+
+  ;; RIGHT — helper chain
+  spec deliver-to-promise Nat SyrupValue PromiseState Vat -> Vat
+  defn deliver-to-promise [pid args pst v]
+    match pst | pst-unresolved msgs -> ... | _ -> v
+
+  spec deliver-to-promise-or-drop Nat SyrupValue Vat -> Vat
+  defn deliver-to-promise-or-drop [target args v]
+    match [lookup-promise target v]
+      | none -> v
+      | some pst -> deliver-to-promise target args pst v
+
+  spec pipeline-deliver Nat SyrupValue Vat -> Vat
+  defn pipeline-deliver [target args v]
+    match [lookup-actor target v]
+      | some _ -> send-only target args v
+      | none -> deliver-to-promise-or-drop target args v
+  ```
+
 ## Application style
 
 - **Uncurried** -- `defn foo [x y z] body`, `spec f A B -> C`. Multiple arguments in one bracket group.
@@ -93,6 +125,38 @@ it) and `=` never binds.
 - **Pipeline `|>` and `compose`** for chaining named functions -- `|> 5 inc dbl sqr` is idiomatic.
 - **Eval is implicit** -- write `[f x]` not `eval [f x]`. Top-level expressions just evaluate.
 - **Don't wrap outer tree** -- top-level forms are implicit.
+- **Keep multi-arg applications on a single line.** A continuation line whose first token is a bare identifier is parsed as a sibling form, not as more args to the previous head. Pitfalls #36 and #38 (goblin-pitfalls log) both stem from this:
+  ```
+  ;; WRONG — `es as qs p oqs ir er pm` is parsed as an application of `es` to 7 args
+  bridge-state [list-filter-listeners-by-notified ls notified]
+               es as qs p oqs ir er pm
+
+  ;; WRONG — `let X := EXPR` value can't span lines; reader sees no value for X
+  let step1 := [captp-incoming-with-state op1 [alloc-vat sa]
+                 [bridge-state-with-our-session ver loc]]
+
+  ;; RIGHT — all positional args on the function-head line; break BEFORE a bracketed sub-call (which becomes the last arg) if the line gets too long
+  bridge-state [list-filter-listeners-by-notified ls notified] es as qs p oqs ir er pm
+  ```
+  If a line is unavoidably long, factor a sub-expression to a separate `let` or top-level helper rather than splitting positional args.
+
+- **Single-arg `defn` over a `data` type uses `defn name [arg] match arg | ...`, NOT multi-arity `defn name | [pat1] -> ... | [pat2] -> ...`.** The latter shape can cause the elaborator to lift a phantom 2nd parameter (pitfall #37 in goblin-pitfalls). Multi-arity `defn` is fine for 2+ args; for one-arg over a data type, prefer `match`:
+  ```
+  ;; WRONG — inferred type becomes `PromiseState SyrupValue -> [Option SyrupValue]` (2 args)
+  spec resolution-syrup-of-pst PromiseState -> [Option SyrupValue]
+  defn resolution-syrup-of-pst
+    | [pst-unresolved _] -> none
+    | [pst-broken     r] -> some [wrap-error r]
+    | [pst-fulfilled  v] -> some v
+
+  ;; RIGHT — inferred type matches the spec
+  spec resolution-syrup-of-pst PromiseState -> [Option SyrupValue]
+  defn resolution-syrup-of-pst [pst]
+    match pst
+      | pst-unresolved _ -> none
+      | pst-broken     r -> some [wrap-error r]
+      | pst-fulfilled  v -> some v
+  ```
 
 ## Type annotations
 
@@ -131,6 +195,11 @@ it) and `=` never binds.
   error was discarded, so a file could report **0 errors while defining
   nothing**.
 
+## Data type definitions
+
+- **Constructor signatures have IMPLICIT return type** (per pitfall #34). Write `data X { ctor : T1 -> T2 }` to mean "ctor takes 2 args of types T1 and T2 and returns X." Do NOT write `ctor : T1 -> T2 -> X` — that means "takes 3 args (T1, T2, X) and returns X." Existing examples: `data Listener { listener : Nat -> Nat }`, `data QEntry { q-entry : Nat -> Nat }`. Symptom of getting it wrong: smart constructors fail with `Type mismatch [Pi T -> Result -> Result]`.
+
+
 ## Relational syntax (`defr` / `rel` / goals)
 
 Landed in Rel Track 1 (POL.7/.8/.9, 2026-07-25). All three are **additive** —