theory Tcb_C

lemma invokeTCB_WriteRegisters_ccorres_helper:
  "\<lbrakk> unat (f (of_nat n)) = incn
         \<and> g (of_nat n) = register_from_H reg \<and> n'=incn
         \<and> of_nat n < bnd \<and> of_nat n < bnd2 \<rbrakk> \<Longrightarrow>
   ccorres dc xfdc (sysargs_rel args buffer and sysargs_rel_n args buffer n' and tcb_at' dst and P)
                   (\<lbrace>\<acute>i = of_nat n\<rbrace>) hs
     (asUser dst (setRegister reg
          (sanitiseRegister tcb reg (args ! incn))))
     (\<acute>ret__unsigned_long :== CALL getSyscallArg(f (\<acute>i),option_to_ptr buffer);;
      Guard ArrayBounds \<lbrace>\<acute>i < bnd\<rbrace>
          (\<acute>unsigned_long_eret_2 :== CALL sanitiseRegister(g (\<acute>i),\<acute>ret__unsigned_long,from_bool t));;
      Guard ArrayBounds \<lbrace>\<acute>i < bnd2\<rbrace>
        (CALL setRegister(tcb_ptr_to_ctcb_ptr dst,g (\<acute>i),\<acute>unsigned_long_eret_2)))" apply (rule ccorres_guard_imp2) apply (rule ccorres_add_return) apply (rule ccorres_rhs_assoc)+ apply (ctac add: getSyscallArg_ccorres_foo[where args=args and n="incn" and buffer=buffer]) apply (rule ccorres_symb_exec_r) apply (ctac add: setRegister_ccorres) apply vcg apply (rule conseqPre, vcg, clarsimp) apply wp apply simp apply (vcg exspec=getSyscallArg_modifies) apply (fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (f (word_of_nat n)) = incn \<and> g (word_of_nat n) = register_from_H reg \<and> n' = incn \<and> word_of_nat n < bnd \<and> word_of_nat n < bnd2 \<Longrightarrow> ccorres dc xfdc (sysargs_rel args buffer and sysargs_rel_n args buffer n' and tcb_at' dst and P) \<lbrace>\<acute>i = word_of_nat n\<rbrace> hs (asUser dst (setRegister reg (local.sanitiseRegister tcb reg (args ! incn)))) (\<acute>ret__unsigned_long :== CALL getSyscallArg_'proc(f \<acute>i,option_to_ptr buffer);;
Guard ArrayBounds \<lbrace>\<acute>i < bnd\<rbrace> (\<acute>unsigned_long_eret_2 :== CALL sanitiseRegister_'proc(g \<acute>i,\<acute>ret__unsigned_long,from_bool t));;
Guard ArrayBounds \<lbrace>\<acute>i < bnd2\<rbrace> (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr dst,g \<acute>i,\<acute>unsigned_long_eret_2))) proof (prove)
goal (2 subgoals):
 1. unat (f (word_of_nat n)) = incn \<and> g (word_of_nat n) = register_from_H reg \<and> n' = incn \<and> word_of_nat n < bnd \<and> word_of_nat n < bnd2 \<Longrightarrow> ccorres dc xfdc ?Q ?Q' hs (asUser dst (setRegister reg (local.sanitiseRegister tcb reg (args ! incn)))) (\<acute>ret__unsigned_long :== CALL getSyscallArg_'proc(f \<acute>i,option_to_ptr buffer);;
Guard ArrayBounds \<lbrace>\<acute>i < bnd\<rbrace> (\<acute>unsigned_long_eret_2 :== CALL sanitiseRegister_'proc(g \<acute>i,\<acute>ret__unsigned_long,from_bool t));;
Guard ArrayBounds \<lbrace>\<acute>i < bnd2\<rbrace> (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr dst,g \<acute>i,\<acute>unsigned_long_eret_2)))
 2. \<And>s s'. \<lbrakk>unat (f (word_of_nat n)) = incn \<and> g (word_of_nat n) = register_from_H reg \<and> n' = incn \<and> word_of_nat n < bnd \<and> word_of_nat n < bnd2; (s, s') \<in> rf_sr; (sysargs_rel args buffer and sysargs_rel_n args buffer n' and tcb_at' dst and P) s; s' \<in> \<lbrace>\<acute>i = word_of_nat n\<rbrace>\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (2 subgoals):
 1. unat (f (word_of_nat n)) = incn \<and> g (word_of_nat n) = register_from_H reg \<and> n' = incn \<and> word_of_nat n < bnd \<and> word_of_nat n < bnd2 \<Longrightarrow> ccorres dc xfdc ?Q ?Q' hs (do _ <- return ();
asUser dst (setRegister reg (local.sanitiseRegister tcb reg (args ! incn)))
od) (\<acute>ret__unsigned_long :== CALL getSyscallArg_'proc(f \<acute>i,option_to_ptr buffer);;
Guard ArrayBounds \<lbrace>\<acute>i < bnd\<rbrace> (\<acute>unsigned_long_eret_2 :== CALL sanitiseRegister_'proc(g \<acute>i,\<acute>ret__unsigned_long,from_bool t));;
Guard ArrayBounds \<lbrace>\<acute>i < bnd2\<rbrace> (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr dst,g \<acute>i,\<acute>unsigned_long_eret_2)))
 2. \<And>s s'. \<lbrakk>unat (f (word_of_nat n)) = incn \<and> g (word_of_nat n) = register_from_H reg \<and> n' = incn \<and> word_of_nat n < bnd \<and> word_of_nat n < bnd2; (s, s') \<in> rf_sr; (sysargs_rel args buffer and sysargs_rel_n args buffer n' and tcb_at' dst and P) s; s' \<in> \<lbrace>\<acute>i = word_of_nat n\<rbrace>\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (2 subgoals):
 1. unat (f (word_of_nat n)) = incn \<and> g (word_of_nat n) = register_from_H reg \<and> n' = incn \<and> word_of_nat n < bnd \<and> word_of_nat n < bnd2 \<Longrightarrow> ccorres dc xfdc ?Q ?Q' hs (do _ <- return ();
asUser dst (setRegister reg (local.sanitiseRegister tcb reg (args ! incn)))
od) (\<acute>ret__unsigned_long :== CALL getSyscallArg_'proc(f \<acute>i,option_to_ptr buffer);;
(Guard ArrayBounds \<lbrace>\<acute>i < bnd\<rbrace> (\<acute>unsigned_long_eret_2 :== CALL sanitiseRegister_'proc(g \<acute>i,\<acute>ret__unsigned_long,from_bool t));;
Guard ArrayBounds \<lbrace>\<acute>i < bnd2\<rbrace> (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr dst,g \<acute>i,\<acute>unsigned_long_eret_2))))
 2. \<And>s s'. \<lbrakk>unat (f (word_of_nat n)) = incn \<and> g (word_of_nat n) = register_from_H reg \<and> n' = incn \<and> word_of_nat n < bnd \<and> word_of_nat n < bnd2; (s, s') \<in> rf_sr; (sysargs_rel args buffer and sysargs_rel_n args buffer n' and tcb_at' dst and P) s; s' \<in> \<lbrace>\<acute>i = word_of_nat n\<rbrace>\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (4 subgoals):
 1. \<And>rv ret__unsigned_long. \<lbrakk>unat (f (word_of_nat n)) = incn \<and> g (word_of_nat n) = register_from_H reg \<and> n' = incn \<and> word_of_nat n < bnd \<and> word_of_nat n < bnd2; ret__unsigned_long = args ! incn\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q9 rv) (?Q'9 rv ret__unsigned_long) hs (asUser dst (setRegister reg (local.sanitiseRegister tcb reg (args ! incn)))) (Guard ArrayBounds \<lbrace>\<acute>i < bnd\<rbrace> (\<acute>unsigned_long_eret_2 :== CALL sanitiseRegister_'proc(g \<acute>i,ret__unsigned_long,from_bool t));;
Guard ArrayBounds \<lbrace>\<acute>i < bnd2\<rbrace> (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr dst,g \<acute>i,\<acute>unsigned_long_eret_2)))
 2. unat (f (word_of_nat n)) = incn \<and> g (word_of_nat n) = register_from_H reg \<and> n' = incn \<and> word_of_nat n < bnd \<and> word_of_nat n < bnd2 \<Longrightarrow> \<lbrace>?R9\<rbrace> return () \<lbrace>?Q9\<rbrace>
 3. unat (f (word_of_nat n)) = incn \<and> g (word_of_nat n) = register_from_H reg \<and> n' = incn \<and> word_of_nat n < bnd \<and> word_of_nat n < bnd2 \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'9 \<acute>ret__unsigned_long :== CALL getSyscallArg_'proc(f \<acute>i,option_to_ptr buffer) {s. \<forall>rv. ret__unsigned_long_' s = args ! incn \<longrightarrow> s \<in> ?Q'9 rv (ret__unsigned_long_' s)}
 4. \<And>s s'. \<lbrakk>unat (f (word_of_nat n)) = incn \<and> g (word_of_nat n) = register_from_H reg \<and> n' = incn \<and> word_of_nat n < bnd \<and> word_of_nat n < bnd2; (s, s') \<in> rf_sr; (sysargs_rel args buffer and sysargs_rel_n args buffer n' and tcb_at' dst and P) s; s' \<in> \<lbrace>\<acute>i = word_of_nat n\<rbrace>\<rbrakk> \<Longrightarrow> (sysargs_rel args buffer and sysargs_rel_n args buffer incn and ?R9) s \<and> s' \<in> {s. ipc_buffer_'_update (\<lambda>_. option_to_ptr buffer) (i_'_update (\<lambda>_. f (i_' s)) s) \<in> UNIV \<inter> \<lbrace>unat \<acute>i = incn\<rbrace> \<inter> \<lbrace>\<acute>ipc_buffer = option_to_ptr buffer\<rbrace>} \<inter> ?R'9 proof (prove)
