kings-crown/FVELER_Isabelle huggingface dataset:
theory DomainSepInv

lemma empty_slot_domain_sep_inv:
  "\<lbrace>\<lambda>s. domain_sep_inv irqs st s \<and> (\<not> irqs \<longrightarrow> b = NullCap)\<rbrace>
   empty_slot a b
   \<lbrace>\<lambda>_ s. domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state)\<rbrace>" unfolding empty_slot_def post_cap_deletion_def by (wpsimp wp: get_cap_wp set_cap_domain_sep_inv set_original_wp dxo_wp_weak
                 hoare_weak_lift_imp deleted_irq_handler_domain_sep_inv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. domain_sep_inv irqs st s \<and> (\<not> irqs \<longrightarrow> b = NullCap)\<rbrace> empty_slot a b \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. domain_sep_inv irqs st s \<and> (\<not> irqs \<longrightarrow> b = NullCap)\<rbrace> do cap <- get_cap a;
if cap = NullCap then return () else do slot_p <- gets (\<lambda>s. cdt s a);
cdt <- gets cdt;
parent <- return $ cdt a;
set_cdt ((\<lambda>p. if cdt p = Some a then parent else cdt p)(a := None));
do_extended_op (empty_slot_ext a slot_p);
set_original a False;
set_cap NullCap a;
case b of IRQHandlerCap irq \<Rightarrow> deleted_irq_handler irq | ArchObjectCap acap \<Rightarrow> arch_post_cap_deletion acap | _ \<Rightarrow> return ()
od
od \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
theory DomainSepInv

lemma thread_set_tcb_fault_update_domain_sep_inv[wp]:
  "thread_set (tcb_fault_update blah) t \<lbrace>domain_sep_inv irqs st\<rbrace>" by (wp domain_sep_inv_triv)

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

lemma get_cap_domain_sep_inv_cap:
  "\<lbrace>domain_sep_inv irqs st\<rbrace> get_cap cap \<lbrace>\<lambda>rv s. domain_sep_inv_cap irqs rv\<rbrace>" by (wpsimp wp: get_cap_wp simp: cte_wp_at_domain_sep_inv_cap)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st\<rbrace> get_cap cap \<lbrace>\<lambda>rv s. domain_sep_inv_cap irqs rv\<rbrace>
theory DomainSepInv

lemma preemption_point_domain_sep_inv[wp]:
  "preemption_point \<lbrace>domain_sep_inv irqs st\<rbrace>" by (wp preemption_point_inv | simp)+

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

lemma reply_cancel_ipc_domain_sep_inv[wp]:
  "\<lbrace>domain_sep_inv irqs st\<rbrace>
   reply_cancel_ipc t
   \<lbrace>\<lambda>_ s. domain_sep_inv irqs  (st :: 'state_ext state) (s :: det_ext state)\<rbrace>" apply (simp add: reply_cancel_ipc_def) apply wp apply (rule hoare_strengthen_post[OF thread_set_tcb_fault_update_domain_sep_inv]) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st\<rbrace> reply_cancel_ipc t \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st\<rbrace> do y <- thread_set (tcb_fault_update (\<lambda>_. None)) t;
cap <- get_cap (t, tcb_cnode_index 2);
descs <- gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt);
when (descs \<noteq> {}) (do y <- assert (\<exists>a b. descs = {(a, b)});
select descs >>= cap_delete_one
od)
od \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>y s. (if (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) s \<noteq> {} then \<lambda>sa. (\<exists>a b. (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) s = {(a, b)}) \<longrightarrow> (\<forall>x\<in>(descendants_of (t, tcb_cnode_index 2) \<circ> cdt) s. domain_sep_inv irqs st sa) else domain_sep_inv irqs st) s\<rbrace>
 2. \<And>s. domain_sep_inv irqs st s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. domain_sep_inv ?irqs14 ?st14 s \<Longrightarrow> (if (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) s \<noteq> {} then \<lambda>sa. (\<exists>a b. (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) s = {(a, b)}) \<longrightarrow> (\<forall>x\<in>(descendants_of (t, tcb_cnode_index 2) \<circ> cdt) s. domain_sep_inv irqs st sa) else domain_sep_inv irqs st) s
 2. \<And>s. domain_sep_inv irqs st s \<Longrightarrow> domain_sep_inv ?irqs14 ?st14 s proof (prove)
goal:
No subgoals!
theory DomainSepInv

