Overhaul arch-split in machine, ASpec and AInvs

camkes/cdl-refine/Eval_CAMKES_CDL.thy

@@ -169,42 +169,43 @@ lemma Collect_asid_high__eval_helper:
    apply (subst arg_cong[where f="(<) _"])
     prefer 2
     apply (rule unat_lt2p)
-   apply (simp add: asid_high_bits_def)
+   apply (simp add: MiscMachine_A.asid_high_bits_def)
   apply (simp add: transform_asid_def asid_high_bits_of_def[abs_def])
   apply (rule set_eqI)
   apply (rule iffI)
    apply clarsimp
   apply (clarsimp simp: Collect_conj_eq image_iff)
   apply (rule_tac x="(of_nat asid_high << asid_low_bits) + 1" in bexI)
    apply (subst add.commute, subst shiftr_irrelevant)
-     apply (clarsimp simp: asid_low_bits_def asid_high_bits_def)
-    apply (clarsimp simp: is_aligned_shift)
-   apply (subst shiftl_shiftr_id)
-     apply (clarsimp simp: asid_low_bits_def asid_high_bits_def)
-    apply (clarsimp simp: asid_low_bits_def asid_high_bits_def word_of_nat_less)
+     apply (clarsimp simp: MiscMachine_A.asid_low_bits_def)
+    apply (clarsimp simp: is_aligned_shift MiscMachine_A.asid_low_bits_def)
+   apply (clarsimp simp: MiscMachine_A.asid_low_bits_def)
+   apply (subst shiftl_shiftr_id, simp)
+    apply (clarsimp simp: MiscMachine_A.asid_high_bits_def word_of_nat_less)
    apply (subst ucast_of_nat_small)
-    apply (clarsimp simp: asid_high_bits_def)
+    apply (clarsimp simp: MiscMachine_A.asid_high_bits_def)
    apply simp
   apply clarsimp
   apply (rule conjI)
    apply (clarsimp simp: unat_ucast_eq_unat_and_mask)
    apply (subst add.commute, subst shiftr_irrelevant)
-     apply (clarsimp simp: asid_low_bits_def asid_high_bits_def)
+     apply (clarsimp simp: MiscMachine_A.asid_low_bits_def MiscMachine_A.asid_high_bits_def)
     apply (clarsimp simp: is_aligned_shift)
    apply (subst shiftl_shiftr_id)
-     apply (clarsimp simp: asid_low_bits_def asid_high_bits_def)
-    apply (clarsimp simp: asid_low_bits_def asid_high_bits_def word_of_nat_less)
+     apply (clarsimp simp: MiscMachine_A.asid_low_bits_def)
+    apply (clarsimp simp: MiscMachine_A.asid_low_bits_def MiscMachine_A.asid_high_bits_def
+                          word_of_nat_less)
    apply (fold asid_high_bits_def)
    apply (subst less_mask_eq)
-    apply (clarsimp simp: asid_high_bits_def word_of_nat_less)
+    apply (clarsimp simp: MiscMachine_A.asid_high_bits_def word_of_nat_less)
    apply (rule unat_of_nat_eq)
-   apply (clarsimp simp: asid_high_bits_def)
+   apply (clarsimp simp: MiscMachine_A.asid_high_bits_def)
   apply (rule less_is_non_zero_p1[where k="2^asid_high_bits << asid_low_bits"])
-  apply (simp only: shiftl_t2n)
+  apply (simp add: shiftl_t2n)
   apply (subst mult.commute, subst mult.commute, rule word_mult_less_mono1)
-    apply (clarsimp simp: asid_high_bits_def word_of_nat_less)
-   apply (clarsimp simp: asid_low_bits_def)
-  apply (clarsimp simp: asid_low_bits_def asid_high_bits_def)
+    apply (clarsimp simp: MiscMachine_A.asid_high_bits_def word_of_nat_less)
+   apply (clarsimp simp: MiscMachine_A.asid_low_bits_def)
+  apply (clarsimp simp: MiscMachine_A.asid_low_bits_def MiscMachine_A.asid_high_bits_def)
   done
 
 

proof/crefine/ARM_HYP/Syscall_C.thy

