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

proofs: updates for monad refactor 

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2023-01-30 17:31:34 +11:00
parent 409d780e07
commit e89813ecf2
No known key found for this signature in database
GPG Key ID: 20A847CE6AB7F5F3
155 changed files with 597 additions and 682 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
lib/Hoare_Sep_Tactics/Hoare_Sep_Tactics.thy
View File

@ -81,14 +81,14 @@ schematic_goal strong_sep_impl_sep_wp':
"\<And>sep_lift.
(\<And>R. \<lbrace>(\<lambda>s. (P \<and>* R) (sep_lift s) )\<rbrace> f \<lbrace>\<lambda>rv. (\<lambda>s. (Q rv \<and>* R) (sep_lift s))\<rbrace>) \<Longrightarrow>
\<lbrace>(\<lambda>s. ( P \<and>* (?f Q R)) (sep_lift s))\<rbrace> f \<lbrace>\<lambda>rv s . R rv (sep_lift s)\<rbrace>"
apply (atomize)
apply (erule_tac x="(\<lambda>s. \<forall>x. (Q x \<longrightarrow>* R x) s)" in allE)
apply (rule hoare_strengthen_post)
apply (assumption)
apply (sep_drule (direct) extract_all)
apply (erule_tac x=r in allE)
apply (sep_solve)
done
apply (atomize)
apply (erule_tac x="(\<lambda>s. \<forall>x. (Q x \<longrightarrow>* R x) s)" in allE)
apply (erule hoare_strengthen_post)
apply (rename_tac rv s)
apply (sep_drule (direct) extract_all)
apply (erule_tac x=rv in allE)
apply (sep_solve)
done
lemma strong_sep_impl_sep_wp'':
"\<And>sep_lift.

5
proof/access-control/ARM/ArchArch_AC.thy
View File

@ -959,8 +959,9 @@ lemma delete_asid_pool_pas_refined [wp]:
crunch respects[wp]: invalidate_asid_entry "integrity aag X st"
crunch respects[wp]: flush_space "integrity aag X st"
(ignore: do_machine_op simp: invalidateLocalTLB_ASID_def cleanCaches_PoU_def
dsb_def clean_D_PoU_def invalidate_I_PoU_def do_machine_op_bind)
(ignore: do_machine_op
simp: invalidateLocalTLB_ASID_def cleanCaches_PoU_def dsb_def clean_D_PoU_def invalidate_I_PoU_def
do_machine_op_bind empty_fail_cond)
lemma delete_asid_pool_respects[wp]:
"\<lbrace>integrity aag X st and

2
proof/capDL-api/IRQ_DP.thy
View File

@ -123,7 +123,7 @@ lemma decode_irq_control_issue_irq_rv:
done
schematic_goal lookup_extra_caps_once_wp: "\<lbrace>?P\<rbrace> lookup_extra_caps root_tcb_id [endpoint_cptr] \<lbrace>Q\<rbrace>, \<lbrace>Q'\<rbrace>"
apply (clarsimp simp: lookup_extra_caps_def mapME_def sequenceE_def, wp, clarsimp)
apply (clarsimp simp: lookup_extra_caps_def mapME_def sequenceE_def, wp)
apply (rule lookup_cap_and_slot_rvu)
done

17
proof/capDL-api/Invocation_DP.thy
View File

@ -622,13 +622,7 @@ lemma invoke_cnode_insert_cap:
apply (simp add:validE_def)
apply (rule hoare_name_pre_state)
apply (clarsimp simp:invoke_cnode_def liftE_bindE validE_def[symmetric])
apply (rule alternative_wp)
apply (rule hoare_pre)
apply (rule insert_cap_sibling_wp)
apply simp
apply (rule hoare_pre)
apply (rule insert_cap_child_wp)
apply simp
apply (wpsimp wp: alternative_wp insert_cap_sibling_wp insert_cap_child_wp)
done
lemma invoke_cnode_move_wp:
@ -1136,13 +1130,8 @@ lemma invoke_cnode_insert_cap':
apply (simp add:validE_def)
apply (rule hoare_name_pre_state)
apply (clarsimp simp:invoke_cnode_def liftE_bindE validE_def[symmetric])
apply (rule alternative_wp)
apply (rule hoare_pre)
apply (rule insert_cap_sibling_wp)
apply (simp add:cap_of_insert_call_def)
apply (rule hoare_pre)
apply (rule insert_cap_child_wp)
apply (simp add:cap_of_insert_call_def)
apply (wpsimp wp: alternative_wp insert_cap_sibling_wp insert_cap_child_wp
simp: cap_of_insert_call_def)
done
lemma object_to_sep_state_slot:

20
proof/capDL-api/KHeap_DP.thy
View File

@ -862,14 +862,9 @@ lemma lookup_cap_rvu :
done
lemma lookup_cap_wp:
"\<lbrace>P\<rbrace>
lookup_cap thread cap_ptr
\<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_ .P \<rbrace> "
apply (clarsimp simp: lookup_cap_def)
apply (wp lookup_slot_wp get_cap_wp)
apply (clarsimp)
apply (wp lookup_slot_wp)
apply assumption
"\<lbrace>P\<rbrace> lookup_cap thread cap_ptr \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_ .P \<rbrace> "
apply (clarsimp simp: lookup_cap_def)
apply (wp lookup_slot_wp get_cap_wp)
done
@ -1119,9 +1114,9 @@ lemma get_thread_sep_wp:
done
lemma get_thread_inv:
"\<lbrace> Q \<rbrace>
get_thread thread \<lbrace>\<lambda>t s. Q s\<rbrace>"
by (simp add:get_thread_def | wp | wpc)+
"\<lbrace> Q \<rbrace> get_thread thread \<lbrace>\<lambda>t s. Q s\<rbrace>"
unfolding get_thread_def
by wpsimp
lemma get_thread_sep_wp_precise:
"\<lbrace>\<lambda>s. tcb_at' (\<lambda>tcb. Q tcb s) thread s \<rbrace>
@ -1145,8 +1140,7 @@ lemma has_restart_cap_sep_wp:
\<lbrace>\<lambda>rv. Q rv\<rbrace>"
apply (rule hoare_name_pre_state)
apply (clarsimp simp: object_at_def)
apply (simp add: object_at_def get_thread_def has_restart_cap_def
| wp+ | wpc | intro conjI)+
apply (wpsimp simp: object_at_def get_thread_def has_restart_cap_def | intro conjI)+
apply (clarsimp dest!: opt_cap_sep_imp
simp: opt_cap_def slots_of_def)
apply (clarsimp simp: object_slots_def)

23
proof/capDL-api/Retype_DP.thy
View File

@ -432,8 +432,7 @@ lemma set_parent_has_children[wp]:
lemma create_cap_has_children[wp]:
"\<lbrace>\<top>\<rbrace> create_cap new_type sz uref slot dev \<lbrace>\<lambda>r. has_children uref\<rbrace>"
apply (clarsimp simp :create_cap_def split_def)
apply wp
apply simp
apply wpsimp
done
abbreviation (input) "retype_with_kids uinv
@ -533,12 +532,10 @@ lemma invoke_untyped_one_wp:
lemma mark_tcb_intent_error_has_children[wp]:
"\<lbrace>\<lambda>s. P (has_children ptr s)\<rbrace>
mark_tcb_intent_error cur_thread b
\<lbrace>\<lambda>rv s. P (has_children ptr s)\<rbrace>"
apply (simp add:has_children_def is_cdt_parent_def
mark_tcb_intent_error_def update_thread_def
set_object_def | wp | wpc)+
done
mark_tcb_intent_error cur_thread b
\<lbrace>\<lambda>rv s. P (has_children ptr s)\<rbrace>"
by (wpsimp simp: has_children_def is_cdt_parent_def mark_tcb_intent_error_def update_thread_def
set_object_def)
crunch cdt[wp]: corrupt_frame "\<lambda>s. P (cdl_cdt s)"
(wp:select_wp simp:crunch_simps corrupt_intents_def)
@ -871,12 +868,10 @@ lemma update_thread_no_pending:
K(\<forall>x. (case cdl_tcb_caps x tcb_pending_op_slot of Some cap \<Rightarrow> \<not> is_pending_cap cap | _ \<Rightarrow> True)\<longrightarrow>
(case cdl_tcb_caps (t x) tcb_pending_op_slot of Some cap \<Rightarrow> \<not> is_pending_cap cap | _ \<Rightarrow> True))\<rbrace>
update_thread thread_ptr t \<lbrace>\<lambda>rv. no_pending\<rbrace>"
apply (simp add: update_thread_def set_object_def | (wp modify_wp)+ | wpc)+
apply (clarsimp simp: no_pending_def)
apply (drule_tac x = oid in spec)
apply (clarsimp simp: opt_cap_def slots_of_def
object_slots_def
split: if_splits option.splits)
unfolding update_thread_def set_object_def
apply wpsimp
apply (fastforce simp: opt_cap_def slots_of_def object_slots_def no_pending_def
split: if_splits option.splits)
done
lemma update_thread_tcb_at:

3
proof/capDL-api/TCB_DP.thy
View File

@ -1222,8 +1222,9 @@ lemma seL4_TCB_WriteRegisters_wp:
apply (wp do_kernel_op_pull_back)
apply (rule hoare_post_imp[OF _ call_kernel_with_intent_allow_error_helper
[where check = False,simplified]])
apply (rename_tac rv s)
apply clarsimp
apply (case_tac r,(clarsimp,assumption)+)[1]
apply (case_tac rv, (clarsimp,assumption)+)[1]
apply fastforce
apply (rule hoare_strengthen_post[OF set_cap_wp])
apply (sep_select 3,sep_cancel)

44
proof/crefine/ARM/ArchMove_C.thy
View File

