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
 
@@ -142,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)
@@ -154,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:

proof/invariant-abstract/ARM/ArchDetSchedSchedule_AI.thy

@@ -19,11 +19,6 @@ crunch
   prepare_thread_delete
   for prepare_thread_delete_idle_thread[wp, DetSchedSchedule_AI_assms]: "\<lambda>(s:: det_ext state). P (idle_thread s)"
 
-crunch
-  arch_switch_to_idle_thread, arch_switch_to_thread, arch_get_sanitise_register_info, arch_post_modify_registers
-  for valid_etcbs[wp, DetSchedSchedule_AI_assms]: valid_etcbs
-  (simp: crunch_simps ignore: clearExMonitor)
-
 crunch
   switch_to_idle_thread, switch_to_thread, set_vm_root, arch_get_sanitise_register_info, arch_post_modify_registers
   for valid_queues[wp, DetSchedSchedule_AI_assms]: valid_queues
@@ -35,11 +30,9 @@ crunch
   (simp: crunch_simps ignore: clearExMonitor)
 
 crunch set_vm_root
-  for ct_not_in_q[wp]: "ct_not_in_q"
-  (wp: crunch_wps simp: crunch_simps)
-
-crunch set_vm_root
-  for ct_not_in_q'[wp]: "\<lambda>s. ct_not_in_q_2 (ready_queues s) (scheduler_action s) t"
+  for ready_queues[wp]: "\<lambda>s. P (ready_queues s)"
+  and ct_not_in_q[wp]: "ct_not_in_q"
+  and ct_not_in_q'[wp]: "\<lambda>s. ct_not_in_q_2 (ready_queues s) (scheduler_action s) t"
   (wp: crunch_wps simp: crunch_simps)
 
 lemma switch_to_idle_thread_ct_not_in_q [wp, DetSchedSchedule_AI_assms]:
@@ -54,7 +47,7 @@ lemma switch_to_idle_thread_ct_not_in_q [wp, DetSchedSchedule_AI_assms]:
 
 crunch set_vm_root
   for valid_sched_action'[wp]: "\<lambda>s. valid_sched_action_2 (scheduler_action s)
-                                                 (ekheap s) (kheap s) thread (cur_domain s)"
+                                                 (etcbs_of s) (kheap s) thread (cur_domain s)"
   (wp: crunch_wps simp: crunch_simps)
 
 lemma switch_to_idle_thread_valid_sched_action [wp, DetSchedSchedule_AI_assms]:
@@ -71,7 +64,7 @@ lemma switch_to_idle_thread_valid_sched_action [wp, DetSchedSchedule_AI_assms]:
 
 crunch set_vm_root
   for ct_in_cur_domain'[wp]: "\<lambda>s. ct_in_cur_domain_2 t (idle_thread s)
-                                                   (scheduler_action s) (cur_domain s) (ekheap s)"
+                                                   (scheduler_action s) (cur_domain s) (etcbs_of s)"
   (wp: crunch_wps simp: crunch_simps)
 
 lemma switch_to_idle_thread_ct_in_cur_domain [wp, DetSchedSchedule_AI_assms]:
@@ -102,7 +95,7 @@ crunch set_vm_root
   (wp: crunch_wps whenE_wp simp: crunch_simps)
 
 crunch arch_switch_to_thread
-  for ct_in_cur_domain_2[wp, DetSchedSchedule_AI_assms]: "\<lambda>s. ct_in_cur_domain_2 thread (idle_thread s) (scheduler_action s) (cur_domain s) (ekheap s)"
+  for ct_in_cur_domain_2[wp, DetSchedSchedule_AI_assms]: "\<lambda>s. ct_in_cur_domain_2 thread (idle_thread s) (scheduler_action s) (cur_domain s) (etcbs_of s)"
   (simp: crunch_simps)
 
 crunch set_vm_root
@@ -192,20 +185,19 @@ lemma switch_to_idle_thread_cur_thread_idle_thread [wp, DetSchedSchedule_AI_assm
   "\<lbrace>\<top>\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>_ s. cur_thread s = idle_thread s\<rbrace>"
   by (wp | simp add:switch_to_idle_thread_def arch_switch_to_idle_thread_def)+
 
-lemma set_pd_valid_etcbs[wp]:
-  "\<lbrace>valid_etcbs\<rbrace> set_pd ptr pd \<lbrace>\<lambda>rv. valid_etcbs\<rbrace>"
-  by (wp hoare_drop_imps valid_etcbs_lift | simp add: set_pd_def)+
-
 lemma set_pt_etcbs[wp]:
   "set_pt ptr pt \<lbrace>\<lambda>s. P (etcbs_of s)\<rbrace>"
   unfolding set_pt_def
-  apply (wpsimp wp: set_object_wp get_object_wp)
-  apply (auto elim!: rsubst[where P=P] simp: obj_at_def etcbs_of'_def split: kernel_object.splits)
-  done
+  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)
 
-lemma set_asid_pool_valid_etcbs[wp]:
-  "\<lbrace>valid_etcbs\<rbrace> set_asid_pool ptr pool \<lbrace>\<lambda>rv. valid_etcbs\<rbrace>"
-  by (wp hoare_drop_imps valid_etcbs_lift | simp add: set_asid_pool_def)+
+lemma set_asid_pool_etcbs[wp]:
+  "set_asid_pool ptr pool \<lbrace>\<lambda>s. P (etcbs_of s)\<rbrace>"
+  unfolding set_asid_pool_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)
 
 lemma set_pt_valid_sched[wp]:
   "\<lbrace>valid_sched\<rbrace> set_pt ptr pt \<lbrace>\<lambda>rv. valid_sched\<rbrace>"
@@ -225,12 +217,6 @@ crunch
   (wp: crunch_wps hoare_drop_imps unless_wp select_inv mapM_wp
        subset_refl if_fun_split simp: crunch_simps ignore: tcb_sched_action)
 
-crunch
-  arch_finalise_cap, prepare_thread_delete
-  for valid_etcbs[wp, DetSchedSchedule_AI_assms]: valid_etcbs
-  (wp: hoare_drop_imps unless_wp select_inv mapM_x_wp mapM_wp subset_refl
-       if_fun_split simp: crunch_simps ignore: set_object thread_set)
-
 crunch
   arch_finalise_cap, prepare_thread_delete
   for simple_sched_action[wp, DetSchedSchedule_AI_assms]: simple_sched_action