Cairn.Fuzz.Main
lean/Cairn/Fuzz/Main.lean
lake exe fuzz
lake exe fuzz <App> [--seed S|random] [--iterations N] [--steps K] [--budget-ms M]
[--out DIR] [--shrink N] [-v]
lake exe fuzz --list [--deps]
Runs sequences with seeds S, S+1, …, S+N−1 (the SEED and ITERATIONS environment variables
set the defaults), stops each at its first failure, shrinks the first failure of each kind,
prints it as a flow, and writes <DIR>/<App>.json (docs/fuzz.md). Exit code 1 when anything
failed. --list names the package's own targets, and its dependencies' too with --deps; any
target can be run by name (cairn_atproto/Claims). Two targets with one name are refused (exit
code 2), never one shadowing the other.
Imports Lean.Data.Json, Cairn.Fuzz.Shrink
Structures 1
Opts : Type
app : Stringseed : Natiterations : Natsteps : NatbudgetMs : Option Natout : Option Stringshrinks : Natverbose : Boollist : Booldeps : BoolDefinitions 23
opJson : TextOp → Lean.Json
kind (k : String) : Lean.Json
ext (k : String) (e : Bool) : Lean.Json
actionJson (a : Action) : Lean.Json
An action step, in the shape of a flow's witness in lake exe claims.
keyName : Key → String
faultName (f : Fault) : String
hexOf (b : ByteArray) : String
replyJson : Reply → Lean.Json
hostJson : HostOp → Lean.Json
hostStatsJson (h : HostStats) : Lean.Json
stepJson (tr : Traced) : Lean.Json
metricsJson : MetricsChoice → Lean.Json
sequenceJson (t : Target) (setup : Setup) (traced : Array Traced) : Lean.Json
parseArgs (o : Opts) : List String → Except String Opts
num (v : String) (k : Nat → Except String Opts) : Except String Opts
usage : String
fmt2 (hundredths : Nat) : String
Hundredths, as text: fmt2 1234 = "12.34".
msText (ns : Nat) : String
Nanoseconds as milliseconds, to hundredths.
msJson (ns : Nat) : Lean.Json
claimJson (t : Target) (stats : Stats) (fails : Array (Failure × Setup)) (c : ClaimInfo) : Lean.Json
Per-claim evidence: pass (true/false), or null with a note when it wasn't run.
runTarget (t : Target) (o : Opts) : IO UInt32
duplicate? : List Target → Option String
A name two of targets share, if any (cairn#221).
main (targets : List Target) (args : List String) : IO UInt32