theory ArchADT_IF

lemma do_user_op_if_invs[ADT_IF_assms]:
  "\<lbrace>invs and ct_running\<rbrace>
   do_user_op_if f tc
   \<lbrace>\<lambda>_. invs and ct_running\<rbrace>" apply (simp add: do_user_op_if_def split_def) apply (wp do_machine_op_ct_in_state device_update_invs | wp (once) dmo_invs | simp)+ apply (clarsimp simp: user_mem_def user_memory_update_def simpler_modify_def restrict_map_def
                        invs_def cur_tcb_def ptable_rights_s_def ptable_lift_s_def) apply (frule ptable_rights_imp_frame) apply fastforce apply simp apply (clarsimp simp: valid_state_def device_frame_in_device_region) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and ct_running\<rbrace> do_user_op_if f tc \<lbrace>\<lambda>_. invs and ct_running\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and ct_running\<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 <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op 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 <- do_machine_op (user_memory_update ((fst (snd (snd p)) |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (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 <- do_machine_op (setExMonitor (snd (snd (snd (snd p)))));
return (fst p, fst (snd p))
od \<lbrace>\<lambda>_. invs and ct_running\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<and> ct_running s \<Longrightarrow> f (cur_thread 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, (\<lambda>a. user_mem s (ptrFromPAddr a)) |` {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 (machine_state 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 (machine_state s)) \<noteq> {} \<longrightarrow> (\<forall>x\<in>f (cur_thread 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, (\<lambda>a. user_mem s (ptrFromPAddr a)) |` {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 (machine_state 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 (machine_state s)). \<forall>m. \<forall>x\<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 (machine_state s)))) m). case x of (r, m') \<Rightarrow> (\<forall>p. in_user_frame p s \<or> underlying_memory m' p = underlying_memory m p) \<and> (m = machine_state s \<longrightarrow> (\<forall>irq. interrupt_states s irq = IRQInactive \<longrightarrow> irq_masks m' irq \<or> irq_masks m' irq = irq_masks (machine_state s) irq))) proof (prove)
goal (1 subgoal):
 1. \<And>s a aa ab ac ad b m p x. \<lbrakk>valid_state s; tcb_at (cur_thread s) s; ct_running s; f (cur_thread s) (\<lambda>a. if ptable_rights (cur_thread s) s a \<noteq> {} then ptable_lift (cur_thread s) s a else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa \<noteq> {} \<longrightarrow> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then if in_user_frame (ptrFromPAddr x) s then Some (underlying_memory (machine_state s) (ptrFromPAddr x)) else None else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa \<noteq> {} \<longrightarrow> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)) \<noteq> {}; (a, aa, ab, ac, ad, b) \<in> f (cur_thread s) (\<lambda>a. if ptable_rights (cur_thread s) s a \<noteq> {} then ptable_lift (cur_thread s) s a else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa \<noteq> {} \<longrightarrow> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then if in_user_frame (ptrFromPAddr x) s then Some (underlying_memory (machine_state s) (ptrFromPAddr x)) else None else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa \<noteq> {} \<longrightarrow> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)); ptable_rights (cur_thread s) s x \<noteq> {}; device_state (machine_state s) p = None; (case ab (addrFromPPtr p) of None \<Rightarrow> underlying_memory m p | Some x \<Rightarrow> x) \<noteq> underlying_memory m p; ptable_lift (cur_thread s) s x = Some (addrFromPPtr p); AllowWrite \<in> ptable_rights (cur_thread s) s x\<rbrakk> \<Longrightarrow> in_user_frame p s proof (prove)
