theory KHeap_R

lemma setObject_idle':
  fixes v :: "'a :: pspace_storable"
  assumes R: "\<And>ko s x y n. (updateObject v ko ptr y n s)
                   = (updateObject_default v ko ptr y n s)"
  assumes n: "\<And>x :: 'a. objBits x = n"
  assumes m: "(1 :: word32) < 2 ^ n"
  assumes z: "\<And>P p q n ko.
       \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> updateObject v p q n ko
       \<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace>"
  shows      "\<lbrace>\<lambda>s. valid_idle' s \<and>
                   (ptr = ksIdleThread s
                        \<longrightarrow> (\<exists>val :: 'a. idle_tcb_ps val)
                        \<longrightarrow> idle_tcb_ps v)\<rbrace>
                setObject ptr v
              \<lbrace>\<lambda>rv s. valid_idle' s\<rbrace>" apply (simp add: valid_idle'_def pred_tcb_at'_def o_def) apply (rule hoare_pre) apply (rule hoare_lift_Pf2 [where f="ksIdleThread"]) apply (simp add: pred_tcb_at'_def obj_at'_real_def) apply (rule setObject_ko_wp_at [OF R n m]) apply (wp z) apply (clarsimp simp add: pred_tcb_at'_def obj_at'_real_def ko_wp_at'_def idle_tcb_ps_def) apply (clarsimp simp add: project_inject) apply (drule_tac x=obja in spec, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_idle' s \<and> (ptr = ksIdleThread s \<longrightarrow> (\<exists>val. idle_tcb_ps val) \<longrightarrow> idle_tcb_ps v)\<rbrace> setObject ptr v \<lbrace>\<lambda>rv. valid_idle'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' idle_tcb' (ksIdleThread s) s \<and> idle_thread_ptr = ksIdleThread s \<and> (ptr = ksIdleThread s \<longrightarrow> Ex idle_tcb_ps \<longrightarrow> idle_tcb_ps v)\<rbrace> setObject ptr v \<lbrace>\<lambda>rv s. obj_at' idle_tcb' (ksIdleThread s) s \<and> idle_thread_ptr = ksIdleThread s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> setObject ptr v \<lbrace>\<lambda>rv s. obj_at' idle_tcb' (ksIdleThread s) s \<and> idle_thread_ptr = ksIdleThread s\<rbrace>
 2. \<And>s. obj_at' idle_tcb' (ksIdleThread s) s \<and> idle_thread_ptr = ksIdleThread s \<and> (ptr = ksIdleThread s \<longrightarrow> Ex idle_tcb_ps \<longrightarrow> idle_tcb_ps v) \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>?Q3 x\<rbrace> setObject ptr v \<lbrace>\<lambda>_ a. obj_at' idle_tcb' x a \<and> idle_thread_ptr = x\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> setObject ptr v \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>
 3. \<And>s. obj_at' idle_tcb' (ksIdleThread s) s \<and> idle_thread_ptr = ksIdleThread s \<and> (ptr = ksIdleThread s \<longrightarrow> Ex idle_tcb_ps \<longrightarrow> idle_tcb_ps v) \<Longrightarrow> ?Q3 (ksIdleThread s) s proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>?Q3 x\<rbrace> setObject ptr v \<lbrace>\<lambda>_ a. ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> idle_tcb' obj) x a \<and> idle_thread_ptr = x\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> setObject ptr v \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>
 3. \<And>s. obj_at' idle_tcb' (ksIdleThread s) s \<and> idle_thread_ptr = ksIdleThread s \<and> (ptr = ksIdleThread s \<longrightarrow> Ex idle_tcb_ps \<longrightarrow> idle_tcb_ps v) \<Longrightarrow> ?Q3 (ksIdleThread s) s proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> setObject ptr v \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>
 2. \<And>s. obj_at' idle_tcb' (ksIdleThread s) s \<and> idle_thread_ptr = ksIdleThread s \<and> (ptr = ksIdleThread s \<longrightarrow> Ex idle_tcb_ps \<longrightarrow> idle_tcb_ps v) \<Longrightarrow> obj_at' (\<lambda>x. True) ptr s \<longrightarrow> ko_wp_at' (if ptr = ksIdleThread s then K (\<exists>obj. projectKO_opt (injectKO v) = Some obj \<and> idle_tcb' obj) else (\<lambda>a. \<exists>obj. projectKO_opt a = Some obj \<and> idle_tcb' obj)) (ksIdleThread s) s \<and> idle_thread_ptr = ksIdleThread s proof (prove)
goal (1 subgoal):
 1. \<And>s. obj_at' idle_tcb' (ksIdleThread s) s \<and> idle_thread_ptr = ksIdleThread s \<and> (ptr = ksIdleThread s \<longrightarrow> Ex idle_tcb_ps \<longrightarrow> idle_tcb_ps v) \<Longrightarrow> obj_at' (\<lambda>x. True) ptr s \<longrightarrow> ko_wp_at' (if ptr = ksIdleThread s then K (\<exists>obj. projectKO_opt (injectKO v) = Some obj \<and> idle_tcb' obj) else (\<lambda>a. \<exists>obj. projectKO_opt a = Some obj \<and> idle_tcb' obj)) (ksIdleThread s) s \<and> idle_thread_ptr = ksIdleThread s proof (prove)
goal (1 subgoal):
 1. \<And>s ko obj obja. \<lbrakk>idle_thread_ptr = ksIdleThread s; ksPSpace s idle_thread_ptr = Some ko; is_aligned idle_thread_ptr (objBitsKO ko); ps_clear idle_thread_ptr (objBitsKO ko) s; projectKO_opt ko = Some obj; idle_tcb' obj; ptr = idle_thread_ptr; projectKO_opt ko = Some obja; \<forall>x tcb. projectKO_opt (injectKO x) = Some tcb \<longrightarrow> \<not> idle_tcb' tcb\<rbrakk> \<Longrightarrow> \<exists>obj. projectKO_opt (injectKO v) = Some obj \<and> idle_tcb' obj proof (prove)
goal (1 subgoal):
 1. \<And>s obj obja. \<lbrakk>idle_thread_ptr = ksIdleThread s; ksPSpace s idle_thread_ptr = Some (KOTCB obj); is_aligned idle_thread_ptr (objBitsKO (KOTCB obj)); ps_clear idle_thread_ptr (objBitsKO (KOTCB obj)) s; idle_tcb' obj; ptr = idle_thread_ptr; injectKO obja = KOTCB obj; \<forall>x tcb. KOTCB tcb = injectKO x \<longrightarrow> \<not> idle_tcb' tcb\<rbrakk> \<Longrightarrow> \<exists>obj. KOTCB obj = injectKO v \<and> idle_tcb' obj proof (prove)
goal:
No subgoals!