The "tag set, but bounds malformed" case should only be possible due to an error in the memory subsystem/bit flips, maybe we should more explicitly call out that these will not exist in a well-defined execution?

The "tag set, but bounds malformed" case should only be possible due to an error in the memory subsystem/bit flips, maybe we should more explicitly call out that these will not exist in a well-defined execution?

I think the culprit is "A capability is malformed if its encoding does not describe a valid capability because its bounds cannot be correctly decoded" in 2.2.6. The reader would expect that sentence to be a definition of "malformed capabilities", which should be something like "A capability is malformed when its bounds cannot be correctly decoded." Whether it is a valid capability is irrelevant here. Also, it's not "because its bounds cannot be correctly decoded" that a malformed capability "does not describe a valid capability". In my understanding, a malformed capability cannot be valid (i.e., tagged) only because well-formedness is always enforced, rather than by definition.

In my understanding, a malformed capability cannot be valid (i.e., tagged) only because well-formedness is always enforced, rather than by definition.

Not quite, and this is something we've been working on very recently.
If a corrupted (tagged and malformed capability) is read by the memory system it will be propagated through stores, and register moves without modification.
Any instruction which needs to decode the bounds will take action, e.g. setting the result to 0 for GCBASE.

We didn't want to clean up bad caps as LC/SC/CMV should just propagate what's there to avoid complicating the micro-architecture.

In my understanding, a malformed capability cannot be valid (i.e., tagged) only because well-formedness is always enforced, rather than by definition.

Not quite, and this is something we've been working on very recently. If a corrupted (tagged and malformed capability) is read by the memory system it will be propagated through stores, and register moves without modification. Any instruction which needs to decode the bounds will take action, e.g. setting the result to 0 for GCBASE.

We didn't want to clean up bad caps as LC/SC/CMV should just propagate what's there to avoid complicating the micro-architecture.

But the only source of malformed but tagged capabilities is errors in the memory subsystem or hardware bugs? The ISA level makes sure that tagged capabilities that can ever be created/derived are all well-formed right?

I believe this is now fixed - please reopen it if not.