Cairn Docs Claims Blog Packages

Package ยท iamnbutler

cairn

Native macOS apps whose behaviour is proved in Lean.

Kind
Library
Owner
iamnbutler
Version
0.2.1
Published
Oct 25, 2026 by iamnbutler
Commit
d08381db7bd9 at v0.2.1
Toolchain
leanprover/lean4:v4.35.0
License
MIT
Claims
114 active3 retired44 moved

Claims in 0.2.1Docs for 0.2.1

Use it

With the cairn tool:

cairn add cairn@^0.2.1

Which writes cairn.toml, and the lakefile and SwiftPM lines that it keeps in step:

[dependencies]
cairn = "^0.2.1"
cairn.toml
[[require]]
name = "cairn"
scope = "iamnbutler"
version = "^0.2.1"
lean/lakefile.toml
.package(url: "https://cairn.registry.nexthub.sh/git/iamnbutler/cairn.git", from: "0.2.1")
Package.swift

Versions

VersionPublishedCommitClaimsDocs
0.5.2Oct 26, 202623f0836cc978 active6 retired115 moveddocs
0.5.1Oct 26, 20263616efdef078 active6 retired115 moveddocs
0.5.0Oct 26, 2026486e8ce6e777 active6 retired115 moveddocs
0.4.1Oct 26, 2026a6a35fb37254 active6 retired115 moveddocs
0.4.0Oct 26, 2026f107007b7052 active6 retired115 moveddocs
0.3.0Oct 25, 202660c448329b51 active6 retired115 moveddocs
0.2.5Oct 25, 2026ea05c5e30d119 active3 retired44 moveddocs
0.2.4Oct 25, 2026654c6695ee119 active3 retired44 moveddocs
0.2.3Oct 25, 20268ecf96ee6b119 active3 retired44 moveddocs
0.2.2Oct 25, 2026885b585520119 active3 retired44 moveddocs
0.2.1Oct 25, 2026d08381db7b114 active3 retired44 moveddocs
0.2.0Oct 25, 202616b70b80d6108 active3 retired44 moveddocs
0.1.3Oct 25, 2026aea142ce26100 active2 retired44 moveddocs
0.1.2Oct 25, 2026597dea82d5100 active2 retired44 moveddocs

What changed in 0.2.1

Claims new, retired or moved since 0.2.0.

IdChangeKindClaim
cairn^506newmoveLoad 24
cairn^507newmoveCancel
cairn^508newflowLoad many, then cancel
cairn^509newmoveReload a tile
cairn^510newinvariantTiles fit the window at every size
cairn^1009newassumecancelRequest stops a running request's work; it is still answered once

Claims in 0.2.1

Every id this package has issued, as its claims.lock held them at this version. An id never moves or changes meaning: the registry refuses a version that drops, renumbers or redefines one. The claim pages show each claim by place, with what it does and its evidence.

