uw-resolve P2: store-backed resolution (D43 indexed catalog)

docs/WAM_BACKEND_CONVENTIONS.md

@@ -22,7 +22,11 @@ are deliberately chosen to exercise every convention below.
 
 ---
 
-## TL;DR — the six things that bite
+## TL;DR — the eight things that bite
+
+*(§1–§6 were found by the conformance fixtures; §7–§8 were found by
+running a whole real program — the A2 exercise — and the fixtures do
+not catch them.)*
 
 | # | Convention | Symptom if you get it wrong | Conformance program that catches it |
 |---|---|---|---|
@@ -32,6 +36,8 @@ are deliberately chosen to exercise every convention below.
 | 4 | **`deref` before every type test** (`is_var`, `is_list`, …) | a *bound* variable is mistaken for unbound → write-mode corruption | `member`, `reverse` |
 | 5 | `is/2` must produce an **integer** for integral results (if unify is type-strict) | `R is N+1` fails when `R` is a ground integer | `fib`, `ack` |
 | 6 | **Never drop or throw on an unhandled instruction** — emit a real no-op so PC/label alignment is preserved | indexing hints (`switch_on_term*`, `switch_on_constant_fallthrough`) vanish from the code vector, shifting every later label by one; backtracking skips `retry_me_else`/`trust_me` and loops or mis-clauses | `fib`, `ack`, `append`, `reverse` |
+| 7 | **`Execute` of a runtime-implemented builtin must run it and then take `Proceed`'s return path** — never halt, never silently fail, never jump to PC 0 | a clause whose *last* goal is a builtin outside `is_builtin_pred/2` (`sub_string/5`, `catch/3`, any runtime-extended builtin) binds its outputs and then kills or fails the whole call | none yet — found by the whole-program benchmark (`examples/cli_args/`), not the fixture suite |
+| 8 | **Do not assume `Allocate` framing protects Y registers** — with the numeric `X→+100 / Y→+200` encoding, X101 aliases Y1, and the shared fact compiler emits >99 X placeholders with **no** `Allocate` | calling a large ground-fact predicate silently corrupts the caller's permanent variables | none yet — same benchmark (a ~7-entry nested registry fact triggers it) |
 
 ---
 
@@ -228,6 +234,88 @@ fallback) through it.
 
 ---
 
