theory CSpace_AI

lemma lookup_slot_for_cnode_op_cap_to[wp]:
  "\<lbrace>\<lambda>s. \<forall>r\<in>cte_refs croot (interrupt_irq_node s). ex_cte_cap_to r s\<rbrace>
    lookup_slot_for_cnode_op is_src croot ptr depth
   \<lbrace>\<lambda>rv. ex_cte_cap_to 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 (rule hoare_pre) 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. \<forall>r\<in>cte_refs croot (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s\<rbrace> lookup_slot_for_cnode_op is_src croot ptr depth \<lbrace>ex_cte_cap_wp_to (\<lambda>_. True)\<rbrace>, - proof (state)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>r\<in>cte_refs croot (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s\<rbrace> lookup_slot_for_cnode_op is_src croot ptr depth \<lbrace>ex_cte_cap_wp_to (\<lambda>_. True)\<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. \<forall>r\<in>cte_refs croot (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s\<rbrace> lookup_slot_for_cnode_op is_src croot ptr depth \<lbrace>ex_cte_cap_wp_to (\<lambda>_. True)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>r\<in>cte_refs croot (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s\<rbrace> lookup_slot_for_cnode_op is_src croot ptr depth \<lbrace>ex_cte_cap_wp_to (\<lambda>_. True)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>r\<in>cte_refs croot (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s\<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 (\<lambda>_. True)\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'7\<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 (\<lambda>_. True)\<rbrace>, -
 2. \<And>s. \<forall>r\<in>cte_refs croot (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s \<Longrightarrow> ?P'7 s proof (prove)
goal (4 subgoals):
 1. is_cnode_cap croot \<Longrightarrow> \<lbrace>?P'20 ()\<rbrace> resolve_address_bits (croot, drop (length ptr - depth) ptr) \<lbrace>\<lambda>p s. snd p = [] \<longrightarrow> ex_cte_cap_wp_to (\<lambda>_. True) (fst p) s\<rbrace>, -
 2. is_cnode_cap croot \<Longrightarrow> \<lbrace>?Qa11\<rbrace> whenE (depth = 0 \<or> word_bits < depth) (throwError (RangeError 1 (word_of_nat word_bits))) \<lbrace>\<lambda>y s. True \<and> ?P'20 y s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<not> is_cnode_cap croot \<Longrightarrow> \<lbrace>?R11\<rbrace> throwError (FailedLookup is_src InvalidRoot) \<lbrace>ex_cte_cap_wp_to (\<lambda>_. True)\<rbrace>, -
 4. \<And>s. \<forall>r\<in>cte_refs croot (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s \<Longrightarrow> (is_cnode_cap croot \<longrightarrow> ?Qa11 s) \<and> (\<not> is_cnode_cap croot \<longrightarrow> ?R11 s) proof (prove)
goal (4 subgoals):
 1. is_cnode_cap croot \<Longrightarrow> \<lbrace>?P'20 ()\<rbrace> resolve_address_bits (croot, drop (length ptr - depth) ptr) \<lbrace>\<lambda>rv. ex_cte_cap_wp_to (\<lambda>_. True) (fst rv)\<rbrace>, -
 2. is_cnode_cap croot \<Longrightarrow> \<lbrace>?Qa11\<rbrace> whenE (depth = 0 \<or> word_bits < depth) (throwError (RangeError 1 (word_of_nat word_bits))) \<lbrace>\<lambda>y s. True \<and> ?P'20 y s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<not> is_cnode_cap croot \<Longrightarrow> \<lbrace>?R11\<rbrace> throwError (FailedLookup is_src InvalidRoot) \<lbrace>ex_cte_cap_wp_to (\<lambda>_. True)\<rbrace>, -
 4. \<And>s. \<forall>r\<in>cte_refs croot (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s \<Longrightarrow> (is_cnode_cap croot \<longrightarrow> ?Qa11 s) \<and> (\<not> is_cnode_cap croot \<longrightarrow> ?R11 s) proof (prove)
goal (4 subgoals):
 1. is_cnode_cap croot \<Longrightarrow> \<lbrace>?P'20 ()\<rbrace> resolve_address_bits (croot, drop (length ptr - depth) ptr) \<lbrace>\<lambda>rv. ex_cte_cap_wp_to (\<lambda>_. True) (fst rv)\<rbrace>, -
 2. is_cnode_cap croot \<Longrightarrow> \<lbrace>?Qa11\<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'20 y s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<not> is_cnode_cap croot \<Longrightarrow> \<lbrace>?R11\<rbrace> throwError (FailedLookup is_src InvalidRoot) \<lbrace>ex_cte_cap_wp_to (\<lambda>_. True)\<rbrace>, -
 4. \<And>s. \<forall>r\<in>cte_refs croot (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s \<Longrightarrow> (is_cnode_cap croot \<longrightarrow> ?Qa11 s) \<and> (\<not> is_cnode_cap croot \<longrightarrow> ?R11 s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>r\<in>cte_refs croot (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s \<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 (\<lambda>cap. True) r s)) \<and> (\<forall>cap. is_cnode_cap cap \<longrightarrow> True))) \<and> (\<not> is_cnode_cap croot \<longrightarrow> True) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>\<lambda>s. \<forall>r\<in>cte_refs croot (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s\<rbrace> lookup_slot_for_cnode_op is_src croot ptr depth \<lbrace>ex_cte_cap_wp_to (\<lambda>_. True)\<rbrace>, -

goal:
No subgoals!