kings-crown/FVELER_Isabelle huggingface dataset:
theory InvariantsPre_AI

lemma a_typeE:
  "\<lbrakk>a_type ko = ACapTable sz; (\<And>cs. \<lbrakk> ko = CNode sz cs; well_formed_cnode_n sz cs \<rbrakk> \<Longrightarrow> R)\<rbrakk> \<Longrightarrow> R"
  "\<lbrakk>a_type ko = ATCB; (\<And>tcb. ko = TCB tcb \<Longrightarrow> R)\<rbrakk> \<Longrightarrow> R"
  "\<lbrakk>a_type ko = AEndpoint; (\<And>ep. ko = Endpoint ep \<Longrightarrow> R)\<rbrakk> \<Longrightarrow> R"
  "\<lbrakk>a_type ko = ANTFN; (\<And>ntfn. ko = Notification ntfn \<Longrightarrow> R)\<rbrakk> \<Longrightarrow> R"
  "\<lbrakk>a_type ko = AArch T; (\<And>ao. \<lbrakk> ko = ArchObj ao; aa_type ao = T \<rbrakk> \<Longrightarrow> R)\<rbrakk> \<Longrightarrow> R"
  "\<lbrakk>a_type ko = AGarbage sz;
    (\<And>sz' cs. \<lbrakk> ko = CNode (sz - cte_level_bits) cs; \<not>well_formed_cnode_n sz' cs;
                cte_level_bits \<le> sz \<rbrakk> \<Longrightarrow> R)\<rbrakk>
   \<Longrightarrow> R" by (cases ko; clarsimp simp add: a_type_def split: if_split_asm)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<lbrakk>a_type ko = ACapTable sz; \<And>cs. \<lbrakk>ko = CNode sz cs; well_formed_cnode_n sz cs\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R) &&& (\<lbrakk>a_type ko = ATCB; \<And>tcb. ko = TCB tcb \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R) &&& (\<lbrakk>a_type ko = AEndpoint; \<And>ep. ko = Endpoint ep \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R)) &&& (\<lbrakk>a_type ko = ANTFN; \<And>ntfn. ko = Notification ntfn \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R) &&& (\<lbrakk>a_type ko = AArch T; \<And>ao. \<lbrakk>ko = ArchObj ao; aa_type ao = T\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R) &&& (\<lbrakk>a_type ko = AGarbage sz; \<And>sz' cs. \<lbrakk>ko = CNode (sz - cte_level_bits) cs; \<not> well_formed_cnode_n sz' cs; cte_level_bits \<le> sz\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R)
theory InvariantsPre_AI

