theory ArchTcbAcc_AI

lemma storeWord_invs[wp, TcbAcc_AI_assms]:
  "\<lbrace>in_user_frame p and invs\<rbrace> do_machine_op (storeWord p w) \<lbrace>\<lambda>rv. invs\<rbrace>" proof - have aligned_offset_ignore:
    "\<And>l sz. l<4 \<Longrightarrow> p && mask 2 = 0 \<Longrightarrow>
       p+l && ~~ mask (pageBitsForSize sz) = p && ~~ mask (pageBitsForSize sz)" proof - fix l sz assume al: "p && mask 2 = 0" assume "(l::word32) < 4" hence less: "l<2^2" by simp have le: "2 \<le> pageBitsForSize sz" by (case_tac sz, simp_all) show "?thesis l sz" by (rule is_aligned_add_helper[simplified is_aligned_mask,
          THEN conjunct2, THEN mask_out_first_mask_some,
          where n=2, OF al less le]) qed show ?thesis apply (wp dmo_invs) apply (clarsimp simp: storeWord_def invs_def valid_state_def) apply (fastforce simp: valid_machine_state_def in_user_frame_def
               assert_def simpler_modify_def fail_def bind_def return_def
               pageBits_def aligned_offset_ignore
             split: if_split_asm) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>in_user_frame p and invs\<rbrace> do_machine_op (storeWord p w) \<lbrace>\<lambda>rv. invs\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>in_user_frame p and invs\<rbrace> do_machine_op (storeWord p w) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>l sz. \<lbrakk>l < 4; p && mask 2 = 0\<rbrakk> \<Longrightarrow> p + l && ~~ mask (pageBitsForSize sz) = p && ~~ mask (pageBitsForSize sz) proof (state)
goal (1 subgoal):
 1. \<And>l sz. \<lbrakk>l < 4; p && mask 2 = 0\<rbrakk> \<Longrightarrow> p + l && ~~ mask (pageBitsForSize sz) = p && ~~ mask (pageBitsForSize sz) proof (state)
goal (1 subgoal):
 1. \<And>l sz. \<lbrakk>l < 4; p && mask 2 = 0\<rbrakk> \<Longrightarrow> p + l && ~~ mask (pageBitsForSize sz) = p && ~~ mask (pageBitsForSize sz) proof (state)
this:
p && mask 2 = 0

goal (1 subgoal):
 1. \<And>l sz. \<lbrakk>l < 4; p && mask 2 = 0\<rbrakk> \<Longrightarrow> p + l && ~~ mask (pageBitsForSize sz) = p && ~~ mask (pageBitsForSize sz) proof (state)
this:
l < 4

goal (1 subgoal):
 1. \<And>l sz. \<lbrakk>l < 4; p && mask 2 = 0\<rbrakk> \<Longrightarrow> p + l && ~~ mask (pageBitsForSize sz) = p && ~~ mask (pageBitsForSize sz) proof (prove)
using this:
l < 4

goal (1 subgoal):
 1. l < 2\<^sup>2 proof (state)
this:
l < 2\<^sup>2

goal (1 subgoal):
 1. \<And>l sz. \<lbrakk>l < 4; p && mask 2 = 0\<rbrakk> \<Longrightarrow> p + l && ~~ mask (pageBitsForSize sz) = p && ~~ mask (pageBitsForSize sz) proof (prove)
goal (1 subgoal):
 1. 2 \<le> pageBitsForSize sz proof (state)
this:
2 \<le> pageBitsForSize sz

goal (1 subgoal):
 1. \<And>l sz. \<lbrakk>l < 4; p && mask 2 = 0\<rbrakk> \<Longrightarrow> p + l && ~~ mask (pageBitsForSize sz) = p && ~~ mask (pageBitsForSize sz) proof (prove)
goal (1 subgoal):
 1. p + l && ~~ mask (pageBitsForSize sz) = p && ~~ mask (pageBitsForSize sz) proof (state)
this:
p + l && ~~ mask (pageBitsForSize sz) = p && ~~ mask (pageBitsForSize sz)

goal:
No subgoals! proof (state)
this:
\<lbrakk>?l < 4; p && mask 2 = 0\<rbrakk> \<Longrightarrow> p + ?l && ~~ mask (pageBitsForSize ?sz) = p && ~~ mask (pageBitsForSize ?sz)

goal (1 subgoal):
 1. \<lbrace>in_user_frame p and invs\<rbrace> do_machine_op (storeWord p w) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>in_user_frame p and invs\<rbrace> do_machine_op (storeWord p w) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (in_user_frame p and invs) s \<Longrightarrow> \<forall>m. \<forall>(r, m')\<in>fst (storeWord p w m). (\<forall>p. in_user_frame p s \<or> underlying_memory m' p = underlying_memory m p) \<and> (\<forall>irq. m = machine_state s \<longrightarrow> (interrupt_states s irq = IRQInactive \<longrightarrow> irq_masks m' irq) \<or> irq_masks m' irq = irq_masks m irq) \<and> invs s proof (prove)
goal (1 subgoal):
 1. \<And>s m b. \<lbrakk>((), b) \<in> fst ((do y <- assert (p && mask 2 = 0);
modify (underlying_memory_update (\<lambda>m. m(p := word_rsplit w ! 3, p + 1 := word_rsplit w ! 2, p + 2 := word_rsplit w ! Suc 0, p + 3 := word_rsplit w ! 0)))
od) m); in_user_frame p s; valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s\<rbrakk> \<Longrightarrow> (\<forall>p. in_user_frame p s \<or> underlying_memory b p = underlying_memory m p) \<and> (m = machine_state s \<longrightarrow> (\<forall>irq. interrupt_states s irq = IRQInactive \<longrightarrow> irq_masks b irq \<or> irq_masks b irq = irq_masks (machine_state s) irq)) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>in_user_frame p and invs\<rbrace> do_machine_op (storeWord p w) \<lbrace>\<lambda>rv. invs\<rbrace>

goal:
No subgoals!