theory Retype_AC

lemma retype_region_integrity:
  "\<lbrace>integrity aag X st and K (range_cover ptr sz (obj_bits_api type o_bits) num_objects \<and>
                              (\<forall>x\<in>{ptr..(ptr && ~~ mask sz) + (2 ^ sz - 1)}. is_subject aag x))\<rbrace>
   retype_region ptr num_objects o_bits type dev
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (rule hoare_gen_asm)+ apply (simp only: retype_region_def retype_region_ext_extended.dxo_eq) apply (simp only: retype_addrs_def retype_region_ext_def
                    foldr_upd_app_if' fun_app_def K_bind_def) apply wp apply (clarsimp simp: not_less) apply (erule integrity_trans) apply (clarsimp simp: integrity_def retype_region_integrity_asids) apply (fastforce intro: tro_lrefl tre_lrefl
                    dest: retype_addrs_subset_ptr_bits[simplified retype_addrs_def]
                    simp: image_def p_assoc_help power_sub) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and K (range_cover ptr sz (obj_bits_api type o_bits) num_objects \<and> (\<forall>x\<in>up_aligned_area ptr sz. is_subject aag x))\<rbrace> retype_region ptr num_objects o_bits type dev \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (obj_bits_api type o_bits) num_objects \<and> (\<forall>x\<in>up_aligned_area ptr sz. is_subject aag x) \<Longrightarrow> \<lbrace>integrity aag X st\<rbrace> retype_region ptr num_objects o_bits type dev \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (obj_bits_api type o_bits) num_objects \<and> (\<forall>x\<in>up_aligned_area ptr sz. is_subject aag x) \<Longrightarrow> \<lbrace>integrity aag X st\<rbrace> do obj_size <- return $ 2 ^ obj_bits_api type o_bits;
ptrs <- return $ map (\<lambda>p. ptr_add ptr (p * obj_size)) [0..<num_objects];
when (type \<noteq> Untyped) (do kh <- gets kheap;
kh' <- return $ foldr (\<lambda>p kh. kh(p \<mapsto> default_object type dev o_bits)) ptrs kh;
retype_region_ext ptrs type;
modify $ kheap_update (K kh')
od);
return $ ptrs
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (obj_bits_api type o_bits) num_objects \<and> (\<forall>x\<in>up_aligned_area ptr sz. is_subject aag x) \<Longrightarrow> \<lbrace>integrity aag X st\<rbrace> do obj_size <- return (2 ^ obj_bits_api type o_bits);
ptrs <- return (map (\<lambda>p. ptr_add ptr (p * obj_size)) [0..<num_objects]);
y <- when (type \<noteq> Untyped) (do kh <- gets kheap;
kh' <- return (\<lambda>x. if x \<in> set ptrs then Some (default_object type dev o_bits) else kh x);
y <- do ekh <- gets ekheap;
cdom <- gets cur_domain;
ekh' <- return (\<lambda>x. if x \<in> set ptrs then default_ext type cdom else ekh x);
modify (ekheap_update (\<lambda>_. ekh'))
od;
modify (kheap_update (K kh'))
od);
return ptrs
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects \<and> (\<forall>x\<in>up_aligned_area ptr sz. is_subject aag x); integrity aag X st s\<rbrakk> \<Longrightarrow> (if type \<noteq> Untyped then \<lambda>s. integrity aag X st (kheap_update (K (\<lambda>a. if a \<in> set (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<num_objects]) then Some (default_object type dev o_bits) else kheap s a)) (ekheap_update (\<lambda>_ a. if a \<in> set (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<num_objects]) then default_ext type (cur_domain s) else ekheap s a) s)) else integrity aag X st) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>integrity aag X st s; range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>ekheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then default_ext type (cur_domain s) else ekheap s a, kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped\<rbrakk> \<Longrightarrow> integrity aag X s (s\<lparr>ekheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then default_ext type (cur_domain s) else ekheap s a, kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} then Some (default_object type dev o_bits) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>range_cover ptr sz (obj_bits_api type o_bits) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; type \<noteq> Untyped\<rbrakk> \<Longrightarrow> (\<forall>x. x \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} \<longrightarrow> object_integrity aag (pasObjectAbs aag x) (kheap s x) (Some (default_object type dev o_bits))) \<and> (\<forall>x. x \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api type o_bits)) ` {0..<num_objects} \<longrightarrow> integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap s x) (default_ext type (cur_domain s))) proof (prove)
goal:
No subgoals!