x64 ainvs: prove uniqueness of IOPortControlCaps

This invariant is currently proved on the Haskell level only. This
commit is in preparation of removing the invariant from the Haskell
level, crossing it over via assertions.

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

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
 

proof/invariant-abstract/X64/ArchCSpace_AI.thy

@@ -419,30 +419,54 @@ lemma cap_insert_derived_ioports:
   apply (drule_tac cap=cap in valid_ioports_issuedD, simp+)
   done
 
+lemma is_derived_not_ioport_control:
+  "is_derived (cdt s) src cap cap' \<Longrightarrow> cap \<noteq> ArchObjectCap IOPortControlCap"
+  by (clarsimp simp add: is_derived_def is_derived_arch_def split: if_splits)
+
+lemma cap_insert_derived_ioport_control:
+  "\<lbrace>ioport_control_unique and (\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s)\<rbrace>
+     cap_insert cap src dest
+   \<lbrace>\<lambda>rv. ioport_control_unique\<rbrace>"
+  unfolding cap_insert_def set_untyped_cap_as_full_def
+  apply (wpsimp wp: get_cap_wp)
+  apply (auto dest!: is_derived_not_ioport_control
+              simp: cte_wp_at_caps_of_state ioport_control_unique_def is_cap_simps)
+  done
+
 lemma cap_insert_derived_valid_arch_state[CSpace_AI_assms]:
   "\<lbrace>valid_arch_state and (\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s)\<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_derived_ioports)+
+  by (wp valid_arch_state_lift_ioports_aobj_at cap_insert_aobj_at cap_insert_derived_ioports
+         cap_insert_derived_ioport_control)+
      (simp add: cap_insert_aobj_at valid_arch_state_def)
 
 lemma cap_insert_simple_ioports:
   "\<lbrace>valid_ioports and (\<lambda>s. cte_wp_at (\<lambda>cap'. safe_ioport_insert cap cap' s) dest s) and
         K (is_simple_cap cap \<and> \<not>is_ap_cap cap)\<rbrace>
-     cap_insert cap src dest
+   cap_insert cap src dest
    \<lbrace>\<lambda>rv. valid_ioports\<rbrace>"
   apply (simp add: cap_insert_def)
   apply (wp get_cap_wp set_cap_ioports_safe set_untyped_cap_as_full_ioports
             set_untyped_cap_as_full_gross_ioports
          | wpc | simp split del: if_splits)+
   done
 
+lemma cap_insert_simple_ioport_control:
+  "\<lbrace>ioport_control_unique and K (is_simple_cap cap)\<rbrace>
+   cap_insert cap src dest
+   \<lbrace>\<lambda>rv. ioport_control_unique\<rbrace>"
+  unfolding cap_insert_def set_untyped_cap_as_full_def
+  by (wpsimp wp: get_cap_wp)
+     (auto simp: cte_wp_at_caps_of_state is_simple_cap_def ioport_control_unique_def)
+
 lemma cap_insert_simple_valid_arch_state:
   "\<lbrace>valid_arch_state and (\<lambda>s. cte_wp_at (\<lambda>cap'. safe_ioport_insert cap cap' s) dest s) and
     K (is_simple_cap cap \<and> \<not>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_simple_ioports)+
+  by (wp valid_arch_state_lift_ioports_aobj_at cap_insert_aobj_at cap_insert_simple_ioports
+         cap_insert_simple_ioport_control)+
      (simp add: valid_arch_state_def)
 
 end
@@ -629,6 +653,11 @@ lemma setup_reply_master_ioports[wp]:
   apply (wpsimp simp: setup_reply_master_def wp: set_cap_ioports_no_new_ioports get_cap_wp)
   by (clarsimp simp: cte_wp_at_caps_of_state)
 
+lemma setup_reply_master_arch_ioport_control[wp]:
+  "setup_reply_master t \<lbrace>ioport_control_unique\<rbrace>"
+  unfolding setup_reply_master_def
+  by (wpsimp wp: get_cap_wp simp: ioport_control_unique_def)
+
 lemma setup_reply_master_arch[CSpace_AI_assms]:
   "setup_reply_master t \<lbrace> valid_arch_state \<rbrace>"
   by (wp valid_arch_state_lift_ioports_typ_at setup_reply_master_ioports)+

