Yichus

Guide

Give a check the inputs it needs

Some questions need more than source code: a finite set of concurrent requests, a view of related implementations, or seeded database rows. These examples supply those inputs. The safety guide explains which tool to choose and what its result means.

Connect your agent, open the WebMCP workbench, and ask it to run these requests using the linked files.

Check retries, receipts, and concurrent requests

api_protocol_check explores compiled handlers within a declared finite case. It can check that an acknowledged withdrawal has a matching durable receipt, including schedules with uncertain commits. It does not contact a production database.

Download the withdrawal program and its complete case. These are the fixed twin and case from the repository’s transaction-receipt evaluation. Read each file in full, then call:

api_protocol_check({
  "sources": [{"fileName": "withdrawal.bosatsu", "source": SOURCE_TEXT}],
  "case": PARSED_CASE_JSON
})

Inspect protocol and allHold. A completed search establishes only this finite case; a holds result still has proven: false. Exhausted bounds, unsupported operations, and missing required witnesses are inconclusive.

All required case fields

The version is protocol-case-1.0. Every field below is required, even when its value is an empty array or object. Unknown fields and duplicate JSON keys are errors.

schemaVersion, name
The exact version string and a case name.
assumptions
Exactly the six strings in the linked case, once each. They include serializable atomic transactions, no unmodeled writers, and preauthenticated principals.
initialRows
Table names mapped to row-key/value objects. Values follow the checked row types.
initialize
Ordered seed calls with call, integer time, and outcome (committed or unknown-committed). These seed a state; their history is not explored.
requests
Objects with instance, delivery, and call. Each instance/delivery pair is unique. A call names a qualified binding and arguments by parameter name; omit Db, which the checker supplies.
times
A nonempty, strictly increasing array of integer clock values.
externalResults
External binding names mapped to nonempty arrays of typed possible results. The closed model supports article fetch and OpenRouter model calls; unsupported externals are refused.
invariants
Named compiled IO[Bool] observations with argument selectors and a when condition. Predicates may read model databases, not mutate them.
traceInvariants
Named structural assertions, such as return-receipt, immutable-rows, and atomic-writes. At least one invariant across the two invariant arrays is required.
witnesses
Named conditions the search must reach, such as a returned request or nonempty receipt table. An unobserved requirement does not silently pass.
bounds
Positive integers maxStates, maxDepth, maxOperations; nonnegative maxFaults and maxCrashes.

The full protocol specification defines every selector, trace assertion, witness, and assumption. Read it before constructing a new case.

Keep the requirement separate from the implementation. Changing a receipt assertion to accept the receipt your broken handler happens to return does not repair that handler.

Compare implementations against a question

Start with api_abstraction_map for definitions, dependencies, and layers. Use api_organize with lens: "stack" for reading order and a map, "conventions" for neighboring signatures, or "page" for reuse and bypasses. The "implementations" lens adds an authored question, pinned definitions, and comparison roles.

Read the moderator example and its complete view, then call:

api_organize({
  "sources": [{"fileName": "moderator-notes.bosatsu", "source": SOURCE_TEXT}],
  "lens": "implementations",
  "view": JSON.stringify(PARSED_VIEW_JSON)
})

Check ok before reading comparison. The engine validates the referenced definitions and regenerates references, signatures, effects, and source locations. Your group labels and comparison question remain your interpretation; they do not prove organization quality or access safety.

The implementation-view-1 format
schemaVersion
Exactly implementation-view-1.
question
Nonempty text, at most 500 characters.
pins
A nonempty array of distinct Package/Name::binding identities from supplied user packages.
groups
An array, possibly empty. Each group has unique id, label, members (binding identities), and optional parent (group id). A definition may belong directly to one group; parents must exist and cannot cycle.
roles
A nonempty array of objects with unique id, label, and references (binding identities). $effects is reserved.
order
Optional manual layout order, using node:Package/Name::binding and group:id. Omit it to let dependencies determine the order.

Unknown fields, duplicate identities within a list, and nonexistent binding references are refused. Use exact identities from the map instead of guessing package names. focus applies to the stack lens; implementation views use pins.

Edit and compare the larger Forum example.

Seed the key the handler will actually read

api_why accepts rows as table names mapped to key/value objects. For owner_key(principal, local_key), derive the key using that same Bosatsu function. This helper is for computing a test-world key. In the service under analysis, keep owner_key directly at the database operation: the access checker currently cannot follow its proof through a helper function. A row under the plain local key is a different row.

Read the key helper as SOURCE_TEXT and evaluate it:

api_why({
  "sources": [{"fileName": "owner-key.bosatsu", "source": SOURCE_TEXT}],
  "binding": "Yichus/Examples/OwnerKey::key_for",
  "inputs": {"p": {"user_id": "u1", "roles": []}, "local_key": "c1"},
  "observe": false
})

The helper returns IO[String] because the current Why evaluator requires IO for entry points taking a Principal. The key calculation itself is pure.

The returned String is 2:u1c1. Use that value as the JSON row key; for different inputs, evaluate the same helper instead of reimplementing the encoding. Read the Access package source for its definition. Direct handler evaluation uses your supplied identity and seeded world; it does not authenticate an HTTP caller.

Where this fits

What this is about: Safety and Permissions

See it

Learn it

Do it