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

refine: integrate all architectures

This commit is contained in:
Joel Beeren 2017-08-02 16:05:04 +10:00 committed by Matthew Brecknell
parent 7602a6c350
commit 42401684b0
30 changed files with 303 additions and 189 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
proof/refine/ARM/ADT_H.thy
View File

@ -436,7 +436,7 @@ lemma ArchFaultMap_arch_fault_map: "ArchFaultMap (arch_fault_map f) = f"
lemma FaultMap_fault_map[simp]:
"valid_fault ft \<Longrightarrow> FaultMap (fault_map ft) = ft"
apply (case_tac ft, simp_all)
apply (simp add: valid_fault_def LookupFailureMap_lookup_failure_map)
apply (simp add: valid_fault_def LookupFailureMap_lookup_failure_map word_bits_def)
apply (rule ArchFaultMap_arch_fault_map)
done

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

@ -242,9 +242,9 @@ lemma pac_corres:
updateFreeIndex_caps_overlap_reserved
| simp add: descendants_of_null_filter' split del: if_split)+
apply (wp get_cap_wp)+
apply (subgoal_tac "word1 && ~~ mask pageBits = word1 \<and> pageBits \<le> word_bits \<and> 2 \<le> pageBits")
apply (subgoal_tac "word1 && ~~ mask pageBits = word1 \<and> pageBits \<le> word_bits \<and> word_size_bits \<le> pageBits")
prefer 2
apply (clarsimp simp:pageBits_def word_bits_def is_aligned_neg_mask_eq)
apply (clarsimp simp:pageBits_def word_bits_def is_aligned_neg_mask_eq word_size_bits_def)
apply (simp only:delete_objects_rewrite)
apply wp+
apply (clarsimp simp: conj_comms)

2
proof/refine/ARM/CNodeInv_R.thy
View File

@ -99,7 +99,7 @@ lemma cap_relation_NullCap:
split del: if_split)
apply simp
apply simp
apply (clarsimp simp: word_size word_size_def)
apply (clarsimp simp: word_size word_size_def cteRightsBits_def cteGuardBits_def)
apply (clarsimp simp: ARM_H.updateCapData_def isCap_simps split del: if_split)
done

5
proof/refine/ARM/CSpace1_R.thy
View File

@ -452,7 +452,8 @@ proof -
ARM_H.updateCapData_def)[5]
-- CNodeCap
apply (simp add: simps word_bits_def the_cnode_cap_def andCapRights_def
rightsFromWord_def data_to_rights_def nth_ucast)
rightsFromWord_def data_to_rights_def nth_ucast cteRightsBits_def
cteGuardBits_def)
apply (insert x)
apply (subgoal_tac "unat ((x >> 3) && mask 5) < unat (2^5::word32)")
prefer 2
@ -624,7 +625,7 @@ proof (induct a arbitrary: c' cref' bits rule: resolve_address_bits'.induct)
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)
apply (erule valid_CNodeCapE; fastforce simp: cte_level_bits_def)
subgoal premises prems for s s' x
apply (insert prems)
apply (rule context_conjI)

4
proof/refine/ARM/IpcCancel_R.thy
View File

@ -697,8 +697,8 @@ lemma cancelSignal_invs':
apply (clarsimp split: if_split_asm)
subgoal
by (fastforce simp: symreftype_inverse' ntfn_bound_refs'_def
tcb_bound_refs'_def ntfn_q_refs_of'_def
split: ntfn.splits)
tcb_bound_refs'_def ntfn_q_refs_of'_def obj_at'_def projectKOs
split: ntfn.splits option.splits)
subgoal
by (fastforce simp: symreftype_inverse' ntfn_bound_refs'_def
tcb_bound_refs'_def)

2
proof/refine/ARM/Tcb_R.thy
View File

@ -1110,7 +1110,7 @@ definition valid_tcb_invocation :: "tcbinvocation \<Rightarrow> bool" where
lemma arch_tcb_set_ipc_buffer_corres:
"corres dc (tcb_at target) (tcb_at' target) (arch_tcb_set_ipc_buffer target ptr) (asUser target $ setTCBIPCBuffer ptr)"
apply (simp add: setTCBIPCBuffer_def ARM_H.tpidrurwRegister_def ARM.tpidrurwRegister_def)
apply (simp add: setTCBIPCBuffer_def)
apply (rule user_setreg_corres)
done

2
proof/refine/ARM/Untyped_R.thy
View File

@ -223,7 +223,7 @@ next
apply (clarsimp simp: cte_map_def)
apply (subst of_bl_nat_to_cref)
apply simp
apply simp
apply (simp add: word_bits_def)
apply (subst S)
apply simp
apply simp

2
proof/refine/ARM_HYP/ADT_H.thy
View File

@ -306,7 +306,7 @@ lemma ArchFaultMap_arch_fault_map: "ArchFaultMap (arch_fault_map f) = f"
lemma FaultMap_fault_map[simp]:
"valid_fault ft \<Longrightarrow> FaultMap (fault_map ft) = ft"
apply (case_tac ft, simp_all)
apply (simp add: valid_fault_def LookupFailureMap_lookup_failure_map)
apply (simp add: valid_fault_def LookupFailureMap_lookup_failure_map word_bits_def)
apply (rule ArchFaultMap_arch_fault_map)
done

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

@ -242,9 +242,9 @@ lemma pac_corres:
updateFreeIndex_caps_overlap_reserved
| simp add: descendants_of_null_filter' split del: if_split)+
apply (wp get_cap_wp)+
apply (subgoal_tac "word1 && ~~ mask pageBits = word1 \<and> pageBits \<le> word_bits \<and> 2 \<le> pageBits")
apply (subgoal_tac "word1 && ~~ mask pageBits = word1 \<and> pageBits \<le> word_bits \<and> word_size_bits \<le> pageBits")
prefer 2
apply (clarsimp simp:pageBits_def word_bits_def is_aligned_neg_mask_eq)
apply (clarsimp simp:pageBits_def word_bits_def is_aligned_neg_mask_eq word_size_bits_def)
apply (simp only:delete_objects_rewrite)
apply wp+
apply (clarsimp simp: conj_comms)

2
proof/refine/ARM_HYP/CNodeInv_R.thy
View File

@ -99,7 +99,7 @@ lemma cap_relation_NullCap:
split del: if_split)
apply simp
apply simp
apply (clarsimp simp: word_size word_size_def)
apply (clarsimp simp: word_size word_size_def cteRightsBits_def cteGuardBits_def)
apply (clarsimp simp: ARM_HYP_H.updateCapData_def isCap_simps split del: if_split)
done

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

@ -456,7 +456,8 @@ proof -
ARM_HYP_H.updateCapData_def)[6]
-- CNodeCap
apply (simp add: simps word_bits_def the_cnode_cap_def andCapRights_def
rightsFromWord_def data_to_rights_def nth_ucast)
rightsFromWord_def data_to_rights_def nth_ucast cteRightsBits_def
cteGuardBits_def)
apply (insert x)
apply (subgoal_tac "unat ((x >> 3) && mask 5) < unat (2^5::word32)")
prefer 2
@ -627,7 +628,7 @@ proof (induct a arbitrary: c' cref' bits rule: resolve_address_bits'.induct)
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)
apply (erule valid_CNodeCapE; fastforce simp: cte_level_bits_def)
subgoal premises prems for s s' x
apply (insert prems)
apply (rule context_conjI)

2
proof/refine/ARM_HYP/Tcb_R.thy
View File

@ -1102,7 +1102,7 @@ definition valid_tcb_invocation :: "tcbinvocation \<Rightarrow> bool" where
lemma arch_tcb_set_ipc_buffer_corres:
"corres dc (tcb_at target) (tcb_at' target) (arch_tcb_set_ipc_buffer target ptr) (asUser target $ setTCBIPCBuffer ptr)"
apply (simp add: setTCBIPCBuffer_def ARM_HYP_H.tpidrurwRegister_def ARM_HYP.tpidrurwRegister_def)
apply (simp add: setTCBIPCBuffer_def)
apply (rule user_setreg_corres)
done

2
proof/refine/ARM_HYP/Untyped_R.thy
View File

@ -224,7 +224,7 @@ next
apply (clarsimp simp: cte_map_def)
apply (subst of_bl_nat_to_cref)
apply simp
apply simp
apply (simp add: word_bits_def)
apply (subst S)
apply simp
apply simp

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

@ -2138,7 +2138,7 @@ definition
checkActiveIRQ :: "(kernel_state, bool) nondet_monad"
where
"checkActiveIRQ \<equiv>
do irq \<leftarrow> doMachineOp getActiveIRQ;
do irq \<leftarrow> doMachineOp (getActiveIRQ False);
return (irq \<noteq> None)
od"

59
proof/refine/X64/ArchAcc_R.thy
View File

