Cairn
Docs
Claims
Blog
Packages
Claims ยท cairn_atproto
cairn_atproto 0.1.0: claims
Everything cairn_atproto 0.1.0 claims a person can do and see, and what holds, by place, each with its evidence.
1 assumed9 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 |
Invariants
What holds in every state the app can reach.
| Id | Claim | Reads as |
|---|---|---|
cairn_atproto^5 | 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^6 | A call is sent at most twiceEvery call the app makes is sent at most twice. | proved |
cairn_atproto^7 | 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^8 | Signed out, no secret is sentWhile signed out or signing in, no request carrying a Keychain secret is issued. | proved |
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 |
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 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). By construction; checked by the trusted-base fuzz. | assumed |