Cairn Docs Claims Blog Packages

Claim ยท cairn 0.2.4

cairn^409 Pending requests have fresh ids

An invariant of cairn 0.2.4.

Id
cairn^409
Kind
invariant
Reads as
proved
Version
0.2.4

All of cairn 0.2.4's claims

What it says

The pending save and load, if any, have ids below the next request's, so a reply to a later request is never taken for theirs.

Evidence

provedinitExamples.Clock.freshRequests.init
provedstepExamples.Clock.freshRequests.step
provedreceiveExamples.Clock.freshRequests.receive
provedreachableExamples.Clock.freshRequests.reachable
provedreachableAllExamples.Clock.freshRequests.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.Clock.freshRequests
Module
Examples.Clock
Source
lean/Examples/Clock.lean:225 at v0.2.4
Machine
Examples.Clock.machine
Statement
Examples.Clock.freshRequests.holds
Statement hash
631e025c1afbf429

Ledger

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