diff options
| -rw-r--r-- | aarch64/Makefile | 2 | ||||
| -rwxr-xr-x | aarch64/mono/demo/mk | 2 | ||||
| -rw-r--r-- | cheri/Makefile | 2 | ||||
| -rw-r--r-- | lib/isabelle/manual/Manual.thy | 28 | ||||
| -rw-r--r-- | mips/Makefile | 2 | ||||
| -rw-r--r-- | riscv/Makefile | 4 |
6 files changed, 21 insertions, 19 deletions
diff --git a/aarch64/Makefile b/aarch64/Makefile index 07bc67ae..38900d5f 100644 --- a/aarch64/Makefile +++ b/aarch64/Makefile @@ -18,7 +18,7 @@ aarch64.lem: no_vector.sail aarch64_types.lem: aarch64.lem Aarch64.thy: aarch64_extras.lem aarch64_types.lem aarch64.lem - lem -isa -outdir . -lib $(SAIL_DIR)/src/gen_lib -lib $(SAIL_DIR)/src/lem_interp $^ + lem -isa -outdir . -lib Sail=$(SAIL_DIR)/src/gen_lib -lib Sail=$(SAIL_DIR)/src/lem_interp $^ LOC_FILES:=prelude.sail full/spec.sail decode_start.sail full/decode.sail decode_end.sail main.sail include ../etc/loc.mk diff --git a/aarch64/mono/demo/mk b/aarch64/mono/demo/mk index b7513edd..54c71977 100755 --- a/aarch64/mono/demo/mk +++ b/aarch64/mono/demo/mk @@ -5,5 +5,5 @@ set -ex -no_lexp_bounds_check -memo_z3 -undefined_gen \ -auto_mono -mono_rewrites -dall_split_errors -dmono_continue \ -lem -lem_mwords -lem_sequential -lem_lib Aarch64_extras -o aarch64_mono -lem -isa -lib ../../../src/gen_lib/ -lib ../../../src/lem_interp ../aarch64_extras.lem aarch64_mono_types.lem aarch64_mono.lem +lem -isa -lib "Sail=../../../src/gen_lib/" -lib "Sail=../../../src/lem_interp" ../aarch64_extras.lem aarch64_mono_types.lem aarch64_mono.lem isabelle jedit -d ~/local/rems/github/lem/isabelle-lib -d ../../../lib/isabelle -l Sail Aarch64_mono.thy diff --git a/cheri/Makefile b/cheri/Makefile index d1084dc0..89c8f1c7 100644 --- a/cheri/Makefile +++ b/cheri/Makefile @@ -111,7 +111,7 @@ cheri128.lem: $(CHERI128_SAILS) cheri128_types.lem: cheri128.lem C%.thy: c%.lem c%_types.lem $(MIPS_SAIL_DIR)/mips_extras.lem - lem -isa -outdir . -lib $(SAIL_DIR)/src/gen_lib -lib $(SAIL_DIR)/src/lem_interp $^ + lem -isa -outdir . -lib Sail=$(SAIL_DIR)/src/gen_lib -lib Sail=$(SAIL_DIR)/src/lem_interp $^ sed -i 's/datatype ast/datatype (plugins only: size) ast/' C$*_types.thy %Script.sml: %.lem %_types.lem $(MIPS_SAIL_DIR)/mips_extras.lem diff --git a/lib/isabelle/manual/Manual.thy b/lib/isabelle/manual/Manual.thy index 0d67f6c5..1ac300b4 100644 --- a/lib/isabelle/manual/Manual.thy +++ b/lib/isabelle/manual/Manual.thy @@ -60,10 +60,12 @@ This uses the following options: Isabelle definitions can then be generated by passing the @{verbatim "-isa"} flag to Lem. In order for Lem to find the Sail library, the subdirectories @{path "src/gen_lib"} and @{path "src/lem_interp"} of Sail will have to be added to Lem's include path using the -@{verbatim "-lib"} option, e.g. +@{verbatim "-lib"} option. In the following example, these directories are also associated with +the session name @{session Sail}, so that Lem generates import statements with session-qualified +theory names such as @{theory Sail.Hoare}. @{verbatim [display] -"lem -isa -outdir . -lib ../src/lem_interp -lib ../src/gen_lib +"lem -isa -outdir . -lib Sail=../src/lem_interp -lib Sail=../src/gen_lib riscv_extras.lem riscv_duopod_types.lem riscv_duopod.lem"} For further examples, see the @{path Makefile}s of the other specifications included in the Sail @@ -183,8 +185,8 @@ Vectors in Sail are mapped to lists in Isabelle, except for bitvectors, which ar Both increasing and decreasing indexing order are supported by having two versions for each operation that involves indexing, such as @{term update_list_inc} and @{term update_list_dec}, or @{term subrange_list_inc} and @{term subrange_list_dec}. These operations are defined in the -theory @{theory Sail2_values}, while @{theory Sail2_values_lemmas} provides simplification rules -such as +theory @{theory Sail.Sail2_values}, while @{theory Sail.Sail2_values_lemmas} provides simplification +rules such as @{lemma "access_list_inc xs i = xs ! nat i" by auto} \\ @{thm access_list_dec_nth} @@ -209,7 +211,7 @@ into multiple clauses with concrete bitvector lengths. This is not enabled by d so Sail generates Lem definitions using bit lists unless the @{verbatim "-lem_mwords"} command line flag is used. -The theory @{theory Sail2_values} defines a (Lem) typeclass @{verbatim Bitvector}, which provides +The theory @{theory Sail.Sail2_values} defines a (Lem) typeclass @{verbatim Bitvector}, which provides an interface to some basic bitvector operations and has instantiations for both bit lists and machine words. It is mainly intended for internal use in the Sail library,\<^footnote>\<open>Lem typeclasses are not very convenient to use in Isabelle, as they get translated to dictionaries that have to be passed to functions @@ -219,7 +221,7 @@ representations. For use in Sail specifications, wrappers are defined in the th right theory is automatically added to the generated files, depending on which bitvector representation is used. Hence, bitvector operations can be referred to in the Sail source code using uniform names, e.g.~@{term add_vec}, @{term update_vec_dec}, or @{term subrange_vec_inc}. -The theory @{theory Sail2_operators_mwords_lemmas} sets up simplification rules that relate these +The theory @{theory Sail.Sail2_operators_mwords_lemmas} sets up simplification rules that relate these operations to the native operations in Isabelle, e.g. @{lemma "add_vec l r = l + r" by simp} \\ @@ -235,9 +237,9 @@ for integration with relaxed memory models. For the sequential case, we use a s exceptions and nondeterminism). The generated definitions use the free monad, and the sequential case is supported via a lifting -to the state monad defined in the theory @{theory Sail2_state}. Simplification rules are set up in the -theory @{theory Sail2_state_lemmas}, allowing seamless reasoning about the generated definitions in terms -of the state monad.\<close> +to the state monad defined in the theory @{theory Sail.Sail2_state}. Simplification rules are set up +in the theory @{theory Sail.Sail2_state_lemmas}, allowing seamless reasoning about the generated +definitions in terms of the state monad.\<close> subsubsection \<open>State Monad \label{sec:state-monad}\<close> @@ -305,8 +307,8 @@ instances.\<close> subsubsection \<open>Free Monad \label{sec:free-monad}\<close> -text \<open>In addition to the state monad, the theory @{theory Sail2_prompt_monad} defines a free monad of an -effect datatype. A monadic expression either returns a pure value @{term a}, denoted +text \<open>In addition to the state monad, the theory @{theory Sail.Sail2_prompt_monad} defines a free +monad of an effect datatype. A monadic expression either returns a pure value @{term a}, denoted @{term "Done a"}, or it has an effect. The latter can be a failure or an exception, or an effect together with a continuation. For example, @{term \<open>Read_reg ''PC'' k\<close>} represents a request to read the register @{term PC} and continue as @{term k}, which is a function that takes the @@ -380,7 +382,7 @@ register state record: Sail aims to generate Isabelle definitions that can be used with either the state or the free monad. To achieve this, the definitions are generated using the free monad, and a lifting to the state monad is provided together with simplification rules. These include generic simplification rules -(proved in the theory @{theory Sail2_state_lemmas}) such as +(proved in the theory @{theory Sail.Sail2_state_lemmas}) such as @{thm [display] liftState_return[where r = "(get_regval, set_regval)"] liftState_bind[where r = "(get_regval, set_regval)"] @@ -400,7 +402,7 @@ section \<open>Example Proof \label{sec:ex-proof}\<close> text \<open>As a toy example for illustration, we prove that the add instruction in the RISC-V duopod actually performs an addition. We consider the sequential case and use the state monad. The -theory @{theory Hoare} defines (a shallow embedding of) a simple Hoare logic, where +theory @{theory Sail.Hoare} defines (a shallow embedding of) a simple Hoare logic, where @{term "PrePost P f Q"} denotes a triple of a precondition @{term P}, monadic expression @{term f}, and postcondition @{term Q}. Its validity is defined by @{thm [display] PrePost_def} diff --git a/mips/Makefile b/mips/Makefile index 03144f50..a156428a 100644 --- a/mips/Makefile +++ b/mips/Makefile @@ -55,7 +55,7 @@ COQ_LIBS = -R ../../bbv/theories bbv -R ../lib/coq Sail mips.vo: mips_types.vo mips_extras.vo M%.thy: m%.lem m%_types.lem mips_extras.lem - lem -isa -outdir . -lib $(SAIL_DIR)/src/gen_lib -lib $(SAIL_DIR)/src/lem_interp $^ + lem -isa -outdir . -lib Sail=$(SAIL_DIR)/src/gen_lib -lib Sail=$(SAIL_DIR)/src/lem_interp $^ sed -i 's/datatype ast/datatype (plugins only: size) ast/' M$*_types.thy %Script.sml: %.lem %_types.lem $(MIPS_SAIL_DIR)/mips_extras.lem diff --git a/riscv/Makefile b/riscv/Makefile index 6499fe7d..4d2baaf1 100644 --- a/riscv/Makefile +++ b/riscv/Makefile @@ -47,7 +47,7 @@ riscv_duopod_ocaml: prelude.sail riscv_duopod.sail riscv_duopod.lem: prelude.sail riscv_duopod.sail $(SAIL) $(SAIL_FLAGS) -lem -lem_mwords -lem_lib Riscv_extras -o riscv_duopod $^ Riscv_duopod.thy: riscv_duopod.lem riscv_extras.lem - lem -isa -outdir . -lib ../src/lem_interp -lib ../src/gen_lib \ + lem -isa -outdir . -lib Sail=../src/lem_interp -lib Sail=../src/gen_lib \ riscv_extras.lem \ riscv_duopod_types.lem \ riscv_duopod.lem @@ -55,7 +55,7 @@ Riscv_duopod.thy: riscv_duopod.lem riscv_extras.lem riscv_duopod: riscv_duopod_ocaml Riscv_duopod.thy Riscv.thy: riscv.lem riscv_extras.lem - lem -isa -outdir . -lib ../src/lem_interp -lib ../src/gen_lib \ + lem -isa -outdir . -lib Sail=../src/lem_interp -lib Sail=../src/gen_lib \ riscv_extras.lem \ riscv_types.lem \ riscv.lem |