Cairn Docs Claims Blog Packages

Package ยท iamnbutler

cairn

Native macOS apps whose behaviour is proved in Lean.

Kind
Library
Owner
iamnbutler
Version
0.5.2
Published
Oct 26, 2026 by iamnbutler
Commit
23f0836cc992 at v0.5.2
Toolchain
leanprover/lean4:v4.35.0
License
MIT
Claims
78 active6 retired115 moved

Claims in 0.5.2Docs for 0.5.2

Use it

With the cairn tool:

cairn add cairn@^0.5.2

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

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

No claim is new, retired or moved since 0.5.1.

Claims in 0.5.2

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^945assumeactiveA control's menu shows exactly the frame's menu records
cairn^946assumeactiveChoosing a control menu's item reports its ref, then the close
cairn^947assumeactiveThe host shows a control menu only while Lean has it open
cairn^948assumeactiveAXShowMenu opens a control's menu as a right click does
cairn^949assumeactiveThe menu bar shows the app's menu items
cairn^950assumeactiveA menu bar item, by click or key equivalent, reports that item's ref
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^1012assumeactiveThe host reports scrolls where they happen, toward the end positive
cairn^1020assumeactiveSecure event input is on exactly while a secure field has focus
cairn^1021assumeactiveAssistive apps reach only what a scroll area shows
cairn^1022assumeactiveA secure field shows assistive apps nothing typed
cairn^1030assumeactiveThe badge the host shows is the label of the last badge effect, or none
cairn^1031assumeactiveAn announcement is posted once, with exactly its text
cairn^1032assumeactiveUnder holdWorld the host sends no clock, wake or reply of its own
cairn^1100moveactiveSet a value
cairn^1101moveactiveThe server handles a request
cairn^1102moveactiveThe server refuses a request
cairn^1103moveactiveAn answer arrives
cairn^1104moveactiveA request or answer is lost
cairn^1105moveactiveA retry comes due
cairn^1106moveactiveA view is fetched
cairn^1107invariantactiveA set shows in its own step
cairn^1108invariantactiveAt most one write in flight per key
cairn^1109invariantactiveNever more writes than sets
cairn^1110invariantactiveA refusal rolls back in its step
cairn^1111invariantactiveSettled keys show what the server holds
cairn^1112invariantactiveReplies for different keys commute
cairn^1113invariantactiveA settled count is the server's
cairn^1114invariantactiveA view never moves a written key