kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchFinalCaps

lemma perform_page_directory_invocation_silc_inv:
  "perform_page_directory_invocation iv \<lbrace>silc_inv aag st\<rbrace>" unfolding perform_page_directory_invocation_def apply (cases iv) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st\<rbrace> perform_page_directory_invocation iv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st\<rbrace> case iv of PageDirectoryFlush typ start end pstart pd asid \<Rightarrow> when (start < end) $ do root_switched <- set_vm_root_for_flush pd asid;
do_machine_op $ do_flush typ start end pstart;
when root_switched $ gets cur_thread >>= set_vm_root
od | PageDirectoryNothing \<Rightarrow> return () \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16. iv = PageDirectoryFlush x11 x12 x13 x14 x15 x16 \<Longrightarrow> \<lbrace>silc_inv aag st\<rbrace> case iv of PageDirectoryFlush typ start end pstart pd asid \<Rightarrow> when (start < end) $ do root_switched <- set_vm_root_for_flush pd asid;
do_machine_op $ do_flush typ start end pstart;
when root_switched $ gets cur_thread >>= set_vm_root
od | PageDirectoryNothing \<Rightarrow> return () \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. iv = PageDirectoryNothing \<Longrightarrow> \<lbrace>silc_inv aag st\<rbrace> case iv of PageDirectoryFlush typ start end pstart pd asid \<Rightarrow> when (start < end) $ do root_switched <- set_vm_root_for_flush pd asid;
do_machine_op $ do_flush typ start end pstart;
when root_switched $ gets cur_thread >>= set_vm_root
od | PageDirectoryNothing \<Rightarrow> return () \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchFinalCaps

