Update ARM Access for det_ext changes

proof/access-control/ARM/ArchAccess.thy

@@ -88,6 +88,11 @@ lemmas state_vrefs_upd =
   revokable_update.state_vrefs
   machine_state_update.state_vrefs
   more_update.state_vrefs
+  scheduler_action_update.state_vrefs
+  domain_index_update.state_vrefs
+  cur_domain_update.state_vrefs
+  domain_time_update.state_vrefs
+  ready_queues_update.state_vrefs
 
 end
 
@@ -138,6 +143,7 @@ abbreviation integrity_asids_aux ::
      pp_opt = pp_opt' \<or> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of asid
                                  \<longrightarrow> pasASIDAbs aag asid' \<in> subjects)"
 
+\<comment> \<open>FIXME: could we define integrity_asids to operate on arch_state only?\<close>
 definition integrity_asids ::
   "'a PAS \<Rightarrow> 'a set \<Rightarrow> obj_ref \<Rightarrow> asid \<Rightarrow> 'y::state_ext state \<Rightarrow> 'z:: state_ext state  \<Rightarrow> bool" where
   "integrity_asids aag subjects x a s s' \<equiv>
@@ -159,6 +165,11 @@ lemmas integrity_asids_updates =
   interrupt_update.integrity_asids_update
   cur_thread_update.integrity_asids_update
   machine_state_update.integrity_asids_update
+  scheduler_action_update.integrity_asids_update
+  domain_index_update.integrity_asids_update
+  cur_domain_update.integrity_asids_update
+  domain_time_update.integrity_asids_update
+  ready_queues_update.integrity_asids_update
 
 (* The kheap isn't used in ARM's integrity_asids definition,
    but we need the following lemmas in some generic contexts *)

proof/access-control/ARM/ArchArch_AC.thy

@@ -1011,21 +1011,20 @@ lemma delete_asid_respects:
   by (wpsimp wp: set_asid_pool_respects_clear hoare_vcg_all_lift
            simp: obj_at_def pas_refined_refl delete_asid_def asid_pool_integrity_def)
 
-lemma authorised_arch_inv_sa_update:
+lemma authorised_arch_inv_sa_update[simp]:
   "authorised_arch_inv aag i (scheduler_action_update (\<lambda>_. act) s) =
    authorised_arch_inv aag i s"
   by (clarsimp simp: authorised_arch_inv_def authorised_page_inv_def authorised_slots_def
               split: arch_invocation.splits page_invocation.splits)
 
+crunch set_thread_state_act
+  for authorised_arch_inv[wp]: "authorised_arch_inv aag i"
+
 lemma set_thread_state_authorised_arch_inv[wp]:
   "set_thread_state ref ts \<lbrace>authorised_arch_inv aag i\<rbrace>"
   unfolding set_thread_state_def
-  apply (wpsimp wp: dxo_wp_weak)
-     apply (clarsimp simp: authorised_arch_inv_def authorised_page_inv_def authorised_slots_def
-                    split: arch_invocation.splits page_invocation.splits)
-    apply (wpsimp wp: set_object_wp)+
-  by (clarsimp simp: authorised_arch_inv_def authorised_page_inv_def authorised_slots_def
-              split: arch_invocation.splits page_invocation.splits)
+  apply (wpsimp wp: set_object_wp)
+  by (clarsimp simp: authorised_arch_inv_def)
 
 end
 

proof/access-control/ARM/ArchCNode_AC.thy

@@ -114,15 +114,12 @@ lemma list_integ_lift[CNode_AC_assms]:
     "\<lbrace>list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st and Q\<rbrace>
      f
      \<lbrace>\<lambda>_. list_integ (cdt_change_allowed aag {pasSubject aag}  (cdt st) (tcb_states_of_state st)) st\<rbrace>"
-  assumes ekh: "\<And>P. f \<lbrace>\<lambda>s. P (ekheap s)\<rbrace>"
-  assumes rq: "\<And>P. f \<lbrace>\<lambda>s. P (ready_queues s)\<rbrace>"
   shows "\<lbrace>integrity aag X st and Q\<rbrace> f \<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
   apply (rule hoare_pre)
    apply (unfold integrity_def[abs_def] integrity_asids_def)
    apply (simp only: integrity_cdt_list_as_list_integ)
-   apply (rule hoare_lift_Pf2[where f="ekheap"])
-    apply (simp add: tcb_states_of_state_def get_tcb_def)
-    apply (wp li[simplified tcb_states_of_state_def get_tcb_def] ekh rq)+
+   apply (simp add: tcb_states_of_state_def get_tcb_def)
+   apply (wp li[simplified tcb_states_of_state_def get_tcb_def])+
   apply (simp only: integrity_cdt_list_as_list_integ)
   apply (simp add: tcb_states_of_state_def get_tcb_def)
   done