lemma typ_at_typs_of:
  "typ_at T p s = (typs_of s p = Some T)" by (auto simp: obj_at_def in_opt_map_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. typ_at T p s = (typs_of s p = Some T)
theory InvariantsPre_AI

lemma pd_shifting_gen:
  "\<lbrakk>b \<le> a; size pd - c \<le> a - b; is_aligned pd c \<rbrakk> \<Longrightarrow> pd + (vptr >> a << b) && ~~ mask c = pd" apply (subgoal_tac "(vptr >> a << b) && ~~ mask c = 0") apply (subst word_plus_and_or_coroll) apply (erule aligned_mask_disjoint) apply (simp add: and_mask_0_iff_le_mask[symmetric]) apply (simp add: bit.conj_disj_distrib2) apply (simp add: shiftr_shiftl1 neg_mask_twice word_bw_assocs) apply (rule shiftr_not_mask_0) apply (fastforce simp: max_def word_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b \<le> a; size pd - c \<le> a - b; is_aligned pd c\<rbrakk> \<Longrightarrow> pd + (vptr >> a << b) && ~~ mask c = pd proof (prove)
goal (2 subgoals):
 1. \<lbrakk>b \<le> a; size pd - c \<le> a - b; is_aligned pd c; (vptr >> a << b) && ~~ mask c = 0\<rbrakk> \<Longrightarrow> pd + (vptr >> a << b) && ~~ mask c = pd
 2. \<lbrakk>b \<le> a; size pd - c \<le> a - b; is_aligned pd c\<rbrakk> \<Longrightarrow> (vptr >> a << b) && ~~ mask c = 0 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>b \<le> a; size pd - c \<le> a - b; is_aligned pd c; (vptr >> a << b) && ~~ mask c = 0\<rbrakk> \<Longrightarrow> pd && (vptr >> a << b) = 0
 2. \<lbrakk>b \<le> a; size pd - c \<le> a - b; is_aligned pd c; (vptr >> a << b) && ~~ mask c = 0\<rbrakk> \<Longrightarrow> (pd || (vptr >> a << b)) && ~~ mask c = pd
 3. \<lbrakk>b \<le> a; size pd - c \<le> a - b; is_aligned pd c\<rbrakk> \<Longrightarrow> (vptr >> a << b) && ~~ mask c = 0 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>b \<le> a; size pd - c \<le> a - b; (vptr >> a << b) && ~~ mask c = 0\<rbrakk> \<Longrightarrow> vptr >> a << b \<le> mask c
 2. \<lbrakk>b \<le> a; size pd - c \<le> a - b; is_aligned pd c; (vptr >> a << b) && ~~ mask c = 0\<rbrakk> \<Longrightarrow> (pd || (vptr >> a << b)) && ~~ mask c = pd
 3. \<lbrakk>b \<le> a; size pd - c \<le> a - b; is_aligned pd c\<rbrakk> \<Longrightarrow> (vptr >> a << b) && ~~ mask c = 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>b \<le> a; size pd - c \<le> a - b; is_aligned pd c; (vptr >> a << b) && ~~ mask c = 0\<rbrakk> \<Longrightarrow> (pd || (vptr >> a << b)) && ~~ mask c = pd
 2. \<lbrakk>b \<le> a; size pd - c \<le> a - b; is_aligned pd c\<rbrakk> \<Longrightarrow> (vptr >> a << b) && ~~ mask c = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b \<le> a; size pd - c \<le> a - b; is_aligned pd c\<rbrakk> \<Longrightarrow> (vptr >> a << b) && ~~ mask c = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b \<le> a; size pd - c \<le> a - b; is_aligned pd c\<rbrakk> \<Longrightarrow> (vptr >> a - b) && ~~ mask (max b c) = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b \<le> a; size pd - c \<le> a - b; is_aligned pd c\<rbrakk> \<Longrightarrow> LENGTH('a) \<le> a - b + max b c proof (prove)
goal:
No subgoals!
theory ArchInvariants_AI

lemma iarch_tcb_set_registers[simp]:
  "arch_tcb_to_iarch_tcb (arch_tcb_set_registers regs arch_tcb)
     = arch_tcb_to_iarch_tcb arch_tcb" by (simp add: arch_tcb_set_registers_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_tcb_to_iarch_tcb (arch_tcb_set_registers regs arch_tcb) = arch_tcb_to_iarch_tcb arch_tcb
theory ArchInvariants_AI

lemma arch_cap_fun_lift_expand[simp]:
  "(arch_cap_fun_lift (\<lambda> ac. case ac of
                                ASIDPoolCap obj_ref asid \<Rightarrow> P_ASIDPoolCap obj_ref asid
                              | ASIDControlCap \<Rightarrow> P_ASIDControlCap
                              | PageCap dev obj_ref rights sz vr \<Rightarrow> P_PageCap dev obj_ref rights sz vr
                              | PageTableCap obj_ref vr \<Rightarrow> P_PageTableCap obj_ref vr
                              | PageDirectoryCap obj_ref asid \<Rightarrow> P_PageDirectoryCap obj_ref asid)
                      F) = (\<lambda>c.
   (case c of
      ArchObjectCap (ASIDPoolCap obj_ref asid) \<Rightarrow> P_ASIDPoolCap obj_ref asid
    | ArchObjectCap (ASIDControlCap) \<Rightarrow> P_ASIDControlCap
    | ArchObjectCap (PageCap dev obj_ref rights sz vr) \<Rightarrow> P_PageCap dev obj_ref rights sz vr
    | ArchObjectCap (PageTableCap obj_ref vr) \<Rightarrow> P_PageTableCap obj_ref vr
    | ArchObjectCap (PageDirectoryCap obj_ref asid) \<Rightarrow> P_PageDirectoryCap obj_ref asid
    | _ \<Rightarrow> F))" apply (rule ext) by (simp add: arch_cap_fun_lift_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_cap_fun_lift (\<lambda>ac. case ac of ASIDPoolCap obj_ref asid \<Rightarrow> P_ASIDPoolCap obj_ref asid | ASIDControlCap \<Rightarrow> P_ASIDControlCap | PageCap dev obj_ref rights sz vr \<Rightarrow> P_PageCap dev obj_ref rights sz vr | PageTableCap obj_ref vr \<Rightarrow> P_PageTableCap obj_ref vr | PageDirectoryCap obj_ref asid \<Rightarrow> P_PageDirectoryCap obj_ref asid) F = (\<lambda>c. case c of ArchObjectCap (ASIDPoolCap obj_ref asid) \<Rightarrow> P_ASIDPoolCap obj_ref asid | ArchObjectCap ASIDControlCap \<Rightarrow> P_ASIDControlCap | ArchObjectCap (PageCap dev obj_ref rights sz vr) \<Rightarrow> P_PageCap dev obj_ref rights sz vr | ArchObjectCap (PageTableCap obj_ref vr) \<Rightarrow> P_PageTableCap obj_ref vr | ArchObjectCap (PageDirectoryCap obj_ref asid) \<Rightarrow> P_PageDirectoryCap obj_ref asid | _ \<Rightarrow> F) proof (prove)
goal (1 subgoal):
 1. \<And>c. arch_cap_fun_lift (\<lambda>ac. case ac of ASIDPoolCap obj_ref asid \<Rightarrow> P_ASIDPoolCap obj_ref asid | ASIDControlCap \<Rightarrow> P_ASIDControlCap | PageCap dev obj_ref rights sz vr \<Rightarrow> P_PageCap dev obj_ref rights sz vr | PageTableCap obj_ref vr \<Rightarrow> P_PageTableCap obj_ref vr | PageDirectoryCap obj_ref asid \<Rightarrow> P_PageDirectoryCap obj_ref asid) F c = (case c of ArchObjectCap (ASIDPoolCap obj_ref asid) \<Rightarrow> P_ASIDPoolCap obj_ref asid | ArchObjectCap ASIDControlCap \<Rightarrow> P_ASIDControlCap | ArchObjectCap (PageCap dev obj_ref rights sz vr) \<Rightarrow> P_PageCap dev obj_ref rights sz vr | ArchObjectCap (PageTableCap obj_ref vr) \<Rightarrow> P_PageTableCap obj_ref vr | ArchObjectCap (PageDirectoryCap obj_ref asid) \<Rightarrow> P_PageDirectoryCap obj_ref asid | _ \<Rightarrow> F)
theory ArchInvariants_AI

lemma typ_at_pg_user:
  "typ_at (AArch (AUserData sz)) buf s = ko_at (ArchObj (DataPage False sz)) buf s" unfolding obj_at_def by (auto simp: a_type_def split: Structures_A.kernel_object.split_asm arch_kernel_obj.split_asm if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. typ_at (AArch (AUserData sz)) buf s = ako_at (DataPage False sz) buf s proof (prove)
goal (1 subgoal):
 1. (\<exists>ko. kheap s buf = Some ko \<and> a_type ko = AArch (AUserData sz)) = (\<exists>ko. kheap s buf = Some ko \<and> ArchObj (DataPage False sz) = ko)
theory ArchInvariants_AI

lemma typ_at_pg_device:
  "typ_at (AArch (ADeviceData sz)) buf s = ko_at (ArchObj (DataPage True sz)) buf s" unfolding obj_at_def by (auto simp: a_type_def split: Structures_A.kernel_object.split_asm arch_kernel_obj.split_asm if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. typ_at (AArch (ADeviceData sz)) buf s = ako_at (DataPage True sz) buf s proof (prove)
goal (1 subgoal):
 1. (\<exists>ko. kheap s buf = Some ko \<and> a_type ko = AArch (ADeviceData sz)) = (\<exists>ko. kheap s buf = Some ko \<and> ArchObj (DataPage True sz) = ko)
theory ArchInvariants_AI

lemma wellformed_arch_pspace: "\<And>ao. \<lbrakk>arch_valid_obj ao s; kheap s = kheap s'\<rbrakk>
          \<Longrightarrow> arch_valid_obj ao s'" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>ao. \<lbrakk>arch_valid_obj ao s; kheap s = kheap s'\<rbrakk> \<Longrightarrow> arch_valid_obj ao s'
theory ArchInvariants_AI

lemma is_arch_cap_simps:
  "is_pg_cap cap = (\<exists>dev p R sz m. cap = (ArchObjectCap (PageCap dev p R sz m)))"
  "is_pd_cap cap = (\<exists>p asid. cap = (ArchObjectCap (PageDirectoryCap p asid)))"
  "is_pt_cap cap = (\<exists>p asid. cap = (ArchObjectCap (PageTableCap p asid)))" by (auto simp add: is_pg_cap_def is_pd_cap_def is_pt_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_pg_cap cap = (\<exists>dev p R sz m. cap = ArchObjectCap (PageCap dev p R sz m)) &&& is_pd_cap cap = (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) &&& is_pt_cap cap = (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))
theory ArchInvariants_AI

lemma vmsz_aligned_ARMSection:
  "vmsz_aligned vref ARMSection = is_aligned vref (pageBitsForSize ARMSection)" by (simp add: vmsz_aligned_def pageBitsForSize_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vmsz_aligned vref ARMSection = is_aligned vref (pageBitsForSize ARMSection)
theory ArchInvariants_AI

lemma valid_arch_cap_def2:
  "valid_arch_cap c s \<equiv> wellformed_acap c \<and> valid_arch_cap_ref c s" apply (rule eq_reflection) apply (cases c) by (auto simp add: wellformed_acap_simps valid_arch_cap_simps
                       valid_arch_cap_ref_simps vmsz_aligned_ARMSection
                split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_arch_cap c s \<equiv> wellformed_acap c \<and> valid_arch_cap_ref c s proof (prove)
goal (1 subgoal):
 1. valid_arch_cap c s = (wellformed_acap c \<and> valid_arch_cap_ref c s) proof (prove)
goal (5 subgoals):
 1. \<And>x11 x12. c = ASIDPoolCap x11 x12 \<Longrightarrow> valid_arch_cap c s = (wellformed_acap c \<and> valid_arch_cap_ref c s)
 2. c = ASIDControlCap \<Longrightarrow> valid_arch_cap c s = (wellformed_acap c \<and> valid_arch_cap_ref c s)
 3. \<And>x31 x32 x33 x34 x35. c = PageCap x31 x32 x33 x34 x35 \<Longrightarrow> valid_arch_cap c s = (wellformed_acap c \<and> valid_arch_cap_ref c s)
 4. \<And>x41 x42. c = PageTableCap x41 x42 \<Longrightarrow> valid_arch_cap c s = (wellformed_acap c \<and> valid_arch_cap_ref c s)
 5. \<And>x51 x52. c = PageDirectoryCap x51 x52 \<Longrightarrow> valid_arch_cap c s = (wellformed_acap c \<and> valid_arch_cap_ref c s)
theory ArchInvariants_AI

lemma vs_lookup1_obj_at:
  "((rs,p) \<rhd>1 (r # rs,p')) s = obj_at (\<lambda>ko. (r, p') \<in> vs_refs ko) p s" by (fastforce simp: vs_lookup1_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (((rs, p), r # rs, p') \<in> vs_lookup1 s) = obj_at (\<lambda>ko. (r, p') \<in> vs_refs ko) p s
theory ArchInvariants_AI

lemma vs_lookup1I:
  "\<lbrakk> ko_at ko p s; (r, p') \<in> vs_refs ko;
          rs' = r # rs \<rbrakk> \<Longrightarrow> ((rs,p) \<rhd>1 (rs',p')) s" by (fastforce simp add: vs_lookup1_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at ko p s; (r, p') \<in> vs_refs ko; rs' = r # rs\<rbrakk> \<Longrightarrow> ((rs, p), rs', p') \<in> vs_lookup1 s
theory ArchInvariants_AI

lemma vs_lookup_pages1I:
  "\<lbrakk> ko_at ko p s; (r, p') \<in> vs_refs_pages ko;
          rs' = r # rs \<rbrakk> \<Longrightarrow> ((rs,p) \<unrhd>1 (rs',p')) s" by (fastforce simp add: vs_lookup_pages1_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at ko p s; (r, p') \<in> vs_refs_pages ko; rs' = r # rs\<rbrakk> \<Longrightarrow> ((rs, p), rs', p') \<in> vs_lookup_pages1 s
theory ArchInvariants_AI

lemma vs_lookup1D:
  "(x \<rhd>1 y) s \<Longrightarrow> \<exists>rs r p p' ko. x = (rs,p) \<and> y = (r # rs,p')
                          \<and> ko_at ko p s \<and> (r,p') \<in> vs_refs ko" by (cases x, cases y) (fastforce simp: vs_lookup1_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> vs_lookup1 s \<Longrightarrow> \<exists>rs r p p' ko. x = (rs, p) \<and> y = (r # rs, p') \<and> ko_at ko p s \<and> (r, p') \<in> vs_refs ko
theory ArchInvariants_AI

lemma vs_lookup_pages1D:
  "(x \<unrhd>1 y) s \<Longrightarrow> \<exists>rs r p p' ko. x = (rs,p) \<and> y = (r # rs,p')
                          \<and> ko_at ko p s \<and> (r,p') \<in> vs_refs_pages ko" by (cases x, cases y) (fastforce simp: vs_lookup_pages1_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> vs_lookup_pages1 s \<Longrightarrow> \<exists>rs r p p' ko. x = (rs, p) \<and> y = (r # rs, p') \<and> ko_at ko p s \<and> (r, p') \<in> vs_refs_pages ko
theory ArchInvariants_AI

lemma vs_lookup1_stateI:
  assumes 1: "(r \<rhd>1 r') s"
  assumes ko: "\<And>ko. ko_at ko (snd r) s \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') (snd r) s'"
  shows "(r \<rhd>1 r') s'" using 1 ko by (fastforce simp: obj_at_def vs_lookup1_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (r, r') \<in> vs_lookup1 s' proof (prove)
using this:
(r, r') \<in> vs_lookup1 s
ko_at ?ko (snd r) s \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs ?ko \<subseteq> vs_refs ko') (snd r) s'

goal (1 subgoal):
 1. (r, r') \<in> vs_lookup1 s'
theory ArchInvariants_AI

lemma vs_lookup_pages1_stateI2:
  assumes 1: "(r \<unrhd>1 r') s"
  assumes ko: "\<And>ko. \<lbrakk> ko_at ko (snd r) s; vs_refs_pages ko \<noteq> {} \<rbrakk>
               \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs_pages ko \<subseteq> vs_refs_pages ko') (snd r) s'"
  shows "(r \<unrhd>1 r') s'" using 1 ko by (fastforce simp: obj_at_def vs_lookup_pages1_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (r, r') \<in> vs_lookup_pages1 s' proof (prove)
using this:
(r, r') \<in> vs_lookup_pages1 s
\<lbrakk>ko_at ?ko (snd r) s; vs_refs_pages ?ko \<noteq> {}\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs_pages ?ko \<subseteq> vs_refs_pages ko') (snd r) s'

goal (1 subgoal):
 1. (r, r') \<in> vs_lookup_pages1 s'
theory ArchInvariants_AI

lemma vs_lookup_trans_sub:
  assumes ko: "\<And>ko p. ko_at ko p s \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s'"
  shows "vs_lookup_trans s \<subseteq> vs_lookup_trans s'" proof - have "vs_lookup1 s \<subseteq> vs_lookup1 s'" by (fastforce dest: ko elim: vs_lookup1_stateI) thus ?thesis by (rule rtrancl_mono) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (vs_lookup1 s)\<^sup>* \<subseteq> (vs_lookup1 s')\<^sup>* proof (state)
goal (1 subgoal):
 1. (vs_lookup1 s)\<^sup>* \<subseteq> (vs_lookup1 s')\<^sup>* proof (prove)
goal (1 subgoal):
 1. vs_lookup1 s \<subseteq> vs_lookup1 s' proof (state)
this:
vs_lookup1 s \<subseteq> vs_lookup1 s'

goal (1 subgoal):
 1. (vs_lookup1 s)\<^sup>* \<subseteq> (vs_lookup1 s')\<^sup>* proof (prove)
using this:
vs_lookup1 s \<subseteq> vs_lookup1 s'

goal (1 subgoal):
 1. (vs_lookup1 s)\<^sup>* \<subseteq> (vs_lookup1 s')\<^sup>* proof (state)
this:
(vs_lookup1 s)\<^sup>* \<subseteq> (vs_lookup1 s')\<^sup>*

goal:
No subgoals!
theory ArchInvariants_AI

lemma vs_lookup_sub:
  assumes ko: "\<And>ko p. ko_at ko p s \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s'"
  assumes table: "graph_of (arm_asid_table (arch_state s)) \<subseteq> graph_of (arm_asid_table (arch_state s'))"
  shows "vs_lookup s \<subseteq> vs_lookup s'" unfolding vs_lookup_def apply (rule Image_mono) apply (rule vs_lookup_trans_sub) apply (erule ko) apply (unfold vs_asid_refs_def) apply (rule image_mono) apply (rule table) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vs_lookup s \<subseteq> vs_lookup s' proof (prove)
goal (1 subgoal):
 1. (vs_lookup1 s)\<^sup>* `` vs_asid_refs (asid_table s) \<subseteq> (vs_lookup1 s')\<^sup>* `` vs_asid_refs (asid_table s') proof (prove)
goal (2 subgoals):
 1. (vs_lookup1 s)\<^sup>* \<subseteq> (vs_lookup1 s')\<^sup>*
 2. vs_asid_refs (asid_table s) \<subseteq> vs_asid_refs (asid_table s') proof (prove)
goal (2 subgoals):
 1. \<And>ko p. ko_at ko p s \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s'
 2. vs_asid_refs (asid_table s) \<subseteq> vs_asid_refs (asid_table s') proof (prove)
goal (1 subgoal):
 1. vs_asid_refs (asid_table s) \<subseteq> vs_asid_refs (asid_table s') proof (prove)
goal (1 subgoal):
 1. (\<lambda>(r, p). ([VSRef (UCAST(7 \<rightarrow> 32) r) None], p)) ` graph_of (asid_table s) \<subseteq> (\<lambda>(r, p). ([VSRef (UCAST(7 \<rightarrow> 32) r) None], p)) ` graph_of (asid_table s') proof (prove)
goal (1 subgoal):
 1. graph_of (asid_table s) \<subseteq> graph_of (asid_table s') proof (prove)
goal:
No subgoals!
theory ArchInvariants_AI

lemma vs_lookup_pages_trans_sub:
  assumes ko: "\<And>ko p. ko_at ko p s \<Longrightarrow>
                      obj_at (\<lambda>ko'. vs_refs_pages ko \<subseteq> vs_refs_pages ko') p s'"
  shows "vs_lookup_pages_trans s \<subseteq> vs_lookup_pages_trans s'" proof - have "vs_lookup_pages1 s \<subseteq> vs_lookup_pages1 s'" by (fastforce simp add: ko elim: vs_lookup_pages1_stateI) thus ?thesis by (rule rtrancl_mono) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (vs_lookup_pages1 s)\<^sup>* \<subseteq> (vs_lookup_pages1 s')\<^sup>* proof (state)
goal (1 subgoal):
 1. (vs_lookup_pages1 s)\<^sup>* \<subseteq> (vs_lookup_pages1 s')\<^sup>* proof (prove)
goal (1 subgoal):
 1. vs_lookup_pages1 s \<subseteq> vs_lookup_pages1 s' proof (state)
this:
vs_lookup_pages1 s \<subseteq> vs_lookup_pages1 s'

goal (1 subgoal):
 1. (vs_lookup_pages1 s)\<^sup>* \<subseteq> (vs_lookup_pages1 s')\<^sup>* proof (prove)
using this:
vs_lookup_pages1 s \<subseteq> vs_lookup_pages1 s'

goal (1 subgoal):
 1. (vs_lookup_pages1 s)\<^sup>* \<subseteq> (vs_lookup_pages1 s')\<^sup>* proof (state)
this:
(vs_lookup_pages1 s)\<^sup>* \<subseteq> (vs_lookup_pages1 s')\<^sup>*

goal:
No subgoals!
theory ArchInvariants_AI

lemma vs_lookup_pages_sub:
  assumes ko: "\<And>ko p. ko_at ko p s \<Longrightarrow>
                      obj_at (\<lambda>ko'. vs_refs_pages ko \<subseteq> vs_refs_pages ko') p s'"
  assumes table:
    "graph_of (arm_asid_table (arch_state s)) \<subseteq>
     graph_of (arm_asid_table (arch_state s'))"
  shows "vs_lookup_pages s \<subseteq> vs_lookup_pages s'" unfolding vs_lookup_pages_def apply (rule Image_mono) apply (rule vs_lookup_pages_trans_sub) apply (erule ko) apply (unfold vs_asid_refs_def) apply (rule image_mono) apply (rule table) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vs_lookup_pages s \<subseteq> vs_lookup_pages s' proof (prove)
goal (1 subgoal):
 1. (vs_lookup_pages1 s)\<^sup>* `` vs_asid_refs (asid_table s) \<subseteq> (vs_lookup_pages1 s')\<^sup>* `` vs_asid_refs (asid_table s') proof (prove)
goal (2 subgoals):
 1. (vs_lookup_pages1 s)\<^sup>* \<subseteq> (vs_lookup_pages1 s')\<^sup>*
 2. vs_asid_refs (asid_table s) \<subseteq> vs_asid_refs (asid_table s') proof (prove)
goal (2 subgoals):
 1. \<And>ko p. ko_at ko p s \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs_pages ko \<subseteq> vs_refs_pages ko') p s'
 2. vs_asid_refs (asid_table s) \<subseteq> vs_asid_refs (asid_table s') proof (prove)
goal (1 subgoal):
 1. vs_asid_refs (asid_table s) \<subseteq> vs_asid_refs (asid_table s') proof (prove)
goal (1 subgoal):
 1. (\<lambda>(r, p). ([VSRef (UCAST(7 \<rightarrow> 32) r) None], p)) ` graph_of (asid_table s) \<subseteq> (\<lambda>(r, p). ([VSRef (UCAST(7 \<rightarrow> 32) r) None], p)) ` graph_of (asid_table s') proof (prove)
goal (1 subgoal):
 1. graph_of (asid_table s) \<subseteq> graph_of (asid_table s') proof (prove)
goal:
No subgoals!
theory ArchInvariants_AI

lemma vs_lookup_pagesI:
  "\<lbrakk> ref' \<in> vs_asid_refs (arm_asid_table (arch_state s));
     (ref',(ref,p)) \<in> (vs_lookup_pages1 s)^*  \<rbrakk> \<Longrightarrow>
  (ref \<unrhd> p) s" by (simp add: vs_lookup_pages_def) blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ref' \<in> vs_asid_refs (asid_table s); (ref', ref, p) \<in> (vs_lookup_pages1 s)\<^sup>*\<rbrakk> \<Longrightarrow> (ref \<unrhd> p) s
theory ArchInvariants_AI

lemma vs_lookup_pages_stateI:
  assumes 1: "(ref \<unrhd> p) s"
  assumes ko: "\<And>ko p. ko_at ko p s \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs_pages ko \<subseteq> vs_refs_pages ko') p s'"
  assumes table: "graph_of (arm_asid_table (arch_state s)) \<subseteq> graph_of (arm_asid_table (arch_state s'))"
  shows "(ref \<unrhd> p) s'" using 1 vs_lookup_pages_sub [OF ko table] by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (ref \<unrhd> p) s' proof (prove)
using this:
(ref \<unrhd> p) s
(\<And>ko p. ko_at ko p s \<Longrightarrow> ko_at ko p s) \<Longrightarrow> vs_lookup_pages s \<subseteq> vs_lookup_pages s'

goal (1 subgoal):
 1. (ref \<unrhd> p) s'
theory ArchInvariants_AI

lemma vs_lookup_stateI:
  assumes 1: "(ref \<rhd> p) s"
  assumes ko: "\<And>ko p. ko_at ko p s \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s'"
  assumes table: "graph_of (arm_asid_table (arch_state s)) \<subseteq> graph_of (arm_asid_table (arch_state s'))"
  shows "(ref \<rhd> p) s'" using 1 vs_lookup_sub [OF ko table] by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (ref \<rhd> p) s' proof (prove)
using this:
(ref \<rhd> p) s
(\<And>ko p. ko_at ko p s \<Longrightarrow> ko_at ko p s) \<Longrightarrow> vs_lookup s \<subseteq> vs_lookup s'

goal (1 subgoal):
 1. (ref \<rhd> p) s'