theory KHeap_DR

lemma get_cap_corres:
  "ptr' = transform_cslot_ptr ptr \<Longrightarrow>
   dcorres (\<lambda>rv rv'. rv = transform_cap rv') \<top>
   (valid_idle and not_idle_thread (fst ptr) and valid_etcbs)
     (KHeap_D.get_cap ptr')
     (CSpaceAcc_A.get_cap ptr)" apply (case_tac ptr) apply (clarsimp simp:CSpaceAcc_A.get_cap_def[simplified tcb_cnode_map_def]
                       gets_def get_object_def gets_the_def bind_assoc) apply (rule dcorres_get) apply (clarsimp simp:assert_def corres_free_fail assert_opt_def) apply (case_tac y) apply (simp_all add:assert_def corres_free_fail) apply (rename_tac nat "fun") apply (case_tac "fun b") apply (simp add:corres_free_fail) apply clarsimp apply (drule (2) cap_slot_cnode_property_lift, simp, fastforce) apply simp apply (clarsimp simp:transform_tcb_slot_simp[simplified]) apply (drule get_tcb_rev) apply (drule(1) valid_etcbs_get_tcb_get_etcb) apply (clarsimp simp:lift_simp not_idle_thread_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr' = transform_cslot_ptr ptr \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') (\<lambda>_. True) (valid_idle and not_idle_thread (fst ptr) and valid_etcbs) (KHeap_D.get_cap ptr') (CSpaceAcc_A.get_cap ptr) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>ptr' = transform_cslot_ptr ptr; ptr = (a, b)\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') (\<lambda>_. True) (valid_idle and not_idle_thread (fst ptr) and valid_etcbs) (KHeap_D.get_cap ptr') (CSpaceAcc_A.get_cap ptr) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>ptr' = transform_cslot_ptr (a, b); ptr = (a, b)\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') (\<lambda>_. True) (valid_idle and not_idle_thread a and valid_etcbs) (do s <- get;
assert_opt (opt_cap (transform_cslot_ptr (a, b)) s)
od) (do x <- get;
y <- assert (\<exists>y. kheap x a = Some y);
caps <- case the (kheap x a) of kernel_object.CNode sz cnode \<Rightarrow> do assert (well_formed_cnode_n sz cnode);
return cnode
od | TCB tcb \<Rightarrow> return [tcb_cnode_index 0 \<mapsto> tcb_ctable tcb, tcb_cnode_index 1 \<mapsto> tcb_vtable tcb, tcb_cnode_index 2 \<mapsto> tcb_reply tcb, tcb_cnode_index 3 \<mapsto> tcb_caller tcb, tcb_cnode_index 4 \<mapsto> tcb_ipcframe tcb] | _ \<Rightarrow> fail;
assert_opt (caps b)
od) proof (prove)
goal (1 subgoal):
 1. \<And>a b s x. \<lbrakk>ptr' = transform_cslot_ptr (a, b); ptr = (a, b); s = transform x; True; (valid_idle and not_idle_thread a and valid_etcbs) x\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) s) ((=) x) (assert_opt (opt_cap (transform_cslot_ptr (a, b)) s)) (do y <- assert (\<exists>y. kheap x a = Some y);
caps <- case the (kheap x a) of kernel_object.CNode sz cnode \<Rightarrow> do assert (well_formed_cnode_n sz cnode);
return cnode
od | TCB tcb \<Rightarrow> return [tcb_cnode_index 0 \<mapsto> tcb_ctable tcb, tcb_cnode_index 1 \<mapsto> tcb_vtable tcb, tcb_cnode_index 2 \<mapsto> tcb_reply tcb, tcb_cnode_index 3 \<mapsto> tcb_caller tcb, tcb_cnode_index 4 \<mapsto> tcb_ipcframe tcb] | _ \<Rightarrow> fail;
assert_opt (caps b)
od) proof (prove)
goal (1 subgoal):
 1. \<And>a b x y. \<lbrakk>ptr' = transform_cslot_ptr (a, b); ptr = (a, b); valid_idle x; not_idle_thread a x; valid_etcbs x; kheap x a = Some y\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, b)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (do caps <- case y of kernel_object.CNode sz cnode \<Rightarrow> do assert (well_formed_cnode_n sz cnode);
