kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchInterrupt_AC

lemma arch_invoke_irq_handler_pas_refined[Interrupt_AC_assms]:
  "\<lbrace>pas_refined aag and invs and (\<lambda>s. interrupt_states s x1 \<noteq> IRQInactive)\<rbrace>
   arch_invoke_irq_handler (ACKIrq x1)
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and invs and (\<lambda>s. interrupt_states s x1 \<noteq> IRQInactive)\<rbrace> arch_invoke_irq_handler (ACKIrq x1) \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
theory ArchInterrupt_AC

lemma arch_invoke_irq_control_respects[Interrupt_AC_assms]:
  "\<lbrace>integrity aag X st and pas_refined aag and K (arch_authorised_irq_ctl_inv aag acinv)\<rbrace>
   arch_invoke_irq_control acinv
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (case_tac acinv, clarsimp simp add: setIRQTrigger_def arch_authorised_irq_ctl_inv_def) apply (wpsimp wp: cap_insert_integrity_autarch aag_Control_into_owns_irq
                    dmo_mol_respects do_machine_op_pas_refined) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and K (arch_authorised_irq_ctl_inv aag acinv)\<rbrace> arch_invoke_irq_control acinv \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 a b aa ba x4. acinv = ArchIRQControlIssue x1 (a, b) (aa, ba) x4 \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and (\<lambda>y. is_subject aag a \<and> is_subject aag aa \<and> (pasSubject aag, Control, pasIRQAbs aag x1) \<in> pasPolicy aag)\<rbrace> liftE (do y <- do_machine_op (machine_op_lift (setIRQTrigger_impl x1 x4));
y <- set_irq_state IRQSignal x1;
cap_insert (IRQHandlerCap x1) (aa, ba) (a, b)
od) \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchInterrupt_AC

lemma arch_invoke_irq_handler_respects[Interrupt_AC_assms]:
  "\<lbrace>integrity aag X st and pas_refined aag and einvs\<rbrace>
   arch_invoke_irq_handler (ACKIrq x1)
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" by (wpsimp wp: dmo_wp simp: maskInterrupt_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and einvs\<rbrace> arch_invoke_irq_handler (ACKIrq x1) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
theory DomainSepInv

lemma domain_sep_inv_def2:
  "domain_sep_inv irqs st s =
    ((\<forall>slot. \<not> cte_wp_at ((=) DomainCap) slot s) \<and>
     (irqs \<or> (\<forall>irq slot. \<not> cte_wp_at ((=) IRQControlCap) slot s
                       \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) slot s)) \<and>
     (irqs \<or> (\<forall>irq. interrupt_states s irq \<noteq> IRQSignal
                  \<and> interrupt_states s irq \<noteq> IRQReserved
                  \<and> interrupt_states s = interrupt_states st)))" by (fastforce simp: domain_sep_inv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. domain_sep_inv irqs st s = ((\<forall>slot. \<not> cte_wp_at ((=) DomainCap) slot s) \<and> (irqs \<or> (\<forall>irq slot. \<not> cte_wp_at ((=) IRQControlCap) slot s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) slot s)) \<and> (irqs \<or> (\<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st)))
theory DomainSepInv

lemma domain_sep_inv_triv:
  assumes cte_pres: "\<And>P slot. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> f \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace>"
  assumes irq_pres: "\<And>P. \<lbrace>\<lambda>s. P (interrupt_states s)\<rbrace> f \<lbrace>\<lambda>_ s. P (interrupt_states s)\<rbrace>"
  shows "\<lbrace>domain_sep_inv irqs st\<rbrace> f \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" apply (rule domain_sep_inv_wp[where P="\<top>" and R="\<top>", simplified]) apply (rule cte_pres, rule irq_pres) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st\<rbrace> f \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>slot. \<lbrace>\<lambda>s. \<not> cte_wp_at (not domain_sep_inv_cap irqs) slot s\<rbrace> f \<lbrace>\<lambda>_ s. \<not> cte_wp_at (not domain_sep_inv_cap irqs) slot s\<rbrace>
 2. \<And>P. \<not> irqs \<Longrightarrow> \<lbrace>\<lambda>s. P (interrupt_states s)\<rbrace> f \<lbrace>\<lambda>_ s. P (interrupt_states s)\<rbrace> proof (prove)
