kings-crown/FVELER_Isabelle huggingface dataset:
theory Interrupt_R

lemma arch_check_irq_maxIRQ_valid:
  "\<lbrace>\<top>\<rbrace> arch_check_irq y \<lbrace>\<lambda>_. (\<lambda>s. unat y \<le> unat maxIRQ)\<rbrace>, -" unfolding arch_check_irq_def supply hoare_vcg_prop[wp del]  (* FIXME lib: check rule order *)
   apply (wpsimp simp: validE_R_def wp: whenE_throwError_wp) by (metis unat_ucast_10_32 word_le_nat_alt word_le_not_less)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> arch_check_irq y \<lbrace>\<lambda>_ s. unat y \<le> unat maxIRQ\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> whenE (UCAST(10 \<rightarrow> 32) maxIRQ < y) $ throwError (ExceptionTypes_A.syscall_error.RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ)) \<lbrace>\<lambda>_ s. unat y \<le> unat maxIRQ\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> whenE (UCAST(10 \<rightarrow> 32) maxIRQ < y) $ throwError (ExceptionTypes_A.syscall_error.RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ)) \<lbrace>\<lambda>_ s. unat y \<le> unat maxIRQ\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> whenE (UCAST(10 \<rightarrow> 32) maxIRQ < y) $ throwError (ExceptionTypes_A.syscall_error.RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ)) \<lbrace>\<lambda>_ s. unat y \<le> unat maxIRQ\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<not> UCAST(10 \<rightarrow> 32) maxIRQ < y \<Longrightarrow> unat y \<le> unat maxIRQ
theory Interrupt_R

lemma arch_check_irq_maxIRQ_valid':
  "\<lbrace>\<top>\<rbrace> arch_check_irq y \<lbrace>\<lambda>_ _. unat y \<le> unat maxIRQ\<rbrace>, \<lbrace>\<lambda>_. \<top>\<rbrace>" by (wp arch_check_irq_maxIRQ_valid)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> arch_check_irq y \<lbrace>\<lambda>_ _. unat y \<le> unat maxIRQ\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
theory Interrupt_R

lemma irqhandler_simp[simp]:
  "gen_invocation_type label \<noteq> IRQIssueIRQHandler \<Longrightarrow>
   (case gen_invocation_type label of IRQIssueIRQHandler \<Rightarrow> b | _ \<Rightarrow> c) = c" by (clarsimp split: gen_invocation_labels.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gen_invocation_type label \<noteq> IRQIssueIRQHandler \<Longrightarrow> (case gen_invocation_type label of IRQIssueIRQHandler \<Rightarrow> b | _ \<Rightarrow> c) = c
theory Interrupt_R

