theory KHeap_DR

lemma get_cap_no_fail:
  "dcorres r P (P' and cte_at slot) f (get_cap slot>>=h) \<Longrightarrow> dcorres r P P' f (get_cap slot>>=h)" apply (rule dcorres_expand_pfx) apply (case_tac "cte_at slot s'") apply (drule dcorres_absorb_pfx) apply simp+ apply (case_tac slot) apply (simp(no_asm) add:get_cap_def[simplified tcb_cnode_map_def]) apply (clarsimp simp:bind_assoc get_object_def gets_def) apply (rule dcorres_absorb_get_r) apply (clarsimp simp: assert_def corres_free_fail) apply (case_tac y) apply (simp_all add:corres_free_fail assert_def cte_at_cases) apply (rule impI) apply (simp add:dom_def  assert_opt_def corres_free_fail) apply (simp add:assert_opt_def corres_free_fail) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres r P (P' and cte_wp_at (\<lambda>_. True) slot) f (CSpaceAcc_A.get_cap slot >>= h) \<Longrightarrow> dcorres r P P' f (CSpaceAcc_A.get_cap slot >>= h) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>dcorres r P (P' and cte_wp_at (\<lambda>_. True) slot) f (CSpaceAcc_A.get_cap slot >>= h); s = transform s'; P s; P' s'\<rbrakk> \<Longrightarrow> dcorres r ((=) s) ((=) s') f (CSpaceAcc_A.get_cap slot >>= h) proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>dcorres r P (P' and cte_wp_at (\<lambda>_. True) slot) f (CSpaceAcc_A.get_cap slot >>= h); s = transform s'; P s; P' s'; cte_wp_at (\<lambda>_. True) slot s'\<rbrakk> \<Longrightarrow> dcorres r ((=) s) ((=) s') f (CSpaceAcc_A.get_cap slot >>= h)
 2. \<And>s s'. \<lbrakk>dcorres r P (P' and cte_wp_at (\<lambda>_. True) slot) f (CSpaceAcc_A.get_cap slot >>= h); s = transform s'; P s; P' s'; \<not> cte_wp_at (\<lambda>_. True) slot s'\<rbrakk> \<Longrightarrow> dcorres r ((=) s) ((=) s') f (CSpaceAcc_A.get_cap slot >>= h) proof (prove)
goal (5 subgoals):
 1. \<And>s s'. \<lbrakk>s = transform s'; P s; P' s'; cte_wp_at (\<lambda>_. True) slot s'\<rbrakk> \<Longrightarrow> ?s3 s s' = transform (?s'3 s s')
 2. \<And>s s'. \<lbrakk>s = transform s'; P s; P' s'; cte_wp_at (\<lambda>_. True) slot s'\<rbrakk> \<Longrightarrow> P (?s3 s s')
 3. \<And>s s'. \<lbrakk>s = transform s'; P s; P' s'; cte_wp_at (\<lambda>_. True) slot s'\<rbrakk> \<Longrightarrow> (P' and cte_wp_at (\<lambda>_. True) slot) (?s'3 s s')
 4. \<And>s s'. \<lbrakk>s = transform s'; P s; P' s'; cte_wp_at (\<lambda>_. True) slot s'; dcorres r ((=) (?s3 s s')) ((=) (?s'3 s s')) f (CSpaceAcc_A.get_cap slot >>= h)\<rbrakk> \<Longrightarrow> dcorres r ((=) s) ((=) s') f (CSpaceAcc_A.get_cap slot >>= h)
 5. \<And>s s'. \<lbrakk>dcorres r P (P' and cte_wp_at (\<lambda>_. True) slot) f (CSpaceAcc_A.get_cap slot >>= h); s = transform s'; P s; P' s'; \<not> cte_wp_at (\<lambda>_. True) slot s'\<rbrakk> \<Longrightarrow> dcorres r ((=) s) ((=) s') f (CSpaceAcc_A.get_cap slot >>= h) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>dcorres r P (P' and cte_wp_at (\<lambda>_. True) slot) f (CSpaceAcc_A.get_cap slot >>= h); s = transform s'; P (transform s'); P' s'; \<not> cte_wp_at (\<lambda>_. True) slot s'\<rbrakk> \<Longrightarrow> dcorres r ((=) (transform s')) ((=) s') f (CSpaceAcc_A.get_cap slot >>= h) proof (prove)
goal (1 subgoal):
 1. \<And>s s' a b. \<lbrakk>dcorres r P (P' and cte_wp_at (\<lambda>_. True) slot) f (CSpaceAcc_A.get_cap slot >>= h); s = transform s'; P (transform s'); P' s'; \<not> cte_wp_at (\<lambda>_. True) slot s'; slot = (a, b)\<rbrakk> \<Longrightarrow> dcorres r ((=) (transform s')) ((=) s') f (CSpaceAcc_A.get_cap slot >>= h) proof (prove)
goal (1 subgoal):
 1. \<And>s s' a b. \<lbrakk>dcorres r P (P' and cte_wp_at (\<lambda>_. True) slot) f (CSpaceAcc_A.get_cap slot >>= h); s = transform s'; P (transform s'); P' s'; \<not> cte_wp_at (\<lambda>_. True) slot s'; slot = (a, b)\<rbrakk> \<Longrightarrow> dcorres r ((=) (transform s')) ((=) s') f ((case slot of (oref, cref) \<Rightarrow> do obj <- KHeap_A.get_object oref;
caps <- case obj 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 cref)
od) >>= h) proof (prove)
goal (1 subgoal):
 1. \<And>s' a b. \<lbrakk>dcorres r P (P' and cte_wp_at (\<lambda>_. True) (a, b)) f (CSpaceAcc_A.get_cap (a, b) >>= h); P (transform s'); P' s'; \<not> cte_wp_at (\<lambda>_. True) (a, b) s'; slot = (a, b)\<rbrakk> \<Longrightarrow> dcorres r ((=) (transform s')) ((=) s') f (do x <- get;
xa <- assert (\<exists>y. kheap x a = Some y);
x <- 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 (x b) >>= h
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' a b s'a. \<lbrakk>dcorres r P (P' and cte_wp_at (\<lambda>_. True) (a, b)) f (CSpaceAcc_A.get_cap (a, b) >>= h); P (transform s'); P' s'; \<not> cte_wp_at (\<lambda>_. True) (a, b) s'; slot = (a, b); transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> dcorres r ((=) (transform s'a)) ((=) s'a) f (do x <- assert (\<exists>y. kheap s'a a = Some y);
x <- case the (kheap s'a 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 (x b) >>= h
od) proof (prove)
goal (1 subgoal):
 1. \<And>a b s'a y. \<lbrakk>dcorres r P (P' and cte_wp_at (\<lambda>_. True) (a, b)) f (CSpaceAcc_A.get_cap (a, b) >>= h); P (transform s'a); P' s'a; \<not> cte_wp_at (\<lambda>_. True) (a, b) s'a; slot = (a, b); kheap s'a a = Some y\<rbrakk> \<Longrightarrow> dcorres r ((=) (transform s'a)) ((=) s'a) f (do x <- 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;
assert_opt (x b) >>= h
od) proof (prove)
goal (5 subgoals):
 1. \<And>a b s'a y x11 x12. \<lbrakk>dcorres r P (P' and cte_wp_at (\<lambda>_. True) (a, b)) f (CSpaceAcc_A.get_cap (a, b) >>= h); P (transform s'a); P' s'a; \<not> cte_wp_at (\<lambda>_. True) (a, b) s'a; slot = (a, b); kheap s'a a = Some y; y = kernel_object.CNode x11 x12\<rbrakk> \<Longrightarrow> dcorres r ((=) (transform s'a)) ((=) s'a) f (do x <- 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;
assert_opt (x b) >>= h
od)
 2. \<And>a b s'a y x2. \<lbrakk>dcorres r P (P' and cte_wp_at (\<lambda>_. True) (a, b)) f (CSpaceAcc_A.get_cap (a, b) >>= h); P (transform s'a); P' s'a; \<not> cte_wp_at (\<lambda>_. True) (a, b) s'a; slot = (a, b); kheap s'a a = Some y; y = TCB x2\<rbrakk> \<Longrightarrow> dcorres r ((=) (transform s'a)) ((=) s'a) f (do x <- 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;
assert_opt (x b) >>= h
od)
 3. \<And>a b s'a y x3. \<lbrakk>dcorres r P (P' and cte_wp_at (\<lambda>_. True) (a, b)) f (CSpaceAcc_A.get_cap (a, b) >>= h); P (transform s'a); P' s'a; \<not> cte_wp_at (\<lambda>_. True) (a, b) s'a; slot = (a, b); kheap s'a a = Some y; y = kernel_object.Endpoint x3\<rbrakk> \<Longrightarrow> dcorres r ((=) (transform s'a)) ((=) s'a) f (do x <- 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;
assert_opt (x b) >>= h
od)
 4. \<And>a b s'a y x4. \<lbrakk>dcorres r P (P' and cte_wp_at (\<lambda>_. True) (a, b)) f (CSpaceAcc_A.get_cap (a, b) >>= h); P (transform s'a); P' s'a; \<not> cte_wp_at (\<lambda>_. True) (a, b) s'a; slot = (a, b); kheap s'a a = Some y; y = kernel_object.Notification x4\<rbrakk> \<Longrightarrow> dcorres r ((=) (transform s'a)) ((=) s'a) f (do x <- 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;
assert_opt (x b) >>= h
od)
 5. \<And>a b s'a y x5. \<lbrakk>dcorres r P (P' and cte_wp_at (\<lambda>_. True) (a, b)) f (CSpaceAcc_A.get_cap (a, b) >>= h); P (transform s'a); P' s'a; \<not> cte_wp_at (\<lambda>_. True) (a, b) s'a; slot = (a, b); kheap s'a a = Some y; y = ArchObj x5\<rbrakk> \<Longrightarrow> dcorres r ((=) (transform s'a)) ((=) s'a) f (do x <- 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;
assert_opt (x b) >>= h
od) proof (prove)
goal (2 subgoals):
 1. \<And>a b s'a y x11 x12. \<lbrakk>dcorres r P (P' and cte_wp_at (\<lambda>_. True) (a, b)) f (CSpaceAcc_A.get_cap (a, b) >>= h); P (transform s'a); P' s'a; well_formed_cnode_n x11 x12 \<longrightarrow> b \<notin> dom x12; slot = (a, b); kheap s'a a = Some (kernel_object.CNode x11 x12); y = kernel_object.CNode x11 x12\<rbrakk> \<Longrightarrow> well_formed_cnode_n x11 x12 \<longrightarrow> dcorres r ((=) (transform s'a)) ((=) s'a) f (assert_opt (x12 b) >>= h)
 2. \<And>a b s'a y x2. \<lbrakk>dcorres r P (P' and cte_wp_at (\<lambda>_. True) (a, b)) f (CSpaceAcc_A.get_cap (a, b) >>= h); P (transform s'a); P' s'a; b \<notin> dom tcb_cap_cases; slot = (a, b); kheap s'a a = Some (TCB x2); y = TCB x2\<rbrakk> \<Longrightarrow> (b = tcb_cnode_index 0 \<longrightarrow> dcorres r ((=) (transform s'a)) ((=) s'a) f (h (tcb_ctable x2))) \<and> (b \<noteq> tcb_cnode_index 0 \<longrightarrow> (b = tcb_cnode_index (Suc 0) \<longrightarrow> dcorres r ((=) (transform s'a)) ((=) s'a) f (h (tcb_vtable x2))) \<and> (b \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (b = tcb_cnode_index 2 \<longrightarrow> dcorres r ((=) (transform s'a)) ((=) s'a) f (h (tcb_reply x2))) \<and> (b \<noteq> tcb_cnode_index 2 \<longrightarrow> (b = tcb_cnode_index 3 \<longrightarrow> dcorres r ((=) (transform s'a)) ((=) s'a) f (h (tcb_caller x2))) \<and> (b \<noteq> tcb_cnode_index 3 \<longrightarrow> (b = tcb_cnode_index 4 \<longrightarrow> dcorres r ((=) (transform s'a)) ((=) s'a) f (h (tcb_ipcframe x2))) \<and> (b \<noteq> tcb_cnode_index 4 \<longrightarrow> dcorres r ((=) (transform s'a)) ((=) s'a) f (assert_opt None >>= h)))))) proof (prove)
goal (2 subgoals):
 1. \<And>a b s'a y x11 x12. \<lbrakk>dcorres r P (P' and cte_wp_at (\<lambda>_. True) (a, b)) f (CSpaceAcc_A.get_cap (a, b) >>= h); P (transform s'a); P' s'a; well_formed_cnode_n x11 x12 \<longrightarrow> b \<notin> dom x12; slot = (a, b); kheap s'a a = Some (kernel_object.CNode x11 x12); y = kernel_object.CNode x11 x12; well_formed_cnode_n x11 x12\<rbrakk> \<Longrightarrow> dcorres r ((=) (transform s'a)) ((=) s'a) f (assert_opt (x12 b) >>= h)
 2. \<And>a b s'a y x2. \<lbrakk>dcorres r P (P' and cte_wp_at (\<lambda>_. True) (a, b)) f (CSpaceAcc_A.get_cap (a, b) >>= h); P (transform s'a); P' s'a; b \<notin> dom tcb_cap_cases; slot = (a, b); kheap s'a a = Some (TCB x2); y = TCB x2\<rbrakk> \<Longrightarrow> (b = tcb_cnode_index 0 \<longrightarrow> dcorres r ((=) (transform s'a)) ((=) s'a) f (h (tcb_ctable x2))) \<and> (b \<noteq> tcb_cnode_index 0 \<longrightarrow> (b = tcb_cnode_index (Suc 0) \<longrightarrow> dcorres r ((=) (transform s'a)) ((=) s'a) f (h (tcb_vtable x2))) \<and> (b \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (b = tcb_cnode_index 2 \<longrightarrow> dcorres r ((=) (transform s'a)) ((=) s'a) f (h (tcb_reply x2))) \<and> (b \<noteq> tcb_cnode_index 2 \<longrightarrow> (b = tcb_cnode_index 3 \<longrightarrow> dcorres r ((=) (transform s'a)) ((=) s'a) f (h (tcb_caller x2))) \<and> (b \<noteq> tcb_cnode_index 3 \<longrightarrow> (b = tcb_cnode_index 4 \<longrightarrow> dcorres r ((=) (transform s'a)) ((=) s'a) f (h (tcb_ipcframe x2))) \<and> (b \<noteq> tcb_cnode_index 4 \<longrightarrow> dcorres r ((=) (transform s'a)) ((=) s'a) f (assert_opt None >>= h)))))) proof (prove)
goal (1 subgoal):
 1. \<And>a b s'a y x2. \<lbrakk>dcorres r P (P' and cte_wp_at (\<lambda>_. True) (a, b)) f (CSpaceAcc_A.get_cap (a, b) >>= h); P (transform s'a); P' s'a; b \<notin> dom tcb_cap_cases; slot = (a, b); kheap s'a a = Some (TCB x2); y = TCB x2\<rbrakk> \<Longrightarrow> (b = tcb_cnode_index 0 \<longrightarrow> dcorres r ((=) (transform s'a)) ((=) s'a) f (h (tcb_ctable x2))) \<and> (b \<noteq> tcb_cnode_index 0 \<longrightarrow> (b = tcb_cnode_index (Suc 0) \<longrightarrow> dcorres r ((=) (transform s'a)) ((=) s'a) f (h (tcb_vtable x2))) \<and> (b \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (b = tcb_cnode_index 2 \<longrightarrow> dcorres r ((=) (transform s'a)) ((=) s'a) f (h (tcb_reply x2))) \<and> (b \<noteq> tcb_cnode_index 2 \<longrightarrow> (b = tcb_cnode_index 3 \<longrightarrow> dcorres r ((=) (transform s'a)) ((=) s'a) f (h (tcb_caller x2))) \<and> (b \<noteq> tcb_cnode_index 3 \<longrightarrow> (b = tcb_cnode_index 4 \<longrightarrow> dcorres r ((=) (transform s'a)) ((=) s'a) f (h (tcb_ipcframe x2))) \<and> (b \<noteq> tcb_cnode_index 4 \<longrightarrow> dcorres r ((=) (transform s'a)) ((=) s'a) f (assert_opt None >>= h)))))) proof (prove)
goal (1 subgoal):
 1. \<And>a b s'a y x2. \<lbrakk>dcorres r P (P' and cte_wp_at (\<lambda>_. True) (a, b)) f (CSpaceAcc_A.get_cap (a, b) >>= h); P (transform s'a); P' s'a; b \<notin> dom tcb_cap_cases; slot = (a, b); kheap s'a a = Some (TCB x2); y = TCB x2\<rbrakk> \<Longrightarrow> (b = tcb_cnode_index 0 \<longrightarrow> dcorres r ((=) (transform s'a)) ((=) s'a) f (h (tcb_ctable x2))) \<and> (b \<noteq> tcb_cnode_index 0 \<longrightarrow> (b = tcb_cnode_index (Suc 0) \<longrightarrow> dcorres r ((=) (transform s'a)) ((=) s'a) f (h (tcb_vtable x2))) \<and> (b \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (b = tcb_cnode_index 2 \<longrightarrow> dcorres r ((=) (transform s'a)) ((=) s'a) f (h (tcb_reply x2))) \<and> (b \<noteq> tcb_cnode_index 2 \<longrightarrow> (b = tcb_cnode_index 3 \<longrightarrow> dcorres r ((=) (transform s'a)) ((=) s'a) f (h (tcb_caller x2))) \<and> (b \<noteq> tcb_cnode_index 3 \<longrightarrow> b = tcb_cnode_index 4 \<longrightarrow> dcorres r ((=) (transform s'a)) ((=) s'a) f (h (tcb_ipcframe x2)))))) proof (prove)
goal:
No subgoals!