# 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](https://cairn.iamnbutler.workers.dev/docs/guide/effects.md) shows the app's side. This page is about the other side:
adding a new kind of request to Cairn itself.

> **Today.** Apps can't declare their own effects yet. The set of requests is fixed by Cairn, and adding one
> means changing Cairn: the Lean types, the encoding and the Swift host, as below. An app in its
> own repository uses Cairn's effects and can't add one of its own; letting it is
> [issue #84](https://github.com/iamnbutler/cairn/issues/84).

## The pieces

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

```lean
/-- 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

```lean
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:

```swift
/// 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](https://cairn.iamnbutler.workers.dev/docs/internals/trusted-base.md). 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.

From https://cairn.iamnbutler.workers.dev/docs/internals/host-effects/. All of Cairn's docs for language models: https://cairn.iamnbutler.workers.dev/llms.txt