fix(specializer): harden the IR boundary against adversarial findings — TASK-41

Six agents (4 attack lenses + 2 reviews) probed the initial IR; every
confirmed finding is fixed and pinned by a regression test:

- reachability DFS made iterative: a ~8k-block legal CFG stack-overflowed
  the process; 50k blocks now verify (deep_cfg_verifies_without_crashing)
- verified programs must print to parseable text: reject empty map static
  signatures (grammar can't express `map() -> ()`) and non-identifier
  function names
- Lit::F64 equality treats all NaNs as one class, matching the text form's
  canonical `nan` token — non-canonical payloads round-trip again
- store dataflow runs over the reachable subgraph: an unreachable cyclic
  island no longer starves a reachable join and masks its store errors
- docs aligned: double stores rejected on ALL paths incl. trap (deliberate),
  grammar EBNF covers store/comments/lenient %names, canonical-form note
- dead Inst::uses/Term::uses deleted; 7 missing rule-coverage tests added
  (entry params, duplicate cols, branch-to-entry, sload-on-map, scalar-static
  .opt pairing both ways, store.opt on non-nullable)

cargo 45 passed; gate green.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

Author: ahrzb

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

@@ -209,12 +209,19 @@ the direction of a smaller, more verifiable core):
   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), 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, and the
-store-completeness dataflow (exactly-once per column at `emit`, zero at
-`skip`, agreement at joins).
+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;

src/specializer/ir/mod.rs

@@ -18,6 +18,10 @@
 //! * `trap "msg"` — abort the whole call with a runtime error (CAST failures,
 //!   division guards — whatever the lowered dialect defines as an error).
 //!
+//! No path may store the same column twice, whatever its terminator — a
+//! double store is always a lowering bug, so the verifier rejects it even on
+//! paths that end in `trap`.
+//!
 //! `|out| == |in|` therefore holds exactly when `skip` is unreachable, which
 //! is statically known — the design doc's "filter is the one allowed
 //! divergence and must declare it".
@@ -66,12 +70,16 @@
 //!
 //! Canonical, round-trippable; `parse(print(p)) == p` for every program whose
 //! value ids are dense and in definition order (the parser and [`gen`] both
-//! produce that form, so the property is closed under round-trip). Names in
-//! the text are presentation only — they are not stored in the IR; printing
-//! uses canonical `%vN` / `bN` names.
+//! produce that form, so the property is closed under round-trip). A program
+//! with sparse or out-of-order ids still verifies and still prints; the
+//! round-trip then performs a bijective renumbering into canonical form, so
+//! structural equality is only meaningful between canonical programs. Names
+//! in the text are presentation only — they are not stored in the IR;
+//! printing uses canonical `%vN` / `bN` names.
 //!
 //! ```text
 //! program   := static* func
+//! comment   := "#" ... end-of-line     // allowed anywhere whitespace is
 //! static    := "static" "@" INT ":" static_ty
 //! static_ty := "scalar" "<" col_ty ">"
 //!            | "map" "(" ty ("," ty)* ")" "->" "(" ty ("," ty)* ")"
@@ -81,12 +89,15 @@
 //! col_ty    := ty ["?"]
 //! ty        := "i1" | "i64" | "f64" | "str"
 //! block     := IDENT ["(" VALUE ":" ty ("," VALUE ":" ty)* ")"] ":" inst* term
-//! inst      := VALUE ("," VALUE)* "=" OPCODE operands
+//! inst      := [VALUE ("," VALUE)* "="] OPCODE operands
+//!              // only store/store.opt omit the dests; everything else
+//!              // defines at least one value
 //! term      := "jump" target
 //!            | "brif" VALUE "," target "," target
 //!            | "emit" | "skip" | "trap" STRING
 //! target    := IDENT ["(" VALUE ("," VALUE)* ")"]
-//! VALUE     := "%" IDENT
+//! VALUE     := "%" NAME               // NAME: any run of [A-Za-z0-9_];
+//!                                     // the printer only emits %vN
 //! ```
 //!
 //! Instruction surface (`%d` result, `%f` an `i1` flag result):
