Bobai Kato for Ota

Posted on Jul 8 • Originally published at ota.run

Pressure-testing Ota on OrchardCore: first-class dotnet restore and honest narrow .NET proof

#pressuretesting #reporeadiness #dependencyhydration #runtimeproof

Overview

OrchardCore mattered because it is a real .NET repo, not a toy starter.

Even a narrow slice of the repo carries several different truths at once:

dotnet as the real toolchain owner
restore as a real dependency-hydration lane
build and test as finite CLI surfaces, not shell glue
native and container execution both advertised by the contract
a much larger repo outside the selected slice that the contract should not pretend to own

That made OrchardCore a useful pressure repo for a simple question:

can Ota represent a serious .NET contributor path cleanly without collapsing back into raw shell
or overclaiming the whole repository?

Why this repo mattered

OrchardCore is a broad ASP.NET Core codebase with:

many projects
broader CI workflows
functional and browser-heavy test surfaces
asset and documentation paths outside the selected unit-project slice

That is exactly why the repo is useful.

A weak readiness contract would try to flatten all of that into one vague “build and test”
surface. A stronger contract narrows intentionally and says what it really owns.

The selected OrchardCore slice is honest:

restore one unit-test project
build that same project
test that same project
prove the slice on host and container paths where the contract advertises them

That is the right pressure bar for this repo.

What OrchardCore proved

1. Ota's .NET story is stronger when restore is first-class

The mature setup lane is not:

setup:
  run: dotnet restore test/OrchardCore.Abstractions.Tests/OrchardCore.Abstractions.Tests.csproj

The stronger contract shape is:

setup:
  prepare:
    kind: dependency_hydration
    medium: package_dependencies
    source:
      kind: dotnet_restore
      cwd: test/OrchardCore.Abstractions.Tests

That matters because the contract now owns:

the hydration lane itself
the fact that it is package dependency preparation
the requirement on the dotnet toolchain
the network semantics of the lane

Instead of leaving all of that implicit inside one shell string.

2. Finite .NET task bodies should stay structured

OrchardCore also proved that plain dotnet build and dotnet test lanes do not need to stay as
raw run bodies.

The stronger shape is:

build:
  command:
    exe: dotnet
    args:
      - build
      - --no-restore
    cwd: test/OrchardCore.Abstractions.Tests

and:

test:
  command:
    exe: dotnet
    args:
      - test
      - --no-restore
      - --verbosity
      - minimal
    cwd: test/OrchardCore.Abstractions.Tests

That gives Ota a better execution boundary:

executable identity is explicit
arguments are explicit
working directory is explicit
mode branches only need to vary context, not duplicate command text

That is more mature governance than copying the same shell body across native and container modes.

3. Honest narrowing is more valuable than fake full-repo coverage

OrchardCore did not force a dramatic new Ota core bug.

What it proved instead is equally useful:

Ota can already carry a real .NET repo slice cleanly when the contract is disciplined about what
it is and is not claiming.

This contract does not pretend to own:

the entire OrchardCore solution
every functional test lane
every database-backed or browser-backed path
every asset or documentation workflow

It owns one clear contributor-readiness slice and proves that slice well.

That is better than a broader but less trustworthy contract.

What changed in the contract

The important changes were not dramatic. They were governance upgrades.

Toolchain ownership is explicit:

toolchains:
  dotnet:
    version: "10.0"
    fulfillment:
      source: dotnet
      mode: run

The workflow now owns the setup boundary directly:

workflows:
  verify:
    prepare:
      task: setup
    run:
      task: verify

And verification stays aggregate-owned instead of shell-chained:

verify:
  aggregate:
    tasks:
      - build
      - test

That final shape is small, but it is honest and machine-readable.

What the matrix proves

The current green OrchardCore matrix run for this narrowed slice is #28971743168.

That run is enough to support the note because it proved the slice the contract actually claims:

ota validate
ota doctor
ota tasks --use
ota tasks --safe --use
dry-run task coverage
dry-run workflow coverage
native execution on the selected unit-project slice
container planning and execution for the same declared task surfaces
matrix coverage across Ubuntu, macOS, and Windows for the contract branch at that time

That matters more than pretending the branch should already prove every broader OrchardCore lane.

The linked pressure branch is now pinned to released Ota v1.6.23 for stable reference. This
green matrix run is the proof artifact for the narrowed slice this note describes.

Why this repo mattered for Ota

OrchardCore helped confirm that Ota's current .NET surfaces are no longer theoretical.

They are strong enough to model a real ASP.NET Core repo slice with:

first-class restore hydration
structured finite dotnet commands
workflow-owned setup
explicit host/container mode truth

without falling back to raw shell or overclaiming repo coverage.

That is the real value of this pressure repo.

