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

crefine: invocation label proof updates

This commit is contained in:
Gerwin Klein 2019-11-28 17:25:26 +10:30
parent 54f557f2b2
commit 430f2c525b
12 changed files with 105 additions and 93 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -133,7 +133,7 @@ lemma ntfn_case_can_send:
by (cases cap, simp_all add: isCap_simps)
lemma decodeIRQHandlerInvocation_ccorres:
notes if_cong[cong]
notes if_cong[cong] gen_invocation_type_eq[simp]
shows
"interpret_excaps extraCaps' = excaps_map extraCaps \<Longrightarrow>
ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
@ -245,7 +245,8 @@ lemma decodeIRQHandlerInvocation_ccorres:
apply (rule ccorres_return_CE, simp+)[1]
apply (wp sts_invs_minor')+
apply (rule ccorres_equals_throwError)
apply (fastforce simp: invocationCatch_def throwError_bind split: invocation_label.split)
apply (fastforce simp: invocationCatch_def throwError_bind
split: gen_invocation_labels.split)
apply (simp add: ccorres_cond_iffs cong: StateSpace.state.fold_congs globals.fold_congs)
apply (rule syscall_error_throwError_ccorres_n)
apply (simp add: syscall_error_to_H_cases)
@ -406,9 +407,9 @@ lemma maxIRQ_ucast_scast [simp]:
"ucast (scast Kernel_C.maxIRQ :: 10 word) = scast Kernel_C.maxIRQ"
by (clarsimp simp: Kernel_C.maxIRQ_def)
lemma decodeIRQ_arch_helper: "x \<noteq> invocation_label.IRQIssueIRQHandler \<Longrightarrow>
(case x of invocation_label.IRQIssueIRQHandler \<Rightarrow> f | _ \<Rightarrow> g) = g"
by (clarsimp split: invocation_label.splits)
lemma decodeIRQ_arch_helper: "x \<noteq> IRQIssueIRQHandler \<Longrightarrow>
(case x of IRQIssueIRQHandler \<Rightarrow> f | _ \<Rightarrow> g) = g"
by (clarsimp split: gen_invocation_labels.splits)
lemma decodeIRQ_arch_helper': "x \<noteq> ArchInvocationLabel ARMIRQIssueIRQHandler \<Longrightarrow>
(case x of ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> f | _ \<Rightarrow> g) = g"
@ -634,6 +635,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]
apply (cinit' lift: invLabel_' srcSlot_' length___unsigned_long_' excaps_' buffer_')
apply (simp add: decodeIRQControlInvocation_def invocation_eq_use_types
del: Collect_const

40
proof/crefine/ARM/Invoke_C.thy
View File

@ -119,6 +119,7 @@ lemma decodeDomainInvocation_ccorres:
(decodeDomainInvocation lab args extraCaps
>>= invocationCatch thread isBlocking isCall (uncurry InvokeDomain))
(Call decodeDomainInvocation_'proc)"
supply gen_invocation_type_eq[simp]
apply (cinit' lift: length___unsigned_long_' excaps_' call_' invLabel_' buffer_'
simp: decodeDomainInvocation_def list_case_If2 whenE_def)
apply (rule ccorres_Cond_rhs_Seq)
@ -499,20 +500,20 @@ lemma ccorres_subgoal_tailE:
\<Longrightarrow> ccorres rvr xf P P' hs (a >>=E b) (c ;; d)"
by simp
lemmas invocation_eq_use_types_sym = invocation_eq_use_types[TRY [symmetric]]
lemma label_in_CNodeInv_ranges:
notes invocation_eq_use_types_symm
= all_invocation_label_defs[THEN invocation_eq_use_type, symmetric, simplified,
unfolded enum_invocation_label, simplified]
shows
"(label < scast Kernel_C.CNodeRevoke \<or> scast Kernel_C.CNodeSaveCaller < label)
= (invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller])"
= (gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller])"
"(scast Kernel_C.CNodeCopy \<le> label \<and> label \<le> scast Kernel_C.CNodeMutate)
= (invocation_type label \<in> set [CNodeCopy .e. CNodeMutate])"
apply (simp_all add: upto_enum_def fromEnum_def enum_invocation_label
= (gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate])"
apply (simp_all add: upto_enum_def fromEnum_def enum_gen_invocation_labels
del: upt.simps)
apply (simp_all add: atLeastLessThanSuc)
apply (simp_all add: toEnum_def enum_invocation_label)
apply (simp_all add: invocation_eq_use_types_symm[simplified] invocation_label_defs)
apply (simp_all add: toEnum_def enum_invocation_label enum_gen_invocation_labels)
apply (simp_all flip: gen_invocation_type_eq)
apply (simp_all add: invocation_eq_use_types_sym invocation_label_defs)
apply (simp_all add: unat_arith_simps)
apply arith+
done
@ -523,7 +524,7 @@ lemma cnode_invok_case_cleanup2:
| CNodeRotate \<Rightarrow> S | CNodeSaveCaller \<Rightarrow> T | _ \<Rightarrow> U) = U"
apply (rule cnode_invok_case_cleanup)
apply (simp add: upto_enum_def fromEnum_def toEnum_def
enum_invocation_label)
enum_invocation_label enum_gen_invocation_labels)
apply auto
done
@ -561,6 +562,7 @@ lemma ctes_of_valid_strengthen:
done
lemma decodeCNodeInvocation_ccorres:
notes gen_invocation_type_eq[simp]
shows
"interpret_excaps extraCaps' = excaps_map extraCaps \<Longrightarrow>
ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
@ -596,7 +598,7 @@ lemma decodeCNodeInvocation_ccorres:
simp del: Collect_const
cong: call_ignore_cong globals.fold_congs
StateSpace.state.fold_congs bool.case_cong
cong del: invocation_label.case_cong_weak)
cong del: invocation_label.case_cong_weak gen_invocation_labels.case_cong_weak)
apply (rule ccorres_Cond_rhs_Seq)
apply (simp add: unlessE_def throwError_bind invocationCatch_def)
apply (rule syscall_error_throwError_ccorres_n)
@ -783,8 +785,7 @@ lemma decodeCNodeInvocation_ccorres:
apply (vcg exspec=getSyscallArg_modifies)
apply (rule ccorres_Cond_rhs_Seq)
\<comment> \<open>CNodeMint case\<close>
apply (simp add: Collect_const[symmetric]
del: Collect_const)
apply (simp flip: Collect_const)
apply (rule ccorres_rhs_assoc)+
apply (rule ccorres_Cond_rhs_Seq)
apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV])
@ -899,7 +900,7 @@ lemma decodeCNodeInvocation_ccorres:
apply (rule ccorres_Cond_rhs_Seq)
\<comment> \<open>CNodeMutate case\<close>
apply (rule ccorres_rhs_assoc)+
apply (simp add: Collect_const[symmetric] del: Collect_const
apply (simp add: flip: Collect_const
cong: call_ignore_cong)
apply (rule ccorres_Cond_rhs_Seq)
apply (simp add: injection_handler_throwError dc_def[symmetric] if_P)
@ -947,7 +948,7 @@ lemma decodeCNodeInvocation_ccorres:
apply simp
apply (rule ccorres_inst[where P=\<top> and P'=UNIV])
apply (simp add: upto_enum_def fromEnum_def toEnum_def
enum_invocation_label)
enum_gen_invocation_labels)
apply (wp getCTE_wp')
apply (simp add: Collect_const_mem)
apply vcg
@ -1345,7 +1346,7 @@ lemma decodeCNodeInvocation_ccorres:
apply (vcg exspec=getSyscallArg_modifies)
apply (rule ccorres_inst[where P=\<top> and P'=UNIV])
apply (simp add: upto_enum_def fromEnum_def toEnum_def
enum_invocation_label)
enum_gen_invocation_labels)
apply (rule ccorres_split_throws)
apply (simp add: ccorres_cond_iffs)
apply (rule ccorres_return_C_errorE, simp+)[1]
@ -2685,9 +2686,10 @@ lemma Arch_isFrameType_spec:
lemma decodeUntypedInvocation_ccorres_helper:
notes TripleSuc[simp] untypedBits_defs[simp]
notes valid_untyped_inv_wcap'.simps[simp del] tl_drop_1[simp]
shows
notes TripleSuc[simp] untypedBits_defs[simp]
notes valid_untyped_inv_wcap'.simps[simp del] tl_drop_1[simp]
notes gen_invocation_type_eq[simp]
shows
"interpret_excaps extraCaps' = excaps_map extraCaps \<Longrightarrow>
ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
(invs' and (\<lambda>s. ksCurThread s = thread)

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

@ -1283,23 +1283,23 @@ lemma invocation_eq_use_type:
"\<lbrakk> value \<equiv> (value' :: 32 signed word);
unat (scast value' :: word32) < length (enum :: invocation_label list); (scast value' :: word32) \<noteq> 0 \<rbrakk>
\<Longrightarrow> (label = (scast value)) = (invocation_type label = enum ! unat (scast value' :: word32))"
apply (fold invocation_type_eq, unfold invocationType_def)
apply (fold invocationType_eq, unfold invocationType_def)
apply (simp add: maxBound_is_length Let_def toEnum_def
nth_eq_iff_index_eq nat_le_Suc_less_imp
split: if_split)
apply (intro impI conjI)
apply (simp add: enum_invocation_label)
apply (subgoal_tac "InvalidInvocation = enum ! 0")
apply (subgoal_tac "GenInvocationLabel InvalidInvocation = enum ! 0")
apply (erule ssubst, subst nth_eq_iff_index_eq, simp+)
apply (clarsimp simp add: unat_eq_0)
apply (simp add: enum_invocation_label)
apply (simp add: enum_invocation_label enum_gen_invocation_labels)
done
lemmas all_invocation_label_defs = invocation_label_defs arch_invocation_label_defs sel4_arch_invocation_label_defs
lemmas invocation_eq_use_types
= all_invocation_label_defs[THEN invocation_eq_use_type, simplified,
unfolded enum_invocation_label enum_arch_invocation_label, simplified]
unfolded enum_invocation_label enum_gen_invocation_labels enum_arch_invocation_label, simplified]
lemma ccorres_equals_throwError:
"\<lbrakk> f = throwError v; ccorres_underlying sr Gamm rr xf arr axf P P' hs (throwError v) c \<rbrakk>

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

@ -4508,7 +4508,7 @@ lemma decodeTCBInvocation_ccorres:
>>= invocationCatch thread isBlocking isCall InvokeTCB)
(Call decodeTCBInvocation_'proc)"
apply (cinit' lift: invLabel_' cap_' length___unsigned_long_' slot_' excaps_' call_' buffer_')
apply (simp add: decodeTCBInvocation_def invocation_eq_use_types
apply (simp add: decodeTCBInvocation_def invocation_eq_use_types gen_invocation_type_eq
del: Collect_const)
apply (rule ccorres_Cond_rhs)
apply simp
@ -4607,14 +4607,14 @@ lemma decodeTCBInvocation_ccorres:
apply (rule ccorres_return_C_errorE, simp+)[1]
apply wp
apply (rule ccorres_Cond_rhs)
apply simp
apply (simp add: gen_invocation_type_eq)
apply (rule ccorres_add_returnOk, ctac(no_vcg) add: decodeSetTLSBase_ccorres)
apply (rule ccorres_return_CE, simp+)[1]
apply (rule ccorres_return_C_errorE, simp+)[1]
apply wp
apply (rule ccorres_equals_throwError)
apply (fastforce simp: throwError_bind invocationCatch_def
split: invocation_label.split)
split: invocation_label.split gen_invocation_labels.split)
apply (simp add: ccorres_cond_iffs
cong: StateSpace.state.fold_congs globals.fold_congs)
apply (rule syscall_error_throwError_ccorres_n)

12
proof/crefine/ARM_HYP/Interrupt_C.thy
View File

@ -138,7 +138,7 @@ lemma list_length_geq_helper[simp]:
by (frule length_ineq_not_Nil(3), simp, metis list.exhaust)
lemma decodeIRQHandlerInvocation_ccorres:
notes if_cong[cong]
notes if_cong[cong] gen_invocation_type_eq[simp]
shows
"interpret_excaps extraCaps' = excaps_map extraCaps \<Longrightarrow>
ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
@ -250,7 +250,8 @@ lemma decodeIRQHandlerInvocation_ccorres:
apply (rule ccorres_return_CE, simp+)[1]
apply (wp sts_invs_minor')+
apply (rule ccorres_equals_throwError)
apply (fastforce simp: invocationCatch_def throwError_bind split: invocation_label.split)
apply (fastforce simp: invocationCatch_def throwError_bind
split: gen_invocation_labels.split)
apply (simp add: ccorres_cond_iffs cong: StateSpace.state.fold_congs globals.fold_congs)
apply (rule syscall_error_throwError_ccorres_n)
apply (simp add: syscall_error_to_H_cases)
@ -424,9 +425,9 @@ lemma maxIRQ_ucast_scast [simp]:
"ucast (scast Kernel_C.maxIRQ :: 10 word) = scast Kernel_C.maxIRQ"
by (clarsimp simp: Kernel_C.maxIRQ_def)
lemma decodeIRQ_arch_helper: "x \<noteq> invocation_label.IRQIssueIRQHandler \<Longrightarrow>
(case x of invocation_label.IRQIssueIRQHandler \<Rightarrow> f | _ \<Rightarrow> g) = g"
by (clarsimp split: invocation_label.splits)
lemma decodeIRQ_arch_helper: "x \<noteq> IRQIssueIRQHandler \<Longrightarrow>
(case x of IRQIssueIRQHandler \<Rightarrow> f | _ \<Rightarrow> g) = g"
by (clarsimp split: gen_invocation_labels.splits)
lemma decodeIRQ_arch_helper': "x \<noteq> ArchInvocationLabel ARMIRQIssueIRQHandler \<Longrightarrow>
@ -655,6 +656,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]
apply (cinit' lift: invLabel_' srcSlot_' length___unsigned_long_' excaps_' buffer_')
apply (simp add: decodeIRQControlInvocation_def invocation_eq_use_types
del: Collect_const

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

@ -119,6 +119,7 @@ lemma decodeDomainInvocation_ccorres:
(decodeDomainInvocation lab args extraCaps
>>= invocationCatch thread isBlocking isCall (uncurry InvokeDomain))
(Call decodeDomainInvocation_'proc)"
supply gen_invocation_type_eq[simp]
apply (cinit' lift: length___unsigned_long_' excaps_' call_' invLabel_' buffer_'
simp: decodeDomainInvocation_def list_case_If2 whenE_def)
apply (rule ccorres_Cond_rhs_Seq)
@ -518,20 +519,20 @@ lemma ccorres_subgoal_tailE:
\<Longrightarrow> ccorres rvr xf P P' hs (a >>=E b) (c ;; d)"
by simp
lemmas invocation_eq_use_types_sym = invocation_eq_use_types[TRY [symmetric]]
lemma label_in_CNodeInv_ranges:
notes invocation_eq_use_types_symm
= all_invocation_label_defs[THEN invocation_eq_use_type, symmetric, simplified,
unfolded enum_invocation_label, simplified]
shows
"(label < scast Kernel_C.CNodeRevoke \<or> scast Kernel_C.CNodeSaveCaller < label)
= (invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller])"
= (gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller])"
"(scast Kernel_C.CNodeCopy \<le> label \<and> label \<le> scast Kernel_C.CNodeMutate)
= (invocation_type label \<in> set [CNodeCopy .e. CNodeMutate])"
apply (simp_all add: upto_enum_def fromEnum_def enum_invocation_label
= (gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate])"
apply (simp_all add: upto_enum_def fromEnum_def enum_gen_invocation_labels
del: upt.simps)
apply (simp_all add: atLeastLessThanSuc)
apply (simp_all add: toEnum_def enum_invocation_label)
apply (simp_all add: invocation_eq_use_types_symm[simplified] invocation_label_defs)
apply (simp_all add: toEnum_def enum_invocation_label enum_gen_invocation_labels)
apply (simp_all flip: gen_invocation_type_eq)
apply (simp_all add: invocation_eq_use_types_sym invocation_label_defs)
apply (simp_all add: unat_arith_simps)
apply arith+
done
@ -542,7 +543,7 @@ lemma cnode_invok_case_cleanup2:
| CNodeRotate \<Rightarrow> S | CNodeSaveCaller \<Rightarrow> T | _ \<Rightarrow> U) = U"
apply (rule cnode_invok_case_cleanup)
apply (simp add: upto_enum_def fromEnum_def toEnum_def
enum_invocation_label)
enum_invocation_label enum_gen_invocation_labels)
apply auto
done
@ -585,6 +586,7 @@ lemma hoare_vcg_imp_lift_R:
by (auto simp add: valid_def validE_R_def validE_def split_def split: sum.splits)
lemma decodeCNodeInvocation_ccorres:
notes gen_invocation_type_eq[simp]
shows
"interpret_excaps extraCaps' = excaps_map extraCaps \<Longrightarrow>
ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
@ -620,7 +622,7 @@ lemma decodeCNodeInvocation_ccorres:
simp del: Collect_const
cong: call_ignore_cong globals.fold_congs
StateSpace.state.fold_congs bool.case_cong
cong del: invocation_label.case_cong_weak)
cong del: invocation_label.case_cong_weak gen_invocation_labels.case_cong_weak)
apply (rule ccorres_Cond_rhs_Seq)
apply (simp add: unlessE_def throwError_bind invocationCatch_def)
apply (rule syscall_error_throwError_ccorres_n)
@ -807,8 +809,7 @@ lemma decodeCNodeInvocation_ccorres:
apply (vcg exspec=getSyscallArg_modifies)
apply (rule ccorres_Cond_rhs_Seq)
\<comment> \<open>CNodeMint case\<close>
apply (simp add: Collect_const[symmetric]
del: Collect_const)
apply (simp flip: Collect_const)
apply (rule ccorres_rhs_assoc)+
apply (rule ccorres_Cond_rhs_Seq)
apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV])
@ -923,7 +924,7 @@ lemma decodeCNodeInvocation_ccorres:
apply (rule ccorres_Cond_rhs_Seq)
\<comment> \<open>CNodeMutate case\<close>
apply (rule ccorres_rhs_assoc)+
apply (simp add: Collect_const[symmetric] del: Collect_const
apply (simp add: flip: Collect_const
cong: call_ignore_cong)
apply (rule ccorres_Cond_rhs_Seq)
apply (simp add: injection_handler_throwError dc_def[symmetric] if_P)
@ -971,7 +972,7 @@ lemma decodeCNodeInvocation_ccorres:
apply simp
apply (rule ccorres_inst[where P=\<top> and P'=UNIV])
apply (simp add: upto_enum_def fromEnum_def toEnum_def
enum_invocation_label)
enum_gen_invocation_labels)
apply (wp getCTE_wp')
apply (simp add: Collect_const_mem)
apply vcg
@ -1369,7 +1370,7 @@ lemma decodeCNodeInvocation_ccorres:
apply (vcg exspec=getSyscallArg_modifies)
apply (rule ccorres_inst[where P=\<top> and P'=UNIV])
apply (simp add: upto_enum_def fromEnum_def toEnum_def
enum_invocation_label)
enum_gen_invocation_labels)
apply (rule ccorres_split_throws)
apply (simp add: ccorres_cond_iffs)
apply (rule ccorres_return_C_errorE, simp+)[1]
@ -2902,9 +2903,10 @@ lemma Arch_isFrameType_spec:
lemma decodeUntypedInvocation_ccorres_helper:
notes TripleSuc[simp] untypedBits_defs[simp]
notes valid_untyped_inv_wcap'.simps[simp del] tl_drop_1[simp]
shows
notes TripleSuc[simp] untypedBits_defs[simp]
notes valid_untyped_inv_wcap'.simps[simp del] tl_drop_1[simp]
notes gen_invocation_type_eq[simp]
shows
"interpret_excaps extraCaps' = excaps_map extraCaps \<Longrightarrow>
ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
(invs' and (\<lambda>s. ksCurThread s = thread)

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

@ -1317,23 +1317,23 @@ lemma invocation_eq_use_type:
"\<lbrakk> value \<equiv> (value' :: 32 signed word);
unat (scast value' :: word32) < length (enum :: invocation_label list); (scast value' :: word32) \<noteq> 0 \<rbrakk>
\<Longrightarrow> (label = (scast value)) = (invocation_type label = enum ! unat (scast value' :: word32))"
apply (fold invocation_type_eq, unfold invocationType_def)
apply (fold invocationType_eq, unfold invocationType_def)
apply (simp add: maxBound_is_length Let_def toEnum_def
nth_eq_iff_index_eq nat_le_Suc_less_imp
split: if_split)
apply (intro impI conjI)
apply (simp add: enum_invocation_label)
apply (subgoal_tac "InvalidInvocation = enum ! 0")
apply (subgoal_tac "GenInvocationLabel InvalidInvocation = enum ! 0")
apply (erule ssubst, subst nth_eq_iff_index_eq, simp+)
apply (clarsimp simp add: unat_eq_0)
apply (simp add: enum_invocation_label)
apply (simp add: enum_invocation_label enum_gen_invocation_labels)
done
lemmas all_invocation_label_defs = invocation_label_defs arch_invocation_label_defs sel4_arch_invocation_label_defs
lemmas invocation_eq_use_types
= all_invocation_label_defs[THEN invocation_eq_use_type, simplified,
unfolded enum_invocation_label enum_arch_invocation_label, simplified]
unfolded enum_invocation_label enum_gen_invocation_labels enum_arch_invocation_label, simplified]
lemma ccorres_equals_throwError:
"\<lbrakk> f = throwError v; ccorres_underlying sr Gamm rr xf arr axf P P' hs (throwError v) c \<rbrakk>

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

@ -4607,7 +4607,7 @@ lemma decodeTCBInvocation_ccorres:
>>= invocationCatch thread isBlocking isCall InvokeTCB)
(Call decodeTCBInvocation_'proc)"
apply (cinit' lift: invLabel_' cap_' length___unsigned_long_' slot_' excaps_' call_' buffer_')
apply (simp add: decodeTCBInvocation_def invocation_eq_use_types
apply (simp add: decodeTCBInvocation_def invocation_eq_use_types gen_invocation_type_eq
del: Collect_const)
apply (rule ccorres_Cond_rhs)
apply simp
@ -4706,14 +4706,14 @@ lemma decodeTCBInvocation_ccorres:
apply (rule ccorres_return_C_errorE, simp+)[1]
apply wp
apply (rule ccorres_Cond_rhs)
apply simp
apply (simp add: gen_invocation_type_eq)
apply (rule ccorres_add_returnOk, ctac(no_vcg) add: decodeSetTLSBase_ccorres)
apply (rule ccorres_return_CE, simp+)[1]
apply (rule ccorres_return_C_errorE, simp+)[1]
apply wp
apply (rule ccorres_equals_throwError)
apply (fastforce simp: throwError_bind invocationCatch_def
split: invocation_label.split)
split: invocation_label.split gen_invocation_labels.split)
apply (simp add: ccorres_cond_iffs
cong: StateSpace.state.fold_congs globals.fold_congs)
apply (rule syscall_error_throwError_ccorres_n)

12
proof/crefine/X64/Interrupt_C.thy
View File

@ -138,7 +138,7 @@ lemma list_length_geq_helper[simp]:
by (frule length_ineq_not_Nil(3), simp, metis list.exhaust)
lemma decodeIRQHandlerInvocation_ccorres:
notes if_cong[cong]
notes if_cong[cong] gen_invocation_type_eq[simp]
shows
"interpret_excaps extraCaps' = excaps_map extraCaps \<Longrightarrow>
ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
@ -250,7 +250,8 @@ lemma decodeIRQHandlerInvocation_ccorres:
apply (rule ccorres_return_CE, simp+)[1]
apply (wp sts_invs_minor')+
apply (rule ccorres_equals_throwError)
apply (fastforce simp: invocationCatch_def throwError_bind split: invocation_label.split)
apply (fastforce simp: invocationCatch_def throwError_bind
split: gen_invocation_labels.split)
apply (simp add: ccorres_cond_iffs cong: StateSpace.state.fold_congs globals.fold_congs)
apply (rule syscall_error_throwError_ccorres_n)
apply (simp add: syscall_error_to_H_cases)
@ -949,9 +950,9 @@ lemma maxIRQ_ucast_scast [simp]:
"ucast (scast Kernel_C.maxIRQ :: 8 word) = scast Kernel_C.maxIRQ"
by (clarsimp simp: Kernel_C.maxIRQ_def)
lemma decodeIRQ_arch_helper: "x \<noteq> invocation_label.IRQIssueIRQHandler \<Longrightarrow>
(case x of invocation_label.IRQIssueIRQHandler \<Rightarrow> f | _ \<Rightarrow> g) = g"
by (clarsimp split: invocation_label.splits)
lemma decodeIRQ_arch_helper: "x \<noteq> IRQIssueIRQHandler \<Longrightarrow>
(case x of IRQIssueIRQHandler \<Rightarrow> f | _ \<Rightarrow> g) = g"
by (clarsimp split: gen_invocation_labels.splits)
lemma Arch_checkIRQ_ccorres:
"ccorres (syscall_error_rel \<currency> dc) (liftxf errstate id undefined ret__unsigned_long_')
@ -995,6 +996,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]
apply (cinit' lift: invLabel_' srcSlot_' length___unsigned_long_' excaps_' buffer_')
apply (simp add: decodeIRQControlInvocation_def invocation_eq_use_types
del: Collect_const

40
proof/crefine/X64/Invoke_C.thy
View File

@ -119,6 +119,7 @@ lemma decodeDomainInvocation_ccorres:
(decodeDomainInvocation lab args extraCaps
>>= invocationCatch thread isBlocking isCall (uncurry InvokeDomain))
(Call decodeDomainInvocation_'proc)"
supply gen_invocation_type_eq[simp]
apply (cinit' lift: length___unsigned_long_' excaps_' call_' invLabel_' buffer_'
simp: decodeDomainInvocation_def list_case_If2 whenE_def)
apply (rule ccorres_Cond_rhs_Seq)
@ -508,20 +509,20 @@ lemma ccorres_subgoal_tailE:
\<Longrightarrow> ccorres rvr xf P P' hs (a >>=E b) (c ;; d)"
by simp
lemmas invocation_eq_use_types_sym = invocation_eq_use_types[TRY [symmetric]]
lemma label_in_CNodeInv_ranges:
notes invocation_eq_use_types_symm
= all_invocation_label_defs[THEN invocation_eq_use_type, symmetric, simplified,
unfolded enum_invocation_label, simplified]
shows
"(label < scast Kernel_C.CNodeRevoke \<or> scast Kernel_C.CNodeSaveCaller < label)
= (invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller])"
= (gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller])"
"(scast Kernel_C.CNodeCopy \<le> label \<and> label \<le> scast Kernel_C.CNodeMutate)
= (invocation_type label \<in> set [CNodeCopy .e. CNodeMutate])"
apply (simp_all add: upto_enum_def fromEnum_def enum_invocation_label
= (gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate])"
apply (simp_all add: upto_enum_def fromEnum_def enum_gen_invocation_labels
del: upt.simps)
apply (simp_all add: atLeastLessThanSuc)
apply (simp_all add: toEnum_def enum_invocation_label)
apply (simp_all add: invocation_eq_use_types_symm[simplified] invocation_label_defs)
apply (simp_all add: toEnum_def enum_invocation_label enum_gen_invocation_labels)
apply (simp_all flip: gen_invocation_type_eq)
apply (simp_all add: invocation_eq_use_types_sym invocation_label_defs)
apply (simp_all add: unat_arith_simps)
apply arith+
done
@ -532,7 +533,7 @@ lemma cnode_invok_case_cleanup2:
| CNodeRotate \<Rightarrow> S | CNodeSaveCaller \<Rightarrow> T | _ \<Rightarrow> U) = U"
apply (rule cnode_invok_case_cleanup)
apply (simp add: upto_enum_def fromEnum_def toEnum_def
enum_invocation_label)
enum_invocation_label enum_gen_invocation_labels)
apply auto
done
@ -575,6 +576,7 @@ lemma hoare_vcg_imp_lift_R:
by (auto simp add: valid_def validE_R_def validE_def split_def split: sum.splits)
lemma decodeCNodeInvocation_ccorres:
notes gen_invocation_type_eq[simp]
shows
"interpret_excaps extraCaps' = excaps_map extraCaps \<Longrightarrow>
ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
@ -610,7 +612,7 @@ lemma decodeCNodeInvocation_ccorres:
simp del: Collect_const
cong: call_ignore_cong globals.fold_congs
StateSpace.state.fold_congs bool.case_cong
cong del: invocation_label.case_cong_weak)
cong del: invocation_label.case_cong_weak gen_invocation_labels.case_cong_weak)
apply (rule ccorres_Cond_rhs_Seq)
apply (simp add: unlessE_def throwError_bind invocationCatch_def)
apply (rule syscall_error_throwError_ccorres_n)
@ -797,8 +799,7 @@ lemma decodeCNodeInvocation_ccorres:
apply (vcg exspec=getSyscallArg_modifies)
apply (rule ccorres_Cond_rhs_Seq)
\<comment> \<open>CNodeMint case\<close>
apply (simp add: Collect_const[symmetric]
del: Collect_const)
apply (simp flip: Collect_const)
apply (rule ccorres_rhs_assoc)+
apply (rule ccorres_Cond_rhs_Seq)
apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV])
@ -913,7 +914,7 @@ lemma decodeCNodeInvocation_ccorres:
apply (rule ccorres_Cond_rhs_Seq)
\<comment> \<open>CNodeMutate case\<close>
apply (rule ccorres_rhs_assoc)+
apply (simp add: Collect_const[symmetric] del: Collect_const
apply (simp add: flip: Collect_const
cong: call_ignore_cong)
apply (rule ccorres_Cond_rhs_Seq)
apply (simp add: injection_handler_throwError dc_def[symmetric] if_P)
@ -961,7 +962,7 @@ lemma decodeCNodeInvocation_ccorres:
apply simp
apply (rule ccorres_inst[where P=\<top> and P'=UNIV])
apply (simp add: upto_enum_def fromEnum_def toEnum_def
enum_invocation_label)
enum_gen_invocation_labels)
apply (wp getCTE_wp')
apply (simp add: Collect_const_mem)
apply vcg
@ -1359,7 +1360,7 @@ lemma decodeCNodeInvocation_ccorres:
apply (vcg exspec=getSyscallArg_modifies)
apply (rule ccorres_inst[where P=\<top> and P'=UNIV])
apply (simp add: upto_enum_def fromEnum_def toEnum_def
enum_invocation_label)
enum_gen_invocation_labels)
apply (rule ccorres_split_throws)
apply (simp add: ccorres_cond_iffs)
apply (rule ccorres_return_C_errorE, simp+)[1]
@ -2918,9 +2919,10 @@ lemma Arch_isFrameType_spec:
lemma decodeUntypedInvocation_ccorres_helper:
notes TripleSuc[simp]
notes valid_untyped_inv_wcap'.simps[simp del] tl_drop_1[simp]
shows
notes TripleSuc[simp]
notes valid_untyped_inv_wcap'.simps[simp del] tl_drop_1[simp]
notes gen_invocation_type_eq[simp]
shows
"interpret_excaps extraCaps' = excaps_map extraCaps \<Longrightarrow>
ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
(invs' and (\<lambda>s. ksCurThread s = thread)

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

@ -1234,23 +1234,23 @@ lemma invocation_eq_use_type:
"\<lbrakk> value \<equiv> (value' :: 32 signed word);
unat (scast value' :: machine_word) < length (enum :: invocation_label list); (scast value' :: machine_word) \<noteq> 0 \<rbrakk>
\<Longrightarrow> (label = (scast value)) = (invocation_type label = enum ! unat (scast value' :: machine_word))"
apply (fold invocation_type_eq, unfold invocationType_def)
apply (fold invocationType_eq, unfold invocationType_def)
apply (simp add: maxBound_is_length Let_def toEnum_def
nth_eq_iff_index_eq nat_le_Suc_less_imp
split: if_split)
apply (intro impI conjI)
apply (simp add: enum_invocation_label)
apply (subgoal_tac "InvalidInvocation = enum ! 0")
apply (subgoal_tac "GenInvocationLabel InvalidInvocation = enum ! 0")
apply (erule ssubst, subst nth_eq_iff_index_eq, simp+)
apply (clarsimp simp add: unat_eq_0)
apply (simp add: enum_invocation_label)
apply (simp add: enum_invocation_label enum_gen_invocation_labels)
done
lemmas all_invocation_label_defs = invocation_label_defs arch_invocation_label_defs sel4_arch_invocation_label_defs
lemmas invocation_eq_use_types
= all_invocation_label_defs[THEN invocation_eq_use_type, simplified,
unfolded enum_invocation_label enum_arch_invocation_label, simplified]
unfolded enum_invocation_label enum_gen_invocation_labels enum_arch_invocation_label, simplified]
lemma ccorres_equals_throwError:
"\<lbrakk> f = throwError v; ccorres_underlying sr Gamm rr xf arr axf P P' hs (throwError v) c \<rbrakk>

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

@ -4610,7 +4610,7 @@ lemma decodeTCBInvocation_ccorres:
>>= invocationCatch thread isBlocking isCall InvokeTCB)
(Call decodeTCBInvocation_'proc)"
apply (cinit' lift: invLabel_' cap_' length___unsigned_long_' slot_' excaps_' call_' buffer_')
apply (simp add: decodeTCBInvocation_def invocation_eq_use_types
apply (simp add: decodeTCBInvocation_def invocation_eq_use_types gen_invocation_type_eq
del: Collect_const)
apply (rule ccorres_Cond_rhs)
apply simp
@ -4709,14 +4709,14 @@ lemma decodeTCBInvocation_ccorres:
apply (rule ccorres_return_C_errorE, simp+)[1]
apply wp
apply (rule ccorres_Cond_rhs)
apply simp
apply (simp add: gen_invocation_type_eq)
apply (rule ccorres_add_returnOk, ctac(no_vcg) add: decodeSetTLSBase_ccorres)
apply (rule ccorres_return_CE, simp+)[1]
apply (rule ccorres_return_C_errorE, simp+)[1]
apply wp
apply (rule ccorres_equals_throwError)
apply (fastforce simp: throwError_bind invocationCatch_def
split: invocation_label.split)
split: invocation_label.split gen_invocation_labels.split)
apply (simp add: ccorres_cond_iffs
cong: StateSpace.state.fold_congs globals.fold_congs)
apply (rule syscall_error_throwError_ccorres_n)