Re-engineer prompt monad of Lem shallow embedding

- Use simplified monad type (e.g., without the with_aux constructors that are
  not needed by the shallow embedding).
- Add support for registers with arbitrary types (e.g., records, enumerations,
  vectors of vectors). Instead of using bit lists as the common representation
  of register values at the monad interface, use a register_value type that is
  generated per spec as a union of all register types that occur in the spec.
  Conversion functions between register_value and concrete types are generated.
- Use the same representation of register references as the state monad, in
  preparation of rebasing the state monad onto the prompt monad.
- Split out those types from sail_impl_base.lem that are used by the shallow
  embedding into a new module sail_instr_kinds.lem, and import that.  Removing
  the dependency on Sail_impl_base from the shallow embedding avoids name clashes
  between the different monad types.

Not yet done:
- Support for reading/writing register slices.  Currently, a rewriting pass
  pushes register slices in l-expressions to the right-hand side, turning a
  write to a register slice into a read-modify-write.  For interfacing with the
  concurreny model, we will want to be more precise than that (in particular
  since some specs represent register files as big single registers containing a
  vector of bitvectors).
- Lemmas about the conversion functions to/from register_value should be
  generated automatically.

3 files changed, 48 insertions, 133 deletions

diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile
index 84af5d75..50e6d471 100644
--- a/lib/isabelle/Makefile
+++ b/lib/isabelle/Makefile
@@ -1,4 +1,4 @@
-THYS = Sail_impl_base.thy Sail_values.thy Sail_operators.thy \
+THYS = Sail_instr_kinds.thy Sail_values.thy Sail_operators.thy \
   Sail_operators_mwords.thy Sail_operators_bitlists.thy \
   State_monad.thy State.thy Prompt_monad.thy Prompt.thy
 EXTRA_THYS = State_monad_extras.thy Prompt_monad_extras.thy
@@ -14,10 +14,10 @@ heap-img: $(THYS) $(EXTRA_THYS) ROOT
 	@echo '*** and add the isabelle binary to your PATH.'
 	isabelle build -b Sail
 
-Sail_impl_base.thy: ../../src/lem_interp/sail_impl_base.lem
+Sail_instr_kinds.thy: ../../src/lem_interp/sail_instr_kinds.lem
 	lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $<
 
-Sail_values.thy: ../../src/gen_lib/sail_values.lem Sail_impl_base.thy
+Sail_values.thy: ../../src/gen_lib/sail_values.lem Sail_instr_kinds.thy
 	lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $<
 
 Sail_operators.thy: ../../src/gen_lib/sail_operators.lem Sail_values.thy
diff --git a/lib/isabelle/Prompt_monad_extras.thy b/lib/isabelle/Prompt_monad_extras.thy
index 0c319f97..e93c6052 100644
--- a/lib/isabelle/Prompt_monad_extras.thy
+++ b/lib/isabelle/Prompt_monad_extras.thy
@@ -2,60 +2,50 @@ theory Prompt_monad_extras
   imports Prompt_monad
 begin
 
-lemma All_bind_dom: "bind_dom (oc, f)"
-  by (induction oc) (auto intro: bind.domintros; blast intro: bind.domintros)+
+lemma All_bind_dom: "bind_dom (m, f)"
+  by (induction m) (auto intro: bind.domintros)
 
 termination bind using All_bind_dom by auto
+lemmas bind_induct[case_names Done Read_mem Write_memv Read_reg Excl_res Write_ea Barrier Write_reg Fail Error Exception] = bind.induct
 
