Specializer M-ir: imperative IR — grammar, types, verifier, text format

backlog/tasks/task-41 - Specializer-M-ir-imperative-IR-—-grammar-types-verifier-text-format.md

@@ -1,9 +1,10 @@
 ---
 id: TASK-41
 title: 'Specializer M-ir: imperative IR — grammar, types, verifier, text format'
-status: To Do
+status: In Progress
 assignee: []
 created_date: '2026-07-25 02:31'
+updated_date: '2026-07-25 13:46'
 labels: []
 milestone: m-7
 dependencies: []
@@ -21,8 +22,24 @@ Define the specializer's imperative IR per §6 of docs/superpowers/specs/2026-07
 
 ## Acceptance Criteria
 <!-- AC:BEGIN -->
-- [ ] #1 Verifier rejects: non-SSA defs, type mismatches, any arithmetic on a T? value not routed through the null-lane ops, unresolvable StaticRef ids, allocating constructs
-- [ ] #2 Text format round-trips: parse(print(ir)) == ir on every test program, including a property/fuzz round-trip test
-- [ ] #3 Hand-written IR programs covering every instruction exist as test fixtures
-- [ ] #4 mise gate-specializer green
+- [x] #1 Verifier rejects: non-SSA defs, type mismatches, any arithmetic on a T? value not routed through the null-lane ops, unresolvable StaticRef ids, allocating constructs
+- [x] #2 Text format round-trips: parse(print(ir)) == ir on every test program, including a property/fuzz round-trip test
+- [x] #3 Hand-written IR programs covering every instruction exist as test fixtures
+- [x] #4 mise gate-specializer green
 <!-- AC:END -->
+
+## Implementation Plan
+
+<!-- SECTION:PLAN:BEGIN -->
+1. Freeze IR design decisions (recorded in design doc §6 update): implicit row cursors (no idx params), strict block-param SSA (cross-block value uses forbidden — no dominance analysis needed), acyclic CFG for v0, terminators emit/skip/trap/jump/brif, store-completeness dataflow at emit.
+2. Implement src/specializer/ir/: core types + instructions (mod.rs), verifier (verify.rs), printer (print.rs), parser (parse.rs), shared fixtures (fixtures.rs).
+3. Tests: per-instruction fixture programs (parse+verify+round-trip), negative verifier tests per rule, negative parser tests, deterministic seeded fuzz round-trip (hand-rolled xorshift generator, no new deps).
+4. Adversarial workflow: fan-out attackers on verifier soundness + round-trip edge cases (float/string literals), plus design-conformance and simplification reviewers; fix confirmed findings.
+5. Gate green; stacked PR onto claude/duckdb-native-interpreter-36d016.
+<!-- SECTION:PLAN:END -->
+
+## Implementation Notes
+
+<!-- SECTION:NOTES:BEGIN -->
+Implemented in src/specializer/ir/ (mod, verify, print, parse, fixtures, gen, tests). Key decisions vs the original sketch (design doc §6 updated): implicit row cursor, emit/skip/trap terminators carrying the store contract, strict block-param SSA (no dominance analysis), acyclic v0 CFG, presentation-only names (canonical %vN/bN). Adversarial pass (6 agents) found and I fixed: recursive-DFS process abort on deep CFGs (now iterative, 50k blocks OK), empty map static signatures and non-ident fn names verifying but printing unparseably, non-canonical NaN payloads breaking bitwise round-trip equality (NaN-class equality now), unreachable-island starvation masking join store errors (topo indegrees over reachable sources only), doc/grammar drift, dead uses() code. 45 cargo tests; every verifier rule and parser guard has a rejecting test; 300-seed fuzz round-trip.
+<!-- SECTION:NOTES:END -->

docs/superpowers/specs/2026-07-25-sql-specializer-design.md

@@ -166,40 +166,67 @@ enum StaticStruct {
 }
 ```
 
-## 6. Imperative IR sketch
+## 6. Imperative IR (as implemented — M-ir, `src/specializer/ir/`)
 
 SSA, typed, no allocation vocabulary, explicit null lane. Text format is the
-diagnostic surface and must round-trip (`parse(print(ir)) == ir`).
+diagnostic surface and round-trips: `parse(print(p)) == p`. The module docs of
+`src/specializer/ir/mod.rs` are the normative spec; highlights:
 
 ```
