kings-crown/FVELER_Isabelle huggingface dataset:
theory Syscall_AC

lemma dec_domain_time_pas_refined[wp]:
  "dec_domain_time \<lbrace>pas_refined aag\<rbrace>" apply (simp add: dec_domain_time_def | wp)+ apply (clarsimp simp: pas_refined_def tcb_domain_map_wellformed_aux_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag\<rbrace> dec_domain_time \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pas_refined aag s \<Longrightarrow> pas_refined aag (domain_time_update (\<lambda>_. domain_time s - 1) s) proof (prove)
goal:
No subgoals!
theory Syscall_AC

lemma handle_interrupt_pas_refined:
  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace>
    handle_interrupt irq \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (simp add: handle_interrupt_def) apply (rule conjI; rule impI;rule hoare_pre) apply (wp send_signal_pas_refined get_cap_wp
         | wpc
         | simp add: get_irq_slot_def get_irq_state_def )+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace> handle_interrupt irq \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. (maxIRQ < irq \<longrightarrow> \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace> do_machine_op (do y <- maskInterrupt True irq;
ackInterrupt irq
od) \<lbrace>\<lambda>_. pas_refined aag\<rbrace>) \<and> (\<not> maxIRQ < irq \<longrightarrow> \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace> do st <- get_irq_state irq;
y <- case st of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do slot <- get_irq_slot irq;
cap <- get_cap slot;
when (is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap) $ send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal irq
od | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq irq;
do_machine_op (ackInterrupt irq)
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace>) proof (prove)
goal (4 subgoals):
 1. maxIRQ < irq \<Longrightarrow> \<lbrace>?Q27\<rbrace> do_machine_op (do y <- maskInterrupt True irq;
ackInterrupt irq
od) \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>s. \<lbrakk>maxIRQ < irq; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state) s\<rbrakk> \<Longrightarrow> ?Q27 s
 3. \<not> maxIRQ < irq \<Longrightarrow> \<lbrace>?Q22\<rbrace> do st <- get_irq_state irq;
y <- case st of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do slot <- get_irq_slot irq;
cap <- get_cap slot;
when (is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap) $ send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal irq
od | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq irq;
do_machine_op (ackInterrupt irq)
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 4. \<And>s. \<lbrakk>\<not> maxIRQ < irq; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state) s\<rbrakk> \<Longrightarrow> ?Q22 s proof (prove)
goal:
No subgoals!
theory Syscall_AC

lemma dec_domain_time_integrity[wp]:
  "dec_domain_time \<lbrace>integrity aag X st\<rbrace>" apply (simp add: dec_domain_time_def | wp)+ apply (clarsimp simp: integrity_subjects_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st\<rbrace> dec_domain_time \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. integrity aag X st s \<Longrightarrow> integrity aag X st (domain_time_update (\<lambda>_. domain_time s - 1) s) proof (prove)
goal:
No subgoals!
theory Syscall_AC

lemma timer_tick_integrity[wp]:
  "\<lbrace>integrity aag X st and pas_refined aag and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s))\<rbrace>
   timer_tick
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: timer_tick_def) apply (wp ethread_set_integrity_autarch gts_wp
         | wpc | simp add: thread_set_time_slice_def split del: if_split)+ apply (clarsimp simp: ct_in_state_def st_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s))\<rbrace> timer_tick \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s))\<rbrace> do cur <- gets cur_thread;
state <- get_thread_state cur;
y <- case state of Running \<Rightarrow> do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then thread_set_time_slice cur ts' else do thread_set_time_slice cur timeSlice;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od | _ \<Rightarrow> return ();
when (Suc 0 < numDomains) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. integrity aag X st s \<and> pas_refined aag s \<and> (ct_active s \<longrightarrow> is_subject aag (cur_thread s)) \<Longrightarrow> st_tcb_at ((=) Running) (cur_thread s) s \<longrightarrow> etcb_at (\<lambda>t. is_subject aag (cur_thread s)) (cur_thread s) s proof (prove)
goal:
No subgoals!
theory Syscall_AC

