Cairn Docs Claims Blog Packages

Claim ยท cairn_atproto 0.1.0

cairn_atproto^8 Signed out, no secret is sent

An invariant of cairn_atproto 0.1.0.

Id
cairn_atproto^8
Kind
invariant
Reads as
proved
Version
0.1.0

All of cairn_atproto 0.1.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:123 at v0.1.0
Machine
CairnAtproto.Claims.machine
Statement
CairnAtproto.Claims.noSecretSignedOut.holds
Statement hash
aca7b74513e33d03

Ledger

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