Cairn
Docs
Claims
Blog
Packages
Claim ยท sky 0.3.1
sky^10 Sign in
A move of sky 0.3.1, in Sky window.
- Id
sky^10- Kind
- move
- Reads as
- proved
- Place
- Sky window
^1 - Version
- 0.3.1
What you do
Type 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.
What you see
Sky sends the one createSession request (its body redacted in every tool), and the password field is empty from that step on. Signed in, it loads the head of the home feed; refused, it says why in words.
Evidence
| proved | sound press | Sky.signInMove.press.sound |
| fuzzed | Not shown yet: the claim-driven fuzzer held it in every random sequence (docs/fuzz.md). A CI step will publish it (#95). | |
| tested | Not shown yet: the running app matched the model at every step that exercised it (docs/conformance.md). A CI step will publish it (#95). | |
| seen | Not shown yet: a screenshot of the app shows it. A CI step will publish it (#95). | |
Where it's defined
- Declaration
Sky.signInMove- Module
Sky.Claims- Source
lean/Sky/Claims.lean:118atv0.3.1- Statement
Sky.signInMove.enabledSky.signInMove.press.post- Statement hash
e8985a9abb7a20f9
Ledger
sky^10 is active in this version's claims.lock, statement e8985a9abb7a20f9. An id never moves or changes meaning.