lemma handle_yield_pas_refined[wp]:
  "handle_yield \<lbrace>pas_refined aag\<rbrace>" by (simp add: handle_yield_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag\<rbrace> handle_yield \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
theory Syscall_AC

lemma valid_fault_Unknown[simp]:
  "valid_fault (UnknownSyscallException x)" by (simp add: valid_fault_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_fault (UnknownSyscallException x)
theory Syscall_AC

lemma valid_fault_User[simp]:
  "valid_fault (UserException word1 word2)" by (simp add: valid_fault_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_fault (UserException word1 word2)
theory Syscall_AC

lemma ct_in_state_machine_state_update[simp]:
  "ct_in_state s (st\<lparr>machine_state := x\<rparr>) = ct_in_state s st" by (simp add: ct_in_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ct_in_state s (st\<lparr>machine_state := x\<rparr>) = ct_in_state s st
theory Syscall_AC

lemma activate_thread_respects:
  "\<lbrace>integrity aag X st and K (pasMayActivate aag)\<rbrace>
   activate_thread
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: activate_thread_def get_thread_state_def) apply (wpsimp wp: set_thread_state_restart_to_running_respects thread_get_wp') apply (clarsimp simp: st_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and K (pasMayActivate aag)\<rbrace> activate_thread \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and (\<lambda>y. pasMayActivate aag)\<rbrace> do thread <- gets cur_thread;
state <- thread_get tcb_state thread;
case state of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user thread getRestartPC;
as_user thread $ setNextPC pc;
set_thread_state thread Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread thread | _ \<Rightarrow> fail
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. \<lbrakk>integrity_subjects {pasSubject aag} aag True X st s; pasMayActivate aag; ko_at (TCB tcb) (cur_thread s) s; tcb_state tcb = Restart\<rbrakk> \<Longrightarrow> st_tcb_at ((=) Restart) (cur_thread s) s proof (prove)
goal:
No subgoals!
theory Syscall_AC

lemma activate_thread_integrity:
  "\<lbrace>integrity aag X st and valid_idle and
    (\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s))\<rbrace>
   activate_thread
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: activate_thread_def ) apply (rule hoare_pre) apply (wpsimp wp: gts_wp set_thread_state_integrity_autarch as_user_integrity_autarch)+ apply (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and valid_idle and (\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s))\<rbrace> activate_thread \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and valid_idle and (\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s))\<rbrace> do thread <- gets cur_thread;
state <- get_thread_state thread;
case state of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user thread getRestartPC;
as_user thread $ setNextPC pc;
set_thread_state thread Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread thread | _ \<Rightarrow> fail
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do thread <- gets cur_thread;
state <- get_thread_state thread;
case state of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user thread getRestartPC;
as_user thread $ setNextPC pc;
set_thread_state thread Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread thread | _ \<Rightarrow> fail
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>s. (integrity aag X st and valid_idle and (\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s))) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>integrity aag X st s; valid_idle s; st_tcb_at ((=) Restart) (idle_thread s) s; pasObjectAbs aag (idle_thread s) \<noteq> pasSubject aag; cur_thread s = idle_thread s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Syscall_AC

lemma activate_thread_pas_refined:
  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace>
   activate_thread
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" unfolding activate_thread_def get_thread_state_def thread_get_def apply (wpsimp wp: set_thread_state_pas_refined hoare_drop_imps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace> activate_thread \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace> do thread <- gets cur_thread;
state <- do tcb <- gets_the $ get_tcb thread;
return $ tcb_state tcb
od;
case state of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user thread getRestartPC;
as_user thread $ setNextPC pc;
set_thread_state thread Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread thread | _ \<Rightarrow> fail
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_AC

lemma integrity_cur_thread[iff]:
  "integrity aag X st (s\<lparr>cur_thread := v\<rparr>) = integrity aag X st s" unfolding integrity_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. integrity aag X st (s\<lparr>cur_thread := v\<rparr>) = integrity aag X st s proof (prove)
