kings-crown/FVELER_Isabelle huggingface dataset:
theory Decode_IF

lemma decode_irq_handler_invocation_rev:
  "reads_equiv_valid_inv A aag \<top> (decode_irq_handler_invocation label irq cps)" unfolding decode_irq_handler_invocation_def by (wp | simp add: split_def Let_def | rule conjI impI)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (\<lambda>_. True) (decode_irq_handler_invocation label irq cps) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (\<lambda>_. True) (if gen_invocation_type label = IRQAckIRQ then returnOk $ ACKIrq irq else if gen_invocation_type label = IRQSetIRQHandler then if cps \<noteq> [] then let (cap, slot) = hd cps in if is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap then returnOk $ SetIRQHandler irq cap slot else throwError $ InvalidCapability 0 else throwError TruncatedMessage else if gen_invocation_type label = IRQClearIRQHandler then returnOk $ ClearIRQHandler irq else throwError IllegalOperation)
theory Decode_IF

lemma gets_applyE:
  "(liftE $ gets f) >>=E (\<lambda> f. g (f x)) = liftE (gets_apply f x) >>=E g" apply (simp add: liftE_bindE) apply (rule gets_apply) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. doE f <- liftE $ gets f;
g (f x)
odE = liftE (gets_apply f x) >>=E g proof (prove)
goal (1 subgoal):
 1. do f <- gets f;
g (f x)
od = gets_apply f x >>= g proof (prove)
goal:
No subgoals!
theory Decode_IF

lemma owns_cnode_owns_obj_ref_of_child_cnodes:
  "\<lbrakk> pas_refined aag s; is_subject aag (fst slot); cte_wp_at ((=) cap) slot s; is_cnode_cap cap \<rbrakk>
     \<Longrightarrow> is_subject aag (obj_ref_of cap)" by (blast intro: owns_cnode_owns_obj_ref_of_child_cnodes_threads_and_zombies)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); cte_wp_at ((=) cap) slot s; is_cnode_cap cap\<rbrakk> \<Longrightarrow> is_subject aag (obj_ref_of cap)
theory Decode_IF

