diff --git a/Docs/Generator-config.md b/Docs/Generator-config.md
new file mode 100644
index 0000000..e9d0d8e
--- /dev/null
+++ b/Docs/Generator-config.md
@@ -0,0 +1,236 @@
+# Selecting and Configuring Generators
+
+It is rarely the case that a generator for values of a particular type works for every application. Maybe booleans are the only exception! Thus an important question is: For a particular PBT application, how do we define, select, and configure the right generator? In this document we consider how to control the size of inputs, and how to select sub generators. We discuss some other issues at the end.
+
+## Sizing inputs
+
+A common configuration paramater for generators is a preferred _size_. Intuitively, small inputs are preferred for their faster generation times, faster running times, and easier debugging when faults are found. Large inputs might be better when bugs require executing many distinct code paths, and one large but diverse input might be effectively the same as several small ones. Usually the choice is left up to the user, who best knows their application. But how should that choice be expressed? There are two common knobs: Explicit upper bounds, and probabilistic bounds.
+
+### Explicit bounds
+
+The code examples here and throughout are written in [Basalt](https://github.com/hgoldstein95/basalt/), anticipating that Specimen will eventually target it. 
+
+Here is a generator in which the list length is specified, and chosen uniformly at random.
+
+```
+def genListNatMax [Gen G] (max : Nat) : G (List Nat) := do
+  let size ← RandomChoice.choose 0 max (by omega)
+  go size.down
+where
+  go : (size : Nat) → G (List Nat)
+    | 0 => pure []
+    | Nat.succ size' => do
+        let x ← Nat.arbitrary 
+        let xs ← go size'
+        return x :: xs
+```
+
+Lists with max := 10.
+
+[0, 1, 0, 0]
+[3, 1, 0, 1, 3, 1, 0]
+[0]
+[1, 2, 0, 0, 0, 1, 0, 0, 3, 4]
+[2, 0, 1, 1, 4, 0, 0, 2, 1]
+[0, 1, 2, 4, 3, 7, 0, 0, 3, 1]
+[2, 1, 0, 0, 1, 0, 0, 0, 1]
+[3, 2, 2, 0, 4, 1, 1]
+[1, 0, 1]
+[1, 3, 0, 0, 0, 6, 1]
+[0, 2]
+[4, 1, 0, 1, 0]
+[1, 1, 1, 1, 0, 0]
+[1, 0]
+[1, 3, 0, 1, 0, 0, 3, 1, 1]
+[0, 0, 1, 2, 0, 1, 0]
+[0, 0, 1, 0, 0]
+[2, 0, 0, 0, 0, 1, 1, 0, 1, 0]
+[0, 2]
+[0, 0, 0, 2, 0]
+
+### Probabilistic bounding
+
+Here is an example in which there is no upper bound on a list's length, but the probability distribution of length controlled by a given bias. 
+
+```
+def genListNatProb [Gen G] (bias: Rat) : G (List Nat) := do
+  if ← RandomChoice.coin bias then
+    pure []
+  else do
+    let x ← Nat.arbitrary
+    let xs ← genListNatProb bias
+    return x :: xs
+partial_fixpoint
+```
+
+Lists with bias to 1/4.
+
+[2]
+[2, 1, 1, 0, 1]
+[2]
+[]
+[1]
+[]
+[0, 0, 0]
+[2]
+[]
+[2, 0, 1, 2, 1, 5]
+[1, 2, 0, 3, 0, 1]
+[1, 2, 0, 1]
+[3, 0, 0, 3, 2, 0, 2]
+[2]
+[4]
+[1, 1, 1, 3, 0, 1]
+[0, 0, 0]
+[0, 0]
+[4, 2, 0, 0, 1, 0, 2, 0, 0, 0, 0, 1, 1, 9, 0, 0, 2]
+[1, 1, 1, 0, 1, 4]
+
+### Combination
+
+We can create an upper bound on length, while using a bias to control the distribution.
+
+```
+def genListNatProbMax [Gen G] (max : Nat) (bias: Rat) : G (List Nat) := do
+  match max with
+  | Nat.zero => pure []
+  | Nat.succ max' =>
+      if ← RandomChoice.coin bias then
+        pure []
+      else do
+        let x ← Nat.arbitrary
+        let xs ← genListNatProbMax max' bias
+        return x :: xs
+```
+
+Lists with bias of 1/4 and a max length of 10
+
+[0, 0, 0]
+[0, 3, 1]
+[1, 1, 1]
+[2, 1, 0]
+[0]
+[0, 1, 0, 4, 0, 0, 0, 4, 0, 0]
+[1, 1, 0, 0, 0, 0, 1]
+[0]
+[1]
+[1, 2, 0, 1, 4, 1]
+[2, 0]
+[]
+[4, 0, 0]
+[4, 0, 0, 0]
+[0, 2, 0, 1, 0, 1, 1]
+[3, 0, 0, 0, 0, 1, 3, 0]
+[0]
+[]
+[2, 2, 2]
+[1, 0, 3, 4]
+
+## Calling sub generators
+
+In the examples above we call `Nat.arbitrary` for the elements of a list. This uses a 50/50 probability bound on generating numbers. What if we wanted to use a different generator for Nats, how would we specify it? 
+
+Embedded in these examples is a default answer to another question, which is how to specify the size of sub-generated values. We assume the size given to the outer generator (here: `max`) is given to the sub-generators too. We discuss this choice separately in the next section.
+
+### Sub-generator: Direct call
+
+The easiest approach is to just hard-code a call to the generator.
+
+```
+def genNat [Gen G] (max : Nat) : G Nat :=
+  ULift.down <$> RandomChoice.choose 0 max (by omega)
+  
+def genListNatMaxMax [Gen G] (max : Nat) : G (List Nat) := do
+  let size ← RandomChoice.choose 0 max (by omega)
+  go size.down
+where
+  go : (size : Nat) → G (List Nat)
+    | 0 => pure []
+    | Nat.succ size' => do
+        let x ← genNat max
+        let xs ← go size'
+        return x :: xs
+```
+
+Doing this requires knowing the name of the generator you want to call (e.g., `genNat`) which may not be convenient. It also hurts polymorphism: A list generator that calls `genNat` can only generate lists of natural numbers, even though the structure of the generator shouldn’t change for other kinds of lists.
+
+### Sub-generator: Typeclass
+
+To solve the problems of locating generators and making them polymorphic, QuickChick selects nested generators by using typeclass resolution.
+
+```
+class Arb (T : Type) (G : Type → Type) [Gen G] where
+  arb : Nat → G T
+
+instance [Gen G] : Arb Nat G where
+  arb := genNat
+  
+def genListNatMaxMax' [Gen G] [Arb T G] (max : Nat) : G (List T) := do
+  let size ← RandomChoice.choose 0 max (by omega)
+  go size.down
+where
+  go : (size : Nat) → G (List T)
+    | 0 => pure []
+    | Nat.succ size' => do
+        let x ← Arb.arb max
+        let xs ← go size'
+        return x :: xs
+```
+
+Here, `genListNatMaxMax'` calls `Arb.arb max` rather than `genNat max`, with the benefit that it works for type `T` for which an `Arb T G` instance exists. 
+
+Using typeclasses means we must create a uniform structure for generators, e.g., that they take a `max` parameter. This is potentially limiting — this structure needs to be the least common denominator for generators we might call. There is also an issue that while we have a level of indirection, there is still only one possible generator per type.
+
+### Sub-generator: Parameter
+
+We could pass the sub-generator to the generator, rather than calling it directly or resolving via typeclass:
+
+```
+def genListNatMaxMax'' [Gen G] (g: Nat → G T) (max : Nat) : G (List T) := do
+  let size ← RandomChoice.choose 0 max (by omega)
+  go size.down
+where
+  go : (size : Nat) → G (List T)
+    | 0 => pure []
+    | Nat.succ size' => do
+        let x ← g max
+        let xs ← go size'
+        return x :: xs
+```
+
+The drawback with this approach is that the top-most generator must explicitly specify all of the generators of the generators it might call, transitively. But this also affords greater flexibility for the user. For example, we could default to typeclass resolution but allow specific parameters as desired.
+
+```
+def genListNatMaxMax'' [Gen G] [Arb T G] (max : Nat) (g : Nat → G T := Arb.arb) : G (List T) := do ...
+```
+
+## Managing the size and distribution of sub-generated values
+
+However we decide which sub generator to call, what configuration parameters should we pass to that call (and indeed, to the parent call originally) to control the size and distribution of generated values?
+
+### Controlling size
+
+In the examples above, we pass along `max` to the list generator as the initial size. Its value is decremented while generating the list, but the unchanged `max` is passed to calls to the list-element generator. This matches the approach of Specimen, where the outer (global) size is called `initSize` and the inner (local) one is called `size`. In Specimen, the inner one bounds termination, and the outer one specifies policy.
+
+While this approach is not bad, it has several issues:
+
+1. The same size may not make sense for every generator. For example, I might want short lists containing potentially large numbers in some cases.
+
+2. The same size may not make sense for every instance of the same generator. For example, if I am generating pairs of numbers and trees of numbers, I might want numbers in the pair to be potentially large but those in the trees to be mostly small.
+
+3. Having to choose the size at all may be difficult: Users may not wish to guess what size makes sense for their application, and would prefer the system dynamically discover a reasonable size.
+
+Note that the use of size to ensure termination (as a kind of "fuel") is not strictly necessary. Basalt's `partial_fixpoint` eliminates the need for fuel; see `Docs/Specimen-Basalt-port.md` for more about this. Thus we should really be thinking of sizing with respect to effectiveness.
+
+### Controlling the distribution
+
+The size parameter is capturing one aspect of the *distribution* of values that a generator produces. 
+
+The bias parameter mentioned in the **Probabilistic bounding** section makes very large items unlikely, but not impossible. How can we adjust the distribution? The paper [Tuning Random Generators](https://arxiv.org/pdf/2508.14394) looks at using ML inference to do this. It basically takes generators in which sub-generators are inlined in the parent and then does ML inference to tune bias parameters against an objective function. The main objective function of interest is "maximum entropy" up to a size bound for the overall objects. This seems useful!
+
+One of the benefits of [Tyche](https://andrewhead.info/assets/pdf/tyche.pdf) is that it allows you to visualize the distribution of generated inputs from your generator, according to metrics you care about. Using that visualization you can tune the generator by hand, or ask an LLM to do it (or help). There are some simple failure modes that Tyche can quickly identify:
+
+1. Generating too many constants or default values
+2. Generating too many duplicate values
+4. Generating too many invalid (discarded) values
+3. Not generating certain kinds of inputs very often (e.g., abstract syntax trees with calls to multi-argument functions when generating lambda-calculus terms)
diff --git a/Docs/Specimen-Basalt-port.md b/Docs/Specimen-Basalt-port.md
new file mode 100644
index 0000000..10c9500
--- /dev/null
+++ b/Docs/Specimen-Basalt-port.md
@@ -0,0 +1,811 @@
+# Bridging Specimen and Basalt via `BacktrackGen`
+
+## Executive Summary
+
+**Goal.** Make Specimen-derived generators polymorphic over Basalt's `Gen` class so they can be both *executed* (via `Plausible.Gen`) and *proved correct* (at `SetGen.Set`).
+
+**Dependency change.** Today Specimen depends only on Plausible; after this work it will also depend on Basalt, using Basalt's `Gen` abstraction as the target monad for emitted generators.
+
+**Four problems to solve:**
+
+1. **Backtracking.** Basalt's `Gen` has no exceptions. We introduce `BacktrackGen G α` (a newtype over `G (Option α)`) and a `backtrack` combinator with retry semantics.
+2. **Sub-generator resolution.** Plausible's `Arbitrary`/`ArbitrarySizedSuchThat` wrap `Plausible.Gen` specifically. We introduce `GenFor α P` and `BacktrackGenFor α P` — Basalt-polymorphic typeclasses for sub-generator lookup.
+3. **Checkers.** `DecOpt` currently returns `Except GenError Bool`. We redefine it to return `BacktrackGen G Bool`, making it polymorphic over `G`.
+4. **Unconstrained generators.** `derive Arbitrary` uses Plausible-specific combinators. We emit Basalt-polymorphic generators using a `frequency` combinator and `GenFor` instances.
+
+**Plan of work:**
+
+- *Phase 1* — Emit Basalt-compatible generators that execute via Plausible. All existing tests pass; the `plausible` tactic works end-to-end.
+- *Phase 2* — Emit `BacktrackGenCorrect` certificates (soundness + completeness proofs at `SetGen.Set`) alongside every derived generator.
+
+**What does NOT change:** User-facing syntax (`derive_generator`, `derive Arbitrary`), enumerators (future work), and almost-sure termination proofs (future work).
+
+A glossary of terms appears at the end, for quick reference.
+
+**Experiments.** The design in this document was validated by the experiments in `SpecimenTest/BasaltPort/`: `BridgeBacktrackMockup.lean` demonstrates all three bridging mechanisms (backtracking, sub-generators, and checkers) in a single example, while `BridgeBenchmark.lean` provides performance comparisons between legacy and bridge-based generators.
+
+---
+
+## 1. Status Quo and Goal
+
+### The three frameworks
+
+**Plausible** is a property-based testing library for Lean. Its `Gen` monad is a stack of monad transformers:
+```
+abbrev Gen (α : Type u) := RandT (ReaderT (ULift Nat) (Except GenError)) α
+```
+It provides randomness, a size parameter, and exception-based failure. The `plausible` tactic finds `Testable` instances (which bottom out at `Arbitrary` instances) via typeclass synthesis and executes them.
+
+**Specimen** derives generators for values satisfying inductive relations, built on top of Plausible. It emits `Plausible.Gen α` terms that use `throw`/`tryCatch` for backtracking: when a branch can't satisfy constraints, it throws a `GenError`, and the `backtrack` combinator catches it and retries another branch. Key typeclasses:
+- `ArbitrarySizedSuchThat α P` — a sized generator (`Nat → Gen α`) for values satisfying `P`
+- `ArbitrarySuchThat α P` — the unsized wrapper (via `Gen.sized`)
+
+**[Basalt](https://github.com/hgoldstein95/basalt/)** defines a `Gen` typeclass abstracting the capabilities needed by a generator:
+```lean
+class Gen (g : Type u → Type v) where
+  instInhabited : ∀ α, Inhabited (g α)
+  instMonad : Monad g
+  instRandomChoice : RandomChoice g
+  instCCPO : ∀ α, CCPO (g α)
+  instMonoBind : MonoBind g
+```
+Basalt provides multiple instances: `SetGen.Set` (for soundness/completeness proofs), `SPMF` (for termination/distribution proofs), `SPMF.Cost` (for cost bounds), and `Plausible.Gen` (for execution, via `Basalt/PlausibleGen.lean`). A generator written polymorphically as `[Gen G] → G α` can be proved correct at `SetGen`/`SPMF` and executed at `Plausible.Gen`.
+
+Basalt also defines correctness classes for individual generator terms:
+- `IsSoundAndComplete (g : SPMF α) (P : α → Prop)` — the generator's support equals `{a | P a}`
+- `IsAlmostSurelyTerminating (g : SPMF α)` — the generator's mass sums to 1
+- `IsCostBounded (g : SPMF.Cost α) (c : α → Nat)` — the generator makes at most `c a` choices to produce `a`
+- `LawfulGenerator (g : ∀ {G} [Gen G], G α) (P) (c)` — combines all three
+
+### The goal
+
+We want Specimen-derived generators to be **polymorphic over Basalt's `Gen` class** so they can be:
+- **Specified as today.** The `derive_generator (fun τ => ∃ e, HasType e τ)` command syntax remains unchanged. The difference is purely in what code gets emitted.
+- **Executed** via `Plausible.Gen` (as today)
+- **Proved sound/complete** at `SetGen.Set`
+
+### Example
+
+We use the following small typed language throughout to illustrate changes. It exercises all three mechanisms: backtracking (multiple constructors per type), checkers (`isPos` has a decidable guard `n ≠ 0`), and cross-generator composition (`WellFormed` calls `HasType`).
+
+```lean
+inductive Ty | nat | bool
+
+inductive Expr
+  | lit (n : Nat)
+  | isPos (n : Nat)
+  | add (l r : Expr)
+
+inductive HasType : Expr → Ty → Prop
+  | lit (n) : HasType (.lit n) .nat
+  | isPos (n) : n ≠ 0 → HasType (.isPos n) .bool
+  | add (l r) : HasType l .nat → HasType r .nat → HasType (.add l r) .nat
+
+inductive Prog
+  | expr (e : Expr)
+  | both (e1 e2 : Expr)
+
+inductive WellFormed : Prog → Prop
+  | expr (e τ) : HasType e τ → WellFormed (.expr e)
+  | both (e1 e2 τ) : HasType e1 τ → HasType e2 τ → WellFormed (.both e1 e2)
+```
+
+To get generators, a user invokes Specimen (this syntax will not change):
+
+```lean
+derive_generator (fun τ => ∃ e, HasType e τ)
+derive_generator (fun _ => ∃ p, WellFormed p)
+```
+
+### What Specimen emits today
+
+For the `HasType` relation, Specimen produces:
+
+```lean
+instance : ArbitrarySizedSuchThat Expr (fun e => HasType e τ) where
+  arbitrarySizedST :=
+    let rec aux_arb (initSize : Nat) (size : Nat) (τ : Ty) : Plausible.Gen Expr :=
+      match size with
+      | Nat.zero =>
+        GeneratorCombinators.backtrack
+          [(1, match τ with
+            | Ty.nat => do
+              let n ← Arbitrary.arbitrary
+              return Expr.lit n
+            | _ => MonadExcept.throw Gen.genericFailure),
+           (1, match τ with
+            | Ty.bool => do
+              let n ← Arbitrary.arbitrary
+              match @DecOpt.decOpt (¬(n = 0)) _ initSize with
+              | Except.ok true => return Expr.isPos n
+              | _ => MonadExcept.throw Gen.genericFailure
+            | _ => MonadExcept.throw Gen.genericFailure)]
+      | Nat.succ size' =>
+        GeneratorCombinators.backtrack
+          [(1, match τ with
+            | Ty.nat => do
+              let n ← Arbitrary.arbitrary
+              return Expr.lit n
+            | _ => MonadExcept.throw Gen.genericFailure),
+           (1, match τ with
+            | Ty.bool => do
+              let n ← Arbitrary.arbitrary
+              match @DecOpt.decOpt (¬(n = 0)) _ initSize with
+              | Except.ok true => return Expr.isPos n
+              | _ => MonadExcept.throw Gen.genericFailure
+            | _ => MonadExcept.throw Gen.genericFailure),
+           (Nat.succ size', match τ with
+            | Ty.nat => do
+              let l ← aux_arb initSize size' Ty.nat
+              let r ← aux_arb initSize size' Ty.nat
+              return Expr.add l r
+            | _ => MonadExcept.throw Gen.genericFailure)]
+    fun size => aux_arb size size τ
+```
+
+For `WellFormed`, Specimen produces a generator that calls the `HasType` generator **via typeclass resolution** (`ArbitrarySizedSuchThat.arbitrarySizedST`):
+
+```lean
+instance : ArbitrarySizedSuchThat Prog (fun p => WellFormed p) where
+  arbitrarySizedST :=
+    let rec aux_arb (initSize : Nat) (size : Nat) : Plausible.Gen Prog :=
+      match size with
+      | Nat.zero =>
+        GeneratorCombinators.backtrack
+          [(1, do let τ ← Arbitrary.arbitrary
+                  let e ← @ArbitrarySizedSuchThat.arbitrarySizedST _ (fun e => HasType e τ) _ initSize
+                  return Prog.expr e),
+           (1, do let τ ← Arbitrary.arbitrary
+                  let e1 ← @ArbitrarySizedSuchThat.arbitrarySizedST _ (fun e => HasType e τ) _ initSize
+                  let e2 ← @ArbitrarySizedSuchThat.arbitrarySizedST _ (fun e => HasType e τ) _ initSize
+                  return Prog.both e1 e2)]
+      | Nat.succ size' =>
+        GeneratorCombinators.backtrack
+          [(1, do let τ ← Arbitrary.arbitrary
+                  let e ← @ArbitrarySizedSuchThat.arbitrarySizedST _ (fun e => HasType e τ) _ initSize
+                  return Prog.expr e),
+           (1, do let τ ← Arbitrary.arbitrary
+                  let e1 ← @ArbitrarySizedSuchThat.arbitrarySizedST _ (fun e => HasType e τ) _ initSize
+                  let e2 ← @ArbitrarySizedSuchThat.arbitrarySizedST _ (fun e => HasType e τ) _ initSize
+                  return Prog.both e1 e2)]
+    fun size => aux_arb size size
+```
+
+These generators work for execution but cannot be proved correct. To bridge them to Basalt, we need to solve the four problems listed in the executive summary.
+
+## 2. Solving Problem 1: `BacktrackGen`
+
+We introduce a newtype that wraps `G (Option α)` to represent generators that may fail locally:
+
+```lean
+/-- A backtracking generator: wraps G (Option α) where none = local failure, some = success. -/
+structure BacktrackGen (G : Type u → Type v) (α : Type u) where
+  run : G (Option α)
+```
+
+The `Option` layer is *inside* the generator monad `G`, meaning failure is a **value** that the generator successfully produces (as opposed to ⊥/`default`, which represents divergence). This lets other generators observe and react to failure — enabling retry.
+
+```lean
+instance [Gen G] : Monad (BacktrackGen G) where
+  pure a := ⟨pure (some a)⟩
+  bind x f := ⟨do
+    match ← x.run with
+    | some a => (f a).run
+    | none => pure none⟩
+```
+
+### The `backtrack` combinator
+
+```lean
+def backtrack [Gen G] (gs : List (Nat × (Unit → BacktrackGen G α))) : BacktrackGen G α :=
+  ⟨go gs.length (sumWeights gs) gs⟩
+where
+  go : Nat → Nat → List (Nat × (Unit → BacktrackGen G α)) → G (Option α)
+  | _, _, [] => pure none
+  | 0, _, _ => pure none
+  | fuel + 1, total, gs@(_ :: _) => do
+    let n ← RandomChoice.choose 0 (total - 1) (by omega)
+    let (k, g, gs') := pickDrop gs n.down
+    match ← (g ()).run with
+    | some a => pure (some a)
+    | none => go fuel (total - k) gs'
+```
+
+Operational semantics: pick a branch randomly (weighted), try it; if it returns `none`, remove it from the pool and retry with decremented fuel. Termination is structural on fuel (starts at `gs.length`).
+
+### Helpers
+
+```lean
+/-- Lift a non-failing G α into BacktrackGen G α. -/
+def BacktrackGen.liftGen [Gen G] (g : G α) : BacktrackGen G α :=
+  ⟨do let a ← g; pure (some a)⟩
+
+/-- Signal local failure (backtrack). -/
+def BacktrackGen.fail [Gen G] : BacktrackGen G α :=
+  ⟨pure none⟩
+```
+
+### Boundary: unwrapping `BacktrackGen`
+
+At the outermost level — where a generator must produce a value for Plausible's testing machinery — we collapse the `Option`:
+
+```lean
+def BacktrackGen.toGen [Gen G] [Inhabited α] (g : BacktrackGen G α) : G α := do
+  match ← g.run with
+  | some a => pure a
+  | none => pure default  -- ⊥ (divergence)
+
+def BacktrackGen.toPlausibleGen (g : BacktrackGen Plausible.Gen α) : Plausible.Gen α := do
+  match ← g.run with
+  | some a => pure a
+  | none => throw (.genError "backtracking exhausted")
+```
+
+> **Design rationale** (why a newtype, interpretations across Basalt instances): see Appendix A.
+
+## 3. Solving Problem 2: Sub-generator Resolution
+
+Today, Specimen resolves sub-generators via Plausible's `Arbitrary` (for unconstrained types) and `ArbitrarySizedSuchThat` (for constrained types). These wrap `Plausible.Gen` specifically — they cannot be used inside a polymorphic `G`.
+
+### Design: `GenFor` and `BacktrackGenFor`
+
+```lean
+/-- A non-backtracking generator for type α whose outputs satisfy P.
+    Always succeeds. Analogous to Plausible's Arbitrary, but polymorphic over Gen G. -/
+class GenFor (α : Type) (P : α → Prop) where
+  gen : ∀ {G : Type → Type} [Gen G], G α
+
+/-- A backtracking generator for type α whose successful outputs satisfy P.
+    May fail. Takes a Nat fuel parameter for structural termination.
+    Analogous to Specimen's ArbitrarySizedSuchThat, but polymorphic over Gen G. -/
+class BacktrackGenFor (α : Type) (P : α → Prop) where
+  gen : ∀ {G : Type → Type} [Gen G], Nat → BacktrackGen G α
+```
+
+The calling convention:
+- `GenFor` → always succeeds, caller uses `BacktrackGen.liftGen` to enter `BacktrackGen`
+- `BacktrackGenFor` → may fail, caller binds directly in `BacktrackGen` (failure propagates via `bind`)
+
+### Standard `GenFor` instances
+
+```lean
+instance : GenFor Nat (fun _ => True) where
+  gen := Nat.arbitrary  -- Basalt's polymorphic Nat generator
+
+instance : GenFor Bool (fun _ => True) where
+  gen := Bool.arbitrary
+```
+
+Bridge to Plausible:
+
+```lean
+instance [GenFor α (fun _ => True)] : Arbitrary α where
+  arbitrary := GenFor.gen  -- specializes at G := Plausible.Gen
+```
+
+## 4. Solving Problem 3: Checkers (`DecOpt`)
+
+Today's `DecOpt` returns `Except GenError Bool` — a Plausible-specific type. We redefine it to return `BacktrackGen G Bool`:
+
+```lean
+class DecOpt (P : Prop) where
+  decOpt : ∀ {G : Type → Type} [Gen G], Nat → BacktrackGen G Bool
+```
+
+The three-valued semantics map to `G (Option Bool)`:
+- `some true` → P holds
+- `some false` → P doesn't hold
+- `none` → can't decide (out of fuel) → causes backtracking
+
+### Bridge from `Decidable`
+
+```lean
+instance [Decidable P] : DecOpt P where
+  decOpt _ := pure (decide P)
+```
+
+> **Interpretations** (how `DecOpt` behaves at each Basalt instance): see Appendix D.
+
+## 5. The Generated Code (Running Example)
+
+Applying `BacktrackGen` (Section 2), `GenFor` / `BacktrackGenFor` (Section 3), and `DecOpt` (Section 4) to the example, the generated code becomes:
+
+```lean
+def genHasType [Gen G] [GenFor Nat (fun _ => True)]
+    (initSize : Nat) (τ : Ty) : (size : Nat) → BacktrackGen G Expr
+  | 0 => backtrack [
+      (1, fun () => match τ with
+        | .nat => do
+            let n ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Nat)
+            pure (Expr.lit n)
+        | _ => BacktrackGen.fail),
+      (1, fun () => match τ with
+        | .bool => do
+            let n ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Nat)
+            match ← DecOpt.decOpt (P := ¬(n = 0)) initSize with
+            | true => pure (Expr.isPos n)
+            | false => BacktrackGen.fail
+        | _ => BacktrackGen.fail)]
+  | size + 1 => backtrack [
+      (1, fun () => match τ with
+        | .nat => do
+            let n ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Nat)
+            pure (Expr.lit n)
+        | _ => BacktrackGen.fail),
+      (1, fun () => match τ with
+        | .bool => do
+            let n ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Nat)
+            match ← DecOpt.decOpt (P := ¬(n = 0)) initSize with
+            | true => pure (Expr.isPos n)
+            | false => BacktrackGen.fail
+        | _ => BacktrackGen.fail),
+      (size + 1, fun () => match τ with
+        | .nat => do
+            let l ← genHasType initSize .nat size
+            let r ← genHasType initSize .nat size
+            pure (Expr.add l r)
+        | _ => BacktrackGen.fail)]
+
+instance [GenFor Nat (fun _ => True)]
+    : ∀ τ, BacktrackGenFor Expr (fun e => HasType e τ) :=
+  fun τ => ⟨fun {_} [_] size => genHasType size τ size⟩
+```
+
+And `genWellFormed` calls the `HasType` generator via `BacktrackGenFor` typeclass resolution:
+
+```lean
+def genWellFormed [Gen G] [GenFor Nat (fun _ => True)] [GenFor Ty (fun _ => True)]
+    [∀ τ, BacktrackGenFor Expr (fun e => HasType e τ)]
+    (initSize : Nat) : (size : Nat) → BacktrackGen G Prog
+  | 0 => backtrack [
+      (1, fun () => do
+        let τ ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Ty)
+        let e ← BacktrackGenFor.gen (P := fun e => HasType e τ) initSize
+        pure (Prog.expr e)),
+      (1, fun () => do
+        let τ ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Ty)
+        let e1 ← BacktrackGenFor.gen (P := fun e => HasType e τ) initSize
+        let e2 ← BacktrackGenFor.gen (P := fun e => HasType e τ) initSize
+        pure (Prog.both e1 e2))]
+  | size + 1 => backtrack [
+      (1, fun () => do
+        let τ ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Ty)
+        let e ← BacktrackGenFor.gen (P := fun e => HasType e τ) initSize
+        pure (Prog.expr e)),
+      (1, fun () => do
+        let τ ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Ty)
+        let e1 ← BacktrackGenFor.gen (P := fun e => HasType e τ) initSize
+        let e2 ← BacktrackGenFor.gen (P := fun e => HasType e τ) initSize
+        pure (Prog.both e1 e2))]
+```
+
+### Key transformations from Specimen's output today 
+
+| Today | After migration |
+|---|---|
+| `MonadExcept.throw Gen.genericFailure` | `BacktrackGen.fail` |
+| `return value` | `pure value` (BacktrackGen Monad wraps in `some`) |
+| `Arbitrary.arbitrary` | `BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G α)` |
+| `ArbitrarySizedSuchThat.arbitrarySizedST (fun e => P e) initSize` | `BacktrackGenFor.gen (P := fun e => P e) initSize` |
+| `match @DecOpt.decOpt P _ fuel with \| Except.ok true => ... \| _ => throw` | `match ← DecOpt.decOpt (P := P) fuel with \| true => ... \| false => BacktrackGen.fail` |
+| Return type: `Plausible.Gen α` | `BacktrackGen G α` |
+| Recursive calls via `let rec aux_arb` | Direct structural recursion on `size : Nat` |
+
+The `initSize`/`size` split remains: `size` is structurally decremented for termination; `initSize` is passed unchanged to sub-generators via `BacktrackGenFor.gen ... initSize`.
+
+### Executing via Plausible
+
+```lean
+instance : ArbitrarySizedSuchThat Expr (HasType · τ) where
+  arbitrarySizedST size := BacktrackGen.toPlausibleGen (genHasType size τ size)
+
+instance : ArbitrarySizedSuchThat Prog WellFormed where
+  arbitrarySizedST size := BacktrackGen.toPlausibleGen (genWellFormed size size)
+```
+
+The `plausible` tactic finds these instances via the existing `ArbitrarySizedSuchThat → ArbitrarySuchThat → Arbitrary` chain and executes them normally.
+
+## 6. Solving Problem 4: Unconstrained Generators (`derive Arbitrary`)
+
+### The problem
+
+Specimen's `derive Arbitrary` emits generators using `Gen.frequency` / `Gen.oneOfWithDefault` and `Arbitrary.arbitrary` — all Plausible-specific. Unlike constrained generators, unconstrained generators never backtrack (always succeed), so no `BacktrackGen` is needed — just the `frequency` combinator and `GenFor`.
+
+### The `frequency` combinator
+
+```lean
+/-- Weighted random selection without retry. For non-backtracking generators.
+    Picks a generator from `gs` by weight interval (matching GeneratorCombinators.frequency).
+    If `gs` is empty, the `default` generator is returned. -/
+def frequency [Gen G] (default : G α) (gs : List (Nat × (Unit → G α))) : G α :=
+  match gs with
+  | [] => default
+  | _ => do
+    let total := sumWeights gs
+    let n ← RandomChoice.choose 0 (total - 1) (by omega)
+    (pick (fun () => default) gs n.down).snd ()
+```
+
+### Example: what changes
+
+For a type like `Tree α`, today's output vs the migrated version:
+
+**Today:**
+```lean
+instance [Arbitrary α] : ArbitraryFueled (Tree α) where
+  arbitraryFueled :=
+    let rec aux_arb (fuel : Nat) : Plausible.Gen (Tree α) := ...
+    fun fuel => aux_arb fuel
+```
+
+**After migration:**
+```lean
+def Tree.gen [Gen G] [GenFor α (fun _ => True)] : (fuel : Nat) → G (Tree α)
+  | 0 => frequency (pure Tree.leaf) [
+      (1, fun () => pure Tree.leaf)]
+  | fuel + 1 => frequency (pure Tree.leaf) [
+      (1, fun () => pure Tree.leaf),
+      (fuel + 1, fun () => do
+        let left ← Tree.gen fuel
+        let val ← GenFor.gen (P := fun _ => True)
+        let right ← Tree.gen fuel
+        pure (Tree.node left val right))]
+
+instance [GenFor α (fun _ => True)] : GenFor (Tree α) (fun _ => True) where
+  gen := Gen.sized Tree.gen
+```
+
+### Key transformations
+
+| Today | After migration |
+|---|---|
+| `Gen.oneOfWithDefault default [gs]` / `Gen.frequency default [(w, g), ...]` | `frequency default [(w, fun () => g), ...]` |
+| `Arbitrary.arbitrary` | `GenFor.gen (P := fun _ => True)` |
+| Recursive calls: `aux_arb fuel'` | `Tree.gen fuel` |
+| Return type: `Plausible.Gen α` | `G α` (polymorphic over `[Gen G]`) |
+| Instance: `ArbitraryFueled` | `GenFor α (fun _ => True)` |
+
+### Executing via Plausible
+
+The bridge instance from Section 3 provides backward compatibility:
+
+```lean
+instance [GenFor α (fun _ => True)] : Arbitrary α where
+  arbitrary := GenFor.gen  -- specializes at G := Plausible.Gen
+```
+
+## 7. Design Notes
+
+### Calling patterns summary
+
+The emitted code uses different calling conventions depending on the sub-generator kind:
+
+- **Non-backtracking leaf types** (via `GenFor`): Always succeeds, lifted into `BacktrackGen`:
+  ```lean
+  let n ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Nat)
+  ```
+
+- **Backtracking constrained sub-generator** (via `BacktrackGenFor`): May fail, resolved by typeclass. Failure propagates automatically via `bind`:
+  ```lean
+  let e ← BacktrackGenFor.gen (P := fun e => HasType e τ) initSize
+  ```
+
+- **Self-recursive call**: Direct, with decremented size:
+  ```lean
+  let l ← genHasType initSize .nat size
+  ```
+
+- **Hand-written non-backtracking constrained generator** (e.g., Basalt's `Tree.genBST`): Returns `G α`, registered as a `GenFor`:
+  ```lean
+  instance : GenFor (Tree Nat) (Tree.isBST 0 10) where
+    gen := Tree.genBST 0 10
+  ```
+
+### Mutual recursion
+
+For mutually recursive inductive relations, the emitted code uses Lean's `mutual ... end` block with direct name calls between co-defined generators (not typeclass resolution). After the mutual block, each generator is registered as a `BacktrackGenFor` instance. This is the same pattern Specimen uses today.
+
+### The `initSize` parameter
+
+- `size` is structurally decremented at each recursive call, ensuring termination.
+- `initSize` is the original fuel value, passed unchanged to sub-generators via `BacktrackGenFor.gen ... initSize`.
+
+Sub-generators always get a full budget. This matches today's behavior where `aux_arb initSize size' Ty.nat` passes `initSize` to nested calls.
+
+**Note on future changes.** The current approach — a local `size` that decrements structurally and a global `initSize` passed to sub-generators — is a good balance of generality and simplicity (see [Generator-config.md](Generator-config.md) for alternatives). However, this sizing strategy may need to change in the future as we gain experience with more complex generators or integrate with Basalt's `partial_fixpoint` approach, which eliminates the explicit fuel parameter entirely.
+
+### Known limitations
+
+**`partial_fixpoint` vs explicit fuel.** Basalt's hand-written generators use `partial_fixpoint` for termination (no explicit fuel parameter), enabling proofs of almost-sure termination. Specimen-derived generators use explicit `size : Nat` with structural recursion. The plan preserves this pattern. A future optimization could emit `partial_fixpoint` generators, eliminating the fuel parameter and enabling tighter cost bounds. This is deferred beyond Phase 2.
+
+> **Further design discussion** (typeclass resolution safety, fuel vs `partial_fixpoint`, performance benchmarks): see Appendices A and B.
+
+## 8. Plan of Work
+
+The work proceeds in two major phases. Phase 1 makes Specimen emit Basalt-compatible generators that can be executed via Plausible. Phase 2 upgrades the system so that every derived generator is provably lawful.
+
+### Phase 1: Basalt-compatible generation (execution only)
+
+The goal of this phase is to make Specimen-derived generators polymorphic over Basalt's `Gen` class, using `BacktrackGen` for backtracking and `GenFor` / `BacktrackGenFor` for sub-generator resolution. Generators can be executed via Plausible but do not yet carry correctness proofs.
+
+**Success criteria:** All existing Specimen snapshot tests pass (with updated expected output reflecting the new code shape). The `plausible` tactic works end-to-end for both `derive Arbitrary` and `derive_generator`. At least one manual soundness proof is completed for the running example.
+
+#### Step 1.1: Define `BacktrackGen` and generator typeclasses in Basalt
+
+- Define `BacktrackGen G α := G (Option α)` as a newtype
+- Implement helper functions: `pure`/`fail`/`bind`/`liftGen` for `BacktrackGen`
+- Implement `BacktrackGen.run` and `BacktrackGen.toPlausibleGen`
+- Implement the `backtrack` combinator (weighted random selection with retry)
+- Implement the `frequency` combinator (weighted random selection, no retry — for non-backtracking generators)
+- Define the `GenFor α P` and `BacktrackGenFor α P` typeclasses
+- Redefine `DecOpt P` to return `BacktrackGen G Bool` (polymorphic over `G`)
+- Provide `GenFor` instances for standard types (`Nat`, `Bool`, `List`, etc.) using existing Basalt-polymorphic generators
+- Provide bridge instance: `instance [Decidable P] : DecOpt P`
+- Optionally provide bridge: `instance [GenFor α (fun _ => True)] : Arbitrary α`
+
+#### Step 1.2: Prove SetGen support lemmas
+
+- `backtrack_mem_iff`: `some a ∈ support ((backtrack gs).run)` iff `some a ∈ support ((gs[i].2 ()).run)` for some `i`
+- `frequency_mem_iff`: analogous for `frequency`
+- `backtrackGen_bind_mem`: decomposition of sequential composition inside `BacktrackGen` branches
+- `backtrackGen_pure_mem`: base case for branch decomposition
+- Basic `liftGen` support lemma
+
+#### Step 1.3: Modify Specimen's constrained code emission (`derive_generator`)
+
+- Replace `GeneratorCombinators.backtrack` with Basalt's `backtrack` over `BacktrackGen G`
+- Replace `Gen.frequency` / `oneOfWithDefault` with Basalt's `frequency`
+- Replace `throw` with `BacktrackGen.fail`
+- Replace fuel-based recursion with structural recursion on an explicit `size : Nat`
+- Emit generators polymorphic over `[Gen G]` with `[GenFor α P]` / `[BacktrackGenFor α P]` constraints
+- Replace `Arbitrary.arbitrary` calls with `GenFor.gen` wrapped in `BacktrackGen.liftGen`
+- Replace `ArbitrarySizedSuchThat.arbitrarySizedST` calls with `BacktrackGenFor.gen`
+- Replace `DecOpt.decOpt` calls (pattern-matching on `Except`) with the new polymorphic `DecOpt.decOpt`
+- Emit `ArbitrarySizedSuchThat` instances that call `BacktrackGen.toPlausibleGen`
+
+#### Step 1.4: Modify Specimen's unconstrained code emission (`derive Arbitrary`)
+
+- Replace `Gen.oneOfWithDefault` / `Gen.frequency` with Basalt's `frequency` combinator
+- Replace `Arbitrary.arbitrary` calls with `GenFor.gen (P := fun _ => True)`
+- Emit generators polymorphic over `[Gen G]` with `[GenFor α (fun _ => True)]` constraints
+- Emit `GenFor α (fun _ => True)` instances for each derived type
+- Emit bridge `Arbitrary` instance
+- Ensure mutually recursive types use `mutual ... end` with direct name calls
+
+This step can proceed in parallel with Step 1.3 since the unconstrained deriver (`DeriveArbitrary.lean`) is independent of the constrained deriver (`DeriveConstrainedProducer.lean`).
+
+#### Step 1.5: Validate the pipeline
+
+- Verify existing Specimen test cases still pass (update snapshots for new output shape)
+- Verify `derive Arbitrary` produces working `GenFor` instances for standard test types
+- Verify the `plausible` tactic works end-to-end with both constrained and unconstrained generators
+- Write a manual soundness proof for the `HasType` example demonstrating `BacktrackGenCorrect`
+
+### Phase 2: Lawful generation (with proof synthesis)
+
+The goal of this phase is to make Specimen emit `BacktrackGenCorrect` certificates alongside the generators, so that every derived generator carries a machine-checked proof of soundness and completeness.
+
+#### Step 2.1: Define `BacktrackGenCorrect` in Basalt
+
+- Define `BacktrackGenCorrect` structure with `sound` and `complete` fields at `SetGen.Set`
+- Proofs for composite generators take `BacktrackGenCorrect` certificates as hypotheses
+- Provide `BacktrackGenCorrect` certificates for standard types
+
+#### Step 2.2: Synthesize soundness/completeness proofs in Specimen
+
+For each derived **constrained** generator, Specimen emits a proof that the generator's support at `SetGen.Set` matches the target relation. The proof structure:
+
+1. **Top-level**: `cases` on `size`, matching the generator's pattern match.
+2. **Per-branch**: `backtrack_mem_iff` decomposes into a disjunction over branches.
+3. **Soundness**: For each branch producing `some a`, show `P a` holds.
+4. **Completeness**: For each constructor of the inductive relation, exhibit a `size` and branch that produces the corresponding value.
+
+Sub-generator obligations are stated as `BacktrackGenCorrect` hypotheses — keeping proofs modular.
+
+For **unconstrained** generators, the property is `True`, so soundness is trivial. Completeness amounts to showing every inhabitant is reachable at some fuel — following the inductive structure of the type.
+
+#### Step 2.3: End-to-end validation
+
+- Verify derived generators carry correct proofs (no `sorry`)
+- Verify proofs compose across sub-generators
+- Benchmark elaboration time
+
+### Rollback strategy
+
+If Phase 1 reveals fundamental design issues, the changes are confined to:
+- New definitions in Basalt (additive, do not break existing Basalt code)
+- Modified code emission in Specimen (can be feature-flagged or reverted)
+
+The existing `GeneratorCombinators.backtrack` path remains functional. A feature flag (`set_option specimen.basaltBridge true`) can gate the new emission path.
+
+## Glossary
+
+| Term | Meaning |
+|---|---|
+| **Constrained producer** | A generator that only produces values satisfying a user-specified inductive relation |
+| **Support** | The set of values a generator can produce (with nonzero probability) |
+| **Fuel / size** | A `Nat` parameter that bounds recursion depth, ensuring termination |
+| **`initSize`** | The *original* fuel value passed at the top level; sub-generators receive the full budget |
+| **Schedule** | Specimen's internal representation of how to order constructor attempts |
+| **Backtracking** | The ability for a generator branch to signal failure, causing retry |
+| **`BacktrackGen`** | A newtype wrapping `G (Option α)` — the backtracking layer used in this plan |
+| **`GenFor` / `BacktrackGenFor`** | Typeclasses for sub-generator lookup (analogous to `Arbitrary` / `ArbitrarySizedSuchThat`) |
+
+---
+
+## Appendix A: Design Rationale
+
+### Why `BacktrackGen` is a structure (newtype)
+
+`BacktrackGen` is defined as a `structure` wrapping `G (Option α)` rather than a type alias for two reasons:
+
+1. **Disambiguation.** Without the newtype, `G (Option α)` is ambiguous — it could be a generator that legitimately produces `Option` values (where `none` is a valid output) or a backtracking generator where `none` signals failure. `BacktrackGen` makes the intent explicit at the type level.
+
+2. **Own Monad instance.** As a `structure`, `BacktrackGen G` gets its own `Monad` instance that threads `Option` automatically. This means `pure x` wraps in `some`, and `bind` short-circuits on `none`. Without this, code inside backtracking branches would need to manually construct `pure (some x)` and pattern-match on `Option` at every bind.
+
+### Why typeclass resolution is safe here
+
+A natural concern: typeclass resolution is opaque, so how can a proof about `genWellFormed` know which `BacktrackGenFor Expr (HasType · τ)` instance was resolved?
+
+The answer is that we do **not** attempt to discharge this — correctness proofs are parameterized by a `BacktrackGenCorrect` hypothesis about whatever the sub-generator resolves to. The theorem states: "if the sub-generator (whatever it is) is sound and complete, then `genWellFormed` is sound and complete." This is honest about the opacity of instance resolution and avoids the instance diamond problem entirely.
+
+In practice, for a fully-closed correctness argument, one would need to show that the specific `BacktrackGenFor` instance registered for `HasType` corresponds to `genHasType` (which has its own `BacktrackGenCorrect` certificate). This final connection step is left as an assumption — it's a statement about instance resolution stability that Lean doesn't expose as a provable fact.
+
+### Fuel vs size vs `partial_fixpoint`
+
+The `size`/`fuel` parameter in generated code serves two distinct purposes:
+
+1. **Termination witness.** Lean requires structural recursion (or `partial_fixpoint`) for every recursive definition. The `size : Nat` parameter with pattern-matching on `0` vs `size + 1` provides this.
+
+2. **Size control.** In property-based testing, generators need a knob that controls the size of generated values. Plausible's `Gen.sized` provides this via a `ReaderT (ULift Nat)` layer.
+
+These two roles coincide in today's Specimen output (the fuel *is* the size), but are conceptually independent:
+
+- **For constrained generators (`BacktrackGenFor`):** Both roles are essential. The fuel ensures termination and bounds derivation tree depth.
+
+- **For unconstrained generators (`GenFor`):** The fuel is used *only* for termination and size control. In Basalt, `partial_fixpoint` could eliminate the explicit termination witness, since it provides a well-founded recursion principle with `⊥` as the default.
+
+**Practical upshot:** Phase 1 preserves explicit fuel for both. A future optimization could emit `partial_fixpoint`-based generators:
+```lean
+def Tree.gen [Gen G] [GenFor α (fun _ => True)] : G (Tree α) :=
+  partial_fixpoint fun self => frequency (pure Tree.leaf) [
+    (1, fun () => pure Tree.leaf),
+    (???, fun () => do  -- weight needs to come from somewhere
+      let left ← self
+      let val ← GenFor.gen (P := fun _ => True)
+      let right ← self
+      pure (Tree.node left val right))]
+```
+The open question is expressing size-dependent weights without explicit fuel. Deferred as a research question.
+
+### Why `Bounded` is separate from `P` in `BacktrackGenCorrect`
+
+The property `P` (e.g., `HasType e τ`) is the *semantic* specification the user cares about. But a fuel-based generator cannot produce *all* values satisfying `P` at every size — it only produces values within its size budget and sub-generator ranges. The `Bounded` predicate captures these implementation constraints: `Bounded size a` implies `P a` but additionally requires bounded depth and bounded leaf values.
+
+This two-parameter design is a direct consequence of using explicit fuel for termination. If generators were defined via `partial_fixpoint` — where the generator's support at the fixpoint covers all values satisfying `P` — then `Bounded` would be unnecessary. The `Bounded` parameter is the price of fuel-based termination; eliminating it is a benefit of moving to `partial_fixpoint` in the future.
+
+## Appendix B: Performance
+
+`BacktrackGen` adds an `Option` wrapper at every bind within backtracking branches. Benchmarking (`SpecimenTest/BridgeBenchmark.lean`) shows:
+
+| Scenario | Bridge/legacy ratio | Notes |
+|---|---|---|
+| Recursive generator (5-ary constructor, sizes 2–4) | 97–101% | Dominant cost is recursion; `Option` overhead invisible |
+| Backtracking on guards (`isPos`, DecOpt check) | 100–105% | Within noise |
+| Stress test: 5 branches × 5 `liftGen`s, 4 always fail | **118%** | Worst case: cheap branches that fail frequently |
+| Same stress test with batched `liftGen`s | **106%** | Batching cuts overhead by ~2/3 |
+
+The 18% worst-case arises when branches consist almost entirely of `liftGen` calls and multiple branches are tried per iteration. In realistic generators (like Cedar's `HasType` with 23 constructors), the `Option` overhead is amortized to < 3%.
+
+**IR verification:** The Lean 4 compiler erases the `BacktrackGen` newtype (no `.mk`/`.run` in compiled IR), and `@[specialize]` eliminates the `[Gen G]` dictionary when instantiated at `Plausible.Gen`.
+
+### Optimization: batching consecutive `liftGen` calls
+
+When multiple unconstrained field generations appear consecutively (before any backtracking operation), they can be batched:
+
+```lean
+-- Before (3 Option wraps + 3 Option checks):
+let a ← BacktrackGen.liftGen (GenFor.gen : G Nat)
+let b ← BacktrackGen.liftGen (GenFor.gen : G Nat)
+let c ← BacktrackGen.liftGen (GenFor.gen : G Nat)
+
+-- After (1 Option wrap + 1 Option check):
+let (a, b, c) ← BacktrackGen.liftGen (do
+  let a ← (GenFor.gen : G Nat)
+  let b ← (GenFor.gen : G Nat)
+  let c ← (GenFor.gen : G Nat)
+  pure (a, b, c))
+```
+
+The batching boundary is any operation that can fail: a `BacktrackGenFor.gen` call, a `DecOpt` check, or `BacktrackGen.fail`.
+
+### Optimization: `liftBind` for interleaved non-backtracking operations
+
+When a `liftGen` is followed by a backtracking continuation (not another `liftGen`), a fused combinator eliminates the intermediate `Option`:
+
+```lean
+@[inline] def BacktrackGen.liftBind [Gen G] (g : G α) (f : α → BacktrackGen G β) : BacktrackGen G β :=
+  ⟨do let a ← g; (f a).run⟩
+```
+
+Neither optimization affects provability: `liftBind g f` has the same denotation as `bind (liftGen g) f` at all Basalt interpretations.
+
+## Appendix C: Proof Strategy
+
+### `BacktrackGenCorrect`
+
+```lean
+/-- A correctness certificate for a backtracking generator: soundness + completeness
+    with respect to a size-indexed predicate. This is a proof artifact only — it does not
+    contain or constrain the generator code. -/
+structure BacktrackGenCorrect.{u}
+    (gen : ∀ {G : Type u → Type u} [Gen G], Nat → BacktrackGen G α)
+    (Bounded : Nat → α → Prop) where
+  sound : ∀ size a,
+    some a ∈ SetGen.support ((gen (G := SetGen.Set) size).run) → Bounded size a
+  complete : ∀ size a,
+    Bounded size a → some a ∈ SetGen.support ((gen (G := SetGen.Set) size).run)
+```
+
+**Relationship to Basalt's `LawfulGenerator`:** Basalt's `LawfulGenerator` says "this particular generator is sound, complete, terminating, and cost-bounded." Our `BacktrackGenCorrect` serves a different purpose: it asserts that a generator function is sound and complete with respect to a bounded predicate. It omits cost and termination requirements; these could be added as future structure fields.
+
+### The key lemma: `backtrack_mem_iff`
+
+```lean
+theorem backtrack_mem_iff (gs : List (Nat × (Unit → BacktrackGen SetGen.Set α)))
+    (hpos : ∀ i : Fin gs.length, gs[i].1 > 0) (a : α) :
+    some a ∈ SetGen.support ((backtrack gs).run) ↔
+    ∃ i : Fin gs.length, some a ∈ SetGen.support ((gs[i].2 ()).run) := ...
+```
+
+This reduces reasoning about `backtrack` to reasoning about individual branches.
+
+### Proof structure for the running example
+
+**The predicate:**
+
+```lean
+def HasTypeBounded (τ : Ty) (size : Nat) (e : Expr) : Prop :=
+  HasType e τ ∧ exprBounded size e
+```
+
+where `exprBounded size e` requires leaf naturals ≤ 100 and `add`-nesting ≤ `size`.
+
+**Soundness** proceeds by induction on `size`, applying `backtrack_mem_iff` to decompose into branches, then case-splitting on `τ`. For the `isPos` branch, the `DecOpt` check produces a `Bool` matched on — only `true` reaches `pure (Expr.isPos n)`, yielding `HasType.isPos` with proof `n ≠ 0`.
+
+**Completeness** proceeds by induction on `size`, constructing the appropriate branch index for each `HasType` constructor. `HasType.add` maps to branch 2 in the `size + 1` case.
+
+**Compositionality.** Correctness proofs for generators that call sub-generators are parameterized by correctness certificates of those sub-generators:
+
+```lean
+theorem genWellFormed_correct
+    (sub_correct : ∀ τ, BacktrackGenCorrect
+      (fun {G} [Gen G] (size : Nat) => BacktrackGenFor.gen (P := fun e => HasType e τ) (G := G) size)
+      (HasTypeBounded τ)) :
+    BacktrackGenCorrect (fun size => genWellFormed size size) WellFormedBounded where
+  sound := fun initSize p h => by ...
+  complete := fun initSize p h => by ...
+```
+
+The proof uses `(sub_correct τ).sound` / `(sub_correct τ).complete` to discharge sub-generator obligations. No "lawful instance" routing is needed.
+
+## Appendix D: Interpretations Across Basalt Instances
+
+### `BacktrackGen`
+
+| Instance | `BacktrackGen G α` is... | `none` means... | `some a` means... |
+|---|---|---|---|
+| `SetGen.Set` | `Set (Option α)` | failure is reachable | `a` is reachable |
+| `SPMF` | `SPMF (Option α)` | mass on failure | mass on producing `a` |
+| `SPMF.Cost` | `SPMF (Option α × Nat)` | failure with cost `n` | producing `a` with cost `n` |
+| `Plausible.Gen` | `Plausible.Gen (Option α)` | generation failed | generation succeeded |
+
+Note: `SPMF.Cost` tracks the number of `choose` calls. In `backtrack`, each retry costs one `choose` plus whatever choices that branch made. The cost of backtracking falls out automatically from existing `IsBounded_bind` and `IsBounded_choose` theorems.
+
+### `DecOpt`
+
+| Instance | `DecOpt.decOpt P fuel` is... | `none` means... | `some true/false` means... |
+|---|---|---|---|
+| `SetGen.Set` | `Set (Option Bool)` | checking may fail | P is/isn't decidable as true |
+| `SPMF` | `SPMF (Option Bool)` | mass on undecided | mass on decided |
+| `Plausible.Gen` | `Plausible.Gen (Option Bool)` | checker ran out of fuel | checker decided |
diff --git a/SPECIMEN-BASALT-BRIDGE.md b/SPECIMEN-BASALT-BRIDGE.md
deleted file mode 100644
index 1ebef4d..0000000
--- a/SPECIMEN-BASALT-BRIDGE.md
+++ /dev/null
@@ -1,236 +0,0 @@
-# Bridging Specimen and Basalt via `BacktrackGen`
-
-This document describes a plan to make [Specimen](https://github.com/strata-org/specimen)-derived generators compatible with [Basalt](https://code.amazon.com/packages/Basalt)'s correctness proof infrastructure.
-
-## 1. Status Quo
-
-### The three frameworks
-
-**Plausible** is a property-based testing library for Lean. Its `Gen` monad is a stack of monad transformers:
-```
-abbrev Gen (α : Type u) := RandT (ReaderT (ULift Nat) (Except GenError)) α
-```
-It provides randomness, a size parameter, and exception-based failure. The `plausible` tactic finds `Testable` instances (which bottom out at `Arbitrary` instances) via typeclass synthesis and executes them.
-
-**Specimen** derives generators for values satisfying inductive relations, built on top of Plausible. It emits `Plausible.Gen α` terms that use `throw`/`tryCatch` for backtracking: when a branch can't satisfy constraints, it throws a `GenError`, and the `backtrack` combinator catches it and retries another branch. Key typeclasses:
-- `ArbitrarySizedSuchThat α P` — a sized generator (`Nat → Gen α`) for values satisfying `P`
-- `ArbitrarySuchThat α P` — the unsized wrapper (via `Gen.sized`)
-
-**Basalt** defines a `Gen` typeclass abstracting the capabilities needed by a generator:
-```lean
-class Gen (g : Type u → Type v) where
-  instInhabited : ∀ α, Inhabited (g α)
-  instMonad : Monad g
-  instRandomChoice : RandomChoice g
-  instCCPO : ∀ α, CCPO (g α)
-  instMonoBind : MonoBind g
-```
-Basalt provides multiple instances: `SetGen.Set` (for soundness/completeness proofs), `SPMF` (for termination/distribution proofs), `SPMF.Cost` (for cost bounds), and `Plausible.Gen` (for execution, via `Basalt/PlausibleGen.lean`). A generator written polymorphically as `[Gen G] → G α` can be proved correct at `SetGen`/`SPMF` and executed at `Plausible.Gen`.
-
-### Current dependency structure
-
-```
-Plausible ← Specimen    (Specimen emits Plausible.Gen terms)
-Plausible ← Basalt      (PlausibleGen makes Plausible.Gen a Basalt Gen instance)
-```
-
-Specimen and Basalt are currently unrelated — Specimen-derived generators cannot be reasoned about using Basalt's correctness classes.
-
-### The problem
-
-Specimen emits generators that target `Plausible.Gen` directly. These generators cannot be instantiated at `SetGen.Set` or `SPMF` for proofs. To prove a Specimen-derived generator is sound, complete, terminating, or cost-bounded, we need it to be polymorphic over Basalt's `Gen` class.
-
-The core challenge is **backtracking**. Specimen's `backtrack` combinator uses Plausible's `throw`/`tryCatch` (exception-based control flow) to retry branches. Basalt has no exception mechanism — its `Gen` class provides only `choose`, `bind`, `pure`, and ⊥ (`default`). We need a way to express backtracking that works across all Basalt interpretations.
-
-## 2. The Change: `BacktrackGen`
-
-We introduce a newtype that wraps `G (Option α)` to represent generators that may fail locally:
-
-```lean
-/-- A backtracking generator: G (Option α) where none = local failure, some = success. -/
-def BacktrackGen (G : Type → Type) (α : Type) := G (Option α)
-```
-
-The `Option` layer is *inside* the generator monad `G`, meaning failure is a **value** that the generator successfully produces (as opposed to ⊥/`default`, which represents divergence). This lets other generators observe and react to failure — enabling retry.
-
-### The `backtrack` combinator
-
-```lean
-/-- Weighted backtracking: randomly pick a branch by weight, try it, retry remaining on failure. -/
-def backtrack [Gen G] (gs : List (Nat × (Unit → BacktrackGen G α))) : BacktrackGen G α :=
-  go (sumWeights gs) gs
-where
-  go (total : Nat) : List (Nat × (Unit → BacktrackGen G α)) → BacktrackGen G α
-  | [] => pure none
-  | gs => do
-    let n ← choose 0 (total - 1) (by omega)
-    let (k, g, rest) := pickDrop gs n
-    match ← g () with
-    | some a => pure (some a)
-    | none => go (total - k) rest
-```
-
-This has identical operational semantics to Specimen's current `backtrack`: pick a branch randomly by weight, run it, and if it returns `none` (failure), remove it from the pool and retry with adjusted weights.
-
-### Boundary: unwrapping `BacktrackGen` to `Gen`
-
-At the outermost level — where a generator must produce a value for Plausible's testing machinery — we collapse the `Option`:
-
-```lean
-def BacktrackGen.run [Gen G] (g : BacktrackGen G α) : G α := do
-  match ← g with
-  | some a => pure a
-  | none => default  -- ⊥ (divergence)
-
-def BacktrackGen.toPlausibleGen (g : BacktrackGen Plausible.Gen α) : Plausible.Gen α := do
-  match ← g with
-  | some a => pure a
-  | none => throw (.genError "backtracking exhausted")
-```
-
-### Why a newtype?
-
-Without the newtype, `G (Option α)` is ambiguous — it could be a generator that legitimately produces `Option` values (where `none` is a valid output) or a backtracking generator where `none` signals failure. `BacktrackGen` makes the intent explicit at the type level.
-
-### Composability
-
-Internal backtracking generators compose by staying in `BacktrackGen G`:
-
-```lean
--- A Stmt generator calling an Expr generator — failure propagates naturally
-def genStmt [Gen G] (ctx : Ctx) : BacktrackGen G Stmt := do
-  let some e ← genExpr ctx τ | pure none   -- observe failure, propagate
-  pure (some (Stmt.assign x e))
-```
-
-Failure information is only lost at the outermost boundary (`toPlausibleGen`). This avoids the problem where wrapping a sub-generator too early prevents the caller from backtracking through it.
-
-### Interpretations across Basalt instances
-
-| Instance | `BacktrackGen G α` is... | `none` means... | `some a` means... |
-|---|---|---|---|
-| `SetGen.Set` | `Set (Option α)` | failure is reachable | `a` is reachable |
-| `SPMF` | `SPMF (Option α)` | mass on failure | mass on producing `a` |
-| `SPMF.Cost` | `SPMF (Option α × Nat)` | failure with cost `n` | producing `a` with cost `n` |
-| `Plausible.Gen` | `Plausible.Gen (Option α)` | generation failed | generation succeeded |
-
-### Cost tracking
-
-Basalt's `SPMF.Cost` tracks the number of `choose` calls. In `backtrack`, each retry costs one `choose` (to select the next branch) plus whatever choices that branch made. The cost of backtracking falls out automatically from existing `IsBounded_bind` and `IsBounded_choose` theorems — no new cost infrastructure is needed. You can prove bounds like "producing value `a` costs at most `n + c(a)`" where `n` is the number of branches (worst-case retries) and `c(a)` is the cost of the successful branch.
-
-### New dependency structure
-
-```
-Plausible ← Basalt ← Specimen
-```
-
-Specimen depends on Basalt for `Gen`, `BacktrackGen`, and `backtrack`. The `plausible` tactic still works: Specimen emits `ArbitrarySizedSuchThat` instances (as it does today) whose body calls `BacktrackGen.toPlausibleGen` to produce the `Plausible.Gen α` that Plausible's machinery expects.
-
-## 3. Example
-
-Consider a simple typing relation:
-
-```lean
-inductive Ty | nat | bool
-inductive Expr | lit (n : Nat) | isZero (e : Expr)
-
-inductive HasType : Expr → Ty → Prop
-  | litNat (n : Nat) : HasType (.lit n) .nat
-  | isZero (e : Expr) : HasType e .nat → HasType (.isZero e) .bool
-```
-
-### What Specimen emits today
-
-```lean
-def genHasType (τ : Ty) : Nat → Plausible.Gen Expr
-  | 0 => GeneratorCombinators.backtrack [
-      (1, match τ with | .nat => do let n ← Arbitrary.arbitrary; pure (.lit n)
-                       | _ => throw Gen.genericFailure)]
-  | size + 1 => GeneratorCombinators.backtrack [
-      (1, match τ with | .nat => do let n ← Arbitrary.arbitrary; pure (.lit n)
-                       | _ => throw Gen.genericFailure),
-      (1, match τ with | .bool => do let e ← genHasType .nat size; pure (.isZero e)
-                       | _ => throw Gen.genericFailure)]
-```
-
-This can be executed but not proved correct.
-
-### What Specimen would emit after the change
-
-```lean
-def genHasType [Gen G] (τ : Ty) : Nat → BacktrackGen G Expr
-  | 0 => backtrack [
-      (1, fun () => match τ with
-        | .nat => do let n ← liftGen (genNat : G Nat); pure (some (.lit n))
-        | _ => pure none)]
-  | size + 1 => backtrack [
-      (1, fun () => match τ with
-        | .nat => do let n ← liftGen (genNat : G Nat); pure (some (.lit n))
-        | _ => pure none),
-      (1, fun () => match τ with
-        | .bool => do
-            let some e ← genHasType .nat size | pure none
-            pure (some (.isZero e))
-        | _ => pure none)]
-where
-  liftGen (g : G α) : BacktrackGen G α := do let a ← g; pure (some a)
-```
-
-### Proving correctness (at `SetGen.Set`)
-
-```lean
-theorem genHasType_sound (τ : Ty) (size : Nat) (e : Expr) :
-    some e ∈ SetGen.support (genHasType (G := SetGen.Set) τ size) → HasType e τ := ...
-
-theorem genHasType_complete (τ : Ty) (e : Expr) (h : HasType e τ) :
-    ∃ size, some e ∈ SetGen.support (genHasType (G := SetGen.Set) τ size) := ...
-```
-
-### Executing via Plausible
-
-```lean
-instance : ArbitrarySizedSuchThat Expr (HasType · τ) where
-  arbitrarySizedST size := BacktrackGen.toPlausibleGen (genHasType τ size)
-```
-
-The `plausible` tactic finds this instance via the existing `ArbitrarySizedSuchThat → ArbitrarySuchThat → Arbitrary` chain and executes it normally.
-
-### The size pattern
-
-The generator takes `size : Nat` as an explicit parameter (structural recursion ensures termination). At the Plausible call site, `Gen.sized` bridges Plausible's reader-based size to this parameter:
-
-```lean
-instance : ArbitrarySuchThat Expr (HasType · τ) where
-  arbitraryST := Gen.sized (fun n => BacktrackGen.toPlausibleGen (genHasType τ n))
-```
-
-## 4. Plan of Work
-
-### Step 1: Define `BacktrackGen` in Basalt
-
-- Define `BacktrackGen G α := G (Option α)` as a newtype
-- Implement helper functions: `pure`/`fail`/`bind`/`liftGen` for `BacktrackGen`
-- Implement `BacktrackGen.run` and `BacktrackGen.toPlausibleGen`
-- Implement the `backtrack` combinator (weighted random selection with retry)
-- Implement `frequency` combinator (weighted random selection, no retry — for unconstrained generators)
-
-### Step 2: Prove SetGen support lemmas
-
-- `backtrack_mem_iff`: `some a ∈ support (backtrack gs)` iff `some a ∈ support (gᵢ ())` for some `i`
-- `frequency_mem_iff`: analogous for `frequency`
-- Basic `liftGen`/`pure`/`bind` support lemmas
-
-### Step 3: Modify Specimen's code emission
-
-- Replace `GeneratorCombinators.backtrack` with Basalt's `backtrack` over `BacktrackGen G`
-- Replace `Gen.frequency` / `oneOfWithDefault` with Basalt's `frequency`
-- Replace `throw` with `pure none`
-- Replace fuel-based recursion with structural recursion on an explicit `size : Nat`
-- Emit generators polymorphic over `[Gen G]` instead of targeting `Plausible.Gen`
-- Emit `ArbitrarySizedSuchThat` instances that call `BacktrackGen.toPlausibleGen`
-
-### Step 4: Validate the pipeline
-
-- Verify existing Specimen test cases still pass (generators execute correctly via Plausible)
-- Write a small proof (e.g., the `HasType` example) demonstrating that a Specimen-derived generator can be proved sound at `SetGen.Set`
-- Verify the `plausible` tactic works end-to-end with the new generators
diff --git a/SpecimenTest/BasaltPort/BridgeBacktrackMockup.lean b/SpecimenTest/BasaltPort/BridgeBacktrackMockup.lean
new file mode 100644
index 0000000..89a6441
--- /dev/null
+++ b/SpecimenTest/BasaltPort/BridgeBacktrackMockup.lean
@@ -0,0 +1,470 @@
+import Plausible
+import Specimen.DecOpt
+import Specimen.ArbitrarySizedSuchThat
+import Specimen.GeneratorCombinators
+
+/-!
+# Specimen–Basalt Bridge Mockup: Backtracking, Sub-generators, and Checkers
+
+This file demonstrates all three mechanisms from Specimen-Basalt-port.md in a single
+example that genuinely exercises each:
+
+1. **Backtracking**: The `isPos` branch (targeting `.bool`) generates `n` randomly and
+   fails if `n = 0`. The `add` and `lit` branches fail when `τ ≠ .nat`. The `backtrack`
+   combinator retries another branch on failure.
+2. **Sub-generators (BacktrackGenFor)**: The `WellFormed` generator calls into the
+   `HasType` generator via typeclass resolution (`BacktrackGenFor.gen`).
+3. **Checkers (DecOpt)**: `n ≠ 0` is checked via `DecOpt` after `n` is already generated —
+   this is a pure guard on an already-determined value.
+
+The mockup presents:
+- What Specimen generates **today** (status quo, using Plausible directly)
+- What the **migrated** code looks like (using BacktrackGen, GenFor, BacktrackGenFor, DecOpt)
+
+The status-quo code is taken directly from Specimen's trace output for this example.
+-/
+
+open Lean.Order
+
+namespace MockBacktrack
+
+/-! ## Basalt infrastructure -/
+
+class RandomChoice (m : Type u → Type v) where
+  choose : (lo hi : Nat) → (h : lo ≤ hi) → m (ULift Nat)
+
+class Gen (g : Type u → Type v) where
+  instInhabited : ∀ α, Inhabited (g α)
+  instMonad : Monad g
+  instRandomChoice : RandomChoice g
+  instCCPO : ∀ α, CCPO (g α)
+  instMonoBind : MonoBind g
+
+instance [m : Gen g] : ∀ α, Inhabited (g α) := m.instInhabited
+instance [m : Gen g] : Monad g := m.instMonad
+instance [m : Gen g] : RandomChoice g := m.instRandomChoice
+instance [m : Gen g] : ∀ α, CCPO (g α) := m.instCCPO
+instance [m : Gen g] : MonoBind g := m.instMonoBind
+
+private instance instPartialOrderExceptGenError : PartialOrder (Except Plausible.GenError α) :=
+  FlatOrder.instOrder (b := Except.error default)
+
+private instance instCCPOExceptGenError : CCPO (Except Plausible.GenError α) :=
+  FlatOrder.instCCPO (b := Except.error default)
+
+private instance : MonoBind (Except Plausible.GenError) where
+  bind_mono_left h := by
+    cases h with
+    | bot => exact FlatOrder.rel.bot
+    | refl => exact FlatOrder.rel.refl
+  bind_mono_right h := by
+    cases ‹Except Plausible.GenError _› with
+    | error => exact FlatOrder.rel.refl
+    | ok a => exact h a
+
+private instance : RandomChoice Plausible.Gen where
+  choose lo hi _ := do
+    let ⟨val, _⟩ ← Plausible.Gen.choose Nat lo hi (by omega)
+    ULift.up <$> pure val
+
+instance : Gen Plausible.Gen where
+  instInhabited := inferInstance
+  instMonad := inferInstance
+  instRandomChoice := inferInstance
+  instCCPO := inferInstance
+  instMonoBind := inferInstance
+
+/-! ## BacktrackGen -/
+
+structure BacktrackGen (G : Type → Type) (α : Type) where
+  run : G (Option α)
+
+namespace BacktrackGen
+
+instance [Gen G] : Monad (BacktrackGen G) where
+  pure a := ⟨pure (some a)⟩
+  bind x f := ⟨do
+    match ← x.run with
+    | some a => (f a).run
+    | none => pure none⟩
+
+instance [Gen G] : Inhabited (BacktrackGen G α) where
+  default := ⟨pure none⟩
+
+def liftGen [Gen G] (g : G α) : BacktrackGen G α :=
+  ⟨do let a ← g; pure (some a)⟩
+
+def fail [Gen G] : BacktrackGen G α :=
+  ⟨pure none⟩
+
+def toPlausibleGen (x : BacktrackGen Plausible.Gen α) : Plausible.Gen α := do
+  match ← x.run with
+  | some a => pure a
+  | none => throw (.genError "backtracking exhausted")
+
+end BacktrackGen
+
+/-! ## Combinators -/
+
+/-- Sum of weights in a weighted generator list. -/
+def sumWeights (gs : List (Nat × β)) : Nat :=
+  gs.map Prod.fst |>.sum
+
+/-- Weighted selection with drop: given `n ∈ [0, total-1]`, find the element whose weight
+    interval contains `n`, return its weight, the element, and the remaining list. -/
+def pickDrop [Inhabited β] (gs : List (Nat × β)) (n : Nat) : Nat × β × List (Nat × β) :=
+  match gs with
+  | [] => (0, default, [])
+  | (k, g) :: rest =>
+    if n < k then (k, g, rest)
+    else
+      let (k', g', rest') := pickDrop rest (n - k)
+      (k', g', (k, g) :: rest')
+
+/-- Weighted backtracking: randomly pick a branch by weight, try it, retry remaining on failure.
+    Uses fuel (initially gs.length) for termination, matching Specimen's backtrackFuel. -/
+def backtrack [Gen G] (gs : List (Nat × (Unit → BacktrackGen G α))) : BacktrackGen G α :=
+  ⟨go gs.length (sumWeights gs) gs⟩
+where
+  go : Nat → Nat → List (Nat × (Unit → BacktrackGen G α)) → G (Option α)
+  | _, _, [] => pure none
+  | 0, _, _ => pure none
+  | fuel + 1, total, gs@(_ :: _) => do
+    let n ← RandomChoice.choose 0 (total - 1) (by omega)
+    let (k, g, gs') := pickDrop gs n.down
+    match ← (g ()).run with
+    | some a => pure (some a)
+    | none => go fuel (total - k) gs'
+
+/-! ## Typeclasses -/
+
+class GenFor (α : Type) (P : α → Prop) where
+  gen : ∀ {G : Type → Type} [Gen G], G α
+
+class BacktrackGenFor (α : Type) (P : α → Prop) where
+  gen : ∀ {G : Type → Type} [Gen G], Nat → BacktrackGen G α
+
+class DecOpt (P : Prop) where
+  decOpt : ∀ {G : Type → Type} [Gen G], Nat → BacktrackGen G Bool
+
+instance (priority := low) [Decidable P] : DecOpt P where
+  decOpt _ := pure (decide P)
+
+/-! ## Running example -/
+
+inductive Ty | nat | bool
+  deriving Repr, Inhabited, BEq, DecidableEq
+
+inductive Expr
+  | lit (n : Nat)
+  | isPos (n : Nat)
+  | add (l r : Expr)
+  deriving Repr, Inhabited
+
+inductive HasType : Expr → Ty → Prop
+  | lit (n) : HasType (.lit n) .nat
+  | isPos (n) : n ≠ 0 → HasType (.isPos n) .bool
+  | add (l r) : HasType l .nat → HasType r .nat → HasType (.add l r) .nat
+
+inductive Prog
+  | expr (e : Expr)
+  | both (e1 e2 : Expr)
+  deriving Repr, Inhabited
+
+inductive WellFormed : Prog → Prop
+  | expr (e τ) : HasType e τ → WellFormed (.expr e)
+  | both (e1 e2 τ) : HasType e1 τ → HasType e2 τ → WellFormed (.both e1 e2)
+
+/-! ## GenFor instances for leaf types -/
+
+instance : GenFor Nat (fun _ => True) where
+  gen := do
+    let n ← RandomChoice.choose 0 100 (by omega)
+    pure n.down
+
+instance : GenFor Ty (fun _ => True) where
+  gen := do
+    let n ← RandomChoice.choose 0 1 (by omega)
+    pure (if n.down == 0 then Ty.nat else Ty.bool)
+
+/-! ## Migrated genHasType (Basalt-polymorphic)
+
+This is what Specimen should emit after the migration. It mirrors the structure of
+the actual Specimen output (shown in the StatusQuo section below) with the following
+mechanical transformations:
+- `GeneratorCombinators.backtrack [(w, body)]` → `backtrack [(w, fun () => body)]`
+- `MonadExcept.throw ...` → `BacktrackGen.fail`
+- `Arbitrary.arbitrary` → `BacktrackGen.liftGen (GenFor.gen ...)`
+- `match DecOpt.decOpt ... with | Except.ok true => ... | _ => throw` →
+  `match ← DecOpt.decOpt ... with | true => ... | false => BacktrackGen.fail`
+- `return` → `pure`
+- Return type: `Plausible.Gen Expr` → `BacktrackGen G Expr`
+- Polymorphic over `[Gen G]`
+-/
+
+def genHasType [Gen G] [GenFor Nat (fun _ => True)]
+    (initSize : Nat) (τ : Ty) : (size : Nat) → BacktrackGen G Expr
+  | 0 => backtrack [
+      (1, fun () => match τ with
+        | .nat => do
+            let n ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Nat)
+            pure (Expr.lit n)
+        | _ => BacktrackGen.fail),
+      (1, fun () => match τ with
+        | .bool => do
+            let n ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Nat)
+            -- *** CHECKER (DecOpt) ***: check n ≠ 0 on already-generated n
+            match ← DecOpt.decOpt (P := ¬(n = 0)) initSize with
+            | true => pure (Expr.isPos n)
+            | false => BacktrackGen.fail
+        | _ => BacktrackGen.fail)]
+  | size + 1 => backtrack [
+      (1, fun () => match τ with
+        | .nat => do
+            let n ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Nat)
+            pure (Expr.lit n)
+        | _ => BacktrackGen.fail),
+      (1, fun () => match τ with
+        | .bool => do
+            let n ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Nat)
+            -- *** CHECKER (DecOpt) ***
+            match ← DecOpt.decOpt (P := ¬(n = 0)) initSize with
+            | true => pure (Expr.isPos n)
+            | false => BacktrackGen.fail
+        | _ => BacktrackGen.fail),
+      -- *** BACKTRACKING ***: this branch fails when τ ≠ .nat
+      (size + 1, fun () => match τ with
+        | .nat => do
+            let l ← genHasType initSize .nat size
+            let r ← genHasType initSize .nat size
+            pure (Expr.add l r)
+        | _ => BacktrackGen.fail)]
+
+/-! ## Register genHasType as a BacktrackGenFor instance -/
+
+instance [GenFor Nat (fun _ => True)]
+    : ∀ τ, BacktrackGenFor Expr (fun e => HasType e τ) :=
+  fun τ => ⟨fun {_} [_] size => genHasType size τ size⟩
+
+/-! ## Migrated genWellFormed (Basalt-polymorphic)
+
+Demonstrates the sub-generator mechanism: calls HasType via BacktrackGenFor resolution. -/
+
+def genWellFormed [Gen G] [GenFor Nat (fun _ => True)] [GenFor Ty (fun _ => True)]
+    [∀ τ, BacktrackGenFor Expr (fun e => HasType e τ)]
+    (initSize : Nat) : (size : Nat) → BacktrackGen G Prog
+  | 0 => backtrack [
+      (1, fun () => do
+        let τ ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Ty)
+        -- *** SUB-GENERATOR (BacktrackGenFor) ***
+        let e ← BacktrackGenFor.gen (P := fun e => HasType e τ) initSize
+        pure (Prog.expr e)),
+      (1, fun () => do
+        let τ ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Ty)
+        -- *** SUB-GENERATOR *** (twice, for same type)
+        let e1 ← BacktrackGenFor.gen (P := fun e => HasType e τ) initSize
+        let e2 ← BacktrackGenFor.gen (P := fun e => HasType e τ) initSize
+        pure (Prog.both e1 e2))]
+  | _size + 1 => backtrack [
+      (1, fun () => do
+        let τ ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Ty)
+        let e ← BacktrackGenFor.gen (P := fun e => HasType e τ) initSize
+        pure (Prog.expr e)),
+      (1, fun () => do
+        let τ ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Ty)
+        let e1 ← BacktrackGenFor.gen (P := fun e => HasType e τ) initSize
+        let e2 ← BacktrackGenFor.gen (P := fun e => HasType e τ) initSize
+        pure (Prog.both e1 e2))]
+
+/-! ## frequency combinator (for non-backtracking generators) -/
+
+/-- Weighted selection by interval: given `n ∈ [0, total-1]`, find the element whose weight
+    interval contains `n`. -/
+def pick (default : β) (gs : List (Nat × β)) (n : Nat) : Nat × β :=
+  match gs with
+  | [] => (0, default)
+  | (k, g) :: rest =>
+    if n < k then (k, g)
+    else pick default rest (n - k)
+
+/-- Weighted random selection without retry (matches GeneratorCombinators.frequency).
+    Picks a generator from `gs` by weight interval. Returns `default` if `gs` is empty. -/
+def frequency [Gen G] (default : G α) (gs : List (Nat × (Unit → G α))) : G α :=
+  match gs with
+  | [] => default
+  | _ => do
+    let total := sumWeights gs
+    let n ← RandomChoice.choose 0 (total - 1) (by omega)
+    (pick (fun () => default) gs n.down).snd ()
+
+/-! ## Unconstrained generator example (derive Arbitrary → GenFor) -/
+
+/-- A simple parametric binary tree to illustrate unconstrained generator derivation. -/
+inductive Tree (α : Type) where
+  | leaf
+  | node (left : Tree α) (val : α) (right : Tree α)
+  deriving Repr
+
+/-- Basalt-polymorphic unconstrained generator for Tree α.
+    This is what Specimen should emit instead of the Plausible-specific ArbitraryFueled instance. -/
+def Tree.gen [Gen G] [GenFor α (fun _ => True)] : (fuel : Nat) → G (Tree α)
+  | 0 => frequency (pure Tree.leaf) [
+      (1, fun () => pure Tree.leaf)]
+  | fuel + 1 => frequency (pure Tree.leaf) [
+      (1, fun () => pure Tree.leaf),
+      (fuel + 1, fun () => do
+        let left ← Tree.gen fuel
+        let val ← GenFor.gen (P := fun _ => True)
+        let right ← Tree.gen fuel
+        pure (Tree.node left val right))]
+
+/-- Register as a GenFor instance. -/
+instance [GenFor α (fun _ => True)] : GenFor (Tree α) (fun _ => True) where
+  gen := Tree.gen 5  -- fixed default fuel; in practice would use Gen.sized
+
+end MockBacktrack
+
+/-! ## Status quo: what Specimen actually generates today (from trace output)
+
+This is the *exact* code Specimen produces for this example, confirming the mockup above
+faithfully mirrors the structure. -/
+
+namespace StatusQuo
+open Plausible
+open MockBacktrack (Ty Expr HasType Prog WellFormed)
+
+instance : Arbitrary Ty where
+  arbitrary := do
+    let n ← Gen.choose Nat 0 1 (by omega)
+    pure (if n.val == 0 then Ty.nat else Ty.bool)
+
+instance : ArbitrarySizedSuchThat Expr (fun e => HasType e τ) where
+  arbitrarySizedST :=
+    let rec aux_arb (initSize : Nat) (size : Nat) (τ : Ty) : Plausible.Gen Expr :=
+      match size with
+      | Nat.zero =>
+        GeneratorCombinators.backtrack
+          [(1, match τ with
+            | Ty.nat => do
+              let (n : Nat) ← Arbitrary.arbitrary
+              return Expr.lit n
+            | _ => MonadExcept.throw (Plausible.GenError.genError "fail")),
+           (1, match τ with
+            | Ty.bool => do
+              let (n : Nat) ← Arbitrary.arbitrary
+              match _root_.DecOpt.decOpt (P := ¬(n = 0)) initSize with
+              | Except.ok true => return Expr.isPos n
+              | _ => MonadExcept.throw (Plausible.GenError.genError "fail")
+            | _ => MonadExcept.throw (Plausible.GenError.genError "fail"))]
+      | Nat.succ size' =>
+        GeneratorCombinators.backtrack
+          [(1, match τ with
+            | Ty.nat => do
+              let (n : Nat) ← Arbitrary.arbitrary
+              return Expr.lit n
+            | _ => MonadExcept.throw (Plausible.GenError.genError "fail")),
+           (1, match τ with
+            | Ty.bool => do
+              let (n : Nat) ← Arbitrary.arbitrary
+              match _root_.DecOpt.decOpt (P := ¬(n = 0)) initSize with
+              | Except.ok true => return Expr.isPos n
+              | _ => MonadExcept.throw (Plausible.GenError.genError "fail")
+            | _ => MonadExcept.throw (Plausible.GenError.genError "fail")),
+           (Nat.succ size', match τ with
+            | Ty.nat => do
+              let (l : Expr) ← aux_arb initSize size' Ty.nat
+              let (r : Expr) ← aux_arb initSize size' Ty.nat
+              return Expr.add l r
+            | _ => MonadExcept.throw (Plausible.GenError.genError "fail"))]
+    fun size => aux_arb size size τ
+
+instance : ArbitrarySizedSuchThat Prog (fun p => WellFormed p) where
+  arbitrarySizedST :=
+    let rec aux_arb (initSize : Nat) (size : Nat) : Plausible.Gen Prog :=
+      match size with
+      | Nat.zero =>
+        GeneratorCombinators.backtrack
+          [(1, do
+            let (τ : Ty) ← Arbitrary.arbitrary
+            let (e : Expr) ← @ArbitrarySizedSuchThat.arbitrarySizedST _ (fun e => HasType e τ) _ initSize
+            return Prog.expr e),
+           (1, do
+            let (τ : Ty) ← Arbitrary.arbitrary
+            let (e1 : Expr) ← @ArbitrarySizedSuchThat.arbitrarySizedST _ (fun e => HasType e τ) _ initSize
+            let (e2 : Expr) ← @ArbitrarySizedSuchThat.arbitrarySizedST _ (fun e => HasType e τ) _ initSize
+            return Prog.both e1 e2)]
+      | Nat.succ _size' =>
+        GeneratorCombinators.backtrack
+          [(1, do
+            let (τ : Ty) ← Arbitrary.arbitrary
+            let (e : Expr) ← @ArbitrarySizedSuchThat.arbitrarySizedST _ (fun e => HasType e τ) _ initSize
+            return Prog.expr e),
+           (1, do
+            let (τ : Ty) ← Arbitrary.arbitrary
+            let (e1 : Expr) ← @ArbitrarySizedSuchThat.arbitrarySizedST _ (fun e => HasType e τ) _ initSize
+            let (e2 : Expr) ← @ArbitrarySizedSuchThat.arbitrarySizedST _ (fun e => HasType e τ) _ initSize
+            return Prog.both e1 e2)]
+    fun size => aux_arb size size
+
+end StatusQuo
+
+/-! ## Execution -/
+
+open MockBacktrack
+
+#eval do
+  IO.println "=== genHasType (τ = .bool, size = 5) — isPos with DecOpt n≠0 check ==="
+  for _ in List.range 8 do
+    let result ← Plausible.Gen.run
+      (BacktrackGen.toPlausibleGen (genHasType (G := Plausible.Gen) 5 .bool 5)) 10
+    IO.println s!"  {repr result}"
+
+#eval do
+  IO.println "=== genHasType (τ = .nat, size = 3) — lit and add, with backtracking ==="
+  for _ in List.range 5 do
+    let result ← Plausible.Gen.run
+      (BacktrackGen.toPlausibleGen (genHasType (G := Plausible.Gen) 3 .nat 3)) 10
+    IO.println s!"  {repr result}"
+
+#eval do
+  IO.println "=== genWellFormed (size = 3) — sub-generator calls into HasType ==="
+  for _ in List.range 5 do
+    let result : Prog ← Plausible.Gen.run
+      (BacktrackGen.toPlausibleGen (genWellFormed (G := Plausible.Gen) 3 3)) 10
+    IO.println s!"  {repr result}"
+
+-- Also run the status-quo version to confirm both produce the same kinds of output
+#eval do
+  IO.println "=== StatusQuo HasType (τ = .bool, size = 5) ==="
+  for _ in List.range 5 do
+    let inst : ArbitrarySizedSuchThat Expr (fun e => HasType e .bool) := inferInstance
+    let result ← Plausible.Gen.run (inst.arbitrarySizedST 5) 10
+    IO.println s!"  {repr result}"
+
+/-! ## Status quo: what Specimen emits today for unconstrained generators -/
+namespace UnconstrainedStatusQuo
+open Plausible
+open MockBacktrack (Tree)
+
+instance [Arbitrary α] : ArbitraryFueled (Tree α) where
+  arbitraryFueled :=
+    let rec aux_arb (fuel : Nat) : Plausible.Gen (Tree α) :=
+      match fuel with
+      | Nat.zero => Gen.oneOfWithDefault (pure Tree.leaf) [pure Tree.leaf]
+      | fuel' + 1 => Gen.frequency (pure Tree.leaf)
+          [(1, pure Tree.leaf),
+           (fuel' + 1, do
+              let left ← aux_arb fuel'
+              let val ← Arbitrary.arbitrary
+              let right ← aux_arb fuel'
+              return Tree.node left val right)]
+    fun fuel => aux_arb fuel
+
+end UnconstrainedStatusQuo
+
+-- Run the migrated unconstrained generator
+#eval do
+  IO.println "=== Tree.gen (fuel = 3) ==="
+  for _ in List.range 5 do
+    let result ← Plausible.Gen.run (Tree.gen (G := Plausible.Gen) (α := Nat) 3) 10
+    IO.println s!"  {repr result}"
diff --git a/SpecimenTest/BasaltPort/BridgeBenchmark.lean b/SpecimenTest/BasaltPort/BridgeBenchmark.lean
new file mode 100644
index 0000000..5229d38
--- /dev/null
+++ b/SpecimenTest/BasaltPort/BridgeBenchmark.lean
@@ -0,0 +1,509 @@
+import Plausible
+import Specimen.DecOpt
+import Specimen.ArbitrarySizedSuchThat
+import Specimen.GeneratorCombinators
+
+/-!
+# Benchmark: Legacy Specimen generators vs Basalt-bridge BacktrackGen
+
+This file provides an apples-to-apples performance comparison between:
+- **Legacy**: exception-based backtracking via `GeneratorCombinators.backtrack`
+- **Bridge**: Option-based backtracking via `BacktrackGen` (Basalt approach)
+
+Both versions generate the same set of values for the same size parameter.
+The leaf Nat generator uses a fixed range [0, 100] in both versions to ensure equivalence.
+-/
+
+open Lean.Order
+
+namespace BridgeBenchmark
+
+/-! ## Shared definitions -/
+
+inductive Ty | nat | bool
+  deriving Repr, Inhabited, BEq, DecidableEq
+
+inductive Expr
+  | lit (n : Nat)
+  | isPos (n : Nat)
+  | nary (a b c d e : Expr)
+  deriving Repr, Inhabited
+
+inductive HasType : Expr → Ty → Prop
+  | lit (n) : HasType (.lit n) .nat
+  | isPos (n) : n ≠ 0 → HasType (.isPos n) .bool
+  | nary (a b c d e) : HasType a .nat → HasType b .nat → HasType c .nat →
+      HasType d .nat → HasType e .nat → HasType (.nary a b c d e) .nat
+
+/-- Fixed-range Nat generator for the legacy side (matches bridge's [0,100] range). -/
+private def genNatLegacy : Plausible.Gen Nat := do
+  let ⟨n, _⟩ ← Plausible.Gen.choose Nat 0 100 (by omega)
+  pure n
+
+/-! ## Legacy (exception-based) -/
+
+namespace Legacy
+
+/-- The exact code pattern Specimen emits today, using exception-based backtracking.
+    Uses `genNatLegacy` (fixed [0,100]) instead of `Arbitrary.arbitrary` for equivalence. -/
+@[specialize] def genHasType (initSize : Nat) (size : Nat) (τ : Ty) : Plausible.Gen Expr :=
+  match size with
+  | 0 =>
+    GeneratorCombinators.backtrack
+      [(1, match τ with
+        | .nat => do
+          let n ← genNatLegacy
+          return Expr.lit n
+        | _ => MonadExcept.throw (.genError "fail")),
+       (1, match τ with
+        | .bool => do
+          let n ← genNatLegacy
+          match @DecOpt.decOpt (¬(n = 0)) _ initSize with
+          | .ok true => return Expr.isPos n
+          | _ => MonadExcept.throw (.genError "fail")
+        | _ => MonadExcept.throw (.genError "fail"))]
+  | size' + 1 =>
+    GeneratorCombinators.backtrack
+      [(1, match τ with
+        | .nat => do
+          let n ← genNatLegacy
+          return Expr.lit n
+        | _ => MonadExcept.throw (.genError "fail")),
+       (1, match τ with
+        | .bool => do
+          let n ← genNatLegacy
+          match @DecOpt.decOpt (¬(n = 0)) _ initSize with
+          | .ok true => return Expr.isPos n
+          | _ => MonadExcept.throw (.genError "fail")
+        | _ => MonadExcept.throw (.genError "fail")),
+       (size' + 1, match τ with
+        | .nat => do
+          let a ← genHasType initSize size' .nat
+          let b ← genHasType initSize size' .nat
+          let c ← genHasType initSize size' .nat
+          let d ← genHasType initSize size' .nat
+          let e ← genHasType initSize size' .nat
+          return Expr.nary a b c d e
+        | _ => MonadExcept.throw (.genError "fail"))]
+
+def run (τ : Ty) (size : Nat) : Plausible.Gen Expr :=
+  genHasType size size τ
+
+end Legacy
+
+/-! ## Bridge (Option-based BacktrackGen) -/
+
+namespace Bridge
+
+/-! ### Basalt infrastructure (minimal, for benchmarking) -/
+
+class RandomChoice (m : Type u → Type v) where
+  choose : (lo hi : Nat) → (h : lo ≤ hi) → m (ULift Nat)
+
+class Gen (g : Type u → Type v) where
+  instInhabited : ∀ α, Inhabited (g α)
+  instMonad : Monad g
+  instRandomChoice : RandomChoice g
+  instCCPO : ∀ α, CCPO (g α)
+  instMonoBind : MonoBind g
+
+instance [m : Gen g] : ∀ α, Inhabited (g α) := m.instInhabited
+instance [m : Gen g] : Monad g := m.instMonad
+instance [m : Gen g] : RandomChoice g := m.instRandomChoice
+instance [m : Gen g] : ∀ α, CCPO (g α) := m.instCCPO
+instance [m : Gen g] : MonoBind g := m.instMonoBind
+
+private instance : PartialOrder (Except Plausible.GenError α) :=
+  FlatOrder.instOrder (b := Except.error default)
+
+private instance : CCPO (Except Plausible.GenError α) :=
+  FlatOrder.instCCPO (b := Except.error default)
+
+private instance : MonoBind (Except Plausible.GenError) where
+  bind_mono_left h := by
+    cases h with
+    | bot => exact FlatOrder.rel.bot
+    | refl => exact FlatOrder.rel.refl
+  bind_mono_right h := by
+    cases ‹Except Plausible.GenError _› with
+    | error => exact FlatOrder.rel.refl
+    | ok a => exact h a
+
+private instance : RandomChoice Plausible.Gen where
+  choose lo hi h := do
+    let ⟨val, _⟩ ← Plausible.Gen.choose Nat lo hi h
+    pure ⟨val⟩
+
+instance : Gen Plausible.Gen where
+  instInhabited := inferInstance
+  instMonad := inferInstance
+  instRandomChoice := inferInstance
+  instCCPO := inferInstance
+  instMonoBind := inferInstance
+
+/-! ### BacktrackGen -/
+
+structure BacktrackGen (G : Type → Type) (α : Type) where
+  run : G (Option α)
+
+namespace BacktrackGen
+
+@[inline] def bind' [Gen G] (x : BacktrackGen G α) (f : α → BacktrackGen G β) : BacktrackGen G β :=
+  ⟨do match ← x.run with
+      | some a => (f a).run
+      | none => pure none⟩
+
+instance [Gen G] : Monad (BacktrackGen G) where
+  pure a := ⟨pure (some a)⟩
+  bind := bind'
+
+instance [Gen G] : Inhabited (BacktrackGen G α) where
+  default := ⟨pure none⟩
+
+@[inline] def liftGen [Gen G] (g : G α) : BacktrackGen G α :=
+  ⟨do let a ← g; pure (some a)⟩
+
+@[inline] def fail [Gen G] : BacktrackGen G α :=
+  ⟨pure none⟩
+
+def toPlausibleGen (x : BacktrackGen Plausible.Gen α) : Plausible.Gen α := do
+  match ← x.run with
+  | some a => pure a
+  | none => throw (.genError "backtracking exhausted")
+
+end BacktrackGen
+
+/-! ### backtrack combinator -/
+
+/-- Sum of weights in a weighted generator list. -/
+def sumWeights (gs : List (Nat × β)) : Nat :=
+  gs.map Prod.fst |>.sum
+
+/-- Weighted selection with drop: given `n ∈ [0, total-1]`, find the element whose weight
+    interval contains `n`, return its weight, the element, and the remaining list. -/
+def pickDrop [Inhabited β] (gs : List (Nat × β)) (n : Nat) : Nat × β × List (Nat × β) :=
+  match gs with
+  | [] => (0, default, [])
+  | (k, g) :: rest =>
+    if n < k then (k, g, rest)
+    else
+      let (k', g', rest') := pickDrop rest (n - k)
+      (k', g', (k, g) :: rest')
+
+/-- Weighted backtracking: randomly pick a branch by weight, try it, retry remaining on failure.
+    Uses fuel (initially gs.length) for termination, matching Specimen's backtrackFuel. -/
+def backtrack [Gen G] (gs : List (Nat × (Unit → BacktrackGen G α))) : BacktrackGen G α :=
+  ⟨go gs.length (sumWeights gs) gs⟩
+where
+  go : Nat → Nat → List (Nat × (Unit → BacktrackGen G α)) → G (Option α)
+  | _, _, [] => pure none
+  | 0, _, _ => pure none
+  | fuel + 1, total, gs@(_ :: _) => do
+    let n ← RandomChoice.choose 0 (total - 1) (by omega)
+    let (k, g, gs') := pickDrop gs n.down
+    match ← (g ()).run with
+    | some a => pure (some a)
+    | none => go fuel (total - k) gs'
+
+/-! ### GenFor and DecOpt -/
+
+class GenFor (α : Type) (P : α → Prop) where
+  gen : ∀ {G : Type → Type} [Gen G], G α
+
+class BDecOpt (P : Prop) where
+  decOpt : ∀ {G : Type → Type} [Gen G], Nat → BacktrackGen G Bool
+
+instance (priority := low) [Decidable P] : BDecOpt P where
+  decOpt _ := pure (decide P)
+
+/-- Fixed-range [0,100] Nat generator, matching the legacy side. -/
+instance : GenFor Nat (fun _ => True) where
+  gen := do
+    let n ← RandomChoice.choose 0 100 (by omega)
+    pure n.down
+
+/-! ### The bridge generator -/
+
+@[specialize] def genHasType [Gen G] [GenFor Nat (fun _ => True)]
+    (initSize : Nat) (τ : Ty) : (size : Nat) → BacktrackGen G Expr
+  | 0 => backtrack [
+      (1, fun () => match τ with
+        | .nat => do
+            let n ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Nat)
+            pure (Expr.lit n)
+        | _ => BacktrackGen.fail),
+      (1, fun () => match τ with
+        | .bool => do
+            let n ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Nat)
+            match ← BDecOpt.decOpt (P := ¬(n = 0)) initSize with
+            | true => pure (Expr.isPos n)
+            | false => BacktrackGen.fail
+        | _ => BacktrackGen.fail)]
+  | size + 1 => backtrack [
+      (1, fun () => match τ with
+        | .nat => do
+            let n ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Nat)
+            pure (Expr.lit n)
+        | _ => BacktrackGen.fail),
+      (1, fun () => match τ with
+        | .bool => do
+            let n ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Nat)
+            match ← BDecOpt.decOpt (P := ¬(n = 0)) initSize with
+            | true => pure (Expr.isPos n)
+            | false => BacktrackGen.fail
+        | _ => BacktrackGen.fail),
+      (size + 1, fun () => match τ with
+        | .nat => do
+            let a ← genHasType initSize .nat size
+            let b ← genHasType initSize .nat size
+            let c ← genHasType initSize .nat size
+            let d ← genHasType initSize .nat size
+            let e ← genHasType initSize .nat size
+            pure (Expr.nary a b c d e)
+        | _ => BacktrackGen.fail)]
+
+def run (τ : Ty) (size : Nat) : Plausible.Gen Expr :=
+  BacktrackGen.toPlausibleGen (genHasType (G := Plausible.Gen) size τ size)
+
+end Bridge
+
+/-! ## Benchmark harness -/
+
+/-- Run a generator `n` times, discarding failures, return elapsed ms. -/
+def timeGen (gen : Plausible.Gen Expr) (n : Nat) (runSize : Nat) : IO Nat := do
+  let t0 ← IO.monoMsNow
+  for _ in List.range n do
+    try
+      let _ ← Plausible.Gen.run gen runSize
+    catch _ => pure ()
+  let t1 ← IO.monoMsNow
+  pure (t1 - t0)
+
+/-- Run benchmark at a given recursion size, comparing legacy vs bridge. -/
+def benchAtSize (size : Nat) (iters : Nat) (τ : Ty) : IO Unit := do
+  -- Warm up
+  for _ in List.range 100 do
+    try let _ ← Plausible.Gen.run (Legacy.run τ size) 10 catch _ => pure ()
+    try let _ ← Plausible.Gen.run (Bridge.run τ size) 10 catch _ => pure ()
+
+  let legacyMs ← timeGen (Legacy.run τ size) iters 10
+  let bridgeMs ← timeGen (Bridge.run τ size) iters 10
+
+  let ratio := if legacyMs == 0 then "∞" else s!"{(bridgeMs * 100) / legacyMs}%"
+  IO.println s!"  size={size}: legacy={legacyMs}ms, bridge={bridgeMs}ms, ratio(bridge/legacy)={ratio}"
+
+/-! ## Main benchmark -/
+
+#eval do
+  let iters := 2000
+  IO.println s!"=== A/B Benchmark: Legacy vs Bridge (HasType, {iters} iterations) ==="
+  IO.println ""
+
+  IO.println "--- τ = .nat (all branches succeed, exercises recursion) ---"
+  for size in [2, 3, 4] do
+    benchAtSize size iters .nat
+
+  IO.println ""
+  IO.println "--- τ = .bool (isPos branch only, exercises backtracking + DecOpt check) ---"
+  for size in [2, 3, 4] do
+    benchAtSize size iters .bool
+
+/-! ## Microbenchmark: stress backtracking (multiple branch retries)
+
+The interesting case for backtracking overhead is when multiple branches are tried
+and fail before one succeeds. Each failed branch does real work (generates values,
+checks conditions) before failing. This exercises:
+- The retry loop (picking a new branch after failure)
+- Failure propagation through nested binds within a branch
+
+We set up 5 branches where the first 4 always fail (after doing some work)
+and only the last one can succeed. With weight-based selection, the failing
+branches are tried first with high probability.
+-/
+
+namespace StressBacktrack
+
+private def genNat100Legacy : Plausible.Gen Nat := do
+  let ⟨n, _⟩ ← Plausible.Gen.choose Nat 0 100 (by omega)
+  pure n
+
+/-- Legacy: 5 branches with heavy weights on the failing ones.
+    Each failing branch generates 5 Nats (simulating liftGen work) before failing. -/
+@[specialize] def legacyMultiBranch (initSize : Nat) : Plausible.Gen Expr :=
+  GeneratorCombinators.backtrack
+    [(10, do
+      let a ← genNat100Legacy
+      let _ ← genNat100Legacy
+      let _ ← genNat100Legacy
+      let _ ← genNat100Legacy
+      let _ ← genNat100Legacy
+      if a + 1 == 999 then return Expr.lit a
+      else MonadExcept.throw (.genError "fail")),
+     (10, do
+      let a ← genNat100Legacy
+      let _ ← genNat100Legacy
+      let _ ← genNat100Legacy
+      let _ ← genNat100Legacy
+      let _ ← genNat100Legacy
+      if a + 2 == 999 then return Expr.lit a
+      else MonadExcept.throw (.genError "fail")),
+     (10, do
+      let a ← genNat100Legacy
+      let _ ← genNat100Legacy
+      let _ ← genNat100Legacy
+      let _ ← genNat100Legacy
+      let _ ← genNat100Legacy
+      if a + 3 == 999 then return Expr.lit a
+      else MonadExcept.throw (.genError "fail")),
+     (10, do
+      let a ← genNat100Legacy
+      let _ ← genNat100Legacy
+      let _ ← genNat100Legacy
+      let _ ← genNat100Legacy
+      let _ ← genNat100Legacy
+      if a + 4 == 999 then return Expr.lit a
+      else MonadExcept.throw (.genError "fail")),
+     (1, do
+      let n ← genNat100Legacy
+      match @DecOpt.decOpt (¬(n = 0)) _ initSize with
+      | .ok true => return Expr.isPos n
+      | _ => return Expr.isPos 1)]
+
+/-- Bridge (unbatched): 5 separate liftGens per failing branch. -/
+@[specialize] def bridgeMultiBranch [Bridge.Gen G] [Bridge.GenFor Nat (fun _ => True)]
+    (initSize : Nat) : Bridge.BacktrackGen G Expr :=
+  Bridge.backtrack
+    [(10, fun () => do
+      let a ← Bridge.BacktrackGen.liftGen (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+      let _ ← Bridge.BacktrackGen.liftGen (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+      let _ ← Bridge.BacktrackGen.liftGen (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+      let _ ← Bridge.BacktrackGen.liftGen (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+      let _ ← Bridge.BacktrackGen.liftGen (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+      if a + 1 == 999 then pure (Expr.lit a)
+      else Bridge.BacktrackGen.fail),
+     (10, fun () => do
+      let a ← Bridge.BacktrackGen.liftGen (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+      let _ ← Bridge.BacktrackGen.liftGen (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+      let _ ← Bridge.BacktrackGen.liftGen (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+      let _ ← Bridge.BacktrackGen.liftGen (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+      let _ ← Bridge.BacktrackGen.liftGen (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+      if a + 2 == 999 then pure (Expr.lit a)
+      else Bridge.BacktrackGen.fail),
+     (10, fun () => do
+      let a ← Bridge.BacktrackGen.liftGen (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+      let _ ← Bridge.BacktrackGen.liftGen (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+      let _ ← Bridge.BacktrackGen.liftGen (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+      let _ ← Bridge.BacktrackGen.liftGen (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+      let _ ← Bridge.BacktrackGen.liftGen (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+      if a + 3 == 999 then pure (Expr.lit a)
+      else Bridge.BacktrackGen.fail),
+     (10, fun () => do
+      let a ← Bridge.BacktrackGen.liftGen (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+      let _ ← Bridge.BacktrackGen.liftGen (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+      let _ ← Bridge.BacktrackGen.liftGen (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+      let _ ← Bridge.BacktrackGen.liftGen (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+      let _ ← Bridge.BacktrackGen.liftGen (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+      if a + 4 == 999 then pure (Expr.lit a)
+      else Bridge.BacktrackGen.fail),
+     (1, fun () => do
+      let n ← Bridge.BacktrackGen.liftGen (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+      match ← Bridge.BDecOpt.decOpt (P := ¬(n = 0)) initSize with
+      | true => pure (Expr.isPos n)
+      | false => pure (Expr.isPos 1))]
+
+/-- Bridge (batched): consecutive liftGens grouped into one lift. -/
+@[specialize] def bridgeMultiBranchBatched [Bridge.Gen G] [Bridge.GenFor Nat (fun _ => True)]
+    (initSize : Nat) : Bridge.BacktrackGen G Expr :=
+  Bridge.backtrack
+    [(10, fun () => do
+      let (a, _, _, _, _) ← Bridge.BacktrackGen.liftGen (do
+        let a ← (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+        let b ← (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+        let c ← (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+        let d ← (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+        let e ← (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+        pure (a, b, c, d, e))
+      if a + 1 == 999 then pure (Expr.lit a)
+      else Bridge.BacktrackGen.fail),
+     (10, fun () => do
+      let (a, _, _, _, _) ← Bridge.BacktrackGen.liftGen (do
+        let a ← (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+        let b ← (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+        let c ← (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+        let d ← (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+        let e ← (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+        pure (a, b, c, d, e))
+      if a + 2 == 999 then pure (Expr.lit a)
+      else Bridge.BacktrackGen.fail),
+     (10, fun () => do
+      let (a, _, _, _, _) ← Bridge.BacktrackGen.liftGen (do
+        let a ← (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+        let b ← (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+        let c ← (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+        let d ← (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+        let e ← (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+        pure (a, b, c, d, e))
+      if a + 3 == 999 then pure (Expr.lit a)
+      else Bridge.BacktrackGen.fail),
+     (10, fun () => do
+      let (a, _, _, _, _) ← Bridge.BacktrackGen.liftGen (do
+        let a ← (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+        let b ← (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+        let c ← (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+        let d ← (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+        let e ← (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+        pure (a, b, c, d, e))
+      if a + 4 == 999 then pure (Expr.lit a)
+      else Bridge.BacktrackGen.fail),
+     (1, fun () => do
+      let n ← Bridge.BacktrackGen.liftGen (Bridge.GenFor.gen (P := fun _ => True) : G Nat)
+      match ← Bridge.BDecOpt.decOpt (P := ¬(n = 0)) initSize with
+      | true => pure (Expr.isPos n)
+      | false => pure (Expr.isPos 1))]
+
+end StressBacktrack
+
+#eval do
+  let iters := 10000
+  IO.println s!""
+  IO.println s!"=== Stress Backtrack: 5 branches, 4 always fail after work, {iters} iters ==="
+
+  let t0 ← IO.monoMsNow
+  for _ in List.range iters do
+    try let _ ← Plausible.Gen.run (StressBacktrack.legacyMultiBranch 5) 10 catch _ => pure ()
+  let t1 ← IO.monoMsNow
+
+  let t2 ← IO.monoMsNow
+  for _ in List.range iters do
+    try
+      let _ ← Plausible.Gen.run
+        (Bridge.BacktrackGen.toPlausibleGen
+          (StressBacktrack.bridgeMultiBranch (G := Plausible.Gen) 5)) 10
+    catch _ => pure ()
+  let t3 ← IO.monoMsNow
+
+  let t4 ← IO.monoMsNow
+  for _ in List.range iters do
+    try
+      let _ ← Plausible.Gen.run
+        (Bridge.BacktrackGen.toPlausibleGen
+          (StressBacktrack.bridgeMultiBranchBatched (G := Plausible.Gen) 5)) 10
+    catch _ => pure ()
+  let t5 ← IO.monoMsNow
+
+  let legacyMs := t1 - t0
+  let bridgeMs := t3 - t2
+  let batchedMs := t5 - t4
+  let ratio := if legacyMs == 0 then "∞" else s!"{(bridgeMs * 100) / legacyMs}%"
+  let ratioBatched := if legacyMs == 0 then "∞" else s!"{(batchedMs * 100) / legacyMs}%"
+  IO.println s!"  legacy={legacyMs}ms, bridge={bridgeMs}ms ({ratio}), bridge-batched={batchedMs}ms ({ratioBatched})"
+
+/-! ## IR inspection
+
+To check newtype erasure and specialization, uncomment and build separately:
+  set_option trace.compiler.ir.result true in
+  def inspectIR : Plausible.Gen Expr :=
+    Bridge.BacktrackGen.toPlausibleGen (Bridge.genHasType (G := Plausible.Gen) 3 .nat 3)
+-/
+
+end BridgeBenchmark