theory ArchADT_IF_Refine

lemma dmo'_getActiveIRQ_wp[ADT_IF_Refine_assms]:
  "\<lbrace>\<lambda>s. P (irq_at (irq_state (ksMachineState s) + 1) (irq_masks (ksMachineState s)))
          (s\<lparr>ksMachineState := (ksMachineState s\<lparr>irq_state := irq_state (ksMachineState s) + 1\<rparr>)\<rparr>)\<rbrace>
   doMachineOp (getActiveIRQ in_kernel)
   \<lbrace>P\<rbrace>" apply(simp add: doMachineOp_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) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (irq_at (irq_state (ksMachineState s) + 1) (irq_masks (ksMachineState s))) (s\<lparr>ksMachineState := ksMachineState s\<lparr>irq_state := irq_state (ksMachineState s) + 1\<rparr>\<rparr>)\<rbrace> doMachineOp (getActiveIRQ in_kernel) \<lbrace>P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (irq_at (Suc (irq_state (ksMachineState s))) (irq_masks (ksMachineState s))) (s\<lparr>ksMachineState := ksMachineState s\<lparr>irq_state := Suc (irq_state (ksMachineState s))\<rparr>\<rparr>)\<rbrace> do ms <- gets ksMachineState;
(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 (ksMachineState_update (\<lambda>_. ms'));
return r
od \<lbrace>P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (irq_at (Suc (irq_state (ksMachineState s))) (irq_masks (ksMachineState s))) (s\<lparr>ksMachineState := ksMachineState s\<lparr>irq_state := Suc (irq_state (ksMachineState 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) (ksMachineState s)). \<forall>xa xb. x = (xa, xb) \<longrightarrow> P xa (s\<lparr>ksMachineState := xb\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa. \<lbrakk>P (irq_at (Suc (irq_state (ksMachineState s))) (irq_masks (ksMachineState s))) (s\<lparr>ksMachineState := ksMachineState s\<lparr>irq_state := Suc (irq_state (ksMachineState 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) (ksMachineState s))\<rbrakk> \<Longrightarrow> P x (s\<lparr>ksMachineState := xa\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s x xa. P (irq_at (Suc (irq_state (ksMachineState s))) (irq_masks (ksMachineState s))) (s\<lparr>ksMachineState := ksMachineState s\<lparr>irq_state := Suc (irq_state (ksMachineState 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>ksMachineState := b\<rparr>)\<rbrace>
 2. \<And>s x xa. P (irq_at (Suc (irq_state (ksMachineState s))) (irq_masks (ksMachineState s))) (s\<lparr>ksMachineState := ksMachineState s\<lparr>irq_state := Suc (irq_state (ksMachineState s))\<rparr>\<rparr>) \<Longrightarrow> ?P32 s x xa (ksMachineState s) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa. P (irq_at (Suc (irq_state (ksMachineState s))) (irq_masks (ksMachineState s))) (s\<lparr>ksMachineState := ksMachineState s\<lparr>irq_state := Suc (irq_state (ksMachineState s))\<rparr>\<rparr>) \<Longrightarrow> (irq_masks (ksMachineState s) ((irq_oracle \<circ> irq_state) (ksMachineState s\<lparr>irq_state := Suc (irq_state (ksMachineState s))\<rparr>)) \<or> (irq_oracle \<circ> irq_state) (ksMachineState s\<lparr>irq_state := Suc (irq_state (ksMachineState s))\<rparr>) = 0x3FF \<longrightarrow> P None (s\<lparr>ksMachineState := ksMachineState s\<lparr>irq_state := Suc (irq_state (ksMachineState s))\<rparr>\<rparr>)) \<and> (\<not> (irq_masks (ksMachineState s) ((irq_oracle \<circ> irq_state) (ksMachineState s\<lparr>irq_state := Suc (irq_state (ksMachineState s))\<rparr>)) \<or> (irq_oracle \<circ> irq_state) (ksMachineState s\<lparr>irq_state := Suc (irq_state (ksMachineState s))\<rparr>) = 0x3FF) \<longrightarrow> P (Some ((irq_oracle \<circ> irq_state) (ksMachineState s\<lparr>irq_state := Suc (irq_state (ksMachineState s))\<rparr>))) (s\<lparr>ksMachineState := ksMachineState s\<lparr>irq_state := Suc (irq_state (ksMachineState s))\<rparr>\<rparr>)) proof (prove)
goal:
No subgoals!