rt riscv ainvs: set handler params when configuring TCBs

This updates ainvs after modifying the tcb_decode functions so that it
is possible to set the badge and rights of fault and timeout handler caps.

Signed-off-by: Corey Lewis <[email protected]>

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/ArchTcb_AI.thy

@@ -93,7 +93,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>
                                   vspace_asid c = vspace_asid new_cap) src_slot)\<rbrace>
@@ -128,7 +128,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 *)
@@ -240,26 +240,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
@@ -296,15 +296,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
-                      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)
+    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
+            | 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 is_cnode_or_valid_arch_def)
 
 lemma tcc_invs[Tcb_AI_asms]:
@@ -331,21 +332,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)
@@ -354,9 +355,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"
@@ -396,7 +398,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)
@@ -466,10 +467,20 @@ 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
+                  split: cap.split)
+  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
+                  split: cap.split arch_cap.split)
   apply simp
   done