lemma finalise_cap_returns_NullCap:
  "\<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace>
   finalise_cap cap b
   \<lbrace>\<lambda>rv s :: det_ext state. \<not> irqs \<longrightarrow> snd rv = NullCap\<rbrace>" apply (case_tac cap) by (wpsimp wp: arch_finalise_cap_rv simp: o_def domain_sep_inv_cap_def split_del: if_split)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace> finalise_cap cap b \<lbrace>\<lambda>rv s. \<not> irqs \<longrightarrow> snd rv = NullCap\<rbrace> proof (prove)
goal (12 subgoals):
 1. cap = NullCap \<Longrightarrow> \<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace> finalise_cap cap b \<lbrace>\<lambda>rv s. \<not> irqs \<longrightarrow> snd rv = NullCap\<rbrace>
 2. \<And>x21 x22 x23 x24. cap = UntypedCap x21 x22 x23 x24 \<Longrightarrow> \<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace> finalise_cap cap b \<lbrace>\<lambda>rv s. \<not> irqs \<longrightarrow> snd rv = NullCap\<rbrace>
 3. \<And>x31 x32 x33. cap = EndpointCap x31 x32 x33 \<Longrightarrow> \<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace> finalise_cap cap b \<lbrace>\<lambda>rv s. \<not> irqs \<longrightarrow> snd rv = NullCap\<rbrace>
 4. \<And>x41 x42 x43. cap = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace> finalise_cap cap b \<lbrace>\<lambda>rv s. \<not> irqs \<longrightarrow> snd rv = NullCap\<rbrace>
 5. \<And>x51 x52 x53. cap = ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace> finalise_cap cap b \<lbrace>\<lambda>rv s. \<not> irqs \<longrightarrow> snd rv = NullCap\<rbrace>
 6. \<And>x61 x62 x63. cap = CNodeCap x61 x62 x63 \<Longrightarrow> \<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace> finalise_cap cap b \<lbrace>\<lambda>rv s. \<not> irqs \<longrightarrow> snd rv = NullCap\<rbrace>
 7. \<And>x7. cap = ThreadCap x7 \<Longrightarrow> \<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace> finalise_cap cap b \<lbrace>\<lambda>rv s. \<not> irqs \<longrightarrow> snd rv = NullCap\<rbrace>
 8. cap = DomainCap \<Longrightarrow> \<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace> finalise_cap cap b \<lbrace>\<lambda>rv s. \<not> irqs \<longrightarrow> snd rv = NullCap\<rbrace>
 9. cap = IRQControlCap \<Longrightarrow> \<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace> finalise_cap cap b \<lbrace>\<lambda>rv s. \<not> irqs \<longrightarrow> snd rv = NullCap\<rbrace>
 10. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace> finalise_cap cap b \<lbrace>\<lambda>rv s. \<not> irqs \<longrightarrow> snd rv = NullCap\<rbrace>
A total of 12 subgoals...
theory DomainSepInv

lemma rec_del_domain_sep_inv:
  "\<lbrace>domain_sep_inv irqs st\<rbrace>
   rec_del call
   \<lbrace>\<lambda>_ s. domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state)\<rbrace>" apply (rule validE_valid) apply (rule use_spec) apply (rule spec_strengthen_postE[OF rec_del_domain_sep_inv']) by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del call \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del call \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<turnstile> \<lbrace>domain_sep_inv irqs st\<rbrace> rec_del call \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s sa r. (case call of FinaliseSlotCall x y \<Rightarrow> y \<or> fst sa \<longrightarrow> \<not> irqs \<longrightarrow> snd sa = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st r \<Longrightarrow> domain_sep_inv irqs st r
theory DomainSepInv

lemma cap_move_cte_wp_at_other:
  "\<lbrace>cte_wp_at P slot and K (slot \<noteq> dest_slot \<and> slot \<noteq> src_slot)\<rbrace>
   cap_move cap src_slot dest_slot
   \<lbrace>\<lambda>_. cte_wp_at P slot\<rbrace>" unfolding cap_move_def by (wpsimp wp: set_cdt_cte_wp_at set_cap_cte_wp_at' dxo_wp_weak hoare_weak_lift_imp set_original_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at P slot and K (slot \<noteq> dest_slot \<and> slot \<noteq> src_slot)\<rbrace> cap_move cap src_slot dest_slot \<lbrace>\<lambda>_. cte_wp_at P slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at P slot and K (slot \<noteq> dest_slot \<and> slot \<noteq> src_slot)\<rbrace> do set_cap 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>_. cte_wp_at P slot\<rbrace>