goal (6 subgoals):
 1. \<And>rv ret__unsigned_long. \<lbrakk>unat (f (word_of_nat n)) = incn \<and> g (word_of_nat n) = register_from_H reg \<and> n' = incn \<and> word_of_nat n < bnd \<and> word_of_nat n < bnd2; ret__unsigned_long = args ! incn\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q9 rv) (?Q'85 rv ret__unsigned_long) hs (asUser dst (setRegister reg (local.sanitiseRegister tcb reg (args ! incn)))) (Guard ArrayBounds \<lbrace>\<acute>i < bnd2\<rbrace> (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr dst,g \<acute>i,\<acute>unsigned_long_eret_2)))
 2. \<And>rv ret__unsigned_long. \<lbrakk>unat (f (word_of_nat n)) = incn \<and> g (word_of_nat n) = register_from_H reg \<and> n' = incn \<and> word_of_nat n < bnd \<and> word_of_nat n < bnd2; ret__unsigned_long = args ! incn\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'9 rv ret__unsigned_long) Guard ArrayBounds \<lbrace>\<acute>i < bnd\<rbrace> (\<acute>unsigned_long_eret_2 :== CALL sanitiseRegister_'proc(g \<acute>i,ret__unsigned_long,from_bool t)) (?Q'85 rv ret__unsigned_long)
 3. \<And>rv ret__unsigned_long s. \<lbrakk>unat (f (word_of_nat n)) = incn \<and> g (word_of_nat n) = register_from_H reg \<and> n' = incn \<and> word_of_nat n < bnd \<and> word_of_nat n < bnd2; ret__unsigned_long = args ! incn; ?Q9 rv s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'9 rv ret__unsigned_long \<inter> {s'. (s, s') \<in> rf_sr}) Guard ArrayBounds \<lbrace>\<acute>i < bnd\<rbrace> (\<acute>unsigned_long_eret_2 :== CALL sanitiseRegister_'proc(g \<acute>i,ret__unsigned_long,from_bool t)) {s'. (s, s') \<in> rf_sr}
 4. unat (f (word_of_nat n)) = incn \<and> g (word_of_nat n) = register_from_H reg \<and> n' = incn \<and> word_of_nat n < bnd \<and> word_of_nat n < bnd2 \<Longrightarrow> \<lbrace>?R9\<rbrace> return () \<lbrace>?Q9\<rbrace>
 5. unat (f (word_of_nat n)) = incn \<and> g (word_of_nat n) = register_from_H reg \<and> n' = incn \<and> word_of_nat n < bnd \<and> word_of_nat n < bnd2 \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'9 \<acute>ret__unsigned_long :== CALL getSyscallArg_'proc(f \<acute>i,option_to_ptr buffer) {s. \<forall>rv. ret__unsigned_long_' s = args ! incn \<longrightarrow> s \<in> ?Q'9 rv (ret__unsigned_long_' s)}
 6. \<And>s s'. \<lbrakk>unat (f (word_of_nat n)) = incn \<and> g (word_of_nat n) = register_from_H reg \<and> n' = incn \<and> word_of_nat n < bnd \<and> word_of_nat n < bnd2; (s, s') \<in> rf_sr; (sysargs_rel args buffer and sysargs_rel_n args buffer n' and tcb_at' dst and P) s; s' \<in> \<lbrace>\<acute>i = word_of_nat n\<rbrace>\<rbrakk> \<Longrightarrow> (sysargs_rel args buffer and sysargs_rel_n args buffer incn and ?R9) s \<and> s' \<in> {s. ipc_buffer_'_update (\<lambda>_. option_to_ptr buffer) (i_'_update (\<lambda>_. f (i_' s)) s) \<in> UNIV \<inter> \<lbrace>unat \<acute>i = incn\<rbrace> \<inter> \<lbrace>\<acute>ipc_buffer = option_to_ptr buffer\<rbrace>} \<inter> ?R'9 proof (prove)
