theory ArchAcc_AI

lemma set_pt_valid_vspace_objs[wp]:
  "valid (\<lambda>s. valid_vspace_objs s \<and> ((\<exists>\<rhd> p) s \<longrightarrow> (\<forall>x. valid_pte (pt x) s)))
             (set_pt p pt) (\<lambda>_. valid_vspace_objs)" apply (rule valid_set_ptI) apply (clarsimp simp: valid_vspace_objs_def) subgoal for s opt pa rs ao apply (spec pa) apply (prop_tac "(\<exists>\<rhd> pa) s") apply (rule exI[where x=rs]) apply (erule vs_lookupE) apply clarsimp apply (erule vs_lookupI) apply (erule rtrancl.induct, simp) subgoal for \<dots> b c apply (prop_tac "(b \<rhd>1 c) s") apply (thin_tac "_ : rtrancl _")+ apply (clarsimp simp add: vs_lookup1_def obj_at_def vs_refs_def
                            split: if_split_asm) by simp apply simp apply (spec ao) apply (cases "pa = p") apply (clarsimp simp: obj_at_def) subgoal for _ x apply (drule_tac x=x in spec) by (cases "pt x"; clarsimp simp: data_at_def obj_at_def a_type_simps) apply (cases ao; simp add: obj_at_def a_type_simps) apply clarsimp apply (drule bspec, assumption, clarsimp) apply clarsimp subgoal for "fun" _ x apply (spec x) by (cases "fun x"; clarsimp simp: obj_at_def data_at_def a_type_simps) apply clarsimp apply (drule bspec,fastforce) subgoal for "fun" x by (cases "fun x"; clarsimp simp: data_at_def obj_at_def a_type_simps) done done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_vspace_objs s \<and> ((\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s))\<rbrace> set_pt p pt \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s opt. \<lbrakk>valid_vspace_objs s \<and> ((\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s)); kheap s p = Some (ArchObj (PageTable opt))\<rbrakk> \<Longrightarrow> valid_vspace_objs (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s opt pa rs ao. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); ako_at ao pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>)\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); ako_at ao pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>)\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); ako_at ao pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); (\<exists>rs. (rs \<rhd> pa) s) \<longrightarrow> (\<forall>ao. ako_at ao pa s \<longrightarrow> valid_vspace_obj ao s)\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); ako_at ao pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); (\<exists>rs. (rs \<rhd> pa) s) \<longrightarrow> (\<forall>ao. ako_at ao pa s \<longrightarrow> valid_vspace_obj ao s)\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> pa) s
 2. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); ako_at ao pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); (\<exists>rs. (rs \<rhd> pa) s) \<longrightarrow> (\<forall>ao. ako_at ao pa s \<longrightarrow> valid_vspace_obj ao s); \<exists>ref. (ref \<rhd> pa) s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); ako_at ao pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); (\<exists>rs. (rs \<rhd> pa) s) \<longrightarrow> (\<forall>ao. ako_at ao pa s \<longrightarrow> valid_vspace_obj ao s)\<rbrakk> \<Longrightarrow> (rs \<rhd> pa) s
 2. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); ako_at ao pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); (\<exists>rs. (rs \<rhd> pa) s) \<longrightarrow> (\<forall>ao. ako_at ao pa s \<longrightarrow> valid_vspace_obj ao s); \<exists>ref. (ref \<rhd> pa) s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>ref' p'. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); ako_at ao pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); (\<exists>rs. (rs \<rhd> pa) s) \<longrightarrow> (\<forall>ao. ako_at ao pa s \<longrightarrow> valid_vspace_obj ao s); (ref', p') \<in> vs_asid_refs (asid_table (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>)); ((ref', p'), rs, pa) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>))\<^sup>*\<rbrakk> \<Longrightarrow> (rs \<rhd> pa) s
 2. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); ako_at ao pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); (\<exists>rs. (rs \<rhd> pa) s) \<longrightarrow> (\<forall>ao. ako_at ao pa s \<longrightarrow> valid_vspace_obj ao s); \<exists>ref. (ref \<rhd> pa) s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>ref' p'. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); ako_at ao pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); (\<exists>rs. (rs \<rhd> pa) s) \<longrightarrow> (\<forall>ao. ako_at ao pa s \<longrightarrow> valid_vspace_obj ao s); (ref', p') \<in> vs_asid_refs (asid_table s); ((ref', p'), rs, pa) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>))\<^sup>*\<rbrakk> \<Longrightarrow> (rs \<rhd> pa) s
 2. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); ako_at ao pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); (\<exists>rs. (rs \<rhd> pa) s) \<longrightarrow> (\<forall>ao. ako_at ao pa s \<longrightarrow> valid_vspace_obj ao s); \<exists>ref. (ref \<rhd> pa) s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>ref' p'. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); ako_at ao pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); (\<exists>rs. (rs \<rhd> pa) s) \<longrightarrow> (\<forall>ao. ako_at ao pa s \<longrightarrow> valid_vspace_obj ao s); ((ref', p'), rs, pa) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>))\<^sup>*\<rbrakk> \<Longrightarrow> ((ref', p'), rs, pa) \<in> (vs_lookup1 s)\<^sup>*
 2. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); ako_at ao pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); (\<exists>rs. (rs \<rhd> pa) s) \<longrightarrow> (\<forall>ao. ako_at ao pa s \<longrightarrow> valid_vspace_obj ao s); \<exists>ref. (ref \<rhd> pa) s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>ref' p' a b c. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); ako_at ao pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); (\<exists>rs. (rs \<rhd> pa) s) \<longrightarrow> (\<forall>ao. ako_at ao pa s \<longrightarrow> valid_vspace_obj ao s); (a, b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>))\<^sup>*; (a, b) \<in> (vs_lookup1 s)\<^sup>*; (b, c) \<in> vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>)\<rbrakk> \<Longrightarrow> (a, c) \<in> (vs_lookup1 s)\<^sup>*
 2. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); ako_at ao pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); (\<exists>rs. (rs \<rhd> pa) s) \<longrightarrow> (\<forall>ao. ako_at ao pa s \<longrightarrow> valid_vspace_obj ao s); \<exists>ref. (ref \<rhd> pa) s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); ako_at ao pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); (\<exists>rs. (rs \<rhd> pa) s) \<longrightarrow> (\<forall>ao. ako_at ao pa s \<longrightarrow> valid_vspace_obj ao s); (a_, b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>))\<^sup>*; (a_, b) \<in> (vs_lookup1 s)\<^sup>*; (b, c) \<in> vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>)\<rbrakk> \<Longrightarrow> (a_, c) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); ako_at ao pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); (\<exists>rs. (rs \<rhd> pa) s) \<longrightarrow> (\<forall>ao. ako_at ao pa s \<longrightarrow> valid_vspace_obj ao s); (a_, b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>))\<^sup>*; (a_, b) \<in> (vs_lookup1 s)\<^sup>*; (b, c) \<in> vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>)\<rbrakk> \<Longrightarrow> (b, c) \<in> vs_lookup1 s
 2. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); ako_at ao pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); (\<exists>rs. (rs \<rhd> pa) s) \<longrightarrow> (\<forall>ao. ako_at ao pa s \<longrightarrow> valid_vspace_obj ao s); (a_, b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>))\<^sup>*; (a_, b) \<in> (vs_lookup1 s)\<^sup>*; (b, c) \<in> vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); (b, c) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> (a_, c) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); ako_at ao pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); (\<exists>rs. (rs \<rhd> pa) s) \<longrightarrow> (\<forall>ao. ako_at ao pa s \<longrightarrow> valid_vspace_obj ao s); (b, c) \<in> vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>)\<rbrakk> \<Longrightarrow> (b, c) \<in> vs_lookup1 s
 2. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); ako_at ao pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); (\<exists>rs. (rs \<rhd> pa) s) \<longrightarrow> (\<forall>ao. ako_at ao pa s \<longrightarrow> valid_vspace_obj ao s); (a_, b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>))\<^sup>*; (a_, b) \<in> (vs_lookup1 s)\<^sup>*; (b, c) \<in> vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); (b, c) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> (a_, c) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); ako_at ao pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); (\<exists>rs. (rs \<rhd> pa) s) \<longrightarrow> (\<forall>ao. ako_at ao pa s \<longrightarrow> valid_vspace_obj ao s); (a_, b) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>))\<^sup>*; (a_, b) \<in> (vs_lookup1 s)\<^sup>*; (b, c) \<in> vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); (b, c) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> (a_, c) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); ako_at ao pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); (\<exists>rs. (rs \<rhd> pa) s) \<longrightarrow> (\<forall>ao. ako_at ao pa s \<longrightarrow> valid_vspace_obj ao s); \<exists>ref. (ref \<rhd> pa) s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); ako_at ao pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); \<forall>ao. ako_at ao pa s \<longrightarrow> valid_vspace_obj ao s; \<exists>ref. (ref \<rhd> pa) s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); ako_at ao pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); \<exists>ref. (ref \<rhd> pa) s; ako_at ao pa s \<longrightarrow> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); ako_at ao pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); \<exists>ref. (ref \<rhd> pa) s; ako_at ao pa s \<longrightarrow> valid_vspace_obj ao s; pa = p\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>)
 2. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); ako_at ao pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); \<exists>ref. (ref \<rhd> pa) s; ako_at ao pa s \<longrightarrow> valid_vspace_obj ao s; pa \<noteq> p\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>ref x. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); \<forall>x. valid_pte (pt x) s; (rs \<rhd> p) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); ao = PageTable pt; pt = opt \<longrightarrow> (\<forall>x. valid_pte (opt x) s); pa = p; (ref \<rhd> p) s\<rbrakk> \<Longrightarrow> valid_pte (pt x) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>)
 2. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); ako_at ao pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); \<exists>ref. (ref \<rhd> pa) s; ako_at ao pa s \<longrightarrow> valid_vspace_obj ao s; pa \<noteq> p\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); \<forall>x. valid_pte (pt x) s; (rs \<rhd> p) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); ao = PageTable pt; pt = opt \<longrightarrow> (\<forall>x. valid_pte (opt x) s); pa = p; (ref_ \<rhd> p) s\<rbrakk> \<Longrightarrow> valid_pte (pt x) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (rs \<rhd> p) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); ao = PageTable pt; pt = opt \<longrightarrow> (\<forall>x. valid_pte (opt x) s); pa = p; (ref_ \<rhd> p) s; valid_pte (pt x) s\<rbrakk> \<Longrightarrow> valid_pte (pt x) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); ako_at ao pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); \<exists>ref. (ref \<rhd> pa) s; ako_at ao pa s \<longrightarrow> valid_vspace_obj ao s; pa \<noteq> p\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>x1. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); kheap s pa = Some (ArchObj (ASIDPool x1)); \<exists>ref. (ref \<rhd> pa) s; \<forall>x\<in>ran x1. \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory; pa \<noteq> p; ao = ASIDPool x1\<rbrakk> \<Longrightarrow> \<forall>x\<in>ran x1. x \<noteq> p
 2. \<And>x2. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); kheap s pa = Some (ArchObj (PageTable x2)); \<exists>ref. (ref \<rhd> pa) s; \<forall>x. valid_pte (x2 x) s; pa \<noteq> p; ao = PageTable x2\<rbrakk> \<Longrightarrow> \<forall>x. valid_pte (x2 x) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>)
 3. \<And>x3. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); kheap s pa = Some (ArchObj (PageDirectory x3)); \<exists>ref. (ref \<rhd> pa) s; \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) s; pa \<noteq> p; ao = PageDirectory x3\<rbrakk> \<Longrightarrow> \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>x1 ref. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); kheap s pa = Some (ArchObj (ASIDPool x1)); \<forall>x\<in>ran x1. \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory; pa \<noteq> p; ao = ASIDPool x1; p \<in> ran x1; (ref \<rhd> pa) s\<rbrakk> \<Longrightarrow> False
 2. \<And>x2. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); kheap s pa = Some (ArchObj (PageTable x2)); \<exists>ref. (ref \<rhd> pa) s; \<forall>x. valid_pte (x2 x) s; pa \<noteq> p; ao = PageTable x2\<rbrakk> \<Longrightarrow> \<forall>x. valid_pte (x2 x) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>)
 3. \<And>x3. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); kheap s pa = Some (ArchObj (PageDirectory x3)); \<exists>ref. (ref \<rhd> pa) s; \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) s; pa \<noteq> p; ao = PageDirectory x3\<rbrakk> \<Longrightarrow> \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); kheap s pa = Some (ArchObj (PageTable x2)); \<exists>ref. (ref \<rhd> pa) s; \<forall>x. valid_pte (x2 x) s; pa \<noteq> p; ao = PageTable x2\<rbrakk> \<Longrightarrow> \<forall>x. valid_pte (x2 x) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>)
 2. \<And>x3. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); kheap s pa = Some (ArchObj (PageDirectory x3)); \<exists>ref. (ref \<rhd> pa) s; \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) s; pa \<noteq> p; ao = PageDirectory x3\<rbrakk> \<Longrightarrow> \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>x2 ref x. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); kheap s pa = Some (ArchObj (PageTable x2)); \<forall>x. valid_pte (x2 x) s; pa \<noteq> p; ao = PageTable x2; (ref \<rhd> pa) s\<rbrakk> \<Longrightarrow> valid_pte (x2 x) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>)
 2. \<And>x3. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); kheap s pa = Some (ArchObj (PageDirectory x3)); \<exists>ref. (ref \<rhd> pa) s; \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) s; pa \<noteq> p; ao = PageDirectory x3\<rbrakk> \<Longrightarrow> \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); kheap s pa = Some (ArchObj (PageTable fun)); \<forall>x. valid_pte (fun x) s; pa \<noteq> p; ao = PageTable fun; (ref_ \<rhd> pa) s\<rbrakk> \<Longrightarrow> valid_pte (fun x) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); kheap s pa = Some (ArchObj (PageTable fun)); pa \<noteq> p; ao = PageTable fun; (ref_ \<rhd> pa) s; valid_pte (fun x) s\<rbrakk> \<Longrightarrow> valid_pte (fun x) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); kheap s pa = Some (ArchObj (PageDirectory x3)); \<exists>ref. (ref \<rhd> pa) s; \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) s; pa \<noteq> p; ao = PageDirectory x3\<rbrakk> \<Longrightarrow> \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>x3 x ref. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); kheap s pa = Some (ArchObj (PageDirectory x3)); \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) s; pa \<noteq> p; ao = PageDirectory x3; x \<notin> kernel_mapping_slots; (ref \<rhd> pa) s\<rbrakk> \<Longrightarrow> valid_pde (x3 x) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>x3 x ref. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); kheap s pa = Some (ArchObj (PageDirectory x3)); pa \<noteq> p; ao = PageDirectory x3; x \<notin> kernel_mapping_slots; (ref \<rhd> pa) s; valid_pde (x3 x) s\<rbrakk> \<Longrightarrow> valid_pde (x3 x) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some (ArchObj (PageTable opt)); (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); (rs \<rhd> pa) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>); kheap s pa = Some (ArchObj (PageDirectory fun)); pa \<noteq> p; ao = PageDirectory fun; x \<notin> kernel_mapping_slots; (ref_ \<rhd> pa) s; valid_pde (fun x) s\<rbrakk> \<Longrightarrow> valid_pde (fun x) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!