Cairn.Runtime.WorldProofs
lean/Cairn/Runtime/WorldProofs.lean
What the runtime guarantees about the outside world (docs/effects.md, "Semantics").
- The clock never goes back (
step_clock). - A timer reaches
receiveonly while it is set: a cancelled timer never fires, and a timer fires once per setting (steps_book, read withBook.run). - A reply reaches
receiveonly for a pending request, with the id it was sent under, in the shape that answers its kind, and once (steps_book,step_reply,step_reply_ignored). - Subscription diffs start exactly the wanted subscriptions that are not running, stop exactly
the running ones no longer wanted, and the active set becomes what the app wants
(
diffSubs_stop,diffSubs_start,diffSubs_active).
The timer and reply statements are about a recording wrapper, logged app, whose state carries
the list of everything delivered to receive and update, with the effects each returned.
Book.run is the specification such a log must meet: it replays the log against a book of
armed timers and pending requests and fails at the first delivery the book does not allow.
Imports Cairn.Runtime.Proofs
Structures 1
Book : Type
The specification's state: which timers are armed and which requests are pending.
armed : Boolpending : Option Request.Kind
Inductive types 1
Entry : Type
What a delivery log records: a message to receive or an action to update, with the
effects it returned.
Definitions 18
Same (w w' : World) : Prop
Absorbing effects touches only timers and requests.
arm (b : Book) (n : String) (on : Bool) : Book
drop (b : Book) (id : Nat) : Book
take (b : Book) : Effect → Book
One effect: setTimer arms, cancelTimer disarms, a request with a fresh id becomes
pending (one whose id is pending is refused), cancelRequest withdraws a pending request. Whether
a request is sent at once or waits for a slot is the runtime's business, not the book's: the
book's pending requests are the ones the app may still hear about.
takeAll (b : Book) (es : List Effect) : Book
admits (b : Book) : Msg → Bool
Which messages may be delivered: a timer only while armed, a reply only to a pending request and in the shape that answers it.
pre (b : Book) : Msg → Book
Delivering a message uses it up: a fired timer is disarmed, an answered request is no longer pending.
run (b : Book) : List Entry → Option Book
Replay a log; none at the first delivery the book does not allow.
Keys (w : World) : Prop
No id is both pending and queued, or twice in either.
wkind (p : Nat × Request) : Nat × Request.Kind
How a queued request shows in entries.
Agrees (w : World) (b : Book) : Prop
The runtime's tables and a book agree: the same timers armed, and the requests the app may still hear about (pending or queued) the same, each id once.
qkind (q : Nat × Nat × Request) : Nat × Request.Kind
How a queued request shows in entries.
logUpdate {S : Type} (app : App S) (st : S × List Entry) (a : Action) :
(S × List Entry) × List Effect
logReceive {S : Type} (app : App S) (st : S × List Entry) (m : Msg) :
(S × List Entry) × List Effect
logged {S : Type} (app : App S) : App (S × List Entry)app, with a log of every delivery in its state. It behaves as app does: every field
reads only the first component.
Inv {S : Type} (log0 : List Entry) (b0 : Book) (c : Ctx (S × List Entry)) :
PropA context whose log extends log0 by entries the book b0 allows, ending at a book that
agrees with the context's world.
Grows (w w' : World) : Prop
The clock does not go back and a booted world stays booted.
KeepsOnClock {S : Type} (app : App S) (id : Nat) : PropThe app does not withdraw request id when it hears the time.
Theorems 102
lookup_append {β : Type} (l m : List (Nat × β)) (x : Nat) :
List.lookup x (l ++ m) = (List.lookup x l).or (List.lookup x m)
lookup_filter {β : Type} (l : List (Nat × β)) (id x : Nat) :
List.lookup x (List.filter (fun p => p.fst != id) l) =
if x = id then none else List.lookup x l
any_eq_lookup {β : Type} (l : List (Nat × β)) (id : Nat) :
(l.any fun p => p.fst == id) = (List.lookup id l).isSome
trans {a b c : World} (h1 : Same a b) (h2 : Same b c) : Same a c
cancel_same (w : World) (id : Nat) : Same w (w.cancel id).fst
absorb1_same (w : World) (e : Effect) : Same w (w.absorb1 e).fst
absorb_cons (w : World) (e : Effect) (es : List Effect) : (w.absorb (e :: es)).fst = ((w.absorb1 e).fst.absorb es).fst
absorb_same (es : List Effect) (w : World) : Same w (w.absorb es).fst
run_append (xs ys : List Entry) (b : Book) : b.run (xs ++ ys) = (b.run xs).bind fun x => x.run ys
takeAll_append (b : Book) (xs ys : List Effect) : b.takeAll (xs ++ ys) = (b.takeAll xs).takeAll ys
cancel_disarms (b : Book) (n : String) (es rest : List Effect) (h : ∀ (ms : Nat), ¬Effect.setTimer n ms ∈ rest) : (b.takeAll (es ++ Effect.cancelTimer n :: rest)).armed n = false
A timer whose last word in a delivery's effects was cancelTimer is not armed after it.
cancel_blocks (b : Book) (id : Nat) (es rest : List Effect) (r : Reply) (h : ∀ (q : Request), ¬Effect.request id q ∈ rest) : (b.takeAll (es ++ Effect.cancelRequest id :: rest)).admits (Msg.reply id r) = false
A cancelled request is never answered: once cancelRequest id is the last word on id
in a delivery's effects (no request under id after it), no reply to id is admitted.
reply_once (b : Book) (id : Nat) (r r' : Reply) : (b.pre (Msg.reply id r)).admits (Msg.reply id r') = false
A reply uses up its request: right after delivery a second reply to the same id is not admitted.
lookup_some_mem {β : Type} {l : List (Nat × β)} {x : Nat} {v : β}
(h : List.lookup x l = some v) : (x, v) ∈ l
lookup_none_of {β : Type} {l : List (Nat × β)} {x : Nat}
(h : ¬x ∈ List.map (fun x => x.fst) l) : List.lookup x l = none
lookup_isSome_iff {β : Type} (l : List (Nat × β)) (x : Nat) :
(List.lookup x l).isSome = true ↔ x ∈ List.map (fun x => x.fst) l
lookup_of_mem {β : Type} {l : List (Nat × β)} {x : Nat} {v : β}
(hn : (List.map (fun x => x.fst) l).Nodup) (h : (x, v) ∈ l) : List.lookup x l = some v
lookup_congr {β : Type} {l l' : List (Nat × β)}
(hm : ∀ (p : Nat × β), p ∈ l ↔ p ∈ l') (hn : (List.map (fun x => x.fst) l).Nodup)
(hn' : (List.map (fun x => x.fst) l').Nodup) (x : Nat) :
List.lookup x l = List.lookup x l'Two keyed lists with the same members and no repeated key look up alike.
nodup_middle {α : Type} {a c : List α} {x : α} (h : (a ++ c).Nodup)
(hx : ¬x ∈ a ++ c) : (a ++ [x] ++ c).Nodup
nodup_snoc {α : Type} {a : List α} {x : α} (h : a.Nodup) (hx : ¬x ∈ a) :
(a ++ [x]).Nodup
entries_eq (w : World) : w.entries = w.pending ++ List.map wkind w.waiting
map_wkind_keys (l : List (Nat × Request)) : List.map (fun x => x.fst) (List.map wkind l) = List.map (fun x => x.fst) l
live_none {w : World} {id : Nat} (h : w.live id = none) :
List.lookup id w.pending = none ∧ List.lookup id (List.map wkind w.waiting) = none
waiting_any {w : World} {id : Nat} :
(w.waiting.any fun x => x.fst == id) = true ↔ id ∈ List.map (fun x => x.fst) w.waiting
keys_disjoint {w : World} (hk : w.Keys) {id : Nat}
(hp : id ∈ List.map (fun x => x.fst) w.pending)
(hq : id ∈ List.map (fun x => x.fst) w.waiting) : FalseAn id both pending and queued contradicts Keys.
waiting_filter (w : World) (id : Nat) : List.map (fun x => x.snd) (List.filter (fun x => x.snd.fst != id) w.queued) = List.filter (fun x => x.fst != id) w.waiting
map_wkind_filter (l : List (Nat × Request)) (id : Nat) : List.map wkind (List.filter (fun x => x.fst != id) l) = List.filter (fun x => x.fst != id) (List.map wkind l)
mem_setTimer (w : World) (n x : String) (ms : Nat) : x ∈ (w.setTimer n ms).timerNames ↔ x = n ∨ x ∈ w.timerNames
mem_cancelTimer (w : World) (n x : String) : x ∈ (w.cancelTimer n).timerNames ↔ x ≠ n ∧ x ∈ w.timerNames
send_agrees {w : World} {b : Book} (h : Agrees w b) {id : Nat}
(k : Request.Kind) (hb : b.pending id = none) :
Agrees (w.send id k)
{ armed := b.armed, pending := fun x => if x = id then some k else b.pending x }Sending a request with a fresh id.
enqueue_agrees {w : World} {b : Book} (h : Agrees w b) {id : Nat}
(r : Request) (hb : b.pending id = none) :
Agrees (w.enqueue id r)
{ armed := b.armed, pending := fun x => if x = id then some r.kind else b.pending x }Queueing a request with a fresh id.
cancel_agrees {w : World} {b : Book} (h : Agrees w b) (id : Nat) :
Agrees (w.cancel id).fst (b.drop id)
absorb1_agrees {w : World} {b : Book} (h : Agrees w b) (e : Effect) :
Agrees (w.absorb1 e).fst (b.take e)
absorb_agrees (es : List Effect) {w : World} {b : Book} : Agrees w b → Agrees (w.absorb es).fst (b.takeAll es)
takeReply_some {w w' : World} {id : Nat} {r : Reply}
(h : w.takeReply id r = some w') :
∃ k,
List.lookup id w.pending = some k ∧
Reply.answers k r = true ∧
w' =
{ clock := w.clock, heard := w.heard, booted := w.booted, timers := w.timers,
pending := List.filter (fun p => p.fst != id) w.pending, queued := w.queued,
stopping := w.stopping, cap := w.cap, nextTicket := w.nextTicket,
subs := w.subs, nextSub := w.nextSub }
entries_queued (w : World) : w.entries = w.pending ++ List.map qkind w.queued
promoteGo_spec (rest : List (Nat × Nat × Request)) (w : World) : (∃ p q, (w.promoteGo rest).fst = { clock := w.clock, heard := w.heard, booted := w.booted, timers := w.timers, pending := p, queued := q, stopping := w.stopping, cap := w.cap, nextTicket := w.nextTicket, subs := w.subs, nextSub := w.nextSub }) ∧ (w.promoteGo rest).fst.entries.Perm (w.entries ++ List.map qkind rest)
promoteGo moves the requests it is given into pending or the queue, touching nothing
else.
promote_spec (w : World) : (∃ p q, w.promote.fst = { clock := w.clock, heard := w.heard, booted := w.booted, timers := w.timers, pending := p, queued := q, stopping := w.stopping, cap := w.cap, nextTicket := w.nextTicket, subs := w.subs, nextSub := w.nextSub }) ∧ w.promote.fst.entries.Perm w.entries
agrees_entries {w w' : World} {b : Book} (ht : w'.timers = w.timers)
(hp : w'.entries.Perm w.entries) (h : Agrees w b) : Agrees w' b
promote_agrees {w : World} {b : Book} (h : Agrees w b) :
Agrees w.promote.fst b
takeStop_some {w w' : World} {id : Nat} (h : w.takeStop id = some w') :
w.isStopping id = true ∧
w' =
{ clock := w.clock, heard := w.heard, booted := w.booted, timers := w.timers,
pending := w.pending, queued := w.queued,
stopping := List.filter (fun x => x.fst != id) w.stopping, cap := w.cap,
nextTicket := w.nextTicket, subs := w.subs, nextSub := w.nextSub }
takeStop_agrees {w w' : World} {b : Book} {id : Nat} (h : Agrees w b)
(hw : w.takeStop id = some w') : Agrees w' b
takeReply_agrees {w w' : World} {b : Book} {id : Nat} {r : Reply}
(h : Agrees w b) (hw : w.takeReply id r = some w') : Agrees w' (b.drop id)
live_of_pending {w : World} {id : Nat} {k : Request.Kind}
(h : List.lookup id w.pending = some k) : w.live id = some kA pending request is live, with its kind.
deliver_acc {S : Type} (u : S → Action → S × List Effect) (acts : List Action)
(st : S) (effs : List Effect) :
List.foldl
(fun x a =>
match x with
| (st, effs) =>
match u st a with
| (st', e) => (st', effs ++ e))
(st, effs) acts =
((deliver u st acts).fst, effs ++ (deliver u st acts).snd)
deliver_cons {S : Type} (u : S → Action → S × List Effect) (st : S)
(a : Action) (acts : List Action) :
deliver u st (a :: acts) =
((deliver u (u st a).fst acts).fst, (u st a).snd ++ (deliver u (u st a).fst acts).snd)
deliver_logged {S : Type} (app : App S) (acts : List Action)
(st : S × List Entry) :
∃ ups,
(deliver (logUpdate app) st acts).fst.snd = st.snd ++ ups ∧
∀ (b : Book), b.run ups = some (b.takeAll (deliver (logUpdate app) st acts).snd)
give_inv {S : Type} (app : App S) {log0 : List Entry} {b0 b : Book}
{c : Ctx (S × List Entry)} {new : List Entry} {m : Msg} (hl : c.app.snd = log0 ++ new)
(hr : b0.run new = some b) (ha : b.admits m = true) (hw : Agrees c.world (b.pre m)) :
Inv log0 b0 (give (logged app) c m)
hear_inv {S : Type} (app : App S) {log0 : List Entry} {b0 : Book}
{c : Ctx (S × List Entry)} (h : Inv log0 b0 c) : Inv log0 b0 (hear (logged app) c)
fire_inv {S : Type} (app : App S) {log0 : List Entry} {b0 : Book}
{c : Ctx (S × List Entry)} (n : String) (h : Inv log0 b0 c) :
Inv log0 b0 (fire (logged app) c n)
foldl_fire_inv {S : Type} (app : App S) {log0 : List Entry} {b0 : Book}
(ns : List String) {c : Ctx (S × List Entry)} :
Inv log0 b0 c → Inv log0 b0 (List.foldl (fire (logged app)) c ns)
boot_booted {S : Type} (app : App S) (c : Ctx S) (h : c.world.booted = true) :
boot app c = c
ack_inv {S : Type} {log0 : List Entry} {b0 : Book} {c : Ctx (S × List Entry)}
(h : Inv log0 b0 c) (id : Nat) : Inv log0 b0 (ack c id)
admit_inv {S : Type} (app : App S) (s : State (S × List Entry)) (e : Event)
(hb : s.world.booted = true) {b0 : Book} (ha : Agrees s.world b0) :
Inv s.app.snd b0 (admit (logged app) s e)
act_inv {S : Type} (app : App S) {log0 : List Entry} {b0 : Book}
{c : Ctx (S × List Entry)} (acts : List Action) (h : Inv log0 b0 c) :
Inv log0 b0 (act (logged app) c acts)
act_nil {S : Type} (app : App S) (c : Ctx S) : act app c [] = c
step_ctx {S : Type} (app : App S) (cfg : Config) (s : State S) (e : Event) :
have c := act app (admit app s e) (route cfg.metrics s e).snd;
(step app cfg s e).fst.app = c.app ∧
∃ subs next,
(step app cfg s e).fst.world =
have __src := c.world;
{ clock := __src.clock, heard := __src.heard, booted := __src.booted,
timers := __src.timers, pending := __src.pending, queued := __src.queued,
stopping := __src.stopping, cap := __src.cap, nextTicket := __src.nextTicket,
subs := subs, nextSub := next }
step_book {S : Type} (app : App S) (cfg : Config) (s : State (S × List Entry))
(e : Event) (hb : s.world.booted = true) {b0 : Book} (ha : Agrees s.world b0) :
∃ new b,
(step (logged app) cfg s e).fst.app.snd = s.app.snd ++ new ∧
b0.run new = some b ∧ Agrees (step (logged app) cfg s e).fst.world bOne step of the recording app: the log grows by entries the book allows, and the runtime's tables agree with the book afterwards.
refl (w : World) : Grows w w
trans {a b c : World} (h1 : Grows a b) (h2 : Grows b c) : Grows a c
grows {w w' : World} (h : Same w w') : Grows w w'
give_grows {S : Type} (app : App S) (c : Ctx S) (m : Msg) :
Grows c.world (give app c m).world
give_grows' {S : Type} (app : App S) {w : World} {c : Ctx S} {m : Msg}
(h : Grows w c.world) : Grows w (give app c m).world
hear_grows {S : Type} (app : App S) (c : Ctx S) :
Grows c.world (hear app c).world
fire_grows {S : Type} (app : App S) (c : Ctx S) (n : String) :
Grows c.world (fire app c n).world
foldl_fire_grows {S : Type} (app : App S) (ns : List String) (c : Ctx S) :
Grows c.world (List.foldl (fire app) c ns).world
boot_grows {S : Type} (app : App S) (c : Ctx S) :
Grows c.world (boot app c).world
tick_mono (w : World) (t : Time) : w.clock.mono ≤ (w.tick t).clock.mono
tick_reaches (w : World) (t : Time) : t.mono ≤ (w.tick t).clock.mono
admit_clock_grows {S : Type} (app : App S) (s : State S) (t : Time) :
Grows (s.world.tick t) (admit app s (Event.clock t)).world
promoteGo_same (rest : List (Nat × Nat × Request)) (w : World) : Same w (w.promoteGo rest).fst
promote_same (w : World) : Same w w.promote.fst
release_grows {S : Type} (c : Ctx S) (w : World) (h : Same c.world w) :
Grows c.world (release c w).world
ack_grows {S : Type} (c : Ctx S) (id : Nat) : Grows c.world (ack c id).world
admit_grows {S : Type} (app : App S) (s : State S) (e : Event) :
Grows s.world (admit app s e).world
act_grows {S : Type} (app : App S) (c : Ctx S) (acts : List Action) :
Grows c.world (act app c acts).world
step_clock {S : Type} (app : App S) (cfg : Config) (s : State S) (e : Event) :
Grows s.world (step app cfg s e).fst.worldA step never moves the clock back, and once the first clock has booted the app it stays booted.
step_clock_reaches {S : Type} (app : App S) (cfg : Config) (s : State S)
(t : Time) : t.mono ≤ (step app cfg s (Event.clock t)).fst.world.clock.monoA clock event brings the runtime's clock at least to the host's time.
steps_go {S : Type} (app : App S) (cfg : Config) (P : State S → Prop)
(hstep : ∀ (s : State S) (e : Event), P s → P (step app cfg s e).fst) (es : List Event)
(s : State S) (effs : List Effect) :
P s →
P
(List.foldl
(fun x e =>
match x with
| (s, effs) =>
match step app cfg s e with
| (s', e') => (s', effs ++ e'))
(s, effs) es).fst
steps_clock {S : Type} (app : App S) (cfg : Config) (s : State S)
(es : List Event) :
s.world.clock.mono ≤ (steps app cfg s es).fst.world.clock.mono ∧
(s.world.booted = true → (steps app cfg s es).fst.world.booted = true)A batch never moves the clock back.
steps_book {S : Type} (app : App S) (cfg : Config)
(s : State (S × List Entry)) (es : List Event) (hb : s.world.booted = true) {b0 : Book}
(ha : Agrees s.world b0) :
∃ new b,
(steps (logged app) cfg s es).fst.app.snd = s.app.snd ++ new ∧
b0.run new = some b ∧ Agrees (steps (logged app) cfg s es).fst.world bTimers and replies. Over any batch of events after the first clock, everything
delivered to the app is allowed by the book: a timer reaches receive only while it is set
(never after cancelTimer, and once per setTimer), and a reply only to a pending request of
the kind it answers, once. And the runtime's tables still agree with the book at the end.
absorb1_pending (w : World) (e : Effect) {id : Nat} {k : Request.Kind} (he : e ≠ Effect.cancelRequest id) (h : List.lookup id w.pending = some k) : List.lookup id (w.absorb1 e).fst.pending = some k
absorb_pending (es : List Effect) (w : World) {id : Nat} {k : Request.Kind} : ¬Effect.cancelRequest id ∈ es → List.lookup id w.pending = some k → List.lookup id (w.absorb es).fst.pending = some k
hear_pending {S : Type} (app : App S) (c : Ctx S) {id : Nat}
{k : Request.Kind} (hq : KeepsOnClock app id)
(h : List.lookup id c.world.pending = some k) :
List.lookup id (hear app c).world.pending = some k
route_reply {S : Type} (m : TextMetrics) (s : State S) (id : Nat)
(r : Reply) : (route m s (Event.reply id r)).snd = []
route_subEvent {S : Type} (m : TextMetrics) (s : State S) (id : Nat)
(ev : SubEvent) : (route m s (Event.subEvent id ev)).snd = []
step_reply {S : Type} (app : App S) (cfg : Config)
(s : State (S × List Entry)) {id : Nat} {r : Reply} {k : Request.Kind}
(hk : List.lookup id s.world.pending = some k) (ha : Reply.answers k r = true)
(hq : KeepsOnClock app id) :
∃ es,
(step (logged app) cfg s (Event.reply id r)).fst.app.snd.getLast? =
some (Entry.recv (Msg.reply id r) es)A reply to a pending request, in the shape that answers it, is delivered to receive
with the id it was requested under: it is the last thing the app hears in that step. (Unless the
app withdrew the request on hearing the time just before: then it is swallowed,
step_reply_cancelled.)
step_reply_ignored {S : Type} (app : App S) (cfg : Config) (s : State S)
{id : Nat} {r : Reply} (h : s.world.takeReply id r = none) :
(step app cfg s (Event.reply id r)).fst.app = s.appA reply to an id that is not pending, or in the wrong shape, reaches no one.
step_sub {S : Type} (app : App S) (cfg : Config) (s : State (S × List Entry))
{id : Nat} {sub : Sub} (ev : SubEvent) (h : s.world.subOf id = some sub) :
∃ es,
(step (logged app) cfg s (Event.subEvent id ev)).fst.app.snd.getLast? =
some (Entry.recv (Msg.sub sub ev) es)An event from an active subscription is delivered as that subscription's message.
step_sub_ignored {S : Type} (app : App S) (cfg : Config) (s : State S)
{id : Nat} (ev : SubEvent) (h : s.world.subOf id = none) :
(step app cfg s (Event.subEvent id ev)).fst.app = s.appAn event for a subscription that is not active (stopped, or never started) reaches no one.
mem_freshSubs (want seen : List Sub) (x : Sub) : x ∈ freshSubs seen want ↔ x ∈ want ∧ ¬x ∈ seen
mem_number (l : List Sub) (n id : Nat) (x : Sub) : (id, x) ∈ number n l → x ∈ l ∧ n ≤ id ∧ id < n + l.length
number_mem (l : List Sub) (n : Nat) (x : Sub) : x ∈ l → ∃ id, (id, x) ∈ number n l
contains_false {l : List Sub} {x : Sub} : (!l.contains x) = true ↔ ¬x ∈ l
diffSubs_stop (active : List (Nat × Sub)) (want : List Sub) (next id : Nat) : SubCmd.stop id ∈ (diffSubs active want next).snd.fst ↔ ∃ sub, (id, sub) ∈ active ∧ ¬sub ∈ want
The diff stops exactly the running subscriptions the app no longer wants.
diffSubs_start (active : List (Nat × Sub)) (want : List Sub) (next id : Nat) (sub : Sub) : SubCmd.start id sub ∈ (diffSubs active want next).snd.fst ↔ (id, sub) ∈ number next (freshSubs (List.map (fun x => x.snd) (List.filter (fun p => want.contains p.snd) active)) want)
The new subscriptions the diff starts, under the ids it gives them.
fresh_iff (active : List (Nat × Sub)) (want : List Sub) (sub : Sub) : sub ∈ freshSubs (List.map (fun x => x.snd) (List.filter (fun p => want.contains p.snd) active)) want ↔ sub ∈ want ∧ ∀ (id : Nat), ¬(id, sub) ∈ active
diffSubs_starts (active : List (Nat × Sub)) (want : List Sub) (next : Nat) (sub : Sub) : (∃ id, SubCmd.start id sub ∈ (diffSubs active want next).snd.fst) ↔ sub ∈ want ∧ ∀ (id : Nat), ¬(id, sub) ∈ active
The diff starts exactly the wanted subscriptions that are not running, each once.
diffSubs_fresh (active : List (Nat × Sub)) (want : List Sub) (next id : Nat) (sub : Sub) (h : SubCmd.start id sub ∈ (diffSubs active want next).snd.fst) : next ≤ id ∧ id < (diffSubs active want next).snd.snd
Started subscriptions get fresh ids: at least next and below the new next.
diffSubs_active (active : List (Nat × Sub)) (want : List Sub) (next : Nat) (sub : Sub) : sub ∈ List.map (fun x => x.snd) (diffSubs active want next).fst ↔ sub ∈ want
After the diff, the running subscriptions are exactly the ones the app wants.
lookup_eq_none {β : Type} (l : List (Nat × β)) (id : Nat)
(h : ∀ (x : β), ¬(id, x) ∈ l) : List.lookup id l = none
diffSubs_stopped (active : List (Nat × Sub)) (want : List Sub) (next id : Nat) (hlt : ∀ (p : Nat × Sub), p ∈ active → p.fst < next) (hu : ∀ (a b : Sub), (id, a) ∈ active → (id, b) ∈ active → a = b) (h : SubCmd.stop id ∈ (diffSubs active want next).snd.fst) : List.lookup id (diffSubs active want next).fst = none
A stopped subscription is gone from the active set (when ids are below next and name one
subscription each, as diffSubs keeps them), so its late events reach no one
(step_sub_ignored).
Lookup tables
The world's other fields stay put
Books
Keyed lists
The runtime's request tables are lists keyed by id. While no id appears twice (Keys), a lookup
is a membership test.