Verified just-in-time compiler on x86

This page contains supporting material for a POPL paper:
Magnus O. Myreen.
Verified just-in-time compiler on x86 (.pdf).
POPL 2010, ACM.

The verified x86 machine code, C wrapper file and the C implementation of GCD, to which we compare the JIT compiler, are included in the following ZIP file:

verified-jit-code.zip
Note: the C wrapper file makes a few calls to the operating system and might, as a result, only work on Mac OS X 10.5. The C wrapper interfaces correctly with the operating system and the JIT compiler when built using the following version of GCC:
$ gcc --version
i686-apple-darwin9-gcc-4.0.1 (GCC) 4.0.1 (Apple Inc. build 5490)
Copyright (C) 2005 Free Software Foundation, Inc.
This is free software; see the source for copying conditions.  There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.    
The HOL4 proofs, which are currently undocumented, are compressed into the following zip-file.
jit-proofs.zip