IdKindStatusClaim
cairn^1moveactiveIncrement
cairn^2moveactiveReset
cairn^3placeactiveCounter window
cairn^4flowactiveCount to three
cairn^5flowactiveStart over
cairn^6invariantretiredMoves never leave a press in progress
cairn^7assumeactiveThe host reports clicks where they happen
cairn^101moveactiveType a new item
cairn^102moveactiveAdd
cairn^103moveactiveToggle an item
cairn^104moveactiveDelete an item
cairn^105invariantactiveItems left
cairn^106placeactiveBasics window
cairn^107flowactiveAdd two items and finish one
cairn^108flowactiveBlank text adds nothing
cairn^109flowactiveAdd an item, then delete it
cairn^201placeactiveTodos window
cairn^202moveactiveNew todo
cairn^203moveactiveMark all as complete
cairn^204moveactiveComplete a todo
cairn^205moveactiveEdit a todo
cairn^206moveactiveDelete a todo
cairn^207moveactiveEdit field
cairn^208moveactiveAll
cairn^209moveactiveActive
cairn^210moveactiveCompleted
cairn^211moveactiveClear completed
cairn^212invariantactiveCounter and ids
cairn^213invariantretiredThe list is the filter applied to the todos
cairn^214assumeactiveThe host reports a double click as a second click
cairn^215moveretiredBack through filters
cairn^216flowactiveAdd two todos and complete one
cairn^217flowactiveBlank text adds nothing
cairn^218flowactiveEdit a todo and save with Enter
cairn^219flowactiveSaving a blank edit deletes the todo
cairn^220flowactiveEscape cancels an edit
cairn^221flowactiveThe Active filter hides completed todos
cairn^222flowactiveClear completed
cairn^223flowactiveMark all as complete, then undo it
cairn^224flowactiveA new todo under the Completed filter
cairn^225invariantactiveThe list is the filter applied to the todos
cairn^301placemoved:yapMenu bar menu
cairn^302movemoved:yapCopy Last Transcript
cairn^303movemoved:yapRecent transcript
cairn^304movemoved:yapKeep Transcripts
cairn^305movemoved:yapPress Return After Dictating
cairn^306movemoved:yapDictate with Key
cairn^307movemoved:yapOpen Transcripts Folder
cairn^308movemoved:yapEdit Dictionary
cairn^309movemoved:yapEdit Settings
cairn^310movemoved:yapGrant Accessibility Access
cairn^311invariantmoved:yapA shortcut never sends
cairn^312invariantmoved:yapHold to talk, tap to latch: 300 ms
cairn^313invariantmoved:yapOne recording at a time
cairn^314invariantmoved:yapEvery recording ends
cairn^315invariantmoved:yapKept before it is typed
cairn^316invariantmoved:yapA failed type is kept and flagged
cairn^317invariantmoved:yapLate and cancelled replies never type
cairn^318invariantmoved:yapEach clip is typed at most once
cairn^319invariantmoved:yapFixes replace whole words
cairn^320invariantmoved:yapRetention never deletes today
cairn^321invariantmoved:yapOnly the first 25 terms are sent
cairn^322invariantmoved:yapRecent Transcripts holds five
cairn^323invariantmoved:yapToo short, silent or nowhere to type: never sent
cairn^330assumemoved:yapThe host reports the dictation key and every other key
cairn^331assumemoved:yapThe host delivers the ticks it is asked for
cairn^332assumemoved:yapThe host answers requests by id, in order of commands
cairn^333assumemoved:yapThe host reports the microphone faithfully
cairn^334assumemoved:yapThe host transcribes the samples it was asked for
cairn^335assumemoved:yapThe host types into the app it was given
cairn^336assumemoved:yapThe host reports config.json and dictionary.txt when they change
cairn^337assumemoved:yapThe host lists day files and today by the local calendar
cairn^340flowmoved:yapTurn Dictate with Key off
cairn^341flowmoved:yapKeep Transcripts off and on again
cairn^342movemoved:yapQuit Yap (Cairn)
cairn^343movemoved:yapGrant Microphone Access
cairn^344movemoved:yapOpen the menu
cairn^345placemoved:yapOverlay panel
cairn^346invariantmoved:yapThe original Yap keeps its key
cairn^347invariantmoved:yapA mark waits for the appends
cairn^348assumemoved:yapThe host reports the microphone's start or its failure
cairn^349invariantmoved:yapThe overlay waits for the microphone
cairn^350invariantmoved:yapKeys wait for the microphone
cairn^351invariantmoved:yapHold to talk, tap to latch: 300 ms, timed as the original
cairn^399placemoved:yapOverlay panel
cairn^401moveactiveStart / Stop
cairn^402moveactiveLap
cairn^403moveactiveReset
cairn^404moveactiveSave laps
cairn^405moveactiveLoad laps
cairn^406placeactiveClock window
cairn^407flowactiveTwo laps
cairn^408flowactiveStart over
cairn^409invariantactivePending requests have fresh ids
cairn^450placeactiveTray menu
cairn^451placeactiveRecent Items submenu
cairn^452placeactiveOverlay panel
cairn^453moveactiveOpen the menu
cairn^454moveactiveShow Overlay
cairn^455moveactiveKeep Recent Items
cairn^456moveactiveAdd Item
cairn^457moveactiveRecent item
cairn^458moveactiveClear Recent Items
cairn^459moveactiveQuit Tray
cairn^460invariantactiveAt most five recent items
cairn^461flowactiveShow the overlay
cairn^462flowactiveAdd an item and pick it
cairn^501moveactiveReload
cairn^502moveactiveFit
cairn^503placeactiveGallery window
cairn^504invariantactivePending loads have fresh ids
cairn^505flowactiveReload, then fit inside
cairn^506moveactiveLoad 24
cairn^507moveactiveCancel
cairn^508flowactiveLoad many, then cancel
cairn^509moveactiveReload a tile
cairn^510invariantactiveTiles fit the window at every size
cairn^901assumeactiveThe Swift frame decoder agrees with Lean's
cairn^902assumeactiveLean decodes what the Swift event encoder writes
cairn^903assumeactiveUTF-16 offsets and scalar indices convert exactly
cairn^904assumeactiveThe text-input shadow predicts Lean's field
cairn^905assumeactiveInput-method geometry agrees with Lean's caret
cairn^906assumeactiveThe host's text metrics are what layout assumes
cairn^907assumeactiveCarets follow the painted glyphs
cairn^908assumeactiveThe host's clock is monotonic milliseconds
cairn^909assumeactiveThe host wakes Lean by wake
cairn^910assumeactivereadFile replies with the file's bytes, or failed
cairn^911assumeactivewriteFile is atomic, and replies done only when the bytes are there
cairn^912assumeactiveplaySound starts a known sound and refuses an unknown one
cairn^913assumeactivehttp sends the request as given and returns the response as received
cairn^914assumeactiveThe host answers every request exactly once, with its id
cairn^915assumeactiveevery ms ticks while started and never after it is stopped
cairn^940assumeactiveThe native menu shows exactly the frame's menu records
cairn^941assumeactiveChoosing a menu item reports that item's ref
cairn^942assumeactiveOpening and closing the menu are reported once each
cairn^943assumeactiveAn overlay panel never takes focus or clicks
cairn^944assumeactiveAn overlay panel is where its anchor says
cairn^960assumeactiveappendFile adds exactly the bytes at the end, or fails and adds nothing
cairn^961assumeactivelistDir lists exactly the directory's names, sorted
cairn^962assumeactivedeleteFile removes a file or a link, never a directory
cairn^963assumeactivewatchFile reports every change to its file, and nothing after its stop
cairn^964assumeactivefrontmostApp answers the app in front
cairn^965assumeactivepermission answers whether the app holds it, and prompts only when asked
cairn^966assumeactiverecord streams the levels of exactly the samples it keeps, and nothing after its stop
cairn^967assumeactiveA clip's WAV for a range of windows holds exactly those samples
cairn^968assumeactiveglobalKey reports the hotkey's press and release, and other keys while it is held
cairn^969assumeactivetypeText types exactly the text into that app, or nothing
cairn^970assumeactiveupload sends the body assembled from its parts, with the secret in its header
cairn^971assumeactiveA secret is read from the environment or its file, and never shown
cairn^990assumeactiveWrapped lines paint as wide as Lean measured them
cairn^991assumeactiveLean breaks lines where Core Text would
cairn^1000assumeactiveopenItem opens exactly the URL or existing file it names
cairn^1001assumeactiveappRunning answers whether an app with that bundle id runs
cairn^1002assumeactivereadDefault answers the default's value as text
cairn^1003assumeactivemakeDir makes a private directory and its parents
cairn^1004assumeactiveA painter's pixels stay inside its box
cairn^1005assumeactiverecord reports started once its microphone is running, before any audio, or fails without it
cairn^1006assumeactiveloadImage answers the image's pixel size, or the fault
cairn^1007assumeactiveAn image's pixels stay inside its box
cairn^1008assumeactiveAn image is drawn where its oriented pixels are
cairn^1009assumeactivecancelRequest stops a running request's work; it is still answered once