Update arch doc for LG vs. seal

archdoc/chap-changes.tex

@@ -25,5 +25,17 @@ \chapter{Version history}
     \item[\ghpr{38}] Fix reversed T and B fields in the capability encoding diagram (\cref{fig:capformat}).
     There was an inconsistency between the Sail implementation and this document about the locations of the T and B fields in the capability encoding.
     The document had the T and B fields swapped compared to the Sail (which matches the Ibex implementation) so we treat the Sail as canonical and update the document to match i.e. B is in bits 0 to 8 of the metadata word and T is in 9 to 17.
+    \item[\ghpr{44}] Fix two long-standing nits regarding transitive permissions:
+      \begin{description}
+        \item[\ghissue{13}] If we clear the tag on a loaded capability because the authority lacks \cappermMC,
+          we do not also attenuate the loaded capability's permissions as per \cappermILG and \cappermLM,
+          as the result is an untagged bit pattern anyway.
+          The old behavior may have been confusing to humans or debuggers.
+        \item[\ghissue{14}] When loading a sealed capability through an authority lacking \cappermILG,
+          the loaded capability will lack \cappermG but will retain \cappermILG if present under seal.
+          This is more in line with our handling of \cappermLM, which does not modify sealed capabilities.
+          Software accepting sealed capabilities must be prepared to recieve local (that is, \cappermG-lacking) variants,
+          even if none were ever explicitly constructed.
+      \end{description}
     \end{description}
 \end{description}

archdoc/chap-cheri-riscv.tex

@@ -329,8 +329,11 @@ \subsection{Capability permissions}
 \item[LG] If \cappermILG is not set then any tagged capabilities loaded via this capability will have LG and GL cleared.
 Thus, if LG and GL are cleared before delegating a capability then it, and any capability loaded via it (including via indirection), may be stored only via capabilities with \cappermSLC.
 This limits the ability of the delegee to retain capabilities to a delegated data structure or part thereof, making it easier to later revoke access to the delegated data structure.
-Note that GL and LG are cleared even on sealed capabilities that are loaded, making this an exception to the immutability of sealed capabilities.
-This differs from the behavior of LM on sealed capabilities. Untagged capabilities are unaffected.
+In the case of loaded sealed capabilities, GL, but not LG, is cleared, making this an exception to the immutability of sealed capabilities.
+Thus, a sealed capability reached via an authority lacking LG may be stored only through a \cappermSLC authority,
+as may its unsealed form, but the further authority borne by the sealed capability once unsealed is unaltered.
+This differs from the behavior of LM on sealed capabilities.
+Untagged capabilities are unaffected.
 \item[MC] If \cappermMC is set then the load and store permissions for this capability are modified to enable capability loads (\cappermLC) and / or stores (\cappermSC).
 The \insnriscvref{CLC} instruction logically ANDs the tag of the loaded capability with MC from the capability base operand, so only capabilities with MC and LD set can be used to load tagged capabilities.
 The \insnriscvref{CSC} instruction raises an exception if the stored capability has the tag set and the capability base operand lacks either MC or SD permission, so only capabilities with MC and SD can be used to store tagged capabilities.