Cairn
Docs
Claims
Blog
Packages
Claim ยท cairn 0.5.2
cairn^1004 A painter's pixels stay inside its box
An assumption of cairn 0.5.2.
- Id
cairn^1004- Kind
- assume
- Reads as
- assumed
- Version
- 0.5.2
What it says
A paint draw changes no pixel outside its rect (snapped to device pixels as rects are) within the clip in force, whatever its painter draws and whatever data, time or scale it is given; a paint naming no registered painter changes nothing. Checked offscreen against the same frame without its paint draws, with Yap's tape painter and painters whose triangles cover the whole target or land anywhere.
Evidence
| assumed | Stated, not proved. The proofs rely on it. | |
| fuzzed | Not shown yet: the trusted-base fuzzer's check render.paint.bounds held. A CI step will publish it (#95). | |
Where it's defined
- Declaration
Cairn.Fuzz.Trusted.Claims.hostPaintBounds- Module
Cairn.Fuzz.Trusted.Claims- Source
lean/Cairn/Fuzz/Trusted/Claims.lean:220atv0.5.2- Statement hash
-
Ledger
cairn^1004 is active in this version's claims.lock. An id never moves or changes meaning.