theory ArchAcc_AI

lemma vs_refs_pages_subset2:
  "\<lbrakk>vs_refs_pages ko \<subseteq> vs_refs_pages ko';
    (\<forall>ao. (ko = ArchObj ao) \<longrightarrow> valid_vspace_obj ao s);
    (\<forall>ao'. (ko' = ArchObj ao') \<longrightarrow> valid_vspace_obj ao' s)\<rbrakk>
   \<Longrightarrow> vs_refs ko \<subseteq> vs_refs ko'" apply clarsimp apply (drule (1) subsetD[OF _ subsetD[OF vs_refs_pages_subset]]) apply (case_tac ko; simp add: vs_refs_def) subgoal for fstref b arch_kernel_obj apply (cases arch_kernel_obj; simp add: vs_refs_def) apply (cases ko'; simp add: vs_refs_pages_def) subgoal for \<dots> arch_kernel_obja by (cases arch_kernel_obja;clarsimp) apply (cases ko'; simp add: vs_refs_pages_def) subgoal for \<dots> arch_kernel_obja apply (cases arch_kernel_obja; clarsimp) apply (clarsimp simp: graph_of_def split: if_splits) subgoal for "fun" a apply (cut_tac
        imageI[where
               A="{(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref (fun x)) = Some y}"
               and f="(\<lambda>(r, y). (VSRef (ucast r) (Some APageDirectory), y))" and x="(a,b)"]) apply simp apply (clarsimp simp: pde_ref_def pde_ref_pages_def
          split: pde.splits) apply (drule bspec,simp)+ apply (simp add: valid_pde_def) apply (clarsimp simp: data_at_def obj_at_def a_type_def) apply (drule bspec, simp split: if_splits)+ by (clarsimp simp: obj_at_def a_type_def data_at_def) done done done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vs_refs_pages ko \<subseteq> vs_refs_pages ko'; \<forall>ao. ko = ArchObj ao \<longrightarrow> valid_vspace_obj ao s; \<forall>ao'. ko' = ArchObj ao' \<longrightarrow> valid_vspace_obj ao' s\<rbrakk> \<Longrightarrow> vs_refs ko \<subseteq> vs_refs ko' proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>vs_refs_pages ko \<subseteq> vs_refs_pages ko'; \<forall>ao. ko = ArchObj ao \<longrightarrow> valid_vspace_obj ao s; \<forall>ao'. ko' = ArchObj ao' \<longrightarrow> valid_vspace_obj ao' s; (a, b) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (a, b) \<in> vs_refs ko' proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>ao. ko = ArchObj ao \<longrightarrow> valid_vspace_obj ao s; \<forall>ao'. ko' = ArchObj ao' \<longrightarrow> valid_vspace_obj ao' s; (a, b) \<in> vs_refs ko; (a, b) \<in> vs_refs_pages ko'\<rbrakk> \<Longrightarrow> (a, b) \<in> vs_refs ko' proof (prove)
