a few more fixups, squash into main commit

Signed-off-by: Michael McInerney <[email protected]>
seL4 · Dec 19, 2024 · 747ada7 · 747ada7
1 parent 8676d46
commit 747ada7
Show file tree

Hide file tree

Showing 5 changed files with 8 additions and 11 deletions.
diff --git a/proof/invariant-abstract/AInvs.thy b/proof/invariant-abstract/AInvs.thy
@@ -2513,7 +2513,6 @@ lemma call_kernel_cur_sc_offset_ready_and_sufficient:
    \<lbrace>\<lambda>_ s :: det_state. cur_sc_offset_ready (consumed_time s) s
                        \<and> cur_sc_offset_sufficient (consumed_time s) s\<rbrace>"
   (is "\<lbrace>_\<rbrace> _ \<lbrace>\<lambda>_. ?Q\<rbrace>")
-  supply comp_apply[simp del]
   apply (clarsimp simp: call_kernel_def)
   apply (simp flip: bind_assoc)
   apply (rule_tac Q'="\<lambda>_. ?Q" in bind_wp)

diff --git a/proof/invariant-abstract/ARM/ArchDetSchedAux_AI.thy b/proof/invariant-abstract/ARM/ArchDetSchedAux_AI.thy
@@ -72,8 +72,8 @@ lemma set_asid_pool_ntfns_of[wp]:
   "set_asid_pool ptr pool \<lbrace>\<lambda>s. P (ntfns_of s)\<rbrace>"
   by (set_object_easy_cases def: set_asid_pool_def)
 
-lemma set_asid_pool_prios_of[wp]:
-  "set_asid_pool ptr pool \<lbrace>\<lambda>s. P (prios_of s)\<rbrace>"
+lemma set_asid_pool_tcbs_of[wp]:
+  "set_asid_pool ptr pool \<lbrace>\<lambda>s. P (tcbs_of s)\<rbrace>"
   by (set_object_easy_cases def: set_asid_pool_def)
 
 lemma set_asid_pool_bound_sc_obj_tcb_at[wp]:

diff --git a/proof/invariant-abstract/ARM/ArchDetSchedSchedule_AI.thy b/proof/invariant-abstract/ARM/ArchDetSchedSchedule_AI.thy
@@ -60,7 +60,7 @@ lemma misc_dmo_valid_sched_pred_strong[wp]:
 crunch arch_switch_to_thread, arch_switch_to_idle_thread, arch_finalise_cap,
        arch_invoke_irq_control
   for valid_sched_pred_strong[wp, DetSchedSchedule_AI_assms]: "valid_sched_pred_strong P"
-  (wp: dmo_valid_sched_pred crunch_wps simp: crunch_simps simp_del: comp_apply)
+  (wp: dmo_valid_sched_pred crunch_wps simp: crunch_simps)
 
 lemma handle_vm_fault_valid_sched_pred_strong[wp, DetSchedSchedule_AI_assms]:
   "handle_vm_fault thread fault_type \<lbrace>valid_sched_pred_strong P\<rbrace>"
@@ -70,8 +70,7 @@ crunch
   perform_page_table_invocation, perform_page_directory_invocation,
   perform_page_invocation, perform_asid_pool_invocation
   for valid_sched_misc[wp]: "valid_sched_pred_strong P"
-  (wp: dmo_valid_sched_pred crunch_wps simp: crunch_simps detype_def ignore: do_machine_op
-   simp_del: comp_apply)
+  (wp: dmo_valid_sched_pred crunch_wps simp: crunch_simps detype_def ignore: do_machine_op)
 
 crunch arch_perform_invocation
   for valid_sched_misc[wp, DetSchedSchedule_AI_assms]:

diff --git a/proof/invariant-abstract/RISCV64/ArchDetSchedAux_AI.thy b/proof/invariant-abstract/RISCV64/ArchDetSchedAux_AI.thy
@@ -47,8 +47,8 @@ lemma set_asid_pool_ntfns_of[wp]:
   "set_asid_pool ptr pool \<lbrace>\<lambda>s. P (ntfns_of s)\<rbrace>"
   by (set_object_easy_cases def: set_asid_pool_def)
 
-lemma set_asid_pool_prios_of[wp]:
-  "set_asid_pool ptr pool \<lbrace>\<lambda>s. P (prios_of s)\<rbrace>"
+lemma set_asid_pool_tcbs_of[wp]:
+  "set_asid_pool ptr pool \<lbrace>\<lambda>s. P (tcbs_of s)\<rbrace>"
   by (set_object_easy_cases def: set_asid_pool_def)
 
 lemma set_asid_pool_bound_sc_obj_tcb_at[wp]:

diff --git a/proof/invariant-abstract/RISCV64/ArchDetSchedSchedule_AI.thy b/proof/invariant-abstract/RISCV64/ArchDetSchedSchedule_AI.thy
@@ -43,7 +43,7 @@ lemma misc_dmo_valid_sched_pred_strong[wp]:
 crunch arch_switch_to_thread, arch_switch_to_idle_thread, arch_finalise_cap,
        arch_invoke_irq_control
   for valid_sched_pred_strong[wp, DetSchedSchedule_AI_assms]: "valid_sched_pred_strong P"
-  (wp: dmo_valid_sched_pred crunch_wps simp: crunch_simps simp_del: comp_apply)
+  (wp: dmo_valid_sched_pred crunch_wps simp: crunch_simps)
 
 lemma handle_vm_fault_valid_sched_pred_strong[wp, DetSchedSchedule_AI_assms]:
   "handle_vm_fault thread fault_type \<lbrace>valid_sched_pred_strong P\<rbrace>"
@@ -54,8 +54,7 @@ crunch
   perform_page_table_invocation,
   perform_page_invocation, perform_asid_pool_invocation
   for valid_sched_misc[wp]: "valid_sched_pred_strong P"
-  (wp: dmo_valid_sched_pred crunch_wps simp: crunch_simps detype_def ignore: do_machine_op
-   simp_del: comp_apply)
+  (wp: dmo_valid_sched_pred crunch_wps simp: crunch_simps detype_def ignore: do_machine_op)
 
 crunch arch_perform_invocation
   for valid_sched_misc[wp, DetSchedSchedule_AI_assms]: