Cairn Docs Claims Blog Packages

Claim ยท sky 0.3.1

sky^34 Posts keep their keys

An invariant of sky 0.3.1.

Id
sky^34
Kind
invariant
Reads as
proved
Version
0.3.1

All of sky 0.3.1's claims

What it says

The rows of the list are the feed's posts in its order, keyed from a first key up, with the end row's key 0 last and never a post's. Posts a refresh puts on top take the keys below the first; every post already there keeps its key and the list stays the same one, so the reader's post is found where it was; they are counted as new posts until they come into view. A feed replaced or emptied starts a new list, at the top.

Evidence

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

Ledger

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