diff --git a/proof/crefine/ARM/Interrupt_C.thy b/proof/crefine/ARM/Interrupt_C.thy index 036b34cd8..ba0316ecb 100644 --- a/proof/crefine/ARM/Interrupt_C.thy +++ b/proof/crefine/ARM/Interrupt_C.thy @@ -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 \ ccorres (intr_and_se_rel \ 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 \ invocation_label.IRQIssueIRQHandler \ - (case x of invocation_label.IRQIssueIRQHandler \ f | _ \ g) = g" - by (clarsimp split: invocation_label.splits) +lemma decodeIRQ_arch_helper: "x \ IRQIssueIRQHandler \ + (case x of IRQIssueIRQHandler \ f | _ \ g) = g" + by (clarsimp split: gen_invocation_labels.splits) lemma decodeIRQ_arch_helper': "x \ ArchInvocationLabel ARMIRQIssueIRQHandler \ (case x of ArchInvocationLabel ARMIRQIssueIRQHandler \ f | _ \ 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 diff --git a/proof/crefine/ARM/Invoke_C.thy b/proof/crefine/ARM/Invoke_C.thy index d1aa207f8..182f82051 100644 --- a/proof/crefine/ARM/Invoke_C.thy +++ b/proof/crefine/ARM/Invoke_C.thy @@ -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: \ 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 \ scast Kernel_C.CNodeSaveCaller < label) - = (invocation_type label \ set [CNodeRevoke .e. CNodeSaveCaller])" + = (gen_invocation_type label \ set [CNodeRevoke .e. CNodeSaveCaller])" "(scast Kernel_C.CNodeCopy \ label \ label \ scast Kernel_C.CNodeMutate) - = (invocation_type label \ set [CNodeCopy .e. CNodeMutate])" - apply (simp_all add: upto_enum_def fromEnum_def enum_invocation_label + = (gen_invocation_type label \ 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 \ S | CNodeSaveCaller \ T | _ \ 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 \ ccorres (intr_and_se_rel \ 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) \ \CNodeMint case\ - 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=\ and P'=UNIV]) @@ -899,7 +900,7 @@ lemma decodeCNodeInvocation_ccorres: apply (rule ccorres_Cond_rhs_Seq) \ \CNodeMutate case\ 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=\ 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=\ 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 \ ccorres (intr_and_se_rel \ dc) (liftxf errstate id (K ()) ret__unsigned_long_') (invs' and (\s. ksCurThread s = thread) diff --git a/proof/crefine/ARM/SyscallArgs_C.thy b/proof/crefine/ARM/SyscallArgs_C.thy index 30cc8ec5f..95a28041f 100644 --- a/proof/crefine/ARM/SyscallArgs_C.thy +++ b/proof/crefine/ARM/SyscallArgs_C.thy @@ -1283,23 +1283,23 @@ lemma invocation_eq_use_type: "\ value \ (value' :: 32 signed word); unat (scast value' :: word32) < length (enum :: invocation_label list); (scast value' :: word32) \ 0 \ \ (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: "\ f = throwError v; ccorres_underlying sr Gamm rr xf arr axf P P' hs (throwError v) c \ diff --git a/proof/crefine/ARM/Tcb_C.thy b/proof/crefine/ARM/Tcb_C.thy index 04f80cbb1..9f22c7ece 100644 --- a/proof/crefine/ARM/Tcb_C.thy +++ b/proof/crefine/ARM/Tcb_C.thy @@ -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) diff --git a/proof/crefine/ARM_HYP/Interrupt_C.thy b/proof/crefine/ARM_HYP/Interrupt_C.thy index 66ff5f99d..35660e3e2 100644 --- a/proof/crefine/ARM_HYP/Interrupt_C.thy +++ b/proof/crefine/ARM_HYP/Interrupt_C.thy @@ -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 \ ccorres (intr_and_se_rel \ 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 \ invocation_label.IRQIssueIRQHandler \ - (case x of invocation_label.IRQIssueIRQHandler \ f | _ \ g) = g" - by (clarsimp split: invocation_label.splits) +lemma decodeIRQ_arch_helper: "x \ IRQIssueIRQHandler \ + (case x of IRQIssueIRQHandler \ f | _ \ g) = g" + by (clarsimp split: gen_invocation_labels.splits) lemma decodeIRQ_arch_helper': "x \ ArchInvocationLabel ARMIRQIssueIRQHandler \ @@ -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 diff --git a/proof/crefine/ARM_HYP/Invoke_C.thy b/proof/crefine/ARM_HYP/Invoke_C.thy index 12d2f55c3..98725cba5 100644 --- a/proof/crefine/ARM_HYP/Invoke_C.thy +++ b/proof/crefine/ARM_HYP/Invoke_C.thy @@ -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: \ 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 \ scast Kernel_C.CNodeSaveCaller < label) - = (invocation_type label \ set [CNodeRevoke .e. CNodeSaveCaller])" + = (gen_invocation_type label \ set [CNodeRevoke .e. CNodeSaveCaller])" "(scast Kernel_C.CNodeCopy \ label \ label \ scast Kernel_C.CNodeMutate) - = (invocation_type label \ set [CNodeCopy .e. CNodeMutate])" - apply (simp_all add: upto_enum_def fromEnum_def enum_invocation_label + = (gen_invocation_type label \ 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 \ S | CNodeSaveCaller \ T | _ \ 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 \ ccorres (intr_and_se_rel \ 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) \ \CNodeMint case\ - 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=\ and P'=UNIV]) @@ -923,7 +924,7 @@ lemma decodeCNodeInvocation_ccorres: apply (rule ccorres_Cond_rhs_Seq) \ \CNodeMutate case\ 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=\ 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=\ 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 \ ccorres (intr_and_se_rel \ dc) (liftxf errstate id (K ()) ret__unsigned_long_') (invs' and (\s. ksCurThread s = thread) diff --git a/proof/crefine/ARM_HYP/SyscallArgs_C.thy b/proof/crefine/ARM_HYP/SyscallArgs_C.thy index 625867f63..4d8d294e9 100644 --- a/proof/crefine/ARM_HYP/SyscallArgs_C.thy +++ b/proof/crefine/ARM_HYP/SyscallArgs_C.thy @@ -1317,23 +1317,23 @@ lemma invocation_eq_use_type: "\ value \ (value' :: 32 signed word); unat (scast value' :: word32) < length (enum :: invocation_label list); (scast value' :: word32) \ 0 \ \ (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: "\ f = throwError v; ccorres_underlying sr Gamm rr xf arr axf P P' hs (throwError v) c \ diff --git a/proof/crefine/ARM_HYP/Tcb_C.thy b/proof/crefine/ARM_HYP/Tcb_C.thy index 10b9e2456..cb267215f 100644 --- a/proof/crefine/ARM_HYP/Tcb_C.thy +++ b/proof/crefine/ARM_HYP/Tcb_C.thy @@ -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) diff --git a/proof/crefine/X64/Interrupt_C.thy b/proof/crefine/X64/Interrupt_C.thy index 3d500a918..0d58b8508 100644 --- a/proof/crefine/X64/Interrupt_C.thy +++ b/proof/crefine/X64/Interrupt_C.thy @@ -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 \ ccorres (intr_and_se_rel \ 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 \ invocation_label.IRQIssueIRQHandler \ - (case x of invocation_label.IRQIssueIRQHandler \ f | _ \ g) = g" - by (clarsimp split: invocation_label.splits) +lemma decodeIRQ_arch_helper: "x \ IRQIssueIRQHandler \ + (case x of IRQIssueIRQHandler \ f | _ \ g) = g" + by (clarsimp split: gen_invocation_labels.splits) lemma Arch_checkIRQ_ccorres: "ccorres (syscall_error_rel \ 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 diff --git a/proof/crefine/X64/Invoke_C.thy b/proof/crefine/X64/Invoke_C.thy index f67dae920..4821f6ab4 100644 --- a/proof/crefine/X64/Invoke_C.thy +++ b/proof/crefine/X64/Invoke_C.thy @@ -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: \ 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 \ scast Kernel_C.CNodeSaveCaller < label) - = (invocation_type label \ set [CNodeRevoke .e. CNodeSaveCaller])" + = (gen_invocation_type label \ set [CNodeRevoke .e. CNodeSaveCaller])" "(scast Kernel_C.CNodeCopy \ label \ label \ scast Kernel_C.CNodeMutate) - = (invocation_type label \ set [CNodeCopy .e. CNodeMutate])" - apply (simp_all add: upto_enum_def fromEnum_def enum_invocation_label + = (gen_invocation_type label \ 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 \ S | CNodeSaveCaller \ T | _ \ 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 \ ccorres (intr_and_se_rel \ 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) \ \CNodeMint case\ - 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=\ and P'=UNIV]) @@ -913,7 +914,7 @@ lemma decodeCNodeInvocation_ccorres: apply (rule ccorres_Cond_rhs_Seq) \ \CNodeMutate case\ 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=\ 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=\ 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 \ ccorres (intr_and_se_rel \ dc) (liftxf errstate id (K ()) ret__unsigned_long_') (invs' and (\s. ksCurThread s = thread) diff --git a/proof/crefine/X64/SyscallArgs_C.thy b/proof/crefine/X64/SyscallArgs_C.thy index 1bc562f0e..97f65dda8 100644 --- a/proof/crefine/X64/SyscallArgs_C.thy +++ b/proof/crefine/X64/SyscallArgs_C.thy @@ -1234,23 +1234,23 @@ lemma invocation_eq_use_type: "\ value \ (value' :: 32 signed word); unat (scast value' :: machine_word) < length (enum :: invocation_label list); (scast value' :: machine_word) \ 0 \ \ (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: "\ f = throwError v; ccorres_underlying sr Gamm rr xf arr axf P P' hs (throwError v) c \ diff --git a/proof/crefine/X64/Tcb_C.thy b/proof/crefine/X64/Tcb_C.thy index 797f802bd..f8be39915 100644 --- a/proof/crefine/X64/Tcb_C.thy +++ b/proof/crefine/X64/Tcb_C.thy @@ -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)