theory KHeap_R

lemma set_ep_valid_queues'[wp]:
  "\<lbrace>valid_queues'\<rbrace> setEndpoint epptr ep \<lbrace>\<lambda>rv. valid_queues'\<rbrace>" apply (unfold setEndpoint_def) apply (simp only: valid_queues'_def imp_conv_disj
                    obj_at'_real_def) apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift) apply (rule setObject_ko_wp_at) apply simp apply (simp add: objBits_simps') apply simp apply (wp updateObject_default_inv | simp)+ apply (clarsimp simp: projectKOs ko_wp_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues'\<rbrace> setEndpoint epptr ep \<lbrace>\<lambda>rv. valid_queues'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues'\<rbrace> setObject epptr ep \<lbrace>\<lambda>rv. valid_queues'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>d p t. \<not> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> inQ d p obj) t s \<or> t \<in> set (ksReadyQueues s (d, p))\<rbrace> setObject epptr ep \<lbrace>\<lambda>rv s. \<forall>d p t. \<not> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> inQ d p obj) t s \<or> t \<in> set (ksReadyQueues s (d, p))\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>d p t. \<lbrace>?P4 d p t\<rbrace> setObject epptr ep \<lbrace>\<lambda>rv s. \<not> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> inQ d p obj) t s\<rbrace>
 2. \<And>d p t. \<lbrace>?P'4 d p t\<rbrace> setObject epptr ep \<lbrace>\<lambda>rv s. t \<in> set (ksReadyQueues s (d, p))\<rbrace>
 3. \<And>s. \<forall>d p t. \<not> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> inQ d p obj) t s \<or> t \<in> set (ksReadyQueues s (d, p)) \<Longrightarrow> \<forall>x xa xb. ?P4 x xa xb s \<or> ?P'4 x xa xb s proof (prove)
goal (5 subgoals):
 1. \<And>d p t ko s x y n. updateObject ep ko epptr y n s = updateObject_default ep ko epptr y n s
 2. \<And>d p t v'. objBits v' = ?n5 d p t
 3. \<And>d p t. 1 < 2 ^ ?n5 d p t
 4. \<And>d p t. \<lbrace>?P'4 d p t\<rbrace> setObject epptr ep \<lbrace>\<lambda>rv s. t \<in> set (ksReadyQueues s (d, p))\<rbrace>
 5. \<And>s. \<forall>d p t. \<not> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> inQ d p obj) t s \<or> t \<in> set (ksReadyQueues s (d, p)) \<Longrightarrow> \<forall>x xa xb. (ep_at' epptr s \<longrightarrow> \<not> ko_wp_at' (if epptr = xb then K (\<exists>obj. projectKO_opt (injectKO ep) = Some obj \<and> inQ x xa obj) else (\<lambda>a. \<exists>obj. projectKO_opt a = Some obj \<and> inQ x xa obj)) xb s) \<or> ?P'4 x xa xb s proof (prove)
goal (4 subgoals):
 1. \<And>d p t v'. objBits v' = ?n5 d p t
 2. \<And>d p t. 1 < 2 ^ ?n5 d p t
 3. \<And>d p t. \<lbrace>?P'4 d p t\<rbrace> setObject epptr ep \<lbrace>\<lambda>rv s. t \<in> set (ksReadyQueues s (d, p))\<rbrace>
 4. \<And>s. \<forall>d p t. \<not> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> inQ d p obj) t s \<or> t \<in> set (ksReadyQueues s (d, p)) \<Longrightarrow> \<forall>x xa xb. (ep_at' epptr s \<longrightarrow> \<not> ko_wp_at' (if epptr = xb then K (\<exists>obj. projectKO_opt (injectKO ep) = Some obj \<and> inQ x xa obj) else (\<lambda>a. \<exists>obj. projectKO_opt a = Some obj \<and> inQ x xa obj)) xb s) \<or> ?P'4 x xa xb s proof (prove)
goal (3 subgoals):
 1. \<And>d p t. 1 < 2 ^ 4
 2. \<And>d p t. \<lbrace>?P'4 d p t\<rbrace> setObject epptr ep \<lbrace>\<lambda>rv s. t \<in> set (ksReadyQueues s (d, p))\<rbrace>
 3. \<And>s. \<forall>d p t. \<not> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> inQ d p obj) t s \<or> t \<in> set (ksReadyQueues s (d, p)) \<Longrightarrow> \<forall>x xa xb. (ep_at' epptr s \<longrightarrow> \<not> ko_wp_at' (if epptr = xb then K (\<exists>obj. projectKO_opt (injectKO ep) = Some obj \<and> inQ x xa obj) else (\<lambda>a. \<exists>obj. projectKO_opt a = Some obj \<and> inQ x xa obj)) xb s) \<or> ?P'4 x xa xb s proof (prove)
goal (2 subgoals):
 1. \<And>d p t. \<lbrace>?P'4 d p t\<rbrace> setObject epptr ep \<lbrace>\<lambda>rv s. t \<in> set (ksReadyQueues s (d, p))\<rbrace>
 2. \<And>s. \<forall>d p t. \<not> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> inQ d p obj) t s \<or> t \<in> set (ksReadyQueues s (d, p)) \<Longrightarrow> \<forall>x xa xb. (ep_at' epptr s \<longrightarrow> \<not> ko_wp_at' (if epptr = xb then K (\<exists>obj. projectKO_opt (injectKO ep) = Some obj \<and> inQ x xa obj) else (\<lambda>a. \<exists>obj. projectKO_opt a = Some obj \<and> inQ x xa obj)) xb s) \<or> ?P'4 x xa xb s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>d p t. ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> inQ d p obj) t s \<longrightarrow> t \<in> set (ksReadyQueues s (d, p)) \<Longrightarrow> ep_at' epptr s \<longrightarrow> (\<forall>x xa. ko_wp_at' (\<lambda>y. \<exists>obj. projectKO_opt (KOEndpoint ep) = Some obj \<and> inQ x xa obj) epptr s \<longrightarrow> epptr \<in> set (ksReadyQueues s (x, xa))) proof (prove)
goal:
No subgoals!