theory CSpaceInv_AI

lemma thread_set_mdb:
  assumes c: "\<And>t getF v. (getF, v) \<in> ran tcb_cap_cases
                    \<Longrightarrow> getF (f t) = getF t"
  shows "\<lbrace>valid_mdb\<rbrace> thread_set f p \<lbrace>\<lambda>r. valid_mdb\<rbrace>" apply (simp add: thread_set_def set_object_def get_object_def) apply (rule valid_mdb_lift) apply wp apply clarsimp apply (subst caps_of_state_after_update) apply (clarsimp simp: c) apply simp apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_mdb\<rbrace> thread_set f p \<lbrace>\<lambda>r. valid_mdb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_mdb\<rbrace> do tcb <- gets_the (get_tcb p);
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p = Some y);
return (the (kh p))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB (f tcb))\<rparr>)
od \<lbrace>\<lambda>r. valid_mdb\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> do tcb <- gets_the (get_tcb p);
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p = Some y);
return (the (kh p))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB (f tcb))\<rparr>)
od \<lbrace>\<lambda>r s. P (caps_of_state s)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> do tcb <- gets_the (get_tcb p);
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p = Some y);
return (the (kh p))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB (f tcb))\<rparr>)
od \<lbrace>\<lambda>r s. P (cdt s)\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>s. P (is_original_cap s)\<rbrace> do tcb <- gets_the (get_tcb p);
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p = Some y);
return (the (kh p))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB (f tcb))\<rparr>)
od \<lbrace>\<lambda>r s. P (is_original_cap s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>P s. P (caps_of_state s) \<Longrightarrow> get_tcb p s \<noteq> None \<longrightarrow> (\<exists>y. kheap s p = Some y) \<longrightarrow> a_type (the (kheap s p)) = ATCB \<longrightarrow> P (caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB (f (the (get_tcb p s))))\<rparr>))
 2. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> do tcb <- gets_the (get_tcb p);
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p = Some y);
return (the (kh p))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB (f tcb))\<rparr>)
od \<lbrace>\<lambda>r s. P (cdt s)\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>s. P (is_original_cap s)\<rbrace> do tcb <- gets_the (get_tcb p);
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p = Some y);
return (the (kh p))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB (f tcb))\<rparr>)
od \<lbrace>\<lambda>r s. P (is_original_cap s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>P s y tcb. \<lbrakk>P (caps_of_state s); get_tcb p s = Some y; kheap s p = Some (TCB tcb)\<rbrakk> \<Longrightarrow> P (caps_of_state (s\<lparr>kheap := \<lambda>a. if a = p then Some (TCB (f (the (get_tcb p s)))) else kheap s a\<rparr>))
 2. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> do tcb <- gets_the (get_tcb p);
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p = Some y);
return (the (kh p))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB (f tcb))\<rparr>)
od \<lbrace>\<lambda>r s. P (cdt s)\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>s. P (is_original_cap s)\<rbrace> do tcb <- gets_the (get_tcb p);
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p = Some y);
return (the (kh p))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB (f tcb))\<rparr>)
od \<lbrace>\<lambda>r s. P (is_original_cap s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>P s y tcb. \<lbrakk>P (caps_of_state s); get_tcb p s = Some y; kheap s p = Some (TCB tcb)\<rbrakk> \<Longrightarrow> obj_at (same_caps (TCB (f (the (get_tcb p s))))) p s
 2. \<And>P s y tcb. \<lbrakk>P (caps_of_state s); get_tcb p s = Some y; kheap s p = Some (TCB tcb)\<rbrakk> \<Longrightarrow> P (caps_of_state s)
 3. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> do tcb <- gets_the (get_tcb p);
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p = Some y);
return (the (kh p))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB (f tcb))\<rparr>)
od \<lbrace>\<lambda>r s. P (cdt s)\<rbrace>
 4. \<And>P. \<lbrace>\<lambda>s. P (is_original_cap s)\<rbrace> do tcb <- gets_the (get_tcb p);
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p = Some y);
return (the (kh p))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB (f tcb))\<rparr>)
od \<lbrace>\<lambda>r s. P (is_original_cap s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>P s y tcb. \<lbrakk>P (caps_of_state s); get_tcb p s = Some y; kheap s p = Some (TCB tcb)\<rbrakk> \<Longrightarrow> P (caps_of_state s)
 2. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> do tcb <- gets_the (get_tcb p);
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p = Some y);
return (the (kh p))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB (f tcb))\<rparr>)
od \<lbrace>\<lambda>r s. P (cdt s)\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>s. P (is_original_cap s)\<rbrace> do tcb <- gets_the (get_tcb p);
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p = Some y);
return (the (kh p))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB (f tcb))\<rparr>)
od \<lbrace>\<lambda>r s. P (is_original_cap s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> do tcb <- gets_the (get_tcb p);
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p = Some y);
return (the (kh p))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB (f tcb))\<rparr>)
od \<lbrace>\<lambda>r s. P (cdt s)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (is_original_cap s)\<rbrace> do tcb <- gets_the (get_tcb p);
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p = Some y);
return (the (kh p))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB (f tcb))\<rparr>)
od \<lbrace>\<lambda>r s. P (is_original_cap s)\<rbrace> proof (prove)
goal:
No subgoals!