From 05c03453c25f1c259670283a9a92a6c21c9ec319 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Fri, 19 Oct 2018 12:02:20 +0100
Subject: Fix Isabelle library

---
 lib/isabelle/Sail2_prompt_monad_lemmas.thy | 76 +++++++++++-------------------
 lib/isabelle/Sail2_state_lemmas.thy        | 24 ++++++----
 lib/isabelle/Sail2_state_monad_lemmas.thy  | 21 +++++----
 3 files changed, 55 insertions(+), 66 deletions(-)

(limited to 'lib')

diff --git a/lib/isabelle/Sail2_prompt_monad_lemmas.thy b/lib/isabelle/Sail2_prompt_monad_lemmas.thy
index 25eb9f52..406b5871 100644
--- a/lib/isabelle/Sail2_prompt_monad_lemmas.thy
+++ b/lib/isabelle/Sail2_prompt_monad_lemmas.thy
@@ -30,42 +30,17 @@ 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"
+| 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 t k), E_write_mem 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"
+| Undefined: "((Undefined k), E_undefined v, k v) \<in> T"
+| Print: "((Print msg k), E_print msg, k) \<in> T"
 
 inductive_set Traces :: "(('rv, 'a, 'e) monad \<times> 'rv event list \<times> ('rv, 'a, 'e) monad) set" where
   Nil: "(s, [], s) \<in> Traces"
@@ -85,25 +60,28 @@ 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 tag where "m = Read_mem rk addr s k" and "t = E_read_mem rk addr s (v, tag) # t'" and "(k (v, tag), t', m') \<in> Traces"
+  | (Write_mem) wk addr sz val tag k t' v where "m = Write_mem wk addr sz val tag k" and "t = E_write_mem 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"
+  | (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"
 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_mem 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"
diff --git a/lib/isabelle/Sail2_state_lemmas.thy b/lib/isabelle/Sail2_state_lemmas.thy
index ba69d0d8..25d4edea 100644
--- a/lib/isabelle/Sail2_state_lemmas.thy
+++ b/lib/isabelle/Sail2_state_lemmas.thy
@@ -18,7 +18,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]
@@ -82,7 +82,10 @@ 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)
+  by (auto simp: read_mem_def read_mem_bytes_def read_memS_def read_mem_bytesS_def maybe_failS_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
+           cong: option.case_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"
@@ -91,17 +94,22 @@ lemma liftState_read_mem[liftState_simp]:
 
 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)
+  shows "liftState r (write_mem_ea BCa rk a sz) = returnS ()"
+  using assms by (auto simp: write_mem_ea_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)"
+  "\<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 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_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)
+  "liftState r (write_mem BC_mword BCv wk addr sz v t) = write_memS BC_mword BCv wk addr sz v t"
+  by (auto simp: write_mem_def write_memS_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)"
diff --git a/lib/isabelle/Sail2_state_monad_lemmas.thy b/lib/isabelle/Sail2_state_monad_lemmas.thy
index 3a286c10..b2fde7ba 100644
--- a/lib/isabelle/Sail2_state_monad_lemmas.thy
+++ b/lib/isabelle/Sail2_state_monad_lemmas.thy
@@ -205,24 +205,27 @@ lemma no_throw_basic_builtins[simp]:
 
 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>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>BC wk addr sz v t s. ignore_throw (write_mem_bytesS BC wk addr sz v t) s = write_mem_bytesS BC wk addr sz v t s"
+  "\<And>BC_a BC_v wk addr sz v t s. ignore_throw (write_memS BC_a BC_v wk addr sz v t) s = write_memS BC_a BC_v 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_memS_def read_tagS_def write_memS_def
+  unfolding write_mem_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)
+           simp: prod.case_distrib ignore_throw_option_case_distrib ignore_throw_let_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)
+  by (auto simp: read_memS_def no_throw_mem_builtins prod.case_distrib comp_def cong: bindS_ext_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: option.case_distrib cong: bindS_cong option.case_cong)
-- 
cgit v1.2.3


From d733aa5c7409c645807589d268c0b80055bf671d Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Tue, 20 Nov 2018 18:32:37 +0000
Subject: Use nat instead of (list bitU) for addresses in monad outcomes

Removes some friction by back-and-forth conversion when handling events
---
 lib/isabelle/Sail2_state_lemmas.thy       | 12 ++++++------
 lib/isabelle/Sail2_state_monad_lemmas.thy |  4 ++--
 2 files changed, 8 insertions(+), 8 deletions(-)

