Should MRET/SRET check for PCC.ASR?

[tariqkurd-repo]

// Is XRET from given mode permitted by extension?
function ext_check_xret_priv (p : Privilege) : Privilege -> bool =
  pcc_access_system_regs()
// Called if above check fails
function ext_fail_xret_priv () : unit -> unit =
  handle_cheri_pcc_exception(CapEx_AccessSystemRegsViolation)

This is in the SAIL model but I don't see anything in the v9 spec about MRET/SRET requiring PCC.ASR. What's the correct behaviour?

[bsdjhb]

I suspect SAIL is correct here as ASR is intended to control "privileged" operations within a given ring. The intention is that you could create lesser privileged compartments in supervisor mode that can't, e.g. alter satp. Returning to a lower privilege mode definitely seems like a privileged operation that ASR should guard.

[jrtc27]

Specifically, xRET does a whole lot of CSR/SCR accesses on behalf of the requesting code, and therefore should be constrained by ASR. It's not 100% explicit, as the CSRs/SCRs aren't named in the instruction mnemonic, but it's still explicitly requested by virtue of xRET's semantics reading xEPC(C) and both reading and writing xSTATUS.

[tariqkurd-repo]

It's certainly true that xRET updates CSRs which need ASR permission, so it makes sense. It would be good to explicitly list in the spec though.