Cairn Docs Claims Blog Packages

Claim ยท sky 0.3.1

sky^22 The cursor is never lost

An invariant of sky 0.3.1.

Id
sky^22
Kind
invariant
Reads as
proved
Version
0.3.1

All of sky 0.3.1's claims

What it says

A feed with posts that isn't at its end holds a cursor: the one that came with its last page (fuzzed: equal to it).

Evidence

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

Ledger

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