Cairn Docs Claims Blog Packages
Contents

Contributing

Writing host effects

How a new kind of request reaches the host, and what it takes to trust the answer.

An app asks the outside world for something by returning a request effect with an id it chooses. The host runs it and sends back exactly one reply under that id. The effects chapter shows the app's side. This page is about the other side: adding a new kind of request to Cairn itself.

The pieces

A request is a constructor of Request. Each one has a kind, and the kind decides which replies can answer it:

/-- Something the host does that answers back. Closed: adding a kind is a constructor, its
encoding, a `Reply.answers` case and one host handler (docs/effects.md). -/
inductive Request where
  | readFile (path : String)
  /-- Replace the file atomically, creating missing parent directories. -/
  | writeFile (path : String) (data : ByteArray)
  /-- A named system sound ("Tink", "Pop", "Basso", …). -/
  | playSound (name : String)
  /-- An HTTP request. With a `secret`, the host adds its header as it sends (a missing secret
  answers `failed notFound` and sends nothing). With a non-empty `capture`, a 2xx reply whose
  body is a JSON object has each listed top-level string field (`(field, account)`) written to
  the Keychain item `account` and its value replaced by `""` in the body Lean receives; all or
  nothing: a body that isn't a JSON object, or a listed field that is missing, repeated or not
  a string, answers `failed invalid` and writes nothing. Other replies pass through as they
  came. With `redact`, the request carries a secret the person typed (a secure field's text,
  `Cairn.Text.SecureField`): every dump, log and report prints its URL, headers and body as
  `<redacted N bytes>`, and the host sends it as given. -/
  | http (method url : String) (headers : List (String × String)) (body : ByteArray)
      (timeoutMs : Nat) (secret : Option Secret := none)
      (capture : List (String × String) := []) (redact : Bool := false)
  /-- Append to the file, creating it (mode 600) and missing parent directories. -/
  | appendFile (path : String) (data : ByteArray)
  /-- The names in a directory (not `.` and `..`), sorted by their UTF-8 bytes. -/
  | listDir (path : String)
  /-- Remove a file or a symbolic link; never a directory. -/
  | deleteFile (path : String)
  /-- The app in front: its process id and name. -/
  | frontmostApp
  /-- Whether the app holds `p`; with `prompt`, the system also asks the person if it doesn't. -/
  | permission (p : Permission) (prompt : Bool)
  /-- Bring process `pid` to the front and type `text` into it as key events, then Return if
  `pressReturn`. Needs Accessibility. -/
  | typeText (pid : Nat) (text : String) (pressReturn : Bool)
  /-- `http` with a body of parts the host assembles and an optional secret header (OpenAI's
  transcription request: multipart framing from Lean, the clip's WAV and the key from the
  host). -/
  | upload (method url : String) (headers : List (String × String)) (secret : Option Secret)
      (body : List Part) (timeoutMs : Nat)
  /-- The host may drop the clip's samples. -/
  | forgetClip (clip : Nat)
  /-- Open `target` with its default app (the Finder for a folder, the default editor for a
  text file, System Settings for its URLs): a path (`~/` is the home folder) or a URL with a
  scheme. -/
  | openItem (target : String)
  /-- Whether an app with this bundle identifier is running. -/
  | appRunning (bundleId : String)
  /-- The value of `key` in the defaults domain `domain` (`defaults read domain key`), as UTF-8
  text: a string as it is, a number or a boolean as its text (booleans as `1` or `0`). -/
  | readDefault (domain key : String)
  /-- Create the directory and its missing parents, each private (mode 700); `done` if it is
  already a directory. -/
  | makeDir (path : String)
  /-- Load the image at `source` (a file path, `~/` for the home folder, or an `http`/`https`
  URL) and answer its size in pixels (`Reply.image`); the host keeps the decoded pixels under
  `source` and paints them for `Style.image`s that name it. Lean never sees the pixels. An image
  the host already holds is answered from what it holds, unless `reload`, which reads `source`
  again. -/
  | loadImage (source : String) (reload : Bool)
  /-- Delete the Keychain item `account` (`Secret.Source.keychain`): `done`, also when there is
  none. -/
  | forgetSecret (account : String)
deriving Repr, BEq, Inhabited
lean/Cairn/Effects.lean, lines 69–130
inductive Reply where
  /-- `writeFile`, `appendFile`, `deleteFile`, `makeDir`, `forgetSecret` and `playSound`
  succeeded. -/
  | done
  /-- `readFile`'s contents, or `readDefault`'s value. -/
  | bytes (data : ByteArray)
  /-- An HTTP response, whatever its status. -/
  | http (status : Nat) (headers : List (String × String)) (body : ByteArray)
  /-- Any request can fail. -/
  | failed (fault : Fault) (message : String)
  /-- `listDir`'s names. -/
  | names (names : List String)
  /-- `frontmostApp`'s process id and name (empty when it has none). -/
  | app (pid : Nat) (name : String)
  /-- `permission`'s or `appRunning`'s answer. -/
  | flag (granted : Bool)
  /-- `loadImage`'s answer: the image's size in pixels (after its orientation is applied). -/
  | image (width height : Nat)
deriving Repr, BEq, Inhabited

