Shipping · Cairn docs

Check it

make check is what every change to Cairn must pass. It lints for banned constructs, builds everything, audits every theorem's axioms, replays every declaration through the kernel, checks the claim ledger, runs the Swift tests, and runs the per-app checks on the fixture: its self test, a short fuzz, its binary size and its own ledger.

# Everything a PR must pass. The per-app checks run on test/fixture, Cairn's own app; the
# example apps are in their own repository, iamnbutler/cairn_examples.
check: lint audit ledger kernel doctest test selftest fuzz-quick fuzz-scope size fuzz-trusted-quick fixture-ledger site-build registry-check new-check cairn-tool-test

Makefile, lines 68–70

The self test

An app's executable has a --selftest mode: it runs the real host, with its threads and accessibility mirror, but no window, and drives the app through its controls. The fixture's checks presence through accessibility, the way an assistive app would see it:

var f = settle()
expect("first frame size", "\(f.size.w)x\(f.size.h)", "480x600")
if need("^2").accessibilityRole() != .textField { fail("^2 is not a text field") }
if need("^3").accessibilityRole() != .button { fail("^3 is not a button") }
expect("left at start", label(" left") ?? "", "0 items left")

// Focus the field (an AX focus is a click at its centre), type, press Enter.
need("^2").setAccessibilityFocused(true)
f = settle()
if f.textInput?.control.label != "^2" { fail("the field is not focused after an AX focus") }
type("  Buy milk ")
view.doCommand(by: #selector(NSResponder.insertNewline(_:)))
settle()
expect("checkboxes after Enter", ids("^4#"), ["^4#1"])
expect("item label (trimmed)", need("^4#1").accessibilityLabel() ?? "", "Buy milk")

// Type again, then press Add; toggle item 1; delete item 2.
type("Eggs")
press("^3")
expect("checkboxes after Add", ids("^4#"), ["^4#1", "^4#2"])
press("^4#1")
expect("^4#1 value", need("^4#1").accessibilityValue() as? Int ?? -1, 1)
expect("left after toggle", label(" left") ?? "", "1 item left")
press("^5#2")
expect("delete buttons after delete", ids("^5#"), ["^5#1"])

test/fixture/Sources/Fixture/main.swift, lines 108–132

and waits for the timer Flash set to come back through the host's clock:

// Flash: its timer comes back through the host's clock, and the note goes.
press("^6")
if label("Flashing") == nil { fail("no Flashing note after a press on ^6") }
let deadline = hostNow() + 5
while label("Flashing") != nil {
    if hostNow() > deadline { fail("the Flash timer never fired") }
    RunLoop.current.run(until: Date(timeIntervalSinceNow: 0.05))
    view.applyLatestFrame()
}

test/fixture/Sources/Fixture/main.swift, lines 136–144

Fuzzing and conformance

cairn fuzz generates random sequences of moves from the claims and checks every claim's post, every invariant, and presence and pressability, after every step. cairn conformance replays sequences against the running app through its debug socket and compares it with the Lean model at every step. Each needs a little of the package: a fuzz executable over fuzz_targets%, and a generator module, <App>.Conformance. The fixture's lakefile declares both:

/-- `cairn conformance`'s generator entry point (Cairn's docs/conformance.md). Declared after
`Fixture`, whose root would otherwise claim it. -/
lean_lib FixtureConformance where
  roots := #[`Fixture.Conformance]

/-- `cairn fuzz`: Cairn's claim-driven fuzzer on the app (Cairn's docs/fuzz.md). -/
lean_exe fuzz where
  root := `FuzzMain

/-- The likes' mutant (Fixture/LikeMutant.lean): `cairn fuzz`'s server catches a write retried
blind after a lost reply. -/
lean_exe likeMutant where
  root := `Fixture.LikeMutant

test/fixture/lean/lakefile.lean, lines 27–39

Cairn's make check runs cairn fuzz --iterations 200 on the fixture. Conformance opens the app's window, so it isn't in make check.

Size

A Cairn app should be a few megabytes. The commands that declare claims need Lean's compiler at build time, and linking the compiler into an app makes it about 100 MB, so apps only meta import them. cairn size builds the app for release, attributes its bytes, and fails past 5 MB:

# Binary size (bench/size.md): the fixture's executable built for release with a link map,
# stripped, attributed (Lean runtime, Cairn, the app, Swift host, shaders), and checked against
# SIZE_LIMIT bytes, with `cairn size` (test/fixture/build/size/). No app links `Lean` (the
# compiler, about 100 MB), so it is a few MB; crossing the limit almost always means something
# imported `Lean`.
SIZE_LIMIT = 5000000

Makefile, lines 269–274

Bundle and sign

cairn bundle writes a .app bundle, build/apps/<Name>.app, from a release build. The package's bundle/Info.plist and bundle/entitlements.plist go in it when they exist. --sign signs it with an identity; without it the bundle is signed ad hoc.

Sign a release build with a stable identity. Signing with the same identity every time matters: macOS grants permissions such as Accessibility and the microphone to the code signature, so a differently signed build is a new app and has to be granted again. A package's Makefile can find the first valid Apple Development identity with security find-identity and pass it to cairn bundle --sign.

Publish it

cairn publish sends a tagged version to the registry with its claims export, and the site renders its claim pages from that: every claim, grouped by place, with its proofs, a flow's steps and where it's defined. Nothing on them is written by hand. See the evidence ladder and the cairn tool.