Remove incorrect privilege assert

The condition checks whether it's possible for a mode other than
machine mode to take interrupts, but just because it can't, that
doesn't mean we can never call this function while in another
mode.
In particular, this causes a crash if you run with S mode disabled
but U mode enabled, then mret to U mode without NExt.

model/riscv_sys_control.sail

@@ -277,21 +277,29 @@ function dispatchInterrupt(priv : Privilege) -> option((InterruptType, Privilege
  /* If we don't have different privilege levels, we don't need to check delegation.
  * Absence of U-mode implies absence of S-mode.
  */
- if not(extensionEnabled(Ext_U)) | (not(extensionEnabled(Ext_S)) & not(extensionEnabled(Ext_N))) then {
- assert(priv == Machine, "invalid current privilege");
- let enabled_pending = mip.bits & mie.bits;
- match findPendingInterrupt(enabled_pending) {
- Some(i) => let r = (i, Machine) in Some(r),
- None() => None()
- }
- } else {
+ let multipleModesSupported = extensionEnabled(Ext_U);
+ if not(multipleModesSupported) then {
+ assert(priv == Machine, "invalid current privilege")
+ };
+ /* Even with U-mode, we don't need to check delegation when M-mode is the only
+ one that can take interrupts, i.e. when we don't have S-mode and don't have
+ the N extension
+ */
+ let delegationPossible = extensionEnabled(Ext_S) | extensionEnabled(Ext_N);
+ if multipleModesSupported & delegationPossible then {
  match getPendingSet(priv) {
  None() => None(),
  Some(ip, p) => match findPendingInterrupt(ip) {
  None() => None(),
  Some(i) => let r = (i, p) in Some(r)
  }
  }
+ } else {
+ let enabled_pending = mip.bits & mie.bits;
+ match findPendingInterrupt(enabled_pending) {
+ Some(i) => let r = (i, Machine) in Some(r),
+ None() => None()
+ }
  }
 }