From 0fe23222243bcadf6393d899e235ac35aaf57d63 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Tue, 10 Jul 2018 13:56:08 +0100 Subject: Add more Isabelle lemmas to library --- lib/isabelle/Hoare.thy | 131 +++++++++++++++++++++++ lib/isabelle/Sail2_operators_mwords_lemmas.thy | 57 ++++++++++ lib/isabelle/Sail2_prompt_monad_lemmas.thy | 41 ++++++++ lib/isabelle/Sail2_state_lemmas.thy | 109 ++++++++++++++++--- lib/isabelle/Sail2_values_lemmas.thy | 140 ++++++++++++++++++++++++- 5 files changed, 460 insertions(+), 18 deletions(-) diff --git a/lib/isabelle/Hoare.thy b/lib/isabelle/Hoare.thy index 88807c7c..76750117 100644 --- a/lib/isabelle/Hoare.thy +++ b/lib/isabelle/Hoare.thy @@ -253,6 +253,27 @@ lemma PrePostE_weaken_post: named_theorems PrePostE_compositeI named_theorems PrePostE_atomI +lemma PrePostE_conj_conds: + assumes "PrePostE P1 m Q1 E1" + and "PrePostE P2 m Q2 E2" + shows "PrePostE (\s. P1 s \ P2 s) m (\r s. Q1 r s \ Q2 r s) (\e s. E1 e s \ E2 e s)" + using assms by (auto intro: PrePostE_I elim: PrePostE_elim) + +lemmas PrePostE_conj_conds_consequence = PrePostE_conj_conds[THEN PrePostE_consequence] + +lemma PrePostE_post_mp: + assumes "PrePostE P m Q' E" + and "PrePostE P m (\r s. Q' r s \ Q r s) E" + shows "PrePostE P m Q E" + using PrePostE_conj_conds[OF assms] by (auto intro: PrePostE_weaken_post) + +lemma PrePostE_cong: + assumes "\s. P1 s \ P2 s" and "\s. P1 s \ m1 s = m2 s" and "\r s. Q1 r s \ Q2 r s" + and "\e s. E1 e s \ E2 e s" + shows "PrePostE P1 m1 Q1 E1 \ PrePostE P2 m2 Q2 E2" + using assms unfolding PrePostE_def PrePost_def + by (auto split: result.splits) + lemma PrePostE_True_post[PrePostE_atomI, intro, simp]: "PrePostE P m (\_ _. True) (\_ _. True)" unfolding PrePost_defs by (auto split: result.splits) @@ -320,6 +341,11 @@ lemma PrePostE_option_cases[PrePostE_compositeI]: shows "PrePostE (case x of Some a \ PS a | None \ PN) (case x of Some a \ s a | None \ n) Q E" using assms by (auto split: option.splits) +lemma PrePostE_sum_cases[PrePostE_compositeI]: + assumes "\a. PrePostE (Pl a) (l a) Q E" and "\b. PrePostE (Pr b) (r b) Q E" + shows "PrePostE (case x of Inl a \ Pl a | Inr b \ Pr b) (case x of Inl a \ l a | Inr b \ r b) Q E" + using assms by (auto split: sum.splits) + lemma PrePostE_let[PrePostE_compositeI]: assumes "PrePostE P (m y) Q E" shows "PrePostE P (let x = y in m x) Q E" @@ -347,10 +373,51 @@ lemma PrePostE_failS[PrePostE_atomI, intro]: "PrePostE (E (Failure msg)) (failS msg) Q E" unfolding PrePostE_def by (auto intro: PrePost_strengthen_pre) +lemma PrePostE_maybe_failS[PrePostE_atomI]: + "PrePostE (\s. case v of Some v \ Q v s | None \ E (Failure msg) s) (maybe_failS msg v) Q E" + by (auto simp: maybe_failS_def split: option.splits) + +lemma PrePostE_exitS[PrePostE_atomI, intro]: "PrePostE (E (Failure ''exit'')) (exitS msg) Q E" + unfolding exitS_def PrePostE_def PrePost_def failS_def by auto + lemma PrePostE_chooseS[intro, PrePostE_atomI]: "PrePostE (\s. \x \ xs. Q x s) (chooseS xs) Q E" unfolding PrePostE_def by (auto intro: PrePost_strengthen_pre) +lemma PrePostE_throwS[PrePostE_atomI]: "PrePostE (E (Throw e)) (throwS e) Q E" + by (intro PrePostE_I) (auto simp: throwS_def) + +lemma PrePostE_try_catchS[PrePostE_compositeI]: + assumes Ph: "\s e s'. (Ex (Throw e), s') \ m s \ PrePostE (Ph e) (h e) Q E" + and m: "PrePostE P m Q (\ex. case ex of Throw e \ Ph e | Failure msg \ E (Failure msg))" + shows "PrePostE P (try_catchS m h) Q E" + unfolding PrePostE_def +proof (intro PrePostI) + fix s r s' + assume "(r, s') \ try_catchS m h s" and P: "P s" + then show "(case r of Value a \ Q a | result.Ex e \ E e) s'" using m + proof (cases rule: try_catchS_cases) + case (h e s'') + then have "Ph e s''" using P m by (auto elim!: PrePostE_elim) + then show ?thesis using Ph[OF h(1)] h(2) by (auto elim!: PrePostE_elim) + qed (auto elim!: PrePostE_elim) +qed + +lemma PrePostE_catch_early_returnS[PrePostE_compositeI]: + assumes "PrePostE P m Q (\ex. case ex of Throw (Inl a) \ Q a | Throw (Inr e) \ E (Throw e) | Failure msg \ E (Failure msg))" + shows "PrePostE P (catch_early_returnS m) Q E" + unfolding catch_early_returnS_def + by (rule PrePostE_try_catchS, rule PrePostE_sum_cases[OF PrePostE_returnS PrePostE_throwS]) + (auto intro: assms) + +lemma PrePostE_early_returnS[PrePostE_atomI]: "PrePostE (E (Throw (Inl r))) (early_returnS r) Q E" + by (auto simp: early_returnS_def intro: PrePostE_throwS) + +lemma PrePostE_liftRS[PrePostE_compositeI]: + assumes "PrePostE P m Q (\ex. case ex of Throw e \ E (Throw (Inr e)) | Failure msg \ E (Failure msg))" + shows "PrePostE P (liftRS m) Q E" + using assms unfolding liftRS_def by (intro PrePostE_try_catchS[OF PrePostE_throwS]) + lemma PrePostE_foreachS_Cons: assumes "\s vars' s'. (Value vars', s') \ body x vars s \ PrePostE (Q vars') (foreachS xs vars' body) Q E" and "PrePostE (Q vars) (body x vars) Q E" @@ -363,6 +430,70 @@ lemma PrePostE_foreachS_invariant: using assms unfolding PrePostE_def by (intro PrePost_foreachS_invariant[THEN PrePost_strengthen_pre]) auto +lemma PrePostE_untilS: + assumes dom: "\s. Inv Q vars s \ untilS_dom (vars, cond, body, s)" + and cond: "\vars. PrePostE (Inv' Q vars) (cond vars) (\c s'. Inv Q vars s' \ (c \ Q vars s')) E" + and body: "\vars. PrePostE (Inv Q vars) (body vars) (Inv' Q) E" + shows "PrePostE (Inv Q vars) (untilS vars cond body) Q E" +proof (unfold PrePostE_def, rule PrePostI) + fix s r s' + assume Inv_s: "Inv Q vars s" and r: "(r, s') \ untilS vars cond body s" + with dom[OF Inv_s] cond body + show "(case r of Value a \ Q a | result.Ex e \ E e) s'" + proof (induction vars cond body s rule: untilS.pinduct[case_names Step]) + case (Step vars cond body s) + consider + (Value) vars' c sb sc where "(Value vars', sb) \ body vars s" and "(Value c, sc) \ cond vars' sb" + and "if c then r = Value vars' \ s' = sc else (r, s') \ untilS vars' cond body sc" + | (Ex) e where "(Ex e, s') \ bindS (body vars) cond s" and "r = Ex e" + using Step(1,6) + by (auto simp: untilS.psimps returnS_def Ex_bindS_iff elim!: bindS_cases split: if_splits; fastforce) + then show ?case + proof cases + case Value + then show ?thesis using Step.IH[OF Value(1,2) _ Step(3,4)] Step(3,4,5) + by (auto split: if_splits elim: PrePostE_elim) + next + case Ex + then show ?thesis using Step(3,4,5) by (auto elim!: bindS_cases PrePostE_elim) + qed + qed +qed + +lemma PrePostE_untilS_pure_cond: + assumes dom: "\s. Inv Q vars s \ untilS_dom (vars, returnS \ cond, body, s)" + and body: "\vars. PrePostE (Inv Q vars) (body vars) (\vars' s'. Inv Q vars' s' \ (cond vars' \ Q vars' s')) E" + shows "PrePostE (Inv Q vars) (untilS vars (returnS \ cond) body) Q E" + using assms by (intro PrePostE_untilS) (auto simp: comp_def) + +lemma PrePostE_liftState_untilM: + assumes dom: "\s. Inv Q vars s \ untilM_dom (vars, cond, body)" + and cond: "\vars. PrePostE (Inv' Q vars) (liftState r (cond vars)) (\c s'. Inv Q vars s' \ (c \ Q vars s')) E" + and body: "\vars. PrePostE (Inv Q vars) (liftState r (body vars)) (Inv' Q) E" + shows "PrePostE (Inv Q vars) (liftState r (untilM vars cond body)) Q E" +proof - + have domS: "untilS_dom (vars, liftState r \ cond, liftState r \ body, s)" if "Inv Q vars s" for s + using dom that by (intro untilM_dom_untilS_dom) + then have "PrePostE (Inv Q vars) (untilS vars (liftState r \ cond) (liftState r \ body)) Q E" + using cond body by (auto intro: PrePostE_untilS simp: comp_def) + moreover have "liftState r (untilM vars cond body) s = untilS vars (liftState r \ cond) (liftState r \ body) s" + if "Inv Q vars s" for s + unfolding liftState_untilM[OF domS[OF that] dom[OF that]] .. + ultimately show ?thesis by (auto cong: PrePostE_cong) +qed + +lemma PrePostE_liftState_untilM_pure_cond: + assumes dom: "\s. Inv Q vars s \ untilM_dom (vars, return \ cond, body)" + and body: "\vars. PrePostE (Inv Q vars) (liftState r (body vars)) (\vars' s'. Inv Q vars' s' \ (cond vars' \ Q vars' s')) E" + shows "PrePostE (Inv Q vars) (liftState r (untilM vars (return \ cond) body)) Q E" + using assms by (intro PrePostE_liftState_untilM) (auto simp: comp_def liftState_simp) + +lemma PrePostE_undefined_boolS[PrePostE_atomI]: + "PrePostE (\s. \b. Q b s) + (undefined_boolS unit) Q E" + unfolding undefined_boolS_def seqS_def + by (auto intro: PrePostE_strengthen_pre PrePostE_chooseS) + lemma PrePostE_bool_of_bitU_nondetS_any: "PrePostE (\s. \b. Q b s) (bool_of_bitU_nondetS b) Q E" unfolding bool_of_bitU_nondetS_def undefined_boolS_def diff --git a/lib/isabelle/Sail2_operators_mwords_lemmas.thy b/lib/isabelle/Sail2_operators_mwords_lemmas.thy index 2a6272c2..fd54c93a 100644 --- a/lib/isabelle/Sail2_operators_mwords_lemmas.thy +++ b/lib/isabelle/Sail2_operators_mwords_lemmas.thy @@ -78,6 +78,57 @@ lemma len_of_minus_One_minus_nonneg_lt_len_of[simp]: "n \ 0 \ nat (int LENGTH('a::len) - 1 - n) < LENGTH('a)" by (metis diff_mono diff_zero len_gt_0 nat_eq_iff2 nat_less_iff order_refl zle_diff1_eq) +declare subrange_vec_dec_def[simp] + +lemma update_subrange_vec_dec_update_subrange_list_dec: + assumes "0 \ j" and "j \ i" and "i < int LENGTH('a)" + shows "update_subrange_vec_dec (w :: 'a::len word) i j w' = + of_bl (update_subrange_list_dec (to_bl w) i j (to_bl w'))" + using assms + unfolding update_subrange_vec_dec_def update_subrange_list_dec_def update_subrange_list_inc_def + by (auto simp: word_update_def split_at_def Let_def nat_diff_distrib min_def) + +lemma subrange_vec_dec_subrange_list_dec: + assumes "0 \ j" and "j \ i" and "i < int LENGTH('a)" and "int LENGTH('b) = i - j + 1" + shows "subrange_vec_dec (w :: 'a::len word) i j = (of_bl (subrange_list_dec (to_bl w) i j) :: 'b::len word)" + using assms unfolding subrange_vec_dec_def + by (auto simp: subrange_list_dec_drop_take slice_take of_bl_drop') + +lemma slice_simp[simp]: "slice w lo len = Word.slice (nat lo) w" + by (auto simp: slice_def) + +declare slice_id[simp] + +lemma of_bools_of_bl[simp]: "of_bools_method BC_mword = of_bl" + by (auto simp: BC_mword_defs) + +lemma of_bl_bin_word_of_int: + "len = LENGTH('a) \ of_bl (bin_to_bl_aux len n []) = (word_of_int n :: ('a::len) word)" + by (auto simp: of_bl_def bin_bl_bin') + +lemma get_slice_int_0_bin_to_bl[simp]: + "len > 0 \ get_slice_int len n 0 = of_bl (bin_to_bl (nat len) n)" + unfolding get_slice_int_def get_slice_int_bv_def subrange_list_def + by (auto simp: subrange_list_dec_drop_take len_bin_to_bl_aux) + +lemma to_bl_of_bl[simp]: + fixes bl :: "bool list" + defines w: "w \ of_bl bl :: 'a::len word" + assumes len: "length bl = LENGTH('a)" + shows "to_bl w = bl" + using len unfolding w by (intro word_bl.Abs_inverse) auto + +lemma reverse_endianness_byte[simp]: + "LENGTH('a) = 8 \ reverse_endianness (w :: 'a::len word) = w" + unfolding reverse_endianness_def by (auto simp: reverse_endianness_list_simps) + +lemma reverse_reverse_endianness[simp]: + "8 dvd LENGTH('a) \ reverse_endianness (reverse_endianness w) = (w :: 'a::len word)" + unfolding reverse_endianness_def by (simp) + +lemma replicate_bits_zero[simp]: "replicate_bits 0 n = 0" + by (intro word_eqI) (auto simp: replicate_bits_def test_bit_of_bl rev_nth nth_repeat simp del: repeat.simps) + declare extz_vec_def[simp] declare exts_vec_def[simp] declare concat_vec_def[simp] @@ -109,4 +160,10 @@ lemma arith_vec_int_simps[simp]: unfolding add_vec_int_def sub_vec_int_def mult_vec_int_def by (auto simp: arith_op_bv_int_def BC_mword_defs word_add_def word_sub_wi word_mult_def) +lemma shiftl_simp[simp]: "shiftl w l = w << (nat l)" + by (auto simp: shiftl_def shiftl_mword_def) + +lemma shiftr_simp[simp]: "shiftr w l = w >> (nat l)" + by (auto simp: shiftr_def shiftr_mword_def) + end diff --git a/lib/isabelle/Sail2_prompt_monad_lemmas.thy b/lib/isabelle/Sail2_prompt_monad_lemmas.thy index 3ca1729f..25eb9f52 100644 --- a/lib/isabelle/Sail2_prompt_monad_lemmas.thy +++ b/lib/isabelle/Sail2_prompt_monad_lemmas.thy @@ -129,6 +129,16 @@ lemma bind_T_cases: | (Bind) m' where "s' = bind m' f" and "(m, e, m') \ T" using assms by (cases; blast elim: bind.elims) +lemma Run_bindI: + fixes m :: "('r, 'a, 'e) monad" + assumes "Run m t1 a1" + and "Run (f a1) t2 a2" + shows "Run (m \ f) (t1 @ t2) a2" +proof (use assms in \induction m t1 "Done a1 :: ('r, 'a, 'e) monad" rule: Traces.induct\) + case (Step s e s'' t) + then show ?case by (elim T.cases) auto +qed auto + lemma Run_bindE: fixes m :: "('rv, 'b, 'e) monad" and a :: 'a assumes "Run (bind m f) t a" @@ -161,6 +171,31 @@ lemma Run_DoneE: lemma Run_Done_iff_Nil[simp]: "Run (Done a) t a' \ t = [] \ a' = a" by (auto elim: Run_DoneE) +lemma Run_bindE_ignore_trace: + assumes "Run (m \ f) t a" + obtains tm tf am where "Run m tm am" and "Run (f am) tf a" + using assms by (elim Run_bindE) + +lemma Run_letE: + assumes "Run (let x = y in f x) t a" + obtains "Run (f y) t a" + using assms by auto + +lemma Run_ifE: + assumes "Run (if b then f else g) t a" + obtains "b" and "Run f t a" | "\b" and "Run g t a" + using assms by (auto split: if_splits) + +lemma Run_returnE: + assumes "Run (return x) t a" + obtains "t = []" and "a = x" + using assms by (auto simp: return_def) + +lemma Run_early_returnE: + assumes "Run (early_return x) t a" + shows P + using assms by (auto simp: early_return_def throw_def elim: Traces_cases) + lemma bind_cong[fundef_cong]: assumes m: "m1 = m2" and f: "\t a. Run m2 t a \ f1 a = f2 a" @@ -168,4 +203,10 @@ lemma bind_cong[fundef_cong]: unfolding m using f by (induction m2 f1 arbitrary: f2 rule: bind.induct; unfold bind.simps; blast) +lemma liftR_read_reg[simp]: "liftR (read_reg reg) = read_reg reg" by (auto simp: read_reg_def liftR_def split: option.splits) +lemma try_catch_return[simp]: "try_catch (return x) h = return x" by (auto simp: return_def) +lemma liftR_return[simp]: "liftR (return x) = return x" by (auto simp: liftR_def) +lemma liftR_undefined_bool[simp]: "liftR (undefined_bool ()) = undefined_bool ()" by (auto simp: undefined_bool_def liftR_def) +lemma assert_exp_True_return[simp]: "assert_exp True msg = return ()" by (auto simp: assert_exp_def return_def) + end diff --git a/lib/isabelle/Sail2_state_lemmas.thy b/lib/isabelle/Sail2_state_lemmas.thy index 8f04e850..ba69d0d8 100644 --- a/lib/isabelle/Sail2_state_lemmas.thy +++ b/lib/isabelle/Sail2_state_lemmas.thy @@ -23,21 +23,13 @@ lemma Value_liftState_Run: lemmas liftState_if_distrib[liftState_simp] = if_distrib[where f = "liftState ra" for ra] -lemma member_set_nth: - assumes "x \ set xs" - obtains n where "x = xs ! n" and "n < length xs" -proof (use assms in \induction xs arbitrary: thesis\) - case (Cons a xs) print_cases - show ?case proof cases - assume "x = a" - then show ?thesis using Cons(2)[where n = 0] Cons(3) by auto - next - assume "x \ a" - then obtain n where "x = xs ! n" and "n < length xs" using Cons by auto - then show ?thesis using Cons(2)[of "Suc n"] by auto - qed -qed auto +lemma Value_bindS_iff: + "(Value b, s'') \ bindS m f s \ (\a s'. (Value a, s') \ m s \ (Value b, s'') \ f a s')" + by (auto elim!: bindS_cases intro: bindS_intros) +lemma Ex_bindS_iff: + "(Ex e, s'') \ bindS m f s \ (Ex e, s'') \ m s \ (\a s'. (Value a, s') \ m s \ (Ex e, s'') \ f a s')" + by (auto elim!: bindS_cases intro: bindS_intros) lemma liftState_throw[liftState_simp]: "liftState r (throw e) = throwS e" by (auto simp: throw_def) @@ -67,7 +59,7 @@ lemma liftState_try_catch[liftState_simp]: by (induction m h rule: try_catch_induct) (auto simp: try_catchS_bindS_no_throw) lemma liftState_early_return[liftState_simp]: - "liftState r (early_return r) = early_returnS r" + "liftState r (early_return x) = early_returnS x" by (auto simp: early_return_def early_returnS_def liftState_simp) lemma liftState_catch_early_return[liftState_simp]: @@ -158,6 +150,68 @@ lemma liftState_internal_pick[liftState_simp]: simp del: repeat.simps cong: option.case_cong) +lemma liftRS_returnS[simp]: "liftRS (returnS x) = returnS x" + by (auto simp: liftRS_def) + +lemma liftRS_bindS: + fixes m :: "('regs, 'a, 'e) monadS" and f :: "'a \ ('regs, 'b, 'e) monadS" + shows "(liftRS (bindS m f) :: ('regs, 'b, 'r, 'e) monadRS) = bindS (liftRS m) (liftRS \ f)" +proof (intro ext set_eqI iffI) + fix s and rs' :: "('b, 'r + 'e) result \ 'regs sequential_state" + assume lhs: "rs' \ liftRS (bindS m f) s" + then show "rs' \ bindS (liftRS m) (liftRS \ f) s" + by (cases rs') + (fastforce simp: liftRS_def throwS_def elim!: bindS_cases try_catchS_cases + intro: bindS_intros try_catchS_intros) +next + fix s and rs' :: "('b, 'r + 'e) result \ 'regs sequential_state" + assume "rs' \ bindS (liftRS m) (liftRS \ f) s" + then show "rs' \ liftRS (bindS m f) s" + by (cases rs') + (fastforce simp: liftRS_def throwS_def elim!: bindS_cases try_catchS_cases + intro: bindS_intros try_catchS_intros) +qed + +lemma liftRS_assert_expS_True[simp]: "liftRS (assert_expS True msg) = returnS ()" + by (auto simp: liftRS_def assert_expS_def) + +lemma untilM_domI: + fixes V :: "'vars \ nat" + assumes "Inv vars" + and "\vars t vars' t'. \Inv vars; Run (body vars) t vars'; Run (cond vars') t' False\ \ V vars' < V vars \ Inv vars'" + shows "untilM_dom (vars, cond, body)" + using assms + by (induction vars rule: measure_induct_rule[where f = V]) + (auto intro: untilM.domintros) + +lemma untilM_dom_untilS_dom: + assumes "untilM_dom (vars, cond, body)" + shows "untilS_dom (vars, liftState r \ cond, liftState r \ body, s)" + using assms + by (induction vars cond body arbitrary: s rule: untilM.pinduct) + (rule untilS.domintros, auto elim!: Value_liftState_Run) + +lemma measure2_induct: + fixes f :: "'a \ 'b \ nat" + assumes "\x1 y1. (\x2 y2. f x2 y2 < f x1 y1 \ P x2 y2) \ P x1 y1" + shows "P x y" +proof - + have "P (fst x) (snd x)" for x + by (induction x rule: measure_induct_rule[where f = "\x. f (fst x) (snd x)"]) (auto intro: assms) + then show ?thesis by auto +qed + +lemma untilS_domI: + fixes V :: "'vars \ 'regs sequential_state \ nat" + assumes "Inv vars s" + and "\vars s vars' s' s''. + \Inv vars s; (Value vars', s') \ body vars s; (Value False, s'') \ cond vars' s'\ + \ V vars' s'' < V vars s \ Inv vars' s''" + shows "untilS_dom (vars, cond, body, s)" + using assms + by (induction vars s rule: measure2_induct[where f = V]) + (auto intro: untilS.domintros) + lemma whileS_dom_step: assumes "whileS_dom (vars, cond, body, s)" and "(Value True, s') \ cond vars s" @@ -262,6 +316,9 @@ lemma and_boolM_return_if: "and_boolM (return b) y = (if b then y else return False)" by (auto simp: and_boolM_def) +lemma and_boolM_return_return_and[simp]: "and_boolM (return l) (return r) = return (l \ r)" + by (auto simp: and_boolM_def) + lemmas and_boolM_if_distrib[simp] = if_distrib[where f = "\x. and_boolM x y" for y] lemma or_boolM_simps[simp]: @@ -275,6 +332,9 @@ lemma or_boolM_return_if: "or_boolM (return b) y = (if b then return True else y)" by (auto simp: or_boolM_def) +lemma or_boolM_return_return_or[simp]: "or_boolM (return l) (return r) = return (l \ r)" + by (auto simp: or_boolM_def) + lemmas or_boolM_if_distrib[simp] = if_distrib[where f = "\x. or_boolM x y" for y] lemma if_returnS_returnS[simp]: "(if a then returnS True else returnS False) = returnS a" by auto @@ -292,8 +352,12 @@ lemma and_boolS_returnS_if: lemmas and_boolS_if_distrib[simp] = if_distrib[where f = "\x. and_boolS x y" for y] +lemma and_boolS_returnS_True[simp]: "and_boolS (returnS True) c = c" + by (auto simp: and_boolS_def) + lemma or_boolS_simps[simp]: "or_boolS (returnS b) (returnS c) = returnS (b \ c)" + "or_boolS (returnS False) m = m" "or_boolS x (returnS True) = bindS x (\_. returnS True)" "or_boolS x (returnS False) = x" "\x y z. or_boolS (bindS x y) z = (bindS x (\r. or_boolS (y r) z))" @@ -305,4 +369,19 @@ lemma or_boolS_returnS_if: lemmas or_boolS_if_distrib[simp] = if_distrib[where f = "\x. or_boolS x y" for y] +lemma Run_or_boolM_E: + assumes "Run (or_boolM l r) t a" + obtains "Run l t True" and "a" + | tl tr where "Run l tl False" and "Run r tr a" and "t = tl @ tr" + using assms by (auto simp: or_boolM_def elim!: Run_bindE Run_ifE Run_returnE) + +lemma Run_and_boolM_E: + assumes "Run (and_boolM l r) t a" + obtains "Run l t False" and "\a" + | tl tr where "Run l tl True" and "Run r tr a" and "t = tl @ tr" + using assms by (auto simp: and_boolM_def elim!: Run_bindE Run_ifE Run_returnE) + +lemma maybe_failS_Some[simp]: "maybe_failS msg (Some v) = returnS v" + by (auto simp: maybe_failS_def) + end diff --git a/lib/isabelle/Sail2_values_lemmas.thy b/lib/isabelle/Sail2_values_lemmas.thy index b50d8942..576cd8ea 100644 --- a/lib/isabelle/Sail2_values_lemmas.thy +++ b/lib/isabelle/Sail2_values_lemmas.thy @@ -2,18 +2,135 @@ theory Sail2_values_lemmas imports Sail2_values begin +lemma while_domI: + fixes V :: "'vars \ nat" + assumes "\vars. cond vars \ V (body vars) < V vars" + shows "while_dom (vars, cond, body)" + by (induction vars rule: measure_induct_rule[where f = V]) + (use assms in \auto intro: while.domintros\) + lemma nat_of_int_nat_simps[simp]: "nat_of_int = nat" by (auto simp: nat_of_int_def) termination reverse_endianness_list by (lexicographic_order simp add: drop_list_def) +declare reverse_endianness_list.simps[simp del] +declare take_list_def[simp] +declare drop_list_def[simp] + +function take_chunks :: "nat \ 'a list \ 'a list list" where + "take_chunks n [] = []" +| "take_chunks 0 xs = []" +| "take_chunks n xs = take n xs # take_chunks n (drop n xs)" if "n > 0" and "xs \ []" + by auto blast +termination by lexicographic_order + +lemma take_chunks_length_leq_n: "length xs \ n \ xs \ [] \ take_chunks n xs = [xs]" + by (cases n) auto + +lemma take_chunks_append: "n dvd length a \ take_chunks n (a @ b) = take_chunks n a @ take_chunks n b" + by (induction n a rule: take_chunks.induct) (auto simp: dvd_imp_le) + +lemma Suc8_plus8: "Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc x))))))) = 8 + x" + by auto + +lemma byte_chunks_take_chunks_8: + assumes "8 dvd length xs" + shows "byte_chunks xs = Some (take_chunks 8 xs)" +proof - + have Suc8_plus8: "Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc x))))))) = 8 + x" for x + by auto + from assms show ?thesis + by (induction xs rule: byte_chunks.induct) (auto simp: Suc8_plus8 nat_dvd_not_less) +qed + +lemma reverse_endianness_list_rev_take_chunks: + "reverse_endianness_list bits = List.concat (rev (take_chunks 8 bits))" + by (induction "8 :: nat" bits rule: take_chunks.induct) + (auto simp: reverse_endianness_list.simps) + +lemma reverse_endianness_list_simps: + "length bits \ 8 \ reverse_endianness_list bits = bits" + "length bits > 8 \ reverse_endianness_list bits = reverse_endianness_list (drop 8 bits) @ take 8 bits" + by (cases bits; auto simp: reverse_endianness_list_rev_take_chunks)+ + +lemma reverse_endianness_list_append: + assumes "8 dvd length a" + shows "reverse_endianness_list (a @ b) = reverse_endianness_list b @ reverse_endianness_list a" + using assms by (auto simp: reverse_endianness_list_rev_take_chunks take_chunks_append) + +lemma length_reverse_endianness_list[simp]: + "length (reverse_endianness_list l) = length l" + by (induction l rule: reverse_endianness_list.induct) (auto simp: reverse_endianness_list.simps) + +lemma reverse_endianness_list_take_8[simp]: + "reverse_endianness_list (take 8 bits) = take 8 bits" + by (auto simp: reverse_endianness_list_simps) + +lemma reverse_reverse_endianness_list[simp]: + assumes "8 dvd length l" + shows "reverse_endianness_list (reverse_endianness_list l) = l" +proof (use assms in \induction l rule: reverse_endianness_list.induct[case_names Step]\) + case (Step bits) + then show ?case + by (auto simp: reverse_endianness_list.simps[of bits] reverse_endianness_list_append) +qed + +declare repeat.simps[simp del] + +lemma length_repeat[simp]: "length (repeat xs n) = nat n * length xs" +proof (induction xs n rule: repeat.induct[case_names Step]) + case (Step xs n) + then show ?case unfolding repeat.simps[of xs n] + by (auto simp del: mult_Suc simp: mult_Suc[symmetric]) +qed + +lemma nth_repeat: + assumes "i < nat n * length xs" + shows "repeat xs n ! i = xs ! (i mod length xs)" +proof (use assms in \induction xs n arbitrary: i rule: repeat.induct[case_names Step]\) + case (Step xs n i) + show ?case + using Step.prems Step.IH[of "i - length xs"] + unfolding repeat.simps[of xs n] + by (auto simp: nth_append mod_geq[symmetric] nat_diff_distrib diff_mult_distrib) +qed termination index_list by (relation "measure (\(i, j, step). nat ((j - i + step) * sgn step))") auto +lemma index_list_Zero[simp]: "index_list i j 0 = []" + by auto + +lemma index_list_singleton[simp]: "n \ 0 \ index_list i i n = [i]" + by auto + +lemma index_list_simps: + "0 < step \ from \ to \ index_list from to step = from # index_list (from + step) to step" + "0 < step \ from > to \ index_list from to step = []" + "0 > step \ from \ to \ index_list from to step = from # index_list (from + step) to step" + "0 > step \ from < to \ index_list from to step = []" + by auto + +lemma index_list_step1_upto[simp]: "index_list i j 1 = [i..j]" + by (induction i j "1 :: int" rule: index_list.induct) + (auto simp: index_list_simps upto.simps) + +lemma length_upto[simp]: "i \ j \ length [i..j] = nat (j - i + 1)" + by (induction i j rule: upto.induct) (auto simp: upto.simps) + +lemma nth_upto[simp]: "i + int n \ j \ [i..j] ! n = i + int n" + by (induction i j arbitrary: n rule: upto.induct) + (auto simp: upto.simps nth_Cons split: nat.splits) + +declare index_list.simps[simp del] + lemma just_list_map_Some[simp]: "just_list (map Some v) = Some v" by (induction v) auto lemma just_list_None_iff[simp]: "just_list xs = None \ None \ set xs" by (induction xs) (auto split: option.splits) +lemma just_list_None_member_None: "None \ set xs \ just_list xs = None" + by auto + lemma just_list_Some_iff[simp]: "just_list xs = Some ys \ xs = map Some ys" by (induction xs arbitrary: ys) (auto split: option.splits) @@ -28,10 +145,10 @@ lemma repeat_singleton_replicate[simp]: proof (induction n) case (nonneg n) have "nat (1 + int m) = Suc m" for m by auto - then show ?case by (induction n) auto + then show ?case by (induction n) (auto simp: repeat.simps) next case (neg n) - then show ?case by auto + then show ?case by (auto simp: repeat.simps) qed lemma bool_of_bitU_simps[simp]: @@ -102,6 +219,15 @@ lemma unsigned_bits_of_mword[simp]: "unsigned_method BC_bitU_list (bits_of_method BC_mword a) = Some (uint a)" by (auto simp: BC_bitU_list_def BC_mword_defs unsigned_of_bits_def unsigned_of_bools_def) +definition mem_bytes_of_word :: "'a::len word \ bitU list list" where + "mem_bytes_of_word w = rev (take_chunks 8 (map bitU_of_bool (to_bl w)))" + +lemma mem_bytes_of_bits_mem_bytes_of_word[simp]: + assumes "8 dvd LENGTH('a)" + shows "mem_bytes_of_bits BC_mword (w :: 'a::len word) = Some (mem_bytes_of_word w)" + using assms + by (auto simp: mem_bytes_of_bits_def bytes_of_bits_def BC_mword_defs byte_chunks_take_chunks_8 mem_bytes_of_word_def) + lemma bits_of_bitU_list[simp]: "bits_of_method BC_bitU_list v = v" "of_bits_method BC_bitU_list v = Some v" @@ -158,6 +284,14 @@ lemma update_list_dec_update[simp]: "update_list_dec xs n x = xs[length xs - nat (n + 1) := x]" by (auto simp: update_list_dec_def add.commute diff_diff_add nat_minus_as_int) +lemma update_list_dec_update_rev: + "0 \ n \ nat n < length xs \ update_list_dec xs n x = rev ((rev xs)[nat n := x])" + by (auto simp: update_list_dec_def add.commute diff_diff_add nat_minus_as_int rev_update) + +lemma access_list_dec_update_list_dec[simp]: + "0 \ n \ nat n < length xs \ access_list_dec (update_list_dec xs n x) n = x" + by (auto simp: access_list_dec_rev_nth update_list_dec_update_rev) + lemma bools_of_nat_aux_simps[simp]: "\len. len \ 0 \ bools_of_nat_aux len x acc = acc" "\len. bools_of_nat_aux (int (Suc len)) x acc = @@ -200,7 +334,7 @@ proof (induction len arbitrary: n acc) qed auto lemma bools_of_int_bin_to_bl[simp]: - "bools_of_int (int len) n = bin_to_bl len n" + "bools_of_int len n = bin_to_bl (nat len) n" by (auto simp: bools_of_int_def Let_def map_Not_bin_to_bl rbl_succ[unfolded bin_to_bl_def]) end -- cgit v1.2.3 From f652ae23b6cbaa3d70ae38f8942d6ae61af2c1d6 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Tue, 10 Jul 2018 13:57:17 +0100 Subject: Another AArch64 patch Makes CheckAndUpdateDescriptor respect endianness --- aarch64/mono/demo/aarch64_no_vector/spec.sail | 3 +++ 1 file changed, 3 insertions(+) diff --git a/aarch64/mono/demo/aarch64_no_vector/spec.sail b/aarch64/mono/demo/aarch64_no_vector/spec.sail index ecb3a050..1cd6fdbd 100644 --- a/aarch64/mono/demo/aarch64_no_vector/spec.sail +++ b/aarch64/mono/demo/aarch64_no_vector/spec.sail @@ -6715,6 +6715,7 @@ function AArch64_SecondStageTranslate (S1, vaddress, acctype, iswrite, wasaligne } function AArch64_CheckAndUpdateDescriptor (result, fault, secondstage, vaddress, acctype, iswrite, s2fs1walk, hwupdatewalk__arg) = { + let reversedescriptors = (aget_SCTLR()[25] == bitone); hwupdatewalk = hwupdatewalk__arg; hw_update_AF : bool = undefined; if result.AF then if fault.typ == Fault_None then hw_update_AF = true else if ConstrainUnpredictable(Unpredictable_AFUPDATE) == Constraint_TRUE then hw_update_AF = true else hw_update_AF = false else hw_update_AF = false; @@ -6735,8 +6736,10 @@ function AArch64_CheckAndUpdateDescriptor (result, fault, secondstage, vaddress, }; accdesc = CreateAccessDescriptor(AccType_ATOMICRW); desc = aget__Mem(descaddr2, 8, accdesc); + if reversedescriptors then desc = BigEndianReverse(desc) else (); if hw_update_AF then desc = __SetSlice_bits(64, 1, desc, 10, 0b1) else (); if hw_update_AP then desc = __SetSlice_bits(64, 1, desc, 7, if secondstage then 0b1 else 0b0) else (); + if reversedescriptors then desc = BigEndianReverse(desc) else (); aset__Mem(descaddr2, 8, accdesc, desc) } else (); return(fault) -- cgit v1.2.3 From adadda8dfc80d0b7e6a967ceeda98624198800c1 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Tue, 10 Jul 2018 14:05:36 +0100 Subject: Update HOL setup --- aarch64/mono/demo/mk.hol | 4 +- lib/hol/Holmakefile | 9 ++- lib/hol/Makefile | 31 +++---- lib/hol/prompt.lem | 18 ----- lib/hol/prompt_monad.lem | 49 ----------- lib/hol/sail2_prompt.lem | 19 +++++ lib/hol/sail2_prompt_monad.lem | 49 +++++++++++ lib/hol/sail2_stateAuxiliaryScript.sml | 61 ++++++++++++++ lib/hol/sail2_valuesAuxiliaryScript.sml | 139 ++++++++++++++++++++++++++++++++ lib/hol/sail_valuesAuxiliaryScript.sml | 139 -------------------------------- lib/hol/stateAuxiliaryScript.sml | 61 -------------- 11 files changed, 293 insertions(+), 286 deletions(-) delete mode 100644 lib/hol/prompt.lem delete mode 100644 lib/hol/prompt_monad.lem create mode 100644 lib/hol/sail2_prompt.lem create mode 100644 lib/hol/sail2_prompt_monad.lem create mode 100644 lib/hol/sail2_stateAuxiliaryScript.sml create mode 100644 lib/hol/sail2_valuesAuxiliaryScript.sml delete mode 100644 lib/hol/sail_valuesAuxiliaryScript.sml delete mode 100644 lib/hol/stateAuxiliaryScript.sml diff --git a/aarch64/mono/demo/mk.hol b/aarch64/mono/demo/mk.hol index cd9f84fc..3aa142a3 100755 --- a/aarch64/mono/demo/mk.hol +++ b/aarch64/mono/demo/mk.hol @@ -5,5 +5,7 @@ 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 -hol -outdir . -lib ../../../lib/hol -lib ../../../src/gen_lib/ -lib ../../../src/lem_interp ../aarch64_extras.lem aarch64_mono_types.lem aarch64_mono.lem +# Explicitly include replacement prompt files, as Lem's choice of file depends +# on some internal dependency ordering +lem -hol -outdir . -lib ../../../lib/hol ../../../lib/hol/sail2_prompt_monad.lem ../../../lib/hol/sail2_prompt.lem -lib ../../../src/gen_lib/ -lib ../../../src/lem_interp ../aarch64_extras.lem aarch64_mono_types.lem aarch64_mono.lem Holmake diff --git a/lib/hol/Holmakefile b/lib/hol/Holmakefile index eac4fec8..8e8403f3 100644 --- a/lib/hol/Holmakefile +++ b/lib/hol/Holmakefile @@ -1,11 +1,12 @@ -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_SCRIPTS = sail2_instr_kindsScript.sml sail2_valuesScript.sml sail2_operatorsScript.sml \ + sail2_operators_mwordsScript.sml sail2_operators_bitlistsScript.sml \ + sail2_state_monadScript.sml sail2_stateScript.sml sail2_promptScript.sml sail2_prompt_monadScript.sml \ + sail2_stringScript.sml LEM_CLEANS = $(LEM_SCRIPTS) SCRIPTS = $(LEM_SCRIPTS) \ - sail_valuesAuxiliaryScript.sml stateAuxiliaryScript.sml + sail2_valuesAuxiliaryScript.sml sail2_stateAuxiliaryScript.sml THYS = $(patsubst %Script.sml,%Theory.uo,$(SCRIPTS)) diff --git a/lib/hol/Makefile b/lib/hol/Makefile index 065f887a..783ef23d 100644 --- a/lib/hol/Makefile +++ b/lib/hol/Makefile @@ -1,22 +1,25 @@ 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 + ../../src/lem_interp/sail2_instr_kinds.lem \ + ../../src/gen_lib/sail2_values.lem \ + ../../src/gen_lib/sail2_operators.lem \ + ../../src/gen_lib/sail2_operators_mwords.lem \ + ../../src/gen_lib/sail2_operators_bitlists.lem \ + ../../src/gen_lib/sail2_state_monad.lem \ + ../../src/gen_lib/sail2_state.lem \ + ../../src/gen_lib/sail2_string.lem \ + sail2_prompt_monad.lem \ + sail2_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 +SCRIPTS = sail2_instr_kindsScript.sml sail2_valuesScript.sml sail2_operatorsScript.sml \ + sail2_operators_mwordsScript.sml sail2_operators_bitlistsScript.sml \ + sail2_state_monadScript.sml sail2_stateScript.sml \ + sail2_prompt_monadScript.sml sail2_promptScript.sml \ + sail2_stringScript.sml THYS = $(patsubst %Script.sml,%Theory.uo,$(SCRIPTS)) all: sail-heap $(THYS) +all-scripts: $(SCRIPTS) $(SCRIPTS): $(LEMSRC) lem -hol -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $(LEMSRC) @@ -28,4 +31,4 @@ $(THYS) sail-heap: $(SCRIPTS) clean: Holmake cleanAll -.PHONY: all clean +.PHONY: all all-scripts clean diff --git a/lib/hol/prompt.lem b/lib/hol/prompt.lem deleted file mode 100644 index 3597fa06..00000000 --- a/lib/hol/prompt.lem +++ /dev/null @@ -1,18 +0,0 @@ -open import Prompt_monad -open import State_monad -open import State - -let inline undefined_bool = undefined_boolS -let inline bool_of_bitU_nondet = bool_of_bitU_nondetS -let inline bool_of_bitU_fail = bool_of_bitU_fail -let inline bools_of_bits_nondet = bools_of_bits_nondetS -let inline of_bits_nondet = of_bits_nondetS -let inline of_bits_fail = of_bits_failS -let inline mword_nondet = mword_nondetS -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 deleted file mode 100644 index 8fcd645a..00000000 --- a/lib/hol/prompt_monad.lem +++ /dev/null @@ -1,49 +0,0 @@ -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/sail2_prompt.lem b/lib/hol/sail2_prompt.lem new file mode 100644 index 00000000..674d4e34 --- /dev/null +++ b/lib/hol/sail2_prompt.lem @@ -0,0 +1,19 @@ +open import Sail2_prompt_monad +open import Sail2_state_monad +open import Sail2_state + +let inline undefined_bool = undefined_boolS +let inline bool_of_bitU_nondet = bool_of_bitU_nondetS +let inline bool_of_bitU_fail = bool_of_bitU_fail +let inline bools_of_bits_nondet = bools_of_bits_nondetS +let inline of_bits_nondet = of_bits_nondetS +let inline of_bits_fail = of_bits_failS +let inline mword_nondet = mword_nondetS +let inline reg_deref = read_regS +let inline internal_pick = internal_pickS + +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/sail2_prompt_monad.lem b/lib/hol/sail2_prompt_monad.lem new file mode 100644 index 00000000..3af931a5 --- /dev/null +++ b/lib/hol/sail2_prompt_monad.lem @@ -0,0 +1,49 @@ +open import Pervasives_extra +open import Sail2_instr_kinds +open import Sail2_values +open import Sail2_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/sail2_stateAuxiliaryScript.sml b/lib/hol/sail2_stateAuxiliaryScript.sml new file mode 100644 index 00000000..4d70b033 --- /dev/null +++ b/lib/hol/sail2_stateAuxiliaryScript.sml @@ -0,0 +1,61 @@ +(*Generated by Lem from ../../src/gen_lib/state.lem.*) +open HolKernel Parse boolLib bossLib; +open lem_pervasives_extraTheory sail2_valuesTheory sail2_state_monadTheory sail2_stateTheory; + +val _ = numLib.prefer_num(); + + + +open lemLib; +(* val _ = lemLib.run_interactive := true; *) +val _ = new_theory "sail2_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() + diff --git a/lib/hol/sail2_valuesAuxiliaryScript.sml b/lib/hol/sail2_valuesAuxiliaryScript.sml new file mode 100644 index 00000000..b475c5ea --- /dev/null +++ b/lib/hol/sail2_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 sail2_valuesTheory; +open intLib; + +val _ = numLib.prefer_num(); + + + +open lemLib; +(* val _ = lemLib.run_interactive := true; *) +val _ = new_theory "sail2_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/sail_valuesAuxiliaryScript.sml b/lib/hol/sail_valuesAuxiliaryScript.sml deleted file mode 100644 index aa169979..00000000 --- a/lib/hol/sail_valuesAuxiliaryScript.sml +++ /dev/null @@ -1,139 +0,0 @@ -(*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 deleted file mode 100644 index c8269750..00000000 --- a/lib/hol/stateAuxiliaryScript.sml +++ /dev/null @@ -1,61 +0,0 @@ -(*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() - -- cgit v1.2.3