@@ -1628,7 +1628,7 @@ lemma virq_virq_active_set_virqEOIIRQEN_spec':
        \<lbrace> \<acute>ret__struct_virq_C = virq_C (ARRAY _. virqSetEOIIRQEN (virq_to_H \<^bsup>s\<^esup>virq) \<^bsup>s\<^esup>v32) \<rbrace>"
   apply (hoare_rule HoarePartial.ProcNoRec1) (* force vcg to unfold non-recursive procedure *)
   apply vcg
-  apply (clarsimp simp: virq_to_H_def ARM_A.virqSetEOIIRQEN_def)
+  apply (clarsimp simp: virq_to_H_def ARM_HYP_A.virqSetEOIIRQEN_def)
   apply (case_tac virq)
   apply clarsimp
   apply (rule array_ext)
@@ -1641,7 +1641,7 @@ lemma virq_virq_invalid_set_virqEOIIRQEN_spec':
        \<lbrace> \<acute>ret__struct_virq_C = virq_C (ARRAY _. virqSetEOIIRQEN (virq_to_H \<^bsup>s\<^esup>virq) \<^bsup>s\<^esup>v32) \<rbrace>"
   apply (hoare_rule HoarePartial.ProcNoRec1) (* force vcg to unfold non-recursive procedure *)
   apply vcg
-  apply (clarsimp simp: virq_to_H_def ARM_A.virqSetEOIIRQEN_def)
+  apply (clarsimp simp: virq_to_H_def ARM_HYP_A.virqSetEOIIRQEN_def)
   apply (case_tac virq)
   apply clarsimp
   apply (rule array_ext)
@@ -1654,7 +1654,7 @@ lemma virq_virq_pending_set_virqEOIIRQEN_spec':
        \<lbrace> \<acute>ret__struct_virq_C = virq_C (ARRAY _. virqSetEOIIRQEN (virq_to_H \<^bsup>s\<^esup>virq) \<^bsup>s\<^esup>v32) \<rbrace>"
   apply (hoare_rule HoarePartial.ProcNoRec1) (* force vcg to unfold non-recursive procedure *)
   apply vcg
-  apply (clarsimp simp: virq_to_H_def ARM_A.virqSetEOIIRQEN_def)
+  apply (clarsimp simp: virq_to_H_def ARM_HYP_A.virqSetEOIIRQEN_def)
   apply (case_tac virq)
   apply clarsimp
   apply (rule array_ext)
@@ -1676,7 +1676,7 @@ lemma virqSetEOIIRQEN_id:
      virq_get_tag (virq_C (ARRAY _. idx)) \<noteq> scast virq_virq_pending;
      virq_get_tag (virq_C (ARRAY _. idx)) \<noteq> scast virq_virq_invalid \<rbrakk>
     \<Longrightarrow> virqSetEOIIRQEN idx 0 = idx"
-  apply (clarsimp simp: ARM_A.virqSetEOIIRQEN_def virq_get_tag_def virq_tag_defs mask_def
+  apply (clarsimp simp: ARM_HYP_A.virqSetEOIIRQEN_def virq_get_tag_def virq_tag_defs mask_def
                   split: if_split)
   apply (rule_tac x="idx >> 28" in two_bits_cases; simp)
   done

proof/dpolicy/Dpolicy.thy

@@ -217,26 +217,26 @@ lemmas cdl_state_objs_to_policy_cases
     = cdl_state_bits_to_policy.cases[OF cdl_state_objs_to_policy_mem[THEN iffD1]]
 
 lemma transform_asid_rev [simp]:
-  "asid \<le> 2 ^ ARM_A.asid_bits - 1 \<Longrightarrow> transform_asid_rev (transform_asid asid) = asid"
+  "asid \<le> 2 ^ MiscMachine_A.asid_bits - 1 \<Longrightarrow> transform_asid_rev (transform_asid asid) = asid"
   apply (clarsimp simp:transform_asid_def transform_asid_rev_def
-                       asid_high_bits_of_def ARM_A.asid_low_bits_def)
+                       asid_high_bits_of_def asid_low_bits_def)
   apply (subgoal_tac "asid >> 10 < 2 ^ asid_high_bits")
-   apply (simp add:ARM_A.asid_high_bits_def ARM_A.asid_bits_def)
+   apply (simp add: MiscMachine_A.asid_high_bits_def MiscMachine_A.asid_bits_def MiscMachine_A.asid_low_bits_def)
    apply (subst ucast_ucast_len)
     apply simp
    apply (subst shiftr_shiftl1)
     apply simp
    apply (subst ucast_ucast_mask)
    apply (simp add:mask_out_sub_mask)
