From 503069e6a5e3b237abab2b20a0c6e3650a76a108 Mon Sep 17 00:00:00 2001 From: Corey Lewis Date: Tue, 19 Nov 2024 12:42:24 +1100 Subject: [PATCH] rt trivial: rename arch_split -> arch-split again after merge Signed-off-by: Corey Lewis --- .../AARCH64/ArchRetype_AI.thy | 2 +- proof/invariant-abstract/CSpaceInvPre_AI.thy | 2 +- proof/refine/ARM/ArchAcc_R.thy | 2 +- proof/refine/ARM/CNodeInv_R.thy | 8 ++++---- proof/refine/ARM/CSpace1_R.thy | 2 +- proof/refine/ARM/Detype_R.thy | 6 +++--- proof/refine/ARM/Finalise_R.thy | 16 ++++++++-------- proof/refine/ARM/IpcCancel_R.thy | 2 +- proof/refine/ARM/Ipc_R.thy | 18 +++++++++--------- proof/refine/ARM/KHeap_R.thy | 14 +++++++------- proof/refine/ARM/SchedContextInv_R.thy | 2 +- proof/refine/ARM/SchedContext_R.thy | 4 ++-- proof/refine/ARM/Schedule_R.thy | 2 +- proof/refine/ARM/Syscall_R.thy | 4 ++-- proof/refine/ARM/TcbAcc_R.thy | 4 ++-- proof/refine/ARM/Tcb_R.thy | 2 +- proof/refine/ARM/Untyped_R.thy | 2 +- proof/refine/ARM/VSpace_R.thy | 10 +++++----- proof/refine/RISCV64/ArchAcc_R.thy | 4 ++-- proof/refine/RISCV64/CNodeInv_R.thy | 8 ++++---- proof/refine/RISCV64/CSpace1_R.thy | 2 +- proof/refine/RISCV64/Detype_R.thy | 4 ++-- proof/refine/RISCV64/Finalise_R.thy | 14 +++++++------- proof/refine/RISCV64/IpcCancel_R.thy | 2 +- proof/refine/RISCV64/Ipc_R.thy | 18 +++++++++--------- proof/refine/RISCV64/KHeap_R.thy | 12 ++++++------ proof/refine/RISCV64/LevityCatch.thy | 4 ++-- proof/refine/RISCV64/SchedContextInv_R.thy | 2 +- proof/refine/RISCV64/SchedContext_R.thy | 4 ++-- proof/refine/RISCV64/Schedule_R.thy | 2 +- proof/refine/RISCV64/Syscall_R.thy | 4 ++-- proof/refine/RISCV64/TcbAcc_R.thy | 4 ++-- proof/refine/RISCV64/Tcb_R.thy | 2 +- proof/refine/RISCV64/Untyped_R.thy | 2 +- proof/refine/RISCV64/VSpace_R.thy | 2 +- 35 files changed, 96 insertions(+), 96 deletions(-) diff --git a/proof/invariant-abstract/AARCH64/ArchRetype_AI.thy b/proof/invariant-abstract/AARCH64/ArchRetype_AI.thy index eaa296e016..2312ee018f 100644 --- a/proof/invariant-abstract/AARCH64/ArchRetype_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchRetype_AI.thy @@ -268,7 +268,7 @@ locale retype_region_proofs_arch context retype_region_proofs begin -(* FIXME arch_split: is there any way to optimise this interpretation out? we can't nest contexts *) +(* FIXME arch-split: is there any way to optimise this interpretation out? we can't nest contexts *) interpretation Arch . lemma valid_cap: diff --git a/proof/invariant-abstract/CSpaceInvPre_AI.thy b/proof/invariant-abstract/CSpaceInvPre_AI.thy index f106a48467..8e810f0b8f 100644 --- a/proof/invariant-abstract/CSpaceInvPre_AI.thy +++ b/proof/invariant-abstract/CSpaceInvPre_AI.thy @@ -139,7 +139,7 @@ lemma empty_table_caps_of: "empty_table S ko \ caps_of ko = {}" by (cases ko, simp_all add: empty_table_def caps_of_def cap_of_def) -(* FIXME arch_split: exports properties of functions that are not necessarily in global context, +(* FIXME arch-split: exports properties of functions that are not necessarily in global context, and then they get placed in the global simpset *) lemma (in Arch) free_index_update_test_function_stuff[simp]: "cap_asid (src_cap\free_index := a\) = cap_asid src_cap" diff --git a/proof/refine/ARM/ArchAcc_R.thy b/proof/refine/ARM/ArchAcc_R.thy index d549a36961..c65929564c 100644 --- a/proof/refine/ARM/ArchAcc_R.thy +++ b/proof/refine/ARM/ArchAcc_R.thy @@ -1189,7 +1189,7 @@ end sublocale Arch < copyGlobalMappings: typ_at_all_props' "copyGlobalMappings newPD" by typ_at_props' -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma arch_cap_rights_update: "acap_relation c c' \ diff --git a/proof/refine/ARM/CNodeInv_R.thy b/proof/refine/ARM/CNodeInv_R.thy index 2977be6ced..827877ebf7 100644 --- a/proof/refine/ARM/CNodeInv_R.thy +++ b/proof/refine/ARM/CNodeInv_R.thy @@ -6512,7 +6512,7 @@ lemma cteDelete_sch_act_simple: apply simp+ done -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) crunch "Arch.finaliseCap", unbindMaybeNotification, prepareThreadDelete, schedContextMaybeUnbindNtfn, cleanReply @@ -6880,7 +6880,7 @@ lemmas rec_del_concrete_unfold = rec_del_concrete.simps red_zombie_will_fail.simps if_True if_False ball_simps simp_thms -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma cap_relation_removables: "\ cap_relation cap cap'; isNullCap cap' \ isZombie cap'; @@ -6945,7 +6945,7 @@ lemmas finaliseSlot_typ_ats[wp] = typ_at_lifts[OF finaliseSlot_typ_at'] lemmas rec_del_valid_list_irq_state_independent[wp] = rec_del_preservation[OF cap_swap_for_delete_valid_list set_cap_valid_list empty_slot_valid_list finalise_cap_valid_list preemption_point_valid_list] -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma rec_del_corres: "\C \ rec_del_concrete args. @@ -8631,7 +8631,7 @@ lemmas finalise_slot_corres' simplified, folded finalise_slot_def] for slot exp lemmas finalise_slot_corres = use_spec_corres [OF finalise_slot_corres'] -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma cap_relation_same: "\ cap_relation cap cap'; cap_relation cap cap'' \ diff --git a/proof/refine/ARM/CSpace1_R.thy b/proof/refine/ARM/CSpace1_R.thy index 84b71b0c0c..54caa6daa6 100644 --- a/proof/refine/ARM/CSpace1_R.thy +++ b/proof/refine/ARM/CSpace1_R.thy @@ -926,7 +926,7 @@ abbreviation abbreviation "revokable' a b \ global.isCapRevocable b a" -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) declare arch_is_cap_revocable_def[simp] ARM_H.isCapRevocable_def[simp] diff --git a/proof/refine/ARM/Detype_R.thy b/proof/refine/ARM/Detype_R.thy index dee418e312..0bb16e10c2 100644 --- a/proof/refine/ARM/Detype_R.thy +++ b/proof/refine/ARM/Detype_R.thy @@ -448,7 +448,7 @@ end locale detype_locale' = detype_locale + constrains s::"det_state" -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) text \Invariant preservation across concrete deletion\ @@ -503,7 +503,7 @@ locale delete_locale = context delete_locale begin -interpretation Arch . (*FIXME: arch_split*) +interpretation Arch . (*FIXME: arch-split*) lemma valid_objs: "valid_objs' s'" and vreplies: "valid_replies' s'" and pspace: "valid_pspace' s'" @@ -717,7 +717,7 @@ lemma deletionIsSafe_holds: and vu: "valid_untyped (cap.UntypedCap d base bits idx) s" shows "deletionIsSafe base bits s'" proof - - interpret Arch . (* FIXME: arch_split *) + interpret Arch . (* FIXME: arch-split *) have arch: "\ ko p. \ ksPSpace s' p = Some (KOArch ko); p \ {base..base + 2 ^ bits - 1} \ \ 6 \ bits" diff --git a/proof/refine/ARM/Finalise_R.thy b/proof/refine/ARM/Finalise_R.thy index 6504e323f0..4944bb81c8 100644 --- a/proof/refine/ARM/Finalise_R.thy +++ b/proof/refine/ARM/Finalise_R.thy @@ -72,7 +72,7 @@ crunch clearUntypedFreeIndex global_interpretation clearUntypedFreeIndex: typ_at_all_props' "clearUntypedFreeIndex slot" by typ_at_props' -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) crunch postCapDeletion for tcb_at'[wp]: "tcb_at' t" @@ -2181,7 +2181,7 @@ lemma finaliseCap_cases[wp]: apply (auto simp add: isCap_simps cap_has_cleanup'_def) done -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) crunch finaliseCap for aligned'[wp]: "pspace_aligned'" @@ -2332,7 +2332,7 @@ crunch replyRemove and pspace_bounded'[wp]: pspace_bounded' (simp: crunch_simps) -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) crunch replyRemove, handleFaultReply for ex_nonz_cap_to'[wp]: "ex_nonz_cap_to' ptr" @@ -2756,7 +2756,7 @@ lemma finaliseCap_True_invs'[wp]: apply clarsimp done -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) crunch flushSpace for invs'[wp]: "invs'" (ignore: doMachineOp) @@ -2823,7 +2823,7 @@ end sublocale Arch < flushSpace: typ_at_all_props' "flushSpace asid" by typ_at_props' -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma deleteASID_invs'[wp]: "\invs'\ deleteASID asid pd \\rv. invs'\" @@ -4277,7 +4277,7 @@ lemma finaliseCap_cte_cap_wp_to[wp]: global_interpretation unbindNotification: typ_at_all_props' "unbindNotification tcb" by typ_at_props' -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma finaliseCap_valid_cap[wp]: "\valid_cap' cap\ finaliseCap cap final flag \\rv. valid_cap' (fst rv)\" @@ -4920,7 +4920,7 @@ lemma can_fast_finalise_finaliseCap: = do finaliseCap cap final True; return (NullCap, NullCap) od" by (cases cap; simp add: finaliseCap_def isCap_simps) -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma finaliseCap_corres: "\ final_matters' cap' \ final = final'; cap_relation cap cap'; @@ -5060,7 +5060,7 @@ end sublocale Arch < invalidateTLBByASID: typ_at_all_props' "invalidateTLBByASID asid" by typ_at_props' -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) crunch invalidateTLBByASID for cteCaps_of: "\s. P (cteCaps_of s)" diff --git a/proof/refine/ARM/IpcCancel_R.thy b/proof/refine/ARM/IpcCancel_R.thy index 735f77eb57..e80019b3d7 100644 --- a/proof/refine/ARM/IpcCancel_R.thy +++ b/proof/refine/ARM/IpcCancel_R.thy @@ -2971,7 +2971,7 @@ lemma setThreadState_unlive_other: apply (fastforce simp: ko_wp_at'_def obj_at'_def) done -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma possibleSwitchTo_unlive_other: "\ko_wp_at' (Not \ live') p and sch_act_not p and K (p \ t)\ diff --git a/proof/refine/ARM/Ipc_R.thy b/proof/refine/ARM/Ipc_R.thy index 044f8ba2bd..5cbc1f26b3 100644 --- a/proof/refine/ARM/Ipc_R.thy +++ b/proof/refine/ARM/Ipc_R.thy @@ -363,7 +363,7 @@ lemma maskedAsFull_null_cap[simp]: "(capability.NullCap = maskedAsFull x y) = (x = capability.NullCap)" by (case_tac x, auto simp:maskedAsFull_def isCap_simps ) -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma maskCapRights_eq_null: "(RetypeDecls_H.maskCapRights r xa = capability.NullCap) = @@ -1082,7 +1082,7 @@ crunch transferCaps global_interpretation transferCaps: typ_at_all_props' "transferCaps info caps endpoint receiver receiveBuffer" by typ_at_props' -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma isIRQControlCap_mask [simp]: "isIRQControlCap (maskCapRights R c) = isIRQControlCap c" @@ -1159,7 +1159,7 @@ crunch copyMRs global_interpretation copyMRs: typ_at_all_props' "copyMRs s sb r rb n" by typ_at_props' -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma copy_mrs_invs'[wp]: "\ invs' and tcb_at' s and tcb_at' r \ copyMRs s sb r rb n \\rv. invs' \" @@ -1496,7 +1496,7 @@ lemma msgFromLookupFailure_map[simp]: = msg_from_lookup_failure lf" by (cases lf, simp_all add: lookup_failure_map_def msgFromLookupFailure_def) -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma asUser_getRestartPC_corres: "corres (=) (tcb_at t and pspace_aligned and pspace_distinct) \ @@ -1581,7 +1581,7 @@ lemmas threadget_fault_corres = and f = tcb_fault and f' = tcbFault, simplified tcb_relation_def, simplified] -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) crunch make_fault_msg for in_user_Frame[wp]: "in_user_frame buffer" @@ -1720,7 +1720,7 @@ end global_interpretation doIPCTransfer: typ_at_all_props' "doIPCTransfer s e b g r" by typ_at_props' -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemmas dit_irq_node'[wp] = valid_irq_node_lift [OF doIPCTransfer_irq_node' doIPCTransfer_typ_at'] @@ -1925,7 +1925,7 @@ crunch handleFaultReply crunch handleFaultReply for tcb_in_cur_domain'[wp]: "tcb_in_cur_domain' t" -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) crunch handleFaultReply for pred_tcb_at'[wp]: "pred_tcb_at' proj P t" @@ -2745,7 +2745,7 @@ global_interpretation maybeReturnSc: typ_at_all_props' "maybeReturnSc ntfnPtr tc global_interpretation setMessageInfo: typ_at_all_props' "setMessageInfo t info" by typ_at_props' -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) crunch cancel_ipc for cur[wp]: "cur_tcb" @@ -5139,7 +5139,7 @@ lemma cteInsert_cap_to': apply (clarsimp simp: cte_wp_at_ctes_of)+ done -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) crunch setExtraBadge, doIPCTransfer for cap_to'[wp]: "ex_nonz_cap_to' p" diff --git a/proof/refine/ARM/KHeap_R.thy b/proof/refine/ARM/KHeap_R.thy index 2ec8f004ae..742ddc895a 100644 --- a/proof/refine/ARM/KHeap_R.thy +++ b/proof/refine/ARM/KHeap_R.thy @@ -574,7 +574,7 @@ local @{typ reply}, @{typ endpoint}, - (*FIXME: arch_split*) + (*FIXME: arch-split*) @{typ asidpool}, @{typ pte}, @{typ pde} @@ -668,7 +668,7 @@ lemma setObject_typ_at'[wp]: global_interpretation setObject: typ_at_all_props' "setObject p v" by typ_at_props' -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma setObject_cte_wp_at2': assumes x: "\x n tcb s t. \ t \ fst (updateObject v (KOTCB tcb) ptr x n s); Q s; @@ -942,7 +942,7 @@ end end -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma pspace_dom_update: "\ ps ptr = Some x; a_type x = a_type v \ \ pspace_dom (ps(ptr \ v)) = pspace_dom ps" @@ -2807,7 +2807,7 @@ interpretation setBoundNotification: pspace_only' "setBoundNotification ntfnPtr by (simp add: setBoundNotification_def threadSet_pspace_only') -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemmas setNotification_cap_to'[wp] = ex_cte_cap_to'_pres [OF set_ntfn'.cte_wp_at' set_ntfn'.ksInterruptState] @@ -3202,7 +3202,7 @@ crunch doMachineOp and pde_mappings'[wp]: "valid_pde_mappings'" and ko_wp_at'[wp]: "\s. P (ko_wp_at' T p s)" -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemmas bit_simps' = pteBits_def asidHighBits_def asid_low_bits_def asid_high_bits_def minSchedContextBits_def @@ -3540,7 +3540,7 @@ lemma ep_queued_st_tcb_at': (* cross lemmas *) -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma pspace_aligned_cross: "\ pspace_aligned s; pspace_relation (kheap s) (ksPSpace s') \ \ pspace_aligned' s'" @@ -4379,7 +4379,7 @@ lemma set_refills_is_active_sc2[wp]: (* updateSchedContext *) -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma state_relation_sc_update: assumes diff --git a/proof/refine/ARM/SchedContextInv_R.thy b/proof/refine/ARM/SchedContextInv_R.thy index 4fb2d8cd92..8700c9fa0e 100644 --- a/proof/refine/ARM/SchedContextInv_R.thy +++ b/proof/refine/ARM/SchedContextInv_R.thy @@ -11,7 +11,7 @@ begin global_interpretation schedContextCompleteYieldTo: typ_at_all_props' "schedContextCompleteYieldTo scp" by typ_at_props' -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) primrec valid_sc_inv' :: "sched_context_invocation \ kernel_state \ bool" where "valid_sc_inv' (InvokeSchedContextConsumed scptr args) = diff --git a/proof/refine/ARM/SchedContext_R.thy b/proof/refine/ARM/SchedContext_R.thy index 90e87133c7..0611509537 100644 --- a/proof/refine/ARM/SchedContext_R.thy +++ b/proof/refine/ARM/SchedContext_R.thy @@ -163,7 +163,7 @@ lemma updateSchedContext_invs'_indep: apply (frule (1) invs'_ko_at_valid_sched_context', simp) done -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma schedContextUpdateConsumed_corres: "corres (=) (sc_at scp) (sc_at' scp) @@ -826,7 +826,7 @@ lemma readRefillReady_no_ofail[wp]: apply (wpsimp wp: no_ofail_readCurTime) done -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma get_sc_released_corres: "corres (=) (active_scs_valid and sc_at sc_ptr) (valid_objs' and sc_at' sc_ptr) diff --git a/proof/refine/ARM/Schedule_R.thy b/proof/refine/ARM/Schedule_R.thy index 1e349f7984..95fc80cf4f 100644 --- a/proof/refine/ARM/Schedule_R.thy +++ b/proof/refine/ARM/Schedule_R.thy @@ -115,7 +115,7 @@ global_interpretation refillUpdate: typ_at_all_props' "refillUpdate scPtr newPe global_interpretation updateSchedContext: typ_at_all_props' "updateSchedContext scPtr f" by typ_at_props' -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma findM_awesome': assumes x: "\x xs. suffix (x # xs) xs' \ diff --git a/proof/refine/ARM/Syscall_R.thy b/proof/refine/ARM/Syscall_R.thy index f85e0a1918..5e1daf67fd 100644 --- a/proof/refine/ARM/Syscall_R.thy +++ b/proof/refine/ARM/Syscall_R.thy @@ -549,7 +549,7 @@ lemma sts_mcpriority_tcb_at'[wp]: crunch setThreadState for valid_ipc_buffer_ptr'[wp]: "valid_ipc_buffer_ptr' buf" -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma sts_valid_inv'[wp]: "setThreadState st t \valid_invocation' i\" @@ -1950,7 +1950,7 @@ end global_interpretation refillResetRR: typ_at_all_props' "refillResetRR scPtr" by typ_at_props' -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma refillResetRR_invs'[wp]: "refillResetRR scp \invs'\" diff --git a/proof/refine/ARM/TcbAcc_R.thy b/proof/refine/ARM/TcbAcc_R.thy index 2b8962512c..35d8c6c30d 100644 --- a/proof/refine/ARM/TcbAcc_R.thy +++ b/proof/refine/ARM/TcbAcc_R.thy @@ -1579,7 +1579,7 @@ lemma no_fail_asUser [wp]: apply (wpsimp wp: hoare_drop_imps no_fail_threadGet)+ done -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma asUser_setRegister_corres: "corres dc (tcb_at t and pspace_aligned and pspace_distinct) \ @@ -3349,7 +3349,7 @@ lemma threadGet_const: apply (clarsimp simp: obj_at'_def) done -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) schematic_goal l2BitmapSize_def': (* arch specific consequence *) "l2BitmapSize = numeral ?X" diff --git a/proof/refine/ARM/Tcb_R.thy b/proof/refine/ARM/Tcb_R.thy index 93072ac4d7..97c90110dd 100644 --- a/proof/refine/ARM/Tcb_R.thy +++ b/proof/refine/ARM/Tcb_R.thy @@ -1091,7 +1091,7 @@ termination recursive apply simp done -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma cte_map_tcb_0: "cte_map (t, tcb_cnode_index 0) = t" diff --git a/proof/refine/ARM/Untyped_R.thy b/proof/refine/ARM/Untyped_R.thy index 855fbefba1..b14b747d35 100644 --- a/proof/refine/ARM/Untyped_R.thy +++ b/proof/refine/ARM/Untyped_R.thy @@ -2707,7 +2707,7 @@ end global_interpretation updateNewFreeIndex: typ_at_all_props' "updateNewFreeIndex slot" by typ_at_props' -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma updateNewFreeIndex_valid_objs[wp]: "\valid_objs'\ updateNewFreeIndex slot \\_. valid_objs'\" diff --git a/proof/refine/ARM/VSpace_R.thy b/proof/refine/ARM/VSpace_R.thy index b4f784eade..c690f98c7e 100644 --- a/proof/refine/ARM/VSpace_R.thy +++ b/proof/refine/ARM/VSpace_R.thy @@ -1101,7 +1101,7 @@ sublocale Arch < loadHWASID: typ_at_all_props' "loadHWASID asid" sublocale Arch < setVMRootForFlush: typ_at_all_props' "setVMRootForFlush pd asid" by typ_at_props' -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) crunch setVMRootForFlush for aligned'[wp]: pspace_aligned' @@ -1332,7 +1332,7 @@ sublocale Arch < flushPage: typ_at_all_props' "flushPage arg1 pd asid vptr" sublocale Arch < findPDForASID: typ_at_all_props' "findPDForASID asid" by typ_at_props' -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) crunch unmapPageTable for aligned'[wp]: "pspace_aligned'" @@ -2054,7 +2054,7 @@ crunch setMRs global_interpretation setMRs: typ_at_all_props' "setMRs thread buffer data" by typ_at_props' -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma set_mrs_invs'[wp]: "\ invs' and tcb_at' receiver \ setMRs receiver recv_buf mrs \\rv. invs' \" @@ -2360,7 +2360,7 @@ end sublocale Arch < unmapPageTable: typ_at_all_props' "unmapPageTable asid vaddr pt" by typ_at_props' -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma performPageTableInvocation_corres: "page_table_invocation_map pti pti' \ @@ -2631,7 +2631,7 @@ sublocale Arch < performASIDPoolInvocation: typ_at_all_props' "performASIDPoolIn sublocale Arch < unmapPage: typ_at_all_props' "unmapPage magnitude asid vptr ptr" by typ_at_props' -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma dmo_ct[wp]: "\\s. P (ksCurThread s)\ doMachineOp m \\rv s. P (ksCurThread s)\" diff --git a/proof/refine/RISCV64/ArchAcc_R.thy b/proof/refine/RISCV64/ArchAcc_R.thy index c1ec1f2162..563c8f6d30 100644 --- a/proof/refine/RISCV64/ArchAcc_R.thy +++ b/proof/refine/RISCV64/ArchAcc_R.thy @@ -29,7 +29,7 @@ method simp_to_elim = (drule fun_all, elim allE impE) end -context Arch begin global_naming RISCV64_A (*FIXME: arch_split*) +context Arch begin global_naming RISCV64_A (*FIXME: arch-split*) lemma asid_pool_at_ko: "asid_pool_at p s \ \pool. ko_at (ArchObj (RISCV64_A.ASIDPool pool)) p s" @@ -63,7 +63,7 @@ lemmas storePTE_valid_pspace'[wp] = end -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) method readObject_arch_obj_at'_method = clarsimp simp: readObject_def obind_def omonad_defs split_def loadObject_default_def obj_at'_def diff --git a/proof/refine/RISCV64/CNodeInv_R.thy b/proof/refine/RISCV64/CNodeInv_R.thy index 16b5a14628..1448b61c00 100644 --- a/proof/refine/RISCV64/CNodeInv_R.thy +++ b/proof/refine/RISCV64/CNodeInv_R.thy @@ -6487,7 +6487,7 @@ lemma cteDelete_cte_wp_at_invs: apply simp done -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) crunch "Arch.finaliseCap", unbindMaybeNotification, prepareThreadDelete, schedContextMaybeUnbindNtfn, cleanReply @@ -6850,7 +6850,7 @@ lemmas rec_del_concrete_unfold = rec_del_concrete.simps red_zombie_will_fail.simps if_True if_False ball_simps simp_thms -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma cap_relation_removables: "\ cap_relation cap cap'; isNullCap cap' \ isZombie cap'; @@ -6915,7 +6915,7 @@ lemmas finaliseSlot_typ_ats[wp] = typ_at_lifts[OF finaliseSlot_typ_at'] lemmas rec_del_valid_list_irq_state_independent[wp] = rec_del_preservation[OF cap_swap_for_delete_valid_list set_cap_valid_list empty_slot_valid_list finalise_cap_valid_list preemption_point_valid_list] -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma rec_del_corres: "\C \ rec_del_concrete args. @@ -8625,7 +8625,7 @@ lemma corres_disj_abs: \ corres rv (\s. P s \ Q s) R f g" by (auto simp: corres_underlying_def) -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma cap_relation_same: "\ cap_relation cap cap'; cap_relation cap cap'' \ diff --git a/proof/refine/RISCV64/CSpace1_R.thy b/proof/refine/RISCV64/CSpace1_R.thy index 91f4465749..b5cb02e60c 100644 --- a/proof/refine/RISCV64/CSpace1_R.thy +++ b/proof/refine/RISCV64/CSpace1_R.thy @@ -951,7 +951,7 @@ lemma updateMDB_no_0 [wp]: \\rv s. no_0 (ctes_of s)\" by wp simp -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma isMDBParentOf_next_update [simp]: "isMDBParentOf (cteMDBNode_update (mdbNext_update f) cte) cte' = diff --git a/proof/refine/RISCV64/Detype_R.thy b/proof/refine/RISCV64/Detype_R.thy index 11e791450c..701e90409e 100644 --- a/proof/refine/RISCV64/Detype_R.thy +++ b/proof/refine/RISCV64/Detype_R.thy @@ -672,7 +672,7 @@ lemma deletionIsSafe_holds: and vu: "valid_untyped (cap.UntypedCap d base bits idx) s" shows "deletionIsSafe base bits s'" proof - - interpret Arch . (* FIXME: arch_split *) + interpret Arch . (* FIXME: arch-split *) note [simp del] = atLeastAtMost_simps have arch: @@ -1722,7 +1722,7 @@ lemma (in delete_locale) delete_sym_refs': state'))" (is "sym_refs (state_refs_of' (?state''))") proof - - interpret Arch . (*FIXME: arch_split*) + interpret Arch . (*FIXME: arch-split*) let ?s = state' let ?ran = base_bits diff --git a/proof/refine/RISCV64/Finalise_R.thy b/proof/refine/RISCV64/Finalise_R.thy index 2cfd111e55..a5756daa59 100644 --- a/proof/refine/RISCV64/Finalise_R.thy +++ b/proof/refine/RISCV64/Finalise_R.thy @@ -88,7 +88,7 @@ crunch clearUntypedFreeIndex global_interpretation clearUntypedFreeIndex: typ_at_all_props' "clearUntypedFreeIndex slot" by typ_at_props' -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) crunch postCapDeletion for tcb_at'[wp]: "tcb_at' t" @@ -2248,7 +2248,7 @@ lemma finaliseCap_cases[wp]: apply (auto simp add: isCap_simps cap_has_cleanup'_def) done -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) crunch finaliseCap for aligned'[wp]: pspace_aligned' @@ -2402,7 +2402,7 @@ crunch replyRemove and pspace_in_kernel_mappings'[wp]: pspace_in_kernel_mappings' (simp: crunch_simps wp: crunch_wps) -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) crunch replyRemove, handleFaultReply for ex_nonz_cap_to'[wp]: "ex_nonz_cap_to' ptr" @@ -2682,7 +2682,7 @@ lemma finaliseCap_True_invs'[wp]: apply (wp irqs_masked_lift| simp | wpc)+ done -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma invs_asid_update_strg': "invs' s \ tab = riscvKSASIDTable (ksArchState s) \ @@ -3914,7 +3914,7 @@ lemma finaliseCap_cte_cap_wp_to[wp]: global_interpretation unbindNotification: typ_at_all_props' "unbindNotification tcb" by typ_at_props' -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma finaliseCap_valid_cap[wp]: "\valid_cap' cap\ finaliseCap cap final flag \\rv. valid_cap' (fst rv)\" @@ -4559,7 +4559,7 @@ lemma can_fast_finalise_finaliseCap: = do finaliseCap cap final True; return (NullCap, NullCap) od" by (cases cap; simp add: finaliseCap_def isCap_simps) -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma finaliseCap_corres: "\ final_matters' cap' \ final = final'; cap_relation cap cap'; @@ -4662,7 +4662,7 @@ lemma threadSet_ct_idle_or_in_cur_domain': apply (auto simp: obj_at'_def) done -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemmas final_matters'_simps = final_matters'_def [split_simps capability.split arch_capability.split] diff --git a/proof/refine/RISCV64/IpcCancel_R.thy b/proof/refine/RISCV64/IpcCancel_R.thy index e5c65216bb..bad293b5d7 100644 --- a/proof/refine/RISCV64/IpcCancel_R.thy +++ b/proof/refine/RISCV64/IpcCancel_R.thy @@ -3239,7 +3239,7 @@ lemma setThreadState_unlive_other: apply (fastforce simp: ko_wp_at'_def obj_at'_def) done -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma possibleSwitchTo_unlive_other: "\ko_wp_at' (Not \ live') p and K (p \ t) and valid_tcbs'\ diff --git a/proof/refine/RISCV64/Ipc_R.thy b/proof/refine/RISCV64/Ipc_R.thy index 776ed2956b..477208f37b 100644 --- a/proof/refine/RISCV64/Ipc_R.thy +++ b/proof/refine/RISCV64/Ipc_R.thy @@ -377,7 +377,7 @@ lemma maskedAsFull_null_cap[simp]: "(capability.NullCap = maskedAsFull x y) = (x = capability.NullCap)" by (case_tac x, auto simp:maskedAsFull_def isCap_simps ) -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma maskCapRights_eq_null: "(RetypeDecls_H.maskCapRights r xa = capability.NullCap) = @@ -1079,7 +1079,7 @@ crunch transferCaps global_interpretation transferCaps: typ_at_all_props' "transferCaps info caps endpoint receiver receiveBuffer" by typ_at_props' -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma isIRQControlCap_mask [simp]: "isIRQControlCap (maskCapRights R c) = isIRQControlCap c" @@ -1181,7 +1181,7 @@ crunch copyMRs global_interpretation copyMRs: typ_at_all_props' "copyMRs s sb r rb n" by typ_at_props' -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma copy_mrs_invs'[wp]: "\ invs' and tcb_at' s and tcb_at' r \ copyMRs s sb r rb n \\rv. invs' \" @@ -1524,7 +1524,7 @@ lemma msgFromLookupFailure_map[simp]: = msg_from_lookup_failure lf" by (cases lf, simp_all add: lookup_failure_map_def msgFromLookupFailure_def) -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma asUser_getRestartPC_corres: "corres (=) (tcb_at t and pspace_aligned and pspace_distinct) \ @@ -1608,7 +1608,7 @@ lemmas threadget_fault_corres = and f = tcb_fault and f' = tcbFault, simplified tcb_relation_def, simplified] -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) crunch make_fault_msg for in_user_Frame[wp]: "in_user_frame buffer" @@ -1738,7 +1738,7 @@ end global_interpretation doIPCTransfer: typ_at_all_props' "doIPCTransfer s e b g r" by typ_at_props' -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemmas dit_irq_node'[wp] = valid_irq_node_lift [OF doIPCTransfer_irq_node' doIPCTransfer_typ_at'] @@ -1905,7 +1905,7 @@ crunch replyRemove, replyRemoveTCB, cancelSignal, cancelIPC, replyClear, cteDele for weak_sch_act_wf[wp]: "\s. weak_sch_act_wf (ksSchedulerAction s) s" (simp: crunch_simps wp: crunch_wps) -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) crunch handleFaultReply for pred_tcb_at'[wp]: "pred_tcb_at' proj P t" @@ -2768,7 +2768,7 @@ global_interpretation maybeReturnSc: typ_at_all_props' "maybeReturnSc ntfnPtr tc global_interpretation setMessageInfo: typ_at_all_props' "setMessageInfo t info" by typ_at_props' -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) crunch cancel_ipc for cur[wp]: "cur_tcb" @@ -5905,7 +5905,7 @@ lemma cteInsert_cap_to': apply (clarsimp simp: cte_wp_at_ctes_of)+ done -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) crunch setExtraBadge, doIPCTransfer for cap_to'[wp]: "ex_nonz_cap_to' p" diff --git a/proof/refine/RISCV64/KHeap_R.thy b/proof/refine/RISCV64/KHeap_R.thy index b82ee44b98..a5f1ba40cb 100644 --- a/proof/refine/RISCV64/KHeap_R.thy +++ b/proof/refine/RISCV64/KHeap_R.thy @@ -564,7 +564,7 @@ local @{typ reply}, @{typ endpoint}, - (*FIXME: arch_split*) + (*FIXME: arch-split*) @{typ asidpool}, @{typ pte} ]; @@ -653,7 +653,7 @@ lemma setObject_typ_at'[wp]: global_interpretation setObject: typ_at_all_props' "setObject p v" by typ_at_props' -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma setObject_cte_wp_at2': assumes x: "\x n tcb s t. \ t \ fst (updateObject v (KOTCB tcb) ptr x n s); Q s; @@ -2865,7 +2865,7 @@ interpretation setBoundNotification: pspace_only' "setBoundNotification ntfnPtr by (simp add: setBoundNotification_def threadSet_pspace_only') -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemmas setNotification_cap_to'[wp] = ex_cte_cap_to'_pres [OF set_ntfn'.cte_wp_at' set_ntfn'.ksInterruptState] @@ -3219,7 +3219,7 @@ crunch doMachineOp and idle'[wp]: "valid_idle'" and ko_wp_at'[wp]: "\s. P (ko_wp_at' T p s)" -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemmas is_aligned_add_step_le' = is_aligned_add_step_le[simplified mask_2pm1 add_diff_eq] @@ -3434,7 +3434,7 @@ lemma ep_queued_st_tcb_at': (* cross lemmas *) -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma pspace_aligned_cross: "\ pspace_aligned s; pspace_relation (kheap s) (ksPSpace s') \ \ pspace_aligned' s'" @@ -4362,7 +4362,7 @@ lemma set_refills_is_active_sc2[wp]: (* updateSchedContext *) -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) (* update wp rules without ko_at' *) lemma updateSchedContext_wp: diff --git a/proof/refine/RISCV64/LevityCatch.thy b/proof/refine/RISCV64/LevityCatch.thy index 9ed1c7eda7..d693347f6a 100644 --- a/proof/refine/RISCV64/LevityCatch.thy +++ b/proof/refine/RISCV64/LevityCatch.thy @@ -22,7 +22,7 @@ lemma magnitudeCheck_assert: "magnitudeCheck x y n = assert (case y of None \ True | Some z \ 1 << n \ z - x)" by (simp add: magnitudeCheck_def read_magnitudeCheck_assert) -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemmas makeObject_simps = makeObject_endpoint makeObject_notification makeObject_cte makeObject_tcb makeObject_user_data makeObject_pte @@ -60,7 +60,7 @@ lemma updateObject_default_inv: unfolding updateObject_default_def by (simp, wp magnitudeCheck_inv alignCheck_inv projectKO_inv, simp) -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma to_from_apiType [simp]: "toAPIType (fromAPIType x) = Some x" by (cases x) (auto simp add: fromAPIType_def RISCV64_H.fromAPIType_def diff --git a/proof/refine/RISCV64/SchedContextInv_R.thy b/proof/refine/RISCV64/SchedContextInv_R.thy index 78865be38a..8e3da19b1b 100644 --- a/proof/refine/RISCV64/SchedContextInv_R.thy +++ b/proof/refine/RISCV64/SchedContextInv_R.thy @@ -11,7 +11,7 @@ begin global_interpretation schedContextCompleteYieldTo: typ_at_all_props' "schedContextCompleteYieldTo scp" by typ_at_props' -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) primrec valid_sc_inv' :: "sched_context_invocation \ kernel_state \ bool" where "valid_sc_inv' (InvokeSchedContextConsumed scptr args) = diff --git a/proof/refine/RISCV64/SchedContext_R.thy b/proof/refine/RISCV64/SchedContext_R.thy index df9fc1b4eb..a15b65e367 100644 --- a/proof/refine/RISCV64/SchedContext_R.thy +++ b/proof/refine/RISCV64/SchedContext_R.thy @@ -172,7 +172,7 @@ lemma updateSchedContext_invs'_indep: apply (frule (1) invs'_ko_at_valid_sched_context', simp) done -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma schedContextUpdateConsumed_corres: "corres (=) (sc_at scp) (sc_at' scp) @@ -784,7 +784,7 @@ lemma readRefillReady_no_ofail[wp]: apply (wpsimp wp: no_ofail_readCurTime) done -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma refillReady_corres: "sc_ptr = scPtr \ diff --git a/proof/refine/RISCV64/Schedule_R.thy b/proof/refine/RISCV64/Schedule_R.thy index b0a3c7a770..d118ee1a79 100644 --- a/proof/refine/RISCV64/Schedule_R.thy +++ b/proof/refine/RISCV64/Schedule_R.thy @@ -106,7 +106,7 @@ global_interpretation refillNew: typ_at_all_props' "refillNew scPtr maxRefills b global_interpretation refillUpdate: typ_at_all_props' "refillUpdate scPtr newPeriod newBudget newMaxRefills" by typ_at_props' -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma findM_awesome': assumes x: "\x xs. suffix (x # xs) xs' \ diff --git a/proof/refine/RISCV64/Syscall_R.thy b/proof/refine/RISCV64/Syscall_R.thy index 314387871e..831eb78040 100644 --- a/proof/refine/RISCV64/Syscall_R.thy +++ b/proof/refine/RISCV64/Syscall_R.thy @@ -581,7 +581,7 @@ lemma sts_mcpriority_tcb_at'[wp]: crunch setThreadState for valid_ipc_buffer_ptr'[wp]: "valid_ipc_buffer_ptr' buf" -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma sts_valid_inv'[wp]: "setThreadState st t \valid_invocation' i\" @@ -1928,7 +1928,7 @@ end global_interpretation refillResetRR: typ_at_all_props' "refillResetRR scPtr" by typ_at_props' -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma refillResetRR_invs'[wp]: "refillResetRR scp \invs'\" diff --git a/proof/refine/RISCV64/TcbAcc_R.thy b/proof/refine/RISCV64/TcbAcc_R.thy index a49a625b85..807829012c 100644 --- a/proof/refine/RISCV64/TcbAcc_R.thy +++ b/proof/refine/RISCV64/TcbAcc_R.thy @@ -1630,7 +1630,7 @@ lemma no_fail_asUser[wp]: apply (wpsimp wp: hoare_drop_imps no_fail_threadGet)+ done -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma asUser_setRegister_corres: "corres dc (tcb_at t and pspace_aligned and pspace_distinct) \ @@ -3758,7 +3758,7 @@ lemma threadGet_const: apply (clarsimp simp: obj_at'_def) done -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) schematic_goal l2BitmapSize_def': (* arch specific consequence *) "l2BitmapSize = numeral ?X" diff --git a/proof/refine/RISCV64/Tcb_R.thy b/proof/refine/RISCV64/Tcb_R.thy index dc9ebc245a..e22d145f03 100644 --- a/proof/refine/RISCV64/Tcb_R.thy +++ b/proof/refine/RISCV64/Tcb_R.thy @@ -1126,7 +1126,7 @@ termination recursive apply simp done -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma cte_map_tcb_0: "cte_map (t, tcb_cnode_index 0) = t" diff --git a/proof/refine/RISCV64/Untyped_R.thy b/proof/refine/RISCV64/Untyped_R.thy index 8ebc4bc290..322c16af35 100644 --- a/proof/refine/RISCV64/Untyped_R.thy +++ b/proof/refine/RISCV64/Untyped_R.thy @@ -2754,7 +2754,7 @@ end global_interpretation updateNewFreeIndex: typ_at_all_props' "updateNewFreeIndex slot" by typ_at_props' -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma updateNewFreeIndex_valid_objs[wp]: "\valid_objs'\ updateNewFreeIndex slot \\_. valid_objs'\" diff --git a/proof/refine/RISCV64/VSpace_R.thy b/proof/refine/RISCV64/VSpace_R.thy index 8c5820d02e..94eaea373a 100644 --- a/proof/refine/RISCV64/VSpace_R.thy +++ b/proof/refine/RISCV64/VSpace_R.thy @@ -300,7 +300,7 @@ sublocale Arch < performASIDPoolInvocation: typ_at_all_props' "performASIDPoolIn sublocale Arch < performPageInvocation: typ_at_all_props' "performPageInvocation iv" by typ_at_props' -context begin interpretation Arch . (*FIXME: arch_split*) +context begin interpretation Arch . (*FIXME: arch-split*) lemma getObject_PTE_corres'': assumes "p' = p"