+## 7. `Execute` of a builtin must return to the continuation
+
+*Adopted 2026-09 from the JS-runtime findings of the whole-program
+(A2) exercise — see [`WAM_FLEET_GAPS.md`](WAM_FLEET_GAPS.md). Unlike
+§1–§6, the conformance fixtures do **not** catch violations; the
+`examples/cli_args/` benchmark does.*
+
+The compiler emits a clause's last goal as `deallocate` + `execute
+P/N` (TCO). When `P/N` is in `is_builtin_pred/2` it becomes
+`builtin_call` + `proceed` instead — but many predicates a runtime
+implements are **not** in that shared table (`sub_string/5`,
+`catch/3`, `call/N`, every runtime-extended builtin), so they reach
+the backend as `execute` of a name **with no label**.
+
+**Rule:** the `Execute` arm, after failing label lookup, must try the
+runtime's own builtin/foreign dispatch, and on success perform exactly
+what `Proceed` would: restore the caller and jump to CP (halting only
+when CP is the top-level sentinel). Three observed failure modes, all
+wrong:
+
+- **halt** — the JS runtime set `halt = true` after the builtin
+  succeeded, dropping the rest of the caller (`substring_from/3`
+  ending in `Execute sub_string/5` left `parse_args/3`'s result
+  unbound); fixed by routing through the shared `proceed_to_cp`.
+- **silent failure** — most runtimes (Lua, Python, C, Clojure, and the
+  general case in Rust/Haskell/F#/Elixir) fail the goal when the label
+  is missing, so a *succeeding* builtin reports failure.
+- **PC 0** — WAT's `resolve_label` encodes an unknown label as PC 0: a
+  silent jump to instruction 0.
+
+**Precedents:** Go's dedicated `BuiltinExecute` instruction
+(`instructions.go.mustache` — run the builtin, then Proceed's return
+step; kept as one instruction so PC/label alignment survives, per §6);
+C++'s `Execute` fallback-then-proceed (`wam_cpp_target.pl:8035-8040`);
+R's `call_library` + Proceed protocol (`runtime.R.mustache:1424-1467`);
+JS post-A2 (`proceed_to_cp`). A builtin the runtime genuinely does not
+implement should still **fail loudly enough to find** (a diagnostic on
+stderr costs nothing); it must never be encoded as a jump.
+
+---
+
+## 8. Y registers are not protected by `Allocate` framing — the X window aliases into Y space
+
+*Adopted 2026-09 from the same exercise. This is a property of the
+**shared bytecode**, so every backend must pick a defence.*
+
+The shared fact compiler emits a large ground fact (e.g. a 7-entry
+nested registry, `default_registry/1` in `examples/cli_args/`) as a
+plain `get_*`/`unify_*` sequence with **no `Allocate`** and with more
+than 99 X-register placeholders. Under the common numeric register
+encoding — `A_n→n, X_n→n+100, Y_n→n+200` (or 0-based / 128-slot
+variants) — **X101 and Y1 are the same slot**. Calling such a fact
+therefore overwrites the caller's permanent (Y) registers, and the
+callee's missing `Allocate` means no frame discipline ever saves them.
+Frame-based runtimes are *not* exempt: a runtime that routes "id ≥
+200" to the topmost environment frame (Haskell, Python at ≥ 301, R,
+F#) writes the fact's spilled X registers into the **caller's** frame.
+
+**Rule — one of, in order of preference:**
+
+1. **Non-aliasing register spaces.** String-named registers or
+   segregated banks (`"X101"` ≠ `"Y1"`): Rust, Kotlin, C++, Clojure, C
+   are structurally immune. If the bank is a fixed-size array (C's
+   `WAM_MAX_REGS 256`), bounds-check it — an oversized fact must fail
+   loudly, not corrupt memory.
+2. **Save/restore the Y range across `Call`.** The JS workaround:
+   `Call`/`CallPc` snapshot registers ≥ Y-base, `Proceed` restores
+   (`push_y_save` / `proceed_to_cp` in `runtime.js.mustache`); the
+   snapshot must also be captured into choice points.
+3. *(Upstream, preferred long-term)*: make `wam_target.pl`'s fact
+   compilation stay inside the X window (spill to a dedicated range),
+   at which point this section demotes to a historical note. Until
+   then, assume any fact with >99 placeholders is hostile to your Y
+   registers.
+
+**Test:** call a ground fact whose single argument needs ≥ 120
+placeholder registers from a clause that holds live Y registers across
+the call, and check the Y values afterwards. `probe_y_preserve/0` in
+`tests/test_wam_javascript_builtins.pl` is the model.
+
+---
+
 ## New-backend checklist
 
 Before declaring a WAM backend conformant, confirm each of these against a
@@ -250,8 +338,77 @@ expression (the conformance fixtures do both):
       `append`). (§6)
 - [ ] operator functors are escaped for the host string syntax (`=\=` must
       survive as `=\\=` in a C/Java/… literal). (§2)
-- [ ] `CONFORMANCE_TARGETS=<target>` is green with no `ct_xfail` entries.
+- [ ] `execute` of an unlabelled name falls back to the runtime's builtin
+      dispatch and then takes `Proceed`'s return path — test a clause whose
+      *last* goal is a builtin outside `is_builtin_pred/2`. (§7)
+- [ ] Y registers survive a call to a no-`Allocate` ground fact with ≥ 120
+      placeholder registers (non-aliasing register spaces, or a Y snapshot
+      on `Call`). (§8)
+- [ ] `CONFORMANCE_TARGETS=<target>` is green with no `ct_xfail` entries —
+      and remember the fixtures do **not** cover §7/§8; the
+      `examples/cli_args/` whole-program benchmark does
+      ([`WAM_FLEET_GAPS.md`](WAM_FLEET_GAPS.md), Class C).
 
 The first backend that hits a *new* class of divergence should add a row
 to the table in `WAM_CROSS_TARGET_CONFORMANCE.md` and, if it is a general
 convention rather than a one-off, a section here.
+
+### §9 — Cut is a barrier, never a stack wipe
+
+*(Adopted 2026-09 from the JS-backend cut-semantics audit: twelve divergences,
+every one invisible to the 48-query conformance set.)*
+
+A cut prunes choice points back to a **barrier**, never to zero. Every backend
+must maintain an explicit barrier and every runtime that can nest one execution
+inside another must maintain two:
+
+1. **`cut_barrier` (WAM `B0`)** — the choice-point-stack height recorded when
+   the current predicate activation was entered. `!` truncates back to it and
+   no further.
+2. **`cp_barrier` (isolation floor)** — the height at which a nested run driven
+   from host code begins. Neither backtracking nor cutting may cross it.
+
+The effective floor for any cut is `max(cut_barrier, cp_barrier)`. Implementing
+`!` as "clear the choice-point stack" is a defect even when the test suite
+passes: it only shows up once a nondeterministic caller sits below a cutting
+callee.
+
+**Both `call` and `execute` set `B0 <- B`.** Last-call optimization reuses the
+caller's frame slot, so `execute` must *replace* the barrier rather than push a
+new one — but it must still replace it. A backend that rebases on `call` only
+will let a `!` in a tail-called predicate destroy its caller's clause
+alternatives.
+
+**Every choice point must snapshot and restore the barrier state**
+(`cut_barrier` and the saved-`B0` stack) alongside the trail mark and
+registers. A hand-written choice-point record that omits them silently deletes
+the barrier regime on backtrack. Backends should funnel all choice-point
+creation through a single snapshot routine rather than open-coding the record.
+
+**Barrier-raising contexts.** The condition of `( C -> T ; E )`, the argument
+of `\+`, the goal of `call/1`, and the inner goal of
+`findall`/`bagof`/`setof`/`aggregate_all` are each opaque cut scopes: a `!`
+inside one may prune only that scope's own choice points. In particular,
+entering the *then* branch of an if-then-else must cut the condition's choice
+points, and an inlined aggregate must raise the barrier above its own aggregate
+choice point so an inner `!` cannot strand the collection. The *then* and
+*else* branches are **not** opaque — a `!` there cuts the enclosing clause
+(ISO).
+
+**Lowered tiers are first-solution.** A lowered host function that returns
+through the host stack cannot resume a callee's choice point. A backend with a
+lowered tier must therefore *decline to lower* any predicate that (a) reaches a
+choice-point-creating builtin outside a commit wrapper, (b) calls a user
+predicate that can succeed more than once outside a commit wrapper, (c) can
+itself succeed more than once, or (d) contains a commit-less disjunction. The
+set in (a) is the set of builtins that actually push on that backend's
+choice-point stack — it is backend-specific and must be derived from the
+runtime, not copied. Where a lowered call cannot avoid leaving a choice point
+behind, the leftover must be **dropped**, not left to be resumed incoherently:
+honestly first-solution beats silently wrong.
+
+**Conformance.** A backend claiming §9 must ship a cut-semantics probe corpus
+run against a reference Prolog, covering each context above in *both* the
+interpreted and lowered tiers and at the boundary between them.
+Forty-eight-query conformance suites do not exercise this: the JS backend
+passed all of them while `!` was wiping the entire choice-point stack.