theory KHeap_DP

lemma resolve_cap_u_nf:
   "\<lbrace>\<lambda>s. Q (((cap_object cnode_cap), offset cap_ptr r), 0) s \<and>
         < user_pointer_at (r,r_s) cnode_cap cap_ptr cap  \<and>* R> s \<rbrace>
         gets_the (resolve_cap cnode_cap cap_ptr r_s)
    \<lbrace>Q\<rbrace>,\<lbrace>Q'\<rbrace>" apply (wp gets_the_wpE) apply (clarsimp simp: user_pointer_at_def Let_unfold guard_equal_def one_lvl_lookup_def
                        offset_def sep.mult_assoc) apply (clarsimp simp: split_def split: sum.splits option.splits) apply (safe) apply (simp add: split_def resolve_cap.simps split: if_split_asm) apply (simp add: obind_def split:option.splits) apply (sep_drule (direct) sep_f_size_opt_cnode) apply (fastforce)+ apply (simp add: split_def resolve_cap.simps split: if_split_asm) apply (simp add: obind_def split:option.splits) apply (sep_drule (direct) sep_f_size_opt_cnode) apply (fastforce split: if_split_asm)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q ((cap_object cnode_cap, offset cap_ptr r), 0) s \<and> cdl.lift (\<box> (r, r_s) : cnode_cap cap_ptr \<mapsto>u cap \<and>* R) s\<rbrace> gets_the (resolve_cap cnode_cap cap_ptr r_s) \<lbrace>Q\<rbrace>, \<lbrace>Q'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. Q ((cap_object cnode_cap, offset cap_ptr r), 0) s \<and> cdl.lift (\<box> (r, r_s) : cnode_cap cap_ptr \<mapsto>u cap \<and>* R) s \<Longrightarrow> case resolve_cap cnode_cap cap_ptr r_s s of None \<Rightarrow> True | Some (Inl e) \<Rightarrow> Q' e s | Some (Inr r) \<Rightarrow> Q r s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>Q ((cap_object cnode_cap, unat (cap_ptr && mask r)), 0) s; r_s = r + cap_guard_size cnode_cap; (cap_ptr >> r) && mask (cap_guard_size cnode_cap) = cap_guard cnode_cap; is_cnode_cap cnode_cap; cdl.lift (cap_object cnode_cap \<mapsto>f CNode (empty_cnode r) \<and>* (cap_object cnode_cap, unat (cap_ptr && mask r)) \<mapsto>c cap \<and>* R) s\<rbrakk> \<Longrightarrow> case resolve_cap cnode_cap cap_ptr (r + cap_guard_size cnode_cap) s of None \<Rightarrow> True | Some (Inl e) \<Rightarrow> Q' e s | Some (Inr r) \<Rightarrow> Q r s proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>Q ((cap_object cnode_cap, unat (cap_ptr && mask r)), 0) s; r_s = r + cap_guard_size cnode_cap; (cap_ptr >> r) && mask (cap_guard_size cnode_cap) = cap_guard cnode_cap; is_cnode_cap cnode_cap; cdl.lift (cap_object cnode_cap \<mapsto>f CNode (empty_cnode r) \<and>* (cap_object cnode_cap, unat (cap_ptr && mask r)) \<mapsto>c cap \<and>* R) s; resolve_cap cnode_cap cap_ptr (r + cap_guard_size cnode_cap) s = Some x2\<rbrakk> \<Longrightarrow> (\<forall>x1. x2 = Inl x1 \<longrightarrow> Q' x1 s) \<and> (\<forall>a b ba. x2 = Inr ((a, b), ba) \<longrightarrow> Q ((a, b), ba) s) proof (prove)
