What ^1100 does on press.

The human half of claim ^1100.

To show every handler of ^1100 keeps a property, show it in the move's own terms.

^1100 Set a value, on press: whenever the move is enabled, apply meets post.

^1100 Set a value (move)

Does: The person flips key k (likes or unlikes it).

Sees: Key k shows the new value in that step, whatever is in flight.

What must follow ^1100 Set a value on press: Key k shows the new value in that step, whatever is in flight.

What ^1101 does on press.

^1101 The server handles a request, on press: whenever the move is enabled, apply meets post.

To show every handler of ^1101 keeps a property, show it in the move's own terms.

^1101 The server handles a request (move)

Does: The server handles the i-th packet in the network: applies a write (its answer becomes acked) or answers a read with what it holds.

Sees: Nothing changes on screen: the table hears nothing until an answer arrives.

The human half of claim ^1101.

What must follow ^1101 The server handles a request on press: Nothing changes on screen: the table hears nothing until an answer arrives.

What must follow ^1102 The server refuses a request on press: Neither the screen nor the server changes; the refusal is on its way.

What ^1102 does on press.

To show every handler of ^1102 keeps a property, show it in the move's own terms.

The human half of claim ^1102.

^1102 The server refuses a request (move)

Does: The server refuses the i-th packet in the network, and changes nothing.

Sees: Neither the screen nor the server changes; the refusal is on its way.

^1102 The server refuses a request, on press: whenever the move is enabled, apply meets post.

What ^1103 does on press.

^1103 An answer arrives (move)

Does: The network delivers the i-th packet, an answer or a view, to the table.

Sees: The table settles, rolls back, retries or takes the view; the server is unchanged.

What must follow ^1103 An answer arrives on press: The table settles, rolls back, retries or takes the view; the server is unchanged.

To show every handler of ^1103 keeps a property, show it in the move's own terms.

The human half of claim ^1103.

^1103 An answer arrives, on press: whenever the move is enabled, apply meets post.

To show every handler of ^1104 keeps a property, show it in the move's own terms.

The human half of claim ^1104.

^1104 A request or answer is lost, on press: whenever the move is enabled, apply meets post.

^1104 A request or answer is lost (move)

Does: The network loses the i-th packet, before or after the server handled it; the table hears lost (a write) or readFailed (a read).

Sees: A lost write puts its key in doubt and sends a read; the server is unchanged.

What ^1104 does on press.

What must follow ^1104 A request or answer is lost on press: A lost write puts its key in doubt and sends a read; the server is unchanged.

^1105 A retry comes due, on press: whenever the move is enabled, apply meets post.

^1105 A retry comes due (move)

Does: Key k's backoff timer fires.

Sees: A key waiting after a failed read sends the next read; the server is unchanged.

The human half of claim ^1105.

What must follow ^1105 A retry comes due on press: A key waiting after a failed read sends the next read; the server is unchanged.

What ^1105 does on press.

To show every handler of ^1105 keeps a property, show it in the move's own terms.

What must follow ^1106 A view is fetched on press: Nothing changes until the view arrives.

The human half of claim ^1106.

^1106 A view is fetched, on press: whenever the move is enabled, apply meets post.

To show every handler of ^1106 keeps a property, show it in the move's own terms.

What ^1106 does on press.

^1106 A view is fetched (move)

Does: The app fetches a view of key k: what the server holds now, delivered whenever (^1103).

Sees: Nothing changes until the view arrives.

The human half of claim ^1107.

Every message from the world preserves ^1107.

^1107 holds in the initial state.

Every update, so every move, preserves ^1107.

^1107 A set shows in its own step: Whatever is in flight or in doubt, setting a key to f of what it shows makes it show exactly that in the same step: what is shown is want, and a set changes want at once.

^1107 holds in every state reachable by actions and messages from the world.

^1107 A set shows in its own step (invariant)

Whatever is in flight or in doubt, setting a key to f of what it shows makes it show exactly that in the same step: what is shown is want, and a set changes want at once.

^1107 holds in every reachable state.

^1108 holds in the initial state.

^1108 At most one write in flight per key (invariant)

For every key, at most one write is in the network, before or after the server handled it: a set while one is in flight only changes what is shown.

