Improving forward generation by "inlining" -- experiments and design doc

Docs/Steering-notes.md

@@ -0,0 +1,82 @@
+# Notes: Steering Command-Sequence Generation Toward a Target
+
+*Speculative. Separate from [Lookahead-experiment.md](./Lookahead-experiment.md),
+which is about generating valid command sequences at all — including commands
+with hard-to-satisfy preconditions. These notes assume that problem is solved and
+ask a further question.*
+
+## The problem
+
+Given an *adequate* forward generator for a state-transition specification (one
+that can produce valid sequences exercising every command, including
+precondition-heavy ones), it still produces only *random* valid sequences. A
+distinct goal is **steering**: bias generation to reach a *specific, rare target*
+— e.g. "a state where the `GetOp` branch is enabled", so we can test that branch,
+or a designated destination state.
+
+This is orthogonal to the forward-generation-adequacy problem. Step inlining (the
+subject of the companion doc) makes a generator *capable* of hard steps; it does
+nothing to *aim* it. A fused generator still walks forward and still produces
+random valid sequences.
+
+## Planning vs. generation
+
+A natural decomposition:
+
+- **Planning (control):** decide *which* constructors fire, and in what order —
+  the command skeleton from the start to the target.
+- **Generation (data):** decide *what values* instantiate the states and command
+  arguments along that skeleton.
+
+The tempting design is to treat the specification as an explicit **state machine**
+and plan by pathfinding, then solve constraints along the path. Two observations
+complicate that:
+
+1. **The states are symbolic.** A "node" like `([], n)` is a *family* of states
+   (a pattern with a free variable), and edges carry *constraints*
+   (`WithinCapacity`, the equality `s' = concat s v`). "Reaching the target" is
+   unification + constraint solving over the relation's constructors — a form of
+   narrowing. No separate graph is required; the state machine is a *lens* on that
+   search, not an input to it.
+
+2. **Pure control planning is unsound**, because data dependencies determine which
+   control paths are feasible. In the KV store, a versioned `Get` (version 1)
+   requires two prior `Set`s **of the same key** (`LookupKV.LFoundS` bumps the
+   version only when a newer entry for the same key is prepended). A control-only
+   planner would propose `Create; Set; Get@v1` — a skeleton with no concrete
+   realization. The skeleton cannot be chosen without partly accounting for the
+   data.
+
+So planning and solving must be **interleaved, not staged.** What survives as a
+clean distinction is *reachability-relevant data* (what guards branch on — must be
+tracked during planning) vs. *inert data* (appears in commands but never gates a
+transition — can be deferred to cheap unconstrained generation).
+
+## Directions
+
+- **Target-mode / backward derivation.** Combine an adequate forward generator
+  with backward/target-mode derivation (`fun s => ∃ t i, Trace i t s`) so a target
+  biases which edges are explored. The abstract state machine acts as a heuristic
+  that prunes and orders constructor choices, while the actual work is narrowing
+  over the constructors.
+
+- **Backtracking over plans (CEGAR).** Any finite state abstraction can propose a
+  skeleton with no concrete realization. Treat a skeleton as a *bias with a
+  fallback* and backtrack when its accumulated constraints go unsat, refining the
+  abstraction on failure.
+
+- **The proven state machine (optional).** A Lean-*defined* transition system with
+  a proof of equivalence to the source relation would be a nice artifact for trust
+  and visualization, but it is not on the critical path: the generator needs only
+  the internal, heuristic version, whose soundness comes from checking the
+  relation's guards during generation.
+
+## Relationship to the inlining work
+
+The static analyses proposed for taming the inlining blow-up (culling
+unsatisfiable step-combinations, classifying forward-functional vs. inversion
+links) are effectively a *local, bounded* form of the planning search described
+here. Steering generalizes them: instead of pruning fixed-length step windows, it
+searches for a path of arbitrary length toward a chosen target. A good next step
+is to see whether the same reachability pruning that culls dead `b^k`
+combinations extends naturally into goal-directed path search.

