theory FinalCaps

lemma get_cap_weak_derived[wp]:
  "\<lbrace>\<top>\<rbrace> get_cap slot \<lbrace>\<lambda>rv s. cte_wp_at (weak_derived rv) slot s\<rbrace>" unfolding get_cap_def apply (wp get_object_wp | simp add: split_def | wpc)+ apply safe apply (rule cte_wp_at_cteI) apply (fastforce simp: obj_at_def) apply assumption apply assumption apply simp apply (clarsimp simp: tcb_cnode_map_tcb_cap_cases) apply (rule cte_wp_at_tcbI) apply (fastforce simp: obj_at_def) apply assumption apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> get_cap slot \<lbrace>\<lambda>rv. cte_wp_at (weak_derived rv) slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> case slot of (oref, cref) \<Rightarrow> do obj <- get_object oref;
caps <- case obj of CNode sz cnode \<Rightarrow> do assert (well_formed_cnode_n sz cnode);
return cnode
od | TCB tcb \<Rightarrow> return (tcb_cnode_map tcb) | _ \<Rightarrow> fail;
assert_opt (caps cref)
od \<lbrace>\<lambda>rv. cte_wp_at (weak_derived rv) slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>ko. ko_at ko (fst slot) s \<longrightarrow> (\<forall>x xa. ko = CNode x xa \<longrightarrow> well_formed_cnode_n x xa \<longrightarrow> (\<exists>y. xa (snd slot) = Some y) \<longrightarrow> cte_wp_at (weak_derived (the (xa (snd slot)))) slot s) \<and> (\<forall>x. ko = TCB x \<longrightarrow> (\<exists>y. tcb_cnode_map x (snd slot) = Some y) \<longrightarrow> cte_wp_at (weak_derived (the (tcb_cnode_map x (snd slot)))) slot s) proof (prove)
goal (2 subgoals):
 1. \<And>s ko x xa y. \<lbrakk>ko_at (CNode x xa) (fst slot) s; well_formed_cnode_n x xa; xa (snd slot) = Some y\<rbrakk> \<Longrightarrow> cte_wp_at (weak_derived (the (xa (snd slot)))) slot s
 2. \<And>s ko x y. \<lbrakk>ko_at (TCB x) (fst slot) s; tcb_cnode_map x (snd slot) = Some y\<rbrakk> \<Longrightarrow> cte_wp_at (weak_derived (the (tcb_cnode_map x (snd slot)))) slot s proof (prove)
goal (5 subgoals):
 1. \<And>s ko x xa y. \<lbrakk>ko_at (CNode x xa) (fst slot) s; well_formed_cnode_n x xa; xa (snd slot) = Some y\<rbrakk> \<Longrightarrow> kheap s (fst slot) = Some (CNode (?sz70 s ko x xa y) (?fun70 s ko x xa y))
 2. \<And>s ko x xa y. \<lbrakk>ko_at (CNode x xa) (fst slot) s; well_formed_cnode_n x xa; xa (snd slot) = Some y\<rbrakk> \<Longrightarrow> well_formed_cnode_n (?sz70 s ko x xa y) (?fun70 s ko x xa y)
 3. \<And>s ko x xa y. \<lbrakk>ko_at (CNode x xa) (fst slot) s; well_formed_cnode_n x xa; xa (snd slot) = Some y\<rbrakk> \<Longrightarrow> ?fun70 s ko x xa y (snd slot) = Some (?cte70 s ko x xa y)
 4. \<And>s ko x xa y. \<lbrakk>ko_at (CNode x xa) (fst slot) s; well_formed_cnode_n x xa; xa (snd slot) = Some y\<rbrakk> \<Longrightarrow> weak_derived (the (xa (snd slot))) (?cte70 s ko x xa y)
 5. \<And>s ko x y. \<lbrakk>ko_at (TCB x) (fst slot) s; tcb_cnode_map x (snd slot) = Some y\<rbrakk> \<Longrightarrow> cte_wp_at (weak_derived (the (tcb_cnode_map x (snd slot)))) slot s proof (prove)
goal (4 subgoals):
 1. \<And>s ko x xa y. \<lbrakk>ko_at (CNode x xa) (fst slot) s; well_formed_cnode_n x xa; xa (snd slot) = Some y\<rbrakk> \<Longrightarrow> well_formed_cnode_n x xa
 2. \<And>s ko x xa y. \<lbrakk>ko_at (CNode x xa) (fst slot) s; well_formed_cnode_n x xa; xa (snd slot) = Some y\<rbrakk> \<Longrightarrow> xa (snd slot) = Some (?cte70 s ko x xa y)
 3. \<And>s ko x xa y. \<lbrakk>ko_at (CNode x xa) (fst slot) s; well_formed_cnode_n x xa; xa (snd slot) = Some y\<rbrakk> \<Longrightarrow> weak_derived (the (xa (snd slot))) (?cte70 s ko x xa y)
 4. \<And>s ko x y. \<lbrakk>ko_at (TCB x) (fst slot) s; tcb_cnode_map x (snd slot) = Some y\<rbrakk> \<Longrightarrow> cte_wp_at (weak_derived (the (tcb_cnode_map x (snd slot)))) slot s proof (prove)
