Cairn · claims

Claims

Every claim Cairn declares, by id. Each links to its entry in the module that declares it, with its statement, its proofs and the evidence from this build.

Id	Claim	Kind	Reads as	proved	fuzzed	tested	seen	assumed	Module
^7	The host reports clicks where they happen	assume	assumed		unchecked			assumed	Cairn.Fuzz.Trusted.Claims
^214	The host reports a double click as a second click	assume	assumed		unchecked			assumed	Cairn.Fuzz.Trusted.Claims
^901	The Swift frame decoder agrees with Lean's	assume	assumed		fuzzed 20k			assumed	Cairn.Fuzz.Trusted.Claims
^902	Lean decodes what the Swift event encoder writes	assume	assumed		fuzzed 20k			assumed	Cairn.Fuzz.Trusted.Claims
^903	UTF-16 offsets and scalar indices convert exactly	assume	assumed		fuzzed 20k			assumed	Cairn.Fuzz.Trusted.Claims
^904	The text-input shadow predicts Lean's field	assume	assumed		fuzzed 4k			assumed	Cairn.Fuzz.Trusted.Claims
^905	Input-method geometry agrees with Lean's caret	assume	assumed		fuzzed 4k			assumed	Cairn.Fuzz.Trusted.Claims
^906	The host's text metrics are what layout assumes	assume	assumed		fuzzed 20k			assumed	Cairn.Fuzz.Trusted.Claims
^907	Carets follow the painted glyphs	assume	assumed		fuzzed 11k			assumed	Cairn.Fuzz.Trusted.Claims
^908	The host's clock is monotonic milliseconds	assume	assumed		fuzzed 1k			assumed	Cairn.Fuzz.Trusted.Claims
^909	The host wakes Lean by wake	assume	assumed		fuzzed 1k			assumed	Cairn.Fuzz.Trusted.Claims
^910	readFile replies with the file's bytes, or failed	assume	assumed		fuzzed 3.8k			assumed	Cairn.Fuzz.Trusted.Claims
^911	writeFile is atomic, and replies done only when the bytes are there	assume	assumed		fuzzed 5k			assumed	Cairn.Fuzz.Trusted.Claims
^912	playSound starts a known sound and refuses an unknown one	assume	assumed		fuzzed 5k			assumed	Cairn.Fuzz.Trusted.Claims
^913	http sends the request as given and returns the response as received	assume	retired						Cairn.Fuzz.Trusted.Claims
^914	The host answers every request exactly once, with its id	assume	assumed		fuzzed 1.0k			assumed	Cairn.Fuzz.Trusted.Claims
^915	every ms ticks while started and never after it is stopped	assume	assumed		fuzzed 969			assumed	Cairn.Fuzz.Trusted.Claims
^940	The native menu shows exactly the frame's menu records	assume	assumed		fuzzed 2k			assumed	Cairn.Fuzz.Trusted.Claims
^941	Choosing a menu item reports that item's ref	assume	assumed		fuzzed 1.4k			assumed	Cairn.Fuzz.Trusted.Claims
^942	Opening and closing the menu are reported once each	assume	assumed		fuzzed 2k			assumed	Cairn.Fuzz.Trusted.Claims
^943	An overlay panel never takes focus or clicks	assume	assumed		fuzzed 2k			assumed	Cairn.Fuzz.Trusted.Claims
^944	An overlay panel is where its anchor says	assume	assumed		fuzzed 2k			assumed	Cairn.Fuzz.Trusted.Claims
^945	A control's menu shows exactly the frame's menu records	assume	assumed		unchecked			assumed	Cairn.Fuzz.Trusted.Claims
^946	Choosing a control menu's item reports its ref, then the close	assume	assumed		unchecked			assumed	Cairn.Fuzz.Trusted.Claims
^947	The host shows a control menu only while Lean has it open	assume	assumed		unchecked			assumed	Cairn.Fuzz.Trusted.Claims
^948	AXShowMenu opens a control's menu as a right click does	assume	assumed		unchecked			assumed	Cairn.Fuzz.Trusted.Claims
^949	The menu bar shows the app's menu items	assume	assumed		unchecked			assumed	Cairn.Fuzz.Trusted.Claims
^950	A menu bar item, by click or key equivalent, reports that item's ref	assume	assumed		unchecked			assumed	Cairn.Fuzz.Trusted.Claims
^960	appendFile adds exactly the bytes at the end, or fails and adds nothing	assume	assumed		fuzzed 212			assumed	Cairn.Fuzz.Trusted.Claims
^961	listDir lists exactly the directory's names, sorted	assume	assumed		fuzzed 217			assumed	Cairn.Fuzz.Trusted.Claims
^962	deleteFile removes a file or a link, never a directory	assume	assumed		fuzzed 190			assumed	Cairn.Fuzz.Trusted.Claims
^963	watchFile reports every change to its file, and nothing after its stop	assume	assumed		fuzzed 197			assumed	Cairn.Fuzz.Trusted.Claims
^964	frontmostApp answers the app in front	assume	assumed		fuzzed 5k			assumed	Cairn.Fuzz.Trusted.Claims
^965	permission answers whether the app holds it, and prompts only when asked	assume	assumed		fuzzed 5k			assumed	Cairn.Fuzz.Trusted.Claims
^966	record streams the levels of exactly the samples it keeps, and nothing after its stop	assume	assumed		fuzzed 2.5k			assumed	Cairn.Fuzz.Trusted.Claims
^967	A clip's WAV for a range of windows holds exactly those samples	assume	assumed		fuzzed 2.5k			assumed	Cairn.Fuzz.Trusted.Claims
^968	globalKey reports the hotkey's press and release, and other keys while it is held	assume	assumed		fuzzed 5k			assumed	Cairn.Fuzz.Trusted.Claims
^969	typeText types exactly the text into that app, or nothing	assume	assumed		fuzzed 5k			assumed	Cairn.Fuzz.Trusted.Claims
^970	upload sends the body assembled from its parts, with the secret in its header	assume	assumed		fuzzed 4.4k			assumed	Cairn.Fuzz.Trusted.Claims
^971	A secret is read from the environment or its file, and never shown	assume	retired						Cairn.Fuzz.Trusted.Claims
^972	The Keychain keeps what it was given for this app	assume	assumed		unchecked			assumed	Cairn.Fuzz.Trusted.Claims
^973	Captured reply fields go to the Keychain and never to Lean	assume	assumed		unchecked			assumed	Cairn.Fuzz.Trusted.Claims
^974	http sends the request as given, with its secret header, and returns the response as received	assume	assumed		unchecked			assumed	Cairn.Fuzz.Trusted.Claims
^975	An environment secret is read from the environment or its file, and never shown	assume	assumed		unchecked			assumed	Cairn.Fuzz.Trusted.Claims
^990	Wrapped lines paint as wide as Lean measured them	assume	assumed		fuzzed 9.4k			assumed	Cairn.Fuzz.Trusted.Claims
^991	Lean breaks lines where Core Text would	assume	assumed		fuzzed 5.0k			assumed	Cairn.Fuzz.Trusted.Claims
^1000	openItem opens exactly the URL or existing file it names	assume	assumed		fuzzed 5k			assumed	Cairn.Fuzz.Trusted.Claims
^1001	appRunning answers whether an app with that bundle id runs	assume	assumed		fuzzed 5k			assumed	Cairn.Fuzz.Trusted.Claims
^1002	readDefault answers the default's value as text	assume	assumed		fuzzed 5k			assumed	Cairn.Fuzz.Trusted.Claims
^1003	makeDir makes a private directory and its parents	assume	assumed		fuzzed 184			assumed	Cairn.Fuzz.Trusted.Claims
^1004	A painter's pixels stay inside its box	assume	assumed		fuzzed 5k			assumed	Cairn.Fuzz.Trusted.Claims
^1005	record reports started once its microphone is running, before any audio, or fails without it	assume	assumed		unchecked			assumed	Cairn.Fuzz.Trusted.Claims
^1006	loadImage answers the image's pixel size, or the fault	assume	assumed		unchecked			assumed	Cairn.Fuzz.Trusted.Claims
^1007	An image's pixels stay inside its box	assume	assumed		unchecked			assumed	Cairn.Fuzz.Trusted.Claims
^1008	An image is drawn where its oriented pixels are	assume	assumed		unchecked			assumed	Cairn.Fuzz.Trusted.Claims
^1009	cancelRequest stops a running request's work; it is still answered once	assume	assumed		unchecked			assumed	Cairn.Fuzz.Trusted.Claims
^1010	The window is never smaller than the app's minimum size	assume	assumed		unchecked			assumed	Cairn.Fuzz.Trusted.Claims
^1011	The image cache reports every image it drops, after it is gone	assume	assumed		unchecked			assumed	Cairn.Fuzz.Trusted.Claims
^1012	The host reports scrolls where they happen, toward the end positive	assume	assumed		unchecked			assumed	Cairn.Fuzz.Trusted.Claims
^1020	Secure event input is on exactly while a secure field has focus	assume	assumed		unchecked			assumed	Cairn.Fuzz.Trusted.Claims
^1021	Assistive apps reach only what a scroll area shows	assume	assumed		unchecked			assumed	Cairn.Fuzz.Trusted.Claims
^1022	A secure field shows assistive apps nothing typed	assume	assumed		unchecked			assumed	Cairn.Fuzz.Trusted.Claims
^1030	The badge the host shows is the label of the last badge effect, or none	assume	assumed		unchecked			assumed	Cairn.Fuzz.Trusted.Claims
^1031	An announcement is posted once, with exactly its text	assume	assumed		unchecked			assumed	Cairn.Fuzz.Trusted.Claims
^1032	Under holdWorld the host sends no clock, wake or reply of its own	assume	assumed		unchecked			assumed	Cairn.Fuzz.Trusted.Claims
^1100	Set a value	move	proved	proved	not fuzzed	not tested	not seen		Cairn.Optimistic.Claims
^1101	The server handles a request	move	proved	proved	not fuzzed	not tested	not seen		Cairn.Optimistic.Claims
^1102	The server refuses a request	move	proved	proved	not fuzzed	not tested	not seen		Cairn.Optimistic.Claims
^1103	An answer arrives	move	proved	proved	not fuzzed	not tested	not seen		Cairn.Optimistic.Claims
^1104	A request or answer is lost	move	proved	proved	not fuzzed	not tested	not seen		Cairn.Optimistic.Claims
^1105	A retry comes due	move	proved	proved	not fuzzed	not tested	not seen		Cairn.Optimistic.Claims
^1106	A view is fetched	move	proved	proved	not fuzzed	not tested	not seen		Cairn.Optimistic.Claims
^1107	A set shows in its own step	invariant	proved	proved	not fuzzed	not tested			Cairn.Optimistic.Claims
^1108	At most one write in flight per key	invariant	proved	proved	not fuzzed	not tested			Cairn.Optimistic.Claims
^1109	Never more writes than sets	invariant	proved	proved	not fuzzed	not tested			Cairn.Optimistic.Claims
^1110	A refusal rolls back in its step	invariant	proved	proved	not fuzzed	not tested			Cairn.Optimistic.Claims
^1111	Settled keys show what the server holds	invariant	proved	proved	not fuzzed	not tested			Cairn.Optimistic.Claims
^1112	Replies for different keys commute	invariant	proved	proved	not fuzzed	not tested			Cairn.Optimistic.Claims
^1113	A settled count is the server's	invariant	proved	proved	not fuzzed	not tested			Cairn.Optimistic.Claims
^1114	A view never moves a written key	invariant	proved	proved	not fuzzed	not tested			Cairn.Optimistic.Claims