[xgk]

   calling context

In compositional verification, you generally want to prove as much as possible about the piece of code at hand -- irrespective of calling context.

   spec very similar to this

Yes, I was using something similar. Note that this is right only in a purely sequential setting ...

   I recently verified a JIT compiler,

That sounds exciting. That must have been a major piece of work. Anything published yet?

With JIT compilers the issue of self-modification becomes pertinent. I know that Magnus Myreen has verified a small JIT compiler a few years back but I don't remember exactly what theorem he proves. IIRC he was using a tailor-made Hoare logic for x86 code that basically moved some of the complexity of the spec into the logic.