theory Noninterference

lemma check_active_irq_if_partitionIntegrity:
  "check_active_irq_if tc \<lbrace>partitionIntegrity aag st\<rbrace>" apply (simp add: check_active_irq_if_def) apply (wp dmo_getActiveIRQ_wp) apply (simp add: partitionIntegrity_def integrity_subjects_def) apply (simp add: silc_dom_equiv_def equiv_for_def globals_equiv_scheduler_def) apply (fastforce simp: domain_fields_equiv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>partitionIntegrity aag st\<rbrace> check_active_irq_if tc \<lbrace>\<lambda>_. partitionIntegrity aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>partitionIntegrity aag st\<rbrace> do irq <- do_machine_op (getActiveIRQ False);
return (irq, tc)
od \<lbrace>\<lambda>_. partitionIntegrity aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. partitionIntegrity aag st s \<Longrightarrow> partitionIntegrity aag st (s\<lparr>machine_state := machine_state s\<lparr>irq_state := irq_state_of_state s + 1\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>x. integrity_obj (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {pasSubject aag} (pasObjectAbs aag x) (kheap st x) (kheap s x)) \<and> (\<forall>x. integrity_eobj (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x)) \<and> (\<forall>a b. integrity_cdt (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (cdt st) (tcb_states_of_state st) (a, b) (cdt st (a, b), is_original_cap st (a, b)) (cdt s (a, b), is_original_cap s (a, b))) \<and> (\<forall>a b. integrity_cdt_list (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (cdt st) (tcb_states_of_state st) (a, b) (cdt_list st (a, b)) (cdt_list s (a, b))) \<and> (\<forall>x. integrity_interrupts (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node s x, interrupt_states s x)) \<and> (\<forall>d p. integrity_ready_queues (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p)) \<and> (\<forall>x. integrity_mem (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} x (tcb_states_of_state st) (tcb_states_of_state s) (auth_ipc_buffers st) {} (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)) \<and> (\<forall>x. integrity_device (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} x (tcb_states_of_state st) (tcb_states_of_state s) (device_state (machine_state st) x) (device_state (machine_state s) x)) \<and> (\<forall>x a. integrity_asids (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} x a st s) \<and> domain_fields_equiv st s \<and> idle_thread st = idle_thread s \<and> globals_equiv_scheduler st s \<and> silc_dom_equiv aag st s \<Longrightarrow> domain_fields_equiv st (s\<lparr>machine_state := machine_state s\<lparr>irq_state := Suc (irq_state_of_state s)\<rparr>\<rparr>) \<and> globals_equiv_scheduler st (s\<lparr>machine_state := machine_state s\<lparr>irq_state := Suc (irq_state_of_state s)\<rparr>\<rparr>) \<and> silc_dom_equiv aag st (s\<lparr>machine_state := machine_state s\<lparr>irq_state := Suc (irq_state_of_state s)\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>x. integrity_obj (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {pasSubject aag} (pasObjectAbs aag x) (kheap st x) (kheap s x)) \<and> (\<forall>x. integrity_eobj (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x)) \<and> (\<forall>a b. integrity_cdt (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (cdt st) (tcb_states_of_state st) (a, b) (cdt st (a, b), is_original_cap st (a, b)) (cdt s (a, b), is_original_cap s (a, b))) \<and> (\<forall>a b. integrity_cdt_list (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (cdt st) (tcb_states_of_state st) (a, b) (cdt_list st (a, b)) (cdt_list s (a, b))) \<and> (\<forall>x. integrity_interrupts (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node s x, interrupt_states s x)) \<and> (\<forall>d p. integrity_ready_queues (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p)) \<and> (\<forall>x. integrity_mem (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} x (tcb_states_of_state st) (tcb_states_of_state s) (auth_ipc_buffers st) {} (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)) \<and> (\<forall>x. integrity_device (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} x (tcb_states_of_state st) (tcb_states_of_state s) (device_state (machine_state st) x) (device_state (machine_state s) x)) \<and> (\<forall>x a. integrity_asids (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} x a st s) \<and> domain_fields_equiv st s \<and> idle_thread st = idle_thread s \<and> arch_globals_equiv_scheduler (kheap st) (kheap s) (arch_state st) (arch_state s) \<and> idle_equiv st s \<and> dom (device_state (machine_state st)) = dom (device_state (machine_state s)) \<and> (\<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> kheap st x = kheap s x) \<Longrightarrow> domain_fields_equiv st (s\<lparr>machine_state := machine_state s\<lparr>irq_state := Suc (irq_state_of_state s)\<rparr>\<rparr>) proof (prove)
goal:
No subgoals!