MCS: set handler params when configuring TCBs

proof/invariant-abstract/AInvs.thy

@@ -411,9 +411,9 @@ lemma invoke_tcb_schact_is_rct_imp_cur_sc_active:
       apply (intro conjI impI;
              clarsimp simp: is_cnode_or_valid_arch_is_cap_simps tcb_ep_slot_cte_wp_ats real_cte_at_cte
                      dest!: is_valid_vtable_root_is_arch_cap)
-         apply (all \<open>clarsimp simp: is_cap_simps cte_wp_at_caps_of_state valid_fault_handler_def\<close>)
+        apply (all \<open>clarsimp simp: is_cap_simps cte_wp_at_caps_of_state valid_fault_handler_def\<close>)
         apply (all \<open>clarsimp simp: obj_at_def is_tcb typ_at_eq_kheap_obj cap_table_at_typ\<close>)
-        by auto
+      by (auto simp: is_cap_simps dest: is_derived_ep_cap)
    apply (rename_tac target cnode_index cslot_ptr fault_handler mcp priority sc)
    apply (rule validE_valid)
    apply (rule_tac B= "\<lambda>_ s. (schact_is_rct s \<longrightarrow> cur_sc_active s) \<and> tcb_at target s"
@@ -1712,12 +1712,9 @@ lemma invoke_tcb_schact_is_rct_imp_ct_activatable:
                                ct_in_state_def pred_tcb_at_def obj_at_def
                         split: thread_state.splits)
              apply (case_tac "tcb_state tcb"; clarsimp)
-            apply (all \<open>clarsimp simp: is_cap_simps cte_wp_at_caps_of_state valid_fault_handler_def\<close>)
+           apply (all \<open>clarsimp simp: is_cap_simps cte_wp_at_caps_of_state valid_fault_handler_def\<close>)
            apply (all \<open>clarsimp simp: obj_at_def is_tcb typ_at_eq_kheap_obj cap_table_at_typ\<close>)
-           apply (metis (no_types, lifting) cap.simps(38) fst_conv is_obj_defs(3) o_apply obj_atI
-                                            option.simps(5) real_cte_at_not_tcb_at snd_conv)
-          apply auto
-         done
+           by (auto simp: is_cap_simps is_obj_defs dest: is_derived_ep_cap)
       apply (rule validE_valid)
       apply (rule_tac B="\<lambda>_ . ?Q" in hoare_vcg_seqE[rotated])
        apply (wpsimp wp: install_tcb_cap_schact_is_rct_imp_ct_activatable)

proof/invariant-abstract/ARM/ArchEmptyFail_AI.thy

@@ -47,7 +47,7 @@ crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: handle_fault
 crunch (empty_fail) empty_fail[wp]: decode_tcb_configure, decode_bind_notification, decode_unbind_notification,
   decode_set_priority, decode_set_mcpriority, decode_set_sched_params, decode_set_timeout_ep,
   decode_set_tls_base, decode_set_space
-  (simp: cap.splits arch_cap.splits split_def)
+  (simp: cap.splits arch_cap.splits split_def Let_def)
 
 lemma decode_tcb_invocation_empty_fail[wp]:
   "empty_fail (decode_tcb_invocation a b (ThreadCap p) d e)"

proof/invariant-abstract/ARM/ArchIpc_AI.thy

