kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchVSpace_AI

lemma lookup_pd_slot_kernel_mappings_set_strg:
  "is_aligned pd pd_bits \<and> vmsz_aligned vptr ARMSuperSection
     \<and> vptr < kernel_base
          \<longrightarrow>
   (\<forall>x\<in>set [0 , 4 .e. 0x3C]. ucast (x + lookup_pd_slot pd vptr && mask pd_bits >> 2)
            \<notin> kernel_mapping_slots)" apply (clarsimp simp: upto_enum_step_def word_shift_by_2) apply (simp add: less_kernel_base_mapping_slots_both word_leq_minus_one_le) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned pd pd_bits \<and> vmsz_aligned vptr ARMSuperSection \<and> vptr < kernel_base \<longrightarrow> (\<forall>x\<in>set [0 , 4 .e. 0x3C]. UCAST(32 \<rightarrow> 12) (x + lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned pd pd_bits; vmsz_aligned vptr ARMSuperSection; vptr < kernel_base; x \<le> 0xF; UCAST(32 \<rightarrow> 12) ((x << 2) + lookup_pd_slot pd vptr && mask pd_bits >> 2) \<in> kernel_mapping_slots\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma lookup_pt_slot_cap_to2:
  "\<lbrace>invs and \<exists>\<rhd> pd and K (is_aligned pd pd_bits) and K (vptr < kernel_base)\<rbrace>
     lookup_pt_slot pd vptr
   \<lbrace>\<lambda>rv s. \<exists>oref cref cap. caps_of_state s (oref, cref) = Some cap
         \<and> rv && ~~ mask pt_bits \<in> obj_refs cap \<and> is_pt_cap cap\<rbrace>, -" apply (rule hoare_post_imp_R, rule lookup_pt_slot_cap_to) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and K (is_aligned pd pd_bits) and K (vptr < kernel_base)\<rbrace> lookup_pt_slot pd vptr \<lbrace>\<lambda>rv s. \<exists>oref cref cap. caps_of_state s (oref, cref) = Some cap \<and> rv && ~~ mask pt_bits \<in> obj_refs cap \<and> is_pt_cap cap\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pt_cap cap \<and> rv && ~~ mask pt_bits \<in> obj_refs cap \<and> s \<turnstile> cap \<and> cap_asid cap \<noteq> None \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned rv 6) \<Longrightarrow> \<exists>oref cref cap. caps_of_state s (oref, cref) = Some cap \<and> rv && ~~ mask pt_bits \<in> obj_refs cap \<and> is_pt_cap cap proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma page_directory_at_lookup_mask_aligned_strg:
  "is_aligned pd pd_bits \<and> page_directory_at pd s
      \<longrightarrow> page_directory_at (lookup_pd_slot pd vptr && ~~ mask pd_bits) s" by (clarsimp simp: lookup_pd_slot_pd)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned pd pd_bits \<and> typ_at (AArch APageDirectory) pd s \<longrightarrow> typ_at (AArch APageDirectory) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s
theory ArchVSpace_AI

lemma page_directory_at_lookup_mask_add_aligned_strg:
  "is_aligned pd pd_bits \<and> page_directory_at pd s
               \<and> vmsz_aligned vptr ARMSuperSection
               \<and> x \<in> set [0, 4 .e. 0x3C]
      \<longrightarrow> page_directory_at (x + lookup_pd_slot pd vptr && ~~ mask pd_bits) s" by (clarsimp simp: lookup_pd_slot_add_eq vmsz_aligned_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned pd pd_bits \<and> typ_at (AArch APageDirectory) pd s \<and> vmsz_aligned vptr ARMSuperSection \<and> x \<in> set [0 , 4 .e. 0x3C] \<longrightarrow> typ_at (AArch APageDirectory) (x + lookup_pd_slot pd vptr && ~~ mask pd_bits) s
theory ArchVSpace_AI

