theory StoreWord_C

lemma user_data_relation_upd:
  assumes al: "is_aligned ptr 2"
  shows "cuser_user_data_relation
            (byte_to_word_heap
              (underlying_memory (ksMachineState \<sigma>)) (ptr && ~~ mask pageBits))
            (the (cslift s (Ptr (ptr && ~~ mask pageBits)))) \<Longrightarrow>
     cuser_user_data_relation
            (byte_to_word_heap
              ((underlying_memory (ksMachineState \<sigma>))
               (ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2,
                ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))
              (ptr && ~~ mask pageBits))
            (user_data_C.words_C_update
              (\<lambda>ws. Arrays.update ws (unat (ucast ((ptr && mask pageBits) >> 2):: 10 word)) w)
              (the (cslift s (Ptr (ptr && ~~ mask pageBits)))))" unfolding cuser_user_data_relation_def apply - apply (erule allEI) apply (case_tac "off = ucast ((ptr && mask pageBits) >> 2)") apply (clarsimp simp: mask_pageBits_inner_beauty [OF al] byte_to_word_heap_def) apply (subst index_update) apply (simp, unat_arith, simp) apply (subgoal_tac "map ((!) (word_rsplit w)) [0,1,2,3]
                      = (word_rsplit w :: word8 list)") apply (clarsimp simp: word_rcat_rsplit) apply (cut_tac w=w and m=4 and 'a=8
               in length_word_rsplit_even_size [OF refl]) apply (simp add: word_size) apply (rule nth_equalityI[symmetric]) apply simp apply (subgoal_tac "[0,1,2,3] = [0..<4]") apply clarsimp apply (rule nth_equalityI[symmetric]) apply simp apply (auto dest: nat_less_4_cases)[1] apply (frule more_pageBits_inner_beauty) apply (simp add: byte_to_word_heap_upd_neq aligned_already_mask al
                   byte_to_word_heap_upd_neq [where n=0, simplified]) apply (subst index_update2) apply (cut_tac x=off in unat_lt2p, simp) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) (ptr && ~~ mask pageBits)) (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))) \<Longrightarrow> cuser_user_data_relation (byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ptr && ~~ mask pageBits)) (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits))))) proof (prove)
goal (1 subgoal):
 1. \<forall>off. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat off] \<Longrightarrow> \<forall>off. byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits))))).[unat off] proof (prove)
goal (1 subgoal):
 1. \<forall>off. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat off] \<Longrightarrow> \<forall>off. byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits))))).[unat off] proof (prove)
goal (1 subgoal):
 1. \<And>off. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat off] \<Longrightarrow> byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits))))).[unat off] proof (prove)
goal (2 subgoals):
 1. \<And>off. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat off]; off = UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2)\<rbrakk> \<Longrightarrow> byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits))))).[unat off]
 2. \<And>off. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat off]; off \<noteq> UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2)\<rbrakk> \<Longrightarrow> byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits))))).[unat off] proof (prove)
goal (2 subgoals):
 1. word_rcat [underlying_memory (ksMachineState \<sigma>) (ptr + 3), underlying_memory (ksMachineState \<sigma>) (ptr + 2), underlying_memory (ksMachineState \<sigma>) (ptr + 1), underlying_memory (ksMachineState \<sigma>) ptr] = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))] \<Longrightarrow> word_rcat [word_rsplit w ! 0, word_rsplit w ! Suc 0, word_rsplit w ! 2, word_rsplit w ! 3] = Arrays.update (user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits))))) (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w.[unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))]
 2. \<And>off. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat off]; off \<noteq> UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2)\<rbrakk> \<Longrightarrow> byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits))))).[unat off] proof (prove)
goal (3 subgoals):
 1. word_rcat [underlying_memory (ksMachineState \<sigma>) (ptr + 3), underlying_memory (ksMachineState \<sigma>) (ptr + 2), underlying_memory (ksMachineState \<sigma>) (ptr + 1), underlying_memory (ksMachineState \<sigma>) ptr] = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))] \<Longrightarrow> unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2)) < CARD(1024)
 2. word_rcat [underlying_memory (ksMachineState \<sigma>) (ptr + 3), underlying_memory (ksMachineState \<sigma>) (ptr + 2), underlying_memory (ksMachineState \<sigma>) (ptr + 1), underlying_memory (ksMachineState \<sigma>) ptr] = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))] \<Longrightarrow> word_rcat [word_rsplit w ! 0, word_rsplit w ! Suc 0, word_rsplit w ! 2, word_rsplit w ! 3] = w
 3. \<And>off. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat off]; off \<noteq> UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2)\<rbrakk> \<Longrightarrow> byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits))))).[unat off] proof (prove)
