Yichus

Idea

For application authors and their coding agents

Check who may do what

A handler can return valid JSON and still expose someone else’s notes. A test with Alice’s account may miss the mistake. We built a checker that follows how every supported database operation in the supplied program uses its declared access policy.

You write the handlers and policies in Bosatsu; the server engine supplies identities and performs the database operations.

Break a rule, then check the repair

1. Read the caller’s notes

The broken handler reads another user’s row. Choose Run function to see the returned note, then Check access to locate the owner-key violation. Select After the fix and repeat both actions. The policy stays the same; the database key changes to the caller’s key.

Code & run Owner-key defect and repair

2. Keep a private thread behind its guard

The forum’s can_see predicate decides thread visibility. Run read_thread as Bob, then change user_id to carol under Inputs. The seeded thread includes Bob and excludes Carol. Check access verifies the use of guards in the compiled program.

The checker verifies use of the declared guard; it does not decide whether the guard expresses your intended policy. Compare the concrete callers with the rule you intended.

Code & run Membership guards in the forum

3. Keep a moderator helper behind a role-protected route

This smaller example lets moderators read a named owner’s notes. Check access, then edit the route line as shown below and check again. The handler and table policy are unchanged, but an ordinary authenticated route can now reach the privileged read.

The deliberate mistake and its repair

Replace this role-protected route:

role_route("/review", handler("review_notes", review_notes), ["moderator"], [ReadPerm("notes")]),

with this ordinary route:

route("/review", handler("review_notes", review_notes), [ReadPerm("notes")]),

Change the role_route import to route too; Bosatsu checks unused imports. Check access to see the violation. Reset the example to restore the role requirement and recheck. Do not make the table Public to silence the finding.

Code & run Role authority follows every route to a handler

The drawer’s Run function calls a handler directly in a seeded in-memory world. It does not go through HTTP authentication. Check access checks the declared route structure. The server engine must enforce those roles before invocation.

Another experiment: declare the wrong operation permission

Keep the moderator route but remove ReadPerm("notes") from its permission list, leaving []. Also remove ReadPerm from the Yichus/Service import. Run api_permissions on the same sources in the WebMCP workbench. The route still requires a moderator, but its declaration omits the read performed by its handler. Restore the permission and import, then run api_verify to check the complete API contract.

Three questions behind a permission check

Authentication, declared operations, and row access answer different questions. A read permission on a route does not decide whose rows it can read.

  1. At the server boundary

    Who may enter?

    The engine verifies identity and required roles before calling the handler.

    route / role_route / public_route
  2. In the compiled handler

    What may it do?

    Compare declared read, write, create, delete, and query permissions with inferred database effects.

    api_permissions
  3. At each database operation

    Which rows may it use?

    Check owner keys, required guards, or the roles required by every route reaching the operation.

    api_access_check
A map of responsibilities. The two static checks inspect the supplied program; they do not authenticate a network request or certify a production identity provider.

route requires an authenticated caller. role_route also requires every listed role. public_route is anonymous: it may run a storage-free calculation, or read/query resources declared Public. It cannot request a Principal, the runtime-supplied caller identity.

The four resource policies
OwnerScoped
Every supported keyed read, write, or delete must use the caller’s Principal.user_id or owner_key(principal, local_key). The checker currently needs owner_key directly at the database key position; it cannot prove that same key through a helper function. An unproven result does not by itself demonstrate a data leak. An arbitrary request field is not an owner proof. Unkeyed create/query operations are rejected.
Guarded(guards)
Declared predicates control row use. Analysis checks that protected writes and values read from a row are used in supported guarded paths. Fresh-row creation has its own rules. The checker verifies that the required guard is used; you must decide whether that guard expresses the intended policy.
GuardedOrRoles(guards, roles)
Ordinary routes follow the guards. A handler may instead use the resource when every route reaching it requires every listed role. Adding an ordinary route to a privileged helper can invalidate that proof. With no guards, the policy is role-only, including reads and creates.
Public
The resource imposes no owner-key or row-guard discipline. Route authority and declared operation permissions still apply. Declaring a table Public changes the policy; it does not repair an ownership bug.

The Access package reference specifies the supported forms, including guard handling and fresh-row creation. The Service reference defines routes.

Read the property, method, and assumptions

proven / holds
Read the named property and method. A static access proof, a completed finite protocol search, and a law that held on generated cases have different scope.
violated
Inspect the operation or counterexample. Fix the implementation or reconsider an incorrectly specified requirement explicitly; do not silently weaken the policy to get green.
blocked / inconclusive
The check did not establish the property. Missing metadata, unsupported operations, exhausted budgets, and unfilled witnesses need attention.
warning
A qualification remains. The composite API gate can be proven with warnings; preserve them in the explanation and deployment decision.
Why a single-instance declaration changes the result

The Notes add_note handler reads a list and writes the extended list. Multiple engine instances sharing one database can lose updates. An unspecified topology is treated as multiple instances. Compare these commands from a repository checkout:

yichus api verify demos/service/notes-api.bosatsu
yichus api verify --instances 1 demos/service/notes-api.bosatsu

The second command accepts the relevant findings as warnings under the single-instance contract. It does not add a transaction. Declare one instance only when that is the deployment; use transactions or another appropriate serialization mechanism when the operation needs coordination.

The current integrity model can flag multiple transactional writers even when they are correct. The read-modify-write check also cannot distinguish separate transaction instances. Inspect whether the dependent read and write share one transaction; a passing read-modify-write result alone does not establish that. A finite protocol case can test the declared transaction behavior within its stated bounds.

The trusted boundary includes the Bosatsu compiler, Yichus analyzers, and runtime adapters. A transaction model assumes the storage adapter provides its stated atomicity; an owner proof assumes the engine supplies the correct authenticated principal. These tools do not independently prove a production database, JWT implementation, or arbitrary external library correct.

Read the engine contract. A storage-free API may omit AccessSpec only when the checker establishes absence of storage across the supplied bindings and reachable helpers. Unknown effects or missing metadata block that exemption.

Let your agent work in the same examples

Connect your agent through WebMCP, then open this guide with WebMCP enabled on the same computer. Each drawer has source, revision, run, check, and visible-feedback tools. Read the tool schemas after discovery; the relay may add tab suffixes to their names.

Prompt: break and restore the role boundary 
Read yichus_example_guide, then list this page’s examples and read moderator_notes.
Check its access policy and read the visible feedback before editing.
Change its role_route to an ordinary route, updating the import and removing the roles argument.
Keep the handler and GuardedOrRoles policy unchanged. Use the current expectedRevision for each edit.
Run the access check and show the operation whose proof failed.
Restore the required moderator role, recheck, and read yichus_example_feedback.
Explain why direct Run function output does not test HTTP authentication.
Report the source revision, property, evidence, and remaining runtime assumptions.

For the other checks, open the API workbench, call api_guide, and supply every file in the program to the selected tool. Before generating an application, require api_verify to be proven under the intended topology. Use yichus_app_act and yichus_app_feedback to test the generated interface the user sees; keep those observed results separate from static claims.

Where this fits

See it

Learn it

Do it