(limited to 'lib')

diff --git a/lib/isabelle/Sail2_state_lemmas.thy b/lib/isabelle/Sail2_state_lemmas.thy
index 25d4edea..edcd9593 100644
--- a/lib/isabelle/Sail2_state_lemmas.thy
+++ b/lib/isabelle/Sail2_state_lemmas.thy
@@ -93,19 +93,19 @@ lemma liftState_read_mem[liftState_simp]:
   by (auto simp: liftState_read_mem_BC)
 
 lemma liftState_write_mem_ea_BC:
-  assumes "unsigned_method BC_bitU_list (bits_of_method BCa a) = unsigned_method BCa a"
+  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)
+  using assms by (auto simp: write_mem_ea_def nat_of_bv_def maybe_fail_def)
 
-lemma liftState_write_mem_ea[liftState_simp]:
+(*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)
+  by (auto simp: liftState_write_mem_ea_BC)*)
 
-lemma write_mem_bytesS_def_BC_bitU_list_BC_mword[simp]:
+(*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)
+  by (auto simp: write_mem_bytesS_def)*)
 
 lemma liftState_write_mem_val[liftState_simp]:
   "liftState r (write_mem BC_mword BCv wk addr sz v t) = write_memS BC_mword BCv wk addr sz v t"
diff --git a/lib/isabelle/Sail2_state_monad_lemmas.thy b/lib/isabelle/Sail2_state_monad_lemmas.thy
index b2fde7ba..6fb5e7ef 100644
--- a/lib/isabelle/Sail2_state_monad_lemmas.thy
+++ b/lib/isabelle/Sail2_state_monad_lemmas.thy
@@ -211,9 +211,9 @@ lemma ignore_throw_let_distrib: "ignore_throw (let x = y in f x) = (let x = y in
   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>BC rk a sz s. ignore_throw (read_mem_bytesS rk a sz) s = read_mem_bytesS rk a sz s"
   "\<And>BC a s. ignore_throw (read_tagS BC a) s = read_tagS BC a s"
-  "\<And>BC wk addr sz v t s. ignore_throw (write_mem_bytesS BC wk addr sz v t) s = write_mem_bytesS BC wk addr sz v t s"
+  "\<And>BC wk addr sz v t s. ignore_throw (write_mem_bytesS wk addr sz v t) s = write_mem_bytesS wk addr sz v t s"
   "\<And>BC_a BC_v wk addr sz v t s. ignore_throw (write_memS BC_a BC_v wk addr sz v t) s = write_memS BC_a BC_v 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"
-- 
cgit v1.2.3


From c0f8dd2e676c4ce987c73392506dff8872a364ef Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Thu, 29 Nov 2018 15:13:50 +0000
Subject: Add some helper lemmas to Isabelle lib

---
 lib/isabelle/Sail2_state_lemmas.thy  | 121 ++++++++++++++++++++++++++++++++++-
 lib/isabelle/Sail2_values_lemmas.thy |  28 ++++++++
 2 files changed, 148 insertions(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/isabelle/Sail2_state_lemmas.thy b/lib/isabelle/Sail2_state_lemmas.thy
index edcd9593..c7d55d31 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
@@ -309,7 +311,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
 
@@ -392,4 +394,121 @@ 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: "((if b then Some x else None) = Some y) \<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_mem wk addr sz v tag r"
+        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)
+
+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_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"
-- 
cgit v1.2.3


From 17334803f125e3b839fdb7a780989d8eba555555 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Thu, 29 Nov 2018 17:58:15 +0000
Subject: Add separate outcome/event for tagged memory loads

Lets one distinguish in a trace whether an instruction tried to read
tagged memory or just read data without caring about the tag;  this is
useful for formulating predicates on traces.
---
 lib/isabelle/Sail2_prompt_monad_lemmas.thy |  6 ++++--
 lib/isabelle/Sail2_state_lemmas.thy        | 27 ++++++++++++++++-----------
 lib/isabelle/Sail2_state_monad_lemmas.thy  | 14 +++++++-------
 3 files changed, 27 insertions(+), 20 deletions(-)

(limited to 'lib')

