theory DomainSepInv

lemma retype_region_neg_cte_wp_at_not_domain_sep_inv_cap:
  "retype_region  base n sz ty dev \<lbrace>\<lambda>s. \<not> cte_wp_at (not domain_sep_inv_cap irqs) slot s\<rbrace>" apply (rule hoare_pre) apply (simp only: retype_region_def retype_addrs_def foldr_upd_app_if fun_app_def K_bind_def) apply (wp dxo_wp_weak | simp)+ apply clarsimp apply (case_tac "fst slot \<in> (\<lambda>p. ptr_add base (p * 2 ^ obj_bits_api ty sz)) ` {0..<n}") apply clarsimp apply (erule cte_wp_atE) apply (clarsimp simp: default_object_def empty_cnode_def
                   split: apiobject_type.splits if_splits) apply (clarsimp simp: default_object_def default_tcb_def tcb_cap_cases_def
                  split: apiobject_type.splits if_splits) apply (fastforce elim: cte_wp_atE intro: cte_wp_at_tcbI cte_wp_at_cteI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> cte_wp_at (not domain_sep_inv_cap irqs) slot s\<rbrace> retype_region base n sz ty dev \<lbrace>\<lambda>_ s. \<not> cte_wp_at (not domain_sep_inv_cap irqs) slot s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> retype_region base n sz ty dev \<lbrace>\<lambda>_ s. \<not> cte_wp_at (not domain_sep_inv_cap irqs) slot s\<rbrace>
 2. \<And>s. \<not> cte_wp_at (not domain_sep_inv_cap irqs) slot s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do obj_size <- return (2 ^ obj_bits_api ty sz);
ptrs <- return (map (\<lambda>p. ptr_add base (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 sz) else kh x);
y <- do_extended_op (retype_region_ext ptrs ty);
modify (kheap_update (K kh'))
od);
return ptrs
od \<lbrace>\<lambda>_ s. \<not> cte_wp_at (not domain_sep_inv_cap irqs) slot s\<rbrace>
 2. \<And>s. \<not> cte_wp_at (not domain_sep_inv_cap irqs) slot s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<not> cte_wp_at (not domain_sep_inv_cap irqs) slot s \<Longrightarrow> ty \<noteq> Untyped \<longrightarrow> \<not> cte_wp_at (not domain_sep_inv_cap irqs) slot (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add base (x * 2 ^ obj_bits_api ty sz)) ` {0..<n} then Some (default_object ty dev sz) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<not> cte_wp_at (not domain_sep_inv_cap irqs) slot s; ty \<noteq> Untyped; cte_wp_at (not domain_sep_inv_cap irqs) slot (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add base (x * 2 ^ obj_bits_api ty sz)) ` {0..<n} then Some (default_object ty dev sz) else kheap s a\<rparr>)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<not> cte_wp_at (not domain_sep_inv_cap irqs) slot s; ty \<noteq> Untyped; cte_wp_at (not domain_sep_inv_cap irqs) slot (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add base (x * 2 ^ obj_bits_api ty sz)) ` {0..<n} then Some (default_object ty dev sz) else kheap s a\<rparr>); fst slot \<in> (\<lambda>p. ptr_add base (p * 2 ^ obj_bits_api ty sz)) ` {0..<n}\<rbrakk> \<Longrightarrow> False
 2. \<And>s. \<lbrakk>\<not> cte_wp_at (not domain_sep_inv_cap irqs) slot s; ty \<noteq> Untyped; cte_wp_at (not domain_sep_inv_cap irqs) slot (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add base (x * 2 ^ obj_bits_api ty sz)) ` {0..<n} then Some (default_object ty dev sz) else kheap s a\<rparr>); fst slot \<notin> (\<lambda>p. ptr_add base (p * 2 ^ obj_bits_api ty sz)) ` {0..<n}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s p. \<lbrakk>\<not> cte_wp_at (not domain_sep_inv_cap irqs) slot s; ty \<noteq> Untyped; cte_wp_at (not domain_sep_inv_cap irqs) slot (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add base (x * 2 ^ obj_bits_api ty sz)) ` {0..<n} then Some (default_object ty dev sz) else kheap s a\<rparr>); fst slot = ptr_add base (p * 2 ^ obj_bits_api ty sz); p < n\<rbrakk> \<Longrightarrow> False
 2. \<And>s. \<lbrakk>\<not> cte_wp_at (not domain_sep_inv_cap irqs) slot s; ty \<noteq> Untyped; cte_wp_at (not domain_sep_inv_cap irqs) slot (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add base (x * 2 ^ obj_bits_api ty sz)) ` {0..<n} then Some (default_object ty dev sz) else kheap s a\<rparr>); fst slot \<notin> (\<lambda>p. ptr_add base (p * 2 ^ obj_bits_api ty sz)) ` {0..<n}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s p sza fun cte. \<lbrakk>\<not> cte_wp_at (not domain_sep_inv_cap irqs) slot s; ty \<noteq> Untyped; fst slot = ptr_add base (p * 2 ^ obj_bits_api ty sz); p < n; kheap (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add base (x * 2 ^ obj_bits_api ty sz)) ` {0..<n} then Some (default_object ty dev sz) else kheap s a\<rparr>) (fst slot) = Some (CNode sza fun); well_formed_cnode_n sza fun; fun (snd slot) = Some cte; (not domain_sep_inv_cap irqs) cte\<rbrakk> \<Longrightarrow> False
 2. \<And>s p tcb getF setF restr. \<lbrakk>\<not> cte_wp_at (not domain_sep_inv_cap irqs) slot s; ty \<noteq> Untyped; fst slot = ptr_add base (p * 2 ^ obj_bits_api ty sz); p < n; kheap (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add base (x * 2 ^ obj_bits_api ty sz)) ` {0..<n} then Some (default_object ty dev sz) else kheap s a\<rparr>) (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); (not domain_sep_inv_cap irqs) (getF tcb)\<rbrakk> \<Longrightarrow> False
 3. \<And>s. \<lbrakk>\<not> cte_wp_at (not domain_sep_inv_cap irqs) slot s; ty \<noteq> Untyped; cte_wp_at (not domain_sep_inv_cap irqs) slot (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add base (x * 2 ^ obj_bits_api ty sz)) ` {0..<n} then Some (default_object ty dev sz) else kheap s a\<rparr>); fst slot \<notin> (\<lambda>p. ptr_add base (p * 2 ^ obj_bits_api ty sz)) ` {0..<n}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s p tcb getF setF restr. \<lbrakk>\<not> cte_wp_at (not domain_sep_inv_cap irqs) slot s; ty \<noteq> Untyped; fst slot = ptr_add base (p * 2 ^ obj_bits_api ty sz); p < n; kheap (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add base (x * 2 ^ obj_bits_api ty sz)) ` {0..<n} then Some (default_object ty dev sz) else kheap s a\<rparr>) (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); (not domain_sep_inv_cap irqs) (getF tcb)\<rbrakk> \<Longrightarrow> False
 2. \<And>s. \<lbrakk>\<not> cte_wp_at (not domain_sep_inv_cap irqs) slot s; ty \<noteq> Untyped; cte_wp_at (not domain_sep_inv_cap irqs) slot (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add base (x * 2 ^ obj_bits_api ty sz)) ` {0..<n} then Some (default_object ty dev sz) else kheap s a\<rparr>); fst slot \<notin> (\<lambda>p. ptr_add base (p * 2 ^ obj_bits_api ty sz)) ` {0..<n}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<not> cte_wp_at (not domain_sep_inv_cap irqs) slot s; ty \<noteq> Untyped; cte_wp_at (not domain_sep_inv_cap irqs) slot (s\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add base (x * 2 ^ obj_bits_api ty sz)) ` {0..<n} then Some (default_object ty dev sz) else kheap s a\<rparr>); fst slot \<notin> (\<lambda>p. ptr_add base (p * 2 ^ obj_bits_api ty sz)) ` {0..<n}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!