lemma dmo_ccMVA_invs[wp]:
  "\<lbrace>invs\<rbrace> do_machine_op (cleanByVA_PoU a b) \<lbrace>\<lambda>r. invs\<rbrace>" apply (wp dmo_invs) apply safe apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = underlying_memory m p"
          in use_valid) apply ((clarsimp | wp)+)[3] apply(erule use_valid, wp no_irq_cleanByVA_PoU no_irq, assumption) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> do_machine_op (cleanByVA_PoU a b) \<lbrace>\<lambda>r. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<Longrightarrow> \<forall>m. \<forall>(r, m')\<in>fst (cleanByVA_PoU a b m). (\<forall>p. in_user_frame p s \<or> underlying_memory m' p = underlying_memory m p) \<and> (\<forall>irq. m = machine_state s \<longrightarrow> (interrupt_states s irq = IRQInactive \<longrightarrow> irq_masks m' irq) \<or> irq_masks m' irq = irq_masks m irq) \<and> invs s proof (prove)
goal (2 subgoals):
 1. \<And>s m ba p. \<lbrakk>invs s; ((), ba) \<in> fst (cleanByVA_PoU a b m); underlying_memory ba p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> in_user_frame p s
 2. \<And>s m ba irq. \<lbrakk>invs s; ((), ba) \<in> fst (cleanByVA_PoU a b (machine_state s)); interrupt_states s irq = IRQInactive; \<not> irq_masks ba irq; irq_masks (machine_state s) irq\<rbrakk> \<Longrightarrow> irq_masks ba irq proof (prove)
goal (4 subgoals):
 1. \<And>s m ba p. \<lbrakk>invs s; underlying_memory ba p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> \<lbrace>?P19 s m ba p\<rbrace> cleanByVA_PoU a b \<lbrace>\<lambda>_ m'. underlying_memory m' p = underlying_memory m p\<rbrace>
 2. \<And>s m b p. \<lbrakk>invs s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> ?P19 s m b p m
 3. \<And>s m b p. \<lbrakk>invs s; underlying_memory b p \<noteq> underlying_memory m p; underlying_memory b p = underlying_memory m p\<rbrakk> \<Longrightarrow> in_user_frame p s
 4. \<And>s m ba irq. \<lbrakk>invs s; ((), ba) \<in> fst (cleanByVA_PoU a b (machine_state s)); interrupt_states s irq = IRQInactive; \<not> irq_masks ba irq; irq_masks (machine_state s) irq\<rbrakk> \<Longrightarrow> irq_masks ba irq proof (prove)
goal (1 subgoal):
 1. \<And>s m ba irq. \<lbrakk>invs s; ((), ba) \<in> fst (cleanByVA_PoU a b (machine_state s)); interrupt_states s irq = IRQInactive; \<not> irq_masks ba irq; irq_masks (machine_state s) irq\<rbrakk> \<Longrightarrow> irq_masks ba irq proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma dmo_ccr_invs[wp]:
  "\<lbrace>invs\<rbrace> do_machine_op (cleanCacheRange_PoU a b c) \<lbrace>\<lambda>r. invs\<rbrace>" apply (wp dmo_invs) apply safe apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = underlying_memory m p"
          in use_valid) apply ((clarsimp | wp)+)[3] apply(erule use_valid, wp no_irq_cleanCacheRange_PoU no_irq, assumption) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> do_machine_op (cleanCacheRange_PoU a b c) \<lbrace>\<lambda>r. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<Longrightarrow> \<forall>m. \<forall>(r, m')\<in>fst (cleanCacheRange_PoU a b c m). (\<forall>p. in_user_frame p s \<or> underlying_memory m' p = underlying_memory m p) \<and> (\<forall>irq. m = machine_state s \<longrightarrow> (interrupt_states s irq = IRQInactive \<longrightarrow> irq_masks m' irq) \<or> irq_masks m' irq = irq_masks m irq) \<and> invs s proof (prove)
goal (2 subgoals):
 1. \<And>s m ba p. \<lbrakk>invs s; ((), ba) \<in> fst (cleanCacheRange_PoU a b c m); underlying_memory ba p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> in_user_frame p s
 2. \<And>s m ba irq. \<lbrakk>invs s; ((), ba) \<in> fst (cleanCacheRange_PoU a b c (machine_state s)); interrupt_states s irq = IRQInactive; \<not> irq_masks ba irq; irq_masks (machine_state s) irq\<rbrakk> \<Longrightarrow> irq_masks ba irq proof (prove)
goal (4 subgoals):
 1. \<And>s m ba p. \<lbrakk>invs s; underlying_memory ba p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> \<lbrace>?P19 s m ba p\<rbrace> cleanCacheRange_PoU a b c \<lbrace>\<lambda>_ m'. underlying_memory m' p = underlying_memory m p\<rbrace>
 2. \<And>s m b p. \<lbrakk>invs s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> ?P19 s m b p m
 3. \<And>s m b p. \<lbrakk>invs s; underlying_memory b p \<noteq> underlying_memory m p; underlying_memory b p = underlying_memory m p\<rbrakk> \<Longrightarrow> in_user_frame p s
 4. \<And>s m ba irq. \<lbrakk>invs s; ((), ba) \<in> fst (cleanCacheRange_PoU a b c (machine_state s)); interrupt_states s irq = IRQInactive; \<not> irq_masks ba irq; irq_masks (machine_state s) irq\<rbrakk> \<Longrightarrow> irq_masks ba irq proof (prove)
goal (1 subgoal):
 1. \<And>s m ba irq. \<lbrakk>invs s; ((), ba) \<in> fst (cleanCacheRange_PoU a b c (machine_state s)); interrupt_states s irq = IRQInactive; \<not> irq_masks ba irq; irq_masks (machine_state s) irq\<rbrakk> \<Longrightarrow> irq_masks ba irq proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma ex_pt_cap_eq:
  "(\<exists>ref cap. caps_of_state s ref = Some cap \<and>
              p \<in> obj_refs cap \<and> is_pt_cap cap) =
   (\<exists>ref asid. caps_of_state s ref =
               Some (cap.ArchObjectCap (arch_cap.PageTableCap p asid)))" by (fastforce simp add: is_pt_cap_def obj_refs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<exists>ref cap. caps_of_state s ref = Some cap \<and> p \<in> obj_refs cap \<and> is_pt_cap cap) = (\<exists>ref asid. caps_of_state s ref = Some (ArchObjectCap (PageTableCap p asid)))
