kings-crown/FVELER_Isabelle huggingface dataset:
theory Retype_AI

lemma unique_reply_caps:
  "unique_reply_caps (caps_of_state s) \<Longrightarrow> unique_reply_caps (caps_of_state s')" using caps_retype by (fastforce simp add: is_cap_simps unique_reply_caps_def
               simp del: split_paired_All
                  elim!: allEI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unique_reply_caps (caps_of_state s) \<Longrightarrow> unique_reply_caps (caps_of_state s') proof (prove)
using this:
\<lbrakk>?cap \<noteq> NullCap; caps_of_state s' ?p = Some ?cap\<rbrakk> \<Longrightarrow> caps_of_state s ?p = Some ?cap

goal (1 subgoal):
 1. unique_reply_caps (caps_of_state s) \<Longrightarrow> unique_reply_caps (caps_of_state s')
theory Retype_AI

lemma valid_reply_caps:
  "valid_reply_caps s \<Longrightarrow> valid_reply_caps s'" by (clarsimp simp: valid_reply_caps_def unique_reply_caps has_reply_cap_def
                     pred_tcb_at_pres cte_retype is_reply_cap_to_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_reply_caps s \<Longrightarrow> valid_reply_caps s'
theory Retype_AI

lemma valid_reply_masters:
  "valid_reply_masters s \<Longrightarrow> valid_reply_masters s'" by (clarsimp simp: valid_reply_masters_def cte_retype is_cap_simps obj_at_pres is_master_reply_cap_to_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_reply_masters s \<Longrightarrow> valid_reply_masters s'
theory Retype_AI

lemma ran_null_filter:
  "ran (null_filter m) = (ran m - {cap.NullCap})" apply (simp add: null_filter_def ran_def cong: conj_cong) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ran (null_filter m) = ran m - {NullCap} proof (prove)
goal (1 subgoal):
 1. {b. \<exists>a. m a \<noteq> Some NullCap \<and> m a = Some b} = {b. \<exists>a. m a = Some b} - {NullCap} proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma valid_irq_handlers_def2:
  "valid_irq_handlers =
     (\<lambda>s. \<forall>cap \<in> ran (null_filter (caps_of_state s)).
          \<forall>irq \<in> cap_irqs cap. interrupt_states s irq = irq_state.IRQSignal)" apply (rule ext) apply (simp add: valid_irq_handlers_def irq_issued_def
                   ran_null_filter) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_irq_handlers = (\<lambda>s. \<forall>cap\<in>ran (null_filter (caps_of_state s)). \<forall>irq\<in>cap_irqs cap. interrupt_states s irq = IRQSignal) proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_irq_handlers s = (\<forall>cap\<in>ran (null_filter (caps_of_state s)). \<forall>irq\<in>cap_irqs cap. interrupt_states s irq = IRQSignal) proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>cap\<in>ran (caps_of_state s). \<forall>irq\<in>cap_irqs cap. interrupt_states s irq = IRQSignal) = (\<forall>cap\<in>ran (caps_of_state s) - {NullCap}. \<forall>irq\<in>cap_irqs cap. interrupt_states s irq = IRQSignal) proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma p_in_obj_range:
  "\<lbrakk> kheap s p = Some ko; pspace_aligned s; valid_objs s \<rbrakk> \<Longrightarrow> p \<in> obj_range p ko" apply (simp add: pspace_aligned_def) apply (drule bspec, erule domI) apply (drule valid_obj_sizes, erule ranI) apply (simp add: obj_range_def add_diff_eq[symmetric]) apply (erule is_aligned_no_wrap') apply (erule word_power_less_1[where 'a=machine_word_len, folded word_bits_def]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some ko; pspace_aligned s; valid_objs s\<rbrakk> \<Longrightarrow> p \<in> obj_range p ko proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some ko; \<forall>x\<in>dom (kheap s). is_aligned x (obj_bits (the (kheap s x))); valid_objs s\<rbrakk> \<Longrightarrow> p \<in> obj_range p ko proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some ko; valid_objs s; is_aligned p (obj_bits (the (kheap s p)))\<rbrakk> \<Longrightarrow> p \<in> obj_range p ko proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some ko; is_aligned p (obj_bits (the (kheap s p))); obj_bits ko < word_bits\<rbrakk> \<Longrightarrow> p \<in> obj_range p ko proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some ko; is_aligned p (obj_bits ko); obj_bits ko < word_bits\<rbrakk> \<Longrightarrow> p \<le> p + (2 ^ obj_bits ko - 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some ko; obj_bits ko < word_bits\<rbrakk> \<Longrightarrow> 2 ^ obj_bits ko - 1 < 2 ^ obj_bits ko proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma p_in_obj_range_internal:
  "\<lbrakk> kheap s (p && ~~ mask (obj_bits ko))= Some ko; pspace_aligned s; valid_objs s \<rbrakk>
  \<Longrightarrow> p \<in> obj_range (p && ~~ mask (obj_bits ko)) ko" apply (drule p_in_obj_range,simp+) apply (simp add: obj_range_def word_and_le2 word_neg_and_le p_assoc_help) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s (p && ~~ mask (obj_bits ko)) = Some ko; pspace_aligned s; valid_objs s\<rbrakk> \<Longrightarrow> p \<in> obj_range (p && ~~ mask (obj_bits ko)) ko proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_aligned s; valid_objs s; p && ~~ mask (obj_bits ko) \<in> obj_range (p && ~~ mask (obj_bits ko)) ko\<rbrakk> \<Longrightarrow> p \<in> obj_range (p && ~~ mask (obj_bits ko)) ko proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma interrupt_states:
  "interrupt_states s' = interrupt_states s" by (simp add: s'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. interrupt_states s' = interrupt_states s
theory Retype_AI

lemma valid_irq_handlers:
  "valid_irq_handlers s \<Longrightarrow> valid_irq_handlers s'" by (simp add: valid_irq_handlers_def2 null_filter
                interrupt_states)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_irq_handlers s \<Longrightarrow> valid_irq_handlers s'
theory Retype_AI

lemma mdb_and_revokable:
  "cdt s' = cdt s"
  "is_original_cap s' = is_original_cap s" by (simp add: s'_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdt s' = cdt s &&& is_original_cap s' = is_original_cap s
theory Retype_AI

lemma only_idle:
  "only_idle s \<Longrightarrow> only_idle s'" apply (clarsimp simp: only_idle_def) apply (clarsimp simp: s'_def pred_tcb_at_def obj_at_def ps_def split: if_split_asm) apply (simp add: default_object_def tyunt split: Structures_A.apiobject_type.splits) apply (simp add: default_tcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. only_idle s \<Longrightarrow> only_idle s' proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>\<forall>t. st_tcb_at idle t s \<longrightarrow> t = idle_thread s; st_tcb_at idle t s'\<rbrakk> \<Longrightarrow> t = idle_thread s' proof (prove)
goal (1 subgoal):
 1. \<And>t tcb. \<lbrakk>\<forall>t. (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> idle (tcb_state tcb))) \<longrightarrow> t = idle_thread s; t \<in> set (retype_addrs ptr ty n us); default_object ty dev us = TCB tcb; idle (tcb_state tcb)\<rbrakk> \<Longrightarrow> t = idle_thread s proof (prove)
goal (1 subgoal):
 1. \<And>t tcb. \<lbrakk>idle (tcb_state default_tcb); \<forall>t. (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> idle (tcb_state tcb))) \<longrightarrow> t = idle_thread s; t \<in> set (retype_addrs ptr TCBObject n us); ty = TCBObject; default_tcb = tcb\<rbrakk> \<Longrightarrow> t = idle_thread s proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma valid_irq_states:
  "valid_irq_states s \<Longrightarrow> valid_irq_states s'" apply(simp add: s'_def valid_irq_states_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_irq_states s \<Longrightarrow> valid_irq_states s' proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma cap_refs_in_kernel_window:
  "cap_refs_in_kernel_window s \<Longrightarrow> cap_refs_in_kernel_window s'" apply (simp add: cap_refs_in_kernel_window_def valid_refs_def) apply (simp add: cte_retype cap_range_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_refs_in_kernel_window s \<Longrightarrow> cap_refs_in_kernel_window s' proof (prove)
goal (1 subgoal):
 1. \<forall>a b. \<not> cte_wp_at (\<lambda>c. ARM.not_kernel_window_arch (arch_state s) \<inter> cap_range c \<noteq> {}) (a, b) s \<Longrightarrow> \<forall>a b. \<not> cte_wp_at (\<lambda>c. ARM.not_kernel_window_arch (arch_state s) \<inter> cap_range c \<noteq> {}) (a, b) s' proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma valid_ioc:
  "valid_ioc s \<Longrightarrow> valid_ioc s'" using cte_retype by (simp add: valid_ioc_def s'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_ioc s \<Longrightarrow> valid_ioc s' proof (prove)
using this:
\<not> ?P NullCap \<Longrightarrow> cte_wp_at ?P ?p s' = cte_wp_at ?P ?p s

goal (1 subgoal):
 1. valid_ioc s \<Longrightarrow> valid_ioc s'
theory Retype_AI

lemma invs_trans_state[simp]:
  "invs (trans_state f s) = invs s" apply (simp add: invs_def valid_state_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs (trans_state f s) = invs s proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma post_retype_invs_trans_state[simp]:
  "post_retype_invs ty refs (trans_state f s) = post_retype_invs ty refs s" apply (simp add: post_retype_invs_def') apply (simp add: trans_state_update[symmetric] del: trans_state_update) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. post_retype_invs ty refs (trans_state f s) = post_retype_invs ty refs s proof (prove)
goal (1 subgoal):
 1. post_retype_invs_check ty \<longrightarrow> (equal_kernel_mappings (trans_state f s\<lparr>kheap := kheap s |` (- set refs)\<rparr>) \<and> valid_pspace s \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_irq_states s \<and> valid_global_objs s \<and> valid_arch_caps s \<and> valid_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> valid_ioc s \<and> valid_machine_state s \<and> valid_ioports s) = (equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- set refs)\<rparr>) \<and> valid_pspace s \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_irq_states s \<and> valid_global_objs s \<and> valid_arch_caps s \<and> valid_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> valid_ioc s \<and> valid_machine_state s \<and> valid_ioports s) proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma subset_not_le_trans: "\<lbrakk>\<not> A \<subset> B; C \<subseteq> B\<rbrakk> \<Longrightarrow> \<not> A \<subset> C" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> A \<subset> B; C \<subseteq> B\<rbrakk> \<Longrightarrow> \<not> A \<subset> C
theory Retype_AI

lemma cte_wp_at_trans_state[simp]: "cte_wp_at P ptr (kheap_update f (trans_state f' s)) =
       cte_wp_at P ptr (kheap_update f s)" by (simp add: trans_state_update[symmetric] del: trans_state_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at P ptr (kheap_update f (trans_state f' s)) = cte_wp_at P ptr (kheap_update f s)
theory Retype_AI

lemma retype_cte_wp_at:
  "\<lbrace>\<lambda>s. cte_wp_at P ptr s \<and> pspace_no_overlap_range_cover ptr' sz s \<and>
       valid_pspace s \<and> range_cover ptr' sz (obj_bits_api ty us) n\<rbrace>
  retype_region ptr' n us ty dev
  \<lbrace>\<lambda>r. cte_wp_at P ptr\<rbrace>" apply (rule hoare_assume_pre) apply (rule hoare_pre) apply (rule retype_region_cte_at_other) apply fastforce apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at P ptr s \<and> pspace_no_overlap (up_aligned_area ptr' sz) s \<and> valid_pspace s \<and> range_cover ptr' sz (obj_bits_api ty us) n\<rbrace> retype_region ptr' n us ty dev \<lbrace>\<lambda>r. cte_wp_at P ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at P ptr s \<and> pspace_no_overlap (up_aligned_area ptr' sz) s \<and> valid_pspace s \<and> range_cover ptr' sz (obj_bits_api ty us) n \<Longrightarrow> \<lbrace>\<lambda>s. cte_wp_at P ptr s \<and> pspace_no_overlap (up_aligned_area ptr' sz) s \<and> valid_pspace s \<and> range_cover ptr' sz (obj_bits_api ty us) n\<rbrace> retype_region ptr' n us ty dev \<lbrace>\<lambda>r. cte_wp_at P ptr\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. cte_wp_at P ptr s \<and> pspace_no_overlap (up_aligned_area ptr' sz) s \<and> valid_pspace s \<and> range_cover ptr' sz (obj_bits_api ty us) n \<Longrightarrow> \<lbrace>?Q2 s\<rbrace> retype_region ptr' n us ty dev \<lbrace>\<lambda>r. cte_wp_at P ptr\<rbrace>
 2. \<And>s sa. \<lbrakk>cte_wp_at P ptr s \<and> pspace_no_overlap (up_aligned_area ptr' sz) s \<and> valid_pspace s \<and> range_cover ptr' sz (obj_bits_api ty us) n; cte_wp_at P ptr sa \<and> pspace_no_overlap (up_aligned_area ptr' sz) sa \<and> valid_pspace sa \<and> range_cover ptr' sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> ?Q2 s sa proof (prove)
goal (2 subgoals):
 1. \<And>s. cte_wp_at P ptr s \<and> pspace_no_overlap (up_aligned_area ptr' sz) s \<and> valid_pspace s \<and> range_cover ptr' sz (obj_bits_api ty us) n \<Longrightarrow> range_cover ptr' (?sz5 s) (obj_bits_api ty us) n
 2. \<And>s sa. \<lbrakk>cte_wp_at P ptr s \<and> pspace_no_overlap (up_aligned_area ptr' sz) s \<and> valid_pspace s \<and> range_cover ptr' sz (obj_bits_api ty us) n; cte_wp_at P ptr sa \<and> pspace_no_overlap (up_aligned_area ptr' sz) sa \<and> valid_pspace sa \<and> range_cover ptr' sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area ptr' (?sz5 s)) sa \<and> cte_wp_at P ptr sa \<and> valid_pspace sa proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>cte_wp_at P ptr s \<and> pspace_no_overlap (up_aligned_area ptr' sz) s \<and> valid_pspace s \<and> range_cover ptr' sz (obj_bits_api ty us) n; cte_wp_at P ptr sa \<and> pspace_no_overlap (up_aligned_area ptr' sz) sa \<and> valid_pspace sa \<and> range_cover ptr' sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area ptr' sz) sa \<and> cte_wp_at P ptr sa \<and> valid_pspace sa proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma pspace_no_overlap_typ_at_def:
  "pspace_no_overlap S =
  (\<lambda>s. \<forall>T x. typ_at T x s \<longrightarrow> {x..x + (2 ^ obj_bits_type T - 1)} \<inter> S = {})" apply (simp add: pspace_no_overlap_def obj_at_def) apply (rule ext) apply (auto simp: obj_bits_T) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_no_overlap S = (\<lambda>s. \<forall>T x. typ_at T x s \<longrightarrow> {x..x + (2 ^ obj_bits_type T - 1)} \<inter> S = {}) proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. \<forall>x ko. kheap s x = Some ko \<longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> S = {}) = (\<lambda>s. \<forall>T x. (\<exists>ko. kheap s x = Some ko \<and> a_type ko = T) \<longrightarrow> {x..x + (2 ^ obj_bits_type T - 1)} \<inter> S = {}) proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>x ko. kheap s x = Some ko \<longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> S = {}) = (\<forall>T x. (\<exists>ko. kheap s x = Some ko \<and> a_type ko = T) \<longrightarrow> {x..x + (2 ^ obj_bits_type T - 1)} \<inter> S = {}) proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma pspace_no_overlap_typ_at_lift:
  assumes f: "\<And>P T p. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>"
  shows "\<lbrace>pspace_no_overlap S\<rbrace> f \<lbrace>\<lambda>rv. pspace_no_overlap S\<rbrace>" apply (clarsimp simp: pspace_no_overlap_typ_at_def) apply (wp hoare_vcg_all_lift f) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_no_overlap S\<rbrace> f \<lbrace>\<lambda>rv. pspace_no_overlap S\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>T x. typ_at T x s \<longrightarrow> {x..x + (2 ^ obj_bits_type T - 1)} \<inter> S = {}\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>T x. typ_at T x s \<longrightarrow> {x..x + (2 ^ obj_bits_type T - 1)} \<inter> S = {}\<rbrace> proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma swp_clearMemoryVM [simp]:
  "swp clearMemoryVM x = (\<lambda>_. return ())" by (rule ext,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. swp clearMemoryVM x = (\<lambda>_. return ())
theory Retype_AI

lemma ioc_more_swap[simp]: "
    s'\<lparr>exst := sa',
         is_original_cap := sa\<rparr> =
    s'\<lparr>is_original_cap := sa,
         exst := sa'\<rparr>" apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s'\<lparr>exst := sa', is_original_cap := sa\<rparr> = s'\<lparr>is_original_cap := sa, exst := sa'\<rparr> proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma is_final_cap'_more_update[simp]:
  "is_final_cap' cap (trans_state f s) = is_final_cap' cap s" by (simp add: is_final_cap'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_final_cap' cap (trans_state f s) = is_final_cap' cap s
theory Retype_AI

lemma no_cap_to_obj_with_diff_ref_more_update[simp]:
  "no_cap_to_obj_with_diff_ref cap sl (trans_state f s) =
   no_cap_to_obj_with_diff_ref cap sl s" by (simp add: no_cap_to_obj_with_diff_ref_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_cap_to_obj_with_diff_ref cap sl (trans_state f s) = no_cap_to_obj_with_diff_ref cap sl s
theory Retype_AI

lemma cte_wp_at_irq_state_independent[intro!, simp]:
  "is_final_cap' x (s\<lparr>machine_state := machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>)
   = is_final_cap' x s" by (simp add: is_final_cap'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_final_cap' x (s\<lparr>machine_state := machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>) = is_final_cap' x s
theory Retype_AI

lemma zombies_final_irq_state_independent[intro!, simp]:
  "zombies_final (s\<lparr>machine_state := machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>)
   = zombies_final s" by (simp add: zombies_final_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. zombies_final (s\<lparr>machine_state := machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>) = zombies_final s
theory Retype_AI

lemma ex_cte_cap_wp_to_irq_state_independent[intro!, simp]:
  "ex_cte_cap_wp_to x y (s\<lparr>machine_state := machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>)
   = ex_cte_cap_wp_to x y s" by (simp add: ex_cte_cap_wp_to_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ex_cte_cap_wp_to x y (s\<lparr>machine_state := machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>) = ex_cte_cap_wp_to x y s
theory ArchRetype_AI

lemma arch_kobj_size_cong[Retype_AI_assms]:
"\<lbrakk>a = a1; c=c1\<rbrakk> \<Longrightarrow> arch_kobj_size (default_arch_object a b c)
  = arch_kobj_size (default_arch_object a1 b1 c1)" by (simp add: default_arch_object_def split: aobject_type.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a = a1; c = c1\<rbrakk> \<Longrightarrow> arch_kobj_size (default_arch_object a b c) = arch_kobj_size (default_arch_object a1 b1 c1)
theory ArchRetype_AI

lemma slot_bits_def2 [Retype_AI_assms]: "slot_bits = cte_level_bits" by (simp add: slot_bits_def cte_level_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. slot_bits = cte_level_bits
theory ArchRetype_AI

lemma no_gs_types_simps [simp, Retype_AI_assms]:
  "Untyped \<in> no_gs_types"
  "TCBObject \<in> no_gs_types"
  "EndpointObject \<in> no_gs_types"
  "NotificationObject \<in> no_gs_types"
  "ArchObject PageTableObj \<in> no_gs_types"
  "ArchObject PageDirectoryObj \<in> no_gs_types"
  "ArchObject ASIDPoolObj \<in> no_gs_types" by (simp_all add: no_gs_types_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (Untyped \<in> no_gs_types &&& TCBObject \<in> no_gs_types &&& EndpointObject \<in> no_gs_types) &&& (NotificationObject \<in> no_gs_types &&& ArchObject PageTableObj \<in> no_gs_types) &&& ArchObject PageDirectoryObj \<in> no_gs_types &&& ArchObject ASIDPoolObj \<in> no_gs_types
theory ArchRetype_AI

lemma retype_region_ret_folded [Retype_AI_assms]:
  "\<lbrace>\<top>\<rbrace> retype_region y n bits ty dev
   \<lbrace>\<lambda>r s. r = retype_addrs y ty n bits\<rbrace>" unfolding retype_region_def apply (simp add: pageBits_def) apply wp apply (simp add: retype_addrs_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> retype_region y n bits ty dev \<lbrace>\<lambda>r s. r = retype_addrs y ty n bits\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do obj_size <- return $ 2 ^ obj_bits_api ty bits;
ptrs <- return $ map (\<lambda>p. ptr_add y (p * obj_size)) [0..<n];
when (ty \<noteq> Untyped) (do kh <- gets kheap;
kh' <- return $ foldr (\<lambda>p kh. kh(p \<mapsto> default_object ty dev bits)) ptrs kh;
do_extended_op (retype_region_ext ptrs ty);
modify $ kheap_update (K kh')
od);
return $ ptrs
od \<lbrace>\<lambda>r s. r = retype_addrs y ty n bits\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do ya <- when (ty \<noteq> Untyped) (do kh <- gets kheap;
ya <- do_extended_op (retype_region_ext (map (\<lambda>p. ptr_add y (p * 2 ^ obj_bits_api ty bits)) [0..<n]) ty);
modify (kheap_update (\<lambda>ya. foldr (\<lambda>p kh. kh(p \<mapsto> default_object ty dev bits)) (map (\<lambda>p. ptr_add y (p * 2 ^ obj_bits_api ty bits)) [0..<n]) kh))
od);
return (map (\<lambda>p. ptr_add y (p * 2 ^ obj_bits_api ty bits)) [0..<n])
od \<lbrace>\<lambda>r s. r = retype_addrs y ty n bits\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> map (\<lambda>p. ptr_add y (p * 2 ^ obj_bits_api ty bits)) [0..<n] = retype_addrs y ty n bits proof (prove)
goal:
No subgoals!
theory ArchRetype_AI

lemma mdb_cte_at_store_pde[wp]:
  "\<lbrace>\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace>
   store_pde y pde
   \<lbrace>\<lambda>r s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace>" apply (clarsimp simp: mdb_cte_at_def) apply (simp only: imp_conv_disj) apply (wp hoare_vcg_disj_lift hoare_vcg_all_lift) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s)\<rbrace> store_pde y pde \<lbrace>\<lambda>r s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) s\<rbrace> store_pde y pde \<lbrace>\<lambda>r s. \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>a b aa ba. cdt s (aa, ba) \<noteq> Some (a, b) \<or> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) s\<rbrace> store_pde y pde \<lbrace>\<lambda>r s. \<forall>a b aa ba. cdt s (aa, ba) \<noteq> Some (a, b) \<or> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) s\<rbrace> proof (prove)
goal:
No subgoals!