goal (5 subgoals):
 1. \<And>rv ret__unsigned_long. \<lbrakk>unat (f (word_of_nat n)) = incn \<and> g (word_of_nat n) = register_from_H reg \<and> n' = incn \<and> word_of_nat n < bnd \<and> word_of_nat n < bnd2; ret__unsigned_long = args ! incn\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'9 rv ret__unsigned_long) Guard ArrayBounds \<lbrace>\<acute>i < bnd\<rbrace> (\<acute>unsigned_long_eret_2 :== CALL sanitiseRegister_'proc(g \<acute>i,ret__unsigned_long,from_bool t)) ({s. w_'_update (\<lambda>_. unsigned_long_eret_2_' s) (reg_'_update (\<lambda>_. g (i_' s)) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr dst) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr dst\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace> \<inter> \<lbrace>\<acute>w = local.sanitiseRegister tcb reg (args ! incn)\<rbrace>} \<inter> \<lbrace>\<acute>i < bnd2\<rbrace>)
 2. \<And>rv ret__unsigned_long s. \<lbrakk>unat (f (word_of_nat n)) = incn \<and> g (word_of_nat n) = register_from_H reg \<and> n' = incn \<and> word_of_nat n < bnd \<and> word_of_nat n < bnd2; ret__unsigned_long = args ! incn; True\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'9 rv ret__unsigned_long \<inter> {s'. (s, s') \<in> rf_sr}) Guard ArrayBounds \<lbrace>\<acute>i < bnd\<rbrace> (\<acute>unsigned_long_eret_2 :== CALL sanitiseRegister_'proc(g \<acute>i,ret__unsigned_long,from_bool t)) {s'. (s, s') \<in> rf_sr}
 3. unat (f (word_of_nat n)) = incn \<and> g (word_of_nat n) = register_from_H reg \<and> n' = incn \<and> word_of_nat n < bnd \<and> word_of_nat n < bnd2 \<Longrightarrow> \<lbrace>?R9\<rbrace> return () \<lbrace>\<lambda>rv _. True\<rbrace>
 4. unat (f (word_of_nat n)) = incn \<and> g (word_of_nat n) = register_from_H reg \<and> n' = incn \<and> word_of_nat n < bnd \<and> word_of_nat n < bnd2 \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'9 \<acute>ret__unsigned_long :== CALL getSyscallArg_'proc(f \<acute>i,option_to_ptr buffer) {s. \<forall>rv. ret__unsigned_long_' s = args ! incn \<longrightarrow> s \<in> ?Q'9 rv (ret__unsigned_long_' s)}
 5. \<And>s s'. \<lbrakk>unat (f (word_of_nat n)) = incn \<and> g (word_of_nat n) = register_from_H reg \<and> n' = incn \<and> word_of_nat n < bnd \<and> word_of_nat n < bnd2; (s, s') \<in> rf_sr; (sysargs_rel args buffer and sysargs_rel_n args buffer n' and tcb_at' dst and P) s; s' \<in> \<lbrace>\<acute>i = word_of_nat n\<rbrace>\<rbrakk> \<Longrightarrow> (sysargs_rel args buffer and sysargs_rel_n args buffer incn and ?R9) s \<and> s' \<in> {s. ipc_buffer_'_update (\<lambda>_. option_to_ptr buffer) (i_'_update (\<lambda>_. f (i_' s)) s) \<in> UNIV \<inter> \<lbrace>unat \<acute>i = incn\<rbrace> \<inter> \<lbrace>\<acute>ipc_buffer = option_to_ptr buffer\<rbrace>} \<inter> ?R'9 proof (prove)