goal (2 subgoals):
 1. \<And>s x2 x1. \<lbrakk>Q ((cap_object cnode_cap, unat (cap_ptr && mask r)), 0) s; r_s = r + cap_guard_size cnode_cap; (cap_ptr >> r) && mask (cap_guard_size cnode_cap) = cap_guard cnode_cap; is_cnode_cap cnode_cap; cdl.lift (cap_object cnode_cap \<mapsto>f CNode (empty_cnode r) \<and>* (cap_object cnode_cap, unat (cap_ptr && mask r)) \<mapsto>c cap \<and>* R) s; resolve_cap cnode_cap cap_ptr (r + cap_guard_size cnode_cap) s = Some (Inl x1)\<rbrakk> \<Longrightarrow> Q' x1 s
 2. \<And>s x2 a b ba. \<lbrakk>Q ((cap_object cnode_cap, unat (cap_ptr && mask r)), 0) s; r_s = r + cap_guard_size cnode_cap; (cap_ptr >> r) && mask (cap_guard_size cnode_cap) = cap_guard cnode_cap; is_cnode_cap cnode_cap; cdl.lift (cap_object cnode_cap \<mapsto>f CNode (empty_cnode r) \<and>* (cap_object cnode_cap, unat (cap_ptr && mask r)) \<mapsto>c cap \<and>* R) s; resolve_cap cnode_cap cap_ptr (r + cap_guard_size cnode_cap) s = Some (Inr ((a, b), ba))\<rbrakk> \<Longrightarrow> Q ((a, b), ba) s proof (prove)
goal (2 subgoals):
 1. \<And>s x1. \<lbrakk>Q ((cap_object cnode_cap, unat (cap_ptr && mask r)), 0) s; r_s = r + cap_guard_size cnode_cap; (cap_ptr >> r) && mask (cap_guard_size cnode_cap) = cap_guard cnode_cap; is_cnode_cap cnode_cap; cdl.lift (cap_object cnode_cap \<mapsto>f CNode (empty_cnode r) \<and>* (cap_object cnode_cap, unat (cap_ptr && mask r)) \<mapsto>c cap \<and>* R) s; (do {
  cnode \<leftarrow> opt_cnode (cap_object cnode_cap);
y \<leftarrow> oassert (0 < cdl_cnode_size_bits cnode \<or> 0 < cap_guard_size cnode_cap);
if r < cdl_cnode_size_bits cnode then othrow FaultError else do {
  offset \<leftarrow> oreturn $ (cap_ptr >> r + cap_guard_size cnode_cap - (cdl_cnode_size_bits cnode + cap_guard_size cnode_cap)) && mask (cdl_cnode_size_bits cnode);
slot \<leftarrow> oreturn (cap_object cnode_cap, unat offset);
size_left \<leftarrow> oreturn (r + cap_guard_size cnode_cap - (cdl_cnode_size_bits cnode + cap_guard_size cnode_cap));
if size_left = 0 then oreturnOk (slot, 0) else do {
  next_cap \<leftarrow> opt_cap slot;
if is_cnode_cap next_cap then resolve_cap next_cap cap_ptr size_left else oreturnOk (slot, size_left)
}
}
}) s = Some (Inl x1)\<rbrakk> \<Longrightarrow> Q' x1 s
 2. \<And>s x2 a b ba. \<lbrakk>Q ((cap_object cnode_cap, unat (cap_ptr && mask r)), 0) s; r_s = r + cap_guard_size cnode_cap; (cap_ptr >> r) && mask (cap_guard_size cnode_cap) = cap_guard cnode_cap; is_cnode_cap cnode_cap; cdl.lift (cap_object cnode_cap \<mapsto>f CNode (empty_cnode r) \<and>* (cap_object cnode_cap, unat (cap_ptr && mask r)) \<mapsto>c cap \<and>* R) s; resolve_cap cnode_cap cap_ptr (r + cap_guard_size cnode_cap) s = Some (Inr ((a, b), ba))\<rbrakk> \<Longrightarrow> Q ((a, b), ba) s proof (prove)
