remove valid_arch_mdb_ctes

proof/crefine/AARCH64/CSpace_C.thy

@@ -985,8 +985,9 @@ lemma cteInsert_ccorres:
            (Call cteInsert_'proc)"
   supply ctes_of_aligned_bits[simp]
   apply (cinit (no_ignore_call) lift: destSlot_' srcSlot_' newCap_'
-    simp del: return_bind simp add: Collect_const)
+                                simp del: return_bind simp add: Collect_const)
    apply (rule ccorres_move_c_guard_cte)
+   apply (rule ccorres_stateAssert)
    apply (ctac pre: ccorres_pre_getCTE)
      apply (rule ccorres_move_c_guard_cte)
      apply (ctac pre: ccorres_pre_getCTE)
@@ -1040,7 +1041,7 @@ lemma cteInsert_ccorres:
     apply (frule valid_cap_untyped_inv)
     apply clarsimp
    apply (rule conjI)
-    apply (case_tac ctea)
+    apply (case_tac cte)
     apply (clarsimp simp: isUntypedCap_def split: capability.splits)
     apply (frule valid_cap_untyped_inv[OF ctes_of_valid_cap'])
      apply fastforce

proof/crefine/AARCH64/Fastpath_C.thy

@@ -2279,6 +2279,7 @@ proof -
                                apply (rule ccorres_assert2)
                                apply (rule ccorres_pre_threadGet, rename_tac destState)
                                apply (rule_tac P="isReceive destState" in ccorres_gen_asm)
+                               apply (rule ccorres_stateAssert)
                                apply (rule ccorres_pre_getCTE2, rename_tac curThreadReplyCTE2)
                                apply (rule ccorres_pre_getCTE2, rename_tac destCallerCTE)
                                apply (rule ccorres_assert2)+
@@ -2449,6 +2450,7 @@ proof -
                              apply (rule conseqPre, vcg, clarsimp)
                             apply (simp add: cte_level_bits_def field_simps shiftl_t2n
                                              ctes_of_Some_cte_wp_at
+                                             archMDBAssertions_def
                                         del: all_imp_to_ex cong: imp_cong conj_cong)
                             apply (wp hoare_vcg_all_lift threadSet_ctes_of
                                       hoare_vcg_imp_lift' threadSet_valid_objs'

proof/crefine/AARCH64/IsolatedThreadAction.thy

@@ -1528,6 +1528,20 @@ lemma setCTE_isolatable:
   apply (clarsimp simp: obj_at'_def projectKOs)
   done
 
+lemma archMDBAssertions_isolatable:
+  "thread_actions_isolatable idx (stateAssert archMDBAssertions [])"
+  unfolding stateAssert_def archMDBAssertions_def
+  apply (clarsimp simp: thread_actions_isolatable_def)
+  apply (simp add: isolate_thread_actions_def bind_assoc split_def)
+  apply (simp add: bind_select_f_bind[symmetric] select_f_returns)
+  apply (clarsimp simp: monadic_rewrite_def exec_gets getSchedulerAction_def
+                        map_to_ctes_partial_overwrite)
+  apply (simp add: select_f_asserts)
+  apply (clarsimp simp: exec_modify o_def return_def)
+  apply (simp add: ksPSpace_update_partial_id)
+  apply (simp add: return_def fail_def modify_def get_def put_def assert_def bind_def)
+  done
+
 lemma cteInsert_isolatable:
   "thread_actions_isolatable idx (cteInsert cap src dest)"
   supply if_split[split del] if_cong[cong]
@@ -1536,7 +1550,8 @@ lemma cteInsert_isolatable:
   apply (intro thread_actions_isolatable_bind[OF _ _ hoare_weaken_pre]
                thread_actions_isolatable_if
                thread_actions_isolatable_returns
-               getCTE_isolatable setCTE_isolatable)
+               getCTE_isolatable setCTE_isolatable
+               archMDBAssertions_isolatable)
   apply (wp | simp)+
   done
 

proof/crefine/ARM/CSpace_C.thy

@@ -1010,6 +1010,7 @@ lemma cteInsert_ccorres:
                             simp del: return_bind
                             simp add: Collect_const)
    apply (rule ccorres_move_c_guard_cte)
+   apply (rule ccorres_stateAssert)
    apply (ctac pre: ccorres_pre_getCTE)
      apply (rule ccorres_move_c_guard_cte)
      apply (ctac pre: ccorres_pre_getCTE)
@@ -1063,7 +1064,7 @@ lemma cteInsert_ccorres:
     apply (frule valid_cap_untyped_inv)
     apply clarsimp
    apply (rule conjI)
-    apply (case_tac ctea)
+    apply (case_tac cte)
     apply (clarsimp simp: isUntypedCap_def split: capability.splits)
     apply (frule valid_cap_untyped_inv[OF ctes_of_valid_cap'])
      apply fastforce

proof/crefine/ARM/Fastpath_C.thy

@@ -2083,6 +2083,7 @@ proof -
                           apply (rule ccorres_assert2)
                           apply (rule ccorres_pre_threadGet, rename_tac destState)
                           apply (rule_tac P="isReceive destState" in ccorres_gen_asm)
+                          apply (rule ccorres_stateAssert)
                           apply (rule ccorres_pre_getCTE2, rename_tac curThreadReplyCTE2)
                           apply (rule ccorres_pre_getCTE2, rename_tac destCallerCTE)
                           apply (rule ccorres_assert2)+
@@ -2246,6 +2247,7 @@ proof -
                         apply (rule conseqPre, vcg, clarsimp)
                        apply (simp add: cte_level_bits_def field_simps shiftl_t2n
                                         ctes_of_Some_cte_wp_at
+                                        archMDBAssertions_def
                                    del: all_imp_to_ex cong: imp_cong conj_cong)
                        apply (wp hoare_vcg_all_lift threadSet_ctes_of
                                  hoare_vcg_imp_lift' threadSet_valid_objs'

proof/crefine/ARM/IsolatedThreadAction.thy

@@ -1141,6 +1141,20 @@ lemma assert_isolatable:
                 thread_actions_isolatable_returns
                 thread_actions_isolatable_fail)
 
+lemma archMDBAssertions_isolatable:
+  "thread_actions_isolatable idx (stateAssert archMDBAssertions [])"
+  unfolding stateAssert_def archMDBAssertions_def
+  apply (clarsimp simp: thread_actions_isolatable_def)
+  apply (simp add: isolate_thread_actions_def bind_assoc split_def)
+  apply (simp add: bind_select_f_bind[symmetric] select_f_returns)
+  apply (clarsimp simp: monadic_rewrite_def exec_gets getSchedulerAction_def
+                        map_to_ctes_partial_overwrite)
+  apply (simp add: select_f_asserts)
+  apply (clarsimp simp: exec_modify o_def return_def)
+  apply (simp add: ksPSpace_update_partial_id)
+  apply (simp add: return_def fail_def modify_def get_def put_def assert_def bind_def)
+  done
+
 lemma cteInsert_isolatable:
   "thread_actions_isolatable idx (cteInsert cap src dest)"
   supply if_split[split del] if_cong[cong]
@@ -1149,7 +1163,8 @@ lemma cteInsert_isolatable:
   apply (intro thread_actions_isolatable_bind[OF _ _ hoare_weaken_pre]
                thread_actions_isolatable_if
                thread_actions_isolatable_returns assert_isolatable
-               getCTE_isolatable setCTE_isolatable)
+               getCTE_isolatable setCTE_isolatable
+               archMDBAssertions_isolatable)
   apply (wp | simp)+
   done
 

proof/crefine/ARM_HYP/CSpace_C.thy

@@ -1050,6 +1050,7 @@ lemma cteInsert_ccorres:
                             simp del: return_bind
                             simp add: Collect_const)
    apply (rule ccorres_move_c_guard_cte)
+   apply (rule ccorres_stateAssert)
    apply (ctac pre: ccorres_pre_getCTE)
      apply (rule ccorres_move_c_guard_cte)
      apply (ctac pre: ccorres_pre_getCTE)
@@ -1103,7 +1104,7 @@ lemma cteInsert_ccorres:
     apply (frule valid_cap_untyped_inv)
     apply clarsimp
    apply (rule conjI)
-    apply (case_tac ctea)
+    apply (case_tac cte)
     apply (clarsimp simp: isUntypedCap_def split: capability.splits)
     apply (frule valid_cap_untyped_inv[OF ctes_of_valid_cap'])
      apply fastforce

proof/crefine/ARM_HYP/Fastpath_C.thy

@@ -2129,6 +2129,7 @@ proof -
                           apply (rule ccorres_assert2)
                           apply (rule ccorres_pre_threadGet, rename_tac destState)
                           apply (rule_tac P="isReceive destState" in ccorres_gen_asm)
+                          apply (rule ccorres_stateAssert)
                           apply (rule ccorres_pre_getCTE2, rename_tac curThreadReplyCTE2)
                           apply (rule ccorres_pre_getCTE2, rename_tac destCallerCTE)
                           apply (rule ccorres_assert2)+
@@ -2290,6 +2291,7 @@ proof -
                         apply (rule conseqPre, vcg, clarsimp)
                        apply (simp add: cte_level_bits_def field_simps shiftl_t2n
                                         ctes_of_Some_cte_wp_at
+                                        archMDBAssertions_def
                                    del: all_imp_to_ex cong: imp_cong conj_cong)
                        apply (wp hoare_vcg_all_lift threadSet_ctes_of
                                  hoare_vcg_imp_lift' threadSet_valid_objs'

proof/crefine/ARM_HYP/IsolatedThreadAction.thy

@@ -1416,6 +1416,20 @@ lemma assert_isolatable:
                 thread_actions_isolatable_returns
                 thread_actions_isolatable_fail)
 
+lemma archMDBAssertions_isolatable:
+  "thread_actions_isolatable idx (stateAssert archMDBAssertions [])"
+  unfolding stateAssert_def archMDBAssertions_def
+  apply (clarsimp simp: thread_actions_isolatable_def)
+  apply (simp add: isolate_thread_actions_def bind_assoc split_def)
+  apply (simp add: bind_select_f_bind[symmetric] select_f_returns)
+  apply (clarsimp simp: monadic_rewrite_def exec_gets getSchedulerAction_def
+                        map_to_ctes_partial_overwrite)
+  apply (simp add: select_f_asserts)
+  apply (clarsimp simp: exec_modify o_def return_def)
+  apply (simp add: ksPSpace_update_partial_id)
+  apply (simp add: return_def fail_def modify_def get_def put_def assert_def bind_def)
+  done
+
 lemma cteInsert_isolatable:
   "thread_actions_isolatable idx (cteInsert cap src dest)"
   supply if_split[split del] if_cong[cong]
@@ -1424,7 +1438,8 @@ lemma cteInsert_isolatable:
   apply (intro thread_actions_isolatable_bind[OF _ _ hoare_weaken_pre]
                thread_actions_isolatable_if
                thread_actions_isolatable_returns assert_isolatable
-               getCTE_isolatable setCTE_isolatable)
+               getCTE_isolatable setCTE_isolatable
+               archMDBAssertions_isolatable)
   apply (wp | simp)+
   done
 

proof/crefine/X64/CSpace_C.thy

@@ -1020,8 +1020,9 @@ lemma cteInsert_ccorres:
            (Call cteInsert_'proc)"
   supply ctes_of_aligned_bits[simp]
   apply (cinit (no_ignore_call) lift: destSlot_' srcSlot_' newCap_'
-    simp del: return_bind simp add: Collect_const)
+                                simp del: return_bind simp add: Collect_const)
    apply (rule ccorres_move_c_guard_cte)
+   apply (rule ccorres_stateAssert)
    apply (ctac pre: ccorres_pre_getCTE)
      apply (rule ccorres_move_c_guard_cte)
      apply (ctac pre: ccorres_pre_getCTE)
@@ -1075,7 +1076,7 @@ lemma cteInsert_ccorres:
     apply (frule valid_cap_untyped_inv)
     apply clarsimp
    apply (rule conjI)
-    apply (case_tac ctea)
+    apply (case_tac cte)
     apply (clarsimp simp: isUntypedCap_def split: capability.splits)
     apply (frule valid_cap_untyped_inv[OF ctes_of_valid_cap'])
      apply fastforce

proof/crefine/X64/IsolatedThreadAction.thy

@@ -1167,6 +1167,20 @@ lemma assert_isolatable:
                 thread_actions_isolatable_returns
                 thread_actions_isolatable_fail)
 
+lemma archMDBAssertions_isolatable:
+  "thread_actions_isolatable idx (stateAssert archMDBAssertions [])"
+  unfolding stateAssert_def archMDBAssertions_def
+  apply (clarsimp simp: thread_actions_isolatable_def)
+  apply (simp add: isolate_thread_actions_def bind_assoc split_def)
+  apply (simp add: bind_select_f_bind[symmetric] select_f_returns)
+  apply (clarsimp simp: monadic_rewrite_def exec_gets getSchedulerAction_def
+                        map_to_ctes_partial_overwrite)
+  apply (simp add: select_f_asserts)
+  apply (clarsimp simp: exec_modify o_def return_def)
+  apply (simp add: ksPSpace_update_partial_id)
+  apply (simp add: return_def fail_def modify_def get_def put_def assert_def bind_def)
+  done
+
 lemma cteInsert_isolatable:
   "thread_actions_isolatable idx (cteInsert cap src dest)"
   supply if_split[split del] if_cong[cong]
@@ -1175,7 +1189,8 @@ lemma cteInsert_isolatable:
   apply (intro thread_actions_isolatable_bind[OF _ _ hoare_weaken_pre]
                thread_actions_isolatable_if
                thread_actions_isolatable_returns assert_isolatable
-               getCTE_isolatable setCTE_isolatable)
+               getCTE_isolatable setCTE_isolatable
+               archMDBAssertions_isolatable)
   apply (wp | simp)+
   done
 

proof/invariant-abstract/X64/ArchArch_AI.thy

@@ -591,12 +591,22 @@ lemma cap_insert_ioports_ap:
          | wpc | simp split del: if_split)+
   done
 
+lemma cap_insert_ioport_control_ap:
+  "\<lbrace>ioport_control_unique and K (is_ap_cap cap)\<rbrace>
+   cap_insert cap src dest
+   \<lbrace>\<lambda>_. ioport_control_unique\<rbrace>"
+  unfolding cap_insert_def set_untyped_cap_as_full_def
+  apply (wpsimp wp: get_cap_wp set_cap_ioport_control_safe hoare_vcg_const_imp_lift)
+  apply (auto simp: cte_wp_at_caps_of_state is_cap_simps)
+  done
+
 lemma cap_insert_valid_arch_state_ap:
   "\<lbrace>valid_arch_state and (\<lambda>s. cte_wp_at (\<lambda>cap'. safe_ioport_insert cap cap' s) dest s) and
     K (is_ap_cap cap)\<rbrace>
    cap_insert cap src dest
    \<lbrace>\<lambda>rv. valid_arch_state\<rbrace>"
-  by (wp valid_arch_state_lift_ioports_aobj_at cap_insert_aobj_at cap_insert_ioports_ap)+
+  by (wp valid_arch_state_lift_ioports_aobj_at cap_insert_aobj_at cap_insert_ioports_ap
+         cap_insert_ioport_control_ap)+
      (simp add: valid_arch_state_def)
 
 lemma cap_insert_ap_invs:

proof/invariant-abstract/X64/ArchCNodeInv_AI.thy

@@ -444,6 +444,30 @@ lemma cap_swap_ioports[wp]:
                  dest!: weak_derived_cap_ioports)
   by (fastforce elim!: ranE split: if_split_asm)
 
+lemma same_object_as_IOPortControlCap_eq:
+  "same_object_as cap (ArchObjectCap IOPortControlCap) = (cap = ArchObjectCap IOPortControlCap)"
+  unfolding same_object_as_def
+  by (simp split: cap.splits arch_cap.splits)
+
+lemma copy_of_IOPortControlCap_eq:
+  "(copy_of (ArchObjectCap IOPortControlCap) cap) = (cap = ArchObjectCap IOPortControlCap)"
+  unfolding copy_of_def
+  by (auto simp: is_cap_simps same_object_as_IOPortControlCap_eq)
+
+lemma weak_derived_IOPortControlCap_eq[simp]:
+  "weak_derived (ArchObjectCap IOPortControlCap) cap = (cap = ArchObjectCap IOPortControlCap)"
+  unfolding weak_derived_def
+  by (auto simp: copy_of_IOPortControlCap_eq)
+
+lemma cap_swap_ioport_control[wp]:
+  "\<lbrace>ioport_control_unique and cte_wp_at (weak_derived c) a and cte_wp_at (weak_derived c') b\<rbrace>
+   cap_swap c a c' b
+   \<lbrace>\<lambda>_. ioport_control_unique\<rbrace>"
+  apply (wpsimp wp: cap_swap_caps_of_state simp: cte_wp_at_caps_of_state)
+  apply (clarsimp simp: ioport_control_unique_def)
+  apply (cases a, cases b)
+  by (rule conjI; clarsimp)+
+
 lemma cap_swap_valid_arch_state[wp, CNodeInv_AI_assms]:
   "\<lbrace>valid_arch_state and cte_wp_at (weak_derived c) a and cte_wp_at (weak_derived c') b\<rbrace>
    cap_swap c a c' b
@@ -989,6 +1013,16 @@ lemma cap_move_ioports:
                  dest!: weak_derived_cap_ioports)
   by (fastforce elim!: ranE split: if_split_asm)
 