lemma arch_perform_invocation_silc_inv[FinalCaps_assms]:
  "\<lbrace>silc_inv aag st and invs and valid_arch_inv ai and authorised_arch_inv aag ai\<rbrace>
   arch_perform_invocation ai
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" unfolding arch_perform_invocation_def apply (rule hoare_pre) apply (wp perform_page_table_invocation_silc_inv
            perform_page_directory_invocation_silc_inv
            perform_page_invocation_silc_inv
            perform_asid_control_invocation_silc_inv
            perform_asid_pool_invocation_silc_inv
         | wpc)+ apply (clarsimp simp: authorised_arch_inv_def valid_arch_inv_def split: arch_invocation.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and invs and valid_arch_inv ai and authorised_arch_inv aag ai\<rbrace> arch_perform_invocation ai \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and invs and valid_arch_inv ai and authorised_arch_inv aag ai\<rbrace> liftE $ case ai of InvokePageTable oper \<Rightarrow> do perform_page_table_invocation oper;
return []
od | InvokePageDirectory oper \<Rightarrow> do perform_page_directory_invocation oper;
return []
od | InvokePage oper \<Rightarrow> perform_page_invocation oper | InvokeASIDControl oper \<Rightarrow> do perform_asid_control_invocation oper;
return []
od | InvokeASIDPool oper \<Rightarrow> do perform_asid_pool_invocation oper;
return []
od \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> liftE $ case ai of InvokePageTable oper \<Rightarrow> do perform_page_table_invocation oper;
return []
od | InvokePageDirectory oper \<Rightarrow> do perform_page_directory_invocation oper;
return []
od | InvokePage oper \<Rightarrow> perform_page_invocation oper | InvokeASIDControl oper \<Rightarrow> do perform_asid_control_invocation oper;
return []
od | InvokeASIDPool oper \<Rightarrow> do perform_asid_pool_invocation oper;
return []
od \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>s. (silc_inv aag st and invs and valid_arch_inv ai and authorised_arch_inv aag ai) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (silc_inv aag st and invs and valid_arch_inv ai and authorised_arch_inv aag ai) s \<Longrightarrow> (\<forall>x. ai = InvokePageTable x \<longrightarrow> (silc_inv aag st and valid_pti x and K (authorised_page_table_inv aag x)) s) \<and> (\<forall>x. ai = InvokePageDirectory x \<longrightarrow> silc_inv aag st s) \<and> (\<forall>x. ai = InvokePage x \<longrightarrow> (silc_inv aag st and valid_page_inv x and K (authorised_page_inv aag x)) s) \<and> (\<forall>x. ai = InvokeASIDControl x \<longrightarrow> (silc_inv aag st and valid_aci x and invs and K (authorised_asid_control_inv aag x)) s) \<and> (\<forall>x. ai = InvokeASIDPool x \<longrightarrow> (silc_inv aag st and K (authorised_asid_pool_inv aag x)) s) proof (prove)
goal:
No subgoals!
theory ArchFinalCaps

lemma arch_invoke_irq_control_silc_inv[FinalCaps_assms]:
  "\<lbrace>silc_inv aag st and pas_refined aag and arch_irq_control_inv_valid arch_irq_cinv
                    and K (arch_authorised_irq_ctl_inv aag arch_irq_cinv)\<rbrace>
   arch_invoke_irq_control arch_irq_cinv
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" unfolding arch_authorised_irq_ctl_inv_def apply (rule hoare_gen_asm) apply (case_tac arch_irq_cinv) apply (wp cap_insert_silc_inv'' hoare_vcg_ex_lift slots_holding_overlapping_caps_lift
         | simp add: authorised_irq_ctl_inv_def arch_irq_control_inv_valid_def)+ apply (fastforce dest: new_irq_handler_caps_are_intra_label) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and pas_refined aag and arch_irq_control_inv_valid arch_irq_cinv and K (arch_authorised_irq_ctl_inv aag arch_irq_cinv)\<rbrace> arch_invoke_irq_control arch_irq_cinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and pas_refined aag and arch_irq_control_inv_valid arch_irq_cinv and K (case arch_irq_cinv of ArchIRQControlIssue irq x1 x2 trigger \<Rightarrow> is_subject aag (fst x1) \<and> is_subject aag (fst x2) \<and> (pasSubject aag, Control, pasIRQAbs aag irq) \<in> pasPolicy aag)\<rbrace> arch_invoke_irq_control arch_irq_cinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. case arch_irq_cinv of ArchIRQControlIssue irq x1 x2 trigger \<Rightarrow> is_subject aag (fst x1) \<and> is_subject aag (fst x2) \<and> (pasSubject aag, Control, pasIRQAbs aag irq) \<in> pasPolicy aag \<Longrightarrow> \<lbrace>silc_inv aag st and pas_refined aag and arch_irq_control_inv_valid arch_irq_cinv\<rbrace> arch_invoke_irq_control arch_irq_cinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. \<lbrakk>case arch_irq_cinv of ArchIRQControlIssue irq x1 x2 trigger \<Rightarrow> is_subject aag (fst x1) \<and> is_subject aag (fst x2) \<and> (pasSubject aag, Control, pasIRQAbs aag irq) \<in> pasPolicy aag; arch_irq_cinv = ArchIRQControlIssue x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>silc_inv aag st and pas_refined aag and arch_irq_control_inv_valid arch_irq_cinv\<rbrace> arch_invoke_irq_control arch_irq_cinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 s. \<lbrakk>is_subject aag (fst x2) \<and> is_subject aag (fst x3) \<and> (pasSubject aag, Control, pasIRQAbs aag x1) \<in> pasPolicy aag; arch_irq_cinv = ArchIRQControlIssue x1 x2 x3 x4; silc_inv aag st s \<and> pas_refined aag s \<and> cte_wp_at ((=) NullCap) x2 s \<and> cte_wp_at ((=) IRQControlCap) x3 s \<and> ex_cte_cap_wp_to is_cnode_cap x2 s \<and> real_cte_at x2 s \<and> x1 \<le> maxIRQ\<rbrakk> \<Longrightarrow> \<not> cap_points_to_label aag (IRQHandlerCap x1) (pasSubject aag) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (IRQHandlerCap x1) s) \<and> pasObjectAbs aag a = SilcLabel) proof (prove)
goal:
No subgoals!
theory CNode_IF

