theory ArchInvariants_AI

lemma vs_ref_order:
  "\<lbrakk> (r \<rhd> p) s; valid_vspace_objs s; valid_arch_state s \<rbrakk>
       \<Longrightarrow> \<exists>tp. r \<noteq> [] \<and> typ_at (AArch tp) p s \<and>
            rev (Some tp # map vs_ref_aatype r)
               \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]" apply (erule vs_lookup_induct) apply (clarsimp simp: valid_arch_state_def valid_asid_table_def ranI) apply (clarsimp dest!: vs_lookup1D elim!: obj_atE) apply (clarsimp simp: vs_refs_def a_type_simps
                 split: kernel_object.split_asm arch_kernel_obj.split_asm
                 dest!: graph_ofD) apply (drule valid_vspace_objsD) apply (simp add: obj_at_def) apply (assumption) apply (case_tac rs; simp) apply (case_tac list; simp add: ranI) apply (case_tac lista; simp) apply (frule prefix_length_le, clarsimp) apply (drule valid_vspace_objsD, simp add: obj_at_def, assumption) apply (clarsimp simp: pde_ref_def
                 split: pde.split_asm if_split_asm) apply (drule_tac x=a in bspec, simp) apply (case_tac rs; simp) apply (case_tac list; simp) apply (case_tac lista; simp) apply (frule prefix_length_le, clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(r \<rhd> p) s; valid_vspace_objs s; valid_arch_state s\<rbrakk> \<Longrightarrow> \<exists>tp. r \<noteq> [] \<and> typ_at (AArch tp) p s \<and> rev (Some tp # map vs_ref_aatype r) \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable] proof (prove)
goal (2 subgoals):
 1. \<And>asid p. \<lbrakk>valid_vspace_objs s; valid_arch_state s; asid_table s asid = Some p\<rbrakk> \<Longrightarrow> \<exists>tp. [VSRef (UCAST(7 \<rightarrow> 32) asid) None] \<noteq> [] \<and> typ_at (AArch tp) p s \<and> rev (Some tp # map vs_ref_aatype [VSRef (UCAST(7 \<rightarrow> 32) asid) None]) \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]
 2. \<And>ref p ref' p'. \<lbrakk>valid_vspace_objs s; valid_arch_state s; (ref \<rhd> p) s; ((ref, p), ref', p') \<in> vs_lookup1 s; \<exists>tp. ref \<noteq> [] \<and> typ_at (AArch tp) p s \<and> rev (Some tp # map vs_ref_aatype ref) \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]\<rbrakk> \<Longrightarrow> \<exists>tp. ref' \<noteq> [] \<and> typ_at (AArch tp) p' s \<and> rev (Some tp # map vs_ref_aatype ref') \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable] proof (prove)
goal (1 subgoal):
 1. \<And>ref p ref' p'. \<lbrakk>valid_vspace_objs s; valid_arch_state s; (ref \<rhd> p) s; ((ref, p), ref', p') \<in> vs_lookup1 s; \<exists>tp. ref \<noteq> [] \<and> typ_at (AArch tp) p s \<and> rev (Some tp # map vs_ref_aatype ref) \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]\<rbrakk> \<Longrightarrow> \<exists>tp. ref' \<noteq> [] \<and> typ_at (AArch tp) p' s \<and> rev (Some tp # map vs_ref_aatype ref') \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable] proof (prove)
goal (1 subgoal):
 1. \<And>rs r pa p'a tp koa. \<lbrakk>valid_vspace_objs s; valid_arch_state s; (rs \<rhd> pa) s; rs \<noteq> []; rev (map vs_ref_aatype rs) @ [Some tp] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]; a_type koa = AArch tp; (r, p'a) \<in> vs_refs koa; kheap s pa = Some koa\<rbrakk> \<Longrightarrow> \<exists>tp. typ_at (AArch tp) p'a s \<and> rev (map vs_ref_aatype rs) @ [vs_ref_aatype r, Some tp] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable] proof (prove)
goal (2 subgoals):
 1. \<And>rs pa x1 a b. \<lbrakk>kheap s pa = Some (ArchObj (ASIDPool x1)); valid_vspace_objs s; valid_arch_state s; (rs \<rhd> pa) s; rs \<noteq> []; rev (map vs_ref_aatype rs) @ [Some AASIDPool] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]; x1 a = Some b\<rbrakk> \<Longrightarrow> \<exists>tp. typ_at (AArch tp) b s \<and> rev (map vs_ref_aatype rs) @ [Some AASIDPool, Some tp] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]
 2. \<And>rs pa x3 a b. \<lbrakk>kheap s pa = Some (ArchObj (PageDirectory x3)); valid_vspace_objs s; valid_arch_state s; (rs \<rhd> pa) s; rs \<noteq> []; rev (map vs_ref_aatype rs) @ [Some APageDirectory] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]; (if a \<in> kernel_mapping_slots then None else pde_ref (x3 a)) = Some b\<rbrakk> \<Longrightarrow> \<exists>tp. typ_at (AArch tp) b s \<and> rev (map vs_ref_aatype rs) @ [Some APageDirectory, Some tp] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable] proof (prove)
