kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchArch_AI

lemma aligned_sum_less_kernel_base:
  "vmsz_aligned p sz
    \<Longrightarrow> (p + 2 ^ pageBitsForSize sz - 1 < kernel_base) = (p < kernel_base)" apply (rule iffI) apply (rule le_less_trans) apply (rule is_aligned_no_overflow) apply (simp add: vmsz_aligned_def) apply simp apply (simp add:field_simps[symmetric]) apply (erule gap_between_aligned) apply (simp add: vmsz_aligned_def)+ apply (case_tac sz,simp_all add:kernel_base_def is_aligned_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vmsz_aligned p sz \<Longrightarrow> (p + 2 ^ pageBitsForSize sz - 1 < kernel_base) = (p < kernel_base) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>vmsz_aligned p sz; p + 2 ^ pageBitsForSize sz - 1 < kernel_base\<rbrakk> \<Longrightarrow> p < kernel_base
 2. \<lbrakk>vmsz_aligned p sz; p < kernel_base\<rbrakk> \<Longrightarrow> p + 2 ^ pageBitsForSize sz - 1 < kernel_base proof (prove)
goal (3 subgoals):
 1. \<lbrakk>vmsz_aligned p sz; p + 2 ^ pageBitsForSize sz - 1 < kernel_base\<rbrakk> \<Longrightarrow> p \<le> ?y3
 2. \<lbrakk>vmsz_aligned p sz; p + 2 ^ pageBitsForSize sz - 1 < kernel_base\<rbrakk> \<Longrightarrow> ?y3 < kernel_base
 3. \<lbrakk>vmsz_aligned p sz; p < kernel_base\<rbrakk> \<Longrightarrow> p + 2 ^ pageBitsForSize sz - 1 < kernel_base proof (prove)
goal (3 subgoals):
 1. \<lbrakk>vmsz_aligned p sz; p + 2 ^ pageBitsForSize sz - 1 < kernel_base\<rbrakk> \<Longrightarrow> is_aligned p ?sz6
 2. \<lbrakk>vmsz_aligned p sz; p + 2 ^ pageBitsForSize sz - 1 < kernel_base\<rbrakk> \<Longrightarrow> p + 2 ^ ?sz6 - 1 < kernel_base
 3. \<lbrakk>vmsz_aligned p sz; p < kernel_base\<rbrakk> \<Longrightarrow> p + 2 ^ pageBitsForSize sz - 1 < kernel_base proof (prove)
goal (2 subgoals):
 1. \<lbrakk>vmsz_aligned p sz; p + 2 ^ pageBitsForSize sz - 1 < kernel_base\<rbrakk> \<Longrightarrow> p + 2 ^ pageBitsForSize sz - 1 < kernel_base
 2. \<lbrakk>vmsz_aligned p sz; p < kernel_base\<rbrakk> \<Longrightarrow> p + 2 ^ pageBitsForSize sz - 1 < kernel_base proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vmsz_aligned p sz; p < kernel_base\<rbrakk> \<Longrightarrow> p + 2 ^ pageBitsForSize sz - 1 < kernel_base proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vmsz_aligned p sz; p < kernel_base\<rbrakk> \<Longrightarrow> p + (2 ^ pageBitsForSize sz - 1) < kernel_base proof (prove)
goal (3 subgoals):
 1. vmsz_aligned p sz \<Longrightarrow> is_aligned p (pageBitsForSize sz)
 2. vmsz_aligned p sz \<Longrightarrow> is_aligned kernel_base (pageBitsForSize sz)
 3. vmsz_aligned p sz \<Longrightarrow> pageBitsForSize sz < LENGTH(32) proof (prove)
goal (2 subgoals):
 1. is_aligned p (pageBitsForSize sz) \<Longrightarrow> is_aligned kernel_base (pageBitsForSize sz)
 2. vmsz_aligned p sz \<Longrightarrow> pageBitsForSize sz < LENGTH(32) proof (prove)
goal:
No subgoals!
theory Interrupt_AI