/-- Whether a reply has the shape that answers a request of kind `k`. -/
def Reply.answers : Request.Kind → Reply → Bool
  | _, .failed .. => true
  | .readFile, .bytes _ => true
  | .writeFile, .done | .playSound, .done | .appendFile, .done | .deleteFile, .done => true
  | .typeText, .done | .forgetClip, .done | .openItem, .done | .makeDir, .done => true
  | .forgetSecret, .done => true
  | .readDefault, .bytes _ => true
  | .http, .http .. | .upload, .http .. => true
  | .listDir, .names _ => true
  | .frontmostApp, .app .. => true
  | .permission, .flag _ | .appRunning, .flag _ => true
  | .loadImage, .image .. => true
  | _, _ => false
lean/Cairn/Effects.lean, lines 164–197

Reply.answers is what the runtime uses to keep its promise to the app. It keeps a table of pending ids and their kinds, and it delivers a reply only when the id is pending and the reply has a shape that answers that kind; failed answers anything. A duplicate, late or misshapen reply is dropped. This is proved, whatever the host sends, so the app sees each request answered at most once, with a reply of the right shape.

On the host, each kind has one handler in a table, keyed by the kind's code:

/// The requests the host can run, by `Request.kindCode`. Adding a kind is one entry here (and
/// its Lean constructor, encoding and `Reply.answers` case).
public struct Handlers: Sendable {
    public var table: [UInt8: RequestHandler]
    public init(table: [UInt8: RequestHandler]) { self.table = table }

    public static let standard = Handlers(table: [
        0: { r, reply in if case let .readFile(p) = r { reply(Files.read(p)) } },
        1: { r, reply in if case let .writeFile(p, d) = r { reply(Files.write(p, d)) } },
        2: { r, reply in if case let .playSound(n) = r { Sounds.play(n, reply) } },
        4: { r, reply in if case let .appendFile(p, d) = r { reply(Files.append(p, d)) } },
        5: { r, reply in if case let .listDir(p) = r { reply(Files.list(p)) } },
        6: { r, reply in if case let .deleteFile(p) = r { reply(Files.delete(p)) } },
        7: { _, reply in reply(Apps.frontmost()) },
        8: { r, reply in if case let .permission(p, prompt) = r { Permissions.check(p, prompt: prompt, .live, reply) } },
        12: { r, reply in if case let .openItem(t) = r { reply(Opening.open(t)) } },
        13: { r, reply in if case let .appRunning(b) = r { reply(Opening.running(b)) } },
        14: { r, reply in if case let .readDefault(d, k) = r { reply(Opening.readDefault(d, k)) } },
        15: { r, reply in if case let .makeDir(p) = r { reply(Files.makeDir(p)) } },
    ])
}
host/Sources/CairnHost/World.swift, lines 30–50

A handler runs on a global queue and calls reply once. The callback is guarded, so a second answer is ignored; a kind with no handler is answered failed invalid. Handlers must not call Lean. When the app restarts, answers to earlier requests are dropped and every subscription stops. Tests swap the table: a self test sends files to a scratch directory and plays no sound.

Adding a kind of request

  1. The constructor. Add it to Request in lean/Cairn/Effects.lean, with its Kind, and add the cases of Reply.answers that answer it. If no existing reply fits, add a Reply constructor too.
  2. The encoding. Give it a record in the frame encoder (lean/Cairn/Frame/Encode.lean) and, for a new reply, in the event encoder (lean/Cairn/Frame/Events.lean). Extend the round-trip proofs; they close with omega once the new case is written arithmetically. Add it to the canonical dump, which the corpus compares.
  3. The Swift mirror. Add the case to the Swift model and decoder in host/Sources/CairnFrame, and to the debug JSON the conformance driver reads.
  4. The handler. Write it, and add it to Handlers.standard. Keep it to doing what was asked and reporting what happened: anything that decides app behaviour belongs in Lean.
  5. The assumption. The handler is trusted code, so state what it promises as an assume claim, write a fuzz check that gathers evidence for it, and add an entry to the trusted base. Say what it does on bad input: empty strings, NUL, names the file system refuses, a network that never answers.

make check then runs the round trips, the corpus and a short fuzz of the new check.

What makes a good host effect

  • Failure is a reply. A missing file, a refused permission or a timeout is failed with a fault and a message, never a missing reply. An HTTP 500 is not a failure: it is a reply with status 500, and the app decides.
  • The app chooses the id, so it can tell a late answer to an old request from a new one.
  • Fake the device. A handler that touches hardware or other apps (the microphone, the keyboard, typing into another app) takes its device as a parameter, so the fuzz suite and the self tests run against fakes and make check never records audio or types anywhere.
  • Ask for permission explicitly. A request that needs a macOS permission fails with failed denied without it. Whether to prompt is a separate request the app makes on purpose.

Subscriptions

An ongoing input, like a repeating timer, a file watch, recording or a global key, is a subscription rather than a request. The app returns the set it wants after each step; the runtime works out what to start and stop, and the host sends events tagged with the subscription's id. Adding a kind follows the same steps: a Sub constructor, its command encoding, its events, a handler in the host's world, and an assumption with a fuzz check.