Merge branch 'sail2' into rmem_interpreter

19 files changed, 645 insertions, 175 deletions

diff --git a/lib/arith.sail b/lib/arith.sail
index eed257fb..93500794 100644
--- a/lib/arith.sail
+++ b/lib/arith.sail
@@ -70,7 +70,11 @@ val _shl_int = "shl_int" : (int, int) -> int
 
 overload shl_int = {_shl8, _shl32, _shl_int}
 
-val shr_int = "shr_int" : (int, int) -> int
+val _shr32 = {c: "shr_mach_int", _: "shr_int"} : forall 'n, 0 <= 'n <= 31. (int('n), int(1)) -> {'m, 0 <= 'm <= 15. int('m)}
+
+val _shr_int = "shr_int" : (int, int) -> int
+
+overload shr_int = {_shr32, _shr_int}
 
 // ***** div and mod *****
 
@@ -101,6 +105,7 @@ val abs_int = {
   ocaml: "abs_int",
   interpreter: "abs_int",
   lem: "abs_int",
+  c: "abs_int",
   coq: "Z.abs"
 } : (int, int) -> int
 
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 219a6f84..943d850a 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -45,6 +45,26 @@ End Morphism.
 Definition build_ex {T:Type} (n:T) {P:T -> Prop} `{H:ArithFact (P n)} : {x : T & ArithFact (P x)} :=
   existT _ n H.
 
+(* The informative boolean type. *)
+
+Definition Bool (P : Prop) : Type := {P} + {~P}.
+
+Definition build_Bool {P:Prop} (b:bool) `{ArithFact (b = true <-> P)} : Bool P.
+refine (if sumbool_of_bool b then left _ else right _);
+destruct H; subst;
+intuition.
+Defined.
+
+Definition projBool {P:Prop} (b:Bool P) : bool := if b then true else false.
+
+Lemma projBool_true {P:Prop} {b:Bool P} : projBool b = true <-> P.
+destruct b; simpl; intuition.
+Qed.
+Lemma projBool_false {P:Prop} {b:Bool P} : projBool b = false <-> ~P.
+destruct b; simpl; intuition.
+Qed.
+
+
 Definition generic_eq {T:Type} (x y:T) `{Decidable (x = y)} := Decidable_witness.
 Definition generic_neq {T:Type} (x y:T) `{Decidable (x = y)} := negb Decidable_witness.
 Lemma generic_eq_true {T} {x y:T} `{Decidable (x = y)} : generic_eq x y = true -> x = y.
@@ -1037,6 +1057,27 @@ Ltac unbool_comparisons :=
   | H:context [generic_neq _ _ = true] |- _ => apply generic_neq_true in H
   | H:context [generic_neq _ _ = false] |- _ => apply generic_neq_false in H
   end.
+Ltac unbool_comparisons_goal :=
+  repeat match goal with
+  | |- context [Z.geb _ _] => rewrite Z.geb_leb
+  | |- context [Z.gtb _ _] => rewrite Z.gtb_ltb
+  | |- context [Z.leb _ _ = true] => rewrite Z.leb_le
+  | |- context [Z.ltb _ _ = true] => rewrite Z.ltb_lt
+  | |- context [Z.eqb _ _ = true] => rewrite Z.eqb_eq
+  | |- context [Z.leb _ _ = false] => rewrite Z.leb_gt
+  | |- context [Z.ltb _ _ = false] => rewrite Z.ltb_ge
+  | |- context [Z.eqb _ _ = false] => rewrite Z.eqb_neq
+  | |- context [orb _ _ = true] => rewrite Bool.orb_true_iff
+  | |- context [orb _ _ = false] => rewrite Bool.orb_false_iff
+  | |- context [andb _ _ = true] => rewrite Bool.andb_true_iff
+  | |- context [andb _ _ = false] => rewrite Bool.andb_false_iff
+  | |- context [negb _ = true] => rewrite Bool.negb_true_iff
+  | |- context [negb _ = false] => rewrite Bool.negb_false_iff
+  | |- context [generic_eq _ _ = true] => apply generic_eq_true
+  | |- context [generic_eq _ _ = false] => apply generic_eq_false
+  | |- context [generic_neq _ _ = true] => apply generic_neq_true
+  | |- context [generic_neq _ _ = false] => apply generic_neq_false
+  end.
 
 (* Split up dependent pairs to get at proofs of properties *)
 Ltac extract_properties :=
@@ -1072,6 +1113,11 @@ Ltac extract_properties :=
     let Hx := fresh "Hx" in
     destruct X as [x Hx] in *;
     change (projT1 (existT _ x Hx)) with x in * end.
+(* We could also destruct any remaining Bools, if necessary. *)
+Ltac extract_Bool_props :=
+  repeat match goal with
+  | H:projBool _ = true |- _ => rewrite projBool_true in H
+  | H:projBool _ = false |- _ => rewrite projBool_false in H end.
 (* TODO: hyps, too? *)
 Ltac reduce_list_lengths :=
   repeat match goal with |- context [length_list ?X] => 
@@ -1137,10 +1183,12 @@ Ltac prepare_for_solver :=
  autounfold with sail in * |- *; (* You can add Hint Unfold ... : sail to let omega see through fns *)
  split_cases;
  extract_properties;
+ extract_Bool_props;
  repeat match goal with w:mword ?n |- _ => apply ArithFact_mword in w end;
  unwrap_ArithFacts;
  destruct_exists;
  unbool_comparisons;
+ unbool_comparisons_goal;
  unfold_In; (* after unbool_comparisons to deal with && and || *)
  reduce_list_lengths;
  reduce_pow;
@@ -1194,6 +1242,11 @@ Hint Extern 0 (ArithFact _) => run_solver : typeclass_instances.
 
 Hint Unfold length_mword : sail.
 
+Lemma unit_comparison_lemma : true = true <-> True.
+intuition.
+Qed.
+Hint Resolve unit_comparison_lemma : sail.
+
 Definition neq_atom (x : Z) (y : Z) : bool := negb (Z.eqb x y).
 Hint Unfold neq_atom : sail.
 
diff --git a/lib/elf.c b/lib/elf.c
index 4355b44c..397c8f3f 100644
--- a/lib/elf.c
+++ b/lib/elf.c
@@ -411,7 +411,7 @@ int lookupSymbol(const char *buffer, const int total_file_size, const char *symn
         Elf32_Ehdr *ehdr = (Elf32_Ehdr*) &buffer[0];
         if (total_file_size < rdOff32(le, ehdr->e_shoff)
                               + rdHalf32(le, ehdr->e_shnum)*sizeof(Elf32_Shdr)) {
-            fprintf(stderr, "File too small for %d sections from offset %d\n",
+            fprintf(stderr, "File too small for %d sections from offset %ud\n",
                     rdHalf32(le, ehdr->e_shnum), rdOff32(le, ehdr->e_shoff));
             exit(EXIT_FAILURE);
         }
@@ -468,7 +468,7 @@ int lookupSymbol(const char *buffer, const int total_file_size, const char *symn
         Elf64_Ehdr *ehdr = (Elf64_Ehdr*) &buffer[0];
         if (total_file_size < rdOff64(le, ehdr->e_shoff)
                               + rdHalf64(le, ehdr->e_shnum)*sizeof(Elf64_Shdr)) {
-            fprintf(stderr, "File too small for %d sections from offset %ld\n",
+	    fprintf(stderr, "File too small for %d sections from offset %" PRIu64 "\n",
                     rdHalf64(le, ehdr->e_shnum), rdOff64(le, ehdr->e_shoff));
             exit(EXIT_FAILURE);
         }
diff --git a/lib/flow.sail b/lib/flow.sail
index eb7b8038..5c69a128 100644
--- a/lib/flow.sail
+++ b/lib/flow.sail
@@ -9,30 +9,36 @@ therefore be included in just about every Sail specification.
 
 */
 
-val eq_unit : (unit, unit) -> bool
+val eq_unit : (unit, unit) -> bool(true)
 
 val eq_bit = { lem : "eq", _ : "eq_bit" } : (bit, bit) -> bool
 
 function eq_unit(_, _) = true
 
-val not_bool = {coq: "negb", _: "not"} : bool -> bool
+val not_bool = {coq: "negb", _: "not"} : forall ('p : Bool). bool('p) -> bool(not('p))
 /* NB: There are special cases in Sail for effectful uses of and_bool and
    or_bool that are not shown here. */
-val and_bool = {coq: "andb", _: "and_bool"} : (bool, bool) -> bool
-val or_bool = {coq: "orb", _: "or_bool"} : (bool, bool) -> bool
-val eq_int = {ocaml: "eq_int", interpreter: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : (int, int) -> bool
+
+val and_bool = {coq: "andb", _: "and_bool"} : forall ('p : Bool) ('q : Bool). (bool('p), bool('q)) -> bool('p & 'q)
+
+val and_bool_no_flow = {coq: "andb", _: "and_bool"} : (bool, bool) -> bool
+
+val or_bool = {coq: "orb", _: "or_bool"} : forall ('p : Bool) ('q : Bool). (bool('p), bool('q)) -> bool('p | 'q)
+
+val eq_int = {ocaml: "eq_int", interpreter: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : forall 'n 'm. (int('n), int('m)) -> bool('n == 'm)
+
 val eq_bool = {ocaml: "eq_bool", interpreter: "eq_bool", lem: "eq", c: "eq_bool", coq: "Bool.eqb"} : (bool, bool) -> bool
 
-val neq_int = {lem: "neq"} : (int, int) -> bool
+val neq_int = {lem: "neq"} : forall 'n 'm. (int('n), int('m)) -> bool('n != 'm)
 function neq_int (x, y) = not_bool(eq_int(x, y))
 
 val neq_bool : (bool, bool) -> bool
 function neq_bool (x, y) = not_bool(eq_bool(x, y))
 
-val lteq_int = {coq: "Z.leb", _:"lteq"} : (int, int) -> bool
-val gteq_int = {coq: "Z.geb", _:"gteq"} : (int, int) -> bool
-val lt_int = {coq: "Z.ltb", _:"lt"} : (int, int) -> bool
-val gt_int = {coq: "Z.gtb", _:"gt"} : (int, int) -> bool
+val lteq_int = {coq: "Z.leb", _:"lteq"} : forall 'n 'm. (int('n), int('m)) -> bool('n <= 'm)
+val gteq_int = {coq: "Z.geb", _:"gteq"} : forall 'n 'm. (int('n), int('m)) -> bool('n >= 'm)
+val lt_int = {coq: "Z.ltb", _:"lt"} : forall 'n 'm. (int('n), int('m)) -> bool('n < 'm)
+val gt_int = {coq: "Z.gtb", _:"gt"} : forall 'n 'm. (int('n), int('m)) -> bool('n > 'm)
 
 overload operator == = {eq_int, eq_bit, eq_bool, eq_unit}
 overload operator != = {neq_int, neq_bool}
@@ -44,4 +50,15 @@ overload operator < = {lt_int}
 overload operator >= = {gteq_int}
 overload operator > = {gt_int}
 
+/*
+
+when we have sizeof('n) where x : int('n), we can remove that sizeof
+by rewriting it to __size(x).
+
+*/
+
+function __id forall 'n. (x: int('n)) -> int('n) = x
+
+overload __size = {__id}
+
 $endif
diff --git a/lib/hol/sail2_prompt.lem b/lib/hol/sail2_prompt.lem
index 674d4e34..3107d3a5 100644
--- a/lib/hol/sail2_prompt.lem
+++ b/lib/hol/sail2_prompt.lem
@@ -4,12 +4,13 @@ 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 bool_of_bitU_fail = Sail2_state.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 choose msg xs = chooseS xs
 let inline internal_pick = internal_pickS
 
 let inline foreachM = foreachS
diff --git a/lib/hol/sail2_prompt_monad.lem b/lib/hol/sail2_prompt_monad.lem
index 3af931a5..ade12347 100644
--- a/lib/hol/sail2_prompt_monad.lem
+++ b/lib/hol/sail2_prompt_monad.lem
@@ -22,6 +22,8 @@ let inline bind = bindS
 let inline (>>=) = (>>$=)
 let inline (>>) = (>>$)
 
+let inline choose_bool msg = choose_boolS ()
+let inline undefined_bool = undefined_boolS
 let inline exit = exitS
 
 let inline throw = throwS
@@ -34,16 +36,18 @@ let inline try_catchR = try_catchRS
 
 let inline maybe_fail = maybe_failS
 
+let inline read_memt_bytes = read_memt_bytesS
 let inline read_mem_bytes = read_mem_bytesS
 let inline read_reg = read_regS
 let inline reg_deref = read_regS
+let inline read_memt = read_memtS
 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 inline write_mem_ea wk addr sz = return ()
+let inline write_memt = write_memtS
+let inline write_mem = write_memS
 let barrier _ = return ()
+let footprint _ = return ()
 
 let inline assert_exp = assert_expS
diff --git a/lib/isabelle/Hoare.thy b/lib/isabelle/Hoare.thy
index 76750117..98b7d077 100644
--- a/lib/isabelle/Hoare.thy
+++ b/lib/isabelle/Hoare.thy
@@ -164,7 +164,7 @@ qed
 lemma PrePost_assert_expS[intro, PrePost_atomI]: "PrePost (if c then P (Value ()) else P (Ex (Failure m))) (assert_expS c m) P"
   unfolding PrePost_def assert_expS_def by (auto simp: returnS_def failS_def)
 
-lemma PrePost_chooseS[intro, PrePost_atomI]: "PrePost (\<lambda>s. \<forall>x \<in> xs. Q (Value x) s) (chooseS xs) Q"
+lemma PrePost_chooseS[intro, PrePost_atomI]: "PrePost (\<lambda>s. \<forall>x \<in> set xs. Q (Value x) s) (chooseS xs) Q"
   by (auto simp: PrePost_def chooseS_def)
 
 lemma PrePost_failS[intro, PrePost_atomI]: "PrePost (Q (Ex (Failure msg))) (failS msg) Q"
@@ -381,7 +381,7 @@ lemma PrePostE_exitS[PrePostE_atomI, intro]: "PrePostE (E (Failure ''exit'')) (e
   unfolding exitS_def PrePostE_def PrePost_def failS_def by auto
 
 lemma PrePostE_chooseS[intro, PrePostE_atomI]:
-  "PrePostE (\<lambda>s. \<forall>x \<in> xs. Q x s) (chooseS xs) Q E"
+  "PrePostE (\<lambda>s. \<forall>x \<in> set 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"
@@ -488,11 +488,11 @@ lemma PrePostE_liftState_untilM_pure_cond:
   shows "PrePostE (Inv Q vars) (liftState r (untilM vars (return \<circ> cond) body)) Q E"
   using assms by (intro PrePostE_liftState_untilM) (auto simp: comp_def liftState_simp)
 
-lemma PrePostE_undefined_boolS[PrePostE_atomI]:
+lemma PrePostE_choose_boolS_any[PrePostE_atomI]:
   "PrePostE (\<lambda>s. \<forall>b. Q b s)
-            (undefined_boolS unit) Q E"
-  unfolding undefined_boolS_def seqS_def
-  by (auto intro: PrePostE_strengthen_pre PrePostE_chooseS)
+            (choose_boolS unit) Q E"
+  unfolding choose_boolS_def seqS_def
+  by (auto intro: PrePostE_strengthen_pre)
 
 lemma PrePostE_bool_of_bitU_nondetS_any:
   "PrePostE (\<lambda>s. \<forall>b. Q b s) (bool_of_bitU_nondetS b) Q E"
@@ -507,11 +507,19 @@ lemma PrePostE_bools_of_bits_nondetS_any:
             PrePostE_bool_of_bitU_nondetS_any)+)
      auto
 
+lemma PrePostE_choose_boolsS_any:
+  "PrePostE (\<lambda>s. \<forall>bs. Q bs s) (choose_boolsS n) Q E"
+  unfolding choose_boolsS_def genlistS_def Let_def
+  by (rule PrePostE_weaken_post[where B = "\<lambda>_ s. \<forall>bs. Q bs s"], rule PrePostE_strengthen_pre,
+      (rule PrePostE_foreachS_invariant[OF PrePostE_strengthen_pre] PrePostE_bindS PrePostE_returnS
+            PrePostE_choose_boolS_any)+)
+     auto
+
 lemma PrePostE_internal_pick:
   "xs \<noteq> [] \<Longrightarrow> PrePostE (\<lambda>s. \<forall>x \<in> set xs. Q x s) (internal_pickS xs) Q E"
   unfolding internal_pickS_def Let_def
   by (rule PrePostE_strengthen_pre,
-      (rule PrePostE_compositeI PrePostE_atomI PrePostE_bools_of_bits_nondetS_any)+)
+      (rule PrePostE_compositeI PrePostE_atomI PrePostE_choose_boolsS_any)+)
      (auto split: option.splits)
 
 end
diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile
index 039a81f1..465b4c36 100644
--- a/lib/isabelle/Makefile
+++ b/lib/isabelle/Makefile
@@ -21,7 +21,7 @@ heap-img: thys $(EXTRA_THYS) ROOT
 ifeq ($(wildcard $(LEM_ISA_LIB)/ROOT),)
 	$(error isabelle-lib directory of Lem not found. Please set the LEM_ISA_LIB environment variable)
 endif
-	isabelle build -d $(LEM_ISA_LIB) -D .
+	isabelle build -b -d $(LEM_ISA_LIB) -D .
 
 manual: heap-img manual/Manual.thy manual/ROOT manual/document/root.tex
 	cp output/document/session_graph.pdf manual/document/Sail_session_graph.pdf
diff --git a/lib/isabelle/ROOT b/lib/isabelle/ROOT
index 545e47c4..fb73a673 100644
--- a/lib/isabelle/ROOT
+++ b/lib/isabelle/ROOT
@@ -2,7 +2,7 @@ session "Sail" = "LEM" +
   options [browser_info, document = pdf, document_output = "output"]
   sessions
     "HOL-Eisbach"
-  theories [document = false]
+  theories
     Sail2_values_lemmas
     Sail2_prompt
     Sail2_state_lemmas
diff --git a/lib/isabelle/Sail2_operators_mwords_lemmas.thy b/lib/isabelle/Sail2_operators_mwords_lemmas.thy
index fd54c93a..3e8dcb2f 100644
--- a/lib/isabelle/Sail2_operators_mwords_lemmas.thy
+++ b/lib/isabelle/Sail2_operators_mwords_lemmas.thy
@@ -55,7 +55,7 @@ lemma bool_of_bitU_monadic_simps[simp]:
   "bool_of_bitU_fail BU = Fail ''bool_of_bitU''"
   "bool_of_bitU_nondet B0 = return False"
   "bool_of_bitU_nondet B1 = return True"
-  "bool_of_bitU_nondet BU = undefined_bool ()"
+  "bool_of_bitU_nondet BU = choose_bool ''bool_of_bitU''"
   unfolding bool_of_bitU_fail_def bool_of_bitU_nondet_def
   by auto
 
@@ -68,7 +68,7 @@ lemma update_vec_dec_simps[simp]:
   "update_vec_dec_fail w i BU = Fail ''bool_of_bitU''"
   "update_vec_dec_nondet w i B0 = return (set_bit w (nat i) False)"
   "update_vec_dec_nondet w i B1 = return (set_bit w (nat i) True)"
-  "update_vec_dec_nondet w i BU = undefined_bool () \<bind> (\<lambda>b. return (set_bit w (nat i) b))"
+  "update_vec_dec_nondet w i BU = choose_bool ''bool_of_bitU'' \<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_nondet_def update_vec_dec_def
diff --git a/lib/isabelle/Sail2_prompt_monad_lemmas.thy b/lib/isabelle/Sail2_prompt_monad_lemmas.thy
index 25eb9f52..1fde3287 100644
--- a/lib/isabelle/Sail2_prompt_monad_lemmas.thy
+++ b/lib/isabelle/Sail2_prompt_monad_lemmas.thy
@@ -30,42 +30,22 @@ lemma All_try_catch_dom: "try_catch_dom (m, h)"
 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 Exception] = try_catch.induct
 
-datatype 'regval event =
-  (* Request to read memory *)
-    e_read_mem read_kind "bitU list" nat "memory_byte list"
-  | e_read_tag "bitU list" bitU
-  (* Write is imminent, at address lifted, of size nat *)
-  | e_write_ea write_kind "bitU list" nat
-  (* Request the result of store-exclusive *)
-  | e_excl_res bool
-  (* Request to write memory at last signalled address. Memory value should be 8
-     times the size given in ea signal *)
-  | e_write_memv "memory_byte list" bool
-  | e_write_tag "bitU list" bitU bool
-  (* Tell the system to dynamically recalculate dependency footprint *)
-  | e_footprint
-  (* Request a memory barrier *)
-  | e_barrier " barrier_kind "
-  (* Request to read register *)
-  | e_read_reg string 'regval
-  (* Request to write register *)
-  | e_write_reg string 'regval
-  | e_undefined bool
-  | e_print string
-
 inductive_set T :: "(('rv, 'a, 'e) monad \<times> 'rv event \<times> ('rv, 'a, 'e) monad) set" where
-  Read_mem: "((Read_mem rk addr sz k), e_read_mem rk addr sz v, k v) \<in> T"
-| Read_tag: "((Read_tag addr k), e_read_tag addr v, k v) \<in> T"
-| Write_ea: "((Write_ea wk addr sz k), e_write_ea wk addr sz, k) \<in> T"
-| Excl_res: "((Excl_res k), e_excl_res r, k r) \<in> T"
-| Write_memv: "((Write_memv v k), e_write_memv v r, k r) \<in> T"
-| Write_tag: "((Write_tag a v k), e_write_tag a v r, k r) \<in> T"
-| Footprint: "((Footprint k), e_footprint, k) \<in> T"
-| Barrier: "((Barrier bk k), e_barrier bk, k) \<in> T"
-| Read_reg: "((Read_reg r k), e_read_reg r v, k v) \<in> T"
-| Write_reg: "((Write_reg r v k), e_write_reg r v, k) \<in> T"
-| Undefined: "((Undefined k), e_undefined v, k v) \<in> T"
-| Print: "((Print msg k), e_print msg, k) \<in> T"
+  Read_mem: "((Read_mem rk addr sz k), E_read_mem rk addr sz v, k v) \<in> T"
+| Read_memt: "((Read_memt rk addr sz k), E_read_memt rk addr sz v, k v) \<in> T"
+| Write_ea: "((Write_ea wk addr sz k), E_write_ea wk addr sz, k) \<in> T"
+| Excl_res: "((Excl_res k), E_excl_res r, k r) \<in> T"
+| Write_mem: "((Write_mem wk addr sz v k), E_write_mem wk addr sz v r, k r) \<in> T"
+| Write_memt: "((Write_memt wk addr sz v t k), E_write_memt wk addr sz v t r, k r) \<in> T"
+| Footprint: "((Footprint k), E_footprint, k) \<in> T"
+| Barrier: "((Barrier bk k), E_barrier bk, k) \<in> T"
+| Read_reg: "((Read_reg r k), E_read_reg r v, k v) \<in> T"
+| Write_reg: "((Write_reg r v k), E_write_reg r v, k) \<in> T"
+| Choose: "((Choose descr k), E_choose descr v, k v) \<in> T"
+| Print: "((Print msg k), E_print msg, k) \<in> T"
+
+lemma emitEvent_iff_T: "emitEvent m e = Some m' \<longleftrightarrow> (m, e, m') \<in> T"
+  by (cases e) (auto simp: emitEvent_def elim: T.cases intro: T.intros split: monad.splits)
 
 inductive_set Traces :: "(('rv, 'a, 'e) monad \<times> 'rv event list \<times> ('rv, 'a, 'e) monad) set" where
   Nil: "(s, [], s) \<in> Traces"
@@ -81,38 +61,68 @@ lemmas Traces_ConsI = T.intros[THEN Step, rotated]
 inductive_cases Traces_NilE[elim]: "(s, [], s') \<in> Traces"
 inductive_cases Traces_ConsE[elim]: "(s, e # t, s') \<in> Traces"
 
+lemma runTrace_iff_Traces: "runTrace t m = Some m' \<longleftrightarrow> (m, t, m') \<in> Traces"
+  by (induction t m rule: runTrace.induct; fastforce simp: bind_eq_Some_conv emitEvent_iff_T)
+
+lemma hasTrace_iff_Traces_final: "hasTrace t m \<longleftrightarrow> (\<exists>m'. (m, t, m') \<in> Traces \<and> final m')"
+  by (auto simp: hasTrace_def runTrace_iff_Traces[symmetric] split: option.splits)
+
 lemma Traces_cases:
   fixes m :: "('rv, 'a, 'e) monad"
   assumes Run: "(m, t, m') \<in> Traces"
   obtains (Nil) a where "m = m'" and "t = []"
-  | (Read_mem) rk addr s k t' v where "m = Read_mem rk addr s k" and "t = e_read_mem rk addr s v # t'" and "(k v, t', m') \<in> Traces"
-  | (Read_tag) addr k t' v where "m = Read_tag addr k" and "t = e_read_tag addr v # t'" and "(k v, t', m') \<in> Traces"
-  | (Write_memv) val k t' v where "m = Write_memv val k" and "t = e_write_memv val v # t'" and "(k v, t', m') \<in> Traces"
-  | (Write_tag) a val k t' v where "m = Write_tag a val k" and "t = e_write_tag a val v # t'" and "(k v, t', m') \<in> Traces"
-  | (Barrier) bk k t' v where "m = Barrier bk k" and "t = e_barrier bk # t'" and "(k, t', m') \<in> Traces"
-  | (Read_reg) reg k t' v where "m = Read_reg reg k" and "t = e_read_reg reg v # t'" and "(k v, t', m') \<in> Traces"
-  | (Excl_res) k t' v where "m = Excl_res k" and "t = e_excl_res v # t'" and "(k v, t', m') \<in> Traces"
-  | (Write_ea) wk addr s k t' where "m = Write_ea wk addr s k" and "t = e_write_ea wk addr s # t'" and "(k, t', m') \<in> Traces"
-  | (Footprint) k t' where "m = Footprint k" and "t = e_footprint # t'" and "(k, t', m') \<in> Traces"
-  | (Write_reg) reg v k t' where "m = Write_reg reg v k" and "t = e_write_reg reg v # t'" and "(k, t', m') \<in> Traces"
-  | (Undefined) xs v k t' where "m = Undefined k" and "t = e_undefined v # t'" and "(k v, t', m') \<in> Traces"
-  | (Print) msg k t' where "m = Print msg k" and "t = e_print msg # t'" and "(k, t', m') \<in> Traces"
+  | (Read_mem) rk addr s k t' v where "m = Read_mem rk addr s k" and "t = E_read_mem rk addr s v # t'" and "(k v, t', m') \<in> Traces"
+  | (Read_memt) rk addr s k t' v tag where "m = Read_memt rk addr s k" and "t = E_read_memt rk addr s (v, tag) # t'" and "(k (v, tag), t', m') \<in> Traces"
+  | (Write_mem) wk addr sz val k v t' where "m = Write_mem wk addr sz val k" and "t = E_write_mem wk addr sz val v # t'" and "(k v, t', m') \<in> Traces"
+  | (Write_memt) wk addr sz val tag k t' v where "m = Write_memt wk addr sz val tag k" and "t = E_write_memt wk addr sz val tag v # t'" and "(k v, t', m') \<in> Traces"
+  | (Barrier) bk k t' v where "m = Barrier bk k" and "t = E_barrier bk # t'" and "(k, t', m') \<in> Traces"
+  | (Read_reg) reg k t' v where "m = Read_reg reg k" and "t = E_read_reg reg v # t'" and "(k v, t', m') \<in> Traces"
+  | (Excl_res) k t' v where "m = Excl_res k" and "t = E_excl_res v # t'" and "(k v, t', m') \<in> Traces"
+  | (Write_ea) wk addr s k t' where "m = Write_ea wk addr s k" and "t = E_write_ea wk addr s # t'" and "(k, t', m') \<in> Traces"
+  | (Footprint) k t' where "m = Footprint k" and "t = E_footprint # t'" and "(k, t', m') \<in> Traces"
+  | (Write_reg) reg v k t' where "m = Write_reg reg v k" and "t = E_write_reg reg v # t'" and "(k, t', m') \<in> Traces"
+  | (Choose) descr v k t' where "m = Choose descr k" and "t = E_choose descr v # t'" and "(k v, t', m') \<in> Traces"
+  | (Print) msg k t' where "m = Print msg k" and "t = E_print msg # t'" and "(k, t', m') \<in> Traces"
 proof (use Run in \<open>cases m t m' set: Traces\<close>)
   case Nil
   then show ?thesis by (auto intro: that(1))
 next
   case (Step e m'' t')
-  from \<open>(m, e, m'') \<in> T\<close> and \<open>t = e # t'\<close> and \<open>(m'', t', m') \<in> Traces\<close>
-  show ?thesis by (cases m e m'' rule: T.cases; elim that; blast)
+  note t = \<open>t = e # t'\<close>
+  note m' = \<open>(m'', t', m') \<in> Traces\<close>
+  from \<open>(m, e, m'') \<in> T\<close> and t and m'
+  show ?thesis proof (cases m e m'' rule: T.cases)
+    case (Read_memt rk addr sz k v)
+    then show ?thesis using t m' by (cases v; elim that; blast)
+  qed (elim that; blast)+
 qed
 
 abbreviation Run :: "('rv, 'a, 'e) monad \<Rightarrow> 'rv event list \<Rightarrow> 'a \<Rightarrow> bool"
   where "Run s t a \<equiv> (s, t, Done a) \<in> Traces"
 
-lemma Run_appendI:
+lemma final_cases:
+  assumes "final m"
+  obtains (Done) a where "m = Done a" | (Fail) f where "m = Fail f" | (Ex) e where "m = Exception e"
+  using assms by (cases m) (auto simp: final_def)
+
+lemma hasTraces_elim:
+  assumes "hasTrace t m"
+  obtains m' where "(m, t, m') \<in> Traces" and "final m'"
+  using assms
+  unfolding hasTrace_iff_Traces_final
+  by blast
+
+lemma hasTrace_cases:
+  assumes "hasTrace t m"
+  obtains (Run) a where "Run m t a"
+  | (Fail) f where "(m, t, Fail f) \<in> Traces"
+  | (Ex) e where "(m, t, Exception e) \<in> Traces"
+  using assms by (elim hasTraces_elim final_cases) auto
+
+lemma Traces_appendI:
   assumes "(s, t1, s') \<in> Traces"
-    and "Run s' t2 a"
-  shows "Run s (t1 @ t2) a"
+    and "(s', t2, s'') \<in> Traces"
+  shows "(s, t1 @ t2, s'') \<in> Traces"
 proof (use assms in \<open>induction t1 arbitrary: s\<close>)
   case (Cons e t1)
   then show ?case by (elim Traces_ConsE) auto
@@ -125,20 +135,188 @@ lemma bind_DoneE:
 
 lemma bind_T_cases:
   assumes "(bind m f, e, s') \<in> T"
-  obtains (Done) a where "m = Done a"
+  obtains (Done) a where "m = Done a" and "(f a, e, s') \<in> T"
   | (Bind) m' where "s' = bind m' f" and "(m, e, m') \<in> T"
-  using assms by (cases; blast elim: bind.elims)
+  using assms by (cases; fastforce elim: bind.elims)
 
-lemma Run_bindI:
+lemma Traces_bindI:
   fixes m :: "('r, 'a, 'e) monad"
   assumes "Run m t1 a1"
-    and "Run (f a1) t2 a2"
-  shows "Run (m \<bind> f) (t1 @ t2) a2"
+    and "(f a1, t2, m') \<in> Traces"
+  shows "(m \<bind> f, t1 @ t2, m') \<in> Traces"
 proof (use assms in \<open>induction m t1 "Done a1 :: ('r, 'a, 'e) monad" rule: Traces.induct\<close>)
   case (Step s e s'' t)
   then show ?case by (elim T.cases) auto
 qed auto
 
+lemma Run_DoneE:
+  assumes "Run (Done a) t a'"
+  obtains "t = []" and "a' = a"
+  using assms by (auto elim: Traces.cases T.cases)
+
+lemma Run_Done_iff_Nil[simp]: "Run (Done a) t a' \<longleftrightarrow> t = [] \<and> a' = a"
+  by (auto elim: Run_DoneE)
+
+lemma Run_Nil_iff_Done: "Run m [] a \<longleftrightarrow> m = Done a"
+  by auto
+
+lemma Traces_Nil_iff: "(m, [], m') \<in> Traces \<longleftrightarrow> m' = m"
+  by auto
+
+lemma bind_Traces_cases:
+  assumes "(m \<bind> f, t, m') \<in> Traces"
+  obtains (Left) m'' where "(m, t, m'') \<in> Traces" and "m' = m'' \<bind> f"
+  | (Bind) tm am tf where "t = tm @ tf" and "Run m tm am" and "(f am, tf, m') \<in> Traces"
+proof (use assms in \<open>induction "bind m f" t m' arbitrary: m rule: Traces.induct\<close>)
+  case Nil
+  then show ?case by (auto simp: Traces_Nil_iff)
+next
+  case (Step e s'' t s')
+  note IH = Step(3)
+  note Left' = Step(4)
+  note Bind' = Step(5)
+  show thesis
+  proof (use \<open>(m \<bind> f, e, s'') \<in> T\<close> in \<open>cases rule: bind_T_cases\<close>)
+    case (Done a)
+    then show ?thesis using \<open>(s'', t, s') \<in> Traces\<close> Step(5)[of "[]" "e # t" a] by auto
+  next
+    case (Bind m')
+    show ?thesis
+    proof (rule IH)
+      show "s'' = m' \<bind> f" using Bind by blast
+    next
+      fix m''
+      assume "(m', t, m'') \<in> Traces" and "s' = m'' \<bind> f"
+      then show thesis using \<open>(m, e, m') \<in> T\<close> Left'[of m''] by auto
+    next
+      fix tm tf am
+      assume "t = tm @ tf" and "Run m' tm am" and "(f am, tf, s') \<in> Traces"
+      then show thesis using \<open>(m, e, m') \<in> T\<close> Bind'[of "e # tm" tf am] by auto
+    qed
+  qed
+qed
+
+lemma final_bind_cases:
+  assumes "final (m \<bind> f)"
+  obtains (Done) a where "m = Done a" and "final (f a)"
+  | (Fail) msg where "m = Fail msg"
+  | (Ex) e where "m = Exception e"
+  using assms by (cases m) (auto simp: final_def)
+
+lemma hasFailure_iff_Traces_Fail: "hasFailure t m \<longleftrightarrow> (\<exists>msg. (m, t, Fail msg) \<in> Traces)"
+  by (auto simp: hasFailure_def runTrace_iff_Traces[symmetric] split: option.splits monad.splits)
+
+lemma hasException_iff_Traces_Exception: "hasException t m \<longleftrightarrow> (\<exists>e. (m, t, Exception e) \<in> Traces)"
+  by (auto simp: hasException_def runTrace_iff_Traces[symmetric] split: option.splits monad.splits)
+
+lemma hasTrace_bind_cases:
+  assumes "hasTrace t (m \<bind> f)"
+  obtains (Bind) tm am tf where "t = tm @ tf" and "Run m tm am" and "hasTrace tf (f am)"
+  | (Fail) "hasFailure t m"
+  | (Ex) "hasException t m"
+proof -
+  from assms obtain m' where t: "(m \<bind> f, t, m') \<in> Traces" and m': "final m'"
+    by (auto simp: hasTrace_iff_Traces_final)
+  note [simp] = hasTrace_iff_Traces_final hasFailure_iff_Traces_Fail hasException_iff_Traces_Exception
+  from t show thesis
+  proof (cases rule: bind_Traces_cases)
+    case (Left m'')
+    then show ?thesis
+      using m' Fail Ex Bind[of t "[]"]
+      by (fastforce elim!: final_bind_cases)
+  next
+    case (Bind tm am tf)
+    then show ?thesis
+      using m' that
+      by fastforce
+  qed
+qed
+
+lemma try_catch_T_cases:
+  assumes "(try_catch m h, e, m') \<in> T"
+  obtains (NoEx) m'' where "(m, e, m'') \<in> T" and "m' = try_catch m'' h"
+  | (Ex) ex where "m = Exception ex" and "(h ex, e, m') \<in> T"
+  using assms
+  by (cases m) (auto elim!: T.cases)
+
+lemma try_catch_Traces_cases:
+  assumes "(try_catch m h, t, mtc) \<in> Traces"
+  obtains (NoEx) m' where "(m, t, m') \<in> Traces" and "mtc = try_catch m' h"
+  | (Ex) tm ex th where "(m, tm, Exception ex) \<in> Traces" and "(h ex, th, mtc) \<in> Traces" and "t = tm @ th"
+proof (use assms in \<open>induction "try_catch m h" t mtc arbitrary: m rule: Traces.induct\<close>)
+  case Nil
+  then show ?case by auto
+next
+  case (Step e mtc' t mtc)
+  note e = \<open>(try_catch m h, e, mtc') \<in> T\<close>
+  note t = \<open>(mtc', t, mtc) \<in> Traces\<close>
+  note IH = Step(3)
+  note NoEx_ConsE = Step(4)
+  note Ex_ConsE = Step(5)
+  show ?case
+  proof (use e in \<open>cases rule: try_catch_T_cases\<close>)
+    case (NoEx m1)
+    show ?thesis
+    proof (rule IH)
+      show "mtc' = try_catch m1 h" using NoEx by auto
+    next
+      fix m'
+      assume "(m1, t, m') \<in> Traces" and "mtc = try_catch m' h"
+      then show ?thesis
+        using NoEx NoEx_ConsE[of m']
+        by auto
+    next
+      fix tm ex th
+      assume "(m1, tm, Exception ex) \<in> Traces" and "(h ex, th, mtc) \<in> Traces" and "t = tm @ th"
+      then show ?thesis
+        using NoEx Ex_ConsE[of "e # tm" ex th]
+        by auto
+    qed
+  next
+    case (Ex ex)
+    then show ?thesis
+      using t Ex_ConsE[of "[]" ex "e # t"]
+      by auto
+  qed
+qed
+
+lemma Done_Traces_iff[simp]: "(Done a, t, m') \<in> Traces \<longleftrightarrow> t = [] \<and> m' = Done a"
+  by (auto elim: Traces_cases)
+
+lemma Fail_Traces_iff[simp]: "(Fail msg, t, m') \<in> Traces \<longleftrightarrow> t = [] \<and> m' = Fail msg"
+  by (auto elim: Traces_cases)
+
+lemma Exception_Traces_iff[simp]: "(Exception e, t, m') \<in> Traces \<longleftrightarrow> t = [] \<and> m' = Exception e"
+  by (auto elim: Traces_cases)
+
+lemma Read_reg_TracesE:
+  assumes "(Read_reg r k, t, m') \<in> Traces"
+  obtains (Nil) "t = []" and "m' = Read_reg r k"
+  | (Cons) v t' where "t = E_read_reg r v # t'" and "(k v, t', m') \<in> Traces"
+  using assms
+  by (auto elim: Traces_cases)
+
+lemma Write_reg_TracesE:
+  assumes "(Write_reg r v k, t, m') \<in> Traces"
+  obtains (Nil) "t = []" and "m' = Write_reg r v k"
+  | (Cons) t' where "t = E_write_reg r v # t'" and "(k, t', m') \<in> Traces"
+  using assms
+  by (auto elim: Traces_cases)
+
+lemma Write_ea_TracesE:
+  assumes "(Write_ea wk addr sz k, t, m') \<in> Traces"
+  obtains (Nil) "t = []" and "m' = Write_ea wk addr sz k"
+  | (Cons) t' where "t = E_write_ea wk addr sz # t'" and "(k, t', m') \<in> Traces"
+  using assms
+  by (auto elim: Traces_cases)
+
+lemma Write_memt_TracesE:
+  assumes "(Write_memt wk addr sz v tag k, t, m') \<in> Traces"
+  obtains (Nil) "t = []" and "m' = Write_memt wk addr sz v tag k"
+  | (Cons) t' r where "t = E_write_memt wk addr sz v tag r # t'" and "(k r, t', m') \<in> Traces"
+  using assms
+  by (auto elim: Traces_cases)
+
 lemma Run_bindE:
   fixes m :: "('rv, 'b, 'e) monad" and a :: 'a
   assumes "Run (bind m f) t a"
@@ -163,14 +341,6 @@ next
   qed
 qed
 
-lemma Run_DoneE:
-  assumes "Run (Done a) t a'"
-  obtains "t = []" and "a' = a"
-  using assms by (auto elim: Traces.cases T.cases)
-
-lemma Run_Done_iff_Nil[simp]: "Run (Done a) t a' \<longleftrightarrow> t = [] \<and> a' = a"
-  by (auto elim: Run_DoneE)
-
 lemma Run_bindE_ignore_trace:
   assumes "Run (m \<bind> f) t a"
   obtains tm tf am where "Run m tm am" and "Run (f am) tf a"
@@ -205,8 +375,10 @@ lemma bind_cong[fundef_cong]:
 
 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 try_catch_choose_bool[simp]: "try_catch (choose_bool descr) h = choose_bool descr" by (auto simp: choose_bool_def)
+lemma liftR_choose_bool[simp]: "liftR (choose_bool descr) = choose_bool descr" by (auto simp: choose_bool_def liftR_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 liftR_undefined_bool[simp]: "liftR (undefined_bool ()) = undefined_bool ()" by (auto simp: undefined_bool_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 ba69d0d8..8b189f7a 100644
--- a/lib/isabelle/Sail2_state_lemmas.thy
+++ b/lib/isabelle/Sail2_state_lemmas.thy
@@ -2,6 +2,8 @@ theory Sail2_state_lemmas
   imports Sail2_state Sail2_state_lifting
 begin
 
+text \<open>Monad lifting\<close>
+
 lemma All_liftState_dom: "liftState_dom (r, m)"
   by (induction m) (auto intro: liftState.domintros)
 termination liftState using All_liftState_dom by auto
@@ -18,7 +20,7 @@ lemma Value_liftState_Run:
   assumes "(Value a, s') \<in> liftState r m s"
   obtains t where "Run m t a"
   by (use assms in \<open>induction r m arbitrary: s s' rule: liftState.induct\<close>;
-      auto simp add: failS_def throwS_def returnS_def simp del: read_regvalS.simps;
+      simp add: failS_def throwS_def returnS_def del: read_regvalS.simps;
       blast elim: Value_bindS_elim)
 
 lemmas liftState_if_distrib[liftState_simp] = if_distrib[where f = "liftState ra" for ra]
@@ -43,6 +45,9 @@ lemma liftState_barrier[liftState_simp]: "liftState r (barrier bk) = returnS ()"
   by (auto simp: barrier_def)
 lemma liftState_footprint[liftState_simp]: "liftState r (footprint ()) = returnS ()"
   by (auto simp: footprint_def)
+lemma liftState_choose_bool[liftState_simp]: "liftState r (choose_bool descr) = choose_boolS ()"
+  by (auto simp: choose_bool_def liftState_simp)
+declare undefined_boolS_def[simp]
 lemma liftState_undefined[liftState_simp]: "liftState r (undefined_bool ()) = undefined_boolS ()"
   by (auto simp: undefined_bool_def liftState_simp)
 lemma liftState_maybe_fail[liftState_simp]: "liftState r (maybe_fail msg x) = maybe_failS msg x"
@@ -78,30 +83,44 @@ lemma liftState_bool_of_bitU_nondet[liftState_simp]:
   "liftState r (bool_of_bitU_nondet b) = bool_of_bitU_nondetS b"
   by (cases b; auto simp: bool_of_bitU_nondet_def bool_of_bitU_nondetS_def liftState_simp)
 
-lemma liftState_read_mem_BC:
-  assumes "unsigned_method BC_bitU_list (bits_of_method BCa a) = unsigned_method BCa a"
-  shows "liftState r (read_mem BCa BCb rk a sz) = read_memS BCa BCb rk a sz"
-  using assms
-  by (auto simp: read_mem_def read_mem_bytes_def read_memS_def read_mem_bytesS_def maybe_failS_def liftState_simp split: option.splits)
+lemma liftState_read_memt[liftState_simp]:
+  shows "liftState r (read_memt BCa BCb rk a sz) = read_memtS BCa BCb rk a sz"
+  by (auto simp: read_memt_def read_memt_bytes_def maybe_failS_def read_memtS_def
+                 prod.case_distrib option.case_distrib[where h = "liftState r"]
+                 option.case_distrib[where h = "\<lambda>c. c \<bind>\<^sub>S f" for f] liftState_simp
+           split: option.splits intro: bindS_cong)
 
 lemma liftState_read_mem[liftState_simp]:
-  "\<And>a. liftState r (read_mem BC_mword BC_mword rk a sz) = read_memS BC_mword BC_mword rk a sz"
-  "\<And>a. liftState r (read_mem BC_bitU_list BC_bitU_list rk a sz) = read_memS BC_bitU_list BC_bitU_list rk a sz"
-  by (auto simp: liftState_read_mem_BC)
+  shows "liftState r (read_mem BCa BCb rk a sz) = read_memS BCa BCb rk a sz"
+  by (auto simp: read_mem_def read_mem_bytes_def read_memS_def read_mem_bytesS_def maybe_failS_def
+                 read_memtS_def
+                 prod.case_distrib option.case_distrib[where h = "liftState r"]
+                 option.case_distrib[where h = "\<lambda>c. c \<bind>\<^sub>S f" for f] liftState_simp
+           split: option.splits intro: bindS_cong)
 
 lemma liftState_write_mem_ea_BC:
-  assumes "unsigned_method BC_bitU_list (bits_of_method BCa a) = unsigned_method BCa a"
-  shows "liftState r (write_mem_ea BCa rk a sz) = write_mem_eaS BCa rk a (nat sz)"
-  using assms by (auto simp: write_mem_ea_def write_mem_eaS_def)
+  assumes "unsigned_method BCa a = Some a'"
+  shows "liftState r (write_mem_ea BCa rk a sz) = returnS ()"
+  using assms by (auto simp: write_mem_ea_def nat_of_bv_def maybe_fail_def)
 
-lemma liftState_write_mem_ea[liftState_simp]:
-  "\<And>a. liftState r (write_mem_ea BC_mword rk a sz) = write_mem_eaS BC_mword rk a (nat sz)"
-  "\<And>a. liftState r (write_mem_ea BC_bitU_list rk a sz) = write_mem_eaS BC_bitU_list rk a (nat sz)"
-  by (auto simp: liftState_write_mem_ea_BC)
+(*lemma liftState_write_mem_ea[liftState_simp]:
+  "\<And>a. liftState r (write_mem_ea BC_mword rk a sz) = returnS ()"
+  "\<And>a. liftState r (write_mem_ea BC_bitU_list rk a sz) = returnS ()"
+  by (auto simp: liftState_write_mem_ea_BC)*)
 
-lemma liftState_write_mem_val[liftState_simp]:
-  "liftState r (write_mem_val BC v) = write_mem_valS BC v"
-  by (auto simp: write_mem_val_def write_mem_valS_def liftState_simp split: option.splits)
+(*lemma write_mem_bytesS_def_BC_bitU_list_BC_mword[simp]:
+  "write_mem_bytesS BC_bitU_list wk (bits_of_method BC_mword addr) sz v t =
+   write_mem_bytesS BC_mword wk addr sz v t"
+  by (auto simp: write_mem_bytesS_def)*)
+
+lemma liftState_write_memt[liftState_simp]:
+  "liftState r (write_memt BCa BCv wk addr sz v t) = write_memtS BCa BCv wk addr sz v t"
+  by (auto simp: write_memt_def write_memtS_def liftState_simp split: option.splits)
+
+lemma liftState_write_mem[liftState_simp]:
+  "liftState r (write_mem BCa BCv wk addr sz v) = write_memS BCa BCv wk addr sz v"
+  by (auto simp: write_mem_def write_memS_def write_memtS_def write_mem_bytesS_def liftState_simp
+           split: option.splits)
 
 lemma liftState_read_reg_readS:
   assumes "\<And>s. Option.bind (get_regval' (name reg) s) (of_regval reg) = Some (read_from reg s)"
@@ -138,6 +157,14 @@ lemma liftState_foreachM[liftState_simp]:
   by (induction xs vars "\<lambda>x vars. liftState r (body x vars)" rule: foreachS.induct)
      (auto simp: liftState_simp cong: bindS_cong)
 
+lemma liftState_genlistM[liftState_simp]:
+  "liftState r (genlistM f n) = genlistS (liftState r \<circ> f) n"
+  by (auto simp: genlistM_def genlistS_def liftState_simp cong: bindS_cong)
+
+lemma liftState_choose_bools[liftState_simp]:
+  "liftState r (choose_bools descr n) = choose_boolsS n"
+  by (auto simp: choose_bools_def choose_boolsS_def liftState_simp comp_def)
+
 lemma liftState_bools_of_bits_nondet[liftState_simp]:
   "liftState r (bools_of_bits_nondet bs) = bools_of_bits_nondetS bs"
   unfolding bools_of_bits_nondet_def bools_of_bits_nondetS_def
@@ -146,6 +173,7 @@ lemma liftState_bools_of_bits_nondet[liftState_simp]:
 lemma liftState_internal_pick[liftState_simp]:
   "liftState r (internal_pick xs) = internal_pickS xs"
   by (auto simp: internal_pick_def internal_pickS_def liftState_simp comp_def
+                 chooseM_def
                  option.case_distrib[where h = "liftState r"]
            simp del: repeat.simps
            cong: option.case_cong)
@@ -301,7 +329,7 @@ proof (use assms in \<open>induction vars "liftState r \<circ> cond" "liftState
   qed auto
 qed
 
-(* Simplification rules for monadic Boolean connectives *)
+text \<open>Simplification rules for monadic Boolean connectives\<close>
 
 lemma if_return_return[simp]: "(if a then return True else return False) = return a" by auto
 
@@ -384,4 +412,125 @@ lemma Run_and_boolM_E:
 lemma maybe_failS_Some[simp]: "maybe_failS msg (Some v) = returnS v"
   by (auto simp: maybe_failS_def)
 
+text \<open>Event traces\<close>
+
+lemma Some_eq_bind_conv: "Some x = Option.bind f g \<longleftrightarrow> (\<exists>y. f = Some y \<and> g y = Some x)"
+  unfolding bind_eq_Some_conv[symmetric] by auto
+
+lemma if_then_Some_eq_Some_iff: "((if b then Some x else None) = Some y) \<longleftrightarrow> (b \<and> y = x)"
+  by auto
+
+lemma Some_eq_if_then_Some_iff: "(Some y = (if b then Some x else None)) \<longleftrightarrow> (b \<and> y = x)"
+  by auto
+
+lemma emitEventS_update_cases:
+  assumes "emitEventS ra e s = Some s'"
+  obtains
+    (Write_mem) wk addr sz v tag r
+      where "e = E_write_memt wk addr sz v tag r \<or> (e = E_write_mem wk addr sz v r \<and> tag = B0)"
+        and "s' = put_mem_bytes addr sz v tag s"
+  | (Write_reg) r v rs'
+      where "e = E_write_reg r v" and "(snd ra) r v (regstate s) = Some rs'"
+        and "s' = s\<lparr>regstate := rs'\<rparr>"
+  | (Read) "s' = s"
+  using assms
+  by (elim emitEventS.elims)
+     (auto simp: Some_eq_bind_conv bind_eq_Some_conv if_then_Some_eq_Some_iff Some_eq_if_then_Some_iff)
+
+lemma runTraceS_singleton[simp]: "runTraceS ra [e] s = emitEventS ra e s"
+  by (cases "emitEventS ra e s"; auto)
+
+lemma runTraceS_ConsE:
+  assumes "runTraceS ra (e # t) s = Some s'"
+  obtains s'' where "emitEventS ra e s = Some s''" and "runTraceS ra t s'' = Some s'"
+  using assms by (auto simp: bind_eq_Some_conv)
+
+lemma runTraceS_ConsI:
+  assumes "emitEventS ra e s = Some s'" and "runTraceS ra t s' = Some s''"
+  shows "runTraceS ra (e # t) s = Some s''"
+  using assms by auto
+
+lemma runTraceS_Cons_tl:
+  assumes "emitEventS ra e s = Some s'"
+  shows "runTraceS ra (e # t) s = runTraceS ra t s'"
+  using assms by (elim emitEventS.elims) (auto simp: Some_eq_bind_conv bind_eq_Some_conv)
+
+lemma runTraceS_appendE:
+  assumes "runTraceS ra (t @ t') s = Some s'"
+  obtains s'' where "runTraceS ra t s = Some s''" and "runTraceS ra t' s'' = Some s'"
+proof -
+  have "\<exists>s''. runTraceS ra t s = Some s'' \<and> runTraceS ra t' s'' = Some s'"
+  proof (use assms in \<open>induction t arbitrary: s\<close>)
+    case (Cons e t)
+    from Cons.prems
+    obtain s_e where "emitEventS ra e s = Some s_e" and "runTraceS ra (t @ t') s_e = Some s'"
+      by (auto elim: runTraceS_ConsE simp: bind_eq_Some_conv)
+    with Cons.IH[of s_e] show ?case by (auto intro: runTraceS_ConsI)
+  qed auto
+  then show ?thesis using that by blast
+qed
+
+lemma runTraceS_nth_split:
+  assumes "runTraceS ra t s = Some s'" and n: "n < length t"
+  obtains s1 s2 where "runTraceS ra (take n t) s = Some s1"
+    and "emitEventS ra (t ! n) s1 = Some s2"
+    and "runTraceS ra (drop (Suc n) t) s2 = Some s'"
+proof -
+  have "runTraceS ra (take n t @ t ! n # drop (Suc n) t) s = Some s'"
+    using assms
+    by (auto simp: id_take_nth_drop[OF n, symmetric])
+  then show thesis by (blast elim: runTraceS_appendE runTraceS_ConsE intro: that)
+qed
+
+text \<open>Memory accesses\<close>
+
+lemma get_mem_bytes_put_mem_bytes_same_addr:
+  assumes "length v = sz"
+  shows "get_mem_bytes addr sz (put_mem_bytes addr sz v tag s) = Some (v, if sz > 0 then tag else B1)"
+proof (unfold assms[symmetric], induction v rule: rev_induct)
+  case Nil
+  then show ?case by (auto simp: get_mem_bytes_def)
+next
+  case (snoc x xs)
+  then show ?case
+    by (cases tag)
+       (auto simp: get_mem_bytes_def put_mem_bytes_def Let_def and_bit_eq_iff foldl_and_bit_eq_iff
+             cong: option.case_cong split: if_splits option.splits)
+qed
+
+lemma memstate_put_mem_bytes:
+  assumes "length v = sz"
+  shows "memstate (put_mem_bytes addr sz v tag s) addr' =
+         (if addr' \<in> {addr..<addr+sz} then Some (v ! (addr' - addr)) else memstate s addr')"
+  unfolding assms[symmetric]
+  by (induction v rule: rev_induct) (auto simp: put_mem_bytes_def nth_Cons nth_append Let_def)
+
+lemma tagstate_put_mem_bytes:
+  assumes "length v = sz"
+  shows "tagstate (put_mem_bytes addr sz v tag s) addr' =
+         (if addr' \<in> {addr..<addr+sz} then Some tag else tagstate s addr')"
+  unfolding assms[symmetric]
+  by (induction v rule: rev_induct) (auto simp: put_mem_bytes_def nth_Cons nth_append Let_def)
+
+lemma get_mem_bytes_cong:
+  assumes "\<forall>addr'. addr \<le> addr' \<and> addr' < addr + sz \<longrightarrow>
+                   (memstate s' addr' = memstate s addr' \<and> tagstate s' addr' = tagstate s addr')"
+  shows "get_mem_bytes addr sz s' = get_mem_bytes addr sz s"
+proof (use assms in \<open>induction sz\<close>)
+  case 0
+  then show ?case by (auto simp: get_mem_bytes_def)
+next
+  case (Suc sz)
+  then show ?case
+    by (auto simp: get_mem_bytes_def Let_def
+             intro!: map_option_cong map_cong foldl_cong
+                     arg_cong[where f = just_list] arg_cong2[where f = and_bit])
+qed
+
+lemma get_mem_bytes_tagged_tagstate:
+  assumes "get_mem_bytes addr sz s = Some (v, B1)"
+  shows "\<forall>addr' \<in> {addr..<addr + sz}. tagstate s addr' = Some B1"
+  using assms
+  by (auto simp: get_mem_bytes_def foldl_and_bit_eq_iff Let_def split: option.splits)
+
 end
diff --git a/lib/isabelle/Sail2_state_monad_lemmas.thy b/lib/isabelle/Sail2_state_monad_lemmas.thy
index 3a286c10..1e9f50cc 100644
--- a/lib/isabelle/Sail2_state_monad_lemmas.thy
+++ b/lib/isabelle/Sail2_state_monad_lemmas.thy
@@ -38,10 +38,9 @@ lemma bindS_updateS: "bindS (updateS f) m = (\<lambda>s. m () (f s))"
 lemma bindS_assertS_True[simp]: "bindS (assert_expS True msg) f = f ()"
   by (auto simp: assert_expS_def)
 
-lemma bindS_chooseS_returnS[simp]: "bindS (chooseS xs) (\<lambda>x. returnS (f x)) = chooseS (f ` xs)"
+lemma bindS_chooseS_returnS[simp]: "bindS (chooseS xs) (\<lambda>x. returnS (f x)) = chooseS (map f xs)"
   by (intro ext) (auto simp: bindS_def chooseS_def returnS_def)
 
