Cairn.Runtime.Proofs
lean/Cairn/Runtime/Proofs.lean
Theorems about the runtime: actions name controls on screen, interaction state stays sound, and a click at a reachable control presses it.
Imports Cairn.Runtime.Step
Definitions 7
Sound {S : Type} (s : State S) : PropFocus is a focusable control of the tree on screen; hover and press are controls of it.
Names (laid : Laid) (acts : List Action) : Prop
Every action names a control of laid.
Untouched {S : Type} (a0 : S) (c : Ctx S) : PropNothing delivered means the app state is the one it started from.
Quiet {S : Type} (app : App S) : PropAn app that ignores the world: receive never changes its state (the default, and every M1
app's).
feed {S : Type} (app : App S) (st : S) : Action ⊕ Msg → SOne input to an app: an action to update or a message to receive.
Fed {S : Type} (app : App S) (a b : S) : Propb is a after some actions and messages.
Kept {S : Type} (a : S) (c : Ctx S) : PropA context that delivered nothing still holds the app state a.
Theorems 111
tab_fst {S : Type} (s : State S) (back : Bool) :
(tab s back).fst.laid = s.laid ∧ (tab s back).fst.app = s.app
wheel_eq {S : Type} (s : State S) (p : Point) (dx dy : Int) :
∃ ui,
wheel s p dx dy =
{ app := s.app, ui := 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 := s.seen }Scrolling changes only the UI.
keyScrollState_eq {S : Type} (s : State S) (k : Key) (mods : Mods) :
∃ ui,
keyScrollState s k mods =
{ app := s.app, ui := 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 := s.seen }
wheel_fst {S : Type} (s : State S) (p : Point) (dx dy : Int) :
(wheel s p dx dy).laid = s.laid ∧
(wheel s p dx dy).app = s.app ∧ (wheel s p dx dy).surfaces = s.surfaces
keyScrollState_fst {S : Type} (s : State S) (k : Key) (mods : Mods) :
(keyScrollState s k mods).laid = s.laid ∧
(keyScrollState s k mods).app = s.app ∧ (keyScrollState s k mods).surfaces = s.surfaces
openAt_fst {S : Type} (s : State S) (r : ControlRef) :
(openAt s r).laid = s.laid ∧ (openAt s r).app = s.app ∧ (openAt s r).surfaces = s.surfaces
secondaryDown_fst {S : Type} (s : State S) (p : Point) :
(secondaryDown s p).laid = s.laid ∧
(secondaryDown s p).app = s.app ∧ (secondaryDown s p).surfaces = s.surfaces
keyRoute_fst {S : Type} (s : State S) (k : Key) (mods : Mods) :
(keyRoute s k mods).fst.laid = s.laid ∧
(keyRoute s k mods).fst.app = s.app ∧ (keyRoute s k mods).fst.surfaces = s.surfaces
textRoute_fst {S : Type} (s : State S) (str : String)
(rep : Option (Nat × Nat)) :
(textRoute s str rep).fst.laid = s.laid ∧
(textRoute s str rep).fst.app = s.app ∧ (textRoute s str rep).fst.surfaces = s.surfaces
route_laid {S : Type} (m : TextMetrics) (s : State S) (e : Event) :
(route m s e).fst.laid = s.laid ∧ (route m s e).fst.app = s.app
fixUI_sound (laid : Laid) (pointer : Option Point) (ui : UI) (keep : List ControlRef) : (∀ (r : ControlRef), (fixUI laid pointer ui keep).focus = some r → ∃ t, t ∈ targets laid ∧ t.ref = r ∧ t.focusable = true) ∧ (∀ (r : ControlRef), (fixUI laid pointer ui keep).hover = some r → r ∈ refs laid) ∧ ∀ (r : ControlRef), (fixUI laid pointer ui keep).pressed = some r → r ∈ refs laid
settle_spec {S : Type} (app : App S) (cfg : Config) (st : S)
(pointer : Option Point) (ui0 : UI) (fuel : Nat) (ui : UI) :
∃ l, settle app cfg st pointer ui0 fuel ui = (fixUI l pointer ui0 (app.keepScroll st), l)settle always returns ui0 repaired against the tree it returns.
resettle_spec {S : Type} (app : App S) (cfg : Config) (st : S)
(pointer : Option Point) (ui0 : UI) (fuel : Nat) (x : UI × Laid) :
(∃ l, x = (fixUI l pointer ui0 (app.keepScroll st), l)) →
∃ l,
resettle app cfg st pointer ui0 fuel x = (fixUI l pointer ui0 (app.keepScroll st), l)
settleAll_spec {S : Type} (app : App S) (cfg : Config) (st : S)
(pointer : Option Point) (ui0 ui : UI) :
∃ l, settleAll app cfg st pointer ui0 ui = (fixUI l pointer ui0 (app.keepScroll st), l)settleAll always returns ui0 repaired against the tree it returns.
repeat_comm {α : Type} (f : α → α) (n : Nat) (a : α) :
Nat.repeat f n (f a) = f (Nat.repeat f n a)
resettle_stops {S : Type} (app : App S) (cfg : Config) (st : S)
(pointer : Option Point) (ui0 : UI) (fuel : Nat) (x : UI × Laid) :
unsettled (resettle app cfg st pointer ui0 fuel x).snd = false ∨
resettle app cfg st pointer ui0 fuel x =
Nat.repeat (fun y => settle app cfg st pointer ui0 0 y.fst) fuel x
aim_spec {S : Type} (app : App S) (cfg : Config) (st : S)
(pointer : Option Point) (ui1 : UI) (goals : List (ControlRef × ScrollTarget))
(fuel : Nat) (x : UI × Laid) :
(∃ l u,
x = (fixUI l pointer u (app.keepScroll st), l) ∧
u.focus = ui1.focus ∧ u.pressed = ui1.pressed) →
∃ l u,
aim app cfg st pointer ui1 goals fuel x = (fixUI l pointer u (app.keepScroll st), l) ∧
u.focus = ui1.focus ∧ u.pressed = ui1.pressed
lay_spec {S : Type} (app : App S) (cfg : Config) (st : S)
(pointer : Option Point) (goals : List (ControlRef × ScrollTarget)) (ui1 : UI) :
∃ l u,
lay app cfg st pointer goals ui1 = (fixUI l pointer u (app.keepScroll st), l) ∧
u.focus = ui1.focus ∧ u.pressed = ui1.pressed
sound_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) : Sound s
sound_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) : Sound s
sound_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) : Sound s
start_sound {S : Type} (app : App S) (cfg : Config) (size : Size)
(scale : Nat) : Sound (start app cfg size scale)Focus is sound at start.
step_sound {S : Type} (app : App S) (cfg : Config) (s : State S) (e : Event)
(h : Sound s) : Sound (step app cfg s e).fstFocus is sound after every step: focus is none or a focusable control of the tree on screen, and hover and press are none or controls of it.
steps_sound {S : Type} (app : App S) (cfg : Config) (s : State S)
(es : List Event) (h : Sound s) : Sound (steps app cfg s es).fst
names_nil (laid : Laid) : Names laid []
names_append {laid : Laid} {a b : List Action} (ha : Names laid a)
(hb : Names laid b) : Names laid (a ++ b)
names_of {laid : Laid} {t : Target} (ht : t ∈ targets laid)
{acts : List Action} (h : ∀ (a : Action), a ∈ acts → a.control = t.ref) : Names laid actsActions all about one control of the tree.
focused_mem {S : Type} {s : State S} {t : Target} (h : focused s = some t) :
t ∈ targets s.laid
leave_names {S : Type} (s : State S) (n : Option ControlRef) :
Names s.laid (leave s n)
leave_blurs {S : Type} (s : State S) (n : Option ControlRef) (a : Action) :
a ∈ leave s n → ∃ c, a = Action.blur c
onField_names {S : Type} (s : State S) (ops : Target → List TextOp) :
Names s.laid (onField s ops)
keyActions_names {S : Type} (s : State S) (k : Key) (mods : Mods) :
Names s.laid (keyActions s k mods)
textActions_names {S : Type} (s : State S) (str : String)
(rep : Option (Nat × Nat)) : Names s.laid (textActions s str rep)
keyRoute_names {S : Type} (s : State S) (k : Key) (mods : Mods) :
Names s.laid (keyRoute s k mods).snd
textRoute_names {S : Type} (s : State S) (str : String)
(rep : Option (Nat × Nat)) : Names s.laid (textRoute s str rep).snd
tabTarget_mem {S : Type} (s : State S) (back : Bool) {t : Target}
(h : tabTarget s back = some t) : t ∈ targets s.laid
mem_appearRefs {laid : Laid} {r : ControlRef} :
r ∈ appearRefs laid ↔
∃ t, t ∈ targets laid ∧ t.control.appear = true ∧ t.visible.nonempty ∧ t.ref = r
mem_appearing {laid : Laid} {seen : List ControlRef} {a : Action} :
a ∈ appearing laid seen ↔
∃ c,
a = Action.appear c ∧
¬c ∈ seen ∧
∃ t, t ∈ targets laid ∧ t.control.appear = true ∧ t.visible.nonempty ∧ t.ref = cAppear, exactly. The frame event delivers appear c exactly when c is a control of the
tree on screen marked appear with a visible part, and isn't among the controls seen at the last
frame.
appearing_names (laid : Laid) (seen : List ControlRef) : Names laid (appearing laid seen)
tab_names {S : Type} (s : State S) (back : Bool) :
Names s.laid (tab s back).snd
route_names {S : Type} (m : TextMetrics) (s : State S) (e : Event)
(hm : e.isMenu = false) : Names s.laid (route m s e).sndNo action without a control. Every action the runtime passes to update names a
control of the laid tree on screen when the event arrived, unless the event is a menu event
(those name the menu's items: menu_route_names). (step delivers exactly
(route cfg.metrics s e).2.)
release_app {S : Type} (c : Ctx S) (w : World) : (release c w).app = c.app
release_delivered {S : Type} (c : Ctx S) (w : World) :
(release c w).delivered = c.delivered
ack_app {S : Type} (c : Ctx S) (id : Nat) : (ack c id).app = c.app
ack_delivered {S : Type} (c : Ctx S) (id : Nat) :
(ack c id).delivered = c.delivered
give_untouched {S : Type} (app : App S) (a0 : S) (c : Ctx S) (m : Msg) :
Untouched a0 (give app c m)
hear_untouched {S : Type} (app : App S) {a0 : S} {c : Ctx S}
(h : Untouched a0 c) : Untouched a0 (hear app c)
fire_untouched {S : Type} (app : App S) {a0 : S} {c : Ctx S} (n : String)
(h : Untouched a0 c) : Untouched a0 (fire app c n)
foldl_fire_untouched {S : Type} (app : App S) {a0 : S} (ns : List String)
{c : Ctx S} : Untouched a0 c → Untouched a0 (List.foldl (fire app) c ns)
boot_untouched {S : Type} (app : App S) {a0 : S} {c : Ctx S}
(h : Untouched a0 c) : Untouched a0 (boot app c)
admit_untouched {S : Type} (app : App S) (s : State S) (e : Event) :
Untouched s.app (admit app s e)
admit_input {S : Type} (app : App S) (s : State S) {e : Event}
(h : e.isWorld = false) : admit app s e = { app := s.app, world := s.world }
step_app {S : Type} (app : App S) (cfg : Config) (s : State S) (e : Event) :
(step app cfg s e).fst.app = (act app (admit app s e) (route cfg.metrics s e).snd).app
step_delivers {S : Type} (app : App S) (cfg : Config) (s : State S)
(e : Event) (hw : e.isWorld = false) (hh : s.world.heard = some s.world.clock) :
(step app cfg s e).fst.app = (deliver app.update s.app (route cfg.metrics s e).snd).fstFor input events (not from the world), when the app has heard the current time, the app
state after a step is update folded over exactly the routed actions: M1's statement.
give_app {S : Type} {app : App S} (h : Quiet app) (c : Ctx S) (m : Msg) :
(give app c m).app = c.app
hear_app {S : Type} {app : App S} (h : Quiet app) (c : Ctx S) :
(hear app c).app = c.app
fire_app {S : Type} {app : App S} (h : Quiet app) (c : Ctx S) (n : String) :
(fire app c n).app = c.app
foldl_fire_app {S : Type} {app : App S} (h : Quiet app) (ns : List String)
(c : Ctx S) : (List.foldl (fire app) c ns).app = c.app
boot_app {S : Type} {app : App S} (h : Quiet app) (c : Ctx S) :
(boot app c).app = c.app
admit_app {S : Type} {app : App S} (h : Quiet app) (s : State S) (e : Event) :
(admit app s e).app = s.app
act_app {S : Type} {app : App S} (h : Quiet app) (c : Ctx S)
(acts : List Action) : (act app c acts).app = (deliver app.update c.app acts).fst
refl {S : Type} (app : App S) (a : S) : Fed app a a
trans {S : Type} {app : App S} {a b c : S} (h1 : Fed app a b)
(h2 : Fed app b c) : Fed app a c
give_fed {S : Type} (app : App S) (c : Ctx S) (m : Msg) :
Fed app c.app (give app c m).app
hear_fed {S : Type} (app : App S) (c : Ctx S) : Fed app c.app (hear app c).app
fire_fed {S : Type} (app : App S) (c : Ctx S) (n : String) :
Fed app c.app (fire app c n).app
foldl_fire_fed {S : Type} (app : App S) (ns : List String) (c : Ctx S) :
Fed app c.app (List.foldl (fire app) c ns).app
boot_fed {S : Type} (app : App S) (c : Ctx S) : Fed app c.app (boot app c).app
admit_fed {S : Type} (app : App S) (s : State S) (e : Event) :
Fed app s.app (admit app s e).app
deliver_fed {S : Type} (u : S → Action → S × List Effect) (acts : List Action)
(st : S) (effs : List Effect) :
(List.foldl
(fun p a =>
match u p.fst a with
| (st', e) => (st', p.snd ++ e))
(st, effs) acts).fst =
List.foldl (fun s a => (u s a).fst) st acts
foldl_feed_inl {S : Type} (app : App S) (acts : List Action) (st : S) :
List.foldl (fun s a => (app.update s a).fst) st acts =
List.foldl (feed app) st (List.map Sum.inl acts)
act_fed {S : Type} (app : App S) (c : Ctx S) (acts : List Action) :
Fed app c.app (act app c acts).app
step_fed {S : Type} (app : App S) (cfg : Config) (s : State S) (e : Event) :
Fed app s.app (step app cfg s e).fst.appAny app. The app state after a step is the one before after some updates and messages (the routed actions, the clock, due timers, a reply or a subscription event).
step_delivers_quiet {S : Type} {app : App S} (h : Quiet app) (cfg : Config)
(s : State S) (e : Event) :
(step app cfg s e).fst.app = (deliver app.update s.app (route cfg.metrics s e).snd).fstFor an app that ignores the world, the app state after any step is update folded over
exactly the routed actions.
applyFocus_pressed (effs : List Effect) (ui : UI) : (applyFocus effs ui).pressed = ui.pressed
A focus request changes only the focus.
step_down_pressed {S : Type} (app : App S) (cfg : Config) (s : State S)
(t : Target) (p : Point) (clicks : Nat) (mods : Mods) (hhit : hitTarget s.laid p = some t)
(hf : t.isField = false) (hb : t.menuButton = false)
(hpres :
t.ref ∈
refs (step app cfg s (Event.pointerDown p Button.primary clicks mods)).fst.laid) :
(step app cfg s (Event.pointerDown p Button.primary clicks mods)).fst.ui.pressed =
some t.ref ∧
(step app cfg s (Event.pointerDown p Button.primary clicks mods)).fst.clicks = clicksAfter a pointerDown on a non-field control t, the press is recorded on t with the
down's click count, whatever the update and relayout did, provided t's ref is still in the
new tree.
down_actions {S : Type} (m : TextMetrics) (s : State S) (t : Target)
(p : Point) (clicks : Nat) (mods : Mods) (hhit : hitTarget s.laid p = some t)
(hf : t.isField = false) (hb : t.menuButton = false) :
(route m s (Event.pointerDown p Button.primary clicks mods)).snd = leave s noneThe actions of a pointerDown on a non-field control that isn't a menu button: at most a blur of the field that loses focus. No press happens on the way down.
click_presses {S : Type} (app : App S) (cfg : Config) (s : State S)
(t : Target) (p : Point) (mods mods' : Mods) (h0 : Reaches s.laid t p)
(hf : t.isField = false) (hb : t.menuButton = false)
(h1 :
∃ t1,
Reaches (step app cfg s (Event.pointerDown p Button.primary 1 mods)).fst.laid t1 p ∧
t1.ref = t.ref ∧ t1.isField = false) :
(∀ (a : Action),
a ∈ (route cfg.metrics s (Event.pointerDown p Button.primary 1 mods)).snd →
∃ c, a = Action.blur c) ∧
(route cfg.metrics (step app cfg s (Event.pointerDown p Button.primary 1 mods)).fst
(Event.pointerUp p Button.primary mods')).snd =
[Action.press t.ref]Pressable, step level. If a pointer at p reaches non-field control t that isn't a
menu button (a menu button's click opens its menu instead), and after
the pointerDown (and whatever update and relayout it caused) p still reaches a non-field
control with the same ref, then the pointerUp at p delivers exactly press t.ref, and the
pointerDown delivered nothing but blurs.
click_center_presses {S : Type} (app : App S) (cfg : Config) (s : State S)
(t : Target) (mods mods' : Mods) (h0 : LayoutFacts s.laid t) (hf : t.isField = false)
(hb : t.menuButton = false)
(h1 :
∃ t1,
Reaches
(step app cfg s
(Event.pointerDown t.visible.center Button.primary 1 mods)).fst.laid
t1 t.visible.center ∧
t1.ref = t.ref ∧ t1.isField = false) :
(∀ (a : Action),
a ∈
(route cfg.metrics s
(Event.pointerDown t.visible.center Button.primary 1 mods)).snd →
∃ c, a = Action.blur c) ∧
(route cfg.metrics
(step app cfg s (Event.pointerDown t.visible.center Button.primary 1 mods)).fst
(Event.pointerUp t.visible.center Button.primary mods')).snd =
[Action.press t.ref]Pressable at the centre: under LayoutFacts, a click at the centre of the control's
visible rect presses it.
selectMenu_window {S : Type} {s : State S} {p : ClaimId}
(h : Shown.windowPlace s.surfaces = some p) :
selectMenu s p = Option.map (fun x => x.snd.items) (openMenu s)For the window's place, a selection is checked against the control menu open now.
same_self (a : UI) : same a a = true
secondary_opens {S : Type} (m : TextMetrics) (s : State S) {p : Point}
{t : Target} (clicks : Nat) (mods : Mods) (h : menuTarget s.laid p = some t) :
route m s (Event.pointerDown p Button.secondary clicks mods) =
(openAt (withPointer s p) t.ref, [])A secondary click on a control with a menu (or inside one) opens that menu and delivers nothing.
route_open_quiet {S : Type} (m : TextMetrics) (s : State S) (e : Event)
{r : ControlRef} (h : (route m s e).fst.ui.menu = some r) (hne : s.ui.menu ≠ some r) :
(route m s e).snd = []Opening a menu reaches no update. Whenever routing an event opens a control menu (the menu open after it is one that wasn't open before: a secondary click, a menu button's primary click, Space or Return on a focused menu button, the context-menu key), it delivers no action.
step_open_quiet {S : Type} (app : App S) (cfg : Config) (s : State S)
(e : Event) {r : ControlRef} (h : (route cfg.metrics s e).fst.ui.menu = some r)
(hne : s.ui.menu ≠ some r) (hw : e.isWorld = false) :
(step app cfg s e).fst.app = s.app ∧ (step app cfg s e).snd = []Opening a menu changes no app state. A step whose routing opens a control menu (for
instance a secondary click on a control with a menu, secondary_opens) leaves the app state as
it was and asks the host for nothing; only choosing an item (menuSelect) reaches update.
route_surface_other {S : Type} (m : TextMetrics) (s : State S) {p : ClaimId}
(e : Event) (h : Shown.windowPlace s.surfaces ≠ some p) :
route m s (Event.surface p e) = (s, [])Events addressed to a surface other than the window (a panel, a status item) do nothing.
tab_surfaces {S : Type} (s : State S) (back : Bool) :
(tab s back).fst.surfaces = s.surfaces
route_surfaces {S : Type} (m : TextMetrics) (s : State S) (e : Event) :
(route m s e).fst.surfaces = s.surfaces
give_kept {S : Type} (app : App S) (a : S) (c : Ctx S) (m : Msg) :
Kept a (give app c m)
hear_kept {S : Type} (app : App S) (a : S) (c : Ctx S) (h : Kept a c) :
Kept a (hear app c)
fire_kept {S : Type} (app : App S) (a : S) (c : Ctx S) (n : String)
(h : Kept a c) : Kept a (fire app c n)
boot_kept {S : Type} (app : App S) (a : S) (c : Ctx S) (h : Kept a c) :
Kept a (boot app c)
foldl_fire_kept {S : Type} (app : App S) (a : S) (ns : List String)
(c : Ctx S) : Kept a c → Kept a (List.foldl (fire app) c ns)
admit_kept {S : Type} (app : App S) (s : State S) (e : Event) :
Kept s.app (admit app s e)admit changes the app state only by delivering something.
step_surfaces {S : Type} (app : App S) (cfg : Config) (s : State S)
(e : Event) (h : s.surfaces = shows app cfg s.app) :
(step app cfg s e).fst.surfaces = shows app cfg (step app cfg s e).fst.appEach step keeps the runtime's surfaces equal to what the app's surfaces show for its state:
the menu menuSelect is checked against is the menu of the current app state.
start_surfaces {S : Type} (app : App S) (cfg : Config) (size : Size)
(scale : Nat) :
(start app cfg size scale).surfaces = shows app cfg (start app cfg size scale).app
steps_surfaces {S : Type} (app : App S) (cfg : Config) (es : List Event)
(s : State S) :
s.surfaces = shows app cfg s.app →
(steps app cfg s es).fst.surfaces = shows app cfg (steps app cfg s es).fst.appIn every state the running app reaches, the surfaces show the current app state.
Routing leaves the app and the tree alone
Interaction state is sound
No action without a control
Releasing a slot touches neither the app nor what was delivered
Any app: a step is a sequence of updates and messages
Pressable
Menus (docs/surfaces.md, section 1, "Menus on controls" and "The app's menus")
A menu is a description, not a laid tree. A selection is checked against selectMenu: for the
window's place, the control menu open now (openMenu: UI.menu's control's menu in the tree
on screen); for another place, a status item's menu or the menu bar's items, which step
refreshes whenever something is delivered (step_surfaces).