Proofs for SGI API

proof/access-control/ARM/ArchAccess.thy

@@ -94,11 +94,12 @@ end
 context Arch begin
 
 primrec aobj_ref' where
-  "aobj_ref' (ASIDPoolCap p as) = {p}"
+  "aobj_ref' (ASIDPoolCap p _) = {p}"
 | "aobj_ref' ASIDControlCap = {}"
-| "aobj_ref' (PageCap isdev x rs sz as4) = ptr_range x (pageBitsForSize sz)"
-| "aobj_ref' (PageDirectoryCap x as2) = {x}"
-| "aobj_ref' (PageTableCap x as3) = {x}"
+| "aobj_ref' (PageCap isdev x _ sz _) = ptr_range x (pageBitsForSize sz)"
+| "aobj_ref' (PageDirectoryCap x _) = {x}"
+| "aobj_ref' (PageTableCap x _) = {x}"
+| "aobj_ref' (SGISignalCap _ _) = {}"
 
 fun acap_asid' :: "arch_cap \<Rightarrow> asid set" where
   "acap_asid' (PageCap _ _ _ _ mapping) = fst ` set_option mapping"
@@ -107,6 +108,7 @@ fun acap_asid' :: "arch_cap \<Rightarrow> asid set" where
 | "acap_asid' (ASIDPoolCap _ asid)
      = {x. asid_high_bits_of x = asid_high_bits_of asid \<and> x \<noteq> 0}"
 | "acap_asid' ASIDControlCap = UNIV"
+| "acap_asid' (SGISignalCap _ _) = {}"
 
 inductive_set state_asids_to_policy_aux for aag caps asid_tab vrefs where
   sata_asid:

proof/access-control/ARM/ArchArch_AC.thy

@@ -744,12 +744,18 @@ definition authorised_arch_inv :: "'a PAS \<Rightarrow> arch_invocation \<Righta
    | InvokePageDirectory pdi \<Rightarrow> authorised_page_directory_inv aag pdi
    | InvokePage pgi \<Rightarrow> authorised_page_inv aag pgi
    | InvokeASIDControl aci \<Rightarrow> authorised_asid_control_inv aag aci
-   | InvokeASIDPool api \<Rightarrow> authorised_asid_pool_inv aag api"
+   | InvokeASIDPool api \<Rightarrow> authorised_asid_pool_inv aag api
+   | InvokeSGISignal _ \<Rightarrow> True"
 
-crunch respects [wp]: perform_page_directory_invocation "integrity aag X st"
-  (ignore: do_machine_op)
+lemma ipiSendTarget_respects[wp]:
+  "do_machine_op (ipiSendTarget irq targets) \<lbrace>integrity aag X st\<rbrace>"
+  unfolding ipiSendTarget_def
+  by (wpsimp wp: dmo_mol_respects)
 
-crunch pas_refined [wp]: perform_page_directory_invocation "pas_refined aag"
+crunches perform_page_directory_invocation, perform_sgi_invocation
+  for pas_refined [wp]: "pas_refined aag"
+  and respects [wp]: "integrity aag X st"
+  (ignore: do_machine_op)
 
 lemma invoke_arch_respects:
   "\<lbrace>integrity aag X st and authorised_arch_inv aag ai and
@@ -829,7 +835,7 @@ lemma decode_arch_invocation_authorised:
    apply (wp whenE_throwError_wp check_vp_wpR find_pd_for_asid_authority2
           | wpc
           | simp add: authorised_asid_control_inv_def authorised_page_inv_def
-                      authorised_page_directory_inv_def
+                      authorised_page_directory_inv_def decode_sgi_signal_invocation_def
                  del: hoare_True_E_R
                  split del: if_split)+
   apply (clarsimp simp: authorised_asid_pool_inv_def authorised_page_table_inv_def

proof/access-control/ARM/ArchDomainSepInv.thy

@@ -83,12 +83,8 @@ lemma perform_asid_control_invocation_domain_sep_inv:
          | wpc | simp )+
   done
 
-lemma perform_asid_pool_invocation_domain_sep_inv:
-  "perform_asid_pool_invocation iv \<lbrace>domain_sep_inv irqs st\<rbrace>"
-  apply (simp add: perform_asid_pool_invocation_def)
-  apply (rule hoare_pre)
-  apply (wp set_cap_domain_sep_inv get_cap_wp | wpc | simp)+
-  done
+crunches perform_sgi_invocation, perform_asid_pool_invocation
+  for domain_sep_inv[wp]: "domain_sep_inv irqs st"
 
 lemma arch_perform_invocation_domain_sep_inv[DomainSepInv_assms]:
   "\<lbrace>domain_sep_inv irqs st and valid_arch_inv ai\<rbrace>
