theory PageTableDuplicates

lemma performInvocation_valid_duplicates'[wp]:
  "\<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s) \<and> invs' s \<and> sch_act_simple s
    \<and> valid_invocation' i s \<and> ct_active' s\<rbrace>
  RetypeDecls_H.performInvocation isBlocking isCall i
  \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>" apply (clarsimp simp: performInvocation_def) apply (simp add:ct_in_state'_def) apply (rule hoare_name_pre_state) apply (rule hoare_pre) apply wpc apply (wp performArchInvocation_valid_duplicates' |simp)+ apply (cases i) apply (clarsimp simp: simple_sane_strg sch_act_simple_def
                    ct_in_state'_def ct_active_runnable'[unfolded ct_in_state'_def]
                  | wp tcbinv_invs' arch_performInvocation_invs'
                  | rule conjI | erule active_ex_cap')+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s) \<and> invs' s \<and> sch_act_simple s \<and> valid_invocation' i s \<and> ct_active' s\<rbrace> global.performInvocation isBlocking isCall i \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s) \<and> invs' s \<and> sch_act_simple s \<and> valid_invocation' i s \<and> ct_active' s\<rbrace> case i of Invocations_H.invocation.InvokeUntyped invok \<Rightarrow> doE invokeUntyped invok;
returnOk $ []
odE | Invocations_H.invocation.InvokeEndpoint ep badge canGrant canGrantReply \<Rightarrow> withoutPreemption $ do thread <- getCurThread;
sendIPC isBlocking isCall badge canGrant canGrantReply thread ep;
return $ []
od | Invocations_H.invocation.InvokeNotification ep badge \<Rightarrow> doE withoutPreemption $ sendSignal ep badge;
returnOk $ []
odE | Invocations_H.invocation.InvokeReply thread slot canGrant \<Rightarrow> withoutPreemption $ do sender <- getCurThread;
doReplyTransfer sender thread slot canGrant;
return $ []
od | Invocations_H.invocation.InvokeDomain thread domain \<Rightarrow> withoutPreemption $ do setDomain thread domain;
return $ []
od | Invocations_H.invocation.InvokeTCB invok \<Rightarrow> invokeTCB invok | Invocations_H.invocation.InvokeCNode invok \<Rightarrow> doE invokeCNode invok;
returnOk $ []
odE | Invocations_H.invocation.InvokeIRQControl invok \<Rightarrow> doE global.performIRQControl invok;
returnOk $ []
odE | Invocations_H.invocation.InvokeIRQHandler invok \<Rightarrow> doE withoutPreemption $ InterruptDecls_H.invokeIRQHandler invok;
returnOk $ []
odE | Invocations_H.invocation.InvokeArchObject invok \<Rightarrow> Arch.performInvocation invok \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s) \<and> invs' s \<and> sch_act_simple s \<and> valid_invocation' i s \<and> st_tcb_at' active' (ksCurThread s) s\<rbrace> case i of Invocations_H.invocation.InvokeUntyped invok \<Rightarrow> doE invokeUntyped invok;
returnOk $ []
odE | Invocations_H.invocation.InvokeEndpoint ep badge canGrant canGrantReply \<Rightarrow> withoutPreemption $ do thread <- getCurThread;
sendIPC isBlocking isCall badge canGrant canGrantReply thread ep;
return $ []
od | Invocations_H.invocation.InvokeNotification ep badge \<Rightarrow> doE withoutPreemption $ sendSignal ep badge;
returnOk $ []
odE | Invocations_H.invocation.InvokeReply thread slot canGrant \<Rightarrow> withoutPreemption $ do sender <- getCurThread;
doReplyTransfer sender thread slot canGrant;
return $ []
od | Invocations_H.invocation.InvokeDomain thread domain \<Rightarrow> withoutPreemption $ do setDomain thread domain;
return $ []
od | Invocations_H.invocation.InvokeTCB invok \<Rightarrow> invokeTCB invok | Invocations_H.invocation.InvokeCNode invok \<Rightarrow> doE invokeCNode invok;
returnOk $ []
odE | Invocations_H.invocation.InvokeIRQControl invok \<Rightarrow> doE global.performIRQControl invok;
returnOk $ []
odE | Invocations_H.invocation.InvokeIRQHandler invok \<Rightarrow> doE withoutPreemption $ InterruptDecls_H.invokeIRQHandler invok;
returnOk $ []
odE | Invocations_H.invocation.InvokeArchObject invok \<Rightarrow> Arch.performInvocation invok \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. vs_valid_duplicates' (ksPSpace s) \<and> invs' s \<and> sch_act_simple s \<and> valid_invocation' i s \<and> st_tcb_at' active' (ksCurThread s) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> case i of Invocations_H.invocation.InvokeUntyped invok \<Rightarrow> doE invokeUntyped invok;
returnOk $ []
odE | Invocations_H.invocation.InvokeEndpoint ep badge canGrant canGrantReply \<Rightarrow> withoutPreemption $ do thread <- getCurThread;
sendIPC isBlocking isCall badge canGrant canGrantReply thread ep;
return $ []
od | Invocations_H.invocation.InvokeNotification ep badge \<Rightarrow> doE withoutPreemption $ sendSignal ep badge;
returnOk $ []
odE | Invocations_H.invocation.InvokeReply thread slot canGrant \<Rightarrow> withoutPreemption $ do sender <- getCurThread;
doReplyTransfer sender thread slot canGrant;
return $ []
od | Invocations_H.invocation.InvokeDomain thread domain \<Rightarrow> withoutPreemption $ do setDomain thread domain;
return $ []
od | Invocations_H.invocation.InvokeTCB invok \<Rightarrow> invokeTCB invok | Invocations_H.invocation.InvokeCNode invok \<Rightarrow> doE invokeCNode invok;
returnOk $ []
odE | Invocations_H.invocation.InvokeIRQControl invok \<Rightarrow> doE global.performIRQControl invok;
returnOk $ []
odE | Invocations_H.invocation.InvokeIRQHandler invok \<Rightarrow> doE withoutPreemption $ InterruptDecls_H.invokeIRQHandler invok;
returnOk $ []
odE | Invocations_H.invocation.InvokeArchObject invok \<Rightarrow> Arch.performInvocation invok \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. vs_valid_duplicates' (ksPSpace s) \<and> invs' s \<and> sch_act_simple s \<and> valid_invocation' i s \<and> st_tcb_at' active' (ksCurThread s) s \<Longrightarrow> \<lbrace>?Q2 s\<rbrace> case i of Invocations_H.invocation.InvokeUntyped invok \<Rightarrow> doE invokeUntyped invok;
returnOk $ []
odE | Invocations_H.invocation.InvokeEndpoint ep badge canGrant canGrantReply \<Rightarrow> withoutPreemption $ do thread <- getCurThread;
sendIPC isBlocking isCall badge canGrant canGrantReply thread ep;
return $ []
od | Invocations_H.invocation.InvokeNotification ep badge \<Rightarrow> doE withoutPreemption $ sendSignal ep badge;
returnOk $ []
odE | Invocations_H.invocation.InvokeReply thread slot canGrant \<Rightarrow> withoutPreemption $ do sender <- getCurThread;
doReplyTransfer sender thread slot canGrant;
return $ []
od | Invocations_H.invocation.InvokeDomain thread domain \<Rightarrow> withoutPreemption $ do setDomain thread domain;
return $ []
od | Invocations_H.invocation.InvokeTCB invok \<Rightarrow> invokeTCB invok | Invocations_H.invocation.InvokeCNode invok \<Rightarrow> doE invokeCNode invok;
returnOk $ []
odE | Invocations_H.invocation.InvokeIRQControl invok \<Rightarrow> doE global.performIRQControl invok;
returnOk $ []
odE | Invocations_H.invocation.InvokeIRQHandler invok \<Rightarrow> doE withoutPreemption $ InterruptDecls_H.invokeIRQHandler invok;
returnOk $ []
odE | Invocations_H.invocation.InvokeArchObject invok \<Rightarrow> Arch.performInvocation invok \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>s sa. \<lbrakk>vs_valid_duplicates' (ksPSpace s) \<and> invs' s \<and> sch_act_simple s \<and> valid_invocation' i s \<and> st_tcb_at' active' (ksCurThread s) s; s = sa\<rbrakk> \<Longrightarrow> ?Q2 s sa proof (prove)
goal (11 subgoals):
 1. \<And>s x1. \<lbrakk>vs_valid_duplicates' (ksPSpace s) \<and> invs' s \<and> sch_act_simple s \<and> valid_invocation' i s \<and> st_tcb_at' active' (ksCurThread s) s; i = Invocations_H.invocation.InvokeUntyped x1\<rbrakk> \<Longrightarrow> \<lbrace>?R45 s x1\<rbrace> doE invokeUntyped x1;
