kings-crown/FVELER_Isabelle huggingface dataset:
theory Tcb_IF

lemma cap_delete_only_timer_irq_inv:
  "cap_delete slot \<lbrace>only_timer_irq_inv irq (st :: det_state)\<rbrace>" apply (simp add: only_timer_irq_inv_def) apply (wp only_timer_irq_pres cap_delete_irq_masks | force)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>only_timer_irq_inv irq st\<rbrace> cap_delete slot \<lbrace>\<lambda>_. only_timer_irq_inv irq st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv False st and only_timer_irq irq\<rbrace> cap_delete slot \<lbrace>\<lambda>_. domain_sep_inv False st and only_timer_irq irq\<rbrace> proof (prove)
goal:
No subgoals!
theory Tcb_IF

lemma set_priority_only_timer_irq_inv:
  "set_priority t prio \<lbrace>only_timer_irq_inv irq (st :: det_state)\<rbrace>" apply (simp add: only_timer_irq_inv_def) apply (wp only_timer_irq_pres | force)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>only_timer_irq_inv irq st\<rbrace> set_priority t prio \<lbrace>\<lambda>_. only_timer_irq_inv irq st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv False st and only_timer_irq irq\<rbrace> set_priority t prio \<lbrace>\<lambda>_. domain_sep_inv False st and only_timer_irq irq\<rbrace> proof (prove)
goal:
No subgoals!
theory Tcb_IF

lemma set_mcpriority_only_timer_irq_inv:
  "set_mcpriority t prio \<lbrace>only_timer_irq_inv irq (st :: det_state)\<rbrace>" apply (simp add: only_timer_irq_inv_def) apply (wp only_timer_irq_pres | force)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>only_timer_irq_inv irq st\<rbrace> set_mcpriority t prio \<lbrace>\<lambda>_. only_timer_irq_inv irq st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv False st and only_timer_irq irq\<rbrace> set_mcpriority t prio \<lbrace>\<lambda>_. domain_sep_inv False st and only_timer_irq irq\<rbrace> proof (prove)
goal:
No subgoals!
theory Tcb_IF

lemma thread_set_tcb_fault_handler_update_only_timer_irq_inv:
  "thread_set (tcb_fault_handler_update blah) t \<lbrace>only_timer_irq_inv irq (st :: det_state)\<rbrace>" apply (simp add: only_timer_irq_inv_def) apply (wp only_timer_irq_pres | force)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>only_timer_irq_inv irq st\<rbrace> thread_set (tcb_fault_handler_update blah) t \<lbrace>\<lambda>_. only_timer_irq_inv irq st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv False st and only_timer_irq irq\<rbrace> thread_set (tcb_fault_handler_update blah) t \<lbrace>\<lambda>_. domain_sep_inv False st and only_timer_irq irq\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchTcb_IF

lemma cap_ne_global_pd:
  "\<lbrakk> ex_nonz_cap_to word s; valid_global_refs s \<rbrakk>
     \<Longrightarrow> word \<noteq> arm_global_pd (arch_state s)" unfolding ex_nonz_cap_to_def apply (simp only: cte_wp_at_caps_of_state zobj_refs_to_obj_refs) apply (elim exE conjE) apply (drule valid_global_refsD2,simp) apply (unfold global_refs_def) apply clarsimp apply (unfold cap_range_def) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ex_nonz_cap_to word s; valid_global_refs s\<rbrakk> \<Longrightarrow> word \<noteq> arm_global_pd (arch_state s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>cref. cte_wp_at (\<lambda>c. word \<in> zobj_refs c) cref s; valid_global_refs s\<rbrakk> \<Longrightarrow> word \<noteq> arm_global_pd (arch_state s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>cref cap. caps_of_state s cref = Some cap \<and> word \<in> obj_refs cap \<and> \<not> is_zombie cap; valid_global_refs s\<rbrakk> \<Longrightarrow> word \<noteq> arm_global_pd (arch_state s) proof (prove)
goal (1 subgoal):
 1. \<And>cref cap. \<lbrakk>valid_global_refs s; caps_of_state s cref = Some cap; word \<in> obj_refs cap; \<not> is_zombie cap\<rbrakk> \<Longrightarrow> word \<noteq> arm_global_pd (arch_state s) proof (prove)
goal (1 subgoal):
 1. \<And>cref cap. \<lbrakk>valid_global_refs s; word \<in> obj_refs cap; \<not> is_zombie cap; global_refs s \<inter> cap_range cap = {}\<rbrakk> \<Longrightarrow> word \<noteq> arm_global_pd (arch_state s) proof (prove)
