theory StoreWord_C

lemma storeWordUser_ccorres:
  "ccorres dc xfdc (valid_pspace' and (\<lambda>_. is_aligned ptr 2))
              (UNIV \<inter> {s. ptr' s = Ptr ptr} \<inter> {s. w' s = w}) hs
      (storeWordUser ptr w)
      (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>(\<lambda>s. ptr' s)\<rbrace>
          (Basic (\<lambda>s. globals_update (t_hrs_'_update
           (hrs_mem_update (heap_update (ptr' s) (w' s)))) s)))" apply (simp add: storeWordUser_def) apply (rule ccorres_symb_exec_l'[OF _ stateAssert_inv stateAssert_sp empty_fail_stateAssert]) apply (rule ccorres_guard_imp2) apply (rule ccorres_Guard) apply (rule storeWord_ccorres[unfolded fun_app_def]) apply (clarsimp simp: pointerInUserData_c_guard pointerInUserData_h_t_valid) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (valid_pspace' and (\<lambda>_. is_aligned ptr 2)) (UNIV \<inter> {s. ptr' s = PTR(32 word) ptr} \<inter> {s. w' s = w}) hs (storeWordUser ptr w) (Guard C_Guard {s. s \<Turnstile>\<^sub>c ptr' s} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update \<acute>ptr' \<acute>w')))) proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (valid_pspace' and (\<lambda>_. is_aligned ptr 2)) ({s. ptr' s = PTR(32 word) ptr} \<inter> {s. w' s = w}) hs (do y <- stateAssert (pointerInUserData ptr) [];
doMachineOp (storeWord ptr w)
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c ptr' s} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update \<acute>ptr' \<acute>w')))) proof (prove)
goal (1 subgoal):
 1. \<And>y. ccorres dc xfdc (valid_pspace' and (\<lambda>_. is_aligned ptr 2) and pointerInUserData ptr) ({s. ptr' s = PTR(32 word) ptr} \<inter> {s. w' s = w}) hs (doMachineOp (storeWord ptr w)) (Guard C_Guard {s. s \<Turnstile>\<^sub>c ptr' s} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update \<acute>ptr' \<acute>w')))) proof (prove)
goal (2 subgoals):
 1. \<And>y. ccorres dc xfdc (?Q12 y) (?Q'12 y) hs (doMachineOp (storeWord ptr w)) (Guard C_Guard {s. s \<Turnstile>\<^sub>c ptr' s} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update \<acute>ptr' \<acute>w'))))
 2. \<And>y s s'. \<lbrakk>(s, s') \<in> rf_sr; (valid_pspace' and (\<lambda>_. is_aligned ptr 2) and pointerInUserData ptr) s; s' \<in> {s. ptr' s = PTR(32 word) ptr} \<inter> {s. w' s = w}\<rbrakk> \<Longrightarrow> ?Q12 y s \<and> s' \<in> ?Q'12 y proof (prove)
goal (2 subgoals):
 1. \<And>y. ccorres dc xfdc (?Q12 y) (?C'15 y) hs (doMachineOp (storeWord ptr w)) (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update \<acute>ptr' \<acute>w')))
 2. \<And>y s s'. \<lbrakk>(s, s') \<in> rf_sr; (valid_pspace' and (\<lambda>_. is_aligned ptr 2) and pointerInUserData ptr) s; s' \<in> {s. ptr' s = PTR(32 word) ptr} \<inter> {s. w' s = w}\<rbrakk> \<Longrightarrow> ?Q12 y s \<and> s' \<in> ?C'15 y \<inter> {s. s \<Turnstile>\<^sub>c ptr' s} proof (prove)
goal (1 subgoal):
 1. \<And>y s s'. \<lbrakk>(s, s') \<in> rf_sr; (valid_pspace' and (\<lambda>_. is_aligned ptr 2) and pointerInUserData ptr) s; s' \<in> {s. ptr' s = PTR(32 word) ptr} \<inter> {s. w' s = w}\<rbrakk> \<Longrightarrow> (valid_pspace' and K (is_aligned ptr 2) and pointerInUserData ptr) s \<and> s' \<in> UNIV \<inter> {s. ptr' s = PTR(32 word) ptr} \<inter> {s. c_guard (ptr' s)} \<inter> {s. w' s = w} \<inter> {s. s \<Turnstile>\<^sub>c ptr' s} proof (prove)
goal:
No subgoals!