Cairn
Docs
Claims
Blog
Packages
Claims · cairn
cairn 0.5.2: claims
Everything cairn 0.5.2 claims a person can do and see, and what holds, by place, each with its evidence.
6 retired115 moved63 assumed15 proved
Not in a place
Moves and flows that name no place.
| Id | Kind | Claim | Reads as |
|---|---|---|---|
cairn^215 | move | Back through filters | retired |
cairn^1100 | move | Set a valueThe person flips key k (likes or unlikes it). | proved |
cairn^1101 | move | The server handles a requestThe server handles the i-th packet in the network: applies a write (its answer becomes acked) or answers a read with what it holds. | proved |
cairn^1102 | move | The server refuses a requestThe server refuses the i-th packet in the network, and changes nothing. | proved |
cairn^1103 | move | An answer arrivesThe network delivers the i-th packet, an answer or a view, to the table. | proved |
cairn^1104 | move | A request or answer is lostThe network loses the i-th packet, before or after the server handled it; the table hears lost (a write) or readFailed (a read). | proved |
cairn^1105 | move | A retry comes dueKey k's backoff timer fires. | proved |
cairn^1106 | move | A view is fetchedThe app fetches a view of key k: what the server holds now, delivered whenever (^1103). | proved |
Invariants
What holds in every state the app can reach.
| Id | Claim | Reads as |
|---|---|---|
cairn^6 | Moves never leave a press in progress | retired |
cairn^213 | The list is the filter applied to the todos | retired |
cairn^225 | The list is the filter applied to the todos | retired |
cairn^1107 | A set shows in its own stepWhatever is in flight or in doubt, setting a key to f of what it shows makes it show exactly that in the same step: what is shown is want, and a set changes want at once. | proved |
cairn^1108 | At most one write in flight per keyFor every key, at most one write is in the network, before or after the server handled it: a set while one is in flight only changes what is shown. | proved |
cairn^1109 | Never more writes than setsFor every key, the writes the table has sent never outnumber the person's sets of it, whatever answers came back in whatever order: a lost write is read back, never sent again blind. | proved |
cairn^1110 | A refusal rolls back in its stepWhen a key's write in flight is refused, the key shows the server's last confirmed value in that step, that value is unchanged, and nothing is outstanding for the key. | proved |
cairn^1111 | Settled keys show what the server holdsAgainst a server that is a register per key with idempotent writes, for any sequence of sets and any interleaving of replies (each acknowledged, refused, or lost before or after the server applied it, delivered in any order, with views fetched at any time), every key with nothing in flight and nothing in doubt shows what the server holds. So once every reply is in, every key does. | proved |
cairn^1112 | Replies for different keys commuteTwo inputs about different keys, in either order, leave the table the same at every key, and each gives the outputs it gives alone, so the two orders' outputs are the same two lists swapped. | proved |
cairn^1113 | A settled count is the server'sFor a view whose count is other people's o plus the person's own [v], a settled key shows o + [what the server holds]: exactly the server's count when no one else acted since the view. The count shown, c − [v] + [shown], is never below zero, and never below the person's own [shown]. | proved |
cairn^1114 | A view never moves a written keyA value in a view the app fetched, which may be stale (fetched before a write, or from a server that hasn't indexed it yet), never changes what a key written this session shows, or its confirmed value. | proved |
Assumptions
What the proofs rely on and nothing proves: the host, the OS and the hardware behaving as stated. Cairn's own are its trusted base (docs).
Cairn.Fuzz.Trusted.Claims
| Id | Claim | Reads as |
|---|---|---|
cairn^7 | The host reports clicks where they happenThe host sends a pointer down and up at the logical point the person clicked, in order. | assumed |
cairn^214 | The host reports a double click as a second clickThe 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 |
cairn^901 | The Swift frame decoder agrees with Lean'sFor every byte buffer, the host's Frame(bytes:) accepts exactly when Lean's proved decodeFrame does, and then decodes the same frame. | assumed |
cairn^902 | Lean decodes what the Swift event encoder writesFor 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. | assumed |
cairn^903 | UTF-16 offsets and scalar indices convert exactlyTextIndex 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. | assumed |
cairn^904 | The text-input shadow predicts Lean's fieldBetween 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 |
cairn^905 | Input-method geometry agrees with Lean's caretselectedRange 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. | assumed |
cairn^906 | The host's text metrics are what layout assumescairn_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. | assumed |
cairn^907 | Carets follow the painted glyphsOn left-to-right text, the caret offset after each grapheme is at or right of every glyph painted for the text before it. | assumed |
cairn^908 | The host's clock is monotonic millisecondsEvery 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 |
cairn^909 | The host wakes Lean by wakeWhen 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 |
cairn^910 | readFile replies with the file's bytes, or failedreadFile 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. | assumed |
cairn^911 | writeFile is atomic, and replies done only when the bytes are therewriteFile 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 |
cairn^912 | playSound starts a known sound and refuses an unknown oneplaySound finds every system sound by its name and answers done once it starts; any other name is answered notFound, once, without playing anything. | assumed |
cairn^913 | http sends the request as given and returns the response as received | retired |
cairn^914 | The host answers every request exactly once, with its idEvery 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. | assumed |
cairn^915 | every ms ticks while started and never after it is stoppedAn 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 |
cairn^940 | The native menu shows exactly the frame's menu recordsAfter 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 |
cairn^941 | Choosing a menu item reports that item's refWhen 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). | assumed |
cairn^942 | Opening and closing the menu are reported once eachWhen 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 |
cairn^943 | An overlay panel never takes focus or clicksEvery 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. | assumed |
cairn^944 | An overlay panel is where its anchor saysA 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. | assumed |
cairn^945 | A control's menu shows exactly the frame's menu recordsWhile 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. | assumed |
cairn^946 | Choosing a control menu's item reports its ref, then the closeWhen 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 |
cairn^947 | The host shows a control menu only while Lean has it openThe 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 |
cairn^948 | AXShowMenu opens a control's menu as a right click doesAn 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. | assumed |
cairn^949 | The menu bar shows the app's menu itemsAfter 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 |
cairn^950 | A menu bar item, by click or key equivalent, reports that item's refWhen 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 |
cairn^960 | appendFile adds exactly the bytes at the end, or fails and adds nothingappendFile 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. | assumed |
cairn^961 | listDir lists exactly the directory's names, sortedlistDir 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. | assumed |
cairn^962 | deleteFile removes a file or a link, never a directorydeleteFile 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. | assumed |
cairn^963 | watchFile reports every change to its file, and nothing after its stopWhile 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 |
cairn^964 | frontmostApp answers the app in frontfrontmostApp 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. | assumed |
cairn^965 | permission answers whether the app holds it, and prompts only when askedpermission 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 |
cairn^966 | record streams the levels of exactly the samples it keeps, and nothing after its stopWhile 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 |
cairn^967 | A clip's WAV for a range of windows holds exactly those samplesAn 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 |
cairn^968 | globalKey reports the hotkey's press and release, and other keys while it is heldA 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 |
cairn^969 | typeText types exactly the text into that app, or nothingtypeText 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. | assumed |
cairn^970 | upload sends the body assembled from its parts, with the secret in its headerupload 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 |
cairn^971 | A secret is read from the environment or its file, and never shown | retired |
cairn^972 | The Keychain keeps what it was given for this appThe 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. | assumed |
cairn^973 | Captured reply fields go to the Keychain and never to LeanFor 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. | assumed |
cairn^974 | http sends the request as given, with its secret header, and returns the response as receivedhttp 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 |
cairn^975 | An environment secret is read from the environment or its file, and never shownAn 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. | assumed |
cairn^990 | Wrapped lines paint as wide as Lean measured themOn 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 |
cairn^991 | Lean breaks lines where Core Text wouldOn 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. | assumed |
cairn^1000 | openItem opens exactly the URL or existing file it namesopenItem 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 |
cairn^1001 | appRunning answers whether an app with that bundle id runsappRunning answers flag true exactly when the system lists a running, not terminated app with that bundle identifier; an empty identifier is invalid. | assumed |
cairn^1002 | readDefault answers the default's value as textreadDefault 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 |
cairn^1003 | makeDir makes a private directory and its parentsmakeDir 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. | assumed |
cairn^1004 | A painter's pixels stay inside its boxA 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. | assumed |
cairn^1005 | record reports started once its microphone is running, before any audio, or fails without itA 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 |
cairn^1006 | loadImage answers the image's pixel size, or the faultloadImage 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. | assumed |
cairn^1007 | An image's pixels stay inside its boxAn 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 |
cairn^1008 | An image is drawn where its oriented pixels areAn 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. | assumed |
cairn^1009 | cancelRequest stops a running request's work; it is still answered onceOn 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. | assumed |
cairn^1010 | The window is never smaller than the app's minimum sizeThe 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 |
cairn^1011 | The image cache reports every image it drops, after it is goneWhile 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). | assumed |
cairn^1012 | The host reports scrolls where they happen, toward the end positiveThe 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 |
cairn^1020 | Secure event input is on exactly while a secure field has focusThe 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 |
cairn^1021 | Assistive apps reach only what a scroll area showsThe 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. | assumed |
cairn^1022 | A secure field shows assistive apps nothing typedA 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. | assumed |
cairn^1030 | The badge the host shows is the label of the last badge effect, or noneThe 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. | assumed |
cairn^1031 | An announcement is posted once, with exactly its textFor 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. | assumed |
cairn^1032 | Under holdWorld the host sends no clock, wake or reply of its ownOnce 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 |
Moved to other packages
Ids this package issued and another now owns. They stay issued here and can't come back.
| Id | Kind | Claim | Now in |
|---|---|---|---|
cairn^1 | move | Increment | cairn_examples^1 |
cairn^2 | move | Reset | cairn_examples^2 |
cairn^3 | place | Counter window | cairn_examples^3 |
cairn^4 | flow | Count to three | cairn_examples^4 |
cairn^5 | flow | Start over | cairn_examples^5 |
cairn^101 | move | Type a new item | cairn_examples^101 |
cairn^102 | move | Add | cairn_examples^102 |
cairn^103 | move | Toggle an item | cairn_examples^103 |
cairn^104 | move | Delete an item | cairn_examples^104 |
cairn^105 | invariant | Items left | cairn_examples^105 |
cairn^106 | place | Basics window | cairn_examples^106 |
cairn^107 | flow | Add two items and finish one | cairn_examples^107 |
cairn^108 | flow | Blank text adds nothing | cairn_examples^108 |
cairn^109 | flow | Add an item, then delete it | cairn_examples^109 |
cairn^201 | place | Todos window | cairn_examples^201 |
cairn^202 | move | New todo | cairn_examples^202 |
cairn^203 | move | Mark all as complete | cairn_examples^203 |
cairn^204 | move | Complete a todo | cairn_examples^204 |
cairn^205 | move | Edit a todo | cairn_examples^205 |
cairn^206 | move | Delete a todo | cairn_examples^206 |
cairn^207 | move | Edit field | cairn_examples^207 |
cairn^208 | move | All | cairn_examples^208 |
cairn^209 | move | Active | cairn_examples^209 |
cairn^210 | move | Completed | cairn_examples^210 |
cairn^211 | move | Clear completed | cairn_examples^211 |
cairn^212 | invariant | Counter and ids | cairn_examples^212 |
cairn^216 | flow | Add two todos and complete one | cairn_examples^216 |
cairn^217 | flow | Blank text adds nothing | cairn_examples^217 |
cairn^218 | flow | Edit a todo and save with Enter | cairn_examples^218 |
cairn^219 | flow | Saving a blank edit deletes the todo | cairn_examples^219 |
cairn^220 | flow | Escape cancels an edit | cairn_examples^220 |
cairn^221 | flow | The Active filter hides completed todos | cairn_examples^221 |
cairn^222 | flow | Clear completed | cairn_examples^222 |
cairn^223 | flow | Mark all as complete, then undo it | cairn_examples^223 |
cairn^224 | flow | A new todo under the Completed filter | cairn_examples^224 |
cairn^226 | invariant | The list is the filter applied to the todos | cairn_examples^226 |
cairn^301 | place | Menu bar menu | yap^301 |
cairn^302 | move | Copy Last Transcript | yap^302 |
cairn^303 | move | Recent transcript | yap^303 |
cairn^304 | move | Keep Transcripts | yap^304 |
cairn^305 | move | Press Return After Dictating | yap^305 |
cairn^306 | move | Dictate with Key | yap^306 |
cairn^307 | move | Open Transcripts Folder | yap^307 |
cairn^308 | move | Edit Dictionary | yap^308 |
cairn^309 | move | Edit Settings | yap^309 |
cairn^310 | move | Grant Accessibility Access | yap^310 |
cairn^311 | invariant | A shortcut never sends | yap^311 |
cairn^312 | invariant | Hold to talk, tap to latch: 300 ms | yap^312 |
cairn^313 | invariant | One recording at a time | yap^313 |
cairn^314 | invariant | Every recording ends | yap^314 |
cairn^315 | invariant | Kept before it is typed | yap^315 |
cairn^316 | invariant | A failed type is kept and flagged | yap^316 |
cairn^317 | invariant | Late and cancelled replies never type | yap^317 |
cairn^318 | invariant | Each clip is typed at most once | yap^318 |
cairn^319 | invariant | Fixes replace whole words | yap^319 |
cairn^320 | invariant | Retention never deletes today | yap^320 |
cairn^321 | invariant | Only the first 25 terms are sent | yap^321 |
cairn^322 | invariant | Recent Transcripts holds five | yap^322 |
cairn^323 | invariant | Too short, silent or nowhere to type: never sent | yap^323 |
cairn^330 | assume | The host reports the dictation key and every other key | yap^330 |
cairn^331 | assume | The host delivers the ticks it is asked for | yap^331 |
cairn^332 | assume | The host answers requests by id, in order of commands | yap^332 |
cairn^333 | assume | The host reports the microphone faithfully | yap^333 |
cairn^334 | assume | The host transcribes the samples it was asked for | yap^334 |
cairn^335 | assume | The host types into the app it was given | yap^335 |
cairn^336 | assume | The host reports config.json and dictionary.txt when they change | yap^336 |
cairn^337 | assume | The host lists day files and today by the local calendar | yap^337 |
cairn^340 | flow | Turn Dictate with Key off | yap^340 |
cairn^341 | flow | Keep Transcripts off and on again | yap^341 |
cairn^342 | move | Quit Yap (Cairn) | yap^342 |
cairn^343 | move | Grant Microphone Access | yap^343 |
cairn^344 | move | Open the menu | yap^344 |
cairn^345 | place | Overlay panel | yap^345 |
cairn^346 | invariant | The original Yap keeps its key | yap^346 |
cairn^347 | invariant | A mark waits for the appends | yap^347 |
cairn^348 | assume | The host reports the microphone's start or its failure | yap^348 |
cairn^349 | invariant | The overlay waits for the microphone | yap^349 |
cairn^350 | invariant | Keys wait for the microphone | yap^350 |
cairn^351 | invariant | Hold to talk, tap to latch: 300 ms, timed as the original | yap^351 |
cairn^399 | place | Overlay panel | yap^399 |
cairn^401 | move | Start / Stop | cairn_examples^401 |
cairn^402 | move | Lap | cairn_examples^402 |
cairn^403 | move | Reset | cairn_examples^403 |
cairn^404 | move | Save laps | cairn_examples^404 |
cairn^405 | move | Load laps | cairn_examples^405 |
cairn^406 | place | Clock window | cairn_examples^406 |
cairn^407 | flow | Two laps | cairn_examples^407 |
cairn^408 | flow | Start over | cairn_examples^408 |
cairn^409 | invariant | Pending requests have fresh ids | cairn_examples^409 |
cairn^450 | place | Tray menu | cairn_examples^450 |
cairn^451 | place | Recent Items submenu | cairn_examples^451 |
cairn^452 | place | Overlay panel | cairn_examples^452 |
cairn^453 | move | Open the menu | cairn_examples^453 |
cairn^454 | move | Show Overlay | cairn_examples^454 |
cairn^455 | move | Keep Recent Items | cairn_examples^455 |
cairn^456 | move | Add Item | cairn_examples^456 |
cairn^457 | move | Recent item | cairn_examples^457 |
cairn^458 | move | Clear Recent Items | cairn_examples^458 |
cairn^459 | move | Quit Tray | cairn_examples^459 |
cairn^460 | invariant | At most five recent items | cairn_examples^460 |
cairn^461 | flow | Show the overlay | cairn_examples^461 |
cairn^462 | flow | Add an item and pick it | cairn_examples^462 |
cairn^501 | move | Reload | cairn_examples^501 |
cairn^502 | move | Fit | cairn_examples^502 |
cairn^503 | place | Gallery window | cairn_examples^503 |
cairn^504 | invariant | Pending loads have fresh ids | cairn_examples^504 |
cairn^505 | flow | Reload, then fit inside | cairn_examples^505 |
cairn^506 | move | Load 24 | cairn_examples^506 |
cairn^507 | move | Cancel | cairn_examples^507 |
cairn^508 | flow | Load many, then cancel | cairn_examples^508 |
cairn^509 | move | Reload a tile | cairn_examples^509 |
cairn^510 | invariant | Tiles fit the window at every size | cairn_examples^510 |
cairn^511 | invariant | Tiles are at least 180 points wide | cairn_examples^511 |
cairn^512 | move | Next page | cairn_examples^512 |
cairn^513 | invariant | A dropped thumbnail waits to be loaded again | cairn_examples^513 |