theory TcbAcc_R

lemma dmo_invs_no_cicd':
  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_no_cicd'\<rbrace> doMachineOp f \<lbrace>\<lambda>r. invs_no_cicd'\<rbrace>" apply (simp add: doMachineOp_def split_def) apply wp apply clarsimp apply (subst invs_no_cicd'_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 all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> doMachineOp f \<lbrace>\<lambda>r. all_invs_but_ct_idle_or_in_cur_domain'\<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 all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> do ms <- gets ksMachineState;
p <- select_f (f ms);
y <- modify (ksMachineState_update (\<lambda>_. snd p));
return (fst p)
od \<lbrace>\<lambda>r. all_invs_but_ct_idle_or_in_cur_domain'\<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 all_invs_but_ct_idle_or_in_cur_domain') s \<Longrightarrow> \<forall>x\<in>fst (f (ksMachineState s)). all_invs_but_ct_idle_or_in_cur_domain' (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; all_invs_but_ct_idle_or_in_cur_domain' s\<rbrakk> \<Longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' (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; all_invs_but_ct_idle_or_in_cur_domain' 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; all_invs_but_ct_idle_or_in_cur_domain' 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; all_invs_but_ct_idle_or_in_cur_domain' s\<rbrakk> \<Longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' 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; all_invs_but_ct_idle_or_in_cur_domain' 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; all_invs_but_ct_idle_or_in_cur_domain' 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; all_invs_but_ct_idle_or_in_cur_domain' 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; all_invs_but_ct_idle_or_in_cur_domain' 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; all_invs_but_ct_idle_or_in_cur_domain' s\<rbrakk> \<Longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' 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; all_invs_but_ct_idle_or_in_cur_domain' 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; all_invs_but_ct_idle_or_in_cur_domain' s\<rbrakk> \<Longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' 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; all_invs_but_ct_idle_or_in_cur_domain' s\<rbrakk> \<Longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s proof (prove)
goal:
No subgoals!