diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/isabelle/Sail2_prompt_monad_lemmas.thy | 2 | ||||
| -rw-r--r-- | lib/isabelle/Sail2_state_lemmas.thy | 13 | ||||
| -rw-r--r-- | lib/isabelle/Sail2_state_monad_lemmas.thy | 10 |
3 files changed, 17 insertions, 8 deletions
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 |