Cairn
Docs
Claims
Blog
Packages
Claims ยท sky
sky 0.1.0: claims
Everything sky 0.1.0 claims a person can do and see, and what holds, by place, each with its evidence.
10 proved1 no proof
Sky window sky^1
Sky's window. Bare for now: who is signed in, what went wrong, a button for each thing you can do, and the first posts of the home feed.
Moves
| Id | Claim | Reads as |
|---|---|---|
sky^2 | Sign inWhile signed out, press Sign in (with the service, handle and app password typed). | proved |
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^5 | Sign outWhile signed in or signing in, press Sign out. | proved |
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 |