theory TcbAcc_R

lemma preemptionPoint_irq [wp]:
  "\<lbrace>valid_irq_states'\<rbrace> preemptionPoint -,
   \<lbrace>\<lambda>irq s. intStateIRQTable (ksInterruptState s) irq \<noteq> IRQInactive\<rbrace>" apply (simp add: preemptionPoint_def setWorkUnits_def modifyWorkUnits_def getWorkUnits_def) apply (wp whenE_wp|wpc)+ apply (rule hoare_post_imp) prefer 2 apply (rule doMachineOp_getActiveIRQ_IRQ_active) apply clarsimp apply wp+ apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> preemptionPoint -, \<lbrace>\<lambda>irq s. intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> doE y <- liftE (modify (\<lambda>ks. ks\<lparr>ksWorkUnitsCompleted := ksWorkUnitsCompleted ks + 1\<rparr>));
workUnits <- liftE (gets ksWorkUnitsCompleted);
whenE (FaultMonad_H.workUnitsLimit \<le> workUnits) (doE y <- liftE (modify (ksWorkUnitsCompleted_update (\<lambda>_. 0)));
liftE (doMachineOp (getActiveIRQ True)) >>=E case_option (returnOk ()) throwError
odE)
odE -, \<lbrace>\<lambda>irq s. intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>y workUnits ya. FaultMonad_H.workUnitsLimit \<le> workUnits \<Longrightarrow> \<lbrace>?B5 y workUnits ya\<rbrace> doMachineOp (getActiveIRQ True) \<lbrace>\<lambda>x s. (x = None \<longrightarrow> True) \<and> (\<forall>xa. x = Some xa \<longrightarrow> intStateIRQTable (ksInterruptState s) xa \<noteq> irqstate.IRQInactive \<and> True)\<rbrace>
 2. \<And>y workUnits. FaultMonad_H.workUnitsLimit \<le> workUnits \<Longrightarrow> \<lbrace>?Q4 y workUnits\<rbrace> liftE (modify (ksWorkUnitsCompleted_update (\<lambda>_. 0))) \<lbrace>?B5 y workUnits\<rbrace>, \<lbrace>\<lambda>irq s. intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive\<rbrace>
 3. \<And>y. \<lbrace>?B1 y\<rbrace> liftE (gets ksWorkUnitsCompleted) \<lbrace>\<lambda>workUnits. if FaultMonad_H.workUnitsLimit \<le> workUnits then ?Q4 y workUnits else (\<lambda>_. True)\<rbrace>, \<lbrace>\<lambda>irq s. intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive\<rbrace>
 4. \<lbrace>?P'\<rbrace> liftE (modify (\<lambda>ks. ks\<lparr>ksWorkUnitsCompleted := ksWorkUnitsCompleted ks + 1\<rparr>)) \<lbrace>?B1\<rbrace>, \<lbrace>\<lambda>irq s. intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive\<rbrace>
 5. \<And>s. valid_irq_states' s \<Longrightarrow> ?P' s proof (prove)
goal (6 subgoals):
 1. \<And>y workUnits ya rv s. \<lbrakk>FaultMonad_H.workUnitsLimit \<le> workUnits; ?Q30 y workUnits ya rv s\<rbrakk> \<Longrightarrow> (rv = None \<longrightarrow> True) \<and> (\<forall>x. rv = Some x \<longrightarrow> intStateIRQTable (ksInterruptState s) x \<noteq> irqstate.IRQInactive \<and> True)
 2. \<And>y workUnits ya. FaultMonad_H.workUnitsLimit \<le> workUnits \<Longrightarrow> \<lbrace>?B5 y workUnits ya\<rbrace> doMachineOp (getActiveIRQ True) \<lbrace>?Q30 y workUnits ya\<rbrace>
 3. \<And>y workUnits. FaultMonad_H.workUnitsLimit \<le> workUnits \<Longrightarrow> \<lbrace>?Q4 y workUnits\<rbrace> liftE (modify (ksWorkUnitsCompleted_update (\<lambda>_. 0))) \<lbrace>?B5 y workUnits\<rbrace>, \<lbrace>\<lambda>irq s. intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive\<rbrace>
 4. \<And>y. \<lbrace>?B1 y\<rbrace> liftE (gets ksWorkUnitsCompleted) \<lbrace>\<lambda>workUnits. if FaultMonad_H.workUnitsLimit \<le> workUnits then ?Q4 y workUnits else (\<lambda>_. True)\<rbrace>, \<lbrace>\<lambda>irq s. intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive\<rbrace>
 5. \<lbrace>?P'\<rbrace> liftE (modify (\<lambda>ks. ks\<lparr>ksWorkUnitsCompleted := ksWorkUnitsCompleted ks + 1\<rparr>)) \<lbrace>?B1\<rbrace>, \<lbrace>\<lambda>irq s. intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive\<rbrace>
 6. \<And>s. valid_irq_states' s \<Longrightarrow> ?P' s proof (prove)