goal (4 subgoals):
 1. \<And>rs pa x1 a b. \<lbrakk>kheap s pa = Some (ArchObj (ASIDPool x1)); valid_vspace_objs s; valid_arch_state s; rs \<noteq> []; rev (map vs_ref_aatype rs) @ [Some AASIDPool] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]; x1 a = Some b\<rbrakk> \<Longrightarrow> ako_at (?ao97 rs pa x1 a b) pa s
 2. \<And>rs pa x1 a b. \<lbrakk>kheap s pa = Some (ArchObj (ASIDPool x1)); valid_vspace_objs s; valid_arch_state s; rs \<noteq> []; rev (map vs_ref_aatype rs) @ [Some AASIDPool] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]; x1 a = Some b\<rbrakk> \<Longrightarrow> valid_vspace_objs s
 3. \<And>rs pa x1 a b. \<lbrakk>kheap s pa = Some (ArchObj (ASIDPool x1)); valid_vspace_objs s; valid_arch_state s; rs \<noteq> []; rev (map vs_ref_aatype rs) @ [Some AASIDPool] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]; x1 a = Some b; valid_vspace_obj (?ao97 rs pa x1 a b) s\<rbrakk> \<Longrightarrow> \<exists>tp. typ_at (AArch tp) b s \<and> rev (map vs_ref_aatype rs) @ [Some AASIDPool, Some tp] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]
 4. \<And>rs pa x3 a b. \<lbrakk>kheap s pa = Some (ArchObj (PageDirectory x3)); valid_vspace_objs s; valid_arch_state s; (rs \<rhd> pa) s; rs \<noteq> []; rev (map vs_ref_aatype rs) @ [Some APageDirectory] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]; (if a \<in> kernel_mapping_slots then None else pde_ref (x3 a)) = Some b\<rbrakk> \<Longrightarrow> \<exists>tp. typ_at (AArch tp) b s \<and> rev (map vs_ref_aatype rs) @ [Some APageDirectory, Some tp] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable] proof (prove)
goal (3 subgoals):
 1. \<And>rs pa x1 a b. \<lbrakk>kheap s pa = Some (ArchObj (ASIDPool x1)); valid_vspace_objs s; valid_arch_state s; rs \<noteq> []; rev (map vs_ref_aatype rs) @ [Some AASIDPool] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]; x1 a = Some b\<rbrakk> \<Longrightarrow> valid_vspace_objs s
 2. \<And>rs pa x1 a b. \<lbrakk>kheap s pa = Some (ArchObj (ASIDPool x1)); valid_vspace_objs s; valid_arch_state s; rs \<noteq> []; rev (map vs_ref_aatype rs) @ [Some AASIDPool] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]; x1 a = Some b; valid_vspace_obj (ASIDPool x1) s\<rbrakk> \<Longrightarrow> \<exists>tp. typ_at (AArch tp) b s \<and> rev (map vs_ref_aatype rs) @ [Some AASIDPool, Some tp] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]
 3. \<And>rs pa x3 a b. \<lbrakk>kheap s pa = Some (ArchObj (PageDirectory x3)); valid_vspace_objs s; valid_arch_state s; (rs \<rhd> pa) s; rs \<noteq> []; rev (map vs_ref_aatype rs) @ [Some APageDirectory] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]; (if a \<in> kernel_mapping_slots then None else pde_ref (x3 a)) = Some b\<rbrakk> \<Longrightarrow> \<exists>tp. typ_at (AArch tp) b s \<and> rev (map vs_ref_aatype rs) @ [Some APageDirectory, Some tp] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable] proof (prove)
goal (2 subgoals):
 1. \<And>rs pa x1 a b. \<lbrakk>kheap s pa = Some (ArchObj (ASIDPool x1)); valid_vspace_objs s; valid_arch_state s; rs \<noteq> []; rev (map vs_ref_aatype rs) @ [Some AASIDPool] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]; x1 a = Some b; valid_vspace_obj (ASIDPool x1) s\<rbrakk> \<Longrightarrow> \<exists>tp. typ_at (AArch tp) b s \<and> rev (map vs_ref_aatype rs) @ [Some AASIDPool, Some tp] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]
 2. \<And>rs pa x3 a b. \<lbrakk>kheap s pa = Some (ArchObj (PageDirectory x3)); valid_vspace_objs s; valid_arch_state s; (rs \<rhd> pa) s; rs \<noteq> []; rev (map vs_ref_aatype rs) @ [Some APageDirectory] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]; (if a \<in> kernel_mapping_slots then None else pde_ref (x3 a)) = Some b\<rbrakk> \<Longrightarrow> \<exists>tp. typ_at (AArch tp) b s \<and> rev (map vs_ref_aatype rs) @ [Some APageDirectory, Some tp] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable] proof (prove)
