cairn_atproto 0.3.0: claims

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
`cairn_atproto^16`	move	Cancel a callCancel the app's call k (in flight or held for a refresh).	proved
`cairn_atproto^17`	move	Mint a record keyMint a record key (a TID) at clock reading now, in microseconds since the epoch.	proved

Invariants

What holds in every state the app can reach.

Id	Claim	Reads as
`cairn_atproto^5`	One refresh at a time	retired
`cairn_atproto^6`	A call is sent at most twice	retired
`cairn_atproto^7`	A second send only after a successful refresh	retired
`cairn_atproto^8`	Signed out, no secret is sent	retired
`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
`cairn_atproto^11`	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^12`	A call is sent at most twiceEvery call the app makes is sent at most twice.	proved
`cairn_atproto^13`	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^14`	Signed out, no secret is sentWhile signed out or signing in, no request carrying a Keychain secret is issued.	proved
`cairn_atproto^18`	Record keys strictly increaseThe record keys (TIDs) a session mints strictly increase, as numbers and so as text, and so are distinct, whatever the clock reads: when it stands still or steps back, the next key is one microsecond past the last. All carry the session's clock id.	proved
`cairn_atproto^19`	A record key's text reads backEvery record key (TID) is written as 13 characters of the sortable base-32 alphabet (234567abcdefghijklmnopqrstuvwxyz), and reads back as its time in microseconds and its clock id.	proved
`cairn_atproto^20`	The same write is the same requestA record's putRecord call is built from the write alone (repo, record key, record): a POST to com.atproto.repo.putRecord whose body is the write's JSON, which reads back as the write. So the call built again for the same key and record is the same request, and sending it twice is the same write.	proved
`cairn_atproto^21`	How a write's reply is readA write's reply (putRecord, deleteRecord, muteActor, unmuteActor, updateSeen) is read as acknowledged exactly on a 2xx; refused, with its error and the rate limit's reset, on any other status below 500; lost (applied or not: read it back) on a 5xx, a timeout or a network failure; not sent when the host never sent it or the session was signed out.	proved
`cairn_atproto^26`	A paged list is a run of the server'sA paged list (the feed, notifications: any item type with keys distinct in the server's list) is a contiguous run of the server's list, in its order: no item twice, none skipped. A list that is a run stays one when the next page is appended, when a head page puts new items on top or replaces it, and when new items arrive at the server's head.	proved
`cairn_atproto^27`	A stale page changes nothingIn a paged list of any item type, a load-more page asked from a cursor the list no longer holds (a refresh replaced it meanwhile) never changes its items, cursor or end; nor does an answer to any call but the load-more in flight.	proved
`cairn_atproto^28`	The cursor is never lostA paged list with items that isn't at its end holds a cursor (where its next page starts), and the empty list does trivially: appending a page, a head page, a load-more's or refresh's answer and starting either keep it.	proved
`cairn_atproto^29`	A refresh racing a load-moreIn a paged list of any item type, with a load-more and a refresh both in flight, their answers in either order (or either failing) leave the same list.	proved
`cairn_atproto^30`	The decoders read back what the encoders writeEvery lexicon type added for acting decodes what its encoder writes: profiles and posts with the viewer's state, getPosts' and getProfile's answers, records, putRecord and deleteRecord bodies, getRecord's answer, notification pages (reasons as written), the unread count, updateSeen's body, and AT URIs. Through text too (CairnAtprotoProofs.Text). The decoders are total, and every fixture decodes (make fixtures).	proved
`cairn_atproto^31`	The fake's writes are idempotent and read backIn the fake PDS's model, a putRecord sent twice leaves the server as once, and so does a deleteRecord; deleting a record that isn't there changes nothing; after a 200 putRecord the repo holds the record at its key, after a 200 deleteRecord it holds none; and getRecord answers the record the repo holds now, RecordNotFound when there is none, whatever the AppView's lag. So ^22 and ^23 hold of the fake.	proved
`cairn_atproto^32`	The fake's counts are its like recordsIn the fake PDS's model, a post view's like count is its seeded likes plus every like record the AppView shows (other accounts' and the tester's), and viewer.like is set exactly when the tester's like is among them; the same for reposts. Counts and viewer state come from one run of the log, so ^24 holds of the fake.	proved
`cairn_atproto^33`	The fake's notification pages are runsIn the fake PDS's model, a listNotifications page is a contiguous run of the notifications the AppView shows, newest first: the head page is the newest, and the page from a cursor is the next ones after it, none skipped or repeated. New notifications only arrive at the head, so a cursor keeps meaning the same place.	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 token	retired
`cairn_atproto^15`	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). 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.	assumed

`CairnAtproto.ActClaims`

Id	Claim	Reads as
`cairn_atproto^22`	Writes with a chosen key are idempotentA com.atproto.repo.putRecord with a record key already written with the same record changes nothing, and a deleteRecord of a record that isn't there succeeds and changes nothing. So a write sent twice (a retry after a lost reply) is written once. Checked against the fake PDS, whose Lean model proves it of itself (cairn#251), and once against the real network (cairn#258).	assumed
`cairn_atproto^23`	getRecord reads your writescom.atproto.repo.getRecord on the account's own PDS reflects every write that PDS acknowledged (read-your-writes), where the AppView's views (timeline, getPosts, getProfile, notifications) may lag. So a write whose reply was lost is settled by reading its record back. Checked against the fake PDS (cairn#251) and once against the real network (cairn#258).	assumed
`cairn_atproto^24`	A post's counts and viewer are from one momentA post view's like and repost counts and its viewer state are from the same moment: the like count includes the viewer's own like exactly when viewer.like is set, and the repost count their repost exactly when viewer.repost is. So a client shows count - [viewer.like] + [shown liked]. Checked against the fake PDS (cairn#251) and once against the real network (cairn#258).	assumed
`cairn_atproto^25`	A write refused for its token was not appliedA write the server answers 400 ExpiredToken was not applied, so the session's one resend after a refresh (cairn_atproto^12, ^13) writes it at most once. Checked against the fake PDS (cairn#251) and once against the real network (cairn#258).	assumed