kings-crown/FVELER_Isabelle huggingface dataset:
theory Untyped_AI

lemma default_cap_reply:
  "default_cap tp ptr sz dev \<noteq> cap.ReplyCap ptr' bool R" by (cases tp; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. default_cap tp ptr sz dev \<noteq> ReplyCap ptr' bool R
theory Untyped_AI

lemma create_cap_valid_reply_masters[wp]:
  "\<lbrace>valid_reply_masters\<rbrace>
     create_cap tp sz p dev (cref, oref)
   \<lbrace>\<lambda>rv. valid_reply_masters\<rbrace>" apply (simp add: valid_reply_masters_def cte_wp_at_caps_of_state
                   create_cap_def is_master_reply_cap_to_def) apply (wp | simp add: default_cap_reply)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_masters\<rbrace> create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. valid_reply_masters\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>a b t. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>rights. cap = ReplyCap t True rights)) \<longrightarrow> a = t \<and> b = tcb_cnode_index 2\<rbrace> do dest_p <- gets (\<lambda>s. cdt s cref);
cdt <- gets cdt;
y <- set_cdt (cdt(cref \<mapsto> p));
y <- do_extended_op (create_cap_ext p cref dest_p);
y <- set_original cref True;
set_cap (default_cap tp oref sz dev) cref
od \<lbrace>\<lambda>rv s. \<forall>a b t. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>rights. cap = ReplyCap t True rights)) \<longrightarrow> a = t \<and> b = tcb_cnode_index 2\<rbrace> proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma create_cap_aobj_at:
  "arch_obj_pred P' \<Longrightarrow>
  \<lbrace>\<lambda>s. P (obj_at P' pd s)\<rbrace> create_cap type bits ut is_dev cref \<lbrace>\<lambda>r s. P (obj_at P' pd s)\<rbrace>" unfolding create_cap_def split_def set_cdt_def by (wpsimp wp: set_cap.aobj_at)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_obj_pred P' \<Longrightarrow> \<lbrace>\<lambda>s. P (obj_at P' pd s)\<rbrace> create_cap type bits ut is_dev cref \<lbrace>\<lambda>r s. P (obj_at P' pd s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. arch_obj_pred P' \<Longrightarrow> \<lbrace>\<lambda>s. P (obj_at P' pd s)\<rbrace> do dest_p <- gets (\<lambda>s. cdt s (fst cref));