returnOk $ []
odE \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>s x21 x22 x23 x24. \<lbrakk>vs_valid_duplicates' (ksPSpace s) \<and> invs' s \<and> sch_act_simple s \<and> valid_invocation' i s \<and> st_tcb_at' active' (ksCurThread s) s; i = Invocations_H.invocation.InvokeEndpoint x21 x22 x23 x24\<rbrakk> \<Longrightarrow> \<lbrace>?R46 s x21 x22 x23 x24\<rbrace> withoutPreemption $ do thread <- getCurThread;
sendIPC isBlocking isCall x22 x23 x24 thread x21;
return $ []
od \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>s x31 x32. \<lbrakk>vs_valid_duplicates' (ksPSpace s) \<and> invs' s \<and> sch_act_simple s \<and> valid_invocation' i s \<and> st_tcb_at' active' (ksCurThread s) s; i = Invocations_H.invocation.InvokeNotification x31 x32\<rbrakk> \<Longrightarrow> \<lbrace>?R47 s x31 x32\<rbrace> doE withoutPreemption $ sendSignal x31 x32;
returnOk $ []
odE \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>s x41 x42 x43. \<lbrakk>vs_valid_duplicates' (ksPSpace s) \<and> invs' s \<and> sch_act_simple s \<and> valid_invocation' i s \<and> st_tcb_at' active' (ksCurThread s) s; i = Invocations_H.invocation.InvokeReply x41 x42 x43\<rbrakk> \<Longrightarrow> \<lbrace>?R48 s x41 x42 x43\<rbrace> withoutPreemption $ do sender <- getCurThread;
doReplyTransfer sender x41 x42 x43;
return $ []
od \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>s x51 x52. \<lbrakk>vs_valid_duplicates' (ksPSpace s) \<and> invs' s \<and> sch_act_simple s \<and> valid_invocation' i s \<and> st_tcb_at' active' (ksCurThread s) s; i = Invocations_H.invocation.InvokeDomain x51 x52\<rbrakk> \<Longrightarrow> \<lbrace>?R49 s x51 x52\<rbrace> withoutPreemption $ do setDomain x51 x52;
return $ []
od \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 6. \<And>s x6. \<lbrakk>vs_valid_duplicates' (ksPSpace s) \<and> invs' s \<and> sch_act_simple s \<and> valid_invocation' i s \<and> st_tcb_at' active' (ksCurThread s) s; i = Invocations_H.invocation.InvokeTCB x6\<rbrakk> \<Longrightarrow> \<lbrace>?R50 s x6\<rbrace> invokeTCB x6 \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 7. \<And>s x7. \<lbrakk>vs_valid_duplicates' (ksPSpace s) \<and> invs' s \<and> sch_act_simple s \<and> valid_invocation' i s \<and> st_tcb_at' active' (ksCurThread s) s; i = Invocations_H.invocation.InvokeCNode x7\<rbrakk> \<Longrightarrow> \<lbrace>?R51 s x7\<rbrace> doE invokeCNode x7;
returnOk $ []
odE \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 8. \<And>s x8. \<lbrakk>vs_valid_duplicates' (ksPSpace s) \<and> invs' s \<and> sch_act_simple s \<and> valid_invocation' i s \<and> st_tcb_at' active' (ksCurThread s) s; i = Invocations_H.invocation.InvokeIRQControl x8\<rbrakk> \<Longrightarrow> \<lbrace>?R52 s x8\<rbrace> doE global.performIRQControl x8;
returnOk $ []
odE \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 9. \<And>s x9. \<lbrakk>vs_valid_duplicates' (ksPSpace s) \<and> invs' s \<and> sch_act_simple s \<and> valid_invocation' i s \<and> st_tcb_at' active' (ksCurThread s) s; i = Invocations_H.invocation.InvokeIRQHandler x9\<rbrakk> \<Longrightarrow> \<lbrace>?R53 s x9\<rbrace> doE withoutPreemption $ InterruptDecls_H.invokeIRQHandler x9;
returnOk $ []
odE \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 10. \<And>s x10. \<lbrakk>vs_valid_duplicates' (ksPSpace s) \<and> invs' s \<and> sch_act_simple s \<and> valid_invocation' i s \<and> st_tcb_at' active' (ksCurThread s) s; i = Invocations_H.invocation.InvokeArchObject x10\<rbrakk> \<Longrightarrow> \<lbrace>?R54 s x10\<rbrace> Arch.performInvocation x10 \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
A total of 11 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>vs_valid_duplicates' (ksPSpace sa) \<and> invs' sa \<and> sch_act_simple sa \<and> valid_invocation' i sa \<and> st_tcb_at' active' (ksCurThread sa) sa; s = sa\<rbrakk> \<Longrightarrow> (\<forall>x. i = Invocations_H.invocation.InvokeUntyped x \<longrightarrow> valid_untyped_inv' x sa \<and> ct_active' sa) \<and> (\<forall>x. i = Invocations_H.invocation.InvokeTCB x \<longrightarrow> ct_in_state' runnable' sa \<and> tcb_inv_wf' x sa) \<and> (\<forall>x. i = Invocations_H.invocation.InvokeCNode x \<longrightarrow> valid_cnode_inv' x sa) \<and> (\<forall>x. i = Invocations_H.invocation.InvokeArchObject x \<longrightarrow> valid_arch_inv' x sa \<and> ct_active' sa \<and> st_tcb_at' active' (?p206 sa x) sa) proof (prove)
goal (10 subgoals):
 1. \<And>s sa x1. \<lbrakk>vs_valid_duplicates' (ksPSpace sa) \<and> invs' sa \<and> sch_act_simple sa \<and> valid_invocation' i sa \<and> st_tcb_at' active' (ksCurThread sa) sa; s = sa; i = Invocations_H.invocation.InvokeUntyped x1\<rbrakk> \<Longrightarrow> (\<forall>x. i = Invocations_H.invocation.InvokeUntyped x \<longrightarrow> valid_untyped_inv' x sa \<and> ct_active' sa) \<and> (\<forall>x. i = Invocations_H.invocation.InvokeTCB x \<longrightarrow> ct_in_state' runnable' sa \<and> tcb_inv_wf' x sa) \<and> (\<forall>x. i = Invocations_H.invocation.InvokeCNode x \<longrightarrow> valid_cnode_inv' x sa) \<and> (\<forall>x. i = Invocations_H.invocation.InvokeArchObject x \<longrightarrow> valid_arch_inv' x sa \<and> ct_active' sa \<and> st_tcb_at' active' (?p206 sa x) sa)
 2. \<And>s sa x21 x22 x23 x24. \<lbrakk>vs_valid_duplicates' (ksPSpace sa) \<and> invs' sa \<and> sch_act_simple sa \<and> valid_invocation' i sa \<and> st_tcb_at' active' (ksCurThread sa) sa; s = sa; i = Invocations_H.invocation.InvokeEndpoint x21 x22 x23 x24\<rbrakk> \<Longrightarrow> (\<forall>x. i = Invocations_H.invocation.InvokeUntyped x \<longrightarrow> valid_untyped_inv' x sa \<and> ct_active' sa) \<and> (\<forall>x. i = Invocations_H.invocation.InvokeTCB x \<longrightarrow> ct_in_state' runnable' sa \<and> tcb_inv_wf' x sa) \<and> (\<forall>x. i = Invocations_H.invocation.InvokeCNode x \<longrightarrow> valid_cnode_inv' x sa) \<and> (\<forall>x. i = Invocations_H.invocation.InvokeArchObject x \<longrightarrow> valid_arch_inv' x sa \<and> ct_active' sa \<and> st_tcb_at' active' (?p206 sa x) sa)
 3. \<And>s sa x31 x32. \<lbrakk>vs_valid_duplicates' (ksPSpace sa) \<and> invs' sa \<and> sch_act_simple sa \<and> valid_invocation' i sa \<and> st_tcb_at' active' (ksCurThread sa) sa; s = sa; i = Invocations_H.invocation.InvokeNotification x31 x32\<rbrakk> \<Longrightarrow> (\<forall>x. i = Invocations_H.invocation.InvokeUntyped x \<longrightarrow> valid_untyped_inv' x sa \<and> ct_active' sa) \<and> (\<forall>x. i = Invocations_H.invocation.InvokeTCB x \<longrightarrow> ct_in_state' runnable' sa \<and> tcb_inv_wf' x sa) \<and> (\<forall>x. i = Invocations_H.invocation.InvokeCNode x \<longrightarrow> valid_cnode_inv' x sa) \<and> (\<forall>x. i = Invocations_H.invocation.InvokeArchObject x \<longrightarrow> valid_arch_inv' x sa \<and> ct_active' sa \<and> st_tcb_at' active' (?p206 sa x) sa)
 4. \<And>s sa x41 x42 x43. \<lbrakk>vs_valid_duplicates' (ksPSpace sa) \<and> invs' sa \<and> sch_act_simple sa \<and> valid_invocation' i sa \<and> st_tcb_at' active' (ksCurThread sa) sa; s = sa; i = Invocations_H.invocation.InvokeReply x41 x42 x43\<rbrakk> \<Longrightarrow> (\<forall>x. i = Invocations_H.invocation.InvokeUntyped x \<longrightarrow> valid_untyped_inv' x sa \<and> ct_active' sa) \<and> (\<forall>x. i = Invocations_H.invocation.InvokeTCB x \<longrightarrow> ct_in_state' runnable' sa \<and> tcb_inv_wf' x sa) \<and> (\<forall>x. i = Invocations_H.invocation.InvokeCNode x \<longrightarrow> valid_cnode_inv' x sa) \<and> (\<forall>x. i = Invocations_H.invocation.InvokeArchObject x \<longrightarrow> valid_arch_inv' x sa \<and> ct_active' sa \<and> st_tcb_at' active' (?p206 sa x) sa)
 5. \<And>s sa x51 x52. \<lbrakk>vs_valid_duplicates' (ksPSpace sa) \<and> invs' sa \<and> sch_act_simple sa \<and> valid_invocation' i sa \<and> st_tcb_at' active' (ksCurThread sa) sa; s = sa; i = Invocations_H.invocation.InvokeDomain x51 x52\<rbrakk> \<Longrightarrow> (\<forall>x. i = Invocations_H.invocation.InvokeUntyped x \<longrightarrow> valid_untyped_inv' x sa \<and> ct_active' sa) \<and> (\<forall>x. i = Invocations_H.invocation.InvokeTCB x \<longrightarrow> ct_in_state' runnable' sa \<and> tcb_inv_wf' x sa) \<and> (\<forall>x. i = Invocations_H.invocation.InvokeCNode x \<longrightarrow> valid_cnode_inv' x sa) \<and> (\<forall>x. i = Invocations_H.invocation.InvokeArchObject x \<longrightarrow> valid_arch_inv' x sa \<and> ct_active' sa \<and> st_tcb_at' active' (?p206 sa x) sa)
 6. \<And>s sa x6. \<lbrakk>vs_valid_duplicates' (ksPSpace sa) \<and> invs' sa \<and> sch_act_simple sa \<and> valid_invocation' i sa \<and> st_tcb_at' active' (ksCurThread sa) sa; s = sa; i = Invocations_H.invocation.InvokeTCB x6\<rbrakk> \<Longrightarrow> (\<forall>x. i = Invocations_H.invocation.InvokeUntyped x \<longrightarrow> valid_untyped_inv' x sa \<and> ct_active' sa) \<and> (\<forall>x. i = Invocations_H.invocation.InvokeTCB x \<longrightarrow> ct_in_state' runnable' sa \<and> tcb_inv_wf' x sa) \<and> (\<forall>x. i = Invocations_H.invocation.InvokeCNode x \<longrightarrow> valid_cnode_inv' x sa) \<and> (\<forall>x. i = Invocations_H.invocation.InvokeArchObject x \<longrightarrow> valid_arch_inv' x sa \<and> ct_active' sa \<and> st_tcb_at' active' (?p206 sa x) sa)
 7. \<And>s sa x7. \<lbrakk>vs_valid_duplicates' (ksPSpace sa) \<and> invs' sa \<and> sch_act_simple sa \<and> valid_invocation' i sa \<and> st_tcb_at' active' (ksCurThread sa) sa; s = sa; i = Invocations_H.invocation.InvokeCNode x7\<rbrakk> \<Longrightarrow> (\<forall>x. i = Invocations_H.invocation.InvokeUntyped x \<longrightarrow> valid_untyped_inv' x sa \<and> ct_active' sa) \<and> (\<forall>x. i = Invocations_H.invocation.InvokeTCB x \<longrightarrow> ct_in_state' runnable' sa \<and> tcb_inv_wf' x sa) \<and> (\<forall>x. i = Invocations_H.invocation.InvokeCNode x \<longrightarrow> valid_cnode_inv' x sa) \<and> (\<forall>x. i = Invocations_H.invocation.InvokeArchObject x \<longrightarrow> valid_arch_inv' x sa \<and> ct_active' sa \<and> st_tcb_at' active' (?p206 sa x) sa)
 8. \<And>s sa x8. \<lbrakk>vs_valid_duplicates' (ksPSpace sa) \<and> invs' sa \<and> sch_act_simple sa \<and> valid_invocation' i sa \<and> st_tcb_at' active' (ksCurThread sa) sa; s = sa; i = Invocations_H.invocation.InvokeIRQControl x8\<rbrakk> \<Longrightarrow> (\<forall>x. i = Invocations_H.invocation.InvokeUntyped x \<longrightarrow> valid_untyped_inv' x sa \<and> ct_active' sa) \<and> (\<forall>x. i = Invocations_H.invocation.InvokeTCB x \<longrightarrow> ct_in_state' runnable' sa \<and> tcb_inv_wf' x sa) \<and> (\<forall>x. i = Invocations_H.invocation.InvokeCNode x \<longrightarrow> valid_cnode_inv' x sa) \<and> (\<forall>x. i = Invocations_H.invocation.InvokeArchObject x \<longrightarrow> valid_arch_inv' x sa \<and> ct_active' sa \<and> st_tcb_at' active' (?p206 sa x) sa)
 9. \<And>s sa x9. \<lbrakk>vs_valid_duplicates' (ksPSpace sa) \<and> invs' sa \<and> sch_act_simple sa \<and> valid_invocation' i sa \<and> st_tcb_at' active' (ksCurThread sa) sa; s = sa; i = Invocations_H.invocation.InvokeIRQHandler x9\<rbrakk> \<Longrightarrow> (\<forall>x. i = Invocations_H.invocation.InvokeUntyped x \<longrightarrow> valid_untyped_inv' x sa \<and> ct_active' sa) \<and> (\<forall>x. i = Invocations_H.invocation.InvokeTCB x \<longrightarrow> ct_in_state' runnable' sa \<and> tcb_inv_wf' x sa) \<and> (\<forall>x. i = Invocations_H.invocation.InvokeCNode x \<longrightarrow> valid_cnode_inv' x sa) \<and> (\<forall>x. i = Invocations_H.invocation.InvokeArchObject x \<longrightarrow> valid_arch_inv' x sa \<and> ct_active' sa \<and> st_tcb_at' active' (?p206 sa x) sa)
 10. \<And>s sa x10. \<lbrakk>vs_valid_duplicates' (ksPSpace sa) \<and> invs' sa \<and> sch_act_simple sa \<and> valid_invocation' i sa \<and> st_tcb_at' active' (ksCurThread sa) sa; s = sa; i = Invocations_H.invocation.InvokeArchObject x10\<rbrakk> \<Longrightarrow> (\<forall>x. i = Invocations_H.invocation.InvokeUntyped x \<longrightarrow> valid_untyped_inv' x sa \<and> ct_active' sa) \<and> (\<forall>x. i = Invocations_H.invocation.InvokeTCB x \<longrightarrow> ct_in_state' runnable' sa \<and> tcb_inv_wf' x sa) \<and> (\<forall>x. i = Invocations_H.invocation.InvokeCNode x \<longrightarrow> valid_cnode_inv' x sa) \<and> (\<forall>x. i = Invocations_H.invocation.InvokeArchObject x \<longrightarrow> valid_arch_inv' x sa \<and> ct_active' sa \<and> st_tcb_at' active' (?p206 sa x) sa) proof (prove)
goal (1 subgoal):
 1. \<And>sa x10. \<lbrakk>i = Invocations_H.invocation.InvokeArchObject x10; vs_valid_duplicates' (ksPSpace sa); invs' sa; ksSchedulerAction sa = ResumeCurrentThread \<or> ksSchedulerAction sa = ChooseNewThread; valid_arch_inv' x10 sa; st_tcb_at' active' (ksCurThread sa) sa\<rbrakk> \<Longrightarrow> st_tcb_at' active' (?p206 sa x10) sa proof (prove)
goal:
No subgoals!