Make termination of the page table walk functions provable
unconditionally in Isabelle by catching the case when "level" becomes
negative.  On the Sail level, this case cannot occur, because "level"
has type "nat", but we currently don't automatically carry over the
non-negativity constraint of the Sail type "nat" into Isabelle.

The standard pattern completeness proof for recursive functions
generated by Lem for Isabelle seems to get confused in some situations
when there are variables with unit type (in particular the ext_ptw
argument of the page table walk functions).  Solving this properly
requires some more digging into the Isabelle simplifier, but the ad-hoc
workaround in this commit fixes the problem for now.

Extension hooks for CSR access control

Add a hook to allow extensions to veto xret. This will be used by CHERI extension. Note that illegal exception on mode check failure takes precedence over CHERI to allow for virtualisation.

For Lem, bypass the Sail implementation of {read,write}_ram and map to
atomic primitives directly.

We might want to make these functions primitive for other backends as well.

    Rename var to make it clear it is physical and not virtual.

    There are a lot of variables in riscv_mem.sail and riscv_platform.sail named addr and it's not always clear if that is physical or virtual address. These changes rename those variables to paddr to reduce ambiguity.

Run Sail with -dno_cast even when it comes from opam package

Expand getopt_long option string to multiple lines

This will make future diffs easier to read and merge, since adding and
removing options will show up as entire lines that change instead of a
few characters in the middle of the line.