-
 lemma result_cases:
   fixes r :: "('a, 'e) result"
   obtains (Value) a where "r = Value a"
@@ -198,31 +197,37 @@ lemma no_throw_basic_builtins[simp]:
   "\<And>f. ignore_throw (readS f) = readS f"
   "\<And>f. ignore_throw (updateS f) = updateS f"
   "ignore_throw (chooseS xs) = chooseS xs"
+  "ignore_throw (choose_boolS ()) = choose_boolS ()"
   "ignore_throw (failS msg) = failS msg"
   "ignore_throw (maybe_failS msg x) = maybe_failS msg x"
-  unfolding ignore_throw_def returnS_def chooseS_def maybe_failS_def failS_def readS_def updateS_def
+  unfolding ignore_throw_def returnS_def chooseS_def maybe_failS_def failS_def readS_def updateS_def choose_boolS_def
   by (intro ext; auto split: option.splits)+
 
 lemmas ignore_throw_option_case_distrib =
   option.case_distrib[where h = "\<lambda>c. ignore_throw c s" and option = "c s" for c s]
+  option.case_distrib[where h = "\<lambda>c. ignore_throw c" and option = "c" for c]
+
+lemma ignore_throw_let_distrib: "ignore_throw (let x = y in f x) = (let x = y in ignore_throw (f x))"
+  by auto
 
 lemma no_throw_mem_builtins:
-  "\<And>BC rk a sz s. ignore_throw (read_mem_bytesS BC rk a sz) s = read_mem_bytesS BC rk a sz s"
+  "\<And>rk a sz s. ignore_throw (read_mem_bytesS rk a sz) s = read_mem_bytesS rk a sz s"
+  "\<And>rk a sz s. ignore_throw (read_memt_bytesS rk a sz) s = read_memt_bytesS rk a sz s"
   "\<And>BC a s. ignore_throw (read_tagS BC a) s = read_tagS BC a s"
-  "\<And>BC wk a sz s. ignore_throw (write_mem_eaS BC wk a sz) s = write_mem_eaS BC wk a sz s"
-  "\<And>v s. ignore_throw (write_mem_bytesS v) s = write_mem_bytesS v s"
-  "\<And>BC v s. ignore_throw (write_mem_valS BC v) s = write_mem_valS BC v s"
-  "\<And>BC a t s. ignore_throw (write_tagS BC a t) s = write_tagS BC a t s"
+  "\<And>BCa BCv rk a sz s. ignore_throw (read_memS BCa BCv rk a sz) s = read_memS BCa BCv rk a sz s"
+  "\<And>BCa BCv rk a sz s. ignore_throw (read_memtS BCa BCv rk a sz) s = read_memtS BCa BCv rk a sz s"
+  "\<And>BC wk addr sz v s. ignore_throw (write_mem_bytesS wk addr sz v) s = write_mem_bytesS wk addr sz v s"
+  "\<And>BC wk addr sz v t s. ignore_throw (write_memt_bytesS wk addr sz v t) s = write_memt_bytesS wk addr sz v t s"
+  "\<And>BCa BCv wk addr sz v s. ignore_throw (write_memS BCa BCv wk addr sz v) s = write_memS BCa BCv wk addr sz v s"
+  "\<And>BCa BCv wk addr sz v t s. ignore_throw (write_memtS BCa BCv wk addr sz v t) s = write_memtS BCa BCv wk addr sz v t s"
   "\<And>s. ignore_throw (excl_resultS ()) s = excl_resultS () s"
   "\<And>s. ignore_throw (undefined_boolS ()) s = undefined_boolS () s"