@@ -15,25 +15,28 @@ named_theorems Ipc_AI_assms
 lemma update_cap_data_closedform:
   "update_cap_data pres w cap =
    (case cap of
-     cap.EndpointCap r badge rights \<Rightarrow>
-       if badge = 0 \<and> \<not> pres then (cap.EndpointCap r (w && mask 28) rights) else cap.NullCap
-   | cap.NotificationCap r badge rights \<Rightarrow>
-       if badge = 0 \<and> \<not> pres then (cap.NotificationCap r (w && mask 28) rights) else cap.NullCap
-   | cap.CNodeCap r bits guard \<Rightarrow>
-       if word_bits < unat ((w >> 3) && mask 5) + bits
-       then cap.NullCap
-       else cap.CNodeCap r bits ((\<lambda>g''. drop (size g'' - unat ((w >> 3) && mask 5)) (to_bl g'')) ((w >> 8) && mask 18))
-   | cap.ThreadCap r \<Rightarrow> cap.ThreadCap r
-   | cap.DomainCap \<Rightarrow> cap.DomainCap
-   | cap.UntypedCap d p n idx \<Rightarrow> cap.UntypedCap d p n idx
-   | cap.NullCap \<Rightarrow> cap.NullCap
-   | cap.ReplyCap t rights \<Rightarrow> cap.ReplyCap t rights
-   | cap.SchedContextCap s n \<Rightarrow> cap.SchedContextCap s n
-   | cap.SchedControlCap \<Rightarrow> cap.SchedControlCap
-   | cap.IRQControlCap \<Rightarrow> cap.IRQControlCap
-   | cap.IRQHandlerCap irq \<Rightarrow> cap.IRQHandlerCap irq
-   | cap.Zombie r b n \<Rightarrow> cap.Zombie r b n
-   | cap.ArchObjectCap cap \<Rightarrow> cap.ArchObjectCap cap)"
+     EndpointCap r badge rights \<Rightarrow>
+       if badge = 0 \<and> \<not> pres then (EndpointCap r (w && mask badge_bits) rights) else NullCap
+   | NotificationCap r badge rights \<Rightarrow>
+       if badge = 0 \<and> \<not> pres then (NotificationCap r (w && mask badge_bits) rights) else NullCap
+   | CNodeCap r bits guard \<Rightarrow>
+       if word_bits < unat ((w >> cnode_padding_bits) && mask cnode_guard_size_bits) + bits
+       then NullCap
+       else CNodeCap r bits
+                     ((\<lambda>g''. drop (size g'' - unat ((w >> cnode_padding_bits) &&
+                                                    mask cnode_guard_size_bits)) (to_bl g''))
+                     ((w >> cnode_padding_bits + cnode_guard_size_bits) && mask 18))
+   | ThreadCap r \<Rightarrow> ThreadCap r
+   | DomainCap \<Rightarrow> DomainCap
+   | UntypedCap dev p n idx \<Rightarrow> UntypedCap dev p n idx
+   | NullCap \<Rightarrow> NullCap
+   | ReplyCap t rights \<Rightarrow> ReplyCap t rights
+   | SchedContextCap s n \<Rightarrow> SchedContextCap s n
+   | SchedControlCap \<Rightarrow> SchedControlCap
+   | IRQControlCap \<Rightarrow> IRQControlCap
+   | IRQHandlerCap irq \<Rightarrow> IRQHandlerCap irq
+   | Zombie r b n \<Rightarrow> Zombie r b n
+   | ArchObjectCap cap \<Rightarrow> ArchObjectCap cap)"
   apply (cases cap,
          simp_all only: cap.simps update_cap_data_def is_ep_cap.simps if_False if_True
                         is_ntfn_cap.simps is_cnode_cap.simps is_arch_cap_def word_size

proof/invariant-abstract/ARM/ArchTcb_AI.thy

@@ -104,7 +104,7 @@ lemma checked_insert_tcb_invs: (* arch specific *)
         and valid_cap new_cap
         and tcb_cap_valid new_cap (target, ref)
         and (\<lambda>s. valid_fault_handler new_cap
-                         \<longrightarrow> cte_wp_at (\<lambda>c. c = new_cap \<or> c = NullCap) src_slot s)
+                   \<longrightarrow> cte_wp_at (is_derived (cdt s) src_slot new_cap) src_slot s)
         and (cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap
                               \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and>
                                  pt_pd_asid c = pt_pd_asid new_cap) src_slot)\<rbrace>
@@ -140,7 +140,7 @@ lemma checked_insert_tcb_invs: (* arch specific *)
   apply (rule conjI)
    apply (erule disjE)
     apply (erule(1) checked_insert_is_derived, simp+)
-   apply (auto simp: is_cnode_or_valid_arch_def is_derived_def is_cap_simps valid_fault_handler_def)
+  apply (auto simp: is_cnode_or_valid_arch_def is_derived_def is_cap_simps valid_fault_handler_def)
   done
 
 lemma checked_insert_tcb_invs': (* arch specific *)
