Cairn.Fuzz.Trusted.Claims

The human half of claim ^7.

Assumed, never proved (^7 The host reports clicks where they happen): The host sends a pointer down and up at the logical point the person clicked, in order.

^7 The host reports clicks where they happen (assumption)

The host sends a pointer down and up at the logical point the person clicked, in order.

^214 The host reports a double click as a second click (assumption)

The host sends the second click of a double click as a pointer down with a click count of 2, at the same point, within the system's double-click interval; the runtime turns its release into a double press. (T20)

Assumed, never proved (^214 The host reports a double click as a second click): The host sends the second click of a double click as a pointer down with a click count of 2, at the same point, within the system's double-click interval; the runtime turns its release into a double press. (T20)

The human half of claim ^214.

^901 The Swift frame decoder agrees with Lean's (assumption)

For every byte buffer, the host's Frame(bytes:) accepts exactly when Lean's proved decodeFrame does, and then decodes the same frame.

The human half of claim ^901.

Assumed, never proved (^901 The Swift frame decoder agrees with Lean's): For every byte buffer, the host's Frame(bytes:) accepts exactly when Lean's proved decodeFrame does, and then decodes the same frame.

^902 Lean decodes what the Swift event encoder writes (assumption)

For every batch of events, Lean's proved decodeEvents decodes the host's encodeEvents bytes to the same events, and Lean's encoder gives back the same bytes.

The human half of claim ^902.

Assumed, never proved (^902 Lean decodes what the Swift event encoder writes): For every batch of events, Lean's proved decodeEvents decodes the host's encodeEvents bytes to the same events, and Lean's encoder gives back the same bytes.

^903 UTF-16 offsets and scalar indices convert exactly (assumption)

TextIndex maps between AppKit's UTF-16 offsets and Lean's scalar indices exactly on boundaries, rounds offsets inside a surrogate pair to a whole scalar, and clamps AppKit ranges (NSNotFound, negative, past the end) to whole scalars.

The human half of claim ^903.

Assumed, never proved (^903 UTF-16 offsets and scalar indices convert exactly): TextIndex maps between AppKit's UTF-16 offsets and Lean's scalar indices exactly on boundaries, rounds offsets inside a surrogate pair to a whole scalar, and clamps AppKit ranges (NSNotFound, negative, past the end) to whole scalars.

The human half of claim ^904.

Assumed, never proved (^904 The text-input shadow predicts Lean's field): Between an input-method call and the frame that reflects it, the host's copy of the focused field has the text, selection and marked range Lean's field will show.

^904 The text-input shadow predicts Lean's field (assumption)

Between an input-method call and the frame that reflects it, the host's copy of the focused field has the text, selection and marked range Lean's field will show.

Assumed, never proved (^905 Input-method geometry agrees with Lean's caret): selectedRange and markedRange are Lean's, firstRect at the selection is Lean's caret, and characterIndex(for:) maps points back to scalar boundaries of the field.

^905 Input-method geometry agrees with Lean's caret (assumption)

selectedRange and markedRange are Lean's, firstRect at the selection is Lean's caret, and characterIndex(for:) maps points back to scalar boundaries of the field.

The human half of claim ^905.

^906 The host's text metrics are what layout assumes (assumption)

cairn_text_metrics gives one offset per scalar boundary, from 0 and nondecreasing, with nonnegative ascent and descent, and Lean's TextMetrics.host sees those numbers unchanged.

The human half of claim ^906.

Assumed, never proved (^906 The host's text metrics are what layout assumes): cairn_text_metrics gives one offset per scalar boundary, from 0 and nondecreasing, with nonnegative ascent and descent, and Lean's TextMetrics.host sees those numbers unchanged.

^907 Carets follow the painted glyphs (assumption)

On left-to-right text, the caret offset after each grapheme is at or right of every glyph painted for the text before it.

The human half of claim ^907.

Assumed, never proved (^907 Carets follow the painted glyphs): On left-to-right text, the caret offset after each grapheme is at or right of every glyph painted for the text before it.

The human half of claim ^908.

^908 The host's clock is monotonic milliseconds (assumption)

Every batch the host sends Lean starts with exactly one clock event; its monotonic milliseconds never decrease from batch to batch and are not ahead of the system's monotonic clock, its wall time is the wall clock and its zone the current UTC offset.

Assumed, never proved (^908 The host's clock is monotonic milliseconds): Every batch the host sends Lean starts with exactly one clock event; its monotonic milliseconds never decrease from batch to batch and are not ahead of the system's monotonic clock, its wall time is the wall clock and its zone the current UTC offset.

^909 The host wakes Lean by wake (assumption)

When a frame carries a wake deadline, the host sends a clock-only batch whose time is at or past the deadline, soon after it, and sends none for a deadline that a later frame cleared or met.

Assumed, never proved (^909 The host wakes Lean by wake): When a frame carries a wake deadline, the host sends a clock-only batch whose time is at or past the deadline, soon after it, and sends none for a deadline that a later frame cleared or met.

The human half of claim ^909.

Assumed, never proved (^910 readFile replies with the file's bytes, or failed): readFile answers with exactly the bytes the file holds, notFound for a missing file, a failure for a directory or an unreadable file, and invalid for a path that can't name a file.

The human half of claim ^910.

^910 readFile replies with the file's bytes, or failed (assumption)

readFile answers with exactly the bytes the file holds, notFound for a missing file, a failure for a directory or an unreadable file, and invalid for a path that can't name a file.

^911 writeFile is atomic, and replies done only when the bytes are there (assumption)

writeFile answers done only when the file then holds exactly the bytes, creating missing directories; a reader alongside sees the old bytes or the new ones, never a mix; a failed write leaves the old file unchanged; a path that can't name a file is invalid.

Assumed, never proved (^911 writeFile is atomic, and replies done only when the bytes are there): writeFile answers done only when the file then holds exactly the bytes, creating missing directories; a reader alongside sees the old bytes or the new ones, never a mix; a failed write leaves the old file unchanged; a path that can't name a file is invalid.

The human half of claim ^911.

Assumed, never proved (^912 playSound starts a known sound and refuses an unknown one): playSound finds every system sound by its name and answers done once it starts; any other name is answered notFound, once, without playing anything.

The human half of claim ^912.

^912 playSound starts a known sound and refuses an unknown one (assumption)

playSound finds every system sound by its name and answers done once it starts; any other name is answered notFound, once, without playing anything.

The human half of claim ^913.

Assumed, never proved (^914 The host answers every request exactly once, with its id): Every request the host runs is answered at most once and, when its handler answers, exactly once, under its own id with the handler's first answer; a kind with no handler is answered invalid; after the app starts over no answer to an earlier request is sent.

The human half of claim ^914.

^914 The host answers every request exactly once, with its id (assumption)

Every request the host runs is answered at most once and, when its handler answers, exactly once, under its own id with the handler's first answer; a kind with no handler is answered invalid; after the app starts over no answer to an earlier request is sent.

^915 every ms ticks while started and never after it is stopped (assumption)

An every subscription ticks under its id only while it is started and not yet stopped, at most once per period, and the host's running subscriptions are exactly those the frames started and did not stop.

Assumed, never proved (^915 every ms ticks while started and never after it is stopped): An every subscription ticks under its id only while it is started and not yet stopped, at most once per period, and the host's running subscriptions are exactly those the frames started and did not stop.

The human half of claim ^915.

The human half of claim ^940.

Assumed, never proved (^940 The native menu shows exactly the frame's menu records): After each frame, a status item's NSMenu tree holds the frame's menu records in order: each item's title, enabled state, checkmark, key equivalent and ref, separators where they are, each submenu under its item with its own records, and status lines shown but not actionable; updating it in place or rebuilding it gives the same tree.

^940 The native menu shows exactly the frame's menu records (assumption)

After each frame, a status item's NSMenu tree holds the frame's menu records in order: each item's title, enabled state, checkmark, key equivalent and ref, separators where they are, each submenu under its item with its own records, and status lines shown but not actionable; updating it in place or rebuilding it gives the same tree.

Assumed, never proved (^941 Choosing a menu item reports that item's ref): When AppKit performs a menu item's action, the host sends exactly one menuSelect with the status item's place and that item's ref, and nothing for a status line, separator or submenu; Lean checks the ref against the menu it is showing (menu_select_stale).

^941 Choosing a menu item reports that item's ref (assumption)

When AppKit performs a menu item's action, the host sends exactly one menuSelect with the status item's place and that item's ref, and nothing for a status line, separator or submenu; Lean checks the ref against the menu it is showing (menu_select_stale).

The human half of claim ^941.

^942 Opening and closing the menu are reported once each (assumption)

When the status item's menu opens the host sends one menuOpen with its place, and one menuClose when it closes; submenus opening and closing send nothing.

The human half of claim ^942.

Assumed, never proved (^942 Opening and closing the menu are reported once each): When the status item's menu opens the host sends one menuOpen with its place, and one menuClose when it closes; submenus opening and closing send nothing.

Assumed, never proved (^943 An overlay panel never takes focus or clicks): Every overlay panel is a non-activating panel that cannot become key or main, ignores the mouse, sits at status-bar level on every Space and over full-screen apps, is not hidden when the app deactivates and is transparent, whatever frames it is given.

The human half of claim ^943.

^943 An overlay panel never takes focus or clicks (assumption)

Every overlay panel is a non-activating panel that cannot become key or main, ignores the mouse, sits at status-bar level on every Space and over full-screen apps, is not hidden when the app deactivates and is transparent, whatever frames it is given.

The human half of claim ^944.

Assumed, never proved (^944 An overlay panel is where its anchor says): A shown panel's frame has its canvas's size, horizontally centred in the chosen screen's visible frame and the anchor's offset above its bottom, on whole points; the screen is chosen when it appears and kept until it is hidden.

^944 An overlay panel is where its anchor says (assumption)

A shown panel's frame has its canvas's size, horizontally centred in the chosen screen's visible frame and the anchor's offset above its bottom, on whole points; the screen is chosen when it appears and kept until it is hidden.

^945 A control's menu shows exactly the frame's menu records (assumption)

While the window's frame record shows a control's menu (its status: the owner and the menu records), the host's native menu for it holds those records as a status item's does (^940), for that owner, at the window's place; a frame with no menu records shows none.

The human half of claim ^945.

Assumed, never proved (^945 A control's menu shows exactly the frame's menu records): While the window's frame record shows a control's menu (its status: the owner and the menu records), the host's native menu for it holds those records as a status item's does (^940), for that owner, at the window's place; a frame with no menu records shows none.

^946 Choosing a control menu's item reports its ref, then the close (assumption)

When AppKit performs an item's action in a control's menu, the host sends exactly one menuSelect with the window's place and that item's ref, and nothing for a status line, separator or submenu; when the menu closes, chosen from or not, it sends one menuClose with the window's place, after any menuSelect.

Assumed, never proved (^946 Choosing a control menu's item reports its ref, then the close): When AppKit performs an item's action in a control's menu, the host sends exactly one menuSelect with the window's place and that item's ref, and nothing for a status line, separator or submenu; when the menu closes, chosen from or not, it sends one menuClose with the window's place, after any menuSelect.

The human half of claim ^946.

The human half of claim ^947.

Assumed, never proved (^947 The host shows a control menu only while Lean has it open): The host shows a control's menu exactly when the last frame shows one, except that after the host closed it, a frame that does not yet account for that close (its events are numbered below the close) does not open it again; a frame without the menu, or without a window, dismisses one that is open.

^947 The host shows a control menu only while Lean has it open (assumption)

The host shows a control's menu exactly when the last frame shows one, except that after the host closed it, a frame that does not yet account for that close (its events are numbered below the close) does not open it again; a frame without the menu, or without a window, dismisses one that is open.

Assumed, never proved (^948 AXShowMenu opens a control's menu as a right click does): An assistive app may perform AXShowMenu on exactly the AX elements of controls with a menu, and doing so sends a secondary click (move, down, up) at the node's centre, then puts the pointer back; a control that is a menu button is an AXMenuButton.

^948 AXShowMenu opens a control's menu as a right click does (assumption)

An assistive app may perform AXShowMenu on exactly the AX elements of controls with a menu, and doing so sends a secondary click (move, down, up) at the node's centre, then puts the pointer back; a control that is a menu button is an AXMenuButton.

The human half of claim ^948.

Assumed, never proved (^949 The menu bar shows the app's menu items): After each frame with a menuBar surface, each of its top-level submenus is a menu in the main menu before the host's Window menu, with its records as a status item's menu has them (^940), and every other top-level entry is at the top of the app menu, in order, followed by a separator and the host's own Hide and Quit, unchanged; Edit and Window stay where they are.

The human half of claim ^949.

^949 The menu bar shows the app's menu items (assumption)

After each frame with a menuBar surface, each of its top-level submenus is a menu in the main menu before the host's Window menu, with its records as a status item's menu has them (^940), and every other top-level entry is at the top of the app menu, in order, followed by a separator and the host's own Hide and Quit, unchanged; Edit and Window stay where they are.

Assumed, never proved (^950 A menu bar item, by click or key equivalent, reports that item's ref): When AppKit performs an enabled menu bar item's action, chosen with the pointer or by its key equivalent (NSMenu.performKeyEquivalent with the keys a keyboard gives, a capital for a shifted letter), the host sends exactly one menuSelect with the menuBar surface's place and that item's ref; the key equivalent of a greyed item sends nothing.

The human half of claim ^950.

^950 A menu bar item, by click or key equivalent, reports that item's ref (assumption)

When AppKit performs an enabled menu bar item's action, chosen with the pointer or by its key equivalent (NSMenu.performKeyEquivalent with the keys a keyboard gives, a capital for a shifted letter), the host sends exactly one menuSelect with the menuBar surface's place and that item's ref; the key equivalent of a greyed item sends nothing.

Assumed, never proved (^960 appendFile adds exactly the bytes at the end, or fails and adds nothing): appendFile answers done only when the file then holds its old bytes followed by exactly the new ones, creating the file with mode 600 and missing directories; appends from several threads each land whole; a directory, a path under a file, a read-only file and a path that can't name a file fail and leave the file unchanged.

^960 appendFile adds exactly the bytes at the end, or fails and adds nothing (assumption)

appendFile answers done only when the file then holds its old bytes followed by exactly the new ones, creating the file with mode 600 and missing directories; appends from several threads each land whole; a directory, a path under a file, a read-only file and a path that can't name a file fail and leave the file unchanged.

The human half of claim ^960.

^961 listDir lists exactly the directory's names, sorted (assumption)

listDir answers with exactly the names in the directory, without . and .., sorted by their UTF-8 bytes; a missing directory is notFound, a file invalid, an unreadable directory denied.

The human half of claim ^961.

Assumed, never proved (^961 listDir lists exactly the directory's names, sorted): listDir answers with exactly the names in the directory, without . and .., sorted by their UTF-8 bytes; a missing directory is notFound, a file invalid, an unreadable directory denied.

^962 deleteFile removes a file or a link, never a directory (assumption)

deleteFile answers done only when the file or link (not its target) is gone, notFound when there is none, invalid for a directory, which stays, and denied when its directory is read-only, leaving the file.

The human half of claim ^962.

Assumed, never proved (^962 deleteFile removes a file or a link, never a directory): deleteFile answers done only when the file or link (not its target) is gone, notFound when there is none, invalid for a directory, which stays, and denied when its directory is read-only, leaving the file.

The human half of claim ^963.

^963 watchFile reports every change to its file, and nothing after its stop (assumption)

While a watchFile subscription runs, every write, replacement, append, creation, removal, touch or mode change of its file is followed by a changed event within a few polls, an untouched file brings none, and after its stop has been handled none is sent.

Assumed, never proved (^963 watchFile reports every change to its file, and nothing after its stop): While a watchFile subscription runs, every write, replacement, append, creation, removal, touch or mode change of its file is followed by a changed event within a few polls, an untouched file brings none, and after its stop has been handled none is sent.

Assumed, never proved (^964 frontmostApp answers the app in front): frontmostApp answers with the process id and name of the app the system reports in front, notFound when there is none; the pid names a running process.

The human half of claim ^964.

^964 frontmostApp answers the app in front (assumption)

frontmostApp answers with the process id and name of the app the system reports in front, notFound when there is none; the pid names a running process.

^965 permission answers whether the app holds it, and prompts only when asked (assumption)

permission answers flag true exactly when the app holds Accessibility (AXIsProcessTrusted) or the microphone (authorized); the system is asked to prompt only when prompt is set, the microphone only while undecided, answering with the person's choice; each request is answered once.

Assumed, never proved (^965 permission answers whether the app holds it, and prompts only when asked): permission answers flag true exactly when the app holds Accessibility (AXIsProcessTrusted) or the microphone (authorized); the system is asked to prompt only when prompt is set, the microphone only while undecided, answering with the person's choice; each request is answered once.

The human half of claim ^965.

^966 record streams the levels of exactly the samples it keeps, and nothing after its stop (assumption)

While a record subscription runs, its audio events count every sample the clip keeps, in order, and their windows are the 20 ms levels (sum of squares and peak of each 320 samples) of those samples from the start of the clip, however the microphone split them; after its stop has been handled none is sent and the clip is finished; a microphone that can't start (no permission, no device) is one failed event and an empty clip, and the microphone is never started without the permission.

Assumed, never proved (^966 record streams the levels of exactly the samples it keeps, and nothing after its stop): While a record subscription runs, its audio events count every sample the clip keeps, in order, and their windows are the 20 ms levels (sum of squares and peak of each 320 samples) of those samples from the start of the clip, however the microphone split them; after its stop has been handled none is sent and the clip is finished; a microphone that can't start (no permission, no device) is one failed event and an empty clip, and the microphone is never started without the permission.

The human half of claim ^966.

^967 A clip's WAV for a range of windows holds exactly those samples (assumption)

An upload's wav part for clip c and windows s to e is a 16 kHz mono 16-bit RIFF/WAVE file of exactly samples 320 s to 320 e of the clip (to the end of the clip when e is none, waiting for a clip whose recording is being stopped); a range past the end or backwards is invalid, an unknown or forgotten clip notFound, and forgetClip answers done once and notFound after.

Assumed, never proved (^967 A clip's WAV for a range of windows holds exactly those samples): An upload's wav part for clip c and windows s to e is a 16 kHz mono 16-bit RIFF/WAVE file of exactly samples 320 s to 320 e of the clip (to the end of the clip when e is none, waiting for a clip whose recording is being stopped); a range past the end or backwards is invalid, an unknown or forgotten clip notFound, and forgetClip answers done once and notFound after.

The human half of claim ^967.

^968 globalKey reports the hotkey's press and release, and other keys while it is held (assumption)

A globalKey subscription reports keyDown and keyUp of the hotkey and otherKey for any other key pressed while it is down, as Yap's PushToTalk does (a modifier by its flag in flagsChanged, an ordinary key by key down without repeats and key up, no repeated state), with monotonic times; without Accessibility it reports failed denied and installs nothing; after its stop has been handled none is sent.

Assumed, never proved (^968 globalKey reports the hotkey's press and release, and other keys while it is held): A globalKey subscription reports keyDown and keyUp of the hotkey and otherKey for any other key pressed while it is down, as Yap's PushToTalk does (a modifier by its flag in flagsChanged, an ordinary key by key down without repeats and key up, no repeated state), with monotonic times; without Accessibility it reports failed denied and installs nothing; after its stop has been handled none is sent.

The human half of claim ^968.

Assumed, never proved (^969 typeText types exactly the text into that app, or nothing): 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.

The human half of claim ^969.

^969 typeText types exactly the text into that app, or nothing (assumption)

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.

The human half of claim ^970.

^970 upload sends the body assembled from its parts, with the secret in its header (assumption)

upload sends one request whose body is its parts in order, each wav part replaced by the clip's WAV, with its headers and, for a secret, the header scheme ++ value; a missing clip, bad range or missing secret fails before anything is sent; otherwise it answers as http does.

Assumed, never proved (^970 upload sends the body assembled from its parts, with the secret in its header): upload sends one request whose body is its parts in order, each wav part replaced by the clip's WAV, with its headers and, for a secret, the header scheme ++ value; a missing clip, bad range or missing secret fails before anything is sent; otherwise it answers as http does.

The human half of claim ^971.

The human half of claim ^972.

Assumed, never proved (^972 The Keychain keeps what it was given for this app): The host's Keychain store keeps one generic password item per account, under the app's service (its bundle identifier), in the login keychain (file-based, not synchronized to iCloud, no access group): reading an account gives the value last written to it, exactly, until it is deleted; writing one account changes no other; forgetSecret deletes the item and answers done, also when there was none; a Keychain secret whose item is missing answers failed notFound. Values never appear in a reply, failure message, frame, dump or debug description.

^972 The Keychain keeps what it was given for this app (assumption)

The host's Keychain store keeps one generic password item per account, under the app's service (its bundle identifier), in the login keychain (file-based, not synchronized to iCloud, no access group): reading an account gives the value last written to it, exactly, until it is deleted; writing one account changes no other; forgetSecret deletes the item and answers done, also when there was none; a Keychain secret whose item is missing answers failed notFound. Values never appear in a reply, failure message, frame, dump or debug description.

^973 Captured reply fields go to the Keychain and never to Lean (assumption)

For an http request with captures, a 2xx reply whose body is a JSON object with each listed top-level field present once as a string has each value written exactly to its account's Keychain item, and Lean receives the body with each of those values written as an empty string and every other byte as the server sent it; a body that is not a JSON object, or a listed field that is missing, repeated or not a string, answers failed invalid and writes nothing, and a failed write leaves every item as it was. Any other reply passes through unchanged. A captured value appears in no reply, failure message, frame, dump or debug description.

The human half of claim ^973.

Assumed, never proved (^973 Captured reply fields go to the Keychain and never to Lean): For an http request with captures, a 2xx reply whose body is a JSON object with each listed top-level field present once as a string has each value written exactly to its account's Keychain item, and Lean receives the body with each of those values written as an empty string and every other byte as the server sent it; a body that is not a JSON object, or a listed field that is missing, repeated or not a string, answers failed invalid and writes nothing, and a failed write leaves every item as it was. Any other reply passes through unchanged. A captured value appears in no reply, failure message, frame, dump or debug description.

The human half of claim ^974.

^974 http sends the request as given, with its secret header, and returns the response as received (assumption)

http sends the method, URL, headers and body as given, plus for a secret the header scheme ++ value, and answers with the response's status, headers sorted by name and body exactly (captured fields aside, ^973); a missing secret is notFound and sends nothing; a request with a secret never follows a redirect, answering the 3xx; a connection failure is network, no answer in time is timeout, and a non-http URL, a bad method, a header (the secret's too) that could inject another, or an empty account is invalid and sends nothing.

Assumed, never proved (^974 http sends the request as given, with its secret header, and returns the response as received): http sends the method, URL, headers and body as given, plus for a secret the header scheme ++ value, and answers with the response's status, headers sorted by name and body exactly (captured fields aside, ^973); a missing secret is notFound and sends nothing; a request with a secret never follows a redirect, answering the 3xx; a connection failure is network, no answer in time is timeout, and a non-http URL, a bad method, a header (the secret's too) that could inject another, or an empty account is invalid and sends nothing.

^975 An environment secret is read from the environment or its file, and never shown (assumption)

An environment secret's value is the environment variable if set and not empty, else its line in the KEY=value file as Yap's Secrets.parseDotEnv reads it (comments, export, quotes, a later line wins); a missing one is failed notFound; the value appears in the request's header and in no reply, failure message or debug description.

The human half of claim ^975.

Assumed, never proved (^975 An environment secret is read from the environment or its file, and never shown): An environment secret's value is the environment variable if set and not empty, else its line in the KEY=value file as Yap's Secrets.parseDotEnv reads it (comments, export, quotes, a later line wins); a missing one is failed notFound; the value appears in the request's header and in no reply, failure message or debug description.

The human half of claim ^990.

^990 Wrapped lines paint as wide as Lean measured them (assumption)

On left-to-right text without controls or tabs, each line Lean's wrapping chose, shaped again on its own by the host, is within 1 + ceil(0.15 em) points of the width Lean took from the whole string's carets, and so fits the width up to that slack; laid lines sit at x 0, one line height apart.

Assumed, never proved (^990 Wrapped lines paint as wide as Lean measured them): On left-to-right text without controls or tabs, each line Lean's wrapping chose, shaped again on its own by the host, is within 1 + ceil(0.15 em) points of the width Lean took from the whole string's carets, and so fits the width up to that slack; laid lines sit at x 0, one line height apart.

The human half of claim ^991.

Assumed, never proved (^991 Lean breaks lines where Core Text would): On left-to-right letters, digits and spaces, Lean's lines are Core Text's (CTTypesetterSuggestLineBreak, trailing spaces trimmed) except where a line is within one point of the width or a word is cut, where the cut is within two scalars of Core Text's.

^991 Lean breaks lines where Core Text would (assumption)

On left-to-right letters, digits and spaces, Lean's lines are Core Text's (CTTypesetterSuggestLineBreak, trailing spaces trimmed) except where a line is within one point of the width or a word is cut, where the cut is within two scalars of Core Text's.

^1000 openItem opens exactly the URL or existing file it names (assumption)

openItem with a target that has a URL scheme asks the system to open that URL; with a path (a leading ~/ is the home folder) it opens that file or folder with its default app only when it exists, and answers notFound otherwise; it answers done exactly when the system took it, and an empty target or one with NUL is invalid and opens nothing.

Assumed, never proved (^1000 openItem opens exactly the URL or existing file it names): openItem with a target that has a URL scheme asks the system to open that URL; with a path (a leading ~/ is the home folder) it opens that file or folder with its default app only when it exists, and answers notFound otherwise; it answers done exactly when the system took it, and an empty target or one with NUL is invalid and opens nothing.

The human half of claim ^1000.

The human half of claim ^1001.

Assumed, never proved (^1001 appRunning answers whether an app with that bundle id runs): appRunning answers flag true exactly when the system lists a running, not terminated app with that bundle identifier; an empty identifier is invalid.

^1001 appRunning answers whether an app with that bundle id runs (assumption)

appRunning answers flag true exactly when the system lists a running, not terminated app with that bundle identifier; an empty identifier is invalid.

The human half of claim ^1002.

Assumed, never proved (^1002 readDefault answers the default's value as text): readDefault answers the value CFPreferences holds for the key in the domain as UTF-8 bytes: a string as it is, a boolean as 1 or 0, a number as its decimal text; a missing value is notFound, any other type and an empty domain or key invalid. It never writes a default.

^1002 readDefault answers the default's value as text (assumption)

readDefault answers the value CFPreferences holds for the key in the domain as UTF-8 bytes: a string as it is, a boolean as 1 or 0, a number as its decimal text; a missing value is notFound, any other type and an empty domain or key invalid. It never writes a default.

Assumed, never proved (^1003 makeDir makes a private directory and its parents): makeDir answers done only when the path is then a directory, each directory it made mode 700 whatever the umask, one already there done and left as it was; a file in the way, a path under a file, a read-only parent, NUL and the empty path fail.

The human half of claim ^1003.

^1003 makeDir makes a private directory and its parents (assumption)

makeDir answers done only when the path is then a directory, each directory it made mode 700 whatever the umask, one already there done and left as it was; a file in the way, a path under a file, a read-only parent, NUL and the empty path fail.

The human half of claim ^1004.

Assumed, never proved (^1004 A painter's pixels stay inside its box): A paint draw changes no pixel outside its rect (snapped to device pixels as rects are) within the clip in force, whatever its painter draws and whatever data, time or scale it is given; a paint naming no registered painter changes nothing. Checked offscreen against the same frame without its paint draws, with Yap's tape painter and painters whose triangles cover the whole target or land anywhere.

^1004 A painter's pixels stay inside its box (assumption)

A paint draw changes no pixel outside its rect (snapped to device pixels as rects are) within the clip in force, whatever its painter draws and whatever data, time or scale it is given; a paint naming no registered painter changes nothing. Checked offscreen against the same frame without its paint draws, with Yap's tape painter and painters whose triangles cover the whole target or land anywhere.

^1005 record reports started once its microphone is running, before any audio, or fails without it (assumption)

A record subscription's first event is started, sent once, only after the microphone's start has returned (the engine is running), and before every audio event of it, with the host's monotonic milliseconds (the clock of key events) read after the return; a microphone that can't start sends failed and never started. So an app that waits for started shows nothing for a microphone that fails, as Yap shows its overlay only once AudioCapture.start has returned.

The human half of claim ^1005.

Assumed, never proved (^1005 record reports started once its microphone is running, before any audio, or fails without it): A record subscription's first event is started, sent once, only after the microphone's start has returned (the engine is running), and before every audio event of it, with the host's monotonic milliseconds (the clock of key events) read after the return; a microphone that can't start sends failed and never started. So an app that waits for started shows nothing for a microphone that fails, as Yap shows its overlay only once AudioCapture.start has returned.

Assumed, never proved (^1006 loadImage answers the image's pixel size, or the fault): loadImage of a file path (~/ is home, relative to the working directory) or an http(s) URL decodes the first image with ImageIO, applying its EXIF orientation, keeps it for image draws naming the same source and answers image with the oriented pixel size, exactly once; a missing file is notFound, an unreadable one denied, a directory, an empty source, NUL or bytes that are no image invalid; HTTP 404 and 410 notFound, 401 and 403 denied, any other status outside 2xx other, a failed connection network, a timeout timeout. Without reload a kept source is answered from the store without reading; with reload it is read again, and a failure removes it.

^1006 loadImage answers the image's pixel size, or the fault (assumption)

loadImage of a file path (~/ is home, relative to the working directory) or an http(s) URL decodes the first image with ImageIO, applying its EXIF orientation, keeps it for image draws naming the same source and answers image with the oriented pixel size, exactly once; a missing file is notFound, an unreadable one denied, a directory, an empty source, NUL or bytes that are no image invalid; HTTP 404 and 410 notFound, 401 and 403 denied, any other status outside 2xx other, a failed connection network, a timeout timeout. Without reload a kept source is answered from the store without reading; with reload it is read again, and a failure removes it.

The human half of claim ^1006.

The human half of claim ^1007.

^1007 An image's pixels stay inside its box (assumption)

An image draw changes no pixel outside its rect (snapped to device pixels as rects are) within the clip in force, whatever its destination rect and scale; a draw naming a source the host holds no image for changes nothing.

Assumed, never proved (^1007 An image's pixels stay inside its box): An image draw changes no pixel outside its rect (snapped to device pixels as rects are) within the clip in force, whatever its destination rect and scale; a draw naming a source the host holds no image for changes nothing.

Assumed, never proved (^1008 An image is drawn where its oriented pixels are): An image draw scales the oriented image to its destination rect: each quadrant of the image lands in the same quadrant of the destination, in its colour (within 8 per channel, 40 for JPEG and HEIC), whatever the EXIF orientation, format and scale.

^1008 An image is drawn where its oriented pixels are (assumption)

An image draw scales the oriented image to its destination rect: each quadrant of the image lands in the same quadrant of the destination, in its colour (within 8 per channel, 40 for JPEG and HEIC), whatever the EXIF orientation, format and scale.

The human half of claim ^1008.

Assumed, never proved (^1009 cancelRequest stops a running request's work; it is still answered once): On cancelRequest for a request still running, the host stops its work where it can (an http, upload or loadImage download's URLSession task is cancelled) and still answers it exactly once, failed if the work was stopped, at once if its handler had not started; a cancelled loadImage leaves the image store as it was; a cancel of an id already answered or never requested does nothing.

^1009 cancelRequest stops a running request's work; it is still answered once (assumption)

On cancelRequest for a request still running, the host stops its work where it can (an http, upload or loadImage download's URLSession task is cancelled) and still answers it exactly once, failed if the work was stopped, at once if its handler had not started; a cancelled loadImage leaves the image store as it was; a cancel of an id already answered or never requested does nothing.

The human half of claim ^1009.

^1010 The window is never smaller than the app's minimum size (assumption)

The host sets the window's contentMinSize to the minimum size of the frame's window record (a negative side as 0), so a person can't drag it smaller, clamps every live resize AppKit proposes to it, and grows a window already smaller to it, keeping its top-left corner; a minimum the window meets leaves it alone. So every resize Lean hears is at least the minimum the app asked for, from the first frame that asks for it.

Assumed, never proved (^1010 The window is never smaller than the app's minimum size): The host sets the window's contentMinSize to the minimum size of the frame's window record (a negative side as 0), so a person can't drag it smaller, clamps every live resize AppKit proposes to it, and grows a window already smaller to it, keeping its top-left corner; a minimum the window meets leaves it alone. So every resize Lean hears is at least the minimum the app asked for, from the first frame that asks for it.

The human half of claim ^1010.

^1011 The image cache reports every image it drops, after it is gone (assumption)

While an imageCache subscription runs, the host keeps its decoded images within the smallest running budget: past it, it drops the images used least recently, never one the latest published frame draws nor the one just loaded, and sends evicted for every image it drops (a failed reload's removal too) after the pixels are gone. It answers loadImage ready only after it held the pixels for that load. With Images.evicted on the Lean side, an image the app takes for ready has its pixels with the host once every message is heard (Images.Cache.ready_held_quiet).

The human half of claim ^1011.

Assumed, never proved (^1011 The image cache reports every image it drops, after it is gone): While an imageCache subscription runs, the host keeps its decoded images within the smallest running budget: past it, it drops the images used least recently, never one the latest published frame draws nor the one just loaded, and sends evicted for every image it drops (a failed reload's removal too) after the pixels are gone. It answers loadImage ready only after it held the pixels for that load. With Images.evicted on the Lean side, an image the app takes for ready has its pixels with the host once every message is heard (Images.Cache.ready_held_quiet).

^1012 The host reports scrolls where they happen, toward the end positive (assumption)

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).

The human half of claim ^1012.

Assumed, never proved (^1012 The host reports scrolls where they happen, toward the end positive): 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).

Assumed, never proved (^1020 Secure event input is on exactly while a secure field has focus): 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.

The human half of claim ^1020.

^1020 Secure event input is on exactly while a secure field has focus (assumption)

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.

Assumed, never proved (^1021 Assistive apps reach only what a scroll area shows): The host's accessibility tree holds exactly the frame's AX nodes that are not scrolled out, each under its frame parent in frame order: a node is scrolled out when it or a node above it has an empty rect with a scroll area above that (the frame gives each node its visible rect, Frame.ofLaid). A scroll area is an AXScrollArea; a hit test answers only elements in the tree; the focused element is the focused node's even when it is scrolled out.

^1021 Assistive apps reach only what a scroll area shows (assumption)

The host's accessibility tree holds exactly the frame's AX nodes that are not scrolled out, each under its frame parent in frame order: a node is scrolled out when it or a node above it has an empty rect with a scroll area above that (the frame gives each node its visible rect, Frame.ofLaid). A scroll area is an AXScrollArea; a hit test answers only elements in the tree; the focused element is the focused node's even when it is scrolled out.

The human half of claim ^1021.

Assumed, never proved (^1022 A secure field shows assistive apps nothing typed): A frame node marked secure is an AXTextField with subrole AXSecureTextField, no value, no characters, no selected text and an empty string for every range, whatever its node or the text input holds; no other element shows its text. The debug socket's description of an http request shows no header value, body or secret, and no URL when the request is redact.

The human half of claim ^1022.

^1022 A secure field shows assistive apps nothing typed (assumption)

A frame node marked secure is an AXTextField with subrole AXSecureTextField, no value, no characters, no selected text and an empty string for every range, whatever its node or the text input holds; no other element shows its text. The debug socket's description of an http request shows no header value, body or secret, and no URL when the request is redact.

^1030 The badge the host shows is the label of the last badge effect, or none (assumption)

The host sets the Dock tile's badge label (NSApp.dockTile.badgeLabel) to exactly the label of each badge effect, as it is, in the order the frames hand them over, and clears it for badge none; it never sets the badge otherwise. So the badge shown is the label of the last badge effect, or none.

The human half of claim ^1030.

Assumed, never proved (^1030 The badge the host shows is the label of the last badge effect, or none): The host sets the Dock tile's badge label (NSApp.dockTile.badgeLabel) to exactly the label of each badge effect, as it is, in the order the frames hand them over, and clears it for badge none; it never sets the badge otherwise. So the badge shown is the label of the last badge effect, or none.

^1031 An announcement is posted once, with exactly its text (assumption)

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.

The human half of claim ^1031.

Assumed, never proved (^1031 An announcement is posted once, with exactly its text): 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.

^1032 Under holdWorld the host sends no clock, wake or reply of its own (assumption)

Once Engine.holdClock and World.holdRequests have returned, every batch Lean hears is exactly the events the caller sent, in order (the driver's clock and reply events among them): the host adds no clock, sends no wake whatever the frame's wake deadline, and runs and answers no request handed over afterwards; a request from before the hold is answered at most once. Lean never hears an empty batch.

Assumed, never proved (^1032 Under holdWorld the host sends no clock, wake or reply of its own): Once Engine.holdClock and World.holdRequests have returned, every batch Lean hears is exactly the events the caller sent, in order (the driver's clock and reply events among them): the host adds no clock, sends no wake whatever the frame's wake deadline, and runs and answers no request handed over afterwards; a request from before the hold is answered at most once. Lean never hears an empty batch.

The human half of claim ^1032.