return cnode
od | TCB tcb \<Rightarrow> return [tcb_cnode_index 0 \<mapsto> tcb_ctable tcb, tcb_cnode_index 1 \<mapsto> tcb_vtable tcb, tcb_cnode_index 2 \<mapsto> tcb_reply tcb, tcb_cnode_index 3 \<mapsto> tcb_caller tcb, tcb_cnode_index 4 \<mapsto> tcb_ipcframe tcb] | _ \<Rightarrow> fail;
case caps b of None \<Rightarrow> fail | Some x \<Rightarrow> return x
od) proof (prove)
goal (5 subgoals):
 1. \<And>a b x y x11 x12. \<lbrakk>ptr' = transform_cslot_ptr (a, b); ptr = (a, b); valid_idle x; not_idle_thread a x; valid_etcbs x; kheap x a = Some y; y = kernel_object.CNode x11 x12\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, b)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (do caps <- case y of kernel_object.CNode sz cnode \<Rightarrow> do assert (well_formed_cnode_n sz cnode);
return cnode
od | TCB tcb \<Rightarrow> return [tcb_cnode_index 0 \<mapsto> tcb_ctable tcb, tcb_cnode_index 1 \<mapsto> tcb_vtable tcb, tcb_cnode_index 2 \<mapsto> tcb_reply tcb, tcb_cnode_index 3 \<mapsto> tcb_caller tcb, tcb_cnode_index 4 \<mapsto> tcb_ipcframe tcb] | _ \<Rightarrow> fail;
case caps b of None \<Rightarrow> fail | Some x \<Rightarrow> return x
od)
 2. \<And>a b x y x2. \<lbrakk>ptr' = transform_cslot_ptr (a, b); ptr = (a, b); valid_idle x; not_idle_thread a x; valid_etcbs x; kheap x a = Some y; y = TCB x2\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, b)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (do caps <- case y of kernel_object.CNode sz cnode \<Rightarrow> do assert (well_formed_cnode_n sz cnode);
return cnode
od | TCB tcb \<Rightarrow> return [tcb_cnode_index 0 \<mapsto> tcb_ctable tcb, tcb_cnode_index 1 \<mapsto> tcb_vtable tcb, tcb_cnode_index 2 \<mapsto> tcb_reply tcb, tcb_cnode_index 3 \<mapsto> tcb_caller tcb, tcb_cnode_index 4 \<mapsto> tcb_ipcframe tcb] | _ \<Rightarrow> fail;
case caps b of None \<Rightarrow> fail | Some x \<Rightarrow> return x
od)
 3. \<And>a b x y x3. \<lbrakk>ptr' = transform_cslot_ptr (a, b); ptr = (a, b); valid_idle x; not_idle_thread a x; valid_etcbs x; kheap x a = Some y; y = kernel_object.Endpoint x3\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, b)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (do caps <- case y of kernel_object.CNode sz cnode \<Rightarrow> do assert (well_formed_cnode_n sz cnode);
return cnode
od | TCB tcb \<Rightarrow> return [tcb_cnode_index 0 \<mapsto> tcb_ctable tcb, tcb_cnode_index 1 \<mapsto> tcb_vtable tcb, tcb_cnode_index 2 \<mapsto> tcb_reply tcb, tcb_cnode_index 3 \<mapsto> tcb_caller tcb, tcb_cnode_index 4 \<mapsto> tcb_ipcframe tcb] | _ \<Rightarrow> fail;
case caps b of None \<Rightarrow> fail | Some x \<Rightarrow> return x
od)
 4. \<And>a b x y x4. \<lbrakk>ptr' = transform_cslot_ptr (a, b); ptr = (a, b); valid_idle x; not_idle_thread a x; valid_etcbs x; kheap x a = Some y; y = kernel_object.Notification x4\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, b)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (do caps <- case y of kernel_object.CNode sz cnode \<Rightarrow> do assert (well_formed_cnode_n sz cnode);