goal (1 subgoal):
 1. \<And>a b x5. \<lbrakk>valid_vspace_obj x5 s; \<forall>ao'. ko' = ArchObj ao' \<longrightarrow> valid_vspace_obj ao' s; (a, b) \<in> (case x5 of ASIDPool pool \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | PageDirectory pd \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) | _ \<Rightarrow> {}); (a, b) \<in> vs_refs_pages ko'; ko = ArchObj x5\<rbrakk> \<Longrightarrow> (a, b) \<in> (case ko' of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) | ArchObj _ \<Rightarrow> {} | _ \<Rightarrow> {}) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_vspace_obj arch_kernel_obj s; \<forall>ao'. ko' = ArchObj ao' \<longrightarrow> valid_vspace_obj ao' s; (fstref, b) \<in> (case arch_kernel_obj of ASIDPool pool \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | PageDirectory pd \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) | _ \<Rightarrow> {}); (fstref, b) \<in> vs_refs_pages ko'; ko = ArchObj arch_kernel_obj\<rbrakk> \<Longrightarrow> (fstref, b) \<in> (case ko' of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) | ArchObj _ \<Rightarrow> {} | _ \<Rightarrow> {}) proof (prove)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>\<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s; \<forall>ao'. ko' = ArchObj ao' \<longrightarrow> valid_vspace_obj ao' s; (fstref, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), x)) ` graph_of x1; (fstref, b) \<in> vs_refs_pages ko'; ko = ArchObj (ASIDPool x1); arch_kernel_obj = ASIDPool x1\<rbrakk> \<Longrightarrow> (fstref, b) \<in> (case ko' of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) | ArchObj _ \<Rightarrow> {} | _ \<Rightarrow> {})
 2. \<And>x3. \<lbrakk>\<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) s; \<forall>ao'. ko' = ArchObj ao' \<longrightarrow> valid_vspace_obj ao' s; (fstref, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (x3 x)); (fstref, b) \<in> vs_refs_pages ko'; ko = ArchObj (PageDirectory x3); arch_kernel_obj = PageDirectory x3\<rbrakk> \<Longrightarrow> (fstref, b) \<in> (case ko' of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) | ArchObj _ \<Rightarrow> {} | _ \<Rightarrow> {}) proof (prove)
goal (2 subgoals):
 1. \<And>x1 x5. \<lbrakk>\<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s; valid_vspace_obj x5 s; (fstref, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), x)) ` graph_of x1; (fstref, b) \<in> (case x5 of ASIDPool pool \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | PageTable pt \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(8 \<rightarrow> 32) r) (Some APageTable), y)) ` graph_of (pte_ref_pages \<circ> pt) | PageDirectory pd \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref_pages (pd x)) | DataPage dev s \<Rightarrow> {}); ko = ArchObj (ASIDPool x1); arch_kernel_obj = ASIDPool x1; ko' = ArchObj x5\<rbrakk> \<Longrightarrow> (fstref, b) \<in> (case x5 of ASIDPool pool \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | PageDirectory pd \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) | _ \<Rightarrow> {})
 2. \<And>x3. \<lbrakk>\<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) s; \<forall>ao'. ko' = ArchObj ao' \<longrightarrow> valid_vspace_obj ao' s; (fstref, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (x3 x)); (fstref, b) \<in> vs_refs_pages ko'; ko = ArchObj (PageDirectory x3); arch_kernel_obj = PageDirectory x3\<rbrakk> \<Longrightarrow> (fstref, b) \<in> (case ko' of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) | ArchObj _ \<Rightarrow> {} | _ \<Rightarrow> {}) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>ran x1_. typ_at (AArch APageDirectory) x s; valid_vspace_obj arch_kernel_obja s; (fstref, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), x)) ` graph_of x1_; (fstref, b) \<in> (case arch_kernel_obja of ASIDPool pool \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | PageTable pt \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(8 \<rightarrow> 32) r) (Some APageTable), y)) ` graph_of (pte_ref_pages \<circ> pt) | PageDirectory pd \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref_pages (pd x)) | DataPage dev s \<Rightarrow> {}); ko = ArchObj (ASIDPool x1_); arch_kernel_obj = ASIDPool x1_; ko' = ArchObj arch_kernel_obja\<rbrakk> \<Longrightarrow> (fstref, b) \<in> (case arch_kernel_obja of ASIDPool pool \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | PageDirectory pd \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) | _ \<Rightarrow> {}) proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<lbrakk>\<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) s; \<forall>ao'. ko' = ArchObj ao' \<longrightarrow> valid_vspace_obj ao' s; (fstref, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (x3 x)); (fstref, b) \<in> vs_refs_pages ko'; ko = ArchObj (PageDirectory x3); arch_kernel_obj = PageDirectory x3\<rbrakk> \<Longrightarrow> (fstref, b) \<in> (case ko' of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) | ArchObj _ \<Rightarrow> {} | _ \<Rightarrow> {}) proof (prove)
goal (1 subgoal):
 1. \<And>x3 x5. \<lbrakk>\<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) s; valid_vspace_obj x5 s; (fstref, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (x3 x)); (fstref, b) \<in> (case x5 of ASIDPool pool \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | PageTable pt \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(8 \<rightarrow> 32) r) (Some APageTable), y)) ` graph_of (pte_ref_pages \<circ> pt) | PageDirectory pd \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref_pages (pd x)) | DataPage dev s \<Rightarrow> {}); ko = ArchObj (PageDirectory x3); arch_kernel_obj = PageDirectory x3; ko' = ArchObj x5\<rbrakk> \<Longrightarrow> (fstref, b) \<in> (case x5 of ASIDPool pool \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | PageDirectory pd \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) | _ \<Rightarrow> {}) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>- kernel_mapping_slots. valid_pde (x3_ x) s; valid_vspace_obj arch_kernel_obja s; (fstref, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (x3_ x)); (fstref, b) \<in> (case arch_kernel_obja of ASIDPool pool \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | PageTable pt \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(8 \<rightarrow> 32) r) (Some APageTable), y)) ` graph_of (pte_ref_pages \<circ> pt) | PageDirectory pd \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref_pages (pd x)) | DataPage dev s \<Rightarrow> {}); ko = ArchObj (PageDirectory x3_); arch_kernel_obj = PageDirectory x3_; ko' = ArchObj arch_kernel_obja\<rbrakk> \<Longrightarrow> (fstref, b) \<in> (case arch_kernel_obja of ASIDPool pool \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | PageDirectory pd \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) | _ \<Rightarrow> {}) proof (prove)
