Skip to content

arch-split Ipc_R #993

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

Open
Xaphiosis wants to merge 7 commits into
base: master
Choose a base branch
from
Open

arch-split Ipc_R #993

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
40ac22a
refine: improve TcbAcc_R arch-split
Xaphiosis May 12, 2026
8fce45d
refine: Ipc_R given arch prefix
Xaphiosis May 7, 2026
0982e70
[wip] copy AARCH64 version of Ipc_R
Xaphiosis May 7, 2026
7faa48c
refine: arch-split Ipc_R (AARCH64 ONLY)
Xaphiosis May 12, 2026
390dd8f
[wip][fake] copy AARCH64 version of ArchIpc_R
Xaphiosis May 12, 2026
ce78e5a
refine: arch-split Ipc_R (OTHER ARCHES)
Xaphiosis May 12, 2026
a512049
crefine: update for Ipc_R arch-split
Xaphiosis May 12, 2026
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: 4 additions & 2 deletions proof/crefine/AARCH64/Arch_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -898,7 +898,7 @@ lemma decodeARMPageTableInvocation_ccorres:
(decodeARMMMUInvocation label args cptr slot cp extraCaps
>>= invocationCatch thread isBlocking isCall InvokeArchObject)
(Call decodeARMPageTableInvocation_'proc)"
supply Collect_const[simp del] if_cong[cong] option.case_cong[cong]
supply Collect_const[simp del] if_cong[cong] option.case_cong[cong] tl_drop_1[simp]
apply (clarsimp simp only: isCap_simps)
apply (cinit' lift: invLabel_' length___unsigned_long_' cte_'
current_extra_caps_' cap_' buffer_'
Expand Down Expand Up @@ -1828,6 +1828,7 @@ lemma decodeARMFrameInvocation_ccorres:
>>= invocationCatch thread isBlocking isCall InvokeArchObject)
(Call decodeARMFrameInvocation_'proc)"
(is "\<lbrakk> _; _ \<rbrakk> \<Longrightarrow> ccorres _ _ ?P _ _ _ _")
supply tl_drop_1[simp]
apply (clarsimp simp only: isCap_simps)
apply (cinit' lift: invLabel_' length___unsigned_long_' cte_'
current_extra_caps_' cap_' buffer_' call_'
Expand Down Expand Up @@ -2484,6 +2485,7 @@ lemma decodeARMVSpaceRootInvocation_ccorres:
(decodeARMMMUInvocation label args cptr slot cp extraCaps
>>= invocationCatch thread isBlocking isCall InvokeArchObject)
(Call decodeARMVSpaceRootInvocation_'proc)"
supply tl_drop_1[simp]
apply (clarsimp simp only: isCap_simps)
apply (cinit' lift: invLabel_' length___unsigned_long_' cte_' current_extra_caps_' cap_' buffer_')
apply (simp add: Let_def isCap_simps invocation_eq_use_types decodeARMMMUInvocation_def
Expand Down Expand Up @@ -2702,7 +2704,7 @@ lemma decodeARMMMUInvocation_ccorres:
(decodeARMMMUInvocation label args cptr slot cp extraCaps
>>= invocationCatch thread isBlocking isCall InvokeArchObject)
(Call decodeARMMMUInvocation_'proc)"
supply ccorres_prog_only_cong[cong]
supply ccorres_prog_only_cong[cong] tl_drop_1[simp]
apply (cinit' lift: invLabel_' length___unsigned_long_' cte_'
current_extra_caps_' cap_' buffer_' call_')
apply csymbr
Expand Down
4 changes: 2 additions & 2 deletions proof/crefine/AARCH64/Interrupt_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -475,7 +475,7 @@ lemma Arch_decodeIRQControlInvocation_ccorres:
(Arch.decodeIRQControlInvocation label args srcSlot (map fst extraCaps)
>>= invocationCatch thread isBlocking isCall (InvokeIRQControl o ArchIRQControl))
(Call Arch_decodeIRQControlInvocation_'proc)"
supply maxIRQ_casts[simp]
supply maxIRQ_casts[simp] tl_drop_1[simp]
supply gen_invocation_type_eq[simp] if_cong[cong] Collect_const[simp del]
apply (cinit' lift: invLabel_' length___unsigned_long_' srcSlot_' current_extra_caps_' buffer_'
simp: ArchInterrupt_H.AARCH64_H.decodeIRQControlInvocation_def)
Expand Down Expand Up @@ -769,7 +769,7 @@ lemma decodeIRQControlInvocation_ccorres:
>>= invocationCatch thread isBlocking isCall InvokeIRQControl)
(Call decodeIRQControlInvocation_'proc)"
supply gen_invocation_type_eq[simp] if_cong[cong] Collect_const[simp del]
supply maxIRQ_casts[simp]
supply maxIRQ_casts[simp] tl_drop_1[simp]
apply (cinit' lift: invLabel_' srcSlot_' length___unsigned_long_' current_extra_caps_' buffer_')
apply (simp add: decodeIRQControlInvocation_def invocation_eq_use_types
cong: StateSpace.state.fold_congs globals.fold_congs)
Expand Down
1 change: 1 addition & 0 deletions proof/crefine/AARCH64/Invoke_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1007,6 +1007,7 @@ lemma decodeCNodeInvocation_ccorres:
>>= invocationCatch thread isBlocking isCall InvokeCNode)
(Call decodeCNodeInvocation_'proc)"
supply if_cong[cong]
supply tl_drop_1[simp]
apply (cases "\<not>isCNodeCap cp")
apply (simp add: decodeCNodeInvocation_def
cong: conj_cong)
Expand Down
5 changes: 3 additions & 2 deletions proof/crefine/AARCH64/Ipc_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2577,7 +2577,7 @@ lemma transferCapsLoop_ccorres:
(W ep caps')"
unfolding W_def check1_def check2_def split_def
proof (rule ccorres_gen_asm, induct caps arbitrary: n slots mi)
note if_split[split]
note if_split[split] tl_drop_1[simp]
case Nil
thus ?case
apply (simp only: transferCapsToSlots.simps)
Expand Down Expand Up @@ -2812,7 +2812,8 @@ next
in hoare_strengthen_postE_R)
prefer 2
apply (clarsimp simp: cte_wp_at_ctes_of valid_pspace'_splits valid_pspace_canonical'
is_derived_capMasterCap image_def)
is_derived_capMasterCap image_def valid_pspace_mdb'
valid_pspace_valid_objs')
apply (clarsimp split:if_splits)
apply (rule conjI)
apply clarsimp+
Expand Down
3 changes: 2 additions & 1 deletion proof/crefine/AARCH64/Tcb_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2297,7 +2297,7 @@ lemma decodeWriteRegisters_ccorres:
(decodeWriteRegisters args cp
>>= invocationCatch thread isBlocking isCall InvokeTCB)
(Call decodeWriteRegisters_'proc)"
supply unsigned_numeral[simp del]
supply unsigned_numeral[simp del] tl_drop_1[simp]
apply (cinit' lift: cap_' length___unsigned_long_' buffer_' simp: decodeWriteRegisters_def)
apply (rename_tac length' cap')
apply (rule ccorres_Cond_rhs_Seq)
Expand Down Expand Up @@ -4623,6 +4623,7 @@ lemma decodeSetFlags_ccorres:
(decodeSetFlags args cp
>>= invocationCatch thread isBlocking isCall InvokeTCB)
(Call decodeSetFlags_'proc)"
supply tl_drop_1[simp]
apply (cinit' lift: cap_' length___unsigned_long_' buffer_' call_'
simp: decodeSetFlags_def )
apply csymbr+
Expand Down
7 changes: 4 additions & 3 deletions proof/crefine/ARM/Arch_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -601,7 +601,7 @@ lemma decodeARMPageTableInvocation_ccorres:
(decodeARMMMUInvocation label args cptr slot cp extraCaps
>>= invocationCatch thread isBlocking isCall InvokeArchObject)
(Call decodeARMPageTableInvocation_'proc)"
supply if_cong[cong]
supply if_cong[cong] tl_drop_1[simp]
apply (clarsimp simp only: isCap_simps)
apply (cinit' lift: invLabel_' length___unsigned_long_' cte_' current_extra_caps_' cap_' buffer_'
simp: decodeARMMMUInvocation_def invocation_eq_use_types)
Expand Down Expand Up @@ -2294,7 +2294,7 @@ lemma decodeARMFrameInvocation_ccorres:
(decodeARMMMUInvocation label args cptr slot cp extraCaps
>>= invocationCatch thread isBlocking isCall InvokeArchObject)
(Call decodeARMFrameInvocation_'proc)"
supply if_cong[cong] option.case_cong[cong]
supply if_cong[cong] option.case_cong[cong] tl_drop_1[simp]
apply (clarsimp simp only: isCap_simps)
apply (cinit' lift: invLabel_' length___unsigned_long_' cte_' current_extra_caps_' cap_' buffer_' call_'
simp: decodeARMMMUInvocation_def decodeARMPageFlush_def)
Expand Down Expand Up @@ -2943,6 +2943,7 @@ lemma decodeARMPageDirectoryInvocation_ccorres:
(decodeARMMMUInvocation label args cptr slot cp extraCaps
>>= invocationCatch thread isBlocking isCall InvokeArchObject)
(Call decodeARMPageDirectoryInvocation_'proc)"
supply tl_drop_1[simp]
apply (clarsimp simp only: isCap_simps)
apply (cinit' lift: invLabel_' length___unsigned_long_' cte_' current_extra_caps_' cap_' buffer_'
simp: decodeARMMMUInvocation_def invocation_eq_use_types)
Expand Down Expand Up @@ -3256,7 +3257,7 @@ lemma decodeARMMMUInvocation_ccorres:
>>= invocationCatch thread isBlocking isCall InvokeArchObject)
(Call decodeARMMMUInvocation_'proc)"
(is "\<lbrakk> ?F; _ \<rbrakk> \<Longrightarrow> ccorres ?r ?xf ?P (?P' slot_') [] ?a ?c")
supply if_cong[cong]
supply if_cong[cong] tl_drop_1[simp]
apply (cinit' lift: invLabel_' length___unsigned_long_' cte_'
current_extra_caps_' cap_' buffer_' call_')
apply csymbr
Expand Down
10 changes: 6 additions & 4 deletions proof/crefine/ARM/DetWP.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -136,20 +136,22 @@ lemma det_wp_getMRs:
apply (clarsimp simp: getMRs_def)
apply (rule det_wp_pre)
apply (wp det_mapM det_getRegister order_refl det_wp_mapM)
apply (fold word_size_bits_def)
apply (simp add: word_size)
apply (wp asUser_inv mapM_wp' getRegister_inv)
apply clarsimp
apply (simp add: wordSize_word_size pointerInUserData_def)
apply (rule conjI)
apply (simp add: pointerInUserData_def wordSize_def' word_size)
apply (erule valid_ipc_buffer_ptr'D2)
apply (simp add: pointerInUserData_def word_size_def)
apply (rule word_mult_less_mono1)
apply (erule order_le_less_trans)
apply (simp add: msgMaxLength_def max_ipc_words)
apply simp
apply (simp add: max_ipc_words)
apply (simp add: is_aligned_mult_triv2 [where n = 2, simplified] word_bits_conv)
apply (erule valid_ipc_buffer_ptr_aligned_2)
apply (simp add: wordSize_def' is_aligned_mult_triv2 [where n = 2, simplified] word_bits_conv)
apply (simp add: word_size_word_size_bits is_aligned_mult_triv2[where n = word_size_bits])
apply (erule valid_ipc_buffer_ptr_aligned_word_size_bits)
apply (simp add: word_size_word_size_bits is_aligned_mult_triv2[where n = word_size_bits])
done

end
Expand Down
3 changes: 2 additions & 1 deletion proof/crefine/ARM/Interrupt_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -543,6 +543,7 @@ lemma Arch_decodeIRQControlInvocation_ccorres:
(Arch.decodeIRQControlInvocation label args slot (map fst extraCaps)
>>= invocationCatch thread isBlocking isCall (InvokeIRQControl o ArchIRQControl))
(Call Arch_decodeIRQControlInvocation_'proc)"
supply tl_drop_1[simp]
apply (cinit' lift: invLabel_' srcSlot_' length___unsigned_long_' current_extra_caps_' buffer_')
apply (simp add: ARM_H.decodeIRQControlInvocation_def invocation_eq_use_types
del: Collect_const
Expand Down Expand Up @@ -829,7 +830,7 @@ lemma Arch_decodeIRQControlInvocation_ccorres:
dest!: interpret_excaps_eq)

lemma decodeIRQControlInvocation_ccorres:
notes if_cong[cong]
notes if_cong[cong] tl_drop_1[simp]
shows
"interpret_excaps extraCaps' = excaps_map extraCaps \<Longrightarrow>
ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
Expand Down
1 change: 1 addition & 0 deletions proof/crefine/ARM/Invoke_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1003,6 +1003,7 @@ lemma decodeCNodeInvocation_ccorres:
>>= invocationCatch thread isBlocking isCall InvokeCNode)
(Call decodeCNodeInvocation_'proc)"
supply if_cong[cong]
supply tl_drop_1[simp]
apply (cases "\<not>isCNodeCap cp")
apply (simp add: decodeCNodeInvocation_def
cong: conj_cong)
Expand Down
2 changes: 1 addition & 1 deletion proof/crefine/ARM/Ipc_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2374,7 +2374,7 @@ lemma transferCapsLoop_ccorres:
(W ep caps')"
unfolding W_def check1_def check2_def split_def
proof (rule ccorres_gen_asm, induct caps arbitrary: n slots mi)
note if_split[split]
note if_split[split] tl_drop_1[simp]
case Nil
thus ?case
apply (simp only: transferCapsToSlots.simps)
Expand Down
1 change: 1 addition & 0 deletions proof/crefine/ARM/Tcb_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4511,6 +4511,7 @@ lemma decodeSetFlags_ccorres:
(decodeSetFlags args cp
>>= invocationCatch thread isBlocking isCall InvokeTCB)
(Call decodeSetFlags_'proc)"
supply tl_drop_1[simp]
apply (cinit' lift: cap_' length___unsigned_long_' buffer_' call_'
simp: decodeSetFlags_def )
apply csymbr+
Expand Down
4 changes: 2 additions & 2 deletions proof/crefine/ARM_HYP/Arch_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -643,7 +643,7 @@ lemma decodeARMPageTableInvocation_ccorres:
(decodeARMMMUInvocation label args cptr slot cp extraCaps
>>= invocationCatch thread isBlocking isCall InvokeArchObject)
(Call decodeARMPageTableInvocation_'proc)"
supply if_cong[cong]
supply if_cong[cong] tl_drop_1[simp]
apply (clarsimp simp only: isCap_simps)
apply (cinit' lift: invLabel_' length___unsigned_long_' cte_' current_extra_caps_' cap_' buffer_'
simp: decodeARMMMUInvocation_def invocation_eq_use_types)
Expand Down Expand Up @@ -3663,7 +3663,7 @@ lemma decodeARMMMUInvocation_ccorres:
(decodeARMMMUInvocation label args cptr slot cp extraCaps
>>= invocationCatch thread isBlocking isCall InvokeArchObject)
(Call decodeARMMMUInvocation_'proc)"
supply if_cong[cong]
supply if_cong[cong] tl_drop_1[simp]
apply (cinit' lift: invLabel_' length___unsigned_long_' cte_'
current_extra_caps_' cap_' buffer_' call_')
apply csymbr
Expand Down
10 changes: 6 additions & 4 deletions proof/crefine/ARM_HYP/DetWP.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -136,20 +136,22 @@ lemma det_wp_getMRs:
apply (clarsimp simp: getMRs_def)
apply (rule det_wp_pre)
apply (wp det_mapM det_getRegister order_refl det_wp_mapM)
apply (fold word_size_bits_def)
apply (simp add: word_size)
apply (wp asUser_inv mapM_wp' getRegister_inv)
apply clarsimp
apply (simp add: wordSize_word_size pointerInUserData_def)
apply (rule conjI)
apply (simp add: pointerInUserData_def wordSize_def' word_size)
apply (erule valid_ipc_buffer_ptr'D2)
apply (simp add: pointerInUserData_def word_size_def)
apply (rule word_mult_less_mono1)
apply (erule order_le_less_trans)
apply (simp add: msgMaxLength_def max_ipc_words)
apply simp
apply (simp add: max_ipc_words)
apply (simp add: is_aligned_mult_triv2 [where n = 2, simplified] word_bits_conv)
apply (erule valid_ipc_buffer_ptr_aligned_2)
apply (simp add: wordSize_def' is_aligned_mult_triv2 [where n = 2, simplified] word_bits_conv)
apply (simp add: word_size_word_size_bits is_aligned_mult_triv2[where n = word_size_bits])
apply (erule valid_ipc_buffer_ptr_aligned_word_size_bits)
apply (simp add: word_size_word_size_bits is_aligned_mult_triv2[where n = word_size_bits])
done

end
Expand Down
3 changes: 2 additions & 1 deletion proof/crefine/ARM_HYP/Interrupt_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -504,6 +504,7 @@ lemma Arch_decodeIRQControlInvocation_ccorres:
(Arch.decodeIRQControlInvocation label args slot (map fst extraCaps)
>>= invocationCatch thread isBlocking isCall (InvokeIRQControl o ArchIRQControl))
(Call Arch_decodeIRQControlInvocation_'proc)"
supply tl_drop_1[simp]
apply (cinit' lift: invLabel_' srcSlot_' length___unsigned_long_' current_extra_caps_' buffer_')
apply (simp add: ARM_HYP_H.decodeIRQControlInvocation_def invocation_eq_use_types
del: Collect_const
Expand Down Expand Up @@ -808,7 +809,7 @@ lemma decodeIRQControlInvocation_ccorres:
(decodeIRQControlInvocation label args slot (map fst extraCaps)
>>= invocationCatch thread isBlocking isCall InvokeIRQControl)
(Call decodeIRQControlInvocation_'proc)"
supply gen_invocation_type_eq[simp]
supply gen_invocation_type_eq[simp] tl_drop_1[simp]
apply (cinit' lift: invLabel_' srcSlot_' length___unsigned_long_' current_extra_caps_' buffer_')
apply (simp add: decodeIRQControlInvocation_def invocation_eq_use_types
del: Collect_const
Expand Down
1 change: 1 addition & 0 deletions proof/crefine/ARM_HYP/Invoke_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1029,6 +1029,7 @@ lemma decodeCNodeInvocation_ccorres:
>>= invocationCatch thread isBlocking isCall InvokeCNode)
(Call decodeCNodeInvocation_'proc)"
supply if_cong[cong]
supply tl_drop_1[simp]
apply (cases "\<not>isCNodeCap cp")
apply (simp add: decodeCNodeInvocation_def
cong: conj_cong)
Expand Down
11 changes: 6 additions & 5 deletions proof/crefine/ARM_HYP/Ipc_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -187,7 +187,7 @@ crunch getSanitiseRegisterInfo

lemma empty_fail_getSanitiseRegisterInfo[wp, simp]:
"empty_fail (getSanitiseRegisterInfo t)"
by (wpsimp simp: getSanitiseRegisterInfo_def2 wp: ArchMove_C.empty_fail_archThreadGet)
by (wpsimp simp: getSanitiseRegisterInfo_def wp: ArchMove_C.empty_fail_archThreadGet)

lemma asUser_getRegister_getSanitiseRegisterInfo_comm:
"do
Expand Down Expand Up @@ -2294,7 +2294,8 @@ lemma doFaultTransfer_ccorres [corres]:
mask_def msgLengthBits_def
split: fault.split arch_fault.split)
apply (wpsimp simp: setMRs_to_setMR zipWithM_mapM split_def
wp: mapM_wp' setMR_tcbFault_obj_at hoare_drop_imps)+
wp: mapM_wp' setMR_tcbFault_obj_at)+
apply assumption
apply (clarsimp simp: obj_at'_def projectKOs)
done

Expand Down Expand Up @@ -2820,7 +2821,7 @@ lemma transferCapsLoop_ccorres:
(W ep caps')"
unfolding W_def check1_def check2_def split_def
proof (rule ccorres_gen_asm, induct caps arbitrary: n slots mi)
note if_split[split]
note if_split[split] tl_drop_1[simp]
case Nil
thus ?case
apply (simp only: transferCapsToSlots.simps)
Expand Down Expand Up @@ -3712,7 +3713,7 @@ lemma replyFromKernel_error_ccorres [corres]:
apply wp
apply (simp add: Collect_const_mem)
apply (vcg exspec=setMRs_syscall_error_modifies)
apply (wp hoare_case_option_wp)
apply (wp hoare_case_option_wp asUser_valid_ipc_buffer_ptr')
apply (vcg exspec=setRegister_modifies)
apply simp
apply (wp lookupIPCBuffer_aligned_option_to_0)
Expand Down Expand Up @@ -3809,7 +3810,7 @@ lemma Arch_getSanitiseRegisterInfo_ccorres:
(UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr r}) hs
(getSanitiseRegisterInfo r)
(Call Arch_getSanitiseRegisterInfo_'proc)"
apply (cinit' lift: thread_' simp: getSanitiseRegisterInfo_def2)
apply (cinit' lift: thread_' simp: getSanitiseRegisterInfo_def[folded archThreadGet_def])
apply (rule ccorres_move_c_guard_tcb)
apply (rule ccorres_pre_archThreadGet)
apply (rule_tac P="\<lambda>s. v \<noteq> Some 0" in ccorres_cross_over_guard)
Expand Down
1 change: 1 addition & 0 deletions proof/crefine/ARM_HYP/Tcb_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4602,6 +4602,7 @@ lemma decodeSetFlags_ccorres:
(decodeSetFlags args cp
>>= invocationCatch thread isBlocking isCall InvokeTCB)
(Call decodeSetFlags_'proc)"
supply tl_drop_1[simp]
apply (cinit' lift: cap_' length___unsigned_long_' buffer_' call_'
simp: decodeSetFlags_def )
apply csymbr+
Expand Down
4 changes: 2 additions & 2 deletions proof/crefine/RISCV64/Arch_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -765,7 +765,7 @@ lemma decodeRISCVPageTableInvocation_ccorres:
>>= invocationCatch thread isBlocking isCall InvokeArchObject)
(Call decodeRISCVPageTableInvocation_'proc)"
(is "_ \<Longrightarrow> _ \<Longrightarrow> ccorres _ _ ?pre ?pre' _ _ _")
supply Collect_const[simp del] if_cong[cong] option.case_cong[cong]
supply Collect_const[simp del] if_cong[cong] option.case_cong[cong] tl_drop_1[simp]
apply (clarsimp simp only: isCap_simps)
apply (cinit' lift: label___unsigned_long_' length___unsigned_long_' cte_'
current_extra_caps_' cap_' buffer_'
Expand Down Expand Up @@ -2288,7 +2288,7 @@ lemma decodeRISCVMMUInvocation_ccorres:
(decodeRISCVMMUInvocation label args cptr slot cp extraCaps
>>= invocationCatch thread isBlocking isCall InvokeArchObject)
(Call decodeRISCVMMUInvocation_'proc)"
supply ccorres_prog_only_cong[cong]
supply ccorres_prog_only_cong[cong] tl_drop_1[simp]
apply (cinit' lift: label___unsigned_long_' length___unsigned_long_' cte_'
current_extra_caps_' cap_' buffer_' call_')
apply csymbr
Expand Down
4 changes: 2 additions & 2 deletions proof/crefine/RISCV64/Interrupt_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -495,7 +495,7 @@ lemma Arch_decodeIRQControlInvocation_ccorres:
(Arch.decodeIRQControlInvocation label args srcSlot (map fst extraCaps)
>>= invocationCatch thread isBlocking isCall (InvokeIRQControl o ArchIRQControl))
(Call Arch_decodeIRQControlInvocation_'proc)"
supply maxIRQ_casts[simp]
supply maxIRQ_casts[simp] tl_drop_1[simp]
supply gen_invocation_type_eq[simp] if_cong[cong] Collect_const[simp del]
apply (cinit' lift: invLabel_' length___unsigned_long_' srcSlot_' current_extra_caps_' buffer_'
simp: ArchInterrupt_H.RISCV64_H.decodeIRQControlInvocation_def)
Expand Down Expand Up @@ -670,7 +670,7 @@ lemma decodeIRQControlInvocation_ccorres:
>>= invocationCatch thread isBlocking isCall InvokeIRQControl)
(Call decodeIRQControlInvocation_'proc)"
supply gen_invocation_type_eq[simp] if_cong[cong] Collect_const[simp del]
supply maxIRQ_casts[simp]
supply maxIRQ_casts[simp] tl_drop_1[simp]
apply (cinit' lift: invLabel_' srcSlot_' length___unsigned_long_' current_extra_caps_' buffer_')
apply (simp add: decodeIRQControlInvocation_def invocation_eq_use_types
cong: StateSpace.state.fold_congs globals.fold_congs)
Expand Down
1 change: 1 addition & 0 deletions proof/crefine/RISCV64/Invoke_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -998,6 +998,7 @@ lemma decodeCNodeInvocation_ccorres:
>>= invocationCatch thread isBlocking isCall InvokeCNode)
(Call decodeCNodeInvocation_'proc)"
supply if_cong[cong]
supply tl_drop_1[simp]
apply (cases "\<not>isCNodeCap cp")
apply (simp add: decodeCNodeInvocation_def
cong: conj_cong)
Expand Down
Loading
Loading