kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchVSpace_AI

lemma find_pd_for_asid_pde [wp]:
  "\<lbrace>valid_vspace_objs and pspace_aligned\<rbrace>
  find_pd_for_asid asid
  \<lbrace>\<lambda>pd. pde_at (pd + (vptr >> 20 << 2))\<rbrace>, -" proof - have x:
    "\<lbrace>valid_vspace_objs and pspace_aligned\<rbrace> find_pd_for_asid asid
     \<lbrace>\<lambda>pd. pspace_aligned and page_directory_at pd\<rbrace>, -" by (rule hoare_pre) (wp, simp) show ?thesis apply (rule hoare_post_imp_R, rule x) apply clarsimp apply (erule page_directory_pde_atI) prefer 2 apply assumption apply (rule vptr_shiftr_le_2p) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and pspace_aligned\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>pd. pde_at (pd + (vptr >> 20 << 2))\<rbrace>, - proof (state)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and pspace_aligned\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>pd. pde_at (pd + (vptr >> 20 << 2))\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and pspace_aligned\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>pd. pspace_aligned and typ_at (AArch APageDirectory) pd\<rbrace>, - proof (state)
this:
\<lbrace>valid_vspace_objs and pspace_aligned\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>pd. pspace_aligned and typ_at (AArch APageDirectory) pd\<rbrace>, -

goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and pspace_aligned\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>pd. pde_at (pd + (vptr >> 20 << 2))\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and pspace_aligned\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>pd. pde_at (pd + (vptr >> 20 << 2))\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>rv s. (pspace_aligned and typ_at (AArch APageDirectory) rv) s \<Longrightarrow> pde_at (rv + (vptr >> 20 << 2)) s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>pspace_aligned s; typ_at (AArch APageDirectory) rv s\<rbrakk> \<Longrightarrow> pde_at (rv + (vptr >> 20 << 2)) s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. pspace_aligned s \<Longrightarrow> vptr >> 20 < 2 ^ pageBits
 2. \<And>rv s. pspace_aligned s \<Longrightarrow> pspace_aligned s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. pspace_aligned s \<Longrightarrow> pspace_aligned s
 2. \<And>rv s. pspace_aligned s \<Longrightarrow> vptr >> 20 < 2 ^ pageBits proof (prove)
goal (1 subgoal):
 1. \<And>rv s. pspace_aligned s \<Longrightarrow> vptr >> 20 < 2 ^ pageBits proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>valid_vspace_objs and pspace_aligned\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>pd. pde_at (pd + (vptr >> 20 << 2))\<rbrace>, -

goal:
No subgoals!
theory ArchVSpace_AI

lemma find_pd_for_asid_aligned_pd_bits[wp]:
  "\<lbrace>pspace_aligned and valid_vspace_objs\<rbrace>
      find_pd_for_asid asid
   \<lbrace>\<lambda>rv s. is_aligned rv pd_bits\<rbrace>, -" by (simp add: pd_bits_def pageBits_def, rule find_pd_for_asid_aligned_pd)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned and valid_vspace_objs\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>rv s. is_aligned rv pd_bits\<rbrace>, -
theory ArchVSpace_AI

