Program Properties Report

Zoom levels, every fact computed from the compiled IR — nothing is author-asserted:

• overview — the surfaces this program actually has (routes, tables, flows, dist, escrow, effects), counts, per-table one-liners, the concurrency surface (tables with multiple writers), and headline facts. Absent surfaces are omitted, never rendered as zeros.
• needed — declarations the analyzers would use but the program does not have (an AccessSpec for tables with no policy, a ServiceDef for unrouted handlers), each with a paste-ready snippet filled from the IR — the same snippet api_add_artifact returns.
• dataModel — per table: access policy (Public or OwnerScoped) with a three-valued status (holds / violated / inconclusive), the row type with per-field observation (is the field ever read), key-discipline proofs per operation, and readers/writers. A table whose name cannot be resolved statically appears as an (unresolved table) row — never silently dropped.
• surface — routes → handler bindings → tables with declared vs inferred permissions and an effect narrative (pure-read, blind-write, read-modify-write) from the causal IO edges; unrouted IO bindings listed the same way.
• concurrency — shared cells with bounded-interleaving invariants, counterexample traces embedded only when violated, and topologySensitivity: exactly which properties flip at the other deployment topology.
• shape — each package's binding count and its IO-participating bindings with their types, dataflow roles (pure, terminal-io, or an IO orchestrator), and DB effect kinds (DbRead, DbWrite, DbCreate, DbDelete, DbQuery). The default detail: summary lists only the IO-participating bindings; detail: full enumerates every binding.
• abstractions — bindings used from two or more sites, with exact use and caller counts from the IR call-site index, anchored to the routes and tables they serve. Site lists are capped; +N more marks elided entries, the counts stay exact. FlowSpec patterns (a typed binding naming a factory function and the mutations claimed to follow it) are matched against each mutation: instances that provably follow the factory, divergences that don't.
• guarantees — each applicable safety property restated as a program-specific claim with status, an evidence pointer into the section that proves it, degree (bound, topology assumed), and assumptions. Inapplicable properties are omitted, not listed as vacuous passes.

Topology. proven means every applicable property holds under the declared deployment topology. An undeclared topology is treated as multi-instance (many engine instances sharing one DB) — the conservative default. Single-instance semantics must be declared with instances: 1.

Run it on your own program. yichus api report file.bosatsu prints the compact JSON; -o out.html writes a self-contained HTML document; --detail full enumerates every binding; the api_report MCP tool takes the same arguments. Reports are deterministic: the same program produces the same bytes. The tool analyzes Bosatsu programs only.

The presets. Four small programs (the owner-scoped notes API, its deliberately leaky twin, the stock flow demo, and an inventory module with unrouted db_* handlers and no AccessSpec — the needed section in action) and three large ones: ProjectHub, a 2,145-line sync service whose 16 owner-scoped and public tables are proven at the default multi-instance topology with no topology declaration; OrderFlow, an order/inventory module whose six mutations provably instantiate one declared flow factory with zero divergences; and FeedMapper, a 2,022-line pure library of 171 bindings. A companion artifact, the generated ProjectHub frontend, is produced by api_frontend from a FrontendSpec (a typed binding that selects and titles routes as views) in the same sources, gated on the same proof.

Recorded. In the recorded benchmark (eval/corpus/program-report), one fresh agent answers a 30-question closed-option quiz about nine corpus programs from the committed reports alone; another answers from the sources alone. Both arms scored 30/30. Cursor Task completion notifications do not include subagent_tokens, so eval-gate computes tokenLift from bytesReadApprox (1.25 on this pair, verdict pass) rather than invented token counts. Every answer-key label is re-derived from the engine's own output by ProgramReportEvalTest, and the recorded verdict is re-checked byte-for-byte in CI.