cairn_atproto^30 The decoders read back what the encoders write

What it says

Every lexicon type added for acting decodes what its encoder writes: profiles and posts with the viewer's state, getPosts' and getProfile's answers, records, putRecord and deleteRecord bodies, getRecord's answer, notification pages (reasons as written), the unread count, updateSeen's body, and AT URIs. Through text too (CairnAtprotoProofs.Text). The decoders are total, and every fixture decodes (make fixtures).

Evidence

proved	init	`CairnAtproto.ActClaims.readsBackInv.init`
proved	step	`CairnAtproto.ActClaims.readsBackInv.step`
proved	receive	`CairnAtproto.ActClaims.readsBackInv.receive`
proved	reachable	`CairnAtproto.ActClaims.readsBackInv.reachable`
proved	reachableAll	`CairnAtproto.ActClaims.readsBackInv.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.readsBackInv
Module: CairnAtproto.ActClaims
Source: lean/CairnAtproto/ActClaims.lean:239 at v0.3.0
Machine: CairnAtproto.ActClaims.machine
Statement: CairnAtproto.ActClaims.readsBackInv.holds
Statement hash: 0b68743cdae010a2

Ledger

cairn_atproto^30 is active in this version's claims.lock, statement 0b68743cdae010a2. An id never moves or changes meaning.