Coq formalization accompanying the paper: Micro-Policies: A Framework for Verified, Hardware-Assisted Security Monitors.