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

arch_split: Refine: fixup some qualified references

This commit is contained in:
Matthew Brecknell 2016-05-02 16:11:13 +10:00
parent 8f489e14fa
commit 33b4848061
9 changed files with 96 additions and 56 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
proof/drefine/Arch_DR.thy
View File

@ -159,7 +159,7 @@ lemma dcorres_lookup_pt_slot:
apply (rule corres_guard_imp)
apply (rule corres_split[OF _ dcorres_get_pde])
apply (rule_tac F = "case rv' of ARM_A.pde.PageTablePDE ptab x xa \<Rightarrow>
is_aligned (ARM.ptrFromPAddr ptab) 10 | _ \<Rightarrow> True"
is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True"
in corres_gen_asm2)
apply (case_tac rv')
prefer 2
@ -395,7 +395,7 @@ proof -
apply (clarsimp simp: obj_at_def a_type_def del: disjCI)
apply (clarsimp split: Structures_A.kernel_object.split_asm split_if_asm
arch_kernel_obj.split_asm del: disjCI)
apply (frule_tac p="ARM.ptrFromPAddr v" for v in pspace_alignedD, simp+)
apply (frule_tac p="ptrFromPAddr v" for v in pspace_alignedD, simp+)
apply (rule disjI2, rule conjI)
apply (rule_tac x="unat (lookup_pd_slot pd_ptr vptr && mask pd_bits >> 2)"
in exI)
@ -438,14 +438,14 @@ proof -
apply (clarsimp simp: obj_at_def a_type_def del: disjCI)
apply (clarsimp split: Structures_A.kernel_object.split_asm split_if_asm
arch_kernel_obj.split_asm del: disjCI)
apply (frule_tac p="ARM.ptrFromPAddr v" for v in pspace_alignedD, simp+)
apply (frule_tac p="ptrFromPAddr v" for v in pspace_alignedD, simp+)
apply (rule map_includedI)
apply (clarsimp simp: transform_pt_slot_ref_def all_pd_pt_slots_def
opt_object_page_directory[unfolded opt_object_def]
object_slots_def transform_page_directory_contents_def
unat_map_def kernel_pde_mask_def
del: disjCI UnCI)
apply (subgoal_tac "x && ~~ mask pt_bits = ARM.ptrFromPAddr word1")
apply (subgoal_tac "x && ~~ mask pt_bits = ptrFromPAddr word1")
apply (rule disjI2, rule conjI)
apply (rule_tac x="unat (lookup_pd_slot pd_ptr vptr && mask pd_bits >> 2)"
in exI)

12
proof/drefine/Finalise_DR.thy
View File

@ -596,7 +596,7 @@ lemma invalidate_hw_asid_entry_dwp[wp]:
done
lemma set_current_pd_dwp[wp]:
" \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> setCurrentPD (ARM.addrFromPPtr x) \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>"
" \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> setCurrentPD (addrFromPPtr x) \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>"
by (clarsimp simp:setCurrentPD_def writeTTBR0_def isb_def dsb_def,wp)
lemma set_hardware_asid_dwp[wp]:
@ -911,28 +911,28 @@ definition pd_pt_relation :: "word32\<Rightarrow>word32\<Rightarrow>word32\<Righ
where "pd_pt_relation pd pt offset s \<equiv>
\<exists>fun u v ref. ( kheap s pd = Some (ArchObj (arch_kernel_obj.PageDirectory fun))
\<and> page_table_at pt s \<and> fun (ucast (offset && mask pd_bits >> 2)) = ARM_A.pde.PageTablePDE ref u v
\<and> pt = ARM.ptrFromPAddr ref )"
\<and> pt = ptrFromPAddr ref )"
definition pd_section_relation :: "word32\<Rightarrow>word32\<Rightarrow>word32\<Rightarrow>'z::state_ext state\<Rightarrow>bool"
where "pd_section_relation pd pt offset s \<equiv>
\<exists>fun u v ref1 ref2. ( kheap s pd = Some (ArchObj (arch_kernel_obj.PageDirectory fun))
\<and> fun (ucast (offset && mask pd_bits >> 2)) = ARM_A.pde.SectionPDE ref1 u ref2 v
\<and> pt = ARM.ptrFromPAddr ref1 )"
\<and> pt = ptrFromPAddr ref1 )"
definition pd_super_section_relation :: "word32\<Rightarrow>word32\<Rightarrow>word32\<Rightarrow>'z::state_ext state\<Rightarrow>bool"
where "pd_super_section_relation pd pt offset s \<equiv>
\<exists>fun u v ref1. ( kheap s pd = Some (ArchObj (arch_kernel_obj.PageDirectory fun))
\<and> fun (ucast (offset && mask pd_bits >> 2)) = ARM_A.pde.SuperSectionPDE ref1 u v
\<and> pt = ARM.ptrFromPAddr ref1 )"
\<and> pt = ptrFromPAddr ref1 )"
definition pt_page_relation :: "word32\<Rightarrow>word32\<Rightarrow>word32\<Rightarrow>vmpage_size set\<Rightarrow>'z::state_ext state\<Rightarrow>bool"
where "pt_page_relation pt page offset S s \<equiv>
\<exists>fun. (kheap s pt = Some (ArchObj (arch_kernel_obj.PageTable fun)))
\<and> (case fun (ucast (offset && mask pt_bits >> 2)) of
ARM_A.pte.LargePagePTE ref fun1 fun2 \<Rightarrow>
page = ARM.ptrFromPAddr ref \<and> ARMLargePage \<in> S
page = ptrFromPAddr ref \<and> ARMLargePage \<in> S
| ARM_A.pte.SmallPagePTE ref fun1 fun2 \<Rightarrow>
page = ARM.ptrFromPAddr ref \<and> ARMSmallPage \<in> S
page = ptrFromPAddr ref \<and> ARMSmallPage \<in> S
| _ \<Rightarrow> False)"
lemma slot_with_pt_frame_relation:

