theory KHeap_DP

lemma lookup_slot_for_cnode_op_wp [wp]:
  "\<lbrace>P\<rbrace>
    lookup_slot_for_cnode_op cnode_cap cap_ptr remaining_size
  \<lbrace>\<lambda>_. P \<rbrace>" apply (clarsimp simp: lookup_slot_for_cnode_op_def split_def) apply (wp) apply (clarsimp simp: fault_to_except_def) apply (wp) apply (clarsimp simp: gets_the_resolve_cap[symmetric]) apply (wp gets_the_wpE whenE_wp)+ apply (clarsimp split: option.splits 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> 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> proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrace>?B3 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>?B3\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>s. P s \<Longrightarrow> ?Q1 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?B3 ()\<rbrace> resolve_address_bits 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>?B3\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>s. P s \<Longrightarrow> ?Q1 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?B3 ()\<rbrace> resolve_address_bits 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>x s. P s \<and> True\<rbrace>
 2. \<lbrace>?Q1\<rbrace> whenE (remaining_size = 0 \<or> word_bits < remaining_size) throw \<lbrace>?B3\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>s. P s \<Longrightarrow> ?Q1 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?B3 ()\<rbrace> 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>x. P\<rbrace>
 2. \<lbrace>?Q1\<rbrace> whenE (remaining_size = 0 \<or> word_bits < remaining_size) throw \<lbrace>?B3\<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 | Some (Inr r) \<Rightarrow> (snd r = 0 \<longrightarrow> P a) \<and> (0 < snd r \<longrightarrow> P a))) s proof (prove)
goal:
No subgoals!