theory StoreWord_C

lemma storeWord_rf_sr_upd:
  "\<lbrakk> (\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>;  pspace_distinct' \<sigma>;
     pointerInUserData ptr \<sigma> \<or> pointerInDeviceData ptr \<sigma>; is_aligned ptr 2\<rbrakk> \<Longrightarrow>
   (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m.
           m(ptr := word_rsplit (w::word32) ! 3, ptr + 1 := word_rsplit w ! 2,
             ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))
                   (ksMachineState \<sigma>)\<rparr>,
    globals_update (t_hrs_'_update (hrs_mem_update
                    (heap_update (Ptr ptr) w))) s) \<in> rf_sr" apply (elim disjE) apply (cut_tac storeWordUser_rf_sr_upd' [rule_format, where s=s and \<sigma>=\<sigma>]) prefer 2 apply fastforce apply simp apply (erule iffD1 [OF rf_sr_upd, rotated -1], simp_all)[1] apply (cut_tac storeWordDevice_rf_sr_upd' [rule_format, where s=s and \<sigma>=\<sigma>]) prefer 2 apply fastforce apply simp apply (erule iffD1 [OF rf_sr_upd, rotated -1], simp_all)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma> \<or> pointerInDeviceData ptr \<sigma>; is_aligned ptr 2\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) ptr) w))) s) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; is_aligned ptr 2; pointerInUserData ptr \<sigma>\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) ptr) w))) s) \<in> rf_sr
 2. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; is_aligned ptr 2; pointerInDeviceData ptr \<sigma>\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) ptr) w))) s) \<in> rf_sr proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; is_aligned ptr 2; pointerInUserData ptr \<sigma>; (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(?ptr2 := word_rsplit ?w2 ! 3, ?ptr2 + 1 := word_rsplit ?w2 ! 2, ?ptr2 + 2 := word_rsplit ?w2 ! 1, ?ptr2 + 3 := word_rsplit ?w2 ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ?ptr2) ?w2) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) ptr) w))) s) \<in> rf_sr
 2. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; is_aligned ptr 2; pointerInUserData ptr \<sigma>\<rbrakk> \<Longrightarrow> (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ?ptr2 \<sigma> \<and> is_aligned ?ptr2 2
 3. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; is_aligned ptr 2; pointerInDeviceData ptr \<sigma>\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) ptr) w))) s) \<in> rf_sr proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; is_aligned ptr 2; pointerInUserData ptr \<sigma>\<rbrakk> \<Longrightarrow> (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInUserData ?ptr2 \<sigma> \<and> is_aligned ?ptr2 2
 2. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; is_aligned ptr 2; pointerInUserData ptr \<sigma>; (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(?ptr2 := word_rsplit ?w2 ! 3, ?ptr2 + 1 := word_rsplit ?w2 ! 2, ?ptr2 + 2 := word_rsplit ?w2 ! 1, ?ptr2 + 3 := word_rsplit ?w2 ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ?ptr2) ?w2) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) ptr) w))) s) \<in> rf_sr
 3. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; is_aligned ptr 2; pointerInDeviceData ptr \<sigma>\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) ptr) w))) s) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; is_aligned ptr 2; pointerInUserData ptr \<sigma>; (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit ?w2 ! 3, ptr + 1 := word_rsplit ?w2 ! 2, ptr + 2 := word_rsplit ?w2 ! 1, ptr + 3 := word_rsplit ?w2 ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) ?w2) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) ptr) w))) s) \<in> rf_sr
 2. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; is_aligned ptr 2; pointerInDeviceData ptr \<sigma>\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) ptr) w))) s) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; is_aligned ptr 2; pointerInUserData ptr \<sigma>; (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit ?w2 ! 3, ptr + 1 := word_rsplit ?w2 ! 2, ptr + 2 := word_rsplit ?w2 ! Suc 0, ptr + 3 := word_rsplit ?w2 ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) ?w2) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) ptr) w))) s) \<in> rf_sr
 2. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; is_aligned ptr 2; pointerInDeviceData ptr \<sigma>\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) ptr) w))) s) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; is_aligned ptr 2; pointerInDeviceData ptr \<sigma>\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) ptr) w))) s) \<in> rf_sr
