Cull provably-unsatisfiable constructors

Docs/Results.md

@@ -0,0 +1,69 @@
+# Step-Inlining: Implementation Results
+
+*Results for the implemented pieces of the step-inlining design
+([Lookahead-experiment.md](./Lookahead-experiment.md)). The design doc argues
+what to build and why; this doc records what was built and how it behaves. It
+grows one section per landed piece.*
+
+## 1. Culling provably-dead constructors (`specimen.cullDeadCtors`)
+
+Design reference: "Pass B — cull provably-dead combinations" and the "Cull
+unsatisfiable combinations" bullet of §6 in the design doc.
+
+### The disproofs are dischargeable
+
+Before wiring anything into the deriver, `VaultCullProof.lean` establishes the
+premise: that "this constructor can never fire" is a goal Lean's own automation
+closes. For the all-combinations vault relation it states each constructor's
+premise block verbatim and proves `premises → False`:
+
+- `II` and `RR` — closed by `simp_all` (contradictory `some _ = none`
+  equalities); dead regardless of the input state.
+- `RI` — closed by `simp_all` *once a `none` start is assumed*; dead only from
+  that start.
+
+It also exhibits **satisfying witnesses** for `IR` and for `RI` from a `some (sq _)`
+start — evidence that a sound pass must *keep* those. This is the guardrail: cull
+only on a proof of `False`, never on a failure to find a model.
+
+### The implemented pass
+
+`constructorPremisesUnsat` (`Specimen/DeriveConstrainedProducer.lean`) telescopes
+a constructor, opens its premises into the local context, and tries
+`simp_all` / `omega` / `decide` on a `False` goal under a bounded heartbeat
+budget. `compileInductiveSchedule` skips any constructor it proves dead. The pass
+is behind `set_option specimen.cullDeadCtors true` (default off).
+
+Key semantics — **cull only if never satisfiable, under *any* input state**: the
+goal is assembled from the constructor's own premises, with no assumption about
+the start state. So a constructor that is merely unreachable from a particular
+start (like `RI`) is *not* culled. Sound by construction, and a pure optimization:
+the runtime backtracking that prunes these already exists, so a timeout or
+undecidable goal is harmless (keep the constructor).
+
+### Results
+
+- On the hand-written `VaultUnrolledAll` relation, the derivation trace shows
+  `[cull] dropping recursive constructor …VT.II` and `…VT.RR` — exactly the two
+  internally-contradictory constructors — while `IR` and `RI` are kept. Generation
+  still produces valid traces (`VaultCullTest.lean`: ~220 / 1000 Redeem-bearing,
+  and the stable invariant *non-empty ⟹ contains-Redeem* holds — 0 non-empty
+  traces without a Redeem).
+- On the guarded-dereference relation with a deliberately-dead `DeadHead`
+  constructor (premises force `0 = 1`), only `DeadHead` is dropped; every
+  satisfiable rule is kept (`AttrGuardCullTest.lean`: ~566 / 1000 `drf`-bearing).
+- Flag-off is a no-op: BST / STLC / multi-output / Cedar derivations are
+  unchanged.
+
+Counts fluctuate a few percent run to run (`Gen.run` uses real `IO` randomness);
+the invariants (which constructors are dropped, and non-empty ⟹ target-hit) are
+what's stable.
+
+### Files
+
+- `SpecimenTest/VaultExperiment/VaultCullProof.lean` — the by-hand disproofs and
+  the keep-these witnesses.
+- `SpecimenTest/VaultExperiment/VaultCullTest.lean` — culling on the vault
+  all-combinations relation.
+- `SpecimenTest/AttrGuardExperiment/AttrGuardCullTest.lean` — culling on the
+  guarded-dereference relation (drops a planted dead constructor, keeps the rest).

Specimen/Debug.lean

@@ -64,6 +64,17 @@ register_option specimen.silent : Bool := {
   descr := "suppress all informational derivation output (Try this: suggestions, derive_mutual widgets/text)"
 }
 
