theory Detype_R

lemma ksASIDMapSafeI:
  "\<lbrakk> (s,s') \<in> state_relation; invs s; pspace_aligned' s' \<and> pspace_distinct' s' \<rbrakk>
  \<Longrightarrow> ksASIDMapSafe s'" apply (clarsimp simp: ksASIDMapSafe_def) apply (subgoal_tac "valid_asid_map s") prefer 2 apply fastforce apply (clarsimp simp: valid_asid_map_def graph_of_def) apply (subgoal_tac "arm_asid_map (arch_state s) asid = Some (hw_asid, pd)") prefer 2 apply (clarsimp simp: state_relation_def arch_state_relation_def) apply (erule allE)+ apply (erule (1) impE) apply clarsimp apply (drule find_pd_for_asid_eq_helper) apply fastforce apply assumption apply fastforce apply clarsimp apply (rule pspace_relation_pd) apply (fastforce simp: state_relation_def) apply fastforce apply assumption apply assumption apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s' \<and> pspace_distinct' s'\<rbrakk> \<Longrightarrow> ksASIDMapSafe s' proof (prove)
goal (1 subgoal):
 1. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd)\<rbrakk> \<Longrightarrow> page_directory_at' pd s' proof (prove)
goal (2 subgoals):
 1. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); valid_asid_map s\<rbrakk> \<Longrightarrow> page_directory_at' pd s'
 2. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd)\<rbrakk> \<Longrightarrow> valid_asid_map s proof (prove)
goal (2 subgoals):
 1. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd)\<rbrakk> \<Longrightarrow> valid_asid_map s
 2. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); valid_asid_map s\<rbrakk> \<Longrightarrow> page_directory_at' pd s' proof (prove)
goal (1 subgoal):
 1. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); valid_asid_map s\<rbrakk> \<Longrightarrow> page_directory_at' pd s' proof (prove)
goal (1 subgoal):
 1. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; \<forall>a aa b. arm_asid_map (arch_state s) a = Some (aa, b) \<longrightarrow> vspace_at_asid a b s \<and> a \<noteq> 0\<rbrakk> \<Longrightarrow> page_directory_at' pd s' proof (prove)
goal (2 subgoals):
 1. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; \<forall>a aa b. arm_asid_map (arch_state s) a = Some (aa, b) \<longrightarrow> vspace_at_asid a b s \<and> a \<noteq> 0; arm_asid_map (arch_state s) asid = Some (hw_asid, pd)\<rbrakk> \<Longrightarrow> page_directory_at' pd s'
 2. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; \<forall>a aa b. arm_asid_map (arch_state s) a = Some (aa, b) \<longrightarrow> vspace_at_asid a b s \<and> a \<noteq> 0\<rbrakk> \<Longrightarrow> arm_asid_map (arch_state s) asid = Some (hw_asid, pd) proof (prove)
goal (2 subgoals):
 1. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; \<forall>a aa b. arm_asid_map (arch_state s) a = Some (aa, b) \<longrightarrow> vspace_at_asid a b s \<and> a \<noteq> 0\<rbrakk> \<Longrightarrow> arm_asid_map (arch_state s) asid = Some (hw_asid, pd)
 2. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; \<forall>a aa b. arm_asid_map (arch_state s) a = Some (aa, b) \<longrightarrow> vspace_at_asid a b s \<and> a \<noteq> 0; arm_asid_map (arch_state s) asid = Some (hw_asid, pd)\<rbrakk> \<Longrightarrow> page_directory_at' pd s' proof (prove)
goal (1 subgoal):
 1. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; \<forall>a aa b. arm_asid_map (arch_state s) a = Some (aa, b) \<longrightarrow> vspace_at_asid a b s \<and> a \<noteq> 0; arm_asid_map (arch_state s) asid = Some (hw_asid, pd)\<rbrakk> \<Longrightarrow> page_directory_at' pd s' proof (prove)
goal (1 subgoal):
 1. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; arm_asid_map (arch_state s) asid = Some (hw_asid, pd); arm_asid_map (arch_state s) (?a17 asid hw_asid pd) = Some (?a19 asid hw_asid pd, ?b21 asid hw_asid pd) \<longrightarrow> vspace_at_asid (?a17 asid hw_asid pd) (?b21 asid hw_asid pd) s \<and> ?a17 asid hw_asid pd \<noteq> 0\<rbrakk> \<Longrightarrow> page_directory_at' pd s' proof (prove)
