refine+crefine: remove valid_arch_mdb_ctes

- replace the ioport_control invariant with archMDBAssertions
- remove lemmas needed only for the invariant
- add corresponding crossing lemmas for caps_of_state based on existing
  older cte_wp_at lemmas

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

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/RISCV64/ADT_C.thy

@@ -1215,7 +1215,7 @@ lemma ksPSpace_eq_imp_valid_pspace'_eq:
   assumes ksPSpace: "ksPSpace s' = ksPSpace s"
   shows "valid_pspace' s = valid_pspace' s'"
   using assms
-  by (clarsimp simp: valid_pspace'_def pspace_aligned'_def
+  by (clarsimp simp: valid_pspace'_def pspace_aligned'_def pspace_in_kernel_mappings'_def
         pspace_distinct'_def ps_clear_def no_0_obj'_def valid_mdb'_def
         pspace_canonical'_def pspace_in_kernel_mappings'_def
         ksPSpace_eq_imp_valid_objs'_eq[OF ksPSpace])

proof/crefine/RISCV64/ArchMove_C.thy

@@ -33,15 +33,6 @@ lemma ps_clear_is_aligned_ksPSpace_None:
 
 context Arch begin arch_global_naming
 
-lemma ps_clear_is_aligned_ctes_None:
-  assumes "ps_clear p tcbBlockSizeBits s"
-      and "is_aligned p tcbBlockSizeBits"
-  shows "ksPSpace s (p + 2*2^cteSizeBits) = None"
-    and "ksPSpace s (p + 3*2^cteSizeBits) = None"
-    and "ksPSpace s (p + 4*2^cteSizeBits) = None"
-  by (auto intro: assms ps_clear_is_aligned_ksPSpace_None
-            simp: objBits_defs mask_def)+
-
 lemma word_shift_by_3:
   "x * 8 = (x::'a::len word) << 3"
   by (simp add: shiftl_t2n)
@@ -75,6 +66,15 @@ where
 (* FIXME: move to GenericLib *)
 lemmas unat64_eq_of_nat = unat_eq_of_nat[where 'a=64, folded word_bits_def]
 
+lemma ps_clear_is_aligned_ctes_None:
+  assumes "ps_clear p tcbBlockSizeBits s"
+      and "is_aligned p tcbBlockSizeBits"
+  shows "ksPSpace s (p + 2*2^cteSizeBits) = None"
+    and "ksPSpace s (p + 3*2^cteSizeBits) = None"
+    and "ksPSpace s (p + 4*2^cteSizeBits) = None"
+  by (auto intro: assms ps_clear_is_aligned_ksPSpace_None
+            simp: objBits_defs mask_def)+
+
 crunch archThreadGet
   for inv'[wp]: P
 

proof/crefine/RISCV64/CSpace_C.thy

@@ -994,8 +994,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)
@@ -1049,7 +1050,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/RISCV64/IsolatedThreadAction.thy

@@ -1177,13 +1177,27 @@ 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]
   apply (simp add: cteInsert_def updateCap_def updateMDB_def
                    Let_def setUntypedCapAsFull_def)
   apply (intro thread_actions_isolatable_bind[OF _ _ hoare_weaken_pre]
-               thread_actions_isolatable_if
+               thread_actions_isolatable_if archMDBAssertions_isolatable
                thread_actions_isolatable_returns assert_isolatable
                getCTE_isolatable setCTE_isolatable)
   apply (wp | simp)+

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/refine/AARCH64/ArchInvsDefs_H.thy

@@ -200,9 +200,6 @@ definition
 where
  "isArchFrameCap cap \<equiv> case cap of ArchObjectCap (FrameCap _ _ _ _ _) \<Rightarrow> True | _ \<Rightarrow> False"
 
-definition valid_arch_mdb_ctes :: "cte_heap \<Rightarrow> bool" where
-  "valid_arch_mdb_ctes \<equiv> \<top>"
-
 (* Addresses of all PTEs in a VSRoot table at p *)
 definition table_refs' :: "machine_word \<Rightarrow> machine_word set" where
   "table_refs' p \<equiv> (\<lambda>i. p + (i << pte_bits)) ` mask_range 0 (ptTranslationBits VSRootPT_T)"

proof/refine/AARCH64/Arch_R.thy

@@ -143,6 +143,7 @@ lemma performASIDControlInvocation_corres:
   apply (cases i)
   apply (rename_tac word1 prod1 prod2 word2)
   apply (clarsimp simp: asid_ci_map_def)
+  apply (rename_tac p slot p' slot' word2)
   apply (simp add: perform_asid_control_invocation_def placeNewObject_def2
                    performASIDControlInvocation_def)
   apply (rule corres_name_pre)
@@ -195,7 +196,7 @@ lemma performASIDControlInvocation_corres:
                apply wp+
            apply (strengthen safe_parent_strg[where idx = "2^pageBits"])
            apply (strengthen invs_valid_objs invs_distinct
-                             invs_psp_aligned invs_mdb
+                             invs_psp_aligned invs_mdb invs_arch_state
                   | simp cong:conj_cong)+
            apply (wp retype_region_plain_invs[where sz = pageBits]
                      retype_cte_wp_at[where sz = pageBits])+
@@ -279,7 +280,7 @@ lemma performASIDControlInvocation_corres:
     apply (drule detype_locale.non_null_present)
      apply (fastforce simp: cte_wp_at_caps_of_state)
     apply simp
-   apply (frule_tac ptr = "(aa,ba)" in detype_invariants [rotated 3])
+   apply (frule_tac ptr = "(p', slot')" in detype_invariants [rotated 3])
         apply fastforce
        apply simp
       apply (simp add: cte_wp_at_caps_of_state)
@@ -304,7 +305,7 @@ lemma performASIDControlInvocation_corres:
    apply (simp add:detype_clear_um_independent)
    apply (rule conjI)
     apply clarsimp
-    apply (drule_tac p = "(aa,ba)" in cap_refs_in_kernel_windowD2[OF caps_of_state_cteD])
+    apply (drule_tac p = "(p', slot')" in cap_refs_in_kernel_windowD2[OF caps_of_state_cteD])
      apply fastforce
     apply (clarsimp simp: region_in_kernel_window_def valid_cap_def
                           cap_aligned_def is_aligned_neg_mask_eq detype_def clear_um_def)
@@ -319,7 +320,7 @@ lemma performASIDControlInvocation_corres:
                          st_tcb_at_kh_def obj_at_kh_def st_tcb_at_def obj_at_def is_etcb_at_def
                          wrap_ext_det_ext_ext_def)
   apply (simp add: detype_def clear_um_def)
-  apply (drule_tac x = "cte_map (aa,ba)" in pspace_relation_cte_wp_atI[OF state_relation_pspace_relation])
+  apply (drule_tac x = "cte_map (p', slot')" in pspace_relation_cte_wp_atI[OF state_relation_pspace_relation])
     apply (simp add:invs_valid_objs)+
   apply clarsimp
   apply (drule cte_map_inj_eq)

proof/refine/AARCH64/CNodeInv_R.thy

@@ -8398,9 +8398,6 @@ proof
     apply (erule (1) irq_controlD, rule irq_control)
     done
 
-  show "valid_arch_mdb_ctes m'"
-    by simp
-
   have distz: "distinct_zombies m"
     using valid by (simp add: valid_mdb_ctes_def)