Cairn
Docs
Claims
Blog
Packages
Claim ยท cairn_atproto 0.3.0
cairn_atproto^15 No Lean value holds a token
An assumption of cairn_atproto 0.3.0.
- Id
cairn_atproto^15- Kind
- assume
- Reads as
- assumed
- Version
- 0.3.0
What it says
No 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.
Evidence
| assumed | Stated, not proved. The proofs rely on it. | |
| fuzzed | Not shown yet: the trusted-base fuzzer's check atproto.no-token held. A CI step will publish it (#95). | |
Where it's defined
- Declaration
CairnAtproto.Claims.noTokens- Module
CairnAtproto.Claims- Source
lean/CairnAtproto/Claims.lean:162atv0.3.0- Statement hash
-
Ledger
cairn_atproto^15 is active in this version's claims.lock. An id never moves or changes meaning.