diff --git a/docs/decisions/0114-signing-out-and-forgetting-a-server.md b/docs/decisions/0114-signing-out-and-forgetting-a-server.md new file mode 100644 index 0000000..73a4a34 --- /dev/null +++ b/docs/decisions/0114-signing-out-and-forgetting-a-server.md @@ -0,0 +1,332 @@ +# 0114. Signing out, forgetting a server, and holding several sessions + +Date: 2026-08-13 + +Status: accepted. Supersedes nothing. Superseded by nothing. + +Issue: #114 + +## The decision + +Signing out and forgetting a server are two acts rather than one: a sign-out ends +one session, drops its token from memory, forgets its secret through 0033, +resolves that session's outstanding work into named kinds from 0004, leaves every +other session running and completes on a device with no network; forgetting a +server is a second act a client asks for, which does everything a sign-out does +and then removes every cache entry and every queued action under the key space +0041 fixes for that server and that account; and the queue survives a sign-out, +because an undelivered action is the one thing a person did that has no copy +anywhere else. + +## Two acts, and why they are not one + +Every client that was not told they differ collapses them into one button, and +which of the two that button does is then decided by whoever wrote it. + +The two answer different questions. Somebody signing out is saying that the next +person to pick this device up must not be them. Somebody forgetting a server is +saying that this device should stop holding anything about that server at all. +The first is ordinary and happens on a television in a house every evening. The +second is what a person does before they sell the device, or when they have +finished with a server they were only visiting. + +If sign-out did both, then signing back in on a device somebody already used +refetches the whole library over whatever connection they have, and 0006's +argument for keeping entries across a sign-in is lost. If forgetting a server did +only what a sign-out does, then there is no act at all that removes what the core +asked to be kept, and 0068's promise to an operator that they can have it removed +has nothing behind it. + +So both exist, they are named separately in the interface, and the second is +strictly the first plus removal. + +## What a sign-out does + +It takes a session, which 0005 fixes as one server, one account and one device +identity together, and it does five things. + +The token leaves memory. Nothing further is sent under it by this core. + +The secret is forgotten through the interface in 0033, under the name that +record derives from 0041's construction. Forgetting one that is not there +succeeds, so a sign-out on a session whose secret was never written is not a +failure. + +The session's outstanding work is resolved, in the terms of the next section. + +The session moves to signed out and stays addressable. A signed-out session is +still a server, an account and a device identity the client can name, which is +what a later sign-in and a later forget both need, and 0033 already requires the +client rather than the core to be holding that triple. + +The server is told, as one ordinary request under the bounds 0007 and 0038 +already fix, and it is the only half that may fail. A token this core stopped +using is still a token the server accepts until the server decides otherwise, so +telling it is worth attempting and worth reporting. Where the attempt did not +succeed the client is told through 0100, with the fact that the token may still +be live at the server, because that is a thing an operator can act on from the +server's own side and cannot act on if nobody said it. + +The first four happen whatever the network is doing. A sign-out on a train is a +sign-out, and it reports that the server was not told rather than refusing to +complete. Reversing that order, so that the local half waits on the server half, +produces the failure this whole act exists against: a person hands the device to +somebody else believing they signed out, and the token is still in memory because +a request timed out. + +A sign-out of a session that is already signed out succeeds and changes nothing. +A sign-out forced by a refused renewal in 0034 reaches exactly this state, with +the server half skipped because the server has already refused that token, which +is what 0005 requires when it says the answer must be the same whether the +sign-out was asked for or forced. + +## What a sign-out does not do + +It does not touch any other session. Not another account on the same server, not +the same account on another server, and not the same account on the same server +from a second device, which 0005 already fixes as a second session because the +server issued a second token and may end either one alone. + +It does not remove cache entries. 0006 and 0068 both landed this direction with +their reasons, and this record follows them rather than reopening them: the +entries are keyed per server, per account and per device, so leaving them costs +nobody else's privacy, and signing back in on a device somebody already used is +the case the cache exists for. This issue's own list of the parts of a sign-out +puts cache removal inside it, and the two landed records are the later answer; +what removes those entries is the second act below. + +The consequence of that is stated here rather than left to be found. A cache read +needs no token, which is what 0046's cold start depends on, so a signed-out +account's library is still servable to whoever names that session on that device. +0046 already says as much, in the sentence that naming a session is the act that +exposes its cache and that 0041 keeps two accounts apart while doing nothing to +keep one account's entries from whoever picked the device up. This record does +not weaken that and does not improve it: it is the reason the second act exists, +and a client whose sign-out button has to mean the stronger thing calls the +second one. + +It does not stop playback. 0005 guarantees that a token dying mid-playback does +not interrupt what somebody is watching, and an asked-for sign-out is not a +reason to break that guarantee either. The stream is being read by the platform's +own player against the address handed over in #111, and this core does not have a +way to stop it. What may happen is that the address stops working, because the +server was told the token is finished; that is the server's answer to the player +rather than something the core did, and the record says so here rather than +leaving a client to discover it as a defect. + +It does not end sessions elsewhere. What a sign-out reaches is this device. + +## Work in flight + +Four kinds of work can be running when a sign-out arrives, and each ends in a +named state rather than in silence. 0009 already refuses reporting a cancelled or +undelivered thing as something it is not, and this is that rule applied to one +moment. + +A request already sent on that session is cancelled and ends as `cancelled` from +0004. An answer that arrives afterwards is discarded rather than delivered, and +it is not written to the cache, because it was fetched under a session that has +ended. + +A decode running for that session ends the same way, at the step boundary 0009 +and 0115 already fix, since a decoder is not interruptible at an arbitrary +instruction. Bytes already handed to a caller are the caller's and are not +reached, which is the same boundary 0042 draws for eviction. + +A read or a write already begun through the byte store completes. That is 0115's +rule and its reason is that the store is the client's own code, and it holds here +without exception: a sign-out does not abandon a call inside somebody else's +implementation. + +A queued action stays queued, which is the section below. + +Cancelling by session is what makes this possible, and it is the part that will +be got wrong. 0009 gives the core two lanes shared by every session, so the unit +of work on a lane carries the session it belongs to and the sign-out cancels that +set and no other. A sign-out that cancelled a lane's work would stop the other +account's tile wall on a television with two people signed in, and the person who +lost their screen did nothing. + +## The queue survives, and what that costs + +0047 holds one durable queue per session, and its contents are the actions +somebody took that the server has not been told about yet. 0068 names it as the +one piece of this data with no copy on the server. + +So a sign-out keeps it. A later sign-in to the same server, account and device +finds the queue where it was, in its own order, and drains it before anything +else is sent, which is exactly what 0005 already promises for the sign-out that a +refused renewal forces. Keeping the two answers identical is what stops the +queue's guarantee from depending on which of the two ended the session. + +Before the server is told, and only while there is a session to send under, the +sign-out attempts a drain. It is an ordinary attempt under 0007 and 0038 and it +adds no number of its own: what drains, drains, and what does not stays queued. +A sign-out is not allowed to become slow because somebody has a fortnight of +positions waiting, and it is not allowed to discard them either. + +What that costs is a queue nobody comes back for. A person who signs out of a +server and never signs in again leaves entries under 0047's bound that will not +be delivered and will not expire, because 0047 refuses to expire an entry by age +and gives the reason. That cost is real, it is bounded by the count 0047 fixes, +and the act that removes it is the next section. Naming it here is the point: the +alternative is discovering it as a store that holds something forever for a +session that is finished. + +## Forgetting a server + +Everything a sign-out does, and then removal. + +Every cache entry under the key space for that server and that account, in both +tiers of 0054, which 0041 makes a well defined set: every entry whose first three +parts are that server, that account and that device identity, and no other. + +The queue for that session in 0047, including its standing count of what it +dropped. + +Whatever the core keeps to find those entries, which is the index 0042 holds for +eviction. 0040 gives the store no listing and 0041's keys are digests, so that +index is the only route to the set, and a removal that left it holding rows for +entries it has removed would leave the bound counting bytes that are gone. + +Removal goes through the same store interface as everything else. The core +removes what it wrote, through 0040's remove operation, one entry at a time. It +does not reach past the interface, it does not ask the client to delete a +directory, and it makes no claim about what an uninstall leaves behind, which +0068 already refuses to promise and this record does not promise either. + +The act is per server and account rather than per server, because two people on +one television are two key spaces and one of them forgetting a server is not the +other one asking for anything. + +## When a removal cannot be completed + +The index is the single point of failure and the record says so rather than +assuming it is there. + +Where the index is absent or was refused by 0105, the set is not reachable, and +the core reports that it removed what it could and names how many entries it +could not reach. It does not report a removal it did not make. This is 0068's +promise meeting its limit in the open, and the honest report is worth more than a +success value, because an operator who asked for their data to be removed and was +told it was gone has no reason ever to ask again. + +Where a removal fails part way, because the store answered `storage-unavailable` +from 0004, what has been removed stays removed and the act reports how far it +reached. Repeating it is safe, since removing an entry that is not there succeeds +under 0040's rule and the index says what is left. + +The local half of the sign-out inside a forget still completes in both cases. A +device that cannot reach its own store is not a device where somebody should +remain signed in. + +## Holding several at once + +0005 already fixes that the core holds any number, that every call names its +session, and that there is no ambient current session a second call can change +underneath the first. This record adds what holding several requires of the acts +above, and one thing about the set itself. + +The durable list of sessions is the client's, not the core's. 0033's store cannot +be asked what it holds and 0040's cannot either, so nothing in the core can +enumerate what was signed in on a previous run, and 0115 already makes restoring +a session a call the client makes naming the triple it wants. The core knows the +sessions it was told about during this run and no others. + +The consequence is that a client which loses its own list leaves both a secret +and a key space that nothing will ever name again. 0033 already states that cost +for the secret. It is the same cost for the cache, it is the reason forgetting a +server is a call rather than something the core does on its own, and a client +that lost the list clears the platform's own stores itself. + +## Why this is written down before the code + +Sign-out is written by whoever needs it first, and that is #41's own test, which +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 the +result is 0006's argument reversed by a fixture rather than by an argument. + +Each of the other three parts has a cheap default that is wrong in a way nothing +notices for a long time. A sign-out that waits on the server before dropping the +token in memory leaves a token in memory whenever a network is bad, which is the +one 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, +which is the failure 0047 exists against, arriving through 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 person's screen, and on a developer's machine with +one account it is invisible. + +Two of the four 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, and no +later change to the core reaches it. + +None of this has happened here, because there is no session, no queue and no +store in this tree. The records quoted above are not all of the ones that named +this issue as the one that would answer them, and the set moves, so it is derived +rather than counted here: + + $ git grep -l '#114' -- docs/decisions + +## Alternatives, and what each cost + +One act, where signing out removes everything. It is the answer this issue's own +list assumes, it needs no second name in the interface, and it is what a person +who has just read a privacy page expects. It costs 0006's whole argument for +keeping entries across a sign-in, so every sign-in on a shared television refetches +a library over the connection the cache exists to avoid, and it makes the cheap +act destructive in a way that cannot be undone by signing back in. + +One act, where signing out removes nothing but the token, with no second act at +all. The smallest surface, and it is what the core can do without an index. It +costs 0068's promise to an operator outright, since nothing then removes what the +core asked to be kept, and the first client to want it builds its own removal +against a key space it cannot compute. + +Removing the cache lazily, by marking the key space dead and letting 0042's bound +evict it in time. No index walk, no partial removal to report, and the entries do +go eventually. It costs the promise its meaning: data removed when the cache +happens to fill is data still on the device for as long as somebody does not use +the application, which is exactly the period after they stopped using it. + +Discarding the queue at sign-out, on the argument that a session that ended has no +business holding work. Simpler, and it removes the queue-nobody-comes-back-for +cost named above. 0005 already refuses it by naming it as its own reversal +condition, and what it costs is a person's actions, silently, in the case where +they signed out on a train and back in the next morning. + +Waiting for the server to confirm before completing the local half. It makes the +report simple, since either the token is ended everywhere or the sign-out did not +happen. It costs the case the act is for, because a device with no network then +cannot sign out at all. + +Letting the core keep its own list of sessions so that it can offer one and clean +up after a client that lost theirs. It removes the orphan cost above. It costs a +durable list of servers and accounts written by the core somewhere it chose, +which 0101 refuses, and it needs an enumeration over stores that 0033 and 0040 +both deliberately do not have. + +## What would reverse this + +A client is measured, on the harness in #65, to spend longer walking the index at +a forget than an operator will wait on the smallest supported device. Removal by +key space then needs something the store can answer, the store grows an +operation, and that is 0040's reversal and this record's together. + +A supported server line offers no way to end a token from the device. The server +half above is then not merely best effort, it is absent, and what replaces this +record says what an operator is told instead, since the current text promises a +report about an attempt that would never be made. + +A second act turns out not to be enough, named with the case that cannot be +expressed. The candidate is a person wanting their playback positions removed +from the device while staying signed in, which is neither of the two acts here. +Then the removal is expressed per kind rather than per session and this record is +superseded rather than extended, because the argument for two acts is the +argument against a third. + +#105 refuses an index in ordinary use rather than after a version change, so the +report about a removal that could not be completed becomes the common answer +instead of the edge. That is evidence the index is the wrong place to hold the +only route to a key space, and what replaces this record says what holds it +instead. diff --git a/docs/decisions/README.md b/docs/decisions/README.md index 9ed01e2..73d777c 100644 --- a/docs/decisions/README.md +++ b/docs/decisions/README.md @@ -40,4 +40,5 @@ allocated, and why a record is superseded rather than edited are in - [0102. The clocks every deadline is measured against](0102-the-clocks-every-deadline-is-measured-against.md) - [0105. An entry this version did not write, and one that was not finished](0105-an-entry-this-version-did-not-write.md) - [0112. Where the platform decoder begins](0112-where-the-platform-decoder-begins.md) +- [0114. Signing out, forgetting a server, and holding several sessions](0114-signing-out-and-forgetting-a-server.md) - [0115. Creating the core, stopping it, and a host that suspends it](0115-creating-and-stopping-the-core.md)