diff --git a/lib/isabelle/Sail2_prompt_monad_lemmas.thy b/lib/isabelle/Sail2_prompt_monad_lemmas.thy
index 406b5871..c59fc62f 100644
--- a/lib/isabelle/Sail2_prompt_monad_lemmas.thy
+++ b/lib/isabelle/Sail2_prompt_monad_lemmas.thy
@@ -32,6 +32,7 @@ lemmas try_catch_induct[case_names Done Read_mem Write_memv Read_reg Excl_res Wr
 
 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_tagged_mem: "((Read_tagged_mem rk addr sz k), E_read_tagged_mem 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 t k), E_write_mem wk addr sz v t r, k r) \<in> T"
@@ -60,7 +61,8 @@ 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 tag where "m = Read_mem rk addr s k" and "t = E_read_mem rk addr s (v, tag) # t'" and "(k (v, tag), 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_tagged_mem) rk addr s k t' v tag where "m = Read_tagged_mem rk addr s k" and "t = E_read_tagged_mem rk addr s (v, tag) # t'" and "(k (v, tag), t', m') \<in> Traces"
   | (Write_mem) wk addr sz val tag k t' v where "m = Write_mem wk addr sz val tag k" and "t = E_write_mem 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"
@@ -79,7 +81,7 @@ next
   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_mem rk addr sz k v)
+    case (Read_tagged_mem rk addr sz k v)
     then show ?thesis using t m' by (cases v; elim that; blast)
   qed (elim that; blast)+
 qed
diff --git a/lib/isabelle/Sail2_state_lemmas.thy b/lib/isabelle/Sail2_state_lemmas.thy
index c7d55d31..77f4ac5a 100644
--- a/lib/isabelle/Sail2_state_lemmas.thy
+++ b/lib/isabelle/Sail2_state_lemmas.thy
@@ -80,19 +80,20 @@ 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
+lemma liftState_read_tagged_mem[liftState_simp]:
+  shows "liftState r (read_tagged_mem BCa BCb rk a sz) = read_tagged_memS BCa BCb rk a sz"
+  by (auto simp: read_tagged_mem_def read_tagged_mem_bytes_def maybe_failS_def read_tagged_memS_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
-           cong: option.case_cong)
+           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_tagged_memS_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 BCa a = Some a'"
@@ -399,7 +400,10 @@ 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: "((if b then Some x else None) = Some y) \<longleftrightarrow> (b \<and> y = x)"
+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:
@@ -413,7 +417,8 @@ lemma emitEventS_update_cases:
         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)
+  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)
diff --git a/lib/isabelle/Sail2_state_monad_lemmas.thy b/lib/isabelle/Sail2_state_monad_lemmas.thy
index 6fb5e7ef..12452ca4 100644
--- a/lib/isabelle/Sail2_state_monad_lemmas.thy
+++ b/lib/isabelle/Sail2_state_monad_lemmas.thy
@@ -211,22 +211,22 @@ lemma ignore_throw_let_distrib: "ignore_throw (let x = y in f x) = (let x = y in
   by auto
 
 lemma no_throw_mem_builtins:
-  "\<And>BC 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_mem_bytesS rk a sz) s = read_mem_bytesS rk a sz s"
+  "\<And>rk a sz s. ignore_throw (read_tagged_mem_bytesS rk a sz) s = read_tagged_mem_bytesS rk a sz s"
   "\<And>BC a s. ignore_throw (read_tagS BC a) s = read_tagS BC a 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_tagged_memS BCa BCv rk a sz) s = read_tagged_memS BCa BCv rk a sz s"
   "\<And>BC wk addr sz v t s. ignore_throw (write_mem_bytesS wk addr sz v t) s = write_mem_bytesS wk addr sz v t s"
-  "\<And>BC_a BC_v wk addr sz v t s. ignore_throw (write_memS BC_a BC_v wk addr sz v t) s = write_memS BC_a BC_v wk addr sz v t s"
+  "\<And>BCa BCv wk addr sz v t s. ignore_throw (write_memS BCa BCv wk addr sz v t) s = write_memS 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_memS_def
+  unfolding read_mem_bytesS_def read_tagged_mem_bytesS_def read_tagged_memS_def read_memS_def read_tagS_def write_memS_def
   unfolding write_mem_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: prod.case_distrib ignore_throw_option_case_distrib ignore_throw_let_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 prod.case_distrib comp_def cong: bindS_ext_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: option.case_distrib cong: bindS_cong option.case_cong)
 
@@ -234,7 +234,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 *)
 
-- 
cgit v1.2.3


From 747999f5c9f9234d04ef9e574a415a88e2bcb52b Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Fri, 30 Nov 2018 18:28:32 +0000
Subject: Rename Undefined outcome to Choose

