kings-crown/FVELER_Isabelle huggingface dataset:
theory Syscall_AC

lemma switch_to_idle_thread_pas_refined:
  "switch_to_idle_thread \<lbrace>pas_refined aag\<rbrace>" unfolding switch_to_idle_thread_def by (wpsimp wp: do_machine_op_pas_refined)

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

lemma schedule_choose_new_thread_integrity:
  "\<lbrace>invs and valid_sched and valid_list and integrity aag X st and pas_refined aag
         and K (pasMayEditReadyQueues aag)
         and (\<lambda>s. scheduler_action s = choose_new_thread)\<rbrace>
   schedule_choose_new_thread
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" unfolding schedule_choose_new_thread_def by (wpsimp wp: choose_thread_respects_pasMayEditReadyQueues
                 next_domain_valid_sched next_domain_valid_queues
           simp: schedule_choose_new_thread_def valid_sched_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_sched and valid_list and integrity aag X st and pas_refined aag and K (pasMayEditReadyQueues aag) and (\<lambda>s. scheduler_action s = choose_new_thread)\<rbrace> schedule_choose_new_thread \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_sched and valid_list and integrity aag X st and pas_refined aag and K (pasMayEditReadyQueues aag) and (\<lambda>s. scheduler_action s = choose_new_thread)\<rbrace> do dom_time <- gets domain_time;
when (dom_time = 0) next_domain;
choose_thread;
set_scheduler_action resume_cur_thread
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
theory Syscall_AC

