theory Retype_C

lemma insertNewCap_ccorres:
  "ccorres dc xfdc (pspace_aligned' and valid_mdb' and cte_wp_at' (\<lambda>_. True) slot
          and valid_objs' and valid_cap' cap)
     ({s. cap_get_tag (cap_' s) = scast cap_untyped_cap
         \<longrightarrow> (case untypedZeroRange (cap_to_H (the (cap_lift (cap_' s)))) of None \<Rightarrow> True
          | Some (a, b) \<Rightarrow> region_actually_is_zero_bytes a (unat ((b + 1) - a)) s)}
       \<inter> {s. ccap_relation cap (cap_' s)} \<inter> {s. parent_' s = Ptr parent}
       \<inter> {s. slot_' s = Ptr slot}) []
     (insertNewCap parent slot cap)
     (Call insertNewCap_'proc)"
  (is "ccorres _ _ ?P ?P' _ _ _") apply (rule ccorres_guard_imp2, rule insertNewCap_ccorres1) apply (clarsimp simp: cap_get_tag_isCap) apply (clarsimp simp: ccap_relation_def map_option_Some_eq2) apply (simp add: untypedZeroRange_def Let_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (pspace_aligned' and valid_mdb' and cte_wp_at' (\<lambda>_. True) slot and valid_objs' and valid_cap' cap) ({s. cap_get_tag (cap_' s) = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<longrightarrow> (case untypedZeroRange (cap_to_H (the (cap_lift (cap_' s)))) of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0)} \<inter> \<lbrace>ccap_relation cap \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>parent = cte_Ptr parent\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace>) [] (insertNewCap parent slot cap) (Call insertNewCap_'proc) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (pspace_aligned' and valid_mdb' and cte_wp_at' (\<lambda>_. True) slot and valid_objs' and valid_cap' cap) s; s' \<in> {s. cap_get_tag (cap_' s) = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<longrightarrow> (case untypedZeroRange (cap_to_H (the (cap_lift (cap_' s)))) of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0)} \<inter> \<lbrace>ccap_relation cap \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>parent = cte_Ptr parent\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace>\<rbrakk> \<Longrightarrow> (pspace_aligned' and valid_mdb' and valid_objs' and valid_cap' cap) s \<and> s' \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0} \<inter> \<lbrace>ccap_relation cap \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>parent = cte_Ptr parent\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; pspace_aligned' s; isUntypedCap cap \<longrightarrow> (case untypedZeroRange (cap_to_H (the (cap_lift (cap_' s')))) of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s' \<and> heap_list (hrs_mem (t_hrs_' (globals s'))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0); valid_mdb' s; ccap_relation cap (cap_' s'); cte_wp_at' (\<lambda>_. True) slot s; parent_' s' = cte_Ptr parent; slot_' s' = cte_Ptr slot; valid_objs' s; valid_cap' cap s\<rbrakk> \<Longrightarrow> case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s' \<and> heap_list (hrs_mem (t_hrs_' (globals s'))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0 proof (prove)
goal (1 subgoal):
 1. \<And>s s' z. \<lbrakk>(s, s') \<in> rf_sr; pspace_aligned' s; valid_mdb' s; cte_wp_at' (\<lambda>_. True) slot s; parent_' s' = cte_Ptr parent; slot_' s' = cte_Ptr slot; valid_objs' s; valid_cap' (cap_to_H z) s; c_valid_cap (cap_' s'); cap_lift (cap_' s') = Some z; cap = cap_to_H z; \<not> isUntypedCap (cap_to_H z)\<rbrakk> \<Longrightarrow> case untypedZeroRange (cap_to_H z) of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s' \<and> heap_list (hrs_mem (t_hrs_' (globals s'))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0 proof (prove)
goal:
No subgoals!