theory ArchNoninterference

lemma getActiveIRQ_ret_no_dmo[Noninterference_assms, wp]:
  "\<lbrace>\<top>\<rbrace> 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) 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> 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 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. \<lbrace>?Q1\<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>rv s. \<forall>x. rv = Some x \<longrightarrow> x \<le> maxIRQ\<rbrace>
 2. \<And>s. True \<Longrightarrow> ?Q1 s proof (prove)
goal (2 subgoals):
 1. \<forall>n. irq_oracle n \<le> maxIRQ \<Longrightarrow> \<lbrace>?Q1\<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>rv s. \<forall>x. rv = Some x \<longrightarrow> x \<le> maxIRQ\<rbrace>
 2. \<And>s. \<lbrakk>True; \<forall>n. irq_oracle n \<le> maxIRQ\<rbrakk> \<Longrightarrow> ?Q1 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>True; \<forall>n. irq_oracle n \<le> maxIRQ\<rbrakk> \<Longrightarrow> (irq_masks s ((irq_oracle \<circ> irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>)) \<or> (irq_oracle \<circ> irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>) = 0x3FF \<or> in_kernel \<and> (irq_oracle \<circ> irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>) \<in> non_kernel_IRQs \<longrightarrow> (\<forall>x. None = Some x \<longrightarrow> x \<le> maxIRQ)) \<and> (\<not> (irq_masks s ((irq_oracle \<circ> irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>)) \<or> (irq_oracle \<circ> irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>) = 0x3FF \<or> in_kernel \<and> (irq_oracle \<circ> irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>) \<in> non_kernel_IRQs) \<longrightarrow> (\<forall>x. Some ((irq_oracle \<circ> irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>)) = Some x \<longrightarrow> x \<le> maxIRQ)) proof (prove)
goal:
No subgoals!