Add/generate Isabelle lemmas about the monad lifting

Architecture-specific lemmas about concrete registers and types are generated
and written to a file <prefix>_lemmas.thy, generic lemmas are in the
theories *_extras.thy in lib/isabelle.  In particular, State_extras contains
simplification lemmas about the lifting from prompt to state monad.

14 files changed, 684 insertions, 339 deletions

diff --git a/lib/isabelle/Prompt_monad_extras.thy b/lib/isabelle/Prompt_monad_extras.thy
index e93c6052..9d29f5a2 100644
--- a/lib/isabelle/Prompt_monad_extras.thy
+++ b/lib/isabelle/Prompt_monad_extras.thy
@@ -1,5 +1,7 @@
 theory Prompt_monad_extras
-  imports Prompt_monad
+  imports
+    Prompt_monad
+    Sail_values_extras
 begin
 
 lemma All_bind_dom: "bind_dom (m, f)"
@@ -21,14 +23,18 @@ lemmas try_catch_induct[case_names Done Read_mem Write_memv Read_reg Excl_res Wr
 
 datatype 'regval event =
   (* Request to read memory *)
-    e_read_mem read_kind int int "memory_byte list"
+    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 int int
+  | 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_tagv bitU bool
+  (* Tell the system to dynamically recalculate dependency footprint *)
+  | e_footprint
   (* Request a memory barrier *)
   | e_barrier " barrier_kind "
   (* Request to read register *)
@@ -38,9 +44,12 @@ datatype 'regval event =
 
 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_tagv: "((Write_tagv v k), e_write_tagv 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"
@@ -59,6 +68,29 @@ 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 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_tagv) val k t' v where "m = Write_tagv val k" and "t = e_write_tagv 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"
+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)
+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"
 
@@ -114,11 +146,6 @@ lemma Run_DoneE:
 lemma Run_Done_iff_Nil[simp]: "Run (Done a) t a' \<longleftrightarrow> t = [] \<and> a' = a"
   by (auto elim: Run_DoneE)
 
-lemma Run_BarrierE[elim!]:
-  assumes "Run (Barrier bk k) t a"
-  obtains t' where "t = e_barrier bk # t'" and "Run k t' a"
-  using assms by cases (auto elim: T.cases)
-
 lemma bind_cong[fundef_cong]:
   assumes m: "m1 = m2"
     and f: "\<And>t a. Run m2 t a \<Longrightarrow> f1 a = f2 a"
diff --git a/lib/isabelle/ROOT b/lib/isabelle/ROOT
index d826ea08..b07bc807 100644
--- a/lib/isabelle/ROOT
+++ b/lib/isabelle/ROOT
@@ -1,7 +1,7 @@
 session "Sail" = "LEM" +
   options [document = false]
   theories
-    Sail_values
+    Sail_values_extras
     Prompt
     State_extras
     Sail_operators_mwords
diff --git a/lib/isabelle/Sail_values_extras.thy b/lib/isabelle/Sail_values_extras.thy
new file mode 100644
index 00000000..66bcba48
--- /dev/null
+++ b/lib/isabelle/Sail_values_extras.thy
@@ -0,0 +1,52 @@
+theory Sail_values_extras
+  imports Sail_values
+begin
+
+termination reverse_endianness_list by (lexicographic_order simp add: drop_list_def)
+
+termination index_list
+  by (relation "measure (\<lambda>(i, j, step). nat ((j - i + step) * sgn step))") auto
+
+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"
+  by (induction xs) (auto split: option.splits)
+
+lemma just_list_Some_iff[simp]: "just_list xs = Some ys \<longleftrightarrow> xs = map Some ys"
+  by (induction xs arbitrary: ys) (auto split: option.splits)
+
+lemma just_list_cases:
+  assumes "just_list xs = y"
+  obtains (None) "None \<in> set xs" and "y = None"
+        | (Some) ys where "xs = map Some ys" and "y = Some ys"
+  using assms by (cases y) auto
+
+abbreviation "BC_bitU_list \<equiv> instance_Sail_values_Bitvector_list_dict instance_Sail_values_BitU_Sail_values_bitU_dict"
+lemmas BC_bitU_list_def = instance_Sail_values_Bitvector_list_dict_def instance_Sail_values_BitU_Sail_values_bitU_dict_def
+abbreviation "BC_mword \<equiv> instance_Sail_values_Bitvector_Machine_word_mword_dict"
+lemmas BC_mword_def = instance_Sail_values_Bitvector_Machine_word_mword_dict_def
+
+lemma image_bitU_of_bool_B0_B1: "bitU_of_bool ` bs \<subseteq> {B0, B1}"
+  by (auto simp: bitU_of_bool_def split: if_splits)
+
+lemma bool_of_bitU_bitU_of_bool[simp]: "bool_of_bitU \<circ> bitU_of_bool = id"
+  by (intro ext) (auto simp: bool_of_bitU_def bitU_of_bool_def)
+
+lemma nat_of_bits_aux_bl_to_bin_aux:
+  assumes "set bs \<subseteq> {B0, B1}"
+  shows "nat_of_bits_aux acc bs = nat (bl_to_bin_aux (map bool_of_bitU bs) (int acc))"
+  by (use assms in \<open>induction acc bs rule: nat_of_bits_aux.induct\<close>)
+     (auto simp: Bit_def bool_of_bitU_def intro!: arg_cong[where f = nat] arg_cong2[where f = bl_to_bin_aux])
+
+lemma nat_of_bits_bl_to_bin[simp]: "nat_of_bits (map bitU_of_bool bs) = nat (bl_to_bin bs)"
+  by (auto simp: nat_of_bits_def bl_to_bin_def nat_of_bits_aux_bl_to_bin_aux image_bitU_of_bool_B0_B1)
+
+lemma unsigned_bits_of_mword:
+  "unsigned_method BC_bitU_list (bits_of_method BC_mword a) = unsigned_method BC_mword a"
+  by (auto simp: BC_bitU_list_def BC_mword_def unsigned_of_bits_def)
+
+lemma unsigned_bits_of_bitU_list:
+  "unsigned_method BC_bitU_list (bits_of_method BC_bitU_list a) = unsigned_method BC_bitU_list a"
+  by (auto simp: BC_bitU_list_def)
+
+end
diff --git a/lib/isabelle/State_extras.thy b/lib/isabelle/State_extras.thy
index 096fb19b..924861b0 100644
--- a/lib/isabelle/State_extras.thy
+++ b/lib/isabelle/State_extras.thy
@@ -4,32 +4,187 @@ begin
 
 lemma All_liftState_dom: "liftState_dom (r, m)"
   by (induction m) (auto intro: liftState.domintros)
-
 termination liftState using All_liftState_dom by auto
 
+lemma liftState_bind[simp]:
+  "liftState r (bind m f) = bindS (liftState r m) (liftState r \<circ> f)"
+  by (induction m f rule: bind.induct) auto
+
 lemma liftState_return[simp]: "liftState r (return a) = returnS a" by (auto simp: return_def)
+
+lemma Value_liftState_Run:
+  assumes "(Value a, s') \<in> set (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;
+      blast elim: Value_bindS_elim)
+
 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)
+lemma liftState_exclResult[simp]: "liftState r (excl_result ()) = excl_resultS ()" by (auto simp: excl_result_def)
+lemma liftState_barrier[simp]: "liftState r (barrier bk) = returnS ()" by (auto simp: barrier_def)
+lemma liftState_footprint[simp]: "liftState r (footprint ()) = returnS ()" by (auto simp: footprint_def)
 
-lemma liftState_bind[simp]:
-  "liftState r (bind m f) = bindS (liftState r m) (liftState r \<circ> f)"
-  by (induction m f rule: bind.induct) auto
+lemma liftState_try_catch[simp]:
+  "liftState r (try_catch m h) = try_catchS (liftState r m) (liftState r \<circ> h)"
+  by (induction m h rule: try_catch_induct) (auto simp: try_catchS_bindS_no_throw)
+
+lemma liftState_early_return[simp]:
+  "liftState r (early_return r) = early_returnS r"
+  by (auto simp: early_return_def early_returnS_def)
+
+lemma liftState_catch_early_return[simp]:
+  "liftState r (catch_early_return m) = catch_early_returnS (liftState r m)"
+  by (auto simp: catch_early_return_def catch_early_returnS_def sum.case_distrib cong: sum.case_cong)
+
+lemma liftState_liftR[simp]:
+  "liftState r (liftR m) = liftSR (liftState r m)"
+  by (auto simp: liftR_def liftSR_def)
+
+lemma liftState_try_catchR[simp]:
+  "liftState r (try_catchR m h) = try_catchSR (liftState r m) (liftState r \<circ> h)"
+  by (auto simp: try_catchR_def try_catchSR_def sum.case_distrib cong: sum.case_cong)
+
+lemma liftState_read_mem_BC[simp]:
+  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_memS_def read_mem_bytesS_def)
+lemmas liftState_read_mem[simp] =
+  liftState_read_mem_BC[OF unsigned_bits_of_mword] liftState_read_mem_BC[OF unsigned_bits_of_bitU_list]
+
+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 sz"
+  using assms by (auto simp: write_mem_ea_def write_mem_eaS_def)
+lemmas liftState_write_mem_ea[simp] =
+  liftState_write_mem_ea_BC[OF unsigned_bits_of_mword] liftState_write_mem_ea_BC[OF unsigned_bits_of_bitU_list]
 