goal (1 subgoal):
 1. \<And>cref cap. \<lbrakk>valid_global_refs s; word \<in> obj_refs cap; \<not> is_zombie cap; ({idle_thread s, arm_global_pd (arch_state s)} \<union> range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range cap = {}\<rbrakk> \<Longrightarrow> word \<noteq> arm_global_pd (arch_state s) proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>valid_global_refs s; arm_global_pd (arch_state s) \<in> obj_refs cap; \<not> is_zombie cap; idle_thread s \<notin> cap_range cap; arm_global_pd (arch_state s) \<notin> cap_range cap; (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range cap = {}; word = arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>valid_global_refs s; arm_global_pd (arch_state s) \<in> obj_refs cap; \<not> is_zombie cap; idle_thread s \<notin> untyped_range cap \<union> obj_refs cap; arm_global_pd (arch_state s) \<notin> untyped_range cap \<union> obj_refs cap; (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> (untyped_range cap \<union> obj_refs cap) = {}; word = arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory ArchTcb_IF

lemma valid_arch_caps_vs_lookup[Tcb_IF_assms]:
  "valid_arch_caps s \<Longrightarrow> valid_vs_lookup s" by (simp add: valid_arch_caps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_arch_caps s \<Longrightarrow> valid_vs_lookup s
theory ArchTcb_IF

lemma no_cap_to_idle_thread'[Tcb_IF_assms]:
  "valid_global_refs s \<Longrightarrow> \<not> ex_nonz_cap_to (idle_thread s) s" apply (clarsimp simp add: ex_nonz_cap_to_def valid_global_refs_def valid_refs_def) apply (drule_tac x=a in spec) apply (drule_tac x=b in spec) apply (clarsimp simp: cte_wp_at_def global_refs_def cap_range_def) apply (case_tac cap,simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_global_refs s \<Longrightarrow> \<not> ex_nonz_cap_to (idle_thread s) s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a b. \<not> cte_wp_at (\<lambda>c. global_refs s \<inter> cap_range c \<noteq> {}) (a, b) s; cte_wp_at (\<lambda>c. idle_thread s \<in> zobj_refs c) (a, b) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>cte_wp_at (\<lambda>c. idle_thread s \<in> zobj_refs c) (a, b) s; \<forall>b. \<not> cte_wp_at (\<lambda>c. global_refs s \<inter> cap_range c \<noteq> {}) (a, b) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>cte_wp_at (\<lambda>c. idle_thread s \<in> zobj_refs c) (a, b) s; \<not> cte_wp_at (\<lambda>c. global_refs s \<inter> cap_range c \<noteq> {}) (a, b) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b cap. \<lbrakk>fst (get_cap (a, b) s) = {(cap, s)}; idle_thread s \<in> zobj_refs cap; idle_thread s \<notin> untyped_range cap; idle_thread s \<notin> obj_refs cap; arm_global_pd (arch_state s) \<notin> untyped_range cap; arm_global_pd (arch_state s) \<notin> obj_refs cap; (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> (untyped_range cap \<union> obj_refs cap) = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory ArchTcb_IF

lemma no_cap_to_idle_thread''[Tcb_IF_assms]:
  "valid_global_refs s \<Longrightarrow> caps_of_state s ref \<noteq> Some (ThreadCap (idle_thread s))" apply (clarsimp simp add: valid_global_refs_def valid_refs_def cte_wp_at_caps_of_state) apply (drule_tac x="fst ref" in spec) apply (drule_tac x="snd ref" in spec) apply (simp add: cap_range_def global_refs_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_global_refs s \<Longrightarrow> caps_of_state s ref \<noteq> Some (ThreadCap (idle_thread s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> global_refs s \<inter> cap_range cap = {}; caps_of_state s ref = Some (ThreadCap (idle_thread s))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s ref = Some (ThreadCap (idle_thread s)); \<forall>b cap. caps_of_state s (fst ref, b) = Some cap \<longrightarrow> global_refs s \<inter> cap_range cap = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s ref = Some (ThreadCap (idle_thread s)); \<forall>cap. caps_of_state s (fst ref, snd ref) = Some cap \<longrightarrow> global_refs s \<inter> cap_range cap = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory ArchTcb_IF

lemma arch_post_modify_registers_reads_respects_f[Tcb_IF_assms, wp]:
  "reads_respects_f aag l \<top> (arch_post_modify_registers cur t)" by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (\<lambda>_. True) (arch_post_modify_registers cur t)
theory ArchTcb_IF

lemma arch_get_sanitise_register_info_reads_respects_f[Tcb_IF_assms, wp]:
  "reads_respects_f aag l \<top> (arch_get_sanitise_register_info rv)" by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (\<lambda>_. True) (arch_get_sanitise_register_info rv)
theory Interrupt_IF

lemma invoke_irq_control_reads_respects:
  "reads_respects aag l (K (authorised_irq_ctl_inv aag i)) (invoke_irq_control i)" apply (cases i) apply (wp cap_insert_reads_respects set_irq_state_reads_respects | simp)+ apply (clarsimp simp: authorised_irq_ctl_inv_def) apply (simp add: authorised_irq_ctl_inv_def) apply (rule arch_invoke_irq_control_reads_respects[simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (authorised_irq_ctl_inv aag i)) (invoke_irq_control i) proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13. i = IRQControl x11 x12 x13 \<Longrightarrow> reads_respects aag l (K (authorised_irq_ctl_inv aag i)) (invoke_irq_control i)
 2. \<And>x2. i = ArchIRQControl x2 \<Longrightarrow> reads_respects aag l (K (authorised_irq_ctl_inv aag i)) (invoke_irq_control i) proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13. \<lbrakk>i = IRQControl x11 x12 x13; authorised_irq_ctl_inv aag (IRQControl x11 x12 x13)\<rbrakk> \<Longrightarrow> aag_can_read aag (fst x13) \<and> aag_can_read aag (fst x12)
 2. \<And>x2. i = ArchIRQControl x2 \<Longrightarrow> reads_respects aag l (K (authorised_irq_ctl_inv aag i)) (invoke_irq_control i) proof (prove)
goal (1 subgoal):
 1. \<And>x2. i = ArchIRQControl x2 \<Longrightarrow> reads_respects aag l (K (authorised_irq_ctl_inv aag i)) (invoke_irq_control i) proof (prove)
goal (1 subgoal):
 1. \<And>x2. i = ArchIRQControl x2 \<Longrightarrow> reads_respects aag l (\<lambda>y. arch_authorised_irq_ctl_inv aag x2) (arch_invoke_irq_control x2) proof (prove)
goal:
No subgoals!
theory Interrupt_IF

lemma invoke_irq_control_globals_equiv:
  "\<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace>
   invoke_irq_control a
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" apply (induct a) apply (wpsimp wp: set_irq_state_globals_equiv cap_insert_globals_equiv''
                     set_irq_state_valid_global_objs arch_invoke_irq_control_globals_equiv)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace> invoke_irq_control a \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2a x3. \<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace> invoke_irq_control (IRQControl x1 x2a x3) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>x. \<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace> invoke_irq_control (ArchIRQControl x) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal:
No subgoals!
theory Interrupt_IF

lemma invoke_irq_handler_globals_equiv:
  "\<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace>
   invoke_irq_handler a
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" apply (induct a) by (wpsimp wp: modify_wp cap_insert_globals_equiv''
                 cap_delete_one_globals_equiv cap_delete_one_valid_global_objs)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace> invoke_irq_handler a \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace> invoke_irq_handler (ACKIrq x) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>x1a x2 x3a. \<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace> invoke_irq_handler (SetIRQHandler x1a x2 x3a) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 3. \<And>x. \<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace> invoke_irq_handler (ClearIRQHandler x) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
theory Interrupt_IF

lemma invoke_irq_handler_reads_respects_f_g:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows
  "reads_respects_f_g aag l (silc_inv aag st and invs and pas_refined aag
                                             and irq_handler_inv_valid irq_inv
                                             and K (authorised_irq_hdl_inv aag irq_inv))
                      (invoke_irq_handler irq_inv)" apply (rule equiv_valid_guard_imp[OF reads_respects_f_g]) apply (rule invoke_irq_handler_reads_respects_f[OF domains_distinct]) apply (rule doesnt_touch_globalsI) apply (wp invoke_irq_handler_globals_equiv | simp)+ by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f_g aag l (silc_inv aag st and invs and pas_refined aag and irq_handler_inv_valid irq_inv and K (authorised_irq_hdl_inv aag irq_inv)) (invoke_irq_handler irq_inv) proof (prove)
goal (3 subgoals):
 1. reads_respects_f aag l ?P1 (invoke_irq_handler irq_inv)
 2. doesnt_touch_globals ?Q1 (invoke_irq_handler irq_inv)
 3. \<And>s. (silc_inv aag st and invs and pas_refined aag and irq_handler_inv_valid irq_inv and K (authorised_irq_hdl_inv aag irq_inv)) s \<Longrightarrow> (?P1 and ?Q1) s proof (prove)
goal (2 subgoals):
 1. doesnt_touch_globals ?Q1 (invoke_irq_handler irq_inv)
 2. \<And>s. (silc_inv aag st and invs and pas_refined aag and irq_handler_inv_valid irq_inv and K (authorised_irq_hdl_inv aag irq_inv)) s \<Longrightarrow> (silc_inv aag ?st5 and pas_refined aag and invs and pas_refined aag and irq_handler_inv_valid irq_inv and K (authorised_irq_hdl_inv aag irq_inv) and ?Q1) s proof (prove)
goal (2 subgoals):
 1. \<And>st. \<lbrace>globals_equiv st and ?Q1\<rbrace> invoke_irq_handler irq_inv \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>s. (silc_inv aag st and invs and pas_refined aag and irq_handler_inv_valid irq_inv and K (authorised_irq_hdl_inv aag irq_inv)) s \<Longrightarrow> (silc_inv aag ?st5 and pas_refined aag and invs and pas_refined aag and irq_handler_inv_valid irq_inv and K (authorised_irq_hdl_inv aag irq_inv) and ?Q1) s proof (prove)
goal (1 subgoal):
 1. \<And>s. silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> irq_handler_inv_valid irq_inv s \<and> authorised_irq_hdl_inv aag irq_inv \<Longrightarrow> silc_inv aag ?st5 s \<and> valid_arch_state s \<and> valid_global_objs s
theory Interrupt_IF

lemma invoke_irq_control_reads_respects_g:
  "reads_respects_g aag l (valid_global_objs and valid_arch_state
                                             and K (authorised_irq_ctl_inv aag i))
                    (invoke_irq_control i)" apply (rule equiv_valid_guard_imp[OF reads_respects_g]) apply (rule invoke_irq_control_reads_respects) apply (rule doesnt_touch_globalsI) apply (wp invoke_irq_control_globals_equiv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (valid_global_objs and valid_arch_state and K (authorised_irq_ctl_inv aag i)) (invoke_irq_control i) proof (prove)
goal (3 subgoals):
 1. reads_respects aag l ?P1 (invoke_irq_control i)
 2. doesnt_touch_globals ?Q1 (invoke_irq_control i)
 3. \<And>s. (valid_global_objs and valid_arch_state and K (authorised_irq_ctl_inv aag i)) s \<Longrightarrow> (?P1 and ?Q1) s proof (prove)
goal (2 subgoals):
 1. doesnt_touch_globals ?Q1 (invoke_irq_control i)
 2. \<And>s. (valid_global_objs and valid_arch_state and K (authorised_irq_ctl_inv aag i)) s \<Longrightarrow> (K (authorised_irq_ctl_inv aag i) and ?Q1) s proof (prove)
goal (2 subgoals):
 1. \<And>st. \<lbrace>globals_equiv st and ?Q1\<rbrace> invoke_irq_control i \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>s. (valid_global_objs and valid_arch_state and K (authorised_irq_ctl_inv aag i)) s \<Longrightarrow> (K (authorised_irq_ctl_inv aag i) and ?Q1) s proof (prove)
goal:
No subgoals!
theory ArchInterrupt_IF

lemma arch_invoke_irq_handler_reads_respects[Interrupt_IF_assms, wp]:
  "reads_respects_f aag l (silc_inv aag st) (arch_invoke_irq_handler irq)" apply (cases irq; wpsimp) apply (rule reads_respects_f[OF dmo_maskInterrupt_reads_respects, where Q=\<top>, simplified]) apply wpsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st) (arch_invoke_irq_handler irq) proof (prove)
goal (1 subgoal):
 1. \<And>x1. irq = ACKIrq x1 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st) (do_machine_op (maskInterrupt False x1)) proof (prove)
goal (1 subgoal):
 1. \<And>x1. irq = ACKIrq x1 \<Longrightarrow> \<lbrace>silc_inv aag st\<rbrace> do_machine_op (maskInterrupt False x1) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchInterrupt_IF

lemma arch_invoke_irq_control_reads_respects[Interrupt_IF_assms]:
  "reads_respects aag (l :: 'a subject_label) (K (arch_authorised_irq_ctl_inv aag i))
                  (arch_invoke_irq_control i)" apply (cases i) apply (simp add: setIRQTrigger_def) apply (wp cap_insert_reads_respects set_irq_state_reads_respects dmo_mol_reads_respects | simp)+ apply (clarsimp simp: arch_authorised_irq_ctl_inv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (arch_authorised_irq_ctl_inv aag i)) (arch_invoke_irq_control i) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. i = ArchIRQControlIssue x1 x2 x3 x4 \<Longrightarrow> reads_respects aag l (K (arch_authorised_irq_ctl_inv aag i)) (arch_invoke_irq_control i) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. i = ArchIRQControlIssue x1 x2 x3 x4 \<Longrightarrow> reads_respects aag l (\<lambda>y. arch_authorised_irq_ctl_inv aag (ArchIRQControlIssue x1 x2 x3 x4)) (liftE (do y <- do_machine_op (machine_op_lift (setIRQTrigger_impl x1 x4));
y <- set_irq_state IRQSignal x1;
cap_insert (IRQHandlerCap x1) x3 x2
od)) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. \<lbrakk>i = ArchIRQControlIssue x1 x2 x3 x4; arch_authorised_irq_ctl_inv aag (ArchIRQControlIssue x1 x2 x3 x4)\<rbrakk> \<Longrightarrow> aag_can_read aag (fst x3) \<and> aag_can_read aag (fst x2) proof (prove)
goal:
No subgoals!
theory ArchInterrupt_IF

lemma arch_invoke_irq_control_globals_equiv[Interrupt_IF_assms]:
  "\<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace>
   arch_invoke_irq_control ai
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" apply (induct ai) apply (simp add: setIRQTrigger_def) apply (wpsimp wp: set_irq_state_globals_equiv set_irq_state_valid_global_objs
                    cap_insert_globals_equiv'' dmo_mol_globals_equiv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace> arch_invoke_irq_control ai \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1a x2a x3a x4a. \<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace> arch_invoke_irq_control (ArchIRQControlIssue x1a x2a x3a x4a) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1a x2a x3a x4a. \<lbrace>\<lambda>a. globals_equiv st a \<and> valid_arch_state a \<and> valid_global_objs a\<rbrace> liftE (do y <- do_machine_op (machine_op_lift (setIRQTrigger_impl x1a x4a));
y <- set_irq_state IRQSignal x1a;
cap_insert (IRQHandlerCap x1a) x3a x2a
od) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchInterrupt_IF

lemma arch_invoke_irq_handler_globals_equiv[Interrupt_IF_assms, wp]:
  "arch_invoke_irq_handler irq \<lbrace>globals_equiv st\<rbrace>" by (cases irq; wpsimp wp: dmo_no_mem_globals_equiv simp: maskInterrupt_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st\<rbrace> arch_invoke_irq_handler irq \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
theory Ipc_IF

lemma get_cap_reads_respects:
  "reads_respects aag l (K (aag_can_read aag (fst slot) \<or> aag_can_affect aag l (fst slot))) (get_cap slot)" apply (simp add: get_cap_def split_def) apply (wp get_object_reads_respects | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (aag_can_read_or_affect aag l (fst slot))) (get_cap slot) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>y. aag_can_read_or_affect aag l (fst slot)) (do obj <- get_object (fst slot);
caps <- case obj of CNode sz cnode \<Rightarrow> do assert (well_formed_cnode_n sz cnode);
return cnode
od | TCB tcb \<Rightarrow> return (tcb_cnode_map tcb) | _ \<Rightarrow> fail;
assert_opt (caps (snd slot))
od) proof (prove)
goal:
No subgoals!
theory Ipc_IF

lemma set_thread_state_ext_runnable_equiv_but_for_labels:
  "\<lbrace>equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L) and st_tcb_at runnable thread\<rbrace>
   set_thread_state_ext thread
   \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>" apply (simp add: set_thread_state_ext_def) apply (wp gts_wp | rule hoare_pre_cont)+ apply (force simp: st_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L) and st_tcb_at runnable thread\<rbrace> set_thread_state_ext thread \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>equiv_but_for_labels aag L st and (\<lambda>y. pasObjectAbs aag thread \<in> L) and st_tcb_at runnable thread\<rbrace> do ts <- get_thread_state thread;
cur <- gets cur_thread;
action <- gets scheduler_action;
when (\<not> runnable ts \<and> cur = thread \<and> action = resume_cur_thread) (set_scheduler_action choose_new_thread)
od \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (equiv_but_for_labels aag L st and (\<lambda>y. pasObjectAbs aag thread \<in> L) and st_tcb_at runnable thread) s \<Longrightarrow> \<forall>sta. st_tcb_at ((=) sta) thread s \<longrightarrow> (if \<not> runnable sta \<and> cur_thread s = thread \<and> scheduler_action s = resume_cur_thread then \<lambda>_. False else equiv_but_for_labels aag L st) s proof (prove)
goal:
No subgoals!