kings-crown/FVELER_Isabelle huggingface dataset:
theory KHeap_DP

lemma empty_slot_wp:
  "\<lbrace><dest \<mapsto>c - \<and>* R>\<rbrace>
    empty_slot dest
   \<lbrace>\<lambda>_. <dest \<mapsto>c NullCap \<and>* R>\<rbrace>" apply (clarsimp simp: empty_slot_def sep_any_def sep_conj_exists) apply (subst hoare_ex_all [THEN sym], clarsimp) apply (wp set_cap_wp remove_parent_wp get_cap_rv[where R=R]) apply (rule conjI, assumption) apply safe apply (clarsimp simp: reset_cap_asid_def split: cdl_cap.splits) apply sep_solve done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (dest \<mapsto>c - \<and>* R)\<rbrace> empty_slot dest \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c NullCap \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>v. cdl.lift (dest \<mapsto>c v \<and>* R) s\<rbrace> do cap <- get_cap dest;
if cap = NullCap then return () else do remove_parent dest;
set_cap dest NullCap
od
od \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c NullCap \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>cdl.lift (dest \<mapsto>c x \<and>* R)\<rbrace> do cap <- get_cap dest;
if cap = NullCap then return () else do remove_parent dest;
set_cap dest NullCap
od
od \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c NullCap \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x s. cdl.lift (dest \<mapsto>c x \<and>* R) s \<Longrightarrow> cdl.lift (dest \<mapsto>c ?cap9 x \<and>* R) s \<and> (\<forall>c. reset_cap_asid c = reset_cap_asid (?cap9 x) \<longrightarrow> (c = NullCap \<longrightarrow> cdl.lift (dest \<mapsto>c NullCap \<and>* R) s) \<and> (c \<noteq> NullCap \<longrightarrow> cdl.lift (dest \<mapsto>c - \<and>* R) s)) proof (prove)
goal (1 subgoal):
 1. \<And>x s. cdl.lift (dest \<mapsto>c x \<and>* R) s \<Longrightarrow> \<forall>c. reset_cap_asid c = reset_cap_asid x \<longrightarrow> (c = NullCap \<longrightarrow> cdl.lift (dest \<mapsto>c NullCap \<and>* R) s) \<and> (c \<noteq> NullCap \<longrightarrow> cdl.lift (dest \<mapsto>c - \<and>* R) s) proof (prove)
goal (2 subgoals):
 1. \<And>x s c. \<lbrakk>cdl.lift (dest \<mapsto>c x \<and>* R) s; reset_cap_asid NullCap = reset_cap_asid x\<rbrakk> \<Longrightarrow> cdl.lift (dest \<mapsto>c NullCap \<and>* R) s
 2. \<And>x s c. \<lbrakk>cdl.lift (dest \<mapsto>c x \<and>* R) s; reset_cap_asid c = reset_cap_asid x; c \<noteq> NullCap\<rbrakk> \<Longrightarrow> cdl.lift (dest \<mapsto>c - \<and>* R) s proof (prove)