goal (2 subgoals):
 1. word_rcat [underlying_memory (ksMachineState \<sigma>) (ptr + 3), underlying_memory (ksMachineState \<sigma>) (ptr + 2), underlying_memory (ksMachineState \<sigma>) (ptr + 1), underlying_memory (ksMachineState \<sigma>) ptr] = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))] \<Longrightarrow> word_rcat [word_rsplit w ! 0, word_rsplit w ! Suc 0, word_rsplit w ! 2, word_rsplit w ! 3] = w
 2. \<And>off. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat off]; off \<noteq> UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2)\<rbrakk> \<Longrightarrow> byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits))))).[unat off] proof (prove)
goal (3 subgoals):
 1. \<lbrakk>word_rcat [underlying_memory (ksMachineState \<sigma>) (ptr + 3), underlying_memory (ksMachineState \<sigma>) (ptr + 2), underlying_memory (ksMachineState \<sigma>) (ptr + 1), underlying_memory (ksMachineState \<sigma>) ptr] = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))]; map ((!) (word_rsplit w)) [0, 1, 2, 3] = word_rsplit w\<rbrakk> \<Longrightarrow> word_rcat [word_rsplit w ! 0, word_rsplit w ! Suc 0, word_rsplit w ! 2, word_rsplit w ! 3] = w
 2. word_rcat [underlying_memory (ksMachineState \<sigma>) (ptr + 3), underlying_memory (ksMachineState \<sigma>) (ptr + 2), underlying_memory (ksMachineState \<sigma>) (ptr + 1), underlying_memory (ksMachineState \<sigma>) ptr] = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))] \<Longrightarrow> map ((!) (word_rsplit w)) [0, 1, 2, 3] = word_rsplit w
 3. \<And>off. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat off]; off \<noteq> UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2)\<rbrakk> \<Longrightarrow> byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits))))).[unat off] proof (prove)
goal (2 subgoals):
 1. word_rcat [underlying_memory (ksMachineState \<sigma>) (ptr + 3), underlying_memory (ksMachineState \<sigma>) (ptr + 2), underlying_memory (ksMachineState \<sigma>) (ptr + 1), underlying_memory (ksMachineState \<sigma>) ptr] = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))] \<Longrightarrow> map ((!) (word_rsplit w)) [0, 1, 2, 3] = word_rsplit w
 2. \<And>off. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat off]; off \<noteq> UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2)\<rbrakk> \<Longrightarrow> byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits))))).[unat off] proof (prove)
goal (3 subgoals):
 1. word_rcat [underlying_memory (ksMachineState \<sigma>) (ptr + 3), underlying_memory (ksMachineState \<sigma>) (ptr + 2), underlying_memory (ksMachineState \<sigma>) (ptr + 1), underlying_memory (ksMachineState \<sigma>) ptr] = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))] \<Longrightarrow> size w = 4 * LENGTH(8)
 2. \<lbrakk>word_rcat [underlying_memory (ksMachineState \<sigma>) (ptr + 3), underlying_memory (ksMachineState \<sigma>) (ptr + 2), underlying_memory (ksMachineState \<sigma>) (ptr + 1), underlying_memory (ksMachineState \<sigma>) ptr] = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))]; length (word_rsplit w) = 4\<rbrakk> \<Longrightarrow> map ((!) (word_rsplit w)) [0, 1, 2, 3] = word_rsplit w
 3. \<And>off. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat off]; off \<noteq> UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2)\<rbrakk> \<Longrightarrow> byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits))))).[unat off] proof (prove)
goal (2 subgoals):
 1. \<lbrakk>word_rcat [underlying_memory (ksMachineState \<sigma>) (ptr + 3), underlying_memory (ksMachineState \<sigma>) (ptr + 2), underlying_memory (ksMachineState \<sigma>) (ptr + 1), underlying_memory (ksMachineState \<sigma>) ptr] = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))]; length (word_rsplit w) = 4\<rbrakk> \<Longrightarrow> map ((!) (word_rsplit w)) [0, 1, 2, 3] = word_rsplit w
 2. \<And>off. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat off]; off \<noteq> UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2)\<rbrakk> \<Longrightarrow> byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits))))).[unat off] proof (prove)