goal (4 subgoals):
 1. \<And>rv ret__unsigned_long s. \<lbrakk>unat (f (word_of_nat n)) = incn \<and> g (word_of_nat n) = register_from_H reg \<and> n' = incn \<and> word_of_nat n < bnd \<and> word_of_nat n < bnd2; ret__unsigned_long = args ! incn; True\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (\<lbrace>\<acute>i < bnd \<and> (\<exists>t r. g \<acute>i = register_from_H r \<and> (\<forall>ta. \<^bsup>ta\<^esup>ret__unsigned_long = local.sanitiseRegister t r ret__unsigned_long \<longrightarrow> g \<acute>i = register_from_H reg \<and> local.sanitiseRegister t r ret__unsigned_long = local.sanitiseRegister tcb reg (args ! incn) \<and> \<acute>i < bnd2))\<rbrace> \<inter> {s'. (s, s') \<in> rf_sr}) Guard ArrayBounds \<lbrace>\<acute>i < bnd\<rbrace> (\<acute>unsigned_long_eret_2 :== CALL sanitiseRegister_'proc(g \<acute>i,ret__unsigned_long,from_bool t)) {s'. (s, s') \<in> rf_sr}
 2. unat (f (word_of_nat n)) = incn \<and> g (word_of_nat n) = register_from_H reg \<and> n' = incn \<and> word_of_nat n < bnd \<and> word_of_nat n < bnd2 \<Longrightarrow> \<lbrace>?R9\<rbrace> return () \<lbrace>\<lambda>rv _. True\<rbrace>
 3. unat (f (word_of_nat n)) = incn \<and> g (word_of_nat n) = register_from_H reg \<and> n' = incn \<and> word_of_nat n < bnd \<and> word_of_nat n < bnd2 \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'9 \<acute>ret__unsigned_long :== CALL getSyscallArg_'proc(f \<acute>i,option_to_ptr buffer) {s. \<forall>rv. ret__unsigned_long_' s = args ! incn \<longrightarrow> s \<in> \<lbrace>\<acute>i < bnd \<and> (\<exists>t r. g \<acute>i = register_from_H r \<and> (\<forall>ta. \<^bsup>ta\<^esup>ret__unsigned_long = local.sanitiseRegister t r \<^bsup>s\<^esup>ret__unsigned_long \<longrightarrow> g \<acute>i = register_from_H reg \<and> local.sanitiseRegister t r \<^bsup>s\<^esup>ret__unsigned_long = local.sanitiseRegister tcb reg (args ! incn) \<and> \<acute>i < bnd2))\<rbrace>}
 4. \<And>s s'. \<lbrakk>unat (f (word_of_nat n)) = incn \<and> g (word_of_nat n) = register_from_H reg \<and> n' = incn \<and> word_of_nat n < bnd \<and> word_of_nat n < bnd2; (s, s') \<in> rf_sr; (sysargs_rel args buffer and sysargs_rel_n args buffer n' and tcb_at' dst and P) s; s' \<in> \<lbrace>\<acute>i = word_of_nat n\<rbrace>\<rbrakk> \<Longrightarrow> (sysargs_rel args buffer and sysargs_rel_n args buffer incn and ?R9) s \<and> s' \<in> {s. ipc_buffer_'_update (\<lambda>_. option_to_ptr buffer) (i_'_update (\<lambda>_. f (i_' s)) s) \<in> UNIV \<inter> \<lbrace>unat \<acute>i = incn\<rbrace> \<inter> \<lbrace>\<acute>ipc_buffer = option_to_ptr buffer\<rbrace>} \<inter> ?R'9 proof (prove)