return cnode
od | TCB tcb \<Rightarrow> return [tcb_cnode_index 0 \<mapsto> tcb_ctable tcb, tcb_cnode_index 1 \<mapsto> tcb_vtable tcb, tcb_cnode_index 2 \<mapsto> tcb_reply tcb, tcb_cnode_index 3 \<mapsto> tcb_caller tcb, tcb_cnode_index 4 \<mapsto> tcb_ipcframe tcb] | _ \<Rightarrow> fail;
case caps b of None \<Rightarrow> fail | Some x \<Rightarrow> return x
od)
 5. \<And>a b x y x5. \<lbrakk>ptr' = transform_cslot_ptr (a, b); ptr = (a, b); valid_idle x; not_idle_thread a x; valid_etcbs x; kheap x a = Some y; y = ArchObj x5\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, b)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (do caps <- case y of kernel_object.CNode sz cnode \<Rightarrow> do assert (well_formed_cnode_n sz cnode);
return cnode
od | TCB tcb \<Rightarrow> return [tcb_cnode_index 0 \<mapsto> tcb_ctable tcb, tcb_cnode_index 1 \<mapsto> tcb_vtable tcb, tcb_cnode_index 2 \<mapsto> tcb_reply tcb, tcb_cnode_index 3 \<mapsto> tcb_caller tcb, tcb_cnode_index 4 \<mapsto> tcb_ipcframe tcb] | _ \<Rightarrow> fail;
case caps b of None \<Rightarrow> fail | Some x \<Rightarrow> return x
od) proof (prove)
goal (2 subgoals):
 1. \<And>a b x y x11 x12. \<lbrakk>ptr' = transform_cslot_ptr (a, b); ptr = (a, b); valid_idle x; not_idle_thread a x; valid_etcbs x; kheap x a = Some (kernel_object.CNode x11 x12); y = kernel_object.CNode x11 x12\<rbrakk> \<Longrightarrow> well_formed_cnode_n x11 x12 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, b)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (case x12 b of None \<Rightarrow> fail | Some x \<Rightarrow> return x)
 2. \<And>a b x y x2. \<lbrakk>ptr' = transform_cslot_ptr (a, b); ptr = (a, b); valid_idle x; not_idle_thread a x; valid_etcbs x; kheap x a = Some (TCB x2); y = TCB x2\<rbrakk> \<Longrightarrow> (b = tcb_cnode_index 0 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, tcb_cnode_index 0)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_ctable x2))) \<and> (b \<noteq> tcb_cnode_index 0 \<longrightarrow> (b = tcb_cnode_index (Suc 0) \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, tcb_cnode_index (Suc 0))) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_vtable x2))) \<and> (b \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (b = tcb_cnode_index 2 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, tcb_cnode_index 2)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_reply x2))) \<and> (b \<noteq> tcb_cnode_index 2 \<longrightarrow> (b = tcb_cnode_index 3 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, tcb_cnode_index 3)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_caller x2))) \<and> (b \<noteq> tcb_cnode_index 3 \<longrightarrow> b = tcb_cnode_index 4 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, tcb_cnode_index 4)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_ipcframe x2)))))) proof (prove)
goal (2 subgoals):
 1. \<And>a b x y nat fun. \<lbrakk>ptr' = transform_cslot_ptr (a, b); ptr = (a, b); valid_idle x; not_idle_thread a x; valid_etcbs x; kheap x a = Some (kernel_object.CNode nat fun); y = kernel_object.CNode nat fun\<rbrakk> \<Longrightarrow> well_formed_cnode_n nat fun \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, b)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (case fun b of None \<Rightarrow> fail | Some x \<Rightarrow> return x)
 2. \<And>a b x y x2. \<lbrakk>ptr' = transform_cslot_ptr (a, b); ptr = (a, b); valid_idle x; not_idle_thread a x; valid_etcbs x; kheap x a = Some (TCB x2); y = TCB x2\<rbrakk> \<Longrightarrow> (b = tcb_cnode_index 0 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, tcb_cnode_index 0)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_ctable x2))) \<and> (b \<noteq> tcb_cnode_index 0 \<longrightarrow> (b = tcb_cnode_index (Suc 0) \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, tcb_cnode_index (Suc 0))) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_vtable x2))) \<and> (b \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (b = tcb_cnode_index 2 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, tcb_cnode_index 2)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_reply x2))) \<and> (b \<noteq> tcb_cnode_index 2 \<longrightarrow> (b = tcb_cnode_index 3 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, tcb_cnode_index 3)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_caller x2))) \<and> (b \<noteq> tcb_cnode_index 3 \<longrightarrow> b = tcb_cnode_index 4 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, tcb_cnode_index 4)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_ipcframe x2)))))) proof (prove)
