Example

Application case study / Icetakes

Find a better home for shared code.

A diagram of an application we were building showed why adding its next workflow felt awkward: shared records and storage lived inside other workflows. We moved those definitions into modules that both could use.

Icetakes is a reading-site project: people submit articles and arguments, and an editorial workflow evaluates them. Its application rules are written in Bosatsu. Yichus compiles those rules and gives us tools to inspect their structure, check declared properties, and run them.

This is a development record. It covers a storage refactor, a decoder cleanup, and defects we discovered in Yichus itself. It does not establish that the whole application is ready to deploy.

01 / Organization

Preparation needed storage owned by completion.

One workflow prepares an article for evaluation. Another accepts a completed evaluation. Both need the same task records and job tables, but their definitions originally lived in JudgmentCompletion. Preparation had to import that workflow to use its storage.

Before

Reuse crosses a workflow boundary.

LawyerPreparation imports JudgmentTask, jobs_table, and judgment_tasks_table from JudgmentCompletion.

After

Both workflows use a shared store.

Those definitions live in JudgmentStore. Preparation and completion each import the shared module.

What the tool showed

Through WebMCP, an agent called api_abstraction_map and api_organize with the implementations lens. The resulting map let us follow preparation’s references to the tables and inspect their source. This made the ownership problem concrete before we added another evaluation stage.

The compiler establishes the references. Calling their arrangement awkward is our design judgment. The diagram’s group names are authored explanations; an arrow does not prove execution order or permission safety.

Explore the recorded before/after maps and source

The view starts at create_preparation. Select a definition to read its checked source, or use the map controls to explore the whole program. On a phone, scroll inside the map.

Recorded version

Before: exact source and diagram artifact · After: exact source and diagram artifact

What we changed—and checked separately

We also moved shared contribution records into ContributionModel and site/key helpers into Identity. Each workflow kept its own orchestration, transaction boundaries, and authority checks. Preparation still references completion to register its route; the refactor did not remove every connection between them.

Generated-runtime tests, access checks, and bounded protocol checks accompanied the change. A cleaner diagram alone would not establish equivalent behavior. The refactor record describes those checks and their limits; the original organization review explains the decisions.

02 / Abstraction

Make validation read in the order it happens.

The application receives untrusted JSON describing an article evaluation. Its decoder checks the expected fields, their types, and whether citations belong to the supplied evidence set. Each failed check must return its error without running the remaining checks.

The organization map drew attention to a large decoder. Reading its source showed the same error propagation nested around every field. That was a candidate for a shared composition operation—not evidence that the decoder returned wrong answers.

Before / excerpt

Repeat the error handling.

match required_basis_points(value):
  case DecodeError(path, reason): DecodeError(path, reason)
  case Decoded(score):
    match required_nonempty_string("congruence_reasoning", value):
      case DecodeError(path, reason): DecodeError(path, reason)
      case Decoded(congruence_reasoning):
        match required_event_time(value):

After / excerpt

Name each check, then continue.

score <- decode_bind(required_basis_points(value))
congruence_reasoning <- decode_bind(required_nonempty_string("congruence_reasoning", value))
event_time <- decode_bind(required_event_time(value))

decode_bind continues only after a successful decode and preserves a failure’s path and reason. Bosatsu’s <- syntax passes the rest of the function as that continuation. The role-specific checks and their order remain visible in the application.

Run the complete decoder below. Both versions accept the supplied valid response. Replace article:1 with article:other in the response’s evidence_refs, leaving the allowed evidence unchanged, and both reject the citation. Malformed JSON also fails. The response is a hand-written test input; no model or provider call occurs. These are concrete regression cases; accepting a response’s structure does not establish that its prose is true.

Code & run Compare, edit, and execute both complete decoders

Before request and full decoder source · After request and full decoder source · Recorded inputs and outputs · Replay engine identity

The records above replay the frozen source using a newer browser engine. The diagrams remain the historical recordings. The original independent audit also compared successful values and exact errors across the decoder’s boundary cases.

Use your agent with this example

Connect your agent using the WebMCP connection guide, then keep this page open. The example tools expose the loaded source, revision-aware edits, execution results, and feedback about what is visible.

Call yichus_example_guide. Read exampleId "icetakes_decoder" with yichus_example_read.
Compare the before and after versions. Explain how error propagation changed, and what stayed application-specific.
Run the valid response, then change only its evidence_refs citation to "article:other" and rerun. Keep the allowed evidence set unchanged.
Use yichus_example_feedback to report the visible result and its limits. If you edit source, use the current revision and rerun the checks.

03 / Improving Yichus

Sometimes the finding exposed a bug in the tool.

Building Icetakes also gave us reasons to question Yichus’s answers. These were defects in our analysis and guidance, not application bugs that the checker successfully caught.

A string input was incorrectly called unused.

A suffix predicate returned different answers for barfoo and foobar, yet the analysis said its input influenced nothing. Investigation found a missing control dependency through the compiler’s mutable intermediate representation. The repaired analysis reports guard-only: the input can select a different result without supplying the returned value’s data.

A later WebMCP replay caught advice that still described guard-only inputs as independent of the output. That wording was corrected too. Analysis counterexample and repair · Browser replay and guidance correction.

An unknown callback was incorrectly treated as storage-free.

Negative probes showed that an abstract callback result could conceal IO, including deferred actions inside lists or records. The verifier had accepted some of these programs. The fix follows the checked result types and refuses a storage-absence claim when effects remain unresolved. These probes demonstrated an incorrect proof claim, not a production data leak.

The subsequent specialization work lets supported concrete pure callbacks pass while retaining the negative controls. False-safe examples and before/after verdicts · Specialization and generated-app replay.

The full Icetakes gap log distinguishes executed counterexamples, proof limitations, and integration work. It is the development record behind this case study.