goal:
No subgoals!
theory DomainSepInv

lemma domain_sep_inv_arch_state_update[simp]:
  "domain_sep_inv irqs st (s\<lparr>arch_state := blah\<rparr>) = domain_sep_inv irqs st s" by (simp add: domain_sep_inv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. domain_sep_inv irqs st (s\<lparr>arch_state := blah\<rparr>) = domain_sep_inv irqs st s
theory DomainSepInv

lemma domain_sep_inv_machine_state_update[simp]:
  "domain_sep_inv irqs st (s\<lparr>machine_state := X\<rparr>) = domain_sep_inv irqs st s" by (simp add: domain_sep_inv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. domain_sep_inv irqs st (s\<lparr>machine_state := X\<rparr>) = domain_sep_inv irqs st s
theory DomainSepInv

lemma detype_interrupts_states[simp]:
  "interrupt_states (detype S s) = interrupt_states s" by (simp add: detype_def)

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

lemma detype_domain_sep_inv[simp]:
  "domain_sep_inv irqs st s \<longrightarrow> domain_sep_inv irqs st (detype 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 st (detype S s)
theory DomainSepInv

lemma domain_sep_inv_detype_lift:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. domain_sep_inv irqs st\<rbrace> \<Longrightarrow>
   \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. domain_sep_inv irqs st (detype S s)\<rbrace>" by (strengthen detype_domain_sep_inv, assumption)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. domain_sep_inv irqs st\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. domain_sep_inv irqs st (detype S s)\<rbrace>
theory DomainSepInv

lemma set_cap_neg_cte_wp_at_other_helper:
  "\<lbrakk> \<not> cte_wp_at P slot s; oslot \<noteq> slot; ko_at (TCB x) (fst oslot) s;
     tcb_cap_cases (snd oslot) = Some (getF, setF, restr) \<rbrakk>
     \<Longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(fst oslot \<mapsto> TCB (setF (\<lambda> x. cap) x))\<rparr>)" apply (rule notI) apply (erule cte_wp_atE) apply (fastforce elim: notE intro: cte_wp_at_cteI split: if_splits) apply (fastforce elim: notE intro: set_cap_neg_cte_wp_at_other_helper') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> cte_wp_at P slot s; oslot \<noteq> slot; ko_at (TCB x) (fst oslot) s; tcb_cap_cases (snd oslot) = Some (getF, setF, restr)\<rbrakk> \<Longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(fst oslot \<mapsto> TCB (setF (\<lambda>x. cap) x))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> cte_wp_at P slot s; oslot \<noteq> slot; ko_at (TCB x) (fst oslot) s; tcb_cap_cases (snd oslot) = Some (getF, setF, restr); cte_wp_at P slot (s\<lparr>kheap := (kheap s)(fst oslot \<mapsto> TCB (setF (\<lambda>x. cap) x))\<rparr>)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>sz fun cte. \<lbrakk>\<not> cte_wp_at P slot s; oslot \<noteq> slot; ko_at (TCB x) (fst oslot) s; tcb_cap_cases (snd oslot) = Some (getF, setF, restr); kheap (s\<lparr>kheap := (kheap s)(fst oslot \<mapsto> TCB (setF (\<lambda>x. cap) x))\<rparr>) (fst slot) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd slot) = Some cte; P cte\<rbrakk> \<Longrightarrow> False
 2. \<And>tcb getFa setFa restra. \<lbrakk>\<not> cte_wp_at P slot s; oslot \<noteq> slot; ko_at (TCB x) (fst oslot) s; tcb_cap_cases (snd oslot) = Some (getF, setF, restr); kheap (s\<lparr>kheap := (kheap s)(fst oslot \<mapsto> TCB (setF (\<lambda>x. cap) x))\<rparr>) (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getFa, setFa, restra); P (getFa tcb)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>tcb getFa setFa restra. \<lbrakk>\<not> cte_wp_at P slot s; oslot \<noteq> slot; ko_at (TCB x) (fst oslot) s; tcb_cap_cases (snd oslot) = Some (getF, setF, restr); kheap (s\<lparr>kheap := (kheap s)(fst oslot \<mapsto> TCB (setF (\<lambda>x. cap) x))\<rparr>) (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getFa, setFa, restra); P (getFa tcb)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory DomainSepInv

lemma domain_sep_inv_cap_IRQControlCap:
  "\<lbrakk> domain_sep_inv_cap irqs cap; \<not> irqs \<rbrakk> \<Longrightarrow> cap \<noteq> IRQControlCap" by (auto simp: domain_sep_inv_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>domain_sep_inv_cap irqs cap; \<not> irqs\<rbrakk> \<Longrightarrow> cap \<noteq> IRQControlCap
theory DomainSepInv

lemma set_cap_domain_sep_inv:
  "\<lbrace>domain_sep_inv irqs st and K (domain_sep_inv_cap irqs cap)\<rbrace>
   set_cap cap slot
   \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" apply (rule hoare_gen_asm) apply (rule hoare_pre) apply (rule domain_sep_inv_wp) apply (wp set_cap_neg_cte_wp_at | simp add: pred_neg_def | blast)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and K (domain_sep_inv_cap irqs cap)\<rbrace> set_cap cap slot \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. domain_sep_inv_cap irqs cap \<Longrightarrow> \<lbrace>domain_sep_inv irqs st\<rbrace> set_cap cap slot \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (2 subgoals):
 1. domain_sep_inv_cap irqs cap \<Longrightarrow> \<lbrace>?Q2\<rbrace> set_cap cap slot \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>s. \<lbrakk>domain_sep_inv_cap irqs cap; domain_sep_inv irqs st s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (3 subgoals):
 1. \<And>slota. domain_sep_inv_cap irqs cap \<Longrightarrow> \<lbrace>(\<lambda>s. \<not> cte_wp_at (not domain_sep_inv_cap irqs) slota s) and ?P5\<rbrace> set_cap cap slot \<lbrace>\<lambda>_ s. \<not> cte_wp_at (not domain_sep_inv_cap irqs) slota s\<rbrace>
 2. \<And>P. \<lbrakk>domain_sep_inv_cap irqs cap; \<not> irqs\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. P (interrupt_states s)) and ?R5\<rbrace> set_cap cap slot \<lbrace>\<lambda>_ s. P (interrupt_states s)\<rbrace>
 3. \<And>s. \<lbrakk>domain_sep_inv_cap irqs cap; domain_sep_inv irqs st s\<rbrakk> \<Longrightarrow> (domain_sep_inv irqs st and ?P5 and (\<lambda>s. irqs \<or> ?R5 s)) s proof (prove)
goal:
No subgoals!
theory DomainSepInv

lemma cte_wp_at_domain_sep_inv_cap:
  "\<lbrakk> domain_sep_inv irqs st s; cte_wp_at ((=) cap) slot s \<rbrakk>
     \<Longrightarrow> domain_sep_inv_cap irqs cap" apply (case_tac slot) apply (auto simp: domain_sep_inv_def domain_sep_inv_cap_def split: cap.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>domain_sep_inv irqs st s; cte_wp_at ((=) cap) slot s\<rbrakk> \<Longrightarrow> domain_sep_inv_cap irqs cap proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>domain_sep_inv irqs st s; cte_wp_at ((=) cap) slot s; slot = (a, b)\<rbrakk> \<Longrightarrow> domain_sep_inv_cap irqs cap proof (prove)
goal:
No subgoals!
theory DomainSepInv

lemma weak_derived_irq_handler:
  "weak_derived (IRQHandlerCap irq) cap \<Longrightarrow> cap = (IRQHandlerCap irq)" by (auto simp: weak_derived_def copy_of_def same_object_as_def split: cap.splits if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_derived (IRQHandlerCap irq) cap \<Longrightarrow> cap = IRQHandlerCap irq
theory DomainSepInv

lemma weak_derived_DomainCap:
  "weak_derived c' c \<Longrightarrow> (c' = DomainCap) = (c = DomainCap)" apply (clarsimp simp: weak_derived_def) apply (erule disjE) apply (clarsimp simp: copy_of_def split: if_split_asm) apply (auto simp: is_cap_simps same_object_as_def
              split: cap.splits)[1] apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_derived c' c \<Longrightarrow> (c' = DomainCap) = (c = DomainCap) proof (prove)
goal (1 subgoal):
 1. copy_of c' c \<and> cap_asid c' = cap_asid c \<and> cap_asid_base c' = cap_asid_base c \<and> cap_vptr c' = cap_vptr c \<or> c = c' \<Longrightarrow> (c' = DomainCap) = (c = DomainCap) proof (prove)
