Cairn Docs Claims Blog Packages

Claim ยท cairn 0.5.2

cairn^1108 At most one write in flight per key

An invariant of cairn 0.5.2.

Id
cairn^1108
Kind
invariant
Reads as
proved
Version
0.5.2

All of cairn 0.5.2's claims

What it says

For every key, at most one write is in the network, before or after the server handled it: a set while one is in flight only changes what is shown.

Evidence

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

Ledger

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