goal (1 subgoal):
 1. \<And>x s c. \<lbrakk>cdl.lift (dest \<mapsto>c x \<and>* R) s; reset_cap_asid c = reset_cap_asid x; c \<noteq> NullCap\<rbrakk> \<Longrightarrow> cdl.lift (dest \<mapsto>c - \<and>* R) s proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma invoke_cnode_insert_wp:
  "\<lbrace><dest \<mapsto>c - \<and>* R> and K (\<not> is_untyped_cap cap)\<rbrace>
     invoke_cnode (InsertCall cap src dest)
   \<lbrace>\<lambda>_. <dest \<mapsto>c cap \<and>* R>\<rbrace>" apply (rule hoare_gen_asm) apply (clarsimp simp: invoke_cnode_def) apply (wp insert_cap_sibling_wp insert_cap_child_wp) apply (clarsimp) 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> invoke_cnode (InsertCall cap src dest) \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c cap \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. cap_type cap \<noteq> Some UntypedType \<Longrightarrow> \<lbrace>cdl.lift (dest \<mapsto>c - \<and>* R)\<rbrace> invoke_cnode (InsertCall cap src dest) \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c cap \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. cap_type cap \<noteq> Some UntypedType \<Longrightarrow> \<lbrace>cdl.lift (dest \<mapsto>c - \<and>* R)\<rbrace> liftE (insert_cap_sibling cap src dest \<sqinter> insert_cap_child cap src dest) \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c cap \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cap_type cap \<noteq> Some UntypedType; cdl.lift (dest \<mapsto>c - \<and>* R) s\<rbrakk> \<Longrightarrow> (cdl.lift (dest \<mapsto>c - \<and>* R) and K (cap_type cap \<noteq> Some UntypedType) and (cdl.lift (dest \<mapsto>c - \<and>* R) and K (cap_type cap \<noteq> Some UntypedType))) s proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma invoke_cnode_move_cap:
  "\<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>,\<lbrace>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 (wp move_cap_wp) apply simp 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>, \<lbrace>Q\<rbrace> 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>v s. case v of Inl e \<Rightarrow> Q e s | Inr r \<Rightarrow> cdl.lift (dest \<mapsto>c cap' \<and>* src \<mapsto>c NullCap \<and>* R) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cdl.lift (dest \<mapsto>c - \<and>* src \<mapsto>c cap \<and>* R) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> invoke_cnode (MoveCall cap' src dest) \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q e s | Inr r \<Rightarrow> cdl.lift (dest \<mapsto>c cap' \<and>* src \<mapsto>c NullCap \<and>* R) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cdl.lift (dest \<mapsto>c - \<and>* src \<mapsto>c cap \<and>* R) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> move_cap cap' src dest \<lbrace>\<lambda>r. cdl.lift (dest \<mapsto>c cap' \<and>* src \<mapsto>c NullCap \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>cdl.lift (dest \<mapsto>c - \<and>* src \<mapsto>c cap \<and>* R) s; s = sa\<rbrakk> \<Longrightarrow> cdl.lift (dest \<mapsto>c - \<and>* src \<mapsto>c ?cap5 s \<and>* R) sa proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma invoke_cnode_rotate1_wp:
  "\<lbrace><dest \<mapsto>c cap1 \<and>* src \<mapsto>c cap2 \<and>* R> \<rbrace>
     invoke_cnode (RotateCall cap1 cap2 dest src dest)
   \<lbrace>\<lambda>_. <dest \<mapsto>c cap2 \<and>* src \<mapsto>c cap1 \<and>* R>\<rbrace>" apply (clarsimp simp: invoke_cnode_def) apply (wp sep_wand: swap_cap_wp) apply sep_solve done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (dest \<mapsto>c cap1 \<and>* src \<mapsto>c cap2 \<and>* R)\<rbrace> invoke_cnode (RotateCall cap1 cap2 dest src dest) \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c cap2 \<and>* src \<mapsto>c cap1 \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (dest \<mapsto>c cap1 \<and>* src \<mapsto>c cap2 \<and>* R)\<rbrace> liftE (swap_cap cap1 dest cap2 src) \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c cap2 \<and>* src \<mapsto>c cap1 \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cdl.lift (dest \<mapsto>c cap1 \<and>* src \<mapsto>c cap2 \<and>* R) s \<Longrightarrow> cdl.lift ((src \<mapsto>c cap2 \<and>* dest \<mapsto>c cap1) \<and>* (src \<mapsto>c cap1 \<and>* dest \<mapsto>c cap2 \<longrightarrow>* dest \<mapsto>c cap2 \<and>* src \<mapsto>c cap1 \<and>* R)) s proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma invoke_cnode_rotate2_wp:
   "(dest) \<noteq> (rnd) \<Longrightarrow>
  \<lbrace><dest \<mapsto>c cap1 \<and>* src \<mapsto>c cap2 \<and>*
    rnd \<mapsto>c - \<and>* R>\<rbrace>
     invoke_cnode (RotateCall cap1 cap2 dest src rnd)
  \<lbrace>\<lambda>_. <dest \<mapsto>c NullCap \<and>* src \<mapsto>c cap1 \<and>*
    rnd \<mapsto>c cap2 \<and>* R>\<rbrace>" apply (clarsimp simp: invoke_cnode_def) apply (wp sep_wand: move_cap_wp) apply sep_solve done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dest \<noteq> rnd \<Longrightarrow> \<lbrace>cdl.lift (dest \<mapsto>c cap1 \<and>* src \<mapsto>c cap2 \<and>* rnd \<mapsto>c - \<and>* R)\<rbrace> invoke_cnode (RotateCall cap1 cap2 dest src rnd) \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c NullCap \<and>* src \<mapsto>c cap1 \<and>* rnd \<mapsto>c cap2 \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. dest \<noteq> rnd \<Longrightarrow> \<lbrace>cdl.lift (dest \<mapsto>c cap1 \<and>* src \<mapsto>c cap2 \<and>* rnd \<mapsto>c - \<and>* R)\<rbrace> liftE (do y <- move_cap cap2 src rnd;
