cairn_atproto

Use it

With the cairn tool:

cairn add cairn_atproto@^0.3.0

Which writes cairn.toml, and the lakefile line that it keeps in step:

[dependencies]
cairn_atproto = "^0.3.0"

cairn.toml

[[require]]
name = "cairn_atproto"
scope = "iamnbutler"
version = "^0.3.0"

lean/lakefile.toml

Depends on

cairn ^0.5.0
cairn_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.3.0

Claims new, retired or moved since 0.2.0.

Id	Change	Kind	Claim
`cairn_atproto^17`	new	move	Mint a record key
`cairn_atproto^18`	new	invariant	Record keys strictly increase
`cairn_atproto^19`	new	invariant	A record key's text reads back
`cairn_atproto^20`	new	invariant	The same write is the same request
`cairn_atproto^21`	new	invariant	How a write's reply is read
`cairn_atproto^22`	new	assume	Writes with a chosen key are idempotent
`cairn_atproto^23`	new	assume	getRecord reads your writes
`cairn_atproto^24`	new	assume	A post's counts and viewer are from one moment
`cairn_atproto^25`	new	assume	A write refused for its token was not applied
`cairn_atproto^26`	new	invariant	A paged list is a run of the server's
`cairn_atproto^27`	new	invariant	A stale page changes nothing
`cairn_atproto^28`	new	invariant	The cursor is never lost
`cairn_atproto^29`	new	invariant	A refresh racing a load-more
`cairn_atproto^30`	new	invariant	The decoders read back what the encoders write
`cairn_atproto^31`	new	invariant	The fake's writes are idempotent and read back
`cairn_atproto^32`	new	invariant	The fake's counts are its like records
`cairn_atproto^33`	new	invariant	The fake's notification pages are runs

Claims in 0.3.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	retired	One refresh at a time
`cairn_atproto^6`	invariant	retired	A call is sent at most twice
`cairn_atproto^7`	invariant	retired	A second send only after a successful refresh
`cairn_atproto^8`	invariant	retired	Signed out, no secret is sent
`cairn_atproto^9`	invariant	active	A failed refresh ends the held calls
`cairn_atproto^10`	assume	retired	No Lean value holds a token
`cairn_atproto^11`	invariant	active	One refresh at a time
`cairn_atproto^12`	invariant	active	A call is sent at most twice
`cairn_atproto^13`	invariant	active	A second send only after a successful refresh
`cairn_atproto^14`	invariant	active	Signed out, no secret is sent
`cairn_atproto^15`	assume	active	No Lean value holds a token
`cairn_atproto^16`	move	active	Cancel a call
`cairn_atproto^17`	move	active	Mint a record key
`cairn_atproto^18`	invariant	active	Record keys strictly increase
`cairn_atproto^19`	invariant	active	A record key's text reads back
`cairn_atproto^20`	invariant	active	The same write is the same request
`cairn_atproto^21`	invariant	active	How a write's reply is read
`cairn_atproto^22`	assume	active	Writes with a chosen key are idempotent
`cairn_atproto^23`	assume	active	getRecord reads your writes
`cairn_atproto^24`	assume	active	A post's counts and viewer are from one moment
`cairn_atproto^25`	assume	active	A write refused for its token was not applied
`cairn_atproto^26`	invariant	active	A paged list is a run of the server's
`cairn_atproto^27`	invariant	active	A stale page changes nothing
`cairn_atproto^28`	invariant	active	The cursor is never lost
`cairn_atproto^29`	invariant	active	A refresh racing a load-more
`cairn_atproto^30`	invariant	active	The decoders read back what the encoders write
`cairn_atproto^31`	invariant	active	The fake's writes are idempotent and read back
`cairn_atproto^32`	invariant	active	The fake's counts are its like records
`cairn_atproto^33`	invariant	active	The fake's notification pages are runs