theory Finalise_AC

lemma tcb_sched_action_append_integrity[wp]:
  "\<lbrace>integrity aag X st and pas_refined aag and K (is_subject aag thread)\<rbrace>
   tcb_sched_action tcb_sched_append thread
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: tcb_sched_action_def) apply wp apply (clarsimp simp: integrity_def integrity_ready_queues_def pas_refined_def
                        tcb_domain_map_wellformed_aux_def etcb_at_def get_etcb_def
                 split: option.splits) apply (erule_tac x="(thread, tcb_domain (the (ekheap s thread)))" in ballE) apply (auto intro: domtcbs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and K (is_subject aag thread)\<rbrace> tcb_sched_action tcb_sched_append thread \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and (\<lambda>y. is_subject aag thread)\<rbrace> do d <- ethread_get tcb_domain thread;
prio <- ethread_get tcb_priority thread;
queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_append thread queue)
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (integrity aag X st and pas_refined aag and (\<lambda>y. is_subject aag thread)) s \<Longrightarrow> etcb_at (\<lambda>t. etcb_at (\<lambda>ta. integrity aag X st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain t \<and> p = tcb_priority ta then tcb_sched_append thread (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s t' p) s)) thread s) thread s proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} st s; \<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x); \<forall>a b. cdt_integrity 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)); \<forall>a b. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt_list st (a, b)) (cdt_list s (a, b)); \<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node s x, interrupt_states s x); \<forall>d. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> (\<forall>p. \<exists>threads. threads @ ready_queues st d p = ready_queues s d p); \<forall>x. memory_integrity X 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); \<forall>x. integrity_device aag {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); \<forall>x a. integrity_asids aag {pasSubject aag} x a st s; pas_wellformed aag; irq_map_wellformed aag s; \<forall>x\<in>domains_of_state s. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; is_subject aag thread; ekheap s thread = Some x2; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain x2); \<not> pasMayEditReadyQueues aag\<rbrakk> \<Longrightarrow> \<exists>threads. threads @ ready_queues st (tcb_domain x2) (tcb_priority x2) = tcb_sched_append thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) proof (prove)
goal (2 subgoals):
 1. \<And>s x2. \<lbrakk>integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} st s; \<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x); \<forall>a b. cdt_integrity 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)); \<forall>a b. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt_list st (a, b)) (cdt_list s (a, b)); \<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node s x, interrupt_states s x); \<forall>d. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> (\<forall>p. \<exists>threads. threads @ ready_queues st d p = ready_queues s d p); \<forall>x. memory_integrity X 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); \<forall>x. integrity_device aag {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); \<forall>x a. integrity_asids aag {pasSubject aag} x a st s; pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; is_subject aag thread; ekheap s thread = Some x2; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain x2); \<not> pasMayEditReadyQueues aag; case (thread, tcb_domain (the (ekheap s thread))) of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d\<rbrakk> \<Longrightarrow> \<exists>threads. threads @ ready_queues st (tcb_domain x2) (tcb_priority x2) = tcb_sched_append thread (ready_queues s (tcb_domain x2) (tcb_priority x2))
 2. \<And>s x2. \<lbrakk>integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} st s; \<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x); \<forall>a b. cdt_integrity 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)); \<forall>a b. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt_list st (a, b)) (cdt_list s (a, b)); \<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node s x, interrupt_states s x); \<forall>d. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> (\<forall>p. \<exists>threads. threads @ ready_queues st d p = ready_queues s d p); \<forall>x. memory_integrity X 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); \<forall>x. integrity_device aag {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); \<forall>x a. integrity_asids aag {pasSubject aag} x a st s; pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; is_subject aag thread; ekheap s thread = Some x2; pasSubject aag \<notin> pasDomainAbs aag (tcb_domain x2); \<not> pasMayEditReadyQueues aag; (thread, tcb_domain (the (ekheap s thread))) \<notin> domains_of_state s\<rbrakk> \<Longrightarrow> \<exists>threads. threads @ ready_queues st (tcb_domain x2) (tcb_priority x2) = tcb_sched_append thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) proof (prove)
goal:
No subgoals!