squash arm access: update for relaxed conditions

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>

Author: corlewis

proof/access-control/Syscall_AC.thy

@@ -402,9 +402,7 @@ lemma handle_reply_respects:
 
 
 lemma thread_set_time_slice_pas_refined[wp]:
-  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace>
-   thread_set_time_slice tptr time
-   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
+  "thread_set_time_slice tptr time \<lbrace>pas_refined aag\<rbrace>"
   by (simp add: thread_set_time_slice_def | wp thread_set_pas_refined)+
 
 lemma dec_domain_time_pas_refined[wp]:
@@ -583,8 +581,7 @@ lemma dec_domain_time_integrity[wp]:
   done
 
 lemma timer_tick_integrity[wp]:
-  "\<lbrace>integrity aag X st and pas_refined aag and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s))
-    and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace>
+  "\<lbrace>integrity aag X st and pas_refined aag and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s))\<rbrace>
    timer_tick
    \<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
   apply (simp add: timer_tick_def)
@@ -616,8 +613,6 @@ lemma handle_interrupt_integrity_autarch:
                        ackInterrupt_device_state_inv resetTimer_device_state_inv
                        handle_reserved_irq_integrity_autarch
                  simp: get_irq_slot_def get_irq_state_def)+
-  apply (rule conjI[rotated], fastforce) \<comment> \<open>IRQTimer preconditions\<close>
-  apply clarsimp
   apply (rule conjI, fastforce)+ \<comment> \<open>valid_objs etc.\<close>
   apply (clarsimp simp: cte_wp_at_caps_of_state)
   apply (rule_tac s = s in hacky_ipc_Send [where irq = irq])

proof/access-control/Tcb_AC.thy

@@ -134,9 +134,7 @@ lemma set_priority_integrity_autarch[wp]:
   by (simp add: set_priority_def | wp)+
 
 lemma set_priority_pas_refined[wp]:
-  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace>
-   set_priority tptr prio
-   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
+  "set_priority tptr prio \<lbrace>pas_refined aag\<rbrace>"
   unfolding set_priority_def thread_set_priority_def
   by (wpsimp wp: thread_set_pas_refined)