theory Tcb_DR

lemma cnode_cap_unique_bits:
  "is_cnode_cap cap \<Longrightarrow>
  \<lbrace>\<lambda>s. (\<forall>a b. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap) (a, b) s)
        \<and> valid_cap cap s \<and> valid_objs s\<rbrace>
    CSpaceAcc_A.get_cap (ba, c)
  \<lbrace>\<lambda>rv s. (Structures_A.is_cnode_cap rv \<and> obj_refs rv = obj_refs cap) \<longrightarrow> (bits_of rv = bits_of cap)\<rbrace>" apply (rule hoare_pre) apply (rule_tac Q="\<lambda>r s. (\<forall>a b. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and>
                                                    table_cap_ref c \<noteq> table_cap_ref cap) (a, b) s)
                            \<and> valid_cap cap s \<and> valid_objs s
                            \<and> valid_objs s \<and> cte_wp_at (\<lambda>x. x = r) (ba,c) s"
    in hoare_strengthen_post) apply (wp get_cap_cte_wp_at) apply (clarsimp simp:is_cap_simps) apply (drule_tac x = ba in spec) apply (drule_tac x = c in spec) apply (drule(1) cte_wp_at_valid_objs_valid_cap) apply (clarsimp simp:valid_cap_def obj_at_def is_ep_def is_ntfn_def is_cap_table_def,
          clarsimp split:Structures_A.kernel_object.split_asm)+ apply (clarsimp simp:well_formed_cnode_n_def bits_of_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Structures_A.is_cnode_cap cap \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>a b. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap) (a, b) s) \<and> s \<turnstile> cap \<and> valid_objs s\<rbrace> CSpaceAcc_A.get_cap (ba, c) \<lbrace>\<lambda>rv s. Structures_A.is_cnode_cap rv \<and> obj_refs rv = obj_refs cap \<longrightarrow> bits_of rv = bits_of cap\<rbrace> proof (prove)
goal (2 subgoals):
 1. Structures_A.is_cnode_cap cap \<Longrightarrow> \<lbrace>?Q\<rbrace> CSpaceAcc_A.get_cap (ba, c) \<lbrace>\<lambda>rv s. Structures_A.is_cnode_cap rv \<and> obj_refs rv = obj_refs cap \<longrightarrow> bits_of rv = bits_of cap\<rbrace>
 2. \<And>s. \<lbrakk>Structures_A.is_cnode_cap cap; (\<forall>a b. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap) (a, b) s) \<and> s \<turnstile> cap \<and> valid_objs s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. Structures_A.is_cnode_cap cap \<Longrightarrow> \<lbrace>?Q\<rbrace> CSpaceAcc_A.get_cap (ba, c) \<lbrace>\<lambda>r s. (\<forall>a b. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap) (a, b) s) \<and> s \<turnstile> cap \<and> valid_objs s \<and> valid_objs s \<and> cte_wp_at (\<lambda>x. x = r) (ba, c) s\<rbrace>
 2. \<And>rv s. \<lbrakk>Structures_A.is_cnode_cap cap; (\<forall>a b. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap) (a, b) s) \<and> s \<turnstile> cap \<and> valid_objs s \<and> valid_objs s \<and> cte_wp_at (\<lambda>x. x = rv) (ba, c) s\<rbrakk> \<Longrightarrow> Structures_A.is_cnode_cap rv \<and> obj_refs rv = obj_refs cap \<longrightarrow> bits_of rv = bits_of cap
 3. \<And>s. \<lbrakk>Structures_A.is_cnode_cap cap; (\<forall>a b. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap) (a, b) s) \<and> s \<turnstile> cap \<and> valid_objs s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>Structures_A.is_cnode_cap cap; (\<forall>a b. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap) (a, b) s) \<and> s \<turnstile> cap \<and> valid_objs s \<and> valid_objs s \<and> cte_wp_at (\<lambda>x. x = rv) (ba, c) s\<rbrakk> \<Longrightarrow> Structures_A.is_cnode_cap rv \<and> obj_refs rv = obj_refs cap \<longrightarrow> bits_of rv = bits_of cap
 2. \<And>s. \<lbrakk>Structures_A.is_cnode_cap cap; (\<forall>a b. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap) (a, b) s) \<and> s \<turnstile> cap \<and> valid_objs s\<rbrakk> \<Longrightarrow> (\<forall>a b. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap) (a, b) s) \<and> s \<turnstile> cap \<and> valid_objs s \<and> valid_objs s \<and> True proof (prove)
goal (2 subgoals):
 1. \<And>s r bits g bitsa ga. \<lbrakk>cap = cap.CNodeCap r bits g; \<forall>a b. \<not> cte_wp_at (\<lambda>c. obj_refs c = {r} \<and> table_cap_ref c \<noteq> table_cap_ref (cap.CNodeCap r bits g)) (a, b) s; s \<turnstile> cap.CNodeCap r bits g; valid_objs s; cte_wp_at (\<lambda>x. x = cap.CNodeCap r bitsa ga) (ba, c) s\<rbrakk> \<Longrightarrow> bits_of (cap.CNodeCap r bitsa ga) = bits_of (cap.CNodeCap r bits g)
 2. \<And>s. \<lbrakk>Structures_A.is_cnode_cap cap; (\<forall>a b. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap) (a, b) s) \<and> s \<turnstile> cap \<and> valid_objs s\<rbrakk> \<Longrightarrow> (\<forall>a b. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap) (a, b) s) \<and> s \<turnstile> cap \<and> valid_objs s \<and> valid_objs s \<and> True proof (prove)
