Oracle synthesis

Oracle work happens in three stages, and only the last one may say what happened. Synthesis decides what instrument to build. A gate admits or refuses the result. A runner executes it over hashed evidence and emits an outcome.

Synthesis holds no capability that acts on the world. It cannot call your application, drive the harness, or materialize a fixture. Calling the endpoint from inside synthesis to save a round trip would move acting code into the persuadable domain — a violation of the split, not a shortcut.

An outcome is one of four: satisfied, refuted, inconclusive, or blocked. The first two must carry measurements. An assertion that reports a conclusion without a measurement is unfalsifiable by inspection, and Certus does not accept one.

Synthesis starts at the bottom and stops at the first rung that can establish the claim. It records both where it stopped and a machine-checked reason for every rung it passed over.

recipe

Instantiate a pre-validated recipe from the registry. No model is involved; the service simply looks it up.

primitives

Compose trusted, catalogued measurement primitives into a measurement graph. Still no model — a solver does it.

expression

A declarative assertion over the graph's outputs: total, no input or output, statically costed. Written by a model, compiled by the service.

wasm checker

A checker compiled to WebAssembly and executed in a constrained tier.

native checker

A bespoke program, as a signed bundle, in the most constrained tier of all.

experiment

Refuse. Emit a bounded request for the evidence that would make an honest measurement possible.

Skipping the bottom two rungs is structurally impossible rather than forbidden: the service searches them before a model is invoked at all. If a recipe or a composition of primitives can discharge the obligation, no model ever sees the question. From the third rung up, the invocation names a floor the model cannot raise, and there is no parameter that means “start higher”.

This is the thing to get right. A recipe-level oracle and a native-checker oracle measuring the same observable get the same grade.

A bespoke program that decodes the same image, compares the same rectangle and asserts the same predicate has exactly the same interpretive distance to the claim as a catalogued primitive doing the same work. What differs is how many people can read it and how many ways it can be wrong as code — a different axis entirely.

Making the rung an input to the grade would have two bad effects. It would make a grade a fact about Certus's catalog rather than about your run, so shipping a new primitive would raise the grade of a claim nobody touched. And it would make the rung worth lying about.

Every step up carries one reason, and the service checks the reason itself rather than believing it.

no matching recipe

The registry lookup found nothing — and the service ran the query.

unexpressible in primitives

The solver could not express the named measurement, and the service ran the solver.

unexpressible in expression language

The compiler rejected the predicate. The service recompiles it: if it compiles within the cost ceiling, the escalation is refused and the simpler oracle is used.

no toolchain for the language

Checked against a static toolchain table.

requires a native extension

The frozen dependency lock must actually contain such a package.

insufficient evidence

The observable must genuinely be absent from the evidence manifest.

Each rung has its own budget, and budgets do not transfer. Running out stops synthesis at the rung it was on; it never buys a climb.

At the top of the ladder, synthesis emits nothing. It refuses, and says what evidence would let it measure honestly.

That refusal is not a failure of your change and it is not a fifth kind of outcome. The obligation ends INCONCLUSIVE with a named reason, and it is rendered in the voice of the debt register rather than the voice of an error:

“Could not prove: the image returned by the crop operation is exactly the source region the user selected. Evidence available: output dimensions only. What would prove it: a coordinate-grid source image, the coordinates actually selected, and the resulting image. This is not a failure of the change. It is a gap in the proof.”

A refusal names the gap precisely: the observable is absent; the artifact exists but lacks the shape needed; the wrong thing was captured; the comparison has no comparand; the fixture has no diagnostic property. That list is the actionable part — it is what your harness needs to be able to capture.

Certus makes the request to itself, and the planner may satisfy or decline it. The whole loop is bounded: three synthesis attempts, so at most two experiments, non-transferable between obligations and between runs. Each round is a full boot of both twins against your claim's budget, so the bound is your protection, not a limitation.

A synthesized program is hashed, and the hash covers the source that is published alongside the measurements in the verdict. Every declared input must be referenced in the source, measurements are mandatory and non-empty, and the challenger recomputes the result independently.

Execution is hermetic by construction rather than by policy. There is no network interface at all — not a deny rule, no interface. Evidence is materialized read-only by hash before the process starts, and a single result file is read by a supervisor after it exits. The clock is frozen, the hash seed is fixed, the environment is a short fixed list and reading outside it raises, and there are hard ceilings on time, memory and decoded bytes.

The runner is Certus's own trusted code, and it is caged anyway, because it is the one trusted component whose inputs are adversarial bytes chosen by the party under examination. Every defect class that matters lives in decoders — images, video, JSON, schema validators, regular expressions — which are exactly the libraries useful assertions need.

Determinism is measured, not asserted: every bespoke program runs twice within the run, catalogued oracles are sampled, and the challenger's recomputation is a third execution. When two executions disagree, the obligation is INCONCLUSIVE naming both digests — never a coin flip, never a majority vote, never first-result-wins. A disagreeing oracle has not measured anything. Hitting a resource ceiling is the same: a program that timed out measured nothing, and calling that a failure would be an assertion Certus did not earn.

A refusal you cannot act on

Read “what would prove it”. If your harness cannot capture those observations at the current frontier, the obligation stays as debt and is eligible to reopen with a richer fixture or a wider frontier.

A request declined as outside the frontier

The experiment needed something the verification scope does not include. That is a scope decision, not a defect. Widening the frontier is the fix.

A request declined for budget

The estimated twin experiment exceeded what remains of the claim's budget. Raise the claim budget if the proof is worth it.

Determinism divergence

Not retryable. Something in the measurement is not a function of the evidence — usually a clock, a hash order, or a decoder that is not stable.

The obligation is inconclusive because of an escalation limit

Your policy forbids model-written code above a rung. That is deliberately inconclusive rather than a lower grade: a capped grade would say the evidence was weak, where the truth is that no admissible instrument was produced.