test: SKA op2 gap tests + doc updates (411/411)

AGENTS.md

@@ -217,11 +217,10 @@ CI: QEMU 9.2.0 from source (raspi4b).
 
 ## Immediate Tasks for This Agent
 
-Phase 9 is complete (all 376 tests passing). The PoC gate (Phases 0–9) is cleared.
+Phase 9 is complete (all 411 tests passing). The PoC gate (Phases 0–9) is cleared.
 The Forth dictionary IS the jet dashboard — thesis demonstrated.
 
 Next priorities:
-- **Test hardening**: remaining crash recovery sites, gate jet direct tests, control flow
 - **Phase 10**: North integration (pending external dependency)
 - **Phase 11**: SKA Phase 2 / full Hoon subset
 - **Phase 12**: Large atom cold store (SD card backing)
@@ -526,11 +525,11 @@ core = run_nomm1(subject, c_nomm1, ...)  // %ds2 already resolved to jet_fn_t
 | 5c | PILL loader (QEMU file loader at 0x10000000) | DONE |
 | 5d | Noun tag redesign (direct atom = raw integer) | DONE |
 | 7 | Kernel loop: Arvo + Shrine shapes, UART framing, effect dispatch | DONE |
-| CI | QEMU raspi4b + 376 tests (REPL + Nock reference + crash recovery + SKA coverage) | DONE |
+| CI | QEMU raspi4b + 411 tests (REPL + Nock reference + crash recovery + SKA coverage inc. op2 all sub-cases) | DONE |
 | 8 | SKA: symbolic partial eval, `$nomm` AST, compile-time jet matching | DONE |
 | 9 | Forth as jet dashboard: evaluator dispatch in dictionary | DONE |
 
-PoC gate: Phases 0–9 all DONE. **376 tests passing.** Next: Phases 10+ (pending external deps).
+PoC gate: Phases 0–9 all DONE. **411 tests passing.** Next: Phases 10+ (pending external deps).
 
 ## Key Source References in the Codebase
 

ROADMAP.md

@@ -404,12 +404,12 @@ initial sock. After SKA, op-9 dispatch skips `sock_match` entirely at
 |-------|---------|---------|
 | **7a** Types           | `src/ska.h`  | ✅ `cape_t`, `sock_t`, `nomm_t`, `nomm1_t`, `bell_t`, `site_t`, `short_t`, `long_t`, `cycle_t` |
 | **7b** Sock ops        | `src/ska.c`  | ✅ `cape_and/or`, `cape_app`, `sock_pull`, `sock_huge`, `sock_knit`, `sock_purr`, `sock_pack`, `sock_darn`, `dunno` |
-| **7c** Scan (linear)   | `src/ska.c`  | ✅ All opcodes inc. Op2 partial eval; `%9` → `NOMM_DS2` or `NOMM_9` fallback; `SKNOCK` Forth word |
-| **7d** Memo cache      | `src/ska.c`  | ✅ Cross-arm cache keyed by `(formula, sub-sock)`; per-pass reset |
+| **7c** Scan (linear)   | `src/ska.c`  | ✅ All opcodes inc. Op2 partial eval (NOMM_I2, NOMM_7 inline, NOMM_DS2 memo/fresh-scan); `SKNOCK` Forth word |
+| **7d** Memo cache      | `src/ska.c`  | ✅ Cross-arm cache keyed by `(formula, sub-sock)`; per-pass reset; shared between op2 and op9 sites |
 | **7e** Loop detection  | `src/ska.c`  | ✅ `close()` heuristic, fols_stack, frond validation, redo-loop |
 | **7f** Cook pass       | `src/ska.c`  | ✅ `nomm → nomm-1`; `cook_nomm()`, `run_nomm1()`; static jet pre-wiring at DS2 sites |
 | **7g** Integration     | `src/forth.s` | ✅ `SKA-EN` variable, `NOCK` routes through SKA when set, `.SKA` stats word |
-| **7h** Tests           | `tests/run_tests.sh` | ✅ SKA-EN, .SKA no-crash, 182 tests total |
+| **7h** Tests           | `tests/run_tests.sh` | ✅ SKA-EN, .SKA, op2 all 4 sub-cases (I2/inline/memo/DS2), 411 tests total |
 
 Stage 9c alone gives partial benefit (non-looping direct calls annotated).
 Stage 9e is required for all tail-recursive Hoon gates (`dec`, `add`, etc.).
@@ -535,8 +535,8 @@ the word will be present and cook pre-wires the jet at O(1).
 | **9f** `%tame` handler | `src/nock.c`                  | ✅ Parse `[label forth-source]` clue, idempotency guard, call `forth_eval_string` |
 | **9g** Cache + bench   | `src/ska.c` / `src/forth.s`   | ✅ `TIMER@` (`mrs CNTVCT_EL0`); SKA formula cache (nomm1_t* keyed by formula noun); `BENCH` word; `EXECUTE` word |
 
