kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchCSpace_AI

lemma getActiveIRQ_wp [CSpace_AI_assms]:
  "irq_state_independent_A P \<Longrightarrow>
   valid P (do_machine_op (getActiveIRQ in_kernel)) (\<lambda>_. P)" apply (simp add: getActiveIRQ_def do_machine_op_def split_def exec_gets
                   select_f_select[simplified liftM_def]
                   select_modify_comm gets_machine_state_modify) apply wp apply (clarsimp simp: irq_state_independent_A_def in_monad return_def split: if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. irq_state_independent_A P \<Longrightarrow> \<lbrace>P\<rbrace> do_machine_op (getActiveIRQ in_kernel) \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. irq_state_independent_A P \<Longrightarrow> \<lbrace>P\<rbrace> do ms <- gets machine_state;
p <- select_f ((do y <- modify (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>);
active_irq <- gets (irq_oracle \<circ> irq_state);
if irq_masks ms active_irq \<or> active_irq = 0x3FF \<or> in_kernel \<and> active_irq \<in> non_kernel_IRQs then return None else return (Some active_irq)
od) ms);
y <- modify (machine_state_update (\<lambda>_. snd p));
return (fst p)
od \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>irq_state_independent_A P; P s\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst ((do y <- modify (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>);
active_irq <- gets (irq_oracle \<circ> irq_state);
if irq_masks (machine_state s) active_irq \<or> active_irq = 0x3FF \<or> in_kernel \<and> active_irq \<in> non_kernel_IRQs then return None else return (Some active_irq)
od) (machine_state s)). P (s\<lparr>machine_state := snd x\<rparr>) proof (prove)
goal:
No subgoals!
theory ArchCSpace_AI

lemma weak_derived_valid_cap [CSpace_AI_assms]:
  "\<lbrakk> s \<turnstile> c; wellformed_cap c'; weak_derived c' c\<rbrakk> \<Longrightarrow> s \<turnstile> c'" apply (case_tac "c = c'", simp) apply (clarsimp simp: weak_derived_def) apply (clarsimp simp: copy_of_def split: if_split_asm) apply (auto simp: is_cap_simps same_object_as_def wellformed_cap_simps
                    valid_cap_def cap_aligned_def bits_of_def
                    aobj_ref_cases Let_def cap_asid_def
             split: cap.splits arch_cap.splits option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> c; wellformed_cap c'; weak_derived c' c\<rbrakk> \<Longrightarrow> s \<turnstile> c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> c; wellformed_cap c'; weak_derived c' c; c \<noteq> c'\<rbrakk> \<Longrightarrow> s \<turnstile> c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> c; wellformed_cap c'; c \<noteq> c'; copy_of c' c; cap_asid c' = cap_asid c; cap_asid_base c' = cap_asid_base c; cap_vptr c' = cap_vptr c\<rbrakk> \<Longrightarrow> s \<turnstile> c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_asid c' = cap_asid c; cap_asid_base c' = cap_asid_base c; cap_vptr c' = cap_vptr c; s \<turnstile> c; wellformed_cap c'; c \<noteq> c'; \<not> is_untyped_cap c; same_object_as c c'; is_reply_cap c = is_reply_cap c'; is_master_reply_cap c = is_master_reply_cap c'\<rbrakk> \<Longrightarrow> s \<turnstile> c' proof (prove)
goal:
No subgoals!
theory ArchCSpace_AI

lemma copy_obj_refs [CSpace_AI_assms]:
  "copy_of cap cap' \<Longrightarrow> obj_refs cap' = obj_refs cap" apply (cases cap) apply (auto simp: copy_of_def same_object_as_def is_cap_simps
                    aobj_ref_cases
             split: if_split_asm cap.splits arch_cap.splits) done

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

lemma weak_derived_cap_class[simp, CSpace_AI_assms]:
  "weak_derived cap src_cap \<Longrightarrow> cap_class cap = cap_class src_cap" apply (simp add:weak_derived_def) apply (auto simp:copy_of_def same_object_as_def is_cap_simps cap_asid_base_def
    split:if_splits cap.splits arch_cap.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_derived cap src_cap \<Longrightarrow> cap_class cap = cap_class src_cap proof (prove)
goal (1 subgoal):
 1. copy_of cap src_cap \<and> cap_asid cap = cap_asid src_cap \<and> cap_asid_base cap = cap_asid_base src_cap \<and> cap_vptr cap = cap_vptr src_cap \<or> src_cap = cap \<Longrightarrow> cap_class cap = cap_class src_cap proof (prove)
goal:
No subgoals!
theory ArchCSpace_AI

lemma weak_derived_obj_ref_of [CSpace_AI_assms]:
  "weak_derived dcap cap \<Longrightarrow> obj_ref_of dcap = obj_ref_of cap" by (cases dcap, auto simp: is_cap_simps weak_derived_def copy_of_def
                             same_object_as_def aobj_ref_cases
                       split: if_split_asm cap.splits arch_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_derived dcap cap \<Longrightarrow> obj_ref_of dcap = obj_ref_of cap
theory ArchCSpace_AI

lemma unique_table_refs_upd_eqD:
  "\<lbrakk>ms a = Some b; obj_refs b = obj_refs b'; table_cap_ref b = table_cap_ref b'\<rbrakk>
   \<Longrightarrow> unique_table_refs (ms (a \<mapsto> b')) = unique_table_refs ms" unfolding unique_table_refs_def 
  (* match up p and p' on both sides of equality *)
   apply (rule all_cong[where Q=\<top>, simplified]) apply (rule all_cong[where Q=\<top>, simplified]) by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ms a = Some b; obj_refs b = obj_refs b'; table_cap_ref b = table_cap_ref b'\<rbrakk> \<Longrightarrow> unique_table_refs (ms(a \<mapsto> b')) = unique_table_refs ms proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ms a = Some b; obj_refs b = obj_refs b'; table_cap_ref b = table_cap_ref b'\<rbrakk> \<Longrightarrow> (\<forall>p p' cap cap'. (ms(a \<mapsto> b')) p = Some cap \<longrightarrow> (ms(a \<mapsto> b')) p' = Some cap' \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> table_cap_ref cap' = table_cap_ref cap) = (\<forall>p p' cap cap'. ms p = Some cap \<longrightarrow> ms p' = Some cap' \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> table_cap_ref cap' = table_cap_ref cap) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ms a = Some b; obj_refs b = obj_refs b'; table_cap_ref b = table_cap_ref b'\<rbrakk> \<Longrightarrow> (\<forall>p p' cap cap'. (ms(a \<mapsto> b')) p = Some cap \<longrightarrow> (ms(a \<mapsto> b')) p' = Some cap' \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> table_cap_ref cap' = table_cap_ref cap) = (\<forall>p p' cap cap'. ms p = Some cap \<longrightarrow> ms p' = Some cap' \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> table_cap_ref cap' = table_cap_ref cap) proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>ms a = Some b; obj_refs b = obj_refs b'; table_cap_ref b = table_cap_ref b'\<rbrakk> \<Longrightarrow> (\<forall>p' cap cap'. (ms(a \<mapsto> b')) p = Some cap \<longrightarrow> (ms(a \<mapsto> b')) p' = Some cap' \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> table_cap_ref cap' = table_cap_ref cap) = (\<forall>p' cap cap'. ms p = Some cap \<longrightarrow> ms p' = Some cap' \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> table_cap_ref cap' = table_cap_ref cap) proof (prove)
goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>ms a = Some b; obj_refs b = obj_refs b'; table_cap_ref b = table_cap_ref b'\<rbrakk> \<Longrightarrow> (\<forall>cap cap'. (ms(a \<mapsto> b')) p = Some cap \<longrightarrow> (ms(a \<mapsto> b')) p' = Some cap' \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> table_cap_ref cap' = table_cap_ref cap) = (\<forall>cap cap'. ms p = Some cap \<longrightarrow> ms p' = Some cap' \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> table_cap_ref cap' = table_cap_ref cap)
theory ArchCSpace_AI

lemma set_untyped_cap_as_full[wp, CSpace_AI_assms]:
  "\<lbrace>\<lambda>s. no_cap_to_obj_with_diff_ref a b s \<and> cte_wp_at ((=) src_cap) src s\<rbrace>
   set_untyped_cap_as_full src_cap cap src
   \<lbrace>\<lambda>rv s. no_cap_to_obj_with_diff_ref a b s\<rbrace>" apply (clarsimp simp:no_cap_to_obj_with_diff_ref_def) apply (wp hoare_vcg_ball_lift set_untyped_cap_as_full_cte_wp_at_neg) apply (clarsimp simp:cte_wp_at_caps_of_state) apply (drule_tac x=src in bspec, simp) apply (erule_tac x=src_cap in allE) apply (auto simp: table_cap_ref_def masked_as_full_def
             split: Structures_A.cap.splits arch_cap.splits option.splits
                    vmpage_size.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_cap_to_obj_with_diff_ref a b s \<and> cte_wp_at ((=) src_cap) src s\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>rv. no_cap_to_obj_with_diff_ref a b\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>p\<in>UNIV - b. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs a \<and> table_cap_ref c \<noteq> table_cap_ref a) p s) \<and> cte_wp_at ((=) src_cap) src s\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>rv s. \<forall>p\<in>UNIV - b. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs a \<and> table_cap_ref c \<noteq> table_cap_ref a) p s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>p\<in>UNIV - b. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs a \<and> table_cap_ref c \<noteq> table_cap_ref a) p s) \<and> cte_wp_at ((=) src_cap) src s \<Longrightarrow> \<forall>x\<in>UNIV - b. (x \<noteq> src \<and> \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs a \<and> table_cap_ref c \<noteq> table_cap_ref a) x s \<or> x = src \<and> \<not> cte_wp_at (\<lambda>aa. obj_refs (masked_as_full aa cap) = obj_refs a \<and> table_cap_ref (masked_as_full aa cap) \<noteq> table_cap_ref a) src s) \<and> cte_wp_at ((=) src_cap) src s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>p\<in>UNIV - b. \<forall>cap. obj_refs cap = obj_refs a \<longrightarrow> caps_of_state s p = Some cap \<longrightarrow> table_cap_ref cap = table_cap_ref a; caps_of_state s src = Some src_cap; src \<notin> b; obj_refs src_cap = obj_refs a\<rbrakk> \<Longrightarrow> table_cap_ref (masked_as_full src_cap cap) = table_cap_ref a proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>caps_of_state s src = Some src_cap; src \<notin> b; obj_refs src_cap = obj_refs a; \<forall>cap. obj_refs cap = obj_refs a \<longrightarrow> caps_of_state s src = Some cap \<longrightarrow> table_cap_ref cap = table_cap_ref a\<rbrakk> \<Longrightarrow> table_cap_ref (masked_as_full src_cap cap) = table_cap_ref a proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>caps_of_state s src = Some src_cap; src \<notin> b; obj_refs src_cap = obj_refs a; obj_refs src_cap = obj_refs a \<longrightarrow> caps_of_state s src = Some src_cap \<longrightarrow> table_cap_ref src_cap = table_cap_ref a\<rbrakk> \<Longrightarrow> table_cap_ref (masked_as_full src_cap cap) = table_cap_ref a proof (prove)
goal:
No subgoals!
theory ArchCSpace_AI

lemma vs_lookup_pages1_tcb_update:
  "kheap s p = Some (TCB t) \<Longrightarrow>
   vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB t')\<rparr>) = vs_lookup_pages1 s" by (clarsimp simp: vs_lookup_pages1_def obj_at_def vs_refs_pages_def
             intro!: set_eqI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. kheap s p = Some (TCB t) \<Longrightarrow> vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB t')\<rparr>) = vs_lookup_pages1 s
theory ArchCSpace_AI

lemma vs_lookup_pages_tcb_update:
  "kheap s p = Some (TCB t) \<Longrightarrow>
   vs_lookup_pages (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB t')\<rparr>) = vs_lookup_pages s" by (clarsimp simp add: vs_lookup_pages_def vs_lookup_pages1_tcb_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. kheap s p = Some (TCB t) \<Longrightarrow> vs_lookup_pages (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB t')\<rparr>) = vs_lookup_pages s
theory ArchCSpace_AI

lemma vs_lookup_pages1_cnode_update:
  "kheap s p = Some (CNode n cs) \<Longrightarrow>
   vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> CNode m cs')\<rparr>) =
   vs_lookup_pages1 s" by (clarsimp simp: vs_lookup_pages1_def obj_at_def vs_refs_pages_def
             intro!: set_eqI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. kheap s p = Some (CNode n cs) \<Longrightarrow> vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> CNode m cs')\<rparr>) = vs_lookup_pages1 s
theory ArchCSpace_AI

lemma vs_lookup_pages_cnode_update:
  "kheap s p = Some (CNode n cs) \<Longrightarrow>
   vs_lookup_pages (s\<lparr>kheap := (kheap s)(p \<mapsto> CNode n cs')\<rparr>) = vs_lookup_pages s" by (clarsimp simp: vs_lookup_pages_def
              dest!: vs_lookup_pages1_cnode_update[where m=n and cs'=cs'])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. kheap s p = Some (CNode n cs) \<Longrightarrow> vs_lookup_pages (s\<lparr>kheap := (kheap s)(p \<mapsto> CNode n cs')\<rparr>) = vs_lookup_pages s
theory ArchCSpace_AI

lemma is_derived_is_pt_pd:
  "is_derived m p cap cap' \<Longrightarrow> (is_pt_cap cap = is_pt_cap cap') \<and> (is_pd_cap cap = is_pd_cap cap')" apply (clarsimp simp: is_derived_def split: if_split_asm) apply (clarsimp simp: cap_master_cap_def is_pt_cap_def is_pd_cap_def
    split: cap.splits arch_cap.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_derived m p cap cap' \<Longrightarrow> is_pt_cap cap = is_pt_cap cap' \<and> is_pd_cap cap = is_pd_cap cap' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_untyped_cap cap'; cap \<noteq> NullCap; \<not> is_zombie cap'; cap \<noteq> IRQControlCap; cap_master_cap cap' = cap_master_cap cap; descendants_of p m = {}; is_master_reply_cap cap' = is_reply_cap cap; is_derived_arch cap cap'; \<not> is_reply_cap cap'; \<not> is_master_reply_cap cap\<rbrakk> \<Longrightarrow> is_pt_cap cap = is_pt_cap cap' \<and> is_pd_cap cap = is_pd_cap cap'
 2. \<lbrakk>\<not> is_untyped_cap cap'; cap \<noteq> NullCap; \<not> is_zombie cap'; cap \<noteq> IRQControlCap; cap_master_cap cap' = cap_master_cap cap; (cap_badge cap', cap_badge cap) \<in> capBadge_ordering False; is_master_reply_cap cap' = is_reply_cap cap; is_derived_arch cap cap'; \<not> is_reply_cap cap'; \<not> is_master_reply_cap cap\<rbrakk> \<Longrightarrow> is_pt_cap cap = is_pt_cap cap' \<and> is_pd_cap cap = is_pd_cap cap' proof (prove)
goal:
No subgoals!
theory ArchCSpace_AI

lemma mask_cap_objrefs[simp, CSpace_AI_assms]:
  "obj_refs (mask_cap rs cap) = obj_refs cap" by (cases cap, simp_all add: mask_cap_def cap_rights_update_def
                               acap_rights_update_def
                        split: arch_cap.split bool.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_refs (mask_cap rs cap) = obj_refs cap
theory ArchCSpace_AI

lemma mask_cap_zobjrefs[simp, CSpace_AI_assms]:
  "zobj_refs (mask_cap rs cap) = zobj_refs cap" by (cases cap, simp_all add: mask_cap_def cap_rights_update_def
                               acap_rights_update_def
                        split: arch_cap.split bool.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. zobj_refs (mask_cap rs cap) = zobj_refs cap
theory ArchCSpace_AI

lemma derive_cap_valid_cap [CSpace_AI_assms]:
  "\<lbrace>valid_cap cap\<rbrace> derive_cap slot cap \<lbrace>valid_cap\<rbrace>,-" apply (simp add: derive_cap_def) apply (rule hoare_pre) apply (wpc, (wp arch_derive_cap_valid_cap | simp)+) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap cap\<rbrace> derive_cap slot cap \<lbrace>valid_cap\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap cap\<rbrace> case cap of UntypedCap dev ptr sz f \<Rightarrow> doE ensure_no_children slot;
returnOk cap
odE | ReplyCap ptr m cr \<Rightarrow> returnOk NullCap | IRQControlCap \<Rightarrow> returnOk NullCap | Zombie ptr n sz \<Rightarrow> returnOk NullCap | ArchObjectCap c \<Rightarrow> arch_derive_cap c | _ \<Rightarrow> returnOk cap \<lbrace>valid_cap\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> case cap of UntypedCap dev ptr sz f \<Rightarrow> doE ensure_no_children slot;
returnOk cap
odE | ReplyCap ptr m cr \<Rightarrow> returnOk NullCap | IRQControlCap \<Rightarrow> returnOk NullCap | Zombie ptr n sz \<Rightarrow> returnOk NullCap | ArchObjectCap c \<Rightarrow> arch_derive_cap c | _ \<Rightarrow> returnOk cap \<lbrace>valid_cap\<rbrace>, -
 2. \<And>s. s \<turnstile> cap \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<turnstile> cap \<Longrightarrow> (\<forall>x xa xb xc. cap = UntypedCap x xa xb xc \<longrightarrow> s \<turnstile> UntypedCap x xa xb xc) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> s \<turnstile> EndpointCap x xa xb) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> s \<turnstile> NotificationCap x xa xb) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> s \<turnstile> CNodeCap x xa xb) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> s \<turnstile> ThreadCap x) \<and> (cap = DomainCap \<longrightarrow> s \<turnstile> DomainCap) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> s \<turnstile> IRQHandlerCap x) \<and> (\<forall>x. cap = ArchObjectCap x \<longrightarrow> s \<turnstile> ArchObjectCap x) proof (prove)
goal:
No subgoals!
theory ArchCSpace_AI

lemma tcb_cnode_index_def2 [CSpace_AI_assms]:
  "tcb_cnode_index n = nat_to_cref 3 n" apply (simp add: tcb_cnode_index_def nat_to_cref_def) apply (rule nth_equalityI) apply (simp add: word_bits_def) apply (clarsimp simp: to_bl_nth word_size word_bits_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_cnode_index n = nat_to_cref 3 n proof (prove)
goal (1 subgoal):
 1. to_bl (word_of_nat n) = drop (word_bits - 3) (to_bl (word_of_nat n)) proof (prove)
goal (2 subgoals):
 1. length (to_bl (word_of_nat n)) = length (drop (word_bits - 3) (to_bl (word_of_nat n)))
 2. \<And>i. i < length (to_bl (word_of_nat n)) \<Longrightarrow> to_bl (word_of_nat n) ! i = drop (word_bits - 3) (to_bl (word_of_nat n)) ! i proof (prove)
goal (1 subgoal):
 1. \<And>i. i < length (to_bl (word_of_nat n)) \<Longrightarrow> to_bl (word_of_nat n) ! i = drop (word_bits - 3) (to_bl (word_of_nat n)) ! i proof (prove)
goal (1 subgoal):
 1. \<And>i. i < 3 \<Longrightarrow> (2 - i < 3 \<and> n !! (2 - i)) = (2 - i < 32 \<and> n !! (2 - i)) proof (prove)
goal:
No subgoals!
theory ArchCSpace_AI

lemma ex_nonz_tcb_cte_caps [CSpace_AI_assms]:
  "\<lbrakk>ex_nonz_cap_to t s; tcb_at t s; valid_objs s; ref \<in> dom tcb_cap_cases\<rbrakk>
   \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cp) (t, ref) s" apply (clarsimp simp: ex_nonz_cap_to_def ex_cte_cap_wp_to_def
                        cte_wp_at_caps_of_state) apply (subgoal_tac "s \<turnstile> cap") apply (rule_tac x=a in exI, rule_tac x=ba in exI) apply (clarsimp simp: valid_cap_def obj_at_def
                         is_obj_defs dom_def
                         appropriate_cte_cap_def
                  split: cap.splits arch_cap.split_asm if_splits) apply (clarsimp simp: caps_of_state_valid_cap) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ex_nonz_cap_to t s; tcb_at t s; valid_objs s; ref \<in> dom tcb_cap_cases\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cp) (t, ref) s proof (prove)
