theory Fastpath_C

lemma isMasterReplyCap_fp_conv:
  "ccap_relation cap cap' \<Longrightarrow>
    (index (cap_C.words_C cap') 0 && 0x1F = scast cap_reply_cap)
       = (isReplyCap cap \<and> \<not> capReplyMaster cap)" apply (rule trans) apply (rule_tac m="mask 4" in split_word_eq_on_mask) apply (simp add: cap_get_tag_isCap[symmetric]) apply (rule conj_cong) apply (simp add: mask_def word_bw_assocs cap_get_tag_eq_x
                    cap_reply_cap_def split: if_split) apply (clarsimp simp: cap_lift_reply_cap cap_to_H_simps
                        isCap_simps
                 elim!: ccap_relationE) apply (simp add: mask_def cap_reply_cap_def word_bw_assocs
                   to_bool_def) apply (thin_tac "P" for P) apply (rule iffI) apply (drule_tac f="\<lambda>v. v >> 4" in arg_cong) apply (simp add: shiftr_over_and_dist) apply (drule_tac f="\<lambda>v. v << 4" in arg_cong) apply (simp add: shiftl_over_and_dist shiftr_shiftl1 mask_def
                   word_bw_assocs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccap_relation cap cap' \<Longrightarrow> (cap_C.words_C cap'.[0] && 0x1F = SCAST(32 signed \<rightarrow> 32) cap_reply_cap) = (isReplyCap cap \<and> \<not> capReplyMaster cap) proof (prove)
goal (2 subgoals):
 1. ccap_relation cap cap' \<Longrightarrow> (cap_C.words_C cap'.[0] && 0x1F = SCAST(32 signed \<rightarrow> 32) cap_reply_cap) = ?s
 2. ccap_relation cap cap' \<Longrightarrow> ?s = (isReplyCap cap \<and> \<not> capReplyMaster cap) proof (prove)