goal (1 subgoal):
 1. \<And>x3a aa. \<lbrakk>\<forall>x\<in>- kernel_mapping_slots. valid_pde (x3_ x) s; \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3a x) s; ko = ArchObj (PageDirectory x3_); arch_kernel_obj = PageDirectory x3_; ko' = ArchObj (PageDirectory x3a); arch_kernel_obja = PageDirectory x3a; (aa, b) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (x3_ x)); (aa, b) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref_pages (x3a x)); fstref = VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory)\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (x3a x)) proof (prove)
goal (1 subgoal):
 1. \<And>x3a aa. \<lbrakk>pde_ref_pages (x3a aa) = Some b; fstref = VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory); \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3_ x) s; \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3a x) s; ko = ArchObj (PageDirectory x3_); arch_kernel_obj = PageDirectory x3_; ko' = ArchObj (PageDirectory x3a); arch_kernel_obja = PageDirectory x3a; aa \<notin> kernel_mapping_slots; pde_ref (x3_ aa) = Some b\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref (x3a x)) = Some y} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pde_ref_pages (fun a) = Some b; fstref = VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory); \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3_ x) s; \<forall>x\<in>- kernel_mapping_slots. valid_pde (fun x) s; ko = ArchObj (PageDirectory x3_); arch_kernel_obj = PageDirectory x3_; ko' = ArchObj (PageDirectory fun); arch_kernel_obja = PageDirectory fun; a \<notin> kernel_mapping_slots; pde_ref (x3_ a) = Some b\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory), b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref (fun x)) = Some y} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pde_ref_pages (fun a) = Some b; fstref = VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory); \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3_ x) s; \<forall>x\<in>- kernel_mapping_slots. valid_pde (fun x) s; ko = ArchObj (PageDirectory x3_); arch_kernel_obj = PageDirectory x3_; ko' = ArchObj (PageDirectory fun); arch_kernel_obja = PageDirectory fun; a \<notin> kernel_mapping_slots; pde_ref (x3_ a) = Some b; (case (a, b) of (r, y) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) \<in> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref (fun x)) = Some y}\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory), b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref (fun x)) = Some y}
 2. \<lbrakk>pde_ref_pages (fun a) = Some b; fstref = VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory); \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3_ x) s; \<forall>x\<in>- kernel_mapping_slots. valid_pde (fun x) s; ko = ArchObj (PageDirectory x3_); arch_kernel_obj = PageDirectory x3_; ko' = ArchObj (PageDirectory fun); arch_kernel_obja = PageDirectory fun; a \<notin> kernel_mapping_slots; pde_ref (x3_ a) = Some b\<rbrakk> \<Longrightarrow> (a, b) \<in> {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref (fun x)) = Some y} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pde_ref_pages (fun a) = Some b; fstref = VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory); \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3_ x) s; \<forall>x\<in>- kernel_mapping_slots. valid_pde (fun x) s; ko = ArchObj (PageDirectory x3_); arch_kernel_obj = PageDirectory x3_; ko' = ArchObj (PageDirectory fun); arch_kernel_obja = PageDirectory fun; a \<notin> kernel_mapping_slots; pde_ref (x3_ a) = Some b\<rbrakk> \<Longrightarrow> (a, b) \<in> {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref (fun x)) = Some y} proof (prove)
