kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpace_RAB_C

lemma lookupSlotForThread_ccorres[corres]:
  "ccorres (lookup_failure_rel \<currency> lookupSlot_raw_rel) lookupSlot_raw_xf
  (invs' and tcb_at' thread)
  (UNIV \<inter> {s. capptr_' s = cptr} \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr thread}) []
  (lookupSlotForThread thread cptr) (Call lookupSlot_'proc)" apply (rule ccorres_guard_imp2, rule lookupSlotForThread_ccorres') apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (lookup_failure_rel \<currency> lookupSlot_raw_rel) (liftxf errstate lookupSlot_raw_ret_C.status_C lookupSlot_raw_ret_C.slot_C ret__struct_lookupSlot_raw_ret_C_') (invs' and tcb_at' thread) (UNIV \<inter> \<lbrace>\<acute>capptr = cptr\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>) [] (lookupSlotForThread thread cptr) (Call lookupSlot_'proc) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and tcb_at' thread) s; s' \<in> UNIV \<inter> \<lbrace>\<acute>capptr = cptr\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>\<rbrakk> \<Longrightarrow> (valid_pspace' and tcb_at' thread) s \<and> s' \<in> \<lbrace>\<acute>capptr = cptr\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> proof (prove)
goal:
No subgoals!
theory Machine_C

lemma index_xf_for_sequence:
  "\<forall>s f. index_' (index_'_update f s) = f (index_' s)
          \<and> globals (index_'_update f s) = globals s" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s f. index_' (index_'_update f s) = f (index_' s) \<and> globals (index_'_update f s) = globals s
theory Machine_C

lemma lineStart_le_mono:
  "x \<le> y \<Longrightarrow> lineStart x \<le> lineStart y" by (clarsimp simp: lineStart_def cacheLineBits_def shiftr_shiftl1 neg_mask_mono_le)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> lineStart x \<le> lineStart y
theory Machine_C

lemma lineStart_sub:
  "\<lbrakk> x && mask 5 = y && mask 5\<rbrakk> \<Longrightarrow> lineStart (x - y) = lineStart x - lineStart y" apply (clarsimp simp: lineStart_def cacheLineBits_def shiftr_shiftl1) apply (clarsimp simp: mask_out_sub_mask) apply (clarsimp simp: mask_eqs(8)[symmetric]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x && mask 5 = y && mask 5 \<Longrightarrow> lineStart (x - y) = lineStart x - lineStart y proof (prove)
goal (1 subgoal):
 1. x && mask 5 = y && mask 5 \<Longrightarrow> x - y && ~~ mask 5 = (x && ~~ mask 5) - (y && ~~ mask 5) proof (prove)
goal (1 subgoal):
 1. x && mask 5 = y && mask 5 \<Longrightarrow> x - y && mask 5 = 0 proof (prove)
goal:
No subgoals!
theory Machine_C

lemma lineStart_mask:
  "lineStart x && mask 5 = 0" by (clarsimp simp: lineStart_def cacheLineBits_def shiftr_shiftl1 mask_AND_NOT_mask)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lineStart x && mask 5 = 0
theory Machine_C

lemma lineIndex_def2:
  "lineIndex x = x >> cacheLineBits" by (simp add: lineIndex_def lineStart_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lineIndex x = x >> cacheLineBits
theory Machine_C

lemma lineIndex_le_mono:
  "x \<le> y \<Longrightarrow> lineIndex x \<le> lineIndex y" by (clarsimp simp: lineIndex_def2 cacheLineBits_def le_shiftr)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> lineIndex x \<le> lineIndex y
theory Machine_C

lemma lineIndex_lineStart_diff:
  "w1 \<le> w2 \<Longrightarrow> (unat (lineStart w2 - lineStart w1) div 32) = unat (lineIndex w2 - lineIndex w1)" apply (subst shiftr_div_2n'[symmetric, where n=5, simplified]) apply (drule lineStart_le_mono) apply (drule sub_right_shift[OF lineStart_mask lineStart_mask]) apply (simp add: lineIndex_def cacheLineBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w1 \<le> w2 \<Longrightarrow> unat (lineStart w2 - lineStart w1) div 32 = unat (lineIndex w2 - lineIndex w1) proof (prove)
goal (1 subgoal):
 1. w1 \<le> w2 \<Longrightarrow> unat (lineStart w2 - lineStart w1 >> 5) = unat (lineIndex w2 - lineIndex w1) proof (prove)
goal (1 subgoal):
 1. lineStart w1 \<le> lineStart w2 \<Longrightarrow> unat (lineStart w2 - lineStart w1 >> 5) = unat (lineIndex w2 - lineIndex w1) proof (prove)
goal (1 subgoal):
 1. lineStart w2 - lineStart w1 >> 5 = (lineStart w2 >> 5) - (lineStart w1 >> 5) \<Longrightarrow> unat (lineStart w2 - lineStart w1 >> 5) = unat (lineIndex w2 - lineIndex w1) proof (prove)
goal:
No subgoals!
theory Machine_C

lemma lineStart_eq_minus_mask:
  "lineStart w1 = w1 - (w1 && mask 5)" by (simp add: lineStart_def cacheLineBits_def mask_out_sub_mask[symmetric] and_not_mask)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lineStart w1 = w1 - (w1 && mask 5)
theory Machine_C

lemma lineStart_idem[simp]:
  "lineStart (lineStart x) = lineStart x" by (simp add: lineStart_def cacheLineBits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lineStart (lineStart x) = lineStart x
theory Machine_C

lemma cache_range_lineIndex_helper:
  "lineIndex w1 + of_nat n << 5 = w1 - (w1 && mask 5) + of_nat n * 0x20" apply (clarsimp simp: lineIndex_def cacheLineBits_def word_shiftl_add_distrib lineStart_def[symmetric, unfolded cacheLineBits_def] lineStart_eq_minus_mask[symmetric]) apply (simp add: shiftl_t2n) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lineIndex w1 + word_of_nat n << 5 = w1 - (w1 && mask 5) + word_of_nat n * 0x20 proof (prove)
goal (1 subgoal):
 1. word_of_nat n << 5 = word_of_nat n * 0x20 proof (prove)
goal:
No subgoals!
theory Machine_C

lemma dmo_if:
  "(doMachineOp (if a then b else c)) = (if a then (doMachineOp b) else (doMachineOp c))" by (simp split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. doMachineOp (if a then b else c) = (if a then doMachineOp b else doMachineOp c)
theory Machine_C

lemma writeTTBR0Ptr_ccorres:
  "ccorres dc xfdc \<top> (UNIV \<inter> \<lbrace>\<acute>addr = pd\<rbrace>) hs
           (doMachineOp (writeTTBR0Ptr pd))
           (Call writeTTBR0Ptr_'proc)" apply (cinit' lift: addr_' simp: writeTTBR0Ptr_def fromPAddr_def) apply (ctac (no_vcg) add: writeTTBR0_ccorres) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>_. True) (UNIV \<inter> \<lbrace>\<acute>addr = pd\<rbrace>) hs (doMachineOp (writeTTBR0Ptr pd)) (Call writeTTBR0Ptr_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>addr. addr = pd \<Longrightarrow> ccorres dc xfdc (?Q30 addr) (?Q'30 addr) (SKIP # hs) (doMachineOp (writeTTBR0 (pd && 0xFFFFE000 || 0x18))) (CALL writeTTBR0_'proc(addr && UCAST(32 \<rightarrow> 32) 0xFFFFE000 || SCAST(32 signed \<rightarrow> 32) 0x18))
 2. \<And>addr s s'. \<lbrakk>addr = pd; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q30 addr s \<and> s' \<in> ?Q'30 addr proof (prove)
goal (1 subgoal):
 1. \<And>addr s s'. \<lbrakk>addr = pd; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> True \<and> s' \<in> {s. val_'_update (\<lambda>_. addr && UCAST(32 \<rightarrow> 32) 0xFFFFE000 || SCAST(32 signed \<rightarrow> 32) 0x18) s \<in> \<lbrace>\<acute>val = pd && 0xFFFFE000 || 0x18\<rbrace>} proof (prove)
goal:
No subgoals!
theory CSpace_C

lemma wordFromVMRights_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s} Call wordFromVMRights_'proc \<lbrace>\<acute>ret__unsigned_long = \<^bsup>s\<^esup>vm_rights\<rbrace>" by vcg simp?

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call wordFromVMRights_'proc \<lbrace>\<acute>ret__unsigned_long = \<^bsup>s\<^esup>vm_rights\<rbrace>
theory CSpace_C

lemma vmRightsFromWord_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s} Call vmRightsFromWord_'proc \<lbrace>\<acute>ret__unsigned_long = \<^bsup>s\<^esup>w\<rbrace>" by vcg simp?

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call vmRightsFromWord_'proc \<lbrace>\<acute>ret__unsigned_long = \<^bsup>s\<^esup>w\<rbrace>
theory CSpace_C

lemma small_frame_cap_rights [simp]:
  "cap_get_tag cap = scast cap_small_frame_cap
  \<Longrightarrow> cap_small_frame_cap_CL.capFVMRights_CL (cap_small_frame_cap_lift cap) && mask 2 =
     cap_small_frame_cap_CL.capFVMRights_CL (cap_small_frame_cap_lift cap)" apply (simp add: cap_small_frame_cap_lift_def) by (simp add: cap_lift_def cap_tag_defs mask_def word_bw_assocs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<Longrightarrow> cap_small_frame_cap_CL.capFVMRights_CL (cap_small_frame_cap_lift cap) && mask 2 = cap_small_frame_cap_CL.capFVMRights_CL (cap_small_frame_cap_lift cap) proof (prove)
goal (1 subgoal):
 1. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<Longrightarrow> cap_small_frame_cap_CL.capFVMRights_CL (case cap_lift cap of Some (Cap_small_frame_cap rec) \<Rightarrow> rec) && mask 2 = cap_small_frame_cap_CL.capFVMRights_CL (case cap_lift cap of Some (Cap_small_frame_cap rec) \<Rightarrow> rec)
theory CSpace_C

lemma frame_cap_rights [simp]:
  "cap_get_tag cap = scast cap_frame_cap
  \<Longrightarrow> cap_frame_cap_CL.capFVMRights_CL (cap_frame_cap_lift cap) && mask 2 =
     cap_frame_cap_CL.capFVMRights_CL (cap_frame_cap_lift cap)" apply (simp add: cap_frame_cap_lift_def) by (simp add: cap_lift_def cap_tag_defs mask_def word_bw_assocs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<Longrightarrow> cap_frame_cap_CL.capFVMRights_CL (cap_frame_cap_lift cap) && mask 2 = cap_frame_cap_CL.capFVMRights_CL (cap_frame_cap_lift cap) proof (prove)
goal (1 subgoal):
 1. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<Longrightarrow> cap_frame_cap_CL.capFVMRights_CL (case cap_lift cap of Some (Cap_frame_cap rec) \<Rightarrow> rec) && mask 2 = cap_frame_cap_CL.capFVMRights_CL (case cap_lift cap of Some (Cap_frame_cap rec) \<Rightarrow> rec)
theory CSpace_C

lemma to_bool_cap_rights_bf:
  "to_bool (capAllowRead_CL (seL4_CapRights_lift R)) =
   to_bool_bf (capAllowRead_CL (seL4_CapRights_lift R))"
  "to_bool (capAllowWrite_CL (seL4_CapRights_lift R)) =
   to_bool_bf (capAllowWrite_CL (seL4_CapRights_lift R))"
  "to_bool (capAllowGrant_CL (seL4_CapRights_lift R)) =
   to_bool_bf (capAllowGrant_CL (seL4_CapRights_lift R))"
  "to_bool (capAllowGrantReply_CL (seL4_CapRights_lift R)) =
   to_bool_bf (capAllowGrantReply_CL (seL4_CapRights_lift R))" by (subst to_bool_bf_to_bool_mask,
      simp add: seL4_CapRights_lift_def mask_def word_bw_assocs, simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (to_bool (capAllowRead_CL (seL4_CapRights_lift R)) = to_bool_bf (capAllowRead_CL (seL4_CapRights_lift R)) &&& to_bool (capAllowWrite_CL (seL4_CapRights_lift R)) = to_bool_bf (capAllowWrite_CL (seL4_CapRights_lift R))) &&& to_bool (capAllowGrant_CL (seL4_CapRights_lift R)) = to_bool_bf (capAllowGrant_CL (seL4_CapRights_lift R)) &&& to_bool (capAllowGrantReply_CL (seL4_CapRights_lift R)) = to_bool_bf (capAllowGrantReply_CL (seL4_CapRights_lift R))
theory CSpace_C

lemma to_bool_ntfn_cap_bf:
  "cap_lift c = Some (Cap_notification_cap cap) \<Longrightarrow>
  to_bool (capNtfnCanSend_CL cap) = to_bool_bf (capNtfnCanSend_CL cap) \<and>
  to_bool (capNtfnCanReceive_CL cap) = to_bool_bf (capNtfnCanReceive_CL cap)" apply (simp add:cap_lift_def Let_def split: if_split_asm) apply (subst to_bool_bf_to_bool_mask,
         clarsimp simp: cap_lift_thread_cap mask_def word_bw_assocs)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_lift c = Some (Cap_notification_cap cap) \<Longrightarrow> to_bool (capNtfnCanSend_CL cap) = to_bool_bf (capNtfnCanSend_CL cap) \<and> to_bool (capNtfnCanReceive_CL cap) = to_bool_bf (capNtfnCanReceive_CL cap) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_notification_cap \<noteq> cap_null_cap; cap_notification_cap \<noteq> cap_untyped_cap; cap_notification_cap \<noteq> cap_endpoint_cap; cap_get_tag c = SCAST(32 signed \<rightarrow> 32) cap_notification_cap; \<lparr>capNtfnBadge_CL = (cap_C.words_C c.[Suc 0] >> 4) && mask 28, capNtfnCanReceive_CL = (cap_C.words_C c.[Suc 0] >> Suc 0) && 1, capNtfnCanSend_CL = cap_C.words_C c.[Suc 0] && 1, capNtfnPtr_CL = cap_C.words_C c.[0] && ~~ mask 4\<rparr> = cap\<rbrakk> \<Longrightarrow> to_bool (capNtfnCanSend_CL cap) = to_bool_bf (capNtfnCanSend_CL cap) \<and> to_bool (capNtfnCanReceive_CL cap) = to_bool_bf (capNtfnCanReceive_CL cap) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_notification_cap \<noteq> cap_null_cap; cap_notification_cap \<noteq> cap_untyped_cap; cap_notification_cap \<noteq> cap_endpoint_cap; cap_get_tag c = SCAST(32 signed \<rightarrow> 32) cap_notification_cap; \<lparr>capNtfnBadge_CL = (cap_C.words_C c.[Suc 0] >> 4) && mask 28, capNtfnCanReceive_CL = (cap_C.words_C c.[Suc 0] >> Suc 0) && 1, capNtfnCanSend_CL = cap_C.words_C c.[Suc 0] && 1, capNtfnPtr_CL = cap_C.words_C c.[0] && ~~ mask 4\<rparr> = cap\<rbrakk> \<Longrightarrow> to_bool (capNtfnCanSend_CL cap) = to_bool (capNtfnCanSend_CL cap) \<and> to_bool (capNtfnCanReceive_CL cap) = to_bool (capNtfnCanReceive_CL cap) proof (prove)
goal:
No subgoals!
theory CSpace_C

lemma to_bool_reply_cap_bf:
  "cap_lift c = Some (Cap_reply_cap cap)
   \<Longrightarrow> to_bool (capReplyMaster_CL cap) = to_bool_bf (capReplyMaster_CL cap)
      \<and> to_bool (capReplyCanGrant_CL cap) = to_bool_bf (capReplyCanGrant_CL cap)" apply (simp add: cap_lift_def Let_def split: if_split_asm) apply (subst to_bool_bf_to_bool_mask,
         clarsimp simp: cap_lift_thread_cap mask_def word_bw_assocs)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_lift c = Some (Cap_reply_cap cap) \<Longrightarrow> to_bool (capReplyMaster_CL cap) = to_bool_bf (capReplyMaster_CL cap) \<and> to_bool (capReplyCanGrant_CL cap) = to_bool_bf (capReplyCanGrant_CL cap) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_reply_cap \<noteq> cap_null_cap; cap_reply_cap \<noteq> cap_untyped_cap; cap_reply_cap \<noteq> cap_endpoint_cap; cap_reply_cap \<noteq> cap_notification_cap; cap_get_tag c = SCAST(32 signed \<rightarrow> 32) cap_reply_cap; \<lparr>capReplyCanGrant_CL = (cap_C.words_C c.[0] >> 5) && 1, capReplyMaster_CL = (cap_C.words_C c.[0] >> 4) && 1, capTCBPtr_CL = cap_C.words_C c.[0] && ~~ mask 6\<rparr> = cap\<rbrakk> \<Longrightarrow> to_bool (capReplyMaster_CL cap) = to_bool_bf (capReplyMaster_CL cap) \<and> to_bool (capReplyCanGrant_CL cap) = to_bool_bf (capReplyCanGrant_CL cap) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_reply_cap \<noteq> cap_null_cap; cap_reply_cap \<noteq> cap_untyped_cap; cap_reply_cap \<noteq> cap_endpoint_cap; cap_reply_cap \<noteq> cap_notification_cap; cap_get_tag c = SCAST(32 signed \<rightarrow> 32) cap_reply_cap; \<lparr>capReplyCanGrant_CL = (cap_C.words_C c.[0] >> 5) && 1, capReplyMaster_CL = (cap_C.words_C c.[0] >> 4) && 1, capTCBPtr_CL = cap_C.words_C c.[0] && ~~ mask 6\<rparr> = cap\<rbrakk> \<Longrightarrow> to_bool (capReplyMaster_CL cap) = to_bool (capReplyMaster_CL cap) \<and> to_bool (capReplyCanGrant_CL cap) = to_bool (capReplyCanGrant_CL cap) proof (prove)
goal:
No subgoals!
theory CSpace_C

lemma to_bool_ep_cap_bf:
  "cap_lift c = Some (Cap_endpoint_cap cap) \<Longrightarrow>
  to_bool (capCanSend_CL cap) = to_bool_bf (capCanSend_CL cap) \<and>
  to_bool (capCanReceive_CL cap) = to_bool_bf (capCanReceive_CL cap) \<and>
  to_bool (capCanGrant_CL cap) = to_bool_bf (capCanGrant_CL cap) \<and>
  to_bool (capCanGrantReply_CL cap) = to_bool_bf (capCanGrantReply_CL cap)" apply (simp add:cap_lift_def Let_def split: if_split_asm) apply (subst to_bool_bf_to_bool_mask,
         clarsimp simp: cap_lift_thread_cap mask_def word_bw_assocs)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_lift c = Some (Cap_endpoint_cap cap) \<Longrightarrow> to_bool (capCanSend_CL cap) = to_bool_bf (capCanSend_CL cap) \<and> to_bool (capCanReceive_CL cap) = to_bool_bf (capCanReceive_CL cap) \<and> to_bool (capCanGrant_CL cap) = to_bool_bf (capCanGrant_CL cap) \<and> to_bool (capCanGrantReply_CL cap) = to_bool_bf (capCanGrantReply_CL cap) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_endpoint_cap \<noteq> cap_null_cap; cap_endpoint_cap \<noteq> cap_untyped_cap; cap_get_tag c = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap; \<lparr>capEPBadge_CL = (cap_C.words_C c.[0] >> 4) && mask 28, capCanGrantReply_CL = (cap_C.words_C c.[Suc 0] >> 3) && 1, capCanGrant_CL = (cap_C.words_C c.[Suc 0] >> 2) && 1, capCanSend_CL = cap_C.words_C c.[Suc 0] && 1, capCanReceive_CL = (cap_C.words_C c.[Suc 0] >> Suc 0) && 1, capEPPtr_CL = cap_C.words_C c.[Suc 0] && ~~ mask 4\<rparr> = cap\<rbrakk> \<Longrightarrow> to_bool (capCanSend_CL cap) = to_bool_bf (capCanSend_CL cap) \<and> to_bool (capCanReceive_CL cap) = to_bool_bf (capCanReceive_CL cap) \<and> to_bool (capCanGrant_CL cap) = to_bool_bf (capCanGrant_CL cap) \<and> to_bool (capCanGrantReply_CL cap) = to_bool_bf (capCanGrantReply_CL cap) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_endpoint_cap \<noteq> cap_null_cap; cap_endpoint_cap \<noteq> cap_untyped_cap; cap_get_tag c = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap; \<lparr>capEPBadge_CL = (cap_C.words_C c.[0] >> 4) && mask 28, capCanGrantReply_CL = (cap_C.words_C c.[Suc 0] >> 3) && 1, capCanGrant_CL = (cap_C.words_C c.[Suc 0] >> 2) && 1, capCanSend_CL = cap_C.words_C c.[Suc 0] && 1, capCanReceive_CL = (cap_C.words_C c.[Suc 0] >> Suc 0) && 1, capEPPtr_CL = cap_C.words_C c.[Suc 0] && ~~ mask 4\<rparr> = cap\<rbrakk> \<Longrightarrow> to_bool (capCanSend_CL cap) = to_bool (capCanSend_CL cap) \<and> to_bool (capCanReceive_CL cap) = to_bool (capCanReceive_CL cap) \<and> to_bool (capCanGrant_CL cap) = to_bool (capCanGrant_CL cap) \<and> to_bool (capCanGrantReply_CL cap) = to_bool (capCanGrantReply_CL cap) proof (prove)
goal:
No subgoals!
theory CSpace_C

lemma isArchCap_spec:
  "\<forall>s. \<Gamma>\<turnstile> {s} Call isArchCap_'proc \<lbrace>\<acute>ret__unsigned_long = from_bool (isArchCap_tag (cap_get_tag (cap_' s)))\<rbrace>" apply vcg apply (clarsimp simp: from_bool_def isArchCap_tag_def bool.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call isArchCap_'proc \<lbrace>\<acute>ret__unsigned_long = from_bool (isArchCap_tag (cap_get_tag \<^bsup>s\<^esup>cap))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<forall>ret__unsigned. ret__unsigned = cap_get_tag cap \<longrightarrow> 2 \<noteq> 0 \<and> UCAST(32 \<rightarrow> 32) (cap_get_tag cap mod SCAST(32 signed \<rightarrow> 32) 2) = from_bool (isArchCap_tag (cap_get_tag cap)) proof (prove)
goal:
No subgoals!
theory CSpace_C

lemma heap_update_field_ext:
  "\<lbrakk>field_ti TYPE('a :: packed_type) f = Some t; c_guard p;
  export_uinfo t = export_uinfo (typ_info_t TYPE('b :: packed_type))\<rbrakk>
  \<Longrightarrow> heap_update (Ptr &(p\<rightarrow>f) :: 'b ptr) =
  (\<lambda>v hp. heap_update p (update_ti t (to_bytes_p v) (h_val hp p)) hp)" apply (rule ext, rule ext) apply (erule (2) heap_update_field) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>field_ti TYPE('a) f = Some t; c_guard p; export_uinfo t = export_uinfo (typ_info_t TYPE('b))\<rbrakk> \<Longrightarrow> heap_update (PTR('b) &(p\<rightarrow>f)) = (\<lambda>v hp. heap_update p (update_ti t (to_bytes_p v) (h_val hp p)) hp) proof (prove)
goal (1 subgoal):
 1. \<And>v hp. \<lbrakk>field_ti TYPE('a) f = Some t; c_guard p; export_uinfo t = export_uinfo (typ_info_t TYPE('b))\<rbrakk> \<Longrightarrow> heap_update (PTR('b) &(p\<rightarrow>f)) v hp = heap_update p (update_ti t (to_bytes_p v) (h_val hp p)) hp proof (prove)
goal:
No subgoals!
theory CSpace_C

lemma Arch_isCapRevocable_spec:
  "\<forall>s. \<Gamma>\<turnstile> {\<sigma>. s = \<sigma> \<and> True}
          Call Arch_isCapRevocable_'proc
        {t. \<forall>c c'.  ccap_relation c (derivedCap_' s) \<and> ccap_relation c' (srcCap_' s)
            \<longrightarrow> ret__unsigned_long_' t = from_bool (Arch.isCapRevocable c c')}" apply vcg by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. True\<rbrace> Call Arch_isCapRevocable_'proc \<lbrace>\<forall>c c'. ccap_relation c \<^bsup>s\<^esup>derivedCap \<and> ccap_relation c' \<^bsup>s\<^esup>srcCap \<longrightarrow> \<acute>ret__unsigned_long = from_bool (Arch.isCapRevocable c c')\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>derivedCap srcCap. True \<Longrightarrow> \<forall>c c'. ccap_relation c derivedCap \<and> ccap_relation c' srcCap \<longrightarrow> SCAST(32 signed \<rightarrow> 32) false = from_bool (Arch.isCapRevocable c c')
theory CSpace_C

lemma ccorres_updateMDB_skip:
  "ccorres dc xfdc (\<top> and (\<lambda>_. n = 0)) UNIV hs (updateMDB n f) SKIP" unfolding updateMDB_def apply (rule ccorres_gen_asm) apply simp apply (rule ccorres_return) apply simp apply vcg done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc ((\<lambda>_. True) and (\<lambda>_. n = 0)) UNIV hs (updateMDB n f) SKIP proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc ((\<lambda>_. True) and (\<lambda>_. n = 0)) UNIV hs (let slot = n in if slot = 0 then return () else do cte <- getCTE slot;
mdb <- return (cteMDBNode cte);
mdb' <- return (f mdb);
return (cteMDBNode_update (\<lambda>_. mdb') cte) >>= setCTE slot
od) SKIP proof (prove)
goal (1 subgoal):
 1. n = 0 \<Longrightarrow> ccorres dc xfdc (\<lambda>_. True) UNIV hs (let slot = n in if slot = 0 then return () else do cte <- getCTE slot;
mdb <- return (cteMDBNode cte);
mdb' <- return (f mdb);
return (cteMDBNode_update (\<lambda>_. mdb') cte) >>= setCTE slot
od) SKIP proof (prove)
goal (1 subgoal):
 1. n = 0 \<Longrightarrow> ccorres dc xfdc (\<lambda>_. True) UNIV hs (return ()) SKIP proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>n = 0; True\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (UNIV \<inter> {s'. (s, s') \<in> rf_sr}) SKIP {s'. (s, s') \<in> rf_sr \<and> dc () (xfdc s')} proof (prove)
goal (1 subgoal):
 1. \<And>s. n = 0 \<Longrightarrow> \<Gamma>\<turnstile> {s'. (s, s') \<in> rf_sr} SKIP {s'. (s, s') \<in> rf_sr} proof (prove)
goal:
No subgoals!
theory CSpace_C

lemma setUntypedCapAsFull_cte_at_wp [wp]:
  "\<lbrace> cte_at' x \<rbrace> setUntypedCapAsFull rvb cap src \<lbrace> \<lambda>_. cte_at' x \<rbrace>" apply (clarsimp simp: setUntypedCapAsFull_def) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>_. True) x\<rbrace> setUntypedCapAsFull rvb cap src \<lbrace>\<lambda>_. cte_wp_at' (\<lambda>_. True) x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isUntypedCap rvb; isUntypedCap cap; capPtr rvb = capPtr cap; capBlockSize rvb = capBlockSize cap\<rbrakk> \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>_. True) x\<rbrace> updateCap src (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) rvb) \<lbrace>\<lambda>_. cte_wp_at' (\<lambda>_. True) x\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_C

lemma valid_cap_untyped_inv:
  "valid_cap' (UntypedCap d r n f) s \<Longrightarrow>
    n \<ge> minUntypedSizeBits \<and> is_aligned (of_nat f :: word32) minUntypedSizeBits
      \<and> n \<le> maxUntypedSizeBits \<and> n < word_bits" apply (clarsimp simp:valid_cap'_def capAligned_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_cap' (capability.UntypedCap d r n f) s \<Longrightarrow> minUntypedSizeBits \<le> n \<and> is_aligned (word_of_nat f) minUntypedSizeBits \<and> n \<le> maxUntypedSizeBits \<and> n < word_bits proof (prove)
goal:
No subgoals!