Cairn
Docs
Claims
Blog
Packages
Claims · yap
yap 0.1.0: claims
Everything yap 0.1.0 claims a person can do and see, and what holds, by place, each with its evidence.
2 retired9 assumed31 proved2 no proof
Menu bar menu yap^301
Yap's menu bar menu: the status line, Copy Last Transcript, Recent Transcripts, Keep Transcripts, Press Return After Dictating, Dictate with Key, Open Transcripts Folder, Edit Dictionary, Edit Settings, and Grant Accessibility Access while it is missing.
Moves
| Id | Claim | Reads as |
|---|---|---|
yap^302 | Copy Last TranscriptChoose Copy Last Transcript. | proved |
yap^303 | Recent transcriptChoose a transcript under Recent Transcripts (the newest first, five at most). | proved |
yap^304 | Keep TranscriptsChoose Keep Transcripts. | proved |
yap^305 | Press Return After DictatingChoose Press Return After Dictating, available while Dictate with Key is on. | proved |
yap^306 | Dictate with KeyChoose Dictate with Key. | proved |
yap^307 | Open Transcripts FolderChoose Open Transcripts Folder. | proved |
yap^308 | Edit DictionaryChoose Edit Dictionary. | proved |
yap^309 | Edit SettingsChoose Edit Settings. | proved |
yap^310 | Grant Accessibility AccessChoose Grant Accessibility Access, shown while Yap can't type. | proved |
yap^342 | Quit Yap (Cairn)Choose Quit Yap (Cairn), or press ⌘Q with the menu open. | proved |
yap^343 | Grant Microphone AccessChoose Grant Microphone Access, shown while the microphone is denied. | proved |
yap^344 | Open the menuClick Yap's menu bar item. | proved |
Flows
| Id | Claim | Reads as |
|---|---|---|
yap^340 | Turn Dictate with Key offChoose Dictate with Key. | proved |
yap^341 | Keep Transcripts off and on againChoose Keep Transcripts twice. | proved |
Overlay panel yap^345 retired
No claim names this place.
Overlay panel yap^399
Yap's panel at the bottom of the screen, over every app, that never takes focus or clicks, drawn as the original's: the phase (REC, hands free, transcribing, typed, not typed) with a glowing dot and a clock that stops when recording does, the tape (the original's shader: the scope, the ruler, the reel and the meter, from the microphone's levels and the preview's cuts) and the live transcript's last 280 characters; when the text changes the panel eases to its new height over 0.15 s as the original's does, new text fading in and old text fading out. Hidden 1.5 s after a transcript is typed and 4 s after one fails.
No claim names this place.
Invariants
What holds in every state the app can reach.
| Id | Claim | Reads as |
|---|---|---|
yap^311 | A shortcut never sendsWhile the dictation key is held and another key has gone down with it (a shortcut such as the key plus C), nothing the host reports leads to a clip's upload for transcription: not the key's release, not a new key in config.json, not a reply, and never the menu. Only the clock (or a timer) can, for a hands-free recording that hits its ten-minute limit (`app_shortcut_never_sends`, `shortcut_never_sends`). | proved |
yap^312 | Hold to talk, tap to latch: 300 ms | retired |
yap^313 | One recording at a timeThe app records exactly while the machine has a recording: one `record` subscription, for its clip. Whatever the host reports, a recording the machine didn't have is the next clip, started when there was none; the menu only ever stops one (`record_sub_iff`, `app_new_recording`, `step_new_recording`). | proved |
yap^314 | Every recording endsA recording is either held down or hands free with its deadline at most ten minutes away; so once the key's release is heard and the clock reads ten minutes on, there is no recording. A release that comes while the microphone is starting waits for the start; if the start is never reported, the recording is given up ten minutes after that release (the original would wait forever: see docs/yap-parity.md). A recording held down has no limit, as in Swift Yap (`step_recInv`, `keyUp_tick_none`, `app_recording_ends`). | proved |
yap^315 | Kept before it is typedWhen Yap types a transcript, it is already in Recent Transcripts, marked not yet typed, and when transcripts are kept the request appending it to its day file comes before the request typing it (`app_saved_before_typed`, `saved_before_typed`). Swift Yap saves after typing; see the README. | proved |
yap^316 | A failed type is kept and flaggedWhen typing fails, the transcript is first in Recent Transcripts (so Copy Last Transcript copies it), marked as never having reached its app, and the error sound plays (`app_failed_type_flagged`). | proved |
yap^317 | Late and cancelled replies never typeOnly a reply to a whole-clip transcription that is still in flight, and was not cancelled since it was sent, types anything; a duplicate, a reply to something else, or a reply after Dictate with Key was turned off types nothing (`app_only_live_replies_type`, `late_reply_never_types`). | proved |
yap^318 | Each clip is typed at most onceHowever replies arrive (late, twice, out of order, or never), and whatever else the host reports, no clip's transcript has been typed twice: the app's log of typed clips counts each at most once (`TypedInv`, `step_rel`). | proved |
yap^319 | Fixes replace whole wordsWhat is typed is the text of a successful transcription reply with each dictionary fix applied to whole words only, case-insensitively, then trimmed, then a space (or Return) (`app_typed_text`, `typed_text`, `replaceWord_replaces`). | proved |
yap^320 | Retention never deletes todayThe only day files deleted are ones the host listed that are older than today by the clock; today's is never deleted, whatever retentionDays says (`app_retention_never_today`, `retention_never_today`). | proved |
yap^321 | Only the first 25 terms are sentEvery upload is a transcription, of a whole clip or a preview chunk, whose prompt is the one a dictionary of just its first 25 terms would give (`app_prompt`, `step_prompt`). | proved |
yap^322 | Recent Transcripts holds fiveThe recent list never holds more than five transcripts (`step_small`, `menu_small`). | proved |
yap^323 | Too short, silent or nowhere to type: never sentEvery whole-clip upload is of the recording in progress, at least 0.3 s long, with a sample at or above the silence peak, and with an app to type into (`app_sendable`, `step_transcribe`). | proved |
yap^346 | The original Yap keeps its keyYap (Cairn) takes the dictation key only once it has checked that the original Yap (dev.yap.Yap) is not running: while it runs, or before the check is answered, there is no global key subscription, and the menu says so (`wantsKey`). | proved |
yap^347 | A mark waits for the appendsYap marks a typed transcript's line in its day file (`"typed":true`) by rewriting the file, and the host runs requests concurrently, so a line is only known to be there once its append is answered. The app keeps the day-file appends it has sent and not heard back from (`Io.appends`): every append it sends is kept, with its line, and one leaves only when a reply with its id arrives; a line is saved for marking only when the reply to its append says it worked; and a mark's read goes out only for a saved line, when no append is in flight after the message, so never before its own append is answered nor in the same frame as another. The menu starts no mark and drops no append (`receive_tracks`, `receive_answers`, `receive_saves`, `receive_marks`, `menuStep_marks`). That a typed transcript then ends up marked on disk is fuzzed, not proved (`yapfuzz`, app mode). | proved |
yap^349 | The overlay waits for the microphoneAs in the original, whose `begin` shows the overlay only once `AudioCapture.start` has returned: the overlay never shows a recording whose microphone hasn't started, so a microphone that fails to start never shows it. Only the host's report that the clip's microphone started (`micStarted`) begins the overlay (`step_begin`); every recording's clip, and the overlay's, is one numbered so far, so a new recording is never the overlay's clip (`OvInv`, `receive_ovInv`, `menuStep_ovInv`). | proved |
yap^350 | Keys wait for the microphoneWhile a recording's microphone is starting, a key going down or up, or another key, leaves the recording as it is: the event waits, and is handled once the host reports the start (or its failure), as the original's main thread handles key events only once `engine.start()` returns (`app_keys_wait`). Only the key's listener failing ends it. | proved |
yap^351 | Hold to talk, tap to latch: 300 ms, timed as the originalReleasing the key ends a press that began a recording, not part of a shortcut: held for less than 300 ms it was a tap, and the recording goes on hands free with its deadline ten minutes on; held 300 ms or more, the recording ends and is sent (`hold_tap_split`). As in the original, whose main thread is busy in `engine.start()` until the microphone runs, a release that comes while the microphone is starting waits, and is timed from when the start finished, not from its own timestamp: a tap during a slow start (one that ends 300 ms or more after the press) is a hold (`micStarted_replay`). | proved |
Assumptions
What the proofs rely on and nothing proves: the host, the OS and the hardware behaving as stated.
Yap
| Id | Claim | Reads as |
|---|---|---|
yap^330 | The host reports the dictation key and every other keyThe host reports the dictation key going down and up, once each per press, with its monotonic clock in milliseconds, and reports every other key that goes down while the dictation key is held, before the dictation key's release. Key repeats are not reported as presses. | assumed |
yap^331 | The host delivers the ticks it is asked forAfter `wakeAt t`, the host sends a `tick` with a time at or after `t`, while the app runs. Ticks may come late, early ones are ignored, and the clock may jump. | assumed |
yap^332 | The host answers requests by id, in order of commandsThe host runs a step's commands in the order given, and a reply carries the id of the request it answers. Replies may be slow, fail, come out of order, twice, or never. | assumed |
yap^333 | The host reports the microphone faithfullyAudio reports name the clip they belong to and come between its start and stop; frames and peak are of the 16 kHz mono samples since the last report, and windows are the 320-sample windows those samples complete, counted from the start of the clip. A microphone that fails to start is reported once as `micFailed`. | assumed |
yap^334 | The host transcribes the samples it was asked forA transcription reply's text is the transcript of the whole clip (or of the samples asked for), from the model asked for, with the prompt given. | assumed |
yap^335 | The host types into the app it was givenThe host brings the app with the given process forward and types the text, then Return if asked; it replies failed when it can't (no Accessibility access, the app is gone), and ok only when the text was typed. | assumed |
yap^336 | The host reports config.json and dictionary.txt when they changeAfter `readConfig` and `readDictionary`, the host reports each file's contents now and whenever it changes, decoding config.json's fields (a field left out is none) and reporting a file that won't parse as unreadable. | assumed |
yap^337 | The host lists day files and today by the local calendarAfter `listDays`, the host reports today's day number and the day files there are, as day numbers on the same calendar, and deletes exactly the files named by `deleteDays`. | assumed |
yap^348 | The host reports the microphone's start or its failureAfter `startRecording`, the host starts the microphone and reports, once, that it is running (`started`, with its monotonic clock in milliseconds read after the start returned: the clock of key events) or that it failed (`micFailed`), before any audio of the clip. A start that never returns is never reported; the app then gives the recording up ten minutes after a release waits for it. | assumed |