-lemma liftState_read_reg[intro]:
+lemma liftState_write_mem_val:
+  "liftState r (write_mem_val BC v) = write_mem_valS BC v"
+  by (auto simp: write_mem_val_def write_mem_valS_def 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)"
-  shows "liftState (get_regval', set_regval') (read_reg reg) = read_regS reg"
+  shows "liftState (get_regval', set_regval') (read_reg reg) = readS (read_from reg \<circ> regstate)"
 proof
   fix s :: "'a sequential_state"
   obtain rv v where "get_regval' (name reg) (regstate s) = Some rv"
-    and "of_regval reg rv = Some v" and "read_from reg (regstate s) = v"
+    and "of_regval reg rv \<equiv> Some v" and "read_from reg (regstate s) = v"
     using assms unfolding bind_eq_Some_conv by blast
-  then show "liftState (get_regval', set_regval') (read_reg reg) s = read_regS reg s"
-    by (auto simp: read_reg_def bindS_def returnS_def read_regS_def)
+  then show "liftState (get_regval', set_regval') (read_reg reg) s = readS (read_from reg \<circ> regstate) s"
+    by (auto simp: read_reg_def bindS_def returnS_def read_regS_def readS_def)
+qed
+
+lemma liftState_write_reg_updateS:
+  assumes "\<And>s. set_regval' (name reg) (regval_of reg v) s = Some (write_to reg v s)"
+  shows "liftState (get_regval', set_regval') (write_reg reg v) = updateS (regstate_update (write_to reg v))"
+  using assms by (auto simp: write_reg_def bindS_readS updateS_def returnS_def)
+
+lemma liftState_iter_aux[simp]:
+  shows "liftState r (iter_aux i f xs) = iterS_aux i (\<lambda>i x. liftState r (f i x)) xs"
+  by (induction i "\<lambda>i x. liftState r (f i x)" xs rule: iterS_aux.induct) (auto cong: bindS_cong)
+
+lemma liftState_iteri[simp]:
+  "liftState r (iteri f xs) = iteriS (\<lambda>i x. liftState r (f i x)) xs"
+  by (auto simp: iteri_def iteriS_def)
+
+lemma liftState_iter[simp]:
+  "liftState r (iter f xs) = iterS (liftState r \<circ> f) xs"
+  by (auto simp: iter_def iterS_def)
+
+lemma liftState_foreachM[simp]:
+  "liftState r (foreachM xs vars body) = foreachS xs vars (\<lambda>x vars. liftState r (body x vars))"
+  by (induction xs vars "\<lambda>x vars. liftState r (body x vars)" rule: foreachS.induct)
+     (auto cong: bindS_cong)
+
+lemma whileS_dom_step:
+  assumes "whileS_dom (vars, cond, body, s)"
+    and "(Value True, s') \<in> set (cond vars s)"
+    and "(Value vars', s'') \<in> set (body vars s')"
+  shows "whileS_dom (vars', cond, body, s'')"
+  by (use assms in \<open>induction vars cond body s arbitrary: vars' s' s'' rule: whileS.pinduct\<close>)
+     (auto intro: whileS.domintros)
+
+lemma whileM_dom_step:
+  assumes "whileM_dom (vars, cond, body)"
+    and "Run (cond vars) t True"
+    and "Run (body vars) t' vars'"
+  shows "whileM_dom (vars', cond, body)"
+  by (use assms in \<open>induction vars cond body arbitrary: vars' t t' rule: whileM.pinduct\<close>)
+     (auto intro: whileM.domintros)
+
+lemma whileM_dom_ex_step:
+  assumes "whileM_dom (vars, cond, body)"
+    and "\<exists>t. Run (cond vars) t True"
+    and "\<exists>t'. Run (body vars) t' vars'"
+  shows "whileM_dom (vars', cond, body)"
+  using assms by (blast intro: whileM_dom_step)
+
+lemmas whileS_pinduct = whileS.pinduct[case_names Step]
+
+lemma liftState_whileM:
+  assumes "whileS_dom (vars, liftState r \<circ> cond, liftState r \<circ> body, s)"
+    and "whileM_dom (vars, cond, body)"
+  shows "liftState r (whileM vars cond body) s = whileS vars (liftState r \<circ> cond) (liftState r \<circ> body) s"
+proof (use assms in \<open>induction vars "liftState r \<circ> cond" "liftState r \<circ> body" s rule: whileS.pinduct\<close>)
+  case Step: (1 vars s)
+  note domS = Step(1) and IH = Step(2) and domM = Step(3)
+  show ?case unfolding whileS.psimps[OF domS] whileM.psimps[OF domM] liftState_bind
+  proof (intro bindS_ext_cong, goal_cases cond while)
+    case (while a s')
+    have "bindS (liftState r (body vars)) (liftState r \<circ> (\<lambda>vars. whileM vars cond body)) s' =
+          bindS (liftState r (body vars)) (\<lambda>vars. whileS vars (liftState r \<circ> cond) (liftState r \<circ> body)) s'"
+      if "a"
+    proof (intro bindS_ext_cong, goal_cases body while')
+      case (while' vars' s'')
+      have "whileM_dom (vars', cond, body)" proof (rule whileM_dom_ex_step[OF domM])
+        show "\<exists>t. Run (cond vars) t True" using while that by (auto elim: Value_liftState_Run)
+        show "\<exists>t'. Run (body vars) t' vars'" using while' that by (auto elim: Value_liftState_Run)
+      qed
+      then show ?case using while while' that by (auto intro: IH)
+    qed auto
+    then show ?case by auto
+  qed auto
 qed
 
-lemma liftState_write_reg[intro]:
-  assumes "\<And>s. set_regval' (name reg) (regval_of reg v) s = Some (write_to reg s v)"
-  shows "liftState (get_regval', set_regval') (write_reg reg v) = write_regS reg v"
-  using assms by (auto simp: write_reg_def bindS_def returnS_def write_regS_def)
+
+lemma untilM_dom_step:
+  assumes "untilM_dom (vars, cond, body)"
+    and "Run (body vars) t vars'"
+    and "Run (cond vars') t' False"
+  shows "untilM_dom (vars', cond, body)"
+  by (use assms in \<open>induction vars cond body arbitrary: vars' t t' rule: untilM.pinduct\<close>)
+     (auto intro: untilM.domintros)
+
+lemma untilM_dom_ex_step:
+  assumes "untilM_dom (vars, cond, body)"
+    and "\<exists>t. Run (body vars) t vars'"
+    and "\<exists>t'. Run (cond vars') t' False"
+  shows "untilM_dom (vars', cond, body)"
+  using assms by (blast intro: untilM_dom_step)
+
+lemma liftState_untilM:
+  assumes "untilS_dom (vars, liftState r \<circ> cond, liftState r \<circ> body, s)"
+    and "untilM_dom (vars, cond, body)"
+  shows "liftState r (untilM vars cond body) s = untilS vars (liftState r \<circ> cond) (liftState r \<circ> body) s"
+proof (use assms in \<open>induction vars "liftState r \<circ> cond" "liftState r \<circ> body" s rule: untilS.pinduct\<close>)
+  case Step: (1 vars s)
+  note domS = Step(1) and IH = Step(2) and domM = Step(3)
+  show ?case unfolding untilS.psimps[OF domS] untilM.psimps[OF domM] liftState_bind
+  proof (intro bindS_ext_cong, goal_cases body k)
+    case (k vars' s')
+    show ?case unfolding comp_def liftState_bind
+    proof (intro bindS_ext_cong, goal_cases cond until)
+      case (until a s'')
+      have "untilM_dom (vars', cond, body)" if "\<not>a"
+      proof (rule untilM_dom_ex_step[OF domM])
+        show "\<exists>t. Run (body vars) t vars'" using k by (auto elim: Value_liftState_Run)
+        show "\<exists>t'. Run (cond vars') t' False" using until that by (auto elim: Value_liftState_Run)
+      qed
+      then show ?case using k until IH by (auto simp: comp_def)
+    qed auto
+  qed auto
+qed
 
 end
diff --git a/lib/isabelle/State_monad_extras.thy b/lib/isabelle/State_monad_extras.thy
index eb8ed678..406aec79 100644
--- a/lib/isabelle/State_monad_extras.thy
+++ b/lib/isabelle/State_monad_extras.thy
@@ -1,15 +1,22 @@
 theory State_monad_extras
-  imports State_monad
+  imports
+    State_monad
+    Sail_values_extras
+begin
+
+context
+  notes returnS_def[simp] and failS_def[simp] and throwS_def[simp] and readS_def[simp] and updateS_def[simp]
 begin
 
 abbreviation "bindS_aux f \<equiv> (\<lambda>r. case r of (Value a, s') \<Rightarrow> f a s' | (Ex e, s') \<Rightarrow> [(Ex e, s')])"
+abbreviation "bindS_app ms f \<equiv> List.concat (List.map (bindS_aux f) ms)"
 
 lemma bindS_ext_cong[fundef_cong]:
   assumes m: "m1 s = m2 s"
     and f: "\<And>a s'. (Value a, s') \<in> set (m2 s) \<Longrightarrow> f1 a s' = f2 a s'"
-  shows "(bindS m1 f1) s = (bindS m2 f2) s"
+  shows "bindS m1 f1 s = bindS m2 f2 s"
 proof -
-  have "List.concat (map (bindS_aux f1) (m2 s)) = List.concat (map (bindS_aux f2) (m2 s))"
+  have "bindS_app (m2 s) f1 = bindS_app (m2 s) f2"
     using f by (intro arg_cong[where f = List.concat]) (auto intro: map_ext split: result.splits)
   then show ?thesis using m by (auto simp: bindS_def)
 qed
@@ -20,8 +27,21 @@ lemma bindS_cong[fundef_cong]:
   shows "bindS m1 f1 = bindS m2 f2"
   using assms by (blast intro: bindS_ext_cong)
 
-lemma bindS_returnS[simp]: "bindS (returnS x) m = m x"
-  by (auto simp add: bindS_def returnS_def)
+lemma bindS_returnS_left[simp]: "bindS (returnS x) f = f x"
+  by (auto simp add: bindS_def)
+
+lemma bindS_returnS_right[simp]: "bindS m returnS = (m :: ('regs, 'a, 'e) monadS)"
+proof -
+  have "List.concat (map (bindS_aux returnS) ms) = ms" for ms :: "(('a, 'e) result \<times> 'regs sequential_state) list"
+    by (induction ms) (auto split: result.splits)
+  then show ?thesis unfolding bindS_def by blast
+qed
+
+lemma bindS_readS: "bindS (readS f) m = (\<lambda>s. m (f s) s)"
+  by (auto simp: bindS_def)
+
+lemma bindS_updateS: "bindS (updateS f) m = (\<lambda>s. m () (f s))"
+  by (auto simp: bindS_def)
 
 lemma bindS_assoc[simp]: "bindS (bindS m f) g = bindS m (\<lambda>x. bindS (f x) g)"
 proof -
@@ -31,13 +51,96 @@ proof -
   then show ?thesis unfolding bindS_def by auto
 qed
 
-lemma bindS_failS[simp]: "bindS (failS msg) f = failS msg" by (auto simp: bindS_def failS_def)
-lemma bindS_throwS[simp]: "bindS (throwS e) f = throwS e" by (auto simp: bindS_def throwS_def)
+lemma bindS_failS[simp]: "bindS (failS msg) f = failS msg" by (auto simp: bindS_def)
+lemma bindS_throwS[simp]: "bindS (throwS e) f = throwS e" by (auto simp: bindS_def)
 declare seqS_def[simp]
 
+lemma Value_bindS_elim:
+  assumes "(Value a, s') \<in> set (bindS m f s)"
+  obtains s'' a' where "(Value a', s'') \<in> set (m s)" and "(Value a, s') \<in> set (f a' s'')"
+  using assms by (auto simp: bindS_def; split result.splits; auto)
+
+abbreviation
+  "try_catchS_aux h r \<equiv>
+    (case r of
+       (Value a, s') => returnS a s'
+     | (Ex (Throw e), s') => h e s'
+     | (Ex (Failure msg), s') => [(Ex (Failure msg), s')])"
+abbreviation "try_catchS_app ms h \<equiv> List.concat (List.map (try_catchS_aux h) ms)"
+
 lemma try_catchS_returnS[simp]: "try_catchS (returnS a) h = returnS a"
   and try_catchS_failS[simp]: "try_catchS (failS msg) h = failS msg"
   and try_catchS_throwS[simp]: "try_catchS (throwS e) h = h e"
-  by (auto simp: returnS_def failS_def throwS_def try_catchS_def)
+  by (auto simp: try_catchS_def)
+
+lemma try_catchS_cong[cong]:
+  assumes "\<And>s. m1 s = m2 s" and "\<And>e s. h1 e s = h2 e s"
+  shows "try_catchS m1 h1 = try_catchS m2 h2"
+  using assms by (intro arg_cong2[where f = try_catchS] ext) auto
+
+fun ignore_throw_app :: "(('a, 'e1) result \<times> 's) list \<Rightarrow> (('a, 'e2) result \<times> 's) list" where
+  "ignore_throw_app [] = []"
+| "ignore_throw_app ((Value a, s) # ms) = (Value a, s) # ignore_throw_app ms"
+| "ignore_throw_app ((Ex (Failure msg), s) # ms) = (Ex (Failure msg), s) # ignore_throw_app ms"
+| "ignore_throw_app ((Ex (Throw e), s) # ms) = ignore_throw_app ms"
+abbreviation ignore_throw :: "('r, 'a, 'e1) monadS \<Rightarrow> ('r, 'a, 'e2) monadS" where
+  "ignore_throw m \<equiv> \<lambda>s. ignore_throw_app (m s)"
+
+lemma [simp]: "ignore_throw_app ms = (Ex (Throw e), s) # ms' \<longleftrightarrow> False"
+  by (induction ms rule: ignore_throw_app.induct) auto
+
+lemma ignore_throw_app_append[simp]:
+  "ignore_throw_app (ms1 @ ms2) = ignore_throw_app ms1 @ ignore_throw_app ms2"
+  by (induction ms1 rule: ignore_throw_app.induct) auto
+
+lemma ignore_throw_app_bindS_app[simp]:
+  "ignore_throw_app (bindS_app ms f) = bindS_app (ignore_throw_app ms) (ignore_throw \<circ> f)"
+  by (induction ms rule: ignore_throw_app.induct) (auto split: result.splits)
+
+lemma ignore_throw_bindS[simp]:
+  "ignore_throw (bindS m f) = bindS (ignore_throw m) (ignore_throw \<circ> f)"
+  "ignore_throw (bindS m f) s = bindS (ignore_throw m) (ignore_throw \<circ> f) s"
+  unfolding bindS_def by auto
+
+lemma try_catchS_bindS_no_throw:
+  fixes m1 :: "('r, 'a, 'e1) monadS" and m2 :: "('r, 'a, 'e2) monadS"
+  assumes m1: "\<And>s. ignore_throw m1 s = m1 s"
+    and m2: "\<And>s. ignore_throw m1 s = m2 s"
+  shows "try_catchS (bindS m1 f) h = bindS m2 (\<lambda>a. try_catchS (f a) h)"
+proof
+  fix s
+  have 1: "try_catchS_app (bindS_app ms f) h =
+        bindS_app (ignore_throw_app ms) (\<lambda>a s'. try_catchS_app (f a s') h)"
+    if "ignore_throw_app ms = ms" for ms
+    using that by (induction ms rule: ignore_throw_app.induct) auto
+  then show "try_catchS (bindS m1 f) h s = bindS m2 (\<lambda>a. try_catchS (f a) h) s"
+    using m1 unfolding try_catchS_def bindS_def m2[symmetric] by blast
+qed
+
+lemma no_throw_mem_builtins:
+  "\<And>a. ignore_throw (returnS a) = returnS a"
+  "\<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>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>t s. ignore_throw (write_tagS t) s = write_tagS t s"
+  "\<And>s. ignore_throw (excl_resultS ()) s = excl_resultS () s"
+  unfolding read_mem_bytesS_def read_memS_def read_tagS_def write_mem_eaS_def write_mem_valS_def write_mem_bytesS_def write_tagS_def excl_resultS_def
+  by (auto simp: bindS_def chooseS_def Let_def split: option.splits)+
+
+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_cong)
+
+lemma no_throw_read_regvalS: "ignore_throw (read_regvalS r reg_name) s = read_regvalS r reg_name s"
+  by (cases r) (auto simp: bindS_def split: option.splits)
+
+lemma no_throw_write_regvalS: "ignore_throw (write_regvalS r reg_name v) s = write_regvalS r reg_name v s"
+  by (cases r) (auto simp: bindS_def split: option.splits)
+
+lemmas no_throw_builtins[simp, intro] =
+  no_throw_mem_builtins no_throw_read_regvalS no_throw_write_regvalS no_throw_read_memS
+
+end
 
 end
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 756bb699..728014eb 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -10,81 +10,38 @@ let rec iter_aux i f xs = match xs with
   | [] -> return ()
   end
 