move_cap cap1 dest src
od) \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c NullCap \<and>* src \<mapsto>c cap1 \<and>* rnd \<mapsto>c cap2 \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>dest \<noteq> rnd; cdl.lift (dest \<mapsto>c cap1 \<and>* src \<mapsto>c cap2 \<and>* rnd \<mapsto>c - \<and>* R) s\<rbrakk> \<Longrightarrow> cdl.lift ((rnd \<mapsto>c - \<and>* src \<mapsto>c ?cap7) \<and>* (rnd \<mapsto>c cap2 \<and>* src \<mapsto>c NullCap \<longrightarrow>* (src \<mapsto>c - \<and>* dest \<mapsto>c ?cap9) \<and>* (src \<mapsto>c cap1 \<and>* dest \<mapsto>c NullCap \<longrightarrow>* dest \<mapsto>c NullCap \<and>* src \<mapsto>c cap1 \<and>* rnd \<mapsto>c cap2 \<and>* R))) s proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma get_cnode_wp [wp]:
  "\<lbrace> \<lambda>s. case (cdl_objects s a) of Some (CNode x) \<Rightarrow> P x s | _ \<Rightarrow> False \<rbrace>
     get_cnode a
   \<lbrace> P \<rbrace>" apply (clarsimp simp: get_cnode_def) apply (wp | wpc)+ apply (clarsimp split: cdl_object.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. case cdl_objects s a of None \<Rightarrow> False | Some (CNode x) \<Rightarrow> P x s | Some _ \<Rightarrow> False\<rbrace> get_cnode a \<lbrace>P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. case cdl_objects s a of None \<Rightarrow> False | Some (CNode x) \<Rightarrow> P x s | Some _ \<Rightarrow> False\<rbrace> do t <- get_object a;
case t of CNode cnode \<Rightarrow> return cnode | _ \<Rightarrow> fail
od \<lbrace>P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. case cdl_objects s a of None \<Rightarrow> False | Some (CNode x) \<Rightarrow> P x s | Some _ \<Rightarrow> False \<Longrightarrow> cdl_objects s a \<noteq> None \<longrightarrow> (the (cdl_objects s a) = Endpoint \<longrightarrow> True) \<and> (the (cdl_objects s a) = Notification \<longrightarrow> True) \<and> (\<forall>x. the (cdl_objects s a) = Tcb x \<longrightarrow> True) \<and> (\<forall>x. the (cdl_objects s a) = CNode x \<longrightarrow> P x s) \<and> (\<forall>x. the (cdl_objects s a) = AsidPool x \<longrightarrow> True) \<and> (\<forall>x. the (cdl_objects s a) = PageTable x \<longrightarrow> True) \<and> (\<forall>x. the (cdl_objects s a) = PageDirectory x \<longrightarrow> True) \<and> (\<forall>x. the (cdl_objects s a) = Frame x \<longrightarrow> True) \<and> (the (cdl_objects s a) = Untyped \<longrightarrow> True) \<and> (\<forall>x. the (cdl_objects s a) = IRQNode x \<longrightarrow> True) proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma resolve_address_bits_wp:
 "\<lbrace> \<lambda>s. P s \<rbrace>
  resolve_address_bits cnode_cap cap_ptr remaining_size
  \<lbrace> \<lambda>_. P \<rbrace>, \<lbrace> \<lambda>_. P \<rbrace>" apply (clarsimp simp: gets_the_resolve_cap[symmetric]) apply (wp) apply simp done

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

lemma resolve_cap_wp [wp]:
  "\<lbrace> P \<rbrace>
    gets_the (resolve_cap cnode_cap cap_ptr remaining_size)
  \<lbrace> \<lambda>_. P \<rbrace>" by (wp gets_the_inv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> gets_the (resolve_cap cnode_cap cap_ptr remaining_size) \<lbrace>\<lambda>_. P\<rbrace>
theory KHeap_DP

lemma lookup_slot_for_cnode_op_wpE:
  "\<lbrace>P\<rbrace>
    lookup_slot_for_cnode_op cnode_cap cap_ptr remaining_size
  \<lbrace>\<lambda>_. P \<rbrace>,\<lbrace>\<lambda>_. P \<rbrace>" apply (clarsimp simp: lookup_slot_for_cnode_op_def split_def) apply (wp) apply (clarsimp simp: gets_the_resolve_cap[symmetric]) apply (clarsimp simp: fault_to_except_def) apply (wp gets_the_wpE whenE_wp)+ apply (clarsimp split: option.splits split: sum.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> lookup_slot_for_cnode_op cnode_cap cap_ptr remaining_size \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> doE y <- whenE (remaining_size = 0 \<or> word_bits < remaining_size) throw;
p <- fault_to_except (resolve_address_bits cnode_cap cap_ptr remaining_size);
if snd p = 0 then returnOk (fst p) else throw
odE \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrace>?B2 y\<rbrace> fault_to_except (resolve_address_bits cnode_cap cap_ptr remaining_size) \<lbrace>\<lambda>p s. (snd p = 0 \<longrightarrow> P s) \<and> (snd p \<noteq> 0 \<longrightarrow> P s \<and> True)\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 2. \<lbrace>?Q1\<rbrace> whenE (remaining_size = 0 \<or> word_bits < remaining_size) throw \<lbrace>?B2\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>s. P s \<Longrightarrow> ?Q1 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?B2 ()\<rbrace> fault_to_except (gets_the (resolve_cap cnode_cap cap_ptr remaining_size)) \<lbrace>\<lambda>p s. (snd p = 0 \<longrightarrow> P s) \<and> (0 < snd p \<longrightarrow> P s)\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 2. \<lbrace>?Q1\<rbrace> whenE (remaining_size = 0 \<or> word_bits < remaining_size) throw \<lbrace>?B2\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>s. P s \<Longrightarrow> ?Q1 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?B2 ()\<rbrace> gets_the (resolve_cap cnode_cap cap_ptr remaining_size) <handle2> (\<lambda>x. throw) \<lbrace>\<lambda>p s. (snd p = 0 \<longrightarrow> P s) \<and> (0 < snd p \<longrightarrow> P s)\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 2. \<lbrace>?Q1\<rbrace> whenE (remaining_size = 0 \<or> word_bits < remaining_size) throw \<lbrace>?B2\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>s. P s \<Longrightarrow> ?Q1 s proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> (if remaining_size = 0 \<or> word_bits < remaining_size then \<lambda>s. P s \<and> True else (\<lambda>a. case resolve_cap cnode_cap cap_ptr remaining_size a of None \<Rightarrow> True | Some (Inl e) \<Rightarrow> P a \<and> True | Some (Inr r) \<Rightarrow> (snd r = 0 \<longrightarrow> P a) \<and> (0 < snd r \<longrightarrow> P a))) s proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma resolve_cap_rv:
 "\<lbrace>\<lambda>s. cap_object cnode_cap = c \<and> slot = offset cap_ptr r \<and>
    < c \<mapsto>f CNode (empty_cnode r) \<and>* (c, slot) \<mapsto>c cap \<and>* R> s \<and>
    one_lvl_lookup cnode_cap remaining_size r\<rbrace>
         gets_the (resolve_cap cnode_cap cap_ptr remaining_size)
  \<lbrace>\<lambda>rv s. (fst rv) = (c,slot) \<and> <
  c \<mapsto>f CNode (empty_cnode r)  \<and>* (c,slot) \<mapsto>c cap \<and>* R> s \<and> (snd rv) = 0\<rbrace>,\<lbrace>\<lambda>_ _ . True\<rbrace>" apply (wp resolve_cap_rv1 gets_the_invE) apply (clarsimp) apply (safe|fastforce)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cap_object cnode_cap = c \<and> slot = offset cap_ptr r \<and> cdl.lift (c \<mapsto>f CNode (empty_cnode r) \<and>* (c, slot) \<mapsto>c cap \<and>* R) s \<and> one_lvl_lookup cnode_cap remaining_size r\<rbrace> gets_the (resolve_cap cnode_cap cap_ptr remaining_size) \<lbrace>\<lambda>rv s. fst rv = (c, slot) \<and> cdl.lift (c \<mapsto>f CNode (empty_cnode r) \<and>* (c, slot) \<mapsto>c cap \<and>* R) s \<and> snd rv = 0\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cap_object cnode_cap = c \<and> slot = offset cap_ptr r \<and> cdl.lift (c \<mapsto>f CNode (empty_cnode r) \<and>* (c, slot) \<mapsto>c cap \<and>* R) s \<and> one_lvl_lookup cnode_cap remaining_size r \<Longrightarrow> (fst ((?c1, ?slot1), 0) = (c, slot) \<and> cdl.lift (c \<mapsto>f CNode (empty_cnode r) \<and>* (c, slot) \<mapsto>c cap \<and>* R) s \<and> snd ((?c1, ?slot1), 0) = 0) \<and> cap_object cnode_cap = ?c1 \<and> ?slot1 = offset cap_ptr ?r1 \<and> cdl.lift (?c1 \<mapsto>f CNode (empty_cnode ?r1) \<and>* (?c1, ?slot1) \<mapsto>c ?cap1 \<and>* ?R1) s \<and> one_lvl_lookup cnode_cap remaining_size ?r1 proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>c = cap_object cnode_cap; slot = offset cap_ptr r; cdl.lift (cap_object cnode_cap \<mapsto>f CNode (empty_cnode r) \<and>* (cap_object cnode_cap, offset cap_ptr r) \<mapsto>c cap \<and>* R) s; one_lvl_lookup cnode_cap remaining_size r\<rbrakk> \<Longrightarrow> ?c1 = cap_object cnode_cap \<and> ?slot1 = offset cap_ptr r \<and> cap_object cnode_cap = ?c1 \<and> ?slot1 = offset cap_ptr ?r1 \<and> cdl.lift (?c1 \<mapsto>f CNode (empty_cnode ?r1) \<and>* (?c1, ?slot1) \<mapsto>c ?cap1 \<and>* ?R1) s \<and> one_lvl_lookup cnode_cap remaining_size ?r1 proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma lookup_slot_for_cnode_op_rv':
    "\<lbrace>\<lambda>s. Q (c,slot) s \<and> cap_object cnode_cap = c \<and> slot = offset cap_ptr r \<and>
    < c \<mapsto>f CNode (empty_cnode r)  \<and>* (c, slot) \<mapsto>c cap \<and>* R> s \<and>
    one_lvl_lookup cnode_cap remaining_size r\<rbrace>
      lookup_slot_for_cnode_op cnode_cap cap_ptr remaining_size
     \<lbrace>\<lambda>rv s. Q rv s\<rbrace>,-" apply (clarsimp simp: lookup_slot_for_cnode_op_def gets_the_resolve_cap[symmetric] split_def fault_to_except_def) apply (wp resolve_cap_rv1 whenE_wp) apply (fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q (c, slot) s \<and> cap_object cnode_cap = c \<and> slot = offset cap_ptr r \<and> cdl.lift (c \<mapsto>f CNode (empty_cnode r) \<and>* (c, slot) \<mapsto>c cap \<and>* R) s \<and> one_lvl_lookup cnode_cap remaining_size r\<rbrace> lookup_slot_for_cnode_op cnode_cap cap_ptr remaining_size \<lbrace>Q\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q (c, slot) s \<and> cap_object cnode_cap = c \<and> slot = offset cap_ptr r \<and> cdl.lift (c \<mapsto>f CNode (empty_cnode r) \<and>* (c, slot) \<mapsto>c cap \<and>* R) s \<and> one_lvl_lookup cnode_cap remaining_size r\<rbrace> doE y <- whenE (remaining_size = 0 \<or> word_bits < remaining_size) throw;