goal (1 subgoal):
 1. \<And>a aa ab b ba cap. \<lbrakk>tcb_at t s; valid_objs s; tcb_cap_cases ref = Some (aa, ab, b); caps_of_state s (a, ba) = Some cap; t \<in> zobj_refs cap\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> appropriate_cte_cap cp cap \<and> (t, ref) \<in> cte_refs cap (interrupt_irq_node s) proof (prove)
goal (2 subgoals):
 1. \<And>a aa ab b ba cap. \<lbrakk>tcb_at t s; valid_objs s; tcb_cap_cases ref = Some (aa, ab, b); caps_of_state s (a, ba) = Some cap; t \<in> zobj_refs cap; s \<turnstile> cap\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> appropriate_cte_cap cp cap \<and> (t, ref) \<in> cte_refs cap (interrupt_irq_node s)
 2. \<And>a aa ab b ba cap. \<lbrakk>tcb_at t s; valid_objs s; tcb_cap_cases ref = Some (aa, ab, b); caps_of_state s (a, ba) = Some cap; t \<in> zobj_refs cap\<rbrakk> \<Longrightarrow> s \<turnstile> cap proof (prove)
goal (2 subgoals):
 1. \<And>a aa ab b ba cap. \<lbrakk>tcb_at t s; valid_objs s; tcb_cap_cases ref = Some (aa, ab, b); caps_of_state s (a, ba) = Some cap; t \<in> zobj_refs cap; s \<turnstile> cap\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state s (a, ba) = Some cap \<and> appropriate_cte_cap cp cap \<and> (t, ref) \<in> cte_refs cap (interrupt_irq_node s)
 2. \<And>a aa ab b ba cap. \<lbrakk>tcb_at t s; valid_objs s; tcb_cap_cases ref = Some (aa, ab, b); caps_of_state s (a, ba) = Some cap; t \<in> zobj_refs cap\<rbrakk> \<Longrightarrow> s \<turnstile> cap proof (prove)
