Optimized refinements of the RISC-V specification.
The specification is aimed at clarity, and not at efficient execution, or even execution. In executable, the specification is refined to be executable. Here, we perform further refinements to make the specification efficiently executable.