-lemma bind_induct[case_names Done Read_mem Read_reg Write_memv Excl_res Write_ea Barrier Footprint Write_reg Escape Fail Error Exception Internal]:
-  fixes m :: "('a, 'e) outcome" and f :: "'a \<Rightarrow> ('b, 'e) outcome"
-  assumes "\<And>a f. P (Done a) f"
-    and "\<And>rk addr sz k f. (\<And>v m' opt. (m', opt) = k v \<Longrightarrow> P m' f) \<Longrightarrow> P (Read_mem (rk, addr, sz) k) f"
-    and "\<And>reg k f. (\<And>v m' opt. (m', opt) = k v \<Longrightarrow> P m' f) \<Longrightarrow> P (Read_reg reg k) f"
-    and "\<And>val k f. (\<And>v m' opt. (m', opt) = k v \<Longrightarrow> P m' f) \<Longrightarrow> P (Write_memv val k) f"
-    and "\<And>k f. (\<And>v m' opt. (m', opt) = k v \<Longrightarrow> P m' f) \<Longrightarrow> P (Excl_res k) f"
-    and "\<And>wk addr sz m opt f. P m f \<Longrightarrow> P (Write_ea (wk, addr, sz) (m, opt)) f"
-    and "\<And>bk m opt f. P m f \<Longrightarrow> P (Barrier bk (m, opt)) f"
-    and "\<And>m opt f. P m f \<Longrightarrow> P (Footprint (m, opt)) f"
-    and "\<And>reg val m opt f. P m f \<Longrightarrow> P (Write_reg (reg, val) (m, opt)) f"
-    and "\<And>descr f. P (Escape descr) f"
-    and "\<And>descr f. P (Fail descr) f" and "\<And>descr f. P (Error descr) f" and "\<And>e f. P (Exception e) f"
-    and "\<And>i m opt f. P m f \<Longrightarrow> P (Internal i (m, opt)) f"
-  shows "P m f"
-  by (rule bind.induct[split_format (complete), OF assms]; blast)
-
-datatype event =
+lemma bind_return[simp]: "bind (return a) f = f a"
+  by (auto simp: return_def)
+
+lemma bind_assoc[simp]: "bind (bind m f) g = bind m (\<lambda>x. bind (f x) g)"
+  by (induction m f arbitrary: g rule: bind.induct) auto
+
+lemma All_try_catch_dom: "try_catch_dom (m, h)"
+  by (induction m) (auto intro: try_catch.domintros)
+termination try_catch using All_try_catch_dom by auto
+lemmas try_catch_induct[case_names Done Read_mem Write_memv Read_reg Excl_res Write_ea Barrier Write_reg Fail Error Exception] = try_catch.induct
+
+datatype 'regval event =
   (* Request to read memory *)
-    Read_mem read_kind address_lifted nat memory_value
+    e_read_mem read_kind int int "memory_byte list"
   (* Write is imminent, at address lifted, of size nat *)
-  | Write_ea write_kind address_lifted nat
+  | e_write_ea write_kind int int
   (* Request the result of store-exclusive *)
-  | Excl_res bool
+  | e_excl_res bool
   (* Request to write memory at last signalled address. Memory value should be 8
      times the size given in ea signal *)
-  | Write_memv memory_value bool
+  | e_write_memv "memory_byte list" bool
   (* Request a memory barrier *)
-  | Barrier " barrier_kind "
-  (* Tell the system to dynamically recalculate dependency footprint *)
-  | Footprint
+  | e_barrier " barrier_kind "
   (* Request to read register *)
-  | Read_reg reg_name register_value
+  | e_read_reg string 'regval
   (* Request to write register *)
-  | Write_reg reg_name register_value
-  | Internal " ( string option *  (unit \<Rightarrow> string)option) "
-
-inductive_set T :: "(('a, 'e)outcome \<times> event \<times> ('a, 'e)outcome) set" where
-  Read_mem: "\<exists>opt. k v = (m, opt) \<Longrightarrow> ((outcome.Read_mem (rk, addr, sz) k), Read_mem rk addr sz v, m) \<in> T"
-| Write_ea: "\<exists>opt. k = (m, opt) \<Longrightarrow> ((outcome.Write_ea (rk, addr, sz) k), Write_ea rk addr sz, m) \<in> T"
-| Excl_res: "\<exists>opt. k r = (m, opt) \<Longrightarrow> ((outcome.Excl_res k), Excl_res r, m) \<in> T"
-| Write_memv: "\<exists>opt. k r = (m, opt) \<Longrightarrow> ((outcome.Write_memv v k), Write_memv v r, m) \<in> T"
-| Barrier: "\<exists>opt. k = (m, opt) \<Longrightarrow> ((outcome.Barrier bk k), Barrier bk, m) \<in> T"
-| Footprint: "\<exists>opt. k = (m, opt) \<Longrightarrow> ((outcome.Footprint k), Footprint, m) \<in> T"
-| Read_reg: "\<exists>opt. k v = (m, opt) \<Longrightarrow> ((outcome.Read_reg r k), Read_reg r v, m) \<in> T"
-| Write_reg: "\<exists>opt. k = (m, opt) \<Longrightarrow> ((outcome.Write_reg (r, v) k), Write_reg r v, m) \<in> T"
-| Internal: "\<exists>opt. k = (m, opt) \<Longrightarrow> ((outcome.Internal descr k), Internal descr, m) \<in> T"
-
-inductive_set Traces :: "(('a, 'r)outcome \<times> event list \<times> ('a, 'r)outcome) set" where
+  | e_write_reg string 'regval
+
+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"
+| 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"
+| 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"
+
+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"
 
