theory Syscall_AI

lemma handle_reply_nonz_cap:
  "\<lbrace>\<lambda>s :: 'state_ext state. ex_nonz_cap_to p s \<and> valid_objs s \<and> valid_mdb s \<and> tcb_at p s\<rbrace>
     handle_reply
   \<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace>" apply (simp add: handle_reply_def) apply (wp delete_caller_cap_nonz_cap do_reply_transfer_nonz_cap | wpc)+ apply (wp get_cap_wp)+ apply clarsimp apply (drule(1) cte_wp_valid_cap) apply (clarsimp simp: valid_cap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ex_nonz_cap_to p s \<and> valid_objs s \<and> valid_mdb s \<and> tcb_at p s\<rbrace> handle_reply \<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ex_nonz_cap_to p s \<and> valid_objs s \<and> valid_mdb s \<and> tcb_at p s\<rbrace> do thread <- gets cur_thread;
caller_cap <- get_cap (thread, tcb_cnode_index 3);
case caller_cap of NullCap \<Rightarrow> return () | ReplyCap caller True R \<Rightarrow> fail | ReplyCap caller False R \<Rightarrow> do_reply_transfer thread caller (thread, tcb_cnode_index 3) (AllowGrant \<in> R) | _ \<Rightarrow> fail
od \<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>thread. \<lbrace>?B1 thread\<rbrace> get_cap (thread, tcb_cnode_index 3) \<lbrace>\<lambda>caller_cap s. (caller_cap = NullCap \<longrightarrow> ex_nonz_cap_to p s) \<and> (\<forall>x xa xb xc. caller_cap = UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb. caller_cap = EndpointCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. caller_cap = NotificationCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. caller_cap = ReplyCap x xa xb \<longrightarrow> (xa = True \<longrightarrow> True) \<and> (xa = False \<longrightarrow> ex_nonz_cap_to p s \<and> valid_objs s \<and> tcb_at p s \<and> valid_mdb s \<and> tcb_at x s)) \<and> (\<forall>x xa xb. caller_cap = CNodeCap x xa xb \<longrightarrow> True) \<and> (\<forall>x. caller_cap = ThreadCap x \<longrightarrow> True) \<and> (caller_cap = DomainCap \<longrightarrow> True) \<and> (caller_cap = IRQControlCap \<longrightarrow> True) \<and> (\<forall>x. caller_cap = IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. caller_cap = Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. caller_cap = ArchObjectCap x \<longrightarrow> True)\<rbrace>
 2. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?B1\<rbrace>
 3. \<And>s. ex_nonz_cap_to p s \<and> valid_objs s \<and> valid_mdb s \<and> tcb_at p s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. ex_nonz_cap_to p s \<and> valid_objs s \<and> valid_mdb s \<and> tcb_at p s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) (cur_thread s, tcb_cnode_index 3) s \<longrightarrow> (cap = NullCap \<longrightarrow> ex_nonz_cap_to p s) \<and> (\<forall>x xa xb xc. cap = UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = ReplyCap x xa xb \<longrightarrow> (xa = True \<longrightarrow> True) \<and> (xa = False \<longrightarrow> ex_nonz_cap_to p s \<and> valid_objs s \<and> tcb_at p s \<and> valid_mdb s \<and> tcb_at x s)) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> True) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> True) \<and> (cap = DomainCap \<longrightarrow> True) \<and> (cap = IRQControlCap \<longrightarrow> True) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. cap = ArchObjectCap x \<longrightarrow> True) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb. \<lbrakk>ex_nonz_cap_to p s; valid_objs s; valid_mdb s; tcb_at p s; cte_wp_at ((=) (ReplyCap x False xb)) (cur_thread s, tcb_cnode_index 3) s; \<not> xa\<rbrakk> \<Longrightarrow> tcb_at x s proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb. \<lbrakk>ex_nonz_cap_to p s; valid_objs s; valid_mdb s; tcb_at p s; \<not> xa; s \<turnstile> ReplyCap x False xb\<rbrakk> \<Longrightarrow> tcb_at x s proof (prove)
goal:
No subgoals!