theory ArchVSpace_AI

lemma pt_aligned:
  "\<lbrakk>page_table_at pt s; pspace_aligned s\<rbrakk> \<Longrightarrow> is_aligned pt 10" by (auto simp: obj_at_def pspace_aligned_def pt_bits_def pageBits_def dom_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at (AArch APageTable) pt s; pspace_aligned s\<rbrakk> \<Longrightarrow> is_aligned pt 10
theory ArchVSpace_AI

lemma vaddr_segment_nonsense:
  "is_aligned (p :: word32) 14 \<Longrightarrow> p + (vaddr >> 20 << 2) && ~~ mask pd_bits = p" by (fact pd_shifting)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned p 14 \<Longrightarrow> p + (vaddr >> 20 << 2) && ~~ mask pd_bits = p
theory ArchVSpace_AI

lemma vaddr_segment_nonsense2:
  "is_aligned (p :: word32) 14 \<Longrightarrow>
   p + (vaddr >> 20 << 2) && mask pd_bits >> 2 = vaddr >> 20" by (simp add: shiftl_less_t2n'[where m=12 and n=2, simplified]
                shiftr_less_t2n'[where m=12 and n=20, simplified]
                pd_bits_def pageBits_def is_aligned_add_helper[THEN conjunct1] triple_shift_fun)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned p 14 \<Longrightarrow> p + (vaddr >> 20 << 2) && mask pd_bits >> 2 = vaddr >> 20
theory ArchVSpace_AI

lemma vaddr_segment_nonsense3:
  "is_aligned (p :: word32) 10 \<Longrightarrow>
   (p + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits) = p" apply (rule is_aligned_add_helper[THEN conjunct2]) apply (simp add: pt_bits_def pageBits_def)+ apply (rule shiftl_less_t2n[where m=10 and n=2, simplified, OF and_mask_less'[where n=8, unfolded mask_def, simplified]]) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned p 10 \<Longrightarrow> p + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits = p proof (prove)
goal (2 subgoals):
 1. is_aligned p 10 \<Longrightarrow> is_aligned p pt_bits
 2. is_aligned p 10 \<Longrightarrow> (vaddr >> 12) && 0xFF << 2 < 2 ^ pt_bits proof (prove)
goal (1 subgoal):
 1. is_aligned p 10 \<Longrightarrow> (vaddr >> 12) && 0xFF << 2 < 0x400 proof (prove)