@@ -179,9 +190,11 @@ pub struct Value(pub u32);
 #[derive(Clone, Copy, PartialEq, Eq, Debug, Hash)]
 pub struct BlockId(pub u32);
 
-/// Literal for `const.*`. `F64` equality is bitwise so that programs
-/// containing NaN still satisfy `parse(print(p)) == p` (the text form
-/// canonicalizes NaN payloads to the one `nan` token).
+/// Literal for `const.*`. `F64` equality is bitwise — so `-0.0 != 0.0`
+/// survives a round-trip — EXCEPT that all NaNs compare equal: the text form
+/// canonicalizes every NaN payload to the one `nan` token, and equality must
+/// match what the text format can distinguish or `parse(print(p)) == p`
+/// would fail for non-canonical payloads (found by adversarial fuzzing).
 #[derive(Clone, Debug)]
 pub enum Lit {
     I1(bool),
@@ -195,7 +208,9 @@ impl PartialEq for Lit {
         match (self, other) {
             (Lit::I1(a), Lit::I1(b)) => a == b,
             (Lit::I64(a), Lit::I64(b)) => a == b,
-            (Lit::F64(a), Lit::F64(b)) => a.to_bits() == b.to_bits(),
+            (Lit::F64(a), Lit::F64(b)) => {
+                a.to_bits() == b.to_bits() || (a.is_nan() && b.is_nan())
+            }
             (Lit::Str(a), Lit::Str(b)) => a == b,
             _ => false,
         }
@@ -463,30 +478,6 @@ impl Inst {
         }
     }
 
-    /// Values this instruction uses.
-    pub fn uses(&self) -> Vec<Value> {
-        match self {
-            Inst::Const { .. }
-            | Inst::Load { .. }
-            | Inst::LoadOpt { .. }
-            | Inst::Sload { .. }
-            | Inst::SloadOpt { .. } => vec![],
-            Inst::Not { a, .. }
-            | Inst::Itof { a, .. }
-            | Inst::Ftoi { a, .. }
-            | Inst::Itos { a, .. }
-            | Inst::Ftos { a, .. }
-            | Inst::StoiOpt { a, .. }
-            | Inst::StofOpt { a, .. } => vec![*a],
-            Inst::Bin { a, b, .. } | Inst::Cmp { a, b, .. } | Inst::Sconcat { a, b, .. } => {
-                vec![*a, *b]
-            }
-            Inst::Select { cond, a, b, .. } => vec![*cond, *a, *b],
-            Inst::Store { val, .. } => vec![*val],
-            Inst::StoreOpt { flag, val, .. } => vec![*flag, *val],
-            Inst::Probe { keys, .. } => keys.clone(),
-        }
-    }
 }
 
 impl Term {
@@ -507,17 +498,6 @@ impl Term {
             Term::Emit | Term::Skip | Term::Trap { .. } => vec![],
         }
     }
-
-    pub fn uses(&self) -> Vec<Value> {
-        let mut out = Vec::new();
-        if let Term::Brif { cond, .. } = self {
-            out.push(*cond);
-        }
-        for (_, args) in self.successors() {
-            out.extend_from_slice(args);
-        }
-        out
-    }
 }
 
 /// Builds programs with dense, definition-ordered value ids — the canonical

src/specializer/ir/print.rs

@@ -227,8 +227,10 @@ fn col_name(p: &Program, out: bool, idx: u32) -> String {
     }
 }
 
-/// Column and function names print bare when they are identifiers, quoted
-/// otherwise (SQL-derived output names like `COALESCE(a, b)` survive).
+/// Column names print bare when they are identifiers, quoted otherwise
+/// (SQL-derived output names like `COALESCE(a, b)` survive). Function names
+/// are NOT routed through this: the verifier requires them to be
+/// identifiers, so the printer writes them raw.
 fn ident_or_quoted(name: &str) -> String {
     if is_ident(name) {
         name.to_string()