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.

x64: add new modifies prover

Modifies proofs now include a preprocessing step which breaks programs
into parts before passing goals to the VCG. This means there are more
calls to the VCG, but the VCG only sees individual Basic and Spec
commands, and procedure calls.

This avoids performance issues in some pathological cases. In
particular, long sequences of updates to arrays via pointer-to-struct
previously seemed to be exponential in the number of updates.