Cairn Docs Claims Blog Packages

Claim ยท cairn 0.2.5

cairn^510 Tiles fit the window at every size

An invariant of cairn 0.2.5.

Id
cairn^510
Kind
invariant
Reads as
proved
Version
0.2.5

All of cairn 0.2.5's claims

What it says

At every window size the tiles don't overlap, read left to right and top to bottom, and stay inside the window; resizing reflows them.

Evidence

provedinitExamples.Gallery.tilesFitInvariant.init
provedstepExamples.Gallery.tilesFitInvariant.step
provedreceiveExamples.Gallery.tilesFitInvariant.receive
provedreachableExamples.Gallery.tilesFitInvariant.reachable
provedreachableAllExamples.Gallery.tilesFitInvariant.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
Examples.Gallery.tilesFitInvariant
Module
Examples.Gallery
Source
lean/Examples/Gallery.lean:584 at v0.2.5
Machine
Examples.Gallery.machine
Statement
Examples.Gallery.tilesFitInvariant.holds
Statement hash
4b77d8ad02a81eb4

Ledger

cairn^510 is active in this version's claims.lock, statement 4b77d8ad02a81eb4. An id never moves or changes meaning.