-**All stages complete.** 376 tests passing (63 Nock reference vectors, 20 crash recovery,
-20 Forth primitives, 10 indirect atom hardening, 48 SKA coverage tests, plus existing
+**All stages complete.** 411 tests passing (63 Nock reference vectors, 20 crash recovery,
+20 Forth primitives, 10 indirect atom hardening, 52 SKA coverage tests inc. op2 all 4 sub-cases, plus existing
 regression suite).
 
 #### Key Design Decisions

tests/run_tests.sh

@@ -844,6 +844,43 @@ T "ska op2: op2 resolves to inc(0)"  "0000000000000001" \
 T "ska op2: nested known formula"  "000000000000000B" \
     "10 N>N  2 N>N  1 N>N 10 N>N CONS  1 N>N  4 N>N 0 N>N 1 N>N CONS CONS  CONS CONS CONS  SKNOCK NOUN> ."
 
+# ── Op2 partial eval gap tests ─────────────────────────────────────────────
+# These four tests exercise the four sub-cases of the op2 scan:
+#   (a) NOMM_I2  — formula c not statically known (dynamic slot)
+#   (b) Memo hit — same resolved formula seen twice in one scan
+#   (c) DS2 with non-constant subject formula (nock_ex fallback, no jet)
+#   (d) DS2 with resolved formula containing op7 (deep fresh-scan)
+
+# (a) NOMM_I2 via SKNOCK — c=[0 3] is a dynamic slot; cape is wildcard,
+#     so run_nomm1 takes the q!=NULL branch and calls nock_ex at runtime.
+# *[[42 [4 [0 1]]] [2 [0 2] [0 3]]] = *[42 [4 [0 1]]] = 43
+T "ska op2: I2 fallback via SKNOCK"  "000000000000002B" \
+    "42 N>N  4 N>N 0 N>N 1 N>N CONS CONS  CONS  2 N>N  0 N>N 2 N>N CONS  0 N>N 3 N>N CONS  CONS CONS  SKNOCK NOUN> ."
+
+# (b) Memo hit — distribution formula [f.f] where f=[2 [0 1] [1 [4 [0 1]]]].
+#     SKA scans the head op2 first (fresh scan → populates g_memo with [4 [0 1]]),
+#     then scans the identical tail op2 (memo hit: same fol, compatible sub-sock).
+# *[5 [[f][f]]] = [*[5 f] *[5 f]] = [6 6]; CAR = 6
+T "ska op2: memo hit via distribution"  "0000000000000006" \
+    "5 N>N  2 N>N  0 N>N 1 N>N CONS  1 N>N  4 N>N 0 N>N 1 N>N CONS CONS  CONS  CONS CONS  DUP CONS  SKNOCK CAR NOUN> ."
+
+# (c) DS2 with non-constant subject formula — p=[4 [0 1]] (inc) produces a
+#     wildcard sock, so cook_find_jet returns NULL and run_nomm1 falls through
+#     to nock_ex(core, bell.fol, ...) to evaluate the resolved formula.
+# *[5 [2 [4 [0 1]] [1 [4 [0 1]]]]] = *[inc(5) [4 [0 1]]] = *[6 [4 [0 1]]] = 7
+T "ska op2: DS2 inc subject formula"  "0000000000000007" \
+    "5 N>N  2 N>N  4 N>N 0 N>N 1 N>N CONS CONS  1 N>N  4 N>N 0 N>N 1 N>N CONS CONS  CONS CONS CONS  SKNOCK NOUN> ."
+
+# (d) DS2 with resolved formula [7 [4 [0 1]] [4 [0 1]]] (double-inc via op7).
+#     Fresh scan recurses into op7, exercising the full scan path for a complex
+#     resolved formula that is itself not a trivial [0 ax] or [1 val].
+# *[3 [2 [0 1] [1 [7 [4 [0 1]] [4 [0 1]]]]]]
+#   = *[3 [7 [4 [0 1]] [4 [0 1]]]]
+#   = *[*[3 [4 [0 1]]] [4 [0 1]]]
+#   = *[4 [4 [0 1]]] = 5
+T "ska op2: DS2 resolved to op7 (double-inc)"  "0000000000000005" \
+    "3 N>N  2 N>N  0 N>N 1 N>N CONS  1 N>N  7 N>N  4 N>N 0 N>N 1 N>N CONS CONS  4 N>N 0 N>N 1 N>N CONS CONS  CONS  CONS  CONS CONS CONS  SKNOCK NOUN> ."
+
 # Op2 via SKA-EN (NOCK routes through ska_nock)
 # *[42 [2 [0 1] [1 [4 [0 1]]]]] = *[42 [4 [0 1]]] = 43
 T "ska-en op2: known formula via NOCK"  "000000000000002B" \