@@ -251,26 +251,26 @@ lemma install_tcb_cap_invs:
   "\<lbrace>invs and tcb_at target and
     (\<lambda>s. \<forall>new_cap src_slot.
        slot_opt = Some (new_cap, src_slot)
-         \<longrightarrow> K (is_cnode_or_valid_arch new_cap \<or>
-                valid_fault_handler new_cap) s
+         \<longrightarrow> K (is_cnode_or_valid_arch new_cap \<or> valid_fault_handler new_cap) s
           \<and> valid_cap new_cap s
           \<and> tcb_cap_valid new_cap (target, tcb_cnode_index n) s
           \<and> (valid_fault_handler new_cap
-               \<longrightarrow> cte_wp_at valid_fault_handler (target, tcb_cnode_index n) s
-               \<and> cte_wp_at (\<lambda>c. c = new_cap \<or> c = NullCap) src_slot s)
+               \<longrightarrow> cte_wp_at valid_fault_handler (target, tcb_cnode_index n) s)
+          \<and> (is_ep_cap new_cap \<longrightarrow> cte_wp_at (is_derived (cdt s) src_slot new_cap) src_slot s)
           \<and> (case tcb_cap_cases (tcb_cnode_index n) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> \<forall>st. restr target st new_cap)
           \<and> (tcb_cnode_index n = tcb_cnode_index 2 \<longrightarrow> (\<forall>ptr. valid_ipc_buffer_cap new_cap ptr))
           \<and> real_cte_at src_slot s \<and> no_cap_to_obj_dr_emp new_cap s)\<rbrace>
    install_tcb_cap target slot n slot_opt
    \<lbrace>\<lambda>_. invs\<rbrace>"
-  apply (simp add: install_tcb_cap_def)
+  unfolding install_tcb_cap_def
   apply (wpsimp wp: checked_insert_tcb_invs cap_delete_deletes
                     hoare_vcg_imp_lift_R
          | strengthen tcb_cap_always_valid_strg use_no_cap_to_obj_asid_strg
-         | wpsimp wp: cap_delete_ep)+
+         | wpsimp wp: cap_delete_is_derived_ep)+
   by (auto simp: typ_at_eq_kheap_obj cap_table_at_typ tcb_at_typ
                  is_cnode_or_valid_arch_def is_cap_simps real_cte_at_cte
-          elim!: cte_wp_at_weakenE)
+                 valid_fault_handler_def
+          elim!: notE[OF _ cte_wp_at_weakenE] is_derived_ep_cap)
 
 lemma install_tcb_cap_no_cap_to_obj_dr_emp[wp, Tcb_AI_asms]:
   "\<lbrace>no_cap_to_obj_dr_emp cap and
@@ -306,15 +306,16 @@ lemma install_tcb_frame_cap_invs:
    \<comment> \<open>non-exception case\<close>
    apply wpsimp
      apply (wpsimp wp: checked_insert_tcb_invs[where ref="tcb_cnode_index 2"])
