Translation-Validation Harness¶

Verification harness — instantiates Specification-to-Execution Lowering

Instead of proving a translator correct once, it checks each individual translation after the fact — establishing that this output faithfully realizes this input against the source as oracle.

Verifying a translator — a compiler, an optimizer, a code generator — once and for all is often infeasible: the tool is large, changes constantly, or is closed. A Translation-Validation Harness sidesteps that by shifting the burden from the translator to each translation: it treats the tool as an untrusted black box and, after every run, checks that this particular output correctly realizes this particular input.^[1] Its defining move is that the source itself serves as the oracle — the harness constructs a correspondence check between input and output and discharges it, so a passing run yields evidence for that run and a failing run pinpoints the divergence. Nothing is proven about the translator in general; everything is established about the artifact in hand, which is exactly what you need when the translator is too complex or too mutable to verify directly.

Example¶

A team runs an aggressive optimizing compiler on safety-relevant control code. Verifying the compiler itself is out of reach — it is third-party and updated quarterly — so they wrap it in a translation-validation harness. After each build the harness takes the source intermediate form and the optimized output and constructs a simulation relation: a mapping asserting that every observable behaviour of the optimized code corresponds to a behaviour the source allows. It feeds the resulting verification conditions to an SMT solver. On one build, an optimization that reorders memory operations produces a condition the solver cannot discharge — the harness flags the exact instruction pair and the mismatch, and the build fails before the binary ships. The compiler was never certified; this compilation was, and it is the compilations that fly. The check is keyed to the exact source and compiler versions, so a re-run after either changes is a fresh validation rather than a stale pass carried forward.

How it works¶

Take source and output as a pair. The input specification or model, and the translator's product for it, per run.
Build a correspondence check. Construct the relation that must hold for the output to realize the source — a simulation, an equivalence, a refinement — as verification conditions.
Discharge against the oracle. Use the source as reference and a solver or checker to establish the conditions; a pass is per-run evidence, a failure localizes the divergence.
Bind to versions. Record which source and translator versions this validation covers, so it is re-run when either one moves.

Tuning parameters¶

Correspondence relation — strict equivalence vs. simulation vs. observational refinement. A stricter relation catches more but rejects benign, intended differences (an optimization that changes timing but not results).
Check completeness — fully prove the conditions vs. bounded or sampled checking. Full discharge is strongest; bounded checking is cheaper and always within reach but leaves a residue of unchecked behaviour.
Oracle fidelity — how completely the source model captures intended behaviour. A partial oracle validates only what it specifies; behaviour outside it passes unexamined.
Failure handling — block the build vs. warn-and-log on an undischarged condition. Blocking is safe but can stall on solver limits; warning keeps flow but demotes the guarantee.

When it helps, and when it misleads¶

Its strength is that it delivers per-artifact assurance for translators too big or too closed to verify, survives translator upgrades (each new version is simply re-validated), and localizes failures to a specific divergence rather than a vague "miscompile." It is the pragmatic route to trust when an a-priori proof of the tool is not available.

Its failure modes trace to the oracle. It validates against the source model, so it inherits that model's blind spots — behaviour the source does not pin down passes unchecked, and a passing validation is only as complete as the correspondence relation demands. Solver limits mean hard conditions may be quietly downgraded to warnings, and a green run can be mistaken for total correctness rather than "this relation held for this pair." The classic misuse is loosening the correspondence relation until validations pass — converting a real check into a rubber stamp. The discipline is to fix the relation and the oracle up front and treat an undischarged condition as a failure to investigate, not a threshold to relax.

How it implements the components¶

reference_model_or_oracle — the source specification or model serves as the oracle every output is checked against; the harness needs no independently-written expected answer.
correspondence_criterion — its signature: the explicit relation (equivalence, simulation, refinement) defining when an output faithfully realizes its input, which the check discharges.
versioned_change_record — each validation is bound to the exact source and translator versions it covers, so a change to either re-opens it rather than silently inheriting an old pass.

It does not have the producer ship a proof re-checkable without the source (lowering_provenance_record, assurance_strength_profile — that's Proof-Carrying Transformation), nor perform the translation itself (intermediate_representation_ladder — that's Query-Plan Lowering and Optimization); it is the independent checker sitting after the translator, not the translator.

Instantiates: Specification-to-Execution Lowering — it certifies the fidelity of the level shift one run at a time.
Consumes: an SMT solver or Model Checker and Static Analyzer to discharge the correspondence conditions.
Sibling mechanisms: Proof-Carrying Transformation · Differential Equivalence Test · Contract Test Suite · Regression Test Suite · Model-Driven Code Generation

Notes¶

Three siblings guard translation fidelity by different means. This harness proves a correspondence for each run; a Differential Equivalence Test samples inputs and compares outputs, catching divergences it happens to hit but proving nothing in general; Proof-Carrying Transformation moves the proof to the producer. Reach for validation when the translator is a black box you cannot change but the source is a usable oracle.

References¶

[1] Translation validation (introduced by Pnueli, Siegel, and Singerman in the late 1990s) verifies each run of a translator rather than the translator itself, by constructing and discharging a correspondence between source and target for that specific input. It is the practical alternative to verifying an optimizing compiler end-to-end, and real verified-compiler efforts have used it for exactly the passes that resist direct proof. ↩