theory Arch_DP

lemma decode_invocation_invER[wp]:
  "\<lbrace>P and Q\<rbrace> decode_invocation a b c d\<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. Q\<rbrace>" apply (simp add:decode_invocation_def) apply (case_tac a,simp_all) apply (rule hoare_pre, (wp | simp add:throw_opt_def | wpc | intro conjI impI)+)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and Q\<rbrace> decode_invocation a b c d \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and Q\<rbrace> case a of UntypedCap x xa xb \<Rightarrow> doE untyped_intent <- throw_opt undefined $ get_untyped_intent d;
liftME InvokeUntyped $ decode_untyped_invocation a b c untyped_intent
odE | EndpointCap o_id badge rights \<Rightarrow> if AllowWrite \<in> rights then returnOk $ InvokeEndpoint (SyncMessage badge (AllowGrant \<in> rights) (AllowGrantReply \<in> rights) o_id) else throw | NotificationCap o_id badge rights \<Rightarrow> if AllowWrite \<in> rights then returnOk $ InvokeNotification (Signal badge o_id) else throw | ReplyCap o_id rights \<Rightarrow> returnOk $ InvokeReply (ReplyMessage o_id b (AllowGrant \<in> rights)) | CNodeCap x xa xb xc \<Rightarrow> doE cnode_intent <- throw_opt undefined $ get_cnode_intent d;
liftME InvokeCNode $ decode_cnode_invocation a b c cnode_intent
odE | TcbCap x \<Rightarrow> doE tcb_intent <- throw_opt undefined $ get_tcb_intent d;
liftME InvokeTcb $ decode_tcb_invocation a b c tcb_intent
odE | DomainCap \<Rightarrow> doE domain_intent <- throw_opt undefined $ get_domain_intent d;
liftME InvokeDomain $ decode_domain_invocation c domain_intent
odE | IrqControlCap \<Rightarrow> doE irq_control_intent <- throw_opt undefined $ get_irq_control_intent d;
liftME InvokeIrqControl $ decode_irq_control_invocation a b c irq_control_intent
odE | IrqHandlerCap x \<Rightarrow> doE irq_handler_intent <- throw_opt undefined $ get_irq_handler_intent d;
liftME InvokeIrqHandler $ decode_irq_handler_invocation a b c irq_handler_intent
odE | FrameCap x xa xb xc xd xe \<Rightarrow> doE page_intent <- throw_opt undefined $ get_page_intent d;
liftME InvokePage $ decode_page_invocation a b c page_intent
odE | PageTableCap x xa xb \<Rightarrow> doE page_table_intent <- throw_opt undefined $ get_page_table_intent d;
liftME InvokePageTable $ decode_page_table_invocation a b c page_table_intent
odE | PageDirectoryCap x xa xb \<Rightarrow> doE page_directory_intent <- throw_opt undefined $ get_page_directory_intent d;
liftME InvokePageDirectory $ decode_page_directory_invocation a b c page_directory_intent
odE | AsidControlCap \<Rightarrow> doE asid_control_intent <- throw_opt undefined $ get_asid_control_intent d;
liftME InvokeAsidControl $ decode_asid_control_invocation a b c asid_control_intent
odE | AsidPoolCap x xa \<Rightarrow> doE asid_pool_intent <- throw_opt undefined $ get_asid_pool_intent d;
liftME InvokeAsidPool $ decode_asid_pool_invocation a b c asid_pool_intent
odE | _ \<Rightarrow> throw \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (27 subgoals):
 1. a = NullCap \<Longrightarrow> \<lbrace>P and Q\<rbrace> throw \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. Q\<rbrace>
 2. \<And>x21 x22 x23. a = UntypedCap x21 x22 x23 \<Longrightarrow> \<lbrace>P and Q\<rbrace> doE untyped_intent <- throw_opt undefined (get_untyped_intent d);
liftME InvokeUntyped (decode_untyped_invocation (UntypedCap x21 x22 x23) b c untyped_intent)
odE \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. Q\<rbrace>
 3. \<And>x31 x32 x33. a = EndpointCap x31 x32 x33 \<Longrightarrow> (AllowWrite \<in> x33 \<longrightarrow> \<lbrace>P and Q\<rbrace> returnOk (InvokeEndpoint (SyncMessage x32 (AllowGrant \<in> x33) (AllowGrantReply \<in> x33) x31)) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. Q\<rbrace>) \<and> (AllowWrite \<notin> x33 \<longrightarrow> \<lbrace>P and Q\<rbrace> throw \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. Q\<rbrace>)
 4. \<And>x41 x42 x43. a = NotificationCap x41 x42 x43 \<Longrightarrow> (AllowWrite \<in> x43 \<longrightarrow> \<lbrace>P and Q\<rbrace> returnOk (InvokeNotification (Signal x42 x41)) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. Q\<rbrace>) \<and> (AllowWrite \<notin> x43 \<longrightarrow> \<lbrace>P and Q\<rbrace> throw \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. Q\<rbrace>)
 5. \<And>x51 x52. a = ReplyCap x51 x52 \<Longrightarrow> \<lbrace>P and Q\<rbrace> returnOk (InvokeReply (ReplyMessage x51 b (AllowGrant \<in> x52))) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. Q\<rbrace>
 6. \<And>x6. a = MasterReplyCap x6 \<Longrightarrow> \<lbrace>P and Q\<rbrace> throw \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. Q\<rbrace>
 7. \<And>x71 x72 x73 x74. a = CNodeCap x71 x72 x73 x74 \<Longrightarrow> \<lbrace>P and Q\<rbrace> doE cnode_intent <- throw_opt undefined (get_cnode_intent d);
liftME InvokeCNode (decode_cnode_invocation (CNodeCap x71 x72 x73 x74) b c cnode_intent)
odE \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. Q\<rbrace>
 8. \<And>x8. a = TcbCap x8 \<Longrightarrow> \<lbrace>P and Q\<rbrace> doE tcb_intent <- throw_opt undefined (get_tcb_intent d);
liftME InvokeTcb (decode_tcb_invocation (TcbCap x8) b c tcb_intent)
odE \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. Q\<rbrace>
 9. a = DomainCap \<Longrightarrow> \<lbrace>P and Q\<rbrace> doE domain_intent <- throw_opt undefined (get_domain_intent d);
liftME InvokeDomain (decode_domain_invocation c domain_intent)
odE \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. Q\<rbrace>
 10. \<And>x101 x102 x103 x104 x105 x106. a = PendingSyncSendCap x101 x102 x103 x104 x105 x106 \<Longrightarrow> \<lbrace>P and Q\<rbrace> throw \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. Q\<rbrace>
A total of 27 subgoals... proof (prove)
goal:
No subgoals!