Add some lemmas about bitvectors

Also clean up some library functions a bit, and add some missing failure
handling variants of division operations on bitvectors.

5 files changed, 217 insertions, 11 deletions

diff --git a/lib/isabelle/Prompt_monad_lemmas.thy b/lib/isabelle/Prompt_monad_lemmas.thy
index 84f3333e..e883c2a0 100644
--- a/lib/isabelle/Prompt_monad_lemmas.thy
+++ b/lib/isabelle/Prompt_monad_lemmas.thy
@@ -13,7 +13,7 @@ lemma All_bind_dom: "bind_dom (m, f)"
   by (induction m) (auto intro: bind.domintros)
 
 termination bind using All_bind_dom by auto
-lemmas bind_induct[case_names Done Read_mem Write_memv Read_reg Excl_res Write_ea Barrier Write_reg Fail Error Exception] = bind.induct
+lemmas bind_induct[case_names Done Read_mem Write_memv Read_reg Excl_res Write_ea Barrier Write_reg Fail Exception] = bind.induct
 
 lemma bind_return[simp]: "bind (return a) f = f a"
   by (auto simp: return_def)
@@ -21,10 +21,13 @@ lemma bind_return[simp]: "bind (return a) f = f a"
 lemma bind_assoc[simp]: "bind (bind m f) g = bind m (\<lambda>x. bind (f x) g)"
   by (induction m f arbitrary: g rule: bind.induct) auto
 
+lemma bind_assert_True[simp]: "bind (assert_exp True msg) f = f ()"
+  by (auto simp: assert_exp_def)
+
 lemma All_try_catch_dom: "try_catch_dom (m, h)"
   by (induction m) (auto intro: try_catch.domintros)
 termination try_catch using All_try_catch_dom by auto
-lemmas try_catch_induct[case_names Done Read_mem Write_memv Read_reg Excl_res Write_ea Barrier Write_reg Fail Error Exception] = try_catch.induct
+lemmas try_catch_induct[case_names Done Read_mem Write_memv Read_reg Excl_res Write_ea Barrier Write_reg Fail Exception] = try_catch.induct
 
 datatype 'regval event =
   (* Request to read memory *)
