This directory contains snapshots of the Isabelle theories generated by Sail for the CHERI-MIPS, RISC-V, and ARM v8.3 specifications, together with snapshots of the Sail and Lem libraries. These snapshots are provided for convenience, and are not guaranteed to be up-to-date.
In order to open a theory of one of the specifications in Isabelle, use the -l Sail command-line flag to load the session containing the Sail library.
Snapshots of the Sail and Lem libraries are in the lib/sail and
lib/lem directories, respectively. The ROOTS file in this directory
contains pointers to them; you can tell Isabelle to use it with the -d flag,
as in
isabelle jedit -l Sail -d . riscv/Riscv.thy
This will open the RISC-V specification.
The file Manual.thy (and its PDF rendering in Manual.pdf) contains an introduction on how to use the Sail specifications in Isabelle.
The Lem library files in lib/lem have been generated from the
Lem sources. The Lem license can be
found in lib/lem/LICENSE.