goal (2 subgoals):
 1. \<And>s r bits g bitsa ga. \<lbrakk>cap = cap.CNodeCap r bits g; s \<turnstile> cap.CNodeCap r bits g; valid_objs s; cte_wp_at (\<lambda>x. x = cap.CNodeCap r bitsa ga) (ba, c) s; \<forall>b. \<not> cte_wp_at (\<lambda>c. obj_refs c = {r} \<and> table_cap_ref c \<noteq> table_cap_ref (cap.CNodeCap r bits g)) (ba, b) s\<rbrakk> \<Longrightarrow> bits_of (cap.CNodeCap r bitsa ga) = bits_of (cap.CNodeCap r bits g)
 2. \<And>s. \<lbrakk>Structures_A.is_cnode_cap cap; (\<forall>a b. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap) (a, b) s) \<and> s \<turnstile> cap \<and> valid_objs s\<rbrakk> \<Longrightarrow> (\<forall>a b. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap) (a, b) s) \<and> s \<turnstile> cap \<and> valid_objs s \<and> valid_objs s \<and> True proof (prove)
goal (2 subgoals):
 1. \<And>s r bits g bitsa ga. \<lbrakk>cap = cap.CNodeCap r bits g; s \<turnstile> cap.CNodeCap r bits g; valid_objs s; cte_wp_at (\<lambda>x. x = cap.CNodeCap r bitsa ga) (ba, c) s; \<not> cte_wp_at (\<lambda>c. obj_refs c = {r} \<and> table_cap_ref c \<noteq> table_cap_ref (cap.CNodeCap r bits g)) (ba, c) s\<rbrakk> \<Longrightarrow> bits_of (cap.CNodeCap r bitsa ga) = bits_of (cap.CNodeCap r bits g)
 2. \<And>s. \<lbrakk>Structures_A.is_cnode_cap cap; (\<forall>a b. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap) (a, b) s) \<and> s \<turnstile> cap \<and> valid_objs s\<rbrakk> \<Longrightarrow> (\<forall>a b. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap) (a, b) s) \<and> s \<turnstile> cap \<and> valid_objs s \<and> valid_objs s \<and> True proof (prove)
goal (2 subgoals):
 1. \<And>s r bits g bitsa ga. \<lbrakk>cap = cap.CNodeCap r bits g; s \<turnstile> cap.CNodeCap r bits g; valid_objs s; \<not> cte_wp_at (\<lambda>c. obj_refs c = {r} \<and> table_cap_ref c \<noteq> table_cap_ref (cap.CNodeCap r bits g)) (ba, c) s; \<exists>cap. cap = cap.CNodeCap r bitsa ga \<and> s \<turnstile> cap\<rbrakk> \<Longrightarrow> bits_of (cap.CNodeCap r bitsa ga) = bits_of (cap.CNodeCap r bits g)
 2. \<And>s. \<lbrakk>Structures_A.is_cnode_cap cap; (\<forall>a b. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap) (a, b) s) \<and> s \<turnstile> cap \<and> valid_objs s\<rbrakk> \<Longrightarrow> (\<forall>a b. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap) (a, b) s) \<and> s \<turnstile> cap \<and> valid_objs s \<and> valid_objs s \<and> True proof (prove)
goal (2 subgoals):
 1. \<And>s r bits g ga x12. \<lbrakk>0 < bits; length ga \<le> word_bits; kheap s r = Some (kernel_object.CNode bits x12); well_formed_cnode_n bits x12; cap = cap.CNodeCap r bits g; valid_objs s; \<not> cte_wp_at (\<lambda>c. obj_refs c = {r} \<and> table_cap_ref c \<noteq> table_cap_ref (cap.CNodeCap r bits g)) (ba, c) s; cap_aligned (cap.CNodeCap r bits g); cap_aligned (cap.CNodeCap r bits ga); length g \<le> word_bits\<rbrakk> \<Longrightarrow> bits_of (cap.CNodeCap r bits ga) = bits_of (cap.CNodeCap r bits g)
 2. \<And>s. \<lbrakk>Structures_A.is_cnode_cap cap; (\<forall>a b. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap) (a, b) s) \<and> s \<turnstile> cap \<and> valid_objs s\<rbrakk> \<Longrightarrow> (\<forall>a b. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap) (a, b) s) \<and> s \<turnstile> cap \<and> valid_objs s \<and> valid_objs s \<and> True proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>Structures_A.is_cnode_cap cap; (\<forall>a b. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap) (a, b) s) \<and> s \<turnstile> cap \<and> valid_objs s\<rbrakk> \<Longrightarrow> (\<forall>a b. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap) (a, b) s) \<and> s \<turnstile> cap \<and> valid_objs s \<and> valid_objs s \<and> True proof (prove)
goal:
No subgoals!