Single-flight OAuth token refresh

[kmatzen]

getAccessToken read-modify-wrote a single localStorage record across an await, with no mutex. Nine independent call sites can overlap freely — autosave firing while the user clicks Share, the project list loading thumbnails during a save — and each issued its own refresh, writing back a record snapshotted before its await.

TLA+ models of both protocols are in specs/. TLC's counterexample against the old design: two callers snapshot the same record, both refresh, the first succeeds and advances the record, and the second then writes based on a read the record has already moved past. When that second call fails — a blip, a 5xx, a rotated refresh token — its write is writePersisted(null), signing the user out mid-save and discarding the session the first caller just established.

Changes

• Single-flight. The first caller needing a refresh stores its promise; concurrent callers await that same promise. At most one refresh is ever in flight, so no caller can be signed out by another's failure.
• Only a definitive auth failure clears the session. RefreshError carries a definitive flag, set for 400 invalid_grant and 401. A network error or 5xx now rejects the caller but leaves the record intact — previously any failure wiped it, turning a dropped packet into a forced re-auth.
• The refresh re-reads storage after its await rather than spreading its pre-await snapshot, so a logout or a second tab's sign-in landing mid-refresh is no longer resurrected.

Verification

check	result
tsc --noEmit	exit 0
new tests, this branch	7/7 pass
new tests, old design	(reported below)

Honest notes on the spec

Two things worth stating rather than glossing:

My first property was wrong. I initially wrote NoSpuriousLogout as "a successful refresh is never followed by a logout". That is too strong — a later, sequential refresh may legitimately discover a dead token and sign out correctly. TLC's "violation" of it was the trivial sequential path, not the concurrency bug, so that first counterexample proved nothing. The corrected property is NoStaleOverwrite: no caller writes based on a read the record has already moved past.

A precedence bug made a property pass vacuously. staleWrite' = staleWrite \/ IsStale(c) parses as (staleWrite' = staleWrite) \/ IsStale(c), since = binds tighter than \/. In the old-design spec TLC flagged an unassigned variable; in the fixed spec it silently meant the flag could never be set, so the property passed for no reason. Both are parenthesized now.

The fixed model's NoStaleOverwrite is close to structural. Single-flight makes staleness impossible by construction, and my vacuity check (removing the lock) deadlocks the model rather than violating that property — so I cannot demonstrate it has independent teeth there. The properties that do are AtMostOneRefreshInFlight and WaitersDoNotRefresh; removing the lock violates the former.

Related

Independent of #50 — different files, no overlap. Both add to specs/, but disjoint files.

🤖 Generated with Claude Code

[kmatzen]

Old-design discrimination check: the 7 tests run against main's getAccessToken give 4 failed / 3 passed.

The three that pass are behaviors both designs share (definitive-failure signout, sequential refresh, skip-when-not-near-expiry). The four that fail are exactly the defects:

test	failure on old design
issues one refresh for concurrent callers	fired three
does not sign the user out when a concurrent caller fails	second caller rejected, session wiped
keeps the session on a transient failure	record wiped by a 502
does not resurrect a record removed during the refresh	resurrected the removed record

So these are regression tests, not tests that merely happen to pass.