-;; SELECT age / s.mean_age AS z FROM __THIS__ t LEFT JOIN stats s ON t.seg = s.seg
-;; after BTA: stats collapsed into staticref @0 (perfect hash: seg -> mean_age)
+static @0: map(str) -> (f64)
 
 fn run(in: batch{age: i64?, seg: str}, out: batch{z: f64?}) {
-entry(row: idx):
-  %age.f, %age.v = load.opt in.age, row        ; (i1 flag, i64 payload)
-  %seg        = load     in.seg, row           ; NOT NULL lane: no flag
-  %hit.f, %m  = probe.opt @0, %seg             ; miss -> flag=0 (LEFT JOIN)
-  %num        = cast f64, %age.v
-  %q          = fdiv %num, %m
-  %z.f        = and %age.f, %hit.f             ; null iff either input null
-  store.opt out.z, row, %z.f, %q
-  next row
+entry:
+  %age_f, %age_v = load.opt in.age    # (i1 flag, i64 payload); row cursor implicit
+  %seg = load in.seg                  # NOT NULL lane: no flag
+  %hit, %mean = probe @0, %seg        # miss -> hit=false (LEFT JOIN)
+  %num = itof %age_v
+  %q = fdiv %num, %mean
+  %zf = and %age_f, %hit              # null iff either input null
+  store.opt out.z, %zf, %q
+  emit
 }
 ```
 
-Verifier rules (initial set):
-
-1. SSA: single def, defs dominate uses.
-2. Type check every op; `load.opt`/`probe.opt`/`store.opt` are the only ops that
-   touch flags; a `T?` value cannot flow into an arithmetic op — the verifier
-   rejects it (this is the "3VL mistakes are statically impossible" property).
-3. `StaticRef` ids must resolve against the plan's static-structure table, with
-   matching key/value types.
-4. No op allocates; `scratch` is reachable only from varlen `store` ops.
-5. `out` column set and row count semantics must match the declared plan shape
-   (`|out| = |in|` for pure projection; filter introduces the one allowed
-   divergence and must declare it).
+Decisions made at implementation (deviations from the original sketch, all in
+the direction of a smaller, more verifiable core):
+
+- **Implicit row cursor** — no `idx` values, no `row` operand; nothing in v0
+  needs random row access, and it removes a whole type from the verifier.
+- **Terminators carry the row protocol**: `emit` (row complete; every out
+  column stored exactly once on the path), `skip` (filter drop; path must
+  store nothing), `trap "msg"` (runtime error — CAST failures, div guards),
+  plus `jump`/`brif`. `|out| == |in|` iff `skip` is unreachable — statically
+  known, per the "filter must declare divergence" requirement.
+- **Strict block-param SSA**: values cross blocks only as branch args to
+  block params, so the verifier needs no dominance analysis. CFG acyclic in
+  v0 (lift when a lowering pattern needs loops, e.g. QuickScorer).
+- **Nullability is structural, not checked**: SSA values are always bare
+  scalars; only `load.opt`/`store.opt`/`probe`/`sload.opt` touch flags. A
+  `T?` cannot reach arithmetic because the type system cannot express it.
+- Names in text are presentation-only; printing canonicalizes to `%vN`/`bN`.
+  NaN payloads canonicalize to one `nan` token (literal equality is bitwise,
+  so `-0.0` and NaN round-trip).
+
+Verifier rules (each has a rejecting test in `ir/tests.rs`): structure (entry
+has no params, unique column names, no branch to entry, identifier function
+name, non-empty map signatures — a verified program must print to parseable
+text), SSA (single def, same-block visibility), per-op operand types incl.
+mandatory/forbidden `.opt` pairing against column/static nullability, static
+resolution + kind/arity/key types, CFG reachability + acyclicity + branch-arg
+typing (iterative DFS — deep legal CFGs must not overflow the native stack),
+and the store-completeness dataflow (never twice on any path, exactly-once
+per column at `emit`, zero at `skip`, agreement at joins, computed over the
+reachable subgraph so an unreachable island can't mask a join's errors).
+
+An adversarial pass (4 attack lenses + design-conformance + simplification
+reviews, 2026-07-25) ran against the initial implementation; every confirmed
+finding is pinned by a regression test in `ir/tests.rs`.
+
+Deferred to M-interp, pinned there against the DuckDB oracle: `ftoi.round`
+tie behavior and `fcmp` NaN ordering. `idiv`/`irem` trap on zero/overflow;
+SQL-level NULL-on-zero (or error) semantics are a lowering decision built
+from `brif` + `trap`.
 
 ## 7. Backends
 

src/lib.rs

@@ -17,6 +17,7 @@ mod duckdb;
 mod error;
 mod lookup;
 mod schema;
+pub mod specializer;
 mod types;
 mod value;
 

src/specializer/ir/fixtures.rs

@@ -0,0 +1,147 @@
+//! Hand-written IR programs, one habitat per instruction. Written in the
+//! human-friendly form (named values, named labels) that the parser accepts
+//! and the printer canonicalizes — the round-trip tests exercise exactly that
+//! path. M-interp reuses these as its first executable programs.
+
+/// The design-doc example: nullable arithmetic against a probed static.
+/// Covers: load, load.opt, probe, itof, fdiv, and, store.opt, emit.
+pub const PROJECTION: &str = r#"
+static @0: map(str) -> (f64)
+
+fn run(in: batch{age: i64?, seg: str}, out: batch{z: f64?}) {
+entry:
+  %age_f, %age_v = load.opt in.age
+  %seg = load in.seg
+  %hit, %mean = probe @0, %seg
+  %num = itof %age_v
+  %q = fdiv %num, %mean
+  %zf = and %age_f, %hit
+  store.opt out.z, %zf, %q
+  emit
+}
+"#;
+
+/// A WHERE clause: the one construct allowed to change |out|.
+/// Covers: const.f64, fcmp, brif (no args), skip, store.
+pub const FILTER: &str = r#"
+fn keep_positive(in: batch{score: f64}, out: batch{score: f64}) {
+entry:
+  %s = load in.score
+  %zero = const.f64 0.0
+  %pos = fcmp.gt %s, %zero
+  brif %pos, keep, drop
+keep:
+  %s2 = load in.score
+  store out.score, %s2
+  emit
+drop:
+  skip
+}
+"#;
+
+/// A CASE diamond joining through a block param, plus the i1 algebra.
+/// Covers: const.i64, const.i1, const.str, icmp, jump with args, block
+/// params, xor, not, select, store of i1.
+pub const CASE_DIAMOND: &str = r#"
+fn bucket(in: batch{age: i64}, out: batch{label: str, flag: i1}) {
+entry:
+  %age = load in.age
+  %lim = const.i64 30
+  %old = icmp.ge %age, %lim
+  brif %old, old_b, young_b
+old_b:
+  %a = const.str "old"
+  jump join(%a)
+young_b:
+  %b = const.str "young"
+  jump join(%b)
+join(%label: str):
+  store out.label, %label
+  %t = const.i1 true
+  %f = const.i1 false
+  %x = xor %t, %f
+  %n = not %x
+  %pick = select %n, %t, %f
+  store out.flag, %pick
+  emit
+}
+"#;
+
+/// The cast family and scalar statics; a failed parse traps (SQL CAST
+/// semantics — TRY_CAST lowers to a select instead).
+/// Covers: stoi.opt, sload, sload.opt, ftoi.round, ftoi.trunc, isub, ftos,
+/// sconcat, scmp, trap.
+pub const CASTS: &str = r#"
+static @0: scalar<f64>
+static @1: scalar<i64?>
+
+fn casts(in: batch{s: str}, out: batch{n: i64, msg: str}) {
+entry:
+  %raw = load in.s
+  %ok, %parsed = stoi.opt %raw
+  brif %ok, good, bad
+good:
+  %base = sload @0
+  %r1 = ftoi.round %base
+  %t1 = ftoi.trunc %base
+  %d = isub %r1, %t1
+  %pf, %pv = sload.opt @1
+  %n2 = select %pf, %pv, %d
+  store out.n, %n2
+  %ftxt = ftos %base
+  %sep = const.str ":"
+  %msg1 = sconcat %ftxt, %sep
+  %same = scmp.eq %msg1, %sep
+  %sel = select %same, %msg1, %sep
+  store out.msg, %sel
+  emit
+bad:
+  trap "cast to i64 failed"
+}
+"#;
+
+/// Everything else: the full integer/float binary set, a compound-key probe
+/// with multiple value columns, and the remaining casts.
+/// Covers: iadd, imul, idiv, irem, fadd, fsub, fmul, or, icmp.ne, fcmp.lt,
+/// itos, stof.opt, multi-key/multi-value probe, quoted column names.
+pub const KITCHEN: &str = r#"
+static @0: map(i64, str) -> (f64, i64)
+
+fn kitchen(in: batch{a: i64, b: i64?, k: str, x: f64}, out: batch{"r?": f64?, s: str}) {
+entry:
+  %a = load in.a
+  %bf, %bv = load.opt in.b
+  %sum = iadd %a, %bv
+  %prod = imul %sum, %a
+  %quot = idiv %prod, %a
+  %rem = irem %quot, %a
+  %k = load in.k
+  %h, %vf, %vi = probe @0, %rem, %k
+  %x = load in.x
+  %fa = fadd %x, %vf
+  %fs = fsub %fa, %vf
+  %fm = fmul %fs, %x
+  %lt = fcmp.lt %fm, %x
+  %ne = icmp.ne %vi, %a
+  %both = or %lt, %ne
+  %rf = and %both, %bf
+  %rv = select %lt, %fm, %x
+  store.opt out."r?", %rf, %rv
+  %istr = itos %vi
+  %ff, %fv = stof.opt %istr
+  %num2 = select %ff, %fv, %fm
+  %ns = ftos %num2
+  store out.s, %ns
+  emit
+}
+"#;
+
+pub fn all() -> Vec<(&'static str, &'static str)> {
+    vec![
+        ("projection", PROJECTION),
+        ("filter", FILTER),
+        ("case_diamond", CASE_DIAMOND),
+        ("casts", CASTS),
+        ("kitchen", KITCHEN),
+    ]
+}