A feed that never ends

2026-10-25Milestone 4, done

Sky is the reading half of a Bluesky client, built on Cairn: sign in with an app password, keep the session, and read the home feed for as long as you scroll. It was the fourth milestone and the first of four on Bluesky, which needs nearly everything a small app doesn't: long lists, authentication, paging and requests that race.

Sky lives in its own repository, iamnbutler/sky, as the package sky, built only from registry packages. Its claims are on the registry.

What Cairn gained

Scrolling owned by the runtime. Every scroll offset belongs to Cairn, not the app, and is clamped after every step. A virtual list builds and lays out only the rows on screen: a step costs about 0.17 ms at 1,000 rows and at 100,000.
Secrets. The host captures the session's tokens from the server's replies straight into the Keychain, so they never reach Lean. The password goes in a secure field that shows bullets, keeps no undo and copies nothing.
cairn_atproto, a package for XRPC, the session calls and the timeline, with proofs that only one token refresh runs at a time and each call is sent at most twice.

What's proved about the feed

No duplicates and no gaps.
A late page for an old cursor never changes the feed.
A refresh racing a load-more ends as one of the two would have, in order.

Refresh puts new posts above without moving the post you're reading, and offers a way back to the top. Flinging through 1,102 posts with images, Sky's Lean thread takes a median of 1.5 to 1.7 ms a frame.

The catch

Everything the host is trusted with, from the Keychain to what VoiceOver sees of a scrolled list, is an assumption with a fuzz check of its own rather than a proof. Every path runs against a fake server with no account and no network; reading a real timeline is something I do by hand with the installed app.

Progress log

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

Sky 0.3.1, signed and installed
Sky 0.3.1 is on the public registry as iamnbutler/sky, built on Cairn 0.4.1 with cairn_json and cairn_atproto, all from the registry, and so is its CI in iamnbutler/sky. Its claims export, 26 active claims, is on the registry for its claim pages.
cairn bundle --sign made Sky.app, signed with a Developer ID under the hardened runtime, and it is installed in ~/Applications. Signing in with a real account is the next step, by a person, not by a test: every test signs in to the fake server.
2026-10-26sky@bd64e76
Cairn 0.4.1: the trusted base for M4, fuzzed
Cairn 0.4.1 is out on the public registry as iamnbutler/cairn. Every Keychain call now goes through one serial queue for the process, so a forgetSecret racing a read of the same app's items no longer deadlocks inside Security's file-based keychain (#237), and a value that starts with a byte order mark reads back with it.
What VoiceOver and other assistive apps see of a scrolled list or a secure field was reviewed by hand; it is now two assume claims with a fuzz check each. ^1021: the accessibility tree holds exactly what a scroll area shows, walked through AppKit's own accessibility API on a real view. ^1022: a secure field shows nothing typed, and the debug socket's request log shows no secret. docs/trusted.md lists every assumption M4 added with its check; the full trusted fuzz run passes all 54 checks.
The registry's ledger check accepted 0.4.0 to 0.4.1, a patch release: two new claims and nothing retired. It serves the claims export, 54 active claims, for the claim pages.
2026-10-26a6a35fb
Sky: refresh keeps the reader
Three posts arrived and Refresh put them above: the post at the top of the view didn't move, and Sky offers ↑ 3 new posts to go back to the top. Offscreen render, fake PDS.
2026-10-2596355c0
Sky: scrolled to the end
Scrolling to the end shows the list's end row; its appear loads the next page (30 → 43 posts). Reposts say who reposted; link cards are words for now. Offscreen render, fake PDS.
2026-10-2596355c0
Sky: the home feed
Posts in Cairn's virtual list: avatars and images load from the fake PDS into fixed-size placeholders, text wraps, counts under each post. Offscreen render, fake PDS.
2026-10-2596355c0
Cairn 0.4.0: runtime scrolling, Action.appear, virtual lists and package-scoped fuzzing
Cairn 0.4.0 is out on the public registry as iamnbutler/cairn. Scroll offsets belong to the runtime: a box names itself with Style.scrollRef, the runtime keeps its offset in UI.scroll, moves it for the wheel, trackpad and scroll keys, and clamps it after every step, and a scroll never reaches update (#225). A control with appear := true is told when it comes on screen, through Action.appear. The host's scroll sign is a new assume claim, ^1012.
VList.node lays out only the rows of a list that meet its box, so a runtime step costs about the same at 1,000 rows as at 100,000, with proofs that the rows built are exactly those in view and that the first row showing stays still when rows are inserted above it (#231). Fuzz targets are scoped by package: cairn fuzz runs only a package's own machines unless given --deps, and two targets with one name fail to compile (#224).
The registry's ledger check accepted 0.3.0 to 0.4.0: the only change to the ledger is ^1012. It is a minor release because Event, Action and Trigger gain constructors, so exhaustive matches need new cases; Style and UI gain defaulted fields, and settleFuel is 4. The registry checked the claims export, 54 claims, against the ledger and serves it for the claim pages.
2026-10-25f107007
Sky: a slow sign-in
After a few seconds Sky says it's still signing in and offers Cancel. Offscreen render, fake PDS.
2026-10-256f0aa14
Sky: offline
Sign-in errors are words, not codes: here the service can't be reached. Offscreen render, fake PDS.
2026-10-256f0aa14
Sky: a wrong app password
A wrong password, said in words; the field is emptied as the request is sent. Offscreen render, fake PDS.
2026-10-256f0aa14
Sky: sign in
Sky's sign-in screen (cairn#210): handle or email, the app password in a secure field (bullets only), the service. An offscreen render from the selftest against the fake PDS.
2026-10-256f0aa14
The runtime scrolls the fixture's rows
Cairn's runtime now owns scroll offsets (#203). A scroll of 100,000 points over the fixture's 200 rows is clamped to the end, the app's state never sees it, and the end line, marked appear, hears that it came on screen: an Action.appear move counted in the app. Offscreen render through the real engine (Fixture --scroll-shots).
2026-10-25bed3b86
Cairn 0.3.0: the example apps leave, Keychain secrets, secure fields and scroll boxes
Cairn 0.3.0 is out on the public registry as iamnbutler/cairn. The example apps (Counter, Basics, Todo, Clock, Tray, Gallery) live in their own package, cairn_examples, and their 71 claims keep their numbers there: cairn^202 is now cairn_examples^202, marked moved:cairn_examples in Cairn's ledger, which now holds only framework claims (#219).
A secret can live in the Keychain, and http can capture reply fields into it before Lean sees the body (#216). Text.SecureField shows bullets, never puts its text on the clipboard, in undo history or in any frame dump, and the host turns on secure event input while it has focus (#217). Style.scroll lays out scroll boxes, with proofs that what shows stays inside the box and a control is pressed only where it shows (#218). The frame format is version 11, and the 0.1.3 shims are gone.
The registry's ledger check accepted 0.2.5 to 0.3.0: moving and retiring released claims needs a new minor while at 0.x, and 0.2.6 would have been refused. It checked the claims export, 53 claims, against the ledger and serves it for the claim pages. Apps upgrade by naming an environment secret's source, matching http with eight arguments and importing Cairn.Abi for Cairn.Frame.Boundary.
2026-10-2560c4483
Secure text field
The fixture's Passcode field after typing seven characters: the frame holds seven bullets, never the text, and the host gives it the AXSecureTextField role with no value. An offscreen render of the frame (Renderer.image).
2026-10-251968755