Cairn.UI.Images
lean/Cairn/UI/Images.lean
Images: what an app knows of the images it shows
An app keeps one Images in its state. load asks the host for a source (Request.loadImage)
and remembers which request id is the source's latest; receive takes the reply to that id and
records the size or the failure. A reply to an earlier load of the same source, or to an id this
table never issued, changes nothing (receive_stale, load_supersedes), so a slow first load
can't overwrite a reload that answered first.
The view reads state for each source and builds Node.image with it: the node's size is the
app's choice and the same in every state (Layout.measure_image).
Imports Cairn.UI.Node, Cairn.Input
Structures 3
Images : Type
known : List (String × ImageState)
What is known of each source; a source not listed is loading.
pending : List (Nat × String)
Each source's latest load: request id and source.
Sys : Type
t : Images
has : BoolWhether the host holds pixels for each source.
q : List Note
Messages to the app, the next one first.
found : List (Nat × String)
Loads the host has held pixels for, which it may answer ready.
asked : List (Nat × String)
Every load the app made: id and source.
next : NatThe id the app's next load gets.
Inv (s : Sys) : Prop
What every reachable state keeps.
fresh : p.fst < s.next
unique : a = b
pendingAsked : p ∈ s.asked
foundAsked : p ∈ s.asked
readyFound : ∃ src, (id, src) ∈ s.found
held : s.has src = true ∨ Note.evicted src ∈ s.qAn image the table takes for ready is held, or its eviction is on its way.
heldPending : s.has src = true ∨ Note.evicted src ∈ s.qSo is one whose pending load the host answered or may answer ready.
Inductive types 3
Note : Type
A message to the app.
Step : Sys → Sys → Prop
load (s : Sys) (src : String) (reload : Bool) : Step s { t := (s.t.load s.next src reload).fst, has := s.has, q := s.q, found := s.found, asked := (s.next, src) :: s.asked, next := s.next + 1 }
The app loads src under its next id.
cancel (s : Sys) (t : Images) (hk : t.known = s.t.known) (hp : ∀ (p : Nat × String), p ∈ t.pending → p ∈ s.t.pending) : Step s { t := t, has := s.has, q := s.q, found := s.found, asked := s.asked, next := s.next }
The app stops waiting for some loads (cancel, cancelWhere, cancelAll).
find (s : Sys) (id : Nat) (src : String) (h : (id, src) ∈ s.asked) : Step s { t := s.t, has := setHas s.has src true, q := s.q, found := (id, src) :: s.found, asked := s.asked, next := s.next }
The host holds pixels for a load the app made (read and decoded, or already kept).
ready (s : Sys) (id : Nat) (src : String) (w h : Nat) (hf : (id, src) ∈ s.found) : Step s { t := s.t, has := s.has, q := s.q ++ [Note.reply id (Reply.image w h)], found := s.found, asked := s.asked, next := s.next }
The host answers ready a load it held the pixels for.
other (s : Sys) (id : Nat) (r : Reply) (hr : ∀ (w h : Nat), r ≠ Reply.image w h) : Step s { t := s.t, has := s.has, q := s.q ++ [Note.reply id r], found := s.found, asked := s.asked, next := s.next }
Any other answer, to any id.
evict (s : Sys) (src : String) : Step s { t := s.t, has := setHas s.has src false, q := s.q ++ [Note.evicted src], found := s.found, asked := s.asked, next := s.next }
The host drops src's pixels, then says so.
hearReply (s : Sys) (id : Nat) (r : Reply) (rest : List Note) (hq : s.q = Note.reply id r :: rest) : Step s { t := s.t.receive id r, has := s.has, q := rest, found := s.found, asked := s.asked, next := s.next }
The app hears a reply.
Reach : Sys → Prop
init (has : String → Bool) : Reach (init has)
step {s s' : Sys} : Reach s → Step s s' → Reach s'Definitions 14
setAt {α : Type} : List (String × α) → String → α → List (String × α)xs with k's entry replaced by v (or (k, v) appended).
state (t : Images) (source : String) : ImageState
What is known of source.
load (t : Images) (id : Nat) (source : String) (reload : Bool := false) : Images × Effect
Load source under request id id (fresh: the app's next request id). The source shows as
loading until the reply; any earlier load of it is forgotten. reload reads it again rather than
answering from the host's cache.
ofReply : Reply → ImageState
What a reply says about an image.
receive (t : Images) (id : Nat) (r : Reply) : Images
A reply: if id is a source's latest load, record what it says and stop waiting for it;
otherwise nothing changes.
waiting (t : Images) (id : Nat) : Bool
Whether the table is waiting for a reply to id.
loadAll (t : Images) (id : Nat) (reload : Bool) : List String → Images × List Effect
Load each of sources in order, under ids id, id + 1, …: the table and the requests.
cancel (t : Images) (source : String) : Images × List Effect
Stop waiting for source's latest load and cancel it.
cancelAll (t : Images) : Images × List Effect
Stop waiting for every load and cancel each one.
cancelWhere (t : Images) (p : String → Bool) : Images × List Effect
Stop waiting for the loads of every source p picks, and cancel each one.
isReady (t : Images) (source : String) : Bool
Whether the table takes source for ready.
evicted (t : Images) (source : String) : Images × List Effect
The host dropped source's pixels (SubEvent.evicted): forget that it is ready, stop waiting
for its loads and cancel them.
setHas (has : String → Bool) (src : String) (b : Bool) : String → Bool
has with src set to b.
init (has : String → Bool) : Sys
The app's table before anything was asked.
Theorems 32
lookup_setAt {α : Type} (xs : List (String × α)) (k : String) (v : α) :
List.lookup k (setAt xs k v) = some v
lookup_setAt_ne {α : Type} (xs : List (String × α)) (k k2 : String) (v : α)
(h : k ≠ k2) : List.lookup k2 (setAt xs k v) = List.lookup k2 xs
state_load (t : Images) (id : Nat) (source : String) (reload : Bool) : (t.load id source reload).fst.state source = ImageState.loading
receive_stale (t : Images) (id : Nat) (r : Reply) (h : List.lookup id t.pending = none) : t.receive id r = t
state_receive (t : Images) (id : Nat) (source : String) (r : Reply) (h : List.lookup id t.pending = some source) : (t.receive id r).state source = ofReply r
load_supersedes (t : Images) (id old : Nat) (source : String) (reload : Bool) (hne : old ≠ id) : List.lookup old (t.load id source reload).fst.pending ≠ some source
After a load of source, the table waits for no other id for it.
superseded_reply (t : Images) (id old : Nat) (source : String) (reload : Bool) (r : Reply) (hne : old ≠ id) : ((t.load id source reload).fst.receive old r).state source = ImageState.loading
A reply to a superseded load changes nothing: once source was loaded again under
id, the reply to any earlier id for it leaves what the table knows of source alone.
state_load_ne (t : Images) (id : Nat) (src other : String) (reload : Bool) (h : src ≠ other) : (t.load id src reload).fst.state other = t.state other
state_loadAll_notin (t : Images) (id : Nat) (reload : Bool) (src : String) (srcs : List String) : ¬src ∈ srcs → (t.loadAll id reload srcs).fst.state src = t.state src
state_loadAll (t : Images) (id : Nat) (reload : Bool) (src : String) (srcs : List String) : src ∈ srcs → (t.loadAll id reload srcs).fst.state src = ImageState.loading
After loading a list, each of its sources shows as loading until its reply.
pending_load (t : Images) (id : Nat) (src : String) (reload : Bool) (p : Nat × String) (h : p ∈ (t.load id src reload).fst.pending) : p.fst = id ∨ p ∈ t.pending
pending_loadAll (t : Images) (reload : Bool) (srcs : List String) (id : Nat) (p : Nat × String) : p ∈ (t.loadAll id reload srcs).fst.pending → id ≤ p.fst ∧ p.fst < id + srcs.length ∨ p ∈ t.pending
pending_load_src (t : Images) (id : Nat) (src : String) (reload : Bool) (p : Nat × String) (h : p ∈ (t.load id src reload).fst.pending) : p.snd = src ∨ p ∈ t.pending
pending_loadAll_src (t : Images) (reload : Bool) (srcs : List String) (id : Nat) (p : Nat × String) : p ∈ (t.loadAll id reload srcs).fst.pending → p.snd ∈ srcs ∨ p ∈ t.pending
pending_receive (t : Images) (id : Nat) (r : Reply) (p : Nat × String) (h : p ∈ (t.receive id r).pending) : p ∈ t.pending
loadAll_length (t : Images) (id : Nat) (reload : Bool) (srcs : List String) : (t.loadAll id reload srcs).snd.length = srcs.length
pending_cancelWhere (t : Images) (p : String → Bool) (q : Nat × String) (h : q ∈ (t.cancelWhere p).fst.pending) : q ∈ t.pending ∧ p q.snd = false
receive_cancelAll (t : Images) (id : Nat) (r : Reply) : t.cancelAll.fst.receive id r = t.cancelAll.fst
After cancelAll, no reply changes the table.
cancelAll_effects (t : Images) : t.cancelAll.snd = List.map (fun p => Effect.cancelRequest p.fst) t.pending
cancelAll cancels exactly the ids the table was waiting for.
receive_cancel (t : Images) (source : String) (id : Nat) (r : Reply) : ((t.cancel source).fst.receive id r).state source = (t.cancel source).fst.state source
After cancel source, a reply to any id leaves what is known of source alone.
state_evicted (t : Images) (source : String) (w h : Nat) : (t.evicted source).fst.state source ≠ ImageState.ready w h
After evicted, the source is not ready.
state_evicted_ne (t : Images) (source other : String) (h : source ≠ other) : (t.evicted source).fst.state other = t.state other
pending_evicted (t : Images) (source : String) (p : Nat × String) (h : p ∈ (t.evicted source).fst.pending) : p ∈ t.pending ∧ p.snd ≠ source
receive_evicted (t : Images) (source : String) (id : Nat) (r : Reply) : ((t.evicted source).fst.receive id r).state source = (t.evicted source).fst.state source
After evicted, no reply makes the source ready: the table waits for no load of it.
state_receive_waiting (t : Images) (id : Nat) (r : Reply) (source : String) (h : ∀ (p : Nat × String), p ∈ t.pending → p.snd ≠ source) : (t.receive id r).state source = t.state source
A reply leaves alone the state of a source the table waits for no load of.
ofReply_ready {r : Reply} {w h : Nat}
(e : ofReply r = ImageState.ready w h) : r = Reply.image w h
inv_init (has : String → Bool) : Inv (init has)
evicted_tail {src : String} {n : Note} {rest : List Note}
(hn : ∀ (s : String), n ≠ Note.evicted s) (h : Note.evicted src ∈ n :: rest) :
Note.evicted src ∈ restAn evicted notice behind a reply is still there once the reply is heard.
inv_step {s s' : Sys} (hi : Inv s) (hs : Step s s') : Inv s'
inv_reach {s : Sys} (h : Reach s) : Inv s
ready_held {s : Sys} (h : Reach s) (src : String) (w hh : Nat)
(e : s.t.state src = ImageState.ready w hh) : s.has src = true ∨ Note.evicted src ∈ s.qReady is never stale for long: in every state reached, an image the app's table takes for
ready has its pixels with the host, or an evicted notice for it is on its way to the app.
ready_held_quiet {s : Sys} (h : Reach s) (hq : s.q = []) (src : String)
(w hh : Nat) (e : s.t.state src = ImageState.ready w hh) : s.has src = trueOnce the app has heard everything, ready means the host holds the pixels.
Instances 2
instReprImages : Repr Images
instInhabitedImages : Inhabited Images
Loading several sources
Pending ids
Cancelling
A load still in flight holds one of the runtime's request slots (App.maxInFlight) until the
host answers it. cancel and cancelAll stop waiting and ask the runtime to cancel: a queued
request is never sent, a sent one is cancelled at the host, and its reply reaches no app
(Book.cancel_blocks). A cancelled source keeps what was known of it (loading if it never
answered) until it is loaded again.
Evicted images
With Sub.imageCache the host keeps its decoded images within a byte budget: past it, it drops
the images used least recently that the latest frame doesn't draw, and says so with
SubEvent.evicted once the pixels are gone. evicted forgets such an image: a ready one goes
back to loading, and the table stops waiting for (and cancels) any load of it still in flight,
because that load's reply may say ready for pixels dropped since. The app loads it again when it
wants to show it.
The cache, modelled
Cache puts the table together with the host: whether it holds each source's pixels, the
messages on their way to the app (replies and evicted notices, in the order the app hears
them), and the loads the host has found pixels for. The host's moves are what ^1011 says of it:
it answers a load ready only after it held the pixels for it (find, then ready), and every
time it drops a source's pixels it says so afterwards (evict). The app's are loads, cancels
and hearing each message in turn with receive and evicted; the runtime may swallow a reply
(drop). In every state reached, an image the table takes for ready has its pixels with the
host, or an evicted notice for it is still on its way (ready_held); so once the app has heard
everything, ready means the pixels are there (ready_held_quiet).