Cairn Docs Claims Blog Packages

Claim ยท cairn_atproto 0.1.0

cairn_atproto^7 A second send only after a successful refresh

An invariant of cairn_atproto 0.1.0.

Id
cairn_atproto^7
Kind
invariant
Reads as
proved
Version
0.1.0

All of cairn_atproto 0.1.0's claims

What it says

A call that was sent before is sent again only in the step a refresh in flight gets a 2xx session reply.

Evidence

provedinitCairnAtproto.Claims.retryAfterRefresh.init
provedstepCairnAtproto.Claims.retryAfterRefresh.step
provedreceiveCairnAtproto.Claims.retryAfterRefresh.receive
provedreachableCairnAtproto.Claims.retryAfterRefresh.reachable
provedreachableAllCairnAtproto.Claims.retryAfterRefresh.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.retryAfterRefresh
Module
CairnAtproto.Claims
Source
lean/CairnAtproto/Claims.lean:116 at v0.1.0
Machine
CairnAtproto.Claims.machine
Statement
CairnAtproto.Claims.retryAfterRefresh.holds
Statement hash
ff581c2c33688c4c

Ledger

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