theory Invocation_DP

lemma syscall_valid_helper_allow_error:
  "\<lbrakk> \<And>x xa. \<lbrace>Qa x xa \<rbrace> perform_syscall_fn xa
     \<lbrace>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>;
     \<And>r. \<lbrace>Qi r\<rbrace>arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>ret. P\<rbrace>;
    \<lbrace>Pre\<rbrace>cap_decoder_fn \<lbrace>Qi\<rbrace>,\<lbrace>\<lambda>r s. False\<rbrace>;
    \<lbrace>P\<rbrace>mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>rv s. P s\<rbrace>;
    \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>\<lambda>ya. P\<rbrace>;
    \<And>s. Pre s \<Longrightarrow> P s
   \<rbrakk> \<Longrightarrow>
   \<lbrace>Pre and (\<lambda>s. \<not> tcb_has_error thread_ptr s) \<rbrace>syscall cap_decoder_fn decode_error_handler
    arg_decode_fn
    (do ya \<leftarrow> corrupt_ipc_buffer thread_ptr True;
        mark_tcb_intent_error thread_ptr True
    od)
    perform_syscall_fn
   \<lbrace>\<lambda>r s. (\<not> tcb_has_error thread_ptr s \<longrightarrow> Q s)
       \<and>  (tcb_has_error thread_ptr s \<longrightarrow> P s)\<rbrace>,\<lbrace>\<lambda>r. Inv\<rbrace>" apply (simp add:syscall_def) apply (rule hoare_vcg_handle_elseE) apply (erule hoare_pre) apply simp apply simp apply (rule hoare_vcg_handle_elseE) apply assumption including no_pre apply wp apply (wp mark_tcb_intent_error_no_error) apply (rule hoare_drop_imp,simp) apply simp apply (rule hoare_post_impErr) apply fastforce apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>ret. P\<rbrace>; \<lbrace>Pre\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>rv. P\<rbrace>; \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>\<lambda>ya. P\<rbrace>; \<And>s. Pre s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> \<lbrace>Pre and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<rbrace> syscall cap_decoder_fn decode_error_handler arg_decode_fn (do ya <- corrupt_ipc_buffer thread_ptr True;
