theory Refine

lemma doUserOp_invs':
  "\<lbrace>invs' and ex_abs einvs and
    (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and
    (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list'\<rbrace>
   doUserOp f tc
   \<lbrace>\<lambda>_. invs' and
        (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and
        (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list'\<rbrace>" apply (simp add: doUserOp_def split_def ex_abs_def) apply (wp device_update_invs'
    | (wp (once) dmo_invs', wpsimp simp: no_irq_modify device_memory_update_def
                                       user_memory_update_def))+ apply (clarsimp simp: user_memory_update_def simpler_modify_def
                        restrict_map_def
                 split: option.splits) apply (frule ptable_rights_imp_UserData[rotated 2], auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ex_abs einvs and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list'\<rbrace> doUserOp f tc \<lbrace>\<lambda>_. invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list'\<rbrace> do t <- getCurThread;
trans <- gets (ptable_lift t \<circ> absKState);
perms <- gets (ptable_rights t \<circ> absKState);
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);
p <- select (fst (f t (trans |` {pa. perms pa \<noteq> {}}) perms (tc, um |` {pa. \<exists>va. trans va = Some pa \<and> AllowRead \<in> perms va}, (ds \<circ> ptrFromPAddr) |` {pa. \<exists>va. trans va = Some pa \<and> AllowRead \<in> perms va})));
y <- doMachineOp (user_memory_update ((fst (snd (snd p)) |` {pa. \<exists>va. trans va = Some pa \<and> AllowWrite \<in> perms va} \<circ> addrFromPPtr) |` (- dom ds)));
y <- doMachineOp (device_memory_update ((snd (snd (snd p)) |` {pa. \<exists>va. trans va = Some pa \<and> AllowWrite \<in> perms va} \<circ> addrFromPPtr) |` dom ds));
return (fst p, fst (snd p))
od \<lbrace>\<lambda>_. invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list') 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> (\<forall>x\<in>fst (f (ksCurThread s) ((ptable_lift (ksCurThread s) \<circ> absKState) s |` {pa. (ptable_rights (ksCurThread s) \<circ> absKState) s pa \<noteq> {}}) ((ptable_rights (ksCurThread s) \<circ> absKState) s) (tc, (user_mem' s \<circ> ptrFromPAddr) |` {pa. \<exists>va. (ptable_lift (ksCurThread s) \<circ> absKState) s va = Some pa \<and> AllowRead \<in> (ptable_rights (ksCurThread s) \<circ> absKState) s va}, ((device_state \<circ> ksMachineState) s \<circ> ptrFromPAddr) |` {pa. \<exists>va. (ptable_lift (ksCurThread s) \<circ> absKState) s va = Some pa \<and> AllowRead \<in> (ptable_rights (ksCurThread s) \<circ> absKState) s va})). ((\<lambda>sa. \<forall>m. \<forall>(r, m')\<in>fst (user_memory_update ((fst (snd (snd x)) |` {pa. \<exists>va. (ptable_lift (ksCurThread s) \<circ> absKState) s va = Some pa \<and> AllowWrite \<in> (ptable_rights (ksCurThread s) \<circ> absKState) s va} \<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 \<and> ksSchedulerAction s = ResumeCurrentThread \<and> ct_running' s \<and> 0 < ksDomainTime s \<and> valid_domain_list' s) proof (prove)
goal (1 subgoal):
 1. \<And>s sa a aa ab b m p x2 va. \<lbrakk>invs' s; ksSchedulerAction s = ResumeCurrentThread; (sa, s) \<in> state_relation; ct_running' s; invs sa; 0 < ksDomainTime s; valid_domain_list' s; 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)); (a, aa, ab, b) \<in> fst (f (ksCurThread s) (\<lambda>x. if ptable_rights (ksCurThread s) (absKState s) x \<noteq> {} then ptable_lift (ksCurThread s) (absKState s) x else None) (ptable_rights (ksCurThread s) (absKState s)) (tc, \<lambda>x. if \<exists>va. ptable_lift (ksCurThread s) (absKState s) va = Some x \<and> AllowRead \<in> ptable_rights (ksCurThread s) (absKState s) va then user_mem' s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>va. ptable_lift (ksCurThread s) (absKState s) va = Some x \<and> AllowRead \<in> ptable_rights (ksCurThread s) (absKState s) va then device_state (ksMachineState s) (ptrFromPAddr x) else None)); ab (addrFromPPtr p) = Some x2; ptable_lift (ksCurThread s) (absKState s) va = Some (addrFromPPtr p); AllowWrite \<in> ptable_rights (ksCurThread s) (absKState s) va; device_state (ksMachineState s) p = None; \<not> pointerInUserData p s; x2 \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal:
No subgoals!