It is used for nondeterministic choice, so Undefined might be
misleading.
---
 lib/isabelle/Hoare.thy                         | 22 +++++++++++++++-------
 lib/isabelle/ROOT                              |  2 +-
 lib/isabelle/Sail2_operators_mwords_lemmas.thy |  4 ++--
 lib/isabelle/Sail2_prompt_monad_lemmas.thy     |  8 +++++---
 lib/isabelle/Sail2_state_lemmas.thy            | 12 ++++++++++++
 lib/isabelle/Sail2_state_monad_lemmas.thy      |  6 +++---
 6 files changed, 38 insertions(+), 16 deletions(-)

(limited to 'lib')

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/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 c59fc62f..54f58fad 100644
--- a/lib/isabelle/Sail2_prompt_monad_lemmas.thy
+++ b/lib/isabelle/Sail2_prompt_monad_lemmas.thy
@@ -40,7 +40,7 @@ inductive_set T :: "(('rv, 'a, 'e) monad \<times> 'rv event \<times> ('rv, 'a, '
 | 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"
+| Choose: "((Choose descr k), E_choose descr v, k v) \<in> T"
 | Print: "((Print msg k), E_print msg, k) \<in> T"
 
 inductive_set Traces :: "(('rv, 'a, 'e) monad \<times> 'rv event list \<times> ('rv, 'a, 'e) monad) set" where
@@ -70,7 +70,7 @@ lemma Traces_cases:
   | (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"
+  | (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
@@ -185,8 +185,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 77f4ac5a..d99dfc85 100644
--- a/lib/isabelle/Sail2_state_lemmas.thy
+++ b/lib/isabelle/Sail2_state_lemmas.thy
@@ -45,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"
@@ -149,6 +152,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
@@ -157,6 +168,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)
diff --git a/lib/isabelle/Sail2_state_monad_lemmas.thy b/lib/isabelle/Sail2_state_monad_lemmas.thy
index 12452ca4..ca7e5751 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,9 +197,10 @@ 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 =
-- 
cgit v1.2.3


From b4495040178bc7552acc76c14de7151583456ee6 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Mon, 3 Dec 2018 12:42:32 +0000
Subject: Make names of memory r/w events more consistent

Use E_read_memt for reading tagged memory, as in sail2_impl_base.lem,
and rename E_write_mem to E_write_memt, since it always writes a tag.
---
 lib/isabelle/Sail2_prompt_monad_lemmas.thy | 10 +++++-----
 lib/isabelle/Sail2_state_lemmas.thy        | 10 +++++-----
 lib/isabelle/Sail2_state_monad_lemmas.thy  |  6 +++---
 3 files changed, 13 insertions(+), 13 deletions(-)

(limited to 'lib')

diff --git a/lib/isabelle/Sail2_prompt_monad_lemmas.thy b/lib/isabelle/Sail2_prompt_monad_lemmas.thy
index 54f58fad..500d260d 100644
--- a/lib/isabelle/Sail2_prompt_monad_lemmas.thy
+++ b/lib/isabelle/Sail2_prompt_monad_lemmas.thy
@@ -32,10 +32,10 @@ lemmas try_catch_induct[case_names Done Read_mem Write_memv Read_reg Excl_res Wr
 
 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_tagged_mem: "((Read_tagged_mem rk addr sz k), E_read_tagged_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 t k), E_write_mem wk addr sz v t 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"
@@ -62,8 +62,8 @@ lemma Traces_cases:
   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_tagged_mem) rk addr s k t' v tag where "m = Read_tagged_mem rk addr s k" and "t = E_read_tagged_mem rk addr s (v, tag) # t'" and "(k (v, tag), t', m') \<in> Traces"
-  | (Write_mem) wk addr sz val tag k t' v where "m = Write_mem wk addr sz val tag k" and "t = E_write_mem wk addr sz val tag 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_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"
@@ -81,7 +81,7 @@ next
   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_tagged_mem rk addr sz k v)
