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.0
- Published
- Oct 25, 2026 by iamnbutler
- Commit
d2c27568e404atv0.1.0- Toolchain
leanprover/lean4:v4.35.0- License
- MIT
- Claims
- 10 active
Use it
With the cairn tool:
cairn add cairn_atproto@^0.1.0Which writes cairn.toml, and the lakefile line that it keeps in step:
[dependencies]
cairn_atproto = "^0.1.0"cairn.toml[[require]]
name = "cairn_atproto"
scope = "iamnbutler"
version = "^0.1.0"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 |
Claims in 0.1.0
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 |