goal (6 subgoals):
 1. \<And>y workUnits ya. FaultMonad_H.workUnitsLimit \<le> workUnits \<Longrightarrow> \<lbrace>?B5 y workUnits ya\<rbrace> doMachineOp (getActiveIRQ True) \<lbrace>?Q30 y workUnits ya\<rbrace>
 2. \<And>y workUnits ya rv s. \<lbrakk>FaultMonad_H.workUnitsLimit \<le> workUnits; ?Q30 y workUnits ya rv s\<rbrakk> \<Longrightarrow> (rv = None \<longrightarrow> True) \<and> (\<forall>x. rv = Some x \<longrightarrow> intStateIRQTable (ksInterruptState s) x \<noteq> irqstate.IRQInactive \<and> True)
 3. \<And>y workUnits. FaultMonad_H.workUnitsLimit \<le> workUnits \<Longrightarrow> \<lbrace>?Q4 y workUnits\<rbrace> liftE (modify (ksWorkUnitsCompleted_update (\<lambda>_. 0))) \<lbrace>?B5 y workUnits\<rbrace>, \<lbrace>\<lambda>irq s. intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive\<rbrace>
 4. \<And>y. \<lbrace>?B1 y\<rbrace> liftE (gets ksWorkUnitsCompleted) \<lbrace>\<lambda>workUnits. if FaultMonad_H.workUnitsLimit \<le> workUnits then ?Q4 y workUnits else (\<lambda>_. True)\<rbrace>, \<lbrace>\<lambda>irq s. intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive\<rbrace>
 5. \<lbrace>?P'\<rbrace> liftE (modify (\<lambda>ks. ks\<lparr>ksWorkUnitsCompleted := ksWorkUnitsCompleted ks + 1\<rparr>)) \<lbrace>?B1\<rbrace>, \<lbrace>\<lambda>irq s. intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive\<rbrace>
 6. \<And>s. valid_irq_states' s \<Longrightarrow> ?P' s proof (prove)
goal (5 subgoals):
 1. \<And>y workUnits ya rv s. \<lbrakk>FaultMonad_H.workUnitsLimit \<le> workUnits; \<forall>irq. rv = Some irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive\<rbrakk> \<Longrightarrow> (rv = None \<longrightarrow> True) \<and> (\<forall>x. rv = Some x \<longrightarrow> intStateIRQTable (ksInterruptState s) x \<noteq> irqstate.IRQInactive \<and> True)
 2. \<And>y workUnits. FaultMonad_H.workUnitsLimit \<le> workUnits \<Longrightarrow> \<lbrace>?Q4 y workUnits\<rbrace> liftE (modify (ksWorkUnitsCompleted_update (\<lambda>_. 0))) \<lbrace>\<lambda>ya. valid_irq_states'\<rbrace>, \<lbrace>\<lambda>irq s. intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive\<rbrace>
 3. \<And>y. \<lbrace>?B1 y\<rbrace> liftE (gets ksWorkUnitsCompleted) \<lbrace>\<lambda>workUnits. if FaultMonad_H.workUnitsLimit \<le> workUnits then ?Q4 y workUnits else (\<lambda>_. True)\<rbrace>, \<lbrace>\<lambda>irq s. intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive\<rbrace>
 4. \<lbrace>?P'\<rbrace> liftE (modify (\<lambda>ks. ks\<lparr>ksWorkUnitsCompleted := ksWorkUnitsCompleted ks + 1\<rparr>)) \<lbrace>?B1\<rbrace>, \<lbrace>\<lambda>irq s. intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive\<rbrace>
 5. \<And>s. valid_irq_states' s \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<And>y workUnits. FaultMonad_H.workUnitsLimit \<le> workUnits \<Longrightarrow> \<lbrace>?Q4 y workUnits\<rbrace> liftE (modify (ksWorkUnitsCompleted_update (\<lambda>_. 0))) \<lbrace>\<lambda>ya. valid_irq_states'\<rbrace>, \<lbrace>\<lambda>irq s. intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive\<rbrace>
 2. \<And>y. \<lbrace>?B1 y\<rbrace> liftE (gets ksWorkUnitsCompleted) \<lbrace>\<lambda>workUnits. if FaultMonad_H.workUnitsLimit \<le> workUnits then ?Q4 y workUnits else (\<lambda>_. True)\<rbrace>, \<lbrace>\<lambda>irq s. intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive\<rbrace>
 3. \<lbrace>?P'\<rbrace> liftE (modify (\<lambda>ks. ks\<lparr>ksWorkUnitsCompleted := ksWorkUnitsCompleted ks + 1\<rparr>)) \<lbrace>?B1\<rbrace>, \<lbrace>\<lambda>irq s. intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive\<rbrace>
 4. \<And>s. valid_irq_states' s \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_irq_states' s \<Longrightarrow> (if FaultMonad_H.workUnitsLimit \<le> ksWorkUnitsCompleted (s\<lparr>ksWorkUnitsCompleted := ksWorkUnitsCompleted s + 1\<rparr>) then \<lambda>s. valid_irq_states' (s\<lparr>ksWorkUnitsCompleted := 0\<rparr>) else (\<lambda>_. True)) (s\<lparr>ksWorkUnitsCompleted := ksWorkUnitsCompleted s + 1\<rparr>) proof (prove)
goal:
No subgoals!