Yichus

Example

Bosatsu Service Fixtures and Notes API Verification

This page separates one working generated application and its verified API from smaller source fixtures. The Notes API has routes, owner-scoped storage, verification tools, and a generated frontend. The other files demonstrate individual pure or IO patterns; they are not deployed servers.

Code & run Run and repair the Notes handler

Start with the Notes app for working behavior, or open the browser verification tools to run the same API checks against editable source.

Notes API: owner-scoped routes and generated frontend

notes-api.bosatsu is a multi-tenant notes service: every row is keyed by Principal.user_id, declared OwnerScoped. yichus access / api_verify check that from Matchless IR. notes-api-leaky.bosatsu is the same module with list_notes reading another user's row; the checkers report access:notes violated. For the exact source files supplied at generation time, api_verify checks the applicable static properties under instances: 1, and api_frontend refuses generation unless that verdict is proven and every declared view matches a typed route, its input and result fields are representable, and the configured transport and authentication pair is supported. This does not establish that a separately deployed API will remain the same version as the generated screen. Inspect the API source, frontend specification, and generated verifier request and response. In the generated in-process app, switching Dev user ids demonstrates that the owner-keyed rows shown to alice and bob are separate. The complete Notes check needs instances: 1 because add_note is a read-modify-write handler; the default multi-instance topology reports that concurrency risk.

Owner-scoped access check

Call api_access_check for owner scoping. Call api_verify with instances: 1 for the full Notes verdict. The verdict artifact class is api-safety-1.0.

Open `notes-api.bosatsu`

Read the generated `api_verify` request and verdict

Leaky Notes fixture and violated access verdict

db_read(..., "other-user") is a typed-IR violation, not a naming heuristic.

Open `notes-api-leaky.bosatsu`

Generated notes app

This app is an in-process frontend generated from notes-app.bosatsu. Add a note as alice, switch to bob, and see an empty list.

Open the generated app

Source fixture inventory and implemented scope

These files are useful for reading isolated program shapes. Only the Notes route above links to a working generated application. Each card states what its fixture implements and links to the complete source for context.

Pure route selection

Maps a path string to a handler-name string. It does not start a server or process a request.

Open `api-gateway.bosatsu`

Inventory read/write/create sequence

Sequences a database read, writes the unchanged item back, then creates an order. It does not validate stock or decrement inventory.

Open `inventory.bosatsu`

Open `inventory-service.bosatsu`

Transport transforms

Decode wire data, map it into domain types, and expose compiled dependencies to the Explorer.

Open `dynamo-transform.bosatsu`

Handler registries

Looks up entity-specific parsers, field accessors, and serializers from a handler list.

See `make_handler` and `find_handler`

String-format pipeline fixture

Composes three pure functions that prefix a string with ingest, transform, and emit labels.

Open `data-pipeline.bosatsu`

String-format scheduler fixture

Formats a job name and minute into one string. It has no queue, retries, clock, or execution state.

Open `job-scheduler.bosatsu`

API gateway fixture performs pure route selection

api-gateway.bosatsu is a pure String -> String function. It selects labels for two paths and otherwise returns a not-found label; no HTTP server, transport, or handler execution is present.

Pure path-to-label function

package Demo/Service/ApiGateway

def route: String -> String =
  path ->
    if path == "/health" then "health-handler"
    else if path == "/metrics" then "metrics-handler"
    else "not-found"

Fixture scope and next route

Use this fixture to inspect typed control flow and input influence. It demonstrates route selection only.

For implemented routes, permissions, storage effects, and a generated frontend, read the Notes API and run the Notes app.

Inventory fixture sequences three database effects

The function reads an inventory item, writes that same item back unchanged, then creates an order. It demonstrates effect composition, not inventory purchasing rules.

Read, unchanged write, and order creation

package Demo/Service/Inventory

