theory CSpace_AI

lemma lookup_slot_for_cnode_op_cap_to2[wp]:
  "\<lbrace>\<lambda>s. (is_cnode_cap croot \<longrightarrow>
          (\<forall>r\<in>cte_refs croot (interrupt_irq_node s). ex_cte_cap_wp_to P r s))
       \<and> (\<forall>cp. is_cnode_cap cp \<longrightarrow> P cp)\<rbrace>
    lookup_slot_for_cnode_op is_src croot ptr depth
   \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P rv\<rbrace>,-" proof - have x: "\<And>x f g. (case x of [] \<Rightarrow> f | _ \<Rightarrow> g) = (if x = [] then f else g)" by (simp split: list.splits) show ?thesis apply (simp   add: lookup_slot_for_cnode_op_def split_def x
            split del: if_split cong: if_cong) apply (wp | simp)+ apply (rule hoare_drop_imps) apply (unfold unlessE_def whenE_def) apply (wp rab_cte_cap_to)+ apply clarsimp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (is_cnode_cap croot \<longrightarrow> (\<forall>r\<in>cte_refs croot (interrupt_irq_node s). ex_cte_cap_wp_to P r s)) \<and> (\<forall>cp. is_cnode_cap cp \<longrightarrow> P cp)\<rbrace> lookup_slot_for_cnode_op is_src croot ptr depth \<lbrace>ex_cte_cap_wp_to P\<rbrace>, - proof (state)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (is_cnode_cap croot \<longrightarrow> (\<forall>r\<in>cte_refs croot (interrupt_irq_node s). ex_cte_cap_wp_to P r s)) \<and> (\<forall>cp. is_cnode_cap cp \<longrightarrow> P cp)\<rbrace> lookup_slot_for_cnode_op is_src croot ptr depth \<lbrace>ex_cte_cap_wp_to P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>x f g. (case x of [] \<Rightarrow> f | a # list \<Rightarrow> g) = (if x = [] then f else g) proof (state)
this:
(case ?x of [] \<Rightarrow> ?f | a # list \<Rightarrow> ?g) = (if ?x = [] then ?f else ?g)

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (is_cnode_cap croot \<longrightarrow> (\<forall>r\<in>cte_refs croot (interrupt_irq_node s). ex_cte_cap_wp_to P r s)) \<and> (\<forall>cp. is_cnode_cap cp \<longrightarrow> P cp)\<rbrace> lookup_slot_for_cnode_op is_src croot ptr depth \<lbrace>ex_cte_cap_wp_to P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (is_cnode_cap croot \<longrightarrow> (\<forall>r\<in>cte_refs croot (interrupt_irq_node s). ex_cte_cap_wp_to P r s)) \<and> (\<forall>cp. is_cnode_cap cp \<longrightarrow> P cp)\<rbrace> lookup_slot_for_cnode_op is_src croot ptr depth \<lbrace>ex_cte_cap_wp_to P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (is_cnode_cap croot \<longrightarrow> (\<forall>r\<in>cte_refs croot (interrupt_irq_node s). ex_cte_cap_wp_to P r s)) \<and> (\<forall>cp. is_cnode_cap cp \<longrightarrow> P cp)\<rbrace> if is_cnode_cap croot then doE y <- whenE (depth = 0 \<or> word_bits < depth) (throwError (RangeError 1 (word_of_nat word_bits)));
lookup_error_on_failure is_src (doE p <- resolve_address_bits (croot, drop (length ptr - depth) ptr);
if snd p = [] then returnOk (fst p) else throwError (DepthMismatch (length (snd p)) 0)
odE)
odE else throwError (FailedLookup is_src InvalidRoot) \<lbrace>ex_cte_cap_wp_to P\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. is_cnode_cap croot \<Longrightarrow> \<lbrace>?P'17 ()\<rbrace> resolve_address_bits (croot, drop (length ptr - depth) ptr) \<lbrace>\<lambda>p s. snd p = [] \<longrightarrow> ex_cte_cap_wp_to P (fst p) s\<rbrace>, -
 2. is_cnode_cap croot \<Longrightarrow> \<lbrace>?Qa8\<rbrace> whenE (depth = 0 \<or> word_bits < depth) (throwError (RangeError 1 (word_of_nat word_bits))) \<lbrace>\<lambda>y s. True \<and> ?P'17 y s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<not> is_cnode_cap croot \<Longrightarrow> \<lbrace>?R8\<rbrace> throwError (FailedLookup is_src InvalidRoot) \<lbrace>ex_cte_cap_wp_to P\<rbrace>, -
 4. \<And>s. (is_cnode_cap croot \<longrightarrow> (\<forall>r\<in>cte_refs croot (interrupt_irq_node s). ex_cte_cap_wp_to P r s)) \<and> (\<forall>cp. is_cnode_cap cp \<longrightarrow> P cp) \<Longrightarrow> (is_cnode_cap croot \<longrightarrow> ?Qa8 s) \<and> (\<not> is_cnode_cap croot \<longrightarrow> ?R8 s) proof (prove)
goal (4 subgoals):
 1. is_cnode_cap croot \<Longrightarrow> \<lbrace>?P'17 ()\<rbrace> resolve_address_bits (croot, drop (length ptr - depth) ptr) \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, -
 2. is_cnode_cap croot \<Longrightarrow> \<lbrace>?Qa8\<rbrace> whenE (depth = 0 \<or> word_bits < depth) (throwError (RangeError 1 (word_of_nat word_bits))) \<lbrace>\<lambda>y s. True \<and> ?P'17 y s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<not> is_cnode_cap croot \<Longrightarrow> \<lbrace>?R8\<rbrace> throwError (FailedLookup is_src InvalidRoot) \<lbrace>ex_cte_cap_wp_to P\<rbrace>, -
 4. \<And>s. (is_cnode_cap croot \<longrightarrow> (\<forall>r\<in>cte_refs croot (interrupt_irq_node s). ex_cte_cap_wp_to P r s)) \<and> (\<forall>cp. is_cnode_cap cp \<longrightarrow> P cp) \<Longrightarrow> (is_cnode_cap croot \<longrightarrow> ?Qa8 s) \<and> (\<not> is_cnode_cap croot \<longrightarrow> ?R8 s) proof (prove)
goal (4 subgoals):
 1. is_cnode_cap croot \<Longrightarrow> \<lbrace>?P'17 ()\<rbrace> resolve_address_bits (croot, drop (length ptr - depth) ptr) \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, -
 2. is_cnode_cap croot \<Longrightarrow> \<lbrace>?Qa8\<rbrace> if depth = 0 \<or> word_bits < depth then throwError (RangeError 1 (word_of_nat word_bits)) else returnOk () \<lbrace>\<lambda>y s. True \<and> ?P'17 y s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<not> is_cnode_cap croot \<Longrightarrow> \<lbrace>?R8\<rbrace> throwError (FailedLookup is_src InvalidRoot) \<lbrace>ex_cte_cap_wp_to P\<rbrace>, -
 4. \<And>s. (is_cnode_cap croot \<longrightarrow> (\<forall>r\<in>cte_refs croot (interrupt_irq_node s). ex_cte_cap_wp_to P r s)) \<and> (\<forall>cp. is_cnode_cap cp \<longrightarrow> P cp) \<Longrightarrow> (is_cnode_cap croot \<longrightarrow> ?Qa8 s) \<and> (\<not> is_cnode_cap croot \<longrightarrow> ?R8 s) proof (prove)
goal (1 subgoal):
 1. \<And>s. (is_cnode_cap croot \<longrightarrow> (\<forall>r\<in>cte_refs croot (interrupt_irq_node s). ex_cte_cap_wp_to P r s)) \<and> (\<forall>cp. is_cnode_cap cp \<longrightarrow> P cp) \<Longrightarrow> (is_cnode_cap croot \<longrightarrow> True \<and> True \<and> (depth = 0 \<or> word_bits < depth \<longrightarrow> True) \<and> (\<not> (depth = 0 \<or> word_bits < depth) \<longrightarrow> (is_cnode_cap (fst (croot, drop (length ptr - depth) ptr)) \<longrightarrow> (\<forall>r\<in>cte_refs (fst (croot, drop (length ptr - depth) ptr)) (interrupt_irq_node s). ex_cte_cap_wp_to P r s)) \<and> (\<forall>cap. is_cnode_cap cap \<longrightarrow> P cap))) \<and> (\<not> is_cnode_cap croot \<longrightarrow> True) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>\<lambda>s. (is_cnode_cap croot \<longrightarrow> (\<forall>r\<in>cte_refs croot (interrupt_irq_node s). ex_cte_cap_wp_to P r s)) \<and> (\<forall>cp. is_cnode_cap cp \<longrightarrow> P cp)\<rbrace> lookup_slot_for_cnode_op is_src croot ptr depth \<lbrace>ex_cte_cap_wp_to P\<rbrace>, -

goal:
No subgoals!