Translation 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/5amd64_regs_check.plcheck_regs+Metadata, +Map, +Before, +After, +AnalysissemidetAs check_regs/4, with the effects, CFG and home liveness of Before's implementation body already computed by body_analysis/3 (the driver computes it once and shares it with the allocator). The analysis must be of that very body and cover every mapped home; liveness bits are independent per home, so extra homes change nothing., 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:, refinesrefines nanofilopt:refines/2 is the outcome relation that translation validation of the middle end uses: the original's undefined behaviour allows anything, an unknown value allows any consistent one, and otherwise the outcomes must be equal. An optimized run may go on where the original ran out of memory, a runtime's choice; too_big must stay.). A wrong pass then makes a compile fail rather than produce a wrong output, as far as the checker is right.

The validatorvalidator nanofilThe validator decides whether a module is well formed and, in checked IR, whether every access is covered by evidence that still holds. Every producer of checked IR must get its output past it, and Soundness.v proves that a module it accepts never runs to unchecked. plays the same part for check passes: every producer of checked IR must get past it, and soundnesssoundness of checking nanofilSoundness of checking is the validator's theorem: every run of every valid checked module avoids unchecked, so the checks the validator demands, and those it lets a pass remove or reuse, are enough, and a check that fails is the run's whole story. It does not say a check never fails: a module that reads past an array is valid and traps. makes that checker proved. At formal.md's horizon, filcc's own output would be validated the same way.