+    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
diff --git a/lib/isabelle/Sail2_state_lemmas.thy b/lib/isabelle/Sail2_state_lemmas.thy
index d99dfc85..05ae99ee 100644
--- a/lib/isabelle/Sail2_state_lemmas.thy
+++ b/lib/isabelle/Sail2_state_lemmas.thy
@@ -83,9 +83,9 @@ 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_tagged_mem[liftState_simp]:
-  shows "liftState r (read_tagged_mem BCa BCb rk a sz) = read_tagged_memS BCa BCb rk a sz"
-  by (auto simp: read_tagged_mem_def read_tagged_mem_bytes_def maybe_failS_def read_tagged_memS_def
+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)
@@ -93,7 +93,7 @@ lemma liftState_read_tagged_mem[liftState_simp]:
 lemma liftState_read_mem[liftState_simp]:
   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_tagged_memS_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)
@@ -422,7 +422,7 @@ lemma emitEventS_update_cases:
   assumes "emitEventS ra e s = Some s'"
   obtains
     (Write_mem) wk addr sz v tag r
-      where "e = E_write_mem wk addr sz v tag r"
+      where "e = E_write_memt wk addr sz v tag r"
         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'"
diff --git a/lib/isabelle/Sail2_state_monad_lemmas.thy b/lib/isabelle/Sail2_state_monad_lemmas.thy
index ca7e5751..d870c4a8 100644
--- a/lib/isabelle/Sail2_state_monad_lemmas.thy
+++ b/lib/isabelle/Sail2_state_monad_lemmas.thy
@@ -212,15 +212,15 @@ lemma ignore_throw_let_distrib: "ignore_throw (let x = y in f x) = (let x = y in
 
 lemma no_throw_mem_builtins:
   "\<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_tagged_mem_bytesS rk a sz) s = read_tagged_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>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_tagged_memS BCa BCv rk a sz) s = read_tagged_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 t s. ignore_throw (write_mem_bytesS wk addr sz v t) s = write_mem_bytesS wk addr sz v t s"
   "\<And>BCa BCv wk addr sz v t s. ignore_throw (write_memS BCa BCv wk addr sz v t) s = write_memS 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_tagged_mem_bytesS_def read_tagged_memS_def read_memS_def read_tagS_def write_memS_def
+  unfolding read_mem_bytesS_def read_memt_bytesS_def read_memtS_def read_memS_def read_tagS_def write_memS_def
   unfolding write_mem_bytesS_def
   unfolding excl_resultS_def undefined_boolS_def maybe_failS_def
   unfolding ignore_throw_bindS
-- 
cgit v1.2.3


From df0e02bc0c8259962f25d4c175fa950391695ab6 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Mon, 3 Dec 2018 16:03:24 +0000
Subject: Add Write_mem event/outcome without tag

The inter-instruction semantics is responsible for correctly handling memory
writes without tags; the lifting to the state monad handles it as writing a
value with a zero tag bit.
---
 lib/isabelle/Sail2_prompt_monad_lemmas.thy |  2 ++
 lib/isabelle/Sail2_state_lemmas.thy        | 13 +++++++++----
 lib/isabelle/Sail2_state_monad_lemmas.thy  | 10 ++++++----
 3 files changed, 17 insertions(+), 8 deletions(-)

(limited to 'lib')

diff --git a/lib/isabelle/Sail2_prompt_monad_lemmas.thy b/lib/isabelle/Sail2_prompt_monad_lemmas.thy
index 500d260d..3658296b 100644
--- a/lib/isabelle/Sail2_prompt_monad_lemmas.thy
+++ b/lib/isabelle/Sail2_prompt_monad_lemmas.thy
@@ -35,6 +35,7 @@ inductive_set T :: "(('rv, 'a, 'e) monad \<times> 'rv event \<times> ('rv, 'a, '
 | 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"
@@ -63,6 +64,7 @@ lemma Traces_cases:
   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_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"
diff --git a/lib/isabelle/Sail2_state_lemmas.thy b/lib/isabelle/Sail2_state_lemmas.thy
index 05ae99ee..8b189f7a 100644
--- a/lib/isabelle/Sail2_state_lemmas.thy
+++ b/lib/isabelle/Sail2_state_lemmas.thy
@@ -113,9 +113,14 @@ lemma liftState_write_mem_ea_BC:
    write_mem_bytesS BC_mword wk addr sz v t"
   by (auto simp: write_mem_bytesS_def)*)
 