goal (3 subgoals):
 1. \<And>a b x y nat fun. \<lbrakk>ptr' = transform_cslot_ptr (a, b); ptr = (a, b); valid_idle x; not_idle_thread a x; valid_etcbs x; kheap x a = Some (kernel_object.CNode nat fun); y = kernel_object.CNode nat fun; fun b = None\<rbrakk> \<Longrightarrow> well_formed_cnode_n nat fun \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, b)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (case fun b of None \<Rightarrow> fail | Some x \<Rightarrow> return x)
 2. \<And>a b x y nat fun aa. \<lbrakk>ptr' = transform_cslot_ptr (a, b); ptr = (a, b); valid_idle x; not_idle_thread a x; valid_etcbs x; kheap x a = Some (kernel_object.CNode nat fun); y = kernel_object.CNode nat fun; fun b = Some aa\<rbrakk> \<Longrightarrow> well_formed_cnode_n nat fun \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, b)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (case fun b of None \<Rightarrow> fail | Some x \<Rightarrow> return x)
 3. \<And>a b x y x2. \<lbrakk>ptr' = transform_cslot_ptr (a, b); ptr = (a, b); valid_idle x; not_idle_thread a x; valid_etcbs x; kheap x a = Some (TCB x2); y = TCB x2\<rbrakk> \<Longrightarrow> (b = tcb_cnode_index 0 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, tcb_cnode_index 0)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_ctable x2))) \<and> (b \<noteq> tcb_cnode_index 0 \<longrightarrow> (b = tcb_cnode_index (Suc 0) \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, tcb_cnode_index (Suc 0))) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_vtable x2))) \<and> (b \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (b = tcb_cnode_index 2 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, tcb_cnode_index 2)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_reply x2))) \<and> (b \<noteq> tcb_cnode_index 2 \<longrightarrow> (b = tcb_cnode_index 3 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, tcb_cnode_index 3)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_caller x2))) \<and> (b \<noteq> tcb_cnode_index 3 \<longrightarrow> b = tcb_cnode_index 4 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, tcb_cnode_index 4)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_ipcframe x2)))))) proof (prove)
goal (2 subgoals):
 1. \<And>a b x y nat fun aa. \<lbrakk>ptr' = transform_cslot_ptr (a, b); ptr = (a, b); valid_idle x; not_idle_thread a x; valid_etcbs x; kheap x a = Some (kernel_object.CNode nat fun); y = kernel_object.CNode nat fun; fun b = Some aa\<rbrakk> \<Longrightarrow> well_formed_cnode_n nat fun \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, b)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (case fun b of None \<Rightarrow> fail | Some x \<Rightarrow> return x)
 2. \<And>a b x y x2. \<lbrakk>ptr' = transform_cslot_ptr (a, b); ptr = (a, b); valid_idle x; not_idle_thread a x; valid_etcbs x; kheap x a = Some (TCB x2); y = TCB x2\<rbrakk> \<Longrightarrow> (b = tcb_cnode_index 0 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, tcb_cnode_index 0)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_ctable x2))) \<and> (b \<noteq> tcb_cnode_index 0 \<longrightarrow> (b = tcb_cnode_index (Suc 0) \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, tcb_cnode_index (Suc 0))) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_vtable x2))) \<and> (b \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (b = tcb_cnode_index 2 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, tcb_cnode_index 2)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_reply x2))) \<and> (b \<noteq> tcb_cnode_index 2 \<longrightarrow> (b = tcb_cnode_index 3 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, tcb_cnode_index 3)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_caller x2))) \<and> (b \<noteq> tcb_cnode_index 3 \<longrightarrow> b = tcb_cnode_index 4 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, tcb_cnode_index 4)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_ipcframe x2)))))) proof (prove)
