opt:refines/2opt.plrefines+Before, +AftersemidetAfter is an outcome the original program allows, given that the original's outcome was Before, both from interp:run/5 on the same inputs: is the outcome relation that translation validationtranslation validation nanofilTranslation validation checks each transformation's result rather than proving the transformation once: nanofil's register checker, the check passes' *_refines/2, and the interpreter refinement of difftest -O (amd64_regs_check:check_regs/5, opt:refines/2, refines). A wrong pass then makes a compile fail rather than produce a wrong output, as far as the checker is right. of the middle end uses: the original's undefined behaviour allows anything, an unknown value allows any consistent one, and otherwise the outcomesoutcome nanofilAn outcome is how a run ends: a return, unreachable, undefined behaviour, a trap, unchecked, or running out of fuel. interp.pl and the model give the same outcomes term for term, which is what the outcome gate compares. must be equal. An optimized run may go on where the original ran out of memory, a runtime's choice; too_big must stay.

The Rocq model has no counterpart yet: Campaign 4 plans to restate it as trace inclusion (formal.md, Campaign 4).