theory ArchArch_AI

lemma arch_pinv_st_tcb_at:
  "\<lbrace>invs and valid_arch_inv ai and ct_active and
    st_tcb_at (P and (Not \<circ> inactive) and (Not \<circ> idle)) t\<rbrace>
     arch_perform_invocation ai
   \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace>" apply (cases ai, simp_all add: arch_perform_invocation_def valid_arch_inv_def) apply (wp perform_page_table_invocation_pred_tcb_at,
            fastforce elim!: pred_tcb_weakenE) apply (wp perform_page_directory_invocation_pred_tcb_at, fastforce elim: pred_tcb_weakenE) apply (wp perform_page_invocation_pred_tcb_at, fastforce elim!: pred_tcb_weakenE) apply (wp perform_asid_control_invocation_st_tcb_at,
          fastforce elim!: pred_tcb_weakenE) apply (wp perform_asid_pool_invocation_pred_tcb_at,
         fastforce elim!: pred_tcb_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_arch_inv ai and ct_active and st_tcb_at (P and Not \<circ> inactive and Not \<circ> idle) t\<rbrace> arch_perform_invocation ai \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x1. ai = InvokePageTable x1 \<Longrightarrow> \<lbrace>invs and valid_pti x1 and ct_active and st_tcb_at (P and Not \<circ> inactive and Not \<circ> idle) t\<rbrace> liftE (do y <- perform_page_table_invocation x1;
return []
od) \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace>
 2. \<And>x2. ai = InvokePageDirectory x2 \<Longrightarrow> \<lbrace>invs and valid_pdi x2 and ct_active and st_tcb_at (P and Not \<circ> inactive and Not \<circ> idle) t\<rbrace> liftE (do y <- perform_page_directory_invocation x2;
return []
od) \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace>
 3. \<And>x3. ai = InvokePage x3 \<Longrightarrow> \<lbrace>invs and valid_page_inv x3 and ct_active and st_tcb_at (P and Not \<circ> inactive and Not \<circ> idle) t\<rbrace> liftE (perform_page_invocation x3) \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace>
 4. \<And>x4. ai = InvokeASIDControl x4 \<Longrightarrow> \<lbrace>invs and valid_aci x4 and ct_active and st_tcb_at (P and Not \<circ> inactive and Not \<circ> idle) t\<rbrace> liftE (do y <- perform_asid_control_invocation x4;
return []
od) \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace>
 5. \<And>x5. ai = InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs and valid_apinv x5 and ct_active and st_tcb_at (P and Not \<circ> inactive and Not \<circ> idle) t\<rbrace> liftE (do y <- perform_asid_pool_invocation x5;
return []
od) \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x2. ai = InvokePageDirectory x2 \<Longrightarrow> \<lbrace>invs and valid_pdi x2 and ct_active and st_tcb_at (P and Not \<circ> inactive and Not \<circ> idle) t\<rbrace> liftE (do y <- perform_page_directory_invocation x2;
return []
od) \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace>
 2. \<And>x3. ai = InvokePage x3 \<Longrightarrow> \<lbrace>invs and valid_page_inv x3 and ct_active and st_tcb_at (P and Not \<circ> inactive and Not \<circ> idle) t\<rbrace> liftE (perform_page_invocation x3) \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace>
 3. \<And>x4. ai = InvokeASIDControl x4 \<Longrightarrow> \<lbrace>invs and valid_aci x4 and ct_active and st_tcb_at (P and Not \<circ> inactive and Not \<circ> idle) t\<rbrace> liftE (do y <- perform_asid_control_invocation x4;
return []
od) \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace>
 4. \<And>x5. ai = InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs and valid_apinv x5 and ct_active and st_tcb_at (P and Not \<circ> inactive and Not \<circ> idle) t\<rbrace> liftE (do y <- perform_asid_pool_invocation x5;
return []
od) \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x3. ai = InvokePage x3 \<Longrightarrow> \<lbrace>invs and valid_page_inv x3 and ct_active and st_tcb_at (P and Not \<circ> inactive and Not \<circ> idle) t\<rbrace> liftE (perform_page_invocation x3) \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace>
 2. \<And>x4. ai = InvokeASIDControl x4 \<Longrightarrow> \<lbrace>invs and valid_aci x4 and ct_active and st_tcb_at (P and Not \<circ> inactive and Not \<circ> idle) t\<rbrace> liftE (do y <- perform_asid_control_invocation x4;
return []
od) \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace>
 3. \<And>x5. ai = InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs and valid_apinv x5 and ct_active and st_tcb_at (P and Not \<circ> inactive and Not \<circ> idle) t\<rbrace> liftE (do y <- perform_asid_pool_invocation x5;
return []
od) \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x4. ai = InvokeASIDControl x4 \<Longrightarrow> \<lbrace>invs and valid_aci x4 and ct_active and st_tcb_at (P and Not \<circ> inactive and Not \<circ> idle) t\<rbrace> liftE (do y <- perform_asid_control_invocation x4;
return []
od) \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace>
 2. \<And>x5. ai = InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs and valid_apinv x5 and ct_active and st_tcb_at (P and Not \<circ> inactive and Not \<circ> idle) t\<rbrace> liftE (do y <- perform_asid_pool_invocation x5;
return []
od) \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x5. ai = InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs and valid_apinv x5 and ct_active and st_tcb_at (P and Not \<circ> inactive and Not \<circ> idle) t\<rbrace> liftE (do y <- perform_asid_pool_invocation x5;
return []
od) \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace> proof (prove)
goal:
No subgoals!