theory DomainSepInv

lemma thread_set_tcb_registers_caps_merge_default_tcb_domain_sep_inv[wp]:
  "thread_set (tcb_registers_caps_merge default_tcb) word \<lbrace>domain_sep_inv irqs st\<rbrace>" by (wp domain_sep_inv_triv)

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

lemma cancel_badged_sends_domain_sep_inv[wp]:
  "cancel_badged_sends epptr badge \<lbrace>domain_sep_inv irqs st\<rbrace>" apply (simp add: cancel_badged_sends_def) apply (wpsimp wp: dxo_wp_weak mapM_wp | simp add: filterM_mapM | wp (once) hoare_drop_imps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st\<rbrace> cancel_badged_sends epptr badge \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st\<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>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal:
No subgoals!
theory DomainSepInv

lemma retype_region_domain_sep_inv[wp]:
  "retype_region base n sz tp dev \<lbrace>domain_sep_inv irqs st\<rbrace>" apply (rule domain_sep_inv_wp[where P="\<top>" and R="\<top>", simplified]) apply (rule retype_region_neg_cte_wp_at_not_domain_sep_inv_cap) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st\<rbrace> retype_region base n sz tp dev \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>slot. \<lbrace>\<lambda>s. \<not> cte_wp_at (not domain_sep_inv_cap irqs) slot s\<rbrace> retype_region base n sz tp dev \<lbrace>\<lambda>_ s. \<not> cte_wp_at (not domain_sep_inv_cap irqs) slot s\<rbrace>
 2. \<And>P. \<not> irqs \<Longrightarrow> \<lbrace>\<lambda>s. P (interrupt_states s)\<rbrace> retype_region base n sz tp dev \<lbrace>\<lambda>_ s. P (interrupt_states s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P. \<not> irqs \<Longrightarrow> \<lbrace>\<lambda>s. P (interrupt_states s)\<rbrace> retype_region base n sz tp dev \<lbrace>\<lambda>_ s. P (interrupt_states s)\<rbrace> proof (prove)
goal:
No subgoals!
theory DomainSepInv

lemma domain_sep_inv_cap_UntypedCap[simp]:
  "domain_sep_inv_cap irqs (UntypedCap dev base sz n)" by (simp add: domain_sep_inv_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. domain_sep_inv_cap irqs (UntypedCap dev base sz n)
theory DomainSepInv

lemma perform_page_invocation_domain_sep_inv_get_cap_helper:
  "\<lbrace>\<top>\<rbrace> get_cap blah \<lbrace>\<lambda>rv s. domain_sep_inv_cap irqs (ArchObjectCap (F rv))\<rbrace>" apply (simp add: domain_sep_inv_cap_def) apply (rule wp_post_taut) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> get_cap blah \<lbrace>\<lambda>rv s. domain_sep_inv_cap irqs (ArchObjectCap (F rv))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> get_cap blah \<lbrace>\<lambda>rv s. True\<rbrace> proof (prove)
goal:
No subgoals!
theory DomainSepInv

lemma set_object_tcb_arch_update_domain_sep_inv:
  "\<lbrace>domain_sep_inv irqs st and obj_at ((=) (TCB tcb)) ptr\<rbrace>
   set_object ptr (TCB (tcb\<lparr>tcb_arch := arch\<rparr>))
   \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" apply (wp set_object_wp) apply (simp add: domain_sep_inv_def fun_upd_def cte_wp_at_caps_of_state) apply (fastforce simp: caps_of_state_after_update obj_at_def tcb_cap_cases_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and ko_at (TCB tcb) ptr\<rbrace> set_object ptr (TCB (tcb\<lparr>tcb_arch := arch\<rparr>)) \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (domain_sep_inv irqs st and ko_at (TCB tcb) ptr) s \<Longrightarrow> domain_sep_inv irqs st (s\<lparr>kheap := (kheap s)(ptr \<mapsto> TCB (tcb\<lparr>tcb_arch := arch\<rparr>))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>a b. caps_of_state s (a, b) \<noteq> Some DomainCap) \<and> (irqs \<or> (\<forall>irq a b. caps_of_state s (a, b) \<noteq> Some IRQControlCap \<and> caps_of_state s (a, b) \<noteq> Some (IRQHandlerCap irq) \<and> interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st)) \<and> ko_at (TCB tcb) ptr s \<Longrightarrow> (\<forall>a b. caps_of_state (s\<lparr>kheap := \<lambda>x. if x = ptr then Some (TCB (tcb\<lparr>tcb_arch := arch\<rparr>)) else kheap s x\<rparr>) (a, b) \<noteq> Some DomainCap) \<and> (irqs \<or> (\<forall>irq a b. caps_of_state (s\<lparr>kheap := \<lambda>x. if x = ptr then Some (TCB (tcb\<lparr>tcb_arch := arch\<rparr>)) else kheap s x\<rparr>) (a, b) \<noteq> Some IRQControlCap \<and> caps_of_state (s\<lparr>kheap := \<lambda>x. if x = ptr then Some (TCB (tcb\<lparr>tcb_arch := arch\<rparr>)) else kheap s x\<rparr>) (a, b) \<noteq> Some (IRQHandlerCap irq) \<and> interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st)) proof (prove)
goal:
No subgoals!
theory DomainSepInv

lemma dxo_domain_sep_inv[wp]:
  "do_extended_op eop \<lbrace>domain_sep_inv irqs st\<rbrace>" by (simp | wp dxo_wp_weak)+

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

lemma cap_insert_domain_sep_inv':
  "\<lbrace>domain_sep_inv irqs st and K (domain_sep_inv_cap irqs cap)\<rbrace>
   cap_insert cap slot dest_slot
   \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" apply (simp add: cap_insert_def) apply (wp set_cap_domain_sep_inv get_cap_wp dxo_wp_weak | simp split del: if_split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and K (domain_sep_inv_cap irqs cap)\<rbrace> cap_insert cap slot dest_slot \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and (\<lambda>y. domain_sep_inv_cap irqs cap)\<rbrace> do src_cap <- get_cap slot;
old_cap <- get_cap dest_slot;
y <- assert (old_cap = NullCap);
y <- set_untyped_cap_as_full src_cap cap slot;
y <- set_cap cap dest_slot;
is_original <- gets is_original_cap;
src_p <- gets (\<lambda>s. cdt s slot);
dest_p <- gets (\<lambda>s. cdt s dest_slot);
y <- update_cdt (\<lambda>cdt. cdt(dest_slot := if should_be_parent_of src_cap (is_original slot) cap (is_cap_revocable cap src_cap) then Some slot else cdt slot));
y <- do_extended_op (cap_insert_ext (should_be_parent_of src_cap (is_original slot) cap (is_cap_revocable cap src_cap)) slot dest_slot src_p dest_p);
set_original dest_slot (is_cap_revocable cap src_cap)
od \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal:
No subgoals!
theory DomainSepInv

lemma domain_sep_inv_cap_max_free_index_update[simp]:
  "domain_sep_inv_cap irqs (max_free_index_update cap) =
   domain_sep_inv_cap irqs cap" by (simp add: max_free_index_def free_index_update_def split: cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. domain_sep_inv_cap irqs (max_free_index_update cap) = domain_sep_inv_cap irqs cap
theory DomainSepInv

lemma domain_sep_inv_cap_ArchObjectCap[simp]:
  "domain_sep_inv_cap irqs (ArchObjectCap arch_cap)" by (simp add: domain_sep_inv_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. domain_sep_inv_cap irqs (ArchObjectCap arch_cap)
theory DomainSepInv

lemma invoke_irq_handler_domain_sep_inv:
  "\<lbrace>domain_sep_inv irqs st and irq_handler_inv_valid i\<rbrace>
   invoke_irq_handler i
   \<lbrace>\<lambda>_ s. domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state)\<rbrace>" apply (case_tac i) apply (wp cap_insert_domain_sep_inv' | simp)+ apply (rename_tac irq cap cslot_ptr s) apply (case_tac cap, simp_all add: domain_sep_inv_cap_def)[1] apply (wp | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and irq_handler_inv_valid i\<rbrace> invoke_irq_handler i \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x1. i = ACKIrq x1 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and irq_handler_inv_valid i\<rbrace> invoke_irq_handler i \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>x21 x22 x23. i = SetIRQHandler x21 x22 x23 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and irq_handler_inv_valid i\<rbrace> invoke_irq_handler i \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 3. \<And>x3. i = ClearIRQHandler x3 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and irq_handler_inv_valid i\<rbrace> invoke_irq_handler i \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 x23 s. \<lbrakk>i = SetIRQHandler x21 x22 x23; domain_sep_inv irqs st s \<and> ex_cte_cap_wp_to is_cnode_cap x23 s \<and> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap x21)) (a, b) s) \<and> cte_wp_at (interrupt_derived x22) x23 s \<and> s \<turnstile> x22 \<and> is_ntfn_cap x22\<rbrakk> \<Longrightarrow> domain_sep_inv_cap irqs x22
 2. \<And>x3. i = ClearIRQHandler x3 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and irq_handler_inv_valid i\<rbrace> invoke_irq_handler i \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>irq cap cslot_ptr s. \<lbrakk>i = SetIRQHandler irq cap cslot_ptr; domain_sep_inv irqs st s \<and> ex_cte_cap_wp_to is_cnode_cap cslot_ptr s \<and> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s) \<and> cte_wp_at (interrupt_derived cap) cslot_ptr s \<and> s \<turnstile> cap \<and> is_ntfn_cap cap\<rbrakk> \<Longrightarrow> domain_sep_inv_cap irqs cap
 2. \<And>x3. i = ClearIRQHandler x3 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and irq_handler_inv_valid i\<rbrace> invoke_irq_handler i \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x3. i = ClearIRQHandler x3 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and irq_handler_inv_valid i\<rbrace> invoke_irq_handler i \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal:
No subgoals!
theory DomainSepInv

lemma derive_cap_domain_sep_inv_cap:
  "\<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace>
   derive_cap slot cap
   \<lbrace>\<lambda>rv s :: det_ext state. domain_sep_inv_cap irqs rv\<rbrace>,-" apply (simp add: derive_cap_def) apply (rule hoare_pre) apply (wp | wpc | simp add: )+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace> derive_cap slot cap \<lbrace>\<lambda>rv s. domain_sep_inv_cap irqs rv\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace> case cap of UntypedCap dev ptr sz f \<Rightarrow> doE ensure_no_children slot;
returnOk cap
odE | ReplyCap ptr m cr \<Rightarrow> returnOk NullCap | IRQControlCap \<Rightarrow> returnOk NullCap | Zombie ptr n sz \<Rightarrow> returnOk NullCap | ArchObjectCap c \<Rightarrow> arch_derive_cap c | _ \<Rightarrow> returnOk cap \<lbrace>\<lambda>rv s. domain_sep_inv_cap irqs rv\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> case cap of UntypedCap dev ptr sz f \<Rightarrow> doE ensure_no_children slot;
returnOk cap
odE | ReplyCap ptr m cr \<Rightarrow> returnOk NullCap | IRQControlCap \<Rightarrow> returnOk NullCap | Zombie ptr n sz \<Rightarrow> returnOk NullCap | ArchObjectCap c \<Rightarrow> arch_derive_cap c | _ \<Rightarrow> returnOk cap \<lbrace>\<lambda>rv s. domain_sep_inv_cap irqs rv\<rbrace>, -
 2. \<And>s. domain_sep_inv_cap irqs cap \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. domain_sep_inv_cap irqs cap \<Longrightarrow> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> domain_sep_inv_cap irqs (EndpointCap x xa xb)) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> domain_sep_inv_cap irqs (NotificationCap x xa xb)) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> domain_sep_inv_cap irqs (CNodeCap x xa xb)) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> domain_sep_inv_cap irqs (ThreadCap x)) \<and> (cap = DomainCap \<longrightarrow> domain_sep_inv_cap irqs DomainCap) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> domain_sep_inv_cap irqs (IRQHandlerCap x)) proof (prove)
goal:
No subgoals!
theory DomainSepInv

lemma domain_sep_inv_cap_ReplyCap[simp]:
  "domain_sep_inv_cap irqs (ReplyCap param_a param_b param_c)" by (simp add: domain_sep_inv_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. domain_sep_inv_cap irqs (ReplyCap param_a param_b param_c)
theory DomainSepInv

lemma setup_caller_cap_domain_sep_inv[wp]:
  "\<lbrace>domain_sep_inv irqs st\<rbrace>
   setup_caller_cap a b c
   \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" apply (simp add: setup_caller_cap_def split del:if_split) apply (wp cap_insert_domain_sep_inv' | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st\<rbrace> setup_caller_cap a b c \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st\<rbrace> do y <- set_thread_state a BlockedOnReply;
cap_insert (ReplyCap a False (if c then {AllowGrant, AllowWrite} else {AllowWrite})) (a, tcb_cnode_index 2) (b, tcb_cnode_index 3)
od \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal:
No subgoals!