Add support for undefined bit oracle to Lem shallow embedding

Add an Undefined outcome to the prompt monad that asks the environment for a
Boolean value.  For the state monad, add fields for a random generator and a
seed (currently of type nat) to the state.

3 files changed, 9 insertions, 2 deletions

diff --git a/lib/isabelle/Prompt_monad_lemmas.thy b/lib/isabelle/Prompt_monad_lemmas.thy
index d2466764..ffed5afb 100644
--- a/lib/isabelle/Prompt_monad_lemmas.thy
+++ b/lib/isabelle/Prompt_monad_lemmas.thy
@@ -41,6 +41,7 @@ datatype 'regval event =
   | e_read_reg string 'regval
   (* Request to write register *)
   | e_write_reg string 'regval
+  | e_undefined bool
 
 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"
@@ -53,6 +54,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"
 
 inductive_set Traces :: "(('rv, 'a, 'e) monad \<times> 'rv event list \<times> ('rv, 'a, 'e) monad) set" where
   Nil: "(s, [], s) \<in> Traces"
@@ -82,6 +84,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) v k t' where "m = Undefined k" and "t = e_undefined v # t'" and "(k v, 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))
diff --git a/lib/isabelle/State_lemmas.thy b/lib/isabelle/State_lemmas.thy
index e230bd37..9c5dd8af 100644
--- a/lib/isabelle/State_lemmas.thy
+++ b/lib/isabelle/State_lemmas.thy
@@ -25,6 +25,7 @@ lemma liftState_exit[simp]: "liftState r (exit0 ()) = exitS ()" by (auto simp: e
 lemma liftState_exclResult[simp]: "liftState r (excl_result ()) = excl_resultS ()" by (auto simp: excl_result_def)
 lemma liftState_barrier[simp]: "liftState r (barrier bk) = returnS ()" by (auto simp: barrier_def)
 lemma liftState_footprint[simp]: "liftState r (footprint ()) = returnS ()" by (auto simp: footprint_def)
+lemma liftState_undefined[simp]: "liftState r (undefined_bool ()) = undefined_boolS ()" by (auto simp: undefined_bool_def)
 
 lemma liftState_try_catch[simp]:
   "liftState r (try_catch m h) = try_catchS (liftState r m) (liftState r \<circ> h)"
diff --git a/lib/isabelle/State_monad_lemmas.thy b/lib/isabelle/State_monad_lemmas.thy
index fe827c66..d8730421 100644
--- a/lib/isabelle/State_monad_lemmas.thy
+++ b/lib/isabelle/State_monad_lemmas.thy
@@ -126,8 +126,11 @@ lemma no_throw_mem_builtins:
   "\<And>BC v s. ignore_throw (write_mem_valS BC v) s = write_mem_valS BC v s"
   "\<And>t s. ignore_throw (write_tagS t) s = write_tagS t s"
   "\<And>s. ignore_throw (excl_resultS ()) s = excl_resultS () s"
-  unfolding read_mem_bytesS_def read_memS_def read_tagS_def write_mem_eaS_def write_mem_valS_def write_mem_bytesS_def write_tagS_def excl_resultS_def
-  by (auto simp: bindS_def chooseS_def Let_def split: option.splits)+
+  "\<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
+  by (auto simp: bindS_def chooseS_def Let_def split: option.splits prod.splits)+
 
 lemma no_throw_read_memS: "ignore_throw (read_memS BCa BCb rk a sz) s = read_memS BCa BCb rk a sz s"
   by (auto simp: read_memS_def no_throw_mem_builtins cong: bindS_cong)