SpecimenTest.lean

@@ -48,7 +48,6 @@ import SpecimenTest.DeriveArbitrarySuchThat.MultiOutputTest
 import SpecimenTest.DeriveArbitrarySuchThat.MultiOutputSTLCTest
 import SpecimenTest.DeriveArbitrarySuchThat.EqMultiOutputTest
 import SpecimenTest.DeriveArbitrarySuchThat.UserInstancePriorityTest
-import SpecimenTest.DeriveArbitrarySuchThat.BoundedBuffer
 
 -- Tests for instances of `Enum` for simple types and for correctness of enumerator combinators
 import SpecimenTest.Enum.EnumInstancesTest
@@ -95,6 +94,24 @@ import SpecimenTest.CedarExample.Cedar
 import SpecimenTest.CedarExample.CedarCheckerGenerators
 import SpecimenTest.CedarExample.CedarWellTypedTermGenerator
 
+-- Bounded Buffer Example
+import SpecimenTest.BoundedBuffer.BoundedBufferSpec
+import SpecimenTest.BoundedBuffer.BackwardGenerator
+import SpecimenTest.BoundedBuffer.BoundedBuffer
+
+-- Multi-step precondition experiments (perfect-square vault): baseline, and the
+-- hand-written step-inlined variants (fused pair, all-combinations).
+import SpecimenTest.VaultExperiment.VaultBaseline
+import SpecimenTest.VaultExperiment.VaultFused
+import SpecimenTest.VaultExperiment.VaultUnrolledAll
+
+-- Tree-structured analog (guarded dereference): baseline and hand-written
+-- inlined variants, inlining across a self-recursive typing relation and the
+-- membership relation it depends on.
+import SpecimenTest.AttrGuardExperiment.AttrGuardBaseline
+import SpecimenTest.AttrGuardExperiment.AttrGuardFused
+import SpecimenTest.AttrGuardExperiment.AttrGuardUnrolledAll
+
 -- Strata Lambda Example: well-typed `LExpr` generator via `HasTypeA`
 import SpecimenTest.StrataLexprGen
 
@@ -111,5 +128,3 @@ import SpecimenTest.WeightCustomizationTest
 
 -- `specimen.silent` output-suppression option tests
 import SpecimenTest.SilentOptionTest
-
-

SpecimenTest/AttrGuardExperiment/AttrGuardBaseline.lean

