Verified Mutation Flows

Several mutations can share a rule: read, try an update, retry on conflict, or fail. Declare that flow once, then check whether each mutation follows it. The checker reports where a mutation’s structure diverges from the declared family.

Code & run Run the stock mutation

The code is Bosatsu, a small pure language whose IO effects are values a checker can inspect. The checker is yichus, a static-analysis toolkit for Bosatsu; this page's examples live in its repository under demos/flow, and every output below is a real run against those files.

Prerequisites before running a command: clone the Yichus repository, install a JDK 17+ and sbt, run from the repository root, and build the CLI with sbt assembly. The commands below resolve their demos/flow paths from that root.

The source blocks are focused excerpts, while generated-output blocks show what the tools emitted. Use the linked demos/flow directory for the complete files that compile together; do not assemble a program by concatenating the excerpts.

1 Write the flow once

The flow is an ordinary function. Its function-typed parameters are the holes where the per-mutation steps go. Nobody ever calls it. (Outcome is the family's result type: a mutation ends Accepted into a commit, or exhausts its retry and wraps a user error.) The complete factory is in stock.bosatsu.

def retry_flow(
  observe: i -> IO[Int],
  propose: (i, Int) -> Int,
  reconcile: (i, Int) -> Int,
  explain: (i, Int) -> Int
) -> i -> IO[Outcome]:
  def run(input: i) -> IO[Outcome]:
    (
      current <- observe(input).flat_map()
      match apply_change(
          current, propose(input, current)):
        case Accepted(next): commit(next)
        case Rejected(_):
          match apply_change(
              current, reconcile(input, current)):
            case Accepted(next2): commit(next2)
            case Rejected(deficit):
              pure(wrap_error(
                explain(input, deficit)))
    )
  run

2 Write each mutation as plain code

The mutation makes no factory call and takes no lambdas. It reads like what it does. (Reading the do-block: x <- e.flat_map() means “run e, bind its result to x”; pure lifts a plain value back into IO.) The complete mutations and helpers are in stock.bosatsu.

def restock(order: Order) -> IO[Outcome]:
  (
    current <- observe_stock(order).flat_map()
    match apply_change(
        current, restock_delta(order, current)):
      case Accepted(next): commit(next)
      case Rejected(_):
        match apply_change(
            current,
            restock_reconcile(order, current)):
          case Accepted(next2): commit(next2)
          case Rejected(deficit):
            pure(wrap_error(
              restock_explain(order, deficit)))
  )

Its parts are ordinary named helpers (this one tops the level up to 200 on a rejection):

def restock_reconcile(o: Order, current: Int) -> Int:
  _ = o
  sub(200, current)

3 Declare the family

One typed declaration (FlowSpec1..6, one per factory arity) names the flow, hands the checker the factory function itself, a failure predicate, and the mutations that claim to follow it. Because the factory is a typed field, a typo, wrong arity, or wrong hole type is a compile error. The complete declaration is in stock.flow.bosatsu.

stock_flow = FlowSpec4(
  "retry-stock",
  retry_flow,
  is_error,
  [restock, consume, withdraw]
)

In order, the fields are the name reports use, the factory, the failure predicate (is_error is how a batch will decide a member failed), and the declared family.

4 Verify structural conformance and extract named parts

yichus flow report demos/flow/*.bosatsu

The exact report and parts commands use the complete stock source and declaration files.

Every declared mutation is matched against the factory's whole body. The check is a static walk of both sides' compiled IR in lockstep, not a type check or a text comparison. Local names are matched by position, never by spelling, so you can rename every variable in a mutation and it still conforms. The one thing matched by name is a reference to a top-level binding, where a shared helper must be the same binding and not a look-alike. Conforming mutations yield their parts, which are lambdas nobody wrote:

Structural matching: Matchless lockstep and verified extraction points

Both sides compile to Bosatsu's post-typecheck IR (called Matchless), and the checker walks the two trees constructor-for-constructor. Function parameters, let bindings, do-block binders, match binders, and even a recursive inner function's own name are paired by position into a renaming map; a bare variable matches if the map says its counterpart is the one in the other tree. Compiler-introduced temporaries and the mutable slots that loops compile to are paired the same way, by correspondence maps rather than by their numbering.

Where the factory applies a hole to flow variables, the mutation must apply a named top-level helper to the correspondingly-wired variables. That application is the extraction point, and it is why parts are always real bindings with verified argument wiring rather than guessed lambdas. "Safe inlining" means exactly one normalization is allowed before matching: a named, pure, single-use intermediate may be inlined (capture-aware, and never a function value), so naming a subexpression does not break conformance.

Conformance claims that the mutation is a structural instance of the factory body with these parts, so the shape, the shared helpers, and the wiring all line up. It does not by itself claim runtime equivalence with retry_flow(parts…); that is what step 7's seeded oracle tests from the outside.

Hole	Part	Receives
observe	observe_stock	input
propose	restock_delta	input, current
reconcile	restock_reconcile	input, current
explain	restock_explain	input, deficit

And yichus flow parts --out parts.bosatsu demos/flow/*.bosatsu writes the extraction back as code, then compiles it, so the compiler itself re-checks every hole's type (actual output):

# retry-stock: verified parts of Demo/Stock/restock
restock_parts = (
  observe_stock,
  restock_delta,
  restock_reconcile,
  restock_explain
)

restock_composed = retry_flow(
  observe_stock,
  restock_delta,
  restock_reconcile,
  restock_explain
)

5 Locate incorrect argument wiring as a flow divergence

Wire the error from the wrong value:

case Rejected(deficit):
  _ = deficit
  pure(wrap_error(
    withdraw_explain(order, current)))

The checker exits with code 1. Gate it in CI and the build enforces conformance instead of leaving it to review convention. In this repository, the CI workflow runs sbt test, including FlowCommandTest, which checks both the accepted fixture and a divergent fixture. In another workflow, add the exact yichus flow report demos/flow/*.bosatsu invocation from step 4 after assembly; its exit code 1 stops the job on divergence.

6 Replay a typed all-or-nothing mutation batch

The demo's mutations all act on one state cell, a stock level declared to start at 100. A batch is a list of operations to apply in order, all-or-nothing. It is written as an ordinary binding rather than JSON, with FlowOp pairing a declared mutation to a compiler-checked input. Misspell a mutation, or hand it the wrong field or the wrong type, and you get a compile error. The complete operation list is in stock.batch.bosatsu; the exact batch command names every required source file.

restock_then_consume = [
  FlowOp(restock, Order(50, 1)),
  FlowOp(consume, Order(30, 2))
]

yichus flow batch \
  --ops Demo/StockBatch/restock_then_consume \
  demos/flow/*.bosatsu

7 Compare extracted composition with each mutation on seeded inputs

yichus flow equivalence --seed 42 \
  demos/flow/*.bosatsu

It is refutable: swap two type-compatible parts and it reports refuted with the witness input and both results. That test is in the suite. Run it over the complete stock files with the exact equivalence command.

8 Verify structurally recursive retry flows

A retry that loops is recursion. recur is Bosatsu's structural-recursion form: each call must consume a smaller piece of its argument (here, one Attempts layer of the budget), so the loop provably terminates. It is written once as a factory, like any other flow:

def retry_loop(
  observe: j -> IO[Int],
  step: (j, Int) -> Int,
  explain: (j, Int) -> Int
) -> j -> IO[Outcome]:
  def run(job: j) -> IO[Outcome]:
    def attempt(budget: Budget) -> IO[Outcome]:
      recur budget:
        case Exhausted:
          (
            current <- observe(job).flat_map()
            pure(give_up(explain(job, current)))
          )
        case Attempts(rest):
          (
            current <- observe(job).flat_map()
            match apply_step(
                current, step(job, current)):
              case Applied(next): finish(next)
              case Stuck(_): attempt(rest)
          )
    attempt(Attempts(Attempts(Exhausted)))
  run

Each mutation repeats the same recursion in plain code, and verification sees through the compiled loop machinery: the mutable slots the compiler introduces for the loop are matched by correspondence, never by number. The complete recursive source, family declaration, and exact report command belong together.

Benchmark: a blind conformance census

This benchmark compares a fact-only conformance census with a source-only census. An AI generated a 2,811-line library-circulation API this checker had never seen. That API declares two flow families and 14 mutations, 5 of which are deliberately nonconforming, and it carries 3 more undeclared look-alike mutations. A hidden answer key records the truth about each one. Two fresh AI reviewers were asked for a full census of the family. A census names which mutations conform and with what parts, which diverge and where, and whether a given batch is admissible. One reviewer could use only the yichus flow facts; the other could only read the source. Neither saw the key.

	Facts only	Source only
Nonconforming found (of 5)	5 / 5, located	5 / 5, located
Parts manifests (9 conforming)	9 / 9 complete	9 / 9 complete
Look-alikes (3 undeclared)	flagged, "not provable"	flagged
False accusations	0	0
Evidence standing	14 machine-verified claims	textual argument
Batch admission question	answered, by replay	argued, partial credit
Source lines read	0	2,819 of 2,811 (re-reads)
Cost (tokens)	143.7k	77.4k

The honest summary is that both reviewers found everything, and at 2,811 lines the reader was 1.9× cheaper, so the round failed its cost gate (a round only passes if the facts match reading's accuracy at lower cost). What the facts bought here was standing rather than price. Every answer shipped as a claim a verifier re-checked mechanically, and the batch question was answered by replaying the batch, which the reader could only argue about. This round does not locate a cost crossover. For a different program and review task, see the 46,922-line round, and this round's full record, on the measurement scoreboard (round 010).

Conformance matching and seeded-equivalence limits

• Matching is modulo renaming and safe inlining of named intermediates. It does not cover arbitrary refactoring equivalence.
• Parts must be named top-level helpers; an inline part is a divergence fact (that is what makes extraction sound).
• Divergence locations are the binding's source region plus a structural path (the breadcrumb in the fact, e.g. “at hole 'explain'”), not sub-expression line numbers yet.
• The equivalence oracle samples; it never claims proof.

Build the CLI and run each flow checker path

git clone https://github.com/snoble/yichus
cd yichus
sbt assembly
java -jar target/scala-*/yichus.jar flow report \
  demos/flow/stock.bosatsu \
  demos/flow/stock.flow.bosatsu

Requires a JVM (17+) and sbt; sbt assembly writes yichus.jar under target/. Every command on this page works the same way: java -jar …/yichus.jar flow <subcommand> …

The stock family uses three exact source paths for report, parts, typed-batch, and equivalence checks. The recursive family has its own factory and declaration paths:

java -jar target/scala-*/yichus.jar flow report demos/flow/stock.bosatsu demos/flow/stock.flow.bosatsu
java -jar target/scala-*/yichus.jar flow parts --out parts.bosatsu demos/flow/stock.bosatsu demos/flow/stock.flow.bosatsu
java -jar target/scala-*/yichus.jar flow batch --ops Demo/StockBatch/restock_then_consume demos/flow/stock.bosatsu demos/flow/stock.flow.bosatsu demos/flow/stock.batch.bosatsu
java -jar target/scala-*/yichus.jar flow equivalence --seed 42 demos/flow/stock.bosatsu demos/flow/stock.flow.bosatsu
java -jar target/scala-*/yichus.jar flow report demos/flow/loop.bosatsu demos/flow/loop.flow.bosatsu

Troubleshooting by outcome

A compile error points to a source location; correct it in the complete file and rerun the same command. A missing file or jar means the command is not running from the repository root or sbt assembly has not produced the jar. Checker exit code 1 is a conformance failure, so use its located divergence. A rejected batch names the failing operation and keeps the initial state. A refuted equivalence result includes the witness input and both results; compare their extracted parts before rerunning with the same seed.

Demo source: demos/flow · Fact-based review: fact tooling · Measured results: tooling evals