← yich.us

Verified Mutation Flows

A family of API mutations shares one flow: try, read, retry, or fail. The usual fix is a factory full of lambdas nobody can read, or plain copies kept in sync by review convention, which nothing checks. Here, every mutation stays plain code and a checker proves each one follows the flow.

The code is Bosatsu, a small pure language whose IO effects are values a checker can inspect, and that is what makes this verifiable. 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.

1Write the flow once

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.)

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

2Write each mutation as plain code

No factory call, 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.)

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)

3Declare 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.

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

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

4Verify: the parts come free

yichus flow report demos/flow/*.bosatsu

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:

Dig deeper: what the match actually is

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
)

5Break it: get a located fact

Wire the error from the wrong value:

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

Exit code 1. Gate it in CI and the build enforces conformance instead of leaving it to review convention.

6A batch is a program

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.

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

7Verify the extraction itself

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.

8Flows can recurse

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.

Benchmark: a blind conformance census

Does any of this beat reading the code by hand? One measurement round put the feature under test. An AI generated a 2,811-line library-circulation API this checker had never seen: two flow families, 14 declared mutations (5 of them deliberately nonconforming), plus 3 undeclared look-alike mutations, with a hidden answer key. Two fresh AI reviewers were asked for a full census of the family (which mutations conform, with what parts; which diverge, where; is a given batch 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

Honest summary: 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. The cost crossover belongs to larger codebases: see the 46,922-line round, and this round's full record, on the measurement scoreboard (round 010).

Limitations

• 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.

Run it yourself

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> …

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