Cairn
Docs
Claims
Blog
Packages
Claims ยท cairn_atproto
cairn_atproto 0.2.0: claims
Everything cairn_atproto 0.2.0 claims a person can do and see, and what holds, by place, each with its evidence.
5 retired1 assumed10 proved
Not in a place
Moves and flows that name no place.
| Id | Kind | Claim | Reads as |
|---|---|---|---|
cairn_atproto^1 | move | Sign inSign in with a handle and an app password. | proved |
cairn_atproto^2 | move | ResumeLaunch with a saved service: resume the session the Keychain items hold. | proved |
cairn_atproto^3 | move | Make a callMake an XRPC call (here getTimeline) with id k. | proved |
cairn_atproto^4 | move | Sign outSign out. | proved |
cairn_atproto^16 | move | Cancel a callCancel the app's call k (in flight or held for a refresh). | proved |
Invariants
What holds in every state the app can reach.
| Id | Claim | Reads as |
|---|---|---|
cairn_atproto^5 | One refresh at a time | retired |
cairn_atproto^6 | A call is sent at most twice | retired |
cairn_atproto^7 | A second send only after a successful refresh | retired |
cairn_atproto^8 | Signed out, no secret is sent | retired |
cairn_atproto^9 | A failed refresh ends the held callsWhen the refresh in flight fails every held call is answered in that step; when it is refused both Keychain items are forgotten and the held calls are answered signedOut. Calls are held only while a refresh is in flight. | proved |
cairn_atproto^11 | One refresh at a timeAt most one refreshSession request is in flight: a call answered ExpiredToken while one is in flight joins it. | proved |
cairn_atproto^12 | A call is sent at most twiceEvery call the app makes is sent at most twice. | proved |
cairn_atproto^13 | A second send only after a successful refreshA call that was sent before is sent again only in the step a refresh in flight gets a 2xx session reply. | proved |
cairn_atproto^14 | Signed out, no secret is sentWhile signed out or signing in, no request carrying a Keychain secret is issued. | proved |
Assumptions
What the proofs rely on and nothing proves: the host, the OS and the hardware behaving as stated.
CairnAtproto.Claims
| Id | Claim | Reads as |
|---|---|---|
cairn_atproto^10 | No Lean value holds a token | retired |
cairn_atproto^15 | No Lean value holds a tokenNo type in cairn_atproto holds an access or refresh token: the session state has DIDs, handles, service URLs, request ids and the app's calls; SessionInfo has no token field and its decoder never reads accessJwt or refreshJwt (SessionInfo.ofJson_replaceTokens). Tokens go from the host's capture to the Keychain and back as a request's secret header (Cairn's Request.http). By construction; checked by this package's make fake-fuzz (atproto.no-token), which runs the session against the fake PDS and its host and searches every Lean value for the fake's token markers. | assumed |