def purchase(db: Db, item_id: String, quantity: Int) -> IO[Order]:
  item <- db_read(inventory_table(db), item_id).flat_map()
  _ <- db_write(inventory_table(db), item_id, item).flat_map()
  db_create(orders_table(db), Order("pending", item_id, quantity))

Implemented behavior and limits

  • The effect sequence is visible in one place: read inventory, write the unchanged item, create an order.
  • No branch checks available stock, and no expression decrements the item's stock field.
  • Use the Explorer to inspect which read and arguments influence each effect.

Read the companion service fixture for more service-shaped source, or return to Notes for working routes.

Structural properties exposed by the service fixtures

Typed IR makes effect sites, dependencies, and argument influence available to analysis. These are structural facts, not a universal safety verdict. Use the Explorer guide to inspect a particular binding.

Effects are values

The supported read and write primitives return IO values. Handlers compose those values, and the host runtime executes them.

Input-influence analysis

Yichus can inspect whether a parser, handler, or transform depends on its inputs and report constant-derived or discarded paths.

Handler selection and domain functions

Handler selection, transforms, and domain rules can be expressed as normal functions and registries rather than framework-specific annotations spread across files.

Transport and domain stay separate

The demos lean on explicit transport types and explicit mapping into plain application models. Those mapping functions provide a place to handle wire-format differences.

Explicit filters and permissions

The Dynamo fixture carries FilterConfig values, and Notes routes carry permission lists. The scheduler fixture does not implement scheduling.

Source links match the displayed examples

Each section links to the complete Bosatsu file behind its excerpt, so the omitted definitions and fixture limits are available for inspection.

Dynamo transport parsing and mapping

This pure Bosatsu fixture parses Dynamo-shaped values, chooses a registered entity parser, applies filters, and maps transport records into plain application records. Read the complete source alongside the layer map below.

Parsed and mapped structures

Takes raw DynamoDB JSON (as DynamoValue enums), parses them into typed transport models (User[String], Post[String]), applies workspace and date-range filters, converts numeric strings into plain application models (UserPlain, PostPlain), and routes items through a handler registry based on entity type tags.

The nested author pattern is particularly useful for CRUD systems: a Post contains a User author, and the parser plus mapper stack keeps that shape intact instead of flattening everything into ad hoc maps.

Analysis questions and limits

Transport parsing, handler lookup, filter application, and output construction all live in one analyzable file. The fixture does not connect to DynamoDB or run a server.

For this file, the Explorer can report whether a parser depends on the incoming record, whether a filter reads the configured fields, and whether a transform is rooted in constants. Those are typed-IR dependency facts about this fixture, not a runtime correctness or performance result.

Source and tests

Start with dynamo-transform.bosatsu for the implementation, then compare each top-level test value with the relevant function.

Dynamo wire-to-application transformation layers

The diagram names the four source-level representations in the fixture and the functions connecting them. Open the source to inspect each parser, mapper, and handler lookup.

Wire layer: DynamoValue (DynString, DynNumber, DynMap, ...)
↓ parse_User / parse_Post
Transport layer: User[String], Post[String]
↓ map_User / map_Post (with to_int)
Application layer: UserPlain, PostPlain
↓ process_item + find_handler
Handler layer: EntityHandler dispatch + FilterConfig

Parameterized transport types

User[num] and Post[num] are parameterized by their numeric type. When parsed from DynamoDB, numbers come as strings: User[String]. The map_User function converts them generically: pass in string_to_Int and you get User[Int]. This pattern means you write the mapping logic once and reuse it across all numeric conversions.

Single-pass collectors

Instead of calling lookup(entries, "field") for each field (which scans the list each time), the parsers use a single-pass collector that walks the entry list once and accumulates all fields simultaneously. This is a performance optimization that also makes the parsing logic more explicit -- each field match is visible in one place.

Handler registry