goal (2 subgoals):
 1. \<And>rs pa x1 a b aa list. \<lbrakk>kheap s pa = Some (ArchObj (ASIDPool x1)); valid_vspace_objs s; valid_arch_state s; rev (map vs_ref_aatype list) @ [vs_ref_aatype aa, Some AASIDPool] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]; x1 a = Some b; \<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s; rs = aa # list\<rbrakk> \<Longrightarrow> \<exists>tp. typ_at (AArch tp) b s \<and> rev (map vs_ref_aatype list) @ [vs_ref_aatype aa, Some AASIDPool, Some tp] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]
 2. \<And>rs pa x3 a b. \<lbrakk>kheap s pa = Some (ArchObj (PageDirectory x3)); valid_vspace_objs s; valid_arch_state s; (rs \<rhd> pa) s; rs \<noteq> []; rev (map vs_ref_aatype rs) @ [Some APageDirectory] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]; (if a \<in> kernel_mapping_slots then None else pde_ref (x3 a)) = Some b\<rbrakk> \<Longrightarrow> \<exists>tp. typ_at (AArch tp) b s \<and> rev (map vs_ref_aatype rs) @ [Some APageDirectory, Some tp] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable] proof (prove)
goal (2 subgoals):
 1. \<And>rs pa x1 a b aa list ab lista. \<lbrakk>kheap s pa = Some (ArchObj (ASIDPool x1)); valid_vspace_objs s; valid_arch_state s; rev (map vs_ref_aatype lista) @ [vs_ref_aatype ab, vs_ref_aatype aa, Some AASIDPool] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]; x1 a = Some b; \<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s; rs = aa # ab # lista; list = ab # lista\<rbrakk> \<Longrightarrow> \<exists>tp. typ_at (AArch tp) b s \<and> rev (map vs_ref_aatype lista) @ [vs_ref_aatype ab, vs_ref_aatype aa, Some AASIDPool, Some tp] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]
 2. \<And>rs pa x3 a b. \<lbrakk>kheap s pa = Some (ArchObj (PageDirectory x3)); valid_vspace_objs s; valid_arch_state s; (rs \<rhd> pa) s; rs \<noteq> []; rev (map vs_ref_aatype rs) @ [Some APageDirectory] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]; (if a \<in> kernel_mapping_slots then None else pde_ref (x3 a)) = Some b\<rbrakk> \<Longrightarrow> \<exists>tp. typ_at (AArch tp) b s \<and> rev (map vs_ref_aatype rs) @ [Some APageDirectory, Some tp] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable] proof (prove)
goal (2 subgoals):
 1. \<And>rs pa x1 a b aa list ab lista ac listb. \<lbrakk>kheap s pa = Some (ArchObj (ASIDPool x1)); valid_vspace_objs s; valid_arch_state s; rev (map vs_ref_aatype listb) @ [vs_ref_aatype ac, vs_ref_aatype ab, vs_ref_aatype aa, Some AASIDPool] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]; x1 a = Some b; \<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s; rs = aa # ab # ac # listb; list = ab # ac # listb; lista = ac # listb\<rbrakk> \<Longrightarrow> \<exists>tp. typ_at (AArch tp) b s \<and> rev (map vs_ref_aatype listb) @ [vs_ref_aatype ac, vs_ref_aatype ab, vs_ref_aatype aa, Some AASIDPool, Some tp] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]
 2. \<And>rs pa x3 a b. \<lbrakk>kheap s pa = Some (ArchObj (PageDirectory x3)); valid_vspace_objs s; valid_arch_state s; (rs \<rhd> pa) s; rs \<noteq> []; rev (map vs_ref_aatype rs) @ [Some APageDirectory] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]; (if a \<in> kernel_mapping_slots then None else pde_ref (x3 a)) = Some b\<rbrakk> \<Longrightarrow> \<exists>tp. typ_at (AArch tp) b s \<and> rev (map vs_ref_aatype rs) @ [Some APageDirectory, Some tp] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable] proof (prove)
goal (1 subgoal):
 1. \<And>rs pa x3 a b. \<lbrakk>kheap s pa = Some (ArchObj (PageDirectory x3)); valid_vspace_objs s; valid_arch_state s; (rs \<rhd> pa) s; rs \<noteq> []; rev (map vs_ref_aatype rs) @ [Some APageDirectory] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]; (if a \<in> kernel_mapping_slots then None else pde_ref (x3 a)) = Some b\<rbrakk> \<Longrightarrow> \<exists>tp. typ_at (AArch tp) b s \<and> rev (map vs_ref_aatype rs) @ [Some APageDirectory, Some tp] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable] proof (prove)