diff --git a/lib/isabelle/Sail_operators_mwords_lemmas.thy b/lib/isabelle/Sail_operators_mwords_lemmas.thy
new file mode 100644
index 00000000..22c35e1f
--- /dev/null
+++ b/lib/isabelle/Sail_operators_mwords_lemmas.thy
@@ -0,0 +1,112 @@
+theory "Sail_operators_mwords_lemmas"
+  imports Sail_operators_mwords
+begin
+
+lemmas uint_simps[simp] = uint_maybe_def uint_fail_def uint_oracle_def
+lemmas sint_simps[simp] = sint_maybe_def sint_fail_def sint_oracle_def
+
+lemma bools_of_bits_oracle_just_list[simp]:
+  assumes "just_list (map bool_of_bitU bus) = Some bs"
+  shows "bools_of_bits_oracle bus = return bs"
+proof -
+  have f: "foreachM bus bools (\<lambda>b bools. bool_of_bitU_oracle b \<bind> (\<lambda>b. return (bools @ [b]))) = return (bools @ bs)"
+    if "just_list (map bool_of_bitU bus) = Some bs" for bus bs bools
+  proof (use that in \<open>induction bus arbitrary: bs bools\<close>)
+    case (Cons bu bus bs)
+    obtain b bs' where bs: "bs = b # bs'" and bu: "bool_of_bitU bu = Some b"
+      using Cons.prems by (cases bu) (auto split: option.splits)
+    then show ?case
+      using Cons.prems Cons.IH[where bs = bs' and bools = "bools @ [b]"]
+      by (cases bu) (auto simp: bool_of_bitU_oracle_def split: option.splits)
+  qed auto
+  then show ?thesis using f[OF assms, of "[]"] unfolding bools_of_bits_oracle_def
+    by auto
+qed
+
+lemma of_bits_mword_return_of_bl[simp]:
+  assumes "just_list (map bool_of_bitU bus) = Some bs"
+  shows "of_bits_oracle BC_mword bus = return (of_bl bs)"
+    and "of_bits_fail BC_mword bus = return (of_bl bs)"
+  by (auto simp: of_bits_oracle_def of_bits_fail_def maybe_fail_def assms BC_mword_defs)
+
+lemma vec_of_bits_of_bl[simp]:
+  assumes "just_list (map bool_of_bitU bus) = Some bs"
+  shows "vec_of_bits_maybe bus = Some (of_bl bs)"
+    and "vec_of_bits_fail bus = return (of_bl bs)"
+    and "vec_of_bits_oracle bus = return (of_bl bs)"
+    and "vec_of_bits_failwith bus = of_bl bs"
+    and "vec_of_bits bus = of_bl bs"
+  unfolding vec_of_bits_maybe_def vec_of_bits_fail_def vec_of_bits_oracle_def
+            vec_of_bits_failwith_def vec_of_bits_def
+  by (auto simp: assms)
+
+lemmas access_vec_dec_test_bit[simp] = access_bv_dec_mword[folded access_vec_dec_def]
+
+lemma access_vec_inc_test_bit[simp]:
+  fixes w :: "('a::len) word"
+  assumes "n \<ge> 0" and "nat n < LENGTH('a)"
+  shows "access_vec_inc w n = bitU_of_bool (w !! (LENGTH('a) - 1 - nat n))"
+  using assms
+  by (auto simp: access_vec_inc_def access_bv_inc_def access_list_def BC_mword_defs rev_nth test_bit_bl)
+
+lemma bool_of_bitU_monadic_simps[simp]:
+  "bool_of_bitU_fail B0 = return False"
+  "bool_of_bitU_fail B1 = return True"
+  "bool_of_bitU_fail BU = Fail ''bool_of_bitU''"
+  "bool_of_bitU_oracle B0 = return False"
+  "bool_of_bitU_oracle B1 = return True"
+  "bool_of_bitU_oracle BU = undefined_bool ()"
+  unfolding bool_of_bitU_fail_def bool_of_bitU_oracle_def
+  by auto
+
+lemma update_vec_dec_simps[simp]:
+  "update_vec_dec_maybe w i B0 = Some (set_bit w (nat i) False)"
+  "update_vec_dec_maybe w i B1 = Some (set_bit w (nat i) True)"
+  "update_vec_dec_maybe w i BU = None"
+  "update_vec_dec_fail w i B0 = return (set_bit w (nat i) False)"
+  "update_vec_dec_fail w i B1 = return (set_bit w (nat i) True)"
+  "update_vec_dec_fail w i BU = Fail ''bool_of_bitU''"
+  "update_vec_dec_oracle w i B0 = return (set_bit w (nat i) False)"
+  "update_vec_dec_oracle w i B1 = return (set_bit w (nat i) True)"
+  "update_vec_dec_oracle w i BU = undefined_bool () \<bind> (\<lambda>b. return (set_bit w (nat i) b))"
+  "update_vec_dec w i B0 = set_bit w (nat i) False"
+  "update_vec_dec w i B1 = set_bit w (nat i) True"
+  unfolding update_vec_dec_maybe_def update_vec_dec_fail_def update_vec_dec_oracle_def update_vec_dec_def
+  by (auto simp: update_mword_dec_def update_mword_bool_dec_def maybe_failwith_def)
+
+lemma len_of_minus_One_minus_nonneg_lt_len_of[simp]:
+  "n \<ge> 0 \<Longrightarrow> 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 extz_vec_def[simp]
+declare exts_vec_def[simp]
+declare concat_vec_def[simp]
+
+lemma msb_Bits_msb[simp]:
+  "msb w = bitU_of_bool (Bits.msb w)"
+  by (auto simp: msb_def most_significant_def BC_mword_defs word_msb_alt split: list.splits)
+
+declare and_vec_def[simp]
+declare or_vec_def[simp]
+declare xor_vec_def[simp]
+declare not_vec_def[simp]
+
+lemma arith_vec_simps[simp]:
+  "add_vec l r = l + r"
+  "sub_vec l r = l - r"
+  "mult_vec l r = (ucast l) * (ucast r)"
+  unfolding add_vec_def sub_vec_def mult_vec_def
+  by (auto simp: int_of_mword_def word_add_def word_sub_wi word_mult_def)
+
+declare adds_vec_def[simp]
+declare subs_vec_def[simp]
+declare mults_vec_def[simp]
+
+lemma arith_vec_int_simps[simp]:
+  "add_vec_int l r = l + (word_of_int r)"
+  "sub_vec_int l r = l - (word_of_int r)"
+  "mult_vec_int l r = (ucast l) * (word_of_int r)"
+  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)
+
+end
diff --git a/lib/isabelle/Sail_values_lemmas.thy b/lib/isabelle/Sail_values_lemmas.thy
index 256e76d0..dd008695 100644
--- a/lib/isabelle/Sail_values_lemmas.thy
+++ b/lib/isabelle/Sail_values_lemmas.thy
@@ -23,6 +23,23 @@ lemma just_list_cases:
         | (Some) ys where "xs = map Some ys" and "y = Some ys"
   using assms by (cases y) auto
 
