arm ainvs: proof update for det_ext refactor

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

proof/invariant-abstract/ARM/ArchBCorres2_AI.thy

@@ -15,11 +15,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)
@@ -28,7 +28,7 @@ crunch invoke_untyped
   for (bcorres) bcorres[wp]: truncate_state
   (ignore: sequence_x)
 
-crunch set_mcpriority,
+crunch set_mcpriority, set_priority,
           arch_get_sanitise_register_info, arch_post_modify_registers
   for (bcorres) bcorres[wp, BCorres2_AI_assms]: truncate_state
 
@@ -74,10 +74,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
@@ -86,11 +82,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
          storeWord lookup_error_on_failure getRestartPC getRegister mapME)
@@ -148,10 +142,8 @@ lemma handle_vm_fault_bcorres[wp]: "bcorres (handle_vm_fault a b) (handle_vm_fau
 lemma handle_reserved_irq_bcorres[wp]: "bcorres (handle_reserved_irq a) (handle_reserved_irq a)"
   by (simp add: handle_reserved_irq_def; wp)
 
-lemma handle_hypervisor_fault_bcorres[wp]: "bcorres (handle_hypervisor_fault a b) (handle_hypervisor_fault a b)"
-  apply (cases b)
-  apply (simp | wp)+
-  done
+crunch handle_hypervisor_fault, timer_tick
+  for (bcorres) bcorres[wp]: truncate_state
 
 lemma handle_event_bcorres[wp]: "bcorres (handle_event e) (handle_event e)"
   apply (cases e)
@@ -160,23 +152,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 clearExMonitor)
-
-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/ARM/ArchDetSchedAux_AI.thy

@@ -12,118 +12,59 @@ context Arch begin arch_global_naming
 
 named_theorems DetSchedAux_AI_assms
 
+lemma set_pd_etcbs[wp]:
+  "set_pd p pd \<lbrace>\<lambda>s. P (etcbs_of s)\<rbrace>"
+  unfolding set_pd_def
+  apply (wpsimp wp: set_object_wp_strong)
+  by (auto elim!: rsubst[where P=P] simp: etcbs_of'_def obj_at_def a_type_def
+           split: kernel_object.splits)
+
 crunch init_arch_objects
   for exst[wp]: "\<lambda>s. P (exst s)"
-  and ct[wp]: "\<lambda>s. P (cur_thread s)"
-  and valid_etcbs[wp, DetSchedAux_AI_assms]: valid_etcbs
-  (wp: crunch_wps unless_wp valid_etcbs_lift)
-
-crunch invoke_untyped
-  for ct[wp, DetSchedAux_AI_assms]: "\<lambda>s. P (cur_thread s)"
-  (wp: crunch_wps dxo_wp_weak preemption_point_inv mapME_x_inv_wp
-   simp: crunch_simps do_machine_op_def detype_def mapM_x_defsym unless_def
-   ignore: freeMemory retype_region_ext)
-crunch invoke_untyped
-  for ready_queues[wp, DetSchedAux_AI_assms]: "\<lambda>s. P (ready_queues 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
-   ignore: freeMemory)
-crunch invoke_untyped
-  for scheduler_action[wp, DetSchedAux_AI_assms]: "\<lambda>s. P (scheduler_action 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
-   ignore: freeMemory)
-crunch invoke_untyped
-  for 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
-   ignore: freeMemory)
-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: freeMemory retype_region_ext)
+  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)
 
-lemma tcb_sched_action_valid_idle_etcb:
-  "\<lbrace>valid_idle_etcb\<rbrace>
-     tcb_sched_action foo thread
-   \<lbrace>\<lambda>_. valid_idle_etcb\<rbrace>"
-  apply (rule valid_idle_etcb_lift)
-  apply (simp add: tcb_sched_action_def set_tcb_queue_def)
-  apply (wp | simp)+
-  done
-
-lemma delete_objects_etcb_at[wp, DetSchedAux_AI_assms]:
-  "\<lbrace>\<lambda>s::det_ext state. etcb_at P t s\<rbrace> delete_objects a b \<lbrace>\<lambda>r s. etcb_at P t s\<rbrace>"
-  apply (simp add: delete_objects_def)
-  apply (wp)
-  apply (simp add: detype_def detype_ext_def wrap_ext_det_ext_ext_def etcb_at_def|wp)+
-  done
-
-crunch reset_untyped_cap
-  for etcb_at[wp]: "etcb_at P t"
-  (wp: preemption_point_inv' mapME_x_inv_wp crunch_wps
-    simp: unless_def)
-
-crunch reset_untyped_cap
-  for 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>(\<lambda>s :: det_ext state. etcb_at P t s) 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 whenE_def
-           split del: if_split)
-  apply (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]
-      | simp
-      | (wp (once) hoare_drop_impE_E))+
-  done
+crunch init_arch_objects
+  for valid_queues[wp]: valid_queues
+  and valid_sched_action[wp]: valid_sched_action
+  and valid_sched[wp]: valid_sched
+  (wp: valid_queues_lift valid_sched_action_lift valid_sched_lift)
 