goal (3 subgoals):
 1. \<And>s ko x xa y. \<lbrakk>ko_at (CNode x xa) (fst slot) s; well_formed_cnode_n x xa; xa (snd slot) = Some y\<rbrakk> \<Longrightarrow> xa (snd slot) = Some (?cte70 s ko x xa y)
 2. \<And>s ko x xa y. \<lbrakk>ko_at (CNode x xa) (fst slot) s; well_formed_cnode_n x xa; xa (snd slot) = Some y\<rbrakk> \<Longrightarrow> weak_derived (the (xa (snd slot))) (?cte70 s ko x xa y)
 3. \<And>s ko x y. \<lbrakk>ko_at (TCB x) (fst slot) s; tcb_cnode_map x (snd slot) = Some y\<rbrakk> \<Longrightarrow> cte_wp_at (weak_derived (the (tcb_cnode_map x (snd slot)))) slot s proof (prove)
goal (2 subgoals):
 1. \<And>s ko x xa y. \<lbrakk>ko_at (CNode x xa) (fst slot) s; well_formed_cnode_n x xa; xa (snd slot) = Some y\<rbrakk> \<Longrightarrow> weak_derived (the (xa (snd slot))) y
 2. \<And>s ko x y. \<lbrakk>ko_at (TCB x) (fst slot) s; tcb_cnode_map x (snd slot) = Some y\<rbrakk> \<Longrightarrow> cte_wp_at (weak_derived (the (tcb_cnode_map x (snd slot)))) slot s proof (prove)
goal (1 subgoal):
 1. \<And>s ko x y. \<lbrakk>ko_at (TCB x) (fst slot) s; tcb_cnode_map x (snd slot) = Some y\<rbrakk> \<Longrightarrow> cte_wp_at (weak_derived (the (tcb_cnode_map x (snd slot)))) slot s proof (prove)
goal (1 subgoal):
 1. \<And>s x a aa b. \<lbrakk>ko_at (TCB x) (fst slot) s; tcb_cap_cases (snd slot) = Some (a, aa, b)\<rbrakk> \<Longrightarrow> cte_wp_at (weak_derived (a x)) slot s proof (prove)
goal (3 subgoals):
 1. \<And>s x a aa b. \<lbrakk>ko_at (TCB x) (fst slot) s; tcb_cap_cases (snd slot) = Some (a, aa, b)\<rbrakk> \<Longrightarrow> kheap s (fst slot) = Some (TCB (?tcb85 s x a aa b))
 2. \<And>s x a aa b. \<lbrakk>ko_at (TCB x) (fst slot) s; tcb_cap_cases (snd slot) = Some (a, aa, b)\<rbrakk> \<Longrightarrow> tcb_cap_cases (snd slot) = Some (?getF85 s x a aa b, ?setF85 s x a aa b)
 3. \<And>s x a aa b. \<lbrakk>ko_at (TCB x) (fst slot) s; tcb_cap_cases (snd slot) = Some (a, aa, b)\<rbrakk> \<Longrightarrow> weak_derived (a x) (?getF85 s x a aa b (?tcb85 s x a aa b)) proof (prove)
goal (2 subgoals):
 1. \<And>s x a aa b. \<lbrakk>ko_at (TCB x) (fst slot) s; tcb_cap_cases (snd slot) = Some (a, aa, b)\<rbrakk> \<Longrightarrow> tcb_cap_cases (snd slot) = Some (?getF85 s x a aa b, ?setF85 s x a aa b)
 2. \<And>s x a aa b. \<lbrakk>ko_at (TCB x) (fst slot) s; tcb_cap_cases (snd slot) = Some (a, aa, b)\<rbrakk> \<Longrightarrow> weak_derived (a x) (?getF85 s x a aa b x) proof (prove)
goal (1 subgoal):
 1. \<And>s x a aa b. \<lbrakk>ko_at (TCB x) (fst slot) s; tcb_cap_cases (snd slot) = Some (a, aa, b)\<rbrakk> \<Longrightarrow> weak_derived (a x) (a x) proof (prove)
goal:
No subgoals!