The seL4 paper, and our class discussion on 1/25, discussed the forward simulation that shows the functional correctness of seL4’s implementation relative to its spec. The CompCert paper also discusses functional correctness, in Section 2, but it does not use simulation. Describe at least two ways that Equation (1) differs from a forward simulation.

Section 4.3 gives the following relation between original registers and allocated registers: “R(r) = R'(φ(r)) for all pseudo-registers r live at point 𝓁.” Say that CompCert’s designer made a mistake in the definition of “live pseudo-registers,” so that in some cases, a pseudo-register was incorrectly considered dead at point 𝓁 (even though its value was used at some later point). What would be a consequence of this mistake?