theory Syscall_AI

lemma delete_caller_cap_nonz_cap:
  "\<lbrace>ex_nonz_cap_to p and tcb_at t and valid_objs\<rbrace>
      delete_caller_cap t
   \<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace>" apply (simp add: delete_caller_cap_def ex_nonz_cap_to_def cte_wp_at_caps_of_state) apply (rule hoare_pre) apply (wp hoare_vcg_ex_lift cap_delete_one_caps_of_state) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (rule_tac x=a in exI) apply (rule_tac x=b in exI) apply clarsimp apply (drule (1) tcb_cap_valid_caps_of_stateD) apply (drule (1) tcb_cnode_index_3_reply_or_null) apply (auto simp: is_cap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_nonz_cap_to p and tcb_at t and valid_objs\<rbrace> delete_caller_cap t \<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> zobj_refs cap) and tcb_at t and valid_objs\<rbrace> cap_delete_one (t, tcb_cnode_index 3) \<lbrace>\<lambda>rv s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> zobj_refs cap\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> cap_delete_one (t, tcb_cnode_index 3) \<lbrace>\<lambda>rv s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> zobj_refs cap\<rbrace>
 2. \<And>s. ((\<lambda>s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> zobj_refs cap) and tcb_at t and valid_objs) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> zobj_refs cap) and tcb_at t and valid_objs) s \<Longrightarrow> \<exists>x xa xb. cte_wp_at can_fast_finalise (t, tcb_cnode_index 3) s \<longrightarrow> ((caps_of_state s)((t, tcb_cnode_index 3) \<mapsto> NullCap)) (x, xa) = Some xb \<and> p \<in> zobj_refs xb proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap capa. \<lbrakk>tcb_at t s; valid_objs s; caps_of_state s (a, b) = Some cap; p \<in> zobj_refs cap; caps_of_state s (t, tcb_cnode_index 3) = Some capa; can_fast_finalise capa\<rbrakk> \<Longrightarrow> \<exists>x xa. (x = t \<longrightarrow> xa \<noteq> tcb_cnode_index 3) \<and> ((x = t \<longrightarrow> xa \<noteq> tcb_cnode_index 3) \<longrightarrow> (\<exists>xb. caps_of_state s (x, xa) = Some xb \<and> p \<in> zobj_refs xb)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap capa. \<lbrakk>tcb_at t s; valid_objs s; caps_of_state s (a, b) = Some cap; p \<in> zobj_refs cap; caps_of_state s (t, tcb_cnode_index 3) = Some capa; can_fast_finalise capa\<rbrakk> \<Longrightarrow> \<exists>x. (a = t \<longrightarrow> x \<noteq> tcb_cnode_index 3) \<and> ((a = t \<longrightarrow> x \<noteq> tcb_cnode_index 3) \<longrightarrow> (\<exists>xa. caps_of_state s (a, x) = Some xa \<and> p \<in> zobj_refs xa)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap capa. \<lbrakk>tcb_at t s; valid_objs s; caps_of_state s (a, b) = Some cap; p \<in> zobj_refs cap; caps_of_state s (t, tcb_cnode_index 3) = Some capa; can_fast_finalise capa\<rbrakk> \<Longrightarrow> (a = t \<longrightarrow> b \<noteq> tcb_cnode_index 3) \<and> ((a = t \<longrightarrow> b \<noteq> tcb_cnode_index 3) \<longrightarrow> (\<exists>x. caps_of_state s (a, b) = Some x \<and> p \<in> zobj_refs x)) proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>tcb_at t s; valid_objs s; p \<in> zobj_refs cap; caps_of_state s (t, tcb_cnode_index 3) = Some cap; can_fast_finalise cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>tcb_at t s; valid_objs s; p \<in> zobj_refs cap; can_fast_finalise cap; tcb_cap_valid cap (t, tcb_cnode_index 3) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>valid_objs s; p \<in> zobj_refs cap; can_fast_finalise cap; tcb_cap_valid cap (t, tcb_cnode_index 3) s; is_reply_cap cap \<or> cap = NullCap\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!