Cairn
Docs
Claims
Blog
Packages
Claim ยท cairn_atproto 0.3.0
cairn_atproto^22 Writes with a chosen key are idempotent
An assumption of cairn_atproto 0.3.0.
- Id
cairn_atproto^22- Kind
- assume
- Reads as
- assumed
- Version
- 0.3.0
What it says
A com.atproto.repo.putRecord with a record key already written with the same record changes nothing, and a deleteRecord of a record that isn't there succeeds and changes nothing. So a write sent twice (a retry after a lost reply) is written once. Checked against the fake PDS, whose Lean model proves it of itself (cairn#251), and once against the real network (cairn#258).
Evidence
| assumed | Stated, not proved. The proofs rely on it. | |
| fuzzed | Not shown yet: the trusted-base fuzzer's check atproto.idempotent-writes held. A CI step will publish it (#95). | |
Where it's defined
- Declaration
CairnAtproto.ActClaims.idempotentWrites- Module
CairnAtproto.ActClaims- Source
lean/CairnAtproto/ActClaims.lean:132atv0.3.0- Statement hash
-
Ledger
cairn_atproto^22 is active in this version's claims.lock. An id never moves or changes meaning.