theory Retype_DP

lemma set_cap_opt_cap:
  "\<lbrace>\<lambda>s. P (Some cap)\<rbrace>
  set_cap cref cap
  \<lbrace>\<lambda>rv s. P (opt_cap cref s)\<rbrace>" apply (cases cref) apply (simp add: set_cap_def gets_the_def gets_def get_def assert_opt_def bind_assoc) apply (clarsimp simp: bind_def return_def valid_def split:option.splits) apply (clarsimp simp: fail_def assert_def return_def select_def bind_def
                 split: cdl_object.split_asm) apply (simp_all add: set_object_def simpler_modify_def opt_cap_def
                                 slots_of_def has_slots_def update_slots_def
                         split: cdl_object.split_asm)+ apply (clarsimp simp: select_def return_def bind_def
                             object_slots_def update_slots_def
                      split: if_splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (Some cap)\<rbrace> set_cap cref cap \<lbrace>\<lambda>rv s. P (opt_cap cref s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b. cref = (a, b) \<Longrightarrow> \<lbrace>\<lambda>s. P (Some cap)\<rbrace> set_cap cref cap \<lbrace>\<lambda>rv s. P (opt_cap cref s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b. cref = (a, b) \<Longrightarrow> \<lbrace>\<lambda>s. P (Some cap)\<rbrace> do x <- \<lambda>s. ({(s, s)}, False);
obj <- case cdl_objects x a of None \<Rightarrow> fail | Some x \<Rightarrow> return x;
y <- assert (has_slots obj);
(case update_slots ((object_slots obj)(b \<mapsto> cap)) obj of Tcb t \<Rightarrow> if b = tcb_ipcbuffer_slot \<and> object_slots obj b \<noteq> Some cap then do intent' <- select UNIV;
return $ Tcb (t\<lparr>cdl_tcb_intent := intent'\<rparr>)
od else return (update_slots ((object_slots obj)(b \<mapsto> cap)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(b \<mapsto> cap)) obj)) >>= set_object a
od \<lbrace>\<lambda>rv s. P (opt_cap (a, b) s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b s. \<lbrakk>cref = (a, b); P (Some cap)\<rbrakk> \<Longrightarrow> (cdl_objects s a = None \<longrightarrow> (\<forall>y\<in>fst (fail s). \<forall>x\<in>fst (case y of (obj, s) \<Rightarrow> (\<Union>aa\<in>fst (assert (has_slots obj) s). fst (case aa of (y, s) \<Rightarrow> (\<Union>aa\<in>fst ((case update_slots ((object_slots obj)(b \<mapsto> cap)) obj of Tcb t \<Rightarrow> if b = tcb_ipcbuffer_slot \<and> object_slots obj b \<noteq> Some cap then do intent' <- select UNIV;
return $ Tcb (t\<lparr>cdl_tcb_intent := intent'\<rparr>)
od else return (update_slots ((object_slots obj)(b \<mapsto> cap)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(b \<mapsto> cap)) obj)) s). fst (case aa of (x, xa) \<Rightarrow> set_object a x xa), (\<exists>x\<in>fst ((case update_slots ((object_slots obj)(b \<mapsto> cap)) obj of Tcb t \<Rightarrow> if b = tcb_ipcbuffer_slot \<and> object_slots obj b \<noteq> Some cap then do intent' <- select UNIV;
return $ Tcb (t\<lparr>cdl_tcb_intent := intent'\<rparr>)
od else return (update_slots ((object_slots obj)(b \<mapsto> cap)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(b \<mapsto> cap)) obj)) s). snd (case x of (x, xa) \<Rightarrow> set_object a x xa)) \<or> snd ((case update_slots ((object_slots obj)(b \<mapsto> cap)) obj of Tcb t \<Rightarrow> if b = tcb_ipcbuffer_slot \<and> object_slots obj b \<noteq> Some cap then do intent' <- select UNIV;
return $ Tcb (t\<lparr>cdl_tcb_intent := intent'\<rparr>)
od else return (update_slots ((object_slots obj)(b \<mapsto> cap)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(b \<mapsto> cap)) obj)) s))), (\<exists>x\<in>fst (assert (has_slots obj) s). snd (case x of (y, s) \<Rightarrow> (\<Union>aa\<in>fst ((case update_slots ((object_slots obj)(b \<mapsto> cap)) obj of Tcb t \<Rightarrow> if b = tcb_ipcbuffer_slot \<and> object_slots obj b \<noteq> Some cap then do intent' <- select UNIV;
return $ Tcb (t\<lparr>cdl_tcb_intent := intent'\<rparr>)
od else return (update_slots ((object_slots obj)(b \<mapsto> cap)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(b \<mapsto> cap)) obj)) s). fst (case aa of (x, xa) \<Rightarrow> set_object a x xa), (\<exists>x\<in>fst ((case update_slots ((object_slots obj)(b \<mapsto> cap)) obj of Tcb t \<Rightarrow> if b = tcb_ipcbuffer_slot \<and> object_slots obj b \<noteq> Some cap then do intent' <- select UNIV;
return $ Tcb (t\<lparr>cdl_tcb_intent := intent'\<rparr>)
od else return (update_slots ((object_slots obj)(b \<mapsto> cap)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(b \<mapsto> cap)) obj)) s). snd (case x of (x, xa) \<Rightarrow> set_object a x xa)) \<or> snd ((case update_slots ((object_slots obj)(b \<mapsto> cap)) obj of Tcb t \<Rightarrow> if b = tcb_ipcbuffer_slot \<and> object_slots obj b \<noteq> Some cap then do intent' <- select UNIV;
return $ Tcb (t\<lparr>cdl_tcb_intent := intent'\<rparr>)
od else return (update_slots ((object_slots obj)(b \<mapsto> cap)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(b \<mapsto> cap)) obj)) s)))) \<or> snd (assert (has_slots obj) s))). case x of (r, s') \<Rightarrow> P (opt_cap (a, b) s'))) \<and> (\<forall>x2. cdl_objects s a = Some x2 \<longrightarrow> (\<forall>y\<in>fst (assert (has_slots x2) s). \<forall>x\<in>fst (case y of (y, s) \<Rightarrow> (\<Union>aa\<in>fst ((case update_slots ((object_slots x2)(b \<mapsto> cap)) x2 of Tcb t \<Rightarrow> if b = tcb_ipcbuffer_slot \<and> object_slots x2 b \<noteq> Some cap then do intent' <- select UNIV;
return $ Tcb (t\<lparr>cdl_tcb_intent := intent'\<rparr>)
od else return (update_slots ((object_slots x2)(b \<mapsto> cap)) x2) | _ \<Rightarrow> return (update_slots ((object_slots x2)(b \<mapsto> cap)) x2)) s). fst (case aa of (x, xa) \<Rightarrow> set_object a x xa), (\<exists>x\<in>fst ((case update_slots ((object_slots x2)(b \<mapsto> cap)) x2 of Tcb t \<Rightarrow> if b = tcb_ipcbuffer_slot \<and> object_slots x2 b \<noteq> Some cap then do intent' <- select UNIV;
return $ Tcb (t\<lparr>cdl_tcb_intent := intent'\<rparr>)
od else return (update_slots ((object_slots x2)(b \<mapsto> cap)) x2) | _ \<Rightarrow> return (update_slots ((object_slots x2)(b \<mapsto> cap)) x2)) s). snd (case x of (x, xa) \<Rightarrow> set_object a x xa)) \<or> snd ((case update_slots ((object_slots x2)(b \<mapsto> cap)) x2 of Tcb t \<Rightarrow> if b = tcb_ipcbuffer_slot \<and> object_slots x2 b \<noteq> Some cap then do intent' <- select UNIV;
return $ Tcb (t\<lparr>cdl_tcb_intent := intent'\<rparr>)
od else return (update_slots ((object_slots x2)(b \<mapsto> cap)) x2) | _ \<Rightarrow> return (update_slots ((object_slots x2)(b \<mapsto> cap)) x2)) s))). case x of (r, s') \<Rightarrow> P (opt_cap (a, b) s'))) proof (prove)
goal (10 subgoals):
 1. \<And>a b s x2 bb. \<lbrakk>((), bb) \<in> fst (set_object a Endpoint s); cref = (a, b); P (Some cap); has_slots x2; cdl_objects s a = Some x2; update_slots ((object_slots x2)(b \<mapsto> cap)) x2 = Endpoint\<rbrakk> \<Longrightarrow> P (opt_cap (a, b) bb)
 2. \<And>a b s x2 aa bb. \<lbrakk>((), bb) \<in> fst (set_object a Notification s); cref = (a, b); P (Some cap); has_slots x2; cdl_objects s a = Some x2; update_slots ((object_slots x2)(b \<mapsto> cap)) x2 = Notification; aa = Notification\<rbrakk> \<Longrightarrow> P (opt_cap (a, b) bb)
 3. \<And>a b s x2 aa ba bb x3. \<lbrakk>((), bb) \<in> fst (set_object a aa ba); cref = (a, b); P (Some cap); has_slots x2; cdl_objects s a = Some x2; update_slots ((object_slots x2)(b \<mapsto> cap)) x2 = Tcb x3; (aa, ba) \<in> fst ((if b = tcb_ipcbuffer_slot \<and> object_slots x2 b \<noteq> Some cap then do intent' <- select UNIV;
return $ Tcb (x3\<lparr>cdl_tcb_intent := intent'\<rparr>)
od else return (update_slots ((object_slots x2)(b \<mapsto> cap)) x2)) s)\<rbrakk> \<Longrightarrow> P (opt_cap (a, b) bb)
 4. \<And>a b s x2 aa bb x4. \<lbrakk>((), bb) \<in> fst (set_object a (CNode x4) s); cref = (a, b); P (Some cap); has_slots x2; cdl_objects s a = Some x2; update_slots ((object_slots x2)(b \<mapsto> cap)) x2 = CNode x4; aa = CNode x4\<rbrakk> \<Longrightarrow> P (opt_cap (a, b) bb)
 5. \<And>a b s x2 aa bb x5. \<lbrakk>((), bb) \<in> fst (set_object a (AsidPool x5) s); cref = (a, b); P (Some cap); has_slots x2; cdl_objects s a = Some x2; update_slots ((object_slots x2)(b \<mapsto> cap)) x2 = AsidPool x5; aa = AsidPool x5\<rbrakk> \<Longrightarrow> P (opt_cap (a, b) bb)
 6. \<And>a b s x2 aa bb x6. \<lbrakk>((), bb) \<in> fst (set_object a (PageTable x6) s); cref = (a, b); P (Some cap); has_slots x2; cdl_objects s a = Some x2; update_slots ((object_slots x2)(b \<mapsto> cap)) x2 = PageTable x6; aa = PageTable x6\<rbrakk> \<Longrightarrow> P (opt_cap (a, b) bb)
 7. \<And>a b s x2 aa bb x7. \<lbrakk>((), bb) \<in> fst (set_object a (PageDirectory x7) s); cref = (a, b); P (Some cap); has_slots x2; cdl_objects s a = Some x2; update_slots ((object_slots x2)(b \<mapsto> cap)) x2 = PageDirectory x7; aa = PageDirectory x7\<rbrakk> \<Longrightarrow> P (opt_cap (a, b) bb)
 8. \<And>a b s x2 aa bb x8. \<lbrakk>((), bb) \<in> fst (set_object a (Frame x8) s); cref = (a, b); P (Some cap); has_slots x2; cdl_objects s a = Some x2; update_slots ((object_slots x2)(b \<mapsto> cap)) x2 = Frame x8; aa = Frame x8\<rbrakk> \<Longrightarrow> P (opt_cap (a, b) bb)
 9. \<And>a b s x2 aa bb. \<lbrakk>((), bb) \<in> fst (set_object a Untyped s); cref = (a, b); P (Some cap); has_slots x2; cdl_objects s a = Some x2; update_slots ((object_slots x2)(b \<mapsto> cap)) x2 = Untyped; aa = Untyped\<rbrakk> \<Longrightarrow> P (opt_cap (a, b) bb)
 10. \<And>a b s x2 aa bb x10. \<lbrakk>((), bb) \<in> fst (set_object a (IRQNode x10) s); cref = (a, b); P (Some cap); has_slots x2; cdl_objects s a = Some x2; update_slots ((object_slots x2)(b \<mapsto> cap)) x2 = IRQNode x10; aa = IRQNode x10\<rbrakk> \<Longrightarrow> P (opt_cap (a, b) bb) proof (prove)
goal (6 subgoals):
 1. \<And>a b s x2 aa ba bb x3 x3a. \<lbrakk>cdl_objects s a = Some (Tcb x3a); x3a\<lparr>cdl_tcb_caps := (object_slots (Tcb x3a))(b \<mapsto> cap)\<rparr> = x3; (aa, ba) \<in> fst ((if b = tcb_ipcbuffer_slot \<and> object_slots (Tcb x3a) b \<noteq> Some cap then do intent' <- select UNIV;
return $ Tcb (x3\<lparr>cdl_tcb_intent := intent'\<rparr>)
od else return (update_slots ((object_slots x2)(b \<mapsto> cap)) x2)) s); bb = ba\<lparr>cdl_objects := (cdl_objects ba)(a \<mapsto> aa)\<rparr>; cref = (a, b); P (Some cap); x2 = Tcb x3a\<rbrakk> \<Longrightarrow> P (object_slots aa b)
 2. \<And>a b s x2 aa bb x4 x4a. \<lbrakk>cdl_objects s a = Some (CNode x4a); x4a\<lparr>cdl_cnode_caps := (object_slots (CNode x4a))(b \<mapsto> cap)\<rparr> = x4; aa = CNode x4; bb = s\<lparr>cdl_objects := (cdl_objects s)(a \<mapsto> CNode x4)\<rparr>; cref = (a, b); P (Some cap); x2 = CNode x4a\<rbrakk> \<Longrightarrow> P (object_slots (CNode x4) b)
 3. \<And>a b s x2 aa bb x5 x5a. \<lbrakk>cdl_objects s a = Some (AsidPool x5a); x5a\<lparr>cdl_asid_pool_caps := (object_slots (AsidPool x5a))(b \<mapsto> cap)\<rparr> = x5; aa = AsidPool x5; bb = s\<lparr>cdl_objects := (cdl_objects s)(a \<mapsto> AsidPool x5)\<rparr>; cref = (a, b); P (Some cap); x2 = AsidPool x5a\<rbrakk> \<Longrightarrow> P (object_slots (AsidPool x5) b)
 4. \<And>a b s x2 aa bb x6 x6a. \<lbrakk>cdl_objects s a = Some (PageTable x6a); x6a\<lparr>cdl_page_table_caps := (object_slots (PageTable x6a))(b \<mapsto> cap)\<rparr> = x6; aa = PageTable x6; bb = s\<lparr>cdl_objects := (cdl_objects s)(a \<mapsto> PageTable x6)\<rparr>; cref = (a, b); P (Some cap); x2 = PageTable x6a\<rbrakk> \<Longrightarrow> P (object_slots (PageTable x6) b)
 5. \<And>a b s x2 aa bb x7 x7a. \<lbrakk>cdl_objects s a = Some (PageDirectory x7a); x7a\<lparr>cdl_page_directory_caps := (object_slots (PageDirectory x7a))(b \<mapsto> cap)\<rparr> = x7; aa = PageDirectory x7; bb = s\<lparr>cdl_objects := (cdl_objects s)(a \<mapsto> PageDirectory x7)\<rparr>; cref = (a, b); P (Some cap); x2 = PageDirectory x7a\<rbrakk> \<Longrightarrow> P (object_slots (PageDirectory x7) b)
 6. \<And>a b s x2 aa bb x10 x10a. \<lbrakk>cdl_objects s a = Some (IRQNode x10a); x10a\<lparr>cdl_irq_node_caps := (object_slots (IRQNode x10a))(b \<mapsto> cap)\<rparr> = x10; aa = IRQNode x10; bb = s\<lparr>cdl_objects := (cdl_objects s)(a \<mapsto> IRQNode x10)\<rparr>; cref = (a, b); P (Some cap); x2 = IRQNode x10a\<rbrakk> \<Longrightarrow> P (object_slots (IRQNode x10) b) proof (prove)
goal:
No subgoals!