Cairn
Docs
Claims
Blog
Packages
Claim ยท cairn 0.5.2
cairn^1012 The host reports scrolls where they happen, toward the end positive
An assumption of cairn 0.5.2.
- Id
cairn^1012- Kind
- assume
- Reads as
- assumed
- Version
- 0.5.2
What it says
The host sends each wheel or trackpad scroll as a scroll event at the logical point under the pointer, with positive dy toward the end of the content (AppKit's deltas negated, natural scrolling already applied) and 16 points to a wheel line; fractions carry, so the total stays within a point of AppKit's. The runtime moves the scroll box under that point by it (Runtime.wheel).
Evidence
| assumed | Stated, not proved. The proofs rely on it. | |
| fuzzed | Not shown yet: the trusted-base fuzzer's check pointer.scroll held. A CI step will publish it (#95). | |
Where it's defined
- Declaration
Cairn.Fuzz.Trusted.Claims.hostScroll- Module
Cairn.Fuzz.Trusted.Claims- Source
lean/Cairn/Fuzz/Trusted/Claims.lean:266atv0.5.2- Statement hash
-
Ledger
cairn^1012 is active in this version's claims.lock. An id never moves or changes meaning.