EntityHandler wraps a name, a parser, field accessors, and a serializer into a single existential type. find_handler looks up the right handler by entity type tag ("_et"). This pattern scales cleanly: adding a new entity type means adding a new handler to the list, not modifying existing dispatch logic.

Composable filters

FilterConfig combines workspace ID filtering with date-range filtering (both created and modified). Each filter dimension is independently optional. The pipeline applies all filters after parsing, so an item that passes the workspace filter but fails the date filter is still rejected. Empty filter lists mean "accept all."

FeedSnapshot recursively maps nested numeric fields

The fixture includes a FeedSnapshot type that nests FeedEntry → Post → User. The existing source excerpt shows the type shape; the recursive mapping test value supplies a complete example. 

struct FeedEntry[num](
  post: Post[num],
  featured_author: User[num],
  ranking_score: num
)

struct FeedSnapshot[num](
  workspace_id: String,
  generated_at: String,
  entries: List[FeedEntry[num]],
  total_score: num
)

# Converting the entire tree from String to Int requires
# exactly one function call:
mapped = map_FeedSnapshot(snapshot, safe_int)

The map_FeedSnapshot function automatically applies the conversion to every numeric field at every nesting level: the snapshot's total_score, each entry's ranking_score, each post's view_count and word_count, and each author's age and score. Read the mapper definitions to see each recursive call.

Ten top-level Dynamo test values

The test file exports one suite containing 10 top-level test values. Some values contain nested TestSuite values with several assertions, so “10” counts top-level entries rather than assertions. Read the full test source for the nested assertions and fixtures.

Wire → Transport

  • DynNumber values unwrap to strings
  • Nested DynMap authors parse correctly
  • All seven User fields are extracted
  • All eight Post fields are extracted

Transport → Application

  • map_Post applies conversion recursively
  • Nested author fields convert to Int
  • parse_UserPlain composes parse + convert
  • parse_PostPlain handles nested conversion

Pipeline & Filters

  • Unknown entity types are dropped
  • Workspace filter keeps matching items
  • Date-range filter rejects out-of-range items
  • Deep FeedSnapshot mapping converts all levels

Explorer questions for the Dynamo transform

Point Explorer at the Dynamo source to inspect each binding's dependencies, arguments, and constant-derived paths. The result is evidence for the specific query you run, not a universal verdict over every binding. Follow the Explorer command guide for overview and trace routes.

Checks to run

  • Do the parse_* functions depend on their entries input?
  • Does process_item actually call find_handler?
  • Do the map_* functions apply the conversion function to every numeric field?
  • Are any filter predicates hardcoded to always return True?

How to interpret the results

A return-data path represents a potential dependency from the named input to a selected output in the compiled model. A literal-root, discarded argument, or missing dependency identifies a path to inspect. None of those labels alone proves the whole program safe.

Compare the reported path with the corresponding test value and the complete implementation.

Additional source fixtures and their scope

These links are source-reading routes. The cards distinguish implemented structure from service behavior that is not present in the fixture.

Inventory

This fixture reads an item, writes it back unchanged, and creates an order. It never decrements stock.

API gateway routing

This fixture maps a request path to a label with pure functions. It has no server, no request parsing, and no handler invocation.

Dynamo transform

This fixture implements wire decoding, handler registries, transport mapping, and composable filtering.

Data pipeline

This fixture composes three pure string-prefix functions in order.

Background job scheduler

This fixture formats a job name and a minute as a string. It has no queue, no retries, and no execution state.

Run the Notes verifier or inspect a source fixture

For a computed verdict, open the API verification tools, load the Notes source, and run api_verify with instances: 1. For the smaller fixtures, use Explorer overview and trace commands to inspect a stated dependency question.

Run the API tools · Read a generated verdict example · Read the inventory effect fixture · Read the pure route selector · Read the full Dynamo source · Read the tests · Read the Explorer operation guide

Where this fits

What this is about: Safety and Permissions

See it

Learn it

Do it