kings-crown/FVELER_Isabelle huggingface dataset:
theory Ipc_R

lemma lookup_cap_to'[wp]:
  "\<lbrace>\<top>\<rbrace> lookupCap t cref \<lbrace>\<lambda>rv s. \<forall>r\<in>cte_refs' rv (irq_node' s). ex_cte_cap_to' r s\<rbrace>,-" by (simp add: lookupCap_def lookupCapAndSlot_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> lookupCap t cref \<lbrace>\<lambda>rv s. \<forall>r\<in>cte_refs' rv (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s\<rbrace>, -
theory Ipc_R

lemma grs_cap_to'[wp]:
  "\<lbrace>\<top>\<rbrace> getReceiveSlots t buf \<lbrace>\<lambda>rv s. \<forall>x \<in> set rv. ex_cte_cap_to' x s\<rbrace>" apply (cases buf; simp add: getReceiveSlots_def split_def unlessE_def) apply (wp, simp) apply (wp | simp | rule hoare_drop_imps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> getReceiveSlots t buf \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. ex_cte_cap_wp_to' (\<lambda>_. True) x s\<rbrace> proof (prove)
goal (2 subgoals):
 1. buf = None \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return [] \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. ex_cte_cap_wp_to' (\<lambda>_. True) x s\<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. \<forall>x\<in>set rv. ex_cte_cap_wp_to' (\<lambda>_. True) x s\<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. \<forall>x\<in>set rv. ex_cte_cap_wp_to' (\<lambda>_. True) x s\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma grs_length'[wp]:
  "\<lbrace>\<lambda>s. 1 \<le> n\<rbrace> getReceiveSlots receiver recv_buf \<lbrace>\<lambda>rv s. length rv \<le> n\<rbrace>" apply (simp add: getReceiveSlots_def split_def unlessE_def) apply (rule hoare_pre) apply (wp | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. 1 \<le> n\<rbrace> getReceiveSlots receiver recv_buf \<lbrace>\<lambda>rv s. length rv \<le> n\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Suc 0 \<le> n\<rbrace> case recv_buf of None \<Rightarrow> return [] | Some buffer \<Rightarrow> do ct <- loadCapTransfer buffer;
emptyOnFailure (doE cnode <- unifyFailure (lookupCap receiver (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. length rv \<le> n\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q4\<rbrace> case recv_buf of None \<Rightarrow> return [] | Some buffer \<Rightarrow> do ct <- loadCapTransfer buffer;
emptyOnFailure (doE cnode <- unifyFailure (lookupCap receiver (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. length rv \<le> n\<rbrace>
 2. \<And>s. Suc 0 \<le> n \<Longrightarrow> ?Q4 s proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma transferCaps_invs' [wp]:
  "\<lbrace>invs' and transferCaps_srcs caps\<rbrace>
    transferCaps mi caps ep receiver recv_buf
   \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (simp add: transferCaps_def Let_def split_def) apply (wp get_rs_cte_at' hoare_vcg_const_Ball_lift
             | wpcw | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)\<rbrace> transferCaps mi caps ep receiver recv_buf \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)\<rbrace> do destSlots <- getReceiveSlots receiver recv_buf;
case recv_buf of None \<Rightarrow> return (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) mi)) | Some rcvBuffer \<Rightarrow> transferCapsToSlots ep rcvBuffer 0 caps destSlots (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) mi))
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma get_mrs_inv'[wp]:
  "\<lbrace>P\<rbrace> getMRs t buf info \<lbrace>\<lambda>rv. P\<rbrace>" by (simp add: getMRs_def load_word_offs_def getRegister_def
          | wp dmo_inv' loadWord_inv mapM_wp'
            asUser_inv det_mapM[where S=UNIV] | wpc)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> getMRs t buf info \<lbrace>\<lambda>rv. P\<rbrace>
theory Ipc_R

lemma copyMRs_typ_at':
  "\<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> copyMRs s sb r rb n \<lbrace>\<lambda>rv s. P (typ_at' T p s)\<rbrace>" by (simp add: copyMRs_def | wp mapM_wp [where S=UNIV, simplified] | wpc)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> copyMRs s sb r rb n \<lbrace>\<lambda>rv s. P (typ_at' T p s)\<rbrace>
theory Ipc_R

lemma set_mrs_valid_objs' [wp]:
  "\<lbrace>valid_objs'\<rbrace> setMRs t a msgs \<lbrace>\<lambda>rv. valid_objs'\<rbrace>" apply (simp add: setMRs_def zipWithM_x_mapM split_def) apply (wp asUser_valid_objs crunch_wps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> setMRs t a msgs \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> do y <- asUser t (do _ <- mapM (\<lambda>p. setRegister (fst p) (snd p)) (zip TCB_H.msgRegisters (take (min (length msgs) (length TCB_H.msgRegisters + length (case a of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))) msgs));
return ()
od);
_ <- mapM (\<lambda>p. storeWordUser (fst p) (snd p)) (zip (case a of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) (drop (length TCB_H.msgRegisters) (take (min (length msgs) (length TCB_H.msgRegisters + length (case a of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))) msgs)));
return (word_of_nat (min (length msgs) (length TCB_H.msgRegisters + length (case a of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))))
od \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma setMRs_invs_bits[wp]:
  "\<lbrace>valid_pspace'\<rbrace> setMRs t buf mrs \<lbrace>\<lambda>rv. valid_pspace'\<rbrace>"
  "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace>
     setMRs t buf mrs \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>"
  "\<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
     setMRs t buf mrs \<lbrace>\<lambda>rv s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>"
  "\<lbrace>Invariants_H.valid_queues\<rbrace> setMRs t buf mrs \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace>"
  "\<lbrace>valid_queues'\<rbrace> setMRs t buf mrs \<lbrace>\<lambda>rv. valid_queues'\<rbrace>"
  "\<lbrace>\<lambda>s. P (state_refs_of' s)\<rbrace>
     setMRs t buf mrs
   \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace>"
  "\<lbrace>if_live_then_nonz_cap'\<rbrace> setMRs t buf mrs \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>"
  "\<lbrace>ex_nonz_cap_to' p\<rbrace> setMRs t buf mrs \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace>"
  "\<lbrace>cur_tcb'\<rbrace> setMRs t buf mrs \<lbrace>\<lambda>rv. cur_tcb'\<rbrace>"
  "\<lbrace>if_unsafe_then_cap'\<rbrace> setMRs t buf mrs \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace>" by (simp add: setMRs_def zipWithM_x_mapM split_def storeWordUser_def | wp crunch_wps)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<lbrace>valid_pspace'\<rbrace> setMRs t buf mrs \<lbrace>\<lambda>rv. valid_pspace'\<rbrace> &&& \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> setMRs t buf mrs \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>) &&& \<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> setMRs t buf mrs \<lbrace>\<lambda>rv s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> &&& \<lbrace>Invariants_H.valid_queues\<rbrace> setMRs t buf mrs \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace> &&& \<lbrace>valid_queues'\<rbrace> setMRs t buf mrs \<lbrace>\<lambda>rv. valid_queues'\<rbrace>) &&& (\<lbrace>\<lambda>s. P (state_refs_of' s)\<rbrace> setMRs t buf mrs \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace> &&& \<lbrace>if_live_then_nonz_cap'\<rbrace> setMRs t buf mrs \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>) &&& \<lbrace>ex_nonz_cap_to' p\<rbrace> setMRs t buf mrs \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace> &&& \<lbrace>cur_tcb'\<rbrace> setMRs t buf mrs \<lbrace>\<lambda>rv. cur_tcb'\<rbrace> &&& \<lbrace>if_unsafe_then_cap'\<rbrace> setMRs t buf mrs \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace>
theory Ipc_R

lemma copyMRs_invs_bits[wp]:
  "\<lbrace>valid_pspace'\<rbrace> copyMRs s sb r rb n \<lbrace>\<lambda>rv. valid_pspace'\<rbrace>"
  "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> copyMRs s sb r rb n
      \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>"
  "\<lbrace>Invariants_H.valid_queues\<rbrace> copyMRs s sb r rb n \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace>"
  "\<lbrace>valid_queues'\<rbrace> copyMRs s sb r rb n \<lbrace>\<lambda>rv. valid_queues'\<rbrace>"
  "\<lbrace>\<lambda>s. P (state_refs_of' s)\<rbrace>
      copyMRs s sb r rb n
   \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace>"
  "\<lbrace>if_live_then_nonz_cap'\<rbrace> copyMRs s sb r rb n \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>"
  "\<lbrace>ex_nonz_cap_to' p\<rbrace> copyMRs s sb r rb n \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace>"
  "\<lbrace>cur_tcb'\<rbrace> copyMRs s sb r rb n \<lbrace>\<lambda>rv. cur_tcb'\<rbrace>"
  "\<lbrace>if_unsafe_then_cap'\<rbrace> copyMRs s sb r rb n \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace>" by (simp add: copyMRs_def  storeWordUser_def | wp mapM_wp' | wpc)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<lbrace>valid_pspace'\<rbrace> copyMRs s sb r rb n \<lbrace>\<lambda>rv. valid_pspace'\<rbrace> &&& \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> copyMRs s sb r rb n \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>) &&& \<lbrace>Invariants_H.valid_queues\<rbrace> copyMRs s sb r rb n \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace> &&& \<lbrace>valid_queues'\<rbrace> copyMRs s sb r rb n \<lbrace>\<lambda>rv. valid_queues'\<rbrace>) &&& (\<lbrace>\<lambda>s. P (state_refs_of' s)\<rbrace> copyMRs s sb r rb n \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace> &&& \<lbrace>if_live_then_nonz_cap'\<rbrace> copyMRs s sb r rb n \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>) &&& \<lbrace>ex_nonz_cap_to' p\<rbrace> copyMRs s sb r rb n \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace> &&& \<lbrace>cur_tcb'\<rbrace> copyMRs s sb r rb n \<lbrace>\<lambda>rv. cur_tcb'\<rbrace> &&& \<lbrace>if_unsafe_then_cap'\<rbrace> copyMRs s sb r rb n \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace>
theory Ipc_R

lemma mi_map_length[simp]: "msgLength (message_info_map mi) = mi_length mi" by (cases mi, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. msgLength (message_info_map mi) = mi_length mi
theory Ipc_R

lemma invs_mdb_strengthen':
  "invs' s \<longrightarrow> valid_mdb' s" by auto

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

lemma lookupExtraCaps_length:
  "\<lbrace>\<lambda>s. unat (msgExtraCaps mi) \<le> n\<rbrace> lookupExtraCaps thread send_buf mi \<lbrace>\<lambda>rv s. length rv \<le> n\<rbrace>,-" apply (simp add: lookupExtraCaps_def getExtraCPtrs_def) apply (rule hoare_pre) apply (wp mapME_length | wpc)+ apply (clarsimp simp: upto_enum_step_def Suc_unat_diff_1 word_le_sub1) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. unat (msgExtraCaps mi) \<le> n\<rbrace> lookupExtraCaps thread send_buf mi \<lbrace>\<lambda>rv s. length rv \<le> n\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. unat (msgExtraCaps mi) \<le> n\<rbrace> liftE (case mi of Types_H.message_info.MI x count xa xb \<Rightarrow> do intSize <- return (fromIntegral wordSize);
case send_buf of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> do offset <- return (msgMaxLength + 1);
return (map (\<lambda>x. bufferPtr + PPtr ((x + offset) * intSize)) [1 , 2 .e. count]) >>= mapM (liftM CPtr \<circ> loadWordUser)
od
od) >>=E mapME (\<lambda>cptr. capFaultOnFailure cptr False (lookupCapAndSlot thread cptr)) \<lbrace>\<lambda>rv s. length rv \<le> n\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> liftE (case mi of Types_H.message_info.MI x count xa xb \<Rightarrow> do intSize <- return (fromIntegral wordSize);
case send_buf of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> do offset <- return (msgMaxLength + 1);
return (map (\<lambda>x. bufferPtr + PPtr ((x + offset) * intSize)) [1 , 2 .e. count]) >>= mapM (liftM CPtr \<circ> loadWordUser)
od
od) >>=E mapME (\<lambda>cptr. capFaultOnFailure cptr False (lookupCapAndSlot thread cptr)) \<lbrace>\<lambda>rv s. length rv \<le> n\<rbrace>, -
 2. \<And>s. unat (msgExtraCaps mi) \<le> n \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. unat (msgExtraCaps mi) \<le> n \<Longrightarrow> True \<and> (\<forall>x xa xb xc. mi = Types_H.message_info.MI x xa xb xc \<longrightarrow> (send_buf = None \<longrightarrow> length [] \<le> n) \<and> (\<forall>x. send_buf = Some x \<longrightarrow> length (map (\<lambda>xa. x + PPtr ((xa + (msgMaxLength + 1)) * fromIntegral wordSize)) [1 , 2 .e. xa]) \<le> n)) proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma getMessageInfo_msgExtraCaps[wp]:
  "\<lbrace>\<top>\<rbrace> getMessageInfo t \<lbrace>\<lambda>rv s. unat (msgExtraCaps rv) \<le> msgMaxExtraCaps\<rbrace>" apply (simp add: getMessageInfo_def) apply wp apply (simp add: messageInfoFromWord_def Let_def msgMaxExtraCaps_def
                    shiftL_nat) apply (subst nat_le_Suc_less_imp) apply (rule unat_less_power) apply (simp add: word_bits_def msgExtraCapBits_def) apply (rule and_mask_less'[unfolded mask_2pm1]) apply (simp add: msgExtraCapBits_def) apply wpsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> getMessageInfo t \<lbrace>\<lambda>rv s. unat (msgExtraCaps rv) \<le> msgMaxExtraCaps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do x <- asUser t (getRegister TCB_H.msgInfoRegister);
return (messageInfoFromWord x)
od \<lbrace>\<lambda>rv s. unat (msgExtraCaps rv) \<le> msgMaxExtraCaps\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> asUser t (getRegister TCB_H.msgInfoRegister) \<lbrace>\<lambda>x a. unat (msgExtraCaps (messageInfoFromWord x)) \<le> msgMaxExtraCaps\<rbrace>
 2. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> asUser t (getRegister TCB_H.msgInfoRegister) \<lbrace>\<lambda>x a. unat ((x >> msgLengthBits) && 2 ^ msgExtraCapBits - 1) \<le> 2 ^ msgExtraCapBits - Suc 0\<rbrace>
 2. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>a x. unat ((x >> msgLengthBits) && 2 ^ msgExtraCapBits - 1) < 2 ^ msgExtraCapBits
 2. \<lbrace>?Q\<rbrace> asUser t (getRegister TCB_H.msgInfoRegister) \<lbrace>\<lambda>x a. True\<rbrace>
 3. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>a x. msgExtraCapBits < LENGTH(32)
 2. \<And>a x. (x >> msgLengthBits) && 2 ^ msgExtraCapBits - 1 < 2 ^ msgExtraCapBits
 3. \<lbrace>?Q\<rbrace> asUser t (getRegister TCB_H.msgInfoRegister) \<lbrace>\<lambda>x a. True\<rbrace>
 4. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>a x. (x >> msgLengthBits) && 2 ^ msgExtraCapBits - 1 < 2 ^ msgExtraCapBits
 2. \<lbrace>?Q\<rbrace> asUser t (getRegister TCB_H.msgInfoRegister) \<lbrace>\<lambda>x a. True\<rbrace>
 3. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>a x. msgExtraCapBits < LENGTH(32)
 2. \<lbrace>?Q\<rbrace> asUser t (getRegister TCB_H.msgInfoRegister) \<lbrace>\<lambda>x a. True\<rbrace>
 3. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> asUser t (getRegister TCB_H.msgInfoRegister) \<lbrace>\<lambda>x a. True\<rbrace>
 2. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma copyMRs_valid_mdb[wp]:
  "\<lbrace>valid_mdb'\<rbrace> copyMRs t buf t' buf' n \<lbrace>\<lambda>rv. valid_mdb'\<rbrace>" by (simp add: valid_mdb'_def copyMRs_ctes_of)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_mdb'\<rbrace> copyMRs t buf t' buf' n \<lbrace>\<lambda>rv. valid_mdb'\<rbrace>
theory Ipc_R

lemma corres_liftE_lift:
  "corres r1 P P' m m' \<Longrightarrow>
  corres (f1 \<oplus> r1) P P' (liftE m) (withoutFailure m')" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres r1 P P' m m' \<Longrightarrow> corres (f1 \<oplus> r1) P P' (liftE m) (withoutFailure m')
theory Ipc_R

lemma doNormal_invs'[wp]:
  "\<lbrace>tcb_at' sender and tcb_at' receiver and invs'\<rbrace>
    doNormalTransfer sender send_buf ep badge
             can_grant receiver recv_buf \<lbrace>\<lambda>r. invs'\<rbrace>" apply (simp add: doNormalTransfer_def) apply (wp hoare_vcg_const_Ball_lift | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' sender and tcb_at' receiver and invs'\<rbrace> doNormalTransfer sender send_buf ep badge can_grant receiver recv_buf \<lbrace>\<lambda>r. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' sender and tcb_at' receiver and invs'\<rbrace> do tag <- getMessageInfo sender;
caps <- if can_grant then lookupExtraCaps sender send_buf tag <catch> const (return []) else return [];
msgTransferred <- copyMRs sender send_buf receiver recv_buf (msgLength tag);
tag' <- transferCaps tag caps ep receiver recv_buf;
y <- setMessageInfo receiver (msgLength_update (\<lambda>_. msgTransferred) tag');
asUser receiver (setRegister Notification_H.badgeRegister badge)
od \<lbrace>\<lambda>r. invs'\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma transferCaps_urz[wp]:
  "\<lbrace>untyped_ranges_zero' and valid_pspace'
      and (\<lambda>s. (\<forall>x\<in>set caps. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s))\<rbrace>
    transferCaps tag caps ep receiver recv_buf
  \<lbrace>\<lambda>r. untyped_ranges_zero'\<rbrace>" apply (simp add: transferCaps_def) apply (rule hoare_pre) apply (wp hoare_vcg_all_lift hoare_vcg_const_imp_lift
      | wpc
      | simp add: ball_conj_distrib)+ apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>untyped_ranges_zero' and valid_pspace' and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)\<rbrace> transferCaps tag caps ep receiver recv_buf \<lbrace>\<lambda>r. untyped_ranges_zero'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>untyped_ranges_zero' and valid_pspace' and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)\<rbrace> do destSlots <- getReceiveSlots receiver recv_buf;
case recv_buf of None \<Rightarrow> return (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) tag)) | Some rcvBuffer \<Rightarrow> transferCapsToSlots ep rcvBuffer 0 caps destSlots (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) tag))
od \<lbrace>\<lambda>r. untyped_ranges_zero'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do destSlots <- getReceiveSlots receiver recv_buf;
case recv_buf of None \<Rightarrow> return (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) tag)) | Some rcvBuffer \<Rightarrow> transferCapsToSlots ep rcvBuffer 0 caps destSlots (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) tag))
od \<lbrace>\<lambda>r. untyped_ranges_zero'\<rbrace>
 2. \<And>s. (untyped_ranges_zero' and valid_pspace' and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. untyped_ranges_zero' s \<and> valid_pspace' 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> (\<exists>x. recv_buf = Some x) \<longrightarrow> valid_objs' s proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma msgFromLookupFailure_map[simp]:
  "msgFromLookupFailure (lookup_failure_map lf)
     = msg_from_lookup_failure lf" by (cases lf, simp_all add: lookup_failure_map_def msgFromLookupFailure_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. msgFromLookupFailure (lookup_failure_map lf) = msg_from_lookup_failure lf
theory Ipc_R

lemma asUser_getRestartPC_corres:
  "corres (=) (tcb_at t) (tcb_at' t)
                 (as_user t getRestartPC) (asUser t getRestartPC)" apply (rule asUser_corres') apply (rule corres_Id, simp, simp) apply (rule no_fail_getRestartPC) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (tcb_at t) (tcb_at' t) (as_user t getRestartPC) (asUser t getRestartPC) proof (prove)
goal (1 subgoal):
 1. corres_underlying Id False True (=) (\<lambda>_. True) (\<lambda>_. True) getRestartPC getRestartPC proof (prove)
goal (1 subgoal):
 1. True \<Longrightarrow> no_fail (\<lambda>_. True) getRestartPC proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma asUser_mapM_getRegister_corres:
  "corres (=) (tcb_at t) (tcb_at' t)
     (as_user t (mapM getRegister regs))
     (asUser t (mapM getRegister regs))" apply (rule asUser_corres') apply (rule corres_Id [OF refl refl]) apply (rule no_fail_mapM) apply (simp add: getRegister_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (tcb_at t) (tcb_at' t) (as_user t (mapM getRegister regs)) (asUser t (mapM getRegister regs)) proof (prove)
goal (1 subgoal):
 1. corres_underlying Id False True (=) (\<lambda>_. True) (\<lambda>_. True) (mapM getRegister regs) (mapM getRegister regs) proof (prove)
goal (1 subgoal):
 1. True \<Longrightarrow> no_fail (\<lambda>_. True) (mapM getRegister regs) proof (prove)
goal (1 subgoal):
 1. True \<Longrightarrow> \<forall>x. no_fail (\<lambda>_. True) (getRegister x) proof (prove)
goal:
No subgoals!