lemma cap_fault_on_failure_rev:
  "reads_equiv_valid_inv A aag P m
   \<Longrightarrow> reads_equiv_valid_inv A aag P (cap_fault_on_failure cptr rp m)" unfolding cap_fault_on_failure_def handleE'_def by (wp | wpc | simp add: o_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag P m \<Longrightarrow> reads_equiv_valid_inv A aag P (cap_fault_on_failure cptr rp m) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag P m \<Longrightarrow> reads_equiv_valid_inv A aag P (do v <- m;
case v of Inl e \<Rightarrow> (throwError \<circ> CapFault cptr rp) e | Inr v' \<Rightarrow> return (Inr v')
od)
theory CNode_IF

lemma cap_fault_on_failure_rev_g:
  "reads_respects_g aag l P m \<Longrightarrow> reads_respects_g aag l P (cap_fault_on_failure cptr rp m)" unfolding cap_fault_on_failure_def handleE'_def by (wp | wpc | simp add: o_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_g aag l P m \<Longrightarrow> reads_respects_g aag l P (cap_fault_on_failure cptr rp m) proof (prove)
goal (1 subgoal):
 1. reads_respects_g aag l P m \<Longrightarrow> reads_respects_g aag l P (do v <- m;
case v of Inl e \<Rightarrow> (throwError \<circ> CapFault cptr rp) e | Inr v' \<Rightarrow> return (Inr v')
od)
theory CNode_IF

