theory Syscall_DR

lemma transform_intent_thread_cap_None:
  "\<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.ThreadCap 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>" including no_pre apply (clarsimp simp:Decode_A.decode_invocation_def) apply wp+ apply (simp add:Decode_A.decode_tcb_invocation_def) apply (cases "gen_invocation_type label"; simp; wp?) apply (clarsimp simp: transform_intent_def decode_read_registers_def decode_write_registers_def
                                     decode_copy_registers_def decode_tcb_configure_def decode_set_priority_def
                                     decode_set_mcpriority_def decode_set_sched_params_def
                                     decode_set_ipc_buffer_def transform_intent_tcb_defs
                              simp flip: gen_invocation_type_eq
                              split: list.split_asm
                     | wp+)+ apply (clarsimp simp: transform_intent_def decode_set_space_def decode_bind_notification_def
                               decode_unbind_notification_def transform_intent_tcb_set_space_def
                        split: list.split_asm
               , wp+
               | clarsimp simp: transform_intent_def simp flip: gen_invocation_type_eq)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = ThreadCap 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 = ThreadCap 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 = ThreadCap w\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> liftME InvokeTCB (Decode_A.decode_tcb_invocation label args (ThreadCap w) slot 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 = ThreadCap w\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_tcb_invocation label args (ThreadCap w) slot excaps \<lbrace>(\<lambda>r _. False) \<circ> InvokeTCB\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = ThreadCap w\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label of TCBReadRegisters \<Rightarrow> decode_read_registers args (ThreadCap w) | TCBWriteRegisters \<Rightarrow> decode_write_registers args (ThreadCap w) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args (ThreadCap w) $ map fst excaps | TCBConfigure \<Rightarrow> decode_tcb_configure args (ThreadCap w) slot excaps | TCBSetPriority \<Rightarrow> decode_set_priority args (ThreadCap w) slot excaps | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args (ThreadCap w) slot excaps | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args (ThreadCap w) slot excaps | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args (ThreadCap w) slot excaps | TCBSetSpace \<Rightarrow> decode_set_space args (ThreadCap w) slot excaps | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap w) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap w) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap w) excaps | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap w) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args (ThreadCap w) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (14 subgoals):
 1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = ThreadCap w; gen_invocation_type label = TCBReadRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> decode_read_registers args (ThreadCap w) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 2. \<lbrakk>transform_intent (invocation_type label) args = None; cap = ThreadCap w; gen_invocation_type label = TCBWriteRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> decode_write_registers args (ThreadCap w) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 3. \<lbrakk>transform_intent (invocation_type label) args = None; cap = ThreadCap w; gen_invocation_type label = TCBCopyRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> decode_copy_registers args (ThreadCap w) (map fst excaps) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 4. \<lbrakk>transform_intent (invocation_type label) args = None; cap = ThreadCap w; gen_invocation_type label = TCBConfigure\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> decode_tcb_configure args (ThreadCap w) slot excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 5. \<lbrakk>transform_intent (invocation_type label) args = None; cap = ThreadCap w; gen_invocation_type label = TCBSetPriority\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> decode_set_priority args (ThreadCap w) slot excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 6. \<lbrakk>transform_intent (invocation_type label) args = None; cap = ThreadCap w; gen_invocation_type label = TCBSetMCPriority\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> decode_set_mcpriority args (ThreadCap w) slot excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 7. \<lbrakk>transform_intent (invocation_type label) args = None; cap = ThreadCap w; gen_invocation_type label = TCBSetSchedParams\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> decode_set_sched_params args (ThreadCap w) slot excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 8. \<lbrakk>transform_intent (invocation_type label) args = None; cap = ThreadCap w; gen_invocation_type label = TCBSetIPCBuffer\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> decode_set_ipc_buffer args (ThreadCap w) slot excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 9. \<lbrakk>transform_intent (invocation_type label) args = None; cap = ThreadCap w; gen_invocation_type label = TCBSetSpace\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> decode_set_space args (ThreadCap w) slot excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 10. \<lbrakk>transform_intent (invocation_type label) args = None; cap = ThreadCap w; gen_invocation_type label = TCBSuspend\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> returnOk (tcb_invocation.Suspend w) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
A total of 14 subgoals... proof (prove)
goal (8 subgoals):
 1. \<lbrakk>cap = ThreadCap w; invocation_type label = GenInvocationLabel TCBSetSpace; args = []\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> decode_set_space [] (ThreadCap w) slot excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 2. \<And>x21. \<lbrakk>cap = ThreadCap w; invocation_type label = GenInvocationLabel TCBSetSpace; args = [x21]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> decode_set_space [x21] (ThreadCap w) slot excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 3. \<And>x21 x21a. \<lbrakk>cap = ThreadCap w; invocation_type label = GenInvocationLabel TCBSetSpace; args = [x21, x21a]\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> decode_set_space [x21, x21a] (ThreadCap w) slot excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 4. \<lbrakk>transform_intent (invocation_type label) args = None; cap = ThreadCap w; gen_invocation_type label = TCBSuspend\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> returnOk (tcb_invocation.Suspend w) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 5. \<lbrakk>transform_intent (invocation_type label) args = None; cap = ThreadCap w; gen_invocation_type label = TCBResume\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> returnOk (tcb_invocation.Resume w) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 6. \<lbrakk>transform_intent (invocation_type label) args = None; cap = ThreadCap w; gen_invocation_type label = TCBBindNotification\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> decode_bind_notification (ThreadCap w) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 7. \<lbrakk>transform_intent (invocation_type label) args = None; cap = ThreadCap w; gen_invocation_type label = TCBUnbindNotification\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> decode_unbind_notification (ThreadCap w) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 8. \<lbrakk>transform_intent (invocation_type label) args = None; cap = ThreadCap w; gen_invocation_type label = TCBSetTLSBase\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> decode_set_tls_base args (ThreadCap w) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal:
No subgoals!