goal (3 subgoals):
 1. \<lbrakk>word_rcat [underlying_memory (ksMachineState \<sigma>) (ptr + 3), underlying_memory (ksMachineState \<sigma>) (ptr + 2), underlying_memory (ksMachineState \<sigma>) (ptr + 1), underlying_memory (ksMachineState \<sigma>) ptr] = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))]; length (word_rsplit w) = 4\<rbrakk> \<Longrightarrow> length (word_rsplit w) = length (map ((!) (word_rsplit w)) [0, 1, 2, 3])
 2. \<And>i. \<lbrakk>word_rcat [underlying_memory (ksMachineState \<sigma>) (ptr + 3), underlying_memory (ksMachineState \<sigma>) (ptr + 2), underlying_memory (ksMachineState \<sigma>) (ptr + 1), underlying_memory (ksMachineState \<sigma>) ptr] = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))]; length (word_rsplit w) = 4; i < length (word_rsplit w)\<rbrakk> \<Longrightarrow> word_rsplit w ! i = map ((!) (word_rsplit w)) [0, 1, 2, 3] ! i
 3. \<And>off. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat off]; off \<noteq> UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2)\<rbrakk> \<Longrightarrow> byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits))))).[unat off] proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>word_rcat [underlying_memory (ksMachineState \<sigma>) (ptr + 3), underlying_memory (ksMachineState \<sigma>) (ptr + 2), underlying_memory (ksMachineState \<sigma>) (ptr + 1), underlying_memory (ksMachineState \<sigma>) ptr] = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))]; length (word_rsplit w) = 4; i < length (word_rsplit w)\<rbrakk> \<Longrightarrow> word_rsplit w ! i = map ((!) (word_rsplit w)) [0, 1, 2, 3] ! i
 2. \<And>off. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat off]; off \<noteq> UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2)\<rbrakk> \<Longrightarrow> byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits))))).[unat off] proof (prove)
goal (3 subgoals):
 1. \<And>i. \<lbrakk>word_rcat [underlying_memory (ksMachineState \<sigma>) (ptr + 3), underlying_memory (ksMachineState \<sigma>) (ptr + 2), underlying_memory (ksMachineState \<sigma>) (ptr + 1), underlying_memory (ksMachineState \<sigma>) ptr] = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))]; length (word_rsplit w) = 4; i < length (word_rsplit w); [0, 1, 2, 3] = [0..<4]\<rbrakk> \<Longrightarrow> word_rsplit w ! i = map ((!) (word_rsplit w)) [0, 1, 2, 3] ! i
 2. \<And>i. \<lbrakk>word_rcat [underlying_memory (ksMachineState \<sigma>) (ptr + 3), underlying_memory (ksMachineState \<sigma>) (ptr + 2), underlying_memory (ksMachineState \<sigma>) (ptr + 1), underlying_memory (ksMachineState \<sigma>) ptr] = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))]; length (word_rsplit w) = 4; i < length (word_rsplit w)\<rbrakk> \<Longrightarrow> [0, 1, 2, 3] = [0..<4]
 3. \<And>off. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat off]; off \<noteq> UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2)\<rbrakk> \<Longrightarrow> byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits))))).[unat off] proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>word_rcat [underlying_memory (ksMachineState \<sigma>) (ptr + 3), underlying_memory (ksMachineState \<sigma>) (ptr + 2), underlying_memory (ksMachineState \<sigma>) (ptr + 1), underlying_memory (ksMachineState \<sigma>) ptr] = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))]; length (word_rsplit w) = 4; i < length (word_rsplit w)\<rbrakk> \<Longrightarrow> [0, 1, 2, 3] = [0..<4]
 2. \<And>off. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat off]; off \<noteq> UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2)\<rbrakk> \<Longrightarrow> byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits))))).[unat off] proof (prove)
