theory Syscall_DR

lemma transform_intent_irq_handler_None:
  "\<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.IRQHandlerCap w\<rbrakk>
             \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r. \<bottom>\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>" supply gen_invocation_type_eq[symmetric, simp] apply (clarsimp simp:Decode_A.decode_invocation_def) apply (wp) apply (clarsimp simp:decode_irq_handler_invocation_def|rule conjI)+ apply (clarsimp simp:transform_intent_def split: list.splits)+ apply (clarsimp simp:transform_intent_def |rule conjI | wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = IRQHandlerCap w\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = IRQHandlerCap w\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = IRQHandlerCap w\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> liftME InvokeIRQHandler (Decode_A.decode_irq_handler_invocation label w excaps) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = IRQHandlerCap w\<rbrakk> \<Longrightarrow> \<lbrace>?P'3\<rbrace> Decode_A.decode_irq_handler_invocation label w excaps \<lbrace>(\<lambda>r _. False) \<circ> InvokeIRQHandler\<rbrace>, -
 2. \<And>sa. \<lbrakk>transform_intent (invocation_type label) args = None; cap = IRQHandlerCap w; s = sa\<rbrakk> \<Longrightarrow> s = sa \<and> ?P'3 sa proof (prove)
goal (3 subgoals):
 1. \<lbrakk>transform_intent (GenInvocationLabel IRQClearIRQHandler) args = None; cap = IRQHandlerCap w; invocation_type label = GenInvocationLabel IRQClearIRQHandler\<rbrakk> \<Longrightarrow> \<lbrace>?P'3\<rbrace> returnOk (ClearIRQHandler w) \<lbrace>\<lambda>r _. False\<rbrace>, -
 2. \<lbrakk>transform_intent (invocation_type label) args = None; cap = IRQHandlerCap w\<rbrakk> \<Longrightarrow> invocation_type label \<noteq> GenInvocationLabel IRQClearIRQHandler \<longrightarrow> (excaps \<noteq> [] \<longrightarrow> (invocation_type label = GenInvocationLabel IRQSetIRQHandler \<longrightarrow> \<lbrace>?P'3\<rbrace> case hd excaps of (cap, slot) \<Rightarrow> if Structures_A.is_ntfn_cap cap \<and> AllowWrite \<in> Structures_A.cap_rights cap then returnOk $ SetIRQHandler w cap slot else throwError $ InvalidCapability 0 \<lbrace>\<lambda>r _. False\<rbrace>, -) \<and> (invocation_type label \<noteq> GenInvocationLabel IRQSetIRQHandler \<longrightarrow> (invocation_type label = GenInvocationLabel IRQAckIRQ \<longrightarrow> \<lbrace>?P'3\<rbrace> returnOk (ACKIrq w) \<lbrace>\<lambda>r _. False\<rbrace>, -) \<and> (invocation_type label \<noteq> GenInvocationLabel IRQAckIRQ \<longrightarrow> \<lbrace>?P'3\<rbrace> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, -))) \<and> (excaps = [] \<longrightarrow> (invocation_type label = GenInvocationLabel IRQSetIRQHandler \<longrightarrow> \<lbrace>?P'3\<rbrace> throwError TruncatedMessage \<lbrace>\<lambda>r _. False\<rbrace>, -) \<and> (invocation_type label \<noteq> GenInvocationLabel IRQSetIRQHandler \<longrightarrow> (invocation_type label = GenInvocationLabel IRQAckIRQ \<longrightarrow> \<lbrace>?P'3\<rbrace> returnOk (ACKIrq w) \<lbrace>\<lambda>r _. False\<rbrace>, -) \<and> (invocation_type label \<noteq> GenInvocationLabel IRQAckIRQ \<longrightarrow> \<lbrace>?P'3\<rbrace> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, -)))
 3. \<And>sa. \<lbrakk>transform_intent (invocation_type label) args = None; cap = IRQHandlerCap w; s = sa\<rbrakk> \<Longrightarrow> s = sa \<and> ?P'3 sa proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(case invocation_type label of GenInvocationLabel InvalidInvocation \<Rightarrow> None | GenInvocationLabel UntypedRetype \<Rightarrow> map_option UntypedIntent (transform_intent_untyped_retype args) | GenInvocationLabel TCBReadRegisters \<Rightarrow> map_option TcbIntent (transform_intent_tcb_read_registers args) | GenInvocationLabel TCBWriteRegisters \<Rightarrow> map_option TcbIntent (transform_intent_tcb_write_registers args) | GenInvocationLabel TCBCopyRegisters \<Rightarrow> map_option TcbIntent (transform_intent_tcb_copy_registers args) | GenInvocationLabel TCBConfigure \<Rightarrow> map_option TcbIntent (transform_intent_tcb_configure args) | GenInvocationLabel TCBSetPriority \<Rightarrow> map_option TcbIntent (transform_intent_tcb_set_priority args) | GenInvocationLabel TCBSetMCPriority \<Rightarrow> map_option TcbIntent (transform_intent_tcb_set_mcpriority args) | GenInvocationLabel TCBSetSchedParams \<Rightarrow> map_option TcbIntent (transform_intent_tcb_set_sched_params args) | GenInvocationLabel TCBSetIPCBuffer \<Rightarrow> map_option TcbIntent (transform_intent_tcb_set_ipc_buffer args) | GenInvocationLabel TCBSetSpace \<Rightarrow> map_option TcbIntent (transform_intent_tcb_set_space args) | GenInvocationLabel TCBSuspend \<Rightarrow> Some (TcbIntent TcbSuspendIntent) | GenInvocationLabel TCBResume \<Rightarrow> Some (TcbIntent TcbResumeIntent) | GenInvocationLabel TCBBindNotification \<Rightarrow> Some (TcbIntent TcbBindNTFNIntent) | GenInvocationLabel TCBUnbindNotification \<Rightarrow> Some (TcbIntent TcbUnbindNTFNIntent) | GenInvocationLabel TCBSetTLSBase \<Rightarrow> Some (TcbIntent TcbSetTLSBaseIntent) | GenInvocationLabel CNodeRevoke \<Rightarrow> map_option CNodeIntent (transform_cnode_index_and_depth CNodeRevokeIntent args) | GenInvocationLabel CNodeDelete \<Rightarrow> map_option CNodeIntent (transform_cnode_index_and_depth CNodeDeleteIntent args) | GenInvocationLabel CNodeCancelBadgedSends \<Rightarrow> map_option CNodeIntent (transform_cnode_index_and_depth CNodeCancelBadgedSendsIntent args) | GenInvocationLabel CNodeCopy \<Rightarrow> map_option CNodeIntent (transform_intent_cnode_copy args) | GenInvocationLabel CNodeMint \<Rightarrow> map_option CNodeIntent (transform_intent_cnode_mint args) | GenInvocationLabel CNodeMove \<Rightarrow> map_option CNodeIntent (transform_intent_cnode_move args) | GenInvocationLabel CNodeMutate \<Rightarrow> map_option CNodeIntent (transform_intent_cnode_mutate args) | GenInvocationLabel CNodeRotate \<Rightarrow> map_option CNodeIntent (transform_intent_cnode_rotate args) | GenInvocationLabel CNodeSaveCaller \<Rightarrow> map_option CNodeIntent (transform_cnode_index_and_depth CNodeSaveCallerIntent args) | GenInvocationLabel IRQIssueIRQHandler \<Rightarrow> map_option IrqControlIntent (transform_intent_issue_irq_handler args) | GenInvocationLabel IRQAckIRQ \<Rightarrow> Some (IrqHandlerIntent IrqHandlerAckIntent) | GenInvocationLabel IRQSetIRQHandler \<Rightarrow> Some (IrqHandlerIntent IrqHandlerSetEndpointIntent) | GenInvocationLabel IRQClearIRQHandler \<Rightarrow> Some (IrqHandlerIntent IrqHandlerClearIntent) | GenInvocationLabel DomainSetSet \<Rightarrow> map_option DomainIntent (transform_intent_domain args) | ArchInvocationLabel ARMPageTableMap \<Rightarrow> map_option PageTableIntent (transform_intent_page_table_map args) | ArchInvocationLabel ARMPageTableUnmap \<Rightarrow> Some (PageTableIntent PageTableUnmapIntent) | ArchInvocationLabel ARMPageMap \<Rightarrow> map_option PageIntent (transform_intent_page_map args) | ArchInvocationLabel ARMPageUnmap \<Rightarrow> Some (PageIntent PageUnmapIntent) | ArchInvocationLabel ARMPageClean_Data \<Rightarrow> Some (PageIntent PageFlushCachesIntent) | ArchInvocationLabel ARMPageInvalidate_Data \<Rightarrow> Some (PageIntent PageFlushCachesIntent) | ArchInvocationLabel ARMPageCleanInvalidate_Data \<Rightarrow> Some (PageIntent PageFlushCachesIntent) | ArchInvocationLabel ARMPageUnify_Instruction \<Rightarrow> Some (PageIntent PageFlushCachesIntent) | ArchInvocationLabel ARMPageGetAddress \<Rightarrow> Some (PageIntent PageGetAddressIntent) | ArchInvocationLabel ARMASIDControlMakePool \<Rightarrow> map_option AsidControlIntent (transform_cnode_index_and_depth AsidControlMakePoolIntent args) | ArchInvocationLabel ARMASIDPoolAssign \<Rightarrow> Some (AsidPoolIntent AsidPoolAssignIntent) | ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> map_option IrqControlIntent (arch_transform_intent_issue_irq_handler args) | ArchInvocationLabel _ \<Rightarrow> Some (PageDirectoryIntent PageDirectoryFlushIntent)) = None; cap = IRQHandlerCap w; invocation_type label \<noteq> GenInvocationLabel IRQClearIRQHandler\<rbrakk> \<Longrightarrow> (excaps \<noteq> [] \<longrightarrow> (invocation_type label = GenInvocationLabel IRQSetIRQHandler \<longrightarrow> \<lbrace>?P'3\<rbrace> case hd excaps of (cap, slot) \<Rightarrow> if Structures_A.is_ntfn_cap cap \<and> AllowWrite \<in> Structures_A.cap_rights cap then returnOk $ SetIRQHandler w cap slot else throwError $ InvalidCapability 0 \<lbrace>\<lambda>r _. False\<rbrace>, -) \<and> (invocation_type label \<noteq> GenInvocationLabel IRQSetIRQHandler \<longrightarrow> (invocation_type label = GenInvocationLabel IRQAckIRQ \<longrightarrow> \<lbrace>?P'3\<rbrace> returnOk (ACKIrq w) \<lbrace>\<lambda>r _. False\<rbrace>, -) \<and> (invocation_type label \<noteq> GenInvocationLabel IRQAckIRQ \<longrightarrow> \<lbrace>?P'3\<rbrace> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, -))) \<and> (excaps = [] \<longrightarrow> (invocation_type label = GenInvocationLabel IRQSetIRQHandler \<longrightarrow> \<lbrace>?P'3\<rbrace> throwError TruncatedMessage \<lbrace>\<lambda>r _. False\<rbrace>, -) \<and> (invocation_type label \<noteq> GenInvocationLabel IRQSetIRQHandler \<longrightarrow> (invocation_type label = GenInvocationLabel IRQAckIRQ \<longrightarrow> \<lbrace>?P'3\<rbrace> returnOk (ACKIrq w) \<lbrace>\<lambda>r _. False\<rbrace>, -) \<and> (invocation_type label \<noteq> GenInvocationLabel IRQAckIRQ \<longrightarrow> \<lbrace>?P'3\<rbrace> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, -)))
 2. \<And>sa. \<lbrakk>transform_intent (invocation_type label) args = None; cap = IRQHandlerCap w; s = sa\<rbrakk> \<Longrightarrow> s = sa \<and> ?P'3 sa proof (prove)
goal:
No subgoals!