-lemma liftState_write_mem_val[liftState_simp]:
-  "liftState r (write_mem BC_mword BCv wk addr sz v t) = write_memS BC_mword BCv wk addr sz v t"
-  by (auto simp: write_mem_def write_memS_def liftState_simp split: option.splits)
+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)"
@@ -422,7 +427,7 @@ 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"
+      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'"
diff --git a/lib/isabelle/Sail2_state_monad_lemmas.thy b/lib/isabelle/Sail2_state_monad_lemmas.thy
index d870c4a8..1e9f50cc 100644
--- a/lib/isabelle/Sail2_state_monad_lemmas.thy
+++ b/lib/isabelle/Sail2_state_monad_lemmas.thy
@@ -216,12 +216,14 @@ lemma no_throw_mem_builtins:
   "\<And>BC a s. ignore_throw (read_tagS BC a) s = read_tagS BC a 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 t s. ignore_throw (write_mem_bytesS wk addr sz v t) s = write_mem_bytesS wk addr sz v t s"
-  "\<And>BCa BCv wk addr sz v t s. ignore_throw (write_memS BCa BCv wk addr sz v t) s = write_memS BCa BCv wk addr sz v t 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_memt_bytesS_def read_memtS_def read_memS_def read_tagS_def write_memS_def
-  unfolding write_mem_bytesS_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
-- 
cgit v1.2.3


From 586b5f5c27bef271a9a013cad8d5b132df354c23 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Mon, 17 Dec 2018 20:29:11 +0000
Subject: Changes for ASL parser

---
 lib/flow.sail | 23 +++++++++++++----------
 1 file changed, 13 insertions(+), 10 deletions(-)

(limited to 'lib')

diff --git a/lib/flow.sail b/lib/flow.sail
index 5c182af2..1655a719 100644
--- a/lib/flow.sail
+++ b/lib/flow.sail
@@ -9,30 +9,33 @@ 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", 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 or_bool = {coq: "orb", _: "or_bool"} : forall ('p : Bool) ('q : Bool). (bool('p), bool('q)) -> bool('p | 'q)
+
+val eq_int = {ocaml: "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", 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}
-- 
cgit v1.2.3


From 24c2f4c5d9224d094083e2b4859b39c2ca0b1071 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Tue, 18 Dec 2018 18:06:55 +0000
Subject: Fix rewriter issues

Fixes some re-writer issues that was preventing RISC-V from building
with new flow-typing constraints. Unfortunately because the flow
typing now understands slightly more about boolean variables, the very
large nested case statements with matches predicates produced by the
string-matching end up causing a huge blowup in the overall
compilation time.
---
 lib/flow.sail | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'lib')

diff --git a/lib/flow.sail b/lib/flow.sail
index 1655a719..cb77f5b1 100644
--- a/lib/flow.sail
+++ b/lib/flow.sail
@@ -20,6 +20,9 @@ val not_bool = {coq: "negb", _: "not"} : forall ('p : Bool). bool('p) -> bool(no
    or_bool that are not shown here. */
 
 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", lem: "eq", c: "eq_int", coq: "Z.eqb"} : forall 'n 'm. (int('n), int('m)) -> bool('n == 'm)
-- 
cgit v1.2.3


From 36d876fd74d8fdcb9bb54a4c0aa220f0ab14e5da Mon Sep 17 00:00:00 2001
From: Alastair Reid
Date: Fri, 4 Jan 2019 10:55:19 +0000
Subject: C library: fix fprintf warnings in lib/elf.c

---
 lib/elf.c | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'lib')

diff --git a/lib/elf.c b/lib/elf.c
index 4355b44c..888169f5 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 %llu\n",
                     rdHalf64(le, ehdr->e_shnum), rdOff64(le, ehdr->e_shoff));
             exit(EXIT_FAILURE);
         }
-- 
cgit v1.2.3


From 886cff213039c034bc78408ea52689514e0c9a69 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Thu, 3 Jan 2019 18:31:04 +0000
Subject: Add a few helper lemmas

---
 lib/isabelle/Sail2_prompt_monad_lemmas.thy | 220 ++++++++++++++++++++++++++---
 1 file changed, 204 insertions(+), 16 deletions(-)

(limited to 'lib')

diff --git a/lib/isabelle/Sail2_prompt_monad_lemmas.thy b/lib/isabelle/Sail2_prompt_monad_lemmas.thy
index 3658296b..1fde3287 100644
--- a/lib/isabelle/Sail2_prompt_monad_lemmas.thy
+++ b/lib/isabelle/Sail2_prompt_monad_lemmas.thy
@@ -44,6 +44,9 @@ inductive_set T :: "(('rv, 'a, 'e) monad \<times> 'rv event \<times> ('rv, 'a, '
 | 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"
 | Step: "\<lbrakk>(s, e, s'') \<in> T; (s'', t, s') \<in> Traces\<rbrakk> \<Longrightarrow> (s, e # t, s') \<in> Traces"
