theory ArchADT_AI

lemma get_pd_of_thread_def2:
  "get_pd_of_thread khp astate tcb_ref \<equiv>
        case khp tcb_ref of Some (TCB tcb) \<Rightarrow>
          (case tcb_vtable tcb of
             ArchObjectCap (PageDirectoryCap pd_ref (Some asid))
               \<Rightarrow> if (\<exists>p apool.
                        arm_asid_table astate (asid_high_bits_of asid) = Some p \<and>
                        khp p = Some (ArchObj (ASIDPool apool)) \<and>
                        apool (ucast (asid && mask asid_low_bits)) = Some pd_ref)
                    then pd_ref
                    else arm_global_pd astate
           | _ \<Rightarrow>  arm_global_pd astate)
        | _ \<Rightarrow>  arm_global_pd astate" apply (rule eq_reflection) apply (clarsimp simp: get_pd_of_thread_def
                 split: kernel_object.splits option.splits) apply (rename_tac tcb) apply (case_tac "tcb_vtable tcb",
         simp_all split: cap.splits arch_cap.splits kernel_object.splits
                         arch_kernel_obj.splits option.splits) apply (auto simp: VSRef_AASIDPool_in_vs_refs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. get_pd_of_thread khp astate tcb_ref \<equiv> case khp tcb_ref of None \<Rightarrow> arm_global_pd astate | Some (TCB tcb) \<Rightarrow> case tcb_vtable tcb of ArchObjectCap (PageDirectoryCap pd_ref None) \<Rightarrow> arm_global_pd astate | ArchObjectCap (PageDirectoryCap pd_ref (Some asid)) \<Rightarrow> if \<exists>p apool. arm_asid_table astate (asid_high_bits_of asid) = Some p \<and> khp p = Some (ArchObj (ASIDPool apool)) \<and> apool (UCAST(32 \<rightarrow> 10) (asid && mask local.asid_low_bits)) = Some pd_ref then pd_ref else arm_global_pd astate | ArchObjectCap _ \<Rightarrow> arm_global_pd astate | _ \<Rightarrow> arm_global_pd astate | Some _ \<Rightarrow> arm_global_pd astate proof (prove)
goal (1 subgoal):
 1. get_pd_of_thread khp astate tcb_ref = (case khp tcb_ref of None \<Rightarrow> arm_global_pd astate | Some (TCB tcb) \<Rightarrow> case tcb_vtable tcb of ArchObjectCap (PageDirectoryCap pd_ref None) \<Rightarrow> arm_global_pd astate | ArchObjectCap (PageDirectoryCap pd_ref (Some asid)) \<Rightarrow> if \<exists>p apool. arm_asid_table astate (asid_high_bits_of asid) = Some p \<and> khp p = Some (ArchObj (ASIDPool apool)) \<and> apool (UCAST(32 \<rightarrow> 10) (asid && mask local.asid_low_bits)) = Some pd_ref then pd_ref else arm_global_pd astate | ArchObjectCap _ \<Rightarrow> arm_global_pd astate | _ \<Rightarrow> arm_global_pd astate | Some _ \<Rightarrow> arm_global_pd astate) proof (prove)
goal (1 subgoal):
 1. \<And>x2. khp tcb_ref = Some (TCB x2) \<Longrightarrow> (case tcb_vtable x2 of ArchObjectCap (PageDirectoryCap pd_ref None) \<Rightarrow> arm_global_pd astate | ArchObjectCap (PageDirectoryCap pd_ref (Some asid)) \<Rightarrow> case arm_asid_table astate (asid_high_bits_of asid) of None \<Rightarrow> arm_global_pd astate | Some p \<Rightarrow> case khp p of None \<Rightarrow> arm_global_pd astate | Some (ArchObj ako) \<Rightarrow> if (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd_ref) \<in> vs_refs_arch ako then pd_ref else arm_global_pd astate | Some _ \<Rightarrow> arm_global_pd astate | ArchObjectCap _ \<Rightarrow> arm_global_pd astate | _ \<Rightarrow> arm_global_pd astate) = (case tcb_vtable x2 of ArchObjectCap (PageDirectoryCap pd_ref None) \<Rightarrow> arm_global_pd astate | ArchObjectCap (PageDirectoryCap pd_ref (Some asid)) \<Rightarrow> if \<exists>p apool. arm_asid_table astate (asid_high_bits_of asid) = Some p \<and> khp p = Some (ArchObj (ASIDPool apool)) \<and> apool (UCAST(32 \<rightarrow> 10) (asid && mask local.asid_low_bits)) = Some pd_ref then pd_ref else arm_global_pd astate | ArchObjectCap _ \<Rightarrow> arm_global_pd astate | _ \<Rightarrow> arm_global_pd astate) proof (prove)
goal (1 subgoal):
 1. \<And>tcb. khp tcb_ref = Some (TCB tcb) \<Longrightarrow> (case tcb_vtable tcb of ArchObjectCap (PageDirectoryCap pd_ref None) \<Rightarrow> arm_global_pd astate | ArchObjectCap (PageDirectoryCap pd_ref (Some asid)) \<Rightarrow> case arm_asid_table astate (asid_high_bits_of asid) of None \<Rightarrow> arm_global_pd astate | Some p \<Rightarrow> case khp p of None \<Rightarrow> arm_global_pd astate | Some (ArchObj ako) \<Rightarrow> if (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd_ref) \<in> vs_refs_arch ako then pd_ref else arm_global_pd astate | Some _ \<Rightarrow> arm_global_pd astate | ArchObjectCap _ \<Rightarrow> arm_global_pd astate | _ \<Rightarrow> arm_global_pd astate) = (case tcb_vtable tcb of ArchObjectCap (PageDirectoryCap pd_ref None) \<Rightarrow> arm_global_pd astate | ArchObjectCap (PageDirectoryCap pd_ref (Some asid)) \<Rightarrow> if \<exists>p apool. arm_asid_table astate (asid_high_bits_of asid) = Some p \<and> khp p = Some (ArchObj (ASIDPool apool)) \<and> apool (UCAST(32 \<rightarrow> 10) (asid && mask local.asid_low_bits)) = Some pd_ref then pd_ref else arm_global_pd astate | ArchObjectCap _ \<Rightarrow> arm_global_pd astate | _ \<Rightarrow> arm_global_pd astate) proof (prove)
goal (1 subgoal):
 1. \<And>tcb x12. \<lbrakk>khp tcb_ref = Some (TCB tcb); tcb_vtable tcb = ArchObjectCap x12\<rbrakk> \<Longrightarrow> \<forall>x51 x2 x2a x5. ((VSRef (x2 && mask local.asid_low_bits) (Some AASIDPool), x51) \<in> vs_refs_arch x5 \<longrightarrow> khp x2a = Some (ArchObj x5) \<longrightarrow> arm_asid_table astate (asid_high_bits_of x2) = Some x2a \<longrightarrow> (\<forall>apool. x5 = ASIDPool apool \<longrightarrow> apool (UCAST(32 \<rightarrow> 10) (x2 && mask local.asid_low_bits)) \<noteq> Some x51) \<longrightarrow> x12 = PageDirectoryCap x51 (Some x2) \<longrightarrow> x51 = arm_global_pd astate) \<and> ((VSRef (x2 && mask local.asid_low_bits) (Some AASIDPool), x51) \<notin> vs_refs_arch x5 \<longrightarrow> khp x2a = Some (ArchObj x5) \<longrightarrow> arm_asid_table astate (asid_high_bits_of x2) = Some x2a \<longrightarrow> (\<exists>apool. x5 = ASIDPool apool \<and> apool (UCAST(32 \<rightarrow> 10) (x2 && mask local.asid_low_bits)) = Some x51) \<longrightarrow> x12 = PageDirectoryCap x51 (Some x2) \<longrightarrow> arm_global_pd astate = x51) proof (prove)
goal:
No subgoals!