@ -82,21 +82,13 @@ lemma setCTE_asidpool':
lemma empty_fail_findPDForASID[iff]:
"empty_fail (findPDForASID asid)"
apply (simp add: findPDForASID_def liftME_def)
apply (intro empty_fail_bindE, simp_all split: option.split)
apply (simp add: assertE_def split: if_split)
apply (simp add: assertE_def split: if_split)
apply (simp add: empty_fail_getObject)
apply (simp add: assertE_def liftE_bindE checkPDAt_def split: if_split)
done
unfolding findPDForASID_def checkPDAt_def
by (wpsimp wp: empty_fail_getObject)
lemma empty_fail_findPDForASIDAssert[iff]:
"empty_fail (findPDForASIDAssert asid)"
apply (simp add: findPDForASIDAssert_def catch_def
checkPDAt_def checkPDUniqueToASID_def
checkPDASIDMapMembership_def)
apply (intro empty_fail_bind, simp_all split: sum.split)
done
unfolding findPDForASIDAssert_def checkPDAt_def checkPDUniqueToASID_def checkPDASIDMapMembership_def
by (wpsimp wp: empty_fail_getObject)
crunches Arch.switchToThread
for valid_queues'[wp]: valid_queues'
@ -209,7 +201,7 @@ lemma cap_case_isPageDirectoryCap:
lemma empty_fail_loadWordUser[intro!, simp]:
"empty_fail (loadWordUser x)"
by (simp add: loadWordUser_def ef_loadWord ef_dmo')
by (fastforce simp: loadWordUser_def ef_loadWord ef_dmo')
lemma empty_fail_getMRs[iff]:
"empty_fail (getMRs t buf mi)"
@ -219,26 +211,14 @@ lemma empty_fail_getReceiveSlots:
"empty_fail (getReceiveSlots r rbuf)"
proof -
note
empty_fail_assertE[iff]
empty_fail_resolveAddressBits[iff]
empty_fail_resolveAddressBits[wp]
empty_fail_rethrowFailure[wp]
empty_fail_rethrowFailure[wp]
show ?thesis
apply (clarsimp simp: getReceiveSlots_def loadCapTransfer_def split_def
split: option.split)
apply (rule empty_fail_bind)
apply (simp add: capTransferFromWords_def)
apply (simp add: emptyOnFailure_def unifyFailure_def)
apply (intro empty_fail_catch empty_fail_bindE empty_fail_rethrowFailure,
simp_all add: empty_fail_whenEs)
apply (simp_all add: lookupCap_def split_def lookupCapAndSlot_def
lookupSlotForThread_def liftME_def
getThreadCSpaceRoot_def locateSlot_conv bindE_assoc
lookupSlotForCNodeOp_def lookupErrorOnFailure_def
cong: if_cong)
apply (intro empty_fail_bindE,
simp_all add: getSlotCap_def)
apply (intro empty_fail_If empty_fail_bindE empty_fail_rethrowFailure impI,
simp_all add: empty_fail_whenEs rangeCheck_def)
done
unfolding getReceiveSlots_def loadCapTransfer_def lookupCap_def lookupCapAndSlot_def
by (wpsimp simp: emptyOnFailure_def unifyFailure_def lookupSlotForThread_def
capTransferFromWords_def getThreadCSpaceRoot_def locateSlot_conv bindE_assoc
lookupSlotForCNodeOp_def lookupErrorOnFailure_def rangeCheck_def)
qed
lemma user_getreg_rv:

2
proof/crefine/ARM/CLevityCatch.thy
View File

@ -66,7 +66,7 @@ lemma asUser_get_registers:
apply (simp add: mapM_empty asUser_return)
apply wp
apply simp
apply (simp add: mapM_Cons asUser_bind_distrib asUser_return)
apply (simp add: mapM_Cons asUser_bind_distrib asUser_return empty_fail_cond)
apply wp
apply simp
apply (rule hoare_strengthen_post)

2
proof/crefine/ARM/Fastpath_Equiv.thy
View File

@ -864,7 +864,7 @@ lemma receiveIPC_simple_rewrite:
lemma empty_fail_isFinalCapability:
"empty_fail (isFinalCapability cte)"
by (simp add: isFinalCapability_def Let_def split: if_split)
by (simp add: isFinalCapability_def Let_def empty_fail_cond split: if_split)
lemma cteDeleteOne_replycap_rewrite:
"monadic_rewrite True False

3
proof/crefine/ARM/IpcCancel_C.thy
View File

@ -2216,6 +2216,7 @@ lemma scheduleTCB_ccorres':
rescheduleRequired
od)
(Call scheduleTCB_'proc)"
supply empty_fail_cond[simp]
apply (cinit' lift: tptr_')
apply (rule ccorres_rhs_assoc2)+
apply (rule_tac xf'="ret__int_'" in ccorres_split_nothrow_novcg)
@ -2270,6 +2271,7 @@ lemma scheduleTCB_ccorres_valid_queues'_pre:
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) rescheduleRequired
od)
(Call scheduleTCB_'proc)"
supply empty_fail_cond[simp]
apply (cinit' lift: tptr_' simp del: word_neq_0_conv)
apply (rule ccorres_rhs_assoc2)+
apply (rule_tac xf'="ret__int_'" in ccorres_split_nothrow_novcg)
@ -2362,6 +2364,7 @@ lemma scheduleTCB_ccorres_valid_queues'_pre_simple:
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) rescheduleRequired
od)
(Call scheduleTCB_'proc)"
supply empty_fail_cond[simp]
apply (cinit' lift: tptr_' simp del: word_neq_0_conv)
apply (rule ccorres_rhs_assoc2)+
apply (rule_tac xf'="ret__int_'" in ccorres_split_nothrow_novcg)

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

@ -377,6 +377,7 @@ lemma handleArchFaultReply':
msg \<leftarrow> getMRs s sb tag;
handleArchFaultReply f r (msgLabel tag) msg
od) x' = handleArchFaultReply' f s r tag x'"
supply empty_fail_cond[simp]
apply (unfold handleArchFaultReply'_def getMRs_def msgMaxLength_def
bit_def msgLengthBits_def msgRegisters_unfold
fromIntegral_simp1 fromIntegral_simp2
@ -461,6 +462,7 @@ lemma handleFaultReply':
msg \<leftarrow> getMRs s sb tag;
handleFaultReply f r (msgLabel tag) msg
od) (handleFaultReply' f s r)"
supply empty_fail_cond[simp]
apply (unfold handleFaultReply'_def getMRs_def msgMaxLength_def
bit_def msgLengthBits_def msgRegisters_unfold
fromIntegral_simp1 fromIntegral_simp2
@ -1607,6 +1609,7 @@ proof -
let ?obj_at_ft = "obj_at' (\<lambda>tcb. tcbFault tcb = Some ft) sender"
note symb_exec_r_fault = ccorres_symb_exec_r_known_rv_UNIV
[where xf'=ret__unsigned_' and R="?obj_at_ft" and R'=UNIV]
note empty_fail_cond[simp]
show ?thesis
apply (unfold K_def)
apply (intro ccorres_gen_asm)
@ -2919,6 +2922,7 @@ proof -
let ?curr = "\<lambda>s. current_extra_caps_' (globals s)"
let ?EXCNONE = "{s. ret__unsigned_long_' s = scast EXCEPTION_NONE}"
let ?interpret = "\<lambda>v n. take n (array_to_list (excaprefs_C v))"
note empty_fail_cond[simp]
show ?thesis
apply (rule ccorres_gen_asm)+
apply (cinit(no_subst_asm) lift: thread_' bufferPtr_' info_' simp: whileAnno_def)

5
proof/crefine/ARM/IsolatedThreadAction.thy
View File

@ -345,6 +345,9 @@ lemma getObject_get_assert:
apply (simp add: lookupAround2_known1 assert_opt_def
obj_at'_def projectKO_def2
split: option.split)
apply (rule conjI)
apply (clarsimp simp: fail_def fst_return conj_comms project_inject
objBits_def bind_def simpler_gets_def)
apply (clarsimp simp: fail_def fst_return conj_comms project_inject
objBits_def)
apply (simp only: assert2[symmetric],
@ -757,7 +760,7 @@ lemma doIPCTransfer_simple_rewrite:
(* FIXME move *)
lemma empty_fail_isRunnable[intro!, wp, simp]:
"empty_fail (isRunnable t)"
by (simp add: isRunnable_def isStopped_def)
by (simp add: isRunnable_def isStopped_def empty_fail_cond)
lemma setupCallerCap_rewrite:
"monadic_rewrite True True (\<lambda>s. reply_masters_rvk_fb (ctes_of s))

13
proof/crefine/ARM/Machine_C.thy
View File

@ -442,7 +442,7 @@ lemma cleanInvalidateCacheRange_RAM_ccorres:
apply (rule ccorres_basic_srnoop)
apply (simp add: cleanInvalidateCacheRange_RAM_def doMachineOp_bind
empty_fail_dsb empty_fail_cleanInvalidateL2Range
empty_fail_cleanInvalByVA)
empty_fail_cleanInvalByVA empty_fail_cond)
apply (ctac (no_vcg) add: cleanCacheRange_PoC_ccorres)
apply (ctac (no_vcg) add: dsb_ccorres)
apply (ctac (no_vcg) add: cleanInvalidateL2Range_ccorres)
@ -474,7 +474,8 @@ lemma cleanCacheRange_RAM_ccorres:
(doMachineOp (cleanCacheRange_RAM w1 w2 w3))
(Call cleanCacheRange_RAM_'proc)"
apply (cinit' lift: start_' end_' pstart_')
apply (simp add: cleanCacheRange_RAM_def doMachineOp_bind empty_fail_dsb empty_fail_cleanL2Range)
apply (simp add: cleanCacheRange_RAM_def doMachineOp_bind empty_fail_dsb empty_fail_cleanL2Range
empty_fail_cond)
apply (rule ccorres_Guard_Seq)
apply (rule ccorres_basic_srnoop2, simp)
apply (ctac (no_vcg) add: cleanCacheRange_PoC_ccorres)
@ -536,8 +537,8 @@ lemma invalidateCacheRange_RAM_ccorres:
apply (clarsimp simp: word_sle_def whileAnno_def split del: if_split)
apply (ccorres_remove_UNIV_guard)
apply (simp add: invalidateCacheRange_RAM_def doMachineOp_bind when_def
if_split_empty_fail empty_fail_invalidateL2Range empty_fail_invalidateByVA
empty_fail_dsb dmo_if
empty_fail_invalidateL2Range empty_fail_invalidateByVA
empty_fail_dsb dmo_if empty_fail_cond
split del: if_split)
apply (rule ccorres_split_nothrow_novcg)
apply (rule ccorres_cond[where R=\<top>])
@ -646,7 +647,7 @@ lemma cleanCaches_PoU_ccorres:
(doMachineOp cleanCaches_PoU)
(Call cleanCaches_PoU_'proc)"
apply cinit'
apply (simp add: cleanCaches_PoU_def doMachineOp_bind
apply (simp add: cleanCaches_PoU_def doMachineOp_bind empty_fail_cond
empty_fail_dsb empty_fail_clean_D_PoU empty_fail_invalidate_I_PoU)
apply (ctac (no_vcg) add: dsb_ccorres)
apply (ctac (no_vcg) add: clean_D_PoU_ccorres)
@ -672,7 +673,7 @@ lemma setCurrentPD_ccorres:
(Call setCurrentPD_'proc)"
apply cinit'
apply (clarsimp simp: setCurrentPD_def doMachineOp_bind empty_fail_dsb empty_fail_isb
writeTTBR0_empty_fail
writeTTBR0_empty_fail empty_fail_cond
intro!: ccorres_cond_empty)
apply (rule ccorres_rhs_assoc)+
apply (ctac (no_vcg) add: dsb_ccorres)

13
proof/crefine/ARM/Retype_C.thy
View File

@ -2103,8 +2103,8 @@ lemma getCTE_pre_cte_at:
apply clarsimp
done
lemmas ccorres_guard_from_wp_liftM = ccorres_guard_from_wp [OF liftM_pre iffD2 [OF empty_fail_liftM]]
lemmas ccorres_guard_from_wp_bind_liftM = ccorres_guard_from_wp_bind [OF liftM_pre iffD2 [OF empty_fail_liftM]]
lemmas ccorres_guard_from_wp_liftM = ccorres_guard_from_wp [OF liftM_pre empty_fail_liftM]
lemmas ccorres_guard_from_wp_bind_liftM = ccorres_guard_from_wp_bind [OF liftM_pre empty_fail_liftM]
lemmas ccorres_liftM_getCTE_cte_at = ccorres_guard_from_wp_liftM [OF getCTE_pre_cte_at empty_fail_getCTE]
ccorres_guard_from_wp_bind_liftM [OF getCTE_pre_cte_at empty_fail_getCTE]
@ -5998,7 +5998,8 @@ lemma createObject_caps_overlap_reserved_ret':
apply clarsimp
apply (rule hoare_strengthen_post[OF createNewCaps_caps_overlap_reserved_ret'[where sz = "APIType_capBits ty us"]])
apply assumption
apply (case_tac r,simp)
apply (rename_tac rv s)
apply (case_tac rv,simp)
apply clarsimp
apply (erule caps_overlap_reserved'_subseteq)
apply (rule untypedRange_in_capRange)
@ -6067,7 +6068,8 @@ lemma createObject_IRQHandler:
apply clarsimp
apply (rule hoare_strengthen_post[OF createNewCaps_IRQHandler[where irq = x and P = "\<lambda>_ _. False"]])
apply assumption
apply (case_tac r,clarsimp+)
apply (rename_tac rv s)
apply (case_tac rv; clarsimp)
apply (clarsimp simp:word_bits_conv)
done
@ -6084,7 +6086,8 @@ lemma createObject_capClass[wp]:
apply clarsimp
apply (rule hoare_strengthen_post[OF createNewCaps_range_helper])
apply assumption
apply (case_tac r,clarsimp+)
apply (rename_tac rv s)
apply (case_tac rv; clarsimp)
apply (clarsimp simp:word_bits_conv )
apply (rule range_cover_full)
apply (simp add:word_bits_conv)+

4
proof/crefine/ARM/SyscallArgs_C.thy
View File

@ -1194,7 +1194,7 @@ lemma getSyscallArg_ccorres_foo:
apply (simp add: index_msgRegisters_less unat_less_helper)
apply wp[1]
apply (wp getMRs_tcbContext)
apply simp
apply fastforce
apply (rule ccorres_seq_skip [THEN iffD2])
apply (rule ccorres_add_return2)
apply (rule ccorres_symb_exec_l)
@ -1218,7 +1218,7 @@ lemma getSyscallArg_ccorres_foo:
in hoare_pre(1))
apply (wp getMRs_user_word)
apply (clarsimp simp: msgMaxLength_def unat_less_helper)
apply simp
apply fastforce
apply (clarsimp simp: sysargs_rel_def sysargs_rel_n_def)
apply (rule conjI, clarsimp simp: unat_of_nat32 word_bits_def)
apply (drule equalityD2)

12
proof/crefine/ARM/Tcb_C.thy
View File

@ -1469,6 +1469,7 @@ lemma invokeTCB_WriteRegisters_ccorres[where S=UNIV]:
\<inter> {s. buffer_' s = option_to_ptr buffer}) []
(invokeTCB (WriteRegisters dst resume values arch))
(Call invokeTCB_WriteRegisters_'proc)"
supply empty_fail_cond[simp]
apply (rule ccorres_gen_asm)
apply (erule conjE)
apply (cinit lift: n_' dest_' resumeTarget_' buffer_'
@ -1707,7 +1708,7 @@ shows
(doE reply \<leftarrow> invokeTCB (ReadRegisters target susp n archCp);
liftE (replyOnRestart thread reply isCall) odE)
(Call invokeTCB_ReadRegisters_'proc)"
supply option.case_cong_weak[cong]
supply option.case_cong_weak[cong] empty_fail_cond[simp]
apply (rule ccorres_gen_asm)
apply (cinit' lift: tcb_src_' suspendSource_' n_' call_'
simp: invokeTCB_def liftE_bindE bind_assoc)
@ -3566,11 +3567,10 @@ lemma decodeSetSchedParams_ccorres:
apply (simp only: cap_get_tag_isCap[symmetric], drule(1) cap_get_tag_to_H)
apply (clarsimp simp: valid_cap'_def capAligned_def interpret_excaps_eq excaps_map_def)
apply (intro conjI impI allI)
apply (clarsimp simp: unat_eq_0 le_max_word_ucast_id
thread_control_update_mcp_def thread_control_update_priority_def
cap_get_tag_isCap_unfolded_H_cap isCap_simps
interpret_excaps_eq excaps_map_def)+
done
by (clarsimp simp: unat_eq_0 le_max_word_ucast_id
thread_control_update_mcp_def thread_control_update_priority_def
cap_get_tag_isCap_unfolded_H_cap isCap_simps
interpret_excaps_eq excaps_map_def)+
lemma decodeSetIPCBuffer_ccorres:
"interpret_excaps extraCaps' = excaps_map extraCaps \<Longrightarrow>

4
proof/crefine/ARM/VSpace_C.thy
View File

@ -1594,7 +1594,9 @@ lemma doFlush_ccorres:
apply (rule ccorres_cond_false)
apply (rule ccorres_cond_false)
apply (rule ccorres_cond_true)
apply (simp add: empty_fail_cleanCacheRange_PoU empty_fail_dsb empty_fail_invalidateCacheRange_I empty_fail_branchFlushRange empty_fail_isb doMachineOp_bind)
apply (simp add: empty_fail_cond empty_fail_cleanCacheRange_PoU empty_fail_dsb
empty_fail_invalidateCacheRange_I empty_fail_branchFlushRange empty_fail_isb
doMachineOp_bind)
apply (rule ccorres_rhs_assoc)+
apply (fold dc_def)
apply (ctac (no_vcg) add: cleanCacheRange_PoU_ccorres)

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

@ -187,21 +187,13 @@ lemma dmo_invalidateCacheRange_RAM_invs'[wp]:
lemma empty_fail_findPDForASID[iff]:
"empty_fail (findPDForASID asid)"
apply (simp add: findPDForASID_def liftME_def)
apply (intro empty_fail_bindE, simp_all split: option.split)
apply (simp add: assertE_def split: if_split)
apply (simp add: assertE_def split: if_split)
apply (simp add: empty_fail_getObject)
apply (simp add: assertE_def liftE_bindE checkPDAt_def split: if_split)
done
unfolding findPDForASID_def checkPDAt_def
by (wpsimp wp: empty_fail_getObject)
lemma empty_fail_findPDForASIDAssert[iff]:
"empty_fail (findPDForASIDAssert asid)"
apply (simp add: findPDForASIDAssert_def catch_def
checkPDAt_def checkPDUniqueToASID_def
checkPDASIDMapMembership_def)
apply (intro empty_fail_bind, simp_all split: sum.split)
done
unfolding findPDForASIDAssert_def checkPDAt_def checkPDUniqueToASID_def checkPDASIDMapMembership_def
by (wpsimp wp: empty_fail_getObject)
lemma vcpu_at_ko:
"vcpu_at' p s \<Longrightarrow> \<exists>vcpu. ko_at' (vcpu::vcpu) p s"
@ -229,7 +221,7 @@ lemma atg_sp':
(* FIXME: MOVE to EmptyFail *)
lemma empty_fail_archThreadGet [intro!, wp, simp]:
"empty_fail (archThreadGet f p)"
by (simp add: archThreadGet_def getObject_def split_def)
by (fastforce simp: archThreadGet_def getObject_def split_def)
lemma mab_gt_2 [simp]:
"2 \<le> msg_align_bits" by (simp add: msg_align_bits)
@ -608,7 +600,7 @@ lemma cap_case_isPageDirectoryCap:
lemma empty_fail_loadWordUser[intro!, simp]:
"empty_fail (loadWordUser x)"
by (simp add: loadWordUser_def ef_loadWord ef_dmo')
by (fastforce simp: loadWordUser_def ef_loadWord ef_dmo')
lemma empty_fail_getMRs[iff]:
"empty_fail (getMRs t buf mi)"
@ -618,26 +610,14 @@ lemma empty_fail_getReceiveSlots:
"empty_fail (getReceiveSlots r rbuf)"
proof -
note
empty_fail_assertE[iff]
empty_fail_resolveAddressBits[iff]
empty_fail_resolveAddressBits[wp]
empty_fail_rethrowFailure[wp]
empty_fail_rethrowFailure[wp]
show ?thesis
apply (clarsimp simp: getReceiveSlots_def loadCapTransfer_def split_def
split: option.split)
apply (rule empty_fail_bind)
apply (simp add: capTransferFromWords_def)
apply (simp add: emptyOnFailure_def unifyFailure_def)
apply (intro empty_fail_catch empty_fail_bindE empty_fail_rethrowFailure,
simp_all add: empty_fail_whenEs)
apply (simp_all add: lookupCap_def split_def lookupCapAndSlot_def
lookupSlotForThread_def liftME_def
getThreadCSpaceRoot_def locateSlot_conv bindE_assoc
lookupSlotForCNodeOp_def lookupErrorOnFailure_def
cong: if_cong)
apply (intro empty_fail_bindE,
simp_all add: getSlotCap_def)
apply (intro empty_fail_If empty_fail_bindE empty_fail_rethrowFailure impI,
simp_all add: empty_fail_whenEs rangeCheck_def)
done
unfolding getReceiveSlots_def loadCapTransfer_def lookupCap_def lookupCapAndSlot_def
by (wpsimp simp: emptyOnFailure_def unifyFailure_def lookupSlotForThread_def
capTransferFromWords_def getThreadCSpaceRoot_def locateSlot_conv bindE_assoc
lookupSlotForCNodeOp_def lookupErrorOnFailure_def rangeCheck_def)
qed
lemma user_getreg_rv:

6
proof/crefine/ARM_HYP/CLevityCatch.thy
View File

@ -64,12 +64,12 @@ 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)
apply (cases sendBuffer; fastforce)
done
lemma empty_fail_loadCapTransfer [intro!, simp]:
"empty_fail (loadCapTransfer a)"
by (simp add: loadCapTransfer_def capTransferFromWords_def)
by (fastforce simp: loadCapTransfer_def capTransferFromWords_def)
lemma empty_fail_emptyOnFailure [intro!, simp]:
"empty_fail m \<Longrightarrow> empty_fail (emptyOnFailure m)"
@ -89,7 +89,7 @@ lemma asUser_get_registers:
apply (simp add: mapM_empty asUser_return)
apply wp
apply simp
apply (simp add: mapM_Cons asUser_bind_distrib asUser_return)
apply (simp add: mapM_Cons asUser_bind_distrib asUser_return empty_fail_cond)
apply wp
apply simp
apply (rule hoare_strengthen_post)

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

@ -867,7 +867,7 @@ lemma receiveIPC_simple_rewrite:
lemma empty_fail_isFinalCapability:
"empty_fail (isFinalCapability cte)"
by (simp add: isFinalCapability_def Let_def split: if_split)
by (simp add: isFinalCapability_def Let_def empty_fail_cond split: if_split)
lemma cteDeleteOne_replycap_rewrite:
"monadic_rewrite True False

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

@ -1334,7 +1334,7 @@ lemma setObject_ccorres_lemma:
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 (simp add: setObject_def split_def empty_fail_cond)
apply (rule ccontr)
apply (clarsimp elim!: nonemptyE)
apply (frule use_valid [OF _ obj_at_setObject3[where P=\<top>]], simp_all)[1]

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

@ -2396,6 +2396,7 @@ lemma scheduleTCB_ccorres':
rescheduleRequired
od)
(Call scheduleTCB_'proc)"
supply empty_fail_cond[simp]
apply (cinit' lift: tptr_' simp del: word_neq_0_conv)
apply (rule ccorres_rhs_assoc2)+
apply (rule_tac xf'="ret__int_'" in ccorres_split_nothrow_novcg)
@ -2450,6 +2451,7 @@ lemma scheduleTCB_ccorres_valid_queues'_pre:
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) rescheduleRequired
od)
(Call scheduleTCB_'proc)"
supply empty_fail_cond[simp]
apply (cinit' lift: tptr_' simp del: word_neq_0_conv)
apply (rule ccorres_rhs_assoc2)+
apply (rule_tac xf'="ret__int_'" in ccorres_split_nothrow_novcg)
@ -2542,6 +2544,7 @@ lemma scheduleTCB_ccorres_valid_queues'_pre_simple:
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) rescheduleRequired
od)
(Call scheduleTCB_'proc)"
supply empty_fail_cond[simp]
apply (cinit' lift: tptr_' simp del: word_neq_0_conv)
apply (rule ccorres_rhs_assoc2)+
apply (rule_tac xf'="ret__int_'" in ccorres_split_nothrow_novcg)

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

@ -466,6 +466,7 @@ lemma handleArchFaultReply':
msg \<leftarrow> getMRs s sb tag;
handleArchFaultReply f r (msgLabel tag) msg
od) x' = handleArchFaultReply' f s r tag x'"
supply empty_fail_cond[simp]
apply (unfold handleArchFaultReply'_def getMRs_def msgMaxLength_def
bit_def msgLengthBits_def msgRegisters_unfold
fromIntegral_simp1 fromIntegral_simp2
@ -628,7 +629,7 @@ lemma handleFaultReply':
msg \<leftarrow> getMRs s sb tag;
handleFaultReply f r (msgLabel tag) msg
od) (handleFaultReply' f s r)"
supply if_cong[cong]
supply if_cong[cong] empty_fail_cond[simp]
supply empty_fail_asUser[wp] empty_fail_getRegister[wp]
apply (unfold handleFaultReply'_def getMRs_def msgMaxLength_def
bit_def msgLengthBits_def msgRegisters_unfold
@ -2013,6 +2014,7 @@ proof -
let ?obj_at_ft = "obj_at' (\<lambda>tcb. tcbFault tcb = Some ft) sender"
note symb_exec_r_fault = ccorres_symb_exec_r_known_rv_UNIV
[where xf'=ret__unsigned_' and R="?obj_at_ft" and R'=UNIV]
note empty_fail_cond[simp]
show ?thesis
apply (unfold K_def)
apply (intro ccorres_gen_asm)
@ -3388,6 +3390,7 @@ proof -
let ?EXCNONE = "{s. ret__unsigned_long_' s = scast EXCEPTION_NONE}"
let ?interpret = "\<lambda>v n. take n (array_to_list (excaprefs_C v))"
note if_split[split del]
note empty_fail_cond[simp]
show ?thesis
apply (rule ccorres_gen_asm)+
apply (cinit(no_subst_asm) lift: thread_' bufferPtr_' info_' simp: whileAnno_def)

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

@ -1016,7 +1016,7 @@ lemma rescheduleRequired_simple_rewrite:
(* FIXME move *)
lemma empty_fail_isRunnable[intro!, wp, simp]:
"empty_fail (isRunnable t)"
by (simp add: isRunnable_def isStopped_def)
by (simp add: isRunnable_def isStopped_def empty_fail_cond)
lemma setupCallerCap_rewrite:
"monadic_rewrite True True (\<lambda>s. reply_masters_rvk_fb (ctes_of s))

15
proof/crefine/ARM_HYP/Machine_C.thy
View File

@ -588,7 +588,7 @@ lemma cleanInvalidateCacheRange_RAM_ccorres:
apply (rule ccorres_basic_srnoop)
apply (simp add: cleanInvalidateCacheRange_RAM_def doMachineOp_bind
empty_fail_dsb empty_fail_cleanInvalidateL2Range
empty_fail_cleanInvalByVA)
empty_fail_cleanInvalByVA empty_fail_cond)
apply (ctac (no_vcg) add: cleanCacheRange_PoC_ccorres)
apply (ctac (no_vcg) add: dsb_ccorres)
apply (ctac (no_vcg) add: plat_cleanInvalidateL2Range_ccorres)
@ -620,7 +620,8 @@ lemma cleanCacheRange_RAM_ccorres:
(doMachineOp (cleanCacheRange_RAM w1 w2 w3))
(Call cleanCacheRange_RAM_'proc)"
apply (cinit' lift: start_' end_' pstart_')
apply (simp add: cleanCacheRange_RAM_def doMachineOp_bind empty_fail_dsb empty_fail_cleanL2Range)
apply (simp add: cleanCacheRange_RAM_def doMachineOp_bind empty_fail_dsb empty_fail_cleanL2Range
empty_fail_cond)
apply (rule ccorres_Guard_Seq)
apply (rule ccorres_basic_srnoop2, simp)
apply (ctac (no_vcg) add: cleanCacheRange_PoC_ccorres)
@ -680,9 +681,9 @@ lemma invalidateCacheRange_RAM_ccorres:
apply (cinit' lift: start_' end_' pstart_')
apply (clarsimp simp: word_sle_def whileAnno_def split del: if_split)
apply (simp add: invalidateCacheRange_RAM_def doMachineOp_bind when_def
if_split_empty_fail empty_fail_invalidateL2Range empty_fail_invalidateByVA
empty_fail_dsb dmo_if
split del: if_split)
empty_fail_invalidateL2Range empty_fail_invalidateByVA
empty_fail_dsb dmo_if empty_fail_cond
split del: if_split)
apply (rule ccorres_split_nothrow_novcg)
apply (rule ccorres_cond[where R=\<top>])
apply (clarsimp simp: lineStart_def cacheLineBits_def)
@ -776,7 +777,7 @@ lemma cleanCaches_PoU_ccorres:
(doMachineOp cleanCaches_PoU)
(Call cleanCaches_PoU_'proc)"
apply cinit'
apply (simp add: cleanCaches_PoU_def doMachineOp_bind
apply (simp add: cleanCaches_PoU_def doMachineOp_bind empty_fail_cond
empty_fail_dsb empty_fail_clean_D_PoU empty_fail_invalidate_I_PoU)
apply (ctac (no_vcg) add: dsb_ccorres)
apply (ctac (no_vcg) add: clean_D_PoU_ccorres)
@ -793,7 +794,7 @@ lemma setCurrentPD_ccorres:
(Call setCurrentPD_'proc)"
apply cinit'
apply (clarsimp simp: setCurrentPD_def doMachineOp_bind empty_fail_dsb empty_fail_isb
setCurrentPDPL2_empty_fail
setCurrentPDPL2_empty_fail empty_fail_cond
intro!: ccorres_cond_empty)
apply (ctac (no_vcg) add: setCurrentPDPL2_ccorres)
apply wpsimp

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

@ -2470,8 +2470,8 @@ lemma getCTE_pre_cte_at:
lemmas ccorres_getCTE_cte_at = ccorres_guard_from_wp [OF getCTE_pre_cte_at empty_fail_getCTE]
ccorres_guard_from_wp_bind [OF getCTE_pre_cte_at empty_fail_getCTE]
lemmas ccorres_guard_from_wp_liftM = ccorres_guard_from_wp [OF liftM_pre iffD2 [OF empty_fail_liftM]]
lemmas ccorres_guard_from_wp_bind_liftM = ccorres_guard_from_wp_bind [OF liftM_pre iffD2 [OF empty_fail_liftM]]
lemmas ccorres_guard_from_wp_liftM = ccorres_guard_from_wp [OF liftM_pre empty_fail_liftM]
lemmas ccorres_guard_from_wp_bind_liftM = ccorres_guard_from_wp_bind [OF liftM_pre empty_fail_liftM]
lemmas ccorres_liftM_getCTE_cte_at = ccorres_guard_from_wp_liftM [OF getCTE_pre_cte_at empty_fail_getCTE]
ccorres_guard_from_wp_bind_liftM [OF getCTE_pre_cte_at empty_fail_getCTE]
@ -7331,7 +7331,8 @@ lemma createObject_caps_overlap_reserved_ret':
apply clarsimp
apply (rule hoare_strengthen_post[OF createNewCaps_caps_overlap_reserved_ret'[where sz = "APIType_capBits ty us"]])
apply assumption
apply (case_tac r,simp)
apply (rename_tac rv s)
apply (case_tac rv,simp)
apply clarsimp
apply (erule caps_overlap_reserved'_subseteq)
apply (rule untypedRange_in_capRange)
@ -7404,7 +7405,8 @@ lemma createObject_IRQHandler:
apply clarsimp
apply (rule hoare_strengthen_post[OF createNewCaps_IRQHandler[where irq = x and P = "\<lambda>_ _. False"]])
apply assumption
apply (case_tac r,clarsimp+)
apply (rename_tac rv s)
apply (case_tac rv; clarsimp)
apply (clarsimp simp:word_bits_conv)
done
@ -7421,7 +7423,8 @@ lemma createObject_capClass[wp]:
apply clarsimp
apply (rule hoare_strengthen_post[OF createNewCaps_range_helper])
apply assumption
apply (case_tac r,clarsimp+)
apply (rename_tac rv s)
apply (case_tac rv; clarsimp)
apply (clarsimp simp:word_bits_conv )
apply (rule range_cover_full)
apply (simp add:word_bits_conv)+

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

@ -1228,7 +1228,7 @@ lemma getSyscallArg_ccorres_foo:
apply (simp add: index_msgRegisters_less unat_less_helper)
apply wp[1]
apply (wp getMRs_tcbContext)
apply simp
apply fastforce
apply (rule ccorres_seq_skip [THEN iffD2])
apply (rule ccorres_add_return2)
apply (rule ccorres_symb_exec_l)
@ -1252,7 +1252,7 @@ lemma getSyscallArg_ccorres_foo:
in hoare_pre(1))
apply (wp getMRs_user_word)
apply (clarsimp simp: msgMaxLength_def unat_less_helper)
apply simp
apply fastforce
apply (clarsimp simp: sysargs_rel_def sysargs_rel_n_def)
apply (rule conjI, clarsimp simp: unat_of_nat32 word_bits_def)
apply (drule equalityD2)

11
proof/crefine/ARM_HYP/Tcb_C.thy
View File

@ -1540,6 +1540,7 @@ lemma invokeTCB_WriteRegisters_ccorres[where S=UNIV]:
\<inter> {s. buffer_' s = option_to_ptr buffer}) []
(invokeTCB (WriteRegisters dst resume values arch))
(Call invokeTCB_WriteRegisters_'proc)"
supply empty_fail_cond[simp]
apply (rule ccorres_gen_asm)
apply (erule conjE)
apply (cinit lift: n_' dest_' resumeTarget_' buffer_'
@ -1788,6 +1789,7 @@ shows
(doE reply \<leftarrow> invokeTCB (ReadRegisters target susp n archCp);
liftE (replyOnRestart thread reply isCall) odE)
(Call invokeTCB_ReadRegisters_'proc)"
supply empty_fail_cond[simp]
apply (rule ccorres_gen_asm) using [[goals_limit=1]]
apply (cinit' lift: tcb_src_' suspendSource_' n_' call_'
simp: invokeTCB_def liftE_bindE bind_assoc)
@ -3652,11 +3654,10 @@ lemma decodeSetSchedParams_ccorres:
apply (simp only: cap_get_tag_isCap[symmetric], drule(1) cap_get_tag_to_H)
apply (clarsimp simp: valid_cap'_def capAligned_def interpret_excaps_eq excaps_map_def)
apply (intro conjI impI allI)
apply (clarsimp simp: unat_eq_0 le_max_word_ucast_id
thread_control_update_mcp_def thread_control_update_priority_def
cap_get_tag_isCap_unfolded_H_cap isCap_simps
interpret_excaps_eq excaps_map_def)+
done
by (clarsimp simp: unat_eq_0 le_max_word_ucast_id
thread_control_update_mcp_def thread_control_update_priority_def
cap_get_tag_isCap_unfolded_H_cap isCap_simps
interpret_excaps_eq excaps_map_def)+
lemma decodeSetIPCBuffer_ccorres:
"interpret_excaps extraCaps' = excaps_map extraCaps \<Longrightarrow>

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

@ -2022,7 +2022,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]
supply if_cong[cong] option.case_cong[cong] empty_fail_cond[simp]
apply (cinit lift: vcpu_')
apply (ctac (no_vcg) add: dsb_ccorres)
apply (rule ccorres_split_nothrow_novcg)
@ -2072,6 +2072,7 @@ lemma vcpu_enable_ccorres:
and valid_arch_state' and vcpu_at' v)
(UNIV \<inter> {s. vcpu_' s = vcpu_Ptr v}) hs
(vcpuEnable v) (Call vcpu_enable_'proc)"
supply empty_fail_cond[simp]
apply (cinit lift: vcpu_')
apply (ctac (no_vcg) add: vcpu_restore_reg_ccorres)+
apply (rule ccorres_pre_getObject_vcpu, rename_tac vcpu)
@ -2132,6 +2133,7 @@ lemma vcpu_restore_ccorres:
and vcpu_at' vcpuPtr)
(UNIV \<inter> {s. vcpu_' s = vcpu_Ptr vcpuPtr}) hs
(vcpuRestore vcpuPtr) (Call vcpu_restore_'proc)"
supply empty_fail_cond[simp]
apply (cinit lift: vcpu_' simp: whileAnno_def)
apply (simp add: doMachineOp_bind uncurry_def split_def doMachineOp_mapM_x)+
apply (clarsimp simp: bind_assoc)
@ -2724,7 +2726,7 @@ lemma doFlush_ccorres:
apply (rule ccorres_cond_true)
apply (simp add: empty_fail_cleanCacheRange_PoU empty_fail_dsb
empty_fail_invalidateCacheRange_I empty_fail_branchFlushRange empty_fail_isb
doMachineOp_bind)
doMachineOp_bind empty_fail_cond)
apply (rule ccorres_rhs_assoc)+
apply (fold dc_def)
apply (ctac (no_vcg) add: cleanCacheRange_PoU_ccorres)

15
proof/crefine/Move_C.thy
View File

@ -670,6 +670,7 @@ lemma empty_fail_asUser[iff]:
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"
supply empty_fail_cond[simp]
apply (simp add: mapM_x_mapM asUser_bind_distrib)
apply (subst submonad_mapM [OF submonad_asUser submonad_asUser])
apply simp
@ -785,7 +786,7 @@ lemma empty_fail_rethrowFailure:
lemma empty_fail_resolveAddressBits:
"empty_fail (resolveAddressBits cap cptr bits)"
proof -
note empty_fail_assertE[iff]
note empty_fail_cond[simp]
show ?thesis
apply (rule empty_fail_use_cutMon)
apply (induct rule: resolveAddressBits.induct)
@ -793,8 +794,7 @@ proof -
apply (unfold Let_def cnode_cap_case_if fun_app_def
K_bind_def haskell_assertE_def split_def)
apply (intro empty_fail_cutMon_intros)
apply (clarsimp simp: empty_fail_drop_cutMon empty_fail_whenEs
locateSlot_conv returnOk_liftE[symmetric]
apply (clarsimp simp: empty_fail_drop_cutMon locateSlot_conv returnOk_liftE[symmetric]
isCap_simps)+
done
qed
@ -828,8 +828,9 @@ lemma getMessageInfo_le3:
apply wp
apply (rule_tac Q="\<lambda>_. \<top>" in hoare_strengthen_post)
apply wp
apply (rename_tac rv s)
apply (simp add: messageInfoFromWord_def Let_def msgExtraCapBits_def)
apply (cut_tac y="r >> Types_H.msgLengthBits" in word_and_le1 [where a=3])
apply (cut_tac y="rv >> Types_H.msgLengthBits" in word_and_le1 [where a=3])
apply (simp add: word_le_nat_alt)
done
@ -998,8 +999,7 @@ lemma empty_fail_slotCapLongRunningDelete:
"empty_fail (slotCapLongRunningDelete slot)"
by (auto simp: slotCapLongRunningDelete_def Let_def
case_Null_If isFinalCapability_def
split: if_split
intro!: empty_fail_bind)
split: if_split)
lemmas mapM_x_append = mapM_x_append2
@ -1020,9 +1020,6 @@ lemma getSlotCap_wp':
apply (clarsimp simp: cte_wp_at_ctes_of)
done
lemma fromIntegral_simp_nat[simp]: "(fromIntegral :: nat \<Rightarrow> nat) = id"
by (simp add: fromIntegral_def fromInteger_nat toInteger_nat)
lemma invs_cicd_valid_objs' [elim!]:
"all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> valid_objs' s"
by (simp add: all_invs_but_ct_idle_or_in_cur_domain'_def valid_pspace'_def)

30
proof/crefine/RISCV64/ArchMove_C.thy
View File

@ -93,7 +93,7 @@ lemma atg_sp':
(* FIXME: MOVE to EmptyFail *)
lemma empty_fail_archThreadGet [intro!, wp, simp]:
"empty_fail (archThreadGet f p)"
by (simp add: archThreadGet_def getObject_def split_def)
by (fastforce simp: archThreadGet_def getObject_def split_def)
(* FIXME: move to ainvs? *)
lemma sign_extend_canonical_address:
@ -377,7 +377,7 @@ lemma length_msgRegisters[simplified size_msgRegisters_def]:
lemma empty_fail_loadWordUser[intro!, simp]:
"empty_fail (loadWordUser x)"
by (simp add: loadWordUser_def ef_loadWord ef_dmo')
by (fastforce simp: loadWordUser_def ef_loadWord ef_dmo')
lemma empty_fail_getMRs[iff]:
"empty_fail (getMRs t buf mi)"
@ -387,26 +387,14 @@ lemma empty_fail_getReceiveSlots:
"empty_fail (getReceiveSlots r rbuf)"
proof -
note
empty_fail_assertE[iff]
empty_fail_resolveAddressBits[iff]
empty_fail_resolveAddressBits[wp]
empty_fail_rethrowFailure[wp]
empty_fail_rethrowFailure[wp]
show ?thesis
apply (clarsimp simp: getReceiveSlots_def loadCapTransfer_def split_def
split: option.split)
apply (rule empty_fail_bind)
apply (simp add: capTransferFromWords_def)
apply (simp add: emptyOnFailure_def unifyFailure_def)
apply (intro empty_fail_catch empty_fail_bindE empty_fail_rethrowFailure,
simp_all add: empty_fail_whenEs)
apply (simp_all add: lookupCap_def split_def lookupCapAndSlot_def
lookupSlotForThread_def liftME_def
getThreadCSpaceRoot_def locateSlot_conv bindE_assoc
lookupSlotForCNodeOp_def lookupErrorOnFailure_def
cong: if_cong)
apply (intro empty_fail_bindE,
simp_all add: getSlotCap_def)
apply (intro empty_fail_If empty_fail_bindE empty_fail_rethrowFailure impI,
simp_all add: empty_fail_whenEs rangeCheck_def)
done
unfolding getReceiveSlots_def loadCapTransfer_def lookupCap_def lookupCapAndSlot_def
by (wpsimp simp: emptyOnFailure_def unifyFailure_def lookupSlotForThread_def
capTransferFromWords_def getThreadCSpaceRoot_def locateSlot_conv bindE_assoc
lookupSlotForCNodeOp_def lookupErrorOnFailure_def rangeCheck_def)
qed
lemma user_getreg_rv:

6
proof/crefine/RISCV64/CLevityCatch.thy
View File

@ -65,12 +65,12 @@ 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)
apply (cases sendBuffer; fastforce)
done
lemma empty_fail_loadCapTransfer [intro!, simp]:
"empty_fail (loadCapTransfer a)"
by (simp add: loadCapTransfer_def capTransferFromWords_def)
by (fastforce simp: loadCapTransfer_def capTransferFromWords_def)
lemma empty_fail_emptyOnFailure [intro!, simp]:
"empty_fail m \<Longrightarrow> empty_fail (emptyOnFailure m)"
@ -90,7 +90,7 @@ lemma asUser_get_registers:
apply (simp add: mapM_empty asUser_return)
apply wp
apply simp
apply (simp add: mapM_Cons asUser_bind_distrib asUser_return)
apply (simp add: mapM_Cons asUser_bind_distrib asUser_return empty_fail_cond)
apply wp
apply simp
apply (rule hoare_strengthen_post)

2
proof/crefine/RISCV64/Finalise_C.thy
View File

@ -1185,7 +1185,7 @@ lemma setObject_ccorres_lemma:
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 (simp add: setObject_def split_def empty_fail_cond)
apply (rule ccontr)
apply (clarsimp elim!: nonemptyE)
apply (frule use_valid [OF _ obj_at_setObject3[where P=\<top>]], simp_all)[1]

7
proof/crefine/RISCV64/IpcCancel_C.thy
View File

@ -2353,6 +2353,7 @@ lemma scheduleTCB_ccorres':
rescheduleRequired
od)
(Call scheduleTCB_'proc)"
supply empty_fail_cond[simp]
apply (cinit' lift: tptr_')
apply (rule ccorres_rhs_assoc2)+
apply (rule_tac xf'="ret__int_'" in ccorres_split_nothrow_novcg)
@ -2407,7 +2408,8 @@ lemma scheduleTCB_ccorres_valid_queues'_pre:
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) rescheduleRequired
od)
(Call scheduleTCB_'proc)"
apply (cinit' lift: tptr_' simp del: word_neq_0_conv)
supply empty_fail_cond[simp]
apply (cinit' lift: tptr_')
apply (rule ccorres_rhs_assoc2)+
apply (rule_tac xf'="ret__int_'" in ccorres_split_nothrow_novcg)
defer
@ -2428,7 +2430,7 @@ lemma scheduleTCB_ccorres_valid_queues'_pre:
\<and> weak_sch_act_wf (ksSchedulerAction s) s"
and P'=UNIV in ccorres_from_vcg)
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: return_def if_1_0_0 split del: if_split)
apply (clarsimp simp: return_def)
apply (clarsimp simp: from_bool_0 rf_sr_ksCurThread)
apply (rule conjI)
apply (clarsimp simp: st_tcb_at'_def)
@ -2499,6 +2501,7 @@ lemma scheduleTCB_ccorres_valid_queues'_pre_simple:
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) rescheduleRequired
od)
(Call scheduleTCB_'proc)"
supply empty_fail_cond[simp]
apply (cinit' lift: tptr_' simp del: word_neq_0_conv)
apply (rule ccorres_rhs_assoc2)+
apply (rule_tac xf'="ret__int_'" in ccorres_split_nothrow_novcg)

11
proof/crefine/RISCV64/Ipc_C.thy
View File

@ -405,6 +405,7 @@ lemma handleArchFaultReply':
msg \<leftarrow> getMRs s sb tag;
handleArchFaultReply f r (msgLabel tag) msg
od) x' = handleArchFaultReply' f s r tag x'"
supply empty_fail_cond[simp]
apply (unfold handleArchFaultReply'_def getMRs_def msgMaxLength_def
bit_def msgLengthBits_def msgRegisters_unfold
fromIntegral_simp1 fromIntegral_simp2
@ -549,6 +550,7 @@ lemma handleFaultReply':
msg \<leftarrow> getMRs s sb tag;
handleFaultReply f r (msgLabel tag) msg
od) (handleFaultReply' f s r)"
supply empty_fail_cond[simp]
apply (unfold handleFaultReply'_def getMRs_def msgMaxLength_def
bit_def msgLengthBits_def msgRegisters_unfold
fromIntegral_simp1 fromIntegral_simp2
@ -1771,12 +1773,12 @@ proof -
let ?obj_at_ft = "obj_at' (\<lambda>tcb. tcbFault tcb = Some ft) sender"
note symb_exec_r_fault = ccorres_symb_exec_r_known_rv_UNIV
[where xf'=ret__unsigned_longlong_' and R="?obj_at_ft" and R'=UNIV]
note empty_fail_cond[simp]
show ?thesis
apply (unfold K_def)
apply (intro ccorres_gen_asm)
apply (cinit' lift: sender_' receiver_' receiveIPCBuffer_' simp: whileAnno_def)
apply (simp add: makeFaultMessage_def setMRs_to_setMR
del: Collect_const split del: if_split)
apply (simp add: makeFaultMessage_def setMRs_to_setMR)
apply (rule_tac val="fault_to_fault_tag ft" in symb_exec_r_fault)
apply (vcg, clarsimp)
apply (drule(1) obj_at_cslift_tcb)
@ -1789,8 +1791,7 @@ proof -
apply wpc
apply (simp add: bind_assoc seL4_Fault_tag_defs ccorres_cond_iffs
Collect_True Collect_False
zipWithM_mapM zip_append2 mapM_append
del: Collect_const split del: if_split)
zipWithM_mapM zip_append2 mapM_append)
apply (rule ccorres_symb_exec_l)
apply (rule ccorres_stateAssert)
apply (rule_tac P="length msg = unat n_exceptionMessage"
@ -3144,6 +3145,7 @@ proof -
let ?curr = "\<lambda>s. current_extra_caps_' (globals s)"
let ?EXCNONE = "{s. ret__unsigned_long_' s = scast EXCEPTION_NONE}"
let ?interpret = "\<lambda>v n. take n (array_to_list (excaprefs_C v))"
note empty_fail_cond[simp]
show ?thesis
apply (rule ccorres_gen_asm)+
apply (cinit(no_subst_asm) lift: thread_' bufferPtr_' info_' simp: whileAnno_def)
@ -3697,6 +3699,7 @@ lemma copyMRsFaultReply_ccorres_syscall:
let ?obj_at_ft = "obj_at' (\<lambda>tcb. tcbFault tcb = Some f) s"
note symb_exec_r_fault = ccorres_symb_exec_r_known_rv_UNIV
[where xf'=ret__unsigned_' and R="?obj_at_ft" and R'=UNIV]
note empty_fail_cond[simp]
show ?thesis
apply (unfold K_def, rule ccorres_gen_asm) using [[goals_limit=1]]
apply (cinit' lift: sender_' receiver_'

4
proof/crefine/RISCV64/IsolatedThreadAction.thy
View File

@ -400,7 +400,7 @@ lemma getObject_get_assert:
apply (simp add: lookupAround2_known1 assert_opt_def
obj_at'_def projectKO_def2
split: option.split)
apply (clarsimp simp: fail_def fst_return conj_comms project_inject
apply (clarsimp simp: fail_set fst_return conj_comms project_inject
objBits_def)
apply (simp only: assert2[symmetric],
rule bind_apply_cong[OF refl])
@ -816,7 +816,7 @@ lemma rescheduleRequired_simple_rewrite:
(* FIXME move *)
lemma empty_fail_isRunnable[intro!, wp, simp]:
"empty_fail (isRunnable t)"
by (simp add: isRunnable_def isStopped_def)
by (simp add: isRunnable_def isStopped_def empty_fail_cond)
lemma setupCallerCap_rewrite:
"monadic_rewrite True True (\<lambda>s. reply_masters_rvk_fb (ctes_of s))

13
proof/crefine/RISCV64/Retype_C.thy
View File

@ -2275,8 +2275,8 @@ lemma getCTE_pre_cte_at:
lemmas ccorres_getCTE_cte_at = ccorres_guard_from_wp [OF getCTE_pre_cte_at empty_fail_getCTE]
ccorres_guard_from_wp_bind [OF getCTE_pre_cte_at empty_fail_getCTE]
lemmas ccorres_guard_from_wp_liftM = ccorres_guard_from_wp [OF liftM_pre iffD2 [OF empty_fail_liftM]]
lemmas ccorres_guard_from_wp_bind_liftM = ccorres_guard_from_wp_bind [OF liftM_pre iffD2 [OF empty_fail_liftM]]
lemmas ccorres_guard_from_wp_liftM = ccorres_guard_from_wp [OF liftM_pre empty_fail_liftM]
lemmas ccorres_guard_from_wp_bind_liftM = ccorres_guard_from_wp_bind [OF liftM_pre empty_fail_liftM]
lemmas ccorres_liftM_getCTE_cte_at = ccorres_guard_from_wp_liftM [OF getCTE_pre_cte_at empty_fail_getCTE]
ccorres_guard_from_wp_bind_liftM [OF getCTE_pre_cte_at empty_fail_getCTE]
@ -6439,7 +6439,8 @@ lemma createObject_caps_overlap_reserved_ret':
apply clarsimp
apply (rule hoare_strengthen_post[OF createNewCaps_caps_overlap_reserved_ret'[where sz = "APIType_capBits ty us"]])
apply assumption
apply (case_tac r,simp)
apply (rename_tac rv s)
apply (case_tac rv,simp)
apply clarsimp
apply (erule caps_overlap_reserved'_subseteq)
apply (rule untypedRange_in_capRange)
@ -6512,7 +6513,8 @@ lemma createObject_IRQHandler:
apply clarsimp
apply (rule hoare_strengthen_post[OF createNewCaps_IRQHandler[where irq = x and P = "\<lambda>_ _. False"]])
apply assumption
apply (case_tac r,clarsimp+)
apply (rename_tac rv s)
apply (case_tac rv; clarsimp)
apply (clarsimp simp:word_bits_conv)
done
@ -6529,7 +6531,8 @@ lemma createObject_capClass[wp]:
apply clarsimp
apply (rule hoare_strengthen_post[OF createNewCaps_range_helper])
apply assumption
apply (case_tac r,clarsimp+)
apply (rename_tac rv s)
apply (case_tac rv; clarsimp)
apply (clarsimp simp:word_bits_conv )
apply (rule range_cover_full)
apply (simp add:word_bits_conv)+

4
proof/crefine/RISCV64/SyscallArgs_C.thy
View File

@ -1135,7 +1135,7 @@ lemma getSyscallArg_ccorres_foo:
apply (clarsimp simp: index_msgRegisters_less' ucast_up_less_bounded_iff_less_ucast_down')
apply wp[1]
apply (wp getMRs_tcbContext)
apply simp
apply fastforce
apply (rule ccorres_seq_skip [THEN iffD2])
apply (rule ccorres_add_return2)
apply (rule ccorres_symb_exec_l)
@ -1159,7 +1159,7 @@ lemma getSyscallArg_ccorres_foo:
in hoare_pre(1))
apply (wp getMRs_user_word)
apply (clarsimp simp: msgMaxLength_def unat_less_helper)
apply simp
apply fastforce
apply (clarsimp simp: sysargs_rel_def sysargs_rel_n_def)
apply (rule conjI, clarsimp simp: unat_of_nat64 word_bits_def)
apply (drule equalityD2)

11
proof/crefine/RISCV64/Tcb_C.thy
View File

@ -1563,6 +1563,7 @@ lemma invokeTCB_WriteRegisters_ccorres[where S=UNIV]:
\<inter> {s. buffer_' s = option_to_ptr buffer}) []
(invokeTCB (WriteRegisters dst resume values arch))
(Call invokeTCB_WriteRegisters_'proc)"
supply empty_fail_cond[simp]
apply (rule ccorres_gen_asm)
apply (erule conjE)
apply (cinit lift: n_' dest___ptr_to_struct_tcb_C_' resumeTarget_' buffer_'
@ -1811,6 +1812,7 @@ shows
(doE reply \<leftarrow> invokeTCB (ReadRegisters target susp n archCp);
liftE (replyOnRestart thread reply isCall) odE)
(Call invokeTCB_ReadRegisters_'proc)"
supply empty_fail_cond[simp]
apply (rule ccorres_gen_asm)
apply (cinit' lift: tcb_src_' suspendSource_' n_' call_'
simp: invokeTCB_def liftE_bindE bind_assoc)
@ -3642,11 +3644,10 @@ lemma decodeSetSchedParams_ccorres:
apply (simp only: cap_get_tag_isCap[symmetric], drule(1) cap_get_tag_to_H)
apply (clarsimp simp: valid_cap'_def capAligned_def interpret_excaps_eq excaps_map_def)
apply (intro conjI impI allI)
apply (clarsimp simp: unat_eq_0 le_max_word_ucast_id
thread_control_update_mcp_def thread_control_update_priority_def
cap_get_tag_isCap_unfolded_H_cap isCap_simps
interpret_excaps_eq excaps_map_def)+
done
by (clarsimp simp: unat_eq_0 le_max_word_ucast_id
thread_control_update_mcp_def thread_control_update_priority_def
cap_get_tag_isCap_unfolded_H_cap isCap_simps
interpret_excaps_eq excaps_map_def)+
lemma decodeSetIPCBuffer_ccorres:
"interpret_excaps extraCaps' = excaps_map extraCaps \<Longrightarrow>

51
proof/crefine/X64/ArchMove_C.thy
View File

@ -16,7 +16,7 @@ lemma ps_clear_is_aligned_ksPSpace_None:
\<Longrightarrow> ksPSpace s (p + d) = None"
apply (simp add: ps_clear_def add_diff_eq[symmetric] mask_2pm1[symmetric])
apply (drule equals0D[where a="p + d"])
apply (simp add: dom_def word_gt_0 del: word_neq_0_conv)
apply (simp add: dom_def word_gt_0)
apply (drule mp)
apply (rule word_plus_mono_right)
apply simp
@ -47,8 +47,6 @@ where
"port_mask start end =
mask (unat (end && mask wordRadix)) && ~~ mask (unat (start && mask wordRadix))"
declare word_neq_0_conv [simp del]
lemma unat_ucast_prio_L1_cmask_simp:
"unat (ucast (p::priority) && 0x3F :: machine_word) = unat (p && 0x3F)"
using unat_ucast_prio_mask_simp[where m=6]
@ -183,13 +181,8 @@ lemma vmsz_aligned_aligned_pageBits:
lemma empty_fail_findVSpaceForASID[iff]:
"empty_fail (findVSpaceForASID asid)"
apply (simp add: findVSpaceForASID_def liftME_def)
apply (intro empty_fail_bindE, simp_all split: option.split)
apply (simp add: assertE_def split: if_split)
apply (simp add: assertE_def split: if_split)
apply (simp add: empty_fail_getObject)
apply (simp add: assertE_def liftE_bindE checkPML4At_def split: if_split)
done
unfolding findVSpaceForASID_def checkPML4At_def
by (wpsimp wp: empty_fail_getObject)
crunch inv'[wp]: archThreadGet P
@ -209,7 +202,7 @@ lemma atg_sp':
(* FIXME: MOVE to EmptyFail *)
lemma empty_fail_archThreadGet [intro!, wp, simp]:
"empty_fail (archThreadGet f p)"
by (simp add: archThreadGet_def getObject_def split_def)
by (fastforce simp: archThreadGet_def getObject_def split_def)
lemma more_pageBits_inner_beauty:
fixes x :: "9 word"
@ -354,7 +347,7 @@ lemma asUser_get_registers:
apply (simp add: mapM_empty asUser_return)
apply wp
apply simp
apply (simp add: mapM_Cons asUser_bind_distrib asUser_return)
apply (simp add: mapM_Cons asUser_bind_distrib asUser_return empty_fail_cond)
apply wp
apply simp
apply (rule hoare_strengthen_post)
@ -374,7 +367,7 @@ lemma asUser_get_registers:
(* FIXME: move to where is_aligned_ptrFromPAddr is *)
lemma is_aligned_ptrFromPAddr_pageBitsForSize:
"is_aligned p (pageBitsForSize sz) \<Longrightarrow> is_aligned (ptrFromPAddr p) (pageBitsForSize sz)"
by (cases sz ; simp add: is_aligned_ptrFromPAddr_n pageBits_def bit_simps)
by (cases sz ; simp add: is_aligned_ptrFromPAddr_n bit_simps)
lemma is_aligned_pageBitsForSize_minimum:
"\<lbrakk> is_aligned p (pageBitsForSize sz) ; n \<le> pageBits \<rbrakk> \<Longrightarrow> is_aligned p n"
@ -405,10 +398,6 @@ lemma valid_eq_wf_asid_pool'[simp]:
declare valid_asid_pool'.simps[simp del]
(*<<<*)
(* FIXME: change the original to be predicated! *)
crunch ko_at'2[wp]: doMachineOp "\<lambda>s. P (ko_at' p t s)"
(simp: crunch_simps)
(* FIXME: change the original to be predicated! *)
crunch pred_tcb_at'2[wp]: doMachineOp "\<lambda>s. P (pred_tcb_at' a b p s)"
(simp: crunch_simps)
@ -473,7 +462,7 @@ lemma length_msgRegisters[simplified size_msgRegisters_def]:
lemma empty_fail_loadWordUser[intro!, simp]:
"empty_fail (loadWordUser x)"
by (simp add: loadWordUser_def ef_loadWord ef_dmo')
by (fastforce simp: loadWordUser_def ef_loadWord ef_dmo')
lemma empty_fail_getMRs[iff]:
"empty_fail (getMRs t buf mi)"
@ -483,26 +472,14 @@ lemma empty_fail_getReceiveSlots:
"empty_fail (getReceiveSlots r rbuf)"
proof -
note
empty_fail_assertE[iff]
empty_fail_resolveAddressBits[iff]
empty_fail_resolveAddressBits[wp]
empty_fail_rethrowFailure[wp]
empty_fail_rethrowFailure[wp]
show ?thesis
apply (clarsimp simp: getReceiveSlots_def loadCapTransfer_def split_def
split: option.split)
apply (rule empty_fail_bind)
apply (simp add: capTransferFromWords_def)
apply (simp add: emptyOnFailure_def unifyFailure_def)
apply (intro empty_fail_catch empty_fail_bindE empty_fail_rethrowFailure,
simp_all add: empty_fail_whenEs)
apply (simp_all add: lookupCap_def split_def lookupCapAndSlot_def
lookupSlotForThread_def liftME_def
getThreadCSpaceRoot_def locateSlot_conv bindE_assoc
lookupSlotForCNodeOp_def lookupErrorOnFailure_def
cong: if_cong)
apply (intro empty_fail_bindE,
simp_all add: getSlotCap_def)
apply (intro empty_fail_If empty_fail_bindE empty_fail_rethrowFailure impI,
simp_all add: empty_fail_whenEs rangeCheck_def)
done
unfolding getReceiveSlots_def loadCapTransfer_def lookupCap_def lookupCapAndSlot_def
by (wpsimp simp: emptyOnFailure_def unifyFailure_def lookupSlotForThread_def
capTransferFromWords_def getThreadCSpaceRoot_def locateSlot_conv bindE_assoc
lookupSlotForCNodeOp_def lookupErrorOnFailure_def rangeCheck_def)
qed
lemma user_getreg_rv:

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

@ -55,12 +55,12 @@ 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)
apply (cases sendBuffer; fastforce)
done
lemma empty_fail_loadCapTransfer [intro!, simp]:
"empty_fail (loadCapTransfer a)"
by (simp add: loadCapTransfer_def capTransferFromWords_def)
by (fastforce simp: loadCapTransfer_def capTransferFromWords_def)
lemma empty_fail_emptyOnFailure [intro!, simp]:
"empty_fail m \<Longrightarrow> empty_fail (emptyOnFailure m)"

2
proof/crefine/X64/Finalise_C.thy
View File

@ -1319,7 +1319,7 @@ lemma setObject_ccorres_lemma:
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 (simp add: setObject_def split_def empty_fail_cond)
apply (rule ccontr)
apply (clarsimp elim!: nonemptyE)
apply (frule use_valid [OF _ obj_at_setObject3[where P=\<top>]], simp_all)[1]

9
proof/crefine/X64/IpcCancel_C.thy
View File

@ -2407,7 +2407,8 @@ lemma scheduleTCB_ccorres':
rescheduleRequired
od)
(Call scheduleTCB_'proc)"
apply (cinit' lift: tptr_' simp del: word_neq_0_conv)
supply empty_fail_cond[simp]
apply (cinit' lift: tptr_')
apply (rule ccorres_rhs_assoc2)+
apply (rule_tac xf'="ret__int_'" in ccorres_split_nothrow_novcg)
defer
@ -2428,7 +2429,7 @@ lemma scheduleTCB_ccorres':
\<and> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t s)"
and P'=UNIV in ccorres_from_vcg)
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: return_def if_1_0_0 split del: if_split)
apply (clarsimp simp: return_def)
apply (clarsimp simp: from_bool_0 rf_sr_ksCurThread)
apply (rule conjI)
apply (clarsimp simp: st_tcb_at'_def)
@ -2461,7 +2462,8 @@ lemma scheduleTCB_ccorres_valid_queues'_pre:
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) rescheduleRequired
od)
(Call scheduleTCB_'proc)"
apply (cinit' lift: tptr_' simp del: word_neq_0_conv)
supply empty_fail_cond[simp]
apply (cinit' lift: tptr_')
apply (rule ccorres_rhs_assoc2)+
apply (rule_tac xf'="ret__int_'" in ccorres_split_nothrow_novcg)
defer
@ -2553,6 +2555,7 @@ lemma scheduleTCB_ccorres_valid_queues'_pre_simple:
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) rescheduleRequired
od)
(Call scheduleTCB_'proc)"
supply empty_fail_cond[simp]
apply (cinit' lift: tptr_' simp del: word_neq_0_conv)
apply (rule ccorres_rhs_assoc2)+
apply (rule_tac xf'="ret__int_'" in ccorres_split_nothrow_novcg)

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

@ -408,6 +408,7 @@ lemma handleArchFaultReply':
msg \<leftarrow> getMRs s sb tag;
handleArchFaultReply f r (msgLabel tag) msg
od) x' = handleArchFaultReply' f s r tag x'"
supply empty_fail_cond[simp]
apply (unfold handleArchFaultReply'_def getMRs_def msgMaxLength_def
bit_def msgLengthBits_def msgRegisters_unfold
fromIntegral_simp1 fromIntegral_simp2
@ -552,7 +553,7 @@ lemma handleFaultReply':
msg \<leftarrow> getMRs s sb tag;
handleFaultReply f r (msgLabel tag) msg
od) (handleFaultReply' f s r)"
supply if_cong[cong]
supply if_cong[cong] empty_fail_cond[simp]
supply empty_fail_asUser[wp] empty_fail_getRegister[wp]
apply (unfold handleFaultReply'_def getMRs_def msgMaxLength_def
bit_def msgLengthBits_def msgRegisters_unfold
@ -1780,6 +1781,7 @@ proof -
let ?obj_at_ft = "obj_at' (\<lambda>tcb. tcbFault tcb = Some ft) sender"
note symb_exec_r_fault = ccorres_symb_exec_r_known_rv_UNIV
[where xf'=ret__unsigned_longlong_' and R="?obj_at_ft" and R'=UNIV]
note empty_fail_cond[simp]
show ?thesis
apply (unfold K_def)
apply (intro ccorres_gen_asm)
@ -3153,6 +3155,7 @@ proof -
let ?curr = "\<lambda>s. current_extra_caps_' (globals s)"
let ?EXCNONE = "{s. ret__unsigned_long_' s = scast EXCEPTION_NONE}"
let ?interpret = "\<lambda>v n. take n (array_to_list (excaprefs_C v))"
note empty_fail_cond[simp]
show ?thesis
apply (rule ccorres_gen_asm)+
apply (cinit(no_subst_asm) lift: thread_' bufferPtr_' info_' simp: whileAnno_def)
@ -3707,6 +3710,7 @@ lemma copyMRsFaultReply_ccorres_syscall:
let ?obj_at_ft = "obj_at' (\<lambda>tcb. tcbFault tcb = Some f) s"
note symb_exec_r_fault = ccorres_symb_exec_r_known_rv_UNIV
[where xf'=ret__unsigned_' and R="?obj_at_ft" and R'=UNIV]
note empty_fail_cond[simp]
show ?thesis
apply (unfold K_def, rule ccorres_gen_asm) using [[goals_limit=1]]
apply (cinit' lift: sender_' receiver_'

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

@ -401,7 +401,7 @@ lemma getObject_get_assert:
apply (simp add: lookupAround2_known1 assert_opt_def
obj_at'_def projectKO_def2
split: option.split)
apply (clarsimp simp: fail_def fst_return conj_comms project_inject
apply (clarsimp simp: fail_set fst_return conj_comms project_inject
objBits_def)
apply (simp only: assert2[symmetric],
rule bind_apply_cong[OF refl])
@ -823,7 +823,7 @@ lemma rescheduleRequired_simple_rewrite:
(* FIXME move *)
lemma empty_fail_isRunnable[intro!, wp, simp]:
"empty_fail (isRunnable t)"
by (simp add: isRunnable_def isStopped_def)
by (simp add: isRunnable_def isStopped_def empty_fail_cond)
lemma setupCallerCap_rewrite:
"monadic_rewrite True True (\<lambda>s. reply_masters_rvk_fb (ctes_of s))

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

@ -2821,8 +2821,8 @@ lemma getCTE_pre_cte_at:
lemmas ccorres_getCTE_cte_at = ccorres_guard_from_wp [OF getCTE_pre_cte_at empty_fail_getCTE]
ccorres_guard_from_wp_bind [OF getCTE_pre_cte_at empty_fail_getCTE]
lemmas ccorres_guard_from_wp_liftM = ccorres_guard_from_wp [OF liftM_pre iffD2 [OF empty_fail_liftM]]
lemmas ccorres_guard_from_wp_bind_liftM = ccorres_guard_from_wp_bind [OF liftM_pre iffD2 [OF empty_fail_liftM]]
lemmas ccorres_guard_from_wp_liftM = ccorres_guard_from_wp [OF liftM_pre empty_fail_liftM]
lemmas ccorres_guard_from_wp_bind_liftM = ccorres_guard_from_wp_bind [OF liftM_pre empty_fail_liftM]
lemmas ccorres_liftM_getCTE_cte_at = ccorres_guard_from_wp_liftM [OF getCTE_pre_cte_at empty_fail_getCTE]
ccorres_guard_from_wp_bind_liftM [OF getCTE_pre_cte_at empty_fail_getCTE]
@ -7553,7 +7553,8 @@ lemma createObject_caps_overlap_reserved_ret':
apply clarsimp
apply (rule hoare_strengthen_post[OF createNewCaps_caps_overlap_reserved_ret'[where sz = "APIType_capBits ty us"]])
apply assumption
apply (case_tac r,simp)
apply (rename_tac rv s)
apply (case_tac rv,simp)
apply clarsimp
apply (erule caps_overlap_reserved'_subseteq)
apply (rule untypedRange_in_capRange)
@ -7626,7 +7627,8 @@ lemma createObject_IRQHandler:
apply clarsimp
apply (rule hoare_strengthen_post[OF createNewCaps_IRQHandler[where irq = x and P = "\<lambda>_ _. False"]])
apply assumption
apply (case_tac r,clarsimp+)
apply (rename_tac rv s)
apply (case_tac rv; clarsimp)
apply (clarsimp simp:word_bits_conv)
done
@ -7643,7 +7645,8 @@ lemma createObject_capClass[wp]:
apply clarsimp
apply (rule hoare_strengthen_post[OF createNewCaps_range_helper])
apply assumption
apply (case_tac r,clarsimp+)
apply (rename_tac rv s)
apply (case_tac rv; clarsimp)
apply (clarsimp simp:word_bits_conv )
apply (rule range_cover_full)
apply (simp add:word_bits_conv)+

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

@ -1141,7 +1141,7 @@ lemma getSyscallArg_ccorres_foo:
apply (simp add: index_msgRegisters_less unat_less_helper)
apply wp[1]
apply (wp getMRs_tcbContext)
apply simp
apply fastforce
apply (rule ccorres_seq_skip [THEN iffD2])
apply (rule ccorres_add_return2)
apply (rule ccorres_symb_exec_l)
@ -1165,7 +1165,7 @@ lemma getSyscallArg_ccorres_foo:
in hoare_pre(1))
apply (wp getMRs_user_word)
apply (clarsimp simp: msgMaxLength_def unat_less_helper)
apply simp
apply fastforce
apply (clarsimp simp: sysargs_rel_def sysargs_rel_n_def)
apply (rule conjI, clarsimp simp: unat_of_nat64 word_bits_def)
apply (drule equalityD2)

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

@ -1557,6 +1557,7 @@ lemma invokeTCB_WriteRegisters_ccorres[where S=UNIV]:
\<inter> {s. buffer_' s = option_to_ptr buffer}) []
(invokeTCB (WriteRegisters dst resume values arch))
(Call invokeTCB_WriteRegisters_'proc)"
supply empty_fail_cond[simp]
apply (rule ccorres_gen_asm)
apply (erule conjE)
apply (cinit lift: n_' dest___ptr_to_struct_tcb_C_' resumeTarget_' buffer_'
@ -1805,6 +1806,7 @@ shows
(doE reply \<leftarrow> invokeTCB (ReadRegisters target susp n archCp);
liftE (replyOnRestart thread reply isCall) odE)
(Call invokeTCB_ReadRegisters_'proc)"
supply empty_fail_cond[simp]
apply (rule ccorres_gen_asm)
apply (cinit' lift: tcb_src_' suspendSource_' n_' call_'
simp: invokeTCB_def liftE_bindE bind_assoc)
@ -3635,11 +3637,10 @@ lemma decodeSetSchedParams_ccorres:
apply (simp only: cap_get_tag_isCap[symmetric], drule(1) cap_get_tag_to_H)
apply (clarsimp simp: valid_cap'_def capAligned_def interpret_excaps_eq excaps_map_def)
apply (intro conjI impI allI)
apply (clarsimp simp: unat_eq_0 le_max_word_ucast_id
thread_control_update_mcp_def thread_control_update_priority_def
cap_get_tag_isCap_unfolded_H_cap isCap_simps
interpret_excaps_eq excaps_map_def)+
done
by (clarsimp simp: unat_eq_0 le_max_word_ucast_id
thread_control_update_mcp_def thread_control_update_priority_def
cap_get_tag_isCap_unfolded_H_cap isCap_simps
interpret_excaps_eq excaps_map_def)+
lemma decodeSetIPCBuffer_ccorres:
"interpret_excaps extraCaps' = excaps_map extraCaps \<Longrightarrow>

9
proof/drefine/Arch_DR.thy
View File

@ -783,7 +783,8 @@ next
apply (rule corres_from_rdonly, simp_all)[1]
apply (wp+ | simp)+
apply (rule hoare_strengthen_post, rule hoare_post_taut)
apply (case_tac r, auto simp add: in_monad)[1]
apply (rename_tac rv s)
apply (case_tac rv, auto simp add: in_monad)[1]
apply (simp add: corres_whenE_throwError_split_rhs corres_alternate2
check_vp_alignment_def unlessE_whenE)
apply (clarsimp simp add: liftE_bindE[symmetric])
@ -822,7 +823,8 @@ next
apply (rule corres_from_rdonly, simp_all)[1]
apply (wp+ | simp)+
apply (rule hoare_strengthen_post, rule hoare_post_taut)
apply (case_tac r, auto simp add: in_monad)[1]
apply (rename_tac rv s)
apply (case_tac rv, auto simp add: in_monad)[1]
apply (simp add: corres_whenE_throwError_split_rhs corres_alternate2
check_vp_alignment_def unlessE_whenE)
apply (clarsimp simp add: liftE_bindE[symmetric])
@ -935,7 +937,8 @@ next
apply (rule corres_from_rdonly, simp_all)[1]
apply (wp | simp)+
apply (rule hoare_strengthen_post, rule hoare_post_taut)
apply (case_tac r, auto simp add: in_monad)[1]
apply (rename_tac rv s)
apply (case_tac rv, auto simp add: in_monad)[1]
apply (simp add: corres_whenE_throwError_split_rhs corres_alternate2
check_vp_alignment_def unlessE_whenE)
apply clarsimp

9
proof/drefine/CNode_DR.thy
View File

@ -792,9 +792,10 @@ lemma cap_revoke_corres_helper:
in corres_split_forwards')
apply (rule corres_guard_imp[OF corres_trivial[OF preemption_corres]])
apply simp+
apply (rule alternative_wp)
apply (simp add:valid_def throwError_def return_def)
apply (simp add:valid_def returnOk_def return_def)
apply (wp alternative_wp)
apply (simp add:valid_def throwError_def return_def)
apply (simp add:valid_def returnOk_def return_def)
apply fastforce
apply (clarsimp simp: valid_def)
apply clarsimp
apply (case_tac rva)
@ -1346,7 +1347,7 @@ next
show ?case
apply (clarsimp simp:mapM_Cons)
apply (subst do_machine_op_bind)
apply (clarsimp simp:ef_storeWord)+
apply (clarsimp simp:ef_storeWord empty_fail_cond)+
apply (subst corrupt_frame_duplicate[symmetric])
apply (rule corres_guard_imp)
apply (rule corres_split)

2
proof/drefine/Intent_DR.thy
View File

@ -551,7 +551,7 @@ lemma mapM_load_word_offs_do_machine_op:
"mapM (load_word_offs ptr) list
= do_machine_op (mapM loadWord (map (\<lambda>offs. ptr + of_nat (offs * word_size)) list))"
apply (subst submonad_mapM[OF submonad_do_machine_op submonad_do_machine_op])
apply (simp add: loadWord_def)
apply (simp add: loadWord_def empty_fail_cond)
apply (simp add: load_word_offs_def[abs_def] mapM_map_simp o_def)
done

3
proof/drefine/Ipc_DR.thy
View File

@ -1345,7 +1345,8 @@ next
\<and> valid_mdb s \<and> QM s cap'))" for QM
in hoare_post_imp_R)
prefer 2
apply (subgoal_tac "r\<noteq> cap.NullCap \<longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) (slot_ptr, slot_idx) s")
apply (rename_tac rv s)
apply (subgoal_tac "rv \<noteq> cap.NullCap \<longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) (slot_ptr, slot_idx) s")
apply (intro impI)
apply simp
apply (elim conjE)

7
proof/drefine/KHeap_DR.thy
View File

@ -2776,15 +2776,16 @@ lemma get_tcb_reply_cap_wp_original_cap:
apply (rule hoare_post_imp
[where Q="\<lambda>r. cte_wp_at (\<lambda>c. r \<noteq> cap.NullCap) (sid,tcb_cnode_index 2) and valid_mdb
and tcb_at sid and valid_objs and cte_wp_at ((=) r) (sid,tcb_cnode_index 2)"])
apply (rename_tac rv s)
apply clarsimp
apply (subgoal_tac "is_master_reply_cap r \<and> obj_ref_of r = sid")
apply (subgoal_tac "is_master_reply_cap rv \<and> obj_ref_of rv = sid")
apply clarsimp
apply (frule cte_wp_tcb_cap_valid)
apply simp+
apply (clarsimp simp:valid_mdb_def reply_master_revocable_def)
apply (drule_tac x = "obj_ref_of r" in spec)
apply (drule_tac x = "obj_ref_of rv" in spec)
apply (drule_tac x = "tcb_cnode_index 2" in spec)
apply (drule_tac x = r in spec)
apply (drule_tac x = rv in spec)
apply (drule iffD1[OF cte_wp_at_caps_of_state])+
apply clarsimp
apply (frule cte_wp_tcb_cap_valid)

9
proof/drefine/Untyped_DR.thy
View File

@ -65,12 +65,16 @@ next
apply (rule someI2_ex, fastforce+)+
done
(* FIXME: For some reason In_Monad.in_fail doesn't fire below. This version would probably
have been better in the first place. *)
have [simp]: "\<And>s. fst (fail s) = {}" by (simp add: fail_def)
have loadWord_const:
"\<And>a s. \<forall>x\<in>fst (loadWord a s). snd x = s"
apply (case_tac "is_aligned a 2")
apply (simp add: loadWord_def is_aligned_mask exec_gets)
apply (simp add: return_def)
apply (simp add: loadWord_def exec_gets fail_def is_aligned_mask)
apply (simp add: loadWord_def exec_gets is_aligned_mask)
done
have loadWord_atMostOneResult:
@ -78,7 +82,7 @@ next
apply (case_tac "is_aligned a 2")
apply (simp add: loadWord_def is_aligned_mask exec_gets)
apply (simp add: return_def)
apply (simp add: loadWord_def exec_gets fail_def is_aligned_mask)
apply (simp add: loadWord_def exec_gets is_aligned_mask)
done
have mapM_loadWord_atMostOneResult[rule_format]:
@ -648,6 +652,7 @@ lemma clearMemory_unused_corres_noop:
(return ())
(do_machine_op (clearMemory p (2 ^ (obj_bits_api ty us))))"
(is "\<lbrakk> ?def; ?szv; ?in \<rbrakk> \<Longrightarrow> dcorres dc \<top> ?P ?f ?g")
supply empty_fail_cond[simp]
apply (drule page_objects_default_object[where us=us and dev = dev], clarsimp)
apply (rename_tac pgsz)
apply (simp add: clearMemory_def do_machine_op_bind cleanCacheRange_PoC_def

12
proof/infoflow/ARM/ArchArch_IF.thy
View File

@ -399,8 +399,9 @@ lemma find_pd_for_asid_assert_reads_respects:
apply (wpsimp wp: get_pde_rev find_pd_for_asid_reads_respects hoare_vcg_all_lift)
apply (rule_tac Q'="\<lambda>rv s. is_subject aag (lookup_pd_slot rv 0 && ~~ mask pd_bits)"
in hoare_post_imp_R)
apply (rule find_pd_for_asid_pd_slot_authorised)
apply (subgoal_tac "lookup_pd_slot r 0 = r")
apply (rule find_pd_for_asid_pd_slot_authorised)
apply (rename_tac rv s)
apply (subgoal_tac "lookup_pd_slot rv 0 = rv")
apply fastforce
apply (simp add: lookup_pd_slot_def)
apply fastforce
@ -410,7 +411,7 @@ lemma modify_arm_hwasid_table_reads_respects:
"reads_respects aag l \<top> (modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := param\<rparr>\<rparr>))"
apply (simp add: equiv_valid_def2)
apply (rule modify_ev2)
(* FIXME: slow 5s *)
(* slow 5s *)
by (auto simp: reads_equiv_def affects_equiv_def states_equiv_for_def equiv_for_def
intro: equiv_asids_triv' split: if_splits)
@ -419,7 +420,7 @@ lemma modify_arm_asid_map_reads_respects:
"reads_respects aag l \<top> (modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := param\<rparr>\<rparr>))"
apply (simp add: equiv_valid_def2)
apply (rule modify_ev2)
(* FIXME: slow 5s *)
(* slow 5s *)
by (auto simp: reads_equiv_def affects_equiv_def states_equiv_for_def equiv_for_def
intro: equiv_asids_triv' split: if_splits)
@ -427,7 +428,7 @@ lemma modify_arm_next_asid_reads_respects:
"reads_respects aag l \<top> (modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := param\<rparr>\<rparr>))"
apply (simp add: equiv_valid_def2)
apply (rule modify_ev2)
(* FIXME: slow 5s *)
(* slow 5s *)
by (auto simp: reads_equiv_def affects_equiv_def states_equiv_for_def equiv_for_def
intro: equiv_asids_triv' split: if_splits)
@ -1277,6 +1278,7 @@ lemma do_flush_globals_equiv:
apply (cases "typ")
by (wp dmo_cacheRangeOp_lift
| simp add: do_flush_def cache_machine_op_defs do_flush_defs do_machine_op_bind when_def
empty_fail_cond
| clarsimp | rule conjI)+
lemma perform_page_directory_invocation_globals_equiv:

5
proof/infoflow/ARM/ArchIRQMasks_IF.thy
View File

@ -24,9 +24,6 @@ lemma delete_objects_irq_masks[IRQMasks_IF_assms, wp]:
apply (wp dmo_wp no_irq_mapM_x no_irq | simp add: freeMemory_def no_irq_storeWord)+
done
crunch irq_masks[wp]: cleanCacheRange_PoU "\<lambda>s. P (irq_masks s)"
(ignore_del: cleanCacheRange_PoU)
crunch irq_masks[IRQMasks_IF_assms, wp]: invoke_untyped "\<lambda>s. P (irq_masks_of_state s)"
(ignore: delete_objects wp: crunch_wps dmo_wp
wp: mapME_x_inv_wp preemption_point_inv
@ -135,7 +132,7 @@ lemma invoke_tcb_irq_masks[IRQMasks_IF_assms]:
apply (rule hoare_post_impErr[OF cap_delete_irq_masks[where P=P]])
apply blast
apply blast
apply (wpsimp wp: hoare_vcg_all_lift_R hoare_vcg_const_imp_lift_R
apply (wpsimp wp: hoare_vcg_all_lift_R hoare_vcg_const_imp_lift_R hoare_vcg_all_lift hoare_drop_imps
checked_cap_insert_domain_sep_inv)+
apply (rule_tac Q="\<lambda> r s. domain_sep_inv False st s \<and> P (irq_masks_of_state s)"
and E="\<lambda>_ s. P (irq_masks_of_state s)" in hoare_post_impErr)

2
proof/infoflow/CNode_IF.thy
View File

@ -576,7 +576,7 @@ lemma preemption_point_def2:
odE"
apply (rule ext)
apply (simp add: preemption_point_def OR_choiceE_def wrap_ext_bool_det_ext_ext_def
ef_mk_ef work_units_limit_reached_def select_f_def)
ef_mk_ef work_units_limit_reached_def select_f_def empty_fail_cond)
apply (clarsimp simp: work_units_limit_reached_def gets_def liftE_def select_f_def get_def
lift_def return_def bind_def bindE_def split_def image_def
split: option.splits sum.splits)

2
proof/infoflow/Finalise_IF.thy
View File

@ -583,7 +583,7 @@ lemma tcb_sched_action_reads_respects:
apply (simp | wp)+
apply (clarsimp simp: equiv_valid_2_def gets_apply_def get_def
bind_def return_def labels_are_invisible_def)
apply wp+
apply wpsimp+
apply (force intro: domtcbs simp: get_etcb_def pas_refined_def tcb_domain_map_wellformed_aux_def)
done

3
proof/infoflow/Noninterference.thy
View File

@ -2103,8 +2103,7 @@ lemma tcb_sched_action_reads_respects_g':
apply (rule doesnt_touch_globalsI | simp | wp)+
apply (clarsimp simp: equiv_valid_2_def gets_apply_def get_def bind_def return_def
labels_are_invisible_def)
apply wp+
apply clarsimp
apply wpsimp+
apply (clarsimp simp: pas_refined_def tcb_domain_map_wellformed_aux_def)
apply (erule_tac x="(thread, tcb_domain y)" in ballE)
apply force

2
proof/infoflow/RISCV64/ArchIRQMasks_IF.thy
View File

@ -128,7 +128,7 @@ lemma invoke_tcb_irq_masks[IRQMasks_IF_assms]:
apply (rule hoare_post_impErr[OF cap_delete_irq_masks[where P=P]])
apply blast
apply blast
apply (wpsimp wp: hoare_vcg_all_lift_R hoare_vcg_const_imp_lift_R
apply (wpsimp wp: hoare_vcg_all_lift_R hoare_vcg_const_imp_lift_R hoare_vcg_all_lift hoare_drop_imps
checked_cap_insert_domain_sep_inv)+
apply (rule_tac Q="\<lambda> r s. domain_sep_inv False st s \<and> P (irq_masks_of_state s)"
and E="\<lambda>_ s. P (irq_masks_of_state s)" in hoare_post_impErr)

7
proof/infoflow/Syscall_IF.thy
View File

@ -446,14 +446,11 @@ lemma syscall_requiv_f_g:
apply assumption+
apply (rule hoare_strengthen_post)
apply assumption
apply (case_tac r)
apply simp
apply simp
apply (simp split: sum.splits)
apply (rule hoare_strengthen_post, rule hoare_pre)
apply assumption
apply simp
apply (case_tac r)
apply simp+
apply (simp split: sum.splits)
done
(*FIXME: Move to base*)

3
proof/infoflow/Tcb_IF.thy
View File

@ -501,7 +501,8 @@ lemma invoke_tcb_reads_respects_f:
| wpsimp wp: when_ev restart_reads_respects_f reschedule_required_reads_respects_f
as_user_reads_respects_f restart_silc_inv restart_pas_refined hoare_vcg_if_lift)+
apply (rule hoare_strengthen_post[where Q="\<lambda>_ s. \<forall>rv. R rv s" and R=R for R, rotated])
apply (erule_tac x=r in allE, assumption)
apply (rename_tac rv s)
apply (erule_tac x=rv in allE, assumption)
apply wpsimp+
apply (solves \<open>auto intro!: det_zipWithM
simp: det_setRegister det_getRestartPC det_setNextPC

2
proof/invariant-abstract/AARCH64/ArchDetype_AI.thy
View File

@ -83,7 +83,7 @@ next
qed
lemma empty_fail_freeMemory [Detype_AI_asms]: "empty_fail (freeMemory ptr bits)"
by (simp add: freeMemory_def mapM_x_mapM)
by (fastforce simp: freeMemory_def mapM_x_mapM)
lemma region_in_kernel_window_detype[simp]:

19
proof/invariant-abstract/AARCH64/ArchEmptyFail_AI.thy
View File

@ -34,7 +34,7 @@ context Arch begin global_naming AARCH64
crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: handle_fault
(simp: kernel_object.splits option.splits arch_cap.splits cap.splits endpoint.splits
bool.splits list.splits thread_state.splits split_def catch_def sum.splits
Let_def wp: zipWithM_x_empty_fail)
Let_def)
crunch (empty_fail) empty_fail[wp]:
decode_tcb_configure, decode_bind_notification, decode_unbind_notification,
@ -60,14 +60,13 @@ lemma arch_decode_ARMASIDControlMakePool_empty_fail:
apply (simp add: decode_asid_control_invocation_def)
apply (intro impI conjI allI)
apply (simp add: split_def)
apply wp
apply simp
apply (wp (once), simp)
apply (subst bindE_assoc[symmetric])
apply (rule empty_fail_bindE)
subgoal by (fastforce simp: empty_fail_def whenE_def throwError_def select_ext_def bindE_def
bind_def return_def returnOk_def lift_def liftE_def fail_def
gets_def get_def assert_def select_def
split: if_split_asm)
subgoal by (force simp: empty_fail_def whenE_def throwError_def select_ext_def bindE_def
bind_def return_def returnOk_def lift_def liftE_def fail_def
gets_def get_def assert_def select_def
split: if_split_asm)
apply wpsimp
apply (wpsimp simp: decode_frame_invocation_def decode_fr_inv_flush_def Let_def)
apply (wpsimp simp: decode_vspace_invocation_def decode_vs_inv_flush_def
@ -93,9 +92,9 @@ lemma arch_decode_ARMASIDPoolAssign_empty_fail:
apply (rule empty_fail_bindE, wpsimp)
apply (subst bindE_assoc[symmetric])
apply (rule empty_fail_bindE)
subgoal by (fastforce simp: empty_fail_def whenE_def throwError_def select_def bindE_def
bind_def return_def returnOk_def lift_def liftE_def select_ext_def
gets_def get_def assert_def fail_def)
subgoal by (force simp: empty_fail_def whenE_def throwError_def select_def bindE_def
bind_def return_def returnOk_def lift_def liftE_def select_ext_def
gets_def get_def assert_def fail_def)
apply wpsimp
done

3
proof/invariant-abstract/AARCH64/ArchTcb_AI.thy
View File

@ -179,7 +179,6 @@ lemma cap_delete_no_cap_to_obj_asid[wp, Tcb_AI_asms]:
apply (simp add: cap_delete_def
no_cap_to_obj_with_diff_ref_ran_caps_form)
apply wp
apply simp
apply (rule use_spec)
apply (rule rec_del_all_caps_in_range)
apply (simp | rule obj_ref_none_no_asid)+
@ -235,7 +234,7 @@ lemma tc_invs[Tcb_AI_asms]:
apply (simp add: split_def set_mcpriority_def cong: option.case_cong)
apply (rule hoare_vcg_precond_imp)
apply wp
apply ((simp only: simp_thms
apply ((simp only: simp_thms cong: conj_cong
| (simp add: conj_comms del: hoare_True_E_R,
strengthen imp_consequent[where Q="x = None" for x], simp cong: conj_cong)
| rule wp_split_const_if wp_split_const_if_R

2
proof/invariant-abstract/AARCH64/ArchVSpace_AI.thy
View File

@ -2864,7 +2864,7 @@ lemma vcpu_enable_invs[wp]:
lemma vcpu_restore_invs[wp]:
"vcpu_restore v \<lbrace>invs\<rbrace>"
apply (simp add: vcpu_restore_def do_machine_op_bind dom_mapM)
apply (simp add: vcpu_restore_def do_machine_op_bind dom_mapM empty_fail_cond)
apply (wpsimp wp: mapM_wp_inv)
done

2
proof/invariant-abstract/AARCH64/Machine_AI.thy
View File

@ -89,7 +89,7 @@ text \<open>Failure on empty result\<close>
crunches loadWord, storeWord, machine_op_lift, clearMemory
for (empty_fail) empty_fail[intro!, wp, simp]
(ignore: NonDetMonad.bind mapM_x simp: machine_op_lift_def)
(ignore: NonDetMonad.bind mapM_x simp: machine_op_lift_def empty_fail_cond)
lemmas ef_machine_op_lift = machine_op_lift_empty_fail \<comment> \<open>required for generic interface\<close>

2
proof/invariant-abstract/ARM/ArchDetype_AI.thy
View File

@ -89,7 +89,7 @@ next
qed
lemma empty_fail_freeMemory [Detype_AI_asms]: "empty_fail (freeMemory ptr bits)"
by (simp add: freeMemory_def mapM_x_mapM ef_storeWord)
by (fastforce simp: freeMemory_def mapM_x_mapM ef_storeWord)
lemma region_in_kernel_window_detype[simp]:

16
proof/invariant-abstract/ARM/ArchEmptyFail_AI.thy
View File

@ -37,7 +37,7 @@ context Arch begin global_naming ARM
crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: handle_fault
(simp: kernel_object.splits option.splits arch_cap.splits cap.splits endpoint.splits
bool.splits list.splits thread_state.splits split_def catch_def sum.splits
Let_def wp: zipWithM_x_empty_fail)
Let_def)
crunch (empty_fail) empty_fail[wp]:
decode_tcb_configure, decode_bind_notification, decode_unbind_notification,
@ -61,11 +61,13 @@ lemma arch_decode_ARMASIDControlMakePool_empty_fail:
apply (simp add: isPageFlushLabel_def isPDFlushLabel_def split: arch_cap.splits)+
apply (rule impI)
apply (simp add: split_def)
apply wp
apply simp
apply (wp (once), simp)
apply (subst bindE_assoc[symmetric])
apply (rule empty_fail_bindE)
subgoal by (fastforce simp: empty_fail_def whenE_def throwError_def select_ext_def bindE_def bind_def return_def returnOk_def lift_def liftE_def fail_def gets_def get_def assert_def select_def split: if_split_asm)
subgoal by (force simp: empty_fail_def whenE_def throwError_def select_ext_def bindE_def
bind_def return_def returnOk_def lift_def liftE_def fail_def gets_def
get_def assert_def select_def
split: if_split_asm)
by (simp add: Let_def split: cap.splits arch_cap.splits option.splits bool.splits | wp | intro conjI impI allI)+
lemma arch_decode_ARMASIDPoolAssign_empty_fail:
@ -83,9 +85,9 @@ lemma arch_decode_ARMASIDPoolAssign_empty_fail:
apply ((simp | wp)+)[1]
apply (subst bindE_assoc[symmetric])
apply (rule empty_fail_bindE)
subgoal by (fastforce simp: empty_fail_def whenE_def throwError_def select_def bindE_def
bind_def return_def returnOk_def lift_def liftE_def select_ext_def
gets_def get_def assert_def fail_def)
subgoal by (force simp: empty_fail_def whenE_def throwError_def select_def bindE_def
bind_def return_def returnOk_def lift_def liftE_def select_ext_def
gets_def get_def assert_def fail_def)
apply wp
done

6
proof/invariant-abstract/ARM/ArchTcb_AI.thy
View File

@ -187,7 +187,6 @@ lemma cap_delete_no_cap_to_obj_asid[wp, Tcb_AI_asms]:
apply (simp add: cap_delete_def
no_cap_to_obj_with_diff_ref_ran_caps_form)
apply wp
apply simp
apply (rule use_spec)
apply (rule rec_del_all_caps_in_range)
apply (simp add: table_cap_ref_def[simplified, split_simps cap.split]
@ -238,8 +237,9 @@ lemma tc_invs[Tcb_AI_asms]:
apply (simp add: split_def set_mcpriority_def cong: option.case_cong)
apply (rule hoare_vcg_precond_imp)
apply wp
(* takes long: *)
apply ((simp only: simp_thms
(* takes long: (30 sec) *)
apply ((simp only: simp_thms cong: conj_cong
| (strengthen invs_strengthen)+
| rule wp_split_const_if wp_split_const_if_R
hoare_vcg_all_lift_R
hoare_vcg_E_elim hoare_vcg_const_imp_lift_R

2
proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy
View File

@ -1074,8 +1074,6 @@ lemma perform_invocation_valid_pdpt[wp]:
\<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>"
apply (cases i, simp_all)
apply (wp send_signal_interrupt_states | simp)+
apply (clarsimp simp: invocation_duplicates_valid_def)
apply (wp | wpc | simp)+
apply (simp add: arch_perform_invocation_def)
apply (rule hoare_pre)
apply (wp | wpc | simp)+

23
proof/invariant-abstract/ARM/Machine_AI.thy
View File

@ -83,13 +83,13 @@ lemma det_getRestartPC: "det getRestartPC"
lemma det_setNextPC: "det (setNextPC p)"
by (simp add: setNextPC_def det_setRegister)
(* FIXME empty_fail: make all empty_fail [intro!, wp], and non-conditional ones [simp] *)
lemma ef_loadWord: "empty_fail (loadWord x)"
by (simp add: loadWord_def)
by (fastforce simp: loadWord_def)
lemma ef_storeWord: "empty_fail (storeWord x y)"
by (simp add: storeWord_def)
by (fastforce simp: storeWord_def)
lemma no_fail_getRestartPC: "no_fail \<top> getRestartPC"
@ -731,11 +731,12 @@ lemma empty_fail_cleanCacheRange_PoC[simp, intro!]:
lemma empty_fail_cleanInvalidateCacheRange_RAM[simp, intro!]:
"empty_fail (cleanInvalidateCacheRange_RAM s e p)"
by (simp add: cleanInvalidateCacheRange_RAM_def empty_fail_dsb empty_fail_cleanInvalidateL2Range empty_fail_cleanInvalByVA)
by (fastforce simp: cleanInvalidateCacheRange_RAM_def empty_fail_dsb
empty_fail_cleanInvalidateL2Range empty_fail_cleanInvalByVA)
lemma empty_fail_cleanCacheRange_RAM[simp, intro!]:
"empty_fail (cleanCacheRange_RAM s e p)"
by (simp add: cleanCacheRange_RAM_def empty_fail_dsb empty_fail_cleanL2Range)
by (fastforce simp: cleanCacheRange_RAM_def empty_fail_dsb empty_fail_cleanL2Range)
lemma empty_fail_invalidateCacheRange_I[simp, intro!]:
"empty_fail (invalidateCacheRange_I s e p)"
@ -743,8 +744,8 @@ lemma empty_fail_invalidateCacheRange_I[simp, intro!]:
lemma empty_fail_invalidateCacheRange_RAM[simp, intro!]:
"empty_fail (invalidateCacheRange_RAM s e p)"
by (simp add: invalidateCacheRange_RAM_def lineStart_def cacheLineBits_def
empty_fail_invalidateL2Range empty_fail_invalidateByVA empty_fail_dsb)
by (fastforce simp: invalidateCacheRange_RAM_def lineStart_def cacheLineBits_def
empty_fail_invalidateL2Range empty_fail_invalidateByVA empty_fail_dsb)
lemma empty_fail_branchFlushRange[simp, intro!]:
"empty_fail (branchFlushRange s e p)"
@ -752,16 +753,16 @@ lemma empty_fail_branchFlushRange[simp, intro!]:
lemma empty_fail_cleanCaches_PoU[simp, intro!]:
"empty_fail cleanCaches_PoU"
by (simp add: cleanCaches_PoU_def empty_fail_dsb empty_fail_clean_D_PoU empty_fail_invalidate_I_PoU)
by (fastforce simp: cleanCaches_PoU_def empty_fail_dsb empty_fail_clean_D_PoU empty_fail_invalidate_I_PoU)
lemma empty_fail_cleanInvalidateL1Caches[simp, intro!]:
"empty_fail cleanInvalidateL1Caches"
by (simp add: cleanInvalidateL1Caches_def empty_fail_dsb empty_fail_cleanInvalidate_D_PoC
empty_fail_invalidate_I_PoU)
by (fastforce simp: cleanInvalidateL1Caches_def empty_fail_dsb empty_fail_cleanInvalidate_D_PoC
empty_fail_invalidate_I_PoU)
lemma empty_fail_clearMemory [simp, intro!]:
"\<And>a b. empty_fail (clearMemory a b)"
by (simp add: clearMemory_def mapM_x_mapM ef_storeWord)
by (fastforce simp: clearMemory_def mapM_x_mapM ef_storeWord)
end

2
proof/invariant-abstract/ARM_HYP/ArchArch_AI.thy
View File

@ -1145,7 +1145,7 @@ lemma vcpu_enable_valid_machine_state[wp]:
crunches vcpu_restore, vcpu_save
for valid_machine_state[wp]: valid_machine_state
(wp: mapM_wp_inv simp: do_machine_op_bind dom_mapM ignore: do_machine_op)
(wp: mapM_wp_inv simp: do_machine_op_bind dom_mapM empty_fail_cond ignore: do_machine_op)
crunches associate_vcpu_tcb
for valid_machine_state[wp]: valid_machine_state

2
proof/invariant-abstract/ARM_HYP/ArchDetype_AI.thy
View File

@ -93,7 +93,7 @@ next
qed
lemma empty_fail_freeMemory [Detype_AI_asms]: "empty_fail (freeMemory ptr bits)"
by (simp add: freeMemory_def mapM_x_mapM ef_storeWord)
by (fastforce simp: freeMemory_def mapM_x_mapM ef_storeWord)
lemma region_in_kernel_window_detype[simp]:

17
proof/invariant-abstract/ARM_HYP/ArchEmptyFail_AI.thy
View File

@ -37,7 +37,8 @@ context Arch begin global_naming ARM_HYP
crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: handle_fault
(simp: kernel_object.splits option.splits arch_cap.splits cap.splits endpoint.splits
bool.splits list.splits thread_state.splits split_def catch_def sum.splits
Let_def wp: zipWithM_x_empty_fail empty_fail_addressTranslateS1)
Let_def
wp: empty_fail_addressTranslateS1)
crunch (empty_fail) empty_fail[wp]:
decode_tcb_configure, decode_bind_notification, decode_unbind_notification,
@ -65,11 +66,13 @@ lemma arch_decode_ARMASIDControlMakePool_empty_fail:
prefer 2
apply (simp add: isPageFlushLabel_def isPDFlushLabel_def split: arch_cap.splits)+
apply (simp add: split_def)
apply wp
apply simp
apply (wp (once), simp)
apply (subst bindE_assoc[symmetric])
apply (rule empty_fail_bindE)
subgoal by (fastforce simp: empty_fail_def whenE_def throwError_def select_ext_def bindE_def bind_def return_def returnOk_def lift_def liftE_def fail_def gets_def get_def assert_def select_def split: if_split_asm)
subgoal by (force simp: empty_fail_def whenE_def throwError_def select_ext_def bindE_def bind_def
return_def returnOk_def lift_def liftE_def fail_def gets_def get_def
assert_def select_def
split: if_split_asm)
apply (simp add: Let_def split: cap.splits arch_cap.splits option.splits bool.splits | wp | intro conjI impI allI)+
done (* needs tidying up *)
@ -89,9 +92,9 @@ lemma arch_decode_ARMASIDPoolAssign_empty_fail:
apply ((simp | wp)+)[1]
apply (subst bindE_assoc[symmetric])
apply (rule empty_fail_bindE)
subgoal by (fastforce simp: empty_fail_def whenE_def throwError_def select_def bindE_def
bind_def return_def returnOk_def lift_def liftE_def select_ext_def
gets_def get_def assert_def fail_def)
subgoal by (force simp: empty_fail_def whenE_def throwError_def select_def bindE_def
bind_def return_def returnOk_def lift_def liftE_def select_ext_def
gets_def get_def assert_def fail_def)
apply wp+
done

16
proof/invariant-abstract/ARM_HYP/ArchSchedule_AI.thy
View File

@ -27,22 +27,6 @@ lemma dmo_mapM_storeWord_0_invs[wp,Schedule_AI_asms]:
apply wp
apply (clarsimp simp: word_bits_conv)
done
(*
global_naming ARM_HYP (*FIXME: arch_split*)
lemma set_vm_root_kheap_arch_state[wp]:
"\<lbrace>\<lambda>s. P (kheap s) (arm_globals_frame (arch_state s))\<rbrace> set_vm_root a
\<lbrace>\<lambda>_ s. P (kheap s) (arm_globals_frame (arch_state s))\<rbrace>" (is "valid ?P _ _")
apply (simp add: set_vm_root_def arm_context_switch_def)
apply (wp | wpcw | simp add: arm_context_switch_def get_hw_asid_def
store_hw_asid_def find_pd_for_asid_assert_def find_free_hw_asid_def
invalidate_hw_asid_entry_def invalidate_asid_def load_hw_asid_def)+
apply (simp add: whenE_def, intro conjI impI)
apply (wp, simp add: returnOk_def validE_E_def validE_def)+
apply (simp add: whenE_def, intro conjI[rotated] impI)
apply (wp | simp add: returnOk_def validE_E_def validE_def)+
apply (wp | simp add: throwError_def validE_R_def validE_def)+
done
*)
crunch device_state_inv[wp]: clearExMonitor "\<lambda>ms. P (device_state ms)"

6
proof/invariant-abstract/ARM_HYP/ArchTcb_AI.thy
View File

@ -189,7 +189,6 @@ lemma cap_delete_no_cap_to_obj_asid[wp, Tcb_AI_asms]:
apply (simp add: cap_delete_def
no_cap_to_obj_with_diff_ref_ran_caps_form)
apply wp
apply simp
apply (rule use_spec)
apply (rule rec_del_all_caps_in_range)
apply (rule mp[OF _ obj_ref_none_no_asid(1)[of cap]], simp)
@ -240,8 +239,9 @@ lemma tc_invs[Tcb_AI_asms]:
apply (simp add: split_def set_mcpriority_def cong: option.case_cong)
apply (rule hoare_vcg_precond_imp)
apply wp
(* takes long: *)
apply ((simp only: simp_thms
(* takes long: (30 sec) *)
apply ((simp only: simp_thms cong: conj_cong
| (strengthen invs_strengthen)+
| rule wp_split_const_if wp_split_const_if_R
hoare_vcg_all_lift_R
hoare_vcg_E_elim hoare_vcg_const_imp_lift_R

2
proof/invariant-abstract/ARM_HYP/ArchVSpaceEntries_AI.thy
View File

@ -1033,8 +1033,6 @@ lemma perform_invocation_valid_pdpt[wp]:
\<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>"
apply (cases i, simp_all)
apply (wp send_signal_interrupt_states | simp)+
apply (clarsimp simp: invocation_duplicates_valid_def)
apply (wp | wpc | simp)+
apply (simp add: arch_perform_invocation_def)
apply (rule hoare_pre)
apply (wp | wpc | simp)+

4
proof/invariant-abstract/ARM_HYP/ArchVSpace_AI.thy
View File

@ -2538,7 +2538,7 @@ lemma vcpu_enable_invs[wp]:
lemma vcpu_restore_invs[wp]:
"\<lbrace>\<lambda>s. invs s\<rbrace> vcpu_restore v \<lbrace>\<lambda>_. invs\<rbrace>"
apply (simp add: vcpu_restore_def do_machine_op_bind dom_mapM)
apply (simp add: vcpu_restore_def do_machine_op_bind dom_mapM empty_fail_cond)
apply (wpsimp wp: mapM_wp_inv)
done
@ -2571,7 +2571,7 @@ lemma vcpu_save_invs[wp]:
lemma vcpu_disable_invs[wp]:
"\<lbrace>\<lambda> s. invs s\<rbrace> vcpu_disable v \<lbrace>\<lambda>_ s . invs s\<rbrace>"
apply (simp add: vcpu_disable_def)
apply (wpsimp simp: do_machine_op_bind empty_fail_isb
apply (wpsimp simp: do_machine_op_bind empty_fail_isb empty_fail_cond
wp: set_vcpu_invs_eq_hyp get_vcpu_wp maskInterrupt_invs
| wp hoare_vcg_all_lift hoare_vcg_imp_lift')+
done

27
proof/invariant-abstract/ARM_HYP/Machine_AI.thy
View File

@ -83,13 +83,13 @@ lemma det_getRestartPC: "det getRestartPC"
lemma det_setNextPC: "det (setNextPC p)"
by (simp add: setNextPC_def det_setRegister)
(* FIXME empty_fail: make all empty_fail [intro!, wp], and non-conditional ones [simp] *)
lemma ef_loadWord: "empty_fail (loadWord x)"
by (simp add: loadWord_def)
by (fastforce simp: loadWord_def)
lemma ef_storeWord: "empty_fail (storeWord x y)"
by (simp add: storeWord_def)
by (fastforce simp: storeWord_def)
lemma no_fail_getRestartPC: "no_fail \<top> getRestartPC"
@ -772,7 +772,7 @@ lemma empty_fail_setHCR[simp, intro!]:
lemma empty_fail_addressTranslateS1[simp, intro!]:
"empty_fail (addressTranslateS1 w)"
by (simp add: addressTranslateS1_def)
by (fastforce simp: addressTranslateS1_def)
lemma empty_fail_writeContextIDAndPD[simp, intro!]:
"empty_fail (writeContextIDAndPD asid w)"
@ -804,7 +804,7 @@ lemma empty_fail_set_gic_vcpu_ctrl_apr[simp, intro!]:
lemma empty_fail_get_gic_vcpu_ctrl_lr[simp, intro!]:
"empty_fail (get_gic_vcpu_ctrl_lr n)"
by (simp add: get_gic_vcpu_ctrl_lr_def)
by (fastforce simp: get_gic_vcpu_ctrl_lr_def)
lemma empty_fail_set_gic_vcpu_ctrl_lr[simp, intro!]:
"empty_fail (set_gic_vcpu_ctrl_lr n w)"
@ -846,11 +846,12 @@ lemma empty_fail_cleanCacheRange_PoC[simp, intro!]:
lemma empty_fail_cleanInvalidateCacheRange_RAM[simp, intro!]:
"empty_fail (cleanInvalidateCacheRange_RAM s e p)"
by (simp add: cleanInvalidateCacheRange_RAM_def empty_fail_dsb empty_fail_cleanInvalidateL2Range empty_fail_cleanInvalByVA)
by (fastforce simp: cleanInvalidateCacheRange_RAM_def empty_fail_dsb
empty_fail_cleanInvalidateL2Range empty_fail_cleanInvalByVA)
lemma empty_fail_cleanCacheRange_RAM[simp, intro!]:
"empty_fail (cleanCacheRange_RAM s e p)"
by (simp add: cleanCacheRange_RAM_def empty_fail_dsb empty_fail_cleanL2Range)
by (fastforce simp: cleanCacheRange_RAM_def empty_fail_dsb empty_fail_cleanL2Range)
lemma empty_fail_invalidateCacheRange_I[simp, intro!]:
"empty_fail (invalidateCacheRange_I s e p)"
@ -858,8 +859,8 @@ lemma empty_fail_invalidateCacheRange_I[simp, intro!]:
lemma empty_fail_invalidateCacheRange_RAM[simp, intro!]:
"empty_fail (invalidateCacheRange_RAM s e p)"
by (simp add: invalidateCacheRange_RAM_def lineStart_def cacheLineBits_def
empty_fail_invalidateL2Range empty_fail_invalidateByVA empty_fail_dsb)
by (fastforce simp: invalidateCacheRange_RAM_def lineStart_def cacheLineBits_def
empty_fail_invalidateL2Range empty_fail_invalidateByVA empty_fail_dsb)
lemma empty_fail_branchFlushRange[simp, intro!]:
"empty_fail (branchFlushRange s e p)"
@ -867,16 +868,16 @@ lemma empty_fail_branchFlushRange[simp, intro!]:
lemma empty_fail_cleanCaches_PoU[simp, intro!]:
"empty_fail cleanCaches_PoU"
by (simp add: cleanCaches_PoU_def empty_fail_dsb empty_fail_clean_D_PoU empty_fail_invalidate_I_PoU)
by (fastforce simp: cleanCaches_PoU_def empty_fail_dsb empty_fail_clean_D_PoU empty_fail_invalidate_I_PoU)
lemma empty_fail_cleanInvalidateL1Caches[simp, intro!]:
"empty_fail cleanInvalidateL1Caches"
by (simp add: cleanInvalidateL1Caches_def empty_fail_dsb empty_fail_cleanInvalidate_D_PoC
empty_fail_invalidate_I_PoU)
by (fastforce simp: cleanInvalidateL1Caches_def empty_fail_dsb empty_fail_cleanInvalidate_D_PoC
empty_fail_invalidate_I_PoU)
lemma empty_fail_clearMemory [simp, intro!]:
"\<And>a b. empty_fail (clearMemory a b)"
by (simp add: clearMemory_def mapM_x_mapM ef_storeWord)
by (fastforce simp: clearMemory_def mapM_x_mapM ef_storeWord)
end

3
proof/invariant-abstract/CNodeInv_AI.thy
View File

@ -448,6 +448,7 @@ lemma decode_cnode_inv_wf[wp]:
and cte_wp_at (\<lambda>c. c = src_cap) src_slot
and cte_wp_at ((=) cap.NullCap) x"
in hoare_post_imp)
apply (rename_tac rv s)
apply (clarsimp simp: cte_wp_at_caps_of_state all_rights_def)
apply (simp add: cap_master_update_cap_data weak_derived_update_cap_data
cap_asid_update_cap_data
@ -455,7 +456,7 @@ lemma decode_cnode_inv_wf[wp]:
apply (strengthen cap_badge_update_cap_data)
apply simp
apply (frule (1) caps_of_state_valid_cap)
apply (case_tac "is_zombie r")
apply (case_tac "is_zombie rv")
apply (clarsimp simp add: valid_cap_def2 update_cap_data_def
is_cap_simps
split: if_split_asm)

2
proof/invariant-abstract/EmptyFail_AI.thy
View File

@ -45,7 +45,7 @@ lemma do_machine_op_empty_fail[wp]:
"empty_fail f \<Longrightarrow> empty_fail (do_machine_op f)"
apply (simp add: do_machine_op_def | wp)+
apply (simp add: empty_fail_def)
apply (simp add: split_def)
apply (simp add: split_def empty_fail_cond)
done
lemma throw_on_false_empty_fail[wp]:

15
proof/invariant-abstract/Include_AI.thy
View File

@ -8,13 +8,14 @@ theory Include_AI
imports
Lib.Lib
ArchCrunchSetup_AI
"Monads.Eisbach_WP"
"ASpec.Syscall_A"
"Lib.LemmaBucket"
"Lib.ListLibLemmas"
"Lib.LemmaBucket"
"Lib.SplitRule"
"Rights_AI"
Monads.Eisbach_WP
Monads.Strengthen_Setup
ASpec.Syscall_A
Lib.LemmaBucket
Lib.ListLibLemmas
Lib.LemmaBucket
Lib.SplitRule
Rights_AI
begin
no_notation bind_drop (infixl ">>" 60)

2
proof/invariant-abstract/RISCV64/ArchDetype_AI.thy
View File

@ -82,7 +82,7 @@ next
qed
lemma empty_fail_freeMemory [Detype_AI_asms]: "empty_fail (freeMemory ptr bits)"
by (simp add: freeMemory_def mapM_x_mapM ef_storeWord)
by (fastforce simp: freeMemory_def mapM_x_mapM ef_storeWord)
lemma region_in_kernel_window_detype[simp]:

19
proof/invariant-abstract/RISCV64/ArchEmptyFail_AI.thy
View File

@ -32,7 +32,7 @@ context Arch begin global_naming RISCV64
crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: handle_fault
(simp: kernel_object.splits option.splits arch_cap.splits cap.splits endpoint.splits
bool.splits list.splits thread_state.splits split_def catch_def sum.splits
Let_def wp: zipWithM_x_empty_fail)
Let_def)
crunch (empty_fail) empty_fail[wp]:
decode_tcb_configure, decode_bind_notification, decode_unbind_notification,
@ -54,14 +54,13 @@ lemma arch_decode_RISCVASIDControlMakePool_empty_fail:
apply (simp add: decode_asid_control_invocation_def)
apply (intro impI conjI allI)
apply (simp add: split_def)
apply wp
apply simp
apply (wp (once), simp)
apply (subst bindE_assoc[symmetric])
apply (rule empty_fail_bindE)
subgoal by (fastforce simp: empty_fail_def whenE_def throwError_def select_ext_def bindE_def
bind_def return_def returnOk_def lift_def liftE_def fail_def
gets_def get_def assert_def select_def
split: if_split_asm)
subgoal by (force simp: empty_fail_def whenE_def throwError_def select_ext_def bindE_def
bind_def return_def returnOk_def lift_def liftE_def fail_def
gets_def get_def assert_def select_def
split: if_split_asm)
apply wpsimp
apply (wpsimp simp: decode_frame_invocation_def)
apply (wpsimp simp: decode_page_table_invocation_def)
@ -84,9 +83,9 @@ lemma arch_decode_RISCVASIDPoolAssign_empty_fail:
apply (rule empty_fail_bindE, wpsimp)
apply (subst bindE_assoc[symmetric])
apply (rule empty_fail_bindE)
subgoal by (fastforce simp: empty_fail_def whenE_def throwError_def select_def bindE_def
bind_def return_def returnOk_def lift_def liftE_def select_ext_def
gets_def get_def assert_def fail_def)
subgoal by (force simp: empty_fail_def whenE_def throwError_def select_def bindE_def
bind_def return_def returnOk_def lift_def liftE_def select_ext_def
gets_def get_def assert_def fail_def)
apply wpsimp
done

3
proof/invariant-abstract/RISCV64/ArchTcb_AI.thy
View File

@ -181,7 +181,6 @@ lemma cap_delete_no_cap_to_obj_asid[wp, Tcb_AI_asms]:
apply (simp add: cap_delete_def
no_cap_to_obj_with_diff_ref_ran_caps_form)
apply wp
apply simp
apply (rule use_spec)
apply (rule rec_del_all_caps_in_range)
apply (simp | rule obj_ref_none_no_asid)+
@ -237,7 +236,7 @@ lemma tc_invs[Tcb_AI_asms]:
apply (simp add: split_def set_mcpriority_def cong: option.case_cong)
apply (rule hoare_vcg_precond_imp)
apply wp
apply ((simp only: simp_thms
apply ((simp only: simp_thms cong: conj_cong
| (simp add: conj_comms del: hoare_True_E_R,
strengthen imp_consequent[where Q="x = None" for x], simp cong: conj_cong)
| rule wp_split_const_if wp_split_const_if_R

2
proof/invariant-abstract/RISCV64/ArchVSpaceEntries_AI.thy
View File

@ -287,8 +287,6 @@ lemma perform_invocation_valid_vspace_objs'[wp]:
\<lbrace>\<lambda>rv. valid_vspace_objs'\<rbrace>"
apply (cases i, simp_all)
apply (wp send_signal_interrupt_states | simp)+
apply (clarsimp simp:)
apply (wp | wpc | simp)+
apply (simp add: arch_perform_invocation_def)
apply (wp | wpc | simp)+
apply (auto simp: valid_arch_inv_def intro: valid_objs_caps)

8
proof/invariant-abstract/RISCV64/Machine_AI.thy
View File

@ -83,13 +83,13 @@ lemma det_getRestartPC: "det getRestartPC"
lemma det_setNextPC: "det (setNextPC p)"
by (simp add: setNextPC_def det_setRegister)
(* FIXME empty_fail: make all empty_fail [intro!, wp], and non-conditional ones [simp] *)
lemma ef_loadWord: "empty_fail (loadWord x)"
by (simp add: loadWord_def)
by (fastforce simp: loadWord_def)
lemma ef_storeWord: "empty_fail (storeWord x y)"
by (simp add: storeWord_def)
by (fastforce simp: storeWord_def)
lemma no_fail_getRestartPC: "no_fail \<top> getRestartPC"
@ -356,7 +356,7 @@ lemma empty_fail_initL2Cache: "empty_fail initL2Cache"
lemma empty_fail_clearMemory [simp, intro!]:
"\<And>a b. empty_fail (clearMemory a b)"
by (simp add: clearMemory_def mapM_x_mapM ef_storeWord)
by (fastforce simp: clearMemory_def mapM_x_mapM ef_storeWord)
lemma no_irq_setVSpaceRoot:
"no_irq (setVSpaceRoot r a)"

2
proof/invariant-abstract/SubMonad_AI.thy
View File

@ -42,7 +42,7 @@ lemma assert_get_thread_do_machine_op_comm:
apply (rule submonad_comm2 [OF _ _ submonad_do_machine_op])
apply (rule submonad_args_pspace)
apply (rule assert_get_tcb_pspace)
apply simp+
apply (simp add: empty_fail_cond)+
done
end

1
proof/invariant-abstract/VSpaceEntries_AI.thy
View File

@ -148,7 +148,6 @@ lemma mapME_x_wp:
shows "set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> mapME_x f xs \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace>"
apply (subst mapME_x_mapME)
apply wp
apply simp
apply (rule mapME_wp)
apply (rule x)
apply assumption+

2
proof/invariant-abstract/X64/ArchDetype_AI.thy
View File

@ -82,7 +82,7 @@ next
qed
lemma empty_fail_freeMemory [Detype_AI_asms]: "empty_fail (freeMemory ptr bits)"
by (simp add: freeMemory_def mapM_x_mapM ef_storeWord)
by (fastforce simp: freeMemory_def mapM_x_mapM ef_storeWord)
lemma region_in_kernel_window_detype[simp]:

21
proof/invariant-abstract/X64/ArchEmptyFail_AI.thy
View File

@ -37,7 +37,7 @@ context Arch begin global_naming X64
crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: handle_fault
(simp: kernel_object.splits option.splits arch_cap.splits cap.splits endpoint.splits
bool.splits list.splits thread_state.splits split_def catch_def sum.splits
Let_def wp: zipWithM_x_empty_fail)
Let_def)
lemma port_out_empty_fail[simp, intro!]:
assumes ef: "\<And>a. empty_fail (oper a)"
@ -80,12 +80,11 @@ lemma arch_decode_X64ASIDControlMakePool_empty_fail:
apply (simp split: arch_cap.splits)
apply (intro conjI impI)
apply (simp add: split_def)
apply wp
apply simp
apply (wp (once), simp)
apply (subst bindE_assoc[symmetric])
apply (rule empty_fail_bindE)
subgoal by (fastforce simp: empty_fail_def whenE_def throwError_def select_ext_def bindE_def bind_def return_def
returnOk_def lift_def liftE_def fail_def gets_def get_def assert_def select_def split: if_split_asm)
subgoal by (force simp: empty_fail_def whenE_def throwError_def select_ext_def bindE_def bind_def return_def
returnOk_def lift_def liftE_def fail_def gets_def get_def assert_def select_def split: if_split_asm)
apply (simp add: Let_def split: cap.splits arch_cap.splits option.splits bool.splits | wp | intro conjI impI allI)+
by (clarsimp simp add: decode_page_invocation_def decode_page_table_invocation_def
decode_page_directory_invocation_def decode_pdpt_invocation_def
@ -110,9 +109,9 @@ lemma arch_decode_X64ASIDPoolAssign_empty_fail:
apply ((simp | wp)+)[1]
apply (subst bindE_assoc[symmetric])
apply (rule empty_fail_bindE)
subgoal by (fastforce simp: empty_fail_def whenE_def throwError_def select_def bindE_def
bind_def return_def returnOk_def lift_def liftE_def select_ext_def
gets_def get_def assert_def fail_def)
subgoal by (force simp: empty_fail_def whenE_def throwError_def select_def bindE_def
bind_def return_def returnOk_def lift_def liftE_def select_ext_def
gets_def get_def assert_def fail_def)
apply (clarsimp simp: decode_page_invocation_def decode_page_table_invocation_def
decode_page_directory_invocation_def decode_pdpt_invocation_def | wp | intro conjI)+
done
@ -142,9 +141,7 @@ context Arch begin global_naming X64
lemma flush_table_empty_fail[simp, wp]: "empty_fail (flush_table a b c d)"
unfolding flush_table_def
apply simp
apply (wp | wpc | simp)+
done
by wpsimp
crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: maskInterrupt, empty_slot,
finalise_cap, preemption_point,
@ -152,7 +149,7 @@ crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: maskInterrupt, empty_slo
(simp: Let_def catch_def split_def OR_choiceE_def mk_ef_def option.splits endpoint.splits
notification.splits thread_state.splits sum.splits cap.splits arch_cap.splits
kernel_object.splits vmpage_size.splits pde.splits bool.splits list.splits
forM_x_def empty_fail_mapM_x set_object_def
set_object_def
ignore: nativeThreadUsingFPU_impl switchFpuOwner_impl)
crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: setRegister, setNextPC

4
proof/invariant-abstract/X64/ArchTcb_AI.thy
View File

@ -198,7 +198,6 @@ lemma cap_delete_no_cap_to_obj_asid[wp, Tcb_AI_asms]:
apply (simp add: cap_delete_def
no_cap_to_obj_with_diff_ref_ran_caps_form)
apply wp
apply simp
apply (rule use_spec)
apply (rule rec_del_all_caps_in_range)
apply (simp add: table_cap_ref_def[simplified, split_simps cap.split]
@ -233,7 +232,8 @@ lemma tc_invs[Tcb_AI_asms]:
apply (simp add: split_def set_mcpriority_def cong: option.case_cong)
apply (rule hoare_vcg_precond_imp)
apply wp
apply ((simp only: simp_thms
apply ((simp only: simp_thms cong: conj_cong
| (strengthen invs_strengthen)+
| (simp add: conj_comms del: hoare_True_E_R,
strengthen imp_consequent[where Q="x = None" for x], simp cong: conj_cong)
| rule wp_split_const_if wp_split_const_if_R

2
proof/invariant-abstract/X64/ArchVSpaceEntries_AI.thy
View File

@ -681,8 +681,6 @@ lemma perform_invocation_valid_vspace_objs'[wp]:
\<lbrace>\<lambda>rv. valid_vspace_objs'\<rbrace>"
apply (cases i, simp_all)
apply (wp send_signal_interrupt_states | simp)+
apply (clarsimp simp:)
apply (wp | wpc | simp)+
apply (simp add: arch_perform_invocation_def)
apply (wp | wpc | simp)+
apply (auto simp: valid_arch_inv_def )

16
proof/invariant-abstract/X64/Machine_AI.thy
View File

@ -83,13 +83,13 @@ lemma det_getRestartPC: "det getRestartPC"
lemma det_setNextPC: "det (setNextPC p)"
by (simp add: setNextPC_def det_setRegister)
(* FIXME empty_fail: make all empty_fail [intro!, wp], and non-conditional ones [simp] *)
lemma ef_loadWord: "empty_fail (loadWord x)"
by (simp add: loadWord_def)
by (fastforce simp: loadWord_def)
lemma ef_storeWord: "empty_fail (storeWord x y)"
by (simp add: storeWord_def)
by (fastforce simp: storeWord_def)
lemma no_fail_getRestartPC: "no_fail \<top> getRestartPC"
@ -407,7 +407,7 @@ lemma empty_fail_initL2Cache: "empty_fail initL2Cache"
lemma empty_fail_clearMemory [simp, intro!]:
"\<And>a b. empty_fail (clearMemory a b)"
by (simp add: clearMemory_def mapM_x_mapM ef_storeWord)
by (fastforce simp: clearMemory_def mapM_x_mapM ef_storeWord)
lemma getFaultAddress_ef[simp,wp]: "empty_fail getFaultAddress"
by (simp add: getFaultAddress_def)
@ -428,19 +428,19 @@ lemma hwASIDInvalidate_ef[simp,wp]: "empty_fail (hwASIDInvalidate b a)"
by (simp add: hwASIDInvalidate_def)
lemma updateIRQState_ef[simp,wp]: "empty_fail (updateIRQState b c)"
by (simp add: updateIRQState_def)
by (fastforce simp: updateIRQState_def)
lemma writeCR3_ef[simp,wp]: "empty_fail (writeCR3 a b)"
by (simp add: writeCR3_def)
lemma in8_ef[simp,wp]: "empty_fail (in8 port)"
by (simp add: in8_def)
by (fastforce simp: in8_def)
lemma in16_ef[simp,wp]: "empty_fail (in16 port)"
by (simp add: in16_def)
by (fastforce simp: in16_def)
lemma in32_ef[simp,wp]: "empty_fail (in32 port)"
by (simp add: in32_def)
by (fastforce simp: in32_def)
lemma out8_ef[simp,wp]: "empty_fail (out8 port dat)"
by (simp add: out8_def)

3
proof/refine/ARM/Arch_R.thy
View File

@ -1536,7 +1536,8 @@ lemma createMappingEntires_valid_slots_duplicated'[wp]:
apply (rule_tac Q' = "\<lambda>p s. is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s"
in hoare_post_imp_R)
apply (wp lookupPTSlot_aligned lookupPTSlot_page_table_at')
apply (rule_tac x = r in exI)
apply (rename_tac rv s)
apply (rule_tac x = rv in exI)
apply (clarsimp simp: largePagePTEOffsets_def pteBits_def)
apply (frule is_aligned_no_wrap'[where off = "0x3c"])
apply simp

3
proof/refine/ARM/CSpace_R.thy
View File

@ -3968,8 +3968,9 @@ lemma setupReplyMaster_corres:
cte_wp_at' ((=) rv) (cte_map (t, tcb_cnode_index 2))"
in hoare_strengthen_post)
apply (wp hoare_drop_imps getCTE_wp')
apply (rename_tac rv s)
apply (clarsimp simp: cte_wp_at_ctes_of valid_mdb'_def valid_mdb_ctes_def)
apply (case_tac r, fastforce elim: valid_nullcapsE)
apply (case_tac rv, fastforce elim: valid_nullcapsE)
apply (fastforce elim: tcb_at_cte_at)
apply (clarsimp simp: cte_at'_obj_at' tcb_cte_cases_def cte_map_def)
apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def)

2
proof/refine/ARM/Detype_R.thy
View File

@ -2101,7 +2101,7 @@ qed
lemma empty_fail_locateCTE:
"empty_fail (locateCTE src)"
by (simp add:locateCTE_def bind_assoc split_def)
by (fastforce simp: locateCTE_def bind_assoc split_def)
lemma fail_empty_locateCTE:
"snd (locateCTE src s) \<Longrightarrow> fst (locateCTE src s) = {}"

31
proof/refine/ARM/EmptyFail.thy
View File

@ -19,12 +19,12 @@ lemma empty_fail_projectKO [simp, intro!]:
lemma empty_fail_alignCheck [intro!, wp, simp]:
"empty_fail (alignCheck a b)"
unfolding alignCheck_def
by (simp add: alignError_def)
by (fastforce simp: alignError_def)
lemma empty_fail_magnitudeCheck [intro!, wp, simp]:
"empty_fail (magnitudeCheck a b c)"
unfolding magnitudeCheck_def
by (simp split: option.splits)
by (fastforce split: option.splits)
lemma empty_fail_loadObject_default [intro!, wp, simp]:
shows "empty_fail (loadObject_default x b c d)"
@ -33,7 +33,7 @@ lemma empty_fail_loadObject_default [intro!, wp, simp]:
lemma empty_fail_threadGet [intro!, wp, simp]:
"empty_fail (threadGet f p)"
by (simp add: threadGet_def getObject_def split_def)
by (fastforce simp: threadGet_def getObject_def split_def)
lemma empty_fail_getCTE [intro!, wp, simp]:
"empty_fail (getCTE slot)"
@ -47,12 +47,12 @@ lemma empty_fail_getCTE [intro!, wp, simp]:
lemma empty_fail_updateObject_cte [intro!, wp, simp]:
"empty_fail (updateObject (v :: cte) ko a b c)"
by (simp add: updateObject_cte typeError_def unless_def split: kernel_object.splits )
by (fastforce simp: updateObject_cte typeError_def unless_def split: kernel_object.splits )
lemma empty_fail_setCTE [intro!, wp, simp]:
"empty_fail (setCTE p cte)"
unfolding setCTE_def
by (simp add: setObject_def split_def)
by (fastforce simp: setObject_def split_def)
lemma empty_fail_updateMDB [intro!, wp, simp]:
"empty_fail (updateMDB a b)"
@ -60,16 +60,15 @@ lemma empty_fail_updateMDB [intro!, wp, simp]:
lemma empty_fail_getSlotCap [intro!, wp, simp]:
"empty_fail (getSlotCap a)"
unfolding getSlotCap_def by simp
unfolding getSlotCap_def by fastforce
context begin interpretation Arch . (*FIXME: arch_split*)
lemma empty_fail_getObject:
assumes x: "(\<And>b c d. empty_fail (loadObject x b c d::'a :: pspace_storable kernel))"
assumes "\<And>b c d. empty_fail (loadObject x b c d::'a :: pspace_storable kernel)"
shows "empty_fail (getObject x :: 'a :: pspace_storable kernel)"
apply (simp add: getObject_def split_def)
apply (safe intro!: empty_fail_bind empty_fail_gets empty_fail_assert_opt)
apply (rule x)
apply (safe intro!: assms)
done
lemma empty_fail_getObject_tcb [intro!, wp, simp]:
@ -78,22 +77,22 @@ lemma empty_fail_getObject_tcb [intro!, wp, simp]:
lemma empty_fail_updateTrackedFreeIndex [intro!, wp, simp]:
shows "empty_fail (updateTrackedFreeIndex p idx)"
by (simp add: updateTrackedFreeIndex_def)
by (fastforce simp add: updateTrackedFreeIndex_def)
lemma empty_fail_updateNewFreeIndex [intro!, wp, simp]:
shows "empty_fail (updateNewFreeIndex p)"
apply (simp add: updateNewFreeIndex_def)
apply (safe intro!: empty_fail_bind)
apply safe
apply (simp split: capability.split)
done
lemma empty_fail_insertNewCap [intro!, wp, simp]:
"empty_fail (insertNewCap p p' cap)"
unfolding insertNewCap_def by simp
unfolding insertNewCap_def by fastforce
lemma empty_fail_getIRQSlot [intro!, wp, simp]:
"empty_fail (getIRQSlot irq)"
by (simp add: getIRQSlot_def getInterruptState_def locateSlot_conv)
by (fastforce simp: getIRQSlot_def getInterruptState_def locateSlot_conv)
lemma empty_fail_getObject_ntfn [intro!, wp, simp]:
"empty_fail (getObject p :: Structures_H.notification kernel)"
@ -107,15 +106,15 @@ lemma empty_fail_lookupIPCBuffer [intro!, wp, simp]:
"empty_fail (lookupIPCBuffer a b)"
by (clarsimp simp: lookupIPCBuffer_def
Let_def getThreadBufferSlot_def locateSlot_conv
split: capability.splits arch_capability.splits | wp | wpc)+
split: capability.splits arch_capability.splits | wp | wpc | safe)+
lemma empty_fail_updateObject_default [intro!, wp, simp]:
"empty_fail (updateObject_default v ko a b c)"
by (simp add: updateObject_default_def typeError_def unless_def split: kernel_object.splits )
by (fastforce simp: updateObject_default_def typeError_def unless_def split: kernel_object.splits)
lemma empty_fail_threadSet [intro!, wp, simp]:
"empty_fail (threadSet f p)"
by (simp add: threadSet_def getObject_def setObject_def split_def)
by (fastforce simp: threadSet_def getObject_def setObject_def split_def)
lemma empty_fail_getThreadState[iff]:
"empty_fail (getThreadState t)"

Some files were not shown because too many files have changed in this diff Show More