Cairn.Runtime.ScrollProofs
lean/Cairn/Runtime/ScrollProofs.lean
Theorems about scrolling and appear (docs/runtime.md, "Scrolling" and "Appear"): every
offset stays within its box after every step, a scroll changes nothing but the UI, Tab brings
the focus into view, and appear moves are exactly the marked controls that came on screen.
Imports Cairn.Runtime.Proofs
Definitions 1
Clamped (laid : Laid) (ui : UI) : Prop
Every offset the runtime keeps is for a scroll box of laid, within
[0, max 0 (content − viewport)] of that box.
Theorems 47
clampOff_mem (o : Int) (sc : Scroller) : 0 ≤ clampOff o sc.limit ∧ clampOff o sc.limit ≤ max 0 (sc.content - sc.viewport)
clampScroll_clamped (scs : List Scroller) (offs : List (ControlRef × Int)) (e : ControlRef × Int) : e ∈ clampScroll scs offs → ∃ sc, sc ∈ scs ∧ sc.ref = e.fst ∧ 0 ≤ e.snd ∧ e.snd ≤ max 0 (sc.content - sc.viewport)
fixUI_clamped (laid : Laid) (pointer : Option Point) (ui : UI) (keep : List ControlRef) : Clamped laid (fixUI laid pointer ui keep)
clamped_settle {S : Type} (app : App S) (cfg : Config) (st : S)
(pointer : Option Point) (ui0 : UI) (fuel : Nat) (ui : UI) (s : State S)
(h : (s.ui, s.laid) = settle app cfg st pointer ui0 fuel ui) : Clamped s.laid s.ui
clamped_settleAll {S : Type} (app : App S) (cfg : Config) (st : S)
(pointer : Option Point) (ui0 ui : UI) (s : State S)
(h : (s.ui, s.laid) = settleAll app cfg st pointer ui0 ui) : Clamped s.laid s.ui
clamped_lay {S : Type} (app : App S) (cfg : Config) (st : S)
(pointer : Option Point) (goals : List (ControlRef × ScrollTarget)) (ui1 : UI)
(s : State S) (h : (s.ui, s.laid) = lay app cfg st pointer goals ui1) :
Clamped s.laid s.ui
start_clamped {S : Type} (app : App S) (cfg : Config) (size : Size)
(scale : Nat) : Clamped (start app cfg size scale).laid (start app cfg size scale).uiOffsets are clamped at start.
step_clamped {S : Type} (app : App S) (cfg : Config) (s : State S) (e : Event)
(h : Clamped s.laid s.ui) : Clamped (step app cfg s e).fst.laid (step app cfg s e).fst.uiOffsets are clamped after every step: each offset the runtime keeps belongs to a scroll
box on screen and lies within [0, max 0 (content − viewport)] of it.
steps_clamped {S : Type} (app : App S) (cfg : Config) (s : State S)
(es : List Event) (h : Clamped s.laid s.ui) :
Clamped (steps app cfg s es).fst.laid (steps app cfg s es).fst.ui
route_scroll {S : Type} (m : TextMetrics) (s : State S) (p : Point)
(dx dy : Int) : route m s (Event.scroll p dx dy) = (wheel s p dx dy, [])
step_scroll {S : Type} (app : App S) (cfg : Config) (s : State S) (p : Point)
(dx dy : Int) :
(step app cfg s (Event.scroll p dx dy)).fst.app = s.app ∧
(step app cfg s (Event.scroll p dx dy)).fst.world = s.world ∧
(step app cfg s (Event.scroll p dx dy)).snd = []A scroll changes no app state: a wheel or trackpad event leaves the app's state and the
world as they were and issues no effects (so no request, no timer, and no appear move: those
come only from Event.frame).
revealOff_shows (sc : Scroller) (cur : Int) (q : Rect) (hcur : 0 ≤ cur ∧ cur ≤ sc.limit) (hfit : mainLen sc.horiz q ≤ sc.viewport) (hin : 0 ≤ cur + (mainStart sc.horiz q - mainStart sc.horiz sc.rect) ∧ cur + (mainStart sc.horiz q - mainStart sc.horiz sc.rect) + mainLen sc.horiz q ≤ sc.content) : 0 ≤ mainStart sc.horiz q - mainStart sc.horiz sc.rect - (revealOff sc cur q - cur) ∧ mainStart sc.horiz q - mainStart sc.horiz sc.rect - (revealOff sc cur q - cur) + mainLen sc.horiz q ≤ sc.viewport
scrollOf_setScroll (ui : UI) (r : ControlRef) (o : Int) : (ui.setScroll r o).scrollOf r = o
aimOff_start {laid : Laid} {ui : UI} {r : ControlRef} {sc : Scroller}
(h : List.find? (fun sc => decide (sc.ref = r)) (scrollersOf laid) = some sc) :
aimOff laid ui r ScrollTarget.start = some 0start lands at 0, for a box on screen.
aimOff_finish {laid : Laid} {ui : UI} {r : ControlRef} {sc : Scroller}
(h : List.find? (fun sc => decide (sc.ref = r)) (scrollersOf laid) = some sc) :
aimOff laid ui r ScrollTarget.finish = some sc.limitfinish lands at the box's limit, max 0 (content − viewport): the content's end at the
box's end.
aimOff_key {laid : Laid} {ui : UI} {r : ControlRef} {sc : Scroller}
{ll : LaidList} {k i : Nat}
(hs : List.find? (fun sc => decide (sc.ref = r)) (scrollersOf laid) = some sc)
(hl : List.find? (fun ll => decide (ll.ref = r)) (listsOf laid) = some ll)
(hi : Array.findIdx? (fun x => x == k) ll.info.keys = some i) :
aimOff laid ui r (ScrollTarget.key k) =
some
(clampOff ((VList.model ll.info.keys (ui.listOf r) ll.info.estimate).top i) sc.limit)key k lands at the row's top: for a virtual list on screen whose row i has key k,
the offset is the row's top in the heights the runtime knows, clamped as every offset is.
aimOff_clamped {laid : Laid} {ui : UI} {r : ControlRef} {t : ScrollTarget}
{o : Int} (h : aimOff laid ui r t = some o) :
∃ sc, sc ∈ scrollersOf laid ∧ sc.ref = r ∧ 0 ≤ o ∧ o ≤ max 0 (sc.content - sc.viewport)Clamped as every offset is: an aimed offset lies in [0, max 0 (content − viewport)] of
the box it names.
aimScroll_single (laid : Laid) (ui : UI) (r : ControlRef) (t : ScrollTarget) {o : Int} (h : aimOff laid ui r t = some o) : (aimScroll [(r, t)] laid ui).scrollOf r = o
A request for a box on screen sets its offset to the aimed one (the last request wins).
firstF_top (M : VList.Model) (hM : M.Good) (hpos : ∀ (j : Nat), 1 ≤ M.height j) {i : Nat} (hi : i < M.count) : M.firstF M.pre (M.top i) = i
The key's row is the one at the top. Laid at the top of row i (in a model whose rows
are at least a point tall), the first row showing is row i: so scrollTo a key, unclamped,
lays that row first, and it is the row the runtime then keeps still (VList.keepRow,
VList.record_keeps).
find?_clampScroll_none (scs : List Scroller) (offs : List (ControlRef × Int)) {r : ControlRef} (h : onScreen scs r = false) : List.find? (fun x => x.fst == r) (clampScroll scs offs) = none
find?_filter_of {α : Type} (l : List α) (p q : α → Bool)
(h : ∀ (a : α), q a = true → p a = true) : List.find? q (List.filter p l) = List.find? q l
find?_keepOff {α : Type} (on : ControlRef → Bool) (keep : List ControlRef)
(now old : List (ControlRef × α)) {r : ControlRef} (hk : r ∈ keep) (ho : on r = false) :
List.find? (fun x => x.fst == r) (keepOff on keep now old) =
(List.find? (fun x => x.fst == r) now).or (List.find? (fun x => x.fst == r) old)
fixUI_keeps_offset (laid : Laid) (pointer : Option Point) (ui : UI) (keep : List ControlRef) {r : ControlRef} (hk : r ∈ keep) (hs : onScreen (scrollersOf laid) r = false) : (fixUI laid pointer ui keep).scrollOf r = ui.scrollOf r
A box the app keeps keeps its offset while it is not on screen: the offset the view
reads for it (UI.scrollOf) is the one it had before the repair.
fixUI_keeps_list (laid : Laid) (pointer : Option Point) (ui : UI) (keep : List ControlRef) {r : ControlRef} (hk : r ∈ keep) (hs : ((recordLists laid).any fun x => decide (x.fst = r)) = false) : (fixUI laid pointer ui keep).listOf r = ui.listOf r
A list the app keeps keeps what the runtime knew of it while it is not on screen: its
heights, estimate and anchor, as the view reads them (UI.listOf).
find?_setOff (offs : List (ControlRef × Int)) {r r' : ControlRef} (o : Int) (h : r' ≠ r) : List.find? (fun x => x.fst == r) (setOff offs r' o) = List.find? (fun x => x.fst == r) offs
find?_foldl_setOff (recs : List (ControlRef × VList.Known × Int)) {r : ControlRef} (h : ∀ (x : ControlRef × VList.Known × Int), x ∈ recs → x.fst ≠ r) (offs : List (ControlRef × Int)) : List.find? (fun x => x.fst == r) (List.foldl (fun offs x => setOff offs x.fst x.snd.snd) offs recs) = List.find? (fun x => x.fst == r) offs
find?_clampScroll (scs : List Scroller) {r : ControlRef} {sc : Scroller} (hs : List.find? (fun sc => decide (sc.ref = r)) scs = some sc) (offs : List (ControlRef × Int)) : List.find? (fun x => x.fst == r) (clampScroll scs offs) = Option.map (fun e => (e.fst, clampOff e.snd sc.limit)) (List.find? (fun x => x.fst == r) offs)
fixUI_revives (laid : Laid) (pointer : Option Point) (ui : UI) (keep : List ControlRef) {r : ControlRef} {sc : Scroller} {o : Int} (hs : List.find? (fun sc => decide (sc.ref = r)) (scrollersOf laid) = some sc) (hl : ((recordLists laid).any fun x => decide (x.fst = r)) = false) (hn : List.find? (fun x => x.fst == r) ui.scroll = none) (hk : List.find? (fun x => x.fst == r) ui.kept = some (r, o)) : (fixUI laid pointer ui keep).scrollOf r = clampOff o sc.limit
A kept box comes back where it was: a box back on screen with no offset of its own
resumes its kept offset, clamped to its content as every offset is. (A virtual list's is first
corrected by its record, VList.record, from what was kept of it, fixUI_keeps_list; this is
the box that is no virtual list.)
route_frame {S : Type} (m : TextMetrics) (s : State S) :
route m s Event.frame =
({ app := s.app, ui := s.ui, clicks := s.clicks, pointer := s.pointer, scale := s.scale,
laid := s.laid, effects := s.effects, world := s.world, subCmds := s.subCmds,
surfaces := s.surfaces, seen := appearRefs s.laid },
appearing s.laid s.seen)
leave_noAppear {S : Type} (s : State S) (n : Option ControlRef)
(c : ControlRef) : ¬Action.appear c ∈ leave s n
onField_noAppear {S : Type} (s : State S) (ops : Target → List TextOp)
(c : ControlRef) : ¬Action.appear c ∈ onField s ops
keyActions_noAppear {S : Type} (s : State S) (k : Key) (mods : Mods)
(c : ControlRef) : ¬Action.appear c ∈ keyActions s k mods
textActions_noAppear {S : Type} (s : State S) (str : String)
(rep : Option (Nat × Nat)) (c : ControlRef) : ¬Action.appear c ∈ textActions s str rep
keyRoute_noAppear {S : Type} (s : State S) (k : Key) (mods : Mods)
(c : ControlRef) : ¬Action.appear c ∈ (keyRoute s k mods).snd
textRoute_noAppear {S : Type} (s : State S) (str : String)
(rep : Option (Nat × Nat)) (c : ControlRef) : ¬Action.appear c ∈ (textRoute s str rep).snd
keyScrollState_seen {S : Type} (s : State S) (k : Key) (mods : Mods) :
(keyScrollState s k mods).seen = s.seen
secondaryDown_seen {S : Type} (s : State S) (p : Point) :
(secondaryDown s p).seen = s.seen
keyRoute_seen {S : Type} (s : State S) (k : Key) (mods : Mods) :
(keyRoute s k mods).fst.seen = s.seen
textRoute_seen {S : Type} (s : State S) (str : String)
(rep : Option (Nat × Nat)) : (textRoute s str rep).fst.seen = s.seen
tab_noAppear {S : Type} (s : State S) (back : Bool) (c : ControlRef) :
¬Action.appear c ∈ (tab s back).snd
route_appear {S : Type} (m : TextMetrics) (s : State S) (e : Event)
(c : ControlRef) (h : Action.appear c ∈ (route m s e).snd) :
e = Event.frame ∨ ∃ p e', e = Event.surface p e'Only the frame event routes appear moves (a window surface's events are routed as the window's own, and a frame event is never sent by the host).
route_seen {S : Type} (m : TextMetrics) (s : State S) (e : Event)
(h : e ≠ Event.frame) : (route m s e).fst.seen = s.seenOnly the frame event changes what was seen.
step_seen {S : Type} (app : App S) (cfg : Config) (s : State S) (e : Event) :
(step app cfg s e).fst.seen = (route cfg.metrics s e).fst.seenA step keeps what routing made of seen.
step_frame_seen {S : Type} (app : App S) (cfg : Config) (s : State S) :
(step app cfg s Event.frame).fst.seen = appearRefs s.laidAfter a frame event, seen is the appear-marked controls on screen at that frame; no other
event changes it.
step_seen_other {S : Type} (app : App S) (cfg : Config) (s : State S)
(e : Event) (h : e ≠ Event.frame) : (step app cfg s e).fst.seen = s.seen
appear_iff {S : Type} (m : TextMetrics) (s : State S) (c : ControlRef) :
Action.appear c ∈ (route m s Event.frame).snd ↔
(∃ t, t ∈ targets s.laid ∧ t.control.appear = true ∧ t.visible.nonempty ∧ t.ref = c) ∧
¬c ∈ s.seenAppear, exactly. A frame delivers appear c exactly when c is a control marked
Control.appear with a visible part on screen now, and was not one at the last frame. (A
control is on screen only while its move is enabled, by the app's presence claims, so "visible
and enabled".)
step_frame_delivers {S : Type} (app : App S) (cfg : Config) (s : State S)
(hh : s.world.heard = some s.world.clock) :
(step app cfg s Event.frame).fst.app =
(deliver app.update s.app (appearing s.laid s.seen)).fstThe app hears a frame's appear moves through update, in paint order, like any other
action (when it has heard the current time, as after any input).