kings-crown/FVELER_Isabelle huggingface dataset:
theory Ipc_R

lemma makeArchFaultMessage_corres:
  "corres (=) (tcb_at t) (tcb_at' t)
  (make_arch_fault_msg f t)
  (makeArchFaultMessage (arch_fault_map f) t)" apply (cases f, clarsimp simp: makeArchFaultMessage_def split: arch_fault.split) apply (rule corres_guard_imp) apply (rule corres_split_eqr[OF asUser_getRestartPC_corres]) apply (rule corres_trivial, simp add: arch_fault_map_def) apply (wp+, auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (tcb_at t) (tcb_at' t) (make_arch_fault_msg f t) (makeArchFaultMessage (arch_fault_map f) t) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. f = ARM_A.VMFault x1 x2 \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (do pc <- as_user t getRestartPC;
return (5, pc # x1 # x2)
od) (do pc <- asUser t getRestartPC;
return (5, pc # x1 # x2)
od) proof (prove)
goal (3 subgoals):
 1. \<And>x1 x2. f = ARM_A.VMFault x1 x2 \<Longrightarrow> corres (=) (?Q1 x1 x2) (?Q'1 x1 x2) (do pc <- as_user t getRestartPC;
return (5, pc # x1 # x2)
od) (do pc <- asUser t getRestartPC;
return (5, pc # x1 # x2)
od)
 2. \<And>x1 x2 s. \<lbrakk>f = ARM_A.VMFault x1 x2; tcb_at t s\<rbrakk> \<Longrightarrow> ?Q1 x1 x2 s
 3. \<And>x1 x2 s. \<lbrakk>f = ARM_A.VMFault x1 x2; tcb_at' t s\<rbrakk> \<Longrightarrow> ?Q'1 x1 x2 s proof (prove)
goal (5 subgoals):
 1. \<And>x1 x2 pc. f = ARM_A.VMFault x1 x2 \<Longrightarrow> corres (=) (?R5 x1 x2 pc) (?R'5 x1 x2 pc) (return (5, pc # x1 # x2)) (return (5, pc # x1 # x2))
 2. \<And>x1 x2. f = ARM_A.VMFault x1 x2 \<Longrightarrow> \<lbrace>?Q5 x1 x2\<rbrace> as_user t getRestartPC \<lbrace>?R5 x1 x2\<rbrace>
 3. \<And>x1 x2. f = ARM_A.VMFault x1 x2 \<Longrightarrow> \<lbrace>?Q'5 x1 x2\<rbrace> asUser t getRestartPC \<lbrace>?R'5 x1 x2\<rbrace>
 4. \<And>x1 x2 s. \<lbrakk>f = ARM_A.VMFault x1 x2; tcb_at t s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q5 x1 x2) s
 5. \<And>x1 x2 s. \<lbrakk>f = ARM_A.VMFault x1 x2; tcb_at' t s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'5 x1 x2) s proof (prove)
goal (4 subgoals):
 1. \<And>x1 x2. f = ARM_A.VMFault x1 x2 \<Longrightarrow> \<lbrace>?Q5 x1 x2\<rbrace> as_user t getRestartPC \<lbrace>\<lambda>pc _. True\<rbrace>
 2. \<And>x1 x2. f = ARM_A.VMFault x1 x2 \<Longrightarrow> \<lbrace>?Q'5 x1 x2\<rbrace> asUser t getRestartPC \<lbrace>\<lambda>pc _. True\<rbrace>
 3. \<And>x1 x2 s. \<lbrakk>f = ARM_A.VMFault x1 x2; tcb_at t s\<rbrakk> \<Longrightarrow> (tcb_at t and ?Q5 x1 x2) s
 4. \<And>x1 x2 s. \<lbrakk>f = ARM_A.VMFault x1 x2; tcb_at' t s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?Q'5 x1 x2) s proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma makeFaultMessage_inv[wp]:
  "\<lbrace>P\<rbrace> makeFaultMessage ft t \<lbrace>\<lambda>rv. P\<rbrace>" apply (cases ft, simp_all add: makeFaultMessage_def) apply (wp asUser_inv mapM_wp' det_mapM[where S=UNIV]
               det_getRestartPC getRestartPC_inv
             | clarsimp simp: getRegister_def makeArchFaultMessage_def
                        split: arch_fault.split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> makeFaultMessage ft t \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x11 x12. ft = Fault_H.fault.UserException x11 x12 \<Longrightarrow> \<lbrace>P\<rbrace> do msg <- asUser t (mapM getRegister FaultHandler_H.exceptionMessage);
return (3, msg @ [x11, x12])
od \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>x21 x22 x23. ft = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> \<lbrace>P\<rbrace> do pc <- asUser t getRestartPC;
return (1, pc # x21 # word_of_nat (fromEnum x22) # msgFromLookupFailure x23)
od \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<And>x3. ft = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>P\<rbrace> do msg <- asUser t (mapM getRegister FaultHandler_H.syscallMessage);
return (2, msg @ [x3])
od \<lbrace>\<lambda>rv. P\<rbrace>
 4. \<And>x4. ft = Fault_H.fault.ArchFault x4 \<Longrightarrow> \<lbrace>P\<rbrace> makeArchFaultMessage x4 t \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma doFaultTransfer_invs[wp]:
  "\<lbrace>invs' and tcb_at' receiver\<rbrace>
      doFaultTransfer badge sender receiver recv_buf
   \<lbrace>\<lambda>rv. invs'\<rbrace>" by (simp add: doFaultTransfer_def split_def | wp
    | clarsimp split: option.split)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' receiver\<rbrace> doFaultTransfer badge sender receiver recv_buf \<lbrace>\<lambda>rv. invs'\<rbrace>
theory Ipc_R

lemma valid_pspace_valid_objs'[elim!]:
  "valid_pspace' s \<Longrightarrow> valid_objs' s" by (simp add: valid_pspace'_def)

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

lemma lec_valid_cap' [wp]:
  "\<lbrace>valid_objs'\<rbrace> lookupExtraCaps thread xa mi \<lbrace>\<lambda>rv s. (\<forall>x\<in>set rv. s \<turnstile>' fst x)\<rbrace>, -" apply (rule hoare_pre, rule hoare_post_imp_R) apply (rule hoare_vcg_conj_lift_R[where R=valid_objs' and S="\<lambda>_. valid_objs'"]) apply (rule lookupExtraCaps_srcs) apply wp apply (clarsimp simp: cte_wp_at_ctes_of) apply (fastforce elim: ctes_of_valid') apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> lookupExtraCaps thread xa mi \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. valid_cap' (fst x) s\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'\<rbrace> lookupExtraCaps thread xa mi \<lbrace>?Q'3\<rbrace>, -
 2. \<And>rv s. ?Q'3 rv s \<Longrightarrow> \<forall>x\<in>set rv. valid_cap' (fst x) s
 3. \<And>s. valid_objs' s \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P6\<rbrace> lookupExtraCaps thread xa mi \<lbrace>?Q6\<rbrace>, -
 2. \<lbrace>valid_objs'\<rbrace> lookupExtraCaps thread xa mi \<lbrace>\<lambda>_. valid_objs'\<rbrace>, -
 3. \<And>rv s. ?Q6 rv s \<and> valid_objs' s \<Longrightarrow> \<forall>x\<in>set rv. valid_cap' (fst x) s
 4. \<And>s. valid_objs' s \<Longrightarrow> ?P6 s \<and> valid_objs' s proof (prove)
goal (3 subgoals):
 1. \<lbrace>valid_objs'\<rbrace> lookupExtraCaps thread xa mi \<lbrace>\<lambda>_. valid_objs'\<rbrace>, -
 2. \<And>rv s. (\<forall>x\<in>set rv. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) \<and> valid_objs' s \<Longrightarrow> \<forall>x\<in>set rv. valid_cap' (fst x) s
 3. \<And>s. valid_objs' s \<Longrightarrow> True \<and> valid_objs' s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. (\<forall>x\<in>set rv. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) \<and> valid_objs' s \<Longrightarrow> \<forall>x\<in>set rv. valid_cap' (fst x) s
 2. \<And>s. valid_objs' s \<Longrightarrow> True \<and> valid_objs' s proof (prove)
goal (2 subgoals):
 1. \<And>rv s a b. \<lbrakk>(a, b) \<in> set rv; \<forall>x\<in>set rv. \<exists>cte. ctes_of s (snd x) = Some cte \<and> (fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x); valid_objs' s\<rbrakk> \<Longrightarrow> valid_cap' a s
 2. \<And>s. valid_objs' s \<Longrightarrow> True \<and> valid_objs' s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_objs' s \<Longrightarrow> True \<and> valid_objs' s proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma doIPCTransfer_invs[wp]:
  "\<lbrace>invs' and tcb_at' s and tcb_at' r\<rbrace>
   doIPCTransfer s ep bg grt r
   \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (simp add: doIPCTransfer_def) apply (wpsimp wp: hoare_drop_imp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' s and tcb_at' r\<rbrace> doIPCTransfer s ep bg grt r \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' s and tcb_at' r\<rbrace> do receiveBuffer <- lookupIPCBuffer True r;
fault <- threadGet tcbFault s;
case fault of None \<Rightarrow> do sendBuffer <- lookupIPCBuffer False s;
doNormalTransfer s sendBuffer ep bg grt r receiveBuffer
od | Some v21 \<Rightarrow> doFaultTransfer bg s r receiveBuffer
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma handleFaultReply_corres:
  "ft' = fault_map ft \<Longrightarrow>
   corres (=) (tcb_at t) (tcb_at' t)
     (handle_fault_reply ft t label msg)
     (handleFaultReply ft' t label msg)" apply (cases ft) apply(simp_all add: handleFaultReply_def
                         handle_arch_fault_reply_def handleArchFaultReply_def
                         syscallMessage_def exceptionMessage_def
                    split: arch_fault.split) by (rule handle_fault_reply_registers_corres)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ft' = fault_map ft \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (handle_fault_reply ft t label msg) (handleFaultReply ft' t label msg) proof (prove)
goal (4 subgoals):
 1. \<And>x11 x12 x13. \<lbrakk>ft' = fault_map ft; ft = ExceptionTypes_A.fault.CapFault x11 x12 x13\<rbrakk> \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (handle_fault_reply ft t label msg) (handleFaultReply ft' t label msg)
 2. \<And>x2. \<lbrakk>ft' = fault_map ft; ft = ExceptionTypes_A.fault.UnknownSyscallException x2\<rbrakk> \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (handle_fault_reply ft t label msg) (handleFaultReply ft' t label msg)
 3. \<And>x31 x32. \<lbrakk>ft' = fault_map ft; ft = ExceptionTypes_A.fault.UserException x31 x32\<rbrakk> \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (handle_fault_reply ft t label msg) (handleFaultReply ft' t label msg)
 4. \<And>x4. \<lbrakk>ft' = fault_map ft; ft = ExceptionTypes_A.fault.ArchFault x4\<rbrakk> \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (handle_fault_reply ft t label msg) (handleFaultReply ft' t label msg) proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>ft' = Fault_H.fault.UnknownSyscallException x2; ft = ExceptionTypes_A.fault.UnknownSyscallException x2\<rbrakk> \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (do ta <- arch_get_sanitise_register_info t;
y <- as_user t (zipWithM_x (\<lambda>r v. setRegister r (sanitise_register ta r v)) MachineExports.syscallMessage msg);
return (label = 0)
od) (do b <- local.getSanitiseRegisterInfo t;
y <- asUser t (zipWithM_x (\<lambda>r v. setRegister r (local.sanitiseRegister b r v)) MachineExports.syscallMessage msg);
return (label = 0)
od)
 2. \<And>x31 x32. \<lbrakk>ft' = Fault_H.fault.UserException x31 x32; ft = ExceptionTypes_A.fault.UserException x31 x32\<rbrakk> \<Longrightarrow> corres (=) (tcb_at t) (tcb_at' t) (do ta <- arch_get_sanitise_register_info t;
y <- as_user t (zipWithM_x (\<lambda>r v. setRegister r (sanitise_register ta r v)) MachineExports.exceptionMessage msg);
return (label = 0)
od) (do b <- local.getSanitiseRegisterInfo t;
y <- asUser t (zipWithM_x (\<lambda>r v. setRegister r (local.sanitiseRegister b r v)) MachineExports.exceptionMessage msg);
return (label = 0)
od)
theory Ipc_R