goal (2 subgoals):
 1. \<And>a b x nat fun aa. \<lbrakk>ptr' = transform_cslot_ptr (a, b); ptr = (a, b); valid_idle x; not_idle_thread a x; valid_etcbs x; kheap x a = Some (kernel_object.CNode nat fun); fun b = Some aa; well_formed_cnode_n nat fun\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, b)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return aa)
 2. \<And>a b x y x2. \<lbrakk>ptr' = transform_cslot_ptr (a, b); ptr = (a, b); valid_idle x; not_idle_thread a x; valid_etcbs x; kheap x a = Some (TCB x2); y = TCB x2\<rbrakk> \<Longrightarrow> (b = tcb_cnode_index 0 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, tcb_cnode_index 0)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_ctable x2))) \<and> (b \<noteq> tcb_cnode_index 0 \<longrightarrow> (b = tcb_cnode_index (Suc 0) \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, tcb_cnode_index (Suc 0))) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_vtable x2))) \<and> (b \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (b = tcb_cnode_index 2 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, tcb_cnode_index 2)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_reply x2))) \<and> (b \<noteq> tcb_cnode_index 2 \<longrightarrow> (b = tcb_cnode_index 3 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, tcb_cnode_index 3)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_caller x2))) \<and> (b \<noteq> tcb_cnode_index 3 \<longrightarrow> b = tcb_cnode_index 4 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, tcb_cnode_index 4)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_ipcframe x2)))))) proof (prove)
goal (2 subgoals):
 1. \<And>a b x nat fun aa. \<lbrakk>ptr' = transform_cslot_ptr (a, b); ptr = (a, b); valid_idle x; not_idle_thread a x; kheap x a = Some (kernel_object.CNode nat fun); fun b = Some aa; well_formed_cnode_n nat fun; opt_cap (transform_cslot_ptr (a, b)) (transform x) = (case fun b of None \<Rightarrow> None | Some y \<Rightarrow> Some (transform_cap y))\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, b)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return aa)
 2. \<And>a b x y x2. \<lbrakk>ptr' = transform_cslot_ptr (a, b); ptr = (a, b); valid_idle x; not_idle_thread a x; valid_etcbs x; kheap x a = Some (TCB x2); y = TCB x2\<rbrakk> \<Longrightarrow> (b = tcb_cnode_index 0 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, tcb_cnode_index 0)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_ctable x2))) \<and> (b \<noteq> tcb_cnode_index 0 \<longrightarrow> (b = tcb_cnode_index (Suc 0) \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, tcb_cnode_index (Suc 0))) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_vtable x2))) \<and> (b \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (b = tcb_cnode_index 2 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, tcb_cnode_index 2)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_reply x2))) \<and> (b \<noteq> tcb_cnode_index 2 \<longrightarrow> (b = tcb_cnode_index 3 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, tcb_cnode_index 3)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_caller x2))) \<and> (b \<noteq> tcb_cnode_index 3 \<longrightarrow> b = tcb_cnode_index 4 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, tcb_cnode_index 4)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_ipcframe x2)))))) proof (prove)
