Cairn
Docs
Claims
Blog
Packages
Claim ยท cairn 0.5.2
cairn^1031 An announcement is posted once, with exactly its text
An assumption of cairn 0.5.2.
- Id
cairn^1031- Kind
- assume
- Reads as
- assumed
- Version
- 0.5.2
What it says
For each announce effect the host posts one announcementRequested accessibility notification (NSAccessibility.post) for its window, carrying exactly the effect's text and its priority (low or high), in order, and posts none otherwise. Its text is the app's: the fuzzer checks that text typed into a secure field never reaches an effect's dump, announcements included.
Evidence
| assumed | Stated, not proved. The proofs rely on it. | |
| fuzzed | Not shown yet: the trusted-base fuzzer's check ax.announce held. A CI step will publish it (#95). | |
Where it's defined
- Declaration
Cairn.Fuzz.Trusted.Claims.hostAnnounce- Module
Cairn.Fuzz.Trusted.Claims- Source
lean/Cairn/Fuzz/Trusted/Claims.lean:299atv0.5.2- Statement hash
-
Ledger
cairn^1031 is active in this version's claims.lock. An id never moves or changes meaning.