theory Untyped_AI

lemma reset_untyped_cap_pred_tcb_at:
  "\<lbrace>invs and pred_tcb_at proj P t and cte_wp_at (\<lambda>cp. t \<notin> cap_range cp \<and> is_untyped_cap cp) slot\<rbrace>
   reset_untyped_cap slot
   \<lbrace>\<lambda>_. pred_tcb_at proj P t\<rbrace>, \<lbrace>\<lambda>_. pred_tcb_at proj P t\<rbrace>" apply (simp add: reset_untyped_cap_def) apply (rule hoare_pre) apply (wp mapME_x_inv_wp preemption_point_inv | simp add: unless_def)+ apply (simp add: delete_objects_def) apply (wp get_cap_wp hoare_vcg_const_imp_lift | simp)+ apply (auto simp: cte_wp_at_caps_of_state cap_range_def
                        bits_of_def is_cap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and pred_tcb_at proj P t and cte_wp_at (\<lambda>cp. t \<notin> cap_range cp \<and> is_untyped_cap cp) slot\<rbrace> reset_untyped_cap slot \<lbrace>\<lambda>_. pred_tcb_at proj P t\<rbrace>, \<lbrace>\<lambda>_. pred_tcb_at proj P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and pred_tcb_at proj P t and cte_wp_at (\<lambda>cp. t \<notin> cap_range cp \<and> is_untyped_cap cp) slot\<rbrace> doE cap <- liftE (get_cap slot);
if free_index_of cap = 0 then returnOk () else doE liftE $ delete_objects (obj_ref_of cap) (bits_of cap);
dev <- returnOk $ is_device_untyped_cap cap;
if dev \<or> bits_of cap < resetChunkBits then liftE $ do unless dev $ do_machine_op $ clearMemory (obj_ref_of cap) (2 ^ bits_of cap);
set_cap (UntypedCap dev (obj_ref_of cap) (bits_of cap) 0) slot
od else mapME_x (\<lambda>i. doE liftE $ do_machine_op $ clearMemory (obj_ref_of cap + (word_of_nat i << resetChunkBits)) (2 ^ resetChunkBits);
liftE $ set_cap (UntypedCap dev (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>_. pred_tcb_at proj P t\<rbrace>, \<lbrace>\<lambda>_. pred_tcb_at proj P t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> doE cap <- liftE (get_cap slot);
if free_index_of cap = 0 then returnOk () else doE liftE $ delete_objects (obj_ref_of cap) (bits_of cap);
dev <- returnOk $ is_device_untyped_cap cap;
if dev \<or> bits_of cap < resetChunkBits then liftE $ do unless dev $ do_machine_op $ clearMemory (obj_ref_of cap) (2 ^ bits_of cap);
set_cap (UntypedCap dev (obj_ref_of cap) (bits_of cap) 0) slot
od else mapME_x (\<lambda>i. doE liftE $ do_machine_op $ clearMemory (obj_ref_of cap + (word_of_nat i << resetChunkBits)) (2 ^ resetChunkBits);
liftE $ set_cap (UntypedCap dev (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>_. pred_tcb_at proj P t\<rbrace>, \<lbrace>\<lambda>_. pred_tcb_at proj P t\<rbrace>
 2. \<And>s. (invs and pred_tcb_at proj P t and cte_wp_at (\<lambda>cp. t \<notin> cap_range cp \<and> is_untyped_cap cp) slot) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>cap. 0 < free_index_of cap \<Longrightarrow> \<lbrace>?P'89 cap\<rbrace> delete_objects (obj_ref_of cap) (bits_of cap) \<lbrace>\<lambda>rv s. (is_device_untyped_cap cap \<longrightarrow> pred_tcb_at proj P t s) \<and> (bits_of cap < resetChunkBits \<longrightarrow> pred_tcb_at proj P t s) \<and> (\<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits \<longrightarrow> pred_tcb_at proj P t s)\<rbrace>
 2. \<lbrace>?Q\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> pred_tcb_at proj P t s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> True \<and> True \<and> ((\<lambda>s. is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits \<longrightarrow> True) and ?P'89 cap) s)\<rbrace>, \<lbrace>\<lambda>_. pred_tcb_at proj P t\<rbrace>
 3. \<And>s. (invs and pred_tcb_at proj P t and cte_wp_at (\<lambda>cp. t \<notin> cap_range cp \<and> is_untyped_cap cp) slot) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>cap. 0 < free_index_of cap \<Longrightarrow> \<lbrace>?P'89 cap\<rbrace> do y <- do_machine_op (freeMemory (obj_ref_of cap) (bits_of cap));
modify (detype {obj_ref_of cap..obj_ref_of cap + 2 ^ bits_of cap - 1})
od \<lbrace>\<lambda>rv s. (is_device_untyped_cap cap \<longrightarrow> pred_tcb_at proj P t s) \<and> (bits_of cap < resetChunkBits \<longrightarrow> pred_tcb_at proj P t s) \<and> (\<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits \<longrightarrow> pred_tcb_at proj P t s)\<rbrace>
 2. \<lbrace>?Q\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap s. (free_index_of cap = 0 \<longrightarrow> pred_tcb_at proj P t s) \<and> (free_index_of cap \<noteq> 0 \<longrightarrow> True \<and> True \<and> ((\<lambda>s. is_device_untyped_cap cap \<or> bits_of cap < resetChunkBits \<longrightarrow> True) and ?P'89 cap) s)\<rbrace>, \<lbrace>\<lambda>_. pred_tcb_at proj P t\<rbrace>
 3. \<And>s. (invs and pred_tcb_at proj P t and cte_wp_at (\<lambda>cp. t \<notin> cap_range cp \<and> is_untyped_cap cp) slot) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<and> pred_tcb_at proj P t s \<and> cte_wp_at (\<lambda>cp. t \<notin> cap_range cp \<and> is_untyped_cap cp) slot s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> 0 < free_index_of cap \<longrightarrow> (is_device_untyped_cap cap \<longrightarrow> obj_ref_of cap \<le> t \<longrightarrow> \<not> t \<le> obj_ref_of cap + 2 ^ bits_of cap - 1) \<and> (bits_of cap < resetChunkBits \<longrightarrow> obj_ref_of cap \<le> t \<longrightarrow> \<not> t \<le> obj_ref_of cap + 2 ^ bits_of cap - 1) \<and> (\<not> is_device_untyped_cap cap \<and> \<not> bits_of cap < resetChunkBits \<longrightarrow> obj_ref_of cap \<le> t \<longrightarrow> \<not> t \<le> obj_ref_of cap + 2 ^ bits_of cap - 1) proof (prove)
goal:
No subgoals!