Start working on documentation

14 files changed, 1981 insertions, 0 deletions

diff --git a/doc/Makefile b/doc/Makefile
new file mode 100644
index 00000000..b5a74dd6
--- /dev/null
+++ b/doc/Makefile
@@ -0,0 +1,81 @@
+##########################################################################
+#     Sail                                                               #
+#                                                                        #
+#  Copyright (c) 2013-2017                                               #
+#    Kathyrn Gray                                                        #
+#    Shaked Flur                                                         #
+#    Stephen Kell                                                        #
+#    Gabriel Kerneis                                                     #
+#    Robert Norton-Wright                                                #
+#    Christopher Pulte                                                   #
+#    Peter Sewell                                                        #
+#    Alasdair Armstrong                                                  #
+#    Brian Campbell                                                      #
+#    Thomas Bauereiss                                                    #
+#    Anthony Fox                                                         #
+#    Jon French                                                          #
+#    Dominic Mulligan                                                    #
+#    Stephen Kell                                                        #
+#    Mark Wassell                                                        #
+#                                                                        #
+#  All rights reserved.                                                  #
+#                                                                        #
+#  This software was developed by the University of Cambridge Computer   #
+#  Laboratory as part of the Rigorous Engineering of Mainstream Systems  #
+#  (REMS) project, funded by EPSRC grant EP/K008528/1.                   #
+#                                                                        #
+#  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.                                                          #
+##########################################################################
+
+ifeq ($(shell which sail),)
+$(error Cannot find sail executable, make sure it is in PATH)
+endif
+
+.PHONY: clean
+
+code_riscv.tex: ../riscv/prelude.sail ../riscv/riscv_duopod.sail
+	sail -o code_riscv -latex ../riscv/prelude.sail ../riscv/riscv_duopod.sail
+	cp code_riscv/commands.tex code_riscv.tex
+
+code_myreplicatebits.tex: examples/my_replicate_bits.sail
+	sail -o code_myreplicatebits -latex -latex_prefix mrb examples/my_replicate_bits.sail
+	cp code_myreplicatebits/commands.tex code_myreplicatebits.tex
+
+grammar.tex: ../language/sail.ott
+	ott -pp_grammar -tex_wrap false -tex_suppress_category I -tex_suppress_category D -tex_suppress_ntr terminals -tex_suppress_ntr formula -tex_suppress_ntr judgement -tex_suppress_ntr user_syntax -tex_suppress_ntr dec_comm -sort false -generate_aux_rules false  -picky_multiple_parses true -i ../language/sail.ott -o grammar.tex
+
+manual.pdf: grammar.tex introduction.tex usage.tex types.tex code_riscv.tex riscv.tex manual.tex manual.bib tutorial.tex code_myreplicatebits.tex
+	pdflatex manual.tex
+	bibtex manual
+	pdflatex manual.tex
+	pdflatex manual.tex
+
+clean:
+	-rm manual.pdf
+	-rm -rf code_riscv/
+	-rm -f code_riscv.tex
+	-rm -rf code_myreplicatebits/
+	-rm -f code_myreplicatebits.tex
+	-rm *.aux
+	-rm *.log
diff --git a/doc/examples/bitfield.sail b/doc/examples/bitfield.sail
new file mode 100644
index 00000000..a7e23738
--- /dev/null
+++ b/doc/examples/bitfield.sail
@@ -0,0 +1,8 @@
+bitfield cr : vector(8, dec, bit) = {
+  CR0 : 7 .. 4,
+  LT  : 7,
+  GT  : 6,
+  CR1 : 3 .. 2,
+  CR3 : 1 .. 0
+}
+register CR : cr
\ No newline at end of file
diff --git a/doc/examples/enum.sail b/doc/examples/enum.sail
new file mode 100644
index 00000000..3abad2d3
--- /dev/null
+++ b/doc/examples/enum.sail
@@ -0,0 +1,7 @@
+enum Foo = Bar | Baz | quux
+
+enum Foo = {
+  Bar,
+  Baz,
+  quux
+}
\ No newline at end of file
diff --git a/doc/examples/enum1.sail b/doc/examples/enum1.sail
new file mode 100644
index 00000000..7234e4d8
--- /dev/null
+++ b/doc/examples/enum1.sail
@@ -0,0 +1 @@
+enum Foo = Bar | Baz | quux
diff --git a/doc/examples/enum2.sail b/doc/examples/enum2.sail
new file mode 100644
index 00000000..b3856191
--- /dev/null
+++ b/doc/examples/enum2.sail
@@ -0,0 +1,5 @@
+enum Foo = {
+  Bar,
+  Baz,
+  quux
+}
diff --git a/doc/examples/my_replicate_bits.sail b/doc/examples/my_replicate_bits.sail
new file mode 100644
index 00000000..bd45a32d
--- /dev/null
+++ b/doc/examples/my_replicate_bits.sail
@@ -0,0 +1,52 @@
+default Order dec
+
+$include <prelude.sail>
+
+infixl 7 <<
+infixl 7 >>
+
+val operator << = "shiftl" : forall 'm. (bits('m), int) -> bits('m)
+val "shiftl" : forall 'm. (bits('m), int) -> bits('m)
+
+val operator >> = {
+  ocaml: "shiftr_ocaml",
+  c: "shiftr_c",
+  lem: "shiftr_lem"
+} : forall 'm. (bits('m), int) -> bits('m)
+
+val "or_vec" : forall 'n. (bits('n), bits('n)) -> bits('n)
+
+overload operator | = {or_vec}
+
+val my_replicate_bits : forall 'n 'm, 'm >= 1 & 'n >= 1. (int('n), bits('m)) -> bits('n * 'm)
+
+function my_replicate_bits(n, xs) = {
+  ys = zeros(n * length(xs));
+  foreach (i from 1 to n) {
+    ys = ys << length(xs);
+    ys = ys | zero_extend(xs, length(ys))
+  };
+  ys
+}
+
+val my_replicate_bits_2 : forall 'n 'm, 'm >= 1 & 'n >= 1. (int('n), bits('m)) -> bits('n * 'm)
+
+function my_replicate_bits_2(n, xs) = {
+  ys = zeros('n * 'm);
+  foreach (i from 1 to n) {
+    ys = (ys << 'm) | zero_extend(xs, 'n * 'm)
+  };
+  ys
+}
+
+val cast extz : forall 'n 'm, 'm >= 'n. bits('n) -> bits('m)
+
+function extz(xs) = zero_extend(xs, 'm)
+
+val my_replicate_bits_3 : forall 'n 'm, 'm >= 1 & 'n >= 1. (int('n), bits('m)) -> bits('n * 'm)
+
+function my_replicate_bits_3(n, xs) = {
+  ys = zeros('n * 'm);
+  foreach (i from 1 to n) ys = ys << 'm | xs;
+  ys
+}
\ No newline at end of file
diff --git a/doc/examples/struct.sail b/doc/examples/struct.sail
new file mode 100644
index 00000000..a7b267e9
--- /dev/null
+++ b/doc/examples/struct.sail
@@ -0,0 +1,5 @@
+struct Foo = {
+  bar : vector(4, dec, bit),
+  baz : int,
+  quux : range(0, 9)
+}
\ No newline at end of file
diff --git a/doc/examples/type_operator.sail b/doc/examples/type_operator.sail
new file mode 100644
index 00000000..871c8e0e
--- /dev/null
+++ b/doc/examples/type_operator.sail
@@ -0,0 +1,5 @@
+infix 3 ...
+
+type operator ... ('n : Int) ('m : Int) = range('n, 'm)
+
+let x : 3 ... 5 = 4
\ No newline at end of file
diff --git a/doc/introduction.tex b/doc/introduction.tex
new file mode 100644
index 00000000..5969f34f
--- /dev/null
+++ b/doc/introduction.tex
@@ -0,0 +1,142 @@
+\section{Introduction}
+\label{sec:intro}
+
+Sail is a language for expressing the instruction-set
+architecture (ISA) semantics of processors.
+
+Vendor architecture specification documents typically describe the
+sequential behaviour of their ISA with a combination of prose, tables,
+and pseudocode for each instruction.
+
+They vary in how precise that pseudocode is: in some it is just
+suggestive, while in others it is close to a complete description of
+the envelope of architecturally allowed behaviour for sequential code.
+
+For x86~\cite{Intel61}, the Intel pseudocode is just suggestive, with
+embedded prose, while the AMD descriptions~\cite{AMD_3_21} are prose
+alone.  For IBM Power~\cite{Power2.06}, there is reasonably detailed
+pseudocode for many instructions in the manual, but it has never been
+machine-parsed.  For ARM~\cite{armarmv8}, there is detailed
+pseudocode, which has recently become machine-processed~\cite{Reid16}.
+For MIPS~\cite{MIPS64-II,MIPS64-III} there is also reasonably detailed
+pseudocode.
+
+The behaviour of concurrent code is often described less well.  In a
+line of research from 2007--2018 we have developed mathematically
+rigorous models for the allowed architectural envelope of concurrent
+code, for x86, IBM Power, \riscv, and ARM, that have been reasonably
+well validated by experimental testing and by discussion with the
+vendors and
+others~\cite{x86popl,tphols09,cacm,CAV2010,Alglave:2011:LRT:1987389.1987395,pldi105,pldi2012,micro2015,FGP16,mixed17}.
+In the course of this, we have identified a number of subtle issues
+relating to the interface between the intra-instruction semantics and
+the inter-instruction concurrency
+semantics~\cite{pldi105,pldi2012,micro2015,FGP16,mixed17}. For
+example, the concurrency models, rather than treating each instruction
+execution as an atomic unit, require exposed register and memory
+events, knowledge of the potential register and memory footprints of
+instructions, and knowledge of changes to those during execution.  Our
+early work in this area had hand-coded instruction semantics for quite
+small fragments of the instruction sets, just enough for concurrency
+litmus tests and expressed in various ad hoc ways. As our models have
+matured, we have switched to modelling the intra-instruction semantics
+more completely and in a style closer to the vendor-documentation
+pseudocode, and Sail was developed for this.
+
+
+Sail is intended:
+\begin{itemize}
+\item To support precise definition of real-world ISA semantics;
+\item To be accessible to engineers familiar with existing vendor
+  pseudocodes, with a similar style to the pseudocodes used by ARM and IBM Power
+  (modulo minor syntactic differences);
+\item To expose the structure needed to combine the sequential ISA
+  semantics with the relaxed-memory concurrency models we have
+  developed;
+\item To provide an expressive type system that can statically check
+  the bitvector length and indexing computation that arises in these
+  specifications, to detect errors and to support code generation,
+  with type inference to minimise the required type annotations;
+\item To support execution, for architecturally complete emulation
+  automatically based on the definition;
+\item To support automatic generation of theorem-prover definitions, for
+  mechanised reasoning about ISA specifications; and
+\item To be as minimal as possible given the above, to ease the tasks
+  of code generation and theorem-prover definition generation.
+\end{itemize}
+
+A Sail specification will typically define an abstract syntax type
+(AST) of machine instructions, a decode function that takes binary
+values to AST values, and an execute function that describes how each
+of those behaves at runtime, together with whatever auxiliary
+functions and types are needed.
+%
+Given such a specification, the Sail implementation can typecheck it
+and generate:
+\begin{itemize}
+\item An internal representation of the fully type-annotated
+  definition (a deep embedding of the definition) in a form that can
+  be executed by the Sail interpreter.  These are both expressed in
+  Lem~\cite{Lem-icfp2014,Lemcode}, a language of type, function, and
+  relation definitions that can be compiled into OCaml and various
+  theorem provers. The Sail interpreter can also be used to analyse
+  instruction definitions (or partially executed instructions) to
+  determine their potential register and memory footprints.
+\item A shallow embedding of the definition, also in Lem, that can be
+  executed or converted to theorem-prover code more directly.
+Currently this is aimed at Isabelle/HOL or HOL4, though the Sail
+dependent types should support generation of idiomatic Coq definitions
+(directly rather than via Lem).
+\item A compiled version of the specification
+  directly into OCaml.
+\item A efficient executable version of the specification, compiled
+  into C code.
+\end{itemize}
+Sail does not currently support description of the assembly syntax of
+instructions, or the mapping between that and instruction AST or
+binary descriptions, although this is something we plan to add.
+
+\medskip
+
+Sail has been used to develop models of parts of several architectures:
+\begin{center}
+\begin{tabular}{|l|l|} \hline
+ARMv8 (hand) & hand-written \\ \hline
+ARMv8 (ASL)  & generated from ARM's v8.3 public ASL spec \\ \hline
+IBM Power    & extracted/patched from IBM Framemaker XML \\ \hline
+MIPS         & hand-written \\ \hline
+CHERI        & hand-written \\ \hline
+\riscv       & hand-written \\ \hline
+\end{tabular}
+\end{center}
+The ARMv8 (hand) and IBM Power models cover all user-mode instructions
+except vector, float, and load-multiple instructions, without
+exceptions; for ARMv8 this is for the A64 fragment.
+
+The ARMv8 (hand) model is hand-written based on the ARMv8-A
+specification document~\cite{armarmv8,FGP16}, principally by Flur.
+
+The Power model is based on an automatic extraction of pseudocode and
+decoding data from an XML export of the Framemaker document source of
+the IBM Power manual~\cite{Power2.06,micro2015}, with manual patching
+as necessary, principally by Kerneis and Gray.
+
+The ARMv8 (ASL) model is based on an automatic translation of ARM's
+machine-readable public v8.3 ASL specification\footnote{ARM v8-A
+  Architecture Specification:
+  \url{https://github.com/meriac/archex}}. It includes everything in
+ARM's specification.
+
+The MIPS model is hand-written based on the MIPS64 manual version
+2.5~\cite{MIPS64-II,MIPS64-III},
+but covering only the features in the BERI hardware
+reference~\cite{UCAM-CL-TR-868},
+which in turn drew on MIPS4000 and MIPS32~\cite{MIPS4000,MIPS32-I}.
+%
+The CHERI model is based on that and the CHERI ISA reference manual
+version~5~\cite{UCAM-CL-TR-891}. These two are both principally by
+Norton-Wright; they cover all basic user and kernel mode MIPS features
+sufficient to boot FreeBSD, including a TLB, exceptions and a basic
+UART for console interaction. ISA extensions such as floating point
+are not covered. The CHERI model supports either 256-bit capabilities
+or 128-bit compressed capabilities.
diff --git a/doc/manual.bib b/doc/manual.bib
new file mode 100644
index 00000000..b0dcb021
--- /dev/null
+++ b/doc/manual.bib
@@ -0,0 +1,725 @@
+@article{alglave:herd,
+  acmid = "2627752",
+  address = "New York, NY, USA",
+  articleno = "7",
+  author = "Jade Alglave and Luc Maranget and Michael Tautschnig",
+  doi = "10.1145/2627752",
+  issn = "0164-0925",
+  issue_date = "July 2014",
+  journal = "ACM TOPLAS",
+  keywords = "Concurrency; software verification; weak memory models",
+  month = jul,
+  number = "2",
+  numpages = "74",
+  pages = "7:1--7:74",
+  publisher = "ACM",
+  title = "{Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory}",
+  volume = "36",
+  year = "2014"
+}
+
+@inproceedings{tphols09,
+  author    = {Scott Owens and Susmit Sarkar and Peter Sewell},
+  title     = {A better x86 memory model: {x86-TSO}},
+  booktitle = {Proceedings of TPHOLs 2009: Theorem Proving in Higher Order Logics, LNCS 5674},
+  pages     ={391--407},
+  year      = {2009},
+}
+
+@Article{cacm,
+  author =       {Peter Sewell and Susmit Sarkar and Scott Owens and Zappa Nardelli, Francesco  and Magnus O. Myreen},
+  title =        {{x86-TSO}: A Rigorous and Usable Programmer's Model for x86 Multiprocessors},
+  journal =      {Communications of the ACM},
+  year =         {2010},
+  OPTkey =       {},
+  volume =       {53},
+  number =       {7},
+  pages =        {89--97},
+  month =        jul,
+  note =         {(Research Highlights)},
+  OPTannote =    {}
+}
+
+
+@InProceedings{pldi105,
+  author =       {Susmit Sarkar and Peter Sewell and Jade Alglave and Luc Maranget and Derek Williams},
+  title =        {Understanding {POWER} Multiprocessors},
+  OPTcrossref =  {},
+  OPTkey =       {},
+  booktitle = {Proceedings of PLDI 2011: the 32nd ACM SIGPLAN conference on Programming Language Design and Implementation},
+  OPTbooktitle =    {Proc.~PLDI},
+  OPTpages =     {},
+  year =         {2011},
+  pages = {175--186},
+  numpages = {12},
+  url = {http://doi.acm.org/10.1145/1993498.1993520},
+  doi = {10.1145/1993498.1993520},
+  OPTeditor =    {},
+  OPTvolume =    {},
+  OPTnumber =    {},
+  OPTseries =    {},
+  OPTaddress =   {},
+  OPTmonth =     {},
+  OPTorganization = {},
+  OPTpublisher = {},
+  OPTnote =      {},
+  OPTannote =    {}
+}
+
+
+
+@book{opac-b1105256,
+   title = "Reasoning about parallel architectures",
+   author = "Collier, William W.",
+   publisher = "Prentice Hall",
+   address = "Englewood Cliffs",
+   url = "http://opac.inria.fr/record=b1105256",
+   isbn = "0-13-767187-3",
+   year = 1992
+}
+
+@Misc{a57,
+  OPTkey =       {},
+  author =       {ARM},
+  title =        {Cortex-A57 Processor},
+  OPThowpublished = {},
+  OPTmonth =     {},
+  OPTyear =      {},
+  note =         {\url{www.arm.com/products/processors/} \url{cortex-a/cortex-a57-processor.php}, Accessed 2015/07/06},
+  OPTannote =    {}
+}
+
+@InProceedings{Lem-icfp2014,
+  OPTauthor =       {D. P. Mulligan and S. Owens and K. E. Gray and T. Ridge and P. Sewell},
+  author =       {Dominic P. Mulligan and Scott Owens and Kathryn E. Gray and Tom Ridge and Peter Sewell},
+  title =        {Lem: reusable engineering of real-world semantics},
+  OPTcrossref =  {},
+  OPTkey =       {},
+  booktitle =    {Proceedings of ICFP 2014: the 19th ACM SIGPLAN International Conference on Functional Programming},
+  pages =        {175--188},
+  year =         {2014},
+  url = {http://doi.acm.org/10.1145/2628136.2628143},
+  doi = {10.1145/2628136.2628143},
+  OPTeditor =    {},
+  OPTvolume =    {},
+  OPTnumber =    {},
+  OPTseries =    {},
+  OPTaddress =   {},
+  OPTmonth =     {},
+  OPTorganization = {},
+  OPTpublisher = {},
+  OPTnote =         {To appear},
+  OPTannote =    {}
+}
+
+
+
+@Misc{Lemcode,
+  OPTkey =       {},
+  OPTauthor =    {The Lem team},
+  title =        {Lem implementation},
+  howpublished = {\url{https://bitbucket.org/Peter_Sewell/lem/}},
+  OPTmonth =     {},
+  year =         {2017},
+  OPTnote =      {},
+  OPTannote =    {}
+}
+
+@InProceedings{pldi2012,
+  author = 	 {Susmit Sarkar and Kayvan Memarian and Scott Owens and Mark Batty and Peter Sewell and Luc Maranget and Jade Alglave and Derek Williams},
+  title = 	 {Synchronising {C/C++} and {POWER}},
+  OPTcrossref =  {},
+  OPTkey = 	 {},
+  booktitle =	 {Proceedings of {PLDI 2012}, the 33rd {ACM SIGPLAN conference on Programming Language Design and Implementation (Beijing)}},
+  pages = {311--322},
+  numpages = {12},
+  url = {http://doi.acm.org/10.1145/2254064.2254102},
+  doi = {10.1145/2254064.2254102},
+  year =	 {2012},
+  OPTeditor = 	 {},
+  OPTvolume = 	 {},
+  OPTnumber = 	 {},
+  OPTseries = 	 {},
+  OPTaddress = 	 {},
+  OPTmonth = 	 {},
+  OPTorganization = {},
+  OPTpublisher = {},
+  OPTnote = 	 {},
+  OPTannote = 	 {}
+}
+
+@Misc{tut,
+  OPTkey =       {},
+  author =       {Luc Maranget and Susmit Sarkar and Peter Sewell},
+  title =        {A Tutorial Introduction to the {ARM} and {POWER} Relaxed Memory
+  Models},
+  howpublished = {Draft available from \url{http://www.cl.cam.ac.uk/~pes20/ppc-supplemental/test7.pdf}},
+  OPTmonth =     {},
+  year =         2012,
+  OPTnote =      {},
+  OPTannote =    {}
+}
+
+
+@InProceedings{CAV2010,
+  OPTauthor =       {Jade Alglave and Luc Maranget and Susmit Sarkar and Peter Sewell},
+  author =       {J. Alglave and L. Maranget and S. Sarkar and P. Sewell},
+  title =        {Fences in Weak Memory Models},
+  OPTcrossref =  {},
+  OPTkey =       {},
+  booktitle =    {Proc. CAV},
+  OPTpages =     {},
+  year =         {2010},
+  OPTeditor =    {},
+  OPTvolume =    {},
+  OPTnumber =    {},
+  OPTseries =    {},
+  OPTaddress =   {},
+  OPTmonth =     {},
+  OPTorganization = {},
+  OPTpublisher = {},
+  note =         {},
+  OPTannote =    {}
+}
+
+@inproceedings{Alglave:2011:LRT:1987389.1987395,
+ author = {Alglave, Jade and Maranget, Luc and Sarkar, Susmit and Sewell, Peter},
+ title = {Litmus: running tests against hardware},
+ booktitle = {Proceedings of TACAS 2011: the 17th international conference on Tools and Algorithms for the Construction and Analysis of Systems},
+ OPTseries = {TACAS'11/ETAPS'11},
+ year = {2011},
+ isbn = {978-3-642-19834-2},
+ location = {Saarbr\&\#252;cken, Germany},
+ pages = {41--44},
+ numpages = {4},
+ url = {http://dl.acm.org/citation.cfm?id=1987389.1987395},
+ acmid = {1987395},
+ publisher = {Springer-Verlag},
+ address = {Berlin, Heidelberg},
+} 
+
+@Misc{diy,
+  OPTkey =       {},
+  author =       {Jade Alglave and Luc Maranget},
+  title =        {The \texttt{diy} tool},
+  howpublished = {\url{http://diy.inria.fr/}},
+  OPTmonth =     {},
+  OPTyear =      {},
+  OPTnote =      {},
+  OPTannote =    {}
+}
+@Book{PDL,
+  ALTauthor =    {},
+  editor =       {Prabhat Misra and Nikil Dutt},
+  title =        {Processor Description Languages},
+  publisher =    {Morgan Kaufmann},
+  year =         {2008},
+  OPTkey =       {},
+  OPTvolume =    {},
+  OPTnumber =    {},
+  OPTseries =    {},
+  OPTaddress =   {},
+  OPTedition =   {},
+  OPTmonth =     {},
+  OPTnote =      {},
+  OPTannote =    {}
+}
+@inproceedings{Goel:2014:SFV:2682923.2682944,
+ author = {Goel, Shilpi and Hunt, Warren A. and Kaufmann, Matt and Ghosh, Soumava},
+ title = {Simulation and Formal Verification of x86 Machine-Code Programs That Make System Calls},
+ booktitle = {Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design},
+ series = {FMCAD '14},
+ year = {2014},
+ isbn = {978-0-9835678-4-4},
+ location = {Lausanne, Switzerland},
+ pages = {18:91--18:98},
+ articleno = {18},
+ numpages = {8},
+ url = {http://dl.acm.org/citation.cfm?id=2682923.2682944},
+ acmid = {2682944},
+ publisher = {FMCAD Inc},
+ address = {Austin, TX},
+} 
+
+@inproceedings{DBLP:conf/itp/Fox12,
+  author    = {Anthony C. J. Fox},
+  title     = {Directions in {ISA} Specification},
+  booktitle = {Interactive Theorem Proving -- Third International Conference, {ITP}
+               2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings},
+  pages     = {338--344},
+  year      = {2012},
+  crossref  = {DBLP:conf/itp/2012},
+  url       = {http://dx.doi.org/10.1007/978-3-642-32347-8_23},
+  doi       = {10.1007/978-3-642-32347-8_23},
+  timestamp = {Tue, 14 Aug 2012 11:20:26 +0200},
+  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/itp/Fox12},
+  bibsource = {dblp computer science bibliography, http://dblp.org}
+}
+@article{Sevcik:2013:CVC:2487241.2487248,
+ author = {\v{S}ev\v{c}\'{\i}k, Jaroslav and Vafeiadis, Viktor and Zappa Nardelli, Francesco and Jagannathan, Suresh and Sewell, Peter},
+ title = {{CompCertTSO}: A Verified Compiler for Relaxed-Memory Concurrency},
+ OPTjournal = {Journal of the ACM},
+ journal = {J. ACM},
+ issue_date = {June 2013},
+ volume = {60},
+ number = {3},
+ month = jun,
+ year = {2013},
+ issn = {0004-5411},
+ pages = {22:1--22:50},
+ articleno = {22},
+ numpages = {50},
+ url = {http://doi.acm.org/10.1145/2487241.2487248},
+ doi = {10.1145/2487241.2487248},
+ acmid = {2487248},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ keywords = {Relaxed memory models, semantics, verified compilation},
+} 
+
+
+@incollection{shi2011,
+year={2011},
+isbn={978-3-642-25378-2},
+booktitle={Certified Programs and Proofs},
+volume={7086},
+series={Lecture Notes in Computer Science},
+editor={Jouannaud, Jean-Pierre and Shao, Zhong},
+doi={10.1007/978-3-642-25379-9_25},
+title={First Steps towards the Certification of an {ARM} Simulator Using {Compcert}},
+url={http://dx.doi.org/10.1007/978-3-642-25379-9_25},
+publisher={Springer Berlin Heidelberg},
+author={Shi, Xiaomu and Monin, Jean-François and Tuong, Frédéric and Blanqui, Frédéric},
+pages={346-361},
+language={English}
+}
+
+
+
+@Manual{armarmv8,
+  title =        {ARM Architecture Reference Manual (ARMv8, for ARMv8-A architecture profile)},
+  OPTkey =       {},
+  OPTauthor =    {},
+  organization = {ARM Ltd.},
+  OPTaddress =   {},
+  OPTedition =   {},
+  OPTmonth =     {},
+  year =         {2015},
+  note =         {ARM DDI 0487A.h (ID092915)},
+  OPTannote =    {}
+}
+
+
+@inproceedings{Dias:2010:AGI:1706299.1706346,
+ author = {Dias, Jo\~{a}o and Ramsey, Norman},
+ title = {Automatically Generating Instruction Selectors Using Declarative Machine Descriptions},
+ booktitle = {Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
+ series = {POPL '10},
+ year = {2010},
+ isbn = {978-1-60558-479-9},
+ location = {Madrid, Spain},
+ pages = {403--416},
+ numpages = {14},
+ url = {http://doi.acm.org/10.1145/1706299.1706346},
+ doi = {10.1145/1706299.1706346},
+ acmid = {1706346},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ keywords = {declarative machine descriptions, instruction selection, retargetable compilers},
+} 
+
+ 
+@ARTICLE{Leroy-backend,
+  AUTHOR = {Xavier Leroy},
+  TITLE = {A formally verified compiler back-end},
+  JOURNAL = {Journal of Automated Reasoning},
+  VOLUME = 43,
+  NUMBER = 4,
+  PAGES = {363--446},
+  YEAR = 2009,
+  URL = {http://gallium.inria.fr/~xleroy/publi/compcert-backend.pdf},
+  URLPUBLISHER = {http://dx.doi.org/10.1007/s10817-009-9155-4},
+  HAL = {http://hal.inria.fr/inria-00360768/},
+  PUBKIND = {journal-int-mono}
+}
+
+
+@inproceedings{DBLP:conf/fopara/AmadioABBCGMMMPPRCST13,
+  author    = {Roberto M. Amadio and
+               Nicholas Ayache and
+               Fran{\c{c}}ois Bobot and
+               Jaap Boender and
+               Brian Campbell and
+               Ilias Garnier and
+               Antoine Madet and
+               James McKinna and
+               Dominic P. Mulligan and
+               Mauro Piccolo and
+               Randy Pollack and
+               Yann R{\'{e}}gis{-}Gianas and
+               Claudio Sacerdoti Coen and
+               Ian Stark and
+               Paolo Tranquilli},
+  title     = {Certified Complexity (CerCo)},
+  booktitle = {Foundational and Practical Aspects of Resource Analysis - Third International
+               Workshop, {FOPARA} 2013, Bertinoro, Italy, August 29-31, 2013, Revised
+               Selected Papers},
+  pages     = {1--18},
+  year      = {2013},
+  crossref  = {DBLP:conf/fopara/2013},
+  url       = {http://dx.doi.org/10.1007/978-3-319-12466-7_1},
+  doi       = {10.1007/978-3-319-12466-7_1},
+  timestamp = {Sat, 25 Oct 2014 15:12:46 +0200},
+  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/fopara/AmadioABBCGMMMPPRCST13},
+  bibsource = {dblp computer science bibliography, http://dblp.org}
+}
+
+@inproceedings{Kumar:2014:CVI:2535838.2535841,
+ author = {Kumar, Ramana and Myreen, Magnus O. and Norrish, Michael and Owens, Scott},
+ title = {CakeML: A Verified Implementation of ML},
+ booktitle = {Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
+ series = {POPL '14},
+ year = {2014},
+ isbn = {978-1-4503-2544-8},
+ location = {San Diego, California, USA},
+ pages = {179--191},
+ numpages = {13},
+ url = {http://doi.acm.org/10.1145/2535838.2535841},
+ doi = {10.1145/2535838.2535841},
+ acmid = {2535841},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ keywords = {ML, compiler bootstrapping, compiler verification, machine code verification, read-eval-print loop, verified garbage collection., verified parsing, verified type checking},
+} 
+
+
+
+@inproceedings{Kennedy:2013:CWB:2505879.2505897,
+ author = {Kennedy, Andrew and Benton, Nick and Jensen, Jonas B. and Dagand, Pierre-Evariste},
+ title = {Coq: The World's Best Macro Assembler?},
+ booktitle = {Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming},
+ series = {PPDP '13},
+ year = {2013},
+ isbn = {978-1-4503-2154-9},
+ location = {Madrid, Spain},
+ pages = {13--24},
+ numpages = {12},
+ url = {http://doi.acm.org/10.1145/2505879.2505897},
+ doi = {10.1145/2505879.2505897},
+ acmid = {2505897},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ keywords = {Coq, assembly code, dependent types},
+} 
+
+
+@inproceedings{DBLP:conf/pldi/MorrisettTTTG12,
+  author    = {Greg Morrisett and
+               Gang Tan and
+               Joseph Tassarotti and
+               Jean{-}Baptiste Tristan and
+               Edward Gan},
+  title     = {RockSalt: better, faster, stronger {SFI} for the x86},
+  booktitle = {{ACM} {SIGPLAN} Conference on Programming Language Design and Implementation,
+               {PLDI} '12, Beijing, China - June 11 - 16, 2012},
+  pages     = {395--404},
+  year      = {2012},
+  crossref  = {DBLP:conf/pldi/2012},
+  url       = {http://doi.acm.org/10.1145/2254064.2254111},
+  doi       = {10.1145/2254064.2254111},
+  timestamp = {Tue, 12 Jun 2012 20:04:16 +0200},
+  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/pldi/MorrisettTTTG12},
+  bibsource = {dblp computer science bibliography, http://dblp.org}
+}
+
+
+@Misc{ppcmemlwn,
+  OPTkey =       {},
+  author =       {Paul McKenney},
+  title =        {Validating Memory Barriers and Atomic Instructions},
+  howpublished = {Linux Weekly News article},
+  month =        dec,
+  year =         2011,
+  note =         {\url{https://lwn.net/Articles/470681/}},
+  OPTannote =    {}
+}
+
+@InProceedings{micro2015,
+  author =       {Kathryn E. Gray and Gabriel Kerneis and Dominic Mulligan and Christopher Pulte and Susmit Sarkar and  Peter Sewell},
+  title =        {An integrated concurrency and core-{ISA} architectural envelope definition, and test oracle, for {IBM POWER} multiprocessors},
+  OPTcrossref =  {},
+  OPTkey =       {},
+  booktitle =    {Proc.~MICRO-48, the 48th Annual IEEE/ACM International Symposium on Microarchitecture},
+  OPTpages =     {},
+  year =         {2015},
+  OPTeditor =    {},
+  OPTvolume =    {},
+  OPTnumber =    {},
+  OPTseries =    {},
+  OPTaddress =   {},
+  month =        dec,
+  OPTorganization = {},
+  OPTpublisher = {},
+  OPTnote =      {},
+  OPTannote =    {}
+}
+
+
+
+@Misc{Intel61,
+  OPTkey =       {},
+  author =       {Intel},
+  title =        {{Intel 64 and IA-32 Architectures Software Developer's Manual}},
+  howpublished = {\url{https://software.intel.com/en-us/articles/intel-sdm}},
+  month =        dec,
+  year =         2016,
+  note =         {325462-061US},
+  OPTannote =    {}
+}
+
+
+
+
+
+@Misc{AMD_3_21,
+  OPTkey =       {},
+  author =       {AMD},
+  title =        {{AMD64} Architecture Programmer's Manual Volume 1: Application Programming},
+  howpublished = {\url{http://support.amd.com/TechDocs/24592.pdf}},
+  month =        oct,
+  year =         {2013},
+  note =         {Revision 3.21},
+  OPTannote =    {}
+}
+
+@Book{Power2.06,
+  ALTauthor =    {},
+  ALTeditor =    {},
+  title =        {Power ISA Version 2.06B},
+  publisher =    {IBM},
+  year =         {2010},
+  OPTkey =       {},
+  OPTvolume =    {},
+  OPTnumber =    {},
+  OPTseries =    {},
+  OPTaddress =   {},
+  OPTedition =   {},
+  OPTmonth =     {},
+  note =         {\url{https://www.power.org/wp-content/uploads/2012/07/PowerISA_V2.06B_V2_PUBLIC.pdf} (accessed 2015/07/22)},
+  OPTannote =    {}
+}
+
+
+@InProceedings{Reid16,
+  author =       {Alastair Reid},
+  title =        {Trustworthy Specifications of {ARM} {v8-A} and {v8-M} System Level Architecture},
+  OPTcrossref =  {},
+  OPTkey =       {},
+  booktitle =    {Proc.~FMCAD},
+  OPTpages =     {},
+  year =         {2016},
+  OPTeditor =    {},
+  OPTvolume =    {},
+  OPTnumber =    {},
+  OPTseries =    {},
+  OPTaddress =   {},
+  OPTmonth =     {},
+  OPTorganization = {},
+  OPTpublisher = {},
+  OPTnote =      {},
+  OPTannote =    {}
+}
+
+
+@InProceedings{x86popl,
+  OPTkey =       {},
+  OPTauthor =       {S. Sarkar and P. Sewell and Zappa Nardelli, F. and S. Owens and T. Ridge and T. Braibant and M. Myreen and J. Alglave},
+  author =       {Susmit Sarkar and Peter Sewell and Zappa Nardelli, Francesco and Scott Owens and Tom Ridge and Thomas Braibant and Magnus Myreen and Jade Alglave},
+  title =        {The Semantics of {x86-CC} Multiprocessor Machine Code},
+  year =         {2009},
+  OPTpages =         {},
+  OPTcrossref =  {},
+  OPTkey =       {},
+  booktitle = {Proceedings of POPL 2009: the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages},
+  OPTbooktitle =    {Proc.~POPL 2009},
+  pages = {379--391},
+  numpages = {13},
+  url = {http://doi.acm.org/10.1145/1594834.1480929},
+  doi = {10.1145/1594834.1480929},
+  OPTpages =     {},
+  OPTyear =      {},
+  OPTeditor =    {},
+  OPTvolume =    {},
+  OPTnumber =    {},
+  OPTseries =    {},
+  OPTaddress =   {},
+  month =        jan,
+  OPTorganization = {},
+  OPTpublisher = {},
+  OPTnote =         {To appear},
+  OPTannote =    {},
+  OPTurl = ""
+}
+@InProceedings{FGP16,
+  author =       {Shaked Flur and Kathryn E. Gray and Christopher Pulte and Susmit Sarkar and Ali Sezgin and  Luc Maranget and Will Deacon and Peter Sewell},
+  title =        {Modelling the {ARMv8} Architecture, Operationally: Concurrency and {ISA}},
+  OPTcrossref =  {},
+  OPTkey =       {},
+  booktitle =    {Proceedings of POPL: the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
+  OPTpages =     {},
+  year =         {2016},
+  OPTeditor =    {},
+  OPTvolume =    {},
+  OPTnumber =    {},
+  OPTseries =    {},
+  OPTaddress =   {},
+  OPTmonth =     {},
+  OPTorganization = {},
+  OPTpublisher = {},
+  OPTnote =      {},
+  OPTannote =    {}
+}
+@inproceedings{mixed17,
+  author    = {Shaked Flur and Susmit Sarkar and Christopher Pulte and Kyndylan Nienhuis and Luc Maranget and Kathryn E. Gray and Ali Sezgin and Mark Batty and Peter Sewell},
+  title     = {Mixed-size Concurrency: {ARM}, {POWER}, {C/C++11}, and {SC}},
+  booktitle = {{{POPL} 2017}: The 44th Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of
+               Programming Languages,  Paris, France},
+  OPTpages     = {179--192},
+  year      = {2017},
+  month = jan,
+  OPTcrossref  = {DBLP:conf/popl/2014},
+  OPTurl       = {http://doi.acm.org/10.1145/2535838.2535841},
+  OPTdoi       = {10.1145/2535838.2535841},
+  OPTtimestamp = {Thu, 09 Jan 2014 08:32:32 +0100},
+  OPTbiburl    = {http://dblp.uni-trier.de/rec/bib/conf/popl/KumarMNO14},
+  OPTbibsource = {dblp computer science bibliography, http://dblp.org},
+  abstract  = {
+Previous work on the semantics of relaxed shared-memory concurrency has only considered the case in which each load reads the data of exactly one store.  In practice, however, multiprocessors support mixed-size accesses, and these are used by systems software and (to some degree) exposed at the C/C++ language level.  A semantic foundation for software therefore has to address them.
+
+
+We investigate the mixed-size behaviour of ARMv8 and IBM POWER architectures and implementations: by experiment, by developing semantic models, by testing the correspondence between these, and by discussion with ARM and IBM staff.  This turns out to be surprisingly subtle, and on the way we have to revisit the fundamental concepts of coherence and sequential consistency, which change in this setting.  In particular, we show that adding a memory barrier between each instruction does not restore sequential consistency.  We go on to extend the C/C++11 model to support non-atomic mixed-size memory accesses, and prove the standard compilation scheme from C11 atomics to POWER remains sound.
+
+
+This is a necessary step towards semantics for real-world shared-memory concurrent code, beyond litmus tests.
+}
+}
+
+
+@TechReport{UCAM-CL-TR-891,
+  author =	 {Watson, Robert N. M. and Neumann, Peter G. and Woodruff,
+          	  Jonathan and Roe, Michael and Anderson, Jonathan and
+          	  Chisnall, David and Davis, Brooks and Joannou, Alexandre
+          	  and Laurie, Ben and Moore, Simon W. and Murdoch, Steven J.
+          	  and Norton, Robert and Son, Stacey and Xia, Hongyan},
+  title = 	 {{Capability Hardware Enhanced RISC Instructions: CHERI
+         	   Instruction-Set Architecture (Version 5)}},
+  year = 	 2016,
+  month = 	 jun,
+  url = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-891.pdf},
+  institution =  {University of Cambridge, Computer Laboratory},
+  number = 	 {UCAM-CL-TR-891}
+}
+
+@article{ott-jfp,
+  author =       {Peter Sewell and Zappa Nardelli, Francesco  and Scott Owens and Gilles Peskine and Thomas Ridge and Susmit Sarkar and Rok Strni\v sa},
+  title =        {{Ott}: Effective Tool Support for the Working Semanticist},
+  OPTcrossref =  {},
+  OPTkey =       {},
+  optjournal =      {J. Functional Programming},
+  journal =      {Journal of Functional Programming},
+  year =         {2010},
+  OPTkey =       {},
+  volume =       {20},
+  number =       {1},
+  pages =        {70--122},
+  month =        jan,
+  note =         {Invited submission from ICFP 2007},
+  OPTannote =    {}
+}
+
+@Misc{ottcode,
+  OPTkey =       {},
+  author =       {Peter Sewell and Zappa Nardelli, Francesco and Scott Owens},
+  title =        {Ott},
+  howpublished = {\url{https://github.com/ott-lang/ott}},
+  OPTmonth =     {},
+  year =         {2017},
+  OPTnote =      {},
+  OPTannote =    {}
+}
+
+
+
+@TechReport{UCAM-CL-TR-868,
+  author =	 {Watson, Robert N. M. and Woodruff, Jonathan and Chisnall,
+          	  David and Davis, Brooks and Koszek, Wojciech and Markettos,
+          	  A. Theodore and Moore, Simon W. and Murdoch, Steven J. and
+          	  Neumann, Peter G. and Norton, Robert and Roe, Michael},
+  title = 	 {{Bluespec Extensible RISC Implementation: BERI Hardware
+         	   reference}},
+  year = 	 2015,
+  month = 	 apr,
+  url = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-868.pdf},
+  institution =  {University of Cambridge, Computer Laboratory},
+  number = 	 {UCAM-CL-TR-868}
+}
+
+
+
+
+
+@Misc{MIPS64-II,
+  OPTkey =       {},
+  author =       {{MIPS Technologies, Inc.}},
+  title =        {{MIPS64 Architecture For Programmers. Volume II: The MIPS64 Instruction Set}},
+  OPThowpublished = {},
+  month =        jul,
+  year =         {2005},
+  note =         {Revision 2.50. Document Number: MD00087},
+  OPTannote =    {}
+}
+
+
+@Misc{MIPS64-III,
+  OPTkey =       {},
+  author =       {{MIPS Technologies, Inc.}},
+  title =        {{MIPS64 Architecture For Programmers. Volume III: The MIPS64 Privileged Resource Architecture}},
+  OPThowpublished = {},
+  month =        jul,
+  year =         {2005},
+  note =         {Revision 2.50. Document Number: MD00091},
+  OPTannote =    {}
+}
+
+
+
+
+@Book{MIPS4000,
+  author =       {Joe Heinrich},
+  ALTeditor =    {},
+  title =        {{MIPS R4000 Microprocessor User's Manual (Second Edition)}},
+  publisher =    {{MIPS Technologies, Inc.}},
+  year =         {1994},
+  OPTkey =       {},
+  OPTvolume =    {},
+  OPTnumber =    {},
+  OPTseries =    {},
+  OPTaddress =   {},
+  OPTedition =   {},
+  OPTmonth =     {},
+  OPTnote =      {},
+  OPTannote =    {}
+}
+
+
+@Misc{MIPS32-I,
+  OPTkey =       {},
+  author =       {{MIPS Technologies, Inc.}},
+  title =        {{MIPS32 Architecture For Programmers. Volume I: Introduction to the MIPS32 Architecture}},
+  OPThowpublished = {},
+  month =        mar,
+  year =         2001,
+  note =         {Revision 0.95. Document Number  MD00082},
+  OPTannote =    {}
+}
+
diff --git a/doc/manual.tex b/doc/manual.tex
new file mode 100644
index 00000000..a52600a5
--- /dev/null
+++ b/doc/manual.tex
@@ -0,0 +1,87 @@
+\documentclass[a4paper]{article}
+
+\usepackage[nounderscore]{syntax}
+\usepackage{amsmath,amssymb}
+\usepackage[svgnames]{xcolor}
+\usepackage{algorithmicx}
+\usepackage{algpseudocode}
+\usepackage{fullpage}
+\usepackage{listings}
+\usepackage{tikz}
+\usetikzlibrary{arrows}
+\usepackage{hyperref}
+
+\hypersetup{colorlinks=true,linkcolor=DarkRed}
+
+\newcommand{\TODO}[1]{{\color{red}{TODO: #1}}}
+
+\lstset{
+  basicstyle=\ttfamily\small,
+  columns=fullflexible,
+  breaklines=true,
+  postbreak=\mbox{\textcolor{red}{$\hookrightarrow$}\space},
+}
+
+\lstdefinelanguage{sail}
+  { morekeywords={val,function,cast,type,forall,overload,operator,enum,union,undefined,exit,and,assert,sizeof,
+      scattered,register,inc,dec,if,then,else,effect,let,as,@,in,end,Type,Int,Order,match,clause,struct,
+      foreach,from,to,by,infix,infixl,infixr,bitfield,default},
+    keywordstyle={\bf\ttfamily\color{blue}},
+    morestring=[b]",
+    stringstyle={\ttfamily\color{red}},
+    morecomment=[l][\itshape\color{DarkGreen}]{//},
+    morecomment=[s][\itshape\color{DarkGreen}]{/*}{*/},
+    deletestring=[bd]{'},
+    escapechar=\#,
+    emphstyle={\it},
+    literate=
+      {\{|}{{$\{|$}}1
+      {|\}}{{$|\}$}}1
+  }
+
+\lstset{language=sail}
+
+\def\sail{\trivlist \item\relax}
+\def\endsail{\endtrivlist}
+
+\renewcommand{\ll}[1]{\lstinline{#1}}
+
+\newcommand{\riscv}{RISC-V}
+
+%% \input{grammar}
+
+%% \renewcommand{\ottkw}[1]{\mbox{\ttfamily\bfseries{#1}}}
+%% \renewcommand{\ottsym}[1]{\mathop{\mbox{\ttfamily{#1}}}}
+%% %\renewcommand{\ottgrammartabular}[1]{\begin{center}\begin{tabular}{llcllllll}#1\end{tabular}\end{center}}
+%% \renewcommand{\ottgrammartabular}[1]{\medskip\par\begin{supertabular}{llcllllll}#1\end{supertabular}\medskip\par\noindent}
+%% \newcommand{\ottpartialrulehead}[3]{$#1$ & & $#2$ & $\ldots$ & & \multicolumn{2}{l}{#3}}
+%% \renewcommand{\ottrulehead}[3]{\multicolumn{9}{l}{$#1$\quad $#2$}}%
+%% \renewcommand{\ottprodline}[6]{\multicolumn{9}{l}{\quad$#1$\quad $#2$}}%
+
+\begin{document}
+
+\input{code_riscv}
+
+\title{The Sail instruction-set semantics specification language}
+
+\author{Kathryn E. Gray \and Peter Sewell \and Christopher Pulte \and
+  Shaked Flur \and Robert Norton-Wright \and Alasdair Armstrong}
+
+\maketitle
+
+\tableofcontents
+
+\include{introduction}
+
+\include{riscv}
+
+\include{usage}
+
+\include{tutorial}
+
+\include{types}
+
+\bibliographystyle{unsrt}
+\bibliography{manual}
+
+\end{document}
diff --git a/doc/riscv.tex b/doc/riscv.tex
new file mode 100644
index 00000000..e2aa3025
--- /dev/null
+++ b/doc/riscv.tex
@@ -0,0 +1,140 @@
+\section{A tutorial \riscv\ example}
+\label{sec:riscv}
+
+We introduce the basic features of Sail via a small example from our
+\riscv\ model that includes just two instructions: add immediate and
+load double.
+
+We start with some basic type synonyms. We create a type \ll{xlen_t}
+for bitvectors of length 64, then we define a type \ll{regno}, which
+is a type synonym for the builtin type \ll{atom}. The type
+\ll{atom('n)} is a number which is exactly equal to the type variable
+\ll{atom('n)}. Type variables are syntactically marked with single
+quotes, as in ML. A \emph{constraint} can be attached to this type
+synonym---ensuring that it is only used where we can guarantee that
+its value will be between 0 and 31. Sail supports a rich variety of
+numeric types, including range types, which are statically checked. We
+then define a synonym \ll{regbits} for \ll{bits(5)}. We don't want to
+manually convert between \ll{regbits} and \ll{regno} all the time, so
+we define a function that maps between them and declare it as a
+\emph{cast}, which allows the type-checker to insert it where
+needed. By default, we do not do any automatic casting (except between
+basic numeric types when safe), but to allow idioms in ISA vendor
+description documents we support flexible user defined casts. To ensure
+that the constraint on the \ll{regno} type synonym is satisfied, we
+return an existentially quantified type \ll{\{'n, 0 <= 'n <
+  32. regno('n)\}}.
+
+\sailxlent
+\sailregno
+\sailregbits
+\sailregbitstoregno
+\sailfnregbitstoregno
+
+We now set up some basic architectural state. First creating a
+register of type \ll{xlen_t} for both the program counter \ll{PC}, and
+the next program counter, \ll{nextPC}. We define the general purpose
+registers as a vector of 32 \ll{xlen_t} bitvectors. The \ll{dec}
+keyword isn't important in this example, but Sail supports two
+different numbering schemes for (bit)vectors \ll{inc}, for most
+significant bit is zero, and \ll{dec} for least significant bit is
+zero. We then define a getter and setter for the registers, which
+ensure that the zero register is treated specially (in
+\riscv\ register 0 is always hardcoded to be 0). Finally we overload
+both the read (\ll{rX}) and write (\ll{wX}) functions as simply
+\ll{X}. This allows us to write registers as \ll{X(r) = value} and
+read registers as \ll{value = X(r)}. Sail supports flexible ad-hoc
+overloading, and has an expressive l-value language in assignments,
+with the aim of allowing pseudo-code like definitions.
+
+\begin{lstlisting}
+register PC : xlen_t
+register nextPC : xlen_t
+
+register Xs : vector(32, dec, xlen_t)
+\end{lstlisting}
+
+\sailrX
+\sailfnrX
+\sailfnrXA
+
+\sailwX
+\sailfnwX
+\sailX
+
+We also give a function \ll{MEMr} for reading memory, this function
+just points at a builtin we have defined elsewhere \TODO{Section where
+  we talk about preludes, built-in type environment etc}. Note that functions in sail are
+annotated with effects. This effect system is quite basic, but
+indicates whether or not functions read or write registers (rreg and
+wreg), read and write memory (rmem and wmem), as well as a host of
+other concurrency model related effects. They also indicate whether a
+function throws exceptions or has other non-local control flow (the
+escape effect).
+
+\sailMEMr
+\sailfnMEMr
+
+It's common when defining architecture specications to break
+instruction semantics down into separate functions that handle
+decoding (possibly even in several stages) into custom intermediate
+datatypes and executing the decoded instructions. However it's often
+desirable to group the relevant parts of these functions and datatypes
+together in one place, as they would usually be found in an
+architecture reference manual. To support this sail supports
+\emph{scattered} definitions. First we give types for the execute and
+decode functions, and declare them as scattered functions, as well as
+the \ll{ast} union.
+
+\sailiop
+
+\begin{lstlisting}
+scattered union ast
+
+val decode : bits(32) -> option(ast) effect pure
+scattered function decode
+
+val execute : ast -> unit effect {rmem, rreg, wreg}
+scattered function execute
+\end{lstlisting}
+
+Now we provide the clauses for the add immediate \ll{ast} type, as
+well as it's execute and decode clauses. We can define the decode
+function by directly pattern matching on the bitvector representing
+the instruction. Sail supports vector concatentation patterns (\ll{@}
+is the vector concatenation operator), and uses the types provided
+(e.g. \ll{bits(12)} and \ll{regbits}) to destructure the vector in the
+correct way.
+
+\begin{lstlisting}
+union clause ast = ITYPE : (bits(12), regbits, regbits, iop)
+\end{lstlisting}
+
+\sailfndecodeSomeITYPE
+\sailfnexecuteITYPE
+
+\noindent Now we do the same thing for the load duble instruction:
+
+\begin{lstlisting}
+union clause ast = LOAD : (bits(12), regbits, regbits)
+\end{lstlisting}
+
+\sailfndecodeSomeLOAD
+\sailfnexecuteLOAD
+
+Finally we define the fallthrough case for the decode function, and
+end all our scattered definitions. Note that the clauses in a
+scattered function will be executed in the order they appear in the
+file.
+
+\sailfndecodeNone
+
+\begin{lstlisting}
+end ast
+end decode
+end execute
+\end{lstlisting}
+
+The actual code for this example, as well as our more complete
+\riscv\ specification can be found on our github at
+\url{https://github.com/rems-project/sail/blob/sail2/riscv/riscv_duopod.sail}.
diff --git a/doc/tutorial.tex b/doc/tutorial.tex
new file mode 100644
index 00000000..61ec73f3
--- /dev/null
+++ b/doc/tutorial.tex
@@ -0,0 +1,558 @@
+\section{Sail Language}
+
+\subsection{Functions}
+\label{sec:functions}
+
+\input{code_myreplicatebits}
+
+In Sail, functions are declared in two parts. First we write the type
+signature for the function using the \ll{val} keyword, then define the
+body of the function via the \ll{function} keyword. In this
+Subsection, we will write our own version of the \ll{replicate_bits}
+function from the Sail library. This function takes a number $n$ and a
+bitvector, and copies that bitvector $n$ times.
+
+\mrbmyreplicatebits
+
+\noindent The general syntax for a function type in Sail is as follows:
+\begin{center}
+  \ll{val} \textit{name} \ll{:} \ll{forall} \textit{type variables} \ll{,} \textit{constraint} \ll{. (} \textit{type$_1$} \ll{,} $\ldots$ \ll{,} \textit{type$_2$} \ll{)} \ll{->} \textit{return type}
+\end{center}
+An implementation for the \ll{replicate_bits} function would be
+follows \mrbfnmyreplicatebits
+
+The general syntax for a function declaration is:
+\begin{center}
+  \ll{function} \textit{name} \ll{(} \textit{argument$_1$} \ll{,} $\ldots$ \ll{,} \textit{argument$_n$} \ll{)} \ll{=} \textit{expression}
+\end{center}
+
+Code for this example can be found in
+the Sail repository in \verb|doc/examples/my_replicate_bits.sail|. To
+test it, we can invoke Sail interactively using the \verb|-i| option,
+passing the above file on the command line. Typing
+\verb|replicate_bits(3, 0xA)| will step through the execution of the
+above function, and eventually return the result \verb|0xAAA|. Typing
+\verb|:run| in the interactive interpreter will cause the expression
+to be evaluated fully, rather than stepping through the execution.
+
+Sail allows type variables to be used directly within expressions, so
+the above could be re-written as \mrbfnmyreplicatebitstwo This
+notation can be succinct, but should be used with caution. What
+happens is that Sail will try to re-write the type variables using
+expressions of the appropriate size that are available within the
+surrounding scope, in this case \ll{n} and \ll{length(xs)}. If no
+suitable expressions are found to trivially rewrite these type
+variables, then additional function parameters will be automatically
+added to pass around this information at runtime. This feature is
+however very useful for implementing functions with implicit
+parameters, e.g. we can implement a zero extension function that
+implicitly picks up its result length from the calling context as
+follows:
+\mrbextzz
+\mrbfnextzz
+
+Notice that we annotated the \ll{val} declaration as a
+\ll{cast}---this means that the type checker is allowed to
+automatically insert it where needed in order to make our code type
+check. This is another feature that must be used carefully, because
+too many implicit casts can quickly result in unreadable code. Sail
+does not make any distinction between expressions and statements, so
+since there is only a single line of code within the foreach block, we
+can drop it and simply write: \mrbfnmyreplicatebitsthree
+
+\subsection{Numeric Types}
+
+Sail has three basic numeric types, \ll{int}, \ll{nat}, and
+\ll{range}. The type \ll{int} is an arbitrary precision mathematical
+integer, and likewise \ll{nat} is an arbitrary precision natural
+number. The type \ll{range('n,'m)} is an inclusive range between the
+\ll{Int}-kinded type variables \ll{'n} and \ll{'m}. The type
+\ll{int('o)} is an integer exactly equal to the \ll{Int}-kinded type
+variable \ll{'n}, i.e. \ll{int('o)} $=$ \ll{range('o,'o)}. These types
+can be used interchangably provided the rules summarised in the below
+diagram are satisfied (via constraint solving).
+
+\begin{center}
+\begin{tikzpicture}
+  [type/.style={rectangle},auto,>=stealth',semithick]
+  \node[type] (int) at (0, 3) {\ll{int}};
+  \node[type] (nat) at (3, 0) {\ll{nat}};
+  \node[type] (range) at (-3, 0) {\ll{range('n,'m)}};
+  \node[type] (atom) at (0, -3) {\ll{int('o)}};
+
+  \draw[->] (nat) -- (int);
+  \draw[->] (range) -- (int);
+  \draw[->] (atom) to [bend left=10] node {} (int);
+  \draw[->] (range) to node {\ll{'n} $\ge$ \ll{0}} (nat);
+  \draw[->] (atom) to node {\ll{'o} $\ge$ \ll{0}} (nat);
+  \draw[->] (atom) to [bend right=35] node {\ll{'n} $\le$ \ll{'o} $\le$ \ll{'m}} (range);
+  \draw[->] (range) to [bend right=35] node [swap] {\ll{'n} $=$ \ll{'m} $=$ \ll{'o}} (atom);
+\end{tikzpicture}
+\end{center}
+
+Note that \ll{bit} isn't a numeric type (i.e. it's not
+\ll{range(0,1)}. This is intentional, as otherwise it would be
+possible to write expressions like \ll{(1 : bit) + 5} which would end
+up being equal to \ll{6 : range(5, 6)}. This kind of implicit casting
+from bits to other numeric types would be highly undesirable.
+
+\subsection{Vector Type}
+
+Sail has the builtin type vector, which is a polymorphic type for
+fixed-length vectors. For example, we could define a vector \ll{v} of
+three integers as follows:
+\begin{lstlisting}
+let v : vector(3, dec, int) = [1, 2, 3]
+\end{lstlisting}
+The first argument of the vector type is a numeric expression
+representing the length of the vector, and the last is the type of the
+vector's elements. But what is the second argument? Sail allows two
+different types of vector orderings---increasing (\ll{inc}) and
+decreasing (\ll{dec}). These two orderings are shown for the bitvector
+0b10110000 below.
+
+\begin{center}
+\begin{tikzpicture}[scale=0.7]
+  \draw (0,0) rectangle (1,1) node[pos=.5] {1};
+  \draw (1,0) rectangle (2,1) node[pos=.5] {0};
+  \draw (2,0) rectangle (3,1) node[pos=.5] {1};
+  \draw (3,0) rectangle (4,1) node[pos=.5] {1};
+  \draw (4,0) rectangle (5,1) node[pos=.5] {0};
+  \draw (5,0) rectangle (6,1) node[pos=.5] {0};
+  \draw (6,0) rectangle (7,1) node[pos=.5] {0};
+  \draw (7,0) rectangle (8,1) node[pos=.5] {0};
+
+  \node at (.5,1.5) {0};
+  \node at (7.5,1.5) {7};
+  \draw[->] (1.5,1.5) -- (6.5,1.5);
+  \node at (.5,-0.5) {MSB};
+  \node at (7.5,-0.5) {LSB};
+  \node at (4,2) {\ll{inc}};
+\end{tikzpicture}
+\qquad
+\begin{tikzpicture}[scale=0.7]
+  \draw (0,0) rectangle (1,1) node[pos=.5] {1};
+  \draw (1,0) rectangle (2,1) node[pos=.5] {0};
+  \draw (2,0) rectangle (3,1) node[pos=.5] {1};
+  \draw (3,0) rectangle (4,1) node[pos=.5] {1};
+  \draw (4,0) rectangle (5,1) node[pos=.5] {0};
+  \draw (5,0) rectangle (6,1) node[pos=.5] {0};
+  \draw (6,0) rectangle (7,1) node[pos=.5] {0};
+  \draw (7,0) rectangle (8,1) node[pos=.5] {0};
+
+  \node at (.5,1.5) {7};
+  \node at (7.5,1.5) {0};
+  \draw[->] (1.5,1.5) -- (6.5,1.5);
+  \node at (.5,-0.5) {MSB};
+  \node at (7.5,-0.5) {LSB};
+  \node at (4,2) {\ll{dec}};
+\end{tikzpicture}
+\end{center}
+
+For increasing (bit)vectors, the 0 index is the most significant bit
+and the indexing increases towards the least significant bit. Whereas
+for decreasing (bit)vectors the least significant bit is 0 indexed,
+and the indexing decreases from the most significant to the least
+significant bit. For this reason, increasing indexing is sometimes
+called `most significant bit is zero' or MSB0, while decreasing
+indexing is sometimes called `least significant bit is zero' or
+LSB0. While this vector ordering makes most sense for bitvectors (it
+is usually called bit-ordering), in Sail it applies to all
+vectors. A default ordering can be set using
+\begin{lstlisting}
+default Order dec
+\end{lstlisting}
+and this should usually be done right at the beginning of a
+specification. Most architectures stick to either convention or the
+other, but Sail also allows functions which are polymorphic over
+vector order, like so:
+\begin{lstlisting}
+val foo : forall ('a : Order). vector(8, 'a, bit) -> vector(8, 'a, bit)
+\end{lstlisting}
+
+\paragraph{Bitvector Literals}
+
+Bitvector literals in Sail are written as either
+\lstinline[mathescape]{0x$\textit{hex string}$} or
+\lstinline[mathescape]{0b$\textit{binary string}$}, for example
+\ll{0x12FE} or \ll{0b1010100}. The length of a hex literal is always
+four times the number of digits, and the length of binary string is
+always the exact number of digits, so \ll{0x12FE} has length 16, while
+\ll{0b1010100} has length 7.
+
+\paragraph{Accessing and Updating Vectors}
+
+A vector can be indexed by using the
+\lstinline[mathescape]{$\textit{vector}$[$\textit{index}$]}
+notation. So, in the following code:
+\begin{lstlisting}
+  let v : vector(4, dec, int) = [1, 2, 3, 4]
+  let a = v[0]
+  let b = v[3]
+\end{lstlisting}
+\ll{a} will be \ll{4}, and \ll{b} will be \ll{1} (not that \ll{v} is
+\ll{dec}). By default, Sail will statically check for out of bounds
+errors, and will raise a type error if it cannot prove that all such
+vector accesses are valid.
+
+Vectors can be sliced using the
+%
+\lstinline[mathescape]{$\textit{vector}$[$\textit{index}_{msb}$ .. $\textit{index}_{lsb}$]}
+%
+notation. The indexes are always supplied with the index closest to
+the MSB being given first, so we would take the bottom 32-bits of a
+decreasing bitvector \ll{v} as \ll{v[31 .. 0]}, and the upper 32-bits
+of an increasing bitvector as \ll{v[0 .. 31]}, i.e. the indexing order
+for decreasing vectors decreases, and the indexing order for
+increasing vectors increases.
+
+A vector index can be updated using
+\lstinline[mathescape]{[$\textit{vector}$ with $\textit{index}$ = $\textit{expression}$]}
+notation.
+%
+Similarly, a subrange of a vector can be updated using
+%
+\lstinline[mathescape]{[$\textit{vector}$ with $\textit{index}_{msb}$ .. $\textit{index}_{lsb}$ = $\textit{expression}$]},
+%
+where the order of the indexes is the same as described above for
+increasing and decreasing vectors.
+
+These expressions are actually just syntactic sugar for several
+builtin functions, namely \ll{vector_access}, \ll{vector_subrange},
+\ll{vector_update}, and \ll{vector_update_subrange}.
+
+\subsection{List Type}
+
+In addition to vectors, Sail also has \ll{list} as a builtin type. For
+example:
+\begin{lstlisting}
+let l : list(int) = [|1, 2, 3|]
+\end{lstlisting}
+The cons operator is \ll{::}, so we could equally write:
+\lstinputlisting{examples/list.sail}
+Pattern matching can be used to destructure lists, see Section~\ref{sec:pat}
+
+\subsection{Other Types}
+
+
+\subsection{Pattern Matching}
+\label{sec:pat}
+
+Like most functional languages, Sail supports pattern matching via the
+\ll{match} keyword. For example:
+\begin{lstlisting}
+let n : int = f();
+match n {
+  1 => print("1"),
+  2 => print("2"),
+  3 => print("3"),
+  _ => print("wildcard")
+}
+\end{lstlisting}
+The \ll{match} keyword takes an expression and then branches using a
+pattern based on its value. Each case in the match expression takes
+the form \lstinline[mathescape]{$\textit{pattern}$ => $\textit{expression}$},
+separated by commas. The cases are checked sequentially from top to
+bottom, and when the first pattern matches its expression will be
+evaluated.
+
+\ll{match} in Sail is not currently check for exhaustiveness---after
+all we could have arbitrary constraints on a numeric variable being
+matched upon, which would restrict the possible cases in ways that we
+could not determine with just a simple syntactic check. However, there
+is a simple exhaustiveness checker which runs and gives warnings (not
+errors) if it cannot tell that the pattern match is exhaustive, but
+this check can give false positives. It can be turned off with the
+\verb+-no_warn+ flag.
+
+When we match on numeric literals, the type of the variable we are
+matching on will be adjusted. In the above example in the
+\ll{print("1")} case, $n$ will have the type \ll{int('e)}, where
+\ll{'e} is some fresh type variable, and there will be a constraint
+that \ll{'e} is equal to one.
+
+We can also have guards on patterns, for example we could modify the
+above code to have an additional guarded case like so:
+\begin{lstlisting}
+let n : int = f();
+match n {
+  1 => print("1"),
+  2 => print("2"),
+  3 => print("3"),
+  m if m <= 10 => print("n is less than or equal to 10"),
+  _ => print("wildcard")
+}
+\end{lstlisting}
+The variable pattern m will match against anything, and the guard can
+refer to variables bound by the pattern.
+
+\paragraph{Matching on enums}
+
+Match can be used to match on possible values of an enum, like so:
+\begin{lstlisting}
+enum E = A | B | C
+
+match x {
+  A => print("A"),
+  B => print("B"),
+  C => print("C")
+}
+\end{lstlisting}
+Note that because Sail places no restrictions on the lexical structure
+of enumeration elements to differentiate them from ordinary
+identifiers, pattern matches on variables and enum elements can be
+somewhat ambiguous. This is the primary reason why we have the basic,
+but incomplete, pattern exhaustiveness check mentioned above---it can
+warn you if removing an enum constructor breaks a pattern match.
+
+\paragraph{Matching on unions}
+
+Match can also be used to destructure union constructors, for example
+using the option type from Section~\ref{sec:union}:
+\begin{lstlisting}
+match option {
+  Some(x) => foo(x),
+  None()  => print("matched None()")
+}
+\end{lstlisting}
+Note that like how calling a function with a unit argument can be done
+as \ll{f()} rather than \ll{f(())}, matching on a constructor \ll{C}
+with a unit type can be acheived by using \ll{C()} rather than
+\ll{C(())}.
+
+\paragraph{Matching on bit vectors}
+
+Sail allows numerous ways to match on bitvectors, for example:
+\begin{lstlisting}
+match v {
+  0xFF => print("hex match"),
+  0x0000_0001 => print("binary match"),
+  0xF @ v : bits(4) => print("vector concatentation pattern"),
+  0xF @ [bitone, _, b1, b0] => print("vector pattern"),
+  _ : bits(4) @ v : bits(4) => print("annotated wildcard pattern")
+}
+\end{lstlisting}
+We can match on bitvector literals in either hex or binary forms. We
+also have vector concatantion patterns, of the form
+\lstinline[mathescape]{$\mathit{pattern}$ @ $\ldots$ @ $\mathit{pattern}$}.
+We must be able to infer the length of all the subpatterns in a vector
+concatentation pattern, hence why in the example above all the
+wildcard and variable patterns beneath vector concatenation patterns
+have type annotations. In the context of a pattern the \ll{:} operator
+binds tighter than the \ll{@} operator (as it does elsewhere).
+
+We also have vector patterns, which for bitvectors match on individual
+bits. In the above example, \ll{b0} and \ll{b1} will have type
+\ll{bit}. The pattern \ll{bitone} is a bit literal, with \ll{bitzero}
+being the other bit literal pattern.
+
+Note that because vectors in sail are type-polymorphic, we can also
+use both vector concatentation patterns and vector patterns to match
+against non-bit vectors.
+
+\paragraph{Matching on lists}
+
+Sail allows lists to be destructured using patterns. There are two
+types of patterns for lists, cons patterns and list literal patterns.
+
+\begin{lstlisting}
+match ys {
+  x :: xs => print("cons pattern"),
+  [||]    => print("empty list")
+}
+\end{lstlisting}
+
+\begin{lstlisting}
+match ys {
+  [|1, 2, 3|] => print("list pattern"),
+  _           => print("wildcard")
+}
+\end{lstlisting}
+
+\paragraph{As patterns}
+
+\subsection{Mutable and Immutable Variables}
+
+\subsection{Type declarations}
+
+\subsubsection{Enumerations}
+
+Enumerations can be defined in either a Haskell-like syntax
+(useful for smaller enums) or a more traditional C-like syntax, which
+is often more readable for enumerations with more members. There are
+no lexical constraints on the identifiers that can be part of an
+enumeration. There are also no restrictions on the name of a
+enumeration type, other than it must be a valid identifier. For
+example, the following shows two ways to define the enumeration
+\ll{Foo} with three members, \ll{Bar}, \ll{Baz}, and \ll{quux}:
+
+\lstinputlisting{examples/enum1.sail}
+\lstinputlisting{examples/enum2.sail}
+
+For every enumeration type $E$ sail generates a
+\lstinline[mathescape]{num_of_$E$} function and a
+\lstinline[mathescape]{$E$_of_num} function, which for \ll{Foo} above
+will have the following definitions\footnote{It will ensure that the
+  generated function name \ll{arg} does not clash with any enumeration
+  constructor.}:
+\begin{lstlisting}
+val Foo_of_num : forall 'e, 0 <= 'e <= 2. int('e) -> Foo
+function Foo_of_num(arg) = match arg {
+  0 => Bar,
+  1 => Baz,
+  _ => quux
+}
+
+val num_of_Foo : Foo -> {'e, 0 <= 'e <= 2. int('e)}
+function num_of_Foo(arg) = match arg {
+  Bar  => 0,
+  Baz  => 1,
+  quux => 2
+}
+\end{lstlisting}
+Note that these functions are not automatically made into implicit
+casts.
+
+\subsubsection{Structs}
+
+Structs are defined using the struct keyword like so:
+\lstinputlisting{examples/struct.sail}
+
+If we have a struct \ll{foo : Foo}, its fields can be accessed by
+\ll{foo.bar}, and set as \ll{foo.bar = 0xF}. It can also be updated in
+a purely functional fashion using the construct \ll{\{foo with bar =
+  0xF\}}. There is no lexical restriction on the name of a struct or
+the names of its fields.
+
+\subsubsection{Unions}
+\label{sec:union}
+
+As an example, the \ll{maybe} type \'{a} la Haskell could be defined
+in Sail as follows:
+\begin{lstlisting}
+union maybe ('a : Type) = {
+  Just : 'a,
+  None : unit
+}
+\end{lstlisting}
+Constructors, such as \ll{Just} are called like functions, as in
+\ll{Just(3) : maybe(int)}. The \ll{None} constructor is also called in
+this way, as \ll{None()}. Notice that unlike in other languages, every
+constructor must be associated with a type---there are no nullary
+constructors. As with structs there are no lexical restrictions on the
+names of either the constructors nor the type itself, other than they
+must be valid identifiers.
+
+\subsubsection{Bitfields}
+
+The following example creates a bitfield type called \ll{cr} and a
+register \ll{CR} of that type.
+
+\lstinputlisting{examples/bitfield.sail}
+
+A bitfield definition creates a wrapper around a bit vector type, and
+generates getters and setters for the fields. For the setters, it is
+assumed that they are being used to set registers with the bitfield
+type\footnote{This functionality was originally called \emph{register
+    types} for this reason, but this was confusing because types of
+  registers are not always register types.}. If the bitvector is
+decreasing then indexes for the fields must also be in decreasing
+order, and vice-versa for an increasing vector. For the above example,
+the bitfield wrapper type will be the following:
+
+\begin{lstlisting}
+union cr = { Mk_cr(vector(8, dec, bit)) }
+\end{lstlisting}
+
+The complete vector can be accessed as \ll{CR.bits()}, and a register
+of type \ll{cr} can be set like \ll{CR->bits() = 0xFF}. Getting and
+setting individual fields can be done similarly, as \ll{CR.CR0()} and
+\ll{CR->CR0() = 0xF}. Internally, the bitfield definition will
+generate a \lstinline[mathescape]{_get_$F$} and
+\lstinline[mathescape]{_set_$F$} function for each field
+\lstinline[mathescape]{$F$}, and then overload them as
+\lstinline[mathescape]{_mod_$F$} for the accessor syntax. The setter
+takes the bitfield as a reference to a register, hence why we use the
+\ll{->} notation. For pure updates of values of type \ll{cr} a
+function \lstinline[mathescape]{update_$F$} is also defined. For more
+details on getters and setters, see Section~\ref{sec:getset}. A
+singleton bit in a bitfield definition, such as \ll{LT : 7} will be
+defined as a bitvector of length one, and not as a value of type
+\ll{bit}, which mirrors the behavior of ARM's ASL language.
+
+\subsection{Operators}
+
+Valid operators in Sail are sequences of the following non
+alpha-numeric characters: \verb#!%&*+-./:<>=@^|#. Additionally, any
+such sequence may be suffixed by an underscore followed by any valid
+identifier, so \verb#<=_u# or even \verb#<=_unsigned# are valid
+operator names. Operators may be left, right, or non-associative, and
+there are 10 different precedence levels, ranging from 0 to 9, with 9
+binding the tightest. To declare the precedence of an operator, we use a fixity declaration like:
+\begin{lstlisting}
+infix <=_u 4
+\end{lstlisting}
+For left or right associative operators, we'd use the keywords
+\ll{infixl} or \ll{infixr} respectively. An operator can be used
+anywhere a normal identifier could be used via the \ll{operator}
+keyword. As such, the \verb#<=_u# operator can be defined as:
+\begin{lstlisting}
+val operator <=_u : forall 'n. (bits('n), bits('n)) -> bool
+function operator <=_u(x, y) = unsigned(x) <= unsigned(y)
+\end{lstlisting}
+
+\paragraph{Builtin precedences}
+The precedence of several common operators are built into Sail. These
+include all the operators that are used in type-level numeric
+expressions, as well as several common operations such as equality,
+division, and modulus. The precedences for these operators are
+summarised in Table~\ref{tbl:operators}.
+
+\begin{table}[hbt]
+  \center
+  \begin{tabular}{| c || l | l | l |}
+    \hline
+    Precedence & Left associative & Non-associative & Right associative\\
+    \hline
+    9 & & &\\
+    \hline
+    8 & & & \ll{^}\\
+    \hline
+    7 & \ll{*}, \ll{/}, \ll{\%} & &\\
+    \hline
+    6 & \ll{+}, \ll{-} & &\\
+    \hline
+    5 & & &\\
+    \hline
+    4 & & \ll{<}, \ll{<=}, \ll{>}, \ll{>=}, \ll{!=}, \ll{=}, \ll{==} &\\
+    \hline
+    3 & & & \ll{&}\\
+    \hline
+    2 & & & \ll{|}\\
+    \hline
+    1 & & &\\
+    \hline
+    0 & & &\\
+    \hline
+  \end{tabular}
+  \caption{Default Sail operator precedences}
+  \label{tbl:operators}
+\end{table}
+
+\paragraph{Type operators}
+Sail allows operators to be used at the type level. For example, we
+could define a synonym for the builtin \ll{range} type as:
+\lstinputlisting{examples/type_operator.sail} Note that we can't use
+\ll{..} as an operator name, because that is reserved syntax for
+vector slicing. Operators used in types always share precedence with
+identically named operators at the expression level.
+
+\subsection{Ad-hoc Overloading}
+
+\subsection{Getters and Setters}
+\label{sec:getset}
+
+\subsection{Sizeof and Constraint}
+
+\subsection{Preludes and Default Environment}
+\label{sec:prelude}
diff --git a/doc/usage.tex b/doc/usage.tex
new file mode 100644
index 00000000..12095822
--- /dev/null
+++ b/doc/usage.tex
@@ -0,0 +1,165 @@
+\section{Using Sail}
+\label{sec:usage}
+
+In its most basic use-case Sail is a command-line tool, analogous to
+a compiler: one gives it a list of input Sail files; it type-checks
+them and provides translated output.
+
+To simply typecheck Sail files, one can pass them on the command line
+with no other options, so for our \riscv\ spec:
+\begin{verbatim}
+sail prelude.sail riscv_types.sail riscv_sys.sail riscv.sail
+\end{verbatim}
+The sail files passed on the command line are simply treated as if
+they are one large file concatentated together, although the parser
+will keep track of locations on a per-file basis for
+error-reporting. As can be seen, this specification is split into
+several logical components. \verb+prelude.sail+ defines the initial
+type environment and builtins, \verb+riscv_types.sail+ gives type
+definitions used in the rest of the specification and then
+\verb+riscv_sys.sail+ and \verb+riscv.sail+ implement most of the
+specification.
+
+For more complex projects, once can use \ll{$include} statments in
+Sail source, for example: \TODO{use \# like C}
+\begin{lstlisting}
+$include <library.sail>
+$include "file.sail"
+\end{lstlisting}
+
+Here, Sail will look for \verb+library.sail+ in the
+\verb+$SAIL_DIR/lib+, where \verb+$SAIL_DIR+ is usually the root of
+the sail repository. It will search for \verb+file.sail+ relative to
+the location of the file containing the \ll{$include}. The space after
+the include is mandatory. Sail also supports \ll{$define},
+\ll{$ifdef}, and \ll{$ifndef}. These are things that are understood by
+Sail itself, not a separate preprocessor, and are handled after the
+AST is parsed~\footnote{This can affect precedence declarations for custom user defined operators---the precedence must be redeclared in the file you are including the operator into.}.
+
+\subsection{OCaml compilation}
+
+To compile a sail specification into OCaml, one calls Sail as
+\begin{verbatim}
+sail -ocaml FILES
+\end{verbatim}
+This will produce a version of the specification translated into
+Ocaml, which is placed into a directory called \verb+_sbuild+, similar
+to ocamlbuild's \verb+_build+ directory. The generated OCaml is
+intended to be fairly close to the original Sail source, and currently
+we do not attempt to do much optimisation on this output.
+
+The contents of the \verb+_sbuild+ directory are set up as an
+ocamlbuild project, so one can simply switch into that directory and run
+\begin{verbatim}
+ocamlbuild -use-ocamlfind out.cmx
+\end{verbatim}
+to compile the generated model. Currently the OCaml compilation
+requires that lem, linksem, and zarith are available as ocamlfind
+findable libraries, and also that the environment variable
+\verb+$SAIL_DIR+ is set to the root of the Sail repository.
+
+If the Sail specification contains a \ll{main} function with type
+\ll{unit -> unit} that implements a fetch/decode/execute loop then the
+OCaml backend can produce a working executable, by running
+\begin{verbatim}
+sail -o out -ocaml FILES
+\end{verbatim}
+Then one can run
+\begin{verbatim}
+./out ELF_FILE
+\end{verbatim}
+to simulate an ELF file on the specification. One can do \ll{$include
+  <elf.sail>} to gain access to some useful functions for accessing
+information about the loaded ELF file from within the Sail
+specification. In particular \verb+elf.sail+ defines a function
+\ll{elf_entry : unit -> int} which can be used to set the PC to the
+correct location. ELF loading is done by the linksem
+library\footnote{\url{https://github.com/rems-project/linksem}}.
+
+There is also an \verb+-ocaml_trace+ option which instruments the
+generated OCaml code with tracing information this option implies \verb+-ocaml+.
+
+\subsection{C compilation}
+
+WIP but basically like OCaml
+
+\subsection{Lem embedding}
+
+\TODO{Document generating lem}
+
+\subsection{Interactive mode}
+
+Compiling sail with
+\begin{verbatim}
+make isail
+\end{verbatim}
+builds it with a GHCi-style interactive interpreter. This can be used
+by starting Sail with \verb+sail -i+. If sail is not compiled with
+interactive support the \verb+-i+ flag does nothing. Sail will still
+handle any other command line arguments as per usual, including
+compiling to OCaml or Lem. One can also pass a list of commands to the
+interpreter by using the \verb+-is+ flag, as
+\begin{verbatim}
+sail -is FILE
+\end{verbatim}
+where \verb+FILE+ contains a list of commands. Once inside the interactive
+mode, a list of commands can be accessed by typing \verb+:commands+,
+while \verb+:help+ can be used to provide some documentation for each
+command.
+
+\subsection{Other options}
+
+Here we summarize most of the other options available for
+Sail. Debugging options (usually for debugging Sail itself) are
+indicated by starting with the letter d.
+
+\begin{itemize}
+\item {\verb+-v+} Print the Sail version.
+
+\item {\verb+-help+} Print a list of options.
+
+\item {\verb+-no_warn+} Turn off warnings.
+
+\item {\verb+-enum_casts+} Allow elements of enumerations to be
+  automatically casted to numbers.
+
+\item \verb+-memo_z3+ Memoize calls to the Z3 solver. This can greatly
+  improve typechecking times if you are repeatedly typechecking the
+  same specification while developing it.
+
+\item \verb+-no_effects+ Turn off effect checking. May break some
+  backends that assume effects are properly checked.
+
+\item \verb+-undefined_gen+ Generate functions that create undefined
+  values of user-defined types. Every type \ll{T} will get a
+  \ll{undefined_T} function created for it. This flag is set
+  automatically by some backends that want to re-write \ll{undefined}.
+
+\item \verb+-just_check+ Force Sail to terminate immediately after
+  typechecking.
+
+\item \verb+-dno_cast+ Force Sail to never perform type coercions
+  under any circumstances.
+
+\item \verb+-dtc_verbose <verbosity>+ Make the typechecker print a
+  trace of typing judgements. If the verbosity level is 1, then this
+  should only include fairly readable judgements about checking and
+  inference rules. If verbosity is 2 then it will include a large
+  amount of debugging information. This option can be useful to
+  diagnose tricky type-errors, especially if the error message isn't
+  very good.
+
+\item \verb+-ddump_tc_ast+ Write the typechecked AST to stdout after
+  typechecking
+
+\item \verb+-ddump_rewrite_ast <prefix>+ Write the AST out after each
+  re-writing pass. The output from each pass is placed in a file
+  starting with \verb+prefix+.
+
+\item \verb+-dsanity+ Perform extra sanity checks on the AST.
+
+\item \verb+-dmagic_hash+ Allow the \# symbol in identifiers. It's
+  currently used as a magic symbol to separate generated identifiers
+  from those the user can write, so this option allows for the output
+  of the various other debugging options to be fed back into Sail.
+\end{itemize}