kings-crown/FVELER_Isabelle huggingface dataset:
theory IpcCancel_AI

lemma descendants_of_nullcap:
  "\<lbrakk>descendants_of (a, b) (cdt s) \<noteq> {}; valid_mdb s \<rbrakk> \<Longrightarrow> caps_of_state s (a, b) \<noteq> Some NullCap" apply clarsimp apply (drule_tac cs="caps_of_state s" and p="(a,b)" and m="(cdt s)" in mdb_cte_at_Null_descendants) apply (clarsimp simp: valid_mdb_def2)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>descendants_of (a, b) (cdt s) \<noteq> {}; valid_mdb s\<rbrakk> \<Longrightarrow> caps_of_state s (a, b) \<noteq> Some NullCap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>descendants_of (a, b) (cdt s) \<noteq> {}; valid_mdb s; caps_of_state s (a, b) = Some NullCap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>descendants_of (a, b) (cdt s) \<noteq> {}; valid_mdb s\<rbrakk> \<Longrightarrow> mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s)
 2. \<lbrakk>descendants_of (a, b) (cdt s) \<noteq> {}; valid_mdb s; descendants_of (a, b) (cdt s) = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory IpcCancel_AI

lemma bound_refs_of_tcb_trans:
  "bound_refs_of_tcb (trans_state f s) x = bound_refs_of_tcb s x" by (clarsimp simp:bound_refs_of_tcb_def trans_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bound_refs_of_tcb (trans_state f s) x = bound_refs_of_tcb s x
theory IpcCancel_AI

lemma ep_no_bound_refs:
  "ep_at p s \<Longrightarrow> {r \<in> state_refs_of s p. snd r = TCBBound} = {}" by (clarsimp simp: obj_at_def state_refs_of_def refs_of_def is_ep ep_q_refs_of_def split: endpoint.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ep_at p s \<Longrightarrow> {r \<in> state_refs_of s p. snd r = TCBBound} = {}
theory IpcCancel_AI

lemma obj_at_conj_distrib:
  "obj_at (\<lambda>ko. P ko \<and> Q ko) p s \<Longrightarrow> obj_at (\<lambda>ko. P ko) p s \<and> obj_at (\<lambda>ko. Q ko) p s" by (auto simp:obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at (\<lambda>ko. P ko \<and> Q ko) p s \<Longrightarrow> obj_at P p s \<and> obj_at Q p s
theory IpcCancel_AI

lemma ep_q_refs_of_no_ntfn_bound:
  "(x, tp) \<in> ep_q_refs_of ep \<Longrightarrow> tp \<noteq> NTFNBound" by (auto simp: ep_q_refs_of_def split:endpoint.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, tp) \<in> ep_q_refs_of ep \<Longrightarrow> tp \<noteq> NTFNBound
theory IpcCancel_AI

lemma ep_q_refs_no_NTFNBound:
  "(x, NTFNBound) \<notin> ep_q_refs_of ep" by (clarsimp simp: ep_q_refs_of_def split:endpoint.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, NTFNBound) \<notin> ep_q_refs_of ep
theory IpcCancel_AI

lemma ep_list_tcb_at:
  "\<lbrakk>ep_at p s; valid_objs s; state_refs_of s p = set q \<times> {k}; x \<in> set q \<rbrakk> \<Longrightarrow> tcb_at x s" apply (erule (1) obj_at_valid_objsE) apply (fastforce simp:is_ep valid_obj_def valid_ep_def state_refs_of_def split:endpoint.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ep_at p s; valid_objs s; state_refs_of s p = set q \<times> {k}; x \<in> set q\<rbrakk> \<Longrightarrow> tcb_at x s proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>valid_objs s; state_refs_of s p = set q \<times> {k}; x \<in> set q; kheap s p = Some ko; is_ep ko; valid_obj p ko s\<rbrakk> \<Longrightarrow> tcb_at x s proof (prove)
goal:
No subgoals!
theory IpcCancel_AI

lemma ep_no_ntfn_bound:
  "\<lbrakk>is_ep ko; refs_of ko = set q \<times> {NTFNBound}; y \<in> set q \<rbrakk> \<Longrightarrow> False" apply (subst (asm) set_eq_iff) apply (drule_tac x="(y, NTFNBound)" in spec) apply (clarsimp simp: refs_of_rev is_ep) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_ep ko; refs_of ko = set q \<times> {NTFNBound}; y \<in> set q\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_ep ko; \<forall>x. (x \<in> refs_of ko) = (x \<in> set q \<times> {NTFNBound}); y \<in> set q\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_ep ko; y \<in> set q; ((y, NTFNBound) \<in> refs_of ko) = ((y, NTFNBound) \<in> set q \<times> {NTFNBound})\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory IpcCancel_AI

lemma ntfn_q_refs_no_NTFNBound:
  "(x, NTFNBound) \<notin> ntfn_q_refs_of ntfn" by (auto simp: ntfn_q_refs_of_def split:ntfn.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, NTFNBound) \<notin> ntfn_q_refs_of ntfn
theory IpcCancel_AI

lemma ntfn_q_refs_no_TCBBound:
  "(x, TCBBound) \<notin> ntfn_q_refs_of ntfn" by (auto simp: ntfn_q_refs_of_def split:ntfn.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, TCBBound) \<notin> ntfn_q_refs_of ntfn
theory IpcCancel_AI

lemma ntfn_bound_tcb_get_set[simp]:
  "ntfn_bound_tcb (ntfn_set_bound_tcb ntfn ntfn') = ntfn'" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ntfn_bound_tcb (ntfn_set_bound_tcb ntfn ntfn') = ntfn'
theory IpcCancel_AI

lemma ntfn_obj_tcb_get_set[simp]:
  "ntfn_obj (ntfn_set_bound_tcb ntfn ntfn') = ntfn_obj ntfn" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ntfn_obj (ntfn_set_bound_tcb ntfn ntfn') = ntfn_obj ntfn
theory IpcCancel_AI

lemma valid_ntfn_set_bound_None:
  "valid_ntfn ntfn s \<Longrightarrow> valid_ntfn (ntfn_set_bound_tcb ntfn None) s" by (auto simp: valid_ntfn_def split:ntfn.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_ntfn ntfn s \<Longrightarrow> valid_ntfn (ntfn_set_bound_tcb ntfn None) s
theory IpcCancel_AI

lemma ntfn_bound_tcb_at:
  "\<lbrakk>sym_refs (state_refs_of s); valid_objs s; kheap s ntfnptr = Some (Notification ntfn);
    ntfn_bound_tcb ntfn = Some tcbptr; P (Some ntfnptr)\<rbrakk>
  \<Longrightarrow> bound_tcb_at P tcbptr s" apply (drule_tac x=ntfnptr in sym_refsD[rotated]) apply (fastforce simp: state_refs_of_def) apply (fastforce simp: pred_tcb_at_def obj_at_def valid_obj_def valid_ntfn_def is_tcb
                         state_refs_of_def refs_of_rev
                   simp del: refs_of_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sym_refs (state_refs_of s); valid_objs s; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some tcbptr; P (Some ntfnptr)\<rbrakk> \<Longrightarrow> bound_tcb_at P tcbptr s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_objs s; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some tcbptr; P (Some ntfnptr)\<rbrakk> \<Longrightarrow> (?y, ?tp) \<in> state_refs_of s ntfnptr
 2. \<lbrakk>valid_objs s; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some tcbptr; P (Some ntfnptr); (ntfnptr, symreftype ?tp) \<in> state_refs_of s ?y\<rbrakk> \<Longrightarrow> bound_tcb_at P tcbptr s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some tcbptr; P (Some ntfnptr); (ntfnptr, symreftype NTFNBound) \<in> state_refs_of s tcbptr\<rbrakk> \<Longrightarrow> bound_tcb_at P tcbptr s proof (prove)
goal:
No subgoals!
theory IpcCancel_AI

lemma bound_tcb_bound_notification_at:
  "\<lbrakk>sym_refs (state_refs_of s); valid_objs s; kheap s ntfnptr = Some (Notification ntfn);
    bound_tcb_at (\<lambda>ptr. ptr = (Some ntfnptr)) tcbptr s \<rbrakk>
  \<Longrightarrow> ntfn_bound_tcb ntfn = Some tcbptr" apply (drule_tac x=tcbptr in sym_refsD[rotated]) apply (fastforce simp: state_refs_of_def pred_tcb_at_def obj_at_def) apply (auto simp: pred_tcb_at_def obj_at_def valid_obj_def valid_ntfn_def is_tcb
                    state_refs_of_def refs_of_rev
          simp del: refs_of_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sym_refs (state_refs_of s); valid_objs s; kheap s ntfnptr = Some (Notification ntfn); bound_tcb_at (\<lambda>ptr. ptr = Some ntfnptr) tcbptr s\<rbrakk> \<Longrightarrow> ntfn_bound_tcb ntfn = Some tcbptr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_objs s; kheap s ntfnptr = Some (Notification ntfn); bound_tcb_at (\<lambda>ptr. ptr = Some ntfnptr) tcbptr s\<rbrakk> \<Longrightarrow> (?y, ?tp) \<in> state_refs_of s tcbptr
 2. \<lbrakk>valid_objs s; kheap s ntfnptr = Some (Notification ntfn); bound_tcb_at (\<lambda>ptr. ptr = Some ntfnptr) tcbptr s; (tcbptr, symreftype ?tp) \<in> state_refs_of s ?y\<rbrakk> \<Longrightarrow> ntfn_bound_tcb ntfn = Some tcbptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; kheap s ntfnptr = Some (Notification ntfn); bound_tcb_at (\<lambda>ptr. ptr = Some ntfnptr) tcbptr s; (tcbptr, symreftype TCBBound) \<in> state_refs_of s ntfnptr\<rbrakk> \<Longrightarrow> ntfn_bound_tcb ntfn = Some tcbptr proof (prove)
goal:
No subgoals!
theory IpcCancel_AI

lemma tcb_at_ko_at:
  "tcb_at p s \<Longrightarrow> \<exists>tcb. ko_at (TCB tcb) p s" by (fastforce simp: obj_at_def is_tcb)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_at p s \<Longrightarrow> \<exists>tcb. ko_at (TCB tcb) p s
theory IpcCancel_AI

lemma tcb_state_refs_no_tcb:
  "\<lbrakk>valid_objs s; tcb_at y s; (x, ref) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> ~ tcb_at x s" apply (clarsimp simp: ko_at_state_refs_ofD dest!: tcb_at_ko_at) apply (erule (1) obj_at_valid_objsE) apply (clarsimp simp: is_tcb valid_obj_def) apply (erule disjE) apply (clarsimp simp: tcb_st_refs_of_def valid_tcb_def valid_tcb_state_def obj_at_def is_ep is_ntfn
                  split:thread_state.splits) apply (clarsimp simp: tcb_bound_refs_def valid_tcb_def obj_at_def is_ntfn
                  split:option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; tcb_at y s; (x, ref) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> \<not> tcb_at x s proof (prove)
goal (1 subgoal):
 1. \<And>tcb tcba. \<lbrakk>valid_objs s; (x, ref) \<in> tcb_st_refs_of (tcb_state tcb) \<or> (x, ref) \<in> tcb_bound_refs (tcb_bound_notification tcb); ko_at (TCB tcb) y s; ko_at (TCB tcba) x s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>tcb tcba ko. \<lbrakk>valid_objs s; (x, ref) \<in> tcb_st_refs_of (tcb_state tcb) \<or> (x, ref) \<in> tcb_bound_refs (tcb_bound_notification tcb); ko_at (TCB tcba) x s; kheap s y = Some ko; TCB tcb = ko; valid_obj y ko s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>tcb tcba. \<lbrakk>valid_objs s; (x, ref) \<in> tcb_st_refs_of (tcb_state tcb) \<or> (x, ref) \<in> tcb_bound_refs (tcb_bound_notification tcb); ko_at (TCB tcba) x s; kheap s y = Some (TCB tcb); valid_tcb y tcb s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>tcb tcba. \<lbrakk>valid_objs s; ko_at (TCB tcba) x s; kheap s y = Some (TCB tcb); valid_tcb y tcb s; (x, ref) \<in> tcb_st_refs_of (tcb_state tcb)\<rbrakk> \<Longrightarrow> False
 2. \<And>tcb tcba. \<lbrakk>valid_objs s; ko_at (TCB tcba) x s; kheap s y = Some (TCB tcb); valid_tcb y tcb s; (x, ref) \<in> tcb_bound_refs (tcb_bound_notification tcb)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>tcb tcba. \<lbrakk>valid_objs s; ko_at (TCB tcba) x s; kheap s y = Some (TCB tcb); valid_tcb y tcb s; (x, ref) \<in> tcb_bound_refs (tcb_bound_notification tcb)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory IpcCancel_AI

lemma cancel_badged_sends_invs_helper:
  "{r. snd r \<noteq> TCBBound \<and>
       (r \<in> tcb_st_refs_of ts \<or> r \<in> tcb_bound_refs ntfnptr)} =
   tcb_st_refs_of ts" by (auto simp add: tcb_st_refs_of_def tcb_bound_refs_def split: thread_state.splits option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {r. snd r \<noteq> TCBBound \<and> (r \<in> tcb_st_refs_of ts \<or> r \<in> tcb_bound_refs ntfnptr)} = tcb_st_refs_of ts
theory IpcCancel_AI

lemma real_cte_emptyable_strg:
  "real_cte_at p s \<longrightarrow> emptyable p s" by (clarsimp simp: emptyable_def obj_at_def is_tcb is_cap_table)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. real_cte_at p s \<longrightarrow> emptyable p s
theory InterruptAcc_AI

lemma get_irq_slot_real_cte[wp]:
  "\<lbrace>invs\<rbrace> get_irq_slot irq \<lbrace>real_cte_at\<rbrace>" apply (simp add: get_irq_slot_def) apply wp apply (clarsimp simp: invs_def valid_state_def valid_irq_node_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> get_irq_slot irq \<lbrace>real_cte_at\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> gets (\<lambda>st. (interrupt_irq_node st irq, [])) \<lbrace>real_cte_at\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<Longrightarrow> real_cte_at (interrupt_irq_node s irq, []) s proof (prove)
goal:
No subgoals!
theory InterruptAcc_AI

lemma get_irq_slot_cte_at[wp]:
  "\<lbrace>invs\<rbrace> get_irq_slot irq \<lbrace>cte_at\<rbrace>" apply (rule hoare_strengthen_post [OF get_irq_slot_real_cte]) apply (clarsimp simp: real_cte_at_cte) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> get_irq_slot irq \<lbrace>cte_wp_at (\<lambda>_. True)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. real_cte_at rv s \<Longrightarrow> cte_wp_at (\<lambda>_. True) rv s proof (prove)
goal:
No subgoals!
theory ArchInterruptAcc_AI

lemma dmo_maskInterrupt_invs [InterruptAcc_AI_assms]:
  "\<lbrace>all_invs_but_valid_irq_states_for irq and (\<lambda>s. state = interrupt_states s irq)\<rbrace>
   do_machine_op (maskInterrupt (state = IRQInactive) irq)
   \<lbrace>\<lambda>rv. invs\<rbrace>" apply (simp add: do_machine_op_def split_def maskInterrupt_def) apply wp apply (clarsimp simp: in_monad invs_def valid_state_def all_invs_but_valid_irq_states_for_def valid_irq_states_but_def valid_irq_masks_but_def valid_machine_state_def cur_tcb_def valid_irq_states_def valid_irq_masks_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_valid_irq_states_for irq and (\<lambda>s. state = interrupt_states s irq)\<rbrace> do_machine_op (maskInterrupt (state = IRQInactive) irq) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_valid_irq_states_for irq and (\<lambda>s. state = interrupt_states s irq)\<rbrace> do ms <- gets machine_state;
p <- select_f (modify (\<lambda>s. s\<lparr>irq_masks := (irq_masks s)(irq := state = IRQInactive)\<rparr>) ms);
modify (machine_state_update (\<lambda>_. snd p))
od \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (all_invs_but_valid_irq_states_for irq and (\<lambda>s. state = interrupt_states s irq)) s \<Longrightarrow> \<forall>x\<in>fst (modify (\<lambda>s. s\<lparr>irq_masks := (irq_masks s)(irq := state = IRQInactive)\<rparr>) (machine_state s)). invs (s\<lparr>machine_state := snd x\<rparr>) proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma default_object_tcbE:
  "\<lbrakk> default_object ty dev us = TCB tcb; ty \<noteq> Untyped;
   \<lbrakk> tcb = default_tcb; ty = Structures_A.TCBObject \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" unfolding default_object_def by (cases ty, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>default_object ty dev us = TCB tcb; ty \<noteq> Untyped; \<lbrakk>tcb = default_tcb; ty = TCBObject\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(case ty of TCBObject \<Rightarrow> TCB default_tcb | EndpointObject \<Rightarrow> Endpoint default_ep | NotificationObject \<Rightarrow> Notification default_notification | CapTableObject \<Rightarrow> CNode us (empty_cnode us) | ArchObject aobj \<Rightarrow> ArchObj (default_arch_object aobj dev us)) = TCB tcb; ty \<noteq> Untyped; \<lbrakk>tcb = default_tcb; ty = TCBObject\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
theory Retype_AI

lemma (in Retype_AI_slot_bits) obj_bits_cong:
  "\<lbrakk>a = a1; c=c1\<rbrakk> \<Longrightarrow> obj_bits (default_object a b c)
    = obj_bits (default_object a1 b1 c1)" by (simp add: default_object_def arch_kobj_size_cong
         split: if_splits apiobject_type.splits)

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

lemma (in Retype_AI_slot_bits) obj_bits_api_default_object:
  "\<lbrakk> ty \<noteq> Untyped\<rbrakk> \<Longrightarrow> obj_bits_api ty us = obj_bits (default_object ty dev us)" unfolding obj_bits_api_def default_object_def by (cases ty)
     (simp_all add: slot_bits_def2 arch_kobj_size_cong wf_empty_bits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ty \<noteq> Untyped \<Longrightarrow> obj_bits_api ty us = obj_bits (default_object ty dev us) proof (prove)
goal (1 subgoal):
 1. ty \<noteq> Untyped \<Longrightarrow> (case ty of Untyped \<Rightarrow> us | TCBObject \<Rightarrow> obj_bits (TCB default_tcb) | EndpointObject \<Rightarrow> obj_bits (Endpoint undefined) | NotificationObject \<Rightarrow> obj_bits (Notification undefined) | CapTableObject \<Rightarrow> us + slot_bits | ArchObject aobj \<Rightarrow> obj_bits $ ArchObj $ default_arch_object aobj False us) = obj_bits (case ty of TCBObject \<Rightarrow> TCB default_tcb | EndpointObject \<Rightarrow> Endpoint default_ep | NotificationObject \<Rightarrow> Notification default_notification | CapTableObject \<Rightarrow> CNode us (empty_cnode us) | ArchObject aobj \<Rightarrow> ArchObj (default_arch_object aobj dev us))
theory Retype_AI

lemma obj_bits_api_default_CapTableObject:
  "obj_bits (default_object Structures_A.apiobject_type.CapTableObject dev us)
  = cte_level_bits + us" by (simp add: default_object_def wf_empty_bits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_bits (default_object CapTableObject dev us) = cte_level_bits + us
theory Retype_AI

lemma empty_cnode_dom:
  "x \<in> dom (empty_cnode n) \<Longrightarrow> length x = n" unfolding dom_def empty_cnode_def by (simp split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> dom (empty_cnode n) \<Longrightarrow> length x = n proof (prove)
goal (1 subgoal):
 1. x \<in> {a. (if length a = n then Some NullCap else None) \<noteq> None} \<Longrightarrow> length x = n
theory Retype_AI

lemma obj_bits_api_def2:
  "obj_bits_api type obj_size_bits =
   (case type of Structures_A.Untyped \<Rightarrow> obj_size_bits
           | _ \<Rightarrow> obj_bits (default_object type False obj_size_bits))" by (simp add: obj_bits_api_def default_object_def
                wf_empty_bits dom_empty_cnode ex_with_length
                slot_bits_def2
         split: apiobject_type.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_bits_api type obj_size_bits = (case type of Untyped \<Rightarrow> obj_size_bits | _ \<Rightarrow> obj_bits (default_object type False obj_size_bits))
theory Retype_AI

lemma obj_bits_api_def3:
  "obj_bits_api type obj_size_bits =
   (if type = Structures_A.Untyped then obj_size_bits
     else obj_bits (default_object type False obj_size_bits))" by (simp add: obj_bits_api_def default_object_def
                wf_empty_bits dom_empty_cnode ex_with_length
                slot_bits_def2
         split: apiobject_type.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_bits_api type obj_size_bits = (if type = Untyped then obj_size_bits else obj_bits (default_object type False obj_size_bits))
theory Retype_AI

lemma obj_bits_api_def4:
  "obj_bits_api type obj_size_bits =
   (if type = Structures_A.Untyped then obj_size_bits
     else obj_bits (default_object type True obj_size_bits))" by (simp add: obj_bits_api_def default_object_def arch_kobj_size_cong
                wf_empty_bits dom_empty_cnode ex_with_length
                slot_bits_def2
         split: apiobject_type.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_bits_api type obj_size_bits = (if type = Untyped then obj_size_bits else obj_bits (default_object type True obj_size_bits))
theory Retype_AI

lemma obj_bits_dev_irr:
  "ty \<noteq> Untyped \<Longrightarrow> obj_bits (default_object ty dev us) = obj_bits_api ty us" by (simp add: obj_bits_api_def3 cong: obj_bits_cong)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ty \<noteq> Untyped \<Longrightarrow> obj_bits (default_object ty dev us) = obj_bits_api ty us
theory Retype_AI

lemma default_obj_range:
  "ty \<noteq> Untyped \<Longrightarrow> obj_range p (default_object ty dev us) = {p..p + 2 ^ (obj_bits_api ty us) - 1}" by (simp add: obj_range_def obj_bits_dev_irr)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ty \<noteq> Untyped \<Longrightarrow> obj_range p (default_object ty dev us) = {p..p + (2::'a) ^ obj_bits_api ty us - (1::'a)}
theory Retype_AI

lemma retype_addrs_base [simp]:
  "0 < n \<Longrightarrow> x \<in> set (retype_addrs x ty n us)" unfolding retype_addrs_def apply (simp add: ptr_add_def) apply (rule image_eqI [where x = 0]) apply simp apply (simp add: power_sub[symmetric]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> x \<in> set (retype_addrs x ty n us) proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> x \<in> set (map (\<lambda>p. ptr_add x (p * 2 ^ obj_bits_api ty us)) [0..<n]) proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> x \<in> (\<lambda>xa. x + word_of_nat xa * 2 ^ obj_bits_api ty us) ` {0..<n} proof (prove)
goal (2 subgoals):
 1. 0 < n \<Longrightarrow> x = x + word_of_nat 0 * 2 ^ obj_bits_api ty us
 2. 0 < n \<Longrightarrow> 0 \<in> {0..<n} proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> 0 \<in> {0..<n} proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma retype_addrs_aligned:
  assumes xin: "x \<in> set (retype_addrs ptr ty n us)"
  and      al: "is_aligned ptr (obj_bits_api ty us)"
  and      nv: "sz < word_bits"
  and     oav: "obj_bits_api ty us \<le> sz"
  shows   "is_aligned x (obj_bits_api ty us)" using xin unfolding retype_addrs_def ptr_add_def apply (clarsimp simp: word_unat_power [symmetric]) apply (subst mult.commute, subst shiftl_t2n [symmetric]) apply (rule aligned_add_aligned[OF al is_aligned_shift]) apply (insert assms) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned x (obj_bits_api ty us) proof (prove)
using this:
x \<in> set (retype_addrs ptr ty n us)

goal (1 subgoal):
 1. is_aligned x (obj_bits_api ty us) proof (prove)
using this:
x \<in> set (map (\<lambda>p. ptr + word_of_nat (p * 2 ^ obj_bits_api ty us)) [0..<n])

goal (1 subgoal):
 1. is_aligned x (obj_bits_api ty us) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>xa < n; x = ptr + word_of_nat xa * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> is_aligned (ptr + word_of_nat xa * 2 ^ obj_bits_api ty us) (obj_bits_api ty us) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>xa < n; x = ptr + word_of_nat xa * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> is_aligned (ptr + (word_of_nat xa << obj_bits_api ty us)) (obj_bits_api ty us) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>xa < n; x = ptr + word_of_nat xa * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> obj_bits_api ty us \<le> obj_bits_api ty us proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>xa < n; x = ptr + word_of_nat xa * 2 ^ obj_bits_api ty us; x \<in> set (retype_addrs ptr ty n us); is_aligned ptr (obj_bits_api ty us); sz < word_bits; obj_bits_api ty us \<le> sz\<rbrakk> \<Longrightarrow> obj_bits_api ty us \<le> obj_bits_api ty us proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma (in pspace_update_eq) pspace_no_overlap_update [simp]:
  "pspace_no_overlap S (f s) = pspace_no_overlap S s" by (simp add: pspace_no_overlap_def pspace)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_no_overlap S (f s) = pspace_no_overlap S s