goal (3 subgoals):
 1. \<And>s a aa ab ac ad b m p x. \<lbrakk>valid_state s; tcb_at (cur_thread s) s; ct_running s; f (cur_thread s) (\<lambda>a. if ptable_rights (cur_thread s) s a \<noteq> {} then ptable_lift (cur_thread s) s a else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa \<noteq> {} \<longrightarrow> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then if in_user_frame (ptrFromPAddr x) s then Some (underlying_memory (machine_state s) (ptrFromPAddr x)) else None else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa \<noteq> {} \<longrightarrow> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)) \<noteq> {}; (a, aa, ab, ac, ad, b) \<in> f (cur_thread s) (\<lambda>a. if ptable_rights (cur_thread s) s a \<noteq> {} then ptable_lift (cur_thread s) s a else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa \<noteq> {} \<longrightarrow> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then if in_user_frame (ptrFromPAddr x) s then Some (underlying_memory (machine_state s) (ptrFromPAddr x)) else None else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa \<noteq> {} \<longrightarrow> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)); ptable_rights (cur_thread s) s x \<noteq> {}; device_state (machine_state s) p = None; (case ab (addrFromPPtr p) of None \<Rightarrow> underlying_memory m p | Some x \<Rightarrow> x) \<noteq> underlying_memory m p; ptable_lift (cur_thread s) s x = Some (addrFromPPtr p); AllowWrite \<in> ptable_rights (cur_thread s) s x\<rbrakk> \<Longrightarrow> ptable_rights (?t195 s a aa ab ac ad b m p x) s (?x195 s a aa ab ac ad b m p x) \<noteq> {}
 2. \<And>s a aa ab ac ad b m p x. \<lbrakk>valid_state s; tcb_at (cur_thread s) s; ct_running s; f (cur_thread s) (\<lambda>a. if ptable_rights (cur_thread s) s a \<noteq> {} then ptable_lift (cur_thread s) s a else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa \<noteq> {} \<longrightarrow> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then if in_user_frame (ptrFromPAddr x) s then Some (underlying_memory (machine_state s) (ptrFromPAddr x)) else None else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa \<noteq> {} \<longrightarrow> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)) \<noteq> {}; (a, aa, ab, ac, ad, b) \<in> f (cur_thread s) (\<lambda>a. if ptable_rights (cur_thread s) s a \<noteq> {} then ptable_lift (cur_thread s) s a else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa \<noteq> {} \<longrightarrow> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then if in_user_frame (ptrFromPAddr x) s then Some (underlying_memory (machine_state s) (ptrFromPAddr x)) else None else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa \<noteq> {} \<longrightarrow> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)); ptable_rights (cur_thread s) s x \<noteq> {}; device_state (machine_state s) p = None; (case ab (addrFromPPtr p) of None \<Rightarrow> underlying_memory m p | Some x \<Rightarrow> x) \<noteq> underlying_memory m p; ptable_lift (cur_thread s) s x = Some (addrFromPPtr p); AllowWrite \<in> ptable_rights (cur_thread s) s x\<rbrakk> \<Longrightarrow> ptable_lift (?t195 s a aa ab ac ad b m p x) s (?x195 s a aa ab ac ad b m p x) = Some (addrFromPPtr (?y195 s a aa ab ac ad b m p x))
 3. \<And>s a aa ab ac ad b m p x. \<lbrakk>valid_state s; tcb_at (cur_thread s) s; ct_running s; f (cur_thread s) (\<lambda>a. if ptable_rights (cur_thread s) s a \<noteq> {} then ptable_lift (cur_thread s) s a else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa \<noteq> {} \<longrightarrow> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then if in_user_frame (ptrFromPAddr x) s then Some (underlying_memory (machine_state s) (ptrFromPAddr x)) else None else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa \<noteq> {} \<longrightarrow> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)) \<noteq> {}; (a, aa, ab, ac, ad, b) \<in> f (cur_thread s) (\<lambda>a. if ptable_rights (cur_thread s) s a \<noteq> {} then ptable_lift (cur_thread s) s a else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa \<noteq> {} \<longrightarrow> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then if in_user_frame (ptrFromPAddr x) s then Some (underlying_memory (machine_state s) (ptrFromPAddr x)) else None else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa \<noteq> {} \<longrightarrow> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)); ptable_rights (cur_thread s) s x \<noteq> {}; device_state (machine_state s) p = None; (case ab (addrFromPPtr p) of None \<Rightarrow> underlying_memory m p | Some x \<Rightarrow> x) \<noteq> underlying_memory m p; ptable_lift (cur_thread s) s x = Some (addrFromPPtr p); AllowWrite \<in> ptable_rights (cur_thread s) s x; in_user_frame (?y195 s a aa ab ac ad b m p x) s \<or> in_device_frame (?y195 s a aa ab ac ad b m p x) s\<rbrakk> \<Longrightarrow> in_user_frame p s proof (prove)
