kings-crown/FVELER_Isabelle huggingface dataset:
theory Ipc_R

lemma loadWordUser_corres':
  "\<lbrakk> y < unat max_ipc_words; y' = of_nat y * 4 \<rbrakk> \<Longrightarrow>
  corres (=) \<top> (valid_ipc_buffer_ptr' a) (load_word_offs a y) (loadWordUser (a + y'))" apply simp apply (erule loadWordUser_corres) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y < unat max_ipc_words; y' = word_of_nat y * 4\<rbrakk> \<Longrightarrow> corres (=) (\<lambda>_. True) (valid_ipc_buffer_ptr' a) (load_word_offs a y) (loadWordUser (a + y')) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y < unat max_ipc_words; y' = word_of_nat y * 4\<rbrakk> \<Longrightarrow> corres (=) (\<lambda>_. True) (valid_ipc_buffer_ptr' a) (load_word_offs a y) (loadWordUser (a + word_of_nat y * 4)) proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma getExtraCptrs_inv[wp]:
  "\<lbrace>P\<rbrace> getExtraCPtrs buf mi \<lbrace>\<lambda>rv. P\<rbrace>" apply (cases mi, cases buf, simp_all add: getExtraCPtrs_def) apply (wp dmo_inv' mapM_wp' loadWord_inv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> getExtraCPtrs buf mi \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 a. \<lbrakk>mi = Types_H.message_info.MI x1 x2 x3 x4; buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> mapM loadWordUser (map (\<lambda>x. a + (x + (msgMaxLength + 1)) * word_of_nat wordSize) [1 , 2 .e. x2]) \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma badge_derived_mask [simp]:
  "badge_derived' (maskCapRights R c) c' = badge_derived' c c'" by (simp add: badge_derived'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. badge_derived' (global.maskCapRights R c) c' = badge_derived' c c'
theory Ipc_R

lemma corres_set_extra_badge:
  "b' = b \<Longrightarrow>
  corres dc (in_user_frame buffer)
         (valid_ipc_buffer_ptr' buffer and
          (\<lambda>_. msg_max_length + 2 + n < unat max_ipc_words))
         (set_extra_badge buffer b n) (setExtraBadge buffer b' n)" apply (rule corres_gen_asm2) apply (drule storeWordUser_corres [where a=buffer and w=b]) apply (simp add: set_extra_badge_def setExtraBadge_def buffer_cptr_index_def
                   bufferCPtrOffset_def Let_def) apply (simp add: word_size word_size_def wordSize_def wordBits_def
                   bufferCPtrOffset_def buffer_cptr_index_def msgMaxLength_def
                   msg_max_length_def msgLengthBits_def store_word_offs_def
                   add.commute add.left_commute) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. b' = b \<Longrightarrow> corres dc (in_user_frame buffer) (valid_ipc_buffer_ptr' buffer and (\<lambda>_. msg_max_length + 2 + n < unat max_ipc_words)) (set_extra_badge buffer b n) (setExtraBadge buffer b' n) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b' = b; msg_max_length + 2 + n < unat max_ipc_words\<rbrakk> \<Longrightarrow> corres dc (in_user_frame buffer) (valid_ipc_buffer_ptr' buffer) (set_extra_badge buffer b n) (setExtraBadge buffer b' n) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b' = b; corres dc (in_user_frame buffer) (valid_ipc_buffer_ptr' buffer) (store_word_offs buffer (msg_max_length + 2 + n) b) (storeWordUser (buffer + word_of_nat (msg_max_length + 2 + n) * 4) b)\<rbrakk> \<Longrightarrow> corres dc (in_user_frame buffer) (valid_ipc_buffer_ptr' buffer) (set_extra_badge buffer b n) (setExtraBadge buffer b' n) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b' = b; corres dc (in_user_frame buffer) (valid_ipc_buffer_ptr' buffer) (store_word_offs buffer (Suc (Suc (msg_max_length + n))) b) (storeWordUser (buffer + (8 + (word_of_nat msg_max_length * 4 + word_of_nat n * 4))) b)\<rbrakk> \<Longrightarrow> corres dc (in_user_frame buffer) (valid_ipc_buffer_ptr' buffer) (store_word_offs buffer (Suc (Suc (msg_max_length + n))) b) (storeWordUser (buffer + (msgMaxLength + 2) * word_of_nat wordSize + word_of_nat n * word_of_nat wordSize) b) proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma valid_mdb_untyped_incD':
  "valid_mdb' s \<Longrightarrow> untyped_inc' (ctes_of s)" by (simp add: valid_mdb'_def valid_mdb_ctes_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_mdb' s \<Longrightarrow> untyped_inc' (ctes_of s)
theory Ipc_R

lemma cteInsert_weak_cte_wp_at3:
  assumes imp:"\<And>c. P c \<Longrightarrow> \<not> isUntypedCap c"
  shows " \<lbrace>\<lambda>s. if p = dest then P cap
            else cte_wp_at' (\<lambda>c. P (cteCap c)) p s\<rbrace>
    cteInsert cap src dest
   \<lbrace>\<lambda>uu. cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace>" by (wp updateMDB_weak_cte_wp_at updateCap_cte_wp_at_cases getCTE_wp' hoare_weak_lift_imp
         | clarsimp simp: comp_def cteInsert_def
         | unfold setUntypedCapAsFull_def
         | auto simp: cte_wp_at'_def dest!: imp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if p = dest then P cap else cte_wp_at' (\<lambda>c. P (cteCap c)) p s\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>uu. cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace>
theory Ipc_R

lemma maskedAsFull_null_cap[simp]:
  "(maskedAsFull x y = capability.NullCap) = (x = capability.NullCap)"
  "(capability.NullCap  = maskedAsFull x y) = (x = capability.NullCap)" by (case_tac x, auto simp:maskedAsFull_def isCap_simps )

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (maskedAsFull x y = capability.NullCap) = (x = capability.NullCap) &&& (capability.NullCap = maskedAsFull x y) = (x = capability.NullCap)
theory Ipc_R

lemma maskCapRights_eq_null:
  "(RetypeDecls_H.maskCapRights r xa = capability.NullCap) =
   (xa = capability.NullCap)" apply (cases xa; simp add: maskCapRights_def isCap_simps) apply (rename_tac arch_capability) apply (case_tac arch_capability) apply (simp_all add: ARM_H.maskCapRights_def isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (global.maskCapRights r xa = capability.NullCap) = (xa = capability.NullCap) proof (prove)
goal (1 subgoal):
 1. \<And>x8. xa = capability.ArchObjectCap x8 \<Longrightarrow> Arch.maskCapRights r x8 \<noteq> capability.NullCap proof (prove)
goal (1 subgoal):
 1. \<And>arch_capability. xa = capability.ArchObjectCap arch_capability \<Longrightarrow> Arch.maskCapRights r arch_capability \<noteq> capability.NullCap proof (prove)
goal (5 subgoals):
 1. \<And>arch_capability x11 x12. \<lbrakk>xa = capability.ArchObjectCap arch_capability; arch_capability = arch_capability.ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> Arch.maskCapRights r arch_capability \<noteq> capability.NullCap
 2. \<And>arch_capability. \<lbrakk>xa = capability.ArchObjectCap arch_capability; arch_capability = arch_capability.ASIDControlCap\<rbrakk> \<Longrightarrow> Arch.maskCapRights r arch_capability \<noteq> capability.NullCap
 3. \<And>arch_capability x31 x32 x33 x34 x35. \<lbrakk>xa = capability.ArchObjectCap arch_capability; arch_capability = arch_capability.PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> Arch.maskCapRights r arch_capability \<noteq> capability.NullCap
 4. \<And>arch_capability x41 x42. \<lbrakk>xa = capability.ArchObjectCap arch_capability; arch_capability = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> Arch.maskCapRights r arch_capability \<noteq> capability.NullCap
 5. \<And>arch_capability x51 x52. \<lbrakk>xa = capability.ArchObjectCap arch_capability; arch_capability = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> Arch.maskCapRights r arch_capability \<noteq> capability.NullCap proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma transferCapsToSlots_aligned'[wp]:
  "\<lbrace>pspace_aligned'\<rbrace>
     transferCapsToSlots ep buffer n caps slots mi
   \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace>" by (wp transferCapsToSlots_pres1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned'\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace>
theory Ipc_R

lemma transferCapsToSlots_no_0_obj' [wp]:
  "\<lbrace>no_0_obj'\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. no_0_obj'\<rbrace>" by (wp transferCapsToSlots_pres1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_0_obj'\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. no_0_obj'\<rbrace>
theory Ipc_R

lemma transferCapsToSlots_vp[wp]:
  "\<lbrace>\<lambda>s. valid_pspace' s \<and> distinct slots
          \<and> length slots \<le> 1
          \<and> (\<forall>x \<in> set slots. ex_cte_cap_to' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s)
          \<and> (\<forall>x \<in> set slots. real_cte_at' x s)
          \<and> transferCaps_srcs caps s\<rbrace>
    transferCapsToSlots ep buffer n caps slots mi
   \<lbrace>\<lambda>rv. valid_pspace'\<rbrace>" apply (rule hoare_pre) apply (simp add: valid_pspace'_def | wp)+ apply (fastforce simp: cte_wp_at_ctes_of dest: ctes_of_valid') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_pspace' s \<and> distinct slots \<and> length slots \<le> 1 \<and> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set slots. real_cte_at' x s) \<and> (\<forall>x\<in>set caps. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. valid_pspace'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. valid_pspace'\<rbrace>
 2. \<And>s. valid_pspace' s \<and> distinct slots \<and> length slots \<le> 1 \<and> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set slots. real_cte_at' x s) \<and> (\<forall>x\<in>set caps. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s \<and> distinct slots \<and> length slots \<le> Suc 0 \<and> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set slots. real_cte_at' x s) \<and> (\<forall>x\<in>set caps. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) \<Longrightarrow> \<forall>x\<in>set caps. valid_cap' (fst x) s proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma tcts_sch_act[wp]:
  "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace>
     transferCapsToSlots ep buffer n caps slots mi
   \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>" by (wp sch_act_wf_lift tcb_in_cur_domain'_lift transferCapsToSlots_pres1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>
theory Ipc_R

lemma tcts_vq'[wp]:
  "\<lbrace>valid_queues'\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. valid_queues'\<rbrace>" by (wp valid_queues_lift' transferCapsToSlots_pres1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues'\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. valid_queues'\<rbrace>
theory Ipc_R

lemma tcts_state_refs_of'[wp]:
  "\<lbrace>\<lambda>s. P (state_refs_of' s)\<rbrace>
     transferCapsToSlots ep buffer n caps slots mi
   \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace>" by (wp transferCapsToSlots_pres1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_refs_of' s)\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace>
theory Ipc_R

lemma tcts_iflive[wp]:
  "\<lbrace>\<lambda>s. if_live_then_nonz_cap' s \<and> distinct slots \<and>
         (\<forall>x\<in>set slots.
             ex_cte_cap_to' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s)\<rbrace>
  transferCapsToSlots ep buffer n caps slots mi
   \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>" by (wp transferCapsToSlots_pres2 | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if_live_then_nonz_cap' s \<and> distinct slots \<and> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s)\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>
theory Ipc_R

lemma tcts_ifunsafe[wp]:
  "\<lbrace>\<lambda>s. if_unsafe_then_cap' s \<and> distinct slots \<and>
         (\<forall>x\<in>set slots.  cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s \<and>
             ex_cte_cap_to' x s)\<rbrace> transferCapsToSlots ep buffer n caps slots mi
   \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace>" by (wp transferCapsToSlots_pres2 | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if_unsafe_then_cap' s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) x s)\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace>
theory Ipc_R

lemma tcts_ct[wp]:
  "\<lbrace>cur_tcb'\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. cur_tcb'\<rbrace>" by (wp transferCapsToSlots_pres1 cur_tcb_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cur_tcb'\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. cur_tcb'\<rbrace>
theory Ipc_R

lemma transferCapsToSlots_valid_arch [wp]:
  "\<lbrace>valid_arch_state'\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. valid_arch_state'\<rbrace>" by (rule transferCapsToSlots_pres1; wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state'\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. valid_arch_state'\<rbrace>
theory Ipc_R

lemma transferCapsToSlots_irq_node'[wp]:
  "\<lbrace>\<lambda>s. P (irq_node' s)\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv s. P (irq_node' s)\<rbrace>" by (wp transferCapsToSlots_pres1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (irq_node' s)\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv s. P (irq_node' s)\<rbrace>
theory Ipc_R

lemma valid_irq_handlers_ctes_ofD:
  "\<lbrakk> ctes_of s p = Some cte; cteCap cte = IRQHandlerCap irq; valid_irq_handlers' s \<rbrakk>
       \<Longrightarrow> irq_issued' irq s" by (auto simp: valid_irq_handlers'_def cteCaps_of_def ran_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; cteCap cte = capability.IRQHandlerCap irq; valid_irq_handlers' s\<rbrakk> \<Longrightarrow> irq_issued' irq s
theory Ipc_R

lemma setExtraBadge_irq_states'[wp]:
  "\<lbrace>valid_irq_states'\<rbrace> setExtraBadge buffer b n \<lbrace>\<lambda>_. valid_irq_states'\<rbrace>" apply (wp valid_irq_states_lift') apply (simp add: setExtraBadge_def storeWordUser_def) apply (wpsimp wp: no_irq dmo_lift' no_irq_storeWord) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> setExtraBadge buffer b n \<lbrace>\<lambda>_. valid_irq_states'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (irq_masks (ksMachineState s))\<rbrace> setExtraBadge buffer b n \<lbrace>\<lambda>_ s. P (irq_masks (ksMachineState s))\<rbrace>
 2. \<And>s. valid_irq_states' s \<Longrightarrow> valid_irq_states' s proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (irq_masks (ksMachineState s))\<rbrace> do y <- stateAssert (pointerInUserData (buffer + bufferCPtrOffset + word_of_nat n * word_of_nat wordSize)) [];
doMachineOp (storeWord (buffer + bufferCPtrOffset + word_of_nat n * word_of_nat wordSize) b)
od \<lbrace>\<lambda>_ s. P (irq_masks (ksMachineState s))\<rbrace>
 2. \<And>s. valid_irq_states' s \<Longrightarrow> valid_irq_states' s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_irq_states' s \<Longrightarrow> valid_irq_states' s proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma transferCapsToSlots_irq_states' [wp]:
  "\<lbrace>valid_irq_states'\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>_. valid_irq_states'\<rbrace>" by (wp transferCapsToSlots_pres1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>_. valid_irq_states'\<rbrace>
theory Ipc_R

lemma transferCapsToSlots_irqs_masked'[wp]:
  "\<lbrace>irqs_masked'\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. irqs_masked'\<rbrace>" by (wp transferCapsToSlots_pres1 irqs_masked_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>irqs_masked'\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. irqs_masked'\<rbrace>
theory Ipc_R

lemma setExtraBadge_vms'[wp]:
  "\<lbrace>valid_machine_state'\<rbrace> setExtraBadge buffer b n \<lbrace>\<lambda>_. valid_machine_state'\<rbrace>" by (simp add: setExtraBadge_def) wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state'\<rbrace> setExtraBadge buffer b n \<lbrace>\<lambda>_. valid_machine_state'\<rbrace>
theory Ipc_R

lemma transferCapsToSlots_vms[wp]:
  "\<lbrace>\<lambda>s. valid_machine_state' s\<rbrace>
   transferCapsToSlots ep buffer n caps slots mi
   \<lbrace>\<lambda>_ s. valid_machine_state' s\<rbrace>" by (wp transferCapsToSlots_pres1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state'\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>_. valid_machine_state'\<rbrace>
theory Ipc_R

lemma tcts_ct_not_inQ[wp]:
  "\<lbrace>ct_not_inQ\<rbrace>
   transferCapsToSlots ep buffer n caps slots mi
   \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>" by (wp transferCapsToSlots_pres1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_inQ\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>
theory Ipc_R

lemma grs_distinct'[wp]:
  "\<lbrace>\<top>\<rbrace> getReceiveSlots t buf \<lbrace>\<lambda>rv s. distinct rv\<rbrace>" apply (cases buf, simp_all add: getReceiveSlots_def
                                  split_def unlessE_def) apply (wp, simp) apply (wp | simp only: distinct.simps list.simps empty_iff)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> getReceiveSlots t buf \<lbrace>\<lambda>rv s. distinct rv\<rbrace> proof (prove)
goal (2 subgoals):
 1. buf = None \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return [] \<lbrace>\<lambda>rv s. distinct rv\<rbrace>
 2. \<And>a. buf = Some a \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do ct <- loadCapTransfer a;
emptyOnFailure (doE cnode <- unifyFailure (lookupCap t (ctReceiveRoot ct));
slot <- unifyFailure (lookupSlotForCNodeOp False cnode (ctReceiveIndex ct) (ctReceiveDepth ct));
cte <- liftE (getCTE slot);
y <- if cteCap cte = capability.NullCap then returnOk () else throwError ();
returnOk [slot]
odE)
od \<lbrace>\<lambda>rv s. distinct rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. buf = Some a \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do ct <- loadCapTransfer a;
emptyOnFailure (doE cnode <- unifyFailure (lookupCap t (ctReceiveRoot ct));
slot <- unifyFailure (lookupSlotForCNodeOp False cnode (ctReceiveIndex ct) (ctReceiveDepth ct));
cte <- liftE (getCTE slot);
y <- if cteCap cte = capability.NullCap then returnOk () else throwError ();
returnOk [slot]
odE)
od \<lbrace>\<lambda>rv s. distinct rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a s. \<lbrakk>buf = Some a; True\<rbrakk> \<Longrightarrow> True \<and> True \<and> True \<and> True \<and> True \<and> True \<and> \<not> False \<and> True proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma isPageCap_maskCapRights[simp]:
" isArchCap isPageCap (RetypeDecls_H.maskCapRights R c) = isArchCap isPageCap c" apply (case_tac c; simp add: isCap_simps isArchCap_def maskCapRights_def) apply (rename_tac arch_capability) apply (case_tac arch_capability; simp add: isCap_simps ARM_H.maskCapRights_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isArchCap isPageCap (global.maskCapRights R c) = isArchCap isPageCap c proof (prove)
goal (1 subgoal):
 1. \<And>x8. c = capability.ArchObjectCap x8 \<Longrightarrow> (case Arch.maskCapRights R x8 of capability.ArchObjectCap acap \<Rightarrow> isPageCap acap | _ \<Rightarrow> False) = (\<exists>d v0 v1 v2 v3. x8 = arch_capability.PageCap d v0 v1 v2 v3) proof (prove)
goal (1 subgoal):
 1. \<And>arch_capability. c = capability.ArchObjectCap arch_capability \<Longrightarrow> (case Arch.maskCapRights R arch_capability of capability.ArchObjectCap acap \<Rightarrow> isPageCap acap | _ \<Rightarrow> False) = (\<exists>d v0 v1 v2 v3. arch_capability = arch_capability.PageCap d v0 v1 v2 v3) proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma capReplyMaster_mask[simp]:
  "isReplyCap c \<Longrightarrow> capReplyMaster (maskCapRights R c) = capReplyMaster c" by (clarsimp simp: isCap_simps maskCapRights_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isReplyCap c \<Longrightarrow> capReplyMaster (global.maskCapRights R c) = capReplyMaster c
theory Ipc_R

lemma is_derived_mask' [simp]:
  "is_derived' m p (maskCapRights R c) = is_derived' m p c" apply (rule ext) apply (simp add: is_derived'_def badge_derived'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_derived' m p (global.maskCapRights R c) = is_derived' m p c proof (prove)
goal (1 subgoal):
 1. \<And>x. is_derived' m p (global.maskCapRights R c) x = is_derived' m p c x proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma updateCapData_ordering:
  "\<lbrakk> (x, capBadge cap) \<in> capBadge_ordering P; updateCapData p d cap \<noteq> NullCap \<rbrakk>
    \<Longrightarrow> (x, capBadge (updateCapData p d cap)) \<in> capBadge_ordering P" apply (cases cap, simp_all add: updateCapData_def isCap_simps Let_def
                                  capBadge_def ARM_H.updateCapData_def
                           split: if_split_asm) apply fastforce+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x, capBadge cap) \<in> capBadge_ordering P; global.updateCapData p d cap \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> (x, capBadge (global.updateCapData p d cap)) \<in> capBadge_ordering P proof (prove)
goal (2 subgoals):
 1. \<And>x31 x32 x33 x34. \<lbrakk>cap = capability.NotificationCap x31 0 x33 x34; x = None \<or> x = Some 0; \<not> p; x32 = 0\<rbrakk> \<Longrightarrow> (x, Some (d && mask 28)) \<in> capBadge_ordering P \<and> ((\<forall>v2. x33 = (\<not> v2)) \<longrightarrow> x = None) \<and> ((\<forall>v3. x34 = (\<not> v3)) \<longrightarrow> x = None)
 2. \<And>x51 x52 x53 x54 x55 x56. \<lbrakk>cap = capability.EndpointCap x51 0 x53 x54 x55 x56; x = None \<or> x = Some 0; \<not> p; x52 = 0\<rbrakk> \<Longrightarrow> (x, Some (d && mask 28)) \<in> capBadge_ordering P \<and> ((\<forall>v2. x53 = (\<not> v2)) \<longrightarrow> x = None) \<and> ((\<forall>v3. x54 = (\<not> v3)) \<longrightarrow> x = None) \<and> ((\<forall>v4. x55 = (\<not> v4)) \<longrightarrow> x = None) \<and> ((\<forall>v5. x56 = (\<not> v5)) \<longrightarrow> x = None) proof (prove)
goal:
No subgoals!