Cairn.Fuzz.Walk
lean/Cairn/Fuzz/Walk.lean
The walk
One sequence: a window size, text metrics, and operations generated from the current state (or replayed from a list), each checked against the app's claims (docs/fuzz.md).
An app with an App is driven through the real runtime (Runtime.route and Runtime.step):
an action is performed as the pointer and key events a person would use, so hit testing, focus
and routing are exercised along with the app. A machine without an App gets its actions
directly (machine.update).
Between a person's operations the host has its say (Cairn.Fuzz.Host): it answers the requests
the frames carried, fires timers by sending the clock, sends subscription events and drops
images, as the trusted claims allow.
Imports Cairn.Fuzz.Target, Cairn.Fuzz.Text, Cairn.Fuzz.Metrics, Cairn.Fuzz.Host, Cairn.Runtime, Cairn.Layout.Check, Cairn.Frame.Dump, Std.Data.HashMap, Std.Data.HashSet
Structures 6
Failure : Type
A failed check: which check, on which claim and key, after which operation.
Setup : Type
How a sequence starts.
seed : Natsize : Size
metrics : MetricsChoice
start : Time
The host's clock when the sequence starts: its first clock boots the app.
World (S W : Type) : Type
A sequence's state: the runtime's, what the fuzzer has seen, the host's, and the world of
the app's server (Custom.server; Unit without one).
rt : Runtime.State S
seen : Std.HashMap ClaimId Nat
The largest key seen on screen per keyed move, so "enabled but missing" can be probed.
host : Host
The host: what the frames asked of it, its clock, its images.
secure : List ControlRef
Every secure field seen on screen so far, whose edits are printed redacted.
server : W
parked : List (ControlRef × Nat × Int)
The virtual lists the app keeps (App.keepScroll) that are not on screen, with the row
that was first showing when each left, and where in the box.
lastLists : List Runtime.LaidList
Each virtual list as it was last on screen: while a list is off screen (hidden, kept), none of its rows is laid, so a control keyed like one of its rows may be missing.
Performed (S W : Type) : Type
The result of performing one operation.
world : World S W
acts : List Action
The actions delivered to update, in order.
ran : BoolWhether the operation ran at all (an act whose control is missing is skipped).
maxNs : NatThe slowest event's Runtime.step (update, view, layout, settle), in nanoseconds.
dropped : BoolA press or double press the runtime dropped by design: its pointerDown delivered a blur,
and after that step the pressed control is no longer at the point, so the release lands
elsewhere and presses nothing (docs/runtime.md; TodoMVC decision T33 in docs/plan.md: the
edit saves first, and if saving moved what was clicked, the click is dropped). This is
exactly where Runtime.click_presses's hypothesis fails, so "performed" does not apply.
msg : Option Msg
The message the host sent, for a host's move (Custom.relations).
effects : List Effect
The effects the operation's steps put on the frame.
msgDropped : BoolWhether the runtime dropped the host's message without delivering it.
ClaimStat : Type
Counters for one claim.
steps : Natchecks : Std.HashMap String Nat
sequences : NatlastSeq : Option NatThe last sequence that touched it, so sequences counts each once.
Outcome : Type
What one sequence did.
setup : Setup
ops : Array Op
failure : Option Failure
stats : Stats
steps : Natover : Array (Nat × Nat)
Steps over the frame budget: (step, nanoseconds).
maxNs : Natskipped : NatSteps where pressability was skipped because the window was below the minimum.
host : HostStats
What the host did.
secure : List ControlRef
The secure fields seen, whose edits are printed redacted.
Inductive types 2
Op : Type
One operation of a sequence. Self-contained, so a subsequence replays without the seed.
Source : Type
Where a sequence's operations come from: the generator, or a fixed list (replay).
Definitions 73
refLean (c : ControlRef) : String
opLean : TextOp → String
actionLean : Action → String
keyText (k : Key) (m : Mods) : String
opText : Op → String
An operation, as a person would say it.
secureRefs (l : Laid) : List ControlRef
The secure fields in a laid tree.
bulletsOf (s : String) : String
redactText : TextOp → TextOp
A text operation with its text replaced by bullets.
redactAction (secure : List ControlRef) : Action → Action
An action, with an edit of one of secure redacted.
redactIn (secure : List ControlRef) : Op → Op
mkFail (check : String) (r : ControlRef) (step : Nat) (message : String) : Failure
same (a b : Failure) : Bool
Ran : Type
A check that ran on a claim: (claim, check kind).
cfgOf (m : MetricsChoice) : Runtime.Config
runApp (t : Target) : App t.S
The app, or a stand-in with an empty view for a machine without one.
move? (t : Target) (id : ClaimId) : Option (Claims.Move t.S)
isKeyed (t : Target) (id : ClaimId) : Bool
budgetNs (t : Target) : Nat
minSize (t : Target) (m : TextMetrics) (s : t.S) (ui : UI) : Size
The smallest window for a state: the fuzz config's; else the minimum the app asks the host
for (App.minSize), which the host keeps the window at or above (trusted ^1010), so a person
never sees a smaller one; else, when the app asks for none, the view's preferred size.
after {S : Type} (h : Host) (before : List (Nat × Sub))
(rt : Runtime.State S) (es : List Effect) : HostThe host after a step: it takes in the effects the frame carried, the frame's images count as used, and the subscriptions the runtime stopped are remembered (their events can still be in flight).
serverStart (t : Target) (setup : Setup) : t.W
The server's world a sequence starts with: Server.init from the sequence's seed.
start (t : Target) (setup : Setup) : World t.S t.W
The first frame, then the host's first clock, which boots the app (App.initEffects).
opEvents : TextOp → List Event
The events a text operation arrives as. setCaret has none (it comes from clicks).
clickEvents (p : Point) (clicks : Nat) : List Event
statusControls {S : Type} (rt : Runtime.State S) :
List (ClaimId × ControlRef × Bool)The controls a shown status item puts on screen besides the window's laid tree: its button
(StatusItem.control, pressed by opening its menu) and its menu's items, each with its place and
whether it is enabled. The frame carries them in its surface records (docs/surfaces.md); the host
builds the button and a real NSMenu from them, so they are on screen whenever the item is shown,
the menu's items whether or not it is open.
controlMenuItems {S : Type} (rt : Runtime.State S) (visible : Bool := false) :
List (Runtime.Target × ControlRef × Bool)The items of the menus of controls on screen (docs/surfaces.md, "Menus on controls"), each
with its owner and whether it is enabled. They are in the frame whenever their control is (as
present counts a control scrolled out of view): the host builds the native menu from the frame
when it opens. visible: only those whose control shows, which a person can open.
controlMenuPress {S : Type} (rt : Runtime.State S) (c : ControlRef)
(enabled : Bool := true) : Option (List Event)The events that choose c in a control's menu: open it, choose the item, and the close the
host sends when the menu returns.
onStatus {S : Type} (rt : Runtime.State S) (r : ControlRef) : BoolWhether r is an enabled control on a status item: one a person can press now.
statusPress {S : Type} (rt : Runtime.State S) (c : ControlRef) :
Option (List Event)The events that press c on a status item: opening the menu for its button, choosing the
item for a menu item (Runtime.step's menuOpen and menuSelect).
opToEvents {S : Type} (rt : Runtime.State S) : Op → Option (List Event)The events that perform an operation in the current state; none when an action's control
isn't on screen (or can't take that action), so the operation is skipped.
hostPlan {S : Type} (rt : Runtime.State S) (h : Host) :
HostOp → Option (Host × List Event × Option Msg)The host's events for its move, the host once it has made it, and the message it sent (for
Custom.relations); none when the move can't happen now (a replayed subsequence whose request
was never made). Every batch starts with the clock (^908).
hostStep {S : Type} (sv : Server S) (rt : Runtime.State S) (h : Host)
(sw : sv.W) : HostOp → sv.W × Option (Host × List Event × Option Msg)The host's move with server sv (Custom.server), whose world is sw: the world after,
and the host, events and message as hostPlan's, or none when the move can't happen now (then
the world is sw). serve and tick change the world; a reply to a request the server takes
sends the reply it gave (and can't happen until it has given one); lose (lost after) and
fail (failed before) answer a request it takes with a fault, after and before it handled it.
Every other move is hostPlan's, and leaves the world alone. The world is returned even when
the move can't happen, so the caller never keeps a second reference to it.
answers (id : Nat) : HostOp → Bool
The moves that answer request id.
perform (t : Target) (setup : Setup) (w : World t.S t.W) (op : Op) : IO (Performed t.S t.W)
probeKeys {W : Type} (t : Target) (w : World t.S W) (id : ClaimId) : List NatKeys to probe for a move: those on screen, the largest seen so far, and one past it.
noteSeen {S W : Type} (w : World S W) (laid : Laid) : World S W
isPointer {S : Type} (m : Claims.Move S) : Bool
firstBad (l : Laid) : Option (String × Laid)
The first node, in paint order, that breaks one of Pressable's conditions, and which.
firstBadList : List Laid → Option (String × Laid)
indexOf (ll : LaidList) (k : Nat) : Option Nat
The index of key k among a laid list's keys, if it is one.
laidAt (ll : LaidList) (i : Nat) : Bool
Whether the list laid its row i.
rows (ll : LaidList) : List (Nat × Laid)
The rows the list laid, each with its index: its children between the two spacers.
contentTop (ll : LaidList) : Int
The top of the list's content box, on screen.
rowClaims (lists : List Runtime.LaidList) : List ClaimId
The moves with a control in a laid row of a list, keyed by the row's key: their controls show exactly when their row is laid.
noteLists (known lists : List Runtime.LaidList) : List Runtime.LaidList
lastLists after a frame: each list on screen replaces what was known of it.
vlistFault (ll : Runtime.LaidList) : Option String
What is wrong with a laid list, if anything: the rows laid are exactly those whose extent
meets the viewport widened by the overscan, in the heights the view laid out by (Model.top,
the specification, not the fast path the view used; VList.node_rows); there are no more than
(viewport + 2·overscan) / minHeight + 2 of them; and the spacers and rows are one under the
other from the content's top less the offset (Layout.vlist_stacked).
unsettledRow (ll : Runtime.LaidList) : Option (Nat × Int × Int)
A laid row whose height isn't the one the view laid the list out by: the runtime hadn't
recorded it yet when it stopped laying out (Runtime.settleAll, Runtime.unsettled).
anchor (ll : LaidList) : Option (Nat × Int)
The first row of a laid list that shows: its key and its top, relative to the content's top.
moves : Op → Bool
An operation that may scroll or resize, after which the anchor needn't stay still.
lastScrolls (effects : List Effect) : List (ControlRef × ScrollTarget)
A step's scroll requests, the last for each box.
scrollToChecks (laid : Laid) (ui : UI) (effects : List Effect) (stepIx : Nat) : List Ran × List Failure
scrollTo lands (Runtime.aimOff_start, aimOff_finish, aimOff_key,
firstF_top). After a step that asked for it, a box on screen is at 0 for start and at its
limit for finish; for key k, the row with key k is the first showing, at the top of the
box, unless the clamp holds the list at its end.
keptChecks (keep : List ControlRef) (ui0 ui : UI) (before after : List Runtime.LaidList) (parked : List (ControlRef × Nat × Int)) (stepIx : Nat) : List Ran × List Failure × List (ControlRef × Nat × Int)
A kept list comes back where it was (Runtime.fixUI_keeps_offset,
fixUI_keeps_list). A virtual list the app keeps (App.keepScroll) that leaves the view keeps
its offset while it is away, and when it comes back the row that was first showing when it left
is first showing again, at the same place in the box, unless the clamp moved it (to 0 or the
limit) or the row is gone. Returns the lists parked now.
anchorChecks (before after : List Runtime.LaidList) (op : Op) (stepIx : Nat) (effects : List Effect := []) : List Ran × List Failure
The anchor stays still. Over an operation that doesn't scroll or resize, the first row
showing in each virtual list keeps its place in the box, wherever rows were inserted or heights
changed above it (VList.record_keeps), unless the clamp moved the offset (to 0 or the
limit) or the row is gone. A clamp within the operation's batch that a later step lifts doesn't
excuse it: the row is held, and put back (VList.record_holds, record_returns).
droppedCheck : StringThe check name a dropped click is counted under (Performed.dropped).
checks {W : Type} (t : Target) (setup : Setup) (w : World t.S W)
(act? : Option Action) (acts : List Action) (stepIx : Nat) (dropped : Bool := false)
(effects : List Effect := []) : List Ran × List FailureEvery check after an operation: the checks that ran and the failures. act? is the
action the operation meant to perform, if it ran.
candidates {W : Type} (t : Target) (w : World t.S W) :
List (ControlRef × Trigger × Bool)The actions available now: for each control on screen whose move is enabled, each trigger
it can take there, and a press on each enabled status-item control (statusControls). Without
an App, each enabled move and probed key.
textScript (t : Target) (s : t.S) (id : ClaimId) : Gen (List TextOp)
genAct {W : Type} (t : Target) (w : World t.S W) : Gen (Option (List Op))An action of a control on screen, picked in proportion to the control's weight
(Custom.weights, default 1; 0 never). none when nothing can be picked.
genPoint {S W : Type} (w : World S W) : Gen Point
genSize (min : Size) : Gen Size
A window size at or above the minimum, or (one in twenty) below it.
genScroll {S W : Type} (w : World S W) : Gen OpA wheel or trackpad scroll: mostly at a point in a scroll box, by a tick, a flick or (one in eight) far past either end, to test the clamp; sometimes sideways.
scrollKeys : List Key
The keys that scroll (docs/runtime.md, "Scrolling").
genNoise {W : Type} (t : Target) (setup : Setup) (w : World t.S W) :
Gen (List Op)
genOps {W : Type} (t : Target) (setup : Setup) (w : World t.S W) : Gen (List Op)The next operations: the host's move (Host.share: one time in five or more while it has
something to say, a request, a timer or a subscription, one in thirty otherwise); else mostly an enabled
action, otherwise pointer, key or window noise.
genSetup (t : Target) (seed : Nat) : Setup × Rng
A sequence's setup from its seed: metrics, then a window at or above the initial minimum.
relationChecks (t : Target) (tr : Transition t.S) (stepIx : Nat) (direct : Bool := false) : List Ran × List Failure
The app's checks over one step (Custom.relations), from state s0 by the host's message
msg (none for a person's operation) to s1.
drain (t : Target) (setup : Setup) (w : World t.S t.W) (rng : Rng) (fuel : Nat) : IO (World t.S t.W × Nat)
The host answers everything outstanding, oldest first, with the app's replies (or the
default), until nothing is or fuel runs out. Returns the world and how many replies it sent.
serverChecks (t : Target) (w : World t.S t.W) (stepIx : Nat) (kind : String) (cks : List (ClaimId × (t.S → t.W → Bool))) (after : String) : List Ran × List Failure
The server's checks (Server.checks) on the app's state and the world: the checks that ran
and the failures, each failure's message naming the world (Server.describe).
Stats : Type
record (st : Stats) (seq : Nat) (ran : List Ran) : Stats
runSeq (t : Target) (setup : Setup) (src : Source) (stats : Stats := ∅) (verbose : Bool := false) : IO Outcome
Run one sequence, stopping at the first failure. Verbose prints each step.
Theorems 7
lookup_filter_ne (l : List (Nat × Request)) (id : Nat) : List.lookup id (List.filter (fun x => x.fst != id) l) = none
hostPlan_reply_sent {S : Type} {rt : Runtime.State S} {h h' : Host} {id : Nat}
{r : Reply} {es : List Event} {m : Option Msg}
(hp : hostPlan rt h (HostOp.reply id r) = some (h', es, m)) :
h'.sent = List.filter (fun x => x.fst != id) h.sentA reply leaves the host holding every request but the one answered.
hostStep_answers_once {S : Type} (sv : Server S) (rt : Runtime.State S)
(h : Host) (sw : sv.W) (op : HostOp) (id : Nat) (ha : HostOp.answers id op = true)
{h' : Host} {es : List Event} {m : Option Msg}
(hs : (hostStep sv rt h sw op).snd = some (h', es, m)) :
(h.request? id).isSome = true ∧ h'.request? id = noneEach request is answered at most once, with or without a server: a move that answers
request id happens only while the host holds it, and the host holds it no more after.
hostStep_no_second_answer {S : Type} (sv : Server S) (rt rt' : Runtime.State S)
(h : Host) (sw sw' : sv.W) (op op' : HostOp) (id : Nat) (ha : HostOp.answers id op = true)
(ha' : HostOp.answers id op' = true) {h' : Host} {es : List Event} {m : Option Msg}
(hs : (hostStep sv rt h sw op).snd = some (h', es, m)) :
(hostStep sv rt' h' sw' op').snd = noneSo no second answer: once a move has answered request id, no move answers it again from
the host it leaves (until a new request with that id is sent, which the runtime never does).
hostStep_fail_world {S : Type} (sv : Server S) (rt : Runtime.State S) (h : Host)
(sw : sv.W) (id : Nat) (r : Reply) : (hostStep sv rt h sw (HostOp.fail id r)).fst = swA failed-before answer leaves the world as it was (by construction), and so do a lost-after answer and a reply.
hostStep_lose_world {S : Type} (sv : Server S) (rt : Runtime.State S) (h : Host)
(sw : sv.W) (id : Nat) (r : Reply) : (hostStep sv rt h sw (HostOp.lose id r)).fst = sw
hostStep_reply_world {S : Type} (sv : Server S) (rt : Runtime.State S) (h : Host)
(sw : sv.W) (id : Nat) (r : Reply) : (hostStep sv rt h sw (HostOp.reply id r)).fst = sw
Instances 8
instReprOp : Repr Op
instInhabitedOp : Inhabited Op
instBEqOp : BEq Op
instInhabitedFailure : Inhabited Failure
instReprFailure : Repr Failure
instReprSetup : Repr Setup
instInhabitedSetup : Inhabited Setup
instInhabitedClaimStat : Inhabited ClaimStat
As text: flow witness syntax for actions
Secure fields: printed as their length
What a person typed into a secure field (FieldView.secure) is printed as bullets, one per
scalar, in every report, shrunk sequence, flow and failure message: a fuzz report never holds
it (docs/fuzz.md, "Secure fields").
The world a sequence runs in
What the host does with a server
Two facts about hostStep, which hold with any server (Server.empty included), so with a
server present the host answers as it did without one:
- each request is answered at most once: a
reply, aloseor afailanswers only a request the host holds, and the host holds it no more after (hostStep_answers_once), so a second answer to it can't happen (hostStep_no_second_answer). A request the app cancelled is answered once too (^1009), and the runtime swallows it (step_reply_ignored); astraygoes only to ids neither holds (hostPlan); - a failed-before answer leaves the server's world as it was, as do a lost-after answer and a
reply(hostStep_fail_world): onlyserveandtickchange it.