kings-crown/FVELER_Isabelle huggingface dataset:
theory Syscall_IF

lemma equiv_valid_hoist_guard:
  assumes a: "Q \<Longrightarrow> equiv_valid_inv I A P f"
  assumes b: "\<And>s. P s \<Longrightarrow> Q"
  shows "equiv_valid_inv I A P f" using assms by (fastforce simp: equiv_valid_def2 equiv_valid_2_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A P f proof (prove)
using this:
Q \<Longrightarrow> equiv_valid_inv I A P f
P ?s \<Longrightarrow> Q

goal (1 subgoal):
 1. equiv_valid_inv I A P f
theory Syscall_IF

lemma as_user_reads_respects_g:
  "reads_respects_g aag k
     (valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s) and K (det f \<and> is_subject aag thread))
     (as_user thread f)" apply (rule equiv_valid_guard_imp) apply (rule reads_respects_g) apply (rule as_user_reads_respects) apply (rule doesnt_touch_globalsI) apply (wp as_user_globals_equiv) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag k) aag (valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s) and K (det f \<and> is_subject aag thread)) (as_user thread f) proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_g_inv (affects_equiv aag k) aag ?Q (as_user thread f)
 2. \<And>s. (valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s) and K (det f \<and> is_subject aag thread)) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. reads_respects aag k ?P3 (as_user thread f)
 2. doesnt_touch_globals ?Q3 (as_user thread f)
 3. \<And>s. (valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s) and K (det f \<and> is_subject aag thread)) s \<Longrightarrow> (?P3 and ?Q3) s proof (prove)
goal (2 subgoals):
 1. doesnt_touch_globals ?Q3 (as_user thread f)
 2. \<And>s. (valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s) and K (det f \<and> is_subject aag thread)) s \<Longrightarrow> (K (det f \<and> aag_can_read_or_affect aag k thread) and ?Q3) s proof (prove)
goal (2 subgoals):
 1. \<And>st. \<lbrace>globals_equiv st and ?Q3\<rbrace> as_user thread f \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>s. (valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s) and K (det f \<and> is_subject aag thread)) s \<Longrightarrow> (K (det f \<and> aag_can_read_or_affect aag k thread) and ?Q3) s proof (prove)
goal (2 subgoals):
 1. \<And>st s. (globals_equiv st and ?Q3) s \<Longrightarrow> (globals_equiv st and valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s)) s
 2. \<And>s. (valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s) and K (det f \<and> is_subject aag thread)) s \<Longrightarrow> (K (det f \<and> aag_can_read_or_affect aag k thread) and ?Q3) s proof (prove)
goal:
No subgoals!
theory Syscall_IF

lemma handle_interrupt_globals_equiv:
  "\<lbrace>globals_equiv (st :: det_state) and invs\<rbrace>
   handle_interrupt irq
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" unfolding handle_interrupt_def apply (rule hoare_if) apply (wp dmo_maskInterrupt_globals_equiv dmo_return_globals_equiv send_signal_globals_equiv
            hoare_vcg_if_lift2 hoare_drop_imps dxo_wp_weak no_fail_bind bind_known_operation_eq
         | wpc
         | simp add: dmo_bind_valid invs_imps invs_valid_idle)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and invs\<rbrace> handle_interrupt irq \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and invs\<rbrace> if maxIRQ < irq then do_machine_op $ do maskInterrupt True irq;
ackInterrupt irq
od else do st <- get_irq_state irq;
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>_. globals_equiv st\<rbrace> proof (prove)
goal (2 subgoals):
 1. maxIRQ < irq \<Longrightarrow> \<lbrace>globals_equiv st and invs\<rbrace> do_machine_op $ do maskInterrupt True irq;
ackInterrupt irq
od \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<not> maxIRQ < irq \<Longrightarrow> \<lbrace>globals_equiv st and invs\<rbrace> do st <- get_irq_state irq;
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>_. globals_equiv st\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_IF

lemma handle_vm_fault_reads_respects_g:
  "reads_respects_g aag l (K (is_subject aag t) and (valid_arch_state and (\<lambda>s. t \<noteq> idle_thread s)))
                    (handle_vm_fault t vmfault_type)" apply (rule reads_respects_g) apply (rule handle_vm_fault_reads_respects) apply (rule doesnt_touch_globalsI) apply (wp handle_vm_fault_globals_equiv) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (K (is_subject aag t) and (valid_arch_state and (\<lambda>s. t \<noteq> idle_thread s))) (handle_vm_fault t vmfault_type) proof (prove)