goal (3 subgoals):
 1. unat (f (word_of_nat n)) = incn \<and> g (word_of_nat n) = register_from_H reg \<and> n' = incn \<and> word_of_nat n < bnd \<and> word_of_nat n < bnd2 \<Longrightarrow> \<lbrace>?R9\<rbrace> return () \<lbrace>\<lambda>rv _. True\<rbrace>
 2. unat (f (word_of_nat n)) = incn \<and> g (word_of_nat n) = register_from_H reg \<and> n' = incn \<and> word_of_nat n < bnd \<and> word_of_nat n < bnd2 \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'9 \<acute>ret__unsigned_long :== CALL getSyscallArg_'proc(f \<acute>i,option_to_ptr buffer) {s. \<forall>rv. ret__unsigned_long_' s = args ! incn \<longrightarrow> s \<in> \<lbrace>\<acute>i < bnd \<and> (\<exists>t r. g \<acute>i = register_from_H r \<and> (\<forall>ta. \<^bsup>ta\<^esup>ret__unsigned_long = local.sanitiseRegister t r \<^bsup>s\<^esup>ret__unsigned_long \<longrightarrow> g \<acute>i = register_from_H reg \<and> local.sanitiseRegister t r \<^bsup>s\<^esup>ret__unsigned_long = local.sanitiseRegister tcb reg (args ! incn) \<and> \<acute>i < bnd2))\<rbrace>}
 3. \<And>s s'. \<lbrakk>unat (f (word_of_nat n)) = incn \<and> g (word_of_nat n) = register_from_H reg \<and> n' = incn \<and> word_of_nat n < bnd \<and> word_of_nat n < bnd2; (s, s') \<in> rf_sr; (sysargs_rel args buffer and sysargs_rel_n args buffer n' and tcb_at' dst and P) s; s' \<in> \<lbrace>\<acute>i = word_of_nat n\<rbrace>\<rbrakk> \<Longrightarrow> (sysargs_rel args buffer and sysargs_rel_n args buffer incn and ?R9) s \<and> s' \<in> {s. ipc_buffer_'_update (\<lambda>_. option_to_ptr buffer) (i_'_update (\<lambda>_. f (i_' s)) s) \<in> UNIV \<inter> \<lbrace>unat \<acute>i = incn\<rbrace> \<inter> \<lbrace>\<acute>ipc_buffer = option_to_ptr buffer\<rbrace>} \<inter> ?R'9 proof (prove)
goal (2 subgoals):
 1. unat (f (word_of_nat n)) = incn \<and> g (word_of_nat n) = register_from_H reg \<and> n' = incn \<and> word_of_nat n < bnd \<and> word_of_nat n < bnd2 \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'9 \<acute>ret__unsigned_long :== CALL getSyscallArg_'proc(f \<acute>i,option_to_ptr buffer) {s. \<forall>rv. ret__unsigned_long_' s = args ! incn \<longrightarrow> s \<in> \<lbrace>\<acute>i < bnd \<and> (\<exists>t r. g \<acute>i = register_from_H r \<and> (\<forall>ta. \<^bsup>ta\<^esup>ret__unsigned_long = local.sanitiseRegister t r \<^bsup>s\<^esup>ret__unsigned_long \<longrightarrow> g \<acute>i = register_from_H reg \<and> local.sanitiseRegister t r \<^bsup>s\<^esup>ret__unsigned_long = local.sanitiseRegister tcb reg (args ! incn) \<and> \<acute>i < bnd2))\<rbrace>}
 2. \<And>s s'. \<lbrakk>unat (f (word_of_nat n)) = incn \<and> g (word_of_nat n) = register_from_H reg \<and> n' = incn \<and> word_of_nat n < bnd \<and> word_of_nat n < bnd2; (s, s') \<in> rf_sr; (sysargs_rel args buffer and sysargs_rel_n args buffer n' and tcb_at' dst and P) s; s' \<in> \<lbrace>\<acute>i = word_of_nat n\<rbrace>\<rbrakk> \<Longrightarrow> (sysargs_rel args buffer and sysargs_rel_n args buffer incn and (\<lambda>a. True)) s \<and> s' \<in> {s. ipc_buffer_'_update (\<lambda>_. option_to_ptr buffer) (i_'_update (\<lambda>_. f (i_' s)) s) \<in> UNIV \<inter> \<lbrace>unat \<acute>i = incn\<rbrace> \<inter> \<lbrace>\<acute>ipc_buffer = option_to_ptr buffer\<rbrace>} \<inter> ?R'9 proof (prove)