+lemma cap_move_ioport_control[wp]:
+  "\<lbrace>ioport_control_unique and cte_wp_at (weak_derived cap) ptr\<rbrace>
+   cap_move cap ptr ptr'
+   \<lbrace>\<lambda>_. ioport_control_unique\<rbrace>"
+  apply (wpsimp wp: cap_move_caps_of_state simp: cte_wp_at_caps_of_state)
+  apply (clarsimp simp: ioport_control_unique_def)
+  apply (cases ptr)
+  apply (rule conjI; clarsimp)
+  done
+
 lemma cap_move_valid_arch:
   "\<lbrace>valid_arch_state and cte_wp_at ((=) cap.NullCap) ptr'
     and cte_wp_at (weak_derived cap) ptr

proof/invariant-abstract/X64/ArchCSpaceInv_AI.thy

@@ -49,13 +49,22 @@ lemma set_cap_ioports_safe:
     apply blast+
   done
 
+lemma set_cap_ioport_control_safe:
+ "\<lbrace>\<lambda>s. ioport_control_unique s \<and>
+       (cap = ArchObjectCap IOPortControlCap \<longrightarrow> cte_wp_at ((=) (ArchObjectCap IOPortControlCap)) ptr s) \<rbrace>
+    set_cap cap ptr
+  \<lbrace>\<lambda>rv. ioport_control_unique \<rbrace>"
+  apply wp
+  apply (auto simp: ioport_control_unique_def cte_wp_at_caps_of_state)
+  done
+
 lemma set_cap_non_arch_valid_arch_state:
  "\<lbrace>\<lambda>s. valid_arch_state s \<and> cte_wp_at (\<lambda>_. \<not>is_arch_cap cap) ptr s\<rbrace>
   set_cap cap ptr
   \<lbrace>\<lambda>rv. valid_arch_state \<rbrace>"
   unfolding valid_arch_state_def
   by (wp set_cap.aobj_at valid_asid_table_lift valid_global_pts_lift valid_global_pds_lift
-         valid_global_pdpts_lift typ_at_lift set_cap_ioports_safe)+
+         valid_global_pdpts_lift typ_at_lift set_cap_ioports_safe set_cap_ioport_control_safe)+
      (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps valid_pspace_def safe_ioport_insert_triv)
 
 lemma set_cap_ioports_no_new_ioports:
@@ -80,12 +89,15 @@ lemma set_cap_ioports_no_new_ioports:
 
 lemma set_cap_no_new_ioports_arch_valid_arch_state:
  "\<lbrace>\<lambda>s. valid_arch_state s
-       \<and> cte_wp_at (\<lambda>cap'. cap_ioports cap = {} \<or> cap_ioports cap = cap_ioports cap') ptr s\<rbrace>
+       \<and> cte_wp_at (\<lambda>cap'. cap_ioports cap = {} \<or> cap_ioports cap = cap_ioports cap') ptr s
+       \<and> (cap = ArchObjectCap IOPortControlCap \<longrightarrow>
+          cte_wp_at ((=) (ArchObjectCap IOPortControlCap)) ptr s) \<rbrace>
   set_cap cap ptr
   \<lbrace>\<lambda>rv. valid_arch_state \<rbrace>"
   unfolding valid_arch_state_def
   by (wp set_cap.aobj_at valid_asid_table_lift valid_global_pts_lift valid_global_pds_lift
-         valid_global_pdpts_lift typ_at_lift set_cap_ioports_no_new_ioports)+
+         valid_global_pdpts_lift typ_at_lift set_cap_ioports_no_new_ioports
+         set_cap_ioport_control_safe)+
      (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps valid_pspace_def)
 
 lemma valid_ioportsD:
@@ -111,6 +123,10 @@ lemma unique_table_refs_no_cap_asidE:
 lemmas unique_table_refs_no_cap_asidD
      = unique_table_refs_no_cap_asidE[where S="{}"]
 
+lemma is_ioport_control_cap_simp[simp]:
+  "is_ioport_control_cap (ArchObjectCap IOPortControlCap)"
+  by (simp add: is_ioport_control_cap_def)
+
 lemma replace_cap_invs:
   "\<lbrace>\<lambda>s. invs s \<and> cte_wp_at (replaceable s p cap) p s
         \<and> cap \<noteq> cap.NullCap
@@ -214,6 +230,7 @@ lemma replace_cap_invs:
                     valid_arch_caps_def unique_table_refs_no_cap_asidE)
   apply clarsimp
   apply (rule conjI, solves clarsimp)
+  apply (rule conjI, solves clarsimp)
   apply (rule Ball_emptyI, simp add: gen_obj_refs_subset)
   done