It did not need to expose a dramatic bug to matter. It proved that Ota's newer .NET contract
story is mature enough to use on a serious repository, provided the contract narrows honestly.

Top comments (17)

Vinicius Pereira • Jul 8

Making restore first-class is the move, and it quietly names two inputs at once that fail differently. The command names the dependency, which packages, but the restore's flakiness usually lives in the other one, the feed it reaches at run time. Same restore, same lockfile, green on Tuesday and red on Thursday because the feed moved or went slow, not because anything in the repo changed. So the honest version of dependency_hydration declares the feed posture too, which feed, pinned to what, offline or online, not just the verb, because that is where the non-determinism actually hides.

And the narrow proof is only as honest as where its boundary lives. You scoped out the functional lanes and the db paths in the writeup, but a downstream agent reads the contract, not the blog. The honest-narrow-net holds only if the contract carries its own "here is what I did not prove" as a first-class field, so the boundary travels with the artifact. Otherwise the scope is honest today and silently over-read tomorrow. Bounded honesty is exactly right, make the bound machine-readable too.

Bobai Kato Ota • Jul 9

You are right that restore is really two truths at once: the dependency verb and the feed posture behind it. If the contract only names the verb, it still hides a big part of where nondeterminism lives.

Same with narrow proof. The scope should not only live in the writeup. If the proof is intentionally bounded, that boundary should travel with the contract and artifact in machine-readable form so it cannot be over-read later.

I’m going to add both of those to Ota.

If you had to choose, which would be more valuable first in practice: feed posture on hydration, or machine-readable proof boundaries on narrow runtime lanes?

Vinicius Pereira • Jul 9

Proof boundaries first, and the tiebreaker is failure mode. A restore that flakes because the feed moved fails loud: the lane goes red, someone reruns it, time is lost, nobody is deceived. A narrow proof without its boundary fails silent: it stays green while a downstream reader acts on a guarantee it never made. Loud failures cost minutes, silent ones cost correctness, and a proof tool's credibility survives flakiness far better than it survives one over-read proof.

It is also the smaller lift with the bigger contract change: a first-class "not proven" field on the artifact, plus the rule that consumers must read it, can ship almost immediately, while feed posture reaches into how restore executes and deserves to be done properly. So boundary first to make the claims safe, feed posture second to make the runs quiet. Glad to hear both are landing in Ota.

Bobai Kato Ota • Jul 9

That makes a lot of sense.

Proof boundaries first is the right call. A flaky restore fails loud, but a green proof that gets over-read fails silent, and that is the worst trust failure.

The “claims safe first, runs quiet second” framing is very useful. I’m going to use that ordering in Ota too.

If Ota added a first-class not_proven boundary, what would you want it to name first, so a downstream reader cannot over-read the proof: skipped lanes, unproven dependencies, unproven external state, or something else?

Vinicius Pereira • Jul 9

I'd order it by how invisible the gap is to someone reading only the top line, not by category.

Skipped lanes I'd name last, not first. A skip is already loud, it announces itself. The reader can see "we didn't run this." That's the honest kind of gap.

The dangerous one, the true silent failure, is what the green rested ON without exercising. Unproven external state first, unproven dependencies right after. A restore that passes against synthetic state and breaks against real prod state is the textbook case: the proof never touched the state that actually matters, so nothing in the green warns the reader. That is the over-read that costs you.

So my not_proven order would be:

unproven external state (what the pass assumed about the world)
unproven dependencies (what the pass assumed about its neighbors)
skipped lanes (what you chose not to run, self-declared)

One more thing: whatever not_proven names has to be non-collapsible. If the top-line PASS can swallow it, it gets over-read again. The boundary has to travel attached to the proof, not sit in a footnote the reader skips. "proven, assuming X" with X always in frame beats "proven" with an asterisk.

Bobai Kato Ota • Jul 10

Very insightful. That is the distinction Ota needs. A skipped lane is visible; the dangerous boundary is what a green proof assumed without exercising. I’m refining Ota’s proof model around that order: external state first, dependencies next, skipped lanes last, with the boundary carried in the top-level proof verdict rather than buried under a green result.

When a proof depends on a neighbouring service or dependency, what evidence would make you trust that it was actually exercised rather than merely reachable?

Vinicius Pereira • Jul 10

The evidence has to be a negative control, not more green. Reachable means the call came back. Exercised means the interaction left a fingerprint on the dependency's own state that you read back and assert on. The proof is the test that FAILS when you swap the real dependency for a stub that answers but does nothing: if a null stand-in keeps it green, you proved reachability and the boundary was decorative.

The stronger version is fault injection: break the dependency on purpose and require the proof to go red. One that stays green while its neighbour is down never rested on that neighbour. I leaned on this exact distinction this week: the tests that drive the real engine fail the moment it is swapped for the in-memory double, so a green there means the seam was actually crossed.

