diff --git a/Docs/The-perfect-generator.md b/Docs/The-perfect-generator.md new file mode 100644 index 0000000..1e8a179 --- /dev/null +++ b/Docs/The-perfect-generator.md @@ -0,0 +1,345 @@ +# Towards Automating Thorough Input Generation + +A property-based tester wants to test its target *thoroughly*. When the target's +inputs are *sparse* — most are invalid or rejected, and the interesting behaviors +are reached by only a few valid inputs — thoroughness is hard to come by. This +note lays out two routes to it, and what each one needs to work: + +1. **One generator that does it all** — derive a single constrained generator and + *tune* it (reweight and restructure its choices) until its output distribution + exercises the target thoroughly. This is the subject of most of the note. +2. **Two-part scenario generation** — first synthesize the *scenarios* worth + testing, then generate a concrete input realizing each. This is genuinely + different: you are not running one generator over and over, but planning a + suite. The generation half is a (roughly backwards) constrained generator; the + scenario-synthesis half is a separate problem, developed in the companion + scenario-generation design and sketched in the last section here. + +## Problem: Thorough input generation by automated tuning + +A typical goal of a property-based tester is to _throughly_ test a target. We want to generate inputs that put the code through all of its paces, exposing failiures due to unforeseen interactions and missed corner cases. + +This is challenging when the inputs to that target are _sparse_, meaning that most are either _invalid_ － the behavior is undefined on them － or _erroneous_ － the behavior is to reject the input as non-sensical, and thus not explore much of the target's interesting functionality. + +Tools like Specimen aim to address the sparse input problem by automatically deriving constrained generators, for which we can be sure inputs satisfy a (sparse) predicate that defines what it means to be valid/non-erroneous. The Basalt library defines correctness conditions for generators, enabling GenAI can write the generators and prove their are correct (sound & complete with respect to a constraining predicate). + +Unfortunately, just because Specimen or GenAI produce a generator that _may_ produce an input, the chances of doing so may not be sufficiently _likely_. This is a problem when some program behaviors are exercised by very few inputs. To thoroughly test those behaviors, we need to generate those inputs. + +The process of altering a generator to produce a better _distribution_ of inputs, i.e., those that test a target more thoroughly, quickly, and reliably, is called _tuning_ the generator. Our goal is to automate generator tuning. + +### Examples + +Here we define three examples to frame the discussion. For the first two, the validity predicate is _state based_, as many interesting examples are such (even ones that don't necessarily appear to be). + +1. **Amazon Verified Permissions**. We want to synthesize a sequence of API calls to AVP that (mostly) do not fail. Then we can ensure that AVP behaves properly using model-based testing, and also that it satisfies properties like idempotence of certain operations. + + AVP is obviously state-based: We create a repository, add a policy to it, remove a policy from it, list the current policies, carry out an authorization request. Each of these is an API call and their validity is predicated on the current state of the repository. A generator for such API calls would track an abstraction of the state (e.g., what repositories are created, what policies are in them, etc.) to know what API calls could be generated next. + +2. **Cedar**. We want to synthesize Cedar programs that are (mostly) well-typed. Then we can test theorems like type soundness, and we can do differential testing against Cedar implementations. + + Some sub-expressions are only valid when paired with others, which establish a precondition. Example + ``` + principal has manager && principal.manager.level > 8 + ``` + The second sub-expression, `principal.manager...` is only legal if `principal` has `manager` as an attribute, and that fact is established by the first sub-expression. In the type system, the fact that `has` on an attribute has surely occurred is carried in the _capability_, which is essentially a state; the judgment form is `ɑ ; Γ ⊢ e : τ ; ε`, where `ɑ` is the input capability (collecting the attributes in `has` checks that have succeeded to this point), and `ε` is the output capability, which are checked attributes (still) conditionally valid, going forward. The type rule for `has C` will add `C` to `ε`. The type rule for `x.C` will confirm that `C` is in `ɑ`. + + In short, the `ɑ` / `ε` are basically the _state_ abstracted by the type system. They allow a decision made by the generator early － to produce a `has` check on `C` － to inform a later decision － what `C` to use on the expression `x.C`. + +3. **Strata**. We want to synthesize Strata Core programs that are (mostly) well typed. Then we can test theorems of the Strata codebase, similarly to Cedar. Strata is built around a core polymorhic lambda calculus parameterized by a set of types and operators, and extends out to support stateful operations (commands), functions, and procedures. + +### Unlikely inputs + +In principle, a generator produced by Specimen or proved correct in Basalt can cover all inputs. But in practice it fail to produce many interesting ones. Here are some examples why. + +1. Consider Cedar. A generator cannot produce a well-typed expression `x.C` on its own; that expression needs to be generated within a _context_ `x has C && []` where the `x.C` plugs into the hole `[]`. The context can be more general than this, of course, e.g., it could be `x has C && x has D && []` or `(if true then x has C else false) && []` and so on. In essence, we are saying the context is one which induces `C ∈ ɑ` when typing `x has C`. Overall, it is relatively unlikely that you will generate such a context by chance and then, by chance, generate `x has C`. You need to decide to generate `&&` and then to generate `x has C` for the left sub-term and then generate `x.C` for the right. If we assume there is a uniformly random chance for each constructor -- `has`, `&&`, and `.` -- then it's much more likely we'll generate something else. + +2. As another example, consider Strata terms under well typing, i.e., given a type `T`, generate a term with that type. Based on the App typing rule, to produce an expression of type `T` a generator would generate a type `T1`, a value `x` of type `T1`, and a function `f` of type `T1 -> T` and return `f x`. Functions include operators `op`, chosen from a dictionary which maps operators to their type `T1 -> T2 -> ... Tn`. Suppose `+` has type `Nat -> Nat -> Nat` and we want to generate a term of type `Nat` that uses `+`. Then the generator would have (a) decide to generate a function application, and then choose T1 to be `Nat` and generate a function of type `Nat -> Nat`; (b) choose to generate the `Nat -> Nat` by deciding to generate a function application again, in this case `T1` would again be `Nat` and the function type would be `Nat -> Nat -> Nat`; (c) choose to generate the `Nat -> Nat -> Nat` value by looking up an operator and getting `+`. This call then returns `+ x`, and then the outer call returns `(+ x) y` where `x` and `y` are the `Nat` values generated with the applications. In sum: A bunch of lucky choices have to be made here. And this is just for a two-argument function. For 4 or more aruguments it would be very unlikely to succeed. + +## Tuning: Making unlikely inputs more likely (and vice versa) + +General assumption: We will get run-time feedback that will feed into doing these things. But we could also imagine driving them with static analysis, e.g., per the [Boltzman tuning idea, marrying probabilistic programming and PBT](https://dl.acm.org/doi/full/10.1145/3763082), or even just having an LLM look at the code. Deferring this question to the end. + +### Generator refinement: Changing weights + +Generators often randomly choosing amongst a set of alternatives: For a Cedar expression of type `bool` you could generate a conjuction `X && Y`, a conditional `if e then X else Y`, a literal `true` or `false`, etc. (where `X` and `Y` are expressions that have type `bool`, generated recursively). These alternatives might have equal probability by default. During the tuning process we might decide to increase the weight for conjunctions and `has-`checks, which could increase the chances of `x has C && x.C` for example. + +While weighting is surely part of the solution, it's not the whole solution. There are some downsides of only changing the weights of individual terms: + +1. This might result in more failures overall, due to backtracking. We just increase the chances of ending up in an unlikely scenario. So we get a "better" distribution but fewer useful inputs. +2. This might result in a few more intersting terms while skewing the distribution toward "almost interesting" terms, e.g., `x has C && true` or `x has C`. These terms don't test what we really want to test, which is `x.C` when `C` is optional. + +### Generator restructuring: Compound rules + +When changing weights doesn't make a situation likely enough, or has the downsides mentioned above, we can adjust the _structure_ of the generator to make the situation more likely. + +For example, suppose we decide that we are not generating enough `op` applications for Strata. It's not clear how we can address the problems mentioned above just by changing weights (which will also have negative downstream consequences). To make an `op` plus its arguments much more likely, we might just elect to generate them all together with a kind of compund rule: select an `op`, generate expressions with the types of its arguments as normal, and then call it － we are not relying on several "generate a function and apply" rules to land in our favor later. The generate-`op`-then-its-arguments approach was recommended by Palka. It is basically a _derived_ typing rule that adds no additional type-checking power, but directs generation more effectively. + +We might apply this pattern more generally. For example, suppose we decide to generate a record deref `x.C`, then to succeed we know we need to precede it in a conjunction with an expression `e` such that `C ∈ ɑ`. We could hardcode `e` to just be `x has C && ...` but this is a little unsatisfying. What if there is a bug that arises only in the expression `if true then x has C else false && x.C` but not in `x has C && x.C`? We are unlikely to find it. So we want to generate a _compatible context_ for a term, and then the term itself. A key question is how to get this general context reliably (more below). + +### Application to Specimen, using runtime feedback + +My sense is that to apply these two ideas two Specimen, we can take the following steps: + +1. For frequency weights, we can configure the generator so that the weights can be specified from the outside. That allows an LLM agent to make observations and tune the weights. I have a feeling that this is possible now, but I'm not sure. + +2. For structural composition, we can ask an LLM to synthesize new rules that should be admissable by the existing ones, but which improve the quality of generation. For example, in addition to rules for application and op-lookup, we synthesize an admissable rule like Palka's. Then we ask the LLM to prove that the admissable rule is indeed admissable, and act as normal. + +A key question is what sort of signal does an agent need to leverage these tuning approaches. Let's assume that we will gather run-time information from test runs, based on instrumentation -- this is one reason, BTW, for Specimen to target Basalt generators, since they can be parameterized to include instrumentation and Plausible cannot. One potentially useful sort of generation is failures: When a checker fails which causes backtracking, log the construct the failure was in and the variable it was on. If we also instrument the constructor in which a variable was first generated, we can see that the creation site failed to produce a value that satisfied the checking site. That might be an opportunity for composition. + +> As an aside: You could also imagine a special kind of backtracking in which a failed check backtracks directly to the generation site along with the failed constraint, which the generator can attempt to satisfy. I think this is difficult though because there may be other implicit constraints that were satisfied by checks in between that we don't necessarily know about. You'd need to gather per-variable successful checks along with the failed ones in order to re-generate properly. Then you also probably need some way to "replay" the same choices you made before, to get back to the failed check. Seems hard. + +### The feedback loop + +Both interventions — reweighting and rule-addition — are moves in a loop that +observes generation, decides what to change, and re-runs. It's worth naming the +loop's parts, because each has open design questions. + +- **Observation.** What do we log from a run? Candidates, from cheap to rich: + (a) *coverage* — which constructors of the target relation fired, and how often + (a histogram); (b) *outcome shape* — of the inputs produced, how many were + trivial vs. interesting (e.g. the "non-empty ⟹ contains-Redeem" invariant we + already track in `Results.md`); (c) *backtracking events* — the + `(constructor, variable, failed-check)` records described above, which point at + *where* a path got stuck. Coverage tells you *what* is under-explored; + backtracking tells you *why*. Only Basalt generators can carry this + instrumentation, which is one reason to target them. + +- **Inference.** Given observations, what do we change and how? The observation + →action map is the hard part, and there are several plausible drivers: + *statistical* (hill-climb weights to flatten a coverage histogram — cheap, + local, and blind to structure); *heuristic* (a fixed rule like "a constructor + with 0 coverage and repeated backtracking on variable `v` is a candidate for + inlining/compound-rule around `v`"); or *LLM-driven* (hand the agent the + coverage histogram, the backtracking log, and the relation source, and ask for + a diagnosis plus a proposed intervention). These are not exclusive — statistics + can pick weights while an LLM proposes rules. + +- **Action.** The two levers differ in cost and reversibility. Reweighting is a + cheap, continuous, fully-reversible edit to a config vector (see + `Generator-config.md`). Rule-addition is a discrete, structural change that + carries a proof obligation (the new rule must be admissible — see below) and + cannot be undone by nudging a number. A loop should probably exhaust the cheap + lever before reaching for the expensive one, but see the note below on why + that's a cost ordering, not a strict hierarchy. + +- **Reward / stopping.** When is the generator "tuned enough"? We need a target + the loop optimizes toward. Flat constructor coverage is one proxy; distance + from a Boltzmann-style target distribution over term *shapes* is another (see + the aside on Boltzmann tuning below); "every scenario in a synthesized suite is + realized at least once" is the criterion the scenario approach gives for free. + Without a stopping condition the loop has no notion of done. + +Two clarifications on how the levers relate. First, they **compose** cleanly — +you can reweight a generator that has had compound rules added, and adding a rule +introduces new choice points that themselves want weights. Second, it is *not* +clear that one **dominates** the other, so this is a cost ordering (try the cheap +lever first), not a strict hierarchy: reweighting cannot make a 0-coverage +constructor fire when the path to it is un-invertible (that's the whole point of +the inlining experiments), and rule-addition is overkill when a path is reachable +but merely under-sampled. They address different failure modes — "unreachable" +vs. "under-explored" — and a real tuner needs both. + +> Aside — Boltzmann tuning. The [probabilistic-programming-meets-PBT line of +> work](https://dl.acm.org/doi/full/10.1145/3763082) gives a principled way to +> hit a *target distribution over term shapes* by solving for branch weights, +> rather than hand-tuning them. It is the right theory for the reweighting lever +> — but it tunes a distribution over shapes a generator can *already* produce; it +> says nothing about shapes the generator reaches with probability zero. So +> Boltzmann tuning is the mature form of the *weight* lever, and structural +> rule-addition is what you need when no weight vector suffices. + +## A different approach: Scenario-based testing + +We might imagine trying to be more goal directed. Rather than randomly picking an expression type, or API command, at each step, we could say, first: +1. "I want to generate an application with op" (for Strata) +2. "I want to generate a `x.C` (for Cedar) +3. "I want to generate a "delete policy P" (for AVP) + +Then, second, we generate inputs to produce the necessary context that makes generating 1, 2, or 3 valid, and then generate that. + +Thus testing becomes: Enumerate _scenarios_ you want to test (step 1), and then generate contexts for each scenario and run the tests (step 2). + +This is basically what S3 HiFi does, where the scenarios are defined by a kind of predicate abstraction over the S3 state space, with especial attention paid to failure cases, and testing those are handled properly. + +**Why this is not just "tune one generator harder."** The single-generator route +of the previous sections produces a *distribution* and samples it repeatedly; you +get thoroughness by making the interesting inputs likely and drawing enough +samples. Scenario testing changes the shape of the activity: you *enumerate* a +finite set of behaviorally-distinct situations, then produce one input per +situation. HiFi's headline result is exactly this contrast — systematic +enumeration deterministically covers in ~8 requests what random PBT covers +stochastically in ~3200. You are trading a distribution you sample for a suite +you construct. The two halves of that construction are quite different problems: + +- **Second half — realize a scenario (mostly solved).** Given a chosen scenario, + produce a concrete input that realizes it. This is a constrained generation + problem, run roughly *backwards*: the scenario fixes a target (a state, or an + enabled command, or a required judgment) and we generate a context reaching it. + The mechanisms of the previous sections apply directly. For a scenario "test a + call to `op`" in Strata, the context is satisfied by a Palka-style rule — I can + call `op` once I have well-typed values for its arguments. For "test a `x.C` + dereference" in Cedar, the context is a term with a hole that makes `x.C` + well-typed. The context-generation machinery below is what does this half. + +- **First half — synthesize the scenarios (the open problem).** Where does the + scenario set come from? HiFi gets it from a human-authored predicate + abstraction over the state space. The ambition is to *derive* it from the + inductive specification: the constructors' premises are the features, the + implications between premises are the state invariant `inv_Ω` that rules out + spurious combinations, and the satisfying truth-assignments over features are + the scenarios (partitioned into success vs. error cases). This note does not + solve the first half — the companion **scenario-generation design** develops it + as a four-phase pipeline (feature/scenario extraction, goal-directed planning, + campaign organization by error count, validation), with a hand-written + BoundedBuffer prototype. See that document for the details and its open + questions (feature granularity, planner complexity, generation-by-execution vs. + upfront generation, scaling, non-determinism). + +The through-line of this whole note: **you want thorough testing, and you have +two routes to it** — one generator that you tune until its samples cover +everything, or the two-part scenario approach that constructs a covering suite +directly. They share the second-half machinery (constrained, backwards-ish +context generation); they differ in whether a scenario set is synthesized up +front. + +## Context generation: the shared machinery + +Both routes lean on the same capability, so it deserves its own treatment: given +a target we want to hit (a required judgment, an enabled command), produce a +*context* — a term with a hole — into which the target term can be plugged so the +whole thing is valid. + +One way to view this is as a kind of _backwards_ generator. For the Cedar +example: instead of a generator that takes `ɑ`, `Γ`, `τ` and produces `e`, `ε` +such that `ɑ ; Γ ⊢ e : τ ; ε`, we want a generator that takes `ɑ`, `Γ`, `τ`, `ε` +and produces a context `E` such that the hole in `E` can be filled by a term `e` +with `ɑ ; Γ ⊢ e : τ ; ε`. For `x.C` the `Γ` says `x` has optional field `C` of +type `τ`, `ε` is empty, and `C ∈ ɑ`. We are giving *constraints* on the input to +this backwards generator, not the inputs themselves, so we'd have to synthesize +them from those constraints. + +But it's not really a backwards generator, because we are producing a context +(which has a hole), not a term. The Palka rule is similar: to call `op`, generate +a context `E` that invokes `op` on its arguments, e.g. `E = [] 1 2` where +`op = +`. + +**Is there a general way to derive this?** I think the promising framing is: a +context is itself an object of a *derived inductive relation*, and if we can +state that relation, Specimen derives its generator by the usual machinery. So +the question "can we generate contexts?" reduces to "can we *derive the context +relation* from the term relation?" Sketch, for a typing judgment +`WellTyped : Env → Expr → Ty → Prop`: + +```lean +-- WTContext env E envₕ τₕ τ ≜ E is a one-hole context such that, if the hole +-- is filled by any e with `WellTyped envₕ e τₕ`, then `WellTyped env E[e] τ`. +-- (envₕ, τₕ) are the *requirements the context imposes on its hole*. +inductive WTContext : Env → Ctx → Env → Ty → Ty → Prop where +| Hole : WTContext env □ env τ τ -- the empty context +| ConjR : WellTyped env lhs Bool → -- lhs establishes capability + WTContext (extend env lhs) (Expr.and lhs □) envₕ τₕ Bool +-- ...one such rule per position of the hole in each WellTyped constructor +``` + +The content of each `WTContext` constructor is mechanical from a `WellTyped` +constructor: pick which sub-expression is the hole, keep the *other* premises as +context obligations (`WellTyped env lhs Bool`), and thread the environment the way +the original rule does (so `x has C && []` correctly delivers `C ∈ ɑ` to the +hole). This is the same move as the step-inlining work, generalized: inlining +pulls a callee relation's constructors into a caller and threads a shared +variable; deriving `WTContext` "pulls the hole out" of `WellTyped` and threads the +environment to the hole. Two things make this more than a rename and are the real +work to validate: + +1. **Multiple holes and depth.** `Hole` gives a depth-0 context; the recursive + rules grow it. We likely want a size/depth bound (as with inlining's `k`) and, + for realism, more than one hole (to reach `x has C && [] && []`). A one-hole + relation is the place to start. +2. **Admissibility is automatic here.** For the *single-generator* route we add + compound rules and must prove them admissible (every term the rule generates + was already derivable). Here there is no separate obligation: `WTContext` is + *defined* so that `WTContext env E envₕ τₕ τ` and `WellTyped envₕ e τₕ` imply + `WellTyped env E[e] τ` — that implication is the derivation target, provable + once, generically, over the shape of the derivation, rather than per generated + term. + +Concrete next experiment: hand-write `WTContext` for the `AttrGuardExperiment`'s +`WT` relation (its `chk`/`drf` are a stripped-down `has`/`x.C`), derive its +generator with Specimen, and check that it produces *diverse* guarding contexts +for a `drf`, not just the single `chk (sq k) □` pairing the fused experiment +already gets. Success = high `drf` rate *and* context diversity; that would show +the backwards/context half of both routes is derivable, not just hand-buildable. + +## Appendix: prior work in this project + +The ideas above are not starting from scratch — several pieces are already +built or designed. This appendix positions each within the note's framing so the +main text can stay at the level of intent. + +- **Step inlining** ([Lookahead-experiment.md](./Lookahead-experiment.md)) is the + worked-out form of the *structural rule-addition* lever, for the special case of + a `Step`/`Trace` state-transition spec. A forward (0-lookahead) generator can + fail to fire a command *at all* when its precondition was set up by an earlier + step and can't be read back off the state; inlining `k+1` adjacent steps into + one constructor moves the cross-step link inside the scheduler's joint-scheduling + window, so a fresh variable is bound once and the link is *computed forward* + rather than guessed-and-inverted. The vault and attr-guard experiments show the + 0 → ~320 / 0 → ~580 jumps this produces. This is exactly a mechanically-derived + Palka-style compound rule — evidence that the "structural" lever is real and, at + least for step relations, automatable. The `WTContext` sketch above is the + generalization of this move from step relations to arbitrary judgments. + +- **Culling provably-dead constructors** ([Results.md](./Results.md), + `specimen.cullDeadCtors`) is the static-pruning half of inlining: inlining emits + `bᵏ` constructors, most of them infeasible, and culling discharges "this + constructor can never fire" as a `premises → False` goal handed to Lean's own + automation (`simp_all`/`omega`/`decide`). Sound by construction (drop only what + Lean proves dead), it is what keeps the structural lever from blowing up. In the + feedback-loop terms above, this is not a tuning move an agent makes — it's a + derivation-time optimization that makes the structural lever affordable. + +- **Scenario generation** (the companion scenario-generation design, HiFi-derived) + is the *first half* of the two-part route: deriving the scenario set (features + from premises, `inv_Ω` from premise implications, scenarios as satisfying + assignments, campaigns by error count) from the inductive spec, with a + hand-written BoundedBuffer prototype. The note above deliberately does not + duplicate it; it only connects the *second* half (realize-a-scenario = backwards + context generation) to the single-generator machinery. + +- **Steering** ([Steering-notes.md](./Steering-notes.md)) is the adjacent, still + speculative question of *aiming* an already-adequate forward generator at a + specific rare target — orthogonal to making it adequate. It argues (as the main + text does) that control-planning and data-solving cannot be staged, only + interleaved, and connects the reachability pruning of culling to goal-directed + path search. + +- **Generator configuration** ([Generator-config.md](./Generator-config.md)) is + the plumbing the *reweighting* lever needs: externally-specified size bounds and + sub-generator selection, in the Basalt style Specimen is expected to target. + +### On implicit cross-command constraints + +The `Issue`/`Redeem` vault is worth calling out as a case where the constraint +from an earlier command to a later one is *implicit* — the state does not record +what the later step will need. Recall the relation: + +```lean +inductive VStep : Vault → VCmd → VResult → Vault → Prop where +| DoIssue : ∀ t, VStep none (VCmd.Issue t) VResult.IssueOk (some t) +| DoRedeem : ∀ t k, t = sq k → + VStep (some t) (VCmd.Redeem k) VResult.RedeemOk none +``` + +The state is `Option Nat`. It faithfully carries the ticket `t` from `Issue` to +`Redeem` — so in one sense the constraint *is* state-based. But the state tells +you nothing *useful* for generation: `Redeem` needs the *root* `k` with +`t = sq k`, and the state stores the square, from which the root cannot be read +back. The obligation that `t` be a perfect square is never stated at `Issue` +(where `t` is chosen); it is imposed only later, at `Redeem`, and by then the +value is committed. So the earlier command must satisfy a precondition it is never +told about — the link is implicit, discoverable only by looking across the step +boundary. This is precisely why 0-lookahead forward generation scores 0/1000 +Redeems and why inlining (which puts both steps in one scope, binds a fresh `k`, +and computes `t = sq k` forward) is the fix. It is also the cleanest small example +of the general point that the state abstraction which makes a spec *look* +state-based can hide the constraint that actually governs generation. \ No newline at end of file diff --git a/Scenario-Generation-DESIGN.md b/Scenario-Generation-DESIGN.md new file mode 100644 index 0000000..d1f9522 --- /dev/null +++ b/Scenario-Generation-DESIGN.md @@ -0,0 +1,177 @@ +# Scenario Generation: From Random Traces to Systematic Validation + +## Problem Statement + +Specimen can derive constrained generators from inductive relation specifications. +For trace-based testing (e.g., `SafeBBTrace`), the forward generator produces random +sequences of operations starting from an initial state — but the resulting traces +cluster around easy-to-satisfy paths (lots of `SizeOp`, few interesting interleavings +of `PutOp`/`GetOp`). The backward generator is worse: it degenerates to all-`SizeOp` +traces because it guesses predecessor states rather than computing them. + +The fundamental issue: **random generation explores stochastically, when what we need +is systematic coverage of all behaviorally-distinct scenarios.** + +## Inspiration: HiFi (High Fidelity Models for Large Scale Stateful Services) + +The HiFi paper (Jaber et al., OSDI '26) describes a manual MBT pipeline for S3 that: + +1. **Abstracts** API parameters and state into features/categories (equivalence classes + that trigger the same SuT behavior) +2. **Enumerates** all non-spurious input scenarios (truth assignments over feature + predicates, filtered by a state invariant inv_Ω) +3. **Plans** a path from the current state to each scenario's required state via an + API-planner that issues preparatory requests +4. **Concretizes** abstract scenarios into concrete requests +5. **Validates** the SuT's response against the model, organized by error count + (0-error, 1-error, 2-error campaigns) + +Key results: systematic scenario enumeration deterministically covers in 8 requests +what PBT covers stochastically in ~3200. The tool prevents 300+ regressions in S3's +CI/CD pipeline. + +## The Opportunity + +For an inductive relation like `BBSafeStep`, the entire HiFi pipeline structure is +**already implicit in the specification**: + +| HiFi Concept | Lean Inductive Analog | +|---|---| +| Features/categories | Premises of each constructor | +| Scenarios | Distinct premise configurations | +| inv_Ω | Implications derivable from constructor structure | +| API-planner | Goal-directed trace generator | +| Model execution | Relation evaluation via `DecOpt`/enumerator | +| Response validator | Differential testing (relation vs. implementation) | +| Error scenarios | `¬CanStep` / negative constructors | + +The vision: **derive the entire systematic testing pipeline from the inductive spec.** + +## Architecture (4 Phases) + +### Phase 1: Feature & Scenario Extraction + +From the constructors of a step relation, identify: +- **Features**: abstract predicates over state (buffer_empty, buffer_full, etc.) +- **State invariant (inv_Ω)**: implications between features that rule out spurious + combinations (can't be both empty and full; non-empty implies within-capacity) +- **Scenarios**: all satisfying truth assignments to features, partitioned by whether + the operation succeeds (safe) or fails (error) + +For `BBSafeStep`, the features are derived from premise shapes: +- `WithinCapacity (v :: s) c` → "buffer not full" (length < capacity) +- Pattern `v :: s` in GetOp → "buffer non-empty" +- `WithinCapacity s c` in SizeOp → "buffer within capacity" (always true for reachable states) + +### Phase 2: Goal-Directed Planning (API-Planner) + +Given a target scenario (a set of state predicates that must hold), produce a +trace from the initial state to a state satisfying those predicates. + +For BoundedBuffer: +- Target "buffer non-empty": generate one or more PutOps +- Target "buffer full": generate exactly `capacity` PutOps +- Target "buffer empty": either start (already empty) or generate Gets to drain + +This is **generation-by-execution**: iteratively pick an action that moves toward +the goal, execute it against the model, repeat until the goal holds. + +For simple systems like BB, the planner is deterministic. For complex systems +(many features, indirect dependencies), planning becomes a search problem — +potentially reducible to proof search over the constructors. + +### Phase 3: Campaign Organization + +Organize scenarios by error count (following HiFi's first-error hypothesis): + +- **0-error campaigns**: For each safe constructor, plan to a state where its + premises hold, then execute the operation and validate. +- **1-error campaigns**: For each error constructor, plan to a state where the + error's precondition holds (e.g., buffer full → PutOp errors), execute, and + validate that the error is produced correctly. +- **2-error campaigns**: Validate error precedence when multiple errors are possible. + +### Phase 4: Validation Execution + +For each scenario in a campaign: +1. Run the planner to reach the target state (executing each step against both + model and SuT to detect deviations during setup) +2. Concretize the scenario request (pick concrete values from the relevant category) +3. Execute against both model and SuT +4. Compare responses + +## Implementation Plan + +### Step 1: Manual Prototype (this PR) + +Hand-write the complete HiFi pipeline for BoundedBuffer: +- Explicitly define features, scenarios, and inv_Ω +- Implement a goal-directed planner that reaches each scenario's target state +- Organize tests into 0-error and 1-error campaigns +- Demonstrate deterministic coverage vs. the existing random approach + +This validates the architecture works in Lean and identifies which parts are +mechanical/automatable. + +### Step 2: Scheduler Enhancement — Invertible Functions + +Teach Specimen's scheduler that when generating backward, equalities involving +invertible functions (e.g., `s' = List.concat s v` with `s'` known) can be +solved by inversion rather than guess-and-check. This directly fixes the +backward generator quality issue. + +### Step 3: Derive Planner + +Implement a `derive_planner` metaprogram that, given a trace relation and a +goal predicate, synthesizes a goal-directed generator. The planner analyzes +each constructor's "effect" (how it changes state) and selects constructors +whose effects move toward the goal. + +### Step 4: Derive Campaign + +Implement `derive_campaign` that: +1. Extracts features from the step relation's premises +2. Derives inv_Ω from constructor structure +3. Enumerates non-spurious scenarios (via all-SAT or enumeration) +4. Synthesizes a planner for each scenario +5. Produces a complete test harness + +## Comparison: Random PBT vs. Systematic Scenario Generation + +For the BoundedBuffer with capacity 3: + +**Random PBT** (current forward generator, 1000 traces of size ≤10): +- Covers PutOp, GetOp, SizeOp in various combinations +- May never hit "buffer exactly full then Put" (error scenario) +- May never hit "buffer exactly full then Get" (interesting safe scenario) +- Coverage depends on luck and trace length + +**Systematic** (HiFi-style): +- 0-error scenarios: PutOp-on-non-full, GetOp-on-non-empty, SizeOp (3 scenarios) +- 1-error scenarios: PutOp-on-full, GetOp-on-empty (2 scenarios) +- Total: 5 scenarios, each hit exactly once with a planned trace +- 100% behavioral coverage, deterministic + +## Open Questions + +1. **Feature granularity**: How fine-grained should extracted features be? HiFi + uses domain expertise to identify meaningful categories. Can we derive + "meaningful" automatically from the relation structure? + +2. **Planner complexity**: For BB, planning is trivial. For systems with + non-reversible operations or complex state dependencies, planning may require + backtracking search. How does this compose with Specimen's existing search + infrastructure (enumerators, bounded search)? + +3. **Generation-by-execution vs. upfront generation**: Specimen currently generates + entire values upfront. The planner model requires interleaving generation with + model execution. Can this be expressed as a monadic generator that threads + state, or does it require a fundamentally different execution model? + +4. **Scaling**: HiFi handles 10^25 scenarios for GetObject via campaign budgeting + and the first-error hypothesis. For Specimen, what's the analog of "time budget" + when tests run at elaboration time vs. runtime? + +5. **Non-determinism**: HiFi's model allows multiple valid responses (set of + acceptable errors). Specimen's inductive relations are inherently deterministic + in their logical content. How to express "the SuT may return any of these errors"? diff --git a/SpecimenTest/DeriveArbitrarySuchThat/BoundedBufferScenarios.lean b/SpecimenTest/DeriveArbitrarySuchThat/BoundedBufferScenarios.lean new file mode 100644 index 0000000..2711900 --- /dev/null +++ b/SpecimenTest/DeriveArbitrarySuchThat/BoundedBufferScenarios.lean @@ -0,0 +1,452 @@ +import Plausible.Arbitrary +import Plausible.DeriveArbitrary +import Specimen.DeriveChecker +import Specimen.DeriveConstrainedProducer +import Specimen.EnumeratorCombinators + +/-! +# Systematic Scenario Generation for BoundedBuffer + +This file implements the HiFi-style systematic testing pipeline manually for the +BoundedBuffer specification. It demonstrates what we ultimately want to derive +automatically from the inductive relation. + +The pipeline: +1. Feature extraction (predicates over state) +2. Scenario enumeration (non-spurious truth assignments) +3. Goal-directed planning (reach a state satisfying each scenario) +4. Campaign execution (differential testing per scenario) +-/ + +open Plausible + +namespace BoundedBufferScenarios + +----- +-- SPECIFICATION (imported from BoundedBuffer, repeated here for self-containment) +----- + +abbrev BB := (List String) × Nat + +inductive BBCmd where +| Put (v : String) +| Get +| Size +deriving Repr + +inductive BBResult where +| PutOk +| GetOk (v : String) +| SizeOk (n : Nat) +| Error +deriving Repr, BEq + +abbrev BBTrace := List (BBCmd × BBResult) + +inductive WithinCapacity : List String → Nat → Prop where +| mk : s.length ≤ c → WithinCapacity s c + +inductive BBSafeStep : BB → BBCmd → BBResult → BB → Prop where +| PutOp: ∀ s s' c v, + WithinCapacity (v :: s) c → + s' = List.concat s v → + BBSafeStep (s,c) (BBCmd.Put v) BBResult.PutOk (s',c) +| GetOp: ∀ s c v, + WithinCapacity (v :: s) c → BBSafeStep (v :: s, c) BBCmd.Get (BBResult.GetOk v) (s,c) +| SizeOp: ∀ s c, + WithinCapacity s c → BBSafeStep (s,c) BBCmd.Size (BBResult.SizeOk (List.length s)) (s,c) + +inductive CanStep : BB → BBCmd → Prop where +| intro : ∀ bb c r bb', BBSafeStep bb c r bb' → CanStep bb c + +inductive BBStep : BB → BBCmd → BBResult → BB → Prop where +| SafeStep: ∀ bb c r bb', BBSafeStep bb c r bb' → BBStep bb c r bb' +| ErrStep: ∀ bb c, ¬ CanStep bb c → BBStep bb c BBResult.Error bb + +----- +-- PHASE 1: FEATURE EXTRACTION +----- + +-- Features are boolean predicates over state that appear (explicitly or +-- implicitly) as premises in the step relation's constructors. +-- +-- From BBSafeStep we extract: +-- PutOp premises: WithinCapacity (v :: s) c → "not full" (s.length + 1 ≤ c) +-- GetOp premises: pattern (v :: s) → "non-empty" (s.length ≥ 1) +-- WithinCapacity (v :: s) c → "within capacity" +-- SizeOp premises: WithinCapacity s c → "within capacity" +-- +-- Distilled features for BB state (s, c): +-- buffer_empty: s.length = 0 +-- buffer_full: s.length = c +-- buffer_partial: 0 < s.length ∧ s.length < c +-- +-- These partition the state space (given capacity > 0). + +structure BBFeatures where + bufferEmpty : Bool + bufferFull : Bool + bufferPartial : Bool + deriving Repr, BEq + +def extractFeatures (bb : BB) : BBFeatures := + let (s, c) := bb + { bufferEmpty := s.length == 0 + bufferFull := s.length == c + bufferPartial := s.length > 0 && s.length < c } + +----- +-- STATE INVARIANT (inv_Ω) +----- + +-- Implications that rule out spurious feature combinations: +-- buffer_empty ∧ buffer_full → only if capacity = 0 (degenerate) +-- buffer_empty → ¬buffer_partial +-- buffer_full → ¬buffer_partial +-- exactly one of {empty, partial, full} holds (partition) +-- +-- For capacity > 0, the features form a clean partition. + +def featuresConsistent (f : BBFeatures) (capacity : Nat) : Bool := + -- Exactly one of the three is true + let count := (if f.bufferEmpty then 1 else 0) + + (if f.bufferFull then 1 else 0) + + (if f.bufferPartial then 1 else 0) + count == 1 && + -- Full requires capacity > 0 (otherwise degenerate) + (!f.bufferFull || capacity > 0) + +----- +-- PHASE 2: SCENARIO ENUMERATION +----- + +-- A scenario pairs a target state feature configuration with an operation to test. +-- We distinguish safe scenarios (operation succeeds) from error scenarios. + +inductive ScenarioOutcome where +| Safe +| Error +deriving Repr, BEq + +structure Scenario where + name : String + targetFeatures : BBFeatures + operation : BBCmd + expectedOutcome : ScenarioOutcome + deriving Repr + +-- Enumerate all non-spurious scenarios for BB with capacity > 0. +-- For each (feature-config, operation) pair, determine if the operation +-- succeeds or errors in that state. +-- +-- PutOp: succeeds when ¬full (empty or partial), errors when full +-- GetOp: succeeds when ¬empty (partial or full), errors when empty +-- SizeOp: always succeeds (no error condition in the spec) + +def allScenarios : List Scenario := [ + -- 0-error scenarios (safe operations) + { name := "put_on_empty" + targetFeatures := { bufferEmpty := true, bufferFull := false, bufferPartial := false } + operation := .Put "X" + expectedOutcome := .Safe }, + { name := "put_on_partial" + targetFeatures := { bufferEmpty := false, bufferFull := false, bufferPartial := true } + operation := .Put "X" + expectedOutcome := .Safe }, + { name := "get_on_partial" + targetFeatures := { bufferEmpty := false, bufferFull := false, bufferPartial := true } + operation := .Get + expectedOutcome := .Safe }, + { name := "get_on_full" + targetFeatures := { bufferEmpty := false, bufferFull := true, bufferPartial := false } + operation := .Get + expectedOutcome := .Safe }, + { name := "size_on_empty" + targetFeatures := { bufferEmpty := true, bufferFull := false, bufferPartial := false } + operation := .Size + expectedOutcome := .Safe }, + { name := "size_on_partial" + targetFeatures := { bufferEmpty := false, bufferFull := false, bufferPartial := true } + operation := .Size + expectedOutcome := .Safe }, + { name := "size_on_full" + targetFeatures := { bufferEmpty := false, bufferFull := true, bufferPartial := false } + operation := .Size + expectedOutcome := .Safe }, + -- 1-error scenarios + { name := "put_on_full" + targetFeatures := { bufferEmpty := false, bufferFull := true, bufferPartial := false } + operation := .Put "X" + expectedOutcome := .Error }, + { name := "get_on_empty" + targetFeatures := { bufferEmpty := true, bufferFull := false, bufferPartial := false } + operation := .Get + expectedOutcome := .Error } +] + +def zeroErrorScenarios : List Scenario := + allScenarios.filter (·.expectedOutcome == .Safe) + +def oneErrorScenarios : List Scenario := + allScenarios.filter (·.expectedOutcome == .Error) + +----- +-- PHASE 3: GOAL-DIRECTED PLANNING (API-PLANNER) +----- + +-- The planner produces a trace from the initial state to a state satisfying +-- the target features. It works by generation-by-execution: at each step, +-- pick an operation that moves toward the goal, execute it against the model, +-- and repeat. + +-- Model execution: given a state and command, compute the result and new state. +-- Returns none if the command errors (shouldn't happen during planning since +-- the planner only issues commands it knows will succeed). +def modelStep (bb : BB) (cmd : BBCmd) : Option (BBResult × BB) := + let (s, c) := bb + match cmd with + | .Put v => + if s.length + 1 ≤ c then + some (.PutOk, (List.concat s v, c)) + else + none + | .Get => + match s with + | v :: rest => some (.GetOk v, (rest, c)) + | [] => none + | .Size => + some (.SizeOk s.length, (s, c)) + +-- Values to use during planning (arbitrary concrete choices). +def planValues : List String := ["A", "B", "C", "D", "E"] + +-- The planner: reach a state satisfying the target features from the given state. +-- Returns the trace of operations executed to reach the target state, and the +-- final state achieved. +-- +-- Strategy: +-- target empty + currently non-empty → Get until empty +-- target full + currently not full → Put until full +-- target partial + currently empty → Put once +-- target partial + currently full → Get once +partial def plan (current : BB) (target : BBFeatures) (fuel : Nat := 20) : Option (BBTrace × BB) := + if fuel == 0 then none + else + let currentFeatures := extractFeatures current + if currentFeatures == target then + some ([], current) + else + let (s, _) := current + -- Decide next action based on where we are vs where we want to be + let nextCmd := + if target.bufferEmpty && !currentFeatures.bufferEmpty then + -- Need to empty: Get + some BBCmd.Get + else if target.bufferFull && !currentFeatures.bufferFull then + -- Need to fill: Put + let v := planValues.getD s.length "Z" + some (BBCmd.Put v) + else if target.bufferPartial && currentFeatures.bufferEmpty then + -- Need partial from empty: Put once + some (BBCmd.Put (planValues.getD 0 "Z")) + else if target.bufferPartial && currentFeatures.bufferFull then + -- Need partial from full: Get once + some BBCmd.Get + else + none + match nextCmd with + | none => none + | some cmd => + match modelStep current cmd with + | none => none -- shouldn't happen if planner logic is correct + | some (result, newState) => + match plan newState target (fuel - 1) with + | none => none + | some (restTrace, finalState) => + some ((cmd, result) :: restTrace, finalState) + +----- +-- PHASE 4: CAMPAIGN EXECUTION (DIFFERENTIAL TESTING) +----- + +-- System under test: the circular buffer implementation +structure CircularBuffer where + buf : Array String + head : Nat + tail : Nat + +def mkCircularBuffer (capacity : Nat) (buggy : Bool := false) : IO (ST.Ref IO.RealWorld CircularBuffer) := + let slots := if buggy then capacity else capacity + 1 + ST.mkRef { buf := Array.replicate slots "", head := 0, tail := 0 } + +def sutPut (cb : ST.Ref IO.RealWorld CircularBuffer) (v : String) (buggy : Bool := false) : IO Unit := do + let s ← cb.get + let newTail := (s.tail + 1) % s.buf.size + if !buggy && newTail == s.head then + throw <| IO.userError "put: buffer full" + let buf := s.buf.set! s.tail v + cb.set { s with buf, tail := newTail } + +def sutGet (cb : ST.Ref IO.RealWorld CircularBuffer) (buggy : Bool := false) : IO String := do + let s ← cb.get + if !buggy && s.head == s.tail then + throw <| IO.userError "get: buffer empty" + let v := s.buf[s.head]! + cb.set { s with head := (s.head + 1) % s.buf.size } + return v + +def sutSize (cb : ST.Ref IO.RealWorld CircularBuffer) : IO Nat := do + let s ← cb.get + return (s.tail + s.buf.size - s.head) % s.buf.size + +-- Execute a single command against the SuT, returning its result. +-- For error scenarios, we expect the SuT to throw. +def sutExecuteCmd (cb : ST.Ref IO.RealWorld CircularBuffer) (cmd : BBCmd) (buggy : Bool := false) + : IO (Option BBResult) := do + match cmd with + | .Put v => + let ok ← (do sutPut cb v buggy; return true) <|> return false + return if ok then some .PutOk else some .Error + | .Get => + let result ← (do let v ← sutGet cb buggy; return (some (.GetOk v))) <|> return (some .Error) + return result + | .Size => + let n ← sutSize cb + return some (.SizeOk n) + +-- Execute a trace against the SuT, validating each step matches the model. +def executeAndValidateTrace (cb : ST.Ref IO.RealWorld CircularBuffer) + (trace : BBTrace) (buggy : Bool := false) : IO Unit := do + for (cmd, expectedResult) in trace do + let sutResult ← sutExecuteCmd cb cmd buggy + match sutResult with + | none => throw <| IO.userError s!"SuT returned no result for {repr cmd}" + | some actual => + if actual != expectedResult then + throw <| IO.userError s!"Deviation: cmd={repr cmd}, model={repr expectedResult}, sut={repr actual}" + +-- Execute a single scenario end-to-end: +-- 1. Plan a trace to reach the target state +-- 2. Execute the setup trace against both model and SuT (validating agreement) +-- 3. Execute the scenario's operation and validate the outcome +def executeScenario (scenario : Scenario) (capacity : Nat) (buggy : Bool := false) : IO Unit := do + let initial : BB := ([], capacity) + -- Phase 3: Plan to reach target state + let some (setupTrace, targetState) := plan initial scenario.targetFeatures + | throw <| IO.userError s!"Planner failed for scenario '{scenario.name}'" + -- Phase 4a: Execute setup trace against SuT (validates model/SuT agreement during setup) + let cb ← mkCircularBuffer capacity buggy + executeAndValidateTrace cb setupTrace buggy + -- Phase 4b: Execute the scenario's operation + let sutResult ← sutExecuteCmd cb scenario.operation buggy + -- Phase 4c: Validate against model expectation + let modelResult := modelStep targetState scenario.operation + match scenario.expectedOutcome, modelResult, sutResult with + | .Safe, some (expectedRes, _), some actualRes => + if actualRes != expectedRes then + throw <| IO.userError s!"Scenario '{scenario.name}': model={repr expectedRes}, sut={repr actualRes}" + | .Error, none, some .Error => + pure () -- Both model and SuT agree: operation errors + | .Error, none, some other => + throw <| IO.userError s!"Scenario '{scenario.name}': expected error, sut returned {repr other}" + | .Safe, none, _ => + throw <| IO.userError s!"Scenario '{scenario.name}': model says error but scenario expects safe" + | .Error, some _, _ => + throw <| IO.userError s!"Scenario '{scenario.name}': model says safe but scenario expects error" + | _, _, none => + throw <| IO.userError s!"Scenario '{scenario.name}': SuT returned no result" + +----- +-- CAMPAIGN RUNNERS +----- + +-- 0-error campaign: all safe scenarios +def zeroErrorCampaign (buggy : Bool := false) : IO Unit := do + IO.println s!"=== 0-Error Campaign ({zeroErrorScenarios.length} scenarios) ===" + for scenario in zeroErrorScenarios do + executeScenario scenario 3 buggy + IO.println s!" PASS: {scenario.name}" + IO.println "All 0-error scenarios passed." + +-- 1-error campaign: all error scenarios +def oneErrorCampaign (buggy : Bool := false) : IO Unit := do + IO.println s!"=== 1-Error Campaign ({oneErrorScenarios.length} scenarios) ===" + for scenario in oneErrorScenarios do + executeScenario scenario 3 buggy + IO.println s!" PASS: {scenario.name}" + IO.println "All 1-error scenarios passed." + +-- Full campaign: run all scenarios systematically +def fullCampaign (buggy : Bool := false) : IO Unit := do + zeroErrorCampaign buggy + oneErrorCampaign buggy + IO.println s!"\n=== SUMMARY ===" + IO.println s!"Total scenarios: {allScenarios.length}" + IO.println s!" Safe scenarios: {zeroErrorScenarios.length}" + IO.println s!" Error scenarios: {oneErrorScenarios.length}" + IO.println "All campaigns passed. 100% behavioral coverage achieved." + +-- Run the full campaign against the correct implementation +#guard_msgs(drop info) in +#eval fullCampaign + +-- Run against the buggy implementation — should detect deviation during setup +-- (the buggy impl doesn't reject puts on a full buffer, so the "put_on_full" +-- scenario will see the SuT succeed where the model expects an error) +/--error: Scenario 'size_on_full': model=BoundedBufferScenarios.BBResult.SizeOk 3, sut=BoundedBufferScenarios.BBResult.SizeOk 0-/ +#guard_msgs(error, drop info) in +#eval fullCampaign (buggy := true) + +----- +-- COMPARISON: COVERAGE ANALYSIS +----- + +-- The systematic approach covers every distinct behavior in exactly 9 test executions. +-- Compare with the random approach that needs ~1000 traces to probabilistically +-- cover the same space (and may miss the error scenarios entirely). + +def coverageReport : IO Unit := do + IO.println "=== Coverage Report ===" + IO.println "" + IO.println "Feature space: {empty, partial, full} × {Put, Get, Size}" + IO.println " = 9 combinations total" + IO.println "" + IO.println "Non-spurious scenarios: 9" + IO.println " Safe (0-error): 7" + IO.println " put_on_empty, put_on_partial" + IO.println " get_on_partial, get_on_full" + IO.println " size_on_empty, size_on_partial, size_on_full" + IO.println " Error (1-error): 2" + IO.println " put_on_full, get_on_empty" + IO.println "" + IO.println "Spurious (filtered by inv_Ω): 0" + IO.println " (all feature×operation pairs are reachable for capacity > 0)" + IO.println "" + IO.println "Deterministic coverage: 9 test executions = 100% of distinct behaviors" + IO.println "Random PBT equivalent: ~1000 traces to probabilistically approach same coverage" + +#guard_msgs(drop info) in +#eval coverageReport + +----- +-- INTROSPECTION: WHAT THE PLANNER PRODUCES +----- + +-- Show the setup traces generated by the planner for each scenario +def showPlannerTraces : IO Unit := do + IO.println "=== Planner Traces (capacity=3) ===" + for scenario in allScenarios do + let initial : BB := ([], 3) + match plan initial scenario.targetFeatures with + | none => IO.println s!" {scenario.name}: PLANNER FAILED" + | some (trace, finalState) => + let steps := trace.map fun (cmd, _) => repr cmd + IO.println s!" {scenario.name}:" + IO.println s!" setup = {steps}" + IO.println s!" reached state = {repr finalState}" + IO.println s!" then execute: {repr scenario.operation} → {repr scenario.expectedOutcome}" + +#guard_msgs(drop info) in +#eval showPlannerTraces + +end BoundedBufferScenarios