Cairn Docs Claims Blog Packages

Claim ยท sky 0.3.1

sky^21 A stale page changes nothing

An invariant of sky 0.3.1.

Id
sky^21
Kind
invariant
Reads as
proved
Version
0.3.1

All of sky 0.3.1's claims

What it says

A load-more page asked from a cursor the feed no longer holds (a refresh replaced the feed meanwhile) never changes the posts, the cursor or the end; nor does an answer to any call but the load-more in flight.

Evidence

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

Ledger

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