goal (3 subgoals):
 1. \<And>i. \<lbrakk>word_rcat [underlying_memory (ksMachineState \<sigma>) (ptr + 3), underlying_memory (ksMachineState \<sigma>) (ptr + 2), underlying_memory (ksMachineState \<sigma>) (ptr + 1), underlying_memory (ksMachineState \<sigma>) ptr] = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))]; length (word_rsplit w) = 4; i < length (word_rsplit w)\<rbrakk> \<Longrightarrow> length [0..<4] = length [0, 1, 2, 3]
 2. \<And>i ia. \<lbrakk>word_rcat [underlying_memory (ksMachineState \<sigma>) (ptr + 3), underlying_memory (ksMachineState \<sigma>) (ptr + 2), underlying_memory (ksMachineState \<sigma>) (ptr + 1), underlying_memory (ksMachineState \<sigma>) ptr] = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))]; length (word_rsplit w) = 4; i < length (word_rsplit w); ia < length [0..<4]\<rbrakk> \<Longrightarrow> [0..<4] ! ia = [0, 1, 2, 3] ! ia
 3. \<And>off. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat off]; off \<noteq> UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2)\<rbrakk> \<Longrightarrow> byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits))))).[unat off] proof (prove)
goal (2 subgoals):
 1. \<And>i ia. \<lbrakk>word_rcat [underlying_memory (ksMachineState \<sigma>) (ptr + 3), underlying_memory (ksMachineState \<sigma>) (ptr + 2), underlying_memory (ksMachineState \<sigma>) (ptr + 1), underlying_memory (ksMachineState \<sigma>) ptr] = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))]; length (word_rsplit w) = 4; i < length (word_rsplit w); ia < length [0..<4]\<rbrakk> \<Longrightarrow> [0..<4] ! ia = [0, 1, 2, 3] ! ia
 2. \<And>off. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat off]; off \<noteq> UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2)\<rbrakk> \<Longrightarrow> byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits))))).[unat off] proof (prove)
goal (1 subgoal):
 1. \<And>off. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat off]; off \<noteq> UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2)\<rbrakk> \<Longrightarrow> byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits))))).[unat off] proof (prove)
goal (1 subgoal):
 1. \<And>off. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat off]; off \<noteq> UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2); (ptr && ~~ mask pageBits) + UCAST(10 \<rightarrow> 32) off * 4 \<noteq> ptr\<rbrakk> \<Longrightarrow> byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (user_data_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits))))).[unat off] proof (prove)
goal (1 subgoal):
 1. \<And>off. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat off]; off \<noteq> UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2); (ptr && ~~ mask pageBits) + UCAST(10 \<rightarrow> 32) off * 4 \<noteq> ptr\<rbrakk> \<Longrightarrow> user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat off] = Arrays.update (user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits))))) (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w.[unat off] proof (prove)
goal (3 subgoals):
 1. \<And>off. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat off]; off \<noteq> UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2); (ptr && ~~ mask pageBits) + UCAST(10 \<rightarrow> 32) off * 4 \<noteq> ptr\<rbrakk> \<Longrightarrow> unat off < CARD(1024)
 2. \<And>off. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat off]; off \<noteq> UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2); (ptr && ~~ mask pageBits) + UCAST(10 \<rightarrow> 32) off * 4 \<noteq> ptr\<rbrakk> \<Longrightarrow> unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2)) \<noteq> unat off
 3. \<And>off. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat off]; off \<noteq> UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2); (ptr && ~~ mask pageBits) + UCAST(10 \<rightarrow> 32) off * 4 \<noteq> ptr\<rbrakk> \<Longrightarrow> user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat off] = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat off] proof (prove)
goal (2 subgoals):
 1. \<And>off. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat off]; off \<noteq> UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2); (ptr && ~~ mask pageBits) + UCAST(10 \<rightarrow> 32) off * 4 \<noteq> ptr\<rbrakk> \<Longrightarrow> unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2)) \<noteq> unat off
 2. \<And>off. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat off]; off \<noteq> UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2); (ptr && ~~ mask pageBits) + UCAST(10 \<rightarrow> 32) off * 4 \<noteq> ptr\<rbrakk> \<Longrightarrow> user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat off] = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat off] proof (prove)
goal (1 subgoal):
 1. \<And>off. \<lbrakk>byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) (ptr && ~~ mask pageBits) off = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat off]; off \<noteq> UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2); (ptr && ~~ mask pageBits) + UCAST(10 \<rightarrow> 32) off * 4 \<noteq> ptr\<rbrakk> \<Longrightarrow> user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat off] = user_data_C.words_C (the (cslift s (PTR(user_data_C) (ptr && ~~ mask pageBits)))).[unat off] proof (prove)
goal:
No subgoals!