theory Detype_R

lemma setCTE_pde_at':
  "\<lbrace>ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr and
    cte_wp_at' (\<lambda>_. True) src and pspace_distinct'\<rbrace>
   setCTE src cte
   \<lbrace>\<lambda>x s. ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrace>" apply (clarsimp simp:setCTE_def2) including no_pre apply wp apply (simp add:split_def) apply (clarsimp simp:valid_def) apply (subgoal_tac "b = s") prefer 2 apply (erule use_valid[OF _ locateCTE_inv]) apply simp apply (subgoal_tac "ptr \<noteq> a") apply (frule use_valid[OF _ locateCTE_ko_wp_at']) apply simp apply (clarsimp simp:ko_wp_at'_def ps_clear_def) apply (simp add:in_dom_eq) apply (drule use_valid[OF _ locateCTE_case]) apply simp apply (clarsimp simp:ko_wp_at'_def objBits_simps archObjSize_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct'\<rbrace> setCTE src cte \<lbrace>\<lambda>x. ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct'\<rbrace> do ptr <- locateCTE src;
modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> cte_update cte (the (ps ptr)) src ptr)))
od \<lbrace>\<lambda>x. ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct'\<rbrace> do ptr <- locateCTE src;
modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> cte_update cte (the (ps ptr)) src ptr)))
od \<lbrace>\<lambda>x. ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct'\<rbrace> locateCTE src \<lbrace>\<lambda>ptra s. ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr (ksPSpace_update (\<lambda>ps. ps(ptra \<mapsto> cte_update cte (the (ps ptra)) src ptra)) s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct'\<rbrace> locateCTE src \<lbrace>\<lambda>ptra s. ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr (ksPSpace_update (\<lambda>ps a. if a = ptra then Some (cte_update cte (the (ps ptra)) src ptra) else ps a) s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (locateCTE src s); ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s\<rbrakk> \<Longrightarrow> ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr (ksPSpace_update (\<lambda>ps b. if b = a then Some (cte_update cte (the (ps a)) src a) else ps b) b) proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (locateCTE src s); ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; b = s\<rbrakk> \<Longrightarrow> ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr (ksPSpace_update (\<lambda>ps b. if b = a then Some (cte_update cte (the (ps a)) src a) else ps b) b)
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (locateCTE src s); ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s\<rbrakk> \<Longrightarrow> b = s proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (locateCTE src s); ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s\<rbrakk> \<Longrightarrow> b = s
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (locateCTE src s); ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; b = s\<rbrakk> \<Longrightarrow> ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr (ksPSpace_update (\<lambda>ps b. if b = a then Some (cte_update cte (the (ps a)) src a) else ps b) b) proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s\<rbrakk> \<Longrightarrow> s = s
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (locateCTE src s); ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; b = s\<rbrakk> \<Longrightarrow> ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr (ksPSpace_update (\<lambda>ps b. if b = a then Some (cte_update cte (the (ps a)) src a) else ps b) b) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (locateCTE src s); ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; b = s\<rbrakk> \<Longrightarrow> ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr (ksPSpace_update (\<lambda>ps b. if b = a then Some (cte_update cte (the (ps a)) src a) else ps b) b) proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (locateCTE src s); ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; b = s; ptr \<noteq> a\<rbrakk> \<Longrightarrow> ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr (ksPSpace_update (\<lambda>ps b. if b = a then Some (cte_update cte (the (ps a)) src a) else ps b) b)
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (locateCTE src s); ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; b = s\<rbrakk> \<Longrightarrow> ptr \<noteq> a proof (prove)
goal (3 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (locateCTE src s); ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; b = s; ptr \<noteq> a\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) src and pspace_distinct') s
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (locateCTE src s); ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; b = s; ptr \<noteq> a; ko_wp_at' (\<lambda>_. True) a b\<rbrakk> \<Longrightarrow> ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr (ksPSpace_update (\<lambda>ps b. if b = a then Some (cte_update cte (the (ps a)) src a) else ps b) b)
 3. \<And>s a b. \<lbrakk>(a, b) \<in> fst (locateCTE src s); ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; b = s\<rbrakk> \<Longrightarrow> ptr \<noteq> a proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (locateCTE src s); ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; b = s; ptr \<noteq> a; ko_wp_at' (\<lambda>_. True) a b\<rbrakk> \<Longrightarrow> ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr (ksPSpace_update (\<lambda>ps b. if b = a then Some (cte_update cte (the (ps a)) src a) else ps b) b)
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (locateCTE src s); ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; b = s\<rbrakk> \<Longrightarrow> ptr \<noteq> a proof (prove)
goal (2 subgoals):
 1. \<And>s a ko. \<lbrakk>(a, s) \<in> fst (locateCTE src s); cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; ptr \<noteq> a; ksPSpace s ptr = Some (KOArch (KOPDE pde)); ksPSpace s a = Some ko; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ({ptr..ptr + 2 ^ objBitsKO (KOArch (KOPDE pde)) - 1} - {ptr}) \<inter> dom (ksPSpace s) = {}; is_aligned a (objBitsKO ko); ({a..a + 2 ^ objBitsKO ko - 1} - {a}) \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> ({ptr..ptr + 2 ^ objBitsKO (KOArch (KOPDE pde)) - 1} - {ptr}) \<inter> dom (\<lambda>b. if b = a then Some (cte_update cte (the (ksPSpace s a)) src a) else ksPSpace s b) = {}
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (locateCTE src s); ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; b = s\<rbrakk> \<Longrightarrow> ptr \<noteq> a proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (locateCTE src s); ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; b = s\<rbrakk> \<Longrightarrow> ptr \<noteq> a proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; b = s\<rbrakk> \<Longrightarrow> True
 2. \<And>s a b. \<lbrakk>ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; b = s; \<exists>obj. ksPSpace b a = Some obj \<and> (case obj of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False)\<rbrakk> \<Longrightarrow> ptr \<noteq> a proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; b = s; \<exists>obj. ksPSpace b a = Some obj \<and> (case obj of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False)\<rbrakk> \<Longrightarrow> ptr \<noteq> a proof (prove)
goal:
No subgoals!