aarch64 ainvs: proof update for det_ext refactor

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

proof/invariant-abstract/AARCH64/ArchArch_AI.thy

@@ -1221,6 +1221,9 @@ lemma invoke_arch_invs[wp]:
   apply (wp perform_vcpu_invs|simp)+
   done
 
+crunch set_thread_state_act
+  for aobjs_of[wp]: "\<lambda>s. P (aobjs_of s)"
+
 lemma sts_aobjs_of[wp]:
   "set_thread_state t st \<lbrace>\<lambda>s. P (aobjs_of s)\<rbrace>"
   unfolding set_thread_state_def

proof/invariant-abstract/AARCH64/ArchBCorres2_AI.thy

@@ -16,11 +16,11 @@ named_theorems BCorres2_AI_assms
 
 crunch invoke_cnode
   for (bcorres) bcorres[wp, BCorres2_AI_assms]: truncate_state
-  (simp: swp_def ignore: clearMemory without_preemption filterM ethread_set)
+  (simp: swp_def ignore: clearMemory without_preemption filterM)
 
 crunch create_cap,init_arch_objects,retype_region,delete_objects
   for (bcorres) bcorres[wp]: truncate_state
-  (ignore: freeMemory clearMemory retype_region_ext)
+  (ignore: freeMemory clearMemory)
 
 crunch set_extra_badge,derive_cap
   for (bcorres) bcorres[wp]: truncate_state (ignore: storeWord)
@@ -29,7 +29,7 @@ crunch invoke_untyped
   for (bcorres) bcorres[wp]: truncate_state
   (ignore: sequence_x)
 
-crunch set_mcpriority
+crunch set_mcpriority, set_priority
   for (bcorres) bcorres[wp]: truncate_state
 
 crunch arch_get_sanitise_register_info, arch_post_modify_registers
@@ -75,10 +75,6 @@ lemma  handle_arch_fault_reply_bcorres[wp,BCorres2_AI_assms]:
   "bcorres ( handle_arch_fault_reply a b c d) (handle_arch_fault_reply a b c d)"
   by (cases a; simp add: handle_arch_fault_reply_def; wp)
 
-crunch
-    arch_switch_to_thread,arch_switch_to_idle_thread
-  for (bcorres) bcorres[wp, BCorres2_AI_assms]: truncate_state
-
 end
 
 interpretation BCorres2_AI?: BCorres2_AI
@@ -87,11 +83,9 @@ interpretation BCorres2_AI?: BCorres2_AI
   case 1 show ?case by (unfold_locales; (fact BCorres2_AI_assms)?)
   qed
 
-lemmas schedule_bcorres[wp] = schedule_bcorres1[OF BCorres2_AI_axioms]
-
 context Arch begin arch_global_naming
 
-crunch send_ipc,send_signal,do_reply_transfer,arch_perform_invocation
+crunch send_ipc,send_signal,do_reply_transfer,arch_perform_invocation,invoke_domain
   for (bcorres) bcorres[wp]: truncate_state
   (simp: gets_the_def swp_def
    ignore: freeMemory clearMemory loadWord cap_fault_on_failure
@@ -153,7 +147,7 @@ lemma vppi_event_bcorres[wp]:
 lemma handle_reserved_irq_bcorres[wp]: "bcorres (handle_reserved_irq a) (handle_reserved_irq a)"
   unfolding handle_reserved_irq_def by wpsimp
 
-crunch handle_hypervisor_fault
+crunch handle_hypervisor_fault, timer_tick
   for (bcorres) bcorres[wp]: truncate_state
 
 lemma handle_event_bcorres[wp]: "bcorres (handle_event e) (handle_event e)"
@@ -163,23 +157,6 @@ lemma handle_event_bcorres[wp]: "bcorres (handle_event e) (handle_event e)"
          | intro impI conjI allI | wp | wpc)+
   done
 
