theory Untyped_R

lemma dui_sp_helper':
  "\<lbrace>P\<rbrace> if Q then returnOk root_cap
       else doE slot \<leftarrow>
                  lookupTargetSlot root_cap cref dpth;
                  liftE (getSlotCap slot)
            odE \<lbrace>\<lambda>rv s. (rv = root_cap \<or> (\<exists>slot. cte_wp_at' ((=) rv o cteCap) slot s)) \<and> P s\<rbrace>, -" apply (cases Q, simp_all add: lookupTargetSlot_def) apply (wp, simp) apply (simp add: getSlotCap_def split_def) apply wp apply (rule hoare_strengthen_post [OF getCTE_sp[where P=P]]) apply (clarsimp simp: cte_wp_at_ctes_of) apply (elim allE, drule(1) mp) apply clarsimp apply wpsimp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> if Q then returnOk root_cap else doE slot <- lookupTargetSlot root_cap cref dpth;
liftE (getSlotCap slot)
odE \<lbrace>\<lambda>rv s. (rv = root_cap \<or> (\<exists>slot. cte_wp_at' ((=) rv \<circ> cteCap) slot s)) \<and> P s\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. Q \<Longrightarrow> \<lbrace>P\<rbrace> returnOk root_cap \<lbrace>\<lambda>rv s. (rv = root_cap \<or> (\<exists>slot. cte_wp_at' ((=) rv \<circ> cteCap) slot s)) \<and> P s\<rbrace>, -
 2. \<not> Q \<Longrightarrow> \<lbrace>P\<rbrace> doE slot <- lookupSlotForCNodeOp False root_cap cref dpth;
liftE (getSlotCap slot)
odE \<lbrace>\<lambda>rv s. (rv = root_cap \<or> (\<exists>slot. cte_wp_at' ((=) rv \<circ> cteCap) slot s)) \<and> P s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<not> Q \<Longrightarrow> \<lbrace>P\<rbrace> doE slot <- lookupSlotForCNodeOp False root_cap cref dpth;
liftE (getSlotCap slot)
odE \<lbrace>\<lambda>rv s. (rv = root_cap \<or> (\<exists>slot. cte_wp_at' ((=) rv \<circ> cteCap) slot s)) \<and> P s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<not> Q \<Longrightarrow> \<lbrace>P\<rbrace> doE slot <- lookupSlotForCNodeOp False root_cap cref dpth;
liftE (do cte <- getCTE slot;
return (cteCap cte)
od)
odE \<lbrace>\<lambda>rv s. (rv = root_cap \<or> (\<exists>slot. cte_wp_at' ((=) rv \<circ> cteCap) slot s)) \<and> P s\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>slot. \<not> Q \<Longrightarrow> \<lbrace>?B8 slot\<rbrace> getCTE slot \<lbrace>\<lambda>cte a. (cteCap cte = root_cap \<or> (\<exists>slot. cte_wp_at' ((=) (cteCap cte) \<circ> cteCap) slot a)) \<and> P a\<rbrace>
 2. \<not> Q \<Longrightarrow> \<lbrace>?P'7\<rbrace> lookupSlotForCNodeOp False root_cap cref dpth \<lbrace>?B8\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. \<lbrakk>\<not> Q; P s\<rbrakk> \<Longrightarrow> ?P'7 s proof (prove)
goal (3 subgoals):
 1. \<And>slot rv s. \<lbrakk>\<not> Q; (cte_wp_at' (\<lambda>c. c = rv) slot and P) s\<rbrakk> \<Longrightarrow> (cteCap rv = root_cap \<or> (\<exists>slot. cte_wp_at' ((=) (cteCap rv) \<circ> cteCap) slot s)) \<and> P s
 2. \<not> Q \<Longrightarrow> \<lbrace>?P'7\<rbrace> lookupSlotForCNodeOp False root_cap cref dpth \<lbrace>\<lambda>slot. P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. \<lbrakk>\<not> Q; P s\<rbrakk> \<Longrightarrow> ?P'7 s proof (prove)
goal (3 subgoals):
 1. \<And>slot rv s. \<lbrakk>\<not> Q; ctes_of s slot = Some rv; P s; \<forall>slot cte. ctes_of s slot = Some cte \<longrightarrow> cteCap rv \<noteq> cteCap cte\<rbrakk> \<Longrightarrow> cteCap rv = root_cap
 2. \<not> Q \<Longrightarrow> \<lbrace>?P'7\<rbrace> lookupSlotForCNodeOp False root_cap cref dpth \<lbrace>\<lambda>slot. P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. \<lbrakk>\<not> Q; P s\<rbrakk> \<Longrightarrow> ?P'7 s proof (prove)
goal (3 subgoals):
 1. \<And>slot rv s. \<lbrakk>\<not> Q; ctes_of s slot = Some rv; P s; cteCap rv \<noteq> cteCap rv\<rbrakk> \<Longrightarrow> cteCap rv = root_cap
 2. \<not> Q \<Longrightarrow> \<lbrace>?P'7\<rbrace> lookupSlotForCNodeOp False root_cap cref dpth \<lbrace>\<lambda>slot. P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. \<lbrakk>\<not> Q; P s\<rbrakk> \<Longrightarrow> ?P'7 s proof (prove)
goal (2 subgoals):
 1. \<not> Q \<Longrightarrow> \<lbrace>?P'7\<rbrace> lookupSlotForCNodeOp False root_cap cref dpth \<lbrace>\<lambda>slot. P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>s. \<lbrakk>\<not> Q; P s\<rbrakk> \<Longrightarrow> ?P'7 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<not> Q; P s\<rbrakk> \<Longrightarrow> True \<and> P s proof (prove)
goal:
No subgoals!