theory Retype_AI

lemma retype_region_cte_at_other:
  assumes cover: "range_cover ptr' sz (obj_bits_api ty us) n"
  shows "\<lbrace>\<lambda>s. pspace_no_overlap_range_cover ptr' sz s \<and> cte_wp_at P ptr s \<and> valid_pspace s\<rbrace>
  retype_region ptr' n us ty dev \<lbrace>\<lambda>r. cte_wp_at P ptr\<rbrace>" unfolding retype_region_def apply (simp only: foldr_upd_app_if fun_app_def K_bind_def) apply wp apply (simp only: cte_wp_at_trans_state) apply wp+ apply (subst retype_addrs_fold) apply clarsimp apply (clarsimp simp: cte_wp_at_cases del: disjCI) apply (erule disjEI) apply (auto dest!: pspace_no_overlapD1[OF _ _ cover]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap (up_aligned_area ptr' sz) s \<and> cte_wp_at P ptr s \<and> valid_pspace s\<rbrace> retype_region ptr' n us ty dev \<lbrace>\<lambda>r. cte_wp_at P ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap (up_aligned_area ptr' sz) s \<and> cte_wp_at P ptr s \<and> valid_pspace s\<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. cte_wp_at P ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap (up_aligned_area ptr' sz) s \<and> cte_wp_at P ptr s \<and> valid_pspace s\<rbrace> do obj_size <- return (2 ^ obj_bits_api ty us);
ptrs <- return (map (\<lambda>p. ptr_add ptr' (p * obj_size)) [0..<n]);
y <- when (ty \<noteq> Untyped) (do kh <- gets kheap;
kh' <- return (\<lambda>x. if x \<in> set ptrs then Some (default_object ty dev us) else kh x);
y <- do_extended_op (retype_region_ext ptrs ty);
modify (kheap_update (K kh'))
od);
return ptrs
od \<lbrace>\<lambda>r. cte_wp_at P ptr\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>obj_size ptrs kh kh' s f. ty \<noteq> Untyped \<Longrightarrow> cte_wp_at P ptr (kheap_update (K kh') (trans_state f s)) = cte_wp_at P ptr (kheap_update (K kh') s)
 2. \<And>obj_size ptrs kh. ty \<noteq> Untyped \<Longrightarrow> \<lbrace>?B6 obj_size ptrs kh\<rbrace> return (\<lambda>x. if x \<in> set ptrs then Some (default_object ty dev us) else kh x) \<lbrace>\<lambda>kh' s. cte_wp_at P ptr (kheap_update (K kh') s)\<rbrace>
 3. \<And>obj_size ptrs. ty \<noteq> Untyped \<Longrightarrow> \<lbrace>?Q5 obj_size ptrs\<rbrace> gets kheap \<lbrace>?B6 obj_size ptrs\<rbrace>
 4. \<And>obj_size. \<lbrace>?B1 obj_size\<rbrace> return (map (\<lambda>p. ptr_add ptr' (p * obj_size)) [0..<n]) \<lbrace>\<lambda>ptrs. if ty \<noteq> Untyped then ?Q5 obj_size ptrs else cte_wp_at P ptr\<rbrace>
 5. \<lbrace>?Q\<rbrace> return (2 ^ obj_bits_api ty us) \<lbrace>?B1\<rbrace>
 6. \<And>s. pspace_no_overlap (up_aligned_area ptr' sz) s \<and> cte_wp_at P ptr s \<and> valid_pspace s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>obj_size ptrs kh. ty \<noteq> Untyped \<Longrightarrow> \<lbrace>?B6 obj_size ptrs kh\<rbrace> return (\<lambda>x. if x \<in> set ptrs then Some (default_object ty dev us) else kh x) \<lbrace>\<lambda>kh' s. cte_wp_at P ptr (kheap_update (K kh') s)\<rbrace>
 2. \<And>obj_size ptrs. ty \<noteq> Untyped \<Longrightarrow> \<lbrace>?Q5 obj_size ptrs\<rbrace> gets kheap \<lbrace>?B6 obj_size ptrs\<rbrace>
 3. \<And>obj_size. \<lbrace>?B1 obj_size\<rbrace> return (map (\<lambda>p. ptr_add ptr' (p * obj_size)) [0..<n]) \<lbrace>\<lambda>ptrs. if ty \<noteq> Untyped then ?Q5 obj_size ptrs else cte_wp_at P ptr\<rbrace>
 4. \<lbrace>?Q\<rbrace> return (2 ^ obj_bits_api ty us) \<lbrace>?B1\<rbrace>
 5. \<And>s. pspace_no_overlap (up_aligned_area ptr' sz) s \<and> cte_wp_at P ptr s \<and> valid_pspace s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_no_overlap (up_aligned_area ptr' sz) s \<and> cte_wp_at P ptr s \<and> valid_pspace s \<Longrightarrow> (if ty \<noteq> Untyped then \<lambda>s. cte_wp_at P ptr (kheap_update (K (\<lambda>a. if a \<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 a)) s) else cte_wp_at P ptr) s proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_no_overlap (up_aligned_area ptr' sz) s \<and> cte_wp_at P ptr s \<and> valid_pspace s \<Longrightarrow> (if ty \<noteq> Untyped then \<lambda>s. cte_wp_at P ptr (kheap_update (K (\<lambda>a. if a \<in> set (retype_addrs ptr' ty n us) then Some (default_object ty dev us) else kheap s a)) s) else cte_wp_at P ptr) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pspace_no_overlap (up_aligned_area ptr' sz) s; cte_wp_at P ptr s; valid_pspace s; ty \<noteq> Untyped\<rbrakk> \<Longrightarrow> cte_wp_at P ptr (s\<lparr>kheap := \<lambda>a. if a \<in> set (retype_addrs ptr' ty n us) then Some (default_object ty dev us) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pspace_no_overlap (up_aligned_area ptr' sz) s; (\<exists>sz fun. kheap s (fst ptr) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun (snd ptr) = Some cap \<and> P cap)) \<or> (\<exists>tcb. kheap s (fst ptr) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd ptr) = Some (get, set, restr)) \<and> P (get tcb))); valid_pspace s; ty \<noteq> Untyped; fst ptr \<in> set (retype_addrs ptr' ty n us)\<rbrakk> \<Longrightarrow> (\<exists>sz fun. default_object ty dev us = CNode sz fun \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun (snd ptr) = Some cap \<and> P cap)) \<or> (\<exists>tcb. default_object ty dev us = TCB tcb \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd ptr) = Some (get, set, restr)) \<and> P (get tcb))) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>pspace_no_overlap (up_aligned_area ptr' sz) s; valid_pspace s; ty \<noteq> Untyped; fst ptr \<in> set (retype_addrs ptr' ty n us); \<exists>sz fun. kheap s (fst ptr) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun (snd ptr) = Some cap \<and> P cap)\<rbrakk> \<Longrightarrow> \<exists>sz fun. default_object ty dev us = CNode sz fun \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun (snd ptr) = Some cap \<and> P cap)
 2. \<And>s. \<lbrakk>pspace_no_overlap (up_aligned_area ptr' sz) s; valid_pspace s; ty \<noteq> Untyped; fst ptr \<in> set (retype_addrs ptr' ty n us); \<exists>tcb. kheap s (fst ptr) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd ptr) = Some (get, set, restr)) \<and> P (get tcb))\<rbrakk> \<Longrightarrow> \<exists>tcb. default_object ty dev us = TCB tcb \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd ptr) = Some (get, set, restr)) \<and> P (get tcb)) proof (prove)
goal:
No subgoals!