theory Untyped_DR

lemma monad_commute_set_cap_cdt:
  "monad_commute \<top> (KHeap_D.set_cap ptr cap) (modify (\<lambda>s. s\<lparr>cdl_cdt := (cdl_cdt s)(ptr2 \<mapsto> ptr3)\<rparr>))" apply (clarsimp simp:monad_commute_def) apply (rule sym) apply (subst bind_assoc[symmetric]) apply (subst oblivious_modify_swap) apply (simp add: KHeap_D.set_cap_def split_def gets_the_def
     KHeap_D.set_object_def) apply (intro oblivious_bind oblivious_assert impI conjI allI oblivious_select |
          simp split: cdl_object.split)+ apply (clarsimp simp:bind_assoc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (\<lambda>_. True) (KHeap_D.set_cap ptr cap) (modify (\<lambda>s. s\<lparr>cdl_cdt := (cdl_cdt s)(ptr2 \<mapsto> ptr3)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s. (do x <- KHeap_D.set_cap ptr cap;
y <- modify (\<lambda>s. s\<lparr>cdl_cdt := (cdl_cdt s)(ptr2 \<mapsto> ptr3)\<rparr>);
return ((), ())
od) s = (do y <- modify (\<lambda>s. s\<lparr>cdl_cdt := (cdl_cdt s)(ptr2 \<mapsto> ptr3)\<rparr>);
x <- KHeap_D.set_cap ptr cap;
return ((), ())
od) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (do y <- modify (\<lambda>s. s\<lparr>cdl_cdt := (cdl_cdt s)(ptr2 \<mapsto> ptr3)\<rparr>);
x <- KHeap_D.set_cap ptr cap;
return ((), ())
od) s = (do x <- KHeap_D.set_cap ptr cap;
y <- modify (\<lambda>s. s\<lparr>cdl_cdt := (cdl_cdt s)(ptr2 \<mapsto> ptr3)\<rparr>);
return ((), ())
od) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (do x <- do y <- modify (\<lambda>s. s\<lparr>cdl_cdt := (cdl_cdt s)(ptr2 \<mapsto> ptr3)\<rparr>);
KHeap_D.set_cap ptr cap
od;
return ((), ())
od) s = (do x <- KHeap_D.set_cap ptr cap;
y <- modify (\<lambda>s. s\<lparr>cdl_cdt := (cdl_cdt s)(ptr2 \<mapsto> ptr3)\<rparr>);
return ((), ())
od) s proof (prove)
goal (2 subgoals):
 1. \<And>s. oblivious (\<lambda>s. s\<lparr>cdl_cdt := (cdl_cdt s)(ptr2 \<mapsto> ptr3)\<rparr>) (KHeap_D.set_cap ptr cap)
 2. \<And>s. (do x <- do rv <- KHeap_D.set_cap ptr cap;
modify (\<lambda>s. s\<lparr>cdl_cdt := (cdl_cdt s)(ptr2 \<mapsto> ptr3)\<rparr>)
od;
return ((), ())
od) s = (do x <- KHeap_D.set_cap ptr cap;
y <- modify (\<lambda>s. s\<lparr>cdl_cdt := (cdl_cdt s)(ptr2 \<mapsto> ptr3)\<rparr>);
return ((), ())
od) s proof (prove)
goal (2 subgoals):
 1. oblivious (\<lambda>s. s\<lparr>cdl_cdt := (cdl_cdt s)(ptr2 \<mapsto> ptr3)\<rparr>) (do obj <- gets (\<lambda>s. cdl_objects s (fst ptr)) >>= assert_opt;
y <- assert (has_slots obj);
obj'' <- case update_slots ((object_slots obj)(snd ptr \<mapsto> cap)) obj of Tcb t \<Rightarrow> if snd ptr = tcb_ipcbuffer_slot \<and> object_slots obj (snd ptr) \<noteq> Some cap then do intent' <- select UNIV;
return $ Tcb (dupdate_tcb_intent intent' t)
od else return (update_slots ((object_slots obj)(snd ptr \<mapsto> cap)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(snd ptr \<mapsto> cap)) obj);
modify (dupdate_cdl_object (fst ptr) obj'')
od)
 2. \<And>s. (do x <- do rv <- KHeap_D.set_cap ptr cap;
modify (\<lambda>s. s\<lparr>cdl_cdt := (cdl_cdt s)(ptr2 \<mapsto> ptr3)\<rparr>)
od;
return ((), ())
od) s = (do x <- KHeap_D.set_cap ptr cap;
y <- modify (\<lambda>s. s\<lparr>cdl_cdt := (cdl_cdt s)(ptr2 \<mapsto> ptr3)\<rparr>);
return ((), ())
od) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (do x <- do rv <- KHeap_D.set_cap ptr cap;
modify (\<lambda>s. s\<lparr>cdl_cdt := (cdl_cdt s)(ptr2 \<mapsto> ptr3)\<rparr>)
od;
return ((), ())
od) s = (do x <- KHeap_D.set_cap ptr cap;
y <- modify (\<lambda>s. s\<lparr>cdl_cdt := (cdl_cdt s)(ptr2 \<mapsto> ptr3)\<rparr>);
return ((), ())
od) s proof (prove)
goal:
No subgoals!