Program Properties Report

The report combines facts extracted from compiled IR, declarations supplied by the program author, and checker results. Policies and deployment assumptions are inputs to the checks; they are not observations of a deployed system.

• headline: the program's class from a closed vocabulary (crud-api, flow-family, dist-world, escrow-ledger, unrouted-io, pure-library, mixed), derived counts, and counts for unrouted bindings, undeclared tables, and needed artifacts. The schema retains the field name liminal; it means these specific incomplete-wiring counts. The headline is always emitted, including zeros, so zeros mean none of those specific missing-wiring conditions was found.
• map: a structure index. Every node is kind:name; the name joins to the section carrying its data. Each node has a zone (surface / work / state / specs), usage size, an optional problem status, cond references naming unresolved guarantees or needed items, and typed edges (routes_to, reads, writes, deletes, calls, follows, diverges, guards, covers). Call edges appear at detail: full under a deterministic cap that reports elisions.
• overview: the surfaces this program has (routes, tables, flows, dist, escrow, effects, shared-cells, frontend), counts, per-table summaries, tables with multiple writers, and headline facts. Absent surfaces are omitted.
• needed: declarations the analyzers can use but the program lacks, such as an AccessSpec for tables without policy or a ServiceDef for unrouted handlers. Each item includes the same IR-filled snippet returned by api_add_artifact.
• dataModel: each table's access policy (Public, OwnerScoped, Guarded, or GuardedOrRoles) and status (holds / violated / inconclusive), row type, field-read observations, operation key-discipline proofs, readers, and writers. A table whose name cannot be resolved statically appears as an (unresolved table) row and is not dropped. The safety guide explains each policy.
• surface: routes → handler bindings → tables, with declared and inferred permissions plus an effect classification (pure-read, blind-write, read-modify-write) from causal IO edges. A route status of match means only that its declared permissions exactly equal the permissions inferred from that handler's typed-IR effects; it does not prove route behavior or any other guarantee. Unrouted IO bindings are listed in the same form.
• concurrency: shared cells with bounded-interleaving invariants, counterexample traces for violations, and topologySensitivity, which names properties that change under the other deployment topology.
• shape: each package's binding count and 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 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 and links to the routes and tables they serve. Site lists are capped; +N more marks elided entries while counts remain exact. FlowSpec factories are matched against each declared mutation to report structural instances and divergences.
• guarantees: each applicable safety property as a program-specific claim with status, an evidence pointer, bound or topology degree, and assumptions. Inapplicable properties are omitted instead of shown as vacuous passes.

Topology and proof status. proven means no applicable property is violated or blocked under the declared deployment topology. Per-property warnings can remain and are shown with their assumptions. An undeclared topology is treated as multi-instance, meaning many engine instances share one DB. Single-instance semantics must be declared with instances: 1. A blocked property was not established because its check could not run or finish. Warnings can include bounded evidence or deployment assumptions; the composite flag is not an unconditional proof of the application.

Status scopes. The banner summarizes applicable declared guarantees. A needed item is a declaration the IR can support but the program has not supplied, so it is outside that declared set. A warning qualifies the named row or guarantee with an assumption or incomplete degree. A violated status belongs to the named table, operation, invariant, flow, or guarantee; follow its evidence and degree instead of treating every status on the page as one shared verdict.

Briefing an LLM. The companion api_report_brief tool packages the same derived facts for a consumer model: a constant instruction template (byte-identical across programs, "use only these facts; never invent names, counts, causes, or guarantees") plus a projection of the report (headline, map, facts, needed, guarantee claims). The consuming model may write a narrative; this pipeline does not.

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. With the same engine version, source set, options, and topology, reports are deterministic. The tool analyzes Bosatsu programs only.

Preset programs. Four small programs cover 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 inventory preset exercises the needed section. Three larger programs cover ProjectHub, a multi-entity sync service with owner-scoped and public tables; OrderFlow, an order/inventory module whose six mutations provably instantiate one declared flow factory with zero divergences; and FeedMapper, a larger pure transformation library. 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, subject to the frontend generator’s verification and route-shape checks.

Recorded benchmark. The committed corpus at eval/corpus/program-report gives one fresh agent a 30-question closed-option quiz about nine programs using reports alone and another the same quiz using sources alone. The gate requires equal or better accuracy than the source arm and tokenLift above 1 (source-arm tokens divided by report-arm tokens, so above 1 means the report arm was cheaper). This is a self-run, single recorded probe, rerun after table-status and cap-accounting changes. ProgramReportEvalTest re-derives each answer-key label from engine output, and CI checks the recorded verdict byte-for-byte.

In that recorded probe, both arms scored 29/30. The probe environment recorded per-arm token totals, so eval-gate reports measured tokenLift of 1.31 and a pass. The report arm used fewer tokens at the same recorded accuracy. Read the exact latest gate artifact, report-arm score, and source-arm score.