theory Invocation_DP

lemma syscall_valid_helper:
  "\<lbrakk> \<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>;
     \<And>r. \<lbrace>Qi r\<rbrace>arg_decode_fn r \<lbrace>Qa r\<rbrace>,\<lbrace>\<lambda>r s. False\<rbrace>;
    \<lbrace>P\<rbrace>cap_decoder_fn \<lbrace>Qi\<rbrace>,\<lbrace>\<lambda>r s. False\<rbrace>
   \<rbrakk> \<Longrightarrow>
   \<lbrace>P\<rbrace>syscall cap_decoder_fn decode_error_handler
    arg_decode_fn arg_error_handler_fn
    perform_syscall_fn
   \<lbrace>Q\<rbrace>,\<lbrace>\<lambda>r. Inv\<rbrace>" apply (simp add:syscall_def) apply (rule hoare_vcg_handle_elseE) apply simp apply simp apply (rule hoare_vcg_handle_elseE) apply fastforce apply (rule hoare_FalseE) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> syscall cap_decoder_fn decode_error_handler arg_decode_fn arg_error_handler_fn perform_syscall_fn \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> cap_decoder_fn <handle> \<lambda>_. liftE decode_error_handler <else> \<lambda>a. arg_decode_fn a <handle> \<lambda>_. liftE arg_error_handler_fn <else> perform_syscall_fn \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> cap_decoder_fn \<lbrace>?Q\<rbrace>, \<lbrace>?E\<rbrace>
 2. \<And>e. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?E e\<rbrace> liftE decode_error_handler \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>
 3. \<And>x. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q x\<rbrace> arg_decode_fn x <handle> \<lambda>_. liftE arg_error_handler_fn <else> perform_syscall_fn \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>e. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. False\<rbrace> liftE decode_error_handler \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>
 2. \<And>x. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>Qi x\<rbrace> arg_decode_fn x <handle> \<lambda>_. liftE arg_error_handler_fn <else> perform_syscall_fn \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>Qi x\<rbrace> arg_decode_fn x <handle> \<lambda>_. liftE arg_error_handler_fn <else> perform_syscall_fn \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>Qi x\<rbrace> arg_decode_fn x \<lbrace>?Q4 x\<rbrace>, \<lbrace>?E4 x\<rbrace>
 2. \<And>x e. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?E4 x e\<rbrace> liftE arg_error_handler_fn \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>
 3. \<And>x xa. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q4 x xa\<rbrace> perform_syscall_fn xa \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x e. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. False\<rbrace> liftE arg_error_handler_fn \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>
 2. \<And>x xa. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace> proof (prove)
goal:
No subgoals!