kings-crown/FVELER_Isabelle huggingface dataset:
theory Invocation_DP

lemma decode_asid_pool_invocation_inv[wp]:
  "\<lbrace>P\<rbrace> decode_asid_pool_invocation a b c d \<lbrace>\<lambda>_. P\<rbrace>" apply (simp add:decode_asid_pool_invocation_def) apply (rule hoare_pre) apply (wpc|wp |simp add:throw_on_none_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> decode_asid_pool_invocation a b c d \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> case d of AsidPoolAssignIntent \<Rightarrow> doE (pd_cap, pd_cap_ref) <- throw_on_none $ get_index c 0;
case pd_cap of PageDirectoryCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
base <- case a of AsidPoolCap p base \<Rightarrow> returnOk $ base | _ \<Rightarrow> throw;
offset <- liftE $ select {x. x < 2 ^ asid_low_bits};
returnOk $ Assign (base, offset) pd_cap_ref (cap_object a, offset)
odE \<sqinter> throw \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case d of AsidPoolAssignIntent \<Rightarrow> doE (pd_cap, pd_cap_ref) <- throw_on_none $ get_index c 0;
case pd_cap of PageDirectoryCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
base <- case a of AsidPoolCap p base \<Rightarrow> returnOk $ base | _ \<Rightarrow> throw;
offset <- liftE $ select {x. x < 2 ^ asid_low_bits};
returnOk $ Assign (base, offset) pd_cap_ref (cap_object a, offset)
odE \<sqinter> throw \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Invocation_DP

lemma nonep_invocation_simps:
  "nonep_invocation (InvokeUntyped a) = True" by (simp add:nonep_invocation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. nonep_invocation (InvokeUntyped a) = True
theory Invocation_DP

lemma ep_related_cap_reset_simp[simp]:
  "ep_related_cap (reset_cap_asid x) = ep_related_cap x" apply (case_tac x) apply (auto simp:reset_cap_asid_def ep_related_cap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ep_related_cap (reset_cap_asid x) = ep_related_cap x proof (prove)
goal (27 subgoals):
 1. x = NullCap \<Longrightarrow> ep_related_cap (reset_cap_asid x) = ep_related_cap x
 2. \<And>x21 x22 x23. x = UntypedCap x21 x22 x23 \<Longrightarrow> ep_related_cap (reset_cap_asid x) = ep_related_cap x
 3. \<And>x31 x32 x33. x = EndpointCap x31 x32 x33 \<Longrightarrow> ep_related_cap (reset_cap_asid x) = ep_related_cap x
 4. \<And>x41 x42 x43. x = NotificationCap x41 x42 x43 \<Longrightarrow> ep_related_cap (reset_cap_asid x) = ep_related_cap x
 5. \<And>x51 x52. x = ReplyCap x51 x52 \<Longrightarrow> ep_related_cap (reset_cap_asid x) = ep_related_cap x
 6. \<And>x6. x = MasterReplyCap x6 \<Longrightarrow> ep_related_cap (reset_cap_asid x) = ep_related_cap x
 7. \<And>x71 x72 x73 x74. x = CNodeCap x71 x72 x73 x74 \<Longrightarrow> ep_related_cap (reset_cap_asid x) = ep_related_cap x
 8. \<And>x8. x = TcbCap x8 \<Longrightarrow> ep_related_cap (reset_cap_asid x) = ep_related_cap x
 9. x = DomainCap \<Longrightarrow> ep_related_cap (reset_cap_asid x) = ep_related_cap x
 10. \<And>x101 x102 x103 x104 x105 x106. x = PendingSyncSendCap x101 x102 x103 x104 x105 x106 \<Longrightarrow> ep_related_cap (reset_cap_asid x) = ep_related_cap x
A total of 27 subgoals... proof (prove)
goal:
No subgoals!
theory Invocation_DP

lemma liftE_wp_split_r:
  "\<lbrakk>\<And>r. \<lbrace>P' r\<rbrace> g r \<lbrace>Q\<rbrace>,\<lbrace>\<lambda>r. R\<rbrace>;\<lbrace>P\<rbrace>f\<lbrace>\<lambda>r. P' r\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> liftE f >>=E g \<lbrace>Q\<rbrace>,\<lbrace>\<lambda>r. R\<rbrace>" apply (simp add:liftE_bindE validE_def) including no_pre apply wp apply assumption apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r. \<lbrace>P' r\<rbrace> g r \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r. R\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>P'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> liftE f >>=E g \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r. R\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r. \<lbrace>P' r\<rbrace> g r \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R s | Inr r \<Rightarrow> Q r s\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>P'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f >>= g \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R s | Inr r \<Rightarrow> Q r s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r. \<lbrace>P' r\<rbrace> g r \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R s | Inr r \<Rightarrow> Q r s\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>P'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f >>= g \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R s | Inr r \<Rightarrow> Q r s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<And>r. \<lbrace>P' r\<rbrace> g r \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R s | Inr r \<Rightarrow> Q r s\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>P'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?B2 x\<rbrace> g x \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R s | Inr r \<Rightarrow> Q r s\<rbrace>
 2. \<lbrakk>\<And>r. \<lbrace>P' r\<rbrace> g r \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R s | Inr r \<Rightarrow> Q r s\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>P'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>?B2\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r. \<lbrace>P' r\<rbrace> g r \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> R s | Inr r \<Rightarrow> Q r s\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>P'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>P'\<rbrace> proof (prove)
goal:
No subgoals!
theory Invocation_DP

lemma wp_no_exception_seq_r:
  assumes validE_g: "\<And>r. \<lbrace>P' r\<rbrace> g r \<lbrace>Q\<rbrace>,\<lbrace>\<lambda>r s. False\<rbrace>"
      and validE_f: "\<lbrace>P\<rbrace>f\<lbrace>\<lambda>r. P' r\<rbrace>,\<lbrace>\<lambda>r. Inv\<rbrace>"
  shows "\<lbrace>P\<rbrace> f >>=E g \<lbrace>Q\<rbrace>,\<lbrace>\<lambda>r. Inv\<rbrace>" apply (rule hoare_pre) apply (rule hoare_vcg_seqE) apply (rule hoare_post_impErr[OF validE_g]) apply simp apply simp apply (wp validE_f) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f >>=E g \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> f >>=E g \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>?B3 x\<rbrace> g x \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>
 2. \<lbrace>?Q\<rbrace> f \<lbrace>?B3\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>
 3. \<And>s. P s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>x rv s. Q rv s \<Longrightarrow> Q rv s
 2. \<And>x e s. False \<Longrightarrow> Inv s
 3. \<lbrace>?Q\<rbrace> f \<lbrace>P'\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>
 4. \<And>s. P s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>x e s. False \<Longrightarrow> Inv s
 2. \<lbrace>?Q\<rbrace> f \<lbrace>P'\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>
 3. \<And>s. P s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> f \<lbrace>P'\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> P s proof (prove)
goal:
No subgoals!
theory Invocation_DP

lemma corrupt_tcb_intent_all_active_tcbs[wp]:
  "\<lbrace>\<lambda>s. P (all_scheduable_tcbs (cdl_objects s)) \<rbrace>
    corrupt_tcb_intent thread
  \<lbrace>\<lambda>rv s. P (all_scheduable_tcbs (cdl_objects s)) \<rbrace>" apply (rule sep_inv_to_all_scheduable_tcbs) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (all_scheduable_tcbs (cdl_objects s))\<rbrace> corrupt_tcb_intent thread \<lbrace>\<lambda>rv s. P (all_scheduable_tcbs (cdl_objects s))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrace>cdl.lift P\<rbrace> corrupt_tcb_intent thread \<lbrace>\<lambda>rv. cdl.lift P\<rbrace> proof (prove)
goal:
No subgoals!
theory Invocation_DP

lemma corrupt_ipc_buffer_active_tcbs[wp]:
  "\<lbrace>\<lambda>s. P (all_scheduable_tcbs (cdl_objects s)) \<rbrace>
    corrupt_ipc_buffer thread p
  \<lbrace>\<lambda>rv s. P (all_scheduable_tcbs (cdl_objects s)) \<rbrace>" apply (rule sep_inv_to_all_scheduable_tcbs) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (all_scheduable_tcbs (cdl_objects s))\<rbrace> corrupt_ipc_buffer thread p \<lbrace>\<lambda>rv s. P (all_scheduable_tcbs (cdl_objects s))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrace>cdl.lift P\<rbrace> corrupt_ipc_buffer thread p \<lbrace>\<lambda>rv. cdl.lift P\<rbrace> proof (prove)
goal:
No subgoals!
theory Invocation_DP

lemma update_thread_wp:
  "\<lbrace>tcb_at' (\<lambda>tcb. P (f tcb)) thread\<rbrace> update_thread thread f
  \<lbrace>\<lambda>rv. tcb_at' P thread \<rbrace>" apply (simp add:update_thread_def) apply (wp|wpc | simp add:set_object_def)+ apply (simp add:object_at_def) apply (clarsimp simp:object_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' (\<lambda>tcb. P (f tcb)) thread\<rbrace> update_thread thread f \<lbrace>\<lambda>rv. tcb_at' P thread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' (\<lambda>tcb. P (f tcb)) thread\<rbrace> do t <- get_object thread;
case t of Tcb tcb \<Rightarrow> set_object thread (Tcb (f tcb)) | _ \<Rightarrow> fail
od \<lbrace>\<lambda>rv. tcb_at' P thread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. tcb_at' (\<lambda>tcb. P (f tcb)) thread s \<Longrightarrow> (\<exists>y. cdl_objects s thread = Some y) \<longrightarrow> (\<forall>x. the (cdl_objects s thread) = Tcb x \<longrightarrow> tcb_at' P thread (s\<lparr>cdl_objects := \<lambda>a. if a = thread then Some (Tcb (f x)) else cdl_objects s a\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<exists>object. cdl_objects s thread = Some object \<and> (\<exists>tcb. object = Tcb tcb \<and> P (f tcb)) \<Longrightarrow> (\<exists>y. cdl_objects s thread = Some y) \<longrightarrow> (\<forall>x. the (cdl_objects s thread) = Tcb x \<longrightarrow> P (f x)) proof (prove)
goal:
No subgoals!
theory Invocation_DP

lemma invoke_cnode_insert_cap:
  "\<lbrace>\<lambda>s. < dest_slot \<mapsto>c - \<and>* R> s \<and> \<not> is_untyped_cap cap'  \<rbrace>
  invoke_cnode (InsertCall cap' src_slot dest_slot)
  \<lbrace>\<lambda>rv s. <dest_slot \<mapsto>c cap' \<and>* R> s\<rbrace>,\<lbrace>\<lambda>r s. Q\<rbrace>" apply (simp add:validE_def) apply (rule hoare_name_pre_state) apply (clarsimp simp:invoke_cnode_def liftE_bindE validE_def[symmetric]) apply (wpsimp wp: insert_cap_sibling_wp insert_cap_child_wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cdl.lift (dest_slot \<mapsto>c - \<and>* R) s \<and> cap_type cap' \<noteq> Some UntypedType\<rbrace> invoke_cnode (InsertCall cap' src_slot dest_slot) \<lbrace>\<lambda>rv. cdl.lift (dest_slot \<mapsto>c cap' \<and>* R)\<rbrace>, \<lbrace>\<lambda>r s. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cdl.lift (dest_slot \<mapsto>c - \<and>* R) s \<and> cap_type cap' \<noteq> Some UntypedType\<rbrace> invoke_cnode (InsertCall cap' src_slot dest_slot) \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q | Inr r \<Rightarrow> cdl.lift (dest_slot \<mapsto>c cap' \<and>* R) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cdl.lift (dest_slot \<mapsto>c - \<and>* R) s \<and> cap_type cap' \<noteq> Some UntypedType \<Longrightarrow> \<lbrace>(=) s\<rbrace> invoke_cnode (InsertCall cap' src_slot dest_slot) \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q | Inr r \<Rightarrow> cdl.lift (dest_slot \<mapsto>c cap' \<and>* R) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cdl.lift (dest_slot \<mapsto>c - \<and>* R) s; cap_type cap' \<noteq> Some UntypedType\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> insert_cap_sibling cap' src_slot dest_slot \<sqinter> insert_cap_child cap' src_slot dest_slot \<lbrace>\<lambda>r. cdl.lift (dest_slot \<mapsto>c cap' \<and>* R)\<rbrace> proof (prove)
goal:
No subgoals!
theory Invocation_DP

lemma invoke_cnode_move_wp:
  "\<lbrace><dest \<mapsto>c - \<and>* src \<mapsto>c cap \<and>* R>\<rbrace> invoke_cnode (MoveCall cap' src dest)
  \<lbrace>\<lambda>_. <dest \<mapsto>c cap' \<and>* src \<mapsto>c NullCap \<and>* R>\<rbrace>" apply (simp add:invoke_cnode_def) apply (wp move_cap_wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (dest \<mapsto>c - \<and>* src \<mapsto>c cap \<and>* R)\<rbrace> invoke_cnode (MoveCall cap' src dest) \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c cap' \<and>* src \<mapsto>c NullCap \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (dest \<mapsto>c - \<and>* src \<mapsto>c cap \<and>* R)\<rbrace> liftE (move_cap cap' src dest) \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c cap' \<and>* src \<mapsto>c NullCap \<and>* R)\<rbrace> proof (prove)
goal:
No subgoals!
theory Invocation_DP

lemma decode_invocation_simps:
  "is_cnode_cap cap
    \<Longrightarrow> decode_invocation cap cap_ref caps (CNodeIntent intent)
    = liftME InvokeCNode (decode_cnode_invocation cap cap_ref caps intent)" by (clarsimp simp: decode_invocation_def get_cnode_intent_def
                     throw_opt_def cap_type_def
              split: cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_cnode_cap cap \<Longrightarrow> decode_invocation cap cap_ref caps (CNodeIntent intent) = liftME InvokeCNode (decode_cnode_invocation cap cap_ref caps intent)
theory Invocation_DP

lemma sep_normal_conj_absorb:
  "(<A \<and>* sep_true> s \<and> <A \<and>* B> s)  = <A \<and>* B> s" by (auto intro:sep_conj_sep_true_right)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (cdl.lift (A \<and>* (\<lambda>s. True)) s \<and> cdl.lift (A \<and>* B) s) = cdl.lift (A \<and>* B) s
theory Invocation_DP

lemma sep_normal_conj_absorb':
  "(<A \<and>* sep_true > s \<and> < C \<and>* A \<and>* B > s) = < C \<and>* A \<and>* B> s" apply (subst sep_conj_left_commute) apply (simp add:sep_normal_conj_absorb) apply (simp add:sep_conj_left_commute) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (cdl.lift (A \<and>* (\<lambda>s. True)) s \<and> cdl.lift (C \<and>* A \<and>* B) s) = cdl.lift (C \<and>* A \<and>* B) s proof (prove)
goal (1 subgoal):
 1. (cdl.lift (A \<and>* (\<lambda>s. True)) s \<and> cdl.lift (A \<and>* C \<and>* B) s) = cdl.lift (C \<and>* A \<and>* B) s proof (prove)
goal (1 subgoal):
 1. cdl.lift (A \<and>* C \<and>* B) s = cdl.lift (C \<and>* A \<and>* B) s proof (prove)
goal:
No subgoals!
theory Invocation_DP

lemma cnode_cap_non_ep_related:
  "is_cnode_cap cap \<Longrightarrow> \<not> ep_related_cap cap" by (clarsimp simp: cap_type_def ep_related_cap_def split:cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_cnode_cap cap \<Longrightarrow> \<not> ep_related_cap cap
theory Invocation_DP

lemma update_thread_cnode_at:
  "\<lbrace>object_at(\<lambda>x. x = CNode cnode) ptr\<rbrace>
  update_thread cur_thread content
  \<lbrace>\<lambda>rv. object_at (\<lambda>x. x = CNode cnode) ptr \<rbrace>" apply (simp add:update_thread_def get_thread_def set_object_def) apply (wp|wpc|simp add: object_at_def set_object_def)+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>object_at (\<lambda>x. x = CNode cnode) ptr\<rbrace> update_thread cur_thread content \<lbrace>\<lambda>rv. object_at (\<lambda>x. x = CNode cnode) ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>object_at (\<lambda>x. x = CNode cnode) ptr\<rbrace> do t <- get_object cur_thread;
case t of Tcb tcb \<Rightarrow> set_object cur_thread (Tcb (content tcb)) | _ \<Rightarrow> fail
od \<lbrace>\<lambda>rv. object_at (\<lambda>x. x = CNode cnode) ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cdl_objects s ptr = Some (CNode cnode) \<Longrightarrow> (\<exists>y. cdl_objects s cur_thread = Some y) \<longrightarrow> ptr = cur_thread \<longrightarrow> (\<forall>x. the (cdl_objects s cur_thread) \<noteq> Tcb x) proof (prove)
goal:
No subgoals!
theory Invocation_DP

lemma cdl_cur_thread_detype:
  "cdl_current_thread (detype m s) = cdl_current_thread s" by (simp add:detype_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdl_current_thread (detype m s) = cdl_current_thread s
theory Invocation_DP

lemma cnode_insert_cap_cdl_current_thread:
  "\<lbrace>\<lambda>s. P (cdl_current_thread s)  \<rbrace>
  invoke_cnode (InsertCall a b c)
  \<lbrace>\<lambda>rv s. P (cdl_current_thread s)\<rbrace>" apply (rule hoare_name_pre_state) apply (clarsimp simp:
    invoke_cnode_def liftE_bindE validE_def[symmetric]) apply (rule hoare_pre) apply (wp | simp | wpc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cdl_current_thread s)\<rbrace> invoke_cnode (InsertCall a b c) \<lbrace>\<lambda>rv s. P (cdl_current_thread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (cdl_current_thread s) \<Longrightarrow> \<lbrace>(=) s\<rbrace> invoke_cnode (InsertCall a b c) \<lbrace>\<lambda>rv s. P (cdl_current_thread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (cdl_current_thread s) \<Longrightarrow> \<lbrace>(=) s\<rbrace> liftE (insert_cap_sibling a b c \<sqinter> insert_cap_child a b c) \<lbrace>\<lambda>rv s. P (cdl_current_thread s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. P (cdl_current_thread s) \<Longrightarrow> \<lbrace>?Q2 s\<rbrace> liftE (insert_cap_sibling a b c \<sqinter> insert_cap_child a b c) \<lbrace>\<lambda>rv s. P (cdl_current_thread s)\<rbrace>
 2. \<And>s sa. \<lbrakk>P (cdl_current_thread s); s = sa\<rbrakk> \<Longrightarrow> ?Q2 s sa proof (prove)
goal:
No subgoals!
theory Invocation_DP

lemma cnode_move_cap_cdl_current_thread:
  "\<lbrace>\<lambda>s. P (cdl_current_thread s)  \<rbrace>
  invoke_cnode (MoveCall a b c)
  \<lbrace>\<lambda>rv s. P (cdl_current_thread s)\<rbrace>" apply (rule hoare_name_pre_state) apply (clarsimp simp:
    invoke_cnode_def liftE_bindE validE_def[symmetric]) apply (rule hoare_pre) apply (wp | simp | wpc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cdl_current_thread s)\<rbrace> invoke_cnode (MoveCall a b c) \<lbrace>\<lambda>rv s. P (cdl_current_thread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (cdl_current_thread s) \<Longrightarrow> \<lbrace>(=) s\<rbrace> invoke_cnode (MoveCall a b c) \<lbrace>\<lambda>rv s. P (cdl_current_thread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (cdl_current_thread s) \<Longrightarrow> \<lbrace>(=) s\<rbrace> liftE (move_cap a b c) \<lbrace>\<lambda>rv s. P (cdl_current_thread s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. P (cdl_current_thread s) \<Longrightarrow> \<lbrace>?Q2 s\<rbrace> liftE (move_cap a b c) \<lbrace>\<lambda>rv s. P (cdl_current_thread s)\<rbrace>
 2. \<And>s sa. \<lbrakk>P (cdl_current_thread s); s = sa\<rbrakk> \<Longrightarrow> ?Q2 s sa proof (prove)
goal:
No subgoals!
theory Invocation_DP

lemma sep_any_imp_c'_conj:
 "< slot \<mapsto>c cap \<and>* R> s \<Longrightarrow> < slot \<mapsto>c - \<and>* R> s" by sep_solve

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdl.lift (slot \<mapsto>c cap \<and>* R) s \<Longrightarrow> cdl.lift (slot \<mapsto>c - \<and>* R) s
theory Invocation_DP

lemma reset_cap_asid_cnode_cap_cong:
  "\<lbrakk>reset_cap_asid cap = reset_cap_asid cap'\<rbrakk>
  \<Longrightarrow> is_cnode_cap cap = is_cnode_cap cap'" by (case_tac cap,
       simp_all add: cap_type_def reset_cap_asid_def
              split: cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reset_cap_asid cap = reset_cap_asid cap' \<Longrightarrow> is_cnode_cap cap = is_cnode_cap cap'
theory Invocation_DP

lemma is_exclusive_cap_update_cap[simp]:
  "safe_for_derive (update_cap_data_det data cap) = safe_for_derive cap" by (case_tac cap,
      simp_all add: update_cap_data_det_def update_cap_badge_def
                    safe_for_derive_def badge_update_def guard_update_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. safe_for_derive (update_cap_data_det data cap) = safe_for_derive cap
theory Invocation_DP

lemma cnode_cap_reset_asid:
  "is_cnode_cap cap \<Longrightarrow> (reset_cap_asid cap) = cap" by (unfold cap_type_def,
      simp add: reset_cap_asid_def
         split: cdl_cap.splits cdl_object_type.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_cnode_cap cap \<Longrightarrow> reset_cap_asid cap = cap
theory Invocation_DP

lemma is_cnode_cap_guard_equal:
  "is_cnode_cap x \<Longrightarrow> guard_equal (reset_cap_asid x) = guard_equal x" apply (rule ext)+ by (unfold cap_type_def, simp add:guard_equal_def  Let_def cap_guard_size_def
    reset_cap_asid_def split:cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_cnode_cap x \<Longrightarrow> guard_equal (reset_cap_asid x) = guard_equal x proof (prove)
goal (1 subgoal):
 1. \<And>xa xaa. is_cnode_cap x \<Longrightarrow> guard_equal (reset_cap_asid x) xa xaa = guard_equal x xa xaa
theory Invocation_DP

lemma valid_src_cap_has_type[simp]:
  "cap_type cap = Some type
  \<Longrightarrow> valid_src_cap (default_cap type ids (cnode_cap_size cap) dev)
  = valid_src_cap cap" apply (rule ext) apply (clarsimp simp: default_cap_def valid_src_cap_def
                        is_cnode_cap_simps
                  split: cdl_cap.splits cdl_object_type.splits) apply (clarsimp simp: cap_type_def cnode_cap_size_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_type cap = Some type \<Longrightarrow> valid_src_cap (default_cap type ids (cnode_cap_size cap) dev) = valid_src_cap cap proof (prove)
goal (1 subgoal):
 1. \<And>x. cap_type cap = Some type \<Longrightarrow> valid_src_cap (default_cap type ids (cnode_cap_size cap) dev) x = valid_src_cap cap x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_cnode_cap cap; type = CNodeType\<rbrakk> \<Longrightarrow> (unat ((x >> 3) && mask 5) + cnode_cap_size (CNodeCap (pick ids) 0 0 (cnode_cap_size cap)) \<le> word_bits) = (unat ((x >> 3) && mask 5) + cnode_cap_size cap \<le> word_bits) proof (prove)
goal:
No subgoals!
theory Invocation_DP

lemma exclusive_cap_has_type[simp]:
  "cap_type cap = Some type
  \<Longrightarrow> safe_for_derive (default_cap type ids sz dev) = safe_for_derive cap" by (fastforce simp: default_cap_def
                      cap_type_def safe_for_derive_def
               split: cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_type cap = Some type \<Longrightarrow> safe_for_derive (default_cap type ids sz dev) = safe_for_derive cap
theory Invocation_DP

lemma is_untyped_cap_derived[simp]:
  "is_untyped_cap (derived_cap cap) = (is_untyped_cap cap)" by (case_tac cap, simp_all add:derived_cap_def cap_type_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_untyped_cap (derived_cap cap) = is_untyped_cap cap
theory Invocation_DP

lemma cap_type_cdl_update_cnode_cap_data [simp]:
  "cap_type (cdl_update_cnode_cap_data cap data) = cap_type cap" by (clarsimp simp: cap_type_def cdl_update_cnode_cap_data_def split: cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_type (cdl_update_cnode_cap_data cap data) = cap_type cap
theory Invocation_DP

lemma cap_type_guard_update [simp]:
  "cap_type (guard_update cap data) = cap_type cap" by (clarsimp simp: cap_type_def guard_update_def split: cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_type (guard_update cap data) = cap_type cap
theory Invocation_DP

lemma cap_type_badge_update [simp]:
  "cap_type (badge_update data cap) = cap_type cap" by (clarsimp simp: badge_update_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_type (badge_update data cap) = cap_type cap