Merge branch 'sail2' into mappings

(involved some manual tinkering with gitignore, type_check, riscv)

7 files changed, 339 insertions, 0 deletions

diff --git a/lib/hol/.gitignore b/lib/hol/.gitignore
new file mode 100644
index 00000000..fe652801
--- /dev/null
+++ b/lib/hol/.gitignore
@@ -0,0 +1,9 @@
+prompt_monadScript.sml
+promptScript.sml
+sail_instr_kindsScript.sml
+sail_operators_bitlistsScript.sml
+sail_operators_mwordsScript.sml
+sail_operatorsScript.sml
+sail_valuesScript.sml
+state_monadScript.sml
+stateScript.sml
diff --git a/lib/hol/Holmakefile b/lib/hol/Holmakefile
new file mode 100644
index 00000000..eac4fec8
--- /dev/null
+++ b/lib/hol/Holmakefile
@@ -0,0 +1,32 @@
+LEM_SCRIPTS = sail_instr_kindsScript.sml sail_valuesScript.sml sail_operatorsScript.sml \
+  sail_operators_mwordsScript.sml sail_operators_bitlistsScript.sml \
+  state_monadScript.sml stateScript.sml promptScript.sml prompt_monadScript.sml
+
+LEM_CLEANS = $(LEM_SCRIPTS)
+
+SCRIPTS = $(LEM_SCRIPTS) \
+  sail_valuesAuxiliaryScript.sml stateAuxiliaryScript.sml
+
+THYS = $(patsubst %Script.sml,%Theory.uo,$(SCRIPTS))
+
+LEMDIR=../../../lem/hol-lib
+
+INCLUDES = $(LEMDIR)
+
+all: $(THYS)
+.PHONY: all
+
+EXTRA_CLEANS = $(LEM_CLEANS)
+
+ifdef POLY
+HOLHEAP = sail-heap
+EXTRA_CLEANS = $(LEM_CLEANS) $(HOLHEAP) $(HOLHEAP).o
+
+BASE_HEAP = $(LEMDIR)/lemheap
+
+$(HOLHEAP): $(BASE_HEAP)
+	$(protect $(HOLDIR)/bin/buildheap) -o $(HOLHEAP) -b $(BASE_HEAP)
+
+all: $(HOLHEAP)
+
+endif
diff --git a/lib/hol/Makefile b/lib/hol/Makefile
new file mode 100644
index 00000000..065f887a
--- /dev/null
+++ b/lib/hol/Makefile
@@ -0,0 +1,31 @@
+LEMSRC =  \
+  ../../src/lem_interp/sail_instr_kinds.lem \
+  ../../src/gen_lib/sail_values.lem \
+  ../../src/gen_lib/sail_operators.lem \
+  ../../src/gen_lib/sail_operators_mwords.lem \
+  ../../src/gen_lib/sail_operators_bitlists.lem \
+  ../../src/gen_lib/state_monad.lem \
+  ../../src/gen_lib/state.lem \
+  prompt_monad.lem \
+  prompt.lem
+
+SCRIPTS = sail_instr_kindsScript.sml sail_valuesScript.sml sail_operatorsScript.sml \
+  sail_operators_mwordsScript.sml sail_operators_bitlistsScript.sml \
+  state_monadScript.sml stateScript.sml \
+  prompt_monadScript.sml promptScript.sml
+
+THYS = $(patsubst %Script.sml,%Theory.uo,$(SCRIPTS))
+
+all: sail-heap $(THYS)
+
+$(SCRIPTS): $(LEMSRC)
+	lem -hol -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $(LEMSRC)
+
+$(THYS) sail-heap: $(SCRIPTS)
+	Holmake
+
+# Holmake will also clear out the generated $(SCRIPTS) files
+clean:
+	Holmake cleanAll
+
+.PHONY: all clean
diff --git a/lib/hol/prompt.lem b/lib/hol/prompt.lem
new file mode 100644
index 00000000..edbd3752
--- /dev/null
+++ b/lib/hol/prompt.lem
@@ -0,0 +1,18 @@
+open import Prompt_monad
+open import State_monad
+open import State
+
+let inline undefined_bool = undefined_boolS
+let inline bool_of_bitU_oracle = bool_of_bitU_oracleS
+let inline bool_of_bitU_fail = bool_of_bitU_fail
+let inline bools_of_bits_oracle = bools_of_bits_oracleS
+let inline of_bits_oracle = of_bits_oracleS
+let inline of_bits_fail = of_bits_failS
+let inline mword_oracle = mword_oracleS
+let inline reg_deref = read_regS
+
+let inline foreachM = foreachS
+let inline whileM = whileS
+let inline untilM = untilS
+let inline and_boolM = and_boolS
+let inline or_boolM = or_boolS
diff --git a/lib/hol/prompt_monad.lem b/lib/hol/prompt_monad.lem
new file mode 100644
index 00000000..8fcd645a
--- /dev/null
+++ b/lib/hol/prompt_monad.lem
@@ -0,0 +1,49 @@
+open import Pervasives_extra
+open import Sail_instr_kinds
+open import Sail_values
+open import State_monad
+
+(* Fake interface of the prompt monad by redirecting to the state monad, since
+   the former is not currently supported by HOL4 *)
+
+type monad 'rv 'a 'e = monadS 'rv 'a 'e
+type monadR 'rv 'a 'e 'r = monadRS 'rv 'a 'e 'r
+
+(* We need to use a target_rep for these because HOL doesn't handle unused
+   type parameters well. *)
+
+type base_monad 'regval 'regstate 'a 'e = monad 'regstate 'a 'e
+declare hol target_rep type base_monad 'regval 'regstate 'a 'e = `monad` 'regstate 'a 'e
+type base_monadR 'regval 'regstate 'a 'r 'e = monadR 'regstate 'a 'r 'e
+declare hol target_rep type base_monadR 'regval 'regstate 'a 'r 'e = `monadR` 'regstate 'a 'r 'e
+
+let inline return = returnS
+let inline bind = bindS
+let inline (>>=) = (>>$=)
+let inline (>>) = (>>$)
+
+let inline exit = exitS
+
+let inline throw = throwS
+let inline try_catch = try_catchS
+
+let inline catch_early_return = catch_early_returnS
+let inline early_return = early_returnS
+let inline liftR = liftRS
+let inline try_catchR = try_catchRS
+
+let inline maybe_fail = maybe_failS
+
+let inline read_mem_bytes = read_mem_bytesS
+let inline read_reg = read_regS
+let inline reg_deref = read_regS
+let inline read_mem = read_memS
+let inline read_tag = read_tagS
+let inline excl_result = excl_resultS
+let inline write_reg = write_regS
+let inline write_tag = write_tagS
+let inline write_mem_ea wk addr sz = write_mem_eaS wk addr (nat_of_int sz)
+let inline write_mem_val = write_mem_valS
+let barrier _ = return ()
+
+let inline assert_exp = assert_expS
diff --git a/lib/hol/sail_valuesAuxiliaryScript.sml b/lib/hol/sail_valuesAuxiliaryScript.sml
new file mode 100644
index 00000000..aa169979
--- /dev/null
+++ b/lib/hol/sail_valuesAuxiliaryScript.sml
@@ -0,0 +1,139 @@
+(*Generated by Lem from ../../src/gen_lib/sail_values.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_pervasives_extraTheory lem_machine_wordTheory sail_valuesTheory;
+open intLib;
+
+val _ = numLib.prefer_num();
+
+
+
+open lemLib;
+(* val _ = lemLib.run_interactive := true; *)
+val _ = new_theory "sail_valuesAuxiliary"
+
+
+(****************************************************)
+(*                                                  *)
+(* Termination Proofs                               *)
+(*                                                  *)
+(****************************************************)
+
+(* val gst = Defn.tgoal_no_defn (shr_int_def, shr_int_ind) *)
+val (shr_int_rw, shr_int_ind_rw) =
+  Defn.tprove_no_defn ((shr_int_def, shr_int_ind),
+    WF_REL_TAC`measure (Num o SND)` \\ COOPER_TAC
+  )
+val shr_int_rw = save_thm ("shr_int_rw", shr_int_rw);
+val shr_int_ind_rw = save_thm ("shr_int_ind_rw", shr_int_ind_rw);
+val () = computeLib.add_persistent_funs["shr_int_rw"];
+
+
+(* val gst = Defn.tgoal_no_defn (shl_int_def, shl_int_ind) *)
+val (shl_int_rw, shl_int_ind_rw) =
+  Defn.tprove_no_defn ((shl_int_def, shl_int_ind),
+    WF_REL_TAC`measure (Num o SND)` \\ COOPER_TAC
+  )
+val shl_int_rw = save_thm ("shl_int_rw", shl_int_rw);
+val shl_int_ind_rw = save_thm ("shl_int_ind_rw", shl_int_ind_rw);
+val () = computeLib.add_persistent_funs["shl_int_rw"];
+
+
+(* val gst = Defn.tgoal_no_defn (repeat_def, repeat_ind) *)
+val (repeat_rw, repeat_ind_rw) =
+  Defn.tprove_no_defn ((repeat_def, repeat_ind),
+    WF_REL_TAC`measure (Num o SND)` \\ COOPER_TAC
+  )
+val repeat_rw = save_thm ("repeat_rw", repeat_rw);
+val repeat_ind_rw = save_thm ("repeat_ind_rw", repeat_ind_rw);
+val () = computeLib.add_persistent_funs["repeat_rw"];
+
+
+(* val gst = Defn.tgoal_no_defn (bools_of_nat_aux_def, bools_of_nat_aux_ind) *)
+val (bools_of_nat_aux_rw, bools_of_nat_aux_ind_rw) =
+  Defn.tprove_no_defn ((bools_of_nat_aux_def, bools_of_nat_aux_ind),
+    WF_REL_TAC`measure (Num o FST)` \\ COOPER_TAC
+  )
+val bools_of_nat_aux_rw = save_thm ("bools_of_nat_aux_rw", bools_of_nat_aux_rw);
+val bools_of_nat_aux_ind_rw = save_thm ("bools_of_nat_aux_ind_rw", bools_of_nat_aux_ind_rw);
+val () = computeLib.add_persistent_funs["bools_of_nat_aux_rw"];
+
+
+(* val gst = Defn.tgoal_no_defn (pad_list_def, pad_list_ind) *)
+val (pad_list_rw, pad_list_ind_rw) =
+  Defn.tprove_no_defn ((pad_list_def, pad_list_ind),
+    WF_REL_TAC`measure (Num o SND o SND)` \\ COOPER_TAC
+  )
+val pad_list_rw = save_thm ("pad_list_rw", pad_list_rw);
+val pad_list_ind_rw = save_thm ("pad_list_ind_rw", pad_list_ind_rw);
+val () = computeLib.add_persistent_funs["pad_list_rw"];
+
+
+(* val gst = Defn.tgoal_no_defn (reverse_endianness_list_def, reverse_endianness_list_ind) *)
+val (reverse_endianness_list_rw, reverse_endianness_list_ind_rw) =
+  Defn.tprove_no_defn ((reverse_endianness_list_def, reverse_endianness_list_ind),
+    WF_REL_TAC`measure LENGTH` \\ rw[drop_list_def,nat_of_int_def]
+  )
+val reverse_endianness_list_rw = save_thm ("reverse_endianness_list_rw", reverse_endianness_list_rw);
+val reverse_endianness_list_ind_rw = save_thm ("reverse_endianness_list_ind_rw", reverse_endianness_list_ind_rw);
+val () = computeLib.add_persistent_funs["reverse_endianness_list_rw"];
+
+
+(* val gst = Defn.tgoal_no_defn (index_list_def, index_list_ind) *)
+val (index_list_rw, index_list_ind_rw) =
+  Defn.tprove_no_defn ((index_list_def, index_list_ind),
+    WF_REL_TAC`measure (λ(x,y,z). Num(1+(if z > 0 then int_max (-1) (y - x) else int_max (-1) (x - y))))`
+    \\ rw[integerTheory.INT_MAX]
+    \\ intLib.COOPER_TAC
+  )
+val index_list_rw = save_thm ("index_list_rw", index_list_rw);
+val index_list_ind_rw = save_thm ("index_list_ind_rw", index_list_ind_rw);
+val () = computeLib.add_persistent_funs["index_list_rw"];
+
+
+(*
+(* val gst = Defn.tgoal_no_defn (while_def, while_ind) *)
+val (while_rw, while_ind_rw) =
+  Defn.tprove_no_defn ((while_def, while_ind),
+    cheat (* the termination proof *)
+  )
+val while_rw = save_thm ("while_rw", while_rw);
+val while_ind_rw = save_thm ("while_ind_rw", while_ind_rw);
+*)
+
+
+(*
+(* val gst = Defn.tgoal_no_defn (until_def, until_ind) *)
+val (until_rw, until_ind_rw) =
+  Defn.tprove_no_defn ((until_def, until_ind),
+    cheat (* the termination proof *)
+  )
+val until_rw = save_thm ("until_rw", until_rw);
+val until_ind_rw = save_thm ("until_ind_rw", until_ind_rw);
+*)
+
+
+(****************************************************)
+(*                                                  *)
+(* Lemmata                                          *)
+(*                                                  *)
+(****************************************************)
+
+val just_list_spec = store_thm("just_list_spec",
+``((! xs. (just_list xs = NONE) <=> MEM NONE xs) /\
+   (! xs es. (just_list xs = SOME es) <=> (xs = MAP SOME es)))``,
+  (* Theorem: just_list_spec*)
+  conj_tac
+  \\ ho_match_mp_tac just_list_ind
+  \\ Cases \\ rw[]
+  \\ rw[Once just_list_def]
+  >- ( CASE_TAC \\ fs[] \\ CASE_TAC )
+  >- PROVE_TAC[]
+  \\ Cases_on`es` \\ fs[]
+  \\ CASE_TAC \\ fs[]
+  \\ CASE_TAC \\ fs[]
+);
+
+
+
+val _ = export_theory()
+
diff --git a/lib/hol/stateAuxiliaryScript.sml b/lib/hol/stateAuxiliaryScript.sml
new file mode 100644
index 00000000..c8269750
--- /dev/null
+++ b/lib/hol/stateAuxiliaryScript.sml
@@ -0,0 +1,61 @@
+(*Generated by Lem from ../../src/gen_lib/state.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_pervasives_extraTheory sail_valuesTheory state_monadTheory stateTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+open lemLib;
+(* val _ = lemLib.run_interactive := true; *)
+val _ = new_theory "stateAuxiliary"
+
+
+(****************************************************)
+(*                                                  *)
+(* Termination Proofs                               *)
+(*                                                  *)
+(****************************************************)
+
+(* val gst = Defn.tgoal_no_defn (iterS_aux_def, iterS_aux_ind) *)
+val (iterS_aux_rw, iterS_aux_ind_rw) =
+  Defn.tprove_no_defn ((iterS_aux_def, iterS_aux_ind),
+    WF_REL_TAC`measure (LENGTH o SND o SND)` \\ rw[]
+  )
+val iterS_aux_rw = save_thm ("iterS_aux_rw", iterS_aux_rw);
+val iterS_aux_ind_rw = save_thm ("iterS_aux_ind_rw", iterS_aux_ind_rw);
+
+
+(* val gst = Defn.tgoal_no_defn (foreachS_def, foreachS_ind) *)
+val (foreachS_rw, foreachS_ind_rw) =
+  Defn.tprove_no_defn ((foreachS_def, foreachS_ind),
+    WF_REL_TAC`measure (LENGTH o FST)` \\ rw[]
+  )
+val foreachS_rw = save_thm ("foreachS_rw", foreachS_rw);
+val foreachS_ind_rw = save_thm ("foreachS_ind_rw", foreachS_ind_rw);
+
+
+(*
+These are unprovable.
+
+(* val gst = Defn.tgoal_no_defn (whileS_def, whileS_ind) *)
+val (whileS_rw, whileS_ind_rw) =
+  Defn.tprove_no_defn ((whileS_def, whileS_ind),
+    cheat (* the termination proof *)
+  )
+val whileS_rw = save_thm ("whileS_rw", whileS_rw);
+val whileS_ind_rw = save_thm ("whileS_ind_rw", whileS_ind_rw);
+
+
+(* val gst = Defn.tgoal_no_defn (untilS_def, untilS_ind) *)
+val (untilS_rw, untilS_ind_rw) =
+  Defn.tprove_no_defn ((untilS_def, untilS_ind),
+    cheat (* the termination proof *)
+  )
+val untilS_rw = save_thm ("untilS_rw", untilS_rw);
+val untilS_ind_rw = save_thm ("untilS_ind_rw", untilS_ind_rw);
+*)
+
+
+val _ = export_theory()
+