-  apply (simp add:ARM_A.asid_high_bits_def)
-  apply (rule shiftr_less_t2n[where m=7, simplified])
-  apply (simp add:ARM_A.asid_bits_def)
+  apply (simp add: asid_high_bits_def)
+  apply (rule shiftr_less_t2n[where m=MiscMachine_A.asid_high_bits, simplified])
+  apply (simp add: MiscMachine_A.asid_bits_def MiscMachine_A.asid_high_bits_def)
   done
 
 abbreviation
   "valid_asid_mapping mapping \<equiv> (case mapping of
     None \<Rightarrow> True
-  | Some (asid, ref) \<Rightarrow> asid \<le>  2 ^ ARM_A.asid_bits - 1)"
+  | Some (asid, ref) \<Rightarrow> asid \<le>  2 ^ asid_bits - 1)"
 
 lemma transform_asid_rev_transform_mapping [simp]:
   "valid_asid_mapping mapping \<Longrightarrow>
@@ -1073,7 +1073,7 @@ lemma state_vrefs_asid_pool_transform_rev:
   "\<lbrakk> einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap;
      \<not> is_null_cap poolcap; \<not> is_null_cap pdcap; pdptr = cap_object pdcap;
      opt_cap (cap_object poolcap, snd (transform_asid asid)) (transform s) = Some pdcap \<rbrakk> \<Longrightarrow>
-     (pdptr, asid && mask ARM_A.asid_low_bits, AASIDPool, Control)
+     (pdptr, asid && mask MiscMachine_A.asid_low_bits, AASIDPool, Control)
           \<in> state_vrefs s (cap_object poolcap)"
   apply (subgoal_tac "cap_object poolcap \<noteq> idle_thread s")
    prefer 2

proof/drefine/Arch_DR.thy

@@ -730,7 +730,7 @@ next
               apply (thin_tac "free_asid_select v \<notin> dom v")
               apply clarsimp
               apply (subgoal_tac "unat ((ucast (free_asid_select v) :: word32) << 10) mod 1024=0")
-               apply (simp add: asid_high_bits_of_shift[simplified asid_low_bits_def])
+               apply (simp add: asid_high_bits_of_shift[simplified asid_low_bits_def[simplified]])
               apply (rule shiftl_mod[where n=10, simplified])
               apply (cut_tac x="free_asid_select v" and 'a=32 in ucast_less)
                apply simp
@@ -1638,8 +1638,8 @@ proof -
         "CSpaceAcc_A.descendants_of cref (cdt s') = {}"
         "caps_of_state s' cref = Some cap"
         "cap = cap.UntypedCap False frame pageBits idx"
-        "is_aligned (base::word32) ARM_A.asid_low_bits"
-        "base < 2 ^ ARM_A.asid_bits"
+        "is_aligned (base::word32) asid_low_bits"
+        "base < 2 ^ asid_bits"
   assume relation:"arch_invocation_relation (InvokeAsidControl asid_inv)
          (arch_invocation.InvokeASIDControl (asid_control_invocation.MakePool frame cnode_ref cref base))"
   assume asid_para: "asid_inv' = asid_control_invocation.MakePool frame cnode_ref cref base"

proof/drefine/CNode_DR.thy

@@ -1159,7 +1159,7 @@ lemma set_asid_pool_empty':
   done
 
 lemma empty_pool:
-  "(\<lambda>x. if x \<le> 2 ^ ARM_A.asid_low_bits - 1 then None else (ap :: 10 word \<rightharpoonup> word32) x) = Map.empty"
+  "(\<lambda>x. if x \<le> 2 ^ asid_low_bits - 1 then None else (ap :: 10 word \<rightharpoonup> word32) x) = Map.empty"
   apply (rule ext)
   apply (cut_tac ptr=x and 'a=10 in word_up_bound)
   apply (simp add:asid_low_bits_def)
@@ -1180,8 +1180,8 @@ lemma get_set_asid_pool:
 lemma set_asid_pool_empty:
   "set_asid_pool a Map.empty \<equiv>
    mapM_x (\<lambda>slot. get_asid_pool a >>= (\<lambda>pool. set_asid_pool a (pool(ucast slot:=None))))
-          [0 :: word32 .e. 2 ^ ARM_A.asid_low_bits - 1]"
-  using set_asid_pool_empty' [of "2 ^ ARM_A.asid_low_bits - 1" a]
+          [0 :: word32 .e. 2 ^ asid_low_bits - 1]"
+  using set_asid_pool_empty' [of "2 ^ asid_low_bits - 1" a]
   apply -
   apply (rule eq_reflection)
   apply simp
@@ -1243,7 +1243,7 @@ lemma dcorres_set_asid_pool_empty:
   "dcorres dc \<top> (valid_idle and asid_pool_at a and
                  (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)))
     (mapM_x PageTableUnmap_D.empty_slot
-                            (map (Pair a) [0 .e. 2 ^ ARM_A.asid_low_bits - 1]))
+                            (map (Pair a) [0 .e. 2 ^ asid_low_bits - 1]))
     (set_asid_pool a Map.empty)"
   apply (unfold set_asid_pool_empty)
   apply (rule dcorres_list_all2_mapM_[where F="\<lambda>x y. snd x = snd (transform_asid y)"])