goal (2 subgoals):
 1. unat (f (word_of_nat n)) = incn \<and> g (word_of_nat n) = register_from_H reg \<and> n' = incn \<and> word_of_nat n < bnd \<and> word_of_nat n < bnd2 \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'9 \<acute>ret__unsigned_long :== CALL getSyscallArg_'proc(f \<acute>i,option_to_ptr buffer) \<lbrace>\<acute>ret__unsigned_long = args ! incn \<longrightarrow> \<acute>i < bnd \<and> (\<exists>t r. g \<acute>i = register_from_H r \<and> ((\<exists>ta. \<^bsup>ta\<^esup>ret__unsigned_long = local.sanitiseRegister t r (args ! incn)) \<longrightarrow> g \<acute>i = register_from_H reg \<and> local.sanitiseRegister t r (args ! incn) = local.sanitiseRegister tcb reg (args ! incn) \<and> \<acute>i < bnd2))\<rbrace>
 2. \<And>s s'. \<lbrakk>unat (f (word_of_nat n)) = incn \<and> g (word_of_nat n) = register_from_H reg \<and> n' = incn \<and> word_of_nat n < bnd \<and> word_of_nat n < bnd2; (s, s') \<in> rf_sr; (sysargs_rel args buffer and sysargs_rel_n args buffer n' and tcb_at' dst and P) s; s' \<in> \<lbrace>\<acute>i = word_of_nat n\<rbrace>\<rbrakk> \<Longrightarrow> (sysargs_rel args buffer and sysargs_rel_n args buffer incn and (\<lambda>a. True)) s \<and> s' \<in> {s. ipc_buffer_'_update (\<lambda>_. option_to_ptr buffer) (i_'_update (\<lambda>_. f (i_' s)) s) \<in> UNIV \<inter> \<lbrace>unat \<acute>i = incn\<rbrace> \<inter> \<lbrace>\<acute>ipc_buffer = option_to_ptr buffer\<rbrace>} \<inter> ?R'9 proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>unat (f (word_of_nat n)) = incn \<and> g (word_of_nat n) = register_from_H reg \<and> n' = incn \<and> word_of_nat n < bnd \<and> word_of_nat n < bnd2; (s, s') \<in> rf_sr; (sysargs_rel args buffer and sysargs_rel_n args buffer n' and tcb_at' dst and P) s; s' \<in> \<lbrace>\<acute>i = word_of_nat n\<rbrace>\<rbrakk> \<Longrightarrow> (sysargs_rel args buffer and sysargs_rel_n args buffer incn and (\<lambda>a. True)) s \<and> s' \<in> {s. ipc_buffer_'_update (\<lambda>_. option_to_ptr buffer) (i_'_update (\<lambda>_. f (i_' s)) s) \<in> UNIV \<inter> \<lbrace>unat \<acute>i = incn\<rbrace> \<inter> \<lbrace>\<acute>ipc_buffer = option_to_ptr buffer\<rbrace>} \<inter> \<lbrace>\<forall>t. \<^bsup>t\<^esup>ret__unsigned_long = args ! incn \<longrightarrow> \<acute>i < bnd \<and> (\<exists>t r. g \<acute>i = register_from_H r \<and> g \<acute>i = register_from_H reg \<and> local.sanitiseRegister t r (args ! incn) = local.sanitiseRegister tcb reg (args ! incn) \<and> \<acute>i < bnd2)\<rbrace> proof (prove)
goal:
No subgoals!