Rollup merge of #128851 - compiler-errors:validate-mir-opt-mir, r=matthiaskrgr

Add comment that bors did not see pushed before it merged

In #128612, bors merged 470ada2de0ec507191ad8da35b0712986646d01c instead of 1e07c19.

This means it dropped a useful comment I added, and a stage rename that is more descriptive.