theory FinalCaps

lemma reset_untyped_cap_untyped_cap:
  "\<lbrace>cte_wp_at (\<lambda>cp. is_untyped_cap cp \<and> P True (untyped_range cp)) slot and
    invs and (\<lambda>s. descendants_of slot (cdt s) = {})\<rbrace>
   reset_untyped_cap slot
   \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>cp. P (is_untyped_cap cp) (untyped_range cp)) slot\<rbrace>" apply (simp add: reset_untyped_cap_def cong: if_cong) apply (rule hoare_pre) apply (wp set_cap_cte_wp_at | simp add: unless_def)+ apply (rule valid_validE,
            rule_tac Q="\<lambda>rv. cte_wp_at (\<lambda>cp. is_untyped_cap cp \<and> is_untyped_cap cap \<and>
                                             untyped_range cp = untyped_range cap \<and>
                                             P True (untyped_range cp)) slot"
                  in hoare_strengthen_post) apply (wp mapME_x_inv_wp preemption_point_inv set_cap_cte_wp_at
            | simp add: if_apply_def2
            | clarsimp simp: cte_wp_at_caps_of_state is_cap_simps bits_of_def ptr_range_def[symmetric])+ apply (wp get_cap_wp) apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps ptr_range_def[symmetric]) apply (frule if_unsafe_then_capD[OF caps_of_state_cteD], clarsimp+) apply (drule ex_cte_cap_protects[OF _ _ _ _ order_refl], erule caps_of_state_cteD) apply (clarsimp simp: descendants_range_def2 empty_descendants_range_in) apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (\<lambda>cp. is_untyped_cap cp \<and> P True (untyped_range cp)) slot and invs and (\<lambda>s. descendants_of slot (cdt s) = {})\<rbrace> reset_untyped_cap slot \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>cp. P (is_untyped_cap cp) (untyped_range cp)) slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (\<lambda>cp. is_untyped_cap cp \<and> P True (untyped_range cp)) slot and invs and (\<lambda>s. descendants_of slot (cdt s) = {})\<rbrace> doE cap <- liftE (get_cap slot);
if free_index_of cap = 0 then returnOk () else doE y <- liftE (delete_objects (obj_ref_of cap) (bits_of cap));
if is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits then liftE (do y <- unless (is_device_untyped_cap cap) (do_machine_op (clearMemory (obj_ref_of cap) (2 ^ bits_of cap)));
set_cap (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0) slot
od) else mapME_x (\<lambda>i. doE y <- liftE (do_machine_op (clearMemory (obj_ref_of cap + (word_of_nat i << resetChunkBits)) (2 ^ resetChunkBits)));
y <- liftE (set_cap (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) (i * 2 ^ resetChunkBits)) slot);
preemption_point
odE) (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of cap) [0..<2 ^ (bits_of cap - resetChunkBits)]))
odE
odE \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>cp. P (is_untyped_cap cp) (untyped_range cp)) slot\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q6\<rbrace> doE cap <- liftE (get_cap slot);
if free_index_of cap = 0 then returnOk () else doE y <- liftE (delete_objects (obj_ref_of cap) (bits_of cap));
if is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits then liftE (do y <- unless (is_device_untyped_cap cap) (do_machine_op (clearMemory (obj_ref_of cap) (2 ^ bits_of cap)));
set_cap (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0) slot
od) else mapME_x (\<lambda>i. doE y <- liftE (do_machine_op (clearMemory (obj_ref_of cap + (word_of_nat i << resetChunkBits)) (2 ^ resetChunkBits)));
y <- liftE (set_cap (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) (i * 2 ^ resetChunkBits)) slot);
preemption_point
odE) (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of cap) [0..<2 ^ (bits_of cap - resetChunkBits)]))
odE
odE \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>cp. P (is_untyped_cap cp) (untyped_range cp)) slot\<rbrace>
 2. \<And>s. (cte_wp_at (\<lambda>cp. is_untyped_cap cp \<and> P True (untyped_range cp)) slot and invs and (\<lambda>s. descendants_of slot (cdt s) = {})) s \<Longrightarrow> ?Q6 s proof (prove)