@@ -63,15 +53,13 @@ declare Traces.intros[intro]
 declare T.intros[intro]
 
 declare prod.splits[split]
-(* lemma fst_case_bind[simp]: "fst (case k of (o1, x) \<Rightarrow> (bind o1 f, x)) = bind (fst k) f"
-  by (cases k) auto *)
 
 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"
 
-abbreviation Run :: "('a, 'r)outcome \<Rightarrow> event list \<Rightarrow> 'a \<Rightarrow> bool"
+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:
@@ -84,60 +72,21 @@ proof (use assms in \<open>induction t1 arbitrary: s\<close>)
 qed auto
 
 lemma bind_DoneE:
-  assumes "bind m f = outcome.Done a"
-  obtains a' where "m = outcome.Done a'" and "f a' = outcome.Done a"
+  assumes "bind m f = Done a"
+  obtains a' where "m = Done a'" and "f a' = Done a"
   using assms by (auto elim: bind.elims)
 
 lemma bind_T_cases:
   assumes "(bind m f, e, s') \<in> T"
   obtains (Done) a where "m = Done a"
   | (Bind) m' where "s' = bind m' f" and "(m, e, m') \<in> T"
-proof cases
-  assume D: "\<forall>a. m \<noteq> Done a"
-  show thesis using assms proof cases
-    case (Read_mem k v rk addr sz)
-    then obtain k' where "m = outcome.Read_mem (rk, addr, sz) k'" using D by (cases m) auto
-    then show ?thesis using Read_mem by (intro Bind[of "fst (k' v)"]) auto
-  next
-    case (Write_ea k rk addr sz)
-    then obtain k' where "m = outcome.Write_ea (rk, addr, sz) k'" using D by (cases m) auto
-    then show ?thesis using Write_ea by (intro Bind[of "fst k'"]) auto
-  next
-    case (Excl_res k r)
-    then obtain k' where "m = outcome.Excl_res k'" using D by (cases m) auto
-    then show ?thesis using Excl_res by (intro Bind[of "fst (k' r)"]) auto
-  next
-    case (Write_memv k r v)
-    then obtain k' where "m = outcome.Write_memv v k'" using D by (cases m) auto
-    then show ?thesis using Write_memv by (intro Bind[of "fst (k' r)"]) auto
-  next
-    case (Barrier k bk)
-    then obtain k' where "m = outcome.Barrier bk k'" using D by (cases m) auto
-    then show ?thesis using Barrier by (intro Bind[of "fst k'"]) auto
-  next
-    case (Footprint k)
-    then obtain k' where "m = outcome.Footprint k'" using D by (cases m) auto
-    then show ?thesis using Footprint by (intro Bind[of "fst k'"]) auto
-  next
-    case (Read_reg k v r)
-    then obtain k' where "m = outcome.Read_reg r k'" using D by (cases m) auto
-    then show ?thesis using Read_reg by (intro Bind[of "fst (k' v)"]) (auto split: prod.splits)
-  next
-    case (Write_reg k r v)
-    then obtain k' where "m = outcome.Write_reg (r, v) k'" using D by (cases m) auto
-    then show ?thesis using Write_reg by (intro Bind[of "fst k'"]) auto
-  next
-    case (Internal k descr)
-    then obtain k' where "m = outcome.Internal descr k'" using D by (cases m) auto
-    then show ?thesis using Internal by (intro Bind[of "fst k'"]) auto
-  qed
-qed auto
+  using assms by (cases; blast elim: bind.elims)
 
 lemma Run_bindE:
-  fixes m :: "('b, 'r) outcome" and a :: 'a
+  fixes m :: "('rv, 'b, 'e) monad" and a :: 'a
   assumes "Run (bind m f) t a"
   obtains tm am tf where "t = tm @ tf" and "Run m tm am" and "Run (f am) tf a"
-proof (use assms in \<open>induction "bind m f" t "Done a :: ('a,'r) outcome" arbitrary: m rule: Traces.induct\<close>)
+proof (use assms in \<open>induction "bind m f" t "Done a :: ('rv, 'a, 'e) monad" arbitrary: m rule: Traces.induct\<close>)
   case Nil
   obtain am where "m = Done am" and "f am = Done a" using Nil(1) by (elim bind_DoneE)
   then show ?case by (intro Nil(2)) auto
