Cairn Docs Claims Blog Packages

Claim ยท sky 0.3.1

sky^29 Signed out, no secret

An invariant of sky 0.3.1.

Id
sky^29
Kind
invariant
Reads as
proved
Version
0.3.1

All of sky 0.3.1's claims

What it says

Sign out's effects include forgetting both Keychain items (access and refresh). While signed out, no step sends a request carrying a Keychain secret.

Evidence

provedinitSky.signOutSecrets.init
provedstepSky.signOutSecrets.step
provedreceiveSky.signOutSecrets.receive
provedreachableSky.signOutSecrets.reachable
provedreachableAllSky.signOutSecrets.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.signOutSecrets
Module
Sky.Claims
Source
lean/Sky/Claims.lean:294 at v0.3.1
Machine
Sky.machine
Statement
Sky.signOutSecrets.holds
Statement hash
7eae90c0e25bda9b

Ledger

sky^29 is active in this version's claims.lock, statement 7eae90c0e25bda9b. An id never moves or changes meaning.