goal (1 subgoal):
 1. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; arm_asid_map (arch_state s) asid = Some (hw_asid, pd); vspace_at_asid asid pd s \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> page_directory_at' pd s' proof (prove)
goal (1 subgoal):
 1. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; arm_asid_map (arch_state s) asid = Some (hw_asid, pd); vspace_at_asid asid pd s; asid \<noteq> 0\<rbrakk> \<Longrightarrow> page_directory_at' pd s' proof (prove)
goal (4 subgoals):
 1. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; arm_asid_map (arch_state s) asid = Some (hw_asid, pd); asid \<noteq> 0\<rbrakk> \<Longrightarrow> valid_vspace_objs s
 2. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; arm_asid_map (arch_state s) asid = Some (hw_asid, pd); asid \<noteq> 0\<rbrakk> \<Longrightarrow> asid \<noteq> 0
 3. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; arm_asid_map (arch_state s) asid = Some (hw_asid, pd); asid \<noteq> 0\<rbrakk> \<Longrightarrow> pspace_aligned s
 4. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; arm_asid_map (arch_state s) asid = Some (hw_asid, pd); asid \<noteq> 0; find_pd_for_asid asid s = returnOk pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pdBits\<rbrakk> \<Longrightarrow> page_directory_at' pd s' proof (prove)
goal (3 subgoals):
 1. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; arm_asid_map (arch_state s) asid = Some (hw_asid, pd); asid \<noteq> 0\<rbrakk> \<Longrightarrow> asid \<noteq> 0
 2. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; arm_asid_map (arch_state s) asid = Some (hw_asid, pd); asid \<noteq> 0\<rbrakk> \<Longrightarrow> pspace_aligned s
 3. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; arm_asid_map (arch_state s) asid = Some (hw_asid, pd); asid \<noteq> 0; find_pd_for_asid asid s = returnOk pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pdBits\<rbrakk> \<Longrightarrow> page_directory_at' pd s' proof (prove)
goal (2 subgoals):
 1. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; arm_asid_map (arch_state s) asid = Some (hw_asid, pd); asid \<noteq> 0\<rbrakk> \<Longrightarrow> pspace_aligned s
 2. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; arm_asid_map (arch_state s) asid = Some (hw_asid, pd); asid \<noteq> 0; find_pd_for_asid asid s = returnOk pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pdBits\<rbrakk> \<Longrightarrow> page_directory_at' pd s' proof (prove)
goal (1 subgoal):
 1. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; arm_asid_map (arch_state s) asid = Some (hw_asid, pd); asid \<noteq> 0; find_pd_for_asid asid s = returnOk pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pdBits\<rbrakk> \<Longrightarrow> page_directory_at' pd s' proof (prove)
goal (1 subgoal):
 1. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; arm_asid_map (arch_state s) asid = Some (hw_asid, pd); asid \<noteq> 0; find_pd_for_asid asid s = returnOk pd s; typ_at (AArch APageDirectory) pd s; is_aligned pd pdBits\<rbrakk> \<Longrightarrow> page_directory_at' pd s' proof (prove)
goal (5 subgoals):
 1. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; arm_asid_map (arch_state s) asid = Some (hw_asid, pd); asid \<noteq> 0; find_pd_for_asid asid s = returnOk pd s; typ_at (AArch APageDirectory) pd s; is_aligned pd pdBits\<rbrakk> \<Longrightarrow> pspace_relation (kheap (?a40 asid hw_asid pd)) (ksPSpace s')
 2. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; arm_asid_map (arch_state s) asid = Some (hw_asid, pd); asid \<noteq> 0; find_pd_for_asid asid s = returnOk pd s; typ_at (AArch APageDirectory) pd s; is_aligned pd pdBits\<rbrakk> \<Longrightarrow> pspace_aligned (?a40 asid hw_asid pd)
 3. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; arm_asid_map (arch_state s) asid = Some (hw_asid, pd); asid \<noteq> 0; find_pd_for_asid asid s = returnOk pd s; typ_at (AArch APageDirectory) pd s; is_aligned pd pdBits\<rbrakk> \<Longrightarrow> pspace_aligned' s'
 4. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; arm_asid_map (arch_state s) asid = Some (hw_asid, pd); asid \<noteq> 0; find_pd_for_asid asid s = returnOk pd s; typ_at (AArch APageDirectory) pd s; is_aligned pd pdBits\<rbrakk> \<Longrightarrow> pspace_distinct' s'
 5. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; arm_asid_map (arch_state s) asid = Some (hw_asid, pd); asid \<noteq> 0; find_pd_for_asid asid s = returnOk pd s; typ_at (AArch APageDirectory) pd s; is_aligned pd pdBits\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) pd (?a40 asid hw_asid pd) proof (prove)
