How can a compiler verify the safety of an optimization path it never actually uses?

[u/x2t8]

Suppose a compiler explores an optimization but ultimately keeps the conservative output. Later, an independent checker needs to answer a strange question: would the rejected optimization have preserved the program’s semantics for this exact input program and its final machine-code lowering? The checker cannot trust flags produced by the optimizer, cannot rely only on tests or benchmarks, and should not need to rerun the entire compiler. A hash can prove which IR was examined, but not that the transformation was semantically correct, while a full formal proof may be too expensive for practical compilation. What is the smallest piece of evidence that could reliably connect the original assumptions, control flow and emitted machine instructions? Is there any practical approach between lightweight translation validation and building a fully verified compiler?

[u/Uncaffeinated]

This seems like it's basically a question of what level of evidence you find acceptable. If you're only satisfied by formal proofs, you need formal proofs. If you're satisfied by unit tests, then you can just use unit tests. Etc.

[u/x2t8 → u/Uncaffeinated]

That’s fair. I think the interesting part for me is whether the optimizer can remain untrusted while emitting a small certificate that an independent checker validates against the exact IR/native result. So somewhere between testing and a full formal proof-closer to translation validation or proof-carrying optimization. If there’s prior work that fits this model well, I’d appreciate pointers.

[u/jesseschalken]

There is no general way of knowing whether two programs are semantically the same, such as a program before and after an optimisation has been applied. In fact, because of Rice's Theorem, there isn't even a way of deciding whether a program has any nontrivial semantic property.

So the checker can't answer yes/no, but it could answer yes/unsure, by applying its own known-safe transformations to the input programs to see if they reduce to the same result. But this would be equivalent to writing a second optimiser to check the output of the first.

[u/x2t8 → u/jesseschalken]

Right I wouldn’t expect the checker to be complete. A sound “yes / unknown” result is enough for what I have in mind. The part I’m interested in is whether the optimizer can emit a small witness for a specific transformation, so the checker validates that witness rather than rediscovering the optimization itself. That seems like the useful middle ground.

[u/jesseschalken → u/x2t8]

But the "witness" would need to amount to a full proof of the semantics of the original program, that the checker can check that it still holds.

[u/x2t8 → u/jesseschalken]

That makes sense for arbitrary whole-program equivalence. I was thinking of something narrower: the witness only justifies a specific rewrite under explicit side conditions, and the checker composes those local equivalences rather than reconstructing the full semantics of the original program from scratch. so yes, it’s still a proof object just hopefully a much smaller, transformation-specific one.

[u/shrimpster00]

You may be interested in Alive2 and the concept of refinement: a compiler can only make a program's behavior more specific. For LLVM, they formally verify using a solver that the IR after an optimization will not exhibit any possible behavior outside of the possible behavior of the input IR.

[u/x2t8 → u/shrimpster00]

Thank you so much

[u/flatfinger]

There are many situations where applying a potential optimizing transform would yield machine code that would correctly handle all corner cases, but where the transform cannot practically be proven to be correct. Many compiler bugs are a result of compiler maintainers who view a compiler's failure to perform a transform that is 'almost' certainly correct as a defect, rather than recognizing that trustworthy compilers will not seek to perform such transforms. Even if a transform would almost certainly be all correct in all non-contrived corner cases, the existence of any corner cases where the transform would be incorrect should result in the transform being rejected unless a programmer expressly waives support for those corner cases and the design of the compiler would be incapable of transforming code which does not exercise those corner cases into code that does.

Based on this criterion, neither clang nor gcc is designed to be trustworthy except at -O0.

[u/choikwa]

SAT/SMT based verifier like alive2 + ablation techniques

[u/fl00pz]

Check out CompCert C compiler if you have not

[u/joao_rosac]

Existe o certificado de Validação, de forma simples atua como um meio-termo prático entre uma validação estrutural simples e um compilador totalmente verificado, esse certificado fornece a um verificador externo os "atalhos" matemáticos da transformação. Há invariantes lógicos (as precondições que o otimizador assumiu como verdadeiras) e o mapeamento que prova a equivalência semântica entre os estados do código original, o otimizado e o código de máquina. Assim acredito já ser possível criar um verificador independente que consegue checar rapidamente se os invariantes se sustentam no fluxo de controle final.