lemma gets_apply_ev:
  "equiv_valid I A A (K (\<forall>s t. I s t \<and> A s t \<longrightarrow> (f s) x = (f t) x)) (gets_apply f x)" apply (simp add: gets_apply_def get_def bind_def return_def) apply (clarsimp simp: equiv_valid_def2 equiv_valid_2_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A (K (\<forall>s t. I s t \<and> A s t \<longrightarrow> f s x = f t x)) (gets_apply f x) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A (\<lambda>y. \<forall>s t. I s t \<and> A s t \<longrightarrow> f s x = f t x) (\<lambda>s. ({(f s x, s)}, False)) proof (prove)
goal:
No subgoals!
theory CNode_IF

lemma gets_apply:
  "gets f >>= (\<lambda>f. g (f x)) = gets_apply f x >>= g" by (simp add: gets_apply_def gets_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do f <- gets f;
g (f x)
od = gets_apply f x >>= g
theory CNode_IF

lemma get_object_rev:
  "reads_equiv_valid_inv A aag (\<lambda>s. aag_can_read aag oref) (get_object oref)" apply (unfold get_object_def fun_app_def) apply (subst gets_apply) apply (wp gets_apply_ev | wp (once) hoare_drop_imps)+ apply (fastforce elim: reads_equivE equiv_forE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (\<lambda>s. aag_can_read aag oref) (get_object oref) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (\<lambda>s. aag_can_read aag oref) (do kh <- gets kheap;
assert (kh oref \<noteq> None);
return (the (kh oref))
od) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (\<lambda>s. aag_can_read aag oref) (do a <- gets_apply kheap oref;
assert (a \<noteq> None);
return (the a)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. aag_can_read aag oref \<Longrightarrow> K (\<forall>s t. reads_equiv aag s t \<and> A s t \<longrightarrow> kheap s oref = kheap t oref) s \<and> True \<and> True proof (prove)
goal:
No subgoals!
theory CNode_IF

lemma resolve_address_bits_rev:
  "reads_equiv_valid_inv A aag
     (pas_refined aag and K (is_cnode_cap (fst ref) \<longrightarrow> is_subject aag (obj_ref_of (fst ref))))
     (resolve_address_bits ref)" by (rule use_spec_ev[OF resolve_address_bits_spec_rev])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (pas_refined aag and K (is_cnode_cap (fst ref) \<longrightarrow> is_subject aag (obj_ref_of (fst ref)))) (resolve_address_bits ref)
theory CNode_IF

lemma lookup_cap_and_slot_rev[wp]:
  "reads_equiv_valid_inv A aag (pas_refined aag and K (is_subject aag thread))
                         (lookup_cap_and_slot thread cptr)" unfolding lookup_cap_and_slot_def by (wp lookup_slot_for_thread_rev lookup_slot_for_thread_authorised get_cap_rev
      | simp add: split_def
      | strengthen aag_can_read_self)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (pas_refined aag and K (is_subject aag thread)) (lookup_cap_and_slot thread cptr) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (pas_refined aag and K (is_subject aag thread)) (doE (slot, cr) <- lookup_slot_for_thread thread cptr;
cap <- liftE $ get_cap slot;
returnOk (cap, slot)
odE)
theory CNode_IF

lemma set_cap_reads_respects:
  "reads_respects aag l (K (aag_can_read aag (fst slot))) (set_cap cap slot)" by (wpsimp wp: set_object_reads_respects get_object_rev hoare_vcg_all_lift
           simp: set_cap_def split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (aag_can_read aag (fst slot))) (set_cap cap slot)
theory CNode_IF

lemma set_cdt_reads_respects:
  "reads_respects aag l \<top> (set_cdt c)" unfolding set_cdt_def apply (unfold equiv_valid_def2) apply (rule get_bind_ev2) apply (unfold fun_app_def, rule put_ev2) apply (fastforce intro: reads_equiv_cdt_update affects_equiv_cdt_update equiv_for_refl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (set_cdt c) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (do s <- get;
put $ s\<lparr>cdt := c\<rparr>
od) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) (\<lambda>_. True) (do s <- get;
put $ s\<lparr>cdt := c\<rparr>
od) proof (prove)
goal (1 subgoal):
 1. \<And>rv rv'. \<lbrakk>reads_equiv aag rv rv'; affects_equiv aag l rv rv'\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) ((\<lambda>_. True) and (=) rv) ((\<lambda>_. True) and (=) rv') (put $ rv\<lparr>cdt := c\<rparr>) (put $ rv'\<lparr>cdt := c\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>rv rv' s t. \<lbrakk>reads_equiv aag rv rv'; affects_equiv aag l rv rv'; reads_equiv aag s t; affects_equiv aag l s t; ((\<lambda>_. True) and (=) rv) s; ((\<lambda>_. True) and (=) rv') t\<rbrakk> \<Longrightarrow> () = () \<and> reads_equiv aag (rv\<lparr>cdt := c\<rparr>) (rv'\<lparr>cdt := c\<rparr>) \<and> affects_equiv aag l (rv\<lparr>cdt := c\<rparr>) (rv'\<lparr>cdt := c\<rparr>) proof (prove)
goal:
No subgoals!
theory CNode_IF

lemma set_cdt_ev2:
  "equiv_for (((aag_can_read aag) or (aag_can_affect aag l)) \<circ> fst) id c c'
   \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l)
                     (=) \<top> \<top> (set_cdt c) (set_cdt c')" unfolding set_cdt_def apply (rule get_bind_ev2) apply (unfold fun_app_def, rule put_ev2) apply (fastforce simp: equiv_for_or or_comp_dist reads_equiv_cdt_update affects_equiv_cdt_update) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id c c' \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>_. True) (\<lambda>_. True) (set_cdt c) (set_cdt c') proof (prove)
goal (1 subgoal):
 1. equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id c c' \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>_. True) (\<lambda>_. True) (do s <- get;
put $ s\<lparr>cdt := c\<rparr>
od) (do s <- get;
put $ s\<lparr>cdt := c'\<rparr>
od) proof (prove)
goal (1 subgoal):
 1. \<And>rv rv'. \<lbrakk>equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id c c'; reads_equiv aag rv rv'; affects_equiv aag l rv rv'\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) ((\<lambda>_. True) and (=) rv) ((\<lambda>_. True) and (=) rv') (put $ rv\<lparr>cdt := c\<rparr>) (put $ rv'\<lparr>cdt := c'\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>rv rv' s t. \<lbrakk>equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id c c'; reads_equiv aag rv rv'; affects_equiv aag l rv rv'; reads_equiv aag s t; affects_equiv aag l s t; ((\<lambda>_. True) and (=) rv) s; ((\<lambda>_. True) and (=) rv') t\<rbrakk> \<Longrightarrow> () = () \<and> reads_equiv aag (rv\<lparr>cdt := c\<rparr>) (rv'\<lparr>cdt := c'\<rparr>) \<and> affects_equiv aag l (rv\<lparr>cdt := c\<rparr>) (rv'\<lparr>cdt := c'\<rparr>) proof (prove)
goal:
No subgoals!
theory CNode_IF

lemma set_cdt_list_ev2:
  "equiv_for (((aag_can_read aag) or (aag_can_affect aag l)) \<circ> fst) id c c'
   \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l)
                     (=) \<top> \<top> (set_cdt_list c) (set_cdt_list c')" unfolding set_cdt_list_def apply (rule get_bind_ev2) apply (unfold fun_app_def, rule put_ev2) apply (fastforce simp: equiv_for_or or_comp_dist reads_equiv_cdt_list_update affects_equiv_cdt_list_update) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id c c' \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>_. True) (\<lambda>_. True) (set_cdt_list c) (set_cdt_list c') proof (prove)
goal (1 subgoal):
 1. equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id c c' \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>_. True) (\<lambda>_. True) (do s <- get;
put $ cdt_list_update (\<lambda>_. c) s
od) (do s <- get;
put $ cdt_list_update (\<lambda>_. c') s
od) proof (prove)
goal (1 subgoal):
 1. \<And>rv rv'. \<lbrakk>equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id c c'; reads_equiv aag rv rv'; affects_equiv aag l rv rv'\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) ((\<lambda>_. True) and (=) rv) ((\<lambda>_. True) and (=) rv') (put $ cdt_list_update (\<lambda>_. c) rv) (put $ cdt_list_update (\<lambda>_. c') rv') proof (prove)
goal (1 subgoal):
 1. \<And>rv rv' s t. \<lbrakk>equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id c c'; reads_equiv aag rv rv'; affects_equiv aag l rv rv'; reads_equiv aag s t; affects_equiv aag l s t; ((\<lambda>_. True) and (=) rv) s; ((\<lambda>_. True) and (=) rv') t\<rbrakk> \<Longrightarrow> () = () \<and> reads_equiv aag (cdt_list_update (\<lambda>_. c) rv) (cdt_list_update (\<lambda>_. c') rv') \<and> affects_equiv aag l (cdt_list_update (\<lambda>_. c) rv) (cdt_list_update (\<lambda>_. c') rv') proof (prove)
