Cairn Docs Claims Blog Packages

Claim ยท sky 0.3.1

sky^25 Signed out, nothing shown or in flight

An invariant of sky 0.3.1.

Id
sky^25
Kind
invariant
Reads as
proved
Version
0.3.1

All of sky 0.3.1's claims

What it says

Whenever the session isn't signed in, the feed is empty and no call is in flight or held: every one was cancelled.

Evidence

provedinitSky.signedOutEmpty.init
provedstepSky.signedOutEmpty.step
provedreceiveSky.signedOutEmpty.receive
provedreachableSky.signedOutEmpty.reachable
provedreachableAllSky.signedOutEmpty.reachableAll
fuzzedNot shown yet: the claim-driven fuzzer held it in every random sequence (docs/fuzz.md). A CI step will publish it (#95).
testedNot shown yet: the running app matched the model at every step that exercised it (docs/conformance.md). A CI step will publish it (#95).

Where it's defined

Declaration
Sky.signedOutEmpty
Module
Sky.Claims
Source
lean/Sky/Claims.lean:276 at v0.3.1
Machine
Sky.machine
Statement
Sky.signedOutEmpty.holds
Statement hash
3efa62dad23fd6a2

Ledger

sky^25 is active in this version's claims.lock, statement 3efa62dad23fd6a2. An id never moves or changes meaning.