theory Syscall_AI

lemma lsft_ex_cte_cap_to:
  "\<lbrace>invs and K (\<forall>cap. is_cnode_cap cap \<longrightarrow> P cap)\<rbrace>
     lookup_slot_for_thread t cref
   \<lbrace>\<lambda>rv s. ex_cte_cap_wp_to P (fst rv) s\<rbrace>,-" apply (simp add: lookup_slot_for_thread_def) apply (wp rab_cte_cap_to) apply (clarsimp simp: ex_cte_cap_wp_to_def) apply (clarsimp dest!: get_tcb_SomeD) apply (frule cte_wp_at_tcbI[where t="(t', tcb_cnode_index 0)" and P="(=) v" for t' v, simplified]) apply fastforce apply fastforce apply (intro exI, erule cte_wp_at_weakenE) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and K (\<forall>cap. is_cnode_cap cap \<longrightarrow> P cap)\<rbrace> lookup_slot_for_thread t cref \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>y. \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap)\<rbrace> doE tcb <- liftE (gets_the (get_tcb t));
resolve_address_bits (tcb_ctable tcb, cref)
odE \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (fst rv)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs and (\<lambda>y. \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap)) s \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> (is_cnode_cap (fst (tcb_ctable (the (get_tcb t s)), cref)) \<longrightarrow> (\<forall>r\<in>cte_refs (fst (tcb_ctable (the (get_tcb t s)), cref)) (interrupt_irq_node s). ex_cte_cap_wp_to P r s)) \<and> (\<forall>cap. is_cnode_cap cap \<longrightarrow> P cap) proof (prove)
goal (1 subgoal):
 1. \<And>s y a b. \<lbrakk>invs s; \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap; get_tcb t s = Some y; is_cnode_cap (tcb_ctable y); (a, b) \<in> cte_refs (tcb_ctable y) (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> \<exists>aa ba. cte_wp_at (\<lambda>c. P c \<and> (a, b) \<in> cte_refs c (interrupt_irq_node s)) (aa, ba) s proof (prove)
goal (1 subgoal):
 1. \<And>s y a b. \<lbrakk>invs s; \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap; is_cnode_cap (tcb_ctable y); (a, b) \<in> cte_refs (tcb_ctable y) (interrupt_irq_node s); kheap s t = Some (TCB y)\<rbrakk> \<Longrightarrow> \<exists>aa ba. cte_wp_at (\<lambda>c. P c \<and> (a, b) \<in> cte_refs c (interrupt_irq_node s)) (aa, ba) s proof (prove)
goal (3 subgoals):
 1. \<And>s y a b. \<lbrakk>invs s; \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap; is_cnode_cap (tcb_ctable y); (a, b) \<in> cte_refs (tcb_ctable y) (interrupt_irq_node s); kheap s t = Some (TCB y)\<rbrakk> \<Longrightarrow> tcb_ctable = ?getF16 s y a b \<and> (tcb_ctable_update, \<lambda>_ _ _. True) = ?setF16 s y a b
 2. \<And>s y a b. \<lbrakk>invs s; \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap; is_cnode_cap (tcb_ctable y); (a, b) \<in> cte_refs (tcb_ctable y) (interrupt_irq_node s); kheap s t = Some (TCB y)\<rbrakk> \<Longrightarrow> ?v16 s y a b = ?getF16 s y a b y
 3. \<And>s y a b. \<lbrakk>invs s; \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap; is_cnode_cap (tcb_ctable y); (a, b) \<in> cte_refs (tcb_ctable y) (interrupt_irq_node s); kheap s t = Some (TCB y); cte_wp_at ((=) (?v16 s y a b)) (t, tcb_cnode_index 0) s\<rbrakk> \<Longrightarrow> \<exists>aa ba. cte_wp_at (\<lambda>c. P c \<and> (a, b) \<in> cte_refs c (interrupt_irq_node s)) (aa, ba) s proof (prove)
goal (2 subgoals):
 1. \<And>s y a b. \<lbrakk>invs s; \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap; is_cnode_cap (tcb_ctable y); (a, b) \<in> cte_refs (tcb_ctable y) (interrupt_irq_node s); kheap s t = Some (TCB y)\<rbrakk> \<Longrightarrow> ?v16 s y a b = tcb_ctable y
 2. \<And>s y a b. \<lbrakk>invs s; \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap; is_cnode_cap (tcb_ctable y); (a, b) \<in> cte_refs (tcb_ctable y) (interrupt_irq_node s); kheap s t = Some (TCB y); cte_wp_at ((=) (?v16 s y a b)) (t, tcb_cnode_index 0) s\<rbrakk> \<Longrightarrow> \<exists>aa ba. cte_wp_at (\<lambda>c. P c \<and> (a, b) \<in> cte_refs c (interrupt_irq_node s)) (aa, ba) s proof (prove)
goal (1 subgoal):
 1. \<And>s y a b. \<lbrakk>invs s; \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap; is_cnode_cap (tcb_ctable y); (a, b) \<in> cte_refs (tcb_ctable y) (interrupt_irq_node s); kheap s t = Some (TCB y); cte_wp_at ((=) (tcb_ctable y)) (t, tcb_cnode_index 0) s\<rbrakk> \<Longrightarrow> \<exists>aa ba. cte_wp_at (\<lambda>c. P c \<and> (a, b) \<in> cte_refs c (interrupt_irq_node s)) (aa, ba) s proof (prove)
goal (1 subgoal):
 1. \<And>s y a b c. \<lbrakk>invs s; \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap; is_cnode_cap (tcb_ctable y); (a, b) \<in> cte_refs (tcb_ctable y) (interrupt_irq_node s); kheap s t = Some (TCB y); tcb_ctable y = c\<rbrakk> \<Longrightarrow> P c \<and> (a, b) \<in> cte_refs c (interrupt_irq_node s) proof (prove)
goal:
No subgoals!