cairn 0.1.2: claims

Counter window `cairn^3`

Which claims are in this place is in the claims export, which this version doesn't have.

Basics window `cairn^106`

Which claims are in this place is in the claims export, which this version doesn't have.

Todos window `cairn^201`

Which claims are in this place is in the claims export, which this version doesn't have.

Clock window `cairn^406`

Which claims are in this place is in the claims export, which this version doesn't have.

Tray menu `cairn^450`

Which claims are in this place is in the claims export, which this version doesn't have.

Recent Items submenu `cairn^451`

Which claims are in this place is in the claims export, which this version doesn't have.

Overlay panel `cairn^452`

Which claims are in this place is in the claims export, which this version doesn't have.

Moves and flows

Id	Kind	Claim	Reads as
`cairn^1`	move	Increment	ledger only
`cairn^2`	move	Reset	ledger only
`cairn^4`	flow	Count to three	ledger only
`cairn^5`	flow	Start over	ledger only
`cairn^101`	move	Type a new item	ledger only
`cairn^102`	move	Add	ledger only
`cairn^103`	move	Toggle an item	ledger only
`cairn^104`	move	Delete an item	ledger only
`cairn^107`	flow	Add two items and finish one	ledger only
`cairn^108`	flow	Blank text adds nothing	ledger only
`cairn^109`	flow	Add an item, then delete it	ledger only
`cairn^202`	move	New todo	ledger only
`cairn^203`	move	Mark all as complete	ledger only
`cairn^204`	move	Complete a todo	ledger only
`cairn^205`	move	Edit a todo	ledger only
`cairn^206`	move	Delete a todo	ledger only
`cairn^207`	move	Edit field	ledger only
`cairn^208`	move	All	ledger only
`cairn^209`	move	Active	ledger only
`cairn^210`	move	Completed	ledger only
`cairn^211`	move	Clear completed	ledger only
`cairn^215`	move	Back through filters	retired
`cairn^216`	flow	Add two todos and complete one	ledger only
`cairn^217`	flow	Blank text adds nothing	ledger only
`cairn^218`	flow	Edit a todo and save with Enter	ledger only
`cairn^219`	flow	Saving a blank edit deletes the todo	ledger only
`cairn^220`	flow	Escape cancels an edit	ledger only
`cairn^221`	flow	The Active filter hides completed todos	ledger only
`cairn^222`	flow	Clear completed	ledger only
`cairn^223`	flow	Mark all as complete, then undo it	ledger only
`cairn^224`	flow	A new todo under the Completed filter	ledger only
`cairn^401`	move	Start / Stop	ledger only
`cairn^402`	move	Lap	ledger only
`cairn^403`	move	Reset	ledger only
`cairn^404`	move	Save laps	ledger only
`cairn^405`	move	Load laps	ledger only
`cairn^407`	flow	Two laps	ledger only
`cairn^408`	flow	Start over	ledger only
`cairn^453`	move	Open the menu	ledger only
`cairn^454`	move	Show Overlay	ledger only
`cairn^455`	move	Keep Recent Items	ledger only
`cairn^456`	move	Add Item	ledger only
`cairn^457`	move	Recent item	ledger only
`cairn^458`	move	Clear Recent Items	ledger only
`cairn^459`	move	Quit Tray	ledger only
`cairn^461`	flow	Show the overlay	ledger only
`cairn^462`	flow	Add an item and pick it	ledger only

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^105`	Items left	ledger only
`cairn^212`	Counter and ids	ledger only
`cairn^213`	The list is the filter applied to the todos	ledger only
`cairn^409`	Pending requests have fresh ids	ledger only
`cairn^460`	At most five recent items	ledger only

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

Id	Claim	Reads as
`cairn^7`	The host reports clicks where they happen	ledger only
`cairn^214`	The host reports a double click as a second click	ledger only
`cairn^901`	The Swift frame decoder agrees with Lean's	ledger only
`cairn^902`	Lean decodes what the Swift event encoder writes	ledger only
`cairn^903`	UTF-16 offsets and scalar indices convert exactly	ledger only
`cairn^904`	The text-input shadow predicts Lean's field	ledger only
`cairn^905`	Input-method geometry agrees with Lean's caret	ledger only
`cairn^906`	The host's text metrics are what layout assumes	ledger only
`cairn^907`	Carets follow the painted glyphs	ledger only
`cairn^908`	The host's clock is monotonic milliseconds	ledger only
`cairn^909`	The host wakes Lean by wake	ledger only
`cairn^910`	readFile replies with the file's bytes, or failed	ledger only
`cairn^911`	writeFile is atomic, and replies done only when the bytes are there	ledger only
`cairn^912`	playSound starts a known sound and refuses an unknown one	ledger only
`cairn^913`	http sends the request as given and returns the response as received	ledger only
`cairn^914`	The host answers every request exactly once, with its id	ledger only
`cairn^915`	every ms ticks while started and never after it is stopped	ledger only
`cairn^940`	The native menu shows exactly the frame's menu records	ledger only
`cairn^941`	Choosing a menu item reports that item's ref	ledger only
`cairn^942`	Opening and closing the menu are reported once each	ledger only
`cairn^943`	An overlay panel never takes focus or clicks	ledger only
`cairn^944`	An overlay panel is where its anchor says	ledger only
`cairn^960`	appendFile adds exactly the bytes at the end, or fails and adds nothing	ledger only
`cairn^961`	listDir lists exactly the directory's names, sorted	ledger only
`cairn^962`	deleteFile removes a file or a link, never a directory	ledger only
`cairn^963`	watchFile reports every change to its file, and nothing after its stop	ledger only
`cairn^964`	frontmostApp answers the app in front	ledger only
`cairn^965`	permission answers whether the app holds it, and prompts only when asked	ledger only
`cairn^966`	record streams the levels of exactly the samples it keeps, and nothing after its stop	ledger only
`cairn^967`	A clip's WAV for a range of windows holds exactly those samples	ledger only
`cairn^968`	globalKey reports the hotkey's press and release, and other keys while it is held	ledger only
`cairn^969`	typeText types exactly the text into that app, or nothing	ledger only
`cairn^970`	upload sends the body assembled from its parts, with the secret in its header	ledger only
`cairn^971`	A secret is read from the environment or its file, and never shown	ledger only
`cairn^990`	Wrapped lines paint as wide as Lean measured them	ledger only
`cairn^991`	Lean breaks lines where Core Text would	ledger only
`cairn^1000`	openItem opens exactly the URL or existing file it names	ledger only
`cairn^1001`	appRunning answers whether an app with that bundle id runs	ledger only
`cairn^1002`	readDefault answers the default's value as text	ledger only
`cairn^1003`	makeDir makes a private directory and its parents	ledger only
`cairn^1004`	A painter's pixels stay inside its box	ledger only
`cairn^1005`	record reports started once its microphone is running, before any audio, or fails without it	ledger only

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^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`

Counter window cairn^3

Basics window cairn^106

Todos window cairn^201

Clock window cairn^406

Tray menu cairn^450

Recent Items submenu cairn^451

Overlay panel cairn^452

Moves and flows

Invariants

Assumptions

Moved to other packages

Counter window `cairn^3`

Basics window `cairn^106`

Todos window `cairn^201`

Clock window `cairn^406`

Tray menu `cairn^450`

Recent Items submenu `cairn^451`

Overlay panel `cairn^452`