goal (2 subgoals):
 1. reads_respects aag l (K (is_subject aag t)) (handle_vm_fault t vmfault_type)
 2. doesnt_touch_globals (valid_arch_state and (\<lambda>s. t \<noteq> idle_thread s)) (handle_vm_fault t vmfault_type) proof (prove)
goal (1 subgoal):
 1. doesnt_touch_globals (valid_arch_state and (\<lambda>s. t \<noteq> idle_thread s)) (handle_vm_fault t vmfault_type) proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrace>globals_equiv st and (valid_arch_state and (\<lambda>s. t \<noteq> idle_thread s))\<rbrace> handle_vm_fault t vmfault_type \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>st s. (globals_equiv st and (valid_arch_state and (\<lambda>s. t \<noteq> idle_thread s))) s \<Longrightarrow> (globals_equiv st and valid_arch_state and (\<lambda>s. t \<noteq> idle_thread s)) s proof (prove)
goal:
No subgoals!
theory Syscall_IF

lemma handle_hypervisor_fault_reads_respects_g:
  "reads_respects_g aag l \<top> (handle_hypervisor_fault thread hyp)" apply (rule reads_respects_g[where P="\<top>" and Q="\<top>", simplified]) apply (rule handle_hypervisor_fault_reads_respects) apply (rule doesnt_touch_globalsI) apply (wp handle_hypervisor_fault_globals_equiv) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>_. True) (handle_hypervisor_fault thread hyp) proof (prove)
goal (2 subgoals):
 1. reads_respects aag l (\<lambda>_. True) (handle_hypervisor_fault thread hyp)
 2. doesnt_touch_globals (\<lambda>_. True) (handle_hypervisor_fault thread hyp) proof (prove)
goal (1 subgoal):
 1. doesnt_touch_globals (\<lambda>_. True) (handle_hypervisor_fault thread hyp) proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrace>globals_equiv st and (\<lambda>_. True)\<rbrace> handle_hypervisor_fault thread hyp \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>st s. (globals_equiv st and (\<lambda>_. True)) s \<Longrightarrow> globals_equiv st s proof (prove)
goal:
No subgoals!
theory Syscall_IF

lemma activate_thread_reads_respects:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "reads_respects aag (l :: 'a subject_label)
           (cur_tcb and (\<lambda>s. aag_can_read_label aag (pasObjectAbs aag (cur_thread s))))
           activate_thread" apply (simp add: activate_thread_def) apply (wpsimp wp: set_thread_state_runnable_reads_respects get_thread_state_rev) by (wp set_object_reads_respects get_thread_state_rev
      | simp add: as_user_def select_f_returns tcb_at_st_tcb_at[symmetric] cur_tcb_def
      | rule hoare_drop_imps conjI requiv_cur_thread_eq requiv_get_tcb_eq'
      | clarsimp simp: st_tcb_at_def obj_at_def is_tcb_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (cur_tcb and (\<lambda>s. aag_can_read aag (cur_thread s))) activate_thread proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (cur_tcb and (\<lambda>s. aag_can_read aag (cur_thread s))) (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) proof (prove)
