kings-crown/FVELER_Isabelle huggingface dataset:
theory DomainSepInv

lemma transfer_caps_domain_sep_inv:
  "\<lbrace>domain_sep_inv irqs st and valid_objs and valid_mdb
        and (\<lambda> s. (\<forall>x\<in>set caps.
               s \<turnstile> fst x) \<and>
              (\<forall>x\<in>set caps.
               cte_wp_at
                (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow>
                      cp = fst x)
                (snd x) s \<and>
               real_cte_at (snd x) s))\<rbrace>
  transfer_caps mi caps endpoint receiver receive_buffer
  \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" unfolding transfer_caps_def apply (wpsimp wp: transfer_caps_loop_pres_dest cap_insert_domain_sep_inv
                    hoare_vcg_all_lift hoare_vcg_imp_lift) apply (fastforce elim: cte_wp_at_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and valid_objs and valid_mdb and (\<lambda>s. (\<forall>x\<in>set caps. s \<turnstile> fst x) \<and> (\<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s))\<rbrace> transfer_caps mi caps endpoint receiver receive_buffer \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and valid_objs and valid_mdb and (\<lambda>s. (\<forall>x\<in>set caps. s \<turnstile> fst x) \<and> (\<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s))\<rbrace> do dest_slots <- get_receive_slots receiver receive_buffer;
mi' <- return $ MI (mi_length mi) 0 0 (mi_label mi);
case receive_buffer of None \<Rightarrow> return mi' | Some receive_buffer \<Rightarrow> transfer_caps_loop endpoint receive_buffer 0 caps dest_slots mi'
od \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a aa b x. \<lbrakk>domain_sep_inv irqs st s; valid_objs s; valid_mdb s; \<forall>x\<in>set caps. s \<turnstile> fst x; \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s; (a, aa, b) \<in> set caps; receive_buffer = Some x\<rbrakk> \<Longrightarrow> s \<turnstile> a \<and> cap_table_at (length b) aa s \<and> cte_wp_at (\<lambda>cp. a \<noteq> NullCap \<and> cp \<noteq> a \<longrightarrow> cp = masked_as_full a a) (aa, b) s proof (prove)
goal:
No subgoals!
theory DomainSepInv

lemma do_normal_transfer_domain_sep_inv:
  "\<lbrace>domain_sep_inv irqs st and valid_objs and valid_mdb\<rbrace>
   do_normal_transfer sender send_buffer ep badge grant receiver recv_buffer
   \<lbrace>\<lambda>_ s. domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state)\<rbrace>" unfolding do_normal_transfer_def by (wp transfer_caps_domain_sep_inv hoare_vcg_ball_lift lec_valid_cap' | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and valid_objs and valid_mdb\<rbrace> do_normal_transfer sender send_buffer ep badge grant receiver recv_buffer \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and valid_objs and valid_mdb\<rbrace> do mi <- get_message_info sender;
caps <- if grant then lookup_extra_caps sender send_buffer mi <catch> K (return []) else return [];
mrs_transferred <- copy_mrs sender send_buffer receiver recv_buffer (mi_length mi);
mi' <- transfer_caps mi caps ep receiver recv_buffer;
set_message_info receiver $ MI mrs_transferred (mi_extra_caps mi') (mi_caps_unwrapped mi') (mi_label mi);
as_user receiver $ setRegister badge_register badge
od \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
theory DomainSepInv

lemma do_ipc_transfer_domain_sep_inv:
  "\<lbrace>domain_sep_inv irqs st and valid_objs and valid_mdb\<rbrace>
   do_ipc_transfer sender ep badge grant receiver
   \<lbrace>\<lambda>_ s. domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state)\<rbrace>" unfolding do_ipc_transfer_def apply (wp do_normal_transfer_domain_sep_inv hoare_vcg_all_lift | wpc | wp (once) hoare_drop_imps)+ apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and valid_objs and valid_mdb\<rbrace> do_ipc_transfer sender ep badge grant receiver \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and valid_objs and valid_mdb\<rbrace> do recv_buffer <- lookup_ipc_buffer True receiver;
