kings-crown/FVELER_Isabelle huggingface dataset:
theory Invocation_DP

lemma cap_type_update_cap_data_det [simp]:
  "cap_type (update_cap_data_det data cap) = cap_type cap" by (auto simp: update_cap_data_det_def
          split: cdl_cap.splits)

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

lemma safe_for_derive_not_untyped:
  "safe_for_derive cap \<Longrightarrow> \<not> is_untyped_cap cap" by (clarsimp simp: safe_for_derive_def cap_type_def
              split: cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. safe_for_derive cap \<Longrightarrow> cap_type cap \<noteq> Some UntypedType
theory Invocation_DP

lemma mark_tcb_intent_error_no_error:
  "\<lbrace>\<top> \<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>r s. \<not> tcb_has_error thread_ptr s \<longrightarrow> Q r s\<rbrace>" apply (simp add:mark_tcb_intent_error_def tcb_has_error_def) apply (simp add:object_at_def update_thread_def
    gets_the_def gets_def ) apply (wp|wpc|simp add:set_object_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>r s. \<not> tcb_has_error thread_ptr s \<longrightarrow> Q r s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> update_thread thread_ptr (\<lambda>t. t\<lparr>cdl_tcb_intent := cdl_tcb_intent t\<lparr>cdl_intent_error := True\<rparr>\<rparr>) \<lbrace>\<lambda>r s. \<not> object_at (\<lambda>obj. case obj of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False) thread_ptr s \<longrightarrow> Q () s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do t <- do s <- get;
assert_opt (cdl_objects s thread_ptr)
od;
case t of Tcb tcb \<Rightarrow> set_object thread_ptr (Tcb (tcb\<lparr>cdl_tcb_intent := cdl_tcb_intent tcb\<lparr>cdl_intent_error := True\<rparr>\<rparr>)) | _ \<Rightarrow> fail
od \<lbrace>\<lambda>r s. (\<forall>object. cdl_objects s thread_ptr = Some object \<longrightarrow> \<not> (case object of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<longrightarrow> Q () s\<rbrace> proof (prove)
goal:
No subgoals!
theory Invocation_DP

lemma mark_tcb_intent_error_no_error':
  "\<lbrace>\<top> \<rbrace> mark_tcb_intent_error thread_ptr False \<lbrace>\<lambda>r s. \<not> tcb_has_error thread_ptr s\<rbrace>" apply (simp add:mark_tcb_intent_error_def update_thread_def
    gets_the_def set_object_def) apply (wp|wpc|simp add:set_object_def)+ apply (clarsimp simp: tcb_has_error_def object_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> mark_tcb_intent_error thread_ptr False \<lbrace>\<lambda>r s. \<not> tcb_has_error thread_ptr s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do t <- gets (\<lambda>s. cdl_objects s thread_ptr) >>= assert_opt;
case t of Tcb tcb \<Rightarrow> set_object thread_ptr (Tcb (tcb\<lparr>cdl_tcb_intent := cdl_tcb_intent tcb\<lparr>cdl_intent_error := False\<rparr>\<rparr>)) | _ \<Rightarrow> fail
od \<lbrace>\<lambda>r s. \<not> tcb_has_error thread_ptr s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<exists>y. cdl_objects s thread_ptr = Some y) \<longrightarrow> (\<forall>x. the (cdl_objects s thread_ptr) = Tcb x \<longrightarrow> \<not> tcb_has_error thread_ptr (s\<lparr>cdl_objects := \<lambda>a. if a = thread_ptr then Some (Tcb (x\<lparr>cdl_tcb_intent := cdl_tcb_intent x\<lparr>cdl_intent_error := False\<rparr>\<rparr>)) else cdl_objects s a\<rparr>)) proof (prove)
goal:
No subgoals!
theory Invocation_DP

lemma thread_has_error_wp:
  "\<lbrace> \<lambda>s. Q (tcb_has_error thread_ptr s) s\<rbrace>
  thread_has_error thread_ptr \<lbrace>\<lambda>has_error s. Q has_error s\<rbrace>" apply (clarsimp simp:thread_has_error_def get_thread_def
    gets_the_def tcb_has_error_def) apply (wp|wpc)+ apply (clarsimp simp: object_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q (tcb_has_error thread_ptr s) s\<rbrace> thread_has_error thread_ptr \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q (object_at (\<lambda>obj. case obj of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False) thread_ptr s) s\<rbrace> do tcb <- do t <- gets (\<lambda>s. cdl_objects s thread_ptr) >>= assert_opt;
case t of Tcb tcb \<Rightarrow> return tcb | _ \<Rightarrow> fail
od;
return (cdl_intent_error (cdl_tcb_intent tcb))
od \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. Q (object_at (\<lambda>obj. case obj of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False) thread_ptr s) s \<Longrightarrow> cdl_objects s thread_ptr \<noteq> None \<longrightarrow> (the (cdl_objects s thread_ptr) = Endpoint \<longrightarrow> True) \<and> (the (cdl_objects s thread_ptr) = Notification \<longrightarrow> True) \<and> (\<forall>x. the (cdl_objects s thread_ptr) = Tcb x \<longrightarrow> Q (cdl_intent_error (cdl_tcb_intent x)) s) \<and> (\<forall>x. the (cdl_objects s thread_ptr) = CNode x \<longrightarrow> True) \<and> (\<forall>x. the (cdl_objects s thread_ptr) = AsidPool x \<longrightarrow> True) \<and> (\<forall>x. the (cdl_objects s thread_ptr) = PageTable x \<longrightarrow> True) \<and> (\<forall>x. the (cdl_objects s thread_ptr) = PageDirectory x \<longrightarrow> True) \<and> (\<forall>x. the (cdl_objects s thread_ptr) = Frame x \<longrightarrow> True) \<and> (the (cdl_objects s thread_ptr) = Untyped \<longrightarrow> True) \<and> (\<forall>x. the (cdl_objects s thread_ptr) = IRQNode x \<longrightarrow> True) proof (prove)
goal:
No subgoals!
theory Invocation_DP

lemma invoke_cnode_insert_cap':
  "incall = InsertCall cap src_slot dest_slot
  \<Longrightarrow> \<lbrace>\<lambda>s. < dest_slot \<mapsto>c - \<and>* R> s \<and> \<not> is_untyped_cap (cap_of_insert_call (InvokeCNode incall))  \<rbrace>
  invoke_cnode incall
  \<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
                simp: cap_of_insert_call_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. incall = InsertCall cap src_slot dest_slot \<Longrightarrow> \<lbrace>\<lambda>s. cdl.lift (dest_slot \<mapsto>c - \<and>* R) s \<and> cap_type (cap_of_insert_call (InvokeCNode incall)) \<noteq> Some UntypedType\<rbrace> invoke_cnode incall \<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. incall = InsertCall cap src_slot dest_slot \<Longrightarrow> \<lbrace>\<lambda>s. cdl.lift (dest_slot \<mapsto>c - \<and>* R) s \<and> cap_type (cap_of_insert_call (InvokeCNode (InsertCall cap src_slot dest_slot))) \<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. \<lbrakk>incall = InsertCall cap src_slot dest_slot; cdl.lift (dest_slot \<mapsto>c - \<and>* R) s \<and> cap_type (cap_of_insert_call (InvokeCNode (InsertCall cap src_slot dest_slot))) \<noteq> Some UntypedType\<rbrakk> \<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>incall = InsertCall cap src_slot dest_slot; cdl.lift (dest_slot \<mapsto>c - \<and>* R) s; cap_type (cap_of_insert_call (InvokeCNode (InsertCall cap src_slot dest_slot))) \<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 object_to_sep_state_slot:
  "object_to_sep_state (fst ptr) obj {Slot (snd ptr)} = [(fst ptr, Slot (snd ptr)) \<mapsto>
  (CDL_Cap ((reset_cap_asid \<circ>\<^sub>M object_slots obj) (snd ptr)))]" apply (rule ext) apply (clarsimp simp:object_to_sep_state_def
    object_project_slot object_slots_object_clean
    split:if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_to_sep_state (fst ptr) obj {Slot (snd ptr)} = [(fst ptr, Slot (snd ptr)) \<mapsto> CDL_Cap ((reset_cap_asid o_M object_slots obj) (snd ptr))] proof (prove)
goal (1 subgoal):
 1. \<And>x. object_to_sep_state (fst ptr) obj {Slot (snd ptr)} x = [(fst ptr, Slot (snd ptr)) \<mapsto> CDL_Cap ((reset_cap_asid o_M object_slots obj) (snd ptr))] x proof (prove)
goal:
No subgoals!
theory Invocation_DP

lemma reset_cap_asid_update_cap_data:
  "reset_cap_asid (update_cap_data_det data dcap)
  = update_cap_data_det data (reset_cap_asid dcap)" by (case_tac dcap,simp_all add:reset_cap_asid_def badge_update_def
    guard_update_def update_cap_badge_def
    update_cap_data_det_def)

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

lemma reset_cap_asid_derived:
  "reset_cap_asid a = reset_cap_asid b
  \<Longrightarrow> reset_cap_asid (derived_cap a) = reset_cap_asid (derived_cap b)" apply (frule reset_cap_asid_id) apply (safe, (case_tac b, simp_all add: reset_cap_asid_def derived_cap_simps)+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reset_cap_asid a = reset_cap_asid b \<Longrightarrow> reset_cap_asid (derived_cap a) = reset_cap_asid (derived_cap b) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reset_cap_asid a = reset_cap_asid b; a = b \<or> (\<exists>aa b c d e f. a = FrameCap f aa b c d e) \<or> (\<exists>aa b c. a = PageTableCap aa b c) \<or> (\<exists>aa b c. a = PageDirectoryCap aa b c)\<rbrakk> \<Longrightarrow> reset_cap_asid (derived_cap a) = reset_cap_asid (derived_cap b) proof (prove)
goal:
No subgoals!
theory Invocation_DP

lemma reset_cap_asid_update_cap_rights:
  "reset_cap_asid (update_cap_rights rights b) = update_cap_rights rights (reset_cap_asid b)" by (case_tac b,simp_all add:update_cap_rights_def reset_cap_asid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reset_cap_asid (update_cap_rights rights b) = update_cap_rights rights (reset_cap_asid b)
theory Retype_DP

lemma pick_rev:
  assumes "target_object_ids = map (\<lambda>x. {x}) ids"
  shows "ids = map (\<lambda>x. pick x) target_object_ids" unfolding assms by (induct ids) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ids = map pick target_object_ids proof (prove)
goal (1 subgoal):
 1. ids = map pick (map (\<lambda>x. {x}) ids)
theory Retype_DP

lemma nonempty_pick_in:
  "a\<noteq>{} \<Longrightarrow> pick a \<in> a" by (metis all_not_in_conv someI_ex)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a \<noteq> {} \<Longrightarrow> pick a \<in> a
theory Retype_DP

lemma map_zip_first_simp:
  "length x = length y \<Longrightarrow> map (\<lambda>a. g (fst a)) (zip x y) = map g x" proof (induct x arbitrary: y) case Nil show ?case by simp next case Cons show ?case using local.Cons.prems apply (case_tac y) apply clarsimp+ apply (simp add:local.Cons.hyps) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length x = length y \<Longrightarrow> map (\<lambda>a. g (fst a)) (zip x y) = map g x proof (state)
goal (2 subgoals):
 1. \<And>y. length [] = length y \<Longrightarrow> map (\<lambda>a. g (fst a)) (zip [] y) = map g []
 2. \<And>a x y. \<lbrakk>\<And>y. length x = length y \<Longrightarrow> map (\<lambda>a. g (fst a)) (zip x y) = map g x; length (a # x) = length y\<rbrakk> \<Longrightarrow> map (\<lambda>a. g (fst a)) (zip (a # x) y) = map g (a # x) proof (state)
this:
length [] = length y

goal (2 subgoals):
 1. \<And>y. length [] = length y \<Longrightarrow> map (\<lambda>a. g (fst a)) (zip [] y) = map g []
 2. \<And>a x y. \<lbrakk>\<And>y. length x = length y \<Longrightarrow> map (\<lambda>a. g (fst a)) (zip x y) = map g x; length (a # x) = length y\<rbrakk> \<Longrightarrow> map (\<lambda>a. g (fst a)) (zip (a # x) y) = map g (a # x) proof (prove)
goal (1 subgoal):
 1. map (\<lambda>a. g (fst a)) (zip [] y) = map g [] proof (state)
this:
map (\<lambda>a. g (fst a)) (zip [] y) = map g []

goal (1 subgoal):
 1. \<And>a x y. \<lbrakk>\<And>y. length x = length y \<Longrightarrow> map (\<lambda>a. g (fst a)) (zip x y) = map g x; length (a # x) = length y\<rbrakk> \<Longrightarrow> map (\<lambda>a. g (fst a)) (zip (a # x) y) = map g (a # x) proof (state)
goal (1 subgoal):
 1. \<And>a x y. \<lbrakk>\<And>y. length x = length y \<Longrightarrow> map (\<lambda>a. g (fst a)) (zip x y) = map g x; length (a # x) = length y\<rbrakk> \<Longrightarrow> map (\<lambda>a. g (fst a)) (zip (a # x) y) = map g (a # x) proof (state)
this:
length x_ = length ?y \<Longrightarrow> map (\<lambda>a. g (fst a)) (zip x_ ?y) = map g x_
length (a_ # x_) = length y

goal (1 subgoal):
 1. \<And>a x y. \<lbrakk>\<And>y. length x = length y \<Longrightarrow> map (\<lambda>a. g (fst a)) (zip x y) = map g x; length (a # x) = length y\<rbrakk> \<Longrightarrow> map (\<lambda>a. g (fst a)) (zip (a # x) y) = map g (a # x) proof (prove)
goal (1 subgoal):
 1. map (\<lambda>a. g (fst a)) (zip (a_ # x_) y) = map g (a_ # x_) proof (prove)
using this:
length (a_ # x_) = length y

goal (1 subgoal):
 1. map (\<lambda>a. g (fst a)) (zip (a_ # x_) y) = map g (a_ # x_) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length (a_ # x_) = length y; y = []\<rbrakk> \<Longrightarrow> map (\<lambda>a. g (fst a)) (zip (a_ # x_) y) = map g (a_ # x_)
 2. \<And>aa list. \<lbrakk>length (a_ # x_) = length y; y = aa # list\<rbrakk> \<Longrightarrow> map (\<lambda>a. g (fst a)) (zip (a_ # x_) y) = map g (a_ # x_) proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>length x_ = length list; y = a # list\<rbrakk> \<Longrightarrow> map (\<lambda>a. g (fst a)) (zip x_ list) = map g x_ proof (prove)
goal:
No subgoals! proof (state)
this:
map (\<lambda>a. g (fst a)) (zip (a_ # x_) y) = map g (a_ # x_)

goal:
No subgoals!
theory Retype_DP

lemma reset_cap_asid_untyped_cap_eqD:
  "reset_cap_asid c = UntypedCap dev a b
  \<Longrightarrow> c = UntypedCap dev a b" by (simp add:reset_cap_asid_def split:cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reset_cap_asid c = UntypedCap dev a b \<Longrightarrow> c = UntypedCap dev a b
theory Retype_DP

lemma mapME_x_singleton:
  "mapME_x f [a] = (f a >>= return)" by (simp add:mapME_x_def sequenceE_x_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapME_x f [a] = f a >>= return
theory Retype_DP

lemma mapME_singleton:
  "mapME f [a] = (doE x \<leftarrow> f a; returnOk [x] odE)" by (simp add:mapME_def sequenceE_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapME f [a] = doE x <- f a;
returnOk [x]
odE
theory Retype_DP

lemma decode_untyped_invocation_rvu:
  "\<lbrakk>nt \<noteq> UntypedType\<rbrakk> \<Longrightarrow>
  \<lbrace> (\<lambda>s. Q (InvokeUntyped (Retype ref nt (unat ts)
    [(cap_object cnode_cap, unat node_offset)]
    (has_children ref s) (Suc 0))) s)
  and R and K(is_cnode_cap cnode_cap)\<rbrace>
  decode_invocation (UntypedCap dev tot_range free_range) ref [(cnode_cap,cnode_ref)]
  (UntypedIntent (UntypedRetypeIntent nt ts node_index 0 node_offset 1))
  \<lbrace>\<lambda>r. Q r\<rbrace>, \<lbrace>\<lambda>r. R\<rbrace>" apply (simp add:decode_invocation_def
    get_untyped_intent_def throw_opt_def
    get_index_def throw_on_none_def
    decode_untyped_invocation_def mapME_x_singleton) apply (rule hoare_pre) apply (wp unlessE_wp
    lookup_slot_for_cnode_op_rvu' | wpc | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. nt \<noteq> UntypedType \<Longrightarrow> \<lbrace>(\<lambda>s. Q (InvokeUntyped (Retype ref nt (unat ts) [(cap_object cnode_cap, unat node_offset)] (has_children ref s) (Suc 0))) s) and R and K (is_cnode_cap cnode_cap)\<rbrace> decode_invocation (UntypedCap dev tot_range free_range) ref [(cnode_cap, cnode_ref)] (UntypedIntent (UntypedRetypeIntent nt ts node_index 0 node_offset 1)) \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r. R\<rbrace> proof (prove)
goal (1 subgoal):
 1. nt \<noteq> UntypedType \<Longrightarrow> \<lbrace>(\<lambda>s. Q (InvokeUntyped (Retype ref nt (unat ts) [(cap_object cnode_cap, unat node_offset)] (has_children ref s) (Suc 0))) s) and R and (\<lambda>y. is_cnode_cap cnode_cap)\<rbrace> liftME InvokeUntyped (doE y <- unlessE (is_cnode_cap cnode_cap) throw;
y <- ensure_empty (cap_object cnode_cap, unat node_offset);
s <- liftE get;
returnOk (Retype ref nt (unat ts) [(cap_object cnode_cap, unat node_offset)] (has_children ref s) (Suc 0))
odE \<sqinter> throw) \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r. R\<rbrace> proof (prove)
goal (2 subgoals):
 1. nt \<noteq> UntypedType \<Longrightarrow> \<lbrace>?Q4\<rbrace> liftME InvokeUntyped (doE y <- unlessE (is_cnode_cap cnode_cap) throw;
y <- ensure_empty (cap_object cnode_cap, unat node_offset);
s <- liftE get;
returnOk (Retype ref nt (unat ts) [(cap_object cnode_cap, unat node_offset)] (has_children ref s) (Suc 0))
odE \<sqinter> throw) \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r. R\<rbrace>
 2. \<And>s. \<lbrakk>nt \<noteq> UntypedType; ((\<lambda>s. Q (InvokeUntyped (Retype ref nt (unat ts) [(cap_object cnode_cap, unat node_offset)] (has_children ref s) (Suc 0))) s) and R and (\<lambda>y. is_cnode_cap cnode_cap)) s\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal:
No subgoals!
theory Retype_DP

lemma set_parent_has_children[wp]:
  "\<lbrace>\<top>\<rbrace> set_parent cref uref \<lbrace>\<lambda>r. has_children uref\<rbrace>" apply (clarsimp simp add:set_parent_def simpler_modify_def
    valid_def has_children_def gets_def assert_def bind_def
    get_def return_def fail_def) apply (case_tac cref) apply (auto simp:is_cdt_parent_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> set_parent cref uref \<lbrace>\<lambda>r. has_children uref\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cdl_cdt s cref = None \<Longrightarrow> \<exists>a b. is_cdt_parent (s\<lparr>cdl_cdt := (cdl_cdt s)(cref \<mapsto> uref)\<rparr>) uref (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>cdl_cdt s cref = None; cref = (a, b)\<rbrakk> \<Longrightarrow> \<exists>a b. is_cdt_parent (s\<lparr>cdl_cdt := (cdl_cdt s)(cref \<mapsto> uref)\<rparr>) uref (a, b) proof (prove)
goal:
No subgoals!
theory Retype_DP

lemma create_cap_has_children[wp]:
  "\<lbrace>\<top>\<rbrace> create_cap new_type sz uref slot dev \<lbrace>\<lambda>r. has_children uref\<rbrace>" apply (clarsimp simp :create_cap_def split_def) apply wpsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> create_cap new_type sz uref slot dev \<lbrace>\<lambda>r. has_children uref\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do old_cap <- get_cap (fst dev);
y <- assert (old_cap = NullCap);
y <- set_cap (fst dev) (default_cap new_type (snd dev) sz slot);
set_parent (fst dev) uref
od \<lbrace>\<lambda>r. has_children uref\<rbrace> proof (prove)
goal:
No subgoals!
theory Retype_DP

lemma mark_tcb_intent_error_has_children[wp]:
  "\<lbrace>\<lambda>s. P (has_children ptr s)\<rbrace>
   mark_tcb_intent_error cur_thread b
   \<lbrace>\<lambda>rv s. P (has_children ptr s)\<rbrace>" by (wpsimp simp: has_children_def is_cdt_parent_def mark_tcb_intent_error_def update_thread_def
                   set_object_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (has_children ptr s)\<rbrace> mark_tcb_intent_error cur_thread b \<lbrace>\<lambda>rv s. P (has_children ptr s)\<rbrace>
theory Retype_DP

lemma corrupt_ipc_buffer_has_children[wp]:
  "\<lbrace>\<lambda>s. P (has_children ptr s)\<rbrace>
  corrupt_ipc_buffer cur_thread b
  \<lbrace>\<lambda>rv s. P (has_children ptr s)\<rbrace>" by (simp add: has_children_def is_cdt_parent_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (has_children ptr s)\<rbrace> corrupt_ipc_buffer cur_thread b \<lbrace>\<lambda>rv s. P (has_children ptr s)\<rbrace>
theory Retype_DP

lemma update_thread_intent_has_children[wp]:
  "\<lbrace>\<lambda>s. P (has_children ptr s)\<rbrace>
  update_thread cur_thread (cdl_tcb_intent_update f)
  \<lbrace>\<lambda>rv s. P (has_children ptr s)\<rbrace>" by (simp add:has_children_def is_cdt_parent_def | wp )+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (has_children ptr s)\<rbrace> update_thread cur_thread (cdl_tcb_intent_update f) \<lbrace>\<lambda>rv s. P (has_children ptr s)\<rbrace>
theory Retype_DP

lemma hoare_drop_impE_R:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. R r s \<longrightarrow> Q s\<rbrace>, -" apply (rule validE_validE_R) apply (clarsimp simp:validE_def valid_def) apply (case_tac a,simp_all) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. R r s \<longrightarrow> Q s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. R r s \<longrightarrow> Q s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, x) \<Rightarrow> Q x); P s; (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> case a of Inl e \<Rightarrow> True | Inr r \<Rightarrow> R r b \<longrightarrow> Q b proof (prove)
goal (1 subgoal):
 1. \<And>s a b ba. \<lbrakk>\<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, x) \<Rightarrow> Q x); P s; (Inr ba, b) \<in> fst (f s); a = Inr ba\<rbrakk> \<Longrightarrow> R ba b \<longrightarrow> Q b proof (prove)
goal:
No subgoals!
theory Retype_DP

lemma set_parent_other:
  "\<lbrace>\<lambda>s. cdl_cdt s child = Some parent\<rbrace> set_parent dest uref \<lbrace>\<lambda>_ s. cdl_cdt s child = Some parent\<rbrace>" apply (simp add:set_parent_def) apply wp apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cdl_cdt s child = Some parent\<rbrace> set_parent dest uref \<lbrace>\<lambda>_ s. cdl_cdt s child = Some parent\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cdl_cdt s child = Some parent\<rbrace> do cdt <- gets cdl_cdt;
y <- assert (cdt dest = None);
modify (\<lambda>s. s\<lparr>cdl_cdt := (cdl_cdt s)(dest \<mapsto> uref)\<rparr>)
od \<lbrace>\<lambda>_ s. cdl_cdt s child = Some parent\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cdl_cdt s child = Some parent \<Longrightarrow> cdl_cdt s dest = None \<longrightarrow> cdl_cdt (s\<lparr>cdl_cdt := (cdl_cdt s)(dest \<mapsto> uref)\<rparr>) child = Some parent proof (prove)
goal:
No subgoals!
theory Retype_DP

lemma object_at_cdl_cdt[simp]:
  "object_at P ptr (s\<lparr>cdl_cdt := a\<rparr>)
   = object_at P ptr s" by (simp add: object_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_at P ptr (s\<lparr>cdl_cdt := a\<rparr>) = object_at P ptr s