Record sign-out, forgetting a server, and holding several sessions

[iderex]

The issue this belongs to

Refs #114. It does not meet that issue's definition of done, and the last section
says which parts are untouched and why.

What changed

One decision record, docs/decisions/0114-signing-out-and-forgetting-a-server.md,
and its line in docs/decisions/README.md.

It separates signing out from forgetting a server. A sign-out ends one session:
the token leaves memory, the secret is forgotten through the interface in 0033
under the name 0041's construction gives it, the session's outstanding work ends
in named kinds from 0004, every other session keeps running, and all of that
completes on a device with no network. Telling the server is the only half that
may fail, and a sign-out that could not tell it reports that the token may still
be live there rather than refusing to complete. Forgetting a server is a second
act that does everything the first does and then removes every cache entry and
every queued action under the key space 0041 fixes for that server and that
account.

The queue survives a sign-out. 0005 already requires the answer to be the same
whether the sign-out was asked for or forced by a refused renewal, and it already
promises that a person who signs in again gets those positions reported in order,
so discarding them on the asked-for path would have made that promise depend on
which of the two ended the session.

The record also answers the two things landed records left pointing at this
issue with nothing behind them. 0042 says a route by which a client clears a
store it supplied is decided nowhere; that route is the second act. 0041 says
removal by key space needs the core's own index because 0040 gives the store no
listing and a digest is not reversible; the record says what the removal does
when that index is not there, which is to report how many entries it could not
reach rather than to report a removal it did not make.

What failure it prevents

The one that has a name and a date attached to it here is the first: sign-out is
written by whoever needs it first, which is the test in #41 that signs in, signs
out and signs in as somebody else. A sign-out written to make that test pass
removes the cache, because the test is about the cache, and 0006's argument for
keeping entries across a sign-in is then reversed by a fixture rather than by an
argument.

Three more, each with a cheap default that is wrong and nothing that notices.
A sign-out that waits on the server before dropping the token in memory leaves a
token in memory whenever the network is bad, which is the condition under which
somebody is most likely to hand the device to somebody else. A sign-out that
discards the queue loses actions a person took, silently, in the one act where
throwing things away looks like the point. A sign-out that cancels a lane rather
than a session stops the other account's screen on a television with two people
signed in, and on a machine with one account it is invisible.

Two of those cannot be corrected afterwards. An action discarded at sign-out is
gone from the only device that held it. A token left live at a server because
nobody reported that it was not ended stays live until the server decides.

Where this departs from the issue

The issue's list of the parts of a sign-out includes the cache entries removed
through the keying in #41, and its third condition asks for a test proving that
nothing from that identity is readable afterwards from memory, the cache or the
secret store. Two landed records answer the other way. 0006 says signing out does
not by itself destroy the cache and that what a sign-out removes is the token.
0068 says cache entries survive a sign-out, deliberately, and that a caller who
wants them gone asks for that.

The record follows the two landed records and puts the removal in the second act.
So the issue's third condition reads against that act rather than against a
sign-out, and as written against sign-out alone it cannot be met without
superseding 0006 and 0068.

Evidence

The record names no path that does not resolve, and the index line it adds is
checked by the same run:

$ bash .github/doc-paths/doc-paths.sh check
Every fixture held. The rules the gate applies are the rules these fixtures ran.

Documents read: every tracked file whose name ends in .md.
Compared against: 63 tracked paths and the directories holding them.

-- names-a-path-that-resolves
ok    45 document(s), 49 named path(s) resolved, 0 excused as examples

Every path these documents name resolves against the tracked set.

The record carries no non-ASCII:

$ git grep -nIP '[^\x00-\x7F]' -- docs/decisions/0114-signing-out-and-forgetting-a-server.md ; echo "exit=$?"
exit=1

The size of the change:

$ git show --stat --oneline HEAD
11f67e8 Record sign-out, forgetting a server, and holding several sessions
 .../0114-signing-out-and-forgetting-a-server.md    | 332 +++++++++++++++++++++
 docs/decisions/README.md                           |   1 +
 2 files changed, 333 insertions(+)

Both runs above were made at 11f67e8324c5a5a0f892cb25d372b32eb321e329, which is
this branch's head.

What this does not cover

It adds no guard, no check and no test, so there is nothing here whose direction
was watched. Nothing in this repository refuses a violation of anything the
record decides, and nothing will until there is code.

Three of the issue's four conditions are untouched and are not reachable in this
tree. A test signing in against two servers at once, a test signing out of one
and proving the second is untouched, and a test proving that nothing from an
identity is readable afterwards are all statements about running code. There is
no language chosen, no build and no test command here to assert them against.

The record's numbers are not its own. It restates none of the intervals in 0007
or 0038 and adds no new one, so there is no number in it that needed a
measurement. Where it says an attempt is bounded it points at those records
rather than repeating a value.

Nothing here was run against a server, a store or a device. Every claim about
what a platform does is inherited from the records cited rather than measured.

Who has read it

Nobody other than the author has read this change. The evidence above stands in
place of a review rather than beside one.