Cairn
Docs
Claims
Blog
Packages
Claims ยท sky
sky 0.3.1: claims
Everything sky 0.3.1 claims a person can do and see, and what holds, by place, each with its evidence.
5 retired24 proved2 no proof
Sky window sky^1
Sky's window. Signed out, the sign-in screen: handle or email, app password, service, Sign in, and what went wrong. Signed in: the home feed (Following), with Refresh and Account above it and a status line that offers new posts.
Moves
| Id | Claim | Reads as |
|---|---|---|
sky^4 | RefreshWhile signed in, press Refresh. | proved |
sky^6 | Type your handle or emailWhile signed out, type in the Handle or email field, and press Enter. | proved |
sky^7 | Type your app passwordWhile signed out, type in the App password field, and press Enter. | proved |
sky^8 | Type the serviceWhile signed out, type in the Service field (empty: https://bsky.social, or the default Sky reads at launch). | proved |
sky^9 | What's an app password?While signed out, press What's an app password? | proved |
sky^10 | Sign inType a handle or email and an app password, and press Sign in. It is enabled exactly when both fields are typed in and no sign-in (or resume) is in flight. | proved |
sky^11 | Sign outWhile signed in, open the account panel and press Sign out. | proved |
sky^12 | Cancel signing inWhile Sky has been signing in or resuming the session for a few seconds, press Cancel. | proved |
sky^13 | AccountWhile signed in, press Account (Done when it is open). | proved |
sky^33 | Show new postsAfter a refresh put posts above the one you are reading, press N new posts. | proved |
The feed sky^14
The home feed in a virtual list: one row per post (avatar, name, handle, time, the text wrapped, up to four images, Reposted by and Replying to, other embeds as a line, the counts), then the end row. Cairn owns its offset and lays only the rows near the view; the wheel, the trackpad and the page keys move it.
Moves
| Id | Claim | Reads as |
|---|---|---|
sky^30 | Reach the end of the feedScroll the feed to its end, while it isn't at the end of the timeline. | proved |
sky^31 | Retry loading moreAfter a load-more failed, press Retry at the end of the feed. | proved |
sky^32 | A postPress a post (or Return on it); or scroll it into view. | proved |
Not in a place
Moves and flows that name no place.
Invariants
What holds in every state the app can reach.
| Id | Claim | Reads as |
|---|---|---|
sky^20 | The feed is a run of the timelineThe feed is a contiguous run of the server's timeline, in its order: no post twice, none skipped. Stated against a timeline with no duplicates: a feed that is a run of it stays one when the next page is appended, when a head page puts new posts on top, and when a head page that doesn't reach the feed replaces it. | proved |
sky^21 | A stale page changes nothingA load-more page asked from a cursor the feed no longer holds (a refresh replaced the feed meanwhile) never changes the posts, the cursor or the end; nor does an answer to any call but the load-more in flight. | proved |
sky^22 | The cursor is never lostA feed with posts that isn't at its end holds a cursor: the one that came with its last page (fuzzed: equal to it). | proved |
sky^23 | A refresh racing a load-moreWith a load-more and a refresh both in flight, their answers in either order (or either failing) leave the same feed: the result of one of the two orders, and so of both. | proved |
sky^24 | Requests in flight are accounted forAt most one load-more and one refresh are in flight, each a different call the session has taken on (sent or held for a token refresh); the load-more was asked from the cursor the feed holds; the session's requests have distinct ids. The fuzz checks every request is answered, cancelled or live. | proved |
sky^25 | Signed out, nothing shown or in flightWhenever the session isn't signed in, the feed is empty and no call is in flight or held: every one was cancelled. | proved |
sky^26 | The password reaches one request | retired |
sky^27 | Signed out, no secret | retired |
sky^28 | The password reaches one requestEvery step but Sign in (the button, or Enter in the password field) has the same effects whatever the password field holds. Sign in's effects are the same too, for any password of the same length, once the redacted request's contents are blanked; with Sign in enabled its only request is createSession, carrying the password and marked redact, and the field is empty after. So the password is sent in exactly one request, and never shown by a tool (Cairn redacts it in dumps and logs; the fuzzer plants text in the field and checks). | proved |
sky^29 | Signed out, no secretSign out's effects include forgetting both Keychain items (access and refresh). While signed out, no step sends a request carrying a Keychain secret. | proved |
sky^34 | Posts keep their keysThe rows of the list are the feed's posts in its order, keyed from a first key up, with the end row's key 0 last and never a post's. Posts a refresh puts on top take the keys below the first; every post already there keeps its key and the list stays the same one, so the reader's post is found where it was; they are counted as new posts until they come into view. A feed replaced or emptied starts a new list, at the top. | proved |
sky^35 | The post you are reading stays stillWhen a refresh puts posts above the post at the top of the view (^34 keeps its key), or heights above it are corrected, the runtime moves the offset by exactly as much as that post moved, so it stays where it was on screen, unless the offset is clamped. At the very top too: the new posts land above the view, and N new posts (^33) offers them. Checked by the fuzzer at every step. | proved |
sky^36 | Image loads only near the viewWhen a post comes into view, every image load still in flight is for a post within 12 rows of it: loads for posts scrolled far away are cancelled. Signed out, no image load is in flight and there are no rows. At most 6 requests are with the host at once (Cairn's maxInFlight, Runtime.step_cap). | proved |