lemma getThreadCallerSlot_inv:
  "\<lbrace>P\<rbrace> getThreadCallerSlot t \<lbrace>\<lambda>_. P\<rbrace>" by (simp add: getThreadCallerSlot_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> getThreadCallerSlot t \<lbrace>\<lambda>_. P\<rbrace>
theory Ipc_R

lemma deleteCallerCap_ct_not_ksQ:
  "\<lbrace>invs' and ct_in_state' simple' and sch_act_sane
          and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace>
   deleteCallerCap t
   \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>" apply (simp add: deleteCallerCap_def getSlotCap_def getThreadCallerSlot_def locateSlot_conv) apply (wp getThreadCallerSlot_inv cteDeleteOne_ct_not_ksQ getCTE_wp) apply (clarsimp simp: cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> deleteCallerCap t \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> do cte <- getCTE (t + 2 ^ cte_level_bits * tcbCallerSlot);
y <- assert (isReplyCap (cteCap cte) \<or> cteCap cte = capability.NullCap);
cteDeleteOne (t + 2 ^ cte_level_bits * tcbCallerSlot)
od \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))) s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (t + 2 ^ cte_level_bits * tcbCallerSlot) s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> (isReplyCap (cteCap cte) \<or> cteCap cte = capability.NullCap \<longrightarrow> (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))) s)) proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma finaliseCapTrue_standin_cur':
  "\<lbrace>\<lambda>s. cur_tcb' s\<rbrace> finaliseCapTrue_standin cap v2 \<lbrace>\<lambda>_ s'. cur_tcb' s'\<rbrace>" apply (simp add: cur_tcb'_def) apply (rule hoare_lift_Pf2 [OF _ finaliseCapTrue_standin_ct']) apply (wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cur_tcb'\<rbrace> finaliseCapTrue_standin cap v2 \<lbrace>\<lambda>_. cur_tcb'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at' (ksCurThread s) s\<rbrace> finaliseCapTrue_standin cap v2 \<lbrace>\<lambda>_ s'. tcb_at' (ksCurThread s') s'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>tcb_at' x\<rbrace> finaliseCapTrue_standin cap v2 \<lbrace>\<lambda>_. tcb_at' x\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma cteDeleteOne_cur' [wp]:
  "\<lbrace>\<lambda>s. cur_tcb' s\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>_ s'. cur_tcb' s'\<rbrace>" apply (simp add: cteDeleteOne_def unless_def when_def) apply (wp hoare_drop_imps finaliseCapTrue_standin_cur' isFinalCapability_cur'
         | simp add: split_def | wp (once) cur_tcb_lift)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cur_tcb'\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>_. cur_tcb'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cur_tcb'\<rbrace> do cte <- getCTE slot;