lemma vs_lookup1_inj:
  "\<lbrakk> ((ref, p), (ref', p')) \<in> vs_lookup1 s ^^ n;
     ((ref, p), (ref', p'')) \<in> vs_lookup1 s ^^ n \<rbrakk>
       \<Longrightarrow> p' = p''" apply (induct n arbitrary: ref ref' p p' p'') apply simp apply (clarsimp dest!: vs_lookup1D) apply (subgoal_tac "pa = pb", simp_all) apply (simp add: obj_at_def) apply (auto simp: vs_refs_def up_ucast_inj_eq dest!: graph_ofD
             split: Structures_A.kernel_object.split_asm arch_kernel_obj.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((ref, p), ref', p') \<in> vs_lookup1 s ^^ n; ((ref, p), ref', p'') \<in> vs_lookup1 s ^^ n\<rbrakk> \<Longrightarrow> p' = p'' proof (prove)
goal (2 subgoals):
 1. \<And>ref ref' p p' p''. \<lbrakk>((ref, p), ref', p') \<in> vs_lookup1 s ^^ 0; ((ref, p), ref', p'') \<in> vs_lookup1 s ^^ 0\<rbrakk> \<Longrightarrow> p' = p''
 2. \<And>n ref ref' p p' p''. \<lbrakk>\<And>ref ref' p p' p''. \<lbrakk>((ref, p), ref', p') \<in> vs_lookup1 s ^^ n; ((ref, p), ref', p'') \<in> vs_lookup1 s ^^ n\<rbrakk> \<Longrightarrow> p' = p''; ((ref, p), ref', p') \<in> vs_lookup1 s ^^ Suc n; ((ref, p), ref', p'') \<in> vs_lookup1 s ^^ Suc n\<rbrakk> \<Longrightarrow> p' = p'' proof (prove)
goal (1 subgoal):
 1. \<And>n ref ref' p p' p''. \<lbrakk>\<And>ref ref' p p' p''. \<lbrakk>((ref, p), ref', p') \<in> vs_lookup1 s ^^ n; ((ref, p), ref', p'') \<in> vs_lookup1 s ^^ n\<rbrakk> \<Longrightarrow> p' = p''; ((ref, p), ref', p') \<in> vs_lookup1 s ^^ Suc n; ((ref, p), ref', p'') \<in> vs_lookup1 s ^^ Suc n\<rbrakk> \<Longrightarrow> p' = p'' proof (prove)
goal (1 subgoal):
 1. \<And>n ac bc rsa ra pa pb p'a p'b ko koa. \<lbrakk>\<And>ref ref' p p' p''. \<lbrakk>((ref, p), ref', p') \<in> vs_lookup1 s ^^ n; ((ref, p), ref', p'') \<in> vs_lookup1 s ^^ n\<rbrakk> \<Longrightarrow> p' = p''; ((ac, bc), rsa, pa) \<in> vs_lookup1 s ^^ n; ((ac, bc), rsa, pb) \<in> vs_lookup1 s ^^ n; ko_at ko pa s; (ra, p'a) \<in> vs_refs ko; ko_at koa pb s; (ra, p'b) \<in> vs_refs koa\<rbrakk> \<Longrightarrow> p'a = p'b proof (prove)
goal (1 subgoal):
 1. \<And>n ac bc rsa ra pa pb p'a p'b ko koa. \<lbrakk>\<And>ref ref' p p' p''. \<lbrakk>((ref, p), ref', p') \<in> vs_lookup1 s ^^ n; ((ref, p), ref', p'') \<in> vs_lookup1 s ^^ n\<rbrakk> \<Longrightarrow> p' = p''; ((ac, bc), rsa, pb) \<in> vs_lookup1 s ^^ n; ko_at ko pb s; (ra, p'a) \<in> vs_refs ko; ko_at koa pb s; (ra, p'b) \<in> vs_refs koa; pa = pb\<rbrakk> \<Longrightarrow> p'a = p'b proof (prove)
goal (1 subgoal):
 1. \<And>n ac bc rsa ra pa pb p'a p'b ko koa. \<lbrakk>\<And>ref ref' p p' p''. \<lbrakk>((ref, p), ref', p') \<in> vs_lookup1 s ^^ n; ((ref, p), ref', p'') \<in> vs_lookup1 s ^^ n\<rbrakk> \<Longrightarrow> p' = p''; ((ac, bc), rsa, pb) \<in> vs_lookup1 s ^^ n; kheap s pb = Some ko; (ra, p'a) \<in> vs_refs ko; koa = ko; (ra, p'b) \<in> vs_refs ko; pa = pb\<rbrakk> \<Longrightarrow> p'a = p'b proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma vptr_shifting_3_ways:
  fixes vptr :: word32 shows
  "vptr >> 20 << 2 >> 2 = vptr >> 20" apply (rule shiftl_shiftr_id, simp add: word_bits_def) apply (rule shiftr_less_t2n', simp_all add: word_bits_def) apply (cut_tac word_log_esimps[where x=vptr]) apply (simp add: mask_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vptr >> 20 << 2 >> 2 = vptr >> 20 proof (prove)
goal (1 subgoal):
 1. vptr >> 20 < 2 ^ (LENGTH(32) - 2) proof (prove)
goal (1 subgoal):
 1. vptr && mask 50 = vptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vptr && 0 = 0; vptr && - 1 = vptr; vptr || 0 = vptr; vptr || - 1 = - 1; vptr xor 0 = vptr; vptr xor - 1 = ~~ vptr; 0 && vptr = 0; - 1 && vptr = vptr; 0 || vptr = vptr; - 1 || vptr = - 1; 0 xor vptr = vptr; - 1 xor vptr = ~~ vptr\<rbrakk> \<Longrightarrow> vptr && mask 50 = vptr proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma flush_page_pd_at_asid [wp]:
  "\<lbrace>vspace_at_asid a pd\<rbrace> flush_page pgsz pd asid vptr \<lbrace>\<lambda>_. vspace_at_asid a pd\<rbrace>" apply (simp add: vspace_at_asid_def) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>vspace_at_asid a pd\<rbrace> flush_page pgsz pd asid vptr \<lbrace>\<lambda>_. vspace_at_asid a pd\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>[VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> pd\<rbrace> flush_page pgsz pd asid vptr \<lbrace>\<lambda>_. [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> pd\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma lookup_pd_slot_aligned_6:
  "\<lbrakk> vmsz_aligned vptr ARMSuperSection; is_aligned pd 14 \<rbrakk>
        \<Longrightarrow> is_aligned (lookup_pd_slot pd vptr) 6" apply (simp add: lookup_pd_slot_def) apply (erule aligned_add_aligned, simp_all add: word_bits_conv) apply (intro is_aligned_shiftl is_aligned_shiftr) apply (simp add: vmsz_aligned_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vmsz_aligned vptr ARMSuperSection; is_aligned pd 14\<rbrakk> \<Longrightarrow> is_aligned (lookup_pd_slot pd vptr) 6 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vmsz_aligned vptr ARMSuperSection; is_aligned pd 14\<rbrakk> \<Longrightarrow> is_aligned (pd + (vptr >> 20 << 2)) 6 proof (prove)
goal (1 subgoal):
 1. vmsz_aligned vptr ARMSuperSection \<Longrightarrow> is_aligned (vptr >> 20 << 2) 6 proof (prove)
goal (1 subgoal):
 1. vmsz_aligned vptr ARMSuperSection \<Longrightarrow> is_aligned vptr (6 - 2 + 20) proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma page_directory_at_aligned_pd_bits:
  "\<lbrakk>page_directory_at pd s;pspace_aligned s\<rbrakk>
       \<Longrightarrow> is_aligned pd pd_bits" apply (clarsimp simp:obj_at_def) apply (drule(1) pspace_alignedD) apply (simp add:pd_bits_def pageBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at (AArch APageDirectory) pd s; pspace_aligned s\<rbrakk> \<Longrightarrow> is_aligned pd pd_bits proof (prove)
goal (1 subgoal):
 1. \<And>pda. \<lbrakk>pspace_aligned s; kheap s pd = Some (ArchObj (PageDirectory pda))\<rbrakk> \<Longrightarrow> is_aligned pd pd_bits proof (prove)
goal (1 subgoal):
 1. \<And>pda. \<lbrakk>pspace_aligned s; is_aligned pd (obj_bits (ArchObj (PageDirectory pda)))\<rbrakk> \<Longrightarrow> is_aligned pd pd_bits proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma invalidateLocalTLB_ASID_valid_irq_states:
  "\<lbrace>\<lambda>m. valid_irq_states (s\<lparr>machine_state := m\<rparr>)\<rbrace> invalidateLocalTLB_ASID x
   \<lbrace>\<lambda>a b. valid_irq_states (s\<lparr>machine_state := b\<rparr>)\<rbrace>" apply(simp add: valid_irq_states_def | wp no_irq | simp add: no_irq_invalidateLocalTLB_ASID)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>m. valid_irq_states (s\<lparr>machine_state := m\<rparr>)\<rbrace> invalidateLocalTLB_ASID x \<lbrace>\<lambda>a b. valid_irq_states (s\<lparr>machine_state := b\<rparr>)\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma get_hw_asid_invs [wp]:
  "\<lbrace>invs and K (a \<le> mask asid_bits)\<rbrace> get_hw_asid a \<lbrace>\<lambda>hw_asid. invs\<rbrace>" apply (simp add: get_hw_asid_def) apply (wp store_hw_asid_invs load_hw_asid_wp|wpc)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and K (a \<le> mask local.asid_bits)\<rbrace> get_hw_asid a \<lbrace>\<lambda>hw_asid. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>y. a \<le> mask local.asid_bits)\<rbrace> do maybe_hw_asid <- load_hw_asid a;
case maybe_hw_asid of None \<Rightarrow> do new_hw_asid <- find_free_hw_asid;
store_hw_asid a new_hw_asid;
return new_hw_asid
od | Some hw_asid \<Rightarrow> return hw_asid
od \<lbrace>\<lambda>hw_asid. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs and (\<lambda>y. a \<le> mask local.asid_bits)) s \<Longrightarrow> (map_option fst (arm_asid_map (arch_state s) a) = None \<longrightarrow> invs s \<and> arm_asid_map (arch_state s) a = None \<and> True \<and> a \<le> mask local.asid_bits) \<and> (\<forall>x. map_option fst (arm_asid_map (arch_state s) a) = Some x \<longrightarrow> invs s) proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma dmo_set_current_pd_invs[wp]: "\<lbrace>invs\<rbrace> do_machine_op (set_current_pd addr) \<lbrace>\<lambda>y. 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 simp: set_current_pd_def writeTTBR0_def dsb_def isb_def machine_op_lift_def
                           machine_rest_lift_def split_def | wp)+)[3] apply(erule (1) use_valid[OF _ set_current_pd_irq_masks]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> do_machine_op (set_current_pd addr) \<lbrace>\<lambda>y. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<Longrightarrow> \<forall>m. \<forall>(r, m')\<in>fst (set_current_pd addr 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 b p. \<lbrakk>invs s; ((), b) \<in> fst (set_current_pd addr m); underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> in_user_frame p s
 2. \<And>s m b irq. \<lbrakk>invs s; ((), b) \<in> fst (set_current_pd addr (machine_state s)); interrupt_states s irq = IRQInactive; \<not> irq_masks b irq; irq_masks (machine_state s) irq\<rbrakk> \<Longrightarrow> irq_masks b irq proof (prove)
goal (4 subgoals):
 1. \<And>s m b p. \<lbrakk>invs s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> \<lbrace>?P19 s m b p\<rbrace> set_current_pd addr \<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 b irq. \<lbrakk>invs s; ((), b) \<in> fst (set_current_pd addr (machine_state s)); interrupt_states s irq = IRQInactive; \<not> irq_masks b irq; irq_masks (machine_state s) irq\<rbrakk> \<Longrightarrow> irq_masks b irq proof (prove)
goal (1 subgoal):
 1. \<And>s m b irq. \<lbrakk>invs s; ((), b) \<in> fst (set_current_pd addr (machine_state s)); interrupt_states s irq = IRQInactive; \<not> irq_masks b irq; irq_masks (machine_state s) irq\<rbrakk> \<Longrightarrow> irq_masks b irq proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma dmo_ackInterrupt[wp]: "\<lbrace>invs\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>y. 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 simp: ackInterrupt_def machine_op_lift_def
                           machine_rest_lift_def split_def | wp)+)[3] apply(erule (1) use_valid[OF _ ackInterrupt_irq_masks]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>y. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<Longrightarrow> \<forall>m. \<forall>(r, m')\<in>fst (ackInterrupt irq 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 b p. \<lbrakk>invs s; ((), b) \<in> fst (ackInterrupt irq m); underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> in_user_frame p s
 2. \<And>s m b irqa. \<lbrakk>invs s; ((), b) \<in> fst (ackInterrupt irq (machine_state s)); interrupt_states s irqa = IRQInactive; \<not> irq_masks b irqa; irq_masks (machine_state s) irqa\<rbrakk> \<Longrightarrow> irq_masks b irqa proof (prove)
goal (4 subgoals):
 1. \<And>s m b p. \<lbrakk>invs s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> \<lbrace>?P19 s m b p\<rbrace> ackInterrupt irq \<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 b irqa. \<lbrakk>invs s; ((), b) \<in> fst (ackInterrupt irq (machine_state s)); interrupt_states s irqa = IRQInactive; \<not> irq_masks b irqa; irq_masks (machine_state s) irqa\<rbrakk> \<Longrightarrow> irq_masks b irqa proof (prove)
goal (1 subgoal):
 1. \<And>s m b irqa. \<lbrakk>invs s; ((), b) \<in> fst (ackInterrupt irq (machine_state s)); interrupt_states s irqa = IRQInactive; \<not> irq_masks b irqa; irq_masks (machine_state s) irqa\<rbrakk> \<Longrightarrow> irq_masks b irqa proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma dmo_setIRQTrigger_invs[wp]: "\<lbrace>invs\<rbrace> do_machine_op (setIRQTrigger irq b) \<lbrace>\<lambda>y. 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 simp: setIRQTrigger_def machine_op_lift_def
                           machine_rest_lift_def split_def | wp)+)[3] apply(erule (1) use_valid[OF _ setIRQTrigger_irq_masks]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> do_machine_op (setIRQTrigger irq b) \<lbrace>\<lambda>y. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<Longrightarrow> \<forall>m. \<forall>(r, m')\<in>fst (setIRQTrigger irq 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 (setIRQTrigger irq b m); underlying_memory ba p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> in_user_frame p s
 2. \<And>s m ba irqa. \<lbrakk>invs s; ((), ba) \<in> fst (setIRQTrigger irq b (machine_state s)); interrupt_states s irqa = IRQInactive; \<not> irq_masks ba irqa; irq_masks (machine_state s) irqa\<rbrakk> \<Longrightarrow> irq_masks ba irqa 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> setIRQTrigger irq 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 irqa. \<lbrakk>invs s; ((), ba) \<in> fst (setIRQTrigger irq b (machine_state s)); interrupt_states s irqa = IRQInactive; \<not> irq_masks ba irqa; irq_masks (machine_state s) irqa\<rbrakk> \<Longrightarrow> irq_masks ba irqa proof (prove)
goal (1 subgoal):
 1. \<And>s m ba irqa. \<lbrakk>invs s; ((), ba) \<in> fst (setIRQTrigger irq b (machine_state s)); interrupt_states s irqa = IRQInactive; \<not> irq_masks ba irqa; irq_masks (machine_state s) irqa\<rbrakk> \<Longrightarrow> irq_masks ba irqa proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma set_cap_valid_pte_stronger:
  "\<lbrace>\<lambda>s. P (valid_pte pte s)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv s. P (valid_pte pte s)\<rbrace>" by (wp valid_pte_lift3 set_cap_typ_at)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (valid_pte pte s)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv s. P (valid_pte pte s)\<rbrace>
theory ArchVSpace_AI

lemma vs_lookup1:
  "vs_lookup1 s' \<subseteq> vs_lookup1 s \<union> new_lookups" apply (simp add: vs_lookup1_def) apply (clarsimp simp: obj_at_def s'_def new_lookups_def) apply (auto split: if_split_asm simp: refs old) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vs_lookup1 s' \<subseteq> vs_lookup1 s \<union> new_lookups proof (prove)
goal (1 subgoal):
 1. {((rs, p), rs', p'). \<exists>ko. ko_at ko p s' \<and> (\<exists>r. rs' = r # rs \<and> (r, p') \<in> vs_refs ko)} \<subseteq> {((rs, p), rs', p'). \<exists>ko. ko_at ko p s \<and> (\<exists>r. rs' = r # rs \<and> (r, p') \<in> vs_refs ko)} \<union> new_lookups proof (prove)
goal (1 subgoal):
 1. \<And>b ba ko r. \<lbrakk>(r, ba) \<in> S \<longrightarrow> b \<noteq> pdp; (if b = pdp then Some (ArchObj (PageDirectory pd')) else kheap s b) = Some ko; (r, ba) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s b = Some ko \<and> (r, ba) \<in> vs_refs ko proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma vs_lookup_trans:
  "(vs_lookup1 s')^* \<subseteq> (vs_lookup1 s)^* \<union> (vs_lookup1 s)^* O new_lookups^*" apply (rule ord_le_eq_trans, rule rtrancl_mono, rule vs_lookup1) apply (rule union_trans) apply (clarsimp simp add: new_lookups_def) apply (drule bspec [OF pts]) apply (clarsimp simp: vs_lookup1_def obj_at_def vs_refs_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (vs_lookup1 s')\<^sup>* \<subseteq> (vs_lookup1 s)\<^sup>* \<union> (vs_lookup1 s)\<^sup>* O new_lookups\<^sup>* proof (prove)
goal (1 subgoal):
 1. (vs_lookup1 s \<union> new_lookups)\<^sup>* = (vs_lookup1 s)\<^sup>* \<union> (vs_lookup1 s)\<^sup>* O new_lookups\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> new_lookups; (y, z) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> (x, z) \<in> new_lookups\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>a ba ab bb r. \<lbrakk>((r # a, ba), ab, bb) \<in> vs_lookup1 s; (r, ba) \<in> S\<rbrakk> \<Longrightarrow> ((a, pdp), ab, bb) \<in> {((rs, p), rs', p'). \<exists>r. rs' = r # rs \<and> (r, p') \<in> S \<and> p = pdp}\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>a ba ab bb r. \<lbrakk>((r # a, ba), ab, bb) \<in> vs_lookup1 s; typ_at (AArch APageTable) (snd (r, ba)) s\<rbrakk> \<Longrightarrow> ((a, pdp), ab, bb) \<in> {((rs, p), rs', p'). \<exists>r. rs' = r # rs \<and> (r, p') \<in> S \<and> p = pdp}\<^sup>* proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma double_new_lookup:
  "\<lbrakk> (x, y) \<in> new_lookups; (y, z) \<in> new_lookups \<rbrakk> \<Longrightarrow> False" by (auto simp: new_lookups_def obj_at_def old a_type_def
          dest!: bspec [OF pts])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x, y) \<in> new_lookups; (y, z) \<in> new_lookups\<rbrakk> \<Longrightarrow> False