theory ArchDetype_AI

lemma vs_lookup_pages: (* SIMP *)
  "vs_lookup_pages (detype (untyped_range cap) s) = vs_lookup_pages s" apply (rule set_eqI) apply clarsimp apply (rule iffI) apply (erule vs_lookup_pages_induct) apply (simp add: arch_state_det) apply (erule vs_lookup_pages_atI) apply (erule vs_lookup_pages_step) apply (clarsimp simp: vs_lookup_pages1_def) apply (erule vs_lookup_pages_induct) apply (rule vs_lookup_pages_atI) apply (simp add: arch_state_det) apply (erule vs_lookup_pages_step) apply (clarsimp simp: vs_lookup_pages1_def) apply (drule valid_vs_lookupD, rule valid_vs_lookup) apply (elim conjE exE) apply (insert cap) apply (simp add: cte_wp_at_caps_of_state) apply (drule untyped_mdbD, rule untyped, assumption) apply blast apply (rule ut_mdb) apply (drule descendants_range_inD[OF drange]) apply (simp add: cte_wp_at_caps_of_state) apply (simp add: cap_range_def) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vs_lookup_pages (detype (untyped_range cap) s) = vs_lookup_pages s proof (prove)
goal (1 subgoal):
 1. \<And>x. (x \<in> vs_lookup_pages (detype (untyped_range cap) s)) = (x \<in> vs_lookup_pages s) proof (prove)
goal (1 subgoal):
 1. \<And>a b. (a \<unrhd> b) (detype (untyped_range cap) s) = (a \<unrhd> b) s proof (prove)
goal (2 subgoals):
 1. \<And>a b. (a \<unrhd> b) (detype (untyped_range cap) s) \<Longrightarrow> (a \<unrhd> b) s
 2. \<And>a b. (a \<unrhd> b) s \<Longrightarrow> (a \<unrhd> b) (detype (untyped_range cap) s) proof (prove)
goal (3 subgoals):
 1. \<And>a b asid p. asid_table (detype (untyped_range cap) s) asid = Some p \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) asid) None] \<unrhd> p) s
 2. \<And>a b ref p ref' p'. \<lbrakk>(ref \<unrhd> p) (detype (untyped_range cap) s); ((ref, p), ref', p') \<in> vs_lookup_pages1 (detype (untyped_range cap) s); (ref \<unrhd> p) s\<rbrakk> \<Longrightarrow> (ref' \<unrhd> p') s
 3. \<And>a b. (a \<unrhd> b) s \<Longrightarrow> (a \<unrhd> b) (detype (untyped_range cap) s) proof (prove)
goal (3 subgoals):
 1. \<And>asid p. asid_table s asid = Some p \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) asid) None] \<unrhd> p) s
 2. \<And>a b ref p ref' p'. \<lbrakk>(ref \<unrhd> p) (detype (untyped_range cap) s); ((ref, p), ref', p') \<in> vs_lookup_pages1 (detype (untyped_range cap) s); (ref \<unrhd> p) s\<rbrakk> \<Longrightarrow> (ref' \<unrhd> p') s
 3. \<And>a b. (a \<unrhd> b) s \<Longrightarrow> (a \<unrhd> b) (detype (untyped_range cap) s) proof (prove)
goal (2 subgoals):
 1. \<And>a b ref p ref' p'. \<lbrakk>(ref \<unrhd> p) (detype (untyped_range cap) s); ((ref, p), ref', p') \<in> vs_lookup_pages1 (detype (untyped_range cap) s); (ref \<unrhd> p) s\<rbrakk> \<Longrightarrow> (ref' \<unrhd> p') s
 2. \<And>a b. (a \<unrhd> b) s \<Longrightarrow> (a \<unrhd> b) (detype (untyped_range cap) s) proof (prove)
goal (2 subgoals):
 1. \<And>a b ref p ref' p'. \<lbrakk>(ref \<unrhd> p) (detype (untyped_range cap) s); ((ref, p), ref', p') \<in> vs_lookup_pages1 (detype (untyped_range cap) s)\<rbrakk> \<Longrightarrow> ((ref, p), ref', p') \<in> vs_lookup_pages1 s
 2. \<And>a b. (a \<unrhd> b) s \<Longrightarrow> (a \<unrhd> b) (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. \<And>a b. (a \<unrhd> b) s \<Longrightarrow> (a \<unrhd> b) (detype (untyped_range cap) s) proof (prove)
goal (2 subgoals):
 1. \<And>a b asid p. asid_table s asid = Some p \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) asid) None] \<unrhd> p) (detype (untyped_range cap) s)
 2. \<And>a b ref p ref' p'. \<lbrakk>(ref \<unrhd> p) s; ((ref, p), ref', p') \<in> vs_lookup_pages1 s; (ref \<unrhd> p) (detype (untyped_range cap) s)\<rbrakk> \<Longrightarrow> (ref' \<unrhd> p') (detype (untyped_range cap) s) proof (prove)
