theory ArchVSpace_AI

lemma vs_lookup_pages1:
  "vs_lookup_pages1 s' = vs_lookup_pages1 s \<union> new_lookups" using pde pd new ap apply (clarsimp simp: vs_lookup_pages1_def new_lookups_def) apply (rule set_eqI) apply (clarsimp simp: obj_at_def s'_def vs_refs_pages_def graph_of_def) apply (rule iffI) apply (clarsimp simp: image_def split: if_split_asm) apply fastforce apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vs_lookup_pages1 s' = vs_lookup_pages1 s \<union> new_lookups proof (prove)
using this:
empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd))
kheap s pdp = Some (ArchObj (PageDirectory pd))
pool asid = None
kheap s ap = Some (ArchObj (ASIDPool pool))

goal (1 subgoal):
 1. vs_lookup_pages1 s' = vs_lookup_pages1 s \<union> new_lookups proof (prove)
goal (1 subgoal):
 1. \<lbrakk>empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)); kheap s pdp = Some (ArchObj (PageDirectory pd)); pool asid = None; kheap s ap = Some (ArchObj (ASIDPool pool))\<rbrakk> \<Longrightarrow> {((rs, p), rs', p'). \<exists>ko. ko_at ko p s' \<and> (\<exists>r. rs' = r # rs \<and> (r, p') \<in> vs_refs_pages ko)} = {((rs, p), rs', p'). \<exists>ko. ko_at ko p s \<and> (\<exists>r. rs' = r # rs \<and> (r, p') \<in> vs_refs_pages ko)} \<union> {((rs, p), rs', p'). rs' = VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rs \<and> p = ap \<and> p' = pdp} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)); kheap s pdp = Some (ArchObj (PageDirectory pd)); pool asid = None; kheap s ap = Some (ArchObj (ASIDPool pool))\<rbrakk> \<Longrightarrow> (x \<in> {((rs, p), rs', p'). \<exists>ko. ko_at ko p s' \<and> (\<exists>r. rs' = r # rs \<and> (r, p') \<in> vs_refs_pages ko)}) = (x \<in> {((rs, p), rs', p'). \<exists>ko. ko_at ko p s \<and> (\<exists>r. rs' = r # rs \<and> (r, p') \<in> vs_refs_pages ko)} \<union> {((rs, p), rs', p'). rs' = VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rs \<and> p = ap \<and> p' = pdp}) proof (prove)
goal (1 subgoal):
 1. \<And>a aa ba. \<lbrakk>empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)); kheap s pdp = Some (ArchObj (PageDirectory pd)); pool asid = None; kheap s ap = Some (ArchObj (ASIDPool pool))\<rbrakk> \<Longrightarrow> (\<exists>r. aa = r # a \<and> (r, ba) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), x)) ` {(x, y). (if x = asid then Some pdp else pool x) = Some y}) = ((\<exists>r. aa = r # a \<and> (r, ba) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), x)) ` {(x, y). pool x = Some y}) \<or> aa = VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # a \<and> ba = pdp) proof (prove)
goal (2 subgoals):
 1. \<And>a aa ba. \<lbrakk>empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)); kheap s pdp = Some (ArchObj (PageDirectory pd)); pool asid = None; kheap s ap = Some (ArchObj (ASIDPool pool)); \<exists>r. aa = r # a \<and> (r, ba) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), x)) ` {(x, y). (if x = asid then Some pdp else pool x) = Some y}\<rbrakk> \<Longrightarrow> (\<exists>r. aa = r # a \<and> (r, ba) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), x)) ` {(x, y). pool x = Some y}) \<or> aa = VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # a \<and> ba = pdp
 2. \<And>a aa ba. \<lbrakk>empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)); kheap s pdp = Some (ArchObj (PageDirectory pd)); pool asid = None; kheap s ap = Some (ArchObj (ASIDPool pool)); (\<exists>r. aa = r # a \<and> (r, ba) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), x)) ` {(x, y). pool x = Some y}) \<or> aa = VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # a \<and> ba = pdp\<rbrakk> \<Longrightarrow> \<exists>r. aa = r # a \<and> (r, ba) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), x)) ` {(x, y). (if x = asid then Some pdp else pool x) = Some y} proof (prove)
goal (2 subgoals):
 1. \<And>ba r ab. \<lbrakk>empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)); kheap s pdp = Some (ArchObj (PageDirectory pd)); pool asid = None; kheap s ap = Some (ArchObj (ASIDPool pool)); ab = asid \<longrightarrow> pdp = ba \<and> r = VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool); ab = asid \<or> pool ab = Some ba \<and> r = VSRef (UCAST(10 \<rightarrow> 32) ab) (Some AASIDPool); r = VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) \<longrightarrow> ba \<noteq> pdp\<rbrakk> \<Longrightarrow> \<exists>a. pool a = Some ba \<and> r = VSRef (UCAST(10 \<rightarrow> 32) a) (Some AASIDPool)
 2. \<And>a aa ba. \<lbrakk>empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)); kheap s pdp = Some (ArchObj (PageDirectory pd)); pool asid = None; kheap s ap = Some (ArchObj (ASIDPool pool)); (\<exists>r. aa = r # a \<and> (r, ba) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), x)) ` {(x, y). pool x = Some y}) \<or> aa = VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # a \<and> ba = pdp\<rbrakk> \<Longrightarrow> \<exists>r. aa = r # a \<and> (r, ba) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), x)) ` {(x, y). (if x = asid then Some pdp else pool x) = Some y} proof (prove)
goal (1 subgoal):
 1. \<And>a aa ba. \<lbrakk>empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)); kheap s pdp = Some (ArchObj (PageDirectory pd)); pool asid = None; kheap s ap = Some (ArchObj (ASIDPool pool)); (\<exists>r. aa = r # a \<and> (r, ba) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), x)) ` {(x, y). pool x = Some y}) \<or> aa = VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # a \<and> ba = pdp\<rbrakk> \<Longrightarrow> \<exists>r. aa = r # a \<and> (r, ba) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), x)) ` {(x, y). (if x = asid then Some pdp else pool x) = Some y} proof (prove)
goal:
No subgoals!