Skip to content

Proof-Carrying Transformation

Transformation method — instantiates Specification-to-Execution Lowering

Emits, alongside each lowering step, a machine-checkable proof that the step preserves the source's meaning — so the result is trusted by re-checking the proof, not by trusting the translator.

Proof-Carrying Transformation lowers a specification toward execution while attaching, to each step, a formal certificate that the step is meaning-preserving. The idea generalizes proof-carrying code, where mobile code arrives bundled with a proof that it obeys the host's safety policy and the host runs a small, trusted checker rather than trusting the code's producer.[1] Here the "code" is any lowering step and the "policy" is a semantic-correspondence contract; the mechanism's defining move is that trust is relocated from the transformer to an independently re-checkable artifact. You do not have to believe the tool did the right thing, or re-audit it each release — you check the proof that ships with this particular output, and a valid proof is the guarantee.

Example

A browser sandbox accepts third-party native extensions for speed, but a malicious or buggy one could read outside its memory arena. Rather than trust each vendor or hand-audit binaries, the platform requires every submitted extension to arrive with a proof — produced by the vendor's certifying compiler — that its memory accesses stay in bounds and it never jumps outside its own code region. On submission the platform runs a proof checker a few hundred lines long: it re-derives that the attached proof really does establish the safety contract for this exact binary. A vendor shipping hand-optimized code still gets in, as long as the proof checks. One submission's proof fails to discharge a bounds obligation on an array write; the extension is rejected automatically, with the unproven obligation named exactly, before it ever runs. The platform never had to trust the vendor's toolchain — only its own small checker.

How it works

  • State the correspondence contract. Fix precisely what "preserves meaning" means for the step: a safety property, a simulation relation, an invariant the target must satisfy relative to the source.
  • Generate obligations and discharge them. Derive the proof obligations the step must satisfy and prove each — typically with a theorem prover or checker — producing a checkable certificate.
  • Ship the proof with the artifact. The certificate travels with the output; it is not a report filed somewhere else.
  • Re-check on receipt. The consumer runs a small proof checker; a valid proof is accepted, a failed obligation names exactly what could not be established.

Tuning parameters

  • Contract strength — how much the proof actually asserts, from a narrow safety property (cheap, weak) up to full functional correspondence (expensive, strong). The proof is worth only what the contract demands of it.
  • Proof automation — fully automatic (solver-discharged, limited reach) vs. interactive (covers deep properties, needs expertise). Trades coverage against human cost.
  • Trusted computing base — how small the checker and the contract are. A smaller TCB is more trustworthy but constrains what you can express; everything inside it is believed, not proven.
  • Proof granularity — per-step certificates vs. one end-to-end proof. Per-step localizes failures and survives partial edits; end-to-end is stronger but brittle to change.

When it helps, and when it misleads

Its strength is that it makes trust transferable and cheap to re-verify: you can accept output from an untrusted or fast-changing producer, because the verification cost lives in a small checker instead of a re-audit of the whole tool. Failures are precise — a named unproven obligation — and the guarantee does not decay as the transformer evolves.

Its failure modes trace back to the contract. The proof covers only what the contract states, so proving the wrong contract gives you a rigorous guarantee of the wrong thing (the archetype's "consistently encode the wrong semantics," now with a certificate attached). Everything in the trusted computing base — checker, contract, axioms — is believed, so a bug there is invisible. Deep functional contracts are costly enough that teams quietly weaken them until the proof is easy, and a weakly-stated proved property can read as more assurance than it is. The classic misuse is treating a green checkmark as total correctness rather than "this stated contract holds." The discipline is to publish the contract and the TCB alongside the proof, so a reader knows exactly what was — and wasn't — guaranteed.

How it implements the components

  • semantic_correspondence_contract — the explicit statement of what the proof must establish; the transformation's anchor and the thing every obligation is measured against.
  • proof_and_test_obligation_set — the obligations derived from that contract and discharged formally, step by step.
  • lowering_provenance_record — the certificate itself: a portable, re-checkable record of why this output is faithful, carried with it.
  • assurance_strength_profile — a machine-checked proof sits at the strong end of the assurance spectrum; the mechanism makes that level explicit and independently confirmable.

It does not sample inputs to compare behaviours empirically (reference_model_or_oracle, correspondence_criterion — that's Translation-Validation Harness), nor derive the implementation in the first place (refinement_chain, admissible_transformation_rule_set — that's Refinement-Calculus Derivation); it certifies a transformation, it does not perform or optimize one.

Notes

Proof-Carrying Transformation and Translation-Validation Harness attack the same trust problem from opposite ends. This mechanism makes the producer emit a certificate proven a priori, which the consumer re-checks without the source; the harness has an independent checker validate each output a posteriori against the source as oracle. Reach for proof-carrying when you can require producers to prove; reach for validation when the translator is a black box you cannot change.

References

[1] Proof-carrying code, introduced by Necula and Lee in the mid-1990s: mobile code is accompanied by a formal proof that it satisfies the host's safety policy, which the host validates with a small proof checker. The trust shift — from the code producer to a checkable certificate — is exactly the property this mechanism generalizes to arbitrary lowering steps. ↩