if cteCap cte \<noteq> capability.NullCap then do final <- isFinalCapability cte;
(remainder, info) <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable remainder slot \<and> info = capability.NullCap);
emptySlot slot capability.NullCap
od else return ()
od \<lbrace>\<lambda>_. cur_tcb'\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma handleFaultReply_cur' [wp]:
  "\<lbrace>\<lambda>s. cur_tcb' s\<rbrace> handleFaultReply x0 thread label msg \<lbrace>\<lambda>_ s'. cur_tcb' s'\<rbrace>" apply (clarsimp simp add: cur_tcb'_def) apply (rule hoare_lift_Pf2 [OF _ handleFaultReply_ct']) apply (wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cur_tcb'\<rbrace> handleFaultReply x0 thread label msg \<lbrace>\<lambda>_. cur_tcb'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at' (ksCurThread s) s\<rbrace> handleFaultReply x0 thread label msg \<lbrace>\<lambda>_ s'. tcb_at' (ksCurThread s') s'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>tcb_at' x\<rbrace> handleFaultReply x0 thread label msg \<lbrace>\<lambda>_. tcb_at' x\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma emptySlot_weak_sch_act[wp]:
  "\<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
   emptySlot slot irq
   \<lbrace>\<lambda>_ s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>" by (wp weak_sch_act_wf_lift tcb_in_cur_domain'_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> emptySlot slot irq \<lbrace>\<lambda>_ s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
