theory Arch_R

lemma setTCB_pdpt_bits'[wp]:
 "\<lbrace>\<lambda>s. ko_wp_at' (\<lambda>ko. P (vs_entry_align ko)) p s\<rbrace>
   setObject a (tcb::tcb)
  \<lbrace>\<lambda>rv. ko_wp_at' (\<lambda>ko. P (vs_entry_align ko)) p\<rbrace>" apply (clarsimp simp: setObject_def split_def valid_def in_monad
                        projectKOs pspace_aligned'_def ps_clear_upd
                        objBits_def[symmetric] lookupAround2_char1
                 split: if_split_asm) apply (frule pspace_storable_class.updateObject_type[where v = tcb,simplified]) apply (clarsimp simp:ko_wp_at'_def) apply (intro conjI) subgoal by (clarsimp simp:updateObject_default_def assert_def bind_def
    alignCheck_def in_monad when_def alignError_def magnitudeCheck_def
    assert_opt_def return_def fail_def typeError_def objBits_simps
    vs_entry_align_def
    split:if_splits option.splits Structures_H.kernel_object.splits,
    ((erule(1) ps_clear_updE)+)) apply (clarsimp) apply (erule(1) ps_clear_updE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ko_wp_at' (\<lambda>ko. P (vs_entry_align ko)) p\<rbrace> setObject a tcb \<lbrace>\<lambda>rv. ko_wp_at' (\<lambda>ko. P (vs_entry_align ko)) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s aa ba s''a obj'. \<lbrakk>ko_wp_at' (\<lambda>ko. P (vs_entry_align ko)) p s; aa \<le> a; ksPSpace s aa = Some ba; \<forall>z. aa < z \<and> z \<le> a \<longrightarrow> ksPSpace s z = None; (obj', s''a) \<in> fst (updateObject_default tcb ba a aa (snd (lookupAround2 a (ksPSpace s))) s)\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. P (vs_entry_align ko)) p (s''a\<lparr>ksPSpace := (ksPSpace s)(aa \<mapsto> obj')\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s aa ba s''a obj'. \<lbrakk>ko_wp_at' (\<lambda>ko. P (vs_entry_align ko)) p s; aa \<le> a; ksPSpace s aa = Some ba; \<forall>z. aa < z \<and> z \<le> a \<longrightarrow> ksPSpace s z = None; (obj', s''a) \<in> fst (updateObject_default tcb ba a aa (snd (lookupAround2 a (ksPSpace s))) s); koTypeOf obj' = koTypeOf ba\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. P (vs_entry_align ko)) p (s''a\<lparr>ksPSpace := (ksPSpace s)(aa \<mapsto> obj')\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s aa ba s''a obj' ko. \<lbrakk>aa \<le> a; ksPSpace s aa = Some ba; \<forall>z. aa < z \<and> z \<le> a \<longrightarrow> ksPSpace s z = None; (obj', s''a) \<in> fst (updateObject_default tcb ba a aa (snd (lookupAround2 a (ksPSpace s))) s); koTypeOf obj' = koTypeOf ba; ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); P (vs_entry_align ko); ps_clear p (objBitsKO ko) s\<rbrakk> \<Longrightarrow> (p = aa \<longrightarrow> is_aligned aa (objBitsKO obj') \<and> P (vs_entry_align obj') \<and> ps_clear aa (objBitsKO obj') (s''a\<lparr>ksPSpace := (ksPSpace s)(aa \<mapsto> obj')\<rparr>)) \<and> (p \<noteq> aa \<longrightarrow> ps_clear p (objBitsKO ko) (s''a\<lparr>ksPSpace := (ksPSpace s)(aa \<mapsto> obj')\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>s aa ba s''a obj' ko. \<lbrakk>aa \<le> a; ksPSpace s aa = Some ba; \<forall>z. aa < z \<and> z \<le> a \<longrightarrow> ksPSpace s z = None; (obj', s''a) \<in> fst (updateObject_default tcb ba a aa (snd (lookupAround2 a (ksPSpace s))) s); koTypeOf obj' = koTypeOf ba; ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); P (vs_entry_align ko); ps_clear p (objBitsKO ko) s\<rbrakk> \<Longrightarrow> p = aa \<longrightarrow> is_aligned aa (objBitsKO obj') \<and> P (vs_entry_align obj') \<and> ps_clear aa (objBitsKO obj') (s''a\<lparr>ksPSpace := (ksPSpace s)(aa \<mapsto> obj')\<rparr>)
 2. \<And>s aa ba s''a obj' ko. \<lbrakk>aa \<le> a; ksPSpace s aa = Some ba; \<forall>z. aa < z \<and> z \<le> a \<longrightarrow> ksPSpace s z = None; (obj', s''a) \<in> fst (updateObject_default tcb ba a aa (snd (lookupAround2 a (ksPSpace s))) s); koTypeOf obj' = koTypeOf ba; ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); P (vs_entry_align ko); ps_clear p (objBitsKO ko) s\<rbrakk> \<Longrightarrow> p \<noteq> aa \<longrightarrow> ps_clear p (objBitsKO ko) (s''a\<lparr>ksPSpace := (ksPSpace s)(aa \<mapsto> obj')\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aa_ \<le> a; ksPSpace s_ aa_ = Some ba_; \<forall>z. aa_ < z \<and> z \<le> a \<longrightarrow> ksPSpace s_ z = None; (obj'_, s''a_) \<in> fst (updateObject_default tcb ba_ a aa_ (snd (lookupAround2 a (ksPSpace s_))) s_); koTypeOf obj'_ = koTypeOf ba_; ksPSpace s_ p = Some ko_; is_aligned p (objBitsKO ko_); P (vs_entry_align ko_); ps_clear p (objBitsKO ko_) s_\<rbrakk> \<Longrightarrow> p = aa_ \<longrightarrow> is_aligned aa_ (objBitsKO obj'_) \<and> P (vs_entry_align obj'_) \<and> ps_clear aa_ (objBitsKO obj'_) (s''a_\<lparr>ksPSpace := (ksPSpace s_)(aa_ \<mapsto> obj'_)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s aa ba s''a obj' ko. \<lbrakk>aa \<le> a; ksPSpace s aa = Some ba; \<forall>z. aa < z \<and> z \<le> a \<longrightarrow> ksPSpace s z = None; (obj', s''a) \<in> fst (updateObject_default tcb ba a aa (snd (lookupAround2 a (ksPSpace s))) s); koTypeOf obj' = koTypeOf ba; ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); P (vs_entry_align ko); ps_clear p (objBitsKO ko) s\<rbrakk> \<Longrightarrow> p \<noteq> aa \<longrightarrow> ps_clear p (objBitsKO ko) (s''a\<lparr>ksPSpace := (ksPSpace s)(aa \<mapsto> obj')\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s aa ba s''a obj' ko. \<lbrakk>aa \<le> a; ksPSpace s aa = Some ba; \<forall>z. aa < z \<and> z \<le> a \<longrightarrow> ksPSpace s z = None; (obj', s''a) \<in> fst (updateObject_default tcb ba a aa (snd (lookupAround2 a (ksPSpace s))) s); koTypeOf obj' = koTypeOf ba; ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); P (vs_entry_align ko); ps_clear p (objBitsKO ko) s; p \<noteq> aa\<rbrakk> \<Longrightarrow> ps_clear p (objBitsKO ko) (s''a\<lparr>ksPSpace := (ksPSpace s)(aa \<mapsto> obj')\<rparr>) proof (prove)
goal:
No subgoals!