kings-crown/FVELER_Isabelle huggingface dataset:
theory KHeap_DR

lemma tcb_type_at_set_ep:
  "\<lbrace>(=) s'a\<rbrace> set_endpoint word1 Structures_A.endpoint.IdleEP \<lbrace>\<lambda>r s. \<forall>x. tcb_at x s \<longrightarrow> tcb_at x s'a\<rbrace>" apply (clarsimp simp: set_simple_ko_def) apply (wp tcb_type_set_obj_ep) apply (clarsimp simp: get_object_def) apply wp apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(=) s'a\<rbrace> set_endpoint word1 IdleEP \<lbrace>\<lambda>r s. \<forall>x. tcb_at x s \<longrightarrow> tcb_at x s'a\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(=) s'a\<rbrace> do obj <- KHeap_A.get_object word1;
y <- assert (a_type obj = AEndpoint \<or> a_type obj = ANTFN);
y <- assert (\<exists>y. kernel_object.Endpoint y = obj);
KHeap_A.set_object word1 (kernel_object.Endpoint IdleEP)
od \<lbrace>\<lambda>r s. \<forall>x. tcb_at x s \<longrightarrow> tcb_at x s'a\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> KHeap_A.get_object word1 \<lbrace>\<lambda>obj s. a_type obj = AEndpoint \<or> a_type obj = ANTFN \<longrightarrow> (\<exists>y. kernel_object.Endpoint y = obj) \<longrightarrow> s'a = s\<rbrace>
 2. \<And>s. s'a = s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do kh <- gets kheap;