flex-flex pairs:
?intStateIRQNode_'11 (globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>) \<equiv>\<^sup>? ?intStateIRQNode_'11 (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) ptr) w)) (globals s)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; is_aligned ptr 2; pointerInDeviceData ptr \<sigma>; (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(?ptr33 := word_rsplit ?w33 ! 3, ?ptr33 + 1 := word_rsplit ?w33 ! 2, ?ptr33 + 2 := word_rsplit ?w33 ! 1, ?ptr33 + 3 := word_rsplit ?w33 ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ?ptr33) ?w33) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) ptr) w))) s) \<in> rf_sr
 2. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; is_aligned ptr 2; pointerInDeviceData ptr \<sigma>\<rbrakk> \<Longrightarrow> (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInDeviceData ?ptr33 \<sigma> \<and> is_aligned ?ptr33 2
flex-flex pairs:
?intStateIRQNode_'11 (globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>) \<equiv>\<^sup>? ?intStateIRQNode_'11 (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) ptr) w)) (globals s)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; is_aligned ptr 2; pointerInDeviceData ptr \<sigma>\<rbrakk> \<Longrightarrow> (\<sigma>, s) \<in> rf_sr \<and> pspace_aligned' \<sigma> \<and> pspace_distinct' \<sigma> \<and> pointerInDeviceData ?ptr33 \<sigma> \<and> is_aligned ?ptr33 2
 2. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; is_aligned ptr 2; pointerInDeviceData ptr \<sigma>; (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(?ptr33 := word_rsplit ?w33 ! 3, ?ptr33 + 1 := word_rsplit ?w33 ! 2, ?ptr33 + 2 := word_rsplit ?w33 ! 1, ?ptr33 + 3 := word_rsplit ?w33 ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ?ptr33) ?w33) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) ptr) w))) s) \<in> rf_sr
flex-flex pairs:
?intStateIRQNode_'11 (globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>) \<equiv>\<^sup>? ?intStateIRQNode_'11 (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) ptr) w)) (globals s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; is_aligned ptr 2; pointerInDeviceData ptr \<sigma>; (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit ?w33 ! 3, ptr + 1 := word_rsplit ?w33 ! 2, ptr + 2 := word_rsplit ?w33 ! 1, ptr + 3 := word_rsplit ?w33 ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) ?w33) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) ptr) w))) s) \<in> rf_sr
flex-flex pairs:
?intStateIRQNode_'11 (globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>) \<equiv>\<^sup>? ?intStateIRQNode_'11 (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) ptr) w)) (globals s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; is_aligned ptr 2; pointerInDeviceData ptr \<sigma>; (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit ?w33 ! 3, ptr + 1 := word_rsplit ?w33 ! 2, ptr + 2 := word_rsplit ?w33 ! Suc 0, ptr + 3 := word_rsplit ?w33 ! 0)) (ksMachineState \<sigma>)\<rparr>, s\<lparr>globals := globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) ?w33) (t_hrs_' (globals s))\<rparr>\<rparr>) \<in> rf_sr\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ksMachineState \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) ptr) w))) s) \<in> rf_sr
flex-flex pairs:
?intStateIRQNode_'11 (globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>) \<equiv>\<^sup>? ?intStateIRQNode_'11 (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) ptr) w)) (globals s)) proof (prove)
goal:
No subgoals!
flex-flex pairs:
?intStateIRQNode_'42 (globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>) \<equiv>\<^sup>? ?intStateIRQNode_'42 (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) ptr) w)) (globals s))
?intStateIRQNode_'11 (globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (PTR(32 word) ptr) w) (t_hrs_' (globals s))\<rparr>) \<equiv>\<^sup>? ?intStateIRQNode_'11 (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) ptr) w)) (globals s))