theory Retype_AI

lemma retype_region_obj_at:
  assumes tyunt: "ty \<noteq> Structures_A.apiobject_type.Untyped"
  shows "\<lbrace>\<top>\<rbrace> retype_region ptr n us ty dev
  \<lbrace>\<lambda>r s. \<forall>x \<in> set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = default_object ty dev us) x s\<rbrace>" using tyunt unfolding retype_region_def apply (simp only: return_bind bind_return foldr_upd_app_if fun_app_def K_bind_def) apply wp apply (simp only: obj_at_kheap_trans_state) apply wp apply (simp only: simp_thms if_True) apply (rule ballI) apply (subst retype_addrs_fold) apply simp apply (unfold obj_at_def) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>r s. \<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = default_object ty dev us) x s\<rbrace> proof (prove)
using this:
ty \<noteq> Untyped

goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>r s. \<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = default_object ty dev us) x s\<rbrace> proof (prove)
using this:
ty \<noteq> Untyped

goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do obj_size <- return $ 2 ^ obj_bits_api ty us;
ptrs <- return $ map (\<lambda>p. ptr_add ptr (p * obj_size)) [0..<n];
when (ty \<noteq> Untyped) (do kh <- gets kheap;
kh' <- return $ foldr (\<lambda>p kh. kh(p \<mapsto> default_object ty dev us)) ptrs kh;
do_extended_op (retype_region_ext ptrs ty);
modify $ kheap_update (K kh')
od);
return $ ptrs
od \<lbrace>\<lambda>r s. \<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = default_object ty dev us) x s\<rbrace> proof (prove)
goal (1 subgoal):
 1. ty \<noteq> Untyped \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do y <- when (\<not> False) (do kh <- gets kheap;
y <- do_extended_op (retype_region_ext (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n]) ty);
modify (kheap_update (K (\<lambda>x. if x \<in> set (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n]) then Some (default_object ty dev us) else kh x)))
od);
return (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n])
od \<lbrace>\<lambda>r s. \<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = default_object ty dev us) x s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>kh s f. \<lbrakk>ty \<noteq> Untyped; \<not> False\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = default_object ty dev us) x (kheap_update (K (\<lambda>x. if x \<in> set (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n]) then Some (default_object ty dev us) else kh x)) (trans_state f s))) = (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = default_object ty dev us) x (kheap_update (K (\<lambda>x. if x \<in> set (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n]) then Some (default_object ty dev us) else kh x)) s))
 2. \<lbrakk>ty \<noteq> Untyped; \<not> False\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> gets kheap \<lbrace>\<lambda>kh s. \<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = default_object ty dev us) x (kheap_update (K (\<lambda>x. if x \<in> set (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n]) then Some (default_object ty dev us) else kh x)) s)\<rbrace>
 3. \<And>s. \<lbrakk>ty \<noteq> Untyped; True\<rbrakk> \<Longrightarrow> (if \<not> False then ?Q4 else (\<lambda>a. \<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = default_object ty dev us) x a)) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ty \<noteq> Untyped; \<not> False\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> gets kheap \<lbrace>\<lambda>kh s. \<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = default_object ty dev us) x (kheap_update (K (\<lambda>x. if x \<in> set (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n]) then Some (default_object ty dev us) else kh x)) s)\<rbrace>
 2. \<And>s. \<lbrakk>ty \<noteq> Untyped; True\<rbrakk> \<Longrightarrow> (if \<not> False then ?Q4 else (\<lambda>a. \<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = default_object ty dev us) x a)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>ty \<noteq> Untyped; True\<rbrakk> \<Longrightarrow> (if \<not> False then \<lambda>s. \<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = default_object ty dev us) x (kheap_update (K (\<lambda>x. if x \<in> set (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n]) then Some (default_object ty dev us) else kheap s x)) s) else (\<lambda>a. \<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = default_object ty dev us) x a)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>ty \<noteq> Untyped; True\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = default_object ty dev us) x (kheap_update (K (\<lambda>x. if x \<in> set (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n]) then Some (default_object ty dev us) else kheap s x)) s) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>ty \<noteq> Untyped; True; x \<in> set (retype_addrs ptr ty n us)\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. ko = default_object ty dev us) x (kheap_update (K (\<lambda>x. if x \<in> set (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n]) then Some (default_object ty dev us) else kheap s x)) s) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>ty \<noteq> Untyped; True; x \<in> set (retype_addrs ptr ty n us)\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. ko = default_object ty dev us) x (kheap_update (K (\<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x)) s) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>ty \<noteq> Untyped; x \<in> set (retype_addrs ptr ty n us)\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. ko = default_object ty dev us) x (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>ty \<noteq> Untyped; x \<in> set (retype_addrs ptr ty n us)\<rbrakk> \<Longrightarrow> \<exists>ko. kheap (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) x = Some ko \<and> ko = default_object ty dev us proof (prove)
goal:
No subgoals!