goal (14 subgoals):
 1. \<And>rv rvb. reads_respects aag l (?P'42 rv (ds_id Restart) rvb) (as_user rv (setNextPC rvb))
 2. \<And>rv rva rvb. rva = Restart \<Longrightarrow> \<lbrace>?P''42 rv rva rvb\<rbrace> as_user rv $ setNextPC rvb \<lbrace>\<lambda>rvc _. True\<rbrace>
 3. \<And>rv rva. rva = Restart \<Longrightarrow> reads_respects aag l (?P'41 rv rva) (as_user rv getRestartPC)
 4. \<And>rv rva. rva = Restart \<Longrightarrow> \<lbrace>?P''41 rv rva\<rbrace> as_user rv getRestartPC \<lbrace>\<lambda>rvb s. ?P'42 rv rva rvb s \<and> ?P''42 rv rva rvb s\<rbrace>
 5. \<And>rv rva x41 x42. rva = BlockedOnReceive x41 x42 \<Longrightarrow> reads_respects aag l (?R22 rv rva x41 x42) fail
 6. \<And>rv rva x51 x52. rva = BlockedOnSend x51 x52 \<Longrightarrow> reads_respects aag l (?R19 rv rva x51 x52) fail
 7. \<And>rv rva. awaiting_reply rva \<Longrightarrow> reads_respects aag l (?R16 rv rva) fail
 8. \<And>rv rva x7. rva = BlockedOnNotification x7 \<Longrightarrow> reads_respects aag l (?R15 rv rva x7) fail
 9. \<And>rv rva. idle rva \<Longrightarrow> reads_respects aag l (?R13 rv rva) (arch_activate_idle_thread rv)
 10. \<And>rv. reads_respects aag l (?P'2 rv) (get_thread_state rv)
A total of 14 subgoals...
theory Syscall_IF

lemma activate_thread_globals_equiv:
  "\<lbrace>globals_equiv st and valid_arch_state and valid_idle\<rbrace>
   activate_thread
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" unfolding activate_thread_def by (wpsimp wp: set_thread_state_globals_equiv gts_wp
           simp: valid_idle_def pred_tcb_at_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state and valid_idle\<rbrace> activate_thread \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state and valid_idle\<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>_. globals_equiv st\<rbrace>
theory Syscall_IF

lemma activate_thread_reads_respects_g:
  assumes domains_distinct: "pas_domains_distinct aag"
  shows "reads_respects_g aag (l :: 'a subject_label)
           (invs and (\<lambda>s. aag_can_read_label aag (pasObjectAbs aag (cur_thread s))))
           activate_thread" apply (rule equiv_valid_guard_imp) apply (rule reads_respects_g) apply (rule activate_thread_reads_respects[OF domains_distinct]) apply (rule doesnt_touch_globalsI) apply (rule hoare_pre) apply (rule activate_thread_globals_equiv) apply (simp add: invs_imps invs_valid_idle)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (invs and (\<lambda>s. aag_can_read aag (cur_thread s))) activate_thread proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?Q activate_thread
 2. \<And>s. (invs and (\<lambda>s. aag_can_read aag (cur_thread s))) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. reads_respects aag l ?P3 activate_thread
 2. doesnt_touch_globals ?Q3 activate_thread
 3. \<And>s. (invs and (\<lambda>s. aag_can_read aag (cur_thread s))) s \<Longrightarrow> (?P3 and ?Q3) s proof (prove)
goal (2 subgoals):
 1. doesnt_touch_globals ?Q3 activate_thread
 2. \<And>s. (invs and (\<lambda>s. aag_can_read aag (cur_thread s))) s \<Longrightarrow> (cur_tcb and (\<lambda>s. aag_can_read aag (cur_thread s)) and ?Q3) s proof (prove)
goal (2 subgoals):
 1. \<And>st. \<lbrace>globals_equiv st and ?Q3\<rbrace> activate_thread \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>s. (invs and (\<lambda>s. aag_can_read aag (cur_thread s))) s \<Longrightarrow> (cur_tcb and (\<lambda>s. aag_can_read aag (cur_thread s)) and ?Q3) s proof (prove)
goal (3 subgoals):
 1. \<And>st. \<lbrace>?Q9 st\<rbrace> activate_thread \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>st s. (globals_equiv st and ?Q3) s \<Longrightarrow> ?Q9 st s
 3. \<And>s. (invs and (\<lambda>s. aag_can_read aag (cur_thread s))) s \<Longrightarrow> (cur_tcb and (\<lambda>s. aag_can_read aag (cur_thread s)) and ?Q3) s proof (prove)
goal (2 subgoals):
 1. \<And>st s. (globals_equiv st and ?Q3) s \<Longrightarrow> (globals_equiv st and valid_arch_state and valid_idle) s
 2. \<And>s. (invs and (\<lambda>s. aag_can_read aag (cur_thread s))) s \<Longrightarrow> (cur_tcb and (\<lambda>s. aag_can_read aag (cur_thread s)) and ?Q3) s proof (prove)
goal:
No subgoals!
theory Syscall_IF

lemma perform_invocation_globals_equiv:
  "\<lbrace>invs and ct_active and valid_invocation oper and globals_equiv (st :: det_state)
                                                 and authorised_for_globals_inv oper\<rbrace>
   perform_invocation blocking calling oper
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" by (cases oper
      ; wpsimp wp: invoke_untyped_globals_equiv send_ipc_globals_equiv send_signal_globals_equiv
                   arch_perform_invocation_globals_equiv do_reply_transfer_globals_equiv
                   invoke_tcb_globals_equiv invoke_irq_control_globals_equiv
                   invoke_cnode_globals_equiv invoke_irq_handler_globals_equiv
      ; fastforce simp: invs_imps authorised_for_globals_inv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and ct_active and valid_invocation oper and globals_equiv st and authorised_for_globals_inv oper\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
theory Syscall_IF

lemma handle_event_globals_equiv:
  "\<lbrace>invs and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and globals_equiv st\<rbrace>
   handle_event ev
   \<lbrace>\<lambda>_. globals_equiv (st :: det_state)\<rbrace>" apply (case_tac ev) by (wp hoare_weaken_pre[OF receive_ipc_globals_equiv, where P="globals_equiv st and invs"]
         hoare_weaken_pre[OF receive_signal_globals_equiv, where P="globals_equiv st and invs"]
         handle_invocation_globals_equiv handle_fault_globals_equiv' handle_recv_globals_equiv
         handle_reply_globals_equiv handle_interrupt_globals_equiv handle_vm_fault_globals_equiv
         handle_hypervisor_fault_globals_equiv
      | wpc
      | simp add: handle_send_def handle_call_def Let_def
      | wp (once) hoare_drop_imps
      | clarsimp simp: invs_imps invs_valid_idle ct_active_not_idle)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and globals_equiv st\<rbrace> handle_event ev \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x1. ev = SyscallEvent x1 \<Longrightarrow> \<lbrace>invs and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and globals_equiv st\<rbrace> handle_event ev \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>x2. ev = UnknownSyscall x2 \<Longrightarrow> \<lbrace>invs and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and globals_equiv st\<rbrace> handle_event ev \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 3. \<And>x31 x32. ev = UserLevelFault x31 x32 \<Longrightarrow> \<lbrace>invs and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and globals_equiv st\<rbrace> handle_event ev \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 4. ev = Interrupt \<Longrightarrow> \<lbrace>invs and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and globals_equiv st\<rbrace> handle_event ev \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 5. \<And>x5. ev = VMFaultEvent x5 \<Longrightarrow> \<lbrace>invs and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and globals_equiv st\<rbrace> handle_event ev \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 6. \<And>x6. ev = HypervisorEvent x6 \<Longrightarrow> \<lbrace>invs and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and globals_equiv st\<rbrace> handle_event ev \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
theory Syscall_IF

lemma ev_modify:
  "(\<And>s t. \<lbrakk>P s; P t; A s t; I s t\<rbrakk> \<Longrightarrow> I (f s) (f t) \<and> B (f s) (f t))
   \<Longrightarrow> equiv_valid I A B P (modify f)" by (clarsimp simp: equiv_valid_def2 equiv_valid_2_def simpler_modify_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s t. \<lbrakk>P s; P t; A s t; I s t\<rbrakk> \<Longrightarrow> I (f s) (f t) \<and> B (f s) (f t)) \<Longrightarrow> equiv_valid I A B P (modify f)
theory ArchSyscall_IF

lemma globals_equiv_irq_state_update[Syscall_IF_assms, simp]:
  "globals_equiv st (s\<lparr>machine_state :=
                       machine_state s \<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>) =
   globals_equiv st s" by (auto simp: globals_equiv_def idle_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. globals_equiv st (s\<lparr>machine_state := machine_state s\<lparr>irq_state := f (irq_state_of_state s)\<rparr>\<rparr>) = globals_equiv st s
theory ArchSyscall_IF

lemma thread_set_globals_equiv'[Syscall_IF_assms]:
  "\<lbrace>globals_equiv s and valid_arch_state and (\<lambda>s. tptr \<noteq> idle_thread s)\<rbrace>
   thread_set f tptr
   \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" unfolding thread_set_def apply (wp set_object_globals_equiv) apply simp apply (intro impI conjI allI) apply (fastforce simp: obj_at_def get_tcb_def valid_arch_state_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_arch_state and (\<lambda>s. tptr \<noteq> idle_thread s)\<rbrace> thread_set f tptr \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_arch_state and (\<lambda>s. tptr \<noteq> idle_thread s)\<rbrace> do tcb <- gets_the $ get_tcb tptr;
set_object tptr $ TCB $ f tcb
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. (globals_equiv s and valid_arch_state and (\<lambda>s. tptr \<noteq> idle_thread s)) sa \<Longrightarrow> get_tcb tptr sa \<noteq> None \<longrightarrow> (globals_equiv s and (\<lambda>s. tptr \<noteq> arm_global_pd (arch_state s)) and (\<lambda>t. tptr = idle_thread t \<longrightarrow> (\<forall>tcb. kheap t (idle_thread t) = Some (TCB tcb) \<longrightarrow> (\<exists>tcb'. (TCB $ f (the (get_tcb tptr sa))) = TCB tcb' \<and> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb'))) \<and> (\<forall>tcb'. (TCB $ f (the (get_tcb tptr sa))) = TCB tcb' \<longrightarrow> tcb_at (idle_thread t) t))) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa. globals_equiv s sa \<and> valid_arch_state sa \<and> tptr \<noteq> idle_thread sa \<Longrightarrow> (\<exists>y. get_tcb tptr sa = Some y) \<longrightarrow> tptr \<noteq> arm_global_pd (arch_state sa) proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>globals_equiv s sa \<and> valid_arch_state sa \<and> tptr \<noteq> idle_thread sa; \<exists>y. get_tcb tptr sa = Some y\<rbrakk> \<Longrightarrow> tptr \<noteq> arm_global_pd (arch_state sa) proof (prove)
goal:
No subgoals!
theory ArchSyscall_IF

lemma dmo_maskInterrupt_globals_equiv[Syscall_IF_assms, wp]:
  "do_machine_op (maskInterrupt b irq) \<lbrace>globals_equiv s\<rbrace>" unfolding maskInterrupt_def apply (rule dmo_no_mem_globals_equiv) apply (wp modify_wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> do_machine_op (maskInterrupt b irq) \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> do_machine_op (modify (\<lambda>s. s\<lparr>irq_masks := (irq_masks s)(irq := b)\<rparr>)) \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>P. \<lbrace>\<lambda>ms. P (underlying_memory ms)\<rbrace> modify (\<lambda>s. s\<lparr>irq_masks := (irq_masks s)(irq := b)\<rparr>) \<lbrace>\<lambda>_ ms. P (underlying_memory ms)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>ms. P (device_state ms)\<rbrace> modify (\<lambda>s. s\<lparr>irq_masks := (irq_masks s)(irq := b)\<rparr>) \<lbrace>\<lambda>_ ms. P (device_state ms)\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>ms. P (exclusive_state ms)\<rbrace> modify (\<lambda>s. s\<lparr>irq_masks := (irq_masks s)(irq := b)\<rparr>) \<lbrace>\<lambda>_ ms. P (exclusive_state ms)\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchSyscall_IF

lemma dmo_ackInterrupt_globals_equiv[Syscall_IF_assms, wp]:
  "do_machine_op (ackInterrupt irq) \<lbrace>globals_equiv s\<rbrace>" unfolding ackInterrupt_def by (rule dmo_mol_globals_equiv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> do_machine_op (machine_op_lift (ackInterrupt_impl irq)) \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
theory ArchSyscall_IF

lemma dmo_resetTimer_globals_equiv[Syscall_IF_assms, wp]:
  "do_machine_op resetTimer \<lbrace>globals_equiv s\<rbrace>" unfolding resetTimer_def by (rule dmo_mol_globals_equiv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> do_machine_op (machine_op_lift resetTimer_impl) \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
theory ArchSyscall_IF

lemma arch_mask_irq_signal_globals_equiv[Syscall_IF_assms, wp]:
  "arch_mask_irq_signal irq \<lbrace>globals_equiv st\<rbrace>" by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st\<rbrace> arch_mask_irq_signal irq \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
theory ArchSyscall_IF

lemma handle_reserved_irq_globals_equiv[Syscall_IF_assms, wp]:
  "handle_reserved_irq irq \<lbrace>globals_equiv st\<rbrace>" unfolding handle_reserved_irq_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st\<rbrace> handle_reserved_irq irq \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st\<rbrace> return () \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
theory ArchSyscall_IF

lemma handle_hypervisor_fault_reads_respects[Syscall_IF_assms]:
  "reads_respects aag l \<top> (handle_hypervisor_fault thread hypfault_type)" by (cases hypfault_type; wpsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (handle_hypervisor_fault thread hypfault_type)