fault <- thread_get tcb_fault sender;
case fault of None \<Rightarrow> do send_buffer <- lookup_ipc_buffer False sender;
do_normal_transfer sender send_buffer ep badge grant receiver recv_buffer
od | Some f \<Rightarrow> do_fault_transfer badge sender receiver recv_buffer
od \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (domain_sep_inv irqs st and valid_objs and valid_mdb) s \<Longrightarrow> (domain_sep_inv irqs st and valid_objs and valid_mdb) s \<and> (\<forall>x. domain_sep_inv irqs st s) proof (prove)
goal:
No subgoals!
theory DomainSepInv

lemma thread_set_tcb_ipc_buffer_update_domain_sep_inv[wp]:
  "thread_set (tcb_ipc_buffer_update f) t \<lbrace>domain_sep_inv irqs st\<rbrace>" by (rule domain_sep_inv_triv; wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st\<rbrace> thread_set (tcb_ipc_buffer_update f) t \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
theory DomainSepInv

lemma thread_set_tcb_fault_handler_update_domain_sep_inv[wp]:
  "thread_set (tcb_fault_handler_update f) t \<lbrace>domain_sep_inv irqs st\<rbrace>" by (rule domain_sep_inv_triv; wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st\<rbrace> thread_set (tcb_fault_handler_update f) t \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
theory DomainSepInv

lemma thread_set_tcb_tcp_mcpriority_update_domain_sep_inv[wp]:
  "thread_set (tcb_mcpriority_update f) t \<lbrace>domain_sep_inv irqs st\<rbrace>" by (rule domain_sep_inv_triv; wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st\<rbrace> thread_set (tcb_mcpriority_update f) t \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
theory DomainSepInv

lemma same_object_as_domain_sep_inv_cap:
  "\<lbrakk> same_object_as a cap; domain_sep_inv_cap irqs cap \<rbrakk>
     \<Longrightarrow> domain_sep_inv_cap irqs a" apply (case_tac a, simp_all add: same_object_as_def domain_sep_inv_cap_def) apply (case_tac cap, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>same_object_as a cap; domain_sep_inv_cap irqs cap\<rbrakk> \<Longrightarrow> domain_sep_inv_cap irqs a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>case cap of IRQHandlerCap n \<Rightarrow> False | _ \<Rightarrow> same_region_as IRQControlCap cap; case cap of DomainCap \<Rightarrow> False | IRQControlCap \<Rightarrow> irqs | IRQHandlerCap irq \<Rightarrow> irqs | _ \<Rightarrow> True; a = IRQControlCap\<rbrakk> \<Longrightarrow> irqs proof (prove)
goal:
No subgoals!
theory DomainSepInv

lemma checked_cap_insert_domain_sep_inv:
  "check_cap_at a b (check_cap_at c d (cap_insert a b e)) \<lbrace>domain_sep_inv irqs st\<rbrace>" apply (wp get_cap_wp cap_insert_domain_sep_inv' | simp add: check_cap_at_def)+ apply clarsimp apply (drule_tac cap=cap in cte_wp_at_domain_sep_inv_cap) apply assumption apply (erule (1) same_object_as_domain_sep_inv_cap) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st\<rbrace> check_cap_at a b (check_cap_at c d (cap_insert a b e)) \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. domain_sep_inv irqs st s \<Longrightarrow> \<forall>cap. same_object_as a cap \<longrightarrow> cte_wp_at ((=) cap) b s \<longrightarrow> (\<forall>cap. same_object_as c cap \<longrightarrow> cte_wp_at ((=) cap) d s \<longrightarrow> domain_sep_inv_cap irqs a) proof (prove)
goal (1 subgoal):
 1. \<And>s cap capa. \<lbrakk>domain_sep_inv irqs st s; same_object_as a cap; cte_wp_at ((=) cap) b s; same_object_as c capa; cte_wp_at ((=) capa) d s\<rbrakk> \<Longrightarrow> domain_sep_inv_cap irqs a proof (prove)
goal (2 subgoals):
 1. \<And>s cap capa. \<lbrakk>same_object_as a cap; cte_wp_at ((=) cap) b s; same_object_as c capa; cte_wp_at ((=) capa) d s\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (?slot34 s cap capa) s
 2. \<And>s cap capa. \<lbrakk>same_object_as a cap; cte_wp_at ((=) cap) b s; same_object_as c capa; cte_wp_at ((=) capa) d s; domain_sep_inv_cap irqs cap\<rbrakk> \<Longrightarrow> domain_sep_inv_cap irqs a proof (prove)
goal (1 subgoal):
 1. \<And>s cap capa. \<lbrakk>same_object_as a cap; cte_wp_at ((=) cap) b s; same_object_as c capa; cte_wp_at ((=) capa) d s; domain_sep_inv_cap irqs cap\<rbrakk> \<Longrightarrow> domain_sep_inv_cap irqs a proof (prove)
goal:
No subgoals!
theory DomainSepInv

lemma set_mcpriority_domain_sep_inv[wp]:
  "set_mcpriority tcb_ref mcp \<lbrace>domain_sep_inv irqs st\<rbrace>" unfolding set_mcpriority_def by wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st\<rbrace> set_mcpriority tcb_ref mcp \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st\<rbrace> thread_set (tcb_mcpriority_update (\<lambda>_. mcp)) tcb_ref \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
theory DomainSepInv

lemma invoke_domain_domain_set_inv:
  "invoke_domain word1 word2 \<lbrace>domain_sep_inv irqs st\<rbrace>" apply (simp add: invoke_domain_def) apply (wp dxo_wp_weak | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st\<rbrace> invoke_domain word1 word2 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st\<rbrace> liftE (do y <- do_extended_op (set_domain word1 word2);
return []
od) \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal:
No subgoals!
theory DomainSepInv

lemma handle_send_domain_sep_inv:
  "\<lbrace>domain_sep_inv irqs st and invs and ct_active\<rbrace>
   handle_send a
   \<lbrace>\<lambda>_ s. domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state)\<rbrace>" apply (simp add: handle_send_def) apply (wp handle_invocation_domain_sep_inv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and invs and ct_active\<rbrace> handle_send a \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and invs and ct_active\<rbrace> handle_invocation False a \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal:
No subgoals!
theory DomainSepInv

lemma handle_call_domain_sep_inv:
  "\<lbrace>domain_sep_inv irqs st and invs and ct_active\<rbrace>
   handle_call
   \<lbrace>\<lambda>_ s. domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state)\<rbrace>" apply (simp add: handle_call_def) apply (wp handle_invocation_domain_sep_inv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and invs and ct_active\<rbrace> handle_call \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and invs and ct_active\<rbrace> handle_invocation True True \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal:
No subgoals!
theory DomainSepInv

lemma handle_reply_domain_sep_inv:
  "\<lbrace>domain_sep_inv irqs st and invs\<rbrace>
   handle_reply
   \<lbrace>\<lambda>_ s. domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state)\<rbrace>" apply (simp add: handle_reply_def) apply (wp get_cap_wp | wpc)+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and invs\<rbrace> handle_reply \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and invs\<rbrace> do thread <- gets cur_thread;
caller_cap <- get_cap (thread, tcb_cnode_index 3);
case caller_cap of NullCap \<Rightarrow> return () | ReplyCap caller True R \<Rightarrow> fail | ReplyCap caller False R \<Rightarrow> do_reply_transfer thread caller (thread, tcb_cnode_index 3) (AllowGrant \<in> R) | _ \<Rightarrow> fail
od \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (domain_sep_inv irqs st and invs) s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) (cur_thread s, tcb_cnode_index 3) s \<longrightarrow> (cap = NullCap \<longrightarrow> domain_sep_inv irqs st s) \<and> (\<forall>x xa xb xc. cap = UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = ReplyCap x xa xb \<longrightarrow> (xa = True \<longrightarrow> True) \<and> (xa = False \<longrightarrow> (domain_sep_inv irqs st and (valid_objs and valid_mdb)) s)) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> True) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> True) \<and> (cap = DomainCap \<longrightarrow> True) \<and> (cap = IRQControlCap \<longrightarrow> True) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. cap = ArchObjectCap x \<longrightarrow> True) proof (prove)
goal:
No subgoals!
theory DomainSepInv