theory Ipc_R

lemma cancelAllIPC_weak_sch_act_wf[wp]:
  "\<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
   cancelAllIPC epptr
   \<lbrace>\<lambda>_ s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>" apply (simp add: cancelAllIPC_def) apply (wp rescheduleRequired_weak_sch_act_wf hoare_drop_imp | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> cancelAllIPC epptr \<lbrace>\<lambda>_ s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> do ep <- getEndpoint epptr;
case ep of Structures_H.endpoint.IdleEP \<Rightarrow> return () | _ \<Rightarrow> do setEndpoint epptr Structures_H.endpoint.IdleEP;
forM_x (epQueue ep) (\<lambda>t. do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od);
rescheduleRequired
od
od \<lbrace>\<lambda>_ s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma cancelAllSignals_weak_sch_act_wf[wp]:
  "\<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
   cancelAllSignals ntfnptr
   \<lbrace>\<lambda>_ s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>" apply (simp add: cancelAllSignals_def) apply (wp rescheduleRequired_weak_sch_act_wf hoare_drop_imp | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> cancelAllSignals ntfnptr \<lbrace>\<lambda>_ s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> do ntfn <- getNotification ntfnptr;
case ntfnObj ntfn of Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> do setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn);
forM_x queue (\<lambda>t. do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od);
rescheduleRequired
od | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>_ s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma cteDeleteOne_weak_sch_act[wp]:
  "\<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
   cteDeleteOne sl
   \<lbrace>\<lambda>_ s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>" apply (simp add: cteDeleteOne_def unless_def) apply (wp hoare_drop_imps finaliseCapTrue_standin_cur' isFinalCapability_cur'
         | simp add: split_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> cteDeleteOne sl \<lbrace>\<lambda>_ s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> do cte <- getCTE sl;