@@ -1269,7 +1269,7 @@ lemma dcorres_set_asid_pool_empty:
            apply (wp | clarsimp)+
         apply simp
        apply (wp get_asid_pool_triv | clarsimp simp:typ_at_eq_kheap_obj obj_at_def swp_def)+
-     apply (subgoal_tac "(aa, snd (transform_asid y)) \<in> set (map (Pair a) [0..<2 ^ ARM_A.asid_low_bits])")
+     apply (subgoal_tac "(aa, snd (transform_asid y)) \<in> set (map (Pair a) [0..<2 ^ asid_low_bits])")
       apply clarsimp
      apply (clarsimp simp del:set_map simp: suffix_def)
     apply (wp | clarsimp simp:swp_def)+

proof/invariant-abstract/AARCH64/ArchADT_AI.thy

@@ -12,7 +12,7 @@ imports
   "Lib.Simulation"
   Invariants_AI
 begin
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 subsection \<open>Constructing a virtual-memory view\<close>
 

proof/invariant-abstract/AARCH64/ArchAInvsPre.thy

@@ -11,9 +11,7 @@ begin
 
 unbundle l4v_word_context
 
-context Arch begin
-
-global_naming AARCH64
+context Arch begin arch_global_naming
 
 lemma ucast_ucast_mask_low: "(ucast (x && mask asid_low_bits) :: asid_low_index) = ucast x"
   by (rule ucast_mask_drop, simp add: asid_low_bits_def)
@@ -81,7 +79,6 @@ lemma device_frame_in_device_region:
   \<Longrightarrow> device_state (machine_state s) p \<noteq> None"
   by (auto simp add: pspace_respects_device_region_def dom_def device_mem_def)
 
-global_naming Arch
 named_theorems AInvsPre_assms
 
 lemma get_vspace_of_thread_asid_or_global_pt:
@@ -143,9 +140,4 @@ proof goal_cases
   case 1 show ?case by (intro_locales; (unfold_locales; fact AInvsPre_assms)?)
 qed
 
-requalify_facts
-  AARCH64.user_mem_dom_cong
-  AARCH64.device_mem_dom_cong
-  AARCH64.device_frame_in_device_region
-
 end

proof/invariant-abstract/AARCH64/ArchAcc_AI.thy

@@ -17,7 +17,7 @@ lemma valid_vso_at[wp]:"\<lbrace>valid_vso_at level p\<rbrace> f \<lbrace>\<lamb
 
 end
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 (* Is there a lookup that leads to a page table at (level, p)? *)
 locale_abbrev ex_vs_lookup_table ::

proof/invariant-abstract/AARCH64/ArchArch_AI.thy

@@ -11,7 +11,7 @@ begin
 
 unbundle l4v_word_context
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 definition
   "valid_aci aci \<equiv> case aci of MakePool frame slot parent base \<Rightarrow>
@@ -414,7 +414,7 @@ lemma equal_kernel_mappings:
 end
 
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 lemma vmid_for_asid_empty_update:
   "\<lbrakk> asid_table s asid_high = None; asid_pools_of s ap = Some Map.empty \<rbrakk> \<Longrightarrow>
