Cairn
Docs
Claims
Blog
Packages
Claim ยท cairn 0.5.2
cairn^1112 Replies for different keys commute
An invariant of cairn 0.5.2.
- Id
cairn^1112- Kind
- invariant
- Reads as
- proved
- Version
- 0.5.2
What it says
Two inputs about different keys, in either order, leave the table the same at every key, and each gives the outputs it gives alone, so the two orders' outputs are the same two lists swapped.
Evidence
| proved | init | Cairn.Optimistic.Claims.commute.init |
| proved | step | Cairn.Optimistic.Claims.commute.step |
| proved | receive | Cairn.Optimistic.Claims.commute.receive |
| proved | reachable | Cairn.Optimistic.Claims.commute.reachable |
| proved | reachableAll | Cairn.Optimistic.Claims.commute.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.commute- Module
Cairn.Optimistic.Claims- Source
lean/Cairn/Optimistic/Claims.lean:215atv0.5.2- Machine
Cairn.Optimistic.Claims.machine- Statement
Cairn.Optimistic.Claims.commute.holds- Statement hash
5885d4aca69a60fe
Ledger
cairn^1112 is active in this version's claims.lock, statement 5885d4aca69a60fe. An id never moves or changes meaning.