Scenario generation: design doc and manual BB prototype

[mwhicks1]

Summary

• Adds a design document (Scenario-Generation-DESIGN.md) outlining a HiFi-style systematic testing pipeline for Specimen, based on HiFi: High Fidelity Models for Large Scale Stateful Services (Jaber et al., OSDI '26)
• Implements a manual prototype (BoundedBufferScenarios.lean) demonstrating the full pipeline for the BoundedBuffer spec: feature extraction → scenario enumeration → goal-directed planning → differential testing campaigns
• Achieves 100% behavioral coverage deterministically in 9 test executions (7 safe + 2 error scenarios) vs. the ~1000 random traces needed by the existing PBT approach

Motivation

The existing forward/backward Specimen generators for SafeBBTrace explore stochastically — they cluster around easy-to-satisfy paths (mostly SizeOp) and may miss important scenarios (Put on full, Get on empty). The HiFi paper shows that systematic scenario enumeration with goal-directed planning is dramatically more efficient and provides measurable coverage guarantees.

The long-term goal is to derive this entire pipeline automatically from the inductive relation spec via new derive_planner / derive_campaign commands.

Design (4-phase architecture)

1. Feature extraction — identify predicates over state from constructor premises
2. Scenario enumeration — all-SAT over features filtered by state invariant (inv_Ω)
3. Goal-directed planning — generation-by-execution to reach each scenario's target state
4. Campaign execution — differential testing organized by error count (0-error, 1-error, ...)

Test plan

• BoundedBufferScenarios.lean builds cleanly with lake env lean
• All #guard_msgs assertions pass (correct impl passes, buggy impl detected)
• Planner reaches all 9 scenarios from initial state ([], 3)
• Discussion: does this architecture generalize well to STLC / LExpr examples?
• Discussion: which phases are most important to automate first?