@@ -166,49 +115,15 @@ lemma Run_Done_iff_Nil[simp]: "Run (Done a) t a' \<longleftrightarrow> t = [] \<
   by (auto elim: Run_DoneE)
 
 lemma Run_BarrierE[elim!]:
-  assumes "Run (outcome.Barrier bk k) t a"
-  obtains t' where "t = Barrier bk # t'" and "Run (fst k) t' a"
+  assumes "Run (Barrier bk k) t a"
+  obtains t' where "t = e_barrier bk # t'" and "Run k t' a"
   using assms by cases (auto elim: T.cases)
 
 lemma bind_cong[fundef_cong]:
   assumes m: "m1 = m2"
     and f: "\<And>t a. Run m2 t a \<Longrightarrow> f1 a = f2 a"
   shows "bind m1 f1 = bind m2 f2"
-proof (unfold m, use f in \<open>induction m2 f1 arbitrary: f2 rule: bind_induct\<close>)
-  case (Read_mem rk addr sz k f)
-  have "bind m' f = bind m' f2" if k: "k v = (m', opt)" for v m' opt
-    using k by (auto intro!: Read_mem.IH[of _ opt v] Read_mem.prems)
-  then show ?case by auto
-next
-  case (Read_reg reg k f)
-  have "bind m' f = bind m' f2" if k: "k v = (m', opt)" for v m' opt
-    using k by (auto intro!: Read_reg.IH[of _ opt v] Read_reg.prems)
-  then show ?case by auto
-next
-  case (Write_memv val k f)
-  have "bind m' f = bind m' f2" if k: "k v = (m', opt)" for v m' opt
-    using k by (auto intro!: Write_memv.IH[of _ opt v] Write_memv.prems)
-  then show ?case by auto
-next
-  case (Excl_res k f)
-  have "bind m' f = bind m' f2" if k: "k v = (m', opt)" for v m' opt
-    using k by (auto intro!: Excl_res.IH[of _ opt v] Excl_res.prems)
-  then show ?case by auto
-next
-  case (Write_ea wk addr sz m opt f)
-  show ?case by (auto intro!: Write_ea)
-next
-  case (Barrier bk m opt f)
-  show ?case by (auto intro!: Barrier)
-next
-  case (Footprint m opt f)
-  show ?case by (auto intro!: Footprint)
-next
-  case (Write_reg reg val m opt f)
-  show ?case by (auto intro!: Write_reg)
-next
-  case (Internal i m opt f)
-  show ?case by (auto intro!: Internal)
-qed auto
+  unfolding m using f
+  by (induction m2 f1 arbitrary: f2 rule: bind.induct; unfold bind.simps; blast)
 
 end
diff --git a/lib/isabelle/State_monad_extras.thy b/lib/isabelle/State_monad_extras.thy
index c9522f58..cf042a02 100644
--- a/lib/isabelle/State_monad_extras.thy
+++ b/lib/isabelle/State_monad_extras.thy
@@ -7,8 +7,8 @@ lemma bind_ext_cong[fundef_cong]:
     and f: "\<And>a s'. (Value a, s') \<in> set (m2 s) \<Longrightarrow> f1 a s' = f2 a s'"
   shows "(bind m1 f1) s = (bind m2 f2) s"
 proof -
-  have "List.concat (map (\<lambda>x. case x of (Value a, s') \<Rightarrow> f1 a s' | (Exception0 e, s') \<Rightarrow> [(Exception0 e, s')]) (m2 s)) =
-        List.concat (map (\<lambda>x. case x of (Value a, s') \<Rightarrow> f2 a s' | (Exception0 e, s') \<Rightarrow> [(Exception0 e, s')]) (m2 s))"
+  have "List.concat (map (\<lambda>x. case x of (Value a, s') \<Rightarrow> f1 a s' | (Exception e, s') \<Rightarrow> [(Exception e, s')]) (m2 s)) =
+        List.concat (map (\<lambda>x. case x of (Value a, s') \<Rightarrow> f2 a s' | (Exception e, s') \<Rightarrow> [(Exception e, s')]) (m2 s))"
     using f by (intro arg_cong[where f = List.concat]) (auto intro: map_ext split: result.splits)
   then show ?thesis using m by (auto simp: bind_def)
 qed