These comments could be removed.

I think I would just remove this code. Add a comment explaining it maybe.

I'd like to include the Sail code in the Sail-included fork of the manual to replace the pseudo-code. This condition would get lost if we removed this code, and it would not match the earlier pseudo-code. I'd rather keep the code. I'm not sure about the comment though. I'm leaning to keeping it, since it does point out the redundancy, so that we don't miss that too.

I was suggesting removing the comment because it would look odd in the ISA manual.

Same in other locations

Agreed that it would look odd in the manual. It indicates a need for a comment construct that is omitted when Sail code is inserted into documentation.

rems-project/sail#1619

these comments could be removed.

Here's the PR: riscv/riscv-isa-manual#2646

Actually it now changes both to be "read-only zero", but that actually does mean that we can do the zeroing in the read_senvcfg accessor. This isn't really different from any of our other cross-CSR WARL field legalisations, so I think I would just remove this comment. You have the comment on legalize_senvcfg anyway.

Does this line need to go before the new code?

(I missed this comment) No it should not. The Zicfiss code in Step 7 needs to check the actual R,W,X bits in the PTE.

I think we should use code like in the PR message here:

// "Raw" value of xenvcfg.SSE according to the current privilege.
// This is not the same as xSSE from the ISA manual becuase it is 1 for
// machine mode and it is not 0 if supervisor is not implemented.
function zicfiss_xSSE_raw(priv : Privilege) -> bool =
  bool_bits(match priv {
    Machine           => 0b1
    Supervisor        => menvcfg[SSE],
    VirtualSupervisor => read_henvcfg()[SSE], // The `read_` takes care of the "reads as 0".
    User              => read_senvcfg()[SSE],
    VirtualUser       => read_senvcfg()[SSE],
  })

// xSSE from the ISA manual. 0 in machine mode or if S-mode is not implemented.
function zicfiss_xSSE(priv : Privilege) -> bool =
  priv != Machine & extensionEnabled(Ext_S) & zicfiss_xSSE_raw()

// Return true if we should raise a virtual instruction exception instead
// of an illegal instruction.
function zicfiss_exception_is_virtual(priv : Privilege) -> bool =
  menvcfg[SSE] == 0b1 & (priv == VirtualSupervisor | priv == VirtualUser)

function access_ssp(priv : Privilege) = {
    if not(zicfiss_xSSE_raw(priv))
    then return (if zicfiss_exception_is_virtual(priv) then Virtual_Instruction else Illegal_Instruction);
    // ... ok
}

function execute_sspush() = {
    if not(zicfiss_xSSE(cur_privilege)) then return RETIRE_SUCCESS;

    // ... normal execution
}

function execute_ssamoswap() = {
    if not(zicfiss_xSSE(priv))
    then return (if zicfiss_exception_is_virtual(priv) then Virtual_Instruction else Illegal_Instruction);

    // ... normal execuion
}

In this code zicfiss_xSSE_raw() is the replacement for is_ssp_accessible, so I guess you could call it that, and then

function zicfiss_xSSE(priv : Privilege) -> bool =
  priv != Machine & extensionEnabled(Ext_S) & is_ssp_accessible(priv)

I don't know if that's easier to understand or not - up to you.

I find the zicfiss_xSSE_raw() here confusing because it does a read_senvcfg() without checking for currentlyEnabled(Ext_S). In my version (zicfiss_xSSE()), that read is gated by the S-mode check.

Since zicfiss_zSSE and is_ssp_accessible differ slightly for both M-mode and U-mode (since access to ssp is not gated on S-mode being implemented), I kept them separate instead of trying to unify them.

I'd prefer to handle the virtual-instruction exception using the approach in #1556, and leave a comment here for it instead. With #1556, is_ssp_accessible() will not be restricted to returning a bool, and virtual-instruction exceptions will be more straightforward.

Hmm that's a good point actually. My code exactly follows the spec as written - accessing ssp depends on senvcfg even if S mode is not implemented, which makes no sense at all. Probably needs a spec fix. I'll open an issue.

is_ssp_accessible() will not be restricted to returning a bool, and virtual-instruction exceptions will be more straightforward.

I dunno if that is simpler since none of the information that is_ssp_accessible() determines is needed to know the exception type. IMO it's simpler to have a separate function. I guess we can defer that anyway.

Looks like I even noticed that:

it is not 0 if supervisor is not implemented.

I think probably they just meant to disable access if supervisor is not implemented.

riscv/riscv-isa-manual#2708

I think the issue is more about how zicfiss_xSSE() is written. The way I have it exactly captures the Shadow-Stack-Enabled (SSE) State section of the spec. The boolean is_ssp_accessible() is an unfortunate artifact of the boolean functions we've used so far for CSR access checks, which #1556 rectifies. With #1556, the is_CSR_accessible (unfortunately named since it's no longer a boolean) can return success, illegal instruction or virtual instruction as the case may be. We would no longer need the is_ssp_accessible() in this PR and your zicfiss_exception_is_virtual() above (and hence also the zicfiss_xSSE_raw()).