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

x64: clear some sorry proofs from CSpace_C 

Also update some Haskell and abstract specs relating to IO ports.
This commit is contained in:
Matthew Brecknell 2018-02-02 10:40:38 +11:00 committed by Joel Beeren
parent b072714ca1
commit bcac2c8492
20 changed files with 711 additions and 1365 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

21
lib/Word_Lib/Word_Lemmas.thy
View File

@ -3753,6 +3753,11 @@ lemma ucast_mono_le:
apply (simp add: word_le_nat_alt)
done
lemma ucast_mono_le':
"\<lbrakk> unat y < 2 ^ LENGTH('b); LENGTH('b::len) < LENGTH('a::len); x \<le> y \<rbrakk>
\<Longrightarrow> UCAST('a \<rightarrow> 'b) x \<le> UCAST('a \<rightarrow> 'b) y"
by (auto simp: word_less_nat_alt intro: ucast_mono_le)
lemma zero_sle_ucast_up:
"\<not> is_down (ucast :: 'a word \<Rightarrow> 'b signed word) \<Longrightarrow>
(0 <=s ((ucast (b::('a::len) word)) :: ('b::len) signed word))"
@ -5418,6 +5423,22 @@ lemma ucast_le_ucast:
apply simp
done
lemma ucast_le_ucast_eq:
fixes x y :: "'a::len word"
assumes x: "x < 2 ^ n"
assumes y: "y < 2 ^ n"
assumes n: "n = LENGTH('b::len)"
shows "(UCAST('a \<rightarrow> 'b) x \<le> UCAST('a \<rightarrow> 'b) y) = (x \<le> y)"
apply (rule iffI)
apply (cases "LENGTH('b) < LENGTH('a)")
apply (subst less_mask_eq[OF x, symmetric])
apply (subst less_mask_eq[OF y, symmetric])
apply (unfold n)
apply (subst ucast_ucast_mask[symmetric])+
apply (simp add: ucast_le_ucast)+
apply (erule ucast_mono_le[OF _ y[unfolded n]])
done
(* High bits w.r.t. mask operations. *)
lemma and_neg_mask_eq_iff_not_mask_le:

13
proof/crefine/X64/CSpaceAcc_C.thy
View File

@ -260,11 +260,11 @@ lemma updateMDB_pre_cte_at:
lemma getSlotCap_pre_cte_at:
"\<lbrace>\<lambda>s. \<not> cte_at' p s \<rbrace> getSlotCap p \<lbrace> \<lambda>_ _. False \<rbrace>"
unfolding getSlotCap_def
apply simp
apply (wp getCTE_wp)
apply clarsimp
done
unfolding getSlotCap_def by (wpsimp wp: getCTE_wp)
lemma updateCap_pre_cte_at:
"\<lbrace>\<lambda>s. \<not> cte_at' p s \<rbrace> updateCap p f \<lbrace> \<lambda>_ _. False \<rbrace>"
unfolding updateCap_def by (wpsimp wp: getCTE_wp)
lemmas ccorres_updateMDB_cte_at = ccorres_guard_from_wp [OF updateMDB_pre_cte_at empty_fail_updateMDB]
ccorres_guard_from_wp_bind [OF updateMDB_pre_cte_at empty_fail_updateMDB]
@ -272,6 +272,9 @@ lemmas ccorres_updateMDB_cte_at = ccorres_guard_from_wp [OF updateMDB_pre_cte_at
lemmas ccorres_getSlotCap_cte_at = ccorres_guard_from_wp [OF getSlotCap_pre_cte_at empty_fail_getSlotCap]
ccorres_guard_from_wp_bind [OF getSlotCap_pre_cte_at empty_fail_getSlotCap]
lemmas ccorres_updateCap_cte_at = ccorres_guard_from_wp [OF updateCap_pre_cte_at empty_fail_updateCap]
ccorres_guard_from_wp_bind [OF updateCap_pre_cte_at empty_fail_updateCap]
lemma wordFromRights_spec:
defines "crl s \<equiv> (seL4_CapRights_lift \<^bsup>s\<^esup>seL4_CapRights)"
shows "\<forall>s. \<Gamma> \<turnstile> {s} \<acute>ret__unsigned_long :== PROC wordFromRights(\<acute>seL4_CapRights)

1702
proof/crefine/X64/CSpace_C.thy
View File

File diff suppressed because it is too large Load Diff

8
proof/crefine/X64/Interrupt_C.thy
View File

@ -57,7 +57,7 @@ lemma cte_at_irq_node':
cte_at' (irq_node' s + 2 ^ cte_level_bits * ucast (irq :: 8 word)) s"
by (clarsimp simp: invs'_def valid_state'_def valid_irq_node'_def
cte_level_bits_def real_cte_at')
thm Collect_const
lemma invokeIRQHandler_SetIRQHandler_ccorres:
"ccorres dc xfdc
(invs' and sch_act_simple
@ -79,8 +79,8 @@ proof -
apply (ctac(no_vcg) add: cteDeleteOne_ccorres[where w="-1"])
apply (ctac(no_vcg) add: cteInsert_ccorres)
apply (simp add: pred_conj_def)
apply (strengthen ntfn_badge_derived_enough_strg[unfolded o_def]
invs_mdb_strengthen' valid_objs_invs'_strg)
apply (strengthen invs_mdb_strengthen' valid_objs_invs'_strg
invs_pspace_canonical' invs_pspace_aligned')
apply (wp cteDeleteOne_other_cap[unfolded o_def])[1]
apply vcg
apply (rule conseqPre, vcg, clarsimp simp: rf_sr_def
@ -90,7 +90,7 @@ proof -
apply (simp add: guard_is_UNIV_def ghost_assertion_data_get_def
ghost_assertion_data_set_def)
apply (clarsimp simp: cte_at_irq_node' ucast_nat_def)
apply (clarsimp simp: invs_pspace_aligned' cte_wp_at_ctes_of badge_derived'_def
apply (clarsimp simp: cte_wp_at_ctes_of badge_derived'_def
Collect_const_mem unat_gt_0 valid_cap_simps' X64.maxIRQ_def)
apply (drule word_le_nat_alt[THEN iffD1])
apply (clarsimp simp:uint_0_iff unat_gt_0 uint_up_ucast is_up unat_def[symmetric])

22
proof/crefine/X64/Invoke_C.thy
View File

@ -299,7 +299,8 @@ lemma invokeCNodeCancelBadgedSends_ccorres:
lemma invokeCNodeInsert_ccorres:
"ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
(cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capMasterCap cap) src
and valid_mdb' and pspace_aligned' and valid_objs' and valid_cap' cap)
and valid_mdb' and pspace_aligned' and pspace_canonical'
and valid_objs' and valid_cap' cap)
(UNIV \<inter> {s. destSlot_' s = Ptr dest} \<inter>
{s. srcSlot_' s = Ptr src} \<inter>
{s. ccap_relation cap (cap_' s)}) []
@ -312,9 +313,7 @@ lemma invokeCNodeInsert_ccorres:
apply (rule allI, rule conseqPre,vcg) apply clarsimp apply (simp add: return_def)
apply wp
apply (clarsimp simp: cte_wp_at_ctes_of)
done
done
(************************************************************************)
@ -325,7 +324,7 @@ done
lemma invokeCNodeMove_ccorres:
"ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
(valid_mdb' and pspace_aligned' )
(valid_mdb' and pspace_aligned' and pspace_canonical')
(UNIV \<inter> {s. destSlot_' s = Ptr dest} \<inter>
{s. srcSlot_' s = Ptr src} \<inter>
{s. ccap_relation cap (cap_' s)}) []
@ -338,11 +337,7 @@ lemma invokeCNodeMove_ccorres:
apply (rule allI, rule conseqPre,vcg) apply clarsimp apply (simp add: return_def)
apply wp
apply clarsimp
done
done
(************************************************************************)
@ -351,8 +346,6 @@ done
(* *)
(************************************************************************)
lemma invokeCNodeRotate_ccorres:
"ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
(\<lambda>s. cte_at' slot1 s \<and> cte_at' slot2 s \<and> slot1 \<noteq> slot2
@ -404,7 +397,7 @@ lemma invokeCNodeRotate_ccorres:
lemma invokeCNodeSaveCaller_ccorres:
"ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
(valid_mdb' and pspace_aligned' and cur_tcb')
(valid_mdb' and pspace_aligned' and pspace_canonical' and cur_tcb')
(UNIV \<inter> {s. destSlot_' s = Ptr destSlot}) []
(invokeCNode (SaveCaller destSlot))
(Call invokeCNodeSaveCaller_'proc)"
@ -470,9 +463,6 @@ lemma invokeCNodeSaveCaller_ccorres:
done
(************************************************************************)
(* *)
(* decodeCNodeInvocation ***********************************************)

4
proof/crefine/X64/Ipc_C.thy
View File

@ -4892,7 +4892,7 @@ lemma setupCallerCap_ccorres [corres]:
tcb_cnode_index_defs)
apply simp
apply (rule_tac Q="\<lambda>rv. valid_pspace' and tcb_at' receiver" in hoare_post_imp)
apply (auto simp: cte_wp_at_ctes_of isCap_simps
apply (auto simp: cte_wp_at_ctes_of isCap_simps valid_pspace'_def
tcbSlots Kernel_C.tcbCaller_def size_of_def
cte_level_bits_def)[1]
apply (case_tac cte,clarsimp)
@ -4911,7 +4911,7 @@ lemma setupCallerCap_ccorres [corres]:
valid_tcb_state'_def Collect_const_mem
tcb_cnode_index_defs)
done
thm sendIPC_body_def
lemma sendIPC_dequeue_ccorres_helper:
"ep_ptr = Ptr ep ==>
ccorres (\<lambda>rv rv'. rv' = tcb_ptr_to_ctcb_ptr dest) dest___ptr_to_struct_tcb_C_'

81
proof/crefine/X64/SR_lemmas_C.thy
View File

@ -959,7 +959,7 @@ lemma cte_bits_le_3 [simp]: "3 \<le> cte_level_bits"
lemma cte_bits_le_tcb_bits: "cte_level_bits \<le> tcbBlockSizeBits"
by (simp add: cte_level_bits_def objBits_defs)
lemma ctes_of_aligned_bits [simp]:
lemma ctes_of_aligned_bits:
assumes pa: "pspace_aligned' s"
and cof: "ctes_of s p = Some cte"
and bits: "bits \<le> cte_level_bits"
@ -982,21 +982,12 @@ qed
lemma mdbNext_not_zero_eq:
"cmdbnode_relation n n' \<Longrightarrow> \<forall>s s'. (s, s') \<in> rf_sr (*ja \<and> (is_aligned (mdbNext n) 3)*)
\<longrightarrow> (mdbNext n \<noteq> 0) = (s' \<in> {_. mdbNext_CL (mdb_node_lift n') \<noteq> 0})"
apply clarsimp
apply (erule cmdbnode_relationE)
apply (fastforce simp: mdbNext_to_H)
done
by (fastforce elim: cmdbnode_relationE)
lemma mdbPrev_not_zero_eq:
"cmdbnode_relation n n' \<Longrightarrow> \<forall>s s'. (s, s') \<in> rf_sr (*ja\<and> (is_aligned (mdbPrev n) 3)*)
\<longrightarrow> (mdbPrev n \<noteq> 0) = (s' \<in> {_. mdbPrev_CL (mdb_node_lift n') \<noteq> 0})"
apply clarsimp
apply (erule cmdbnode_relationE)
apply (unfold mdb_node_to_H_def)
apply (fastforce)
done
declare is_aligned_0 [simp]
by (fastforce elim: cmdbnode_relationE)
abbreviation
"nullCapPointers cte \<equiv> cteCap cte = NullCap \<and> mdbNext (cteMDBNode cte) = nullPointer \<and> mdbPrev (cteMDBNode cte) = nullPointer"
@ -2199,6 +2190,72 @@ lemma cap_get_tag_isCap_ArchObject2:
simp add: cap_get_tag_isCap_ArchObject,
simp add: isArchCap_tag_def2 cap_tag_defs)+
schematic_goal cap_io_port_cap_lift_def':
"cap_get_tag cap = SCAST(32 signed \<rightarrow> 64) cap_io_port_cap
\<Longrightarrow> cap_io_port_cap_lift cap =
\<lparr> capIOPortFirstPort_CL = ?first,
capIOPortLastPort_CL = ?last \<rparr>"
by (simp add: cap_io_port_cap_lift_def cap_lift_def cap_tag_defs)
schematic_goal cap_frame_cap_lift_def':
"cap_get_tag cap = SCAST(32 signed \<rightarrow> 64) cap_frame_cap
\<Longrightarrow> cap_frame_cap_lift cap =
\<lparr> capFMappedASID_CL = ?mapped_asid,
capFBasePtr_CL = ?base_ptr,
capFSize_CL = ?frame_size,
capFMapType_CL = ?map_type,
capFMappedAddress_CL = ?mapped_address,
capFVMRights_CL = ?vm_rights,
capFIsDevice_CL = ?is_device \<rparr>"
by (simp add: cap_frame_cap_lift_def cap_lift_def cap_tag_defs)
lemmas ccap_rel_cap_get_tag_cases_generic =
cap_get_tag_isCap_unfolded_H_cap(1-11)
[OF back_subst[of "\<lambda>cap. ccap_relation cap cap'" for cap']]
lemmas ccap_rel_cap_get_tag_cases_arch =
cap_get_tag_isCap_unfolded_H_cap(12-19)
[OF back_subst[of "\<lambda>cap. ccap_relation (ArchObjectCap cap) cap'" for cap'],
OF back_subst[of "\<lambda>cap. ccap_relation cap cap'" for cap']]
lemmas ccap_rel_cap_get_tag_cases_arch' =
ccap_rel_cap_get_tag_cases_arch[OF _ refl]
lemmas cap_lift_defs =
cap_untyped_cap_lift_def
cap_endpoint_cap_lift_def
cap_notification_cap_lift_def
cap_reply_cap_lift_def
cap_cnode_cap_lift_def
cap_thread_cap_lift_def
cap_irq_handler_cap_lift_def
cap_zombie_cap_lift_def
cap_frame_cap_lift_def
cap_page_table_cap_lift_def
cap_page_directory_cap_lift_def
cap_pdpt_cap_lift_def
cap_pml4_cap_lift_def
cap_asid_pool_cap_lift_def
cap_io_port_cap_lift_def
lemma cap_lift_Some_CapD:
"\<And>c'. cap_lift c = Some (Cap_untyped_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_untyped_cap"
"\<And>c'. cap_lift c = Some (Cap_endpoint_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_endpoint_cap"
"\<And>c'. cap_lift c = Some (Cap_notification_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_notification_cap"
"\<And>c'. cap_lift c = Some (Cap_reply_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_reply_cap"
"\<And>c'. cap_lift c = Some (Cap_cnode_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_cnode_cap"
"\<And>c'. cap_lift c = Some (Cap_thread_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_thread_cap"
"\<And>c'. cap_lift c = Some (Cap_irq_handler_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_irq_handler_cap"
"\<And>c'. cap_lift c = Some (Cap_zombie_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_zombie_cap"
"\<And>c'. cap_lift c = Some (Cap_frame_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_frame_cap"
"\<And>c'. cap_lift c = Some (Cap_page_table_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_page_table_cap"
"\<And>c'. cap_lift c = Some (Cap_page_directory_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_page_directory_cap"
"\<And>c'. cap_lift c = Some (Cap_pdpt_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_pdpt_cap"
"\<And>c'. cap_lift c = Some (Cap_pml4_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_pml4_cap"
"\<And>c'. cap_lift c = Some (Cap_asid_pool_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_asid_pool_cap"
"\<And>c'. cap_lift c = Some (Cap_io_port_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_io_port_cap"
by (auto simp: cap_lifts cap_lift_defs)
lemma rf_sr_x64KSGlobalPML4:
"(s, s') \<in> rf_sr
\<Longrightarrow> x64KSGlobalPML4 (ksArchState s)

36
proof/crefine/X64/Tcb_C.thy
View File

@ -784,30 +784,22 @@ lemma invokeTCB_ThreadControl_ccorres:
apply simp
apply (rule hoare_strengthen_post[where
Q="\<lambda>a b. ((case snd (the buf) of None \<Rightarrow> 0 | Some x \<Rightarrow> snd x) \<noteq> 0 \<longrightarrow>
valid_cap' (fst (the (snd (the buf)))) b \<and>
invs' b \<and>
valid_cap' (capability.ThreadCap target) b \<and>
(cte_wp_at'
(\<lambda>a. is_derived' (ctes_of b) (snd (the (snd (the buf)))) (fst (the (snd (the buf)))) (cteCap a))
(snd (the (snd (the buf)))) b \<longrightarrow>
cte_wp_at'
(\<lambda>scte. capMasterCap (cteCap scte) = capMasterCap (fst (the (snd (the buf)))) \<or>
is_simple_cap' (fst (the (snd (the buf)))))
(snd (the (snd (the buf)))) b \<and>
valid_mdb' b \<and>
valid_objs' b \<and>
pspace_aligned' b \<and>
cte_wp_at' (\<lambda>c. True) (snd (the (snd (the buf)))) b \<and>
Invariants_H.valid_queues b \<and>
sch_act_wf (ksSchedulerAction b) b)) \<and>
(target = ksCurThread b \<longrightarrow>
Invariants_H.valid_queues b \<and> weak_sch_act_wf (ksSchedulerAction b) b \<and> valid_objs' b)"])
valid_cap' (fst (the (snd (the buf)))) b \<and>
invs' b \<and>
valid_cap' (capability.ThreadCap target) b \<and>
(cte_wp_at'
(\<lambda>a. is_derived' (ctes_of b) (snd (the (snd (the buf)))) (fst (the (snd (the buf)))) (cteCap a))
(snd (the (snd (the buf)))) b \<longrightarrow>
cte_wp_at'
(\<lambda>scte. capMasterCap (cteCap scte) = capMasterCap (fst (the (snd (the buf)))) \<or>
is_simple_cap' (fst (the (snd (the buf)))))
(snd (the (snd (the buf)))) b \<and>
cte_wp_at' (\<lambda>c. True) (snd (the (snd (the buf)))) b)) \<and>
(target = ksCurThread b \<longrightarrow>
Invariants_H.valid_queues b \<and> weak_sch_act_wf (ksSchedulerAction b) b \<and> valid_objs' b)"])
prefer 2 subgoal by auto
apply (wp hoare_vcg_conj_lift)
apply (strengthen cte_is_derived_capMasterCap_strg
invs_queues invs_weak_sch_act_wf
invs_valid_objs' invs_mdb' invs_pspace_aligned',
simp add: o_def)
apply (strengthen cte_is_derived_capMasterCap_strg, simp add: o_def)
apply (wp static_imp_wp )
apply (wp hoare_drop_imp)
apply (wp hoare_drop_imp)

14
proof/crefine/X64/VSpace_C.thy
View File

@ -1264,20 +1264,6 @@ lemma invs'_invs_no_cicd:
"invs' s \<Longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s"
by (clarsimp simp add: invs'_def all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def newKernelState_def)
(* FIXME: move to StateRelation_C *)
definition
"framesize_from_H sz \<equiv> case sz of
X64.X64SmallPage \<Rightarrow> (scast Kernel_C.X86_SmallPage :: machine_word)
| X64.X64LargePage \<Rightarrow> scast Kernel_C.X86_LargePage
| X64.X64HugePage \<Rightarrow> scast Kernel_C.X64_HugePage"
lemma framesize_from_to_H:
"framesize_to_H (framesize_from_H sz) = sz"
by (simp add: framesize_to_H_def framesize_from_H_def
Kernel_C.X86_SmallPage_def Kernel_C.X86_LargePage_def
Kernel_C.X64_HugePage_def
split: if_split vmpage_size.splits)
lemma ccorres_seq_IF_False:
"ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (IF False THEN x ELSE y FI ;; c) = ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (y ;; c)"
by simp

21
proof/crefine/X64/Wellformed_C.thy
View File

@ -220,6 +220,27 @@ where
else if c = scast Kernel_C.X86_LargePage then X64LargePage
else X64HugePage"
definition
framesize_from_H :: "vmpage_size \<Rightarrow> machine_word"
where
"framesize_from_H sz \<equiv>
case sz of
X64SmallPage \<Rightarrow> scast Kernel_C.X86_SmallPage
| X64LargePage \<Rightarrow> scast Kernel_C.X86_LargePage
| X64HugePage \<Rightarrow> scast Kernel_C.X64_HugePage"
lemma framesize_from_to_H:
"framesize_to_H (framesize_from_H sz) = sz"
by (simp add: framesize_to_H_def framesize_from_H_def
Kernel_C.X86_SmallPage_def Kernel_C.X86_LargePage_def
Kernel_C.X64_HugePage_def
split: if_split vmpage_size.splits)
lemma framesize_from_H_eq:
"(framesize_from_H sz = framesize_from_H sz') = (sz = sz')"
by (cases sz; cases sz';
simp add: framesize_from_H_def X86_SmallPage_def X86_LargePage_def X64_HugePage_def)
definition
maptype_to_H :: "machine_word \<Rightarrow> vmmap_type"
where

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

@ -123,9 +123,7 @@ lemma same_arch_region_as_relation:
"\<lbrakk>acap_relation c d; acap_relation c' d'\<rbrakk> \<Longrightarrow>
arch_same_region_as c c' =
sameRegionAs (ArchObjectCap d) (ArchObjectCap d')"
apply (cases c)
by (((cases c', auto simp: X64_H.sameRegionAs_def sameRegionAs_def Let_def isCap_simps)[1])+)
by (cases c; cases c') (auto simp: X64_H.sameRegionAs_def sameRegionAs_def Let_def isCap_simps)
lemma is_phyiscal_relation:
"cap_relation c c' \<Longrightarrow> is_physical c = isPhysicalCap c'"

76
proof/refine/X64/CSpace_I.thy
View File

@ -649,30 +649,30 @@ lemma capMasterCap_simps[simp]:
"capMasterCap (NotificationCap ref bdg s r) = NotificationCap ref 0 True True"
"capMasterCap (CNodeCap ref bits gd gs) = CNodeCap ref bits 0 0"
"capMasterCap (ThreadCap ref) = ThreadCap ref"
"capMasterCap capability.NullCap = capability.NullCap"
"capMasterCap capability.DomainCap = capability.DomainCap"
"capMasterCap (capability.IRQHandlerCap irq) = capability.IRQHandlerCap irq"
"capMasterCap (capability.Zombie word zombie_type n) = capability.Zombie word zombie_type n"
"capMasterCap (capability.ArchObjectCap (arch_capability.ASIDPoolCap word1 word2)) =
capability.ArchObjectCap (arch_capability.ASIDPoolCap word1 0)"
"capMasterCap (capability.ArchObjectCap arch_capability.ASIDControlCap) =
capability.ArchObjectCap arch_capability.ASIDControlCap"
"capMasterCap (capability.ArchObjectCap (arch_capability.PageCap word vmrights mt vmpage_size d pdata)) =
capability.ArchObjectCap (arch_capability.PageCap word VMReadWrite VMNoMap vmpage_size d None)"
"capMasterCap (capability.ArchObjectCap (arch_capability.PageTableCap word ptdata)) =
capability.ArchObjectCap (arch_capability.PageTableCap word None)"
"capMasterCap (capability.ArchObjectCap (arch_capability.PageDirectoryCap word pddata)) =
capability.ArchObjectCap (arch_capability.PageDirectoryCap word None)"
"capMasterCap (capability.ArchObjectCap (arch_capability.PDPointerTableCap word pdptdata)) =
capability.ArchObjectCap (arch_capability.PDPointerTableCap word None)"
"capMasterCap (capability.ArchObjectCap (arch_capability.PML4Cap word pml4data)) =
capability.ArchObjectCap (arch_capability.PML4Cap word None)"
"capMasterCap (capability.ArchObjectCap (arch_capability.IOPortCap ft lt)) =
capability.ArchObjectCap (arch_capability.IOPortCap ft lt)"
"capMasterCap NullCap = NullCap"
"capMasterCap DomainCap = DomainCap"
"capMasterCap (IRQHandlerCap irq) = IRQHandlerCap irq"
"capMasterCap (Zombie word zombie_type n) = Zombie word zombie_type n"
"capMasterCap (ArchObjectCap (ASIDPoolCap word1 word2)) =
ArchObjectCap (ASIDPoolCap word1 0)"
"capMasterCap (ArchObjectCap ASIDControlCap) =
ArchObjectCap ASIDControlCap"
"capMasterCap (ArchObjectCap (PageCap word vmrights mt vmpage_size d pdata)) =
ArchObjectCap (PageCap word VMReadWrite VMNoMap vmpage_size d None)"
"capMasterCap (ArchObjectCap (PageTableCap word ptdata)) =
ArchObjectCap (PageTableCap word None)"
"capMasterCap (ArchObjectCap (PageDirectoryCap word pddata)) =
ArchObjectCap (PageDirectoryCap word None)"
"capMasterCap (ArchObjectCap (PDPointerTableCap word pdptdata)) =
ArchObjectCap (PDPointerTableCap word None)"
"capMasterCap (ArchObjectCap (PML4Cap word pml4data)) =
ArchObjectCap (PML4Cap word None)"
"capMasterCap (ArchObjectCap (IOPortCap ft lt)) =
ArchObjectCap (IOPortCap ft lt)"
"capMasterCap (ArchObjectCap IOPortControlCap) = ArchObjectCap IOPortControlCap"
"capMasterCap (capability.UntypedCap d word n f) = capability.UntypedCap d word n 0"
"capMasterCap capability.IRQControlCap = capability.IRQControlCap"
"capMasterCap (capability.ReplyCap word m) = capability.ReplyCap word True"
"capMasterCap (UntypedCap d word n f) = UntypedCap d word n 0"
"capMasterCap IRQControlCap = IRQControlCap"
"capMasterCap (ReplyCap word m) = ReplyCap word True"
by (simp_all add: capMasterCap_def)
lemma capMasterCap_eqDs1:
@ -715,8 +715,8 @@ lemma capMasterCap_eqDs1:
\<Longrightarrow> data3 = None \<and> (\<exists>data3. cap = ArchObjectCap (PDPointerTableCap ptr data3))"
"capMasterCap cap = ArchObjectCap (PML4Cap ptr data4)
\<Longrightarrow> data4 = None \<and> (\<exists>data4. cap = ArchObjectCap (PML4Cap ptr data4))"
"capMasterCap cap = ArchObjectCap (IOPortCap f span)
\<Longrightarrow> cap = ArchObjectCap (IOPortCap f span)"
"capMasterCap cap = ArchObjectCap (IOPortCap first_port last_port)
\<Longrightarrow> cap = ArchObjectCap (IOPortCap first_port last_port)"
"capMasterCap cap = ArchObjectCap IOPortControlCap
\<Longrightarrow> cap = ArchObjectCap IOPortControlCap"
by (clarsimp simp: capMasterCap_def
@ -788,6 +788,18 @@ lemma capUntypedSize_capBits:
apply fastforce
done
definition
"portSubRange r r' \<equiv>
case (r, r') of
(Some (f, l), Some (f', l')) \<Rightarrow> f \<le> f' \<and> l' \<le> l
| _ \<Rightarrow> False"
lemmas portRange_defs = portSubRange_def portRange_def
lemma portSubRange_eq [simp]:
"portSubRange (portRange cap) (portRange cap) = isArchIOPortCap cap"
by (auto simp: portRange_defs isCap_simps
split: capability.splits arch_capability.splits)
lemma sameRegionAs_def2:
"sameRegionAs cap cap' = (\<lambda>cap cap'.
(cap = cap'
@ -810,7 +822,7 @@ lemma sameRegionAs_def2:
apply (clarsimp del: subsetI intro!: range_subsetI)
apply clarsimp
apply (simp cong: conj_cong)
apply (simp add: capMasterCap_def sameRegionAs_def isArchPageCap_def isArchIOPortCap_def
apply (simp add: capMasterCap_def sameRegionAs_def isArchPageCap_def
split: capability.split
split del: if_split cong: if_cong)
apply (simp add: X64_H.sameRegionAs_def isCap_simps
@ -825,22 +837,20 @@ lemma sameRegionAs_def2:
lemma sameObjectAs_def2:
"sameObjectAs cap cap' = (\<lambda>cap cap'.
(cap = cap'
\<and> (\<not> isNullCap cap \<and> \<not> isZombie cap
\<and> \<not> isUntypedCap cap)
\<and> (\<not> isNullCap cap' \<and> \<not> isZombie cap'
\<and> \<not> isUntypedCap cap')
\<and> (\<not> isNullCap cap \<and> \<not> isZombie cap \<and> \<not> isUntypedCap cap)
\<and> (\<not> isNullCap cap' \<and> \<not> isZombie cap' \<and> \<not> isUntypedCap cap')
\<and> (isArchPageCap cap \<longrightarrow> capRange cap \<noteq> {})
\<and> (isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {})))
(capMasterCap cap) (capMasterCap cap')"
(capMasterCap cap) (capMasterCap cap')"
apply (simp add: sameObjectAs_def sameRegionAs_def2
isCap_simps capMasterCap_def
split: capability.split)
apply (clarsimp simp: X64_H.sameObjectAs_def isCap_simps
split: arch_capability.split cong: if_cong)
apply (clarsimp simp: X64_H.sameRegionAs_def isCap_simps
split del: if_split cong: if_cong)
split del: if_split cong: if_cong)
apply (simp add: capRange_def isCap_simps
split del: if_split)
split del: if_split)
apply fastforce
done

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

@ -58,6 +58,10 @@ lemma empty_fail_setCTE [intro!, wp, simp]:
unfolding setCTE_def
by (simp add: setObject_def split_def)
lemma empty_fail_updateCap [intro!, wp, simp]:
"empty_fail (updateCap p f)"
unfolding updateCap_def by auto
lemma empty_fail_updateMDB [intro!, wp, simp]:
"empty_fail (updateMDB a b)"
unfolding updateMDB_def Let_def by auto

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

@ -2524,22 +2524,19 @@ lemma do_reply_transfer_corres:
lemma valid_pspace'_splits[elim!]:
"valid_pspace' s \<Longrightarrow> valid_objs' s"
"valid_pspace' s \<Longrightarrow> pspace_aligned' s"
"valid_pspace' s \<Longrightarrow> pspace_canonical' s"
"valid_pspace' s \<Longrightarrow> pspace_distinct' s"
"valid_pspace' s \<Longrightarrow> valid_mdb' s"
"valid_pspace' s \<Longrightarrow> no_0_obj' s"
by (simp add: valid_pspace'_def)+
lemma sts_valid_pspace_hangers:
"\<lbrace>valid_pspace' and tcb_at' t and
valid_tcb_state' st\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_objs'\<rbrace>"
"\<lbrace>valid_pspace' and tcb_at' t and
valid_tcb_state' st\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. pspace_distinct'\<rbrace>"
"\<lbrace>valid_pspace' and tcb_at' t and
valid_tcb_state' st\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace>"
"\<lbrace>valid_pspace' and tcb_at' t and
valid_tcb_state' st\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_mdb'\<rbrace>"
"\<lbrace>valid_pspace' and tcb_at' t and
valid_tcb_state' st\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. no_0_obj'\<rbrace>"
"\<lbrace>valid_pspace' and tcb_at' t and valid_tcb_state' st\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_objs'\<rbrace>"
"\<lbrace>valid_pspace' and tcb_at' t and valid_tcb_state' st\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. pspace_distinct'\<rbrace>"
"\<lbrace>valid_pspace' and tcb_at' t and valid_tcb_state' st\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace>"
"\<lbrace>valid_pspace' and tcb_at' t and valid_tcb_state' st\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. pspace_canonical'\<rbrace>"
"\<lbrace>valid_pspace' and tcb_at' t and valid_tcb_state' st\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_mdb'\<rbrace>"
"\<lbrace>valid_pspace' and tcb_at' t and valid_tcb_state' st\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. no_0_obj'\<rbrace>"
by (safe intro!: hoare_strengthen_post [OF sts'_valid_pspace'_inv])
declare no_fail_getSlotCap [wp]

9
proof/refine/X64/KHeap_R.thy
View File

@ -745,12 +745,9 @@ proof -
from ctes_of have "cte_wp_at' (op = cte) p s"
by (simp add: cte_wp_at_ctes_of)
thus ?thesis using canonical
apply (simp add: pspace_canonical'_def)
apply (erule cte_wp_atE')
apply fastforce
by (fastforce simp: tcb_cte_cases_def field_simps objBits_defs
split: if_split_asm
elim: canonical_address_add)
by (fastforce simp: pspace_canonical'_def tcb_cte_cases_def field_simps objBits_defs
split: if_splits
elim: cte_wp_atE' canonical_address_add)
qed
lemma tcb_cte_cases_small:

4
spec/abstract/ARM/ArchVSpace_A.thy
View File

@ -565,9 +565,9 @@ where
text {* No user-modifiable data is stored in ARM-specific capabilities. *}
definition
arch_update_cap_data :: "data \<Rightarrow> arch_cap \<Rightarrow> cap"
arch_update_cap_data :: "bool \<Rightarrow> data \<Rightarrow> arch_cap \<Rightarrow> cap"
where
"arch_update_cap_data data c \<equiv> ArchObjectCap c"
"arch_update_cap_data preserve data c \<equiv> ArchObjectCap c"
text {* Actions that must be taken on finalisation of ARM-specific

4
spec/abstract/ARM_HYP/ArchVSpace_A.thy
View File

@ -841,9 +841,9 @@ where
text {* No user-modifiable data is stored in ARM-specific capabilities. *}
definition
arch_update_cap_data :: "data \<Rightarrow> arch_cap \<Rightarrow> cap"
arch_update_cap_data :: "bool \<Rightarrow> data \<Rightarrow> arch_cap \<Rightarrow> cap"
where
"arch_update_cap_data data c \<equiv> ArchObjectCap c"
"arch_update_cap_data preserve data c \<equiv> ArchObjectCap c"
text {* Actions that must be taken on finalisation of AR\_MHYP-specific

2
spec/abstract/CSpace_A.thy
View File

@ -147,7 +147,7 @@ definition
then NullCap
else CNodeCap oref bits guard'
else if is_arch_cap cap then
arch_update_cap_data w (the_arch_cap cap)
arch_update_cap_data preserve w (the_arch_cap cap)
else
cap"

5
spec/abstract/X64/ArchVSpace_A.thy
View File

@ -402,12 +402,11 @@ where
| IOPortCap _ _ \<Rightarrow> returnOk (ArchObjectCap c)
| IOPortControlCap \<Rightarrow> returnOk NullCap"
(* FIXME: update when IOSpace comes through, first/last ports may be wrong order *)
text {* No user-modifiable data is stored in x64-specific capabilities. *}
definition
arch_update_cap_data :: "data \<Rightarrow> arch_cap \<Rightarrow> cap"
arch_update_cap_data :: "bool \<Rightarrow> data \<Rightarrow> arch_cap \<Rightarrow> cap"
where
"arch_update_cap_data data c \<equiv> ArchObjectCap c"
"arch_update_cap_data preserve data c \<equiv> ArchObjectCap c"
text {* Actions that must be taken on finalisation of x64-specific

29
spec/haskell/src/SEL4/Object/ObjectType/X64.lhs
View File

@ -65,7 +65,7 @@ ASID capabilities can be copied without modification, as can IOPort and IOSpace
> deriveCap _ IOPortControlCap = return NullCap
> -- deriveCap _ (c@IOSpaceCap {}) = return c
IOPTs
% IOPTs
> -- deriveCap _ (c@IOPageTableCap { capIOPTMappedAddress = Just _ }) = return c
> -- deriveCap _ (IOPageTableCap { capIOPTMappedAddress = Nothing })
@ -90,13 +90,11 @@ IOPTs
>-- ioSpaceGetPCIDevice :: Word -> Maybe IOASID
>-- ioSpaceGetPCIDevice _ = error "Not implemented"
> -- FIXME x64: io_port_capdata_get_firstPort
> ioPortGetFirstPort :: Word -> Word16
> ioPortGetFirstPort _ = error "Not implemented"
>-- ioPortGetFirstPort :: Word -> Word16
>-- ioPortGetFirstPort capdata = fromIntegral (shiftR capdata 16)
> -- FIXME x64: io_port_capdata_get_lastPort
> ioPortGetLastPort :: Word -> Word16
> ioPortGetLastPort _ = error "Not implemented"
>-- ioPortGetLastPort :: Word -> Word16
>-- ioPortGetLastPort capdata = fromIntegral capdata
> updateCapData :: Bool -> Word -> ArchCapability -> Capability
>-- updateCapData preserve newData (c@IOSpaceCap {}) =
@ -110,19 +108,17 @@ IOPTs
>-- && domID /= 0 && domID <= mask domIDBits)
>-- then (ArchObjectCap (IOSpaceCap domID pciDevice))
>-- else NullCap -}
>-- updateCapData _ newData (c@IOPortCap {}) =
>-- updateCapData preserve newData (c@IOPortCap {}) =
>-- let
>-- firstPort = ioPortGetFirstPort newData;
>-- lastPort = ioPortGetLastPort newData;
>-- oldLast = capIOPortLastPort c;
>-- oldFirst = capIOPortFirstPort c
>-- oldFirst = capIOPortFirstPort c;
>-- oldLast = capIOPortLastPort c
>-- in
>-- if (oldFirst <= oldLast) then
>-- if (firstPort <= lastPort && firstPort >= capIOPortFirstPort c
>-- && lastPort <= oldLast)
>-- then (ArchObjectCap (IOPortCap firstPort lastPort))
>-- else NullCap
>-- else error "first port must be less than last"
>-- if (not preserve && firstPort <= lastPort
>-- && firstPort >= oldFirst && lastPort <= oldLast)
>-- then (ArchObjectCap (IOPortCap firstPort lastPort))
>-- else NullCap
> updateCapData _ _ c = ArchObjectCap c
CNodes have differing numbers of guard bits and rights bits
@ -262,7 +258,6 @@ Deletion of a final capability to a page table that has been mapped requires tha
> lB = capIOPortLastPort b
> sameRegionAs IOPortControlCap IOPortControlCap = True
> sameRegionAs IOPortControlCap (IOPortCap {}) = True
> --sameRegionAs (a@IOSpaceCap {}) (b@IOSpaceCap {}) =
> -- capIOPCIDevice a == capIOPCIDevice b
> --sameRegionAs (a@IOPageTableCap {}) (b@IOPageTableCap {}) =