-    apply (wpsimp wp: hoare_vcg_all_lift static_imp_wp
+    apply ((wpsimp wp: hoare_vcg_all_lift static_imp_wp
                       thread_set_tcb_ipc_buffer_cap_cleared_invs
                       thread_set_cte_wp_at_trivial[where Q="\<lambda>x. x", OF ball_tcb_cap_casesI]
-                      thread_set_ipc_tcb_cap_valid)
+                      thread_set_ipc_tcb_cap_valid
+            | wps)+)[1]
    apply((wpsimp wp: cap_delete_deletes
              hoare_vcg_const_imp_lift_R hoare_vcg_all_lift_R hoare_vcg_all_lift
              static_imp_wp static_imp_conj_wp
            | strengthen use_no_cap_to_obj_asid_strg
-           | wp cap_delete_ep)+)[1]
+           | wp cap_delete_is_derived_ep)+)[1]
   by (clarsimp simp: is_cap_simps' valid_fault_handler_def)
 
 lemma tcc_invs[Tcb_AI_asms]:
@@ -341,21 +342,21 @@ lemma tcc_invs[Tcb_AI_asms]:
      apply ((wpsimp wp: hoare_vcg_const_imp_lift_R hoare_vcg_all_lift_R
                         install_tcb_cap_invs
             | strengthen tcb_cap_always_valid_strg
-            | wp install_tcb_cap_cte_wp_at_ep)+)[1]
+            | wp install_tcb_cap_cte_wp_at_ep install_tcb_cap_is_derived_ep)+)[1]
     \<comment> \<open>install_tcb_cap 4\<close>
     apply (simp)
     apply (rule hoare_vcg_E_elim, wp install_tcb_cap_invs)
     apply ((wpsimp wp: hoare_vcg_const_imp_lift_R hoare_vcg_all_lift_R
                        install_tcb_cap_invs
            | strengthen tcb_cap_always_valid_strg
-           | wp install_tcb_cap_cte_wp_at_ep)+)[1]
+           | wp install_tcb_cap_cte_wp_at_ep install_tcb_cap_is_derived_ep)+)[1]
    \<comment> \<open>install_tcb_cap 3\<close>
    apply (simp)
    apply (rule hoare_vcg_E_elim, wp install_tcb_cap_invs)
    apply ((wpsimp wp: hoare_vcg_const_imp_lift_R hoare_vcg_all_lift_R
                       install_tcb_cap_invs
           | strengthen tcb_cap_always_valid_strg
-          | wp install_tcb_cap_cte_wp_at_ep)+)[1]
+          | wp install_tcb_cap_cte_wp_at_ep install_tcb_cap_is_derived_ep)+)[1]
   \<comment> \<open>cleanup\<close>
   apply (simp)
   apply (strengthen tcb_cap_always_valid_strg)
@@ -364,9 +365,10 @@ lemma tcc_invs[Tcb_AI_asms]:
   apply (intro conjI impI;
          clarsimp simp: is_cnode_or_valid_arch_is_cap_simps tcb_ep_slot_cte_wp_ats real_cte_at_cte
                  dest!: is_valid_vtable_root_is_arch_cap)
-      apply (all \<open>clarsimp simp: is_cap_simps cte_wp_at_caps_of_state\<close>)
+     apply (all \<open>clarsimp simp: is_cap_simps cte_wp_at_caps_of_state\<close>)
      apply (all \<open>clarsimp simp: obj_at_def is_tcb typ_at_eq_kheap_obj cap_table_at_typ\<close>)
-  by (auto simp: valid_ipc_buffer_cap valid_fault_handler_def)
+  by (auto simp: valid_ipc_buffer_cap valid_fault_handler_def is_cap_simps
+           dest: is_derived_ep_cap)
 
 crunches empty_slot
   for sc_tcb_sc_at[wp]: "sc_tcb_sc_at P target"
@@ -406,7 +408,6 @@ lemma tcs_invs[Tcb_AI_asms]:
    apply (intro conjI impI;
           (clarsimp simp: is_cnode_or_valid_arch_is_cap_simps tcb_ep_slot_cte_wp_ats real_cte_at_cte
                   dest!: is_valid_vtable_root_is_arch_cap)?)
-     apply (erule cte_wp_at_strengthen, simp)
     apply (clarsimp simp: obj_at_def is_ep is_tcb)
    apply (intro conjI; intro allI impI)
     apply (clarsimp simp: pred_tcb_at_def obj_at_def is_tcb)
@@ -476,10 +477,21 @@ lemma no_cap_to_obj_with_diff_ref_update_cap_data[Tcb_AI_asms]:
                                  = vs_cap_ref c")
    apply (simp add: no_cap_to_obj_with_diff_ref_def
                     update_cap_objrefs)