+lemma repeat_singleton_replicate[simp]:
+  "repeat [x] n = replicate (nat n) x"
+proof (induction n)
+  case (nonneg n)
+  have "nat (1 + int m) = Suc m" for m by auto
+  then show ?case by (induction n) auto
+next
+  case (neg n)
+  then show ?case by auto
+qed
+
+lemma bool_of_bitU_simps[simp]:
+  "bool_of_bitU B0 = Some False"
+  "bool_of_bitU B1 = Some True"
+  "bool_of_bitU BU = None"
+  by (auto simp: bool_of_bitU_def)
+
 lemma bitops_bitU_of_bool[simp]:
   "and_bit (bitU_of_bool x) (bitU_of_bool y) = bitU_of_bool (x \<and> y)"
   "or_bit (bitU_of_bool x) (bitU_of_bool y) = bitU_of_bool (x \<or> y)"
@@ -49,11 +66,28 @@ lemmas BC_mword_defs = instance_Sail_values_Bitvector_Machine_word_mword_dict_de
   subrange_list_def subrange_list_inc_def subrange_list_dec_def
   update_subrange_list_def update_subrange_list_inc_def update_subrange_list_dec_def
 
+declare size_itself_int_def[simp]
+declare size_itself_def[simp]
+declare word_size[simp]
+
+lemma int_of_mword_simps[simp]:
+  "int_of_mword False w = uint w"
+  "int_of_mword True w = sint w"
+  "int_of_bv BC_mword False w = Some (uint w)"
+  "int_of_bv BC_mword True w = Some (sint w)"
+  by (auto simp: int_of_mword_def int_of_bv_def BC_mword_defs)
+
 lemma BC_mword_simps[simp]:
   "unsigned_method BC_mword a = Some (uint a)"
   "signed_method BC_mword a = Some (sint a)"
   "length_method BC_mword (a :: ('a :: len) word) = int (LENGTH('a))"
-  by (auto simp: BC_mword_defs word_size)
+  by (auto simp: BC_mword_defs)
+
+lemma of_bits_mword_of_bl[simp]:
+  assumes "just_list (map bool_of_bitU bus) = Some bs"
+  shows "of_bits_method BC_mword bus = Some (of_bl bs)"
+    and "of_bits_failwith BC_mword bus = of_bl bs"
+  using assms by (auto simp: BC_mword_defs of_bits_failwith_def maybe_failwith_def)
 
 lemma nat_of_bits_aux_bl_to_bin_aux:
   "nat_of_bools_aux acc bs = nat (bl_to_bin_aux bs (int acc))"
@@ -97,12 +131,6 @@ lemma update_subrange_list_dec_drop_take:
 
 declare access_list_inc_def[simp]
 
-lemma access_list_dec_nth:
-  assumes "0 \<le> i"
-  shows "access_list_dec xs i = xs ! (length xs - nat (i + 1))"
-  using assms
-  by (auto simp: access_list_dec_def add.commute diff_diff_add nat_minus_as_int)
-
 lemma access_list_dec_rev_nth:
   assumes "0 \<le> i" and "nat i < length xs"
   shows "access_list_dec xs i = rev xs ! (nat i)"
@@ -114,14 +142,65 @@ lemma access_bv_dec_mword[simp]:
   assumes "0 \<le> n" and "nat n < LENGTH('a)"
   shows "access_bv_dec BC_mword w n = bitU_of_bool (w !! (nat n))"
   using assms unfolding access_bv_dec_def access_list_def
-  by (auto simp: access_list_dec_rev_nth BC_mword_defs rev_map test_bit_bl word_size)
+  by (auto simp: access_list_dec_rev_nth BC_mword_defs rev_map test_bit_bl)
+
+lemma access_list_dec_nth[simp]:
+  assumes "0 \<le> i"
+  shows "access_list_dec xs i = xs ! (length xs - nat (i + 1))"
+  using assms
+  by (auto simp: access_list_dec_def add.commute diff_diff_add nat_minus_as_int)
 
 lemma update_list_inc_update[simp]:
   "update_list_inc xs n x = xs[nat n := x]"
   by (auto simp: update_list_inc_def)
 