lemma valid_irq_handlersD:
  "\<lbrakk>cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s; valid_irq_handlers s\<rbrakk>  \<Longrightarrow>
  interrupt_states s irq = IRQSignal" apply(auto simp: valid_irq_handlers_def cte_wp_at_caps_of_state irq_issued_def cap_irqs_def cap_irq_opt_def split: cap.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s; valid_irq_handlers s\<rbrakk> \<Longrightarrow> interrupt_states s irq = IRQSignal proof (prove)
goal:
No subgoals!
theory Interrupt_AI

lemma mod_le:
  "\<lbrakk>b < c;b dvd c\<rbrakk>  \<Longrightarrow> (a mod b \<le> a mod (c::nat))" apply (subst mod_mod_cancel[symmetric],simp) by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b < c; b dvd c\<rbrakk> \<Longrightarrow> a mod b \<le> a mod c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b < c; b dvd c\<rbrakk> \<Longrightarrow> a mod c mod b \<le> a mod c
theory Interrupt_AI

lemma is_up_8_32: "is_up (ucast :: word8 \<Rightarrow> word32)" by (simp add: is_up_def source_size_def target_size_def word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_up UCAST(8 \<rightarrow> 32)
theory Interrupt_AI

lemma cap_delete_one_cte_cap_to[wp]:
  "\<lbrace>ex_cte_cap_wp_to P ptr\<rbrace> cap_delete_one ptr' \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P ptr\<rbrace>" apply (simp add: ex_cte_cap_wp_to_def) apply (wp hoare_vcg_ex_lift
            hoare_use_eq_irq_node [OF cap_delete_one_irq_node
                                      cap_delete_one_cte_wp_at_preserved]) apply (clarsimp simp: can_fast_finalise_def split: cap.split_asm)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_cte_cap_wp_to P ptr\<rbrace> cap_delete_one ptr' \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>a b. cte_wp_at (\<lambda>c. P c \<and> ptr \<in> cte_refs c (interrupt_irq_node s)) (a, b) s\<rbrace> cap_delete_one ptr' \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (\<lambda>c. P c \<and> ptr \<in> cte_refs c (interrupt_irq_node s)) (a, b) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a b f cap. P cap \<and> ptr \<in> cte_refs cap f \<Longrightarrow> \<not> can_fast_finalise cap
 2. \<And>s. \<exists>a b. cte_wp_at (\<lambda>c. P c \<and> ptr \<in> cte_refs c (interrupt_irq_node s)) (a, b) s \<Longrightarrow> \<exists>x xa. cte_wp_at (\<lambda>a. P a \<and> ptr \<in> cte_refs a (interrupt_irq_node s)) (x, xa) s proof (prove)
goal:
No subgoals!
theory Interrupt_AI

lemma get_irq_slot_ex_cte:
  "\<lbrace>\<lambda>s. \<exists>ptr. cte_wp_at ((=) (cap.IRQHandlerCap irq)) ptr s \<and> P (cap.IRQHandlerCap irq)\<rbrace>
      get_irq_slot irq
   \<lbrace>ex_cte_cap_wp_to P\<rbrace>" apply (simp add: get_irq_slot_def) apply wp apply (simp add: ex_cte_cap_wp_to_def) apply (elim conjE exEI cte_wp_at_weakenE) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>ptr. cte_wp_at ((=) (IRQHandlerCap irq)) ptr s \<and> P (IRQHandlerCap irq)\<rbrace> get_irq_slot irq \<lbrace>ex_cte_cap_wp_to P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s) \<and> P (IRQHandlerCap irq)\<rbrace> gets (\<lambda>st. (interrupt_irq_node st irq, [])) \<lbrace>ex_cte_cap_wp_to P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s) \<and> P (IRQHandlerCap irq) \<Longrightarrow> ex_cte_cap_wp_to P (interrupt_irq_node s irq, []) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s) \<and> P (IRQHandlerCap irq) \<Longrightarrow> \<exists>a b. cte_wp_at (\<lambda>c. P c \<and> (interrupt_irq_node s irq, []) \<in> cte_refs c (interrupt_irq_node s)) (a, b) s proof (prove)
goal (1 subgoal):
 1. \<And>s x xa c. \<lbrakk>P (IRQHandlerCap irq); IRQHandlerCap irq = c\<rbrakk> \<Longrightarrow> P c \<and> (interrupt_irq_node s irq, []) \<in> cte_refs c (interrupt_irq_node s) proof (prove)
goal:
No subgoals!
theory Interrupt_AI

lemma valid_mdb_interrupts[simp]:
  "valid_mdb (interrupt_states_update f s) = valid_mdb s" by (simp add: valid_mdb_def mdb_cte_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_mdb (interrupt_states_update f s) = valid_mdb s
theory Interrupt_AI

lemma set_irq_state_issued[wp]:
  "\<lbrace>\<top>\<rbrace> set_irq_state irq_state.IRQSignal irq \<lbrace>\<lambda>rv. irq_issued irq\<rbrace>" apply (simp add: set_irq_state_def irq_issued_def) apply wp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> set_irq_state IRQSignal irq \<lbrace>\<lambda>rv. irq_issued irq\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do y <- modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(irq := IRQSignal)\<rparr>);
do_machine_op (maskInterrupt False irq)
od \<lbrace>\<lambda>rv s. interrupt_states s irq = IRQSignal\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> interrupt_states (s\<lparr>interrupt_states := (interrupt_states s)(irq := IRQSignal)\<rparr>) irq = IRQSignal proof (prove)
goal:
No subgoals!
theory Interrupt_AI

lemma IRQHandler_valid:
  "(s \<turnstile> cap.IRQHandlerCap irq) = (irq \<le> maxIRQ)" by (simp add: valid_cap_def cap_aligned_def word_bits_conv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> IRQHandlerCap irq = (irq \<le> maxIRQ)
theory ArchInterrupt_AI

lemma get_irq_slot_different_ARCH[Interrupt_AI_asms]:
  "\<lbrace>\<lambda>s. valid_global_refs s \<and> ex_cte_cap_wp_to is_cnode_cap ptr s\<rbrace>
      get_irq_slot irq
   \<lbrace>\<lambda>rv s. rv \<noteq> ptr\<rbrace>" apply (simp add: get_irq_slot_def) apply wp apply (clarsimp simp: valid_global_refs_def valid_refs_def
                        ex_cte_cap_wp_to_def) apply (elim allE, erule notE, erule cte_wp_at_weakenE) apply (clarsimp simp: global_refs_def is_cap_simps cap_range_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_global_refs s \<and> ex_cte_cap_wp_to is_cnode_cap ptr s\<rbrace> get_irq_slot irq \<lbrace>\<lambda>rv s. rv \<noteq> ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_global_refs s \<and> ex_cte_cap_wp_to is_cnode_cap ptr s\<rbrace> gets (\<lambda>st. (interrupt_irq_node st irq, [])) \<lbrace>\<lambda>rv s. rv \<noteq> ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_global_refs s \<and> ex_cte_cap_wp_to is_cnode_cap ptr s \<Longrightarrow> (interrupt_irq_node s irq, []) \<noteq> ptr proof (prove)
goal (1 subgoal):
 1. \<And>s 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. is_cnode_cap c \<and> (interrupt_irq_node s irq, []) \<in> cte_refs c (interrupt_irq_node s)) (a, b) s; ptr = (interrupt_irq_node s irq, [])\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s a b c. \<lbrakk>ptr = (interrupt_irq_node s irq, []); is_cnode_cap c \<and> (interrupt_irq_node s irq, []) \<in> cte_refs c (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> global_refs s \<inter> cap_range c \<noteq> {} proof (prove)
goal:
No subgoals!
theory ArchInterrupt_AI

lemma is_derived_use_interrupt_ARCH[Interrupt_AI_asms]:
  "(is_ntfn_cap cap \<and> interrupt_derived cap cap') \<longrightarrow> (is_derived m p cap cap')" apply (clarsimp simp: is_cap_simps) apply (clarsimp simp: interrupt_derived_def is_derived_def) apply (clarsimp simp: cap_master_cap_def split: cap.split_asm) apply (simp add: is_cap_simps is_pt_cap_def vs_cap_ref_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_ntfn_cap cap \<and> interrupt_derived cap cap' \<longrightarrow> is_derived m p cap cap' proof (prove)
goal (1 subgoal):
 1. \<And>r b R. \<lbrakk>interrupt_derived (NotificationCap r b R) cap'; cap = NotificationCap r b R\<rbrakk> \<Longrightarrow> is_derived m p (NotificationCap r b R) cap' proof (prove)
goal (1 subgoal):
 1. \<And>r b R. \<lbrakk>cap = NotificationCap r b R; cap_master_cap (NotificationCap r b R) = cap_master_cap cap'; (cap_badge cap', Some b) \<in> capBadge_ordering False\<rbrakk> \<Longrightarrow> (is_untyped_cap cap' \<longrightarrow> \<not> is_zombie cap' \<and> descendants_of p m = {} \<and> is_master_reply_cap cap' = is_reply_cap (NotificationCap r b R) \<and> \<not> is_pt_cap (NotificationCap r b R) \<and> \<not> is_pd_cap (NotificationCap r b R) \<and> (vs_cap_ref (NotificationCap r b R) = vs_cap_ref cap' \<or> is_pg_cap cap') \<and> \<not> is_reply_cap cap' \<and> \<not> is_master_reply_cap (NotificationCap r b R)) \<and> (\<not> is_untyped_cap cap' \<longrightarrow> \<not> is_zombie cap' \<and> is_master_reply_cap cap' = is_reply_cap (NotificationCap r b R) \<and> \<not> is_pt_cap (NotificationCap r b R) \<and> \<not> is_pd_cap (NotificationCap r b R) \<and> (vs_cap_ref (NotificationCap r b R) = vs_cap_ref cap' \<or> is_pg_cap cap') \<and> \<not> is_reply_cap cap' \<and> \<not> is_master_reply_cap (NotificationCap r b R)) proof (prove)
goal (1 subgoal):
 1. \<And>b R x41 x42 x43. \<lbrakk>x42 = 0 \<or> x42 = b; cap = NotificationCap x41 b R; cap' = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> \<not> is_zombie (NotificationCap x41 x42 x43) \<and> is_master_reply_cap (NotificationCap x41 x42 x43) = is_reply_cap (NotificationCap x41 b R) \<and> \<not> is_pt_cap (NotificationCap x41 b R) \<and> \<not> is_pd_cap (NotificationCap x41 b R) \<and> (vs_cap_ref (NotificationCap x41 b R) = vs_cap_ref (NotificationCap x41 x42 x43) \<or> is_pg_cap (NotificationCap x41 x42 x43)) \<and> \<not> is_reply_cap (NotificationCap x41 x42 x43) \<and> \<not> is_master_reply_cap (NotificationCap x41 b R) proof (prove)
goal:
No subgoals!
theory ArchInterrupt_AI

lemma maskInterrupt_invs_ARCH[Interrupt_AI_asms]:
  "\<lbrace>invs and (\<lambda>s. \<not>b \<longrightarrow> interrupt_states s irq \<noteq> IRQInactive)\<rbrace>
   do_machine_op (maskInterrupt b irq)
   \<lbrace>\<lambda>rv. invs\<rbrace>" apply (simp add: do_machine_op_def split_def maskInterrupt_def) apply wp apply (clarsimp simp: in_monad invs_def valid_state_def all_invs_but_valid_irq_states_for_def
     valid_irq_states_but_def valid_irq_masks_but_def valid_machine_state_def cur_tcb_def valid_irq_states_def valid_irq_masks_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. \<not> b \<longrightarrow> interrupt_states s irq \<noteq> IRQInactive)\<rbrace> do_machine_op (maskInterrupt b irq) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. \<not> b \<longrightarrow> interrupt_states s irq \<noteq> IRQInactive)\<rbrace> do ms <- gets machine_state;
