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

x64 refine: RAB_FN (needed for x64 crefine)

This commit is contained in:
Gerwin Klein 2018-03-10 15:36:50 +11:00 committed by Joel Beeren
parent 1e73cba198
commit 99f2868803
1 changed files with 2 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
proof/refine/X64/RAB_FN.thy
View File

@ -33,7 +33,7 @@ abbreviation (input)
function
resolveAddressBitsFn ::
"capability \<Rightarrow> cptr \<Rightarrow> nat \<Rightarrow> (word32 \<Rightarrow> capability option)
"capability \<Rightarrow> cptr \<Rightarrow> nat \<Rightarrow> (machine_word \<Rightarrow> capability option)
\<Rightarrow> (lookup_failure + (machine_word * nat))"
where
"resolveAddressBitsFn a b c =
@ -92,8 +92,6 @@ lemma resolveAddressBitsFn_eq:
(is "monadic_rewrite F E (?P cap) (?f cap bits) (?g cap capptr bits)")
proof (induct cap capptr bits rule: resolveAddressBits.induct)
case (1 cap cref depth)
note resolveAddressBits.simps[simp del] resolveAddressBitsFn.simps[simp del]
show ?case
apply (subst resolveAddressBits.simps, subst resolveAddressBitsFn.simps)
apply (simp only: Let_def haskell_assertE_def K_bind_def)
@ -142,7 +140,7 @@ proof (induct cap capptr bits rule: resolveAddressBits.induct)
apply (clarsimp simp: isCap_simps)
apply (frule(1) cte_wp_at_valid_objs_valid_cap')
apply (clarsimp simp: cte_level_bits_def valid_cap_simps'
real_cte_at' isCap_simps)
real_cte_at' isCap_simps cteSizeBits_def objBits_simps)
apply (clarsimp simp: cte_wp_at_ctes_of only_cnode_caps_def ball_Un
cnode_caps_gsCNodes_def ran_map_option o_def)
apply (drule bspec, rule IntI, erule ranI, simp add: isCap_simps)