theory Finalise_AC

lemma tcb_sched_action_enqueue_integrity[wp]:
  "tcb_sched_action tcb_sched_enqueue thread \<lbrace>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 tcb_at_def get_etcb_def
                        tcb_sched_enqueue_def etcb_at_def
             split: option.splits) apply (metis append.simps(2)) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st\<rbrace> tcb_sched_action tcb_sched_enqueue thread \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st\<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_enqueue thread queue)
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. integrity aag X st 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_enqueue 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> pasMayEditReadyQueues aag \<or> (\<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; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> (thread \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2)) \<longrightarrow> (\<forall>d. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> pasMayEditReadyQueues aag \<or> (\<forall>p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> (\<exists>threads. threads @ ready_queues st (tcb_domain x2) (tcb_priority x2) = thread # ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> (\<exists>threads. threads @ ready_queues st d p = ready_queues s d p))))) \<and> (thread \<in> set (ready_queues s (tcb_domain x2) (tcb_priority x2)) \<longrightarrow> (\<forall>d. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> pasMayEditReadyQueues aag \<or> (\<forall>p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> (\<exists>threads. threads @ ready_queues st (tcb_domain x2) (tcb_priority x2) = ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> (\<exists>threads. threads @ ready_queues st d p = ready_queues s d p))))) proof (prove)
goal:
No subgoals!