diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/hol/.gitignore | 9 | ||||
| -rw-r--r-- | lib/hol/Holmakefile | 32 | ||||
| -rw-r--r-- | lib/hol/Makefile | 31 | ||||
| -rw-r--r-- | lib/hol/prompt.lem | 18 | ||||
| -rw-r--r-- | lib/hol/prompt_monad.lem | 49 | ||||
| -rw-r--r-- | lib/hol/sail_valuesAuxiliaryScript.sml | 132 | ||||
| -rw-r--r-- | lib/isabelle/Makefile | 5 | ||||
| -rw-r--r-- | lib/isabelle/State_lemmas.thy | 10 | ||||
| -rw-r--r-- | lib/isabelle/manual/Manual.thy | 2 | ||||
| -rw-r--r-- | lib/mono_rewrites.sail | 157 |
10 files changed, 438 insertions, 7 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..6698e210 --- /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 + +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): + $(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..af3f56c5 --- /dev/null +++ b/lib/hol/sail_valuesAuxiliaryScript.sml @@ -0,0 +1,132 @@ +(*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 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 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 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 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 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 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 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/isabelle/Makefile b/lib/isabelle/Makefile index f8786321..b10dde78 100644 --- a/lib/isabelle/Makefile +++ b/lib/isabelle/Makefile @@ -1,6 +1,6 @@ THYS = Sail_instr_kinds.thy Sail_values.thy Sail_operators.thy \ Sail_operators_mwords.thy Sail_operators_bitlists.thy \ - State_monad.thy State.thy Prompt_monad.thy Prompt.thy + State_monad.thy State.thy State_lifting.thy Prompt_monad.thy Prompt.thy EXTRA_THYS = State_monad_lemmas.thy State_lemmas.thy Prompt_monad_lemmas.thy \ Sail_operators_mwords_lemmas.thy Hoare.thy @@ -51,5 +51,8 @@ State_monad.thy: ../../src/gen_lib/state_monad.lem Sail_values.thy State.thy: ../../src/gen_lib/state.lem Prompt.thy State_monad.thy State_monad_lemmas.thy lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< +State_lifting.thy: ../../src/gen_lib/state_lifting.lem Prompt.thy State.thy + lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< + clean: -rm $(THYS) diff --git a/lib/isabelle/State_lemmas.thy b/lib/isabelle/State_lemmas.thy index 84b08e6c..253c21b9 100644 --- a/lib/isabelle/State_lemmas.thy +++ b/lib/isabelle/State_lemmas.thy @@ -1,5 +1,5 @@ theory State_lemmas - imports State + imports State State_lifting begin lemma All_liftState_dom: "liftState_dom (r, m)" @@ -44,12 +44,12 @@ lemma liftState_catch_early_return[simp]: by (auto simp: catch_early_return_def catch_early_returnS_def sum.case_distrib cong: sum.case_cong) lemma liftState_liftR[simp]: - "liftState r (liftR m) = liftSR (liftState r m)" - by (auto simp: liftR_def liftSR_def) + "liftState r (liftR m) = liftRS (liftState r m)" + by (auto simp: liftR_def liftRS_def) lemma liftState_try_catchR[simp]: - "liftState r (try_catchR m h) = try_catchSR (liftState r m) (liftState r \<circ> h)" - by (auto simp: try_catchR_def try_catchSR_def sum.case_distrib cong: sum.case_cong) + "liftState r (try_catchR m h) = try_catchRS (liftState r m) (liftState r \<circ> h)" + by (auto simp: try_catchR_def try_catchRS_def sum.case_distrib cong: sum.case_cong) lemma liftState_read_mem_BC: assumes "unsigned_method BC_bitU_list (bits_of_method BCa a) = unsigned_method BCa a" diff --git a/lib/isabelle/manual/Manual.thy b/lib/isabelle/manual/Manual.thy index 6cdfbfa1..51591531 100644 --- a/lib/isabelle/manual/Manual.thy +++ b/lib/isabelle/manual/Manual.thy @@ -288,7 +288,7 @@ exception handler as arguments. The exception mechanism is also used to implement early returns by throwing and catching return values: A function body with one or more early returns of type @{typ 'a} (and exception type @{typ 'e}) is lifted to a monadic expression with exception type @{typ "('a + 'e)"} using -@{term liftSR}, such that an early return of the value @{term a} throws @{term "Inl a"}, and a +@{term liftRS}, such that an early return of the value @{term a} throws @{term "Inl a"}, and a regular exception @{term e} is thrown as @{term "Inr e"}. The function body is then wrapped in @{term catch_early_returnS} to lower it back to the default monad and exception type. These liftings and lowerings are automatically inserted by Sail for functions with early returns.\<^footnote>\<open>To be diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail new file mode 100644 index 00000000..c9164b6c --- /dev/null +++ b/lib/mono_rewrites.sail @@ -0,0 +1,157 @@ +/* Definitions for use with the -mono_rewrites option */ + +/* External definitions not in the usual asl prelude */ + +infix 6 << + +val shiftleft = "shiftl" : forall 'n ('ord : Order). + (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) effect pure + +overload operator << = {shiftleft} + +infix 6 >> + +val shiftright = "shiftr" : forall 'n ('ord : Order). + (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) effect pure + +overload operator >> = {shiftright} + +val arith_shiftright = "arith_shiftr" : forall 'n ('ord : Order). + (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) effect pure + +val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure +val extzv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure +function extzv(v) = extz_vec(sizeof('m),v) + +val "exts_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure +val extsv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure +function extsv(v) = exts_vec(sizeof('m),v) + +/* This is generated internally to deal with case splits which reveal the size + of a bitvector */ +val bitvector_cast = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure + +/* Definitions for the rewrites */ + +val slice_mask : forall 'n, 'n >= 0. (int, int) -> bits('n) effect pure +function slice_mask(i,l) = + let one : bits('n) = extzv(0b1) in + ((one << l) - one) << i + +val is_zero_subrange : forall 'n, 'n >= 0. + (bits('n), int, int) -> bool effect pure + +function is_zero_subrange (xs, i, j) = { + (xs & slice_mask(j, i-j)) == extzv(0b0) +} + +val is_ones_subrange : forall 'n, 'n >= 0. + (bits('n), int, int) -> bool effect pure + +function is_ones_subrange (xs, i, j) = { + let m : bits('n) = slice_mask(j,j-i) in + (xs & m) == m +} + +val slice_slice_concat : forall 'n 'm 'r, 'n >= 0 & 'm >= 0 & 'r >= 0. + (bits('n), int, int, bits('m), int, int) -> bits('r) effect pure + +function slice_slice_concat (xs, i, l, ys, i', l') = { + let xs = (xs & slice_mask(i,l)) >> i in + let ys = (ys & slice_mask(i',l')) >> i' in + extzv(xs) << l' | extzv(ys) +} + +val slice_zeros_concat : forall 'n 'p 'q 'r, 'r = 'p + 'q & 'n >= 0 & 'p >= 0 & 'q >= 0 & 'r >= 0. + (bits('n), int, atom('p), atom('q)) -> bits('r) effect pure + +function slice_zeros_concat (xs, i, l, l') = { + let xs = (xs & slice_mask(i,l)) >> i in + extzv(xs) << l' +} + +/* Assumes initial vectors are of equal size */ + +val subrange_subrange_eq : forall 'n, 'n >= 0. + (bits('n), int, int, bits('n), int, int) -> bool effect pure + +function subrange_subrange_eq (xs, i, j, ys, i', j') = { + let xs = (xs & slice_mask(j,i-j)) >> j in + let ys = (ys & slice_mask(j',i'-j')) >> j' in + xs == ys +} + +val subrange_subrange_concat : forall 'n 'o 'p 'm 'q 'r 's, 's = 'o - ('p - 1) + 'q - ('r - 1) & 'n >= 0 & 'm >= 0. + (bits('n), atom('o), atom('p), bits('m), atom('q), atom('r)) -> bits('s) effect pure + +function subrange_subrange_concat (xs, i, j, ys, i', j') = { + let xs = (xs & slice_mask(j,i-j)) >> j in + let ys = (ys & slice_mask(j',i'-j')) >> j' in + extzv(xs) << i' - (j' - 1) | extzv(ys) +} + +val place_subrange : forall 'n 'm, 'n >= 0 & 'm >= 0. + (bits('n), int, int, int) -> bits('m) effect pure + +function place_subrange(xs,i,j,shift) = { + let xs = (xs & slice_mask(j,i-j)) >> j in + extzv(xs) << shift +} + +val place_slice : forall 'n 'm, 'n >= 0 & 'm >= 0. + (bits('n), int, int, int) -> bits('m) effect pure + +function place_slice(xs,i,l,shift) = { + let xs = (xs & slice_mask(i,l)) >> i in + extzv(xs) << shift +} + +val zext_slice : forall 'n 'm, 'n >= 0 & 'm >= 0. + (bits('n), int, int) -> bits('m) effect pure + +function zext_slice(xs,i,l) = { + let xs = (xs & slice_mask(i,l)) >> i in + extzv(xs) +} + +val sext_slice : forall 'n 'm, 'n >= 0 & 'm >= 0. + (bits('n), int, int) -> bits('m) effect pure + +function sext_slice(xs,i,l) = { + let xs = arith_shiftright(((xs & slice_mask(i,l)) << ('n - i - l)), 'n - l) in + extsv(xs) +} + +/* This has different names in the aarch64 prelude (UInt) and the other + preludes (unsigned). To avoid variable name clashes, we redeclare it + here with a suitably awkward name. */ +val _builtin_unsigned = { + ocaml: "uint", + lem: "uint", + interpreter: "uint", + c: "sail_uint" +} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1) + +val unsigned_slice : forall 'n, 'n >= 0. + (bits('n), int, int) -> int effect pure + +function unsigned_slice(xs,i,l) = { + let xs = (xs & slice_mask(i,l)) >> i in + _builtin_unsigned(xs) +} + +val unsigned_subrange : forall 'n, 'n >= 0. + (bits('n), int, int) -> int effect pure + +function unsigned_subrange(xs,i,j) = { + let xs = (xs & slice_mask(j,i-j)) >> i in + _builtin_unsigned(xs) +} + + +val zext_ones : forall 'n, 'n >= 0. int -> bits('n) effect pure + +function zext_ones(m) = { + let v : bits('n) = extsv(0b1) in + v >> ('n - m) +} |