Cairn Docs Claims Blog Packages

Claim ยท cairn_atproto 0.3.0

cairn_atproto^13 A second send only after a successful refresh

An invariant of cairn_atproto 0.3.0.

Id
cairn_atproto^13
Kind
invariant
Reads as
proved
Version
0.3.0

All of cairn_atproto 0.3.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:141 at v0.3.0
Machine
CairnAtproto.Claims.machine
Statement
CairnAtproto.Claims.retryAfterRefresh.holds
Statement hash
8410c4bfd6c4507b

Ledger

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