Cairn Docs Claims Blog Packages

Package ยท iamnbutler

cairn

Native macOS apps whose behaviour is proved in Lean.

Kind
Library
Owner
iamnbutler
Version
0.3.0
Published
Oct 25, 2026 by iamnbutler
Commit
60c448329be3 at v0.3.0
Toolchain
leanprover/lean4:v4.35.0
License
MIT
Claims
51 active6 retired115 moved

Claims in 0.3.0Docs for 0.3.0

Use it

With the cairn tool:

cairn add cairn@^0.3.0

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

[dependencies]
cairn = "^0.3.0"
cairn.toml
[[require]]
name = "cairn"
scope = "iamnbutler"
version = "^0.3.0"
lean/lakefile.toml
.package(url: "https://cairn.registry.nexthub.sh/git/iamnbutler/cairn.git", from: "0.3.0")
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.3.0

Claims new, retired or moved since 0.2.5.

IdChangeKindClaim
cairn^1moved:cairn_examplesmoveIncrement
cairn^2moved:cairn_examplesmoveReset
cairn^3moved:cairn_examplesplaceCounter window
cairn^4moved:cairn_examplesflowCount to three
cairn^5moved:cairn_examplesflowStart over
cairn^101moved:cairn_examplesmoveType a new item
cairn^102moved:cairn_examplesmoveAdd
cairn^103moved:cairn_examplesmoveToggle an item
cairn^104moved:cairn_examplesmoveDelete an item
cairn^105moved:cairn_examplesinvariantItems left
cairn^106moved:cairn_examplesplaceBasics window
cairn^107moved:cairn_examplesflowAdd two items and finish one
cairn^108moved:cairn_examplesflowBlank text adds nothing
cairn^109moved:cairn_examplesflowAdd an item, then delete it
cairn^201moved:cairn_examplesplaceTodos window
cairn^202moved:cairn_examplesmoveNew todo
cairn^203moved:cairn_examplesmoveMark all as complete
cairn^204moved:cairn_examplesmoveComplete a todo
cairn^205moved:cairn_examplesmoveEdit a todo
cairn^206moved:cairn_examplesmoveDelete a todo
cairn^207moved:cairn_examplesmoveEdit field
cairn^208moved:cairn_examplesmoveAll
cairn^209moved:cairn_examplesmoveActive
cairn^210moved:cairn_examplesmoveCompleted
cairn^211moved:cairn_examplesmoveClear completed
cairn^212moved:cairn_examplesinvariantCounter and ids
cairn^216moved:cairn_examplesflowAdd two todos and complete one
cairn^217moved:cairn_examplesflowBlank text adds nothing
cairn^218moved:cairn_examplesflowEdit a todo and save with Enter
cairn^219moved:cairn_examplesflowSaving a blank edit deletes the todo
cairn^220moved:cairn_examplesflowEscape cancels an edit
cairn^221moved:cairn_examplesflowThe Active filter hides completed todos
cairn^222moved:cairn_examplesflowClear completed
cairn^223moved:cairn_examplesflowMark all as complete, then undo it
cairn^224moved:cairn_examplesflowA new todo under the Completed filter
cairn^225retiredinvariantThe list is the filter applied to the todos
cairn^226new, moved:cairn_examplesinvariantThe list is the filter applied to the todos
cairn^401moved:cairn_examplesmoveStart / Stop
cairn^402moved:cairn_examplesmoveLap
cairn^403moved:cairn_examplesmoveReset
cairn^404moved:cairn_examplesmoveSave laps
cairn^405moved:cairn_examplesmoveLoad laps
cairn^406moved:cairn_examplesplaceClock window
cairn^407moved:cairn_examplesflowTwo laps
cairn^408moved:cairn_examplesflowStart over
cairn^409moved:cairn_examplesinvariantPending requests have fresh ids
cairn^450moved:cairn_examplesplaceTray menu
cairn^451moved:cairn_examplesplaceRecent Items submenu
cairn^452moved:cairn_examplesplaceOverlay panel
cairn^453moved:cairn_examplesmoveOpen the menu
cairn^454moved:cairn_examplesmoveShow Overlay
cairn^455moved:cairn_examplesmoveKeep Recent Items
cairn^456moved:cairn_examplesmoveAdd Item
cairn^457moved:cairn_examplesmoveRecent item
cairn^458moved:cairn_examplesmoveClear Recent Items
cairn^459moved:cairn_examplesmoveQuit Tray
cairn^460moved:cairn_examplesinvariantAt most five recent items
cairn^461moved:cairn_examplesflowShow the overlay
cairn^462moved:cairn_examplesflowAdd an item and pick it
cairn^501moved:cairn_examplesmoveReload
cairn^502moved:cairn_examplesmoveFit
cairn^503moved:cairn_examplesplaceGallery window
cairn^504moved:cairn_examplesinvariantPending loads have fresh ids
cairn^505moved:cairn_examplesflowReload, then fit inside
cairn^506moved:cairn_examplesmoveLoad 24
cairn^507moved:cairn_examplesmoveCancel
cairn^508moved:cairn_examplesflowLoad many, then cancel
cairn^509moved:cairn_examplesmoveReload a tile
cairn^510moved:cairn_examplesinvariantTiles fit the window at every size
cairn^511moved:cairn_examplesinvariantTiles are at least 180 points wide
cairn^512moved:cairn_examplesmoveNext page
cairn^513moved:cairn_examplesinvariantA dropped thumbnail waits to be loaded again
cairn^913retiredassumehttp sends the request as given and returns the response as received
cairn^971retiredassumeA secret is read from the environment or its file, and never shown
cairn^972newassumeThe Keychain keeps what it was given for this app
cairn^973newassumeCaptured reply fields go to the Keychain and never to Lean
cairn^974newassumehttp sends the request as given, with its secret header, and returns the response as received
cairn^975newassumeAn environment secret is read from the environment or its file, and never shown
cairn^1020newassumeSecure event input is on exactly while a secure field has focus