-  unfolding read_mem_bytesS_def read_memS_def read_tagS_def write_mem_eaS_def
-  unfolding write_mem_valS_def write_mem_bytesS_def write_tagS_def
-  unfolding excl_resultS_def undefined_boolS_def
+  unfolding read_mem_bytesS_def read_memt_bytesS_def read_memtS_def read_memS_def read_tagS_def
+  unfolding write_memS_def write_memtS_def write_mem_bytesS_def write_memt_bytesS_def
+  unfolding excl_resultS_def undefined_boolS_def maybe_failS_def
+  unfolding ignore_throw_bindS
   by (auto cong: bindS_cong bindS_ext_cong ignore_throw_cong option.case_cong
-           simp: option.case_distrib prod.case_distrib ignore_throw_option_case_distrib comp_def)
-
-lemma no_throw_read_memS: "ignore_throw (read_memS BCa BCb rk a sz) s = read_memS BCa BCb rk a sz s"
-  by (auto simp: read_memS_def no_throw_mem_builtins cong: bindS_ext_cong)
+           simp: prod.case_distrib ignore_throw_option_case_distrib ignore_throw_let_distrib comp_def)
 
 lemma no_throw_read_regvalS: "ignore_throw (read_regvalS r reg_name) s = read_regvalS r reg_name s"
   by (cases r) (auto simp: option.case_distrib cong: bindS_cong option.case_cong)
