theory KHeap_DP

lemma resolve_cap_rv1:
   "\<lbrace>\<lambda>s. Q ((c,slot),0) 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>
         gets_the (resolve_cap cnode_cap cap_ptr remaining_size)
  \<lbrace>\<lambda>rv s. Q rv s\<rbrace>,\<lbrace>\<lambda>_ _ . True\<rbrace>" apply (wp gets_the_wpE) apply (clarsimp simp: one_lvl_lookup_def offset_def) apply (clarsimp simp: split_def split: sum.splits option.splits) apply (simp add: split_def resolve_cap.simps split: if_split_asm) apply (simp add: obind_def split:option.splits) apply (drule sep_f_size_opt_cnode) apply (simp split: if_split_asm)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q ((c, slot), 0) 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> gets_the (resolve_cap cnode_cap cap_ptr remaining_size) \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. Q ((c, slot), 0) 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> case resolve_cap cnode_cap cap_ptr remaining_size 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. \<lbrakk>Q ((cap_object cnode_cap, unat (cap_ptr && mask r)), 0) s; c = cap_object cnode_cap; slot = unat (cap_ptr && mask r); 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; remaining_size = r + cap_guard_size cnode_cap\<rbrakk> \<Longrightarrow> case resolve_cap cnode_cap cap_ptr (r + cap_guard_size cnode_cap) 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; c = cap_object cnode_cap; slot = unat (cap_ptr && mask r); 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; remaining_size = r + cap_guard_size cnode_cap; 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; c = cap_object cnode_cap; slot = unat (cap_ptr && mask r); 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; remaining_size = r + cap_guard_size cnode_cap; is_cnode_cap cnode_cap; (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; c = cap_object cnode_cap; slot = unat (cap_ptr && mask r); 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; remaining_size = 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> 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; c = cap_object cnode_cap; slot = unat (cap_ptr && mask r); remaining_size = 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 (?obj68 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; c = cap_object cnode_cap; slot = unat (cap_ptr && mask r); remaining_size = 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 (?obj68 s a b ba x2)\<rbrakk> \<Longrightarrow> Q ((a, b), ba) s proof (prove)
goal:
No subgoals!