arm crefine: remove some unused lemmas.

Add some comments on unused lemmas that we want to move or keep.
This commit is contained in:
Edward Pierzchalski 2018-11-13 20:19:41 +11:00
parent fd6d4b87ae
commit 17f3263d5e
29 changed files with 72 additions and 4405 deletions

View File

@ -496,11 +496,6 @@ lemma array_relation_to_map:
"array_relation r n a c \<Longrightarrow> \<forall>i\<le>n. r (a i) (the (array_to_map n c i))"
by (simp add: array_relation_def array_to_map_def)
lemma dom_array_to_map[simp]: "dom (array_to_map n c) = {i. i\<le>n}"
by (simp add: array_to_map_def dom_def)
lemma ran_array_to_map:
"ran (array_to_map n c) = {y. \<exists>i\<le>n. index c (unat i) = y}"
by (auto simp: array_to_map_def ran_def Collect_eq)
text {* Note: Sometimes, @{text array_map_conv} might be more convenient
in conjunction with @{const array_relation}. *}
@ -510,22 +505,10 @@ lemma array_map_conv_def2:
"array_map_conv f n c \<equiv> \<lambda>i. if i\<le>n then f (index c (unat i)) else None"
by (rule eq_reflection, rule ext) (simp add: array_map_conv_def map_comp_def
array_to_map_def)
lemma array_relation_map_conv:
"array_relation r n a c \<Longrightarrow> \<forall>x y. r y x \<longrightarrow> (f x) = y \<Longrightarrow>
\<forall>i>n. a i = None \<Longrightarrow> array_map_conv f n c = a"
by (rule ext) (simp add: array_relation_def array_map_conv_def2)
lemma array_relation_map_conv2:
"array_relation r n a c \<Longrightarrow> \<forall>x. \<forall>y\<in>range a. r y x \<longrightarrow> (f x) = y \<Longrightarrow>
\<forall>i>n. a i = None \<Longrightarrow> array_map_conv f n c = a"
by (rule ext) (simp add: array_relation_def array_map_conv_def2)
lemma array_map_conv_Some[simp]: "array_map_conv Some n c = array_to_map n c"
by (simp add: array_map_conv_def map_comp_def)
lemma map_comp_array_map_conv_comm:
"map_comp f (array_map_conv g n c) = array_map_conv (map_comp f g) n c"
by (rule ext) (simp add: array_map_conv_def2 map_option_def map_comp_def)
lemma ran_array_map_conv:
"ran (array_map_conv f n c) = {y. \<exists>i\<le>n. f (index c (unat i)) = Some y}"
by (auto simp add: array_map_conv_def2 ran_def Collect_eq)
(* FIXME: move to somewhere sensible >>> *)
text {* Map inversion (implicitly assuming injectivity). *}
@ -570,8 +553,6 @@ lemma is_inv_unique:
apply (drule_tac x=x in spec)+
apply (case_tac "g x", clarsimp+)
done
lemma assumes A: "is_inv f g" shows the_inv_map_eq: "the_inv_map f = g"
by (simp add: is_inv_unique[OF A A[THEN is_inv_inj, THEN is_inv_the_inv_map]])
(*<<<*)
definition
@ -586,15 +567,6 @@ definition
(the_inv_map (array_map_conv (\<lambda>x. if x=0 then None else Some x)
0xFF hw_asid_table) asid))"
(* FIXME: move *)
lemma ran_map_comp_subset: "ran (map_comp f g) <= (ran f)"
by (fastforce simp: map_comp_def ran_def split: option.splits)
(* FIXME: move *)(* NOTE: unused. *)
lemma inj_on_option_map:
"inj_on (map_option f o m) (dom m) \<Longrightarrow> inj_on m (dom m)"
by (auto simp add: inj_on_def map_option_def dom_def)
lemma eq_option_to_0_rev:
"Some 0 ~: A \<Longrightarrow> \<forall>x. \<forall>y\<in>A.
((=) \<circ> option_to_0) y x \<longrightarrow> (if x = 0 then None else Some x) = y"
@ -632,7 +604,7 @@ lemma (in kernel_m)
apply (cut_tac w=i in word_le_p2m1, simp add: minus_one_norm)
apply clarsimp
apply (case_tac "armKSASIDMap (ksArchState astate) x")
apply (clarsimp simp: ran_array_map_conv option_to_0_def split:option.splits)
apply (clarsimp simp: option_to_0_def split:option.splits)
apply (fastforce simp: is_inv_def)
apply clarsimp
apply (rule conjI)
@ -1443,11 +1415,6 @@ where
"mk_gsUntypedZeroRanges s
= ran (untypedZeroRange \<circ>\<^sub>m (option_map cteCap o map_to_ctes (cstate_to_pspace_H s)))"
lemma cpspace_user_data_relation_user_mem'[simp]:
"\<lbrakk>pspace_aligned' as;pspace_distinct' as\<rbrakk> \<Longrightarrow> cpspace_user_data_relation (ksPSpace as) (option_to_0 \<circ> user_mem' as) (t_hrs_' cs)
= cpspace_user_data_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs)"
by (simp add: cmap_relation_def)
lemma cpspace_device_data_relation_user_mem'[simp]:
"cpspace_device_data_relation (ksPSpace as) (option_to_0 \<circ> user_mem' as) (t_hrs_' cs)
= cpspace_device_data_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs)"
@ -1495,9 +1462,6 @@ where
ksMachineState = cstate_to_machine_H s\<rparr>"
lemma trivial_eq_conj: "B = C \<Longrightarrow> (A \<and> B) = (A \<and> C)"
by simp
lemma (in kernel_m) cstate_to_H_correct:
assumes valid: "valid_state' as"
assumes cstate_rel: "cstate_relation as cs"

View File