y <- assert (\<exists>y. kh word1 = Some y);
return (the (kh word1))
od \<lbrace>\<lambda>obj s. (a_type obj = AEndpoint \<longrightarrow> (\<exists>y. kernel_object.Endpoint y = obj) \<longrightarrow> s'a = s) \<and> (a_type obj = ANTFN \<longrightarrow> (\<exists>y. kernel_object.Endpoint y = obj) \<longrightarrow> s'a = s)\<rbrace>
 2. \<And>s. s'a = s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. s'a = s \<Longrightarrow> (\<exists>y. kheap s word1 = Some y) \<longrightarrow> (a_type (the (kheap s word1)) = AEndpoint \<longrightarrow> (\<exists>y. kernel_object.Endpoint y = the (kheap s word1)) \<longrightarrow> s'a = s) \<and> (a_type (the (kheap s word1)) = ANTFN \<longrightarrow> (\<exists>y. kernel_object.Endpoint y = the (kheap s word1)) \<longrightarrow> s'a = s) proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma is_thread_blocked_on_sth:
  "{x. \<exists>tcb. cdl_objects s x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb ep}
    = (get_waiting_sync_recv_threads ep s) \<union> (get_waiting_sync_send_threads ep s) \<union> (get_waiting_ntfn_recv_threads ep s)" apply (rule set_eqI) apply (rule iffI) apply (clarsimp simp: is_thread_blocked_on_endpoint_def split: option.splits) apply (case_tac y; simp add: get_waiting_sync_recv_threads_def get_waiting_sync_send_threads_def
                                get_waiting_ntfn_recv_threads_def) apply (fastforce simp: is_thread_blocked_on_endpoint_def get_waiting_sync_recv_threads_def
                         get_waiting_sync_send_threads_def get_waiting_ntfn_recv_threads_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {x. \<exists>tcb. cdl_objects s x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb ep} = get_waiting_sync_recv_threads ep s \<union> get_waiting_sync_send_threads ep s \<union> get_waiting_ntfn_recv_threads ep s proof (prove)
goal (1 subgoal):
 1. \<And>x. (x \<in> {x. \<exists>tcb. cdl_objects s x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb ep}) = (x \<in> get_waiting_sync_recv_threads ep s \<union> get_waiting_sync_send_threads ep s \<union> get_waiting_ntfn_recv_threads ep s) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> {x. \<exists>tcb. cdl_objects s x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb ep} \<Longrightarrow> x \<in> get_waiting_sync_recv_threads ep s \<union> get_waiting_sync_send_threads ep s \<union> get_waiting_ntfn_recv_threads ep s
 2. \<And>x. x \<in> get_waiting_sync_recv_threads ep s \<union> get_waiting_sync_send_threads ep s \<union> get_waiting_ntfn_recv_threads ep s \<Longrightarrow> x \<in> {x. \<exists>tcb. cdl_objects s x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb ep} proof (prove)
goal (2 subgoals):
 1. \<And>x tcb y. \<lbrakk>cdl_tcb_caps tcb tcb_pending_op_slot = Some y; x \<notin> get_waiting_sync_recv_threads ep s; x \<notin> get_waiting_ntfn_recv_threads ep s; cdl_objects s x = Some (Tcb tcb); case y of PendingSyncSendCap p x xa xb xc xd \<Rightarrow> p = ep | PendingSyncRecvCap p is_reply x \<Rightarrow> p = ep \<and> \<not> is_reply | PendingNtfnRecvCap p \<Rightarrow> p = ep | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> x \<in> get_waiting_sync_send_threads ep s
 2. \<And>x. x \<in> get_waiting_sync_recv_threads ep s \<union> get_waiting_sync_send_threads ep s \<union> get_waiting_ntfn_recv_threads ep s \<Longrightarrow> x \<in> {x. \<exists>tcb. cdl_objects s x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb ep} proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> get_waiting_sync_recv_threads ep s \<union> get_waiting_sync_send_threads ep s \<union> get_waiting_ntfn_recv_threads ep s \<Longrightarrow> x \<in> {x. \<exists>tcb. cdl_objects s x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb ep} proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma set_ep_exec_wp: (* generalise? *)
  "\<lbrace>(=) s\<rbrace> set_endpoint epptr ep \<lbrace>\<lambda>r s'. s' = update_kheap ((kheap s)(epptr \<mapsto> Endpoint ep)) s\<rbrace> " by (wpsimp simp: set_simple_ko_def set_object_def get_object_def a_type_def fun_upd_def
            split: option.splits Structures_A.kernel_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(=) s\<rbrace> set_endpoint epptr ep \<lbrace>\<lambda>r s'. s' = update_kheap ((kheap s)(epptr \<mapsto> kernel_object.Endpoint ep)) s\<rbrace>
theory KHeap_DR

lemma set_ntfn_exec_wp:
  "\<lbrace>(=) s\<rbrace> set_notification epptr ep \<lbrace>\<lambda>r s'. s' = update_kheap ((kheap s)(epptr \<mapsto> Notification ep)) s\<rbrace> " by (wpsimp simp: set_simple_ko_def set_object_def get_object_def a_type_def fun_upd_def
            split: option.splits Structures_A.kernel_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(=) s\<rbrace> set_notification epptr ep \<lbrace>\<lambda>r s'. s' = update_kheap ((kheap s)(epptr \<mapsto> kernel_object.Notification ep)) s\<rbrace>
theory KHeap_DR

lemma pending_thread_in_recv_not_idle:
  "\<lbrakk>valid_state s'; valid_idle s';
    ko_at (kernel_object.Endpoint (Structures_A.endpoint.RecvEP list)) epptr s'; a\<in> set list\<rbrakk> \<Longrightarrow> not_idle_thread a s'" apply (frule get_endpoint_pick) apply (fastforce simp:obj_at_def is_ep_def) apply (clarsimp simp:valid_ep_abstract_def) apply (clarsimp simp:ep_waiting_set_recv_def) apply (clarsimp simp:not_idle_thread_def pred_tcb_at_def valid_idle_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; a \<in> set list\<rbrakk> \<Longrightarrow> not_idle_thread a s' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; a \<in> set list\<rbrakk> \<Longrightarrow> kheap s' ?epptr = Some (kernel_object.Endpoint ?endpoint)
 2. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; a \<in> set list; valid_ep_abstract ?endpoint ?epptr s'\<rbrakk> \<Longrightarrow> not_idle_thread a s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; a \<in> set list; valid_ep_abstract (RecvEP list) epptr s'\<rbrakk> \<Longrightarrow> not_idle_thread a s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; a \<in> ep_waiting_set_recv epptr s'; kheap s' epptr = Some (kernel_object.Endpoint (RecvEP list)); list \<noteq> []; set list = ep_waiting_set_recv epptr s'; none_is_sending_ep epptr s'; \<forall>p'. Some (kernel_object.Endpoint (RecvEP list)) = kheap s' p' \<longrightarrow> epptr = p'\<rbrakk> \<Longrightarrow> not_idle_thread a s' proof (prove)
goal (1 subgoal):
 1. \<And>t payload. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; kheap s' epptr = Some (kernel_object.Endpoint (RecvEP list)); list \<noteq> []; set list = {tcb. \<exists>t. kheap s' tcb = Some (TCB t) \<and> (\<exists>payload. tcb_state t = BlockedOnReceive epptr payload)}; none_is_sending_ep epptr s'; \<forall>p'. Some (kernel_object.Endpoint (RecvEP list)) = kheap s' p' \<longrightarrow> epptr = p'; kheap s' a = Some (TCB t); tcb_state t = BlockedOnReceive epptr payload\<rbrakk> \<Longrightarrow> not_idle_thread a s' proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma pending_thread_in_send_not_idle:
  "\<lbrakk> valid_state s';valid_idle s'; a\<in> set list;
          ko_at (kernel_object.Endpoint (Structures_A.endpoint.SendEP list)) epptr s'\<rbrakk>
  \<Longrightarrow> not_idle_thread a s'" apply (frule get_endpoint_pick) apply (fastforce simp:obj_at_def is_ep_def) apply (clarsimp simp:valid_ep_abstract_def) apply (clarsimp simp:ep_waiting_set_send_def) apply (clarsimp simp:not_idle_thread_def pred_tcb_at_def valid_idle_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_state s'; valid_idle s'; a \<in> set list; ko_at (kernel_object.Endpoint (SendEP list)) epptr s'\<rbrakk> \<Longrightarrow> not_idle_thread a s' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_state s'; valid_idle s'; a \<in> set list; ko_at (kernel_object.Endpoint (SendEP list)) epptr s'\<rbrakk> \<Longrightarrow> kheap s' ?epptr = Some (kernel_object.Endpoint ?endpoint)
 2. \<lbrakk>valid_state s'; valid_idle s'; a \<in> set list; ko_at (kernel_object.Endpoint (SendEP list)) epptr s'; valid_ep_abstract ?endpoint ?epptr s'\<rbrakk> \<Longrightarrow> not_idle_thread a s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_state s'; valid_idle s'; a \<in> set list; ko_at (kernel_object.Endpoint (SendEP list)) epptr s'; valid_ep_abstract (SendEP list) epptr s'\<rbrakk> \<Longrightarrow> not_idle_thread a s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_state s'; valid_idle s'; a \<in> ep_waiting_set_send epptr s'; ko_at (kernel_object.Endpoint (SendEP list)) epptr s'; kheap s' epptr = Some (kernel_object.Endpoint (SendEP list)); list \<noteq> []; set list = ep_waiting_set_send epptr s'; none_is_receiving_ep epptr s'; \<forall>p'. Some (kernel_object.Endpoint (SendEP list)) = kheap s' p' \<longrightarrow> epptr = p'\<rbrakk> \<Longrightarrow> not_idle_thread a s' proof (prove)
goal (1 subgoal):
 1. \<And>t payload. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (SendEP list)) epptr s'; kheap s' epptr = Some (kernel_object.Endpoint (SendEP list)); list \<noteq> []; set list = {tcb. \<exists>t. kheap s' tcb = Some (TCB t) \<and> (\<exists>payload. tcb_state t = BlockedOnSend epptr payload)}; none_is_receiving_ep epptr s'; \<forall>p'. Some (kernel_object.Endpoint (SendEP list)) = kheap s' p' \<longrightarrow> epptr = p'; kheap s' a = Some (TCB t); tcb_state t = BlockedOnSend epptr payload\<rbrakk> \<Longrightarrow> not_idle_thread a s' proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma pending_thread_in_wait_not_idle:
  "\<lbrakk> valid_state s'; valid_idle s'; a \<in> set list;
     ko_at (kernel_object.Notification ntfn) epptr s';
     ntfn_obj ntfn = (Structures_A.ntfn.WaitingNtfn list)\<rbrakk>
  \<Longrightarrow> not_idle_thread a s'" apply (frule get_notification_pick[rotated]) apply (fastforce simp:obj_at_def is_ep_def) apply (clarsimp simp:valid_ntfn_abstract_def) apply (clarsimp simp:ntfn_waiting_set_def) apply (clarsimp simp:not_idle_thread_def pred_tcb_at_def valid_idle_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_state s'; valid_idle s'; a \<in> set list; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> not_idle_thread a s' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_state s'; valid_idle s'; a \<in> set list; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> kheap s' ?epptr = Some (kernel_object.Notification ?notification)
 2. \<lbrakk>valid_state s'; valid_idle s'; a \<in> set list; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; valid_ntfn_abstract ?notification ?epptr s'\<rbrakk> \<Longrightarrow> not_idle_thread a s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_state s'; valid_idle s'; a \<in> set list; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; valid_ntfn_abstract ntfn epptr s'\<rbrakk> \<Longrightarrow> not_idle_thread a s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_state s'; valid_idle s'; a \<in> ntfn_waiting_set epptr s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; kheap s' epptr = Some (kernel_object.Notification ntfn); set_option (ntfn_bound_tcb ntfn) = ntfn_bound_set epptr s'; list \<noteq> []; set list = ntfn_waiting_set epptr s'; \<forall>p'. Some (kernel_object.Notification ntfn) = kheap s' p' \<longrightarrow> epptr = p'\<rbrakk> \<Longrightarrow> not_idle_thread a s' proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; kheap s' epptr = Some (kernel_object.Notification ntfn); set_option (ntfn_bound_tcb ntfn) = ntfn_bound_set epptr s'; list \<noteq> []; set list = {tcb. \<exists>t. kheap s' tcb = Some (TCB t) \<and> tcb_state t = BlockedOnNotification epptr}; \<forall>p'. Some (kernel_object.Notification ntfn) = kheap s' p' \<longrightarrow> epptr = p'; kheap s' a = Some (TCB t); tcb_state t = BlockedOnNotification epptr\<rbrakk> \<Longrightarrow> not_idle_thread a s' proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma cnode_not_idle:
  "\<lbrakk>valid_idle s'; kheap s' ptr = Some (CNode sz cnode)\<rbrakk> \<Longrightarrow> not_idle_thread ptr s'" by (clarsimp simp:valid_idle_def not_idle_thread_def pred_tcb_at_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s'; kheap s' ptr = Some (kernel_object.CNode sz cnode)\<rbrakk> \<Longrightarrow> not_idle_thread ptr s'
theory KHeap_DR

lemma irq_node_image_not_idle:
  "\<lbrakk>valid_idle s'; valid_irq_node s'\<rbrakk>
  \<Longrightarrow> not_idle_thread (interrupt_irq_node s' y) s' " apply (clarsimp simp:valid_irq_node_def) apply (drule_tac x = y in spec) apply (clarsimp simp:obj_at_def is_cap_table_def) apply (clarsimp split:Structures_A.kernel_object.splits) apply (erule cnode_not_idle) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s'; valid_irq_node s'\<rbrakk> \<Longrightarrow> not_idle_thread (interrupt_irq_node s' y) s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s'; inj (interrupt_irq_node s'); \<forall>irq. cap_table_at 0 (interrupt_irq_node s' irq) s'\<rbrakk> \<Longrightarrow> not_idle_thread (interrupt_irq_node s' y) s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s'; inj (interrupt_irq_node s'); cap_table_at 0 (interrupt_irq_node s' y) s'\<rbrakk> \<Longrightarrow> not_idle_thread (interrupt_irq_node s' y) s' proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>valid_idle s'; inj (interrupt_irq_node s'); kheap s' (interrupt_irq_node s' y) = Some ko; case ko of kernel_object.CNode sz cs \<Rightarrow> 0 = sz \<and> well_formed_cnode_n 0 cs | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> not_idle_thread (interrupt_irq_node s' y) s' proof (prove)
goal (1 subgoal):
 1. \<And>x12. \<lbrakk>valid_idle s'; inj (interrupt_irq_node s'); kheap s' (interrupt_irq_node s' y) = Some (kernel_object.CNode 0 x12); well_formed_cnode_n 0 x12\<rbrakk> \<Longrightarrow> not_idle_thread (interrupt_irq_node s' y) s' proof (prove)
goal (1 subgoal):
 1. \<And>x12. \<lbrakk>inj (interrupt_irq_node s'); kheap s' (interrupt_irq_node s' y) = Some (kernel_object.CNode 0 x12); well_formed_cnode_n 0 x12\<rbrakk> \<Longrightarrow> kheap s' (interrupt_irq_node s' y) = Some (kernel_object.CNode (?sz32 x12) (?cnode32 x12)) proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma generates_pending_not_idle:
  "\<lbrakk>valid_idle s';st_tcb_at generates_pending y s'\<rbrakk> \<Longrightarrow> not_idle_thread y s'" by (clarsimp simp :valid_idle_def pred_tcb_at_def obj_at_def generates_pending_def not_idle_thread_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s'; st_tcb_at generates_pending y s'\<rbrakk> \<Longrightarrow> not_idle_thread y s'
theory KHeap_DR

lemma valid_idle_set_thread_state_wp:
  "\<lbrace>valid_idle and not_idle_thread a\<rbrace>set_thread_state a Structures_A.thread_state.Restart \<lbrace>\<lambda>x. valid_idle\<rbrace>" apply wp apply (simp add: not_idle_thread_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle and not_idle_thread a\<rbrace> set_thread_state a Restart \<lbrace>\<lambda>x. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_idle and not_idle_thread a) s \<Longrightarrow> (valid_idle and (\<lambda>s. a = idle_thread s \<longrightarrow> idle Restart)) s proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma tcb_at_set_thread_state_wp:
  "\<lbrace>\<lambda>s. (\<forall>x\<in>set list. tcb_at x s \<and> not_idle_thread x s)\<rbrace>
  set_thread_state a Structures_A.thread_state.Restart
  \<lbrace>\<lambda>x s. (\<forall>x\<in>set list. tcb_at x s \<and> not_idle_thread x s)\<rbrace>" apply (rule hoare_Ball_helper) apply (wpsimp simp:not_idle_thread_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x\<in>set list. tcb_at x s \<and> not_idle_thread x s\<rbrace> set_thread_state a Restart \<lbrace>\<lambda>x s. \<forall>x\<in>set list. tcb_at x s \<and> not_idle_thread x s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>\<lambda>s. tcb_at x s \<and> not_idle_thread x s\<rbrace> set_thread_state a Restart \<lbrace>\<lambda>rv s. tcb_at x s \<and> not_idle_thread x s\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (set list)\<rbrace> set_thread_state a Restart \<lbrace>\<lambda>x s. P (set list)\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma invalid_cte_wp_at_pending_slot:
  "\<lbrakk>tcb_at y s;transform_cslot_ptr (ad, bd) = (y, tcb_pending_op_slot);
    cte_wp_at ((\<noteq>) cap.NullCap) (ad, bd) s\<rbrakk> \<Longrightarrow> False" apply (clarsimp simp:transform_cslot_ptr_def
      cte_wp_at_cases tcb_at_def dest!:get_tcb_SomeD) apply (clarsimp simp:tcb_cap_cases_def tcb_cnode_index_def tcb_pending_op_slot_def
        split:if_splits) apply (clarsimp simp:bl_to_bin_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_at y s; transform_cslot_ptr (ad, bd) = (y, tcb_pending_op_slot); cte_wp_at ((\<noteq>) cap.NullCap) (ad, bd) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>tcb get set restr. \<lbrakk>kheap s y = Some (TCB tcb); ad = y; nat (bl_to_bin bd) = tcb_pending_op_slot; cap.NullCap \<noteq> get tcb; tcb_cap_cases bd = Some (get, set, restr)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrakk>kheap s y = Some (TCB tcb); ad = y; nat (bl_to_bin [True, False, False]) = 5; cap.NullCap \<noteq> tcb_ipcframe tcb; bd = [True, False, False]\<rbrakk> \<Longrightarrow> False
 2. \<And>tcb. \<lbrakk>kheap s y = Some (TCB tcb); ad = y; nat (bl_to_bin [True, True]) = 5; cap.NullCap \<noteq> tcb_caller tcb; bd = [False, True, True]\<rbrakk> \<Longrightarrow> False
 3. \<And>tcb. \<lbrakk>kheap s y = Some (TCB tcb); ad = y; nat (bl_to_bin [True, False]) = 5; cap.NullCap \<noteq> tcb_reply tcb; bd = [False, True, False]\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma corres_dummy_set_thread_inactive:
  "dcorres dc \<top> (st_tcb_at (Not \<circ> generates_pending) thread) (return ())
  (set_thread_state thread Structures_A.thread_state.Inactive)" by (rule corres_dummy_set_thread_state) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (st_tcb_at (Not \<circ> generates_pending) thread) (return ()) (set_thread_state thread Inactive)
theory KHeap_DR

lemma tcb_sched_action_transform: "\<lbrace>\<lambda>ps. transform ps = cs\<rbrace> tcb_sched_action f t \<lbrace>\<lambda>r s. transform s = cs\<rbrace>" by (clarsimp simp: tcb_sched_action_def etcb_at_def| wp )+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> tcb_sched_action f t \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
theory KHeap_DR

lemma set_bound_notification_corres:
  "dcorres dc \<top> (not_idle_thread y and valid_etcbs and K (cap = infer_tcb_bound_notification ntfn_opt))
    (KHeap_D.set_cap (y, tcb_boundntfn_slot) cap)
    (KHeap_A.set_bound_notification y ntfn_opt)" apply (simp add:set_bound_notification_def) apply (rule dcorres_absorb_gets_the) apply (rule corres_guard_imp) apply (rule set_boundntfn_cap_corres) apply simp apply (clarsimp dest!: get_tcb_SomeD simp: obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (not_idle_thread y and valid_etcbs and K (cap = infer_tcb_bound_notification ntfn_opt)) (KHeap_D.set_cap (y, tcb_boundntfn_slot) cap) (set_bound_notification y ntfn_opt) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (not_idle_thread y and valid_etcbs and (\<lambda>y. cap = infer_tcb_bound_notification ntfn_opt)) (KHeap_D.set_cap (y, tcb_boundntfn_slot) cap) (do tcb <- gets_the (get_tcb y);
KHeap_A.set_object y (TCB (update_tcb_boundntfn ntfn_opt tcb))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' obj'. \<lbrakk>(not_idle_thread y and valid_etcbs and (\<lambda>y. cap = infer_tcb_bound_notification ntfn_opt)) s'; get_tcb y s' = Some obj'; True\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (y, tcb_boundntfn_slot) cap) (KHeap_A.set_object y (TCB (update_tcb_boundntfn ntfn_opt obj'))) proof (prove)
goal (3 subgoals):
 1. \<And>s' obj'. \<lbrakk>(not_idle_thread y and valid_etcbs and (\<lambda>y. cap = infer_tcb_bound_notification ntfn_opt)) s'; get_tcb y s' = Some obj'; True\<rbrakk> \<Longrightarrow> dcorres dc (?Q2 s' obj') (?Q'2 s' obj') (KHeap_D.set_cap (y, tcb_boundntfn_slot) cap) (KHeap_A.set_object y (TCB (update_tcb_boundntfn ntfn_opt obj')))
 2. \<And>s' obj' s. \<lbrakk>(not_idle_thread y and valid_etcbs and (\<lambda>y. cap = infer_tcb_bound_notification ntfn_opt)) s'; get_tcb y s' = Some obj'; True; transform s' = s\<rbrakk> \<Longrightarrow> ?Q2 s' obj' s
 3. \<And>s' obj' s. \<lbrakk>(not_idle_thread y and valid_etcbs and (\<lambda>y. cap = infer_tcb_bound_notification ntfn_opt)) s'; get_tcb y s' = Some obj'; True; s' = s\<rbrakk> \<Longrightarrow> ?Q'2 s' obj' s proof (prove)
goal (2 subgoals):
 1. \<And>s' obj' s. \<lbrakk>(not_idle_thread y and valid_etcbs and (\<lambda>y. cap = infer_tcb_bound_notification ntfn_opt)) s'; get_tcb y s' = Some obj'; True; transform s' = s\<rbrakk> \<Longrightarrow> True
 2. \<And>s' obj' s. \<lbrakk>(not_idle_thread y and valid_etcbs and (\<lambda>y. cap = infer_tcb_bound_notification ntfn_opt)) s'; get_tcb y s' = Some obj'; True; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread y and ko_at (TCB obj') y and K (cap = infer_tcb_bound_notification ntfn_opt) and valid_etcbs) s proof (prove)
goal (1 subgoal):
 1. \<And>s' obj' s. \<lbrakk>(not_idle_thread y and valid_etcbs and (\<lambda>y. cap = infer_tcb_bound_notification ntfn_opt)) s'; get_tcb y s' = Some obj'; True; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread y and ko_at (TCB obj') y and K (cap = infer_tcb_bound_notification ntfn_opt) and valid_etcbs) s proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma option_set_option_select:
  "option_select (set_option x) = return x" by (auto simp: option_select_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. option_select (set_option x) = return x