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

x64: refine: cleanup after ioportcontrol

This commit is contained in:
Joel Beeren 2018-04-23 05:01:57 +10:00
parent d4b830738f
commit 8cb2744306
2 changed files with 1 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
proof/refine/X64/CSpace_I.thy
View File

@ -788,18 +788,6 @@ lemma capUntypedSize_capBits:
apply fastforce
done
definition
"portSubRange r r' \<equiv>
case (r, r') of
(Some (f, l), Some (f', l')) \<Rightarrow> f \<le> f' \<and> l' \<le> l
| _ \<Rightarrow> False"
lemmas portRange_defs = portSubRange_def portRange_def
lemma portSubRange_eq [simp]:
"portSubRange (portRange cap) (portRange cap) = isArchIOPortCap cap"
by (auto simp: portRange_defs isCap_simps
split: capability.splits arch_capability.splits)
lemma sameRegionAs_def2:
"sameRegionAs cap cap' = (\<lambda>cap cap'.
(cap = cap'

2
proof/refine/X64/VSpace_R.thy
View File

@ -1885,7 +1885,7 @@ lemma dmo_writeCR3_invs_no_cicd'[wp]:
done
lemma valid_ioports_cr3_update[elim!]:
"valid_ioports' s \<Longrightarrow> valid_ioports' (s\<lparr>ksArchState := x64KSCurrentCR3_update (\<lambda>_. c) (ksArchState s)\<rparr>)"
"valid_ioports' s \<Longrightarrow> valid_ioports' (s\<lparr>ksArchState := x64KSCurrentUserCR3_update (\<lambda>_. c) (ksArchState s)\<rparr>)"
by (clarsimp simp: valid_ioports'_simps)
lemma setCurrentUserCR3_invs' [wp]: