theory ArchTcb_AI

lemma derive_no_cap_asid[wp,Tcb_AI_asms]:
  "\<lbrace>(no_cap_to_obj_with_diff_ref cap S)::'state_ext::state_ext state\<Rightarrow>bool\<rbrace>
     derive_cap slot cap
   \<lbrace>\<lambda>rv. no_cap_to_obj_with_diff_ref rv S\<rbrace>,-" apply (simp add: derive_cap_def arch_derive_cap_def
             cong: cap.case_cong) apply (rule hoare_pre) apply (wp | simp | wpc)+ apply (auto simp add: no_cap_to_obj_with_diff_ref_Null,
         auto simp add: no_cap_to_obj_with_diff_ref_def
                        table_cap_ref_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_cap_to_obj_with_diff_ref cap S\<rbrace> derive_cap slot cap \<lbrace>\<lambda>rv. no_cap_to_obj_with_diff_ref rv S\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_cap_to_obj_with_diff_ref cap S\<rbrace> case cap of UntypedCap dev ptr sz f \<Rightarrow> doE y <- ensure_no_children slot;
returnOk (UntypedCap dev ptr sz f)
odE | EndpointCap word1 word2 set \<Rightarrow> returnOk (EndpointCap word1 word2 set) | NotificationCap word1 word2 set \<Rightarrow> returnOk (NotificationCap word1 word2 set) | CNodeCap word nat list \<Rightarrow> returnOk (CNodeCap word nat list) | ThreadCap word \<Rightarrow> returnOk (ThreadCap word) | DomainCap \<Rightarrow> returnOk DomainCap | IRQHandlerCap word \<Rightarrow> returnOk (IRQHandlerCap word) | ArchObjectCap c \<Rightarrow> case c of PageCap dev r R pgs x \<Rightarrow> returnOk (ArchObjectCap (PageCap dev r R pgs None)) | PageTableCap xa None \<Rightarrow> throwError IllegalOperation | PageTableCap xa (Some x) \<Rightarrow> returnOk (ArchObjectCap c) | PageDirectoryCap xa None \<Rightarrow> throwError IllegalOperation | PageDirectoryCap xa (Some x) \<Rightarrow> returnOk (ArchObjectCap c) | _ \<Rightarrow> returnOk (ArchObjectCap c) | _ \<Rightarrow> returnOk NullCap \<lbrace>\<lambda>rv. no_cap_to_obj_with_diff_ref rv S\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'14\<rbrace> case cap of UntypedCap dev ptr sz f \<Rightarrow> doE y <- ensure_no_children slot;
returnOk (UntypedCap dev ptr sz f)
odE | EndpointCap word1 word2 set \<Rightarrow> returnOk (EndpointCap word1 word2 set) | NotificationCap word1 word2 set \<Rightarrow> returnOk (NotificationCap word1 word2 set) | CNodeCap word nat list \<Rightarrow> returnOk (CNodeCap word nat list) | ThreadCap word \<Rightarrow> returnOk (ThreadCap word) | DomainCap \<Rightarrow> returnOk DomainCap | IRQHandlerCap word \<Rightarrow> returnOk (IRQHandlerCap word) | ArchObjectCap c \<Rightarrow> case c of PageCap dev r R pgs x \<Rightarrow> returnOk (ArchObjectCap (PageCap dev r R pgs None)) | PageTableCap xa None \<Rightarrow> throwError IllegalOperation | PageTableCap xa (Some x) \<Rightarrow> returnOk (ArchObjectCap c) | PageDirectoryCap xa None \<Rightarrow> throwError IllegalOperation | PageDirectoryCap xa (Some x) \<Rightarrow> returnOk (ArchObjectCap c) | _ \<Rightarrow> returnOk (ArchObjectCap c) | _ \<Rightarrow> returnOk NullCap \<lbrace>\<lambda>rv. no_cap_to_obj_with_diff_ref rv S\<rbrace>, -
 2. \<And>s. no_cap_to_obj_with_diff_ref cap S s \<Longrightarrow> ?P'14 s proof (prove)
goal (1 subgoal):
 1. \<And>s. no_cap_to_obj_with_diff_ref cap S s \<Longrightarrow> (cap = NullCap \<longrightarrow> no_cap_to_obj_with_diff_ref NullCap S s) \<and> (\<forall>x xa xb xc. cap = UntypedCap x xa xb xc \<longrightarrow> no_cap_to_obj_with_diff_ref (UntypedCap x xa xb xc) S s) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> no_cap_to_obj_with_diff_ref (EndpointCap x xa xb) S s) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> no_cap_to_obj_with_diff_ref (NotificationCap x xa xb) S s) \<and> ((\<exists>x xa xb. cap = ReplyCap x xa xb) \<longrightarrow> no_cap_to_obj_with_diff_ref NullCap S s) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> no_cap_to_obj_with_diff_ref (CNodeCap x xa xb) S s) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> no_cap_to_obj_with_diff_ref (ThreadCap x) S s) \<and> (cap = DomainCap \<longrightarrow> no_cap_to_obj_with_diff_ref DomainCap S s) \<and> (cap = IRQControlCap \<longrightarrow> no_cap_to_obj_with_diff_ref NullCap S s) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> no_cap_to_obj_with_diff_ref (IRQHandlerCap x) S s) \<and> ((\<exists>x xa xb. cap = Zombie x xa xb) \<longrightarrow> no_cap_to_obj_with_diff_ref NullCap S s) \<and> (\<forall>x. cap = ArchObjectCap x \<longrightarrow> (\<forall>xa xb. x = ASIDPoolCap xa xb \<longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap (ASIDPoolCap xa xb)) S s) \<and> (x = ASIDControlCap \<longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap ASIDControlCap) S s) \<and> (\<forall>xa xb xc xd. (\<exists>xe. x = PageCap xa xb xc xd xe) \<longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageCap xa xb xc xd None)) S s) \<and> (\<forall>xa xb. x = PageTableCap xa xb \<longrightarrow> (\<forall>a b. xb = Some (a, b) \<longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageTableCap xa (Some (a, b)))) S s)) \<and> (\<forall>xa xb. x = PageDirectoryCap xa xb \<longrightarrow> (\<forall>x. xb = Some x \<longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageDirectoryCap xa (Some x))) S s))) proof (prove)
goal:
No subgoals!