lemma lookup_slot_for_thread_cap_fault:
  "\<lbrace>invs\<rbrace> lookup_slot_for_thread t s -, \<lbrace>\<lambda>f s. valid_fault (CapFault x y f)\<rbrace>" apply (simp add: lookup_slot_for_thread_def) apply (wp resolve_address_bits_valid_fault2) apply clarsimp apply (erule (1) invs_valid_tcb_ctable) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> lookup_slot_for_thread t s -, \<lbrace>\<lambda>f s. valid_fault (CapFault x y f)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> doE tcb <- liftE (gets_the (get_tcb t));
resolve_address_bits (tcb_ctable tcb, s)
odE -, \<lbrace>\<lambda>f s. valid_fault (CapFault x y f)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. invs sa \<Longrightarrow> get_tcb t sa \<noteq> None \<longrightarrow> (invs and valid_cap (fst (tcb_ctable (the (get_tcb t sa)), s))) sa proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>invs s; get_tcb t s = Some y\<rbrakk> \<Longrightarrow> s \<turnstile> tcb_ctable y proof (prove)
goal:
No subgoals!
theory DomainSepInv

lemma domain_sep_inv_cur_thread_update[simp]:
  "domain_sep_inv irqs st (s\<lparr>cur_thread := X\<rparr>) = domain_sep_inv irqs st s" apply (simp add: domain_sep_inv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. domain_sep_inv irqs st (s\<lparr>cur_thread := X\<rparr>) = domain_sep_inv irqs st s proof (prove)
goal:
No subgoals!
theory DomainSepInv

lemma schedule_domain_sep_inv:
  "(schedule :: (unit,det_ext) s_monad) \<lbrace>domain_sep_inv irqs (st :: 'state_ext state)\<rbrace>" apply (simp add: schedule_def allActiveTCBs_def) apply (wp add: guarded_switch_to_lift hoare_drop_imps
            del: ethread_get_wp
         | wpc | clarsimp simp: get_thread_state_def thread_get_def trans_state_update'[symmetric]
                                schedule_choose_new_thread_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st\<rbrace> schedule \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st\<rbrace> do ct <- gets cur_thread;
ct_st <- get_thread_state ct;
gets scheduler_action >>= case_scheduler_action (do id <- gets idle_thread;
assert (runnable ct_st \<or> ct = id)
od) (\<lambda>candidate. do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (ct \<noteq> it) tcb_priority ct;
fastfail <- schedule_switch_thread_fastfail ct it ct_prio target_prio;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do y <- tcb_sched_action tcb_sched_enqueue candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable ct_st \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od) (do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
schedule_choose_new_thread
od)
od \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal:
No subgoals!
theory DomainSepInv

lemma call_kernel_domain_sep_inv:
  "\<lbrace>domain_sep_inv irqs st and invs and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s)\<rbrace>
   call_kernel ev :: (unit,det_ext) s_monad
   \<lbrace>\<lambda>_ s. domain_sep_inv irqs (st :: 'state_ext state) s\<rbrace>" apply (simp add: call_kernel_def) apply (wp handle_interrupt_domain_sep_inv handle_event_domain_sep_inv schedule_domain_sep_inv
         | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and invs and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s)\<rbrace> call_kernel ev \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and invs and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s)\<rbrace> do y <- handle_event ev <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od));