@@ -374,16 +371,9 @@ lemma auth_graph_map_def2:
   "auth_graph_map f S = (\<lambda>(x, auth, y). (f x, auth, f y)) ` S"
   by (auto simp add: auth_graph_map_def image_def intro: rev_bexI)
 
-(* FIXME move to AInvs *)
-lemma store_pte_ekheap[wp]:
-  "store_pte p pte \<lbrace>\<lambda>s. P (ekheap s)\<rbrace>"
-  apply (simp add: store_pte_def set_pt_def)
-  apply (wp get_object_wp)
-  apply simp
-  done
-
 crunch store_pte
-  for asid_table_inv[wp]: "\<lambda>s. P (asid_table s)"
+  for etcbs_of[wp]: "\<lambda>s. P (etcbs_of s)"
+  and asid_table_inv[wp]: "\<lambda>s. P (asid_table s)"
 
 lemma store_pte_pas_refined[wp]:
   "\<lbrace>pas_refined aag and
@@ -501,13 +491,6 @@ lemma set_asid_pool_thread_bound_ntfns[wp]:
                  split: kernel_object.split_asm option.split)
   done
 
-(* FIXME move to AInvs *)
-lemma set_asid_pool_ekheap[wp]:
-  "set_asid_pool p pool \<lbrace>\<lambda>s. P (ekheap s)\<rbrace>"
-  apply (simp add: set_asid_pool_def)
-  apply (wp get_object_wp | simp)+
-  done
-
 lemma set_asid_pool_pas_refined[wp]:
   "\<lbrace>pas_refined aag and
     (\<lambda>s. \<forall>(x, y) \<in> graph_of pool.

proof/access-control/ARM/ArchIpc_AC.thy

@@ -17,6 +17,7 @@ declare handle_arch_fault_reply_typ_at[Ipc_AC_assms]
 
 crunch cap_insert_ext
   for integrity_asids[Ipc_AC_assms, wp]: "integrity_asids aag subjects x a st"
+  (ignore_del: cap_insert_ext) \<comment> \<open>FIXME: should these ext consts still be ignored in DetSched_AI files and beyond?\<close>
 
 lemma arch_derive_cap_auth_derived[Ipc_AC_assms]:
   "\<lbrace>\<top>\<rbrace> arch_derive_cap acap \<lbrace>\<lambda>rv _. rv \<noteq> NullCap \<longrightarrow> auth_derived rv (ArchObjectCap acap)\<rbrace>, -"
@@ -203,18 +204,15 @@ lemma list_integ_lift_in_ipc[Ipc_AC_assms]:
    "\<lbrace>list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st and Q\<rbrace>
     f
     \<lbrace>\<lambda>_. list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st\<rbrace>"
-  assumes ekh: "\<And>P. \<lbrace>\<lambda>s. P (ekheap s)\<rbrace> f \<lbrace>\<lambda>rv s. P (ekheap s)\<rbrace>"
-  assumes rq: "\<And>P. \<lbrace> \<lambda>s. P (ready_queues s) \<rbrace> f \<lbrace> \<lambda>rv s. P (ready_queues s) \<rbrace>"
   shows "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st and Q\<rbrace>
          f
          \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>"
   apply (unfold integrity_tcb_in_ipc_def integrity_def[abs_def])
   apply (simp del:split_paired_All)
   apply (rule hoare_pre)
    apply (simp only: integrity_cdt_list_as_list_integ)
-   apply (rule hoare_lift_Pf2[where f="ekheap"])
-    apply (simp add: tcb_states_of_state_def get_tcb_def)
-    apply (wp li[simplified tcb_states_of_state_def get_tcb_def] ekh rq)+
+   apply (simp add: tcb_states_of_state_def get_tcb_def)
+   apply (wp li[simplified tcb_states_of_state_def get_tcb_def])+
   apply (simp only: integrity_cdt_list_as_list_integ)
   apply (simp add: tcb_states_of_state_def get_tcb_def)
   done

proof/access-control/ARM/ArchRetype_AC.thy

@@ -17,7 +17,7 @@ lemma invs_mdb_cte':
 context retype_region_proofs begin interpretation Arch .
 
 lemma vs_refs_no_global_pts_default[simp]:
-  "vs_refs_no_global_pts (default_object ty dev us) = {}"
+  "vs_refs_no_global_pts (default_object ty dev us d) = {}"
   by (simp add: default_object_def default_arch_object_def tyunt
                 vs_refs_no_global_pts_def pde_ref2_def pte_ref_def
                 o_def
@@ -33,12 +33,25 @@ end
 
 context retype_region_proofs' begin interpretation Arch .
 
+\<comment> \<open>FIXME: move to pas_refined_state_objs_to_policy_subset?\<close>
+lemma pas_refined_subsets_tcb_domain_map_wellformed:
+  "\<lbrakk> pas_refined aag s;
+     state_objs_to_policy s' \<subseteq> state_objs_to_policy s;
+     state_asids_to_policy aag s' \<subseteq> state_asids_to_policy aag s;
+     state_irqs_to_policy aag s' \<subseteq> state_irqs_to_policy aag s;
+     tcb_domain_map_wellformed aag s \<Longrightarrow> tcb_domain_map_wellformed aag s';
+     interrupt_irq_node s' = interrupt_irq_node s \<rbrakk>
+     \<Longrightarrow> pas_refined aag s'"
+  by (simp add: pas_refined_def)
+     (blast dest: auth_graph_map_mono[where G="pasObjectAbs aag"])
+
 lemma pas_refined:
-  "\<lbrakk> invs s; pas_refined aag s \<rbrakk> \<Longrightarrow> pas_refined aag s'"
-  apply (erule pas_refined_state_objs_to_policy_subset)
-     apply (simp add: state_objs_to_policy_def refs_eq vrefs_eq mdb_and_revokable)
-     apply (rule subsetI, rename_tac x, case_tac x, simp)
-     apply (erule state_bits_to_policy.cases)
+  "\<lbrakk> invs s; pas_refined aag s; pas_cur_domain aag s; \<forall>x\<in> set (retype_addrs ptr ty n us). is_subject aag x \<rbrakk>
+   \<Longrightarrow> pas_refined aag s'"
+  apply (erule pas_refined_subsets_tcb_domain_map_wellformed)
+      apply (simp add: state_objs_to_policy_def refs_eq vrefs_eq mdb_and_revokable)
+      apply (rule subsetI, rename_tac x, case_tac x, simp)
+      apply (erule state_bits_to_policy.cases)
             apply (solves \<open>auto intro!: sbta_caps intro: caps_retype split: cap.split\<close>)
            apply (solves \<open>auto intro!: sbta_untyped intro: caps_retype split: cap.split\<close>)
           apply (blast intro: state_bits_to_policy.intros)
@@ -57,7 +70,7 @@ lemma pas_refined:
     apply clarsimp
     apply (erule state_irqs_to_policy_aux.cases)
     apply (solves\<open>auto intro!: sita_controlled intro: caps_retype split: cap.split\<close>)
-   apply (rule domains_of_state)
+   apply (erule (2) tcb_domain_map_wellformed)
   apply simp
   done
 
@@ -427,7 +440,7 @@ lemma retype_region_integrity_asids[Retype_AC_assms]:
      \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; integrity_asids aag {pasSubject aag} x a s st \<rbrakk>
      \<Longrightarrow> integrity_asids aag {pasSubject aag} x a s
            (st\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api typ o_bits)) ` {0 ..< n}
-                            then Some (default_object typ dev o_bits)
+                            then Some (default_object typ dev o_bits d)
                             else kheap s a\<rparr>)"
   by clarsimp
 

proof/access-control/ARM/ArchTcb_AC.thy

@@ -32,14 +32,12 @@ lemma invoke_tcb_tc_respects_aag[Tcb_AC_assms]:
   apply (rule hoare_gen_asm)+
   apply (subst invoke_tcb.simps)
   apply (subst option_update_thread_def)
-  apply (subst set_priority_extended.dxo_eq)
   apply (rule hoare_weaken_pre)
    apply (rule_tac P="case ep of Some v \<Rightarrow> length v = word_bits | _ \<Rightarrow> True"
                  in hoare_gen_asm)
    apply (simp only: split_def)
    apply (((simp add: conj_comms,
            strengthen imp_consequent[where Q="x = None" for x], simp cong: conj_cong)
-          | strengthen invs_psp_aligned invs_vspace_objs invs_arch_state
           | rule wp_split_const_if wp_split_const_if_R hoare_vcg_all_liftE_R
                  hoare_vcg_conj_elimE hoare_vcg_const_imp_liftE_R hoare_vcg_conj_liftE_R
           | wp restart_integrity_autarch set_mcpriority_integrity_autarch
@@ -79,7 +77,8 @@ lemma invoke_tcb_tc_respects_aag[Tcb_AC_assms]:
           | simp add: ran_tcb_cap_cases dom_tcb_cap_cases[simplified]
                       emptyable_def a_type_def partial_inv_def
           | wpc
-          | strengthen invs_mdb use_no_cap_to_obj_asid_strg
+          | strengthen invs_psp_aligned invs_vspace_objs invs_arch_state
+                       invs_mdb use_no_cap_to_obj_asid_strg
                        tcb_cap_always_valid_strg[where p="tcb_cnode_index 0"]
                        tcb_cap_always_valid_strg[where p="tcb_cnode_index (Suc 0)"]))+
   apply (clarsimp simp: authorised_tcb_inv_def)