rt trivial: rename arch_split -> arch-split again after merge

Signed-off-by: Corey Lewis <[email protected]>

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:

proof/invariant-abstract/CSpaceInvPre_AI.thy

@@ -139,7 +139,7 @@ lemma empty_table_caps_of:
   "empty_table S ko \<Longrightarrow> 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\<lparr>free_index := a\<rparr>) = cap_asid src_cap"

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' \<Longrightarrow>

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:
   "\<lbrakk> cap_relation cap cap'; isNullCap cap' \<or> 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:
   "\<forall>C \<in> 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:
   "\<lbrakk> cap_relation cap cap'; cap_relation cap cap'' \<rbrakk>

proof/refine/ARM/CSpace1_R.thy

@@ -926,7 +926,7 @@ abbreviation
 abbreviation
   "revokable' a b \<equiv> 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]
 

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 \<open>Invariant preservation across concrete deletion\<close>
 
@@ -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: "\<And> ko p. \<lbrakk> ksPSpace s' p = Some (KOArch ko); p \<in> {base..base + 2 ^ bits - 1} \<rbrakk>
                        \<Longrightarrow> 6 \<le> bits"

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]:
   "\<lbrace>invs'\<rbrace> deleteASID asid pd \<lbrace>\<lambda>rv. invs'\<rbrace>"
@@ -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]:
   "\<lbrace>valid_cap' cap\<rbrace> finaliseCap cap final flag \<lbrace>\<lambda>rv. valid_cap' (fst rv)\<rbrace>"
@@ -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:
   "\<lbrakk> final_matters' cap' \<Longrightarrow> 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: "\<lambda>s. P (cteCaps_of s)"

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:
   "\<lbrace>ko_wp_at' (Not \<circ> live') p and sch_act_not p and K (p \<noteq> t)\<rbrace>

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]:
   "\<lbrace> invs' and tcb_at' s and tcb_at' r \<rbrace> copyMRs s sb r rb n \<lbrace>\<lambda>rv. invs' \<rbrace>"
@@ -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) \<top>
@@ -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"

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: "\<And>x n tcb s t. \<lbrakk> t \<in> 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:
   "\<lbrakk> ps ptr = Some x; a_type x = a_type v \<rbrakk> \<Longrightarrow> pspace_dom (ps(ptr \<mapsto> 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]: "\<lambda>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:
   "\<lbrakk> pspace_aligned s; pspace_relation (kheap s) (ksPSpace s') \<rbrakk> \<Longrightarrow> 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

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 \<Rightarrow> kernel_state \<Rightarrow> bool" where
   "valid_sc_inv' (InvokeSchedContextConsumed scptr args) =

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)

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: "\<And>x xs. suffix (x # xs) xs' \<Longrightarrow>

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 \<lbrace>valid_invocation' i\<rbrace>"
@@ -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 \<lbrace>invs'\<rbrace>"

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) \<top>
@@ -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"