Cairn.Fuzz.Shrink
lean/Cairn/Fuzz/Shrink.lean
Shrinking, and what a failure is printed as
Delta debugging (Zeller and Hildebrandt's ddmin) over a failing sequence's operations: remove chunks while the shorter sequence still fails the same check on the same claim, halving the chunk size down to single operations. Operations are self-contained, so a subsequence replays from the same setup without the seed.
The shrunk sequence becomes a ready-to-paste flow (with the next free id), whose witness is
the actions the runtime delivered while replaying it, minus those no move accepts (no-ops in
the model), so the witness is live.
Imports Cairn.Fuzz.Walk
Structures 1
Traced : Type
One replayed operation: the operation, the control a pointer operation hit (in the model), and the delivered actions some move accepts.
Definitions 7
stillFails (t : Target) (setup : Setup) (target : Failure) (ops : Array Op) : IO Bool
Whether replaying ops from setup fails the same check on the same claim.
without (xs : Array Op) (lo hi : Nat) : Array Op
shrink (t : Target) (setup : Setup) (target : Failure) (ops : Array Op) : IO (Array Op × Nat)
ddmin over complements, then a pass removing single operations. Returns the shrunk operations and how many replays it took.
trace (t : Target) (setup : Setup) (ops : Array Op) : IO (Array Traced)
Replay operations, recording what each did. Edits of a secure field are recorded redacted
(Op.redactIn), so a report, its sequence and its flow never hold what was typed into one.
capitalize (s : String) : String
lockMax (path : System.FilePath) : IO (Option Nat)
The largest id in claims.lock, if it can be read.
flowSource (t : Target) (setup : Setup) (f : Failure) (traced : Array Traced) (id : Nat) : String
A ready-to-paste flow for a shrunk failure, and for presence and pressability failures a
theorem to put beside the app's proofs. A flow's goal can only talk about the state (claims are
declared before the view), so the flow pins the state the failure needs, with a durable id,
and the theorem states what the view must do in it.