goal (2 subgoals):
 1. copy_of c' c \<and> cap_asid c' = cap_asid c \<and> cap_asid_base c' = cap_asid_base c \<and> cap_vptr c' = cap_vptr c \<Longrightarrow> (c' = DomainCap) = (c = DomainCap)
 2. c = c' \<Longrightarrow> (c' = DomainCap) = (c = DomainCap) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<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'; cap_asid c' = cap_asid c; cap_asid_base c' = cap_asid_base c; cap_vptr c' = cap_vptr c\<rbrakk> \<Longrightarrow> (c' = DomainCap) = (c = DomainCap)
 2. c = c' \<Longrightarrow> (c' = DomainCap) = (c = DomainCap) proof (prove)
goal (1 subgoal):
 1. c = c' \<Longrightarrow> (c' = DomainCap) = (c = DomainCap) proof (prove)
goal:
No subgoals!
theory DomainSepInv

lemma cte_wp_at_weak_derived_domain_sep_inv_cap:
  "\<lbrakk> domain_sep_inv irqs st s; cte_wp_at (weak_derived cap) slot s \<rbrakk>
     \<Longrightarrow> domain_sep_inv_cap irqs cap" apply (cases slot) apply (force simp: domain_sep_inv_def domain_sep_inv_cap_def
              split: cap.splits
               dest: cte_wp_at_norm weak_derived_irq_handler weak_derived_DomainCap) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>domain_sep_inv irqs st s; cte_wp_at (weak_derived cap) slot s\<rbrakk> \<Longrightarrow> domain_sep_inv_cap irqs cap proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>domain_sep_inv irqs st s; cte_wp_at (weak_derived cap) slot s; slot = (a, b)\<rbrakk> \<Longrightarrow> domain_sep_inv_cap irqs cap proof (prove)