-crunch guarded_switch_to,switch_to_idle_thread
-  for (bcorres) bcorres[wp]: truncate_state (ignore: storeWord)
-
-lemma choose_switch_or_idle:
-  "((), s') \<in> fst (choose_thread s) \<Longrightarrow>
-       (\<exists>word. ((),s') \<in> fst (guarded_switch_to word s)) \<or>
-       ((),s') \<in> fst (switch_to_idle_thread s)"
-  apply (simp add: choose_thread_def)
-  apply (clarsimp simp add: switch_to_idle_thread_def bind_def gets_def
-                   arch_switch_to_idle_thread_def in_monad
-                   return_def get_def modify_def put_def
-                    get_thread_state_def
-                   thread_get_def
-                   split: if_split_asm)
-  apply force
-  done
-
 end
 
 end

proof/invariant-abstract/AARCH64/ArchDetSchedAux_AI.thy

@@ -15,67 +15,27 @@ named_theorems DetSchedAux_AI_assms
 
 crunch init_arch_objects
   for exst[wp]: "\<lambda>s. P (exst s)"
-  and valid_etcbs[wp, DetSchedAux_AI_assms]: valid_etcbs
   and valid_queues[wp]: valid_queues
   and valid_sched_action[wp]: valid_sched_action
   and valid_sched[wp]: valid_sched
-  (wp: mapM_x_wp')
-
-(* already proved earlier *)
-declare invoke_untyped_cur_thread[DetSchedAux_AI_assms]
-
-crunch invoke_untyped
-  for ready_queues[wp, DetSchedAux_AI_assms]: "\<lambda>s. P (ready_queues s)"
-  and scheduler_action[wp, DetSchedAux_AI_assms]: "\<lambda>s. P (scheduler_action s)"
+  and etcbs_of[wp, DetSchedAux_AI_assms]: "\<lambda>s. P (etcbs_of s)"
+  and ready_queues[wp, DetSchedAux_AI_assms]: "\<lambda>s. P (ready_queues s)"
+  and idle_thread[wp, DetSchedAux_AI_assms]: "\<lambda>s. P (idle_thread s)"
+  and schedact[wp, DetSchedAux_AI_assms]: "\<lambda>s. P (scheduler_action s)"
   and cur_domain[wp, DetSchedAux_AI_assms]: "\<lambda>s. P (cur_domain s)"
-  (wp: crunch_wps mapME_x_inv_wp preemption_point_inv'
-   simp: detype_def detype_ext_def crunch_simps wrap_ext_det_ext_ext_def mapM_x_defsym)
-
-crunch invoke_untyped
-  for idle_thread[wp, DetSchedAux_AI_assms]: "\<lambda>s. P (idle_thread s)"
-  (wp: crunch_wps mapME_x_inv_wp preemption_point_inv dxo_wp_weak
-   simp: detype_def detype_ext_def crunch_simps wrap_ext_det_ext_ext_def mapM_x_defsym
-   ignore: retype_region_ext)
+  (wp: mapM_x_wp')
 
 lemma tcb_sched_action_valid_idle_etcb:
   "tcb_sched_action foo thread \<lbrace>valid_idle_etcb\<rbrace>"
   by (rule valid_idle_etcb_lift)
      (wpsimp simp: tcb_sched_action_def set_tcb_queue_def)
 
-crunch do_machine_op
-  for ekheap[wp]: "\<lambda>s. P (ekheap s)"
-
-lemma delete_objects_etcb_at[wp, DetSchedAux_AI_assms]:
-  "delete_objects a b \<lbrace>etcb_at P t\<rbrace>"
-  unfolding delete_objects_def detype_def detype_ext_def
-  by (wpsimp simp: wrap_ext_det_ext_ext_def etcb_at_def)
-
-crunch reset_untyped_cap
-  for etcb_at[wp]: "etcb_at P t"
-  and valid_etcbs[wp]: "valid_etcbs"
-  (wp: preemption_point_inv' mapME_x_inv_wp crunch_wps
-    simp: unless_def)
-
-lemma invoke_untyped_etcb_at [DetSchedAux_AI_assms]:
-  "\<lbrace>etcb_at P t and valid_etcbs\<rbrace>
-   invoke_untyped ui
-   \<lbrace>\<lambda>r s. st_tcb_at (Not o inactive) t s \<longrightarrow> etcb_at P t s\<rbrace>"
-  apply (cases ui)
-  apply (simp add: mapM_x_def[symmetric] invoke_untyped_def)
-  apply (wpsimp wp: retype_region_etcb_at mapM_x_wp'
-                    create_cap_no_pred_tcb_at typ_at_pred_tcb_at_lift
-                    hoare_convert_imp[OF create_cap_no_pred_tcb_at]
-                    hoare_convert_imp[OF _ init_arch_objects_exst]
-                    hoare_drop_impE_E)
-  done
-
-
 crunch init_arch_objects
   for valid_blocked[wp, DetSchedAux_AI_assms]: valid_blocked
-  (wp: valid_blocked_lift set_cap_typ_at)
+  (wp: valid_blocked_lift crunch_wps)
 
 lemma perform_asid_control_etcb_at:
-  "\<lbrace>etcb_at P t and valid_etcbs\<rbrace>
+  "\<lbrace>etcb_at P t\<rbrace>
    perform_asid_control_invocation aci
    \<lbrace>\<lambda>r s. st_tcb_at (Not \<circ> inactive) t s \<longrightarrow> etcb_at P t s\<rbrace>"
   apply (simp add: perform_asid_control_invocation_def)
@@ -88,12 +48,11 @@ lemma perform_asid_control_etcb_at:
 
 crunch perform_asid_control_invocation
   for idle_thread[wp]: "\<lambda>s. P (idle_thread s)"
-  and valid_etcbs[wp]: valid_etcbs
   and valid_blocked[wp]: valid_blocked
   and schedact[wp]: "\<lambda>s. P (scheduler_action s)"
   and ready_queues[wp]: "\<lambda>s. P (ready_queues s)"
   and cur_domain[wp]: "\<lambda>s. P (cur_domain s)"
-  (wp: hoare_weak_lift_imp)
+  (wp: hoare_weak_lift_imp simp: detype_def)
 
 lemma perform_asid_control_invocation_valid_sched:
   "\<lbrace>ct_active and invs and valid_aci aci and valid_sched and valid_idle\<rbrace>
@@ -118,12 +77,6 @@ end
 lemmas tcb_sched_action_valid_idle_etcb
     = AARCH64.tcb_sched_action_valid_idle_etcb
 
-global_interpretation DetSchedAux_AI_det_ext?: DetSchedAux_AI_det_ext
-proof goal_cases
-  interpret Arch .
-  case 1 show ?case by (unfold_locales; (fact DetSchedAux_AI_assms)?)
-qed
-
 global_interpretation DetSchedAux_AI?: DetSchedAux_AI
 proof goal_cases
   interpret Arch .

proof/invariant-abstract/AARCH64/ArchDetSchedDomainTime_AI.thy

@@ -32,7 +32,7 @@ crunch
   prepare_thread_delete, handle_hypervisor_fault, make_arch_fault_msg,
   arch_post_modify_registers, arch_post_cap_deletion, handle_vm_fault,
   arch_invoke_irq_handler
-  for domain_list_inv[wp, DetSchedDomainTime_AI_assms]: "\<lambda>s. P (domain_list s)"
+  for domain_list_inv[wp, DetSchedDomainTime_AI_assms]: "\<lambda>s::det_state. P (domain_list s)"
   (simp: crunch_simps isFpuEnable_def wp: mapM_wp' transfer_caps_loop_pres)
 
 crunch arch_finalise_cap
@@ -46,12 +46,9 @@ crunch
   prepare_thread_delete, handle_hypervisor_fault, handle_vm_fault,
   arch_post_modify_registers, arch_post_cap_deletion, make_arch_fault_msg,
   arch_invoke_irq_handler, handle_reserved_irq, arch_mask_irq_signal
-  for domain_time_inv[wp, DetSchedDomainTime_AI_assms]: "\<lambda>s. P (domain_time s)"
+  for domain_time_inv[wp, DetSchedDomainTime_AI_assms]: "\<lambda>s::det_state. P (domain_time s)"
   (simp: crunch_simps wp: transfer_caps_loop_pres crunch_wps)
 
-crunch do_machine_op
-  for exst[wp]: "\<lambda>s. P (exst s)"
-
 declare init_arch_objects_exst[DetSchedDomainTime_AI_assms]
 
 end
@@ -65,15 +62,15 @@ qed
 context Arch begin arch_global_naming
 
 crunch arch_perform_invocation
-  for domain_time_inv[wp, DetSchedDomainTime_AI_assms]: "\<lambda>s. P (domain_time s)"
+  for domain_time_inv[wp, DetSchedDomainTime_AI_assms]: "\<lambda>s::det_state. P (domain_time s)"
   (wp: crunch_wps check_cap_inv simp: if_apply_def2)
 
 crunch arch_perform_invocation
-  for domain_list_inv[wp, DetSchedDomainTime_AI_assms]: "\<lambda>s. P (domain_list s)"
+  for domain_list_inv[wp, DetSchedDomainTime_AI_assms]: "\<lambda>s::det_state. P (domain_list s)"
   (wp: crunch_wps check_cap_inv simp: if_apply_def2)
 
 lemma vgic_maintenance_valid_domain_time:
-  "\<lbrace>\<lambda>s. 0 < domain_time s\<rbrace>
+  "\<lbrace>\<lambda>s::det_state. 0 < domain_time s\<rbrace>
     vgic_maintenance \<lbrace>\<lambda>y s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace>"
   unfolding vgic_maintenance_def
   apply (rule hoare_strengthen_post[where Q'="\<lambda>_ s. 0 < domain_time s"])
@@ -106,18 +103,21 @@ lemma timer_tick_valid_domain_time:
    \<lbrace>\<lambda>x s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace>" (is "\<lbrace> ?dtnot0 \<rbrace> _ \<lbrace> _ \<rbrace>")
   unfolding timer_tick_def
   supply if_split[split del]
-  supply ethread_get_wp[wp del]
+  supply thread_get_wp[wp del]
   supply if_apply_def2[simp]
   apply (wpsimp
            wp: reschedule_required_valid_domain_time hoare_vcg_const_imp_lift gts_wp
                (* unless we hit dec_domain_time we know ?dtnot0 holds on the state, so clean up the
                   postcondition once we hit thread_set_time_slice *)
                hoare_post_imp[where Q'="\<lambda>_. ?dtnot0" and Q="\<lambda>_ s. domain_time s = 0 \<longrightarrow> X s"
                                 and f="thread_set_time_slice t ts" for X t ts]
-               hoare_drop_imp[where f="ethread_get t f" for t f])
+               hoare_drop_imp[where f="thread_get t f" for t f])
   apply fastforce
   done
 
+crunch do_machine_op
+  for domain_time_sched[wp]: "\<lambda>s. P (domain_time s) (scheduler_action s)"
+
 lemma handle_interrupt_valid_domain_time [DetSchedDomainTime_AI_assms]:
   "\<lbrace>\<lambda>s :: det_ext state. 0 < domain_time s \<rbrace>
    handle_interrupt i
@@ -141,7 +141,7 @@ lemma handle_interrupt_valid_domain_time [DetSchedDomainTime_AI_assms]:
   done
 
 crunch handle_reserved_irq, arch_mask_irq_signal
-  for domain_list_inv [wp, DetSchedDomainTime_AI_assms]: "\<lambda>s. P (domain_list s)"
+  for domain_list_inv [wp, DetSchedDomainTime_AI_assms]: "\<lambda>s::det_state. P (domain_list s)"
   (wp: crunch_wps mapM_wp subset_refl simp: crunch_simps)
 
 end