theory Tcb_AI

lemma decode_tcb_inv_wf:
  "\<lbrace>invs and tcb_at t and ex_nonz_cap_to t
         and cte_at slot and ex_cte_cap_to slot
         and (\<lambda>(s::'state_ext::state_ext state). \<forall>x \<in> set extras. real_cte_at (snd x) s \<and> s \<turnstile> fst x
                                 \<and> ex_cte_cap_to (snd x) s
                                 \<and> (\<forall>y \<in> zobj_refs (fst x). ex_nonz_cap_to y s)
                                 \<and> no_cap_to_obj_dr_emp (fst x) s)\<rbrace>
      decode_tcb_invocation label args (cap.ThreadCap t) slot extras
   \<lbrace>tcb_inv_wf\<rbrace>,-" apply (simp add: decode_tcb_invocation_def Let_def
              cong: if_cong split del: if_split) apply (rule hoare_vcg_precond_impE_R) apply wpc apply (wp decode_tcb_conf_wf decode_readreg_wf
             decode_writereg_wf decode_copyreg_wf
             decode_bind_notification_wf decode_unbind_notification_wf
             decode_set_priority_wf decode_set_tls_base_wf)+ apply (clarsimp simp: real_cte_at_cte) apply (fastforce simp: real_cte_at_not_tcb_at) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and tcb_at t and ex_nonz_cap_to t and cte_wp_at (\<lambda>_. True) slot and ex_cte_cap_wp_to (\<lambda>_. True) slot and (\<lambda>s. \<forall>x\<in>set extras. real_cte_at (snd x) s \<and> s \<turnstile> fst x \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd x) s \<and> (\<forall>y\<in>zobj_refs (fst x). ex_nonz_cap_to y s) \<and> no_cap_to_obj_dr_emp (fst x) s)\<rbrace> decode_tcb_invocation label args (ThreadCap t) slot extras \<lbrace>tcb_inv_wf\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and tcb_at t and ex_nonz_cap_to t and cte_wp_at (\<lambda>_. True) slot and ex_cte_cap_wp_to (\<lambda>_. True) slot and (\<lambda>s. \<forall>x\<in>set extras. real_cte_at (snd x) s \<and> s \<turnstile> fst x \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd x) s \<and> (\<forall>y\<in>zobj_refs (fst x). ex_nonz_cap_to y s) \<and> no_cap_to_obj_dr_emp (fst x) s)\<rbrace> case gen_invocation_type label of TCBReadRegisters \<Rightarrow> decode_read_registers args (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args (ThreadCap t) $ map fst extras | TCBConfigure \<Rightarrow> decode_tcb_configure args (ThreadCap t) slot extras | TCBSetPriority \<Rightarrow> decode_set_priority args (ThreadCap t) slot extras | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args (ThreadCap t) slot extras | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args (ThreadCap t) slot extras | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args (ThreadCap t) slot extras | TCBSetSpace \<Rightarrow> decode_set_space args (ThreadCap t) slot extras | TCBSuspend \<Rightarrow> returnOk $ Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) extras | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>tcb_inv_wf\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> case gen_invocation_type label of TCBReadRegisters \<Rightarrow> decode_read_registers args (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args (ThreadCap t) $ map fst extras | TCBConfigure \<Rightarrow> decode_tcb_configure args (ThreadCap t) slot extras | TCBSetPriority \<Rightarrow> decode_set_priority args (ThreadCap t) slot extras | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args (ThreadCap t) slot extras | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args (ThreadCap t) slot extras | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args (ThreadCap t) slot extras | TCBSetSpace \<Rightarrow> decode_set_space args (ThreadCap t) slot extras | TCBSuspend \<Rightarrow> returnOk $ Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) extras | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>tcb_inv_wf\<rbrace>, -
 2. \<And>s. (invs and tcb_at t and ex_nonz_cap_to t and cte_wp_at (\<lambda>_. True) slot and ex_cte_cap_wp_to (\<lambda>_. True) slot and (\<lambda>s. \<forall>x\<in>set extras. real_cte_at (snd x) s \<and> s \<turnstile> fst x \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd x) s \<and> (\<forall>y\<in>zobj_refs (fst x). ex_nonz_cap_to y s) \<and> no_cap_to_obj_dr_emp (fst x) s)) s \<Longrightarrow> ?P' s proof (prove)
goal (31 subgoals):
 1. gen_invocation_type label = InvalidInvocation \<Longrightarrow> \<lbrace>?R64\<rbrace> throwError IllegalOperation \<lbrace>tcb_inv_wf\<rbrace>, -
 2. gen_invocation_type label = UntypedRetype \<Longrightarrow> \<lbrace>?R63\<rbrace> throwError IllegalOperation \<lbrace>tcb_inv_wf\<rbrace>, -
 3. gen_invocation_type label = TCBReadRegisters \<Longrightarrow> \<lbrace>?R62\<rbrace> decode_read_registers args (ThreadCap t) \<lbrace>tcb_inv_wf\<rbrace>, -
 4. gen_invocation_type label = TCBWriteRegisters \<Longrightarrow> \<lbrace>?R61\<rbrace> decode_write_registers args (ThreadCap t) \<lbrace>tcb_inv_wf\<rbrace>, -
 5. gen_invocation_type label = TCBCopyRegisters \<Longrightarrow> \<lbrace>?R60\<rbrace> decode_copy_registers args (ThreadCap t) $ map fst extras \<lbrace>tcb_inv_wf\<rbrace>, -
 6. gen_invocation_type label = TCBConfigure \<Longrightarrow> \<lbrace>?R59\<rbrace> decode_tcb_configure args (ThreadCap t) slot extras \<lbrace>tcb_inv_wf\<rbrace>, -
 7. gen_invocation_type label = TCBSetPriority \<Longrightarrow> \<lbrace>?R58\<rbrace> decode_set_priority args (ThreadCap t) slot extras \<lbrace>tcb_inv_wf\<rbrace>, -
 8. gen_invocation_type label = TCBSetMCPriority \<Longrightarrow> \<lbrace>?R57\<rbrace> decode_set_mcpriority args (ThreadCap t) slot extras \<lbrace>tcb_inv_wf\<rbrace>, -
 9. gen_invocation_type label = TCBSetSchedParams \<Longrightarrow> \<lbrace>?R56\<rbrace> decode_set_sched_params args (ThreadCap t) slot extras \<lbrace>tcb_inv_wf\<rbrace>, -
 10. gen_invocation_type label = TCBSetIPCBuffer \<Longrightarrow> \<lbrace>?R55\<rbrace> decode_set_ipc_buffer args (ThreadCap t) slot extras \<lbrace>tcb_inv_wf\<rbrace>, -
A total of 31 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs and tcb_at t and ex_nonz_cap_to t and cte_wp_at (\<lambda>_. True) slot and ex_cte_cap_wp_to (\<lambda>_. True) slot and (\<lambda>s. \<forall>x\<in>set extras. real_cte_at (snd x) s \<and> s \<turnstile> fst x \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd x) s \<and> (\<forall>y\<in>zobj_refs (fst x). ex_nonz_cap_to y s) \<and> no_cap_to_obj_dr_emp (fst x) s)) s \<Longrightarrow> (gen_invocation_type label = InvalidInvocation \<longrightarrow> True) \<and> (gen_invocation_type label = UntypedRetype \<longrightarrow> True) \<and> (gen_invocation_type label = TCBReadRegisters \<longrightarrow> (invs and tcb_at t and ex_nonz_cap_to t) s) \<and> (gen_invocation_type label = TCBWriteRegisters \<longrightarrow> (invs and tcb_at t and ex_nonz_cap_to t) s) \<and> (gen_invocation_type label = TCBCopyRegisters \<longrightarrow> (invs and tcb_at t and ex_nonz_cap_to t and (\<lambda>s. \<forall>x\<in>set (map fst extras). s \<turnstile> x \<and> (\<forall>y\<in>zobj_refs x. ex_nonz_cap_to y s))) s) \<and> (gen_invocation_type label = TCBConfigure \<longrightarrow> (invs and tcb_at t and cte_wp_at (\<lambda>_. True) slot and ex_cte_cap_wp_to (\<lambda>_. True) slot and ex_nonz_cap_to t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd x) s \<and> t \<noteq> fst (snd x) \<and> no_cap_to_obj_dr_emp (fst x) s)) s) \<and> (gen_invocation_type label = TCBSetPriority \<longrightarrow> (invs and tcb_at t and ex_nonz_cap_to t) s) \<and> (gen_invocation_type label = TCBSetMCPriority \<longrightarrow> (invs and tcb_at t and ex_nonz_cap_to t) s) \<and> (gen_invocation_type label = TCBSetSchedParams \<longrightarrow> (invs and tcb_at t and ex_nonz_cap_to t) s) \<and> (gen_invocation_type label = TCBSetIPCBuffer \<longrightarrow> (invs and tcb_at t and cte_wp_at (\<lambda>_. True) slot and ex_cte_cap_wp_to (\<lambda>_. True) slot and ex_nonz_cap_to t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd x) s \<and> no_cap_to_obj_dr_emp (fst x) s)) s) \<and> (gen_invocation_type label = TCBSetSpace \<longrightarrow> (invs and tcb_at t and cte_wp_at (\<lambda>_. True) slot and ex_cte_cap_wp_to (\<lambda>_. True) slot and ex_nonz_cap_to t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd x) s \<and> t \<noteq> fst (snd x) \<and> no_cap_to_obj_dr_emp (fst x) s)) s) \<and> (gen_invocation_type label = TCBSuspend \<longrightarrow> tcb_inv_wf (Suspend $ obj_ref_of (ThreadCap t)) s) \<and> (gen_invocation_type label = TCBResume \<longrightarrow> tcb_inv_wf (Resume $ obj_ref_of (ThreadCap t)) s) \<and> (gen_invocation_type label = TCBBindNotification \<longrightarrow> (invs and tcb_at t and ex_nonz_cap_to t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> (\<forall>y\<in>zobj_refs (fst x). ex_nonz_cap_to y s))) s) \<and> (gen_invocation_type label = TCBUnbindNotification \<longrightarrow> (invs and tcb_at t and ex_nonz_cap_to t) s) \<and> (gen_invocation_type label = TCBSetTLSBase \<longrightarrow> (invs and tcb_at t and ex_nonz_cap_to t) s) \<and> (gen_invocation_type label = CNodeRevoke \<longrightarrow> True) \<and> (gen_invocation_type label = CNodeDelete \<longrightarrow> True) \<and> (gen_invocation_type label = CNodeCancelBadgedSends \<longrightarrow> True) \<and> (gen_invocation_type label = CNodeCopy \<longrightarrow> True) \<and> (gen_invocation_type label = CNodeMint \<longrightarrow> True) \<and> (gen_invocation_type label = CNodeMove \<longrightarrow> True) \<and> (gen_invocation_type label = CNodeMutate \<longrightarrow> True) \<and> (gen_invocation_type label = CNodeRotate \<longrightarrow> True) \<and> (gen_invocation_type label = CNodeSaveCaller \<longrightarrow> True) \<and> (gen_invocation_type label = IRQIssueIRQHandler \<longrightarrow> True) \<and> (gen_invocation_type label = IRQAckIRQ \<longrightarrow> True) \<and> (gen_invocation_type label = IRQSetIRQHandler \<longrightarrow> True) \<and> (gen_invocation_type label = IRQClearIRQHandler \<longrightarrow> True) \<and> (gen_invocation_type label = DomainSetSet \<longrightarrow> True) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs s; tcb_at t s; ex_nonz_cap_to t s; cte_wp_at (\<lambda>_. True) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; \<forall>x\<in>set extras. real_cte_at (snd x) s \<and> s \<turnstile> fst x \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd x) s \<and> (\<forall>y\<in>zobj_refs (fst x). ex_nonz_cap_to y s) \<and> no_cap_to_obj_dr_emp (fst x) s\<rbrakk> \<Longrightarrow> (gen_invocation_type label = TCBConfigure \<longrightarrow> (\<forall>x\<in>set extras. t \<noteq> fst (snd x))) \<and> (gen_invocation_type label = TCBSetSpace \<longrightarrow> (\<forall>x\<in>set extras. t \<noteq> fst (snd x))) proof (prove)
goal:
No subgoals!