lemma select_ext_ev_bind_lift:
  "(\<And>s t. \<lbrakk>I s t; A s t; a s \<in> S; a t \<in> S\<rbrakk> \<Longrightarrow> a s = a t)
   \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> equiv_valid_inv I A P (g x))
   \<Longrightarrow> equiv_valid_inv I A P (doE x \<leftarrow> (liftE $ (select_ext a S :: ('a, det_ext) s_monad)); g x odE)" apply (simp add: bindE_def liftE_def lift_def) apply (rule select_ext_ev_bind) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s t. \<lbrakk>I s t; A s t; a s \<in> S; a t \<in> S\<rbrakk> \<Longrightarrow> a s = a t; \<And>x. x \<in> S \<Longrightarrow> equiv_valid_inv I A P (g x)\<rbrakk> \<Longrightarrow> equiv_valid_inv I A P ((liftE $ select_ext a S) >>=E g) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s t. \<lbrakk>I s t; A s t; a s \<in> S; a t \<in> S\<rbrakk> \<Longrightarrow> a s = a t; \<And>x. x \<in> S \<Longrightarrow> equiv_valid_inv I A P (g x)\<rbrakk> \<Longrightarrow> equiv_valid_inv I A P (select_ext a S >>= g) proof (prove)
goal (2 subgoals):
 1. \<And>s t. \<lbrakk>\<And>s t. \<lbrakk>I s t; A s t; a s \<in> S; a t \<in> S\<rbrakk> \<Longrightarrow> a s = a t; \<And>x. x \<in> S \<Longrightarrow> equiv_valid_inv I A P (g x); I s t; A s t; a s \<in> S; a t \<in> S\<rbrakk> \<Longrightarrow> a s = a t
 2. \<And>x. \<lbrakk>\<And>s t. \<lbrakk>I s t; A s t; a s \<in> S; a t \<in> S\<rbrakk> \<Longrightarrow> a s = a t; \<And>x. x \<in> S \<Longrightarrow> equiv_valid_inv I A P (g x); x \<in> S\<rbrakk> \<Longrightarrow> equiv_valid_inv I A P (g x) proof (prove)
goal:
No subgoals!
theory Decode_IF

lemma decode_domain_invocation_reads_respects_f:
  "reads_respects_f aag l \<top> (decode_domain_invocation label args excaps)" apply (simp add: decode_domain_invocation_def) apply (wp | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (\<lambda>_. True) (decode_domain_invocation label args excaps) proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (\<lambda>_. True) (doE y <- whenE (gen_invocation_type label \<noteq> DomainSetSet) (throwError IllegalOperation);
domain <- case args of [] \<Rightarrow> throwError TruncatedMessage | x # xs \<Rightarrow> doE whenE (numDomains \<le> unat x) $ throwError $ InvalidArgument 0;
returnOk (UCAST(32 \<rightarrow> 8) x)
odE;
y <- whenE (excaps = []) (throwError TruncatedMessage);
case fst (hd excaps) of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE) proof (prove)
goal:
No subgoals!
theory ArchDecode_IF

lemma check_valid_ipc_buffer_rev[Decode_IF_assms]:
  "reads_equiv_valid_inv A aag \<top> (check_valid_ipc_buffer vptr cap)" unfolding check_valid_ipc_buffer_def fun_app_def apply (rule equiv_valid_guard_imp) apply (wpc | wp)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (\<lambda>_. True) (check_valid_ipc_buffer vptr cap) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (\<lambda>_. True) (case cap of ArchObjectCap (PageCap True x xa xb xc) \<Rightarrow> throwError IllegalOperation | ArchObjectCap (PageCap False x xa xb xc) \<Rightarrow> doE whenE (\<not> is_aligned vptr msg_align_bits) (throwError AlignmentError);
returnOk ()
odE | ArchObjectCap _ \<Rightarrow> throwError IllegalOperation | _ \<Rightarrow> throwError IllegalOperation) proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_inv A aag ?Q (case cap of ArchObjectCap (PageCap True x xa xb xc) \<Rightarrow> throwError IllegalOperation | ArchObjectCap (PageCap False x xa xb xc) \<Rightarrow> doE whenE (\<not> is_aligned vptr msg_align_bits) (throwError AlignmentError);
returnOk ()
odE | ArchObjectCap _ \<Rightarrow> throwError IllegalOperation | _ \<Rightarrow> throwError IllegalOperation)
 2. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> (cap = NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. cap = UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = ReplyCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> True) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> True) \<and> (cap = DomainCap \<longrightarrow> True) \<and> (cap = IRQControlCap \<longrightarrow> True) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. cap = ArchObjectCap x \<longrightarrow> (\<forall>xa xb. x = ASIDPoolCap xa xb \<longrightarrow> True) \<and> (x = ASIDControlCap \<longrightarrow> True) \<and> (\<forall>xa xb xc xd xe. x = PageCap xa xb xc xd xe \<longrightarrow> (xa = True \<longrightarrow> True) \<and> (xa = False \<longrightarrow> (\<not> is_aligned vptr msg_align_bits \<longrightarrow> True) \<and> True)) \<and> (\<forall>xa xb. x = PageTableCap xa xb \<longrightarrow> True) \<and> (\<forall>xa xb. x = PageDirectoryCap xa xb \<longrightarrow> True)) proof (prove)
goal:
No subgoals!
theory ArchDecode_IF

lemma arch_check_irq_rev[Decode_IF_assms, wp]:
  "reads_equiv_valid_inv A aag \<top> (arch_check_irq irq)" unfolding arch_check_irq_def apply (rule equiv_valid_guard_imp) apply wpsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (\<lambda>_. True) (arch_check_irq irq) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (\<lambda>_. True) (whenE (UCAST(10 \<rightarrow> 32) maxIRQ < irq) $ throwError (RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ))) proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_inv A aag ?Q (whenE (UCAST(10 \<rightarrow> 32) maxIRQ < irq) $ throwError (RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ)))
 2. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory ArchDecode_IF

lemma vspace_cap_rights_to_auth_mono[Decode_IF_assms]:
  "R \<subseteq> S \<Longrightarrow> vspace_cap_rights_to_auth R \<subseteq> vspace_cap_rights_to_auth S" by (auto simp: vspace_cap_rights_to_auth_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. R \<subseteq> S \<Longrightarrow> vspace_cap_rights_to_auth R \<subseteq> vspace_cap_rights_to_auth S
theory ArchDecode_IF

lemma lookup_pt_slot_rev:
  "reads_equiv_valid_inv A aag (K (is_subject aag (lookup_pd_slot pd vptr && ~~ mask pd_bits)))
                         (lookup_pt_slot pd vptr)" apply (simp add: lookup_pt_slot_def lookup_pd_slot_def) apply (wp get_pde_rev | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (K (is_subject aag (lookup_pd_slot pd vptr && ~~ mask pd_bits))) (lookup_pt_slot pd vptr) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (\<lambda>y. is_subject aag (pd + (vptr >> 20 << 2) && ~~ mask pd_bits)) (liftE (get_pde (pd + (vptr >> 20 << 2))) >>=E case_pde (throwError (MissingCapability 20)) (\<lambda>ptab x xa. returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2))) (\<lambda>word1 set1 word2 set2. throwError (MissingCapability 20)) (\<lambda>word set1 set2. throwError (MissingCapability 20))) proof (prove)
goal:
No subgoals!
theory ArchDecode_IF

lemma check_vp_alignment_rev:
  "reads_equiv_valid_inv A aag \<top> (check_vp_alignment sz vptr)" unfolding check_vp_alignment_def by (wp | simp add: crunch_simps split del: if_split)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (\<lambda>_. True) (check_vp_alignment sz vptr) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (\<lambda>_. True) (unlessE (is_aligned vptr (pageBitsForSize sz)) $ throwError AlignmentError)
theory ArchDecode_IF

lemma pas_cap_cur_auth_ASIDControlCap:
  "\<lbrakk> pas_cap_cur_auth aag (ArchObjectCap ASIDControlCap); reads_equiv aag s t; pas_refined aag x \<rbrakk>
     \<Longrightarrow> arm_asid_table (arch_state s) = arm_asid_table (arch_state t)" apply (rule ext) apply (subst asid_high_bits_of_shift[symmetric]) apply (subst (3) asid_high_bits_of_shift[symmetric]) apply (rule requiv_arm_asid_table_asid_high_bits_of_asid_eq'') apply (clarsimp simp: aag_cap_auth_def cap_links_asid_slot_def label_owns_asid_slot_def) apply (rule pas_refined_Control_into_is_subject_asid, blast+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_cap_cur_auth aag (ArchObjectCap ASIDControlCap); reads_equiv aag s t; pas_refined aag x\<rbrakk> \<Longrightarrow> asid_table s = asid_table t proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>pas_cap_cur_auth aag (ArchObjectCap ASIDControlCap); reads_equiv aag s t; pas_refined aag x\<rbrakk> \<Longrightarrow> asid_table s xa = asid_table t xa proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>pas_cap_cur_auth aag (ArchObjectCap ASIDControlCap); reads_equiv aag s t; pas_refined aag x\<rbrakk> \<Longrightarrow> asid_table s (asid_high_bits_of (UCAST(7 \<rightarrow> 32) xa << local.asid_low_bits)) = asid_table t xa proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>pas_cap_cur_auth aag (ArchObjectCap ASIDControlCap); reads_equiv aag s t; pas_refined aag x\<rbrakk> \<Longrightarrow> asid_table s (asid_high_bits_of (UCAST(7 \<rightarrow> 32) xa << local.asid_low_bits)) = asid_table t (asid_high_bits_of (UCAST(7 \<rightarrow> 32) xa << local.asid_low_bits)) proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>pas_cap_cur_auth aag (ArchObjectCap ASIDControlCap); reads_equiv aag s t; pas_refined aag x\<rbrakk> \<Longrightarrow> \<forall>asid. is_subject_asid (?aag4 xa) asid
 2. \<And>xa. \<lbrakk>pas_cap_cur_auth aag (ArchObjectCap ASIDControlCap); reads_equiv aag s t; pas_refined aag x\<rbrakk> \<Longrightarrow> reads_equiv (?aag4 xa) s t
 3. \<And>xa. \<lbrakk>pas_cap_cur_auth aag (ArchObjectCap ASIDControlCap); reads_equiv aag s t; pas_refined aag x\<rbrakk> \<Longrightarrow> pas_refined (?aag4 xa) (?x4 xa) proof (prove)
goal (3 subgoals):
 1. \<And>xa asid. \<lbrakk>reads_equiv aag s t; pas_refined aag x; \<forall>asid. (pasSubject aag, Control, pasASIDAbs aag asid) \<in> pasPolicy aag; cap_links_irq aag (pasSubject aag) (ArchObjectCap ASIDControlCap)\<rbrakk> \<Longrightarrow> is_subject_asid (?aag4 xa) asid
 2. \<And>xa. \<lbrakk>pas_cap_cur_auth aag (ArchObjectCap ASIDControlCap); reads_equiv aag s t; pas_refined aag x\<rbrakk> \<Longrightarrow> reads_equiv (?aag4 xa) s t
 3. \<And>xa. \<lbrakk>pas_cap_cur_auth aag (ArchObjectCap ASIDControlCap); reads_equiv aag s t; pas_refined aag x\<rbrakk> \<Longrightarrow> pas_refined (?aag4 xa) (?x4 xa) proof (prove)
goal:
No subgoals!
theory ArchDecode_IF

lemma resolve_vaddr_reads_respects:
  "reads_respects aag l
     (K (is_subject aag (lookup_pd_slot pd vptr && ~~ mask pd_bits)) and
        (\<lambda>s. case kheap s (lookup_pd_slot pd vptr && ~~ mask pd_bits) of
               Some (ArchObj (PageDirectory pd')) \<Rightarrow>
               (case pd' (ucast (lookup_pd_slot pd vptr && mask pd_bits >> 2)) of
                  PageTablePDE x y z \<Rightarrow> is_subject aag (lookup_pt_slot_no_fail (ptrFromPAddr x) vptr && ~~ mask pt_bits)
                | _ \<Rightarrow> True)
             | _ \<Rightarrow> True))
     (resolve_vaddr pd vptr)" apply (simp add: resolve_vaddr_def
         | wp get_master_pte_reads_respects get_master_pde_reads_respects get_master_pde_wp | wpc)+ apply (fastforce simp: obj_at_def split: pde.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (is_subject aag (lookup_pd_slot pd vptr && ~~ mask pd_bits)) and (\<lambda>s. case kheap s (lookup_pd_slot pd vptr && ~~ mask pd_bits) of None \<Rightarrow> True | Some (ArchObj (PageDirectory pd')) \<Rightarrow> case pd' (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) of PageTablePDE x y z \<Rightarrow> is_subject aag (lookup_pt_slot_no_fail (ptrFromPAddr x) vptr && ~~ mask pt_bits) | _ \<Rightarrow> True | Some (ArchObj _) \<Rightarrow> True | Some _ \<Rightarrow> True)) (resolve_vaddr pd vptr) proof (prove)
goal (1 subgoal):
 1. \<And>s. is_subject aag (lookup_pd_slot pd vptr && ~~ mask pd_bits) \<and> (case kheap s (lookup_pd_slot pd vptr && ~~ mask pd_bits) of None \<Rightarrow> True | Some (ArchObj (PageDirectory pd')) \<Rightarrow> case pd' (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) of PageTablePDE x y z \<Rightarrow> is_subject aag (lookup_pt_slot_no_fail (ptrFromPAddr x) vptr && ~~ mask pt_bits) | _ \<Rightarrow> True | Some (ArchObj _) \<Rightarrow> True | Some _ \<Rightarrow> True) \<Longrightarrow> \<forall>pda. ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s \<longrightarrow> (\<forall>x. (\<exists>xa xb. (case pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && ~~ mask 6 && mask pd_bits >> 2)) of SuperSectionPDE x xa xb \<Rightarrow> pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && ~~ mask 6 && mask pd_bits >> 2)) | _ \<Rightarrow> pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) = PageTablePDE x xa xb) \<longrightarrow> is_subject aag (lookup_pt_slot_no_fail (ptrFromPAddr x) vptr && ~~ mask pt_bits)) proof (prove)
goal:
No subgoals!
theory Syscall_IF

lemma tcb_context_merge[simp]:
  "arch_tcb_context_get (tcb_arch (tcb_registers_caps_merge tcb tcb')) =
   arch_tcb_context_get (tcb_arch tcb)" by (simp add: tcb_registers_caps_merge_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_tcb_context_get (tcb_arch (tcb_registers_caps_merge tcb tcb')) = arch_tcb_context_get (tcb_arch tcb)
theory Syscall_IF

lemma cap_revoke_globals_equiv:
  "\<lbrace>globals_equiv st and invs\<rbrace>
   cap_revoke slot
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" apply (rule hoare_strengthen_post, rule validE_valid,
         rule cap_revoke_preservation_desc_of[where Q="\<lambda>_. emptyable"]) by (wp cap_delete_globals_equiv preemption_point_inv
      | fastforce simp: emptyable_def dest: reply_slot_not_descendant)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and invs\<rbrace> cap_revoke slot \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s p. \<lbrace>globals_equiv st and invs and emptyable p\<rbrace> cap_delete p \<lbrace>\<lambda>_. globals_equiv st and invs\<rbrace>
 2. \<And>s sl sa. (globals_equiv st and invs) sa \<Longrightarrow> \<forall>sl'\<in>descendants_of sl (cdt sa). emptyable sl' sa
 3. \<And>s. \<lbrace>globals_equiv st and invs\<rbrace> preemption_point \<lbrace>\<lambda>_. globals_equiv st and invs\<rbrace>
 4. \<And>rv s. (globals_equiv st and invs) s \<Longrightarrow> globals_equiv st s
theory Syscall_IF

lemma invoke_cnode_globals_equiv:
  "\<lbrace>globals_equiv st and invs and valid_cnode_inv cinv\<rbrace>
   invoke_cnode cinv
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" unfolding invoke_cnode_def without_preemption_def fun_app_def apply (wp cap_insert_globals_equiv cap_move_globals_equiv cap_revoke_globals_equiv
            cap_delete_globals_equiv cap_swap_globals_equiv hoare_vcg_all_lift
            cancel_badged_sends_globals_equiv
         | wpc | wp (once) hoare_drop_imps | simp add: invs_valid_global_objs)+ apply (case_tac cinv; clarsimp simp: real_cte_emptyable_strg) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and invs and valid_cnode_inv cinv\<rbrace> invoke_cnode cinv \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and invs and valid_cnode_inv cinv\<rbrace> case cinv of InsertCall cap src_slot dest_slot \<Rightarrow> liftE (cap_insert cap src_slot dest_slot) | MoveCall cap src_slot dest_slot \<Rightarrow> liftE (cap_move cap src_slot dest_slot) | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> liftE (if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od) | SaveCall slot \<Rightarrow> liftE (do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od) | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> liftE (when (b \<noteq> 0) (cancel_badged_sends ep b)) | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. globals_equiv st s \<and> invs s \<and> valid_cnode_inv cinv s \<Longrightarrow> ((\<exists>x a b aa ba. cinv = InsertCall x (a, b) (aa, ba)) \<longrightarrow> valid_arch_state s) \<and> ((\<exists>x a b aa ba. cinv = MoveCall x (a, b) (aa, ba)) \<longrightarrow> valid_arch_state s) \<and> (\<forall>a b. cinv = DeleteCall (a, b) \<longrightarrow> emptyable (a, b) s) \<and> ((\<exists>x xa a b aa ba ab bb. cinv = RotateCall x xa (a, b) (aa, ba) (ab, bb)) \<longrightarrow> valid_arch_state s) \<and> ((\<exists>a b. cinv = SaveCall (a, b)) \<longrightarrow> valid_arch_state s) \<and> (\<forall>x. cinv = CancelBadgedSendsCall x \<longrightarrow> (\<forall>xa xb. xb \<noteq> 0 \<longrightarrow> (\<exists>xc. x = EndpointCap xa xb xc) \<longrightarrow> valid_arch_state s)) proof (prove)
goal:
No subgoals!
theory Syscall_IF

lemma cap_delete_reads_respects_f:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "reads_respects_f aag l
           (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action
                            and emptyable slot and pas_refined aag and cdt_change_allowed' aag slot)
           (cap_delete slot)" unfolding cap_delete_def by (wp rec_del_CTEDeleteCall_reads_respects_f) force

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and emptyable slot and pas_refined aag and cdt_change_allowed' aag slot) (cap_delete slot) proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and emptyable slot and pas_refined aag and cdt_change_allowed' aag slot) (doE rec_del (CTEDeleteCall slot True);
returnOk ()
odE)
theory Syscall_IF

lemma spec_gen_asm:
  "(Q \<Longrightarrow> spec_equiv_valid st D A B P f) \<Longrightarrow> spec_equiv_valid st D A B (P and K Q) f" by (simp add: spec_equiv_valid_def equiv_valid_2_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (Q \<Longrightarrow> spec_equiv_valid st D A B P f) \<Longrightarrow> spec_equiv_valid st D A B (P and K Q) f
theory Syscall_IF

lemma select_ev:
  "equiv_valid_inv I A (K(S \<noteq> {} \<longrightarrow> (\<exists>x. S = {x}))) (select S)" apply (clarsimp simp: equiv_valid_def spec_equiv_valid_def equiv_valid_2_def select_def) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A (K (S \<noteq> {} \<longrightarrow> (\<exists>x. S = {x}))) (select S) proof (prove)
goal (1 subgoal):
 1. \<And>x xa st t. \<lbrakk>x \<in> S; xa \<in> S; S \<noteq> {} \<longrightarrow> (\<exists>x. S = {x}); I st t; A st t\<rbrakk> \<Longrightarrow> x = xa proof (prove)
goal:
No subgoals!
theory Syscall_IF

lemma next_revoke_eq:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) cdt_list rv rv'
   \<Longrightarrow> is_subject aag (fst src_slot)
   \<Longrightarrow> next_revoke_cap src_slot rv = next_revoke_cap src_slot rv'" by (clarsimp simp: next_child_def equiv_for_def next_revoke_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) cdt_list rv rv'; is_subject aag (fst src_slot)\<rbrakk> \<Longrightarrow> next_revoke_cap src_slot rv = next_revoke_cap src_slot rv'
theory Syscall_IF

lemma next_revoke_eq':
  "\<lbrakk> reads_equiv_f aag s t; is_subject aag (fst src_slot) \<rbrakk>
     \<Longrightarrow> next_revoke_cap src_slot s = next_revoke_cap src_slot t" apply (rule next_revoke_eq) apply (fastforce simp: reads_equiv_f_def reads_equiv_def2 states_equiv_for_def equiv_for_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv_f aag s t; is_subject aag (fst src_slot)\<rbrakk> \<Longrightarrow> next_revoke_cap src_slot s = next_revoke_cap src_slot t proof (prove)
goal (2 subgoals):
 1. \<lbrakk>reads_equiv_f aag s t; is_subject aag (fst src_slot)\<rbrakk> \<Longrightarrow> equiv_for ((aag_can_read ?aag or aag_can_affect ?aag ?l) \<circ> fst) cdt_list s t
 2. \<lbrakk>reads_equiv_f aag s t; is_subject aag (fst src_slot)\<rbrakk> \<Longrightarrow> is_subject ?aag (fst src_slot) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv_f aag s t; is_subject aag (fst src_slot)\<rbrakk> \<Longrightarrow> is_subject aag (fst src_slot) proof (prove)
goal:
No subgoals!