@@ -58,6 +61,12 @@ 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"
@@ -91,10 +100,29 @@ 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
@@ -107,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"
@@ -145,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"
-- 
cgit v1.2.3


From 05e6058795e71cf1543e282752cbf95e471894cc Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Thu, 10 Jan 2019 17:10:19 +0000
Subject: Fixes so 8.5 with vector instructions compiles to C

---
 lib/smt.sail | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/smt.sail b/lib/smt.sail
index c57f7bd1..680898a3 100644
--- a/lib/smt.sail
+++ b/lib/smt.sail
@@ -9,7 +9,7 @@ val div = {
   lem: "integerDiv",
   c: "tdiv_int",
   coq: "div_with_eq"
-} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o == div('n, 'm). atom('o)}
+} : forall 'n 'm. (atom('n), atom('m)) -> atom(div('n, 'm)) // {'o, 'o == div('n, 'm). atom('o)}
 
 overload operator / = {div}
 
-- 
cgit v1.2.3


From 9fffbae81148b2e4c65017d79fde20102c19a3b5 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 24 Jan 2019 14:57:28 +0000
Subject: Start supporting informative bool types in Coq backend

---
 lib/coq/Sail2_values.v | 53 ++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 53 insertions(+)

(limited to 'lib')

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.
 
-- 
cgit v1.2.3


From 0b3273e99772d426b8f9843228cf295d7716eea0 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Tue, 29 Jan 2019 17:10:32 +0000
Subject: Add a few more type annotations after mono rewrites

---
 lib/mono_rewrites.sail | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail
index 93ad3db5..8259ec47 100644
--- a/lib/mono_rewrites.sail
+++ b/lib/mono_rewrites.sail
@@ -63,7 +63,7 @@ function slice_slice_concat (xs, i, l, ys, i', l') = {
   extzv(xs) << l' | extzv(ys)
 }
 
-val slice_zeros_concat : forall 'n 'p 'q 'r, 'r == 'p + 'q & 'n >= 0 & 'p >= 0 & 'q >= 0 & 'r >= 0.
+val slice_zeros_concat : forall 'n 'p 'q 'r, 'r == 'p + 'q & 'n >= 0 & /*'p >= 0 & 'q >= 0 &*/ 'r >= 0.
   (bits('n), int, atom('p), atom('q)) -> bits('r) effect pure
 
 function slice_zeros_concat (xs, i, l, l') = {
-- 
cgit v1.2.3


From cca2016b7a339da00fcf8ffdf8e5e758234a0234 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Tue, 29 Jan 2019 19:24:11 +0000
Subject: Fixes for full v8.5

---
 lib/arith.sail | 6 +++++-
 lib/sail.c     | 8 +++++---
 lib/sail.h     | 1 +
 3 files changed, 11 insertions(+), 4 deletions(-)

(limited to 'lib')

diff --git a/lib/arith.sail b/lib/arith.sail
index a3a80fc5..b233048e 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 *****
 
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 53b9c6be..4225a3d4 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);
 
-- 
cgit v1.2.3


From 6070a0775d61a1551b8e2c1ca2ff7e39f2ba32f4 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Thu, 31 Jan 2019 14:41:47 +0000
Subject: Adapt HOL library to monad changes

---
 lib/hol/sail2_prompt_monad.lem | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'lib')

diff --git a/lib/hol/sail2_prompt_monad.lem b/lib/hol/sail2_prompt_monad.lem
index 3af931a5..5f0f7478 100644
--- a/lib/hol/sail2_prompt_monad.lem
+++ b/lib/hol/sail2_prompt_monad.lem
@@ -34,16 +34,17 @@ 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 inline assert_exp = assert_expS
-- 
cgit v1.2.3


From ccc11a48d38f634f98853fe940d1d484bb7b7fe8 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Thu, 31 Jan 2019 14:42:29 +0000
Subject: Build Isabelle heap image instead of just running session

---
 lib/isabelle/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib')

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
-- 
cgit v1.2.3


From 84d30fd9dee6dd4f22a58b55f93ca39d30266c4f Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Mon, 4 Feb 2019 21:30:33 +0000
Subject: Fix some warnings

---
 lib/elf.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/elf.c b/lib/elf.c
