kings-crown/FVELER_Isabelle huggingface dataset:
theory KHeap_DP

lemma has_slots_simps:
  "has_slots (Tcb tcb)"
  "has_slots (CNode cnode)"
  "has_slots (AsidPool ap)"
  "has_slots (PageTable pt)"
  "has_slots (PageDirectory pd)"
  "\<not> has_slots Endpoint"
  "\<not> has_slots Notification"
  "\<not> has_slots (Frame f)"
  "\<not> has_slots Untyped" by (simp add: has_slots_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((has_slots (Tcb tcb) &&& has_slots (CNode cnode)) &&& has_slots (AsidPool ap) &&& has_slots (PageTable pt)) &&& (has_slots (PageDirectory pd) &&& \<not> has_slots Endpoint) &&& \<not> has_slots Notification &&& \<not> has_slots (Frame f) &&& \<not> has_slots Untyped
theory KHeap_DP

lemma reset_cap_asid_id:
  "reset_cap_asid cap = reset_cap_asid cap'
  \<Longrightarrow> cap = cap'
     \<or> (\<exists>a b c d e f. cap = FrameCap f a b c d e)
     \<or> (\<exists>a b c. cap = PageTableCap a b c)
     \<or> (\<exists>a b c. cap = PageDirectoryCap a b c)" by (case_tac cap, (clarsimp simp: 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> cap = cap' \<or> (\<exists>a b c d e f. cap = FrameCap f a b c d e) \<or> (\<exists>a b c. cap = PageTableCap a b c) \<or> (\<exists>a b c. cap = PageDirectoryCap a b c)
theory KHeap_DP

lemma reset_cap_asid_memory_cap [simp]:
  "\<not>is_memory_cap cap \<Longrightarrow> reset_cap_asid cap = cap" by (clarsimp simp: is_memory_cap_def reset_cap_asid_def
              split: cdl_cap.splits)

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

lemma is_memory_cap_reset_cap_asid [simp]:
  "is_memory_cap (reset_cap_asid cap) = is_memory_cap cap" by (clarsimp simp: is_memory_cap_def reset_cap_asid_def
              split: cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_memory_cap (reset_cap_asid cap) = is_memory_cap cap
theory KHeap_DP

lemma sep_map_c_any:
  "(p \<mapsto>c cap \<and>* R) s \<Longrightarrow> (p \<mapsto>c - \<and>* R) s" by (fastforce simp: sep_any_def sep_conj_exists)

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

lemma pure_extract:
  "\<lbrakk> <P \<and>* Q> s; pure P \<rbrakk> \<Longrightarrow> <P> s" by (fastforce simp: pure_def sep_state_projection_def sep_conj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cdl.lift (P \<and>* Q) s; pure P\<rbrakk> \<Longrightarrow> cdl.lift P s
theory KHeap_DP

lemma throw_on_none_rv:
  "\<lbrace>\<lambda>s. case x of Some y \<Rightarrow> P y s | otherwise \<Rightarrow> False\<rbrace> throw_on_none x \<lbrace>P\<rbrace>, \<lbrace>Q\<rbrace>" apply (clarsimp simp: throw_on_none_def split: option.splits) apply (wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. case x of None \<Rightarrow> False | Some y \<Rightarrow> P y s\<rbrace> throw_on_none x \<lbrace>P\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x2. x = Some x2 \<Longrightarrow> \<lbrace>P x2\<rbrace> returnOk x2 \<lbrace>P\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma oseq:
  "\<lbrakk> \<lbrace>P\<rbrace> gets_the f \<lbrace>Q\<rbrace>; \<forall>x. \<lbrace>Q x\<rbrace> gets_the $ g x \<lbrace>R\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> gets_the (f |>> g) \<lbrace>R\<rbrace>" apply (fastforce simp: gets_def fail_def get_def return_def gets_the_def obind_def valid_def split_def
    Let_def bind_def assert_opt_def split:option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> gets_the f \<lbrace>Q\<rbrace>; \<forall>x. \<lbrace>Q x\<rbrace> gets_the $ g x \<lbrace>R\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> gets_the (f >>= g) \<lbrace>R\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma hoare_ex_all:
     "(\<forall>x. \<lbrace>P x\<rbrace> f \<lbrace>Q\<rbrace>) = \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f \<lbrace>Q\<rbrace>" apply (rule iffI) apply (fastforce simp: valid_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<forall>x. \<lbrace>P x\<rbrace> f \<lbrace>Q\<rbrace>) = \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<forall>x. \<lbrace>P x\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f \<lbrace>Q\<rbrace>
 2. \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<forall>x. \<lbrace>P x\<rbrace> f \<lbrace>Q\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma sep_any_All: "\<lbrace><ptr \<mapsto>c - \<and>* R>\<rbrace> f \<lbrace>Q\<rbrace> = (\<forall>x. \<lbrace><ptr \<mapsto>c x \<and>* R>\<rbrace> f \<lbrace>Q\<rbrace>)" apply (clarsimp simp: sep_any_def sep_conj_exists hoare_ex_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (ptr \<mapsto>c - \<and>* R)\<rbrace> f \<lbrace>Q\<rbrace> = (\<forall>x. \<lbrace>cdl.lift (ptr \<mapsto>c x \<and>* R)\<rbrace> f \<lbrace>Q\<rbrace>) proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma gets_the_wpE:
  "\<lbrace>\<lambda>s. case (f s) of None \<Rightarrow> True | Some (Inl e) \<Rightarrow> E e s | Some (Inr r) \<Rightarrow> Q r s \<rbrace> gets_the f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" apply (clarsimp simp: validE_def) apply (wp) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. case f s of None \<Rightarrow> True | Some (Inl e) \<Rightarrow> E e s | Some (Inr r) \<Rightarrow> Q r s\<rbrace> gets_the f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. case f s of None \<Rightarrow> True | Some (Inl e) \<Rightarrow> E e s | Some (Inr r) \<Rightarrow> Q r s\<rbrace> gets_the f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. case f s of None \<Rightarrow> True | Some (Inl e) \<Rightarrow> E e s | Some (Inr r) \<Rightarrow> Q r s \<Longrightarrow> f s \<noteq> None \<longrightarrow> (case the (f s) of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s) proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma gets_the_invE : "\<lbrace>P\<rbrace> gets_the f \<lbrace>\<lambda>_. P\<rbrace>, -" apply (wp) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> gets_the f \<lbrace>\<lambda>_. P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> f s \<noteq> None \<longrightarrow> P s proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma return_rv :"\<lbrace>P r\<rbrace> return (Inr r) \<lbrace>\<lambda>rv s. P rv s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>" by (clarsimp simp: validE_def, wp, simp split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P r\<rbrace> return (Inr r) \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
theory KHeap_DP

lemma hoare_if_simp:
  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. (if x then (\<lambda>rv s. Q rv s) else (\<lambda>rv s. Q rv s)) rv s\<rbrace>" by (clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>if x then Q else Q\<rbrace>
theory KHeap_DP

lemma hoare_if_simpE:
  "\<lbrakk>\<And>x. Q x = R x; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-\<rbrakk>
  \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. (if x rv s then (\<lambda>s. Q rv s) else (\<lambda>s. R rv s)) s\<rbrace>,-" by (clarsimp simp: validE_R_def validE_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. Q x = R x; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. (if x rv s then Q rv else R rv) s\<rbrace>, -
theory KHeap_DP

lemma unless_wp_not: "\<lbrace>\<lambda>s. P s \<and> Q\<rbrace> unless Q f \<lbrace>\<lambda>_. P\<rbrace>" by (clarsimp simp: unless_def when_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P s \<and> Q\<rbrace> unless Q f \<lbrace>\<lambda>_. P\<rbrace>
theory KHeap_DP

lemma false_e_explode:
  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>\<lambda>_ _ . False\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>R\<rbrace>" by (fastforce simp: validE_def valid_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>_ _. False\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace>
theory KHeap_DP

lemma sep_any_map_c_imp: "(dest \<mapsto>c cap) s \<Longrightarrow> (dest \<mapsto>c -) s" by (fastforce simp: sep_any_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (dest \<mapsto>c cap) s \<Longrightarrow> (dest \<mapsto>c -) s
theory KHeap_DP

lemma object_slots_asid_reset:
  "object_slots (asid_reset obj) = reset_cap_asid \<circ>\<^sub>M (object_slots obj)" by (clarsimp simp: object_slots_def asid_reset_def update_slots_def
              split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_slots (asid_reset obj) = reset_cap_asid o_M object_slots obj
theory KHeap_DP

lemma reset_cap_asid_idem [simp]:
  "reset_cap_asid (reset_cap_asid cap) = reset_cap_asid cap" by (simp add: reset_cap_asid_def split: cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reset_cap_asid (reset_cap_asid cap) = reset_cap_asid cap
theory KHeap_DP

lemma opt_cap_sep_imp:
  "\<lbrakk><p \<mapsto>c cap \<and>* R> s\<rbrakk>
  \<Longrightarrow> \<exists>cap'. opt_cap p s = Some cap' \<and> reset_cap_asid cap' = reset_cap_asid cap" apply (clarsimp simp: opt_cap_def sep_map_c_conj Let_def) apply (clarsimp simp:  sep_map_c_def lift_def
    split_def
    sep_any_def sep_map_general_def slots_of_def
    sep_state_projection_def object_project_def
    object_slots_object_clean
    Let_unfold split:sep_state.splits option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdl.lift (p \<mapsto>c cap \<and>* R) s \<Longrightarrow> \<exists>cap'. opt_cap p s = Some cap' \<and> reset_cap_asid cap' = reset_cap_asid cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cdl.lift sep_heap s (fst p, Slot (snd p)) = Some (CDL_Cap (Some (reset_cap_asid cap))); R (SepState ((cdl.lift sep_heap s)((fst p, Slot (snd p)) := None)) (cdl.lift sep_irq_node s))\<rbrakk> \<Longrightarrow> \<exists>cap'. (case p of (obj_id, slot) \<Rightarrow> \<lambda>s. slots_of obj_id s slot) s = Some cap' \<and> reset_cap_asid cap' = reset_cap_asid cap proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma opt_cap_sep_any_imp:
  "\<lbrakk><dest \<mapsto>c - \<and>* R> s\<rbrakk> \<Longrightarrow> \<exists>cap. opt_cap (dest) s = Some cap" apply (clarsimp simp: sep_any_exist
    opt_cap_def sep_map_c_conj Let_def) apply (clarsimp simp:  sep_map_c_def lift_def
    split_def object_slots_object_clean
    sep_any_def sep_map_general_def slots_of_def
    sep_state_projection_def object_project_def
    Let_unfold split:sep_state.splits option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdl.lift (dest \<mapsto>c - \<and>* R) s \<Longrightarrow> \<exists>cap. opt_cap dest s = Some cap proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>R (SepState ((cdl.lift sep_heap s)((fst dest, Slot (snd dest)) := None)) (cdl.lift sep_irq_node s)); cdl.lift sep_heap s (fst dest, Slot (snd dest)) = Some (CDL_Cap (Some (reset_cap_asid x)))\<rbrakk> \<Longrightarrow> \<exists>cap. (case dest of (obj_id, slot) \<Rightarrow> \<lambda>s. slots_of obj_id s slot) s = Some cap proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma sep_f_size_opt_cnode:
  "\<lbrakk>< cap_object cnode_cap \<mapsto>f CNode (empty_cnode r) \<and>* R> s;
    (opt_cnode (cap_object cnode_cap) s) = Some obj \<rbrakk>
  \<Longrightarrow> r = cdl_cnode_size_bits obj" apply (clarsimp simp:sep_map_f_conj Let_def) apply (case_tac obj) apply (auto simp: intent_reset_def empty_cnode_def
    opt_cnode_def update_slots_def sep_state_projection_def
    object_wipe_slots_def
    object_project_def object_clean_def asid_reset_def
    split:cdl_cap.splits cdl_object.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cdl.lift (cap_object cnode_cap \<mapsto>f CNode (empty_cnode r) \<and>* R) s; opt_cnode (cap_object cnode_cap) s = Some obj\<rbrakk> \<Longrightarrow> r = cdl_cnode_size_bits obj proof (prove)
goal (1 subgoal):
 1. \<lbrakk>opt_cnode (cap_object cnode_cap) s = Some obj; cdl.lift sep_heap s (cap_object cnode_cap, Fields) = Some (CDL_Object (object_wipe_slots (object_clean (CNode (empty_cnode r))))); R (SepState ((cdl.lift sep_heap s)((cap_object cnode_cap, Fields) := None)) (cdl.lift sep_irq_node s))\<rbrakk> \<Longrightarrow> r = cdl_cnode_size_bits obj proof (prove)
goal (1 subgoal):
 1. \<And>cdl_cnode_caps cdl_cnode_size_bitsa. \<lbrakk>opt_cnode (cap_object cnode_cap) s = Some obj; cdl.lift sep_heap s (cap_object cnode_cap, Fields) = Some (CDL_Object (object_wipe_slots (object_clean (CNode (empty_cnode r))))); R (SepState ((cdl.lift sep_heap s)((cap_object cnode_cap, Fields) := None)) (cdl.lift sep_irq_node s)); obj = \<lparr>cdl_cnode_caps = cdl_cnode_caps, cdl_cnode_size_bits = cdl_cnode_size_bitsa\<rparr>\<rbrakk> \<Longrightarrow> r = cdl_cnode_size_bits obj proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma swap_parents_wp:
  "\<lbrace><R>\<rbrace>
   swap_parents src dest
  \<lbrace>\<lambda>_.  <R>\<rbrace>" by (wpsimp simp: swap_parents_def lift_def sep_state_projection_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift R\<rbrace> swap_parents src dest \<lbrace>\<lambda>_. cdl.lift R\<rbrace>
theory KHeap_DP

lemma insert_cap_orphan_wp:
   "\<lbrace><dest \<mapsto>c - \<and>* R>\<rbrace>
    insert_cap_orphan cap dest
   \<lbrace>\<lambda>_.<dest \<mapsto>c cap \<and>* R>\<rbrace>" apply (clarsimp simp: insert_cap_orphan_def) apply (wp set_cap_wp) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (dest \<mapsto>c - \<and>* R)\<rbrace> insert_cap_orphan cap dest \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c cap \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (dest \<mapsto>c - \<and>* R)\<rbrace> do old_cap <- get_cap dest;
y <- assert (old_cap = NullCap);
set_cap dest cap
od \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c cap \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cdl.lift (dest \<mapsto>c - \<and>* R) s \<Longrightarrow> opt_cap dest s \<noteq> None \<longrightarrow> the (opt_cap dest s) = NullCap \<longrightarrow> cdl.lift (dest \<mapsto>c - \<and>* R) s proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma set_parent_wp:
  "\<lbrace><P>\<rbrace>
    set_parent child parent
   \<lbrace>\<lambda>_.<P>\<rbrace>" apply (clarsimp simp: set_parent_def sep_state_projection_def) apply wp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift P\<rbrace> set_parent child parent \<lbrace>\<lambda>_. cdl.lift P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (SepState (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) (\<lambda>irq. Some (cdl_irq_node s irq)))\<rbrace> do cdt <- gets cdl_cdt;
y <- assert (cdt child = None);
modify (\<lambda>s. s\<lparr>cdl_cdt := (cdl_cdt s)(child \<mapsto> parent)\<rparr>)
od \<lbrace>\<lambda>_ s. P (SepState (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) (\<lambda>irq. Some (cdl_irq_node s irq)))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (SepState (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) (\<lambda>irq. Some (cdl_irq_node s irq))) \<Longrightarrow> cdl_cdt s child = None \<longrightarrow> P (SepState (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects (s\<lparr>cdl_cdt := (cdl_cdt s)(child \<mapsto> parent)\<rparr>) obj_id)) (\<lambda>irq. Some (cdl_irq_node (s\<lparr>cdl_cdt := (cdl_cdt s)(child \<mapsto> parent)\<rparr>) irq))) proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma not_untyped_cap_set_full:
  "\<lbrace>P and K (\<not> is_untyped_cap cap)\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>r. P\<rbrace>" apply (rule hoare_gen_asm) apply (clarsimp simp:set_untyped_cap_as_full_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and K (cap_type cap \<noteq> Some UntypedType)\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>r. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. cap_type cap \<noteq> Some UntypedType \<Longrightarrow> \<lbrace>P\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>r. P\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma insert_cap_child_wp:
 "\<lbrace><dest \<mapsto>c - \<and>* R> and K (\<not> is_untyped_cap cap)\<rbrace>
    insert_cap_child cap src dest
  \<lbrace>\<lambda>_. <dest \<mapsto>c cap \<and>* R>\<rbrace>" apply (clarsimp simp: insert_cap_child_def) apply (wp insert_cap_orphan_wp set_parent_wp set_cap_wp not_untyped_cap_set_full | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (dest \<mapsto>c - \<and>* R) and K (cap_type cap \<noteq> Some UntypedType)\<rbrace> insert_cap_child cap src dest \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c cap \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (dest \<mapsto>c - \<and>* R) and (\<lambda>y. cap_type cap \<noteq> Some UntypedType)\<rbrace> do src_cap <- get_cap src;
old_cap <- get_cap dest;
y <- assert (old_cap = NullCap);
y <- set_untyped_cap_as_full src_cap cap src;
y <- set_cap dest cap;
set_parent dest src
od \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c cap \<and>* R)\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma remove_parent_wp:
  "\<lbrace><P>\<rbrace>
   remove_parent obj
   \<lbrace>\<lambda>_.  <P>\<rbrace>" by (wpsimp simp: remove_parent_def lift_def sep_state_projection_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift P\<rbrace> remove_parent obj \<lbrace>\<lambda>_. cdl.lift P\<rbrace>
theory KHeap_DP

lemma get_cap_wp:
  "\<lbrace>P\<rbrace>
    get_cap obj
   \<lbrace>\<lambda>_. P\<rbrace>" apply (wp) apply (clarsimp simp: opt_cap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> get_cap obj \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> opt_cap obj s \<noteq> None \<longrightarrow> P s proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma get_cap_rv:
  "\<lbrace>\<lambda>s. <ptr \<mapsto>c cap \<and>* R> s \<and>
   (\<forall>c. ((reset_cap_asid c = reset_cap_asid cap ) \<longrightarrow> Q c s)) \<rbrace>
    get_cap ptr
   \<lbrace> Q \<rbrace>" apply (wp) apply (safe) apply (clarsimp simp: split_def dest!: opt_cap_sep_imp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cdl.lift (ptr \<mapsto>c cap \<and>* R) s \<and> (\<forall>c. reset_cap_asid c = reset_cap_asid cap \<longrightarrow> Q c s)\<rbrace> get_cap ptr \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cdl.lift (ptr \<mapsto>c cap \<and>* R) s \<and> (\<forall>c. reset_cap_asid c = reset_cap_asid cap \<longrightarrow> Q c s) \<Longrightarrow> opt_cap ptr s \<noteq> None \<longrightarrow> Q (the (opt_cap ptr s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>cdl.lift (ptr \<mapsto>c cap \<and>* R) s; \<forall>c. reset_cap_asid c = reset_cap_asid cap \<longrightarrow> Q c s; opt_cap ptr s = Some y\<rbrakk> \<Longrightarrow> Q (the (opt_cap ptr s)) s proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma get_cap_rv':
  "\<lbrace>\<lambda>s. <ptr \<mapsto>c cap \<and>* R> s \<and> Q cap s \<and> \<not>is_memory_cap cap\<rbrace>
    get_cap ptr
   \<lbrace>Q\<rbrace>" by (wp get_cap_rv, fastforce)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cdl.lift (ptr \<mapsto>c cap \<and>* R) s \<and> Q cap s \<and> \<not> is_memory_cap cap\<rbrace> get_cap ptr \<lbrace>Q\<rbrace>
theory KHeap_DP

lemma decode_tcb_invocation:
  "\<lbrace>P\<rbrace>decode_tcb_invocation cap cap_ref caps (TcbWriteRegistersIntent resume flags count regs)
  \<lbrace>\<lambda>_. P\<rbrace>" apply (clarsimp simp: decode_tcb_invocation_def) apply wp apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> decode_tcb_invocation cap cap_ref caps (TcbWriteRegistersIntent resume flags count regs) \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> returnOk (WriteRegisters (cap_object cap) resume [0] 0) \<sqinter> throw \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> (P and (\<lambda>s. P s \<and> True)) s proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma get_object_wp:
  "\<lbrace>P\<rbrace>
    get_object ptr
   \<lbrace>\<lambda>_. P\<rbrace>" apply (wp gets_the_inv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> get_object ptr \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal:
No subgoals!