Package ยท iamnbutler
cairn_atproto
The AT Protocol (Bluesky) for Cairn apps: XRPC, lexicon decoders and a proved session machine
- Kind
- Library
- Owner
- iamnbutler
- Version
- 0.1.1
- Published
- Oct 25, 2026 by iamnbutler
- Commit
e7b834944a4aatv0.1.1- Toolchain
leanprover/lean4:v4.35.0- License
- MIT
- Claims
- 10 active
Use it
With the cairn tool:
cairn add cairn_atproto@^0.1.1Which writes cairn.toml, and the lakefile line that it keeps in step:
[dependencies]
cairn_atproto = "^0.1.1"cairn.toml[[require]]
name = "cairn_atproto"
scope = "iamnbutler"
version = "^0.1.1"lean/lakefile.tomlDepends on
cairn^0.2.5cairn_json^0.1.0
Versions
| Version | Published | Commit | Claims | Docs |
|---|---|---|---|---|
| 0.3.0 | Oct 26, 2026 | 11db1badce | 28 active5 retired | docs |
| 0.2.0 | Oct 25, 2026 | a015e7b1fc | 11 active5 retired | docs |
| 0.1.1 | Oct 25, 2026 | e7b834944a | 10 active | docs |
| 0.1.0 | Oct 25, 2026 | d2c27568e4 | 10 active | docs |
What changed in 0.1.1
No claim is new, retired or moved since 0.1.0.
Claims in 0.1.1
Every id this package has issued, as its claims.lock held them at this version. An id never moves or changes meaning: the registry refuses a version that drops, renumbers or redefines one. The claim pages show each claim by place, with what it does and its evidence.
| Id | Kind | Status | Claim |
|---|---|---|---|
cairn_atproto^1 | move | active | Sign in |
cairn_atproto^2 | move | active | Resume |
cairn_atproto^3 | move | active | Make a call |
cairn_atproto^4 | move | active | Sign out |
cairn_atproto^5 | invariant | active | One refresh at a time |
cairn_atproto^6 | invariant | active | A call is sent at most twice |
cairn_atproto^7 | invariant | active | A second send only after a successful refresh |
cairn_atproto^8 | invariant | active | Signed out, no secret is sent |
cairn_atproto^9 | invariant | active | A failed refresh ends the held calls |
cairn_atproto^10 | assume | active | No Lean value holds a token |