theory Ipc_DR

lemma no_pending_cap_when_active_corres:
  "dcorres (\<lambda>cap rv'. cap = cdl_cap.NullCap) \<top> (st_tcb_at (\<lambda>t. \<not> generates_pending t) thread and not_idle_thread thread and valid_etcbs)
     (KHeap_D.get_cap (thread, tcb_pending_op_slot))
     (return b)" apply (simp add:gets_the_def  gets_def  assert_opt_def) apply (rule dcorres_absorb_get_l) apply (clarsimp simp:st_tcb_at_def obj_at_def) apply (frule(1) valid_etcbs_tcb_etcb) apply (subst opt_cap_tcb) apply (erule get_tcb_rev) apply (clarsimp simp: get_etcb_def) apply (simp add:not_idle_thread_def) apply (clarsimp simp:tcb_pending_op_slot_def tcb_caller_slot_def tcb_cspace_slot_def tcb_ipcbuffer_slot_def
    tcb_replycap_slot_def tcb_vspace_slot_def assert_opt_def) apply (clarsimp simp:object_slots_def generates_pending_def infer_tcb_pending_op_def return_def
    split:Structures_A.thread_state.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres (\<lambda>cap rv'. cap = cdl_cap.NullCap) (\<lambda>_. True) (st_tcb_at (\<lambda>t. \<not> generates_pending t) thread and not_idle_thread thread and valid_etcbs) (KHeap_D.get_cap (thread, tcb_pending_op_slot)) (return b) proof (prove)
goal (1 subgoal):
 1. dcorres (\<lambda>cap rv'. cap = cdl_cap.NullCap) (\<lambda>_. True) (st_tcb_at (\<lambda>t. \<not> generates_pending t) thread and not_idle_thread thread and valid_etcbs) (do s <- get;
case opt_cap (thread, tcb_pending_op_slot) s of None \<Rightarrow> fail | Some v \<Rightarrow> return v
od) (return b) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>True; (st_tcb_at (\<lambda>t. \<not> generates_pending t) thread and not_idle_thread thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres (\<lambda>cap rv'. cap = cdl_cap.NullCap) ((=) (transform s')) ((=) s') (case opt_cap (thread, tcb_pending_op_slot) (transform s') of None \<Rightarrow> fail | Some v \<Rightarrow> return v) (return b) proof (prove)
goal (1 subgoal):
 1. \<And>s' tcb. \<lbrakk>not_idle_thread thread s'; valid_etcbs s'; kheap s' thread = Some (TCB tcb); \<not> generates_pending (tcb_state tcb)\<rbrakk> \<Longrightarrow> dcorres (\<lambda>cap rv'. cap = cdl_cap.NullCap) ((=) (transform s')) ((=) s') (case opt_cap (thread, tcb_pending_op_slot) (transform s') of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return b) proof (prove)
