Cairn Docs Claims Blog Packages

Claim ยท cairn 0.5.2

cairn^1109 Never more writes than sets

An invariant of cairn 0.5.2.

Id
cairn^1109
Kind
invariant
Reads as
proved
Version
0.5.2

All of cairn 0.5.2's claims

What it says

For every key, the writes the table has sent never outnumber the person's sets of it, whatever answers came back in whatever order: a lost write is read back, never sent again blind.

Evidence

provedinitCairn.Optimistic.Claims.writesWithinSets.init
provedstepCairn.Optimistic.Claims.writesWithinSets.step
provedreceiveCairn.Optimistic.Claims.writesWithinSets.receive
provedreachableCairn.Optimistic.Claims.writesWithinSets.reachable
provedreachableAllCairn.Optimistic.Claims.writesWithinSets.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
Cairn.Optimistic.Claims.writesWithinSets
Module
Cairn.Optimistic.Claims
Source
lean/Cairn/Optimistic/Claims.lean:193 at v0.5.2
Machine
Cairn.Optimistic.Claims.machine
Statement
Cairn.Optimistic.Claims.writesWithinSets.holds
Statement hash
d3665406f5c7ec0b

Ledger

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