p <- select_f (modify (\<lambda>s. s\<lparr>irq_masks := (irq_masks s)(irq := b)\<rparr>) ms);
modify (machine_state_update (\<lambda>_. snd p))
od \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs and (\<lambda>s. \<not> b \<longrightarrow> interrupt_states s irq \<noteq> IRQInactive)) s \<Longrightarrow> \<forall>x\<in>fst (modify (\<lambda>s. s\<lparr>irq_masks := (irq_masks s)(irq := b)\<rparr>) (machine_state s)). invs (s\<lparr>machine_state := snd x\<rparr>) proof (prove)
goal:
No subgoals!
theory ArchInterrupt_AI

lemma no_cap_to_obj_with_diff_IRQHandler_ARCH[Interrupt_AI_asms]:
  "no_cap_to_obj_with_diff_ref (IRQHandlerCap irq) S = \<top>" by (rule ext, simp add: no_cap_to_obj_with_diff_ref_def
                          cte_wp_at_caps_of_state
                          obj_ref_none_no_asid)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_cap_to_obj_with_diff_ref (IRQHandlerCap irq) S = (\<lambda>_. True)
theory ArchInterrupt_AI

lemma (* set_irq_state_valid_cap *)[Interrupt_AI_asms]:
  "\<lbrace>valid_cap cap\<rbrace> set_irq_state IRQSignal irq \<lbrace>\<lambda>rv. valid_cap cap\<rbrace>" apply (clarsimp simp: set_irq_state_def) apply (wp do_machine_op_valid_cap) apply (auto simp: valid_cap_def valid_untyped_def
             split: cap.splits option.splits arch_cap.splits
         split del: if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap cap\<rbrace> set_irq_state IRQSignal irq \<lbrace>\<lambda>rv. valid_cap cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap cap\<rbrace> do y <- modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(irq := IRQSignal)\<rparr>);
