# Shipping

> Checking an app, putting it in a signed bundle, and publishing it with its claim pages.

> **Today.** An app checks and bundles itself with [the cairn tool](https://cairn.iamnbutler.workers.dev/docs/reference/cairn-tool.md), from anywhere
> in its package. The lint, axiom audit and kernel replay that Cairn's `make check` runs have no
> `cairn check` yet; an app's own Makefile calls Cairn's tools for them.

## 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.

```make
# 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:

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

```swift
// 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:

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

```make
# 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](https://cairn.iamnbutler.workers.dev/docs/evidence.md) 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](https://cairn.iamnbutler.workers.dev/docs/reference/evidence.md) and [the cairn tool](https://cairn.iamnbutler.workers.dev/docs/reference/cairn-tool.md).

From https://cairn.iamnbutler.workers.dev/docs/guide/shipping/. All of Cairn's docs for language models: https://cairn.iamnbutler.workers.dev/llms.txt