  RISC-V is a relatively new, open instruction set architecture with a mature
ecosystem and an official formal machine-readable specification. It is
therefore a promising playground for formal-methods research.
  However, we observe that different formal-methods research projects are
interested in different aspects of RISC-V and want to simplify, abstract,
approximate, or ignore the other aspects. Often, they also require different
encoding styles, resulting in each project starting a new formalization
from-scratch. We set out to identify the commonalities between projects and to
represent the RISC-V specification as a program with holes that can be
instantiated differently by different projects.
  Our formalization of the RISC-V specification is written in Haskell and
leverages existing tools rather than requiring new domain-specific tools,
contrary to other approaches. To our knowledge, it is the first RISC-V
specification able to serve as the interface between a processor-correctness
proof and a compiler-correctness proof, while supporting several other projects
with diverging requirements as well.
