Cairn
Docs
Claims
Blog
Packages
Claim ยท cairn_atproto 0.3.0
cairn_atproto^32 The fake's counts are its like records
An invariant of cairn_atproto 0.3.0.
- Id
cairn_atproto^32- Kind
- invariant
- Reads as
- proved
- Version
- 0.3.0
What it says
In the fake PDS's model, a post view's like count is its seeded likes plus every like record the AppView shows (other accounts' and the tester's), and viewer.like is set exactly when the tester's like is among them; the same for reposts. Counts and viewer state come from one run of the log, so ^24 holds of the fake.
Evidence
| proved | init | CairnAtproto.ActClaims.fakeCounts.init |
| proved | step | CairnAtproto.ActClaims.fakeCounts.step |
| proved | receive | CairnAtproto.ActClaims.fakeCounts.receive |
| proved | reachable | CairnAtproto.ActClaims.fakeCounts.reachable |
| proved | reachableAll | CairnAtproto.ActClaims.fakeCounts.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.fakeCounts- Module
CairnAtproto.ActClaims- Source
lean/CairnAtproto/ActClaims.lean:259atv0.3.0- Machine
CairnAtproto.ActClaims.machine- Statement
CairnAtproto.ActClaims.fakeCounts.holds- Statement hash
223dde90a0d812fe
Ledger
cairn_atproto^32 is active in this version's claims.lock, statement 223dde90a0d812fe. An id never moves or changes meaning.