Cairn
Docs
Claims
Blog
Packages
Claim ยท cairn_atproto 0.3.0
cairn_atproto^20 The same write is the same request
An invariant of cairn_atproto 0.3.0.
- Id
cairn_atproto^20- Kind
- invariant
- Reads as
- proved
- Version
- 0.3.0
What it says
A record's putRecord call is built from the write alone (repo, record key, record): a POST to com.atproto.repo.putRecord whose body is the write's JSON, which reads back as the write. So the call built again for the same key and record is the same request, and sending it twice is the same write.
Evidence
| proved | init | CairnAtproto.ActClaims.sameWriteInv.init |
| proved | step | CairnAtproto.ActClaims.sameWriteInv.step |
| proved | receive | CairnAtproto.ActClaims.sameWriteInv.receive |
| proved | reachable | CairnAtproto.ActClaims.sameWriteInv.reachable |
| proved | reachableAll | CairnAtproto.ActClaims.sameWriteInv.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
CairnAtproto.ActClaims.sameWriteInv- Module
CairnAtproto.ActClaims- Source
lean/CairnAtproto/ActClaims.lean:118atv0.3.0- Machine
CairnAtproto.ActClaims.machine- Statement
CairnAtproto.ActClaims.sameWriteInv.holds- Statement hash
6f92f7a6746ce97b
Ledger
cairn_atproto^20 is active in this version's claims.lock, statement 6f92f7a6746ce97b. An id never moves or changes meaning.