theory Arch_R

lemma invokeArch_tcb_at':
  "\<lbrace>invs' and valid_arch_inv' ai and ct_active' and st_tcb_at' active' p\<rbrace>
     Arch.performInvocation ai
   \<lbrace>\<lambda>rv. tcb_at' p\<rbrace>" apply (simp add: ARM_H.performInvocation_def performARMMMUInvocation_def) apply (cases ai, simp_all) apply (wp, clarsimp simp: pred_tcb_at') apply (wp, clarsimp simp: pred_tcb_at') apply (wp, clarsimp simp: st_tcb_strg'[rule_format]) apply (wp performASIDControlInvocation_tcb_at', clarsimp simp: valid_arch_inv'_def) apply (wp, clarsimp simp: pred_tcb_at') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and valid_arch_inv' ai and ct_active' and st_tcb_at' active' p\<rbrace> Arch.performInvocation ai \<lbrace>\<lambda>rv. tcb_at' p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and valid_arch_inv' ai and ct_active' and st_tcb_at' active' p\<rbrace> liftE (case ai of invocation.InvokePageTable oper \<Rightarrow> do performPageTableInvocation oper;
return []
od | invocation.InvokePageDirectory oper \<Rightarrow> do performPageDirectoryInvocation oper;
return []
od | invocation.InvokePage x \<Rightarrow> performPageInvocation x | invocation.InvokeASIDControl oper \<Rightarrow> do performASIDControlInvocation oper;
return []
od | invocation.InvokeASIDPool oper \<Rightarrow> do performASIDPoolInvocation oper;
return []
od) \<lbrace>\<lambda>rv. tcb_at' p\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x1. ai = invocation.InvokePageTable x1 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePageTable x1) and ct_active' and st_tcb_at' active' p\<rbrace> liftE (do y <- performPageTableInvocation x1;
return []
od) \<lbrace>\<lambda>rv. tcb_at' p\<rbrace>
 2. \<And>x2. ai = invocation.InvokePageDirectory x2 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePageDirectory x2) and ct_active' and st_tcb_at' active' p\<rbrace> liftE (do y <- performPageDirectoryInvocation x2;
return []
od) \<lbrace>\<lambda>rv. tcb_at' p\<rbrace>
 3. \<And>x3. ai = invocation.InvokePage x3 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePage x3) and ct_active' and st_tcb_at' active' p\<rbrace> liftE (performPageInvocation x3) \<lbrace>\<lambda>rv. tcb_at' p\<rbrace>
 4. \<And>x4. ai = invocation.InvokeASIDControl x4 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDControl x4) and ct_active' and st_tcb_at' active' p\<rbrace> liftE (do y <- performASIDControlInvocation x4;
return []
od) \<lbrace>\<lambda>rv. tcb_at' p\<rbrace>
 5. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>rv. tcb_at' p\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x2. ai = invocation.InvokePageDirectory x2 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePageDirectory x2) and ct_active' and st_tcb_at' active' p\<rbrace> liftE (do y <- performPageDirectoryInvocation x2;
return []
od) \<lbrace>\<lambda>rv. tcb_at' p\<rbrace>
 2. \<And>x3. ai = invocation.InvokePage x3 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePage x3) and ct_active' and st_tcb_at' active' p\<rbrace> liftE (performPageInvocation x3) \<lbrace>\<lambda>rv. tcb_at' p\<rbrace>
 3. \<And>x4. ai = invocation.InvokeASIDControl x4 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDControl x4) and ct_active' and st_tcb_at' active' p\<rbrace> liftE (do y <- performASIDControlInvocation x4;
return []
od) \<lbrace>\<lambda>rv. tcb_at' p\<rbrace>
 4. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>rv. tcb_at' p\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x3. ai = invocation.InvokePage x3 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePage x3) and ct_active' and st_tcb_at' active' p\<rbrace> liftE (performPageInvocation x3) \<lbrace>\<lambda>rv. tcb_at' p\<rbrace>
 2. \<And>x4. ai = invocation.InvokeASIDControl x4 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDControl x4) and ct_active' and st_tcb_at' active' p\<rbrace> liftE (do y <- performASIDControlInvocation x4;
return []
od) \<lbrace>\<lambda>rv. tcb_at' p\<rbrace>
 3. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>rv. tcb_at' p\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x4. ai = invocation.InvokeASIDControl x4 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDControl x4) and ct_active' and st_tcb_at' active' p\<rbrace> liftE (do y <- performASIDControlInvocation x4;
return []
od) \<lbrace>\<lambda>rv. tcb_at' p\<rbrace>
 2. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>rv. tcb_at' p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>rv. tcb_at' p\<rbrace> proof (prove)
goal:
No subgoals!