Use existing architecture models to prove properties of instruction set

[andrew-johnson-4]

Proofs with partial knowledge should still be model checked against actual architecture specifications:

• https://github.com/maximedenes/coq-amd64