goal (2 subgoals):
 1. \<And>s x1 x2. \<lbrakk>Q ((cap_object cnode_cap, unat (cap_ptr && mask r)), 0) s; r_s = r + cap_guard_size cnode_cap; (cap_ptr >> r) && mask (cap_guard_size cnode_cap) = cap_guard cnode_cap; is_cnode_cap cnode_cap; cdl.lift (cap_object cnode_cap \<mapsto>f CNode (empty_cnode r) \<and>* (cap_object cnode_cap, unat (cap_ptr && mask r)) \<mapsto>c cap \<and>* R) s; opt_cnode (cap_object cnode_cap) s = Some x2; (if 0 < cdl_cnode_size_bits x2 \<or> 0 < cap_guard_size cnode_cap then Some () else None) = Some (); (if r < cdl_cnode_size_bits x2 then othrow FaultError else do {
  offset \<leftarrow> oreturn $ (cap_ptr >> r + cap_guard_size cnode_cap - (cdl_cnode_size_bits x2 + cap_guard_size cnode_cap)) && mask (cdl_cnode_size_bits x2);
slot \<leftarrow> oreturn (cap_object cnode_cap, unat offset);
size_left \<leftarrow> oreturn (r + cap_guard_size cnode_cap - (cdl_cnode_size_bits x2 + cap_guard_size cnode_cap));
if size_left = 0 then oreturnOk (slot, 0) else do {
  next_cap \<leftarrow> opt_cap slot;
if is_cnode_cap next_cap then resolve_cap next_cap cap_ptr size_left else oreturnOk (slot, size_left)
}
}) s = Some (Inl x1)\<rbrakk> \<Longrightarrow> Q' x1 s
 2. \<And>s x2 a b ba. \<lbrakk>Q ((cap_object cnode_cap, unat (cap_ptr && mask r)), 0) s; r_s = r + cap_guard_size cnode_cap; (cap_ptr >> r) && mask (cap_guard_size cnode_cap) = cap_guard cnode_cap; is_cnode_cap cnode_cap; cdl.lift (cap_object cnode_cap \<mapsto>f CNode (empty_cnode r) \<and>* (cap_object cnode_cap, unat (cap_ptr && mask r)) \<mapsto>c cap \<and>* R) s; resolve_cap cnode_cap cap_ptr (r + cap_guard_size cnode_cap) s = Some (Inr ((a, b), ba))\<rbrakk> \<Longrightarrow> Q ((a, b), ba) s proof (prove)
goal (3 subgoals):
 1. \<And>s x1 x2. \<lbrakk>Q ((cap_object cnode_cap, unat (cap_ptr && mask r)), 0) s; r_s = r + cap_guard_size cnode_cap; (cap_ptr >> r) && mask (cap_guard_size cnode_cap) = cap_guard cnode_cap; is_cnode_cap cnode_cap; opt_cnode (cap_object cnode_cap) s = Some x2; (if 0 < cdl_cnode_size_bits x2 \<or> 0 < cap_guard_size cnode_cap then Some () else None) = Some (); (if r < cdl_cnode_size_bits x2 then othrow FaultError else do {
  offset \<leftarrow> oreturn $ (cap_ptr >> r + cap_guard_size cnode_cap - (cdl_cnode_size_bits x2 + cap_guard_size cnode_cap)) && mask (cdl_cnode_size_bits x2);
slot \<leftarrow> oreturn (cap_object cnode_cap, unat offset);
size_left \<leftarrow> oreturn (r + cap_guard_size cnode_cap - (cdl_cnode_size_bits x2 + cap_guard_size cnode_cap));
if size_left = 0 then oreturnOk (slot, 0) else do {
  next_cap \<leftarrow> opt_cap slot;
if is_cnode_cap next_cap then resolve_cap next_cap cap_ptr size_left else oreturnOk (slot, size_left)
}
}) s = Some (Inl x1)\<rbrakk> \<Longrightarrow> opt_cnode (cap_object cnode_cap) s = Some (?obj64 s x1 x2)
 2. \<And>s x1 x2. \<lbrakk>Q ((cap_object cnode_cap, unat (cap_ptr && mask r)), 0) s; r_s = r + cap_guard_size cnode_cap; (cap_ptr >> r) && mask (cap_guard_size cnode_cap) = cap_guard cnode_cap; is_cnode_cap cnode_cap; opt_cnode (cap_object cnode_cap) s = Some x2; (if 0 < cdl_cnode_size_bits x2 \<or> 0 < cap_guard_size cnode_cap then Some () else None) = Some (); (if r < cdl_cnode_size_bits x2 then othrow FaultError else do {
  offset \<leftarrow> oreturn $ (cap_ptr >> r + cap_guard_size cnode_cap - (cdl_cnode_size_bits x2 + cap_guard_size cnode_cap)) && mask (cdl_cnode_size_bits x2);
slot \<leftarrow> oreturn (cap_object cnode_cap, unat offset);
size_left \<leftarrow> oreturn (r + cap_guard_size cnode_cap - (cdl_cnode_size_bits x2 + cap_guard_size cnode_cap));
if size_left = 0 then oreturnOk (slot, 0) else do {
  next_cap \<leftarrow> opt_cap slot;
if is_cnode_cap next_cap then resolve_cap next_cap cap_ptr size_left else oreturnOk (slot, size_left)
}
}) s = Some (Inl x1); r = cdl_cnode_size_bits (?obj64 s x1 x2)\<rbrakk> \<Longrightarrow> Q' x1 s
 3. \<And>s x2 a b ba. \<lbrakk>Q ((cap_object cnode_cap, unat (cap_ptr && mask r)), 0) s; r_s = r + cap_guard_size cnode_cap; (cap_ptr >> r) && mask (cap_guard_size cnode_cap) = cap_guard cnode_cap; is_cnode_cap cnode_cap; cdl.lift (cap_object cnode_cap \<mapsto>f CNode (empty_cnode r) \<and>* (cap_object cnode_cap, unat (cap_ptr && mask r)) \<mapsto>c cap \<and>* R) s; resolve_cap cnode_cap cap_ptr (r + cap_guard_size cnode_cap) s = Some (Inr ((a, b), ba))\<rbrakk> \<Longrightarrow> Q ((a, b), ba) s proof (prove)