index 888169f5..397c8f3f 100644
--- a/lib/elf.c
+++ b/lib/elf.c
@@ -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 %llu\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);
         }
-- 
cgit v1.2.3


From 0f736fcb7fd46d902dffa171d1458253b2070b79 Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Wed, 6 Feb 2019 03:20:03 +0000
Subject: Remove all sizeof rewriting from C compilation

All sizeof expressions now removed by the type-checker, so it's now
properly a type error if they cannot be removed rather than a bizarre
re-write error. This also greatly improves compilation speed overall, at
the expense of the first type-checking pass.
---
 lib/smt.sail | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'lib')

diff --git a/lib/smt.sail b/lib/smt.sail
index e73897b1..6a5a1327 100644
--- a/lib/smt.sail
+++ b/lib/smt.sail
@@ -19,7 +19,7 @@ val mod = {
   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. (atom('n), atom('m)) -> atom(mod('n, 'm))
 
 overload operator % = {mod}
 
@@ -29,7 +29,7 @@ val abs_atom = {
   lem: "abs_int",
   c: "abs_int",
   coq: "abs_with_eq"
-} : forall 'n. atom('n) -> {'o, 'o == abs_atom('n). atom('o)}
+} : forall 'n. atom('n) -> atom(abs('n))
 
 $ifdef TEST
 
-- 
cgit v1.2.3


From 55f65f92812a6927d5661c2c25a09051630334b3 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 6 Feb 2019 15:26:32 +0000
Subject: Fix some tests

---
 lib/arith.sail      |  1 +
 lib/flow.sail       | 11 +++++++++++
 lib/smt.sail        | 13 +++++--------
 lib/vector_dec.sail |  2 ++
 4 files changed, 19 insertions(+), 8 deletions(-)

(limited to 'lib')

diff --git a/lib/arith.sail b/lib/arith.sail
index b233048e..8825ac2f 100644
--- a/lib/arith.sail
+++ b/lib/arith.sail
@@ -102,6 +102,7 @@ val abs_int = {
   smt : "abs",
   ocaml: "abs_int",
   lem: "abs_int",
+  c: "abs_int",
   coq: "Z.abs"
 } : (int, int) -> int
 
diff --git a/lib/flow.sail b/lib/flow.sail
index cb77f5b1..e6fe7fc0 100644
--- a/lib/flow.sail
+++ b/lib/flow.sail
@@ -50,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/smt.sail b/lib/smt.sail
index 6a5a1327..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)) -> atom(div('n, '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)) -> atom(mod('n, 'm))
+} : 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) -> atom(abs('n))
+} : 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 4e4bad5a..166db243 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -166,4 +166,6 @@ val signed = {
   _: "sint"
 } : forall 'n, 'n > 0. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1)
 
+overload __size = {length}
+
 $endif
-- 
cgit v1.2.3


From 6fffd6ef54ab33441d08f40f56f27daa9c5b333e Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Thu, 7 Feb 2019 18:59:48 +0000
Subject: Monomorphisation tweaks for v8.5

Various tweaks to the monomorphisation rewrites.  Disable old sizeof
rewriting for Lem backend and rely on the type checker rewriting
implicit arguments.  Also avoid unifying nexps with sums, as this can
easily fail due to commutativity and associativity.
---
 lib/mono_rewrites.sail | 92 ++++++++++++++++++++++++++++++++------------------
 lib/vector_dec.sail    |  2 +-
 2 files changed, 60 insertions(+), 34 deletions(-)

(limited to 'lib')

diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail
index 8259ec47..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/vector_dec.sail b/lib/vector_dec.sail
index 166db243..8c6426d4 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -166,6 +166,6 @@ val signed = {
   _: "sint"
 } : forall 'n, 'n > 0. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1)
 
-overload __size = {length}
+overload __size = {__id, length}
 
 $endif
-- 
cgit v1.2.3


From ad868ef0ad22a78021a5de91073416f69e8163d3 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Fri, 8 Feb 2019 18:04:51 +0000
Subject: Add missing functions to HOL monad wrapper

Also make the rewriter keep failed assertions in output when pruning
blocks.
---
 lib/hol/sail2_prompt.lem       | 3 ++-
 lib/hol/sail2_prompt_monad.lem | 3 +++
 2 files changed, 5 insertions(+), 1 deletion(-)

(limited to 'lib')

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 5f0f7478..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
@@ -46,5 +48,6 @@ 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
-- 
cgit v1.2.3