goal (2 subgoals):
 1. \<And>s a aa ab ac ad b m p x. \<lbrakk>valid_state s; tcb_at (cur_thread s) s; ct_running s; f (cur_thread s) (\<lambda>a. if ptable_rights (cur_thread s) s a \<noteq> {} then ptable_lift (cur_thread s) s a else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa \<noteq> {} \<longrightarrow> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then if in_user_frame (ptrFromPAddr x) s then Some (underlying_memory (machine_state s) (ptrFromPAddr x)) else None else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa \<noteq> {} \<longrightarrow> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)) \<noteq> {}; (a, aa, ab, ac, ad, b) \<in> f (cur_thread s) (\<lambda>a. if ptable_rights (cur_thread s) s a \<noteq> {} then ptable_lift (cur_thread s) s a else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa \<noteq> {} \<longrightarrow> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then if in_user_frame (ptrFromPAddr x) s then Some (underlying_memory (machine_state s) (ptrFromPAddr x)) else None else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa \<noteq> {} \<longrightarrow> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)); ptable_rights (cur_thread s) s x \<noteq> {}; device_state (machine_state s) p = None; (case ab (addrFromPPtr p) of None \<Rightarrow> underlying_memory m p | Some x \<Rightarrow> x) \<noteq> underlying_memory m p; ptable_lift (cur_thread s) s x = Some (addrFromPPtr p); AllowWrite \<in> ptable_rights (cur_thread s) s x\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = Some (addrFromPPtr (?y195 s a aa ab ac ad b m p x))
 2. \<And>s a aa ab ac ad b m p x. \<lbrakk>valid_state s; tcb_at (cur_thread s) s; ct_running s; f (cur_thread s) (\<lambda>a. if ptable_rights (cur_thread s) s a \<noteq> {} then ptable_lift (cur_thread s) s a else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa \<noteq> {} \<longrightarrow> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then if in_user_frame (ptrFromPAddr x) s then Some (underlying_memory (machine_state s) (ptrFromPAddr x)) else None else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa \<noteq> {} \<longrightarrow> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)) \<noteq> {}; (a, aa, ab, ac, ad, b) \<in> f (cur_thread s) (\<lambda>a. if ptable_rights (cur_thread s) s a \<noteq> {} then ptable_lift (cur_thread s) s a else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa \<noteq> {} \<longrightarrow> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then if in_user_frame (ptrFromPAddr x) s then Some (underlying_memory (machine_state s) (ptrFromPAddr x)) else None else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa \<noteq> {} \<longrightarrow> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)); ptable_rights (cur_thread s) s x \<noteq> {}; device_state (machine_state s) p = None; (case ab (addrFromPPtr p) of None \<Rightarrow> underlying_memory m p | Some x \<Rightarrow> x) \<noteq> underlying_memory m p; ptable_lift (cur_thread s) s x = Some (addrFromPPtr p); AllowWrite \<in> ptable_rights (cur_thread s) s x; in_user_frame (?y195 s a aa ab ac ad b m p x) s \<or> in_device_frame (?y195 s a aa ab ac ad b m p x) s\<rbrakk> \<Longrightarrow> in_user_frame p s proof (prove)
goal (1 subgoal):
 1. \<And>s a aa ab ac ad b m p x. \<lbrakk>valid_state s; tcb_at (cur_thread s) s; ct_running s; f (cur_thread s) (\<lambda>a. if ptable_rights (cur_thread s) s a \<noteq> {} then ptable_lift (cur_thread s) s a else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa \<noteq> {} \<longrightarrow> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then if in_user_frame (ptrFromPAddr x) s then Some (underlying_memory (machine_state s) (ptrFromPAddr x)) else None else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa \<noteq> {} \<longrightarrow> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)) \<noteq> {}; (a, aa, ab, ac, ad, b) \<in> f (cur_thread s) (\<lambda>a. if ptable_rights (cur_thread s) s a \<noteq> {} then ptable_lift (cur_thread s) s a else None) (ptable_rights (cur_thread s) s) (\<lambda>a. ptable_rights (cur_thread s) s a \<noteq> {} \<and> ptable_xn_s s a) (tc, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa \<noteq> {} \<longrightarrow> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then if in_user_frame (ptrFromPAddr x) s then Some (underlying_memory (machine_state s) (ptrFromPAddr x)) else None else None, \<lambda>x. if \<exists>xa. (ptable_rights (cur_thread s) s xa \<noteq> {} \<longrightarrow> ptable_lift (cur_thread s) s xa = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s xa) \<and> ptable_rights (cur_thread s) s xa \<noteq> {} then (device_state (machine_state s) \<circ> ptrFromPAddr) x else None, exclusive_state (machine_state s)); ptable_rights (cur_thread s) s x \<noteq> {}; device_state (machine_state s) p = None; (case ab (addrFromPPtr p) of None \<Rightarrow> underlying_memory m p | Some x \<Rightarrow> x) \<noteq> underlying_memory m p; ptable_lift (cur_thread s) s x = Some (addrFromPPtr p); AllowWrite \<in> ptable_rights (cur_thread s) s x; in_user_frame p s \<or> in_device_frame p s\<rbrakk> \<Longrightarrow> in_user_frame p s proof (prove)
goal:
No subgoals!