y <- schedule;
activate_thread
od \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchDomainSepInv

lemma arch_finalise_cap_rv[DomainSepInv_assms]:
  "\<lbrace>\<lambda>_. P (NullCap,NullCap)\<rbrace> arch_finalise_cap c x \<lbrace>\<lambda>rv _. P rv\<rbrace>" unfolding arch_finalise_cap_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. P (NullCap, NullCap)\<rbrace> arch_finalise_cap c x \<lbrace>\<lambda>rv _. P rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. P (NullCap, NullCap)\<rbrace> case (c, x) of (ASIDPoolCap ptr b, True) \<Rightarrow> do delete_asid_pool b ptr;
return (NullCap, NullCap)
od | (ASIDPoolCap ptr b, False) \<Rightarrow> return (NullCap, NullCap) | (ASIDControlCap, xb) \<Rightarrow> return (NullCap, NullCap) | (PageCap x ptr xa s None, xb) \<Rightarrow> return (NullCap, NullCap) | (PageCap x ptr xa s (Some (a, v)), xb) \<Rightarrow> do unmap_page s a v ptr;
return (NullCap, NullCap)
od | (PageTableCap ptr None, xb) \<Rightarrow> return (NullCap, NullCap) | (PageTableCap ptr (Some (a, v)), True) \<Rightarrow> do unmap_page_table a v ptr;
return (NullCap, NullCap)
od | (PageTableCap ptr (Some (a, v)), False) \<Rightarrow> return (NullCap, NullCap) | (PageDirectoryCap ptr None, xb) \<Rightarrow> return (NullCap, NullCap) | (PageDirectoryCap ptr (Some a), True) \<Rightarrow> do delete_asid a ptr;
return (NullCap, NullCap)
od | (PageDirectoryCap ptr (Some a), False) \<Rightarrow> return (NullCap, NullCap) \<lbrace>\<lambda>rv _. P rv\<rbrace>
theory ArchDomainSepInv

