Add latex sources for the architecture document.

Currently they will build the tech report as released.
Having them here will allow us to update them together with
the Sail as the architecture evolves.

.gitignore

@@ -1,3 +1,4 @@
 generated_definitions
 z3_problems
 c_emulator
+sail_latex_riscv

archdoc/.gitignore

@@ -0,0 +1,2 @@
+*.pdf
+build

archdoc/LICENSE

@@ -0,0 +1,7 @@
+\noindent
+The CHERI ISA specification is licensed under the Creative Commons Attribution
+4.0 International License.  To view a copy of this license, visit:
+
+\medskip
+
+\url{http://creativecommons.org/licenses/by/4.0/}

archdoc/LICENSE-sail-cheri-riscv

@@ -0,0 +1,57 @@
+\noindent
+The CHERI-RISC-V pseudocode is derived from the Sail CHERI-RISC-V model\footnote{\url{https://github.com/CTSRD-CHERI/sail-cheri-riscv}},
+which has the following license:
+
+\begin{scriptsize}
+\begin{verbatim}
+This CHERI Sail RISC-V architecture model here, comprising all files and
+directories except for the snapshots of the Lem and Sail libraries in the
+prover_snapshots directory (which include copies of their licenses), is subject
+to the BSD two-clause licence below.
+
+Copyright (c) 2017-2021 Alasdair Armstrong, Thomas Bauereiss, Brian Campbell,
+  Jessica Clarke, Nathaniel Wesley Filardo (contributions prior to July 2020,
+  thereafter Microsoft), Alexandre Joannou, Microsoft, Prashanth Mundkur,
+  Robert Norton-Wright (contributions prior to March 2020, thereafter
+  Microsoft), Alexander Richardson, Peter Rugg, Peter Sewell
+
+All rights reserved.
+
+This software was developed by SRI International and the University of
+Cambridge Computer Laboratory (Department of Computer Science and
+Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and
+under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA
+SSITH research programme.
+
+This software was developed within the Rigorous Engineering of
+Mainstream Systems (REMS) project, partly funded by EPSRC grant
+EP/K008528/1, at the Universities of Cambridge and Edinburgh.
+
+This project has received funding from the European Research Council
+(ERC) under the European Union’s Horizon 2020 research and innovation
+programme (grant agreement 789108, ELVER).
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+2. Redistributions in binary form must reproduce the above copyright
+   notice, this list of conditions and the following disclaimer in
+   the documentation and/or other materials provided with the
+   distribution.
+
+THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''
+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR
+CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF
+USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
+ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT
+OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
+SUCH DAMAGE.
+\end{verbatim}
+\end{scriptsize}

archdoc/LICENSE-sail-riscv

@@ -0,0 +1,59 @@
+\noindent
+The RISC-V pseudocode is derived from the Sail RISC-V model\footnote{\url{https://github.com/riscv/sail-riscv}},
+which has the following license:
+\begin{scriptsize}
+\begin{verbatim}
+This Sail RISC-V architecture model, comprising all files and
+directories except for the snapshots of the Lem and Sail libraries
+in the prover_snapshots directory (which include copies of their
+licences), is subject to the BSD two-clause licence below.
+
+Copyright (c) 2017-2021 Prashanth Mundkur, Rishiyur S. Nikhil and
+  Bluespec, Inc., Jon French, Brian Campbell, Robert Norton-Wright,
+  Alasdair Armstrong, Thomas Bauereiss, Shaked Flur, Christopher Pulte,
+  Peter Sewell, Alexander Richardson, Hesham Almatary,
+  Jessica Clarke, Microsoft, for contributions by Robert Norton-Wright and
+  Nathaniel Wesley Filardo, Peter Rugg,
+  Aril Computer Corp., for contributions by Scott Johnson
+
+All rights reserved.
+
+This software was developed by the above within the Rigorous
+Engineering of Mainstream Systems (REMS) project, partly funded by
+EPSRC grant EP/K008528/1, at the Universities of Cambridge and
+Edinburgh.
+
+This software was developed by SRI International and the University of
+Cambridge Computer Laboratory (Department of Computer Science and
+Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and
+under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA
+SSITH research programme.
+
+This project has received funding from the European Research Council
+(ERC) under the European Union’s Horizon 2020 research and innovation
+programme (grant agreement 789108, ELVER).
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+2. Redistributions in binary form must reproduce the above copyright
+   notice, this list of conditions and the following disclaimer in
+   the documentation and/or other materials provided with the
+   distribution.
+
+THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''
+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR
+CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF
+USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
+ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT
+OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
+SUCH DAMAGE.
+\end{verbatim}
+\end{scriptsize}

archdoc/Makefile

@@ -0,0 +1,93 @@
+TARGET=cheriot-architecture.pdf
+MAIN_TEX=cheriot-architecture.tex
+SAIL_LATEX_RISCV_DIR=sail_latex_riscv
+
+SOURCES=$(wildcard *.tex insn-riscv/*.tex $(SAIL_LATEX_RISCV_DIR)/*.tex) cheri.bib LICENSE LICENSE-sail-cheri-riscv LICENSE-sail-riscv
+
+TIKZFIGURES=fig-representable-regions.pdf fig-sentry-plt.pdf fig-type-token.pdf
+FIGSOURCES=						\
+	misc/perms/perms5_clustered.pdf \
+	$(TIKZFIGURES)
+
+V?=0
+ifeq ($(V),0)
+INTERACTION=batchmode
+TEXLOGANALYSER_FLAGS=-w
+else
+INTERACTION=nonstopmode
+# Also include page numbers to make it easier to find what caused the warning
+TEXLOGANALYSER_FLAGS=-w -n
+endif
+
+LATEXMK_COMMON_FLAGS=-bibtex -pdf
+PDFLATEX_FLAGS=-file-line-error -halt-on-error -interaction=$(INTERACTION)
+
+.PHONY: all
+all: sail-latex ${TARGET}
+
+# The texloganalyser tool can be used to find all warning messages in the latex
+# logfile which is useful when using interaction=batchmode. There is also
+# a python package pydflatex that does the same thing (but with colours).
+# Howver, texloganalyser is included by default in some TeX distributions so
+# prefer that one.
+# TODO: fix the broken sail hyperrefs so we don't have to filter the out.
+${TARGET}: ${SOURCES} ${FIGSOURCES}
+	latexmk $(LATEXMK_COMMON_FLAGS) $(MAIN_TEX) $(PDFLATEX_FLAGS); ret=$$?; \
+	    if command -v texloganalyser >/dev/null 2>/dev/null; then \
+	        texloganalyser $(TEXLOGANALYSER_FLAGS) build/cheri-architecture.log; \
+	    fi; exit $$ret
+
+$(TIKZFIGURES): %.pdf: %.tex Makefile
+	latexmk $(LATEXMK_COMMON_FLAGS) $(PDFLATEX_FLAGS) $<
+
+.PHONY: figures
+figures: $(TIKZFIGURES)
+
+.PHONY: quick
+quick:
+	pdflatex $(MAIN_TEX) $(PDFLATEX_FLAGS)
+	@(echo "pdflatex only run once so build may be incomplete")
+
+# The sed commands require GNU sed
+ifeq ($(shell uname -s),Linux)
+SED?=sed
+else
+SED?=gsed
+endif
+
+# Work around `find: fts_read: Invalid argument` on macOS
+ifeq ($(shell uname -s),Darwin)
+FIND?=gfind
+else
+FIND?=find
+endif
+
+SAIL_CHERI_RISCV_DIR?=..
+sail-latex:
+	rm -rf $(SAIL_LATEX_RISCV_DIR)
+	$(MAKE) -C $(SAIL_CHERI_RISCV_DIR) latex
+	mv $(SAIL_CHERI_RISCV_DIR)/$(SAIL_LATEX_RISCV_DIR) .
+	$(FIND) $(SAIL_LATEX_RISCV_DIR) -type f -name 'fcl*zexecute*.tex' -exec $(SED) -i -e '1d; 2{/^{$$/d}; $$d; s/^  //;' {} +
+	touch $(SAIL_LATEX_RISCV_DIR)/0GENERATED_FILES_DO_NOT_EDIT
+	touch $(SAIL_LATEX_RISCV_DIR)/zGENERATED_FILES_DO_NOT_EDIT
+	$(FIND) $(SAIL_LATEX_RISCV_DIR) -type f -exec chmod -w {} +
+
+.PHONY: clean update-sail-defs sail-latex
+clean:
+	latexmk -C $(LATEXMK_COMMON_FLAGS) $(MAIN_TEX)
+	latexmk -C $(LATEXMK_COMMON_FLAGS) fig-*.tex
+	rm -f $(TARGET) $(TIKZFIGURES)
+
+cheri-sorted.bib: cheri.bib bib-sorting.conf
+	biber --tool $< --sortcase=false --strip-comments --sortdebug --isbn13 --isbn-normalise --fixinits \
+	    --output_indent=4 --output_fieldcase=lower --sortlocale=en_GB \
+	    --configfile=bib-sorting.conf --validate-config --output-file=$@
+
+
+.PHONY: check-bibliography check-bibliography-strict
+check-bibliography:
+	# For more detailed output add --debug
+	biber --tool cheri.bib
+
+check-bibliography-strict:
+	biber --tool --validate-datamodel cheri.bib | grep -v "Missing mandatory field 'editor'" | grep -v "is not an integer"

archdoc/acknowledgments.tex

@@ -0,0 +1,134 @@
+\section*{Acknowledgments}
+
+\vspace{-0.2cm}
+
+\noindent
+This document contains some elements from the CHERI ISA Specification\footnote{\url{https://github.com/CTSRD-CHERI/cheri-specification}},
+which is licensed under the Creative Commons Attribution 4.0 International License. 
+To view a copy of this license, visit:
+
+\medskip
+
+\url{http://creativecommons.org/licenses/by/4.0/}
+
+\medskip
+\noindent
+We acknowledge all the authors of that report:
+
+\medskip
+\begin{small}
+\noindent\begin{autogrid}{4}
+Robert~N.~M.~Watson \\
+Peter~G.~Neumann \\
+Jonathan~Woodruff \\
+Michael~Roe \\
+Hesham~Almatary \\
+Jonathan~Anderson \\
+John~Baldwin \\
+Graeme~Barnes \\
+David~Chisnall \\
+Jessica~Clarke \\
+Brooks~Davis \\
+Lee~Eisen \\
+Nathaniel~Wesley~Filardo \\
+Richard~Grisenthwaite \\
+Alexandre~Joannou \\
+Ben~Laurie \\
+A.~Theodore~Markettos \\
+Simon~W.~Moore \\
+Steven~J.~Murdoch \\
+Kyndylan~Nienhuis \\
+Robert~Norton \\
+Alexander~Richardson \\
+Peter~Rugg \\
+Peter~Sewell \\
+Stacey~Son \\
+Hongyan~Xia
+\end{autogrid}
+\end{small}
+
+\medskip
+\noindent
+as well as the many other contributors to the CHERI project:
+\medskip
+
+\begin{small}
+\noindent\begin{autogrid}{4}
+Sam Ainsworth \\
+Ross J. Anderson \\
+Ruben Ayrapetyan \\
+Hadrien Barral \\
+Thomas Bauereiss \\
+Stuart Biles \\
+Andrew Bivin \\
+Peter Blandford-Baker \\
+Matthias Boettcher \\
+David Brazdil \\
+Reuben Broadfoot \\
+Kevin Brodsky \\
+Ruslan Bukin \\
+Brian Campbell \\
+Gregory Chadwick \\
+Serban Constantinescu \\
+Chris Dalton \\
+Nirav Dave \\
+Dominique Devriese \\
+Mike Dodson \\
+Lawrence Esswood \\
+Jonas Fiala \\
+Wedson Filho \\
+Anthony Fox \\
+Paul J. Fox \\
+Franz Fuchs \\
+Ivan Gomes Ribeiro \\
+Paul Gotch \\
+Tom Grocutt \\
+Khilan Gudka \\
+Brett Gutstein \\
+Jong Hun Han \\
+Andy Hopper \\
+Alex Horsman \\
+Timothy Jones \\
+Asif Khan \\
+Myron King \\
+Joe Kiniry \\
+Chris Kitching \\
+Wojciech Koszek \\
+Robert Kovacsics \\
+Karthik Muthusamy \\
+Patrick Lincoln \\
+Marno van der Maas \\
+Anil Madhavapeddy \\
+Ilias Marinos \\
+Tim Marsland \\
+Ed Maste \\
+Alfredo Mazzinghi \\
+Kayvan Memarian \\
+Dejan Milojicic \\
+Andrew W. Moore \\
+Will Morland \\
+Alan Mujumdar \\
+Prashanth Mundkur \\
+Edward Napierala \\
+Philip Paeps \\
+Lucian Paul-Trifu \\
+Austin Roach \\
+Colin Rothwell \\
+John Rushby \\
+Hassen Saidi \\
+Hans Petter Selasky \\
+Andrew Scull \\
+Muhammad Shahbaz \\
+Bradley Smith \\
+Lee Smith \\
+Ian Stark \\
+Ramy Tadros \\
+Andrew Turner \\
+Richard Uhler \\
+Munraj Vadera \\
+Jacques Vidrine \\
+Hugo Vincent \\
+Philip Withnall \\
+Bjoern A. Zeeb \\
+\end{autogrid}
+\end{small}