start work on verified MIPS simulator

As mentioned in the comments in the file, our translation of words into
CakeML probably needs to be changed, although exactly how needs to be
discussed. At the moment, it makes this kind of translation cumbersome
since I have to specify the type of each use of all the polymorphic word
constants. (This could be ameliorated somewhat by more automation.)