theory ArchNoninterference

lemma dmo_getActive_IRQ_reads_respect_scheduler[Noninterference_assms]:
  "reads_respects_scheduler aag l (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s)
                            (do_machine_op (getActiveIRQ in_kernel))" apply (simp add: getActiveIRQ_def) apply (simp add: dmo_distr dmo_if_distr dmo_gets_distr dmo_modify_distr cong: if_cong) apply wp apply (rule ev_modify[where P=\<top>]) apply (clarsimp simp: scheduler_equiv_def domain_fields_equiv_def globals_equiv_scheduler_def
                            scheduler_affects_equiv_def arch_scheduler_affects_equiv_def
                            states_equiv_for_def equiv_for_def equiv_asids_def equiv_asid_def
                            scheduler_globals_frame_equiv_def silc_dom_equiv_def idle_equiv_def) apply wp apply (rule_tac P="\<lambda>s. irq_masks_of_state st = irq_masks_of_state s" in gets_ev') apply wp apply clarsimp apply (simp add: scheduler_equiv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) (do_machine_op (getActiveIRQ in_kernel)) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) (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)) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) (do x <- gets irq_masks_of_state;
xa <- modify (machine_state_update (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>));
xa <- gets (\<lambda>s. irq_oracle (irq_state_of_state s));
if x xa \<or> xa = 0x3FF \<or> in_kernel \<and> xa \<in> non_kernel_IRQs then return None else return (Some xa)
od) proof (prove)
goal (5 subgoals):
 1. \<And>rv. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'5 rv) (modify (machine_state_update (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>)))
 2. \<And>rv. \<lbrace>?P''5 rv\<rbrace> modify (machine_state_update (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>)) \<lbrace>\<lambda>rva s. (\<forall>s t. scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> irq_oracle (irq_state_of_state s) = irq_oracle (irq_state_of_state t)) \<and> (rv (irq_oracle (irq_state_of_state s)) \<or> irq_oracle (irq_state_of_state s) = 0x3FF \<or> in_kernel \<and> irq_oracle (irq_state_of_state s) \<in> non_kernel_IRQs \<longrightarrow> True) \<and> (\<not> (rv (irq_oracle (irq_state_of_state s)) \<or> irq_oracle (irq_state_of_state s) = 0x3FF \<or> in_kernel \<and> irq_oracle (irq_state_of_state s) \<in> non_kernel_IRQs) \<longrightarrow> True)\<rbrace>
 3. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'4 (gets irq_masks_of_state)
 4. \<lbrace>?P''4\<rbrace> gets irq_masks_of_state \<lbrace>\<lambda>rv s. ?P'5 rv s \<and> ?P''5 rv s\<rbrace>
 5. \<And>s. irq_masks_of_state st = irq_masks_of_state s \<Longrightarrow> ?P'4 s \<and> ?P''4 s proof (prove)
goal (5 subgoals):
 1. \<And>rv s t. \<lbrakk>True; True; scheduler_affects_equiv aag l s t; scheduler_equiv aag s t\<rbrakk> \<Longrightarrow> scheduler_equiv aag (machine_state_update (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>) s) (machine_state_update (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>) t) \<and> scheduler_affects_equiv aag l (machine_state_update (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>) s) (machine_state_update (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>) t)
 2. \<And>rv. \<lbrace>?P''5 rv\<rbrace> modify (machine_state_update (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>)) \<lbrace>\<lambda>rva s. (\<forall>s t. scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> irq_oracle (irq_state_of_state s) = irq_oracle (irq_state_of_state t)) \<and> (rv (irq_oracle (irq_state_of_state s)) \<or> irq_oracle (irq_state_of_state s) = 0x3FF \<or> in_kernel \<and> irq_oracle (irq_state_of_state s) \<in> non_kernel_IRQs \<longrightarrow> True) \<and> (\<not> (rv (irq_oracle (irq_state_of_state s)) \<or> irq_oracle (irq_state_of_state s) = 0x3FF \<or> in_kernel \<and> irq_oracle (irq_state_of_state s) \<in> non_kernel_IRQs) \<longrightarrow> True)\<rbrace>
 3. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'4 (gets irq_masks_of_state)
 4. \<lbrace>?P''4\<rbrace> gets irq_masks_of_state \<lbrace>\<lambda>rv s. True \<and> ?P''5 rv s\<rbrace>
 5. \<And>s. irq_masks_of_state st = irq_masks_of_state s \<Longrightarrow> ?P'4 s \<and> ?P''4 s proof (prove)
goal (4 subgoals):
 1. \<And>rv. \<lbrace>?P''5 rv\<rbrace> modify (machine_state_update (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>)) \<lbrace>\<lambda>rva s. (\<forall>s t. scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> irq_oracle (irq_state_of_state s) = irq_oracle (irq_state_of_state t)) \<and> (rv (irq_oracle (irq_state_of_state s)) \<or> irq_oracle (irq_state_of_state s) = 0x3FF \<or> in_kernel \<and> irq_oracle (irq_state_of_state s) \<in> non_kernel_IRQs \<longrightarrow> True) \<and> (\<not> (rv (irq_oracle (irq_state_of_state s)) \<or> irq_oracle (irq_state_of_state s) = 0x3FF \<or> in_kernel \<and> irq_oracle (irq_state_of_state s) \<in> non_kernel_IRQs) \<longrightarrow> True)\<rbrace>
 2. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'4 (gets irq_masks_of_state)
 3. \<lbrace>?P''4\<rbrace> gets irq_masks_of_state \<lbrace>\<lambda>rv s. True \<and> ?P''5 rv s\<rbrace>
 4. \<And>s. irq_masks_of_state st = irq_masks_of_state s \<Longrightarrow> ?P'4 s \<and> ?P''4 s proof (prove)
goal (3 subgoals):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'4 (gets irq_masks_of_state)
 2. \<lbrace>?P''4\<rbrace> gets irq_masks_of_state \<lbrace>\<lambda>rv s. True \<and> (\<forall>s t. scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> irq_oracle (irq_state_of_state s) = irq_oracle (irq_state_of_state t)) \<and> (rv (irq_oracle (irq_state_of_state (machine_state_update (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>) s))) \<or> irq_oracle (irq_state_of_state (machine_state_update (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>) s)) = 0x3FF \<or> in_kernel \<and> irq_oracle (irq_state_of_state (machine_state_update (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>) s)) \<in> non_kernel_IRQs \<longrightarrow> True) \<and> (\<not> (rv (irq_oracle (irq_state_of_state (machine_state_update (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>) s))) \<or> irq_oracle (irq_state_of_state (machine_state_update (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>) s)) = 0x3FF \<or> in_kernel \<and> irq_oracle (irq_state_of_state (machine_state_update (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>) s)) \<in> non_kernel_IRQs) \<longrightarrow> True)\<rbrace>
 3. \<And>s. irq_masks_of_state st = irq_masks_of_state s \<Longrightarrow> ?P'4 s \<and> ?P''4 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P''4\<rbrace> gets irq_masks_of_state \<lbrace>\<lambda>rv s. True \<and> (\<forall>s t. scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> irq_oracle (irq_state_of_state s) = irq_oracle (irq_state_of_state t)) \<and> (rv (irq_oracle (irq_state_of_state (machine_state_update (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>) s))) \<or> irq_oracle (irq_state_of_state (machine_state_update (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>) s)) = 0x3FF \<or> in_kernel \<and> irq_oracle (irq_state_of_state (machine_state_update (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>) s)) \<in> non_kernel_IRQs \<longrightarrow> True) \<and> (\<not> (rv (irq_oracle (irq_state_of_state (machine_state_update (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>) s))) \<or> irq_oracle (irq_state_of_state (machine_state_update (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>) s)) = 0x3FF \<or> in_kernel \<and> irq_oracle (irq_state_of_state (machine_state_update (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>) s)) \<in> non_kernel_IRQs) \<longrightarrow> True)\<rbrace>
 2. \<And>s. irq_masks_of_state st = irq_masks_of_state s \<Longrightarrow> ((\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and K (\<forall>s t. irq_masks_of_state st = irq_masks_of_state s \<longrightarrow> irq_masks_of_state st = irq_masks_of_state t \<longrightarrow> scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> irq_masks_of_state s = irq_masks_of_state t)) s \<and> ?P''4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. irq_masks_of_state st = irq_masks_of_state s \<Longrightarrow> ((\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and K (\<forall>s t. irq_masks_of_state st = irq_masks_of_state s \<longrightarrow> irq_masks_of_state st = irq_masks_of_state t \<longrightarrow> scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> irq_masks_of_state s = irq_masks_of_state t)) s \<and> True \<and> (\<forall>s t. scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> irq_oracle (irq_state_of_state s) = irq_oracle (irq_state_of_state t)) \<and> (irq_masks_of_state s (irq_oracle (irq_state_of_state (machine_state_update (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>) s))) \<or> irq_oracle (irq_state_of_state (machine_state_update (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>) s)) = 0x3FF \<or> in_kernel \<and> irq_oracle (irq_state_of_state (machine_state_update (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>) s)) \<in> non_kernel_IRQs \<longrightarrow> True) \<and> (\<not> (irq_masks_of_state s (irq_oracle (irq_state_of_state (machine_state_update (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>) s))) \<or> irq_oracle (irq_state_of_state (machine_state_update (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>) s)) = 0x3FF \<or> in_kernel \<and> irq_oracle (irq_state_of_state (machine_state_update (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>) s)) \<in> non_kernel_IRQs) \<longrightarrow> True) proof (prove)
goal (1 subgoal):
 1. \<And>s sa t. \<lbrakk>irq_masks_of_state st = irq_masks_of_state s; scheduler_equiv aag sa t; scheduler_affects_equiv aag l sa t\<rbrakk> \<Longrightarrow> irq_oracle (irq_state_of_state sa) = irq_oracle (irq_state_of_state t) proof (prove)
goal:
No subgoals!