theory VSpace_R

lemma setCTE_vs_entry_align[wp]:
  "\<lbrace>\<lambda>s. ko_wp_at' (\<lambda>ko. P (vs_entry_align ko)) p s\<rbrace>
    setCTE ptr cte
  \<lbrace>\<lambda>rv. ko_wp_at' (\<lambda>ko. P (vs_entry_align ko)) p\<rbrace>" apply (clarsimp simp: setCTE_def setObject_def split_def
                        valid_def in_monad ko_wp_at'_def
             split del: if_split
                 elim!: rsubst[where P=P]) apply (drule(1) updateObject_cte_is_tcb_or_cte [OF _ refl, rotated]) apply (elim exE conjE disjE) apply (clarsimp simp: ps_clear_upd objBits_simps
                         lookupAround2_char1) apply (simp add:vs_entry_align_def) apply (clarsimp simp: ps_clear_upd objBits_simps vs_entry_align_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ko_wp_at' (\<lambda>ko. P (vs_entry_align ko)) p\<rbrace> setCTE ptr cte \<lbrace>\<lambda>rv. ko_wp_at' (\<lambda>ko. P (vs_entry_align ko)) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s ko a ba s'' obj'. \<lbrakk>ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); P (vs_entry_align ko); ps_clear p (objBitsKO ko) s; fst (lookupAround2 ptr (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject cte ba ptr a (snd (lookupAround2 ptr (ksPSpace s))) s)\<rbrakk> \<Longrightarrow> \<exists>ko. (if p = a then Some obj' else ksPSpace s p) = Some ko \<and> is_aligned p (objBitsKO ko) \<and> P (vs_entry_align ko) \<and> ps_clear p (objBitsKO ko) (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ko a ba s'' obj'. \<lbrakk>ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); P (vs_entry_align ko); ps_clear p (objBitsKO ko) s; fst (lookupAround2 ptr (ksPSpace s)) = Some (a, ba); (\<exists>tcb getF setF. ba = KOTCB tcb \<and> s'' = s \<and> tcb_cte_cases (ptr - a) = Some (getF, setF) \<and> obj' = KOTCB (setF (\<lambda>x. cte) tcb) \<and> is_aligned a tcbBlockSizeBits \<and> ps_clear a tcbBlockSizeBits s) \<or> (\<exists>cte'. ba = KOCTE cte' \<and> obj' = KOCTE cte \<and> s'' = s \<and> ptr = a \<and> is_aligned ptr cte_level_bits \<and> ps_clear ptr cte_level_bits s)\<rbrakk> \<Longrightarrow> \<exists>ko. (if p = a then Some obj' else ksPSpace s p) = Some ko \<and> is_aligned p (objBitsKO ko) \<and> P (vs_entry_align ko) \<and> ps_clear p (objBitsKO ko) (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s ko a ba s'' obj' tcb getF setF. \<lbrakk>ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); P (vs_entry_align ko); ps_clear p (objBitsKO ko) s; fst (lookupAround2 ptr (ksPSpace s)) = Some (a, ba); ba = KOTCB tcb; s'' = s; tcb_cte_cases (ptr - a) = Some (getF, setF); obj' = KOTCB (setF (\<lambda>x. cte) tcb); is_aligned a tcbBlockSizeBits; ps_clear a tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> \<exists>ko. (if p = a then Some obj' else ksPSpace s p) = Some ko \<and> is_aligned p (objBitsKO ko) \<and> P (vs_entry_align ko) \<and> ps_clear p (objBitsKO ko) (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>)
 2. \<And>s ko a ba s'' obj' cte'. \<lbrakk>ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); P (vs_entry_align ko); ps_clear p (objBitsKO ko) s; fst (lookupAround2 ptr (ksPSpace s)) = Some (a, ba); ba = KOCTE cte'; obj' = KOCTE cte; s'' = s; ptr = a; is_aligned ptr cte_level_bits; ps_clear ptr cte_level_bits s\<rbrakk> \<Longrightarrow> \<exists>ko. (if p = a then Some obj' else ksPSpace s p) = Some ko \<and> is_aligned p (objBitsKO ko) \<and> P (vs_entry_align ko) \<and> ps_clear p (objBitsKO ko) (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s tcb getF setF. \<lbrakk>P (vs_entry_align (KOTCB tcb)); tcb_cte_cases (ptr - p) = Some (getF, setF); is_aligned p tcbBlockSizeBits; ps_clear p tcbBlockSizeBits s; p \<le> ptr; ksPSpace s p = Some (KOTCB tcb); \<forall>z. p < z \<and> z \<le> ptr \<longrightarrow> ksPSpace s z = None\<rbrakk> \<Longrightarrow> P (vs_entry_align (KOTCB (setF (\<lambda>x. cte) tcb)))
 2. \<And>s ko a ba s'' obj' cte'. \<lbrakk>ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); P (vs_entry_align ko); ps_clear p (objBitsKO ko) s; fst (lookupAround2 ptr (ksPSpace s)) = Some (a, ba); ba = KOCTE cte'; obj' = KOCTE cte; s'' = s; ptr = a; is_aligned ptr cte_level_bits; ps_clear ptr cte_level_bits s\<rbrakk> \<Longrightarrow> \<exists>ko. (if p = a then Some obj' else ksPSpace s p) = Some ko \<and> is_aligned p (objBitsKO ko) \<and> P (vs_entry_align ko) \<and> ps_clear p (objBitsKO ko) (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ko a ba s'' obj' cte'. \<lbrakk>ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); P (vs_entry_align ko); ps_clear p (objBitsKO ko) s; fst (lookupAround2 ptr (ksPSpace s)) = Some (a, ba); ba = KOCTE cte'; obj' = KOCTE cte; s'' = s; ptr = a; is_aligned ptr cte_level_bits; ps_clear ptr cte_level_bits s\<rbrakk> \<Longrightarrow> \<exists>ko. (if p = a then Some obj' else ksPSpace s p) = Some ko \<and> is_aligned p (objBitsKO ko) \<and> P (vs_entry_align ko) \<and> ps_clear p (objBitsKO ko) (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>) proof (prove)
goal:
No subgoals!