@@ -231,7 +236,7 @@ lemma no_throw_write_regvalS: "ignore_throw (write_regvalS r reg_name v) s = wri
   by (cases r) (auto simp: option.case_distrib cong: bindS_cong option.case_cong)
 
 lemmas no_throw_builtins[simp] =
-  no_throw_mem_builtins no_throw_read_regvalS no_throw_write_regvalS no_throw_read_memS
+  no_throw_mem_builtins no_throw_read_regvalS no_throw_write_regvalS
 
 (* end *)
 
diff --git a/lib/isabelle/Sail2_values_lemmas.thy b/lib/isabelle/Sail2_values_lemmas.thy
index 576cd8ea..27a6952f 100644
--- a/lib/isabelle/Sail2_values_lemmas.thy
+++ b/lib/isabelle/Sail2_values_lemmas.thy
@@ -123,6 +123,9 @@ lemma nth_upto[simp]: "i + int n \<le> j \<Longrightarrow> [i..j] ! n = i + int
 
 declare index_list.simps[simp del]
 
+lemma genlist_add_upt[simp]: "genlist ((+) start) len = [start..<start + len]"
+  by (auto simp: genlist_def map_add_upt add.commute cong: map_cong)
+
 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 \<longleftrightarrow> None \<in> set xs"
