x64: refine: remove valid_pde_mappings' for the moment
This commit is contained in:
Joel Beeren
parent
5c574a6da4
commit
431b134b19
|
|
@ -3124,19 +3124,6 @@ lemma cteInsert_valid_irq_handlers'[wp]:
|
|||
apply (clarsimp simp:modify_map_def split:if_splits)
|
||||
done
|
||||
|
||||
lemma setCTE_valid_mappings'[wp]:
|
||||
"\<lbrace>valid_pde_mappings'\<rbrace> setCTE x y \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace>"
|
||||
apply (wp valid_pde_mappings_lift' setCTE_typ_at')
|
||||
apply (simp add: setCTE_def)
|
||||
apply (rule obj_at_setObject2)
|
||||
apply (clarsimp simp: updateObject_cte typeError_def in_monad
|
||||
split: Structures_H.kernel_object.split_asm if_split_asm)
|
||||
apply assumption
|
||||
done
|
||||
|
||||
crunch pde_mappings' [wp]: cteInsert valid_pde_mappings'
|
||||
(wp: crunch_wps)
|
||||
|
||||
lemma setCTE_irq_states' [wp]:
|
||||
"\<lbrace>valid_irq_states'\<rbrace> setCTE x y \<lbrace>\<lambda>_. valid_irq_states'\<rbrace>"
|
||||
apply (rule valid_irq_states_lift')
|
||||
|
|
@ -3255,9 +3242,6 @@ lemma cteInsert_valid_globals [wp]:
|
|||
crunch arch [wp]: cteInsert "\<lambda>s. P (ksArchState s)"
|
||||
(wp: crunch_wps simp: cte_wp_at_ctes_of)
|
||||
|
||||
crunch pde_mappings' [wp]: cteInsert valid_pde_mappings'
|
||||
(wp: crunch_wps)
|
||||
|
||||
lemma setCTE_ksMachine[wp]:
|
||||
"\<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> setCTE x y \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>"
|
||||
apply (clarsimp simp: setCTE_def)
|
||||
|
|
@ -4390,8 +4374,6 @@ lemma setupReplyMaster_irq_handlers'[wp]:
|
|||
crunch irq_states' [wp]: setupReplyMaster valid_irq_states'
|
||||
crunch irqs_makes' [wp]: setupReplyMaster irqs_masked'
|
||||
(rule: irqs_masked_lift)
|
||||
crunch pde_mappings' [wp]: setupReplyMaster valid_pde_mappings'
|
||||
|
||||
crunch pred_tcb_at' [wp]: setupReplyMaster "pred_tcb_at' proj P t"
|
||||
|
||||
crunch ksMachine[wp]: setupReplyMaster "\<lambda>s. P (ksMachineState s)"
|
||||
|
|
|
|||
|
|
@ -441,7 +441,7 @@ where valid_cap'_def:
|
|||
| PageTableCap ref mapdata \<Rightarrow>
|
||||
page_table_at' ref s \<and>
|
||||
(case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow>
|
||||
0 < asid \<and> asid \<le> 2^asid_bits - 1 \<and> ref < kernelBase)
|
||||
0 < asid \<and> asid \<le> 2^asid_bits - 1 \<and> ref < pptrBase)
|
||||
| PageDirectoryCap ref mapdata \<Rightarrow>
|
||||
page_directory_at' ref s \<and>
|
||||
(case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le>2^asid_bits-1 \<and> ref < pptrBase)
|
||||
|
|
@ -1107,31 +1107,6 @@ where
|
|||
definition
|
||||
"irqs_masked' \<equiv> \<lambda>s. \<forall>irq > maxIRQ. intStateIRQTable (ksInterruptState s) irq = IRQInactive"
|
||||
|
||||
definition
|
||||
pd_asid_slot :: machine_word
|
||||
where
|
||||
"pd_asid_slot \<equiv> 0xff0"
|
||||
|
||||
(* ideally, all mappings above kernel_base are global and kernel-only, and
|
||||
of them one particular mapping is clear. at the moment all we can easily say
|
||||
is that the mapping is clear. *)
|
||||
definition
|
||||
valid_pde_mapping_offset' :: "machine_word \<Rightarrow> bool"
|
||||
where
|
||||
"valid_pde_mapping_offset' offset \<equiv> offset \<noteq> pd_asid_slot * 4"
|
||||
|
||||
definition
|
||||
valid_pde_mapping' :: "machine_word \<Rightarrow> pde \<Rightarrow> bool"
|
||||
where
|
||||
"valid_pde_mapping' offset pde \<equiv> pde = InvalidPDE \<or> valid_pde_mapping_offset' offset"
|
||||
|
||||
definition
|
||||
valid_pde_mappings' :: "kernel_state \<Rightarrow> bool"
|
||||
where
|
||||
"valid_pde_mappings' \<equiv> \<lambda>s.
|
||||
\<forall>x pde. ko_at' pde x s
|
||||
\<longrightarrow> valid_pde_mapping' (x && mask pdBits) pde"
|
||||
|
||||
definition
|
||||
"valid_irq_masks' table masked \<equiv> \<forall>irq. table irq = IRQInactive \<longrightarrow> masked irq"
|
||||
|
||||
|
|
@ -1183,7 +1158,6 @@ where
|
|||
\<and> valid_queues' s
|
||||
\<and> ct_not_inQ s
|
||||
\<and> ct_idle_or_in_cur_domain' s
|
||||
\<and> valid_pde_mappings' s
|
||||
\<and> pspace_domain_valid s
|
||||
\<and> ksCurDomain s \<le> maxDomain
|
||||
\<and> valid_dom_schedule' s
|
||||
|
|
@ -1253,7 +1227,7 @@ abbreviation(input)
|
|||
\<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s
|
||||
\<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s
|
||||
\<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s
|
||||
\<and> cur_tcb' s \<and> valid_queues' s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s
|
||||
\<and> cur_tcb' s \<and> valid_queues' s \<and> ct_idle_or_in_cur_domain' s
|
||||
\<and> pspace_domain_valid s
|
||||
\<and> ksCurDomain s \<le> maxDomain
|
||||
\<and> valid_dom_schedule' s \<and> untyped_ranges_zero' s"
|
||||
|
|
@ -1266,7 +1240,7 @@ abbreviation(input)
|
|||
\<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s
|
||||
\<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s
|
||||
\<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s
|
||||
\<and> cur_tcb' s \<and> valid_queues' s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s
|
||||
\<and> cur_tcb' s \<and> valid_queues' s \<and> ct_idle_or_in_cur_domain' s
|
||||
\<and> pspace_domain_valid s
|
||||
\<and> ksCurDomain s \<le> maxDomain
|
||||
\<and> valid_dom_schedule' s \<and> untyped_ranges_zero' s"
|
||||
|
|
@ -1287,7 +1261,7 @@ definition
|
|||
\<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s
|
||||
\<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s
|
||||
\<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s
|
||||
\<and> cur_tcb' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> valid_pde_mappings' s
|
||||
\<and> cur_tcb' s \<and> valid_queues' s \<and> ct_not_inQ s
|
||||
\<and> pspace_domain_valid s
|
||||
\<and> ksCurDomain s \<le> maxDomain
|
||||
\<and> valid_dom_schedule' s \<and> untyped_ranges_zero' s"
|
||||
|
|
@ -1889,14 +1863,6 @@ lemma objBits_cte_conv:
|
|||
"objBits (cte :: cte) = 5"
|
||||
by (simp add: objBits_def objBitsKO_def wordSizeCase_def word_size)
|
||||
|
||||
lemma valid_pde_mapping'_simps[simp]:
|
||||
"valid_pde_mapping' offset (InvalidPDE) = True"
|
||||
"valid_pde_mapping' offset (LargePagePDE ptr a b c d e w x y)
|
||||
= valid_pde_mapping_offset' offset"
|
||||
"valid_pde_mapping' offset (PageTablePDE ptr x z'' g h f)
|
||||
= valid_pde_mapping_offset' offset"
|
||||
by (clarsimp simp: valid_pde_mapping'_def)+
|
||||
|
||||
lemmas valid_irq_states'_def = valid_irq_masks'_def
|
||||
|
||||
lemma valid_pspaceI' [intro]:
|
||||
|
|
@ -3036,10 +3002,6 @@ lemma no_0_obj'_update [iff]:
|
|||
"no_0_obj' (f s) = no_0_obj' s"
|
||||
by (simp add: no_0_obj'_def pspace)
|
||||
|
||||
lemma valid_pde_mappings'_update [iff]:
|
||||
"valid_pde_mappings' (f s) = valid_pde_mappings' s"
|
||||
by (simp add: valid_pde_mappings'_def)
|
||||
|
||||
lemma pointerInUserData_update[iff]:
|
||||
"pointerInUserData p (f s) = pointerInUserData p s"
|
||||
by (simp add: pointerInUserData_def)
|
||||
|
|
|
|||
|
|
@ -2096,33 +2096,6 @@ lemmas set_ntfn_irq_handlers'[wp] = valid_irq_handlers_lift'' [OF set_ntfn_ctes_
|
|||
|
||||
lemmas set_ntfn_irq_states' [wp] = valid_irq_states_lift' [OF set_ntfn_ksInterrupt set_ntfn_ksMachine]
|
||||
|
||||
lemma valid_pde_mappings'_def2:
|
||||
"valid_pde_mappings' =
|
||||
(\<lambda>s. \<forall>x. pde_at' x s \<longrightarrow> obj_at' (valid_pde_mapping' (x && mask pdBits)) x s)"
|
||||
apply (clarsimp simp: valid_pde_mappings'_def typ_at_to_obj_at_arches)
|
||||
apply (rule ext, rule iff_allI)
|
||||
apply (clarsimp simp: obj_at'_def projectKOs)
|
||||
apply (auto simp add: objBits_simps archObjSize_def)
|
||||
done
|
||||
|
||||
lemma valid_pde_mappings_lift':
|
||||
assumes x: "\<And>P T p. \<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at' T p s)\<rbrace>"
|
||||
assumes y: "\<And>x. \<lbrace>obj_at' (valid_pde_mapping' (x && mask pdBits)) x\<rbrace>
|
||||
f \<lbrace>\<lambda>rv. obj_at' (valid_pde_mapping' (x && mask pdBits)) x\<rbrace>"
|
||||
shows "\<lbrace>valid_pde_mappings'\<rbrace> f \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace>"
|
||||
apply (simp only: valid_pde_mappings'_def2 imp_conv_disj)
|
||||
apply (rule hoare_vcg_all_lift hoare_vcg_disj_lift x y)+
|
||||
done
|
||||
|
||||
lemma set_ntfn_valid_pde_mappings'[wp]:
|
||||
"\<lbrace>valid_pde_mappings'\<rbrace> setNotification ptr val \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace>"
|
||||
apply (rule valid_pde_mappings_lift')
|
||||
apply wp
|
||||
apply (simp add: setNotification_def)
|
||||
apply (rule obj_at_setObject2)
|
||||
apply (clarsimp simp: updateObject_default_def in_monad)
|
||||
done
|
||||
|
||||
lemma set_ntfn_vms'[wp]:
|
||||
"\<lbrace>valid_machine_state'\<rbrace> setNotification ptr val \<lbrace>\<lambda>rv. valid_machine_state'\<rbrace>"
|
||||
apply (simp add: setNotification_def valid_machine_state'_def pointerInDeviceData_def pointerInUserData_def)
|
||||
|
|
@ -2321,7 +2294,6 @@ crunch obj_at'[wp]: doMachineOp "\<lambda>s. P (obj_at' P' p s)"
|
|||
crunch it[wp]: doMachineOp "\<lambda>s. P (ksIdleThread s)"
|
||||
crunch idle'[wp]: doMachineOp "valid_idle'"
|
||||
(wp: crunch_wps simp: crunch_simps valid_idle'_pspace_itI)
|
||||
crunch pde_mappings'[wp]: doMachineOp "valid_pde_mappings'"
|
||||
|
||||
lemma setEndpoint_ksMachine:
|
||||
"\<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> setEndpoint ptr val \<lbrace>\<lambda>rv s. P (ksMachineState s)\<rbrace>"
|
||||
|
|
|
|||
|
|
@ -1003,19 +1003,9 @@ lemma threadSet_typ_at'[wp]:
|
|||
|
||||
lemmas threadSet_typ_at_lifts[wp] = typ_at_lifts [OF threadSet_typ_at']
|
||||
|
||||
lemma setObject_tcb_pde_mappings'[wp]:
|
||||
"\<lbrace>valid_pde_mappings'\<rbrace> setObject p (tcb :: tcb) \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace>"
|
||||
apply (wp valid_pde_mappings_lift' setObject_typ_at')
|
||||
apply (rule obj_at_setObject2)
|
||||
apply (auto dest: updateObject_default_result)
|
||||
done
|
||||
|
||||
crunch irq_states' [wp]: threadSet valid_irq_states'
|
||||
(ignore: setObject getObject)
|
||||
|
||||
crunch pde_mappings' [wp]: threadSet valid_pde_mappings'
|
||||
(ignore: getObject setObject)
|
||||
|
||||
crunch pspace_domain_valid [wp]: threadSet "pspace_domain_valid"
|
||||
(ignore: getObject setObject)
|
||||
|
||||
|
|
@ -4305,8 +4295,6 @@ lemma sbn_global_reds' [wp]:
|
|||
|
||||
crunch irq_states' [wp]: setThreadState, setBoundNotification valid_irq_states'
|
||||
(simp: unless_def crunch_simps)
|
||||
crunch pde_mappings' [wp]: setThreadState, setBoundNotification valid_pde_mappings'
|
||||
(simp: unless_def crunch_simps)
|
||||
|
||||
lemma addToBitmap_ksMachine[wp]:
|
||||
"\<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> addToBitmap d p \<lbrace>\<lambda>rv s. P (ksMachineState s)\<rbrace>"
|
||||
|
|
|
|||
|
|
@ -1181,11 +1181,6 @@ definition
|
|||
| X64_A.PageGetAddr ptr \<Rightarrow>
|
||||
pgi' = PageGetAddr ptr"
|
||||
|
||||
(* FIXME x64: is this needed? *)
|
||||
definition
|
||||
"valid_pde_slots' m \<equiv> case m of Inl (pte, xs) \<Rightarrow> True
|
||||
| Inr (pde, xs) \<Rightarrow> \<forall>x \<in> set xs. valid_pde_mapping' (x && mask pdBits) pde"
|
||||
|
||||
lemma tl_nat_list_simp:
|
||||
"tl [a..<b] = [a + 1 ..<b]"
|
||||
by (induct b,auto)
|
||||
|
|
@ -1615,7 +1610,7 @@ lemma perform_page_table_corres:
|
|||
subgoal sorry (* FIXME x64: this will be solved by adding "pde_at pd_slot" to valid_pti *)
|
||||
apply (clarsimp simp: cte_wp_at_ctes_of valid_pti'_def)
|
||||
apply auto[1]
|
||||
apply (clarsimp simp:valid_pde_mapping'_def split:X64_H.pde.split)
|
||||
apply (clarsimp simp: split:X64_H.pde.split)
|
||||
apply (rename_tac cap a b)
|
||||
apply (clarsimp simp: page_table_invocation_map_def)
|
||||
apply (rule_tac F="is_pt_cap cap" in corres_req)
|
||||
|
|
@ -2370,18 +2365,115 @@ lemma setObject_pde_ksDomScheduleIdx [wp]:
|
|||
"\<lbrace>\<lambda>s. P (ksDomScheduleIdx s)\<rbrace> setObject p (pde::pde) \<lbrace>\<lambda>_. \<lambda>s. P (ksDomScheduleIdx s)\<rbrace>"
|
||||
by (wp updateObject_default_inv|simp add:setObject_def | wpc)+
|
||||
|
||||
crunch ksDomScheduleIdx[wp]: storePTE, storePDE "\<lambda>s. P (ksDomScheduleIdx s)"
|
||||
lemma storePDPTE_ct_not_inQ[wp]:
|
||||
"\<lbrace>ct_not_inQ\<rbrace> storePDPTE p pdpte \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>"
|
||||
apply (rule ct_not_inQ_lift [OF storePDPTE_nosch])
|
||||
apply (simp add: storePDPTE_def)
|
||||
apply (rule hoare_weaken_pre)
|
||||
apply (wps setObject_PDPTE_ct)
|
||||
apply (rule obj_at_setObject2)
|
||||
apply (clarsimp simp: updateObject_default_def in_monad)+
|
||||
done
|
||||
|
||||
lemma setObject_pdpte_cur_domain[wp]:
|
||||
"\<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> setObject t (v::pdpte) \<lbrace>\<lambda>rv s. P (ksCurDomain s)\<rbrace>"
|
||||
apply (simp add: setObject_def split_def)
|
||||
apply (wp updateObject_default_inv | simp)+
|
||||
done
|
||||
|
||||
lemma setObject_pdpte_ksDomSchedule[wp]:
|
||||
"\<lbrace>\<lambda>s. P (ksDomSchedule s)\<rbrace> setObject t (v::pdpte) \<lbrace>\<lambda>rv s. P (ksDomSchedule s)\<rbrace>"
|
||||
apply (simp add: setObject_def split_def)
|
||||
apply (wp updateObject_default_inv | simp)+
|
||||
done
|
||||
|
||||
lemma storePDPTE_cur_domain[wp]:
|
||||
"\<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> storePDPTE p pdpte \<lbrace>\<lambda>rv s. P (ksCurDomain s)\<rbrace>"
|
||||
by (simp add: storePDPTE_def) wp
|
||||
|
||||
lemma storePDPTE_ksDomSchedule[wp]:
|
||||
"\<lbrace>\<lambda>s. P (ksDomSchedule s)\<rbrace> storePDPTE p pdpte \<lbrace>\<lambda>rv s. P (ksDomSchedule s)\<rbrace>"
|
||||
by (simp add: storePDPTE_def) wp
|
||||
|
||||
lemma storePDPTE_tcb_obj_at'[wp]:
|
||||
"\<lbrace>obj_at' (P::tcb \<Rightarrow> bool) t\<rbrace> storePDPTE p pdpte \<lbrace>\<lambda>_. obj_at' P t\<rbrace>"
|
||||
apply (simp add: storePDPTE_def)
|
||||
apply (rule obj_at_setObject2)
|
||||
apply (clarsimp simp add: updateObject_default_def in_monad)
|
||||
done
|
||||
|
||||
lemma storePDPTE_tcb_in_cur_domain'[wp]:
|
||||
"\<lbrace>tcb_in_cur_domain' t\<rbrace> storePDPTE p pdpte \<lbrace>\<lambda>_. tcb_in_cur_domain' t\<rbrace>"
|
||||
by (wp tcb_in_cur_domain'_lift)
|
||||
|
||||
lemma storePDPTE_ct_idle_or_in_cur_domain'[wp]:
|
||||
"\<lbrace>ct_idle_or_in_cur_domain'\<rbrace> storePDPTE p pdpte \<lbrace>\<lambda>_. ct_idle_or_in_cur_domain'\<rbrace>"
|
||||
by (wp ct_idle_or_in_cur_domain'_lift hoare_vcg_disj_lift)
|
||||
|
||||
lemma setObject_pdpte_ksDomScheduleIdx [wp]:
|
||||
"\<lbrace>\<lambda>s. P (ksDomScheduleIdx s)\<rbrace> setObject p (pdpte::pdpte) \<lbrace>\<lambda>_. \<lambda>s. P (ksDomScheduleIdx s)\<rbrace>"
|
||||
by (wp updateObject_default_inv|simp add:setObject_def | wpc)+
|
||||
|
||||
lemma storePML4E_ct_not_inQ[wp]:
|
||||
"\<lbrace>ct_not_inQ\<rbrace> storePML4E p pml4e \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>"
|
||||
apply (rule ct_not_inQ_lift [OF storePML4E_nosch])
|
||||
apply (simp add: storePML4E_def)
|
||||
apply (rule hoare_weaken_pre)
|
||||
apply (wps setObject_PML4E_ct)
|
||||
apply (rule obj_at_setObject2)
|
||||
apply (clarsimp simp: updateObject_default_def in_monad)+
|
||||
done
|
||||
|
||||
lemma setObject_pml4e_cur_domain[wp]:
|
||||
"\<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> setObject t (v::pml4e) \<lbrace>\<lambda>rv s. P (ksCurDomain s)\<rbrace>"
|
||||
apply (simp add: setObject_def split_def)
|
||||
apply (wp updateObject_default_inv | simp)+
|
||||
done
|
||||
|
||||
lemma setObject_pml4e_ksDomSchedule[wp]:
|
||||
"\<lbrace>\<lambda>s. P (ksDomSchedule s)\<rbrace> setObject t (v::pml4e) \<lbrace>\<lambda>rv s. P (ksDomSchedule s)\<rbrace>"
|
||||
apply (simp add: setObject_def split_def)
|
||||
apply (wp updateObject_default_inv | simp)+
|
||||
done
|
||||
|
||||
lemma storePML4E_cur_domain[wp]:
|
||||
"\<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> storePML4E p pml4e \<lbrace>\<lambda>rv s. P (ksCurDomain s)\<rbrace>"
|
||||
by (simp add: storePML4E_def) wp
|
||||
|
||||
lemma storePML4E_ksDomSchedule[wp]:
|
||||
"\<lbrace>\<lambda>s. P (ksDomSchedule s)\<rbrace> storePML4E p pml4e \<lbrace>\<lambda>rv s. P (ksDomSchedule s)\<rbrace>"
|
||||
by (simp add: storePML4E_def) wp
|
||||
|
||||
lemma storePML4E_tcb_obj_at'[wp]:
|
||||
"\<lbrace>obj_at' (P::tcb \<Rightarrow> bool) t\<rbrace> storePML4E p pml4e \<lbrace>\<lambda>_. obj_at' P t\<rbrace>"
|
||||
apply (simp add: storePML4E_def)
|
||||
apply (rule obj_at_setObject2)
|
||||
apply (clarsimp simp add: updateObject_default_def in_monad)
|
||||
done
|
||||
|
||||
lemma storePML4E_tcb_in_cur_domain'[wp]:
|
||||
"\<lbrace>tcb_in_cur_domain' t\<rbrace> storePML4E p pml4e \<lbrace>\<lambda>_. tcb_in_cur_domain' t\<rbrace>"
|
||||
by (wp tcb_in_cur_domain'_lift)
|
||||
|
||||
lemma storePML4E_ct_idle_or_in_cur_domain'[wp]:
|
||||
"\<lbrace>ct_idle_or_in_cur_domain'\<rbrace> storePML4E p pml4e \<lbrace>\<lambda>_. ct_idle_or_in_cur_domain'\<rbrace>"
|
||||
by (wp ct_idle_or_in_cur_domain'_lift hoare_vcg_disj_lift)
|
||||
|
||||
lemma setObject_pml4e_ksDomScheduleIdx [wp]:
|
||||
"\<lbrace>\<lambda>s. P (ksDomScheduleIdx s)\<rbrace> setObject p (pml4e::pml4e) \<lbrace>\<lambda>_. \<lambda>s. P (ksDomScheduleIdx s)\<rbrace>"
|
||||
by (wp updateObject_default_inv|simp add:setObject_def | wpc)+
|
||||
|
||||
crunch ksDomScheduleIdx[wp]: storePTE, storePDE, storePDPTE, storePML4E "\<lambda>s. P (ksDomScheduleIdx s)"
|
||||
(ignore: getObject setObject)
|
||||
|
||||
crunch gsMaxObjectSize[wp]: storePTE, storePDE "\<lambda>s. P (gsMaxObjectSize s)"
|
||||
crunch gsMaxObjectSize[wp]: storePTE, storePDE, storePDPTE, storePML4E "\<lambda>s. P (gsMaxObjectSize s)"
|
||||
(ignore: getObject setObject wp: setObject_ksPSpace_only updateObject_default_inv)
|
||||
|
||||
crunch gsUntypedZeroRanges[wp]: storePTE, storePDE "\<lambda>s. P (gsUntypedZeroRanges s)"
|
||||
crunch gsUntypedZeroRanges[wp]: storePTE, storePDE, storePDPTE, storePML4E "\<lambda>s. P (gsUntypedZeroRanges s)"
|
||||
(ignore: getObject setObject wp: setObject_ksPSpace_only updateObject_default_inv)
|
||||
|
||||
lemma storePDE_invs[wp]:
|
||||
"\<lbrace>invs' and valid_pde' pde
|
||||
and (\<lambda>s. valid_pde_mapping' (p && mask pdBits) pde)\<rbrace>
|
||||
"\<lbrace>invs' and valid_pde' pde\<rbrace>
|
||||
storePDE p pde
|
||||
\<lbrace>\<lambda>_. invs'\<rbrace>"
|
||||
apply (simp add: invs'_def valid_state'_def valid_pspace'_def)
|
||||
|
|
@ -2672,13 +2764,6 @@ lemma setASIDPool_irq_states' [wp]:
|
|||
apply assumption
|
||||
done
|
||||
|
||||
lemma setObject_asidpool_mappings'[wp]:
|
||||
"\<lbrace>valid_pde_mappings'\<rbrace> setObject p (ap::asidpool) \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace>"
|
||||
apply (wp valid_pde_mappings_lift')
|
||||
apply (rule obj_at_setObject2)
|
||||
apply (clarsimp dest!: updateObject_default_result)
|
||||
apply assumption
|
||||
done
|
||||
|
||||
lemma setASIDPool_vms'[wp]:
|
||||
"\<lbrace>valid_machine_state'\<rbrace> setObject p (ap::asidpool) \<lbrace>\<lambda>_. valid_machine_state'\<rbrace>"
|
||||
|
|
@ -2853,10 +2938,8 @@ lemma mapM_x_storePTE_invs:
|
|||
done
|
||||
|
||||
lemma mapM_x_storePDE_invs:
|
||||
"\<lbrace>invs' and valid_pde' pde
|
||||
and K (\<forall>p \<in> set ps. valid_pde_mapping' (p && mask pdBits) pde)\<rbrace>
|
||||
"\<lbrace>invs' and valid_pde' pde \<rbrace>
|
||||
mapM_x (swp storePDE pde) ps \<lbrace>\<lambda>xa. invs'\<rbrace>"
|
||||
apply (rule hoare_gen_asm)
|
||||
apply (rule hoare_post_imp)
|
||||
prefer 2
|
||||
apply (rule mapM_x_wp[OF _ subset_refl])
|
||||
|
|
|
|||
Loading…
Reference in New Issue