From 4b9633b986df17d18db5b787127d1dd41bb699db Mon Sep 17 00:00:00 2001 From: Mike Hicks Date: Tue, 2 Jun 2026 20:20:21 -0400 Subject: [PATCH 1/8] plan to bridge specimen to basalt, and some mockups --- SPECIMEN-BASALT-BRIDGE.md | 804 ++++++++++++++++++++++++--- SpecimenTest/BridgeDecOptMockup.lean | 157 ++++++ SpecimenTest/BridgeMockup.lean | 333 +++++++++++ 3 files changed, 1205 insertions(+), 89 deletions(-) create mode 100644 SpecimenTest/BridgeDecOptMockup.lean create mode 100644 SpecimenTest/BridgeMockup.lean diff --git a/SPECIMEN-BASALT-BRIDGE.md b/SPECIMEN-BASALT-BRIDGE.md index 1ebef4d..497e4fe 100644 --- a/SPECIMEN-BASALT-BRIDGE.md +++ b/SPECIMEN-BASALT-BRIDGE.md @@ -2,7 +2,9 @@ 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 +A glossary of terms appears at the end, for quick reference. + +## 1. Status Quo and Goal ### The three frameworks @@ -27,83 +29,264 @@ class Gen (g : Type u → Type v) where ``` 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 + ### Current dependency structure ``` -Plausible ← Specimen (Specimen emits Plausible.Gen terms) -Plausible ← Basalt (PlausibleGen makes Plausible.Gen a Basalt Gen instance) +┌──────────┐ ┌──────────┐ +│ Plausible│◄────────│ Specimen │ +└────┬─────┘ └──────────┘ + │ + ▼ +┌──────────┐ +│ Basalt │ +└──────────┘ ``` Specimen and Basalt are currently unrelated — Specimen-derived generators cannot be reasoned about using Basalt's correctness classes. -### The problem +### Target dependency structure + +``` +┌──────────┐ +│ Plausible│ +└────┬─────┘ + │ + ▼ +┌──────────┐ ┌──────────┐ +│ Basalt │◄────────│ Specimen │ +└──────────┘ └──────────┘ +``` + +Specimen will depend on Basalt for `Gen`, `BacktrackGen`, and `backtrack`. The `plausible` tactic will still work: Specimen emits `ArbitrarySizedSuchThat` instances (as it does today) whose body calls `BacktrackGen.toPlausibleGen` to produce the `Plausible.Gen α` that Plausible's machinery expects. + +### The goal + +We want Specimen-derived generators to be **polymorphic over Basalt's `Gen` class** so they can be: +- **Executed** via `Plausible.Gen` (as today) +- **Proved sound/complete** at `SetGen.Set` + +### Non-goals + +The following are explicitly **not** addressed by this plan: + +- **Changing user-facing syntax.** The `derive_generator (fun τ => ∃ e, HasType e τ)` command syntax remains unchanged. The difference is purely in what code gets emitted. +- **Enumerators.** Specimen's deterministic enumerators (`EnumSizedSuchThat`) are a separate concern from random generators and are not addressed here. (But we should address them similarly.) +- **Almost-sure termination proofs for derived generators.** Phase 2 proves soundness/completeness only. Termination and cost bounds for Specimen-derived generators are future work (they would require `partial_fixpoint`-based emission). + +### Example + +We will use the following small typed language throughout this document to illustrate the changes. (Note: the `letBind` form is a simplification — the bound variable is never referenced in the body. This is intentional; the example is designed to show cross-generator composition, not to be a realistic language.) + +```lean +inductive Ty | nat | bool + +inductive Expr + | litNat (n : Nat) + | litBool (b : Bool) + | isZero (e : Expr) + +inductive Stmt + | expr (e : Expr) + | letBind (x : Nat) (e : Expr) (body : Stmt) + | assert (e : Expr) (τ : Ty) + +inductive HasType : Expr → Ty → Prop + | litNat (n : Nat) : HasType (.litNat n) .nat + | litBool (b : Bool) : HasType (.litBool b) .bool + | isZero (e : Expr) : HasType e .nat → HasType (.isZero e) .bool + +inductive WellTypedStmt : Stmt → Prop + | expr (e : Expr) (τ : Ty) : HasType e τ → WellTypedStmt (.expr e) + | letBind (x : Nat) (e : Expr) (body : Stmt) (τ : Ty) : + HasType e τ → WellTypedStmt body → WellTypedStmt (.letBind x e body) + | assert (e : Expr) (τ : Ty) : HasType e τ → WellTypedStmt (.assert e τ) +``` + +To get generators, a user invokes Specimen (this syntax will not change): + +```lean +derive_generator (fun τ => ∃ e, HasType e τ) +derive_generator (fun _ => ∃ s, WellTypedStmt s) +``` + +### 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.litNat n + | _ => MonadExcept.throw Gen.genericFailure), + (1, match τ with + | Ty.bool => do let b ← Arbitrary.arbitrary; return Expr.litBool b + | _ => MonadExcept.throw Gen.genericFailure)] + | Nat.succ size' => + GeneratorCombinators.backtrack + [(1, match τ with + | Ty.nat => do let n ← Arbitrary.arbitrary; return Expr.litNat n + | _ => MonadExcept.throw Gen.genericFailure), + (1, match τ with + | Ty.bool => do let b ← Arbitrary.arbitrary; return Expr.litBool b + | _ => MonadExcept.throw Gen.genericFailure), + (Nat.succ size', match τ with + | Ty.bool => do let e ← aux_arb initSize size' Ty.nat; return Expr.isZero e + | _ => MonadExcept.throw Gen.genericFailure)] + fun size => aux_arb size size τ +``` + +For `WellTypedStmt`, Specimen produces a generator that calls the `HasType` generator **via typeclass resolution** (`ArbitrarySizedSuchThat.arbitrarySizedST`): + +```lean +instance : ArbitrarySizedSuchThat Stmt (fun s => WellTypedStmt s) where + arbitrarySizedST := + let rec aux_arb (initSize : Nat) (size : Nat) : Plausible.Gen Stmt := + match size with + | Nat.zero => + GeneratorCombinators.backtrack + [(1, do let τ ← Arbitrary.arbitrary + let e ← @ArbitrarySizedSuchThat.arbitrarySizedST _ (fun e => HasType e τ) _ initSize + return Stmt.expr e), + (1, do let τ ← Arbitrary.arbitrary + let e ← @ArbitrarySizedSuchThat.arbitrarySizedST _ (fun e => HasType e τ) _ initSize + return Stmt.assert e τ)] + | Nat.succ size' => + GeneratorCombinators.backtrack + [(1, do let τ ← Arbitrary.arbitrary + let e ← @ArbitrarySizedSuchThat.arbitrarySizedST _ (fun e => HasType e τ) _ initSize + return Stmt.expr e), + (1, do let τ ← Arbitrary.arbitrary + let e ← @ArbitrarySizedSuchThat.arbitrarySizedST _ (fun e => HasType e τ) _ initSize + return Stmt.assert e τ), + (Nat.succ size', do + let body ← aux_arb initSize size' + let τ ← Arbitrary.arbitrary + let e ← @ArbitrarySizedSuchThat.arbitrarySizedST _ (fun e => HasType e τ) _ initSize + let x ← Arbitrary.arbitrary + return Stmt.letBind x e body)] + 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 four problems: + +**Problem 1: Backtracking.** The generators use Plausible's `throw`/`tryCatch` for backtracking. Basalt's `Gen` class has no exception mechanism — only `choose`, `bind`, `pure`, and ⊥ (`default`). We need a backtracking mechanism that works across all Basalt interpretations. (Addressed in Section 2.) + +**Problem 2: Sub-generator resolution.** The generators call sub-generators via Plausible-specific typeclasses (`Arbitrary`, `ArbitrarySizedSuchThat`). These typeclasses wrap `Plausible.Gen` and cannot be used polymorphically over `G`. We need a Basalt-compatible typeclass for sub-generator lookup. (Addressed in Section 3.) -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. +**Problem 3: Checkers.** In more complex examples, Specimen invokes `DecOpt.decOpt` within generators to check hypotheses that involve only fixed (input) variables. `DecOpt.decOpt` returns `Except GenError Bool` — a Plausible-specific type. Checkers must also be made polymorphic over `G`. (Addressed in Section 5. Our running example does not trigger this, but it arises frequently in practice — e.g., checking `n < m` or type equality after both sides are determined.) -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. +**Problem 4: Unconstrained generators.** Specimen's `derive Arbitrary` emits generators using Plausible-specific `Gen.frequency` / `Gen.oneOfWithDefault` and `Arbitrary.arbitrary`. These must also become Basalt-polymorphic so they can serve as provably-correct `GenFor` instances for sub-generator resolution in constrained generators. (Addressed in Section 6.) -## 2. The Change: `BacktrackGen` +## 2. Solving Problem 1: `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 α) +/-- A backtracking generator: wraps G (Option α) where none = local failure, some = success. + Defined as a structure (not a type alias) so it can have its own Monad instance, + enabling do-notation within backtracking generators. -/ +structure BacktrackGen (G : Type → Type) (α : Type) 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. +`BacktrackGen` is a `structure` (newtype) rather than a type alias so that it can have its own `Monad` instance. This allows `do`-notation within backtracking generators to bind `BacktrackGen G` values directly, threading `Option` automatically: + +```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 /-- 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 + ⟨go gs⟩ where - go (total : Nat) : List (Nat × (Unit → BacktrackGen G α)) → BacktrackGen G α + go : List (Nat × (Unit → BacktrackGen G α)) → G (Option α) | [] => pure none + | [(_, g)] => (g ()).run | gs => do - let n ← choose 0 (total - 1) (by omega) - let (k, g, rest) := pickDrop gs n - match ← g () with + let idx ← RandomChoice.choose 0 (gs.length - 1) (by omega) + let (_, g) := gs[idx.down]! + match ← (g ()).run with | some a => pure (some a) - | none => go (total - k) rest + | none => go (gs.eraseIdx idx.down) + termination_by gs => gs.length ``` 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. +### The `frequency` combinator + +For **non-backtracking** generators (like unconstrained `Arbitrary` derivations that use `Gen.frequency`), we provide a simpler combinator that picks by weight but does *not* retry on failure: + +```lean +/-- Weighted random selection without retry. For non-backtracking generators. -/ +def frequency [Gen G] (default : G α) (gs : List (Nat × (Unit → G α))) : G α := + match gs with + | [] => default + | [(_, g)] => g () + | gs => do + let idx ← RandomChoice.choose 0 (gs.length - 1) (by omega) + let (_, g) := gs[idx.down]! + g () +``` + +This is the Basalt-polymorphic replacement for `Plausible.Gen.frequency` / `Gen.oneOfWithDefault`. + +### The `liftGen` and `fail` 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` 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 +def BacktrackGen.toGen [Gen G] [Inhabited α] (g : BacktrackGen G α) : G α := do + match ← g.run with | some a => pure a - | none => default -- ⊥ (divergence) + | none => pure default -- ⊥ (divergence) def BacktrackGen.toPlausibleGen (g : BacktrackGen Plausible.Gen α) : Plausible.Gen α := do - match ← g with + match ← g.run 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. +### Why a structure (newtype)? -### Composability +`BacktrackGen` is defined as a `structure` wrapping `G (Option α)` rather than a type alias for two reasons: -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)) -``` +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. -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. +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 — making the generated code verbose and error-prone. ### Interpretations across Basalt instances @@ -114,123 +297,566 @@ Failure information is only lost at the outermost boundary (`toPlausibleGen`). T | `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 +Note: `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. -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. +## 3. Solving Problem 2: Sub-generator Resolution -### New dependency structure +Today, Specimen resolves sub-generators via Plausible's `Arbitrary` typeclass (for unconstrained types like `Nat`) and `ArbitrarySizedSuchThat` (for constrained types like well-typed expressions). But `Arbitrary` wraps `Plausible.Gen α` specifically — it cannot be used inside a polymorphic `G`. +We need a Basalt-compatible typeclass mechanism that: + +1. Works at all Basalt interpretations (`SetGen.Set`, `SPMF`, `Plausible.Gen`) +2. Scales to large developments with many types +3. Supports modular correctness proofs about composite generators + +### Design: `GenFor` and `BacktrackGenFor` + +The key distinction we want to express in the typeclass setup is **backtracking vs non-backtracking** behavior — whether the generator can fail locally. Both kinds target a property `P` characterizing their output. + +```lean +/-- A non-backtracking generator for type α whose outputs satisfy P. + Always succeeds (returns G α, not BacktrackGen G α). + For a truly unconstrained generator, P = fun _ => True. + 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 (returns BacktrackGen G α = G (Option α)). + 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 α ``` -Plausible ← Basalt ← Specimen + +The naming reflects the role: "find me a generator **for** `α` satisfying `P`." 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`) + +The `P` parameter characterizes what the generator produces: + +| Class | Example | Property `P` | +|---|---|---| +| `GenFor Nat (fun _ => True)` | Generates any `Nat`, always succeeds | `True` | +| `GenFor (Tree Nat) (Tree.isBST 0 10)` | `Tree.genBST 0 10`, always succeeds | `isBST 0 10` | +| `BacktrackGenFor Expr (HasType · τ)` | Specimen-derived, may fail on some branches | `HasType · τ` | + +### Lawful versions: `LawfulGenFor` and `LawfulBacktrackGenFor` + +The issue with instances of these typeclasses is that we do not know if they are correct, i.e., whether they are _lawful_. This complicates proving lawfulness of a generator that happens to use a sub generator. For our example, the generator for well-formed statements invokes the generator for well-formed expressions via typeclass resolution. To prove that the well-formed statements generator is correct, we need to know/assume that the one for well-formed expressions is correct, too. + +To this end, we introduce two additional typeclasses: + +```lean +/-- A lawful non-backtracking generator: proves that outputs satisfy P. + Provides only soundness & completeness — weaker than Basalt's LawfulGenerator + which also requires almost-sure termination and cost bounds. -/ +class LawfulGenFor (α : Type) (P : α → Prop) extends GenFor α P where + sound_and_complete : IsSoundAndComplete (gen (G := SPMF)) P + +/-- A lawful backtracking generator: proves that successful outputs satisfy P. -/ +class LawfulBacktrackGenFor (α : Type) (P : α → Prop) extends BacktrackGenFor α P where + sound_and_complete : ∀ size a, + some a ∈ SPMF.support (gen (G := SPMF) size) ↔ P a ``` -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. +Instances of these typeclasses are sure to be sound and complete, i.e., lawful (to a minimal degree). Thus users of them can rely on that lawfulness when proving lawfulness locally. + +**Relationship to Basalt's `LawfulGenerator`:** Basalt defines `LawfulGenerator` as a property of a *specific generator term* — it says "this particular generator `g` is sound, complete, terminating, and cost-bounded." Our `LawfulGenFor` and `LawfulBacktrackGenFor` serve a different purpose: they are *typeclasses for resolution* — they say "there exists a generator for this type/property findable by typeclass synthesis, and it is sound and complete." They intentionally omit cost and termination requirements for simplicity; in the future, these could be strengthened to require `LawfulGenerator` of the underlying term, at which point the system would provide full lawfulness guarantees. -## 3. Example +### Standard `GenFor` instances -Consider a simple typing relation: +For standard types (`Nat`, `Bool`, `List`, etc.), we provide `GenFor` instances using existing Basalt-polymorphic generators: ```lean -inductive Ty | nat | bool -inductive Expr | lit (n : Nat) | isZero (e : Expr) +instance : GenFor Nat (fun _ => True) where + gen := Nat.arbitrary -- Basalt's polymorphic Nat generator -inductive HasType : Expr → Ty → Prop - | litNat (n : Nat) : HasType (.lit n) .nat - | isZero (e : Expr) : HasType e .nat → HasType (.isZero e) .bool +instance : GenFor Bool (fun _ => True) where + gen := Bool.arbitrary ``` -### What Specimen emits today +These are the generators that Specimen-derived code will resolve via typeclass synthesis. They must be Basalt-polymorphic (not Plausible-specific) so they work at all interpretations. If needed, a `GenFor` instance can bridge *down* to Plausible's `Arbitrary` for compatibility with the `plausible` tactic: ```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)] +instance [GenFor α (fun _ => True)] : Arbitrary α where + arbitrary := GenFor.gen -- specializes at G := Plausible.Gen ``` -This can be executed but not proved correct. +## 4. The Generated Code (Running Example) -### What Specimen would emit after the change +Applying `BacktrackGen` (Section 2) and the `GenFor` / `BacktrackGenFor` typeclasses (Section 3) to the example, the generated code becomes: ```lean -def genHasType [Gen G] (τ : Ty) : Nat → BacktrackGen G Expr +def genHasType [Gen G] [GenFor Nat (fun _ => True)] [GenFor Bool (fun _ => True)] + (initSize : Nat) (τ : Ty) : (size : Nat) → BacktrackGen G Expr | 0 => backtrack [ (1, fun () => match τ with - | .nat => do let n ← liftGen (genNat : G Nat); pure (some (.lit n)) - | _ => pure none)] + | .nat => do + let n ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Nat) + pure (Expr.litNat n) + | .bool => do + let b ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Bool) + pure (Expr.litBool b)), + (1, fun () => match τ with + | .bool => do + let b ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Bool) + pure (Expr.litBool b) + | .nat => BacktrackGen.fail)] | size + 1 => backtrack [ (1, fun () => match τ with - | .nat => do let n ← liftGen (genNat : G Nat); pure (some (.lit n)) - | _ => pure none), + | .nat => do + let n ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Nat) + pure (Expr.litNat n) + | .bool => do + let b ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Bool) + pure (Expr.litBool b)), (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) + let b ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Bool) + pure (Expr.litBool b) + | .nat => BacktrackGen.fail), + (size + 1, fun () => match τ with + | .bool => do + let e ← genHasType initSize Ty.nat size + pure (Expr.isZero e) + | .nat => BacktrackGen.fail)] + +instance [GenFor Nat (fun _ => True)] [GenFor Bool (fun _ => True)] + : ∀ τ, BacktrackGenFor Expr (fun e => HasType e τ) := + fun τ => ⟨fun {_} [_] size => genHasType size τ size⟩ ``` -### Proving correctness (at `SetGen.Set`) +And `genWellTypedStmt` calls the `HasType` generator via `BacktrackGenFor` typeclass resolution — the runtime value `τ` is captured in the predicate lambda, just as today's code captures it in `(fun e => HasType e τ)`: ```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) := ... +def genWellTypedStmt [Gen G] [GenFor Nat (fun _ => True)] [GenFor Bool (fun _ => True)] + [GenFor Ty (fun _ => True)] + [∀ τ, BacktrackGenFor Expr (fun e => HasType e τ)] + (initSize : Nat) : (size : Nat) → BacktrackGen G Stmt + | 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 (Stmt.expr e)), + (1, fun () => do + let τ ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Ty) + let e ← BacktrackGenFor.gen (P := fun e => HasType e τ) initSize + pure (Stmt.assert e τ))] + | 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 (Stmt.expr e)), + (1, fun () => do + let τ ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Ty) + let e ← BacktrackGenFor.gen (P := fun e => HasType e τ) initSize + pure (Stmt.assert e τ)), + (size + 1, fun () => do + let body ← genWellTypedStmt initSize size + let τ ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Ty) + let e ← BacktrackGenFor.gen (P := fun e => HasType e τ) initSize + let x ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Nat) + pure (Stmt.letBind x e body))] ``` +### Key transformations from the code Specimen generates today + +- `MonadExcept.throw Gen.genericFailure` → `BacktrackGen.fail` +- `return value` → `pure value` (the `BacktrackGen` Monad wraps in `some` automatically) +- `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` +- Registering the `HasType` generator as `GenFor Bool (fun _ => True)` +- Return type: `Plausible.Gen α` → `BacktrackGen G α` +- Function is now polymorphic over `[Gen G]` +- Recursive calls compose directly in the `BacktrackGen` monad (failure propagates via `bind`) + +The `let rec aux_arb` inner function is eliminated — `initSize` and `τ` are explicit parameters with structural recursion on `size`. However, the double-initialization pattern remains: at the Plausible call site, the same value is used for both `initSize` and `size` (matching today's `fun size => aux_arb size size τ`). The `initSize` variable (passed when calling sub-generators like `BacktrackGenFor.gen ... initSize`) gives sub-generators their full budget without decrementing. + ### Executing via Plausible ```lean instance : ArbitrarySizedSuchThat Expr (HasType · τ) where - arbitrarySizedST size := BacktrackGen.toPlausibleGen (genHasType τ size) + arbitrarySizedST size := BacktrackGen.toPlausibleGen (genHasType size τ size) + +instance : ArbitrarySuchThat Expr (HasType · τ) where + arbitraryST := Gen.sized (fun n => BacktrackGen.toPlausibleGen (genHasType n τ n)) + +instance : ArbitrarySizedSuchThat Stmt WellTypedStmt where + arbitrarySizedST size := BacktrackGen.toPlausibleGen (genWellTypedStmt size size) ``` -The `plausible` tactic finds this instance via the existing `ArbitrarySizedSuchThat → ArbitrarySuchThat → Arbitrary` chain and executes it normally. +The `plausible` tactic finds these instances via the existing `ArbitrarySizedSuchThat → ArbitrarySuchThat → Arbitrary` chain and executes them normally. + +## 5. Solving Problem 3: Checkers (`DecOpt`) -### The size pattern +### The problem -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: +Today's `DecOpt` typeclass returns a Plausible-specific type: ```lean -instance : ArbitrarySuchThat Expr (HasType · τ) where - arbitraryST := Gen.sized (fun n => BacktrackGen.toPlausibleGen (genHasType τ n)) +class DecOpt (P : Prop) where + decOpt : Nat → Except GenError Bool ``` -## 4. Plan of Work +It returns `ok true` (P holds), `ok false` (P doesn't hold), or `error` (can't decide — out of fuel). Inside a generator, the result is pattern-matched: `ok true` continues, anything else causes backtracking via `throw`. + +Since the emitted generator following our proposal is polymorphic over `G`, it cannot call a function like `DecOpt.decOpt` that returns `Except GenError Bool`. The checker must also be polymorphic over `G`. + +### Design: `DecOpt` as `BacktrackGen G Bool` + +We redefine `DecOpt` 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 cleanly to `G (Option Bool)`: +- `some true` → P holds +- `some false` → P doesn't hold +- `none` → can't decide (out of fuel) → causes backtracking + +This fits naturally into the `BacktrackGen` framework: when the checker returns `none`, the calling generator treats it as local failure and backtracks to another branch — exactly today's behavior. + +### Example usage -### Step 1: Define `BacktrackGen` in Basalt +Checkers arise in cases like the following: + +```lean +-- Suppose a relation has a constructor with a decidable guard: +-- | bounded (n m : Nat) : n < m → SomeRel n m +-- Specimen generates n and m, then *checks* n < m: +(1, fun () => do + let n ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Nat) + let m ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Nat) + match ← DecOpt.decOpt (n < m) fuel with + | true => pure (SomeResult n m) + | false => BacktrackGen.fail) +``` + +The checker result is a `Bool` in `BacktrackGen G` — match on `true`/`false` (the `none` case is handled by `BacktrackGen`'s monad: if `decOpt` returns `none` internally, the bind short-circuits to failure automatically). + +### Interpretations + +| 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 | + +### Bridge from `Decidable` + +Any `Decidable` instance gives a `DecOpt` trivially (it never fails): + +```lean +instance [Decidable P] : DecOpt P where + decOpt _ := pure (decide P) +``` + +## 6. Solving Problem 4: Unconstrained Generators (`derive Arbitrary`) + +### The problem + +Specimen derives unconstrained generators for algebraic data types via `derive Arbitrary`. These generators use `Gen.frequency` / `Gen.oneOfWithDefault` and `Arbitrary.arbitrary` — all Plausible-specific combinators. Like the constrained generators, they cannot be used polymorphically over Basalt's `Gen` class and cannot be proved correct at `SetGen.Set`. + +Unlike constrained generators, unconstrained generators never backtrack — they always succeed. This makes the migration simpler: no `BacktrackGen` wrapper is needed, just the `frequency` combinator and `GenFor` for sub-field resolution. + +### What Specimen emits today + +For a type like: + +```lean +inductive Tree (α : Type) where + | leaf + | node (left : Tree α) (val : α) (right : Tree α) + deriving Arbitrary +``` + +Specimen currently emits: + +```lean +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 +``` + +### Design: Basalt-polymorphic unconstrained generators + +The migrated version emits a Basalt-polymorphic generator and a `GenFor` instance: + +```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 -- or a fixed default fuel +``` + +### 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)` | + +No `BacktrackGen` wrapper is needed — unconstrained generators always succeed. + +### 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 +``` + +This ensures `deriving Arbitrary` continues to work with the `plausible` tactic. + +## 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. Runtime parameters are captured in the predicate lambda. Because we are inside a `BacktrackGen` `do`-block, 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 body ← genWellTypedStmt initSize 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 + ``` + +### Why typeclass resolution is safe here + +A natural concern: typeclass resolution is opaque, so how can a proof about `genHasType` know which `GenFor Nat (fun _ => True)` instance was resolved? + +The answer is that we maintain the invariant: **every `GenFor` instance in the system is eventually upgraded to a `LawfulGenFor` instance** (and likewise for `BacktrackGenFor` / `LawfulBacktrackGenFor`). Once this invariant holds, it doesn't matter which instance resolution picks — any instance it finds is provably sound and complete. The opacity of resolution is harmless because all candidates satisfy the same contract. + +This invariant is enforced by the two-step roadmap (see Section 8): +1. First, Specimen emits generators with `GenFor` / `BacktrackGenFor` constraints (for execution only). +2. Then, Specimen is upgraded to also emit `LawfulGenFor` / `LawfulBacktrackGenFor` instances with synthesized proofs, ensuring every derived generator is lawful. + +### Mutual recursion + +Specimen supports mutually recursive inductive relations. For mutually recursive generators, the emitted code uses Lean's `mutual ... end` block with direct name calls between the 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 — mutual generators call each other by name, and only *external* callers go through typeclass resolution. + +### The `initSize` parameter + +The generated code takes both `initSize` and `size` as parameters: +- `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`. + +This means sub-generators always get a full budget. When `genWellTypedStmt` at `size=3` calls `BacktrackGenFor.gen (P := fun e => HasType e τ) initSize`, the `HasType` generator receives the original budget (e.g., 5) rather than the remaining budget (3). This matches today's behavior where `aux_arb initSize size' Ty.nat` passes `initSize` to nested `ArbitrarySizedSuchThat.arbitrarySizedST` calls. + +### Fuel vs size vs `partial_fixpoint` + +The `size`/`fuel` parameter in generated code currently serves two distinct purposes that are worth disentangling: + +1. **Termination witness.** Lean requires structural recursion (or `partial_fixpoint`) for every recursive definition to be accepted. The `size : Nat` parameter with pattern-matching on `0` vs `size + 1` provides a structural termination argument. + +2. **Size control.** In property-based testing, generators need a knob that controls the size of generated values — smaller sizes for initial exploration, larger sizes to stress-test. Plausible's `Gen.sized` provides this via a `ReaderT (ULift Nat)` layer. + +These two roles happen to coincide in today's Specimen output (the fuel *is* the size), but they are conceptually independent: + +- **For constrained generators (`BacktrackGenFor`):** Both roles are essential. The fuel ensures termination, and it also bounds the depth of generated derivation trees, providing natural size control. The `initSize`/`size` split already separates them partially: `size` is the termination witness (structurally decremented), while `initSize` controls sub-generator budgets. + +- **For unconstrained generators (`GenFor`):** The fuel is used *only* for termination and size control — there is no backtracking, no failure. In Basalt, `partial_fixpoint` could eliminate the need for an explicit termination witness entirely, since it provides a well-founded recursion principle for generators with `⊥` as the default. However, the fuel still serves a useful role as a **size parameter**: without it, a recursive generator like `Tree.gen` has no way to bias toward smaller trees at lower sizes. + +The practical upshot for this plan: + +- **Phase 1 preserves explicit fuel for both constrained and unconstrained generators.** This is the simplest path — it matches today's behavior, requires no `partial_fixpoint` infrastructure, and gives users familiar size control. + +- **A future optimization** (noted in Section 9) could emit `partial_fixpoint`-based generators that take an optional size hint rather than mandatory fuel. For unconstrained generators, this would look like: + ```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 would need 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 here is how to express size-dependent weights (today's `(fuel + 1, ...)` pattern) without an explicit fuel parameter. One option is a separate size monad layer; another is to use Basalt's cost infrastructure to bound expected depth. This is deferred as a research question. + +### Performance considerations + +`BacktrackGen` adds an `Option` wrapper at every bind within backtracking branches. For deeply nested generators this means more allocations and pattern-matches compared to today's exception-based approach. In practice this overhead is negligible — the dominant cost is in `choose` calls and the retries themselves, not the `Option` wrapping. If profiling reveals otherwise, the `toPlausibleGen` boundary could be pushed deeper (converting to exception-based execution earlier), at the cost of limiting provability. + +### Proving correctness (at `SetGen.Set`) + +With `[LawfulGenFor Nat (fun _ => True)]` in scope (which provides `GenFor Nat (fun _ => True)` via the subclass relationship), proofs compose modularly: + +```lean +theorem genHasType_sound [LawfulGenFor Nat (fun _ => True)] [LawfulGenFor Bool (fun _ => True)] + (τ : Ty) (size : Nat) (e : Expr) : + some e ∈ SetGen.support (genHasType (G := SetGen.Set) size τ size) → HasType e τ := ... + +theorem genHasType_complete [LawfulGenFor Nat (fun _ => True)] [LawfulGenFor Bool (fun _ => True)] + (τ : Ty) (e : Expr) (h : HasType e τ) : + ∃ size, some e ∈ SetGen.support (genHasType (G := SetGen.Set) size τ size) := ... + +theorem genWellTypedStmt_sound + [LawfulGenFor Nat (fun _ => True)] [LawfulGenFor Bool (fun _ => True)] + [LawfulGenFor Ty (fun _ => True)] + (size : Nat) (s : Stmt) : + some s ∈ SetGen.support (genWellTypedStmt (G := SetGen.Set) size size) → WellTypedStmt s := ... +``` + +The `LawfulGenFor` constraint gives the proof access to `LawfulGenFor.sound_and_complete`. Since any instance resolved for `GenFor Nat (fun _ => True)` must come from a `LawfulGenFor` instance (once the system invariant holds), the proof is sound regardless of which instance was picked. + +## 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 `frequency` combinator (weighted random selection, no retry — for unconstrained generators) +- 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 (e.g., `Nat.arbitrary`) +- Provide bridge instance: `instance [Decidable P] : DecOpt P` +- Optionally provide bridge: `instance [GenFor α (fun _ => True)] : Arbitrary α` for Plausible compatibility -### Step 2: Prove SetGen support lemmas +#### Step 1.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 +#### 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 `pure none` +- Replace `throw` with `BacktrackGen.fail` (equivalently, `pure none` at the `G` level) - Replace fuel-based recursion with structural recursion on an explicit `size : Nat` -- Emit generators polymorphic over `[Gen G]` instead of targeting `Plausible.Gen` +- Emit generators polymorphic over `[Gen G]` with `[GenFor α P]` / `[BacktrackGenFor α P]` constraints for sub-generators +- Replace `Arbitrary.arbitrary` calls with `GenFor.gen` wrapped in `BacktrackGen.liftGen` +- Replace `ArbitrarySizedSuchThat.arbitrarySizedST` calls with `BacktrackGenFor.gen` (or direct name calls for co-derived / mutually-recursive generators) +- Replace `DecOpt.decOpt` calls (pattern-matching on `Except`) with the new polymorphic `DecOpt.decOpt` (pattern-matching on `Bool` within `BacktrackGen`) - Emit `ArbitrarySizedSuchThat` instances that call `BacktrackGen.toPlausibleGen` -### Step 4: Validate the pipeline +#### 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 (for sub-fields) with `GenFor.gen (P := fun _ => True)` +- Emit generators polymorphic over `[Gen G]` with `[GenFor α (fun _ => True)]` constraints for type parameters +- Emit `GenFor α (fun _ => True)` instances (with a `Gen.sized` wrapper or fixed fuel) for each derived type +- Emit bridge `Arbitrary` instance: `instance [GenFor α (fun _ => True)] : Arbitrary α where arbitrary := GenFor.gen` +- Ensure mutually recursive types use Lean's `mutual ... end` block with direct name calls, then register `GenFor` instances after + +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 (expected output will change shape; update snapshots) +- Verify `derive Arbitrary` produces working `GenFor` instances for standard test types (e.g., `Tree`, `Expr`) +- Verify the `plausible` tactic works end-to-end with both constrained and unconstrained generators +- Write a manual soundness proof for the `HasType` example, demonstrating that a Specimen-derived generator can be proved sound at `SetGen.Set` given `LawfulGenFor` / `LawfulBacktrackGenFor` instances for sub-generators + +### Phase 2: Lawful generation (with proof synthesis) + +The goal of this phase is to make Specimen emit `LawfulGenFor` / `LawfulBacktrackGenFor` instances alongside the generators, so that every derived generator carries a machine-checked proof of soundness and completeness. Once this phase is complete, the system invariant holds: all `GenFor` / `BacktrackGenFor` instances are lawful, and proofs about composite generators compose modularly. + +#### Step 2.1: Define `LawfulGenFor` and `LawfulBacktrackGenFor` in Basalt + +- Define `LawfulGenFor` extending `GenFor` with soundness/completeness at `SPMF` +- Define `LawfulBacktrackGenFor` extending `BacktrackGenFor` similarly +- Provide `LawfulGenFor` instances for standard types (using existing Basalt proofs like `Nat.arbitrary_support`) + +#### 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 inductive relation. The proof structure mirrors the generator structure: + +1. **Top-level**: The proof proceeds by `cases` on the `size` parameter, matching the generator's pattern match. +2. **Per-branch**: Each branch in `backtrack [...]` contributes one direction of the `↔`. The `backtrack_mem_iff` lemma decomposes `some a ∈ support (backtrack gs)` into a disjunction over branches. +3. **Soundness** (forward): For each branch that produces `some a`, show `P a` holds. This follows the `do`-block structure — each `liftGen` or `BacktrackGenFor.gen` call contributes a hypothesis (from the sub-generator's `LawfulGenFor` / `LawfulBacktrackGenFor` instance). +4. **Completeness** (backward): For each constructor of the inductive relation, exhibit a `size` and branch that produces the corresponding value. Typically, the recursive constructor needs `size = depth_of_derivation`. + +Sub-generator proof obligations are discharged by the `LawfulGenFor` / `LawfulBacktrackGenFor` instances of sub-generators (available via typeclass resolution). + +Emit `LawfulBacktrackGenFor` instances bundling generator + proof. + +For each derived **unconstrained** generator (`derive Arbitrary`), Specimen emits a `LawfulGenFor α (fun _ => True)` instance. The property is trivially `True`, so the proof obligation reduces to: +- **Soundness**: trivial (every value satisfies `fun _ => True`) +- **Completeness**: show that every inhabitant of `α` is in the support of the generator. This amounts to showing that `frequency` with all constructors covered produces every value at some fuel — each constructor's branch reaches the corresponding value when sub-generators (with their own `LawfulGenFor` instances) are complete. + +The proof follows the inductive structure of the type: base-case constructors are reachable at fuel 0, recursive constructors at fuel ≥ depth. This is simpler than the constrained case because there is no `Option` wrapping and no backtracking — `frequency_mem_iff` directly gives the membership condition. + +#### Step 2.3: End-to-end validation + +- Verify that Specimen-derived generators (both constrained and unconstrained) carry correct proofs (they typecheck with no `sorry`) +- Verify that proofs compose: a generator for type `A` that calls a generator for type `B` can use `B`'s `LawfulGenFor` / `LawfulBacktrackGenFor` proof without manual intervention +- Benchmark elaboration time to ensure proof synthesis does not unacceptably slow down `derive_generator` or `derive Arbitrary` + +### Rollback strategy + +If Phase 1 reveals fundamental design issues (e.g., universe polymorphism problems, instance diamonds at scale, or unacceptable elaboration performance), 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 throughout development. A feature flag (`set_option specimen.basaltBridge true`) can gate the new emission path, allowing incremental rollout and easy revert. + +## 9. Known Limitations and Future Work + +The following issues are related to the migration but are not addressed by the plan above: + +**`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 where almost-sure termination can be proved, eliminating the fuel parameter and enabling tighter cost bounds. This is a research question deferred beyond Phase 2. + +## Glossary -- 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 +| Term | Meaning | +|---|---| +| **Constrained producer** | A generator that only produces values satisfying a user-specified inductive relation (e.g., well-typed expressions) | +| **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, not the decremented counter | +| **Schedule** | Specimen's internal representation of how to order constructor attempts when deriving a generator | +| **Backtracking** | The ability for a generator branch to signal failure, causing the combinator to retry another branch | +| **`BacktrackGen`** | A newtype wrapping `G (Option α)` — the backtracking layer used in this plan | +| **`GenFor` / `BacktrackGenFor`** | Typeclasses for finding generators by typeclass resolution (analogous to `Arbitrary` / `ArbitrarySizedSuchThat`) | diff --git a/SpecimenTest/BridgeDecOptMockup.lean b/SpecimenTest/BridgeDecOptMockup.lean new file mode 100644 index 0000000..4e11c20 --- /dev/null +++ b/SpecimenTest/BridgeDecOptMockup.lean @@ -0,0 +1,157 @@ +import Plausible + +/-! +# Specimen–Basalt Bridge Mockup: DecOpt Example + +This file demonstrates how the proposed Basalt-compatible DecOpt typeclass +works within generators, with execution via Plausible.Gen. +-/ + +open Lean.Order + +namespace MockDecOpt + +/-! ## Basalt infrastructure (same as BridgeMockup.lean) -/ + +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 + +def backtrack [Gen G] (gs : List (Nat × (Unit → BacktrackGen G α))) : BacktrackGen G α := + ⟨go gs⟩ +where + go : List (Nat × (Unit → BacktrackGen G α)) → G (Option α) + | [] => pure none + | [(_, g)] => (g ()).run + | gs => do + let idx ← RandomChoice.choose 0 (gs.length - 1) (by omega) + let (_, g) := gs[idx.down]! + match ← (g ()).run with + | some a => pure (some a) + | none => go (gs.eraseIdx idx.down) + termination_by gs => gs.length + +class GenFor (α : Type) (P : α → Prop) where + gen : ∀ {G : Type → Type} [Gen G], G α + +/-! ## DecOpt: Basalt-compatible checker -/ + +/-- A partial decision procedure for P, polymorphic over Gen G. + Returns some true/false if decided, none if can't decide (backtrack). -/ +class DecOpt (P : Prop) where + decOpt : ∀ {G : Type → Type} [Gen G], Nat → BacktrackGen G Bool + +/-- Any Decidable instance gives a DecOpt that never fails. -/ +instance (priority := low) [Decidable P] : DecOpt P where + decOpt _ := pure (decide P) + +/-! ## Example: generate-then-check with a bounded constraint -/ + +instance : GenFor Nat (fun _ => True) where + gen := do + let n ← RandomChoice.choose 0 20 (by omega) + pure n.down + +/-- Generate a pair (a, b) where a ≤ b and both are in [lo, hi]. + Strategy: generate freely, then check constraints via DecOpt. + Multiple branches allow retrying on failure. -/ +def genSortedBounded [Gen G] [GenFor Nat (fun _ => True)] + (lo hi : Nat) (_initSize : Nat) : (size : Nat) → BacktrackGen G (Nat × Nat) + | _ => + let branch : Unit → BacktrackGen G (Nat × Nat) := fun () => do + let a ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Nat) + let b ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Nat) + -- Check all constraints using DecOpt; fail (backtrack) if any don't hold + match ← DecOpt.decOpt (P := decide (lo ≤ a ∧ a ≤ hi ∧ lo ≤ b ∧ b ≤ hi ∧ a ≤ b) = true) 0 with + | true => pure (a, b) + | false => BacktrackGen.fail + -- Repeat the branch to give multiple retry attempts + backtrack [(1, branch), (1, branch), (1, branch), (1, branch), (1, branch), + (1, branch), (1, branch), (1, branch), (1, branch), (1, branch)] + +end MockDecOpt + +open MockDecOpt + +-- Run genSortedBounded with lo=0, hi=20 (matches generator range for high success rate) +#eval! do + IO.println "=== genSortedBounded (lo=0, hi=20, size=10) ===" + let mut successes := 0 + for _ in List.range 50 do + try + let result ← Plausible.Gen.run + (BacktrackGen.toPlausibleGen (genSortedBounded (G := Plausible.Gen) 0 20 10 0)) 10 + IO.println s!" success: {repr result}" + successes := successes + 1 + catch _ => pure () + IO.println s!" ({successes}/50 attempts succeeded)" diff --git a/SpecimenTest/BridgeMockup.lean b/SpecimenTest/BridgeMockup.lean new file mode 100644 index 0000000..ac7a2ec --- /dev/null +++ b/SpecimenTest/BridgeMockup.lean @@ -0,0 +1,333 @@ +import Plausible + +/-! +# Specimen–Basalt Bridge Mockup: Running Example + +This file mocks up the proposed generator structure using Basalt's actual Gen class +definition (which depends only on core Lean's Lean.Order) and demonstrates execution +via Plausible's Gen monad. +-/ + +open Lean.Order + +/-! ## Basalt Gen class (copied from Basalt/Gen.lean) -/ + +namespace Mock + +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 + +/-! ## Plausible.Gen as a Basalt Gen instance (adapted from Basalt/PlausibleGen.lean) -/ + +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⟩ + +/-- Unwrap BacktrackGen to Plausible.Gen, throwing on failure. -/ +def toPlausibleGen (x : BacktrackGen Plausible.Gen α) : Plausible.Gen α := do + match ← x.run with + | some a => pure a + | none => throw (.genError "backtracking exhausted") + +def BacktrackGen.toGen [Gen G] [Inhabited α] (g : BacktrackGen G α) : G α := do + match ← g.run with + | some a => pure a + | none => pure default -- ⊥ (divergence) + +end BacktrackGen + +/-! ## backtrack combinator -/ + +def backtrack [Gen G] (gs : List (Nat × (Unit → BacktrackGen G α))) : BacktrackGen G α := + ⟨go gs⟩ +where + go : List (Nat × (Unit → BacktrackGen G α)) → G (Option α) + | [] => pure none + | [(_, g)] => (g ()).run + | gs => do + let idx ← RandomChoice.choose 0 (gs.length - 1) (by omega) + let (_, g) := gs[idx.down]! + match ← (g ()).run with + | some a => pure (some a) + | none => go (gs.eraseIdx idx.down) + termination_by gs => gs.length + +/-! ## GenFor / BacktrackGenFor 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 α + +/-! ## Running example -/ + +inductive Ty | nat | bool + deriving Repr, Inhabited, BEq + +inductive Expr + | litNat (n : Nat) + | litBool (b : Bool) + | isZero (e : Expr) + deriving Repr, Inhabited + +inductive Stmt + | expr (e : Expr) + | letBind (x : Nat) (e : Expr) (body : Stmt) + | assert (e : Expr) (τ : Ty) + deriving Repr, Inhabited + +inductive HasType : Expr → Ty → Prop + | litNat (n : Nat) : HasType (.litNat n) .nat + | litBool (b : Bool) : HasType (.litBool b) .bool + | isZero (e : Expr) : HasType e .nat → HasType (.isZero e) .bool + +inductive WellTypedStmt : Stmt → Prop + | expr (e : Expr) (τ : Ty) : HasType e τ → WellTypedStmt (.expr e) + | letBind (x : Nat) (e : Expr) (body : Stmt) (τ : Ty) : + HasType e τ → WellTypedStmt body → WellTypedStmt (.letBind x e body) + | assert (e : Expr) (τ : Ty) : HasType e τ → WellTypedStmt (.assert e τ) + +/-! ## GenFor instances for leaf types -/ + +instance : GenFor Nat (fun _ => True) where + gen := do + -- Simple geometric distribution + let n ← RandomChoice.choose 0 100 (by omega) + pure n.down + +instance : GenFor Bool (fun _ => True) where + gen := do + let n ← RandomChoice.choose 0 1 (by omega) + pure (n.down == 0) + +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) + +/-! ## genHasType: the derived constrained generator -/ + +def genHasType [Gen G] [GenFor Nat (fun _ => True)] [GenFor Bool (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.litNat n) + | .bool => do + let b ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Bool) + pure (Expr.litBool b)), + (1, fun () => match τ with + | .bool => do + let b ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Bool) + pure (Expr.litBool b) + | .nat => BacktrackGen.fail)] + | size + 1 => backtrack [ + (1, fun () => match τ with + | .nat => do + let n ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Nat) + pure (Expr.litNat n) + | .bool => do + let b ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Bool) + pure (Expr.litBool b)), + (1, fun () => match τ with + | .bool => do + let b ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Bool) + pure (Expr.litBool b) + | .nat => BacktrackGen.fail), + (size + 1, fun () => match τ with + | .bool => do + let e ← genHasType initSize Ty.nat size + pure (Expr.isZero e) + | .nat => BacktrackGen.fail)] + +/-! ## Register genHasType as a BacktrackGenFor instance -/ + +instance [GenFor Nat (fun _ => True)] [GenFor Bool (fun _ => True)] + : ∀ τ, BacktrackGenFor Expr (fun e => HasType e τ) := + fun τ => ⟨fun {_} [_] size => genHasType size τ size⟩ + +/-! ## genWellTypedStmt: uses BacktrackGenFor for cross-generator call -/ + +def genWellTypedStmt [Gen G] [GenFor Nat (fun _ => True)] [GenFor Bool (fun _ => True)] + [GenFor Ty (fun _ => True)] + [∀ τ, BacktrackGenFor Expr (fun e => HasType e τ)] + (initSize : Nat) : (size : Nat) → BacktrackGen G Stmt + | 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 (Stmt.expr e)), + (1, fun () => do + let τ ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Ty) + let e ← BacktrackGenFor.gen (P := fun e => HasType e τ) initSize + pure (Stmt.assert e τ))] + | 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 (Stmt.expr e)), + (1, fun () => do + let τ ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Ty) + let e ← BacktrackGenFor.gen (P := fun e => HasType e τ) initSize + pure (Stmt.assert e τ)), + (size + 1, fun () => do + let body ← genWellTypedStmt initSize size + let τ ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Ty) + let e ← BacktrackGenFor.gen (P := fun e => HasType e τ) initSize + let x ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Nat) + pure (Stmt.letBind x e body))] + +/-! ## frequency combinator (for non-backtracking generators) -/ + +/-- Weighted random selection without retry. For non-backtracking generators. -/ +def frequency [Gen G] (default : G α) (gs : List (Nat × (Unit → G α))) : G α := + match gs with + | [] => default + | [(_, g)] => g () + | gs => do + let idx ← RandomChoice.choose 0 (gs.length - 1) (by omega) + let (_, g) := gs[idx.down]! + g () + +/-! ## 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 + +/-! ## Execution via Plausible -/ + +end Mock + +open Mock + +/-! ## Status quo: what Specimen emits today for unconstrained generators (using Plausible directly) + This verifies that the "What Specimen emits today" code in SPECIMEN-BASALT-BRIDGE.md Section 6 + is accurate. -/ +namespace StatusQuo +open Plausible + +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 StatusQuo + +-- Run genHasType at Plausible.Gen and print results. +#eval! do + IO.println "=== genHasType (τ = .nat, size = 3) ===" + 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 "=== genHasType (τ = .bool, size = 3) ===" + for _ in List.range 5 do + let result ← Plausible.Gen.run + (BacktrackGen.toPlausibleGen (genHasType (G := Plausible.Gen) 3 .bool 3)) 10 + IO.println s!" {repr result}" + +#eval! do + IO.println "=== genWellTypedStmt (size = 3) ===" + for _ in List.range 5 do + let result ← Plausible.Gen.run + (BacktrackGen.toPlausibleGen (genWellTypedStmt (G := Plausible.Gen) 3 3)) 10 + IO.println s!" {repr result}" + +#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}" \ No newline at end of file From 20949720c4df5f9b95715fc296eaba89bd65e4c8 Mon Sep 17 00:00:00 2001 From: Mike Hicks Date: Wed, 3 Jun 2026 09:56:42 -0400 Subject: [PATCH 2/8] refactor: Replace running example and consolidate Bridge mockups MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replace the HasType/WellTypedStmt running example with HasType/WellFormed which genuinely exercises all three mechanisms: backtracking (multiple constructors per type), DecOpt checkers (n ≠ 0 guard), and sub-generators (WellFormed calls HasType via BacktrackGenFor). Document changes: - Swap Sections 4 and 5 so DecOpt is defined before the generated code - Add unconstrained generator derivation (derive Arbitrary → GenFor) as Section 6, removing it from Known Limitations - Add fuel/size/partial_fixpoint discussion to Design Notes - Update all cross-references and proof sketches Test file changes: - Consolidate BridgeMockup.lean and BridgeDecOptMockup.lean into a single BridgeBacktrackMockup.lean that demonstrates all mechanisms - Include both status-quo (Specimen trace output) and migrated code - Add unconstrained generator (Tree.gen with frequency) example - Rename Generator/BacktrackGenerator to GenFor/BacktrackGenFor throughout --- SPECIMEN-BASALT-BRIDGE.md | 294 ++++++++-------- SpecimenTest/BridgeBacktrackMockup.lean | 445 ++++++++++++++++++++++++ SpecimenTest/BridgeDecOptMockup.lean | 157 --------- SpecimenTest/BridgeMockup.lean | 333 ------------------ 4 files changed, 585 insertions(+), 644 deletions(-) create mode 100644 SpecimenTest/BridgeBacktrackMockup.lean delete mode 100644 SpecimenTest/BridgeDecOptMockup.lean delete mode 100644 SpecimenTest/BridgeMockup.lean diff --git a/SPECIMEN-BASALT-BRIDGE.md b/SPECIMEN-BASALT-BRIDGE.md index 497e4fe..bb5f26b 100644 --- a/SPECIMEN-BASALT-BRIDGE.md +++ b/SPECIMEN-BASALT-BRIDGE.md @@ -81,38 +81,35 @@ The following are explicitly **not** addressed by this plan: ### Example -We will use the following small typed language throughout this document to illustrate the changes. (Note: the `letBind` form is a simplification — the bound variable is never referenced in the body. This is intentional; the example is designed to show cross-generator composition, not to be a realistic language.) +We will use the following small typed language throughout this document to illustrate the changes. This example is designed to exercise all three mechanisms: backtracking (multiple constructors per type, some of which fail), checkers (the `isPos` constructor has a decidable guard `n ≠ 0`), and cross-generator composition (`WellFormed` calls `HasType`). ```lean inductive Ty | nat | bool inductive Expr - | litNat (n : Nat) - | litBool (b : Bool) - | isZero (e : Expr) - -inductive Stmt - | expr (e : Expr) - | letBind (x : Nat) (e : Expr) (body : Stmt) - | assert (e : Expr) (τ : Ty) + | lit (n : Nat) + | isPos (n : Nat) + | add (l r : Expr) inductive HasType : Expr → Ty → Prop - | litNat (n : Nat) : HasType (.litNat n) .nat - | litBool (b : Bool) : HasType (.litBool b) .bool - | isZero (e : Expr) : HasType e .nat → HasType (.isZero e) .bool + | 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 WellTypedStmt : Stmt → Prop - | expr (e : Expr) (τ : Ty) : HasType e τ → WellTypedStmt (.expr e) - | letBind (x : Nat) (e : Expr) (body : Stmt) (τ : Ty) : - HasType e τ → WellTypedStmt body → WellTypedStmt (.letBind x e body) - | assert (e : Expr) (τ : Ty) : HasType e τ → WellTypedStmt (.assert e τ) +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 _ => ∃ s, WellTypedStmt s) +derive_generator (fun _ => ∃ p, WellFormed p) ``` ### What Specimen emits today @@ -127,54 +124,65 @@ instance : ArbitrarySizedSuchThat Expr (fun e => HasType e τ) where | Nat.zero => GeneratorCombinators.backtrack [(1, match τ with - | Ty.nat => do let n ← Arbitrary.arbitrary; return Expr.litNat n + | Ty.nat => do + let n ← Arbitrary.arbitrary + return Expr.lit n | _ => MonadExcept.throw Gen.genericFailure), (1, match τ with - | Ty.bool => do let b ← Arbitrary.arbitrary; return Expr.litBool b + | 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.litNat n + | Ty.nat => do + let n ← Arbitrary.arbitrary + return Expr.lit n | _ => MonadExcept.throw Gen.genericFailure), (1, match τ with - | Ty.bool => do let b ← Arbitrary.arbitrary; return Expr.litBool b + | 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.bool => do let e ← aux_arb initSize size' Ty.nat; return Expr.isZero e + | 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 `WellTypedStmt`, Specimen produces a generator that calls the `HasType` generator **via typeclass resolution** (`ArbitrarySizedSuchThat.arbitrarySizedST`): +For `WellFormed`, Specimen produces a generator that calls the `HasType` generator **via typeclass resolution** (`ArbitrarySizedSuchThat.arbitrarySizedST`): ```lean -instance : ArbitrarySizedSuchThat Stmt (fun s => WellTypedStmt s) where +instance : ArbitrarySizedSuchThat Prog (fun p => WellFormed p) where arbitrarySizedST := - let rec aux_arb (initSize : Nat) (size : Nat) : Plausible.Gen Stmt := + 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 Stmt.expr e), + return Prog.expr e), (1, do let τ ← Arbitrary.arbitrary - let e ← @ArbitrarySizedSuchThat.arbitrarySizedST _ (fun e => HasType e τ) _ initSize - return Stmt.assert e τ)] + 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 Stmt.expr e), + return Prog.expr e), (1, do let τ ← Arbitrary.arbitrary - let e ← @ArbitrarySizedSuchThat.arbitrarySizedST _ (fun e => HasType e τ) _ initSize - return Stmt.assert e τ), - (Nat.succ size', do - let body ← aux_arb initSize size' - let τ ← Arbitrary.arbitrary - let e ← @ArbitrarySizedSuchThat.arbitrarySizedST _ (fun e => HasType e τ) _ initSize - let x ← Arbitrary.arbitrary - return Stmt.letBind x e body)] + 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 ``` @@ -184,7 +192,7 @@ These generators work for execution but cannot be proved correct. To bridge them **Problem 2: Sub-generator resolution.** The generators call sub-generators via Plausible-specific typeclasses (`Arbitrary`, `ArbitrarySizedSuchThat`). These typeclasses wrap `Plausible.Gen` and cannot be used polymorphically over `G`. We need a Basalt-compatible typeclass for sub-generator lookup. (Addressed in Section 3.) -**Problem 3: Checkers.** In more complex examples, Specimen invokes `DecOpt.decOpt` within generators to check hypotheses that involve only fixed (input) variables. `DecOpt.decOpt` returns `Except GenError Bool` — a Plausible-specific type. Checkers must also be made polymorphic over `G`. (Addressed in Section 5. Our running example does not trigger this, but it arises frequently in practice — e.g., checking `n < m` or type equality after both sides are determined.) +**Problem 3: Checkers.** In more complex examples, Specimen invokes `DecOpt.decOpt` within generators to check hypotheses that involve only fixed (input) variables. `DecOpt.decOpt` returns `Except GenError Bool` — a Plausible-specific type. Checkers must also be made polymorphic over `G`. (Addressed in Section 4. In our running example, the `isPos` constructor triggers this: after generating `n`, Specimen checks `n ≠ 0` via `DecOpt`.) **Problem 4: Unconstrained generators.** Specimen's `derive Arbitrary` emits generators using Plausible-specific `Gen.frequency` / `Gen.oneOfWithDefault` and `Arbitrary.arbitrary`. These must also become Basalt-polymorphic so they can serve as provably-correct `GenFor` instances for sub-generator resolution in constrained generators. (Addressed in Section 6.) @@ -383,81 +391,125 @@ instance [GenFor α (fun _ => True)] : Arbitrary α where arbitrary := GenFor.gen -- specializes at G := Plausible.Gen ``` -## 4. The Generated Code (Running Example) +## 4. Solving Problem 3: Checkers (`DecOpt`) + +### The problem + +Today's `DecOpt` typeclass returns a Plausible-specific type: + +```lean +class DecOpt (P : Prop) where + decOpt : Nat → Except GenError Bool +``` + +It returns `ok true` (P holds), `ok false` (P doesn't hold), or `error` (can't decide — out of fuel). Inside a generator, the result is pattern-matched: `ok true` continues, anything else causes backtracking via `throw`. + +Since the emitted generator following our proposal is polymorphic over `G`, it cannot call a function like `DecOpt.decOpt` that returns `Except GenError Bool`. The checker must also be polymorphic over `G`. + +### Design: `DecOpt` as `BacktrackGen G Bool` + +We redefine `DecOpt` 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 cleanly to `G (Option Bool)`: +- `some true` → P holds +- `some false` → P doesn't hold +- `none` → can't decide (out of fuel) → causes backtracking + +This fits naturally into the `BacktrackGen` framework: when the checker returns `none`, the calling generator treats it as local failure and backtracks to another branch — exactly today's behavior. The running example demonstrates this: in the `isPos` branch, `DecOpt.decOpt (P := ¬(n = 0))` is called after `n` is generated; if it returns `false`, the branch fails and `backtrack` retries another branch. + +### Interpretations -Applying `BacktrackGen` (Section 2) and the `GenFor` / `BacktrackGenFor` typeclasses (Section 3) to the example, the generated code becomes: +| 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 | + +### Bridge from `Decidable` + +Any `Decidable` instance gives a `DecOpt` trivially (it never fails): + +```lean +instance [Decidable P] : DecOpt P where + decOpt _ := pure (decide P) +``` + +## 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)] [GenFor Bool (fun _ => True)] +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.litNat n) - | .bool => do - let b ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Bool) - pure (Expr.litBool b)), + pure (Expr.lit n) + | _ => BacktrackGen.fail), (1, fun () => match τ with | .bool => do - let b ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Bool) - pure (Expr.litBool b) - | .nat => BacktrackGen.fail)] + 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.litNat n) - | .bool => do - let b ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Bool) - pure (Expr.litBool b)), + pure (Expr.lit n) + | _ => BacktrackGen.fail), (1, fun () => match τ with | .bool => do - let b ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Bool) - pure (Expr.litBool b) - | .nat => BacktrackGen.fail), + 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 - | .bool => do - let e ← genHasType initSize Ty.nat size - pure (Expr.isZero e) - | .nat => BacktrackGen.fail)] + | .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)] [GenFor Bool (fun _ => True)] +instance [GenFor Nat (fun _ => True)] : ∀ τ, BacktrackGenFor Expr (fun e => HasType e τ) := fun τ => ⟨fun {_} [_] size => genHasType size τ size⟩ ``` -And `genWellTypedStmt` calls the `HasType` generator via `BacktrackGenFor` typeclass resolution — the runtime value `τ` is captured in the predicate lambda, just as today's code captures it in `(fun e => HasType e τ)`: +And `genWellFormed` calls the `HasType` generator via `BacktrackGenFor` typeclass resolution — the runtime value `τ` is captured in the predicate lambda, just as today's code captures it in `(fun e => HasType e τ)`: ```lean -def genWellTypedStmt [Gen G] [GenFor Nat (fun _ => True)] [GenFor Bool (fun _ => True)] - [GenFor Ty (fun _ => True)] +def genWellFormed [Gen G] [GenFor Nat (fun _ => True)] [GenFor Ty (fun _ => True)] [∀ τ, BacktrackGenFor Expr (fun e => HasType e τ)] - (initSize : Nat) : (size : Nat) → BacktrackGen G Stmt + (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 (Stmt.expr e)), + pure (Prog.expr e)), (1, fun () => do let τ ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Ty) - let e ← BacktrackGenFor.gen (P := fun e => HasType e τ) initSize - pure (Stmt.assert e τ))] + 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 (Stmt.expr e)), + pure (Prog.expr e)), (1, fun () => do let τ ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Ty) - let e ← BacktrackGenFor.gen (P := fun e => HasType e τ) initSize - pure (Stmt.assert e τ)), - (size + 1, fun () => do - let body ← genWellTypedStmt initSize size - let τ ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Ty) - let e ← BacktrackGenFor.gen (P := fun e => HasType e τ) initSize - let x ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Nat) - pure (Stmt.letBind x e body))] + 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 the code Specimen generates today @@ -466,7 +518,7 @@ def genWellTypedStmt [Gen G] [GenFor Nat (fun _ => True)] [GenFor Bool (fun _ => - `return value` → `pure value` (the `BacktrackGen` Monad wraps in `some` automatically) - `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` -- Registering the `HasType` generator as `GenFor Bool (fun _ => True)` +- `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 α` - Function is now polymorphic over `[Gen G]` - Recursive calls compose directly in the `BacktrackGen` monad (failure propagates via `bind`) @@ -482,78 +534,12 @@ instance : ArbitrarySizedSuchThat Expr (HasType · τ) where instance : ArbitrarySuchThat Expr (HasType · τ) where arbitraryST := Gen.sized (fun n => BacktrackGen.toPlausibleGen (genHasType n τ n)) -instance : ArbitrarySizedSuchThat Stmt WellTypedStmt where - arbitrarySizedST size := BacktrackGen.toPlausibleGen (genWellTypedStmt 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. -## 5. Solving Problem 3: Checkers (`DecOpt`) - -### The problem - -Today's `DecOpt` typeclass returns a Plausible-specific type: - -```lean -class DecOpt (P : Prop) where - decOpt : Nat → Except GenError Bool -``` - -It returns `ok true` (P holds), `ok false` (P doesn't hold), or `error` (can't decide — out of fuel). Inside a generator, the result is pattern-matched: `ok true` continues, anything else causes backtracking via `throw`. - -Since the emitted generator following our proposal is polymorphic over `G`, it cannot call a function like `DecOpt.decOpt` that returns `Except GenError Bool`. The checker must also be polymorphic over `G`. - -### Design: `DecOpt` as `BacktrackGen G Bool` - -We redefine `DecOpt` 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 cleanly to `G (Option Bool)`: -- `some true` → P holds -- `some false` → P doesn't hold -- `none` → can't decide (out of fuel) → causes backtracking - -This fits naturally into the `BacktrackGen` framework: when the checker returns `none`, the calling generator treats it as local failure and backtracks to another branch — exactly today's behavior. - -### Example usage - -Checkers arise in cases like the following: - -```lean --- Suppose a relation has a constructor with a decidable guard: --- | bounded (n m : Nat) : n < m → SomeRel n m --- Specimen generates n and m, then *checks* n < m: -(1, fun () => do - let n ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Nat) - let m ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Nat) - match ← DecOpt.decOpt (n < m) fuel with - | true => pure (SomeResult n m) - | false => BacktrackGen.fail) -``` - -The checker result is a `Bool` in `BacktrackGen G` — match on `true`/`false` (the `none` case is handled by `BacktrackGen`'s monad: if `decOpt` returns `none` internally, the bind short-circuits to failure automatically). - -### Interpretations - -| 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 | - -### Bridge from `Decidable` - -Any `Decidable` instance gives a `DecOpt` trivially (it never fails): - -```lean -instance [Decidable P] : DecOpt P where - decOpt _ := pure (decide P) -``` - ## 6. Solving Problem 4: Unconstrained Generators (`derive Arbitrary`) ### The problem @@ -652,7 +638,7 @@ The emitted code uses different calling conventions depending on the sub-generat - **Self-recursive call**: Direct, with decremented size: ```lean - let body ← genWellTypedStmt initSize size + let l ← genHasType initSize .nat size ``` - **Hand-written non-backtracking constrained generator** (e.g., Basalt's `Tree.genBST`): Returns `G α`, registered as a `GenFor`: @@ -681,7 +667,7 @@ The generated code takes both `initSize` and `size` as parameters: - `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`. -This means sub-generators always get a full budget. When `genWellTypedStmt` at `size=3` calls `BacktrackGenFor.gen (P := fun e => HasType e τ) initSize`, the `HasType` generator receives the original budget (e.g., 5) rather than the remaining budget (3). This matches today's behavior where `aux_arb initSize size' Ty.nat` passes `initSize` to nested `ArbitrarySizedSuchThat.arbitrarySizedST` calls. +This means sub-generators always get a full budget. When `genWellFormed` at `size=3` calls `BacktrackGenFor.gen (P := fun e => HasType e τ) initSize`, the `HasType` generator receives the original budget (e.g., 5) rather than the remaining budget (3). This matches today's behavior where `aux_arb initSize size' Ty.nat` passes `initSize` to nested `ArbitrarySizedSuchThat.arbitrarySizedST` calls. ### Fuel vs size vs `partial_fixpoint` @@ -723,19 +709,19 @@ The practical upshot for this plan: With `[LawfulGenFor Nat (fun _ => True)]` in scope (which provides `GenFor Nat (fun _ => True)` via the subclass relationship), proofs compose modularly: ```lean -theorem genHasType_sound [LawfulGenFor Nat (fun _ => True)] [LawfulGenFor Bool (fun _ => True)] +theorem genHasType_sound [LawfulGenFor Nat (fun _ => True)] (τ : Ty) (size : Nat) (e : Expr) : some e ∈ SetGen.support (genHasType (G := SetGen.Set) size τ size) → HasType e τ := ... -theorem genHasType_complete [LawfulGenFor Nat (fun _ => True)] [LawfulGenFor Bool (fun _ => True)] +theorem genHasType_complete [LawfulGenFor Nat (fun _ => True)] (τ : Ty) (e : Expr) (h : HasType e τ) : ∃ size, some e ∈ SetGen.support (genHasType (G := SetGen.Set) size τ size) := ... -theorem genWellTypedStmt_sound - [LawfulGenFor Nat (fun _ => True)] [LawfulGenFor Bool (fun _ => True)] +theorem genWellFormed_sound + [LawfulGenFor Nat (fun _ => True)] [LawfulGenFor Ty (fun _ => True)] - (size : Nat) (s : Stmt) : - some s ∈ SetGen.support (genWellTypedStmt (G := SetGen.Set) size size) → WellTypedStmt s := ... + (size : Nat) (p : Prog) : + some p ∈ SetGen.support (genWellFormed (G := SetGen.Set) size size) → WellFormed p := ... ``` The `LawfulGenFor` constraint gives the proof access to `LawfulGenFor.sound_and_complete`. Since any instance resolved for `GenFor Nat (fun _ => True)` must come from a `LawfulGenFor` instance (once the system invariant holds), the proof is sound regardless of which instance was picked. diff --git a/SpecimenTest/BridgeBacktrackMockup.lean b/SpecimenTest/BridgeBacktrackMockup.lean new file mode 100644 index 0000000..8fbbc87 --- /dev/null +++ b/SpecimenTest/BridgeBacktrackMockup.lean @@ -0,0 +1,445 @@ +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-BRIDGE.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 -/ + +def backtrack [Gen G] (gs : List (Nat × (Unit → BacktrackGen G α))) : BacktrackGen G α := + ⟨go gs⟩ +where + go : List (Nat × (Unit → BacktrackGen G α)) → G (Option α) + | [] => pure none + | [(_, g)] => (g ()).run + | gs => do + let idx ← RandomChoice.choose 0 (gs.length - 1) (by omega) + let (_, g) := gs[idx.down]! + match ← (g ()).run with + | some a => pure (some a) + | none => go (gs.eraseIdx idx.down) + termination_by gs => gs.length + +/-! ## 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 random selection without retry. For non-backtracking generators. -/ +def frequency [Gen G] (default : G α) (gs : List (Nat × (Unit → G α))) : G α := + match gs with + | [] => default + | [(_, g)] => g () + | gs => do + let idx ← RandomChoice.choose 0 (gs.length - 1) (by omega) + let (_, g) := gs[idx.down]! + g () + +/-! ## 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}" \ No newline at end of file diff --git a/SpecimenTest/BridgeDecOptMockup.lean b/SpecimenTest/BridgeDecOptMockup.lean deleted file mode 100644 index 4e11c20..0000000 --- a/SpecimenTest/BridgeDecOptMockup.lean +++ /dev/null @@ -1,157 +0,0 @@ -import Plausible - -/-! -# Specimen–Basalt Bridge Mockup: DecOpt Example - -This file demonstrates how the proposed Basalt-compatible DecOpt typeclass -works within generators, with execution via Plausible.Gen. --/ - -open Lean.Order - -namespace MockDecOpt - -/-! ## Basalt infrastructure (same as BridgeMockup.lean) -/ - -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 - -def backtrack [Gen G] (gs : List (Nat × (Unit → BacktrackGen G α))) : BacktrackGen G α := - ⟨go gs⟩ -where - go : List (Nat × (Unit → BacktrackGen G α)) → G (Option α) - | [] => pure none - | [(_, g)] => (g ()).run - | gs => do - let idx ← RandomChoice.choose 0 (gs.length - 1) (by omega) - let (_, g) := gs[idx.down]! - match ← (g ()).run with - | some a => pure (some a) - | none => go (gs.eraseIdx idx.down) - termination_by gs => gs.length - -class GenFor (α : Type) (P : α → Prop) where - gen : ∀ {G : Type → Type} [Gen G], G α - -/-! ## DecOpt: Basalt-compatible checker -/ - -/-- A partial decision procedure for P, polymorphic over Gen G. - Returns some true/false if decided, none if can't decide (backtrack). -/ -class DecOpt (P : Prop) where - decOpt : ∀ {G : Type → Type} [Gen G], Nat → BacktrackGen G Bool - -/-- Any Decidable instance gives a DecOpt that never fails. -/ -instance (priority := low) [Decidable P] : DecOpt P where - decOpt _ := pure (decide P) - -/-! ## Example: generate-then-check with a bounded constraint -/ - -instance : GenFor Nat (fun _ => True) where - gen := do - let n ← RandomChoice.choose 0 20 (by omega) - pure n.down - -/-- Generate a pair (a, b) where a ≤ b and both are in [lo, hi]. - Strategy: generate freely, then check constraints via DecOpt. - Multiple branches allow retrying on failure. -/ -def genSortedBounded [Gen G] [GenFor Nat (fun _ => True)] - (lo hi : Nat) (_initSize : Nat) : (size : Nat) → BacktrackGen G (Nat × Nat) - | _ => - let branch : Unit → BacktrackGen G (Nat × Nat) := fun () => do - let a ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Nat) - let b ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Nat) - -- Check all constraints using DecOpt; fail (backtrack) if any don't hold - match ← DecOpt.decOpt (P := decide (lo ≤ a ∧ a ≤ hi ∧ lo ≤ b ∧ b ≤ hi ∧ a ≤ b) = true) 0 with - | true => pure (a, b) - | false => BacktrackGen.fail - -- Repeat the branch to give multiple retry attempts - backtrack [(1, branch), (1, branch), (1, branch), (1, branch), (1, branch), - (1, branch), (1, branch), (1, branch), (1, branch), (1, branch)] - -end MockDecOpt - -open MockDecOpt - --- Run genSortedBounded with lo=0, hi=20 (matches generator range for high success rate) -#eval! do - IO.println "=== genSortedBounded (lo=0, hi=20, size=10) ===" - let mut successes := 0 - for _ in List.range 50 do - try - let result ← Plausible.Gen.run - (BacktrackGen.toPlausibleGen (genSortedBounded (G := Plausible.Gen) 0 20 10 0)) 10 - IO.println s!" success: {repr result}" - successes := successes + 1 - catch _ => pure () - IO.println s!" ({successes}/50 attempts succeeded)" diff --git a/SpecimenTest/BridgeMockup.lean b/SpecimenTest/BridgeMockup.lean deleted file mode 100644 index ac7a2ec..0000000 --- a/SpecimenTest/BridgeMockup.lean +++ /dev/null @@ -1,333 +0,0 @@ -import Plausible - -/-! -# Specimen–Basalt Bridge Mockup: Running Example - -This file mocks up the proposed generator structure using Basalt's actual Gen class -definition (which depends only on core Lean's Lean.Order) and demonstrates execution -via Plausible's Gen monad. --/ - -open Lean.Order - -/-! ## Basalt Gen class (copied from Basalt/Gen.lean) -/ - -namespace Mock - -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 - -/-! ## Plausible.Gen as a Basalt Gen instance (adapted from Basalt/PlausibleGen.lean) -/ - -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⟩ - -/-- Unwrap BacktrackGen to Plausible.Gen, throwing on failure. -/ -def toPlausibleGen (x : BacktrackGen Plausible.Gen α) : Plausible.Gen α := do - match ← x.run with - | some a => pure a - | none => throw (.genError "backtracking exhausted") - -def BacktrackGen.toGen [Gen G] [Inhabited α] (g : BacktrackGen G α) : G α := do - match ← g.run with - | some a => pure a - | none => pure default -- ⊥ (divergence) - -end BacktrackGen - -/-! ## backtrack combinator -/ - -def backtrack [Gen G] (gs : List (Nat × (Unit → BacktrackGen G α))) : BacktrackGen G α := - ⟨go gs⟩ -where - go : List (Nat × (Unit → BacktrackGen G α)) → G (Option α) - | [] => pure none - | [(_, g)] => (g ()).run - | gs => do - let idx ← RandomChoice.choose 0 (gs.length - 1) (by omega) - let (_, g) := gs[idx.down]! - match ← (g ()).run with - | some a => pure (some a) - | none => go (gs.eraseIdx idx.down) - termination_by gs => gs.length - -/-! ## GenFor / BacktrackGenFor 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 α - -/-! ## Running example -/ - -inductive Ty | nat | bool - deriving Repr, Inhabited, BEq - -inductive Expr - | litNat (n : Nat) - | litBool (b : Bool) - | isZero (e : Expr) - deriving Repr, Inhabited - -inductive Stmt - | expr (e : Expr) - | letBind (x : Nat) (e : Expr) (body : Stmt) - | assert (e : Expr) (τ : Ty) - deriving Repr, Inhabited - -inductive HasType : Expr → Ty → Prop - | litNat (n : Nat) : HasType (.litNat n) .nat - | litBool (b : Bool) : HasType (.litBool b) .bool - | isZero (e : Expr) : HasType e .nat → HasType (.isZero e) .bool - -inductive WellTypedStmt : Stmt → Prop - | expr (e : Expr) (τ : Ty) : HasType e τ → WellTypedStmt (.expr e) - | letBind (x : Nat) (e : Expr) (body : Stmt) (τ : Ty) : - HasType e τ → WellTypedStmt body → WellTypedStmt (.letBind x e body) - | assert (e : Expr) (τ : Ty) : HasType e τ → WellTypedStmt (.assert e τ) - -/-! ## GenFor instances for leaf types -/ - -instance : GenFor Nat (fun _ => True) where - gen := do - -- Simple geometric distribution - let n ← RandomChoice.choose 0 100 (by omega) - pure n.down - -instance : GenFor Bool (fun _ => True) where - gen := do - let n ← RandomChoice.choose 0 1 (by omega) - pure (n.down == 0) - -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) - -/-! ## genHasType: the derived constrained generator -/ - -def genHasType [Gen G] [GenFor Nat (fun _ => True)] [GenFor Bool (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.litNat n) - | .bool => do - let b ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Bool) - pure (Expr.litBool b)), - (1, fun () => match τ with - | .bool => do - let b ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Bool) - pure (Expr.litBool b) - | .nat => BacktrackGen.fail)] - | size + 1 => backtrack [ - (1, fun () => match τ with - | .nat => do - let n ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Nat) - pure (Expr.litNat n) - | .bool => do - let b ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Bool) - pure (Expr.litBool b)), - (1, fun () => match τ with - | .bool => do - let b ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Bool) - pure (Expr.litBool b) - | .nat => BacktrackGen.fail), - (size + 1, fun () => match τ with - | .bool => do - let e ← genHasType initSize Ty.nat size - pure (Expr.isZero e) - | .nat => BacktrackGen.fail)] - -/-! ## Register genHasType as a BacktrackGenFor instance -/ - -instance [GenFor Nat (fun _ => True)] [GenFor Bool (fun _ => True)] - : ∀ τ, BacktrackGenFor Expr (fun e => HasType e τ) := - fun τ => ⟨fun {_} [_] size => genHasType size τ size⟩ - -/-! ## genWellTypedStmt: uses BacktrackGenFor for cross-generator call -/ - -def genWellTypedStmt [Gen G] [GenFor Nat (fun _ => True)] [GenFor Bool (fun _ => True)] - [GenFor Ty (fun _ => True)] - [∀ τ, BacktrackGenFor Expr (fun e => HasType e τ)] - (initSize : Nat) : (size : Nat) → BacktrackGen G Stmt - | 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 (Stmt.expr e)), - (1, fun () => do - let τ ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Ty) - let e ← BacktrackGenFor.gen (P := fun e => HasType e τ) initSize - pure (Stmt.assert e τ))] - | 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 (Stmt.expr e)), - (1, fun () => do - let τ ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Ty) - let e ← BacktrackGenFor.gen (P := fun e => HasType e τ) initSize - pure (Stmt.assert e τ)), - (size + 1, fun () => do - let body ← genWellTypedStmt initSize size - let τ ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Ty) - let e ← BacktrackGenFor.gen (P := fun e => HasType e τ) initSize - let x ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Nat) - pure (Stmt.letBind x e body))] - -/-! ## frequency combinator (for non-backtracking generators) -/ - -/-- Weighted random selection without retry. For non-backtracking generators. -/ -def frequency [Gen G] (default : G α) (gs : List (Nat × (Unit → G α))) : G α := - match gs with - | [] => default - | [(_, g)] => g () - | gs => do - let idx ← RandomChoice.choose 0 (gs.length - 1) (by omega) - let (_, g) := gs[idx.down]! - g () - -/-! ## 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 - -/-! ## Execution via Plausible -/ - -end Mock - -open Mock - -/-! ## Status quo: what Specimen emits today for unconstrained generators (using Plausible directly) - This verifies that the "What Specimen emits today" code in SPECIMEN-BASALT-BRIDGE.md Section 6 - is accurate. -/ -namespace StatusQuo -open Plausible - -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 StatusQuo - --- Run genHasType at Plausible.Gen and print results. -#eval! do - IO.println "=== genHasType (τ = .nat, size = 3) ===" - 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 "=== genHasType (τ = .bool, size = 3) ===" - for _ in List.range 5 do - let result ← Plausible.Gen.run - (BacktrackGen.toPlausibleGen (genHasType (G := Plausible.Gen) 3 .bool 3)) 10 - IO.println s!" {repr result}" - -#eval! do - IO.println "=== genWellTypedStmt (size = 3) ===" - for _ in List.range 5 do - let result ← Plausible.Gen.run - (BacktrackGen.toPlausibleGen (genWellTypedStmt (G := Plausible.Gen) 3 3)) 10 - IO.println s!" {repr result}" - -#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}" \ No newline at end of file From 177d1ae7b5a36bf3481241df509ff7280068def2 Mon Sep 17 00:00:00 2001 From: Mike Hicks Date: Wed, 3 Jun 2026 12:51:24 -0400 Subject: [PATCH 3/8] updates after doing a some POC work on proofs --- SPECIMEN-BASALT-BRIDGE.md | 71 +++++++++++++++---------- SpecimenTest/BridgeBacktrackMockup.lean | 25 +++++---- 2 files changed, 57 insertions(+), 39 deletions(-) diff --git a/SPECIMEN-BASALT-BRIDGE.md b/SPECIMEN-BASALT-BRIDGE.md index bb5f26b..7afae4e 100644 --- a/SPECIMEN-BASALT-BRIDGE.md +++ b/SPECIMEN-BASALT-BRIDGE.md @@ -224,23 +224,29 @@ instance [Gen G] : Monad (BacktrackGen G) where ### The `backtrack` combinator ```lean -/-- Weighted backtracking: randomly pick a branch by weight, try it, retry remaining on failure. -/ +/-- Weighted backtracking: randomly pick a branch, try it, retry remaining on failure. + Uses fuel (initially gs.length) for structural termination. -/ def backtrack [Gen G] (gs : List (Nat × (Unit → BacktrackGen G α))) : BacktrackGen G α := - ⟨go gs⟩ + ⟨go gs.length gs⟩ where - go : List (Nat × (Unit → BacktrackGen G α)) → G (Option α) - | [] => pure none - | [(_, g)] => (g ()).run - | gs => do + go : Nat → List (Nat × (Unit → BacktrackGen G α)) → G (Option α) + | _, [] => pure none + | 0, _ => pure none + | fuel + 1, gs@(_ :: _) => do let idx ← RandomChoice.choose 0 (gs.length - 1) (by omega) - let (_, g) := gs[idx.down]! - match ← (g ()).run with - | some a => pure (some a) - | none => go (gs.eraseIdx idx.down) - termination_by gs => gs.length + let i := idx.down + if hi : i < gs.length then + let (_, g) := gs[i] + match ← (g ()).run with + | some a => pure (some a) + | none => go fuel (gs.eraseIdx i) + else + pure none ``` -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. +This has identical operational semantics to Specimen's current `backtrack`: pick a branch randomly, run it, and if it returns `none` (failure), remove it from the pool and retry with decremented fuel. Termination is structural on the `fuel : Nat` parameter (which starts at `gs.length`, bounding retries to at most one attempt per branch). + +The key proof lemma for this combinator is `backtrack_mem_iff`, which states that `some a ∈ support ((backtrack gs).run)` iff there exists some branch `i` such that `some a ∈ support ((gs[i].2 ()).run)`. This reduces reasoning about backtracking to reasoning about individual branches, hiding the retry logic entirely. ### The `frequency` combinator @@ -706,25 +712,32 @@ The practical upshot for this plan: ### Proving correctness (at `SetGen.Set`) -With `[LawfulGenFor Nat (fun _ => True)]` in scope (which provides `GenFor Nat (fun _ => True)` via the subclass relationship), proofs compose modularly: +Soundness and completeness proofs for the running example have been carried out manually as a POC. The proof structure is as follows. + +**The key lemma** is `backtrack_mem_iff`, which characterizes membership in `backtrack`'s support: ```lean -theorem genHasType_sound [LawfulGenFor Nat (fun _ => True)] - (τ : Ty) (size : Nat) (e : Expr) : - some e ∈ SetGen.support (genHasType (G := SetGen.Set) size τ size) → HasType e τ := ... +theorem backtrack_mem_iff (gs : List (Nat × (Unit → BacktrackGen SetGen.Set α))) (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 — the random selection and retry logic is abstracted away. -theorem genHasType_complete [LawfulGenFor Nat (fun _ => True)] - (τ : Ty) (e : Expr) (h : HasType e τ) : - ∃ size, some e ∈ SetGen.support (genHasType (G := SetGen.Set) size τ size) := ... +**The predicate.** Because `GenFor Nat (fun _ => True)` generates naturals in a bounded range (0–100 in the example), the generator's support does not cover *all* well-typed expressions — only those whose leaf values fall within range and whose depth fits the size budget. The proven predicate is: -theorem genWellFormed_sound - [LawfulGenFor Nat (fun _ => True)] - [LawfulGenFor Ty (fun _ => True)] - (size : Nat) (p : Prog) : - some p ∈ SetGen.support (genWellFormed (G := SetGen.Set) size size) → WellFormed p := ... +```lean +def HasTypeBounded (τ : Ty) (size : Nat) (e : Expr) : Prop := + HasType e τ ∧ exprBounded size e ``` -The `LawfulGenFor` constraint gives the proof access to `LawfulGenFor.sound_and_complete`. Since any instance resolved for `GenFor Nat (fun _ => True)` must come from a `LawfulGenFor` instance (once the system invariant holds), the proof is sound regardless of which instance was picked. +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 `τ` within each branch. For the `isPos` branch, the `DecOpt` check (`decide (n ≠ 0)`) produces a `Bool` that is matched — only the `true` case reaches `pure (Expr.isPos n)`, directly yielding the `HasType.isPos` constructor with proof `n ≠ 0`. + +**Completeness** also proceeds by induction on `size`, constructing the appropriate branch index (`Fin gs.length`) for each `HasType` constructor. For example, `HasType.add` maps to branch index 2 in the `size + 1` case, with recursive appeals to the induction hypothesis for both subexpressions. + +**Compositionality.** In the full system with `LawfulGenFor` / `LawfulBacktrackGenFor` instances, these proofs compose modularly: the `genWellFormed` proof would discharge its `HasType` sub-generator obligations by appealing to the `LawfulBacktrackGenFor Expr (HasType · τ)` instance rather than inlining the `genHasType` proof. ## 8. Plan of Work @@ -751,9 +764,9 @@ The goal of this phase is to make Specimen-derived generators polymorphic over B #### Step 1.2: Prove SetGen support lemmas -- `backtrack_mem_iff`: `some a ∈ support (backtrack gs)` iff `some a ∈ support (gᵢ ())` for some `i` +- `backtrack_mem_iff`: `some a ∈ support ((backtrack gs).run)` iff `some a ∈ support ((gs[i].2 ()).run)` for some `i : Fin gs.length`. This is the key lemma for proving correctness of derived generators — it reduces backtracking to a disjunction over branches. (Proven now in a separate scratchfile.) - `frequency_mem_iff`: analogous for `frequency` -- Basic `liftGen`/`pure`/`bind` support lemmas +- Basic `liftGen`/`pure`/`bind` support lemmas (follow from Basalt's existing `SetGen.support_bind`, `SetGen.support_pure`) #### Step 1.3: Modify Specimen's constrained code emission (`derive_generator`) @@ -783,7 +796,7 @@ This step can proceed in parallel with Step 1.3 since the unconstrained deriver - Verify existing Specimen test cases still pass (expected output will change shape; update snapshots) - Verify `derive Arbitrary` produces working `GenFor` instances for standard test types (e.g., `Tree`, `Expr`) - Verify the `plausible` tactic works end-to-end with both constrained and unconstrained generators -- Write a manual soundness proof for the `HasType` example, demonstrating that a Specimen-derived generator can be proved sound at `SetGen.Set` given `LawfulGenFor` / `LawfulBacktrackGenFor` instances for sub-generators +- Write a manual soundness proof for the `HasType` example, demonstrating that a Specimen-derived generator can be proved sound at `SetGen.Set` given `LawfulGenFor` / `LawfulBacktrackGenFor` instances for sub-generators. (Complete soundness and completeness proofs of `genHasType` in a scratchfile.) ### Phase 2: Lawful generation (with proof synthesis) @@ -806,6 +819,8 @@ For each derived **constrained** generator, Specimen emits a proof that the gene Sub-generator proof obligations are discharged by the `LawfulGenFor` / `LawfulBacktrackGenFor` instances of sub-generators (available via typeclass resolution). +This structure has been validated by hand-proving soundness and completeness for the running example's `genHasType`. The proofs use `induction size`, `backtrack_mem_iff`, `fin_cases` on branch indices, and `simp` over `SetGen.support` lemmas — a pattern amenable to automation. + Emit `LawfulBacktrackGenFor` instances bundling generator + proof. For each derived **unconstrained** generator (`derive Arbitrary`), Specimen emits a `LawfulGenFor α (fun _ => True)` instance. The property is trivially `True`, so the proof obligation reduces to: diff --git a/SpecimenTest/BridgeBacktrackMockup.lean b/SpecimenTest/BridgeBacktrackMockup.lean index 8fbbc87..9dfe291 100644 --- a/SpecimenTest/BridgeBacktrackMockup.lean +++ b/SpecimenTest/BridgeBacktrackMockup.lean @@ -107,18 +107,21 @@ end BacktrackGen /-! ## Combinators -/ def backtrack [Gen G] (gs : List (Nat × (Unit → BacktrackGen G α))) : BacktrackGen G α := - ⟨go gs⟩ + ⟨go gs.length gs⟩ where - go : List (Nat × (Unit → BacktrackGen G α)) → G (Option α) - | [] => pure none - | [(_, g)] => (g ()).run - | gs => do + go : Nat → List (Nat × (Unit → BacktrackGen G α)) → G (Option α) + | _, [] => pure none + | 0, _ => pure none + | fuel + 1, gs@(_ :: _) => do let idx ← RandomChoice.choose 0 (gs.length - 1) (by omega) - let (_, g) := gs[idx.down]! - match ← (g ()).run with - | some a => pure (some a) - | none => go (gs.eraseIdx idx.down) - termination_by gs => gs.length + let i := idx.down + if hi : i < gs.length then + let (_, g) := gs[i] + match ← (g ()).run with + | some a => pure (some a) + | none => go fuel (gs.eraseIdx i) + else + pure none /-! ## Typeclasses -/ @@ -249,7 +252,7 @@ def genWellFormed [Gen G] [GenFor Nat (fun _ => True)] [GenFor Ty (fun _ => True 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 [ + | _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 From 07a1950c7db15d0d22cd3ff18f492a5e99dd03f7 Mon Sep 17 00:00:00 2001 From: Mike Hicks Date: Wed, 3 Jun 2026 14:27:02 -0400 Subject: [PATCH 4/8] Updates based on some proof work --- SPECIMEN-BASALT-BRIDGE.md | 52 ++++++++++++++++++++++++++++++++------- 1 file changed, 43 insertions(+), 9 deletions(-) diff --git a/SPECIMEN-BASALT-BRIDGE.md b/SPECIMEN-BASALT-BRIDGE.md index 7afae4e..06183f4 100644 --- a/SPECIMEN-BASALT-BRIDGE.md +++ b/SPECIMEN-BASALT-BRIDGE.md @@ -366,16 +366,25 @@ To this end, we introduce two additional typeclasses: Provides only soundness & completeness — weaker than Basalt's LawfulGenerator which also requires almost-sure termination and cost bounds. -/ class LawfulGenFor (α : Type) (P : α → Prop) extends GenFor α P where - sound_and_complete : IsSoundAndComplete (gen (G := SPMF)) P + sound_and_complete : SetGen.IsSoundAndComplete (gen (G := SetGen.Set)) P -/-- A lawful backtracking generator: proves that successful outputs satisfy P. -/ -class LawfulBacktrackGenFor (α : Type) (P : α → Prop) extends BacktrackGenFor α P where - sound_and_complete : ∀ size a, - some a ∈ SPMF.support (gen (G := SPMF) size) ↔ P a +/-- A lawful backtracking generator: proves that successful outputs satisfy a size-indexed + bounded predicate at SetGen.Set. The Bounded predicate refines P with size/range + constraints imposed by the implementation (e.g., bounded leaf values, bounded depth). -/ +class LawfulBacktrackGenFor (α : Type) (P : α → Prop) (Bounded : Nat → α → Prop) + extends BacktrackGenFor α P 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) ``` Instances of these typeclasses are sure to be sound and complete, i.e., lawful (to a minimal degree). Thus users of them can rely on that lawfulness when proving lawfulness locally. +**Why `Bounded` is separate from `P`.** The property `P` (e.g., `HasType e τ`) is the *semantic* specification the user cares about — it's what appears in `derive_generator (fun τ => ∃ e, HasType e τ)`. 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 (e.g., `HasTypeBounded τ`) 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 (see "Fuel vs size vs `partial_fixpoint`" in Section 7). If generators were defined via `partial_fixpoint` instead — where the generator's support at the fixpoint covers all values satisfying `P` — then `Bounded` would be unnecessary and the class could use a simple `iff` with `P`. The `Bounded` parameter is essentially the price of fuel-based termination; eliminating it is a benefit of moving to `partial_fixpoint` in the future. + **Relationship to Basalt's `LawfulGenerator`:** Basalt defines `LawfulGenerator` as a property of a *specific generator term* — it says "this particular generator `g` is sound, complete, terminating, and cost-bounded." Our `LawfulGenFor` and `LawfulBacktrackGenFor` serve a different purpose: they are *typeclasses for resolution* — they say "there exists a generator for this type/property findable by typeclass synthesis, and it is sound and complete." They intentionally omit cost and termination requirements for simplicity; in the future, these could be strengthened to require `LawfulGenerator` of the underlying term, at which point the system would provide full lawfulness guarantees. ### Standard `GenFor` instances @@ -663,6 +672,29 @@ This invariant is enforced by the two-step roadmap (see Section 8): 1. First, Specimen emits generators with `GenFor` / `BacktrackGenFor` constraints (for execution only). 2. Then, Specimen is upgraded to also emit `LawfulGenFor` / `LawfulBacktrackGenFor` instances with synthesized proofs, ensuring every derived generator is lawful. +### Instance diamond with `LawfulBacktrackGenFor` + +A practical issue arises from `LawfulBacktrackGenFor` extending `BacktrackGenFor`: when both a standalone `BacktrackGenFor` instance and a `LawfulBacktrackGenFor` instance exist for the same type/predicate, typeclass synthesis may resolve `BacktrackGenFor.gen` to the standalone instance inside a generator body, while `LawfulBacktrackGenFor.sound`/`.complete` expect the inherited instance. Even though both produce the same generator, Lean treats them as distinct terms, causing type mismatches in proofs. + +**Solution:** Generators that need lawfulness proofs must explicitly route through the lawful instance: + +```lean +def genWellFormed' [Gen G] [GenFor Nat (fun _ => True)] [GenFor Ty (fun _ => True)] + [inst : ∀ τ, LawfulBacktrackGenFor Expr (fun e => HasType e τ) (HasTypeBounded τ)] + (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 _ _ ((inst τ).toBacktrackGenFor) _ _ initSize + pure (Prog.expr e)), + ...] +``` + +**Implication for Specimen's code emission:** When emitting generators that will carry proofs (Phase 2), Specimen must either: +- Emit `@BacktrackGenFor.gen` with explicit instance selection via the lawful instance's `.toBacktrackGenFor` field, or +- Ensure that the `LawfulBacktrackGenFor` instance is the *only* `BacktrackGenFor` instance registered for that type/predicate (i.e., don't register a separate standalone instance once the lawful one exists), or +- Use instance priority to ensure the lawful instance wins synthesis + ### Mutual recursion Specimen supports mutually recursive inductive relations. For mutually recursive generators, the emitted code uses Lean's `mutual ... end` block with direct name calls between the 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 — mutual generators call each other by name, and only *external* callers go through typeclass resolution. @@ -737,7 +769,7 @@ where `exprBounded size e` requires leaf naturals ≤ 100 and `add`-nesting ≤ **Completeness** also proceeds by induction on `size`, constructing the appropriate branch index (`Fin gs.length`) for each `HasType` constructor. For example, `HasType.add` maps to branch index 2 in the `size + 1` case, with recursive appeals to the induction hypothesis for both subexpressions. -**Compositionality.** In the full system with `LawfulGenFor` / `LawfulBacktrackGenFor` instances, these proofs compose modularly: the `genWellFormed` proof would discharge its `HasType` sub-generator obligations by appealing to the `LawfulBacktrackGenFor Expr (HasType · τ)` instance rather than inlining the `genHasType` proof. +**Compositionality.** In the full system with `LawfulGenFor` / `LawfulBacktrackGenFor` instances, these proofs compose modularly: the `genWellFormed` proof discharges its `HasType` sub-generator obligations by appealing to the `LawfulBacktrackGenFor Expr (HasType · τ) (HasTypeBounded τ)` instance's `.sound` and `.complete` fields rather than inlining the `genHasType` proof. This has been validated: soundness and completeness of `genWellFormed` are proved using `backtrack_mem_iff` to decompose into branches, then `backtrackGen_bind_mem` / `backtrackGen_pure_mem` to decompose the sequential `BacktrackGen` bind chain within each branch, and finally `(inst τ).sound` / `(inst τ).complete` to discharge sub-generator obligations. The generator must explicitly route through the lawful instance to avoid the instance diamond described in "Instance diamond with `LawfulBacktrackGenFor`" above. ## 8. Plan of Work @@ -766,7 +798,9 @@ The goal of this phase is to make Specimen-derived generators polymorphic over B - `backtrack_mem_iff`: `some a ∈ support ((backtrack gs).run)` iff `some a ∈ support ((gs[i].2 ()).run)` for some `i : Fin gs.length`. This is the key lemma for proving correctness of derived generators — it reduces backtracking to a disjunction over branches. (Proven now in a separate scratchfile.) - `frequency_mem_iff`: analogous for `frequency` -- Basic `liftGen`/`pure`/`bind` support lemmas (follow from Basalt's existing `SetGen.support_bind`, `SetGen.support_pure`) +- `backtrackGen_bind_mem`: `some b ∈ support ((x >>= f).run)` iff `∃ a, some a ∈ support x.run ∧ some b ∈ support ((f a).run)`. This is essential for decomposing sequential composition inside `BacktrackGen` branches — without it, proofs about composite generators (like `genWellFormed`) are extremely difficult because `BacktrackGen`'s bind introduces nested `match` on `Option` that doesn't reduce with `simp`. +- `backtrackGen_pure_mem`: `some b ∈ support ((pure a : BacktrackGen SetGen.Set α).run)` iff `b = a`. The base case for branch decomposition. +- Basic `liftGen` support lemma (follows from the above and Basalt's existing `SetGen.support_bind`, `SetGen.support_pure`) #### Step 1.3: Modify Specimen's constrained code emission (`derive_generator`) @@ -804,8 +838,8 @@ The goal of this phase is to make Specimen emit `LawfulGenFor` / `LawfulBacktrac #### Step 2.1: Define `LawfulGenFor` and `LawfulBacktrackGenFor` in Basalt -- Define `LawfulGenFor` extending `GenFor` with soundness/completeness at `SPMF` -- Define `LawfulBacktrackGenFor` extending `BacktrackGenFor` similarly +- Define `LawfulGenFor` extending `GenFor` with soundness/completeness at `SetGen.Set` +- Define `LawfulBacktrackGenFor` extending `BacktrackGenFor` with a `Bounded : Nat → α → Prop` parameter and sound/complete fields at `SetGen.Set` - Provide `LawfulGenFor` instances for standard types (using existing Basalt proofs like `Nat.arbitrary_support`) #### Step 2.2: Synthesize soundness/completeness proofs in Specimen From 69c6d95faca75bd7a5f8b8dd4a19ffa4662f9c7f Mon Sep 17 00:00:00 2001 From: Mike Hicks Date: Thu, 4 Jun 2026 08:07:24 -0400 Subject: [PATCH 5/8] benchmark comparing option-based and exception-based approach with corrected backtrack combinator; writeup in doc --- SPECIMEN-BASALT-BRIDGE.md | 66 ++- SpecimenTest/BridgeBacktrackMockup.lean | 43 +- SpecimenTest/BridgeBenchmark.lean | 509 ++++++++++++++++++++++++ 3 files changed, 602 insertions(+), 16 deletions(-) create mode 100644 SpecimenTest/BridgeBenchmark.lean diff --git a/SPECIMEN-BASALT-BRIDGE.md b/SPECIMEN-BASALT-BRIDGE.md index 06183f4..62f2ad6 100644 --- a/SPECIMEN-BASALT-BRIDGE.md +++ b/SPECIMEN-BASALT-BRIDGE.md @@ -740,7 +740,71 @@ The practical upshot for this plan: ### Performance considerations -`BacktrackGen` adds an `Option` wrapper at every bind within backtracking branches. For deeply nested generators this means more allocations and pattern-matches compared to today's exception-based approach. In practice this overhead is negligible — the dominant cost is in `choose` calls and the retries themselves, not the `Option` wrapping. If profiling reveals otherwise, the `toPlausibleGen` boundary could be pushed deeper (converting to exception-based execution earlier), at the cost of limiting provability. +`BacktrackGen` adds an `Option` wrapper at every bind within backtracking branches. For deeply nested generators this means more allocations and pattern-matches compared to today's exception-based approach. Benchmarking (see `SpecimenTest/BridgeBenchmark.lean`) shows: + +**Benchmark results** (bridge/legacy ratio, lower = bridge is faster): + +| Scenario | Ratio | Notes | +|---|---|---| +| Recursive generator (5-ary `nary` 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 overhead arises when branches consist almost entirely of `liftGen` calls (no recursive sub-generator calls) and multiple branches are tried per iteration (due to frequent failure and retry), amplifying the per-`liftGen` `Option` wrap/unwrap cost across many executed branches. In realistic generators (like Cedar's `HasType` with 23 constructors and recursive sub-generators), branch bodies are dominated by recursive calls — 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` (producing `spec_0._redArg` variants). + +#### Optimization: batching consecutive `liftGen` calls + +When Specimen emits code where multiple unconstrained field generations appear consecutively (before any backtracking operation), they can be batched into a single `liftGen`: + +```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 inner `do` block runs in `G` directly (no `Option` overhead). This is purely a code-emission optimization in Specimen — the generated code's semantics are unchanged. 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`), batching doesn't apply. For this case, a fused combinator eliminates the intermediate `Option`: + +```lean +/-- Fused liftGen + bind: runs a non-failing G α and passes the result directly + to a backtracking continuation, without wrapping in some and immediately unwrapping. -/ +@[inline] def BacktrackGen.liftBind [Gen G] (g : G α) (f : α → BacktrackGen G β) : BacktrackGen G β := + ⟨do let a ← g; (f a).run⟩ +``` + +This handles patterns like: +```lean +-- Without liftBind: wraps n in some, then bind unwraps it +let n ← BacktrackGen.liftGen (GenFor.gen : G Nat) +let e ← BacktrackGenFor.gen (P := fun e => HasType e τ) initSize -- may fail + +-- With liftBind: no intermediate Option +BacktrackGen.liftBind (GenFor.gen : G Nat) (fun n => do + let e ← BacktrackGenFor.gen (P := fun e => HasType e τ) initSize + ...) +``` + +In practice, Specimen's emission order places all unconstrained generations before constrained sub-generator calls, so **batching handles the common case**. `liftBind` covers the remaining interleaved cases (e.g., generating a type `τ`, calling a sub-generator parameterized by `τ`, then generating another unconstrained field). Both optimizations are purely in Specimen's code emission — they require no changes to the `BacktrackGen` API or Basalt infrastructure. + +Neither optimization affects provability: `liftBind g f` has the same denotation as `bind (liftGen g) f` at all Basalt interpretations (the `some` wrap/unwrap is semantically invisible). The proof lemma is trivial: +```lean +theorem liftBind_eq_bind_liftGen [Gen G] (g : G α) (f : α → BacktrackGen G β) : + liftBind g f = bind (liftGen g) f +``` ### Proving correctness (at `SetGen.Set`) diff --git a/SpecimenTest/BridgeBacktrackMockup.lean b/SpecimenTest/BridgeBacktrackMockup.lean index 9dfe291..3907876 100644 --- a/SpecimenTest/BridgeBacktrackMockup.lean +++ b/SpecimenTest/BridgeBacktrackMockup.lean @@ -106,22 +106,35 @@ 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 gs⟩ + ⟨go gs.length (sumWeights gs) gs⟩ where - go : Nat → List (Nat × (Unit → BacktrackGen G α)) → G (Option α) - | _, [] => pure none - | 0, _ => pure none - | fuel + 1, gs@(_ :: _) => do - let idx ← RandomChoice.choose 0 (gs.length - 1) (by omega) - let i := idx.down - if hi : i < gs.length then - let (_, g) := gs[i] - match ← (g ()).run with - | some a => pure (some a) - | none => go fuel (gs.eraseIdx i) - else - pure none + 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 -/ @@ -445,4 +458,4 @@ end UnconstrainedStatusQuo 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}" \ No newline at end of file + IO.println s!" {repr result}" diff --git a/SpecimenTest/BridgeBenchmark.lean b/SpecimenTest/BridgeBenchmark.lean new file mode 100644 index 0000000..077eb20 --- /dev/null +++ b/SpecimenTest/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 From 07346f5d02395b596a1572b2bbc8b84fd1060c52 Mon Sep 17 00:00:00 2001 From: Mike Hicks Date: Thu, 4 Jun 2026 14:24:11 -0400 Subject: [PATCH 6/8] reorg doc to make more readable, fix bug in mockup --- SPECIMEN-BASALT-BRIDGE.md | 746 ++++++++++-------------- SpecimenTest/BridgeBacktrackMockup.lean | 21 +- 2 files changed, 311 insertions(+), 456 deletions(-) diff --git a/SPECIMEN-BASALT-BRIDGE.md b/SPECIMEN-BASALT-BRIDGE.md index 62f2ad6..f737981 100644 --- a/SPECIMEN-BASALT-BRIDGE.md +++ b/SPECIMEN-BASALT-BRIDGE.md @@ -1,9 +1,29 @@ # 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. +## 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. +--- + ## 1. Status Quo and Goal ### The three frameworks @@ -35,53 +55,16 @@ Basalt also defines correctness classes for individual generator terms: - `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 -### Current dependency structure - -``` -┌──────────┐ ┌──────────┐ -│ Plausible│◄────────│ Specimen │ -└────┬─────┘ └──────────┘ - │ - ▼ -┌──────────┐ -│ Basalt │ -└──────────┘ -``` - -Specimen and Basalt are currently unrelated — Specimen-derived generators cannot be reasoned about using Basalt's correctness classes. - -### Target dependency structure - -``` -┌──────────┐ -│ Plausible│ -└────┬─────┘ - │ - ▼ -┌──────────┐ ┌──────────┐ -│ Basalt │◄────────│ Specimen │ -└──────────┘ └──────────┘ -``` - -Specimen will depend on Basalt for `Gen`, `BacktrackGen`, and `backtrack`. The `plausible` tactic will still work: Specimen emits `ArbitrarySizedSuchThat` instances (as it does today) whose body calls `BacktrackGen.toPlausibleGen` to produce the `Plausible.Gen α` that Plausible's machinery expects. - ### 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` -### Non-goals - -The following are explicitly **not** addressed by this plan: - -- **Changing user-facing syntax.** The `derive_generator (fun τ => ∃ e, HasType e τ)` command syntax remains unchanged. The difference is purely in what code gets emitted. -- **Enumerators.** Specimen's deterministic enumerators (`EnumSizedSuchThat`) are a separate concern from random generators and are not addressed here. (But we should address them similarly.) -- **Almost-sure termination proofs for derived generators.** Phase 2 proves soundness/completeness only. Termination and cost bounds for Specimen-derived generators are future work (they would require `partial_fixpoint`-based emission). - ### Example -We will use the following small typed language throughout this document to illustrate the changes. This example is designed to exercise all three mechanisms: backtracking (multiple constructors per type, some of which fail), checkers (the `isPos` constructor has a decidable guard `n ≠ 0`), and cross-generator composition (`WellFormed` calls `HasType`). +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 @@ -186,32 +169,20 @@ instance : ArbitrarySizedSuchThat Prog (fun p => WellFormed p) where 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 four problems: - -**Problem 1: Backtracking.** The generators use Plausible's `throw`/`tryCatch` for backtracking. Basalt's `Gen` class has no exception mechanism — only `choose`, `bind`, `pure`, and ⊥ (`default`). We need a backtracking mechanism that works across all Basalt interpretations. (Addressed in Section 2.) - -**Problem 2: Sub-generator resolution.** The generators call sub-generators via Plausible-specific typeclasses (`Arbitrary`, `ArbitrarySizedSuchThat`). These typeclasses wrap `Plausible.Gen` and cannot be used polymorphically over `G`. We need a Basalt-compatible typeclass for sub-generator lookup. (Addressed in Section 3.) - -**Problem 3: Checkers.** In more complex examples, Specimen invokes `DecOpt.decOpt` within generators to check hypotheses that involve only fixed (input) variables. `DecOpt.decOpt` returns `Except GenError Bool` — a Plausible-specific type. Checkers must also be made polymorphic over `G`. (Addressed in Section 4. In our running example, the `isPos` constructor triggers this: after generating `n`, Specimen checks `n ≠ 0` via `DecOpt`.) - -**Problem 4: Unconstrained generators.** Specimen's `derive Arbitrary` emits generators using Plausible-specific `Gen.frequency` / `Gen.oneOfWithDefault` and `Arbitrary.arbitrary`. These must also become Basalt-polymorphic so they can serve as provably-correct `GenFor` instances for sub-generator resolution in constrained generators. (Addressed in Section 6.) +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. - Defined as a structure (not a type alias) so it can have its own Monad instance, - enabling do-notation within backtracking generators. -/ -structure BacktrackGen (G : Type → Type) (α : Type) where +/-- 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. -`BacktrackGen` is a `structure` (newtype) rather than a type alias so that it can have its own `Monad` instance. This allows `do`-notation within backtracking generators to bind `BacktrackGen G` values directly, threading `Option` automatically: - ```lean instance [Gen G] : Monad (BacktrackGen G) where pure a := ⟨pure (some a)⟩ @@ -224,49 +195,23 @@ instance [Gen G] : Monad (BacktrackGen G) where ### The `backtrack` combinator ```lean -/-- Weighted backtracking: randomly pick a branch, try it, retry remaining on failure. - Uses fuel (initially gs.length) for structural termination. -/ def backtrack [Gen G] (gs : List (Nat × (Unit → BacktrackGen G α))) : BacktrackGen G α := - ⟨go gs.length gs⟩ + ⟨go gs.length (sumWeights gs) gs⟩ where - go : Nat → List (Nat × (Unit → BacktrackGen G α)) → G (Option α) - | _, [] => pure none - | 0, _ => pure none - | fuel + 1, gs@(_ :: _) => do - let idx ← RandomChoice.choose 0 (gs.length - 1) (by omega) - let i := idx.down - if hi : i < gs.length then - let (_, g) := gs[i] - match ← (g ()).run with - | some a => pure (some a) - | none => go fuel (gs.eraseIdx i) - else - pure none + 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' ``` -This has identical operational semantics to Specimen's current `backtrack`: pick a branch randomly, run it, and if it returns `none` (failure), remove it from the pool and retry with decremented fuel. Termination is structural on the `fuel : Nat` parameter (which starts at `gs.length`, bounding retries to at most one attempt per branch). - -The key proof lemma for this combinator is `backtrack_mem_iff`, which states that `some a ∈ support ((backtrack gs).run)` iff there exists some branch `i` such that `some a ∈ support ((gs[i].2 ()).run)`. This reduces reasoning about backtracking to reasoning about individual branches, hiding the retry logic entirely. - -### The `frequency` combinator +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`). -For **non-backtracking** generators (like unconstrained `Arbitrary` derivations that use `Gen.frequency`), we provide a simpler combinator that picks by weight but does *not* retry on failure: - -```lean -/-- Weighted random selection without retry. For non-backtracking generators. -/ -def frequency [Gen G] (default : G α) (gs : List (Nat × (Unit → G α))) : G α := - match gs with - | [] => default - | [(_, g)] => g () - | gs => do - let idx ← RandomChoice.choose 0 (gs.length - 1) (by omega) - let (_, g) := gs[idx.down]! - g () -``` - -This is the Basalt-polymorphic replacement for `Plausible.Gen.frequency` / `Gen.oneOfWithDefault`. - -### The `liftGen` and `fail` helpers +### Helpers ```lean /-- Lift a non-failing G α into BacktrackGen G α. -/ @@ -278,7 +223,7 @@ def BacktrackGen.fail [Gen G] : BacktrackGen G α := ⟨pure none⟩ ``` -### Boundary: unwrapping `BacktrackGen` to `Gen` +### Boundary: unwrapping `BacktrackGen` At the outermost level — where a generator must produce a value for Plausible's testing machinery — we collapse the `Option`: @@ -294,103 +239,33 @@ def BacktrackGen.toPlausibleGen (g : BacktrackGen Plausible.Gen α) : Plausible. | none => throw (.genError "backtracking exhausted") ``` -### Why 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 — making the generated code verbose and error-prone. - -### 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 | - -Note: `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. +> **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` typeclass (for unconstrained types like `Nat`) and `ArbitrarySizedSuchThat` (for constrained types like well-typed expressions). But `Arbitrary` wraps `Plausible.Gen α` specifically — it cannot be used inside a polymorphic `G`. - -We need a Basalt-compatible typeclass mechanism that: - -1. Works at all Basalt interpretations (`SetGen.Set`, `SPMF`, `Plausible.Gen`) -2. Scales to large developments with many types -3. Supports modular correctness proofs about composite generators +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` -The key distinction we want to express in the typeclass setup is **backtracking vs non-backtracking** behavior — whether the generator can fail locally. Both kinds target a property `P` characterizing their output. - ```lean /-- A non-backtracking generator for type α whose outputs satisfy P. - Always succeeds (returns G α, not BacktrackGen G α). - For a truly unconstrained generator, P = fun _ => True. - Analogous to Plausible's Arbitrary, but polymorphic over Gen G. -/ + 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 (returns BacktrackGen G α = G (Option α)). - Takes a Nat fuel parameter for structural termination. + 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 naming reflects the role: "find me a generator **for** `α` satisfying `P`." The calling convention: +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`) -The `P` parameter characterizes what the generator produces: - -| Class | Example | Property `P` | -|---|---|---| -| `GenFor Nat (fun _ => True)` | Generates any `Nat`, always succeeds | `True` | -| `GenFor (Tree Nat) (Tree.isBST 0 10)` | `Tree.genBST 0 10`, always succeeds | `isBST 0 10` | -| `BacktrackGenFor Expr (HasType · τ)` | Specimen-derived, may fail on some branches | `HasType · τ` | - -### Lawful versions: `LawfulGenFor` and `LawfulBacktrackGenFor` - -The issue with instances of these typeclasses is that we do not know if they are correct, i.e., whether they are _lawful_. This complicates proving lawfulness of a generator that happens to use a sub generator. For our example, the generator for well-formed statements invokes the generator for well-formed expressions via typeclass resolution. To prove that the well-formed statements generator is correct, we need to know/assume that the one for well-formed expressions is correct, too. - -To this end, we introduce two additional typeclasses: - -```lean -/-- A lawful non-backtracking generator: proves that outputs satisfy P. - Provides only soundness & completeness — weaker than Basalt's LawfulGenerator - which also requires almost-sure termination and cost bounds. -/ -class LawfulGenFor (α : Type) (P : α → Prop) extends GenFor α P where - sound_and_complete : SetGen.IsSoundAndComplete (gen (G := SetGen.Set)) P - -/-- A lawful backtracking generator: proves that successful outputs satisfy a size-indexed - bounded predicate at SetGen.Set. The Bounded predicate refines P with size/range - constraints imposed by the implementation (e.g., bounded leaf values, bounded depth). -/ -class LawfulBacktrackGenFor (α : Type) (P : α → Prop) (Bounded : Nat → α → Prop) - extends BacktrackGenFor α P 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) -``` - -Instances of these typeclasses are sure to be sound and complete, i.e., lawful (to a minimal degree). Thus users of them can rely on that lawfulness when proving lawfulness locally. - -**Why `Bounded` is separate from `P`.** The property `P` (e.g., `HasType e τ`) is the *semantic* specification the user cares about — it's what appears in `derive_generator (fun τ => ∃ e, HasType e τ)`. 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 (e.g., `HasTypeBounded τ`) 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 (see "Fuel vs size vs `partial_fixpoint`" in Section 7). If generators were defined via `partial_fixpoint` instead — where the generator's support at the fixpoint covers all values satisfying `P` — then `Bounded` would be unnecessary and the class could use a simple `iff` with `P`. The `Bounded` parameter is essentially the price of fuel-based termination; eliminating it is a benefit of moving to `partial_fixpoint` in the future. - -**Relationship to Basalt's `LawfulGenerator`:** Basalt defines `LawfulGenerator` as a property of a *specific generator term* — it says "this particular generator `g` is sound, complete, terminating, and cost-bounded." Our `LawfulGenFor` and `LawfulBacktrackGenFor` serve a different purpose: they are *typeclasses for resolution* — they say "there exists a generator for this type/property findable by typeclass synthesis, and it is sound and complete." They intentionally omit cost and termination requirements for simplicity; in the future, these could be strengthened to require `LawfulGenerator` of the underlying term, at which point the system would provide full lawfulness guarantees. - ### Standard `GenFor` instances -For standard types (`Nat`, `Bool`, `List`, etc.), we provide `GenFor` instances using existing Basalt-polymorphic generators: - ```lean instance : GenFor Nat (fun _ => True) where gen := Nat.arbitrary -- Basalt's polymorphic Nat generator @@ -399,7 +274,7 @@ instance : GenFor Bool (fun _ => True) where gen := Bool.arbitrary ``` -These are the generators that Specimen-derived code will resolve via typeclass synthesis. They must be Basalt-polymorphic (not Plausible-specific) so they work at all interpretations. If needed, a `GenFor` instance can bridge *down* to Plausible's `Arbitrary` for compatibility with the `plausible` tactic: +Bridge to Plausible: ```lean instance [GenFor α (fun _ => True)] : Arbitrary α where @@ -408,52 +283,27 @@ instance [GenFor α (fun _ => True)] : Arbitrary α where ## 4. Solving Problem 3: Checkers (`DecOpt`) -### The problem - -Today's `DecOpt` typeclass returns a Plausible-specific type: - -```lean -class DecOpt (P : Prop) where - decOpt : Nat → Except GenError Bool -``` - -It returns `ok true` (P holds), `ok false` (P doesn't hold), or `error` (can't decide — out of fuel). Inside a generator, the result is pattern-matched: `ok true` continues, anything else causes backtracking via `throw`. - -Since the emitted generator following our proposal is polymorphic over `G`, it cannot call a function like `DecOpt.decOpt` that returns `Except GenError Bool`. The checker must also be polymorphic over `G`. - -### Design: `DecOpt` as `BacktrackGen G Bool` - -We redefine `DecOpt` to return `BacktrackGen G Bool`: +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 cleanly to `G (Option 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 -This fits naturally into the `BacktrackGen` framework: when the checker returns `none`, the calling generator treats it as local failure and backtracks to another branch — exactly today's behavior. The running example demonstrates this: in the `isPos` branch, `DecOpt.decOpt (P := ¬(n = 0))` is called after `n` is generated; if it returns `false`, the branch fails and `backtrack` retries another branch. - -### Interpretations - -| 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 | - ### Bridge from `Decidable` -Any `Decidable` instance gives a `DecOpt` trivially (it never fails): - ```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: @@ -499,7 +349,7 @@ instance [GenFor Nat (fun _ => True)] fun τ => ⟨fun {_} [_] size => genHasType size τ size⟩ ``` -And `genWellFormed` calls the `HasType` generator via `BacktrackGenFor` typeclass resolution — the runtime value `τ` is captured in the predicate lambda, just as today's code captures it in `(fun e => HasType e τ)`: +And `genWellFormed` calls the `HasType` generator via `BacktrackGenFor` typeclass resolution: ```lean def genWellFormed [Gen G] [GenFor Nat (fun _ => True)] [GenFor Ty (fun _ => True)] @@ -527,18 +377,19 @@ def genWellFormed [Gen G] [GenFor Nat (fun _ => True)] [GenFor Ty (fun _ => True pure (Prog.both e1 e2))] ``` -### Key transformations from the code Specimen generates today +### Key transformations from Specimen's output today -- `MonadExcept.throw Gen.genericFailure` → `BacktrackGen.fail` -- `return value` → `pure value` (the `BacktrackGen` Monad wraps in `some` automatically) -- `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 α` -- Function is now polymorphic over `[Gen G]` -- Recursive calls compose directly in the `BacktrackGen` monad (failure propagates via `bind`) +| 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 `let rec aux_arb` inner function is eliminated — `initSize` and `τ` are explicit parameters with structural recursion on `size`. However, the double-initialization pattern remains: at the Plausible call site, the same value is used for both `initSize` and `size` (matching today's `fun size => aux_arb size size τ`). The `initSize` variable (passed when calling sub-generators like `BacktrackGenFor.gen ... initSize`) gives sub-generators their full budget without decrementing. +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 @@ -546,9 +397,6 @@ The `let rec aux_arb` inner function is eliminated — `initSize` and `τ` are e instance : ArbitrarySizedSuchThat Expr (HasType · τ) where arbitrarySizedST size := BacktrackGen.toPlausibleGen (genHasType size τ size) -instance : ArbitrarySuchThat Expr (HasType · τ) where - arbitraryST := Gen.sized (fun n => BacktrackGen.toPlausibleGen (genHasType n τ n)) - instance : ArbitrarySizedSuchThat Prog WellFormed where arbitrarySizedST size := BacktrackGen.toPlausibleGen (genWellFormed size size) ``` @@ -559,43 +407,36 @@ The `plausible` tactic finds these instances via the existing `ArbitrarySizedSuc ### The problem -Specimen derives unconstrained generators for algebraic data types via `derive Arbitrary`. These generators use `Gen.frequency` / `Gen.oneOfWithDefault` and `Arbitrary.arbitrary` — all Plausible-specific combinators. Like the constrained generators, they cannot be used polymorphically over Basalt's `Gen` class and cannot be proved correct at `SetGen.Set`. - -Unlike constrained generators, unconstrained generators never backtrack — they always succeed. This makes the migration simpler: no `BacktrackGen` wrapper is needed, just the `frequency` combinator and `GenFor` for sub-field resolution. +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`. -### What Specimen emits today - -For a type like: +### The `frequency` combinator ```lean -inductive Tree (α : Type) where - | leaf - | node (left : Tree α) (val : α) (right : Tree α) - deriving Arbitrary +/-- 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 () ``` -Specimen currently emits: +### 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 α) := - 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)] + let rec aux_arb (fuel : Nat) : Plausible.Gen (Tree α) := ... fun fuel => aux_arb fuel ``` -### Design: Basalt-polymorphic unconstrained generators - -The migrated version emits a Basalt-polymorphic generator and a `GenFor` instance: - +**After migration:** ```lean def Tree.gen [Gen G] [GenFor α (fun _ => True)] : (fuel : Nat) → G (Tree α) | 0 => frequency (pure Tree.leaf) [ @@ -609,7 +450,7 @@ def Tree.gen [Gen G] [GenFor α (fun _ => True)] : (fuel : Nat) → G (Tree α) pure (Tree.node left val right))] instance [GenFor α (fun _ => True)] : GenFor (Tree α) (fun _ => True) where - gen := Gen.sized Tree.gen -- or a fixed default fuel + gen := Gen.sized Tree.gen ``` ### Key transformations @@ -622,8 +463,6 @@ instance [GenFor α (fun _ => True)] : GenFor (Tree α) (fun _ => True) where | Return type: `Plausible.Gen α` | `G α` (polymorphic over `[Gen G]`) | | Instance: `ArbitraryFueled` | `GenFor α (fun _ => True)` | -No `BacktrackGen` wrapper is needed — unconstrained generators always succeed. - ### Executing via Plausible The bridge instance from Section 3 provides backward compatibility: @@ -633,8 +472,6 @@ instance [GenFor α (fun _ => True)] : Arbitrary α where arbitrary := GenFor.gen -- specializes at G := Plausible.Gen ``` -This ensures `deriving Arbitrary` continues to work with the `plausible` tactic. - ## 7. Design Notes ### Calling patterns summary @@ -646,7 +483,7 @@ The emitted code uses different calling conventions depending on the sub-generat let n ← BacktrackGen.liftGen (GenFor.gen (P := fun _ => True) : G Nat) ``` -- **Backtracking constrained sub-generator** (via `BacktrackGenFor`): May fail, resolved by typeclass. Runtime parameters are captured in the predicate lambda. Because we are inside a `BacktrackGen` `do`-block, failure propagates automatically via `bind`: +- **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 ``` @@ -662,102 +499,205 @@ The emitted code uses different calling conventions depending on the sub-generat gen := Tree.genBST 0 10 ``` -### Why typeclass resolution is safe here +### Mutual recursion -A natural concern: typeclass resolution is opaque, so how can a proof about `genHasType` know which `GenFor Nat (fun _ => True)` instance was resolved? +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 answer is that we maintain the invariant: **every `GenFor` instance in the system is eventually upgraded to a `LawfulGenFor` instance** (and likewise for `BacktrackGenFor` / `LawfulBacktrackGenFor`). Once this invariant holds, it doesn't matter which instance resolution picks — any instance it finds is provably sound and complete. The opacity of resolution is harmless because all candidates satisfy the same contract. +### The `initSize` parameter -This invariant is enforced by the two-step roadmap (see Section 8): -1. First, Specimen emits generators with `GenFor` / `BacktrackGenFor` constraints (for execution only). -2. Then, Specimen is upgraded to also emit `LawfulGenFor` / `LawfulBacktrackGenFor` instances with synthesized proofs, ensuring every derived generator is lawful. +- `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`. -### Instance diamond with `LawfulBacktrackGenFor` +Sub-generators always get a full budget. This matches today's behavior where `aux_arb initSize size' Ty.nat` passes `initSize` to nested calls. -A practical issue arises from `LawfulBacktrackGenFor` extending `BacktrackGenFor`: when both a standalone `BacktrackGenFor` instance and a `LawfulBacktrackGenFor` instance exist for the same type/predicate, typeclass synthesis may resolve `BacktrackGenFor.gen` to the standalone instance inside a generator body, while `LawfulBacktrackGenFor.sound`/`.complete` expect the inherited instance. Even though both produce the same generator, Lean treats them as distinct terms, causing type mismatches in proofs. +### Known limitations -**Solution:** Generators that need lawfulness proofs must explicitly route through the lawful instance: +**`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. -```lean -def genWellFormed' [Gen G] [GenFor Nat (fun _ => True)] [GenFor Ty (fun _ => True)] - [inst : ∀ τ, LawfulBacktrackGenFor Expr (fun e => HasType e τ) (HasTypeBounded τ)] - (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 _ _ ((inst τ).toBacktrackGenFor) _ _ initSize - pure (Prog.expr e)), - ...] -``` +> **Further design discussion** (typeclass resolution safety, fuel vs `partial_fixpoint`, performance benchmarks): see Appendices A and B. -**Implication for Specimen's code emission:** When emitting generators that will carry proofs (Phase 2), Specimen must either: -- Emit `@BacktrackGenFor.gen` with explicit instance selection via the lawful instance's `.toBacktrackGenFor` field, or -- Ensure that the `LawfulBacktrackGenFor` instance is the *only* `BacktrackGenFor` instance registered for that type/predicate (i.e., don't register a separate standalone instance once the lawful one exists), or -- Use instance priority to ensure the lawful instance wins synthesis +## 8. Plan of Work -### Mutual recursion +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. -Specimen supports mutually recursive inductive relations. For mutually recursive generators, the emitted code uses Lean's `mutual ... end` block with direct name calls between the 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 — mutual generators call each other by name, and only *external* callers go through typeclass resolution. +### Phase 1: Basalt-compatible generation (execution only) -### The `initSize` parameter +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. -The generated code takes both `initSize` and `size` as parameters: -- `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`. +**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. -This means sub-generators always get a full budget. When `genWellFormed` at `size=3` calls `BacktrackGenFor.gen (P := fun e => HasType e τ) initSize`, the `HasType` generator receives the original budget (e.g., 5) rather than the remaining budget (3). This matches today's behavior where `aux_arb initSize size' Ty.nat` passes `initSize` to nested `ArbitrarySizedSuchThat.arbitrarySizedST` calls. +#### 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 currently serves two distinct purposes that are worth disentangling: +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 to be accepted. The `size : Nat` parameter with pattern-matching on `0` vs `size + 1` provides a structural termination argument. +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 — smaller sizes for initial exploration, larger sizes to stress-test. Plausible's `Gen.sized` provides this via a `ReaderT (ULift Nat)` layer. +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 happen to coincide in today's Specimen output (the fuel *is* the size), but they are conceptually independent: +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 it also bounds the depth of generated derivation trees, providing natural size control. The `initSize`/`size` split already separates them partially: `size` is the termination witness (structurally decremented), while `initSize` controls sub-generator budgets. +- **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 — there is no backtracking, no failure. In Basalt, `partial_fixpoint` could eliminate the need for an explicit termination witness entirely, since it provides a well-founded recursion principle for generators with `⊥` as the default. However, the fuel still serves a useful role as a **size parameter**: without it, a recursive generator like `Tree.gen` has no way to bias toward smaller trees at lower sizes. +- **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. -The practical upshot for this plan: +**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. -- **Phase 1 preserves explicit fuel for both constrained and unconstrained generators.** This is the simplest path — it matches today's behavior, requires no `partial_fixpoint` infrastructure, and gives users familiar size control. +### Why `Bounded` is separate from `P` in `BacktrackGenCorrect` -- **A future optimization** (noted in Section 9) could emit `partial_fixpoint`-based generators that take an optional size hint rather than mandatory fuel. For unconstrained generators, this would look like: - ```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 would need 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 here is how to express size-dependent weights (today's `(fuel + 1, ...)` pattern) without an explicit fuel parameter. One option is a separate size monad layer; another is to use Basalt's cost infrastructure to bound expected depth. This is deferred as a research question. +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. -### Performance considerations +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. -`BacktrackGen` adds an `Option` wrapper at every bind within backtracking branches. For deeply nested generators this means more allocations and pattern-matches compared to today's exception-based approach. Benchmarking (see `SpecimenTest/BridgeBenchmark.lean`) shows: +## Appendix B: Performance -**Benchmark results** (bridge/legacy ratio, lower = bridge is faster): +`BacktrackGen` adds an `Option` wrapper at every bind within backtracking branches. Benchmarking (`SpecimenTest/BridgeBenchmark.lean`) shows: -| Scenario | Ratio | Notes | +| Scenario | Bridge/legacy ratio | Notes | |---|---|---| -| Recursive generator (5-ary `nary` constructor, sizes 2–4) | 97–101% | Dominant cost is recursion; `Option` overhead invisible | +| 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 overhead arises when branches consist almost entirely of `liftGen` calls (no recursive sub-generator calls) and multiple branches are tried per iteration (due to frequent failure and retry), amplifying the per-`liftGen` `Option` wrap/unwrap cost across many executed branches. In realistic generators (like Cedar's `HasType` with 23 constructors and recursive sub-generators), branch bodies are dominated by recursive calls — the `Option` overhead is amortized to < 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` (producing `spec_0._redArg` variants). +**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 +### Optimization: batching consecutive `liftGen` calls -When Specimen emits code where multiple unconstrained field generations appear consecutively (before any backtracking operation), they can be batched into a single `liftGen`: +When multiple unconstrained field generations appear consecutively (before any backtracking operation), they can be batched: ```lean -- Before (3 Option wraps + 3 Option checks): @@ -773,54 +713,52 @@ let (a, b, c) ← BacktrackGen.liftGen (do pure (a, b, c)) ``` -The inner `do` block runs in `G` directly (no `Option` overhead). This is purely a code-emission optimization in Specimen — the generated code's semantics are unchanged. The batching boundary is any operation that can fail: a `BacktrackGenFor.gen` call, a `DecOpt` check, or `BacktrackGen.fail`. +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 +### Optimization: `liftBind` for interleaved non-backtracking operations -When a `liftGen` is followed by a backtracking continuation (not another `liftGen`), batching doesn't apply. For this case, a fused combinator eliminates the intermediate `Option`: +When a `liftGen` is followed by a backtracking continuation (not another `liftGen`), a fused combinator eliminates the intermediate `Option`: ```lean -/-- Fused liftGen + bind: runs a non-failing G α and passes the result directly - to a backtracking continuation, without wrapping in some and immediately unwrapping. -/ @[inline] def BacktrackGen.liftBind [Gen G] (g : G α) (f : α → BacktrackGen G β) : BacktrackGen G β := ⟨do let a ← g; (f a).run⟩ ``` -This handles patterns like: -```lean --- Without liftBind: wraps n in some, then bind unwraps it -let n ← BacktrackGen.liftGen (GenFor.gen : G Nat) -let e ← BacktrackGenFor.gen (P := fun e => HasType e τ) initSize -- may fail +Neither optimization affects provability: `liftBind g f` has the same denotation as `bind (liftGen g) f` at all Basalt interpretations. --- With liftBind: no intermediate Option -BacktrackGen.liftBind (GenFor.gen : G Nat) (fun n => do - let e ← BacktrackGenFor.gen (P := fun e => HasType e τ) initSize - ...) -``` +## Appendix C: Proof Strategy -In practice, Specimen's emission order places all unconstrained generations before constrained sub-generator calls, so **batching handles the common case**. `liftBind` covers the remaining interleaved cases (e.g., generating a type `τ`, calling a sub-generator parameterized by `τ`, then generating another unconstrained field). Both optimizations are purely in Specimen's code emission — they require no changes to the `BacktrackGen` API or Basalt infrastructure. +### `BacktrackGenCorrect` -Neither optimization affects provability: `liftBind g f` has the same denotation as `bind (liftGen g) f` at all Basalt interpretations (the `some` wrap/unwrap is semantically invisible). The proof lemma is trivial: ```lean -theorem liftBind_eq_bind_liftGen [Gen G] (g : G α) (f : α → BacktrackGen G β) : - liftBind g f = bind (liftGen g) f +/-- 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) ``` -### Proving correctness (at `SetGen.Set`) - -Soundness and completeness proofs for the running example have been carried out manually as a POC. The proof structure is as follows. +**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** is `backtrack_mem_iff`, which characterizes membership in `backtrack`'s support: +### The key lemma: `backtrack_mem_iff` ```lean -theorem backtrack_mem_iff (gs : List (Nat × (Unit → BacktrackGen SetGen.Set α))) (a : α) : +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 — the random selection and retry logic is abstracted away. +This reduces reasoning about `backtrack` to reasoning about individual branches. -**The predicate.** Because `GenFor Nat (fun _ => True)` generates naturals in a bounded range (0–100 in the example), the generator's support does not cover *all* well-typed expressions — only those whose leaf values fall within range and whose depth fits the size budget. The proven predicate is: +### Proof structure for the running example + +**The predicate:** ```lean def HasTypeBounded (τ : Ty) (size : Nat) (e : Expr) : Prop := @@ -829,133 +767,41 @@ def HasTypeBounded (τ : Ty) (size : Nat) (e : Expr) : Prop := 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 `τ` within each branch. For the `isPos` branch, the `DecOpt` check (`decide (n ≠ 0)`) produces a `Bool` that is matched — only the `true` case reaches `pure (Expr.isPos n)`, directly yielding the `HasType.isPos` constructor with proof `n ≠ 0`. - -**Completeness** also proceeds by induction on `size`, constructing the appropriate branch index (`Fin gs.length`) for each `HasType` constructor. For example, `HasType.add` maps to branch index 2 in the `size + 1` case, with recursive appeals to the induction hypothesis for both subexpressions. +**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`. -**Compositionality.** In the full system with `LawfulGenFor` / `LawfulBacktrackGenFor` instances, these proofs compose modularly: the `genWellFormed` proof discharges its `HasType` sub-generator obligations by appealing to the `LawfulBacktrackGenFor Expr (HasType · τ) (HasTypeBounded τ)` instance's `.sound` and `.complete` fields rather than inlining the `genHasType` proof. This has been validated: soundness and completeness of `genWellFormed` are proved using `backtrack_mem_iff` to decompose into branches, then `backtrackGen_bind_mem` / `backtrackGen_pure_mem` to decompose the sequential `BacktrackGen` bind chain within each branch, and finally `(inst τ).sound` / `(inst τ).complete` to discharge sub-generator obligations. The generator must explicitly route through the lawful instance to avoid the instance diamond described in "Instance diamond with `LawfulBacktrackGenFor`" above. +**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. -## 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. +**Compositionality.** Correctness proofs for generators that call sub-generators are parameterized by correctness certificates of those sub-generators: -**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 (e.g., `Nat.arbitrary`) -- Provide bridge instance: `instance [Decidable P] : DecOpt P` -- Optionally provide bridge: `instance [GenFor α (fun _ => True)] : Arbitrary α` for Plausible compatibility - -#### 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 : Fin gs.length`. This is the key lemma for proving correctness of derived generators — it reduces backtracking to a disjunction over branches. (Proven now in a separate scratchfile.) -- `frequency_mem_iff`: analogous for `frequency` -- `backtrackGen_bind_mem`: `some b ∈ support ((x >>= f).run)` iff `∃ a, some a ∈ support x.run ∧ some b ∈ support ((f a).run)`. This is essential for decomposing sequential composition inside `BacktrackGen` branches — without it, proofs about composite generators (like `genWellFormed`) are extremely difficult because `BacktrackGen`'s bind introduces nested `match` on `Option` that doesn't reduce with `simp`. -- `backtrackGen_pure_mem`: `some b ∈ support ((pure a : BacktrackGen SetGen.Set α).run)` iff `b = a`. The base case for branch decomposition. -- Basic `liftGen` support lemma (follows from the above and Basalt's existing `SetGen.support_bind`, `SetGen.support_pure`) - -#### 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` (equivalently, `pure none` at the `G` level) -- Replace fuel-based recursion with structural recursion on an explicit `size : Nat` -- Emit generators polymorphic over `[Gen G]` with `[GenFor α P]` / `[BacktrackGenFor α P]` constraints for sub-generators -- Replace `Arbitrary.arbitrary` calls with `GenFor.gen` wrapped in `BacktrackGen.liftGen` -- Replace `ArbitrarySizedSuchThat.arbitrarySizedST` calls with `BacktrackGenFor.gen` (or direct name calls for co-derived / mutually-recursive generators) -- Replace `DecOpt.decOpt` calls (pattern-matching on `Except`) with the new polymorphic `DecOpt.decOpt` (pattern-matching on `Bool` within `BacktrackGen`) -- 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 (for sub-fields) with `GenFor.gen (P := fun _ => True)` -- Emit generators polymorphic over `[Gen G]` with `[GenFor α (fun _ => True)]` constraints for type parameters -- Emit `GenFor α (fun _ => True)` instances (with a `Gen.sized` wrapper or fixed fuel) for each derived type -- Emit bridge `Arbitrary` instance: `instance [GenFor α (fun _ => True)] : Arbitrary α where arbitrary := GenFor.gen` -- Ensure mutually recursive types use Lean's `mutual ... end` block with direct name calls, then register `GenFor` instances after - -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 (expected output will change shape; update snapshots) -- Verify `derive Arbitrary` produces working `GenFor` instances for standard test types (e.g., `Tree`, `Expr`) -- Verify the `plausible` tactic works end-to-end with both constrained and unconstrained generators -- Write a manual soundness proof for the `HasType` example, demonstrating that a Specimen-derived generator can be proved sound at `SetGen.Set` given `LawfulGenFor` / `LawfulBacktrackGenFor` instances for sub-generators. (Complete soundness and completeness proofs of `genHasType` in a scratchfile.) - -### Phase 2: Lawful generation (with proof synthesis) - -The goal of this phase is to make Specimen emit `LawfulGenFor` / `LawfulBacktrackGenFor` instances alongside the generators, so that every derived generator carries a machine-checked proof of soundness and completeness. Once this phase is complete, the system invariant holds: all `GenFor` / `BacktrackGenFor` instances are lawful, and proofs about composite generators compose modularly. - -#### Step 2.1: Define `LawfulGenFor` and `LawfulBacktrackGenFor` in Basalt - -- Define `LawfulGenFor` extending `GenFor` with soundness/completeness at `SetGen.Set` -- Define `LawfulBacktrackGenFor` extending `BacktrackGenFor` with a `Bounded : Nat → α → Prop` parameter and sound/complete fields at `SetGen.Set` -- Provide `LawfulGenFor` instances for standard types (using existing Basalt proofs like `Nat.arbitrary_support`) - -#### 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 inductive relation. The proof structure mirrors the generator structure: - -1. **Top-level**: The proof proceeds by `cases` on the `size` parameter, matching the generator's pattern match. -2. **Per-branch**: Each branch in `backtrack [...]` contributes one direction of the `↔`. The `backtrack_mem_iff` lemma decomposes `some a ∈ support (backtrack gs)` into a disjunction over branches. -3. **Soundness** (forward): For each branch that produces `some a`, show `P a` holds. This follows the `do`-block structure — each `liftGen` or `BacktrackGenFor.gen` call contributes a hypothesis (from the sub-generator's `LawfulGenFor` / `LawfulBacktrackGenFor` instance). -4. **Completeness** (backward): For each constructor of the inductive relation, exhibit a `size` and branch that produces the corresponding value. Typically, the recursive constructor needs `size = depth_of_derivation`. - -Sub-generator proof obligations are discharged by the `LawfulGenFor` / `LawfulBacktrackGenFor` instances of sub-generators (available via typeclass resolution). - -This structure has been validated by hand-proving soundness and completeness for the running example's `genHasType`. The proofs use `induction size`, `backtrack_mem_iff`, `fin_cases` on branch indices, and `simp` over `SetGen.support` lemmas — a pattern amenable to automation. - -Emit `LawfulBacktrackGenFor` instances bundling generator + proof. - -For each derived **unconstrained** generator (`derive Arbitrary`), Specimen emits a `LawfulGenFor α (fun _ => True)` instance. The property is trivially `True`, so the proof obligation reduces to: -- **Soundness**: trivial (every value satisfies `fun _ => True`) -- **Completeness**: show that every inhabitant of `α` is in the support of the generator. This amounts to showing that `frequency` with all constructors covered produces every value at some fuel — each constructor's branch reaches the corresponding value when sub-generators (with their own `LawfulGenFor` instances) are complete. - -The proof follows the inductive structure of the type: base-case constructors are reachable at fuel 0, recursive constructors at fuel ≥ depth. This is simpler than the constrained case because there is no `Option` wrapping and no backtracking — `frequency_mem_iff` directly gives the membership condition. - -#### Step 2.3: End-to-end validation - -- Verify that Specimen-derived generators (both constrained and unconstrained) carry correct proofs (they typecheck with no `sorry`) -- Verify that proofs compose: a generator for type `A` that calls a generator for type `B` can use `B`'s `LawfulGenFor` / `LawfulBacktrackGenFor` proof without manual intervention -- Benchmark elaboration time to ensure proof synthesis does not unacceptably slow down `derive_generator` or `derive Arbitrary` +```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 ... +``` -### Rollback strategy +The proof uses `(sub_correct τ).sound` / `(sub_correct τ).complete` to discharge sub-generator obligations. No "lawful instance" routing is needed. -If Phase 1 reveals fundamental design issues (e.g., universe polymorphism problems, instance diamonds at scale, or unacceptable elaboration performance), 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) +## Appendix D: Interpretations Across Basalt Instances -The existing `GeneratorCombinators.backtrack` path remains functional throughout development. A feature flag (`set_option specimen.basaltBridge true`) can gate the new emission path, allowing incremental rollout and easy revert. +### `BacktrackGen` -## 9. Known Limitations and Future Work - -The following issues are related to the migration but are not addressed by the plan above: +| 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 | -**`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 where almost-sure termination can be proved, eliminating the fuel parameter and enabling tighter cost bounds. This is a research question deferred beyond Phase 2. +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. -## Glossary +### `DecOpt` -| Term | Meaning | -|---|---| -| **Constrained producer** | A generator that only produces values satisfying a user-specified inductive relation (e.g., well-typed expressions) | -| **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, not the decremented counter | -| **Schedule** | Specimen's internal representation of how to order constructor attempts when deriving a generator | -| **Backtracking** | The ability for a generator branch to signal failure, causing the combinator to retry another branch | -| **`BacktrackGen`** | A newtype wrapping `G (Option α)` — the backtracking layer used in this plan | -| **`GenFor` / `BacktrackGenFor`** | Typeclasses for finding generators by typeclass resolution (analogous to `Arbitrary` / `ArbitrarySizedSuchThat`) | +| 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/SpecimenTest/BridgeBacktrackMockup.lean b/SpecimenTest/BridgeBacktrackMockup.lean index 3907876..52d947b 100644 --- a/SpecimenTest/BridgeBacktrackMockup.lean +++ b/SpecimenTest/BridgeBacktrackMockup.lean @@ -278,15 +278,24 @@ def genWellFormed [Gen G] [GenFor Nat (fun _ => True)] [GenFor Ty (fun _ => True /-! ## frequency combinator (for non-backtracking generators) -/ -/-- Weighted random selection without retry. 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 - | [(_, g)] => g () - | gs => do - let idx ← RandomChoice.choose 0 (gs.length - 1) (by omega) - let (_, g) := gs[idx.down]! - g () + | _ => 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) -/ From 0b86370048c435406a30749a5b87fc8566050b58 Mon Sep 17 00:00:00 2001 From: Mike Hicks Date: Tue, 9 Jun 2026 10:51:49 -0400 Subject: [PATCH 7/8] Update port plan, added doc on sizing, naming cleanup --- Docs/Generator-config.md | 236 ++++++++++++++++++ .../Specimen-Basalt-port.md | 6 +- .../BridgeBacktrackMockup.lean | 0 .../{ => BasaltPort}/BridgeBenchmark.lean | 0 4 files changed, 241 insertions(+), 1 deletion(-) create mode 100644 Docs/Generator-config.md rename SPECIMEN-BASALT-BRIDGE.md => Docs/Specimen-Basalt-port.md (97%) rename SpecimenTest/{ => BasaltPort}/BridgeBacktrackMockup.lean (100%) rename SpecimenTest/{ => BasaltPort}/BridgeBenchmark.lean (100%) 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/SPECIMEN-BASALT-BRIDGE.md b/Docs/Specimen-Basalt-port.md similarity index 97% rename from SPECIMEN-BASALT-BRIDGE.md rename to Docs/Specimen-Basalt-port.md index f737981..10c9500 100644 --- a/SPECIMEN-BASALT-BRIDGE.md +++ b/Docs/Specimen-Basalt-port.md @@ -22,6 +22,8 @@ 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 @@ -38,7 +40,7 @@ It provides randomness, a size parameter, and exception-based failure. The `plau - `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: +**[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 α) @@ -510,6 +512,8 @@ For mutually recursive inductive relations, the emitted code uses Lean's `mutual 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. diff --git a/SpecimenTest/BridgeBacktrackMockup.lean b/SpecimenTest/BasaltPort/BridgeBacktrackMockup.lean similarity index 100% rename from SpecimenTest/BridgeBacktrackMockup.lean rename to SpecimenTest/BasaltPort/BridgeBacktrackMockup.lean diff --git a/SpecimenTest/BridgeBenchmark.lean b/SpecimenTest/BasaltPort/BridgeBenchmark.lean similarity index 100% rename from SpecimenTest/BridgeBenchmark.lean rename to SpecimenTest/BasaltPort/BridgeBenchmark.lean From 8bf0cdd5568f30653f0a0f617f9b734fa267d6ad Mon Sep 17 00:00:00 2001 From: Mike Hicks Date: Wed, 10 Jun 2026 08:30:52 -0400 Subject: [PATCH 8/8] #eval! to #eval; fix wrong name --- SpecimenTest/BasaltPort/BridgeBacktrackMockup.lean | 12 ++++++------ SpecimenTest/BasaltPort/BridgeBenchmark.lean | 4 ++-- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/SpecimenTest/BasaltPort/BridgeBacktrackMockup.lean b/SpecimenTest/BasaltPort/BridgeBacktrackMockup.lean index 52d947b..89a6441 100644 --- a/SpecimenTest/BasaltPort/BridgeBacktrackMockup.lean +++ b/SpecimenTest/BasaltPort/BridgeBacktrackMockup.lean @@ -6,7 +6,7 @@ import Specimen.GeneratorCombinators /-! # Specimen–Basalt Bridge Mockup: Backtracking, Sub-generators, and Checkers -This file demonstrates all three mechanisms from SPECIMEN-BASALT-BRIDGE.md in a single +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 @@ -412,21 +412,21 @@ end StatusQuo open MockBacktrack -#eval! do +#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 +#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 +#eval do IO.println "=== genWellFormed (size = 3) — sub-generator calls into HasType ===" for _ in List.range 5 do let result : Prog ← Plausible.Gen.run @@ -434,7 +434,7 @@ open MockBacktrack IO.println s!" {repr result}" -- Also run the status-quo version to confirm both produce the same kinds of output -#eval! do +#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 @@ -463,7 +463,7 @@ instance [Arbitrary α] : ArbitraryFueled (Tree α) where end UnconstrainedStatusQuo -- Run the migrated unconstrained generator -#eval! do +#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 diff --git a/SpecimenTest/BasaltPort/BridgeBenchmark.lean b/SpecimenTest/BasaltPort/BridgeBenchmark.lean index 077eb20..5229d38 100644 --- a/SpecimenTest/BasaltPort/BridgeBenchmark.lean +++ b/SpecimenTest/BasaltPort/BridgeBenchmark.lean @@ -294,7 +294,7 @@ def benchAtSize (size : Nat) (iters : Nat) (τ : Ty) : IO Unit := do /-! ## Main benchmark -/ -#eval! do +#eval do let iters := 2000 IO.println s!"=== A/B Benchmark: Legacy vs Bridge (HasType, {iters} iterations) ===" IO.println "" @@ -463,7 +463,7 @@ private def genNat100Legacy : Plausible.Gen Nat := do end StressBacktrack -#eval! do +#eval do let iters := 10000 IO.println s!"" IO.println s!"=== Stress Backtrack: 5 branches, 4 always fail after work, {iters} iters ==="