theory CNode_IF

lemma lookup_slot_for_thread_rev:
  "reads_equiv_valid_inv A aag (pas_refined aag and K (is_subject aag thread))
                         (lookup_slot_for_thread thread cptr)" unfolding lookup_slot_for_thread_def fun_app_def apply (rule gen_asm_ev) apply (wp resolve_address_bits_rev gets_the_ev | simp)+ apply (rule conjI) apply blast apply (clarsimp simp: tcb.splits) apply (erule (2) owns_thread_owns_cspace) defer apply (case_tac tcb_ctablea, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (pas_refined aag and K (is_subject aag thread)) (lookup_slot_for_thread thread cptr) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (pas_refined aag and K (is_subject aag thread)) (doE tcb <- liftE (gets_the (get_tcb thread));
resolve_address_bits (tcb_ctable tcb, cptr)
odE) proof (prove)
goal (1 subgoal):
 1. is_subject aag thread \<Longrightarrow> reads_equiv_valid_inv A aag (pas_refined aag) (doE tcb <- liftE (gets_the (get_tcb thread));
resolve_address_bits (tcb_ctable tcb, cptr)
odE) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag thread; pas_refined aag s\<rbrakk> \<Longrightarrow> (\<forall>s t. reads_equiv aag s t \<and> A s t \<longrightarrow> get_tcb thread s = get_tcb thread t) \<and> ((\<exists>y. get_tcb thread s = Some y) \<longrightarrow> is_cnode_cap (tcb_ctable (the (get_tcb thread s))) \<longrightarrow> is_subject aag (obj_ref_of (tcb_ctable (the (get_tcb thread s))))) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_subject aag thread; pas_refined aag s\<rbrakk> \<Longrightarrow> \<forall>s t. reads_equiv aag s t \<and> A s t \<longrightarrow> get_tcb thread s = get_tcb thread t
 2. \<And>s. \<lbrakk>is_subject aag thread; pas_refined aag s\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb thread s = Some y) \<longrightarrow> is_cnode_cap (tcb_ctable (the (get_tcb thread s))) \<longrightarrow> is_subject aag (obj_ref_of (tcb_ctable (the (get_tcb thread s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag thread; pas_refined aag s\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb thread s = Some y) \<longrightarrow> is_cnode_cap (tcb_ctable (the (get_tcb thread s))) \<longrightarrow> is_subject aag (obj_ref_of (tcb_ctable (the (get_tcb thread s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb_ctable tcb_vtable tcb_reply tcb_caller tcb_ipcframe tcb_state tcb_fault_handler tcb_ipc_buffer tcb_fault tcb_bound_notification tcb_mcpriority tcb_arch. \<lbrakk>is_subject aag thread; pas_refined aag s; get_tcb thread s = Some \<lparr>tcb_ctable = tcb_ctable, tcb_vtable = tcb_vtable, tcb_reply = tcb_reply, tcb_caller = tcb_caller, tcb_ipcframe = tcb_ipcframe, tcb_state = tcb_state, tcb_fault_handler = tcb_fault_handler, tcb_ipc_buffer = tcb_ipc_buffer, tcb_fault = tcb_fault, tcb_bound_notification = tcb_bound_notification, tcb_mcpriority = tcb_mcpriority, tcb_arch = tcb_arch\<rparr>; is_cnode_cap tcb_ctable\<rbrakk> \<Longrightarrow> is_subject aag (obj_ref_of tcb_ctable) proof (prove)
goal (2 subgoals):
 1. \<And>s tcb_ctablea tcb_vtable tcb_reply tcb_caller tcb_ipcframe tcb_state tcb_fault_handler tcb_ipc_buffer tcb_fault tcb_bound_notification tcb_mcpriority tcb_arch. \<lbrakk>pas_refined aag s; get_tcb thread s = Some \<lparr>tcb_ctable = tcb_ctablea, tcb_vtable = tcb_vtable, tcb_reply = tcb_reply, tcb_caller = tcb_caller, tcb_ipcframe = tcb_ipcframe, tcb_state = tcb_state, tcb_fault_handler = tcb_fault_handler, tcb_ipc_buffer = tcb_ipc_buffer, tcb_fault = tcb_fault, tcb_bound_notification = tcb_bound_notification, tcb_mcpriority = tcb_mcpriority, tcb_arch = tcb_arch\<rparr>; is_cnode_cap tcb_ctablea\<rbrakk> \<Longrightarrow> is_cnode_cap (tcb_ctable \<lparr>tcb_ctable = tcb_ctablea, tcb_vtable = tcb_vtable, tcb_reply = tcb_reply, tcb_caller = tcb_caller, tcb_ipcframe = tcb_ipcframe, tcb_state = tcb_state, tcb_fault_handler = tcb_fault_handler, tcb_ipc_buffer = tcb_ipc_buffer, tcb_fault = tcb_fault, tcb_bound_notification = tcb_bound_notification, tcb_mcpriority = tcb_mcpriority, tcb_arch = tcb_arch\<rparr>)
 2. \<And>s tcb_ctablea tcb_vtable tcb_reply tcb_caller tcb_ipcframe tcb_state tcb_fault_handler tcb_ipc_buffer tcb_fault tcb_bound_notification tcb_mcpriority tcb_arch. \<lbrakk>pas_refined aag s; get_tcb thread s = Some \<lparr>tcb_ctable = tcb_ctablea, tcb_vtable = tcb_vtable, tcb_reply = tcb_reply, tcb_caller = tcb_caller, tcb_ipcframe = tcb_ipcframe, tcb_state = tcb_state, tcb_fault_handler = tcb_fault_handler, tcb_ipc_buffer = tcb_ipc_buffer, tcb_fault = tcb_fault, tcb_bound_notification = tcb_bound_notification, tcb_mcpriority = tcb_mcpriority, tcb_arch = tcb_arch\<rparr>; is_cnode_cap tcb_ctablea\<rbrakk> \<Longrightarrow> obj_ref_of tcb_ctablea \<in> obj_refs_ac (tcb_ctable \<lparr>tcb_ctable = tcb_ctablea, tcb_vtable = tcb_vtable, tcb_reply = tcb_reply, tcb_caller = tcb_caller, tcb_ipcframe = tcb_ipcframe, tcb_state = tcb_state, tcb_fault_handler = tcb_fault_handler, tcb_ipc_buffer = tcb_ipc_buffer, tcb_fault = tcb_fault, tcb_bound_notification = tcb_bound_notification, tcb_mcpriority = tcb_mcpriority, tcb_arch = tcb_arch\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s tcb_ctablea tcb_vtable tcb_reply tcb_caller tcb_ipcframe tcb_state tcb_fault_handler tcb_ipc_buffer tcb_fault tcb_bound_notification tcb_mcpriority tcb_arch. \<lbrakk>pas_refined aag s; get_tcb thread s = Some \<lparr>tcb_ctable = tcb_ctablea, tcb_vtable = tcb_vtable, tcb_reply = tcb_reply, tcb_caller = tcb_caller, tcb_ipcframe = tcb_ipcframe, tcb_state = tcb_state, tcb_fault_handler = tcb_fault_handler, tcb_ipc_buffer = tcb_ipc_buffer, tcb_fault = tcb_fault, tcb_bound_notification = tcb_bound_notification, tcb_mcpriority = tcb_mcpriority, tcb_arch = tcb_arch\<rparr>; is_cnode_cap tcb_ctablea\<rbrakk> \<Longrightarrow> obj_ref_of tcb_ctablea \<in> obj_refs_ac (tcb_ctable \<lparr>tcb_ctable = tcb_ctablea, tcb_vtable = tcb_vtable, tcb_reply = tcb_reply, tcb_caller = tcb_caller, tcb_ipcframe = tcb_ipcframe, tcb_state = tcb_state, tcb_fault_handler = tcb_fault_handler, tcb_ipc_buffer = tcb_ipc_buffer, tcb_fault = tcb_fault, tcb_bound_notification = tcb_bound_notification, tcb_mcpriority = tcb_mcpriority, tcb_arch = tcb_arch\<rparr>)
 2. \<And>s tcb_ctablea tcb_vtable tcb_reply tcb_caller tcb_ipcframe tcb_state tcb_fault_handler tcb_ipc_buffer tcb_fault tcb_bound_notification tcb_mcpriority tcb_arch. \<lbrakk>pas_refined aag s; get_tcb thread s = Some \<lparr>tcb_ctable = tcb_ctablea, tcb_vtable = tcb_vtable, tcb_reply = tcb_reply, tcb_caller = tcb_caller, tcb_ipcframe = tcb_ipcframe, tcb_state = tcb_state, tcb_fault_handler = tcb_fault_handler, tcb_ipc_buffer = tcb_ipc_buffer, tcb_fault = tcb_fault, tcb_bound_notification = tcb_bound_notification, tcb_mcpriority = tcb_mcpriority, tcb_arch = tcb_arch\<rparr>; is_cnode_cap tcb_ctablea\<rbrakk> \<Longrightarrow> is_cnode_cap (tcb_ctable \<lparr>tcb_ctable = tcb_ctablea, tcb_vtable = tcb_vtable, tcb_reply = tcb_reply, tcb_caller = tcb_caller, tcb_ipcframe = tcb_ipcframe, tcb_state = tcb_state, tcb_fault_handler = tcb_fault_handler, tcb_ipc_buffer = tcb_ipc_buffer, tcb_fault = tcb_fault, tcb_bound_notification = tcb_bound_notification, tcb_mcpriority = tcb_mcpriority, tcb_arch = tcb_arch\<rparr>) proof (prove)
goal:
No subgoals!