Cairn
Docs
Claims
Blog
Packages
Claim ยท cairn 0.5.2
cairn^1020 Secure event input is on exactly while a secure field has focus
An assumption of cairn 0.5.2.
- Id
cairn^1020- Kind
- assume
- Reads as
- assumed
- Version
- 0.5.2
What it says
The host turns the system's secure event input on (EnableSecureEventInput) when the applied frame's text input is a secure field, its window is key and the view is live, and off (DisableSecureEventInput) when any of those stops, the view is shut down or released; it calls them in pairs, never twice the same way in a row, so it never leaves secure input on. While it is on, no other process can read the keystrokes.
Evidence
| assumed | Stated, not proved. The proofs rely on it. | |
| fuzzed | Not shown yet: the trusted-base fuzzer's check text.secure-input held. A CI step will publish it (#95). | |
Where it's defined
- Declaration
Cairn.Fuzz.Trusted.Claims.hostSecureInput- Module
Cairn.Fuzz.Trusted.Claims- Source
lean/Cairn/Fuzz/Trusted/Claims.lean:279atv0.5.2- Statement hash
-
Ledger
cairn^1020 is active in this version's claims.lock. An id never moves or changes meaning.