-  apply (clarsimp simp: update_cap_data_closedform
-                        table_cap_ref_def
-                        arch_update_cap_data_def
-                 split: cap.split)
+   apply (clarsimp simp: update_cap_data_closedform table_cap_ref_simps
+                  split: cap.splits)
+  apply simp
+  done
+
+lemma no_cap_to_obj_with_diff_ref_mask_cap[Tcb_AI_asms]:
+  "no_cap_to_obj_with_diff_ref c S s \<longrightarrow>
+    no_cap_to_obj_with_diff_ref (mask_cap R c) S s"
+  apply (case_tac "mask_cap R c = NullCap")
+   apply (simp add: no_cap_to_obj_with_diff_ref_Null del: mask_cap_Null)
+  apply (subgoal_tac "vs_cap_ref (mask_cap R c) = vs_cap_ref c")
+   apply (simp add: no_cap_to_obj_with_diff_ref_def)
+   apply (clarsimp simp: mask_cap_def cap_rights_update_def acap_rights_update_def
+                         table_cap_ref_simps
+                  split: cap.split arch_cap.split)
   apply simp
   done
 

proof/invariant-abstract/CSpace_AI.thy

@@ -3837,7 +3837,7 @@ locale CSpace_AI
     "\<And>rs cap. obj_refs (mask_cap rs cap) = obj_refs cap"
   assumes mask_cap_zobjrefs[simp]:
     "\<And>rs cap. zobj_refs (mask_cap rs cap) = zobj_refs cap"
-  assumes derive_cap_valid_cap:
+  assumes derive_cap_valid_cap[wp]:
     "\<And>cap slot.
       \<lbrace>valid_cap cap :: 'state_ext state \<Rightarrow> bool\<rbrace> derive_cap slot cap \<lbrace>valid_cap\<rbrace>,-"
   assumes valid_cap_update_rights[simp]:

proof/invariant-abstract/DetSchedSchedule_AI.thy

@@ -7722,7 +7722,7 @@ method invoke_tcb_install_tcb_cap_helper uses wp =
    ((wpsimp wp: hoare_vcg_const_imp_lift_R hoare_vcg_all_lift_R hoare_vcg_all_lift
                 install_tcb_cap_invs static_imp_wp static_imp_conj_wp wp
      | strengthen tcb_cap_always_valid_strg
-     | wp install_tcb_cap_cte_wp_at_ep)+)[1])
+     | wp install_tcb_cap_cte_wp_at_ep install_tcb_cap_is_derived_ep)+)[1])
 
 crunches restart_thread_if_no_fault
   for budget_sufficient[wp]: "budget_sufficient tp"
@@ -7871,9 +7871,9 @@ lemma tcc_valid_sched:
   apply (intro conjI impI;
          clarsimp simp: is_cnode_or_valid_arch_is_cap_simps tcb_ep_slot_cte_wp_ats real_cte_at_cte
                  dest!: is_valid_vtable_root_is_arch_cap)
-     apply (all \<open>clarsimp simp: is_cap_simps cte_wp_at_caps_of_state valid_fault_handler_def\<close>)
+    apply (all \<open>clarsimp simp: is_cap_simps cte_wp_at_caps_of_state valid_fault_handler_def\<close>)
     apply (all \<open>clarsimp simp: obj_at_def is_tcb typ_at_eq_kheap_obj cap_table_at_typ\<close>)
-    by auto
+  by (auto simp: is_cap_simps dest: is_derived_ep_cap)
 
 lemma restart_thread_if_no_fault_ct_in_state_neq:
   "\<lbrace>ct_in_state P and (\<lambda>s. t \<noteq> cur_thread s \<or> (P Inactive \<and> P Restart))\<rbrace>
@@ -17205,9 +17205,9 @@ lemma tcc_cur_sc_chargeable:
   apply (intro conjI impI;
          clarsimp simp: is_cnode_or_valid_arch_is_cap_simps tcb_ep_slot_cte_wp_ats real_cte_at_cte
                  dest!: is_valid_vtable_root_is_arch_cap)
-      apply (all \<open>clarsimp simp: is_cap_simps cte_wp_at_caps_of_state valid_fault_handler_def\<close>)
-     apply (all \<open>clarsimp simp: obj_at_def is_tcb typ_at_eq_kheap_obj cap_table_at_typ\<close>)
-  by auto
+    apply (all \<open>clarsimp simp: is_cap_simps cte_wp_at_caps_of_state valid_fault_handler_def\<close>)
+    apply (all \<open>clarsimp simp: obj_at_def is_tcb typ_at_eq_kheap_obj cap_table_at_typ\<close>)
+  by (auto simp: is_cap_simps dest: is_derived_ep_cap)
 
 crunches maybe_sched_context_unbind_tcb, maybe_sched_context_bind_tcb, set_priority
          , bind_notification
