theory TcbAcc_R

lemma dmo_invs':
  assumes masks: "\<And>P. \<lbrace>\<lambda>s. P (irq_masks s)\<rbrace> f \<lbrace>\<lambda>_ s. P (irq_masks s)\<rbrace>"
  shows "\<lbrace>(\<lambda>s. \<forall>m. \<forall>(r,m')\<in>fst (f m). \<forall>p.
             pointerInUserData p s \<or> pointerInDeviceData p s \<or>
             underlying_memory m' p = underlying_memory m p) and
          invs'\<rbrace> doMachineOp f \<lbrace>\<lambda>r. invs'\<rbrace>" apply (simp add: doMachineOp_def split_def) apply wp apply clarsimp apply (subst invs'_machine) apply (drule use_valid) apply (rule_tac P="\<lambda>m. m = irq_masks (ksMachineState s)" in masks, simp+) apply (fastforce simp add: valid_machine_state'_def) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>m. \<forall>(r, m')\<in>fst (f m). \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory m' p = underlying_memory m p) and invs'\<rbrace> doMachineOp f \<lbrace>\<lambda>r. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>m. \<forall>x\<in>fst (f m). \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (snd x) p = underlying_memory m p) and invs'\<rbrace> do ms <- gets ksMachineState;
p <- select_f (f ms);
y <- modify (ksMachineState_update (\<lambda>_. snd p));
return (fst p)
od \<lbrace>\<lambda>r. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. \<forall>m. \<forall>x\<in>fst (f m). \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (snd x) p = underlying_memory m p) and invs') s \<Longrightarrow> \<forall>x\<in>fst (f (ksMachineState s)). invs' (s\<lparr>ksMachineState := snd x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f (ksMachineState s)); \<forall>m. \<forall>x\<in>fst (f m). \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (snd x) p = underlying_memory m p; invs' s\<rbrakk> \<Longrightarrow> invs' (s\<lparr>ksMachineState := b\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f (ksMachineState s)); \<forall>m. \<forall>x\<in>fst (f m). \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (snd x) p = underlying_memory m p; invs' s\<rbrakk> \<Longrightarrow> irq_masks b = irq_masks (ksMachineState s)
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f (ksMachineState s)); \<forall>m. \<forall>x\<in>fst (f m). \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (snd x) p = underlying_memory m p; invs' s\<rbrakk> \<Longrightarrow> valid_machine_state' (s\<lparr>ksMachineState := b\<rparr>) = valid_machine_state' s
 3. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f (ksMachineState s)); \<forall>m. \<forall>x\<in>fst (f m). \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (snd x) p = underlying_memory m p; invs' s\<rbrakk> \<Longrightarrow> invs' s proof (prove)
goal (5 subgoals):
 1. \<And>s a b. \<lbrakk>\<forall>m. \<forall>x\<in>fst (f m). \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (snd x) p = underlying_memory m p; invs' s\<rbrakk> \<Longrightarrow> \<lbrace>?P17 s a b\<rbrace> f \<lbrace>?Q17 s a b\<rbrace>
 2. \<And>s a b. \<lbrakk>\<forall>m. \<forall>x\<in>fst (f m). \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (snd x) p = underlying_memory m p; invs' s\<rbrakk> \<Longrightarrow> ?P17 s a b (ksMachineState s)
 3. \<And>s a b. \<lbrakk>\<forall>m. \<forall>x\<in>fst (f m). \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (snd x) p = underlying_memory m p; invs' s; ?Q17 s a b a b\<rbrakk> \<Longrightarrow> irq_masks b = irq_masks (ksMachineState s)
 4. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f (ksMachineState s)); \<forall>m. \<forall>x\<in>fst (f m). \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (snd x) p = underlying_memory m p; invs' s\<rbrakk> \<Longrightarrow> valid_machine_state' (s\<lparr>ksMachineState := b\<rparr>) = valid_machine_state' s
 5. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f (ksMachineState s)); \<forall>m. \<forall>x\<in>fst (f m). \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (snd x) p = underlying_memory m p; invs' s\<rbrakk> \<Longrightarrow> invs' s proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f (ksMachineState s)); \<forall>m. \<forall>x\<in>fst (f m). \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (snd x) p = underlying_memory m p; invs' s\<rbrakk> \<Longrightarrow> valid_machine_state' (s\<lparr>ksMachineState := b\<rparr>) = valid_machine_state' s
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f (ksMachineState s)); \<forall>m. \<forall>x\<in>fst (f m). \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (snd x) p = underlying_memory m p; invs' s\<rbrakk> \<Longrightarrow> invs' s proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f (ksMachineState s)); \<forall>m. \<forall>x\<in>fst (f m). \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (snd x) p = underlying_memory m p; invs' s\<rbrakk> \<Longrightarrow> invs' s proof (prove)
goal:
No subgoals!