Cairn · module
Cairn.Optimistic.Server
lean/Cairn/Optimistic/Server.lean
Optimistic values against a server: convergence for any order of replies
The abstract server Cairn.Optimistic is proved against (docs/optimistic.md, "The server
model"). A World is a table, the server (a register per key, reg), and the network: every
request the table sent and every answer on its way back, as a bag (net) that any step may take
any element of. The steps (World.press, serve, refuse, deliver, lose, retry,
look) are every way the person, the server and the network can act:
- the person sets a key (
press); - the server handles a request: applies a write (its answer is
acked) or answers a read with what it holds (serve), or refuses either (refuse): a refused write changes nothing; - the network delivers an answer to the table (
deliver), or loses a request or an answer, before or after the server handled it: the table hearslostorreadFailed(lose); - the backoff timer fires (
retry), and the app fetches a view of a key (look), which may arrive after the key has changed.
Writes are idempotent: applying one sets the register to its value, so applying it once or
twice is the same. A write is applied at most once here (serve takes the request out of the
bag), which loses nothing: a second application would set the same value.
Ok is the invariant, kept by every step (Ok.press … Ok.look); from it:
Ok.converges: a settled key shows what the server holds (bysame). So once nothing is in flight or in doubt, whatever order the replies came in, every key shows the server's value;Ok.oneWrite: at most one write in flight per key;Ok.writes_le_sets: never more writes sent for a key than the person's sets of it;Ok.count: a settled key's count is the view's other people plus the server's own.
Every step changes one key; Ok is per key (KeyOk), and a step at one key leaves every other
key's part as it was (World.at_*), which is also why replies for different keys commute
(Table.feed_comm).
Imports Cairn.Optimistic
Order
Structures 4
KeyOk {V : Type} (same : V → V → Bool) (e : Entry V) (r : V)
(ps : List (Pkt V)) : PropOne key is consistent with the server's value r and its packets ps: no packet is
from a request not yet made; every write in flight is the current request; a key never written
is idle and every view of it says r; and the current packets fit the phase.
Fields
le : n ≤ e.seq
writes : p.seq? = some e.seq
unwritten : e.phase = Phase.idle ∧ ∀ (v : V), Pkt.view v ∈ ps → v = r
phase : PhaseOk same e r (List.filter (Pkt.cur e.seq) ps)
World (K V : Type) [Ord K] : Type
The person, the table, the server and the network.
Fields
table : Table K V
srv : Std.TreeMap K V compare
The server: a register per key (reg).
net : List (K × Pkt V)
Every request and answer on its way, keyed.
sets : List K
The key of every set, in order.
writes : List K
The key of every write the table sent, in order.
Ok {K V : Type} [Ord K] [DecidableEq K] [DecidableEq V]
(w : World K V) : PropThe invariant: same is an equivalence, and every key is consistent, with writes within
sets.
Fields
same : Same w.table.same
key : KeyOk w.table.same (w.table.get k) (w.reg k) («at» w.net k)
budget : Entry.Budget w.table.same (w.table.get k) (List.count k w.sets) (List.count k w.writes)
Rest {V : Type} (m : Nat) (ps : List (Pkt V)) : PropThe packets of a key after its current request left: none from a later request, no write, none current.
Fields
le : n ≤ m
noWrite : q.isWrite = falsenoCur : List.filter (Pkt.cur m) ps = []
Inductive types 3
Pkt (V : Type) : Type
A packet about one key, in the network. Numbers are the key's request numbers.
Constructors
write {V : Type} (n : Nat) (v : V) : Pkt VA write the server hasn't handled.
read {V : Type} (n : Nat) : Pkt VA read the server hasn't handled.
acked {V : Type} (n : Nat) : Pkt VThe server applied write n; the answer is on its way.
refused {V : Type} (n : Nat) : Pkt VThe server refused write n and didn't apply it.
answer {V : Type} (n : Nat) (v : V) : Pkt VThe server answered read n with v, what it held then.
failed {V : Type} (n : Nat) : Pkt VThe server refused read n.
view {V : Type} (v : V) : Pkt VA view of the key, saying v.
Instances
Step {K V : Type} [Ord K] [DecidableEq K] [DecidableEq V] :
World K V → World K V → PropEvery step.
Constructors
press {K V : Type} [Ord K] [DecidableEq K] [DecidableEq V]
(w : World K V) (k : K) (f : V → V) : w.Step (w.press k f)serve {K V : Type} [Ord K] [DecidableEq K] [DecidableEq V]
(w : World K V) (k : K) (p : Pkt V) : w.Step (w.serve k p)refuse {K V : Type} [Ord K] [DecidableEq K] [DecidableEq V]
(w : World K V) (k : K) (p : Pkt V) : w.Step (w.refuse k p)deliver {K V : Type} [Ord K] [DecidableEq K] [DecidableEq V]
(w : World K V) (k : K) (p : Pkt V) : w.Step (w.deliver k p)lose {K V : Type} [Ord K] [DecidableEq K] [DecidableEq V]
(w : World K V) (k : K) (p : Pkt V) : w.Step (w.lose k p)retry {K V : Type} [Ord K] [DecidableEq K] [DecidableEq V]
(w : World K V) (k : K) : w.Step (w.retry k)look {K V : Type} [Ord K] [DecidableEq K] [DecidableEq V]
(w : World K V) (k : K) : w.Step (w.look k)Reach {K V : Type} [Ord K] [DecidableEq K] [DecidableEq V] :
World K V → World K V → PropSome steps, in order.
Constructors
refl {K V : Type} [Ord K] [DecidableEq K] [DecidableEq V]
(w : World K V) : w.Reach wtail {K V : Type} [Ord K] [DecidableEq K] [DecidableEq V]
{a b c : World K V} : a.Reach b → b.Step c → a.Reach cDefinitions 24
seq? {V : Type} : Pkt V → Option Nat
isWrite {V : Type} : Pkt V → BoolA write, before or after the server handled it: a write in flight.
cur {V : Type} (n : Nat) (p : Pkt V) : BoolWhether the packet is request n of its key.
Readish {V : Type} (n : Nat) (r : V) (p : Pkt V) : PropA read n, before or after the server handled it; an answer says r.
PhaseOk {V : Type} (same : V → V → Bool) (e : Entry V) (r : V)
(cur : List (Pkt V)) : PropWhat a key's packets with its current number say, by phase. cur is those packets, r the
server's value.
reg {K V : Type} [Ord K] (w : World K V) (k : K) : VWhat the server holds for k.
at {K V : Type} [DecidableEq K] (net : List (K × Pkt V)) (k : K) :
List (Pkt V)The packets about k.
pktOf {K V : Type} : Out K V → Option (K × Pkt V)A table output, as the packet it puts in the network.
writeOf {K V : Type} : Out K V → Option KA table output's key, if it is a write.
feed {K V : Type} [Ord K] (w : World K V) (i : Input K V) : World K VThe table hears i; what it sends goes into the network.
press {K V : Type} [Ord K] (w : World K V) (k : K) (f : V → V) :
World K VThe person sets k to f of what it shows.
serve {K V : Type} [Ord K] [DecidableEq K] [DecidableEq V]
(w : World K V) (k : K) (p : Pkt V) : World K VThe server handles packet (k, p): applies a write, or answers a read with what it holds.
refuse {K V : Type} [Ord K] [DecidableEq K] [DecidableEq V]
(w : World K V) (k : K) (p : Pkt V) : World K VThe server refuses packet (k, p), and changes nothing.
heard {K V : Type} (k : K) : Pkt V → Option (Input K V)The input the table hears when (k, p) arrives.
missed {K V : Type} (k : K) : Pkt V → Option (Input K V)The input the table hears when (k, p) is lost on the way.
deliver {K V : Type} [Ord K] [DecidableEq K] [DecidableEq V]
(w : World K V) (k : K) (p : Pkt V) : World K VThe network delivers answer (k, p) to the table.
lose {K V : Type} [Ord K] [DecidableEq K] [DecidableEq V]
(w : World K V) (k : K) (p : Pkt V) : World K VThe network loses (k, p), before or after the server handled it.
retry {K V : Type} [Ord K] (w : World K V) (k : K) : World K Vk's backoff timer fires.
look {K V : Type} [Ord K] (w : World K V) (k : K) : World K VThe app fetches a view of k: what the server holds now, delivered whenever.
start {K V : Type} [Ord K] (dflt : V) (same : V → V → Bool) :
World K VA world at the start: an empty table, a server holding dflt for every key (srv empty),
nothing in the network.
ofAct {V : Type} : Act V → Option (Pkt V)An entry's action, as the packet it puts in the network.
heard {V : Type} : Pkt V → Option (Ev V)What the key hears when p arrives.
missed {V : Type} : Pkt V → Option (Ev V)What the key hears when p is lost.
after {V : Type} (same : V → V → Bool) (e : Entry V)
(ps : List (Pkt V)) (ev : Ev V) : List (Pkt V)The key hears ev, with ps its packets after the one that brought ev left.
Theorems 71
small {V : Type} [DecidableEq V] {same : V → V → Bool}
{e : Entry V} {r : V} {cur : List (Pkt V)} (h : PhaseOk same e r cur) :
cur = [] ∨ ∃ x, cur = [x]
cur_mem {V : Type} [DecidableEq V] {ps : List (Pkt V)} {n : Nat}
{p : Pkt V} (hp : p ∈ ps) (hc : Pkt.cur n p = true) : p ∈ List.filter (Pkt.cur n) ps
single {V : Type} [DecidableEq V] {same : V → V → Bool} {e : Entry V}
{r : V} {ps : List (Pkt V)} (h : KeyOk same e r ps) {p : Pkt V} (hp : p ∈ ps)
(hc : Pkt.cur e.seq p = true) : List.filter (Pkt.cur e.seq) ps = [p]A current packet is the only one.
isWrite_cur {V : Type} [DecidableEq V] {same : V → V → Bool}
{e : Entry V} {r : V} {ps : List (Pkt V)} (h : KeyOk same e r ps) {q : Pkt V}
(hq : q ∈ ps) (hw : q.isWrite = true) : Pkt.cur e.seq q = true
rest_erase {V : Type} [DecidableEq V] {same : V → V → Bool}
{e : Entry V} {r : V} {ps : List (Pkt V)} (h : KeyOk same e r ps) {p : Pkt V}
(hp : p ∈ ps) (hc : Pkt.cur e.seq p = true) : Rest e.seq (ps.erase p)With the current packet gone, the rest.
rest_self {V : Type} [DecidableEq V] {same : V → V → Bool}
{e : Entry V} {r : V} {ps : List (Pkt V)} (h : KeyOk same e r ps)
(hnc : List.filter (Pkt.cur e.seq) ps = []) : Rest e.seq psWith nothing current, all of them.
fresh {V : Type} [DecidableEq V] {same : V → V → Bool}
{e e' : Entry V} {r : V} {ps : List (Pkt V)}
(hle : ∀ (q : Pkt V), q ∈ ps → ∀ (n : Nat), q.seq? = some n → n ≤ e.seq)
(hnw : ∀ (q : Pkt V), q ∈ ps → q.isWrite = false) (hs : e'.seq = e.seq + 1) {q : Pkt V}
(hq : q.seq? = some e'.seq) (hph : PhaseOk same e' r [q]) (hw : e'.written = true) :
KeyOk same e' r (ps ++ [q])A new request: the rest, and the request's one packet.
quiet {V : Type} [DecidableEq V] {same : V → V → Bool}
{e e' : Entry V} {r : V} {ps : List (Pkt V)} (h : Rest e.seq ps) (hs : e'.seq = e.seq)
(hph : PhaseOk same e' r [])
(hu : e'.written = false → e'.phase = Phase.idle ∧ ∀ (v : V), Pkt.view v ∈ ps → v = r) :
KeyOk same e' r psNothing new: the rest, with nothing current.
erase_stale {V : Type} [DecidableEq V] {same : V → V → Bool}
{e : Entry V} {r : V} {ps : List (Pkt V)} (h : KeyOk same e r ps) {p : Pkt V}
(hc : Pkt.cur e.seq p = false) : KeyOk same e r (ps.erase p)A packet that isn't current can go.
open_facts {V : Type} [DecidableEq V] {same : V → V → Bool}
{e : Entry V} {r : V} {ps : List (Pkt V)} (h : KeyOk same e r ps)
(ho : e.phase.isOpen = true) :
(∀ (q : Pkt V), q ∈ ps → q.isWrite = false) ∧ e.server = r ∧ same e.want e.server = trueNothing in flight: no write among the packets, and the server's value is confirmed.
write_cases {V : Type} [DecidableEq V] {same : V → V → Bool}
{e : Entry V} {r : V} {ps : List (Pkt V)} (h : KeyOk same e r ps) {p : Pkt V}
(hp : p ∈ ps) (hw : p.isWrite = true) :
Pkt.cur e.seq p = true ∧
e.written = true ∧
∃ w,
e.phase = Phase.writing w ∧
(p = Pkt.write e.seq w ∧ r = e.server ∨
p = Pkt.acked e.seq ∧ r = w ∨ p = Pkt.refused e.seq ∧ r = e.server)A write in flight is the current request, and the key is writing it.
read_cases {V : Type} [DecidableEq V] {same : V → V → Bool}
{e : Entry V} {r : V} {ps : List (Pkt V)} (h : KeyOk same e r ps) {p : Pkt V}
(hp : p ∈ ps) (hc : Pkt.cur e.seq p = true) (hw : p.isWrite = false) :
Readish e.seq r p ∧
e.written = true ∧
(e.phase = Phase.checking ∧ e.server = r ∧ same e.want e.server = true ∨
∃ w, e.phase = Phase.doubt w)A current read, before or after the server: the key is checking or in doubt.
settle_ok {V : Type} [DecidableEq V] {same : V → V → Bool}
(_hs : Same same) {e : Entry V} {r : V} {ps : List (Pkt V)} (h : Rest e.seq ps)
(hw : e.written = true) (hr : e.server = r) :
KeyOk same (Entry.settle same e).fst r
(ps ++ List.filterMap Pkt.ofAct (Entry.settle same e).snd)The server's value r is known: rest, or write toward want.
rollback_ok {V : Type} [DecidableEq V] {same : V → V → Bool}
(hs : Same same) {e : Entry V} {r : V} {ps : List (Pkt V)} (h : Rest e.seq ps)
(hw : e.written = true) (hr : e.server = r) (why : Reason) :
KeyOk same (Entry.rollback same e why).fst r
(ps ++ List.filterMap Pkt.ofAct (Entry.rollback same e why).snd)Back to the server's value r.
readFailed_ok {V : Type} [DecidableEq V] {same : V → V → Bool}
{e : Entry V} {r : V} {ps : List (Pkt V)} (h : KeyOk same e r ps) {p : Pkt V}
(hp : p ∈ ps) {n : Nat} (hn : p.seq? = some n) (hw : p.isWrite = false) :
KeyOk same (Entry.step same e (Ev.readFailed n)).fst r
(after same e (ps.erase p) (Ev.readFailed n))A read's failure, current or stale.
lost_ok {V : Type} [DecidableEq V] {same : V → V → Bool}
{e : Entry V} {r : V} {ps : List (Pkt V)} (h : KeyOk same e r ps) {p : Pkt V}
(hp : p ∈ ps) {n : Nat} (hn : p.seq? = some n) (hw : p.isWrite = true) :
KeyOk same (Entry.step same e (Ev.lost n)).fst r (after same e (ps.erase p) (Ev.lost n))A write's answer lost: in doubt, and a read.
press {V : Type} [DecidableEq V] {same : V → V → Bool}
(_hs : Same same) {e : Entry V} {r : V} {ps : List (Pkt V)} (h : KeyOk same e r ps)
(f : V → V) : KeyOk same (Entry.step same e (Ev.set f)).fst r (after same e ps (Ev.set f))
retry {V : Type} [DecidableEq V] {same : V → V → Bool}
(_hs : Same same) {e : Entry V} {r : V} {ps : List (Pkt V)} (h : KeyOk same e r ps) :
KeyOk same (Entry.step same e Ev.retry).fst r (after same e ps Ev.retry)
look {V : Type} [DecidableEq V] {same : V → V → Bool} {e : Entry V}
{r : V} {ps : List (Pkt V)} (h : KeyOk same e r ps) : KeyOk same e r (ps ++ [Pkt.view r])
deliver {V : Type} [DecidableEq V] {same : V → V → Bool}
(hs : Same same) {e : Entry V} {r : V} {ps : List (Pkt V)} (h : KeyOk same e r ps)
{p : Pkt V} (hp : p ∈ ps) {ev : Ev V} (hev : p.heard = some ev) :
KeyOk same (Entry.step same e ev).fst r (after same e (ps.erase p) ev)
lose {V : Type} [DecidableEq V] {same : V → V → Bool}
(_hs : Same same) {e : Entry V} {r : V} {ps : List (Pkt V)} (h : KeyOk same e r ps)
{p : Pkt V} (hp : p ∈ ps) {ev : Ev V} (hev : p.missed = some ev) :
KeyOk same (Entry.step same e ev).fst r (after same e (ps.erase p) ev)
drop {V : Type} [DecidableEq V] {same : V → V → Bool} {e : Entry V}
{r : V} {ps : List (Pkt V)} (h : KeyOk same e r ps) {v : V} :
KeyOk same e r (ps.erase (Pkt.view v))
write_phase {V : Type} [DecidableEq V] {same : V → V → Bool}
{e : Entry V} {r : V} {ps : List (Pkt V)} (h : KeyOk same e r ps) {n : Nat} {v : V}
(hp : Pkt.write n v ∈ ps) :
n = e.seq ∧ e.phase = Phase.writing v ∧ r = e.server ∧ e.written = trueThe current write's phase: writing v, the server's value the confirmed one.
swapWrite {V : Type} [DecidableEq V] {same : V → V → Bool}
{e : Entry V} {r : V} {ps : List (Pkt V)} (h : KeyOk same e r ps) {n : Nat} {v : V}
(hp : Pkt.write n v ∈ ps) {q : Pkt V} {r' : V}
(hq : q = Pkt.acked n ∧ r' = v ∨ q = Pkt.refused n ∧ r' = r) :
KeyOk same e r' (ps.erase (Pkt.write n v) ++ [q])
serveWrite {V : Type} [DecidableEq V] {same : V → V → Bool}
{e : Entry V} {r : V} {ps : List (Pkt V)} (h : KeyOk same e r ps) {n : Nat} {v : V}
(hp : Pkt.write n v ∈ ps) : KeyOk same e v (ps.erase (Pkt.write n v) ++ [Pkt.acked n])
swapRead {V : Type} [DecidableEq V] {same : V → V → Bool}
{e : Entry V} {r : V} {ps : List (Pkt V)} (h : KeyOk same e r ps) {n : Nat}
(hp : Pkt.read n ∈ ps) {q : Pkt V} (hq : q = Pkt.answer n r ∨ q = Pkt.failed n) :
KeyOk same e r (ps.erase (Pkt.read n) ++ [q])
serveRead {V : Type} [DecidableEq V] {same : V → V → Bool}
{e : Entry V} {r : V} {ps : List (Pkt V)} (h : KeyOk same e r ps) {n : Nat}
(hp : Pkt.read n ∈ ps) : KeyOk same e r (ps.erase (Pkt.read n) ++ [Pkt.answer n r])
refuseWrite {V : Type} [DecidableEq V] {same : V → V → Bool}
{e : Entry V} {r : V} {ps : List (Pkt V)} (h : KeyOk same e r ps) {n : Nat} {v : V}
(hp : Pkt.write n v ∈ ps) : KeyOk same e r (ps.erase (Pkt.write n v) ++ [Pkt.refused n])
refuseRead {V : Type} [DecidableEq V] {same : V → V → Bool}
{e : Entry V} {r : V} {ps : List (Pkt V)} (h : KeyOk same e r ps) {n : Nat}
(hp : Pkt.read n ∈ ps) : KeyOk same e r (ps.erase (Pkt.read n) ++ [Pkt.failed n])
converges {V : Type} [DecidableEq V] {same : V → V → Bool}
{e : Entry V} {r : V} {ps : List (Pkt V)} (h : KeyOk same e r ps)
(hi : e.phase.isIdle = true) : same e.want r = trueA settled key shows the server's value.
oneWrite {V : Type} [DecidableEq V] {same : V → V → Bool}
{e : Entry V} {r : V} {ps : List (Pkt V)} (h : KeyOk same e r ps) :
List.countP Pkt.isWrite ps ≤ 1At most one write in flight.
at_append {K V : Type} [Ord K] [Std.TransOrd K] [Std.LawfulEqOrd K]
[DecidableEq K] [DecidableEq V] (a b : List (K × Pkt V)) (k : K) :
«at» (a ++ b) k = «at» a k ++ «at» b k
at_single {K V : Type} [Ord K] [Std.TransOrd K] [Std.LawfulEqOrd K]
[DecidableEq K] [DecidableEq V] (j : K) (p : Pkt V) (k : K) :
«at» [(j, p)] k = if j = k then [p] else []
at_erase {K V : Type} [Ord K] [Std.TransOrd K] [Std.LawfulEqOrd K]
[DecidableEq K] [DecidableEq V] (net : List (K × Pkt V)) (j : K) (p : Pkt V) (k : K) :
«at» (net.erase (j, p)) k = if j = k then («at» net k).erase p else «at» net k
mem_at {K V : Type} [Ord K] [Std.TransOrd K] [Std.LawfulEqOrd K]
[DecidableEq K] [DecidableEq V] {net : List (K × Pkt V)} {j : K} {p : Pkt V}
(h : (j, p) ∈ net) : p ∈ «at» net j
at_out {K V : Type} [Ord K] [Std.TransOrd K] [Std.LawfulEqOrd K]
[DecidableEq K] [DecidableEq V] (os : List (Act V)) (j k : K) :
«at» (List.filterMap pktOf (List.map (Act.out j) os)) k =
if j = k then List.filterMap Pkt.ofAct os else []
count_writeOf {K V : Type} [Ord K] [Std.TransOrd K]
[Std.LawfulEqOrd K] [DecidableEq K] [DecidableEq V] (os : List (Out K V)) (k : K) :
List.count k (List.filterMap writeOf os) = Table.writesFor k os
reg_feed {K V : Type} [Ord K] [Std.TransOrd K] [Std.LawfulEqOrd K]
[DecidableEq K] [DecidableEq V] (w : World K V) (i : Input K V) (k : K) :
(w.feed i).reg k = w.reg k
get_feed {K V : Type} [Ord K] [Std.TransOrd K] [Std.LawfulEqOrd K]
[DecidableEq K] [DecidableEq V] (w : World K V) (i : Input K V) (k : K) :
(w.feed i).table.get k =
if i.key = k then (Entry.step w.table.same (w.table.get i.key) i.ev).fst
else w.table.get k
at_feed {K V : Type} [Ord K] [Std.TransOrd K] [Std.LawfulEqOrd K]
[DecidableEq K] [DecidableEq V] (w : World K V) (i : Input K V) (k : K) :
«at» (w.feed i).net k =
if i.key = k then KeyOk.after w.table.same (w.table.get k) («at» w.net k) i.ev
else «at» w.net k
ok_feed {K V : Type} [Ord K] [Std.TransOrd K] [Std.LawfulEqOrd K]
[DecidableEq K] [DecidableEq V] (w : World K V) (i : Input K V) (hs : Same w.table.same)
(hk : ∀ (k : K), i.key ≠ k → KeyOk w.table.same (w.table.get k) (w.reg k) («at» w.net k))
(hi :
KeyOk w.table.same (Entry.step w.table.same (w.table.get i.key) i.ev).fst (w.reg i.key)
(KeyOk.after w.table.same (w.table.get i.key) («at» w.net i.key) i.ev))
(sets : List K)
(hsets : ∀ (k : K), List.count k sets = List.count k w.sets + Table.setsFor k [i])
(hb :
∀ (k : K),
Entry.Budget w.table.same (w.table.get k) (List.count k w.sets)
(List.count k w.writes)) :
(have __src := w.feed i;
{ table := __src.table, srv := __src.srv, net := __src.net, sets := sets,
writes := __src.writes }).OkThe table hears i in a world whose other keys are fine and whose key i.key is fine after
it: then every key is. Budget: s more sets of i.key (1 for a set).
start {K V : Type} [Ord K] [Std.TransOrd K] [Std.LawfulEqOrd K]
[DecidableEq K] [DecidableEq V] (dflt : V) (same : V → V → Bool) (hs : Same same) :
(World.start dflt same).Ok
sets_single {K V : Type} [Ord K] [Std.TransOrd K]
[Std.LawfulEqOrd K] [DecidableEq K] [DecidableEq V] (w : World K V) (j : K) (f : V → V)
(k : K) :
List.count k (w.sets ++ [j]) = List.count k w.sets + Table.setsFor k [Input.set j f]
sets_other {K V : Type} [Ord K] [Std.TransOrd K]
[Std.LawfulEqOrd K] [DecidableEq K] [DecidableEq V] (w : World K V) (i : Input K V)
(hi : ∀ (j : K) (f : V → V), i ≠ Input.set j f) (k : K) :
List.count k w.sets = List.count k w.sets + Table.setsFor k [i]
press {K V : Type} [Ord K] [Std.TransOrd K] [Std.LawfulEqOrd K]
[DecidableEq K] [DecidableEq V] {w : World K V} (h : w.Ok) (k : K) (f : V → V) :
(w.press k f).Ok
retry {K V : Type} [Ord K] [Std.TransOrd K] [Std.LawfulEqOrd K]
[DecidableEq K] [DecidableEq V] {w : World K V} (h : w.Ok) (k : K) : (w.retry k).Ok
reg_insert {K V : Type} [Ord K] [Std.TransOrd K]
[Std.LawfulEqOrd K] [DecidableEq K] [DecidableEq V] (m : Std.TreeMap K V compare)
(k j : K) (v d : V) : (m.insert k v)[j]?.getD d = if k = j then v else m[j]?.getD d
local_ {K V : Type} [Ord K] [Std.TransOrd K] [Std.LawfulEqOrd K]
[DecidableEq K] [DecidableEq V] {w w' : World K V} (h : w.Ok) (ht : w'.table = w.table)
(hs : w'.sets = w.sets) (hw : w'.writes = w.writes) (k : K)
(hk : KeyOk w.table.same (w.table.get k) (w'.reg k) («at» w'.net k))
(ho : ∀ (j : K), k ≠ j → w'.reg j = w.reg j ∧ «at» w'.net j = «at» w.net j) : w'.OkA step that changes only the server and the network, at key k.
look {K V : Type} [Ord K] [Std.TransOrd K] [Std.LawfulEqOrd K]
[DecidableEq K] [DecidableEq V] {w : World K V} (h : w.Ok) (k : K) : (w.look k).Ok
serve {K V : Type} [Ord K] [Std.TransOrd K] [Std.LawfulEqOrd K]
[DecidableEq K] [DecidableEq V] {w : World K V} (h : w.Ok) (k : K) (p : Pkt V) :
(w.serve k p).Ok
refuse {K V : Type} [Ord K] [Std.TransOrd K] [Std.LawfulEqOrd K]
[DecidableEq K] [DecidableEq V] {w : World K V} (h : w.Ok) (k : K) (p : Pkt V) :
(w.refuse k p).Ok
heard_key {K V : Type} [Ord K] [Std.TransOrd K]
[Std.LawfulEqOrd K] [DecidableEq K] [DecidableEq V] (k : K) (p : Pkt V) (i : Input K V)
(hi : heard k p = some i) : i.key = k ∧ p.heard = some i.ev
missed_key {K V : Type} [Ord K] [Std.TransOrd K]
[Std.LawfulEqOrd K] [DecidableEq K] [DecidableEq V] (k : K) (p : Pkt V) (i : Input K V)
(hi : missed k p = some i) : i.key = k ∧ p.missed = some i.ev
heard_set {K V : Type} [Ord K] [Std.TransOrd K]
[Std.LawfulEqOrd K] [DecidableEq K] [DecidableEq V] (k : K) (p : Pkt V) (i : Input K V)
(hi : heard k p = some i) (j : K) (f : V → V) : i ≠ Input.set j f
missed_set {K V : Type} [Ord K] [Std.TransOrd K]
[Std.LawfulEqOrd K] [DecidableEq K] [DecidableEq V] (k : K) (p : Pkt V) (i : Input K V)
(hi : missed k p = some i) (j : K) (f : V → V) : i ≠ Input.set j f
erase_feed {K V : Type} [Ord K] [Std.TransOrd K]
[Std.LawfulEqOrd K] [DecidableEq K] [DecidableEq V] {w : World K V} (h : w.Ok) (k : K)
(p : Pkt V) (i : Input K V) (hk : i.key = k)
(hset : ∀ (j : K) (f : V → V), i ≠ Input.set j f)
(hi :
KeyOk w.table.same (Entry.step w.table.same (w.table.get k) i.ev).fst (w.reg k)
(KeyOk.after w.table.same (w.table.get k) ((«at» w.net k).erase p) i.ev)) :
({ table := w.table, srv := w.srv, net := w.net.erase (k, p), sets := w.sets,
writes := w.writes }.feed
i).OkThe packet (k, p) leaves the network and the table hears i about k.
deliver {K V : Type} [Ord K] [Std.TransOrd K] [Std.LawfulEqOrd K]
[DecidableEq K] [DecidableEq V] {w : World K V} (h : w.Ok) (k : K) (p : Pkt V) :
(w.deliver k p).Ok
lose {K V : Type} [Ord K] [Std.TransOrd K] [Std.LawfulEqOrd K]
[DecidableEq K] [DecidableEq V] {w : World K V} (h : w.Ok) (k : K) (p : Pkt V) :
(w.lose k p).Ok
step {K V : Type} [Ord K] [Std.TransOrd K] [Std.LawfulEqOrd K]
[DecidableEq K] [DecidableEq V] {w w' : World K V} (h : w.Ok) (hs : w.Step w') : w'.OkEvery step keeps Ok.
converges {K V : Type} [Ord K] [Std.TransOrd K]
[Std.LawfulEqOrd K] [DecidableEq K] [DecidableEq V] {w : World K V} (h : w.Ok) (k : K)
(hk : w.table.settled k = true) : w.table.same (w.table.shown k) (w.reg k) = trueConvergence. In a world reached by any steps, in any order, every settled key (nothing in flight, nothing in doubt) shows what the server holds.
oneWrite {K V : Type} [Ord K] [Std.TransOrd K] [Std.LawfulEqOrd K]
[DecidableEq K] [DecidableEq V] {w : World K V} (h : w.Ok) (k : K) :
List.countP Pkt.isWrite («at» w.net k) ≤ 1One write in flight per key: at most one write about k in the network, before or after
the server handled it.
writes_le_sets {K V : Type} [Ord K] [Std.TransOrd K]
[Std.LawfulEqOrd K] [DecidableEq K] [DecidableEq V] {w : World K V} (h : w.Ok) (k : K) :
List.count k w.writes ≤ List.count k w.setsNever more writes than sets.
count {K : Type} [Ord K] [Std.TransOrd K] [Std.LawfulEqOrd K]
[DecidableEq K] {w : World K Bool} (h : w.Ok) (hsame : w.table.same = fun a b => a == b)
(k : K) (hk : w.table.settled k = true) (o : Nat) (v : Bool) :
Optimistic.count (o + ind v) v (w.table.shown k) = o + ind (w.reg k)Counts. For a boolean key with the view's count o + [v] (others o, the person's own
v), a settled key shows o + [what the server holds]; exactly the server's count when no one
else acted since the view.
reach {K V : Type} [Ord K] [Std.TransOrd K] [Std.LawfulEqOrd K]
[DecidableEq K] [DecidableEq V] {w w' : World K V} (h : w.Ok) (hr : w.Reach w') : w'.OkAny run of steps from the start keeps Ok.
press_same {K V : Type} [Ord K] [DecidableEq K] [DecidableEq V]
(w : World K V) (k : K) (f : V → V) : (w.press k f).table.same = w.table.same
retry_same {K V : Type} [Ord K] [DecidableEq K] [DecidableEq V]
(w : World K V) (k : K) : (w.retry k).table.same = w.table.same
look_same {K V : Type} [Ord K] [DecidableEq K] [DecidableEq V]
(w : World K V) (k : K) : (w.look k).table.same = w.table.same
serve_same {K V : Type} [Ord K] [DecidableEq K] [DecidableEq V]
(w : World K V) (k : K) (p : Pkt V) : (w.serve k p).table.same = w.table.same
refuse_same {K V : Type} [Ord K] [DecidableEq K] [DecidableEq V]
(w : World K V) (k : K) (p : Pkt V) : (w.refuse k p).table.same = w.table.same
deliver_same {K V : Type} [Ord K] [DecidableEq K] [DecidableEq V]
(w : World K V) (k : K) (p : Pkt V) : (w.deliver k p).table.same = w.table.same
lose_same {K V : Type} [Ord K] [DecidableEq K] [DecidableEq V]
(w : World K V) (k : K) (p : Pkt V) : (w.lose k p).table.same = w.table.same
Instances 2
instDecidableEqPkt {V✝ : Type} [DecidableEq V✝] : DecidableEq (Pkt V✝)
instReprPkt {V✝ : Type} [Repr V✝] : Repr (Pkt V✝)
One key
Every key
same and dflt never change.