p <- gets_the (resolve_cap cnode_cap cap_ptr remaining_size) <handle2> (\<lambda>x. throw);
if snd p = 0 then returnOk (fst p) else throw
odE \<lbrace>Q\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. Q (c, slot) s \<and> cap_object cnode_cap = c \<and> slot = offset cap_ptr r \<and> cdl.lift (c \<mapsto>f CNode (empty_cnode r) \<and>* (c, slot) \<mapsto>c cap \<and>* R) s \<and> one_lvl_lookup cnode_cap remaining_size r \<Longrightarrow> (if remaining_size = 0 \<or> word_bits < remaining_size then \<lambda>s. True \<and> True else (\<lambda>s. True \<and> ((snd ((?c14 (), ?slot14 ()), 0) = 0 \<longrightarrow> Q (fst ((?c14 (), ?slot14 ()), 0)) s) \<and> (snd ((?c14 (), ?slot14 ()), 0) \<noteq> 0 \<longrightarrow> True)) \<and> cap_object cnode_cap = ?c14 () \<and> ?slot14 () = offset cap_ptr (?r14 ()) \<and> cdl.lift (?c14 () \<mapsto>f CNode (empty_cnode (?r14 ())) \<and>* (?c14 (), ?slot14 ()) \<mapsto>c ?cap14 () \<and>* ?R14 ()) s \<and> one_lvl_lookup cnode_cap remaining_size (?r14 ()))) s proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma reset_cap_asid_cap_has_object:
  "reset_cap_asid cap = reset_cap_asid cap'
  \<Longrightarrow> cap_has_object cap = cap_has_object cap'" apply (frule reset_cap_asid_id) apply (safe, (clarsimp simp: reset_cap_asid_def cap_has_object_def
                        split: cdl_cap.splits)+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reset_cap_asid cap = reset_cap_asid cap' \<Longrightarrow> cap_has_object cap = cap_has_object cap' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reset_cap_asid cap = reset_cap_asid cap'; 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)\<rbrakk> \<Longrightarrow> cap_has_object cap = cap_has_object cap' proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma cap_object_reset_cap_asid:
  "\<lbrakk>reset_cap_asid cap = reset_cap_asid cap'\<rbrakk> \<Longrightarrow> cap_object cap = cap_object cap'" apply (case_tac cap',simp_all add:reset_cap_asid_def split:cdl_cap.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reset_cap_asid cap = reset_cap_asid cap' \<Longrightarrow> cap_object cap = cap_object cap' proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma cap_type_reset_cap_asid[simp]:
  "cap_type (reset_cap_asid cap) = cap_type cap" by (clarsimp simp: reset_cap_asid_def split: cdl_cap.splits)

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

lemma cap_guard_reset_cap_asid:
  "is_cnode_cap cap \<Longrightarrow> cap_guard (reset_cap_asid cap) = cap_guard cap"
  "is_cnode_cap cap \<Longrightarrow> cap_guard_size (reset_cap_asid cap) = cap_guard_size cap" by (case_tac cap,simp_all add:reset_cap_asid_def cap_guard_def)+

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