goal:
No subgoals!
theory DomainSepInv

lemma is_derived_IRQHandlerCap:
  "is_derived m src (IRQHandlerCap irq) cap \<Longrightarrow> (cap = IRQHandlerCap irq)" apply (clarsimp simp: is_derived_def) apply (case_tac cap, simp_all add: is_cap_simps cap_master_cap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_derived m src (IRQHandlerCap irq) cap \<Longrightarrow> cap = IRQHandlerCap irq proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> is_zombie cap; if is_untyped_cap cap then cap_master_cap cap = cap_master_cap (IRQHandlerCap irq) \<and> descendants_of src m = {} else cap_master_cap cap = cap_master_cap (IRQHandlerCap irq) \<and> cap_badge cap = None; is_master_reply_cap cap = is_reply_cap (IRQHandlerCap irq); is_derived_arch (IRQHandlerCap irq) cap; \<not> is_reply_cap cap; \<not> is_master_reply_cap (IRQHandlerCap irq)\<rbrakk> \<Longrightarrow> cap = IRQHandlerCap irq proof (prove)
goal:
No subgoals!
theory DomainSepInv

lemma DomainCap_is_derived:
  "is_derived m src DomainCap cap \<Longrightarrow> cap = DomainCap" by (auto simp: is_derived_def is_reply_cap_def is_master_reply_cap_def cap_master_cap_def
          split: cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_derived m src DomainCap cap \<Longrightarrow> cap = DomainCap
theory DomainSepInv

lemma cte_wp_at_is_derived_domain_sep_inv_cap:
  "\<lbrakk> domain_sep_inv irqs st s; cte_wp_at (is_derived (cdt s) slot cap) slot s \<rbrakk>
     \<Longrightarrow> domain_sep_inv_cap irqs cap" apply (cases slot) apply (fastforce simp: domain_sep_inv_def domain_sep_inv_cap_def
                  split: cap.splits
                   dest: cte_wp_at_norm DomainCap_is_derived is_derived_IRQHandlerCap) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>domain_sep_inv irqs st s; cte_wp_at (is_derived (cdt s) slot cap) slot s\<rbrakk> \<Longrightarrow> domain_sep_inv_cap irqs cap proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>domain_sep_inv irqs st s; cte_wp_at (is_derived (cdt s) slot cap) slot s; slot = (a, b)\<rbrakk> \<Longrightarrow> domain_sep_inv_cap irqs cap proof (prove)
goal:
No subgoals!
theory DomainSepInv

lemma domain_sep_inv_exst_update[simp]:
  "domain_sep_inv irqs st (trans_state f s) = domain_sep_inv irqs st s" by (simp add: domain_sep_inv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. domain_sep_inv irqs st (trans_state f s) = domain_sep_inv irqs st s
theory DomainSepInv

lemma domain_sep_inv_is_original_cap_update[simp]:
  "domain_sep_inv irqs st (s\<lparr>is_original_cap := X\<rparr>) = domain_sep_inv irqs st s" by (simp add: domain_sep_inv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. domain_sep_inv irqs st (s\<lparr>is_original_cap := X\<rparr>) = domain_sep_inv irqs st s
theory DomainSepInv

lemma domain_sep_inv_cdt_update[simp]:
  "domain_sep_inv irqs st (s\<lparr>cdt := X\<rparr>) = domain_sep_inv irqs st s" by (simp add: domain_sep_inv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. domain_sep_inv irqs st (s\<lparr>cdt := X\<rparr>) = domain_sep_inv irqs st s
theory DomainSepInv

lemma set_untyped_cap_as_full_domain_sep_inv[wp]:
  "set_untyped_cap_as_full a b c \<lbrace>domain_sep_inv irqs st\<rbrace>" apply (clarsimp simp: set_untyped_cap_as_full_def) apply (rule hoare_pre) apply (rule set_cap_domain_sep_inv) apply (case_tac a, simp_all add: domain_sep_inv_cap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st\<rbrace> set_untyped_cap_as_full a b c \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_untyped_cap a; is_untyped_cap b; obj_ref_of a = obj_ref_of b; cap_bits_untyped a = cap_bits_untyped b\<rbrakk> \<Longrightarrow> \<lbrace>domain_sep_inv irqs st\<rbrace> set_cap (max_free_index_update a) c \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_untyped_cap a; is_untyped_cap b; obj_ref_of a = obj_ref_of b; cap_bits_untyped a = cap_bits_untyped b\<rbrakk> \<Longrightarrow> \<lbrace>?Q12\<rbrace> set_cap (max_free_index_update a) c \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>s. \<lbrakk>is_untyped_cap a; is_untyped_cap b; obj_ref_of a = obj_ref_of b; cap_bits_untyped a = cap_bits_untyped b; domain_sep_inv irqs st s\<rbrakk> \<Longrightarrow> ?Q12 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_untyped_cap a; is_untyped_cap b; obj_ref_of a = obj_ref_of b; cap_bits_untyped a = cap_bits_untyped b; domain_sep_inv irqs st s\<rbrakk> \<Longrightarrow> (domain_sep_inv irqs st and K (domain_sep_inv_cap irqs (max_free_index_update a))) s proof (prove)
goal:
No subgoals!
theory DomainSepInv

lemma cap_insert_domain_sep_inv:
  "\<lbrace>domain_sep_inv irqs st and (\<lambda>s. cte_wp_at (is_derived (cdt s) slot cap) slot s)\<rbrace>
   cap_insert cap slot dest_slot
   \<lbrace>\<lambda>_. domain_sep_inv irqs st \<rbrace>" apply (simp add: cap_insert_def) apply (wpsimp wp: set_cap_domain_sep_inv get_cap_wp set_original_wp dxo_wp_weak) apply (blast dest: cte_wp_at_is_derived_domain_sep_inv_cap) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and (\<lambda>s. cte_wp_at (is_derived (cdt s) slot cap) slot s)\<rbrace> cap_insert cap slot dest_slot \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and (\<lambda>s. cte_wp_at (is_derived (cdt s) slot cap) slot s)\<rbrace> do src_cap <- get_cap slot;
old_cap <- get_cap dest_slot;
y <- assert (old_cap = NullCap);
y <- set_untyped_cap_as_full src_cap cap slot;
y <- set_cap cap dest_slot;
is_original <- gets is_original_cap;
src_p <- gets (\<lambda>s. cdt s slot);
dest_p <- gets (\<lambda>s. cdt s dest_slot);
y <- update_cdt (\<lambda>cdt. cdt(dest_slot := if should_be_parent_of src_cap (is_original slot) cap (is_cap_revocable cap src_cap) then Some slot else cdt slot));
y <- do_extended_op (cap_insert_ext (should_be_parent_of src_cap (is_original slot) cap (is_cap_revocable cap src_cap)) slot dest_slot src_p dest_p);
set_original dest_slot (is_cap_revocable cap src_cap)
od \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>domain_sep_inv irqs st s; cte_wp_at (is_derived (cdt s) slot cap) slot s; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) dest_slot s\<rbrakk> \<Longrightarrow> domain_sep_inv_cap irqs cap proof (prove)
goal:
No subgoals!
theory DomainSepInv

lemma domain_sep_inv_cap_NullCap[simp]:
  "domain_sep_inv_cap irqs NullCap" by (simp add: domain_sep_inv_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. domain_sep_inv_cap irqs NullCap
theory DomainSepInv

lemma cap_move_domain_sep_inv:
  "\<lbrace>domain_sep_inv irqs st and (\<lambda>s. cte_wp_at (weak_derived cap) slot s)\<rbrace>
   cap_move cap slot dest_slot
   \<lbrace>\<lambda>_. domain_sep_inv irqs st \<rbrace>" apply (simp add: cap_move_def) apply (wpsimp wp: set_cap_domain_sep_inv get_cap_wp set_original_wp dxo_wp_weak) apply (blast dest: cte_wp_at_weak_derived_domain_sep_inv_cap) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and cte_wp_at (weak_derived cap) slot\<rbrace> cap_move cap slot dest_slot \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and cte_wp_at (weak_derived cap) slot\<rbrace> do y <- set_cap cap dest_slot;
y <- set_cap NullCap slot;
src_p <- gets (\<lambda>s. cdt s slot);
dest_p <- gets (\<lambda>s. cdt s dest_slot);
cdt <- gets cdt;
y <- set_cdt (\<lambda>r. if (if r = slot then None else if r = dest_slot then cdt slot else cdt r) = Some slot then Some dest_slot else if r = slot then None else if r = dest_slot then cdt slot else cdt r);
y <- do_extended_op (cap_move_ext slot dest_slot src_p dest_p);
is_original <- gets is_original_cap;
y <- set_original dest_slot (is_original slot);
set_original slot False
od \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>domain_sep_inv irqs st s; cte_wp_at (weak_derived cap) slot s\<rbrakk> \<Longrightarrow> domain_sep_inv_cap irqs cap proof (prove)
goal:
No subgoals!
theory DomainSepInv

lemma deleted_irq_handler_domain_sep_inv:
  "\<lbrace>domain_sep_inv irqs st and K irqs\<rbrace>
   deleted_irq_handler irq
   \<lbrace>\<lambda>_ s. domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state)\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: deleted_irq_handler_def set_irq_state_def) apply wp apply (simp add: domain_sep_inv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and K irqs\<rbrace> deleted_irq_handler irq \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. irqs \<Longrightarrow> \<lbrace>domain_sep_inv irqs st\<rbrace> deleted_irq_handler irq \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. irqs \<Longrightarrow> \<lbrace>domain_sep_inv True st\<rbrace> do y <- modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(irq := IRQInactive)\<rparr>);
do_machine_op (maskInterrupt True irq)
od \<lbrace>\<lambda>_. domain_sep_inv True st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>irqs; domain_sep_inv True st s\<rbrakk> \<Longrightarrow> domain_sep_inv True st (s\<lparr>interrupt_states := (interrupt_states s)(irq := IRQInactive)\<rparr>) proof (prove)
goal:
No subgoals!