#
c3900139 |
|
21-Apr-2018 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
x64 crefine: prove several lemmas in Retype_C To prove that retyping a TCB establishes the state relation for TCBs, it is necessary to prove that the C FPU null state is always equal to the Haskell FPU null state. This commit therefore includes some machinery for maintaining the state relation for the FPU null state, and repairs many proofs.
|