goal (1 subgoal):
 1. \<And>s x2 a b ba. \<lbrakk>Q ((cap_object cnode_cap, unat (cap_ptr && mask r)), 0) s; r_s = r + cap_guard_size cnode_cap; (cap_ptr >> r) && mask (cap_guard_size cnode_cap) = cap_guard cnode_cap; is_cnode_cap cnode_cap; cdl.lift (cap_object cnode_cap \<mapsto>f CNode (empty_cnode r) \<and>* (cap_object cnode_cap, unat (cap_ptr && mask r)) \<mapsto>c cap \<and>* R) s; resolve_cap cnode_cap cap_ptr (r + cap_guard_size cnode_cap) s = Some (Inr ((a, b), ba))\<rbrakk> \<Longrightarrow> Q ((a, b), ba) s proof (prove)
goal (1 subgoal):
 1. \<And>s a b ba. \<lbrakk>Q ((cap_object cnode_cap, unat (cap_ptr && mask r)), 0) s; r_s = r + cap_guard_size cnode_cap; (cap_ptr >> r) && mask (cap_guard_size cnode_cap) = cap_guard cnode_cap; is_cnode_cap cnode_cap; cdl.lift (cap_object cnode_cap \<mapsto>f CNode (empty_cnode r) \<and>* (cap_object cnode_cap, unat (cap_ptr && mask r)) \<mapsto>c cap \<and>* R) s; (do {
  cnode \<leftarrow> opt_cnode (cap_object cnode_cap);
y \<leftarrow> oassert (0 < cdl_cnode_size_bits cnode \<or> 0 < cap_guard_size cnode_cap);
if r < cdl_cnode_size_bits cnode then othrow FaultError else do {
  offset \<leftarrow> oreturn $ (cap_ptr >> r + cap_guard_size cnode_cap - (cdl_cnode_size_bits cnode + cap_guard_size cnode_cap)) && mask (cdl_cnode_size_bits cnode);
slot \<leftarrow> oreturn (cap_object cnode_cap, unat offset);
size_left \<leftarrow> oreturn (r + cap_guard_size cnode_cap - (cdl_cnode_size_bits cnode + cap_guard_size cnode_cap));
if size_left = 0 then oreturnOk (slot, 0) else do {
  next_cap \<leftarrow> opt_cap slot;
if is_cnode_cap next_cap then resolve_cap next_cap cap_ptr size_left else oreturnOk (slot, size_left)
}
}
}) s = Some (Inr ((a, b), ba))\<rbrakk> \<Longrightarrow> Q ((a, b), ba) s proof (prove)
goal (1 subgoal):
 1. \<And>s a b ba x2. \<lbrakk>Q ((cap_object cnode_cap, unat (cap_ptr && mask r)), 0) s; r_s = r + cap_guard_size cnode_cap; (cap_ptr >> r) && mask (cap_guard_size cnode_cap) = cap_guard cnode_cap; is_cnode_cap cnode_cap; cdl.lift (cap_object cnode_cap \<mapsto>f CNode (empty_cnode r) \<and>* (cap_object cnode_cap, unat (cap_ptr && mask r)) \<mapsto>c cap \<and>* R) s; opt_cnode (cap_object cnode_cap) s = Some x2; (if 0 < cdl_cnode_size_bits x2 \<or> 0 < cap_guard_size cnode_cap then Some () else None) = Some (); (if r < cdl_cnode_size_bits x2 then othrow FaultError else do {
  offset \<leftarrow> oreturn $ (cap_ptr >> r + cap_guard_size cnode_cap - (cdl_cnode_size_bits x2 + cap_guard_size cnode_cap)) && mask (cdl_cnode_size_bits x2);
slot \<leftarrow> oreturn (cap_object cnode_cap, unat offset);
size_left \<leftarrow> oreturn (r + cap_guard_size cnode_cap - (cdl_cnode_size_bits x2 + cap_guard_size cnode_cap));
if size_left = 0 then oreturnOk (slot, 0) else do {
  next_cap \<leftarrow> opt_cap slot;
if is_cnode_cap next_cap then resolve_cap next_cap cap_ptr size_left else oreturnOk (slot, size_left)
}
}) s = Some (Inr ((a, b), ba))\<rbrakk> \<Longrightarrow> Q ((a, b), ba) s proof (prove)
goal (2 subgoals):
 1. \<And>s a b ba x2. \<lbrakk>Q ((cap_object cnode_cap, unat (cap_ptr && mask r)), 0) s; r_s = r + cap_guard_size cnode_cap; (cap_ptr >> r) && mask (cap_guard_size cnode_cap) = cap_guard cnode_cap; is_cnode_cap cnode_cap; opt_cnode (cap_object cnode_cap) s = Some x2; (if 0 < cdl_cnode_size_bits x2 \<or> 0 < cap_guard_size cnode_cap then Some () else None) = Some (); (if r < cdl_cnode_size_bits x2 then othrow FaultError else do {
  offset \<leftarrow> oreturn $ (cap_ptr >> r + cap_guard_size cnode_cap - (cdl_cnode_size_bits x2 + cap_guard_size cnode_cap)) && mask (cdl_cnode_size_bits x2);
slot \<leftarrow> oreturn (cap_object cnode_cap, unat offset);
size_left \<leftarrow> oreturn (r + cap_guard_size cnode_cap - (cdl_cnode_size_bits x2 + cap_guard_size cnode_cap));
if size_left = 0 then oreturnOk (slot, 0) else do {
  next_cap \<leftarrow> opt_cap slot;
if is_cnode_cap next_cap then resolve_cap next_cap cap_ptr size_left else oreturnOk (slot, size_left)
}
}) s = Some (Inr ((a, b), ba))\<rbrakk> \<Longrightarrow> opt_cnode (cap_object cnode_cap) s = Some (?obj102 s a b ba x2)
 2. \<And>s a b ba x2. \<lbrakk>Q ((cap_object cnode_cap, unat (cap_ptr && mask r)), 0) s; r_s = r + cap_guard_size cnode_cap; (cap_ptr >> r) && mask (cap_guard_size cnode_cap) = cap_guard cnode_cap; is_cnode_cap cnode_cap; opt_cnode (cap_object cnode_cap) s = Some x2; (if 0 < cdl_cnode_size_bits x2 \<or> 0 < cap_guard_size cnode_cap then Some () else None) = Some (); (if r < cdl_cnode_size_bits x2 then othrow FaultError else do {
  offset \<leftarrow> oreturn $ (cap_ptr >> r + cap_guard_size cnode_cap - (cdl_cnode_size_bits x2 + cap_guard_size cnode_cap)) && mask (cdl_cnode_size_bits x2);
slot \<leftarrow> oreturn (cap_object cnode_cap, unat offset);
size_left \<leftarrow> oreturn (r + cap_guard_size cnode_cap - (cdl_cnode_size_bits x2 + cap_guard_size cnode_cap));
if size_left = 0 then oreturnOk (slot, 0) else do {
  next_cap \<leftarrow> opt_cap slot;
if is_cnode_cap next_cap then resolve_cap next_cap cap_ptr size_left else oreturnOk (slot, size_left)
}
}) s = Some (Inr ((a, b), ba)); r = cdl_cnode_size_bits (?obj102 s a b ba x2)\<rbrakk> \<Longrightarrow> Q ((a, b), ba) s proof (prove)
goal:
No subgoals!