goal (2 subgoals):
 1. \<And>a b asid p. asid_table s asid = Some p \<Longrightarrow> asid_table (detype (untyped_range cap) s) asid = Some p
 2. \<And>a b ref p ref' p'. \<lbrakk>(ref \<unrhd> p) s; ((ref, p), ref', p') \<in> vs_lookup_pages1 s; (ref \<unrhd> p) (detype (untyped_range cap) s)\<rbrakk> \<Longrightarrow> (ref' \<unrhd> p') (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. \<And>a b ref p ref' p'. \<lbrakk>(ref \<unrhd> p) s; ((ref, p), ref', p') \<in> vs_lookup_pages1 s; (ref \<unrhd> p) (detype (untyped_range cap) s)\<rbrakk> \<Longrightarrow> (ref' \<unrhd> p') (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. \<And>a b ref p ref' p'. \<lbrakk>(ref \<unrhd> p) s; ((ref, p), ref', p') \<in> vs_lookup_pages1 s\<rbrakk> \<Longrightarrow> ((ref, p), ref', p') \<in> vs_lookup_pages1 (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. \<And>ref p p' ko r. \<lbrakk>(ref \<unrhd> p) s; ko_at ko p s; (r, p') \<in> vs_refs_pages ko; p \<in> untyped_range cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ref p p' ko r. \<lbrakk>ko_at ko p s; (r, p') \<in> vs_refs_pages ko; p \<in> untyped_range cap; \<exists>slot cap. caps_of_state s slot = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ref p p' ko r slot capa. \<lbrakk>ko_at ko p s; (r, p') \<in> vs_refs_pages ko; p \<in> untyped_range cap; caps_of_state s slot = Some capa; p \<in> obj_refs capa; vs_cap_ref capa = Some ref\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ref p p' ko r slot capa. \<lbrakk>ko_at ko p s; (r, p') \<in> vs_refs_pages ko; p \<in> untyped_range cap; caps_of_state s slot = Some capa; p \<in> obj_refs capa; vs_cap_ref capa = Some ref; cte_wp_at ((=) cap) ptr s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ref p p' ko r slot capa. \<lbrakk>ko_at ko p s; (r, p') \<in> vs_refs_pages ko; p \<in> untyped_range cap; caps_of_state s slot = Some capa; p \<in> obj_refs capa; vs_cap_ref capa = Some ref; caps_of_state s ptr = Some cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>ref p p' ko r slot capa. \<lbrakk>ko_at ko p s; (r, p') \<in> vs_refs_pages ko; p \<in> untyped_range cap; caps_of_state s slot = Some capa; p \<in> obj_refs capa; vs_cap_ref capa = Some ref\<rbrakk> \<Longrightarrow> obj_refs capa \<inter> untyped_range cap \<noteq> {}
 2. \<And>ref p p' ko r slot capa. \<lbrakk>ko_at ko p s; (r, p') \<in> vs_refs_pages ko; p \<in> untyped_range cap; caps_of_state s slot = Some capa; p \<in> obj_refs capa; vs_cap_ref capa = Some ref\<rbrakk> \<Longrightarrow> untyped_mdb (?m33 ref p p' ko r slot capa) (caps_of_state s)
 3. \<And>ref p p' ko r slot capa. \<lbrakk>ko_at ko p s; (r, p') \<in> vs_refs_pages ko; p \<in> untyped_range cap; caps_of_state s slot = Some capa; p \<in> obj_refs capa; vs_cap_ref capa = Some ref; slot \<in> descendants_of ptr (?m33 ref p p' ko r slot capa)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>ref p p' ko r slot capa. \<lbrakk>ko_at ko p s; (r, p') \<in> vs_refs_pages ko; p \<in> untyped_range cap; caps_of_state s slot = Some capa; p \<in> obj_refs capa; vs_cap_ref capa = Some ref\<rbrakk> \<Longrightarrow> untyped_mdb (?m33 ref p p' ko r slot capa) (caps_of_state s)
 2. \<And>ref p p' ko r slot capa. \<lbrakk>ko_at ko p s; (r, p') \<in> vs_refs_pages ko; p \<in> untyped_range cap; caps_of_state s slot = Some capa; p \<in> obj_refs capa; vs_cap_ref capa = Some ref; slot \<in> descendants_of ptr (?m33 ref p p' ko r slot capa)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ref p p' ko r slot capa. \<lbrakk>ko_at ko p s; (r, p') \<in> vs_refs_pages ko; p \<in> untyped_range cap; caps_of_state s slot = Some capa; p \<in> obj_refs capa; vs_cap_ref capa = Some ref; slot \<in> descendants_of ptr (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>ref p p' ko r slot capa. \<lbrakk>ko_at ko p s; (r, p') \<in> vs_refs_pages ko; p \<in> untyped_range cap; caps_of_state s slot = Some capa; p \<in> obj_refs capa; vs_cap_ref capa = Some ref\<rbrakk> \<Longrightarrow> caps_of_state s slot = Some (?cap50 ref p p' ko r slot capa)
 2. \<And>ref p p' ko r slot capa. \<lbrakk>ko_at ko p s; (r, p') \<in> vs_refs_pages ko; p \<in> untyped_range cap; caps_of_state s slot = Some capa; p \<in> obj_refs capa; vs_cap_ref capa = Some ref; cap_range (?cap50 ref p p' ko r slot capa) \<inter> cap_range cap = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ref p p' ko r slot capa. \<lbrakk>ko_at ko p s; (r, p') \<in> vs_refs_pages ko; p \<in> untyped_range cap; caps_of_state s slot = Some capa; p \<in> obj_refs capa; vs_cap_ref capa = Some ref; cap_range capa \<inter> cap_range cap = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ref p p' ko r slot capa. \<lbrakk>ko_at ko p s; (r, p') \<in> vs_refs_pages ko; p \<in> untyped_range cap; caps_of_state s slot = Some capa; p \<in> obj_refs capa; vs_cap_ref capa = Some ref; (untyped_range capa \<union> obj_refs capa) \<inter> (untyped_range cap \<union> obj_refs cap) = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!