@@ -0,0 +1,134 @@
+import Plausible.Arbitrary
+import Plausible.DeriveArbitrary
+import Specimen.DeriveChecker
+import Specimen.DeriveConstrainedProducer
+import Specimen.EnumeratorCombinators
+
+open Plausible
+
+namespace AttrGuard
+
+/-!
+# Guarded-dereference experiment — BASELINE (0-step lookahead)
+
+A Cedar-shaped analog of the vault experiment. Where the vault was a *flat*
+command trace (a Step/Trace pair), this is a **single self-recursive typing
+relation over an expression tree**, threading a "guard set" state through
+subexpression outputs — the structure of Cedar's `HasType`, which threads a
+`PathSet` from an expression into its subexpressions (`TCondTrue`, `THasAttr`, …).
+
+The language:
+  * `lit n`      — a literal; leaves the guard set unchanged.
+  * `chk c e`    — a "has-attribute" check: records guard code `c`, so its output
+                   guard set is `c :: (guards of e)`.
+  * `drf k e`    — a "dereference": legal ONLY if the guard code `sq k` is already
+                   present in `e`'s output guard set. You must present a root `k`
+                   whose square is an established guard.
+
+`WT g e g'` reads "in guard set `g`, expression `e` is well-typed and yields guard
+set `g'`". The output `g'` of a subexpression flows to its parent — the Cedar
+PathSet threading, in miniature.
+
+The crux mirrors the vault:
+  * A `drf k` is enabled only if an earlier `chk (sq k)` established the guard —
+    a precondition set up by a *different* node in the tree.
+  * The guard set stores *squares*; the root `k` cannot be read back from it, so
+    a forward generator can only guess `k` and check `sq k ∈ g'` — which for
+    arbitrary stored codes ~never hits.
+
+Prediction: the derived forward generator fires `chk` freely but almost never
+produces a `drf`, because by the time it needs a root the guard codes are
+arbitrary (non-squares, or squares of un-guessable roots).
+-/
+
+def sq (k : Nat) : Nat := k * k
+
+inductive Expr where
+| lit (n : Nat)
+| chk (c : Nat) (e : Expr)
+| drf (k : Nat) (e : Expr)
+deriving Repr, DecidableEq
+
+abbrev Guards := List Nat
+
+inductive WT : Guards → Expr → Guards → Prop where
+| TLit : ∀ g n,
+    WT g (Expr.lit n) g
+| TChk : ∀ g c e g',
+    WT g e g' →
+    WT g (Expr.chk c e) (c :: g')
+| TDrf : ∀ g k e g',
+    WT g e g' →
+    sq k ∈ g' →
+    WT g (Expr.drf k e) g'
+
+set_option specimen.multiOutput true
+set_option specimen.autoDeriveDeps true
+set_option match.ignoreUnusedAlts true
+
+-- Hand-written generator for the perfect-square property, since Specimen cannot
+-- invert `sq`. (Dead code in the forward baseline — `chk` picks its code freely —
+-- but the synthesizer should pick it up once a square must be produced.)
+instance : ArbitrarySizedSuchThat Nat (fun t => ∃ k, t = sq k) where
+  arbitrarySizedST size := do
+    let k ← Gen.choose Nat 0 size (by omega)
+    return sq k
+
+deriving instance Arbitrary for Expr
+
+#guard_msgs(drop info, drop warning) in
+derive_mutual
+  (fun g => ∃ e g', WT g e g')
+
+-- Count `drf` nodes in a generated expression.
+def countDrf : Expr → Nat
+  | .lit _ => 0
+  | .chk _ e => countDrf e
+  | .drf _ e => 1 + countDrf e
+
+def countDerefs (numTraces : Nat := 1000) : IO (Nat × Nat) := do
+  let mut exprsWithDrf := 0
+  let mut totalDrf := 0
+  for i in List.range numTraces do
+    let (e, _) ← Gen.run
+      (ArbitrarySizedSuchThat.arbitrarySizedST
+        (fun (e, g') => WT [] e g') 10) (i + 5)
+    let d := countDrf e
+    totalDrf := totalDrf + d
+    if d > 0 then exprsWithDrf := exprsWithDrf + 1
+  return (exprsWithDrf, totalDrf)
+
+#eval do
+  let (withDrf, total) ← countDerefs 1000
+  IO.println s!"expressions containing >=1 drf: {withDrf} / 1000"
+  IO.println s!"total drf nodes generated: {total}"
+
+-- Sanity check: the generator IS exercising the tree (firing chk, building
+-- depth), so the drf=0 result is "never derefs" not "never generates".
+def countChk : Expr → Nat
+  | .lit _ => 0
+  | .chk _ e => 1 + countChk e
+  | .drf _ e => countChk e
+
+def exprSize : Expr → Nat
+  | .lit _ => 1
+  | .chk _ e => 1 + exprSize e
+  | .drf _ e => 1 + exprSize e
+
+def exprStats (numTraces : Nat := 1000) : IO Unit := do
+  let mut totalChk := 0
+  let mut nonTrivial := 0
+  let mut maxSize := 0
+  for i in List.range numTraces do
+    let (e, _) ← Gen.run
+      (ArbitrarySizedSuchThat.arbitrarySizedST
+        (fun (e, g') => WT [] e g') 10) (i + 5)
+    totalChk := totalChk + countChk e
+    if exprSize e > 1 then nonTrivial := nonTrivial + 1
+    if exprSize e > maxSize then maxSize := exprSize e
+  IO.println s!"non-trivial exprs (size>1): {nonTrivial} / {numTraces}"
+  IO.println s!"total chk nodes: {totalChk}, max expr size: {maxSize}"
+
+#eval exprStats 1000
+
+end AttrGuard

SpecimenTest/AttrGuardExperiment/AttrGuardFused.lean

@@ -0,0 +1,77 @@
+import SpecimenTest.AttrGuardExperiment.AttrGuardBaseline
+
+open Plausible
+
+namespace AttrGuard
+
+/-!
+# Guarded-dereference experiment — FUSED (1-step lookahead)
+
+We reuse the `WT` machine but derive a generator for a *fused* typing relation
+`WT2`, whose `DrfChk` constructor inlines the two nodes that must cooperate: a
+`chk (sq k)` establishing a guard, immediately dereferenced by `drf k`.
+
+`DrfChk` brings the check code `sq k`, the dereference root `k`, and the guard
+`sq k ∈ (sq k :: g')` into a single constructor scope. The scheduler can bind a
+fresh `k`, compute the check code `sq k` forward, and the membership is then
+immediate (`sq k` is the head of the guard set) — instead of committing arbitrary
+check codes and later failing to invert `sq`.
+
+Prediction: `drf` now appears reliably, in contrast to the baseline's ~0 / 1000.
+-/
+
+set_option specimen.multiOutput true
+set_option specimen.autoDeriveDeps true
+set_option match.ignoreUnusedAlts true
+
+inductive WT2 : Guards → Expr → Guards → Prop where
+| TLit : ∀ g n,
+    WT2 g (Expr.lit n) g
+| TChk : ∀ g c e g',
+    WT2 g e g' →
+    WT2 g (Expr.chk c e) (c :: g')
+| TDrf : ∀ g k e g',
+    WT2 g e g' →
+    sq k ∈ g' →
+    WT2 g (Expr.drf k e) g'
+-- Fused: drf k (chk (sq k) e). The check code and the deref root are the same
+-- `k`, brought into one scope, so `sq k` is computed forward and the membership
+-- `sq k ∈ sq k :: g'` holds by construction.
+| DrfChk : ∀ g k e g',
+    WT2 g e g' →
+    WT2 g (Expr.drf k (Expr.chk (sq k) e)) (sq k :: g')
+
+#guard_msgs(drop info, drop warning) in
+derive_mutual
+  (fun g => ∃ e g', WT2 g e g')
+
+def countDerefs2 (numTraces : Nat := 1000) : IO (Nat × Nat) := do
+  let mut exprsWithDrf := 0
+  let mut totalDrf := 0
+  for i in List.range numTraces do
+    let (e, _) ← Gen.run
+      (ArbitrarySizedSuchThat.arbitrarySizedST
+        (fun (e, g') => WT2 [] e g') 10) (i + 5)
+    let d := countDrf e
+    totalDrf := totalDrf + d
+    if d > 0 then exprsWithDrf := exprsWithDrf + 1
+  return (exprsWithDrf, totalDrf)
+
+#eval do
+  let (withDrf, total) ← countDerefs2 1000
+  IO.println s!"[fused] expressions containing >=1 drf: {withDrf} / 1000"
+  IO.println s!"[fused] total drf nodes generated: {total}"
+
+-- Confirm the generated derefs are genuinely well-guarded (each `drf k` sits
+-- over a `chk (sq k)`), rather than junk.
+def sampleValidDerefs (numTraces : Nat := 30) : IO Unit := do
+  for i in List.range numTraces do
+    let (e, _) ← Gen.run
+      (ArbitrarySizedSuchThat.arbitrarySizedST
+        (fun (e, g') => WT2 [] e g') 10) (i + 5)
+    if countDrf e > 0 then
+      IO.println s!"{repr e}"
+
+#eval sampleValidDerefs 30
+
+end AttrGuard