Cairn · API
Cairn
Cairn
What an app imports: import Cairn (in a module, public import Cairn). It brings in every
module of the Cairn library, the code bin/cairn-link links into an app (lakefile.lean): the
app model, layout, text, the runtime and its ABI (Cairn.Abi, Cairn.Runtime.Abi,
Cairn.Text.Host), effects, and the claim language, whose commands it meta-imports so they
run at compile time only (docs/claims.md, "Linking"). No proofs, no import Lean at run time.
The proofs, tests and tools are in other libraries, and CairnAll imports them all for the
ledger, the axiom audit and the docs. Keep this list to the Cairn library's roots: a module
outside it would make every app's link fail (bin/cairn-link warns).
75 modules · 2,966 declarations · 1,181 theorems, every one on the standard axioms · 80 claims (15 proved, 63 assumed, 2 retired) · 2 doc tests, all passing · 47 private declarations hidden · trusted base: 39 checks
Modules 75
| Module | Decls | Claims | About |
|---|---|---|---|
| Cairn | What an app imports: import Cairn (in a module, public import Cairn). | ||
| Cairn.Abi | 2 | The runtime's Boundary, filled in: v1 event decoding, Frame.ofLaid, v1 frame encoding. | |
| Cairn.Abi.Tests | 28 | Checks for Cairn.Abi, kept out of the module so they can use #guard (a #guard in a module needs a meta import of what it evaluates): the frame encoder's font clamping, then concrete checks of the runtime on a small app, laid out b | |
| Cairn.App | 19 | An app is its state, its surfaces, and its moves. | |
| Cairn.Claim | 14 | Claims: statements about the product with durable ids. | |
| Cairn.Claims | Claims as a language feature: the runtime vocabulary (Cairn.Claims.Core) and the claim commands (move, flow, invariant, assume, place, retire, moves%, claims%). | ||
| Cairn.Claims.Core | The runtime half of the claim language: moves, dispatch, machines, flows, invariants, assumptions and places, with their theorems. | ||
| Cairn.Claims.Deliver | 5 | The claim guarantees, carried through the runtime. | |
| Cairn.Claims.Elab | 65 | The claim commands: move, flow, invariant, assume, place and retire, and the moves% and claims% terms. | |
| Cairn.Claims.Machine | 25 | A machine is an initial state and the moves that act on it. | |
| Cairn.Claims.Move | 41 | Moves and the update they induce. | |
| Cairn.Claims.Registry | 18 | The claim registry: an environment extension holding one entry per claim declared by the claim commands, in this module and every module it imports. | |
| Cairn.Effects | 62 | The outside world as data (docs/effects.md): the time the host reports, the requests an app can make and the replies they get, and the subscriptions an app can ask for. | |
| Cairn.Font | 21 | Text metrics: the one place layout depends on the host. | |
| Cairn.Frame | 43 | What crosses the boundary each frame, before encoding. | |
| Cairn.Frame.Build | 39 | Frame.ofLaid: a laid-out tree becomes what crosses the boundary: draw commands in paint order, the accessibility tree, and the focused field's text-input state. | |
| Cairn.Frame.BuildTests | Checks for Cairn.Frame.Build, kept out of the module so they can use #guard (a #guard in a module needs a meta import of what it evaluates). | ||
| Cairn.Frame.Bytes | 103 | The byte layer of the boundary format (docs/frame.md): little-endian primitives, three ways. | |
| Cairn.Frame.Dump | 32 | A canonical text dump of frames and events (docs/frame.md, "Canonical dump"). | |
| Cairn.Frame.Encode | 286 | Frame byte format (docs/frame.md; version 13): specification encoder Wire.Enc.frame, decoder Wire.Dec.frame, the executable encoder encodeFrame (proved equal to the specification and installed with @[csimp]), and the round trip `dec | |
| Cairn.Frame.Events | 43 | Event byte format v2 (host → Lean, docs/frame.md): specification encoder Wire.Enc.events, decoder Wire.Dec.events, and the round trip decodeEvents_encodeEvents. | |
| Cairn.Frame.EventsTests | Checks for Cairn.Frame.Events, kept out of the module so they can use #guard (a #guard in a module needs a meta import of what it evaluates). | ||
| Cairn.Frame.Layout | 1 | Frame.ofLaid composed with layout. | |
| Cairn.Frame.Menu | 23 | Frame.ofMenu: a status item's menu description becomes the flat list of menu records the frame carries (docs/frame.md, "Menu records"), parents before children, as the accessibility list is. | |
| Cairn.Fuzz | |||
| Cairn.Fuzz.Collect | 9 | Elaborates to a List Cairn.Fuzz.Target, one per Machine declared in an app module (appModule: an app package's own) of the imported environment. | |
| Cairn.Fuzz.Host | 47 | cairn fuzz's stand-in for the host's side of the world (docs/fuzz.md, "The host"): it keeps what the frames asked of it and answers the way the real host is allowed to, as the trusted claims state it (docs/trusted.md): | |
| Cairn.Fuzz.Main | 24 | `` lake exe fuzz <App> [--seed S|random] [--iterations N] [--steps K] [--budget-ms M] [--out DIR] [--shrink N] [-v] lake exe fuzz --list [--deps] `` | |
| Cairn.Fuzz.Metrics | 17 | Layout and text theorems quantify over every TextMetrics that is Valid, so the fuzzer shouldn't test with the mono stand-in only. | |
| Cairn.Fuzz.Rng | 25 | SplitMix64 (Steele, Lea and Flood, "Fast splittable pseudorandom number generators", 2014): a 64-bit state advanced by a constant, then mixed. | |
| Cairn.Fuzz.Shrink | 8 | Delta debugging (Zeller and Hildebrandt's ddmin) over a failing sequence's operations: remove chunks while the shorter sequence still fails the same check on the same claim, halving the chunk size down to single operations. | |
| Cairn.Fuzz.Target | 4 | A Target bundles a machine (and the App built from it, if any) with what the claims say about it. | |
| Cairn.Fuzz.Text | 5 | Scripts of TextOps for a field's edit moves. | |
| Cairn.Fuzz.Trusted.Claims | 65 ^ | The trusted base's assumptions (docs/trusted.md), each naming the check of the trusted-base fuzzer that gathers its evidence (make fuzz-trusted, build/fuzz/trusted.json, docs/fuzz.md "Trusted base"). | |
| Cairn.Fuzz.Trusted.Export | 13 | C exports for cairn-fuzz-trusted (host/Tests/CairnFuzzTrusted), the Swift executable that links this library next to the Swift host, so both sides of each trusted boundary run in one process (docs/fuzz.md, "Trusted base"). | |
| Cairn.Fuzz.Trusted.Gen | 35 | Random frames for differential fuzzing of the Swift frame decoder (docs/fuzz.md, "Trusted base"). | |
| Cairn.Fuzz.Walk | 96 | One sequence: a window size, text metrics, and operations generated from the current state (or replayed from a list), each checked against the app's claims (docs/fuzz.md). | |
| Cairn.Geometry | 29 | Geometry in integer logical points, origin top-left, y down. | |
| Cairn.Input | 51 | What the host sends Lean (Event), what the runtime gives an app (Action), and what an app asks the host to do (Effect). | |
| Cairn.Layout | |||
| Cairn.Layout.Bridge | 53 | The runtime's pressable theorems (Cairn.Runtime.hitTest_center, click_center_presses) take Cairn.Runtime.LayoutFacts laid t: the control's visible rect is nonempty and a pointer at its centre reaches it. | |
| Cairn.Layout.Check | 18 | Pressable w l (Bridge.lean) is stated with Laid.Everywhere, an inductive Prop, so it can't be decided directly. | |
| Cairn.Layout.Core | 55 | layout m window node turns a Node into a Laid: every rect, clip, baseline, caret and selection resolved in integer logical points. | |
| Cairn.Layout.Facts | 22 | The vocabulary for the layout theorems: controls of a tree, a predicate holding at every node (Laid.Everywhere), the local facts layout establishes at each node, and Facts, the package the runtime's pressability proof consumes. | |
| Cairn.Layout.Grid | 30 | About Cairn.Grid (Cairn/UI/Grid.lean), for every box size and every number of cards. | |
| Cairn.Layout.Para | 15 | measure turns Node.para ts wr s into a clipping column (paraStyle wr) of one Sized.text per line (paraLines). | |
| Cairn.Layout.Proofs | 124 | The headline is Cairn.Layout.facts: for every valid metrics, window and view, layout satisfies Facts. | |
| Cairn.Layout.Rigid | 47 | Layout/Check.lean proves a view pressable by evaluating its layout, which works for one concrete state, window and set of metrics. | |
| Cairn.Layout.Scroll | 5 | The framework's facts about scroll boxes (Style.scroll, docs/layout.md, "Scroll boxes"), for any scroll box, any children, any text metrics and any window: | |
| Cairn.Layout.Tests | Concrete checks of layout with the mono metrics (13 pt: 7 points per scalar, ascent 10, descent 2, so a line is 12 high). | ||
| Cairn.Layout.VList | 6 | Cairn.VList proves which rows a virtual list builds and that, in the heights it lays out by, each row starts where the one before ends (Model.top_succ). | |
| Cairn.Optimistic | 89 | A Table K V holds values a person changes and a server keeps, keyed by K (a post's URI, an account's DID). | |
| Cairn.Optimistic.Claims | 16 | 15 ^ | Cairn.Optimistic's claims (cairn^1100–cairn^1114, docs/optimistic.md), stated over a harness machine whose state is the server model's World at keys Nat and boolean values (liked or not), with same equality. |
| Cairn.Optimistic.Server | 104 | The abstract server Cairn.Optimistic is proved against (docs/optimistic.md, "The server model"). | |
| Cairn.Runtime | |||
| Cairn.Runtime.Abi | 7 | The Lean side of the app ABI. | |
| Cairn.Runtime.InFlight | 93 | Requests in flight (docs/effects.md, "Requests in flight"): what the runtime guarantees about the cap, the queue and cancelled requests. | |
| Cairn.Runtime.Proofs | 118 | Theorems about the runtime: actions name controls on screen, interaction state stays sound, and a click at a reachable control presses it. | |
| Cairn.Runtime.ScrollProofs | 48 | Theorems about scrolling and appear (docs/runtime.md, "Scrolling" and "Appear"): every offset stays within its box after every step, a scroll changes nothing but the UI, Tab brings the focus into view, and appear moves are exactly the m | |
| Cairn.Runtime.Step | 110 | The interaction runtime: turns host events into the Actions an app's update sees. | |
| Cairn.Runtime.World | 30 | The runtime's view of the outside world (docs/effects.md): the clock, the app's timers, its pending requests and its active subscriptions. | |
| Cairn.Runtime.WorldProofs | 122 | What the runtime guarantees about the outside world (docs/effects.md, "Semantics"). | |
| Cairn.Surface | 30 | What an app shows besides a window (docs/surfaces.md): a menu bar status item with its native menu, and a non-activating, click-through overlay panel, both as data. | |
| Cairn.Text.Field | 63 | Field is the editing model behind every text field: the text, caret, anchor, IME marked range, undo and redo stacks, and placeholder. | |
| Cairn.Text.FieldTests | Checks for Cairn.Text.Field, kept out of the module so they can use #guard (a #guard in a module needs a meta import of what it evaluates). | ||
| Cairn.Text.Host | 21 | Core Text metrics from the host, as a TextMetrics. | |
| Cairn.Text.Proofs | 77 | 1. | |
| Cairn.Text.Wrap | 19 | Lean decides where wrapped text (Node.para) breaks; the host only measures. | |
| Cairn.Text.WrapProofs | 30 | For every text cs, width W and offsets o (any function: nothing here assumes the offsets are monotone, so it holds for every TextMetrics, valid or not): | |
| Cairn.UI.Grid | 63 | A Grid lays equal cards out in rows, as many columns as fit the box's width. | |
| Cairn.UI.Hit | 40 | Hit testing over a laid-out tree. | |
| Cairn.UI.Images | 54 | An app keeps one Images in its state. | |
| Cairn.UI.Node | 135 | What view returns (Node) and what layout produces (Laid). | |
| Cairn.VList | 89 | A VList is a scroll box over a list the view names in full (every row's key) but builds only in part: the rows that meet the viewport, plus overscan points above and below, with a spacer for the rest above and one for the rest below (do | |
| CairnAll | Every module of Cairn but the tools and the fuzzer: the linked code (Cairn), its proofs and tests, and the umbrellas over them. |