Cairn Docs Claims Blog Packages

Claim ยท cairn_atproto 0.3.0

cairn_atproto^14 Signed out, no secret is sent

An invariant of cairn_atproto 0.3.0.

Id
cairn_atproto^14
Kind
invariant
Reads as
proved
Version
0.3.0

All of cairn_atproto 0.3.0's claims

What it says

While signed out or signing in, no request carrying a Keychain secret is issued.

Evidence

provedinitCairnAtproto.Claims.noSecretSignedOut.init
provedstepCairnAtproto.Claims.noSecretSignedOut.step
provedreceiveCairnAtproto.Claims.noSecretSignedOut.receive
provedreachableCairnAtproto.Claims.noSecretSignedOut.reachable
provedreachableAllCairnAtproto.Claims.noSecretSignedOut.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
CairnAtproto.Claims.noSecretSignedOut
Module
CairnAtproto.Claims
Source
lean/CairnAtproto/Claims.lean:148 at v0.3.0
Machine
CairnAtproto.Claims.machine
Statement
CairnAtproto.Claims.noSecretSignedOut.holds
Statement hash
497edb490a99ed9d

Ledger

cairn_atproto^14 is active in this version's claims.lock, statement 497edb490a99ed9d. An id never moves or changes meaning.