theory Untyped_AI

lemma dui_sp_helper:
  "(\<And>s. P s \<Longrightarrow> valid_objs s) \<Longrightarrow>
   \<lbrace>P\<rbrace> if val = 0 then returnOk root_cap
       else doE node_slot \<leftarrow>
                  lookup_target_slot root_cap (to_bl (args ! 2)) (unat (args ! 3));
                  liftE $ get_cap node_slot
            odE \<lbrace>\<lambda>rv s. (rv = root_cap \<or> (\<exists>slot. cte_wp_at ((=) rv) slot s)) \<and> P s\<rbrace>, -" apply (simp add: split_def lookup_target_slot_def) apply (intro impI conjI) apply wpsimp apply (wp get_cap_wp) apply (rule hoare_post_imp_R [where Q'="\<lambda>rv. valid_objs and P"]
          ; wpsimp simp: cte_wp_at_caps_of_state) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. P s \<Longrightarrow> valid_objs s) \<Longrightarrow> \<lbrace>P\<rbrace> if val = (0::'b) then returnOk root_cap else doE node_slot <- lookup_target_slot root_cap (to_bl (args ! 2)) (unat (args ! 3));
liftE $ get_cap node_slot
odE \<lbrace>\<lambda>rv s. (rv = root_cap \<or> (\<exists>slot. cte_wp_at ((=) rv) slot s)) \<and> P s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. (\<And>s. P s \<Longrightarrow> valid_objs s) \<Longrightarrow> (val = (0::'b) \<longrightarrow> \<lbrace>P\<rbrace> returnOk root_cap \<lbrace>\<lambda>rv s. (rv = root_cap \<or> (\<exists>a b. cte_wp_at ((=) rv) (a, b) s)) \<and> P s\<rbrace>, -) \<and> (val \<noteq> (0::'b) \<longrightarrow> \<lbrace>P\<rbrace> doE node_slot <- lookup_slot_for_cnode_op False root_cap (to_bl (args ! 2)) (unat (args ! 3));
liftE (get_cap node_slot)
odE \<lbrace>\<lambda>rv s. (rv = root_cap \<or> (\<exists>a b. cte_wp_at ((=) rv) (a, b) s)) \<and> P s\<rbrace>, -) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>s. P s \<Longrightarrow> valid_objs s; val = (0::'b)\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> returnOk root_cap \<lbrace>\<lambda>rv s. (rv = root_cap \<or> (\<exists>a b. cte_wp_at ((=) rv) (a, b) s)) \<and> P s\<rbrace>, -
 2. \<lbrakk>\<And>s. P s \<Longrightarrow> valid_objs s; val \<noteq> (0::'b)\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE node_slot <- lookup_slot_for_cnode_op False root_cap (to_bl (args ! 2)) (unat (args ! 3));
liftE (get_cap node_slot)
odE \<lbrace>\<lambda>rv s. (rv = root_cap \<or> (\<exists>a b. cte_wp_at ((=) rv) (a, b) s)) \<and> P s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. P s \<Longrightarrow> valid_objs s; val \<noteq> (0::'b)\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE node_slot <- lookup_slot_for_cnode_op False root_cap (to_bl (args ! 2)) (unat (args ! 3));
liftE (get_cap node_slot)
odE \<lbrace>\<lambda>rv s. (rv = root_cap \<or> (\<exists>a b. cte_wp_at ((=) rv) (a, b) s)) \<and> P s\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>s. P s \<Longrightarrow> valid_objs s; val \<noteq> (0::'b)\<rbrakk> \<Longrightarrow> \<lbrace>?P'17\<rbrace> lookup_slot_for_cnode_op False root_cap (to_bl (args ! 2)) (unat (args ! 3)) \<lbrace>\<lambda>node_slot s. \<forall>cap. cte_wp_at ((=) cap) node_slot s \<longrightarrow> (cap = root_cap \<or> (\<exists>a b. cte_wp_at ((=) cap) (a, b) s)) \<and> P s\<rbrace>, -
 2. \<And>s. \<lbrakk>\<And>s. P s \<Longrightarrow> valid_objs s; val \<noteq> (0::'b); P s\<rbrakk> \<Longrightarrow> True \<and> ?P'17 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>s. P s \<Longrightarrow> valid_objs s; val \<noteq> (0::'b); P s\<rbrakk> \<Longrightarrow> True \<and> (valid_objs and P) s proof (prove)
goal:
No subgoals!