^1108 holds in every reachable state.

The human half of claim ^1108.

^1108 holds in every state reachable by actions and messages from the world.

^1108 At most one write in flight per key: For every key, at most one write is in the network, before or after the server handled it: a set while one is in flight only changes what is shown.

Every update, so every move, preserves ^1108.

Every message from the world preserves ^1108.

^1109 Never more writes than sets: For every key, the writes the table has sent never outnumber the person's sets of it, whatever answers came back in whatever order: a lost write is read back, never sent again blind.

The human half of claim ^1109.

^1109 holds in every state reachable by actions and messages from the world.

Every update, so every move, preserves ^1109.

Every message from the world preserves ^1109.

^1109 Never more writes than sets (invariant)

For every key, the writes the table has sent never outnumber the person's sets of it, whatever answers came back in whatever order: a lost write is read back, never sent again blind.

^1109 holds in the initial state.

^1109 holds in every reachable state.

The human half of claim ^1110.

^1110 A refusal rolls back in its step: When a key's write in flight is refused, the key shows the server's last confirmed value in that step, that value is unchanged, and nothing is outstanding for the key.

Every update, so every move, preserves ^1110.

Every message from the world preserves ^1110.

^1110 holds in the initial state.

^1110 holds in every state reachable by actions and messages from the world.

^1110 A refusal rolls back in its step (invariant)

When a key's write in flight is refused, the key shows the server's last confirmed value in that step, that value is unchanged, and nothing is outstanding for the key.

^1110 holds in every reachable state.

Every update, so every move, preserves ^1111.

Every message from the world preserves ^1111.

^1111 holds in the initial state.

^1111 holds in every reachable state.

The human half of claim ^1111.

^1111 holds in every state reachable by actions and messages from the world.

^1111 Settled keys show what the server holds (invariant)

Against a server that is a register per key with idempotent writes, for any sequence of sets and any interleaving of replies (each acknowledged, refused, or lost before or after the server applied it, delivered in any order, with views fetched at any time), every key with nothing in flight and nothing in doubt shows what the server holds. So once every reply is in, every key does.

^1111 Settled keys show what the server holds: Against a server that is a register per key with idempotent writes, for any sequence of sets and any interleaving of replies (each acknowledged, refused, or lost before or after the server applied it, delivered in any order, with views fetched at any time), every key with nothing in flight and nothing in doubt shows what the server holds. So once every reply is in, every key does.

^1112 Replies for different keys commute (invariant)

Two inputs about different keys, in either order, leave the table the same at every key, and each gives the outputs it gives alone, so the two orders' outputs are the same two lists swapped.

The human half of claim ^1112.

^1112 holds in the initial state.

^1112 holds in every reachable state.

^1112 Replies for different keys commute: Two inputs about different keys, in either order, leave the table the same at every key, and each gives the outputs it gives alone, so the two orders' outputs are the same two lists swapped.

Every update, so every move, preserves ^1112.

^1112 holds in every state reachable by actions and messages from the world.

Every message from the world preserves ^1112.

The human half of claim ^1113.

Every message from the world preserves ^1113.

^1113 holds in the initial state.

^1113 holds in every reachable state.

Every update, so every move, preserves ^1113.

^1113 A settled count is the server's (invariant)

For a view whose count is other people's o plus 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. The count shown, c − [v] + [shown], is never below zero, and never below the person's own [shown].

^1113 A settled count is the server's: For a view whose count is other people's o plus 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. The count shown, c − [v] + [shown], is never below zero, and never below the person's own [shown].

^1113 holds in every state reachable by actions and messages from the world.

Every update, so every move, preserves ^1114.

^1114 holds in every reachable state.

^1114 holds in every state reachable by actions and messages from the world.

The human half of claim ^1114.

^1114 A view never moves a written key: A value in a view the app fetched, which may be stale (fetched before a write, or from a server that hasn't indexed it yet), never changes what a key written this session shows, or its confirmed value.

^1114 holds in the initial state.

^1114 A view never moves a written key (invariant)

A value in a view the app fetched, which may be stale (fetched before a write, or from a server that hasn't indexed it yet), never changes what a key written this session shows, or its confirmed value.

Every message from the world preserves ^1114.