Add address to Write_tag outcome

The state monad currently assumes that tags are written to and read from
properly aligned addresses (since it does not know the capability size used in
the Sail model).  This change allows the Sail model to pass in the aligned
address(es) even if data is written to an unaligned address.  There might be
better ways to model tag writing, but this approach seems rather general.

2 files changed, 4 insertions, 4 deletions

diff --git a/lib/isabelle/Prompt_monad_lemmas.thy b/lib/isabelle/Prompt_monad_lemmas.thy
index 2f2d43ef..56aa6e87 100644
--- a/lib/isabelle/Prompt_monad_lemmas.thy
+++ b/lib/isabelle/Prompt_monad_lemmas.thy
@@ -32,7 +32,7 @@ datatype 'regval event =
   (* Request to write memory at last signalled address. Memory value should be 8
      times the size given in ea signal *)
   | e_write_memv "memory_byte list" bool
-  | e_write_tagv bitU bool
+  | e_write_tag "bitU list" bitU bool
   (* Tell the system to dynamically recalculate dependency footprint *)
   | e_footprint
   (* Request a memory barrier *)
@@ -50,7 +50,7 @@ inductive_set T :: "(('rv, 'a, 'e) monad \<times> 'rv event \<times> ('rv, 'a, '
 | Write_ea: "((Write_ea wk addr sz k), e_write_ea wk addr sz, k) \<in> T"
 | Excl_res: "((Excl_res k), e_excl_res r, k r) \<in> T"
 | Write_memv: "((Write_memv v k), e_write_memv v r, k r) \<in> T"
-| Write_tagv: "((Write_tagv v k), e_write_tagv v r, k r) \<in> T"
+| 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"
@@ -79,7 +79,7 @@ lemma Traces_cases:
   | (Read_mem) rk addr s k t' v where "m = Read_mem rk addr s k" and "t = e_read_mem rk addr s v # t'" and "(k v, t', m') \<in> Traces"
   | (Read_tag) addr k t' v where "m = Read_tag addr k" and "t = e_read_tag addr v # t'" and "(k v, t', m') \<in> Traces"
   | (Write_memv) val k t' v where "m = Write_memv val k" and "t = e_write_memv val v # t'" and "(k v, t', m') \<in> Traces"
-  | (Write_tagv) val k t' v where "m = Write_tagv val k" and "t = e_write_tagv val v # t'" and "(k v, t', m') \<in> Traces"
+  | (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"
diff --git a/lib/isabelle/State_monad_lemmas.thy b/lib/isabelle/State_monad_lemmas.thy
index 746fd315..291157f5 100644
--- a/lib/isabelle/State_monad_lemmas.thy
+++ b/lib/isabelle/State_monad_lemmas.thy
@@ -274,7 +274,7 @@ lemma no_throw_mem_builtins:
   "\<And>BC wk a sz s. ignore_throw (write_mem_eaS BC wk a sz) s = write_mem_eaS BC wk a sz s"
   "\<And>v s. ignore_throw (write_mem_bytesS v) s = write_mem_bytesS v s"
   "\<And>BC v s. ignore_throw (write_mem_valS BC v) s = write_mem_valS BC v s"
-  "\<And>t s. ignore_throw (write_tagS t) s = write_tagS t s"
+  "\<And>BC a t s. ignore_throw (write_tagS BC a t) s = write_tagS BC a 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