@@ -111,8 +107,7 @@ lemma arch_invoke_irq_control_domain_sep_inv[DomainSepInv_assms]:
   "\<lbrace>domain_sep_inv irqs st and arch_irq_control_inv_valid ivk\<rbrace>
    arch_invoke_irq_control ivk
    \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>"
-  apply (cases ivk)
-  apply (wpsimp wp: cap_insert_domain_sep_inv' simp: set_irq_state_def)
+  apply (cases ivk; wpsimp wp: cap_insert_domain_sep_inv' simp: set_irq_state_def)
    apply (rule_tac Q="\<lambda>_. domain_sep_inv irqs st and arch_irq_control_inv_valid ivk"
                 in hoare_strengthen_post[rotated])
     apply (fastforce simp: domain_sep_inv_def domain_sep_inv_cap_def arch_irq_control_inv_valid_def)

proof/access-control/ARM/ArchInterrupt_AC.thy

@@ -16,21 +16,24 @@ named_theorems Interrupt_AC_assms
 definition arch_authorised_irq_ctl_inv ::
   "'a PAS \<Rightarrow> Invocations_A.arch_irq_control_invocation \<Rightarrow> bool" where
   "arch_authorised_irq_ctl_inv aag cinv \<equiv>
-     case cinv of (ArchIRQControlIssue irq x1 x2 trigger) \<Rightarrow>
-       is_subject aag (fst x1) \<and> is_subject aag (fst x2) \<and>
-       (pasSubject aag, Control, pasIRQAbs aag irq) \<in> pasPolicy aag"
+     case cinv of
+       ArchIRQControlIssue irq x1 x2 trigger \<Rightarrow>
+         is_subject aag (fst x1) \<and> is_subject aag (fst x2) \<and>
+         (pasSubject aag, Control, pasIRQAbs aag irq) \<in> pasPolicy aag
+     | IssueSGISignal irq argets x1 x2 \<Rightarrow>
+        is_subject aag (fst x1) \<and> is_subject aag (fst x2)"
 
 lemma arch_invoke_irq_control_pas_refined[Interrupt_AC_assms]:
   "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state
                     and valid_mdb and arch_irq_control_inv_valid irq_ctl_inv
                     and K (arch_authorised_irq_ctl_inv aag irq_ctl_inv)\<rbrace>
    arch_invoke_irq_control irq_ctl_inv
    \<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
-  apply (cases irq_ctl_inv; simp)
-  apply (wpsimp wp: cap_insert_pas_refined_not_transferable)
-  apply (clarsimp simp: cte_wp_at_caps_of_state clas_no_asid cap_links_irq_def
-                        arch_authorised_irq_ctl_inv_def aag_cap_auth_def
-                        arch_irq_control_inv_valid_def)
+  apply (cases irq_ctl_inv;
+         wpsimp wp: cap_insert_pas_refined_not_transferable
+                simp: cte_wp_at_caps_of_state clas_no_asid cap_links_irq_def
+                      arch_authorised_irq_ctl_inv_def aag_cap_auth_def
+                      arch_irq_control_inv_valid_def)
   done
 
 lemma arch_invoke_irq_handler_pas_refined[Interrupt_AC_assms]:
@@ -43,9 +46,10 @@ lemma arch_invoke_irq_control_respects[Interrupt_AC_assms]:
   "\<lbrace>integrity aag X st and pas_refined aag and K (arch_authorised_irq_ctl_inv aag acinv)\<rbrace>
    arch_invoke_irq_control acinv
    \<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
-  apply (case_tac acinv, clarsimp simp add: setIRQTrigger_def arch_authorised_irq_ctl_inv_def)
-  apply (wpsimp wp: cap_insert_integrity_autarch aag_Control_into_owns_irq
-                    dmo_mol_respects do_machine_op_pas_refined)
+  apply (case_tac acinv;
+         wpsimp wp: cap_insert_integrity_autarch aag_Control_into_owns_irq
+                    dmo_mol_respects do_machine_op_pas_refined
+                simp: setIRQTrigger_def arch_authorised_irq_ctl_inv_def)
   done
 
 lemma integrity_irq_masks [iff]:

proof/access-control/DomainSepInv.thy

@@ -998,9 +998,7 @@ lemma thread_set_tcb_tcp_mcpriority_update_domain_sep_inv[wp]:
 lemma same_object_as_domain_sep_inv_cap:
   "\<lbrakk> same_object_as a cap; domain_sep_inv_cap irqs cap \<rbrakk>
      \<Longrightarrow> domain_sep_inv_cap irqs a"
-  apply (case_tac a, simp_all add: same_object_as_def domain_sep_inv_cap_def)
-  apply (case_tac cap, simp_all)
-  done
+  by (case_tac a, simp_all add: same_object_as_def domain_sep_inv_cap_def)
 
 lemma checked_cap_insert_domain_sep_inv:
   "check_cap_at a b (check_cap_at c d (cap_insert a b e)) \<lbrace>domain_sep_inv irqs st\<rbrace>"