Add version history as an appendix in architecture document.

Also update archdoc for change to tag clearing on store local violations (#20, #26).

archdoc/chap-changes.tex

@@ -0,0 +1,16 @@
+\newcommand{\ghissue}[1]{\href{https://github.com/microsoft/cheriot-sail/issues/#1}{Issue #1}}
+\newcommand{\ghpr}[1]{\href{https://github.com/microsoft/cheriot-sail/pull/#1}{PR #1}}
+\chapter{Version history}
+\label{chap:changes}
+
+\begin{description}
+\item[0.5] The version released as technical report MSR-TR-2023-6: \emph{CHERIoT: Rethinking security for low-cost embedded systems}, February 2023\footnote{\url{https://aka.ms/cheriot-tech-report}}.
+\item[0.6] The current, under-development version of the ISA. The following changes have been made since the previous released version:
+    \begin{description}
+    \item[\ghissue{20}, \ghpr{26}] Capability stores now clear the tag of the stored value instead of raising an exception in case of a store-local violation
+    (i.e. an attempt to store a non-global capability via a capability without the store-local permission).
+    Tag clearing is preferable for software because it removes the possibility of a trap when copying untrusted inputs.
+    It is also likely easier to implement hardware.
+    The CHERI exception cause code that was previously used for this (0x16) is now reserved.
+    \end{description}
+\end{description}

archdoc/chap-cheri-riscv.tex

@@ -229,7 +229,7 @@ \section{Changes to exception handling}
 0x13 & \cappermS Violation \\
 % 0x14 & \cappermLC Violation \\
 0x15 & \cappermSC Violation \\
-0x16 & \cappermSLC Violation \\
+% 0x16 & \cappermSLC Violation \\
 % 0x17 & \cappermSeal Violation \\
 0x18 & \cappermASR Violation \\
 % 0x19 & \cappermCInvoke Violation \\
@@ -301,7 +301,7 @@ \subsection{Capability permissions}
 \item[US] If \cappermUnseal is set then this capability may be used as the authority for \insnriscvref{CUnseal}.
 \item[U0] \cappermUZ is a user permission on capabilities with the sealing format. It has no special meaning to hardware but behaves like other permissions in that it may be cleared by \insnriscvref{CAndPerm} and cannot be set after being cleared. It is intended to be used as a software defined permission.
 \item[GL] If \cappermG is set then this capability is global and can be stored anywhere, otherwise it is local and may be stored only via capabilities with the \cappermSLC permission.
-\item[SL] If \cappermSLC is set (along with \cappermS and \cappermMC) then any capability may be stored via this capability, otherwise attempting to store a capability with GL cleared will result in an exception.
+\item[SL] If \cappermSLC is set (along with \cappermS and \cappermMC) then any capability may be stored via this capability. Otherwise, attempting to store a local capability (with GL unset) will store the capability with the tag cleared.
 \item[LM] If \cappermLM is not set then any tagged capabilities loaded via this capability will have SD and LM cleared.
 Thus, if SD and LM are cleared on a capability then it, and any capability loaded via it (including via indirection), will be read-only.
 This is useful for delegating a read-only pointer to a data structure, for example to enforce a language level transitive \asm{const}.

archdoc/cheriot-architecture.tex

@@ -20,8 +20,8 @@
 \input{preamble}
 
 \begin{document}
-\title{\cherimcu{}: Rethinking security\\ for low-cost embedded systems \\
-  {\large Microsoft Technical Report MSR-TR-2023-6}}
+\title{\cherimcu{} Architecture specification\\
+  Version 0.5}
 \author{
   \parbox{\linewidth}{\centering%
     Saar~Amar,
@@ -90,7 +90,9 @@ \part{Architecture specification}
 \input{chap-isaref-riscv}
 
 \appendix
+\part{Appendices}
 
+\input{chap-changes}
 \input{chap-encoding-sail}
 \input{chap-permissions}
 \input{chap-altbounds}