Cairn.Fuzz.Target
lean/Cairn/Fuzz/Target.lean
What the fuzzer knows about an app
A Target bundles a machine (and the App built from it, if any) with what the claims say
about it. fuzz_targets% (Cairn.Fuzz.Collect) builds one per machine in the app's
modules (and its dependencies') at compile time, so an app needs no fuzz code of its own.
Imports Cairn.Fuzz.Rng, Cairn.Claims.Core
Structures 2
InvCheck (S : Type) : Type
An invariant, with its runnable check if it has one (invariant generates check when its
statement is decidable).
info : ClaimInfo
decl : StringThe invariant's declaration, relative to the app's namespace (for printed flows).
check : Option (S → Bool)Target : Type 1
name : StringFixture: what lake exe fuzz is given. A dependency's has its package in front,
cairn_atproto/Claims.
module : StringFixture, the machine's module.
package : StringThe machine's Lake package (fixture), or "" if Lake named none.
dependency : BoolWhether the machine is a dependency's rather than the fuzz executable's own package's: run
only when named, or with --deps.
ns : StringThe namespace the claims live in, for printed flows.
machineDecl : StringThe machine's and the app's declarations, relative to ns.
appDecl : Option StringS : Type
machine : Claims.Machine self.S
app : Option (App self.S)
keyed : List ClaimId
Claim ids of the keyed moves (^N#k).
invariants : List (InvCheck self.S)
claims : List ClaimInfo
Every claim the app's module declares, retired ones included.
custom : Custom self.S
Definitions 2
srv (t : Target) : Server t.S
The app's server, or Server.empty (no world, nothing handled).
W (t : Target) : Type
What the app's server holds (Unit without one).