Cairn
Docs
Claims
Blog
Packages
Claims ยท sky
sky 0.2.0: claims
Everything sky 0.2.0 claims a person can do and see, and what holds, by place, each with its evidence.
2 retired18 proved1 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: who, Sign out, Load more, Refresh and the first posts of the home feed.
Moves
| Id | Claim | Reads as |
|---|---|---|
sky^3 | Load moreWith a feed that isn't at its end, press Load more. | proved |
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 |
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 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^27 | 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 |