lemma lsfco_real_cte_at'[wp]:
  "\<lbrace>valid_objs' and valid_cap' croot\<rbrace>
     lookupSlotForCNodeOp is_src croot ptr depth
   \<lbrace>\<lambda>rv s. real_cte_at' rv s\<rbrace>,-" apply (simp add: lookupSlotForCNodeOp_def split_def unlessE_def
                   whenE_def
               split del: if_split
             cong: if_cong list.case_cong capability.case_cong) apply (rule hoare_pre) apply (wp resolveAddressBits_real_cte_at'
            | simp
            | wpc | wp (once) hoare_drop_imps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and valid_cap' croot\<rbrace> lookupSlotForCNodeOp is_src croot ptr depth \<lbrace>real_cte_at'\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and valid_cap' croot\<rbrace> if isCNodeCap croot then doE y <- rangeCheck depth (Suc 0) (size ptr);
lookupErrorOnFailure is_src (doE result <- CSpace_H.resolveAddressBits croot ptr depth;
if snd result = 0 then returnOk (fst result) else throwError (Fault_H.lookup_failure.DepthMismatch (snd result) 0)
odE)
odE else throwError (Fault_H.syscall_error.FailedLookup is_src Fault_H.lookup_failure.InvalidRoot) \<lbrace>real_cte_at'\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'7\<rbrace> if isCNodeCap croot then doE y <- rangeCheck depth (Suc 0) (size ptr);
lookupErrorOnFailure is_src (doE result <- CSpace_H.resolveAddressBits croot ptr depth;
if snd result = 0 then returnOk (fst result) else throwError (Fault_H.lookup_failure.DepthMismatch (snd result) 0)
odE)
odE else throwError (Fault_H.syscall_error.FailedLookup is_src Fault_H.lookup_failure.InvalidRoot) \<lbrace>real_cte_at'\<rbrace>, -
 2. \<And>s. (valid_objs' and valid_cap' croot) s \<Longrightarrow> ?P'7 s proof (prove)
goal:
No subgoals!
theory Interrupt_R

lemma arch_invokeIRQHandler_corres:
  "irq_handler_inv_relation i i' \<Longrightarrow>
   corres dc \<top> \<top> (arch_invoke_irq_handler i) (ARM_H.invokeIRQHandler i')" apply (cases i; clarsimp simp: ARM_H.invokeIRQHandler_def) apply (rule corres_machine_op, rule corres_Id; simp) apply (rule no_fail_maskInterrupt) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. irq_handler_inv_relation i i' \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (arch_invoke_irq_handler i) (local.invokeIRQHandler i') proof (prove)
goal (1 subgoal):
 1. \<And>x1. \<lbrakk>i' = AckIRQ x1; i = ACKIrq x1\<rbrakk> \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (do_machine_op (maskInterrupt False x1)) (doMachineOp (maskInterrupt False x1)) proof (prove)
goal (1 subgoal):
 1. \<And>x1. \<lbrakk>i' = AckIRQ x1; i = ACKIrq x1\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) (maskInterrupt False x1) proof (prove)
goal:
No subgoals!
theory Interrupt_R

lemma ntfn_badge_derived_enough_strg:
  "cte_wp_at' (\<lambda>cte. isNotificationCap cap \<and> badge_derived' cap (cteCap cte)) ptr s
        \<longrightarrow> cte_wp_at' (is_derived' ctes ptr cap \<circ> cteCap) ptr s" by (clarsimp simp: cte_wp_at_ctes_of isCap_simps
                     badge_derived'_def is_derived'_def vsCapRef_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at' (\<lambda>cte. isNotificationCap cap \<and> badge_derived' cap (cteCap cte)) ptr s \<longrightarrow> cte_wp_at' (is_derived' ctes ptr cap \<circ> cteCap) ptr s
theory Interrupt_R