goal (2 subgoals):
 1. is_aligned p 10 \<Longrightarrow> 8 < LENGTH(32)
 2. is_aligned p 10 \<Longrightarrow> 10 < LENGTH(32) proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma vaddr_segment_nonsense4:
  "is_aligned (p :: word32) 10 \<Longrightarrow>
   p + ((vaddr >> 12) && 0xFF << 2) && mask pt_bits = (vaddr >> 12) && 0xFF << 2" apply (subst is_aligned_add_helper[THEN conjunct1]) apply (simp_all add: pt_bits_def pageBits_def) apply (rule shiftl_less_t2n'[where n=2 and m=8, simplified]) apply (rule and_mask_less'[where n=8, unfolded mask_def, simplified]) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned p 10 \<Longrightarrow> p + ((vaddr >> 12) && 0xFF << 2) && mask pt_bits = (vaddr >> 12) && 0xFF << 2 proof (prove)
goal (3 subgoals):
 1. is_aligned p 10 \<Longrightarrow> is_aligned p pt_bits
 2. is_aligned p 10 \<Longrightarrow> (vaddr >> 12) && 0xFF << 2 < 2 ^ pt_bits
 3. is_aligned p 10 \<Longrightarrow> (vaddr >> 12) && 0xFF << 2 = (vaddr >> 12) && 0xFF << 2 proof (prove)
goal (1 subgoal):
 1. is_aligned p 10 \<Longrightarrow> (vaddr >> 12) && 0xFF << 2 < 0x400 proof (prove)
goal (2 subgoals):
 1. is_aligned p 10 \<Longrightarrow> (vaddr >> 12) && 0xFF < 0x100
 2. is_aligned p 10 \<Longrightarrow> 10 < LENGTH(32) proof (prove)
goal (2 subgoals):
 1. is_aligned p 10 \<Longrightarrow> 8 < LENGTH(32)
 2. is_aligned p 10 \<Longrightarrow> 10 < LENGTH(32) proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma lookup_pt_slot_inv_validE:
  "\<lbrace>P\<rbrace> lookup_pt_slot pd vptr \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>" apply (simp add: lookup_pt_slot_def) apply (wp get_pde_inv hoare_drop_imp lookup_pt_slot_inv | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> lookup_pt_slot pd vptr \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> liftE (get_pde (lookup_pd_slot pd vptr)) >>=E case_pde (throwError (MissingCapability 20)) (\<lambda>ptab x xa. returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2))) (\<lambda>word1 set1 word2 set2. throwError (MissingCapability 20)) (\<lambda>word set1 set2. throwError (MissingCapability 20)) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma unmap_page_no_lookup_pages:
  "\<lbrace>\<lambda>s. \<not> (ref \<unrhd> p) s\<rbrace>
   unmap_page sz asid vaddr pptr
   \<lbrace>\<lambda>_ s. \<not> (ref \<unrhd> p) s\<rbrace>" apply (rule hoare_pre) apply (wp store_pte_no_lookup_pages hoare_drop_imps lookup_pt_slot_inv_validE
         mapM_UNIV_wp store_pde_no_lookup_pages
      | wpc | simp add: unmap_page_def swp_def | strengthen imp_consequent)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (ref, p) \<notin> vs_lookup_pages s\<rbrace> unmap_page sz asid vaddr pptr \<lbrace>\<lambda>_ s. (ref, p) \<notin> vs_lookup_pages s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> unmap_page sz asid vaddr pptr \<lbrace>\<lambda>_ s. (ref, p) \<notin> vs_lookup_pages s\<rbrace>
 2. \<And>s. (ref, p) \<notin> vs_lookup_pages s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma vs_refs_pages_inj:
  "\<lbrakk> (r, p) \<in> vs_refs_pages ko; (r, p') \<in> vs_refs_pages ko \<rbrakk> \<Longrightarrow> p = p'" by (clarsimp simp: vs_refs_pages_def up_ucast_inj_eq dest!: graph_ofD
              split: Structures_A.kernel_object.split_asm arch_kernel_obj.splits)

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

