theory StoreWord_C

lemma storeWord_ccorres':
  "ccorres dc xfdc
     (pspace_aligned' and pspace_distinct' and
               K (is_aligned ptr 2) and (\<lambda>s. pointerInUserData ptr s \<or> pointerInDeviceData ptr s))
     (UNIV \<inter> {s. ptr' s = Ptr ptr} \<inter> {s. c_guard (ptr' s)} \<inter> {s. val' s = val}) hs
     (doMachineOp $ storeWord ptr val)
     (Basic (\<lambda>s. globals_update (t_hrs_'_update
           (hrs_mem_update (heap_update (ptr' s) (val' s)))) s))" apply (clarsimp simp: storeWordUser_def) apply (rule ccorres_from_vcg_nofail) apply (rule allI) apply (rule conseqPre, vcg) apply (clarsimp split: if_split_asm) apply (rule bexI[rotated]) apply (subst in_doMachineOp) apply (fastforce simp: storeWord_def in_monad is_aligned_mask) apply simp apply (fold fun_upd_def)+ apply (fastforce elim: storeWord_rf_sr_upd) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (pspace_aligned' and pspace_distinct' and K (is_aligned ptr 2) and (\<lambda>s. pointerInUserData ptr s \<or> pointerInDeviceData ptr s)) (UNIV \<inter> {s. ptr' s = PTR(32 word) ptr} \<inter> {s. c_guard (ptr' s)} \<inter> {s. val' s = val}) hs (doMachineOp $ storeWord ptr val) (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update \<acute>ptr' \<acute>val'))) proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (pspace_aligned' and pspace_distinct' and (\<lambda>y. is_aligned ptr 2) and (\<lambda>s. pointerInUserData ptr s \<or> pointerInDeviceData ptr s)) ({s. ptr' s = PTR(32 word) ptr} \<inter> {s. c_guard (ptr' s)} \<inter> {s. val' s = val}) hs (doMachineOp (storeWord ptr val)) (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update \<acute>ptr' \<acute>val'))) proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. (pspace_aligned' and pspace_distinct' and (\<lambda>y. is_aligned ptr 2) and (\<lambda>s. pointerInUserData ptr s \<or> pointerInDeviceData ptr s)) \<sigma> \<and> s \<in> {s. ptr' s = PTR(32 word) ptr} \<inter> {s. c_guard (ptr' s)} \<inter> {s. val' s = val} \<and> (\<sigma>, s) \<in> rf_sr} \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update \<acute>ptr' \<acute>val')) {s. \<not> snd (doMachineOp (storeWord ptr val) \<sigma>) \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (doMachineOp (storeWord ptr val) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s))} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. \<Gamma>\<turnstile> {s. (pspace_aligned' and pspace_distinct' and (\<lambda>y. is_aligned ptr 2) and (\<lambda>s. pointerInUserData ptr s \<or> pointerInDeviceData ptr s)) \<sigma> \<and> s \<in> {s. ptr' s = PTR(32 word) ptr} \<inter> {s. c_guard (ptr' s)} \<inter> {s. val' s = val} \<and> (\<sigma>, s) \<in> rf_sr} \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update \<acute>ptr' \<acute>val')) {s. \<not> snd (doMachineOp (storeWord ptr val) \<sigma>) \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (doMachineOp (storeWord ptr val) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s))} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. {s. (pspace_aligned' and pspace_distinct' and (\<lambda>y. is_aligned ptr 2) and (\<lambda>s. pointerInUserData ptr s \<or> pointerInDeviceData ptr s)) \<sigma> \<and> s \<in> {s. ptr' s = PTR(32 word) ptr} \<inter> {s. c_guard (ptr' s)} \<inter> {s. val' s = val} \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<not> snd (doMachineOp (storeWord ptr val) \<sigma>) \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (doMachineOp (storeWord ptr val) \<sigma>). (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update (ptr' s) (val' s)))) s) \<in> rf_sr \<and> dc rv (xfdc (globals_update (t_hrs_'_update (hrs_mem_update (heap_update (ptr' s) (val' s)))) s)))} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; is_aligned ptr 2; pointerInUserData ptr \<sigma> \<or> pointerInDeviceData ptr \<sigma>; ptr' x = PTR(32 word) ptr; c_guard (PTR(32 word) ptr); (\<sigma>, x) \<in> rf_sr; val = val' x; \<not> snd (doMachineOp (storeWord ptr (val' x)) \<sigma>)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (doMachineOp (storeWord ptr (val' x)) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) ptr) (val' x)))) x) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; is_aligned ptr 2; pointerInUserData ptr \<sigma> \<or> pointerInDeviceData ptr \<sigma>; ptr' x = PTR(32 word) ptr; c_guard (PTR(32 word) ptr); (\<sigma>, x) \<in> rf_sr; val = val' x; \<not> snd (doMachineOp (storeWord ptr (val' x)) \<sigma>)\<rbrakk> \<Longrightarrow> ?x31 \<sigma> x \<in> fst (doMachineOp (storeWord ptr (val' x)) \<sigma>)
 2. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; is_aligned ptr 2; pointerInUserData ptr \<sigma> \<or> pointerInDeviceData ptr \<sigma>; ptr' x = PTR(32 word) ptr; c_guard (PTR(32 word) ptr); (\<sigma>, x) \<in> rf_sr; val = val' x; \<not> snd (doMachineOp (storeWord ptr (val' x)) \<sigma>)\<rbrakk> \<Longrightarrow> case ?x31 \<sigma> x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) ptr) (val' x)))) x) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; is_aligned ptr 2; pointerInUserData ptr \<sigma> \<or> pointerInDeviceData ptr \<sigma>; ptr' x = PTR(32 word) ptr; c_guard (PTR(32 word) ptr); (\<sigma>, x) \<in> rf_sr; val = val' x; \<not> snd (doMachineOp (storeWord ptr (val' x)) \<sigma>)\<rbrakk> \<Longrightarrow> \<exists>b. (?a35 \<sigma> x \<sigma> x, b) \<in> fst (storeWord ptr (val' x) (ksMachineState \<sigma>)) \<and> ?s35 \<sigma> x \<sigma> x = \<sigma>\<lparr>ksMachineState := b\<rparr>
 2. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; is_aligned ptr 2; pointerInUserData ptr \<sigma> \<or> pointerInDeviceData ptr \<sigma>; ptr' x = PTR(32 word) ptr; c_guard (PTR(32 word) ptr); (\<sigma>, x) \<in> rf_sr; val = val' x; \<not> snd (doMachineOp (storeWord ptr (val' x)) \<sigma>)\<rbrakk> \<Longrightarrow> case (?a35 \<sigma> x \<sigma> x, ?s35 \<sigma> x \<sigma> x) of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) ptr) (val' x)))) x) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; is_aligned ptr 2; pointerInUserData ptr \<sigma> \<or> pointerInDeviceData ptr \<sigma>; ptr' x = PTR(32 word) ptr; c_guard (PTR(32 word) ptr); (\<sigma>, x) \<in> rf_sr; val = val' x; \<not> snd (doMachineOp (storeWord ptr (val' x)) \<sigma>)\<rbrakk> \<Longrightarrow> case (?a35 \<sigma> x \<sigma> x, \<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit (val' x) ! 3, ptr + 1 := word_rsplit (val' x) ! 2, ptr + 2 := word_rsplit (val' x) ! Suc 0, ptr + 3 := word_rsplit (val' x) ! 0)) (ksMachineState \<sigma>)\<rparr>) of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) ptr) (val' x)))) x) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; is_aligned ptr 2; pointerInUserData ptr \<sigma> \<or> pointerInDeviceData ptr \<sigma>; ptr' x = PTR(32 word) ptr; c_guard (PTR(32 word) ptr); (\<sigma>, x) \<in> rf_sr; val = val' x; \<not> snd (doMachineOp (storeWord ptr (val' x)) \<sigma>)\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m a. if a = ptr + 3 then word_rsplit (val' x) ! 0 else if a = ptr + 2 then word_rsplit (val' x) ! Suc 0 else if a = ptr + 1 then word_rsplit (val' x) ! 2 else if a = ptr then word_rsplit (val' x) ! 3 else m a) (ksMachineState \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) ptr) (val' x)))) x) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x. \<lbrakk>pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; is_aligned ptr 2; pointerInUserData ptr \<sigma> \<or> pointerInDeviceData ptr \<sigma>; ptr' x = PTR(32 word) ptr; c_guard (PTR(32 word) ptr); (\<sigma>, x) \<in> rf_sr; val = val' x; \<not> snd (doMachineOp (storeWord ptr (val' x)) \<sigma>)\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit (val' x) ! 3, ptr + 1 := word_rsplit (val' x) ! 2, ptr + 2 := word_rsplit (val' x) ! Suc 0, ptr + 3 := word_rsplit (val' x) ! 0)) (ksMachineState \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) ptr) (val' x)))) x) \<in> rf_sr proof (prove)
goal:
No subgoals!