theory Untyped_R

lemma updateCap_isUntypedCap_corres:
  "\<lbrakk>is_untyped_cap cap; isUntypedCap cap'; cap_relation cap cap'\<rbrakk>
   \<Longrightarrow> corres dc
         (cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and>
          cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src and valid_objs and
          pspace_aligned and pspace_distinct)
         (cte_at' (cte_map src) and pspace_distinct' and pspace_aligned')
         (set_cap cap src) (updateCap (cte_map src) cap')" apply (rule corres_name_pre) apply (simp add: updateCap_def) apply (frule state_relation_pspace_relation) apply (clarsimp simp: cte_wp_at_ctes_of) apply (frule pspace_relation_cte_wp_atI) apply (fastforce simp: cte_wp_at_ctes_of) apply simp apply clarify apply (frule cte_map_inj_eq) apply (fastforce simp: cte_wp_at_ctes_of cte_wp_at_caps_of_state)+ apply (clarsimp simp: is_cap_simps isCap_simps) apply (rule corres_guard_imp) apply (rule corres_symb_exec_r) apply (rule_tac F = "cteCap_update (\<lambda>_. capability.UntypedCap dev r bits f) ctea
        = cteCap_update (\<lambda>cap. capFreeIndex_update (\<lambda>_. f) (cteCap cte)) cte" in corres_gen_asm2) apply (rule_tac F = " (cap.UntypedCap dev r bits f) = free_index_update (\<lambda>_. f) c"
                      in corres_gen_asm) apply simp apply (rule setCTE_UntypedCap_corres) apply ((clarsimp simp: cte_wp_at_caps_of_state cte_wp_at_ctes_of)+)[3] apply (subst identity_eq) apply (wp getCTE_sp getCTE_get no_fail_getCTE)+ apply (clarsimp simp: cte_wp_at_ctes_of cte_wp_at_caps_of_state)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_untyped_cap cap; isUntypedCap cap'; cap_relation cap cap'\<rbrakk> \<Longrightarrow> corres dc (cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src and valid_objs and pspace_aligned and pspace_distinct) (cte_wp_at' (\<lambda>_. True) (cte_map src) and pspace_distinct' and pspace_aligned') (set_cap cap src) (updateCap (cte_map src) cap') proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>is_untyped_cap cap; isUntypedCap cap'; cap_relation cap cap'; (cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src and valid_objs and pspace_aligned and pspace_distinct) s; (cte_wp_at' (\<lambda>_. True) (cte_map src) and pspace_distinct' and pspace_aligned') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> corres dc ((=) s) ((=) s') (set_cap cap src) (updateCap (cte_map src) cap') proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>is_untyped_cap cap; isUntypedCap cap'; cap_relation cap cap'; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> corres dc ((=) s) ((=) s') (set_cap cap src) (do cte <- getCTE (cte_map src);
setCTE (cte_map src) (cteCap_update (\<lambda>_. cap') cte)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>is_untyped_cap cap; isUntypedCap cap'; cap_relation cap cap'; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s; cte_wp_at' (\<lambda>_. True) (cte_map src) s' \<and> pspace_distinct' s' \<and> pspace_aligned' s'; (s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s')\<rbrakk> \<Longrightarrow> corres dc ((=) s) ((=) s') (set_cap cap src) (do cte <- getCTE (cte_map src);
setCTE (cte_map src) (cteCap_update (\<lambda>_. cap') cte)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s s' cte. \<lbrakk>is_untyped_cap cap; isUntypedCap cap'; cap_relation cap cap'; (s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s; ctes_of s' (cte_map src) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s\<rbrakk> \<Longrightarrow> corres dc ((=) s) ((=) s') (set_cap cap src) (do cte <- getCTE (cte_map src);
setCTE (cte_map src) (cteCap_update (\<lambda>_. cap') cte)
od) proof (prove)
goal (3 subgoals):
 1. \<And>s s' cte. \<lbrakk>is_untyped_cap cap; isUntypedCap cap'; cap_relation cap cap'; (s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s; ctes_of s' (cte_map src) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s\<rbrakk> \<Longrightarrow> ctes_of s' (?x10 s s' cte) = Some (?cte10 s s' cte)
 2. \<And>s s' cte. \<lbrakk>is_untyped_cap cap; isUntypedCap cap'; cap_relation cap cap'; (s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s; ctes_of s' (cte_map src) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s\<rbrakk> \<Longrightarrow> valid_objs s
 3. \<And>s s' cte. \<lbrakk>is_untyped_cap cap; isUntypedCap cap'; cap_relation cap cap'; (s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s; ctes_of s' (cte_map src) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; \<exists>c slot. cte_wp_at ((=) c) slot s \<and> cap_relation c (cteCap (?cte10 s s' cte)) \<and> ?x10 s s' cte = cte_map slot\<rbrakk> \<Longrightarrow> corres dc ((=) s) ((=) s') (set_cap cap src) (do cte <- getCTE (cte_map src);
setCTE (cte_map src) (cteCap_update (\<lambda>_. cap') cte)
od) proof (prove)
goal (2 subgoals):
 1. \<And>s s' cte. \<lbrakk>is_untyped_cap cap; isUntypedCap cap'; cap_relation cap cap'; (s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s; ctes_of s' (cte_map src) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<And>s s' cte. \<lbrakk>is_untyped_cap cap; isUntypedCap cap'; cap_relation cap cap'; (s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s; ctes_of s' (cte_map src) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; \<exists>c slot. cte_wp_at ((=) c) slot s \<and> cap_relation c (cteCap cte) \<and> cte_map src = cte_map slot\<rbrakk> \<Longrightarrow> corres dc ((=) s) ((=) s') (set_cap cap src) (do cte <- getCTE (cte_map src);
setCTE (cte_map src) (cteCap_update (\<lambda>_. cap') cte)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s s' cte. \<lbrakk>is_untyped_cap cap; isUntypedCap cap'; cap_relation cap cap'; (s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s; ctes_of s' (cte_map src) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; \<exists>c slot. cte_wp_at ((=) c) slot s \<and> cap_relation c (cteCap cte) \<and> cte_map src = cte_map slot\<rbrakk> \<Longrightarrow> corres dc ((=) s) ((=) s') (set_cap cap src) (do cte <- getCTE (cte_map src);
setCTE (cte_map src) (cteCap_update (\<lambda>_. cap') cte)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s s' cte c a b. \<lbrakk>is_untyped_cap cap; isUntypedCap cap'; cap_relation cap cap'; (s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s; ctes_of s' (cte_map src) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); cte_map src = cte_map (a, b)\<rbrakk> \<Longrightarrow> corres dc ((=) s) ((=) s') (set_cap cap src) (do cte <- getCTE (cte_map src);
setCTE (cte_map src) (cteCap_update (\<lambda>_. cap') cte)
od) proof (prove)
goal (6 subgoals):
 1. \<And>s s' cte c a b. \<lbrakk>is_untyped_cap cap; isUntypedCap cap'; cap_relation cap cap'; (s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s; ctes_of s' (cte_map src) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); cte_map src = cte_map (a, b)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) src (?s20 s s' cte c a b)
 2. \<And>s s' cte c a b. \<lbrakk>is_untyped_cap cap; isUntypedCap cap'; cap_relation cap cap'; (s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s; ctes_of s' (cte_map src) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); cte_map src = cte_map (a, b)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (a, b) (?s20 s s' cte c a b)
 3. \<And>s s' cte c a b. \<lbrakk>is_untyped_cap cap; isUntypedCap cap'; cap_relation cap cap'; (s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s; ctes_of s' (cte_map src) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); cte_map src = cte_map (a, b)\<rbrakk> \<Longrightarrow> valid_objs (?s20 s s' cte c a b)
 4. \<And>s s' cte c a b. \<lbrakk>is_untyped_cap cap; isUntypedCap cap'; cap_relation cap cap'; (s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s; ctes_of s' (cte_map src) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); cte_map src = cte_map (a, b)\<rbrakk> \<Longrightarrow> pspace_aligned (?s20 s s' cte c a b)
 5. \<And>s s' cte c a b. \<lbrakk>is_untyped_cap cap; isUntypedCap cap'; cap_relation cap cap'; (s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s; ctes_of s' (cte_map src) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); cte_map src = cte_map (a, b)\<rbrakk> \<Longrightarrow> pspace_distinct (?s20 s s' cte c a b)
 6. \<And>s s' cte c a b. \<lbrakk>is_untyped_cap cap; isUntypedCap cap'; cap_relation cap cap'; (s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s; ctes_of s' (cte_map src) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); cte_map src = cte_map (a, b); src = (a, b)\<rbrakk> \<Longrightarrow> corres dc ((=) s) ((=) s') (set_cap cap src) (do cte <- getCTE (cte_map src);
setCTE (cte_map src) (cteCap_update (\<lambda>_. cap') cte)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s s' cte c a b. \<lbrakk>is_untyped_cap cap; isUntypedCap cap'; cap_relation cap cap'; (s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_ref_of c = obj_ref_of cap \<and> cap_bits c = cap_bits cap \<and> cap_is_device c = cap_is_device cap) src s; ctes_of s' (cte_map src) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); cte_map src = cte_map (a, b); src = (a, b)\<rbrakk> \<Longrightarrow> corres dc ((=) s) ((=) s') (set_cap cap src) (do cte <- getCTE (cte_map src);
setCTE (cte_map src) (cteCap_update (\<lambda>_. cap') cte)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s s' cte c a b dev r bits f. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> corres dc ((=) s) ((=) s') (set_cap (cap.UntypedCap dev r bits f) (a, b)) (do cte <- getCTE (cte_map (a, b));
setCTE (cte_map (a, b)) (cteCap_update (\<lambda>_. capability.UntypedCap dev r bits f) cte)
od) proof (prove)
goal (3 subgoals):
 1. \<And>s s' cte c a b dev r bits f. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> corres dc (?Q57 s s' cte c a b dev r bits f) (?Q'57 s s' cte c a b dev r bits f) (set_cap (cap.UntypedCap dev r bits f) (a, b)) (do cte <- getCTE (cte_map (a, b));
setCTE (cte_map (a, b)) (cteCap_update (\<lambda>_. capability.UntypedCap dev r bits f) cte)
od)
 2. \<And>s s' cte c a b dev r bits f sa. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f; s = sa\<rbrakk> \<Longrightarrow> ?Q57 s s' cte c a b dev r bits f sa
 3. \<And>s s' cte c a b dev r bits f sa. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f; s' = sa\<rbrakk> \<Longrightarrow> ?Q'57 s s' cte c a b dev r bits f sa proof (prove)
goal (6 subgoals):
 1. \<And>s s' cte c a b dev r bits f ctea. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> corres dc (?Q57 s s' cte c a b dev r bits f) (?Q'61 s s' cte c a b dev r bits f ctea) (set_cap (cap.UntypedCap dev r bits f) (a, b)) (setCTE (cte_map (a, b)) (cteCap_update (\<lambda>_. capability.UntypedCap dev r bits f) ctea))
 2. \<And>s s' cte c a b dev r bits f. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> \<lbrace>?Q'57 s s' cte c a b dev r bits f\<rbrace> getCTE (cte_map (a, b)) \<lbrace>?Q'61 s s' cte c a b dev r bits f\<rbrace>
 3. \<And>s s' cte c a b dev r bits f sa. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f; ?Q'57 s s' cte c a b dev r bits f sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> getCTE (cte_map (a, b)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>s s' cte c a b dev r bits f. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f; True\<rbrakk> \<Longrightarrow> no_fail (?Q'57 s s' cte c a b dev r bits f) (getCTE (cte_map (a, b)))
 5. \<And>s s' cte c a b dev r bits f sa. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f; s = sa\<rbrakk> \<Longrightarrow> ?Q57 s s' cte c a b dev r bits f sa
 6. \<And>s s' cte c a b dev r bits f sa. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f; s' = sa\<rbrakk> \<Longrightarrow> ?Q'57 s s' cte c a b dev r bits f sa proof (prove)
goal (6 subgoals):
 1. \<And>s s' cte c a b dev r bits f ctea. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f; cteCap_update (\<lambda>_. capability.UntypedCap dev r bits f) ctea = cteCap_update (\<lambda>cap. capFreeIndex_update (\<lambda>_. f) (cteCap cte)) cte\<rbrakk> \<Longrightarrow> corres dc (?Q57 s s' cte c a b dev r bits f) (?P'66 s s' cte c a b dev r bits f ctea) (set_cap (cap.UntypedCap dev r bits f) (a, b)) (setCTE (cte_map (a, b)) (cteCap_update (\<lambda>_. capability.UntypedCap dev r bits f) ctea))
 2. \<And>s s' cte c a b dev r bits f. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> \<lbrace>?Q'57 s s' cte c a b dev r bits f\<rbrace> getCTE (cte_map (a, b)) \<lbrace>\<lambda>ctea. ?P'66 s s' cte c a b dev r bits f ctea and (\<lambda>s. cteCap_update (\<lambda>_. capability.UntypedCap dev r bits f) ctea = cteCap_update (\<lambda>cap. capFreeIndex_update (\<lambda>_. f) (cteCap cte)) cte)\<rbrace>
 3. \<And>s s' cte c a b dev r bits f sa. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f; ?Q'57 s s' cte c a b dev r bits f sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> getCTE (cte_map (a, b)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>s s' cte c a b dev r bits f. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f; True\<rbrakk> \<Longrightarrow> no_fail (?Q'57 s s' cte c a b dev r bits f) (getCTE (cte_map (a, b)))
 5. \<And>s s' cte c a b dev r bits f sa. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f; s = sa\<rbrakk> \<Longrightarrow> ?Q57 s s' cte c a b dev r bits f sa
 6. \<And>s s' cte c a b dev r bits f sa. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f; s' = sa\<rbrakk> \<Longrightarrow> ?Q'57 s s' cte c a b dev r bits f sa proof (prove)
goal (6 subgoals):
 1. \<And>s s' cte c a b dev r bits f ctea. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f; cteCap_update (\<lambda>_. capability.UntypedCap dev r bits f) ctea = cteCap_update (\<lambda>cap. capFreeIndex_update (\<lambda>_. f) (cteCap cte)) cte; cap.UntypedCap dev r bits f = free_index_update (\<lambda>_. f) c\<rbrakk> \<Longrightarrow> corres dc (?P68 s s' cte c a b dev r bits f) (?P'66 s s' cte c a b dev r bits f ctea) (set_cap (cap.UntypedCap dev r bits f) (a, b)) (setCTE (cte_map (a, b)) (cteCap_update (\<lambda>_. capability.UntypedCap dev r bits f) ctea))
 2. \<And>s s' cte c a b dev r bits f. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> \<lbrace>?Q'57 s s' cte c a b dev r bits f\<rbrace> getCTE (cte_map (a, b)) \<lbrace>\<lambda>ctea. ?P'66 s s' cte c a b dev r bits f ctea and (\<lambda>s. cteCap_update (\<lambda>_. capability.UntypedCap dev r bits f) ctea = cteCap_update (\<lambda>cap. capFreeIndex_update (\<lambda>_. f) (cteCap cte)) cte)\<rbrace>
 3. \<And>s s' cte c a b dev r bits f sa. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f; ?Q'57 s s' cte c a b dev r bits f sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> getCTE (cte_map (a, b)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>s s' cte c a b dev r bits f. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f; True\<rbrakk> \<Longrightarrow> no_fail (?Q'57 s s' cte c a b dev r bits f) (getCTE (cte_map (a, b)))
 5. \<And>s s' cte c a b dev r bits f sa. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f; s = sa\<rbrakk> \<Longrightarrow> (?P68 s s' cte c a b dev r bits f and (\<lambda>s. cap.UntypedCap dev r bits f = free_index_update (\<lambda>_. f) c)) sa
 6. \<And>s s' cte c a b dev r bits f sa. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f; s' = sa\<rbrakk> \<Longrightarrow> ?Q'57 s s' cte c a b dev r bits f sa proof (prove)
goal (6 subgoals):
 1. \<And>s s' cte c a b dev r bits f ctea. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = free_index_update (\<lambda>_. f) c; cap' = capability.UntypedCap dev r bits f; cteCap_update (\<lambda>_. capability.UntypedCap dev r bits f) ctea = cteCap_update (\<lambda>cap. capFreeIndex_update (\<lambda>_. f) (cteCap cte)) cte; cap.UntypedCap dev r bits f = free_index_update (\<lambda>_. f) c\<rbrakk> \<Longrightarrow> corres dc (?P68 s s' cte c a b dev r bits f) (?P'66 s s' cte c a b dev r bits f ctea) (set_cap (free_index_update (\<lambda>_. f) c) (a, b)) (setCTE (cte_map (a, b)) (cteCap_update (\<lambda>cap. capFreeIndex_update (\<lambda>_. f) (cteCap cte)) cte))
 2. \<And>s s' cte c a b dev r bits f. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> \<lbrace>?Q'57 s s' cte c a b dev r bits f\<rbrace> getCTE (cte_map (a, b)) \<lbrace>\<lambda>ctea. ?P'66 s s' cte c a b dev r bits f ctea and (\<lambda>s. cteCap_update (\<lambda>_. capability.UntypedCap dev r bits f) ctea = cteCap_update (\<lambda>cap. capFreeIndex_update (\<lambda>_. f) (cteCap cte)) cte)\<rbrace>
 3. \<And>s s' cte c a b dev r bits f sa. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f; ?Q'57 s s' cte c a b dev r bits f sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> getCTE (cte_map (a, b)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>s s' cte c a b dev r bits f. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f; True\<rbrakk> \<Longrightarrow> no_fail (?Q'57 s s' cte c a b dev r bits f) (getCTE (cte_map (a, b)))
 5. \<And>s s' cte c a b dev r bits f sa. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f; s = sa\<rbrakk> \<Longrightarrow> (?P68 s s' cte c a b dev r bits f and (\<lambda>s. cap.UntypedCap dev r bits f = free_index_update (\<lambda>_. f) c)) sa
 6. \<And>s s' cte c a b dev r bits f sa. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f; s' = sa\<rbrakk> \<Longrightarrow> ?Q'57 s s' cte c a b dev r bits f sa proof (prove)
goal (8 subgoals):
 1. \<And>s s' cte c a b dev r bits f ctea. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = free_index_update (\<lambda>_. f) c; cap' = capability.UntypedCap dev r bits f; cteCap_update (\<lambda>_. capability.UntypedCap dev r bits f) ctea = cteCap_update (\<lambda>cap. capFreeIndex_update (\<lambda>_. f) (cteCap cte)) cte; cap.UntypedCap dev r bits f = free_index_update (\<lambda>_. f) c\<rbrakk> \<Longrightarrow> cap_relation c (cteCap cte)
 2. \<And>s s' cte c a b dev r bits f ctea. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = free_index_update (\<lambda>_. f) c; cap' = capability.UntypedCap dev r bits f; cteCap_update (\<lambda>_. capability.UntypedCap dev r bits f) ctea = cteCap_update (\<lambda>cap. capFreeIndex_update (\<lambda>_. f) (cteCap cte)) cte; cap.UntypedCap dev r bits f = free_index_update (\<lambda>_. f) c\<rbrakk> \<Longrightarrow> is_untyped_cap c
 3. \<And>s s' cte c a b dev r bits f ctea. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = free_index_update (\<lambda>_. f) c; cap' = capability.UntypedCap dev r bits f; cteCap_update (\<lambda>_. capability.UntypedCap dev r bits f) ctea = cteCap_update (\<lambda>cap. capFreeIndex_update (\<lambda>_. f) (cteCap cte)) cte; cap.UntypedCap dev r bits f = free_index_update (\<lambda>_. f) c\<rbrakk> \<Longrightarrow> f = f
 4. \<And>s s' cte c a b dev r bits f. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> \<lbrace>?Q'57 s s' cte c a b dev r bits f\<rbrace> getCTE (cte_map (a, b)) \<lbrace>\<lambda>ctea. cte_wp_at' ((=) cte) (cte_map (a, b)) and pspace_distinct' and pspace_aligned' and (\<lambda>s. cteCap_update (\<lambda>_. capability.UntypedCap dev r bits f) ctea = cteCap_update (\<lambda>cap. capFreeIndex_update (\<lambda>_. f) (cteCap cte)) cte)\<rbrace>
 5. \<And>s s' cte c a b dev r bits f sa. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f; ?Q'57 s s' cte c a b dev r bits f sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> getCTE (cte_map (a, b)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 6. \<And>s s' cte c a b dev r bits f. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f; True\<rbrakk> \<Longrightarrow> no_fail (?Q'57 s s' cte c a b dev r bits f) (getCTE (cte_map (a, b)))
 7. \<And>s s' cte c a b dev r bits f sa. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f; s = sa\<rbrakk> \<Longrightarrow> (cte_wp_at ((=) c) (a, b) and valid_objs and pspace_aligned and pspace_distinct and (\<lambda>s. cap.UntypedCap dev r bits f = free_index_update (\<lambda>_. f) c)) sa
 8. \<And>s s' cte c a b dev r bits f sa. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f; s' = sa\<rbrakk> \<Longrightarrow> ?Q'57 s s' cte c a b dev r bits f sa proof (prove)
goal (5 subgoals):
 1. \<And>s s' cte c a b dev r bits f. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> \<lbrace>?Q'57 s s' cte c a b dev r bits f\<rbrace> getCTE (cte_map (a, b)) \<lbrace>\<lambda>ctea. cte_wp_at' ((=) cte) (cte_map (a, b)) and pspace_distinct' and pspace_aligned' and (\<lambda>s. cteCap_update (\<lambda>_. capability.UntypedCap dev r bits f) ctea = cteCap_update (\<lambda>cap. capFreeIndex_update (\<lambda>_. f) (cteCap cte)) cte)\<rbrace>
 2. \<And>s s' cte c a b dev r bits f sa. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f; ?Q'57 s s' cte c a b dev r bits f sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> getCTE (cte_map (a, b)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 3. \<And>s s' cte c a b dev r bits f. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f; True\<rbrakk> \<Longrightarrow> no_fail (?Q'57 s s' cte c a b dev r bits f) (getCTE (cte_map (a, b)))
 4. \<And>s s' cte c a b dev r bits f sa. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f; s = sa\<rbrakk> \<Longrightarrow> (cte_wp_at ((=) c) (a, b) and valid_objs and pspace_aligned and pspace_distinct and (\<lambda>s. cap.UntypedCap dev r bits f = free_index_update (\<lambda>_. f) c)) sa
 5. \<And>s s' cte c a b dev r bits f sa. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f; s' = sa\<rbrakk> \<Longrightarrow> ?Q'57 s s' cte c a b dev r bits f sa proof (prove)
goal (5 subgoals):
 1. \<And>s s' cte c a b dev r bits f. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> \<lbrace>?Q'85 s s' cte c a b dev r bits f (?s85 s s' cte c a b dev r bits f) (?s'85 s s' cte c a b dev r bits f) cte (?c85 s s' cte c a b dev r bits f) a b dev r bits f\<rbrace> getCTE (cte_map (a, b)) \<lbrace>\<lambda>ctea. cte_wp_at' (\<lambda>c. c = cte) (cte_map (a, b)) and pspace_distinct' and pspace_aligned' and (\<lambda>s. cteCap_update (\<lambda>_. capability.UntypedCap dev r bits f) ctea = cteCap_update (\<lambda>cap. capFreeIndex_update (\<lambda>_. f) (cteCap cte)) cte)\<rbrace>
 2. \<And>s s' cte c a b dev r bits f sa. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f; ?Q'85 s s' cte c a b dev r bits f (?s85 s s' cte c a b dev r bits f) (?s'85 s s' cte c a b dev r bits f) cte (?c85 s s' cte c a b dev r bits f) a b dev r bits f sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> getCTE (cte_map (a, b)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 3. \<And>s s' cte c a b dev r bits f. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f; True\<rbrakk> \<Longrightarrow> no_fail (?Q'85 s s' cte c a b dev r bits f (?s85 s s' cte c a b dev r bits f) (?s'85 s s' cte c a b dev r bits f) cte (?c85 s s' cte c a b dev r bits f) a b dev r bits f) (getCTE (cte_map (a, b)))
 4. \<And>s s' cte c a b dev r bits f sa. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f; s = sa\<rbrakk> \<Longrightarrow> (cte_wp_at ((=) c) (a, b) and valid_objs and pspace_aligned and pspace_distinct and (\<lambda>s. cap.UntypedCap dev r bits f = free_index_update (\<lambda>_. f) c)) sa
 5. \<And>s s' cte c a b dev r bits f sa. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f; s' = sa\<rbrakk> \<Longrightarrow> ?Q'85 s s' cte c a b dev r bits f (?s85 s s' cte c a b dev r bits f) (?s'85 s s' cte c a b dev r bits f) cte (?c85 s s' cte c a b dev r bits f) a b dev r bits f sa proof (prove)
goal (3 subgoals):
 1. \<And>s s' cte c a b dev r bits f sa. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f; True; (cte_wp_at' (\<lambda>c. c = cte) (cte_map (a, b)) and pspace_distinct' and pspace_aligned') sa \<and> cte_wp_at' (\<lambda>a. cteCap_update (\<lambda>_. capability.UntypedCap dev r bits f) a = cteCap_update (\<lambda>cap. capFreeIndex_update (\<lambda>_. f) (cteCap cte)) cte) (cte_map (a, b)) sa\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (cte_map (a, b)) sa
 2. \<And>s s' cte c a b dev r bits f sa. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f; s = sa\<rbrakk> \<Longrightarrow> (cte_wp_at ((=) c) (a, b) and valid_objs and pspace_aligned and pspace_distinct and (\<lambda>s. cap.UntypedCap dev r bits f = free_index_update (\<lambda>_. f) c)) sa
 3. \<And>s s' cte c a b dev r bits f sa. \<lbrakk>(s, s') \<in> state_relation; pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>c. (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<and> obj_ref_of c = r \<and> cap_bits c = bits \<and> cap_is_device c = dev) (a, b) s; ctes_of s' (cte_map (a, b)) = Some cte; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); src = (a, b); cap = cap.UntypedCap dev r bits f; cap' = capability.UntypedCap dev r bits f; s' = sa\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>c. c = cte) (cte_map (a, b)) and pspace_distinct' and pspace_aligned') sa \<and> cte_wp_at' (\<lambda>a. cteCap_update (\<lambda>_. capability.UntypedCap dev r bits f) a = cteCap_update (\<lambda>cap. capFreeIndex_update (\<lambda>_. f) (cteCap cte)) cte) (cte_map (a, b)) sa proof (prove)
goal:
No subgoals!