Katamaran
Katamaran is a verification framework for instruction set architectures in the
Rocq proof assistant.
It provides the deeply-embedded language μSail, a variant
of the Sail language, for the
specification of instructions sets and provides furthermore facilities for the
specification of separation logic-based contracts and for semi-automatically
verifying these contracts. The goal is to formally specify and verify with
machine-checked proofs critical security guarantees of instruction sets. For
more information visit our website.
Dependencies
The development version of Katamaran is tested with Rocq 9.2 and 9.3 and has the following lower bounds:
rocq-core >= 9.2
rocq-equations >= 1.3.2+9.2
rocq-iris >= 4.5
rocq-stdpp >= 1.13
Using opam
An easy way to setup your system is to create a fresh opam switch, pin the Rocq and Iris versions and install equations (stdpp will be installed as a dependency of Iris):
opam switch create katamaran ocaml-base-compiler.5.2.1
opam repo add rocq-released https://rocq-prover.org/opam/released
opam pin add rocq-core 9.2.0
opam pin add rocq-iris 4.5.0
opam pin add rocq-equations 1.3.2+9.2
Using nix
The repository contains a flake.nix file that defines development shells that install all dependencies. To use it, you need to have nix installed. Then, you can enter a development shell with the following command:
nix develop
This will install all dependencies and open a shell with them available. Additionally it will set the COQPATH environment variable to include the dependencies. You can then compile the project within that shell or launch your favorite editor from within it.
There is also an lsp development shell with editor tooling: nix develop .#lsp. With direnv, .envrc loads the default shell; to load the lsp shell instead, create a .envrc.local containing use flake .#lsp (it is not committed).
Installation
Via opam (dev version)
Add our opam repository and install the latest development version from Github
with the following commands:
opam repo add katamaran https://github.com/katamaran-project/opam-repository.git
opam install coq-katamaran
From github
git clone https://github.com/katamaran-project/katamaran.git
cd katamaran && make && make install
Using
The basic usage structure of Katamaran is described in the USING.md file.
The easiest and recommended way to use the library for new developments is to adapt one of our existing case studies, for example the MinimalCaps machine.
Some more information about the internal structure of the library is provided in the HACKING.md file.
License
The Katamaran implementation is distributed under the 2-clause BSD license.