lemma  valid_sched_valid_sched_action:
  "valid_sched s \<Longrightarrow> valid_sched_action s" by (simp add: valid_sched_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_sched s \<Longrightarrow> valid_sched_action s
theory Syscall_AC

lemma zet_zip_contrapos:
  "fst t \<notin> set xs  \<Longrightarrow> t \<notin> set (zip xs ys)" by (auto simp: set_zip_helper)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fst t \<notin> set xs \<Longrightarrow> t \<notin> set (zip xs ys)
theory Syscall_AC

lemma ct_active_update[simp]:
  "ct_active (s\<lparr>cdt := b\<rparr>) = ct_active s"
  "ct_active (s\<lparr>is_original_cap := ic\<rparr>) = ct_active s"
  "ct_active (s\<lparr>interrupt_states := st\<rparr>) = ct_active s"
  "ct_active (s\<lparr>arch_state := as\<rparr>) = ct_active s" by (auto simp: st_tcb_at_def ct_in_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (ct_active (s\<lparr>cdt := b\<rparr>) = ct_active s &&& ct_active (s\<lparr>is_original_cap := ic\<rparr>) = ct_active s) &&& ct_active (s\<lparr>interrupt_states := st\<rparr>) = ct_active s &&& ct_active (s\<lparr>arch_state := as\<rparr>) = ct_active s
theory Syscall_AC

lemma set_cap_ct_active[wp]:
  "set_cap ptr c \<lbrace>ct_active \<rbrace>" apply (rule hoare_pre) apply (wps | wpsimp wp: sts_st_tcb_at_cases thread_set_no_change_tcb_state
                    simp: crunch_simps ct_in_state_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_active\<rbrace> set_cap ptr c \<lbrace>\<lambda>_. ct_active\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> set_cap ptr c \<lbrace>\<lambda>_. ct_active\<rbrace>
 2. \<And>s. ct_active s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Syscall_AC

lemma do_extended_op_ct_active[wp]:
  "do_extended_op ch \<lbrace>ct_active \<rbrace>" apply (rule hoare_pre) apply (wp | simp add: crunch_simps ct_in_state_def do_extended_op_def | wps)+ apply (auto simp: st_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_active\<rbrace> do_extended_op ch \<lbrace>\<lambda>_. ct_active\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do_extended_op ch \<lbrace>\<lambda>_. ct_active\<rbrace>
 2. \<And>s. ct_active s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. st_tcb_at active (cur_thread s) s \<Longrightarrow> \<forall>x\<in>fst (mk_ef (wrap_ext_op ch s)). st_tcb_at active (cur_thread s) (s\<lparr>exst := exst (snd x)\<rparr>) proof (prove)
goal:
No subgoals!
theory Syscall_AC

lemma cap_swap_ct_active[wp]:
  "cap_swap a b c d \<lbrace>ct_active\<rbrace>" by (wp | simp add: cap_swap_def | wps)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_active\<rbrace> cap_swap a b c d \<lbrace>\<lambda>_. ct_active\<rbrace>
theory Syscall_AC

lemma unbind_maybe_notification_ct_active[wp]:
  "unbind_maybe_notification ptr \<lbrace>ct_active\<rbrace>" by (wps | wpsimp simp: unbind_maybe_notification_def ct_in_state_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_active\<rbrace> unbind_maybe_notification ptr \<lbrace>\<lambda>_. ct_active\<rbrace>
theory Syscall_AC

lemma unbind_notification_ct_active[wp]:
  "unbind_notification ptr \<lbrace>ct_active\<rbrace>" by (wps | wpsimp simp: unbind_notification_def ct_in_state_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_active\<rbrace> unbind_notification ptr \<lbrace>\<lambda>_. ct_active\<rbrace>
theory Syscall_AC

lemma sts_Restart_ct_active[wp]:
  "set_thread_state xa Restart \<lbrace>ct_active\<rbrace>" apply (wp set_object_wp | simp add: set_thread_state_def)+ 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>ct_active\<rbrace> set_thread_state xa Restart \<lbrace>\<lambda>_. ct_active\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ct_active s \<Longrightarrow> (\<exists>y. get_tcb xa s = Some y) \<longrightarrow> ct_active (s\<lparr>kheap := (kheap s)(xa \<mapsto> TCB (the (get_tcb xa s)\<lparr>tcb_state := Restart\<rparr>))\<rparr>) proof (prove)
goal:
No subgoals!
theory Syscall_AC

lemma rec_del_cur_thread[wp]:
  "rec_del a \<lbrace>\<lambda>s :: det_ext state. P (cur_thread s)\<rbrace>" apply (rule rec_del_preservation) apply (wp preemption_point_inv|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> rec_del a \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s sl1 sl2. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> cap_swap_for_delete sl1 sl2 \<lbrace>\<lambda>rv s. P (cur_thread s)\<rbrace>
 2. \<And>s sl cap. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> set_cap sl cap \<lbrace>\<lambda>rv s. P (cur_thread s)\<rbrace>
 3. \<And>s sl opt. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> empty_slot sl opt \<lbrace>\<lambda>rv s. P (cur_thread s)\<rbrace>
 4. \<And>s cap fin. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> finalise_cap cap fin \<lbrace>\<lambda>rv s. P (cur_thread s)\<rbrace>
 5. \<And>s. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> preemption_point \<lbrace>\<lambda>rv s. P (cur_thread s)\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_AC

lemma cap_revoke_cur_thread[wp]:
  "cap_revoke a \<lbrace>\<lambda>s :: det_ext state. P (cur_thread s)\<rbrace>" apply (rule cap_revoke_preservation2) apply (wp preemption_point_inv|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> cap_revoke a \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s p. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> cap_delete p \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace>
 2. \<And>s. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> preemption_point \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_AC

lemma invoke_cnode_cur_thread[wp]:
 "invoke_cnode a \<lbrace>\<lambda>s :: det_ext state. P (cur_thread s)\<rbrace>" apply (simp add: invoke_cnode_def) apply (rule hoare_pre) apply (wp hoare_drop_imps hoare_vcg_all_lift | wpc | simp split del: if_split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> invoke_cnode a \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> case a of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case a of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace>
 2. \<And>s. P (cur_thread s) \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Syscall_AC

lemma dxo_idle_thread[wp]:
  "\<lbrace>\<lambda>s. P (idle_thread s) \<rbrace> do_extended_op f \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace>" by (clarsimp simp: valid_def dest!: in_dxo_idle_threadD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> do_extended_op f \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace>
theory Syscall_AC

lemma preemption_point_idle_thread[wp]:
  "preemption_point \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace>" by (wpsimp wp: OR_choiceE_weak_wp simp: preemption_point_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> preemption_point \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace>
theory Syscall_AC

lemma invoke_cnode_idle_thread[wp]:
  "invoke_cnode a \<lbrace>\<lambda>s :: det_ext state. P (idle_thread s)\<rbrace>" apply (simp add: invoke_cnode_def) apply (rule hoare_pre) apply (wp hoare_drop_imps hoare_vcg_all_lift | wpc | simp split del: if_split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> invoke_cnode a \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> case a of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case a of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace>
 2. \<And>s. P (idle_thread s) \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Syscall_AC

lemma invoke_cnode_cur_domain[wp]:
 "invoke_cnode a \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace>" apply (simp add: invoke_cnode_def) apply (rule hoare_pre) apply (wp hoare_drop_imps hoare_vcg_all_lift | wpc | simp split del: if_split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> invoke_cnode a \<lbrace>\<lambda>_ s. P (cur_domain s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> case a of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (cur_domain s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case a of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (cur_domain s)\<rbrace>
 2. \<And>s. P (cur_domain s) \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Syscall_AC

lemma handle_event_guarded_pas_domain[wp]:
  "handle_event e \<lbrace>guarded_pas_domain aag\<rbrace>" by (wpsimp wp: guarded_pas_domain_lift)

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

lemma handle_interrupt_guarded_pas_domain[wp]:
  "handle_interrupt blah \<lbrace>guarded_pas_domain aag\<rbrace>" by (wpsimp wp: guarded_pas_domain_lift)

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

lemma integrity_irq_state_independent[simp]:
  "integrity_subjects subjects aag activate X st (s\<lparr>machine_state := irq_state_update f ms\<rparr>) =
   integrity_subjects subjects aag activate X st (s\<lparr>machine_state := ms\<rparr>)" by (clarsimp simp: integrity_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. integrity_subjects subjects aag activate X st (s\<lparr>machine_state := irq_state_update f ms\<rparr>) = integrity_subjects subjects aag activate X st (s\<lparr>machine_state := ms\<rparr>)
theory Syscall_AC

lemma guarded_pas_domain_machine_state_update[simp]:
  "guarded_pas_domain aag (machine_state_update f s) = guarded_pas_domain aag s" by (simp add: guarded_pas_domain_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. guarded_pas_domain aag (machine_state_update f s) = guarded_pas_domain aag s
theory ArchSyscall_AC

lemma invs_irq_state_update[Syscall_AC_assms, simp]:
  "invs (s\<lparr>machine_state := irq_state_update f sa\<rparr>) = invs (s\<lparr>machine_state := sa\<rparr>)" apply (rule iffI) apply (subst invs_irq_state_independent[symmetric]) apply (subst ARM.fold_congs(2); fastforce) apply (subst (asm) invs_irq_state_independent[symmetric]) apply (subst ARM.fold_congs(2); fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs (s\<lparr>machine_state := irq_state_update f sa\<rparr>) = invs (s\<lparr>machine_state := sa\<rparr>) proof (prove)
goal (2 subgoals):
 1. invs (s\<lparr>machine_state := irq_state_update f sa\<rparr>) \<Longrightarrow> invs (s\<lparr>machine_state := sa\<rparr>)
 2. invs (s\<lparr>machine_state := sa\<rparr>) \<Longrightarrow> invs (s\<lparr>machine_state := irq_state_update f sa\<rparr>) proof (prove)
goal (2 subgoals):
 1. invs (s\<lparr>machine_state := irq_state_update f sa\<rparr>) \<Longrightarrow> invs (s\<lparr>machine_state := sa, machine_state := machine_state (s\<lparr>machine_state := sa\<rparr>)\<lparr>irq_state := ?f4 (irq_state (machine_state (s\<lparr>machine_state := sa\<rparr>)))\<rparr>\<rparr>)
 2. invs (s\<lparr>machine_state := sa\<rparr>) \<Longrightarrow> invs (s\<lparr>machine_state := irq_state_update f sa\<rparr>) proof (prove)
goal (1 subgoal):
 1. invs (s\<lparr>machine_state := sa\<rparr>) \<Longrightarrow> invs (s\<lparr>machine_state := irq_state_update f sa\<rparr>) proof (prove)
goal (1 subgoal):
 1. invs (s\<lparr>machine_state := sa, machine_state := machine_state (s\<lparr>machine_state := sa\<rparr>)\<lparr>irq_state := ?f23 (irq_state (machine_state (s\<lparr>machine_state := sa\<rparr>)))\<rparr>\<rparr>) \<Longrightarrow> invs (s\<lparr>machine_state := irq_state_update f sa\<rparr>) proof (prove)
goal:
No subgoals!
theory ArchSyscall_AC

lemma cap_move_cur_thread[Syscall_AC_assms, wp]:
  "cap_move new_cap src_slot dest_slot \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace>" unfolding cap_move_def by (wpsimp wp: dxo_wp_weak)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> cap_move new_cap src_slot dest_slot \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> do set_cap new_cap dest_slot;
set_cap NullCap src_slot;
src_p <- gets (\<lambda>s. cdt s src_slot);
dest_p <- gets (\<lambda>s. cdt s dest_slot);
cdt <- gets cdt;
parent <- return $ cdt src_slot;
cdt' <- return $ cdt(dest_slot := parent, src_slot := None);
set_cdt (\<lambda>r. if cdt' r = Some src_slot then Some dest_slot else cdt' r);
do_extended_op (cap_move_ext src_slot dest_slot src_p dest_p);
is_original <- gets is_original_cap;
set_original dest_slot (is_original src_slot);
set_original src_slot False
od \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace>
theory ArchSyscall_AC

lemma cancel_badged_sends_cur_thread[Syscall_AC_assms, wp]:
  "cancel_badged_sends epptr badge \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace>" unfolding cancel_badged_sends_def by (wpsimp wp: dxo_wp_weak filterM_preserved crunch_wps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> cancel_badged_sends epptr badge \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> do ep <- get_endpoint epptr;
case ep of SendEP queue \<Rightarrow> do set_endpoint epptr IdleEP;
queue' <- swp filterM queue (\<lambda>t. do st <- get_thread_state t;
if blocking_ipc_badge st = badge then do set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t);
return False
od else return True
od);
ep' <- return (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue');
set_endpoint epptr ep';
do_extended_op reschedule_required
od | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace>
theory ArchSyscall_AC

lemma state_vrefs_cur_thread_update[Syscall_AC_assms, simp]:
  "state_vrefs (cur_thread_update f s) = state_vrefs s" by (simp add: state_vrefs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. state_vrefs (cur_thread_update f s) = state_vrefs s