Cairn Docs Claims Blog Packages

Claim ยท sky 0.3.1

sky^36 Image loads only near the view

An invariant of sky 0.3.1.

Id
sky^36
Kind
invariant
Reads as
proved
Version
0.3.1

All of sky 0.3.1's claims

What it says

When a post comes into view, every image load still in flight is for a post within 12 rows of it: loads for posts scrolled far away are cancelled. Signed out, no image load is in flight and there are no rows. At most 6 requests are with the host at once (Cairn's maxInFlight, Runtime.step_cap).

Evidence

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

Ledger

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