goal (1 subgoal):
 1. \<And>a aa ab b ba cap. \<lbrakk>tcb_at t s; valid_objs s; tcb_cap_cases ref = Some (aa, ab, b); caps_of_state s (a, ba) = Some cap; t \<in> zobj_refs cap\<rbrakk> \<Longrightarrow> s \<turnstile> cap proof (prove)
goal:
No subgoals!
theory ArchCSpace_AI

lemma no_cap_to_obj_with_diff_ref_triv:
  "\<lbrakk> valid_objs s; valid_cap cap s; \<not> is_pt_cap cap;
           \<not> is_pd_cap cap; table_cap_ref cap = None \<rbrakk>
      \<Longrightarrow> no_cap_to_obj_with_diff_ref cap S s" apply (clarsimp simp add: no_cap_to_obj_with_diff_ref_def) apply (drule(1) cte_wp_at_valid_objs_valid_cap) apply (clarsimp simp: table_cap_ref_def valid_cap_def
                        obj_at_def is_ep is_ntfn is_tcb is_cap_table
                        a_type_def is_cap_simps
                 split: cap.split_asm arch_cap.split_asm
                        if_split_asm option.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; s \<turnstile> cap; \<not> is_pt_cap cap; \<not> is_pd_cap cap; table_cap_ref cap = None\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref cap S s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>valid_objs s; s \<turnstile> cap; \<not> is_pt_cap cap; \<not> is_pd_cap cap; table_cap_ref cap = None; (a, b) \<notin> S; cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> (\<exists>y. table_cap_ref c = Some y)) (a, b) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>valid_objs s; s \<turnstile> cap; \<not> is_pt_cap cap; \<not> is_pd_cap cap; table_cap_ref cap = None; (a, b) \<notin> S; \<exists>capa. (obj_refs capa = obj_refs cap \<and> (\<exists>y. table_cap_ref capa = Some y)) \<and> s \<turnstile> capa\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!