@@ -20616,9 +20616,9 @@ lemma tcc_ct_not_queued:
   apply (intro conjI impI;
          clarsimp simp: is_cnode_or_valid_arch_is_cap_simps tcb_ep_slot_cte_wp_ats real_cte_at_cte
                  dest!: is_valid_vtable_root_is_arch_cap)
-     apply (all \<open>clarsimp simp: is_cap_simps cte_wp_at_caps_of_state valid_fault_handler_def\<close>)
+    apply (all \<open>clarsimp simp: is_cap_simps cte_wp_at_caps_of_state valid_fault_handler_def\<close>)
     apply (all \<open>clarsimp simp: obj_at_def is_tcb typ_at_eq_kheap_obj cap_table_at_typ\<close>)
-  by auto
+  by (auto simp: is_cap_simps dest: is_derived_ep_cap)
 
 lemma invoke_tcb_ct_not_queuedE_E[wp]:
   "\<lbrace>ct_not_queued and invs and scheduler_act_sane and ct_not_blocked and tcb_inv_wf iv\<rbrace>
@@ -25471,16 +25471,16 @@ lemma invoke_tcb_ct_ready_if_schedulable[wp]:
          apply wpsimp
         apply wpsimp
            apply invoke_tcb_install_tcb_cap_helper+
-        apply simp
-        apply (strengthen tcb_cap_valid_ep_strgs)
-        apply (clarsimp cong: conj_cong)
-        apply (intro conjI impI;
-               clarsimp simp: is_cnode_or_valid_arch_is_cap_simps tcb_ep_slot_cte_wp_ats
-                              real_cte_at_cte ct_in_state_def
-                       dest!: is_valid_vtable_root_is_arch_cap)
-           apply (all \<open>clarsimp simp: is_cap_simps cte_wp_at_caps_of_state valid_fault_handler_def\<close>)
-          apply (all \<open>clarsimp simp: obj_at_def is_tcb typ_at_eq_kheap_obj cap_table_at_typ\<close>)
-          by auto
+       apply simp
+       apply (strengthen tcb_cap_valid_ep_strgs)
+       apply (clarsimp cong: conj_cong)
+       apply (intro conjI impI;
+              clarsimp simp: is_cnode_or_valid_arch_is_cap_simps tcb_ep_slot_cte_wp_ats
+                             real_cte_at_cte ct_in_state_def
+                      dest!: is_valid_vtable_root_is_arch_cap)
+         apply (all \<open>clarsimp simp: is_cap_simps cte_wp_at_caps_of_state valid_fault_handler_def\<close>)
+         apply (all \<open>clarsimp simp: obj_at_def is_tcb typ_at_eq_kheap_obj cap_table_at_typ\<close>)
+       by (auto simp: is_cap_simps dest: is_derived_ep_cap)
       subgoal for target slot fault_handler mcp priority sc
       apply (rule_tac Q="\<lambda>_ s. released_if_bound_sc_tcb_at (cur_thread s) s" in hoare_strengthen_post[rotated])
        apply (clarsimp simp: ct_ready_if_schedulable_def vs_all_heap_simps)

proof/invariant-abstract/RISCV64/ArchEmptyFail_AI.thy

@@ -42,7 +42,7 @@ crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: handle_fault
 crunch (empty_fail) empty_fail[wp]: decode_tcb_configure, decode_bind_notification, decode_unbind_notification,
   decode_set_priority, decode_set_mcpriority, decode_set_sched_params, decode_set_timeout_ep,
   decode_set_tls_base, decode_set_space
-  (simp: cap.splits arch_cap.splits split_def)
+  (simp: cap.splits arch_cap.splits split_def Let_def)
 
 lemma decode_tcb_invocation_empty_fail[wp]:
   "empty_fail (decode_tcb_invocation a b (ThreadCap p) d e)"