Claims in 0.3.0

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^1movemoved:cairn_examplesIncrement
cairn^2movemoved:cairn_examplesReset
cairn^3placemoved:cairn_examplesCounter window
cairn^4flowmoved:cairn_examplesCount to three
cairn^5flowmoved:cairn_examplesStart over
cairn^6invariantretiredMoves never leave a press in progress
cairn^7assumeactiveThe host reports clicks where they happen
cairn^101movemoved:cairn_examplesType a new item
cairn^102movemoved:cairn_examplesAdd
cairn^103movemoved:cairn_examplesToggle an item
cairn^104movemoved:cairn_examplesDelete an item
cairn^105invariantmoved:cairn_examplesItems left
cairn^106placemoved:cairn_examplesBasics window
cairn^107flowmoved:cairn_examplesAdd two items and finish one
cairn^108flowmoved:cairn_examplesBlank text adds nothing
cairn^109flowmoved:cairn_examplesAdd an item, then delete it
cairn^201placemoved:cairn_examplesTodos window
cairn^202movemoved:cairn_examplesNew todo
cairn^203movemoved:cairn_examplesMark all as complete
cairn^204movemoved:cairn_examplesComplete a todo
cairn^205movemoved:cairn_examplesEdit a todo
cairn^206movemoved:cairn_examplesDelete a todo
cairn^207movemoved:cairn_examplesEdit field
cairn^208movemoved:cairn_examplesAll
cairn^209movemoved:cairn_examplesActive
cairn^210movemoved:cairn_examplesCompleted
cairn^211movemoved:cairn_examplesClear completed
cairn^212invariantmoved:cairn_examplesCounter 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^216flowmoved:cairn_examplesAdd two todos and complete one
cairn^217flowmoved:cairn_examplesBlank text adds nothing
cairn^218flowmoved:cairn_examplesEdit a todo and save with Enter
cairn^219flowmoved:cairn_examplesSaving a blank edit deletes the todo
cairn^220flowmoved:cairn_examplesEscape cancels an edit
cairn^221flowmoved:cairn_examplesThe Active filter hides completed todos
cairn^222flowmoved:cairn_examplesClear completed
cairn^223flowmoved:cairn_examplesMark all as complete, then undo it
cairn^224flowmoved:cairn_examplesA new todo under the Completed filter
cairn^225invariantretiredThe list is the filter applied to the todos
cairn^226invariantmoved:cairn_examplesThe 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^401movemoved:cairn_examplesStart / Stop
cairn^402movemoved:cairn_examplesLap
cairn^403movemoved:cairn_examplesReset
cairn^404movemoved:cairn_examplesSave laps
cairn^405movemoved:cairn_examplesLoad laps
cairn^406placemoved:cairn_examplesClock window
cairn^407flowmoved:cairn_examplesTwo laps
cairn^408flowmoved:cairn_examplesStart over
cairn^409invariantmoved:cairn_examplesPending requests have fresh ids
cairn^450placemoved:cairn_examplesTray menu
cairn^451placemoved:cairn_examplesRecent Items submenu
cairn^452placemoved:cairn_examplesOverlay panel
cairn^453movemoved:cairn_examplesOpen the menu
cairn^454movemoved:cairn_examplesShow Overlay
cairn^455movemoved:cairn_examplesKeep Recent Items
cairn^456movemoved:cairn_examplesAdd Item
cairn^457movemoved:cairn_examplesRecent item
cairn^458movemoved:cairn_examplesClear Recent Items
cairn^459movemoved:cairn_examplesQuit Tray
cairn^460invariantmoved:cairn_examplesAt most five recent items
cairn^461flowmoved:cairn_examplesShow the overlay
cairn^462flowmoved:cairn_examplesAdd an item and pick it
cairn^501movemoved:cairn_examplesReload
cairn^502movemoved:cairn_examplesFit
cairn^503placemoved:cairn_examplesGallery window
cairn^504invariantmoved:cairn_examplesPending loads have fresh ids
cairn^505flowmoved:cairn_examplesReload, then fit inside
cairn^506movemoved:cairn_examplesLoad 24
cairn^507movemoved:cairn_examplesCancel
cairn^508flowmoved:cairn_examplesLoad many, then cancel
cairn^509movemoved:cairn_examplesReload a tile
cairn^510invariantmoved:cairn_examplesTiles fit the window at every size
cairn^511invariantmoved:cairn_examplesTiles are at least 180 points wide
cairn^512movemoved:cairn_examplesNext page
cairn^513invariantmoved:cairn_examplesA dropped thumbnail waits to be loaded again
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^913assumeretiredhttp 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^971assumeretiredA secret is read from the environment or its file, and never shown
cairn^972assumeactiveThe Keychain keeps what it was given for this app
cairn^973assumeactiveCaptured reply fields go to the Keychain and never to Lean
cairn^974assumeactivehttp sends the request as given, with its secret header, and returns the response as received
cairn^975assumeactiveAn environment 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
cairn^1010assumeactiveThe window is never smaller than the app's minimum size
cairn^1011assumeactiveThe image cache reports every image it drops, after it is gone
cairn^1020assumeactiveSecure event input is on exactly while a secure field has focus