goal (1 subgoal):
 1. (integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} st (s\<lparr>cur_thread := v\<rparr>) \<and> (\<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap (s\<lparr>cur_thread := v\<rparr>) x)) \<and> integrity_cdt_state aag {pasSubject aag} st (s\<lparr>cur_thread := v\<rparr>) \<and> (\<forall>x. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) x (cdt_list st x) (cdt_list (s\<lparr>cur_thread := v\<rparr>) x)) \<and> (\<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node (s\<lparr>cur_thread := v\<rparr>) x, interrupt_states (s\<lparr>cur_thread := v\<rparr>) x)) \<and> (\<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues (s\<lparr>cur_thread := v\<rparr>) d p)) \<and> (\<forall>x. memory_integrity X aag x (tcb_states_of_state st) (tcb_states_of_state (s\<lparr>cur_thread := v\<rparr>)) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state (s\<lparr>cur_thread := v\<rparr>)) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (tcb_states_of_state (s\<lparr>cur_thread := v\<rparr>)) (device_state (machine_state st) x) (device_state (machine_state (s\<lparr>cur_thread := v\<rparr>)) x)) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>cur_thread := v\<rparr>))) = (integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} st s \<and> (\<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x)) \<and> integrity_cdt_state aag {pasSubject aag} st s \<and> (\<forall>x. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) x (cdt_list st x) (cdt_list s x)) \<and> (\<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)) \<and> (\<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p)) \<and> (\<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)) \<and> (\<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)) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a st s))
theory Syscall_AC

lemma tcb_sched_action_dequeue_integrity_pasMayEditReadyQueues:
  "\<lbrace>integrity aag X st and pas_refined aag and K (pasMayEditReadyQueues aag)\<rbrace>
   tcb_sched_action tcb_sched_dequeue 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) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and K (pasMayEditReadyQueues aag)\<rbrace> tcb_sched_action tcb_sched_dequeue 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. pasMayEditReadyQueues aag)\<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_dequeue 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. pasMayEditReadyQueues aag)) 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_dequeue thread (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s t' p) s)) thread s) thread s proof (prove)
goal:
No subgoals!
theory Syscall_AC

lemma switch_to_thread_respects_pasMayEditReadyQueues:
  "\<lbrace>integrity aag X st and pas_refined aag and K (pasMayEditReadyQueues aag)\<rbrace>
   switch_to_thread t
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" unfolding switch_to_thread_def apply (simp add: spec_valid_def) apply (wpsimp wp: tcb_sched_action_dequeue_integrity_pasMayEditReadyQueues) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and K (pasMayEditReadyQueues aag)\<rbrace> switch_to_thread t \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and K (pasMayEditReadyQueues aag)\<rbrace> do state <- get;
assert (get_tcb t state \<noteq> None);
arch_switch_to_thread t;
do_extended_op (tcb_sched_action tcb_sched_dequeue t);
modify (cur_thread_update (\<lambda>_. t))
od \<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. pasMayEditReadyQueues aag)\<rbrace> do state <- get;
y <- assert (\<exists>y. get_tcb t state = Some y);
y <- arch_switch_to_thread t;
y <- tcb_sched_action tcb_sched_dequeue t;
modify (cur_thread_update (\<lambda>_. t))
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_AC

lemma switch_to_thread_respects:
  "\<lbrace>integrity aag X st and pas_refined aag and K (is_subject aag t) \<rbrace>
   switch_to_thread t
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" unfolding switch_to_thread_def apply (simp add: spec_valid_def) apply wpsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and K (is_subject aag t)\<rbrace> switch_to_thread t \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and K (is_subject aag t)\<rbrace> do state <- get;
assert (get_tcb t state \<noteq> None);
arch_switch_to_thread t;
do_extended_op (tcb_sched_action tcb_sched_dequeue t);
modify (cur_thread_update (\<lambda>_. t))
od \<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 t)\<rbrace> do state <- get;
y <- assert (\<exists>y. get_tcb t state = Some y);
y <- arch_switch_to_thread t;
y <- tcb_sched_action tcb_sched_dequeue t;
modify (cur_thread_update (\<lambda>_. t))
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_AC

lemma switch_to_thread_respects':
  "\<lbrace>integrity aag X st and pas_refined aag
                       and (\<lambda>s. pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s t))))\<rbrace>
   switch_to_thread t
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" unfolding switch_to_thread_def apply (simp add: spec_valid_def) apply (wpsimp wp: tcb_sched_action_dequeue_integrity') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and (\<lambda>s. pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s t))))\<rbrace> switch_to_thread t \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and (\<lambda>s. pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s t))))\<rbrace> do state <- get;
assert (get_tcb t state \<noteq> None);
arch_switch_to_thread t;
do_extended_op (tcb_sched_action tcb_sched_dequeue t);
modify (cur_thread_update (\<lambda>_. t))
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and (\<lambda>s. pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s t))))\<rbrace> do state <- get;
y <- assert (\<exists>y. get_tcb t state = Some y);
y <- arch_switch_to_thread t;
y <- tcb_sched_action tcb_sched_dequeue t;
modify (cur_thread_update (\<lambda>_. t))
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_AC

