theory TcbAcc_R

lemma storeWord_invs'[wp]:
  "\<lbrace>pointerInUserData p and invs'\<rbrace> doMachineOp (storeWord p w) \<lbrace>\<lambda>rv. invs'\<rbrace>" proof - have aligned_offset_ignore:
    "\<And>l. l<4 \<Longrightarrow> p && mask 2 = 0 \<Longrightarrow> p + l && ~~ mask 12 = p && ~~ mask 12" proof - fix l assume al: "p && mask 2 = 0" assume "(l::word32) < 4" hence less: "l<2^2" by simp have le: "(2::nat) \<le> 12" by simp show "?thesis l" by (rule is_aligned_add_helper[simplified is_aligned_mask,
          THEN conjunct2, THEN mask_out_first_mask_some, OF al less le]) qed show ?thesis apply (wp dmo_invs' no_irq_storeWord no_irq) apply (clarsimp simp: storeWord_def invs'_def valid_state'_def) apply (clarsimp simp: valid_machine_state'_def pointerInUserData_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>pointerInUserData p and invs'\<rbrace> doMachineOp (storeWord p w) \<lbrace>\<lambda>rv. invs'\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>pointerInUserData p and invs'\<rbrace> doMachineOp (storeWord p w) \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>l < 4; p && mask 2 = 0\<rbrakk> \<Longrightarrow> p + l && ~~ mask 12 = p && ~~ mask 12 proof (state)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>l < 4; p && mask 2 = 0\<rbrakk> \<Longrightarrow> p + l && ~~ mask 12 = p && ~~ mask 12 proof (state)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>l < 4; p && mask 2 = 0\<rbrakk> \<Longrightarrow> p + l && ~~ mask 12 = p && ~~ mask 12 proof (state)
this:
p && mask 2 = 0

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

goal (1 subgoal):
 1. \<And>l. \<lbrakk>l < 4; p && mask 2 = 0\<rbrakk> \<Longrightarrow> p + l && ~~ mask 12 = p && ~~ mask 12 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. \<lbrakk>l < 4; p && mask 2 = 0\<rbrakk> \<Longrightarrow> p + l && ~~ mask 12 = p && ~~ mask 12 proof (prove)
goal (1 subgoal):
 1. 2 \<le> 12 proof (state)
this:
2 \<le> 12

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

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

goal (1 subgoal):
 1. \<lbrace>pointerInUserData p and invs'\<rbrace> doMachineOp (storeWord p w) \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pointerInUserData p and invs'\<rbrace> doMachineOp (storeWord p w) \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (pointerInUserData p and invs') s \<Longrightarrow> ((\<lambda>s. \<forall>m. \<forall>(r, m')\<in>fst (storeWord p w m). \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory m' p = underlying_memory m p) and invs') s proof (prove)
goal (1 subgoal):
 1. \<And>s m b pa. \<lbrakk>pointerInUserData p s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ((), 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); \<not> pointerInUserData pa s; underlying_memory b pa \<noteq> underlying_memory m pa\<rbrakk> \<Longrightarrow> pointerInDeviceData pa s proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>pointerInUserData p and invs'\<rbrace> doMachineOp (storeWord p w) \<lbrace>\<lambda>rv. invs'\<rbrace>

goal:
No subgoals!