theory Syscall_DR

lemma not_master_reply_cap_lcs[wp]:
  "\<lbrace>valid_reply_masters and valid_objs\<rbrace>CSpace_A.lookup_cap_and_slot t ptr
            \<lbrace>\<lambda>rv s. \<not> is_master_reply_cap (fst rv)\<rbrace>,-" apply (simp add:lookup_cap_and_slot_def) apply wp apply (simp add:split_def) apply wp apply (rule_tac Q ="\<lambda>cap. cte_wp_at (\<lambda>x. x = cap) (fst x) and real_cte_at (fst x)
                              and valid_reply_masters and valid_objs" in hoare_strengthen_post) apply (wp get_cap_cte_wp_at) apply clarify apply (drule real_cte_not_reply_masterD) apply clarsimp+ apply (simp add:cte_wp_at_def) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_masters and valid_objs\<rbrace> CSpace_A.lookup_cap_and_slot t ptr \<lbrace>\<lambda>rv s. \<not> is_master_reply_cap (fst rv)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_masters and valid_objs\<rbrace> doE (slot, cr) <- lookup_slot_for_thread t ptr;
cap <- liftE (CSpaceAcc_A.get_cap slot);
returnOk (cap, slot)
odE \<lbrace>\<lambda>rv s. \<not> is_master_reply_cap (fst rv)\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>?B1 x\<rbrace> case x of (slot, cr) \<Rightarrow> doE cap <- liftE (CSpaceAcc_A.get_cap slot);
returnOk (cap, slot)
odE \<lbrace>\<lambda>rv s. \<not> is_master_reply_cap (fst rv)\<rbrace>, -
 2. \<lbrace>?P'\<rbrace> lookup_slot_for_thread t ptr \<lbrace>?B1\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. (valid_reply_masters and valid_objs) s \<Longrightarrow> ?P' s proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>?B1 x\<rbrace> doE cap <- liftE (CSpaceAcc_A.get_cap (fst x));
returnOk (cap, fst x)
odE \<lbrace>\<lambda>rv s. \<not> is_master_reply_cap (fst rv)\<rbrace>, -
 2. \<lbrace>?P'\<rbrace> lookup_slot_for_thread t ptr \<lbrace>?B1\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. (valid_reply_masters and valid_objs) s \<Longrightarrow> ?P' s proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>?P'5 x\<rbrace> CSpaceAcc_A.get_cap (fst x) \<lbrace>\<lambda>cap a. \<not> is_master_reply_cap (fst (cap, fst x))\<rbrace>
 2. \<lbrace>?P'\<rbrace> lookup_slot_for_thread t ptr \<lbrace>\<lambda>x s. True \<and> ?P'5 x s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. (valid_reply_masters and valid_objs) s \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrace>?P'5 x\<rbrace> CSpaceAcc_A.get_cap (fst x) \<lbrace>\<lambda>cap. cte_wp_at (\<lambda>x. x = cap) (fst x) and real_cte_at (fst x) and valid_reply_masters and valid_objs\<rbrace>
 2. \<And>x rv s. (cte_wp_at (\<lambda>x. x = rv) (fst x) and real_cte_at (fst x) and valid_reply_masters and valid_objs) s \<Longrightarrow> \<not> is_master_reply_cap (fst (rv, fst x))
 3. \<lbrace>?P'\<rbrace> lookup_slot_for_thread t ptr \<lbrace>\<lambda>x s. True \<and> ?P'5 x s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. (valid_reply_masters and valid_objs) s \<Longrightarrow> ?P' s proof (prove)
goal (3 subgoals):
 1. \<And>x rv s. (cte_wp_at (\<lambda>x. x = rv) (fst x) and real_cte_at (fst x) and valid_reply_masters and valid_objs) s \<Longrightarrow> \<not> is_master_reply_cap (fst (rv, fst x))
 2. \<lbrace>?P'\<rbrace> lookup_slot_for_thread t ptr \<lbrace>\<lambda>x s. True \<and> True \<and> real_cte_at (fst x) s \<and> valid_reply_masters s \<and> valid_objs s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. (valid_reply_masters and valid_objs) s \<Longrightarrow> ?P' s proof (prove)
goal (3 subgoals):
 1. \<And>a b ba rv s. \<lbrakk>valid_objs s; valid_reply_masters s; cte_wp_at (\<lambda>x. x = rv) (fst ((a, b), ba)) s; real_cte_at (fst ((a, b), ba)) s; is_master_reply_cap (fst (rv, fst ((a, b), ba)))\<rbrakk> \<Longrightarrow> False
 2. \<lbrace>?P'\<rbrace> lookup_slot_for_thread t ptr \<lbrace>\<lambda>x s. True \<and> True \<and> real_cte_at (fst x) s \<and> valid_reply_masters s \<and> valid_objs s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. (valid_reply_masters and valid_objs) s \<Longrightarrow> ?P' s proof (prove)
goal (5 subgoals):
 1. \<And>a b ba rv s. \<lbrakk>valid_objs s; valid_reply_masters s; cte_wp_at (\<lambda>x. x = rv) (fst ((a, b), ba)) s; is_master_reply_cap (fst (rv, fst ((a, b), ba)))\<rbrakk> \<Longrightarrow> valid_reply_masters s
 2. \<And>a b ba rv s. \<lbrakk>valid_objs s; valid_reply_masters s; cte_wp_at (\<lambda>x. x = rv) (fst ((a, b), ba)) s; is_master_reply_cap (fst (rv, fst ((a, b), ba)))\<rbrakk> \<Longrightarrow> valid_objs s
 3. \<And>a b ba rv s. \<lbrakk>valid_objs s; valid_reply_masters s; cte_wp_at (\<lambda>x. x = rv) (fst ((a, b), ba)) s; is_master_reply_cap (fst (rv, fst ((a, b), ba))); cte_wp_at (\<lambda>cap. \<not> is_master_reply_cap cap) (fst ((a, b), ba)) s\<rbrakk> \<Longrightarrow> False
 4. \<lbrace>?P'\<rbrace> lookup_slot_for_thread t ptr \<lbrace>\<lambda>x s. True \<and> True \<and> real_cte_at (fst x) s \<and> valid_reply_masters s \<and> valid_objs s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. (valid_reply_masters and valid_objs) s \<Longrightarrow> ?P' s proof (prove)
goal (3 subgoals):
 1. \<And>a b rv s. \<lbrakk>valid_objs s; valid_reply_masters s; cte_wp_at (\<lambda>x. x = rv) (a, b) s; is_master_reply_cap rv; cte_wp_at (\<lambda>cap. \<not> is_master_reply_cap cap) (a, b) s\<rbrakk> \<Longrightarrow> False
 2. \<lbrace>?P'\<rbrace> lookup_slot_for_thread t ptr \<lbrace>\<lambda>x s. True \<and> True \<and> real_cte_at (fst x) s \<and> valid_reply_masters s \<and> valid_objs s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. (valid_reply_masters and valid_objs) s \<Longrightarrow> ?P' s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> lookup_slot_for_thread t ptr \<lbrace>\<lambda>x s. True \<and> True \<and> real_cte_at (fst x) s \<and> valid_reply_masters s \<and> valid_objs s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>s. (valid_reply_masters and valid_objs) s \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_reply_masters and valid_objs) s \<Longrightarrow> True \<and> True \<and> True \<and> valid_objs s \<and> valid_reply_masters s \<and> valid_objs s proof (prove)
goal:
No subgoals!