when (cteCap cte \<noteq> capability.NullCap) (do final <- isFinalCapability cte;
(remainder, info) <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable remainder sl \<and> info = capability.NullCap);
emptySlot sl capability.NullCap
od)
od \<lbrace>\<lambda>_ s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma cancelSignal_valid_queues'[wp]:
  "\<lbrace>valid_queues'\<rbrace> cancelSignal t ntfn \<lbrace>\<lambda>rv. valid_queues'\<rbrace>" apply (simp add: cancelSignal_def) apply (rule hoare_pre) apply (wp getNotification_wp| wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues'\<rbrace> cancelSignal t ntfn \<lbrace>\<lambda>rv. valid_queues'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues'\<rbrace> do ntfna <- getNotification ntfn;
y <- assert (case ntfnObj ntfna of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- case remove1 t (ntfnQueue (ntfnObj ntfna)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfna))) (ntfnObj ntfna);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfna);
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. valid_queues'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do ntfna <- getNotification ntfn;
y <- assert (case ntfnObj ntfna of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- case remove1 t (ntfnQueue (ntfnObj ntfna)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfna))) (ntfnObj ntfna);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfna);
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. valid_queues'\<rbrace>
 2. \<And>s. valid_queues' s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma cte_wp_at_is_reply_cap_toI:
  "cte_wp_at ((=) (cap.ReplyCap t False rights)) ptr s
   \<Longrightarrow> cte_wp_at (is_reply_cap_to t) ptr s" by (fastforce simp: cte_wp_at_reply_cap_to_ex_rights)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at ((=) (cap.ReplyCap t False rights)) ptr s \<Longrightarrow> cte_wp_at (is_reply_cap_to t) ptr s
theory Ipc_R

lemma doReplyTransfer_corres':
  "corres dc
     (einvs and tcb_at receiver and tcb_at sender
           and cte_wp_at (is_reply_cap_to receiver) slot)
     (invs' and tcb_at' sender and tcb_at' receiver
            and valid_pspace' and cte_at' (cte_map slot))
     (do_reply_transfer sender receiver slot grant)
     (doReplyTransfer sender receiver (cte_map slot) grant)" using doReplyTransfer_corres[of receiver sender _ slot] by (fastforce simp add: cte_wp_at_reply_cap_to_ex_rights corres_underlying_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (einvs and tcb_at receiver and tcb_at sender and cte_wp_at (is_reply_cap_to receiver) slot) (invs' and tcb_at' sender and tcb_at' receiver and valid_pspace' and cte_wp_at' (\<lambda>_. True) (cte_map slot)) (do_reply_transfer sender receiver slot grant) (doReplyTransfer sender receiver (cte_map slot) grant) proof (prove)
using this:
corres dc (einvs and tcb_at receiver and tcb_at sender and cte_wp_at ((=) (cap.ReplyCap receiver False ?rights)) slot) (invs' and tcb_at' sender and tcb_at' receiver and valid_pspace' and cte_wp_at' (\<lambda>_. True) (cte_map slot)) (do_reply_transfer sender receiver slot ?grant) (doReplyTransfer sender receiver (cte_map slot) ?grant)

goal (1 subgoal):
 1. corres dc (einvs and tcb_at receiver and tcb_at sender and cte_wp_at (is_reply_cap_to receiver) slot) (invs' and tcb_at' sender and tcb_at' receiver and valid_pspace' and cte_wp_at' (\<lambda>_. True) (cte_map slot)) (do_reply_transfer sender receiver slot grant) (doReplyTransfer sender receiver (cte_map slot) grant)
theory Ipc_R

lemma valid_pspace'_splits[elim!]:
  "valid_pspace' s \<Longrightarrow> valid_objs' s"
  "valid_pspace' s \<Longrightarrow> pspace_aligned' s"
  "valid_pspace' s \<Longrightarrow> pspace_distinct' s"
  "valid_pspace' s \<Longrightarrow> valid_mdb' s"
  "valid_pspace' s \<Longrightarrow> no_0_obj' s" by (simp add: valid_pspace'_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((valid_pspace' s \<Longrightarrow> valid_objs' s) &&& (valid_pspace' s \<Longrightarrow> pspace_aligned' s)) &&& (valid_pspace' s \<Longrightarrow> pspace_distinct' s) &&& (valid_pspace' s \<Longrightarrow> valid_mdb' s) &&& (valid_pspace' s \<Longrightarrow> no_0_obj' s)