An ASM to x86-64 encoder and correctness proof.

The proof could benefit from some extra work, as it currently takes about 1.5hrs to complete. It relies upon HOL4 commit 4f16bf9.