@@ -151,6 +154,31 @@ next
   then show ?case by (auto simp: repeat.simps)
 qed
 
+lemma and_bit_B1[simp]: "and_bit B1 b = b"
+  by (cases b) auto
+
+lemma and_bit_idem[simp]: "and_bit b b = b"
+  by (cases b) auto
+
+lemma and_bit_eq_iff:
+  "and_bit b b' = B0 \<longleftrightarrow> (b = B0 \<or> b' = B0)"
+  "and_bit b b' = BU \<longleftrightarrow> (b = BU \<or> b' = BU) \<and> b \<noteq> B0 \<and> b' \<noteq> B0"
+  "and_bit b b' = B1 \<longleftrightarrow> (b = B1 \<and> b' = B1)"
+  by (cases b; cases b'; auto)+
+
+lemma foldl_and_bit_eq_iff:
+  shows "foldl and_bit b bs = B0 \<longleftrightarrow> (b = B0 \<or> B0 \<in> set bs)" (is ?B0)
+    and "foldl and_bit b bs = B1 \<longleftrightarrow> (b = B1 \<and> set bs \<subseteq> {B1})" (is ?B1)
+    and "foldl and_bit b bs = BU \<longleftrightarrow> (b = BU \<or> BU \<in> set bs) \<and> b \<noteq> B0 \<and> B0 \<notin> set bs" (is ?BU)
+proof -
+  have "?B0 \<and> ?B1 \<and> ?BU"
+  proof (induction bs arbitrary: b)
+    case (Cons b' bs)
+    show ?case using Cons.IH by (cases b; cases b') auto
+  qed auto
+  then show ?B0 and ?B1 and ?BU by auto
+qed
+
 lemma bool_of_bitU_simps[simp]:
   "bool_of_bitU B0 = Some False"
   "bool_of_bitU B1 = Some True"
diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail
index 93ad3db5..90d74149 100644
--- a/lib/mono_rewrites.sail
+++ b/lib/mono_rewrites.sail
@@ -19,13 +19,9 @@ 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 extzv = "extz_vec" : forall 'n 'm. (implicit('m), vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
 
-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)
+val extsv = "exts_vec" : forall 'n 'm. (implicit('m), vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
 
 /* This is generated internally to deal with case splits which reveal the size
    of a bitvector */
@@ -34,9 +30,9 @@ val bitvector_cast_out = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect p
 
 /* 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
+val slice_mask : forall 'n, 'n >= 0. (implicit('n), int, int) -> bits('n) effect pure
+function slice_mask(n,i,l) =
+  let one : bits('n) = extzv(n, 0b1) in
   ((one << l) - one) << i
 
 val is_zero_subrange : forall 'n, 'n >= 0.
@@ -46,6 +42,13 @@ function is_zero_subrange (xs, i, j) = {
   (xs & slice_mask(j, i-j+1)) == extzv(0b0)
 }
 
+val is_zeros_slice : forall 'n, 'n >= 0.
+  (bits('n), int, int) -> bool effect pure
+
+function is_zeros_slice (xs, i, l) = {
+  (xs & slice_mask(i, l)) == extzv(0b0)
+}
+
 val is_ones_subrange : forall 'n, 'n >= 0.
   (bits('n), int, int) -> bool effect pure
 
@@ -54,21 +57,29 @@ function is_ones_subrange (xs, i, j) = {
   (xs & m) == m
 }
 
+val is_ones_slice : forall 'n, 'n >= 0.
+  (bits('n), int, int) -> bool effect pure
+
+function is_ones_slice (xs, i, j) = {
+  let m : bits('n) = slice_mask(i,j) 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
+  (implicit('r), bits('n), int, int, bits('m), int, int) -> bits('r) effect pure
 
-function slice_slice_concat (xs, i, l, ys, i', l') = {
+function slice_slice_concat (r, 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)
+  extzv(r, xs) << l' | extzv(r, 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
+val slice_zeros_concat : forall 'n 'p 'q, 'n >= 0 & 'p + 'q >= 0.
+  (bits('n), int, atom('p), atom('q)) -> bits('p + 'q) effect pure
 
 function slice_zeros_concat (xs, i, l, l') = {
   let xs = (xs & slice_mask(i,l)) >> i in
-  extzv(xs) << l'
+  extzv(l + l', xs) << l'
 }
 
 /* Assumes initial vectors are of equal size */
@@ -83,44 +94,59 @@ function subrange_subrange_eq (xs, i, j, ys, i', j') = {
 }
 
 val subrange_subrange_concat : forall 'n 'o 'p 'm 'q 'r 's, 's >= 0 & 'n >= 0 & 'm >= 0.
-  (bits('n), atom('o), atom('p), bits('m), atom('q), atom('r)) -> bits('s) effect pure
+  (implicit('s), 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') = {
+function subrange_subrange_concat (s, xs, i, j, ys, i', j') = {
   let xs = (xs & slice_mask(j,i-j+1)) >> j in
   let ys = (ys & slice_mask(j',i'-j'+1)) >> j' in
-  extzv(xs) << (i' - j' + 1) | extzv(ys)
+  extzv(s, xs) << (i' - j' + 1) | extzv(s, ys)
 }
 
 val place_subrange : forall 'n 'm, 'n >= 0 & 'm >= 0.
-  (bits('n), int, int, int) -> bits('m) effect pure
+  (implicit('m), bits('n), int, int, int) -> bits('m) effect pure
 
-function place_subrange(xs,i,j,shift) = {
+function place_subrange(m,xs,i,j,shift) = {
   let xs = (xs & slice_mask(j,i-j+1)) >> j in
-  extzv(xs) << shift
+  extzv(m, xs) << shift
 }
 
 val place_slice : forall 'n 'm, 'n >= 0 & 'm >= 0.
-  (bits('n), int, int, int) -> bits('m) effect pure
+  (implicit('m), bits('n), int, int, int) -> bits('m) effect pure
 
-function place_slice(xs,i,l,shift) = {
+function place_slice(m,xs,i,l,shift) = {
   let xs = (xs & slice_mask(i,l)) >> i in
-  extzv(xs) << shift
+  extzv(m, xs) << shift
+}
+
+val set_slice_zeros : forall 'n, 'n >= 0.
+  (atom('n), int, bits('n), int) -> bits('n) effect pure
+
+function set_slice_zeros(n, i, xs, l) = {
+  let ys : bits('n) = slice_mask(n, i, l) in
+  xs & ~(ys)
 }
 
 val zext_slice : forall 'n 'm, 'n >= 0 & 'm >= 0.
-  (bits('n), int, int) -> bits('m) effect pure
+  (implicit('m), bits('n), int, int) -> bits('m) effect pure
 
-function zext_slice(xs,i,l) = {
+function zext_slice(m,xs,i,l) = {
   let xs = (xs & slice_mask(i,l)) >> i in
-  extzv(xs)
+  extzv(m, xs)
 }
 
 val sext_slice : forall 'n 'm, 'n >= 0 & 'm >= 0.
-  (bits('n), int, int) -> bits('m) effect pure
+  (implicit('m), bits('n), int, int) -> bits('m) effect pure
 
-function sext_slice(xs,i,l) = {
+function sext_slice(m,xs,i,l) = {
   let xs = arith_shiftright(((xs & slice_mask(i,l)) << ('n - i - l)), 'n - l) in
-  extsv(xs)
+  extsv(m, xs)
+}
+
+val place_slice_signed : forall 'n 'm, 'n >= 0 & 'm >= 0.
+  (implicit('m), bits('n), int, int, int) -> bits('m) effect pure
+
+function place_slice_signed(m,xs,i,l,shift) = {
+  sext_slice(m, xs, i, l) << shift
 }
 
 /* This has different names in the aarch64 prelude (UInt) and the other
@@ -150,9 +176,9 @@ function unsigned_subrange(xs,i,j) = {
 }
 
 
-val zext_ones : forall 'n, 'n >= 0. int -> bits('n) effect pure
+val zext_ones : forall 'n, 'n >= 0. (implicit('n), int) -> bits('n) effect pure
 
-function zext_ones(m) = {
+function zext_ones(n, m) = {
   let v : bits('n) = extsv(0b1) in
-  v >> ('n - m)
+  v >> (n - m)
 }
diff --git a/lib/sail.c b/lib/sail.c
index 0fcb5d55..22cc5462 100644
--- a/lib/sail.c
+++ b/lib/sail.c
@@ -292,24 +292,26 @@ bool gteq(const mpz_t op1, const mpz_t op2)
   return mpz_cmp(op1, op2) >= 0;
 }
 
-inline
 void shl_int(sail_int *rop, const sail_int op1, const sail_int op2)
 {
   mpz_mul_2exp(*rop, op1, mpz_get_ui(op2));
 }
 
-inline
 mach_int shl_mach_int(const mach_int op1, const mach_int op2)
 {
   return op1 << op2;
 }
 
-inline
 void shr_int(sail_int *rop, const sail_int op1, const sail_int op2)
 {
   mpz_fdiv_q_2exp(*rop, op1, mpz_get_ui(op2));
 }
 
+mach_int shr_mach_int(const mach_int op1, const mach_int op2)
+{
+  return op1 >> op2;
+}
+
 inline
 void undefined_int(sail_int *rop, const int n)
 {
diff --git a/lib/sail.h b/lib/sail.h
index f76ee144..a01e7ec8 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -116,6 +116,7 @@ bool gteq(const sail_int, const sail_int);
  * Left and right shift for integers
  */
 mach_int shl_mach_int(const mach_int, const mach_int);
+mach_int shr_mach_int(const mach_int, const mach_int);
 SAIL_INT_FUNCTION(shl_int, sail_int, const sail_int, const sail_int);
 SAIL_INT_FUNCTION(shr_int, sail_int, const sail_int, const sail_int);
 
diff --git a/lib/smt.sail b/lib/smt.sail
index 7006b190..d886c127 100644
--- a/lib/smt.sail
+++ b/lib/smt.sail
@@ -4,36 +4,33 @@ $define _SMT
 // see http://smtlib.cs.uiowa.edu/theories-Ints.shtml
 
 val div = {
-  smt: "div",
   ocaml: "quotient",
   lem: "integerDiv",
   c: "tdiv_int",
   coq: "ediv_with_eq"
-} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o == div('n, 'm). atom('o)}
+} : forall 'n 'm. (int('n), int('m)) -> int(div('n, 'm))
 
 overload operator / = {div}
 
 val mod = {
-  smt: "mod",
   ocaml: "modulus",
   lem: "integerMod",
   c: "tmod_int",
   coq: "emod_with_eq"
-} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o == mod('n, 'm). atom('o)}
+} : forall 'n 'm. (int('n), int('m)) -> int(mod('n, 'm))
 
 overload operator % = {mod}
 
-val abs_atom = {
-  smt : "abs",
+val abs_int = {
   ocaml: "abs_int",
   lem: "abs_int",
   c: "abs_int",
   coq: "abs_with_eq"
-} : forall 'n. atom('n) -> {'o, 'o == abs_atom('n). atom('o)}
+} : forall 'n. int('n) -> int(abs('n))
 
 $ifdef TEST
 
-let __smt_x : atom(div(4, 2)) = div(8, 4)
+let __smt_x : int(div(4, 2)) = div(8, 4)
 
 $endif
 
diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index 0e97c237..f31e4ed2 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -177,4 +177,6 @@ val signed = {
   _: "sint"
 } : forall 'n, 'n > 0. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1)
 
+overload __size = {__id, length}
+
 $endif