theory ArchADT_IF_Refine

lemma doUserOp_if_invs'[ADT_IF_Refine_assms, wp]:
  "\<lbrace>invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and ex_abs (einvs)\<rbrace>
   doUserOp_if f tc
   \<lbrace>\<lambda>_. invs'\<rbrace>" apply (simp add: doUserOp_if_def split_def ex_abs_def) apply (wp device_update_invs' dmo_setExMonitor_wp' dmo_invs' | simp)+ apply (clarsimp simp add: no_irq_modify user_memory_update_def) apply wpsimp apply wp+ apply (clarsimp simp: user_memory_update_def simpler_modify_def
                        restrict_map_def
                 split: option.splits) apply (auto dest: ptable_rights_imp_UserData[rotated 2]
              simp: ptable_rights_s'_def ptable_lift_s'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and ex_abs einvs\<rbrace> doUserOp_if f tc \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s)\<rbrace> do pr <- gets ptable_rights_s';
pxn <- gets (\<lambda>s x. pr x \<noteq> {} \<and> ptable_xn_s' s x);
pl <- gets (\<lambda>s. ptable_lift_s' s |` {x. pr x \<noteq> {}});
t <- getCurThread;
um <- gets (\<lambda>s. user_mem' s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> ksMachineState);
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
es <- doMachineOp getExMonitor;
y <- assert (f t pl pr pxn (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, es) \<noteq> {});
p <- select (f t pl pr pxn (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, es));
y <- doMachineOp (user_memory_update ((fst (snd (snd p)) |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- doMachineOp (device_memory_update ((fst (snd (snd (snd p))) |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- doMachineOp (setExMonitor (snd (snd (snd (snd p)))));
return (fst p, fst (snd p))
od \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (14 subgoals):
 1. \<And>pr pl ds p P. \<lbrace>\<lambda>s. P (irq_masks s)\<rbrace> user_memory_update ((fst (snd (snd p)) |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)) \<lbrace>\<lambda>_ s. P (irq_masks s)\<rbrace>
 2. \<And>pr pxn pl x um dm ds y ya es yb. \<lbrace>?B11 pr pxn pl x um dm ds y ya es yb\<rbrace> select (f x pl pr pxn (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, es)) \<lbrace>\<lambda>p. (\<lambda>s. \<forall>m. \<forall>(r, m')\<in>fst (user_memory_update ((fst (snd (snd p)) |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)) m). \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory m' p = underlying_memory m p) and invs'\<rbrace>
 3. \<And>pr pxn pl x um dm ds y ya es. \<lbrace>?B10 pr pxn pl x um dm ds y ya es\<rbrace> assert (f x pl pr pxn (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, es) \<noteq> {}) \<lbrace>?B11 pr pxn pl x um dm ds y ya es\<rbrace>
 4. \<And>pr pxn pl x um dm ds y ya. \<lbrace>?B9 pr pxn pl x um dm ds y ya\<rbrace> doMachineOp getExMonitor \<lbrace>?B10 pr pxn pl x um dm ds y ya\<rbrace>
 5. \<And>pr pxn pl x um dm ds y. \<lbrace>?B8 pr pxn pl x um dm ds y\<rbrace> assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds) \<lbrace>?B9 pr pxn pl x um dm ds y\<rbrace>
 6. \<And>pr pxn pl x um dm ds. \<lbrace>?B7 pr pxn pl x um dm ds\<rbrace> assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds) \<lbrace>?B8 pr pxn pl x um dm ds\<rbrace>
 7. \<And>pr pxn pl x um dm. \<lbrace>?B6 pr pxn pl x um dm\<rbrace> gets (device_state \<circ> ksMachineState) \<lbrace>?B7 pr pxn pl x um dm\<rbrace>
 8. \<And>pr pxn pl x um. \<lbrace>?B5 pr pxn pl x um\<rbrace> gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr) \<lbrace>?B6 pr pxn pl x um\<rbrace>
 9. \<And>pr pxn pl x. \<lbrace>?B4 pr pxn pl x\<rbrace> gets (\<lambda>s. user_mem' s \<circ> ptrFromPAddr) \<lbrace>?B5 pr pxn pl x\<rbrace>
 10. \<And>pr pxn pl. \<lbrace>?B3 pr pxn pl\<rbrace> getCurThread \<lbrace>?B4 pr pxn pl\<rbrace>
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>pr pl ds a P. \<lbrace>\<lambda>s. P (irq_masks s)\<rbrace> modify (\<lambda>ms. ms\<lparr>underlying_memory := \<lambda>aa. case ((a |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)) aa of None \<Rightarrow> underlying_memory ms aa | Some x \<Rightarrow> x\<rparr>) \<lbrace>\<lambda>_ s. P (irq_masks s)\<rbrace>
 2. \<And>pr pxn pl x um dm ds y ya es yb. \<lbrace>?B11 pr pxn pl x um dm ds y ya es yb\<rbrace> select (f x pl pr pxn (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, es)) \<lbrace>\<lambda>p. (\<lambda>s. \<forall>m. \<forall>(r, m')\<in>fst (user_memory_update ((fst (snd (snd p)) |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)) m). \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory m' p = underlying_memory m p) and invs'\<rbrace>
 3. \<And>pr pxn pl x um dm ds y ya es. \<lbrace>?B10 pr pxn pl x um dm ds y ya es\<rbrace> assert (f x pl pr pxn (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, es) \<noteq> {}) \<lbrace>?B11 pr pxn pl x um dm ds y ya es\<rbrace>
 4. \<And>pr pxn pl x um dm ds y ya. \<lbrace>?B9 pr pxn pl x um dm ds y ya\<rbrace> doMachineOp getExMonitor \<lbrace>?B10 pr pxn pl x um dm ds y ya\<rbrace>
 5. \<And>pr pxn pl x um dm ds y. \<lbrace>?B8 pr pxn pl x um dm ds y\<rbrace> assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds) \<lbrace>?B9 pr pxn pl x um dm ds y\<rbrace>
 6. \<And>pr pxn pl x um dm ds. \<lbrace>?B7 pr pxn pl x um dm ds\<rbrace> assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds) \<lbrace>?B8 pr pxn pl x um dm ds\<rbrace>
 7. \<And>pr pxn pl x um dm. \<lbrace>?B6 pr pxn pl x um dm\<rbrace> gets (device_state \<circ> ksMachineState) \<lbrace>?B7 pr pxn pl x um dm\<rbrace>
 8. \<And>pr pxn pl x um. \<lbrace>?B5 pr pxn pl x um\<rbrace> gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr) \<lbrace>?B6 pr pxn pl x um\<rbrace>
 9. \<And>pr pxn pl x. \<lbrace>?B4 pr pxn pl x\<rbrace> gets (\<lambda>s. user_mem' s \<circ> ptrFromPAddr) \<lbrace>?B5 pr pxn pl x\<rbrace>
 10. \<And>pr pxn pl. \<lbrace>?B3 pr pxn pl\<rbrace> getCurThread \<lbrace>?B4 pr pxn pl\<rbrace>
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>pr pxn pl x um dm ds y ya es yb. \<lbrace>?B11 pr pxn pl x um dm ds y ya es yb\<rbrace> select (f x pl pr pxn (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, es)) \<lbrace>\<lambda>p. (\<lambda>s. \<forall>m. \<forall>(r, m')\<in>fst (user_memory_update ((fst (snd (snd p)) |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)) m). \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory m' p = underlying_memory m p) and invs'\<rbrace>
 2. \<And>pr pxn pl x um dm ds y ya es. \<lbrace>?B10 pr pxn pl x um dm ds y ya es\<rbrace> assert (f x pl pr pxn (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, es) \<noteq> {}) \<lbrace>?B11 pr pxn pl x um dm ds y ya es\<rbrace>
 3. \<And>pr pxn pl x um dm ds y ya. \<lbrace>?B9 pr pxn pl x um dm ds y ya\<rbrace> doMachineOp getExMonitor \<lbrace>?B10 pr pxn pl x um dm ds y ya\<rbrace>
 4. \<And>pr pxn pl x um dm ds y. \<lbrace>?B8 pr pxn pl x um dm ds y\<rbrace> assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds) \<lbrace>?B9 pr pxn pl x um dm ds y\<rbrace>
 5. \<And>pr pxn pl x um dm ds. \<lbrace>?B7 pr pxn pl x um dm ds\<rbrace> assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds) \<lbrace>?B8 pr pxn pl x um dm ds\<rbrace>
 6. \<And>pr pxn pl x um dm. \<lbrace>?B6 pr pxn pl x um dm\<rbrace> gets (device_state \<circ> ksMachineState) \<lbrace>?B7 pr pxn pl x um dm\<rbrace>
 7. \<And>pr pxn pl x um. \<lbrace>?B5 pr pxn pl x um\<rbrace> gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr) \<lbrace>?B6 pr pxn pl x um\<rbrace>
 8. \<And>pr pxn pl x. \<lbrace>?B4 pr pxn pl x\<rbrace> gets (\<lambda>s. user_mem' s \<circ> ptrFromPAddr) \<lbrace>?B5 pr pxn pl x\<rbrace>
 9. \<And>pr pxn pl. \<lbrace>?B3 pr pxn pl\<rbrace> getCurThread \<lbrace>?B4 pr pxn pl\<rbrace>
 10. \<And>pr pxn. \<lbrace>?B2 pr pxn\<rbrace> gets (\<lambda>s. ptable_lift_s' s |` {x. pr x \<noteq> {}}) \<lbrace>?B3 pr pxn\<rbrace>
A total of 13 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s)) s \<Longrightarrow> dom (user_mem' s \<circ> ptrFromPAddr \<circ> addrFromPPtr) \<subseteq> - dom ((device_state \<circ> ksMachineState) s) \<longrightarrow> dom (device_mem' s \<circ> ptrFromPAddr \<circ> addrFromPPtr) \<subseteq> dom ((device_state \<circ> ksMachineState) s) \<longrightarrow> f (ksCurThread s) (ptable_lift_s' s |` {x. ptable_rights_s' s x \<noteq> {}}) (ptable_rights_s' s) (\<lambda>a. ptable_rights_s' s a \<noteq> {} \<and> ptable_xn_s' s a) (tc, (user_mem' s \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s' s |` {x. ptable_rights_s' s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s' s x}, ((device_state \<circ> ksMachineState) s \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s' s |` {x. ptable_rights_s' s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s' s x}, exclusive_state (ksMachineState s)) \<noteq> {} \<longrightarrow> (\<forall>x\<in>f (ksCurThread s) (ptable_lift_s' s |` {x. ptable_rights_s' s x \<noteq> {}}) (ptable_rights_s' s) (\<lambda>a. ptable_rights_s' s a \<noteq> {} \<and> ptable_xn_s' s a) (tc, (user_mem' s \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s' s |` {x. ptable_rights_s' s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s' s x}, ((device_state \<circ> ksMachineState) s \<circ> ptrFromPAddr) |` {y. \<exists>x. (ptable_lift_s' s |` {x. ptable_rights_s' s x \<noteq> {}}) x = Some y \<and> AllowRead \<in> ptable_rights_s' s x}, exclusive_state (ksMachineState s)). ((\<lambda>sa. \<forall>m. \<forall>(r, m')\<in>fst (user_memory_update ((fst (snd (snd x)) |` {y. \<exists>x. (ptable_lift_s' s |` {x. ptable_rights_s' s x \<noteq> {}}) x = Some y \<and> AllowWrite \<in> ptable_rights_s' s x} \<circ> addrFromPPtr) |` (- dom ((device_state \<circ> ksMachineState) s))) m). \<forall>p. pointerInUserData p sa \<or> pointerInDeviceData p sa \<or> underlying_memory m' p = underlying_memory m p) and invs') s) proof (prove)
goal (1 subgoal):
 1. \<And>s sa a aa ab ac ad b m p x2 x. \<lbrakk>invs' s; ksSchedulerAction s = ResumeCurrentThread; ct_running' s; (sa, s) \<in> state_relation; invs sa; valid_list sa; valid_sched sa; dom ((\<lambda>a. user_mem' s (ptrFromPAddr a)) \<circ> addrFromPPtr) \<subseteq> - dom (device_state (ksMachineState s)); dom ((\<lambda>a. device_mem' s (ptrFromPAddr a)) \<circ> addrFromPPtr) \<subseteq> dom (device_state (ksMachineState s)); f (ksCurThread s) (\<lambda>a. if ptable_rights_s' s a \<noteq> {} then ptable_lift_s' s a else None) (ptable_rights_s' s) (\<lambda>a. ptable_rights_s' s a \<noteq> {} \<and> ptable_xn_s' s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights_s' s xa \<noteq> {} \<longrightarrow> ptable_lift_s' s xa = Some x \<and> AllowRead \<in> ptable_rights_s' s xa) \<and> ptable_rights_s' s xa \<noteq> {} then user_mem' s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>xa. (ptable_rights_s' s xa \<noteq> {} \<longrightarrow> ptable_lift_s' s xa = Some x \<and> AllowRead \<in> ptable_rights_s' s xa) \<and> ptable_rights_s' s xa \<noteq> {} then (device_state (ksMachineState s) \<circ> ptrFromPAddr) x else None, exclusive_state (ksMachineState s)) \<noteq> {}; (a, aa, ab, ac, ad, b) \<in> f (ksCurThread s) (\<lambda>a. if ptable_rights_s' s a \<noteq> {} then ptable_lift_s' s a else None) (ptable_rights_s' s) (\<lambda>a. ptable_rights_s' s a \<noteq> {} \<and> ptable_xn_s' s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights_s' s xa \<noteq> {} \<longrightarrow> ptable_lift_s' s xa = Some x \<and> AllowRead \<in> ptable_rights_s' s xa) \<and> ptable_rights_s' s xa \<noteq> {} then user_mem' s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>xa. (ptable_rights_s' s xa \<noteq> {} \<longrightarrow> ptable_lift_s' s xa = Some x \<and> AllowRead \<in> ptable_rights_s' s xa) \<and> ptable_rights_s' s xa \<noteq> {} then (device_state (ksMachineState s) \<circ> ptrFromPAddr) x else None, exclusive_state (ksMachineState s)); ab (addrFromPPtr p) = Some x2; ptable_rights_s' s x \<noteq> {}; device_state (ksMachineState s) p = None; \<not> pointerInUserData p s; x2 \<noteq> underlying_memory m p; ptable_lift_s' s x = Some (addrFromPPtr p); AllowWrite \<in> ptable_rights_s' s x\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal:
No subgoals!