Cairn Docs Claims Blog Packages

Claim ยท cairn_examples 0.2.0

cairn_examples^409 Pending requests have fresh ids

An invariant of cairn_examples 0.2.0.

Id
cairn_examples^409
Kind
invariant
Reads as
proved
Version
0.2.0

All of cairn_examples 0.2.0'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
Clock
Source
lean/Clock.lean:225 at v0.2.0
Machine
Examples.Clock.machine
Statement
Examples.Clock.freshRequests.holds
Statement hash
631e025c1afbf429

Ledger

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