theory Interrupt_R

lemma hint_invs[wp]:
  "\<lbrace>invs'\<rbrace> InterruptDecls_H.handleInterrupt irq \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (simp add: Interrupt_H.handleInterrupt_def getSlotCap_def
             cong: irqstate.case_cong) apply (rule conjI; rule impI) apply (wp dmo_maskInterrupt_True getCTE_wp'
          | wpc | simp add: doMachineOp_bind maskIrqSignal_def )+ apply (rule_tac Q="\<lambda>rv. invs'" in hoare_post_imp) apply (clarsimp simp: cte_wp_at_ctes_of ex_nonz_cap_to'_def) apply fastforce apply (wp threadSet_invs_trivial | simp add: inQ_def handleReservedIRQ_def)+ apply (wp hoare_post_comb_imp_conj hoare_drop_imp getIRQState_inv) apply (assumption)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> handleInterrupt irq \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. (maxIRQ < irq \<longrightarrow> \<lbrace>invs'\<rbrace> doMachineOp (do y <- maskInterrupt True irq;
ackInterrupt irq
od) \<lbrace>\<lambda>rv. invs'\<rbrace>) \<and> (\<not> maxIRQ < irq \<longrightarrow> \<lbrace>invs'\<rbrace> do st <- getIRQState irq;
y <- case st of irqstate.IRQInactive \<Rightarrow> fail | irqstate.IRQSignal \<Rightarrow> do slot <- getIRQSlot irq;
cte <- getCTE slot;
y <- case cteCap cte of capability.NotificationCap x xa True xb \<Rightarrow> sendSignal (capNtfnPtr (cteCap cte)) (capNtfnBadge (cteCap cte)) | capability.NotificationCap x xa False xb \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq | _ \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq;
maskIrqSignal irq
od | irqstate.IRQTimer \<Rightarrow> do y <- timerTick;
doMachineOp resetTimer
od | irqstate.IRQReserved \<Rightarrow> handleReservedIRQ irq;
doMachineOp (ackInterrupt irq)
od \<lbrace>\<lambda>rv. invs'\<rbrace>) proof (prove)
goal (2 subgoals):
 1. maxIRQ < irq \<Longrightarrow> \<lbrace>invs'\<rbrace> doMachineOp (do y <- maskInterrupt True irq;
ackInterrupt irq
od) \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<not> maxIRQ < irq \<Longrightarrow> \<lbrace>invs'\<rbrace> do st <- getIRQState irq;
y <- case st of irqstate.IRQInactive \<Rightarrow> fail | irqstate.IRQSignal \<Rightarrow> do slot <- getIRQSlot irq;
cte <- getCTE slot;
y <- case cteCap cte of capability.NotificationCap x xa True xb \<Rightarrow> sendSignal (capNtfnPtr (cteCap cte)) (capNtfnBadge (cteCap cte)) | capability.NotificationCap x xa False xb \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq | _ \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq;
maskIrqSignal irq
od | irqstate.IRQTimer \<Rightarrow> do y <- timerTick;
doMachineOp resetTimer
od | irqstate.IRQReserved \<Rightarrow> handleReservedIRQ irq;
doMachineOp (ackInterrupt irq)
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>st. \<lbrakk>\<not> maxIRQ < irq; st = irqstate.IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?R43 irqstate.IRQSignal\<rbrace> getIRQSlot irq \<lbrace>\<lambda>slot s. \<forall>cte. cte_wp_at' ((=) cte) slot s \<longrightarrow> ((\<exists>x. cteCap cte = capability.ThreadCap x) \<longrightarrow> invs' s) \<and> (cteCap cte = capability.NullCap \<longrightarrow> invs' s) \<and> (\<forall>x xa xb. (\<exists>xc. cteCap cte = capability.NotificationCap x xa xb xc) \<longrightarrow> (xb \<longrightarrow> invs' s \<and> ex_nonz_cap_to' x s) \<and> (\<not> xb \<longrightarrow> invs' s)) \<and> ((\<exists>x. cteCap cte = capability.IRQHandlerCap x) \<longrightarrow> invs' s) \<and> ((\<exists>x xa xb xc xd xe. cteCap cte = capability.EndpointCap x xa xb xc xd xe) \<longrightarrow> invs' s) \<and> (cteCap cte = capability.DomainCap \<longrightarrow> invs' s) \<and> ((\<exists>x xa xb. cteCap cte = capability.Zombie x xa xb) \<longrightarrow> invs' s) \<and> ((\<exists>x. cteCap cte = capability.ArchObjectCap x) \<longrightarrow> invs' s) \<and> ((\<exists>x xa xb. cteCap cte = capability.ReplyCap x xa xb) \<longrightarrow> invs' s) \<and> ((\<exists>x xa xb xc. cteCap cte = capability.UntypedCap x xa xb xc) \<longrightarrow> invs' s) \<and> ((\<exists>x xa xb xc. cteCap cte = capability.CNodeCap x xa xb xc) \<longrightarrow> invs' s) \<and> (cteCap cte = capability.IRQControlCap \<longrightarrow> invs' s)\<rbrace>
 2. \<And>st. \<lbrakk>\<not> maxIRQ < irq; st = irqstate.IRQTimer\<rbrakk> \<Longrightarrow> \<lbrace>?R42 st\<rbrace> do y <- timerTick;
doMachineOp resetTimer
od \<lbrace>\<lambda>y. invs'\<rbrace>
 3. \<And>st. \<lbrakk>\<not> maxIRQ < irq; st = irqstate.IRQReserved\<rbrakk> \<Longrightarrow> \<lbrace>?R41 st\<rbrace> handleReservedIRQ irq \<lbrace>\<lambda>y. invs'\<rbrace>
 4. \<not> maxIRQ < irq \<Longrightarrow> \<lbrace>?Q31\<rbrace> getIRQState irq \<lbrace>\<lambda>st s. (st = irqstate.IRQInactive \<longrightarrow> True) \<and> (st = irqstate.IRQSignal \<longrightarrow> ?R43 st s) \<and> (st = irqstate.IRQTimer \<longrightarrow> ?R42 st s) \<and> (st = irqstate.IRQReserved \<longrightarrow> ?R41 st s)\<rbrace>
 5. \<And>s. \<lbrakk>\<not> maxIRQ < irq; invs' s\<rbrakk> \<Longrightarrow> ?Q31 s proof (prove)
goal (6 subgoals):
 1. \<And>st rv s. \<lbrakk>\<not> maxIRQ < irq; st = irqstate.IRQSignal; invs' s\<rbrakk> \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) rv s \<longrightarrow> ((\<exists>x. cteCap cte = capability.ThreadCap x) \<longrightarrow> invs' s) \<and> (cteCap cte = capability.NullCap \<longrightarrow> invs' s) \<and> (\<forall>x xa xb. (\<exists>xc. cteCap cte = capability.NotificationCap x xa xb xc) \<longrightarrow> (xb \<longrightarrow> invs' s \<and> ex_nonz_cap_to' x s) \<and> (\<not> xb \<longrightarrow> invs' s)) \<and> ((\<exists>x. cteCap cte = capability.IRQHandlerCap x) \<longrightarrow> invs' s) \<and> ((\<exists>x xa xb xc xd xe. cteCap cte = capability.EndpointCap x xa xb xc xd xe) \<longrightarrow> invs' s) \<and> (cteCap cte = capability.DomainCap \<longrightarrow> invs' s) \<and> ((\<exists>x xa xb. cteCap cte = capability.Zombie x xa xb) \<longrightarrow> invs' s) \<and> ((\<exists>x. cteCap cte = capability.ArchObjectCap x) \<longrightarrow> invs' s) \<and> ((\<exists>x xa xb. cteCap cte = capability.ReplyCap x xa xb) \<longrightarrow> invs' s) \<and> ((\<exists>x xa xb xc. cteCap cte = capability.UntypedCap x xa xb xc) \<longrightarrow> invs' s) \<and> ((\<exists>x xa xb xc. cteCap cte = capability.CNodeCap x xa xb xc) \<longrightarrow> invs' s) \<and> (cteCap cte = capability.IRQControlCap \<longrightarrow> invs' s)
 2. \<And>st. \<lbrakk>\<not> maxIRQ < irq; st = irqstate.IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?R43 irqstate.IRQSignal\<rbrace> getIRQSlot irq \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>st. \<lbrakk>\<not> maxIRQ < irq; st = irqstate.IRQTimer\<rbrakk> \<Longrightarrow> \<lbrace>?R42 st\<rbrace> do y <- timerTick;
doMachineOp resetTimer
od \<lbrace>\<lambda>y. invs'\<rbrace>
 4. \<And>st. \<lbrakk>\<not> maxIRQ < irq; st = irqstate.IRQReserved\<rbrakk> \<Longrightarrow> \<lbrace>?R41 st\<rbrace> handleReservedIRQ irq \<lbrace>\<lambda>y. invs'\<rbrace>
 5. \<not> maxIRQ < irq \<Longrightarrow> \<lbrace>?Q31\<rbrace> getIRQState irq \<lbrace>\<lambda>st s. (st = irqstate.IRQInactive \<longrightarrow> True) \<and> (st = irqstate.IRQSignal \<longrightarrow> ?R43 st s) \<and> (st = irqstate.IRQTimer \<longrightarrow> ?R42 st s) \<and> (st = irqstate.IRQReserved \<longrightarrow> ?R41 st s)\<rbrace>
 6. \<And>s. \<lbrakk>\<not> maxIRQ < irq; invs' s\<rbrakk> \<Longrightarrow> ?Q31 s proof (prove)
goal (6 subgoals):
 1. \<And>rv s cte x xa xb xc. \<lbrakk>\<not> maxIRQ < irq; invs' s; ctes_of s rv = Some cte; cteCap cte = capability.NotificationCap x xa True xc; xb\<rbrakk> \<Longrightarrow> \<exists>cref cte. ctes_of s cref = Some cte \<and> x \<in> zobj_refs' (cteCap cte)
 2. \<And>st. \<lbrakk>\<not> maxIRQ < irq; st = irqstate.IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?R43 irqstate.IRQSignal\<rbrace> getIRQSlot irq \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>st. \<lbrakk>\<not> maxIRQ < irq; st = irqstate.IRQTimer\<rbrakk> \<Longrightarrow> \<lbrace>?R42 st\<rbrace> do y <- timerTick;
doMachineOp resetTimer
od \<lbrace>\<lambda>y. invs'\<rbrace>
 4. \<And>st. \<lbrakk>\<not> maxIRQ < irq; st = irqstate.IRQReserved\<rbrakk> \<Longrightarrow> \<lbrace>?R41 st\<rbrace> handleReservedIRQ irq \<lbrace>\<lambda>y. invs'\<rbrace>
 5. \<not> maxIRQ < irq \<Longrightarrow> \<lbrace>?Q31\<rbrace> getIRQState irq \<lbrace>\<lambda>st s. (st = irqstate.IRQInactive \<longrightarrow> True) \<and> (st = irqstate.IRQSignal \<longrightarrow> ?R43 st s) \<and> (st = irqstate.IRQTimer \<longrightarrow> ?R42 st s) \<and> (st = irqstate.IRQReserved \<longrightarrow> ?R41 st s)\<rbrace>
 6. \<And>s. \<lbrakk>\<not> maxIRQ < irq; invs' s\<rbrakk> \<Longrightarrow> ?Q31 s proof (prove)
goal (5 subgoals):
 1. \<And>st. \<lbrakk>\<not> maxIRQ < irq; st = irqstate.IRQSignal\<rbrakk> \<Longrightarrow> \<lbrace>?R43 irqstate.IRQSignal\<rbrace> getIRQSlot irq \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<And>st. \<lbrakk>\<not> maxIRQ < irq; st = irqstate.IRQTimer\<rbrakk> \<Longrightarrow> \<lbrace>?R42 st\<rbrace> do y <- timerTick;
doMachineOp resetTimer
od \<lbrace>\<lambda>y. invs'\<rbrace>
 3. \<And>st. \<lbrakk>\<not> maxIRQ < irq; st = irqstate.IRQReserved\<rbrakk> \<Longrightarrow> \<lbrace>?R41 st\<rbrace> handleReservedIRQ irq \<lbrace>\<lambda>y. invs'\<rbrace>
 4. \<not> maxIRQ < irq \<Longrightarrow> \<lbrace>?Q31\<rbrace> getIRQState irq \<lbrace>\<lambda>st s. (st = irqstate.IRQInactive \<longrightarrow> True) \<and> (st = irqstate.IRQSignal \<longrightarrow> ?R43 st s) \<and> (st = irqstate.IRQTimer \<longrightarrow> ?R42 st s) \<and> (st = irqstate.IRQReserved \<longrightarrow> ?R41 st s)\<rbrace>
 5. \<And>s. \<lbrakk>\<not> maxIRQ < irq; invs' s\<rbrakk> \<Longrightarrow> ?Q31 s proof (prove)
goal (2 subgoals):
 1. \<not> maxIRQ < irq \<Longrightarrow> \<lbrace>?Q31\<rbrace> getIRQState irq \<lbrace>\<lambda>st s. (st = irqstate.IRQSignal \<longrightarrow> invs' s) \<and> (st = irqstate.IRQTimer \<longrightarrow> invs' s) \<and> (st = irqstate.IRQReserved \<longrightarrow> invs' s)\<rbrace>
 2. \<And>s. \<lbrakk>\<not> maxIRQ < irq; invs' s\<rbrakk> \<Longrightarrow> ?Q31 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<not> maxIRQ < irq; invs' s\<rbrakk> \<Longrightarrow> invs' s proof (prove)
goal:
No subgoals!