theory Syscall_R

lemma decode_inv_wf'[wp]:
  "\<lbrace>valid_cap' cap and invs' and sch_act_simple
          and cte_wp_at' ((=) cap \<circ> cteCap) slot and real_cte_at' slot
          and (\<lambda>s. \<forall>r\<in>zobj_refs' cap. ex_nonz_cap_to' r s)
          and (\<lambda>s. \<forall>r\<in>cte_refs' cap (irq_node' s). ex_cte_cap_to' r s)
          and (\<lambda>s. \<forall>cap \<in> set excaps. \<forall>r\<in>cte_refs' (fst cap) (irq_node' s). ex_cte_cap_to' r s)
          and (\<lambda>s. \<forall>cap \<in> set excaps. \<forall>r\<in>zobj_refs' (fst cap). ex_nonz_cap_to' r s)
          and (\<lambda>s. \<forall>x \<in> set excaps. cte_wp_at' ((=) (fst x) \<circ> cteCap) (snd x) s)
          and (\<lambda>s. \<forall>x \<in> set excaps. s \<turnstile>' fst x)
          and (\<lambda>s. \<forall>x \<in> set excaps. real_cte_at' (snd x) s)
          and (\<lambda>s. \<forall>x \<in> set excaps. ex_cte_cap_wp_to' isCNodeCap (snd x) s)
          and (\<lambda>s. \<forall>x \<in> set excaps. cte_wp_at' (badge_derived' (fst x) \<circ> cteCap) (snd x) s)
          and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace>
     decodeInvocation label args cap_index slot cap excaps
   \<lbrace>valid_invocation'\<rbrace>,-" apply (case_tac cap,
         simp_all add: decodeInvocation_def Let_def isCap_defs uncurry_def split_def
            split del: if_split
                 cong: if_cong) apply ((rule hoare_pre,
                     ((wpsimp wp: decodeTCBInv_wf simp: o_def)+)[1],
                     clarsimp simp: valid_cap'_def cte_wp_at_ctes_of)
                    | intro exI conjI | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap' cap and invs' and sch_act_simple and cte_wp_at' ((=) cap \<circ> cteCap) slot and real_cte_at' slot and (\<lambda>s. \<forall>r\<in>zobj_refs' cap. ex_nonz_cap_to' r s) and (\<lambda>s. \<forall>r\<in>cte_refs' cap (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s) and (\<lambda>s. \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs' (fst cap) (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s) and (\<lambda>s. \<forall>cap\<in>set excaps. \<forall>r\<in>zobj_refs' (fst cap). ex_nonz_cap_to' r s) and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at' ((=) (fst x) \<circ> cteCap) (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. valid_cap' (fst x) s) and (\<lambda>s. \<forall>x\<in>set excaps. real_cte_at' (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. ex_cte_cap_wp_to' isCNodeCap (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at' (badge_derived' (fst x) \<circ> cteCap) (snd x) s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> global.decodeInvocation label args cap_index slot cap excaps \<lbrace>valid_invocation'\<rbrace>, - proof (prove)
goal (12 subgoals):
 1. \<And>x1. cap = capability.ThreadCap x1 \<Longrightarrow> \<lbrace>valid_cap' (capability.ThreadCap x1) and invs' and sch_act_simple and cte_wp_at' ((=) (capability.ThreadCap x1) \<circ> cteCap) slot and real_cte_at' slot and ex_nonz_cap_to' x1 and (\<lambda>s. \<forall>r\<in>dom tcb_cte_cases. ex_cte_cap_wp_to' (\<lambda>_. True) (x1 + r) s) and (\<lambda>s. \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs' (fst cap) (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s) and (\<lambda>s. \<forall>cap\<in>set excaps. \<forall>r\<in>zobj_refs' (fst cap). ex_nonz_cap_to' r s) and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at' ((=) (fst x) \<circ> cteCap) (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. valid_cap' (fst x) s) and (\<lambda>s. \<forall>x\<in>set excaps. real_cte_at' (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. ex_cte_cap_wp_to' isCNodeCap (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at' (badge_derived' (fst x) \<circ> cteCap) (snd x) s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftME Invocations_H.invocation.InvokeTCB (decodeTCBInvocation label args (capability.ThreadCap x1) slot excaps) \<lbrace>valid_invocation'\<rbrace>, -
 2. cap = capability.NullCap \<Longrightarrow> \<lbrace>valid_cap' capability.NullCap and invs' and sch_act_simple and cte_wp_at' ((=) capability.NullCap \<circ> cteCap) slot and real_cte_at' slot and (\<lambda>s. \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs' (fst cap) (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s) and (\<lambda>s. \<forall>cap\<in>set excaps. \<forall>r\<in>zobj_refs' (fst cap). ex_nonz_cap_to' r s) and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at' ((=) (fst x) \<circ> cteCap) (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. valid_cap' (fst x) s) and (\<lambda>s. \<forall>x\<in>set excaps. real_cte_at' (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. ex_cte_cap_wp_to' isCNodeCap (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at' (badge_derived' (fst x) \<circ> cteCap) (snd x) s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> throwError (Fault_H.syscall_error.InvalidCapability 0) \<lbrace>valid_invocation'\<rbrace>, -
 3. \<And>x31 x32 x33 x34. cap = capability.NotificationCap x31 x32 x33 x34 \<Longrightarrow> \<lbrace>valid_cap' (capability.NotificationCap x31 x32 x33 x34) and invs' and sch_act_simple and cte_wp_at' ((=) (capability.NotificationCap x31 x32 x33 x34) \<circ> cteCap) slot and real_cte_at' slot and ex_nonz_cap_to' x31 and (\<lambda>s. \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs' (fst cap) (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s) and (\<lambda>s. \<forall>cap\<in>set excaps. \<forall>r\<in>zobj_refs' (fst cap). ex_nonz_cap_to' r s) and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at' ((=) (fst x) \<circ> cteCap) (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. valid_cap' (fst x) s) and (\<lambda>s. \<forall>x\<in>set excaps. real_cte_at' (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. ex_cte_cap_wp_to' isCNodeCap (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at' (badge_derived' (fst x) \<circ> cteCap) (snd x) s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> if x33 then returnOk (Invocations_H.invocation.InvokeNotification x31 x32) else throwError (Fault_H.syscall_error.InvalidCapability 0) \<lbrace>valid_invocation'\<rbrace>, -
 4. \<And>x4. cap = capability.IRQHandlerCap x4 \<Longrightarrow> \<lbrace>valid_cap' (capability.IRQHandlerCap x4) and invs' and sch_act_simple and cte_wp_at' ((=) (capability.IRQHandlerCap x4) \<circ> cteCap) slot and real_cte_at' slot and (\<lambda>s. ex_cte_cap_wp_to' (\<lambda>_. True) (irq_node' s + UCAST(10 \<rightarrow> 32) x4 * 0x10) s) and (\<lambda>s. \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs' (fst cap) (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s) and (\<lambda>s. \<forall>cap\<in>set excaps. \<forall>r\<in>zobj_refs' (fst cap). ex_nonz_cap_to' r s) and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at' ((=) (fst x) \<circ> cteCap) (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. valid_cap' (fst x) s) and (\<lambda>s. \<forall>x\<in>set excaps. real_cte_at' (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. ex_cte_cap_wp_to' isCNodeCap (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at' (badge_derived' (fst x) \<circ> cteCap) (snd x) s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftME Invocations_H.invocation.InvokeIRQHandler (decodeIRQHandlerInvocation label x4 excaps) \<lbrace>valid_invocation'\<rbrace>, -
 5. \<And>x51 x52 x53 x54 x55 x56. cap = capability.EndpointCap x51 x52 x53 x54 x55 x56 \<Longrightarrow> \<lbrace>valid_cap' (capability.EndpointCap x51 x52 x53 x54 x55 x56) and invs' and sch_act_simple and cte_wp_at' ((=) (capability.EndpointCap x51 x52 x53 x54 x55 x56) \<circ> cteCap) slot and real_cte_at' slot and ex_nonz_cap_to' x51 and (\<lambda>s. \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs' (fst cap) (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s) and (\<lambda>s. \<forall>cap\<in>set excaps. \<forall>r\<in>zobj_refs' (fst cap). ex_nonz_cap_to' r s) and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at' ((=) (fst x) \<circ> cteCap) (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. valid_cap' (fst x) s) and (\<lambda>s. \<forall>x\<in>set excaps. real_cte_at' (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. ex_cte_cap_wp_to' isCNodeCap (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at' (badge_derived' (fst x) \<circ> cteCap) (snd x) s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> if x53 then returnOk (Invocations_H.invocation.InvokeEndpoint x51 x52 x55 x56) else throwError (Fault_H.syscall_error.InvalidCapability 0) \<lbrace>valid_invocation'\<rbrace>, -
 6. cap = capability.DomainCap \<Longrightarrow> \<lbrace>valid_cap' capability.DomainCap and invs' and sch_act_simple and cte_wp_at' ((=) capability.DomainCap \<circ> cteCap) slot and real_cte_at' slot and (\<lambda>s. \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs' (fst cap) (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s) and (\<lambda>s. \<forall>cap\<in>set excaps. \<forall>r\<in>zobj_refs' (fst cap). ex_nonz_cap_to' r s) and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at' ((=) (fst x) \<circ> cteCap) (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. valid_cap' (fst x) s) and (\<lambda>s. \<forall>x\<in>set excaps. real_cte_at' (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. ex_cte_cap_wp_to' isCNodeCap (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at' (badge_derived' (fst x) \<circ> cteCap) (snd x) s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftME (\<lambda>p. Invocations_H.invocation.InvokeDomain (fst p) (snd p)) (decodeDomainInvocation label args excaps) \<lbrace>valid_invocation'\<rbrace>, -
 7. \<And>x71 x72 x73. cap = capability.Zombie x71 x72 x73 \<Longrightarrow> \<lbrace>valid_cap' (capability.Zombie x71 x72 x73) and invs' and sch_act_simple and cte_wp_at' ((=) (capability.Zombie x71 x72 x73) \<circ> cteCap) slot and real_cte_at' slot and (\<lambda>s. \<forall>r\<in>{0..<word_of_nat x73}. ex_cte_cap_wp_to' (\<lambda>_. True) (x71 + r * 2 ^ cteSizeBits) s) and (\<lambda>s. \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs' (fst cap) (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s) and (\<lambda>s. \<forall>cap\<in>set excaps. \<forall>r\<in>zobj_refs' (fst cap). ex_nonz_cap_to' r s) and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at' ((=) (fst x) \<circ> cteCap) (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. valid_cap' (fst x) s) and (\<lambda>s. \<forall>x\<in>set excaps. real_cte_at' (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. ex_cte_cap_wp_to' isCNodeCap (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at' (badge_derived' (fst x) \<circ> cteCap) (snd x) s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> throwError (Fault_H.syscall_error.InvalidCapability 0) \<lbrace>valid_invocation'\<rbrace>, -
 8. \<And>x8. cap = capability.ArchObjectCap x8 \<Longrightarrow> \<lbrace>valid_cap' (capability.ArchObjectCap x8) and invs' and sch_act_simple and cte_wp_at' ((=) (capability.ArchObjectCap x8) \<circ> cteCap) slot and real_cte_at' slot and (\<lambda>s. \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs' (fst cap) (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s) and (\<lambda>s. \<forall>cap\<in>set excaps. \<forall>r\<in>zobj_refs' (fst cap). ex_nonz_cap_to' r s) and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at' ((=) (fst x) \<circ> cteCap) (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. valid_cap' (fst x) s) and (\<lambda>s. \<forall>x\<in>set excaps. real_cte_at' (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. ex_cte_cap_wp_to' isCNodeCap (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at' (badge_derived' (fst x) \<circ> cteCap) (snd x) s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftME Invocations_H.invocation.InvokeArchObject (Arch.decodeInvocation label args cap_index slot x8 excaps) \<lbrace>valid_invocation'\<rbrace>, -
 9. \<And>x91 x92 x93. cap = capability.ReplyCap x91 x92 x93 \<Longrightarrow> \<lbrace>valid_cap' (capability.ReplyCap x91 x92 x93) and invs' and sch_act_simple and cte_wp_at' ((=) (capability.ReplyCap x91 x92 x93) \<circ> cteCap) slot and real_cte_at' slot and (\<lambda>s. \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs' (fst cap) (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s) and (\<lambda>s. \<forall>cap\<in>set excaps. \<forall>r\<in>zobj_refs' (fst cap). ex_nonz_cap_to' r s) and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at' ((=) (fst x) \<circ> cteCap) (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. valid_cap' (fst x) s) and (\<lambda>s. \<forall>x\<in>set excaps. real_cte_at' (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. ex_cte_cap_wp_to' isCNodeCap (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at' (badge_derived' (fst x) \<circ> cteCap) (snd x) s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> if \<not> x92 then returnOk (Invocations_H.invocation.InvokeReply x91 slot x93) else throwError (Fault_H.syscall_error.InvalidCapability 0) \<lbrace>valid_invocation'\<rbrace>, -
 10. \<And>x101 x102 x103 x104. cap = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> \<lbrace>valid_cap' (capability.UntypedCap x101 x102 x103 x104) and invs' and sch_act_simple and cte_wp_at' ((=) (capability.UntypedCap x101 x102 x103 x104) \<circ> cteCap) slot and real_cte_at' slot and (\<lambda>s. \<forall>cap\<in>set excaps. \<forall>r\<in>cte_refs' (fst cap) (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s) and (\<lambda>s. \<forall>cap\<in>set excaps. \<forall>r\<in>zobj_refs' (fst cap). ex_nonz_cap_to' r s) and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at' ((=) (fst x) \<circ> cteCap) (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. valid_cap' (fst x) s) and (\<lambda>s. \<forall>x\<in>set excaps. real_cte_at' (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. ex_cte_cap_wp_to' isCNodeCap (snd x) s) and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at' (badge_derived' (fst x) \<circ> cteCap) (snd x) s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftME Invocations_H.invocation.InvokeUntyped (decodeUntypedInvocation label args slot (capability.UntypedCap x101 x102 x103 x104) (map fst excaps)) \<lbrace>valid_invocation'\<rbrace>, -
A total of 12 subgoals... proof (prove)
goal:
No subgoals!