goal (1 subgoal):
 1. \<And>rs pa x3 a b. \<lbrakk>kheap s pa = Some (ArchObj (PageDirectory x3)); valid_vspace_objs s; valid_arch_state s; rs \<noteq> []; rev (map vs_ref_aatype rs) @ [Some APageDirectory] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]; (if a \<in> kernel_mapping_slots then None else pde_ref (x3 a)) = Some b; valid_vspace_obj (PageDirectory x3) s\<rbrakk> \<Longrightarrow> \<exists>tp. typ_at (AArch tp) b s \<and> rev (map vs_ref_aatype rs) @ [Some APageDirectory, Some tp] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable] proof (prove)
goal (1 subgoal):
 1. \<And>rs pa x3 a x21 x22 x23. \<lbrakk>\<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) s; kheap s pa = Some (ArchObj (PageDirectory x3)); valid_vspace_objs s; valid_arch_state s; rs \<noteq> []; rev (map vs_ref_aatype rs) @ [Some APageDirectory] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]; a \<notin> kernel_mapping_slots; x3 a = PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> \<exists>tp. typ_at (AArch tp) (ptrFromPAddr x21) s \<and> rev (map vs_ref_aatype rs) @ [Some APageDirectory, Some tp] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable] proof (prove)
goal (1 subgoal):
 1. \<And>rs pa x3 a x21 x22 x23. \<lbrakk>kheap s pa = Some (ArchObj (PageDirectory x3)); valid_vspace_objs s; valid_arch_state s; rs \<noteq> []; rev (map vs_ref_aatype rs) @ [Some APageDirectory] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]; a \<notin> kernel_mapping_slots; x3 a = PageTablePDE x21 x22 x23; valid_pde (x3 a) s\<rbrakk> \<Longrightarrow> \<exists>tp. typ_at (AArch tp) (ptrFromPAddr x21) s \<and> rev (map vs_ref_aatype rs) @ [Some APageDirectory, Some tp] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable] proof (prove)
goal (1 subgoal):
 1. \<And>rs pa x3 a x21 x22 x23 aa list. \<lbrakk>kheap s pa = Some (ArchObj (PageDirectory x3)); valid_vspace_objs s; valid_arch_state s; rev (map vs_ref_aatype list) @ [vs_ref_aatype aa, Some APageDirectory] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]; a \<notin> kernel_mapping_slots; x3 a = PageTablePDE x21 x22 x23; typ_at (AArch APageTable) (ptrFromPAddr x21) s; rs = aa # list\<rbrakk> \<Longrightarrow> \<exists>tp. typ_at (AArch tp) (ptrFromPAddr x21) s \<and> rev (map vs_ref_aatype list) @ [vs_ref_aatype aa, Some APageDirectory, Some tp] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable] proof (prove)
goal (1 subgoal):
 1. \<And>rs pa x3 a x21 x22 x23 aa list ab lista. \<lbrakk>kheap s pa = Some (ArchObj (PageDirectory x3)); valid_vspace_objs s; valid_arch_state s; rev (map vs_ref_aatype lista) @ [vs_ref_aatype ab, vs_ref_aatype aa, Some APageDirectory] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]; a \<notin> kernel_mapping_slots; x3 a = PageTablePDE x21 x22 x23; typ_at (AArch APageTable) (ptrFromPAddr x21) s; rs = aa # ab # lista; list = ab # lista\<rbrakk> \<Longrightarrow> \<exists>tp. typ_at (AArch tp) (ptrFromPAddr x21) s \<and> rev (map vs_ref_aatype lista) @ [vs_ref_aatype ab, vs_ref_aatype aa, Some APageDirectory, Some tp] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable] proof (prove)
goal (1 subgoal):
 1. \<And>rs pa x3 a x21 x22 x23 aa list ab lista ac listb. \<lbrakk>kheap s pa = Some (ArchObj (PageDirectory x3)); valid_vspace_objs s; valid_arch_state s; rev (map vs_ref_aatype listb) @ [vs_ref_aatype ac, vs_ref_aatype ab, vs_ref_aatype aa, Some APageDirectory] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]; a \<notin> kernel_mapping_slots; x3 a = PageTablePDE x21 x22 x23; typ_at (AArch APageTable) (ptrFromPAddr x21) s; rs = aa # ab # ac # listb; list = ab # ac # listb; lista = ac # listb\<rbrakk> \<Longrightarrow> \<exists>tp. typ_at (AArch tp) (ptrFromPAddr x21) s \<and> rev (map vs_ref_aatype listb) @ [vs_ref_aatype ac, vs_ref_aatype ab, vs_ref_aatype aa, Some APageDirectory, Some tp] \<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable] proof (prove)
goal:
No subgoals!