adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

arm-hyp refine: update for asidHighBits change

This commit is contained in:
Rafal Kolanski 2017-04-06 06:51:24 +10:00 committed by Alejandro Gomez-Londono
parent f5d073cb62
commit a8b7b7887d
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
proof/refine/ARM_HYP/Arch_R.thy
View File

@ -512,7 +512,7 @@ declare check_vp_alignment_inv[wp del]
lemma select_ext_fa:
"free_asid_select asid_tbl \<in> S
\<Longrightarrow> ((select_ext (\<lambda>_. free_asid_select asid_tbl) S) :: (6 word) det_ext_monad)
\<Longrightarrow> ((select_ext (\<lambda>_. free_asid_select asid_tbl) S) :: (7 word) det_ext_monad)
= return (free_asid_select asid_tbl)"
by (simp add: select_ext_def get_def gets_def bind_def assert_def return_def fail_def)
@ -1037,7 +1037,7 @@ shows
apply (rule corres_whenE)
apply (subst assocs_empty_dom_comp [symmetric])
apply (simp add: o_def)
apply (rule dom_ucast_eq_6)
apply (rule dom_ucast_eq_7)
apply (rule corres_trivial, simp, simp)
apply (simp split del: if_split)
apply (rule_tac F="- dom (asidTable \<circ> ucast) \<inter> {x. x \<le> 2 ^ asid_high_bits - 1} \<noteq> {}" in corres_gen_asm)