theory Ipc_C

lemma doIPCTransfer_reply_or_replyslot:
  "\<lbrace> cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot
      or (valid_objs' and (Not o real_cte_at' slot)
          and  cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot)\<rbrace>
    doIPCTransfer sender ep badge grant receiver
    \<lbrace> \<lambda>rv. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot\<rbrace>" apply (rule hoare_name_pre_state) apply (case_tac "cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot s") apply (rule hoare_pre, rule hoare_strengthen_post,
        rule_tac P="isReplyCap" and ptr=slot in doIPCTransfer_non_null_cte_wp_at2') apply (clarsimp simp: isCap_simps) apply (clarsimp simp: isCap_simps) apply (clarsimp simp: cte_wp_at_ctes_of) apply simp apply (wp doIPCTransfer_local_slots) apply (clarsimp simp: maskedAsFull_def cap_get_tag_isCap isCap_simps
                  split: if_split) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot or valid_objs' and Not \<circ> real_cte_at' slot and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot\<rbrace> doIPCTransfer sender ep badge grant receiver \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot or valid_objs' and Not \<circ> real_cte_at' slot and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> doIPCTransfer sender ep badge grant receiver \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>(cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot or valid_objs' and Not \<circ> real_cte_at' slot and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot) s; cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doIPCTransfer sender ep badge grant receiver \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot\<rbrace>
 2. \<And>s. \<lbrakk>(cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot or valid_objs' and Not \<circ> real_cte_at' slot and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot) s; \<not> cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doIPCTransfer sender ep badge grant receiver \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s cte. \<lbrakk>(cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot or valid_objs' and Not \<circ> real_cte_at' slot and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot) s; cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot s; isReplyCap (cteCap cte)\<rbrakk> \<Longrightarrow> cteCap cte \<noteq> capability.NullCap
 2. \<And>s cap. \<lbrakk>(cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot or valid_objs' and Not \<circ> real_cte_at' slot and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot) s; cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot s; isReplyCap cap\<rbrakk> \<Longrightarrow> \<not> isUntypedCap cap
 3. \<And>s rv sa. \<lbrakk>(cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot or valid_objs' and Not \<circ> real_cte_at' slot and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot) s; cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot s; cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot sa\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot sa
 4. \<And>s sa. \<lbrakk>(cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot or valid_objs' and Not \<circ> real_cte_at' slot and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot) s; cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot s; s = sa\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot sa
 5. \<And>s. \<lbrakk>(cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot or valid_objs' and Not \<circ> real_cte_at' slot and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot) s; \<not> cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doIPCTransfer sender ep badge grant receiver \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s cap. \<lbrakk>(cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot or valid_objs' and Not \<circ> real_cte_at' slot and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot) s; cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot s; isReplyCap cap\<rbrakk> \<Longrightarrow> \<not> isUntypedCap cap
 2. \<And>s rv sa. \<lbrakk>(cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot or valid_objs' and Not \<circ> real_cte_at' slot and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot) s; cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot s; cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot sa\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot sa
 3. \<And>s sa. \<lbrakk>(cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot or valid_objs' and Not \<circ> real_cte_at' slot and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot) s; cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot s; s = sa\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot sa
 4. \<And>s. \<lbrakk>(cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot or valid_objs' and Not \<circ> real_cte_at' slot and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot) s; \<not> cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doIPCTransfer sender ep badge grant receiver \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s rv sa. \<lbrakk>(cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot or valid_objs' and Not \<circ> real_cte_at' slot and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot) s; cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot s; cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot sa\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot sa
 2. \<And>s sa. \<lbrakk>(cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot or valid_objs' and Not \<circ> real_cte_at' slot and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot) s; cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot s; s = sa\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot sa
 3. \<And>s. \<lbrakk>(cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot or valid_objs' and Not \<circ> real_cte_at' slot and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot) s; \<not> cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doIPCTransfer sender ep badge grant receiver \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s sa. \<lbrakk>(cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot or valid_objs' and Not \<circ> real_cte_at' slot and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot) s; cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot s; s = sa\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot sa
 2. \<And>s. \<lbrakk>(cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot or valid_objs' and Not \<circ> real_cte_at' slot and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot) s; \<not> cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doIPCTransfer sender ep badge grant receiver \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>(cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot or valid_objs' and Not \<circ> real_cte_at' slot and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot) s; \<not> cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doIPCTransfer sender ep badge grant receiver \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s c cap. \<lbrakk>(cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot or valid_objs' and Not \<circ> real_cte_at' slot and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot) s; \<not> cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot s\<rbrakk> \<Longrightarrow> (maskedAsFull c cap = capability.NullCap \<or> isReplyCap (maskedAsFull c cap)) = (c = capability.NullCap \<or> isReplyCap c)
 2. \<And>s sa. \<lbrakk>(cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot or valid_objs' and Not \<circ> real_cte_at' slot and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot) s; \<not> cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot s; s = sa\<rbrakk> \<Longrightarrow> (valid_objs' and Not \<circ> real_cte_at' slot and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot) sa proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>(cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot or valid_objs' and Not \<circ> real_cte_at' slot and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot) s; \<not> cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot s; s = sa\<rbrakk> \<Longrightarrow> (valid_objs' and Not \<circ> real_cte_at' slot and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) slot) sa proof (prove)
goal:
No subgoals!