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

arm-hyp refine: repair for rebase (new corres) 

- fixes the fallout from the updated corres method.
- also includes some fixes by: Daniel Matichuk <daniel.matichuk@data61.csiro.au>
This commit is contained in:
Miki Tanaka 2017-04-05 14:38:44 +10:00 committed by Alejandro Gomez-Londono
parent 776408a2e9
commit fc74a6440f
11 changed files with 457 additions and 546 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

426
proof/refine/ARM_HYP/ArchAcc_R.thy
View File

@ -16,6 +16,25 @@ theory ArchAcc_R
imports SubMonad_R
begin
(*FIXME move*)
lemma hoare_add_post':
"\<lbrakk>\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>; \<lbrace>P''\<rbrace> f \<lbrace>\<lambda>rv s. Q' rv s \<longrightarrow> Q rv s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P' and P''\<rbrace> f \<lbrace>Q\<rbrace>"
by (fastforce simp add: valid_def)
context begin
lemma fun_all: "f = f' \<Longrightarrow> (\<forall>s. f s \<longrightarrow> f' s)"
by simp
lemma distrib_imp:
"P \<longrightarrow> Q \<and> Q' \<Longrightarrow> ((P \<longrightarrow> Q) \<Longrightarrow> (P \<longrightarrow> Q') \<Longrightarrow> R) \<Longrightarrow> R"
by simp
method def_to_elim = (drule meta_eq_to_obj_eq, drule fun_all, elim allE, elim distrib_imp)
method simp_to_elim = (drule fun_all, elim allE impE)
end
context Arch begin global_naming ARM_A (*FIXME: arch_split*)
lemma asid_pool_at_ko:
@ -26,22 +45,66 @@ lemma asid_pool_at_ko:
apply (case_tac arch_kernel_obj, auto split: if_split_asm)
done
declare valid_arch_state_def[@def_to_elim, conjuncts]
lemmas valid_arch_state_elims[rule_format, elim!] = conjuncts
lemmas valid_arch_obj_elims[rule_format, elim!] =
valid_arch_obj.simps[@simp_to_elim, @ \<open>(drule bspec)?\<close>]
lemmas valid_vspace_obj_elims[rule_format, elim!] =
valid_vspace_obj.simps[@simp_to_elim, @ \<open>(drule bspec)?\<close>]
end
context begin interpretation Arch . (*FIXME: arch_split*)
(*FIXME move *)
lemma pspace_relation_None:
"\<lbrakk>pspace_relation p p'; p' ptr = None \<rbrakk> \<Longrightarrow> p ptr = None"
apply (rule not_Some_eq[THEN iffD1, OF allI, OF notI])
apply (drule(1) pspace_relation_absD)
apply (case_tac y; clarsimp simp: cte_map_def of_bl_def well_formed_cnode_n_def split: if_splits)
subgoal for n
apply (drule spec[of _ ptr])
apply (drule spec)
apply clarsimp
apply (drule spec[of _ "replicate n False"])
apply (drule mp[OF _ refl])
apply (drule mp)
subgoal premises by (induct n; simp)
apply clarsimp
done
subgoal for x
apply (cases x; clarsimp)
apply ((drule spec[of _ 0], fastforce)+)[2]
apply (drule spec[of _ ptr])
apply (drule spec)
apply clarsimp
apply (drule mp[OF _ refl])
apply (drule spec[of _ 0])
subgoal for _ sz by (cases sz; simp add: pageBits_def)
done
done
lemma no_0_obj'_abstract:
"(s, s') \<in> state_relation \<Longrightarrow> no_0_obj' s' \<Longrightarrow> kheap s 0 = None"
by (auto intro: pspace_relation_None simp add: no_0_obj'_def)
declare if_cong[cong]
lemma corres_gets_asid:
lemma corres_gets_asid [corres]:
"corres (\<lambda>a c. a = c o ucast) \<top> \<top> (gets (arm_asid_table \<circ> arch_state)) (gets (armKSASIDTable \<circ> ksArchState))"
by (simp add: state_relation_def arch_state_relation_def)
lemmas arm_asid_table_related = corres_gets_asid[simplified, rule_format]
lemma asid_low_bits [simp]:
"asidLowBits = asid_low_bits"
by (simp add: asid_low_bits_def asidLowBits_def)
lemma get_asid_pool_corres:
lemma get_asid_pool_corres [corres]:
"corres (\<lambda>p p'. p = inv ASIDPool p' o ucast)
(asid_pool_at p) (asid_pool_at' p)
(get_asid_pool p) (getObject p)"
@ -175,51 +238,23 @@ lemma storePTE_state_hyp_refs_of[wp]:
crunch cte_wp_at'[wp]: setIRQState "\<lambda>s. P (cte_wp_at' P' p s)"
crunch inv[wp]: getIRQSlot "P"
lemma set_asid_pool_corres:
lemma set_asid_pool_corres [corres]:
"a = inv ASIDPool a' o ucast \<Longrightarrow>
corres dc (asid_pool_at p and valid_etcbs) (asid_pool_at' p)
(set_asid_pool p a) (setObject p a')"
apply (simp add: set_asid_pool_def)
apply (rule corres_symb_exec_l)
apply (rule corres_symb_exec_l)
apply (rule corres_guard_imp)
apply (rule set_other_obj_corres [where P="\<lambda>ko::asidpool. True"])
apply simp
apply (clarsimp simp: obj_at'_def projectKOs)
apply (erule map_to_ctes_upd_other, simp, simp)
apply (simp add: a_type_def is_other_obj_relation_type_def)
apply (simp add: objBits_simps archObjSize_def)
apply simp
apply (simp add: objBits_simps archObjSize_def pageBits_def)
apply (simp add: other_obj_relation_def asid_pool_relation_def)
apply assumption
apply (simp add: typ_at'_def obj_at'_def ko_wp_at'_def projectKOs)
apply clarsimp
apply (case_tac ko; simp)
apply (rename_tac arch_kernel_object)
apply (case_tac arch_kernel_object; simp)
prefer 5
apply (rule get_object_sp)
apply (clarsimp simp: obj_at_def exs_valid_def assert_def a_type_def return_def fail_def)
apply (auto split: Structures_A.kernel_object.split_asm arch_kernel_obj.split_asm if_split_asm)[1]
apply wp
apply (clarsimp simp: obj_at_def a_type_def)
apply (auto split: Structures_A.kernel_object.split_asm arch_kernel_obj.split_asm if_split_asm)[1]
apply (rule no_fail_pre, wp)
apply (clarsimp simp: simp: obj_at_def a_type_def)
apply (auto split: Structures_A.kernel_object.splits arch_kernel_obj.splits if_split_asm)[1]
apply (clarsimp simp: obj_at_def exs_valid_def get_object_def exec_gets)
apply (simp add: return_def)
apply (rule no_fail_pre, wp)
apply (clarsimp simp add: obj_at_def)
done
apply (corressimp search: set_other_obj_corres[where P="\<lambda>_. True"]
wp: get_object_ret get_object_wp)
apply (simp add: other_obj_relation_def asid_pool_relation_def)
apply (clarsimp simp: obj_at_simps )
by (auto simp: obj_at_simps typ_at_to_obj_at_arches
split: Structures_A.kernel_object.splits if_splits arch_kernel_obj.splits)
lemma set_asid_pool_corres':
"a = inv ASIDPool a' o ucast \<Longrightarrow>
corres dc (asid_pool_at p and valid_etcbs) (pspace_aligned' and pspace_distinct')
(set_asid_pool p a) (setObject p a')"
apply (rule stronger_corres_guard_imp,
erule set_asid_pool_corres)
apply (rule stronger_corres_guard_imp[OF set_asid_pool_corres])
apply auto
done
@ -230,7 +265,7 @@ lemma pde_relation_aligned_simp:
by (clarsimp simp: pde_relation_aligned_def pde_bits_def
split: ARM_HYP_H.pde.splits if_splits)
lemma get_pde_corres:
lemma get_pde_corres [corres]:
"corres (pde_relation_aligned (p >> pde_bits)) (pde_at p) (pde_at' p)
(get_pde p) (getObject p)"
apply (simp add: getObject_def get_pde_def get_pd_def get_object_def split_def bind_assoc)
@ -327,7 +362,7 @@ lemma pde_at_ksPSpace_not_None:
apply (clarsimp simp:typ_at'_def ko_wp_at'_def)
done
lemma get_master_pde_corres:
lemma get_master_pde_corres [corres]:
"corres pde_relation' (pde_at p)
(pde_at' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and
pspace_aligned' and pspace_distinct')
@ -512,7 +547,7 @@ lemma pte_relation_aligned_simp:
by (clarsimp simp: pte_relation_aligned_def pte_bits_def
split: ARM_HYP_H.pte.splits if_splits)
lemma get_pte_corres:
lemma get_pte_corres [corres]:
"corres (pte_relation_aligned (p >> pte_bits)) (pte_at p) (pte_at' p)
(get_pte p) (getObject p)"
apply (simp add: getObject_def get_pte_def get_pt_def get_object_def split_def bind_assoc)
@ -607,7 +642,7 @@ lemma pte_at_ksPSpace_not_None:
apply (clarsimp simp:typ_at'_def ko_wp_at'_def)
done
lemma get_master_pte_corres:
lemma get_master_pte_corres [corres]:
"corres pte_relation' (pte_at p)
(pte_at' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and
pspace_aligned' and pspace_distinct')
@ -776,7 +811,7 @@ lemma pt_slot_eq:
done
-- "set_other_obj_corres unfortunately doesn't work here"
lemma set_pd_corres:
lemma set_pd_corres [corres]:
"pde_relation_aligned (p>>pde_bits) pde pde' \<Longrightarrow>
corres dc (ko_at (ArchObj (PageDirectory pd)) (p && ~~ mask pd_bits)
and pspace_aligned and valid_etcbs)
@ -856,7 +891,7 @@ lemma set_pd_corres:
apply (simp add: caps_of_state_after_update obj_at_def swp_cte_at_caps_of)
done
lemma set_pt_corres:
lemma set_pt_corres [corres]:
"pte_relation_aligned (p >> pte_bits) pte pte' \<Longrightarrow>
corres dc (ko_at (ArchObj (PageTable pt)) (p && ~~ mask pt_bits)
and pspace_aligned and valid_etcbs)
@ -936,7 +971,7 @@ lemma set_pt_corres:
lemma wordsFromPDEis2: "\<exists>a b . wordsFromPDE pde = [a , b]"
by (cases pde ; clarsimp simp: wordsFromPDE_def tailM_def headM_def)
lemma store_pde_corres:
lemma store_pde_corres [corres]:
"pde_relation_aligned (p >> pde_bits) pde pde' \<Longrightarrow>
corres dc (pde_at p and pspace_aligned and valid_etcbs) (pde_at' p) (store_pde p pde) (storePDE p pde')"
apply (simp add: store_pde_def storePDE_def)
@ -961,15 +996,14 @@ lemma store_pde_corres':
corres dc
(pde_at p and pspace_aligned and valid_etcbs) (pspace_aligned' and pspace_distinct')
(store_pde p pde) (storePDE p pde')"
apply (rule stronger_corres_guard_imp,
erule store_pde_corres)
apply (rule stronger_corres_guard_imp, rule store_pde_corres)
apply auto
done
lemma wordsFromPTEis2: "\<exists>a b . wordsFromPTE pte = [a , b]"
by (cases pte ; clarsimp simp: wordsFromPTE_def tailM_def headM_def)
lemma store_pte_corres:
lemma store_pte_corres [corres]:
"pte_relation_aligned (p>>pte_bits) pte pte' \<Longrightarrow>
corres dc (pte_at p and pspace_aligned and valid_etcbs) (pte_at' p) (store_pte p pte) (storePTE p pte')"
apply (simp add: store_pte_def storePTE_def)
@ -994,8 +1028,7 @@ lemma store_pte_corres':
corres dc (pte_at p and pspace_aligned and valid_etcbs)
(pspace_aligned' and pspace_distinct')
(store_pte p pte) (storePTE p pte')"
apply (rule stronger_corres_guard_imp,
erule store_pte_corres)
apply (rule stronger_corres_guard_imp, rule store_pte_corres)
apply auto
done
@ -1003,15 +1036,6 @@ lemma lookup_pd_slot_corres [simp]:
"lookupPDSlot pd vptr = lookup_pd_slot pd vptr"
by (simp add: lookupPDSlot_def lookup_pd_slot_def)
lemma corres_name_pre:
"\<lbrakk> \<And>s s'. \<lbrakk> P s; P' s'; (s, s') \<in> state_relation \<rbrakk>
\<Longrightarrow> corres rvr (op = s) (op = s') f g \<rbrakk>
\<Longrightarrow> corres rvr P P' f g"
apply (simp add: corres_underlying_def split_def
Ball_def)
apply blast
done
defs checkPDAt_def:
"checkPDAt pd \<equiv> stateAssert (page_directory_at' pd) []"
@ -1119,29 +1143,30 @@ lemma getPTE_wp:
projectKOs in_monad valid_def obj_at'_def objBits_simps)
lemma lookup_pt_slot_corres:
lemmas get_pde_wp_valid = hoare_add_post'[OF get_pde_valid get_pde_wp]
lemma page_table_at_lift:
"\<forall>s s'. (s, s') \<in> state_relation \<longrightarrow>
(pspace_aligned s \<and> valid_pde (ARM_A.PageTablePDE ptr) s \<and> (ptrFromPAddr ptr) = ptr') \<longrightarrow>
pspace_distinct' s' \<longrightarrow> page_table_at' ptr' s'"
by (fastforce intro!: page_table_at_state_relation)
lemmas checkPTAt_corres [corresK] =
corres_stateAssert_implied_frame[OF page_table_at_lift, folded checkPTAt_def]
lemma lookup_pt_slot_corres [corres]:
"corres (lfr \<oplus> op =)
(pde_at (lookup_pd_slot pd vptr) and pspace_aligned and valid_vspace_objs
and (\<exists>\<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) and
K (is_aligned pd pd_bits \<and> vptr < kernel_base))
(pspace_aligned' and pspace_distinct')
(lookup_pt_slot pd vptr) (lookupPTSlot pd vptr)"
apply (simp add: lookup_pt_slot_def lookupPTSlot_def)
apply (rule corres_initial_splitE [where Q'="\<lambda>_. pspace_distinct'" and Q = "\<lambda>r. valid_pde r and pspace_aligned"])
apply (rule corres_guard_imp)
apply (simp,rule get_pde_corres')
apply simp
apply simp
apply (case_tac rv, simp_all add: lookup_failure_map_def lookupPTSlotFromPT_def
pde_relation_aligned_def
split: ARM_HYP_H.pde.splits)[1]
apply (simp add: returnOk_liftE checkPTAt_def)
apply (rule corres_stateAssert_implied[where P=\<top>, simplified])
apply simp
apply clarsimp
apply (rule page_table_at_state_relation)
apply (wp getPDE_wp | simp add: vspace_bits_defs valid_arch_imp_valid_vspace_objs)+
done
unfolding lookup_pt_slot_def lookupPTSlot_def lookupPTSlotFromPT_def
apply (corressimp simp: pde_relation_aligned_def lookup_failure_map_def
wp: get_pde_wp_valid getPDE_wp)
by (auto simp: lookup_failure_map_def obj_at_def)
declare in_set_zip_refl[simp]
@ -1183,7 +1208,12 @@ lemma align_entry_add_cong:
apply auto
done
lemma copy_global_mappings_corres:
lemma armhyp_global_pd_corres [corres]:
"corres op = (\<lambda>_. True) (\<lambda>_. True)
(gets (arm_us_global_pd \<circ> arch_state)) (gets (armUSGlobalPD \<circ> ksArchState))"
by (clarsimp simp: state_relation_def arch_state_relation_def)
lemma copy_global_mappings_corres [corres]:
"corres dc (page_directory_at pd and pspace_aligned and valid_arch_state and valid_etcbs)
(page_directory_at' pd and valid_arch_state')
(copy_global_mappings pd) (copyGlobalMappings pd)"
@ -1223,7 +1253,7 @@ lemma arch_deriveCap_valid:
capUntypedPtr_def ARM_HYP_H.capUntypedPtr_def)
done
lemma arch_derive_corres:
lemma arch_derive_corres [corres]:
"cap_relation (cap.ArchObjectCap c) (ArchObjectCap c') \<Longrightarrow>
corres (ser \<oplus> (\<lambda>c c'. cap_relation (cap.ArchObjectCap c) (ArchObjectCap c')))
\<top> \<top>
@ -1243,7 +1273,7 @@ definition
where
"mapping_map \<equiv> pte_relation' \<otimes> (op =) \<oplus> pde_relation' \<otimes> (op =)"
lemma create_mapping_entries_corres:
lemma create_mapping_entries_corres [corres]:
"\<lbrakk> vm_rights' = vmrights_map vm_rights;
attrib' = vmattributes_map attrib \<rbrakk>
\<Longrightarrow> corres (ser \<oplus> mapping_map)
@ -1253,31 +1283,8 @@ lemma create_mapping_entries_corres:
(pspace_aligned' and pspace_distinct')
(create_mapping_entries base vptr pgsz vm_rights attrib pd)
(createMappingEntries base vptr pgsz vm_rights' attrib' pd)"
apply simp
apply (cases pgsz, simp_all add: createMappingEntries_def mapping_map_def)
apply (rule corres_guard_imp)
apply (rule corres_split_eqrE)
apply (rule corres_returnOk [where P="\<top>" and P'="\<top>"])
apply (clarsimp simp: vmattributes_map_def)
apply (rule corres_lookup_error)
apply (rule lookup_pt_slot_corres)
apply wp+
apply clarsimp
apply simp
apply (rule corres_guard_imp)
apply (rule corres_split_eqrE)
apply (rule corres_returnOk [where P="\<top>" and P'="\<top>"])
apply (clarsimp simp: vmattributes_map_def)
apply (rule corres_lookup_error)
apply (rule lookup_pt_slot_corres)
apply wp+
apply clarsimp
apply simp
apply (rule corres_returnOk)
apply (simp add: vmattributes_map_def)
apply (rule corres_returnOk)
apply (simp add: vmattributes_map_def)
done
unfolding createMappingEntries_def mapping_map_def
by (cases pgsz; corressimp simp: vmattributes_map_def)
lemma pte_relation'_Invalid_inv [simp]:
"pte_relation' x ARM_HYP_H.pte.InvalidPTE = (x = ARM_A.pte.InvalidPTE)"
@ -1313,64 +1320,21 @@ lemma createMappingEntries_valid_slots' [wp]:
apply auto
done
lemma ensure_safe_mapping_corres:
lemmas mapME_x_corresK_inv =
mapME_x_corres_inv[OF corresK_unlift[where F=F], THEN corresK_lift[where F=F], corresK] for F
lemma ensure_safe_mapping_corres [corres]:
"mapping_map m m' \<Longrightarrow>
corres (ser \<oplus> dc) (valid_mapping_entries m)
(pspace_aligned' and pspace_distinct'
and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)))
(ensure_safe_mapping m) (ensureSafeMapping m')"
apply (simp add: mapping_map_def)
apply (cases m)
apply (case_tac a)
apply (case_tac aa)
apply (simp add: ensureSafeMapping_def corres_returnOk)
apply (simp add: ensureSafeMapping_def)
apply (rule corres_guard_imp)
apply (rule mapME_x_corres_inv)
apply (rule corres_initial_splitE [where Q="\<lambda>_. \<top>" and Q'="\<lambda>_. \<top>"])
apply simp
apply (rule get_master_pte_corres')
apply (case_tac rv, simp_all add: pte_relation_aligned_def
corres_returnOk split:ARM_HYP_H.pte.splits if_splits)[1]
apply wp[2]
apply (wp hoare_drop_imps|wpc|simp add:
valid_mapping_entries_def)+
apply (simp add: ensureSafeMapping_def corres_returnOk)
apply (rule corres_guard_imp)
apply (rule mapME_x_corres_inv)
apply (rule corres_initial_splitE [where Q="\<lambda>_. \<top>" and Q'="\<lambda>_. \<top>"])
apply simp
apply (rule get_master_pte_corres')
apply (case_tac rv, simp_all add: pte_relation_aligned_def
corres_returnOk split:ARM_HYP_H.pte.splits if_splits)[1]
apply wp[2]
apply (wp hoare_drop_imps|wpc|simp add:
valid_mapping_entries_def)+
apply (case_tac b)
apply clarsimp
apply (case_tac aa)
apply (simp_all add: ensureSafeMapping_def valid_mapping_entries_def)
apply (simp add: corres_returnOk)
apply (clarsimp simp:fail_def corres_underlying_def)
apply clarsimp
apply (rule corres_guard_imp)
apply (rule mapME_x_corres_inv)
apply (rule corres_initial_splitE [where Q="\<lambda>_. \<top>" and Q'="\<lambda>_. \<top>"])
apply simp
apply (rule get_master_pde_corres')
apply (case_tac rv, simp_all add: corres_returnOk )[1]
apply wp[2]
apply (wp hoare_drop_imps|wpc|simp)+
apply clarsimp
apply (rule corres_guard_imp)
apply (rule mapME_x_corres_inv)
apply (rule corres_initial_splitE [where Q="\<lambda>_. \<top>" and Q'="\<lambda>_. \<top>"])
apply simp
apply (rule get_master_pde_corres')
apply (case_tac rv, simp_all add: corres_returnOk)[1]
apply wp[2]
apply (wp hoare_drop_imps|wpc|simp)+
done
unfolding mapping_map_def ensureSafeMapping_def
apply (cases m; cases m'; simp;
match premises in "(_ \<otimes> op =) p p'" for p p' \<Rightarrow> \<open>cases "fst p"; cases "fst p'"\<close>; clarsimp)
by (corressimp corresK: mapME_x_corresK_inv
wp: get_master_pte_wp get_master_pde_wp getPTE_wp getPDE_wp;
auto simp add: valid_mapping_entries_def)+
lemma asidHighBitsOf [simp]:
"asidHighBitsOf asid = ucast (asid_high_bits_of asid)"
@ -1379,85 +1343,79 @@ lemma asidHighBitsOf [simp]:
apply (simp add: word_size nth_ucast)
done
lemma find_pd_for_asid_corres'':
lemma page_directory_at_lift:
"\<forall>s s'. (s, s') \<in> state_relation \<longrightarrow>
(pspace_aligned s \<and> page_directory_at ptr s) \<longrightarrow>
pspace_distinct' s' \<longrightarrow> page_directory_at' ptr s'"
by (fastforce intro!: page_directory_at_state_relation)
lemmas checkPDAt_corres =
corres_stateAssert_implied_frame[OF page_directory_at_lift, folded checkPDAt_def]
lemma getASID_wp:
"\<lbrace>\<lambda>s. \<forall>ko. ko_at' (ko::asidpool) p s \<longrightarrow> Q ko s\<rbrace> getObject p \<lbrace>Q\<rbrace>"
by (clarsimp simp: getObject_def split_def loadObject_default_def
archObjSize_def in_magnitude_check pageBits_def
projectKOs in_monad valid_def obj_at'_def objBits_simps)
lemma ko_at_typ_at_asidpool:
"ko_at (ArchObj (arch_kernel_obj.ASIDPool pool)) x s \<Longrightarrow> typ_at (AArch AASIDPool) x s"
by (clarsimp simp: obj_at_def a_type_simps)
lemma find_pd_for_asid_corres [corres]:
notes [corres del] = get_asid_pool_corres and [corres] = get_asid_pool_corres'
shows
"corres (lfr \<oplus> op =) ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid asid pd s)
and valid_vspace_objs and pspace_aligned
and K (0 < asid \<and> asid \<le> mask asidBits))
(pspace_aligned' and pspace_distinct' and no_0_obj')
(find_pd_for_asid asid) (findPDForASID asid)"
apply (simp add: find_pd_for_asid_def findPDForASID_def)
apply (rule corres_gen_asm, simp)
apply (simp add: liftE_bindE asidRange_def
mask_2pm1[symmetric])
apply (rule_tac r'="\<lambda>x y. x = y o ucast"
in corres_split' [OF _ _ gets_sp gets_sp])
apply (clarsimp simp: state_relation_def arch_state_relation_def)
apply (case_tac "rv (asid_high_bits_of asid)")
apply (simp add: liftME_def lookup_failure_map_def)
apply (simp add: liftME_def bindE_assoc)
apply (simp add: liftE_bindE)
apply (rule corres_guard_imp)
apply (rule corres_split [OF _ get_asid_pool_corres'])
apply (rule_tac P="case_option \<top> page_directory_at (pool (ucast asid)) and pspace_aligned"
and P'="no_0_obj' and pspace_distinct'" in corres_inst)
apply (rule_tac F="pool (ucast asid) \<noteq> Some 0" in corres_req)
apply (clarsimp simp: obj_at_def no_0_obj'_def state_relation_def
pspace_relation_def a_type_def)
apply (simp split: Structures_A.kernel_object.splits
arch_kernel_obj.splits if_split_asm)
apply (drule_tac f="\<lambda>S. 0 \<in> S" in arg_cong)
apply (simp add: pspace_dom_def)
apply (drule iffD1, rule rev_bexI, erule domI)
apply simp
apply (rule image_eqI[rotated])
apply (rule rangeI[where x=0])
apply simp
apply clarsimp
apply (simp add: mask_asid_low_bits_ucast_ucast returnOk_def
lookup_failure_map_def
split: option.split)
apply (clarsimp simp:checkPDAt_def stateAssert_def liftE_bindE bind_assoc)
apply (rule corres_noop)
apply (wpsimp simp:validE_def returnOk_def)+
apply (erule page_directory_at_state_relation)
apply simp+
apply (wp getObject_inv loadObject_default_inv | simp)+
apply clarsimp
apply (rule context_conjI)
apply (erule disjE)
apply (clarsimp simp: valid_arch_state_def valid_asid_table_def)
apply fastforce
apply (clarsimp simp: vspace_at_asid_def valid_arch_objs_def)
apply (clarsimp simp: vs_asid_refs_def graph_of_def elim!: vs_lookupE)
apply (erule rtranclE)
apply simp
apply (clarsimp dest!: vs_lookup1D)
apply (erule rtranclE)
apply (clarsimp simp: vs_refs_def graph_of_def obj_at_def
a_type_def
split: Structures_A.kernel_object.splits
arch_kernel_obj.splits)
apply (clarsimp dest!: vs_lookup1D)
apply (erule rtranclE)
apply (clarsimp dest!: vs_lookup1D)
apply (clarsimp dest!: vs_lookup1D)
apply clarsimp
apply (drule(1) valid_vspace_objsD[rotated])
apply (rule vs_lookupI)
apply (rule vs_asid_refsI)
apply simp
apply (rule rtrancl_refl)
apply (clarsimp split: option.split)
apply fastforce
apply simp
apply (simp add: find_pd_for_asid_def findPDForASID_def liftME_def bindE_assoc)
apply (corressimp simp: liftE_bindE assertE_assert mask_asid_low_bits_ucast_ucast lookup_failure_map_def
wp: getPDE_wp getASID_wp
search: checkPDAt_corres corres_gets_asid)
subgoal premises prems for s s'
apply (intro allI impI conjI)
subgoal asid_pool_at for x
apply (insert prems)
apply (elim conjE disjE)
apply (fastforce dest: valid_asid_tableD)
apply (clarsimp simp: vspace_at_asid_def valid_arch_objs_def)
apply (clarsimp simp: vs_asid_refs_def graph_of_def elim!: vs_lookupE)
apply (erule rtranclE)
subgoal by simp
apply (simp add: arm_asid_table_related[simplified o_def])
apply (clarsimp dest!: vs_lookup1D)
apply (erule rtranclE)
apply (clarsimp simp: vs_refs_def graph_of_def obj_at_def a_type_def
split: Structures_A.kernel_object.splits
arch_kernel_obj.splits)
apply (clarsimp dest!: vs_lookup1D)
apply (erule rtranclE)
apply (fastforce dest!: vs_lookup1D)
by (clarsimp dest!: vs_lookup1D)
subgoal pd_at for x pool xa
apply (insert prems)
apply (rule valid_vspace_obj_elims)
apply (rule valid_vspace_objsD)
apply (rule vs_lookupI)
apply (rule vs_asid_refsI)
apply fastforce
apply (rule rtrancl_refl)
by (simp add: ranI)+
apply (insert prems)
apply (fastforce simp add: asidRange_def mask_2pm1[symmetric])
subgoal for x ko xa
apply (cases ko; simp)
apply (frule arm_asid_table_related[where s'=s', simplified o_def])
apply (cut_tac asid_pool_at[of x, simplified obj_at_def])
apply clarsimp
apply (frule pspace_relation_absD, fastforce)
apply (clarsimp simp: other_obj_relation_def obj_at'_def projectKOs asid_pool_relation_def)
apply (cut_tac pd_at[of _ _ 0]; assumption?)
apply (drule(1) no_0_obj'_abstract)
by (auto simp add: obj_at_def inv_def o_def)
done
lemma find_pd_for_asid_corres:
"corres (lfr \<oplus> op =) ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid asid pd s) and valid_vspace_objs
and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits))
(pspace_aligned' and pspace_distinct' and no_0_obj')
(find_pd_for_asid asid) (findPDForASID asid)"
apply (rule find_pd_for_asid_corres'')
done
lemma find_pd_for_asid_corres':
@ -1465,7 +1423,7 @@ lemma find_pd_for_asid_corres':
and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits))
(pspace_aligned' and pspace_distinct' and no_0_obj')
(find_pd_for_asid asid) (findPDForASID asid)"
apply (rule corres_guard_imp, rule find_pd_for_asid_corres'')
apply (rule corres_guard_imp, rule find_pd_for_asid_corres)
apply fastforce
apply simp
done
@ -1574,12 +1532,6 @@ lemma setObject_pte_cur_tcb' [wp]:
apply wp+
done
lemma getASID_wp:
"\<lbrace>\<lambda>s. \<forall>ko. ko_at' (ko::asidpool) p s \<longrightarrow> Q ko s\<rbrace> getObject p \<lbrace>Q\<rbrace>"
by (clarsimp simp: getObject_def split_def loadObject_default_def
archObjSize_def in_magnitude_check pageBits_def
projectKOs in_monad valid_def obj_at'_def objBits_simps)
(* FIXME in ArcAcc_AI *)
lemma pde_shifting: (* ARMHYP >> 20? *)
"\<lbrakk>is_aligned (vptr::word32) 25; x \<le> 0xF\<rbrakk>

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

@ -826,13 +826,18 @@ lemma resolve_vaddr_valid_mapping_size:
lemma list_all2_Cons: "list_all2 f (x#xs) b \<Longrightarrow> \<exists>y ys. b = y # ys"
by (induct b; simp)
lemma corres_gets_numlistregs[corres]:
lemma corres_gets_numlistregsE[corres]:
"corres (r \<oplus> op =) \<top> \<top>
(liftE (gets (arm_gicvcpu_numlistregs \<circ> arch_state)))
(liftE (gets (armKSGICVCPUNumListRegs \<circ> ksArchState)))"
by (clarsimp simp: state_relation_def arch_state_relation_def)
lemma corres_whenE_str [corres]:
lemma corres_gets_numlistregs [corres]:
"corres (op =) \<top> \<top>
(gets (arm_gicvcpu_numlistregs \<circ> arch_state)) (gets (armKSGICVCPUNumListRegs \<circ> ksArchState))"
by (clarsimp simp: state_relation_def arch_state_relation_def)
lemma corres_whenE_str:
"\<lbrakk>G \<Longrightarrow> G' \<Longrightarrow> corres_underlying sr nf nf' (r \<oplus> dc) P P' a c\<rbrakk>
\<Longrightarrow> corres_underlying sr nf nf' (r \<oplus> dc) (K(G = G') and (\<lambda>x. G \<longrightarrow> P x)) (\<lambda>x. G' \<longrightarrow> P' x) (whenE G a) (whenE G' c)"
apply (simp add: corres_underlying_def)
@ -894,27 +899,16 @@ lemma dec_vcpu_inv_corres:
apply (case_tac a; clarsimp simp add: cap_relation_def)
apply (corres corres: corres_returnOkTT)
apply (clarsimp simp: archinv_relation_def vcpu_invocation_map_def)
apply simp
(* inject_irq *)
apply (simp add: decode_vcpu_inject_irq_def decodeVCPUInjectIRQ_def isVCPUCap_def)
apply (cases args; clarsimp)
apply (case_tac list; clarsimp simp add: rangeCheck_def range_check_def unlessE_whenE)
apply (clarsimp simp: shiftL_nat)
apply (rule corres_guard_imp)
apply (rule corres_splitE[where r'=dc])
apply corres
apply (corres corres: corres_splitE)
apply (rule corres_whenE)
apply simp
apply (rule corres_throwError_ser)
apply (rule dc_simp)
apply (rule corres_returnOkTT)
apply (clarsimp simp: archinv_relation_def vcpu_invocation_map_def ucast_id
make_virq_def makeVIRQ_def)
apply (wpsimp wp: get_vcpu_wp getVCPU_wp whenE_throwError_wp)+
apply (clarsimp simp: valid_cap_def)
apply simp
apply (clarsimp simp: valid_cap'_def)
apply (clarsimp simp: shiftL_nat whenE_bindE_throwError_to_if)
supply corresK(7)[corresK del]
apply (corressimp corresK: corresK_if wp: get_vcpu_wp corres_rv_defer_left)
apply (fastforce simp: archinv_relation_def vcpu_invocation_map_def ucast_id
valid_cap'_def valid_cap_def
make_virq_def makeVIRQ_def split:if_split)
(* read register *)
apply (clarsimp simp: decode_vcpu_read_register_def decodeVCPUReadReg_def)
apply (cases args; clarsimp simp: isCap_simps whenE_def split: if_split)
@ -1398,59 +1392,49 @@ lemma invokeVCPUInjectIRQ_corres:
(invokeVCPUInjectIRQ v index virq)"
unfolding invokeVCPUInjectIRQ_def invoke_vcpu_inject_irq_def
apply (clarsimp simp: bind_assoc)
apply corres
apply (rule option_corres; clarsimp simp: bind_assoc)
apply (corres corres: corres_get_vcpu set_vcpu_corres)
apply (rename_tac vcpu')
apply (case_tac vcpu')
apply (simp add: vcpu_relation_def vgic_map_def)
apply (rename_tac vgic regs)
apply (case_tac vgic)
apply simp
apply (rule ext)
apply simp
apply corres
apply (wpsimp wp: get_vcpu_wp getVCPU_wp)+
apply (corres corres: corres_machine_op corres_underlying_trivial)
apply (simp add: set_gic_vcpu_ctrl_lr_def)
apply (rule no_fail_machine_op_lift)
apply corres
apply wpsimp+
apply (corressimp corres: corres_get_vcpu set_vcpu_corres wp: corres_rv_wp_left get_vcpu_wp)
apply (rule conjI, fastforce)
apply (clarsimp simp: vcpu_relation_def vgic_map_def)
apply (rename_tac vcpu vcpu')
apply (case_tac vcpu; case_tac vcpu'; clarsimp)
apply (rename_tac vgic regs)
apply (case_tac vgic)
apply simp
apply (rule ext)
apply simp
done
lemmas corres_discard_r =
corres_symb_exec_r [where P'=P' and Q'="\<lambda>_. P'" for P', simplified]
lemma corres_prod [corres]:
"corres r P P' (f (fst p) (snd p)) (f' (fst p') (snd p'))
\<Longrightarrow> corres r P P' (case p of (a, b) \<Rightarrow> f a b) (case p' of (a', b') \<Rightarrow> f' a' b')"
by (cases p, cases p', simp)
lemma dmo_gets_corres:
"corres (op =) P P' (do_machine_op (gets f)) (doMachineOp (gets f))"
by (corres corres: corres_machine_op; fastforce)
apply (corres corres: corresK_machine_op)
apply (auto simp : corres_underlyingK_def)
done
lemmas corres_returnTT = corres_return[where P=\<top> and P'=\<top>, THEN iffD2]
lemma [wp]:"no_fail \<top> getSCTLR"
by (clarsimp simp: getSCTLR_def)
lemma invoke_vcpu_read_register_corres:
"corres (op =) (vcpu_at v) (vcpu_at' v)
(invoke_vcpu_read_register v r)
(invokeVCPUReadReg v r)"
unfolding invoke_vcpu_read_register_def invokeVCPUReadReg_def read_vcpu_register_def readVCPUReg_def
apply (rule corres_discard_r)
apply corres
apply (rule corres_if_str [where r="op =" and P="vcpu_at v" and P'="vcpu_at' v"])
apply (cases r; clarsimp simp: vcpuregs_gets dmo_gets_corres getSCTLR_def)
apply (corres corres: corres_get_vcpu corres_returnTT)
apply (simp add: vcpu_relation_def)
apply wpsimp+
apply (corres corres: corres_get_vcpu corres_returnTT)
apply (simp add: vcpu_relation_def)
apply (wp get_vcpu_wp getVCPU_wp)+
apply corres
apply (wpsimp simp: getCurThread_def)+
apply corres
apply (corres_once corresK: corresK_if)
apply (corresc)
apply (corressimp corres: corres_get_vcpu corresK: corresK_if wp: corres_rv_defer_left)+
apply (rule conjI)
apply (intro allI impI conjI; rule TrueI) (* FIXME where is this coming from? *)
apply (clarsimp simp: vcpu_relation_def split: option.splits)
apply (wpsimp simp: getCurThread_def)+
done
lemma dmo_rest_corres:
"corres dc P P' (do_machine_op (machine_op_lift f)) (doMachineOp (machine_op_lift f))"
apply (rule corres_rel_imp, rule corres_guard_imp)
@ -1460,6 +1444,9 @@ lemma dmo_rest_corres:
apply auto
done
lemma [wp]:"no_fail \<top> (setSCTLR x)"
by (clarsimp simp: setSCTLR_def)
lemma invoke_vcpu_write_register_corres:
"corres op = (vcpu_at vcpu) (vcpu_at' vcpu)
(do y \<leftarrow> invoke_vcpu_write_register vcpu r v;
@ -1469,22 +1456,17 @@ lemma invoke_vcpu_write_register_corres:
unfolding invokeVCPUWriteReg_def invoke_vcpu_write_register_def write_vcpu_register_def
writeVCPUReg_def
apply (rule corres_discard_r)
apply corres
apply (rule corres_if_str [where r="dc" and P="vcpu_at vcpu" and P'="vcpu_at' vcpu"])
apply (cases r; clarsimp simp: vcpuregs_sets dmo_rest_corres setSCTLR_def)
apply (corres corres: corres_get_vcpu set_vcpu_corres)
apply (simp add: vcpu_relation_def)
apply (rule ext)
apply simp
apply (wpsimp wp: get_vcpu_wp getVCPU_wp)+
apply (corres corres: corres_get_vcpu set_vcpu_corres)
apply (simp add: vcpu_relation_def)
apply (wp get_vcpu_wp getVCPU_wp)+
apply corres
apply (wpsimp)+
apply corres
apply (corres_once corresK: corresK_if)
apply (corresc)
apply (corressimp corres: set_vcpu_corres corres_get_vcpu corresK: corresK_if wp: corres_rv_defer_left)+
apply (rule conjI)
apply (intro allI impI conjI; rule TrueI) (* FIXME where is this coming from? *)
apply (auto simp: vcpu_relation_def split: option.splits)[1]
apply (wpsimp simp: getCurThread_def)+
done
lemma option_case_corres[corres]:
lemma option_case_corres:
"\<lbrakk> \<lbrakk> x = None; x' = None \<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r P P' A C;
\<And>z. \<lbrakk> x = Some z; x' = Some z \<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r (Q z) (Q' z) (B z) (D z)\<rbrakk>
\<Longrightarrow> corres_underlying sr nf nf' r (\<lambda>s. x = x' \<and> (x = None \<longrightarrow> P s) \<and> (\<forall>z. x = Some z \<longrightarrow> Q z s))
@ -1511,9 +1493,7 @@ lemma associate_vcpu_tcb_corres:
(associateVCPUTCB v t)"
unfolding associate_vcpu_tcb_def associateVCPUTCB_def
apply (clarsimp simp: bind_assoc)
apply (corres corres: corres_get_vcpu set_vcpu_corres)
apply (simp add: vcpu_relation_def)
apply corres
apply (corressimp search: corres_get_vcpu set_vcpu_corres simp: vcpu_relation_def)
apply (wpsimp wp: get_vcpu_wp getVCPU_wp)+
apply (rule_tac Q="\<lambda>_. invs and tcb_at t" in hoare_strengthen_post)
apply wp
@ -1521,10 +1501,8 @@ lemma associate_vcpu_tcb_corres:
apply (rule conjI)
apply (clarsimp simp: vcpu_relation_def)
apply (rule conjI)
apply clarsimp
apply (frule (1) sym_refs_vcpu_tcb, fastforce)
apply (clarsimp simp: obj_at_def)
apply (clarsimp simp: obj_at_def)
apply (clarsimp simp: obj_at_def)+
apply (wpsimp)
apply (rule_tac Q="\<lambda>_. invs' and tcb_at' t" in hoare_strengthen_post)
apply wpsimp
@ -1535,6 +1513,7 @@ lemma associate_vcpu_tcb_corres:
apply (simp add: valid_vcpu'_def typ_at_tcb')
apply (clarsimp simp: typ_at_to_obj_at_arches obj_at'_def)
apply (clarsimp simp: typ_at_to_obj_at_arches obj_at'_def)
apply (rule corres_rv_proveT, clarsimp)
apply (wpsimp wp: arch_thread_get_wp getObject_tcb_wp simp: archThreadGet_def)+
apply (rule conjI)
apply clarsimp
@ -1543,9 +1522,6 @@ lemma associate_vcpu_tcb_corres:
apply (frule (1) sym_refs_tcb_vcpu, fastforce)
apply (clarsimp simp: obj_at_def)
apply clarsimp
apply (rule conjI)
apply (clarsimp simp: vcpu_relation_def)
apply clarsimp
apply (frule (1) sym_refs_vcpu_tcb, fastforce)
apply (clarsimp simp: obj_at_def)
apply normalise_obj_at'

20
proof/refine/ARM_HYP/Bits_R.thy
View File

@ -221,7 +221,7 @@ lemma tcb_in_valid_state':
apply (fastforce simp add: valid_obj'_def valid_tcb'_def)
done
lemma gct_corres: "corres op = \<top> \<top> (gets cur_thread) getCurThread"
lemma gct_corres [corres]: "corres op = \<top> \<top> (gets cur_thread) getCurThread"
by (simp add: getCurThread_def curthread_relation)
lemma gct_wp [wp]: "\<lbrace>\<lambda>s. P (ksCurThread s) s\<rbrace> getCurThread \<lbrace>P\<rbrace>"
@ -278,7 +278,7 @@ lemma corres_injection:
apply (case_tac v, (clarsimp simp: z)+)
done
lemma corres_gets_pspace:
lemma corres_gets_pspace [corres]:
"corres pspace_relation \<top> \<top> (gets kheap) (gets ksPSpace)"
by (subst corres_gets, clarsimp)
@ -305,6 +305,8 @@ lemma corres_cap_fault:
by (fastforce intro: corres_injection[where f'=lfr]
simp: cap_fault_injection capFault_injection)
lemmas corresK_cap_fault = corres_cap_fault[atomized, THEN corresK_lift_rule, rule_format, corresK]
lemmas capFault_wp[wp] = injection_wp[OF capFault_injection]
lemmas capFault_wp_E[wp] = injection_wp_E[OF capFault_injection]
@ -318,6 +320,9 @@ lemma corres_lookup_error:
by (fastforce intro: corres_injection[where f'=lfr]
simp: lookup_error_injection lookupError_injection)
lemmas corresK_lookup_error =
corres_lookup_error[atomized, THEN corresK_lift_rule, rule_format, corresK]
lemmas lookupError_wp[wp] = injection_wp[OF lookupError_injection]
lemmas lookupError_wp_E[wp] = injection_wp_E[OF lookupError_injection]
@ -493,7 +498,8 @@ lemma corres_empty_on_failure:
apply simp+
done
lemmas corresK_empty_on_failure =
corres_empty_on_failure[atomized, THEN corresK_lift_rule, rule_format, corresK]
lemma emptyOnFailure_wp[wp]:
"\<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>,\<lbrace>\<lambda>rv. Q []\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> emptyOnFailure m \<lbrace>Q\<rbrace>"
@ -566,11 +572,19 @@ lemma corres_const_on_failure:
apply simp+
done
lemmas corresK_const_on_failure =
corres_const_on_failure[atomized, THEN corresK_lift_rule, rule_format, corresK]
lemma constOnFailure_wp :
"\<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>rv. Q n\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> constOnFailure n m \<lbrace>Q\<rbrace>"
apply (simp add: constOnFailure_def const_def)
apply (wp|simp)+
done
lemma corres_throwError_str [corres_concrete_rER]:
"corres_underlyingK sr nf nf' (r (Inl a) (Inl b)) r \<top> \<top> (throwError a) (throw b)"
"corres_underlyingK sr nf nf' (r (Inl a) (Inl b)) r \<top> \<top> (throwError a) (throwError b)"
by (simp add: corres_underlyingK_def)+
end
end

160
proof/refine/ARM_HYP/CSpace1_R.thy
View File

@ -285,7 +285,7 @@ lemma get_cap_corres_P:
apply (clarsimp simp: cte_wp_at_ctes_of)
done
lemmas get_cap_corres = get_cap_corres_P[where P="\<top>", simplified]
lemmas get_cap_corres [corres] = get_cap_corres_P[where P="\<top>", simplified]
lemma cap_relation_masks:
"cap_relation c c' \<Longrightarrow> cap_relation
@ -324,6 +324,11 @@ lemma getCTE_wp':
apply clarsimp
done
lemma show_const_pre_corres:
"corres_underlying sr nf nf' r (K F and P) P' f f' \<Longrightarrow>
(F \<Longrightarrow> corres_underlying sr nf nf' r P P' f f')"
by simp
lemma getSlotCap_corres:
"cte_ptr' = cte_map cte_ptr \<Longrightarrow>
corres cap_relation
@ -333,10 +338,7 @@ lemma getSlotCap_corres:
(getSlotCap cte_ptr')"
apply (simp add: getSlotCap_def)
apply (subst bind_return [symmetric])
apply (rule corres_guard_imp)
apply (rule corres_split [OF _ get_cap_corres])
apply (rule corres_trivial, simp)
apply (wp | simp)+
apply (corressimp)
done
lemma maskCapRights [simp]:
@ -538,6 +540,21 @@ lemma cap_table_at_gsCNodes:
declare resolve_address_bits'.simps[simp del]
lemma getSlotCap_valid:
"\<lbrace>\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> Q cap s))\<rbrace>
getSlotCap p \<lbrace>Q\<rbrace>"
apply (rule use_spec)
apply (simp add: spec_valid_def)
apply (rule hoare_add_post[OF getSlotCap_valid_cap1])
apply clarsimp
apply (rule hoare_add_post[OF getSlotCap_valid_cap2])
apply clarsimp
apply (rule hoare_add_post)
apply (rule_tac P="\<lambda>x. x = s" in getSlotCap_inv)
apply (clarsimp)
apply (clarsimp simp add: valid_def)
done
lemma rab_corres':
"\<lbrakk> cap_relation (fst a) c'; drop (32-bits) (to_bl cref') = snd a;
bits = length (snd a) \<rbrakk> \<Longrightarrow>
@ -577,9 +594,8 @@ proof (induct a arbitrary: c' cref' bits rule: resolve_address_bits'.induct)
prefer 7
apply (clarsimp simp: in_monad)
apply (rule get_cap_success)
apply (auto simp: in_monad intro!: get_cap_success) (* takes time *)
done
note if_split [split del]
by (auto simp: in_monad intro!: get_cap_success) (* takes time *)
note if_split [split del] isCNodeCap_cap_map[simp del] drop_append[simp del]
{ assume "cbits + length guard = 0 \<or> cbits = 0 \<and> guard = []"
hence ?thesis
apply (simp add: caps isCap_defs
@ -597,90 +613,62 @@ proof (induct a arbitrary: c' cref' bits rule: resolve_address_bits'.induct)
from "1.prems"
have ?thesis
apply -
apply (rule corres_assume_pre)
apply (subgoal_tac "is_aligned ptr (4 + cbits) \<and> cbits \<le> word_bits - cte_level_bits")
prefer 2
apply (clarsimp simp: caps)
apply (erule valid_CNodeCapE)
apply fastforce
apply fastforce
apply fastforce
apply (thin_tac "t \<in> state_relation" for t)
apply (erule conjE)
apply (subst resolveAddressBits.simps)
apply (subst resolve_address_bits'.simps)
apply (simp add: caps isCap_defs Let_def)
apply (simp add: linorder_not_less drop_postfix_eq)
apply (simp add: liftE_bindE[where a="locateSlotCap a b" for a b])
apply (simp add: locateSlot_conv)
apply (rule corres_stateAssert_assume_stronger[rotated])
apply (clarsimp simp: valid_cap_def cap_table_at_gsCNodes isCap_simps)
apply (rule and_mask_less_size, simp add: word_bits_def word_size cte_level_bits_def)
apply (erule exE)
apply (cases "guard \<le> cref")
prefer 2
apply (clarsimp simp: guard_mask_shift lookup_failure_map_def unlessE_whenE)
apply (clarsimp simp: guard_mask_shift unlessE_whenE)
apply (cases "length cref < cbits + length guard")
apply (simp add: lookup_failure_map_def)
apply simp
apply (cases "length cref = cbits + length guard")
apply clarsimp
apply (rule corres_noopE)
prefer 2
apply wp
apply wp
apply (clarsimp simp: objBits_simps cte_level_bits_def)
apply (erule (2) valid_CNodeCapE)
apply (erule (3) cte_map_shift')
apply simp
apply simp
apply (subgoal_tac "cbits + length guard < length cref"; simp)
apply (rule corres_initial_splitE)
apply clarsimp
apply (rule corres_guard_imp)
apply (rule getSlotCap_corres)
apply (simp add: objBits_simps cte_level_bits_def)
apply (erule (1) cte_map_shift)
apply simp
apply assumption
apply (simp add: cte_level_bits_def)
apply clarsimp
apply (simp add: Let_def unlessE_whenE)
apply (simp add: caps isCap_defs Let_def whenE_bindE_throwError_to_if)
apply (subst cnode_cap_case_if)
apply (corressimp search: getSlotCap_corres IH
wp: get_cap_wp getSlotCap_valid no_fail_stateAssert
corres_rv_defer_right
simp: locateSlot_conv)
supply isCNodeCap_cap_map[simp]
apply (simp add: drop_postfix_eq)
apply clarsimp
apply (prove "is_aligned ptr (4 + cbits) \<and> cbits \<le> word_bits - cte_level_bits")
apply (erule valid_CNodeCapE; fastforce)
subgoal premises prems for s s' x
apply (insert prems)
apply (rule conjI)
apply (clarsimp split: if_splits)
apply safe[1]
apply (clarsimp simp: valid_cap_def)
apply (erule cap_table_at_cte_at)
apply simp
subgoal by simp
apply (frule (1) cte_wp_valid_cap)
subgoal for cap by (cases cap; simp)
apply (simp add: caps lookup_failure_map_def)
apply (frule guard_mask_shift[where guard=guard])
apply (intro conjI)
apply fastforce
apply clarsimp
apply (rule conjI)
apply (clarsimp simp add: objBits_simps cte_level_bits_def)
apply (erule (2) valid_CNodeCapE)
apply (erule (3) cte_map_shift')
subgoal by simp
apply (clarsimp simp add: objBits_simps cte_level_bits_def)
apply (erule (1) cte_map_shift; assumption?)
subgoal by simp
apply (clarsimp simp: cte_level_bits_def)
apply (clarsimp simp: valid_cap_def cap_table_at_gsCNodes isCap_simps)
apply (rule and_mask_less_size, simp add: word_bits_def word_size cte_level_bits_def)
apply (clarsimp simp: isCap_simps caps split: if_splits)
apply (intro conjI impI allI;clarsimp?)
apply (subst \<open>to_bl _ = _\<close>[symmetric])
apply (drule postfix_dropD)
apply clarsimp
apply (case_tac "is_cnode_cap rv")
prefer 2
apply (simp add: cnode_cap_case_if)
apply (rule corres_noopE)
prefer 2
apply (rule no_fail_pre, rule no_fail_returnOK)
apply (rule TrueI)
prefer 2
apply (simp add: unlessE_whenE cnode_cap_case_if)
apply (rule IH, (simp_all)[9])
apply (prove "32 + (cbits + length guard) - length cref =
(cbits + length guard) + (32 - length cref)")
apply (drule len_drop_lemma, simp, arith)
apply simp
apply (subst drop_drop [symmetric])
subgoal by simp
apply (simp add: objBits_simps cte_level_bits_def)
apply (erule (1) cte_map_shift; assumption?)
apply clarsimp
apply (drule postfix_dropD)
apply clarsimp
apply (subgoal_tac "32 + (cbits + length guard) - length cref = (cbits + length guard) + (32 - length cref)")
prefer 2
apply (drule len_drop_lemma)
apply simp
apply arith
apply simp
apply (subst drop_drop [symmetric])
apply simp
apply wp
apply (clarsimp simp: objBits_simps cte_level_bits_def)
apply (erule (1) cte_map_shift)
apply simp
apply assumption
apply (simp add: cte_level_bits_def)
apply (wp get_cap_wp)
apply clarsimp
apply (erule (1) cte_wp_valid_cap)
apply wpsimp
subgoal by (simp add: cte_level_bits_def)
done
done
}
ultimately

3
proof/refine/ARM_HYP/Corres.thy
View File

@ -16,4 +16,7 @@ text {* Instantiating the corres framework to this particular state relation. *}
abbreviation
"corres \<equiv> corres_underlying state_relation False True"
abbreviation
"corresK \<equiv> corres_underlyingK state_relation False True"
end

40
proof/refine/ARM_HYP/Finalise_R.thy
View File

@ -3964,24 +3964,15 @@ lemma sym_refs_vcpu_tcb:
lemma vcpuFinalise_corres [corres]:
"corres dc (invs and vcpu_at vcpu) (invs' and vcpu_at' vcpu) (vcpu_finalise vcpu) (vcpuFinalise vcpu)"
unfolding vcpuFinalise_def vcpu_finalise_def
apply (corres corres: corres_get_vcpu)
apply (clarsimp simp: vcpu_relation_def)
apply (rule option_corres; clarsimp)
apply corres
apply (wp get_vcpu_wp)
apply (wp getVCPU_wp)
apply clarsimp
apply (corressimp corres: corres_get_vcpu simp: vcpu_relation_def)
apply (wpsimp wp: get_vcpu_wp getVCPU_wp)+
apply (rule conjI)
apply clarsimp
apply (rule conjI, fastforce)
apply clarsimp
apply (frule sym_refs_vcpu_tcb)
apply (simp add: vcpu_relation_def)
apply fastforce
apply (clarsimp simp: obj_at_def vcpu_relation_def)
apply clarsimp
apply (rule conjI, fastforce)
apply clarsimp
apply (drule ko_at_valid_objs', fastforce, simp add: projectKOs)
apply (clarsimp simp: valid_obj'_def valid_vcpu'_def typ_at_tcb')
done
@ -4164,7 +4155,7 @@ lemma corres_add_guard:
"\<lbrakk>\<And>s s'. \<lbrakk>Q s; Q' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> P s \<and> P' s';
corres_underlying sr nf nf' r (Q and P) (Q' and P') f g\<rbrakk> \<Longrightarrow>
corres_underlying sr nf nf' r Q Q' f g"
by (erule stronger_corres_guard_imp_str, simp)
by (auto simp: corres_underlying_def)
lemma finalise_cap_corres:
"\<lbrakk> final_matters' cap' \<Longrightarrow> final = final'; cap_relation cap cap';
@ -4751,6 +4742,31 @@ lemma cteDeleteOne_ct_not_ksQ:
apply (clarsimp)
done
(* FIXME move to Corres_Method? *)
lemma corres_underlying_equiv_raw: "(nf \<Longrightarrow> no_fail P f) \<Longrightarrow> (nf' \<Longrightarrow> no_fail P' f) \<Longrightarrow>
corres_underlyingK Id nf nf' True (op =) P P' f f"
apply (simp add: corres_underlyingK_def corres_underlying_def Id_def)
by (auto simp: no_fail_def)
lemma corres_underlying_equiv_dc_raw: "(nf \<Longrightarrow> no_fail P f) \<Longrightarrow> (nf' \<Longrightarrow> no_fail P' f) \<Longrightarrow>
corres_underlyingK Id nf nf' True dc P P' f f"
apply (simp add: corres_underlyingK_def corres_underlying_def Id_def)
by (auto simp: no_fail_def)
(* FIXME cleanup *)
lemmas corres_underlying_equiv [corresK] =
corres_underlying_equiv_raw[where nf=False and nf'=True and P=\<top>, simplified]
lemmas corres_underlying_equiv_dc [corresK] =
corres_underlying_equiv_dc_raw[where nf=False and nf'=True and P=\<top>, simplified]
(* end of move to Corres_Method *)
(* FIXME Move to Machine_AI? *)
lemma no_fail_set_gic_vcpu_ctrl_lr[wp]: "no_fail \<top> (set_gic_vcpu_ctrl_lr w p)"
by (wpsimp simp: set_gic_vcpu_ctrl_lr_def)
end
end

73
proof/refine/ARM_HYP/Interrupt_R.thy
View File

@ -592,11 +592,14 @@ lemma countTrailingZeros_simp [simp]:
lemma corres_do_machine_op_gets[corres]:
"f = f' \<Longrightarrow> corres (op =) \<top> \<top> (do_machine_op (gets f)) (doMachineOp (gets f'))"
by (corres corres: corres_machine_op; simp)
by (corressimp search: corres_machine_op corres_underlying_trivial; simp)
lemma corres_do_machine_op_machine_lift[corres]:
"f = f' \<Longrightarrow> corres dc \<top> \<top> (do_machine_op (machine_op_lift f)) (doMachineOp (machine_op_lift f'))"
by (corres corres: corres_machine_op corres_eq_trivial; simp)
apply (rule corres_machine_op, simp)
apply (rule corres_eq_trivial)
apply (clarsimp simp: no_fail_machine_op_lift)+
done
lemma dmo_machine_op_lift_invs'[wp]:
"doMachineOp (machine_op_lift f) \<lbrace>invs'\<rbrace>"
@ -607,46 +610,55 @@ lemma doMachineOp_get_invs [wp]:
"doMachineOp (gets f) \<lbrace>P\<rbrace>"
unfolding doMachineOp_def by (wpsimp simp: in_monad)
(* FIXME: move to Machine_AI *)
lemma no_fail_get_gic_vcpu_ctrl_eisr0[wp]: "no_fail \<top> get_gic_vcpu_ctrl_eisr0"
by (wpsimp simp: get_gic_vcpu_ctrl_eisr0_def)
lemma no_fail_get_gic_vcpu_ctrl_eisr1[wp]: "no_fail \<top> get_gic_vcpu_ctrl_eisr1"
by (wpsimp simp: get_gic_vcpu_ctrl_eisr1_def)
lemma no_fail_get_gic_vcpu_ctrl_misr[wp]: "no_fail \<top> get_gic_vcpu_ctrl_misr"
by (wpsimp simp: get_gic_vcpu_ctrl_misr_def)
lemma vgic_maintenance_corres [corres]:
"corres dc einvs
(\<lambda>s. invs' s \<and> sch_act_not (ksCurThread s) s \<and> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)))
vgic_maintenance vgicMaintenance"
apply (simp add: vgic_maintenance_def vgicMaintenance_def isRunnable_def Let_def
get_thread_state_def[symmetric] virqSetEOIIRQEN_def ARM_A.virqSetEOIIRQEN_def
get_gic_vcpu_ctrl_eisr0_def get_gic_vcpu_ctrl_eisr1_def
get_gic_vcpu_ctrl_misr_def get_gic_vcpu_ctrl_lr_def set_gic_vcpu_ctrl_lr_def
bind_assoc do_machine_op_bind doMachineOp_bind
cong: if_cong)
apply (corres corres: gct_corres [unfolded getCurThread_def] gts_corres corres_if_str
| simp split del: if_split cong: if_cong)+
apply (wp hoare_vcg_all_lift hoare_drop_imps)+
apply corres
apply (simp split del: if_split cong: if_cong |
wp hoare_TrueI[where P=\<top>])+
apply (corres corres: gct_corres hf_corres)
apply simp
apply (wpsimp split_del: if_split wp: hoare_drop_imps)+
apply (corressimp corresK: corresK_if corres: gct_corres [unfolded getCurThread_def] gts_corres
wp: corres_rv_wp_left no_fail_get_gic_vcpu_ctrl_lr
| simp split del: if_split cong: if_cong )+
apply (corressimp corres: hf_corres wp: hoare_vcg_all_lift hoare_drop_imps )+ (* corres_rv_wp_left causes loop here *)
apply (rule hoare_lift_Pf[where f=ksCurThread])
apply wp+
apply (rule hoare_lift_Pf[where f=ksCurThread])
apply wp+
apply (wpsimp split_del: if_split
simp: valid_fault_def
apply (simp split del: if_split cong: if_cong | wp hoare_TrueI[where P=\<top>])+
apply (wpsimp split_del: if_split
simp: get_gic_vcpu_ctrl_misr_def valid_fault_def get_gic_vcpu_ctrl_eisr0_def get_gic_vcpu_ctrl_eisr1_def
wp: hoare_TrueI[where P=\<top>] gts_wp gts_wp' hoare_vcg_const_imp_lift
hoare_drop_imps hoare_vcg_if_lift2 hoare_vcg_if_lift3)+
apply (clarsimp simp: invs_def invs'_def cur_tcb_def cur_tcb'_def cong: conj_cong)
apply (rule conjI)
apply (clarsimp simp: runnable_eq)
apply (rename_tac st st')
apply (rule context_conjI, (case_tac st; simp))
apply clarsimp
apply (rule context_conjI)
apply (clarsimp simp: st_tcb_at_def obj_at_def)
apply (fastforce elim!: st_tcb_ex_cap simp: valid_state_def valid_pspace_def)
apply (clarsimp cong: conj_cong simp: conj_commute)
apply (rule conjI)
apply (fastforce elim!: st_tcb_ex_cap'' simp: valid_state'_def valid_pspace'_def)
by (clarsimp simp: st_tcb_at'_def obj_at'_def split: thread_state.splits)
hoare_drop_imps hoare_vcg_if_lift2 hoare_vcg_if_lift3
| (rule corres_rv_proveT, fastforce simp: thread_state_relation_def))+
defer
apply (wpsimp split_del: if_splits)+
apply (clarsimp simp: invs_def invs'_def cur_tcb_def cur_tcb'_def cong: conj_cong)
apply (rule conjI, assumption)
apply (rule conjI)
apply (clarsimp simp: runnable_eq, rule conjI; clarsimp, rule context_conjI,
clarsimp simp: st_tcb_at_def obj_at_def;
fastforce elim!: st_tcb_ex_cap simp: valid_state_def valid_pspace_def)
apply (rule conjI, assumption)
apply (clarsimp cong: conj_cong simp: conj_commute)
apply (rule conjI)
apply (fastforce elim!: st_tcb_ex_cap'' simp: valid_state'_def valid_pspace'_def)
apply (clarsimp simp: st_tcb_at'_def obj_at'_def split: thread_state.splits)
apply (rule corres_rv_prove)
apply (clarsimp simp: runnable_eq)
apply (rename_tac st st')
by (rule context_conjI, (case_tac st; simp), simp)
lemma handle_reserved_irq_corres[corres]:
"corres dc einvs
@ -658,6 +670,7 @@ lemma handle_reserved_irq_corres[corres]:
apply (clarsimp simp: non_kernel_IRQs_def)
done
lemma handle_interrupt_corres:
"corres dc
(einvs)
@ -713,7 +726,7 @@ lemma handle_interrupt_corres:
apply wp+
apply clarsimp
apply clarsimp
apply (corres corres: corres_machine_op corres_eq_trivial)
apply (corres corresK: corresK_machine_op)
apply (wpsimp simp: no_fail_ackInterrupt)+
done

68
proof/refine/ARM_HYP/IpcCancel_R.thy
View File

@ -1434,8 +1434,11 @@ lemma archThreadGet_corres:
corres (op =) (tcb_at t) (tcb_at' t) (arch_thread_get f t) (archThreadGet f' t)"
unfolding arch_thread_get_def archThreadGet_def
apply corres
apply (rule corresK_drop)
apply (rule corres_bind_return2)
apply (corres corres: get_tcb_corres)
apply (rule corres_split)
prefer 2
apply (rule get_tcb_corres)
apply (rule corres_return[where P=\<top> and P'=\<top>,THEN iffD2])
apply (clarsimp simp: tcb_relation_def)
apply wpsimp+
@ -1466,20 +1469,11 @@ lemma corres_gets_current_vcpu[corres]:
lemma vcpuInvalidateActive_corres[corres]:
"corres dc \<top> \<top> vcpu_invalidate_active vcpuInvalidateActive"
unfolding vcpuInvalidateActive_def vcpu_invalidate_active_def
apply corres
apply (clarsimp simp: modifyArchState_def split: option.splits)
apply (rule conjI, clarsimp)
apply (corressimp corres: vcpuDisable_corres simp: modifyArchState_def)
apply (rule corresK_assume_guard)
apply (rule corres_modify[where P=\<top> and P'=\<top>])
apply (clarsimp simp: state_relation_def arch_state_relation_def)
apply (clarsimp split: bool.splits)
apply (rule conjI, clarsimp)
apply (corres corres: vcpuDisable_corres)
apply (rule corres_modify[where P=\<top> and P'=\<top>])
apply (clarsimp simp: state_relation_def arch_state_relation_def)
apply wpsimp+
apply (rule corres_modify[where P=\<top> and P'=\<top>])
apply (clarsimp simp: state_relation_def arch_state_relation_def)
apply wpsimp+
apply wpsimp+
done
lemma tcb_ko_at':
@ -1491,18 +1485,11 @@ lemma archThreadSet_corres:
corres dc (tcb_at t) (tcb_at' t) (arch_thread_set f t) (archThreadSet f' t)"
apply (simp add: arch_thread_set_def archThreadSet_def)
apply (corres corres: get_tcb_corres)
apply (rule corresK_drop)
apply (rename_tac tcb tcb')
apply (rule_tac tcb=tcb and tcb'=tcb' in tcb_update_corres')
apply (simp add: tcb_relation_def)
apply (simp add: tcb_cap_cases_def)
apply (simp add: tcb_cte_cases_def)
apply simp
apply (simp add: exst_same_def)
apply wp
apply (wp getObject_tcb_wp)
apply clarsimp
apply (drule tcb_ko_at')
apply fastforce
apply (simp add: tcb_relation_def tcb_cap_cases_def tcb_cte_cases_def exst_same_def)+
apply wpsimp+
done
lemma archThreadSet_corres_vcpu_None[corres]:
@ -1532,7 +1519,6 @@ lemma asUser_sanitise_corres[corres]:
apply (clarsimp simp: tcb_relation_def arch_tcb_relation_def)
apply (rule corres_Id, simp, simp)
apply wpsimp
apply simp
done
crunch typ_at'[wp]: vcpuInvalidateActive "\<lambda>s. P (typ_at' T p s)"
@ -1563,26 +1549,30 @@ lemma imp_drop_strg:
"Q \<Longrightarrow> P \<longrightarrow> Q"
by simp
lemma helper: "vcpu_relation v1 v2 \<Longrightarrow> vcpu_relation v1 v3 \<Longrightarrow> v2 = v3"
apply (auto simp: vcpu_relation_def)
apply (cases v2; cases v3; clarsimp)
done
lemma dissociateVCPUTCB_corres [corres]:
"corres dc (obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> tcb_vcpu (tcb_arch tcb) = Some v) t and
obj_at (\<lambda>ko. \<exists>vcpu. ko = ArchObj (VCPU vcpu) \<and> vcpu_tcb vcpu = Some t) v)
(tcb_at' t and vcpu_at' v)
(dissociate_vcpu_tcb v t) (dissociateVCPUTCB v t)"
apply (clarsimp simp: dissociate_vcpu_tcb_def dissociateVCPUTCB_def bind_assoc
when_fail_assert opt_case_when )
apply (corres corres: corres_get_vcpu set_vcpu_corres get_tcb_corres
| simp add: vcpu_relation_def)+
apply (wpsimp wp: getObject_tcb_wp get_vcpu_wp getVCPU_wp arch_thread_get_wp
simp: tcb_ko_at' tcb_at_typ_at' archThreadSet_def archThreadGet_def
| strengthen imp_drop_strg[where Q="tcb_at t s" for s]
imp_drop_strg[where Q="vcpu_at' v s \<and> typ_at' TCBT t s" for s])+
unfolding dissociate_vcpu_tcb_def dissociateVCPUTCB_def
apply (clarsimp simp: bind_assoc when_fail_assert opt_case_when)
apply (corressimp corres: corres_get_vcpu set_vcpu_corres get_tcb_corres)
apply (wpsimp wp: arch_thread_get_wp
simp: archThreadSet_def tcb_ko_at' tcb_at_typ_at'
| strengthen imp_drop_strg[where Q="tcb_at t s" for s]
imp_drop_strg[where Q="vcpu_at' v s \<and> typ_at' TCBT t s" for s]
| (rule corres_rv_proveT, fastforce simp: vcpu_relation_def ))+
apply (corressimp wp: get_vcpu_wp getVCPU_wp getObject_tcb_wp arch_thread_get_wp corres_rv_wp_left
simp: archThreadGet_def tcb_ko_at')+
apply (clarsimp simp: typ_at_tcb' typ_at_to_obj_at_arches)
apply normalise_obj_at'
apply (drule obj_at_ko_atD)+
apply clarsimp
apply (frule (2) ko_at_tcb_relationD)
apply (frule (2) ko_at_vcpu_relationD)
apply (clarsimp simp: obj_at_def is_tcb vcpu_relation_def tcb_relation_def arch_tcb_relation_def)
apply (clarsimp simp: obj_at_def is_tcb vcpu_relation_def tcb_relation_def
arch_tcb_relation_def vgic_map_def )
done
lemma sym_refs_tcb_vcpu:
@ -1600,10 +1590,12 @@ lemma prepareThreadDelete_corres:
"corres dc (invs and tcb_at t) (valid_objs' and tcb_at' t)
(prepare_thread_delete t) (prepareThreadDelete t)"
apply (simp add: prepare_thread_delete_def prepareThreadDelete_def)
apply (corres|corresc|simp add: tcb_vcpu_relation)+
apply (corressimp simp: tcb_vcpu_relation)
apply (wp arch_thread_get_wp)
apply (wpsimp wp: getObject_tcb_wp simp: archThreadGet_def)
apply clarsimp
apply (rule corres_rv_proveT, simp)
apply clarsimp
apply (rule conjI)
apply clarsimp
apply (frule (1) sym_refs_tcb_vcpu, fastforce)

77
proof/refine/ARM_HYP/KHeap_R.thy
View File

@ -154,7 +154,7 @@ lemma no_fail_getObject_vcpu[wp]: "no_fail (vcpu_at' vcpu) (getObject vcpu :: vc
lemma vcpu_at_ko: "typ_at (AArch AVCPU) p s \<Longrightarrow> \<exists>vcpu. ko_at (ArchObj (arch_kernel_obj.VCPU vcpu)) p s "
by (clarsimp simp add: obj_at_def)
lemma corres_get_tcb:
lemma corres_get_tcb [corres]:
"corres (tcb_relation \<circ> the) (tcb_at t) (tcb_at' t) (gets (get_tcb t)) (getObject t)"
apply (rule corres_no_failI)
apply wp
@ -943,7 +943,7 @@ lemma no_fail_getEndpoint [wp]:
apply (clarsimp split: option.split_asm simp: objBits_simps archObjSize_def)
done
lemma get_ep_corres:
lemma get_ep_corres [corres]:
"corres ep_relation (ep_at ptr) (ep_at' ptr)
(get_endpoint ptr) (getEndpoint ptr)"
apply (rule corres_no_failI)
@ -1127,77 +1127,32 @@ lemma set_other_obj_corres:
apply (case_tac ob;
simp_all add: a_type_def other_obj_relation_def etcb_relation_def
is_other_obj_relation_type t exst_same_def)
apply (clarsimp simp: is_other_obj_relation_type t exst_same_def
by (clarsimp simp: is_other_obj_relation_type t exst_same_def
split: Structures_A.kernel_object.splits Structures_H.kernel_object.splits
ARM_A.arch_kernel_obj.splits)+
done
lemma set_ep_corres:
lemmas obj_at_simps = obj_at_def obj_at'_def projectKOs map_to_ctes_upd_other
is_other_obj_relation_type_def
a_type_def objBits_simps other_obj_relation_def
archObjSize_def pageBits_def
lemma set_ep_corres [corres]:
"ep_relation e e' \<Longrightarrow>
corres dc (ep_at ptr) (ep_at' ptr)
(set_endpoint ptr e) (setEndpoint ptr e')"
apply (simp add: set_endpoint_def setEndpoint_def is_ep_def[symmetric])
apply (rule corres_symb_exec_l)
prefer 4
apply (rule no_fail_pre, wp)
apply (clarsimp simp: obj_at_def)
prefer 3
apply (rule get_object_sp)
apply (rule corres_symb_exec_l)
prefer 4
apply (rule no_fail_pre, wp)
apply (clarsimp simp: obj_at_def)
prefer 3
apply (rule assert_sp)
apply (rule corres_guard_imp)
apply (rule set_other_obj_corres [where P="\<top>"])
apply (rule ext)+
apply simp
apply (clarsimp simp add: obj_at'_def projectKOs map_to_ctes_upd_other)
apply (clarsimp simp: is_other_obj_relation_type_def a_type_def)
apply (simp add: objBits_simps)
apply simp
apply (simp add: objBits_simps)
apply (simp add: other_obj_relation_def)
apply (clarsimp simp: obj_at_def is_ep a_type_def)
apply assumption
apply (clarsimp simp: exs_valid_def assert_def return_def fail_def obj_at_def)
apply (clarsimp simp: exs_valid_def get_object_def bind_def in_monad
gets_def get_def return_def assert_def fail_def obj_at_def)
done
apply (corres_search search: set_other_obj_corres[where P="\<lambda>_. True"])
apply (wp get_object_ret get_object_wp)+
by (clarsimp simp: is_ep obj_at_simps)
lemma set_ntfn_corres:
lemma set_ntfn_corres [corres]:
"ntfn_relation ae ae' \<Longrightarrow>
corres dc (ntfn_at ptr) (ntfn_at' ptr)
(set_notification ptr ae) (setNotification ptr ae')"
apply (simp add: set_notification_def setNotification_def is_ntfn_def[symmetric])
apply (rule corres_symb_exec_l)+
prefer 7
apply (rule no_fail_pre, wp)
apply (clarsimp simp: obj_at_def)
prefer 6
apply (rule get_object_sp)
prefer 3
apply (rule assert_sp)
prefer 3
apply (rule no_fail_pre, wp)
apply (clarsimp simp: obj_at_def)
apply (rule corres_guard_imp)
apply (rule set_other_obj_corres [where P="\<top>"])
apply (rule ext)+
apply simp
apply (clarsimp simp add: obj_at'_def projectKOs map_to_ctes_upd_other)
apply (clarsimp simp: is_other_obj_relation_type_def a_type_def)
apply (simp add: objBits_simps)
apply simp
apply (simp add: objBits_simps)
apply (simp add: other_obj_relation_def)
apply (clarsimp simp: obj_at_def a_type_def is_ntfn)
apply assumption
apply (clarsimp simp: exs_valid_def assert_def return_def fail_def obj_at_def)
apply (clarsimp simp: exs_valid_def get_object_def bind_def in_monad
gets_def get_def return_def assert_def fail_def obj_at_def)
done
apply (corres_search search: set_other_obj_corres[where P="\<lambda>_. True"])
apply (wp get_object_ret get_object_wp)+
by (clarsimp simp: is_ntfn obj_at_simps)
lemma no_fail_getNotification [wp]:
"no_fail (ntfn_at' ptr) (getNotification ptr)"

3
proof/refine/ARM_HYP/SubMonad_R.thy
View File

@ -31,6 +31,9 @@ lemma corres_machine_op:
apply (simp_all add: state_relation_def swp_def)
done
lemmas corresK_machine_op =
corres_machine_op[atomized, THEN corresK_lift_rule, rule_format, corresK]
lemma doMachineOp_mapM:
assumes "\<And>x. empty_fail (m x)"
shows "doMachineOp (mapM m l) = mapM (doMachineOp \<circ> m) l"

3
proof/refine/ARM_HYP/VSpace_R.thy
View File

@ -773,8 +773,7 @@ lemma vcpuSave_corres:
apply (rule corres_guard_imp[OF _ TrueI TrueI])
apply (rule corres_split'[OF corres_machine_op _ wp_post_taut wp_post_taut],
rule corres_underlying_trivial[OF non_fail_gets_simp])+
apply (simp only:)
apply (rule corres_return_eq)
apply corressimp
apply (clarsimp simp add: vcpu_relation_def vcpuSCTLR_def)
apply (drule sym[of "vgic_map _"])
apply (simp add: vgic_map_def)