# Bounded transaction protocol verification `yichus protocol` explores a finite case against the compiled program. It follows actual Matchless guards and values, commits each transaction atomically, and schedules external dispatch separately from its response. It never runs the production database, clock, fetch adapter, or model provider. Run the checked-in Icetakes example from the repository root: ```sh yichus protocol --case icetakes/probes/article-retrieval.protocol.json \ --result /tmp/retrieval-verdict.json --ir /tmp/retrieval-ir.json \ icetakes/app/identity.bosatsu \ icetakes/app/contribution-model.bosatsu \ icetakes/app/contribution-intake.bosatsu \ icetakes/app/article-retrieval.bosatsu \ icetakes/probes/article-retrieval-invariants.bosatsu ``` This input list is the `retrieval-protocol` set printed by `node icetakes/sources.mjs retrieval-protocol --paths`. The command prints a compact verdict. `--result` additionally records a sourced witness trace for every required reachable condition; violations always include a counterexample. `--ir` exports the versioned protocol skeleton, lexical values, and Matchless guards. Requested output files are removed before compilation, so a failed check cannot leave an old success artifact. Exit zero means `holds` within the case; violations, unsupported operations, invalid input, and exhausted bounds exit nonzero. A `holds` result always has `proven: false`. The browser's native `api_protocol_check` tool accepts `sources` (the usual array of `{fileName, source}`) and `case` (the object below). Both may be JSON-encoded strings for WebMCP clients. It returns the compact verdict under `protocol` and an `allHold` boolean. `api_report` accepts the same declaration as `protocol_case`; `yichus api report --protocol-case ` exposes it in the report. The additional section does not change the report's universal proof result. ## Case format: protocol-case-1.0 Every top-level field below is required. Unknown fields and duplicate JSON keys are rejected recursively. The complete runnable example is [article-retrieval.protocol.json](../icetakes/probes/article-retrieval.protocol.json). The replacement-worker and final-attempt cases sit beside it. | Field | Contract | | --- | --- | | `schemaVersion` | Exactly `protocol-case-1.0`. | | `name` | Human-readable case name. | | `assumptions` | Exactly the six strings listed below, each once. | | `initialRows` | Typed world seed: table names to row-key/value objects; `{}` starts empty. | | `initialize` | Ordered seed calls `{call, time, outcome}`. Each executes exactly one successful atomic transaction and then returns. `outcome` is `committed` or `unknown-committed`. These are declared prefixes, not explored histories. | | `requests` | `{instance, delivery, call}` entries with nonempty identities. Each `(instance, delivery)` pair must be unique. | | `times` | Nonempty, strictly increasing integer clock domain. Transactions choose any listed time at least the current time. | | `externalResults` | Binding name to a nonempty finite array of typed results for every external reached. The closed model supports `Yichus/ArticleFetch::fetch_article` and `Yichus/OpenRouter::openrouter_call`. | | `invariants` | Bosatsu observation predicates described below. At least one invariant, including trace invariants, is required. | | `traceInvariants` | Structural schedule assertions described below. | | `witnesses` | Required reachable conditions. Missing witnesses make the result inconclusive. | | `bounds` | Integer `maxStates`, `maxDepth`, `maxOperations` (positive), `maxFaults`, `maxCrashes` (nonnegative). | Required assumptions: ```json ["serializable-atomic-transactions", "rollback-on-abort-and-retry-exhaustion", "commit-unknown-may-commit", "stable-time-within-attempt", "no-unmodeled-writers", "preauthenticated-principals"] ``` A `call` is `{ "binding": "Package/Name::function", "arguments": { ... } }`. Arguments use **parameter names** from the typed function. Supply every non-`Db` parameter and no extra keys; the checker supplies its immutable model database. Values use the public typed JSON codec, including named constructor objects. Field positions and enum tags are resolved from compiler types. The pure `Yichus/Json::parse_json` and `render_json` boundaries run their production JVM implementations in the model. Model calls remain deferred: a case supplies finite `ModelResult` outcomes, and the checker rejects requests or outcomes that the generated OpenRouter adapter would reject before dispatch or return. Each declared provider result is an assumption about that finite case, not a live provider observation. ## Observation predicates An invariant entry names a compiled `IO[Bool]` function: ```json { "name": "current-lease-and-input", "binding": "Icetakes/RetrievalInvariants::completion_has_current_lease", "arguments": { "before": "before", "after": "after", "now": "time" }, "when": "always" } ``` Argument values are selectors, not source expressions. `before` and `after` select immutable databases immediately before and after the latest scheduler transition; `time` selects its integer clock. For `when: "return"`, `return` selects the just-returned value and `request.` selects that request's named argument. Selector types must equal parameter types. Predicates may read these databases; writes and other IO are rejected. Return predicates automatically require a return witness, preventing success from a wholly unobserved return path. Use `explore --agenda` and `organize` on the predicate's complete source set, then read their findings alongside the protocol case. The explorer does not see entry points selected by a separate case JSON, and generic samples of unrelated records may never satisfy an identity comparison. An unexecuted reference or constant-result observation is therefore a prompt to investigate, not evidence that a predicate is dead or correct. Require witnesses for the states the invariant describes, and test a deliberately broken implementation that must produce a named counterexample. The [Icetakes completion cases](../icetakes/probes/2026-09-25-completion-coherence.md) demonstrate this workflow with typed source relationships and durable receipts. ## Trace assertions Every entry has `name` and `kind`; the table lists its remaining required fields. Names across invariants and witnesses must be unique. | Kind | Fields and meaning | | --- | --- | | `external-after-commit` | No extra fields. Each external dispatch's previous event for that delivery must be an acknowledged commit. | | `unique-external` | `field`: named request field whose values must be unique across dispatches. `operation` may name either supported external binding; omitting it retains the original article-fetch meaning. For model calls, use `operation: "Yichus/OpenRouter::openrouter_call"` and `field: "request_key"`. | | `atomic-writes` | `trigger`: table; `required`: nonempty table-name array. A durable transaction writing the trigger must write every required table in that same transition. | | `unique-return` | `resultPath`: across every returned response in a schedule, the projected values must be pairwise distinct; a response the path does not select is ignored. Use it for "at most once" results, such as one dispatch permission per attempt. Like a receipt assertion, it adds a witness that some response was selected. A return is its own scheduler step, so a return predicate's `before` and `after` are the same store and cannot express this. | | `immutable-rows` | `table`: every existing key/value must survive unchanged in the next state. | | `stable-constructor` | `table`, `field`, `constructor`: rows whose named field has that typed constructor must survive unchanged. | | `return-receipt` | `table`, `keyBinding`, `keyArguments`, `resultPath`, `rowPath`: project a returned receipt and its durable row and require exact typed-value equality. The key function returns `String`; its arguments use return selectors. | Projection paths are arrays of `{ "field": "name" }` and `{ "constructor": "Name" }` steps. A constructor step selects one enum arm; a different arm is inapplicable, while unknown fields/constructors are errors. For example `[{"constructor":"Committed"},{"field":"value"}]` selects a committed outcome's value. Result and row projections must have the same type. A receipt assertion automatically requires an applicable returned receipt witness. ## Reachability witnesses Each witness has `name`, `kind`, and these additional fields: | Kind | Fields | | --- | --- | | `table-nonempty` | `table` | | `external-count` | Positive integer `count` (at least this many dispatches). | | `event` | `event`: `unknown-committed`, `unknown-uncommitted`, `crashed`, `aborted`, `retry-exhausted`, `returned`, `external-started`, or `external-returned`. | | `sequence` | Nonempty `events` array of `{event, phase}`; event is `unknown-committed`, `started`, or `returned`. Matches an ordered subsequence across the whole schedule. Phase zero is request start; each transaction increments that delivery's phase. | | `predicate` | `binding`, `arguments`, `when`, with the observation-predicate contract above. | ## Interpretation and limits A successful transaction may acknowledge commit, return commit-unknown with its writes durable, return the same commit-unknown with no durable writes, or exhaust retries with no writes. Fault alternatives consume the declared global fault budget. Retry exhaustion may also happen before an otherwise-aborting body runs (for example, repeated serialization failures at `BEGIN`). Aborted transaction bodies roll back. Each attempt sees one stable clock. A crash ends all active deliveries on an instance; declared deliveries that have not started may run afterward as fresh work. External dispatch and external return are separate schedule transitions, allowing other requests and crashes between them. Exploration is exhaustive only over the supplied requests, initializer state, finite clock/result domains, and fault/crash bounds. State/depth/operation cutoffs and unsupported operations are inconclusive. The checker establishes no unbounded liveness, fairness, authentication, network policy, or production database-adapter correctness. In particular, five declared initialization attempts are a seed history, not an exploration of every possible five-attempt history. The conformance suites replay actual generated JavaScript with a controlled adapter and compare JVM transaction and model-call behavior with model transitions. They test that boundary under the declared adapter contract; they do not certify a deployed PostgreSQL adapter, JWT implementation, external fetch service, or model provider. The retained [earlier retrieval report](../icetakes/probes/article-retrieval-report.json) remains a separate artifact and is not replaced by a runtime-test success label.