Cairn
Docs
Claims
Blog
Packages
Claim ยท cairn 0.5.2
cairn^969 typeText types exactly the text into that app, or nothing
An assumption of cairn 0.5.2.
- Id
cairn^969- Kind
- assume
- Reads as
- assumed
- Version
- 0.5.2
What it says
typeText posts the text as key events whose payloads, in order, are exactly its UTF-16 units, at most 20 per event and never splitting a character, then Return only when asked, and only after the app with that pid is in front; empty text is invalid, no Accessibility denied, no such app notFound and an app that won't come forward failed, and then nothing is posted.
Evidence
| assumed | Stated, not proved. The proofs rely on it. | |
| fuzzed | Not shown yet: the trusted-base fuzzer's check effects.type-text held. A CI step will publish it (#95). | |
Where it's defined
- Declaration
Cairn.Fuzz.Trusted.Claims.hostTypeText- Module
Cairn.Fuzz.Trusted.Claims- Source
lean/Cairn/Fuzz/Trusted/Claims.lean:116atv0.5.2- Statement hash
-
Ledger
cairn^969 is active in this version's claims.lock. An id never moves or changes meaning.