lemma perform_page_invocation_domain_sep_inv:
  "\<lbrace>domain_sep_inv irqs st and valid_page_inv pgi\<rbrace>
   perform_page_invocation pgi
   \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" apply (rule hoare_pre) apply (wp mapM_wp[OF _ subset_refl] set_cap_domain_sep_inv mapM_x_wp[OF _ subset_refl]
             perform_page_invocation_domain_sep_inv_get_cap_helper hoare_weak_lift_imp
          | simp add: perform_page_invocation_def o_def | wpc)+ apply (clarsimp simp: valid_page_inv_def) apply (case_tac xa, simp_all add: domain_sep_inv_cap_def is_pg_cap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and valid_page_inv pgi\<rbrace> perform_page_invocation pgi \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> perform_page_invocation pgi \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>s. (domain_sep_inv irqs st and valid_page_inv pgi) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. domain_sep_inv irqs st s \<and> valid_page_inv pgi s \<Longrightarrow> \<forall>x xa a b xb. pgi = PageMap x xa (a, b) xb \<longrightarrow> ((\<exists>a b. xb = Inl (a, b)) \<longrightarrow> domain_sep_inv_cap irqs xa) \<and> ((\<exists>a b. xb = Inr (a, b)) \<longrightarrow> domain_sep_inv_cap irqs xa) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa a b xb aa pd ba. \<lbrakk>domain_sep_inv irqs st s; pgi = PageMap x xa (a, b) xb; cte_wp_at (is_arch_update xa) (a, b) s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) (a, b) s \<or> cte_wp_at (\<lambda>c. same_refs xb c s) (a, b) s; cte_wp_at is_pg_cap (a, b) s; same_refs xb xa s; valid_slots xb s; s \<turnstile> xa; is_pg_cap xa; empty_refs xb; x \<le> mask local.asid_bits; x \<noteq> 0; vspace_at_asid x pd s; cte_wp_at (parent_for_refs xb) (aa, ba) s\<rbrakk> \<Longrightarrow> ((\<exists>a b. xb = Inl (a, b)) \<longrightarrow> domain_sep_inv_cap irqs xa) \<and> ((\<exists>a b. xb = Inr (a, b)) \<longrightarrow> domain_sep_inv_cap irqs xa) proof (prove)
goal:
No subgoals!
theory ArchDomainSepInv

lemma perform_page_directory_invocation_domain_sep_inv:
  "perform_page_directory_invocation pti \<lbrace>domain_sep_inv irqs st\<rbrace>" apply (simp add: perform_page_directory_invocation_def) apply (cases pti) apply (simp | wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st\<rbrace> perform_page_directory_invocation pti \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st\<rbrace> case pti of PageDirectoryFlush typ start end pstart pd asid \<Rightarrow> when (start < end) $ do root_switched <- set_vm_root_for_flush pd asid;
do_machine_op $ do_flush typ start end pstart;
when root_switched $ gets cur_thread >>= set_vm_root
od | PageDirectoryNothing \<Rightarrow> return () \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16. pti = PageDirectoryFlush x11 x12 x13 x14 x15 x16 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st\<rbrace> case pti of PageDirectoryFlush typ start end pstart pd asid \<Rightarrow> when (start < end) $ do root_switched <- set_vm_root_for_flush pd asid;
do_machine_op $ do_flush typ start end pstart;
when root_switched $ gets cur_thread >>= set_vm_root
od | PageDirectoryNothing \<Rightarrow> return () \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. pti = PageDirectoryNothing \<Longrightarrow> \<lbrace>domain_sep_inv irqs st\<rbrace> case pti of PageDirectoryFlush typ start end pstart pd asid \<Rightarrow> when (start < end) $ do root_switched <- set_vm_root_for_flush pd asid;
do_machine_op $ do_flush typ start end pstart;
when root_switched $ gets cur_thread >>= set_vm_root
od | PageDirectoryNothing \<Rightarrow> return () \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal:
No subgoals!