mark_tcb_intent_error thread_ptr True
od) perform_syscall_fn \<lbrace>\<lambda>r s. (\<not> tcb_has_error thread_ptr s \<longrightarrow> Q s) \<and> (tcb_has_error thread_ptr s \<longrightarrow> P s)\<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>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>ret. P\<rbrace>; \<lbrace>Pre\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>rv. P\<rbrace>; \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>\<lambda>ya. P\<rbrace>; \<And>s. Pre s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> \<lbrace>Pre and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<rbrace> cap_decoder_fn <handle> \<lambda>_. liftE decode_error_handler <else> \<lambda>a. arg_decode_fn a <handle> \<lambda>_. liftE (do ya <- corrupt_ipc_buffer thread_ptr True;
mark_tcb_intent_error thread_ptr True
od) <else> perform_syscall_fn \<lbrace>\<lambda>r s. (\<not> tcb_has_error thread_ptr s \<longrightarrow> Q s) \<and> (tcb_has_error thread_ptr s \<longrightarrow> P s)\<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>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>ret. P\<rbrace>; \<lbrace>Pre\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>rv. P\<rbrace>; \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>\<lambda>ya. P\<rbrace>; \<And>s. Pre s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> \<lbrace>Pre and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<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>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>ret. P\<rbrace>; \<lbrace>Pre\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>rv. P\<rbrace>; \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>\<lambda>ya. P\<rbrace>; \<And>s. Pre s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> \<lbrace>?E e\<rbrace> liftE decode_error_handler \<lbrace>\<lambda>r s. (\<not> tcb_has_error thread_ptr s \<longrightarrow> Q s) \<and> (tcb_has_error thread_ptr s \<longrightarrow> P s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>
 3. \<And>x. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>ret. P\<rbrace>; \<lbrace>Pre\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>rv. P\<rbrace>; \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>\<lambda>ya. P\<rbrace>; \<And>s. Pre s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> \<lbrace>?Q x\<rbrace> arg_decode_fn x <handle> \<lambda>_. liftE (do ya <- corrupt_ipc_buffer thread_ptr True;
mark_tcb_intent_error thread_ptr True
od) <else> perform_syscall_fn \<lbrace>\<lambda>r s. (\<not> tcb_has_error thread_ptr s \<longrightarrow> Q s) \<and> (tcb_has_error thread_ptr s \<longrightarrow> P s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>ret. P\<rbrace>; \<lbrace>P\<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>rv. P\<rbrace>; \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>\<lambda>ya. P\<rbrace>; \<And>s. Pre s \<Longrightarrow> P s; (Pre and (\<lambda>s. \<not> tcb_has_error thread_ptr s)) s\<rbrakk> \<Longrightarrow> Pre s
 2. \<And>e. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>ret. P\<rbrace>; \<lbrace>Pre\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>rv. P\<rbrace>; \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>\<lambda>ya. P\<rbrace>; \<And>s. Pre s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. False\<rbrace> liftE decode_error_handler \<lbrace>\<lambda>r s. (\<not> tcb_has_error thread_ptr s \<longrightarrow> Q s) \<and> (tcb_has_error thread_ptr s \<longrightarrow> P s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>
 3. \<And>x. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>ret. P\<rbrace>; \<lbrace>Pre\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>rv. P\<rbrace>; \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>\<lambda>ya. P\<rbrace>; \<And>s. Pre s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> \<lbrace>Qi x\<rbrace> arg_decode_fn x <handle> \<lambda>_. liftE (do ya <- corrupt_ipc_buffer thread_ptr True;
mark_tcb_intent_error thread_ptr True
od) <else> perform_syscall_fn \<lbrace>\<lambda>r s. (\<not> tcb_has_error thread_ptr s \<longrightarrow> Q s) \<and> (tcb_has_error thread_ptr s \<longrightarrow> P s)\<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>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>ret. P\<rbrace>; \<lbrace>Pre\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>rv. P\<rbrace>; \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>\<lambda>ya. P\<rbrace>; \<And>s. Pre s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. False\<rbrace> liftE decode_error_handler \<lbrace>\<lambda>r s. (\<not> tcb_has_error thread_ptr s \<longrightarrow> Q s) \<and> (tcb_has_error thread_ptr s \<longrightarrow> P s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>
 2. \<And>x. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>ret. P\<rbrace>; \<lbrace>Pre\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>rv. P\<rbrace>; \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>\<lambda>ya. P\<rbrace>; \<And>s. Pre s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> \<lbrace>Qi x\<rbrace> arg_decode_fn x <handle> \<lambda>_. liftE (do ya <- corrupt_ipc_buffer thread_ptr True;
mark_tcb_intent_error thread_ptr True
od) <else> perform_syscall_fn \<lbrace>\<lambda>r s. (\<not> tcb_has_error thread_ptr s \<longrightarrow> Q s) \<and> (tcb_has_error thread_ptr s \<longrightarrow> P s)\<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>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>ret. P\<rbrace>; \<lbrace>Pre\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>rv. P\<rbrace>; \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>\<lambda>ya. P\<rbrace>; \<And>s. Pre s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> \<lbrace>Qi x\<rbrace> arg_decode_fn x <handle> \<lambda>_. liftE (do ya <- corrupt_ipc_buffer thread_ptr True;
mark_tcb_intent_error thread_ptr True
od) <else> perform_syscall_fn \<lbrace>\<lambda>r s. (\<not> tcb_has_error thread_ptr s \<longrightarrow> Q s) \<and> (tcb_has_error thread_ptr s \<longrightarrow> P s)\<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>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>ret. P\<rbrace>; \<lbrace>Pre\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>rv. P\<rbrace>; \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>\<lambda>ya. P\<rbrace>; \<And>s. Pre s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> \<lbrace>Qi x\<rbrace> arg_decode_fn x \<lbrace>?Q6 x\<rbrace>, \<lbrace>?E6 x\<rbrace>
 2. \<And>x e. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>ret. P\<rbrace>; \<lbrace>Pre\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>rv. P\<rbrace>; \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>\<lambda>ya. P\<rbrace>; \<And>s. Pre s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> \<lbrace>?E6 x e\<rbrace> liftE (do ya <- corrupt_ipc_buffer thread_ptr True;
mark_tcb_intent_error thread_ptr True
od) \<lbrace>\<lambda>r s. (\<not> tcb_has_error thread_ptr s \<longrightarrow> Q s) \<and> (tcb_has_error thread_ptr s \<longrightarrow> P s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>
 3. \<And>x xa. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>ret. P\<rbrace>; \<lbrace>Pre\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>rv. P\<rbrace>; \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>\<lambda>ya. P\<rbrace>; \<And>s. Pre s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> \<lbrace>?Q6 x xa\<rbrace> perform_syscall_fn xa \<lbrace>\<lambda>r s. (\<not> tcb_has_error thread_ptr s \<longrightarrow> Q s) \<and> (tcb_has_error thread_ptr s \<longrightarrow> P s)\<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>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>ret. P\<rbrace>; \<lbrace>Pre\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>rv. P\<rbrace>; \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>\<lambda>ya. P\<rbrace>; \<And>s. Pre s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> liftE (do ya <- corrupt_ipc_buffer thread_ptr True;
mark_tcb_intent_error thread_ptr True
od) \<lbrace>\<lambda>r s. (\<not> tcb_has_error thread_ptr s \<longrightarrow> Q s) \<and> (tcb_has_error thread_ptr s \<longrightarrow> P s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>
 2. \<And>x xa. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>ret. P\<rbrace>; \<lbrace>Pre\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>rv. P\<rbrace>; \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>\<lambda>ya. P\<rbrace>; \<And>s. Pre s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>\<lambda>r s. (\<not> tcb_has_error thread_ptr s \<longrightarrow> Q s) \<and> (tcb_has_error thread_ptr s \<longrightarrow> P s)\<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>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>ret. P\<rbrace>; \<lbrace>Pre\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>rv. P\<rbrace>; \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>\<lambda>ya. P\<rbrace>; \<And>s. Pre s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> liftE (do ya <- corrupt_ipc_buffer thread_ptr True;
mark_tcb_intent_error thread_ptr True
od) \<lbrace>\<lambda>r s. (\<not> tcb_has_error thread_ptr s \<longrightarrow> Q s) \<and> (tcb_has_error thread_ptr s \<longrightarrow> P s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>
 2. \<And>x xa. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>ret. P\<rbrace>; \<lbrace>Pre\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>rv. P\<rbrace>; \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>\<lambda>ya. P\<rbrace>; \<And>s. Pre s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>\<lambda>r s. (\<not> tcb_has_error thread_ptr s \<longrightarrow> Q s) \<and> (tcb_has_error thread_ptr s \<longrightarrow> P s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x e ya. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>ret. P\<rbrace>; \<lbrace>Pre\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>rv. P\<rbrace>; \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>\<lambda>ya. P\<rbrace>; \<And>s. Pre s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> \<lbrace>?B14 x e ya\<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>r s. (\<not> tcb_has_error thread_ptr s \<longrightarrow> Q s) \<and> (tcb_has_error thread_ptr s \<longrightarrow> P s)\<rbrace>
 2. \<And>x e. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>ret. P\<rbrace>; \<lbrace>Pre\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>rv. P\<rbrace>; \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>\<lambda>ya. P\<rbrace>; \<And>s. Pre s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>?B14 x e\<rbrace>
 3. \<And>x xa. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>ret. P\<rbrace>; \<lbrace>Pre\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>rv. P\<rbrace>; \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>\<lambda>ya. P\<rbrace>; \<And>s. Pre s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>\<lambda>r s. (\<not> tcb_has_error thread_ptr s \<longrightarrow> Q s) \<and> (tcb_has_error thread_ptr s \<longrightarrow> P s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x e ya. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>ret. P\<rbrace>; \<lbrace>Pre\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>rv. P\<rbrace>; \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>\<lambda>ya. P\<rbrace>; \<And>s. Pre s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> \<lbrace>?P'17 x e ya\<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>rv s. tcb_has_error thread_ptr s \<longrightarrow> P s\<rbrace>
 2. \<And>x e. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>ret. P\<rbrace>; \<lbrace>Pre\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>rv. P\<rbrace>; \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>\<lambda>ya. P\<rbrace>; \<And>s. Pre s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>\<lambda>ya s. True \<and> ?P'17 x e ya s\<rbrace>
 3. \<And>x xa. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>ret. P\<rbrace>; \<lbrace>Pre\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>rv. P\<rbrace>; \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>\<lambda>ya. P\<rbrace>; \<And>s. Pre s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>\<lambda>r s. (\<not> tcb_has_error thread_ptr s \<longrightarrow> Q s) \<and> (tcb_has_error thread_ptr s \<longrightarrow> P s)\<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>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>ret. P\<rbrace>; \<lbrace>Pre\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>rv. P\<rbrace>; \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>\<lambda>ya. P\<rbrace>; \<And>s. Pre s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>\<lambda>ya s. True \<and> P s\<rbrace>
 2. \<And>x xa. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>ret. P\<rbrace>; \<lbrace>Pre\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>rv. P\<rbrace>; \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>\<lambda>ya. P\<rbrace>; \<And>s. Pre s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>\<lambda>r s. (\<not> tcb_has_error thread_ptr s \<longrightarrow> Q s) \<and> (tcb_has_error thread_ptr s \<longrightarrow> P s)\<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>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>ret. P\<rbrace>; \<lbrace>Pre\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>rv. P\<rbrace>; \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>\<lambda>ya. P\<rbrace>; \<And>s. Pre s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>\<lambda>r s. (\<not> tcb_has_error thread_ptr s \<longrightarrow> Q s) \<and> (tcb_has_error thread_ptr s \<longrightarrow> P s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>ret. P\<rbrace>; \<lbrace>Pre\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>rv. P\<rbrace>; \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>\<lambda>ya. P\<rbrace>; \<And>s. Pre s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>?Q22 x xa\<rbrace>, \<lbrace>?E22 x xa\<rbrace>
 2. \<And>x xa rv s. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>ret. P\<rbrace>; \<lbrace>Pre\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>rv. P\<rbrace>; \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>\<lambda>ya. P\<rbrace>; \<And>s. Pre s \<Longrightarrow> P s; ?Q22 x xa rv s\<rbrakk> \<Longrightarrow> (\<not> tcb_has_error thread_ptr s \<longrightarrow> Q s) \<and> (tcb_has_error thread_ptr s \<longrightarrow> P s)
 3. \<And>x xa e s. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>ret. P\<rbrace>; \<lbrace>Pre\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>rv. P\<rbrace>; \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>\<lambda>ya. P\<rbrace>; \<And>s. Pre s \<Longrightarrow> P s; ?E22 x xa e s\<rbrakk> \<Longrightarrow> Inv s proof (prove)
goal (2 subgoals):
 1. \<And>x xa rv s. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>ret. P\<rbrace>; \<lbrace>Pre\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>rv. P\<rbrace>; \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>\<lambda>ya. P\<rbrace>; \<And>s. Pre s \<Longrightarrow> P s; (Q and (\<lambda>s. \<not> tcb_has_error thread_ptr s)) s\<rbrakk> \<Longrightarrow> (\<not> tcb_has_error thread_ptr s \<longrightarrow> Q s) \<and> (tcb_has_error thread_ptr s \<longrightarrow> P s)
 2. \<And>x xa e s. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>ret. P\<rbrace>; \<lbrace>Pre\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>rv. P\<rbrace>; \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>\<lambda>ya. P\<rbrace>; \<And>s. Pre s \<Longrightarrow> P s; Inv s\<rbrakk> \<Longrightarrow> Inv s proof (prove)
goal (1 subgoal):
 1. \<And>x xa e s. \<lbrakk>\<And>x xa. \<lbrace>Qa x xa\<rbrace> perform_syscall_fn xa \<lbrace>\<lambda>r. Q and (\<lambda>s. \<not> tcb_has_error thread_ptr s)\<rbrace>, \<lbrace>\<lambda>r. Inv\<rbrace>; \<And>r. \<lbrace>Qi r\<rbrace> arg_decode_fn r \<lbrace>Qa r\<rbrace>, \<lbrace>\<lambda>ret. P\<rbrace>; \<lbrace>Pre\<rbrace> cap_decoder_fn \<lbrace>Qi\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> mark_tcb_intent_error thread_ptr True \<lbrace>\<lambda>rv. P\<rbrace>; \<lbrace>P\<rbrace> corrupt_ipc_buffer thread_ptr True \<lbrace>\<lambda>ya. P\<rbrace>; \<And>s. Pre s \<Longrightarrow> P s; Inv s\<rbrakk> \<Longrightarrow> Inv s proof (prove)
goal:
No subgoals!