From 76e31e0edbc6e390e448716104bf42b8061b8ef8 Mon Sep 17 00:00:00 2001
From: Jules <julesmt@amazon.com>
Date: Mon, 11 May 2026 17:11:27 -0700
Subject: [PATCH] Add DDM grammar productivity checker with correctness proofs
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Decides whether each declared category in a dialect admits a finite
parse tree.  Productivity is rooted in `frameworkAtomicCategories` —
the categories the parser constructs directly — with all other
categories derived from operator chains.

* Strata/DDM/Analysis/Productivity.lean — algorithm + wrapper
* Strata/DDM/Analysis/Productivity/Spec.lean — sound, complete, and
  correctness proofs for the fixpoint kernel and the top-level wrapper
* StrataTest/DDM/Analysis/ProductivityTest.lean — unit tests
* Scripts/ProductivityCheck.lean — `lake exe productivityCheck`

One sorry remains: `transitiveImports.fuel_suffices` — proving the
`n³` fuel bound is enough for the dialect-import-graph traversal.
---
 Scripts/ProductivityCheck.lean                |  63 +++
 Strata/DDM/Analysis/Productivity.lean         | 287 ++++++++++
 Strata/DDM/Analysis/Productivity/Spec.lean    | 513 ++++++++++++++++++
 Strata/DDM/BundledDialects.lean               |  49 ++
 StrataMain.lean                               |  13 +-
 StrataTest/DDM/Analysis/ProductivityTest.lean | 232 ++++++++
 lakefile.toml                                 |   4 +
 7 files changed, 1150 insertions(+), 11 deletions(-)
 create mode 100644 Scripts/ProductivityCheck.lean
 create mode 100644 Strata/DDM/Analysis/Productivity.lean
 create mode 100644 Strata/DDM/Analysis/Productivity/Spec.lean
 create mode 100644 Strata/DDM/BundledDialects.lean
 create mode 100644 StrataTest/DDM/Analysis/ProductivityTest.lean