@@ -1726,22 +1726,4 @@ lemma arch_pinv_st_tcb_at:
 
 end
 
-
-context begin interpretation Arch .
-
-requalify_consts
-  valid_arch_inv
-
-requalify_facts
-  invoke_arch_tcb
-  invoke_arch_invs
-  sts_valid_arch_inv
-  arch_decode_inv_wf
-  arch_pinv_st_tcb_at
-
-end
-
-declare invoke_arch_invs[wp]
-declare arch_decode_inv_wf[wp]
-
 end

proof/invariant-abstract/AARCH64/ArchBCorres2_AI.thy

@@ -10,7 +10,7 @@ imports
   BCorres2_AI
 begin
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 named_theorems BCorres2_AI_assms
 
@@ -89,7 +89,7 @@ interpretation BCorres2_AI?: BCorres2_AI
 
 lemmas schedule_bcorres[wp] = schedule_bcorres1[OF BCorres2_AI_axioms]
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 crunch send_ipc,send_signal,do_reply_transfer,arch_perform_invocation
   for (bcorres) bcorres[wp]: truncate_state

proof/invariant-abstract/AARCH64/ArchBCorres_AI.thy

@@ -11,7 +11,7 @@ imports
   ArchBitSetup_AI
 begin
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 lemma entry_for_asid_truncate[simp]:
   "entry_for_asid asid (truncate_state s) = entry_for_asid asid s"
@@ -45,8 +45,4 @@ crunch prepare_thread_delete
 
 end
 
-requalify_facts AARCH64.arch_finalise_cap_bcorres AARCH64.prepare_thread_delete_bcorres
-
-declare arch_finalise_cap_bcorres[wp] prepare_thread_delete_bcorres[wp]
-
 end

proof/invariant-abstract/AARCH64/ArchBits_AI.thy

@@ -9,7 +9,7 @@ theory ArchBits_AI
 imports Invariants_AI
 begin
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 (* arch-specific interpretations of update locales: *)
 

proof/invariant-abstract/AARCH64/ArchCNodeInv_AI.thy

@@ -9,7 +9,7 @@ theory ArchCNodeInv_AI
 imports CNodeInv_AI
 begin
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 named_theorems CNodeInv_AI_assms
 
@@ -538,7 +538,7 @@ qed
 termination rec_del by (rule rec_del_termination)
 
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 lemma post_cap_delete_pre_is_final_cap':
   "\<lbrakk>valid_ioports s; caps_of_state s slot = Some cap; is_final_cap' cap s; cap_cleanup_opt cap \<noteq> NullCap\<rbrakk>
@@ -800,7 +800,7 @@ global_interpretation CNodeInv_AI_2?: CNodeInv_AI_2
   qed
 
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 lemma finalise_cap_rvk_prog [CNodeInv_AI_assms]:
    "finalise_cap cap f \<lbrace>\<lambda>s. revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state s x))\<rbrace>"
@@ -905,7 +905,7 @@ termination cap_revoke by (rule cap_revoke_termination)
 declare cap_revoke.simps[simp del]
 
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 crunch finalise_slot
   for typ_at[wp, CNodeInv_AI_assms]: "\<lambda>s. P (typ_at T p s)"
@@ -930,7 +930,7 @@ global_interpretation CNodeInv_AI_4?: CNodeInv_AI_4
   qed
 
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 lemma cap_move_ioports:
   "\<lbrace>valid_ioports and cte_wp_at ((=) cap.NullCap) ptr'

proof/invariant-abstract/AARCH64/ArchCSpaceInvPre_AI.thy

@@ -14,7 +14,7 @@ imports CSpaceInvPre_AI
 begin
 
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 lemma aobj_ref_acap_rights_update[simp]:
   "aobj_ref (acap_rights_update f x) = aobj_ref x"
@@ -363,7 +363,7 @@ lemma cap_master_arch_cap_rights [simp]:
   by (simp add: cap_master_arch_cap_def acap_rights_update_def
            split: arch_cap.splits)
 
-lemma acap_rights_update_id [intro!, simp]:
+lemma valid_acap_rights_update_id [intro!, simp]:
   "valid_arch_cap ac s \<Longrightarrow> acap_rights_update (acap_rights ac) ac = ac"
   unfolding acap_rights_update_def acap_rights_def valid_arch_cap_def
   by (cases ac; simp)