theory IRQ_DP

lemma decode_invocation_irq_endpoint_rv':
"\<lbrace>\<lambda>s. P (SetIrqHandler (the $ cdl_cap_irq cap) endpoint_cap endpoint_ptr) s \<and> caps = [(endpoint_cap, endpoint_ptr)]@xs \<and>
  is_ntfn_cap endpoint_cap   \<rbrace>
decode_irq_handler_invocation cap cap_ref caps (IrqHandlerSetEndpointIntent)
\<lbrace>P\<rbrace>, -" apply (rule validE_R_gen_asm_conj) apply (clarsimp simp: decode_irq_handler_invocation_def) apply (wp | wpc)+ apply (clarsimp split: cdl_cap.splits, safe) apply ((wp throw_on_none_rv)+, clarsimp simp: get_index_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (SetIrqHandler (the $ cdl_cap_irq cap) endpoint_cap endpoint_ptr) s \<and> caps = [(endpoint_cap, endpoint_ptr)] @ xs \<and> is_ntfn_cap endpoint_cap\<rbrace> decode_irq_handler_invocation cap cap_ref caps IrqHandlerSetEndpointIntent \<lbrace>P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. caps = [(endpoint_cap, endpoint_ptr)] @ xs \<and> is_ntfn_cap endpoint_cap \<Longrightarrow> \<lbrace>P (SetIrqHandler (the $ cdl_cap_irq cap) endpoint_cap endpoint_ptr)\<rbrace> decode_irq_handler_invocation cap cap_ref caps IrqHandlerSetEndpointIntent \<lbrace>P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps = (endpoint_cap, endpoint_ptr) # xs; is_ntfn_cap endpoint_cap\<rbrakk> \<Longrightarrow> \<lbrace>P (SetIrqHandler (the (cdl_cap_irq cap)) endpoint_cap endpoint_ptr)\<rbrace> doE endpoint <- throw_on_none (get_index ((endpoint_cap, endpoint_ptr) # xs) 0);
irq <- liftE (assert_opt (cdl_cap_irq cap));
y <- case fst endpoint of NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw;
returnOk (SetIrqHandler irq (fst endpoint) (snd endpoint))
odE \<sqinter> throw \<lbrace>P\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<lbrakk>caps = (endpoint_cap, endpoint_ptr) # xs; is_ntfn_cap endpoint_cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'291\<rbrace> throw_on_none (get_index ((endpoint_cap, endpoint_ptr) # xs) 0) \<lbrace>\<lambda>rv s. cdl_cap_irq cap \<noteq> None \<longrightarrow> True \<and> (fst rv = NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb. fst rv = UntypedCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. fst rv = EndpointCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. fst rv = NotificationCap x xa xb \<longrightarrow> P (SetIrqHandler (the (cdl_cap_irq cap)) (fst rv) (snd rv)) s) \<and> (\<forall>x xa. fst rv = ReplyCap x xa \<longrightarrow> True) \<and> (\<forall>x. fst rv = MasterReplyCap x \<longrightarrow> True) \<and> (\<forall>x xa xb xc. fst rv = CNodeCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x. fst rv = TcbCap x \<longrightarrow> True) \<and> (fst rv = DomainCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. fst rv = PendingSyncSendCap x xa xb xc xd xe \<longrightarrow> True) \<and> (\<forall>x xa xb. fst rv = PendingSyncRecvCap x xa xb \<longrightarrow> True) \<and> (\<forall>x. fst rv = PendingNtfnRecvCap x \<longrightarrow> True) \<and> (fst rv = RestartCap \<longrightarrow> True) \<and> (fst rv = RunningCap \<longrightarrow> True) \<and> (fst rv = IrqControlCap \<longrightarrow> True) \<and> (\<forall>x. fst rv = IrqHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. fst rv = FrameCap x xa xb xc xd xe \<longrightarrow> True) \<and> (\<forall>x xa xb. fst rv = PageTableCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. fst rv = PageDirectoryCap x xa xb \<longrightarrow> True) \<and> (fst rv = AsidControlCap \<longrightarrow> True) \<and> (\<forall>x xa. fst rv = AsidPoolCap x xa \<longrightarrow> True) \<and> (\<forall>x xa. fst rv = IOPortsCap x xa \<longrightarrow> True) \<and> (fst rv = IOSpaceMasterCap \<longrightarrow> True) \<and> (\<forall>x. fst rv = IOSpaceCap x \<longrightarrow> True) \<and> (\<forall>x. fst rv = IOPageTableCap x \<longrightarrow> True) \<and> (\<forall>x. fst rv = ZombieCap x \<longrightarrow> True) \<and> (\<forall>x. fst rv = BoundNotificationCap x \<longrightarrow> True)\<rbrace>, -
 2. \<lbrakk>caps = (endpoint_cap, endpoint_ptr) # xs; is_ntfn_cap endpoint_cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'5\<rbrace> throw \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. \<lbrakk>caps = (endpoint_cap, endpoint_ptr) # xs; is_ntfn_cap endpoint_cap; P (SetIrqHandler (the (cdl_cap_irq cap)) endpoint_cap endpoint_ptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. True \<and> True \<and> True \<and> ?P'291 s) and ?P'5) s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>caps = (endpoint_cap, endpoint_ptr) # xs; is_ntfn_cap endpoint_cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'291\<rbrace> throw_on_none (get_index ((endpoint_cap, endpoint_ptr) # xs) 0) \<lbrace>\<lambda>rv s. (\<exists>y. cdl_cap_irq cap = Some y) \<longrightarrow> (\<forall>x xa xb. fst rv = NotificationCap x xa xb \<longrightarrow> P (SetIrqHandler (the (cdl_cap_irq cap)) (NotificationCap x xa xb) (snd rv)) s)\<rbrace>, -
 2. \<lbrakk>caps = (endpoint_cap, endpoint_ptr) # xs; is_ntfn_cap endpoint_cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'5\<rbrace> throw \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. \<lbrakk>caps = (endpoint_cap, endpoint_ptr) # xs; is_ntfn_cap endpoint_cap; P (SetIrqHandler (the (cdl_cap_irq cap)) endpoint_cap endpoint_ptr) s\<rbrakk> \<Longrightarrow> ?P'291 s
 4. \<And>s. \<lbrakk>caps = (endpoint_cap, endpoint_ptr) # xs; is_ntfn_cap endpoint_cap; P (SetIrqHandler (the (cdl_cap_irq cap)) endpoint_cap endpoint_ptr) s\<rbrakk> \<Longrightarrow> ?P'5 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>caps = (endpoint_cap, endpoint_ptr) # xs; is_ntfn_cap endpoint_cap; P (SetIrqHandler (the (cdl_cap_irq cap)) endpoint_cap endpoint_ptr) s\<rbrakk> \<Longrightarrow> True \<and> True proof (prove)
goal:
No subgoals!