This directory contains proofs for the ASL-derived ARMv8-specific part of the compiler backend.
arm8_asl_configProofScript.sml: For ASL-derived ARMv8, prove that the compiler configuration is well formed, and instantiate the compiler correctness theorem.