theory Syscall_AI

lemma (in Syscall_AI) hr_invs[wp]:
  "\<lbrace>invs :: 'state_ext state \<Rightarrow> _\<rbrace> handle_reply \<lbrace>\<lambda>rv. invs\<rbrace>" apply (simp add: handle_reply_def) apply (rule hoare_seq_ext [OF _ gets_sp]) apply (rule hoare_seq_ext [OF _ get_cap_sp]) apply (rule hoare_pre) apply (wp | wpc)+ apply (clarsimp simp: cte_wp_at_eq_simp) apply (frule cte_wp_at_valid_objs_valid_cap) apply clarsimp+ apply (fastforce simp: valid_cap_def is_reply_cap_to_def
                 split: cap.splits
                  elim: cte_wp_at_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> handle_reply \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<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. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>thread. \<lbrace>invs and (\<lambda>s. cur_thread s = thread)\<rbrace> do 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. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>thread caller_cap. \<lbrace>invs and (\<lambda>s. cur_thread s = thread) and cte_wp_at (\<lambda>c. c = caller_cap) (thread, tcb_cnode_index 3)\<rbrace> 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 \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>thread caller_cap. \<lbrace>?Q8 thread caller_cap\<rbrace> 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 \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>thread caller_cap s. (invs and (\<lambda>s. cur_thread s = thread) and cte_wp_at (\<lambda>c. c = caller_cap) (thread, tcb_cnode_index 3)) s \<Longrightarrow> ?Q8 thread caller_cap s proof (prove)
goal (1 subgoal):
 1. \<And>thread caller_cap s. (invs and (\<lambda>s. cur_thread s = thread) and cte_wp_at (\<lambda>c. c = caller_cap) (thread, tcb_cnode_index 3)) s \<Longrightarrow> (caller_cap = NullCap \<longrightarrow> invs 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> (tcb_at x and tcb_at thread and cte_wp_at (is_reply_cap_to x) (thread, tcb_cnode_index 3) and invs) 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) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb. \<lbrakk>invs s; cte_wp_at (\<lambda>c. c = ReplyCap x False xb) (cur_thread s, tcb_cnode_index 3) s; \<not> xa\<rbrakk> \<Longrightarrow> tcb_at x s \<and> tcb_at (cur_thread s) s \<and> cte_wp_at (is_reply_cap_to x) (cur_thread s, tcb_cnode_index 3) s proof (prove)
goal (2 subgoals):
 1. \<And>s x xa xb. \<lbrakk>invs s; cte_wp_at (\<lambda>c. c = ReplyCap x False xb) (cur_thread s, tcb_cnode_index 3) s; \<not> xa\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<And>s x xa xb. \<lbrakk>invs s; cte_wp_at (\<lambda>c. c = ReplyCap x False xb) (cur_thread s, tcb_cnode_index 3) s; \<not> xa; \<exists>cap. cap = ReplyCap x False xb \<and> s \<turnstile> cap\<rbrakk> \<Longrightarrow> tcb_at x s \<and> tcb_at (cur_thread s) s \<and> cte_wp_at (is_reply_cap_to x) (cur_thread s, tcb_cnode_index 3) s proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb. \<lbrakk>invs s; cte_wp_at (\<lambda>c. c = ReplyCap x False xb) (cur_thread s, tcb_cnode_index 3) s; \<not> xa; s \<turnstile> ReplyCap x False xb\<rbrakk> \<Longrightarrow> tcb_at x s \<and> tcb_at (cur_thread s) s \<and> cte_wp_at (is_reply_cap_to x) (cur_thread s, tcb_cnode_index 3) s proof (prove)
goal:
No subgoals!