theory KHeap_R

lemma set_ntfn_valid_queues[wp]:
  "\<lbrace>Invariants_H.valid_queues\<rbrace> setNotification p ntfn \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace>" apply (simp add: Invariants_H.valid_queues_def) apply (rule hoare_pre) apply (wp hoare_vcg_conj_lift) apply (simp add: setNotification_def valid_queues_no_bitmap_def) apply (wp hoare_Ball_helper hoare_vcg_all_lift) apply (rule obj_at_setObject2) apply (clarsimp simp: updateObject_default_def in_monad) apply (wp updateObject_default_inv set_ep_valid_bitmapQ[unfolded setEndpoint_def]
            | simp add: valid_queues_no_bitmap_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues\<rbrace> setNotification p ntfn \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_queues_no_bitmap s \<and> valid_bitmapQ s \<and> bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s\<rbrace> setNotification p ntfn \<lbrace>\<lambda>rv s. valid_queues_no_bitmap s \<and> valid_bitmapQ s \<and> bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> setNotification p ntfn \<lbrace>\<lambda>rv s. valid_queues_no_bitmap s \<and> valid_bitmapQ s \<and> bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s\<rbrace>
 2. \<And>s. valid_queues_no_bitmap s \<and> valid_bitmapQ s \<and> bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P4\<rbrace> setNotification p ntfn \<lbrace>\<lambda>rv. valid_queues_no_bitmap\<rbrace>
 2. \<lbrace>?P'4\<rbrace> setNotification p ntfn \<lbrace>\<lambda>rv s. valid_bitmapQ s \<and> bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s\<rbrace>
 3. \<And>s. valid_queues_no_bitmap s \<and> valid_bitmapQ s \<and> bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s \<Longrightarrow> ?P4 s \<and> ?P'4 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P4\<rbrace> setObject p ntfn \<lbrace>\<lambda>rv s. \<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p and runnable' \<circ> tcbState) t s) \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = [])\<rbrace>
 2. \<lbrace>?P'4\<rbrace> setNotification p ntfn \<lbrace>\<lambda>rv s. valid_bitmapQ s \<and> bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s\<rbrace>
 3. \<And>s. valid_queues_no_bitmap s \<and> valid_bitmapQ s \<and> bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s \<Longrightarrow> ?P4 s \<and> ?P'4 s proof (prove)
goal (5 subgoals):
 1. \<And>d pa t. \<lbrace>?P10 d pa t\<rbrace> setObject p ntfn \<lbrace>\<lambda>rv. obj_at' (inQ d pa and runnable' \<circ> tcbState) t\<rbrace>
 2. \<And>d pa P. \<lbrace>\<lambda>s. P (set (ksReadyQueues s (d, pa)))\<rbrace> setObject p ntfn \<lbrace>\<lambda>rv s. P (set (ksReadyQueues s (d, pa)))\<rbrace>
 3. \<And>d pa. \<lbrace>?P'9 d pa\<rbrace> setObject p ntfn \<lbrace>\<lambda>rv s. distinct (ksReadyQueues s (d, pa)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s (d, pa) = []) \<and> (maxPriority < pa \<longrightarrow> ksReadyQueues s (d, pa) = [])\<rbrace>
 4. \<lbrace>?P'4\<rbrace> setNotification p ntfn \<lbrace>\<lambda>rv s. valid_bitmapQ s \<and> bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s\<rbrace>
 5. \<And>s. valid_queues_no_bitmap s \<and> valid_bitmapQ s \<and> bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s \<Longrightarrow> (\<forall>x xa. (\<forall>xb\<in>set (ksReadyQueues s (x, xa)). ?P10 x xa xb s) \<and> ?P'9 x xa s) \<and> ?P'4 s proof (prove)
goal (5 subgoals):
 1. \<And>d p t ko s' v oko x y n s. (ko, s') \<in> fst (updateObject v oko x y n s) \<Longrightarrow> koTypeOf ko \<noteq> koType TYPE(Structures_H.tcb)
 2. \<And>d pa P. \<lbrace>\<lambda>s. P (set (ksReadyQueues s (d, pa)))\<rbrace> setObject p ntfn \<lbrace>\<lambda>rv s. P (set (ksReadyQueues s (d, pa)))\<rbrace>
 3. \<And>d pa. \<lbrace>?P'9 d pa\<rbrace> setObject p ntfn \<lbrace>\<lambda>rv s. distinct (ksReadyQueues s (d, pa)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s (d, pa) = []) \<and> (maxPriority < pa \<longrightarrow> ksReadyQueues s (d, pa) = [])\<rbrace>
 4. \<lbrace>?P'4\<rbrace> setNotification p ntfn \<lbrace>\<lambda>rv s. valid_bitmapQ s \<and> bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s\<rbrace>
 5. \<And>s. valid_queues_no_bitmap s \<and> valid_bitmapQ s \<and> bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s \<Longrightarrow> (\<forall>x xa. (\<forall>xb\<in>set (ksReadyQueues s (x, xa)). obj_at' (inQ x xa and runnable' \<circ> tcbState) xb s) \<and> ?P'9 x xa s) \<and> ?P'4 s proof (prove)
goal (4 subgoals):
 1. \<And>d pa P. \<lbrace>\<lambda>s. P (set (ksReadyQueues s (d, pa)))\<rbrace> setObject p ntfn \<lbrace>\<lambda>rv s. P (set (ksReadyQueues s (d, pa)))\<rbrace>
 2. \<And>d pa. \<lbrace>?P'9 d pa\<rbrace> setObject p ntfn \<lbrace>\<lambda>rv s. distinct (ksReadyQueues s (d, pa)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s (d, pa) = []) \<and> (maxPriority < pa \<longrightarrow> ksReadyQueues s (d, pa) = [])\<rbrace>
 3. \<lbrace>?P'4\<rbrace> setNotification p ntfn \<lbrace>\<lambda>rv s. valid_bitmapQ s \<and> bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s\<rbrace>
 4. \<And>s. valid_queues_no_bitmap s \<and> valid_bitmapQ s \<and> bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s \<Longrightarrow> (\<forall>x xa. (\<forall>xb\<in>set (ksReadyQueues s (x, xa)). obj_at' (inQ x xa and runnable' \<circ> tcbState) xb s) \<and> ?P'9 x xa s) \<and> ?P'4 s proof (prove)
goal:
No subgoals!