ainvs: proof updates for new arch split functions

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>

proof/invariant-abstract/DetSchedDomainTime_AI.thy

@@ -88,6 +88,10 @@ locale DetSchedDomainTime_AI =
     "\<And>P ft. \<lbrace>\<lambda>s. P (domain_time s)\<rbrace> arch_post_cap_deletion ft \<lbrace>\<lambda>_ s. P (domain_time s)\<rbrace>"
   assumes arch_post_cap_deletion_domain_list_inv'[wp]:
     "\<And>P ft. \<lbrace>\<lambda>s. P (domain_list s)\<rbrace> arch_post_cap_deletion ft \<lbrace>\<lambda>_ s. P (domain_list s)\<rbrace>"
+  assumes arch_invoke_irq_handler_domain_list_inv'[wp]:
+    "\<And>P i. arch_invoke_irq_handler i \<lbrace>\<lambda>s. P (domain_list s)\<rbrace>"
+  assumes arch_invoke_irq_handler_domain_time_inv'[wp]:
+    "\<And>P i. arch_invoke_irq_handler i \<lbrace>\<lambda>s. P (domain_time s)\<rbrace>"
 
 crunches update_restart_pc
   for domain_list[wp]: "\<lambda>s. P (domain_list s)"
@@ -111,6 +115,11 @@ locale DetSchedDomainTime_AI_2 = DetSchedDomainTime_AI +
     "\<And>P irq. \<lbrace>\<lambda>s. P (domain_time s)\<rbrace> handle_reserved_irq irq \<lbrace>\<lambda>_ s. P (domain_time s)\<rbrace>"
   assumes handle_reserved_irq_domain_list_inv'[wp]:
     "\<And>P irq. \<lbrace>\<lambda>s. P (domain_list s)\<rbrace> handle_reserved_irq irq \<lbrace>\<lambda>_ s. P (domain_list s)\<rbrace>"
+  assumes arch_mask_irq_signal_domain_list_inv'[wp]:
+    "\<And>P irq. arch_mask_irq_signal irq \<lbrace>\<lambda>s. P (domain_list s)\<rbrace>"
+  assumes arch_mask_irq_signal_domain_time_inv'[wp]:
+    "\<And>P irq. arch_mask_irq_signal irq \<lbrace>\<lambda>s. P (domain_time s)\<rbrace>"
+
 
 context DetSchedDomainTime_AI begin
 

proof/invariant-abstract/DetSchedSchedule_AI.thy

@@ -858,6 +858,10 @@ locale DetSchedSchedule_AI =
     "\<And>c. arch_post_cap_deletion c \<lbrace>weak_valid_sched_action\<rbrace>"
   assumes arch_finalise_cap_idle_thread[wp] :
     "\<And>P b t. arch_finalise_cap t b \<lbrace>\<lambda> (s:: det_ext state). P (idle_thread s)\<rbrace>"
+  assumes arch_invoke_irq_handler_valid_sched[wp]:
+    "\<And>i. arch_invoke_irq_handler i \<lbrace>valid_sched\<rbrace>"
+  assumes arch_mask_irq_signal_valid_sched[wp]:
+    "\<And>irq. arch_mask_irq_signal irq \<lbrace>valid_sched\<rbrace>"
 
 context DetSchedSchedule_AI begin
 

proof/invariant-abstract/Deterministic_AI.thy

@@ -3984,8 +3984,6 @@ lemma retype_region_ext_valid_list_ext[wp]: "\<lbrace>valid_list\<rbrace> retype
 global_interpretation retype_region_ext_extended: is_extended "retype_region_ext a b"
   by (unfold_locales; wp)
 
-crunch valid_list[wp]: invoke_irq_handler valid_list
-
 crunches timer_tick
   for valid_list[wp]: "valid_list"
   and all_but_exst[wp]: "all_but_exst P"
@@ -3996,6 +3994,8 @@ global_interpretation timer_tick_extended: is_extended "timer_tick"
   by (unfold_locales; wp)
 
 locale Deterministic_AI_2 = Deterministic_AI_1 +
+  assumes arch_invoke_irq_handler_valid_list[wp]:
+    "\<And>i. arch_invoke_irq_handler i \<lbrace>valid_list\<rbrace>"
   assumes handle_interrupt_valid_list[wp]:
     "\<And>irq. \<lbrace>valid_list\<rbrace> handle_interrupt irq \<lbrace>\<lambda>_.valid_list\<rbrace>"
   assumes handle_call_valid_list[wp]:
@@ -4018,6 +4018,8 @@ locale Deterministic_AI_2 = Deterministic_AI_1 +
 
 context Deterministic_AI_2 begin
 
+crunch valid_list[wp]: invoke_irq_handler valid_list
+
 lemma handle_event_valid_list[wp]:
   "\<lbrace>valid_list\<rbrace> handle_event e \<lbrace>\<lambda>_.valid_list\<rbrace>"
   by (case_tac e; wpsimp wp: hoare_drop_imps)

proof/invariant-abstract/Syscall_AI.thy

@@ -23,6 +23,7 @@ requalify_facts
   data_to_cptr_def
   arch_post_cap_deletion_cur_thread
   arch_post_cap_deletion_state_refs_of
+  arch_invoke_irq_handler_typ_at
 end
 
 lemmas [wp] =