proof/invariant-abstract/X64/ArchDetype_AI.thy

@@ -181,11 +181,15 @@ lemma tcb_arch_detype[detype_invs_proofs]:
 
 lemma valid_ioports_detype:
   "valid_ioports s \<Longrightarrow> valid_ioports (detype (untyped_range cap) s)"
-  apply (clarsimp simp: valid_ioports_def all_ioports_issued_def ioports_no_overlap_def issued_ioports_def more_update.caps_of_state_update)
-  apply (clarsimp simp: detype_def cap_ioports_def ran_def elim!: ranE split: if_splits cap.splits arch_cap.splits)
-  apply (rule conjI)
-   apply (force simp: ran_def)
-  by (metis (full_types) ranI)
+  apply (clarsimp simp: valid_ioports_def all_ioports_issued_def ioports_no_overlap_def
+                        issued_ioports_def)
+  apply (clarsimp simp: detype_def cap_ioports_def ran_def)
+  by blast
+
+lemma ioport_control_detype:
+  "ioport_control_unique_2 caps \<Longrightarrow>
+   ioport_control_unique_2 (\<lambda>p. if fst p \<in> S then None else caps p)"
+  by (auto simp: ioport_control_unique_2_def)
 
 lemma valid_arch_state_detype[detype_invs_proofs]:
   "valid_arch_state (detype (untyped_range cap) s)"
@@ -194,7 +198,7 @@ lemma valid_arch_state_detype[detype_invs_proofs]:
   apply (strengthen valid_ioports_detype,
          simp add: valid_arch_state_def valid_asid_table_def
                    valid_global_pdpts_def valid_global_pds_def valid_global_pts_def
-                   global_refs_def cap_range_def)
+                   global_refs_def cap_range_def ioport_control_detype)
   apply (clarsimp simp: ran_def arch_state_det)
   apply (drule vs_lookup_atI)
   apply (drule (1) valid_vs_lookupD[OF vs_lookup_pages_vs_lookupI])

proof/invariant-abstract/X64/ArchInvariants_AI.thy

@@ -1051,6 +1051,21 @@ definition
 where
   "valid_x64_irq_state irqState \<equiv> \<forall>irq > maxIRQ. irqState irq = IRQFree"
 
+
+(* Mainly used to discharge the Haskell assertion archMDBAssertions, which is
+   used in CRefine. The invariant says that there is only one IOPortControlCap
+   in the system. *)
+definition ioport_control_unique_2 :: "(cslot_ptr \<Rightarrow> cap option) \<Rightarrow> bool" where
+  "ioport_control_unique_2 caps \<equiv>
+     \<forall>p p'. caps p = Some (ArchObjectCap IOPortControlCap) \<longrightarrow>
+            caps p' = Some (ArchObjectCap IOPortControlCap) \<longrightarrow>
+            p' = p"
+
+locale_abbrev ioport_control_unique where
+  "ioport_control_unique s \<equiv> ioport_control_unique_2 (caps_of_state s)"
+
+lemmas ioport_control_unique_def = ioport_control_unique_2_def
+
 definition
   valid_arch_state :: "'z::state_ext state \<Rightarrow> bool"
 where
@@ -1062,6 +1077,7 @@ where
       \<and> valid_global_pdpts s
       \<and> valid_cr3 (x64_current_cr3 (arch_state s))
       \<and> valid_x64_irq_state (x64_irq_state (arch_state s))
+      \<and> ioport_control_unique s
       \<and> valid_ioports s"
 
 definition
@@ -1778,23 +1794,23 @@ lemma valid_arch_state_lift:
    apply (wp arch typs caps hoare_vcg_conj_lift hoare_vcg_const_Ball_lift)+
   done
 
