Cairn Docs Claims Blog Packages

Claim ยท cairn 0.2.4

cairn^504 Pending loads have fresh ids

An invariant of cairn 0.2.4.

Id
cairn^504
Kind
invariant
Reads as
proved
Version
0.2.4

All of cairn 0.2.4's claims

What it says

Every load waiting for its reply has an id below the next request's, so a reply to a later load is never taken for an earlier one.

Evidence

provedinitExamples.Gallery.freshLoads.init
provedstepExamples.Gallery.freshLoads.step
provedreceiveExamples.Gallery.freshLoads.receive
provedreachableExamples.Gallery.freshLoads.reachable
provedreachableAllExamples.Gallery.freshLoads.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.freshLoads
Module
Examples.Gallery
Source
lean/Examples/Gallery.lean:379 at v0.2.4
Machine
Examples.Gallery.machine
Statement
Examples.Gallery.freshLoads.holds
Statement hash
d34d5b06e8bc82cb

Ledger

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