Clarifications to PTE specification

src/cheri-pte-ext.adoc

@@ -71,7 +71,9 @@ The page table entry format remains unchanged for Sv32. However, two new
 bits, Capability Write (CW) and Capability Read
 Generation (CRG), are added to leaf PTEs in Sv39, Sv48 and Sv57 as shown in
 xref:sv39pte[xrefstyle=short], xref:sv48pte[xrefstyle=short] and
-xref:sv57pte[xrefstyle=short] respectively.
+xref:sv57pte[xrefstyle=short] respectively. For non-leaf PTEs these bits
+remain reserved and must be cleared by software for forward compatibility,
+or else a page-fault exception is raised.
 
 .Sv39 page table entry
 [#sv39pte]
@@ -102,11 +104,15 @@ If the CW bit is clear then:
  of the capability being written is set.
 * When CRG is set, the "pre-CW state", two schemes are permitted (also see <<section_hardware_pte_updates>>):
 
+NOTE: The tag bit of the stored capability is checked _after_ it is potentially
+cleared <<tags_cleared_by_permissions,due to lack of permissions>>.
+
 ** The same behavior as when CRG is clear, allowing software interpretation
 of this state.
 ** When a capability store or AMO instruction is executed
 and the tag bit of the capability being written is set, the
 implementation sets the CW bit and assigns the CRG bit equal to <<sstatusreg_pte,sstatus>>.CRG.
++
 The PTE update must be
 atomic with respect to other accesses to the PTE, and must atomically check
 that the PTE is valid and grants sufficient permissions. Updates to the CW bit
@@ -129,9 +135,9 @@ regards to the ongoing capability revocation cycle. Two schemes are permitted:
 
 * A load page fault exception is raised when a capability load or AMO instruction is executed
 and the virtual page's CRG bit does not equal <<sstatusreg_pte,sstatus>>.CRG.
-* A load page fault exception is raised when a capability load or AMO instruction is executed,
-the capability read from memory has tag set
-and the virtual page's CRG bit does not equal <<sstatusreg_pte,sstatus>>.CRG.
+* A load page fault exception is raised when a capability load or AMO instruction is executed
+and the virtual page's CRG bit does not equal <<sstatusreg_pte,sstatus>>.CRG
+and the capability read from memory has its tag set.
 
 NOTE: An implementation may avoid a dependency on the tag
 bit value of the capability read. This will introduce additional traps during revocation sweeps.

src/riscv-integration.adoc

@@ -216,6 +216,7 @@ misaligned address fault exceptions when the effective address to access is
 misaligned, even if the implementation supports Zicclsm. To transfer CLEN
 misaligned bits without a tag, use integer loads and stores.
 
+[#tags_cleared_by_permissions]
 For loads, the tag of the capability loaded from memory is cleared if the
 authorising capability does not grant permission to read capabilities (i.e.
 both <<r_perm>> and <<c_perm>> must be set in AP). For stores, the tag of the