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

arm-hyp crefine: update to Isabelle2020 

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
This commit is contained in:
Gerwin Klein 2020-08-02 10:14:19 +08:00 committed by Gerwin Klein
parent 41d1473216
commit eb2de99511
19 changed files with 110 additions and 69 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
proof/crefine/ARM_HYP/ArchMove_C.thy
View File

@ -158,7 +158,7 @@ lemma setCTE_asidpool':
apply (simp add: updateObject_cte)
apply (clarsimp simp: updateObject_cte typeError_def magnitudeCheck_def in_monad
split: kernel_object.splits if_splits option.splits)
apply (clarsimp simp: ps_clear_upd' lookupAround2_char1)
apply (clarsimp simp: ps_clear_upd lookupAround2_char1)
done
lemma udpateCap_asidpool':

8
proof/crefine/ARM_HYP/Arch_C.thy
View File

@ -2276,8 +2276,8 @@ lemma injection_handler_whenE:
= (if a then (injection_handler Inl b)
else (returnOk ()))"
apply (subst injection_handler_returnOk[symmetric])
apply (clarsimp simp:whenE_def injection_handler_def)
apply (fastforce simp:split:if_splits)
apply (clarsimp simp: whenE_def injection_handler_def cong: if_cong)
apply (fastforce split: if_splits)
done
lemma injection_handler_if_returnOk:
@ -2590,7 +2590,7 @@ lemma decodeARMFrameInvocation_ccorres:
(decodeARMMMUInvocation label args cptr slot cp extraCaps
>>= invocationCatch thread isBlocking isCall InvokeArchObject)
(Call decodeARMFrameInvocation_'proc)"
supply if_cong[cong] option.case_cong[cong]
apply (clarsimp simp only: isCap_simps)
apply (cinit' lift: invLabel_' length___unsigned_long_' cte_' excaps_' cap_' buffer_'
simp: decodeARMMMUInvocation_def decodeARMPageFlush_def)
@ -3155,7 +3155,7 @@ proof -
using assms
apply (subst AND_NOT_mask_plus_AND_mask_eq
[where w = start,symmetric,where n = "pageBitsForSize a"])
apply (simp add:sign_simps page_base_def)
apply (simp add: page_base_def)
apply (drule word_le_minus_mono_left[where x= "start && ~~ mask (pageBitsForSize a)"])
apply (rule word_and_le2)
apply (simp(no_asm_use), simp)

8
proof/crefine/ARM_HYP/CSpace_C.thy
View File

@ -853,6 +853,7 @@ lemma update_freeIndex':
have i'_bound_word: "(of_nat i' :: machine_word) \<le> 2 ^ maxUntypedSizeBits"
using order_trans[OF i'_bound power_increasing[OF sz_bound], simplified]
by (simp add: word_of_nat_le untypedBits_defs)
note option.case_cong[cong] if_cong[cong]
show ?thesis
apply (cinit lift: cap_ptr_' v32_')
apply (rule ccorres_pre_getCTE)
@ -2319,7 +2320,7 @@ lemma heap_list_zero_Ball_intvl:
lemma untypedZeroRange_not_device:
"untypedZeroRange cap = Some r
\<Longrightarrow> \<not> capIsDevice cap"
by (clarsimp simp: untypedZeroRange_def)
by (clarsimp simp: untypedZeroRange_def cong: if_cong)
lemma updateTrackedFreeIndex_noop_ccorres:
"ccorres dc xfdc (cte_wp_at' ((\<lambda>cap. isUntypedCap cap
@ -2478,6 +2479,7 @@ lemma emptySlot_ccorres:
[]
(emptySlot slot info)
(Call emptySlot_'proc)"
supply if_cong[cong]
apply (cinit lift: slot_' cleanupInfo_' simp: case_Null_If)
\<comment> \<open>--- handle the clearUntypedFreeIndex\<close>
@ -2740,6 +2742,7 @@ lemma Arch_sameRegionAs_spec:
ccap_relation (ArchObjectCap capb) \<acute>cap_b \<rbrace>
Call Arch_sameRegionAs_'proc
\<lbrace> \<acute>ret__unsigned_long = from_bool (Arch.sameRegionAs capa capb) \<rbrace>"
supply if_cong[cong]
apply vcg
apply clarsimp
@ -3731,7 +3734,7 @@ lemma sameRegionAs_NotificationCap:
done
lemma isMDBParentOf_spec:
notes option.case_cong_weak [cong]
notes option.case_cong_weak [cong] if_cong[cong]
shows "\<forall>ctea cte_a cteb cte_b.
\<Gamma> \<turnstile> {s. cslift s (cte_a_' s) = Some cte_a \<and>
ccte_relation ctea cte_a \<and>
@ -3829,6 +3832,7 @@ lemma updateCapData_spec:
"\<forall>cap. \<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>"
supply if_cong[cong]
apply (rule allI, rule conseqPre)
apply vcg
apply (clarsimp simp: if_1_0_0)

14
proof/crefine/ARM_HYP/CSpace_RAB_C.thy
View File

@ -79,7 +79,7 @@ next
fix s s'
assume "(s, s') \<in> rf_sr" and "(G and P) s" and "s' \<in> G'"
thus "(G and (\<lambda>_. \<exists>s. P s)) s \<and> s' \<in> G'"
by (clarsimp elim!: exI)
by fastforce
qed
(* MOVE, generalise *)
@ -102,10 +102,6 @@ lemma valid_cap_cte_at':
done
declare ucast_id [simp]
declare resolveAddressBits.simps [simp del]
lemma rightsFromWord_wordFromRights:
"rightsFromWord (wordFromRights rghts) = rghts"
apply (cases rghts)
@ -185,11 +181,11 @@ proof (cases "isCNodeCap cap'")
\<comment> \<open>Exception stuff\<close>
apply (rule ccorres_split_throws)
apply (simp add: Collect_const cap_get_tag_isCap isCap_simps ccorres_cond_iffs
resolveAddressBits.simps scast_id)
resolveAddressBits.simps)
apply (rule ccorres_from_vcg_throws [where P = \<top> and P' = UNIV])
apply (rule allI)
apply (rule conseqPre)
apply (simp add: throwError_def return_def split)
apply (simp add: throwError_def return_def)
apply vcg
apply (clarsimp simp add: exception_defs lookup_fault_lift_def)
apply (simp split: if_split)
@ -427,14 +423,14 @@ next
apply (simp add: cap_simps)
done
note if_cong[cong]
note if_cong[cong] option.case_cong[cong]
show ?case
using ind.prems
apply -
apply (rule iffD1 [OF ccorres_expand_while_iff])
apply (subst resolveAddressBits.simps)
apply (unfold case_into_if)
apply (simp add: Let_def ccorres_cond_iffs split del: if_split)
apply (simp add: Let_def ccorres_cond_iffs)
apply (rule ccorres_rhs_assoc)+
apply (cinitlift nodeCap_' n_bits_')
apply (erule_tac t = nodeCapa in ssubst)

5
proof/crefine/ARM_HYP/Delete_C.thy
View File

@ -138,6 +138,7 @@ lemma capRemovable_spec:
"\<forall>cap s. \<Gamma>\<turnstile> \<lbrace>s. ccap_relation cap \<acute>cap \<and> (isZombie cap \<or> cap = NullCap) \<and> capAligned cap\<rbrace>
Call capRemovable_'proc
{s'. ret__unsigned_long_' s' = from_bool (capRemovable cap (ptr_val (slot_' s)))}"
supply if_cong[cong]
apply vcg
apply (clarsimp simp: cap_get_tag_isCap(1-8)[THEN trans[OF eq_commute]])
apply (simp add: capRemovable_def from_bool_def[where b=True] true_def)
@ -157,6 +158,7 @@ lemma capCyclicZombie_spec:
"\<forall>cap s. \<Gamma>\<turnstile> \<lbrace>s. ccap_relation cap \<acute>cap \<and> isZombie cap \<and> capAligned cap\<rbrace>
Call capCyclicZombie_'proc
{s'. ret__unsigned_long_' s' = from_bool (capCyclicZombie cap (ptr_val (slot_' s)))}"
supply if_cong[cong]
apply vcg
apply (clarsimp simp: from_bool_0)
apply (frule(1) cap_get_tag_isCap [THEN iffD2], simp)
@ -393,8 +395,7 @@ lemma ccorres_cutMon_locateSlotCap_Zombie:
apply (drule(1) rf_sr_gsCNodes_array_assertion)
apply (erule notE, erule array_assertion_shrink_right)
apply (frule valid_Zombie_number_word_bits, simp+)
by (simp add: unat_arith_simps unat_of_nat word_bits_def
valid_cap_simps')
by (simp add: unat_arith_simps unat_of_nat word_bits_def valid_cap_simps')
lemma reduceZombie_ccorres1:
assumes fs_cc:

2
proof/crefine/ARM_HYP/DetWP.thy
View File

@ -60,7 +60,7 @@ lemma det_wp_getTCB [wp]:
apply (rule det_wp_pre)
apply (wp|wpc)+
apply (clarsimp simp add: obj_at'_def projectKOs objBits_simps
cong: conj_cong)
cong: conj_cong option.case_cong)
apply (simp add: lookupAround2_known1)
apply (rule ps_clear_lookupAround2, assumption+)
apply simp

25
proof/crefine/ARM_HYP/Fastpath_C.thy
View File

@ -407,9 +407,10 @@ lemma lookup_fp_ccorres':
have cap_get_tag_update_1:
"\<And>f cap. cap_get_tag (cap_C.words_C_update (\<lambda>w. Arrays.update w (Suc 0) (f w)) cap) = cap_get_tag cap"
by (simp add: cap_get_tag_def)
by (simp add: cap_get_tag_def cong: if_cong)
show ?case
supply if_cong[cong]
apply (cinitlift cap_' bits_')
apply (rename_tac cbits ccap)
apply (elim conjE)
@ -502,7 +503,7 @@ lemma lookup_fp_ccorres':
apply (rule ccorres_cutMon)
apply (simp add: cutMon_walk_bindE unlessE_whenE
del: Collect_const
split del: if_split cong: call_ignore_cong)
cong: call_ignore_cong)
apply (rule ccorres_drop_cutMon_bindE)
apply csymbr+
apply (rule ccorres_rhs_assoc2)
@ -2133,7 +2134,7 @@ lemma recv_ep_queued_st_tcb_at':
done
lemma fastpath_call_ccorres:
notes hoare_TrueI[simp]
notes hoare_TrueI[simp] if_cong[cong] option.case_cong[cong]
shows "ccorres dc xfdc
(\<lambda>s. invs' s \<and> ct_in_state' ((=) Running) s
\<and> obj_at' (\<lambda>tcb. (atcbContextGet o tcbArch) tcb ARM_HYP_H.capRegister = cptr
@ -2947,7 +2948,7 @@ lemma fastpath_reply_cap_check_ccorres:
done
lemma fastpath_reply_recv_ccorres:
notes hoare_TrueI[simp]
notes hoare_TrueI[simp] if_cong[cong] option.case_cong[cong]
shows "ccorres dc xfdc
(\<lambda>s. invs' s \<and> ct_in_state' ((=) Running) s
\<and> obj_at' (\<lambda>tcb. (atcbContextGet o tcbArch) tcb capRegister = cptr
@ -3842,9 +3843,13 @@ lemma setCTE_obj_at'_tcbIPCBuffer:
unfolding setCTE_def
by (rule setObject_cte_obj_at_tcb', simp+)
context
notes if_cong[cong]
begin
crunches cteInsert, asUser
for obj_at'_tcbIPCBuffer[wp]: "obj_at' (\<lambda>tcb. P (tcbIPCBuffer tcb)) t"
(wp: setCTE_obj_at'_queued crunch_wps threadSet_obj_at'_really_strongest)
end
crunch ksReadyQueues_inv[wp]: cteInsert "\<lambda>s. P (ksReadyQueues s)"
(wp: hoare_drop_imps)
@ -3889,6 +3894,7 @@ lemma fastpath_callKernel_SysCall_corres:
and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)
and (\<lambda>s. ksDomainTime s \<noteq> 0))
(callKernel (SyscallEvent SysCall)) (fastpaths SysCall)"
supply if_cong[cong] option.case_cong[cong]
apply (rule monadic_rewrite_introduce_alternative)
apply (simp add: callKernel_def)
apply (rule monadic_rewrite_imp)
@ -4649,7 +4655,7 @@ lemma setEndpoint_clearUntypedFreeIndex_pivot[unfolded K_bind_def]:
setEndpoint_getCTE_pivot
updateTrackedFreeIndex_def
modify_setEndpoint_pivot
split: capability.split
split: capability.split cong: option.case_cong
| rule bind_cong[OF refl] allI impI
bind_apply_cong[OF refl])+
@ -4882,8 +4888,12 @@ lemma tcbSchedEnqueue_tcbIPCBuffer:
crunch obj_at'_tcbIPCBuffer[wp]: rescheduleRequired "obj_at' (\<lambda>tcb. P (tcbIPCBuffer tcb)) t"
(wp: crunch_wps tcbSchedEnqueue_tcbIPCBuffer simp: rescheduleRequired_def)
context
notes if_cong[cong]
begin
crunch obj_at'_tcbIPCBuffer[wp]: setThreadState "obj_at' (\<lambda>tcb. P (tcbIPCBuffer tcb)) t"
(wp: crunch_wps threadSet_obj_at'_really_strongest)
end
crunch obj_at'_tcbIPCBuffer[wp]: getCTE "obj_at' (\<lambda>tcb. P (tcbIPCBuffer tcb)) t"
(wp: setCTE_obj_at'_queued crunch_wps threadSet_obj_at'_really_strongest)
@ -4897,9 +4907,13 @@ crunch obj_at'_tcbIPCBuffer[wp]: transferCapsToSlots "obj_at' (\<lambda>tcb. P (
crunch obj_at'_tcbIPCBuffer[wp]: asUser "obj_at' (\<lambda>tcb. P (tcbIPCBuffer tcb)) t"
(wp: crunch_wps)
context
notes if_cong[cong]
begin
crunch obj_at'_tcbIPCBuffer[wp]: handleFault "obj_at' (\<lambda>tcb. P (tcbIPCBuffer tcb)) t"
(wp: crunch_wps constOnFailure_wp tcbSchedEnqueue_tcbIPCBuffer threadSet_obj_at'_really_strongest
simp: zipWithM_x_mapM)
end
lemma fastpath_callKernel_SysReplyRecv_corres:
"monadic_rewrite True False
@ -4907,6 +4921,7 @@ lemma fastpath_callKernel_SysReplyRecv_corres:
and cnode_caps_gsCNodes')
(callKernel (SyscallEvent SysReplyRecv)) (fastpaths SysReplyRecv)"
including no_pre
supply if_cong[cong] option.case_cong[cong]
apply (rule monadic_rewrite_introduce_alternative)
apply ( simp add: callKernel_def)
apply (rule monadic_rewrite_imp)

13
proof/crefine/ARM_HYP/Finalise_C.thy
View File

@ -791,6 +791,7 @@ lemma unbindNotification_ccorres:
"ccorres dc xfdc
(invs') (UNIV \<inter> {s. tcb_' s = tcb_ptr_to_ctcb_ptr tcb}) []
(unbindNotification tcb) (Call unbindNotification_'proc)"
supply option.case_cong[cong]
apply (cinit lift: tcb_')
apply (rule_tac xf'=ntfnPtr_'
and r'="\<lambda>rv rv'. rv' = option_to_ptr rv \<and> rv \<noteq> Some 0"
@ -824,6 +825,7 @@ lemma unbindNotification_ccorres:
lemma unbindMaybeNotification_ccorres:
"ccorres dc xfdc (invs') (UNIV \<inter> {s. ntfnPtr_' s = ntfn_Ptr ntfnptr}) []
(unbindMaybeNotification ntfnptr) (Call unbindMaybeNotification_'proc)"
supply option.case_cong[cong]
apply (cinit lift: ntfnPtr_')
apply (rule ccorres_symb_exec_l [OF _ get_ntfn_inv' _ empty_fail_getNotification])
apply (rule ccorres_rhs_assoc2)
@ -1132,7 +1134,7 @@ lemma deleteASIDPool_ccorres:
apply (erule is_aligned_add_less_t2n)
apply (subst(asm) Suc_unat_diff_1)
apply (simp add: asid_low_bits_def)
apply (simp add: unat_power_lower asid_low_bits_word_bits)
apply (simp add: asid_low_bits_word_bits)
apply (erule of_nat_less_pow_32 [OF _ asid_low_bits_word_bits])
apply (simp add: asid_low_bits_def asid_bits_def)
apply (simp add: asid_bits_def)
@ -2279,6 +2281,7 @@ lemma Arch_finaliseCap_ccorres:
(UNIV \<inter> {s. ccap_relation (ArchObjectCap cp) (cap_' s)}
\<inter> {s. final_' s = from_bool is_final}) []
(Arch.finaliseCap cp is_final) (Call Arch_finaliseCap_'proc)"
supply if_cong[cong]
apply (cinit lift: cap_' final_' cong: call_ignore_cong)
apply csymbr
apply (simp add: ARM_HYP_H.finaliseCap_def cap_get_tag_isCap_ArchObject)
@ -2322,7 +2325,7 @@ lemma Arch_finaliseCap_ccorres:
apply (frule small_frame_cap_is_mapped_alt)
apply (clarsimp simp: cap_small_frame_cap_lift cap_to_H_def
case_option_over_if
elim!: ccap_relationE simp del: Collect_const)
elim!: ccap_relationE)
apply (simp add: split_def)
apply (rule ccorres_rhs_assoc)+
apply csymbr
@ -2338,7 +2341,7 @@ lemma Arch_finaliseCap_ccorres:
apply (frule small_frame_cap_is_mapped_alt)
apply (clarsimp simp: cap_small_frame_cap_lift cap_to_H_def
case_option_over_if
elim!: ccap_relationE simp del: Collect_const)
elim!: ccap_relationE)
apply (simp add: split_def)
apply return_NullCap_pair_ccorres
apply (clarsimp simp: isCap_simps)
@ -2356,7 +2359,7 @@ lemma Arch_finaliseCap_ccorres:
apply (frule frame_cap_is_mapped_alt)
apply (clarsimp simp: cap_frame_cap_lift cap_to_H_def
case_option_over_if
elim!: ccap_relationE simp del: Collect_const)
elim!: ccap_relationE)
apply simp
apply (rule ccorres_rhs_assoc)+
apply csymbr
@ -2373,7 +2376,7 @@ lemma Arch_finaliseCap_ccorres:
apply (frule frame_cap_is_mapped_alt)
apply (clarsimp simp: cap_frame_cap_lift cap_to_H_def
case_option_over_if
elim!: ccap_relationE simp del: Collect_const)
elim!: ccap_relationE)
apply clarsimp
apply return_NullCap_pair_ccorres
apply (clarsimp simp: isCap_simps)

13
proof/crefine/ARM_HYP/Invoke_C.thy
View File

@ -587,6 +587,7 @@ lemma decodeCNodeInvocation_ccorres:
(decodeCNodeInvocation lab args cp (map fst extraCaps)
>>= invocationCatch thread isBlocking isCall InvokeCNode)
(Call decodeCNodeInvocation_'proc)"
supply if_cong[cong]
apply (cases "\<not>isCNodeCap cp")
apply (simp add: decodeCNodeInvocation_def
cong: conj_cong)
@ -635,9 +636,8 @@ lemma decodeCNodeInvocation_ccorres:
del: Collect_const cong: call_ignore_cong)
apply (rule ccorres_split_throws)
apply (rule ccorres_rhs_assoc | csymbr)+
apply (simp add: invocationCatch_use_injection_handler
[symmetric, unfolded o_def]
if_1_0_0 dc_def[symmetric]
apply (simp add: invocationCatch_use_injection_handler[symmetric, unfolded o_def]
dc_def[symmetric]
del: Collect_const cong: call_ignore_cong)
apply (rule ccorres_Cond_rhs_Seq)
apply (simp add:if_P del: Collect_const)
@ -647,8 +647,7 @@ lemma decodeCNodeInvocation_ccorres:
apply (simp add: syscall_error_to_H_cases)
apply (simp add: linorder_not_less del: Collect_const cong: call_ignore_cong)
apply csymbr
apply (simp add: if_1_0_0 interpret_excaps_test_null
excaps_map_def
apply (simp add: if_1_0_0 interpret_excaps_test_null excaps_map_def
del: Collect_const)
apply (rule ccorres_Cond_rhs_Seq)
apply (simp add: throwError_bind invocationCatch_def)
@ -1837,7 +1836,7 @@ lemma byte_regions_unmodified_actually_heap_list:
lemma resetUntypedCap_ccorres:
notes upt.simps[simp del] Collect_const[simp del] replicate_numeral[simp del]
untypedBits_defs[simp]
untypedBits_defs[simp] if_cong[cong] option.case_cong[cong]
shows
"ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
(invs' and sch_act_simple and ct_active' and cte_wp_at' (isUntypedCap o cteCap) slot
@ -2698,6 +2697,7 @@ lemma checkFreeIndex_ccorres:
;; \<acute>reset :== scast false)
(\<acute>freeIndex :== 0
;; \<acute>reset :== scast true)))"
supply if_cong[cong]
apply (simp add: constOnFailure_def catch_def liftE_def bindE_bind_linearise bind_assoc case_sum_distrib)
apply (rule ccorres_guard_imp2)
apply (rule ccorres_split_nothrow_case_sum)
@ -2849,6 +2849,7 @@ lemma decodeUntypedInvocation_ccorres_helper:
liftE (stateAssert (valid_untyped_inv' uinv) []); returnOk uinv odE)
>>= invocationCatch thread isBlocking isCall InvokeUntyped)
(Call decodeUntypedInvocation_'proc)"
supply if_cong[cong] option.case_cong[cong]
apply (rule ccorres_name_pre)
apply (cinit' lift: invLabel_' length___unsigned_long_' cap_' slot_' excaps_' call_' buffer_'
simp: decodeUntypedInvocation_def list_case_If2

4
proof/crefine/ARM_HYP/IpcCancel_C.thy
View File

@ -91,8 +91,6 @@ lemma ntfn_ptr_get_queue_spec:
apply clarsimp
done
declare td_names_word8[simp]
abbreviation
"cslift_all_but_tcb_C s t \<equiv> (cslift s :: cte_C typ_heap) = cslift t
\<and> (cslift s :: endpoint_C typ_heap) = cslift t
@ -2300,7 +2298,7 @@ lemma possibleSwitchTo_ccorres:
\<inter> UNIV) []
(possibleSwitchTo t )
(Call possibleSwitchTo_'proc)"
supply if_split [split del]
supply if_split [split del] if_cong[cong]
supply Collect_const [simp del]
supply dc_simp [simp del]
supply prio_and_dom_limit_helpers[simp]

17
proof/crefine/ARM_HYP/Ipc_C.thy
View File

@ -658,6 +658,7 @@ lemma handleFaultReply':
msg \<leftarrow> getMRs s sb tag;
handleFaultReply f r (msgLabel tag) msg
od) (handleFaultReply' f s r)"
supply if_cong[cong]
apply (unfold handleFaultReply'_def getMRs_def msgMaxLength_def
bit_def msgLengthBits_def msgRegisters_unfold
fromIntegral_simp1 fromIntegral_simp2
@ -772,7 +773,6 @@ lemma handleFaultReply':
split_def n_msgRegisters_def msgMaxLength_def
bind_comm_mapM_comm [OF asUser_loadWordUser_comm, symmetric]
word_size msgLengthBits_def n_syscallMessage_def Let_def
split del: if_split
cong: if_weak_cong register.case_cong)
@ -1468,6 +1468,7 @@ lemma getRestartPC_ccorres [corres]:
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>"
supply if_cong[cong]
apply (simp add: asUser_def split_def)
apply (wp threadGet_wp)
apply simp
@ -4275,6 +4276,7 @@ lemma handleFaultReply_ccorres [corres]:
msg \<leftarrow> getMRs s sb tag;
handleFaultReply f r (msgLabel tag) msg
od) (Call handleFaultReply_'proc)"
supply if_cong[cong] option.case_cong[cong]
apply (unfold K_def, rule ccorres_gen_asm)
apply (rule monadic_rewrite_ccorres_assemble_nodrop[OF _ handleFaultReply',rotated], simp)
apply (cinit lift: sender_' receiver_' simp: whileAnno_def)
@ -4384,6 +4386,10 @@ lemma handleFaultReply_ccorres [corres]:
apply (fastforce simp: seL4_Faults seL4_Arch_Faults)
done
context
notes if_cong[cong]
begin
crunch tcbFault: emptySlot, tcbSchedEnqueue, rescheduleRequired
"obj_at' (\<lambda>tcb. P (tcbFault tcb)) t"
(wp: threadSet_obj_at'_strongish crunch_wps
@ -4393,12 +4399,14 @@ crunch tcbFault: setThreadState, cancelAllIPC, cancelAllSignals
"obj_at' (\<lambda>tcb. P (tcbFault tcb)) t"
(wp: threadSet_obj_at'_strongish crunch_wps)
end
lemma sbn_tcbFault:
"\<lbrace>obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace>
setBoundNotification st t'
\<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace>"
apply (simp add: setBoundNotification_def)
apply (wp threadSet_obj_at' | simp)+
apply (wp threadSet_obj_at' | simp cong: if_cong)+
done
crunch tcbFault: unbindNotification, unbindMaybeNotification "obj_at' (\<lambda>tcb. P (tcbFault tcb)) t"
@ -4431,7 +4439,7 @@ proof (rule hoare_gen_asm, induct caps arbitrary: x mi destSlots)
next
case (Cons cp cps)
show ?case using Cons.prems
by (wpsimp wp: Cons.hyps cteInsert_weak_cte_wp_at2 simp: Let_def split_def weak)
by (wpsimp wp: Cons.hyps cteInsert_weak_cte_wp_at2 simp: Let_def split_def weak cong: if_cong)
qed
lemma transferCaps_local_slots:
@ -4534,7 +4542,7 @@ proof -
apply ceqv
apply csymbr
apply wpc
apply (clarsimp simp: ccorres_cond_iffs split del: if_split)
apply (clarsimp simp: ccorres_cond_iffs)
apply (fold dc_def)[1]
apply (rule ccorres_rhs_assoc)+
apply (ctac(no_vcg))
@ -6733,6 +6741,7 @@ lemma receiveSignal_ccorres [corres]:
(receiveSignal thread cap is_blocking)
(Call receiveSignal_'proc)"
unfolding K_def
supply if_cong[cong]
apply (rule ccorres_gen_asm)
apply (cinit lift: thread_' cap_' isBlocking_')
apply (rule ccorres_pre_getNotification, rename_tac ntfn)

8
proof/crefine/ARM_HYP/IsolatedThreadAction.thy
View File

@ -808,6 +808,7 @@ lemma vcpuDisable_isolatable:
lemma vcpuSwitch_isolatable:
"thread_actions_isolatable idx (vcpuSwitch v)"
supply if_cong[cong] option.case_cong[cong]
apply (clarsimp simp: vcpuSwitch_def when_def split: option.splits)
apply (safe intro!:
thread_actions_isolatable_bind[OF _ _ hoare_pre(1)]
@ -966,6 +967,7 @@ lemma doIPCTransfer_simple_rewrite:
y \<leftarrow> setMessageInfo rcvr ((messageInfoFromWord msgInfo) \<lparr>msgCapsUnwrapped := 0\<rparr>);
asUser rcvr (setRegister ARM_HYP_H.badgeRegister badge)
od)"
supply if_cong[cong]
apply (rule monadic_rewrite_gen_asm)
apply (simp add: doIPCTransfer_def bind_assoc doNormalTransfer_def
getMessageInfo_def
@ -1420,6 +1422,7 @@ lemma assert_isolatable:
lemma cteInsert_isolatable:
"thread_actions_isolatable idx (cteInsert cap src dest)"
supply if_cong[cong]
apply (simp add: cteInsert_def updateCap_def updateMDB_def
Let_def setUntypedCapAsFull_def)
apply (intro thread_actions_isolatable_bind[OF _ _ hoare_pre(1)]
@ -1750,6 +1753,7 @@ lemma updateMDB_isolatable:
lemma clearUntypedFreeIndex_isolatable:
"thread_actions_isolatable idx (clearUntypedFreeIndex slot)"
supply option.case_cong[cong]
apply (simp add: clearUntypedFreeIndex_def getSlotCap_def)
apply (rule thread_actions_isolatable_bind)
apply (rule getCTE_isolatable)
@ -1787,6 +1791,7 @@ lemmas fastpath_isolate_rewrites
lemma lookupIPCBuffer_isolatable:
"thread_actions_isolatable idx (lookupIPCBuffer w t)"
supply if_cong[cong]
apply (simp add: lookupIPCBuffer_def)
apply (rule thread_actions_isolatable_bind)
apply (clarsimp simp: put_tcb_state_regs_tcb_def threadGet_isolatable
@ -1795,11 +1800,10 @@ lemma lookupIPCBuffer_isolatable:
apply (rule thread_actions_isolatable_bind)
apply (clarsimp simp: thread_actions_isolatable_return
getCTE_isolatable
assert_isolatable
split: capability.split arch_capability.split bool.split)+
apply (rule thread_actions_isolatable_if)
apply (rule thread_actions_isolatable_bind)
apply (simp add: assert_isolatable thread_actions_isolatable_return | wp)+
apply (simp add: thread_actions_isolatable_return | wp)+
done
lemma setThreadState_rewrite_simple:

1
proof/crefine/ARM_HYP/Recycle_C.thy
View File

@ -1344,4 +1344,5 @@ lemma ccap_relation_isDeviceCap2:
apply (frule cap_get_tag_UntypedCap)
apply (simp add:cap_get_tag_isCap to_bool_def)
done
end

1
proof/crefine/ARM_HYP/Refine_C.thy
View File

@ -839,6 +839,7 @@ lemma user_memory_update_corres_C:
(\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> dom um \<subseteq> dom (user_mem' s))
\<top>
(doMachineOp (user_memory_update um)) (setUserMem_C um)"
supply option.case_cong[cong]
apply (clarsimp simp: corres_underlying_def)
apply (rule conjI)
prefer 2

19
proof/crefine/ARM_HYP/Retype_C.thy
View File

@ -871,6 +871,7 @@ lemma clift_ptr_retyps_gen_memset_same:
= (\<lambda>y. if y \<in> (CTypesDefs.ptr_add (Ptr p :: 'a :: mem_type ptr) o of_nat) ` {k. k < n}
then Some (from_bytes (replicate (size_of TYPE('a :: mem_type)) 0)) else clift hrs y)"
using sz
supply if_cong[cong]
apply (simp add: nb liftt_if[folded hrs_mem_def hrs_htd_def]
hrs_htd_update hrs_mem_update
h_t_valid_ptr_retyps_gen_same[OF guard cleared not_byte]
@ -915,9 +916,9 @@ lemma clift_ptr_retyps_gen_other:
= clift hrs"
using sz cleared
apply (cases p)
apply (simp add: liftt_if[folded hrs_mem_def hrs_htd_def]
h_t_valid_def hrs_htd_update
ptr_retyps_gen_valid_footprint[simplified addr_card_wb, OF _ other not_byte sz])
apply (simp add: liftt_if[folded hrs_mem_def hrs_htd_def] h_t_valid_def hrs_htd_update
ptr_retyps_gen_valid_footprint[simplified addr_card_wb, OF _ other not_byte sz]
cong: if_cong)
done
lemma clift_heap_list_update_no_heap_other:
@ -2724,6 +2725,7 @@ lemma insertNewCap_ccorres1:
\<inter> {s. slot_' s = Ptr slot}) []
(insertNewCap parent slot cap)
(Call insertNewCap_'proc)"
supply if_cong[cong] option.case_cong[cong]
apply (cinit (no_ignore_call) lift: cap_' parent_' slot_')
apply (rule ccorres_liftM_getCTE_cte_at)
apply (rule ccorres_move_c_guard_cte)
@ -3846,7 +3848,7 @@ lemma zero_ranges_are_zero_update_zero[simp]:
\<Longrightarrow> zero_ranges_are_zero rs (hrs_mem_update (heap_update_list ptr (replicate n 0)) hrs)"
apply (clarsimp simp: zero_ranges_are_zero_def hrs_mem_update)
apply (drule(1) bspec)
apply (clarsimp simp: heap_list_eq_replicate_eq_eq heap_update_list_replicate_eq)
apply (clarsimp simp: heap_list_eq_replicate_eq_eq heap_update_list_replicate_eq cong: if_cong)
done
lemma rf_sr_rep0:
@ -4957,8 +4959,7 @@ proof (intro impI allI)
hence "cpspace_relation ?ks (underlying_memory (ksMachineState \<sigma>)) ?ks'"
unfolding cpspace_relation_def
using empty rc' szo
apply -
using empty rc' szo if_cong[cong]
apply (clarsimp simp: rl' tag_disj_via_td_name cte_C_size ht_rl
clift_ptr_retyps_gen_other
foldr_upd_app_if [folded data_map_insert_def])
@ -4975,10 +4976,9 @@ proof (intro impI allI)
thus ?thesis using rf empty kdr rzo
apply (simp add: rf_sr_def cstate_relation_def Let_def rl' tag_disj_via_td_name )
apply (simp add: carch_state_relation_def cmachine_state_relation_def)
apply (simp add: tag_disj_via_td_name rl' tcb_C_size h_t_valid_clift_Some_iff)
apply (simp add: tag_disj_via_td_name rl' h_t_valid_clift_Some_iff)
apply (clarsimp simp: hrs_htd_update szo'[symmetric] cvariable_array_ptr_retyps[OF szo] rb')
apply (subst zero_ranges_ptr_retyps, simp_all only: szo'[symmetric] power_add,
simp)
apply (subst zero_ranges_ptr_retyps, simp_all only: szo'[symmetric] power_add, simp)
apply (simp add:szo p2dist objBits_simps ko_def ptr_retyps_htd_safe_neg
kernel_data_refs_domain_eq_rotate
rl foldr_upd_app_if [folded data_map_insert_def]
@ -8221,6 +8221,7 @@ shows "ccorres dc xfdc
) []
(createNewObjects newType srcSlot destSlots ptr userSize isdev)
(Call createNewObjects_'proc)"
supply if_cong[cong]
apply (rule ccorres_gen_asm_state)
apply clarsimp
apply (subgoal_tac "unat (of_nat (getObjectSize newType userSize)) = getObjectSize newType userSize")

4
proof/crefine/ARM_HYP/Schedule_C.thy
View File

@ -393,8 +393,8 @@ lemma isHighestPrio_ccorres:
supply prio_and_dom_limit_helpers[simp]
supply Collect_const_mem [simp]
(* FIXME: these should likely be in simpset for CRefine, or even in general *)
supply from_bool_eq_if[simp] from_bool_eq_if'[simp] from_bool_0[simp] if_1_0_0[simp]
ccorres_IF_True[simp]
supply from_bool_eq_if[simp] from_bool_eq_if'[simp] from_bool_0[simp]
ccorres_IF_True[simp] if_cong[cong]
apply (cinit lift: dom_' prio_')
apply clarsimp
apply (rule ccorres_move_const_guard)

1
proof/crefine/ARM_HYP/SyscallArgs_C.thy
View File

@ -1018,6 +1018,7 @@ lemma getMRs_user_word:
\<and> msgLength info \<le> msgMaxLength \<and> i >= scast n_msgRegisters\<rbrace>
getMRs thread (Some buffer) info
\<lbrace>\<lambda>xs. user_word_at (xs ! unat i) (buffer + (i * 4 + 4))\<rbrace>"
supply if_cong[cong]
apply (rule hoare_assume_pre)
apply (elim conjE)
apply (thin_tac "valid_ipc_buffer_ptr' x y" for x y)

7
proof/crefine/ARM_HYP/Syscall_C.thy
View File

@ -609,7 +609,7 @@ lemma sendFaultIPC_ccorres:
\<inter> {s. tptr_' s = tcb_ptr_to_ctcb_ptr tptr})
[] (sendFaultIPC tptr fault)
(Call sendFaultIPC_'proc)"
supply Collect_const[simp del]
supply Collect_const[simp del] if_cong[cong]
apply (cinit lift: tptr_' cong: call_ignore_cong)
apply (simp add: liftE_bindE del:Collect_const cong:call_ignore_cong)
apply (rule ccorres_symb_exec_r)
@ -803,7 +803,7 @@ lemma getMRs_length:
apply simp
apply (wp mapM_length)
apply (simp add: min_def length_msgRegisters)
apply (clarsimp simp: n_msgRegisters_def)
apply (clarsimp simp: n_msgRegisters_def cong: if_cong)
apply (simp add: getMRs_def)
apply (rule hoare_pre, wp)
apply simp
@ -1254,7 +1254,7 @@ lemma not_obj_at'_ntfn:
done
lemma handleRecv_ccorres:
notes rf_sr_upd_safe[simp del]
notes rf_sr_upd_safe[simp del] if_cong[cong]
shows
"ccorres dc xfdc
(\<lambda>s. invs' s \<and> st_tcb_at' simple' (ksCurThread s) s
@ -1853,6 +1853,7 @@ proof -
using word_ctz_le[where w=w, simplified] by (auto simp: unat_of_nat_eq)
show ?thesis
supply if_cong[cong]
apply (cinit)
apply (rule ccorres_pre_getCurVCPU, rename_tac vcpuPtr_opt)
apply wpc

27
proof/crefine/ARM_HYP/VSpace_C.thy
View File

@ -621,8 +621,8 @@ lemma generic_frame_cap_get_capFIsMapped_spec:
Call generic_frame_cap_get_capFIsMapped_'proc
\<lbrace>\<acute>ret__unsigned_long = (if generic_frame_cap_get_capFMappedASID_CL (cap_lift \<^bsup>s\<^esup>cap) \<noteq> 0 then 1 else 0)\<rbrace>"
apply vcg
apply (clarsimp simp: generic_frame_cap_get_capFMappedASID_CL_def if_distrib [where f=scast])
done
apply (clarsimp simp: generic_frame_cap_get_capFMappedASID_CL_def if_distrib [where f=scast] cong: if_cong)
done
@ -2032,6 +2032,7 @@ lemma vcpu_disable_ccorres:
and (case v of None \<Rightarrow> \<top> | Some new \<Rightarrow> vcpu_at' new))
(UNIV \<inter> {s. vcpu_' s = option_to_ptr v}) hs
(vcpuDisable v) (Call vcpu_disable_'proc)"
supply if_cong[cong] option.case_cong[cong]
apply (cinit lift: vcpu_')
apply (ctac (no_vcg) add: dsb_ccorres)
apply (rule ccorres_split_nothrow_novcg)
@ -2274,6 +2275,7 @@ lemma vcpu_save_ccorres:
(UNIV \<inter> {s. vcpu_' s = case_option NULL (vcpu_Ptr \<circ> fst) v}
\<inter> {s. active_' s = case_option 0 (from_bool \<circ> snd) v}) hs
(vcpuSave v) (Call vcpu_save_'proc)"
supply if_cong[cong] option.case_cong[cong]
apply (cinit lift: vcpu_' active_' simp: whileAnno_def)
apply wpc
(* v = None *)
@ -2377,6 +2379,7 @@ lemma vcpu_switch_ccorres_Some:
and valid_arch_state' and vcpu_at' v)
(UNIV \<inter> {s. new_' s = vcpu_Ptr v}) hs
(vcpuSwitch (Some v)) (Call vcpu_switch_'proc)"
supply if_cong[cong] option.case_cong[cong]
apply (cinit lift: new_')
(* v \<noteq> None *)
apply simp
@ -3198,6 +3201,7 @@ lemma ccorres_return_void_C':
lemma is_aligned_cache_preconds:
"\<lbrakk>is_aligned rva n; n \<ge> 7\<rbrakk> \<Longrightarrow> rva \<le> rva + 0x7F \<and>
addrFromPPtr rva \<le> addrFromPPtr rva + 0x7F \<and> rva && mask 6 = addrFromPPtr rva && mask 6"
supply if_cong[cong]
apply (drule is_aligned_weaken, simp)
apply (rule conjI)
apply (drule is_aligned_no_overflow, simp, unat_arith)[1]
@ -3948,37 +3952,38 @@ lemma makeUserPDE_spec:
HAP_CL = hap_from_vm_rights (vmrights_to_H \<^bsup>s\<^esup>vm_rights),
MemAttr_CL = memattr_from_cacheable (to_bool \<^bsup>s\<^esup>cacheable)
\<rparr>) \<rbrace>"
supply if_cong[cong]
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: hap_from_vm_rights_mask split: if_splits)
apply (intro conjI impI allI | clarsimp )+
apply (simp only: pde_pde_section_lift pde_pde_section_lift_def)
apply (simp add: vmsz_aligned'_def gen_framesize_to_H_def hap_from_vm_rights_mask)
apply (clarsimp simp: Kernel_C.ARMSection_def Kernel_C.ARMSmallPage_def
Kernel_C.ARMLargePage_def)
Kernel_C.ARMLargePage_def)
apply (fastforce simp:mask_def hap_from_vm_rights_mask memattr_from_cacheable_def
split:if_splits dest!:mask_eq1_nochoice intro: is_aligned_neg_mask_weaken)
split:if_splits dest!:mask_eq1_nochoice intro: is_aligned_neg_mask_weaken)
apply (simp only: pde_pde_section_lift pde_pde_section_lift_def)
apply (simp add: vmsz_aligned'_def gen_framesize_to_H_def hap_from_vm_rights_mask)
apply (clarsimp simp: Kernel_C.ARMSection_def Kernel_C.ARMSmallPage_def
Kernel_C.ARMLargePage_def is_aligned_neg_mask_eq)
apply (fastforce simp:mask_def hap_from_vm_rights_mask memattr_from_cacheable_def
split:if_splits dest!:mask_eq1_nochoice intro: is_aligned_neg_mask_weaken)
Kernel_C.ARMLargePage_def)
apply (fastforce simp:mask_def hap_from_vm_rights_mask memattr_from_cacheable_def
split:if_splits dest!:mask_eq1_nochoice intro: is_aligned_neg_mask_weaken)
apply (clarsimp)
apply (intro conjI impI allI)
apply (simp add:pde_pde_section_lift pde_pde_section_lift_def)
apply (simp add: vmsz_aligned'_def gen_framesize_to_H_def hap_from_vm_rights_mask)
apply (drule is_aligned_weaken[where y = 21])
apply (clarsimp simp: Kernel_C.ARMSuperSection_def Kernel_C.ARMSmallPage_def
Kernel_C.ARMLargePage_def is_aligned_neg_mask_eq)+
Kernel_C.ARMLargePage_def)+
apply (fastforce simp:mask_def hap_from_vm_rights_mask memattr_from_cacheable_def
split:if_splits dest!:mask_eq1_nochoice intro: is_aligned_neg_mask_weaken)
apply (simp add:pde_pde_section_lift pde_pde_section_lift_def)
apply (simp add: vmsz_aligned'_def gen_framesize_to_H_def hap_from_vm_rights_mask)
apply (drule is_aligned_weaken[where y = 21])
apply (clarsimp simp: Kernel_C.ARMSuperSection_def Kernel_C.ARMSmallPage_def
Kernel_C.ARMLargePage_def is_aligned_neg_mask_eq)+
apply (fastforce simp:mask_def hap_from_vm_rights_mask memattr_from_cacheable_def
split:if_splits dest!:mask_eq1_nochoice intro: is_aligned_neg_mask_weaken)
Kernel_C.ARMLargePage_def)+
apply (fastforce simp:mask_def hap_from_vm_rights_mask memattr_from_cacheable_def
split:if_splits dest!:mask_eq1_nochoice intro: is_aligned_neg_mask_weaken)
done
lemma makeUserPTE_spec: