theory Tcb_C

lemma getSyscallArg_ccorres_foo':
  "ccorres (\<lambda>a rv. rv = ucast (args ! n)) (\<lambda>x. ucast (ret__unsigned_long_' x))
         (sysargs_rel args buffer and sysargs_rel_n args buffer n)
         (UNIV \<inter> \<lbrace>unat \<acute>i = n\<rbrace> \<inter> \<lbrace>\<acute>ipc_buffer = option_to_ptr buffer\<rbrace>) []
    (return ()) (Call getSyscallArg_'proc)" apply (insert getSyscallArg_ccorres_foo
          [where args=args and n=n and buffer=buffer]) apply (clarsimp simp: ccorres_underlying_def) apply  (erule (1) my_BallE) apply clarsimp apply (erule allE, erule allE, erule (1) impE) apply (clarsimp simp: return_def unif_rrel_def split: xstate.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>a rv. rv = UCAST(32 \<rightarrow> 'a) (args ! n)) (\<lambda>x. UCAST(32 \<rightarrow> 'a) (ret__unsigned_long_' x)) (sysargs_rel args buffer and sysargs_rel_n args buffer n) (UNIV \<inter> \<lbrace>unat \<acute>i = n\<rbrace> \<inter> \<lbrace>\<acute>ipc_buffer = option_to_ptr buffer\<rbrace>) [] (return ()) (Call getSyscallArg_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>a rv. rv = args ! n) ret__unsigned_long_' (sysargs_rel args buffer and sysargs_rel_n args buffer n) (UNIV \<inter> \<lbrace>unat \<acute>i = n\<rbrace> \<inter> \<lbrace>\<acute>ipc_buffer = option_to_ptr buffer\<rbrace>) [] (return ()) (Call getSyscallArg_'proc) \<Longrightarrow> ccorres (\<lambda>a rv. rv = UCAST(32 \<rightarrow> 'a) (args ! n)) (\<lambda>x. UCAST(32 \<rightarrow> 'a) (ret__unsigned_long_' x)) (sysargs_rel args buffer and sysargs_rel_n args buffer n) (UNIV \<inter> \<lbrace>unat \<acute>i = n\<rbrace> \<inter> \<lbrace>\<acute>ipc_buffer = option_to_ptr buffer\<rbrace>) [] (return ()) (Call getSyscallArg_'proc) proof (prove)
goal (1 subgoal):
 1. \<And>a b na t. \<lbrakk>\<forall>x\<in>rf_sr. case x of (s, s') \<Rightarrow> sysargs_rel args buffer s \<and> sysargs_rel_n args buffer (unat (i_' b)) s \<and> i_' s' = i_' b \<and> ipc_buffer_' s' = option_to_ptr buffer \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call getSyscallArg_'proc],s'\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (return () s). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length []) (\<lambda>a rv. rv = args ! unat (i_' b)) ret__unsigned_long_' (\<lambda>a rv. rv = args ! unat (i_' b)) ret__unsigned_long_' () s'' | _ \<Rightarrow> False)); (a, b) \<in> rf_sr; sysargs_rel args buffer a; sysargs_rel_n args buffer (unat (i_' b)) a; ipc_buffer_' b = option_to_ptr buffer; n = unat (i_' b); \<Gamma>\<turnstile>\<^sub>h \<langle>[Call getSyscallArg_'proc],b\<rangle> \<Rightarrow> (na, t)\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (return () a). (t, s'') \<in> rf_sr \<and> unif_rrel (na = length []) (\<lambda>a rv. rv = UCAST(32 \<rightarrow> 'a) (args ! unat (i_' b))) (\<lambda>x. UCAST(32 \<rightarrow> 'a) (ret__unsigned_long_' x)) (\<lambda>a rv. rv = UCAST(32 \<rightarrow> 'a) (args ! unat (i_' b))) (\<lambda>x. UCAST(32 \<rightarrow> 'a) (ret__unsigned_long_' x)) () s'' | _ \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; sysargs_rel args buffer a; sysargs_rel_n args buffer (unat (i_' b)) a; ipc_buffer_' b = option_to_ptr buffer; n = unat (i_' b); \<Gamma>\<turnstile>\<^sub>h \<langle>[Call getSyscallArg_'proc],b\<rangle> \<Rightarrow> (na, t); case (a, b) of (s, s') \<Rightarrow> sysargs_rel args buffer s \<and> sysargs_rel_n args buffer (unat (i_' b)) s \<and> i_' s' = i_' b \<and> ipc_buffer_' s' = option_to_ptr buffer \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call getSyscallArg_'proc],s'\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (return () s). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length []) (\<lambda>a rv. rv = args ! unat (i_' b)) ret__unsigned_long_' (\<lambda>a rv. rv = args ! unat (i_' b)) ret__unsigned_long_' () s'' | _ \<Rightarrow> False))\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (return () a). (t, s'') \<in> rf_sr \<and> unif_rrel (na = length []) (\<lambda>a rv. rv = UCAST(32 \<rightarrow> 'a) (args ! unat (i_' b))) (\<lambda>x. UCAST(32 \<rightarrow> 'a) (ret__unsigned_long_' x)) (\<lambda>a rv. rv = UCAST(32 \<rightarrow> 'a) (args ! unat (i_' b))) (\<lambda>x. UCAST(32 \<rightarrow> 'a) (ret__unsigned_long_' x)) () s'' | _ \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; sysargs_rel args buffer a; sysargs_rel_n args buffer (unat (i_' b)) a; ipc_buffer_' b = option_to_ptr buffer; n = unat (i_' b); \<Gamma>\<turnstile>\<^sub>h \<langle>[Call getSyscallArg_'proc],b\<rangle> \<Rightarrow> (na, t); \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call getSyscallArg_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (return () a). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length []) (\<lambda>a rv. rv = args ! unat (i_' b)) ret__unsigned_long_' (\<lambda>a rv. rv = args ! unat (i_' b)) ret__unsigned_long_' () s'' | _ \<Rightarrow> False)\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (return () a). (t, s'') \<in> rf_sr \<and> unif_rrel (na = length []) (\<lambda>a rv. rv = UCAST(32 \<rightarrow> 'a) (args ! unat (i_' b))) (\<lambda>x. UCAST(32 \<rightarrow> 'a) (ret__unsigned_long_' x)) (\<lambda>a rv. rv = UCAST(32 \<rightarrow> 'a) (args ! unat (i_' b))) (\<lambda>x. UCAST(32 \<rightarrow> 'a) (ret__unsigned_long_' x)) () s'' | _ \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b na t. \<lbrakk>(a, b) \<in> rf_sr; sysargs_rel args buffer a; sysargs_rel_n args buffer (unat (i_' b)) a; ipc_buffer_' b = option_to_ptr buffer; n = unat (i_' b); \<Gamma>\<turnstile>\<^sub>h \<langle>[Call getSyscallArg_'proc],b\<rangle> \<Rightarrow> (na, t); case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (return () a). (t, s'') \<in> rf_sr \<and> unif_rrel (na = length []) (\<lambda>a rv. rv = args ! unat (i_' b)) ret__unsigned_long_' (\<lambda>a rv. rv = args ! unat (i_' b)) ret__unsigned_long_' () s'' | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (return () a). (t, s'') \<in> rf_sr \<and> unif_rrel (na = length []) (\<lambda>a rv. rv = UCAST(32 \<rightarrow> 'a) (args ! unat (i_' b))) (\<lambda>x. UCAST(32 \<rightarrow> 'a) (ret__unsigned_long_' x)) (\<lambda>a rv. rv = UCAST(32 \<rightarrow> 'a) (args ! unat (i_' b))) (\<lambda>x. UCAST(32 \<rightarrow> 'a) (ret__unsigned_long_' x)) () s'' | _ \<Rightarrow> False proof (prove)
goal:
No subgoals!