lemma unique_vs_lookup_pages_loop:
  "\<lbrakk> (([r], x), a # list, p) \<in> vs_lookup_pages1 s ^^ length list;
      (([r'], y), a # list, p') \<in> vs_lookup_pages1 s ^^ length list;
      r = r' \<longrightarrow> x = y \<rbrakk>
       \<Longrightarrow> p = p'" apply (induct list arbitrary: a p p') apply simp apply (clarsimp simp: obj_at_def dest!: vs_lookup_pages1D) apply (erule vs_refs_pages_inj) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(([r], x), a # list, p) \<in> vs_lookup_pages1 s ^^ length list; (([r'], y), a # list, p') \<in> vs_lookup_pages1 s ^^ length list; r = r' \<longrightarrow> x = y\<rbrakk> \<Longrightarrow> p = p' proof (prove)
goal (2 subgoals):
 1. \<And>a p p'. \<lbrakk>(([r], x), [a], p) \<in> vs_lookup_pages1 s ^^ length []; (([r'], y), [a], p') \<in> vs_lookup_pages1 s ^^ length []; r = r' \<longrightarrow> x = y\<rbrakk> \<Longrightarrow> p = p'
 2. \<And>a list aa p p'. \<lbrakk>\<And>a p p'. \<lbrakk>(([r], x), a # list, p) \<in> vs_lookup_pages1 s ^^ length list; (([r'], y), a # list, p') \<in> vs_lookup_pages1 s ^^ length list; r = r' \<longrightarrow> x = y\<rbrakk> \<Longrightarrow> p = p'; (([r], x), aa # a # list, p) \<in> vs_lookup_pages1 s ^^ length (a # list); (([r'], y), aa # a # list, p') \<in> vs_lookup_pages1 s ^^ length (a # list); r = r' \<longrightarrow> x = y\<rbrakk> \<Longrightarrow> p = p' proof (prove)
goal (1 subgoal):
 1. \<And>a list aa p p'. \<lbrakk>\<And>a p p'. \<lbrakk>(([r], x), a # list, p) \<in> vs_lookup_pages1 s ^^ length list; (([r'], y), a # list, p') \<in> vs_lookup_pages1 s ^^ length list; r = r' \<longrightarrow> x = y\<rbrakk> \<Longrightarrow> p = p'; (([r], x), aa # a # list, p) \<in> vs_lookup_pages1 s ^^ length (a # list); (([r'], y), aa # a # list, p') \<in> vs_lookup_pages1 s ^^ length (a # list); r = r' \<longrightarrow> x = y\<rbrakk> \<Longrightarrow> p = p' proof (prove)
goal (1 subgoal):
 1. \<And>a list ra pa pb p'a p'b ko koa. \<lbrakk>\<And>a p p'. \<lbrakk>(([r], x), a # list, p) \<in> vs_lookup_pages1 s ^^ length list; (([r'], y), a # list, p') \<in> vs_lookup_pages1 s ^^ length list\<rbrakk> \<Longrightarrow> p = p'; r = r' \<longrightarrow> x = y; (([r], x), a # list, pa) \<in> vs_lookup_pages1 s ^^ length list; (([r'], y), a # list, pb) \<in> vs_lookup_pages1 s ^^ length list; kheap s pa = Some ko; (ra, p'a) \<in> vs_refs_pages ko; kheap s pb = Some koa; (ra, p'b) \<in> vs_refs_pages koa\<rbrakk> \<Longrightarrow> p'a = p'b proof (prove)
