theory KHeap_DR

lemma set_cap_is_noop_opt_cap:
   "opt_cap ptr s = Some cap \<Longrightarrow> KHeap_D.set_cap ptr cap s = return () s" apply (clarsimp simp: opt_cap_def slots_of_def split_def
                 split: option.split_asm) apply (simp add: KHeap_D.set_cap_def split_def exec_gets gets_the_def
                   bind_assoc assert_opt_def has_slots_def
                   KHeap_D.set_object_def) apply (simp add: object_slots_def update_slots_def fun_upd_idem
            split: cdl_object.split_asm) apply (simp_all add: simpler_modify_def
                       return_def fun_upd_idem) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. opt_cap ptr s = Some cap \<Longrightarrow> KHeap_D.set_cap ptr cap s = return () s proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>cdl_objects s (fst ptr) = Some x2; object_slots x2 (snd ptr) = Some cap\<rbrakk> \<Longrightarrow> KHeap_D.set_cap ptr cap s = return () s proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>cdl_objects s (fst ptr) = Some x2; object_slots x2 (snd ptr) = Some cap\<rbrakk> \<Longrightarrow> (do y <- assert (case x2 of cdl_object.Endpoint \<Rightarrow> False | cdl_object.Notification \<Rightarrow> False | Frame cdl_frame_ext \<Rightarrow> False | cdl_object.Untyped \<Rightarrow> False | _ \<Rightarrow> True);
obj'' <- case update_slots ((object_slots x2)(snd ptr \<mapsto> cap)) x2 of Tcb t \<Rightarrow> if snd ptr = tcb_ipcbuffer_slot \<and> object_slots x2 (snd ptr) \<noteq> Some cap then do intent' <- select UNIV;
return $ Tcb (dupdate_tcb_intent intent' t)
od else return (update_slots ((object_slots x2)(snd ptr \<mapsto> cap)) x2) | _ \<Rightarrow> return (update_slots ((object_slots x2)(snd ptr \<mapsto> cap)) x2);
modify (dupdate_cdl_object (fst ptr) obj'')
od) s = return () s proof (prove)
goal (6 subgoals):
 1. \<And>x2 x3. \<lbrakk>cdl_objects s (fst ptr) = Some (Tcb x3); x2 = Tcb x3; cdl_tcb_caps x3 (snd ptr) = Some cap\<rbrakk> \<Longrightarrow> modify (dupdate_cdl_object (fst ptr) (Tcb x3)) s = return () s
 2. \<And>x2 x4. \<lbrakk>cdl_objects s (fst ptr) = Some (cdl_object.CNode x4); x2 = cdl_object.CNode x4; cdl_cnode_caps x4 (snd ptr) = Some cap\<rbrakk> \<Longrightarrow> modify (dupdate_cdl_object (fst ptr) (cdl_object.CNode x4)) s = return () s
 3. \<And>x2 x5. \<lbrakk>cdl_objects s (fst ptr) = Some (AsidPool x5); x2 = AsidPool x5; cdl_asid_pool_caps x5 (snd ptr) = Some cap\<rbrakk> \<Longrightarrow> modify (dupdate_cdl_object (fst ptr) (AsidPool x5)) s = return () s
 4. \<And>x2 x6. \<lbrakk>cdl_objects s (fst ptr) = Some (cdl_object.PageTable x6); x2 = cdl_object.PageTable x6; cdl_page_table_caps x6 (snd ptr) = Some cap\<rbrakk> \<Longrightarrow> modify (dupdate_cdl_object (fst ptr) (cdl_object.PageTable x6)) s = return () s
 5. \<And>x2 x7. \<lbrakk>cdl_objects s (fst ptr) = Some (cdl_object.PageDirectory x7); x2 = cdl_object.PageDirectory x7; cdl_page_directory_caps x7 (snd ptr) = Some cap\<rbrakk> \<Longrightarrow> modify (dupdate_cdl_object (fst ptr) (cdl_object.PageDirectory x7)) s = return () s
 6. \<And>x2 x10. \<lbrakk>cdl_objects s (fst ptr) = Some (IRQNode x10); x2 = IRQNode x10; cdl_irq_node_caps x10 (snd ptr) = Some cap\<rbrakk> \<Longrightarrow> modify (dupdate_cdl_object (fst ptr) (IRQNode x10)) s = return () s proof (prove)
goal:
No subgoals!