+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 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>(\<lambda>s. etcb_at P t s) and valid_etcbs\<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>"
+lemma perform_asid_control_etcb_at:
+  "\<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)
-  apply (rule hoare_pre)
-   apply (wp | wpc | simp)+
+  apply wpsimp
        apply (wp hoare_imp_lift_something typ_at_pred_tcb_at_lift)[1]
       apply (rule hoare_drop_imps)
       apply (wp retype_region_etcb_at)+
   apply simp
   done
 
-crunch perform_asid_control_invocation
-  for ct[wp]: "\<lambda>s. P (cur_thread s)"
-
 crunch perform_asid_control_invocation
   for idle_thread[wp]: "\<lambda>s. P (idle_thread s)"
+  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 simp: detype_def)
 
 crunch perform_asid_control_invocation
-  for valid_etcbs[wp]: valid_etcbs (wp: hoare_weak_lift_imp)
-
-crunch perform_asid_control_invocation
-  for valid_blocked[wp]: valid_blocked (wp: hoare_weak_lift_imp)
-
-crunch perform_asid_control_invocation
-  for schedact[wp]: "\<lambda>s :: det_ext state. P (scheduler_action s)" (wp: crunch_wps simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def cap_insert_ext_def ignore: freeMemory)
-
-crunch perform_asid_control_invocation
-  for rqueues[wp]: "\<lambda>s :: det_ext state. P (ready_queues s)" (wp: crunch_wps simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def cap_insert_ext_def ignore: freeMemory)
-
-crunch perform_asid_control_invocation
-  for cur_domain[wp]: "\<lambda>s :: det_ext state. P (cur_domain s)" (wp: crunch_wps simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def cap_insert_ext_def ignore: freeMemory)
+  for ct[wp]: "\<lambda>s. P (cur_thread s)"
 
 lemma perform_asid_control_invocation_valid_sched:
   "\<lbrace>ct_active and invs and valid_aci aci and valid_sched and valid_idle\<rbrace>
@@ -143,26 +84,11 @@ lemma perform_asid_control_invocation_valid_sched:
   apply simp
   done
 
-crunch init_arch_objects
-  for valid_queues[wp]: valid_queues (wp: valid_queues_lift)
-
-crunch init_arch_objects
-  for valid_sched_action[wp]: valid_sched_action (wp: valid_sched_action_lift)
-
-crunch init_arch_objects
-  for valid_sched[wp]: valid_sched (wp: valid_sched_lift)
-
 end
 
 lemmas tcb_sched_action_valid_idle_etcb
     = ARM.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/ARM/ArchDetSchedDomainTime_AI.thy

@@ -20,9 +20,10 @@ crunch
   arch_activate_idle_thread, arch_switch_to_thread, arch_switch_to_idle_thread,
   handle_arch_fault_reply,
   arch_invoke_irq_control, handle_vm_fault, arch_get_sanitise_register_info,
-  prepare_thread_delete, handle_hypervisor_fault, make_arch_fault_msg,
+  prepare_thread_delete, handle_hypervisor_fault, make_arch_fault_msg, init_arch_objects,
   arch_post_modify_registers, arch_post_cap_deletion, 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)"
+  (wp: crunch_wps)
 
 crunch arch_finalise_cap
   for domain_time_inv[wp, DetSchedDomainTime_AI_assms]: "\<lambda>s. P (domain_time s)"
@@ -34,7 +35,8 @@ crunch
   arch_invoke_irq_control, handle_vm_fault, arch_get_sanitise_register_info,
   prepare_thread_delete, handle_hypervisor_fault,
   arch_post_modify_registers, arch_post_cap_deletion, arch_invoke_irq_handler
-  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)
 declare init_arch_objects_exst[DetSchedDomainTime_AI_assms]
         make_arch_fault_msg_inv[DetSchedDomainTime_AI_assms]
 
@@ -55,11 +57,11 @@ crunch arch_mask_irq_signal
   for domain_list_inv[wp, DetSchedDomainTime_AI_assms]: "\<lambda>s. P (domain_list s)"
 
 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)
 
 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)
 
 lemma timer_tick_valid_domain_time:
@@ -68,18 +70,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