From 092803f2b60ce3d158949fe9af40e6eeab03fb13 Mon Sep 17 00:00:00 2001
From: Tim Hutt <timothy.hutt@codasip.com>
Date: Tue, 10 Dec 2024 10:54:05 +0000
Subject: [PATCH] Add clarification of tag check priority for PTEs

Clarify that the PTE check for a tag when storing capabilities happens after they are potentially removed by permission checks.
---
 src/cheri-pte-ext.adoc     | 3 +++
 src/riscv-integration.adoc | 1 +
 2 files changed, 4 insertions(+)

diff --git a/src/cheri-pte-ext.adoc b/src/cheri-pte-ext.adoc
index ce8b05d4..505d709b 100644
--- a/src/cheri-pte-ext.adoc
+++ b/src/cheri-pte-ext.adoc
@@ -104,6 +104,9 @@ 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
diff --git a/src/riscv-integration.adoc b/src/riscv-integration.adoc
index 08ea3119..b9d7a86a 100644
--- a/src/riscv-integration.adoc
+++ b/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