goal (1 subgoal):
 1. \<And>s' tcb. \<lbrakk>not_idle_thread thread s'; valid_etcbs s'; kheap s' thread = Some (TCB tcb); \<not> generates_pending (tcb_state tcb); \<exists>etcb. ekheap s' thread = Some etcb\<rbrakk> \<Longrightarrow> dcorres (\<lambda>cap rv'. cap = cdl_cap.NullCap) ((=) (transform s')) ((=) s') (case opt_cap (thread, tcb_pending_op_slot) (transform s') of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return b) proof (prove)
goal (4 subgoals):
 1. \<And>s' tcb. \<lbrakk>not_idle_thread thread s'; valid_etcbs s'; kheap s' thread = Some (TCB tcb); \<not> generates_pending (tcb_state tcb); \<exists>etcb. ekheap s' thread = Some etcb\<rbrakk> \<Longrightarrow> get_tcb thread s' = Some (?tcb12 s' tcb)
 2. \<And>s' tcb. \<lbrakk>not_idle_thread thread s'; valid_etcbs s'; kheap s' thread = Some (TCB tcb); \<not> generates_pending (tcb_state tcb); \<exists>etcb. ekheap s' thread = Some etcb\<rbrakk> \<Longrightarrow> \<exists>etcb. get_etcb thread s' = Some etcb
 3. \<And>s' tcb. \<lbrakk>not_idle_thread thread s'; valid_etcbs s'; kheap s' thread = Some (TCB tcb); \<not> generates_pending (tcb_state tcb); \<exists>etcb. ekheap s' thread = Some etcb\<rbrakk> \<Longrightarrow> thread \<noteq> idle_thread s'
 4. \<And>s' tcb. \<lbrakk>not_idle_thread thread s'; valid_etcbs s'; kheap s' thread = Some (TCB tcb); \<not> generates_pending (tcb_state tcb); \<exists>etcb. ekheap s' thread = Some etcb\<rbrakk> \<Longrightarrow> dcorres (\<lambda>cap rv'. cap = cdl_cap.NullCap) ((=) (transform s')) ((=) s') (case if tcb_pending_op_slot \<in> tcb_abstract_slots then map_option (\<lambda>(getF, uu_, uu_). transform_cap (getF (?tcb12 s' tcb))) (tcb_cap_cases (tcb_cnode_index tcb_pending_op_slot)) else if tcb_pending_op_slot = tcb_pending_op_slot then Some (infer_tcb_pending_op thread (tcb_state (?tcb12 s' tcb))) else if tcb_pending_op_slot = tcb_boundntfn_slot then Some (infer_tcb_bound_notification (tcb_bound_notification (?tcb12 s' tcb))) else None of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return b) proof (prove)
goal (3 subgoals):
 1. \<And>s' tcb. \<lbrakk>not_idle_thread thread s'; valid_etcbs s'; kheap s' thread = Some (TCB tcb); \<not> generates_pending (tcb_state tcb); \<exists>etcb. ekheap s' thread = Some etcb\<rbrakk> \<Longrightarrow> \<exists>etcb. get_etcb thread s' = Some etcb
 2. \<And>s' tcb. \<lbrakk>not_idle_thread thread s'; valid_etcbs s'; kheap s' thread = Some (TCB tcb); \<not> generates_pending (tcb_state tcb); \<exists>etcb. ekheap s' thread = Some etcb\<rbrakk> \<Longrightarrow> thread \<noteq> idle_thread s'
 3. \<And>s' tcb. \<lbrakk>not_idle_thread thread s'; valid_etcbs s'; kheap s' thread = Some (TCB tcb); \<not> generates_pending (tcb_state tcb); \<exists>etcb. ekheap s' thread = Some etcb\<rbrakk> \<Longrightarrow> dcorres (\<lambda>cap rv'. cap = cdl_cap.NullCap) ((=) (transform s')) ((=) s') (case if tcb_pending_op_slot \<in> tcb_abstract_slots then map_option (\<lambda>(getF, uu_, uu_). transform_cap (getF tcb)) (tcb_cap_cases (tcb_cnode_index tcb_pending_op_slot)) else if tcb_pending_op_slot = tcb_pending_op_slot then Some (infer_tcb_pending_op thread (tcb_state tcb)) else if tcb_pending_op_slot = tcb_boundntfn_slot then Some (infer_tcb_bound_notification (tcb_bound_notification tcb)) else None of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return b) proof (prove)
goal (2 subgoals):
 1. \<And>s' tcb. \<lbrakk>not_idle_thread thread s'; valid_etcbs s'; kheap s' thread = Some (TCB tcb); \<not> generates_pending (tcb_state tcb); \<exists>etcb. ekheap s' thread = Some etcb\<rbrakk> \<Longrightarrow> thread \<noteq> idle_thread s'
 2. \<And>s' tcb. \<lbrakk>not_idle_thread thread s'; valid_etcbs s'; kheap s' thread = Some (TCB tcb); \<not> generates_pending (tcb_state tcb); \<exists>etcb. ekheap s' thread = Some etcb\<rbrakk> \<Longrightarrow> dcorres (\<lambda>cap rv'. cap = cdl_cap.NullCap) ((=) (transform s')) ((=) s') (case if tcb_pending_op_slot \<in> tcb_abstract_slots then map_option (\<lambda>(getF, uu_, uu_). transform_cap (getF tcb)) (tcb_cap_cases (tcb_cnode_index tcb_pending_op_slot)) else if tcb_pending_op_slot = tcb_pending_op_slot then Some (infer_tcb_pending_op thread (tcb_state tcb)) else if tcb_pending_op_slot = tcb_boundntfn_slot then Some (infer_tcb_bound_notification (tcb_bound_notification tcb)) else None of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return b) proof (prove)
goal (1 subgoal):
 1. \<And>s' tcb. \<lbrakk>not_idle_thread thread s'; valid_etcbs s'; kheap s' thread = Some (TCB tcb); \<not> generates_pending (tcb_state tcb); \<exists>etcb. ekheap s' thread = Some etcb\<rbrakk> \<Longrightarrow> dcorres (\<lambda>cap rv'. cap = cdl_cap.NullCap) ((=) (transform s')) ((=) s') (case if tcb_pending_op_slot \<in> tcb_abstract_slots then map_option (\<lambda>(getF, uu_, uu_). transform_cap (getF tcb)) (tcb_cap_cases (tcb_cnode_index tcb_pending_op_slot)) else if tcb_pending_op_slot = tcb_pending_op_slot then Some (infer_tcb_pending_op thread (tcb_state tcb)) else if tcb_pending_op_slot = tcb_boundntfn_slot then Some (infer_tcb_bound_notification (tcb_bound_notification tcb)) else None of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return b) proof (prove)
goal (1 subgoal):
 1. \<And>s' tcb etcb. \<lbrakk>not_idle_thread thread s'; valid_etcbs s'; kheap s' thread = Some (TCB tcb); \<not> generates_pending (tcb_state tcb); ekheap s' thread = Some etcb\<rbrakk> \<Longrightarrow> infer_tcb_pending_op thread (tcb_state tcb) = cdl_cap.NullCap proof (prove)
goal:
No subgoals!