theory ADT_C

lemma cpspace_tcb_relation_unique:
  assumes tcbs: "cpspace_tcb_relation ah ch" "cpspace_tcb_relation ah' ch"
      and   vs: "\<exists>s. ksPSpace s = ah \<and> no_0_obj' s \<and> valid_objs' s"
      and   vs': "\<exists>s. ksPSpace s = ah' \<and> no_0_obj' s \<and> valid_objs' s"
  assumes ctes: " \<forall>tcb tcb'. (\<exists>p. map_to_tcbs ah p = Some tcb \<and>
                                  map_to_tcbs ah' p = Some tcb') \<longrightarrow>
                  (\<forall>x\<in>ran tcb_cte_cases. fst x tcb' = fst x tcb)"
  shows "map_to_tcbs ah' = map_to_tcbs ah" using tcbs(2) tcbs(1) apply (clarsimp simp add: cmap_relation_def) apply (drule inj_image_inv[OF inj_tcb_ptr_to_ctcb_ptr])+ apply (simp add: tcb_ptr_to_ctcb_ptr_def[abs_def] ctcb_offset_def) apply (rule ext) apply (case_tac "x:dom (map_to_tcbs ah)") apply (drule bspec, assumption)+ apply (simp add: dom_def Collect_eq, drule_tac x=x in spec) apply clarsimp apply (rename_tac p x y) apply (cut_tac ctes) apply (drule_tac x=x in spec, drule_tac x=y in spec, erule impE, fastforce) apply (frule ksPSpace_valid_objs_tcbBoundNotification_nonzero[OF vs]) apply (frule ksPSpace_valid_objs_tcbBoundNotification_nonzero[OF vs']) apply (thin_tac "map_to_tcbs x y = Some z" for x y z)+ apply (case_tac x, case_tac y, case_tac "the (clift ch (tcb_Ptr (p+0x100)))") apply (clarsimp simp: ctcb_relation_def ran_tcb_cte_cases) apply (clarsimp simp: option_to_ptr_def option_to_0_def split: option.splits) apply (auto simp: cfault_rel_imp_eq cthread_state_rel_imp_eq carch_tcb_relation_imp_eq
                     ccontext_relation_imp_eq up_ucast_inj_eq ctcb_size_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map_to_tcbs ah' = map_to_tcbs ah proof (prove)
using this:
cpspace_tcb_relation ah' ch
cpspace_tcb_relation ah ch

goal (1 subgoal):
 1. map_to_tcbs ah' = map_to_tcbs ah proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_ptr_to_ctcb_ptr ` dom (map_to_tcbs ah') = dom (clift ch); \<forall>x\<in>dom (map_to_tcbs ah'). ctcb_relation (the (map_to_tcbs ah' x)) (the (clift ch (tcb_ptr_to_ctcb_ptr x))); tcb_ptr_to_ctcb_ptr ` dom (map_to_tcbs ah) = dom (clift ch); \<forall>x\<in>dom (map_to_tcbs ah). ctcb_relation (the (map_to_tcbs ah x)) (the (clift ch (tcb_ptr_to_ctcb_ptr x)))\<rbrakk> \<Longrightarrow> map_to_tcbs ah' = map_to_tcbs ah proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>dom (map_to_tcbs ah'). ctcb_relation (the (map_to_tcbs ah' x)) (the (clift ch (tcb_ptr_to_ctcb_ptr x))); \<forall>x\<in>dom (map_to_tcbs ah). ctcb_relation (the (map_to_tcbs ah x)) (the (clift ch (tcb_ptr_to_ctcb_ptr x))); inv tcb_ptr_to_ctcb_ptr ` dom (clift ch) = dom (map_to_tcbs ah'); inv tcb_ptr_to_ctcb_ptr ` dom (clift ch) = dom (map_to_tcbs ah)\<rbrakk> \<Longrightarrow> map_to_tcbs ah' = map_to_tcbs ah proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>dom (map_to_tcbs ah). ctcb_relation (the (map_to_tcbs ah' x)) (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); \<forall>x\<in>dom (map_to_tcbs ah). ctcb_relation (the (map_to_tcbs ah x)) (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); inv (\<lambda>p. tcb_Ptr (p + 2 ^ ctcb_size_bits)) ` dom (clift ch) = dom (map_to_tcbs ah); dom (map_to_tcbs ah') = dom (map_to_tcbs ah)\<rbrakk> \<Longrightarrow> map_to_tcbs ah' = map_to_tcbs ah proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_tcbs ah). ctcb_relation (the (map_to_tcbs ah' x)) (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); \<forall>x\<in>dom (map_to_tcbs ah). ctcb_relation (the (map_to_tcbs ah x)) (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); inv (\<lambda>p. tcb_Ptr (p + 2 ^ ctcb_size_bits)) ` dom (clift ch) = dom (map_to_tcbs ah); dom (map_to_tcbs ah') = dom (map_to_tcbs ah)\<rbrakk> \<Longrightarrow> map_to_tcbs ah' x = map_to_tcbs ah x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_tcbs ah). ctcb_relation (the (map_to_tcbs ah' x)) (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); \<forall>x\<in>dom (map_to_tcbs ah). ctcb_relation (the (map_to_tcbs ah x)) (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); inv (\<lambda>p. tcb_Ptr (p + 2 ^ ctcb_size_bits)) ` dom (clift ch) = dom (map_to_tcbs ah); dom (map_to_tcbs ah') = dom (map_to_tcbs ah); x \<in> dom (map_to_tcbs ah)\<rbrakk> \<Longrightarrow> map_to_tcbs ah' x = map_to_tcbs ah x
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_tcbs ah). ctcb_relation (the (map_to_tcbs ah' x)) (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); \<forall>x\<in>dom (map_to_tcbs ah). ctcb_relation (the (map_to_tcbs ah x)) (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); inv (\<lambda>p. tcb_Ptr (p + 2 ^ ctcb_size_bits)) ` dom (clift ch) = dom (map_to_tcbs ah); dom (map_to_tcbs ah') = dom (map_to_tcbs ah); x \<notin> dom (map_to_tcbs ah)\<rbrakk> \<Longrightarrow> map_to_tcbs ah' x = map_to_tcbs ah x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>inv (\<lambda>p. tcb_Ptr (p + 2 ^ ctcb_size_bits)) ` dom (clift ch) = dom (map_to_tcbs ah); dom (map_to_tcbs ah') = dom (map_to_tcbs ah); x \<in> dom (map_to_tcbs ah); ctcb_relation (the (map_to_tcbs ah' x)) (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); ctcb_relation (the (map_to_tcbs ah x)) (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits))))\<rbrakk> \<Longrightarrow> map_to_tcbs ah' x = map_to_tcbs ah x
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_tcbs ah). ctcb_relation (the (map_to_tcbs ah' x)) (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); \<forall>x\<in>dom (map_to_tcbs ah). ctcb_relation (the (map_to_tcbs ah x)) (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); inv (\<lambda>p. tcb_Ptr (p + 2 ^ ctcb_size_bits)) ` dom (clift ch) = dom (map_to_tcbs ah); dom (map_to_tcbs ah') = dom (map_to_tcbs ah); x \<notin> dom (map_to_tcbs ah)\<rbrakk> \<Longrightarrow> map_to_tcbs ah' x = map_to_tcbs ah x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>inv (\<lambda>p. tcb_Ptr (p + 2 ^ ctcb_size_bits)) ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_tcbs ah a = Some y}; \<exists>y. map_to_tcbs ah x = Some y; ctcb_relation (the (map_to_tcbs ah' x)) (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); ctcb_relation (the (map_to_tcbs ah x)) (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); (\<exists>y. map_to_tcbs ah' x = Some y) = (\<exists>y. map_to_tcbs ah x = Some y)\<rbrakk> \<Longrightarrow> map_to_tcbs ah' x = map_to_tcbs ah x
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_tcbs ah). ctcb_relation (the (map_to_tcbs ah' x)) (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); \<forall>x\<in>dom (map_to_tcbs ah). ctcb_relation (the (map_to_tcbs ah x)) (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); inv (\<lambda>p. tcb_Ptr (p + 2 ^ ctcb_size_bits)) ` dom (clift ch) = dom (map_to_tcbs ah); dom (map_to_tcbs ah') = dom (map_to_tcbs ah); x \<notin> dom (map_to_tcbs ah)\<rbrakk> \<Longrightarrow> map_to_tcbs ah' x = map_to_tcbs ah x proof (prove)
goal (2 subgoals):
 1. \<And>x y ya. \<lbrakk>inv (\<lambda>p. tcb_Ptr (p + 2 ^ ctcb_size_bits)) ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_tcbs ah a = Some y}; ctcb_relation ya (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); ctcb_relation y (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); map_to_tcbs ah x = Some y; map_to_tcbs ah' x = Some ya\<rbrakk> \<Longrightarrow> ya = y
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_tcbs ah). ctcb_relation (the (map_to_tcbs ah' x)) (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); \<forall>x\<in>dom (map_to_tcbs ah). ctcb_relation (the (map_to_tcbs ah x)) (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); inv (\<lambda>p. tcb_Ptr (p + 2 ^ ctcb_size_bits)) ` dom (clift ch) = dom (map_to_tcbs ah); dom (map_to_tcbs ah') = dom (map_to_tcbs ah); x \<notin> dom (map_to_tcbs ah)\<rbrakk> \<Longrightarrow> map_to_tcbs ah' x = map_to_tcbs ah x proof (prove)
goal (2 subgoals):
 1. \<And>p x y. \<lbrakk>inv (\<lambda>p. tcb_Ptr (p + 2 ^ ctcb_size_bits)) ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_tcbs ah a = Some y}; ctcb_relation y (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); ctcb_relation x (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); map_to_tcbs ah p = Some x; map_to_tcbs ah' p = Some y\<rbrakk> \<Longrightarrow> y = x
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_tcbs ah). ctcb_relation (the (map_to_tcbs ah' x)) (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); \<forall>x\<in>dom (map_to_tcbs ah). ctcb_relation (the (map_to_tcbs ah x)) (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); inv (\<lambda>p. tcb_Ptr (p + 2 ^ ctcb_size_bits)) ` dom (clift ch) = dom (map_to_tcbs ah); dom (map_to_tcbs ah') = dom (map_to_tcbs ah); x \<notin> dom (map_to_tcbs ah)\<rbrakk> \<Longrightarrow> map_to_tcbs ah' x = map_to_tcbs ah x proof (prove)
goal (2 subgoals):
 1. \<And>p x y. \<lbrakk>inv (\<lambda>p. tcb_Ptr (p + 2 ^ ctcb_size_bits)) ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_tcbs ah a = Some y}; ctcb_relation y (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); ctcb_relation x (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); map_to_tcbs ah p = Some x; map_to_tcbs ah' p = Some y; \<forall>tcb tcb'. (\<exists>p. map_to_tcbs ah p = Some tcb \<and> map_to_tcbs ah' p = Some tcb') \<longrightarrow> (\<forall>x\<in>ran tcb_cte_cases. fst x tcb' = fst x tcb)\<rbrakk> \<Longrightarrow> y = x
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_tcbs ah). ctcb_relation (the (map_to_tcbs ah' x)) (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); \<forall>x\<in>dom (map_to_tcbs ah). ctcb_relation (the (map_to_tcbs ah x)) (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); inv (\<lambda>p. tcb_Ptr (p + 2 ^ ctcb_size_bits)) ` dom (clift ch) = dom (map_to_tcbs ah); dom (map_to_tcbs ah') = dom (map_to_tcbs ah); x \<notin> dom (map_to_tcbs ah)\<rbrakk> \<Longrightarrow> map_to_tcbs ah' x = map_to_tcbs ah x proof (prove)
goal (2 subgoals):
 1. \<And>p x y. \<lbrakk>inv (\<lambda>p. tcb_Ptr (p + 2 ^ ctcb_size_bits)) ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_tcbs ah a = Some y}; ctcb_relation y (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); ctcb_relation x (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); map_to_tcbs ah p = Some x; map_to_tcbs ah' p = Some y; \<forall>xa\<in>ran tcb_cte_cases. fst xa y = fst xa x\<rbrakk> \<Longrightarrow> y = x
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_tcbs ah). ctcb_relation (the (map_to_tcbs ah' x)) (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); \<forall>x\<in>dom (map_to_tcbs ah). ctcb_relation (the (map_to_tcbs ah x)) (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); inv (\<lambda>p. tcb_Ptr (p + 2 ^ ctcb_size_bits)) ` dom (clift ch) = dom (map_to_tcbs ah); dom (map_to_tcbs ah') = dom (map_to_tcbs ah); x \<notin> dom (map_to_tcbs ah)\<rbrakk> \<Longrightarrow> map_to_tcbs ah' x = map_to_tcbs ah x proof (prove)
goal (2 subgoals):
 1. \<And>p x y. \<lbrakk>inv (\<lambda>p. tcb_Ptr (p + 2 ^ ctcb_size_bits)) ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_tcbs ah a = Some y}; ctcb_relation y (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); ctcb_relation x (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); map_to_tcbs ah p = Some x; map_to_tcbs ah' p = Some y; \<forall>xa\<in>ran tcb_cte_cases. fst xa y = fst xa x; tcbBoundNotification x \<noteq> Some 0\<rbrakk> \<Longrightarrow> y = x
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_tcbs ah). ctcb_relation (the (map_to_tcbs ah' x)) (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); \<forall>x\<in>dom (map_to_tcbs ah). ctcb_relation (the (map_to_tcbs ah x)) (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); inv (\<lambda>p. tcb_Ptr (p + 2 ^ ctcb_size_bits)) ` dom (clift ch) = dom (map_to_tcbs ah); dom (map_to_tcbs ah') = dom (map_to_tcbs ah); x \<notin> dom (map_to_tcbs ah)\<rbrakk> \<Longrightarrow> map_to_tcbs ah' x = map_to_tcbs ah x proof (prove)
goal (2 subgoals):
 1. \<And>p x y. \<lbrakk>inv (\<lambda>p. tcb_Ptr (p + 2 ^ ctcb_size_bits)) ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_tcbs ah a = Some y}; ctcb_relation y (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); ctcb_relation x (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); map_to_tcbs ah p = Some x; map_to_tcbs ah' p = Some y; \<forall>xa\<in>ran tcb_cte_cases. fst xa y = fst xa x; tcbBoundNotification x \<noteq> Some 0; tcbBoundNotification y \<noteq> Some 0\<rbrakk> \<Longrightarrow> y = x
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_tcbs ah). ctcb_relation (the (map_to_tcbs ah' x)) (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); \<forall>x\<in>dom (map_to_tcbs ah). ctcb_relation (the (map_to_tcbs ah x)) (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); inv (\<lambda>p. tcb_Ptr (p + 2 ^ ctcb_size_bits)) ` dom (clift ch) = dom (map_to_tcbs ah); dom (map_to_tcbs ah') = dom (map_to_tcbs ah); x \<notin> dom (map_to_tcbs ah)\<rbrakk> \<Longrightarrow> map_to_tcbs ah' x = map_to_tcbs ah x proof (prove)
goal (2 subgoals):
 1. \<And>p x y. \<lbrakk>inv (\<lambda>p. tcb_Ptr (p + 2 ^ ctcb_size_bits)) ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_tcbs ah a = Some y}; ctcb_relation y (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); ctcb_relation x (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); \<forall>xa\<in>ran tcb_cte_cases. fst xa y = fst xa x; tcbBoundNotification x \<noteq> Some 0; tcbBoundNotification y \<noteq> Some 0\<rbrakk> \<Longrightarrow> y = x
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_tcbs ah). ctcb_relation (the (map_to_tcbs ah' x)) (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); \<forall>x\<in>dom (map_to_tcbs ah). ctcb_relation (the (map_to_tcbs ah x)) (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); inv (\<lambda>p. tcb_Ptr (p + 2 ^ ctcb_size_bits)) ` dom (clift ch) = dom (map_to_tcbs ah); dom (map_to_tcbs ah') = dom (map_to_tcbs ah); x \<notin> dom (map_to_tcbs ah)\<rbrakk> \<Longrightarrow> map_to_tcbs ah' x = map_to_tcbs ah x proof (prove)
goal (2 subgoals):
 1. \<And>p x y x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x1a x2a x3a x4a x5a x6a x7a x8a x9a x10a x11a x12a x13a x14a x15a x16a x1b x2b x3b x4b x5b x6b x7b x8b x9b x10b x11b x12b x13b x14b x15b. \<lbrakk>inv (\<lambda>p. tcb_Ptr (p + 2 ^ ctcb_size_bits)) ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_tcbs ah a = Some y}; ctcb_relation y (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); ctcb_relation x (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); \<forall>xa\<in>ran tcb_cte_cases. fst xa y = fst xa x; tcbBoundNotification x \<noteq> Some 0; tcbBoundNotification y \<noteq> Some 0; x = Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16; y = Thread x1a x2a x3a x4a x5a x6a x7a x8a x9a x10a x11a x12a x13a x14a x15a x16a; the (clift ch (tcb_Ptr (p + 0x100))) = tcb_C.tcb_C x1b x2b x3b x4b x5b x6b x7b x8b x9b x10b x11b x12b x13b x14b x15b\<rbrakk> \<Longrightarrow> y = x
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_tcbs ah). ctcb_relation (the (map_to_tcbs ah' x)) (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); \<forall>x\<in>dom (map_to_tcbs ah). ctcb_relation (the (map_to_tcbs ah x)) (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); inv (\<lambda>p. tcb_Ptr (p + 2 ^ ctcb_size_bits)) ` dom (clift ch) = dom (map_to_tcbs ah); dom (map_to_tcbs ah') = dom (map_to_tcbs ah); x \<notin> dom (map_to_tcbs ah)\<rbrakk> \<Longrightarrow> map_to_tcbs ah' x = map_to_tcbs ah x proof (prove)
goal (2 subgoals):
 1. \<And>p x6 x7 x8 x9 x11 x15 x16 x6a x7a x8a x9a x11a x15a x16a x1b x2b x3b x4b x5b x6b x7b x8b x9b x10b x11b x12b x13b x14b x15b. \<lbrakk>inv (\<lambda>p. tcb_Ptr (p + 2 ^ ctcb_size_bits)) ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_tcbs ah a = Some y}; x15 \<noteq> Some 0; x15a \<noteq> Some 0; the (clift ch (tcb_Ptr (p + 0x100))) = tcb_C.tcb_C x1b x2b x3b x4b x5b x6b x7b x8b x9b x10b x11b x12b x13b x14b x15b; cthread_state_relation x7a (tcbState_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))), tcbFault_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits))))); cthread_state_relation x7 (tcbState_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))), tcbFault_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits))))); carch_tcb_relation x16a (tcbArch_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits))))); carch_tcb_relation x16 (tcbArch_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits))))); UCAST(8 \<rightarrow> 32) x6a = tcbDomain_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); UCAST(8 \<rightarrow> 32) x6 = tcbDomain_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); UCAST(8 \<rightarrow> 32) x9a = tcbPriority_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); UCAST(8 \<rightarrow> 32) x9 = tcbPriority_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); UCAST(8 \<rightarrow> 32) x8a = tcbMCP_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); UCAST(8 \<rightarrow> 32) x8 = tcbMCP_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); cfault_rel x11a (seL4_Fault_lift (tcbFault_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))))) (lookup_fault_lift (tcbLookupFailure_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))))); option_to_ptr x15a = tcbBoundNotification_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); cfault_rel x11 (seL4_Fault_lift (tcbFault_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))))) (lookup_fault_lift (tcbLookupFailure_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))))); option_to_ptr x15 = tcbBoundNotification_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits))))\<rbrakk> \<Longrightarrow> x6a = x6 \<and> x7a = x7 \<and> x8a = x8 \<and> x9a = x9 \<and> x11a = x11 \<and> x15a = x15 \<and> x16a = x16
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_tcbs ah). ctcb_relation (the (map_to_tcbs ah' x)) (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); \<forall>x\<in>dom (map_to_tcbs ah). ctcb_relation (the (map_to_tcbs ah x)) (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); inv (\<lambda>p. tcb_Ptr (p + 2 ^ ctcb_size_bits)) ` dom (clift ch) = dom (map_to_tcbs ah); dom (map_to_tcbs ah') = dom (map_to_tcbs ah); x \<notin> dom (map_to_tcbs ah)\<rbrakk> \<Longrightarrow> map_to_tcbs ah' x = map_to_tcbs ah x proof (prove)
goal (5 subgoals):
 1. \<And>p x6 x7 x8 x9 x11 x16 x6a x7a x8a x9a x11a x16a x1b x2b x3b x4b x5b x6b x7b x8b x9b x10b x11b x12b x13b x14b x15b. \<lbrakk>inv (\<lambda>p. tcb_Ptr (p + 2 ^ ctcb_size_bits)) ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_tcbs ah a = Some y}; the (clift ch (tcb_Ptr (p + 0x100))) = tcb_C.tcb_C x1b x2b x3b x4b x5b x6b x7b x8b x9b x10b x11b x12b x13b x14b x15b; cthread_state_relation x7a (tcbState_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))), tcbFault_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits))))); cthread_state_relation x7 (tcbState_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))), tcbFault_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits))))); carch_tcb_relation x16a (tcbArch_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits))))); carch_tcb_relation x16 (tcbArch_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits))))); UCAST(8 \<rightarrow> 32) x6a = tcbDomain_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); UCAST(8 \<rightarrow> 32) x6 = tcbDomain_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); UCAST(8 \<rightarrow> 32) x9a = tcbPriority_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); UCAST(8 \<rightarrow> 32) x9 = tcbPriority_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); UCAST(8 \<rightarrow> 32) x8a = tcbMCP_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); UCAST(8 \<rightarrow> 32) x8 = tcbMCP_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); cfault_rel x11a (seL4_Fault_lift (tcbFault_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))))) (lookup_fault_lift (tcbLookupFailure_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))))); cfault_rel x11 (seL4_Fault_lift (tcbFault_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))))) (lookup_fault_lift (tcbLookupFailure_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))))); NULL = tcbBoundNotification_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits))))\<rbrakk> \<Longrightarrow> x6a = x6 \<and> x7a = x7 \<and> x8a = x8 \<and> x9a = x9 \<and> x11a = x11 \<and> x16a = x16
 2. \<And>p x6 x7 x8 x9 x11 x16 x6a x7a x8a x9a x11a x16a x1b x2b x3b x4b x5b x6b x7b x8b x9b x10b x11b x12b x13b x14b x15b x2. \<lbrakk>inv (\<lambda>p. tcb_Ptr (p + 2 ^ ctcb_size_bits)) ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_tcbs ah a = Some y}; 0 < x2; the (clift ch (tcb_Ptr (p + 0x100))) = tcb_C.tcb_C x1b x2b x3b x4b x5b x6b x7b x8b x9b x10b x11b x12b x13b x14b x15b; cthread_state_relation x7a (tcbState_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))), tcbFault_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits))))); cthread_state_relation x7 (tcbState_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))), tcbFault_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits))))); carch_tcb_relation x16a (tcbArch_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits))))); carch_tcb_relation x16 (tcbArch_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits))))); UCAST(8 \<rightarrow> 32) x6a = tcbDomain_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); UCAST(8 \<rightarrow> 32) x6 = tcbDomain_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); UCAST(8 \<rightarrow> 32) x9a = tcbPriority_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); UCAST(8 \<rightarrow> 32) x9 = tcbPriority_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); UCAST(8 \<rightarrow> 32) x8a = tcbMCP_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); UCAST(8 \<rightarrow> 32) x8 = tcbMCP_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); cfault_rel x11a (seL4_Fault_lift (tcbFault_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))))) (lookup_fault_lift (tcbLookupFailure_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))))); NULL = tcbBoundNotification_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); cfault_rel x11 (seL4_Fault_lift (tcbFault_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))))) (lookup_fault_lift (tcbLookupFailure_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))))); ntfn_Ptr x2 = tcbBoundNotification_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits))))\<rbrakk> \<Longrightarrow> False
 3. \<And>p x6 x7 x8 x9 x11 x16 x6a x7a x8a x9a x11a x16a x1b x2b x3b x4b x5b x6b x7b x8b x9b x10b x11b x12b x13b x14b x15b x2. \<lbrakk>inv (\<lambda>p. tcb_Ptr (p + 2 ^ ctcb_size_bits)) ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_tcbs ah a = Some y}; 0 < x2; the (clift ch (tcb_Ptr (p + 0x100))) = tcb_C.tcb_C x1b x2b x3b x4b x5b x6b x7b x8b x9b x10b x11b x12b x13b x14b x15b; cthread_state_relation x7a (tcbState_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))), tcbFault_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits))))); cthread_state_relation x7 (tcbState_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))), tcbFault_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits))))); carch_tcb_relation x16a (tcbArch_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits))))); carch_tcb_relation x16 (tcbArch_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits))))); UCAST(8 \<rightarrow> 32) x6a = tcbDomain_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); UCAST(8 \<rightarrow> 32) x6 = tcbDomain_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); UCAST(8 \<rightarrow> 32) x9a = tcbPriority_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); UCAST(8 \<rightarrow> 32) x9 = tcbPriority_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); UCAST(8 \<rightarrow> 32) x8a = tcbMCP_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); UCAST(8 \<rightarrow> 32) x8 = tcbMCP_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); cfault_rel x11a (seL4_Fault_lift (tcbFault_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))))) (lookup_fault_lift (tcbLookupFailure_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))))); ntfn_Ptr x2 = tcbBoundNotification_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); cfault_rel x11 (seL4_Fault_lift (tcbFault_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))))) (lookup_fault_lift (tcbLookupFailure_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))))); NULL = tcbBoundNotification_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits))))\<rbrakk> \<Longrightarrow> False
 4. \<And>p x6 x7 x8 x9 x11 x16 x6a x7a x8a x9a x11a x16a x1b x2b x3b x4b x5b x6b x7b x8b x9b x10b x11b x12b x13b x14b x15b x2 x2a. \<lbrakk>inv (\<lambda>p. tcb_Ptr (p + 2 ^ ctcb_size_bits)) ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_tcbs ah a = Some y}; 0 < x2a; 0 < x2; the (clift ch (tcb_Ptr (p + 0x100))) = tcb_C.tcb_C x1b x2b x3b x4b x5b x6b x7b x8b x9b x10b x11b x12b x13b x14b x15b; cthread_state_relation x7a (tcbState_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))), tcbFault_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits))))); cthread_state_relation x7 (tcbState_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))), tcbFault_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits))))); carch_tcb_relation x16a (tcbArch_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits))))); carch_tcb_relation x16 (tcbArch_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits))))); UCAST(8 \<rightarrow> 32) x6a = tcbDomain_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); UCAST(8 \<rightarrow> 32) x6 = tcbDomain_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); UCAST(8 \<rightarrow> 32) x9a = tcbPriority_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); UCAST(8 \<rightarrow> 32) x9 = tcbPriority_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); UCAST(8 \<rightarrow> 32) x8a = tcbMCP_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); UCAST(8 \<rightarrow> 32) x8 = tcbMCP_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); cfault_rel x11a (seL4_Fault_lift (tcbFault_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))))) (lookup_fault_lift (tcbLookupFailure_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))))); ntfn_Ptr x2 = tcbBoundNotification_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))); cfault_rel x11 (seL4_Fault_lift (tcbFault_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))))) (lookup_fault_lift (tcbLookupFailure_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))))); ntfn_Ptr x2a = tcbBoundNotification_C (the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits))))\<rbrakk> \<Longrightarrow> x6a = x6 \<and> x7a = x7 \<and> x8a = x8 \<and> x9a = x9 \<and> x11a = x11 \<and> x2 = x2a \<and> x16a = x16
 5. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_tcbs ah). ctcb_relation (the (map_to_tcbs ah' x)) (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); \<forall>x\<in>dom (map_to_tcbs ah). ctcb_relation (the (map_to_tcbs ah x)) (the (clift ch (tcb_Ptr (x + 2 ^ ctcb_size_bits)))); inv (\<lambda>p. tcb_Ptr (p + 2 ^ ctcb_size_bits)) ` dom (clift ch) = dom (map_to_tcbs ah); dom (map_to_tcbs ah') = dom (map_to_tcbs ah); x \<notin> dom (map_to_tcbs ah)\<rbrakk> \<Longrightarrow> map_to_tcbs ah' x = map_to_tcbs ah x proof (prove)
goal:
No subgoals!