-(* we usually have a rule for valid_ioports, but it often comes with side-conditions *)
+(* we usually have a rule for valid_ioports and ioport_control_unique, but they often come with
+   side-conditions *)
 lemma valid_arch_state_lift_ioports_typ_at:
-  fixes Q
   assumes typs: "\<And>T p. \<lbrace>typ_at (AArch T) p\<rbrace> f \<lbrace>\<lambda>_. typ_at (AArch T) p\<rbrace>"
   assumes arch: "\<And>P. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (arch_state s)\<rbrace>"
   assumes ports: "\<lbrace> Q \<rbrace> f \<lbrace>\<lambda>_. valid_ioports \<rbrace>"
-  shows "\<lbrace>valid_arch_state and Q\<rbrace> f \<lbrace>\<lambda>_. valid_arch_state\<rbrace>"
-  apply (simp add: valid_arch_state_def pred_conj_def)
+  assumes control: "\<lbrace> P \<rbrace> f \<lbrace>\<lambda>_. ioport_control_unique\<rbrace>"
+  shows "\<lbrace>valid_arch_state and Q and P\<rbrace> f \<lbrace>\<lambda>_. valid_arch_state\<rbrace>"
   apply (simp add: valid_arch_state_def valid_asid_table_def
                    valid_global_pts_def valid_global_pds_def valid_global_pdpts_def)
-  (* we need to do this piece-wise so we can grab
-     `valid_ioports_2 (caps_of_state x) (arch_state x) \<and> Q x` at the end *)
-  apply (rule hoare_vcg_conj_lift[rotated])+
-  apply (solves \<open>wpsimp wp: ports\<close>)
-  (* the rest are trivial once arch_state is lifted out *)
-  apply (rule hoare_lift_Pf2[where f="\<lambda>s. arch_state s", OF _ arch],
-         solves \<open>wp typs hoare_vcg_conj_lift hoare_vcg_const_Ball_lift\<close>)+
+  apply wp_pre
+   (* isolate the `valid_ioports_2 (caps_of_state s) (arch_state s)` at the end,
+      because we don't want wps to act on (arch_state s) there. *)
+   apply (rule hoare_vcg_conj_lift[rotated])+
+            apply (rule ports)
+           apply (wps arch | wp control typs hoare_vcg_op_lift)+
+  apply simp
   done
 
 lemma aobj_at_default_arch_cap_valid:

proof/invariant-abstract/X64/ArchIpc_AI.thy

@@ -442,6 +442,25 @@ lemma transfer_caps_loop_ioports:
   apply clarsimp
   done
 
+lemma transfer_caps_loop_ioport_control:
+  "\<lbrace>ioport_control_unique and valid_objs and valid_mdb and K (distinct slots)
+         and (\<lambda>s. \<forall>x \<in> set slots. real_cte_at x s \<and> cte_wp_at (\<lambda>cap. cap = cap.NullCap) x s)
+         and transfer_caps_srcs caps\<rbrace>
+   transfer_caps_loop ep buffer n caps slots mi
+   \<lbrace>\<lambda>rv. ioport_control_unique\<rbrace>"
+  apply (rule hoare_pre)
+   apply (rule transfer_caps_loop_presM[where vo=True and em=False and ex=False])
+     apply (wp cap_insert_derived_ioport_control)
+     apply (clarsimp simp: cte_wp_at_caps_of_state)
+    apply (wp valid_ioports_lift)
+   apply (clarsimp simp:cte_wp_at_caps_of_state|intro conjI ballI)+
+   apply (drule(1) bspec,clarsimp)
+   apply (frule(1) caps_of_state_valid)
+   apply (fastforce simp:valid_cap_def)
+  apply (drule(1) bspec)
+  apply clarsimp
+  done
+
 lemma transfer_caps_loop_valid_arch[Ipc_AI_2_assms]:
   "\<And>slots caps ep buffer n mi.
     \<lbrace>valid_arch_state and valid_objs and valid_mdb and K (distinct slots)
@@ -450,7 +469,7 @@ lemma transfer_caps_loop_valid_arch[Ipc_AI_2_assms]:
       transfer_caps_loop ep buffer n caps slots mi
     \<lbrace>\<lambda>_. valid_arch_state\<rbrace>"
   by (wpsimp wp: valid_arch_state_lift_ioports_aobj_at transfer_caps_loop_ioports
-                 transfer_caps_loop_aobj_at)
+                 transfer_caps_loop_ioport_control transfer_caps_loop_aobj_at)
      (simp add: valid_arch_state_def)
 
 lemma setup_caller_cap_aobj_at:
