Skip to content

Translation Validation Checker

Verification tool — instantiates Generate-and-Verify Separation

Checks that one output of an untrusted transformer is semantically equivalent to its input for that specific translation, instead of proving the whole transformer correct.

A compiler, optimizer, or model-to-model converter is large, fast-changing, and hard to prove correct once and for all. Translation Validation Checker sidesteps that by verifying per translation: each time the transformer turns input A into output A′, a separate checker establishes that A′ preserves A's meaning for this instance, emitting either a validity verdict or a concrete counterexample where the two diverge. Its distinguishing move, versus proving the transformer itself, is that it trusts nothing about how A′ was produced and re-earns confidence every run — a buggy optimizer is caught on the exact program it miscompiles, even if it is correct on everything else.

Example

A safety-critical team compiles control software and cannot ship a binary the optimizer may have silently broken. Instead of trusting the optimizer or turning optimization off, they run a translation validator after each build: for every function it takes the pre- and post-optimization intermediate representations and checks — often by encoding both as formulas and asking a solver whether any input makes them differ — that they compute the same result. When the optimizer is correct, the validator certifies the pair and records which compiler version and pass produced it. When a peephole optimization is subtly wrong, the validator returns an input on which the two versions disagree, and that counterexample goes straight to the compiler team. Tools such as Alive2 apply exactly this idea to LLVM optimizations.

How it works

  • Validate the instance, not the tool. Each run checks one (A, A′) pair for semantic equivalence; nothing is assumed about the transformer's general correctness.
  • Bind output to input. The check is meaningful only because A′ is tied to the specific A it was derived from; the pair is the unit of evidence.
  • Prefer a conservative verdict. When equivalence cannot be established, return "not validated" rather than a false pass — soundness over completeness.
  • Emit a counterexample on failure. Inequivalence yields a concrete distinguishing input, turning "something's wrong" into a reproducible bug report.

Tuning parameters

  • Equivalence relation — exact behavioral identity vs. equivalence up to floating-point tolerance, undefined behavior, or observable effects. Looser relations validate more real translations but can wave through differences that matter.
  • Proof-obligation granularity — per-instruction, per-function, or whole-program. Finer units localize failures and scale better; coarser ones catch cross-boundary effects.
  • Decision-procedure budget — how long the underlying solver may search before giving up. More budget validates harder translations but slows the build and risks timeouts read as failures.
  • Provenance detail — how much of the compiler version, flags, and pass sequence is recorded with each verdict. Richer provenance makes regressions traceable at some logging cost.

When it helps, and when it misleads

Its strength is high-assurance transformation without the enormous cost of a once-and-for-all verified transformer, and it keeps working as the transformer evolves — you re-validate each build instead of re-proving the tool.[1] The counterexample output makes failures actionable rather than merely alarming.

Its failure modes turn on overreading a narrow guarantee. It certifies this translation, not the transformer, so a clean run is no promise about the next build or the next input — per-run soundness is easily mistaken for tool correctness. The check is also incomplete: for hard equivalences the validator may return "unknown," which a rushed team treats as a pass. And it inherits the fidelity of its equivalence model — if that model ignores an effect that matters (overflow, observable timing), a truly divergent translation can validate. The classic misuse is running the validator once, seeing green, and declaring the compiler trusted. The discipline is to run it on every build, keep the equivalence relation honest about effects that matter, and treat "unknown" as unvalidated.

How it implements the components

  • candidate_evidence_binding — the verdict binds output A′ to the specific input A it came from; the (A, A′) pair is the evidence unit and cannot be swapped.
  • coverage_and_completeness_boundary — it is explicitly incomplete: it draws a conservative "validated / not validated" line and refuses to false-pass hard cases.
  • failure_and_counterexample_route — on inequivalence it produces a concrete distinguishing input, routed back to the transformer's authors.
  • versioned_verification_provenance — each verdict records the transformer version, flags, and pass that produced the validated pair, so a later regression is traceable.

It does not concentrate trust in a fixed logical kernel (trusted_verifier_kernel) — that is Proof-Assistant Kernel Check — nor enforce a policy on a running candidate (checkable_acceptance_predicate at runtime), the way Sandboxed Candidate Execution does.

Notes

It differs from a differential checker: translation validation aims to prove equivalence symbolically, over all inputs for the pair at hand, whereas differential testing compares outputs on sampled inputs against a reference. The validator's "unknown" verdict is the price of that stronger claim — when it cannot prove equivalence it declines rather than guessing.

References

[1] Translation validation (Pnueli, Siegel & Singerman, 1998): rather than verify a compiler once, check after each compilation that the target program refines the source. It yields per-run soundness — a guarantee about the translation performed, not about the compiler in general. ↩