Cairn Docs Claims Blog Packages

Claims · cairn

cairn 0.2.1: claims

Everything cairn 0.2.1 claims a person can do and see, and what holds, by place, each with its evidence.

3 retired44 moved46 assumed60 proved8 no proof

Counter window cairn^3

The counter's window: a bar as long as the count, Increment, and Reset when there is something to reset.

Moves

IdClaimReads as
cairn^1IncrementPress Increment.proved
cairn^2ResetPress Reset.proved

Flows

IdClaimReads as
cairn^4Count to threePress Increment three times.proved
cairn^5Start overCount up, then press Reset.proved

Basics window cairn^106

The window: a heading, the New item field and Add, the list of items, and the count of items left.

Moves

IdClaimReads as
cairn^101Type a new itemType in the New item field, and press Enter.proved
cairn^102AddPress Add.proved
cairn^103Toggle an itemPress an item's checkbox.proved
cairn^104Delete an itemPress an item's delete button.proved

Flows

IdClaimReads as
cairn^107Add two items and finish oneType milk and press Enter, type eggs and press Add, then check milk.proved
cairn^108Blank text adds nothingType spaces, then press Enter and Add.proved
cairn^109Add an item, then delete itType milk, press Add, then press milk's delete button.proved

Todos window cairn^201

The window: the heading, toggle all and the new-todo field, the listed todos, the footer with the counter, filters and Clear completed, and the info line.

Moves

IdClaimReads as
cairn^202New todoType in the What needs to be done? field, and press Enter. (T5–T13)proved
cairn^203Mark all as completePress the toggle-all checkbox. (T14–T17)proved
cairn^204Complete a todoPress a todo's checkbox. (T19, T42)proved
cairn^205Edit a todoDouble-click a todo's title. (T20, T25–T27)proved
cairn^206Delete a todoPress a todo's delete button (×, drawn while the pointer is over the row or the button has keyboard focus). (T21, T22, T49)proved
cairn^207Edit fieldIn edit mode, type in the todo's field; then press Enter, click elsewhere or Tab away, or press Escape. (T28–T31, T50)proved
cairn^208AllPress the All filter. (T39–T43)proved
cairn^209ActivePress the Active filter. (T39–T43)proved
cairn^210CompletedPress the Completed filter. (T39–T43)proved
cairn^211Clear completedPress Clear completed, shown while some todo is completed. (T37, T38)proved

Flows

IdClaimReads as
cairn^216Add two todos and complete oneType milk and press Enter, type eggs with spaces around it and press Enter, then check milk.proved
cairn^217Blank text adds nothingType spaces and press Enter.proved
cairn^218Edit a todo and save with EnterAdd milk, double-click it, select all, type oat milk with spaces around it, press Enter.proved
cairn^219Saving a blank edit deletes the todoAdd milk, double-click it, delete its text, and click elsewhere.proved
cairn^220Escape cancels an editAdd milk, double-click it, delete its text, press Escape.proved
cairn^221The Active filter hides completed todosAdd milk and eggs, check milk, press Active.proved
cairn^222Clear completedAdd milk and eggs, check milk, press Clear completed.proved
cairn^223Mark all as complete, then undo itAdd milk and eggs, check milk, press toggle all twice.proved
cairn^224A new todo under the Completed filterAdd milk, press Completed, add eggs.proved

Clock window cairn^406

The stopwatch's window: the reading, the time of day, Start/Stop, Lap, Reset, Save laps, Load laps, a status line and the laps.

Moves

IdClaimReads as
cairn^401Start / StopPress Start (Stop while running).proved
cairn^402LapPress Lap while the stopwatch runs.proved
cairn^403ResetPress Reset while stopped.proved
cairn^404Save lapsPress Save laps.proved
cairn^405Load lapsPress Load laps.proved

Flows

IdClaimReads as
cairn^407Two lapsPress Start, then Lap twice.proved
cairn^408Start overPress Start, Lap, Stop, then Reset.proved

Tray menu cairn^450

The menu of Tray's menu bar item: the status line, Show or Hide Overlay, Keep Recent Items, Add Item, the Recent Items submenu and Quit Tray.

Moves

IdClaimReads as
cairn^453Open the menuClick Tray's menu bar item.proved
cairn^454Show OverlayChoose Show Overlay (Hide Overlay while it is shown), or press ⌘O with the menu open.proved
cairn^455Keep Recent ItemsChoose Keep Recent Items.proved
cairn^456Add ItemChoose Add Item while Keep Recent Items is on.proved
cairn^459Quit TrayChoose Quit Tray, or press ⌘Q with the menu open.proved

Flows

IdClaimReads as
cairn^461Show the overlayOpen the menu and choose Show Overlay.proved
cairn^462Add an item and pick itChoose Add Item, then the new item under Recent Items.proved

Recent Items submenu cairn^451

The Recent Items submenu: the recent items, newest first (or None yet), then Clear Recent Items.

Moves

IdClaimReads as
cairn^457Recent itemChoose an item under Recent Items.proved
cairn^458Clear Recent ItemsChoose Clear Recent Items under Recent Items, while there are some.proved

Overlay panel cairn^452

A panel at the bottom of the screen, over every app, that never takes focus or clicks: a row of moving bars and a line of text. Shown and hidden from the menu.

No claim names this place.

Gallery window cairn^503

Six image tiles in a grid, each with its name and pixel size or fault, under a header with Fit and Reload.

Moves

IdClaimReads as
cairn^501ReloadPress Reload.proved
cairn^502FitPress Fit.proved
cairn^506Load 24Press Load 24.proved
cairn^507CancelPress Cancel.proved
cairn^509Reload a tilePress a tile.proved

