Type-preserving Compilation for End-to-end Verification of Security Enforcement