-lemma update_list_dec_update:
+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 bools_of_nat_aux_simps[simp]:
+  "\<And>len. len \<le> 0 \<Longrightarrow> bools_of_nat_aux len x acc = acc"
+  "\<And>len. bools_of_nat_aux (int (Suc len)) x acc =
+     bools_of_nat_aux (int len) (x div 2) ((if x mod 2 = 1 then True else False) # acc)"
+  by auto
+declare bools_of_nat_aux.simps[simp del]
+
+lemma bools_of_nat_aux_bin_to_bl_aux:
+  "bools_of_nat_aux len n acc = bin_to_bl_aux (nat len) (int n) acc"
+proof (cases len)
+  case (nonneg len')
+  show ?thesis unfolding nonneg
+  proof (induction len' arbitrary: n acc)
+    case (Suc len'' n acc)
+    then show ?case
+      using zmod_int[of n 2]
+      by (auto simp del: of_nat_simps simp add: bin_rest_def bin_last_def zdiv_int)
+  qed auto
+qed auto
+
+lemma bools_of_nat_bin_to_bl[simp]:
+  "bools_of_nat len n = bin_to_bl (nat len) (int n)"
+  by (auto simp: bools_of_nat_def bools_of_nat_aux_bin_to_bl_aux)
+
+lemma add_one_bool_ignore_overflow_aux_rbl_succ[simp]:
+  "add_one_bool_ignore_overflow_aux xs = rbl_succ xs"
+  by (induction xs) auto
+
+lemma add_one_bool_ignore_overflow_rbl_succ[simp]:
+  "add_one_bool_ignore_overflow xs = rev (rbl_succ (rev xs))"
+  unfolding add_one_bool_ignore_overflow_def by auto
+
+lemma map_Not_bin_to_bl:
+  "map Not (bin_to_bl_aux len n acc) = bin_to_bl_aux len (-n - 1) (map Not acc)"
+proof (induction len arbitrary: n acc)
+  case (Suc len n acc)
+  moreover have "(- (n div 2) - 1) = ((-n - 1) div 2)" by auto
+  moreover have "(n mod 2 = 0) = ((- n - 1) mod 2 = 1)" by presburger
+  ultimately show ?case by (auto simp: bin_rest_def bin_last_def)
+qed auto
+
+lemma bools_of_int_bin_to_bl[simp]:
+  "bools_of_int (int len) n = bin_to_bl len n"
+  by (auto simp: bools_of_int_def Let_def map_Not_bin_to_bl rbl_succ[unfolded bin_to_bl_def])
+
 end
diff --git a/lib/isabelle/State_lemmas.thy b/lib/isabelle/State_lemmas.thy
index 36fb987f..84b08e6c 100644
--- a/lib/isabelle/State_lemmas.thy
+++ b/lib/isabelle/State_lemmas.thy
@@ -19,6 +19,8 @@ lemma Value_liftState_Run:
       auto simp add: failS_def throwS_def returnS_def simp del: read_regvalS.simps;
       blast elim: Value_bindS_elim)
 
+lemmas liftState_if_distrib[simp] = if_distrib[where f = "liftState ra" for ra]
+
 lemma liftState_throw[simp]: "liftState r (throw e) = throwS e" by (auto simp: throw_def)
 lemma liftState_assert[simp]: "liftState r (assert_exp c msg) = assert_expS c msg" by (auto simp: assert_exp_def assert_expS_def)
 lemma liftState_exit[simp]: "liftState r (exit0 ()) = exitS ()" by (auto simp: exit0_def exitS_def)
diff --git a/lib/isabelle/State_monad_lemmas.thy b/lib/isabelle/State_monad_lemmas.thy
index e7286fcf..e0d684ba 100644
--- a/lib/isabelle/State_monad_lemmas.thy
+++ b/lib/isabelle/State_monad_lemmas.thy
@@ -32,6 +32,9 @@ lemma bindS_readS: "bindS (readS f) m = (\<lambda>s. m (f s) s)"
 lemma bindS_updateS: "bindS (updateS f) m = (\<lambda>s. m () (f s))"
   by (auto simp: bindS_def updateS_def returnS_def)
 
+lemma bindS_assertS_True[simp]: "bindS (assert_expS True msg) f = f ()"
+  by (auto simp: assert_expS_def)
+
 
 lemma result_cases:
   fixes r :: "('a, 'e) result"
@@ -126,6 +129,13 @@ lemma try_catchS_intros:
   "\<And>m h s e s'' r s'. (Ex (Throw e), s'') \<in> m s \<Longrightarrow> (r, s') \<in> h e s'' \<Longrightarrow> (r, s') \<in> try_catchS m h s"
   by (auto simp: try_catchS_def returnS_def intro: bexI[rotated])
 
+lemma no_Ex_basic_builtins[simp]:
+  "\<And>s e s' a. (Ex e, s') \<in> returnS a s \<longleftrightarrow> False"
+  "\<And>s e s' f. (Ex e, s') \<in> readS f s \<longleftrightarrow> False"
+  "\<And>s e s' f. (Ex e, s') \<in> updateS f s \<longleftrightarrow> False"
+  "\<And>s e s' xs. (Ex e, s') \<in> chooseS xs s \<longleftrightarrow> False"
+  by (auto simp: readS_def updateS_def returnS_def chooseS_def)
+
 fun ignore_throw_aux :: "(('a, 'e1) result \<times> 's) \<Rightarrow> (('a, 'e2) result \<times> 's) set" where
   "ignore_throw_aux (Value a, s') = {(Value a, s')}"
 | "ignore_throw_aux (Ex (Throw e), s') = {}"