goal (4 subgoals):
 1. \<And>cap. \<lbrakk>0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits\<rbrakk> \<Longrightarrow> \<lbrace>?R15 cap ()\<rbrace> mapME_x (\<lambda>i. doE y <- liftE (do_machine_op (clearMemory (obj_ref_of cap + (word_of_nat i << resetChunkBits)) (2 ^ resetChunkBits)));
y <- liftE (set_cap (UntypedCap False (obj_ref_of cap) (bits_of cap) (i * 2 ^ resetChunkBits)) slot);
preemption_point
odE) (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of cap) [0..<2 ^ (bits_of cap - resetChunkBits)])) \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>cp. P (is_untyped_cap cp) (untyped_range cp)) slot\<rbrace>, \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>cp. P (is_untyped_cap cp) (untyped_range cp)) slot\<rbrace>
 2. \<And>cap. free_index_of cap \<noteq> 0 \<Longrightarrow> \<lbrace>?R12 cap\<rbrace> liftE (delete_objects (obj_ref_of cap) (bits_of cap)) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits \<longrightarrow> (if is_device_untyped_cap cap then \<lambda>s. (if slot = slot then P (is_untyped_cap (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) (untyped_range (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) else cte_wp_at (\<lambda>cp. P (is_untyped_cap cp) (untyped_range cp)) slot s) \<and> cte_wp_at (\<lambda>_. True) slot s else (\<lambda>s. (if slot = slot then P (is_untyped_cap (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) (untyped_range (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) else cte_wp_at (\<lambda>a. P (is_untyped_cap a) (untyped_range a)) slot s) \<and> cte_wp_at (\<lambda>_. True) slot s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> ?R15 cap y s)\<rbrace>, \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>cp. P (is_untyped_cap cp) (untyped_range cp)) slot\<rbrace>
 3. \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> cte_wp_at (\<lambda>cp. P (is_untyped_cap cp) (untyped_range cp)) slot s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>cp. P (is_untyped_cap cp) (untyped_range cp)) slot\<rbrace>
 4. \<And>s. (cte_wp_at (\<lambda>cp. is_untyped_cap cp \<and> P True (untyped_range cp)) slot and invs and (\<lambda>s. descendants_of slot (cdt s) = {})) s \<Longrightarrow> ?Q6 s proof (prove)
goal (5 subgoals):
 1. \<And>cap. \<lbrakk>0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits\<rbrakk> \<Longrightarrow> \<lbrace>?R15 cap ()\<rbrace> mapME_x (\<lambda>i. doE y <- liftE (do_machine_op (clearMemory (obj_ref_of cap + (word_of_nat i << resetChunkBits)) (2 ^ resetChunkBits)));
y <- liftE (set_cap (UntypedCap False (obj_ref_of cap) (bits_of cap) (i * 2 ^ resetChunkBits)) slot);
preemption_point
odE) (rev (filter (\<lambda>i. i * 2 ^ resetChunkBits < free_index_of cap) [0..<2 ^ (bits_of cap - resetChunkBits)])) \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>cp. is_untyped_cap cp \<and> is_untyped_cap cap \<and> untyped_range cp = untyped_range cap \<and> P True (untyped_range cp)) slot\<rbrace>
 2. \<And>cap rv s. \<lbrakk>0 < free_index_of cap; \<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits; cte_wp_at (\<lambda>cp. is_untyped_cap cp \<and> is_untyped_cap cap \<and> untyped_range cp = untyped_range cap \<and> P True (untyped_range cp)) slot s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cp. P (is_untyped_cap cp) (untyped_range cp)) slot s
 3. \<And>cap. free_index_of cap \<noteq> 0 \<Longrightarrow> \<lbrace>?R12 cap\<rbrace> liftE (delete_objects (obj_ref_of cap) (bits_of cap)) \<lbrace>\<lambda>y s. (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits \<longrightarrow> (if is_device_untyped_cap cap then \<lambda>s. (if slot = slot then P (is_untyped_cap (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) (untyped_range (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) else cte_wp_at (\<lambda>cp. P (is_untyped_cap cp) (untyped_range cp)) slot s) \<and> cte_wp_at (\<lambda>_. True) slot s else (\<lambda>s. (if slot = slot then P (is_untyped_cap (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) (untyped_range (UntypedCap (is_device_untyped_cap cap) (obj_ref_of cap) (bits_of cap) 0)) else cte_wp_at (\<lambda>a. P (is_untyped_cap a) (untyped_range a)) slot s) \<and> cte_wp_at (\<lambda>_. True) slot s)) s) \<and> (\<not> (is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits) \<longrightarrow> ?R15 cap y s)\<rbrace>, \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>cp. P (is_untyped_cap cp) (untyped_range cp)) slot\<rbrace>
 4. \<lbrace>?Q6\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> cte_wp_at (\<lambda>cp. P (is_untyped_cap cp) (untyped_range cp)) slot s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> ?R12 cap s)\<rbrace>, \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>cp. P (is_untyped_cap cp) (untyped_range cp)) slot\<rbrace>
 5. \<And>s. (cte_wp_at (\<lambda>cp. is_untyped_cap cp \<and> P True (untyped_range cp)) slot and invs and (\<lambda>s. descendants_of slot (cdt s) = {})) s \<Longrightarrow> ?Q6 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q6\<rbrace> get_cap slot \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> (\<exists>cap. caps_of_state s slot = Some cap \<and> P (\<exists>dev r bits f. cap = UntypedCap dev r bits f) (untyped_range cap))) \<and> (0 < free_index_of cap \<longrightarrow> (is_device_untyped_cap cap \<longrightarrow> P True (ptr_range (obj_ref_of cap) (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits))) \<and> (is_device_untyped_cap cap \<longrightarrow> (\<exists>cap. caps_of_state s slot = Some cap)) \<and> (obj_ref_of cap \<le> fst slot \<longrightarrow> \<not> fst slot \<le> obj_ref_of cap + 2 ^ (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) - 1) \<and> ((case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) < resetChunkBits \<longrightarrow> P True (ptr_range (obj_ref_of cap) (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits))) \<and> ((case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) < resetChunkBits \<longrightarrow> (\<exists>cap. caps_of_state s slot = Some cap)) \<and> (obj_ref_of cap \<le> fst slot \<longrightarrow> \<not> fst slot \<le> obj_ref_of cap + 2 ^ (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) - 1) \<and> (\<not> is_device_untyped_cap cap \<and> \<not> (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) < resetChunkBits \<longrightarrow> (\<exists>capa. caps_of_state s slot = Some capa \<and> (\<exists>dev r bits f. capa = UntypedCap dev r bits f) \<and> (\<exists>dev r bits f. cap = UntypedCap dev r bits f) \<and> untyped_range capa = untyped_range cap \<and> P True (untyped_range capa))) \<and> (obj_ref_of cap \<le> fst slot \<longrightarrow> \<not> fst slot \<le> obj_ref_of cap + 2 ^ (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) - 1))\<rbrace>
 2. \<And>s. (cte_wp_at (\<lambda>cp. is_untyped_cap cp \<and> P True (untyped_range cp)) slot and invs and (\<lambda>s. descendants_of slot (cdt s) = {})) s \<Longrightarrow> ?Q6 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (cte_wp_at (\<lambda>cp. is_untyped_cap cp \<and> P True (untyped_range cp)) slot and invs and (\<lambda>s. descendants_of slot (cdt s) = {})) s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> (free_index_of cap = 0 \<longrightarrow> (\<exists>cap. caps_of_state s slot = Some cap \<and> P (\<exists>dev r bits f. cap = UntypedCap dev r bits f) (untyped_range cap))) \<and> (0 < free_index_of cap \<longrightarrow> (is_device_untyped_cap cap \<longrightarrow> P True (ptr_range (obj_ref_of cap) (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits))) \<and> (is_device_untyped_cap cap \<longrightarrow> (\<exists>cap. caps_of_state s slot = Some cap)) \<and> (obj_ref_of cap \<le> fst slot \<longrightarrow> \<not> fst slot \<le> obj_ref_of cap + 2 ^ (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) - 1) \<and> ((case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) < resetChunkBits \<longrightarrow> P True (ptr_range (obj_ref_of cap) (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits))) \<and> ((case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) < resetChunkBits \<longrightarrow> (\<exists>cap. caps_of_state s slot = Some cap)) \<and> (obj_ref_of cap \<le> fst slot \<longrightarrow> \<not> fst slot \<le> obj_ref_of cap + 2 ^ (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) - 1) \<and> (\<not> is_device_untyped_cap cap \<and> \<not> (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) < resetChunkBits \<longrightarrow> (\<exists>capa. caps_of_state s slot = Some capa \<and> (\<exists>dev r bits f. capa = UntypedCap dev r bits f) \<and> (\<exists>dev r bits f. cap = UntypedCap dev r bits f) \<and> untyped_range capa = untyped_range cap \<and> P True (untyped_range capa))) \<and> (obj_ref_of cap \<le> fst slot \<longrightarrow> \<not> fst slot \<le> obj_ref_of cap + 2 ^ (case cap of UntypedCap x xa bits xb \<Rightarrow> bits | CNodeCap x radix_bits xa \<Rightarrow> radix_bits) - 1)) proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f. \<lbrakk>invs s; descendants_of slot (cdt s) = {}; P True (ptr_range r bits); caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f); r \<le> fst slot; fst slot \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f. \<lbrakk>invs s; descendants_of slot (cdt s) = {}; P True (ptr_range r bits); caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f); r \<le> fst slot; fst slot \<le> r + 2 ^ bits - 1; ex_cte_cap_wp_to (appropriate_cte_cap (UntypedCap dev r bits f)) slot s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>s dev r bits f. \<lbrakk>invs s; descendants_of slot (cdt s) = {}; P True (ptr_range r bits); caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f); r \<le> fst slot; fst slot \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> descendants_range_in (untyped_range (UntypedCap dev r bits f)) slot s
 2. \<And>s dev r bits f. \<lbrakk>invs s; descendants_of slot (cdt s) = {}; P True (ptr_range r bits); caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f); r \<le> fst slot; fst slot \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> untyped_children_in_mdb s
 3. \<And>s dev r bits f. \<lbrakk>invs s; descendants_of slot (cdt s) = {}; P True (ptr_range r bits); caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f); r \<le> fst slot; fst slot \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> valid_global_refs s
 4. \<And>s dev r bits f. \<lbrakk>invs s; descendants_of slot (cdt s) = {}; P True (ptr_range r bits); caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f); r \<le> fst slot; fst slot \<le> r + 2 ^ bits - 1; fst slot \<notin> untyped_range (UntypedCap dev r bits f)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s dev r bits f. \<lbrakk>invs s; descendants_of slot (cdt s) = {}; P True (ptr_range r bits); caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f); r \<le> fst slot; fst slot \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> untyped_children_in_mdb s
 2. \<And>s dev r bits f. \<lbrakk>invs s; descendants_of slot (cdt s) = {}; P True (ptr_range r bits); caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f); r \<le> fst slot; fst slot \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> valid_global_refs s
 3. \<And>s dev r bits f. \<lbrakk>invs s; descendants_of slot (cdt s) = {}; P True (ptr_range r bits); caps_of_state s slot = Some (UntypedCap dev r bits f); 0 < free_index_of (UntypedCap dev r bits f); r \<le> fst slot; fst slot \<le> r + 2 ^ bits - 1; fst slot \<notin> untyped_range (UntypedCap dev r bits f)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!