From a13db0459877d7b35459b722249d9a020fb09d3a Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Wed, 25 Jan 2023 10:56:43 +1100 Subject: [PATCH] lib: README.md files for the new sessions Signed-off-by: Gerwin Klein --- lib/Basics/README.md | 16 ++++++++++++++++ lib/Eisbach_Tools/README.md | 19 +++++++++++++++++++ lib/ML_Utils/README.md | 15 +++++++++++++++ lib/Monads/README.md | 38 +++++++++++++++++++++++++++++++++++++ 4 files changed, 88 insertions(+) create mode 100644 lib/Basics/README.md create mode 100644 lib/Eisbach_Tools/README.md create mode 100644 lib/ML_Utils/README.md create mode 100644 lib/Monads/README.md diff --git a/lib/Basics/README.md b/lib/Basics/README.md new file mode 100644 index 000000000..6b952d50b --- /dev/null +++ b/lib/Basics/README.md @@ -0,0 +1,16 @@ + + +# Basic Library Theories + +This session contains basic library theories that are needed in other sessions +of this repository, such as [Monads] or [CParser], but that we do not want to +put into these sessions to avoid circular session dependencies. + +Dependencies on `Word_Lib` and the Isabelle distribution (e.g. `HOL-Libary`) are +fine, but avoid introducing any further session dependencies. + +[Monads]: ../Monads/ +[CParser]: ../../tools/c-parser diff --git a/lib/Eisbach_Tools/README.md b/lib/Eisbach_Tools/README.md new file mode 100644 index 000000000..9999b46a2 --- /dev/null +++ b/lib/Eisbach_Tools/README.md @@ -0,0 +1,19 @@ + + +# Eisbach and Tactic Tools + +This session contains tools and tactics for defining Isabelle [Eisbach] methods. + +Some of the theories in this session are not strictly speaking Eisbach-related, +but are mostly used from Eisbach methods, so we collect them here as well. + +We only include theories that are needed in the [Monads], [CParser], and +[AutoCorres] sessions. + +[Eisbach]: https://isabelle.in.tum.de/dist//doc/eisbach.pdf +[Monads]: ../Monads/ +[CParser]: ../../tools/c-parser/ +[AutoCorres]: ../../tools/autocorres/ diff --git a/lib/ML_Utils/README.md b/lib/ML_Utils/README.md new file mode 100644 index 000000000..d29e6f7f7 --- /dev/null +++ b/lib/ML_Utils/README.md @@ -0,0 +1,15 @@ + + +# Isabelle/ML Utilities + +`ML_Utils` is a collection of 'basic' ML utilities (similar to +`~~/src/Pure/library.ML`}). If you find yourself implementing: + +- a simple data-structure-shuffling task, +- something that shows up in the standard library of other functional languages, or +- something that's "missing" from the general pattern of an Isabelle ML library, + +consider adding it here. diff --git a/lib/Monads/README.md b/lib/Monads/README.md new file mode 100644 index 000000000..d5b13a843 --- /dev/null +++ b/lib/Monads/README.md @@ -0,0 +1,38 @@ + + +# Monad Definitions and Tactics + +This session contains definitions of various monads useful in [AutoCorres] and +the [seL4 verification][l4v] for the verification of C programs. + +In particular, this session defines: + +- a [nondeterministic state monad][nondet] with failure to express stateful + computation. There is a variation of this monad that also allows computation + with exceptions (throw/catch). + +- a [reader option monad][option] to express computation that can depend on + state and can fail, but does not change state. It can also be used to express + projections from the state in preconditions and other state assertions. + +- a [trace monad][trace] that stores a set of traces for expressing concurrent + computation. + +- for each of these monads, weakest-precondition lemmas and corresponding tool + setup. + +- for the nondeterministic state monad, additional concepts such as + wellformedness with respect to failure (`empty_fail`), absence of failure + (`no_fail`), absence of exceptions (`no_throw`). See the respective theories + for more details. + +The directory [`wp/`](./wp/) contains proof methods to reason about these monads +in weakest-precondition style. + +[l4v]: https://github.com/seL4/l4v/ +[nondet]: ./NonDetMonad.thy +[option]: ./OptionMonad.thy +[trace]: ./TraceMonad.thy