Checks on pcc

[jasonyu1996]

According to 3.2.1:

Operations that update pcc, such as changing privilege or executing jump instructions,
unseal capabilities prior to writing. Therefore, implementations do not need to check that
 that pcc is unsealed when executing each instruction. However, this property has not yet
been formally verified and may not hold if additional CHERI extensions beyond
Zcheripurecap are implemented.

I'm wondering if this also holds for the other checks on pcc.
For example, can an implementation omit checks on the tag / X permission of pcc (or even omit storing them), since it seems to me that instructions that change pcc already check them as well.

[tariqkurd-repo]

It's a good question - we'd need to look at all the ways a new PCC can be installed - so from JALR, Xepc, Xtvec.
You can certainly check for the tag and X permission when using the PCC from those sources, as if it's missing it won't be possible to execute from the target PCC. After that point there's no reason to store X and the tag, as PC incrementing, branches and immediate offset jumps can't clear it, because they all check that the target is in bounds before jumping.

[jasonyu1996]

It's a good question - we'd need to look at all the ways a new PCC can be installed - so from JALR, Xepc, Xtvec. You can certainly check for the tag and X permission when using the PCC from those sources, as if it's missing it won't be possible to execute from the target PCC. After that point there's no reason to store X and the tag, as PC incrementing, branches and immediate offset jumps can't clear it, because they all check that the target is in bounds before jumping.

Yes that's also my understanding. Hence the question.

[tariqkurd-repo]

I did prepare a PR clarifying this - I'll try and finish it sometime soon.