theory KHeap_DP

lemma resolve_cap_u:
   "\<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>\<lambda> _ _.  True\<rbrace>" apply (wp gets_the_wpE) apply (clarsimp simp:
    user_pointer_at_def Let_unfold one_lvl_lookup_def
    offset_def  split:option.splits sum.splits) apply (simp add: split_def resolve_cap.simps split: if_split_asm) apply (simp add: obind_def sep_conj_assoc 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>\<lambda>_ _. True\<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> True | Some (Inr r) \<Rightarrow> Q r 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; guard_equal cnode_cap cap_ptr (r + cap_guard_size 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; guard_equal cnode_cap cap_ptr (r + cap_guard_size 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 (cap_ptr >> r) && mask (cap_guard_size cnode_cap) = cap_guard cnode_cap \<longrightarrow> 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; guard_equal cnode_cap cap_ptr (r + cap_guard_size 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 (cap_ptr >> r) && mask (cap_guard_size cnode_cap) = cap_guard cnode_cap \<longrightarrow> 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; guard_equal cnode_cap cap_ptr (r + cap_guard_size 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 (cap_ptr >> r) && mask (cap_guard_size cnode_cap) = cap_guard cnode_cap \<longrightarrow> 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 (?obj56 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; guard_equal cnode_cap cap_ptr (r + cap_guard_size 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 (cap_ptr >> r) && mask (cap_guard_size cnode_cap) = cap_guard cnode_cap \<longrightarrow> 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 (?obj56 s a b ba x2)\<rbrakk> \<Longrightarrow> Q ((a, b), ba) s proof (prove)
goal:
No subgoals!