cdt <- gets cdt;
do s <- get;
put $ s\<lparr>cdt := cdt(fst cref \<mapsto> ut)\<rparr>
od;
do_extended_op (create_cap_ext ut (fst cref) dest_p);
set_original (fst cref) True;
set_cap (default_cap type (snd cref) bits is_dev) (fst cref)
od \<lbrace>\<lambda>r s. P (obj_at P' pd s)\<rbrace>
theory Untyped_AI

lemma create_cap_valid_arch_state[wp]:
  "\<lbrace>valid_arch_state\<rbrace> create_cap type bits ut is_dev cref \<lbrace>\<lambda>_. valid_arch_state\<rbrace>" by (wp valid_arch_state_lift_aobj_at create_cap_aobj_at)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state\<rbrace> create_cap type bits ut is_dev cref \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
theory Untyped_AI

lemma default_cap_irqs[simp]:
  "cap_irqs (default_cap tp oref sz dev) = {}" by (cases tp, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_irqs (default_cap tp oref sz dev) = {}
theory Untyped_AI

lemma create_cap_irq_handlers[wp]:
  "\<lbrace>valid_irq_handlers\<rbrace> create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. valid_irq_handlers\<rbrace>" apply (simp add: valid_irq_handlers_def irq_issued_def) apply (simp add: create_cap_def Ball_def) apply (simp only: imp_conv_disj) apply (wpsimp wp: hoare_vcg_all_lift hoare_vcg_disj_lift) apply (auto simp: ran_def split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_handlers\<rbrace> create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. valid_irq_handlers\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>cap\<in>ran (caps_of_state s). \<forall>irq\<in>cap_irqs cap. interrupt_states s irq = IRQSignal\<rbrace> create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv s. \<forall>cap\<in>ran (caps_of_state s). \<forall>irq\<in>cap_irqs cap. interrupt_states s irq = IRQSignal\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x. x \<in> ran (caps_of_state s) \<longrightarrow> (\<forall>xa. xa \<in> cap_irqs x \<longrightarrow> interrupt_states s xa = IRQSignal)\<rbrace> do dest_p <- gets (\<lambda>s. cdt s cref);
cdt <- gets cdt;
y <- set_cdt (cdt(cref \<mapsto> p));
y <- do_extended_op (create_cap_ext p cref dest_p);
y <- set_original cref True;
set_cap (default_cap tp oref sz dev) cref
od \<lbrace>\<lambda>rv s. \<forall>x. x \<in> ran (caps_of_state s) \<longrightarrow> (\<forall>xa. xa \<in> cap_irqs x \<longrightarrow> interrupt_states s xa = IRQSignal)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x. x \<notin> ran (caps_of_state s) \<or> (\<forall>xa. xa \<notin> cap_irqs x \<or> interrupt_states s xa = IRQSignal)\<rbrace> do dest_p <- gets (\<lambda>s. cdt s cref);
cdt <- gets cdt;
y <- set_cdt (cdt(cref \<mapsto> p));
y <- do_extended_op (create_cap_ext p cref dest_p);
y <- set_original cref True;
set_cap (default_cap tp oref sz dev) cref
od \<lbrace>\<lambda>rv s. \<forall>x. x \<notin> ran (caps_of_state s) \<or> (\<forall>xa. xa \<notin> cap_irqs x \<or> interrupt_states s xa = IRQSignal)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x xa. \<lbrakk>\<forall>x. x \<in> ran (caps_of_state s) \<longrightarrow> (\<forall>xa. xa \<in> cap_irqs x \<longrightarrow> interrupt_states s xa = IRQSignal); x \<in> ran (\<lambda>a. if a = cref then Some (default_cap tp oref sz dev) else caps_of_state s a); xa \<in> cap_irqs x\<rbrakk> \<Longrightarrow> interrupt_states s xa = IRQSignal proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma create_cap_asid_map[wp]:
  "\<lbrace>valid_asid_map\<rbrace> create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. valid_asid_map\<rbrace>" unfolding create_cap_def set_cdt_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid_map\<rbrace> create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. valid_asid_map\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid_map\<rbrace> case (cref, oref) of (dest, oref) \<Rightarrow> do dest_p <- gets (\<lambda>s. cdt s dest);
cdt <- gets cdt;
do s <- get;
put $ s\<lparr>cdt := cdt(dest \<mapsto> p)\<rparr>
od;
do_extended_op (create_cap_ext p dest dest_p);
set_original dest True;
set_cap (default_cap tp oref sz dev) dest
od \<lbrace>\<lambda>rv. valid_asid_map\<rbrace>
theory Untyped_AI

lemma set_original_valid_ioc[wp]:
  "\<lbrace>valid_ioc\<rbrace> create_cap tp sz p dev slot \<lbrace>\<lambda>_. valid_ioc\<rbrace>" apply (cases slot) apply (wpsimp wp: set_cdt_cos_ioc set_cap_caps_of_state
              simp: create_cap_def set_original_set_cap_comm cte_wp_at_caps_of_state) apply (cases tp; simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ioc\<rbrace> create_cap tp sz p dev slot \<lbrace>\<lambda>_. valid_ioc\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b. slot = (a, b) \<Longrightarrow> \<lbrace>valid_ioc\<rbrace> create_cap tp sz p dev slot \<lbrace>\<lambda>_. valid_ioc\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b ba s. \<lbrakk>slot = ((a, b), ba); valid_ioc s\<rbrakk> \<Longrightarrow> (default_cap tp ba sz dev = NullCap \<longrightarrow> \<not> is_original_cap s (a, b)) \<and> default_cap tp ba sz dev \<noteq> NullCap proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma cap_range_subseteq_weaken:
 "\<lbrakk>obj_refs c \<subseteq> untyped_range cap; untyped_range c \<subseteq> untyped_range cap\<rbrakk>
 \<Longrightarrow> cap_range c \<subseteq> cap_range cap" by (fastforce simp add: cap_range_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_refs c \<subseteq> untyped_range cap; untyped_range c \<subseteq> untyped_range cap\<rbrakk> \<Longrightarrow> cap_range c \<subseteq> cap_range cap
theory Untyped_AI

lemma create_cap_ex_cap_to[wp]:
  "\<lbrace>ex_cte_cap_wp_to P p' and cte_wp_at ((=) cap.NullCap) cref\<rbrace>
     create_cap tp sz p dev (cref, oref)
   \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P p'\<rbrace>" apply (simp add: create_cap_def) apply (wp set_cap_cte_cap_wp_to set_cdt_cte_wp_at
            | simp | wps set_cdt_irq_node)+ apply (clarsimp elim!: cte_wp_at_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_cte_cap_wp_to P p' and cte_wp_at ((=) NullCap) cref\<rbrace> create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P p'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_cte_cap_wp_to P p' and cte_wp_at ((=) NullCap) cref\<rbrace> do dest_p <- gets (\<lambda>s. cdt s cref);
cdt <- gets cdt;
y <- set_cdt (cdt(cref \<mapsto> p));
y <- do_extended_op (create_cap_ext p cref dest_p);
y <- set_original cref True;
set_cap (default_cap tp oref sz dev) cref
od \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P p'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ex_cte_cap_wp_to P p' s \<and> cte_wp_at ((=) NullCap) cref s \<Longrightarrow> cte_wp_at (\<lambda>cap'. p' \<in> cte_refs cap' (interrupt_irq_node s) \<and> P cap' \<longrightarrow> p' \<in> cte_refs (default_cap tp oref sz dev) (interrupt_irq_node s) \<and> P (default_cap tp oref sz dev)) cref s proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma create_cap_no_cap[wp]:
  "\<lbrace>\<lambda>s. (\<forall>p'. \<not> cte_wp_at P p' s) \<and> \<not> P (default_cap tp oref sz dev)\<rbrace>
     create_cap tp sz p dev (cref, oref)
   \<lbrace>\<lambda>rv s. \<forall>oref' cref'. \<not> cte_wp_at P (oref', cref') s\<rbrace>" unfolding create_cap_def cte_wp_at_caps_of_state by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>p'. \<not> cte_wp_at P p' s) \<and> \<not> P (default_cap tp oref sz dev)\<rbrace> create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv s. \<forall>oref' cref'. \<not> cte_wp_at P (oref', cref') s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>p'. \<nexists>cap. caps_of_state s p' = Some cap \<and> P cap) \<and> \<not> P (default_cap tp oref sz dev)\<rbrace> case (cref, oref) of (dest, oref) \<Rightarrow> do dest_p <- gets (\<lambda>s. cdt s dest);
cdt <- gets cdt;
set_cdt (cdt(dest \<mapsto> p));
do_extended_op (create_cap_ext p dest dest_p);
set_original dest True;
set_cap (default_cap tp oref sz dev) dest
od \<lbrace>\<lambda>rv s. \<forall>oref' cref'. \<nexists>cap. caps_of_state s (oref', cref') = Some cap \<and> P cap\<rbrace>
theory Untyped_AI

lemma cap_range_not_untyped:
  "\<not> is_untyped_cap c \<Longrightarrow> cap_range c = obj_refs c" apply (case_tac c) apply (simp_all add: is_cap_simps cap_range_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_untyped_cap c \<Longrightarrow> cap_range c = obj_refs c proof (prove)
goal (12 subgoals):
 1. \<lbrakk>\<not> is_untyped_cap c; c = NullCap\<rbrakk> \<Longrightarrow> cap_range c = obj_refs c
 2. \<And>x21 x22 x23 x24. \<lbrakk>\<not> is_untyped_cap c; c = UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> cap_range c = obj_refs c
 3. \<And>x31 x32 x33. \<lbrakk>\<not> is_untyped_cap c; c = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> cap_range c = obj_refs c
 4. \<And>x41 x42 x43. \<lbrakk>\<not> is_untyped_cap c; c = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> cap_range c = obj_refs c
 5. \<And>x51 x52 x53. \<lbrakk>\<not> is_untyped_cap c; c = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> cap_range c = obj_refs c
 6. \<And>x61 x62 x63. \<lbrakk>\<not> is_untyped_cap c; c = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> cap_range c = obj_refs c
 7. \<And>x7. \<lbrakk>\<not> is_untyped_cap c; c = ThreadCap x7\<rbrakk> \<Longrightarrow> cap_range c = obj_refs c
 8. \<lbrakk>\<not> is_untyped_cap c; c = DomainCap\<rbrakk> \<Longrightarrow> cap_range c = obj_refs c
 9. \<lbrakk>\<not> is_untyped_cap c; c = IRQControlCap\<rbrakk> \<Longrightarrow> cap_range c = obj_refs c
 10. \<And>x10. \<lbrakk>\<not> is_untyped_cap c; c = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> cap_range c = obj_refs c
A total of 12 subgoals... proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma cap_range_inter_emptyI:
  "\<lbrakk>is_untyped_cap a = is_untyped_cap b; untyped_range a \<inter> untyped_range b ={};
    obj_refs a \<inter> obj_refs b = {}\<rbrakk>
   \<Longrightarrow> cap_range a \<inter> cap_range b = {}" apply (case_tac "is_untyped_cap a") apply (simp_all add: cap_range_not_untyped) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_untyped_cap a = is_untyped_cap b; untyped_range a \<inter> untyped_range b = {}; obj_refs a \<inter> obj_refs b = {}\<rbrakk> \<Longrightarrow> cap_range a \<inter> cap_range b = {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_untyped_cap a = is_untyped_cap b; untyped_range a \<inter> untyped_range b = {}; obj_refs a \<inter> obj_refs b = {}; is_untyped_cap a\<rbrakk> \<Longrightarrow> cap_range a \<inter> cap_range b = {}
 2. \<lbrakk>is_untyped_cap a = is_untyped_cap b; untyped_range a \<inter> untyped_range b = {}; obj_refs a \<inter> obj_refs b = {}; \<not> is_untyped_cap a\<rbrakk> \<Longrightarrow> cap_range a \<inter> cap_range b = {} proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma retype_region_cte_at_other':
  "\<lbrace>pspace_no_overlap_range_cover ptr sz and cte_wp_at P p
     and valid_pspace and K (range_cover ptr sz (obj_bits_api ty us) n)\<rbrace>
     retype_region ptr n us ty dev
   \<lbrace>\<lambda>rv. cte_wp_at P p\<rbrace>" apply (rule hoare_gen_asm) apply (wpsimp wp: retype_region_cte_at_other) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_no_overlap (up_aligned_area ptr sz) and cte_wp_at P p and valid_pspace and K (range_cover ptr sz (obj_bits_api ty us) n)\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv. cte_wp_at P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (obj_bits_api ty us) n \<Longrightarrow> \<lbrace>pspace_no_overlap (up_aligned_area ptr sz) and cte_wp_at P p and valid_pspace\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv. cte_wp_at P p\<rbrace> proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma retype_region_ex_cte_cap_to:
  "\<lbrace>pspace_no_overlap_range_cover ptr sz and ex_cte_cap_wp_to P p
     and valid_pspace and K (range_cover ptr sz (obj_bits_api ty us) n)\<rbrace>
     retype_region ptr n us ty dev
   \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P p\<rbrace>" apply (simp add: ex_cte_cap_wp_to_def) apply (wp hoare_vcg_ex_lift retype_region_cte_at_other'
               | wps retype_region_irq_node)+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_no_overlap (up_aligned_area ptr sz) and ex_cte_cap_wp_to P p and valid_pspace and K (range_cover ptr sz (obj_bits_api ty us) n)\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_no_overlap (up_aligned_area ptr sz) and (\<lambda>s. \<exists>a b. cte_wp_at (\<lambda>c. P c \<and> p \<in> cte_refs c (interrupt_irq_node s)) (a, b) s) and valid_pspace and (\<lambda>y. range_cover ptr sz (obj_bits_api ty us) n)\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (\<lambda>c. P c \<and> p \<in> cte_refs c (interrupt_irq_node s)) (a, b) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (pspace_no_overlap (up_aligned_area ptr sz) and (\<lambda>s. \<exists>a b. cte_wp_at (\<lambda>c. P c \<and> p \<in> cte_refs c (interrupt_irq_node s)) (a, b) s) and valid_pspace and (\<lambda>y. range_cover ptr sz (obj_bits_api ty us) n)) s \<Longrightarrow> \<exists>x xa. (pspace_no_overlap (up_aligned_area ptr (?sz10 x xa s)) and cte_wp_at (\<lambda>c. P c \<and> p \<in> cte_refs c (interrupt_irq_node s)) (x, xa) and valid_pspace and K (range_cover ptr (?sz10 x xa s) (obj_bits_api ty us) n)) s proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma ge_mask_eq: "len_of TYPE('a) \<le> n \<Longrightarrow> (x::'a::len word) && mask n = x" by (simp add: mask_def p2_eq_0[THEN iffD2])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. LENGTH('a) \<le> n \<Longrightarrow> x && mask n = x
theory Untyped_AI

lemma do_machine_op_obj_at_arch_state[wp]:
  "\<lbrace>\<lambda>s. P (obj_at (Q (arch_state s)) p s)\<rbrace>
   do_machine_op f
   \<lbrace>\<lambda>_ s. P (obj_at (Q (arch_state s)) p s)\<rbrace>" by (clarsimp simp: do_machine_op_def split_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (obj_at (Q (arch_state s)) p s)\<rbrace> do_machine_op f \<lbrace>\<lambda>_ s. P (obj_at (Q (arch_state s)) p s)\<rbrace>
theory Untyped_AI

lemma invs_arch_state_strg:
  "invs s \<longrightarrow> valid_arch_state s" by (clarsimp simp: invs_def valid_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs s \<longrightarrow> valid_arch_state s
theory Untyped_AI

lemma invs_psp_aligned_strg:
  "invs s \<longrightarrow> pspace_aligned s" by (clarsimp simp: invs_def valid_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs s \<longrightarrow> pspace_aligned s
theory Untyped_AI

lemma invs_cap_refs_in_kernel_window[elim!]:
  "invs s \<Longrightarrow> cap_refs_in_kernel_window s" by (simp add: invs_def valid_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs s \<Longrightarrow> cap_refs_in_kernel_window s
theory Untyped_AI

lemma (in Untyped_AI_nonempty_table) set_cap_nonempty_tables[wp]:
  "\<lbrace>\<lambda>s. P (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) p s)\<rbrace>
     set_cap cap cref
   \<lbrace>\<lambda>rv s. P (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) p s)\<rbrace>" apply (rule hoare_pre) apply (rule hoare_use_eq [where f=arch_state, OF set_cap_arch]) apply (wp set_cap_obj_at_impossible) apply (clarsimp simp: nonempty_table_caps_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) p s)\<rbrace> set_cap cap cref \<lbrace>\<lambda>rv s. P (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) p s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> set_cap cap cref \<lbrace>\<lambda>rv s. P (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) p s)\<rbrace>
 2. \<And>s. P (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) p s) \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrace>?P3 f\<rbrace> set_cap cap cref \<lbrace>\<lambda>rv s. P (obj_at (nonempty_table (set (second_level_tables f))) p s)\<rbrace>
 2. \<And>s. P (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) p s) \<Longrightarrow> ?P3 (arch_state s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. P (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) p s) \<Longrightarrow> P (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) p s) \<and> (\<forall>ko. nonempty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {}) proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma ex_cte_cap_wp_to_def_msu[simp]:
  "ex_cte_cap_wp_to P x (machine_state_update f s)  = ex_cte_cap_wp_to P x s" by (simp add: ex_cte_cap_wp_to_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ex_cte_cap_wp_to P x (machine_state_update f s) = ex_cte_cap_wp_to P x s
theory Untyped_AI

lemma global_refs_detype[simp]: "global_refs (detype S s) = global_refs s" by (simp add: detype_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global_refs (detype S s) = global_refs s
theory Untyped_AI

lemma ex_cte_cap_wp_to_clear_um[simp]:
  "ex_cte_cap_wp_to P p (clear_um T s) = ex_cte_cap_wp_to P p s" by (clarsimp simp: ex_cte_cap_wp_to_def clear_um_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ex_cte_cap_wp_to P p (clear_um T s) = ex_cte_cap_wp_to P p s
theory Untyped_AI

lemma retype_region_aligned_for_init_sz:
  "\<lbrace>\<lambda>s. range_cover ptr sz (obj_bits_api new_type obj_sz) n
      \<and> obj_bits_api new_type obj_sz = some_us_sz\<rbrace>
     retype_region ptr n obj_sz new_type is_dev
   \<lbrace>\<lambda>rv s. \<forall>ref \<in> set rv. is_aligned ref some_us_sz\<rbrace>" apply (rule hoare_name_pre_state) apply (rule hoare_pre, rule hoare_strengthen_post,
    rule retype_region_aligned_for_init, auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. range_cover ptr sz (obj_bits_api new_type obj_sz) n \<and> obj_bits_api new_type obj_sz = some_us_sz\<rbrace> retype_region ptr n obj_sz new_type is_dev \<lbrace>\<lambda>rv s. \<forall>ref\<in>set rv. is_aligned ref some_us_sz\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. range_cover ptr sz (obj_bits_api new_type obj_sz) n \<and> obj_bits_api new_type obj_sz = some_us_sz \<Longrightarrow> \<lbrace>(=) s\<rbrace> retype_region ptr n obj_sz new_type is_dev \<lbrace>\<lambda>rv s. \<forall>ref\<in>set rv. is_aligned ref some_us_sz\<rbrace> proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma (in strengthen_implementation) strengthen_Not[strg]:
  "\<lbrakk> st (\<not> F) (\<longrightarrow>) P P' \<rbrakk>
    \<Longrightarrow> st F (\<longrightarrow>) (\<not> P) (\<not> P')" by (cases F, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st (\<not> F) (\<longrightarrow>) P P' \<Longrightarrow> st F (\<longrightarrow>) (\<not> P) (\<not> P')
theory Untyped_AI

lemma retype_region_ret_folded_general:
  "\<lbrace>\<lambda>s. P (retype_addrs y ty n bits)\<rbrace> retype_region y n bits ty dev
   \<lbrace>\<lambda>r s. P r\<rbrace>" apply (rule hoare_name_pre_state) apply (rule hoare_pre, rule hoare_strengthen_post,
    rule retype_region_ret_folded, auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (retype_addrs y ty n bits)\<rbrace> retype_region y n bits ty dev \<lbrace>\<lambda>r s. P r\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (retype_addrs y ty n bits) \<Longrightarrow> \<lbrace>(=) s\<rbrace> retype_region y n bits ty dev \<lbrace>\<lambda>r s. P r\<rbrace> proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma retype_region_post_retype_invs_folded:
  "\<lbrace>P\<rbrace> retype_region y n bits ty dev \<lbrace>\<lambda>r. post_retype_invs ty r\<rbrace>
    \<Longrightarrow> \<lbrace>P\<rbrace> retype_region y n bits ty dev \<lbrace>\<lambda>r. post_retype_invs ty (retype_addrs y ty n bits)\<rbrace>" apply (rule hoare_strengthen_post,
    rule hoare_vcg_conj_lift[OF retype_region_ret_folded, simplified],
    assumption) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> retype_region y n bits ty dev \<lbrace>post_retype_invs ty\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> retype_region y n bits ty dev \<lbrace>\<lambda>r. post_retype_invs ty (retype_addrs y ty n bits)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>\<lbrace>P\<rbrace> retype_region y n bits ty dev \<lbrace>post_retype_invs ty\<rbrace>; rv = retype_addrs y ty n bits \<and> post_retype_invs ty rv s\<rbrakk> \<Longrightarrow> post_retype_invs ty (retype_addrs y ty n bits) s proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma tup_in_fst_image_set_zipD:
  "x \<in> fst ` set (zip xs ys) \<Longrightarrow> x \<in> set xs" by (auto dest!: set_zip_helper)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> fst ` set (zip xs ys) \<Longrightarrow> x \<in> set xs