do_machine_op (maskInterrupt False irq)
od \<lbrace>\<lambda>rv. valid_cap cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<turnstile> cap \<Longrightarrow> s\<lparr>interrupt_states := (interrupt_states s)(irq := IRQSignal)\<rparr> \<turnstile> cap proof (prove)
goal:
No subgoals!
theory ArchInterrupt_AI

lemma empty_fail_ackInterrupt_ARCH[Interrupt_AI_asms]:
  "empty_fail (ackInterrupt irq)" by (wp | simp add: ackInterrupt_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (ackInterrupt irq)
theory ArchInterrupt_AI

lemma empty_fail_maskInterrupt_ARCH[Interrupt_AI_asms]:
  "empty_fail (maskInterrupt f irq)" by (wp | simp add: maskInterrupt_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (maskInterrupt f irq)
theory ArchInterrupt_AI

lemma sts_arch_irq_control_inv_valid[wp, Interrupt_AI_asms]:
  "\<lbrace>arch_irq_control_inv_valid i\<rbrace>
       set_thread_state t st
   \<lbrace>\<lambda>rv. arch_irq_control_inv_valid i\<rbrace>" apply (simp add: arch_irq_control_inv_valid_def) apply (cases i) apply (clarsimp) apply (wp ex_cte_cap_to_pres | simp add: cap_table_at_typ)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>arch_irq_control_inv_valid i\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. arch_irq_control_inv_valid i\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>arch_irq_control_inv_valid_real i\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. arch_irq_control_inv_valid_real i\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. i = ArchIRQControlIssue x1 x2 x3 x4 \<Longrightarrow> \<lbrace>arch_irq_control_inv_valid_real i\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. arch_irq_control_inv_valid_real i\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 a b aa ba x4. i = ArchIRQControlIssue x1 (a, b) (aa, ba) x4 \<Longrightarrow> \<lbrace>cte_wp_at ((=) NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. x1 \<le> maxIRQ)\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. cte_wp_at ((=) NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. x1 \<le> maxIRQ)\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma schedule_invs[wp]: "\<lbrace>invs\<rbrace> (Schedule_A.schedule :: (unit,det_ext) s_monad) \<lbrace>\<lambda>rv. invs\<rbrace>" supply if_split[split del] apply (simp add: Schedule_A.schedule_def) apply (wp dmo_invs thread_get_inv gts_wp
            do_machine_op_tcb when_def hoare_vcg_all_lift
          | wpc
          | clarsimp simp: guarded_switch_to_def get_tcb_def choose_thread_def ethread_get_def
                           ethread_get_when_def
          | wp (once) hoare_drop_imps
          | simp add: schedule_choose_new_thread_def if_apply_def2)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> schedule \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> schedule \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> do ct <- gets cur_thread;
ct_st <- get_thread_state ct;
gets scheduler_action >>= case_scheduler_action (do id <- gets idle_thread;
assert (runnable ct_st \<or> ct = id)
od) (\<lambda>candidate. do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (ct \<noteq> it) tcb_priority ct;
fastfail <- schedule_switch_thread_fastfail ct it ct_prio target_prio;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do y <- tcb_sched_action tcb_sched_enqueue candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable ct_st \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od) (do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
schedule_choose_new_thread
od)
od \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma guarded_switch_to_ct_in_state_activatable[wp]:
  "\<lbrace>\<top>\<rbrace> guarded_switch_to t \<lbrace>\<lambda>a. ct_in_state activatable\<rbrace>" unfolding guarded_switch_to_def apply (wp stt_activatable) apply (wp hoare_vcg_imp_lift gts_wp)+ apply (clarsimp simp: pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> guarded_switch_to t \<lbrace>\<lambda>a. ct_in_state activatable\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do ts <- get_thread_state t;
assert (runnable ts);
switch_to_thread t
od \<lbrace>\<lambda>a. ct_in_state activatable\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> get_thread_state t \<lbrace>\<lambda>ts s. runnable ts \<longrightarrow> st_tcb_at runnable t s\<rbrace>
 2. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> \<not> runnable st) \<or> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> st_tcb_at runnable t s) proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma syscall_valid:
  assumes x:
             "\<And>ft. \<lbrace>P_flt ft\<rbrace> h_flt ft \<lbrace>Q\<rbrace>"
             "\<And>err. \<lbrace>P_err err\<rbrace> h_err err \<lbrace>Q\<rbrace>"
             "\<And>rv. \<lbrace>P_no_err rv\<rbrace> m_fin rv \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
             "\<And>rv. \<lbrace>P_no_flt rv\<rbrace> m_err rv \<lbrace>P_no_err\<rbrace>, \<lbrace>P_err\<rbrace>"
             "\<lbrace>P\<rbrace> m_flt \<lbrace>P_no_flt\<rbrace>, \<lbrace>P_flt\<rbrace>"
  shows "\<lbrace>P\<rbrace> Syscall_A.syscall m_flt h_flt m_err h_err m_fin \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>" apply (simp add: Syscall_A.syscall_def liftE_bindE
             cong: sum.case_cong) apply (rule hoare_split_bind_case_sumE) apply (wp x)[1] apply (rule hoare_split_bind_case_sumE) apply (wp x|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> syscall m_flt h_flt m_err h_err m_fin \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> m_flt >>= case_sum (\<lambda>f. liftE (h_flt f)) (\<lambda>a. m_err a >>= case_sum (\<lambda>e. liftE (h_err e)) m_fin) \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv. \<lbrace>?R6 rv\<rbrace> liftE (h_flt rv) \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>rv. \<lbrace>?S6 rv\<rbrace> m_err rv >>= case_sum (\<lambda>e. liftE (h_err e)) m_fin \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
 3. \<lbrace>P\<rbrace> m_flt \<lbrace>?S6\<rbrace>, \<lbrace>?R6\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv. \<lbrace>?S6 rv\<rbrace> m_err rv >>= case_sum (\<lambda>e. liftE (h_err e)) m_fin \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
 2. \<lbrace>P\<rbrace> m_flt \<lbrace>?S6\<rbrace>, \<lbrace>P_flt\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv rva. \<lbrace>?R14 rv rva\<rbrace> liftE (h_err rva) \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>rv rva. \<lbrace>?S14 rv rva\<rbrace> m_fin rva \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
 3. \<And>rv. \<lbrace>?S6 rv\<rbrace> m_err rv \<lbrace>?S14 rv\<rbrace>, \<lbrace>?R14 rv\<rbrace>
 4. \<lbrace>P\<rbrace> m_flt \<lbrace>?S6\<rbrace>, \<lbrace>P_flt\<rbrace> proof (prove)
goal:
No subgoals!