lemma switch_to_idle_thread_respects:
  "switch_to_idle_thread \<lbrace>integrity aag X st\<rbrace>" unfolding switch_to_idle_thread_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st\<rbrace> do thread <- gets idle_thread;
arch_switch_to_idle_thread;
modify (cur_thread_update (\<lambda>_. thread))
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
theory Syscall_AC

lemma choose_thread_respects_pasMayEditReadyQueues:
  "\<lbrace>integrity aag X st and pas_refined aag and einvs and valid_queues
                       and K (pasMayEditReadyQueues aag)\<rbrace>
   choose_thread
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" by (simp add: choose_thread_def guarded_switch_to_def
      | wp switch_to_thread_respects_pasMayEditReadyQueues switch_to_idle_thread_respects gts_wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and einvs and valid_queues and K (pasMayEditReadyQueues aag)\<rbrace> choose_thread \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
theory Syscall_AC

lemma next_domain_tcb_domain_map_wellformed[wp]:
  "next_domain \<lbrace>tcb_domain_map_wellformed aag\<rbrace>" by (wpsimp simp: next_domain_def thread_set_domain_def ethread_set_def set_eobject_def Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_domain_map_wellformed aag\<rbrace> next_domain \<lbrace>\<lambda>_. tcb_domain_map_wellformed aag\<rbrace>
theory Syscall_AC

lemma valid_blocked_2_valid_blocked_except[simp]:
  "valid_blocked_2 queues kh sa ct \<Longrightarrow> valid_blocked_except_2 t queues kh sa ct" by (clarsimp simp: valid_blocked_def valid_blocked_except_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_blocked_2 queues kh sa ct \<Longrightarrow> valid_blocked_except_2 t queues kh sa ct
theory Syscall_AC

lemma next_domain_integrity[wp]:
  "next_domain \<lbrace>integrity aag X st\<rbrace>" apply (wpsimp simp: next_domain_def thread_set_domain_def ethread_set_def set_eobject_def Let_def) apply (clarsimp simp: get_etcb_def integrity_subjects_def lfp_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st\<rbrace> next_domain \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. integrity aag X st s \<Longrightarrow> integrity aag X st (trans_state (\<lambda>e. e\<lparr>domain_index_internal := Suc (domain_index s) mod length (domain_list s), cur_domain_internal := fst (domain_list s ! (Suc (domain_index s) mod length (domain_list s))), domain_time_internal := snd (domain_list s ! (Suc (domain_index s) mod length (domain_list s))), work_units_completed_internal := 0\<rparr>) s) proof (prove)
goal:
No subgoals!
theory Syscall_AC

lemma pas_refined_cur_thread[iff]:
  "pas_refined aag (s\<lparr>cur_thread := v\<rparr>) = pas_refined aag s" unfolding pas_refined_def by (simp add: state_objs_to_policy_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pas_refined aag (s\<lparr>cur_thread := v\<rparr>) = pas_refined aag s proof (prove)
goal (1 subgoal):
 1. (pas_wellformed aag \<and> irq_map_wellformed aag (s\<lparr>cur_thread := v\<rparr>) \<and> tcb_domain_map_wellformed aag (s\<lparr>cur_thread := v\<rparr>) \<and> state_objs_in_policy aag (s\<lparr>cur_thread := v\<rparr>) \<and> state_asids_to_policy aag (s\<lparr>cur_thread := v\<rparr>) \<subseteq> pasPolicy aag \<and> state_irqs_to_policy aag (s\<lparr>cur_thread := v\<rparr>) \<subseteq> pasPolicy aag) = (pas_wellformed aag \<and> irq_map_wellformed aag s \<and> tcb_domain_map_wellformed aag s \<and> state_objs_in_policy aag s \<and> state_asids_to_policy aag s \<subseteq> pasPolicy aag \<and> state_irqs_to_policy aag s \<subseteq> pasPolicy aag)