squash aarch64 ainvs: minor cleanup

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
seL4 · Dec 11, 2024 · 1bc4f2a · 1bc4f2a
1 parent b9b3498
commit 1bc4f2a
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 2 deletions.
diff --git a/proof/invariant-abstract/AARCH64/ArchBCorres2_AI.thy b/proof/invariant-abstract/AARCH64/ArchBCorres2_AI.thy
@@ -153,7 +153,7 @@ crunch handle_hypervisor_fault, timer_tick
 lemma handle_event_bcorres[wp]: "bcorres (handle_event e) (handle_event e)"
   apply (cases e)
   apply (simp add: handle_send_def handle_call_def handle_recv_def handle_reply_def handle_yield_def
-                   handle_interrupt_def Let_def handle_reserved_irq_def arch_mask_irq_signal_def
+                   handle_interrupt_def Let_def arch_mask_irq_signal_def
          | intro impI conjI allI | wp | wpc)+
   done
 

diff --git a/proof/invariant-abstract/AARCH64/ArchRetype_AI.thy b/proof/invariant-abstract/AARCH64/ArchRetype_AI.thy
@@ -59,6 +59,7 @@ crunch init_arch_objects
   and valid_mdb[wp]: "valid_mdb"
   and cte_wp_at[wp]: "\<lambda>s. P (cte_wp_at P' p s)"
   and typ_at[wp]: "\<lambda>s. P (typ_at T p s)"
+  and cur_thread[wp]: "\<lambda>s. P (cur_thread s)"
   (ignore: clearMemory wp: crunch_wps)
 
 crunch store_pte

diff --git a/proof/invariant-abstract/AARCH64/ArchVSpaceEntries_AI.thy b/proof/invariant-abstract/AARCH64/ArchVSpaceEntries_AI.thy
@@ -299,7 +299,7 @@ lemma handle_event_valid_vspace_objs'[wp]:
   by (case_tac e; simp) (wpsimp simp: Let_def handle_vm_fault_def | wp (once) hoare_drop_imps)+
 
 lemma schedule_valid_vspace_objs'[wp]:
-  "\<lbrace>valid_vspace_objs'\<rbrace> schedule \<lbrace>\<lambda>_. valid_vspace_objs'\<rbrace>"
+  "schedule \<lbrace>valid_vspace_objs'\<rbrace>"
   unfolding schedule_def by (wpsimp wp: hoare_drop_imps)
 
 lemma call_kernel_valid_vspace_objs'[wp]: