x64 refine: remove valid_ioports' from invariants

With the exception of performX64PortInvocation_corres and
arch_performInvocation_invs', the knowledge about IO port cap validity
is unnecessary in Refine. For those two lemmas, we added an assertion
and a cross lemma to re-derive the information from valid_ioports over
the state relation. This leads to a simlified formulation of
post_cap_delete_pre' such that it satisfies the minimum requirements for
the arch-generic formulation of cap finalisation proofs.

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

proof/refine/X64/Arch_R.thy

@@ -1312,6 +1312,11 @@ lemma port_out_corres[@lift_corres_args, corres]:
      apply wpsimp+
   done
 
+defs allIOPortsIssued_asrt_def:
+  "allIOPortsIssued_asrt \<equiv> \<lambda>s. all_ioports_issued' (cteCaps_of s) (ksArchState s)"
+
+lemmas [simp] = allIOPortsIssued_asrt_def
+
 lemma perform_port_inv_corres:
   "\<lbrakk>archinv_relation ai ai'; ai = arch_invocation.InvokeIOPort x\<rbrakk>
   \<Longrightarrow> corres (dc \<oplus> (=))
@@ -1332,20 +1337,34 @@ crunch setIOPortMask
 
 lemma setIOPortMask_invs':
   "\<lbrace>invs' and (\<lambda>s. \<not> b \<longrightarrow> (\<forall>cap'\<in>ran (cteCaps_of s). cap_ioports' cap' \<inter> {f..l} = {}))\<rbrace> setIOPortMask f l b \<lbrace>\<lambda>rv. invs'\<rbrace>"
-  apply (wpsimp wp: setIOPortMask_ioports' simp: invs'_def valid_state'_def setIOPortMask_def simp_del: fun_upd_apply)
+  apply (wpsimp wp: simp: invs'_def valid_state'_def setIOPortMask_def simp_del: fun_upd_apply)
   apply (clarsimp simp: foldl_map foldl_fun_upd_value valid_global_refs'_def global_refs'_def
                         valid_arch_state'_def valid_machine_state'_def)
-  apply (case_tac b; clarsimp simp: valid_ioports'_simps foldl_fun_upd_value)
-   apply (drule_tac x=cap in bspec, assumption)
-   apply auto[1]
-  apply (drule_tac x=cap in bspec, assumption)
-  by auto
+  done
 
-lemma valid_ioports_issuedD':
-  "\<lbrakk>valid_ioports' s; cteCaps_of s src = Some cap\<rbrakk> \<Longrightarrow> cap_ioports' cap \<subseteq> issued_ioports' (ksArchState s)"
-  apply (clarsimp simp: valid_ioports'_def all_ioports_issued'_def)
+lemma all_ioports_issued_issuedD':
+  "\<lbrakk>all_ioports_issued' (cteCaps_of s) (ksArchState s); cteCaps_of s src = Some cap\<rbrakk> \<Longrightarrow> cap_ioports' cap \<subseteq> issued_ioports' (ksArchState s)"
+  apply (clarsimp simp: all_ioports_issued'_def)
   by auto
 
+lemma all_ioports_issued_cross:
+  "\<lbrakk> (s, s') \<in> state_relation; invs s; all_ioports_issued (caps_of_state s) (arch_state s) \<rbrakk>
+   \<Longrightarrow> all_ioports_issued' (cteCaps_of s') (ksArchState s')"
+  apply (simp add: all_ioports_issued_def all_ioports_issued'_def)
+  apply (prop_tac "issued_ioports' (ksArchState s') = issued_ioports (arch_state s)")
+   apply (drule state_relationD)
+   apply (simp add: arch_state_relation_def issued_ioports_def issued_ioports'_def)
+  apply (clarsimp dest!: ranD del: subsetI simp: cteCaps_of_def)
+  apply (rename_tac p' cte')
+  apply (drule (1) pspace_relation_cte_wp_atI'[OF state_relation_pspace_relation ctes_of_cte_wpD])
+   apply clarsimp
+  apply (clarsimp dest!: Retype_AI.F[THEN iffD2] del: subsetI)
+  apply (rename_tac cap ref idx)
+  apply (drule_tac x=cap in bspec)
+   apply (fastforce simp: ran_def)
+  apply (clarsimp simp: cap_ioports_def split: cap.splits arch_cap.splits)
+  done
+
 lemma performX64PortInvocation_corres:
   "\<lbrakk>archinv_relation ai ai'; ai = arch_invocation.InvokeIOPortControl x\<rbrakk> \<Longrightarrow>
    corres (dc \<oplus> (=))
@@ -1356,6 +1375,9 @@ lemma performX64PortInvocation_corres:
   apply (clarsimp simp: perform_ioport_control_invocation_def performX64PortInvocation_def
                         archinv_relation_def ioport_control_inv_relation_def)
   apply (case_tac x; clarsimp simp: bind_assoc simp del: split_paired_All)
+  apply (rule_tac corres_stateAssert_add_assertion[rotated])
+   apply (rule all_ioports_issued_cross;
+          fastforce dest!: invs_valid_ioports simp: valid_ioports_def)
   apply (rule corres_guard_imp)
     apply (rule corres_split_nor[OF set_ioport_mask_corres])
       apply (rule corres_split_nor[OF cteInsert_simple_corres])
@@ -1380,7 +1402,7 @@ lemma performX64PortInvocation_corres:
   apply (clarsimp simp: safe_parent_for'_def cte_wp_at_ctes_of)
   apply (case_tac ctea)
   apply (clarsimp simp: isCap_simps sameRegionAs_def3)
-  apply (drule_tac src=p in valid_ioports_issuedD'[OF invs_valid_ioports'])
+  apply (drule_tac src=p in all_ioports_issued_issuedD')
    apply (fastforce simp: cteCaps_of_def)
   apply force
   done
@@ -1972,7 +1994,6 @@ lemma invs_asid_table_strengthen':
   apply (rule conjI)
    apply (clarsimp simp: valid_pspace'_def)
   apply (simp add: valid_machine_state'_def)
-  apply (clarsimp simp: valid_ioports'_simps)
   done
 
 lemma ex_cte_not_in_untyped_range:
@@ -2183,13 +2204,13 @@ lemma arch_performInvocation_invs':
                         is_simple_cap'_def isCap_simps)
   apply (clarsimp simp: cte_wp_at_ctes_of)
   apply (rule conjI, clarsimp)
-  apply (rule conjI, clarsimp simp: safe_parent_for'_def)
-   apply (case_tac ctea)
-   apply (clarsimp simp: isCap_simps sameRegionAs_def3)
-   apply (drule_tac src=p in valid_ioports_issuedD'[OF invs_valid_ioports'])
-    apply (fastforce simp: cteCaps_of_def)
-   apply force
-  using ranD valid_ioports_issuedD' by fastforce
+  apply (clarsimp simp: safe_parent_for'_def)
+  apply (case_tac ctea)
+  apply (clarsimp simp: isCap_simps sameRegionAs_def3)
+  apply (drule_tac src=p in all_ioports_issued_issuedD')
+   apply (fastforce simp: cteCaps_of_def)
+  apply force
+  done
 
 end
 

proof/refine/X64/CNodeInv_R.thy

@@ -5074,30 +5074,6 @@ lemma weak_derived_cap_ioports':
   apply (case_tac c; clarsimp)
   by (rename_tac ac, case_tac ac; clarsimp)
 
-lemma cteSwap_ioports'[wp]:
-  "\<lbrace>valid_ioports' and cte_wp_at' (weak_derived' c \<circ> cteCap) c1
-           and cte_wp_at' (weak_derived' c' \<circ> cteCap) c2\<rbrace>
-     cteSwap c c1 c' c2
-   \<lbrace>\<lambda>rv. valid_ioports'\<rbrace>"
-  apply (simp add: valid_ioports'_simps)
-  apply (rule hoare_pre)
-   apply (rule hoare_use_eq [where f=ksArchState, OF cteSwap_ksArch])
-   apply (simp add: cteSwap_def)
-   apply wp
-  apply (clarsimp simp: cte_wp_at_ctes_of cteCaps_of_def ran_def)
-  apply (clarsimp simp add: modify_map_def split: if_split_asm dest!: weak_derived_cap_ioports')
-  apply (rule conjI, clarsimp)
-   apply (rule conjI, clarsimp)
-     apply (force simp: isCap_simps)
-   subgoal by ((auto | blast)+) (* long *)
-  apply clarsimp
-  apply (rule conjI, clarsimp)
-   subgoal by (force simp: isCap_simps) (* long *)
-  apply clarsimp
-  apply safe[1]
-                       apply distinct_subgoals
-  by ((auto | blast)+) (* long *)
-
 lemma weak_derived_untypedZeroRange:
   "\<lbrakk> weak_derived' c c'; isUntypedCap c' \<longrightarrow> c' = c \<rbrakk>
     \<Longrightarrow> untypedZeroRange c = untypedZeroRange c'"
@@ -5635,19 +5611,18 @@ lemma make_zombie_invs':
   apply (simp add: invs'_def valid_state'_def valid_pspace'_def valid_mdb'_def
                    valid_irq_handlers'_def irq_issued'_def)
   apply (wp updateCap_ctes_of_wp sch_act_wf_lift valid_queues_lift cur_tcb_lift
-            updateCap_iflive' updateCap_ifunsafe' updateCap_idle' updateCap_ioports'
+            updateCap_iflive' updateCap_ifunsafe' updateCap_idle'
             valid_arch_state_lift' valid_irq_node_lift ct_idle_or_in_cur_domain'_lift2
             updateCap_untyped_ranges_zero_simple
        | simp split del: if_split)+
   apply (intro conjI[rotated])
-         apply (clarsimp simp: cte_wp_at_ctes_of)
-         apply (auto simp: untypedZeroRange_def isCap_simps)[1]
-        apply clarsimp
-       apply (auto simp: cte_wp_at_ctes_of isCap_simps)[1]
+          apply (clarsimp simp: cte_wp_at_ctes_of)
+          apply (auto simp: untypedZeroRange_def isCap_simps)[1]
+         apply clarsimp
         apply (clarsimp simp: modify_map_def ran_def split del: if_split
                        split: if_split_asm)
          apply (clarsimp simp: cteCaps_of_def cte_wp_at_ctes_of isCap_simps)
-      apply (auto)[1]
+        apply (auto)[1]
        apply (clarsimp simp: disj_comms cte_wp_at_ctes_of
                       dest!: ztc_phys capBits_capUntyped_capRange)
        apply (frule(1) capBits_capUntyped_capRange, simp)
@@ -6322,18 +6297,11 @@ proof (induct arbitrary: P p rule: finalise_spec_induct2)
     apply fastforce
     done
   have final_IOPort_no_copy:
-    "\<And>c f l cap' cte  sl sl' sa . \<lbrakk>valid_ioports' sa; ctes_of sa sl = Some cte; cteCap cte = c;
-                        isFinal c sl (cteCaps_of sa); sl \<noteq> sl'; cteCaps_of sa sl' = Some cap';
-                        c = ArchObjectCap (IOPortCap f l)\<rbrakk>
-                     \<Longrightarrow> cap_ioports' c \<inter> cap_ioports' cap' = {}"
-    apply (clarsimp simp: isFinal_def sameObjectAs_def2 isCap_simps valid_ioports'_def ioports_no_overlap'_def)
-    apply (drule_tac x=sl' in spec)
-    apply (drule_tac x="cap'" in spec)
-    apply clarsimp
-    apply (drule_tac x=cap' in bspec, fastforce)
-    apply (drule_tac x="cteCap cte" in bspec, fastforce simp: cteCaps_of_def)
-    apply (case_tac "cap'"; clarsimp)
-    by (rename_tac az, case_tac az; clarsimp)
+    "\<And>f l sl sl' s. \<lbrakk> isFinal (ArchObjectCap (IOPortCap f l)) sl (cteCaps_of s); sl \<noteq> sl' \<rbrakk>
+                    \<Longrightarrow> cteCaps_of s sl' \<noteq> Some (ArchObjectCap (IOPortCap f l))"
+    apply (clarsimp simp: isFinal_def sameObjectAs_def2 isCap_simps)
+    apply fastforce
+    done
   from stuff have stuff':
     "finalise_prop_stuff (no_cte_prop Pr)"
     by (simp add: no_cte_prop_def finalise_prop_stuff_def)
@@ -6384,10 +6352,9 @@ proof (induct arbitrary: P p rule: finalise_spec_induct2)
          apply (clarsimp simp: final_IRQHandler_no_copy)
          apply (drule (1) ctes_of_valid'[OF _ invs_valid_objs'])
          apply (clarsimp simp: valid_cap'_def)
-        apply (rename_tac ac, case_tac ac; clarsimp simp: isCap_simps)
-         apply (rule context_conjI, drule (1) ctes_of_valid'[OF _ invs_valid_objs'], clarsimp simp: valid_cap'_def)
+        apply (rename_tac ac, case_tac ac; clarsimp simp: isCap_simps final_IOPort_no_copy)
+         apply (drule (1) ctes_of_valid'[OF _ invs_valid_objs'], clarsimp simp: valid_cap'_def)
         apply clarsimp
-        apply (drule_tac sl=sl in final_IOPort_no_copy[OF invs_valid_ioports'], assumption+, simp+)
        apply (clarsimp dest!: isCapDs)
        apply (rule conjI)
         apply (clarsimp simp: capRemovable_def)
@@ -8688,30 +8655,6 @@ lemma cteMove_irq_handlers' [wp]:
   apply (auto simp: cteCaps_of_def weak_derived'_def)
   done
 
-lemma cteMove_ioports' [wp]:
-  "\<lbrace>\<lambda>s. valid_ioports' s
-      \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) cap) src s
-      \<and> cte_wp_at' (\<lambda>c. cteCap c = NullCap) dest s\<rbrace>
-     cteMove cap src dest
-   \<lbrace>\<lambda>rv. valid_ioports'\<rbrace>"
-  apply (simp add: valid_ioports'_simps)
-  apply (rule hoare_pre)
-   apply (rule hoare_use_eq [where f=ksArchState, OF cteMove_ksArch])
-   apply (simp add: cteMove_def)
-   apply (wp getCTE_wp)
-  apply (clarsimp simp: cte_wp_at_ctes_of cteCaps_of_def ran_def)
-  apply (clarsimp simp add: modify_map_def split: if_split_asm dest!: weak_derived_cap_ioports')
-  apply (rule conjI, clarsimp)
-   apply (rule conjI, clarsimp)
-    apply blast
-   subgoal by ((auto | blast)+)
-  apply clarsimp
-  apply (rule conjI, clarsimp)
-   subgoal by (auto | blast)+
-  apply clarsimp
-  apply safe
-  by distinct_subgoals ((auto | blast)+)
-
 lemmas cteMove_valid_irq_node'[wp]
     = valid_irq_node_lift[OF cteMove_ksInterrupt cteMove_typ_at']
 
@@ -9059,19 +9002,6 @@ lemma updateCap_noop_irq_handlers:
                 add: modify_map_apply fun_upd_idem)
   done
 
-lemma updateCap_noop_ioports':
-  "\<lbrace>valid_ioports' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot\<rbrace>
-     updateCap slot cap
-   \<lbrace>\<lambda>rv. valid_ioports'\<rbrace>"
-  apply (simp add: valid_ioports'_simps irq_issued'_def)
-  apply (rule hoare_pre)
-   apply (rule hoare_use_eq[where f=ksArchState, OF updateCap_arch])
-   apply wp
-  apply (simp, subst(asm) tree_cte_cteCap_eq[unfolded o_def])
-  apply (simp split: option.split_asm
-                add: modify_map_apply fun_upd_idem)
-  done
-
 crunch updateCap
   for ct_idle_or_in_cur_domain'[wp]: ct_idle_or_in_cur_domain'
   (rule: ct_idle_or_in_cur_domain'_lift2)
@@ -9084,7 +9014,7 @@ lemma updateCap_noop_invs:
                    valid_pspace'_def valid_mdb'_def)
   apply (rule hoare_pre)
    apply (wp updateCap_ctes_of_wp updateCap_iflive'
-             updateCap_ifunsafe' updateCap_idle' updateCap_noop_ioports'
+             updateCap_ifunsafe' updateCap_idle'
              valid_arch_state_lift' valid_irq_node_lift
              updateCap_noop_irq_handlers sch_act_wf_lift
              untyped_ranges_zero_lift)
@@ -9113,12 +9043,9 @@ lemma invokeCNode_invs' [wp]:
   unfolding invokeCNode_def
   apply (cases cinv)
         apply (wp cteRevoke_invs' cteInsert_invs | simp split del: if_split)+
-        apply (rule conjI)
-         apply (clarsimp simp: cte_wp_at_ctes_of is_derived'_def isCap_simps badge_derived'_def)
-         apply (erule(1) valid_irq_handlers_ctes_ofD)
-         apply (clarsimp simp: invs'_def valid_state'_def)
-        apply clarsimp
-        apply (erule (1) valid_ioports'_derivedD[OF invs_valid_ioports'])
+        apply (clarsimp simp: cte_wp_at_ctes_of is_derived'_def isCap_simps badge_derived'_def)
+        apply (erule(1) valid_irq_handlers_ctes_ofD)
+        apply (clarsimp simp: invs'_def valid_state'_def)
        defer
        apply (wp cteRevoke_invs' | simp)+
       apply (clarsimp simp:cte_wp_at_ctes_of)