Cairn Docs Claims Blog Packages

Claim ยท sky 0.3.1

sky^20 The feed is a run of the timeline

An invariant of sky 0.3.1.

Id
sky^20
Kind
invariant
Reads as
proved
Version
0.3.1

All of sky 0.3.1's claims

What it says

The feed is a contiguous run of the server's timeline, in its order: no post twice, none skipped. Stated against a timeline with no duplicates: a feed that is a run of it stays one when the next page is appended, when a head page puts new posts on top, and when a head page that doesn't reach the feed replaces it.

Evidence

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

Ledger

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