riscv ainvs: proof updates for new arch split functions

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

proof/invariant-abstract/RISCV64/ArchBCorres2_AI.thy

@@ -134,7 +134,8 @@ lemma handle_hypervisor_fault_bcorres[wp]: "bcorres (handle_hypervisor_fault a b
 lemma handle_event_bcorres[wp]: "bcorres (handle_event e) (handle_event e)"
   apply (cases e)
   apply (simp add: handle_send_def handle_call_def handle_recv_def handle_reply_def handle_yield_def
-                   handle_interrupt_def Let_def handle_reserved_irq_def | intro impI conjI allI | wp | wpc)+
+                   handle_interrupt_def Let_def handle_reserved_irq_def arch_mask_irq_signal_def
+         | intro impI conjI allI | wp | wpc)+
   done
 
 crunch (bcorres)bcorres[wp]: guarded_switch_to,switch_to_idle_thread truncate_state (ignore: storeWord)

proof/invariant-abstract/RISCV64/ArchDetSchedDomainTime_AI.thy

@@ -20,7 +20,8 @@ crunch domain_list_inv [wp, DetSchedDomainTime_AI_assms]:
   handle_arch_fault_reply,
   arch_invoke_irq_control, arch_get_sanitise_register_info,
   prepare_thread_delete, handle_hypervisor_fault, make_arch_fault_msg,
-  arch_post_modify_registers, arch_post_cap_deletion, handle_vm_fault
+  arch_post_modify_registers, arch_post_cap_deletion, handle_vm_fault,
+  arch_invoke_irq_handler
   "\<lambda>s. P (domain_list s)"
   (simp: crunch_simps)
 
@@ -32,7 +33,8 @@ crunch domain_time_inv [wp, DetSchedDomainTime_AI_assms]:
   handle_arch_fault_reply, init_arch_objects,
   arch_invoke_irq_control, arch_get_sanitise_register_info,
   prepare_thread_delete, handle_hypervisor_fault, handle_vm_fault,
-  arch_post_modify_registers, arch_post_cap_deletion, make_arch_fault_msg
+  arch_post_modify_registers, arch_post_cap_deletion, make_arch_fault_msg,
+  arch_invoke_irq_handler
   "\<lambda>s. P (domain_time s)"
   (simp: crunch_simps)
 
@@ -64,7 +66,7 @@ lemma handle_interrupt_valid_domain_time [DetSchedDomainTime_AI_assms]:
    apply (case_tac "maxIRQ < i"; simp)
     subgoal by (wp hoare_false_imp, simp)
    apply (rule hoare_pre)
-    apply (wp do_machine_op_exst | simp | wpc)+
+    apply (wp do_machine_op_exst | simp add: arch_mask_irq_signal_def | wpc)+
        apply (rule_tac Q="\<lambda>_ s. 0 < domain_time s" in hoare_post_imp, fastforce)
        apply wp
       apply (rule_tac Q="\<lambda>_ s. 0 < domain_time s" in hoare_post_imp, fastforce)
@@ -77,10 +79,9 @@ lemma handle_interrupt_valid_domain_time [DetSchedDomainTime_AI_assms]:
     apply clarsimp
    done
 
-crunch domain_time_inv [wp, DetSchedDomainTime_AI_assms]: handle_reserved_irq "\<lambda>s. P (domain_time s)"
-  (wp: crunch_wps mapM_wp subset_refl simp: crunch_simps)
-
-crunch domain_list_inv [wp, DetSchedDomainTime_AI_assms]: handle_reserved_irq "\<lambda>s. P (domain_list s)"
+crunches handle_reserved_irq, arch_mask_irq_signal
+  for domain_time_inv [wp, DetSchedDomainTime_AI_assms]: "\<lambda>s. P (domain_time s)"
+  and domain_list_inv [wp, DetSchedDomainTime_AI_assms]: "\<lambda>s. P (domain_list s)"
   (wp: crunch_wps mapM_wp subset_refl simp: crunch_simps)
 
 end

proof/invariant-abstract/RISCV64/ArchDetSchedSchedule_AI.thy

@@ -197,7 +197,8 @@ crunch simple_sched_action [wp, DetSchedSchedule_AI_assms]:
    simp: unless_def if_fun_split)
 
 crunch valid_sched [wp, DetSchedSchedule_AI_assms]:
-  arch_finalise_cap, prepare_thread_delete valid_sched
+  arch_finalise_cap, prepare_thread_delete, arch_invoke_irq_handler, arch_mask_irq_signal
+  "valid_sched"
   (ignore: set_object wp: crunch_wps subset_refl simp: if_fun_split)
 
 lemma activate_thread_valid_sched [DetSchedSchedule_AI_assms]:

proof/invariant-abstract/RISCV64/ArchDeterministic_AI.thy

@@ -28,6 +28,8 @@ global_interpretation Deterministic_AI_1?: Deterministic_AI_1
 
 context Arch begin global_naming RISCV64
 
+crunch valid_list[wp,Deterministic_AI_assms]: arch_invoke_irq_handler valid_list
+
 crunch valid_list[wp]: invoke_untyped valid_list
   (wp: crunch_wps preemption_point_inv' hoare_unless_wp mapME_x_wp'
    simp: mapM_x_def_bak crunch_simps)
@@ -67,7 +69,7 @@ lemma handle_interrupt_valid_list[wp, Deterministic_AI_assms]:
   unfolding handle_interrupt_def ackInterrupt_def
   apply (rule hoare_pre)
    by (wp get_cap_wp  do_machine_op_valid_list
-       | wpc | simp add: get_irq_slot_def handle_reserved_irq_def
+       | wpc | simp add: get_irq_slot_def handle_reserved_irq_def arch_mask_irq_signal_def
        | wp (once) hoare_drop_imps)+
 
 crunch valid_list[wp, Deterministic_AI_assms]: handle_send,handle_reply valid_list

proof/invariant-abstract/RISCV64/ArchInterrupt_AI.thy

@@ -238,7 +238,8 @@ lemma (* handle_interrupt_invs *) [Interrupt_AI_asms]:
   apply (simp add: handle_interrupt_def)
   apply (rule conjI; rule impI)
   apply (simp add: do_machine_op_bind empty_fail_ackInterrupt_ARCH empty_fail_maskInterrupt_ARCH)
-     apply (wp dmo_maskInterrupt_invs maskInterrupt_invs_ARCH dmo_ackInterrupt send_signal_interrupt_states | wpc | simp)+
+     apply (wpsimp wp: dmo_maskInterrupt_invs maskInterrupt_invs_ARCH dmo_ackInterrupt
+                      send_signal_interrupt_states simp: arch_mask_irq_signal_def)+
      apply (wp get_cap_wp send_signal_interrupt_states )
     apply (rule_tac Q="\<lambda>rv. invs and (\<lambda>s. st = interrupt_states s irq)" in hoare_post_imp)
      apply (clarsimp simp: ex_nonz_cap_to_def invs_valid_objs)
@@ -258,6 +259,8 @@ lemma sts_arch_irq_control_inv_valid[wp, Interrupt_AI_asms]:
   apply (wpsimp wp: ex_cte_cap_to_pres simp: cap_table_at_typ)
   done
 
+crunch typ_at[wp]: arch_invoke_irq_handler "\<lambda>s. P (typ_at T p s)"
+
 end
 
 interpretation Interrupt_AI?: Interrupt_AI