Proofs in this directory are carried out in NSym using Cryptol specifications. Cryptol specifications are automatically translated into Ocaml to be used in NSym proofs. The NSym proofs cover the verification of Arm assembly programs.

• Memory region accesses are aligned and inbound.