An app built from packages alone

2026-10-24Milestone 3, done

Pairs is a memory game: a grid of face-down cards, flip two, keep them if they match. Decks are theme packs, a JSON manifest and a set of images, loaded from a folder or a URL. It was the third milestone, small enough to finish, and it needs what a Bluesky client needs: images, JSON and many requests in flight at once.

It's also the first app built only through the package path, cairn new pairs --bin, cairn add and cairn build, in a repository of its own. Nothing in it reaches into Cairn's.

What Cairn gained

Images. An image node whose size Lean knows before the pixels arrive, so the layout never jumps, and an effect that loads one. The host decodes and paints; Lean never holds pixels.
JSON as its own package, cairn_json, with a proof that decoding what was encoded gives it back.
Requests in flight: at most six at once, with the rest queued. Switching packs cancels them, and a late reply for an old pack never changes the board.

What's proved

The grid follows the window, and for every width no two cards overlap and every card is inside it.
The deal has every face exactly twice, at most two unmatched cards are face up, and every game can be won.
A best score only improves.

The catch

Decoding images, caching them and the network belong to the host: they're recorded as assumptions and fuzzed, not proved. The grid always fits the window, so nothing in Pairs scrolls; scrolling waited for Sky.

Progress log

The videos and notes from this milestone as the work landed, newest first.