goal (1 subgoal):
 1. \<And>a list ra pa pb p'a p'b ko koa. \<lbrakk>\<And>a p p'. \<lbrakk>(([r], x), a # list, p) \<in> vs_lookup_pages1 s ^^ length list; (([r'], y), a # list, p') \<in> vs_lookup_pages1 s ^^ length list\<rbrakk> \<Longrightarrow> p = p'; r = r' \<longrightarrow> x = y; (([r], x), a # list, pa) \<in> vs_lookup_pages1 s ^^ length list; (([r'], y), a # list, pb) \<in> vs_lookup_pages1 s ^^ length list; kheap s pa = Some ko; kheap s pb = Some koa; (ra, p'b) \<in> vs_refs_pages koa\<rbrakk> \<Longrightarrow> (ra, p'b) \<in> vs_refs_pages ko proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma unique_vs_lookup_pages:
  "\<lbrakk>(r \<unrhd> p) s; (r \<unrhd> p') s\<rbrakk> \<Longrightarrow> p = p'" apply (clarsimp simp: vs_lookup_pages_def vs_asid_refs_def
                 dest!: graph_ofD vs_lookup_pages1_rtrancl_iterations) apply (case_tac r, simp_all) apply (erule(1) unique_vs_lookup_pages_loop) apply (clarsimp simp: up_ucast_inj_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(r \<unrhd> p) s; (r \<unrhd> p') s\<rbrakk> \<Longrightarrow> p = p' proof (prove)
goal (1 subgoal):
 1. \<And>ab bb ac bc. \<lbrakk>asid_table s ab = Some bb; asid_table s ac = Some bc; Suc 0 \<le> length r; (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), r, p) \<in> vs_lookup_pages1 s ^^ (length r - Suc 0); (([VSRef (UCAST(7 \<rightarrow> 32) ac) None], bc), r, p') \<in> vs_lookup_pages1 s ^^ (length r - Suc 0)\<rbrakk> \<Longrightarrow> p = p' proof (prove)
goal (1 subgoal):
 1. \<And>ab bb ac bc a list. \<lbrakk>asid_table s ab = Some bb; asid_table s ac = Some bc; (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), a # list, p) \<in> vs_lookup_pages1 s ^^ length list; (([VSRef (UCAST(7 \<rightarrow> 32) ac) None], bc), a # list, p') \<in> vs_lookup_pages1 s ^^ length list; r = a # list\<rbrakk> \<Longrightarrow> p = p' proof (prove)
goal (1 subgoal):
 1. \<And>ab bb ac bc a list. \<lbrakk>asid_table s ab = Some bb; asid_table s ac = Some bc; (([VSRef (UCAST(7 \<rightarrow> 32) ac) None], bc), a # list, p') \<in> vs_lookup_pages1 s ^^ length list; r = a # list\<rbrakk> \<Longrightarrow> VSRef (UCAST(7 \<rightarrow> 32) ab) None = VSRef (UCAST(7 \<rightarrow> 32) ac) None \<longrightarrow> bb = bc proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma unmap_page_page_unmapped:
  "\<lbrace>pspace_aligned and valid_objs and valid_vspace_objs and
    (\<lambda>s. valid_asid_table (arm_asid_table (arch_state s)) s) and
    data_at sz pptr and
    K (p = pptr) and K (sz = ARMSmallPage \<or> sz = ARMLargePage)\<rbrace>
   unmap_page sz asid vaddr pptr
   \<lbrace>\<lambda>rv s. \<not> ([VSRef ((vaddr >> 12) && mask 8) (Some APageTable),
               VSRef (vaddr >> 20) (Some APageDirectory),
               VSRef (asid && mask asid_low_bits) (Some AASIDPool),
               VSRef (ucast (asid_high_bits_of asid)) None] \<unrhd> p) s\<rbrace>" by (rule hoare_pre_imp[OF _ unmap_page_unmapped]) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned and valid_objs and valid_vspace_objs and (\<lambda>s. valid_asid_table (asid_table s) s) and data_at sz pptr and K (p = pptr) and K (sz = ARMSmallPage \<or> sz = ARMLargePage)\<rbrace> unmap_page sz asid vaddr pptr \<lbrace>\<lambda>rv s. ([VSRef ((vaddr >> 12) && mask 8) (Some APageTable), VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p) \<notin> vs_lookup_pages s\<rbrace>
theory ArchVSpace_AI

lemma unmap_page_section_unmapped:
  "\<lbrace>pspace_aligned and valid_objs and valid_vspace_objs and
    (\<lambda>s. valid_asid_table (arm_asid_table (arch_state s)) s) and
    data_at sz pptr and
    K (p = pptr) and K (sz = ARMSection \<or> sz = ARMSuperSection)\<rbrace>
   unmap_page sz asid vaddr pptr
   \<lbrace>\<lambda>rv s. \<not> ([VSRef (vaddr >> 20) (Some APageDirectory),
               VSRef (asid && mask asid_low_bits) (Some AASIDPool),
               VSRef (ucast (asid_high_bits_of asid)) None] \<unrhd> p) s\<rbrace>" by (rule hoare_pre_imp[OF _ unmap_page_unmapped]) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned and valid_objs and valid_vspace_objs and (\<lambda>s. valid_asid_table (asid_table s) s) and data_at sz pptr and K (p = pptr) and K (sz = ARMSection \<or> sz = ARMSuperSection)\<rbrace> unmap_page sz asid vaddr pptr \<lbrace>\<lambda>rv s. ([VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p) \<notin> vs_lookup_pages s\<rbrace>
theory ArchVSpace_AI

lemma set_mi_invs[wp]: "\<lbrace>invs\<rbrace> set_message_info t a \<lbrace>\<lambda>x. invs\<rbrace>" by (simp add: set_message_info_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> set_message_info t a \<lbrace>\<lambda>x. invs\<rbrace>