theory Syscall_DR

lemma get_ipc_buffer_noop:
  "\<lbrace>P and (\<lambda>s. \<exists>s'. s = transform s' \<and> tcb_at t s' \<and> valid_etcbs s' \<and> not_idle_thread t s')\<rbrace>
     get_ipc_buffer t True \<exists>\<lbrace>\<lambda>r. P\<rbrace>" apply (simp add:gets_the_def gets_def bind_assoc get_def split_def get_ipc_buffer_def tcb_at_def
      exs_valid_def fail_def return_def bind_def assert_opt_def split:cdl_cap.splits) apply clarsimp apply (rule_tac x = "(the (opt_cap (t, tcb_ipcbuffer_slot) s),s)" for s in bexI) apply (rule conjI|fastforce simp:fail_def return_def split:option.splits)+ apply (clarsimp split:option.splits simp:fail_def return_def) apply (frule(1) valid_etcbs_get_tcb_get_etcb) apply (clarsimp simp: opt_cap_tcb not_idle_thread_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and (\<lambda>s. \<exists>s'. s = transform s' \<and> tcb_at t s' \<and> valid_etcbs s' \<and> not_idle_thread t s')\<rbrace> get_ipc_buffer t True \<exists>\<lbrace>\<lambda>r. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>s. P s \<and> (\<exists>s'. s = transform s' \<and> (\<exists>tcb. get_tcb t s' = Some tcb) \<and> valid_etcbs s' \<and> not_idle_thread t s') \<longrightarrow> (\<exists>y\<in>fst ((case opt_cap (t, tcb_ipcbuffer_slot) s of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). (fst y = cdl_cap.NullCap \<longrightarrow> P (snd y)) \<and> ((\<exists>x21 x22 x23. fst y = cdl_cap.UntypedCap x21 x22 x23) \<longrightarrow> P (snd y)) \<and> ((\<exists>x31 x32 x33. fst y = cdl_cap.EndpointCap x31 x32 x33) \<longrightarrow> P (snd y)) \<and> ((\<exists>x41 x42 x43. fst y = cdl_cap.NotificationCap x41 x42 x43) \<longrightarrow> P (snd y)) \<and> ((\<exists>x51 x52. fst y = cdl_cap.ReplyCap x51 x52) \<longrightarrow> P (snd y)) \<and> ((\<exists>x6. fst y = MasterReplyCap x6) \<longrightarrow> P (snd y)) \<and> ((\<exists>x71 x72 x73 x74. fst y = cdl_cap.CNodeCap x71 x72 x73 x74) \<longrightarrow> P (snd y)) \<and> ((\<exists>x8. fst y = TcbCap x8) \<longrightarrow> P (snd y)) \<and> (fst y = cdl_cap.DomainCap \<longrightarrow> P (snd y)) \<and> ((\<exists>x101 x102 x103 x104 x105 x106. fst y = PendingSyncSendCap x101 x102 x103 x104 x105 x106) \<longrightarrow> P (snd y)) \<and> ((\<exists>x111 x112 x113. fst y = PendingSyncRecvCap x111 x112 x113) \<longrightarrow> P (snd y)) \<and> ((\<exists>x12. fst y = PendingNtfnRecvCap x12) \<longrightarrow> P (snd y)) \<and> (fst y = RestartCap \<longrightarrow> P (snd y)) \<and> (fst y = RunningCap \<longrightarrow> P (snd y)) \<and> (fst y = IrqControlCap \<longrightarrow> P (snd y)) \<and> ((\<exists>x16. fst y = IrqHandlerCap x16) \<longrightarrow> P (snd y)) \<and> (\<forall>x171 x172 x173. (AllowWrite \<in> x173 \<and> AllowRead \<in> x173 \<longrightarrow> (\<exists>x174 x175 x176. fst y = FrameCap x171 x172 x173 x174 x175 x176) \<longrightarrow> P (snd y)) \<and> ((AllowWrite \<in> x173 \<longrightarrow> AllowRead \<notin> x173) \<longrightarrow> (\<exists>x174 x175 x176. fst y = FrameCap x171 x172 x173 x174 x175 x176) \<longrightarrow> P (snd y))) \<and> ((\<exists>x181 x182 x183. fst y = cdl_cap.PageTableCap x181 x182 x183) \<longrightarrow> P (snd y)) \<and> ((\<exists>x191 x192 x193. fst y = cdl_cap.PageDirectoryCap x191 x192 x193) \<longrightarrow> P (snd y)) \<and> (fst y = AsidControlCap \<longrightarrow> P (snd y)) \<and> ((\<exists>x211 x212. fst y = AsidPoolCap x211 x212) \<longrightarrow> P (snd y)) \<and> ((\<exists>x221 x222. fst y = IOPortsCap x221 x222) \<longrightarrow> P (snd y)) \<and> (fst y = IOSpaceMasterCap \<longrightarrow> P (snd y)) \<and> ((\<exists>x24. fst y = IOSpaceCap x24) \<longrightarrow> P (snd y)) \<and> ((\<exists>x25. fst y = IOPageTableCap x25) \<longrightarrow> P (snd y)) \<and> ((\<exists>x26. fst y = ZombieCap x26) \<longrightarrow> P (snd y)) \<and> ((\<exists>x27. fst y = BoundNotificationCap x27) \<longrightarrow> P (snd y))) proof (prove)
goal (1 subgoal):
 1. \<And>s' tcb. \<lbrakk>P (transform s'); get_tcb t s' = Some tcb; valid_etcbs s'; not_idle_thread t s'\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst ((case opt_cap (t, tcb_ipcbuffer_slot) (transform s') of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (transform s')). (fst y = cdl_cap.NullCap \<longrightarrow> P (snd y)) \<and> ((\<exists>x21 x22 x23. fst y = cdl_cap.UntypedCap x21 x22 x23) \<longrightarrow> P (snd y)) \<and> ((\<exists>x31 x32 x33. fst y = cdl_cap.EndpointCap x31 x32 x33) \<longrightarrow> P (snd y)) \<and> ((\<exists>x41 x42 x43. fst y = cdl_cap.NotificationCap x41 x42 x43) \<longrightarrow> P (snd y)) \<and> ((\<exists>x51 x52. fst y = cdl_cap.ReplyCap x51 x52) \<longrightarrow> P (snd y)) \<and> ((\<exists>x6. fst y = MasterReplyCap x6) \<longrightarrow> P (snd y)) \<and> ((\<exists>x71 x72 x73 x74. fst y = cdl_cap.CNodeCap x71 x72 x73 x74) \<longrightarrow> P (snd y)) \<and> ((\<exists>x8. fst y = TcbCap x8) \<longrightarrow> P (snd y)) \<and> (fst y = cdl_cap.DomainCap \<longrightarrow> P (snd y)) \<and> ((\<exists>x101 x102 x103 x104 x105 x106. fst y = PendingSyncSendCap x101 x102 x103 x104 x105 x106) \<longrightarrow> P (snd y)) \<and> ((\<exists>x111 x112 x113. fst y = PendingSyncRecvCap x111 x112 x113) \<longrightarrow> P (snd y)) \<and> ((\<exists>x12. fst y = PendingNtfnRecvCap x12) \<longrightarrow> P (snd y)) \<and> (fst y = RestartCap \<longrightarrow> P (snd y)) \<and> (fst y = RunningCap \<longrightarrow> P (snd y)) \<and> (fst y = IrqControlCap \<longrightarrow> P (snd y)) \<and> ((\<exists>x16. fst y = IrqHandlerCap x16) \<longrightarrow> P (snd y)) \<and> (\<forall>x171 x172 x173. (AllowWrite \<in> x173 \<and> AllowRead \<in> x173 \<longrightarrow> (\<exists>x174 x175 x176. fst y = FrameCap x171 x172 x173 x174 x175 x176) \<longrightarrow> P (snd y)) \<and> ((AllowWrite \<in> x173 \<longrightarrow> AllowRead \<notin> x173) \<longrightarrow> (\<exists>x174 x175 x176. fst y = FrameCap x171 x172 x173 x174 x175 x176) \<longrightarrow> P (snd y))) \<and> ((\<exists>x181 x182 x183. fst y = cdl_cap.PageTableCap x181 x182 x183) \<longrightarrow> P (snd y)) \<and> ((\<exists>x191 x192 x193. fst y = cdl_cap.PageDirectoryCap x191 x192 x193) \<longrightarrow> P (snd y)) \<and> (fst y = AsidControlCap \<longrightarrow> P (snd y)) \<and> ((\<exists>x211 x212. fst y = AsidPoolCap x211 x212) \<longrightarrow> P (snd y)) \<and> ((\<exists>x221 x222. fst y = IOPortsCap x221 x222) \<longrightarrow> P (snd y)) \<and> (fst y = IOSpaceMasterCap \<longrightarrow> P (snd y)) \<and> ((\<exists>x24. fst y = IOSpaceCap x24) \<longrightarrow> P (snd y)) \<and> ((\<exists>x25. fst y = IOPageTableCap x25) \<longrightarrow> P (snd y)) \<and> ((\<exists>x26. fst y = ZombieCap x26) \<longrightarrow> P (snd y)) \<and> ((\<exists>x27. fst y = BoundNotificationCap x27) \<longrightarrow> P (snd y)) proof (prove)
goal (2 subgoals):
 1. \<And>s' tcb. \<lbrakk>P (transform s'); get_tcb t s' = Some tcb; valid_etcbs s'; not_idle_thread t s'\<rbrakk> \<Longrightarrow> (fst (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb) = cdl_cap.NullCap \<longrightarrow> P (snd (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb))) \<and> ((\<exists>x21 x22 x23. fst (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb) = cdl_cap.UntypedCap x21 x22 x23) \<longrightarrow> P (snd (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb))) \<and> ((\<exists>x31 x32 x33. fst (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb) = cdl_cap.EndpointCap x31 x32 x33) \<longrightarrow> P (snd (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb))) \<and> ((\<exists>x41 x42 x43. fst (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb) = cdl_cap.NotificationCap x41 x42 x43) \<longrightarrow> P (snd (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb))) \<and> ((\<exists>x51 x52. fst (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb) = cdl_cap.ReplyCap x51 x52) \<longrightarrow> P (snd (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb))) \<and> ((\<exists>x6. fst (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb) = MasterReplyCap x6) \<longrightarrow> P (snd (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb))) \<and> ((\<exists>x71 x72 x73 x74. fst (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb) = cdl_cap.CNodeCap x71 x72 x73 x74) \<longrightarrow> P (snd (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb))) \<and> ((\<exists>x8. fst (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb) = TcbCap x8) \<longrightarrow> P (snd (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb))) \<and> (fst (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb) = cdl_cap.DomainCap \<longrightarrow> P (snd (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb))) \<and> ((\<exists>x101 x102 x103 x104 x105 x106. fst (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb) = PendingSyncSendCap x101 x102 x103 x104 x105 x106) \<longrightarrow> P (snd (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb))) \<and> ((\<exists>x111 x112 x113. fst (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb) = PendingSyncRecvCap x111 x112 x113) \<longrightarrow> P (snd (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb))) \<and> ((\<exists>x12. fst (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb) = PendingNtfnRecvCap x12) \<longrightarrow> P (snd (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb))) \<and> (fst (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb) = RestartCap \<longrightarrow> P (snd (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb))) \<and> (fst (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb) = RunningCap \<longrightarrow> P (snd (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb))) \<and> (fst (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb) = IrqControlCap \<longrightarrow> P (snd (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb))) \<and> ((\<exists>x16. fst (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb) = IrqHandlerCap x16) \<longrightarrow> P (snd (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb))) \<and> (\<forall>x171 x172 x173. (AllowWrite \<in> x173 \<and> AllowRead \<in> x173 \<longrightarrow> (\<exists>x174 x175 x176. fst (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb) = FrameCap x171 x172 x173 x174 x175 x176) \<longrightarrow> P (snd (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb))) \<and> ((AllowWrite \<in> x173 \<longrightarrow> AllowRead \<notin> x173) \<longrightarrow> (\<exists>x174 x175 x176. fst (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb) = FrameCap x171 x172 x173 x174 x175 x176) \<longrightarrow> P (snd (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb)))) \<and> ((\<exists>x181 x182 x183. fst (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb) = cdl_cap.PageTableCap x181 x182 x183) \<longrightarrow> P (snd (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb))) \<and> ((\<exists>x191 x192 x193. fst (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb) = cdl_cap.PageDirectoryCap x191 x192 x193) \<longrightarrow> P (snd (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb))) \<and> (fst (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb) = AsidControlCap \<longrightarrow> P (snd (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb))) \<and> ((\<exists>x211 x212. fst (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb) = AsidPoolCap x211 x212) \<longrightarrow> P (snd (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb))) \<and> ((\<exists>x221 x222. fst (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb) = IOPortsCap x221 x222) \<longrightarrow> P (snd (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb))) \<and> (fst (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb) = IOSpaceMasterCap \<longrightarrow> P (snd (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb))) \<and> ((\<exists>x24. fst (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb) = IOSpaceCap x24) \<longrightarrow> P (snd (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb))) \<and> ((\<exists>x25. fst (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb) = IOPageTableCap x25) \<longrightarrow> P (snd (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb))) \<and> ((\<exists>x26. fst (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb) = ZombieCap x26) \<longrightarrow> P (snd (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb))) \<and> ((\<exists>x27. fst (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb) = BoundNotificationCap x27) \<longrightarrow> P (snd (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb)))
 2. \<And>s' tcb. \<lbrakk>P (transform s'); get_tcb t s' = Some tcb; valid_etcbs s'; not_idle_thread t s'\<rbrakk> \<Longrightarrow> (the (opt_cap (t, tcb_ipcbuffer_slot) (?s68 s' tcb)), ?s68 s' tcb) \<in> fst ((case opt_cap (t, tcb_ipcbuffer_slot) (transform s') of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (transform s')) proof (prove)
goal (1 subgoal):
 1. \<And>s' tcb. \<lbrakk>P (transform s'); get_tcb t s' = Some tcb; valid_etcbs s'; not_idle_thread t s'\<rbrakk> \<Longrightarrow> (the (opt_cap (t, tcb_ipcbuffer_slot) (transform s')), transform s') \<in> fst ((case opt_cap (t, tcb_ipcbuffer_slot) (transform s') of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (transform s')) proof (prove)
goal (1 subgoal):
 1. \<And>s' tcb. \<lbrakk>P (transform s'); get_tcb t s' = Some tcb; valid_etcbs s'; not_idle_thread t s'\<rbrakk> \<Longrightarrow> \<exists>y. opt_cap (t, tcb_ipcbuffer_slot) (transform s') = Some y proof (prove)
goal (1 subgoal):
 1. \<And>s' tcb. \<lbrakk>P (transform s'); get_tcb t s' = Some tcb; valid_etcbs s'; not_idle_thread t s'; \<exists>etcb. get_etcb t s' = Some etcb\<rbrakk> \<Longrightarrow> \<exists>y. opt_cap (t, tcb_ipcbuffer_slot) (transform s') = Some y proof (prove)
goal:
No subgoals!