Cairn.Optimistic
lean/Cairn/Optimistic.lean
Optimistic values: shown at once, then confirmed or rolled back
A Table K V holds values a person changes and a server keeps, keyed by K (a post's URI, an
account's DID). A change shows in the step it is made; the table then sends one write for it,
and the server's answer confirms it or rolls it back (docs/optimistic.md). Nothing here knows
about any particular server: the app turns the table's outputs into requests and the requests'
answers into its inputs.
Per key the table keeps an Entry:
server, the last value the server confirmed: an acknowledged write, an authoritative read, or a view of a key never written this session;want, what the person asked for last. This is what is shown (Table.shown);phase: nothing outstanding (idle), a write in flight (writing v), a write whose answer was lost and a read in flight to settle it (doubt v), the same with the read failed and a retry due (waiting v), or a read checking a view that disagreed (checking);seq, the number of the key's last request: answers carry it (Ticket), and an answer whose number isn't the current one is stale and ignored. So a duplicated, late or superseded answer changes nothing.
The rules (Entry.step):
- One write in flight per key. A
setwhile one is in flight, or in doubt, only changeswant. When the write is answered, one write towardwantis sent ifwantandserverstill differ (by the app'ssame, e.g. "liked or not, whichever record"). - Refused rolls the key back in that step:
want := server, reported asrolledBackwhen what is shown changes. - Lost (no answer: a timeout, a network failure, a 5xx) puts the key in doubt and sends a
read. The read's answer settles it: the server holds the written value (acknowledged) or it
doesn't (refused,
Reason.notApplied). A failed read is retried on a backoff (1 s, doubling, at most 30 s,retryIn), never by writing again. - Views (
seen) move a key only if it has never been written this session. A written key that a view disagrees with, with nothing outstanding, gets a read (checking), whose answer is authoritative. So a stale view never undoes a confirmed write. - Counts over a boolean value:
count c v w = c − [v] + [w](count).
Lookups and updates are O(log n) in the number of keys (Std.TreeMap).
Theorems here, for every table: shown_set (a set shows in its own step), get_feed_ne (an
input touches only its key), feed_comm (inputs for different keys commute: the same table,
the same outputs, in the other order), refused_rollback (a refusal shows server in its step),
seen_written (a view never moves a written key), writes_le_sets (never more writes than sets,
per key, for any sequence of inputs), and the count's arithmetic (count_exact, count_ge).
Convergence against a server, for any order of replies, is Cairn.Optimistic.Server; the claims
(cairn^1100–cairn^1114) are Cairn.Optimistic.Claims.
Imports Std.Data.TreeMap
Structures 4
Entry (V : Type) : Type
One key's state.
server : V
The last value the server confirmed.
want : V
What the person asked for last: what is shown.
written : BoolWhether the person has set this key this session.
phase : Phase V
seq : NatThe number of the key's last request (0: none yet).
backoff : NatThe wait before the next retry of a failed read.
Ticket (K : Type) : Type
A request's ticket: the key it is about and its number among that key's requests. The app keeps its own request ids and maps each to the ticket it was sent for (docs/optimistic.md).
key : K
seq : NatTable (K V : Type) [Ord K] : Type
The table. dflt is the value of a key it hasn't heard of; same a b says whether two
values mean the same to the server (for a like: liked or not, whichever record). same should
be an equivalence (Same); the theorems that need it say so.
entries : Std.TreeMap K (Entry V) compare
dflt : V
same : BoolSame {V : Type} (same : V → V → Bool) : Propsame is an equivalence.
refl : same a a = truesymm : same b a = truetrans : same a c = trueInductive types 6
Phase (V : Type) : Type
What a key is waiting for.
idle {V : Type} : Phase VNothing outstanding.
writing {V : Type} (v : V) : Phase VA write of v is in flight.
doubt {V : Type} (v : V) : Phase VThe write of v got no answer; a read is in flight to learn whether it was applied.
waiting {V : Type} (v : V) : Phase VThe same, with that read failed; a retry sends the next.
checking {V : Type} : Phase VA view disagreed with a written key; a read is in flight to check it.
Reason : Type
Why a key was rolled back.
Ev (V : Type) : Type
What one key hears (Input without the key).
set {V : Type} (f : V → V) : Ev Vacked {V : Type} (n : Nat) : Ev Vrefused {V : Type} (n : Nat) (why : String) : Ev Vlost {V : Type} (n : Nat) : Ev Vread {V : Type} (n : Nat) (v : V) : Ev VreadFailed {V : Type} (n : Nat) : Ev Vretry {V : Type} : Ev Vseen {V : Type} (v : V) : Ev VAct (V : Type) : Type
What one key asks for (Out without the key).
write {V : Type} (n : Nat) (v : V) : Act Vread {V : Type} (n : Nat) : Act VretryIn {V : Type} (ms : Nat) : Act VrolledBack {V : Type} (r : Reason) : Act VInput (K V : Type) : Type
What the table hears.
set {K V : Type} (k : K) (f : V → V) : Input K VThe person changes key k to f of what is shown (f : V → V, so "like" on a value
already liked can keep its record).
acked {K V : Type} (t : Ticket K) : Input K VThe write was applied (a 2xx).
refused {K V : Type} (t : Ticket K) (why : String) : Input K VThe write was refused and not applied (a 4xx), for why.
lost {K V : Type} (t : Ticket K) : Input K VThe write got no answer (a timeout, a network failure, a 5xx): it may or may not have been applied.
read {K V : Type} (t : Ticket K) (v : V) : Input K VAn authoritative read's answer: what the server holds for the key now.
readFailed {K V : Type} (t : Ticket K) : Input K VA read got no usable answer.
retry {K V : Type} (k : K) : Input K VThe backoff timer retryIn asked for came due.
seen {K V : Type} (k : K) (v : V) : Input K VA value in a view the app fetched (a list, a page), which may be stale.
Out (K V : Type) : Type
What the table asks the app to do.
write {K V : Type} (t : Ticket K) (v : V) : Out K VSend a write of v for t.key, and answer it with t.
read {K V : Type} (t : Ticket K) : Out K VRead t.key's value from the server, authoritatively, and answer with t.
retryIn {K V : Type} (k : K) (ms : Nat) : Out K VFeed retry k in ms milliseconds (a timer).
rolledBack {K V : Type} (k : K) (r : Reason) : Out K Vk was rolled back; say so in words.
Definitions 36
firstBackoff : NatThe first retry of a failed read, in milliseconds.
maxBackoff : NatThe longest wait between retries.
nextBackoff (ms : Nat) : Nat
The next wait: double, at most maxBackoff.
isIdle {V : Type} : Phase V → Bool
isOpen {V : Type} : Phase V → BoolWhether a set may send a write now: nothing in flight or in doubt.
pending {V : Type} : Phase V → Option VThe value of the write in flight or in doubt, if any.
fresh {V : Type} (v : V) : Entry VA key the table hasn't heard of: v confirmed and shown.
send {V : Type} (e : Entry V) : Entry V × List (Act V)Send a write of want, as request seq + 1.
ask {V : Type} (e : Entry V) (ph : Phase V) : Entry V × List (Act V)Send a read, as request seq + 1, waiting in ph.
settle {V : Type} (same : V → V → Bool) (e : Entry V) :
Entry V × List (Act V)The server's value is known (e.server): rest if want is the same, else write toward it.
rollback {V : Type} (same : V → V → Bool) (e : Entry V)
(r : Reason) : Entry V × List (Act V)Show the server's value again, saying why if what is shown changes.
step {V : Type} (same : V → V → Bool) (e : Entry V) :
Ev V → Entry V × List (Act V)One key's step.
key {K V : Type} : Input K V → K
ev {K V : Type} : Input K V → Ev V
out {K V : Type} (k : K) : Act V → Out K VAn entry's action, as the table's output for key k.
empty {K V : Type} [Ord K] (dflt : V) (same : V → V → Bool) :
Table K VAn empty table.
get {K V : Type} [Ord K] (t : Table K V) (k : K) : Entry VKey k's entry: O(log n).
shown {K V : Type} [Ord K] (t : Table K V) (k : K) : VWhat is shown for k: want.
server {K V : Type} [Ord K] (t : Table K V) (k : K) : VThe last value the server confirmed for k.
inFlight {K V : Type} [Ord K] (t : Table K V) (k : K) : BoolA write for k is in flight.
inDoubt {K V : Type} [Ord K] (t : Table K V) (k : K) : Boolk's last write got no answer, and isn't settled yet.
settled {K V : Type} [Ord K] (t : Table K V) (k : K) : BoolNothing outstanding for k: no write in flight or in doubt, no read checking a view.
written {K V : Type} [Ord K] (t : Table K V) (k : K) : BoolWhether the person set k this session.
feed {K V : Type} [Ord K] (t : Table K V) (i : Input K V) :
Table K V × List (Out K V)One step: the input's key's entry steps, and its actions become outputs. O(log n).
run {K V : Type} [Ord K] (t : Table K V) :
List (Input K V) → Table K V × List (Out K V)Feed inputs in order; the outputs in order.
allSettled {K V : Type} [Ord K] (t : Table K V) : BoolEvery key with nothing outstanding. O(n).
size {K V : Type} [Ord K] (t : Table K V) : NatThe number of keys the table holds.
ind (b : Bool) : Nat
[b]: one if b.
count (c : Nat) (v w : Bool) : Nat
A count over a boolean key: c and v are the count and the person's own value from
the latest view (the count includes the person's own exactly when v), w is what is shown:
c − [v] + [w]. Never below zero (a Nat, count_ge), and exact whenever the view is
consistent (count_exact).
writes {V : Type} (as : List (Act V)) : NatThe writes among an entry's actions.
Budget {V : Type} (same : V → V → Bool) (e : Entry V) (s w : Nat) :
PropWrites w within sets s; and when the write outstanding isn't what is shown, a set is
yet to be written.
sets {V : Type} : Ev V → NatHow many sets an event is.
setsFor {K V : Type} [DecidableEq K] (k : K)
(is : List (Input K V)) : NatThe sets of k among some inputs.
writesFor {K V : Type} [DecidableEq K] (k : K)
(os : List (Out K V)) : NatThe writes for k among some outputs.
Calm {V : Type} (same : V → V → Bool) (e : Entry V) : PropWith no write in flight or in doubt (idle, or checking a view), what is shown is the
server's last confirmed value (by same).
Calm {K V : Type} [Ord K] (t : Table K V) : PropEvery key at rest shows the server's last confirmed value.
Theorems 25
beq {V : Type} [BEq V] [LawfulBEq V] : Same fun a b => a == bEquality, as same.
count_exact (c : Nat) (v w : Bool) (h : ind v ≤ c) : ↑(count c v w) = ↑c - ↑(ind v) + ↑(ind w)
count_ge (c : Nat) (v w : Bool) : ind w ≤ count c v w
count_view (o : Nat) (v r : Bool) : count (o + ind v) v r = o + ind r
Counts once settled. A view's count is other people's o plus the person's own [v].
When the key shows the server's value r (a settled key does, Server.converges), the count
shown is o + [r]: exactly the server's count when no one else acted since the view.
get_insert {K V : Type} [Ord K] [Std.TransOrd K] [Std.LawfulEqOrd K]
[DecidableEq K] (t : Table K V) (k j : K) (e : Entry V) :
{ entries := t.entries.insert k e, dflt := t.dflt, same := t.same }.get j =
if k = j then e else t.get j
get_feed {K V : Type} [Ord K] [Std.TransOrd K] [Std.LawfulEqOrd K]
[DecidableEq K] (t : Table K V) (i : Input K V) (k : K) :
(t.feed i).fst.get k =
if i.key = k then (Entry.step t.same (t.get i.key) i.ev).fst else t.get kWhat feed does to any key: the input's key steps; every other key is as it was.
get_feed_self {K V : Type} [Ord K] [Std.TransOrd K]
[Std.LawfulEqOrd K] [DecidableEq K] (t : Table K V) (i : Input K V) :
(t.feed i).fst.get i.key = (Entry.step t.same (t.get i.key) i.ev).fst
get_feed_ne {K V : Type} [Ord K] [Std.TransOrd K] [Std.LawfulEqOrd K]
[DecidableEq K] (t : Table K V) (i : Input K V) {k : K} (h : i.key ≠ k) :
(t.feed i).fst.get k = t.get kAn input touches only its key.
feed_same {K V : Type} [Ord K] [Std.TransOrd K] [Std.LawfulEqOrd K]
[DecidableEq K] (t : Table K V) (i : Input K V) : (t.feed i).fst.same = t.same
feed_dflt {K V : Type} [Ord K] [Std.TransOrd K] [Std.LawfulEqOrd K]
[DecidableEq K] (t : Table K V) (i : Input K V) : (t.feed i).fst.dflt = t.dflt
feed_out {K V : Type} [Ord K] [Std.TransOrd K] [Std.LawfulEqOrd K]
[DecidableEq K] (t : Table K V) (i : Input K V) :
(t.feed i).snd = List.map (Act.out i.key) (Entry.step t.same (t.get i.key) i.ev).snd
shown_set {K V : Type} [Ord K] [Std.TransOrd K] [Std.LawfulEqOrd K]
[DecidableEq K] (t : Table K V) (k : K) (f : V → V) :
(t.feed (Input.set k f)).fst.shown k = f (t.shown k)A set shows in its own step: after set k f, k shows f of what it showed.
feed_comm {K V : Type} [Ord K] [Std.TransOrd K] [Std.LawfulEqOrd K]
[DecidableEq K] (t : Table K V) (i j : Input K V) (h : i.key ≠ j.key) :
(∀ (k : K), ((t.feed i).fst.feed j).fst.get k = ((t.feed j).fst.feed i).fst.get k) ∧
((t.feed i).fst.feed j).snd = (t.feed j).snd ∧
((t.feed j).fst.feed i).snd = (t.feed i).sndInputs for different keys commute: in either order the table is the same at every key, and each input's outputs are the ones it gives alone, so the two orders' outputs are the same two lists, swapped.
refused_rollback {K V : Type} [Ord K] [Std.TransOrd K]
[Std.LawfulEqOrd K] [DecidableEq K] (t : Table K V) (k : K) (n : Nat) (why : String)
(w : V) (hp : (t.get k).phase = Phase.writing w) (hn : n = (t.get k).seq) :
(t.feed (Input.refused { key := k, seq := n } why)).fst.shown k = t.server k ∧
(t.feed (Input.refused { key := k, seq := n } why)).fst.server k = t.server k ∧
(t.feed (Input.refused { key := k, seq := n } why)).fst.settled k = trueA refusal rolls back in its step: when k's write n is in flight, refused for it
leaves k showing the server's value, which is unchanged.
seen_written {K V : Type} [Ord K] [Std.TransOrd K]
[Std.LawfulEqOrd K] [DecidableEq K] (t : Table K V) (k : K) (v : V)
(hw : t.written k = true) :
(t.feed (Input.seen k v)).fst.shown k = t.shown k ∧
(t.feed (Input.seen k v)).fst.server k = t.server kA view never moves a written key: seen leaves what a key written this session shows,
and the server value it holds, as they were.
feed_ext {K V : Type} [Ord K] [Std.TransOrd K] [Std.LawfulEqOrd K]
[DecidableEq K] (t u : Table K V) (h : ∀ (k : K), t.get k = u.get k)
(hs : t.same = u.same) (i : Input K V) :
(∀ (k : K), (t.feed i).fst.get k = (u.feed i).fst.get k) ∧ (t.feed i).snd = (u.feed i).snd
budget_step {V : Type} (same : V → V → Bool) (hs : Same same)
(e : Entry V) (s w : Nat) (h : Budget same e s w) (ev : Ev V) :
Budget same (step same e ev).fst (s + Ev.sets ev) (w + writes (step same e ev).snd)
writesFor_map {K V : Type} [Ord K] [Std.TransOrd K]
[Std.LawfulEqOrd K] [DecidableEq K] (k j : K) (as : List (Act V)) :
writesFor k (List.map (Act.out j) as) = if j = k then Entry.writes as else 0
budget_feed {K V : Type} [Ord K] [Std.TransOrd K] [Std.LawfulEqOrd K]
[DecidableEq K] (t : Table K V) (hs : Same t.same) (s w : K → Nat)
(h : ∀ (k : K), Entry.Budget t.same (t.get k) (s k) (w k)) (i : Input K V) (k : K) :
Entry.Budget t.same ((t.feed i).fst.get k) (s k + setsFor k [i])
(w k + writesFor k (t.feed i).snd)
budget_run {K V : Type} [Ord K] [Std.TransOrd K] [Std.LawfulEqOrd K]
[DecidableEq K] (is : List (Input K V)) (t : Table K V) (s w : K → Nat) :
Same t.same →
(∀ (k : K), Entry.Budget t.same (t.get k) (s k) (w k)) →
∀ (k : K),
Entry.Budget t.same ((t.run is).fst.get k) (s k + setsFor k is)
(w k + writesFor k (t.run is).snd)
writes_le_sets {K V : Type} [Ord K] [Std.TransOrd K]
[Std.LawfulEqOrd K] [DecidableEq K] (dflt : V) (same : V → V → Bool) (hs : Same same)
(is : List (Input K V)) (k : K) :
writesFor k ((empty dflt same).run is).snd ≤ setsFor k isNever more writes than sets. From an empty table, for any sequence of inputs (any
answers, in any order, duplicated or stale), the writes the table asks for k never outnumber
the person's sets of k.
calm_step {V : Type} (same : V → V → Bool) (hs : Same same)
(e : Entry V) (h : Calm same e) (ev : Ev V) : Calm same (step same e ev).fst
calm_empty {K V : Type} [Ord K] [Std.TransOrd K] [Std.LawfulEqOrd K]
[DecidableEq K] (dflt : V) (same : V → V → Bool) (hs : Same same) : (empty dflt same).Calm
calm_feed {K V : Type} [Ord K] [Std.TransOrd K] [Std.LawfulEqOrd K]
[DecidableEq K] (t : Table K V) (hs : Same t.same) (h : t.Calm) (i : Input K V) :
(t.feed i).fst.CalmAt rest, a key shows the server's value, after any input.
settled {K V : Type} [Ord K] [Std.TransOrd K]
[Std.LawfulEqOrd K] [DecidableEq K] {t : Table K V} (h : t.Calm) {k : K}
(hk : t.settled k = true) : t.same (t.shown k) (t.server k) = trueA settled key shows what the table last heard from the server.
Instances 18
instDecidableEqPhase {V✝ : Type} [DecidableEq V✝] : DecidableEq (Phase V✝)
instReprPhase {V✝ : Type} [Repr V✝] : Repr (Phase V✝)
instInhabitedPhase {a✝ : Type} : Inhabited (Phase a✝)
instDecidableEqEntry {V✝ : Type} [DecidableEq V✝] : DecidableEq (Entry V✝)
instReprEntry {V✝ : Type} [Repr V✝] : Repr (Entry V✝)
instDecidableEqReason : DecidableEq Reason
instInhabitedReason : Inhabited Reason
instReprReason : Repr Reason
instDecidableEqAct {V✝ : Type} [DecidableEq V✝] : DecidableEq (Act V✝)
instReprAct {V✝ : Type} [Repr V✝] : Repr (Act V✝)
instDecidableEqTicket {K✝ : Type} [DecidableEq K✝] :
DecidableEq (Ticket K✝)
instReprTicket {K✝ : Type} [Repr K✝] : Repr (Ticket K✝)
instInhabitedTicket {a✝ : Type} [Inhabited a✝] : Inhabited (Ticket a✝)
instReprOut {K✝ V✝ : Type} [Repr K✝] [Repr V✝] : Repr (Out K✝ V✝)
instDecidableEqOut {K✝ V✝ : Type} [DecidableEq K✝] [DecidableEq V✝] :
DecidableEq (Out K✝ V✝)
instRepr {K V : Type} [Ord K] [Repr K] [Repr V] : Repr (Table K V)
instBEqOfDecidableEq {K V : Type} [Ord K] [BEq K] [DecidableEq V] :
BEq (Table K V)Two tables are == when they hold the same entries and default; same is a function and
isn't compared. So an app's state that holds a table can derive BEq for its tests.
instInhabited {K V : Type} [Ord K] [Inhabited V] :
Inhabited (Table K V)An empty table of defaults, with every value the same as every other: for deriving Inhabited. A real table is Table.empty.