+/-- When true, `derive_mutual` attempts to prove each constructor's premises
+    jointly unsatisfiable (entailing `False`) and, when it succeeds, omits that
+    constructor from the derived generator. A constructor is culled only when
+    Lean *proves* it can never fire, using only the constructor's own premises
+    (never assuming anything about the input state) — so this is sound and is a
+    pure optimization over the existing runtime backtracking. -/
+register_option specimen.cullDeadCtors : Bool := {
+  defValue := false
+  descr := "cull constructors whose premises Lean proves unsatisfiable"
+}
+
 /-- Global flag for enabling/disabling debug messages -/
 def globalDebugFlag : Bool := false
 

Specimen/DeriveConstrainedProducer.lean

@@ -14,6 +14,7 @@ import Specimen.Debug
 import Plausible.Arbitrary
 
 import Lean.Elab.Command
+import Lean.Elab.Tactic.Basic
 import ProofWidgets.Component.HtmlDisplay
 
 import Lean.Meta.Basic
@@ -1212,6 +1213,43 @@ def propagateConstraints (components : List (List SpecKey))
         result := result.insert key cs
   return result
 
+/-- Attempt to prove that a constructor's premises are jointly unsatisfiable.
+
+    Telescopes the constructor type into its universally-quantified variables and
+    hypotheses, enters a context holding those hypotheses, and tries to close a
+    `False` goal with an escalating tactic (`simp_all` → `omega` → `decide`) under
+    a bounded heartbeat budget. Returns `true` iff some tactic succeeds — i.e.
+    Lean *proved* the premises entail `False`, so the constructor can never fire.
+
+    Only the constructor's own premises are used; nothing is assumed about the
+    input state. Hence a constructor that is merely unreachable from a particular
+    start (but satisfiable from some state) is NOT reported dead. Sound by
+    construction: a `false` result (no proof / timeout / error) is always safe. -/
+def constructorPremisesUnsat (ctorName : Name) (heartbeats : Nat := 2000) : TermElabM Bool := do
+  let ctorInfo ← getConstInfoCtor ctorName
+  try
+    forallTelescopeReducing ctorInfo.type (cleanupAnnotations := true) fun _vars _concl => do
+      -- Try each tactic in turn; success = the goal is closed (no remaining goals).
+      let tacticStxs : List (TSyntax `tactic) ← do
+        let t1 ← `(tactic| simp_all)
+        let t2 ← `(tactic| omega)
+        let t3 ← `(tactic| decide)
+        pure [t1, t2, t3]
+      let tryClose : TermElabM Bool := do
+        for tac in tacticStxs do
+          -- Fresh `False` goal per attempt (a failed tactic may leave it dirty).
+          let goal ← mkFreshExprMVar (Lean.mkConst ``False)
+          let ok ← (do
+            let remaining ← Lean.Elab.Tactic.run goal.mvarId! (Lean.Elab.Tactic.evalTactic tac)
+            pure remaining.isEmpty) <|> pure false
+          if ok then return true
+        return false
+      -- Bound the effort so a hard/undecidable goal can't stall derivation.
+      withTheReader Core.Context (fun ctx => { ctx with maxHeartbeats := heartbeats * 1000 }) tryClose
+  catch _ =>
+    -- Any elaboration error means we could not prove deadness; keep the ctor.
+    pure false
+
 /-- Compiles an InductiveSchedule from the memo into (def, instance) commands.
     Uses the pre-derived schedules directly (no re-derivation).
     `siblings` is the list of specs in the same mutual block (for rewriting to Source.MutRec). -/
@@ -1283,7 +1321,13 @@ def compileInductiveSchedule (indSched : InductiveSchedule)
     let numRec := indSched.recSchedules.length + numBaseMutual.length
     let numBaseLit := Syntax.mkNumLit (toString numBase)
     let numRecLit := Syntax.mkNumLit (toString numRec)
+    -- Optionally omit constructors whose premises Lean proves unsatisfiable
+    -- (see `constructorPremisesUnsat`). Sound: only proved-dead ctors are dropped.
+    let cullDead := Lean.Option.get (← getOptions) specimen.cullDeadCtors
     for (ctorName, schedule) in indSched.baseSchedules do
+      if cullDead && (← constructorPremisesUnsat ctorName) then
+        trace[plausible.deriving.arbitrary] m!"[cull] dropping base constructor {ctorName}: premises proved unsatisfiable"
+      else
       let (steps, sort) := schedule
       let rewrittenSteps := rewriteSchedule steps
       let isRec := scheduleUsesMutualCall rewrittenSteps
@@ -1293,6 +1337,9 @@ def compileInductiveSchedule (indSched : InductiveSchedule)
       if isRec then recursiveProducers := recursiveProducers.push term
       else nonRecursiveProducers := nonRecursiveProducers.push term
     for (ctorName, schedule) in indSched.recSchedules do
+      if cullDead && (← constructorPremisesUnsat ctorName) then
+        trace[plausible.deriving.arbitrary] m!"[cull] dropping recursive constructor {ctorName}: premises proved unsatisfiable"
+      else
       let (steps, sort) := schedule
       let term ← compileWeightedProducer (rewriteSchedule steps, sort) outputType key.deriveSort
         freshFuelPrimeName freshSizePrimeName key.inductiveName
@@ -1728,7 +1775,13 @@ def deriveConstrainedProducerParts
       let numBaseLit := Syntax.mkNumLit (toString numBaseCtors)
       let numRecLit := Syntax.mkNumLit (toString numRecCtors)
       -- For each constructor: derive a schedule, compile to syntax
+      let cullDead := Lean.Option.get (← getOptions) specimen.cullDeadCtors
       for ctorName in inductiveVal.ctors do
+        -- Optionally cull constructors whose premises Lean proves unsatisfiable.
+        if cullDead then
+          if ← constructorPremisesUnsat ctorName then
+            trace[plausible.deriving.arbitrary] m!"[cull] dropping constructor {ctorName}: premises proved unsatisfiable"
+            continue
         let resultOption ← (UnifyM.runInMetaM
           (getProducerScheduleForInductiveConstructor inductiveName ctorName outputNamesTypesIndices
             freshenedInputNamesExcludingOutput freshUnknowns deriveSort localCtx freshRecFnName)

SpecimenTest.lean

@@ -100,17 +100,21 @@ import SpecimenTest.BoundedBuffer.BackwardGenerator
 import SpecimenTest.BoundedBuffer.BoundedBuffer
 
 -- Multi-step precondition experiments (perfect-square vault): baseline, and the
--- hand-written step-inlined variants (fused pair, all-combinations).
+-- hand-written step-inlined variants (fused pair, all-combinations). CullProof
+-- disproves dead constructors by hand; CullTest exercises `specimen.cullDeadCtors`.
 import SpecimenTest.VaultExperiment.VaultBaseline
 import SpecimenTest.VaultExperiment.VaultFused
 import SpecimenTest.VaultExperiment.VaultUnrolledAll
+import SpecimenTest.VaultExperiment.VaultCullProof
+import SpecimenTest.VaultExperiment.VaultCullTest
 
 -- Tree-structured analog (guarded dereference): baseline and hand-written
 -- inlined variants, inlining across a self-recursive typing relation and the
--- membership relation it depends on.
+-- membership relation it depends on. CullTest exercises `specimen.cullDeadCtors`.
 import SpecimenTest.AttrGuardExperiment.AttrGuardBaseline
 import SpecimenTest.AttrGuardExperiment.AttrGuardFused
 import SpecimenTest.AttrGuardExperiment.AttrGuardUnrolledAll
+import SpecimenTest.AttrGuardExperiment.AttrGuardCullTest
 
 -- Strata Lambda Example: well-typed `LExpr` generator via `HasTypeA`
 import SpecimenTest.StrataLexprGen

SpecimenTest/AttrGuardExperiment/AttrGuardCullTest.lean

@@ -0,0 +1,54 @@
+import SpecimenTest.AttrGuardExperiment.AttrGuardBaseline
+
+open Plausible
+
+namespace AttrGuardCull
+
+/-!
+# Test: culling on the guarded-dereference all-combinations relation
+
+`WT`'s inlined all-combinations rules are all individually satisfiable (each
+`sq k ∈ …` premise can hold from *some* guard set), so the "never satisfiable"
+cull must drop **nothing** here — a good check that the pass is not over-eager.
+We include one deliberately-dead constructor (`DeadHead`, whose premises force
+`0 = 1`) to confirm the pass still fires when a genuine contradiction exists.
+-/
+
+open AttrGuard (Expr Guards sq countDrf)
+
+set_option specimen.multiOutput true
+set_option specimen.autoDeriveDeps true
+set_option match.ignoreUnusedAlts true
+
+inductive WTc : Guards → Expr → Guards → Prop where
+| TLit : ∀ g n, WTc g (Expr.lit n) g
+| TChk : ∀ g c e g', WTc g e g' → WTc g (Expr.chk c e) (c :: g')
+| DrfChkHead : ∀ g k e0 g0,
+    WTc g e0 g0 →
+    WTc g (Expr.drf k (Expr.chk (sq k) e0)) (sq k :: g0)
+-- Genuinely dead: premises force 0 = 1, unsatisfiable regardless of state.
+| DeadHead : ∀ g k e0 g0 (h : (0 : Nat) = 1),
+    WTc g e0 g0 →
+    WTc g (Expr.drf k e0) g0
+
+set_option specimen.cullDeadCtors true
+
+#guard_msgs(drop info, drop warning) in
+derive_mutual
+  (fun g => ∃ e g', WTc g e g')
+
+-- Culling is a pure optimization: generation must still produce valid derefs.
+def countDerefs (numTraces : Nat := 1000) : IO Nat := do
+  let mut withDrf := 0
+  for i in List.range numTraces do
+    let (e, _) ← Gen.run
+      (ArbitrarySizedSuchThat.arbitrarySizedST
+        (fun (e, g') => WTc [] e g') 10) (i + 5)
+    if countDrf e > 0 then withDrf := withDrf + 1
+  return withDrf
+
+#eval do
+  let withDrf ← countDerefs 1000
+  IO.println s!"[cull-on] exprs w/ >=1 drf: {withDrf} / 1000"
+
+end AttrGuardCull

SpecimenTest/VaultExperiment/VaultCullProof.lean

@@ -0,0 +1,114 @@
+import SpecimenTest.VaultExperiment.VaultUnrolledAll
+
+open Plausible
+
+-- Several culling lemmas below state a constructor's premise block verbatim and
+-- prove `False`; `simp_all` often closes them from a subset of the hypotheses,
+-- so the rest are reported unused. That is expected (Lean finds the minimal
+-- contradiction), not a defect.
+set_option linter.unusedVariables false
+
+namespace Vault
+
+/-!
+# Proof-of-concept: culling unsatisfiable step-combinations with Lean itself
+
+`VaultUnrolledAll` emits `b^k` constructors (II, IR, RI, RR) and eliminates the
+infeasible ones only at *runtime*, by backtracking. This file shows the
+elimination can be moved to *derivation time* by asking **Lean** to prove a
+combination's inlined premises are jointly unsatisfiable — the exact
+theorem-proving goal a static-pruning pass would discharge.
+
+Each combination's premise block is a conjunction of equations over the state
+variables (and the linking arithmetic). "This combination is dead" is precisely
+"the premises entail `False`". We phrase that as a lemma and try to close it with
+a general-purpose tactic. If the tactic succeeds, a pruning pass would drop the
+constructor before generating any code for it.
+
+Two flavors of deadness, matching §5 of the write-up:
+  * start-INDEPENDENT: contradictory regardless of the start state (II, RR).
+  * start-DEPENDENT: consistent in isolation, but contradicts a *given* start
+    (RI, once we fix the generator's start state to `none`).
+-/
+
+--------------------------------------------------------------------------------
+-- 1. Start-independent deadness: II and RR are contradictory for ANY start `s`.
+--
+-- The premise block of `II` binds `sa = some t1` and `sa = none`; likewise `RR`
+-- binds `sa = none` and `sa = some (sq k2)`. These are contradictory on their
+-- own. We state exactly the premise conjunction and ask Lean to derive `False`.
+--------------------------------------------------------------------------------
+
+-- II premises, verbatim, with the target `False`.
+theorem II_dead
+    (s sa sb : Vault) (t1 t2 : Nat)
+    (h1 : s = none) (h2 : sa = some t1)
+    (h3 : sa = none) (h4 : sb = some t2) : False := by
+  simp_all
+
+-- RR premises, verbatim.
+theorem RR_dead
+    (s sa sb : Vault) (k1 k2 : Nat)
+    (h1 : s = some (sq k1)) (h2 : sa = none)
+    (h3 : sa = some (sq k2)) (h4 : sb = none) : False := by
+  simp_all
+
+--------------------------------------------------------------------------------
+-- 2. Start-dependent deadness: RI is consistent in isolation, but if the
+-- generator's start state is `none`, RI's `s = some (sq k1)` is impossible.
+--
+-- A pruning pass parameterized by a known start state would discharge this.
+--------------------------------------------------------------------------------
+
+theorem RI_dead_from_none
+    (s sa sb : Vault) (k1 t2 : Nat)
+    (hstart : s = none)                 -- the generator's start state
+    (h1 : s = some (sq k1)) (h2 : sa = none)
+    (h3 : sa = none) (h4 : sb = some t2) : False := by
+  simp_all
+
+-- ...but RI is NOT dead in general: from a `some (sq _)` start it is realizable.
+-- We confirm the premises are satisfiable by exhibiting a witness, so a sound
+-- pruning pass must NOT cull RI unconditionally.
+example : ∃ (s sa sb : Vault) (k1 t2 : Nat),
+    s = some (sq k1) ∧ sa = none ∧ sa = none ∧ sb = some t2 :=
+  ⟨some (sq 3), none, some 7, 3, 7, rfl, rfl, rfl, rfl⟩
+
+--------------------------------------------------------------------------------
+-- 3. The survivor: IR's premises ARE jointly satisfiable (with the forward-
+-- functional link `t = sq k`). A pruning pass must keep IR. We show the premise
+-- block has a model, so no `False` proof exists to cull it.
+--------------------------------------------------------------------------------
+
+example : ∃ (s sa sb : Vault) (t k : Nat),
+    s = none ∧ sa = some t ∧ sa = some (sq k) ∧ sb = none :=
+  -- choose k = 4, t = sq 4 = 16, so `sa = some 16 = some (sq 4)` holds.
+  ⟨none, some (sq 4), none, sq 4, 4, rfl, rfl, rfl, rfl⟩
+
+/-!
+## What this shows
+
+The culling decision for a step-combination is a **closed first-order goal over
+the inlined premises**, and the goals arising here are exactly the kind Lean's
+automation closes without help:
+
+  * `II_dead`, `RR_dead`  — `simp_all` (contradictory equalities on an inductive
+    datatype: `some _ = none`).
+  * `RI_dead_from_none`   — same, once a start state is assumed.
+
+So a derivation-time pruning pass could, for each of the `b^k` candidate
+constructors, assemble its premise conjunction and invoke a tactic
+(`simp_all` / `omega` / `decide`, escalating as needed) to *try* to prove
+`premises → False`:
+
+  * **proof found**  → the combination is dead; emit no generator for it.
+  * **no proof / countermodel** → keep it (as IR and the satisfiable RI witness
+    show, we must not cull these).
+
+This is sound by construction: we only drop a constructor when Lean has *proved*
+it can never fire. It leans on Lean-as-prover exactly where §5 wanted, and it
+degrades gracefully — an undecidable or timed-out goal simply means "keep the
+constructor", falling back to today's runtime backtracking for that one.
+-/
+
+end Vault