Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Minor improvements to CRefine #699

Merged
merged 6 commits into from
Apr 13, 2024
Merged

Minor improvements to CRefine #699

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
7270f50
crefine: generalise syscall_error_throwError_ccorres lemmas
corlewis Jun 1, 2023
9030888
crefine: replace get_tsType_ccorres with get_tsType_ccorres2
corlewis May 26, 2023
134f3fd
crefine: remove old-style UNIV from precondition
corlewis Mar 27, 2024
88c3420
cspec+crefine: add ThreadState_defs
corlewis Nov 14, 2023
c5b8400
cspec: add a comment to KernelState_C with its purpose
corlewis Apr 9, 2024
2a83c2c
arm+arm_hyp+aarch64 crefine: fix name of setThreadState_tcbContext
corlewis Dec 6, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 1 addition & 5 deletions proof/crefine/AARCH64/ADT_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -817,11 +817,7 @@ lemma cthread_state_rel_imp_eq:
"cthread_state_relation x z \<Longrightarrow> cthread_state_relation y z \<Longrightarrow> x=y"
apply (simp add: cthread_state_relation_def split_def)
apply (cases x)
apply (cases y, simp_all add: ThreadState_BlockedOnReceive_def
ThreadState_BlockedOnReply_def ThreadState_BlockedOnNotification_def
ThreadState_Running_def ThreadState_Inactive_def
ThreadState_IdleThreadState_def ThreadState_BlockedOnSend_def
ThreadState_Restart_def)+
apply (cases y, simp_all add: ThreadState_defs)+
done