+declare {isabelle} termination_argument iter_aux = automatic
+
 val iteri : forall 'rv 'a 'e. (integer -> 'a -> monad 'rv unit 'e) -> list 'a -> monad 'rv unit 'e
 let iteri f xs = iter_aux 0 f xs
 
 val iter : forall 'rv 'a 'e. ('a -> monad 'rv unit 'e) -> list 'a -> monad 'rv unit 'e
 let iter f xs = iteri (fun _ x -> f x) xs
 
+val foreachM : forall 'a 'rv 'vars 'e.
+  list 'a -> 'vars -> ('a -> 'vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
+let rec foreachM [] vars _ = return vars
+and foreachM (x :: xs) vars body =
+  body x vars >>= fun vars ->
+  foreachM xs vars body
 
-val foreachM_inc : forall 'rv 'vars 'e. (integer * integer * integer) -> 'vars ->
-                  (integer -> 'vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
-let rec foreachM_inc (i,stop,by) vars body =
-  if (by > 0 && i <= stop) || (by < 0 && stop <= i)
-  then
-    body i vars >>= fun vars ->
-    foreachM_inc (i + by,stop,by) vars body
-  else return vars
-
-
-val foreachM_dec : forall 'rv 'vars 'e. (integer * integer * integer) -> 'vars ->
-                  (integer -> 'vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
-let rec foreachM_dec (i,stop,by) vars body =
-  if (by > 0 && i >= stop) || (by < 0 && stop >= i)
-  then
-    body i vars >>= fun vars ->
-    foreachM_dec (i - by,stop,by) vars body
-  else return vars
-
-val while_PP : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
-let rec while_PP vars cond body =
-  if cond vars then while_PP (body vars) cond body else vars
-
-val while_PM : forall 'rv 'vars 'e. 'vars -> ('vars -> bool) ->
-                ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
-let rec while_PM vars cond body =
-  if cond vars then
-    body vars >>= fun vars -> while_PM vars cond body
-  else return vars
+declare {isabelle} termination_argument foreachM = automatic
 
-val while_MP : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
-                ('vars -> 'vars) -> monad 'rv 'vars 'e
-let rec while_MP vars cond body =
-  cond vars >>= fun cond_val ->
-  if cond_val then while_MP (body vars) cond body else return vars
 
-val while_MM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
+val whileM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
                 ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
-let rec while_MM vars cond body =
+let rec whileM vars cond body =
   cond vars >>= fun cond_val ->
   if cond_val then
-    body vars >>= fun vars -> while_MM vars cond body
+    body vars >>= fun vars -> whileM vars cond body
   else return vars
 
-val until_PP : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
-let rec until_PP vars cond body =
-  let vars = body vars in
-  if (cond vars) then vars else until_PP (body vars) cond body
-
-val until_PM : forall 'rv 'vars 'e. 'vars -> ('vars -> bool) ->
-                ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
-let rec until_PM vars cond body =
-  body vars >>= fun vars ->
-  if (cond vars) then return vars else until_PM vars cond body
-
-val until_MP : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
-                ('vars -> 'vars) -> monad 'rv 'vars 'e
-let rec until_MP vars cond body =
-  let vars = body vars in
-  cond vars >>= fun cond_val ->
-  if cond_val then return vars else until_MP vars cond body
-
-val until_MM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
+val untilM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
                 ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
-let rec until_MM vars cond body =
+let rec untilM vars cond body =
   body vars >>= fun vars ->
   cond vars >>= fun cond_val ->
-  if cond_val then return vars else until_MM vars cond body
+  if cond_val then return vars else untilM vars cond body
 
 (*let write_two_regs r1 r2 vec =
   let is_inc =
diff --git a/src/gen_lib/prompt_monad.lem b/src/gen_lib/prompt_monad.lem
index 38f79868..3c414d6e 100644
--- a/src/gen_lib/prompt_monad.lem
+++ b/src/gen_lib/prompt_monad.lem
@@ -4,17 +4,25 @@ open import Sail_instr_kinds
 open import Sail_values
 
 type register_name = string
+type address = list bitU
 
 type monad 'regval 'a 'e =
   | Done of 'a
-  | Read_mem of read_kind * integer * integer * (list memory_byte -> monad 'regval 'a 'e)
+  (* Read a number of bytes from memory, returned in little endian order *)
+  | Read_mem of read_kind * address * nat * (list memory_byte -> monad 'regval 'a 'e)
+  (* Read the tag of a memory address *)
+  | Read_tag of address * (bitU -> monad 'regval 'a 'e)
   (* Tell the system a write is imminent, at address lifted, of size nat *)
-  | Write_ea of write_kind * integer * integer * monad 'regval 'a 'e
+  | Write_ea of write_kind * address * nat * monad 'regval 'a 'e
   (* Request the result of store-exclusive *)
   | Excl_res of (bool -> monad 'regval 'a 'e)
   (* Request to write memory at last signalled address. Memory value should be 8
-     times the size given in ea signal *)
+     times the size given in ea signal, given in little endian order *)
   | Write_memv of list memory_byte * (bool -> monad 'regval 'a 'e)
+  (* Request to write the tag at last signalled address. *)
+  | Write_tagv of bitU * (bool -> monad 'regval 'a 'e)
+  (* Tell the system to dynamically recalculate dependency footprint *)
+  | Footprint of monad 'regval 'a 'e
   (* Request a memory barrier *)
   | Barrier of barrier_kind * monad 'regval 'a 'e
   (* Request to read register, will track dependency when mode.track_values *)
@@ -35,10 +43,13 @@ val bind : forall 'rv 'a 'b 'e. monad 'rv 'a 'e -> ('a -> monad 'rv 'b 'e) -> mo
 let rec bind m f = match m with
   | Done a -> f a
   | Read_mem rk a sz k -> Read_mem rk a sz (fun v -> bind (k v) f)
+  | Read_tag a k ->       Read_tag a       (fun v -> bind (k v) f)
   | Write_memv descr k -> Write_memv descr (fun v -> bind (k v) f)
+  | Write_tagv t k ->     Write_tagv t     (fun v -> bind (k v) f)
   | Read_reg descr k ->   Read_reg descr   (fun v -> bind (k v) f)
   | Excl_res k ->         Excl_res         (fun v -> bind (k v) f)
   | Write_ea wk a sz k -> Write_ea wk a sz (bind k f)
+  | Footprint k ->        Footprint        (bind k f)
   | Barrier bk k ->       Barrier bk       (bind k f)
   | Write_reg r v k ->    Write_reg r v    (bind k f)
   | Fail descr ->         Fail descr
@@ -63,10 +74,13 @@ val try_catch : forall 'rv 'a 'e1 'e2. monad 'rv 'a 'e1 -> ('e1 -> monad 'rv 'a
 let rec try_catch m h = match m with
   | Done a ->             Done a
   | Read_mem rk a sz k -> Read_mem rk a sz (fun v -> try_catch (k v) h)
+  | Read_tag a k ->       Read_tag a       (fun v -> try_catch (k v) h)
   | Write_memv descr k -> Write_memv descr (fun v -> try_catch (k v) h)
+  | Write_tagv t k ->     Write_tagv t     (fun v -> try_catch (k v) h)
   | Read_reg descr k ->   Read_reg descr   (fun v -> try_catch (k v) h)
   | Excl_res k ->         Excl_res         (fun v -> try_catch (k v) h)
   | Write_ea wk a sz k -> Write_ea wk a sz (try_catch k h)
+  | Footprint k ->        Footprint        (try_catch k h)
   | Barrier bk k ->       Barrier bk       (try_catch k h)
   | Write_reg r v k ->    Write_reg r v    (try_catch k h)
   | Fail descr ->         Fail descr
@@ -106,11 +120,8 @@ let try_catchR m h =
 
 val read_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv 'b 'e
 let read_mem rk addr sz =
-  let addr = unsigned addr in
-  let k bytes =
-    let bitv = bits_of_bytes (List.reverse bytes) in
-    (Done bitv) in
-  Read_mem rk addr sz k
+  let k bytes = Done (bits_of_mem_bytes bytes) in
+  Read_mem rk (bits_of addr) (natFromInteger sz) k
 
 val excl_result : forall 'rv 'e. unit -> monad 'rv bool 'e
 let excl_result () =
@@ -118,13 +129,11 @@ let excl_result () =
   Excl_res k
 
 val write_mem_ea : forall 'rv 'a 'e. Bitvector 'a => write_kind -> 'a -> integer -> monad 'rv unit 'e
-let write_mem_ea wk addr sz = Write_ea wk (unsigned addr) sz (Done ())
+let write_mem_ea wk addr sz = Write_ea wk (bits_of addr) (natFromInteger sz) (Done ())
 
 val write_mem_val : forall 'rv 'a 'e. Bitvector 'a => 'a -> monad 'rv bool 'e
-let write_mem_val v = match bytes_of_bits v with
-  | Just v ->
-     let k successful = (return successful) in
-     Write_memv (List.reverse v) k
+let write_mem_val v = match mem_bytes_of_bits v with
+  | Just v -> Write_memv v return
   | Nothing -> Fail "write_mem_val"
 end
 
@@ -182,5 +191,5 @@ let write_reg_field_bit = write_reg_field_pos*)
 val barrier : forall 'rv 'e. barrier_kind -> monad 'rv unit 'e
 let barrier bk = Barrier bk (Done ())
 
-(*val footprint : forall 'rv 'e. monad 'rv unit 'e
-let footprint = Footprint (Done ())*)
+val footprint : forall 'rv 'e. unit -> monad 'rv unit 'e
+let footprint _ = Footprint (Done ())
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index b981bb91..ead63d62 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -205,18 +205,15 @@ let rec bits_of_nat_aux x =
 declare {isabelle} termination_argument bits_of_nat_aux = automatic
 let bits_of_nat n = List.reverse (bits_of_nat_aux n)
 
-val nat_of_bits : list bitU -> natural
-let nat_of_bits bits =
-  let (sum,_) =
-    List.foldr
-      (fun b (acc,exp) ->
-        match b with
-        | B1 -> (acc + naturalPow 2 exp, exp + 1)
-        | B0 -> (acc, exp + 1)
-        | BU -> failwith "nat_of_bits: bitvector has undefined bits"
-        end)
-      (0,0) bits in
-  sum
+val nat_of_bits_aux : natural -> list bitU -> natural
+let rec nat_of_bits_aux acc bs = match bs with
+  | [] -> acc
+  | B1 :: bs -> nat_of_bits_aux ((2 * acc) + 1) bs
+  | B0 :: bs -> nat_of_bits_aux (2 * acc) bs
+  | BU :: _ -> failwith "nat_of_bits_aux: bit list has undefined bits"
+end
+declare {isabelle} termination_argument nat_of_bits_aux = automatic
+let nat_of_bits bits = nat_of_bits_aux 0 bits
 
 let not_bits = List.map not_bit
 
@@ -543,6 +540,9 @@ let bytes_of_bits bs = byte_chunks (bits_of bs)
 val bits_of_bytes : forall 'a. Bitvector 'a => list memory_byte -> 'a
 let bits_of_bytes bs = of_bits (List.concat (List.map bits_of bs))
 
+let mem_bytes_of_bits bs = Maybe.map List.reverse (bytes_of_bits bs)
+let bits_of_mem_bytes bs = bits_of_bytes (List.reverse bs)
+
 (*val bitv_of_byte_lifteds : list Sail_impl_base.byte_lifted -> list bitU
 let bitv_of_byte_lifteds v =
   foldl (fun x (Byte_lifted y) -> x ++ (List.map bitU_of_bit_lifted y)) [] v
@@ -612,7 +612,7 @@ type register_ref 'regstate 'regval 'a =
   <| name : string;
      (*is_inc : bool;*)
      read_from : 'regstate -> 'a;
-     write_to : 'regstate -> 'a -> 'regstate;
+     write_to : 'a -> 'regstate -> 'regstate;
      of_regval : 'regval -> maybe 'a;
      regval_of : 'a -> 'regval |>
 
@@ -750,24 +750,28 @@ let internal_mem_value bytes =
   List.reverse bytes $> bitv_of_byte_lifteds*)
 
 
+val foreach : forall 'a 'vars.
+  (list 'a) -> 'vars -> ('a -> 'vars -> 'vars) -> 'vars
+let rec foreach [] vars _ = vars
+and foreach (x :: xs) vars body = foreach xs (body x vars) body
+
+declare {isabelle} termination_argument foreach = automatic
 
+val index_list : integer -> integer -> integer -> list integer
+let rec index_list from to step =
+  if (step > 0 && from <= to) || (step < 0 && to <= from) then
+    from :: index_list (from + step) to step
+  else []
 
+val while : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
+let rec while vars cond body =
+  if cond vars then while (body vars) cond body else vars
 
-val foreach_inc :  forall 'vars. (integer * integer * integer) -> 'vars ->
-                   (integer -> 'vars -> 'vars) -> 'vars
-let rec foreach_inc (i,stop,by) vars body =
-  if (by > 0 && i <= stop) || (by < 0 && stop <= i)
-  then let vars = body i vars in
-       foreach_inc (i + by,stop,by) vars body
-  else vars
+val until : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
+let rec until vars cond body =
+  let vars = body vars in
+  if cond vars then vars else until (body vars) cond body
 
-val foreach_dec : forall 'vars. (integer * integer * integer) -> 'vars ->
-                  (integer -> 'vars -> 'vars) -> 'vars
-let rec foreach_dec (i,stop,by) vars body =
-  if (by > 0 && i >= stop) || (by < 0 && stop >= i)
-  then let vars = body i vars in
-       foreach_dec (i - by,stop,by) vars body
-  else vars
 
 let assert' b msg_opt =
   let msg = match msg_opt with
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index fba8d9b7..1740174e 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -11,12 +11,15 @@ open import {isabelle} `State_monad_extras`
 val liftState : forall 'regval 'regs 'a 'e. register_accessors 'regs 'regval -> monad 'regval 'a 'e -> monadS 'regs 'a 'e
 let rec liftState ra s = match s with
   | (Done a)             -> returnS a
-  | (Read_mem rk a sz k) -> bindS (read_memS rk a sz)     (fun v -> liftState ra (k v))
-  | (Write_memv descr k) -> bindS (write_mem_valS descr)  (fun v -> liftState ra (k v))
-  | (Read_reg descr k)   -> bindS (read_regvalS ra descr) (fun v -> liftState ra (k v))
-  | (Excl_res k)         -> bindS (excl_resultS ())       (fun v -> liftState ra (k v))
-  | (Write_ea wk a sz k) -> seqS (write_mem_eaS wk a sz)  (liftState ra k)
-  | (Write_reg r v k)    -> seqS (write_regvalS ra r v)   (liftState ra k)
+  | (Read_mem rk a sz k) -> bindS (read_mem_bytesS rk a sz) (fun v -> liftState ra (k v))
+  | (Read_tag t k)       -> bindS (read_tagS t)             (fun v -> liftState ra (k v))
+  | (Write_memv a k)     -> bindS (write_mem_bytesS a)      (fun v -> liftState ra (k v))
+  | (Write_tagv t k)     -> bindS (write_tagS t)            (fun v -> liftState ra (k v))
+  | (Read_reg r k)       -> bindS (read_regvalS ra r)       (fun v -> liftState ra (k v))
+  | (Excl_res k)         -> bindS (excl_resultS ())         (fun v -> liftState ra (k v))
+  | (Write_ea wk a sz k) -> seqS (write_mem_eaS wk a sz)    (liftState ra k)
+  | (Write_reg r v k)    -> seqS (write_regvalS ra r v)     (liftState ra k)
+  | (Footprint k)        -> liftState ra k
   | (Barrier _ k)        -> liftState ra k
   | (Fail descr)         -> failS descr
   | (Error descr)        -> failS descr
@@ -24,99 +27,43 @@ let rec liftState ra s = match s with
 end
 
 
-(* TODO
-val iter_aux : forall 'regs 'e 'a. integer -> (integer -> 'a -> M 'regs unit 'e) -> list 'a -> M 'regs unit 'e
-let rec iter_aux i f xs = match xs with
-  | x :: xs -> f i x >> iter_aux (i + 1) f xs
-  | [] -> return ()
+val iterS_aux : forall 'rv 'a 'e. integer -> (integer -> 'a -> monadS 'rv unit 'e) -> list 'a -> monadS 'rv unit 'e
+let rec iterS_aux i f xs = match xs with
+  | x :: xs -> f i x >>$ iterS_aux (i + 1) f xs
+  | [] -> returnS ()
   end
 
-val iteri : forall 'regs 'e 'a. (integer -> 'a -> M 'regs unit 'e) -> list 'a -> M 'regs unit 'e
-let iteri f xs = iter_aux 0 f xs
+declare {isabelle} termination_argument iterS_aux = automatic
 
-val iter : forall 'regs 'e 'a. ('a -> M 'regs unit 'e) -> list 'a -> M 'regs unit 'e
-let iter f xs = iteri (fun _ x -> f x) xs
+val iteriS : forall 'rv 'a 'e. (integer -> 'a -> monadS 'rv unit 'e) -> list 'a -> monadS 'rv unit 'e
+let iteriS f xs = iterS_aux 0 f xs
 
-val foreachM_inc : forall 'regs 'vars 'e. (integer * integer * integer) -> 'vars ->
-                  (integer -> 'vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e
-let rec foreachM_inc (i,stop,by) vars body =
-  if (by > 0 && i <= stop) || (by < 0 && stop <= i)
-  then
-    body i vars >>= fun vars ->
-    foreachM_inc (i + by,stop,by) vars body
-  else return vars
+val iterS : forall 'rv 'a 'e. ('a -> monadS 'rv unit 'e) -> list 'a -> monadS 'rv unit 'e
+let iterS f xs = iteriS (fun _ x -> f x) xs
 
+val foreachS : forall 'a 'rv 'vars 'e.
+  list 'a -> 'vars -> ('a -> 'vars -> monadS 'rv 'vars 'e) -> monadS 'rv 'vars 'e
+let rec foreachS xs vars body = match xs with
+  | [] -> returnS vars
+  | x :: xs ->
+     body x vars >>$= fun vars ->
+     foreachS xs vars body
+end
 
-val foreachM_dec : forall 'regs 'vars 'e. (integer * integer * integer) -> 'vars ->
-                  (integer -> 'vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e
-let rec foreachM_dec (i,stop,by) vars body =
-  if (by > 0 && i >= stop) || (by < 0 && stop >= i)
-  then
-    body i vars >>= fun vars ->
-    foreachM_dec (i - by,stop,by) vars body
-  else return vars
-
-val while_PP : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
-let rec while_PP vars cond body =
-  if cond vars then while_PP (body vars) cond body else vars
-
-val while_PM : forall 'regs 'vars 'e. 'vars -> ('vars -> bool) ->
-                ('vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e
-let rec while_PM vars cond body s =
-  if cond vars then
-    bind (body vars) (fun vars s' -> while_PM vars cond body s') s
-  else return vars s
-
-val while_MP : forall 'regs 'vars 'e. 'vars -> ('vars -> M 'regs bool 'e) ->
-                ('vars -> 'vars) -> M 'regs 'vars 'e
-let rec while_MP vars cond body s =
-  bind
-    (cond vars)
-    (fun cond_val s' ->
-      if cond_val then while_MP (body vars) cond body s' else return vars s') s
-
-val while_MM : forall 'regs 'vars 'e. 'vars -> ('vars -> M 'regs bool 'e) ->
-                ('vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e
-let rec while_MM vars cond body s =
-  bind
-    (cond vars)
-    (fun cond_val s' ->
-      if cond_val then
-        bind
-          (body vars)
-          (fun vars s'' -> while_MM vars cond body s'') s'
-      else return vars s') s
-
-val until_PP : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
-let rec until_PP vars cond body =
-  let vars = body vars in
-  if (cond vars) then vars else until_PP (body vars) cond body
+declare {isabelle} termination_argument foreachS = automatic
 
-val until_PM : forall 'regs 'vars 'e. 'vars -> ('vars -> bool) ->
-                ('vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e
-let rec until_PM vars cond body s =
-  bind
-    (body vars)
-    (fun vars s' ->
-      if (cond vars) then return vars s' else until_PM vars cond body s') s
 
-val until_MP : forall 'regs 'vars 'e. 'vars -> ('vars -> M 'regs bool 'e) ->
-                ('vars -> 'vars) -> M 'regs 'vars 'e
-let rec until_MP vars cond body s =
-  let vars = body vars in
-  bind
-    (cond vars)
-    (fun cond_val s' ->
-      if cond_val then return vars s' else until_MP vars cond body s') s
+val whileS : forall 'rv 'vars 'e. 'vars -> ('vars -> monadS 'rv bool 'e) ->
+                ('vars -> monadS 'rv 'vars 'e) -> monadS 'rv 'vars 'e
+let rec whileS vars cond body s =
+  (cond vars >>$= (fun cond_val s' ->
+  if cond_val then
+    (body vars >>$= (fun vars s'' -> whileS vars cond body s'')) s'
+  else returnS vars s')) s
 
-val until_MM : forall 'regs 'vars 'e. 'vars -> ('vars -> M 'regs bool 'e) ->
-                ('vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e
-let rec until_MM vars cond body s =
-  bind
-    (body vars)
-    (fun vars s' ->
-      bind
-        (cond vars)
-        (fun cond_val s''->
-          if cond_val then return vars s'' else until_MM vars cond body s'') s') s
-*)
+val untilS : forall 'rv 'vars 'e. 'vars -> ('vars -> monadS 'rv bool 'e) ->
+                ('vars -> monadS 'rv 'vars 'e) -> monadS 'rv 'vars 'e
+let rec untilS vars cond body s =
+  (body vars >>$= (fun vars s' ->
+  (cond vars >>$= (fun cond_val s'' ->
+  if cond_val then returnS vars s'' else untilS vars cond body s'')) s')) s
diff --git a/src/gen_lib/state_monad.lem b/src/gen_lib/state_monad.lem
index f324a9f4..8ff39d62 100644
--- a/src/gen_lib/state_monad.lem
+++ b/src/gen_lib/state_monad.lem
@@ -24,7 +24,6 @@ let init_state regs =
      last_exclusive_operation_was_load = false |>
 
 type ex 'e =
-  | Exit
   | Failure of string
   | Throw of 'e
 
@@ -49,12 +48,24 @@ let bindS m f (s : sequential_state 'regs) =
 val seqS: forall 'regs 'b 'e. monadS 'regs unit 'e -> monadS 'regs 'b 'e -> monadS 'regs 'b 'e
 let seqS m n = bindS m (fun (_ : unit) -> n)
 
-val exitS : forall 'regs 'e 'a. unit -> monadS 'regs 'a 'e
-let exitS () s = [(Ex Exit, s)]
+let inline (>>$=) = bindS
+let inline (>>$) = seqS
+
+val chooseS : forall 'regs 'a 'e. list 'a -> monadS 'regs 'a 'e
+let chooseS xs s = List.map (fun x -> (Value x, s)) xs
+
+val readS : forall 'regs 'a 'e. (sequential_state 'regs -> 'a) -> monadS 'regs 'a 'e
+let readS f = (fun s -> returnS (f s) s)
+
+val updateS : forall 'regs 'e. (sequential_state 'regs -> sequential_state 'regs) -> monadS 'regs unit 'e
+let updateS f = (fun s -> returnS () (f s))
 
 val failS : forall 'regs 'a 'e. string -> monadS 'regs 'a 'e
 let failS msg s = [(Ex (Failure msg), s)]
 
+val exitS : forall 'regs 'e 'a. unit -> monadS 'regs 'a 'e
+let exitS () = failS "exit"
+
 val throwS : forall 'regs 'a 'e. 'e -> monadS 'regs 'a 'e
 let throwS e s = [(Ex (Throw e), s)]
 
@@ -63,7 +74,6 @@ let try_catchS m h s =
   List.concatMap (function
                   | (Value a, s') -> returnS a s'
                   | (Ex (Throw e), s') -> h e s'
-                  | (Ex Exit, s') -> [(Ex Exit, s')]
                   | (Ex (Failure msg), s') -> [(Ex (Failure msg), s')]
                   end) (m s)
 
@@ -99,85 +109,77 @@ let try_catchSR m h =
       | Right e -> h e
      end)
 
-val range : integer -> integer -> list integer
-let rec range i j =
-  if j < i then []
-  else if i = j then [i]
-  else i :: range (i+1) j
-
-val get_regS : forall 'regs 'rv 'a. sequential_state 'regs -> register_ref 'regs 'rv 'a -> 'a
-let get_regS state reg = reg.read_from state.regstate
-
-val set_regS : forall 'regs 'rv 'a. sequential_state 'regs -> register_ref 'regs 'rv 'a -> 'a -> sequential_state 'regs
-let set_regS state reg v =
-  <| state with regstate = reg.write_to state.regstate v |>
-
-
-val read_memS : forall 'regs 'e. read_kind -> integer -> integer -> monadS 'regs (list memory_byte) 'e
-let read_memS read_kind addr sz s =
-  (*let addr = unsigned (bitv_of_address_lifted addr) in
-  let sz = integerFromNat sz in*)
-  let addrs = range addr (addr+sz-1) in
-  match just_list (List.map (fun addr -> Map.lookup addr s.memstate) addrs) with
+val read_tagS : forall 'regs 'a 'e. Bitvector 'a => 'a -> monadS 'regs bitU 'e
+let read_tagS addr =
+  readS (fun s -> fromMaybe B0 (Map.lookup (unsigned addr) s.tagstate))
+
+(* Read bytes from memory and return in little endian order *)
+val read_mem_bytesS : forall 'regs 'e 'a. Bitvector 'a => read_kind -> 'a -> nat -> monadS 'regs (list memory_byte) 'e
+let read_mem_bytesS read_kind addr sz =
+  let addr = unsigned addr in
+  let sz = integerFromNat sz in
+  let addrs = index_list addr (addr+sz-1) 1 in
+  let read_byte s addr = Map.lookup addr s.memstate in
+  readS (fun s -> just_list (List.map (read_byte s) addrs)) >>$= (function
     | Just mem_val ->
-       let s' =
+       updateS (fun s ->
          if read_is_exclusive read_kind
          then <| s with last_exclusive_operation_was_load = true |>
-         else s
-       in
-       returnS (List.reverse mem_val) s'
-    | Nothing -> failS "read_memS" s
-  end
-
-(* caps are aligned at 32 bytes *)
-let cap_alignment = (32 : integer)
-
-val read_tagS : forall 'regs 'a 'e. Bitvector 'a => read_kind -> 'a -> monadS 'regs bitU 'e
-let read_tagS read_kind addr state =
-  let addr = (unsigned addr) / cap_alignment in
-  let tag = match (Map.lookup addr state.tagstate) with
-    | Just t -> t
-    | Nothing -> B0
-  end in
-  if read_is_exclusive read_kind
-  then [(Value tag, <| state with last_exclusive_operation_was_load = true |>)]
-  else [(Value tag, state)]
+         else s) >>$
+       returnS mem_val
+    | Nothing -> failS "read_memS"
+  end)
+
+val read_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs 'b 'e
+let read_memS rk a sz =
+  read_mem_bytesS rk a (natFromInteger sz) >>$= (fun bytes ->
+  returnS (bits_of_mem_bytes bytes))
 
 val excl_resultS : forall 'regs 'e. unit -> monadS 'regs bool 'e
-let excl_resultS () state =
-  let success =
-    (Value true,  <| state with last_exclusive_operation_was_load = false |>) in
-  (Value false, state) :: if state.last_exclusive_operation_was_load then [success] else []
-
-val write_mem_eaS : forall 'regs 'e. write_kind -> integer -> integer -> monadS 'regs unit 'e
-let write_mem_eaS write_kind addr sz state =
-  (*let addr = unsigned (bitv_of_address_lifted addr) in
-  let sz = integerFromNat sz in*)
-  [(Value (), <| state with write_ea = Just (write_kind, addr, sz) |>)]
-
-val write_mem_valS : forall 'regs 'e. list memory_byte -> monadS 'regs bool 'e
-let write_mem_valS v state =
-  let (_,addr,sz) = match state.write_ea with
-    | Nothing -> failwith "write ea has not been announced yet"
-    | Just write_ea -> write_ea end in
-  let addrs = range addr (addr+sz-1) in
-  (*let v = external_mem_value (bits_of v) in*)
-  let addresses_with_value = List.zip addrs (List.reverse v) in
-  let memstate = List.foldl (fun mem (addr,v) -> Map.insert addr v mem)
-                            state.memstate addresses_with_value in
-  [(Value true,  <| state with memstate = memstate |>)]
+let excl_resultS () =
+  readS (fun s -> s.last_exclusive_operation_was_load) >>$= (fun excl_load ->
+  updateS (fun s -> <| s with last_exclusive_operation_was_load = false |>) >>$
+  chooseS (if excl_load then [false; true] else [false]))
+
+val write_mem_eaS : forall 'regs 'e 'a. Bitvector 'a => write_kind -> 'a -> nat -> monadS 'regs unit 'e
+let write_mem_eaS write_kind addr sz =
+  let addr = unsigned addr in
+  let sz = integerFromNat sz in
+  updateS (fun s -> <| s with write_ea = Just (write_kind, addr, sz) |>)
+
+(* Write little-endian list of bytes to previously announced address *)
+val write_mem_bytesS : forall 'regs 'e. list memory_byte -> monadS 'regs bool 'e
+let write_mem_bytesS v =
+  readS (fun s -> s.write_ea) >>$= (function
+      | Nothing -> failS "write ea has not been announced yet"
+      | Just (_, addr, sz) ->
+         let addrs = index_list addr (addr+sz-1) 1 in
+         (*let v = external_mem_value (bits_of v) in*)
+         let a_v = List.zip addrs v in
+         let write_byte mem (addr, v) = Map.insert addr v mem in
+         updateS (fun s ->
+           <| s with memstate = List.foldl write_byte s.memstate a_v |>) >>$
+         returnS true
+    end)
+
+val write_mem_valS : forall 'regs 'e 'a. Bitvector 'a => 'a -> monadS 'regs bool 'e
+let write_mem_valS v = match mem_bytes_of_bits v with
+  | Just v -> write_mem_bytesS v
+  | Nothing -> failS "write_mem_val"
+end
 
 val write_tagS : forall 'regs 'e. bitU -> monadS 'regs bool 'e
-let write_tagS t state =
-  let (_,addr,_) = match state.write_ea with
-    | Nothing -> failwith "write ea has not been announced yet"
-    | Just write_ea -> write_ea end in
-  let taddr = addr / cap_alignment in
-  let tagstate = Map.insert taddr t state.tagstate in
-  [(Value true,  <| state with tagstate = tagstate |>)]
+let write_tagS t =
+  readS (fun s -> s.write_ea) >>$= (function
+      | Nothing -> failS "write ea has not been announced yet"
+      | Just (_, addr, _) ->
+         (*let taddr = addr / cap_alignment in*)
+         updateS (fun s -> <| s with tagstate = Map.insert addr t s.tagstate |>) >>$
+         returnS true
+    end)
 
 val read_regS : forall 'regs 'rv 'a 'e. register_ref 'regs 'rv 'a -> monadS 'regs 'a 'e
-let read_regS reg s = [(Value (reg.read_from s.regstate), s)]
+let read_regS reg = readS (fun s -> reg.read_from s.regstate)
 
 (* TODO
 let read_reg_range reg i j state =
@@ -195,23 +197,23 @@ let read_reg_bitfield reg regfield =
 
 val read_regvalS : forall 'regs 'rv 'e.
   register_accessors 'regs 'rv -> string -> monadS 'regs 'rv 'e
-let read_regvalS (read, _) reg s =
-  match read reg s.regstate with
-    | Just v ->  returnS v s
-    | Nothing -> failS ("read_regvalS " ^ reg) s
-  end
+let read_regvalS (read, _) reg =
+  readS (fun s -> read reg s.regstate) >>$= (function
+      | Just v ->  returnS v
+      | Nothing -> failS ("read_regvalS " ^ reg)
+    end)
 
 val write_regvalS : forall 'regs 'rv 'e.
   register_accessors 'regs 'rv -> string -> 'rv -> monadS 'regs unit 'e
-let write_regvalS (_, write) reg v s =
-  match write reg v s.regstate with
-    | Just rs' -> returnS () (<| s with regstate = rs' |>)
-    | Nothing ->  failS ("write_regvalS " ^ reg) s
-  end
+let write_regvalS (_, write) reg v =
+  readS (fun s -> write reg v s.regstate) >>$= (function
+      | Just rs' -> updateS (fun s -> <| s with regstate = rs' |>)
+      | Nothing ->  failS ("write_regvalS " ^ reg)
+    end)
 
 val write_regS : forall 'regs 'rv 'a 'e. register_ref 'regs 'rv 'a -> 'a -> monadS 'regs unit 'e
-let write_regS reg v state =
-  [(Value (), <| state with regstate = reg.write_to state.regstate v |>)]
+let write_regS reg v =
+  updateS (fun s -> <| s with regstate = reg.write_to v s.regstate |>)
 
 (* TODO
 val update_reg : forall 'regs 'rv 'a 'b 'e. register_ref 'regs 'rv 'a -> ('a -> 'b -> 'a) -> 'b -> monadS 'regs unit 'e
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index ac8ad48d..a0390a94 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -622,13 +622,13 @@ let doc_exp_lem, doc_let_lem =
                  | E_aux (E_let (LB_aux (LB_val (
                      P_aux (P_typ (_, P_aux (P_var (P_aux (P_id id, _), _), _)), _), _), _), body), _) -> id, body
                  | _ -> raise (Reporting_basic.err_unreachable l ("Unable to find loop variable in " ^ string_of_exp body)) in
-               let combinator = match effectful (effect_of body), ord_exp with
-                 | false, E_aux (E_lit (L_aux (L_false, _)), _) -> "foreach_dec"
-                 | false, E_aux (E_lit (L_aux (L_true, _)), _) -> "foreach_inc"
-                 | true, E_aux (E_lit (L_aux (L_false, _)), _) -> "foreachM_dec"
-                 | true, E_aux (E_lit (L_aux (L_true, _)), _) -> "foreachM_inc"
-                 | _ -> raise (Reporting_basic.err_unreachable l "Unable to figure out loop combinator") in
-               let indices_pp = parens (separate_map comma expY [exp1; exp2; exp3]) in
+               let step = match ord_exp with
+                 | E_aux (E_lit (L_aux (L_false, _)), _) ->
+                    parens (separate space [string "integerNegate"; expY exp3])
+                 | _ -> expY exp3
+               in
+               let combinator = if effectful (effect_of body) then "foreachM" else "foreach" in
+               let indices_pp = parens (separate space [string "index_list"; expY exp1; expY exp2; step]) in
                parens (
                    (prefix 2 1)
                      ((separate space) [string combinator; indices_pp; expY vartuple])
@@ -643,11 +643,14 @@ let doc_exp_lem, doc_let_lem =
           begin
             match args with
             | [cond; varstuple; body] ->
-               let csuffix = match effectful (effect_of cond), effectful (effect_of body) with
-                 | false, false -> "_PP"
-                 | false, true  -> "_PM"
-                 | true,  false -> "_MP"
-                 | true,  true  -> "_MM" in
+               let return (E_aux (e, a)) = E_aux (E_internal_return (E_aux (e, a)), a) in
+               let csuffix, cond, body =
+                 match effectful (effect_of cond), effectful (effect_of body) with
+                   | false, false -> "", cond, body
+                   | false, true  -> "M", return cond, body
+                   | true,  false -> "M", cond, return body
+                   | true,  true  -> "M", cond, body
+               in
                parens (
                    (prefix 2 1)
                      ((separate space) [string (combinator ^ csuffix); expY varstuple])
@@ -717,7 +720,7 @@ let doc_exp_lem, doc_let_lem =
         | Some(env, (Typ_aux (Typ_app (tid, _), _)), _)
           when Env.is_record tid env ->
            let fname =
-             if prefix_recordtype
+             if prefix_recordtype && string_of_id tid <> "regstate"
              then (string (string_of_id tid ^ "_")) ^^ doc_id_lem id
              else doc_id_lem id in
            expY fexp ^^ dot ^^ fname
@@ -732,10 +735,11 @@ let doc_exp_lem, doc_let_lem =
        let eff = effect_of full_exp in
        let base_typ = Env.base_typ_of env typ in
        if has_effect eff BE_rreg then
-         let epp = separate space [string "read_reg";doc_id_lem id] in
+         let epp = separate space [string "read_reg";doc_id_lem (append_id id "_ref")] in
          if is_bitvector_typ base_typ
          then liftR (parens (epp ^^ doc_tannot_lem ctxt env true base_typ))
          else liftR epp
+       else if Env.is_register id env then doc_id_lem (append_id id "_ref")
        else if is_ctor env id then doc_id_lem_ctor id
        else doc_id_lem id
     | E_lit lit -> doc_lit_lem lit
@@ -870,7 +874,7 @@ let doc_exp_lem, doc_let_lem =
 
   and doc_fexp ctxt recordtyp (FE_aux(FE_Fexp(id,e),_)) =
     let fname =
-      if prefix_recordtype
+      if prefix_recordtype && string_of_id recordtyp <> "regstate"
       then (string (string_of_id recordtyp ^ "_")) ^^ doc_id_lem id
       else doc_id_lem id in
     group (doc_op equals fname (top_exp ctxt true e))
@@ -886,8 +890,8 @@ let doc_exp_lem, doc_let_lem =
   and doc_lexp_deref_lem ctxt ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with
     | LEXP_field (le,id) ->
        parens (separate empty [doc_lexp_deref_lem ctxt le;dot;doc_id_lem id])
-    | LEXP_id id -> doc_id_lem id
-    | LEXP_cast (typ,id) -> doc_id_lem id
+    | LEXP_id id -> doc_id_lem (append_id id "_ref")
+    | LEXP_cast (typ,id) -> doc_id_lem (append_id id "_ref")
     | LEXP_tup lexps -> parens (separate_map comma_sp (doc_lexp_deref_lem ctxt) lexps)
     | _ ->
        raise (Reporting_basic.err_unreachable l ("doc_lexp_deref_lem: Unsupported lexp"))
@@ -911,7 +915,7 @@ let doc_typdef_lem (TD_aux(td, (l, annot))) = match td with
        (separate space [string "type"; doc_id_lem_type id; doc_typquant_items_lem None typq])
        (doc_typschm_lem false typschm)
   | TD_record(id,nm,typq,fs,_) ->
-    let fname fid = if prefix_recordtype
+    let fname fid = if prefix_recordtype && string_of_id id <> "regstate"
                     then concat [doc_id_lem id;string "_";doc_id_lem_type fid;]
                     else doc_id_lem_type fid in
     let f_pp (typ,fid) =
@@ -1420,7 +1424,7 @@ let pp_defs_lem (types_file,types_modules) (defs_file,defs_modules) (Defs defs)
   let exc_typ = find_exc_typ defs in
   let typdefs, defs = List.partition is_typ_def defs in
   let statedefs, defs = List.partition is_state_def defs in
-  let register_refs = State.register_refs_lem prefix_recordtype !opt_mwords (State.find_registers defs) in
+  let register_refs = State.register_refs_lem !opt_mwords (State.find_registers defs) in
   (print types_file)
     (concat
        [string "(*" ^^ (string top_line) ^^ string "*)";hardline;
diff --git a/src/process_file.ml b/src/process_file.ml
index 80cfdccb..a447061b 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -48,6 +48,9 @@
 (*  SUCH DAMAGE.                                                          *)
 (**************************************************************************)
 
+open PPrint
+open Pretty_print_common
+
 let opt_lem_sequential = ref false
 let opt_lem_mwords = ref false
 
@@ -243,7 +246,22 @@ let output_lem filename libs defs =
       "Sail_values";
       operators_module
     ] @ monad_modules
-    in
+  in
+  let isa_thy_name = String.capitalize filename ^ "_lemmas" in
+  let isa_lemmas =
+    separate hardline [
+      string ("theory " ^ isa_thy_name);
+      string  "  imports";
+      string  "    Sail.Sail_values_extras";
+      string  "    Sail.State_extras";
+      string ("    " ^ String.capitalize filename);
+      string  "begin";
+      string  "";
+      State.generate_isa_lemmas !Pretty_print_lem.opt_mwords defs;
+      string  "";
+      string  "end"
+    ] ^^ hardline
+  in
   let ((ot,_, _) as ext_ot) =
     open_output_with_check_unformatted (filename ^ "_types" ^ ".lem") in
   let ((o,_, _) as ext_o) =
@@ -253,7 +271,11 @@ let output_lem filename libs defs =
      (o, base_imports @ (String.capitalize types_module :: libs))
      defs generated_line);
   close_output_with_check ext_ot;
-  close_output_with_check ext_o
+  close_output_with_check ext_o;
+  let ((ol, _, _) as ext_ol) =
+    open_output_with_check_unformatted (isa_thy_name ^ ".thy") in
+  print ol isa_lemmas;
+  close_output_with_check ext_ol
 
 let rec iterate (f : int -> unit) (n : int) : unit =
   if n = 0 then ()
diff --git a/src/state.ml b/src/state.ml
index 5873c472..690c7948 100644
--- a/src/state.ml
+++ b/src/state.ml
@@ -177,7 +177,7 @@ let rec regval_convs_lem mwords (Typ_aux (t, _) as typ) = match t with
      let id = string_of_id (regval_constr_id mwords typ) in
      "(fun v -> " ^ id ^ "_of_regval v)", "(fun v -> regval_of_" ^ id ^ " v)"
 
-let register_refs_lem prefix_recordtype mwords registers =
+let register_refs_lem mwords registers =
   let generic_convs =
     separate_map hardline string [
       "val vector_of_regval : forall 'a. (register_value -> maybe 'a) -> register_value -> maybe (list 'a)";
@@ -212,20 +212,20 @@ let register_refs_lem prefix_recordtype mwords registers =
   in
   let register_ref (typ, id) =
     let idd = string (string_of_id id) in
-    let field = if prefix_recordtype then string "regstate_" ^^ idd else idd in
+    (* let field = if prefix_recordtype then string "regstate_" ^^ idd else idd in *)
     let of_regval, regval_of = regval_convs_lem mwords typ in
-    concat [string "let "; idd; string " = <|"; hardline;
+    concat [string "let "; idd; string "_ref = <|"; hardline;
       string "  name = \""; idd; string "\";"; hardline;
-      string "  read_from = (fun s -> s."; field; string ");"; hardline;
-      string "  write_to = (fun s v -> (<| s with "; field; string " = v |>));"; hardline;
+      string "  read_from = (fun s -> s."; idd; string ");"; hardline;
+      string "  write_to = (fun v s -> (<| s with "; idd; string " = v |>));"; hardline;
       string "  of_regval = "; string of_regval; string ";"; hardline;
       string "  regval_of = "; string regval_of; string " |>"; hardline]
   in
   let refs = separate_map hardline register_ref registers in
   let get_set_reg (_, id) =
     let idd = string_of_id id in
-    string ("  if reg_name = \"" ^ idd ^ "\" then Just (" ^ idd ^ ".regval_of (" ^ idd ^ ".read_from s)) else"),
-    string ("  if reg_name = \"" ^ idd ^ "\" then Maybe.map (" ^ idd ^ ".write_to s) (" ^ idd ^ ".of_regval v) else")
+    string ("  if reg_name = \"" ^ idd ^ "\" then Just (" ^ idd ^ "_ref.regval_of (" ^ idd ^ "_ref.read_from s)) else"),
+    string ("  if reg_name = \"" ^ idd ^ "\" then Maybe.map (fun v -> " ^ idd ^ "_ref.write_to v s) (" ^ idd ^ "_ref.of_regval v) else")
   in
   let getters_setters =
     let getters, setters = List.split (List.map get_set_reg registers) in
@@ -237,11 +237,72 @@ let register_refs_lem prefix_recordtype mwords registers =
     string "let set_regval reg_name v s =" ^^ hardline ^^
     separate hardline setters ^^ hardline ^^
     string "  Nothing" ^^ hardline ^^ hardline ^^
-    string "let register_accessors = (get_regval, set_regval)" ^^ hardline ^^ hardline ^^
-    string "let liftS s = liftState register_accessors s" ^^ hardline
+    string "let register_accessors = (get_regval, set_regval)" ^^ hardline ^^ hardline
+    (* string "let liftS s = liftState register_accessors s" ^^ hardline *)
   in
   separate hardline [generic_convs; refs; getters_setters]
 
+let generate_isa_lemmas mwords (Defs defs : tannot defs) =
+  let rec drop_while f = function
+    | x :: xs when f x -> drop_while f xs
+    | xs -> xs
+  in
+  let remove_leading_underscores str =
+    String.concat "_" (drop_while (fun s -> s = "") (Util.split_on_char '_' str))
+  in
+  let remove_trailing_underscores str =
+    Util.split_on_char '_' str |> List.rev |>
+    drop_while (fun s -> s = "") |> List.rev |>
+    String.concat "_"
+  in
+  let registers = find_registers defs in
+  let regtyp_ids =
+    register_base_types mwords (List.map fst registers)
+    |> Bindings.bindings |> List.map fst
+  in
+  let register_defs =
+    let reg_id id = remove_leading_underscores (string_of_id id) in
+    hang 2 (flow_map (break 1) string
+      (["lemmas register_defs"; "="; "get_regval_def"; "set_regval_def"] @
+      (List.map (fun (typ, id) -> reg_id id ^ "_ref_def") registers)))
+  in
+  let conv_lemma typ_id =
+    let typ_id = remove_trailing_underscores (string_of_id typ_id) in
+    let typ_id' = remove_leading_underscores typ_id in
+    string ("lemma regval_" ^ typ_id ^ "[simp]:") ^^ hardline ^^
+    string ("  \"" ^ typ_id' ^ "_of_regval (regval_of_" ^ typ_id ^ " v) = Some v\"") ^^ hardline ^^
+    string ("  by (auto simp: regval_of_" ^ typ_id ^ "_def)")
+  in
+  let register_lemmas (typ, id) =
+    let id = remove_leading_underscores (string_of_id id) in
+    let id' = remove_trailing_underscores id in
+    separate_map hardline string [
+      "lemma liftS_read_reg_" ^ id ^ "[simp]:";
+      "  \"liftS (read_reg " ^ id ^ "_ref) = readS (" ^ id' ^ " \\<circ> regstate)\"";
+      "  by (auto simp: liftState_read_reg_readS register_defs)";
+      "";
+      "lemma liftS_write_reg_" ^ id ^ "[simp]:";
+      "  \"liftS (write_reg " ^ id ^ "_ref v) = updateS (regstate_update (" ^ id' ^ "_update (\\<lambda>_. v)))\"";
+      "  by (auto simp: liftState_write_reg_updateS register_defs)"
+    ]
+  in
+  string "abbreviation \"liftS \\<equiv> liftState (get_regval, set_regval)\"" ^^
+  hardline ^^ hardline ^^
+  register_defs ^^
+  hardline ^^ hardline ^^
+  separate_map (hardline ^^ hardline) conv_lemma regtyp_ids ^^
+  hardline ^^ hardline ^^
+  separate_map hardline string [
+    "lemma vector_of_rv_rv_of_vector[simp]:";
+    "  assumes \"\\<And>v. of_rv (rv_of v) = Some v\"";
+    "  shows \"vector_of_regval of_rv (regval_of_vector rv_of len is_inc v) = Some v\"";
+    "proof -";
+    "  from assms have \"of_rv \\<circ> rv_of = Some\" by auto";
+    "  then show ?thesis by (auto simp: vector_of_regval_def regval_of_vector_def)";
+    "qed"] ^^
+  hardline ^^ hardline ^^
+  separate_map (hardline ^^ hardline) register_lemmas registers
+
 let generate_regstate_defs mwords defs =
   (* FIXME We currently don't want to generate undefined_type functions
      for register state and values.  For the Lem backend, this would require
diff --git a/src/type_check.mli b/src/type_check.mli
index b03e2e00..4685b676 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -148,6 +148,8 @@ module Env : sig
 
   val is_union_constructor : id -> t -> bool
 
+  val is_register : id -> t -> bool
+
   (** Return a fresh kind identifier that doesn't exist in the
      environment. The optional argument bases the new identifer on the
      old one. *)