diff --git a/Scripts/ProductivityCheck.lean b/Scripts/ProductivityCheck.lean
new file mode 100644
index 0000000000..b9dbad700e
--- /dev/null
+++ b/Scripts/ProductivityCheck.lean
@@ -0,0 +1,63 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+import Strata.DDM.Analysis.Productivity
+import Strata.DDM.BundledDialects
+
+/-! Quick CLI: `lake exe productivityCheck [<DialectName>|--all]`.
+The only trusted base is `frameworkAtomicCategories`; every other
+category must derive its productivity from operator chains rooted in
+those atoms. -/
+
+open Strata
+
+private def runOn (name : DialectName) : IO UInt32 := do
+  let dialects : DialectMap := DialectMap.ofList! bundledDialects.toList
+  if name ∉ dialects then
+    IO.eprintln s!"ERR: unknown dialect '{name}'"
+    IO.eprintln "Bundled dialects:"
+    for d in bundledDialects do
+      IO.eprintln s!"  {d.name}"
+    return 1
+  let r := Strata.DDM.Productivity.check dialects name
+  IO.println r.format
+  return (if r.isOk then 0 else 1)
+
+private def runAll : IO UInt32 := do
+  let dialects : DialectMap := DialectMap.ofList! bundledDialects.toList
+  let mut bad : Nat := 0
+  for d in bundledDialects do
+    let r := Strata.DDM.Productivity.check dialects d.name
+    let mark := if r.isOk then "✓" else "✗"
+    IO.println s!"{mark} {d.name}: {r.productive.size} productive, {r.unproductive.size} unproductive"
+    if !r.isOk then
+      bad := bad + 1
+      for u in r.unproductive do
+        IO.println s!"    - {u.category.fullName} ({u.blockers.size} blocker(s))"
+        for b in u.blockers do
+          let parts := String.intercalate ", " (b.unmetArgCats.toList.map QualifiedIdent.fullName)
+          IO.println s!"        op {b.opName} blocked on: {parts}"
+  IO.println ""
+  if bad == 0 then
+    IO.println s!"All {bundledDialects.size} dialects productive."
+    return 0
+  else
+    IO.println s!"{bad} of {bundledDialects.size} dialects have unproductive categories."
+    return 1
+
+def main (args : List String) : IO UInt32 := do
+  match args with
+  | [] | ["--help"] =>
+    IO.println "Usage: lake exe productivityCheck [<DialectName>|--all]"
+    IO.println ""
+    IO.println "Bundled dialects:"
+    for d in bundledDialects do
+      IO.println s!"  {d.name}"
+    return 0
+  | ["--all"] => runAll
+  | [name] => runOn name
+  | _ =>
+    IO.eprintln "ERR: expected exactly one dialect name, --all, or --help"
+    return 1
diff --git a/Strata/DDM/Analysis/Productivity.lean b/Strata/DDM/Analysis/Productivity.lean
new file mode 100644
index 0000000000..c234397c7e
--- /dev/null
+++ b/Strata/DDM/Analysis/Productivity.lean
@@ -0,0 +1,287 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+public import Strata.DDM.AST
+
+/-!
+# Grammar Productivity Checker
+
+A category is *productive* iff some operator builds it from productive
+arguments.  The only base case is `frameworkAtomicCategories` — what
+the parser constructs directly.
+-/
+
+public section
+
+namespace Strata.DDM.Productivity
+
+/-! ## Skeleton types -/
+
+structure OpInfo where
+  name : String
+  result : QualifiedIdent
+  args : Array QualifiedIdent
+  deriving Repr, Inhabited
+
+structure Blocker where
+  opName : String
+  unmetArgCats : Array QualifiedIdent
+  deriving Repr, Inhabited
+
+structure UnproductiveCategory where
+  category : QualifiedIdent
+  blockers : Array Blocker
+  deriving Repr, Inhabited
+
+structure Result where
+  dialect : DialectName
+  productive : Array QualifiedIdent
+  unproductive : Array UnproductiveCategory
+  deriving Repr, Inhabited
+
+namespace Result
+
+def isOk (r : Result) : Bool := r.unproductive.isEmpty
+
+end Result
+
+/-! ## Skeleton extraction -/
+
+/-- Containers whose empty form is a valid value. -/
+def nullableContainers : Array QualifiedIdent := #[
+  q`Init.Seq, q`Init.Option,
+  q`Init.CommaSepBy, q`Init.SpaceSepBy, q`Init.SpacePrefixSepBy,
+  q`Init.NewlineSepBy, q`Init.SemicolonSepBy
+]
+
+private def isNullableContainer (c : SyntaxCat) : Bool :=
+  nullableContainers.any (· == c.name)
+
+private def isNonemptyMeta (m : Metadata) : Bool :=
+  q`StrataDDL.nonempty ∈ m
+
+/-- Every category in `c`'s type tree, DFS, head first. -/
+partial def collectAllCategories (c : SyntaxCat) : Array QualifiedIdent :=
+  c.args.foldl (init := #[c.name]) fun acc a => acc ++ collectAllCategories a
+
+/-- Argument's productivity obligations, accounting for `@[nonempty]`. -/
+def collectArgCategories (ad : ArgDecl) : Array QualifiedIdent :=
+  let cat := ad.kind.categoryOf
+  if cat.name == q`Init.Option then
+    #[cat.name]
+  else if isNullableContainer cat && !isNonemptyMeta ad.metadata then
+    #[cat.name]
+  else
+    collectAllCategories cat
+
+def opInfoOfDecl (decl : OpDecl) : OpInfo :=
+  let args := decl.argDecls.toArray.foldl (init := #[]) fun acc ad =>
+    acc ++ collectArgCategories ad
+  { name := decl.name, result := decl.category, args }
+
+def extractOps (d : Dialect) : Array OpInfo := Id.run do
+  let mut out : Array OpInfo := #[]
+  for decl in d.declarations do
+    if let .op od := decl then
+      out := out.push (opInfoOfDecl od)
+  return out
+
+def declaredCategories (d : Dialect) : Array QualifiedIdent := Id.run do
+  let mut out : Array QualifiedIdent := #[]
+  for decl in d.declarations do
+    if let .syncat sc := decl then
+      out := out.push { dialect := d.name, name := sc.name }
+  return out
+
+/-! ## Trusted seed (framework atoms only) -/
+
+/-- Categories the parser constructs directly — the only trusted base. -/
+def frameworkAtomicCategories : Array QualifiedIdent := #[
+  q`Init.Ident, q`Init.Num, q`Init.Str, q`Init.ByteArray, q`Init.Decimal,
+  q`Init.Seq, q`Init.Option,
+  q`Init.CommaSepBy, q`Init.SpaceSepBy, q`Init.SpacePrefixSepBy,
+  q`Init.NewlineSepBy, q`Init.SemicolonSepBy
+]
+
+@[expose] def trustedCategories : Std.HashSet QualifiedIdent :=
+  frameworkAtomicCategories.foldl (init := (∅ : Std.HashSet QualifiedIdent))
+    (fun acc c => acc.insert c)
+
+theorem trustedCategories_eq :
+    trustedCategories =
+      frameworkAtomicCategories.foldl (init := (∅ : Std.HashSet QualifiedIdent))
+        (fun acc c => acc.insert c) := rfl
+
+/-! ## Import closure -/
+
+private def transitiveImports.step (dialects : DialectMap)
+    (state : Std.HashSet DialectName × Array DialectName)
+    : Std.HashSet DialectName × Array DialectName :=
+  let (seen, stack) := state
+  match stack.back? with
+  | none => (seen, stack)
+  | some name =>
+    let stack := stack.pop
+    if seen.contains name then (seen, stack)
+    else
+      let seen := seen.insert name
+      let stack :=
+        if hMem : name ∈ dialects then
+          (dialects[name]'hMem).imports.foldl (init := stack) fun s imp =>
+            if seen.contains imp then s else s.push imp
+        else stack
+      (seen, stack)
+
+private def transitiveImports.loop (dialects : DialectMap)
+    : Nat → Std.HashSet DialectName × Array DialectName
+            → Std.HashSet DialectName
+  | 0,     (seen, _) => seen
+  | _ + 1, (seen, #[]) => seen
+  | n + 1, state =>
+    transitiveImports.loop dialects n (transitiveImports.step dialects state)
+
+/-- Fuel for the closure walk: pushes ≤ `n` (fresh-seen) × `n`
+(imports per dialect) = `n²`; `n³` is comfortable slack. -/
+def transitiveImports.fuel (n : Nat) : Nat := n * n * n
+
+/-- Dialects reachable from `start` via `imports` (including `start`). -/
+def transitiveImports
+    (dialects : DialectMap) (start : DialectName) : Std.HashSet DialectName :=
+  let n := dialects.toList.length
+  transitiveImports.loop dialects (transitiveImports.fuel n) ({}, #[start])
+
+/-- Spec: `d` is reachable from `start` via `imports` edges. -/
+inductive ReachableViaImports (D : DialectMap) (start : DialectName)
+    : DialectName → Prop where
+  | self : ReachableViaImports D start start
+  | step : ∀ {a b}, ReachableViaImports D start a →
+      (h : a ∈ D) → b ∈ (D[a]'h).imports →
+      ReachableViaImports D start b
+
+/-- The closure walk returns exactly the reachable set.  Open obligation. -/
+theorem transitiveImports.fuel_suffices
+    (D : DialectMap) (start : DialectName) :
+    ∀ d, ReachableViaImports D start d ↔ d ∈ transitiveImports D start := by
+  sorry
+
+/-- Operators from `target` and its transitive imports. -/
+def extractOpsClosure (dialects : DialectMap) (target : DialectName)
+    : Array OpInfo := Id.run do
+  let imports := transitiveImports dialects target
+  let mut out : Array OpInfo := #[]
+  for d in dialects.toList do
+    if imports.contains d.name then
+      out := out ++ extractOps d
+  return out
+
+/-! ## Fixpoint -/
+
+/-- One round: add `op.result` for every op whose args are all in `productive`. -/
+@[expose] def step (ops : Array OpInfo) (productive : Std.HashSet QualifiedIdent)
+    : Std.HashSet QualifiedIdent :=
+  ops.foldl (init := productive) fun acc op =>
+    if op.args.all acc.contains then acc.insert op.result else acc
+
+theorem step_eq (ops : Array OpInfo) (productive : Std.HashSet QualifiedIdent) :
+    step ops productive =
+    ops.foldl (init := productive)
+      (fun acc op => if op.args.all acc.contains then acc.insert op.result else acc) :=
+  rfl
+
+/-- Iterate `step`, early-exit on no growth. -/
+@[expose] def iterate (ops : Array OpInfo) (productive : Std.HashSet QualifiedIdent)
+    : Nat → Std.HashSet QualifiedIdent
+  | 0 => productive
+  | n + 1 =>
+    let next := step ops productive
+    if next.size == productive.size then productive
+    else iterate ops next n
+
+theorem iterate_zero (ops : Array OpInfo) (s : Std.HashSet QualifiedIdent) :
+    iterate ops s 0 = s := rfl
+
+theorem iterate_succ
+    (ops : Array OpInfo) (s : Std.HashSet QualifiedIdent) (n : Nat) :
+    iterate ops s (n + 1) =
+      (let next := step ops s
+       if next.size == s.size then s else iterate ops next n) := rfl
+
+/-- Least productive set.  Fuel `ops.size + 1` suffices (one op-result per round). -/
+@[expose] def runFixpoint
+    (trusted : Std.HashSet QualifiedIdent) (ops : Array OpInfo)
+    : Std.HashSet QualifiedIdent :=
+  iterate ops trusted (ops.size + 1)
+
+theorem runFixpoint_eq
+    (trusted : Std.HashSet QualifiedIdent) (ops : Array OpInfo) :
+    runFixpoint trusted ops = iterate ops trusted (ops.size + 1) := rfl
+
+/-! ## Diagnostics -/
+
+def blockersForCategory
+    (cat : QualifiedIdent) (ops : Array OpInfo)
+    (productive : Std.HashSet QualifiedIdent) : Array Blocker := Id.run do
+  let mut out : Array Blocker := #[]
+  for op in ops do
+    if op.result != cat then continue
+    let unmet := op.args.filter (! productive.contains ·)
+    out := out.push { opName := op.name, unmetArgCats := unmet }
+  return out
+
+/-- Run the checker on `target`.  Seed: framework atoms; pool: `target` +
+transitive imports; output: verdicts for `target`'s declared categories. -/
+@[expose] def check (dialects : DialectMap) (target : DialectName) : Result :=
+  if h : target ∈ dialects then
+    let d := dialects[target]
+    let ops := extractOpsClosure dialects target
+    let cats := declaredCategories d
+    let productive := runFixpoint trustedCategories ops
+    let prodOut := cats.filter (productive.contains ·)
+    let unprodOut := (cats.filter (! productive.contains ·)).map fun c =>
+      { category := c, blockers := blockersForCategory c ops productive }
+    { dialect := target, productive := prodOut, unproductive := unprodOut }
+  else
+    panic! s!"productivity check: dialect {target} not in DialectMap"
+
+/-- `check`'s `productive` field as a `filter`. -/
+theorem check_productive_eq
+    (dialects : DialectMap) (target : DialectName) (h : target ∈ dialects) :
+    (check dialects target).productive =
+      (declaredCategories (dialects[target]'h)).filter
+        ((runFixpoint trustedCategories
+            (extractOpsClosure dialects target)).contains ·) := by
+  simp [check, h]
+
+/-! ## Pretty-printing -/
+
+private def joinCommaSep (xs : Array QualifiedIdent) : String :=
+  String.intercalate ", " (xs.toList.map QualifiedIdent.fullName)
+
+private def formatBlocker (b : Blocker) : String :=
+  s!"    op {b.opName} blocked on: {joinCommaSep b.unmetArgCats}"
+
+private def formatUnproductive (u : UnproductiveCategory) : String :=
+  let header := s!"  ✗ {u.category.fullName}"
+  if u.blockers.isEmpty then
+    s!"{header}\n    (no operator declares this category)"
+  else
+    String.intercalate "\n" (header :: u.blockers.toList.map formatBlocker)
+
+def Result.format (r : Result) : String :=
+  let head := s!"Productivity check for dialect {r.dialect}:"
+  let noun := if r.productive.size == 1 then "category" else "categories"
+  let prodLine := s!"  ✓ {r.productive.size} {noun} productive"
+  if r.unproductive.isEmpty then
+    s!"{head}\n{prodLine}"
+  else
+    let unprodHdr := s!"  ✗ {r.unproductive.size} unproductive:"
+    String.intercalate "\n"
+      (head :: prodLine :: unprodHdr :: r.unproductive.toList.map formatUnproductive)
+
+end Strata.DDM.Productivity
+
+end
diff --git a/Strata/DDM/Analysis/Productivity/Spec.lean b/Strata/DDM/Analysis/Productivity/Spec.lean
new file mode 100644
index 0000000000..a0607ca3b1
--- /dev/null
+++ b/Strata/DDM/Analysis/Productivity/Spec.lean
@@ -0,0 +1,513 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+public import Strata.DDM.Analysis.Productivity
+public import Std.Data.HashSet.Lemmas
+
+/-!
+# Productivity spec
+
+`Productive` is the inductive spec; `runFixpoint` computes it.  Kernel
+theorems are parametric in the seed; `runFixpoint_strict_correct`
+specialises to the strict mode where the seed is
+`frameworkAtomicCategories`.
+-/
+
+public section
+
+namespace Strata.DDM.Productivity
+
+/-! ## Spec -/
+
+/--
+Inductive specification of productivity over a flat operator pool.
+
+`OpInfo` is the productivity-relevant skeleton of an operator
+declaration: its result category and the categories of its arguments,
+flattened by `opInfoOfDecl`.  `extractOps` produces these from a
+`Dialect` and `extractOpsClosure` from a target dialect plus its
+import closure.
+
+`Productive ops base C` says category `C` admits a finite derivation
+tree using operators from `ops`, with leaves drawn from `base`
+(typically `frameworkAtomicCategories` — the categories the parser
+constructs directly).
+-/
+inductive Productive (ops : Array OpInfo) (base : QualifiedIdent → Prop)
+    : QualifiedIdent → Prop where
+  | byBase : ∀ {C}, base C → Productive ops base C
+  | byOp : ∀ (op : OpInfo),
+      op ∈ ops →
+      (∀ a ∈ op.args, Productive ops base a) →
+      Productive ops base op.result
+
+/-! ## Soundness -/
+
+theorem step_preserves_productive
+    {ops : Array OpInfo} {base : QualifiedIdent → Prop}
+    {productive : Std.HashSet QualifiedIdent}
+    (h : ∀ c, c ∈ productive → Productive ops base c) :
+    ∀ c, c ∈ step ops productive → Productive ops base c := by
+  intro c hc
+  rw [step_eq] at hc
+  refine Array.foldl_induction
+    (motive := fun _ acc => ∀ c, c ∈ acc → Productive ops base c)
+    h ?_ c hc
+  intro i acc accInv c hc
+  by_cases hall : (ops[i].args.all acc.contains) = true
+  · simp only [hall, if_true] at hc
+    rw [Std.HashSet.mem_insert] at hc
+    rcases hc with heq | hold
+    · have : ops[i].result = c := by simpa using heq
+      subst this
+      have argsProd : ∀ a ∈ ops[i].args, Productive ops base a := fun a haIn =>
+        accInv a (Std.HashSet.mem_iff_contains.mpr ((Array.all_eq_true'.mp hall) a haIn))
+      exact Productive.byOp ops[i] (Array.getElem_mem i.isLt) argsProd
+    · exact accInv c hold
+  · simp only [hall] at hc
+    exact accInv c hc
+
+theorem iterate_preserves_productive
+    (ops : Array OpInfo) (base : QualifiedIdent → Prop) :
+    ∀ (n : Nat) (s : Std.HashSet QualifiedIdent),
+      (∀ c, c ∈ s → Productive ops base c) →
+      ∀ c, c ∈ iterate ops s n → Productive ops base c
+  | 0, _, hs => fun c hc => by rw [iterate_zero] at hc; exact hs c hc
+  | n + 1, s, hs => by
+    intro c hc
+    rw [iterate_succ] at hc
+    by_cases hsame : ((step ops s).size == s.size) = true
+    · simp only [hsame, if_true] at hc; exact hs c hc
+    · simp only [hsame] at hc
+      exact iterate_preserves_productive ops base n (step ops s)
+        (step_preserves_productive hs) c hc
+
+theorem runFixpoint_sound
+    (ops : Array OpInfo) (trusted : Std.HashSet QualifiedIdent)
+    (baseSpec : QualifiedIdent → Prop)
+    (h0 : ∀ c, c ∈ trusted → baseSpec c) :
+    ∀ c, c ∈ runFixpoint trusted ops → Productive ops baseSpec c :=
+  iterate_preserves_productive ops baseSpec (ops.size + 1) trusted
+    (fun c hMem => Productive.byBase (h0 c hMem))
+
+/-! ## Monotonicity -/
+
+theorem step_mono
+    (ops : Array OpInfo) (s : Std.HashSet QualifiedIdent) :
+    ∀ c, c ∈ s → c ∈ step ops s := by
+  intro c hc
+  rw [step_eq]
+  refine Array.foldl_induction
+    (motive := fun _ acc => c ∈ acc) hc ?_
+  intro i acc accMem
+  by_cases hall : (ops[i].args.all acc.contains) = true
+  · simp only [hall, if_true]; exact Std.HashSet.mem_insert.mpr (Or.inr accMem)
+  · simp only [hall]; exact accMem
+
+theorem iterate_mono (ops : Array OpInfo) :
+    ∀ (n : Nat) (s : Std.HashSet QualifiedIdent) (c : QualifiedIdent),
+      c ∈ s → c ∈ iterate ops s n
+  | 0, _, _, hc => by rw [iterate_zero]; exact hc
+  | n + 1, s, c, hc => by
+    rw [iterate_succ]
+    by_cases hsame : ((step ops s).size == s.size) = true
+    · simp only [hsame, if_true]; exact hc
+    · simp only [hsame]
+      exact iterate_mono ops n (step ops s) c (step_mono ops s c hc)
+
+/-- Args of `op` in `s` ⇒ `op.result ∈ step ops s`. -/
+theorem step_grows
+    (ops : Array OpInfo) (s : Std.HashSet QualifiedIdent)
+    (op : OpInfo) (hOp : op ∈ ops)
+    (hArgs : ∀ a ∈ op.args, a ∈ s) :
+    op.result ∈ step ops s := by
+  rw [step_eq]
+  obtain ⟨i, hi_lt, hi⟩ := Array.getElem_of_mem hOp
+  have key := Array.foldl_induction
+    (as := ops) (init := s)
+    (f := fun acc op' =>
+      if op'.args.all acc.contains then acc.insert op'.result else acc)
+    (motive := fun j acc =>
+      (∀ a ∈ op.args, a ∈ acc) ∧ (j > i → op.result ∈ acc))
+    ⟨hArgs, fun h => absurd h (Nat.not_lt_zero _)⟩
+    (by
+      intro j acc ⟨accArgs, accAfter⟩
+      refine ⟨?_, ?_⟩
+      · intro a haIn
+        by_cases hall : (ops[j].args.all acc.contains) = true
+        · simp only [hall, if_true]
+          exact Std.HashSet.mem_insert.mpr (Or.inr (accArgs a haIn))
+        · simp only [hall]; exact accArgs a haIn
+      · intro hgt
+        by_cases hjeq : j.val = i
+        · have hopEq : ops[j] = op := by
+            have : ops[j.val]'j.isLt = ops[i]'hi_lt := by simp [hjeq]
+            rw [show ops[j] = ops[j.val]'j.isLt from rfl, this, hi]
+          have hallArgs : ops[j].args.all acc.contains = true := by
+            rw [hopEq]
+            exact Array.all_eq_true'.mpr fun a haIn =>
+              Std.HashSet.mem_iff_contains.mp (accArgs a haIn)
+          simp only [hallArgs, if_true]
+          have hresEq : ops[j].result = op.result := by rw [hopEq]
+          rw [hresEq]
+          exact Std.HashSet.mem_insert_self
+        · have hjgt : j.val > i := by have : j.val + 1 > i := hgt; omega
+          have prev : op.result ∈ acc := accAfter hjgt
+          by_cases hall : (ops[j].args.all acc.contains) = true
+          · simp only [hall, if_true]
+            exact Std.HashSet.mem_insert.mpr (Or.inr prev)
+          · simp only [hall]; exact prev)
+  exact key.2 hi_lt
+
+/-! ## Size bookkeeping -/
+
+theorem step_size_mono (ops : Array OpInfo) (s : Std.HashSet QualifiedIdent) :
+    s.size ≤ (step ops s).size := by
+  rw [step_eq]
+  refine Array.foldl_induction
+    (motive := fun _ acc => s.size ≤ Std.HashSet.size acc) (Nat.le_refl _) ?_
+  intro i acc accLe
+  by_cases hall : (ops[i].args.all acc.contains) = true
+  · simp only [hall, if_true]
+    exact Nat.le_trans accLe Std.HashSet.size_le_size_insert
+  · simp only [hall]; exact accLe
+
+/-- `step` preserves size ⇒ preserves membership. -/
+theorem step_size_eq_implies_mem_eq
+    (ops : Array OpInfo) (s : Std.HashSet QualifiedIdent)
+    (heq : (step ops s).size = s.size) :
+    ∀ c, c ∈ step ops s → c ∈ s := by
+  have key :
+      (Std.HashSet.size (step ops s) = s.size
+        ∧ ∀ c, c ∈ step ops s → c ∈ s)
+      ∨ Std.HashSet.size (step ops s) > s.size := by
+    rw [step_eq]
+    refine Array.foldl_induction
+      (motive := fun _ acc =>
+        (Std.HashSet.size acc = s.size ∧ ∀ c, c ∈ acc → c ∈ s)
+        ∨ Std.HashSet.size acc > s.size)
+      (Or.inl ⟨rfl, fun _ h => h⟩) ?_
+    intro i acc accInv
+    by_cases hall : (ops[i].args.all acc.contains) = true
+    · simp only [hall, if_true]
+      by_cases hin : ops[i].result ∈ acc
+      · rcases accInv with ⟨hsz, hmem⟩ | hgt
+        · refine Or.inl ⟨?_, ?_⟩
+          · rw [Std.HashSet.size_insert, if_pos hin]; exact hsz
+          · intro c hc
+            rw [Std.HashSet.mem_insert] at hc
+            rcases hc with heq2 | hold
+            · have : ops[i].result = c := by simpa using heq2
+              subst this; exact hmem _ hin
+            · exact hmem _ hold
+        · right; rw [Std.HashSet.size_insert, if_pos hin]; exact hgt
+      · right
+        rw [Std.HashSet.size_insert, if_neg hin]
+        rcases accInv with ⟨hsz, _⟩ | hgt
+        · rw [hsz]; exact Nat.lt_succ_self _
+        · exact Nat.lt_succ_of_lt hgt
+    · simp only [hall]; exact accInv
+  rcases key with ⟨_, hmem⟩ | hgt
+  · exact hmem
+  · exfalso; exact Nat.lt_irrefl _ (heq ▸ hgt)
+
+/-! ## Bounding the iterated set -/
+
+theorem step_mem_origin (ops : Array OpInfo) (s : Std.HashSet QualifiedIdent) :
+    ∀ c, c ∈ step ops s → c ∈ s ∨ ∃ op ∈ ops, op.result = c := by
+  rw [step_eq]
+  intro c
+  refine Array.foldl_induction
+    (motive := fun _ acc =>
+      c ∈ acc → c ∈ s ∨ ∃ op ∈ ops, op.result = c)
+    (fun h => Or.inl h) ?_
+  intro i acc accInv hMem
+  by_cases hall : (ops[i].args.all acc.contains) = true
+  · simp only [hall, if_true] at hMem
+    rw [Std.HashSet.mem_insert] at hMem
+    rcases hMem with heq | hold
+    · right
+      have : ops[i].result = c := by simpa using heq
+      exact ⟨ops[i], Array.getElem_mem i.isLt, this⟩
+    · exact accInv hold
+  · simp only [hall] at hMem; exact accInv hMem
+
+theorem iterate_mem_origin (ops : Array OpInfo) :
+    ∀ (n : Nat) (s : Std.HashSet QualifiedIdent) (c : QualifiedIdent),
+      c ∈ iterate ops s n → c ∈ s ∨ ∃ op ∈ ops, op.result = c
+  | 0, s, c, hMem => by rw [iterate_zero] at hMem; exact Or.inl hMem
+  | n + 1, s, c, hMem => by
+    rw [iterate_succ] at hMem
+    by_cases hsame : ((step ops s).size == s.size) = true
+    · simp only [hsame, if_true] at hMem; exact Or.inl hMem
+    · simp only [hsame] at hMem
+      rcases iterate_mem_origin ops n (step ops s) c hMem with hStep | hOp
+      · exact step_mem_origin ops s c hStep
+      · exact Or.inr hOp
+
+/-- `s ∪ { op.result | op ∈ ops }`. -/
+def boundingSet (ops : Array OpInfo) (s : Std.HashSet QualifiedIdent)
+    : Std.HashSet QualifiedIdent :=
+  ops.foldl (init := s) fun acc op => acc.insert op.result
+
+theorem mem_boundingSet_of_mem_iterate
+    (ops : Array OpInfo) (s : Std.HashSet QualifiedIdent) (n : Nat) :
+    ∀ c, c ∈ iterate ops s n → c ∈ boundingSet ops s := by
+  intro c hMem
+  rcases iterate_mem_origin ops n s c hMem with hS | ⟨op, hOp, hRes⟩
+  · show c ∈ ops.foldl (init := s) (fun acc op => acc.insert op.result)
+    refine Array.foldl_induction
+      (motive := fun _ acc => c ∈ acc) hS ?_
+    intro i acc accMem
+    exact Std.HashSet.mem_insert.mpr (Or.inr accMem)
+  · obtain ⟨i, hi_lt, hi⟩ := Array.getElem_of_mem hOp
+    show c ∈ ops.foldl (init := s) (fun acc op => acc.insert op.result)
+    have key := Array.foldl_induction
+      (as := ops) (init := s)
+      (f := fun acc op => acc.insert op.result)
+      (motive := fun j acc => j > i → c ∈ acc)
+      (fun h => absurd h (Nat.not_lt_zero _))
+      (by
+        intro j acc accAfter hgt
+        by_cases hjeq : j.val = i
+        · have hopEq : ops[j.val] = ops[i] := by simp [hjeq]
+          have hRes' : ops[j].result = c := by
+            show ops[j.val].result = c
+            rw [hopEq, hi]; exact hRes
+          show c ∈ acc.insert ops[j].result
+          rw [hRes']
+          exact Std.HashSet.mem_insert_self
+        · have hjgt : j.val > i := by have : j.val + 1 > i := hgt; omega
+          exact Std.HashSet.mem_insert.mpr (Or.inr (accAfter hjgt)))
+    exact key hi_lt
+
+theorem boundingSet_size_le (ops : Array OpInfo) (s : Std.HashSet QualifiedIdent) :
+    (boundingSet ops s).size ≤ s.size + ops.size := by
+  show Std.HashSet.size
+        (ops.foldl (init := s) (fun acc op => acc.insert op.result))
+      ≤ s.size + ops.size
+  refine Array.foldl_induction
+    (motive := fun i acc => Std.HashSet.size acc ≤ s.size + i)
+    (Nat.le_refl _) ?_
+  intro i acc accLe
+  calc (acc.insert ops[i].result).size
+      ≤ acc.size + 1 := Std.HashSet.size_insert_le
+    _ ≤ s.size + i.val + 1 := Nat.add_le_add_right accLe 1
+    _ = s.size + (i.val + 1) := by omega
+
+theorem hashset_size_le_of_subset
+    (r t : Std.HashSet QualifiedIdent)
+    (hSub : ∀ c, c ∈ r → c ∈ t) :
+    r.size ≤ t.size := by
+  have : (r ∩ t).size = r.size :=
+    Std.HashSet.size_inter_eq_size_left hSub
+  calc r.size = (r ∩ t).size := this.symm
+    _ ≤ t.size := Std.HashSet.size_inter_le_size_right
+
+theorem iterate_size_bound (ops : Array OpInfo) (s : Std.HashSet QualifiedIdent)
+    (n : Nat) :
+    (iterate ops s n).size ≤ s.size + ops.size := by
+  calc (iterate ops s n).size
+      ≤ (boundingSet ops s).size :=
+        hashset_size_le_of_subset _ _ (mem_boundingSet_of_mem_iterate ops s n)
+    _ ≤ s.size + ops.size := boundingSet_size_le ops s
+
+/-! ## Closure under `step` (fuel suffices) -/
+
+/-- After `n` rounds, `iterate` is either at a fixedpoint or has grown by `n`. -/
+theorem iterate_fixedpoint_or_grew
+    (ops : Array OpInfo) :
+    ∀ (n : Nat) (s : Std.HashSet QualifiedIdent),
+      (∀ c, c ∈ step ops (iterate ops s n) → c ∈ iterate ops s n)
+      ∨ (iterate ops s n).size ≥ s.size + n
+  | 0, s => by rw [iterate_zero]; exact Or.inr (Nat.le_refl _)
+  | n + 1, s => by
+    rw [iterate_succ]
+    by_cases hsame : ((step ops s).size == s.size) = true
+    · simp only [hsame, if_true]
+      left
+      exact step_size_eq_implies_mem_eq ops s
+        ((Nat.beq_eq_true_eq _ _).mp hsame)
+    · have hsame' : ((step ops s).size == s.size) = false := by
+        rcases h : ((step ops s).size == s.size) with _ | _
+        · rfl
+        · exact absurd h hsame
+      rw [show (if ((step ops s).size == s.size) = true
+                then s
+                else iterate ops (step ops s) n)
+              = iterate ops (step ops s) n from by simp [hsame']]
+      rcases iterate_fixedpoint_or_grew ops n (step ops s) with hFix | hGrew
+      · exact Or.inl hFix
+      · right
+        have hStrict : (step ops s).size ≥ s.size + 1 := by
+          have hMono := step_size_mono ops s
+          have hNeq : (step ops s).size ≠ s.size := fun hEq =>
+            hsame ((Nat.beq_eq_true_eq _ _).mpr hEq)
+          omega
+        omega
+
+theorem runFixpoint_isFixed
+    (ops : Array OpInfo) (trusted : Std.HashSet QualifiedIdent)
+    (c : QualifiedIdent) :
+    c ∈ step ops (runFixpoint trusted ops) → c ∈ runFixpoint trusted ops := by
+  intro hMem
+  rw [runFixpoint_eq] at *
+  rcases iterate_fixedpoint_or_grew ops (ops.size + 1) trusted with hFix | hGrew
+  · exact hFix c hMem
+  · have hLe : (iterate ops trusted (ops.size + 1)).size ≤ trusted.size + ops.size :=
+      iterate_size_bound ops trusted (ops.size + 1)
+    omega
+
+/-! ## Completeness and parametric correctness -/
+
+theorem runFixpoint_complete
+    (ops : Array OpInfo) (trusted : Std.HashSet QualifiedIdent)
+    (baseSpec : QualifiedIdent → Prop)
+    (h0 : ∀ c, baseSpec c → c ∈ trusted) :
+    ∀ c, Productive ops baseSpec c → c ∈ runFixpoint trusted ops := by
+  intro c hC
+  induction hC with
+  | @byBase C hT =>
+    rw [runFixpoint_eq]
+    exact iterate_mono ops (ops.size + 1) trusted C (h0 _ hT)
+  | byOp op hOp _ argIH =>
+    exact runFixpoint_isFixed ops trusted op.result
+      (step_grows ops _ op hOp argIH)
+
+/-- Parametric kernel correctness. -/
+theorem runFixpoint_correct
+    (ops : Array OpInfo) (trusted : Std.HashSet QualifiedIdent)
+    (baseSpec : QualifiedIdent → Prop)
+    (hAgree : ∀ c, c ∈ trusted ↔ baseSpec c) :
+    ∀ c, c ∈ runFixpoint trusted ops ↔ Productive ops baseSpec c := fun c =>
+  ⟨runFixpoint_sound ops trusted baseSpec (fun c h => (hAgree c).mp h) c,
+   runFixpoint_complete ops trusted baseSpec (fun c h => (hAgree c).mpr h) c⟩
+
+/-! ## Strict-mode bridge and top-level theorem -/
+
+/-- `trustedCategories` and `frameworkAtomicCategories` agree on membership. -/
+theorem mem_trustedCategories_iff_mem_frameworkAtomicCategories
+    (c : QualifiedIdent) :
+    c ∈ trustedCategories ↔ c ∈ frameworkAtomicCategories := by
+  show c ∈ frameworkAtomicCategories.foldl
+            (init := (∅ : Std.HashSet QualifiedIdent))
+            (fun acc x => acc.insert x)
+        ↔ c ∈ frameworkAtomicCategories
+  have key := Array.foldl_induction
+    (as := frameworkAtomicCategories)
+    (init := (∅ : Std.HashSet QualifiedIdent))
+    (f := fun acc x => acc.insert x)
+    (motive := fun j acc =>
+      c ∈ acc ↔
+        ∃ k : Nat, ∃ h : k < frameworkAtomicCategories.size,
+          k < j ∧ frameworkAtomicCategories[k]'h = c)
+    (by
+      refine ⟨fun h => ?_, fun ⟨_, _, hk, _⟩ => ?_⟩
+      · exact absurd h Std.HashSet.not_mem_empty
+      · exact absurd hk (Nat.not_lt_zero _))
+    (by
+      intro j acc accInv
+      refine ⟨fun h => ?_, fun ⟨k, hk_lt, hk_j, hk_eq⟩ => ?_⟩
+      · rw [Std.HashSet.mem_insert] at h
+        rcases h with hEq | hOld
+        · refine ⟨j.val, j.isLt, Nat.lt_succ_self _, ?_⟩
+          have : frameworkAtomicCategories[j.val] = c := by simpa using hEq
+          exact this
+        · rcases (accInv.mp hOld) with ⟨k, hk_lt, hk_j, hk_eq⟩
+          exact ⟨k, hk_lt, Nat.lt_succ_of_lt hk_j, hk_eq⟩
+      · rw [Std.HashSet.mem_insert]
+        by_cases hk_eq_j : k = j.val
+        · left
+          have hEq : frameworkAtomicCategories[j] = c := by
+            show frameworkAtomicCategories[j.val]'j.isLt = c
+            have : frameworkAtomicCategories[j.val]'j.isLt
+                    = frameworkAtomicCategories[k]'hk_lt := by simp [hk_eq_j]
+            rw [this, hk_eq]
+          simp [hEq]
+        · right
+          have hk_lt_j : k < j.val := by
+            have : k < j.val + 1 := hk_j
+            omega
+          exact accInv.mpr ⟨k, hk_lt, hk_lt_j, hk_eq⟩)
+  refine key.trans ?_
+  refine ⟨fun ⟨k, hk_lt, _, hk_eq⟩ => ?_, fun hMem => ?_⟩
+  · rw [← hk_eq]
+    exact Array.getElem_mem hk_lt
+  · obtain ⟨k, hk_lt, hk_eq⟩ := Array.getElem_of_mem hMem
+    exact ⟨k, hk_lt, hk_lt, hk_eq⟩
+
+/-! ## Strict-mode kernel correctness -/
+
+/-- Soundness: every algorithmic ✓ has a derivation tree rooted in
+`frameworkAtomicCategories`. -/
+theorem runFixpoint_strict_sound (ops : Array OpInfo) :
+    ∀ c, c ∈ runFixpoint trustedCategories ops
+          → Productive ops (· ∈ frameworkAtomicCategories) c :=
+  runFixpoint_sound ops trustedCategories (· ∈ frameworkAtomicCategories)
+    (fun c h => (mem_trustedCategories_iff_mem_frameworkAtomicCategories c).mp h)
+
+/-- Completeness: every spec-productive category is in the algorithmic
+output. -/
+theorem runFixpoint_strict_complete (ops : Array OpInfo) :
+    ∀ c, Productive ops (· ∈ frameworkAtomicCategories) c
+          → c ∈ runFixpoint trustedCategories ops :=
+  runFixpoint_complete ops trustedCategories (· ∈ frameworkAtomicCategories)
+    (fun c h => (mem_trustedCategories_iff_mem_frameworkAtomicCategories c).mpr h)
+
+/-- Strict-mode kernel correctness: sound and complete. -/
+theorem runFixpoint_strict_correct (ops : Array OpInfo) :
+    ∀ c, c ∈ runFixpoint trustedCategories ops
+          ↔ Productive ops (· ∈ frameworkAtomicCategories) c := fun c =>
+  ⟨runFixpoint_strict_sound ops c, runFixpoint_strict_complete ops c⟩
+
+/-! ## Wrapper correctness -/
+
+/-- Ops of every dialect reachable from `target`. -/
+def OpInPool (D : DialectMap) (target : DialectName) (op : OpInfo) : Prop :=
+  ∃ d : Dialect, d ∈ D.toList ∧
+    ReachableViaImports D target d.name ∧ op ∈ extractOps d
+
+/-- Soundness: every reported productive category is declared in `target`
+and has a derivation tree over `extractOpsClosure D target`. -/
+theorem check_sound
+    (D : DialectMap) (target : DialectName) (h : target ∈ D) (c : QualifiedIdent) :
+    c ∈ (check D target).productive →
+      c ∈ declaredCategories (D[target]'h)
+      ∧ Productive (extractOpsClosure D target)
+          (· ∈ frameworkAtomicCategories) c := by
+  intro hc
+  rw [check_productive_eq D target h, Array.mem_filter] at hc
+  exact ⟨hc.1, runFixpoint_strict_sound _ c
+    (Std.HashSet.mem_iff_contains.mpr hc.2)⟩
+
+/-- Completeness: every declared category with a derivation tree over
+`extractOpsClosure D target` is reported. -/
+theorem check_complete
+    (D : DialectMap) (target : DialectName) (h : target ∈ D) (c : QualifiedIdent) :
+    c ∈ declaredCategories (D[target]'h)
+    → Productive (extractOpsClosure D target)
+        (· ∈ frameworkAtomicCategories) c
+    → c ∈ (check D target).productive := by
+  intro hDecl hProd
+  rw [check_productive_eq D target h, Array.mem_filter]
+  exact ⟨hDecl, Std.HashSet.mem_iff_contains.mp
+    (runFixpoint_strict_complete _ c hProd)⟩
+
+/-- Wrapper correctness (sound and complete) modulo `extractOpsClosure`.
+Pair with `transitiveImports.fuel_suffices` for full-closure correctness. -/
+theorem check_correct
+    (D : DialectMap) (target : DialectName) (h : target ∈ D) (c : QualifiedIdent) :
+    c ∈ (check D target).productive ↔
+      c ∈ declaredCategories (D[target]'h)
+      ∧ Productive (extractOpsClosure D target)
+          (· ∈ frameworkAtomicCategories) c :=
+  ⟨check_sound D target h c,
+   fun ⟨hDecl, hProd⟩ => check_complete D target h c hDecl hProd⟩
+
+end Strata.DDM.Productivity
+
+end
diff --git a/Strata/DDM/BundledDialects.lean b/Strata/DDM/BundledDialects.lean
new file mode 100644
index 0000000000..62e73ce31f
--- /dev/null
+++ b/Strata/DDM/BundledDialects.lean
@@ -0,0 +1,49 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+public import Strata.DDM.BuiltinDialects
+public import Strata.Languages.Boole.Boole
+public import Strata.Languages.Core.DDMTransform.Grammar
+public import Strata.Languages.Dyn.DDMTransform.Parse
+public import Strata.Languages.B3.DDMTransform.DefinitionAST
+public import Strata.Languages.B3.DDMTransform.ParseCST
+public import Strata.Languages.Laurel.Grammar.LaurelGrammar
+public import Strata.Languages.Python.PythonDialect
+public import Strata.Languages.Python.Specs.DDM
+public import Strata.DL.SMT.DDMTransform.Parse
+
+/-! All dialects bundled with the `strata` binary.  Both the `strata`
+CLI and the `productivityCheck` script load dialects from this list so
+that they stay in sync. -/
+
+public section
+
+namespace Strata
+
+/-- Dialects shipped with the binary, in dependency order (each dialect
+appears after all of its imports). -/
+def bundledDialects : Array Dialect := #[
+  initDialect,
+  headerDialect,
+  StrataDDL,
+  smtReservedKeywordsDialect,
+  SMTCore,
+  SMT,
+  SMTResponse,
+  Core,
+  Boole,
+  Dyn,
+  Python.Python,
+  Python.Specs.DDM.PythonSpecs,
+  B3AST,
+  B3CST,
+  Laurel.Laurel
+]
+
+end Strata
+
+end
diff --git a/StrataMain.lean b/StrataMain.lean
index 1e6700ff54..dcd8e21a18 100644
--- a/StrataMain.lean
+++ b/StrataMain.lean
@@ -31,7 +31,7 @@ import Strata.Util.IO
 import Strata.SimpleAPI
 import Strata.Util.Profile
 import Strata.Util.Json
-import Strata.DDM.BuiltinDialects
+import Strata.DDM.BundledDialects
 import Strata.DDM.Util.String
 import Strata.Languages.Python.PyFactory
 import Strata.Languages.Python.Specs
@@ -133,16 +133,7 @@ def insert (pf : ParsedFlags) (name : String) (value : Option String) : ParsedFl
   { pf with entries := pf.entries.push (name, value) }
 
 def buildDialectFileMap (pflags : ParsedFlags) : IO Strata.DialectFileMap := do
-  let preloaded := Strata.Elab.LoadedDialects.builtin
-    |>.addDialect! Strata.Python.Python
-    |>.addDialect! Strata.Python.Specs.DDM.PythonSpecs
-    |>.addDialect! Strata.Core
-    |>.addDialect! Strata.Boole
-    |>.addDialect! Strata.Laurel.Laurel
-    |>.addDialect! Strata.smtReservedKeywordsDialect
-    |>.addDialect! Strata.SMTCore
-    |>.addDialect! Strata.SMT
-    |>.addDialect! Strata.SMTResponse
+  let preloaded := Strata.Elab.LoadedDialects.ofDialects! Strata.bundledDialects
   let mut sp ← Strata.DialectFileMap.new preloaded
   for path in pflags.getRepeated "include" do
     match ← sp.add path |>.toBaseIO with
diff --git a/StrataTest/DDM/Analysis/ProductivityTest.lean b/StrataTest/DDM/Analysis/ProductivityTest.lean
new file mode 100644
index 0000000000..aa5336576f
--- /dev/null
+++ b/StrataTest/DDM/Analysis/ProductivityTest.lean
@@ -0,0 +1,232 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+meta import Strata.DDM.Analysis.Productivity
+meta import Strata.DDM.BuiltinDialects
+
+namespace Strata.DDM.Productivity.Tests
+
+/-! Hand-built grammar fixtures.  We sidestep the dialect macro and construct
+`Dialect` values directly so we can express deliberately-broken grammars and
+assert exact productivity outcomes.  Everything here is `meta` because DDM
+AST values are only available at elaboration time. -/
+
+private meta def D : DialectName := "Test"
+
+private meta def cat (n : String) : QualifiedIdent := { dialect := D, name := n }
+private meta def syn (n : String) : Decl := .syncat { name := n }
+
+/-- Build an op decl with category arguments only. -/
+private meta def mkOp (name : String) (result : QualifiedIdent)
+    (args : Array QualifiedIdent) : Decl :=
+  let argDecls : ArgDecls := .ofArray <| args.mapIdx fun i a =>
+    { ident := s!"a{i}",
+      kind := .cat (.atom .none a) }
+  let syntaxAtoms : List SyntaxDefAtom :=
+    .str name :: (args.toList.mapIdx fun i _ => .ident i 0)
+  .op {
+    name := name,
+    argDecls := argDecls,
+    category := result,
+    syntaxDef := .ofList syntaxAtoms,
+  }
+
+private meta def mkDialect (decls : Array Decl) : Dialect :=
+  Dialect.ofArray D #[] decls
+
+private meta def mkDialectMap (d : Dialect) : DialectMap :=
+  DialectMap.ofList! [d]
+
+/-! ## Test 1 — single nullary operator is productive. -/
+
+private meta def t1 : Result :=
+  Productivity.check
+    (mkDialectMap (mkDialect #[
+      syn "A",
+      mkOp "aMk" (cat "A") #[]
+    ])) D
+
+#guard t1.isOk
+#guard t1.productive == #[cat "A"]
+#guard t1.unproductive.isEmpty
+
+/-! ## Test 2 — list shape (nil + cons) is productive. -/
+
+private meta def t2 : Result :=
+  Productivity.check
+    (mkDialectMap (mkDialect #[
+      syn "Elem",
+      syn "Lst",
+      mkOp "elemMk" (cat "Elem") #[],
+      mkOp "lstNil"  (cat "Lst")  #[],
+      mkOp "lstCons" (cat "Lst")  #[cat "Elem", cat "Lst"]
+    ])) D
+
+#guard t2.isOk
+#guard t2.productive.size == 2
+#guard t2.unproductive.isEmpty
+
+/-! ## Test 3 — pure self-loop with no base case is unproductive. -/
+
+private meta def t3 : Result :=
+  Productivity.check
+    (mkDialectMap (mkDialect #[
+      syn "Loop",
+      mkOp "loopOnly" (cat "Loop") #[cat "Loop"]
+    ])) D
+
+#guard ! t3.isOk
+#guard t3.productive.isEmpty
+#guard t3.unproductive.size == 1
+#guard t3.unproductive[0]!.category == cat "Loop"
+#guard t3.unproductive[0]!.blockers.size == 1
+#guard t3.unproductive[0]!.blockers[0]!.opName == "loopOnly"
+#guard t3.unproductive[0]!.blockers[0]!.unmetArgCats == #[cat "Loop"]
+
+/-! ## Test 4 — mutual cycle with no base case in the SCC: both unproductive. -/
+
+private meta def t4 : Result :=
+  Productivity.check
+    (mkDialectMap (mkDialect #[
+      syn "A",
+      syn "B",
+      mkOp "aFromB" (cat "A") #[cat "B"],
+      mkOp "bFromA" (cat "B") #[cat "A"]
+    ])) D
+
+#guard ! t4.isOk
+#guard t4.productive.isEmpty
+#guard t4.unproductive.size == 2
+
+/-! ## Test 5 — cascading: B unproductive ⇒ A that depends on B is too,
+even though A is not in any cycle. -/
+
+private meta def t5 : Result :=
+  Productivity.check
+    (mkDialectMap (mkDialect #[
+      syn "A",
+      syn "B",
+      mkOp "aFromB"  (cat "A") #[cat "B"],
+      mkOp "bSelf"   (cat "B") #[cat "B"]
+    ])) D
+
+#guard ! t5.isOk
+#guard t5.productive.isEmpty
+#guard t5.unproductive.size == 2
+
+/-! ## Test 6 — category declared with no operator at all is unproductive,
+and the diagnostic notes the empty blocker list. -/
+
+private meta def t6 : Result :=
+  Productivity.check
+    (mkDialectMap (mkDialect #[ syn "Empty" ])) D
+
+#guard ! t6.isOk
+#guard t6.unproductive.size == 1
+#guard t6.unproductive[0]!.category == cat "Empty"
+#guard t6.unproductive[0]!.blockers.isEmpty
+
+/-! ## Test 7 — framework atoms (`Init.Ident`, …) are trusted, so an
+op taking one of them as an argument is not blocked on it. -/
+
+private meta def initMap : DialectMap :=
+  DialectMap.ofList! [Strata.initDialect]
+
+private meta def t7Dialect : Dialect :=
+  Dialect.ofArray D #[Strata.initDialect.name] #[
+    syn "UsesIdent",
+    mkOp "wrap" (cat "UsesIdent") #[q`Init.Ident]
+  ]
+
+private meta def t7Map : DialectMap :=
+  initMap.insert! t7Dialect
+
+private meta def t7 : Result := Productivity.check t7Map D
+
+#guard t7.isOk
+#guard t7.productive == #[cat "UsesIdent"]
+
+/-! ## Test 8 — nullable container without `@[nonempty]`: inner type's
+productivity is irrelevant (empty list saves us). -/
+
+/-- Op decl with one argument of type `outer (inner)`, optionally `@[nonempty]`. -/
+private meta def mkOpNested
+    (name : String) (result : QualifiedIdent)
+    (outer inner : QualifiedIdent)
+    (nonempty : Bool := false) : Decl :=
+  let nestedCat : SyntaxCat :=
+    { ann := .none, name := outer, args := #[.atom .none inner] }
+  let metadata : Metadata :=
+    if nonempty then
+      Metadata.ofArray #[{ ident := q`StrataDDL.nonempty, args := #[] }]
+    else {}
+  let argDecls : ArgDecls := .ofArray #[
+    { ident := "x", kind := .cat nestedCat, metadata := metadata }
+  ]
+  .op {
+    name := name,
+    argDecls := argDecls,
+    category := result,
+    syntaxDef := .ofList [.str name, .ident 0 0],
+  }
+
+private meta def t8Dialect : Dialect :=
+  Dialect.ofArray D #[Strata.initDialect.name] #[
+    syn "Foo",
+    syn "Bar",
+    mkOpNested "barFromFoos" (cat "Bar")
+      q`Init.CommaSepBy (cat "Foo")
+  ]
+
+private meta def t8Map : DialectMap := initMap.insert! t8Dialect
+
+private meta def t8 : Result := Productivity.check t8Map D
+
+#guard ! t8.isOk
+#guard t8.productive == #[cat "Bar"]
+#guard t8.unproductive.size == 1
+#guard t8.unproductive[0]!.category == cat "Foo"
+
+/-! ## Test 9 — nullable container *with* `@[nonempty]`: inner type's
+productivity becomes mandatory. -/
+
+private meta def t9Dialect : Dialect :=
+  Dialect.ofArray D #[Strata.initDialect.name] #[
+    syn "Foo",
+    syn "Bar",
+    mkOpNested "barFromFoos" (cat "Bar")
+      q`Init.CommaSepBy (cat "Foo") (nonempty := true)
+  ]
+
+private meta def t9Map : DialectMap := initMap.insert! t9Dialect
+
+private meta def t9 : Result := Productivity.check t9Map D
+
+#guard ! t9.isOk
+#guard t9.productive.isEmpty
+#guard t9.unproductive.size == 2
+
+/-! ## Test 10 — `Init.Option` is unconditionally nullable. -/
+
+private meta def t10Dialect : Dialect :=
+  Dialect.ofArray D #[Strata.initDialect.name] #[
+    syn "Foo",
+    syn "Bar",
+    mkOpNested "barFromMaybeFoo" (cat "Bar")
+      q`Init.Option (cat "Foo")
+  ]
+
+private meta def t10Map : DialectMap := initMap.insert! t10Dialect
+
+private meta def t10 : Result := Productivity.check t10Map D
+
+#guard ! t10.isOk
+#guard t10.productive == #[cat "Bar"]
+#guard t10.unproductive.size == 1
+#guard t10.unproductive[0]!.category == cat "Foo"
+
+end Strata.DDM.Productivity.Tests
diff --git a/lakefile.toml b/lakefile.toml
index b59a11c9e8..80d46dd6b8 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -45,3 +45,7 @@ root = "Scripts.ImportStats"
 
 [[lean_exe]]
 name = "DiffTestCore"
+
+[[lean_exe]]
+name = "productivityCheck"
+root = "Scripts.ProductivityCheck"