theory IRQMasks_IF

lemma call_kernel_irq_masks:
  "\<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False (st :: 's state) and einvs
                                   and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s)\<rbrace>
   call_kernel ev
   \<lbrace>\<lambda>rv s. P (irq_masks_of_state s)\<rbrace>" apply (simp add: call_kernel_def) apply (wp handle_interrupt_irq_masks[where st=st])+ apply (rule_tac Q="\<lambda>rv s. P (irq_masks_of_state s) \<and> domain_sep_inv False st s \<and>
                              (\<forall>x. rv = Some x \<longrightarrow> x \<le> maxIRQ)" in hoare_strengthen_post) apply (wp | simp)+ apply (rule_tac Q="\<lambda>x s. P (irq_masks_of_state s) \<and> domain_sep_inv False st s"
               and F="E" for E in hoare_post_impErr) apply (rule valid_validE) apply (wp handle_event_irq_masks[where st=st] valid_validE[OF handle_event_domain_sep_inv]
            | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and einvs and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s)\<rbrace> call_kernel ev \<lbrace>\<lambda>rv s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and einvs and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s)\<rbrace> do y <- handle_event ev <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od));
y <- schedule;
activate_thread
od \<lbrace>\<lambda>rv s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>?F8 x\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>irq. if \<exists>y. irq = Some y then (\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and K (the irq \<le> maxIRQ) else (\<lambda>s. P (irq_masks_of_state s))\<rbrace>
 2. \<lbrace>?Q\<rbrace> handle_event ev \<lbrace>\<lambda>y s. P (irq_masks_of_state s)\<rbrace>, \<lbrace>?F8\<rbrace>
 3. \<And>s. ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and einvs and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s)) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrace>?F8 x\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>rv s. P (irq_masks_of_state s) \<and> domain_sep_inv False st s \<and> (\<forall>x. rv = Some x \<longrightarrow> x \<le> maxIRQ)\<rbrace>
 2. \<And>x rv s. P (irq_masks_of_state s) \<and> domain_sep_inv False st s \<and> (\<forall>x. rv = Some x \<longrightarrow> x \<le> maxIRQ) \<Longrightarrow> (if \<exists>y. rv = Some y then (\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and K (the rv \<le> maxIRQ) else (\<lambda>s. P (irq_masks_of_state s))) s
 3. \<lbrace>?Q\<rbrace> handle_event ev \<lbrace>\<lambda>y s. P (irq_masks_of_state s)\<rbrace>, \<lbrace>?F8\<rbrace>
 4. \<And>s. ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and einvs and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s)) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> handle_event ev \<lbrace>\<lambda>y s. P (irq_masks_of_state s)\<rbrace>, \<lbrace>\<lambda>x s. P (irq_masks_of_state s) \<and> domain_sep_inv False st s\<rbrace>
 2. \<And>s. ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and einvs and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s)) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q\<rbrace> handle_event ev \<lbrace>\<lambda>x s. P (irq_masks_of_state s) \<and> domain_sep_inv False st s\<rbrace>, \<lbrace>?E27\<rbrace>
 2. \<And>rv s. P (irq_masks_of_state s) \<and> domain_sep_inv False st s \<Longrightarrow> P (irq_masks_of_state s)
 3. \<And>e s. ?E27 e s \<Longrightarrow> P (irq_masks_of_state s) \<and> domain_sep_inv False st s
 4. \<And>s. ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and einvs and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s)) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q\<rbrace> handle_event ev \<lbrace>\<lambda>x s. P (irq_masks_of_state s) \<and> domain_sep_inv False st s\<rbrace>
 2. \<And>rv s. P (irq_masks_of_state s) \<and> domain_sep_inv False st s \<Longrightarrow> P (irq_masks_of_state s)
 3. \<And>e s. P (irq_masks_of_state s) \<and> domain_sep_inv False st s \<Longrightarrow> P (irq_masks_of_state s) \<and> domain_sep_inv False st s
 4. \<And>s. ((\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and einvs and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s)) s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!