goal (1 subgoal):
 1. \<And>a b x y x2. \<lbrakk>ptr' = transform_cslot_ptr (a, b); ptr = (a, b); valid_idle x; not_idle_thread a x; valid_etcbs x; kheap x a = Some (TCB x2); y = TCB x2\<rbrakk> \<Longrightarrow> (b = tcb_cnode_index 0 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, tcb_cnode_index 0)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_ctable x2))) \<and> (b \<noteq> tcb_cnode_index 0 \<longrightarrow> (b = tcb_cnode_index (Suc 0) \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, tcb_cnode_index (Suc 0))) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_vtable x2))) \<and> (b \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (b = tcb_cnode_index 2 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, tcb_cnode_index 2)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_reply x2))) \<and> (b \<noteq> tcb_cnode_index 2 \<longrightarrow> (b = tcb_cnode_index 3 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, tcb_cnode_index 3)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_caller x2))) \<and> (b \<noteq> tcb_cnode_index 3 \<longrightarrow> b = tcb_cnode_index 4 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (transform_cslot_ptr (a, tcb_cnode_index 4)) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_ipcframe x2)))))) proof (prove)
goal (1 subgoal):
 1. \<And>a b x x2. \<lbrakk>ptr' = transform_cslot_ptr (a, b); ptr = (a, b); valid_idle x; not_idle_thread a x; valid_etcbs x; kheap x a = Some (TCB x2)\<rbrakk> \<Longrightarrow> (b = tcb_cnode_index 0 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (a, tcb_cspace_slot) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_ctable x2))) \<and> (b \<noteq> tcb_cnode_index 0 \<longrightarrow> (b = tcb_cnode_index (Suc 0) \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (a, tcb_vspace_slot) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_vtable x2))) \<and> (b \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (b = tcb_cnode_index 2 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (a, tcb_replycap_slot) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_reply x2))) \<and> (b \<noteq> tcb_cnode_index 2 \<longrightarrow> (b = tcb_cnode_index 3 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (a, tcb_caller_slot) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_caller x2))) \<and> (b \<noteq> tcb_cnode_index 3 \<longrightarrow> b = tcb_cnode_index 4 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (a, tcb_ipcbuffer_slot) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_ipcframe x2)))))) proof (prove)
goal (1 subgoal):
 1. \<And>a b x x2. \<lbrakk>ptr' = transform_cslot_ptr (a, b); ptr = (a, b); valid_idle x; not_idle_thread a x; valid_etcbs x; get_tcb a x = Some x2\<rbrakk> \<Longrightarrow> (b = tcb_cnode_index 0 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (a, tcb_cspace_slot) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_ctable x2))) \<and> (b \<noteq> tcb_cnode_index 0 \<longrightarrow> (b = tcb_cnode_index (Suc 0) \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (a, tcb_vspace_slot) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_vtable x2))) \<and> (b \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (b = tcb_cnode_index 2 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (a, tcb_replycap_slot) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_reply x2))) \<and> (b \<noteq> tcb_cnode_index 2 \<longrightarrow> (b = tcb_cnode_index 3 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (a, tcb_caller_slot) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_caller x2))) \<and> (b \<noteq> tcb_cnode_index 3 \<longrightarrow> b = tcb_cnode_index 4 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (a, tcb_ipcbuffer_slot) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_ipcframe x2)))))) proof (prove)
goal (1 subgoal):
 1. \<And>a b x x2. \<lbrakk>ptr' = transform_cslot_ptr (a, b); ptr = (a, b); valid_idle x; not_idle_thread a x; get_tcb a x = Some x2; \<exists>etcb. get_etcb a x = Some etcb\<rbrakk> \<Longrightarrow> (b = tcb_cnode_index 0 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (a, tcb_cspace_slot) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_ctable x2))) \<and> (b \<noteq> tcb_cnode_index 0 \<longrightarrow> (b = tcb_cnode_index (Suc 0) \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (a, tcb_vspace_slot) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_vtable x2))) \<and> (b \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (b = tcb_cnode_index 2 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (a, tcb_replycap_slot) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_reply x2))) \<and> (b \<noteq> tcb_cnode_index 2 \<longrightarrow> (b = tcb_cnode_index 3 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (a, tcb_caller_slot) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_caller x2))) \<and> (b \<noteq> tcb_cnode_index 3 \<longrightarrow> b = tcb_cnode_index 4 \<longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_cap rv') ((=) (transform x)) ((=) x) (case opt_cap (a, tcb_ipcbuffer_slot) (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (tcb_ipcframe x2)))))) proof (prove)
goal:
No subgoals!