diff --git a/proof/crefine/AARCH64/ADT_C.thy b/proof/crefine/AARCH64/ADT_C.thy index 8b15aefd26..289b4c474a 100644 --- a/proof/crefine/AARCH64/ADT_C.thy +++ b/proof/crefine/AARCH64/ADT_C.thy @@ -992,7 +992,7 @@ lemma cpspace_ntfn_relation_unique: by (auto simp: NtfnState_Active_def NtfnState_Idle_def NtfnState_Waiting_def typ_heap_simps cnotification_relation_def Let_def tcb_queue_rel'_clift_unique option_to_ctcb_ptr_def valid_obj'_def valid_ntfn'_def valid_bound_tcb'_def - kernel.tcb_at_not_NULL tcb_ptr_to_ctcb_ptr_inj + tcb_at_not_NULL tcb_ptr_to_ctcb_ptr_inj split: ntfn.splits option.splits) (* long *) lemma canonical_pageBits_shift_inj: diff --git a/proof/crefine/AARCH64/ArchMove_C.thy b/proof/crefine/AARCH64/ArchMove_C.thy index 0ecf13acef..5cb7d5ca0e 100644 --- a/proof/crefine/AARCH64/ArchMove_C.thy +++ b/proof/crefine/AARCH64/ArchMove_C.thy @@ -10,6 +10,9 @@ theory ArchMove_C imports Move_C begin +lemma aligned_no_overflow_less: (* FIXME AARCH64: move to Word_Lib *) + "\ is_aligned p n; p + 2 ^ n \ 0 \ \ p < p + 2 ^ n" + by (erule word_leq_minus_one_le) (erule is_aligned_no_overflow) lemma ps_clear_is_aligned_ksPSpace_None: "\ps_clear p n s; is_aligned p n; 0 mask n\ @@ -164,7 +167,7 @@ lemma more_pageBits_inner_beauty: apply (clarsimp simp: word_size pageBits_def) done -(* FIXME x64: figure out where these are needed and adjust appropriately *) +(* used in StoreWord_C *) lemma mask_pageBits_inner_beauty: "is_aligned p 3 \ (p && ~~ mask pageBits) + (ucast ((ucast (p && mask pageBits >> 3)):: 9 word) * 8) = (p::machine_word)" @@ -347,18 +350,6 @@ lemma asid_shiftr_low_bits_less[simplified]: apply simp done -lemma getActiveIRQ_neq_Some0xFF': - "\\\ getActiveIRQ in_kernel \\rv s. rv \ Some 0xFF\" - apply (simp add: getActiveIRQ_def) - apply wpsimp - done - -lemma getActiveIRQ_neq_Some0x3FF: - "\\\ doMachineOp (getActiveIRQ in_kernel) \\rv s. rv \ Some 0xFF\" - apply (wpsimp simp: doMachineOp_def split_def) - apply (auto dest: use_valid intro: getActiveIRQ_neq_Some0xFF') - done - (* We don't have access to n_msgRegisters from C here, but the number of msg registers in C should be equivalent to what we have in the abstract/design specs. We want a number for this definition that automatically updates if the number of registers changes, and we sanity check it later @@ -548,6 +539,187 @@ lemma placeNewObject_object_at_vcpu: by (rule hoare_post_imp[OF _ placeNewObject_creates_object_vcpu]) (fastforce simp: ko_at_vcpu_at'D) +lemma case_option_both[simp]: (* FIXME AARCH64: move to Lib, remove duplicates *) + "(case f of None \ P | _ \ P) = P" + by (auto split: option.splits) + +lemma if_case_opt_same_branches: (* FIXME AARCH64: move to Lib, remove duplicates *) + "cond \ Option.is_none opt \ + (if cond then case opt of None \ f | Some x \ g x else f) = f" + by (cases cond; cases opt; clarsimp) + +(* FIXME AARCH64: move these up to Refine or AInvs *) +lemma haskell_assertE_wp[wp]: + "\\s. F \ Q () s\ haskell_assertE F L \Q\,\E\" + unfolding haskell_assertE_def + by (rule assertE_wp) + +(* FIXME AARCH64: this needs to exist before VSpace_R.haskell_assertE_inv, so that the crunch there + does not make it [wp] *) +lemma haskell_assertE_inv: + "haskell_assertE F L \P\" + unfolding haskell_assertE_def + by wpsimp + +lemma cte_wp_cteCap_valid: + "\ cte_wp_at' ((=) cap \ cteCap) slot s; valid_objs' s \ \ valid_cap' cap s" + by (clarsimp simp: cte_wp_at_ctes_of ctes_of_valid') + +lemma not_VSRootPT_T_eq: + "(pt_t \ VSRootPT_T) = (pt_t = NormalPT_T)" + by (cases pt_t; simp) + +lemma unat_of_nat_pt_bits_mw: + "unat (of_nat (pt_bits pt_t)::machine_word) = pt_bits pt_t" + by (rule unat_of_nat_eq) (simp add: bit_simps split: if_split) + +lemma unat_mask_pt_bits_shift_neq_0[simp]: + "0 < unat (mask (pt_bits pt_t) >> pte_bits :: machine_word)" + by (simp add: bit_simps mask_def split: if_split) + +lemma pptrBaseOffset_alignment_pt_bits[simp, intro!]: + "pt_bits pt_t \ pptrBaseOffset_alignment" + by (simp add: bit_simps pptrBaseOffset_alignment_def split: if_split) + +lemma canonical_address_mask_shift: + "\ canonical_address p; is_aligned p m'; m \ m'; n + m = Suc canonical_bit; 0 < n \ \ + p && (mask n << m) = p" + apply (prop_tac "m = Suc canonical_bit - n", arith) + apply (simp add: canonical_address_def canonical_address_of_def canonical_bit_def) + apply word_eqI + apply (rule iffI; clarsimp) + apply (rename_tac n') + apply (prop_tac "n' < 48", fastforce) + apply fastforce + done + +schematic_goal pptrUserTop_val: + "pptrUserTop = numeral ?n" + by (simp add: pptrUserTop_def mask_def Kernel_Config.config_ARM_PA_SIZE_BITS_40_def + del: word_eq_numeral_iff_iszero) + +lemma user_region_canonical: + "p \ user_region \ canonical_address p" + apply (simp add: canonical_address_range user_region_def canonical_user_def) + apply (erule order_trans) + apply (rule mask_mono) + apply (simp add: ipa_size_def canonical_bit_def split: if_split) + done + +lemma pptrUserTop_eq_mask_ipa_size: + "pptrUserTop = mask ipa_size" + by (simp add: pptrUserTop_def ipa_size_def) + +lemma mask_pptrUserTop_user_region: + "\ is_aligned v n; v + mask n \ pptrUserTop \ \ v \ user_region" + apply (simp add: user_region_def canonical_user_def pptrUserTop_eq_mask_ipa_size + word_and_or_mask_aligned) + apply (simp flip: and_mask_eq_iff_le_mask) + apply word_eqI_solve + done + +lemma canonical_address_pptrUserTop_mask: + "\ p + 2^n - 1 \ pptrUserTop; is_aligned p n \ \ canonical_address p" + apply (rule user_region_canonical) + apply (erule mask_pptrUserTop_user_region) + apply (simp add: mask_def field_simps) + done + +lemma isVTableRoot_ex: + "isVTableRoot cap = (\p m. cap = ArchObjectCap (PageTableCap p VSRootPT_T m))" + by (simp add: isVTableRoot_def split: capability.splits arch_capability.splits pt_type.splits) + +lemma isVTableRoot_cap_eq: + "isVTableRoot cap = + (isArchObjectCap cap \ isPageTableCap (capCap cap) \ capPTType (capCap cap) = VSRootPT_T)" + by (auto simp: isCap_simps isVTableRoot_ex) + +(* FIXME AARCH64: try to make the 48 less magic *) +lemma canonical_address_and_maskD: + "canonical_address p \ p && mask 48 = p" + apply (simp add: word_and_mask_shiftl pageBits_def canonical_address_range canonical_bit_def) + apply word_eqI + apply fastforce + done + +(* FIXME AARCH64: try to make the 48 less magic *) +lemma canonical_address_and_maskI: + "p && mask 48 = p \ canonical_address p" + by (simp add: word_and_mask_shiftl pageBits_def canonical_address_range canonical_bit_def + and_mask_eq_iff_le_mask) + + +lemma addrFromPPtr_canonical_in_kernel_window: + "\ pptrBase \ p; p < pptrTop \ \ canonical_address (addrFromPPtr p)" + apply (simp add: addrFromPPtr_def pptrBaseOffset_def paddrBase_def canonical_address_mask_eq + canonical_bit_def pptrBase_def pageBits_def pptrTop_def) + by word_bitwise clarsimp + +lemma levelType_0[simp]: + "levelType 0 = NormalPT_T" + by (simp add: levelType_def maxPTLevel_def split: if_splits) + +lemma levelType_maxPTLevel[simp]: + "levelType maxPTLevel = VSRootPT_T" + by (simp add: levelType_def) + +(* FIXME AARCH64: move; could be simp *) +lemma pt_bits_minus_pte_bits: + "pt_bits pt_t - pte_bits = ptTranslationBits pt_t" + by (simp add: bit_simps) + +(* FIXME AARCH64: move; could be simp *) +lemma ptTranslationBits_plus_pte_bits: + "ptTranslationBits pt_t + pte_bits = pt_bits pt_t" + by (simp add: bit_simps) + +lemma page_table_pte_at': + "page_table_at' pt_t p s \ pte_at' p s" + apply (clarsimp simp: page_table_at'_def) + apply (erule_tac x=0 in allE) + apply simp + done + +lemma pte_at_ko': + "pte_at' p s \ \pte. ko_at' (pte::pte) p s" + apply (clarsimp simp: typ_at'_def obj_at'_def ko_wp_at'_def) + apply (case_tac ko; simp) + apply (rename_tac arch_kernel_object) + apply (case_tac arch_kernel_object, auto)[1] + done + +lemma getObject_asidpool_inv[wp]: + "\P\ getObject l \\rv :: asidpool. P\" + apply (rule getObject_inv) + apply simp + apply (rule loadObject_default_inv) + done + +lemma asid_pool_at_ko'_eq: + "(\ap :: asidpool. ko_at' ap p s) = asid_pool_at' p s" + apply (rule iffI) + apply (clarsimp simp: typ_at'_def obj_at'_def ko_wp_at'_def) + apply (clarsimp simp: typ_at'_def obj_at'_def ko_wp_at'_def) + apply (case_tac ko, auto) + apply (rename_tac arch_kernel_object) + apply (case_tac arch_kernel_object, auto)[1] + done + +lemma asid_pool_at_ko': + "asid_pool_at' p s \ \pool. ko_at' (ASIDPool pool) p s" + apply (clarsimp simp: typ_at'_def obj_at'_def ko_wp_at'_def) + apply (case_tac ko, auto) + apply (rename_tac arch_kernel_object) + apply (case_tac arch_kernel_object, auto)[1] + apply (rename_tac asidpool) + apply (case_tac asidpool, auto)[1] + done + +(* FIXME AARCH64: move; also add vmid_bits_def to relevant bit defs *) +value_type vmid_bits = "size (0::vmid)" + +(* end of move to Refine/AInvs *) + end end diff --git a/proof/crefine/AARCH64/Arch_C.thy b/proof/crefine/AARCH64/Arch_C.thy index ae1656fe87..d5ddefd69e 100644 --- a/proof/crefine/AARCH64/Arch_C.thy +++ b/proof/crefine/AARCH64/Arch_C.thy @@ -35,30 +35,6 @@ lemma objBits_InvalidPTE_pte_bits: "objBits AARCH64_H.InvalidPTE = pte_bits" by (simp add: objBits_InvalidPTE bit_simps) -lemma unat_of_nat_pt_bits_mw: (* FIXME AARCH64 move *) - "unat (of_nat (pt_bits pt_t)::machine_word) = pt_bits pt_t" - by (rule unat_of_nat_eq) (simp add: bit_simps split: if_split) - -lemma aligned_no_overflow_less: (* FIXME AARCH64: Word_Lib *) - "\ is_aligned p n; p + 2 ^ n \ 0 \ \ p < p + 2 ^ n" - by (erule word_leq_minus_one_le) (erule is_aligned_no_overflow) - -lemma unat_mask_pt_bits_shift_neq_0[simp]: (* FIXME AARCH64 move *) - "0 < unat (mask (pt_bits pt_t) >> pte_bits :: machine_word)" - by (simp add: bit_simps mask_def split: if_split) - -lemma pptrBaseOffset_alignment_pt_bits[simp, intro!]: (* FIXME AARCH64 move *) - "pt_bits pt_t \ pptrBaseOffset_alignment" - by (simp add: bit_simps pptrBaseOffset_alignment_def split: if_split) - -lemma addrFromPPtr_mask_cacheLineSize: (* FIXME AARCH64 move *) - "addrFromPPtr ptr && mask cacheLineSize = ptr && mask cacheLineSize" - apply (simp add: addrFromPPtr_def AARCH64.pptrBase_def pptrBaseOffset_def canonical_bit_def - paddrBase_def cacheLineSize_def) - apply word_bitwise - apply (simp add:mask_def) - done - lemma clearMemory_PT_setObject_PTE_ccorres: "ccorres dc xfdc (page_table_at' pt_t ptr and (\s. 2 ^ ptBits pt_t \ gsMaxObjectSize s) and @@ -509,18 +485,6 @@ lemma ucast_x3_shiftr_asid_low_bits: apply (simp add: asid_low_bits_def asid_bits_def mask_def )+ done -lemma canonical_address_mask_shift: (* FIXME AARCH64: move up *) - "\ canonical_address p; is_aligned p m'; m \ m'; n + m = Suc canonical_bit; 0 < n \ \ - p && (mask n << m) = p" - apply (prop_tac "m = Suc canonical_bit - n", arith) - apply (simp add: canonical_address_def canonical_address_of_def canonical_bit_def) - apply word_eqI - apply (rule iffI; clarsimp) - apply (rename_tac n') - apply (prop_tac "n' < 48", fastforce) - apply fastforce - done - lemma performASIDControlInvocation_ccorres: notes replicate_numeral[simp del] shows @@ -715,6 +679,7 @@ lemmas performARMMMUInvocations AARCH64_H.performInvocation_def performARMMMUInvocation_def liftE_bind_return_bindE_returnOk +(* FIXME AARCH64: consider using isVTableRoot *) lemma slotcap_in_mem_PageTable: "\ slotcap_in_mem cap slot (ctes_of s); (s, s') \ rf_sr \ \ \v. cslift s' (cte_Ptr slot) = Some v @@ -886,16 +851,6 @@ lemma slotcap_in_mem_VSpace: apply (simp add: cap_get_tag_isCap_ArchObject2) done -lemma pptrUserTop_val: (* FIXME AARCH64: need value spelled out for C code, make schematic *) - "pptrUserTop = 0xFFFFFFFFFFF" - by (simp add: pptrUserTop_def mask_def Kernel_Config.config_ARM_PA_SIZE_BITS_40_def) - -lemma ccap_relation_vspace_base: (* FIXME AARCH64: move up if needed in VSpace_R *) - "ccap_relation (ArchObjectCap (PageTableCap p VSRootPT_T m)) cap - \ capVSBasePtr_CL (cap_vspace_cap_lift cap) = p" - by (frule cap_get_tag_isCap_unfolded_H_cap) - (clarsimp simp: cap_vspace_cap_lift ccap_relation_def cap_to_H_def split: if_splits) - lemma Restart_valid[simp]: "valid_tcb_state' Restart s" by (simp add: valid_tcb_state'_def) @@ -1637,7 +1592,7 @@ lemma canonical_address_frame_at': dest!: device_data_at_ko user_data_at_ko intro!: obj_at'_is_canonical) done -definition flushtype_relation :: "flush_type \ machine_word \ bool" where (* FIXME AARCH64: move to VSpace_C *) +definition flushtype_relation :: "flush_type \ machine_word \ bool" where "flushtype_relation typ label \ case typ of Clean \ label \ scast ` {Kernel_C.ARMPageClean_Data, Kernel_C.ARMVSpaceClean_Data} @@ -1648,7 +1603,7 @@ definition flushtype_relation :: "flush_type \ machine_word \ label \ scast ` {Kernel_C.ARMPageUnify_Instruction, Kernel_C.ARMVSpaceUnify_Instruction}" -lemma doFlush_ccorres: (* FIXME AARCH64: move to VSpace_C *) +lemma doFlush_ccorres: "ccorres dc xfdc (\s. vs \ ve \ ps \ ps + (ve - vs) \ vs && mask cacheLineSize = ps && mask cacheLineSize \ ptrFromPAddr ps \ ptrFromPAddr ps + (ve - vs) \ unat (ve - vs) \ gsMaxObjectSize s) @@ -1688,13 +1643,9 @@ lemma doFlush_ccorres: (* FIXME AARCH64: move to VSpace_C *) sel4_arch_invocation_label_defs arch_invocation_label_defs) done -lemma cte_wp_cteCap_valid: (* FIXME AARCH64: move up *) - "\ cte_wp_at' ((=) cap \ cteCap) slot s; valid_objs' s \ \ valid_cap' cap s" - by (clarsimp simp: cte_wp_at_ctes_of ctes_of_valid') - (* The precondition is slightly different here to ARM/ARM_HYP, because we're flushing on kernel virtual addresses instead of user virtual addresses (hence also no VM root switching). *) -lemma performPageFlush_ccorres: (* FIXME AARCH64: move to VSpace_C; needs the [simp] lemmas above *) +lemma performPageFlush_ccorres: "ccorres (K (K \) \ dc) (liftxf errstate id (K ()) ret__unsigned_long_') (\s. pstart \ pstart + (end - start) \ ptrFromPAddr pstart \ ptrFromPAddr pstart + (end - start) \ @@ -1802,18 +1753,6 @@ lemma frame_at'_is_aligned_addrFromPPtr: apply (simp split: kernel_object.splits) done -lemma pptrUserTop_eq_mask_ipa_size: - "pptrUserTop = mask ipa_size" - by (simp add: pptrUserTop_def ipa_size_def) - -lemma mask_pptrUserTop_user_region: - "\ is_aligned v n; v + mask n \ pptrUserTop \ \ v \ user_region" - apply (simp add: user_region_def canonical_user_def pptrUserTop_eq_mask_ipa_size - word_and_or_mask_aligned) - apply (simp flip: and_mask_eq_iff_le_mask) - apply word_eqI_solve - done - lemma cap_frame_cap_lift_asid_upd_idem: "cap_get_tag cap = scast cap_frame_cap \ cap_frame_cap_lift cap\capFMappedASID_CL := capFMappedASID_CL (cap_frame_cap_lift cap) && mask 16\ = @@ -1863,21 +1802,6 @@ lemma ccap_relation_decodePageMap[unfolded asid_bits_def canonical_bit_def, simp cl_valid_cap_def) done -lemma user_region_canonical: (* FIXME AARCH64: move *) - "p \ user_region \ canonical_address p" - apply (simp add: canonical_address_range user_region_def canonical_user_def) - apply (erule order_trans) - apply (rule mask_mono) - apply (simp add: ipa_size_def canonical_bit_def split: if_split) - done - -lemma canonical_address_pptrUserTop_mask: (* FIXME AARCH64: move *) - "\ p + 2^n - 1 \ pptrUserTop; is_aligned p n \ \ canonical_address p" - apply (rule user_region_canonical) - apply (erule mask_pptrUserTop_user_region) - apply (simp add: mask_def field_simps) - done - lemmas canonical_address_C_pptrUserTop = canonical_address_pptrUserTop_mask[unfolded pptrUserTop_val word_le_nat_alt, simplified] @@ -2443,7 +2367,7 @@ lemma framesize_from_H_mask2: apply (simp add: framesize_defs)+ done -lemma performVSpaceFlush_ccorres: (* FIXME AARCH64: move to VSpace_C; needs the [simp] lemmas above *) +lemma performVSpaceFlush_ccorres: "ccorres (\_ rv'. rv' = scast EXCEPTION_NONE) ret__unsigned_long_' (\s. pstart \ pstart + (end - start) \ ptrFromPAddr pstart \ ptrFromPAddr pstart + (end - start) \ @@ -2759,44 +2683,6 @@ lemma injection_handler_stateAssert_relocate: = do v \ stateAssert ass xs; injection_handler Inl (f ()) >>=E g od" by (simp add: injection_handler_def handleE'_def bind_bindE_assoc bind_assoc) -lemma isVTableRoot_cap_eq: (* FIXME AARCH64: move, consider using it in slotcap_in_mem_VSpace *) - "isVTableRoot cap = - (isArchObjectCap cap \ isPageTableCap (capCap cap) \ capPTType (capCap cap) = VSRootPT_T)" - by (auto simp: isCap_simps isVTableRoot_ex) - -lemma ccap_relation_capASIDBase: (* FIXME AARCH64: move *) - "\ ccap_relation (ArchObjectCap (ASIDPoolCap p asid)) cap \ \ - capASIDBase_CL (cap_asid_pool_cap_lift cap) = asid" - by (clarsimp simp: cap_to_H_def Let_def cap_asid_pool_cap_lift_def - elim!: ccap_relationE - split: cap_CL.splits if_splits) - -lemma ccap_relation_capASIDPool: (* FIXME AARCH64: move *) - "\ ccap_relation (ArchObjectCap (ASIDPoolCap p asid)) cap \ \ - capASIDPool_CL (cap_asid_pool_cap_lift cap) = p" - by (clarsimp simp: cap_to_H_def Let_def cap_asid_pool_cap_lift_def - elim!: ccap_relationE - split: cap_CL.splits if_splits) - -lemma asid_map_get_tag_neq_none[simp]: (* FIXME AARCH64: move, beware of [simp] *) - "(asid_map_get_tag amap \ scast asid_map_asid_map_none) = - (asid_map_get_tag amap = scast asid_map_asid_map_vspace)" - by (simp add: asid_map_get_tag_def asid_map_tag_defs) - -lemma asid_map_get_tag_neq_vspace[simp]: (* FIXME AARCH64: move, beware of [simp] *) - "(asid_map_get_tag amap \ scast asid_map_asid_map_vspace) = - (asid_map_get_tag amap = scast asid_map_asid_map_none)" - by (simp add: asid_map_get_tag_def asid_map_tag_defs) - -lemma asid_map_tags_neq[simp]: (* FIXME AARCH64: move, beware of [simp] *) - "(scast asid_map_asid_map_vspace :: machine_word) \ scast asid_map_asid_map_none" - "(scast asid_map_asid_map_none :: machine_word) \ scast asid_map_asid_map_vspace" - by (auto simp: asid_map_tag_defs) - -lemma casid_map_relation_None[simp]: (* FIXME AARCH64: move, beware of [simp] *) - "(casid_map_relation None amap) = (asid_map_get_tag amap = scast asid_map_asid_map_none)" - by (simp add: casid_map_relation_def asid_map_lift_def Let_def split: option.splits if_splits) - lemma decodeARMMMUInvocation_ccorres: notes Collect_const[simp del] if_cong[cong] shows @@ -3588,7 +3474,6 @@ lemma readVCPUReg_ccorres: apply fastforce done -(* FIXME AARCH64 move, something like it used to be in Arch_R on ARM_HYP *) crunch st_tcb_at'[wp]: readVCPUReg "\s. Q (st_tcb_at' P t s)" (wp: crunch_wps simp: crunch_simps) @@ -4288,36 +4173,6 @@ lemma liftE_invokeVCPUAckVPPI_empty_return: unfolding invokeVCPUAckVPPI_def by (clarsimp simp: liftE_bindE bind_assoc) -(* FIXME AARCH64 used to be in Finalise_C *) -lemma checkIRQ_ret_good: - "\\s. (irq \ scast Kernel_C.maxIRQ \ P s) \ Q s\ checkIRQ irq \\rv. P\, \\rv. Q\" - apply (clarsimp simp: checkIRQ_def rangeCheck_def maxIRQ_def minIRQ_def) - apply (rule hoare_pre,wp) - by (clarsimp simp: Kernel_C.maxIRQ_def split: if_split) - -(* FIXME AARCH64 used to be in Finalise_C *) -lemma Arch_checkIRQ_ccorres: - "ccorres (syscall_error_rel \ (\r r'. irq \ scast Kernel_C.maxIRQ)) - (liftxf errstate id undefined ret__unsigned_long_') - \ (UNIV \ \irq = \irq_w___unsigned_long\) [] - (checkIRQ irq) (Call Arch_checkIRQ_'proc)" - apply (cinit lift: irq_w___unsigned_long_' ) - apply (simp add: rangeCheck_def unlessE_def AARCH64.minIRQ_def checkIRQ_def - ucast_nat_def word_le_nat_alt[symmetric] - linorder_not_le[symmetric] maxIRQ_def - length_ineq_not_Nil hd_conv_nth cast_simps - del: Collect_const cong: call_ignore_cong) - apply (rule ccorres_Cond_rhs_Seq) - apply (rule ccorres_from_vcg_split_throws[where P=\ and P'=UNIV]) - apply vcg - apply (rule conseqPre, vcg) - apply (clarsimp simp: throwError_def return_def Kernel_C.maxIRQ_def - exception_defs syscall_error_rel_def - syscall_error_to_H_cases) - apply (clarsimp simp: Kernel_C.maxIRQ_def) - apply (rule ccorres_return_CE, simp+) - done - lemma decodeVCPUAckVPPI_ccorres: notes if_cong[cong] Collect_const[simp del] shows diff --git a/proof/crefine/AARCH64/CLevityCatch.thy b/proof/crefine/AARCH64/CLevityCatch.thy index 13c51fcfbd..0f30569422 100644 --- a/proof/crefine/AARCH64/CLevityCatch.thy +++ b/proof/crefine/AARCH64/CLevityCatch.thy @@ -14,6 +14,65 @@ imports Boolean_C begin +(* FIXME AARCH64: holding area for things to move to CParser/TypHeapLib or higher. + Check other architectures for use. *) + +lemma lift_t_Some_iff: + "lift_t g hrs p = Some v \ hrs_htd hrs, g \\<^sub>t p \ h_val (hrs_mem hrs) p = v" + unfolding hrs_htd_def hrs_mem_def by (cases hrs) (auto simp: lift_t_if) + +context + fixes p :: "'a::mem_type ptr" + fixes q :: "'b::c_type ptr" + fixes d g\<^sub>p g\<^sub>q + assumes val_p: "d,g\<^sub>p \\<^sub>t p" + assumes val_q: "d,g\<^sub>q \\<^sub>t q" + assumes disj: "typ_uinfo_t TYPE('a) \\<^sub>t typ_uinfo_t TYPE('b)" +begin + +lemma h_val_heap_same_typ_disj: + "h_val (heap_update p v h) q = h_val h q" + using disj by (auto intro: h_val_heap_same[OF val_p val_q] + simp: tag_disj_def sub_typ_proper_def field_of_t_def typ_tag_lt_def + field_of_def typ_tag_le_def) + +lemma h_val_heap_same_hrs_mem_update_typ_disj: + "h_val (hrs_mem (hrs_mem_update (heap_update p v) s)) q = h_val (hrs_mem s) q" + by (simp add: hrs_mem_update h_val_heap_same_typ_disj) + +end + +lemmas h_t_valid_nested_fields = + h_t_valid_field[OF h_t_valid_field[OF h_t_valid_field]] + h_t_valid_field[OF h_t_valid_field] + h_t_valid_field + +lemmas h_t_valid_fields_clift = + h_t_valid_nested_fields[OF h_t_valid_clift] + h_t_valid_clift + +lemma aligned_intvl_0: + "\ is_aligned p n; n < LENGTH('a) \ \ (0 \ {p..+2^n}) = (p = 0)" for p::"'a::len word" + apply (rule iffI; clarsimp simp: intvl_def) + apply (drule_tac d="of_nat k" in is_aligned_add_or) + apply (simp add: word_less_nat_alt unat_of_nat order_le_less_trans[rotated]) + apply word_eqI_solve + apply (rule_tac x=0 in exI) + apply simp + done + +lemma heap_list_h_eq_better: (* FIXME AARCH64: replace heap_list_h_eq *) + "\p. \ x \ {p..+q}; heap_list h q p = heap_list h' q p \ + \ h x = h' x" +proof (induct q) + case 0 thus ?case by simp +next + case (Suc n) thus ?case by (force dest: intvl_neq_start) +qed + +(* end holding area *) + + context begin interpretation Arch . (*FIXME: arch_split*) (* Short-hand for unfolding cumbersome machine constants *) @@ -178,7 +237,6 @@ lemma option_to_ptr_simps [simp]: "option_to_ptr (Some x) = Ptr x" by (auto simp: option_to_ptr_def split: option.split) -(* FIXME MOVE *) lemma option_to_ptr_NULL_eq: "\ option_to_ptr p = p' \ \ (p' = NULL) = (p = None \ p = Some 0)" unfolding option_to_ptr_def option_to_0_def diff --git a/proof/crefine/AARCH64/CSpace_C.thy b/proof/crefine/AARCH64/CSpace_C.thy index fc13c5994e..50d876f18a 100644 --- a/proof/crefine/AARCH64/CSpace_C.thy +++ b/proof/crefine/AARCH64/CSpace_C.thy @@ -809,18 +809,8 @@ lemma update_freeIndex: apply (case_tac cte; clarsimp dest!: ctes_of_valid_cap' simp: valid_cap'_def) by auto -(* FIXME: move *) -lemma ccorres_cases: - assumes P: " P \ ccorres r xf G G' hs a b" - assumes notP: "\P \ ccorres r xf H H' hs a b" - shows "ccorres r xf (\s. (P \ G s) \ (\P \ H s)) - ({s. P \ s \ G'} \ {s. \P \ s \ H'}) - hs a b" - apply (cases P, auto simp: P notP) - done - lemma capBlockSize_CL_maxSize: - " \ cap_get_tag c = scast cap_untyped_cap \ \ capBlockSize_CL (cap_untyped_cap_lift c) < 0x40" + "\ cap_get_tag c = scast cap_untyped_cap \ \ capBlockSize_CL (cap_untyped_cap_lift c) < 0x40" apply (clarsimp simp: cap_untyped_cap_lift_def) apply (clarsimp simp: cap_lift_def) apply (clarsimp simp: cap_untyped_cap_def cap_null_cap_def) @@ -2469,41 +2459,6 @@ lemma valid_cap'_PageCap_is_aligned: apply (simp add: valid_cap'_def capAligned_def) done -lemma cap_get_tag_isCap_unfolded_H_cap2: (* FIXME AARCH64: move; potentially replace original *) - shows "ccap_relation (capability.ThreadCap v0) cap' \ (cap_get_tag cap' = scast cap_thread_cap)" - and "ccap_relation (capability.NullCap) cap' \ (cap_get_tag cap' = scast cap_null_cap)" - and "ccap_relation (capability.NotificationCap v4 v5 v6 v7) cap' \ (cap_get_tag cap' = scast cap_notification_cap) " - and "ccap_relation (capability.EndpointCap v8 v9 v10 v10b v11 v12) cap' \ (cap_get_tag cap' = scast cap_endpoint_cap)" - and "ccap_relation (capability.IRQHandlerCap v13) cap' \ (cap_get_tag cap' = scast cap_irq_handler_cap)" - and "ccap_relation (capability.IRQControlCap) cap' \ (cap_get_tag cap' = scast cap_irq_control_cap)" - and "ccap_relation (capability.Zombie v14 v15 v16) cap' \ (cap_get_tag cap' = scast cap_zombie_cap)" - and "ccap_relation (capability.ReplyCap v17 v18 vr18b) cap' \ (cap_get_tag cap' = scast cap_reply_cap)" - and "ccap_relation (capability.UntypedCap v100 v19 v20 v20b) cap' \ (cap_get_tag cap' = scast cap_untyped_cap)" - and "ccap_relation (capability.CNodeCap v21 v22 v23 v24) cap' \ (cap_get_tag cap' = scast cap_cnode_cap)" - and "ccap_relation (capability.DomainCap) cap' \ (cap_get_tag cap' = scast cap_domain_cap)" - - and "ccap_relation (capability.ArchObjectCap arch_capability.ASIDControlCap) cap' \ (cap_get_tag cap' = scast cap_asid_control_cap)" - and "ccap_relation (capability.ArchObjectCap (arch_capability.ASIDPoolCap v28 v29)) cap' \ (cap_get_tag cap' = scast cap_asid_pool_cap)" - and "ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap v30 v32 v31)) cap' - \ if v32 = VSRootPT_T - then cap_get_tag cap' = scast cap_vspace_cap - else cap_get_tag cap' = scast cap_page_table_cap" - and "ccap_relation (capability.ArchObjectCap (arch_capability.FrameCap v101 v44 v45 v46 v47)) cap' \ (cap_get_tag cap' = scast cap_frame_cap)" - and "ccap_relation (capability.ArchObjectCap (arch_capability.VCPUCap v48)) cap' \ (cap_get_tag cap' = scast cap_vcpu_cap)" - apply (simp add: cap_get_tag_isCap cap_get_tag_isCap_ArchObject isCap_simps) - apply (frule cap_get_tag_isCap(2), simp) - apply (clarsimp simp: cap_get_tag_isCap cap_get_tag_isCap_ArchObject isCap_simps - split: if_splits pt_type.splits)+ - done - -lemmas ccap_rel_cap_get_tag_cases_arch2 = (* FIXME AARCH64: move; potentially replace original *) - cap_get_tag_isCap_unfolded_H_cap2(12-16) - [OF back_subst[of "\cap. ccap_relation (ArchObjectCap cap) cap'" for cap'], - OF back_subst[of "\cap. ccap_relation cap cap'" for cap']] - -lemmas ccap_rel_cap_get_tag_cases_arch2' = (* FIXME AARCH64: move; potentially replace original *) - ccap_rel_cap_get_tag_cases_arch2[OF _ refl] - lemma Arch_sameRegionAs_spec: notes cap_get_tag = ccap_rel_cap_get_tag_cases_arch2' shows @@ -3403,10 +3358,6 @@ lemma ensureNoChildren_ccorres: apply (simp add: cte_wp_at_ctes_of) done -lemma not_VSRootPT_T_eq: (* FIXME AARCH64: move to AInvs *) - "(pt_t \ VSRootPT_T) = (pt_t = NormalPT_T)" - by (cases pt_t; simp) - lemma Arch_deriveCap_ccorres: "ccorres (syscall_error_rel \ ccap_relation) deriveCap_xf \ (UNIV \ {s. ccap_relation (ArchObjectCap cap) (cap_' s)}) [] diff --git a/proof/crefine/AARCH64/CSpace_RAB_C.thy b/proof/crefine/AARCH64/CSpace_RAB_C.thy index 83465aae63..9818059f28 100644 --- a/proof/crefine/AARCH64/CSpace_RAB_C.thy +++ b/proof/crefine/AARCH64/CSpace_RAB_C.thy @@ -118,16 +118,6 @@ lemma andCapRights_ac: "andCapRights a (andCapRights b c) = andCapRights b (andCapRights a c)" by (simp add: andCapRights_def conj_comms split: cap_rights.split)+ -(* FIXME: move, duplicated in CSpace_C *) -lemma ccorres_cases: - assumes P: " P \ ccorres_underlying sr \ r xf ar axf G G' hs a b" - assumes notP: "\P \ ccorres_underlying sr \ r xf ar axf H H' hs a b" - shows "ccorres_underlying sr \ r xf ar axf (\s. (P \ G s) \ (\P \ H s)) - ({s. P \ s \ G'} \ {s. \P \ s \ H'}) - hs a b" - apply (cases P, auto simp: P notP) - done - lemma ccorres_locateSlotCap_push: "ccorres_underlying sr \ r xf ar axf P P' hs (a >>=E (\x. locateSlotCap cp n >>= (\p. b p x))) c diff --git a/proof/crefine/AARCH64/Ctac_lemmas_C.thy b/proof/crefine/AARCH64/Ctac_lemmas_C.thy index 3dc03b45ba..cb42899d81 100644 --- a/proof/crefine/AARCH64/Ctac_lemmas_C.thy +++ b/proof/crefine/AARCH64/Ctac_lemmas_C.thy @@ -148,6 +148,38 @@ lemma array_assertion_abs_vspace: lemmas ccorres_move_array_assertion_vspace = ccorres_move_array_assertions[OF array_assertion_abs_vspace] +lemma array_assertion_abs_pt: + "\s s'. (s, s') \ rf_sr + \ (page_table_at' NormalPT_T pt s \ gsPTTypes (ksArchState s) pt = Some NormalPT_T) + \ (n s' \ 2 ^ ptTranslationBits NormalPT_T \ (x s' \ 0 \ n s' \ 0)) + \ (x s' = 0 \ array_assertion (pte_Ptr pt) (n s') (hrs_htd (t_hrs_' (globals s'))))" + apply (intro allI impI disjCI2, clarsimp) + apply (drule (2) ptable_at_rf_sr, clarsimp) + apply (erule clift_array_assertion_imp; simp) + apply (rule_tac x=0 in exI, simp add: bit_simps) + done + +lemmas ccorres_move_array_assertion_pt + = ccorres_move_array_assertions[OF array_assertion_abs_pt] + +lemma array_assertion_abs_pt_gen: + "\s s'. (s, s') \ rf_sr + \ (page_table_at' pt_t pt s \ gsPTTypes (ksArchState s) pt = Some pt_t) + \ (n s' \ 2 ^ ptTranslationBits pt_t \ (x s' \ 0 \ n s' \ 0)) + \ (x s' = 0 \ array_assertion (pte_Ptr pt) (n s') (hrs_htd (t_hrs_' (globals s'))))" + apply (intro allI impI disjCI2, clarsimp) + apply (cases pt_t; simp) + apply (drule (2) vspace_at_rf_sr, clarsimp) + apply (erule clift_array_assertion_imp; simp) + apply (rule_tac x=0 in exI, simp add: bit_simps Kernel_Config.config_ARM_PA_SIZE_BITS_40_def) + apply (drule (2) ptable_at_rf_sr, clarsimp) + apply (erule clift_array_assertion_imp; simp) + apply (rule_tac x=0 in exI, simp add: bit_simps) + done + +lemmas ccorres_move_array_assertion_pt_gen + = ccorres_move_array_assertions[OF array_assertion_abs_pt_gen] + lemma move_c_guard_ap: "\s s'. (s, s') \ rf_sr \ asid_pool_at' (ptr_val p) s \ True \ s' \\<^sub>c (p :: asid_pool_C ptr)" @@ -162,7 +194,7 @@ lemmas ccorres_move_c_guard_ap = ccorres_move_c_guards [OF move_c_guard_ap] lemma array_assertion_abs_irq: "\s s'. (s, s') \ rf_sr \ True - \ (n s' \ 64 \ (x s' \ 0 \ n s' \ 0)) + \ (n s' \ 2 ^ LENGTH(irq_len) \ (x s' \ 0 \ n s' \ 0)) \ (x s' = 0 \ array_assertion intStateIRQNode_Ptr (n s') (hrs_htd (t_hrs_' (globals s'))))" apply (intro allI impI disjCI2) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) @@ -202,6 +234,16 @@ lemma move_c_guard_vcpu: lemmas ccorres_move_c_guard_vcpu = ccorres_move_c_guards[OF move_c_guard_vcpu] +lemma ccorres_h_t_valid_armKSGlobalUserVSpace: + "ccorres r xf P P' hs f (f' ;; g') \ + ccorres r xf P P' hs f (Guard C_Guard {s'. s' \\<^sub>c armKSGlobalUserVSpace_Ptr} f';; g')" + apply (rule ccorres_guard_imp2) + apply (rule ccorres_move_c_guards[where P = \]) + apply clarsimp + apply assumption + apply simp + by (clarsimp simp add: rf_sr_def cstate_relation_def Let_def) + end end diff --git a/proof/crefine/AARCH64/Finalise_C.thy b/proof/crefine/AARCH64/Finalise_C.thy index 1daea13689..b7b077dc41 100644 --- a/proof/crefine/AARCH64/Finalise_C.thy +++ b/proof/crefine/AARCH64/Finalise_C.thy @@ -13,23 +13,6 @@ begin context kernel_m begin -(* FIXME AARCH64: move to CCorres_UL, remove previous ccorres_cases, check RISCV *) -(* note: moving this lemma outside of kernel_m locale currently causes some proofs to fail *) -lemma ccorres_cases: - assumes P: " P \ ccorres_underlying srel Ga rrel xf arrel axf G G' hs a b" - assumes notP: "\P \ ccorres_underlying srel Ga rrel xf arrel axf H H' hs a b" - shows "ccorres_underlying srel Ga rrel xf arrel axf (\s. (P \ G s) \ (\P \ H s)) - ({s. P \ s \ G'} \ {s. \P \ s \ H'}) - hs a b" - apply (cases P, auto simp: P notP) - done - -(* FIXME AARCH64: move up, make ccorres_underlying, check if it could be made [simp], check RISCV *) -(* Provide full ccorres context so it will work with ccorres_prog_only_cong enabled *) -lemma ccorres_dc_comp: - "ccorres (dc \ R) xf P P' hs m c = ccorres dc xf P P' hs m c " - by simp - declare if_split [split del] definition @@ -1362,14 +1345,6 @@ lemma setObject_ccorres_lemma: apply clarsimp done -(* FIXME AARCH64 move to where haskell_assertE_inv is in VSpace_C, and then both of those should get - moved out elsewhere. For future consideration, the _inv assert rules are not safe. - haskell_assert_inv is introduced accidentally in TcbAcc_R during a crunch *) -lemma haskell_assertE_wp: - "\\s. F \ Q () s\ haskell_assertE F L \Q\,\E\" - unfolding haskell_assertE_def - by (rule assertE_wp) - lemma findVSpaceForASID_nonzero: "\\\ findVSpaceForASID asid \\rv s. rv \ 0\,-" unfolding findVSpaceForASID_def @@ -1825,22 +1800,6 @@ lemma getIRQSlot_ccorres_stuff: size_of_def mult.commute mult.left_commute of_int_uint_ucast ) done -(* FIXME AARCH64 override original *) -(* the number here should match the one in intStateIRQNode_array_Ptr for this to be useful*) -lemma array_assertion_abs_irq: - "\s s'. (s, s') \ rf_sr \ True - \ (n s' \ 512 \ (x s' \ 0 \ n s' \ 0)) - \ (x s' = 0 \ array_assertion intStateIRQNode_Ptr (n s') (hrs_htd (t_hrs_' (globals s'))))" - apply (intro allI impI disjCI2) - apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) - apply (clarsimp simp: h_t_valid_clift_Some_iff) - apply (erule clift_array_assertion_imp, (simp add: exI[where x=0])+) - done - -(* FIXME AARCH64 remove *) -lemmas ccorres_move_array_assertion_irq - = ccorres_move_array_assertions [OF array_assertion_abs_irq] - lemma deletingIRQHandler_ccorres: "ccorres dc xfdc (invs' and (\s. weak_sch_act_wf (ksSchedulerAction s) s)) ({s. irq_opt_relation (Some irq) (irq_' s)}) [] @@ -1962,21 +1921,6 @@ lemma cnotification_relation_udpate_arch: apply (safe ; case_tac "xa = p" ; clarsimp simp: option_map2_def map_option_case) done -(* FIXME AARCH64 move (also at least on ARM_HYP) *) -lemma case_option_both[simp]: - "(case f of None \ P | _ \ P) = P" - by (auto split: option.splits) - -(* FIXME AARCH64 move (also at least on ARM_HYP) *) -lemma if_case_opt_same_branches: - "cond \ Option.is_none opt \ - (if cond then - case opt of - None \ f - | Some x \ g x - else f) = f" - by (cases cond; cases opt; clarsimp) - (* FIXME AARCH64 slow, uses unfolding of state relation for typ_heap_simps, the vcpuUpdate or equivalent approach for TCB would be better *) lemma archThreadSet_tcbVCPU_Basic_ccorres: @@ -2012,12 +1956,6 @@ lemma archThreadSet_tcbVCPU_Basic_ccorres: apply (clarsimp simp: cvariable_relation_upd_const) done -(* FIXME AARCH64 move (also on ARM_HYP) *) -lemma update_vcpu_map_to_vcpu: - "map_to_vcpus ((ksPSpace s)(p \ KOArch (KOVCPU vcpu))) - = (map_to_vcpus (ksPSpace s))(p \ vcpu)" - by (rule ext, clarsimp simp: projectKOs map_comp_def split: if_split) - lemma setObject_vcpuTCB_updated_Basic_ccorres: "ccorres dc xfdc (ko_at' (vcpuTCBPtr_update t vcpu) vcpuptr) UNIV hs (setObject vcpuptr (vcpuTCBPtr_update (\_. tptr) vcpu)) @@ -2281,27 +2219,6 @@ lemma dissociateVCPUTCB_vcpu_ccorres: (dissociateVCPUTCB vcpuptr tptr) (Call dissociateVCPUTCB_'proc)" by (rule ccorres_guard_imp2[OF dissociateVCPUTCB_ccorres]) clarsimp - -(* FIXME AARCH64: move up, also use in ADT_C and Tcb_Queue.tcb_at_not_NULL *) -lemma aligned_tcb_ctcb_not_NULL: - assumes "is_aligned p tcbBlockSizeBits" - shows "tcb_ptr_to_ctcb_ptr p \ NULL" -proof - assume "tcb_ptr_to_ctcb_ptr p = NULL" - hence "p + ctcb_offset = 0" - by (simp add: tcb_ptr_to_ctcb_ptr_def) - moreover - from `is_aligned p tcbBlockSizeBits` - have "p + ctcb_offset = p || ctcb_offset" - by (rule word_and_or_mask_aligned) (simp add: ctcb_offset_defs objBits_defs mask_def) - moreover - have "ctcb_offset !! ctcb_size_bits" - by (simp add: ctcb_offset_defs objBits_defs) - ultimately - show False - by (simp add: bang_eq) -qed - lemma associateVCPUTCB_ccorres: "ccorres dc xfdc (invs' and tcb_at' tptr and vcpu_at' vcpuptr) @@ -2920,6 +2837,35 @@ lemma finaliseCap_ccorres: apply (frule(1) ccap_relation_IRQHandler_mask) apply (clarsimp simp add:mask_eq_ucast_eq) done - end + +lemma checkIRQ_ret_good: + "\\s. (irq \ scast Kernel_C.maxIRQ \ P s) \ Q s\ checkIRQ irq \\rv. P\, \\rv. Q\" + apply (clarsimp simp: checkIRQ_def rangeCheck_def maxIRQ_def minIRQ_def) + apply (rule hoare_pre,wp) + by (clarsimp simp: Kernel_C.maxIRQ_def split: if_split) + +lemma Arch_checkIRQ_ccorres: + "ccorres (syscall_error_rel \ (\r r'. irq \ scast Kernel_C.maxIRQ)) + (liftxf errstate id undefined ret__unsigned_long_') + \ (UNIV \ \irq = \irq_w___unsigned_long\) [] + (checkIRQ irq) (Call Arch_checkIRQ_'proc)" + apply (cinit lift: irq_w___unsigned_long_' ) + apply (simp add: rangeCheck_def unlessE_def AARCH64.minIRQ_def checkIRQ_def + ucast_nat_def word_le_nat_alt[symmetric] + linorder_not_le[symmetric] maxIRQ_def + length_ineq_not_Nil hd_conv_nth cast_simps + del: Collect_const cong: call_ignore_cong) + apply (rule ccorres_Cond_rhs_Seq) + apply (rule ccorres_from_vcg_split_throws[where P=\ and P'=UNIV]) + apply vcg + apply (rule conseqPre, vcg) + apply (clarsimp simp: throwError_def return_def Kernel_C.maxIRQ_def + exception_defs syscall_error_rel_def + syscall_error_to_H_cases) + apply (clarsimp simp: Kernel_C.maxIRQ_def) + apply (rule ccorres_return_CE, simp+) + done + +end end diff --git a/proof/crefine/AARCH64/Interrupt_C.thy b/proof/crefine/AARCH64/Interrupt_C.thy index 464f89bc03..2b456b3af3 100644 --- a/proof/crefine/AARCH64/Interrupt_C.thy +++ b/proof/crefine/AARCH64/Interrupt_C.thy @@ -427,36 +427,6 @@ lemma decodeIRQ_arch_helper: "x \ IRQIssueIRQHandler \ (case x of IRQIssueIRQHandler \ f | _ \ g) = g" by (clarsimp split: gen_invocation_labels.splits) -(* FIXME AARCH64 move back to Finalise_C, otherwise we get duplication in Arch_C *) -lemma checkIRQ_ret_good: - "\\s. (irq \ scast Kernel_C.maxIRQ \ P s) \ Q s\ checkIRQ irq \\rv. P\, \\rv. Q\" - apply (clarsimp simp: checkIRQ_def rangeCheck_def maxIRQ_def minIRQ_def) - apply (rule hoare_pre,wp) - by (clarsimp simp: Kernel_C.maxIRQ_def split: if_split) - -(* FIXME AARCH64 move back to Finalise_C, otherwise we get duplication in Arch_C *) -lemma Arch_checkIRQ_ccorres: - "ccorres (syscall_error_rel \ (\r r'. irq \ scast Kernel_C.maxIRQ)) - (liftxf errstate id undefined ret__unsigned_long_') - \ (UNIV \ \irq = \irq_w___unsigned_long\) [] - (checkIRQ irq) (Call Arch_checkIRQ_'proc)" - apply (cinit lift: irq_w___unsigned_long_' ) - apply (simp add: rangeCheck_def unlessE_def AARCH64.minIRQ_def checkIRQ_def - ucast_nat_def word_le_nat_alt[symmetric] - linorder_not_le[symmetric] maxIRQ_def - length_ineq_not_Nil hd_conv_nth cast_simps - del: Collect_const cong: call_ignore_cong) - apply (rule ccorres_Cond_rhs_Seq) - apply (rule ccorres_from_vcg_split_throws[where P=\ and P'=UNIV]) - apply vcg - apply (rule conseqPre, vcg) - apply (clarsimp simp: throwError_def return_def Kernel_C.maxIRQ_def - exception_defs syscall_error_rel_def - syscall_error_to_H_cases) - apply (clarsimp simp: Kernel_C.maxIRQ_def) - apply (rule ccorres_return_CE, simp+) - done - lemma checkIRQ_wpE: "\ \s. irq \ ucast maxIRQ \ P () s \ checkIRQ irq \P\, \\_. \\" unfolding checkIRQ_def rangeCheck_def diff --git a/proof/crefine/AARCH64/Invoke_C.thy b/proof/crefine/AARCH64/Invoke_C.thy index e026ed208d..1962b2f42a 100644 --- a/proof/crefine/AARCH64/Invoke_C.thy +++ b/proof/crefine/AARCH64/Invoke_C.thy @@ -1631,14 +1631,6 @@ lemma pspace_no_overlap_underlying_zero_update: apply blast done -lemma addrFromPPtr_mask_cacheLineSize: (* FIXME AARCH64 move, remove duplicate in Arch_C *) - "addrFromPPtr ptr && mask cacheLineSize = ptr && mask cacheLineSize" - apply (simp add: addrFromPPtr_def AARCH64.pptrBase_def pptrBaseOffset_def canonical_bit_def - paddrBase_def cacheLineSize_def) - apply word_bitwise - apply (simp add:mask_def) - done - lemma clearMemory_untyped_ccorres: "ccorres dc xfdc ((\s. invs' s \ (\cap. cte_wp_at' (\cte. cteCap cte = cap) ut_slot s diff --git a/proof/crefine/AARCH64/IpcCancel_C.thy b/proof/crefine/AARCH64/IpcCancel_C.thy index ae15dd14ba..4513f68ca0 100644 --- a/proof/crefine/AARCH64/IpcCancel_C.thy +++ b/proof/crefine/AARCH64/IpcCancel_C.thy @@ -182,82 +182,6 @@ lemma ntfn_ptr_set_queue_spec: canonical_bit_def) done -(* FIXME AARCH64: move up into TcbQueue_C *) -lemma tcb_queue_relation_next_canonical: - assumes "tcb_queue_relation getNext getPrev mp queue NULL qhead" - assumes valid_ep: "\t\set queue. tcb_at' t s" - "distinct queue" - "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb" - "tcbp \ set queue" - assumes canon: "pspace_canonical' s" - shows "make_canonical (ptr_val (getNext tcb)) = ptr_val (getNext tcb)" -proof (cases "getNext tcb = NULL") - case True - thus ?thesis by simp -next - case False - hence "ctcb_ptr_to_tcb_ptr (getNext tcb) \ set queue" using assms - by (fastforce dest: tcb_queueD split: if_split_asm) - with valid_ep(1) - have tcb: "tcb_at' (ctcb_ptr_to_tcb_ptr (getNext tcb)) s" .. - with canon - have "canonical_address (ctcb_ptr_to_tcb_ptr (getNext tcb))" - by (simp add: obj_at'_is_canonical) - moreover - have "is_aligned (ctcb_ptr_to_tcb_ptr (getNext tcb)) tcbBlockSizeBits" - using tcb by (rule tcb_aligned') - ultimately - have "canonical_address (ptr_val (getNext tcb))" - by (rule canonical_address_ctcb_ptr) - thus ?thesis - by (simp add: canonical_make_canonical_idem) -qed - -lemma tcb_queue_relation'_next_canonical: - "\ tcb_queue_relation' getNext getPrev mp queue qhead qend; \t\set queue. tcb_at' t s; - distinct queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcbp \ set queue; - pspace_canonical' s\ - \ make_canonical (ptr_val (getNext tcb)) = ptr_val (getNext tcb)" - by (rule tcb_queue_relation_next_canonical [OF tcb_queue_relation'_queue_rel]) - -(* FIXME AARCH64: move up into TcbQueue_C *) -lemma tcb_queue_relation_prev_canonical: - assumes "tcb_queue_relation getNext getPrev mp queue NULL qhead" - assumes valid_ep: "\t\set queue. tcb_at' t s" - "distinct queue" - "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb" - "tcbp \ set queue" - assumes canon: "pspace_canonical' s" - shows "make_canonical (ptr_val (getPrev tcb)) = ptr_val (getPrev tcb)" -proof (cases "getPrev tcb = NULL") - case True - thus ?thesis by simp -next - case False - hence "ctcb_ptr_to_tcb_ptr (getPrev tcb) \ set queue" using assms - by (fastforce dest: tcb_queueD split: if_split_asm) - with valid_ep(1) - have tcb: "tcb_at' (ctcb_ptr_to_tcb_ptr (getPrev tcb)) s" .. - with canon - have "canonical_address (ctcb_ptr_to_tcb_ptr (getPrev tcb))" - by (simp add: obj_at'_is_canonical) - moreover - have "is_aligned (ctcb_ptr_to_tcb_ptr (getPrev tcb)) tcbBlockSizeBits" - using tcb by (rule tcb_aligned') - ultimately - have "canonical_address (ptr_val (getPrev tcb))" - by (rule canonical_address_ctcb_ptr) - thus ?thesis - by (simp add: canonical_make_canonical_idem) -qed - -lemma tcb_queue_relation'_prev_canonical: - "\ tcb_queue_relation' getNext getPrev mp queue qhead qend; \t\set queue. tcb_at' t s; - distinct queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcbp \ set queue; - pspace_canonical' s\ - \ make_canonical (ptr_val (getPrev tcb)) = ptr_val (getPrev tcb)" - by (rule tcb_queue_relation_prev_canonical [OF tcb_queue_relation'_queue_rel]) - lemma cancelSignal_ccorres_helper: "ccorres dc xfdc (invs' and st_tcb_at' ((=) (BlockedOnNotification ntfn)) thread and ko_at' ntfn' ntfn) UNIV diff --git a/proof/crefine/AARCH64/Ipc_C.thy b/proof/crefine/AARCH64/Ipc_C.thy index a5e259edbe..b7cdfafc73 100644 --- a/proof/crefine/AARCH64/Ipc_C.thy +++ b/proof/crefine/AARCH64/Ipc_C.thy @@ -296,11 +296,6 @@ lemmas syscallMessageC_def = kernel_all_substitute.fault_messages_def abbreviation "exceptionMessageC \ kernel_all_substitute.fault_messages.[unat MessageID_Exception]" lemmas exceptionMessageC_def = kernel_all_substitute.fault_messages_def -(* FIXME AARCH64 move to StateRelation_C *) -lemma ELR_EL1_is_NextIP[simp]: - "Kernel_C.ELR_EL1 = Kernel_C.NextIP" - by (simp add: C_register_defs) - lemma syscallMessage_ccorres: "n < unat n_syscallMessage \ register_from_H (AARCH64_H.syscallMessage ! n) @@ -567,11 +562,6 @@ lemma threadGet_discarded: apply (simp add: bind_def simpler_gets_def get_def) done -(* FIXME AARCH64 move to IsolatedThreadAction where existing setRegister_simple is commented out *) -lemma setRegister_simple: - "setRegister r v = (\con. ({((), UserContext (fpu_state con) ((user_regs con)(r := v)))}, False))" - by (simp add: setRegister_def simpler_modify_def) - lemma handleFaultReply': notes option.case_cong_weak [cong] wordSize_def'[simp] take_append[simp del] prod.case_cong_weak[cong] assumes neq: "s \ r" @@ -6112,15 +6102,6 @@ lemma receiveIPC_ccorres [corres]: apply (auto simp: isCap_simps valid_cap'_def) done -lemma tcb_ptr_canonical: (* FIXME AARCH64: move *) - "\ pspace_canonical' s; tcb_at' t s \ \ - tcb_Ptr (make_canonical (ptr_val (tcb_ptr_to_ctcb_ptr t))) = tcb_ptr_to_ctcb_ptr t" - apply (frule (1) obj_at'_is_canonical) - apply (drule canonical_address_tcb_ptr) - apply (clarsimp simp: obj_at'_def objBits_simps' split: if_splits) - apply (clarsimp simp: canonical_make_canonical_idem) - done - lemma sendSignal_dequeue_ccorres_helper: "ccorres (\rv rv'. rv' = tcb_ptr_to_ctcb_ptr dest) dest___ptr_to_struct_tcb_C_' (invs' and st_tcb_at' ((=) (BlockedOnNotification ntfn)) dest diff --git a/proof/crefine/AARCH64/IsolatedThreadAction.thy b/proof/crefine/AARCH64/IsolatedThreadAction.thy index 390b1d03fb..528b57802e 100644 --- a/proof/crefine/AARCH64/IsolatedThreadAction.thy +++ b/proof/crefine/AARCH64/IsolatedThreadAction.thy @@ -236,10 +236,9 @@ lemma mapM_getRegister_simple: bind_def return_def) done -(* FIXME AARCH64: confirm this formulation is not needed compared to existing setRegister_simple lemma setRegister_simple: - "setRegister r v = (\con. ({((), UserContext ((user_regs con)(r := v)))}, False))" - by (simp add: setRegister_def simpler_modify_def) *) + "setRegister r v = (\con. ({((), UserContext (fpu_state con) ((user_regs con)(r := v)))}, False))" + by (simp add: setRegister_def simpler_modify_def) lemma zipWithM_setRegister_simple: "zipWithM_x setRegister rs vs @@ -963,14 +962,6 @@ lemma cap_case_isPageTableCap: apply (case_tac option; simp) done -(* FIXME AARCH64 move *) -lemma getObject_asidpool_inv[wp]: - "\P\ getObject l \\(rv :: asidpool). P\" - apply (rule getObject_inv) - apply simp - apply (rule loadObject_default_inv) - done - lemma armContextSwitch_isolatable: "thread_actions_isolatable idx (armContextSwitch p asid)" supply if_split[split del] @@ -991,7 +982,7 @@ lemma armContextSwitch_isolatable: lemma setVMRoot_isolatable: "thread_actions_isolatable idx (setVMRoot t)" - supply if_split[split del] + supply if_split[split del] haskell_assertE_inv[wp] apply (simp add: setVMRoot_def getThreadVSpaceRoot_def locateSlot_conv getSlotCap_def if_bool_simps cap_case_isPageTableCap diff --git a/proof/crefine/AARCH64/Refine_C.thy b/proof/crefine/AARCH64/Refine_C.thy index ec6cf2939d..eb460f7ec0 100644 --- a/proof/crefine/AARCH64/Refine_C.thy +++ b/proof/crefine/AARCH64/Refine_C.thy @@ -43,14 +43,14 @@ lemma ucast_8_32_neq: "x \ 0xFF \ UCAST(8 \ 32 signed) x \ 0xFF" by uint_arith (clarsimp simp: uint_up_ucast is_up) -(* FIXME AARCH64 move, wrong name, original version likely useless in ArchMove_C, check *) +(* FIXME AARCH64 move, wrong name, eliminate magic number *) lemma getActiveIRQ_neq_Some0xFF': "\\\ getActiveIRQ in_kernel \\rv s. rv \ Some 0x1FF\" apply (simp add: getActiveIRQ_def) apply wpsimp using irq_oracle_max_irq apply (simp add: maxIRQ_def) - apply (drule_tac x="(Suc (irq_state s))" in spec) + apply (drule_tac x="Suc (irq_state s)" in spec) apply clarsimp done diff --git a/proof/crefine/AARCH64/Retype_C.thy b/proof/crefine/AARCH64/Retype_C.thy index 2f97581052..b3935e6c9b 100644 --- a/proof/crefine/AARCH64/Retype_C.thy +++ b/proof/crefine/AARCH64/Retype_C.thy @@ -4802,16 +4802,6 @@ lemma placeNewObject_pte_pt: apply (simp add: region_actually_is_bytes bit_simps) done -(* FIXME AARCH64: move; could be simp *) -lemma pt_bits_minus_pte_bits: - "pt_bits pt_t - pte_bits = ptTranslationBits pt_t" - by (simp add: bit_simps) - -(* FIXME AARCH64: move; could be simp *) -lemma ptTranslationBits_plus_pte_bits: - "ptTranslationBits pt_t + pte_bits = pt_bits pt_t" - by (simp add: bit_simps) - lemma placeNewObject_pte_vs: "ccorresG rf_sr \ dc xfdc (valid_global_refs' and pspace_aligned' and pspace_distinct' diff --git a/proof/crefine/AARCH64/SR_lemmas_C.thy b/proof/crefine/AARCH64/SR_lemmas_C.thy index 7dc1bdc46f..fabcff0a28 100644 --- a/proof/crefine/AARCH64/SR_lemmas_C.thy +++ b/proof/crefine/AARCH64/SR_lemmas_C.thy @@ -2022,6 +2022,44 @@ lemmas ccap_rel_cap_get_tag_cases_arch = lemmas ccap_rel_cap_get_tag_cases_arch' = ccap_rel_cap_get_tag_cases_arch[OF _ refl] +(* Same as cap_get_tag_isCap_unfolded_H_cap, but with an "if" for PageTableCap, so that both cases + match. Replacing cap_get_tag_isCap_unfolded_H_cap woudl be nice, but some existing proofs break + if we do that. Might be possible with additional work. *) +lemma cap_get_tag_isCap_unfolded_H_cap2: + shows "ccap_relation (capability.ThreadCap v0) cap' \ (cap_get_tag cap' = scast cap_thread_cap)" + and "ccap_relation (capability.NullCap) cap' \ (cap_get_tag cap' = scast cap_null_cap)" + and "ccap_relation (capability.NotificationCap v4 v5 v6 v7) cap' \ (cap_get_tag cap' = scast cap_notification_cap) " + and "ccap_relation (capability.EndpointCap v8 v9 v10 v10b v11 v12) cap' \ (cap_get_tag cap' = scast cap_endpoint_cap)" + and "ccap_relation (capability.IRQHandlerCap v13) cap' \ (cap_get_tag cap' = scast cap_irq_handler_cap)" + and "ccap_relation (capability.IRQControlCap) cap' \ (cap_get_tag cap' = scast cap_irq_control_cap)" + and "ccap_relation (capability.Zombie v14 v15 v16) cap' \ (cap_get_tag cap' = scast cap_zombie_cap)" + and "ccap_relation (capability.ReplyCap v17 v18 vr18b) cap' \ (cap_get_tag cap' = scast cap_reply_cap)" + and "ccap_relation (capability.UntypedCap v100 v19 v20 v20b) cap' \ (cap_get_tag cap' = scast cap_untyped_cap)" + and "ccap_relation (capability.CNodeCap v21 v22 v23 v24) cap' \ (cap_get_tag cap' = scast cap_cnode_cap)" + and "ccap_relation (capability.DomainCap) cap' \ (cap_get_tag cap' = scast cap_domain_cap)" + + and "ccap_relation (capability.ArchObjectCap arch_capability.ASIDControlCap) cap' \ (cap_get_tag cap' = scast cap_asid_control_cap)" + and "ccap_relation (capability.ArchObjectCap (arch_capability.ASIDPoolCap v28 v29)) cap' \ (cap_get_tag cap' = scast cap_asid_pool_cap)" + and "ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap v30 v32 v31)) cap' + \ if v32 = VSRootPT_T + then cap_get_tag cap' = scast cap_vspace_cap + else cap_get_tag cap' = scast cap_page_table_cap" + and "ccap_relation (capability.ArchObjectCap (arch_capability.FrameCap v101 v44 v45 v46 v47)) cap' \ (cap_get_tag cap' = scast cap_frame_cap)" + and "ccap_relation (capability.ArchObjectCap (arch_capability.VCPUCap v48)) cap' \ (cap_get_tag cap' = scast cap_vcpu_cap)" + apply (simp add: cap_get_tag_isCap cap_get_tag_isCap_ArchObject isCap_simps) + apply (frule cap_get_tag_isCap(2), simp) + apply (clarsimp simp: cap_get_tag_isCap cap_get_tag_isCap_ArchObject isCap_simps + split: if_splits pt_type.splits)+ + done + +lemmas ccap_rel_cap_get_tag_cases_arch2 = + cap_get_tag_isCap_unfolded_H_cap2(12-16) + [OF back_subst[of "\cap. ccap_relation (ArchObjectCap cap) cap'" for cap'], + OF back_subst[of "\cap. ccap_relation cap cap'" for cap']] + +lemmas ccap_rel_cap_get_tag_cases_arch2' = + ccap_rel_cap_get_tag_cases_arch2[OF _ refl] + lemmas cap_lift_defs = cap_untyped_cap_lift_def cap_endpoint_cap_lift_def @@ -2143,31 +2181,6 @@ lemma pt_array_map_relation_pt: apply (clarsimp simp: h_t_valid_def h_t_array_valid_def typ_uinfo_array_tag_n_m_eq bit_simps) done -lemma page_table_pte_at': (* FIXME AARCH64: move *) - "page_table_at' pt_t p s \ pte_at' p s" - apply (clarsimp simp: page_table_at'_def) - apply (erule_tac x=0 in allE) - apply simp - done - -lemma pte_at_ko': (* FIXME AARCH64: move *) - "pte_at' p s \ \pte. ko_at' (pte::pte) p s" - apply (clarsimp simp: typ_at'_def obj_at'_def ko_wp_at'_def) - apply (case_tac ko; simp) - apply (rename_tac arch_kernel_object) - apply (case_tac arch_kernel_object, auto)[1] - done - -lemma aligned_intvl_0: (* FIXME AARCH64: move *) - "\ is_aligned p n; n < LENGTH('a) \ \ (0 \ {p..+2^n}) = (p = 0)" for p::"'a::len word" - apply (rule iffI; clarsimp simp: intvl_def) - apply (drule_tac d="of_nat k" in is_aligned_add_or) - apply (simp add: word_less_nat_alt unat_of_nat order_le_less_trans[rotated]) - apply word_eqI_solve - apply (rule_tac x=0 in exI) - apply simp - done - lemma vspace_at_rf_sr: "\ page_table_at' VSRootPT_T pt s; gsPTTypes (ksArchState s) pt = Some VSRootPT_T; (s, s') \ rf_sr \ @@ -2188,6 +2201,39 @@ lemma vspace_at_rf_sr: apply simp done +lemma ptable_at_rf_sr: + "\ page_table_at' NormalPT_T pt s; gsPTTypes (ksArchState s) pt = Some NormalPT_T; + (s, s') \ rf_sr \ + \ cslift s' (pt_Ptr pt) \ None" + apply (frule rf_sr_cpte_relation) + apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) + apply (drule (1) pt_array_map_relation_pt) + apply (frule page_table_pte_at') + apply (clarsimp dest!: pte_at_ko') + apply (drule (1) cmap_relation_ko_atD) + apply (clarsimp simp: page_table_at'_def) + apply (drule c_guard_clift) + apply (clarsimp simp: c_guard_def c_null_guard_def ptr_aligned_def) + apply (simp add: align_of_def typ_info_array array_tag_def align_td_array_tag) + apply clarsimp + apply (drule aligned_intvl_0, simp) + apply (clarsimp simp: bit_simps intvl_self) + apply simp + done + +lemma asid_pool_at_rf_sr: + "\ko_at' (ASIDPool pool) p s; (s, s') \ rf_sr\ \ + \pool'. cslift s' (ap_Ptr p) = Some pool' \ + casid_pool_relation (ASIDPool pool) pool'" + apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def cpspace_relation_def) + apply (erule (1) cmap_relation_ko_atE) + apply clarsimp + done + +lemma asid_pool_at_c_guard: + "\asid_pool_at' p s; (s, s') \ rf_sr\ \ c_guard (ap_Ptr p)" + by (fastforce intro: typ_heap_simps dest!: asid_pool_at_ko' asid_pool_at_rf_sr) + lemma gsUntypedZeroRanges_rf_sr: "\ (start, end) \ gsUntypedZeroRanges s; (s, s') \ rf_sr \ \ region_actually_is_zero_bytes start (unat ((end + 1) - start)) s'" @@ -2217,15 +2263,6 @@ lemma heap_list_is_zero_mono: apply (case_tac n', simp_all) done -lemma heap_list_h_eq_better: - "\p. \ x \ {p..+q}; heap_list h q p = heap_list h' q p \ - \ h x = h' x" -proof (induct q) - case 0 thus ?case by simp -next - case (Suc n) thus ?case by (force dest: intvl_neq_start) -qed - lemma heap_list_is_zero_mono2: "heap_list_is_zero hmem p n \ {p' ..+ n'} \ {p ..+ n} @@ -2246,11 +2283,17 @@ lemma arch_fault_tag_not_fault_tag_simps [simp]: "(arch_fault_to_fault_tag arch_fault = scast seL4_Fault_UnknownSyscall) = False" by (cases arch_fault ; simp add: seL4_Faults seL4_Arch_Faults)+ -(* FIXME: move *) +lemma pte_at_rf_sr: + "\ko_at' pte p s; (s, s') \ rf_sr\ \ + \pte'. cslift s' (pte_Ptr p) = Some pte' \ cpte_relation pte pte'" + apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def cpspace_relation_def) + apply (erule (1) cmap_relation_ko_atE) + apply clarsimp + done + lemma vcpu_at_rf_sr: "\ko_at' vcpu p s; (s, s') \ rf_sr\ \ - \vcpu'. cslift s' (vcpu_Ptr p) = Some vcpu' \ - cvcpu_relation vcpu vcpu'" + \vcpu'. cslift s' (vcpu_Ptr p) = Some vcpu' \ cvcpu_relation vcpu vcpu'" apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def cpspace_relation_def) apply (erule (1) cmap_relation_ko_atE) apply clarsimp @@ -2373,11 +2416,12 @@ lemma rf_sr_sched_action_relation: by (clarsimp simp: rf_sr_def cstate_relation_def Let_def) lemma canonical_address_tcb_ptr: - "\canonical_address t; is_aligned t tcbBlockSizeBits\ \ - canonical_address (ptr_val (tcb_ptr_to_ctcb_ptr t))" - apply (clarsimp simp: tcb_ptr_to_ctcb_ptr_def) - apply (erule canonical_address_add) - apply (clarsimp simp: objBits_simps' ctcb_offset_defs canonical_bit_def)+ + "\ canonical_address t; is_aligned t tcbBlockSizeBits \ + \ canonical_address (ptr_val (tcb_ptr_to_ctcb_ptr t))" + apply (rule canonical_address_and_maskI) + apply (drule canonical_address_and_maskD) + apply (clarsimp simp: tcb_ptr_to_ctcb_ptr_def canonical_address_range tcbBlockSizeBits_def + ctcb_offset_defs and_mask_plus) done lemma canonical_address_ctcb_ptr: @@ -2411,40 +2455,52 @@ lemma tcb_and_not_mask_canonical: apply simp done -(* FIXME: move up to TypHeap? *) -lemma lift_t_Some_iff: - "lift_t g hrs p = Some v \ hrs_htd hrs, g \\<^sub>t p \ h_val (hrs_mem hrs) p = v" - unfolding hrs_htd_def hrs_mem_def by (cases hrs) (auto simp: lift_t_if) +lemma tcb_ptr_canonical: + "\ pspace_canonical' s; tcb_at' t s \ \ + tcb_Ptr (make_canonical (ptr_val (tcb_ptr_to_ctcb_ptr t))) = tcb_ptr_to_ctcb_ptr t" + apply (frule (1) obj_at'_is_canonical) + apply (drule canonical_address_tcb_ptr) + apply (clarsimp simp: obj_at'_def objBits_simps' split: if_splits) + apply (clarsimp simp: canonical_make_canonical_idem) + done -context - fixes p :: "'a::mem_type ptr" - fixes q :: "'b::c_type ptr" - fixes d g\<^sub>p g\<^sub>q - assumes val_p: "d,g\<^sub>p \\<^sub>t p" - assumes val_q: "d,g\<^sub>q \\<^sub>t q" - assumes disj: "typ_uinfo_t TYPE('a) \\<^sub>t typ_uinfo_t TYPE('b)" -begin +lemma ccap_relation_capASIDBase: + "\ ccap_relation (ArchObjectCap (ASIDPoolCap p asid)) cap \ \ + capASIDBase_CL (cap_asid_pool_cap_lift cap) = asid" + by (clarsimp simp: cap_to_H_def Let_def cap_asid_pool_cap_lift_def + elim!: ccap_relationE + split: cap_CL.splits if_splits) -lemma h_val_heap_same_typ_disj: - "h_val (heap_update p v h) q = h_val h q" - using disj by (auto intro: h_val_heap_same[OF val_p val_q] - simp: tag_disj_def sub_typ_proper_def field_of_t_def typ_tag_lt_def - field_of_def typ_tag_le_def) +lemma ccap_relation_capASIDPool: + "\ ccap_relation (ArchObjectCap (ASIDPoolCap p asid)) cap \ \ + capASIDPool_CL (cap_asid_pool_cap_lift cap) = p" + by (clarsimp simp: cap_to_H_def Let_def cap_asid_pool_cap_lift_def + elim!: ccap_relationE + split: cap_CL.splits if_splits) -lemma h_val_heap_same_hrs_mem_update_typ_disj: - "h_val (hrs_mem (hrs_mem_update (heap_update p v) s)) q = h_val (hrs_mem s) q" - by (simp add: hrs_mem_update h_val_heap_same_typ_disj) +lemma asid_map_get_tag_neq_none[simp]: + "(asid_map_get_tag amap \ scast asid_map_asid_map_none) = + (asid_map_get_tag amap = scast asid_map_asid_map_vspace)" + by (simp add: asid_map_get_tag_def asid_map_tag_defs) -end +lemma asid_map_get_tag_neq_vspace[simp]: + "(asid_map_get_tag amap \ scast asid_map_asid_map_vspace) = + (asid_map_get_tag amap = scast asid_map_asid_map_none)" + by (simp add: asid_map_get_tag_def asid_map_tag_defs) + +lemma asid_map_tags_neq[simp]: + "(scast asid_map_asid_map_vspace :: machine_word) \ scast asid_map_asid_map_none" + "(scast asid_map_asid_map_none :: machine_word) \ scast asid_map_asid_map_vspace" + by (auto simp: asid_map_tag_defs) + +lemma casid_map_relation_None[simp]: + "casid_map_relation None amap = (asid_map_get_tag amap = scast asid_map_asid_map_none)" + by (simp add: casid_map_relation_def asid_map_lift_def Let_def split: option.splits if_splits) -lemmas h_t_valid_nested_fields = - h_t_valid_field[OF h_t_valid_field[OF h_t_valid_field]] - h_t_valid_field[OF h_t_valid_field] - h_t_valid_field +lemma casid_map_relation_None_lift: + "casid_map_relation None v = (asid_map_lift v = Some Asid_map_asid_map_none)" + by (clarsimp simp: casid_map_relation_def split: option.splits asid_map_CL.splits) -lemmas h_t_valid_fields_clift = - h_t_valid_nested_fields[OF h_t_valid_clift] - h_t_valid_clift (* FIXME move and share with other architectures (note: needs locale from C parse) *) abbreviation Basic_heap_update :: diff --git a/proof/crefine/AARCH64/StateRelation_C.thy b/proof/crefine/AARCH64/StateRelation_C.thy index a949af4312..8dfbaef0fd 100644 --- a/proof/crefine/AARCH64/StateRelation_C.thy +++ b/proof/crefine/AARCH64/StateRelation_C.thy @@ -121,9 +121,6 @@ definition cur_vcpu_relation :: at least) armKSVMIDTable in Haskell is armKSHWASIDTable in C *) -(* FIXME AARCH64 move, add vmid_bits_def to relevant bit defs *) -value_type vmid_bits = "size (0::vmid)" - definition carch_state_relation :: "Arch.kernel_state \ globals \ bool" where "carch_state_relation astate cstate \ armKSKernelVSpace astate = armKSKernelVSpace_C \ @@ -257,6 +254,10 @@ fun register_from_H :: "register \ register_idx" where | "register_from_H AARCH64.TPIDR_EL0 = scast Kernel_C.TPIDR_EL0" | "register_from_H AARCH64.TPIDRRO_EL0 = scast Kernel_C.TPIDRRO_EL0" +lemma ELR_EL1_is_NextIP[simp]: + "Kernel_C.ELR_EL1 = Kernel_C.NextIP" + by (simp add: C_register_defs) + definition cregs_relation :: "(MachineTypes.register \ machine_word) \ machine_word[registers_count] \ bool" where @@ -920,7 +921,23 @@ definition definition "ccap_rights_relation cr cr' \ cr = cap_rights_to_H (seL4_CapRights_lift cr')" -lemma (in kernel) syscall_error_to_H_cases_rev: +definition + syscall_from_H :: "syscall \ machine_word" +where + "syscall_from_H c \ case c of + SysSend \ scast Kernel_C.SysSend + | SysNBSend \ scast Kernel_C.SysNBSend + | SysCall \ scast Kernel_C.SysCall + | SysRecv \ scast Kernel_C.SysRecv + | SysReply \ scast Kernel_C.SysReply + | SysReplyRecv \ scast Kernel_C.SysReplyRecv + | SysNBRecv \ scast Kernel_C.SysNBRecv + | SysYield \ scast Kernel_C.SysYield" + +context kernel +begin + +lemma syscall_error_to_H_cases_rev: "\n. syscall_error_to_H e lf = Some (InvalidArgument n) \ syscall_error_C.type_C e = scast seL4_InvalidArgument" "\n. syscall_error_to_H e lf = Some (InvalidCapability n) \ @@ -942,20 +959,7 @@ lemma (in kernel) syscall_error_to_H_cases_rev: by (clarsimp simp: syscall_error_to_H_def syscall_error_type_defs split: if_split_asm)+ -definition - syscall_from_H :: "syscall \ machine_word" -where - "syscall_from_H c \ case c of - SysSend \ scast Kernel_C.SysSend - | SysNBSend \ scast Kernel_C.SysNBSend - | SysCall \ scast Kernel_C.SysCall - | SysRecv \ scast Kernel_C.SysRecv - | SysReply \ scast Kernel_C.SysReply - | SysReplyRecv \ scast Kernel_C.SysReplyRecv - | SysNBRecv \ scast Kernel_C.SysNBRecv - | SysYield \ scast Kernel_C.SysYield" - -lemma (in kernel) cmap_relation_cs_atD: +lemma cmap_relation_cs_atD: "\ cmap_relation as cs addr_fun rel; cs (addr_fun x) = Some y; inj addr_fun \ \ \ko. as x = Some ko \ rel ko y" apply (clarsimp simp: cmap_relation_def) @@ -970,9 +974,11 @@ lemma (in kernel) cmap_relation_cs_atD: apply simp done -definition (in kernel) +definition rf_sr :: "(KernelStateData_H.kernel_state \ cstate) set" where "rf_sr \ {(s, s'). cstate_relation s (globals s')}" end + +end diff --git a/proof/crefine/AARCH64/Syscall_C.thy b/proof/crefine/AARCH64/Syscall_C.thy index 7cb14a79f7..b79464ffd9 100644 --- a/proof/crefine/AARCH64/Syscall_C.thy +++ b/proof/crefine/AARCH64/Syscall_C.thy @@ -1565,20 +1565,6 @@ lemma ucast_maxIRQ_is_not_less: apply (erule notE) using ucast_up_mono by fastforce -(* FIXME AARCH64 move *) -lemma ccorres_return_void_C_Seq: - "ccorres_underlying sr \ r rvxf arrel xf P P' hs X (return_void_C) \ - ccorres_underlying sr \ r rvxf arrel xf P P' hs X (return_void_C ;; Z)" - apply (clarsimp simp: return_void_C_def) - apply (erule ccorres_semantic_equiv0[rotated]) - apply (rule semantic_equivI) - apply (clarsimp simp: exec_assoc[symmetric]) - apply (rule exec_Seq_cong, simp) - apply (rule iffI) - apply (auto elim!:exec_Normal_elim_cases intro: exec.Throw exec.Seq)[1] - apply (auto elim!:exec_Normal_elim_cases intro: exec.Throw) - done - lemma get_gic_vcpu_ctrl_misr_invs'[wp]: "valid invs' (doMachineOp get_gic_vcpu_ctrl_misr) (\_. invs')" by (simp add: get_gic_vcpu_ctrl_misr_def doMachineOp_def split_def select_f_returns | wp)+ diff --git a/proof/crefine/AARCH64/TcbQueue_C.thy b/proof/crefine/AARCH64/TcbQueue_C.thy index 4779ecf855..46f1e3b25c 100644 --- a/proof/crefine/AARCH64/TcbQueue_C.thy +++ b/proof/crefine/AARCH64/TcbQueue_C.thy @@ -204,27 +204,6 @@ proof - finally show ?thesis . qed - -lemma tcb_at_not_NULL: - assumes tat: "tcb_at' t s" - shows "tcb_ptr_to_ctcb_ptr t \ NULL" -proof - assume "tcb_ptr_to_ctcb_ptr t = NULL" - with tat have "tcb_at' (ctcb_ptr_to_tcb_ptr NULL) s" - apply - - apply (erule subst) - apply simp - done - - hence "is_aligned (ctcb_ptr_to_tcb_ptr NULL) tcbBlockSizeBits" - by (rule tcb_aligned') - - moreover have "ctcb_ptr_to_tcb_ptr NULL !! ctcb_size_bits" - unfolding ctcb_ptr_to_tcb_ptr_def ctcb_offset_defs - by simp - ultimately show False by (simp add: is_aligned_nth ctcb_offset_defs objBits_defs) -qed - lemma tcb_queue_relation_not_NULL: assumes tq: "tcb_queue_relation getNext getPrev mp queue qprev qhead" and valid_ep: "\t\set queue. tcb_at' t s" @@ -894,6 +873,80 @@ lemma tcb_queue_relation'_prev_mask: shows "ptr_val (getPrev tcb) && ~~ mask bits = ptr_val (getPrev tcb)" by (rule tcb_queue_relation_prev_mask [OF tcb_queue_relation'_queue_rel], fact+) +lemma tcb_queue_relation_next_canonical: + assumes "tcb_queue_relation getNext getPrev mp queue NULL qhead" + assumes valid_ep: "\t\set queue. tcb_at' t s" + "distinct queue" + "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb" + "tcbp \ set queue" + assumes canon: "pspace_canonical' s" + shows "make_canonical (ptr_val (getNext tcb)) = ptr_val (getNext tcb)" +proof (cases "getNext tcb = NULL") + case True + thus ?thesis by simp +next + case False + hence "ctcb_ptr_to_tcb_ptr (getNext tcb) \ set queue" using assms + by (fastforce dest: tcb_queueD split: if_split_asm) + with valid_ep(1) + have tcb: "tcb_at' (ctcb_ptr_to_tcb_ptr (getNext tcb)) s" .. + with canon + have "canonical_address (ctcb_ptr_to_tcb_ptr (getNext tcb))" + by (simp add: obj_at'_is_canonical) + moreover + have "is_aligned (ctcb_ptr_to_tcb_ptr (getNext tcb)) tcbBlockSizeBits" + using tcb by (rule tcb_aligned') + ultimately + have "canonical_address (ptr_val (getNext tcb))" + by (rule canonical_address_ctcb_ptr) + thus ?thesis + by (simp add: canonical_make_canonical_idem) +qed + +lemma tcb_queue_relation'_next_canonical: + "\ tcb_queue_relation' getNext getPrev mp queue qhead qend; \t\set queue. tcb_at' t s; + distinct queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcbp \ set queue; + pspace_canonical' s\ + \ make_canonical (ptr_val (getNext tcb)) = ptr_val (getNext tcb)" + by (rule tcb_queue_relation_next_canonical [OF tcb_queue_relation'_queue_rel]) + +lemma tcb_queue_relation_prev_canonical: + assumes "tcb_queue_relation getNext getPrev mp queue NULL qhead" + assumes valid_ep: "\t\set queue. tcb_at' t s" + "distinct queue" + "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb" + "tcbp \ set queue" + assumes canon: "pspace_canonical' s" + shows "make_canonical (ptr_val (getPrev tcb)) = ptr_val (getPrev tcb)" +proof (cases "getPrev tcb = NULL") + case True + thus ?thesis by simp +next + case False + hence "ctcb_ptr_to_tcb_ptr (getPrev tcb) \ set queue" using assms + by (fastforce dest: tcb_queueD split: if_split_asm) + with valid_ep(1) + have tcb: "tcb_at' (ctcb_ptr_to_tcb_ptr (getPrev tcb)) s" .. + with canon + have "canonical_address (ctcb_ptr_to_tcb_ptr (getPrev tcb))" + by (simp add: obj_at'_is_canonical) + moreover + have "is_aligned (ctcb_ptr_to_tcb_ptr (getPrev tcb)) tcbBlockSizeBits" + using tcb by (rule tcb_aligned') + ultimately + have "canonical_address (ptr_val (getPrev tcb))" + by (rule canonical_address_ctcb_ptr) + thus ?thesis + by (simp add: canonical_make_canonical_idem) +qed + +lemma tcb_queue_relation'_prev_canonical: + "\ tcb_queue_relation' getNext getPrev mp queue qhead qend; \t\set queue. tcb_at' t s; + distinct queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcbp \ set queue; + pspace_canonical' s\ + \ make_canonical (ptr_val (getPrev tcb)) = ptr_val (getPrev tcb)" + by (rule tcb_queue_relation_prev_canonical [OF tcb_queue_relation'_queue_rel]) + lemma cready_queues_relation_null_queue_ptrs: assumes rel: "cready_queues_relation mp cq aq" and same: "option_map tcb_null_ep_ptrs \ mp' = option_map tcb_null_ep_ptrs \ mp" diff --git a/proof/crefine/AARCH64/Tcb_C.thy b/proof/crefine/AARCH64/Tcb_C.thy index e09f53ce47..c6458eaa9d 100644 --- a/proof/crefine/AARCH64/Tcb_C.thy +++ b/proof/crefine/AARCH64/Tcb_C.thy @@ -533,16 +533,6 @@ lemma threadSet_ipcbuffer_invs: apply (wp threadSet_invs_trivial, simp_all add: inQ_def cong: conj_cong) done -(* FIXME AARCH64 move to SR_Lemmas where the RISCV64 version is *) -lemma canonical_address_tcb_ptr: - "\ canonical_address t; is_aligned t tcbBlockSizeBits \ - \ canonical_address (ptr_val (tcb_ptr_to_ctcb_ptr t))" - apply (rule canonical_address_and_maskI) - apply (drule canonical_address_and_maskD) - apply (clarsimp simp: tcb_ptr_to_ctcb_ptr_def canonical_address_range tcbBlockSizeBits_def - ctcb_offset_defs and_mask_plus) - done - lemma invokeTCB_ThreadControl_ccorres: notes prod.case_cong_weak[cong] shows diff --git a/proof/crefine/AARCH64/VSpace_C.thy b/proof/crefine/AARCH64/VSpace_C.thy index 65153570b3..cbd5fc12ba 100644 --- a/proof/crefine/AARCH64/VSpace_C.thy +++ b/proof/crefine/AARCH64/VSpace_C.thy @@ -464,76 +464,8 @@ lemma getObject_pte_ccorres: apply (clarsimp simp: typ_at'_def obj_at'_def ko_wp_at'_def) done -lemma ptable_at_rf_sr: (* FIXME AARCH64: move to vs version *) - "\ page_table_at' NormalPT_T pt s; gsPTTypes (ksArchState s) pt = Some NormalPT_T; - (s, s') \ rf_sr \ - \ cslift s' (pt_Ptr pt) \ None" - apply (frule rf_sr_cpte_relation) - apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) - apply (drule (1) pt_array_map_relation_pt) - apply (frule page_table_pte_at') - apply (clarsimp dest!: pte_at_ko') - apply (drule (1) cmap_relation_ko_atD) - apply (clarsimp simp: page_table_at'_def) - apply (drule c_guard_clift) - apply (clarsimp simp: c_guard_def c_null_guard_def ptr_aligned_def) - apply (simp add: align_of_def typ_info_array array_tag_def align_td_array_tag) - apply clarsimp - apply (drule aligned_intvl_0, simp) - apply (clarsimp simp: bit_simps intvl_self) - apply simp - done - -lemma array_assertion_abs_pt: (* FIXME AARCH64: move to vs version, rename vspace to vs *) - "\s s'. (s, s') \ rf_sr - \ (page_table_at' NormalPT_T pt s \ gsPTTypes (ksArchState s) pt = Some NormalPT_T) - \ (n s' \ 2 ^ ptTranslationBits NormalPT_T \ (x s' \ 0 \ n s' \ 0)) - \ (x s' = 0 \ array_assertion (pte_Ptr pt) (n s') (hrs_htd (t_hrs_' (globals s'))))" - apply (intro allI impI disjCI2, clarsimp) - apply (drule (2) ptable_at_rf_sr, clarsimp) - apply (erule clift_array_assertion_imp; simp) - apply (rule_tac x=0 in exI, simp add: bit_simps) - done - -lemmas ccorres_move_array_assertion_pt (* FIXME AARCH64: move to vs version, rename vspace to vs *) - = ccorres_move_array_assertions[OF array_assertion_abs_pt] - -lemma array_assertion_abs_pt_gen: (* FIXME AARCH64: move to vs version, rename vspace to vs *) - "\s s'. (s, s') \ rf_sr - \ (page_table_at' pt_t pt s \ gsPTTypes (ksArchState s) pt = Some pt_t) - \ (n s' \ 2 ^ ptTranslationBits pt_t \ (x s' \ 0 \ n s' \ 0)) - \ (x s' = 0 \ array_assertion (pte_Ptr pt) (n s') (hrs_htd (t_hrs_' (globals s'))))" - apply (intro allI impI disjCI2, clarsimp) - apply (cases pt_t; simp) - apply (drule (2) vspace_at_rf_sr, clarsimp) - apply (erule clift_array_assertion_imp; simp) - apply (rule_tac x=0 in exI, simp add: bit_simps Kernel_Config.config_ARM_PA_SIZE_BITS_40_def) - apply (drule (2) ptable_at_rf_sr, clarsimp) - apply (erule clift_array_assertion_imp; simp) - apply (rule_tac x=0 in exI, simp add: bit_simps) - done - -lemmas ccorres_move_array_assertion_pt_gen (* FIXME AARCH64: move to vs version, rename vspace to vs *) - = ccorres_move_array_assertions[OF array_assertion_abs_pt_gen] - lemmas unat_and_mask_le_ptTrans = unat_and_mask_le[OF AARCH64.ptTranslationBits_le_machine_word] -lemma levelType_0[simp]: (* FIXME AARCH64: move *) - "levelType 0 = NormalPT_T" - by (simp add: levelType_def maxPTLevel_def split: if_splits) - -lemma levelType_maxPTLevel[simp]: (* FIXME AARCH64: move *) - "levelType maxPTLevel = VSRootPT_T" - by (simp add: levelType_def) - -lemma pte_at_rf_sr: (* FIXME AARCH64: move *) - "\ko_at' pte p s; (s, s') \ rf_sr\ \ - \pte'. cslift s' (pte_Ptr p) = Some pte' \ cpte_relation pte pte'" - apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def cpspace_relation_def) - apply (erule (1) cmap_relation_ko_atE) - apply clarsimp - done - definition mask_ptTranslationBits :: "pt_type \ machine_word" where "mask_ptTranslationBits pt_t \ mask (ptTranslationBits pt_t)" @@ -734,12 +666,6 @@ proof (induct level arbitrary: pt) done qed -(* FIXME AARCH64: move to Wellformed_C with comment why it is not in Refine/higher (concrete value - should only be used for C) *) -schematic_goal maxPTLevel_val: - "maxPTLevel = numeral ?n" - by (simp add: maxPTLevel_def Kernel_Config.config_ARM_PA_SIZE_BITS_40_def) - lemma lookupPTSlot_ccorres: "ccorres (\(bitsLeft,ptSlot) cr. bitsLeft = unat (ptBitsLeft_C cr) \ ptSlot_C cr = Ptr ptSlot) ret__struct_lookupPTSlot_ret_C_' @@ -853,21 +779,6 @@ lemma getPoolPtr_ccorres: apply simp done -(* FIXME AARCH64 move *) -lemma asid_pool_at_ko'_eq: - "(\ap :: asidpool. ko_at' ap p s) = asid_pool_at' p s" - apply (rule iffI) - apply (clarsimp simp: typ_at'_def obj_at'_def ko_wp_at'_def) - apply (clarsimp simp: typ_at'_def obj_at'_def ko_wp_at'_def) - apply (case_tac ko, auto) - apply (rename_tac arch_kernel_object) - apply (case_tac arch_kernel_object, auto)[1] - done - -lemma casid_map_relation_None: - "casid_map_relation None v = (asid_map_lift v = Some Asid_map_asid_map_none)" - by (clarsimp simp: casid_map_relation_def split: option.splits asid_map_CL.splits) - lemma findMapForASID_ccorres: "ccorres casid_map_relation ret__struct_asid_map_C_' (valid_arch_state' and K (asid_wf asid)) @@ -894,7 +805,8 @@ lemma findMapForASID_ccorres: apply (rename_tac pool) apply (rule ccorres_return_C; clarsimp) apply (wpsimp simp: asid_pool_at_ko'_eq getPoolPtr_def) - apply (clarsimp simp: casid_map_relation_None typ_heap_simps asid_map_lift_def) + apply (clarsimp simp: casid_map_relation_None_lift typ_heap_simps asid_map_lift_def + simp del: casid_map_relation_None) apply (clarsimp simp: casid_pool_relation_def split: asid_pool_C.splits) apply (fastforce simp: word_and_le1 array_relation_def mask_2pm1[symmetric]) apply (clarsimp simp: asid_wf_table_guard valid_arch_state'_def valid_asid_table'_def ran_def) @@ -988,46 +900,6 @@ end context kernel_m begin -(* FIXME AARCH64: move *) -lemma ccorres_h_t_valid_armKSGlobalUserVSpace: - "ccorres r xf P P' hs f (f' ;; g') \ - ccorres r xf P P' hs f (Guard C_Guard {s'. s' \\<^sub>c armKSGlobalUserVSpace_Ptr} f';; g')" - apply (rule ccorres_guard_imp2) - apply (rule ccorres_move_c_guards[where P = \]) - apply clarsimp - apply assumption - apply simp - by (clarsimp simp add: rf_sr_def cstate_relation_def Let_def) - -(* FIXME AARCH64: MOVE copied from CSpace_RAB_C; also in other arches *) -lemma ccorres_gen_asm_state: - assumes rl: "\s. P s \ ccorres r xf G G' hs a c" - shows "ccorres r xf (G and P) G' hs a c" -proof (rule ccorres_guard_imp2) - show "ccorres r xf (G and (\_. \s. P s)) G' hs a c" - apply (rule ccorres_gen_asm) - apply (erule exE) - apply (erule rl) - done -next - fix s s' - assume "(s, s') \ rf_sr" and "(G and P) s" and "s' \ G'" - thus "(G and (\_. \s. P s)) s \ s' \ G'" - by fastforce -qed - -(* FIXME AARCH64: move, duplicates in Ipc_C and Tcb_C; also other arches *) -lemma ccorres_abstract_known: - "\ \rv' t t'. ceqv \ xf' rv' t t' g (g' rv'); ccorres rvr xf P P' hs f (g' val) \ - \ ccorres rvr xf P (P' \ {s. xf' s = val}) hs f g" - apply (rule ccorres_guard_imp2) - apply (rule_tac xf'=xf' in ccorres_abstract) - apply assumption - apply (rule_tac P="rv' = val" in ccorres_gen_asm2) - apply simp - apply simp - done - lemma isValidVTableRoot_def2: "isValidVTableRoot cap = (\pt asid vref. cap = ArchObjectCap (PageTableCap pt VSRootPT_T (Some (asid,vref))))" @@ -1142,33 +1014,6 @@ lemma ccorres_pre_gets_armKSNextVMID_ksArchState: apply clarsimp done -(* FIXME AARCH64: move *) -lemma asid_pool_at_rf_sr: - "\ko_at' (ASIDPool pool) p s; (s, s') \ rf_sr\ \ - \pool'. cslift s' (ap_Ptr p) = Some pool' \ - casid_pool_relation (ASIDPool pool) pool'" - apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def cpspace_relation_def) - apply (erule (1) cmap_relation_ko_atE) - apply clarsimp - done - -(* FIXME AARCH64: move *) -lemma asid_pool_at_ko: - "asid_pool_at' p s \ \pool. ko_at' (ASIDPool pool) p s" - apply (clarsimp simp: typ_at'_def obj_at'_def ko_wp_at'_def) - apply (case_tac ko, auto) - apply (rename_tac arch_kernel_object) - apply (case_tac arch_kernel_object, auto)[1] - apply (rename_tac asidpool) - apply (case_tac asidpool, auto)[1] - done - -(* FIXME AARCH64: move *) -lemma asid_pool_at_c_guard: - "\asid_pool_at' p s; (s, s') \ rf_sr\ \ c_guard (ap_Ptr p)" - by (fastforce intro: typ_heap_simps dest!: asid_pool_at_ko asid_pool_at_rf_sr) - -(* FIXME AARCH64: move *) lemma setObjectASID_Basic_ccorres: "ccorres dc xfdc \ {s. f s = p \ casid_pool_relation pool (asid_pool_C.asid_pool_C (pool' s))} hs (setObject p pool) @@ -1554,27 +1399,6 @@ lemma getHWASID_ccorres: split: if_split) done -(* FIXME AARCH64: move up, try to make the 48 less magic *) -lemma canonical_address_and_maskD: - "canonical_address p \ p && mask 48 = p" - apply (simp add: word_and_mask_shiftl pageBits_def canonical_address_range canonical_bit_def) - apply word_eqI - apply fastforce - done - -(* FIXME AARCH64: move up, try to make the 48 less magic *) -lemma canonical_address_and_maskI: - "p && mask 48 = p \ canonical_address p" - by (simp add: word_and_mask_shiftl pageBits_def canonical_address_range canonical_bit_def - and_mask_eq_iff_le_mask) - - -lemma addrFromPPtr_canonical_in_kernel_window: - "\ pptrBase \ p; p < pptrTop \ \ canonical_address (addrFromPPtr p)" - apply (simp add: addrFromPPtr_def pptrBaseOffset_def paddrBase_def canonical_address_mask_eq - canonical_bit_def pptrBase_def pageBits_def pptrTop_def) - by word_bitwise clarsimp - lemma armv_contextSwitch_ccorres: "ccorres dc xfdc (valid_arch_state' and @@ -1701,14 +1525,6 @@ lemma setVMRoot_ccorres: elim!: ccap_relationE split: if_split_asm cap_CL.splits) -lemma pptrBaseOffset_cacheLineSize_aligned[simp]: (* FIXME AARCH64: move *) - "pptrBaseOffset && mask cacheLineSize = 0" - by (simp add: pptrBaseOffset_def paddrBase_def pptrBase_def cacheLineSize_def mask_def) - -lemma ptrFromPAddr_mask_cacheLineSize[simp]: (* FIXME AARCH64: move *) - "ptrFromPAddr v && mask cacheLineSize = v && mask cacheLineSize" - by (simp add: ptrFromPAddr_def add_mask_ignore) - (* FIXME: move *) lemma register_from_H_bound[simp]: "unat (register_from_H v) < 37" @@ -2130,57 +1946,6 @@ lemma performPageInvocationUnmap_ccorres: c_valid_cap_def cl_valid_cap_def wellformed_mapdata'_def) done -(* FIXME AARCH64 incorporate whichever of these are needed (from RISCV64 and ARM_HYP), remove rest - -lemma RISCVGetWriteFromVMRights_spec: - "\s. \ \ \s. \vm_rights < 4 \ \vm_rights \ 0\ Call ArmGetWriteFromVMRights_'proc - \ \ret__unsigned_long = writable_from_vm_rights (vmrights_to_H \<^bsup>s\<^esup>vm_rights) \" - supply if_cong[cong] - apply vcg - apply (simp add: vmrights_to_H_def writable_from_vm_rights_def Kernel_C.VMKernelOnly_def - Kernel_C.VMReadOnly_def Kernel_C.VMReadWrite_def) - apply (drule word_less_cases, auto)+ - done - -lemma RISCVGetReadFromVMRights_spec: - "\s. \ \ \s. \vm_rights < 4 \ \vm_rights \ 0\ Call RISCVGetReadFromVMRights_'proc - \ \ret__unsigned_long = readable_from_vm_rights (vmrights_to_H \<^bsup>s\<^esup>vm_rights) \" - supply if_cong[cong] - apply vcg - apply (simp add: vmrights_to_H_def readable_from_vm_rights_def Kernel_C.VMKernelOnly_def - Kernel_C.VMReadOnly_def Kernel_C.VMReadWrite_def) - apply (drule word_less_cases, auto)+ - done - -lemma writable_from_vm_rights_mask: - "(writable_from_vm_rights R) && 1 = (writable_from_vm_rights R :: machine_word)" - by (simp add: writable_from_vm_rights_def split: vmrights.splits) - -lemma readable_from_vm_rights_mask: - "(readable_from_vm_rights R) && 1 = (readable_from_vm_rights R :: machine_word)" - by (simp add: readable_from_vm_rights_def split: vmrights.splits) - -lemma user_from_vm_rights_mask: - "user_from_vm_rights R && 1 = (user_from_vm_rights R :: machine_word)" - by (simp add: user_from_vm_rights_def split: vmrights.splits) - -lemma HAPFromVMRights_spec: - "\s. \ \ \s. \vm_rights < 4\ Call HAPFromVMRights_'proc - \ \ret__unsigned_long = hap_from_vm_rights (vmrights_to_H \<^bsup>s\<^esup>vm_rights) \" - apply vcg - apply (simp add: vmrights_to_H_def hap_from_vm_rights_def - Kernel_C.VMNoAccess_def Kernel_C.VMKernelOnly_def - Kernel_C.VMReadOnly_def Kernel_C.VMReadWrite_def) - apply clarsimp - apply (drule word_less_cases, auto)+ - done - -lemma hap_from_vm_rights_mask: - "hap_from_vm_rights R && 3 = (hap_from_vm_rights R :: word32)" - by (simp add: hap_from_vm_rights_def split: vmrights.splits) - -*) - lemma APFromVMRights_spec: "\s. \ \ \s. \vm_rights < 4 \ \vm_rights \ 2 \ Call APFromVMRights_'proc \ \ret__unsigned_long = ap_from_vm_rights (vmrights_to_H \<^bsup>s\<^esup>vm_rights) \" @@ -2323,10 +2088,6 @@ lemma page_table_at'_array_assertion: using assms by (fastforce intro: array_assertion_abs_vspace[where x="\_. (1::nat)", simplified, rule_format]) -lemma isVTableRoot_ex: - "isVTableRoot cap = (\p m. cap = ArchObjectCap (PageTableCap p VSRootPT_T m))" - by (simp add: isVTableRoot_def split: capability.splits arch_capability.splits pt_type.splits) - lemma cap_lift_VSCap_Base: "\ cap_to_H cap_cl = ArchObjectCap (PageTableCap p VSRootPT_T asid); cap_lift cap_c = Some cap_cl \ @@ -2425,12 +2186,11 @@ lemma ccap_relation_vspace_mapped_asid: by (frule cap_get_tag_isCap_unfolded_H_cap) (clarsimp simp: cap_vspace_cap_lift ccap_relation_def cap_to_H_def split: if_splits) -(* FIXME AARCH64 potentially unused *) -lemma ccap_relation_page_table_mapped_asid: - "ccap_relation (ArchObjectCap (PageTableCap p NormalPT_T (Some (asid, vspace)))) cap - \ asid = capPTMappedASID_CL (cap_page_table_cap_lift cap)" +lemma ccap_relation_vspace_base: + "ccap_relation (ArchObjectCap (PageTableCap p VSRootPT_T m)) cap + \ capVSBasePtr_CL (cap_vspace_cap_lift cap) = p" by (frule cap_get_tag_isCap_unfolded_H_cap) - (clarsimp simp: cap_page_table_cap_lift ccap_relation_def cap_to_H_def split: if_splits) + (clarsimp simp: cap_vspace_cap_lift ccap_relation_def cap_to_H_def split: if_splits) lemma performPageTableInvocationMap_ccorres: "ccorres (K (K \) \ dc) (liftxf errstate id (K ()) ret__unsigned_long_') @@ -2461,7 +2221,7 @@ lemma performPageTableInvocationMap_ccorres: (* FIXME AARCH64 VCPU/HYP related block (everything from VSpace_C on ARM_HYP) adapted to AARCH64 some of these might be needed earlier *) -(* FIXME AARCH64 move, potentially to a VCPU theory +(* FIXME AARCH64: potentially put this into a VCPU theory if we try move most of the VCPU lemmas into a VCPU theory, some might need items in this or later theories, meaning we'd need a VCPU low (maybe put into ArchAcc?) and VCPU high theory *) @@ -2486,7 +2246,6 @@ lemma vcpu_hrs_mem_update_helper: apply simp done -(* FIXME AARCH64 move *) lemmas setObject_ccorres_helper_vcpu = setObject_ccorres_helper[where 'a=vcpu, simplified objBits_simps vcpuBits_def, simplified] diff --git a/proof/crefine/AARCH64/Wellformed_C.thy b/proof/crefine/AARCH64/Wellformed_C.thy index efacfd9a1c..8847b542c0 100644 --- a/proof/crefine/AARCH64/Wellformed_C.thy +++ b/proof/crefine/AARCH64/Wellformed_C.thy @@ -17,12 +17,13 @@ begin context begin interpretation Arch . (*FIXME: arch_split*) -(* FIXME AARCH64: this could also go into Invariants_H *) (* Takes an address and ensures it can be given to a function expecting a canonical address. Canonical addresses on 64-bit machines aren't really 64-bit, due to bus sizes. Hence, structures used by the bitfield generator will use packed addresses, resulting in this mask in the C code on AARCH64 (which would be a cast plus sign-extension on X64 and RISCV64). - For our spec rules, it's better to wrap the magic numbers if possible. *) + For our spec rules, it's better to wrap the magic numbers if possible. + + Dependency-wise this could also go into Invariants_H, but we want to limit its use to CRefine. *) definition make_canonical :: "machine_word \ machine_word" where "make_canonical p \ p && mask (Suc canonical_bit)" @@ -636,11 +637,49 @@ where definition cacheLineSize :: nat where "cacheLineSize \ 6" +lemma addrFromPPtr_mask_cacheLineSize: + "addrFromPPtr ptr && mask cacheLineSize = ptr && mask cacheLineSize" + apply (simp add: addrFromPPtr_def AARCH64.pptrBase_def pptrBaseOffset_def canonical_bit_def + paddrBase_def cacheLineSize_def mask_def) + apply word_bitwise + done + +lemma pptrBaseOffset_cacheLineSize_aligned[simp]: + "pptrBaseOffset && mask cacheLineSize = 0" + by (simp add: pptrBaseOffset_def paddrBase_def pptrBase_def cacheLineSize_def mask_def) + +lemma ptrFromPAddr_mask_cacheLineSize[simp]: + "ptrFromPAddr v && mask cacheLineSize = v && mask cacheLineSize" + by (simp add: ptrFromPAddr_def add_mask_ignore) + (* The magic 4 comes out of the bitfield generator -- this applies to all versions of the kernel. *) lemma ThreadState_Restart_mask[simp]: "(scast ThreadState_Restart::machine_word) && mask 4 = scast ThreadState_Restart" by (simp add: ThreadState_Restart_def mask_def) +lemma aligned_tcb_ctcb_not_NULL: + assumes "is_aligned p tcbBlockSizeBits" + shows "tcb_ptr_to_ctcb_ptr p \ NULL" +proof + assume "tcb_ptr_to_ctcb_ptr p = NULL" + hence "p + ctcb_offset = 0" + by (simp add: tcb_ptr_to_ctcb_ptr_def) + moreover + from `is_aligned p tcbBlockSizeBits` + have "p + ctcb_offset = p || ctcb_offset" + by (rule word_and_or_mask_aligned) (simp add: ctcb_offset_defs objBits_defs mask_def) + moreover + have "ctcb_offset !! ctcb_size_bits" + by (simp add: ctcb_offset_defs objBits_defs) + ultimately + show False + by (simp add: bang_eq) +qed + +lemma tcb_at_not_NULL: + "tcb_at' t s \ tcb_ptr_to_ctcb_ptr t \ NULL" + by (rule aligned_tcb_ctcb_not_NULL) (rule tcb_aligned') + (* generic lemmas with arch-specific consequences *) schematic_goal size_gpRegisters: @@ -657,6 +696,12 @@ schematic_goal size_frameRegisters: AARCH64.frameRegisters_def) (simp add: Suc_eq_plus1) +(* Could live in Refine, but we want to make sure this is only used in CRefine. Before CRefine + the numeral value should never be stated explicitly. *) +schematic_goal maxPTLevel_val: + "maxPTLevel = numeral ?n" + by (simp add: maxPTLevel_def Kernel_Config.config_ARM_PA_SIZE_BITS_40_def) + end end diff --git a/proof/crefine/lib/Corres_C.thy b/proof/crefine/lib/Corres_C.thy index b3dc183795..179fa1d7f6 100644 --- a/proof/crefine/lib/Corres_C.thy +++ b/proof/crefine/lib/Corres_C.thy @@ -10,6 +10,55 @@ imports SR_lemmas_C begin +(* FIXME AARCH64: move up to CCorres_UL begin *) +(* check RISCV for duplicates *) + +(* note: moving this lemma outside of kernel_m locale currently causes some proofs to fail *) +lemma ccorres_cases: + assumes "P \ ccorres_underlying srel Ga rrel xf arrel axf G G' hs a b" + assumes "\P \ ccorres_underlying srel Ga rrel xf arrel axf H H' hs a b" + shows "ccorres_underlying srel Ga rrel xf arrel axf + (\s. (P \ G s) \ (\P \ H s)) + ({s. P \ s \ G'} \ {s. \P \ s \ H'}) hs + a b" + by (cases P, auto simp: assms) + +lemma ccorres_dc_comp: + "ccorres_underlying srel G (dc \ R) xf P P' hs m c = ccorres_underlying srel G dc xf P P' hs m c" + by simp + +(* FIXME AARCH64: remove from CSpace_RAB_C; also in other arches *) +lemma ccorres_gen_asm_state: + assumes rl: "\s. P s \ ccorres_underlying srel Ga r xf arrel axf G G' hs a c" + shows "ccorres_underlying srel Ga r xf arrel axf (G and P) G' hs a c" +proof (rule ccorres_guard_imp2) + show "ccorres_underlying srel Ga r xf arrel axf (G and (\_. \s. P s)) G' hs a c" + apply (rule ccorres_gen_asm) + apply (erule exE) + apply (erule rl) + done +next + fix s s' + assume "(s, s') \ srel" and "(G and P) s" and "s' \ G'" + thus "(G and (\_. \s. P s)) s \ s' \ G'" + by fastforce +qed + +(* FIXME AARCH64: duplicates in Ipc_C and Tcb_C; also other arches *) +lemma ccorres_abstract_known: + "\ \rv' t t'. ceqv \ xf' rv' t t' g (g' rv'); + ccorres_underlying srel \ rvr xf arel axf P P' hs f (g' val) \ + \ ccorres_underlying srel \ rvr xf arel axf P (P' \ {s. xf' s = val}) hs f g" + apply (rule ccorres_guard_imp2) + apply (rule_tac xf'=xf' in ccorres_abstract) + apply assumption + apply (rule_tac P="rv' = val" in ccorres_gen_asm2) + apply simp + apply simp + done + +(* move up to CCorres_UL end *) + abbreviation "return_C \ CLanguage.creturn global_exn_var_'_update" lemmas return_C_def = creturn_def @@ -286,10 +335,22 @@ lemma ccorres_return_C_errorE': apply simp done +lemma ccorres_return_void_C_Seq: + "ccorres_underlying sr \ r rvxf arrel xf P P' hs X return_void_C \ + ccorres_underlying sr \ r rvxf arrel xf P P' hs X (return_void_C ;; Z)" + apply (clarsimp simp: return_void_C_def) + apply (erule ccorres_semantic_equiv0[rotated]) + apply (rule semantic_equivI) + apply (clarsimp simp: exec_assoc[symmetric]) + apply (rule exec_Seq_cong, simp) + apply (rule iffI) + apply (auto elim!:exec_Normal_elim_cases intro: exec.Throw exec.Seq)[1] + apply (auto elim!:exec_Normal_elim_cases intro: exec.Throw) + done + context kernel begin - abbreviation "ccorres r xf \ ccorres_underlying rf_sr \ r xf r xf"