goal (4 subgoals):
 1. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; arm_asid_map (arch_state s) asid = Some (hw_asid, pd); asid \<noteq> 0; find_pd_for_asid asid s = returnOk pd s; typ_at (AArch APageDirectory) pd s; is_aligned pd pdBits\<rbrakk> \<Longrightarrow> pspace_aligned s
 2. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; arm_asid_map (arch_state s) asid = Some (hw_asid, pd); asid \<noteq> 0; find_pd_for_asid asid s = returnOk pd s; typ_at (AArch APageDirectory) pd s; is_aligned pd pdBits\<rbrakk> \<Longrightarrow> pspace_aligned' s'
 3. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; arm_asid_map (arch_state s) asid = Some (hw_asid, pd); asid \<noteq> 0; find_pd_for_asid asid s = returnOk pd s; typ_at (AArch APageDirectory) pd s; is_aligned pd pdBits\<rbrakk> \<Longrightarrow> pspace_distinct' s'
 4. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; arm_asid_map (arch_state s) asid = Some (hw_asid, pd); asid \<noteq> 0; find_pd_for_asid asid s = returnOk pd s; typ_at (AArch APageDirectory) pd s; is_aligned pd pdBits\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) pd s proof (prove)
goal (3 subgoals):
 1. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; arm_asid_map (arch_state s) asid = Some (hw_asid, pd); asid \<noteq> 0; find_pd_for_asid asid s = returnOk pd s; typ_at (AArch APageDirectory) pd s; is_aligned pd pdBits\<rbrakk> \<Longrightarrow> pspace_aligned' s'
 2. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; arm_asid_map (arch_state s) asid = Some (hw_asid, pd); asid \<noteq> 0; find_pd_for_asid asid s = returnOk pd s; typ_at (AArch APageDirectory) pd s; is_aligned pd pdBits\<rbrakk> \<Longrightarrow> pspace_distinct' s'
 3. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; arm_asid_map (arch_state s) asid = Some (hw_asid, pd); asid \<noteq> 0; find_pd_for_asid asid s = returnOk pd s; typ_at (AArch APageDirectory) pd s; is_aligned pd pdBits\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) pd s proof (prove)
goal (2 subgoals):
 1. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; arm_asid_map (arch_state s) asid = Some (hw_asid, pd); asid \<noteq> 0; find_pd_for_asid asid s = returnOk pd s; typ_at (AArch APageDirectory) pd s; is_aligned pd pdBits\<rbrakk> \<Longrightarrow> pspace_distinct' s'
 2. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; arm_asid_map (arch_state s) asid = Some (hw_asid, pd); asid \<noteq> 0; find_pd_for_asid asid s = returnOk pd s; typ_at (AArch APageDirectory) pd s; is_aligned pd pdBits\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) pd s proof (prove)
goal (1 subgoal):
 1. \<And>asid hw_asid pd. \<lbrakk>(s, s') \<in> state_relation; invs s; pspace_aligned' s'; pspace_distinct' s'; armKSASIDMap (ksArchState s') asid = Some (hw_asid, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; arm_asid_map (arch_state s) asid = Some (hw_asid, pd); asid \<noteq> 0; find_pd_for_asid asid s = returnOk pd s; typ_at (AArch APageDirectory) pd s; is_aligned pd pdBits\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) pd s proof (prove)
goal:
No subgoals!