Cairn Docs Claims Blog Packages

Claim ยท sky 0.3.1

sky^24 Requests in flight are accounted for

An invariant of sky 0.3.1.

Id
sky^24
Kind
invariant
Reads as
proved
Version
0.3.1

All of sky 0.3.1's claims

What it says

At most one load-more and one refresh are in flight, each a different call the session has taken on (sent or held for a token refresh); the load-more was asked from the cursor the feed holds; the session's requests have distinct ids. The fuzz checks every request is answered, cancelled or live.

Evidence

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

Ledger

sky^24 is active in this version's claims.lock, statement 62815f3f0fb3326f. An id never moves or changes meaning.