Cairn.Fuzz.Host
lean/Cairn/Fuzz/Host.lean
The host
cairn fuzz's stand-in for the host's side of the world (docs/fuzz.md, "The host"): it keeps
what the frames asked of it and answers the way the real host is allowed to, as the trusted
claims state it (docs/trusted.md):
- Requests (^914 answered once; ^1009 a cancelled request is still answered once, usually
failed): each request a frame carries is answered once, in any order, as late as it likes, with a reply of its kind's shape or a failure; a request cancelled after it was sent is answered too (failed other "cancelled", or its answer if the work finished first), which the runtime swallows. - Images (^1006, ^1011): a load puts its pixels before it is answered, and a source the host
holds is answered from what it holds unless
reload; a failed reload drops the source; while animageCachesubscription runs and the held pixels are over its budget, the host drops the image used least recently that the latest frame doesn't draw and isn't the one just put, and says so withevicted(which can cross a load's reply). - Time (^908, ^909): every batch starts with a clock;
mononever goes back; a frame'swakebrings a clock at or up to 40 ms after it, which fires the due timers. - The Dock badge and announcements (^1030, ^1031): the badge is the label of the last
badgeeffect, or none; everyannounceis recorded once, with its text and priority. - Subscriptions (^915 and the device claims): events for active subscriptions,
every's ticks at most one a period; and, rarely, an event from a subscription the runtime just stopped, which crossed the stop.
Beyond the contract, and rarely: a reply to an id the runtime doesn't hold (answered before, or
never sent). The runtime drops it (step_reply_ignored); it is there to show nothing else
reacts.
Everything is decided by the generator from the sequence's seed and recorded in the operation
(HostOp), so a sequence replays without it.
Imports Cairn.Fuzz.Rng, Cairn.Runtime
Structures 3
Held : Type
An image the host holds.
source : Stringw : Nath : NatHostStats : Type
What the host did, over a sequence or a run.
requests : NatRequests and cancels the frames carried.
cancels : Natreplies : NatReplies to requests still awaited by the runtime, of which failures.
failed : NatcancelledReplies : NatReplies to requests cancelled after they were sent (the runtime swallows them).
stray : NatReplies the app's runtime still delivers but the app stopped waiting for are counted by the app, not here. Replies to ids the runtime doesn't hold.
clocks : Natwakes : NattimersDue : NatTimers due at a clock the host sent (they fire, unless an earlier one cancels them).
subEvents : NatlateSubEvents : Natloads : Natevictions : NatmaxOutstanding : NatThe most requests the host held at once.
leftOver : NatRequests still unanswered when sequences ended.
served : NatWith a server: requests it handled (retransmissions included), of which retransmissions; replies lost after it handled them; requests failed before reaching it; and times the world acted on its own.
retransmits : NatlostAfter : NatfailedBefore : Natticks : Natbadges : Natbadge and announce effects.
announcements : NatHost : Type
now : Time
sent : List (Nat × Request)
Requests on a frame, not yet answered: id and request, oldest first.
cancelled : List NatOf those, the ones a later frame cancelled.
ready : List (Nat × Reply)
Answers decided before they are sent: a load whose pixels are already put, or a request
the server has handled (HostOp.serve).
answered : List NatIds answered lately, for stray replies.
held : List Held
Images held, least recently used first.
lastPut : Option StringThe source put last: never the next one dropped.
started : List NatSubscription ids whose record has started, and globalKeys whose key is down.
keysDown : List Natstopped : List (Nat × Sub)
Subscriptions the runtime stopped lately.
stats : HostStats
Inductive types 1
HostOp : Type
What the host does in one step. Self-contained: replaying it needs no seed.
advance (ms : Nat) (wallJump : Int) : HostOp
The clock moves on by ms (wall time by ms + wallJump).
reply (id : Nat) (r : Reply) : HostOp
Answer request id, sent and not yet answered (cancelled or not).
load (id w h : Nat) : HostOp
A loadImage request's work finishes before its answer is sent: its pixels are put.
sub (s : Sub) (e : SubEvent) (dt : Nat) : HostOp
An event for the active subscription s, dt ms after the last batch.
late (id : Nat) (e : SubEvent) : HostOp
An event from a subscription the runtime has stopped (it crossed the stop).
evict (source : String) : HostOp
Drop source's pixels to keep within the image budget, and send evicted.
stray (id : Nat) (r : Reply) : HostOp
Beyond the contract: a reply to an id the runtime doesn't hold.
serve (id seed : Nat) : HostOp
With a server (Custom.server): request id reaches the server, which handles it with
the generator seeded seed (Server.handle); the world changes, and its reply waits until
the host sends it (reply) or loses it (lose). A second serve of the same request is a
retransmission: the server handles it again.
lose (id : Nat) (r : Reply) : HostOp
Lost after: the server handled request id, but its reply is lost; the app hears r.
fail (id : Nat) (r : Reply) : HostOp
Failed before: request id never reached the server, so the world is as it was; the app
hears r.
tick (seed : Nat) : HostOp
The server's world acts on its own (Server.tick, seeded seed).
Definitions 34
bytes (x : Held) : Nat
add (a b : HostStats) : HostStats
isSent (h : Host) (id : Nat) : Bool
isCancelled (h : Host) (id : Nat) : Bool
request? (h : Host) (id : Nat) : Option Request
heldOf (h : Host) (src : String) : Option Held
heldBytes (h : Host) : Nat
put (h : Host) (src : String) (w ht : Nat) : Host
Put src's pixels: it becomes the most recently used and the last put.
drop (h : Host) (src : String) : Host
touch (h : Host) (drawn : List String) : Host
A published frame draws these sources: they become the most recently used.
absorb (h : Host) (es : List Effect) : Host
Take in the effects a step put on the frame, in order.
answer (h : Host) (id : Nat) : Host
id is answered: the host forgets it.
takes {S : Type} (sv : Server S) (r : Request) : Bool
drawnIn : Laid → List String
The image sources a laid tree draws (Style.image, set once an image is ready).
drawnList : List Laid → List String
drawnBy {S : Type} (rt : Runtime.State S) : List StringEvery source the latest frame draws: the window's and the shown panels'.
imageCaches {S : Type} (rt : Runtime.State S) : List (Nat × Nat)The active imageCache subscriptions: ids and budgets.
evictable {S : Type} (h : Host) (rt : Runtime.State S) : Option StringThe image the host would drop next: while an imageCache runs and the held pixels are
over the smallest budget, the least recently used one the latest frame doesn't draw and that
wasn't just put (^1011).
notices {S : Type} (rt : Runtime.State S) (src : String) : List EventThe evicted notices for src, one to each running imageCache.
bytes (lo hi : Nat) : Gen ByteArray
fault : Gen Fault
failure : Gen Reply
word : Gen String
defaultReply (h : Host) (r : Request) : Gen Reply
A reply of r's kind with random contents: bytes, a status, a size, a flag, or a fault
(one in six). An image the host holds is answered with its size unless reload (^1006).
genReply {S : Type} (c : Custom S) (s : S) (h : Host) (id : Nat) (r : Request) :
Gen ReplyThe reply to id: the app's generator if it has one for this request (a reply of the
wrong shape becomes a failure), else the default.
genCancelled {S : Type} (c : Custom S) (s : S) (h : Host) (id : Nat)
(r : Request) : Gen ReplyThe answer to a request cancelled after it was sent (^1009): failed other "cancelled",
or, if its work had already finished (or can't be stopped), its ordinary answer.
genSubEvent {S : Type} (c : Custom S) (s : S) (h : Host) (id : Nat) (sub : Sub) :
Gen SubEventAn event for an active subscription: the app's generator, else one of the kind's events in
an order the host can send them (started once, before any audio; a key's up after its down).
subDelay (sub : Sub) : Gen Nat
The period before an event of sub: every ms ticks at most once a period (^915).
genAdvance : Gen HostOp
How far the clock moves when the host has nothing else to say.
genHost {S : Type} (c : Custom S) (h : Host) (rt : Runtime.State S) : Gen HostOpThe host's next move, given the latest frame.
replyText : Reply → String
The operation as a person reading the log would say it.
subText : Sub → String
text : HostOp → String
Instances 9
instInhabitedHostOp : Inhabited HostOp
instBEqHostOp : BEq HostOp
instReprHostOp : Repr HostOp
instBEqHeld : BEq Held
instReprHeld : Repr Held
instInhabitedHeld : Inhabited Held
instInhabitedHostStats : Inhabited HostStats
instReprHostStats : Repr HostStats
instInhabitedHost : Inhabited Host