Cairn
Docs
Claims
Blog
Packages
Claim ยท cairn 0.5.2
cairn^1111 Settled keys show what the server holds
An invariant of cairn 0.5.2.
- Id
cairn^1111- Kind
- invariant
- Reads as
- proved
- Version
- 0.5.2
What it says
Against a server that is a register per key with idempotent writes, for any sequence of sets and any interleaving of replies (each acknowledged, refused, or lost before or after the server applied it, delivered in any order, with views fetched at any time), every key with nothing in flight and nothing in doubt shows what the server holds. So once every reply is in, every key does.
Evidence
| proved | init | Cairn.Optimistic.Claims.converges.init |
| proved | step | Cairn.Optimistic.Claims.converges.step |
| proved | receive | Cairn.Optimistic.Claims.converges.receive |
| proved | reachable | Cairn.Optimistic.Claims.converges.reachable |
| proved | reachableAll | Cairn.Optimistic.Claims.converges.reachableAll |
| fuzzed | Not shown yet: the claim-driven fuzzer held it in every random sequence (docs/fuzz.md). A CI step will publish it (#95). | |
| tested | Not 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.converges- Module
Cairn.Optimistic.Claims- Source
lean/Cairn/Optimistic/Claims.lean:209atv0.5.2- Machine
Cairn.Optimistic.Claims.machine- Statement
Cairn.Optimistic.Claims.converges.holds- Statement hash
488e71959c11f9fd
Ledger
cairn^1111 is active in this version's claims.lock, statement 488e71959c11f9fd. An id never moves or changes meaning.