Yap on cairn_json
Yap's overlay mid-dictation, now built on Cairn 0.2.5 with JSON from the cairn_json package instead of its own parser. Yap 0.1.0 is on the registry.
2026-10-25bdf391d
Cairn 0.2.5: closing the window quits cleanly
Cairn 0.2.5 is out on the public registry as iamnbutler/cairn. Closing an app's window now quits it cleanly: the window delegate owns the window and shuts the view down before the app terminates. Before, AppKit also released the window on close, and a frame landing afterwards reached the freed window; Pairs 0.1.2 crashed that way. make selftest closes a real window with input, a timer and frames in flight (#199).
cairn builds fetch registry dependencies at the commit the manifest pins and turn Lake's lazy fetches off when every git dependency is on a registry: a stale checkout on Pairs went from 92 s to 4 s (#198). The tray's tick-rate selftest asserts the wall-clock rate on real hardware only (#195).
The registry checked its claims export, 122 claims, against the ledger and serves it for the claim pages. claims.lock is the same as 0.2.4's: no claim was retired, moved, changed or added, so it is a patch release.
2026-10-25ea05c5e
Cairn 0.2.4, with a fuzzer that plays the host
Cairn 0.2.4 is out on the public registry as iamnbutler/cairn. cairn fuzz now plays the host's side: it answers requests late and in any order, replies to cancelled ones, fires timers, moves the clock, sends subscription events and evicts images, within what the trusted claims allow, and checks that every image a frame draws is one the host holds (#189).
An app's Custom fuzz hooks take replies and subEvents generators, relations checked on every step, drained checks once the host has answered everything, and outstanding checks against the requests the runtime still holds (#189, #192).
The registry checked its claims export, 122 claims, against the ledger and serves it for the claim pages. claims.lock is the same as 0.2.3's: no claim was retired, moved, changed or added, so it is a patch release.
2026-10-25654c669
Cairn 0.2.3, with several apps a package and cairn bundle
Cairn 0.2.3 is out on the public registry as iamnbutler/cairn. A package can hold several apps, and cairn build, size, bench and conformance take --app to link one (#177), as iamnbutler/cairn_examples does. cairn bundle wraps an app package's release build in a .app with the SwiftPM resource bundles it uses (#185).
The fuzzer now presses status-item buttons and menu items and takes App.minSize as the window's minimum, so Clock, Tray and Gallery are fuzzed (#178, #182). The click assumptions ^7 and ^214 moved from the examples into Cairn's trusted base, with pointer fuzz checks (#184).
The registry checked its claims export, 122 claims, against the ledger and serves it for the claim pages. claims.lock is the same as 0.2.2's: no claim was retired, moved, changed or added, so it is a patch release.
2026-10-258ecf96e
Pairs: the win screen
All eight pairs of Patterns matched: the board gives way to the result, and the best moves and time for the pack are saved (they only ever improve, pairs^26).
2026-10-25e3d4416
Pairs: a pack that fails
A pack with a missing image: Pairs says which face didn't load and leaves the game exactly as it was. A 404 manifest and a pack.json that isn't JSON are refused the same way.
2026-10-25e3d4416
Pairs: a pack loading over http
A pack typed into the field loads beside the game from the URL tests' stub server, whose images answer after three seconds: the game goes on, with Cancel and a count of the images loaded. Choosing another pack or Cancel stops it; its late replies change nothing (pairs^28, ^29).
2026-10-25e3d4416
Pairs: the grid follows the window
The same game in a wider, shorter window: Grid keeps four columns and shrinks the cards to fit the height; nothing scrolls. App.minSize from Grid.minBox keeps every card at least 64 points wide.
2026-10-25e3d4416
Pairs: a game in progress
Pairs, the M3 memory game, built only from registry packages (cairn 0.2.2, cairn_json). Three pairs of Shapes are matched (green edges); the arrow and the heart don't match and turn back after a second. Rendered offscreen from the app's own frame.
2026-10-25e3d4416
Cairn 0.2.2, with a window minimum and an image budget
Cairn 0.2.2 is out on the public registry as iamnbutler/cairn. An app declares its window's smallest size with App.minSize, and Grid.minBox gives the smallest box in which every card is at least its minimum width, proved for every size; the host keeps the window at least that big (#169, frame format 7). Sub.imageCache keeps the host's images within a byte budget, and the host tells the app with an evicted notice for every image it drops, so ready always means the pixels are there (#170, frame format 8).
The registry checked its claims export, 122 claims, against the ledger and serves it for the claim pages. No claim was retired, moved or changed, so it is a patch release; five are new, ^511–^513, ^1010 and ^1011.
2026-10-25885b585
Image cache under a budget
Gallery runs an imageCache subscription with an 8 MiB budget. Load 24 fetches all 24 thumbnails; the host keeps the twelve on screen and drops the other page's, telling the app, which counts them as evicted and no longer takes them for loaded. Next page loads the dropped ones again, and the host drops the first page's in turn.
2026-10-25ecdc04f25s
Cairn 0.2.1, with claim pages
Cairn 0.2.1 is out on the public registry as iamnbutler/cairn. Requests in flight are capped at 6, with a queue and cancelRequest, frame format 6 (#151). Cairn.UI.Grid lays cards out in as many columns as the window fits, proved for every size (#160). cairn fuzz, claims, bench, size and conformance run on any app, and test/fixture is Cairn's own fixture app (#149).
cairn publish now sends the claims export as well as claims.lock. The registry checked its 117 claims against the ledger and serves it, so Cairn's claim pages group its moves and flows by place instead of showing only ledger rows (#156). No claim was retired, moved or changed, so it is a patch release; six are new, ^506–^510 and ^1009.
2026-10-25d08381d
A floor on tile size
Gallery asks the host to keep its window at least 1020 × 536: the smallest size, proved with Grid.minBox, at which every tile is 180 points wide. The demo drags the window narrower, shorter, then both, through the window's resize delegate as a person's drag goes; it stops at the minimum each time and the tiles stay 180 points wide.
2026-10-25f6e6ad222s
Claim pages
Every package on the registry gets claim pages, rendered by the site from the claims export cairn publish now sends: the overview grouped by place, then the Todos window, a flow's steps, a move, and one of the trusted base's assumptions. No agent and no screenshots of the apps: proofs, witnesses and where each claim is defined come straight from Lean. Shown here with Cairn's export from this branch; the live pages fill in once Cairn is published again. These replace the maps, and /map/ redirects here.
2026-10-24f45df9b15s
Gallery's grid follows the window
Gallery's six tiles in a grid whose column count Lean computes from the window size: three columns at 1120 points, six at 1640, two at 860, in reading order throughout. The host only reports resize events; Lean proves the cells never overlap, stay inside the grid's box, take the most columns that fit, and that a click in a tile reaches that tile.
2026-10-24ee9ecbf15s
Many requests in flight, and Cancel
Gallery asks for 24 thumbnails from a slow server. Lean's runtime sends six at a time and queues the rest; Cancel drops the queued ones and stops the six being fetched, and a late answer for a cancelled one changes nothing.
2026-10-24ebac00223s
Cairn 0.2.0, with images
Cairn 0.2.0 is out, on the public registry as iamnbutler/cairn next to 0.1.3. It has images: Node.image, the loadImage effect, frame format 5 and the Gallery example (#132). import Cairn now links, the old everything-umbrella is CairnAll, and cairn new --bin makes a working app (#134). cairn-link links each dependency's libs from its cairn.toml, and Cairn's says libs = ["Cairn"] (#127).
It was going to be 0.1.4, and v0.1.4 is tagged, but the registry refused it: claim ^213's statement hash changed when Style gained its image field, and a published claim keeps its statement. Its meaning didn't change, so the same invariant is now ^225 and ^213 is retired. Retiring a released claim needs a new minor version while at 0.x, hence 0.2.0.
2026-10-2416b70b8
cairn new makes an app that links
Since the library split, the Cairn umbrella imported every proof and tool, none of which an app links, so an app that wrote import Cairn, as cairn new's template did, failed at the host's link on initialize_cairn_Cairn (#128). Now Cairn is the linked library's umbrella, with the claim commands at compile time only, and the everything-umbrella the ledger, the audit and the docs read is CairnAll. cairn new --bin writes a working app: a place, a move, its exports, the C declaration of its initializer and a host with a selftest. make check now builds one against the checkout, runs its selftest and locks its two claims, which takes about a minute.
2026-10-24a2d3ff9
Gallery: images
Six image tiles, each a 200 × 150 Node.image that Lean lays out before any pixels exist: a PNG, a JPEG turned by its EXIF orientation, a GIF, a poster over https, a text file and a missing file. The host decodes with ImageIO and paints with Metal; Lean only learns the pixel size, or the fault, from the loadImage reply. Reload (^501) sends every tile back to its grey placeholder and reads each source again; Fit (^502) cycles cover, contain and stretch. Nothing moves when a picture arrives or fails. In the self test every tile was answered 6.8 ms after launch.
2026-10-248254f5031s
cairn_json, the first package outside the cairn repository
Yap's JSON parser and encoder is now its own registry package, cairn_json 0.1.0, in iamnbutler/cairn_json. It requires cairn ^0.1.2 from the registry, is pure Lean with no Swift and no extern, and leaves Yap's date arithmetic for a later cairn_date.
The library is 491 lines. 793 lines of proofs hold 49 theorems: decode (encode v) = some v and decode (pretty v) = some v for every value nested at most 512 deep, and that more fuel never changes what the parser answers. decode is total by construction, with no partial def. The axiom audit allows only propext, Classical.choice and Quot.sound, and the kernel replays every declaration.
A trusted fuzz check compares it with Foundation's JSONSerialization: 220,164 documents per seed (valid, mutated, UTF-16 and UTF-32, random bytes and 164 edge cases), 5 seeds, 0 unexplained differences. The known ones are listed in its docs/trusted.md: numbers Foundation can't hold, a leading U+FEFF Foundation drops from strings, short UTF-16 and UTF-32 documents without a byte order mark, invalid UTF-8, and nesting 513 deep.
The commit is cairn_json's.
2026-10-24bf6a0e7
cairn-link links each dependency's libraries
bin/cairn-link no longer links Cairn's library by name (#118). It reads lake-manifest.json, finds the cairn.toml beside each dependency, transitive ones included, and links the Lean libraries that package lists under libs. Cairn's own cairn.toml now lists Cairn, so an app gets the same archive as before, and a library like cairn_json can be linked the same way.
It refuses a Lean module that ends up in two archives, which would be a duplicate symbol, and a dependency that is an app. A dependency with no cairn.toml is linked not at all; if linked code imports it, cairn-link names the package and says to give it one.
Checked with a throwaway app that depends on Cairn and on a second library package with its own libs: it links, and a small C program draws a frame through both. Yap builds against it with its existing --lib Yap and passes its selftest.
2026-10-241e1b640