theory Interrupt_DR

lemma option_get_cap_corres:
  "ptr' = transform_cslot_ptr ptr \<Longrightarrow>
   dcorres (\<lambda>rv rv'. rv = Some (transform_cap rv')) \<top>
   (valid_idle and not_idle_thread (fst ptr) and valid_etcbs)
     (gets (KHeap_D.opt_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 "fun") apply (case_tac "fun b") apply (simp add:corres_free_fail) apply clarsimp apply (subst cap_slot_cnode_property_lift, assumption, simp_all)[1] apply fastforce apply (clarsimp simp: transform_cap_def) apply (clarsimp simp:transform_tcb_slot_simp[simplified]) apply (rename_tac tcb) apply (subgoal_tac "get_tcb a x = Some tcb") apply (frule(1) valid_etcbs_get_tcb_get_etcb) apply (clarsimp simp:lift_simp not_idle_thread_def) apply (clarsimp simp: get_tcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr' = transform_cslot_ptr ptr \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = Some (transform_cap rv')) (\<lambda>_. True) (valid_idle and not_idle_thread (fst ptr) and valid_etcbs) (gets (opt_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 = Some (transform_cap rv')) (\<lambda>_. True) (valid_idle and not_idle_thread (fst ptr) and valid_etcbs) (gets (opt_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 = Some (transform_cap rv')) (\<lambda>_. True) (valid_idle and not_idle_thread a and valid_etcbs) (do s <- get;
return (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 = Some (transform_cap rv')) ((=) s) ((=) x) (return (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 = Some (transform_cap rv')) ((=) (transform x)) ((=) x) (return (opt_cap (transform_cslot_ptr (a, b)) (transform 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 = Some (transform_cap rv')) ((=) (transform x)) ((=) x) (return (opt_cap (transform_cslot_ptr (a, b)) (transform 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 = Some (transform_cap rv')) ((=) (transform x)) ((=) x) (return (opt_cap (transform_cslot_ptr (a, b)) (transform 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 = Some (transform_cap rv')) ((=) (transform x)) ((=) x) (return (opt_cap (transform_cslot_ptr (a, b)) (transform 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 = Some (transform_cap rv')) ((=) (transform x)) ((=) x) (return (opt_cap (transform_cslot_ptr (a, b)) (transform 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 = Some (transform_cap rv')) ((=) (transform x)) ((=) x) (return (opt_cap (transform_cslot_ptr (a, b)) (transform 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 = Some (transform_cap rv')) ((=) (transform x)) ((=) x) (return (opt_cap (transform_cslot_ptr (a, b)) (transform 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> opt_cap (transform_cslot_ptr (a, tcb_cnode_index 0)) (transform x) = Some (transform_cap (tcb_ctable x2))) \<and> (b \<noteq> tcb_cnode_index 0 \<longrightarrow> (b = tcb_cnode_index (Suc 0) \<longrightarrow> opt_cap (transform_cslot_ptr (a, tcb_cnode_index (Suc 0))) (transform x) = Some (transform_cap (tcb_vtable x2))) \<and> (b \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (b = tcb_cnode_index 2 \<longrightarrow> opt_cap (transform_cslot_ptr (a, tcb_cnode_index 2)) (transform x) = Some (transform_cap (tcb_reply x2))) \<and> (b \<noteq> tcb_cnode_index 2 \<longrightarrow> (b = tcb_cnode_index 3 \<longrightarrow> opt_cap (transform_cslot_ptr (a, tcb_cnode_index 3)) (transform x) = Some (transform_cap (tcb_caller x2))) \<and> (b \<noteq> tcb_cnode_index 3 \<longrightarrow> b = tcb_cnode_index 4 \<longrightarrow> opt_cap (transform_cslot_ptr (a, tcb_cnode_index 4)) (transform x) = Some (transform_cap (tcb_ipcframe x2)))))) proof (prove)
goal (2 subgoals):
 1. \<And>a b x y x11 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 x11 fun); y = kernel_object.CNode x11 fun\<rbrakk> \<Longrightarrow> well_formed_cnode_n x11 fun \<longrightarrow> dcorres (\<lambda>rv rv'. rv = Some (transform_cap rv')) ((=) (transform x)) ((=) x) (return (opt_cap (transform_cslot_ptr (a, b)) (transform 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> opt_cap (transform_cslot_ptr (a, tcb_cnode_index 0)) (transform x) = Some (transform_cap (tcb_ctable x2))) \<and> (b \<noteq> tcb_cnode_index 0 \<longrightarrow> (b = tcb_cnode_index (Suc 0) \<longrightarrow> opt_cap (transform_cslot_ptr (a, tcb_cnode_index (Suc 0))) (transform x) = Some (transform_cap (tcb_vtable x2))) \<and> (b \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (b = tcb_cnode_index 2 \<longrightarrow> opt_cap (transform_cslot_ptr (a, tcb_cnode_index 2)) (transform x) = Some (transform_cap (tcb_reply x2))) \<and> (b \<noteq> tcb_cnode_index 2 \<longrightarrow> (b = tcb_cnode_index 3 \<longrightarrow> opt_cap (transform_cslot_ptr (a, tcb_cnode_index 3)) (transform x) = Some (transform_cap (tcb_caller x2))) \<and> (b \<noteq> tcb_cnode_index 3 \<longrightarrow> b = tcb_cnode_index 4 \<longrightarrow> opt_cap (transform_cslot_ptr (a, tcb_cnode_index 4)) (transform x) = Some (transform_cap (tcb_ipcframe x2)))))) proof (prove)
goal (3 subgoals):
 1. \<And>a b x y x11 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 x11 fun); y = kernel_object.CNode x11 fun; fun b = None\<rbrakk> \<Longrightarrow> well_formed_cnode_n x11 fun \<longrightarrow> dcorres (\<lambda>rv rv'. rv = Some (transform_cap rv')) ((=) (transform x)) ((=) x) (return (opt_cap (transform_cslot_ptr (a, b)) (transform x))) (case fun b of None \<Rightarrow> fail | Some x \<Rightarrow> return x)
 2. \<And>a b x y x11 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 x11 fun); y = kernel_object.CNode x11 fun; fun b = Some aa\<rbrakk> \<Longrightarrow> well_formed_cnode_n x11 fun \<longrightarrow> dcorres (\<lambda>rv rv'. rv = Some (transform_cap rv')) ((=) (transform x)) ((=) x) (return (opt_cap (transform_cslot_ptr (a, b)) (transform 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> opt_cap (transform_cslot_ptr (a, tcb_cnode_index 0)) (transform x) = Some (transform_cap (tcb_ctable x2))) \<and> (b \<noteq> tcb_cnode_index 0 \<longrightarrow> (b = tcb_cnode_index (Suc 0) \<longrightarrow> opt_cap (transform_cslot_ptr (a, tcb_cnode_index (Suc 0))) (transform x) = Some (transform_cap (tcb_vtable x2))) \<and> (b \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (b = tcb_cnode_index 2 \<longrightarrow> opt_cap (transform_cslot_ptr (a, tcb_cnode_index 2)) (transform x) = Some (transform_cap (tcb_reply x2))) \<and> (b \<noteq> tcb_cnode_index 2 \<longrightarrow> (b = tcb_cnode_index 3 \<longrightarrow> opt_cap (transform_cslot_ptr (a, tcb_cnode_index 3)) (transform x) = Some (transform_cap (tcb_caller x2))) \<and> (b \<noteq> tcb_cnode_index 3 \<longrightarrow> b = tcb_cnode_index 4 \<longrightarrow> opt_cap (transform_cslot_ptr (a, tcb_cnode_index 4)) (transform x) = Some (transform_cap (tcb_ipcframe x2)))))) proof (prove)
goal (2 subgoals):
 1. \<And>a b x y x11 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 x11 fun); y = kernel_object.CNode x11 fun; fun b = Some aa\<rbrakk> \<Longrightarrow> well_formed_cnode_n x11 fun \<longrightarrow> dcorres (\<lambda>rv rv'. rv = Some (transform_cap rv')) ((=) (transform x)) ((=) x) (return (opt_cap (transform_cslot_ptr (a, b)) (transform 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> opt_cap (transform_cslot_ptr (a, tcb_cnode_index 0)) (transform x) = Some (transform_cap (tcb_ctable x2))) \<and> (b \<noteq> tcb_cnode_index 0 \<longrightarrow> (b = tcb_cnode_index (Suc 0) \<longrightarrow> opt_cap (transform_cslot_ptr (a, tcb_cnode_index (Suc 0))) (transform x) = Some (transform_cap (tcb_vtable x2))) \<and> (b \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (b = tcb_cnode_index 2 \<longrightarrow> opt_cap (transform_cslot_ptr (a, tcb_cnode_index 2)) (transform x) = Some (transform_cap (tcb_reply x2))) \<and> (b \<noteq> tcb_cnode_index 2 \<longrightarrow> (b = tcb_cnode_index 3 \<longrightarrow> opt_cap (transform_cslot_ptr (a, tcb_cnode_index 3)) (transform x) = Some (transform_cap (tcb_caller x2))) \<and> (b \<noteq> tcb_cnode_index 3 \<longrightarrow> b = tcb_cnode_index 4 \<longrightarrow> opt_cap (transform_cslot_ptr (a, tcb_cnode_index 4)) (transform x) = Some (transform_cap (tcb_ipcframe x2)))))) proof (prove)
goal (2 subgoals):
 1. \<And>a b x x11 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 x11 fun); fun b = Some aa; well_formed_cnode_n x11 fun\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr (a, b)) (transform x) = Some (transform_cap 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> opt_cap (transform_cslot_ptr (a, tcb_cnode_index 0)) (transform x) = Some (transform_cap (tcb_ctable x2))) \<and> (b \<noteq> tcb_cnode_index 0 \<longrightarrow> (b = tcb_cnode_index (Suc 0) \<longrightarrow> opt_cap (transform_cslot_ptr (a, tcb_cnode_index (Suc 0))) (transform x) = Some (transform_cap (tcb_vtable x2))) \<and> (b \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (b = tcb_cnode_index 2 \<longrightarrow> opt_cap (transform_cslot_ptr (a, tcb_cnode_index 2)) (transform x) = Some (transform_cap (tcb_reply x2))) \<and> (b \<noteq> tcb_cnode_index 2 \<longrightarrow> (b = tcb_cnode_index 3 \<longrightarrow> opt_cap (transform_cslot_ptr (a, tcb_cnode_index 3)) (transform x) = Some (transform_cap (tcb_caller x2))) \<and> (b \<noteq> tcb_cnode_index 3 \<longrightarrow> b = tcb_cnode_index 4 \<longrightarrow> opt_cap (transform_cslot_ptr (a, tcb_cnode_index 4)) (transform x) = Some (transform_cap (tcb_ipcframe x2)))))) proof (prove)
goal (3 subgoals):
 1. \<And>a b x x11 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 x11 fun); fun b = Some aa; well_formed_cnode_n x11 fun\<rbrakk> \<Longrightarrow> b \<in> dom fun
 2. \<And>a b x x11 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 x11 fun); fun b = Some aa; well_formed_cnode_n x11 fun\<rbrakk> \<Longrightarrow> (case fun b of None \<Rightarrow> None | Some y \<Rightarrow> Some (transform_cap y)) = Some (transform_cap aa)
 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> opt_cap (transform_cslot_ptr (a, tcb_cnode_index 0)) (transform x) = Some (transform_cap (tcb_ctable x2))) \<and> (b \<noteq> tcb_cnode_index 0 \<longrightarrow> (b = tcb_cnode_index (Suc 0) \<longrightarrow> opt_cap (transform_cslot_ptr (a, tcb_cnode_index (Suc 0))) (transform x) = Some (transform_cap (tcb_vtable x2))) \<and> (b \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (b = tcb_cnode_index 2 \<longrightarrow> opt_cap (transform_cslot_ptr (a, tcb_cnode_index 2)) (transform x) = Some (transform_cap (tcb_reply x2))) \<and> (b \<noteq> tcb_cnode_index 2 \<longrightarrow> (b = tcb_cnode_index 3 \<longrightarrow> opt_cap (transform_cslot_ptr (a, tcb_cnode_index 3)) (transform x) = Some (transform_cap (tcb_caller x2))) \<and> (b \<noteq> tcb_cnode_index 3 \<longrightarrow> b = tcb_cnode_index 4 \<longrightarrow> opt_cap (transform_cslot_ptr (a, tcb_cnode_index 4)) (transform x) = Some (transform_cap (tcb_ipcframe x2)))))) proof (prove)
goal (2 subgoals):
 1. \<And>a b x x11 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 x11 fun); fun b = Some aa; well_formed_cnode_n x11 fun\<rbrakk> \<Longrightarrow> (case fun b of None \<Rightarrow> None | Some y \<Rightarrow> Some (transform_cap y)) = Some (transform_cap 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> opt_cap (transform_cslot_ptr (a, tcb_cnode_index 0)) (transform x) = Some (transform_cap (tcb_ctable x2))) \<and> (b \<noteq> tcb_cnode_index 0 \<longrightarrow> (b = tcb_cnode_index (Suc 0) \<longrightarrow> opt_cap (transform_cslot_ptr (a, tcb_cnode_index (Suc 0))) (transform x) = Some (transform_cap (tcb_vtable x2))) \<and> (b \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (b = tcb_cnode_index 2 \<longrightarrow> opt_cap (transform_cslot_ptr (a, tcb_cnode_index 2)) (transform x) = Some (transform_cap (tcb_reply x2))) \<and> (b \<noteq> tcb_cnode_index 2 \<longrightarrow> (b = tcb_cnode_index 3 \<longrightarrow> opt_cap (transform_cslot_ptr (a, tcb_cnode_index 3)) (transform x) = Some (transform_cap (tcb_caller x2))) \<and> (b \<noteq> tcb_cnode_index 3 \<longrightarrow> b = tcb_cnode_index 4 \<longrightarrow> opt_cap (transform_cslot_ptr (a, tcb_cnode_index 4)) (transform x) = Some (transform_cap (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> opt_cap (transform_cslot_ptr (a, tcb_cnode_index 0)) (transform x) = Some (transform_cap (tcb_ctable x2))) \<and> (b \<noteq> tcb_cnode_index 0 \<longrightarrow> (b = tcb_cnode_index (Suc 0) \<longrightarrow> opt_cap (transform_cslot_ptr (a, tcb_cnode_index (Suc 0))) (transform x) = Some (transform_cap (tcb_vtable x2))) \<and> (b \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (b = tcb_cnode_index 2 \<longrightarrow> opt_cap (transform_cslot_ptr (a, tcb_cnode_index 2)) (transform x) = Some (transform_cap (tcb_reply x2))) \<and> (b \<noteq> tcb_cnode_index 2 \<longrightarrow> (b = tcb_cnode_index 3 \<longrightarrow> opt_cap (transform_cslot_ptr (a, tcb_cnode_index 3)) (transform x) = Some (transform_cap (tcb_caller x2))) \<and> (b \<noteq> tcb_cnode_index 3 \<longrightarrow> b = tcb_cnode_index 4 \<longrightarrow> opt_cap (transform_cslot_ptr (a, tcb_cnode_index 4)) (transform x) = Some (transform_cap (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> opt_cap (a, tcb_cspace_slot) (transform x) = Some (transform_cap (tcb_ctable x2))) \<and> (b \<noteq> tcb_cnode_index 0 \<longrightarrow> (b = tcb_cnode_index (Suc 0) \<longrightarrow> opt_cap (a, tcb_vspace_slot) (transform x) = Some (transform_cap (tcb_vtable x2))) \<and> (b \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (b = tcb_cnode_index 2 \<longrightarrow> opt_cap (a, tcb_replycap_slot) (transform x) = Some (transform_cap (tcb_reply x2))) \<and> (b \<noteq> tcb_cnode_index 2 \<longrightarrow> (b = tcb_cnode_index 3 \<longrightarrow> opt_cap (a, tcb_caller_slot) (transform x) = Some (transform_cap (tcb_caller x2))) \<and> (b \<noteq> tcb_cnode_index 3 \<longrightarrow> b = tcb_cnode_index 4 \<longrightarrow> opt_cap (a, tcb_ipcbuffer_slot) (transform x) = Some (transform_cap (tcb_ipcframe x2)))))) proof (prove)
goal (1 subgoal):
 1. \<And>a b x tcb. \<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 tcb)\<rbrakk> \<Longrightarrow> (b = tcb_cnode_index 0 \<longrightarrow> opt_cap (a, tcb_cspace_slot) (transform x) = Some (transform_cap (tcb_ctable tcb))) \<and> (b \<noteq> tcb_cnode_index 0 \<longrightarrow> (b = tcb_cnode_index (Suc 0) \<longrightarrow> opt_cap (a, tcb_vspace_slot) (transform x) = Some (transform_cap (tcb_vtable tcb))) \<and> (b \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (b = tcb_cnode_index 2 \<longrightarrow> opt_cap (a, tcb_replycap_slot) (transform x) = Some (transform_cap (tcb_reply tcb))) \<and> (b \<noteq> tcb_cnode_index 2 \<longrightarrow> (b = tcb_cnode_index 3 \<longrightarrow> opt_cap (a, tcb_caller_slot) (transform x) = Some (transform_cap (tcb_caller tcb))) \<and> (b \<noteq> tcb_cnode_index 3 \<longrightarrow> b = tcb_cnode_index 4 \<longrightarrow> opt_cap (a, tcb_ipcbuffer_slot) (transform x) = Some (transform_cap (tcb_ipcframe tcb)))))) proof (prove)
goal (2 subgoals):
 1. \<And>a b x tcb. \<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 tcb); get_tcb a x = Some tcb\<rbrakk> \<Longrightarrow> (b = tcb_cnode_index 0 \<longrightarrow> opt_cap (a, tcb_cspace_slot) (transform x) = Some (transform_cap (tcb_ctable tcb))) \<and> (b \<noteq> tcb_cnode_index 0 \<longrightarrow> (b = tcb_cnode_index (Suc 0) \<longrightarrow> opt_cap (a, tcb_vspace_slot) (transform x) = Some (transform_cap (tcb_vtable tcb))) \<and> (b \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (b = tcb_cnode_index 2 \<longrightarrow> opt_cap (a, tcb_replycap_slot) (transform x) = Some (transform_cap (tcb_reply tcb))) \<and> (b \<noteq> tcb_cnode_index 2 \<longrightarrow> (b = tcb_cnode_index 3 \<longrightarrow> opt_cap (a, tcb_caller_slot) (transform x) = Some (transform_cap (tcb_caller tcb))) \<and> (b \<noteq> tcb_cnode_index 3 \<longrightarrow> b = tcb_cnode_index 4 \<longrightarrow> opt_cap (a, tcb_ipcbuffer_slot) (transform x) = Some (transform_cap (tcb_ipcframe tcb))))))
 2. \<And>a b x tcb. \<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 tcb)\<rbrakk> \<Longrightarrow> get_tcb a x = Some tcb proof (prove)
goal (2 subgoals):
 1. \<And>a b x tcb. \<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 tcb); get_tcb a x = Some tcb; \<exists>etcb. get_etcb a x = Some etcb\<rbrakk> \<Longrightarrow> (b = tcb_cnode_index 0 \<longrightarrow> opt_cap (a, tcb_cspace_slot) (transform x) = Some (transform_cap (tcb_ctable tcb))) \<and> (b \<noteq> tcb_cnode_index 0 \<longrightarrow> (b = tcb_cnode_index (Suc 0) \<longrightarrow> opt_cap (a, tcb_vspace_slot) (transform x) = Some (transform_cap (tcb_vtable tcb))) \<and> (b \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (b = tcb_cnode_index 2 \<longrightarrow> opt_cap (a, tcb_replycap_slot) (transform x) = Some (transform_cap (tcb_reply tcb))) \<and> (b \<noteq> tcb_cnode_index 2 \<longrightarrow> (b = tcb_cnode_index 3 \<longrightarrow> opt_cap (a, tcb_caller_slot) (transform x) = Some (transform_cap (tcb_caller tcb))) \<and> (b \<noteq> tcb_cnode_index 3 \<longrightarrow> b = tcb_cnode_index 4 \<longrightarrow> opt_cap (a, tcb_ipcbuffer_slot) (transform x) = Some (transform_cap (tcb_ipcframe tcb))))))
 2. \<And>a b x tcb. \<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 tcb)\<rbrakk> \<Longrightarrow> get_tcb a x = Some tcb proof (prove)
goal (1 subgoal):
 1. \<And>a b x tcb. \<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 tcb)\<rbrakk> \<Longrightarrow> get_tcb a x = Some tcb proof (prove)
goal:
No subgoals!