Flows

IdClaimReads as
cairn^505Reload, then fit insidePress Reload, then Fit.proved
cairn^508Load many, then cancelPress Load 24, then Cancel.proved

Not in a place

Moves and flows that name no place.

IdKindClaimReads as
cairn^215moveBack through filtersretired

Invariants

What holds in every state the app can reach.

IdClaimReads as
cairn^6Moves never leave a press in progressretired
cairn^105Items leftThe footer's count equals the number of items not done, and item ids stay distinct, in every reachable state.proved
cairn^212Counter and idsThe counter shows the number of active todos, over all todos; todo ids are distinct, in every reachable state. (T24, T34)proved
cairn^213The list is the filter applied to the todosretired
cairn^225The list is the filter applied to the todosThe rows on screen are exactly the todos the selected filter accepts, in creation order, under any hover and focus, in every reachable state. (T40, T42)proved
cairn^409Pending requests have fresh idsThe pending save and load, if any, have ids below the next request's, so a reply to a later request is never taken for theirs.proved
cairn^460At most five recent itemsRecent Items never lists more than five items, however many are added.proved
cairn^504Pending loads have fresh idsEvery load waiting for its reply has an id below the next request's, so a reply to a later load is never taken for an earlier one.proved
cairn^510Tiles fit the window at every sizeAt every window size the tiles don't overlap, read left to right and top to bottom, and stay inside the window; resizing reflows them.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).

Examples.Counter

IdClaimReads as
cairn^7The host reports clicks where they happenThe host sends a pointer down and up at the logical point the person clicked, in order.assumed

Examples.Todo

IdClaimReads as
cairn^214The 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.Fuzz.Trusted.Claims

IdClaimReads as
cairn^901The 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^902Lean 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^903UTF-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^904The 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^905Input-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^906The 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^907Carets 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^908The 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^909The 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^910readFile 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^911writeFile 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^912playSound 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^913http sends the request as given and returns the response as receivedhttp sends the method, URL, headers and body as given and answers with the response's status, headers sorted by name and body exactly; a connection failure is network, no answer in time is timeout, and a non-http URL, a bad method or a header that could inject another is invalid and sends nothing.assumed
cairn^914The 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^915every 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^940The 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^941Choosing 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^942Opening 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^943An 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^944An 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^960appendFile 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^961listDir 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^962deleteFile 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^963watchFile 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^964frontmostApp 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^965permission 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^966record 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^967A 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^968globalKey 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^969typeText 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^970upload 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^971A secret is read from the environment or its file, and never shownA 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^990Wrapped 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^991Lean 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^1000openItem 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^1001appRunning 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^1002readDefault 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^1003makeDir 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^1004A 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^1005record 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^1006loadImage 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^1007An 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^1008An 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^1009cancelRequest 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

Moved to other packages

Ids this package issued and another now owns. They stay issued here and can't come back.

IdKindClaimNow in
cairn^301placeMenu bar menuyap^301
cairn^302moveCopy Last Transcriptyap^302
cairn^303moveRecent transcriptyap^303
cairn^304moveKeep Transcriptsyap^304
cairn^305movePress Return After Dictatingyap^305
cairn^306moveDictate with Keyyap^306
cairn^307moveOpen Transcripts Folderyap^307
cairn^308moveEdit Dictionaryyap^308
cairn^309moveEdit Settingsyap^309
cairn^310moveGrant Accessibility Accessyap^310
cairn^311invariantA shortcut never sendsyap^311
cairn^312invariantHold to talk, tap to latch: 300 msyap^312
cairn^313invariantOne recording at a timeyap^313
cairn^314invariantEvery recording endsyap^314
cairn^315invariantKept before it is typedyap^315
cairn^316invariantA failed type is kept and flaggedyap^316
cairn^317invariantLate and cancelled replies never typeyap^317
cairn^318invariantEach clip is typed at most onceyap^318
cairn^319invariantFixes replace whole wordsyap^319
cairn^320invariantRetention never deletes todayyap^320
cairn^321invariantOnly the first 25 terms are sentyap^321
cairn^322invariantRecent Transcripts holds fiveyap^322
cairn^323invariantToo short, silent or nowhere to type: never sentyap^323
cairn^330assumeThe host reports the dictation key and every other keyyap^330
cairn^331assumeThe host delivers the ticks it is asked foryap^331
cairn^332assumeThe host answers requests by id, in order of commandsyap^332
cairn^333assumeThe host reports the microphone faithfullyyap^333
cairn^334assumeThe host transcribes the samples it was asked foryap^334
cairn^335assumeThe host types into the app it was givenyap^335
cairn^336assumeThe host reports config.json and dictionary.txt when they changeyap^336
cairn^337assumeThe host lists day files and today by the local calendaryap^337
cairn^340flowTurn Dictate with Key offyap^340
cairn^341flowKeep Transcripts off and on againyap^341
cairn^342moveQuit Yap (Cairn)yap^342
cairn^343moveGrant Microphone Accessyap^343
cairn^344moveOpen the menuyap^344
cairn^345placeOverlay panelyap^345
cairn^346invariantThe original Yap keeps its keyyap^346
cairn^347invariantA mark waits for the appendsyap^347
cairn^348assumeThe host reports the microphone's start or its failureyap^348
cairn^349invariantThe overlay waits for the microphoneyap^349
cairn^350invariantKeys wait for the microphoneyap^350
cairn^351invariantHold to talk, tap to latch: 300 ms, timed as the originalyap^351
cairn^399placeOverlay panelyap^399