Cairn
Docs
Claims
Blog
Packages
Claim ยท cairn 0.5.2
cairn^1011 The image cache reports every image it drops, after it is gone
An assumption of cairn 0.5.2.
- Id
cairn^1011- Kind
- assume
- Reads as
- assumed
- Version
- 0.5.2
What it says
While an imageCache subscription runs, the host keeps its decoded images within the smallest running budget: past it, it drops the images used least recently, never one the latest published frame draws nor the one just loaded, and sends evicted for every image it drops (a failed reload's removal too) after the pixels are gone. It answers loadImage ready only after it held the pixels for that load. With Images.evicted on the Lean side, an image the app takes for ready has its pixels with the host once every message is heard (Images.Cache.ready_held_quiet).
Evidence
| assumed | Stated, not proved. The proofs rely on it. | |
| fuzzed | Not shown yet: the trusted-base fuzzer's check images.cache held. A CI step will publish it (#95). | |
Where it's defined
- Declaration
Cairn.Fuzz.Trusted.Claims.hostImageCache- Module
Cairn.Fuzz.Trusted.Claims- Source
lean/Cairn/Fuzz/Trusted/Claims.lean:273atv0.5.2- Statement hash
-
Ledger
cairn^1011 is active in this version's claims.lock. An id never moves or changes meaning.