Cairn
Docs
Claims
Blog
Packages
Claim ยท cairn 0.5.2
cairn^1021 Assistive apps reach only what a scroll area shows
An assumption of cairn 0.5.2.
- Id
cairn^1021- Kind
- assume
- Reads as
- assumed
- Version
- 0.5.2
What it says
The host's accessibility tree holds exactly the frame's AX nodes that are not scrolled out, each under its frame parent in frame order: a node is scrolled out when it or a node above it has an empty rect with a scroll area above that (the frame gives each node its visible rect, Frame.ofLaid). A scroll area is an AXScrollArea; a hit test answers only elements in the tree; the focused element is the focused node's even when it is scrolled out.
Evidence
| assumed | Stated, not proved. The proofs rely on it. | |
| fuzzed | Not shown yet: the trusted-base fuzzer's check ax.scroll held. A CI step will publish it (#95). | |
Where it's defined
- Declaration
Cairn.Fuzz.Trusted.Claims.hostAxScroll- Module
Cairn.Fuzz.Trusted.Claims- Source
lean/Cairn/Fuzz/Trusted/Claims.lean:285atv0.5.2- Statement hash
-
Ledger
cairn^1021 is active in this version's claims.lock. An id never moves or changes meaning.