lemma ksPSpace_valid_objs_tcbBoundNotification_nonzero:
Expand Down
28 changes: 13 additions & 15 deletions proof/crefine/AARCH64/Arch_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1414,7 +1414,7 @@ lemma performPageGetAddress_ccorres:
apply clarsimp
apply (vcg exspec=setRegister_modifies)
apply wpsimp
apply (clarsimp simp: ThreadState_Running_def)
apply clarsimp
apply (vcg exspec=lookupIPCBuffer_modifies)
apply clarsimp
apply vcg
Expand All @@ -1426,7 +1426,7 @@ lemma performPageGetAddress_ccorres:
seL4_MessageInfo_lift_def message_info_to_H_def mask_def)
apply (cases isCall)
apply (auto simp: AARCH64.badgeRegister_def AARCH64_H.badgeRegister_def Kernel_C.badgeRegister_def
fromPAddr_def ThreadState_Running_def Kernel_C.X0_def Kernel_C.X1_def
fromPAddr_def ThreadState_defs Kernel_C.X0_def Kernel_C.X1_def
pred_tcb_at'_def obj_at'_def ct_in_state'_def)
done

Expand Down Expand Up @@ -2940,7 +2940,7 @@ lemma decodeARMMMUInvocation_ccorres:
apply (rule_tac Q'=UNIV and A'="{}" in conseqPost)
apply (vcg exspec=ensureEmptySlot_modifies)
apply (frule length_ineq_not_Nil)
apply (clarsimp simp: null_def ThreadState_Restart_def mask_def hd_conv_nth
apply (clarsimp simp: null_def ThreadState_defs mask_def hd_conv_nth
isCap_simps rf_sr_ksCurThread cap_get_tag_UntypedCap
word_le_make_less asid_high_bits_def
split: list.split)
Expand Down Expand Up @@ -3290,8 +3290,7 @@ lemma decodeARMMMUInvocation_ccorres:
apply clarsimp
apply (clarsimp simp: cte_wp_at_ctes_of asidHighBits_handy_convs
word_sle_def word_sless_def asidLowBits_handy_convs
rf_sr_ksCurThread "StrictC'_thread_state_defs"
mask_def[where n=4]
rf_sr_ksCurThread ThreadState_defs mask_def[where n=4]
cong: if_cong)
apply (clarsimp simp: ccap_relation_isDeviceCap2 objBits_simps pageBits_def case_bool_If)
apply (rule conjI; clarsimp)
Expand Down Expand Up @@ -3554,7 +3553,7 @@ lemma invokeVCPUReadReg_ccorres: (* styled after invokeTCB_ReadRegisters_ccorres
apply clarsimp
apply (vcg exspec=setRegister_modifies)
apply wpsimp
apply (clarsimp simp: ThreadState_Running_def)
apply clarsimp
apply (vcg exspec=lookupIPCBuffer_modifies)
apply clarsimp
apply (wpsimp wp: hoare_vcg_const_imp_lift hoare_vcg_all_lift hoare_vcg_imp_lift)
Expand All @@ -3565,15 +3564,14 @@ lemma invokeVCPUReadReg_ccorres: (* styled after invokeTCB_ReadRegisters_ccorres
apply (rule conseqPre, vcg)
apply clarsimp
apply (clarsimp simp: invs_no_0_obj' tcb_at_invs' invs_queues invs_valid_objs' invs_sch_act_wf'
rf_sr_ksCurThread msgRegisters_unfold
seL4_MessageInfo_lift_def message_info_to_H_def mask_def)
rf_sr_ksCurThread msgRegisters_unfold ThreadState_defs
seL4_MessageInfo_lift_def message_info_to_H_def mask_def)
apply (cases isCall; clarsimp)
apply (rule conjI, clarsimp simp: ct_in_state'_def st_tcb_at'_def comp_def)
apply (fastforce simp: obj_at'_def projectKOs)
apply (clarsimp simp: Kernel_C.badgeRegister_def AARCH64.badgeRegister_def
AARCH64_H.badgeRegister_def C_register_defs)
apply (simp add: rf_sr_def cstate_relation_def Let_def)
apply (clarsimp simp: ThreadState_Running_def)
apply (rule conjI, clarsimp simp: pred_tcb_at'_def obj_at'_def projectKOs ct_in_state'_def)
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def)
done
Expand Down Expand Up @@ -3662,7 +3660,7 @@ lemma decodeVCPUWriteReg_ccorres:
apply (clarsimp simp: word_less_nat_alt word_le_nat_alt conj_commute
invs_no_0_obj' tcb_at_invs' invs_queues invs_valid_objs' invs_sch_act_wf'
rf_sr_ksCurThread msgRegisters_unfold
valid_tcb_state'_def ThreadState_Restart_def mask_def)
valid_tcb_state'_def ThreadState_defs mask_def)
apply (rule conjI; clarsimp) \<comment> \<open>not enough args\<close>
apply (clarsimp simp: isCap_simps cap_get_tag_isCap capVCPUPtr_eq)
apply (subst from_to_enum; clarsimp simp: fromEnum_maxBound_vcpureg_def)
Expand Down Expand Up @@ -3917,7 +3915,7 @@ lemma decodeVCPUInjectIRQ_ccorres:
apply (clarsimp simp: word_less_nat_alt word_le_nat_alt conj_commute
invs_no_0_obj' tcb_at_invs' invs_queues invs_valid_objs' invs_sch_act_wf'
rf_sr_ksCurThread msgRegisters_unfold
valid_tcb_state'_def ThreadState_Restart_def mask_def)
valid_tcb_state'_def ThreadState_defs mask_def)

apply (frule invs_arch_state')
apply (clarsimp simp: valid_arch_state'_def max_armKSGICVCPUNumListRegs_def rf_sr_armKSGICVCPUNumListRegs)
Expand Down Expand Up @@ -4019,7 +4017,7 @@ lemma decodeVCPUReadReg_ccorres:
apply (clarsimp simp: word_le_nat_alt conj_commute
invs_no_0_obj' tcb_at_invs' invs_queues invs_valid_objs' invs_sch_act_wf'
rf_sr_ksCurThread msgRegisters_unfold
valid_tcb_state'_def ThreadState_Restart_def mask_def)
valid_tcb_state'_def ThreadState_defs mask_def)

apply (rule conjI; clarsimp) \<comment> \<open>no args\<close>
subgoal by (clarsimp simp: isCap_simps cap_get_tag_isCap capVCPUPtr_eq)
Expand Down Expand Up @@ -4123,7 +4121,7 @@ lemma decodeVCPUSetTCB_ccorres:
apply (clarsimp simp: word_less_nat_alt word_le_nat_alt conj_commute
invs_no_0_obj' tcb_at_invs' invs_queues invs_valid_objs' invs_sch_act_wf'
rf_sr_ksCurThread msgRegisters_unfold
valid_tcb_state'_def ThreadState_Restart_def mask_def)
valid_tcb_state'_def ThreadState_defs mask_def)
apply (clarsimp simp: idButNot_def interpret_excaps_test_null
excaps_map_def neq_Nil_conv)
apply (rule conjI; clarsimp)
Expand Down Expand Up @@ -4276,15 +4274,15 @@ proof -
apply (clarsimp simp: word_le_nat_alt conj_commute
invs_no_0_obj' tcb_at_invs' invs_queues invs_valid_objs' invs_sch_act_wf'
rf_sr_ksCurThread msgRegisters_unfold
valid_tcb_state'_def ThreadState_Restart_def mask_def
valid_tcb_state'_def mask_def
valid_cap'_def ct_in_state'_def sysargs_rel_to_n st_tcb_at'_def comp_def
runnable'_eq)
apply (fastforce elim: obj_at'_weakenE)
(* C side *)
apply (clarsimp simp: word_le_nat_alt conj_commute
invs_no_0_obj' tcb_at_invs' invs_queues invs_valid_objs' invs_sch_act_wf'
rf_sr_ksCurThread msgRegisters_unfold
valid_tcb_state'_def ThreadState_Restart_def Kernel_C.maxIRQ_def
valid_tcb_state'_def ThreadState_defs Kernel_C.maxIRQ_def
and_mask_eq_iff_le_mask capVCPUPtr_eq)
apply (clarsimp simp: mask_def)
done
Expand Down
10 changes: 5 additions & 5 deletions proof/crefine/AARCH64/Fastpath_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ lemma setCTE_tcbContext:
apply (rule setObject_cte_obj_at_tcb', simp_all)
done

lemma seThreadState_tcbContext:
lemma setThreadState_tcbContext:
"\<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>
setThreadState a b
\<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>"
Expand All @@ -73,7 +73,7 @@ lemma setBoundNotification_tcbContext:
declare comp_apply [simp del]
crunch tcbContext[wp]: deleteCallerCap "obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t"
(wp: setEndpoint_obj_at_tcb' setBoundNotification_tcbContext
setNotification_tcb crunch_wps seThreadState_tcbContext
setNotification_tcb crunch_wps setThreadState_tcbContext
simp: crunch_simps unless_def)
declare comp_apply [simp]

Expand Down Expand Up @@ -798,7 +798,7 @@ lemma thread_state_ptr_set_tsType_np_spec:
apply (clarsimp simp: typ_heap_simps')
apply (rule exI, rule conjI[OF _ conjI [OF _ refl]])
apply (simp_all add: thread_state_lift_def)
apply (auto simp: "StrictC'_thread_state_defs" mask_def)
apply (auto simp: ThreadState_defs mask_def)
done

(* from the bitfield generator: ep_ref and tsType are stored in the same word, tsType is the lowest
Expand Down Expand Up @@ -3140,7 +3140,7 @@ proof -
apply (clarsimp simp: rf_sr_ksCurThread typ_heap_simps'
h_t_valid_clift_Some_iff)
apply (clarsimp simp: capAligned_def isCap_simps objBits_simps
"StrictC'_thread_state_defs" mask_def)
ThreadState_defs mask_def)
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
typ_heap_simps' objBits_defs)
apply (rule conjI)
Expand All @@ -3151,7 +3151,7 @@ proof -
apply (simp add: cep_relations_drop_fun_upd)
apply (erule cmap_relation_updI, erule ko_at_projectKO_opt)
apply (simp add: ctcb_relation_def cthread_state_relation_def
"StrictC'_thread_state_defs")
ThreadState_defs)
apply (clarsimp simp: ccap_relation_ep_helpers)
apply simp
apply (rule conjI, erule cready_queues_relation_not_queue_ptrs)
Expand Down
6 changes: 3 additions & 3 deletions proof/crefine/AARCH64/Fastpath_Equiv.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,7 @@ lemma setCTE_tcbContext:

context begin interpretation Arch . (*FIXME: arch_split*)

lemma seThreadState_tcbContext:
lemma setThreadState_tcbContext:
"\<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>
setThreadState a b
\<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>"
Expand All @@ -68,7 +68,7 @@ lemma setBoundNotification_tcbContext:
declare comp_apply [simp del]
crunch tcbContext[wp]: deleteCallerCap "obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t"
(wp: setEndpoint_obj_at_tcb' setBoundNotification_tcbContext
setNotification_tcb crunch_wps seThreadState_tcbContext
setNotification_tcb crunch_wps setThreadState_tcbContext
simp: crunch_simps unless_def)
declare comp_apply [simp]

Expand Down Expand Up @@ -1697,7 +1697,7 @@ lemma fastpath_callKernel_SysReplyRecv_corres:
fastpathBestSwitchCandidate_lift[where f="threadSet f t" for f t]
| wps)+)[3]
apply (simp cong: rev_conj_cong)
apply (wpsimp wp: seThreadState_tcbContext[simplified comp_apply]
apply (wpsimp wp: setThreadState_tcbContext[simplified comp_apply]
setThreadState_oa_queued user_getreg_rv
setThreadState_no_sch_change setThreadState_obj_at_unchanged
sts_st_tcb_at'_cases sts_bound_tcb_at'
Expand Down
10 changes: 4 additions & 6 deletions proof/crefine/AARCH64/Finalise_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -241,10 +241,8 @@ next
sts_running_valid_queues sts_st_tcb' setThreadState_oa_queued | simp)+

apply (vcg exspec=setThreadState_cslift_spec exspec=tcbSchedEnqueue_cslift_spec)
apply (clarsimp simp: tcb_at_not_NULL
Collect_const_mem valid_tcb_state'_def
ThreadState_Restart_def mask_def
valid_objs'_maxDomain valid_objs'_maxPriority)
apply (clarsimp simp: tcb_at_not_NULL Collect_const_mem valid_tcb_state'_def
ThreadState_defs mask_def valid_objs'_maxDomain valid_objs'_maxPriority)
apply (drule(1) obj_at_cslift_tcb)
apply (clarsimp simp: typ_heap_simps)
apply (rule conjI)
Expand Down Expand Up @@ -623,7 +621,7 @@ lemma suspend_ccorres:
apply clarsimp
apply (rule iffI)
apply simp
apply (erule thread_state_to_tsType.elims; simp add: StrictC'_thread_state_defs)
apply (erule thread_state_to_tsType.elims; simp add: ThreadState_defs)
apply (ctac (no_vcg) add: updateRestartPC_ccorres)
apply (rule ccorres_return_Skip)
apply ceqv
Expand Down Expand Up @@ -658,7 +656,7 @@ lemma suspend_ccorres:
apply (rule delete_one_conc_fr.cancelIPC_invs)
apply (fastforce simp: invs_valid_queues' invs_queues invs_valid_objs'
valid_tcb_state'_def)
apply (auto simp: "StrictC'_thread_state_defs")
apply (auto simp: ThreadState_defs)
done

lemma cap_to_H_NTFNCap_tag:
Expand Down
11 changes: 4 additions & 7 deletions proof/crefine/AARCH64/Interrupt_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -232,7 +232,7 @@ supply [[goals_limit=20]]
apply (clarsimp simp: Collect_const_mem neq_Nil_conv
dest!: interpret_excaps_eq)
apply (simp add: rf_sr_ksCurThread mask_def[where n=4]
"StrictC'_thread_state_defs" cap_get_tag_isCap excaps_map_def
ThreadState_defs cap_get_tag_isCap excaps_map_def
word_sless_def word_sle_def)
apply (simp add: invocationCatch_def throwError_bind
interpret_excaps_test_null Collect_True
Expand Down Expand Up @@ -262,8 +262,7 @@ supply [[goals_limit=20]]
apply (clarsimp simp: invs_queues invs_valid_objs'
ct_in_state'_def
ccap_rights_relation_def
mask_def[where n=4]
"StrictC'_thread_state_defs")
mask_def[where n=4] ThreadState_defs)
apply (subst pred_tcb'_weakenE, assumption, fastforce)+
apply (clarsimp simp: rf_sr_ksCurThread word_sle_def word_sless_def
sysargs_rel_n_def word_less_nat_alt)
Expand Down Expand Up @@ -585,7 +584,7 @@ lemma Arch_decodeIRQControlInvocation_ccorres:
apply (simp add: and_mask_eq_iff_le_mask)
apply (simp add: mask_def word_le_nat_alt)
apply (clarsimp simp: numeral_2_eq_2 numeral_3_eq_3 exception_defs
ThreadState_Restart_def mask_def)
ThreadState_defs mask_def)
apply (rule conseqPre, vcg)
apply (fastforce simp: exception_defs split: if_split)
apply (rule subset_refl)
Expand All @@ -608,7 +607,6 @@ lemma Arch_decodeIRQControlInvocation_ccorres:
apply clarsimp
apply (clarsimp simp: interpret_excaps_test_null excaps_map_def
Collect_const_mem word_sless_def word_sle_def
ThreadState_Restart_def unat_of_nat mask_def
sysargs_rel_to_n
cong: if_cong)
apply (rule conjI)
Expand Down Expand Up @@ -752,7 +750,7 @@ lemma decodeIRQControlInvocation_ccorres:
apply (rule sym)
apply (simp add: and_mask_eq_iff_le_mask)
apply (simp add: mask_def word_le_nat_alt)
apply (clarsimp simp: numeral_2_eq_2 exception_defs ThreadState_Restart_def mask_def)
apply (clarsimp simp: numeral_2_eq_2 exception_defs ThreadState_defs mask_def)
apply (rule conseqPre, vcg)
apply (fastforce simp: exception_defs)
apply (rule subset_refl)
Expand All @@ -778,7 +776,6 @@ lemma decodeIRQControlInvocation_ccorres:
apply clarsimp
apply (clarsimp simp: interpret_excaps_test_null excaps_map_def
Collect_const_mem word_sless_def word_sle_def
ThreadState_Restart_def unat_of_nat mask_def
sysargs_rel_to_n
cong: if_cong)
apply (rule conjI)
Expand Down
10 changes: 4 additions & 6 deletions proof/crefine/AARCH64/Invoke_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -199,7 +199,7 @@ lemma decodeDomainInvocation_ccorres:
apply (clarsimp simp: valid_tcb_state'_def invs_valid_queues' invs_valid_objs'
invs_queues invs_sch_act_wf' ct_in_state'_def pred_tcb_at'
rf_sr_ksCurThread word_sle_def word_sless_def sysargs_rel_to_n
mask_eq_iff_w2p mask_eq_iff_w2p word_size "StrictC'_thread_state_defs")
mask_eq_iff_w2p mask_eq_iff_w2p word_size ThreadState_defs)
apply (rule conjI)
apply (clarsimp simp: linorder_not_le isCap_simps)
apply (rule conjI, clarsimp simp: unat64_eq_of_nat)
Expand Down Expand Up @@ -1365,7 +1365,7 @@ lemma decodeCNodeInvocation_ccorres:
apply (frule interpret_excaps_eq)
apply (clarsimp simp: excaps_map_def mask_def[where n=4]
ccap_rights_relation_def rightsFromWord_wordFromRights
"StrictC'_thread_state_defs" map_comp_Some_iff
ThreadState_defs map_comp_Some_iff
rf_sr_ksCurThread hd_conv_nth hd_drop_conv_nth)
apply ((rule conjI
| clarsimp simp: rightsFromWord_wordFromRights
Expand Down Expand Up @@ -3294,8 +3294,7 @@ lemma decodeUntypedInvocation_ccorres_helper:
unat_of_nat_APIType_capBits word_size hd_conv_nth length_ineq_not_Nil
not_less word_le_nat_alt isCap_simps valid_cap_simps')
apply (strengthen word_of_nat_less)
apply (clarsimp simp: StrictC'_thread_state_defs mask_def
ccap_relation_isDeviceCap2
apply (clarsimp simp: ThreadState_defs mask_def ccap_relation_isDeviceCap2
split: if_split)
apply (clarsimp simp: not_less shiftr_overflow maxUntypedSizeBits_def
unat_of_nat_APIType_capBits)
Expand Down Expand Up @@ -3401,8 +3400,7 @@ lemma decodeUntypedInvocation_ccorres_helper:
apply (clarsimp simp: hd_drop_conv_nth2 hd_conv_nth neq_Nil_lengthI
ct_in_state'_def pred_tcb_at'
rf_sr_ksCurThread mask_eq_iff_w2p
"StrictC'_thread_state_defs" numeral_eqs[symmetric]
cap_get_tag_isCap cte_wp_at_ctes_of
numeral_eqs[symmetric] cap_get_tag_isCap cte_wp_at_ctes_of
unat_eq_0 ccHoarePost_def)
apply (rule conjI)
apply (clarsimp simp: linorder_not_less isCap_simps)
Expand Down
Loading
Loading