goal:
No subgoals!
theory CNode_IF

lemma kheap_get_tcb_eq: "kheap s ref = kheap t ref \<Longrightarrow> get_tcb ref s = get_tcb ref t" by (simp add: get_tcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. kheap s ref = kheap t ref \<Longrightarrow> get_tcb ref s = get_tcb ref t
theory CNode_IF

lemma gen_asm_ev2':
  assumes "Q \<Longrightarrow> Q' \<Longrightarrow> equiv_valid_2 I A B R P P' f f'"
  shows "equiv_valid_2 I A B R (P and K Q) (P' and K Q') f f'" using assms by (fastforce simp: equiv_valid_def2 equiv_valid_2_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 I A B R (P and K Q) (P' and K Q') f f' proof (prove)
using this:
\<lbrakk>Q; Q'\<rbrakk> \<Longrightarrow> equiv_valid_2 I A B R P P' f f'

goal (1 subgoal):
 1. equiv_valid_2 I A B R (P and K Q) (P' and K Q') f f'
theory CNode_IF

lemma set_untyped_cap_as_full_reads_respects:
  "reads_respects aag l (K (aag_can_read aag (fst src_slot)))
     (set_untyped_cap_as_full src_cap new_cap src_slot)" unfolding set_untyped_cap_as_full_def apply (wp set_cap_reads_respects) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (aag_can_read aag (fst src_slot))) (set_untyped_cap_as_full src_cap new_cap src_slot) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (aag_can_read aag (fst src_slot))) (if is_untyped_cap src_cap \<and> is_untyped_cap new_cap \<and> obj_ref_of src_cap = obj_ref_of new_cap \<and> cap_bits_untyped src_cap = cap_bits_untyped new_cap then set_cap (max_free_index_update src_cap) src_slot else return ()) proof (prove)
goal (1 subgoal):
 1. \<And>s. K (aag_can_read aag (fst src_slot)) s \<Longrightarrow> (is_untyped_cap src_cap \<and> is_untyped_cap new_cap \<and> obj_ref_of src_cap = obj_ref_of new_cap \<and> cap_bits_untyped src_cap = cap_bits_untyped new_cap \<longrightarrow> K (aag_can_read aag (fst src_slot)) s) \<and> (\<not> (is_untyped_cap src_cap \<and> is_untyped_cap new_cap \<and> obj_ref_of src_cap = obj_ref_of new_cap \<and> cap_bits_untyped src_cap = cap_bits_untyped new_cap) \<longrightarrow> True) proof (prove)
goal:
No subgoals!
theory CNode_IF

lemma gets_apply_wp[wp]:
  "\<lbrace>\<lambda>s. P (f s x) s\<rbrace> gets_apply f x \<lbrace>P\<rbrace>" by (wpsimp simp: gets_apply_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (f s x) s\<rbrace> gets_apply f x \<lbrace>P\<rbrace>
theory CNode_IF

lemma get_idemp:
  "do s1 \<leftarrow> get; s2 \<leftarrow> get; f s1 s2 od =
   do s1 \<leftarrow> get; f s1 s1 od" by (simp add: get_def bind_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do s1 <- get;
get >>= f s1
od = do s1 <- get;
f s1 s1
od
theory CNode_IF

lemma gets_apply2:
  "gets f >>= (\<lambda> f. g (f x) (f y)) =
   gets_apply f x >>= (\<lambda> x. gets_apply f y >>= (\<lambda> y. g x y))" by (simp add: gets_def gets_apply_def get_idemp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do f <- gets f;
g (f x) (f y)
od = do x <- gets_apply f x;
gets_apply f y >>= g x
od
theory CNode_IF

lemma tcb_at_def2: "tcb_at ptr s = (\<exists>tcb. kheap s ptr = Some (TCB tcb))" by (clarsimp simp: tcb_at_def get_tcb_def split: kernel_object.splits option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_at ptr s = (\<exists>tcb. kheap s ptr = Some (TCB tcb))
theory CNode_IF

lemma set_cdt_globals_equiv:
  "set_cdt c \<lbrace>globals_equiv s\<rbrace>" unfolding set_cdt_def by (wpsimp simp: globals_equiv_def idle_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> set_cdt c \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> do s <- get;
put $ s\<lparr>cdt := c\<rparr>
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
theory CNode_IF

lemma update_cdt_globals_equiv:
  "update_cdt f \<lbrace>globals_equiv s\<rbrace>" unfolding update_cdt_def by (wp set_cdt_globals_equiv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> update_cdt f \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> do t <- gets cdt;
set_cdt (f t)
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
theory CNode_IF

lemma set_original_globals_equiv:
  "set_original slot v \<lbrace>globals_equiv s\<rbrace>" unfolding set_original_def by (wpsimp simp: globals_equiv_def idle_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> set_original slot v \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> do r <- gets is_original_cap;
modify (is_original_cap_update (\<lambda>_. r(slot := v)))
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
theory CNode_IF

lemma globals_equiv_exst_update[simp]:
  "globals_equiv st (trans_state f s) =
   globals_equiv st s" by (simp add: globals_equiv_def idle_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. globals_equiv st (trans_state f s) = globals_equiv st s
theory CNode_IF

lemma (in is_extended') globals_equiv: "I (globals_equiv st)" by (rule lift_inv,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st\<rbrace> f \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
theory CNode_IF

lemma domain_sep_inv_refl:
  "domain_sep_inv irqs st s \<Longrightarrow> domain_sep_inv irqs s s" by (fastforce simp: domain_sep_inv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. domain_sep_inv irqs st s \<Longrightarrow> domain_sep_inv irqs s s