@@ -459,14 +478,22 @@ lemma setup_caller_cap_aobj_at:
   unfolding setup_caller_cap_def
   by (wpsimp wp: cap_insert_aobj_at sts.aobj_at)
 
+lemma setup_caller_cap_ioport_control[wp]:
+  "setup_caller_cap st rt grant \<lbrace>ioport_control_unique\<rbrace>"
+  unfolding setup_caller_cap_def cap_insert_def set_untyped_cap_as_full_def
+  apply (wpsimp wp: get_cap_wp split_del: if_split simp: cte_wp_at_caps_of_state)
+  apply (auto simp: ioport_control_unique_def)
+  done
+
 lemma setup_caller_cap_valid_arch[Ipc_AI_2_assms, wp]:
   "setup_caller_cap st rt grant \<lbrace>valid_arch_state\<rbrace>"
   by (wp valid_arch_state_lift_ioports_aobj_at[rotated -1] setup_caller_cap_ioports
-         setup_caller_cap_aobj_at)
+         setup_caller_cap_aobj_at)+
      (simp add: valid_arch_state_def)
 
 crunch do_ipc_transfer
   for ioports[wp]: "valid_ioports"
+  and ioport_control[wp]: "ioport_control_unique"
   (wp: crunch_wps hoare_vcg_const_Ball_lift transfer_caps_loop_ioports
    simp: zipWithM_x_mapM crunch_simps ball_conj_distrib )
 

proof/invariant-abstract/X64/ArchKHeap_AI.thy

@@ -541,17 +541,17 @@ lemma typ_at_lift:
      (wpsimp wp: aobj_at)
 
 lemma valid_arch_state_lift_ioports_aobj_at:
-  fixes P
   assumes ioports: "\<lbrace> P \<rbrace> f \<lbrace>\<lambda>_. valid_ioports \<rbrace>"
-  shows "\<lbrace>valid_arch_state and P\<rbrace> f \<lbrace>\<lambda>rv. valid_arch_state\<rbrace>"
+  assumes control: "\<lbrace> Q \<rbrace> f \<lbrace>\<lambda>_. ioport_control_unique \<rbrace>"
+  shows "\<lbrace>valid_arch_state and P and Q\<rbrace> f \<lbrace>\<lambda>rv. valid_arch_state\<rbrace>"
   apply (simp add: valid_arch_state_def)
   apply (rule hoare_vcg_conj_lift
          | wp valid_asid_table_lift typ_at_lift valid_global_pts_lift valid_global_pds_lift
             valid_global_pdpts_lift)+
-  apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch], wp)
-  apply (rule hoare_vcg_conj_lift)
-  apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch], wp)
-  apply (wp ioports)
+    apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch], wp)
+   apply (rule hoare_vcg_conj_lift)
+    apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch], wp)
+   apply (wp control ioports)
   apply simp
   done
 

proof/invariant-abstract/X64/ArchKernelInit_AI.thy

@@ -305,6 +305,8 @@ lemma invs_A:
     apply (clarsimp simp: valid_arch_state_def)
     apply (rule conjI)
      apply (clarsimp simp: valid_asid_table_def state_defs)
+    apply (prop_tac "ioport_control_unique init_A_st")
+     apply (simp add: caps_of_state_init_A_st_Null ioport_control_unique_def)
     apply (subgoal_tac "valid_ioports init_A_st")
      apply (simp add: valid_global_pts_def valid_global_pds_def valid_global_pdpts_def
                       valid_arch_state_def state_defs obj_at_def a_type_def