theory Tcb_DR

lemma thread_set_valid_irq_node:
  "(\<And>t getF v. (getF, v) \<in> ran tcb_cap_cases \<Longrightarrow> getF (f t) = getF t)
   \<Longrightarrow>
   \<lbrace>valid_irq_node\<rbrace> thread_set f p
   \<lbrace>\<lambda>rv s. valid_irq_node s\<rbrace>" apply (simp add: valid_irq_node_def thread_set_def) apply wp apply (simp add: KHeap_A.set_object_def get_object_def) apply wp+ apply (clarsimp simp: obj_at_def is_cap_table_def dest!: get_tcb_SomeD) apply (drule_tac x = irq in spec) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>t getF v. (getF, v) \<in> ran tcb_cap_cases \<Longrightarrow> getF (f t) = getF t) \<Longrightarrow> \<lbrace>valid_irq_node\<rbrace> thread_set f p \<lbrace>\<lambda>rv. valid_irq_node\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>t getF v. (getF, v) \<in> ran tcb_cap_cases \<Longrightarrow> getF (f t) = getF t) \<Longrightarrow> \<lbrace>\<lambda>s. inj (interrupt_irq_node s) \<and> (\<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s)\<rbrace> do tcb <- gets_the (get_tcb p);
KHeap_A.set_object p (TCB (f tcb))
od \<lbrace>\<lambda>rv s. inj (interrupt_irq_node s) \<and> (\<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>tcb. (\<And>t getF v. (getF, v) \<in> ran tcb_cap_cases \<Longrightarrow> getF (f t) = getF t) \<Longrightarrow> \<lbrace>?P'2 tcb\<rbrace> KHeap_A.set_object p (TCB (f tcb)) \<lbrace>\<lambda>rv s. \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s\<rbrace>
 2. (\<And>t getF v. (getF, v) \<in> ran tcb_cap_cases \<Longrightarrow> getF (f t) = getF t) \<Longrightarrow> \<lbrace>?Q\<rbrace> gets_the (get_tcb p) \<lbrace>\<lambda>tcb s. inj (interrupt_irq_node s) \<and> ?P'2 tcb s\<rbrace>
 3. \<And>s. \<lbrakk>\<And>t getF v. (getF, v) \<in> ran tcb_cap_cases \<Longrightarrow> getF (f t) = getF t; inj (interrupt_irq_node s) \<and> (\<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s)\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>tcb. (\<And>t getF v. (getF, v) \<in> ran tcb_cap_cases \<Longrightarrow> getF (f t) = getF t) \<Longrightarrow> \<lbrace>?P'2 tcb\<rbrace> do 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 (update_kheap ((kheap s)(p \<mapsto> TCB (f tcb))) s)
od \<lbrace>\<lambda>rv s. \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s\<rbrace>
 2. (\<And>t getF v. (getF, v) \<in> ran tcb_cap_cases \<Longrightarrow> getF (f t) = getF t) \<Longrightarrow> \<lbrace>?Q\<rbrace> gets_the (get_tcb p) \<lbrace>\<lambda>tcb s. inj (interrupt_irq_node s) \<and> ?P'2 tcb s\<rbrace>
 3. \<And>s. \<lbrakk>\<And>t getF v. (getF, v) \<in> ran tcb_cap_cases \<Longrightarrow> getF (f t) = getF t; inj (interrupt_irq_node s) \<and> (\<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s)\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>t getF v. (getF, v) \<in> ran tcb_cap_cases \<Longrightarrow> getF (f t) = getF t; inj (interrupt_irq_node s) \<and> (\<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s)\<rbrakk> \<Longrightarrow> get_tcb p s \<noteq> None \<longrightarrow> inj (interrupt_irq_node s) \<and> ((\<exists>y. kheap s p = Some y) \<longrightarrow> a_type (the (kheap s p)) = ATCB \<longrightarrow> (\<forall>irq. cap_table_at 0 (interrupt_irq_node (update_kheap ((kheap s)(p \<mapsto> TCB (f (the (get_tcb p s))))) s) irq) (update_kheap ((kheap s)(p \<mapsto> TCB (f (the (get_tcb p s))))) s))) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb irq. \<lbrakk>\<And>t getF a b. (getF, a, b) \<in> ran tcb_cap_cases \<Longrightarrow> getF (f t) = getF t; inj (interrupt_irq_node s); \<forall>irq. \<exists>ko. kheap s (interrupt_irq_node s irq) = Some ko \<and> (case ko of kernel_object.CNode sz cs \<Rightarrow> 0 = sz \<and> well_formed_cnode_n 0 cs | _ \<Rightarrow> False); kheap s (interrupt_irq_node s irq) = Some (TCB tcb); p = interrupt_irq_node s irq\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s tcb irq. \<lbrakk>\<And>t getF a b. (getF, a, b) \<in> ran tcb_cap_cases \<Longrightarrow> getF (f t) = getF t; inj (interrupt_irq_node s); kheap s (interrupt_irq_node s irq) = Some (TCB tcb); p = interrupt_irq_node s irq; \<exists>ko. kheap s (interrupt_irq_node s irq) = Some ko \<and> (case ko of kernel_object.CNode sz cs \<Rightarrow> 0 = sz \<and> well_formed_cnode_n 0 cs | _ \<Rightarrow> False)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!