Package ยท iamnbutler
cairn
Native macOS apps whose behaviour is proved in Lean.
- Kind
- Library
- Owner
- iamnbutler
- Version
- 0.2.0
- Published
- Oct 25, 2026 by iamnbutler
- Commit
16b70b80d67fatv0.2.0- Toolchain
leanprover/lean4:v4.35.0- License
- MIT
- Claims
- 108 active3 retired44 moved
Use it
With the cairn tool:
cairn add cairn@^0.2.0Which writes cairn.toml, and the lakefile and SwiftPM lines that it keeps in step:
[dependencies]
cairn = "^0.2.0"cairn.toml[[require]]
name = "cairn"
scope = "iamnbutler"
version = "^0.2.0"lean/lakefile.toml.package(url: "https://cairn.registry.nexthub.sh/git/iamnbutler/cairn.git", from: "0.2.0")Package.swiftVersions
| Version | Published | Commit | Claims | Docs |
|---|---|---|---|---|
| 0.5.2 | Oct 26, 2026 | 23f0836cc9 | 78 active6 retired115 moved | docs |
| 0.5.1 | Oct 26, 2026 | 3616efdef0 | 78 active6 retired115 moved | docs |
| 0.5.0 | Oct 26, 2026 | 486e8ce6e7 | 77 active6 retired115 moved | docs |
| 0.4.1 | Oct 26, 2026 | a6a35fb372 | 54 active6 retired115 moved | docs |
| 0.4.0 | Oct 26, 2026 | f107007b70 | 52 active6 retired115 moved | docs |
| 0.3.0 | Oct 25, 2026 | 60c448329b | 51 active6 retired115 moved | docs |
| 0.2.5 | Oct 25, 2026 | ea05c5e30d | 119 active3 retired44 moved | docs |
| 0.2.4 | Oct 25, 2026 | 654c6695ee | 119 active3 retired44 moved | docs |
| 0.2.3 | Oct 25, 2026 | 8ecf96ee6b | 119 active3 retired44 moved | docs |
| 0.2.2 | Oct 25, 2026 | 885b585520 | 119 active3 retired44 moved | docs |
| 0.2.1 | Oct 25, 2026 | d08381db7b | 114 active3 retired44 moved | docs |
| 0.2.0 | Oct 25, 2026 | 16b70b80d6 | 108 active3 retired44 moved | docs |
| 0.1.3 | Oct 25, 2026 | aea142ce26 | 100 active2 retired44 moved | docs |
| 0.1.2 | Oct 25, 2026 | 597dea82d5 | 100 active2 retired44 moved | docs |
What changed in 0.2.0
Claims new, retired or moved since 0.1.3.
| Id | Change | Kind | Claim |
|---|---|---|---|
cairn^213 | retired | invariant | The list is the filter applied to the todos |
cairn^225 | new | invariant | The list is the filter applied to the todos |
cairn^501 | new | move | Reload |
cairn^502 | new | move | Fit |
cairn^503 | new | place | Gallery window |
cairn^504 | new | invariant | Pending loads have fresh ids |
cairn^505 | new | flow | Reload, then fit inside |
cairn^1006 | new | assume | loadImage answers the image's pixel size, or the fault |
cairn^1007 | new | assume | An image's pixels stay inside its box |
cairn^1008 | new | assume | An image is drawn where its oriented pixels are |
Claims in 0.2.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.
| Id | Kind | Status | Claim |
|---|---|---|---|
cairn^1 | move | active | Increment |
cairn^2 | move | active | Reset |
cairn^3 | place | active | Counter window |
cairn^4 | flow | active | Count to three |
cairn^5 | flow | active | Start over |
cairn^6 | invariant | retired | Moves never leave a press in progress |
cairn^7 | assume | active | The host reports clicks where they happen |
cairn^101 | move | active | Type a new item |
cairn^102 | move | active | Add |
cairn^103 | move | active | Toggle an item |
cairn^104 | move | active | Delete an item |
cairn^105 | invariant | active | Items left |
cairn^106 | place | active | Basics window |
cairn^107 | flow | active | Add two items and finish one |
cairn^108 | flow | active | Blank text adds nothing |
cairn^109 | flow | active | Add an item, then delete it |
cairn^201 | place | active | Todos window |
cairn^202 | move | active | New todo |
cairn^203 | move | active | Mark all as complete |
cairn^204 | move | active | Complete a todo |
cairn^205 | move | active | Edit a todo |
cairn^206 | move | active | Delete a todo |
cairn^207 | move | active | Edit field |
cairn^208 | move | active | All |
cairn^209 | move | active | Active |
cairn^210 | move | active | Completed |
cairn^211 | move | active | Clear completed |
cairn^212 | invariant | active | Counter and ids |
cairn^213 | invariant | retired | The list is the filter applied to the todos |
cairn^214 | assume | active | The host reports a double click as a second click |
cairn^215 | move | retired | Back through filters |
cairn^216 | flow | active | Add two todos and complete one |
cairn^217 | flow | active | Blank text adds nothing |
cairn^218 | flow | active | Edit a todo and save with Enter |
cairn^219 | flow | active | Saving a blank edit deletes the todo |
cairn^220 | flow | active | Escape cancels an edit |
cairn^221 | flow | active | The Active filter hides completed todos |
cairn^222 | flow | active | Clear completed |
cairn^223 | flow | active | Mark all as complete, then undo it |
cairn^224 | flow | active | A new todo under the Completed filter |
cairn^225 | invariant | active | The list is the filter applied to the todos |
cairn^301 | place | moved:yap | Menu bar menu |
cairn^302 | move | moved:yap | Copy Last Transcript |
cairn^303 | move | moved:yap | Recent transcript |
cairn^304 | move | moved:yap | Keep Transcripts |
cairn^305 | move | moved:yap | Press Return After Dictating |
cairn^306 | move | moved:yap | Dictate with Key |
cairn^307 | move | moved:yap | Open Transcripts Folder |
cairn^308 | move | moved:yap | Edit Dictionary |
cairn^309 | move | moved:yap | Edit Settings |
cairn^310 | move | moved:yap | Grant Accessibility Access |
cairn^311 | invariant | moved:yap | A shortcut never sends |
cairn^312 | invariant | moved:yap | Hold to talk, tap to latch: 300 ms |
cairn^313 | invariant | moved:yap | One recording at a time |
cairn^314 | invariant | moved:yap | Every recording ends |
cairn^315 | invariant | moved:yap | Kept before it is typed |
cairn^316 | invariant | moved:yap | A failed type is kept and flagged |
cairn^317 | invariant | moved:yap | Late and cancelled replies never type |
cairn^318 | invariant | moved:yap | Each clip is typed at most once |
cairn^319 | invariant | moved:yap | Fixes replace whole words |
cairn^320 | invariant | moved:yap | Retention never deletes today |
cairn^321 | invariant | moved:yap | Only the first 25 terms are sent |
cairn^322 | invariant | moved:yap | Recent Transcripts holds five |
cairn^323 | invariant | moved:yap | Too short, silent or nowhere to type: never sent |
cairn^330 | assume | moved:yap | The host reports the dictation key and every other key |
cairn^331 | assume | moved:yap | The host delivers the ticks it is asked for |
cairn^332 | assume | moved:yap | The host answers requests by id, in order of commands |
cairn^333 | assume | moved:yap | The host reports the microphone faithfully |
cairn^334 | assume | moved:yap | The host transcribes the samples it was asked for |
cairn^335 | assume | moved:yap | The host types into the app it was given |
cairn^336 | assume | moved:yap | The host reports config.json and dictionary.txt when they change |
cairn^337 | assume | moved:yap | The host lists day files and today by the local calendar |
cairn^340 | flow | moved:yap | Turn Dictate with Key off |
cairn^341 | flow | moved:yap | Keep Transcripts off and on again |
cairn^342 | move | moved:yap | Quit Yap (Cairn) |
cairn^343 | move | moved:yap | Grant Microphone Access |
cairn^344 | move | moved:yap | Open the menu |
cairn^345 | place | moved:yap | Overlay panel |
cairn^346 | invariant | moved:yap | The original Yap keeps its key |
cairn^347 | invariant | moved:yap | A mark waits for the appends |
cairn^348 | assume | moved:yap | The host reports the microphone's start or its failure |
cairn^349 | invariant | moved:yap | The overlay waits for the microphone |
cairn^350 | invariant | moved:yap | Keys wait for the microphone |
cairn^351 | invariant | moved:yap | Hold to talk, tap to latch: 300 ms, timed as the original |
cairn^399 | place | moved:yap | Overlay panel |
cairn^401 | move | active | Start / Stop |
cairn^402 | move | active | Lap |
cairn^403 | move | active | Reset |
cairn^404 | move | active | Save laps |
cairn^405 | move | active | Load laps |
cairn^406 | place | active | Clock window |
cairn^407 | flow | active | Two laps |
cairn^408 | flow | active | Start over |
cairn^409 | invariant | active | Pending requests have fresh ids |
cairn^450 | place | active | Tray menu |
cairn^451 | place | active | Recent Items submenu |
cairn^452 | place | active | Overlay panel |
cairn^453 | move | active | Open the menu |
cairn^454 | move | active | Show Overlay |
cairn^455 | move | active | Keep Recent Items |
cairn^456 | move | active | Add Item |
cairn^457 | move | active | Recent item |
cairn^458 | move | active | Clear Recent Items |
cairn^459 | move | active | Quit Tray |
cairn^460 | invariant | active | At most five recent items |
cairn^461 | flow | active | Show the overlay |
cairn^462 | flow | active | Add an item and pick it |
cairn^501 | move | active | Reload |
cairn^502 | move | active | Fit |
cairn^503 | place | active | Gallery window |
cairn^504 | invariant | active | Pending loads have fresh ids |
cairn^505 | flow | active | Reload, then fit inside |
cairn^901 | assume | active | The Swift frame decoder agrees with Lean's |
cairn^902 | assume | active | Lean decodes what the Swift event encoder writes |
cairn^903 | assume | active | UTF-16 offsets and scalar indices convert exactly |
cairn^904 | assume | active | The text-input shadow predicts Lean's field |
cairn^905 | assume | active | Input-method geometry agrees with Lean's caret |
cairn^906 | assume | active | The host's text metrics are what layout assumes |
cairn^907 | assume | active | Carets follow the painted glyphs |
cairn^908 | assume | active | The host's clock is monotonic milliseconds |
cairn^909 | assume | active | The host wakes Lean by wake |
cairn^910 | assume | active | readFile replies with the file's bytes, or failed |
cairn^911 | assume | active | writeFile is atomic, and replies done only when the bytes are there |
cairn^912 | assume | active | playSound starts a known sound and refuses an unknown one |
cairn^913 | assume | active | http sends the request as given and returns the response as received |
cairn^914 | assume | active | The host answers every request exactly once, with its id |
cairn^915 | assume | active | every ms ticks while started and never after it is stopped |
cairn^940 | assume | active | The native menu shows exactly the frame's menu records |
cairn^941 | assume | active | Choosing a menu item reports that item's ref |
cairn^942 | assume | active | Opening and closing the menu are reported once each |
cairn^943 | assume | active | An overlay panel never takes focus or clicks |
cairn^944 | assume | active | An overlay panel is where its anchor says |
cairn^960 | assume | active | appendFile adds exactly the bytes at the end, or fails and adds nothing |
cairn^961 | assume | active | listDir lists exactly the directory's names, sorted |
cairn^962 | assume | active | deleteFile removes a file or a link, never a directory |
cairn^963 | assume | active | watchFile reports every change to its file, and nothing after its stop |
cairn^964 | assume | active | frontmostApp answers the app in front |
cairn^965 | assume | active | permission answers whether the app holds it, and prompts only when asked |
cairn^966 | assume | active | record streams the levels of exactly the samples it keeps, and nothing after its stop |
cairn^967 | assume | active | A clip's WAV for a range of windows holds exactly those samples |
cairn^968 | assume | active | globalKey reports the hotkey's press and release, and other keys while it is held |
cairn^969 | assume | active | typeText types exactly the text into that app, or nothing |
cairn^970 | assume | active | upload sends the body assembled from its parts, with the secret in its header |
cairn^971 | assume | active | A secret is read from the environment or its file, and never shown |
cairn^990 | assume | active | Wrapped lines paint as wide as Lean measured them |
cairn^991 | assume | active | Lean breaks lines where Core Text would |
cairn^1000 | assume | active | openItem opens exactly the URL or existing file it names |
cairn^1001 | assume | active | appRunning answers whether an app with that bundle id runs |
cairn^1002 | assume | active | readDefault answers the default's value as text |
cairn^1003 | assume | active | makeDir makes a private directory and its parents |
cairn^1004 | assume | active | A painter's pixels stay inside its box |
cairn^1005 | assume | active | record reports started once its microphone is running, before any audio, or fails without it |
cairn^1006 | assume | active | loadImage answers the image's pixel size, or the fault |
cairn^1007 | assume | active | An image's pixels stay inside its box |
cairn^1008 | assume | active | An image is drawn where its oriented pixels are |