theory ArchCNode_IF

lemma dmo_getActiveIRQ_wp[CNode_IF_assms]:
  "\<lbrace>\<lambda>s. P (irq_at (irq_state (machine_state s) + 1) (irq_masks (machine_state s)))
          (s\<lparr>machine_state := (machine_state s\<lparr>irq_state := irq_state (machine_state s) + 1\<rparr>)\<rparr>)\<rbrace>
   do_machine_op (getActiveIRQ in_kernel)
   \<lbrace>P\<rbrace>" apply (simp add: do_machine_op_def getActiveIRQ_def non_kernel_IRQs_def) apply (wp modify_wp | wpc)+ apply clarsimp apply (erule use_valid) apply (wp modify_wp) apply (auto simp: irq_at_def Let_def split: if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (irq_at (irq_state (machine_state s) + 1) (irq_masks (machine_state s))) (s\<lparr>machine_state := machine_state s\<lparr>irq_state := irq_state (machine_state s) + 1\<rparr>\<rparr>)\<rbrace> do_machine_op (getActiveIRQ in_kernel) \<lbrace>P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (irq_at (Suc (irq_state (machine_state s))) (irq_masks (machine_state s))) (s\<lparr>machine_state := machine_state s\<lparr>irq_state := Suc (irq_state (machine_state s))\<rparr>\<rparr>)\<rbrace> do ms <- gets machine_state;
(r, ms') <- select_f ((do is_masked <- gets irq_masks;
y <- modify (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>);
active_irq <- gets (irq_oracle \<circ> irq_state);
if is_masked active_irq \<or> active_irq = 0x3FF then return None else return (Some active_irq)
od) ms);
y <- modify (machine_state_update (\<lambda>_. ms'));
return r
od \<lbrace>P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (irq_at (Suc (irq_state (machine_state s))) (irq_masks (machine_state s))) (s\<lparr>machine_state := machine_state s\<lparr>irq_state := Suc (irq_state (machine_state s))\<rparr>\<rparr>) \<Longrightarrow> \<forall>x\<in>fst ((do is_masked <- gets irq_masks;
y <- modify (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>);
active_irq <- gets (irq_oracle \<circ> irq_state);
if is_masked active_irq \<or> active_irq = 0x3FF then return None else return (Some active_irq)
od) (machine_state s)). \<forall>xa xb. x = (xa, xb) \<longrightarrow> P xa (s\<lparr>machine_state := xb\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa. \<lbrakk>P (irq_at (Suc (irq_state (machine_state s))) (irq_masks (machine_state s))) (s\<lparr>machine_state := machine_state s\<lparr>irq_state := Suc (irq_state (machine_state s))\<rparr>\<rparr>); (x, xa) \<in> fst ((do is_masked <- gets irq_masks;
y <- modify (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>);
active_irq <- gets (irq_oracle \<circ> irq_state);
if is_masked active_irq \<or> active_irq = 0x3FF then return None else return (Some active_irq)
od) (machine_state s))\<rbrakk> \<Longrightarrow> P x (s\<lparr>machine_state := xa\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s x xa. P (irq_at (Suc (irq_state (machine_state s))) (irq_masks (machine_state s))) (s\<lparr>machine_state := machine_state s\<lparr>irq_state := Suc (irq_state (machine_state s))\<rparr>\<rparr>) \<Longrightarrow> \<lbrace>?P32 s x xa\<rbrace> do is_masked <- gets irq_masks;
y <- modify (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>);
active_irq <- gets (irq_oracle \<circ> irq_state);
if is_masked active_irq \<or> active_irq = 0x3FF then return None else return (Some active_irq)
od \<lbrace>\<lambda>a b. P a (s\<lparr>machine_state := b\<rparr>)\<rbrace>
 2. \<And>s x xa. P (irq_at (Suc (irq_state (machine_state s))) (irq_masks (machine_state s))) (s\<lparr>machine_state := machine_state s\<lparr>irq_state := Suc (irq_state (machine_state s))\<rparr>\<rparr>) \<Longrightarrow> ?P32 s x xa (machine_state s) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa. P (irq_at (Suc (irq_state (machine_state s))) (irq_masks (machine_state s))) (s\<lparr>machine_state := machine_state s\<lparr>irq_state := Suc (irq_state (machine_state s))\<rparr>\<rparr>) \<Longrightarrow> (irq_masks (machine_state s) ((irq_oracle \<circ> irq_state) (machine_state s\<lparr>irq_state := Suc (irq_state (machine_state s))\<rparr>)) \<or> (irq_oracle \<circ> irq_state) (machine_state s\<lparr>irq_state := Suc (irq_state (machine_state s))\<rparr>) = 0x3FF \<longrightarrow> P None (s\<lparr>machine_state := machine_state s\<lparr>irq_state := Suc (irq_state (machine_state s))\<rparr>\<rparr>)) \<and> (\<not> (irq_masks (machine_state s) ((irq_oracle \<circ> irq_state) (machine_state s\<lparr>irq_state := Suc (irq_state (machine_state s))\<rparr>)) \<or> (irq_oracle \<circ> irq_state) (machine_state s\<lparr>irq_state := Suc (irq_state (machine_state s))\<rparr>) = 0x3FF) \<longrightarrow> P (Some ((irq_oracle \<circ> irq_state) (machine_state s\<lparr>irq_state := Suc (irq_state (machine_state s))\<rparr>))) (s\<lparr>machine_state := machine_state s\<lparr>irq_state := Suc (irq_state (machine_state s))\<rparr>\<rparr>)) proof (prove)
goal:
No subgoals!