goal (2 subgoals):
 1. \<And>x31 x32 x33 x34 x21 x22 x23. \<lbrakk>fun a = SectionPDE x31 x32 x33 x34; fstref = VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory); \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3_ x) s; \<forall>x\<in>- kernel_mapping_slots. valid_pde (fun x) s; ko = ArchObj (PageDirectory x3_); arch_kernel_obj = PageDirectory x3_; ko' = ArchObj (PageDirectory fun); arch_kernel_obja = PageDirectory fun; a \<notin> kernel_mapping_slots; x3_ a = PageTablePDE x21 x22 x23; ptrFromPAddr x21 = ptrFromPAddr x31; b = ptrFromPAddr x31\<rbrakk> \<Longrightarrow> False
 2. \<And>x41 x42 x43 x21 x22 x23. \<lbrakk>fun a = SuperSectionPDE x41 x42 x43; fstref = VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory); \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3_ x) s; \<forall>x\<in>- kernel_mapping_slots. valid_pde (fun x) s; ko = ArchObj (PageDirectory x3_); arch_kernel_obj = PageDirectory x3_; ko' = ArchObj (PageDirectory fun); arch_kernel_obja = PageDirectory fun; a \<notin> kernel_mapping_slots; x3_ a = PageTablePDE x21 x22 x23; ptrFromPAddr x21 = ptrFromPAddr x41; b = ptrFromPAddr x41\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x31 x32 x33 x34 x21 x22 x23. \<lbrakk>fun a = SectionPDE x31 x32 x33 x34; fstref = VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory); ko = ArchObj (PageDirectory x3_); arch_kernel_obj = PageDirectory x3_; ko' = ArchObj (PageDirectory fun); arch_kernel_obja = PageDirectory fun; a \<notin> kernel_mapping_slots; x3_ a = PageTablePDE x21 x22 x23; ptrFromPAddr x21 = ptrFromPAddr x31; b = ptrFromPAddr x31; valid_pde (x3_ a) s; valid_pde (fun a) s\<rbrakk> \<Longrightarrow> False
 2. \<And>x41 x42 x43 x21 x22 x23. \<lbrakk>fun a = SuperSectionPDE x41 x42 x43; fstref = VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory); \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3_ x) s; \<forall>x\<in>- kernel_mapping_slots. valid_pde (fun x) s; ko = ArchObj (PageDirectory x3_); arch_kernel_obj = PageDirectory x3_; ko' = ArchObj (PageDirectory fun); arch_kernel_obja = PageDirectory fun; a \<notin> kernel_mapping_slots; x3_ a = PageTablePDE x21 x22 x23; ptrFromPAddr x21 = ptrFromPAddr x41; b = ptrFromPAddr x41\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x31 x32 x33 x34 x21 x22 x23. \<lbrakk>fun a = SectionPDE x31 x32 x33 x34; fstref = VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory); ko = ArchObj (PageDirectory x3_); arch_kernel_obj = PageDirectory x3_; ko' = ArchObj (PageDirectory fun); arch_kernel_obja = PageDirectory fun; a \<notin> kernel_mapping_slots; x3_ a = PageTablePDE x21 x22 x23; ptrFromPAddr x21 = ptrFromPAddr x31; b = ptrFromPAddr x31; typ_at (AArch APageTable) (ptrFromPAddr x31) s; data_at ARMSection (ptrFromPAddr x31) s\<rbrakk> \<Longrightarrow> False
 2. \<And>x41 x42 x43 x21 x22 x23. \<lbrakk>fun a = SuperSectionPDE x41 x42 x43; fstref = VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory); \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3_ x) s; \<forall>x\<in>- kernel_mapping_slots. valid_pde (fun x) s; ko = ArchObj (PageDirectory x3_); arch_kernel_obj = PageDirectory x3_; ko' = ArchObj (PageDirectory fun); arch_kernel_obja = PageDirectory fun; a \<notin> kernel_mapping_slots; x3_ a = PageTablePDE x21 x22 x23; ptrFromPAddr x21 = ptrFromPAddr x41; b = ptrFromPAddr x41\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42 x43 x21 x22 x23. \<lbrakk>fun a = SuperSectionPDE x41 x42 x43; fstref = VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory); \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3_ x) s; \<forall>x\<in>- kernel_mapping_slots. valid_pde (fun x) s; ko = ArchObj (PageDirectory x3_); arch_kernel_obj = PageDirectory x3_; ko' = ArchObj (PageDirectory fun); arch_kernel_obja = PageDirectory fun; a \<notin> kernel_mapping_slots; x3_ a = PageTablePDE x21 x22 x23; ptrFromPAddr x21 = ptrFromPAddr x41; b = ptrFromPAddr x41\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42 x43 x21 x22 x23. \<lbrakk>fun a = SuperSectionPDE x41 x42 x43; fstref = VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory); ko = ArchObj (PageDirectory x3_); arch_kernel_obj = PageDirectory x3_; ko' = ArchObj (PageDirectory fun); arch_kernel_obja = PageDirectory fun; a \<notin> kernel_mapping_slots; x3_ a = PageTablePDE x21 x22 x23; ptrFromPAddr x21 = ptrFromPAddr x41; b = ptrFromPAddr x41; valid_pde (x3_ a) s; valid_pde (fun a) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!