@ -1356,7 +1356,7 @@ lemma getPTE_wp:
projectKOs in_monad valid_def obj_at'_def objBits_simps)
lemma pdpt_at_lift:
"\<forall>s s'. (s, s') \<in> state_relation \<longrightarrow>
"corres_inst_eq ptr ptr' \<Longrightarrow> \<forall>s s'. (s, s') \<in> state_relation \<longrightarrow> True \<longrightarrow>
(pspace_aligned s \<and> valid_pml4e (X64_A.PDPointerTablePML4E ptr x z) s \<and> (ptrFromPAddr ptr) = ptr') \<longrightarrow>
pspace_distinct' s' \<longrightarrow> pd_pointer_table_at' ptr' s'"
by (fastforce intro!: pd_pointer_table_at_state_relation)
@ -1366,7 +1366,7 @@ lemmas checkPDPTAt_corres[corresK] =
lemma lookup_pdpt_slot_corres:
"corres (lfr \<oplus> op =)
(pspace_aligned and valid_arch_objs and page_map_l4_at pml4
(pspace_aligned and valid_vspace_objs and page_map_l4_at pml4
and (\<exists>\<rhd>pml4) and
K (is_aligned pml4 pml4_bits \<and> vptr < pptr_base \<and> canonical_address vptr))
(pspace_aligned' and pspace_distinct')
@ -1396,7 +1396,7 @@ crunch distict'[wp]: lookupPDPTSlot, lookupPDSlot pspace_distinct'
(wp: getPML4E_wp getPDPTE_wp hoare_drop_imps ignore: getObject)
lemma pd_at_lift:
"\<forall>s s'. (s, s') \<in> state_relation \<longrightarrow>
"corres_inst_eq ptr ptr' \<Longrightarrow> \<forall>s s'. (s, s') \<in> state_relation \<longrightarrow> True \<longrightarrow>
(pspace_aligned s \<and> valid_pdpte (X64_A.PageDirectoryPDPTE ptr x z) s \<and> (ptrFromPAddr ptr) = ptr') \<longrightarrow>
pspace_distinct' s' \<longrightarrow> page_directory_at' ptr' s'"
by (fastforce intro!: page_directory_at_state_relation)
@ -1405,20 +1405,20 @@ lemmas checkPDAt_corres[corresK] =
corres_stateAssert_implied_frame[OF pd_at_lift, folded checkPDAt_def]
lemma get_pdpte_valid[wp]:
"\<lbrace>valid_arch_objs and \<exists>\<rhd> (x && ~~ mask pdpt_bits)\<rbrace>
"\<lbrace>valid_vspace_objs and \<exists>\<rhd> (x && ~~ mask pdpt_bits)\<rbrace>
get_pdpte x
\<lbrace>valid_pdpte\<rbrace>"
apply (simp add: get_pdpte_def)
apply wp
apply clarsimp
apply (drule (2) valid_arch_objsD)
apply (drule (2) valid_vspace_objsD)
apply simp
done
lemma lookup_pd_slot_corres:
"corres (lfr \<oplus> op =)
(pspace_aligned and valid_arch_objs and valid_arch_state and equal_kernel_mappings
(pspace_aligned and valid_vspace_objs and valid_arch_state and equal_kernel_mappings
and valid_global_objs and (\<exists>\<rhd> pml4) and page_map_l4_at pml4 and
K (canonical_address vptr \<and> is_aligned pml4 pml4_bits \<and> vptr < pptr_base))
(pspace_aligned' and pspace_distinct')
@ -1443,7 +1443,7 @@ lemma lookup_pd_slot_corres:
done
lemma pt_at_lift:
"\<forall>s s'. (s, s') \<in> state_relation \<longrightarrow>
"corres_inst_eq ptr ptr' \<Longrightarrow> \<forall>s s'. (s, s') \<in> state_relation \<longrightarrow> True \<longrightarrow>
(pspace_aligned s \<and> valid_pde (X64_A.PageTablePDE ptr x z) s \<and> (ptrFromPAddr ptr) = ptr') \<longrightarrow>
pspace_distinct' s' \<longrightarrow> page_table_at' ptr' s'"
by (fastforce intro!: page_table_at_state_relation)
@ -1452,19 +1452,19 @@ lemmas checkPTAt_corres[corresK] =
corres_stateAssert_implied_frame[OF pt_at_lift, folded checkPTAt_def]
lemma get_pde_valid[wp]:
"\<lbrace>valid_arch_objs and \<exists>\<rhd> (x && ~~ mask pd_bits)\<rbrace>
"\<lbrace>valid_vspace_objs and \<exists>\<rhd> (x && ~~ mask pd_bits)\<rbrace>
get_pde x
\<lbrace>valid_pde\<rbrace>"
apply (simp add: get_pde_def)
apply wp
apply clarsimp
apply (drule (2) valid_arch_objsD)
apply (drule (2) valid_vspace_objsD)
apply simp
done
lemma lookup_pt_slot_corres:
"corres (lfr \<oplus> op =)
(pspace_aligned and valid_arch_objs and valid_arch_state and equal_kernel_mappings
(pspace_aligned and valid_vspace_objs and valid_arch_state and equal_kernel_mappings
and valid_global_objs and (\<exists>\<rhd> pml4) and page_map_l4_at pml4 and
K (canonical_address vptr \<and> is_aligned pml4 pml4_bits \<and> vptr < pptr_base))
(pspace_aligned' and pspace_distinct')
@ -1538,28 +1538,21 @@ lemma corres_gets_global_pml4 [corres]:
"corres (op =) \<top> \<top> (gets (x64_global_pml4 \<circ> arch_state)) (gets (x64KSGlobalPML4 \<circ> ksArchState))"
by (simp add: state_relation_def arch_state_relation_def)
lemma copy_global_mappings_corres [corres]:
assumes "pm' = pm"
notes [corresK] =
corresK_mapM_x[where S="op =" and F="op ="
and I="\<lambda>xs s. pspace_aligned s \<and> valid_etcbs s
\<and> (\<forall>x\<in>set xs. pml4e_at (g_pm + (x << word_size_bits)) s
\<and> pml4e_at (pm + (x << word_size_bits)) s)"
and I'="\<lambda>ys s. \<forall>y\<in>set ys. pml4e_at' (g_pm' + (y << word_size_bits)) s
\<and> pml4e_at' (pm + (y << word_size_bits)) s"
for g_pm g_pm']
shows "corres dc (valid_arch_state and valid_etcbs and pspace_aligned and page_map_l4_at pm)
(valid_arch_state' and page_map_l4_at' pm')
lemma copy_global_mappings_corres [@lift_corres_args, corres]:
"corres dc (valid_arch_state and valid_etcbs and pspace_aligned and page_map_l4_at pm)
(valid_arch_state' and page_map_l4_at' pm)
(copy_global_mappings pm)
(copyGlobalMappings pm')"
apply (simp add: assms copy_global_mappings_def copyGlobalMappings_def
objBits_simps archObjSize_def pptr_base_def)
(copyGlobalMappings pm)" (is "corres _ ?apre _ _ _")
unfolding copy_global_mappings_def copyGlobalMappings_def objBits_simps archObjSize_def pptr_base_def
apply (fold word_size_bits_def)
apply corressimp
apply (rule corres_rv_defer_left, fastforce)
apply (wpsimp wp: hoare_vcg_ball_lift abs_atyp_at_lifts[OF store_pml4e_typ_at]
simp: list.rel_eq)+
apply (subst word64_less_sub_le, fastforce simp: bit_simps word_bits_def)+
apply (rule_tac P="page_map_l4_at global_pm and ?apre" and
P'="page_map_l4_at' globalPM and page_map_l4_at' pm"
in corresK_mapM_x[OF order_refl])
apply (corressimp simp: objBits_def mask_def wp: get_pde_wp getPDE_wp)+
apply(rule conjI)
subgoal by (auto intro!: page_map_l4_pml4e_atI page_map_l4_pml4e_atI'
simp: page_bits_def le_less_trans ptTranslationBits_def)
by (auto simp: valid_arch_state_def valid_arch_state'_def
elim: page_map_l4_pml4e_atI page_map_l4_pml4e_atI')
@ -1643,7 +1636,7 @@ lemma create_mapping_entries_corres:
"\<lbrakk> vm_rights' = vmrights_map vm_rights;
attrib' = vmattributes_map attrib \<rbrakk>
\<Longrightarrow> corres (ser \<oplus> mapping_map)
(valid_arch_objs and pspace_aligned and valid_arch_state and valid_global_objs and
(valid_vspace_objs and pspace_aligned and valid_arch_state and valid_global_objs and
equal_kernel_mappings and \<exists>\<rhd> pml4 and page_map_l4_at pml4 and
K (is_aligned pml4 pml4_bits \<and> vmsz_aligned vptr pgsz \<and> vptr < pptr_base
\<and> vm_rights \<in> valid_vm_rights \<and> canonical_address vptr))
@ -1813,7 +1806,7 @@ lemma find_vspace_for_asid_corres:
assumes "asid' = asid"
shows "corres (lfr \<oplus> op =)
((\<lambda>s. valid_arch_state s \<or> vspace_at_asid_ex asid s)
and valid_arch_objs and pspace_aligned
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_vspace_for_asid asid) (findVSpaceForASID asid')"
@ -1875,7 +1868,7 @@ lemma find_vspace_for_asid_corres:
arch_kernel_obj.splits)
apply (clarsimp dest!: vs_lookup1D)
apply (clarsimp dest!: vs_lookup1D)
apply (drule(1) valid_arch_objsD[rotated])
apply (drule(1) valid_vspace_objsD[rotated])
apply (rule vs_lookupI)
apply (rule vs_asid_refsI)
apply simp
@ -1888,7 +1881,7 @@ lemma find_vspace_for_asid_corres:
lemma find_vspace_for_asid_corres':
assumes "asid' = asid"
shows "corres (lfr \<oplus> op =)
(vspace_at_asid_ex asid and valid_arch_objs
(vspace_at_asid_ex asid 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_vspace_for_asid asid) (findVSpaceForASID asid')"

39
proof/refine/X64/Arch_R.thy
View File

@ -571,7 +571,7 @@ lemma userVTop_conv[simp]: "userVTop = user_vtop"
by (simp add: userVTop_def user_vtop_def)
lemma find_vspace_for_asid_lookup_slot [wp]:
"\<lbrace>pspace_aligned and valid_arch_objs\<rbrace>
"\<lbrace>pspace_aligned and valid_vspace_objs\<rbrace>
find_vspace_for_asid asid
\<lbrace>\<lambda>rv. \<exists>\<rhd> (lookup_pml4_slot rv vptr && ~~ mask pml4_bits)\<rbrace>, -"
apply (rule hoare_pre)
@ -619,7 +619,7 @@ lemma decode_page_inv_corres:
apply (rule corres_splitEE)
prefer 2
apply (rule corres_lookup_error)
apply (rule_tac P="valid_arch_state and valid_arch_objs and
apply (rule_tac P="valid_arch_state and valid_vspace_objs and
pspace_aligned and equal_kernel_mappings and valid_global_objs and
valid_cap (cap.ArchObjectCap
(arch_cap.PML4Cap wd (Some optv)))"
@ -629,7 +629,7 @@ lemma decode_page_inv_corres:
apply (simp add: mask_def)
apply assumption
apply (rule whenE_throwError_corres, simp, simp)
apply (rule_tac R="\<lambda>_ s. valid_arch_objs s \<and> pspace_aligned s
apply (rule_tac R="\<lambda>_ s. valid_vspace_objs s \<and> pspace_aligned s
\<and> (hd args && user_vtop) + (2 ^ pageBitsForSize sz - 1) \<le> user_vtop \<and>
valid_arch_state s \<and> equal_kernel_mappings s \<and> valid_global_objs s \<and>
s \<turnstile> (fst (hd excaps)) \<and> (\<exists>\<rhd> (lookup_pml4_slot (obj_ref_of (fst (hd excaps))) (hd args) && ~~ mask pml4_bits)) s \<and>
@ -722,7 +722,7 @@ lemma decode_page_inv_corres:
apply (rule corres_returnOk)
apply (clarsimp simp: archinv_relation_def page_invocation_map_def)
apply (wp)+
apply (subgoal_tac "valid_arch_objs s \<and> pspace_aligned s \<and>
apply (subgoal_tac "valid_vspace_objs s \<and> pspace_aligned s \<and>
(snd v') < pptr_base \<and> canonical_address (snd v') \<and>
equal_kernel_mappings s \<and> valid_global_objs s \<and> valid_arch_state s \<and>
(*(\<exists>\<rhd> (lookup_pml4_slot (fst pa) (snd v') && ~~ mask pml4_bits)) s \<and>*)
@ -813,7 +813,7 @@ lemma decode_page_table_inv_corres:
| wp hoare_whenE_wp hoare_vcg_all_lift_R getPDE_wp get_pde_wp
| wp_once hoare_drop_imps)+)[6]
apply (clarsimp intro!: validE_R_validE)
apply (rule_tac Q'="\<lambda>rv s. pspace_aligned s \<and> valid_arch_objs s \<and> valid_arch_state s \<and>
apply (rule_tac Q'="\<lambda>rv s. pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and>
equal_kernel_mappings s \<and> valid_global_objs s \<and>
(\<exists>ref. (ref \<rhd> rv) s) \<and> typ_at (AArch APageMapL4) rv s \<and>
is_aligned rv pml4_bits"
@ -915,7 +915,7 @@ lemma decode_page_directory_inv_corres:
| wp hoare_whenE_wp hoare_vcg_all_lift_R getPDPTE_wp get_pdpte_wp
| wp_once hoare_drop_imps)+)[6]
apply (clarsimp intro!: validE_R_validE)
apply (rule_tac Q'="\<lambda>rv s. pspace_aligned s \<and> valid_arch_objs s \<and> valid_arch_state s \<and>
apply (rule_tac Q'="\<lambda>rv s. pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and>
equal_kernel_mappings s \<and> valid_global_objs s \<and>
(\<exists>ref. (ref \<rhd> rv) s) \<and> typ_at (AArch APageMapL4) rv s \<and>
is_aligned rv pml4_bits"
@ -1359,22 +1359,29 @@ lemma corresK_machine_op[corresK]: "corres_underlyingK Id False True F r P Q x x
apply (clarsimp simp add: corres_underlyingK_def)
by (erule corres_machine_op)
lemma port_in_corres:
lemma port_in_corres[corres]:
"no_fail \<top> a \<Longrightarrow> corres dc (einvs and ct_active) (invs' and ct_active') (port_in a) (portIn a)"
apply (clarsimp simp: port_in_def portIn_def)
apply (corressimp corres: gct_corres set_mrs_corres set_mi_corres)
apply (rule corresK_drop, rule corres_Id[where r="op ="], simp, simp, simp)
apply (corressimp corres: gct_corres set_mrs_corres set_mi_corres)+
by (clarsimp simp: invs_def invs'_def cur_tcb_def cur_tcb'_def)
apply (rule corres_guard_imp)
apply (rule corres_split_eqr[OF _ gct_corres])
apply (rule corres_split_eqr)
apply (rule corres_split_eqr[OF set_mi_corres set_mrs_corres])
apply wpsimp+
apply (rule corres_machine_op[OF corres_Id], simp+)
apply wpsimp+
done
lemma port_out_corres:
lemma port_out_corres[@lift_corres_args, corres]:
"no_fail \<top> (a w) \<Longrightarrow> corres dc (einvs and ct_active) (invs' and ct_active')
(port_out a w) (portOut a w)"
apply (clarsimp simp: port_out_def portOut_def)
apply (corressimp corres: gct_corres set_mrs_corres set_mi_corres)
apply (rule corresK_drop, rule corres_Id[where r="op ="], simp, simp, simp)
apply (corressimp corres: gct_corres set_mrs_corres set_mi_corres)+
by (clarsimp simp: invs_def invs'_def cur_tcb_def cur_tcb'_def)
apply (rule corres_guard_imp)
apply (rule corres_split_eqr[OF _ gct_corres])
apply (rule corres_split_eqr[OF set_mi_corres])
apply wpsimp+
apply (rule corres_machine_op[OF corres_Id], simp+)
apply wpsimp+
done
(* FIXME x64: move *)
lemma no_fail_in8[wp]:

7
proof/refine/X64/CNodeInv_R.thy
View File

@ -99,7 +99,8 @@ lemma cap_relation_NullCap:
split del: if_split)
apply simp
apply simp
apply (clarsimp simp: word_size word_size_def cnode_padding_bits_def cnode_guard_size_bits_def)
apply (clarsimp simp: word_size word_size_def cnode_padding_bits_def cnode_guard_size_bits_def
cteRightsBits_def cteGuardBits_def)
apply (clarsimp simp: X64_H.updateCapData_def isCap_simps split del: if_split)
done
@ -596,7 +597,7 @@ text {* Various proofs about the two recursive deletion operations.
text {* Proving the termination of rec_del *}
crunch typ_at[wp]: cancel_ipc "\<lambda>s. P (typ_at T p s)"
(wp: crunch_wps hoare_vcg_split_ifE simp: crunch_simps)
(wp: crunch_wps hoare_vcg_if_splitE simp: crunch_simps)
declare if_split [split]
@ -610,7 +611,7 @@ declare word_unat_power [symmetric, simp del]
(* FIXME: move *)
lemma finalise_cap_not_reachable_pg_cap:
"\<lbrace>pspace_aligned and
valid_arch_objs and
valid_vspace_objs and
valid_objs and valid_arch_state and
cte_wp_at (op = cap) slot and
(\<lambda>s. valid_asid_table (x64_asid_table (arch_state s)) s)

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

@ -449,7 +449,7 @@ proof -
X64_H.updateCapData_def)
-- CNodeCap
apply (simp add: simps word_bits_def the_cnode_cap_def andCapRights_def
rightsFromWord_def data_to_rights_def nth_ucast)
rightsFromWord_def data_to_rights_def nth_ucast cteRightsBits_def cteGuardBits_def)
apply (insert x)
apply (subgoal_tac "unat ((x >> 2) && mask 6) < unat (2^6::machine_word)")
prefer 2

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

@ -2844,7 +2844,7 @@ lemma setUntypedCapAsFull_if_live_then_nonz_cap':
apply (clarsimp simp:if_live_then_nonz_cap'_def)
apply (wp hoare_vcg_all_lift hoare_vcg_imp_lift)
apply (clarsimp simp:setUntypedCapAsFull_def split del: if_split)
apply (wp hoare_vcg_split_if)
apply (wp hoare_vcg_if_split)
apply (clarsimp simp:ex_nonz_cap_to'_def cte_wp_at_ctes_of)
apply (wp updateCap_ctes_of_wp)+
apply clarsimp

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

@ -9,7 +9,7 @@
*)
theory Corres
imports StateRelation "../../../lib/Corres_Method"
imports StateRelation "../../../lib/CorresK_Lemmas"
begin
text {* Instantiating the corres framework to this particular state relation. *}

5
proof/refine/X64/Detype_R.thy
View File

@ -648,10 +648,13 @@ lemma cNodeNoPartialOverlap:
apply wp+
done
declare wrap_ext_det_ext_ext_def[simp]
lemma sym_refs_hyp_refs_triv[simp]: "sym_refs (state_hyp_refs_of s)"
apply (clarsimp simp: state_hyp_refs_of_def sym_refs_def)
by (case_tac "kheap s x"; simp)
lemma detype_corres:
"is_aligned base magnitude \<Longrightarrow> magnitude \<ge> 3 \<Longrightarrow>
corres dc

14
proof/refine/X64/Ipc_R.thy
View File

@ -2005,8 +2005,8 @@ crunch nosch[wp]: doIPCTransfer "\<lambda>s. P (ksSchedulerAction s)"
simp: split_def zipWithM_x_mapM)
lemma sanitise_register_corres:
"foldl (\<lambda>s (a, b) c. if c = a then sanitise_register t' a b else s c) s (zip msg_template msg) =
foldl (\<lambda>s (a, b) c. if c = a then sanitiseRegister t'a a b else s c) s (zip msg_template msg)"
"foldl (\<lambda>s (a, b). s ( a := sanitise_register t' a b)) s (zip msg_template msg) =
foldl (\<lambda>s (a, b). s ( a := sanitiseRegister t'a a b)) s (zip msg_template msg)"
apply (rule foldl_cong)
apply simp
apply simp
@ -2018,7 +2018,7 @@ lemma sanitise_register_corres:
lemma handle_fault_reply_registers_corres:
"corres (op =) (tcb_at t) (tcb_at' t)
(do t' \<leftarrow> thread_get id t;
(do t' \<leftarrow> arch_get_sanitise_register_info t;
y \<leftarrow> as_user t
(zipWithM_x
(\<lambda>r v. set_register r
@ -2026,7 +2026,7 @@ lemma handle_fault_reply_registers_corres:
msg_template msg);
return (label = 0)
od)
(do t' \<leftarrow> threadGet id t;
(do t' \<leftarrow> getSanitiseRegisterInfo t;
y \<leftarrow> asUser t
(zipWithM_x
(\<lambda>r v. setRegister r (sanitiseRegister t' r v))
@ -2034,14 +2034,14 @@ lemma handle_fault_reply_registers_corres:
return (label = 0)
od)"
apply (rule corres_guard_imp)
apply (rule corres_split [OF _ threadget_corres, where r'=tcb_relation])
apply (clarsimp simp: arch_get_sanitise_register_info_def getSanitiseRegisterInfo_def)
apply (rule corres_split)
apply (rule corres_trivial, simp)
apply (rule corres_as_user')
apply(simp add: set_register_def setRegister_def syscallMessage_def)
apply(subst zipWithM_x_modify)+
apply(rule corres_modify')
apply (simp add: sanitise_register_corres|wp)+
apply (clarsimp simp: sanitise_register_corres|wp)+
done
lemma handle_fault_reply_corres:
@ -4167,7 +4167,7 @@ lemma ri_invs' [wp]:
apply (rule hoare_seq_ext [OF _ gbn_sp'])
apply (rule hoare_seq_ext)
(* set up precondition for old proof *)
apply (rule_tac R="ko_at' ep (capEPPtr cap) and ?pre" in hoare_vcg_split_if)
apply (rule_tac R="ko_at' ep (capEPPtr cap) and ?pre" in hoare_vcg_if_split)
apply (wp completeSignal_invs)
apply (case_tac ep)
-- "endpoint = RecvEP"

8
proof/refine/X64/Machine_R.thy
View File

@ -43,7 +43,7 @@ lemma irq_state_independent_H_disjI[intro]:
context begin interpretation Arch . (*FIXME: arch_split*)
lemma dmo_getirq_inv[wp]:
"irq_state_independent_H P \<Longrightarrow> \<lbrace>P\<rbrace> doMachineOp getActiveIRQ \<lbrace>\<lambda>rv. P\<rbrace>"
"irq_state_independent_H P \<Longrightarrow> \<lbrace>P\<rbrace> doMachineOp (getActiveIRQ in_kernel) \<lbrace>\<lambda>rv. P\<rbrace>"
apply (simp add: getActiveIRQ_def doMachineOp_def split_def exec_gets
select_f_select[simplified liftM_def]
select_modify_comm gets_machine_state_modify)
@ -52,7 +52,7 @@ lemma dmo_getirq_inv[wp]:
done
lemma getActiveIRQ_masked:
"\<lbrace>\<lambda>s. valid_irq_masks' table (irq_masks s)\<rbrace> getActiveIRQ
"\<lbrace>\<lambda>s. valid_irq_masks' table (irq_masks s)\<rbrace> getActiveIRQ in_kernel
\<lbrace>\<lambda>rv s. \<forall>irq. rv = Some irq \<longrightarrow> table irq \<noteq> IRQInactive\<rbrace>"
apply (simp add: getActiveIRQ_def)
apply wp
@ -87,7 +87,7 @@ lemma setIRQState_irq_states':
done
lemma getActiveIRQ_le_maxIRQ:
"\<lbrace>irqs_masked' and valid_irq_states'\<rbrace> doMachineOp getActiveIRQ \<lbrace>\<lambda>rv s. \<forall>x. rv = Some x \<longrightarrow> x \<le> maxIRQ\<rbrace>"
"\<lbrace>irqs_masked' and valid_irq_states'\<rbrace> doMachineOp (getActiveIRQ in_kernel) \<lbrace>\<lambda>rv s. \<forall>x. rv = Some x \<longrightarrow> x \<le> maxIRQ\<rbrace>"
apply (simp add: doMachineOp_def split_def)
apply wp
apply clarsimp
@ -99,7 +99,7 @@ lemma getActiveIRQ_le_maxIRQ:
(* FIXME: follows already from getActiveIRQ_le_maxIRQ *)
lemma getActiveIRQ_neq_Some0xFF:
"\<lbrace>\<top>\<rbrace> doMachineOp getActiveIRQ \<lbrace>\<lambda>rv s. rv \<noteq> Some 0x3FF\<rbrace>"
"\<lbrace>\<top>\<rbrace> doMachineOp (getActiveIRQ in_kernel) \<lbrace>\<lambda>rv s. rv \<noteq> Some 0x3FF\<rbrace>"
apply (simp add: doMachineOp_def split_def)
apply wp
apply clarsimp

3
proof/refine/X64/Refine.thy
View File

@ -603,7 +603,8 @@ lemma kernel_corres:
apply (simp add: invs'_def valid_state'_def)
apply (rule corres_split [OF _ schedule_corres])
apply (rule activate_corres)
apply (wp schedule_invs' hoare_vcg_if_lift2 hoare_drop_imps |simp)+
apply (wp schedule_invs' hoare_vcg_if_lift2 hoare_drop_imps
handle_interrupt_valid_sched[unfolded non_kernel_IRQs_def, simplified] |simp)+
apply (rule_tac Q="\<lambda>_. valid_sched and invs and valid_list" and E="\<lambda>_. valid_sched and invs and valid_list"
in hoare_post_impErr)
apply (wp handle_event_valid_sched |simp)+

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

@ -5847,12 +5847,12 @@ lemma corres_retype_region_createNewCaps:
-- "PML4"
apply (corressimp corres: corres_retype[where ty="Inr PML4Object" and 'a=pml4e and sz=sz,
simplified, folded retype_region2_retype_region_PML4Obj]
corresK: corresK_mapM_x[where S="op =" and F="op ="
and I="\<lambda>xs s. valid_arch_state s \<and> pspace_aligned s
\<and> valid_etcbs s
\<and> (\<forall>x \<in> set xs. page_map_l4_at x s)"
and I'="\<lambda>ys s. valid_arch_state' s
\<and> (\<forall>y \<in> set ys. page_map_l4_at' y s)"]
corresK: corresK_mapM_x_list_all2[where I="\<lambda>xs s. valid_arch_state s \<and> pspace_aligned s
\<and> valid_etcbs s \<and>
(\<forall>x \<in> set xs. page_map_l4_at x s)"
and I'="\<lambda>xs s. valid_arch_state' s \<and>
(\<forall>x \<in> set xs. page_map_l4_at' x s)"
and S="op ="]
wp: copy_global_mappings_typ_at hoare_vcg_ball_lift retype_region_pml4_at
retype_region_valid_arch[where sz=sz] retype_region_aligned[where sz=sz]
createObjects_valid_arch[where sz=sz] createObjects_pml4_at[where sz=sz]

10
proof/refine/X64/Schedule_R.thy
View File

@ -218,7 +218,7 @@ declare objBitsT_koTypeOf [simp]
lemma arch_switch_thread_corres:
"corres dc (valid_arch_state and valid_objs and valid_asid_map
and valid_arch_objs and pspace_aligned and pspace_distinct
and valid_vspace_objs and pspace_aligned and pspace_distinct
and valid_vs_lookup and valid_global_objs
and unique_table_refs o caps_of_state
and st_tcb_at runnable t)
@ -509,7 +509,7 @@ lemma setQueue_ksReadyQueues_lift:
setQueue d p ts
\<lbrace> \<lambda>_ s. P s (ksReadyQueues s (d,p))\<rbrace>"
unfolding setQueue_def
by (wp, clarsimp simp: fun_upd_def)
by (wp, clarsimp simp: fun_upd_def cong: if_cong)
lemma tcbSchedDequeue_valid_queues'[wp]:
"\<lbrace>valid_queues' and tcb_at' t\<rbrace>
@ -943,7 +943,7 @@ crunch valid_queues[wp]: "Arch.switchToThread" "Invariants_H.valid_queues"
lemma switch_thread_corres:
"corres dc (valid_arch_state and valid_objs and valid_asid_map
and valid_arch_objs and pspace_aligned and pspace_distinct
and valid_vspace_objs and pspace_aligned and pspace_distinct
and valid_vs_lookup and valid_global_objs
and unique_table_refs o caps_of_state
and st_tcb_at runnable t and valid_etcbs)
@ -2216,7 +2216,7 @@ lemma gts_exs_valid[wp]:
lemma guarded_switch_to_corres:
"corres dc (valid_arch_state and valid_objs and valid_asid_map
and valid_arch_objs and pspace_aligned and pspace_distinct
and valid_vspace_objs and pspace_aligned and pspace_distinct
and valid_vs_lookup and valid_global_objs
and unique_table_refs o caps_of_state
and st_tcb_at runnable t and valid_etcbs)
@ -2626,7 +2626,7 @@ lemma schedule_corres:
apply ((wp thread_get_wp' hoare_vcg_conj_lift hoare_drop_imps | clarsimp)+)
apply (rule conjI,simp)
apply (clarsimp split: Deterministic_A.scheduler_action.splits
simp: invs_psp_aligned invs_distinct invs_valid_objs invs_arch_state invs_arch_objs)
simp: invs_psp_aligned invs_distinct invs_valid_objs invs_arch_state invs_vspace_objs)
apply (intro impI conjI allI tcb_at_invs |
(fastforce simp: invs_def cur_tcb_def valid_arch_caps_def valid_etcbs_def
valid_sched_def valid_sched_action_def is_activatable_def

4
proof/refine/X64/Syscall_R.thy
View File

@ -2179,9 +2179,7 @@ lemma hh_corres:
(invs' and sch_act_not thread
and (\<lambda>s. \<forall>p. thread \<notin> set(ksReadyQueues s p))
and st_tcb_at' simple' thread and ex_nonz_cap_to' thread)
(do y \<leftarrow> handle_hypervisor_fault w fault;
return ()
od) (handleHypervisorFault w fault)"
(handle_hypervisor_fault w fault) (handleHypervisorFault w fault)"
apply (cases fault; clarsimp simp add: handleHypervisorFault_def returnOk_def2)
done

4
proof/refine/X64/TcbAcc_R.thy
View File

@ -200,7 +200,7 @@ lemma dmo_lift':
lemma doMachineOp_getActiveIRQ_IRQ_active:
"\<lbrace>valid_irq_states'\<rbrace>
doMachineOp getActiveIRQ
doMachineOp (getActiveIRQ in_kernel)
\<lbrace>\<lambda>rv s. \<forall>irq. rv = Some irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq \<noteq> IRQInactive\<rbrace>"
apply (rule hoare_lift_Pf3 [where f="ksInterruptState"])
prefer 2
@ -213,7 +213,7 @@ lemma doMachineOp_getActiveIRQ_IRQ_active:
lemma doMachineOp_getActiveIRQ_IRQ_active':
"\<lbrace>valid_irq_states'\<rbrace>
doMachineOp getActiveIRQ
doMachineOp (getActiveIRQ in_kernel)
\<lbrace>\<lambda>rv s. rv = Some irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq \<noteq> IRQInactive\<rbrace>"
apply (rule hoare_post_imp)
prefer 2

223
proof/refine/X64/Tcb_R.thy
View File

@ -320,37 +320,54 @@ lemma readreg_corres:
crunch sch_act_simple [wp]: asUser "sch_act_simple"
(rule: sch_act_simple_lift)
lemma invs_valid_queues':
"invs' s \<longrightarrow> valid_queues' s"
by (clarsimp simp: invs'_def valid_state'_def)
declare invs_valid_queues'[rule_format, elim!]
lemma einvs_valid_etcbs: "einvs s \<longrightarrow> valid_etcbs s"
by (clarsimp simp: valid_sched_def)
lemma writereg_corres:
"corres (intr \<oplus> op =) (einvs and tcb_at dest and ex_nonz_cap_to dest)
(invs' and sch_act_simple and tcb_at' dest and ex_nonz_cap_to' dest)
(invoke_tcb (tcb_invocation.WriteRegisters dest resume values arch))
(invokeTCB (tcbinvocation.WriteRegisters dest resume values arch'))"
apply (simp add: invokeTCB_def performTransfer_def
sanitiseRegister_def sanitise_register_def
apply (simp add: invokeTCB_def performTransfer_def arch_get_sanitise_register_info_def
sanitiseRegister_def sanitise_register_def getSanitiseRegisterInfo_def
frameRegisters_def gpRegisters_def)
apply (rule corres_guard_imp)
apply (rule corres_split [OF _ gct_corres])
apply (rule corres_split [OF _ threadget_corres, where r'=tcb_relation])
apply (rule corres_split_nor)
prefer 2
apply (rule corres_as_user)
apply (simp add: zipWithM_mapM getRestartPC_def setNextPC_def)
apply (rule corres_Id)
apply (clarsimp simp: sanitise_or_flags_def sanitise_and_flags_def
sanitiseOrFlags_def sanitiseAndFlags_def
mask_def user_vtop_def
cong: if_cong)
apply simp
apply (rule no_fail_pre, wp no_fail_mapM)
apply (clarsimp simp: sanitiseOrFlags_def sanitiseAndFlags_def)
apply ((safe)[1], (wp no_fail_setRegister | simp)+)
apply (rule corres_split_nor)
apply (rule_tac P=\<top> and P'=\<top> in corres_inst)
apply simp
apply (rule corres_when [OF refl])
apply (rule restart_corres)
apply (wp static_imp_wp | clarsimp simp: invs'_def valid_state'_def
dest!: global'_no_ex_cap)+
apply (rule corres_split_nor)
prefer 2
apply (rule corres_as_user)
apply (simp add: zipWithM_mapM getRestartPC_def setNextPC_def)
apply (rule corres_Id)
apply (clarsimp simp: sanitise_or_flags_def sanitise_and_flags_def
sanitiseOrFlags_def sanitiseAndFlags_def
mask_def user_vtop_def
cong: if_cong)
apply simp
apply (rule no_fail_pre, wp no_fail_mapM)
apply (clarsimp simp: sanitiseOrFlags_def sanitiseAndFlags_def)
apply ((safe)[1], (wp no_fail_setRegister | simp)+)
apply (rule corres_split_nor[OF _ corres_when[OF refl restart_corres]])
apply (rule corres_split_nor[OF _ corres_when[OF refl rescheduleRequired_corres]])
apply (rule_tac P=\<top> and P'=\<top> in corres_inst)
apply simp
apply (wp+)[2]
apply ((wp static_imp_wp restart_invs'
| strengthen valid_sched_weak_strg einvs_valid_etcbs invs_valid_queues' invs_queues
invs_weak_sch_act_wf
| clarsimp simp: invs_def valid_state_def valid_sched_def invs'_def valid_state'_def
dest!: global'_no_ex_cap idle_no_ex_cap)+)[2]
apply (rule_tac Q="\<lambda>_. einvs and tcb_at dest and ex_nonz_cap_to dest" in hoare_post_imp)
apply (fastforce simp: invs_def valid_sched_weak_strg valid_sched_def valid_state_def dest!: idle_no_ex_cap)
prefer 2
apply (rule_tac Q="\<lambda>_. invs' and tcb_at' dest and ex_nonz_cap_to' dest" in hoare_post_imp)
apply (fastforce simp: sch_act_wf_weak invs'_def valid_state'_def dest!: global'_no_ex_cap)
apply wpsimp+
done
crunch it[wp]: suspend "\<lambda>s. P (ksIdleThread s)"
@ -423,27 +440,36 @@ proof -
apply simp+
done
show ?thesis
apply (simp add: invokeTCB_def performTransfer_def)
apply (simp add: invokeTCB_def performTransfer_def)
apply (rule corres_guard_imp)
apply (rule corres_split_nor)
apply (rule corres_split_nor)
apply (rule corres_split_nor)
apply (simp add: liftM_def[symmetric] o_def dc_def[symmetric])
apply (rule corres_split [OF _ corres_when [OF refl suspend_corres]], simp)
apply (rule corres_split [OF _ corres_when [OF refl restart_corres]], simp)
apply (rule corres_split_nor)
apply (rule corres_split_nor)
apply (rule corres_split_eqr[OF _ gct_corres])
apply (rule corres_split[OF _ corres_when[OF refl rescheduleRequired_corres]])
apply (rule_tac P=\<top> and P'=\<top> in corres_inst)
apply simp
apply (wp static_imp_wp)+
apply (rule corres_when[OF refl])
apply (rule R[unfolded S, OF refl refl])
apply (simp add: gpRegisters_def)
apply (rule corres_when[OF refl])
apply (rule corres_split_nor)
apply (simp add: getRestartPC_def setNextPC_def)
apply (rule Q[unfolded S, OF refl refl])
apply (rule R[unfolded S, OF refl refl])
apply (simp add: frame_registers_def frameRegisters_def)
apply (wp mapM_x_wp' static_imp_wp | simp)+
apply (rule corres_when [OF refl])
apply (rule restart_corres)
apply (wp restart_invs' static_imp_wp | simp add: if_apply_def2)+
apply (rule corres_when [OF refl])
apply (rule suspend_corres)
apply (rule_tac Q="\<lambda>_. einvs and tcb_at dest" in hoare_post_imp)
apply (clarsimp simp: invs_def valid_sched_weak_strg valid_sched_def)
prefer 2
apply (rule_tac Q="\<lambda>_. invs' and tcb_at' dest" in hoare_post_imp)
apply (clarsimp simp: invs'_def valid_state'_def invs_weak_sch_act_wf)
apply (wp mapM_x_wp' | simp)+
apply (rule corres_when[OF refl])
apply (rule corres_split_nor)
apply (simp add: getRestartPC_def setNextPC_def dc_def[symmetric])
apply (rule Q[unfolded S, OF refl refl])
apply (rule R[unfolded S, OF refl refl])
apply (simp add: frame_registers_def frameRegisters_def)
apply ((wp mapM_x_wp' static_imp_wp, simp+)+)[2]
apply (wp mapM_x_wp' static_imp_wp, simp+)
apply ((wp mapM_x_wp' static_imp_wp | simp)+)[4]
apply ((wp static_imp_wp restart_invs' | wpc | clarsimp simp: if_apply_def2)+)[2]
apply (wp suspend_nonz_cap_to_tcb static_imp_wp | simp add: if_apply_def2)+
apply (fastforce simp: invs_def valid_state_def valid_pspace_def
dest!: idle_no_ex_cap)
@ -459,6 +485,13 @@ lemma readreg_invs':
| clarsimp simp: invs'_def valid_state'_def
dest!: global'_no_ex_cap)+
crunch invs'[wp]: getSanitiseRegisterInfo invs'
(ignore: getObject setObject)
crunch ex_nonz_cap_to'[wp]: getSanitiseRegisterInfo "ex_nonz_cap_to' d"
crunch it'[wp]: getSanitiseRegisterInfo "\<lambda>s. P (ksIdleThread s)"
crunch tcb_at'[wp]: getSanitiseRegisterInfo "tcb_at' a"
lemma writereg_invs':
"\<lbrace>invs' and sch_act_simple and tcb_at' dest and ex_nonz_cap_to' dest\<rbrace>
invokeTCB (tcbinvocation.WriteRegisters dest resume values arch)
@ -1082,12 +1115,71 @@ definition valid_tcb_invocation :: "tcbinvocation \<Rightarrow> bool" where
ThreadControl _ _ _ mcp p _ _ _ \<Rightarrow> valid_option_prio p \<and> valid_option_prio mcp
| _ \<Rightarrow> True"
lemma arch_tcb_set_ipc_buffer_corres:
"corres dc (tcb_at target) (tcb_at' target) (arch_tcb_set_ipc_buffer target ptr) (asUser target $ setTCBIPCBuffer ptr)"
apply (simp add: setTCBIPCBuffer_def)
apply (subst submonad_asUser.return)
apply (rule corres_stateAssert_assume)
apply simp+
done
lemma threadcontrol_corres_helper1:
"\<lbrace> tcb_at a and einvs and simple_sched_action\<rbrace>
thread_set (tcb_ipc_buffer_update f) a
\<lbrace>\<lambda>x. tcb_at a and (weak_valid_sched_action and valid_etcbs)\<rbrace>"
apply (rule hoare_pre)
apply (simp add: thread_set_def set_object_def)
apply wp
apply (simp add: not_None_eq | intro impI | elim exE conjE)+
apply (frule get_tcb_SomeD)
apply (erule ssubst)
apply (clarsimp simp add: weak_valid_sched_action_def valid_etcbs_2_def st_tcb_at_kh_def
get_tcb_def obj_at_kh_def obj_at_def is_etcb_at'_def valid_sched_def valid_sched_action_def)
apply (erule_tac x=a in allE)+
apply (clarsimp simp: is_tcb_def)
done
lemma threadcontrol_corres_helper2:
"is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>invs' and tcb_at' t\<rbrace>
threadSet (tcbIPCBuffer_update (\<lambda>_. a)) t
\<lbrace>\<lambda>x s. Invariants_H.valid_queues s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>"
by (wp threadSet_invs_trivial
| strengthen invs_valid_queues' invs_queues invs_weak_sch_act_wf
| clarsimp simp: inQ_def )+
lemma threadcontrol_corres_helper3:
"\<lbrace> einvs and simple_sched_action\<rbrace>
check_cap_at aaa (ab, ba) (check_cap_at (cap.ThreadCap a) slot (cap_insert aaa (ab, ba) (a, tcb_cnode_index 4)))
\<lbrace>\<lambda>x. weak_valid_sched_action and valid_etcbs \<rbrace>"
apply (rule hoare_pre)
apply (wp check_cap_inv | simp add:)+
by (clarsimp simp add: weak_valid_sched_action_def valid_etcbs_2_def st_tcb_at_kh_def
get_tcb_def obj_at_kh_def obj_at_def is_etcb_at'_def valid_sched_def valid_sched_action_def)
lemma threadcontrol_corres_helper4:
"isArchObjectCap ac \<Longrightarrow>
\<lbrace>invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (a, tcb_cnode_index 4)) and valid_cap' ac \<rbrace>
checkCapAt ac (cte_map (ab, ba))
(checkCapAt (capability.ThreadCap a) (cte_map slot)
(assertDerived (cte_map (ab, ba)) ac (cteInsert ac (cte_map (ab, ba)) (cte_map (a, tcb_cnode_index 4)))))
\<lbrace>\<lambda>x. Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace>"
apply (wp
| strengthen invs_valid_queues' invs_queues invs_weak_sch_act_wf
| clarsimp simp: )+
by (case_tac ac;
fastforce simp: capBadge_def isArchObjectCap_def isNotificationCap_def isEndpointCap_def
isReplyCap_def isIRQControlCap_def tcb_cnode_index_def cte_map_def cte_wp_at'_def )+
crunch valid_etcbs[wp]: arch_tcb_set_ipc_buffer valid_etcbs
crunch weak_valid_sched_action[wp]: arch_tcb_set_ipc_buffer weak_valid_sched_action
lemma tc_corres:
assumes x: "newroot_rel e e'" and y: "newroot_rel f f'" and p: "p = p'" and mcp: "mcp = mcp'"
and z: "(case g of None \<Rightarrow> g' = None
| Some (vptr, g'') \<Rightarrow> \<exists>g'''. g' = Some (vptr, g''')
\<and> newroot_rel g'' g''')"
and sl: "{e, f, option_map undefined g} \<noteq> {None} \<longrightarrow> sl' = cte_map slot"
notes arch_tcb_set_ipc_buffer_def[simp del]
shows
"corres (intr \<oplus> op =)
(einvs and simple_sched_action and tcb_at a and
@ -1112,6 +1204,8 @@ lemma tc_corres:
K (case_option True (isCNodeCap o fst) e') and
case_option \<top> (valid_cap' o fst) f' and
K (case_option True (isValidVTableRoot o fst) f') and
K (case_option True ((\<lambda>v. is_aligned v msg_align_bits) o fst) g') and
K (case_option True (case_option True (isArchObjectCap o fst) o snd) g') and
case_option \<top> (case_option \<top> (valid_cap' o fst) o snd) g' and
tcb_at' a and ex_nonz_cap_to' a and K (valid_option_prio p' \<and> valid_option_prio mcp') and
(\<lambda>s. case_option True (\<lambda>pr. mcpriority_tcb_at' (op \<le> pr) (ksCurThread s) s) p') and
@ -1210,20 +1304,24 @@ proof -
\<and> is_aligned x msg_align_bits)))
(invs' and sch_act_simple and tcb_at' a and
(\<lambda>s. \<forall>cp \<in> (case g' of None \<Rightarrow> {} | Some (x, v) \<Rightarrow> (case v of
None \<Rightarrow> {} | Some (c, sl) \<Rightarrow> {c})). s \<turnstile>' cp))
None \<Rightarrow> {} | Some (c, sl) \<Rightarrow> {c})). s \<turnstile>' cp) and
K (case g' of None \<Rightarrow> True | Some (x, v) \<Rightarrow> is_aligned x msg_align_bits
\<and> (case v of None \<Rightarrow> True | Some (ac, _) \<Rightarrow> isArchObjectCap ac)) )
(case_option (returnOk ())
(case_prod
(\<lambda>ptr frame.
doE cap_delete (a, tcb_cnode_index 4);
do y \<leftarrow> thread_set (tcb_ipc_buffer_update (\<lambda>_. ptr)) a;
liftE $
case_option (return ())
y \<leftarrow> arch_tcb_set_ipc_buffer a ptr;
y \<leftarrow> case_option (return ())
(case_prod
(\<lambda>new_cap src_slot.
check_cap_at new_cap src_slot $
check_cap_at (cap.ThreadCap a) slot $
cap_insert new_cap src_slot (a, tcb_cnode_index 4)))
frame
frame;
cur \<leftarrow> gets cur_thread;
liftE $ when (a = cur) (reschedule_required)
od
odE))
g)
@ -1232,8 +1330,8 @@ proof -
do bufferSlot \<leftarrow> getThreadBufferSlot a;
doE y \<leftarrow> cteDelete bufferSlot True;
do y \<leftarrow> threadSet (tcbIPCBuffer_update (\<lambda>_. ptr)) a;
liftE
(case_option (return ())
y \<leftarrow> asUser a $ setTCBIPCBuffer ptr;
y \<leftarrow> (case_option (return ())
(case_prod
(\<lambda>newCap srcSlot.
checkCapAt newCap srcSlot $
@ -1242,7 +1340,9 @@ proof -
sl' $
assertDerived srcSlot newCap $
cteInsert newCap srcSlot bufferSlot))
frame)
frame);
cur \<leftarrow> getCurThread;
liftE $ when (a = cur) rescheduleRequired
od odE od)
g')"
using z sl
@ -1256,14 +1356,24 @@ proof -
apply (case_tac b, simp_all add: newroot_rel_def)
apply (rule corres_guard_imp)
apply (rule corres_split_norE)
apply (rule_tac F="is_aligned aa msg_align_bits" in corres_gen_asm2)
apply (rule corres_split_nor)
apply (rule corres_trivial)
apply (rule corres_split)
apply (rule corres_split [OF _ gct_corres], clarsimp)
apply (rule corres_when[OF refl rescheduleRequired_corres])
apply (wpsimp wp: gct_wp)+
apply (rule arch_tcb_set_ipc_buffer_corres[simplified])
apply simp
apply (wp hoare_drop_imp)+
apply (rule threadset_corres,
(simp add: tcb_relation_def), (simp add: exst_same_def)+)[1]
apply wp+
apply (subst pred_conj_def)
apply (rule threadcontrol_corres_helper1[unfolded pred_conj_def])
apply simp
apply (wp threadcontrol_corres_helper2 | wpc | simp)+
apply (rule cap_delete_corres)
apply wp+
apply wp
apply (wp cteDelete_invs' hoare_vcg_conj_lift)
apply (fastforce simp: emptyable_def)
apply fastforce
apply clarsimp
@ -1271,9 +1381,20 @@ proof -
apply (rule corres_split_norE [OF _ cap_delete_corres])
apply (rule_tac F="is_aligned aa msg_align_bits"
in corres_gen_asm)
apply (rule_tac F="isArchObjectCap ac" in corres_gen_asm2)
apply (rule corres_split_nor)
apply (rule corres_split[rotated])
apply (rule arch_tcb_set_ipc_buffer_corres[simplified])
prefer 3
apply simp
apply (erule checked_insert_corres)
apply (rule corres_split_nor)
apply (rule corres_split[OF _ gct_corres], clarsimp)
apply (rule corres_when[OF refl rescheduleRequired_corres])
apply (wp gct_wp)+
apply (erule checked_insert_corres)
apply (wp hoare_drop_imp threadcontrol_corres_helper3)[1]
apply (wp hoare_drop_imp threadcontrol_corres_helper4)[1]
apply (wp | simp add: arch_tcb_set_ipc_buffer_def)+
apply (rule threadset_corres,
simp add: tcb_relation_def, (simp add: exst_same_def)+)
apply (wp thread_set_tcb_ipc_buffer_cap_cleared_invs

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

@ -92,11 +92,11 @@ lemma pspace_relation_pml4:
done
lemma find_vspace_for_asid_eq_helper:
"\<lbrakk> vspace_at_asid asid pm s; valid_arch_objs s;
"\<lbrakk> vspace_at_asid asid pm s; valid_vspace_objs s;
asid \<noteq> 0; pspace_aligned s \<rbrakk>
\<Longrightarrow> find_vspace_for_asid asid s = returnOk pm s
\<and> page_map_l4_at pm s \<and> is_aligned pm pml4Bits"
apply (clarsimp simp: vspace_at_asid_def valid_arch_objs_def)
apply (clarsimp simp: vspace_at_asid_def valid_vspace_objs_def)
apply (frule spec, drule mp, erule exI)
apply (clarsimp simp: vs_asid_refs_def graph_of_def
elim!: vs_lookupE)
@ -134,7 +134,7 @@ lemma find_vspace_for_asid_eq_helper:
done
lemma find_vspace_for_asid_assert_eq:
"\<lbrakk> vspace_at_asid asid pm s; valid_arch_objs s;
"\<lbrakk> vspace_at_asid asid pm s; valid_vspace_objs s;
asid \<noteq> 0; pspace_aligned s \<rbrakk>
\<Longrightarrow> find_vspace_for_asid_assert asid s = return pm s"
apply (drule (3) find_vspace_for_asid_eq_helper)
@ -152,7 +152,7 @@ lemma find_vspace_for_asid_assert_eq:
done
lemma find_vspace_for_asid_assert_eq_ex:
"\<lbrakk> vspace_at_asid_ex asid s; valid_arch_objs s;
"\<lbrakk> vspace_at_asid_ex asid s; valid_vspace_objs s;
asid \<noteq> 0; pspace_aligned s \<rbrakk>
\<Longrightarrow> (do _ \<leftarrow> find_vspace_for_asid_assert asid; return () od) s = return () s"
apply (clarsimp simp: vspace_at_asid_ex_def)
@ -172,7 +172,7 @@ lemma find_vspace_for_asid_assert_eq_ex:
(* FIXME x64: move to invariants *)
lemma find_vspace_for_asid_wp:
"\<lbrace> valid_arch_objs and pspace_aligned and K (asid \<noteq> 0)
"\<lbrace> valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0)
and (\<lambda>s. \<forall>pm. vspace_at_asid asid pm s \<longrightarrow> Q pm s)
and (\<lambda>s. (\<forall>pm. \<not> vspace_at_asid asid pm s) \<longrightarrow> E ExceptionTypes_A.lookup_failure.InvalidRoot s) \<rbrace>
find_vspace_for_asid asid
@ -203,7 +203,7 @@ lemma find_vspace_for_asid_wp:
lemma valid_asid_map_inj_map:
"\<lbrakk> valid_asid_map s; (s, s') \<in> state_relation;
unique_table_refs (caps_of_state s);
valid_vs_lookup s; valid_arch_objs s;
valid_vs_lookup s; valid_vspace_objs s;
valid_arch_state s; valid_global_objs s \<rbrakk>
\<Longrightarrow> inj_on (x64KSASIDMap (ksArchState s'))
(dom (x64KSASIDMap (ksArchState s')))"
@ -227,7 +227,7 @@ lemma find_vspace_for_asid_assert_corres [corres]:
assumes "asid' = asid"
shows "corres (op =)
(K (asid \<noteq> 0 \<and> asid \<le> mask asid_bits)
and pspace_aligned and pspace_distinct and valid_arch_objs and valid_asid_map
and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map
and vspace_at_uniq_ex asid)
(pspace_aligned' and pspace_distinct' and no_0_obj')
(find_vspace_for_asid_assert asid)
@ -312,7 +312,7 @@ lemma corres_add_noop_rhs2:
(* FIXME x64: make intro/elim rules for vspace_at_asid_ex and vspace_at_uniq_ex. *)
lemma invalidate_asid_corres [corres]:
assumes "a' = a"
shows "corres dc (valid_asid_map and valid_arch_objs
shows "corres dc (valid_asid_map and valid_vspace_objs
and pspace_aligned and pspace_distinct
and vspace_at_uniq_ex a
and K (a \<noteq> 0 \<and> a \<le> mask asid_bits))
@ -338,7 +338,7 @@ lemma invalidate_asid_corres [corres]:
lemma invalidate_asid_ext_corres:
"corres dc
(\<lambda>s. \<exists>pd. valid_asid_map s \<and> valid_arch_objs s
(\<lambda>s. \<exists>pd. valid_asid_map s \<and> valid_vspace_objs s
\<and> pspace_aligned s \<and> pspace_distinct s
\<and> vspace_at_asid a pd s \<and> vspace_at_uniq a pd s
\<and> a \<noteq> 0 \<and> a \<le> mask asid_bits)
@ -417,7 +417,7 @@ lemma update_asid_map_corres [corres]:
assumes "a' = a"
shows "corres dc (K (a \<noteq> 0 \<and> a \<le> mask asid_bits) and
pspace_aligned and pspace_distinct and
valid_arch_objs and valid_asid_map and
valid_vspace_objs and valid_asid_map and
vspace_at_uniq_ex a)
(pspace_aligned' and pspace_distinct' and no_0_obj')
(update_asid_map a) (updateASIDMap a')"
@ -425,24 +425,12 @@ lemma update_asid_map_corres [corres]:
apply (simp add: update_asid_map_def updateASIDMap_def)
by corressimp
(* FIXME x64: move to Corres_Method *)
lemma corres_rv_disj_dc: "corres_rv_disj r' r'' dc"
unfolding corres_rv_disj_def by simp
(* FIXME x64: move to Corres_Method *)
lemma corresK_whenE (* [corresK] *):
assumes "G \<Longrightarrow> G' \<Longrightarrow> corres_underlyingK sr nf nf' F (f \<oplus> dc) P P' a c"
shows "corres_underlyingK sr nf nf' ((G = G') \<and> F) (f \<oplus> dc) ((\<lambda>x. G \<longrightarrow> P x)) (\<lambda>x. G' \<longrightarrow> P' x)
(whenE G a) (whenE G' c)"
using assms by (cases G) (auto simp: corres_underlying_def corres_underlyingK_def
whenE_def returnOk_def return_def)
lemma set_vm_root_corres [corres]:
assumes "t' = t"
shows "corres dc (tcb_at t and valid_arch_state and valid_objs and valid_asid_map
and unique_table_refs o caps_of_state and valid_vs_lookup
and valid_global_objs and pspace_aligned and pspace_distinct
and valid_arch_objs)
and valid_vspace_objs)
(pspace_aligned' and pspace_distinct'
and valid_arch_state' and tcb_at' t' and no_0_obj')
(set_vm_root t) (setVMRoot t')"
@ -485,7 +473,7 @@ proof -
apply (simp add: tcbVTableSlot_def cte_map_def objBits_def cte_level_bits_def
objBitsKO_def tcb_cnode_index_def to_bl_1 assms)
apply (rule_tac R="\<lambda>thread_root. valid_arch_state and valid_asid_map and
valid_arch_objs and valid_vs_lookup and
valid_vspace_objs and valid_vs_lookup and
unique_table_refs o caps_of_state and
valid_global_objs and valid_objs and
pspace_aligned and pspace_distinct and
@ -569,7 +557,7 @@ lemma dmo_vspace_at_uniq_ex [wp]:
lemma invalidate_asid_entry_corres:
assumes "pm' = pm" "asid' = asid"
shows "corres dc (valid_arch_objs and valid_asid_map
shows "corres dc (valid_vspace_objs and valid_asid_map
and K (asid \<le> mask asid_bits \<and> asid \<noteq> 0)
and vspace_at_asid asid pm and valid_vs_lookup
and unique_table_refs o caps_of_state
@ -638,10 +626,10 @@ lemma set_asid_pool_asid_map_unmap:
by (simp add: restrict_map_def fun_upd_def if_flip)
(* FIXME x64: move *)
lemma set_asid_pool_arch_objs_unmap_single:
"\<lbrace>valid_arch_objs and ko_at (ArchObj (X64_A.ASIDPool ap)) p\<rbrace>
set_asid_pool p (ap(x := None)) \<lbrace>\<lambda>_. valid_arch_objs\<rbrace>"
using set_asid_pool_arch_objs_unmap[where S="- {x}"]
lemma set_asid_pool_vspace_objs_unmap_single:
"\<lbrace>valid_vspace_objs and ko_at (ArchObj (X64_A.ASIDPool ap)) p\<rbrace>
set_asid_pool p (ap(x := None)) \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>"
using set_asid_pool_vspace_objs_unmap[where S="- {x}"]
by (simp add: restrict_map_def fun_upd_def if_flip)
(* FIXME x64: move *)
@ -655,7 +643,7 @@ lemma invalidate_asid_entry_valid_arch_state[wp]:
lemma valid_global_objs_asid_map_update_inv[simp]:
"valid_global_objs s \<Longrightarrow> valid_global_objs (s\<lparr>arch_state := arch_state s \<lparr>x64_asid_map := b\<rparr>\<rparr>)"
by (clarsimp simp: valid_global_objs_def)
by (clarsimp simp: valid_global_objs_def second_level_tables_def)
crunch valid_global_objs[wp]: invalidate_asid_entry "valid_global_objs"
@ -704,7 +692,7 @@ lemma delete_asid_corres [corres]:
apply (fold cur_tcb_def)
apply (wp set_asid_pool_asid_map_unmap
set_asid_pool_vs_lookup_unmap'
set_asid_pool_arch_objs_unmap_single)+
set_asid_pool_vspace_objs_unmap_single)+
apply simp
apply (fold cur_tcb'_def)
apply (wp add: invalidate_asid_entry_invalidates | clarsimp simp: o_def)+
@ -855,7 +843,7 @@ lemma delete_asid_pool_corres:
apply simp
apply (fold cur_tcb_def)
apply (strengthen valid_arch_state_unmap_strg
valid_arch_objs_unmap_strg
valid_vspace_objs_unmap_strg
valid_asid_map_unmap
valid_vs_lookup_unmap_strg)
apply (simp add: valid_global_objs_arch_update)
@ -1005,7 +993,7 @@ lemma flush_table_corres:
assumes "pm' = pm" "vptr' = vptr" "pt' = pt" "asid' = asid"
shows "corres dc (pspace_aligned and valid_objs and valid_arch_state
and cur_tcb and vspace_at_asid asid pm and valid_asid_map
and valid_arch_objs and pspace_aligned and pspace_distinct
and valid_vspace_objs and pspace_aligned and pspace_distinct
and valid_vs_lookup and valid_global_objs
and unique_table_refs o caps_of_state and page_table_at pt
and K (is_aligned vptr pd_shift_bits \<and> asid \<le> mask asid_bits \<and> asid \<noteq> 0))
@ -1219,7 +1207,7 @@ lemma unmap_page_corres:
apply (rule_tac F = "vptr < pptr_base" in corres_gen_asm)
apply (rule_tac P="\<exists>\<rhd> vspace and page_map_l4_at vspace and vspace_at_asid asid vspace
and (\<exists>\<rhd> vspace)
and valid_arch_state and valid_arch_objs
and valid_arch_state and valid_vspace_objs
and equal_kernel_mappings
and pspace_aligned and valid_global_objs and valid_etcbs and
K (valid_unmap sz (asid,vptr) \<and> canonical_address vptr )" and
@ -1267,7 +1255,7 @@ lemma unmap_page_corres:
simp_del: dc_simp)+
| wp_once hoare_drop_imps)+)
apply (rule conjI[OF disjI1], clarsimp)
apply (clarsimp simp: invs_arch_objs invs_psp_aligned valid_unmap_def invs_arch_state
apply (clarsimp simp: invs_vspace_objs invs_psp_aligned valid_unmap_def invs_arch_state
invs_equal_kernel_mappings)
apply (clarsimp)
done