36
proof/refine/Arch_R.thy
View File

@ -345,7 +345,7 @@ lemma pac_corres:
by (fastforce simp:cte_wp_at_ctes_of)+
definition
archinv_relation :: "arch_invocation \<Rightarrow> ARM_H.invocation \<Rightarrow> bool"
archinv_relation :: "arch_invocation \<Rightarrow> Arch.invocation \<Rightarrow> bool"
where
"archinv_relation ai ai' \<equiv> case ai of
arch_invocation.InvokePageTable pti \<Rightarrow>
@ -360,7 +360,7 @@ where
\<exists>ap'. ai' = InvokeASIDPool ap' \<and> ap' = asid_pool_invocation_map ap"
definition
valid_arch_inv' :: "ARM_H.invocation \<Rightarrow> kernel_state \<Rightarrow> bool"
valid_arch_inv' :: "Arch.invocation \<Rightarrow> kernel_state \<Rightarrow> bool"
where
"valid_arch_inv' ai \<equiv> case ai of
InvokePageTable pti \<Rightarrow> valid_pti' pti
@ -436,7 +436,7 @@ end
lemmas (in Arch) decodeInvocation_def = ARM_H.decodeInvocation_def
context begin interpretation Arch . (*FIXME: arch_split*)
crunch inv [wp]: "ARM_H.decodeInvocation" "P"
crunch inv [wp]: "Arch.decodeInvocation" "P"
(wp: crunch_wps mapME_x_inv_wp getASID_wp
simp: forME_x_def crunch_simps
ARMMMU_improve_cases
@ -847,7 +847,7 @@ shows
(\<lambda>s. vs_valid_duplicates' (ksPSpace s)))
(arch_decode_invocation (mi_label mi) args (to_bl cptr') slot
arch_cap excaps)
(ARM_H.decodeInvocation (mi_label mi) args cptr'
(Arch.decodeInvocation (mi_label mi) args cptr'
(cte_map slot) arch_cap' excaps')"
apply (simp add: arch_decode_invocation_def
ARM_H.decodeInvocation_def
@ -1294,7 +1294,7 @@ lemma inv_arch_corres:
corres (intr \<oplus> op=)
(einvs and ct_active and valid_arch_inv ai)
(invs' and ct_active' and valid_arch_inv' ai' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)))
(arch_perform_invocation ai) (ARM_H.performInvocation ai')"
(arch_perform_invocation ai) (Arch.performInvocation ai')"
apply (clarsimp simp: arch_perform_invocation_def
ARM_H.performInvocation_def
performARMMMUInvocation_def)
@ -1384,7 +1384,7 @@ lemma performASIDControlInvocation_tcb_at':
lemma invokeArch_tcb_at':
"\<lbrace>invs' and valid_arch_inv' ai and ct_active' and st_tcb_at' active' p\<rbrace>
ARM_H.performInvocation ai
Arch.performInvocation ai
\<lbrace>\<lambda>rv. tcb_at' p\<rbrace>"
apply (simp add: ARM_H.performInvocation_def performARMMMUInvocation_def)
apply (cases ai, simp_all)
@ -1774,7 +1774,7 @@ lemma arch_decodeInvocation_wf[wp]:
cte_wp_at' (diminished' (ArchObjectCap arch_cap) o cteCap) slot and
(\<lambda>s. \<forall>x \<in> set excaps. cte_wp_at' (diminished' (fst x) o cteCap) (snd x) s) and
sch_act_simple and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace>
ARM_H.decodeInvocation label args cap_index slot arch_cap excaps
Arch.decodeInvocation label args cap_index slot arch_cap excaps
\<lbrace>valid_arch_inv'\<rbrace>,-"
apply (cases arch_cap)
apply (simp add: decodeARMMMUInvocation_def ARM_H.decodeInvocation_def
@ -2015,7 +2015,7 @@ crunch nosch [wp]: performARMMMUInvocation "\<lambda>s. P (ksSchedulerAction s)"
lemma arch_pinv_nosch[wp]:
"\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace>
ARM_H.performInvocation invok
Arch.performInvocation invok
\<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>"
by (simp add: ARM_H.performInvocation_def) wp
@ -2073,7 +2073,7 @@ lemma performASIDControlInvocation_st_tcb_at':
lemma arch_pinv_st_tcb_at':
"\<lbrace>valid_arch_inv' ai and st_tcb_at' (P and op \<noteq> Inactive and op \<noteq> IdleThreadState) t and
invs' and ct_active'\<rbrace>
ARM_H.performInvocation ai
Arch.performInvocation ai
\<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace>" (is "?pre (pi ai) ?post")
proof(cases ai)
txt {* The preservation rules for each invocation have already been proved by crunch, so
@ -2103,26 +2103,28 @@ next
wp performPageDirectoryInvocation_st_tcb_at', fastforce elim!: pred_tcb'_weakenE)
qed
crunch aligned': "ARM_H.finaliseCap" pspace_aligned'
crunch aligned': "Arch.finaliseCap" pspace_aligned'
(ignore: getObject wp: crunch_wps getASID_wp simp: crunch_simps)
lemmas arch_finalise_cap_aligned' = finaliseCap_aligned'
crunch distinct': "ARM_H.finaliseCap" pspace_distinct'
crunch distinct': "Arch.finaliseCap" pspace_distinct'
(ignore: getObject wp: crunch_wps getASID_wp simp: crunch_simps)
lemmas arch_finalise_cap_distinct' = finaliseCap_distinct'
crunch nosch [wp]: "ARM_H.finaliseCap" "\<lambda>s. P (ksSchedulerAction s)"
crunch nosch [wp]: "Arch.finaliseCap" "\<lambda>s. P (ksSchedulerAction s)"
(ignore: getObject wp: crunch_wps getASID_wp simp: crunch_simps updateObject_default_def)
end
(* FIXME: arch_split crunch bug *)
lemmas (in Arch) finaliseCap_def = ARM_H.finaliseCap_def
context Arch begin global_naming ARM_H''
lemmas finaliseCap_def = ARM_H.finaliseCap_def
end
context begin interpretation Arch . (*FIXME: arch_split*)
crunch st_tcb_at' [wp]: "ARM_H.finaliseCap" "st_tcb_at' P t"
crunch st_tcb_at' [wp]: "Arch.finaliseCap" "st_tcb_at' P t"
(ignore: getObject setObject wp: crunch_wps getASID_wp simp: crunch_simps)
end
@ -2131,10 +2133,10 @@ shadow_facts (in Arch) finaliseCap_def
context begin interpretation Arch . (*FIXME: arch_split*)
crunch typ_at' [wp]: "ARM_H.finaliseCap" "\<lambda>s. P (typ_at' T p s)"
crunch typ_at' [wp]: "Arch.finaliseCap" "\<lambda>s. P (typ_at' T p s)"
(ignore: getObject setObject wp: crunch_wps getASID_wp simp: crunch_simps)
crunch cte_wp_at': "ARM_H.finaliseCap" "cte_wp_at' P p"
crunch cte_wp_at': "Arch.finaliseCap" "cte_wp_at' P p"
(ignore: getObject setObject wp: crunch_wps getASID_wp simp: crunch_simps)
lemma invs_asid_table_strenghten':
@ -2300,7 +2302,7 @@ lemma performPageDirectoryInvocation_invs'[wp]:
lemma arch_performInvocation_invs':
"\<lbrace>invs' and ct_active' and valid_arch_inv' invocation\<rbrace>
ARM_H.performInvocation invocation
Arch.performInvocation invocation
\<lbrace>\<lambda>rv. invs'\<rbrace>"
unfolding ARM_H.performInvocation_def
by (cases invocation,

70
proof/refine/CNodeInv_R.thy
View File

@ -6954,22 +6954,28 @@ crunch st_tcb_at'[wp]: emptySlot "st_tcb_at' P t" (simp: case_Null_If)
end
lemmas (in Arch) finaliseCap_def = ARM_H.finaliseCap_def (*FIXME: arch_split crunch bug*)
(*FIXME: arch_split crunch bug*)
context Arch begin global_naming ARM_H'''
lemmas finaliseCap_def = ARM_H.finaliseCap_def
end
(* FIXME: move to Finalise_R *)
context begin interpretation Arch . (*FIXME: arch_split*)
crunch st_tcb_at'[wp]: "Arch.finaliseCap", unbindMaybeNotification "st_tcb_at' P t"
(ignore: getObject setObject simp: crunch_simps
wp: crunch_wps getObject_inv loadObject_default_inv)
end
shadow_facts (in Arch) finaliseCap_def
context begin interpretation Arch . (*FIXME: arch_split*)
(* FIXME: move to Finalise_R *)
crunch st_tcb_at'[wp]: "ARM_H.finaliseCap", unbindMaybeNotification "st_tcb_at' P t"
(ignore: getObject setObject simp: crunch_simps
wp: crunch_wps getObject_inv loadObject_default_inv)
(* FIXME: arch_split: is there a better way to refer to Retype_H.finaliseCap_def? *)
lemma finaliseCap2_st_tcb_at':
assumes x[simp]: "\<And>st. simple' st \<Longrightarrow> P st"
shows "\<lbrace>st_tcb_at' P t\<rbrace>
finaliseCap cap final flag
\<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace>"
apply (simp add: Retype_H.finaliseCap_def Let_def
apply (simp add: finaliseCap_def Let_def
getThreadCSpaceRoot deletingIRQHandler_def
cong: if_cong split del: split_if)
apply (rule hoare_pre)
@ -7065,12 +7071,26 @@ lemmas threadSet_ctesCaps_of = ctes_of_cteCaps_of_lift[OF threadSet_ctes_of]
lemmas storePTE_cteCaps_of[wp] = ctes_of_cteCaps_of_lift [OF storePTE_ctes]
lemmas storePDE_cteCaps_of[wp] = ctes_of_cteCaps_of_lift [OF storePDE_ctes]
end
(*FIXME: arch_split crunch bug getting ridiculous *)
context Arch begin global_naming ARM_H''''
lemmas finaliseCap_def = ARM_H.finaliseCap_def
end
(* FIXME: move to Finalise_R *)
context begin interpretation Arch . (*FIXME: arch_split*)
crunch rvk_prog': finaliseCap
"\<lambda>s. revoke_progress_ord m (\<lambda>x. option_map capToRPO (cteCaps_of s x))"
(wp: crunch_wps emptySlot_rvk_prog' threadSet_ctesCaps_of
getObject_inv loadObject_default_inv
simp: crunch_simps unless_def setBoundNotification_def
ignore: getObject setObject setCTE)
end
shadow_facts (in Arch) finaliseCap_def
context begin interpretation Arch . (*FIXME: arch_split*)
lemmas finalise_induct3 = finaliseSlot'.induct[where P=
"\<lambda>sl exp s. P sl (finaliseSlot' sl exp) s" for P]
@ -8324,11 +8344,15 @@ end
lemmas (in Arch) recycleCap_def = ARM_H.recycleCap_def
context begin interpretation Arch . (*FIXME: arch_split*)
crunch st_tcb_at'[wp]: "ARM_H.recycleCap" "st_tcb_at' P t"
crunch st_tcb_at'[wp]: "Arch.recycleCap" "st_tcb_at' P t"
(ignore: getObject setObject
wp: crunch_wps undefined_valid
simp: crunch_simps arch_recycleCap_improve_cases')
end
shadow_facts (in Arch) recycleCap_def
context begin interpretation Arch . (*FIXME: arch_split*)
lemma threadSet_st_tcb_at2:
assumes x: "\<forall>tcb. P (tcbState tcb) \<longrightarrow> P (tcbState (f tcb))"
@ -9523,7 +9547,7 @@ lemmas arch_recycleCap_improve_cases'' = arch_recycleCap_improve_cases'[simplifi
lemma arch_recycleCap_valid[wp]:
"\<lbrace>valid_cap' (ArchObjectCap cap) and valid_objs'\<rbrace>
ARM_H.recycleCap is_final cap
Arch.recycleCap is_final cap
\<lbrace>valid_cap' \<circ> capability.ArchObjectCap\<rbrace>"
apply (simp add: ARM_H.recycleCap_def Let_def
arch_recycleCap_improve_cases
@ -9547,12 +9571,18 @@ lemma recycleCap_valid[wp]:
apply (auto simp: isCap_simps valid_cap'_def capAligned_def objBits_simps)
done
end
(*FIXME: arch_split crunch bug *)
context Arch begin global_naming ARM_H'
lemmas recycleCap_def = ARM_H.recycleCap_def
end
context begin interpretation Arch . (*FIXME: arch_split*)
crunch cte_wp_at'[wp]: recycleCap "cte_wp_at' P p"
(ignore: filterM setObject getObject
simp: filterM_mapM crunch_simps arch_recycleCap_improve_cases'
wp: crunch_wps)
end
(*FIXME: arch_split crunch bug *)
@ -9568,7 +9598,7 @@ lemma recycleCap_cases:
ZombieTCB \<Rightarrow> isThreadCap rv
| ZombieCNode n \<Rightarrow> isCNodeCap rv)
\<and> capUntypedPtr rv = capUntypedPtr cap)\<rbrace>"
apply (simp add: Retype_H.recycleCap_def Let_def ARM_H.recycleCap_def
apply (simp add: recycleCap_def Let_def ARM_H.recycleCap_def
arch_recycleCap_improve_cases
split del: split_if cong: if_cong)
apply (rule hoare_pre)
@ -9728,12 +9758,26 @@ declare withoutPreemption_lift [wp]
crunch irq_states' [wp]: capSwapForDelete valid_irq_states'
end
(*FIXME: arch_split crunch bug*)
context Arch begin global_naming ARM_H'''''
lemmas finaliseCap_def = ARM_H.finaliseCap_def
end
(* FIXME: move to Finalise_R *)
context begin interpretation Arch . (*FIXME: arch_split*)
crunch irq_states' [wp]: finaliseCap valid_irq_states'
(wp: crunch_wps hoare_unless_wp getASID_wp no_irq
no_irq_invalidateTLB_ASID no_irq_setHardwareASID
no_irq_setCurrentPD no_irq_invalidateTLB_VAASID
no_irq_cleanByVA_PoU
simp: crunch_simps armv_contextSwitch_HWASID_def ignore: getObject setObject)
end
shadow_facts (in Arch) finaliseCap_def
context begin interpretation Arch . (*FIXME: arch_split*)
lemma finaliseSlot_IRQInactive':
"s \<turnstile> \<lbrace>valid_irq_states'\<rbrace> finaliseSlot' a b

9
proof/refine/Orphanage.thy
View File

@ -13,9 +13,6 @@ imports Refine
begin
context Arch begin
requalify_facts
switchToIdleThread_def
switchToThread_def
shadow_facts
switchToIdleThread_def
switchToThread_def
@ -592,7 +589,7 @@ lemma ArchThreadDecls_H_switchToThread_all_queued_tcb_ptrs [wp]:
"\<lbrace> \<lambda>s. P (all_queued_tcb_ptrs s) \<rbrace>
Arch.switchToThread tcb_ptr
\<lbrace> \<lambda>rv s. P (all_queued_tcb_ptrs s) \<rbrace>"
unfolding Arch.switchToThread_def all_queued_tcb_ptrs_def
unfolding ARM_H.switchToThread_def all_queued_tcb_ptrs_def
apply (wp | clarsimp)+
done
@ -1688,7 +1685,7 @@ lemma arch_finaliseCap_no_orphans [wp]:
"\<lbrace> \<lambda>s. no_orphans s \<rbrace>
Arch.finaliseCap cap fin
\<lbrace> \<lambda>rv s. no_orphans s \<rbrace>"
unfolding Arch.finaliseCap_def
unfolding ARM_H.finaliseCap_def
apply (rule hoare_pre)
apply (wp | wpc | clarsimp)+
done
@ -1990,7 +1987,7 @@ lemma invokeIRQControl_no_orphans [wp]:
"\<lbrace> \<lambda>s. no_orphans s \<rbrace>
performIRQControl i
\<lbrace> \<lambda>rv s. no_orphans s \<rbrace>"
apply (cases i, simp_all add: performIRQControl_def Arch.performIRQControl_def)
apply (cases i, simp_all add: performIRQControl_def ARM_H.performIRQControl_def)
apply (wp | clarsimp)+
done

10
proof/refine/PageTableDuplicates.thy
View File

@ -1145,9 +1145,9 @@ lemma valid_duplicates'_update:
lemma createObject_valid_duplicates'[wp]:
"\<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct'
and pspace_no_overlap' ptr (ARM_H.getObjectSize ty us)
and pspace_no_overlap' ptr (getObjectSize ty us)
and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits)
and K (is_aligned ptr (ARM_H.getObjectSize ty us))
and K (is_aligned ptr (getObjectSize ty us))
and K (ty = APIObjectType apiobject_type.CapTableObject \<longrightarrow> us < 28)\<rbrace>
RetypeDecls_H.createObject ty ptr us
\<lbrace>\<lambda>xa s. vs_valid_duplicates' (ksPSpace s)\<rbrace>"
@ -1277,7 +1277,7 @@ context begin interpretation Arch . (*FIXME: arch_split*)
lemma createNewObjects_valid_duplicates'[wp]:
"\<lbrace> (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_no_overlap' ptr sz
and pspace_aligned' and pspace_distinct' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits)
and K (range_cover ptr sz (ARM_H.getObjectSize ty us) (length dest) \<and>
and K (range_cover ptr sz (getObjectSize ty us) (length dest) \<and>
ptr \<noteq> 0 \<and> (ty = APIObjectType apiobject_type.CapTableObject \<longrightarrow> us < 28) ) \<rbrace>
createNewObjects ty src dest ptr us
\<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>"
@ -1810,7 +1810,7 @@ crunch valid_duplicates'[wp]:
lemma archFinaliseCap_valid_duplicates'[wp]:
"\<lbrace>valid_objs' and pspace_aligned' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))
and (valid_cap' (capability.ArchObjectCap arch_cap))\<rbrace>
ARM_H.finaliseCap arch_cap is_final
Arch.finaliseCap arch_cap is_final
\<lbrace>\<lambda>ya a. vs_valid_duplicates' (ksPSpace a)\<rbrace>"
apply (case_tac arch_cap,simp_all add:ARM_H.finaliseCap_def)
apply (rule hoare_pre)
@ -2327,7 +2327,7 @@ lemma setASIDPool_valid_duplicates':
lemma performArchInvocation_valid_duplicates':
"\<lbrace>invs' and valid_arch_inv' ai and ct_active' and st_tcb_at' active' p
and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace>
ARM_H.performInvocation ai
Arch.performInvocation ai
\<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>"
apply (simp add: ARM_H.performInvocation_def performARMMMUInvocation_def)
apply (cases ai, simp_all)

2
proof/refine/Schedule_R.thy
View File

@ -963,8 +963,6 @@ proof -
done
show ?thesis
apply (rule P_bool_lift [OF pos])
thm lift_neg_pred_tcb_at'
by (rule lift_neg_pred_tcb_at' [OF ArchThreadDecls_H_ARM_H_switchToThread_typ_at' pos])
qed

2
proof/refine/Syscall_R.thy
View File

@ -2422,7 +2422,7 @@ lemma inv_irq_IRQInactive:
done
lemma inv_arch_IRQInactive:
"\<lbrace>\<top>\<rbrace> ARM_H.performInvocation invocation
"\<lbrace>\<top>\<rbrace> Arch.performInvocation invocation
-, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace>"
apply (simp add: ARM_H.performInvocation_def performARMMMUInvocation_def)
apply wp

3
proof/refine/Tcb_R.thy
View File

@ -1417,9 +1417,8 @@ lemma setSchedulerAction_invs'[wp]:
end
(*FIXME: arch_split*)
consts
copyregsets_map :: "arch_copy_register_sets \<Rightarrow> ARM_H.copy_register_sets"
copyregsets_map :: "arch_copy_register_sets \<Rightarrow> Arch.copy_register_sets"
context begin interpretation Arch . (*FIXME: arch_split*)