lemma cteDeleteOne_other_cap:
  "\<lbrace>(\<lambda>s. cte_wp_at' (P o cteCap) p s) and K (p \<noteq> p')\<rbrace>
     cteDeleteOne p'
   \<lbrace>\<lambda>rv s. cte_wp_at' (P o cteCap) p s\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: tree_cte_cteCap_eq) apply (wp cteDeleteOne_cteCaps_of) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (P \<circ> cteCap) p and K (p \<noteq> p')\<rbrace> cteDeleteOne p' \<lbrace>\<lambda>rv. cte_wp_at' (P \<circ> cteCap) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. p \<noteq> p' \<Longrightarrow> \<lbrace>cte_wp_at' (P \<circ> cteCap) p\<rbrace> cteDeleteOne p' \<lbrace>\<lambda>rv. cte_wp_at' (P \<circ> cteCap) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. p \<noteq> p' \<Longrightarrow> \<lbrace>\<lambda>s. case cteCaps_of s p of None \<Rightarrow> False | Some x2 \<Rightarrow> P x2\<rbrace> cteDeleteOne p' \<lbrace>\<lambda>rv s. case cteCaps_of s p of None \<Rightarrow> False | Some x2 \<Rightarrow> P x2\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>p \<noteq> p'; case cteCaps_of s p of None \<Rightarrow> False | Some x2 \<Rightarrow> P x2\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. \<exists>final. global.finaliseCap (cteCap cte) final True \<noteq> fail) p' s \<longrightarrow> (case ((cteCaps_of s)(p' \<mapsto> capability.NullCap)) p of None \<Rightarrow> False | Some x2 \<Rightarrow> P x2) proof (prove)
goal:
No subgoals!
theory Interrupt_R

lemma isnt_irq_handler_strg:
  "(\<not> isIRQHandlerCap cap) \<longrightarrow> (\<forall>irq. cap = IRQHandlerCap irq \<longrightarrow> P irq)" by (clarsimp simp: isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> isIRQHandlerCap cap \<longrightarrow> (\<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> P irq)
theory Interrupt_R

lemma no_fail_setIRQTrigger: "no_fail \<top> (setIRQTrigger irq trig)" by (simp add: setIRQTrigger_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (setIRQTrigger irq trig)
theory Interrupt_R

lemma setIRQTrigger_corres:
  "corres dc \<top> \<top> (do_machine_op (setIRQTrigger irq t)) (doMachineOp (setIRQTrigger irq t))" apply (rule corres_machine_op) apply (rule corres_guard_imp) apply (rule corres_rel_imp) apply (wp
            | rule corres_underlying_trivial
            | rule no_fail_setIRQTrigger
            | simp add: dc_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (\<lambda>_. True) (\<lambda>_. True) (do_machine_op (setIRQTrigger irq t)) (doMachineOp (setIRQTrigger irq t)) proof (prove)
goal (1 subgoal):
 1. corres_underlying Id False True dc (\<lambda>_. True) (\<lambda>_. True) (setIRQTrigger irq t) (setIRQTrigger irq t) proof (prove)
goal (3 subgoals):
 1. corres_underlying Id False True dc ?Q2 ?Q'2 (setIRQTrigger irq t) (setIRQTrigger irq t)
 2. \<And>s. True \<Longrightarrow> ?Q2 s
 3. \<And>s. True \<Longrightarrow> ?Q'2 s proof (prove)
goal (4 subgoals):
 1. corres_underlying Id False True ?r'6 ?Q2 ?Q'2 (setIRQTrigger irq t) (setIRQTrigger irq t)
 2. \<And>x y. ?r'6 x y \<Longrightarrow> dc x y
 3. \<And>s. True \<Longrightarrow> ?Q2 s
 4. \<And>s. True \<Longrightarrow> ?Q'2 s proof (prove)
goal:
No subgoals!
theory Interrupt_R

lemma setIRQState_cte_cap_to'[wp]:
  "\<lbrace>ex_cte_cap_to' p\<rbrace> setIRQState st irq \<lbrace>\<lambda>_. ex_cte_cap_to' p\<rbrace>" apply (simp add: setIRQState_def doMachineOp_def
                   split_def setInterruptState_def getInterruptState_def) apply wp apply (clarsimp simp: ex_cte_cap_to'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_cte_cap_wp_to' (\<lambda>_. True) p\<rbrace> setIRQState st irq \<lbrace>\<lambda>_. ex_cte_cap_wp_to' (\<lambda>_. True) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_cte_cap_wp_to' (\<lambda>_. True) p\<rbrace> do sta <- gets ksInterruptState;
y <- modify (ksInterruptState_update (\<lambda>_. intStateIRQTable_update (\<lambda>_. (intStateIRQTable sta)(irq := st)) sta));
ms <- gets ksMachineState;
p <- select_f (maskInterrupt (st = irqstate.IRQInactive) irq ms);
modify (ksMachineState_update (\<lambda>_. snd p))
od \<lbrace>\<lambda>_. ex_cte_cap_wp_to' (\<lambda>_. True) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ex_cte_cap_wp_to' (\<lambda>_. True) p s \<Longrightarrow> \<forall>x\<in>fst (maskInterrupt (st = irqstate.IRQInactive) irq (ksMachineState (s\<lparr>ksInterruptState := intStateIRQTable_update (\<lambda>_. (intStateIRQTable (ksInterruptState s))(irq := st)) (ksInterruptState s)\<rparr>))). ex_cte_cap_wp_to' (\<lambda>_. True) p (s\<lparr>ksInterruptState := intStateIRQTable_update (\<lambda>_. (intStateIRQTable (ksInterruptState s))(irq := st)) (ksInterruptState s), ksMachineState := snd x\<rparr>) proof (prove)
goal:
No subgoals!
theory Interrupt_R

lemma setIRQState_issued[wp]:
  "\<lbrace>K (st = IRQSignal)\<rbrace> setIRQState st irq \<lbrace>\<lambda>rv. irq_issued' irq\<rbrace>" apply (simp add: setIRQState_def irq_issued'_def setInterruptState_def
                   getInterruptState_def) apply wp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (st = irqstate.IRQSignal)\<rbrace> setIRQState st irq \<lbrace>\<lambda>rv. irq_issued' irq\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>y. st = irqstate.IRQSignal\<rbrace> do sta <- gets ksInterruptState;
y <- modify (ksInterruptState_update (\<lambda>_. intStateIRQTable_update (\<lambda>_. (intStateIRQTable sta)(irq := st)) sta));
doMachineOp (maskInterrupt (st = irqstate.IRQInactive) irq)
od \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. st = irqstate.IRQSignal \<Longrightarrow> intStateIRQTable (ksInterruptState (s\<lparr>ksInterruptState := intStateIRQTable_update (\<lambda>_. (intStateIRQTable (ksInterruptState s))(irq := st)) (ksInterruptState s)\<rparr>)) irq = irqstate.IRQSignal proof (prove)
goal:
No subgoals!
theory Interrupt_R

lemma dmo_setIRQTrigger_invs'[wp]:
  "\<lbrace>invs'\<rbrace> doMachineOp (setIRQTrigger irq t) \<lbrace>\<lambda>r. invs'\<rbrace>" apply (wp dmo_invs' no_irq_setIRQTrigger no_irq) apply clarsimp apply (drule_tac P4="\<lambda>m'. underlying_memory m' p = underlying_memory m p"
         in use_valid[where P=P and Q="\<lambda>_. P" for P]) apply (simp add: setIRQTrigger_def machine_op_lift_def
                     machine_rest_lift_def split_def | wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> doMachineOp (setIRQTrigger irq t) \<lbrace>\<lambda>r. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<Longrightarrow> ((\<lambda>s. \<forall>m. \<forall>(r, m')\<in>fst (setIRQTrigger irq t m). \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory m' p = underlying_memory m p) and invs') s proof (prove)
goal (1 subgoal):
 1. \<And>s m b p. \<lbrakk>invs' s; ((), b) \<in> fst (setIRQTrigger irq t m); \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal (3 subgoals):
 1. \<And>s m b p. \<lbrakk>invs' s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>m'. underlying_memory m' p = underlying_memory m p\<rbrace> setIRQTrigger irq t \<lbrace>\<lambda>_ m'. underlying_memory m' p = underlying_memory m p\<rbrace>
 2. \<And>s m b p. \<lbrakk>invs' s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> underlying_memory m p = underlying_memory m p
 3. \<And>s m b p. \<lbrakk>invs' s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p; underlying_memory b p = underlying_memory m p\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal:
No subgoals!
theory Interrupt_R

lemma getIRQState_corres:
  "corres irq_state_relation \<top> \<top>
       (get_irq_state irq) (getIRQState irq)" apply (simp add: get_irq_state_def getIRQState_def getInterruptState_def) apply (clarsimp simp: state_relation_def interrupt_state_relation_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres irq_state_relation (\<lambda>_. True) (\<lambda>_. True) (get_irq_state irq) (getIRQState irq) proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. (s, s') \<in> state_relation \<longrightarrow> irq_state_relation (interrupt_states s irq) (intStateIRQTable (ksInterruptState s') irq) proof (prove)
goal:
No subgoals!
theory Interrupt_R

lemma getIRQState_prop:
  "\<lbrace>\<lambda>s. P (intStateIRQTable (ksInterruptState s) irq)\<rbrace>
     getIRQState irq
   \<lbrace>\<lambda>rv s. P rv\<rbrace>" apply (simp add: getIRQState_def getInterruptState_def) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (intStateIRQTable (ksInterruptState s) irq)\<rbrace> getIRQState irq \<lbrace>\<lambda>rv s. P rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (intStateIRQTable (ksInterruptState s) irq)\<rbrace> liftM (swp id irq \<circ> intStateIRQTable) (gets ksInterruptState) \<lbrace>\<lambda>rv s. P rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (intStateIRQTable (ksInterruptState s) irq) \<Longrightarrow> ((\<lambda>rv s. P rv) \<circ> (swp id irq \<circ> intStateIRQTable)) (ksInterruptState s) s proof (prove)
goal:
No subgoals!
theory Interrupt_R

lemma decDomainTime_corres:
  "corres dc \<top> \<top> dec_domain_time decDomainTime" apply (simp add:dec_domain_time_def corres_underlying_def
    decDomainTime_def simpler_modify_def) apply (clarsimp simp:state_relation_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (\<lambda>_. True) (\<lambda>_. True) dec_domain_time decDomainTime proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>state_relation. case x of (s, s') \<Rightarrow> (domain_time_update (\<lambda>_. domain_time s - 1) s, s'\<lparr>ksDomainTime := ksDomainTime s' - 1\<rparr>) \<in> state_relation proof (prove)
goal:
No subgoals!
theory Interrupt_R

lemma tcbSchedAppend_valid_objs':
  "\<lbrace>valid_objs'\<rbrace>tcbSchedAppend t \<lbrace>\<lambda>r. valid_objs'\<rbrace>" apply (simp add:tcbSchedAppend_def) apply (wpsimp wp: unless_wp threadSet_valid_objs' threadGet_wp) apply (clarsimp simp add:obj_at'_def typ_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> tcbSchedAppend t \<lbrace>\<lambda>r. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> do queued <- threadGet tcbQueued t;
unless queued (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (queue @ [t]);
y <- when (null queue) (addToBitmap tdom prio);
threadSet (tcbQueued_update (\<lambda>_. True)) t
od)
od \<lbrace>\<lambda>r. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_objs' s; tcb_at' t s\<rbrakk> \<Longrightarrow> \<exists>tcb. (tcbQueued tcb \<longrightarrow> ko_at' tcb t s) \<and> (\<not> tcbQueued tcb \<longrightarrow> ko_at' tcb t s \<and> (\<exists>tcb. ko_at' tcb t s)) proof (prove)
goal:
No subgoals!
theory Interrupt_R

lemma thread_state_case_if:
 "(case state of Structures_A.thread_state.Running \<Rightarrow> f | _ \<Rightarrow> g) =
  (if state = Structures_A.thread_state.Running then f else g)" by (case_tac state,auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case state of Structures_A.thread_state.Running \<Rightarrow> f | _ \<Rightarrow> g) = (if state = Structures_A.thread_state.Running then f else g)
theory Interrupt_R

lemma threadState_case_if:
 "(case state of Structures_H.thread_state.Running \<Rightarrow> f | _ \<Rightarrow> g) =
  (if state = Structures_H.thread_state.Running then f else g)" by (case_tac state,auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case state of Structures_H.thread_state.Running \<Rightarrow> f | _ \<Rightarrow> g) = (if state = Structures_H.thread_state.Running then f else g)
theory Interrupt_R

lemma threadSet_ksDomainTime[wp]:
  "\<lbrace>\<lambda>s. P (ksDomainTime s)\<rbrace> threadSet f ptr \<lbrace>\<lambda>rv s. P (ksDomainTime s)\<rbrace>" apply (simp add: threadSet_def setObject_def split_def) apply (wp crunch_wps | simp add:updateObject_default_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksDomainTime s)\<rbrace> threadSet f ptr \<lbrace>\<lambda>rv s. P (ksDomainTime s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksDomainTime s)\<rbrace> do tcb <- getObject ptr;
ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 ptr ps));
obj' <- updateObject_default (f tcb) (snd p) ptr (fst p) (snd (lookupAround2 ptr ps));
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od \<lbrace>\<lambda>rv s. P (ksDomainTime s)\<rbrace> proof (prove)
goal:
No subgoals!
theory Interrupt_R

lemma updateTimeSlice_valid_pspace[wp]:
  "\<lbrace>valid_pspace'\<rbrace> threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread
  \<lbrace>\<lambda>r. valid_pspace'\<rbrace>" apply (wp threadSet_valid_pspace'T) apply (auto simp:tcb_cte_cases_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pspace'\<rbrace> threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread \<lbrace>\<lambda>r. valid_pspace'\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<forall>tcb. \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF (tcbTimeSlice_update (\<lambda>_. ts') tcb) = getF tcb
 2. \<forall>tcb s. valid_tcb_state' (tcbState tcb) s \<longrightarrow> valid_tcb_state' (tcbState (tcbTimeSlice_update (\<lambda>_. ts') tcb)) s
 3. \<forall>tcb s. valid_bound_ntfn' (tcbBoundNotification tcb) s \<longrightarrow> valid_bound_ntfn' (tcbBoundNotification (tcbTimeSlice_update (\<lambda>_. ts') tcb)) s
 4. \<forall>tcb. is_aligned (tcbIPCBuffer tcb) msg_align_bits \<longrightarrow> is_aligned (tcbIPCBuffer (tcbTimeSlice_update (\<lambda>_. ts') tcb)) msg_align_bits
 5. \<forall>tcb. tcbDomain tcb \<le> maxDomain \<longrightarrow> tcbDomain (tcbTimeSlice_update (\<lambda>_. ts') tcb) \<le> maxDomain
 6. \<forall>tcb. tcbPriority tcb \<le> maxPriority \<longrightarrow> tcbPriority (tcbTimeSlice_update (\<lambda>_. ts') tcb) \<le> maxPriority
 7. \<forall>tcb. tcbMCP tcb \<le> maxPriority \<longrightarrow> tcbMCP (tcbTimeSlice_update (\<lambda>_. ts') tcb) \<le> maxPriority
 8. \<And>s. valid_pspace' s \<Longrightarrow> valid_pspace' s proof (prove)
goal:
No subgoals!
theory Interrupt_R

lemma updateTimeSlice_sch_act_wf[wp]:
  "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<rbrace>
   threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread
   \<lbrace>\<lambda>r s. sch_act_wf (ksSchedulerAction s) s\<rbrace>" by (wp threadSet_sch_act,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread \<lbrace>\<lambda>r s. sch_act_wf (ksSchedulerAction s) s\<rbrace>
theory Interrupt_R

lemma updateTimeSlice_valid_queues[wp]:
  "\<lbrace>\<lambda>s. Invariants_H.valid_queues s \<rbrace>
   threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread
   \<lbrace>\<lambda>r s. Invariants_H.valid_queues s\<rbrace>" apply (wp threadSet_valid_queues,simp) apply (clarsimp simp:obj_at'_def inQ_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues\<rbrace> threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread \<lbrace>\<lambda>r. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. Invariants_H.valid_queues s \<Longrightarrow> \<forall>d p. (\<exists>tcb. inQ d p tcb \<and> runnable' (tcbState tcb) \<and> (inQ d p (tcbTimeSlice_update (\<lambda>_. ts') tcb) \<longrightarrow> \<not> runnable' (tcbState tcb))) \<longrightarrow> obj_at' (\<lambda>tcb. inQ d p tcb \<and> runnable' (tcbState tcb) \<and> (inQ d p (tcbTimeSlice_update (\<lambda>_. ts') tcb) \<longrightarrow> \<not> runnable' (tcbState tcb))) thread s \<longrightarrow> thread \<notin> set (ksReadyQueues s (d, p)) proof (prove)
goal:
No subgoals!