theory ArchIRQMasks_IF

lemma dmo_getActiveIRQ_return_axiom[IRQMasks_IF_assms, wp]:
  "\<lbrace>\<top>\<rbrace> do_machine_op (getActiveIRQ in_kernel) \<lbrace>\<lambda>rv s. (\<forall>x. rv = Some x \<longrightarrow> x \<le> maxIRQ)\<rbrace>" apply (simp add: getActiveIRQ_def) apply (rule hoare_pre, rule dmo_wp) apply (insert irq_oracle_max_irq) apply (wp dmo_getActiveIRQ_irq_masks) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do_machine_op (getActiveIRQ in_kernel) \<lbrace>\<lambda>rv s. \<forall>x. rv = Some x \<longrightarrow> x \<le> maxIRQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do_machine_op (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 \<or> in_kernel \<and> active_irq \<in> non_kernel_IRQs then return None else return (Some active_irq)
od) \<lbrace>\<lambda>rv s. \<forall>x. rv = Some x \<longrightarrow> x \<le> maxIRQ\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrace>?P4 s\<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 \<or> in_kernel \<and> active_irq \<in> non_kernel_IRQs then return None else return (Some active_irq)
od \<lbrace>\<lambda>a b. \<forall>x. a = Some x \<longrightarrow> x \<le> maxIRQ\<rbrace>
 2. \<And>s. True \<Longrightarrow> ?P4 s (machine_state s) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<forall>n. irq_oracle n \<le> maxIRQ \<Longrightarrow> \<lbrace>?P4 s\<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 \<or> in_kernel \<and> active_irq \<in> non_kernel_IRQs then return None else return (Some active_irq)
od \<lbrace>\<lambda>a b. \<forall>x. a = Some x \<longrightarrow> x \<le> maxIRQ\<rbrace>
 2. \<And>s. \<lbrakk>True; \<forall>n. irq_oracle n \<le> maxIRQ\<rbrakk> \<Longrightarrow> ?P4 s (machine_state s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>True; \<forall>n. irq_oracle n \<le> maxIRQ\<rbrakk> \<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 \<or> in_kernel \<and> (irq_oracle \<circ> irq_state) (machine_state s\<lparr>irq_state := Suc (irq_state (machine_state s))\<rparr>) \<in> non_kernel_IRQs \<longrightarrow> (\<forall>x. None = Some x \<longrightarrow> x \<le> maxIRQ)) \<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 \<or> in_kernel \<and> (irq_oracle \<circ> irq_state) (machine_state s\<lparr>irq_state := Suc (irq_state (machine_state s))\<rparr>) \<in> non_kernel_IRQs) \<longrightarrow> (\<forall>x. Some ((irq_oracle \<circ> irq_state) (machine_state s\<lparr>irq_state := Suc (irq_state (machine_state s))\<rparr>)) = Some x \<longrightarrow> x \<le> maxIRQ)) proof (prove)
goal:
No subgoals!