Bobai Kato Ota • Jul 10

That’s precisely the correction.

The important boundary is that ordinary proof can show reachable, and with the right fingerprint, it can show exercised, but only a separate control run can justify fault_tested.

So Ota should not infer counterfactuals it never executed. I’m going to carry that ladder into the proof model exactly that way.

If you had to choose one first, what has been the most trustworthy fingerprint of “exercised” in practice for you: a dependency-side state change, a call trace with asserted payload, or something else?

Vinicius Pereira • Jul 10

Dependency-side state change, without much hesitation, and the reason is the negative control again. A call trace with an asserted payload passes even against a mock that records the call and does nothing, so it certifies reachable plus a correct outgoing message, but not exercised. The payload assertion is really a contract check on my side of the seam. Useful, but a different axis.

State read-back is the one that goes red against a do-nothing double, because the assertion lives on the far side of the seam: for it to be green, the collaborator had to actually process the call and mutate. That is the whole distinction in one line, a fingerprint on my side of the seam is reachability plus contract, a fingerprint on the dependency's side is exercise.

The caveat, since it is not always available: when the dependency is a black box with no readable state, I fall back to a round-trip effect only the real one could produce, a value that comes back transformed in a way my code did not compute, or a downstream read that reflects the write. I reach for a call-trace spy last, and when I do I treat it as reachability rather than proof of exercise, because it fails two ways at once: it passes against an inert stub, and it couples the test to the call shape, so it hands you false confidence and brittleness in the same assertion.

Bobai Kato Ota • Jul 11

This is strong.

The big takeaway is that exercised should default to evidence from the dependency’s side of the seam, not the caller’s side.

So the order is:

dependency-side state change first
real round-trip effect next when state is not readable
call-trace spy last, and only as reachability plus contract, not exercise

That should sharpen Ota’s proof model too. If Ota ever models seam fingerprints, it should distinguish dependency-side from caller-side evidence explicitly.

When you have to rely on a round-trip effect instead of readable dependency state, what has made that effect trustworthy enough to count as exercised rather than just another indirect green signal?

Vinicius Pereira • Jul 11

same negative control, just aimed at the effect instead of at state. i only trust a round-trip whose output an inert double can't fake: a value that's a nontrivial function of what the real dependency computed, not a constant and not an echo of my own input. and i don't assume that property, i run the assertion against a do-nothing stub. if it stays green the effect was reachability in a costume, and it's out. what earns it the "exercised" label isn't the effect itself, it's that the stub provably fails it.

Bobai Kato Ota • Jul 13

This is the missing line.

A round-trip only counts as exercised if the inert double fails the same assertion. Otherwise it is still just reachability in a better disguise.

That sharpens Ota too: dependency-side state first, round-trip effect only with negative control, caller-side traces never promoted to exercised.

What has been the most useful artifact to keep with that negative control in practice: the substitute identity, the failed assertion, or both?

Vinicius Pereira • Jul 13

both, but really the pair on one assertion: real passes, inert fails, same input. the failed assertion is the load-bearing half, except a red alone lies. a stub can go red because it threw or returned null, plumbing not effect, and that's a red i didn't order. the substitute identity is what lets me say the inert one failed on the value not being a nontrivial function of the real compute, not on the double falling over. so the artifact i keep is the failure mode, not just the fail.

Bobai Kato Ota • Jul 13

I strongly agree. The pair belongs on one assertion: real passes, inert fails, same input, with a failure mode that proves the effect disappeared rather than the substitute simply breaking.

That distinction is useful for Ota too. We should record the substitute identity and classified failure mode, not just a red result.

How do you usually classify or enforce that expected failure mode today: a custom matcher/assertion, a test harness convention, or review discipline?

Vinicius Pereira • Jul 13

custom matcher, not review. review just eyeballs a red and moves on. it does two things: gate the control first (well-formed inert, same shape, non-throwing, effect removed, else the run is inconclusive not scored, the red i didn't order), then assert on the reason, that the inert collapsed to baseline instead of tracking the real compute. three verdicts, not pass/fail: proved, inconclusive, unproven. an unclassified red never counts as proved.

Bobai Kato Ota • Jul 14

That distinction is important: a red control is not automatically proof.

The useful model is proved, inconclusive, and unproven, with the inert substitute validated before the result is scored. Same shape, non-throwing, effect removed, then assert that it collapsed to the expected baseline.

That gives Ota a cleaner rule too: a negative control only upgrades evidence when the substitute identity, validity check, and classified failure mode are all recorded. An unclassified red should never count as proof. Thank you.

Vinicius Pereira • Jul 14

that's the rule. and the reason to record all three, identity, validity, failure mode, is that it makes the upgrade re-checkable by someone who never ran it. otherwise "the control validated" is just one more thing to take on trust, which is the failure mode this was trying to close. good thread.