@ -266,7 +266,6 @@ proof -
note cterl = retype_ctes_helper[OF pal pdst pno' al'
le_refl range_cover_sz'[where 'a=32, folded word_bits_def, OF rc] mko rc,simplified]
note ht_rl = clift_eq_h_t_valid_eq[OF rl', OF tag_disj_via_td_name, simplified]
uinfo_array_tag_n_m_not_le_typ_name
have guard:
"\<forall>n<2 ^ (pageBits - objBitsKO ko). c_guard (CTypesDefs.ptr_add ?ptr (of_nat n))"
@ -370,25 +369,6 @@ proof -
done
qed
lemma cmap_relation_ccap_relation:
"\<lbrakk>cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation;ctes_of s p = Some cte; cteCap cte = cap\<rbrakk>
\<Longrightarrow> ccap_relation cap
(h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr p\<rightarrow>[''cap_C''])))"
apply (erule(1) cmap_relationE1)
apply (clarsimp simp add: typ_heap_simps' ccte_relation_ccap_relation)
done
lemma ccorres_move_Guard_Seq_strong:
"\<lbrakk>\<forall>s s'. (s, s') \<in> sr \<and> P s \<and> P' s' \<longrightarrow> G' s';
ccorres_underlying sr \<Gamma> r xf arrel axf A C' hs a (c;;d) \<rbrakk>
\<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (A and P) {s. P' s \<and> (G' s \<longrightarrow> s \<in> C')} hs a
(Guard F (Collect G') c;;
d)"
apply (rule ccorres_guard_imp2, erule ccorres_move_Guard_Seq)
apply assumption
apply auto
done
lemma ghost_assertion_data_get_gs_clear_region:
"gs_get_assn proc (gs_clear_region addr n gs) = gs_get_assn proc gs"
by (clarsimp simp: ghost_assertion_data_get_def gs_clear_region_def)
@ -1472,13 +1452,6 @@ lemma valid_pde_slots_lift2:
apply (wp hoare_vcg_ex_lift hoare_vcg_conj_lift | assumption)+
done
lemma obj_at_pte_aligned:
"obj_at' (\<lambda>a::ARM_H.pte. True) ptr s ==> is_aligned ptr 2"
apply (drule obj_at_ko_at')
apply (clarsimp dest!:ko_at_is_aligned'
simp:objBits_simps archObjSize_def pteBits_def)
done
lemma addrFromPPtr_mask_5:
"addrFromPPtr ptr && mask (5::nat) = ptr && mask (5::nat)"
apply (simp add:addrFromPPtr_def physMappingOffset_def
@ -2353,66 +2326,6 @@ lemma flushtype_relation_triv:
ARM_H.isPDFlushLabel_def
split: flush_type.splits invocation_label.splits arch_invocation_label.splits)
lemma setVMRootForFlush_ccorres2:
"ccorres (\<lambda>rv rv'. rv' = from_bool rv) ret__unsigned_long_'
(invs' and (\<lambda>s. asid \<le> mask asid_bits))
(UNIV \<inter> {s. pd_' s = pde_Ptr pd} \<inter> {s. asid_' s = asid}) hs
(setVMRootForFlush pd asid) (Call setVMRootForFlush_'proc)"
apply (cinit lift: pd_' asid_')
apply (rule ccorres_pre_getCurThread)
apply (simp add: getThreadVSpaceRoot_def locateSlot_conv
del: Collect_const)
apply (rule ccorres_Guard_Seq)+
apply (ctac add: getSlotCap_h_val_ccorres)
apply csymbr
apply csymbr
apply (simp add: cap_get_tag_isCap_ArchObject2 if_1_0_0
del: Collect_const)
apply (rule ccorres_if_lhs)
apply (rule_tac P="(capPDIsMapped_CL (cap_page_directory_cap_lift threadRoot) = 0)
= (capPDMappedASID (capCap rva) = None)
\<and> capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot)
= capPDBasePtr (capCap rva)" in ccorres_gen_asm2)
apply (rule ccorres_rhs_assoc | csymbr | simp add: Collect_True del: Collect_const)+
apply (rule ccorres_split_throws)
apply (rule ccorres_return_C, simp+)
apply vcg
apply (rule ccorres_rhs_assoc2,
rule ccorres_rhs_assoc2,
rule ccorres_symb_exec_r)
apply simp
apply (ctac (no_vcg) add: armv_contextSwitch_ccorres)
apply (ctac add: ccorres_return_C)
apply wp
apply (simp add: true_def from_bool_def)
apply vcg
apply (rule conseqPre, vcg)
apply (simp add: Collect_const_mem)
apply clarsimp
apply simp
apply (wp hoare_drop_imps)
apply vcg
apply (clarsimp simp: Collect_const_mem if_1_0_0 word_sle_def
ccap_rights_relation_def cap_rights_to_H_def
mask_def[where n="Suc 0"] true_def to_bool_def
allRights_def size_of_def cte_level_bits_def
tcbVTableSlot_def Kernel_C.tcbVTable_def invs'_invs_no_cicd)
apply (clarsimp simp: rf_sr_ksCurThread ptr_val_tcb_ptr_mask' [OF tcb_at_invs'])
apply (frule cte_at_tcb_at_16'[OF tcb_at_invs'], clarsimp simp: cte_wp_at_ctes_of)
apply (rule cmap_relationE1[OF cmap_relation_cte], assumption+)
apply (clarsimp simp: false_def true_def from_bool_def
typ_heap_simps' ptr_add_assertion_positive)
apply (clarsimp simp: tcb_cnode_index_defs
rf_sr_tcb_ctes_array_assertion2[OF _ tcb_at_invs',
THEN array_assertion_shrink_right])
apply (case_tac "isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv)")
apply (clarsimp simp: isCap_simps(2) cap_get_tag_isCap_ArchObject[symmetric])
apply (clarsimp simp: cap_page_directory_cap_lift cap_to_H_def
elim!: ccap_relationE)
apply (simp add: to_bool_def split: if_split)
apply (auto simp: cap_get_tag_isCap_ArchObject2)
done
lemma at_least_2_args:
"\<not> length args < 2 \<Longrightarrow> \<exists>a b c. args = a#b#c"
apply (case_tac args)
@ -3279,24 +3192,6 @@ lemma sts_Restart_ct_active [wp]:
apply wp
done
lemma maskCapRights_eq_Untyped [simp]:
"(maskCapRights R cap = UntypedCap d p sz idx) = (cap = UntypedCap d p sz idx)"
apply (cases cap)
apply (auto simp: Let_def isCap_simps maskCapRights_def)
apply (simp add: ARM_H.maskCapRights_def isPageCap_def Let_def split: arch_capability.splits)
done
lemma le_mask_asid_bits_helper:
"x \<le> 2 ^ asid_high_bits - 1 \<Longrightarrow> (x::word32) << asid_low_bits \<le> mask asid_bits"
apply (simp add: mask_def)
apply (drule le2p_bits_unset_32)
apply (simp add: asid_high_bits_def word_bits_def)
apply (subst upper_bits_unset_is_l2p_32 [symmetric])
apply (simp add: asid_bits_def word_bits_def)
apply (clarsimp simp: asid_bits_def asid_low_bits_def asid_high_bits_def nth_shiftl)
done
declare Word_Lemmas.from_bool_mask_simp [simp]
lemma isPDFlush_fold:
@ -3963,8 +3858,7 @@ lemma Arch_decodeInvocation_ccorres:
capBlockSize (fst (hd extraCaps)) = objBits (makeObject ::asidpool)
\<and> \<not> capIsDevice (fst (hd extraCaps))))"
in ccorres_gen_asm2)
apply (clarsimp simp: if_1_0_0 to_bool_if cond_throw_whenE bindE_assoc
from_bool_neq_0)
apply (clarsimp simp: cond_throw_whenE bindE_assoc)
apply (rule ccorres_split_when_throwError_cond[where Q = \<top> and Q' = \<top>])
apply clarsimp
apply (rule syscall_error_throwError_ccorres_n)

View File

@ -89,27 +89,6 @@ lemma empty_fail_getMRs[iff]:
"empty_fail (getMRs t buf mi)"
by (auto simp add: getMRs_def split: option.split)
lemma empty_fail_getExtraCPtrs [intro!, simp]:
"empty_fail (getExtraCPtrs sendBuffer info)"
apply (simp add: getExtraCPtrs_def)
apply (cases info, simp)
apply (cases sendBuffer, simp_all)
done
lemma empty_fail_loadCapTransfer [intro!, simp]:
"empty_fail (loadCapTransfer a)"
by (simp add: loadCapTransfer_def capTransferFromWords_def)
lemma empty_fail_emptyOnFailure [intro!, simp]:
"empty_fail m \<Longrightarrow> empty_fail (emptyOnFailure m)"
by (auto simp: emptyOnFailure_def catch_def split: sum.splits)
lemma empty_fail_unifyFailure [intro!, simp]:
"empty_fail m \<Longrightarrow> empty_fail (unifyFailure m)"
by (auto simp: unifyFailure_def catch_def rethrowFailure_def
handleE'_def throwError_def
split: sum.splits)
lemma asUser_mapM_x:
"(\<And>x. empty_fail (f x)) \<Longrightarrow>
asUser t (mapM_x f xs) = do stateAssert (tcb_at' t) []; mapM_x (\<lambda>x. asUser t (f x)) xs od"
@ -228,17 +207,6 @@ proof -
done
qed
lemma exec_Basic_Guard_UNIV:
"Semantic.exec \<Gamma> (Basic f;; Guard F UNIV (Basic g)) x y =
Semantic.exec \<Gamma> (Basic (g o f)) x y"
apply (rule iffI)
apply (elim exec_elim_cases, simp_all, clarsimp)[1]
apply (simp add: o_def, rule exec.Basic)
apply (elim exec_elim_cases)
apply simp_all
apply (rule exec_Seq' exec.Basic exec.Guard | simp)+
done
(* only exists in Haskell, only used for C refinement *)
crunches writeTTBR0Ptr
for (empty_fail) empty_fail[wp,simp]

View File

@ -14,12 +14,6 @@ theory CSpaceAcc_C
imports "Refine.EmptyFail" Ctac_lemmas_C
begin
(* For resolving schematics *)
lemma lift_t_cslift:
"cslift x p = Some y \<Longrightarrow>
lift_t c_guard (hrs_mem (t_hrs_' (globals x)), hrs_htd (t_hrs_' (globals x))) p = Some y"
by (simp add: hrs_htd_def hrs_mem_def)
context kernel begin
lemma ccorres_pre_getNotification:
@ -229,10 +223,6 @@ lemma ccorres_pre_curDomain:
apply (clarsimp simp: rf_sr_ksCurDomain)
done
lemma scast_EXCPT_NONE [simp]: "scast EXCEPTION_NONE = EXCEPTION_NONE"
unfolding scast_def EXCEPTION_NONE_def
by simp
lemma pageBitsForSize_spec:
"\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. \<acute>pagesize && mask 2 = \<acute>pagesize\<rbrace> Call pageBitsForSize_'proc
\<lbrace> \<acute>ret__unsigned_long = of_nat (pageBitsForSize (gen_framesize_to_H \<^bsup>s\<^esup>pagesize)) \<rbrace>"
@ -276,21 +266,6 @@ 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]
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)
\<lbrace> \<acute>ret__unsigned_long =
((capAllowGrant_CL (crl s) << 2)
|| (capAllowRead_CL (crl s) << 1)
|| capAllowWrite_CL (crl s)) \<rbrace>"
unfolding crl_def
apply vcg
apply (simp add: word_sle_def word_sless_def)
apply (simp add: seL4_CapRights_lift_def shiftr_over_and_dist)
apply (simp add: mask_shift_simps)
apply (simp add: word_ao_dist2[symmetric])
done
lemma array_assertion_abs_cnode_ctes:
"\<forall>s s'. (s, s') \<in> rf_sr \<and> (\<exists>n. gsCNodes s p = Some n \<and> n' \<le> 2 ^ n) \<and> True
\<longrightarrow> (x s' = 0 \<or> array_assertion (cte_Ptr p) n' (hrs_htd (t_hrs_' (globals s'))))"

View File

@ -502,12 +502,6 @@ lemma ccorres_updateMDB_const [corres]:
apply (clarsimp)
done
lemma cap_lift_capNtfnBadge_mask_eq:
"cap_lift cap = Some (Cap_notification_cap ec)
\<Longrightarrow> capNtfnBadge_CL ec && mask 28 = capNtfnBadge_CL ec"
unfolding cap_lift_def
by (fastforce simp: Let_def mask_def word_bw_assocs split: if_split_asm)
lemma cap_lift_capEPBadge_mask_eq:
"cap_lift cap = Some (Cap_endpoint_cap ec)
\<Longrightarrow> capEPBadge_CL ec && mask 28 = capEPBadge_CL ec"
@ -765,8 +759,6 @@ lemma cteInsert_if_helper:
lemma forget_Q':
"(x \<in> Q) = (y \<in> Q) \<Longrightarrow> (x \<in> Q) = (y \<in> Q)" .
lemmas cteInsert_if_helper' = cteInsert_if_helper [OF _ forget_Q']
(* Useful:
apply (tactic {* let val _ = reset CtacImpl.trace_ceqv; val _ = reset CtacImpl.trace_ctac in all_tac end; *})
*)
@ -785,25 +777,6 @@ schematic_goal ccap_relation_tag_Master:
Let_def cap_lift_def cap_to_H_def
split: if_split_asm)
lemma ccap_relation_is_derived_tag_equal:
"\<lbrakk> is_derived' cs p cap cap'; ccap_relation cap ccap; ccap_relation cap' ccap' \<rbrakk>
\<Longrightarrow> cap_get_tag ccap' = cap_get_tag ccap"
unfolding badge_derived'_def is_derived'_def
by (clarsimp simp: ccap_relation_tag_Master)
lemma ccap_relation_Master_tags_eq:
"\<lbrakk> capMasterCap cap = capMasterCap cap'; ccap_relation cap ccap; ccap_relation cap' ccap' \<rbrakk>
\<Longrightarrow> cap_get_tag ccap' = cap_get_tag ccap"
by (clarsimp simp: ccap_relation_tag_Master)
lemma is_simple_cap_get_tag_relation:
"ccap_relation cap ccap
\<Longrightarrow> is_simple_cap_tag (cap_get_tag ccap) = is_simple_cap' cap"
apply (simp add: is_simple_cap_tag_def is_simple_cap'_def
cap_get_tag_isCap)
apply (auto simp: isCap_simps)
done
lemma setUntypedCapAsFull_cte_at_wp [wp]:
"\<lbrace> cte_at' x \<rbrace> setUntypedCapAsFull rvb cap src \<lbrace> \<lambda>_. cte_at' x \<rbrace>"
apply (clarsimp simp: setUntypedCapAsFull_def)
@ -1018,16 +991,6 @@ lemma setUntypedCapAsFull_ccorres [corres]:
apply (clarsimp simp: cap_get_tag_isCap_unfolded_H_cap)
done
lemma ccte_lift:
"\<lbrakk>(s, s') \<in> rf_sr; cslift s' (cte_Ptr p) = Some cte';
cte_lift cte' = Some y; c_valid_cte cte'\<rbrakk>
\<Longrightarrow> ctes_of s p = Some (cte_to_H (the (cte_lift cte')))"
apply (clarsimp simp:rf_sr_def cstate_relation_def Let_def cpspace_relation_def)
apply (drule(1) cmap_relation_cs_atD)
apply simp
apply (clarsimp simp:ccte_relation_def)
done
lemma cmdb_node_relation_mdbNext:
"cmdbnode_relation n n'
\<Longrightarrow> mdbNext_CL (mdb_node_lift n') = mdbNext n"
@ -1073,8 +1036,6 @@ lemma ccorres_move_ptr_safe_Seq:
apply (erule cslift_ptr_safe)
done
lemmas ccorres_move_guard_ptr_safe = ccorres_move_ptr_safe_Seq ccorres_move_ptr_safe
lemma cteInsert_ccorres:
"ccorres dc xfdc (cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capMasterCap cap
\<or> is_simple_cap' cap) src
@ -1157,7 +1118,7 @@ lemma cteInsert_ccorres:
apply (clarsimp simp: map_comp_Some_iff cte_wp_at_ctes_of
split del: if_split)
apply (clarsimp simp: typ_heap_simps c_guard_clift split_def)
apply (clarsimp simp: is_simple_cap_get_tag_relation ccte_relation_ccap_relation cmdb_node_relation_mdbNext[symmetric])
apply (clarsimp simp: ccte_relation_ccap_relation cmdb_node_relation_mdbNext[symmetric])
done
(****************************************************************************)
@ -1301,154 +1262,6 @@ lemma cteMove_ccorres:
false_def to_bool_def)
done
lemma cteMove_ccorres_verbose:
"ccorres dc xfdc
(valid_mdb' and pspace_aligned' )
(UNIV \<inter> {s. destSlot_' s = Ptr dest} \<inter>
{s. srcSlot_' s = Ptr src} \<inter>
{s. ccap_relation cap (newCap_' s)}) []
(cteMove cap src dest)
(Call cteMove_'proc)"
apply (cinit (no_ignore_call) lift: destSlot_' srcSlot_' newCap_' simp del: return_bind)
(* previous line replaces all the following:
unfolding cteMove_def -- "unfolds Haskell side"
apply (rule ccorres_Call) -- "unfolds C side"
apply (rule cteMove_impl [unfolded cteMove_body_def])
-- "retrieves the C body definition"
apply (rule ccorres_rhs_assoc)+ -- "re-associates C sequences to the right: i0;(the rest)"
apply (simp del: return_bind Int_UNIV_left)
-- "gets rid of SKIP and print all haskells instruction as y \<leftarrow> \<dots>"
apply (cinitlift destSlot_' srcSlot_' newCap_')
apply (rule ccorres_guard_imp2) -- "replaces the preconditions by schematics (to be instanciated along the proof)"
-- " \<Rightarrow> creates 2 subgoals (1 for main proof and 1 for ''conjunction of "
-- " preconditions implies conjunction of generalized (schematics) guards'')"
-- "Start proofs"
apply csymbr -- "Remove undefined"
apply csymbr
apply csymbr
*)
\<comment> \<open>***Main goal***\<close>
\<comment> \<open>--- instruction: oldCTE \<leftarrow> getCTE dest; ---\<close>
\<comment> \<open>--- y \<leftarrow> assert (cteCap oldCTE = capability.NullCap); ---\<close>
\<comment> \<open>--- y \<leftarrow> assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (...)); ---\<close>
apply (ctac pre: ccorres_pre_getCTE ccorres_assert iffD2 [OF ccorres_seq_skip])
\<comment> \<open>ccorres_Guard_Seq puts the C guards into the precondition\<close>
\<comment> \<open>ccorres_getCTE applies the corres proof for getCTE\<close>
\<comment> \<open>ccorres_assert add the asserted proposition to the precondition\<close>
\<comment> \<open>iffD2 [\<dots>] removes the SKIPS\<close>
\<comment> \<open>implicit symbolic execution of return\<close>
\<comment> \<open>\<Rightarrow> 2 new subgoals for return (in addition to Main Goal)\<close>
\<comment> \<open>1. pre/post for Haskell side of return\<close>
\<comment> \<open>2. pre/post for C side of return\<close>
\<comment> \<open>(rq: ccorress_getCTE eta expands everything... )\<close>
\<comment> \<open>***Main Goal of return***\<close>
\<comment> \<open>--- instruction: y \<leftarrow> updateCap dest cap ---\<close>
apply ctac
\<comment> \<open>implicit symbolic execution \<Rightarrow> 2 new subgoals for 1st updateCap\<close>
\<comment> \<open>***Main Goal***\<close>
\<comment> \<open>--- instruction: y \<leftarrow> updateCap src capability.NullCap; (but with CALL on C side)\<close>
apply csymbr \<comment> \<open>symb exec of C instruction CALL to create Null Cap\<close>
\<comment> \<open>--- instruction: y \<leftarrow> updateCap src capability.NullCap; (no CALL on C side)\<close>
apply ctac
\<comment> \<open>implicit symbolic execution \<Rightarrow> 2 new subgoals for 2st updateCap\<close>
\<comment> \<open>***Main Goal***\<close>
\<comment> \<open>--- instruction: y \<leftarrow> updateMDB dest (const rv); ---\<close>
\<comment> \<open>if not ctac won't work, because of the eta-expansion\<dots>\<close>
apply ctac
\<comment> \<open>implicit symbolic execution \<Rightarrow> 2 new subgoals for 1st updateMDB\<close>
\<comment> \<open>***Main Goal***\<close>
\<comment> \<open>--- instruction: y \<leftarrow> updateMDB dest (const nullMDBNode); (but with CALL on C side) ---\<close>
apply csymbr \<comment> \<open>symb exec of C instruction CALL to create Null MDB\<close>
\<comment> \<open>--- instruction: y \<leftarrow> updateMDB dest (const nullMDBNode); (no CALL on C side) ---\<close>
apply ctac
\<comment> \<open>implicit symbolic execution \<Rightarrow> 2 new subgoals for 2nd updateMDB\<close>
\<comment> \<open>***Main Goal***\<close>
\<comment> \<open>--- instruction: y <- updateMDB (mdbPrev rv) (mdbNext_update (%_. dest); (but with CALL on C side) ---\<close>
apply csymbr \<comment> \<open>symb exec of C instruction CALL to mdbPrev\<close>
\<comment> \<open>--- instruction: y <- updateMDB (mdbPrev rv) (mdbNext_update (%_. dest); (no CALL on C side) ---\<close>
\<comment> \<open>--- (IF instruction in the C side) ---\<close>
apply (erule_tac t = ret__unsigned in ssubst)
apply csymbr
apply (ctac add: updateMDB_mdbPrev_set_mdbNext)
\<comment> \<open>***the correspondance proof for the rest***\<close>
\<comment> \<open>--- instruction: updateMDB (mdbNext rv) (mdbPrev_update (%_. dest)) (but with CALL on C side) ---\<close>
apply csymbr \<comment> \<open>symb exec of C instruction CALL to mdbNext\<close>
\<comment> \<open>--- instruction: updateMDB (mdbNext rv) (mdbPrev_update (%_. dest)) (no CALL on C side) ---\<close>
\<comment> \<open>--- (IF instruction in the C side) ---\<close>
apply (erule_tac t = ret__unsigned in ssubst)
apply csymbr
apply (rule updateMDB_mdbNext_set_mdbPrev)
apply simp
apply simp
\<comment> \<open>***the pre/post for Haskell side\<close>
apply wp
\<comment> \<open>***the pre/post for C side\<close>
apply vcg
\<comment> \<open>***pre/post for Haskell side of 2nd updateMDB***\<close>
apply wp
\<comment> \<open>***pre/post for C side of 2nd updateMDB***\<close>
apply vcg
\<comment> \<open>***pre/post for Haskell side of 1st updateMDB***\<close>
apply wp
\<comment> \<open>***pre/post for C side of 1st updateMDB***\<close>
apply vcg
\<comment> \<open>***pre/post for Haskell side of 2st updateCap***\<close>
apply wp
\<comment> \<open>***pre/post for C side of 2st updateCap***\<close>
apply vcg
\<comment> \<open>***pre/post for Haskell side of 1st updateCap***\<close>
apply wp
\<comment> \<open>***pre/post for C side of 1st updateCap***\<close>
apply vcg
\<comment> \<open>***pre/post for Haskell side of return***\<close>
apply wp
\<comment> \<open>***pre/post for C side of return***\<close>
apply vcg
\<comment> \<open>********************\<close>
\<comment> \<open>*** LAST SUBGOAL ***\<close>
\<comment> \<open>********************\<close>
\<comment> \<open>***conjunction of generalised precondition ***\<close>
apply (rule conjI)
\<comment> \<open>***--------------------------------***\<close>
\<comment> \<open>***Haskell generalised precondition***\<close>
\<comment> \<open>***--------------------------------***\<close>
\<comment> \<open>(complicated conjunction with many cte_at' and src\<noteq>0 \<dots>)\<close>
apply (clarsimp simp: cte_wp_at_ctes_of)
\<comment> \<open>cte_wp_at_ctes_of replaces (cte_at' p s) in the goal by\<close>
\<comment> \<open>(\<exists>cte.ctes_of s p = Some cte) which is in the hypotheses\<close>
\<comment> \<open>ctes_of s (?ptr908 ...) = Some scte \<and> ...\<close>
apply (rule conjI, assumption) \<comment> \<open>instanciates the schematic with src\<close>
\<comment> \<open>(mdbPrev \<dots> \<noteq> 0 \<longrightarrow> (\<exists>cte. ctes_of s (mdbPrev \<dots>) = Some cte) \<and> is_aligned (mdbPrev \<dots>) 3)\<close>
\<comment> \<open>\<and> (mdbNext \<dots> \<noteq> 0 \<longrightarrow> (\<exists>cte. ctes_of s (mdbNext \<dots>) = Some cte) \<and> is_aligned (mdbNext \<dots>) 3)\<close>
apply (rule conjI)
apply (erule (2) is_aligned_3_prev)
apply (erule (2) is_aligned_3_next)
\<comment> \<open>***--------------------------***\<close>
\<comment> \<open>***C generalised precondition***\<close>
\<comment> \<open>***--------------------------***\<close>
apply (unfold dc_def)
apply (clarsimp simp: ccap_relation_NullCap_iff split del: if_split)
\<comment> \<open>cmdbnode_relation nullMDBNode va\<close>
apply (simp add: cmdbnode_relation_def)
apply (simp add: mdb_node_to_H_def)
apply (simp add: nullMDBNode_def)
apply (simp add: false_def to_bool_def)
done
(************************************************************************)
(* *)
(* lemmas used in cteSwap_ccorres ***************************************)
@ -1480,133 +1293,12 @@ lemma ccorres_return_cte_mdbnode_safer:
apply (clarsimp simp: typ_heap_simps)
done
(*-----------------------------------------------------------------------*)
(* lemmas about map and hrs_mem -----------------------------------------*)
(*-----------------------------------------------------------------------*)
(* FIXME: This is a stray leftover from some lemma deletions.
Check that this can be removed. *)
declare modify_map_exists_cte[simp]
(*------------------------------------------------------------------------------*)
(* lemmas about pointer equality given valid_mdb (prev\<noteq>next, prev\<noteq>myself, etc) *)
(*------------------------------------------------------------------------------*)
lemma valid_mdb_Prev_neq_Next:
"\<lbrakk> valid_mdb' s; ctes_of s p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0 \<rbrakk> \<Longrightarrow>
(mdbNext (cteMDBNode cte)) \<noteq> (mdbPrev (cteMDBNode cte))"
apply (simp add: valid_mdb'_def)
apply (simp add: valid_mdb_ctes_def)
apply (elim conjE)
apply (drule (1) mdb_chain_0_no_loops)
apply (simp add: valid_dlist_def)
apply (erule_tac x=p in allE)
apply (erule_tac x=cte in allE)
apply (simp add: Let_def)
apply clarsimp
apply (drule_tac s="mdbNext (cteMDBNode cte)" in sym)
apply simp
apply (simp add: no_loops_def)
apply (erule_tac x= "(mdbNext (cteMDBNode cte))" in allE)
apply (erule notE, rule trancl_trans)
apply (rule r_into_trancl)
apply (simp add: mdb_next_unfold)
apply (rule r_into_trancl)
apply (simp add: mdb_next_unfold)
done
lemma valid_mdb_Prev_neq_itself:
"\<lbrakk> valid_mdb' s; ctes_of s p = Some cte \<rbrakk> \<Longrightarrow>
(mdbPrev (cteMDBNode cte)) \<noteq> p"
apply (unfold valid_mdb'_def)
apply (simp add: CSpace_I.no_self_loop_prev)
done
lemma valid_mdb_Next_neq_itself:
"\<lbrakk> valid_mdb' s; ctes_of s p = Some cte \<rbrakk> \<Longrightarrow>
(mdbNext (cteMDBNode cte)) \<noteq> p"
apply (unfold valid_mdb'_def)
apply (simp add: CSpace_I.no_self_loop_next)
done
lemma valid_mdb_not_same_Next :
"\<lbrakk> valid_mdb' s; p\<noteq>p'; ctes_of s p = Some cte; ctes_of s p' = Some cte';
(mdbNext (cteMDBNode cte))\<noteq>0 \<or> (mdbNext (cteMDBNode cte'))\<noteq>0 \<rbrakk> \<Longrightarrow>
(mdbNext (cteMDBNode cte)) \<noteq> (mdbNext (cteMDBNode cte')) "
apply (clarsimp)
apply (case_tac cte, clarsimp)
apply (rename_tac capability mdbnode)
apply (case_tac cte', clarsimp)
apply (subgoal_tac "mdb_ptr (ctes_of s) p capability mdbnode")
apply (drule (2) mdb_ptr.p_nextD)
apply clarsimp
apply (unfold mdb_ptr_def vmdb_def mdb_ptr_axioms_def valid_mdb'_def, simp)
done
lemma valid_mdb_not_same_Prev :
"\<lbrakk> valid_mdb' s; p\<noteq>p'; ctes_of s p = Some cte; ctes_of s p' = Some cte';
(mdbPrev (cteMDBNode cte))\<noteq>0 \<or> (mdbPrev (cteMDBNode cte'))\<noteq>0 \<rbrakk> \<Longrightarrow>
(mdbPrev (cteMDBNode cte)) \<noteq> (mdbPrev (cteMDBNode cte')) "
apply (clarsimp)
apply (case_tac cte, clarsimp)
apply (rename_tac capability mdbnode)
apply (case_tac cte', clarsimp)
apply (subgoal_tac "mdb_ptr (ctes_of s) p capability mdbnode")
apply (drule (2) mdb_ptr.p_prevD)
apply clarsimp
apply (unfold mdb_ptr_def vmdb_def mdb_ptr_axioms_def valid_mdb'_def, simp)
done
(*---------------------------------------------------------------------------------*)
(* lemmas to simplify the big last goal on C side to avoid proving things twice ---*)
(*---------------------------------------------------------------------------------*)
lemma c_guard_and_h_t_valid_eq_h_t_valid:
"(POINTER \<noteq> 0 \<longrightarrow>
c_guard ((Ptr &(Ptr POINTER ::cte_C ptr \<rightarrow>[''cteMDBNode_C''])) ::mdb_node_C ptr) \<and>
s' \<Turnstile>\<^sub>c (Ptr (POINTER)::cte_C ptr)) =
(POINTER \<noteq> 0 \<longrightarrow>
s' \<Turnstile>\<^sub>c (Ptr (POINTER)::cte_C ptr))"
apply (rule iffI, clarsimp+)
apply (rule c_guard_field_lvalue)
apply (rule c_guard_h_t_valid, assumption)
apply (fastforce simp: typ_uinfo_t_def)+
done
lemma c_guard_and_h_t_valid_and_rest_eq_h_t_valid_and_rest:
"(POINTER \<noteq> 0 \<longrightarrow>
c_guard ((Ptr &(Ptr POINTER ::cte_C ptr \<rightarrow>[''cteMDBNode_C''])) ::mdb_node_C ptr) \<and>
s' \<Turnstile>\<^sub>c (Ptr (POINTER)::cte_C ptr) \<and> REST) =
(POINTER \<noteq> 0 \<longrightarrow>
s' \<Turnstile>\<^sub>c (Ptr (POINTER)::cte_C ptr) \<and> REST)"
apply (rule iffI, clarsimp+)
apply (rule c_guard_field_lvalue)
apply (rule c_guard_h_t_valid, assumption)
apply (fastforce simp: typ_uinfo_t_def)+
done
(************************************************************************)
(* *)
(* cteSwap_ccorres ******************************************************)
@ -1648,7 +1340,7 @@ lemma cteSwap_ccorres:
\<comment> \<open>Start proofs\<close>
apply (ctac (no_vcg) pre: ccorres_pre_getCTE ccorres_move_guard_ptr_safe
apply (ctac (no_vcg) pre: ccorres_pre_getCTE
add: ccorres_return_cte_mdbnode_safer [where ptr="slot"])+
\<comment> \<open>generates maingoal + 2 subgoals (Haskell pre/post and C pre/post) for each instruction (except getCTE)\<close>
@ -1666,9 +1358,7 @@ lemma cteSwap_ccorres:
apply (ctac (no_vcg) add: updateMDB_mdbNext_set_mdbPrev)
apply (rule ccorres_move_c_guard_cte)
apply (ctac (no_vcg) pre: ccorres_getCTE
ccorres_move_guard_ptr_safe
add: ccorres_return_cte_mdbnode [where ptr = slot']
ccorres_move_guard_ptr_safe )+
add: ccorres_return_cte_mdbnode [where ptr = slot'])+
apply csymbr
apply csymbr
apply (erule_tac t = ret__unsigned in ssubst)
@ -1821,21 +1511,6 @@ done
(* todo change in cteMove (\<lambda>s. ctes_of s src = Some scte) *)
(************************************************************************)
(* *)
(* lemmas used in emptySlot_ccorres *************************************)
@ -1850,25 +1525,6 @@ declare if_split [split del]
one should write CALL mdb_node_ptr_set_mdbNext
*)
lemma not_NullCap_eq_not_cap_null_cap:
" \<lbrakk>ccap_relation cap cap' ; (s, s') \<in> rf_sr \<rbrakk> \<Longrightarrow>
(cap \<noteq> NullCap) = (s' \<in> {_. (cap_get_tag cap' \<noteq> scast cap_null_cap)})"
apply (rule iffI)
apply (case_tac "cap_get_tag cap' \<noteq> scast cap_null_cap", clarsimp+)
apply (erule notE)
apply (simp add: cap_get_tag_NullCap)
apply (case_tac "cap_get_tag cap' \<noteq> scast cap_null_cap")
apply (rule notI)
apply (erule notE)
apply (simp add: cap_get_tag_NullCap)
apply clarsimp
done
lemma mdbPrev_CL_mdb_node_lift_mask [simp]:
"mdbPrev_CL (mdb_node_lift mdbNode) && ~~ mask 3
= mdbPrev_CL (mdb_node_lift mdbNode)"
@ -1936,8 +1592,7 @@ lemma emptySlot_helper:
apply (erule_tac t = s' in ssubst)
apply (simp add: carch_state_relation_def cmachine_state_relation_def h_t_valid_clift_Some_iff
cvariable_array_map_const_add_map_option[where f="tcb_no_ctes_proj"]
typ_heap_simps'
cong: lifth_update)
typ_heap_simps')
apply (erule (1) setCTE_tcb_case)
apply (erule (2) cspace_cte_relation_upd_mdbI)
@ -1967,8 +1622,7 @@ lemma emptySlot_helper:
apply (simp add: carch_state_relation_def cmachine_state_relation_def
h_t_valid_clift_Some_iff
cvariable_array_map_const_add_map_option[where f="tcb_no_ctes_proj"]
typ_heap_simps'
cong: lifth_update)
typ_heap_simps')
apply (erule (1) setCTE_tcb_case)
apply (erule (2) cspace_cte_relation_upd_mdbI)
@ -2014,7 +1668,6 @@ lemma mdbPrev_CL_mdb_node_lift_eq_mdbPrev:
"cmdbnode_relation n n' \<Longrightarrow> (mdbPrev_CL (mdb_node_lift n')) =(mdbPrev n)"
by (erule cmdbnode_relationE, fastforce simp: mdbNext_to_H)
lemma mdbNext_not_zero_eq_simpler:
"cmdbnode_relation n n' \<Longrightarrow> (mdbNext n \<noteq> 0) = (mdbNext_CL (mdb_node_lift n') \<noteq> 0)"
apply clarsimp
@ -2022,8 +1675,6 @@ lemma mdbNext_not_zero_eq_simpler:
apply (fastforce simp: mdbNext_to_H)
done
lemma mdbPrev_not_zero_eq_simpler:
"cmdbnode_relation n n' \<Longrightarrow> (mdbPrev n \<noteq> 0) = (mdbPrev_CL (mdb_node_lift n') \<noteq> 0)"
apply clarsimp
@ -2031,73 +1682,6 @@ lemma mdbPrev_not_zero_eq_simpler:
apply (fastforce simp: mdbPrev_to_H)
done
lemma h_t_valid_and_cslift_and_c_guard_field_mdbPrev_CL:
" \<lbrakk>(s, s') \<in> rf_sr; cte_at' slot s; valid_mdb' s; cslift s' (Ptr slot) = Some cte'\<rbrakk>
\<Longrightarrow> (mdbPrev_CL (mdb_node_lift (cteMDBNode_C cte')) \<noteq> 0) \<longrightarrow>
s' \<Turnstile>\<^sub>c ( Ptr (mdbPrev_CL (mdb_node_lift (cteMDBNode_C cte'))) :: cte_C ptr) \<and>
(\<exists> cten. cslift s' (Ptr (mdbPrev_CL (mdb_node_lift (cteMDBNode_C cte'))) :: cte_C ptr) = Some cten) \<and>
c_guard (Ptr &(Ptr (mdbPrev_CL (mdb_node_lift (cteMDBNode_C cte')))::cte_C ptr\<rightarrow>[''cteMDBNode_C'']) :: mdb_node_C ptr)"
apply (clarsimp simp: cte_wp_at_ctes_of)
apply (drule (1) valid_mdb_ctes_of_prev)
apply (frule (2) rf_sr_cte_relation)
apply (drule ccte_relation_cmdbnode_relation)
apply (simp add: mdbPrev_not_zero_eq_simpler)
apply (clarsimp simp: cte_wp_at_ctes_of)
apply (drule (1) rf_sr_ctes_of_clift [rotated])+
apply (clarsimp simp: typ_heap_simps)
apply (rule c_guard_field_lvalue [rotated])
apply (fastforce simp: typ_uinfo_t_def)+
apply (rule c_guard_clift)
apply (simp add: typ_heap_simps)
done
lemma h_t_valid_and_cslift_and_c_guard_field_mdbNext_CL:
" \<lbrakk>(s, s') \<in> rf_sr; cte_at' slot s; valid_mdb' s; cslift s' (Ptr slot) = Some cte'\<rbrakk>
\<Longrightarrow> (mdbNext_CL (mdb_node_lift (cteMDBNode_C cte')) \<noteq> 0) \<longrightarrow>
s' \<Turnstile>\<^sub>c ( Ptr (mdbNext_CL (mdb_node_lift (cteMDBNode_C cte'))) :: cte_C ptr) \<and>
(\<exists> cten. cslift s' (Ptr (mdbNext_CL (mdb_node_lift (cteMDBNode_C cte'))) :: cte_C ptr) = Some cten) \<and>
c_guard (Ptr &(Ptr (mdbNext_CL (mdb_node_lift (cteMDBNode_C cte')))::cte_C ptr\<rightarrow>[''cteMDBNode_C'']) :: mdb_node_C ptr)"
apply (clarsimp simp: cte_wp_at_ctes_of)
apply (drule (1) valid_mdb_ctes_of_next)
apply (frule (2) rf_sr_cte_relation)
apply (drule ccte_relation_cmdbnode_relation)
apply (simp add: mdbNext_not_zero_eq_simpler)
apply (clarsimp simp: cte_wp_at_ctes_of)
apply (drule (1) rf_sr_ctes_of_clift [rotated])+
apply (clarsimp simp: typ_heap_simps)
apply (rule c_guard_field_lvalue [rotated])
apply (fastforce simp: typ_uinfo_t_def)+
apply (rule c_guard_clift)
apply (simp add: typ_heap_simps)
done
lemma valid_mdb_Prev_neq_Next_better:
"\<lbrakk> valid_mdb' s; ctes_of s p = Some cte \<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow>
(mdbNext (cteMDBNode cte)) \<noteq> (mdbPrev (cteMDBNode cte))"
apply (rule impI)
apply (simp add: valid_mdb'_def)
apply (simp add: valid_mdb_ctes_def)
apply (elim conjE)
apply (drule (1) mdb_chain_0_no_loops)
apply (simp add: valid_dlist_def)
apply (erule_tac x=p in allE)
apply (erule_tac x=cte in allE)
apply (simp add: Let_def)
apply clarsimp
apply (drule_tac s="mdbNext (cteMDBNode cte)" in sym)
apply simp
apply (simp add: no_loops_def)
apply (erule_tac x= "(mdbNext (cteMDBNode cte))" in allE)
apply (erule notE, rule trancl_trans)
apply (rule r_into_trancl)
apply (simp add: mdb_next_unfold)
apply (rule r_into_trancl)
apply (simp add: mdb_next_unfold)
done
(* TODO: move *)
definition
@ -2183,13 +1767,6 @@ lemmas ccorres_split_noop_lhs
= ccorres_split_nothrow[where c=Skip, OF _ ceqv_refl _ _ hoarep.Skip,
simplified ccorres_seq_skip]
(* FIXME: to SR_Lemmas *)
lemma region_is_bytes_subset:
"region_is_bytes' ptr sz htd
\<Longrightarrow> {ptr' ..+ sz'} \<subseteq> {ptr ..+ sz}
\<Longrightarrow> region_is_bytes' ptr' sz' htd"
by (auto simp: region_is_bytes'_def)
lemma region_actually_is_bytes_subset:
"region_actually_is_bytes' ptr sz htd
\<Longrightarrow> {ptr' ..+ sz'} \<subseteq> {ptr ..+ sz}
@ -2507,7 +2084,7 @@ lemma emptySlot_ccorres:
apply (simp only:Ptr_not_null_pointer_not_zero) \<comment> \<open>replaces Ptr p \<noteq> NULL with p\<noteq>0\<close>
\<comment> \<open>--- instruction: y \<leftarrow> updateMDB (mdbPrev rva) (mdbNext_update (\<lambda>_. mdbNext rva))\<close>
apply (ctac (no_simp, no_vcg) pre:ccorres_move_guard_ptr_safe
apply (ctac (no_simp, no_vcg)
add: updateMDB_mdbPrev_set_mdbNext)
\<comment> \<open>here ctac alone does not apply because the subgoal generated
by the rule are not solvable by simp\<close>
@ -2524,11 +2101,11 @@ lemma emptySlot_ccorres:
\<comment> \<open>--- instruction: y \<leftarrow> updateCap slot capability.NullCap;\<close>
apply (simp del: Collect_const)
apply csymbr
apply (ctac (no_vcg) pre:ccorres_move_guard_ptr_safe)
apply (ctac (no_vcg) pre:)
apply csymbr
apply (rule ccorres_move_c_guard_cte)
\<comment> \<open>--- instruction y \<leftarrow> updateMDB slot (\<lambda>a. nullMDBNode);\<close>
apply (ctac (no_vcg) pre: ccorres_move_guard_ptr_safe
apply (ctac (no_vcg)
add: ccorres_updateMDB_const [unfolded const_def])
\<comment> \<open>the post_cap_deletion case\<close>
@ -2692,29 +2269,6 @@ lemma cap_get_tag_PageCap_frame:
apply (simp add: cap_get_tag_isCap isCap_simps pageSize_def)
done
lemma is_aligned_small_frame_cap_lift:
"cap_get_tag cap = scast cap_small_frame_cap \<Longrightarrow>
is_aligned (cap_small_frame_cap_CL.capFBasePtr_CL
(cap_small_frame_cap_lift cap)) 12"
by (simp add: cap_small_frame_cap_lift_def cap_lift_small_frame_cap)
lemma fff_is_pageBits:
"(0xFFF :: word32) = 2 ^ pageBits - 1"
by (simp add: pageBits_def)
(* used? *)
lemma valid_cap'_PageCap_is_aligned:
"valid_cap' (ArchObjectCap (arch_capability.PageCap d w r sz option)) t \<Longrightarrow>
is_aligned w (pageBitsForSize sz)"
apply (simp add: valid_cap'_def capAligned_def)
done
lemma gen_framesize_to_H_is_framesize_to_H_if_not_ARMSmallPage:
" c\<noteq>scast Kernel_C.ARMSmallPage \<Longrightarrow>gen_framesize_to_H c = framesize_to_H c"
by (simp add: gen_framesize_to_H_def framesize_to_H_def)
@ -3064,13 +2618,6 @@ definition
if isZombieTCB_C type then 9 else unat (type && mask 5) + 4
| _ \<Rightarrow> 0"
lemma frame_cap_size [simp]:
"cap_get_tag cap = scast cap_frame_cap
\<Longrightarrow> cap_frame_cap_CL.capFSize_CL (cap_frame_cap_lift cap) && mask 2 =
cap_frame_cap_CL.capFSize_CL (cap_frame_cap_lift cap)"
apply (simp add: cap_frame_cap_lift_def)
by (simp add: cap_lift_def cap_tag_defs mask_def word_bw_assocs)
lemma generic_frame_cap_size[simp]:
"cap_get_tag cap = scast cap_frame_cap \<or> cap_get_tag cap = scast cap_small_frame_cap
\<Longrightarrow> generic_frame_cap_get_capFSize_CL (cap_lift cap) && mask 2 =
@ -3143,13 +2690,6 @@ lemma ccap_relation_get_capSizeBits_physical:
split: if_split_asm)+
done
lemma ccap_relation_get_capSizeBits_untyped:
"\<lbrakk> ccap_relation (UntypedCap d word bits idx) ccap \<rbrakk> \<Longrightarrow>
get_capSizeBits_CL (cap_lift ccap) = bits"
apply (frule cap_get_tag_isCap_unfolded_H_cap)
by (clarsimp simp: get_capSizeBits_CL_def ccap_relation_def
map_option_case cap_to_H_def cap_lift_def cap_tag_defs)
definition
get_capZombieBits_CL :: "cap_zombie_cap_CL \<Rightarrow> word32" where
"get_capZombieBits_CL \<equiv> \<lambda>cap.
@ -3320,12 +2860,6 @@ lemma cap_get_capIsPhysical_spec:
cap_page_directory_cap_lift_def cap_asid_pool_cap_lift_def
Let_def cap_untyped_cap_lift_def split: if_split_asm)
lemma ccap_relation_get_capPtr_not_physical:
"\<lbrakk> ccap_relation hcap ccap; capClass hcap \<noteq> PhysicalClass \<rbrakk> \<Longrightarrow>
get_capPtr_CL (cap_lift ccap) = Ptr 0"
by (clarsimp simp: ccap_relation_def get_capPtr_CL_def cap_to_H_def Let_def
split: option.split cap_CL.split_asm if_split_asm)
lemma ccap_relation_get_capIsPhysical:
"ccap_relation hcap ccap \<Longrightarrow> isPhysicalCap hcap = get_capIsPhysical_CL (cap_lift ccap)"
apply (case_tac hcap; clarsimp simp: cap_lifts cap_lift_domain_cap cap_lift_null_cap
@ -3391,13 +2925,6 @@ lemma ccap_relation_get_capPtr_physical:
done
done
lemma ccap_relation_get_capPtr_untyped:
"\<lbrakk> ccap_relation (UntypedCap d word bits idx) ccap \<rbrakk> \<Longrightarrow>
get_capPtr_CL (cap_lift ccap) = Ptr word"
apply (frule cap_get_tag_isCap_unfolded_H_cap)
by (clarsimp simp: get_capPtr_CL_def ccap_relation_def
map_option_case cap_to_H_def cap_lift_def cap_tag_defs)
lemma cap_get_tag_isArchCap_unfolded_H_cap:
"ccap_relation (capability.ArchObjectCap a_cap) cap' \<Longrightarrow>
(isArchCap_tag (cap_get_tag cap'))"
@ -3515,10 +3042,8 @@ lemma sameRegionAs_spec:
clarsimp simp: unat_of_nat32 word_bits_def
dest!: get_capSizeBits_valid_shift)+
apply (clarsimp simp: ccap_relation_get_capPtr_physical
ccap_relation_get_capPtr_untyped
ccap_relation_get_capIsPhysical[symmetric]
ccap_relation_get_capSizeBits_physical
ccap_relation_get_capSizeBits_untyped)
ccap_relation_get_capSizeBits_physical)
apply (intro conjI impI)
apply ((clarsimp simp: ccap_relation_def map_option_case
cap_untyped_cap_lift cap_to_H_def
@ -3543,15 +3068,6 @@ lemma sameRegionAs_spec:
apply (fastforce simp: isArchCap_tag_def2 split: if_split)
done
lemma gen_framesize_to_H_eq:
"\<lbrakk> a \<le> 3; b \<le> 3 \<rbrakk> \<Longrightarrow>
(gen_framesize_to_H a = gen_framesize_to_H b) = (a = b)"
by (fastforce simp: gen_framesize_to_H_def Kernel_C.ARMSmallPage_def
Kernel_C.ARMLargePage_def Kernel_C.ARMSection_def
word_le_make_less
split: if_split
dest: word_less_cases)
lemma framesize_to_H_eq:
"\<lbrakk> a \<le> 3; b \<le> 3; a \<noteq> 0; b \<noteq> 0 \<rbrakk> \<Longrightarrow>
(framesize_to_H a = framesize_to_H b) = (a = b)"
@ -4239,27 +3755,5 @@ lemma (in kernel_m) updateMDB_set_mdbPrev:
apply (simp)
done
lemma (in kernel_m) updateMDB_set_mdbNext:
"ccorres dc xfdc
( \<lambda>s. is_aligned ptr 3 \<and> (slota\<noteq>0 \<longrightarrow> is_aligned slota 3))
{s. slotc = slota} hs
(updateMDB ptr (mdbNext_update (\<lambda>_. slota)))
(IF ptr \<noteq> 0
THEN
Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t (Ptr ptr:: cte_C ptr)\<rbrace>
(call (\<lambda>ta. ta(| mdb_node_ptr_' := Ptr &(Ptr ptr:: cte_C ptr
\<rightarrow>[''cteMDBNode_C'']),
v32_' := slotc |))
mdb_node_ptr_set_mdbNext_'proc (\<lambda>s t. s\<lparr> globals := globals t \<rparr>) (\<lambda>ta s'. Basic (\<lambda>a. a)))
FI)"
apply (rule ccorres_guard_imp2) \<comment> \<open>replace preconditions by schematics\<close>
\<comment> \<open>Main Goal\<close>
apply (rule ccorres_Cond_rhs)
apply (rule ccorres_updateMDB_cte_at)
apply (ctac add: ccorres_updateMDB_set_mdbNext)
apply (ctac ccorres: ccorres_updateMDB_skip)
apply simp
done
end
end

View File

@ -51,22 +51,6 @@ lemma not_snd_bindE_I1:
unfolding bindE_def
by (erule not_snd_bindI1)
lemma ccorres_remove_bind_returnOk_noguard:
assumes ac: "ccorres (f \<currency> r') xf P P' (SKIP # hs) a c"
and rr: "\<And>v s'. r' v (exvalue (xf s')) \<Longrightarrow> r (g v) (exvalue (xf s'))"
shows "ccorres (f \<currency> r) xf P P' (SKIP # hs) (a >>=E (\<lambda>v. returnOk (g v))) c"
apply (rule ccorresI')
apply clarsimp
apply (drule not_snd_bindE_I1)
apply (erule (4) ccorresE[OF ac])
apply (clarsimp simp add: bindE_def returnOk_def NonDetMonad.lift_def bind_def return_def
split_def)
apply (rule bexI [rotated], assumption)
apply (simp add: throwError_def return_def unif_rrel_def
split: sum.splits)
apply (auto elim!: rr)
done
declare isCNodeCap_CNodeCap[simp]
(* MOVE *)
@ -119,37 +103,6 @@ lemma wordFromRights_inj:
"inj wordFromRights"
by (rule inj_on_inverseI, rule rightsFromWord_wordFromRights)
lemmas wordFromRights_eq = inj_eq [OF wordFromRights_inj]
lemma rightsFromWord_and:
"rightsFromWord (a && b) = andCapRights (rightsFromWord a) (rightsFromWord b)"
by (simp add: rightsFromWord_def andCapRights_def)
lemma andCapRights_ac:
"andCapRights (andCapRights a b) c = andCapRights a (andCapRights b c)"
"andCapRights a b = andCapRights b a"
"andCapRights a (andCapRights b c) = andCapRights b (andCapRights a c)"
by (simp add: andCapRights_def conj_comms split: cap_rights.split)+
lemma wordFromRights_rightsFromWord:
"wordFromRights (rightsFromWord w) = w && mask 3"
apply (simp add: wordFromRights_def rightsFromWord_def
mask_def)
apply (auto simp: bin_nth_ops bin_nth_Bit0 bin_nth_Bit1 numeral_2_eq_2
intro!: word_eqI)
done
(* FIXME: move, duplicated in CSpace_C *)
lemma ccorres_cases:
assumes P: " P \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf ar axf G G' hs a b"
assumes notP: "\<not>P \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf ar axf H H' hs a b"
shows "ccorres_underlying sr \<Gamma> r xf ar axf (\<lambda>s. (P \<longrightarrow> G s) \<and> (\<not>P \<longrightarrow> H s))
({s. P \<longrightarrow> s \<in> G'} \<inter> {s. \<not>P \<longrightarrow> s \<in> H'})
hs a b"
apply (cases P, auto simp: P notP)
done
lemma monadic_rewrite_stateAssert:
"monadic_rewrite F E P (stateAssert P xs) (return ())"
by (simp add: stateAssert_def monadic_rewrite_def exec_get)
@ -604,12 +557,6 @@ lemma cap_rights_to_H_from_word_canon [simp]:
apply (simp add: cap_rights_to_H_def)
done
(* MOVE *)
lemma to_bool_false [simp]:
"to_bool false = False"
unfolding to_bool_def false_def
by simp
(* MOVE *)
lemma tcb_aligned':
"tcb_at' t s \<Longrightarrow> is_aligned t tcbBlockSizeBits"
@ -618,19 +565,6 @@ lemma tcb_aligned':
apply (simp add: objBits_simps)
done
lemma tcb_ptr_to_ctcb_ptr_mask [simp]:
assumes tcbat: "tcb_at' thread s"
shows "ptr_val (tcb_ptr_to_ctcb_ptr thread) && ~~mask tcbBlockSizeBits = thread"
proof -
have "thread + ctcb_offset && ~~ mask tcbBlockSizeBits = thread"
proof (rule add_mask_lower_bits)
show "is_aligned thread tcbBlockSizeBits" using tcbat by (rule tcb_aligned')
qed (auto simp: word_bits_def ctcb_offset_defs objBits_defs)
thus ?thesis
unfolding tcb_ptr_to_ctcb_ptr_def ctcb_offset_def
by (simp add: mask_def)
qed
abbreviation
"lookupSlot_raw_xf \<equiv>
liftxf errstate lookupSlot_raw_ret_C.status_C

View File

@ -148,9 +148,6 @@ lemma array_assertion_abs_pt:
apply (rule_tac x=0 in exI, simp)
done
lemmas ccorres_move_array_assertion_pt
= ccorres_move_array_assertions[OF array_assertion_abs_pt]
lemma c_guard_abs_pde:
"\<forall>s s'. (s, s') \<in> rf_sr \<and> pde_at' (ptr_val p) s \<and> True
\<longrightarrow> s' \<Turnstile>\<^sub>c (p :: pde_C ptr)"

View File

@ -315,40 +315,6 @@ lemma cteDelete_invs'':
apply clarsimp
done
lemma ccorres_Cond_rhs_Seq_ret_int:
"\<lbrakk> P \<Longrightarrow> ccorres rvr xf Q S hs absf (f;;h);
\<And>rv' t t'. ceqv \<Gamma> ret__int_' rv' t t' (g ;; h) (j rv');
\<not> P \<Longrightarrow> ccorres rvr xf R T hs absf (j 0) \<rbrakk>
\<Longrightarrow> ccorres rvr xf (\<lambda>s. (P \<longrightarrow> Q s) \<and> (\<not> P \<longrightarrow> R s))
{s. (P \<longrightarrow> s \<in> S) \<and> (\<not> P \<longrightarrow> s \<in> {s. s \<in> T \<and> ret__int_' s = 0})}
hs absf (Cond {s. P} f g ;; h)"
apply (rule ccorres_guard_imp2)
apply (erule ccorres_Cond_rhs_Seq)
apply (erule ccorres_abstract)
apply (rule_tac P="rv' = 0" in ccorres_gen_asm2)
apply simp
apply simp
done
(* it's a little painful to have to do this from first principles *)
lemma ccorres_cutMon_stateAssert:
"\<lbrakk> Q s \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf P P' hs
(cutMon ((=) s) (a ())) c \<rbrakk> \<Longrightarrow>
ccorres_underlying sr Gamm r xf arrel axf (\<lambda>s. Q s \<longrightarrow> P s) P' hs
(cutMon ((=) s) (stateAssert Q [] >>= a)) c"
apply (simp add: cutMon_walk_bind)
apply (cases "\<not> Q s")
apply (simp add: stateAssert_def cutMon_def exec_get assert_def
ccorres_fail'
cong: if_cong[OF eq_commute])
apply (rule ccorres_guard_imp2)
apply (rule ccorres_drop_cutMon_bind)
apply (rule ccorres_symb_exec_l)
apply (rule ccorres_cutMon)
apply (simp add: stateAssert_def exec_get return_def)
apply (wp | simp)+
done
lemma valid_Zombie_number_word_bits:
"valid_cap' cap s \<Longrightarrow> isZombie cap
\<Longrightarrow> capZombieNumber cap < 2 ^ word_bits"
@ -654,13 +620,6 @@ lemma reduceZombie_ccorres1:
apply auto
done
lemma induction_setup_helper:
"\<lbrakk> \<And>s slot exposed. P s slot exposed \<Longrightarrow> Q s slot exposed;
\<lbrakk> \<And>s slot exposed. P s slot exposed \<Longrightarrow> Q s slot exposed \<rbrakk>
\<Longrightarrow> P s slot exposed \<rbrakk>
\<Longrightarrow> Q s slot exposed"
by auto
schematic_goal finaliseSlot_ccorres_induction_helper:
"\<And>s slot exposed. ?P s slot exposed
\<Longrightarrow> ccorres (cintr \<currency> (\<lambda>(success, irqopt) (success', irq'). success' = from_bool success \<and> ccap_relation irqopt irq' \<and> cleanup_info_wf' irqopt))

View File

@ -146,38 +146,6 @@ lemma heap_list_s_heap_list':
apply (simp add: hrs_htd_def hrs_mem_def heap_list_s_heap_list)
done
lemma lift_t_typ_clear_region:
assumes doms: "\<And>x :: 'a :: mem_type ptr. \<lbrakk> hrs_htd hp,g \<Turnstile>\<^sub>t x; x \<in> - (Ptr ` {ptr ..+2 ^ bits}) \<rbrakk>
\<Longrightarrow> {ptr_val x..+size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {}"
shows "(lift_t g (hrs_htd_update (typ_clear_region ptr bits) hp) :: 'a :: mem_type typ_heap) =
lift_t g hp |` (- Ptr ` {ptr ..+2 ^ bits})"
apply (rule ext)
apply (case_tac "({ptr_val x..+size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {} \<and> hrs_htd hp,g \<Turnstile>\<^sub>t x)")
apply (clarsimp simp add: lift_t_def lift_typ_heap_if s_valid_def h_t_valid_ptr_clear_region)
apply (subgoal_tac "x \<in> - Ptr ` {ptr..+2 ^ bits}")
apply clarsimp
apply (subst heap_list_s_heap_list')
apply (clarsimp simp add: hrs_htd_update h_t_valid_ptr_clear_region)
apply (erule h_t_valid_taut)
apply (subst heap_list_s_heap_list')
apply (clarsimp elim!: h_t_valid_taut)
apply simp
apply clarsimp
apply (drule (1) orthD2)
apply (erule contrapos_np, rule intvl_self)
apply (simp add: size_of_def wf_size_desc_gt)
apply (simp add: lift_t_def lift_typ_heap_if s_valid_def h_t_valid_ptr_clear_region del: disj_not1 split del: if_split)
apply (subst if_not_P)
apply simp
apply (case_tac "x \<in> (- Ptr ` {ptr..+2 ^ bits})")
apply (simp del: disj_not1)
apply (erule contrapos_pn)
apply simp
apply (erule doms)
apply simp
apply simp
done
lemma image_Ptr:
"Ptr ` S = {x. ptr_val x \<in> S}"
apply (safe, simp_all)
@ -240,40 +208,6 @@ proof (rule rl)
qed
(*FIX me: move *)
lemma valid_untyped_pspace_no_overlap':
assumes vuc: "s \<turnstile>' UntypedCap d ptr bits idx"
and idx: "idx< 2^ bits"
and psp_al: "pspace_aligned' s" "pspace_distinct' s"
shows "pspace_no_overlap' (ptr + of_nat idx) bits s"
proof -
note blah[simp del] = atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex
from vuc have al: "is_aligned ptr bits" and vu: "valid_untyped' d ptr bits idx s" and p0: "ptr \<noteq> 0"
and wb: "bits < word_bits"
by (auto elim!: valid_untyped_capE)
from vuc idx
have [simp]: "(ptr + (of_nat idx) && ~~ mask bits) = ptr"
apply -
apply (rule is_aligned_add_helper[THEN conjunct2])
apply (clarsimp simp:valid_cap'_def capAligned_def)+
apply (rule word_of_nat_less)
apply simp
done
show "pspace_no_overlap' (ptr + of_nat idx) bits s"
using vuc idx psp_al
apply -
apply (clarsimp simp:valid_cap'_def valid_untyped'_def pspace_no_overlap'_def)
apply (drule_tac x = x in spec)
apply (frule(1) pspace_alignedD')
apply (frule(1) pspace_distinctD')
apply (clarsimp simp:ko_wp_at'_def obj_range'_def p_assoc_help)
done
qed
lemma cmap_relation_disjoint:
fixes rel :: "'a :: pspace_storable \<Rightarrow> 'b :: mem_type \<Rightarrow> bool" and x :: "'b :: mem_type ptr"
assumes vuc: "s \<turnstile>' UntypedCap d ptr bits idx"
@ -344,23 +278,6 @@ proof -
qed
qed
lemma vut_subseteq:
notes blah[simp del] = atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex
shows "\<lbrakk>s \<turnstile>' UntypedCap d ptr bits idx;idx < 2 ^ bits\<rbrakk>
\<Longrightarrow> Ptr ` {ptr + of_nat idx..ptr + 2 ^ bits - 1} \<subseteq> Ptr ` {ptr ..+ 2^bits}" (is "\<lbrakk>?a1;?a2\<rbrakk> \<Longrightarrow> ?b \<subseteq> ?c")
apply (subgoal_tac "?c = Ptr ` {ptr ..ptr + 2 ^ bits - 1}")
apply (simp add:inj_image_subset_iff)
apply (clarsimp simp:blah valid_cap'_def capAligned_def)
apply (rule is_aligned_no_wrap')
apply simp+
apply (rule word_of_nat_less)
apply simp
apply (rule arg_cong[where f = "\<lambda>x. Ptr ` x"])
apply (rule upto_intvl_eq)
apply (clarsimp simp:valid_cap'_def capAligned_def)+
done
(* CLAG : IpcCancel_C *)
lemma tcb_ptr_to_ctcb_ptr_imageD:
"x \<in> tcb_ptr_to_ctcb_ptr ` S \<Longrightarrow> ctcb_ptr_to_tcb_ptr x \<in> S"
@ -368,12 +285,6 @@ lemma tcb_ptr_to_ctcb_ptr_imageD:
apply simp
done
lemma ctcb_ptr_to_tcb_ptr_imageI:
"ctcb_ptr_to_tcb_ptr x \<in> S \<Longrightarrow> x \<in> tcb_ptr_to_ctcb_ptr ` S"
apply (drule imageI [where f = tcb_ptr_to_ctcb_ptr])
apply simp
done
lemma aligned_ranges_subset_or_disjointE [consumes 2, case_names disjoint subset1 subset2]:
"\<lbrakk>is_aligned p n; is_aligned p' n';
{p..p + 2 ^ n - 1} \<inter> {p'..p' + 2 ^ n' - 1} = {} \<Longrightarrow> P;
@ -641,17 +552,6 @@ lemma tcb_cte_cases_aligned:
apply (simp add: objBits_simps')
done
lemma tcb_cte_in_range':
"\<lbrakk> ksPSpace s p = Some (KOTCB tcb); is_aligned p tcbBlockSizeBits;
tcb_cte_cases n = Some (getF, setF) \<rbrakk>
\<Longrightarrow> {p + n..+2 ^ objBits (cte :: cte)} \<subseteq> {p ..+ 2 ^ objBits tcb}"
apply (subst upto_intvl_eq)
apply (erule (1) tcb_cte_cases_aligned)
apply (subst upto_intvl_eq)
apply (simp add: objBits_simps')
apply (erule (2) tcb_cte_in_range)
done
(* clagged from above :( Were I smarter or if I cared more I could probably factor out more \<dots>*)
lemma cmap_relation_disjoint_cte:
assumes vuc: "s \<turnstile>' UntypedCap d ptr bits idx"
@ -1078,9 +978,6 @@ lemma surj_ctcb_ptr_to_tcb_ptr [simp]:
"surj ctcb_ptr_to_tcb_ptr"
by (rule surjI [where f = "tcb_ptr_to_ctcb_ptr"], simp)
lemma bij_ctcb_ptr_to_tcb_ptr [simp]:
"bij ctcb_ptr_to_tcb_ptr" by (simp add: bijI)
lemma cmap_relation_restrict_both:
"\<lbrakk> cmap_relation am cm f rel; bij f\<rbrakk> \<Longrightarrow> cmap_relation (am |` (- S)) (cm |` (- f ` S)) f rel"
unfolding cmap_relation_def
@ -1450,13 +1347,6 @@ lemma hrs_ghost_update_comm:
(ghost'state_'_update g \<circ> t_hrs_'_update f)"
by (rule ext) simp
lemma htd_safe_typ_clear_region:
"htd_safe S htd \<Longrightarrow> htd_safe S (typ_clear_region ptr bits htd)"
apply (clarsimp simp: htd_safe_def dom_s_def typ_clear_region_def)
apply (simp add: subset_iff)
apply blast
done
lemma htd_safe_typ_region_bytes:
"htd_safe S htd \<Longrightarrow> {ptr ..+ 2 ^ bits} \<subseteq> S \<Longrightarrow> htd_safe S (typ_region_bytes ptr bits htd)"
apply (clarsimp simp: htd_safe_def dom_s_def typ_region_bytes_def)

View File

@ -243,10 +243,6 @@ end
context kernel_m begin
lemma capMasterCap_NullCap_eq:
"(capMasterCap c = NullCap) = (c = NullCap)"
by (auto dest!: capMasterCap_eqDs)
lemma getCTE_h_val_ccorres_split:
assumes var: "\<And>s f s'. var (var_update f s) = f (var s)
\<and> ((s', var_update f s) \<in> rf_sr) = ((s', s) \<in> rf_sr)"
@ -336,11 +332,6 @@ lemma ccorres_abstract_all:
declare of_int_sint_scast[simp]
lemma stateAssert_bind_out_of_if:
"If P f (stateAssert Q xs >>= g) = stateAssert (\<lambda>s. \<not> P \<longrightarrow> Q s) [] >>= (\<lambda>_. If P f (g ()))"
"If P (stateAssert Q xs >>= g) f = stateAssert (\<lambda>s. P \<longrightarrow> Q s) [] >>= (\<lambda>_. If P (g ()) f)"
by (simp_all add: fun_eq_iff stateAssert_def exec_get split: if_split)
lemma isCNodeCap_capUntypedPtr_capCNodePtr:
"isCNodeCap c \<Longrightarrow> capUntypedPtr c = capCNodePtr c"
by (clarsimp simp: isCap_simps)
@ -642,14 +633,14 @@ lemma lookup_fp_ccorres':
apply (simp add: word_bw_assocs mask_and_mask min.absorb2)
apply (simp_all add: unat_sub word_le_nat_alt unat_eq_0[symmetric])
apply (simp_all add: unat_plus_if' if_P)
apply (clarsimp simp: rightsFromWord_and shiftr_over_and_dist
apply (clarsimp simp: shiftr_over_and_dist
size_of_def cte_level_bits_def field_simps shiftl_shiftl
shiftl_shiftr3 word_size)+
apply (clarsimp simp: unat_gt_0 from_bool_0 trans [OF eq_commute from_bool_eq_if])
apply (intro conjI impI, simp_all)[1]
apply (rule word_unat.Rep_inject[THEN iffD1], subst unat_plus_if')
apply (simp add: unat_plus_if' unat_of_nat32 word_bits_def)
apply (clarsimp simp: rightsFromWord_and shiftr_over_and_dist
apply (clarsimp simp: shiftr_over_and_dist
size_of_def cte_level_bits_def field_simps shiftl_shiftl
shiftl_shiftr3 word_size)+
apply (clarsimp simp: unat_gt_0 from_bool_0 trans [OF eq_commute from_bool_eq_if])
@ -669,31 +660,6 @@ lemma ccap_relation_case_sum_Null_endpoint:
by (clarsimp simp: cap_get_tag_isCap isRight_def isCap_simps
split: sum.split_asm)
lemma findPDForASID_pd_at_asid_noex:
"\<lbrace>pd_at_asid' pd asid\<rbrace> findPDForASID asid \<lbrace>\<lambda>rv s. rv = pd\<rbrace>,\<lbrace>\<bottom>\<bottom>\<rbrace>"
apply (simp add: findPDForASID_def
liftME_def bindE_assoc
cong: option.case_cong)
apply (rule seqE, rule assertE_sp)+
apply (rule seqE, rule liftE_wp, rule gets_sp)
apply (rule hoare_pre)
apply (rule seqE[rotated])
apply wpc
apply wp
apply (rule seqE[rotated])
apply (rule seqE[rotated])
apply (rule returnOk_wp)
apply (simp add:checkPDAt_def)
apply wp
apply (rule assertE_wp)
apply wpc
apply wp
apply (rule liftE_wp)
apply (rule getASID_wp)
apply (clarsimp simp: pd_at_asid'_def obj_at'_def projectKOs
inv_ASIDPool)
done
lemma ccorres_catch_bindE_symb_exec_l:
"\<lbrakk> \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; empty_fail f;
\<And>rv. ccorres_underlying sr G r xf ar axf (Q rv) (Q' rv) hs (catch (g rv) h >>= j) c;
@ -713,32 +679,6 @@ lemma ccorres_catch_bindE_symb_exec_l:
apply clarsimp
done
lemmas ccorres_catch_symb_exec_l
= ccorres_catch_bindE_symb_exec_l[where g=returnOk,
simplified bindE_returnOk returnOk_catch_bind]
lemma ccorres_alt_rdonly_bind:
"\<lbrakk> ccorres_underlying sr Gamm r xf arrel axf A A' hs
(f >>= (\<lambda>x. alternative (g x) h)) c;
\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; empty_fail f \<rbrakk>
\<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf A A' hs
(alternative (f >>= (\<lambda>x. g x)) h) c"
apply (rule ccorresI')
apply (erule(3) ccorresE)
defer
apply assumption
apply (subst alternative_left_readonly_bind, assumption)
apply (rule notI, drule(1) empty_failD)
apply (simp add: alternative_def bind_def)
apply fastforce
apply (subgoal_tac "\<forall>x \<in> fst (f s). snd x = s")
apply (simp add: bind_def alternative_def image_image split_def
cong: image_cong)
apply clarsimp
apply (drule use_valid, assumption, simp+)
done
definition
"pd_has_hwasid pd =
(\<lambda>s. \<exists>v. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) pd = {v})"
@ -816,113 +756,6 @@ lemmas stored_hw_asid_get_ccorres_split
= stored_hw_asid_get_ccorres_split'[OF refl]
stored_hw_asid_get_ccorres_split'[OF ptr_add_0xFF0]
lemma doMachineOp_pd_at_asid':
"\<lbrace>\<lambda>s. P (pd_at_asid' pd asid s)\<rbrace> doMachineOp oper \<lbrace>\<lambda>rv s. P (pd_at_asid' pd asid s)\<rbrace>"
apply (simp add: doMachineOp_def split_def)
apply wp
apply (clarsimp simp: pd_at_asid'_def)
done
lemma doMachineOp_page_directory_at_P':
"\<lbrace>\<lambda>s. P (page_directory_at' pd s)\<rbrace> doMachineOp oper \<lbrace>\<lambda>rv s. P (page_directory_at' pd s)\<rbrace>"
apply (simp add: doMachineOp_def split_def)
apply wp
apply (clarsimp simp: pd_at_asid'_def)
done
lemma pde_stored_asid_Some:
"(pde_stored_asid pde = Some v)
= (pde_get_tag pde = scast pde_pde_invalid
\<and> to_bool (stored_asid_valid_CL (pde_pde_invalid_lift pde))
\<and> v = ucast (stored_hw_asid_CL (pde_pde_invalid_lift pde)))"
by (auto simp add: pde_stored_asid_def split: if_split)
lemma pointerInUserData_c_guard':
"\<lbrakk> pointerInUserData ptr s; no_0_obj' s; is_aligned ptr 2 \<rbrakk>
\<Longrightarrow> c_guard (Ptr ptr :: word32 ptr)"
apply (simp add: pointerInUserData_def)
apply (simp add: c_guard_def ptr_aligned_def)
apply (rule conjI)
apply (simp add: is_aligned_def)
apply (simp add: c_null_guard_def)
apply (subst intvl_aligned_bottom_eq[where n=2 and bits=2], simp_all)
apply clarsimp
done
lemma heap_relation_user_word_at_cross_over:
"\<lbrakk> user_word_at x p s; cmap_relation (heap_to_user_data (ksPSpace s)
(underlying_memory (ksMachineState s))) (cslift s') Ptr cuser_user_data_relation;
p' = Ptr p \<rbrakk>
\<Longrightarrow> c_guard p' \<and> hrs_htd (t_hrs_' (globals s')) \<Turnstile>\<^sub>t p'
\<and> h_val (hrs_mem (t_hrs_' (globals s'))) p' = x"
apply (erule cmap_relationE1)
apply (clarsimp simp: heap_to_user_data_def Let_def
user_word_at_def pointerInUserData_def
typ_at_to_obj_at'[where 'a=user_data, simplified])
apply (drule obj_at_ko_at', clarsimp)
apply (rule conjI, rule exI, erule ko_at_projectKO_opt)
apply (rule refl)
apply (thin_tac "heap_to_user_data a b c = d" for a b c d)
apply (cut_tac x=p and w="~~ mask pageBits" in word_plus_and_or_coroll2)
apply (rule conjI)
apply (clarsimp simp: user_word_at_def pointerInUserData_def)
apply (simp add: c_guard_def c_null_guard_def ptr_aligned_def)
apply (drule lift_t_g)
apply (clarsimp simp: )
apply (simp add: align_of_def user_data_C_size_of user_data_C_align_of
size_of_def user_data_C_typ_name)
apply (fold is_aligned_def[where n=2, simplified], simp)
apply (erule contra_subsetD[rotated])
apply (rule order_trans[rotated])
apply (rule_tac x="p && mask pageBits" and y=4 in intvl_sub_offset)
apply (cut_tac y=p and a="mask pageBits && (~~ mask 2)" in word_and_le1)
apply (subst(asm) word_bw_assocs[symmetric], subst(asm) is_aligned_neg_mask_eq,
erule is_aligned_andI1)
apply (simp add: word_le_nat_alt mask_def pageBits_def)
apply simp
apply (clarsimp simp: cuser_user_data_relation_def user_word_at_def)
apply (frule_tac f="[''words_C'']" in h_t_valid_field[OF h_t_valid_clift],
simp+)
apply (drule_tac n="uint (p && mask pageBits >> 2)" in h_t_valid_Array_element)
apply simp
apply (simp add: shiftr_over_and_dist mask_def pageBits_def uint_and)
apply (insert int_and_leR [where a="uint (p >> 2)" and b=1023], clarsimp)[1]
apply (simp add: field_lvalue_def
field_lookup_offset_eq[OF trans, OF _ arg_cong[where f=Some, symmetric], OF _ prod.collapse]
word_shift_by_2 shiftr_shiftl1 is_aligned_neg_mask_eq is_aligned_andI1)
apply (drule_tac x="ucast (p >> 2)" in spec)
apply (simp add: byte_to_word_heap_def Let_def ucast_ucast_mask)
apply (fold shiftl_t2n[where n=2, simplified, simplified mult.commute mult.left_commute])
apply (simp add: aligned_shiftr_mask_shiftl pageBits_def)
apply (rule trans[rotated], rule_tac hp="hrs_mem (t_hrs_' (globals s'))"
and x="Ptr &(Ptr (p && ~~ mask 12) \<rightarrow> [''words_C''])"
in access_in_array)
apply (rule trans)
apply (erule typ_heap_simps)
apply simp+
apply (rule order_less_le_trans, rule unat_lt2p)
apply simp
apply (fastforce simp add: typ_info_word)
apply simp
apply (rule_tac f="h_val hp" for hp in arg_cong)
apply simp
apply (simp add: field_lvalue_def)
apply (simp add: ucast_nat_def ucast_ucast_mask)
apply (fold shiftl_t2n[where n=2, simplified, simplified mult.commute mult.left_commute])
apply (simp add: aligned_shiftr_mask_shiftl)
done
lemma pointerInUserData_h_t_valid2:
"\<lbrakk> pointerInUserData ptr s; cmap_relation (heap_to_user_data (ksPSpace s)
(underlying_memory (ksMachineState s))) (cslift s') Ptr cuser_user_data_relation;
is_aligned ptr 2 \<rbrakk>
\<Longrightarrow> hrs_htd (t_hrs_' (globals s')) \<Turnstile>\<^sub>t (Ptr ptr :: word32 ptr)"
apply (frule_tac p=ptr in
heap_relation_user_word_at_cross_over[rotated, OF _ refl])
apply (simp add: user_word_at_def)
apply simp
done
lemma dmo_clearExMonitor_setCurThread_swap:
"(do _ \<leftarrow> doMachineOp ARM.clearExMonitor;
setCurThread thread
@ -935,12 +768,6 @@ lemma dmo_clearExMonitor_setCurThread_swap:
simp_all add: select_f_oblivious)
done
lemma ccorres_bind_assoc_rev:
"ccorres_underlying sr E r xf arrel axf G G' hs ((a1 >>= a2) >>= a3) c
\<Longrightarrow> ccorres_underlying sr E r xf arrel axf G G' hs
(do x \<leftarrow> a1; y \<leftarrow> a2 x; a3 y od) c"
by (simp add: bind_assoc)
lemma monadic_rewrite_gets_l:
"(\<And>x. monadic_rewrite F E (P x) (g x) m)
\<Longrightarrow> monadic_rewrite F E (\<lambda>s. P (f s) s) (gets f >>= (\<lambda>x. g x)) m"
@ -1198,35 +1025,6 @@ lemma mdb_node_ptr_set_mdbPrev_np_spec:
apply (simp add: mdb_node_lift_def limited_and_simps mask_def)
done
lemma cap_reply_cap_ptr_new_np_spec2:
defines "ptr s \<equiv> cparent \<^bsup>s\<^esup>cap_ptr [''cap_C''] :: cte_C ptr"
shows
"\<forall>s. \<Gamma>\<turnstile> \<lbrace>s. hrs_htd \<^bsup>s\<^esup>t_hrs \<Turnstile>\<^sub>t ptr s \<and> is_aligned (capTCBPtr___unsigned_long_' s) 8
\<and> capReplyMaster___unsigned_long_' s && 1 = capReplyMaster___unsigned_long_' s\<rbrace>
Call cap_reply_cap_ptr_new_np_'proc
{t. (\<exists>cap.
cap_lift cap = Some (Cap_reply_cap \<lparr> capReplyMaster_CL = capReplyMaster___unsigned_long_' s,
capTCBPtr_CL = capTCBPtr___unsigned_long_' s \<rparr>)
\<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (ptr s)
(the (cslift s (ptr s)) \<lparr> cte_C.cap_C := cap \<rparr>))
(t_hrs_' (globals s))
)}"
apply (intro allI, rule conseqPre, vcg)
apply (clarsimp simp: ptr_def)
apply (clarsimp simp: h_t_valid_clift_Some_iff word_sle_def)
apply (frule h_t_valid_c_guard_cparent[OF h_t_valid_clift],
simp+, simp add: typ_uinfo_t_def)
apply (frule clift_subtype, simp+)
apply (clarsimp simp: typ_heap_simps')
apply (subst parent_update_child, erule typ_heap_simps', simp+)
apply (clarsimp simp: typ_heap_simps' word_sless_def word_sle_def)
apply (rule exI, rule conjI [OF _ refl])
apply (fold limited_and_def)
apply (simp add: cap_get_tag_def mask_def cap_tag_defs
word_ao_dist limited_and_simps
cap_lift_reply_cap shiftr_over_or_dist)
done
lemma endpoint_ptr_mset_epQueue_tail_state_spec:
"\<forall>s. \<Gamma>\<turnstile> \<lbrace>s. hrs_htd \<^bsup>s\<^esup>t_hrs \<Turnstile>\<^sub>t ep_ptr_' s \<and> is_aligned (epQueue_tail_' s) 4
\<and> state_' s && mask 2 = state_' s\<rbrace>
@ -1340,14 +1138,6 @@ lemma bind_case_sum_rethrow:
apply (simp add: throwError_bind split: sum.split)
done
lemma ccorres_alt_rdonly_liftE_bindE:
"\<lbrakk> ccorres_underlying sr Gamm r xf arrel axf A A' hs
(f >>= (\<lambda>x. alternative (g x) h)) c;
\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; empty_fail f \<rbrakk>
\<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf A A' hs
(alternative (liftE f >>=E (\<lambda>x. g x)) h) c"
by (simp add: liftE_bindE ccorres_alt_rdonly_bind)
lemma ccorres_pre_getCTE2:
"(\<And>rv. ccorresG rf_sr \<Gamma> r xf (P rv) (P' rv) hs (f rv) c) \<Longrightarrow>
ccorresG rf_sr \<Gamma> r xf (\<lambda>s. \<forall>cte. ctes_of s p = Some cte \<longrightarrow> P cte s)
@ -1483,20 +1273,6 @@ lemma isRecvEP_endpoint_case:
"isRecvEP ep \<Longrightarrow> case_endpoint f g h ep = f (epQueue ep)"
by (clarsimp simp: isRecvEP_def split: endpoint.split_asm)
lemma ccorres_cond_both_seq:
"\<lbrakk> \<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P s = (s' \<in> P');
ccorres_underlying sr \<Gamma> r xf arrel axf Pt Rt hs a (c ;; d);
ccorres_underlying sr \<Gamma> r xf arrel axf Pf Rf hs a (c' ;; d) \<rbrakk>
\<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf
(R and (\<lambda>s. P s \<longrightarrow> Pt s) and (\<lambda>s. \<not> P s \<longrightarrow> Pf s))
{s. (s \<in> P' \<longrightarrow> s \<in> Rt) \<and> (s \<notin> P' \<longrightarrow> s \<in> Rf)}
hs a (Cond P' c c' ;; d)"
apply (subst ccorres_seq_cond_raise)
apply (rule ccorres_guard_imp2, rule ccorres_cond_both, assumption+)
apply auto
done
lemma unifyFailure_catch_If:
"catch (unifyFailure f >>=E g) h
= f >>= (\<lambda>rv. if isRight rv then catch (g (theRight rv)) h else h ())"
@ -1599,11 +1375,6 @@ lemma fastpath_dequeue_ccorres:
apply (rule ext, simp add: tcb_null_ep_ptrs_def split: if_split)
done
lemma tcb_NextPrev_C_update_swap:
"tcbEPPrev_C_update f (tcbEPNext_C_update g tcb)
= tcbEPNext_C_update g (tcbEPPrev_C_update f tcb)"
by simp
lemma st_tcb_at_not_in_ep_queue:
"\<lbrakk> st_tcb_at' P t s; ko_at' ep epptr s; sym_refs (state_refs_of' s);
ep \<noteq> IdleEP; \<And>ts. P ts \<Longrightarrow> tcb_st_refs_of' ts = {} \<rbrakk>
@ -1633,20 +1404,6 @@ lemma cntfn_relation_double_fun_upd:
= cnotification_relation (mp(a := b, c := d)) ntfn ntfn'"
by simp
lemma sym_refs_upd_ko_atD':
"\<lbrakk> ko_at' ko p s; sym_refs ((state_refs_of' s) (p' := S)); p \<noteq> p' \<rbrakk>
\<Longrightarrow> \<forall>(x, tp) \<in> refs_of' (injectKO ko). (x = p' \<and> (p, symreftype tp) \<in> S)
\<or> (x \<noteq> p' \<and> ko_wp_at' (\<lambda>ko. (p, symreftype tp) \<in> refs_of' ko)x s)"
apply (clarsimp del: disjCI)
apply (drule ko_at_state_refs_ofD')
apply (drule_tac y=a and tp=b and x=p in sym_refsD[rotated])
apply simp
apply (case_tac "a = p'")
apply simp
apply simp
apply (erule state_refs_of'_elemD)
done
lemma sym_refs_upd_sD:
"\<lbrakk> sym_refs ((state_refs_of' s) (p := S)); valid_pspace' s;
ko_at' ko p s; refs_of' (injectKO koEx) = S;
@ -1827,44 +1584,6 @@ lemma fastpath_enqueue_ccorres:
apply (rule ext, simp add: tcb_null_ep_ptrs_def split: if_split)
done
lemma ccorres_updateCap [corres]:
fixes ptr :: "cstate \<Rightarrow> cte_C ptr" and val :: "cstate \<Rightarrow> cap_C"
shows "ccorres dc xfdc \<top>
({s. ccap_relation cap (val s)} \<inter> {s. ptr s = Ptr dest}) hs
(updateCap dest cap)
(Basic
(\<lambda>s. globals_update
(t_hrs_'_update
(hrs_mem_update (heap_update (Ptr &(ptr s\<rightarrow>[''cap_C''])) (val s)))) s))"
unfolding updateCap_def
apply (cinitlift ptr)
apply (erule ssubst)
apply (rule ccorres_guard_imp2)
apply (rule ccorres_pre_getCTE)
apply (rule_tac P = "\<lambda>s. ctes_of s dest = Some rva" in ccorres_from_vcg [where P' = "{s. ccap_relation cap (val s)}"])
apply (rule allI)
apply (rule conseqPre)
apply vcg
apply clarsimp
apply (rule fst_setCTE [OF ctes_of_cte_at], assumption)
apply (erule bexI [rotated])
apply (clarsimp simp: cte_wp_at_ctes_of)
apply (frule (1) rf_sr_ctes_of_clift)
apply (clarsimp simp add: rf_sr_def cstate_relation_def typ_heap_simps
Let_def cpspace_relation_def)
apply (rule conjI)
apply (erule (3) cpspace_cte_relation_upd_capI)
apply (erule_tac t = s' in ssubst)
apply (simp add: heap_to_user_data_def)
apply (rule conjI)
apply (erule (1) setCTE_tcb_case)
apply (simp add: carch_state_relation_def cmachine_state_relation_def
cvariable_array_map_const_add_map_option[where f="tcb_no_ctes_proj"]
typ_heap_simps h_t_valid_clift_Some_iff)
apply clarsimp
done
lemma setCTE_rf_sr:
"\<lbrakk> (\<sigma>, s) \<in> rf_sr; ctes_of \<sigma> ptr = Some cte'';
t_hrs_' (globals s') = hrs_mem_update
@ -1994,12 +1713,6 @@ shows
apply (simp add: length_msgRegisters n_msgRegisters_def word_bits_def hoare_TrueI)+
done
lemma switchToThread_ksCurThread:
"\<lbrace>\<lambda>s. P t\<rbrace> switchToThread t \<lbrace>\<lambda>rv s. P (ksCurThread s)\<rbrace>"
apply (simp add: switchToThread_def setCurThread_def)
apply (wp | simp)+
done
lemma updateCap_cte_wp_at_cteMDBNode:
"\<lbrace>cte_wp_at' (\<lambda>cte. P (cteMDBNode cte)) p\<rbrace>
updateCap ptr cap
@ -2103,18 +1816,6 @@ lemma option_case_liftM_getNotification_wp:
apply (auto simp: obj_at'_def)
done
lemma threadSet_st_tcb_at_state:
"\<lbrace>\<lambda>s. tcb_at' t s \<longrightarrow> (if p = t
then obj_at' (\<lambda>tcb. P (tcbState (f tcb))) t s
else st_tcb_at' P p s)\<rbrace>
threadSet f t \<lbrace>\<lambda>_. st_tcb_at' P p\<rbrace>"
apply (rule hoare_chain)
apply (rule threadSet_obj_at'_really_strongest)
prefer 2
apply (simp add: st_tcb_at'_def)
apply (clarsimp split: if_splits simp: st_tcb_at'_def o_def)
done
lemma fastpath_call_ccorres:
notes hoare_TrueI[simp]
shows "ccorres dc xfdc
@ -2647,7 +2348,7 @@ proof -
del: all_imp_to_ex)
apply (wp hoare_vcg_all_lift threadSet_ctes_of
hoare_vcg_imp_lift threadSet_valid_objs'
threadSet_st_tcb_at_state threadSet_cte_wp_at'
threadSet_cte_wp_at'
threadSet_cur
| simp add: cur_tcb'_def[symmetric])+
apply (vcg exspec=thread_state_ptr_set_tsType_np_modifies)
@ -2707,7 +2408,6 @@ proof -
apply (clarsimp simp: obj_at_tcbs_of ct_in_state'_def st_tcb_at_tcbs_of
invs_cur' invs_valid_objs' ctes_of_valid'
word_sle_def
tcb_ptr_to_ctcb_ptr_mask[OF tcb_at_invs']
invs'_bitmapQ_no_L1_orphans)
apply (frule cte_wp_at_valid_objs_valid_cap', clarsimp)
apply (clarsimp simp: isCap_simps valid_cap'_def maskCapRights_def)
@ -3253,7 +2953,7 @@ lemma fastpath_reply_recv_ccorres:
apply (rule conseqPre, vcg)
apply (clarsimp simp: typ_heap_simps' cte_level_bits_def
tcbCallerSlot_def size_of_def
tcb_cnode_index_defs tcb_ptr_to_ctcb_ptr_mask)
tcb_cnode_index_defs)
apply (clarsimp simp: ccte_relation_def map_option_Some_eq2)
apply ceqv
apply (rule ccorres_assert)
@ -3286,7 +2986,7 @@ lemma fastpath_reply_recv_ccorres:
apply (clarsimp simp: cte_wp_at_ctes_of)
apply (rule cmap_relationE1[OF cmap_relation_cte], assumption+)
apply (clarsimp simp: typ_heap_simps' split_def tcbCallerSlot_def
tcb_cnode_index_defs tcb_ptr_to_ctcb_ptr_mask
tcb_cnode_index_defs
cte_level_bits_def size_of_def
packed_heap_update_collapse_hrs)
apply (rule setCTE_rf_sr, simp_all add: typ_heap_simps')[1]
@ -3552,12 +3252,6 @@ lemma lookupBitmapPriority_lift:
apply wpsimp+
done
lemma lookupBitmapPriority_Max_strengthen:
"\<lbrakk> valid_bitmapQ s ; bitmapQ_no_L1_orphans s ; ksReadyQueuesL1Bitmap s d \<noteq> 0 ;
P (Max {prio. ksReadyQueues s (d, prio) \<noteq> []})\<rbrakk>
\<Longrightarrow> P (lookupBitmapPriority d s)"
by (clarsimp simp: lookupBitmapPriority_Max_eqI)
(* slow path additionally requires current thread not idle *)
definition
"fastpathBestSwitchCandidate t \<equiv> \<lambda>s.
@ -3661,18 +3355,6 @@ lemma resolveAddressBits_points_somewhere:
apply clarsimp
done
lemma user_getregs_wp:
"\<lbrace>\<lambda>s. tcb_at' t s \<and> (\<forall>tcb. ko_at' tcb t s \<longrightarrow> Q (map ((atcbContextGet o tcbArch) tcb) regs) s)\<rbrace>
asUser t (mapM getRegister regs) \<lbrace>Q\<rbrace>"
apply (rule hoare_strengthen_post)
apply (rule hoare_vcg_conj_lift)
apply (rule asUser_get_registers)
apply (rule asUser_inv)
apply (wp mapM_wp' getRegister_inv)
apply clarsimp
apply (drule obj_at_ko_at', clarsimp)
done
lemma foldr_copy_register_tsrs:
"foldr (\<lambda>r . copy_register_tsrs x y r r (\<lambda>x. x)) rs s
= (s (y := TCBStateRegs (tsrState (s y))
@ -3684,25 +3366,6 @@ lemma foldr_copy_register_tsrs:
split: if_split)
done
lemma monadic_rewrite_add_lookup_both_sides:
assumes inv: "\<And>P. \<lbrace>P\<rbrace> lu \<lbrace>\<lambda>r. P\<rbrace>"
and ef: "empty_fail lu"
and nf: "no_fail Q lu"
shows
"monadic_rewrite E F P (do lu; f od) (do lu; g od)
\<Longrightarrow> monadic_rewrite E F (P and Q) f g"
apply (rule monadic_rewrite_imp)
apply (rule monadic_rewrite_trans[rotated])
apply (rule monadic_rewrite_symb_exec_l'[where m=lu], (wp inv ef nf impI)+)
apply (rule monadic_rewrite_refl, wp)
apply (simp; erule monadic_rewrite_trans[rotated])
apply (rule monadic_rewrite_transverse[OF _ monadic_rewrite_refl])
apply (rule monadic_rewrite_symb_exec_l'[where m=lu], (wp inv ef nf impI)+)
apply (rule monadic_rewrite_refl, wp)
apply simp
done
lemmas cteInsert_obj_at'_not_queued = cteInsert_obj_at'_queued[of "\<lambda>a. \<not> a"]
lemma monadic_rewrite_exists_v:
@ -3715,22 +3378,6 @@ lemma monadic_rewrite_exists_v:
apply clarsimp
done
lemma monadic_rewrite_threadGet_tcbIPCBuffer:
"monadic_rewrite E F (obj_at' (%tcb. tcbIPCBuffer tcb = v) t)
(threadGet tcbIPCBuffer t) (return v)"
apply (rule monadic_rewrite_imp)
apply (rule monadic_rewrite_trans[rotated])
apply (rule monadic_rewrite_gets_known)
apply (unfold threadGet_def liftM_def fun_app_def)
apply (rule monadic_rewrite_symb_exec_l' | wp | rule empty_fail_getObject getObject_inv)+
apply (clarsimp; rule no_fail_getObject_tcb)
apply (simp only: exec_gets)
apply (rule_tac P = "(\<lambda>s. (tcbIPCBuffer x)=v) and tcb_at' t" in monadic_rewrite_refl3)
apply (simp add:)
apply (wp OMG_getObject_tcb | wpc)+
apply (auto intro: obj_tcb_at')
done
lemma setCTE_obj_at'_tcbIPCBuffer:
"\<lbrace>obj_at' (\<lambda>tcb. P (tcbIPCBuffer tcb)) t\<rbrace> setCTE p v \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P (tcbIPCBuffer tcb)) t\<rbrace>"
unfolding setCTE_def
@ -3752,23 +3399,6 @@ crunch ksReadyQueuesL1Bitmap_inv[wp]: setEndpoint "\<lambda>s. P (ksReadyQueuesL
crunch ksReadyQueuesL2Bitmap_inv[wp]: setEndpoint "\<lambda>s. P (ksReadyQueuesL2Bitmap s)"
(wp: setObject_ksPSpace_only updateObject_default_inv ignore: setObject)
lemma cteInsert_lookupBitmapPriority_inv:
"\<lbrace> \<lambda>s. P (lookupBitmapPriority t s) \<rbrace> cteInsert x y z \<lbrace>\<lambda>_ s. P (lookupBitmapPriority t s)\<rbrace>"
unfolding lookupBitmapPriority_def
apply (rule hoare_pre, wps)
apply (wp)
apply simp
done (* CLEANUP *)
lemma threadSet_lookupBitmapPriority_inv:
"\<lbrace> \<lambda>s. P (lookupBitmapPriority d s) \<rbrace> threadSet F t
\<lbrace>\<lambda>rv s. P (lookupBitmapPriority d s) \<rbrace>"
apply (simp add: lookupBitmapPriority_def)
apply (rule hoare_pre, wps)
apply (wp)
apply simp
done
lemma setThreadState_runnable_bitmap_inv:
"runnable' ts \<Longrightarrow>
\<lbrace> \<lambda>s. P (ksReadyQueuesL1Bitmap s) \<rbrace> setThreadState ts t \<lbrace>\<lambda>rv s. P (ksReadyQueuesL1Bitmap s) \<rbrace>"
@ -3955,7 +3585,6 @@ lemma fastpath_callKernel_SysCall_corres:
fastpathBestSwitchCandidate_lift[where f="setEndpoint a b" for a b]
lookupBitmapPriority_lift
setThreadState_runnable_bitmap_inv
threadSet_lookupBitmapPriority_inv
| simp add: setMessageInfo_def
| wp_once hoare_vcg_disj_lift)+)
@ -3969,11 +3598,11 @@ lemma fastpath_callKernel_SysCall_corres:
apply (simp add: ARM_H.switchToThread_def bind_assoc)
apply (rule monadic_rewrite_trans[OF _ monadic_rewrite_transverse])
apply (rule_tac v=ipcBuffer in monadic_rewrite_threadGet_tcbIPCBuffer | rule monadic_rewrite_bind monadic_rewrite_refl)+
apply (rule monadic_rewrite_bind monadic_rewrite_refl)+
apply (wp mapM_x_wp' getObject_inv | wpc | simp add:
| wp_once hoare_drop_imps )+
apply (rule_tac v=ipcBuffer in monadic_rewrite_threadGet_tcbIPCBuffer | rule monadic_rewrite_bind monadic_rewrite_refl)+
apply (rule monadic_rewrite_bind monadic_rewrite_refl)+
apply (wp mapM_x_wp' getObject_inv | wpc | simp add:
| wp_once hoare_drop_imps )+
@ -4026,7 +3655,7 @@ lemma fastpath_callKernel_SysCall_corres:
apply (simp cong: if_cong bool.case_cong)
apply wp
apply simp
apply (wp user_getreg_wp user_getregs_wp threadGet_wp)+
apply (wp user_getreg_wp threadGet_wp)+
apply clarsimp
apply (subgoal_tac "ksCurThread s \<noteq> ksIdleThread s")
@ -4092,47 +3721,10 @@ lemma capability_case_Null_ReplyCap:
else if isNullCap cap then f else h)"
by (simp add: isCap_simps split: capability.split)
lemma in_getCTE_slot:
"(\<exists>s. (rv, s) \<in> fst (getCTE slot s)) = (is_aligned slot cte_level_bits)"
apply (simp add: getCTE_assert_opt exec_gets assert_opt_member)
apply (rule iffI)
apply clarsimp
apply (subgoal_tac "cte_wp_at' ((=) rv) slot s")
apply (simp add: cte_wp_at_cases')
apply (erule disjE)
apply simp
apply clarsimp
apply (drule(1) tcb_cte_cases_aligned[where cte=rv])
apply (simp add: objBits_simps' cte_level_bits_def)
apply (simp add: cte_wp_at_ctes_of)
apply (rule_tac x="undefined \<lparr> ksPSpace := Map.empty (slot \<mapsto> KOCTE rv) \<rparr>" in exI)
apply (simp add: map_to_ctes_def Let_def objBits_simps' cte_level_bits_def)
done
end
context begin interpretation Arch . (*FIXME: arch_split*)
lemma inj2_assert_opt:
"(assert_opt v s = assert_opt v' s') = (v = v' \<and> (v' = None \<or> s = s'))"
by (simp add: assert_opt_def return_def fail_def split: option.split)
lemma gets_the_inj:
"inj gets_the"
apply (rule injI)
apply (clarsimp simp: gets_the_def fun_eq_iff exec_gets inj2_assert_opt)
done
lemmas gets_the_eq = inj_eq[OF gets_the_inj]
lemma gets_the_eq2:
"(gets_the f s = gets_the g s') = (f s = g s' \<and> (g s' = None \<or> s = s'))"
by (simp add: gets_the_def exec_gets inj2_assert_opt)
lemma return_gets_the:
"return x = gets_the (\<lambda>_. Some x)"
by (simp add: gets_the_def assert_opt_def)
lemma injection_handler_catch:
"catch (injection_handler f x) y
= catch x (y o f)"
@ -4272,20 +3864,6 @@ lemma emptySlot_cnode_caps:
split: if_split)
done
lemma cteDeleteOne_cnode_caps:
"\<lbrace>\<lambda>s. P (only_cnode_caps (ctes_of s))\<rbrace>
cteDeleteOne slot
\<lbrace>\<lambda>rv s. P (only_cnode_caps (ctes_of s))\<rbrace>"
apply (simp add: only_cnode_caps_def map_option_comp2
o_assoc[symmetric] cteCaps_of_def[symmetric])
apply (wp cteDeleteOne_cteCaps_of)
apply clarsimp
apply (erule rsubst[where P=P], rule ext)
apply (clarsimp simp: cteCaps_of_def cte_wp_at_ctes_of isCap_simps)
apply (rule_tac x="cteCap cte" in exI)
apply (clarsimp simp: finaliseCap_def finaliseCapTrue_standin_def isCap_simps)
done
lemma asUser_obj_at_ep[wp]:
"\<lbrace>obj_at' P p\<rbrace> asUser t m \<lbrace>\<lambda>rv. obj_at' (P :: endpoint \<Rightarrow> bool) p\<rbrace>"
apply (simp add: asUser_def split_def)
@ -4437,16 +4015,6 @@ lemma emptySlot_cte_wp_at_cteCap:
apply (clarsimp split: if_split)
done
lemma real_cte_at_tcbs_of_neq:
"[| real_cte_at' p s; tcbs_of s t = Some tcb;
2 ^ cte_level_bits * offs : dom tcb_cte_cases |]
==> p ~= t + 2 ^ cte_level_bits * offs"
apply (clarsimp simp: tcbs_of_def obj_at'_def projectKOs objBits_simps
split: if_split_asm)
apply (erule notE[rotated], erule(2) tcb_ctes_clear[rotated])
apply fastforce
done
lemma setEndpoint_getCTE_pivot[unfolded K_bind_def]:
"do setEndpoint p val; v <- getCTE slot; f v od
= do v <- getCTE slot; setEndpoint p val; f v od"
@ -4726,11 +4294,6 @@ lemmas cnode_caps_gsCNodes_lift
= hoare_lift_Pf2[where P="\<lambda>gs s. cnode_caps_gsCNodes (f s) gs" and f=gsCNodes for f]
hoare_lift_Pf2[where P="\<lambda>gs s. Q s \<longrightarrow> cnode_caps_gsCNodes (f s) gs" and f=gsCNodes for f Q]
lemma monadic_rewrite_option_cases:
"\<lbrakk> v = None \<Longrightarrow> monadic_rewrite F E Q a b; \<And>x. v = Some x \<Longrightarrow> monadic_rewrite F E (R x) a b \<rbrakk>
\<Longrightarrow> monadic_rewrite F E (\<lambda>s. (v = None \<longrightarrow> Q s) \<and> (\<forall>x. v = Some x \<longrightarrow> R x s)) a b"
by (cases v, simp_all)
lemma resolveAddressBitsFn_eq_name_slot:
"monadic_rewrite F E (\<lambda>s. (isCNodeCap cap \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = cap) (slot s) s)
\<and> valid_objs' s \<and> cnode_caps_gsCNodes' s)
@ -4910,11 +4473,11 @@ lemma fastpath_callKernel_SysReplyRecv_corres:
apply (simp add: ARM_H.switchToThread_def bind_assoc)
apply (rule monadic_rewrite_trans[OF _ monadic_rewrite_transverse])
apply (rule_tac v=ipcBuffer in monadic_rewrite_threadGet_tcbIPCBuffer | rule monadic_rewrite_bind monadic_rewrite_refl)+
apply (rule monadic_rewrite_bind monadic_rewrite_refl)+
apply (wp mapM_x_wp' getObject_inv | wpc | simp add:
| wp_once hoare_drop_imps )+
apply (rule_tac v=ipcBuffer in monadic_rewrite_threadGet_tcbIPCBuffer | rule monadic_rewrite_bind monadic_rewrite_refl)+
apply (rule monadic_rewrite_bind monadic_rewrite_refl)+
apply (wp setCTE_obj_at'_tcbIPCBuffer assert_inv mapM_x_wp' getObject_inv | wpc | simp
| wp_once hoare_drop_imps )+
@ -4935,9 +4498,8 @@ lemma fastpath_callKernel_SysReplyRecv_corres:
setThreadState_obj_at_unchanged
asUser_obj_at_unchanged
hoare_strengthen_post[OF _ obj_at_conj'[simplified atomize_conjL], rotated]
lookupBitmapPriority_lift
setThreadState_runnable_bitmap_inv
threadSet_lookupBitmapPriority_inv
lookupBitmapPriority_lift
setThreadState_runnable_bitmap_inv
| simp add: setMessageInfo_def setThreadState_runnable_simp
| wp_once hoare_vcg_disj_lift)+)[1]
apply (simp add: setMessageInfo_def)
@ -5052,10 +4614,10 @@ lemma fastpath_callKernel_SysReplyRecv_corres:
apply (simp add: ARM_H.switchToThread_def bind_assoc)
apply (rule monadic_rewrite_trans[OF _ monadic_rewrite_transverse])
apply (rule_tac v=ipcBuffer in monadic_rewrite_threadGet_tcbIPCBuffer | rule monadic_rewrite_bind monadic_rewrite_refl)+
apply (rule monadic_rewrite_bind monadic_rewrite_refl)+
apply (wp mapM_x_wp' handleFault_obj_at'_tcbIPCBuffer getObject_inv | wpc | simp
| wp_once hoare_drop_imps )+
apply (rule_tac v=ipcBuffer in monadic_rewrite_threadGet_tcbIPCBuffer | rule monadic_rewrite_bind monadic_rewrite_refl)+
apply (rule monadic_rewrite_bind monadic_rewrite_refl)+
apply (wp setCTE_obj_at'_tcbIPCBuffer assert_inv mapM_x_wp' getObject_inv | wpc | simp
| wp_once hoare_drop_imps )+
@ -5141,7 +4703,7 @@ lemma fastpath_callKernel_SysReplyRecv_corres:
apply (simp cong: if_cong bool.case_cong
| rule getCTE_wp' gts_wp' threadGet_wp
getEndpoint_wp gets_wp
user_getreg_wp user_getregs_wp
user_getreg_wp
gets_the_wp gct_wp getNotification_wp
return_wp liftM_wp gbn_wp'
| (simp only: curDomain_def, wp)[1])+

View File

@ -497,29 +497,6 @@ lemma cancelAllSignals_ccorres:
apply clarsimp
done
lemma tcb_queue_concat:
"tcb_queue_relation getNext getPrev mp (xs @ z # ys) qprev qhead
\<Longrightarrow> tcb_queue_relation getNext getPrev mp (z # ys)
(tcb_ptr_to_ctcb_ptr (last ((ctcb_ptr_to_tcb_ptr qprev) # xs))) (tcb_ptr_to_ctcb_ptr z)"
apply (induct xs arbitrary: qprev qhead)
apply clarsimp
apply clarsimp
apply (elim meta_allE, drule(1) meta_mp)
apply (clarsimp cong: if_cong)
done
lemma tcb_fields_ineq_helper:
"\<lbrakk> tcb_at' (ctcb_ptr_to_tcb_ptr x) s; tcb_at' (ctcb_ptr_to_tcb_ptr y) s \<rbrakk> \<Longrightarrow>
&(x\<rightarrow>[''tcbSchedPrev_C'']) \<noteq> &(y\<rightarrow>[''tcbSchedNext_C''])"
apply (clarsimp dest!: tcb_aligned'[OF obj_at'_weakenE, OF _ TrueI]
ctcb_ptr_to_tcb_ptr_aligned)
apply (clarsimp simp: field_lvalue_def ctcb_size_bits_def)
apply (subgoal_tac "is_aligned (ptr_val y - ptr_val x) 8")
apply (drule sym, fastforce simp: is_aligned_def dvd_def)
apply (erule(1) aligned_sub_aligned)
apply (simp add: word_bits_conv)
done
end
primrec
@ -559,17 +536,6 @@ lemma tcb_queue_relation2_concat:
apply simp
done
lemma tcb_queue_relation2_cong:
"\<lbrakk>queue = queue'; before = before'; after = after';
\<And>p. p \<in> set queue' \<Longrightarrow> mp p = mp' p\<rbrakk>
\<Longrightarrow> tcb_queue_relation2 getNext getPrev mp queue before after =
tcb_queue_relation2 getNext getPrev mp' queue' before' after'"
using [[hypsubst_thin = true]]
apply clarsimp
apply (induct queue' arbitrary: before')
apply simp+
done
context kernel_m begin
lemma setThreadState_ccorres_valid_queues'_simple:
@ -632,8 +598,6 @@ lemma cap_to_H_NTFNCap_tag:
apply (clarsimp simp: cap_to_H_def Let_def split: cap_CL.splits if_split_asm)
by (simp_all add: Let_def cap_lift_def split: if_splits)
lemmas ccorres_pre_getBoundNotification = ccorres_pre_threadGet [where f=tcbBoundNotification, folded getBoundNotification_def]
lemma option_to_ptr_not_NULL:
"option_to_ptr x \<noteq> NULL \<Longrightarrow> x \<noteq> None"
by (auto simp: option_to_ptr_def option_to_0_def split: option.splits)
@ -1265,42 +1229,6 @@ lemma deleteASID_ccorres:
plus_one_helper arg_cong[where f="\<lambda>x. 2 ^ x", OF meta_eq_to_obj_eq, OF asid_low_bits_def]
split: option.split_asm)
lemma setObject_ccorres_lemma:
fixes val :: "'a :: pspace_storable" shows
"\<lbrakk> \<And>s. \<Gamma> \<turnstile> (Q s) c {s'. (s \<lparr> ksPSpace := ksPSpace s (ptr \<mapsto> injectKO val) \<rparr>, s') \<in> rf_sr},{};
\<And>s s' val (val' :: 'a). \<lbrakk> ko_at' val' ptr s; (s, s') \<in> rf_sr \<rbrakk>
\<Longrightarrow> s' \<in> Q s;
\<And>val :: 'a. updateObject val = updateObject_default val;
\<And>val :: 'a. (1 :: word32) < 2 ^ objBits val;
\<And>(val :: 'a) (val' :: 'a). objBits val = objBits val';
\<Gamma> \<turnstile> Q' c UNIV \<rbrakk>
\<Longrightarrow> ccorres dc xfdc \<top> Q' hs
(setObject ptr val) c"
apply (rule ccorres_from_vcg_nofail)
apply (rule allI)
apply (case_tac "obj_at' (\<lambda>x :: 'a. True) ptr \<sigma>")
apply (rule_tac P'="Q \<sigma>" in conseqPre, rule conseqPost, assumption)
apply clarsimp
apply (rule bexI [OF _ setObject_eq], simp+)
apply (drule obj_at_ko_at')
apply clarsimp
apply clarsimp
apply (rule conseqPre, erule conseqPost)
apply clarsimp
apply (subgoal_tac "fst (setObject ptr val \<sigma>) = {}")
apply simp
apply (erule notE, erule_tac s=\<sigma> in empty_failD[rotated])
apply (simp add: setObject_def split_def)
apply (rule ccontr)
apply (clarsimp elim!: nonemptyE)
apply (frule use_valid [OF _ obj_at_setObject3[where P=\<top>]], simp_all)[1]
apply (simp add: typ_at_to_obj_at'[symmetric])
apply (frule(1) use_valid [OF _ setObject_typ_at'])
apply simp
apply simp
apply clarsimp
done
lemma findPDForASID_nonzero:
"\<lbrace>\<top>\<rbrace> findPDForASID asid \<lbrace>\<lambda>rv s. rv \<noteq> 0\<rbrace>,-"
apply (simp add: findPDForASID_def cong: option.case_cong)
@ -1421,16 +1349,6 @@ lemma unmapPageTable_ccorres:
apply (simp add: unat_shiftr_le_bound unat_eq_0 pdeBits_def)
done
lemma return_Null_ccorres:
"ccorres ccap_relation ret__struct_cap_C_'
\<top> UNIV (SKIP # hs)
(return NullCap) (\<acute>ret__struct_cap_C :== CALL cap_null_cap_new()
;; return_C ret__struct_cap_C_'_update ret__struct_cap_C_')"
apply (rule ccorres_from_vcg_throws)
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp add: ccap_relation_NullCap_iff return_def)
done
lemma no_0_pd_at'[elim!]:
"\<lbrakk> page_directory_at' 0 s; no_0_obj' s \<rbrakk> \<Longrightarrow> P"
apply (clarsimp simp: page_directory_at'_def)
@ -2042,8 +1960,6 @@ lemma irq_opt_relation_Some_ucast:
apply (clarsimp simp: word_le_nat_alt Kernel_C.maxIRQ_def)
done
lemmas upcast_ucast_id = Word_Lemmas.ucast_up_inj
lemma irq_opt_relation_Some_ucast':
"\<lbrakk> x && mask 10 = x; ucast x \<le> (scast Kernel_C.maxIRQ :: 10 word) \<or> x \<le> (scast Kernel_C.maxIRQ :: word32) \<rbrakk>
\<Longrightarrow> irq_opt_relation (Some (ucast x)) (ucast x)"

View File

@ -130,11 +130,6 @@ lemma ntfn_case_can_send:
else v)"
by (cases cap, simp_all add: isCap_simps)
lemma list_length_geq_helper[simp]:
"\<lbrakk>\<not> length args < 2\<rbrakk>
\<Longrightarrow> \<exists>y ys. args = y # ys"
by (frule length_ineq_not_Nil(3), simp, metis list.exhaust)
lemma decodeIRQHandlerInvocation_ccorres:
notes if_cong[cong]
shows
@ -288,11 +283,6 @@ lemma ucast_maxIRQ_le_eq:
apply simp
by (clarsimp simp: ucast_up_ucast is_up Kernel_C.maxIRQ_def)
lemma ucast_maxIRQ_le_eq':
"UCAST(10 \<rightarrow> 32) irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> irq \<le> maxIRQ"
apply (clarsimp simp: Kernel_C.maxIRQ_def maxIRQ_def)
by word_bitwise
lemma invokeIRQControl_expanded_ccorres:
"ccorres (\<lambda>_ r. r = scast EXCEPTION_NONE) (ret__unsigned_long_')
(invs' and cte_at' parent and (\<lambda>_. (ucast irq) \<le> (scast Kernel_C.maxIRQ :: machine_word)))
@ -317,7 +307,7 @@ lemma invokeIRQControl_expanded_ccorres:
apply (clarsimp simp: is_simple_cap'_def isCap_simps valid_cap_simps' capAligned_def
word_bits_def)
apply (rule conjI)
apply (fastforce simp: word_bits_def intro!: ucast_maxIRQ_le_eq ucast_maxIRQ_le_eq')
apply (fastforce simp: word_bits_def intro!: ucast_maxIRQ_le_eq)
apply (simp add: invs_mdb' invs_valid_objs' invs_pspace_aligned')
apply (rule conjI)
apply (clarsimp simp: maxIRQ_def Kernel_C.maxIRQ_def)
@ -374,14 +364,6 @@ lemma Arch_invokeIRQControl_ccorres:
apply (wpsimp simp: guard_is_UNIV_def)+
done
lemma unat_ucast_16_32:
"unat (ucast (x::(16 word))::32 signed word) = unat x"
apply (subst unat_ucast)
apply (rule Divides.mod_less, simp)
apply (rule less_le_trans[OF unat_lt2p])
apply simp
done
lemma isIRQActive_ccorres:
"ccorres (\<lambda>rv rv'. rv' = from_bool rv) ret__unsigned_long_'
(\<lambda>s. irq \<le> scast Kernel_C.maxIRQ) (UNIV \<inter> {s. irq_' s = ucast irq}) []
@ -459,26 +441,6 @@ lemma checkIRQ_ret_good:
apply (rule hoare_pre,wp)
by (clarsimp simp: Kernel_C.maxIRQ_def split: if_split)
lemma toEnum_of_ucast:
"len_of TYPE('b) \<le> len_of TYPE('a) \<Longrightarrow>
(toEnum (unat (b::('b :: len word))):: ('a :: len word)) = of_nat (unat b)"
apply (subst toEnum_of_nat)
apply (rule less_le_trans[OF unat_lt2p])
apply (simp add:power2_nat_le_eq_le)
apply simp
done
lemma unat_ucast_mask:
"len_of TYPE('b) \<le> len_of TYPE('a) \<Longrightarrow> (unat (ucast (a :: ('a :: len) word) :: ('b :: len) word)) = unat (a && mask (len_of TYPE('b)))"
apply (subst ucast_mask_drop[symmetric])
apply (rule le_refl)
apply (simp add:unat_ucast)
apply (subst nat_mod_eq')
apply (rule less_le_trans[OF word_unat_mask_lt le_refl])
apply (simp add: word_size)
apply simp
done
lemma Arch_decodeIRQControlInvocation_ccorres:
notes if_cong[cong]
shows

View File

@ -480,31 +480,12 @@ lemma invokeCNodeSaveCaller_ccorres:
(* *)
(************************************************************************)
lemma ccorres_basic_srnoop2:
"\<lbrakk> \<And>s. globals (g s) = globals s;
ccorres_underlying rf_sr Gamm r xf arrel axf G (g ` G') hs a c \<rbrakk>
\<Longrightarrow> ccorres_underlying rf_sr Gamm r xf arrel axf G G'
hs a (Basic g ;; c)"
apply (rule ccorres_guard_imp2)
apply (rule ccorres_symb_exec_r)
apply assumption
apply vcg
apply (rule conseqPre, vcg)
apply clarsimp
apply simp
done
lemma updateCapData_spec2:
"\<forall>cap preserve newData. \<Gamma> \<turnstile> \<lbrace> ccap_relation cap \<acute>cap \<and> preserve = to_bool (\<acute>preserve) \<and> newData = \<acute>newData\<rbrace>
Call updateCapData_'proc
\<lbrace> ccap_relation (updateCapData preserve newData cap) \<acute>ret__struct_cap_C \<rbrace>"
by (simp add: updateCapData_spec)
lemma mdbRevocable_CL_cte_to_H:
"(mdbRevocable_CL (cteMDBNode_CL clcte) = 0)
= (\<not> mdbRevocable (cteMDBNode (cte_to_H clcte)))"
by (simp add: cte_to_H_def mdb_node_to_H_def to_bool_def)
lemma ccorres_add_specific_return:
"ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs
(do v \<leftarrow> return val; f v od) c
@ -579,11 +560,6 @@ lemma ctes_of_valid_strengthen:
apply fastforce
done
(* FIXME move: *)
lemma hoare_vcg_imp_lift_R:
"\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. \<not> P rv s\<rbrace>, -; \<lbrace>Q'\<rbrace> f \<lbrace>Q\<rbrace>, - \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P' s \<or> Q' s\<rbrace> f \<lbrace>\<lambda>rv s. P rv s \<longrightarrow> Q rv s\<rbrace>, -"
by (auto simp add: valid_def validE_R_def validE_def split_def split: sum.splits)
lemma decodeCNodeInvocation_ccorres:
shows
"interpret_excaps extraCaps' = excaps_map extraCaps \<Longrightarrow>
@ -1415,7 +1391,7 @@ lemma decodeCNodeInvocation_ccorres:
numeral_eqs hasCancelSendRights_not_Null
ccap_relation_NullCap_iff[symmetric]
if_1_0_0 interpret_excaps_test_null
mdbRevocable_CL_cte_to_H false_def true_def
false_def true_def
| clarsimp simp: typ_heap_simps'
| frule length_ineq_not_Nil)+)
done
@ -1427,8 +1403,6 @@ context begin interpretation Arch . (*FIXME: arch_split*)
crunch valid_queues[wp]: insertNewCap "valid_queues"
(wp: crunch_wps)
lemmas setCTE_def3 = setCTE_def2[THEN eq_reflection]
lemma setCTE_sch_act_wf[wp]:
"\<lbrace> \<lambda>s. sch_act_wf (ksSchedulerAction s) s \<rbrace>
setCTE src cte
@ -1477,27 +1451,6 @@ end
context kernel_m begin
lemma wordFromMessageInfo_spec:
"\<forall>s. \<Gamma> \<turnstile> {s} Call wordFromMessageInfo_'proc
\<lbrace>\<acute>ret__unsigned_long = index (seL4_MessageInfo_C.words_C (mi_' s)) (unat 0)\<rbrace>"
apply (hoare_rule HoarePartial.ProcNoRec1)
apply vcg
apply (simp add: word_sless_def word_sle_def)
done
lemma seL4_MessageInfo_lift_def2:
"seL4_MessageInfo_lift message_info \<equiv>
\<lparr>label_CL = (index (seL4_MessageInfo_C.words_C message_info) 0 >> 12) && mask 20,
capsUnwrapped_CL = (index (seL4_MessageInfo_C.words_C message_info) 0 >> 9) && mask 3,
extraCaps_CL = (index (seL4_MessageInfo_C.words_C message_info) 0 >> 7) && mask 2,
length_CL = (index (seL4_MessageInfo_C.words_C message_info) 0 >> 0) && mask 7\<rparr>"
apply (simp add: seL4_MessageInfo_lift_def mask_def)
done
lemma globals_update_id:
"globals_update (t_hrs_'_update (hrs_htd_update id)) x = x"
by (simp add:id_def hrs_htd_update_def)
lemma getObjectSize_spec:
"\<forall>s. \<Gamma>\<turnstile>\<lbrace>s. \<acute>t \<le> of_nat (length (enum::object_type list) - 1)\<rbrace> Call getObjectSize_'proc
\<lbrace>\<acute>ret__unsigned_long = of_nat (getObjectSize (object_type_to_H (t_' s)) (unat (userObjSize_' s)))\<rbrace>"
@ -1517,13 +1470,6 @@ lemma object_type_from_H_bound:
Kernel_C_defs split:apiobject_type.splits)+
done
lemma updateCap_ct_active'[wp]:
"\<lbrace>ct_active'\<rbrace> updateCap srcSlot cap \<lbrace>\<lambda>rva. ct_active' \<rbrace>"
apply (rule hoare_pre)
apply (simp add:ct_in_state'_def)
apply (wps|wp|simp add:ct_in_state'_def)+
done
lemma APIType_capBits_low:
"\<lbrakk> newType = APIObjectType apiobject_type.CapTableObject \<longrightarrow> 0 < us;
newType = APIObjectType apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits\<rbrakk>
@ -1533,113 +1479,6 @@ lemma APIType_capBits_low:
split: apiobject_type.splits)+
done
lemma APIType_capBits_high:
"\<lbrakk> newType = APIObjectType apiobject_type.CapTableObject \<longrightarrow> us < 28;
newType = APIObjectType apiobject_type.Untyped \<longrightarrow> us \<le> 29\<rbrakk>
\<Longrightarrow> APIType_capBits newType us < 32"
apply (case_tac newType)
apply (clarsimp simp:invokeUntyped_proofs_def APIType_capBits_def objBits_simps'
split: apiobject_type.splits)+
done
lemma typ_clear_region_eq:
notes blah[simp del] = atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
Int_atLeastAtMost atLeastatMost_empty_iff
shows
"\<lbrakk>ctes_of (s::kernel_state) (ptr_val p) = Some cte; is_aligned ptr bits; bits < word_bits;
{ptr..ptr + 2 ^ bits - 1} \<inter> {ptr_val p..ptr_val p + mask cteSizeBits} = {}; ((clift hp) :: (cte_C ptr \<rightharpoonup> cte_C)) p = Some to\<rbrakk> \<Longrightarrow>
(clift (hrs_htd_update (typ_clear_region ptr bits) hp) :: (cte_C ptr \<rightharpoonup> cte_C)) p = Some to"
apply (clarsimp simp:lift_t_def lift_typ_heap_def Fun.comp_def restrict_map_def split:if_splits)
apply (intro conjI impI)
apply (case_tac hp)
apply (clarsimp simp:typ_clear_region_def hrs_htd_update_def)
apply (rule arg_cong[where f = from_bytes])
apply (clarsimp simp:heap_list_s_def lift_state_def proj_h_def)
apply (case_tac hp)
apply (clarsimp simp:typ_clear_region_def hrs_htd_update_def)
apply (clarsimp simp:heap_list_s_def lift_state_def proj_h_def)
apply (clarsimp simp:s_valid_def h_t_valid_def)
apply (clarsimp simp:valid_footprint_def Let_def)
apply (drule spec)
apply (erule(1) impE)
apply clarsimp
apply (rule conjI)
apply (clarsimp simp add:map_le_def)
apply (drule_tac x = aa in bspec)
apply simp
apply (clarsimp simp:proj_d_def)
apply (clarsimp simp:hrs_htd_update_def typ_clear_region_def
split:if_splits option.splits)
apply (simp add:intvl_range_conv[where 'a=machine_word_len, folded word_bits_def])
apply (subgoal_tac "ptr_val p + of_nat y \<in> {ptr_val p..ptr_val p + mask cteSizeBits}")
apply blast
apply (clarsimp simp:blah)
apply (rule context_conjI)
apply (rule is_aligned_no_wrap')
apply (rule ctes_of_is_aligned[where cte = cte and s = s])
apply simp
apply (rule of_nat_power; simp add: objBits_simps')
apply (rule word_plus_mono_right)
apply (simp add: word_of_nat_le objBits_defs mask_def)
apply (rule is_aligned_no_wrap')
apply (rule ctes_of_is_aligned[where cte = cte and s = s])
apply simp
apply (clarsimp simp: objBits_simps' mask_def)
apply (clarsimp simp: proj_d_def)
done
lemma cte_size_inter_empty:
notes blah[simp del] = atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
Int_atLeastAtMost atLeastatMost_empty_iff
shows "\<lbrakk>invs' s;ctes_of s p = Some cte;isUntypedCap (cteCap cte);p\<notin> capRange (cteCap cte) \<rbrakk>
\<Longrightarrow> {p .. p + mask cteSizeBits} \<inter> capRange (cteCap cte) = {}"
apply (frule ctes_of_valid')
apply fastforce
apply (clarsimp simp:isCap_simps valid_cap'_def valid_untyped'_def)
apply (frule ctes_of_ko_at_strong)
apply (erule is_aligned_weaken[OF ctes_of_is_aligned])
apply (simp add:objBits_simps)
apply clarsimp
apply (drule_tac x = ptr in spec)
apply (clarsimp simp:ko_wp_at'_def)
apply (erule impE)
apply (erule pspace_alignedD',fastforce)
apply (frule pspace_distinctD')
apply fastforce
apply (clarsimp simp:capAligned_def)
apply (drule_tac p = v0 and p' = ptr in aligned_ranges_subset_or_disjoint)
apply (erule pspace_alignedD',fastforce)
apply (subst (asm) intvl_range_conv[where bits = cteSizeBits])
apply (erule is_aligned_weaken[OF ctes_of_is_aligned])
apply (simp add: objBits_simps)
apply (simp add: word_bits_def objBits_defs)
apply (erule disjE)
apply (simp add: obj_range'_def field_simps objBits_defs mask_def)
apply blast
apply (subgoal_tac "p \<in> {p .. p + mask cteSizeBits}")
prefer 2
apply (clarsimp simp:blah)
apply (rule is_aligned_no_wrap'[where sz=cteSizeBits])
apply (erule is_aligned_weaken[OF ctes_of_is_aligned])
by (auto simp: obj_range'_def field_simps objBits_simps' mask_def)
lemma region_is_typelessI:
"\<lbrakk>hrs_htd (t_hrs_' (globals t)) = hrs_htd (hrs_htd_update (typ_clear_region ptr sz) h) \<rbrakk>
\<Longrightarrow> region_is_typeless ptr (2^sz) t"
apply (case_tac h)
apply (clarsimp simp: typ_clear_region_def region_is_typeless_def
hrs_htd_def hrs_htd_update_def split:if_splits)
done
lemma rf_sr_cpspace_relation:
"(s,s') \<in> rf_sr \<Longrightarrow> cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) (t_hrs_' (globals s'))"
by (clarsimp simp:rf_sr_def cstate_relation_def Let_def)
lemma rf_sr_htd_safe_kernel_data_refs:
"(s, s') \<in> rf_sr \<Longrightarrow> htd_safe (- kernel_data_refs) (hrs_htd (t_hrs_' (globals s')))"
by (clarsimp simp: rf_sr_def cstate_relation_def Let_def
kernel_data_refs_domain_eq_rotate)
lemma cNodeNoOverlap_retype_have_size:
"\<not> cNodeOverlap cns (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + of_nat num * 2 ^ bits - 1)
\<Longrightarrow> cnodes_retype_have_size {ptr .. ptr + of_nat num * 2 ^ bits - 1} anysz cns"
@ -2278,7 +2117,6 @@ lemma resetUntypedCap_ccorres:
apply (strengthen is_aligned_no_overflow'
typ_region_bytes_dom_s
aligned_intvl_offset_subset
region_is_bytes_typ_region_bytes
intvl_start_le is_aligned_power2
heap_list_is_zero_mono[OF heap_list_update_eq]
byte_regions_unmodified_actually_heap_list[OF _ _ refl, mk_strg I E]
@ -2636,16 +2474,6 @@ lemma invokeUntyped_Retype_ccorres:
done
qed
lemma ccorres_returnOk_Basic:
"\<lbrakk> \<And>\<sigma> s. (\<sigma>, s) \<in> sr \<Longrightarrow> r (Inr v) (xf (f s))
\<and> (\<sigma>, f s) \<in> sr \<rbrakk> \<Longrightarrow>
ccorres_underlying sr \<Gamma> r xf arrel axf \<top> UNIV hs
(returnOk v) (Basic f)"
apply (rule ccorres_from_vcg)
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: returnOk_def return_def)
done
lemma injection_handler_whenE:
"injection_handler injf (whenE P f)
= whenE P (injection_handler injf f)"
@ -2672,12 +2500,6 @@ lemma injection_handler_sequenceE:
Let_def)
done
lemma getSlotCap_capAligned[wp]:
"\<lbrace>valid_objs'\<rbrace> getSlotCap ptr \<lbrace>\<lambda>rv s. capAligned rv\<rbrace>"
apply (rule hoare_strengthen_post, rule getSlotCap_valid_cap)
apply (clarsimp simp: valid_capAligned)
done
lemma ccorres_throwError_inl_rrel:
"ccorres_underlying sr Gamm (inl_rrel r) xf arrel axf hs P P'
(throwError v) c
@ -2714,16 +2536,6 @@ lemma mapME_ensureEmptySlot':
apply clarsimp
done
lemma mapME_ensureEmptySlot:
"\<lbrace>\<top>\<rbrace>
mapME (\<lambda>x. injection_handler Inl (ensureEmptySlot (f x))) [S .e. (E::word32)]
\<lbrace>\<lambda>rva s. \<forall>slot. S \<le> slot \<and> slot \<le> E \<longrightarrow>
(\<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f slot) = Some cte)\<rbrace>, -"
apply (rule hoare_post_imp_R)
apply (rule mapME_ensureEmptySlot')
apply clarsimp
done
lemma capCNodeRadix_CL_less_32:
"cap_get_tag ccap = scast cap_cnode_cap \<Longrightarrow> capCNodeRadix_CL (cap_cnode_cap_lift ccap) < 32"
apply (simp add: cap_cnode_cap_lift_def cap_lift_cnode_cap)
@ -2815,13 +2627,6 @@ lemma valid_untyped_capBlockSize_misc:
apply simp
done
lemma alternative_distrib:
"(do r\<leftarrow>c; (a \<sqinter> b) od) = ((do c; a od) \<sqinter> (do c ; b od))"
apply (rule ext)+
apply (clarsimp simp:alternative_def bind_def split_def)
apply force
done
lemma setThreadStateRestart_ct_active':
"\<lbrace>ct_active'\<rbrace> setThreadState Restart thread
\<lbrace>\<lambda>rva s. ct_active' s\<rbrace>"
@ -2850,14 +2655,6 @@ lemma unat_of_nat_APIType_capBits:
split: apiobject_type.splits)+
done
lemma valid_untyped_inv'_D:
"valid_untyped_inv' (Retype cref reset ptr_base ptr ty us destSlots isdev) s
\<Longrightarrow> APIType_capBits ty us < 32"
apply clarsimp
apply (drule range_cover_sz')
apply (simp add:word_bits_def)
done
lemma object_type_from_to_H:
"unat v \<le> (fromEnum::object_type \<Rightarrow> nat) maxBound
\<Longrightarrow> v = object_type_from_H (object_type_to_H v)"
@ -3290,8 +3087,7 @@ shows
getFreeRef_def hd_conv_nth length_ineq_not_Nil)
apply (rule_tac conseqPost[where A' = "{}" and Q' = UNIV])
apply (vcg exspec=setThreadState_modifies)
apply (clarsimp simp: object_type_from_to_H cap_get_tag_isCap
ccap_relation_isDeviceCap)
apply (clarsimp simp: object_type_from_to_H cap_get_tag_isCap)
apply (frule_tac cap = rv in cap_get_tag_to_H(5))
apply (simp add: cap_get_tag_isCap)
apply (simp add: field_simps Suc_unat_diff_1)
@ -3402,7 +3198,6 @@ shows
\<and> sch_act_simple s \<and> ct_active' s" in hoare_post_imp_R)
apply clarsimp
apply (wp injection_wp_E[OF refl] getSlotCap_cap_to'
getSlotCap_capAligned
| wp_once hoare_drop_imps)+
apply (clarsimp simp: valid_capAligned isCap_simps)
apply (drule_tac x=0 in bspec, simp+)

View File

@ -49,34 +49,6 @@ lemma cready_queues_index_to_C_distinct:
apply (auto simp: cready_queues_index_to_C_inj)
done
lemma cstate_relation_ksReadyQueues_update:
"\<lbrakk> cstate_relation hs cs; arr = ksReadyQueues_' cs;
sched_queue_relation' (clift (t_hrs_' cs)) v (head_C v') (end_C v');
qdom \<le> ucast maxDom; prio \<le> ucast maxPrio \<rbrakk>
\<Longrightarrow> cstate_relation (ksReadyQueues_update (\<lambda>qs. qs ((qdom, prio) := v)) hs)
(ksReadyQueues_'_update (\<lambda>_. Arrays.update arr
(cready_queues_index_to_C qdom prio) v') cs)"
apply (clarsimp simp: cstate_relation_def Let_def
cmachine_state_relation_def
carch_state_relation_def carch_globals_def
cready_queues_relation_def seL4_MinPrio_def minDom_def)
apply (frule cready_queues_index_to_C_in_range, assumption)
apply clarsimp
apply (frule_tac qdom=qdoma and prio=prioa in cready_queues_index_to_C_in_range, assumption)
apply (frule cready_queues_index_to_C_distinct, assumption+)
apply clarsimp
done
lemma cmap_relation_drop_fun_upd:
"\<lbrakk> cm x = Some v; \<And>v''. rel v'' v = rel v'' v' \<rbrakk>
\<Longrightarrow> cmap_relation am (cm (x \<mapsto> v')) f rel
= cmap_relation am cm f rel"
apply (simp add: cmap_relation_def)
apply (rule conj_cong[OF refl])
apply (rule ball_cong[OF refl])
apply (auto split: if_split)
done
lemma valid_queuesD':
"\<lbrakk> obj_at' (inQ d p) t s; valid_queues' s \<rbrakk>
\<Longrightarrow> t \<in> set (ksReadyQueues s (d, p))"
@ -362,48 +334,6 @@ lemma threadGet_vcg_corres_P:
lemmas threadGet_vcg_corres = threadGet_vcg_corres_P[where P=\<top>]
lemma threadGet_specs_corres:
assumes spec: "\<forall>s. \<Gamma> \<turnstile> {s} Call g {t. xf t = f' s}"
and mod: "modifies_spec g"
and xf: "\<And>f s. xf (globals_update f s) = xf s"
shows "ccorres r xf (ko_at' ko thread) {s'. r (f ko) (f' s')} hs (threadGet f thread) (Call g)"
apply (rule ccorres_Call_call_for_vcg)
apply (rule ccorres_guard_imp2)
apply (rule ccorres_add_return2)
apply (rule ccorres_pre_threadGet)
apply (rule_tac P = "\<lambda>s. ko_at' ko thread s \<and> x = f ko" in ccorres_from_vcg [where P' = "{s'. r (f ko) (f' s')}"])
apply (rule allI)
apply (rule HoarePartial.ProcModifyReturnNoAbr [where return' = "\<lambda>s t. t\<lparr> globals := globals s \<rparr>"])
apply (rule HoarePartial.ProcSpecNoAbrupt [OF _ _ spec])
defer
apply vcg
prefer 2
apply (rule mod)
apply (clarsimp simp: mex_def meq_def)
apply (frule obj_at'_weakenE [OF _ TrueI])
apply clarsimp
apply (drule (1) ko_at_obj_congD')
apply simp
apply (clarsimp simp: return_def)
apply (rule conjI)
apply (erule iffD1 [OF rf_sr_upd, rotated -1], simp_all)[1]
apply (simp add: xf)
done
lemma ccorres_exI1:
assumes rl: "\<And>x. ccorres r xf (Q x) (P' x) hs a c"
shows "ccorres r xf (\<lambda>s. (\<exists>x. P x s) \<and> (\<forall>x. P x s \<longrightarrow> Q x s))
{s'. \<forall>x s. (s, s') \<in> rf_sr \<and> P x s \<longrightarrow> s' \<in> P' x} hs a c"
apply (rule ccorresI')
apply clarsimp
apply (drule spec, drule (1) mp)
apply (rule ccorresE [OF rl], assumption+)
apply fastforce
apply assumption
apply assumption
apply fastforce
done
lemma isBlocked_ccorres [corres]:
"ccorres (\<lambda>r r'. r = to_bool r') ret__unsigned_long_'
(tcb_at' thread) (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr thread}) []
@ -578,24 +508,6 @@ lemma valid_queues_valid_q:
apply simp
done
lemma invs_valid_q:
"invs' s \<Longrightarrow> (\<forall>tcb\<in>set (ksReadyQueues s (qdom, prio)). tcb_at' tcb s) \<and> distinct (ksReadyQueues s (qdom, prio))"
apply (rule valid_queues_valid_q)
apply (clarsimp simp: invs'_def valid_state'_def)
done
lemma tcbQueued_not_in_queues:
assumes vq: "valid_queues s"
and objat: "obj_at' (Not \<circ> tcbQueued) thread s"
shows "thread \<notin> set (ksReadyQueues s (d, p))"
using vq objat
apply -
apply clarsimp
apply (drule (1) valid_queues_obj_at'D)
apply (erule obj_atE')+
apply (clarsimp simp: inQ_def)
done
declare unat_ucast_8_32[simp]
lemma rf_sr_sched_queue_relation:
@ -609,33 +521,6 @@ lemma rf_sr_sched_queue_relation:
apply (clarsimp simp: Let_def seL4_MinPrio_def minDom_def)
done
lemma ready_queue_not_in:
assumes vq: "valid_queues s"
and inq: "t \<in> set (ksReadyQueues s (d, p))"
and neq: "d \<noteq> d' \<or> p \<noteq> p'"
shows "t \<notin> set (ksReadyQueues s (d', p'))"
proof
assume "t \<in> set (ksReadyQueues s (d', p'))"
hence "obj_at' (inQ d' p') t s" using vq by (rule valid_queues_obj_at'D)
moreover have "obj_at' (inQ d p) t s" using inq vq by (rule valid_queues_obj_at'D)
ultimately show False using neq
by (clarsimp elim!: obj_atE' simp: inQ_def)
qed
lemma ctcb_relation_unat_prio_eq:
"ctcb_relation tcb tcb' \<Longrightarrow> unat (tcbPriority tcb) = unat (tcbPriority_C tcb')"
apply (clarsimp simp: ctcb_relation_def)
apply (erule_tac t = "tcbPriority_C tcb'" in subst)
apply simp
done
lemma ctcb_relation_unat_dom_eq:
"ctcb_relation tcb tcb' \<Longrightarrow> unat (tcbDomain tcb) = unat (tcbDomain_C tcb')"
apply (clarsimp simp: ctcb_relation_def)
apply (erule_tac t = "tcbDomain_C tcb'" in subst)
apply simp
done
lemma threadSet_queued_ccorres [corres]:
shows "ccorres dc xfdc (tcb_at' thread)
{s. v32_' s = from_bool v \<and> thread_state_ptr_' s = Ptr &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])} []
@ -805,24 +690,6 @@ lemma from_bool_vals [simp]:
"scast true \<noteq> scast false"
by (auto simp add: from_bool_def true_def false_def)
(* FIXME: move *)
lemma cmap_relation_no_upd:
"\<lbrakk> cmap_relation a c f rel; a p = Some ko; rel ko v; inj f \<rbrakk> \<Longrightarrow> cmap_relation a (c(f p \<mapsto> v)) f rel"
apply (clarsimp simp: cmap_relation_def)
apply (subgoal_tac "f p \<in> dom c")
prefer 2
apply (drule_tac t="dom c" in sym)
apply fastforce
apply clarsimp
apply (drule (1) injD)
apply simp
done
(* FIXME: move *)
lemma cmap_relation_rel_upd:
"\<lbrakk> cmap_relation a c f rel; \<And>v v'. rel v v' \<Longrightarrow> rel' v v' \<rbrakk> \<Longrightarrow> cmap_relation a c f rel'"
by (simp add: cmap_relation_def)
declare fun_upd_restrict_conv[simp del]
lemmas queue_in_range = of_nat_mono_maybe[OF _ cready_queues_index_to_C_in_range,
@ -870,22 +737,6 @@ lemma invert_l1index_spec:
by vcg
(simp add: word_sle_def sdiv_int_def sdiv_word_def smod_word_def smod_int_def)
lemma cbitmap_L1_relation_update:
"\<lbrakk> (\<sigma>, s) \<in> rf_sr ; cbitmap_L1_relation cupd aupd \<rbrakk>
\<Longrightarrow> (\<sigma>\<lparr>ksReadyQueuesL1Bitmap := aupd \<rparr>,
globals_update (ksReadyQueuesL1Bitmap_'_update (\<lambda>_. cupd)) s)
\<in> rf_sr"
by (simp add: rf_sr_def cstate_relation_def Let_def carch_state_relation_def
cmachine_state_relation_def)
lemma cbitmap_L2_relation_update:
"\<lbrakk> (\<sigma>, s) \<in> rf_sr ; cbitmap_L2_relation cupd aupd \<rbrakk>
\<Longrightarrow> (\<sigma>\<lparr>ksReadyQueuesL2Bitmap := aupd \<rparr>,
globals_update (ksReadyQueuesL2Bitmap_'_update (\<lambda>_. cupd)) s)
\<in> rf_sr"
by (simp add: rf_sr_def cstate_relation_def Let_def carch_state_relation_def
cmachine_state_relation_def)
lemma unat_ucast_prio_shiftr_simp[simp]:
"unat (ucast (p::priority) >> n :: machine_word) = unat (p >> n)"
by (simp add: shiftr_div_2n')+
@ -1001,39 +852,6 @@ lemma cbitmap_L2_relation_bit_set:
apply (case_tac "da = d" ; clarsimp)
done
lemma carch_state_relation_enqueue_simp:
"carch_state_relation (ksArchState \<sigma>)
(t_hrs_'_update f
(globals \<sigma>' \<lparr>ksReadyQueuesL1Bitmap_' := l1upd, ksReadyQueuesL2Bitmap_' := l2upd \<rparr>)
\<lparr>ksReadyQueues_' := rqupd \<rparr>) =
carch_state_relation (ksArchState \<sigma>) (t_hrs_'_update f (globals \<sigma>'))"
unfolding carch_state_relation_def
by clarsimp
(* FIXME move to lib/Eisbach_Methods *)
(* FIXME consider printing error on solve goal apply *)
context
begin
private definition "bool_protect (b::bool) \<equiv> b"
lemma bool_protectD:
"bool_protect P \<Longrightarrow> P"
unfolding bool_protect_def by simp
lemma bool_protectI:
"P \<Longrightarrow> bool_protect P"
unfolding bool_protect_def by simp
(*
When you want to apply a rule/tactic to transform a potentially complex goal into another
one manually, but want to indicate that any fresh emerging goals are solved by a more
brutal method.
E.g. apply (solves_emerging \<open>frule x=... in my_rule\<close>\<open>fastforce simp: ... intro!: ... \<close> *)
method solves_emerging methods m1 m2 = (rule bool_protectD, (m1 ; (rule bool_protectI | (m2; fail))))
end
lemma t_hrs_ksReadyQueues_upd_absorb:
"t_hrs_'_update f (g s) \<lparr>ksReadyQueues_' := rqupd \<rparr> =
t_hrs_'_update f (g s \<lparr>ksReadyQueues_' := rqupd\<rparr>)"
@ -1058,15 +876,6 @@ lemma rf_sr_drop_bitmaps_enqueue_helper:
carch_state_relation_def cmachine_state_relation_def
by (clarsimp simp: rf_sr_cbitmap_L1_relation rf_sr_cbitmap_L2_relation)
lemma cmachine_state_relation_enqueue_simp:
"cmachine_state_relation (ksMachineState \<sigma>)
(t_hrs_'_update f
(globals \<sigma>' \<lparr>ksReadyQueuesL1Bitmap_' := l1upd, ksReadyQueuesL2Bitmap_' := l2upd \<rparr>)
\<lparr>ksReadyQueues_' := rqupd \<rparr>) =
cmachine_state_relation (ksMachineState \<sigma>) (t_hrs_'_update f (globals \<sigma>'))"
unfolding cmachine_state_relation_def
by clarsimp
lemma tcb_queue_relation'_empty_ksReadyQueues:
"\<lbrakk> sched_queue_relation' (cslift x) (q s) NULL NULL ; \<forall>t\<in> set (q s). tcb_at' t s \<rbrakk> \<Longrightarrow> q s = []"
apply (clarsimp simp add: tcb_queue_relation'_def)
@ -1413,11 +1222,6 @@ lemma filter_noteq_op:
"[x \<leftarrow> xs . x \<noteq> y] = filter ((\<noteq>) y) xs"
by (induct xs) auto
(* FIXME move *)
lemma all_filter_propI:
"\<forall>x\<in>set lst. P x \<Longrightarrow> \<forall>x\<in>set (filter Q lst). P x"
by (induct lst, auto)
lemma cbitmap_L2_relation_bit_clear:
fixes p :: priority
fixes d :: domain
@ -2003,16 +1807,6 @@ lemma true_eq_from_bool [simp]:
"(scast true = from_bool P) = P"
by (simp add: true_def from_bool_def split: bool.splits)
lemma isBlocked_spec:
"\<forall>s. \<Gamma> \<turnstile> ({s} \<inter> {s. cslift s (thread_' s) \<noteq> None}) Call isBlocked_'proc
{s'. ret__unsigned_long_' s' = from_bool (tsType_CL (thread_state_lift (tcbState_C (the (cslift s (thread_' s))))) \<in>
{scast ThreadState_BlockedOnReply,
scast ThreadState_BlockedOnNotification, scast ThreadState_BlockedOnSend,
scast ThreadState_BlockedOnReceive, scast ThreadState_Inactive}) }"
apply vcg
apply (clarsimp simp: typ_heap_simps)
done
lemma isRunnable_spec:
"\<forall>s. \<Gamma> \<turnstile> ({s} \<inter> {s. cslift s (thread_' s) \<noteq> None}) Call isRunnable_'proc
{s'. ret__unsigned_long_' s' = from_bool (tsType_CL (thread_state_lift (tcbState_C (the (cslift s (thread_' s))))) \<in>
@ -2155,48 +1949,18 @@ lemma rf_sr_ksReadyQueuesL1Bitmap_simp:
apply (simp add: cbitmap_L1_relation_def)
done
lemma cguard_UNIV:
"P s \<Longrightarrow> s \<in> (if P s then UNIV else {})"
by fastforce
lemma lookupBitmapPriority_le_maxPriority:
"\<lbrakk> ksReadyQueuesL1Bitmap s d \<noteq> 0 ; valid_queues s \<rbrakk>
\<Longrightarrow> lookupBitmapPriority d s \<le> maxPriority"
unfolding valid_queues_def valid_queues_no_bitmap_def
by (fastforce dest!: bitmapQ_from_bitmap_lookup bitmapQ_ksReadyQueuesI intro: ccontr)
lemma rf_sr_ksReadyQueuesL1Bitmap_not_zero:
"\<lbrakk> (\<sigma>, s') \<in> rf_sr ; d \<le> maxDomain ; ksReadyQueuesL1Bitmap_' (globals s').[unat d] \<noteq> 0 \<rbrakk>
\<Longrightarrow> ksReadyQueuesL1Bitmap \<sigma> d \<noteq> 0"
apply (drule rf_sr_cbitmap_L1_relation)
apply (simp add: cbitmap_L1_relation_def)
done
lemma ksReadyQueuesL1Bitmap_word_log2_max:
"\<lbrakk>valid_queues s; ksReadyQueuesL1Bitmap s d \<noteq> 0\<rbrakk>
\<Longrightarrow> word_log2 (ksReadyQueuesL1Bitmap s d) < l2BitmapSize"
unfolding valid_queues_def
by (fastforce dest: word_log2_nth_same bitmapQ_no_L1_orphansD)
lemma rf_sr_ksReadyQueuesL2Bitmap_simp:
"\<lbrakk> (\<sigma>, s') \<in> rf_sr ; d \<le> maxDomain ; valid_queues \<sigma> ; ksReadyQueuesL1Bitmap \<sigma> d \<noteq> 0 \<rbrakk>
\<Longrightarrow> ksReadyQueuesL2Bitmap_' (globals s').[unat d].[word_log2 (ksReadyQueuesL1Bitmap \<sigma> d)] =
ksReadyQueuesL2Bitmap \<sigma> (d, word_log2 (ksReadyQueuesL1Bitmap \<sigma> d))"
apply (frule rf_sr_cbitmap_L2_relation)
apply (frule (1) ksReadyQueuesL1Bitmap_word_log2_max)
apply (drule (3) cbitmap_L2_relationD)
done
lemma ksReadyQueuesL2Bitmap_nonzeroI:
"\<lbrakk> d \<le> maxDomain ; valid_queues s ; ksReadyQueuesL1Bitmap s d \<noteq> 0 \<rbrakk>
\<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) \<noteq> 0"
unfolding valid_queues_def
apply clarsimp
apply (frule bitmapQ_no_L1_orphansD)
apply (erule word_log2_nth_same)
apply clarsimp
done
lemma clzl_spec:
"\<forall>s. \<Gamma> \<turnstile> {\<sigma>. s = \<sigma> \<and> x_' s \<noteq> 0} Call clzl_'proc
\<lbrace>\<acute>ret__long = of_nat (word_clz (x_' s)) \<rbrace>"

View File

@ -47,17 +47,6 @@ lemma threadSet_obj_at'_nontcb:
| clarsimp simp: updateObject_tcb updateObject_default_def in_monad)+
done
lemma setMRs_ntfn_at[wp]:
"\<lbrace>ko_at' (ntfn :: Structures_H.notification) p\<rbrace>
setMRs badge val thread
\<lbrace>\<lambda>_. ko_at' ntfn p\<rbrace>"
apply (simp add: setMRs_def
zipWithM_x_mapM_x split_def storeWordUser_def
setThreadState_def asUser_def)
apply (wp threadSet_obj_at'_nontcb mapM_x_wp hoare_drop_imps
| simp | rule subset_refl)+
done
lemma asUser_ntfn_at[wp]:
"\<lbrace>ko_at' (ntfn :: Structures_H.notification) p\<rbrace>
asUser tptr f \<lbrace>\<lambda>_. ko_at' ntfn p\<rbrace>"
@ -253,48 +242,6 @@ lemma threadGet_tcbFault_submonad_fn:
select_f_def modify_def put_def)
done
lemma asUser_threadGet_tcbFault_comm:
"empty_fail im \<Longrightarrow>
do y \<leftarrow> asUser t im;
x \<leftarrow> threadGet tcbFault t';
n x y
od =
do x \<leftarrow> threadGet tcbFault t';
asUser t im >>= n x
od"
apply (rule submonad_comm2 [OF tcbFault_submonad_args
threadGet_tcbFault_submonad_fn
submonad_asUser, symmetric])
apply (clarsimp simp: thread_replace_def asUser_replace_def Let_def
split: option.split)
apply (clarsimp simp: fun_upd_idem fun_upd_twist
split: kernel_object.split)
apply (rename_tac tcb)
apply (case_tac tcb, simp)
apply (clarsimp simp: asUser_replace_def Let_def obj_at'_real_def
ko_wp_at'_def ps_clear_upd_None ps_clear_upd
objBitsKO_def projectKOs
split: option.split kernel_object.split)
apply (clarsimp simp: thread_replace_def Let_def obj_at'_real_def
ko_wp_at'_def ps_clear_upd_None
ps_clear_upd objBitsKO_def projectKOs
split: option.split kernel_object.split)
apply (simp add: get_def empty_fail_def)
apply assumption
done
lemma asUser_getRegister_threadGet_comm:
"do
ra \<leftarrow> asUser a (getRegister r);
rb \<leftarrow> threadGet fb b;
c ra rb
od = do
rb \<leftarrow> threadGet fb b;
ra \<leftarrow> asUser a (getRegister r);
c ra rb
od"
by (rule bind_inv_inv_comm, auto; wp)
crunch inv[wp]: getSanitiseRegisterInfo P
(ignore: getObject)
@ -314,18 +261,6 @@ lemma asUser_getRegister_getSanitiseRegisterInfo_comm:
od"
by (rule bind_inv_inv_comm; wpsimp)
lemma asUser_mapMloadWordUser_threadGet_comm:
"do
ra \<leftarrow> mapM loadWordUser xs;
rb \<leftarrow> threadGet fb b;
c ra rb
od = do
rb \<leftarrow> threadGet fb b;
ra \<leftarrow> mapM loadWordUser xs;
c ra rb
od"
by (rule bind_inv_inv_comm, auto; wp mapM_wp')
lemma asUser_mapMloadWordUser_getSanitiseRegisterInfo_comm:
"do
ra \<leftarrow> mapM loadWordUser xs;
@ -338,21 +273,6 @@ lemma asUser_mapMloadWordUser_getSanitiseRegisterInfo_comm:
od"
by (rule bind_inv_inv_comm, auto; wp mapM_wp')
lemma threadGet_tcbFault_doMachineOp_comm:
"\<lbrakk> empty_fail m' \<rbrakk> \<Longrightarrow>
do x \<leftarrow> threadGet tcbFault t; y \<leftarrow> doMachineOp m'; n x y od =
do y \<leftarrow> doMachineOp m'; x \<leftarrow> threadGet tcbFault t; n x y od"
apply (rule submonad_comm2 [OF tcbFault_submonad_args
threadGet_tcbFault_submonad_fn
submonad_doMachineOp])
apply (simp add: thread_replace_def Let_def)
apply simp
apply (rule refl)
apply (simp add: get_def empty_fail_def)
apply assumption
done
lemma getObject_tcb_det:
"(r::tcb,s') \<in> fst (getObject p s) \<Longrightarrow> fst (getObject p s) = {(r,s)} \<and> s' = s"
apply (clarsimp simp add: getObject_def bind_def get_def gets_def
@ -366,18 +286,6 @@ lemma getObject_tcb_det:
unless_def when_def magnitudeCheck_def)
done
lemma threadGet_again:
"\<And>rv s s' n. (rv, s') \<in> fst (threadGet ext t s) \<Longrightarrow>
(threadGet ext t >>= n) s' = n rv s'"
apply (clarsimp simp add: threadGet_def liftM_def in_monad)
apply (frule use_valid [OF _ getObject_obj_at'])
apply (simp add: objBits_simps')+
apply (frule getObject_tcb_det)
apply (clarsimp simp: bind_def split_def)
apply (insert no_fail_getObject_tcb)
apply (clarsimp simp: no_fail_def obj_at'_def is_tcb)
done
lemma asUser_getRegister_discarded:
"(asUser t (getRegister r)) >>= (\<lambda>_. n) =
stateAssert (tcb_at' t) [] >>= (\<lambda>_. n)"
@ -399,38 +307,6 @@ lemma storeWordUser_submonad_fn:
(pointerInUserData p) (storeWord p v)"
by (simp add: storeWordUser_def submonad_doMachineOp.fn_is_sm submonad_fn_def)
lemma threadGet_tcbFault_loadWordUser_comm:
"do x \<leftarrow> threadGet tcbFault t; y \<leftarrow> loadWordUser p; n x y od =
do y \<leftarrow> loadWordUser p; x \<leftarrow> threadGet tcbFault t; n x y od"
apply (rule submonad_comm [OF tcbFault_submonad_args _
threadGet_tcbFault_submonad_fn
loadWordUser_submonad_fn])
apply (simp add: submonad_args_def pointerInUserData_def)
apply (simp add: thread_replace_def Let_def)
apply simp
apply (clarsimp simp: thread_replace_def Let_def typ_at'_def ko_wp_at'_def
ps_clear_upd ps_clear_upd_None pointerInUserData_def
split: option.split kernel_object.split)
apply (simp add: get_def empty_fail_def)
apply (simp add: ef_loadWord)
done
lemma threadGet_tcbFault_storeWordUser_comm:
"do x \<leftarrow> threadGet tcbFault t; y \<leftarrow> storeWordUser p v; n x y od =
do y \<leftarrow> storeWordUser p v; x \<leftarrow> threadGet tcbFault t; n x y od"
apply (rule submonad_comm [OF tcbFault_submonad_args _
threadGet_tcbFault_submonad_fn
storeWordUser_submonad_fn])
apply (simp add: submonad_args_def pointerInUserData_def)
apply (simp add: thread_replace_def Let_def)
apply simp
apply (clarsimp simp: thread_replace_def Let_def typ_at'_def ko_wp_at'_def
ps_clear_upd ps_clear_upd_None pointerInUserData_def
split: option.split kernel_object.split)
apply (simp add: get_def empty_fail_def)
apply (simp add: ef_storeWord)
done
lemma asUser_loadWordUser_comm:
"empty_fail m \<Longrightarrow>
do x \<leftarrow> asUser t m; y \<leftarrow> loadWordUser p; n x y od =
@ -447,22 +323,6 @@ lemma asUser_loadWordUser_comm:
apply assumption
done
lemma asUser_storeWordUser_comm:
"empty_fail m \<Longrightarrow>
do x \<leftarrow> asUser t m; y \<leftarrow> storeWordUser p v; n x y od =
do y \<leftarrow> storeWordUser p v; x \<leftarrow> asUser t m; n x y od"
apply (rule submonad_comm2 [OF _ storeWordUser_submonad_fn
submonad_asUser, symmetric])
apply (simp add: submonad_args_def pointerInUserData_def)
apply (simp add: asUser_replace_def Let_def)
apply (clarsimp simp: asUser_replace_def Let_def typ_at'_def ko_wp_at'_def
ps_clear_upd ps_clear_upd_None pointerInUserData_def
split: option.split kernel_object.split)
apply simp
apply (simp add: ef_storeWord)
apply assumption
done
lemma length_syscallMessage:
"length ARM_H.syscallMessage = unat n_syscallMessage"
apply (simp add: syscallMessage_def ARM.syscallMessage_def
@ -566,15 +426,6 @@ lemma loadWordUser_discarded:
modify_def put_def)
done
lemma stateAssert_mapM_loadWordUser_comm:
"do x \<leftarrow> stateAssert P []; y \<leftarrow> mapM loadWordUser ptrs; n od =
do y \<leftarrow> mapM loadWordUser ptrs; x \<leftarrow> stateAssert P []; n od"
apply (rule bind_inv_inv_comm)
apply (wp stateAssert_inv)
apply (wp mapM_wp_inv)+
apply simp
done
lemmas syscallMessage_unfold
= ARM_H.syscallMessage_def
ARM.syscallMessage_def
@ -605,34 +456,8 @@ lemma handleArchFaultReply':
apply (case_tac sb, simp_all add: word_size n_msgRegisters_def)[1]
done
lemmas lookup_uset_getreg_swap = bind_inv_inv_comm[OF lookupIPCBuffer_inv
user_getreg_inv'
empty_fail_lookupIPCBuffer
empty_fail_asUser[OF empty_fail_getRegister]]
end
lemma mapM_x_zip_take_Cons_append:
"n = 0 \<longrightarrow> zs = []
\<Longrightarrow> mapM_x f (zip (x # xs) (take n (y # ys) @ zs))
= do
when (n > 0) (f (x, y));
mapM_x f (zip xs (take (n - 1) ys @ zs))
od"
by (cases n, simp_all add: mapM_x_Cons)
lemma threadGet_lookupIPCBuffer_comm:
"do
a \<leftarrow> lookupIPCBuffer x y;
t \<leftarrow> threadGet id r;
c a t
od = do
t \<leftarrow> threadGet id r;
a \<leftarrow> lookupIPCBuffer x y;
c a t
od"
by (rule bind_inv_inv_comm; wp?; auto)
lemma getSanitiseRegisterInfo_lookupIPCBuffer_comm:
"do
a \<leftarrow> lookupIPCBuffer x y;
@ -645,28 +470,6 @@ lemma getSanitiseRegisterInfo_lookupIPCBuffer_comm:
od"
by (rule bind_inv_inv_comm; wp?; auto)
lemma threadGet_moreMapM_comm:
"do
a \<leftarrow>
case sb of None \<Rightarrow> return []
| Some bufferPtr \<Rightarrow> return (xs bufferPtr) >>= mapM loadWordUser;
t \<leftarrow> threadGet id r;
c a t
od = do
t \<leftarrow> threadGet id r;
a \<leftarrow>
case sb of None \<Rightarrow> return []
| Some bufferPtr \<Rightarrow> return (xs bufferPtr) >>= mapM loadWordUser;
c a t
od"
apply (rule bind_inv_inv_comm)
apply (rule hoare_pre, wpc; (wp mapM_wp')?)
apply simp
apply wp
apply (auto split: option.splits)
done
lemma getSanitiseRegisterInfo_moreMapM_comm:
"do
a \<leftarrow>
@ -699,14 +502,6 @@ lemma monadic_rewrite_symb_exec_r':
apply simp
done
lemma monadic_rewrite_threadGet_return:
"monadic_rewrite True False (tcb_at' r) (return x) (do t \<leftarrow> threadGet f r; return x od)"
apply (rule monadic_rewrite_symb_exec_r')
apply wp+
apply (rule monadic_rewrite_refl)
apply wp
done
context begin interpretation Arch .
lemma no_fail_getSanitiseRegisterInfo[wp, simp]:
@ -716,36 +511,11 @@ lemma no_fail_getSanitiseRegisterInfo[wp, simp]:
end
lemma monadic_rewrite_getSanitiseRegisterInfo_return:
"monadic_rewrite True False (tcb_at' r) (return x) (do t \<leftarrow> getSanitiseRegisterInfo r; return x od)"
apply (rule monadic_rewrite_symb_exec_r')
apply wp+
apply (rule monadic_rewrite_refl)
apply wp
done
lemma monadic_rewrite_getSanitiseRegisterInfo_drop:
"monadic_rewrite True False (tcb_at' r) (d) (do t \<leftarrow> getSanitiseRegisterInfo r; d od)"
apply (rule monadic_rewrite_symb_exec_r')
apply wp+
apply (rule monadic_rewrite_refl)
apply wp
done
lemma monadic_rewrite_inst: "monadic_rewrite F E P f g \<Longrightarrow> monadic_rewrite F E P f g"
by simp
context kernel_m begin interpretation Arch .
lemma threadGet_discarded:
"(threadGet f t >>= (\<lambda>_. n)) = stateAssert (tcb_at' t) [] >>= (\<lambda>_. n)"
apply (simp add: threadGet_def getObject_get_assert liftM_def bind_assoc stateAssert_def)
apply (rule ext)
apply (simp add: bind_def simpler_gets_def get_def)
done
lemma monadic_rewrite_do_flip:
"monadic_rewrite E F P (do c \<leftarrow> j; a \<leftarrow> f; b \<leftarrow> g c; return (a, c) od)
(do c \<leftarrow> j; b \<leftarrow> g c; a \<leftarrow> f; return (a, c) od)
@ -784,10 +554,10 @@ lemma handleFaultReply':
(erule disjE[OF word_less_cases],
( clarsimp simp: n_msgRegisters_def asUser_bind_distrib
mapM_x_Cons mapM_x_Nil bind_assoc
asUser_getRegister_discarded asUser_mapMloadWordUser_threadGet_comm
asUser_getRegister_discarded
asUser_getRegister_getSanitiseRegisterInfo_comm
asUser_mapMloadWordUser_getSanitiseRegisterInfo_comm
asUser_comm[OF neq] asUser_getRegister_threadGet_comm
asUser_comm[OF neq]
bind_comm_mapM_comm [OF asUser_loadWordUser_comm, symmetric]
word_le_nat_alt[of 4, simplified linorder_not_less[symmetric, of 4]]
asUser_return submonad_asUser.fn_stateAssert
@ -857,8 +627,6 @@ lemma handleFaultReply':
| rule monadic_rewrite_bind_tail monadic_rewrite_refl
monadic_rewrite_symb_exec_l[OF mapM_x_mapM_valid[OF mapM_x_wp']]
monadic_rewrite_symb_exec_l[OF stateAssert_inv]
monadic_rewrite_threadGet_return
monadic_rewrite_getSanitiseRegisterInfo_return
| wp mapM_wp')+)+
apply (simp add: n_msgRegisters_def word_le_nat_alt n_syscallMessage_def
linorder_not_less syscallMessage_unfold)
@ -869,8 +637,8 @@ lemma handleFaultReply':
@ [scast n_syscallMessage + 1 .e. msgMaxLength]")
apply (simp only: upto_enum_word[where y="scast n_syscallMessage :: word32"]
upto_enum_word[where y="scast n_syscallMessage + 1 :: word32"])
apply (clarsimp simp: bind_assoc asUser_bind_distrib asUser_getRegister_threadGet_comm
mapM_x_Cons mapM_x_Nil threadGet_discarded
apply (clarsimp simp: bind_assoc asUser_bind_distrib
mapM_x_Cons mapM_x_Nil
asUser_comm [OF neq] asUser_getRegister_discarded
submonad_asUser.fn_stateAssert take_zip
bind_subst_lift [OF submonad_asUser.stateAssert_fn]
@ -895,9 +663,6 @@ lemma handleFaultReply':
monadic_rewrite_refl
monadic_rewrite_symb_exec_l[OF stateAssert_inv]
monadic_rewrite_symb_exec_l[OF mapM_x_mapM_valid[OF mapM_x_wp']]
monadic_rewrite_threadGet_return
monadic_rewrite_getSanitiseRegisterInfo_return
monadic_rewrite_getSanitiseRegisterInfo_drop
| wp empty_fail_loadWordUser)+)+
apply (clarsimp simp: upto_enum_word word_le_nat_alt simp del: upt.simps cong: if_weak_cong)
apply (cut_tac i="unat n" and j="Suc (unat (scast n_syscallMessage :: word32))"
@ -927,12 +692,6 @@ end
context kernel_m
begin
(* FIXME: move *)
lemma ccorres_merge_return:
"ccorres (\<lambda>a c. r (f a) c) xf P P' hs H C \<Longrightarrow>
ccorres r xf P P' hs (do x \<leftarrow> H; return (f x) od) C"
by (rule ccorres_return_into_rel)
(* FIXME: move *)
lemma ccorres_break:
assumes r: "\<And>s s'. \<lbrakk> (s,s') \<in> rf_sr; P s; s' \<in> P' \<rbrakk> \<Longrightarrow> r (Inl e) (xf s')"
@ -1066,23 +825,6 @@ lemma messageInfoFromWord_ccorres [corres]:
shiftL_nat msgMaxLength_def msgLabelBits_def)
done
lemma getMessageInfo_ccorres:
"ccorres (\<lambda>r r'. r = message_info_to_H r') ret__struct_seL4_MessageInfo_C_'
(tcb_at' sender) UNIV hs (getMessageInfo sender)
(\<acute>ret__unsigned_long :== CALL getRegister(tcb_ptr_to_ctcb_ptr sender,scast Kernel_C.msgInfoRegister);;
\<acute>ret__struct_seL4_MessageInfo_C :== CALL messageInfoFromWord(\<acute>ret__unsigned_long))"
unfolding getMessageInfo_def
apply simp
apply (rule ccorres_guard_imp2)
apply ctac
apply ctac
apply wp
apply vcg
apply (frule (1) obj_at_cslift_tcb)
apply (clarsimp simp: typ_heap_simps ARM_H.msgInfoRegister_def ARM.msgInfoRegister_def
Kernel_C.msgInfoRegister_def Kernel_C.R1_def dest!: c_guard_clift)
done
lemma getMessageInfo_ccorres':
"ccorres (\<lambda>r r'. r = message_info_to_H r') tag_'
(tcb_at' sender) UNIV hs (getMessageInfo sender)
@ -1125,16 +867,6 @@ lemma replyFromKernel_success_empty_ccorres [corres]:
message_info_to_H_def)
done
lemma msgRegisters_offset_conv:
"\<And>offset i. \<lbrakk> offset + i < length ARM_H.msgRegisters \<rbrakk> \<Longrightarrow>
index msgRegistersC (unat ((of_nat offset :: word32) + of_nat i)) =
register_from_H (ARM_H.msgRegisters ! (offset + i))"
apply (simp add: msgRegistersC_def msgRegisters_unfold fupdate_def)
apply (subst of_nat_add [symmetric])
apply (case_tac "offset + i", simp_all del: of_nat_add)
apply (case_tac nat, simp, rename_tac nat, simp)+
done
lemmas ccorres_pre_stateAssert =
ccorres_symb_exec_l [OF _ stateAssert_inv stateAssert_wp
empty_fail_stateAssert]
@ -1405,12 +1137,6 @@ lemma setMRs_syscall_error_ccorres:
| simp add: to_bool_def split: if_split)+
done
lemma lookupIPCBuffer_aligned_option_to_0:
"\<lbrace>valid_objs'\<rbrace> lookupIPCBuffer b s \<lbrace>\<lambda>rv s. is_aligned (option_to_0 rv) msg_align_bits\<rbrace>"
apply (rule hoare_strengthen_post, rule lookupIPCBuffer_valid_ipc_buffer)
apply (simp add: option_to_0_def valid_ipc_buffer_ptr'_def split: option.split_asm)
done
lemma Cond_if_mem:
"(Cond (if P then UNIV else {})) = (Cond {s. P})"
by simp
@ -1450,9 +1176,6 @@ lemma copyMRs_register_loop_helper:
lemma mab_gt_2 [simp]:
"2 \<le> msg_align_bits" by (simp add: msg_align_bits)
lemma wb_gt_2:
"2 < word_bits" by (simp add: word_bits_conv)
(* FIXME move *)
lemma mapM_only_length:
"do ys \<leftarrow> mapM f xs;
@ -1573,17 +1296,6 @@ declare zipWith_Nil2[simp]
declare zipWithM_x_Nil2[simp]
lemma getRestartPC_ccorres [corres]:
"ccorres (=) ret__unsigned_long_' \<top>
(UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>) hs
(asUser thread (getRegister register.FaultInstruction))
(Call getRestartPC_'proc)"
apply (cinit' lift: thread_')
apply (rule ccorres_trim_return, simp, simp)
apply ctac
apply clarsimp
done
lemma asUser_tcbFault_obj_at:
"\<lbrace>obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace> asUser t' m
\<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace>"
@ -1602,15 +1314,6 @@ lemma asUser_atcbContext_obj_at:
apply simp
done
lemma asUser_tcbFault_inv:
"\<lbrace>\<lambda>s. \<exists>t. ko_at' t p' s \<and> tcbFault t = f\<rbrace> asUser p m
\<lbrace>\<lambda>rv s. \<exists>t. ko_at' t p' s \<and> tcbFault t = f\<rbrace>"
apply (rule_tac Q="\<lambda>rv. obj_at' (\<lambda>t. tcbFault t = f) p'"
in hoare_strengthen_post)
apply (wp asUser_tcbFault_obj_at)
apply (clarsimp simp: obj_at'_def)+
done
lemma setMR_atcbContext_obj_at:
"t \<noteq> t' \<Longrightarrow>
\<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>
@ -1860,7 +1563,7 @@ proof -
apply (rule aligned_add_aligned[where n=2])
apply (simp add: is_aligned_def)
apply (rule is_aligned_mult_triv2 [where n=2, simplified])
apply (simp add: wb_gt_2)+
apply (simp)+
apply (simp add: n_msgRegisters_def)
apply (vcg exspec=getRegister_modifies)
apply simp
@ -2543,10 +2246,6 @@ lemma setExtraBadge_ccorres:
msgExtraCapBits_def unat_word_ariths unat_of_nat)
done
lemma option_to_0_Some:
"option_to_0 (Some x) = x"
by (simp add: option_to_0_def)
(* FIXME: move *)
lemma ccorres_constOnFailure:
assumes corr_ac: "ccorres (\<lambda>f c. case f of Inl x \<Rightarrow> r n c | Inr n \<Rightarrow> r n c)
@ -2579,25 +2278,6 @@ lemma ccorres_case_sum_liftE:
apply (fastforce simp: unif_rrel_def)
done
(* FIXME: move *)
lemma ccorres_case_bools_rhs:
assumes P: "ccorres r xf P P' hs a c"
assumes Q: "ccorres r xf Q Q' hs a c"
shows "ccorres r xf (P and Q)
({s. s \<in> B \<longrightarrow> s \<in> P'} \<inter> {s. s \<notin> B \<longrightarrow> s \<in> Q'})
hs a c" using P Q
apply (clarsimp simp: ccorres_underlying_def)
apply (drule (1) bspec)+
apply clarsimp
apply (case_tac "b \<in> B", auto)
done
(* FIXME: move *)
lemma ccorres_return_bind_add:
"ccorres r xf P P' hs (do z \<leftarrow> return (f x); H z od) C \<Longrightarrow> ccorres r xf P P' hs (H (f x)) C"
by simp
(* FIXME: move *)
lemma ccorres_if_cond_throws_break:
fixes e :: 'e
@ -2692,25 +2372,11 @@ lemma maskAsFull_isEndpoint[simp]:
"isEndpointCap a \<Longrightarrow> maskedAsFull a b = a"
by (clarsimp simp:isCap_simps maskedAsFull_def)
lemma maskAsFull_eq_ep:
"maskedAsFull cap cap =
EndpointCap a b c d e \<Longrightarrow> cap = EndpointCap a b c d e"
by (clarsimp simp:maskedAsFull_def isCap_simps split:if_splits)
lemma is_derived_capMasterCap:
"is_derived' m slot cap cap'
\<Longrightarrow> capMasterCap cap = capMasterCap cap'"
by (clarsimp simp:is_derived'_def badge_derived'_def)
lemma maskedAsFull_misc:
"badge_derived' a (maskedAsFull a b)"
"capASID (maskedAsFull a b) = capASID a"
"cap_asid_base' (maskedAsFull a b) = cap_asid_base' a"
"cap_vptr' (maskedAsFull a b) = cap_vptr' a"
"capMasterCap (maskedAsFull a b) = capMasterCap a"
by (auto simp:maskedAsFull_def isCap_simps badge_derived'_def
split:if_split)
lemma maskedAsFull_again:
"maskedAsFull (maskedAsFull aa aa) r = maskedAsFull aa aa"
apply (case_tac aa)
@ -2866,16 +2532,6 @@ next
cap_vptr' scap = cap_vptr' (cteCap cte)) slot s) = relative_at scap slot s"
by (simp add:relative_at_def)
have stableD:
"\<And>scap excap. stable scap excap
\<Longrightarrow> (badge_derived' scap excap \<and>
capASID scap = capASID excap \<and>
cap_asid_base' scap = cap_asid_base' excap \<and> cap_vptr' scap = cap_vptr' excap)"
apply (clarsimp simp:stable_def)
apply (case_tac "excap = scap",simp+)
apply (simp add:maskedAsFull_misc)
done
have stable_eq:
"\<And>scap excap. \<lbrakk>stable scap excap; isEndpointCap excap\<rbrakk> \<Longrightarrow> scap = excap"
by (simp add:isCap_simps stable_def maskedAsFull_def split:if_splits)
@ -3172,18 +2828,6 @@ lemma cte_wp_at_imp_consequent':
"cte_wp_at' Q p s \<longrightarrow> cte_wp_at' (\<lambda>cte. P cte \<longrightarrow> Q cte) p s"
by (clarsimp simp: cte_wp_at_ctes_of)
lemma lookupExtraCaps_srcs2:
"\<lbrace>\<top>\<rbrace> lookupExtraCaps t buf mi \<lbrace>\<lambda>caps s. \<forall>x \<in> set caps. cte_wp_at'
(\<lambda>cte. cteCap cte = fst x) (snd x) s\<rbrace>,-"
apply (simp add: lookupExtraCaps_def lookupCapAndSlot_def
split_def lookupSlotForThread_def
getSlotCap_def)
apply (wp mapME_set[where R=\<top>] getCTE_wp'
| simp add: cte_wp_at_ctes_of
| wp_once hoare_drop_imps
| (rule hoare_strengthen_post [OF hoare_TrueI], rule allI, rule impI, rule TrueI))+
done
lemma transferCaps_ccorres [corres]:
notes if_cong[cong]
notes extra_sle_sless_unfolds[simp del]
@ -3686,10 +3330,6 @@ lemma lookupIPCBuffer_not_Some_0:
| intro conjI impI | wpc)+
done
lemma pageBitsForSize_2 [simp]:
"2 \<le> pageBitsForSize sz"
by (cases sz, auto)
lemma pbfs_msg_align_bits [simp]:
"msg_align_bits \<le> pageBitsForSize sz"
by (cases sz, auto simp: msg_align_bits)
@ -3708,12 +3348,6 @@ lemma lookupIPCBuffer_aligned:
apply (auto elim: aligned_add_aligned intro: is_aligned_andI1)
done
lemma isArchPageCap_def2:
"\<And>cap. isArchPageCap cap = (isArchObjectCap cap \<and> isPageCap (capCap cap))"
by (fastforce simp: isCap_simps)
lemma replyFromKernel_error_ccorres [corres]:
"ccorres dc xfdc (valid_pspace' and tcb_at' thread)
(UNIV \<inter> \<lbrace>syscall_error_to_H \<acute>current_syscall_error
@ -3740,7 +3374,7 @@ lemma replyFromKernel_error_ccorres [corres]:
apply (wp hoare_case_option_wp)
apply (vcg exspec=setRegister_modifies)
apply simp
apply (wp lookupIPCBuffer_aligned_option_to_0)
apply (wp)
apply (simp del: Collect_const)
apply (vcg exspec=lookupIPCBuffer_modifies)
apply (simp add: msgInfoRegister_def
@ -3820,12 +3454,6 @@ lemma doIPCTransfer_ccorres [corres]:
apply (auto simp: to_bool_def true_def)
done
lemma fault_case_absorb_bind:
"(do x \<leftarrow> f; case_fault (p x) (q x) (r x) (s x) ft od)
= case_fault (\<lambda>a b. f >>= (\<lambda>x. p x a b)) (\<lambda>a b c. f >>= (\<lambda>x. q x a b c))
(\<lambda>a. f >>= (\<lambda>x. r x a)) (\<lambda>a. f >>= (\<lambda>x. s x a)) ft"
by (simp split: fault.split)
lemma length_exceptionMessage:
"length ARM_H.exceptionMessage = unat n_exceptionMessage"
by (simp add: ARM_H.exceptionMessage_def ARM.exceptionMessage_def n_exceptionMessage_def)
@ -4236,7 +3864,7 @@ lemma handleFaultReply_ccorres [corres]:
cfault_rel_def seL4_Fault_lift_def Let_def
split: if_split_asm)
apply ceqv
apply (simp add: handleFaultReply_def fault_case_absorb_bind
apply (simp add: handleFaultReply_def
del: Collect_const split del: if_split)
apply wpc
(* UserException *)
@ -4380,19 +4008,6 @@ crunch tcbFault: setThreadState, cancelAllIPC, cancelAllSignals
"obj_at' (\<lambda>tcb. P (tcbFault tcb)) t"
(wp: threadSet_obj_at'_strongish crunch_wps)
(* FIXME: move *)
lemmas setEndpoint_tcb = KHeap_R.setEndpoint_obj_at'_tcb
(* FIXME: move *)
lemma setNotification_tcb:
"\<lbrace>obj_at' (\<lambda>tcb::tcb. P tcb) t\<rbrace>
setNotification ntfn e
\<lbrace>\<lambda>_. obj_at' P t\<rbrace>"
apply (simp add: setNotification_def)
apply (rule obj_at_setObject2)
apply (clarsimp simp: updateObject_default_def in_monad)
done
lemma sbn_tcbFault:
"\<lbrace>obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace>
setBoundNotification st t'
@ -6430,10 +6045,6 @@ lemma sts_runnable:
apply auto
done
lemma st_tcb'_iff:
"st_tcb_at' \<top> t = tcb_at' t"
by (auto simp:st_tcb_at'_def)
lemma sendSignal_ccorres [corres]:
"ccorres dc xfdc (invs')
(UNIV \<inter> \<lbrace>\<acute>ntfnPtr = Ptr ntfnptr\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace>) hs

View File

@ -101,6 +101,8 @@ lemma get_tcb_state_regs_partial_overwrite[simp]:
split: tcb_state_regs.split)
done
(* This is currently unused, but might be useful.
it might be worth fixing if it breaks, but ask around first. *)
lemma isolate_thread_actions_bind:
"inj idx \<Longrightarrow>
isolate_thread_actions idx a b c >>=
@ -126,25 +128,13 @@ lemma tcbSchedEnqueue_obj_at_unchangedT:
apply (wp | simp add: y)+
done
lemma asUser_obj_at_notQ:
"\<lbrace>obj_at' (Not \<circ> tcbQueued) t\<rbrace>
asUser t (setRegister r v)
\<lbrace>\<lambda>rv. obj_at' (Not \<circ> tcbQueued) t\<rbrace>"
apply (simp add: asUser_def)
apply (rule hoare_seq_ext)+
apply (simp add: split_def)
apply (rule threadSet_obj_at'_really_strongest)
apply (wp threadGet_wp |rule gets_inv|wpc|clarsimp)+
apply (clarsimp simp: obj_at'_def)
done
(* FIXME: Move to Schedule_R.thy. Make Arch_switchToThread_obj_at a specialisation of this *)
lemma Arch_switchToThread_obj_at_pre:
"\<lbrace>obj_at' (Not \<circ> tcbQueued) t\<rbrace>
Arch.switchToThread t
\<lbrace>\<lambda>rv. obj_at' (Not \<circ> tcbQueued) t\<rbrace>"
apply (simp add: ARM_H.switchToThread_def)
apply (wp asUser_obj_at_notQ doMachineOp_obj_at setVMRoot_obj_at hoare_drop_imps|wpc)+
apply (wp doMachineOp_obj_at setVMRoot_obj_at hoare_drop_imps|wpc)+
done
lemma rescheduleRequired_obj_at_unchangedT:
@ -298,18 +288,6 @@ lemma isolate_thread_actions_asUser:
apply (case_tac ko, simp)
done
lemma getRegister_simple:
"getRegister r = (\<lambda>con. ({(con r, con)}, False))"
by (simp add: getRegister_def simpler_gets_def)
lemma mapM_getRegister_simple:
"mapM getRegister rs = (\<lambda>con. ({(map con rs, con)}, False))"
apply (induct rs)
apply (simp add: mapM_Nil return_def)
apply (simp add: mapM_Cons getRegister_def simpler_gets_def
bind_def return_def)
done
lemma setRegister_simple:
"setRegister r v = (\<lambda>con. ({((), con (r := v))}, False))"
by (simp add: setRegister_def simpler_modify_def)
@ -847,23 +825,6 @@ lemma doIPCTransfer_simple_rewrite:
apply (auto elim!: obj_at'_weakenE)
done
lemma monadic_rewrite_setSchedulerAction_noop:
"monadic_rewrite F E (\<lambda>s. ksSchedulerAction s = act) (setSchedulerAction act) (return ())"
unfolding setSchedulerAction_def
apply (rule monadic_rewrite_imp, rule monadic_rewrite_modify_noop)
apply simp
done
lemma rescheduleRequired_simple_rewrite:
"monadic_rewrite F E
(sch_act_simple)
rescheduleRequired
(setSchedulerAction ChooseNewThread)"
apply (simp add: rescheduleRequired_def getSchedulerAction_def)
apply (simp add: monadic_rewrite_def exec_gets sch_act_simple_def)
apply auto
done
lemma empty_fail_isRunnable:
"empty_fail (isRunnable t)"
by (simp add: isRunnable_def isBlocked_def)
@ -1348,12 +1309,6 @@ lemma threadGet_isolatable:
split: tcb_state_regs.split)+
done
lemma monadic_rewrite_trans_dup:
"\<lbrakk> monadic_rewrite F E P f g; monadic_rewrite F E P g h \<rbrakk>
\<Longrightarrow> monadic_rewrite F E P f h"
by (auto simp add: monadic_rewrite_def)
lemma setCurThread_isolatable:
"thread_actions_isolatable idx (setCurThread t)"
by (simp add: setCurThread_def modify_isolatable)
@ -1415,37 +1370,6 @@ definition
= tsrs (dest := TCBStateRegs (tsrState (tsrs dest))
((tsrContext (tsrs dest)) (r := v)))"
lemma set_register_isolate:
"\<lbrakk> inj idx; idx y = dest \<rbrakk> \<Longrightarrow>
monadic_rewrite False True
(\<lambda>s. \<forall>x. tcb_at' (idx x) s)
(asUser dest (setRegister r v))
(isolate_thread_actions idx (return ())
(set_register_tsrs y r v) id)"
apply (simp add: asUser_def split_def bind_assoc
getRegister_def setRegister_def
select_f_returns isolate_thread_actions_def
getSchedulerAction_def)
apply (simp add: threadGet_def liftM_def getObject_get_assert
bind_assoc threadSet_def
setObject_modify_assert)
apply (clarsimp simp: monadic_rewrite_def exec_gets
exec_modify tcb_at_KOTCB_upd)
apply (clarsimp simp: simpler_modify_def
intro!: kernel_state.fold_congs[OF refl refl])
apply (clarsimp simp: set_register_tsrs_def o_def
partial_overwrite_fun_upd
partial_overwrite_get_tcb_state_regs)
apply (drule_tac x=y in spec)
apply (clarsimp simp: obj_at'_def projectKOs objBits_simps
cong: if_cong)
apply (case_tac obj)
apply (simp add: projectKO_opt_tcb put_tcb_state_regs_def
put_tcb_state_regs_tcb_def get_tcb_state_regs_def
cong: if_cong)
done
lemma copy_register_isolate:
"\<lbrakk> inj idx; idx x = src; idx y = dest \<rbrakk> \<Longrightarrow>
monadic_rewrite False True
@ -1478,10 +1402,6 @@ lemma copy_register_isolate:
apply (auto simp: fun_eq_iff split: if_split)
done
lemmas monadic_rewrite_bind_alt
= monadic_rewrite_trans[OF monadic_rewrite_bind_tail monadic_rewrite_bind_head, rotated -1]
lemma monadic_rewrite_isolate_final2:
assumes mr: "monadic_rewrite F E Q f g"
and eqs: "\<And>s tsrs. \<lbrakk> P s; tsrs = get_tcb_state_regs o ksPSpace s o idx \<rbrakk>

View File

@ -57,10 +57,6 @@ lemma suspend_st_tcb_at':
apply (simp|wp cancelIPC_st_tcb_at' sts_st_tcb')+
done
lemma to_bool_if:
"(if w \<noteq> 0 then 1 else 0) = (if to_bool w then 1 else 0)"
by (auto simp: to_bool_def)
lemma threadGet_wp'':
"\<lbrace>\<lambda>s. \<forall>v. obj_at' (\<lambda>tcb. f tcb = v) thread s \<longrightarrow> P v s\<rbrace> threadGet f thread \<lbrace>P\<rbrace>"
apply (rule hoare_pre)
@ -68,29 +64,8 @@ lemma threadGet_wp'':
apply (clarsimp simp: obj_at'_def)
done
lemma tcbSchedEnqueue_queued_queues_inv:
"\<lbrace>\<lambda>s. obj_at' tcbQueued t s \<and> P (ksReadyQueues s) \<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_ s. P (ksReadyQueues s)\<rbrace>"
unfolding tcbSchedEnqueue_def unless_def
apply (wpsimp simp: if_apply_def2 wp: threadGet_wp)
apply normalise_obj_at'
done
lemma addToBitmap_sets_L1Bitmap_same_dom:
"\<lbrace>\<lambda>s. p \<le> maxPriority \<and> d' = d \<rbrace> addToBitmap d' p
\<lbrace>\<lambda>rv s. ksReadyQueuesL1Bitmap s d \<noteq> 0 \<rbrace>"
unfolding addToBitmap_def bitmap_fun_defs
apply wpsimp
apply (clarsimp simp: maxPriority_def numPriorities_def word_or_zero le_def
prioToL1Index_max[simplified wordRadix_def, simplified])
done
crunch ksReadyQueuesL1Bitmap[wp]: setQueue "\<lambda>s. P (ksReadyQueuesL1Bitmap s)"
lemma tcb_in_cur_domain'_def':
"tcb_in_cur_domain' t = (\<lambda>s. obj_at' (\<lambda>tcb. tcbDomain tcb = ksCurDomain s) t s)"
unfolding tcb_in_cur_domain'_def
by (auto simp: obj_at'_def)
lemma sts_running_ksReadyQueuesL1Bitmap[wp]:
"\<lbrace>\<lambda>s. P (ksReadyQueuesL1Bitmap s)\<rbrace>
setThreadState Structures_H.thread_state.Running t

View File

@ -15,11 +15,6 @@ begin
context kernel_m
begin
lemma isArchPageCap_ArchObjectCap:
"isArchPageCap (ArchObjectCap acap)
= isPageCap acap"
by (simp add: isArchPageCap_def isPageCap_def)
definition
"replicateHider \<equiv> replicate"
@ -46,7 +41,6 @@ lemma coerce_memset_to_heap_update_user_data:
user_context_C_tag_def thread_state_C_tag_def seL4_Fault_C_tag_def
lookup_fault_C_tag_def update_ti_t_ptr_0s
ti_typ_pad_combine_empty_ti ti_typ_pad_combine_td
ti_typ_combine_empty_ti ti_typ_combine_td
align_of_def padup_def
final_pad_def size_td_lt_ti_typ_pad_combine Let_def size_of_def
align_td_array' size_td_array)
@ -150,19 +144,6 @@ lemma user_data_at_rf_sr_dom_s:
apply (simp add: h_t_valid_dom_s pageBits_def)
done
lemma device_data_at_rf_sr_dom_s:
"\<lbrakk> typ_at' UserDataDeviceT x s; (s, s') \<in> rf_sr \<rbrakk>
\<Longrightarrow> {x ..+ 2 ^ pageBits} \<times> {SIndexVal, SIndexTyp 0}
\<subseteq> dom_s (hrs_htd (t_hrs_' (globals s')))"
apply (drule rf_sr_heap_device_data_relation)
apply (drule device_data_at_ko)
apply (erule_tac x=x in cmap_relationE1)
apply (simp only: heap_to_device_data_def Let_def ko_at_projectKO_opt)
apply simp
apply (drule h_t_valid_clift)
apply (simp add: h_t_valid_dom_s pageBits_def)
done
lemma intvl_2_power_times_decomp:
"\<forall>y < 2 ^ (n - m). {x + y * 2 ^ m ..+ 2 ^ m} \<times> S \<subseteq> T
\<Longrightarrow> m \<le> n \<Longrightarrow> n < word_bits
@ -219,197 +200,6 @@ lemma power_user_page_foldl_zero_ranges:
apply clarsimp
done
lemma heap_to_device_data_disj_mdf':
"\<lbrakk>is_aligned ptr (pageBitsForSize sz); ksPSpace \<sigma> a = Some obj; objBitsKO obj = pageBits; pspace_aligned' \<sigma>;
pspace_distinct' \<sigma>; pspace_no_overlap' ptr (pageBitsForSize sz) \<sigma>\<rbrakk>
\<Longrightarrow> heap_to_device_data (ksPSpace \<sigma>)
(\<lambda>x. if x \<in> {ptr..+2 ^ (pageBitsForSize sz)} then 0
else underlying_memory (ksMachineState \<sigma>) x)
a =
heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) a"
apply (cut_tac heap_to_device_data_disj_mdf[where ptr = ptr
and gbits = "pageBitsForSize sz - pageBits" and n = 1
and sz = "pageBitsForSize sz",simplified])
apply (simp add: pbfs_atleast_pageBits pbfs_less_wb' field_simps| intro range_cover_full )+
done
lemma range_cover_nca_neg: "\<And>x p (off :: 10 word).
\<lbrakk>(x::word32) < 4; {p..+2 ^pageBits } \<inter> {ptr..ptr + (of_nat n * 2 ^ bits - 1)} = {};
range_cover ptr sz bits n\<rbrakk>
\<Longrightarrow> p + ucast off * 4 + x \<notin> {ptr..+n * 2 ^ bits}"
apply (case_tac "n = 0")
apply simp
apply (subst range_cover_intvl,simp)
apply simp
apply (subgoal_tac " p + ucast off * 4 + x \<in> {p..+2 ^ pageBits}")
apply blast
apply (clarsimp simp: intvl_def)
apply (rule_tac x = "unat off * 4 + unat x" in exI)
apply (simp add: ucast_nat_def)
apply (rule nat_add_offset_less [where n = 2, simplified])
apply (simp add: word_less_nat_alt)
apply (rule unat_lt2p)
apply (simp add: pageBits_def objBits_simps)
done
lemma clearMemory_PageCap_ccorres:
"ccorres dc xfdc (invs' and valid_cap' (ArchObjectCap (PageCap False ptr undefined sz None))
and (\<lambda>s. 2 ^ pageBitsForSize sz \<le> gsMaxObjectSize s)
and K ({ptr .. ptr + 2 ^ (pageBitsForSize sz) - 1} \<inter> kernel_data_refs = {})
)
(UNIV \<inter> {s. bits_' s = of_nat (pageBitsForSize sz)}
\<inter> {s. ptr___ptr_to_unsigned_long_' s = Ptr ptr})
[]
(doMachineOp (clearMemory ptr (2 ^ pageBitsForSize sz))) (Call clearMemory_'proc)"
(is "ccorres dc xfdc ?P ?P' [] ?m ?c")
apply (cinit' lift: bits_' ptr___ptr_to_unsigned_long_')
apply (rule_tac P="capAligned (ArchObjectCap (PageCap False ptr undefined sz None))"
in ccorres_gen_asm)
apply (rule ccorres_Guard_Seq)
apply (simp add: clearMemory_def)
apply (simp add: doMachineOp_bind ef_storeWord)
apply (rule ccorres_split_nothrow_novcg_dc)
apply (rule_tac P="?P" in ccorres_from_vcg[where P'=UNIV])
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: valid_cap'_def capAligned_def
is_aligned_no_wrap'[OF _ word32_power_less_1])
apply (subgoal_tac "2 \<le> pageBitsForSize sz")
prefer 2
apply (simp add: pageBitsForSize_def split: vmpage_size.split)
apply (rule conjI)
apply (erule is_aligned_weaken)
apply (clarsimp simp: pageBitsForSize_def split: vmpage_size.splits)
apply (rule conjI)
apply (rule is_aligned_power2)
apply (clarsimp simp: pageBitsForSize_def split: vmpage_size.splits)
apply (clarsimp simp: ghost_assertion_size_logic[unfolded o_def])
apply (simp add: flex_user_data_at_rf_sr_dom_s)
apply (clarsimp simp: field_simps word_size_def mapM_x_storeWord_step)
apply (simp add: doMachineOp_def split_def exec_gets)
apply (simp add: select_f_def simpler_modify_def bind_def)
apply (fold replicateHider_def)[1]
apply (subst coerce_heap_update_to_heap_updates'
[where chunk=4096 and m="2 ^ (pageBitsForSize sz - pageBits)"])
apply (simp add: pageBitsForSize_def pageBits_def
split: vmpage_size.split)
apply (subst coerce_memset_to_heap_update_user_data)
apply (subgoal_tac "\<forall>p<2 ^ (pageBitsForSize sz - pageBits).
x \<Turnstile>\<^sub>c (Ptr (ptr + of_nat p * 0x1000) :: user_data_C ptr)")
prefer 2
apply (erule allfEI[where f=of_nat])
apply clarsimp
apply (subst(asm) of_nat_power, assumption)
apply simp
apply (insert pageBitsForSize_32 [of sz])[1]
apply (erule order_le_less_trans [rotated])
apply simp
apply (simp, drule ko_at_projectKO_opt[OF user_data_at_ko])
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def cpspace_relation_def)
apply (erule cmap_relationE1, simp(no_asm) add: heap_to_user_data_def Let_def)
apply fastforce
subgoal by (simp add: pageBits_def typ_heap_simps)
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def)
apply (clarsimp simp: cpspace_relation_def typ_heap_simps
clift_foldl_hrs_mem_update foldl_id
carch_state_relation_def
cmachine_state_relation_def
foldl_fun_upd_const[unfolded fun_upd_def]
power_user_page_foldl_zero_ranges
dom_heap_to_device_data)
apply (rule conjI[rotated])
apply (simp add:pageBitsForSize_mess_multi)
apply (rule cmap_relationI)
apply (clarsimp simp: dom_heap_to_device_data cmap_relation_def)
apply (simp add:cuser_user_data_device_relation_def)
apply (subst help_force_intvl_range_conv, assumption)
subgoal by (simp add: pageBitsForSize_def split: vmpage_size.split)
apply assumption
apply (subst heap_to_user_data_update_region)
apply (drule map_to_user_data_aligned, clarsimp)
apply (rule aligned_range_offset_mem[where m=pageBits], simp_all)[1]
apply (rule pbfs_atleast_pageBits)
apply (erule cmap_relation_If_upd)
apply (clarsimp simp: cuser_user_data_relation_def fcp_beta
order_less_le_trans[OF unat_lt2p])
apply (fold word_rsplit_0, simp add: word_rcat_rsplit)[1]
apply (rule image_cong[OF _ refl])
apply (rule set_eqI, rule iffI)
apply (clarsimp simp del: atLeastAtMost_iff)
apply (drule map_to_user_data_aligned, clarsimp)
apply (simp only: mask_in_range[symmetric])
apply (rule_tac x="unat ((xa && mask (pageBitsForSize sz)) >> pageBits)" in image_eqI)
apply (simp add: subtract_mask(2)[symmetric])
apply (cut_tac w="xa - ptr" and n=pageBits in and_not_mask[symmetric])
apply (simp add: shiftl_t2n field_simps pageBits_def)
apply (subst is_aligned_neg_mask_eq, simp_all)[1]
apply (erule aligned_sub_aligned, simp_all add: word_bits_def)[1]
apply (erule is_aligned_weaken)
apply (rule pbfs_atleast_pageBits[unfolded pageBits_def])
apply simp
apply (rule unat_less_power)
apply (fold word_bits_def, simp)
apply (rule shiftr_less_t2n)
apply (simp add: pbfs_atleast_pageBits)
apply (rule and_mask_less_size)
apply (simp add: word_bits_def word_size)
apply (rule IntI)
apply (clarsimp simp del: atLeastAtMost_iff)
apply (subst aligned_range_offset_mem, assumption, simp_all)[1]
apply (rule order_le_less_trans[rotated], erule shiftl_less_t2n [OF of_nat_power],
simp_all add: word_bits_def)[1]
apply (insert pageBitsForSize_32 [of sz])[1]
apply (erule order_le_less_trans [rotated])
subgoal by simp
subgoal by (simp add: pageBits_def shiftl_t2n field_simps)
apply clarsimp
apply (drule_tac x="of_nat n" in spec)
apply (simp add: of_nat_power[where 'a=32, folded word_bits_def])
apply (rule exI)
subgoal by (simp add: pageBits_def ko_at_projectKO_opt[OF user_data_at_ko])
subgoal by simp
apply csymbr
apply (ctac add: cleanCacheRange_PoU_ccorres[unfolded dc_def])
apply wp
apply (simp add: guard_is_UNIV_def unat_of_nat
word_bits_def capAligned_def word_of_nat_less)
apply (clarsimp simp: word_bits_def valid_cap'_def
capAligned_def word_of_nat_less)
apply (frule is_aligned_addrFromPPtr_n, simp add: pageBitsForSize_def split: vmpage_size.splits)
by (clarsimp simp: is_aligned_no_overflow'[where n=12, simplified]
is_aligned_no_overflow'[where n=16, simplified]
is_aligned_no_overflow'[where n=20, simplified]
is_aligned_no_overflow'[where n=24, simplified] pageBits_def
field_simps is_aligned_mask[symmetric] mask_AND_less_0
pageBitsForSize_def split: vmpage_size.splits)
lemma coerce_memset_to_heap_update_asidpool:
"heap_update_list x (replicateHider 4096 0)
= heap_update (Ptr x :: asid_pool_C ptr)
(asid_pool_C (FCP (\<lambda>x. Ptr 0)))"
apply (intro ext, simp add: heap_update_def)
apply (rule_tac f="\<lambda>xs. heap_update_list x xs a b" for a b in arg_cong)
apply (simp add: to_bytes_def size_of_def typ_info_simps asid_pool_C_tag_def)
apply (simp add: ti_typ_pad_combine_empty_ti ti_typ_pad_combine_td align_of_def padup_def
final_pad_def size_td_lt_ti_typ_pad_combine Let_def size_of_def)
apply (simp add: typ_info_simps
user_context_C_tag_def thread_state_C_tag_def seL4_Fault_C_tag_def
lookup_fault_C_tag_def update_ti_t_ptr_0s
ti_typ_pad_combine_empty_ti ti_typ_pad_combine_td
ti_typ_combine_empty_ti ti_typ_combine_td
align_of_def padup_def
final_pad_def size_td_lt_ti_typ_pad_combine Let_def size_of_def
align_td_array' size_td_array)
apply (simp add: typ_info_array')
apply (subst access_ti_list_array)
apply simp
apply simp
apply (simp add: fcp_beta typ_info_word typ_info_ptr word_rsplit_0)
apply fastforce
apply (simp add: collapse_foldl_replicate)
done
declare replicate_numeral [simp]
lemma coerce_memset_to_heap_update_pte:
@ -426,20 +216,6 @@ lemma coerce_memset_to_heap_update_pte:
apply (simp add: replicateHider_def)
done
lemma coerce_memset_to_heap_update_pde:
"heap_update_list x (replicateHider 4 0)
= heap_update (Ptr x :: pde_C ptr)
(pde_C.pde_C (FCP (\<lambda>x. 0)))"
apply (intro ext, simp add: heap_update_def)
apply (rule_tac f="\<lambda>xs. heap_update_list x xs a b" for a b in arg_cong)
apply (simp add: to_bytes_def size_of_def typ_info_simps pde_C_tag_def)
apply (simp add: ti_typ_pad_combine_empty_ti ti_typ_pad_combine_td align_of_def padup_def
final_pad_def size_td_lt_ti_typ_pad_combine Let_def size_of_def)
apply (simp add: typ_info_simps align_td_array' size_td_array)
apply (simp add: typ_info_array' typ_info_word word_rsplit_0)
apply (simp add: replicateHider_def)
done
lemma objBits_eq_by_type:
fixes x :: "'a :: pspace_storable" and y :: 'a
shows "objBits x = objBits y"
@ -541,16 +317,6 @@ lemma invalidateTLBByASID_ccorres:
apply (clarsimp simp: pde_stored_asid_def to_bool_def)
done
(* FIXME: also in VSpace_C *)
lemma ignoreFailure_liftM:
"ignoreFailure = liftM (\<lambda>v. ())"
apply (rule ext)+
apply (simp add: ignoreFailure_def liftM_def
catch_def)
apply (rule bind_apply_cong[OF refl])
apply (simp split: sum.split)
done
end
lemma option_to_0_user_mem':
@ -620,25 +386,6 @@ lemma page_table_at_rf_sr_dom_s:
apply (auto simp add: intvl_def shiftl_t2n)[1]
done
lemma page_directory_at_rf_sr_dom_s:
"\<lbrakk> page_directory_at' x s; (s, s') \<in> rf_sr \<rbrakk>
\<Longrightarrow> {x ..+ 2 ^ pdBits} \<times> {SIndexVal, SIndexTyp 0}
\<subseteq> dom_s (hrs_htd (t_hrs_' (globals s')))"
apply (rule_tac m=2 in intvl_2_power_times_decomp,
simp_all add: shiftl_t2n field_simps pdBits_def pageBits_def
word_bits_def pdeBits_def)
apply (clarsimp simp: page_directory_at'_def intvl_def)
apply (drule spec, drule(1) mp)
apply (simp add: typ_at_to_obj_at_arches)
apply (drule obj_at_ko_at', clarsimp)
apply (erule cmap_relationE1[OF rf_sr_cpde_relation])
apply (erule ko_at_projectKO_opt)
apply (drule h_t_valid_clift)
apply (drule h_t_valid_dom_s[OF _ refl refl])
apply (erule subsetD)
apply (auto simp add: intvl_def shiftl_t2n)[1]
done
lemma clearMemory_setObject_PTE_ccorres:
"ccorres dc xfdc (page_table_at' ptr
and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)
@ -699,66 +446,6 @@ lemma clearMemory_setObject_PTE_ccorres:
field_simps is_aligned_mask[symmetric] mask_AND_less_0)
done
lemma ccorres_make_xfdc:
"ccorresG rf_sr \<Gamma> r xf P P' h a c \<Longrightarrow> ccorresG rf_sr \<Gamma> dc xfdc P P' h a c"
apply (erule ccorres_rel_imp)
apply simp
done
lemma ccorres_if_True_False_simps:
"ccorres r xf P P' hs a (IF True THEN c ELSE c' FI) = ccorres r xf P P' hs a c"
"ccorres r xf P P' hs a (IF False THEN c ELSE c' FI) = ccorres r xf P P' hs a c'"
"ccorres r xf P P' hs a (IF True THEN c ELSE c' FI ;; d) = ccorres r xf P P' hs a (c ;; d)"
"ccorres r xf P P' hs a (IF False THEN c ELSE c' FI ;; d) = ccorres r xf P P' hs a (c' ;; d)"
by (simp_all add: ccorres_cond_iffs ccorres_seq_simps)
lemmas cap_tag_values =
cap_untyped_cap_def
cap_endpoint_cap_def
cap_notification_cap_def
cap_reply_cap_def
cap_cnode_cap_def
cap_thread_cap_def
cap_irq_handler_cap_def
cap_null_cap_def
cap_irq_control_cap_def
cap_zombie_cap_def
cap_small_frame_cap_def
cap_frame_cap_def
cap_page_table_cap_def
cap_page_directory_cap_def
cap_asid_pool_cap_def
lemma ccorres_return_C_seq:
"\<lbrakk>\<And>s f. xf (global_exn_var_'_update f (xfu (\<lambda>_. v s) s)) = v s; \<And>s f. globals (xfu f s) = globals s; wfhandlers hs\<rbrakk>
\<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r rvxf arrel xf (\<lambda>_. True) {s. arrel rv (v s)} hs (return rv) (return_C xfu v ;; d)"
apply (rule ccorres_guard_imp)
apply (rule ccorres_split_throws, rule ccorres_return_C, simp+)
apply vcg
apply simp_all
done
lemma ccap_relation_VPIsDevice:
"\<lbrakk>isPageCap cp; ccap_relation (ArchObjectCap cp) cap \<rbrakk> \<Longrightarrow>
(generic_frame_cap_get_capFIsDevice_CL (cap_lift cap) = 0) = (\<not> (capVPIsDevice cp))"
by (clarsimp elim!:ccap_relationE
simp : isPageCap_def generic_frame_cap_get_capFIsDevice_CL_def cap_to_H_def
Let_def to_bool_def
split: arch_capability.split_asm cap_CL.split_asm if_split_asm)
lemma ccap_relation_get_capZombiePtr_CL:
"\<lbrakk> ccap_relation cap cap'; isZombie cap; capAligned cap \<rbrakk>
\<Longrightarrow> get_capZombiePtr_CL (cap_zombie_cap_lift cap') = capZombiePtr cap"
apply (simp only: cap_get_tag_isCap[symmetric])
apply (drule(1) cap_get_tag_to_H)
apply (clarsimp simp: get_capZombiePtr_CL_def get_capZombieBits_CL_def Let_def split: if_split)
apply (subst less_mask_eq)
apply (clarsimp simp add: capAligned_def objBits_simps word_bits_conv)
apply unat_arith
apply simp
done
lemma modify_gets_helper:
"do y \<leftarrow> modify (ksPSpace_update (\<lambda>_. ps)); ps' \<leftarrow> gets ksPSpace; f ps' od
= do y \<leftarrow> modify (ksPSpace_update (\<lambda>_. ps)); f ps od"
@ -789,19 +476,6 @@ lemma double_setEndpoint:
apply (simp add: bind_def simpler_modify_def)
done
lemma filterM_setEndpoint_adjustment:
"\<lbrakk> \<And>v. do setEndpoint epptr IdleEP; body v od
= do v' \<leftarrow> body v; setEndpoint epptr IdleEP; return v' od \<rbrakk>
\<Longrightarrow>
(do q' \<leftarrow> filterM body q; setEndpoint epptr (f q') od)
= (do setEndpoint epptr IdleEP; q' \<leftarrow> filterM body q; setEndpoint epptr (f q') od)"
apply (rule sym)
apply (induct q arbitrary: f)
apply (simp add: double_setEndpoint)
apply (simp add: bind_assoc)
apply (subst bind_assoc[symmetric], simp, simp add: bind_assoc)
done
lemma ccorres_inst_voodoo:
"\<forall>x. ccorres r xf (P x) (P' x) hs (h x) (c x)
\<Longrightarrow> \<forall>x. ccorres r xf (P x) (P' x) hs (h x) (c x)"
@ -838,17 +512,6 @@ crunch ep_obj_at'[wp]: setThreadState "obj_at' (P :: endpoint \<Rightarrow> bool
context kernel_m begin
lemma ccorres_abstract_h_val:
"(\<And>rv. P rv \<Longrightarrow> ccorres r xf G (G' rv) hs a c) \<Longrightarrow>
ccorres r xf G ({s. P (h_val (hrs_mem (t_hrs_' (globals s))) p)
\<longrightarrow> s \<in> G' (h_val (hrs_mem (t_hrs_' (globals s)))
p)}
\<inter> {s. P (h_val (hrs_mem (t_hrs_' (globals s))) p)}) hs a c"
apply (rule ccorres_tmp_lift1 [where P = P])
apply (clarsimp simp: Collect_conj_eq [symmetric])
apply (fastforce intro: ccorres_guard_imp)
done
lemma ccorres_subst_basic_helper:
"\<lbrakk> \<And>s s'. \<lbrakk> P s; s' \<in> P'; (s, s') \<in> rf_sr \<rbrakk> \<Longrightarrow> f s' = f' s';
\<And>s s'. \<lbrakk> P s; s' \<in> P'; (s, s') \<in> rf_sr \<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr;
@ -1214,44 +877,6 @@ lemma cancelBadgedSends_ccorres:
by (auto simp: obj_at'_def projectKOs state_refs_of'_def pred_tcb_at'_def tcb_bound_refs'_def
dest!: symreftype_inverse')
lemma tcb_ptr_to_ctcb_ptr_force_fold:
"x + 2 ^ ctcb_size_bits = ptr_val (tcb_ptr_to_ctcb_ptr x)"
by (simp add: tcb_ptr_to_ctcb_ptr_def ctcb_offset_def)
lemma coerce_memset_to_heap_update:
"heap_update_list x (replicateHider (size_of (TYPE (tcb_C))) 0)
= heap_update (tcb_Ptr x)
(tcb_C (arch_tcb_C (user_context_C (FCP (\<lambda>x. 0))))
(thread_state_C (FCP (\<lambda>x. 0)))
(NULL)
(seL4_Fault_C (FCP (\<lambda>x. 0)))
(lookup_fault_C (FCP (\<lambda>x. 0)))
0 0 0 0 0 0 NULL NULL NULL NULL)"
apply (intro ext, simp add: heap_update_def)
apply (rule_tac f="\<lambda>xs. heap_update_list x xs a b" for a b in arg_cong)
apply (simp add: to_bytes_def size_of_def typ_info_simps tcb_C_tag_def)
apply (simp add: ti_typ_pad_combine_empty_ti ti_typ_pad_combine_td align_of_def padup_def
final_pad_def size_td_lt_ti_typ_pad_combine Let_def size_of_def)
apply (simp add: typ_info_simps
user_context_C_tag_def thread_state_C_tag_def seL4_Fault_C_tag_def
lookup_fault_C_tag_def update_ti_t_ptr_0s arch_tcb_C_tag_def
ti_typ_pad_combine_empty_ti ti_typ_pad_combine_td
ti_typ_combine_empty_ti ti_typ_combine_td
align_of_def padup_def
final_pad_def size_td_lt_ti_typ_pad_combine Let_def size_of_def
align_td_array' size_td_array)
apply (simp add: typ_info_array')
apply (simp add: typ_info_word word_rsplit_0 upt_conv_Cons)
apply (simp add: typ_info_word typ_info_ptr word_rsplit_0
replicateHider_def)
done
lemma isArchObjectCap_capBits:
"isArchObjectCap cap \<Longrightarrow> capBits cap = acapBits (capCap cap)"
by (clarsimp simp: isCap_simps)
declare Kernel_C.tcb_C_size [simp del]
lemma cte_lift_ccte_relation:
@ -1341,14 +966,6 @@ lemma updateFreeIndex_ccorres:
end
(* FIXME: Move *)
lemma ccap_relation_isDeviceCap:
"\<lbrakk>ccap_relation cp cap; isUntypedCap cp
\<rbrakk> \<Longrightarrow> to_bool (capIsDevice_CL (cap_untyped_cap_lift cap)) = (capIsDevice cp)"
apply (frule cap_get_tag_UntypedCap)
apply (simp add:cap_get_tag_isCap )
done
lemma ccap_relation_isDeviceCap2:
"\<lbrakk>ccap_relation cp cap; isUntypedCap cp
\<rbrakk> \<Longrightarrow> (capIsDevice_CL (cap_untyped_cap_lift cap) = 0) = (\<not> (capIsDevice cp))"

File diff suppressed because it is too large Load Diff

View File

@ -371,13 +371,6 @@ lemma tcb_cte_cases_proj_eq [simp]:
unfolding tcb_no_ctes_proj_def tcb_cte_cases_def
by (auto split: if_split_asm)
lemma map_to_ctes_upd_cte':
"\<lbrakk> ksPSpace s p = Some (KOCTE cte'); is_aligned p cte_level_bits; ps_clear p cte_level_bits s \<rbrakk>
\<Longrightarrow> map_to_ctes (ksPSpace s(p |-> KOCTE cte)) = (map_to_ctes (ksPSpace s))(p |-> cte)"
apply (erule (1) map_to_ctes_upd_cte)
apply (simp add: field_simps ps_clear_def3 cte_level_bits_def mask_def)
done
lemma map_to_ctes_upd_tcb':
"[| ksPSpace s p = Some (KOTCB tcb'); is_aligned p tcbBlockSizeBits;
ps_clear p tcbBlockSizeBits s |]
@ -392,12 +385,6 @@ lemma map_to_ctes_upd_tcb':
apply (simp add: field_simps ps_clear_def3 mask_def objBits_defs)
done
lemma tcb_cte_cases_inv [simp]:
"tcb_cte_cases p = Some (getF, setF) \<Longrightarrow> getF (setF (\<lambda>_. v) tcb) = v"
unfolding tcb_cte_cases_def
by (simp split: if_split_asm)
declare insert_dom [simp]
lemma in_alignCheck':
@ -720,17 +707,6 @@ proof (rule cor_map_relI [OF map_option_eq_dom_eq])
by auto
qed fact+
lemma lifth_update:
"clift (t_hrs_' s) ptr = clift (t_hrs_' s') ptr
\<Longrightarrow> lifth ptr s = lifth ptr s'"
unfolding lifth_def
by simp
lemma getCTE_exs_valid:
"cte_at' dest s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getCTE dest \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>"
unfolding exs_valid_def getCTE_def cte_wp_at'_def
by clarsimp
lemma cmap_domE1:
"\<lbrakk> f ` dom am = dom cm; am x = Some v; \<And>v'. cm (f x) = Some v' \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
apply (drule equalityD1)
@ -970,9 +946,6 @@ declare is_aligned_0 [simp]
abbreviation
"nullCapPointers cte \<equiv> cteCap cte = NullCap \<and> mdbNext (cteMDBNode cte) = nullPointer \<and> mdbPrev (cteMDBNode cte) = nullPointer"
lemma nullCapPointers_def:
"is_an_abbreviation" unfolding is_an_abbreviation_def by simp
lemma valid_mdb_ctes_of_next:
"\<lbrakk> valid_mdb' s; ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0 \<rbrakk> \<Longrightarrow> cte_at' (mdbNext (cteMDBNode cte)) s"
unfolding valid_mdb'_def valid_mdb_ctes_def
@ -1164,43 +1137,6 @@ lemma rf_sr_upd_safe[simp]:
shows "((a, (g y)) \<in> rf_sr) = ((a, y) \<in> rf_sr)"
using rl rq rqL1 rqL2 sa ct it isn ist arch wu gs dsi cdom dt by - (rule rf_sr_upd)
(* More of a well-formed lemma, but \<dots> *)
lemma valid_mdb_cslift_next:
assumes vmdb: "valid_mdb' s"
and sr: "(s, s') \<in> rf_sr"
and cof: "ctes_of s p = Some cte"
and nz: "mdbNext (cteMDBNode cte) \<noteq> 0"
shows "cslift s' (Ptr (mdbNext (cteMDBNode cte)) :: cte_C ptr) \<noteq> None"
proof -
from vmdb cof nz obtain cten where
"ctes_of s (mdbNext (cteMDBNode cte)) = Some cten"
by (auto simp: cte_wp_at_ctes_of dest!: valid_mdb_ctes_of_next)
with sr show ?thesis
apply -
apply (drule (1) rf_sr_ctes_of_clift)
apply clarsimp
done
qed
lemma valid_mdb_cslift_prev:
assumes vmdb: "valid_mdb' s"
and sr: "(s, s') \<in> rf_sr"
and cof: "ctes_of s p = Some cte"
and nz: "mdbPrev (cteMDBNode cte) \<noteq> 0"
shows "cslift s' (Ptr (mdbPrev (cteMDBNode cte)) :: cte_C ptr) \<noteq> None"
proof -
from vmdb cof nz obtain cten where
"ctes_of s (mdbPrev (cteMDBNode cte)) = Some cten"
by (auto simp: cte_wp_at_ctes_of dest!: valid_mdb_ctes_of_prev)
with sr show ?thesis
apply -
apply (drule (1) rf_sr_ctes_of_clift)
apply clarsimp
done
qed
lemma rf_sr_cte_at_valid:
"\<lbrakk> cte_wp_at' P (ptr_val p) s; (s,s') \<in> rf_sr \<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c (p :: cte_C ptr)"
apply (clarsimp simp: cte_wp_at_ctes_of)
@ -1776,15 +1712,6 @@ definition
to_bool (capAllowRead_CL cr) = wd !! 1 \<and>
to_bool (capAllowWrite_CL cr) = wd !! 0"
lemma cap_rights_to_H_from_word [simp]:
"cap_rights_to_H (cap_rights_from_word wd) = rightsFromWord wd"
unfolding cap_rights_from_word_def rightsFromWord_def
apply (rule someI2_ex)
apply (rule exI [where x = "cap_rights_from_word_canon wd"])
apply (simp add: cap_rights_from_word_canon_def)
apply (simp add: cap_rights_to_H_def)
done
lemma small_frame_cap_is_mapped_alt:
"cap_get_tag cp = scast cap_small_frame_cap \<Longrightarrow>
(cap_small_frame_cap_CL.capFMappedASIDHigh_CL (cap_small_frame_cap_lift cp) = 0
@ -2138,17 +2065,6 @@ lemma gs_set_assn_Delete_cstate_relation:
cteDeleteOne_'proc_def cap_get_capSizeBits_'proc_def)
done
lemma update_typ_at:
assumes at: "obj_at' P p s"
and tp: "\<forall>obj. P obj \<longrightarrow> koTypeOf (injectKOS obj) = koTypeOf ko"
shows "typ_at' T p' (s \<lparr>ksPSpace := ksPSpace s(p \<mapsto> ko)\<rparr>) = typ_at' T p' s"
using at
by (auto elim!: obj_atE' simp: typ_at'_def ko_wp_at'_def
dest!: tp[rule_format]
simp: project_inject projectKO_eq split: kernel_object.splits if_split_asm,
simp_all add: objBits_def objBitsT_koTypeOf[symmetric] ps_clear_upd
del: objBitsT_koTypeOf)
lemma ptr_val_tcb_ptr_mask:
"obj_at' (P :: tcb \<Rightarrow> bool) thread s
\<Longrightarrow> ptr_val (tcb_ptr_to_ctcb_ptr thread) && (~~ mask tcbBlockSizeBits)

View File

@ -192,23 +192,6 @@ lemma activateThread_ccorres:
apply (clarsimp simp: typ_heap_simps ThreadState_Running_def mask_def)
done
lemma ceqv_Guard_UNIV_Skip:
"ceqv Gamma xf v s s' (a ;; Guard F UNIV Skip) a"
apply (rule ceqvI)
apply (safe elim!: exec_Normal_elim_cases)
apply (case_tac s'a, auto intro: exec.intros elim!: exec_Normal_elim_cases)[1]
apply (cases s', auto intro: exec.intros)
done
lemma ceqv_tail_Guard_onto_Skip:
"ceqv Gamma xf v s s'
(a ;; Guard F G b) ((a ;; Guard F G Skip) ;; b)"
apply (rule ceqvI)
apply (safe elim!: exec_Normal_elim_cases)
apply (case_tac s'a, auto intro: exec.intros elim!: exec_Normal_elim_cases)[1]
apply (case_tac s'aa, auto intro: exec.intros elim!: exec_Normal_elim_cases)[1]
done
lemma ceqv_remove_tail_Guard_Skip:
"\<lbrakk> \<And>s. s \<in> G \<rbrakk> \<Longrightarrow> ceqv Gamma xf v s s' (a ;; Guard F G Skip) a"
apply (rule ceqvI)
@ -217,9 +200,6 @@ lemma ceqv_remove_tail_Guard_Skip:
apply (case_tac s', auto intro: exec.intros elim!: exec_Normal_elim_cases)[1]
done
lemmas ccorres_remove_tail_Guard_Skip
= ccorres_abstract[where xf'="\<lambda>_. ()", OF ceqv_remove_tail_Guard_Skip]
lemma queue_in_range_pre:
"\<lbrakk> (qdom :: word32) \<le> ucast maxDom; prio \<le> ucast maxPrio \<rbrakk>
\<Longrightarrow> qdom * of_nat numPriorities + prio < of_nat (numDomains * numPriorities)"
@ -227,8 +207,6 @@ lemma queue_in_range_pre:
word_le_nat_alt unat_ucast maxDom_def seL4_MaxPrio_def
numPriorities_def unat_word_ariths numDomains_def)
lemmas queue_in_range' = queue_in_range_pre[unfolded numDomains_def numPriorities_def, simplified]
lemma switchToThread_ccorres':
"ccorres (\<lambda>_ _. True) xfdc
(all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' t)
@ -246,7 +224,6 @@ lemma chooseThread_ccorres:
proof -
note prio_and_dom_limit_helpers [simp]
note ksReadyQueuesL2Bitmap_nonzeroI [simp]
note Collect_const_mem [simp]
have invs_no_cicd'_max_CurDomain[intro]:
@ -317,11 +294,6 @@ proof -
done
qed
lemma ksDomSched_length_relation[simp]:
"\<lbrakk>cstate_relation s s'\<rbrakk> \<Longrightarrow> length (kernel_state.ksDomSchedule s) = unat (ksDomScheduleLength)"
apply (auto simp: cstate_relation_def cdom_schedule_relation_def Let_def ksDomScheduleLength_def)
done
lemma ksDomSched_length_dom_relation[simp]:
"\<lbrakk>cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule \<rbrakk> \<Longrightarrow> length (kernel_state.ksDomSchedule s) = unat (ksDomScheduleLength)"
apply (auto simp: cstate_relation_def cdom_schedule_relation_def Let_def ksDomScheduleLength_def)

View File

@ -202,10 +202,6 @@ where
"ccte_relation acte ccte \<equiv> Some acte = option_map cte_to_H (cte_lift ccte)
\<and> c_valid_cte ccte"
lemma ccte_relation_c_valid_cte: "ccte_relation c c' \<Longrightarrow> c_valid_cte c'"
by (simp add: ccte_relation_def)
definition
tcb_queue_relation' :: "(tcb_C \<Rightarrow> tcb_C ptr) \<Rightarrow> (tcb_C \<Rightarrow> tcb_C ptr) \<Rightarrow> (tcb_C ptr \<Rightarrow> tcb_C option) \<Rightarrow> word32 list \<Rightarrow> tcb_C ptr \<Rightarrow> tcb_C ptr \<Rightarrow> bool"
where
@ -281,10 +277,6 @@ definition "is_cap_fault cf \<equiv>
(case cf of (SeL4_Fault_CapFault _) \<Rightarrow> True
| _ \<Rightarrow> False)"
lemma is_cap_fault_simp: "is_cap_fault cf = (\<exists> x. cf=SeL4_Fault_CapFault x)"
by (simp add: is_cap_fault_def split:seL4_Fault_CL.splits)
definition
message_info_to_H :: "seL4_MessageInfo_C \<Rightarrow> Types_H.message_info"
where
@ -494,22 +486,6 @@ where
XN_CL = of_bool xn
\<rparr>))"
(* Invalid PTEs map to large PTEs with reserved bit 0 *)
lemma pte_0:
"index (pte_C.words_C cpte) 0 = 0 \<Longrightarrow> pte_lift cpte = Some (Pte_pte_large
\<lparr> pte_pte_large_CL.address_CL = 0,
XN_CL = 0,
TEX_CL = 0,
nG_CL = 0,
S_CL = 0,
APX_CL = 0,
AP_CL = 0,
C_CL = 0,
B_CL = 0,
reserved_CL = 0
\<rparr>)"
by (simp add: pte_lift_def pte_get_tag_def pte_pte_large_def)
definition
casid_pool_relation :: "asidpool \<Rightarrow> asid_pool_C \<Rightarrow> bool"
where
@ -878,28 +854,6 @@ definition
definition
"ccap_rights_relation cr cr' \<equiv> cr = cap_rights_to_H (seL4_CapRights_lift cr')"
lemma (in kernel) syscall_error_to_H_cases_rev:
"\<And>n. syscall_error_to_H e lf = Some (InvalidArgument n) \<Longrightarrow>
type_C e = scast seL4_InvalidArgument"
"\<And>n. syscall_error_to_H e lf = Some (InvalidCapability n) \<Longrightarrow>
type_C e = scast seL4_InvalidCapability"
"syscall_error_to_H e lf = Some IllegalOperation \<Longrightarrow>
type_C e = scast seL4_IllegalOperation"
"\<And>w1 w2. syscall_error_to_H e lf = Some (RangeError w1 w2) \<Longrightarrow>
type_C e = scast seL4_RangeError"
"syscall_error_to_H e lf = Some AlignmentError \<Longrightarrow>
type_C e = scast seL4_AlignmentError"
"\<And>b lf'. syscall_error_to_H e lf = Some (FailedLookup b lf') \<Longrightarrow>
type_C e = scast seL4_FailedLookup"
"syscall_error_to_H e lf = Some TruncatedMessage \<Longrightarrow>
type_C e = scast seL4_TruncatedMessage"
"syscall_error_to_H e lf = Some DeleteFirst \<Longrightarrow>
type_C e = scast seL4_DeleteFirst"
"syscall_error_to_H e lf = Some RevokeFirst \<Longrightarrow>
type_C e = scast seL4_RevokeFirst"
by (clarsimp simp: syscall_error_to_H_def syscall_error_type_defs
split: if_split_asm)+
definition
syscall_from_H :: "syscall \<Rightarrow> word32"
where

View File

@ -534,15 +534,6 @@ lemma ccorres_injection_handler_csum1:
apply (auto split: sum.split)
done
lemma ccorres_injection_handler_csum2:
"ccorres ((f o injector) \<currency> r) xf P P' hs a c
\<Longrightarrow> ccorres (f \<currency> r) xf P P' hs
(injection_handler injector a) c"
apply (simp add: injection_handler_liftM)
apply (erule ccorres_rel_imp)
apply (auto split: sum.split)
done
definition
is_nondet_refinement :: "('a, 's) nondet_monad
\<Rightarrow> ('a, 's) nondet_monad \<Rightarrow> bool"
@ -607,13 +598,6 @@ lemma ccorres_defer:
apply fastforce
done
lemma no_fail_loadWordUser:
"no_fail (pointerInUserData x and K (is_aligned x 2)) (loadWordUser x)"
apply (simp add: loadWordUser_def)
apply (rule no_fail_pre, wp no_fail_stateAssert)
apply simp
done
lemma no_fail_getMRs:
"no_fail (tcb_at' thread and case_option \<top> valid_ipc_buffer_ptr' buffer)
(getMRs thread buffer info)"
@ -621,14 +605,6 @@ lemma no_fail_getMRs:
apply (rule det_wp_getMRs)
done
lemma msgRegisters_scast:
"n < unat (scast n_msgRegisters :: word32) \<Longrightarrow>
unat (scast (index msgRegistersC n)::word32) = unat (index msgRegistersC n)"
apply (simp add: msgRegisters_def fupdate_def update_def n_msgRegisters_def fcp_beta
Kernel_C.R2_def Kernel_C.R3_def Kernel_C.R4_def Kernel_C.R5_def
Kernel_C.R6_def Kernel_C.R7_def)
done
lemma msgRegisters_ccorres:
"n < unat n_msgRegisters \<Longrightarrow>
register_from_H (ARM_H.msgRegisters ! n) = (index msgRegistersC n)"
@ -786,11 +762,6 @@ lemma capFVMRights_range:
lemma dumb_bool_for_all: "(\<forall>x. x) = False"
by auto
lemma dumb_bool_split_for_vcg:
"\<lbrace>d \<longrightarrow> \<acute>ret__unsigned_long \<noteq> 0\<rbrace> \<inter> \<lbrace>\<not> d \<longrightarrow> \<acute>ret__unsigned_long = 0\<rbrace>
= \<lbrace>d = to_bool \<acute>ret__unsigned_long \<rbrace>"
by (auto simp: to_bool_def)
lemma ccap_relation_page_is_device:
"ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d v0a v1 v2 v3)) c
\<Longrightarrow> (generic_frame_cap_get_capFIsDevice_CL (cap_lift c) \<noteq> 0) = d"
@ -986,11 +957,6 @@ lemma lookupIPCBuffer_ccorres[corres]:
size_of_def)
done
lemma doMachineOp_pointerInUserData:
"\<lbrace>pointerInUserData p\<rbrace> doMachineOp m \<lbrace>\<lambda>rv. pointerInUserData p\<rbrace>"
by (simp add: pointerInUserData_def) wp
lemma loadWordUser_wp:
"\<lbrace>\<lambda>s. is_aligned p 2 \<and> (\<forall>v. user_word_at v p s \<longrightarrow> P v s)\<rbrace>
loadWordUser p
@ -1254,7 +1220,7 @@ lemma getSyscallArg_ccorres_foo:
apply (rule conseqPre, vcg)
apply (clarsimp simp: rf_sr_ksCurThread)
apply (drule (1) obj_at_cslift_tcb)
apply (clarsimp simp: typ_heap_simps' msgRegisters_scast)
apply (clarsimp simp: typ_heap_simps')
apply (clarsimp simp: ctcb_relation_def ccontext_relation_def
msgRegisters_ccorres atcbContextGet_def
carch_tcb_relation_def)

View File

@ -26,12 +26,6 @@ context kernel_m begin
(* FIXME: should do this from the beginning *)
declare true_def [simp] false_def [simp]
lemma ccorres_If_False:
"ccorres_underlying sr Gamm r xf arrel axf R R' hs b c
\<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf
(R and (\<lambda>_. \<not> P)) R' hs (If P a b) c"
by (rule ccorres_gen_asm, simp)
definition
one_on_true :: "bool \<Rightarrow> nat"
where
@ -339,14 +333,6 @@ lemma decodeInvocation_ccorres:
mask_eq_iff_w2p[THEN trans[OF eq_commute]])+
done
lemma ccorres_Call_Seq:
"\<lbrakk> \<Gamma> f = Some v; ccorres r xf P P' hs a (v ;; c) \<rbrakk>
\<Longrightarrow> ccorres r xf P P' hs a (Call f ;; c)"
apply (erule ccorres_semantic_equivD1)
apply (rule semantic_equivI)
apply (auto elim!: exec_elim_cases intro: exec.intros)
done
lemma wordFromRights_mask_0:
"wordFromRights rghts && ~~ mask 4 = 0"
apply (simp add: wordFromRights_def word_ao_dist word_or_zero
@ -354,13 +340,6 @@ lemma wordFromRights_mask_0:
apply (simp add: mask_def split: if_split)
done
lemma wordFromRights_mask_eq:
"wordFromRights rghts && mask 4 = wordFromRights rghts"
apply (cut_tac x="wordFromRights rghts" and y="mask 4" and z="~~ mask 4"
in word_bool_alg.conj_disj_distrib)
apply (simp add: wordFromRights_mask_0)
done
lemma loadWordUser_user_word_at:
"\<lbrace>\<lambda>s. \<forall>rv. user_word_at rv x s \<longrightarrow> Q rv s\<rbrace> loadWordUser x \<lbrace>Q\<rbrace>"
apply (simp add: loadWordUser_def user_word_at_def
@ -371,25 +350,6 @@ lemma loadWordUser_user_word_at:
is_aligned_mask)
done
lemma mapM_loadWordUser_user_words_at:
"\<lbrace>\<lambda>s. \<forall>rv. (\<forall>x < length xs. user_word_at (rv ! x) (xs ! x) s)
\<and> length rv = length xs \<longrightarrow> Q rv s\<rbrace>
mapM loadWordUser xs \<lbrace>Q\<rbrace>"
apply (induct xs arbitrary: Q)
apply (simp add: mapM_def sequence_def)
apply wp
apply (simp add: mapM_Cons)
apply wp
apply assumption
apply (wp loadWordUser_user_word_at)
apply clarsimp
apply (drule spec, erule mp)
apply clarsimp
apply (case_tac x)
apply simp
apply simp
done
lemma getSlotCap_slotcap_in_mem:
"\<lbrace>\<top>\<rbrace> getSlotCap slot \<lbrace>\<lambda>cap s. slotcap_in_mem cap slot (ctes_of s)\<rbrace>"
apply (simp add: getSlotCap_def)
@ -438,27 +398,6 @@ lemma messageInfoFromWord_spec:
Types_H.msgMaxExtraCaps_def shiftL_nat)
done
lemma threadGet_tcbIpcBuffer_ccorres [corres]:
"ccorres (=) w_bufferPtr_' (tcb_at' tptr) UNIV hs
(threadGet tcbIPCBuffer tptr)
(Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t (Ptr &(tcb_ptr_to_ctcb_ptr tptr\<rightarrow>
[''tcbIPCBuffer_C''])::word32 ptr)\<rbrace>
(\<acute>w_bufferPtr :==
h_val (hrs_mem \<acute>t_hrs)
(Ptr &(tcb_ptr_to_ctcb_ptr tptr\<rightarrow>[''tcbIPCBuffer_C''])::word32 ptr)))"
apply (rule ccorres_guard_imp2)
apply (rule ccorres_add_return2)
apply (rule ccorres_pre_threadGet)
apply (rule_tac P = "obj_at' (\<lambda>tcb. tcbIPCBuffer tcb = x) tptr" and
P'="{s'. \<exists>ctcb.
cslift s' (tcb_ptr_to_ctcb_ptr tptr) = Some ctcb \<and>
tcbIPCBuffer_C ctcb = x }" in ccorres_from_vcg)
apply (rule allI, rule conseqPre, vcg)
apply clarsimp
apply (clarsimp simp: return_def typ_heap_simps')
apply (clarsimp simp: obj_at'_def ctcb_relation_def)
done
lemma handleInvocation_def2:
"handleInvocation isCall isBlocking =
do thread \<leftarrow> getCurThread;
@ -770,19 +709,6 @@ lemma handleFault_ccorres:
apply (clarsimp simp: pred_tcb_at')
done
lemma getMessageInfo_less_4:
"\<lbrace>\<top>\<rbrace> getMessageInfo t \<lbrace>\<lambda>rv s. msgExtraCaps rv < 4\<rbrace>"
including no_pre
apply (simp add: getMessageInfo_def)
apply wp
apply (rule hoare_strengthen_post, rule hoare_vcg_prop)
apply (simp add: messageInfoFromWord_def Let_def
Types_H.msgExtraCapBits_def)
apply (rule minus_one_helper5, simp)
apply simp
apply (rule word_and_le1)
done
lemma invs_queues_imp:
"invs' s \<longrightarrow> valid_queues s"
by clarsimp
@ -1021,7 +947,7 @@ lemma handleInvocation_ccorres:
apply clarsimp
apply (vcg exspec= lookupCapAndSlot_modifies)
apply simp
apply (wp getMessageInfo_less_4 getMessageInfo_le3 getMessageInfo_msgLength')+
apply (wp getMessageInfo_le3 getMessageInfo_msgLength')+
apply (simp add: msgMaxLength_def, wp getMessageInfo_msgLength')[1]
apply simp
apply wp
@ -1233,56 +1159,15 @@ lemma capFaultOnFailure_if_case_sum:
>>= sum.case_sum (handleFault thread) return))"
by (case_tac c, clarsimp, clarsimp)
(* FIXME: MOVE to Corres_C.thy *)
lemma ccorres_trim_redundant_throw_break:
"\<lbrakk>ccorres_underlying rf_sr \<Gamma> arrel axf arrel axf G G' (SKIP # hs) a c;
\<And>s f. axf (global_exn_var_'_update f s) = axf s \<rbrakk>
\<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel axf G G' (SKIP # hs)
a (c;; Basic (global_exn_var_'_update (\<lambda>_. Break));; THROW)"
apply -
apply (rule ccorres_trim_redundant_throw')
apply simp
apply simp
apply simp
done
lemma invs_valid_objs_strengthen:
"invs' s \<longrightarrow> valid_objs' s" by fastforce
lemma ct_not_ksQ_strengthen:
"thread = ksCurThread s \<and> ksCurThread s \<notin> set (ksReadyQueues s p) \<longrightarrow> thread \<notin> set (ksReadyQueues s p)" by fastforce
lemma option_to_ctcb_ptr_valid_ntfn:
"valid_ntfn' ntfn s ==> (option_to_ctcb_ptr (ntfnBoundTCB ntfn) = NULL) = (ntfnBoundTCB ntfn = None)"
apply (cases "ntfnBoundTCB ntfn", simp_all add: option_to_ctcb_ptr_def)
apply (clarsimp simp: valid_ntfn'_def tcb_at_not_NULL)
done
lemma deleteCallerCap_valid_ntfn'[wp]:
"\<lbrace>\<lambda>s. valid_ntfn' x s\<rbrace> deleteCallerCap c \<lbrace>\<lambda>rv s. valid_ntfn' x s\<rbrace>"
apply (wp hoare_vcg_ex_lift hoare_vcg_all_lift hoare_vcg_ball_lift hoare_vcg_imp_lift
| simp add: valid_ntfn'_def split: ntfn.splits)+
apply auto
done
lemma hoare_vcg_imp_liftE:
"\<lbrakk>\<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. \<not> P rv s\<rbrace>, \<lbrace>E\<rbrace>; \<lbrace>Q'\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P' s \<or> Q' s\<rbrace> f \<lbrace>\<lambda>rv s. P rv s \<longrightarrow> Q rv s\<rbrace>, \<lbrace>E\<rbrace>"
apply (simp add: validE_def valid_def split_def split: sum.splits)
done
lemma not_obj_at'_ntfn:
"(\<not>obj_at' (P::Structures_H.notification \<Rightarrow> bool) t s) = (\<not> typ_at' NotificationT t s \<or> obj_at' (Not \<circ> P) t s)"
apply (simp add: obj_at'_real_def projectKOs typ_at'_def ko_wp_at'_def objBits_simps)
apply (rule iffI)
apply (clarsimp)
apply (case_tac ko)
apply (clarsimp)+
done
lemma handleRecv_ccorres:
notes rf_sr_upd_safe[simp del]
shows
@ -1596,21 +1481,6 @@ lemma ccorres_ntfn_cases:
apply clarsimp
done
(* FIXME: generalise the one in Interrupt_C *)
lemma getIRQSlot_ccorres2:
"ccorres ((=) \<circ> Ptr) slot_'
\<top> UNIV hs
(getIRQSlot irq) (\<acute>slot :== CTypesDefs.ptr_add \<acute>intStateIRQNode (uint (ucast irq :: word32)))"
apply (rule ccorres_from_vcg[where P=\<top> and P'=UNIV])
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: getIRQSlot_def liftM_def getInterruptState_def
locateSlot_conv)
apply (simp add: simpler_gets_def bind_def return_def)
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
cinterrupt_relation_def size_of_def
cte_level_bits_def mult.commute mult.left_commute ucast_nat_def)
done
lemma getIRQSlot_ccorres3:
"(\<And>rv. ccorresG rf_sr \<Gamma> r xf (P rv) (P' rv) hs (f rv) c) \<Longrightarrow>
ccorresG rf_sr \<Gamma> r xf
@ -1644,9 +1514,6 @@ lemma scast_maxIRQ_is_less:
apply fastforce
done
lemma validIRQcastingLess: "Kernel_C.maxIRQ <s (ucast((ucast (b :: irq))::word16)) \<Longrightarrow> ARM.maxIRQ < b"
by (simp add: Platform_maxIRQ scast_maxIRQ_is_less is_up_def target_size source_size)
lemma scast_maxIRQ_is_not_less: "(\<not> (Kernel_C.maxIRQ) <s (ucast \<circ> (ucast :: irq \<Rightarrow> 16 word)) b) \<Longrightarrow> \<not> (scast Kernel_C.maxIRQ < b)"
apply (subgoal_tac "sint (ucast Kernel_C.maxIRQ :: 32 sword) \<ge> sint (ucast (ucast b))";
simp only: Kernel_C.maxIRQ_def word_sless_def word_sle_def)

View File

@ -53,24 +53,6 @@ lemma threadGet_eq:
apply simp
done
lemma get_tsType_ccorres [corres]:
"ccorres (\<lambda>r r'. r' = thread_state_to_tsType r) ret__unsigned_' (tcb_at' thread)
(UNIV \<inter> {s. thread_state_ptr_' s = Ptr &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])}) []
(getThreadState thread) (Call thread_state_ptr_get_tsType_'proc)"
unfolding getThreadState_def
apply (rule ccorres_from_spec_modifies)
apply (rule thread_state_ptr_get_tsType_spec)
apply (rule thread_state_ptr_get_tsType_modifies)
apply simp
apply (frule (1) obj_at_cslift_tcb)
apply (clarsimp simp: typ_heap_simps)
apply (frule (1) obj_at_cslift_tcb)
apply (clarsimp simp: typ_heap_simps)
apply (rule bexI [rotated, OF threadGet_eq], assumption)
apply simp
apply (erule ctcb_relation_thread_state_to_tsType)
done
lemma threadGet_obj_at2:
"\<lbrace>\<top>\<rbrace> threadGet f thread \<lbrace>\<lambda>v. obj_at' (\<lambda>t. f t = v) thread\<rbrace>"
apply (rule hoare_post_imp)
@ -83,15 +65,6 @@ lemma register_from_H_less:
"register_from_H hr < 20"
by (cases hr, simp_all add: "StrictC'_register_defs")
lemma register_from_H_sless:
"register_from_H hr <s 20"
by (cases hr, simp_all add: "StrictC'_register_defs" word_sless_def word_sle_def)
lemma register_from_H_0_sle[simp]:
"0 <=s register_from_H hr"
using word_0_sle_from_less[OF order_less_le_trans] register_from_H_less
by fastforce
lemma getRegister_ccorres [corres]:
"ccorres (=) ret__unsigned_long_' \<top>
({s. thread_' s = tcb_ptr_to_ctcb_ptr thread} \<inter> {s. reg_' s = register_from_H reg}) []
@ -105,7 +78,7 @@ lemma getRegister_ccorres [corres]:
apply vcg
apply clarsimp
apply (drule (1) obj_at_cslift_tcb)
apply (clarsimp simp: typ_heap_simps register_from_H_less register_from_H_sless)
apply (clarsimp simp: typ_heap_simps register_from_H_less)
apply (clarsimp simp: getRegister_def typ_heap_simps)
apply (rule_tac x = "((atcbContextGet o tcbArch) ko reg, \<sigma>)" in bexI [rotated])
apply (simp add: in_monad' asUser_def select_f_def split_def)

View File

@ -323,27 +323,6 @@ lemma tcb_queue_relation_ptr_rel:
apply (clarsimp simp: distinct_conv_nth)
done
lemma distinct_cons_nth:
assumes dxs: "distinct xs"
and ln: "n < length xs"
and x: "x \<notin> set xs"
shows "(x # xs) ! n \<noteq> xs ! n"
proof
assume n: "(x # xs) ! n = xs ! n"
have ln': "n < length (x # xs)" using ln by simp
have sln: "Suc n < length (x # xs)" using ln by simp
from n have "(x # xs) ! n = (x # xs) ! Suc n" by simp
moreover have "distinct (x # xs)" using dxs x by simp
ultimately show False
unfolding distinct_conv_nth
apply -
apply (drule spec, drule mp [OF _ ln'])
apply (drule spec, drule mp [OF _ sln])
apply simp
done
qed
lemma distinct_nth:
assumes dist: "distinct xs"
and ln: "n < length xs"
@ -380,31 +359,6 @@ next
done
qed
lemma distinct_nth_cons':
assumes dist: "distinct xs"
and xxs: "x \<notin> set xs"
and ln: "n < length xs"
and lm: "m < length xs"
shows "(xs ! n = (x # xs) ! m) = (m = Suc n)"
proof (cases "m = Suc n")
case True
thus ?thesis by simp
next
case False
have ln': "Suc n < length (x # xs)" using ln by simp
have lm': "m < length (x # xs)" using lm by simp
have "distinct (x # xs)" using dist xxs by simp
thus ?thesis using False
unfolding distinct_conv_nth
apply -
apply (drule spec, drule mp [OF _ ln'])
apply (drule spec, drule mp [OF _ lm'])
apply clarsimp
done
qed
lemma nth_first_not_member:
assumes xxs: "x \<notin> set xs"
and ln: "n < length xs"
@ -447,8 +401,8 @@ lemma tcb_queue_next_prev:
apply clarsimp
subgoal by (clarsimp simp: last_conv_nth distinct_nth distinct_nth_cons nth_first_not_member)
subgoal by (fastforce simp: last_conv_nth distinct_nth distinct_nth_cons nth_first_not_member)
subgoal by (clarsimp simp: last_conv_nth distinct_nth distinct_nth_cons distinct_nth_cons' nth_first_not_member)
by (fastforce simp: last_conv_nth distinct_nth distinct_nth_cons distinct_nth_cons' nth_first_not_member)
subgoal by (clarsimp simp: last_conv_nth distinct_nth distinct_nth_cons nth_first_not_member)
by (fastforce simp: last_conv_nth distinct_nth distinct_nth_cons nth_first_not_member)
lemma null_not_in:
@ -1209,8 +1163,5 @@ lemma rf_sr_tcb_update_not_in_queue:
typ_heap_simps')
by (simp add: cmachine_state_relation_def)
lemmas rf_sr_tcb_update_not_in_queue2
= rf_sr_tcb_update_no_queue_helper [OF rf_sr_tcb_update_not_in_queue, simplified]
end
end

View File

@ -83,31 +83,6 @@ end
context kernel_m
begin
lemma getMRs_rel_sched:
"\<lbrakk> getMRs_rel args buffer s;
(cur_tcb' and case_option \<top> valid_ipc_buffer_ptr' buffer) s \<rbrakk>
\<Longrightarrow> getMRs_rel args buffer (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>)"
apply (clarsimp simp: getMRs_rel_def)
apply (rule exI, rule conjI, assumption)
apply (subst det_wp_use, rule det_wp_getMRs)
apply (simp add: cur_tcb'_def split: option.splits)
apply (simp add: valid_ipc_buffer_ptr'_def)
apply (subst (asm) det_wp_use, rule det_wp_getMRs)
apply (simp add: cur_tcb'_def)
apply (clarsimp simp: getMRs_def in_monad)
apply (drule asUser_sched)
apply (intro exI)
apply (erule conjI)
apply (cases buffer)
apply (simp add: return_def)
apply clarsimp
apply (drule mapM_upd [rotated])
prefer 2
apply fastforce
apply (clarsimp simp: loadWordUser_def in_monad stateAssert_def word_size)
apply (erule doMachineOp_sched)
done
lemma getObject_state:
" \<lbrakk>(x, s') \<in> fst (getObject t' s); ko_at' ko t s\<rbrakk>
\<Longrightarrow> (if t = t' then tcbState_update (\<lambda>_. st) x else x,
@ -352,16 +327,6 @@ lemma getMRs_rel_state:
apply (erule doMachineOp_state)
done
(* FIXME: move *)
lemma setTCB_cur:
"\<lbrace>cur_tcb'\<rbrace> setObject t (v::tcb) \<lbrace>\<lambda>_. cur_tcb'\<rbrace>"
including no_pre
apply (wp cur_tcb_lift)
apply (simp add: setObject_def split_def updateObject_default_def)
apply wp
apply simp
done
lemma setThreadState_getMRs_rel:
"\<lbrace>getMRs_rel args buffer and cur_tcb' and case_option \<top> valid_ipc_buffer_ptr' buffer
and (\<lambda>_. runnable' st)\<rbrace>
@ -400,19 +365,6 @@ lemma ccorres_abstract_known:
apply simp
done
lemma distinct_remove1_filter:
"distinct xs \<Longrightarrow> remove1 v xs = [x\<leftarrow>xs. x \<noteq> v]"
apply (induct xs)
apply simp
apply (clarsimp split: if_split)
apply (rule sym, simp add: filter_id_conv)
apply clarsimp
done
lemma hrs_mem_update_cong:
"\<lbrakk> \<And>x. f x = f' x \<rbrakk> \<Longrightarrow> hrs_mem_update f = hrs_mem_update f'"
by (simp add: hrs_mem_update_def)
lemma setPriority_ccorres:
"ccorres dc xfdc
(invs' and tcb_at' t and (\<lambda>s. priority \<le> maxPriority))
@ -520,28 +472,12 @@ lemma checkCapAt_ccorres:
lemmas checkCapAt_ccorres2
= checkCapAt_ccorres[where g=return, simplified bind_return]
lemma invs_psp_aligned_strg':
"invs' s \<longrightarrow> pspace_aligned' s"
by clarsimp
lemma cte_is_derived_capMasterCap_strg:
"cte_wp_at' (is_derived' (ctes_of s) ptr cap \<circ> cteCap) ptr s
\<longrightarrow> cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capMasterCap cap \<or> P) ptr s"
by (clarsimp simp: cte_wp_at_ctes_of is_derived'_def
badge_derived'_def)
lemma cteInsert_cap_to'2:
"\<lbrace>ex_nonz_cap_to' p\<rbrace>
cteInsert newCap srcSlot destSlot
\<lbrace>\<lambda>_. ex_nonz_cap_to' p\<rbrace>"
apply (simp add: cteInsert_def ex_nonz_cap_to'_def setUntypedCapAsFull_def)
apply (rule hoare_vcg_ex_lift)
apply (wp updateMDB_weak_cte_wp_at
updateCap_cte_wp_at_cases getCTE_wp' static_imp_wp)
apply (clarsimp simp: cte_wp_at_ctes_of)
apply auto
done
lemma archSetIPCBuffer_ccorres:
"ccorres dc xfdc \<top> (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr target} \<inter> {s. bufferAddr_' s = buf}) []
(asUser target $ setTCBIPCBuffer buf)
@ -552,12 +488,6 @@ lemma archSetIPCBuffer_ccorres:
apply (clarsimp simp:)
done
lemma threadSet_ipcbuffer_invs:
"is_aligned a msg_align_bits \<Longrightarrow>
\<lbrace>invs' and tcb_at' t\<rbrace> threadSet (tcbIPCBuffer_update (\<lambda>_. a)) t \<lbrace>\<lambda>rv. invs'\<rbrace>"
apply (wp threadSet_invs_trivial, simp_all add: inQ_def cong: conj_cong)
done
lemma invokeTCB_ThreadControl_ccorres:
"ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_')
(invs' and sch_act_simple
@ -1502,14 +1432,6 @@ lemma threadSet_same:
unfolding threadSet_def
by (wpsimp wp: setObject_tcb_strongest getObject_tcb_wp) fastforce
lemma asUser_setRegister_ko_at':
"\<lbrace>obj_at' (\<lambda>tcb'. tcb = tcbArch_update (\<lambda>_. atcbContextSet ((atcbContextGet (tcbArch tcb'))(r := v)) (tcbArch tcb')) tcb') dst\<rbrace>
asUser dst (setRegister r v) \<lbrace>\<lambda>rv. ko_at' (tcb::tcb) dst\<rbrace>"
unfolding asUser_def
apply (wpsimp wp: threadSet_same threadGet_wp)
apply (clarsimp simp: setRegister_def simpler_modify_def obj_at'_def)
done
lemma invokeTCB_WriteRegisters_ccorres[where S=UNIV]:
notes static_imp_wp [wp]
shows
@ -1728,10 +1650,6 @@ lemma ccorres_abstract_cong:
by (simp add: ccorres_underlying_def split_paired_Ball imp_conjL
cong: conj_cong xstate.case_cong)
lemma is_aligned_the_x_strengthen:
"x \<noteq> None \<and> case_option \<top> valid_ipc_buffer_ptr' x s \<longrightarrow> is_aligned (the x) msg_align_bits"
by (clarsimp simp: valid_ipc_buffer_ptr'_def)
lemma valid_ipc_buffer_ptr_the_strengthen:
"x \<noteq> None \<and> case_option \<top> valid_ipc_buffer_ptr' x s \<longrightarrow> valid_ipc_buffer_ptr' (the x) s"
by clarsimp
@ -2531,28 +2449,6 @@ lemma decodeCopyRegisters_ccorres:
word_and_1_shiftl [where n=3,simplified] cap_get_tag_isCap[symmetric] split: if_split_asm)
done
(* FIXME: move *)
lemma ccap_relation_gen_framesize_to_H:
"\<lbrakk> ccap_relation cap cap'; isArchPageCap cap \<rbrakk>
\<Longrightarrow> gen_framesize_to_H (generic_frame_cap_get_capFSize_CL (cap_lift cap'))
= capVPSize (capCap cap)"
apply (clarsimp simp: isCap_simps)
apply (case_tac "sz = ARM.ARMSmallPage")
apply (frule cap_get_tag_PageCap_small_frame)
apply (simp add: cap_get_tag_isCap isCap_simps
pageSize_def cap_lift_small_frame_cap
generic_frame_cap_get_capFSize_CL_def
gen_framesize_to_H_def)
apply (subgoal_tac "cap_get_tag cap' = scast cap_frame_cap")
apply (frule(1) iffD1 [OF cap_get_tag_PageCap_frame])
apply (clarsimp simp: cap_frame_cap_lift generic_frame_cap_get_capFSize_CL_def)
apply (simp add: gen_framesize_to_H_def framesize_to_H_def
split: if_split)
apply (clarsimp simp: ccap_relation_def c_valid_cap_def
cl_valid_cap_def)
apply (simp add: cap_get_tag_isCap isCap_simps pageSize_def)
done
lemma isDevice_PageCap_ccap_relation:
"ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d ref rghts sz data)) cap
\<Longrightarrow> (generic_frame_cap_get_capFIsDevice_CL (cap_lift cap) \<noteq> 0) = d"
@ -3225,7 +3121,7 @@ lemma decodeTCBConfigure_ccorres:
apply (frule interpret_excaps_eq[rule_format, where n=2], simp)
apply (clarsimp simp: mask_def[where n=4] ccap_rights_relation_def
rightsFromWord_wordFromRights
capTCBPtr_eq tcb_ptr_to_ctcb_ptr_mask
capTCBPtr_eq
tcb_cnode_index_defs size_of_def
option_to_0_def rf_sr_ksCurThread
StrictC'_thread_state_defs mask_eq_iff_w2p word_size

View File

@ -50,46 +50,6 @@ lemma unat_of_nat_pageBitsForSize [simp]:
apply simp
done
lemma checkVPAlignment_ccorres:
"ccorres (\<lambda>a c. if to_bool c then a = Inr () else a = Inl AlignmentError) ret__unsigned_long_'
\<top>
(UNIV \<inter> \<lbrace>sz = gen_framesize_to_H \<acute>sz \<and> \<acute>sz && mask 2 = \<acute>sz\<rbrace> \<inter> \<lbrace>\<acute>w = w\<rbrace>)
[]
(checkVPAlignment sz w)
(Call checkVPAlignment_'proc)"
proof -
note [split del] = if_split
show ?thesis
apply (cinit lift: sz_' w_')
apply (csymbr)
apply clarsimp
apply (rule ccorres_Guard [where A=\<top> and C'=UNIV])
apply (simp split: if_split)
apply (rule conjI)
apply (clarsimp simp: mask_def unlessE_def returnOk_def)
apply (rule ccorres_guard_imp)
apply (rule ccorres_return_C)
apply simp
apply simp
apply simp
apply simp
apply (simp split: if_split add: to_bool_def)
apply (clarsimp simp: mask_def unlessE_def throwError_def split: if_split)
apply (rule ccorres_guard_imp)
apply (rule ccorres_return_C)
apply simp
apply simp
apply simp
apply simp
apply (simp split: if_split add: to_bool_def)
apply (clarsimp split: if_split)
apply (simp add: word_less_nat_alt)
apply (rule order_le_less_trans, rule pageBitsForSize_le)
apply simp
done
qed
lemma rf_asidTable:
"\<lbrakk> (\<sigma>, x) \<in> rf_sr; valid_arch_state' \<sigma>; idx \<le> mask asid_high_bits \<rbrakk>
\<Longrightarrow> case armKSASIDTable (ksArchState \<sigma>)
@ -682,11 +642,6 @@ lemma clift_ptr_safe:
\<Longrightarrow> ptr_safe ptr x"
by (erule lift_t_ptr_safe[where g = c_guard])
lemma clift_ptr_safe2:
"clift htd ptr = Some a
\<Longrightarrow> ptr_safe ptr (hrs_htd htd)"
by (cases htd, simp add: hrs_htd_def clift_ptr_safe)
lemma generic_frame_cap_ptr_set_capFMappedAddress_spec:
"\<forall>s cte_slot.
\<Gamma> \<turnstile> \<lbrace>s. (\<exists> cap. cslift s \<^bsup>s\<^esup>cap_ptr = Some cap \<and> cap_lift cap \<noteq> None \<and>
@ -705,7 +660,7 @@ lemma generic_frame_cap_ptr_set_capFMappedAddress_spec:
apply (subgoal_tac "cap_lift ret__struct_cap_C \<noteq> None")
prefer 2
apply (clarsimp simp: generic_frame_cap_set_capFMappedAddress_CL_def split: cap_CL.splits)
apply (clarsimp simp: clift_ptr_safe2 typ_heap_simps)
apply (clarsimp simp: typ_heap_simps)
apply (rule_tac x="cte_C.cap_C_update (\<lambda>_. ret__struct_cap_C) y" in exI)
apply (case_tac y)
apply (clarsimp simp: cte_lift_def typ_heap_simps')
@ -799,15 +754,6 @@ lemma addrFromPPtr_spec:
abbreviation
"lookupPTSlot_xf \<equiv> liftxf errstate lookupPTSlot_ret_C.status_C lookupPTSlot_ret_C.ptSlot_C ret__struct_lookupPTSlot_ret_C_'"
lemma cpde_relation_pde_coarse:
"cpde_relation pdea pde \<Longrightarrow> (pde_get_tag pde = scast pde_pde_coarse) = isPageTablePDE pdea"
apply (simp add: cpde_relation_def Let_def)
apply (simp add: pde_pde_coarse_lift)
apply (case_tac pdea, simp_all add: isPageTablePDE_def) [1]
apply clarsimp
apply (simp add: pde_pde_coarse_lift_def)
done
lemma lookupPTSlot_ccorres:
"ccorres (lookup_failure_rel \<currency> (\<lambda>rv rv'. rv' = pte_Ptr rv)) lookupPTSlot_xf
(page_directory_at' pd)
@ -1661,16 +1607,6 @@ lemma framesize_from_H_mask:
Kernel_C.ARMSection_def Kernel_C.ARMSuperSection_def
split: vmpage_size.splits)
(* FIXME: move *)
lemma dmo_invalidateCacheRange_RAM_invs'[wp]:
"valid invs' (doMachineOp (invalidateCacheRange_RAM vs ve ps)) (\<lambda>rv. invs')"
apply (wp dmo_invs' no_irq no_irq_invalidateCacheRange_RAM)
apply (clarsimp simp: disj_commute[of "pointerInUserData p s" for p s])
apply (erule use_valid)
apply (wp, simp)
done
lemma dmo_flushtype_case:
"(doMachineOp (case t of
ARM_H.flush_type.Clean \<Rightarrow> f
@ -1691,10 +1627,6 @@ definition
| ARM_H.flush_type.CleanInvalidate \<Rightarrow> (label = Kernel_C.ARMPageCleanInvalidate_Data \<or> label = Kernel_C.ARMPDCleanInvalidate_Data)
| ARM_H.flush_type.Unify \<Rightarrow> (label = Kernel_C.ARMPageUnify_Instruction \<or> label = Kernel_C.ARMPDUnify_Instruction)"
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
lemma doFlush_ccorres:
"ccorres dc xfdc (\<lambda>s. vs \<le> ve \<and> ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5
\<and> unat (ve - vs) \<le> gsMaxObjectSize s)
@ -1704,7 +1636,7 @@ lemma doFlush_ccorres:
apply (unfold doMachineOp_bind doFlush_def)
apply (rule ccorres_Guard_Seq)
apply (rule ccorres_basic_srnoop)
apply (simp only: ccorres_seq_IF_False ccorres_seq_skip)
apply (simp only: ccorres_seq_skip)
apply (rule_tac xf'=invLabel___int_' in ccorres_abstract, ceqv, rename_tac invlabel)
apply (rule_tac P="flushtype_relation t invlabel" in ccorres_gen_asm2)
apply (rule_tac xf'=start_' in ccorres_abstract, ceqv, rename_tac start')
@ -1796,11 +1728,6 @@ lemma performPageFlush_ccorres:
apply (clarsimp simp: order_less_imp_le)
done
lemma length_of_msgRegisters:
"length ARM_H.msgRegisters = 4"
by (auto simp: ARM_H.msgRegisters_def msgRegisters_unfold)
(* FIXME: move *)
lemma register_from_H_bound[simp]:
"unat (register_from_H v) < 20"
@ -1845,7 +1772,7 @@ lemma setRegister_ccorres:
atcbContextSet_def atcbContextGet_def
carch_tcb_relation_def
split: if_split)
apply (clarsimp simp: Collect_const_mem register_from_H_sless
apply (clarsimp simp: Collect_const_mem
register_from_H_less)
apply (auto intro: typ_heap_simps elim: obj_at'_weakenE)
done
@ -1878,12 +1805,6 @@ lemma wordFromMessageInfo_ccorres [corres]:
Types_H.msgMaxExtraCaps_def shiftL_nat word_bw_assocs word_bw_comms word_bw_lcs)
done
(* FIXME move *)
lemma register_from_H_eq:
"(r = r') = (register_from_H r = register_from_H r')"
apply (case_tac r, simp_all add: C_register_defs)
by (case_tac r', simp_all add: C_register_defs)+
lemma setMessageInfo_ccorres:
"ccorres dc xfdc (tcb_at' thread)
(UNIV \<inter> \<lbrace>mi = message_info_to_H mi'\<rbrace>) hs
@ -1911,7 +1832,7 @@ lemma performPageGetAddress_ccorres:
apply (cinit lift: vbase_ptr_')
apply csymbr
apply (rule ccorres_pre_getCurThread)
apply (clarsimp simp add: setMRs_def zipWithM_x_mapM_x mapM_x_Nil length_of_msgRegisters zip_singleton msgRegisters_unfold mapM_x_singleton)
apply (clarsimp simp add: setMRs_def zipWithM_x_mapM_x mapM_x_Nil zip_singleton msgRegisters_unfold mapM_x_singleton)
apply (ctac add: setRegister_ccorres)
apply csymbr
apply (rule ccorres_add_return2)
@ -2052,32 +1973,6 @@ lemma ignoreFailure_liftM:
apply (simp split: sum.split)
done
lemma ccorres_pre_getObject_pte:
assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c"
shows "ccorres r xf
(\<lambda>s. (\<forall>pte. ko_at' pte p s \<longrightarrow> P pte s))
{s. \<forall>pte pte'. cslift s (pte_Ptr p) = Some pte' \<and> cpte_relation pte pte'
\<longrightarrow> s \<in> P' pte}
hs (getObject p >>= (\<lambda>rv. f rv)) c"
apply (rule ccorres_guard_imp2)
apply (rule ccorres_symb_exec_l)
apply (rule ccorres_guard_imp2)
apply (rule cc)
apply (rule conjI)
apply (rule_tac Q="ko_at' rv p s" in conjunct1)
apply assumption
apply assumption
apply (wp getPTE_wp empty_fail_getObject | simp)+
apply clarsimp
apply (erule cmap_relationE1 [OF rf_sr_cpte_relation],
erule ko_at_projectKO_opt)
apply simp
done
lemmas unfold_checkMapping_return
= from_bool_0[where 'a=32, folded exception_defs]
to_bool_def
end
context begin interpretation Arch . (*FIXME: arch_split*)
@ -2225,25 +2120,6 @@ lemma ccorres_flip_Guard:
apply (fastforce intro: exec.Guard exec.GuardFault exec_handlers.intros)
done
lemma ccorres_second_Guard:
assumes cc: "ccorres_underlying sr \<Gamma> r xf arrel axf A C' hs a (Guard F1 S1 c)"
shows "ccorres_underlying sr \<Gamma> r xf arrel axf A (C' \<inter> S) hs a (Guard F1 S1 (Guard F S c))"
apply (rule ccorres_flip_Guard)
apply (rule ccorres_Guard)
apply (rule cc)
done
lemma multiple_add_less_nat:
"a < (c :: nat) \<Longrightarrow> x dvd a \<Longrightarrow> x dvd c \<Longrightarrow> b < x
\<Longrightarrow> a + b < c"
apply (subgoal_tac "b < c - a")
apply simp
apply (erule order_less_le_trans)
apply (rule dvd_imp_le)
apply simp
apply simp
done
lemma large_ptSlot_array_constraint:
"is_aligned (ptSlot :: word32) 6 \<Longrightarrow> n \<le> limit - 240 \<and> 240 \<le> limit
\<Longrightarrow> \<exists>i. ptSlot = (ptSlot && ~~ mask ptBits) + of_nat i * 4 \<and> i + n \<le> limit"
@ -2362,8 +2238,7 @@ lemma unmapPage_ccorres:
pte_pte_small_lift_def pte_pte_invalid_def
split: if_split_asm pte.split_asm)
apply (rule ceqv_refl)
apply (simp add: unfold_checkMapping_return liftE_liftM
Collect_const[symmetric] dc_def[symmetric]
apply (simp add: liftE_liftM Collect_const[symmetric] dc_def[symmetric]
del: Collect_const)
apply (rule ccorres_handlers_weaken2)
apply csymbr
@ -2407,7 +2282,7 @@ lemma unmapPage_ccorres:
apply (rule ceqv_refl)
apply (simp add: liftE_liftM dc_def[symmetric]
mapM_discarded whileAnno_def ARMLargePageBits_def ARMSmallPageBits_def
Collect_False unfold_checkMapping_return word_sle_def
Collect_False word_sle_def
del: Collect_const)
apply (ccorres_remove_UNIV_guard)
apply (rule ccorres_rhs_assoc2)
@ -2494,7 +2369,7 @@ lemma unmapPage_ccorres:
Let_def pde_tag_defs isSectionPDE_def
split: pde.split_asm if_split_asm)
apply (rule ceqv_refl)
apply (simp add: unfold_checkMapping_return Collect_False dc_def[symmetric]
apply (simp add: Collect_False dc_def[symmetric]
del: Collect_const)
apply (rule ccorres_handlers_weaken2, simp)
apply csymbr
@ -2534,7 +2409,7 @@ lemma unmapPage_ccorres:
pde_pde_section_lift_def
split: if_split_asm pde.split_asm)
apply (rule ceqv_refl)
apply (simp add: unfold_checkMapping_return Collect_False ARMSuperSectionBits_def
apply (simp add: Collect_False ARMSuperSectionBits_def
ARMSectionBits_def word_sle_def
del: Collect_const)
apply (ccorres_remove_UNIV_guard)
@ -2793,14 +2668,6 @@ lemma getSlotCap_wp':
apply (clarsimp simp: cte_wp_at_ctes_of)
done
lemma vmsz_aligned_aligned_pageBits:
"vmsz_aligned' ptr sz \<Longrightarrow> is_aligned ptr pageBits"
apply (simp add: vmsz_aligned'_def)
apply (erule is_aligned_weaken)
apply (simp add: pageBits_def pageBitsForSize_def
split: vmpage_size.split)
done
lemma ccap_relation_PageCap_generics:
"ccap_relation (ArchObjectCap (PageCap d ptr rghts sz mapdata)) cap'
\<Longrightarrow> (mapdata \<noteq> None \<longrightarrow>
@ -2913,8 +2780,7 @@ lemma performPageInvocationUnmap_ccorres:
apply (drule ccap_relation_mapped_asid_0)
apply (frule ctes_of_valid', clarsimp)
apply (drule valid_global_refsD_with_objSize, clarsimp)
apply (fastforce simp: mask_def valid_cap'_def
vmsz_aligned_aligned_pageBits)
apply (fastforce simp: mask_def valid_cap'_def)
apply assumption
apply (clarsimp simp: cte_wp_at_ctes_of isCap_simps split: if_split)
apply (drule diminished_PageCap)
@ -3122,13 +2988,6 @@ lemma setCTE_asidpool':
apply (clarsimp simp: ps_clear_upd' lookupAround2_char1)
done
(* FIXME: move *)
lemma udpateCap_asidpool':
"\<lbrace> ko_at' (ASIDPool pool) p \<rbrace> updateCap c p' \<lbrace>\<lambda>_. ko_at' (ASIDPool pool) p\<rbrace>"
apply (simp add: updateCap_def)
apply (wp setCTE_asidpool')
done
(* FIXME: move *)
lemma asid_pool_at_rf_sr:
"\<lbrakk>ko_at' (ASIDPool pool) p s; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow>
@ -3150,11 +3009,6 @@ lemma asid_pool_at_ko:
apply (case_tac asidpool, auto)[1]
done
(* FIXME: move *)
lemma asid_pool_at_c_guard:
"\<lbrakk>asid_pool_at' p s; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> c_guard (ap_Ptr p)"
by (fastforce intro: typ_heap_simps dest!: asid_pool_at_ko asid_pool_at_rf_sr)
(* FIXME: move *)
lemma setObjectASID_Basic_ccorres:
"ccorres dc xfdc \<top> {s. f s = p \<and> casid_pool_relation pool (asid_pool_C (pool' s))} hs
@ -3270,7 +3124,7 @@ lemma performASIDPoolInvocation_ccorres:
apply (vcg)
apply (rule conseqPre, vcg)
apply clarsimp
apply (wp udpateCap_asidpool')
apply wp
apply vcg
apply (wp getASID_wp)
apply simp
@ -3304,12 +3158,6 @@ lemma performASIDPoolInvocation_ccorres:
apply (simp add: asid_low_bits_def)
done
lemma pte_case_isInvalidPTE:
"(case pte of InvalidPTE \<Rightarrow> P | _ \<Rightarrow> Q)
= (if isInvalidPTE pte then P else Q)"
by (cases pte, simp_all add: isInvalidPTE_def)
lemma flushTable_ccorres:
"ccorres dc xfdc (invs' and cur_tcb' and (\<lambda>_. asid \<le> mask asid_bits))
(UNIV \<inter> {s. pd_' s = pde_Ptr pd} \<inter> {s. asid_' s = asid}

View File

@ -243,9 +243,6 @@ definition
| Some cap \<Rightarrow> Some \<lparr> cap_CL = cap,
cteMDBNode_CL = mdb_node_lift (cteMDBNode_C c) \<rparr>"
lemma to_bool_false [simp]: "\<not> to_bool false"
by (simp add: to_bool_def false_def)
(* this is slightly weird, but the bitfield generator
masks everything with the expected bit length.
So we do that here too. *)
@ -253,32 +250,12 @@ definition
to_bool_bf :: "'a::len word \<Rightarrow> bool" where
"to_bool_bf w \<equiv> (w && mask 1) = 1"
lemma to_bool_bf_mask1 [simp]:
"to_bool_bf (mask (Suc 0))"
by (simp add: mask_def to_bool_bf_def)
lemma to_bool_bf_0 [simp]: "\<not>to_bool_bf 0"
by (simp add: to_bool_bf_def)
lemma to_bool_bf_1 [simp]: "to_bool_bf 1"
by (simp add: to_bool_bf_def mask_def)
lemma to_bool_bf_false [simp]:
"\<not>to_bool_bf false"
by (simp add: false_def)
lemma to_bool_bf_true [simp]:
"to_bool_bf true"
by (simp add: true_def)
lemma to_bool_to_bool_bf:
"w = false \<or> w = true \<Longrightarrow> to_bool_bf w = to_bool w"
by (auto simp: false_def true_def to_bool_def to_bool_bf_def mask_def)
lemma to_bool_bf_mask_1 [simp]:
"to_bool_bf (w && mask (Suc 0)) = to_bool_bf w"
by (simp add: to_bool_bf_def)
lemma to_bool_bf_and [simp]:
"to_bool_bf (a && b) = (to_bool_bf a \<and> to_bool_bf (b::word32))"
apply (clarsimp simp: to_bool_bf_def)