theory KHeap_R

lemma set_ep_valid_queues[wp]:
  "\<lbrace>Invariants_H.valid_queues\<rbrace> setEndpoint epptr ep \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace>" apply (simp add: Invariants_H.valid_queues_def) apply (wp hoare_vcg_conj_lift) apply (simp add: setEndpoint_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> setEndpoint epptr ep \<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> setEndpoint epptr ep \<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 (3 subgoals):
 1. \<lbrace>?P1\<rbrace> setEndpoint epptr ep \<lbrace>\<lambda>rv. valid_queues_no_bitmap\<rbrace>
 2. \<lbrace>?P'1\<rbrace> setEndpoint epptr ep \<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> ?P1 s \<and> ?P'1 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P1\<rbrace> setObject epptr ep \<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'1\<rbrace> setEndpoint epptr ep \<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> ?P1 s \<and> ?P'1 s proof (prove)
goal (5 subgoals):
 1. \<And>d p t. \<lbrace>?P6 d p t\<rbrace> setObject epptr ep \<lbrace>\<lambda>rv. obj_at' (inQ d p and runnable' \<circ> tcbState) t\<rbrace>
 2. \<And>d p P. \<lbrace>\<lambda>s. P (set (ksReadyQueues s (d, p)))\<rbrace> setObject epptr ep \<lbrace>\<lambda>rv s. P (set (ksReadyQueues s (d, p)))\<rbrace>
 3. \<And>d p. \<lbrace>?P'5 d p\<rbrace> setObject epptr ep \<lbrace>\<lambda>rv s. distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = [])\<rbrace>
 4. \<lbrace>?P'1\<rbrace> setEndpoint epptr ep \<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)). ?P6 x xa xb s) \<and> ?P'5 x xa s) \<and> ?P'1 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 p P. \<lbrace>\<lambda>s. P (set (ksReadyQueues s (d, p)))\<rbrace> setObject epptr ep \<lbrace>\<lambda>rv s. P (set (ksReadyQueues s (d, p)))\<rbrace>
 3. \<And>d p. \<lbrace>?P'5 d p\<rbrace> setObject epptr ep \<lbrace>\<lambda>rv s. distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = [])\<rbrace>
 4. \<lbrace>?P'1\<rbrace> setEndpoint epptr ep \<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'5 x xa s) \<and> ?P'1 s proof (prove)
goal (4 subgoals):
 1. \<And>d p P. \<lbrace>\<lambda>s. P (set (ksReadyQueues s (d, p)))\<rbrace> setObject epptr ep \<lbrace>\<lambda>rv s. P (set (ksReadyQueues s (d, p)))\<rbrace>
 2. \<And>d p. \<lbrace>?P'5 d p\<rbrace> setObject epptr ep \<lbrace>\<lambda>rv s. distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = [])\<rbrace>
 3. \<lbrace>?P'1\<rbrace> setEndpoint epptr ep \<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'5 x xa s) \<and> ?P'1 s proof (prove)
goal:
No subgoals!