Cairn Docs Claims Blog Packages

Claim ยท sky 0.3.1

sky^23 A refresh racing a load-more

An invariant of sky 0.3.1.

Id
sky^23
Kind
invariant
Reads as
proved
Version
0.3.1

All of sky 0.3.1's claims

What it says

With a load-more and a refresh both in flight, their answers in either order (or either failing) leave the same feed: the result of one of the two orders, and so of both.

Evidence

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

Ledger

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