goal (1 subgoal):
 1. ccap_relation cap cap' \<Longrightarrow> ((cap_C.words_C cap'.[0] && 0x1F) && mask 4 = SCAST(32 signed \<rightarrow> 32) cap_reply_cap && mask 4 \<and> (cap_C.words_C cap'.[0] && 0x1F) && ~~ mask 4 = SCAST(32 signed \<rightarrow> 32) cap_reply_cap && ~~ mask 4) = (isReplyCap cap \<and> \<not> capReplyMaster cap) proof (prove)
goal (1 subgoal):
 1. ccap_relation cap cap' \<Longrightarrow> ((cap_C.words_C cap'.[0] && 0x1F) && mask 4 = SCAST(32 signed \<rightarrow> 32) cap_reply_cap && mask 4 \<and> (cap_C.words_C cap'.[0] && 0x1F) && ~~ mask 4 = SCAST(32 signed \<rightarrow> 32) cap_reply_cap && ~~ mask 4) = (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_reply_cap \<and> \<not> capReplyMaster cap) proof (prove)
goal (2 subgoals):
 1. ccap_relation cap cap' \<Longrightarrow> ((cap_C.words_C cap'.[0] && 0x1F) && mask 4 = SCAST(32 signed \<rightarrow> 32) cap_reply_cap && mask 4) = (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_reply_cap)
 2. \<lbrakk>ccap_relation cap cap'; cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_reply_cap\<rbrakk> \<Longrightarrow> ((cap_C.words_C cap'.[0] && 0x1F) && ~~ mask 4 = SCAST(32 signed \<rightarrow> 32) cap_reply_cap && ~~ mask 4) = (\<not> capReplyMaster cap) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation cap cap'; cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_reply_cap\<rbrakk> \<Longrightarrow> ((cap_C.words_C cap'.[0] && 0x1F) && ~~ mask 4 = SCAST(32 signed \<rightarrow> 32) cap_reply_cap && ~~ mask 4) = (\<not> capReplyMaster cap) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_reply_cap; cap = capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_C.words_C cap'.[0] && ~~ mask 6))) (to_bool ((cap_C.words_C cap'.[0] >> 4) && 1)) (to_bool ((cap_C.words_C cap'.[0] >> 5) && 1))\<rbrakk> \<Longrightarrow> ((cap_C.words_C cap'.[0] && 0x1F) && ~~ mask 4 = SCAST(32 signed \<rightarrow> 32) cap_reply_cap && ~~ mask 4) = (\<not> to_bool ((cap_C.words_C cap'.[0] >> 4) && 1)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_get_tag cap' = 8; cap = capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_C.words_C cap'.[0] && 0xFFFFFFC0))) ((cap_C.words_C cap'.[0] >> 4) && 1 = 1) ((cap_C.words_C cap'.[0] >> 5) && 1 = 1)\<rbrakk> \<Longrightarrow> (cap_C.words_C cap'.[0] && 0x10 = 0) = ((cap_C.words_C cap'.[0] >> 4) && 1 = 0) proof (prove)
goal (1 subgoal):
 1. cap = capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_C.words_C cap'.[0] && 0xFFFFFFC0))) ((cap_C.words_C cap'.[0] >> 4) && 1 = 1) ((cap_C.words_C cap'.[0] >> 5) && 1 = 1) \<Longrightarrow> (cap_C.words_C cap'.[0] && 0x10 = 0) = ((cap_C.words_C cap'.[0] >> 4) && 1 = 0) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cap = capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_C.words_C cap'.[0] && 0xFFFFFFC0))) ((cap_C.words_C cap'.[0] >> 4) && 1 = 1) ((cap_C.words_C cap'.[0] >> 5) && 1 = 1); cap_C.words_C cap'.[0] && 0x10 = 0\<rbrakk> \<Longrightarrow> (cap_C.words_C cap'.[0] >> 4) && 1 = 0
 2. \<lbrakk>cap = capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_C.words_C cap'.[0] && 0xFFFFFFC0))) ((cap_C.words_C cap'.[0] >> 4) && 1 = 1) ((cap_C.words_C cap'.[0] >> 5) && 1 = 1); (cap_C.words_C cap'.[0] >> 4) && 1 = 0\<rbrakk> \<Longrightarrow> cap_C.words_C cap'.[0] && 0x10 = 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cap = capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_C.words_C cap'.[0] && 0xFFFFFFC0))) ((cap_C.words_C cap'.[0] >> 4) && 1 = 1) ((cap_C.words_C cap'.[0] >> 5) && 1 = 1); cap_C.words_C cap'.[0] && 0x10 >> 4 = 0 >> 4\<rbrakk> \<Longrightarrow> (cap_C.words_C cap'.[0] >> 4) && 1 = 0
 2. \<lbrakk>cap = capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_C.words_C cap'.[0] && 0xFFFFFFC0))) ((cap_C.words_C cap'.[0] >> 4) && 1 = 1) ((cap_C.words_C cap'.[0] >> 5) && 1 = 1); (cap_C.words_C cap'.[0] >> 4) && 1 = 0\<rbrakk> \<Longrightarrow> cap_C.words_C cap'.[0] && 0x10 = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap = capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_C.words_C cap'.[0] && 0xFFFFFFC0))) ((cap_C.words_C cap'.[0] >> 4) && 1 = 1) ((cap_C.words_C cap'.[0] >> 5) && 1 = 1); (cap_C.words_C cap'.[0] >> 4) && 1 = 0\<rbrakk> \<Longrightarrow> cap_C.words_C cap'.[0] && 0x10 = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap = capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_C.words_C cap'.[0] && 0xFFFFFFC0))) ((cap_C.words_C cap'.[0] >> 4) && 1 = 1) ((cap_C.words_C cap'.[0] >> 5) && 1 = 1); (cap_C.words_C cap'.[0] >> 4) && 1 << 4 = 0 << 4\<rbrakk> \<Longrightarrow> cap_C.words_C cap'.[0] && 0x10 = 0 proof (prove)
goal:
No subgoals!