Compiler Verification in LF