theory AInvs

lemma do_user_op_invs:
  "\<lbrace>invs and ct_running\<rbrace>
   do_user_op f tc
   \<lbrace>\<lambda>_. invs and ct_running\<rbrace>" apply (simp add: do_user_op_def split_def) apply (wp device_update_invs) apply (wp do_machine_op_ct_in_state dmo_invs | simp add:dom_restrict_plus_eq)+ apply (clarsimp simp: user_memory_update_def simpler_modify_def
                        restrict_map_def invs_def cur_tcb_def
                 split: option.splits if_split_asm) apply (frule ptable_rights_imp_frame) apply fastforce+ 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 f tc \<lbrace>\<lambda>_. invs and ct_running\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and ct_running\<rbrace> do t <- gets cur_thread;
conv <- gets (ptable_lift t);
rights <- gets (ptable_rights t);
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);
p <- select (fst (f t (conv |` {pa. rights pa \<noteq> {}}) rights (tc, um |` {pa. \<exists>va. conv va = Some pa \<and> AllowRead \<in> rights va}, (ds \<circ> ptrFromPAddr) |` {pa. \<exists>va. conv va = Some pa \<and> AllowRead \<in> rights va})));
y <- do_machine_op (user_memory_update ((fst (snd (snd p)) |` {pa. \<exists>va. conv va = Some pa \<and> AllowWrite \<in> rights va} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((snd (snd (snd p)) |` {pa. \<exists>va. conv va = Some pa \<and> AllowWrite \<in> rights va} \<circ> addrFromPPtr) |` dom ds));
return (fst p, fst (snd p))
od \<lbrace>\<lambda>_. invs and ct_running\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>t conv rights um dm ds p. \<lbrace>?B7 t conv rights um dm ds p\<rbrace> do_machine_op (user_memory_update ((fst (snd (snd p)) |` {pa. \<exists>va. conv va = Some pa \<and> AllowWrite \<in> rights va} \<circ> addrFromPPtr) |` (- dom ds))) \<lbrace>\<lambda>y s. invs s \<and> dom ((snd (snd (snd p)) |` {pa. \<exists>va. conv va = Some pa \<and> AllowWrite \<in> rights va} \<circ> addrFromPPtr) |` dom ds) \<subseteq> dom (device_state (machine_state s)) \<and> ct_running s\<rbrace>
 2. \<And>t conv rights um dm ds. \<lbrace>?B6 t conv rights um dm ds\<rbrace> select (fst (f t (conv |` {pa. rights pa \<noteq> {}}) rights (tc, um |` {pa. \<exists>va. conv va = Some pa \<and> AllowRead \<in> rights va}, (ds \<circ> ptrFromPAddr) |` {pa. \<exists>va. conv va = Some pa \<and> AllowRead \<in> rights va}))) \<lbrace>?B7 t conv rights um dm ds\<rbrace>
 3. \<And>t conv rights um dm. \<lbrace>?B5 t conv rights um dm\<rbrace> gets (device_state \<circ> machine_state) \<lbrace>?B6 t conv rights um dm\<rbrace>
 4. \<And>t conv rights um. \<lbrace>?B4 t conv rights um\<rbrace> gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr) \<lbrace>?B5 t conv rights um\<rbrace>
 5. \<And>t conv rights. \<lbrace>?B3 t conv rights\<rbrace> gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr) \<lbrace>?B4 t conv rights\<rbrace>
 6. \<And>t conv. \<lbrace>?B2 t conv\<rbrace> gets (ptable_rights t) \<lbrace>?B3 t conv\<rbrace>
 7. \<And>t. \<lbrace>?B1 t\<rbrace> gets (ptable_lift t) \<lbrace>?B2 t\<rbrace>
 8. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?B1\<rbrace>
 9. \<And>s. (invs and ct_running) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<and> ct_running s \<Longrightarrow> \<forall>x\<in>fst (f (cur_thread s) (ptable_lift (cur_thread s) s |` {pa. ptable_rights (cur_thread s) s pa \<noteq> {}}) (ptable_rights (cur_thread s) s) (tc, (\<lambda>a. user_mem s (ptrFromPAddr a)) |` {pa. \<exists>va. ptable_lift (cur_thread s) s va = Some pa \<and> AllowRead \<in> ptable_rights (cur_thread s) s va}, (device_state (machine_state s) \<circ> ptrFromPAddr) |` {pa. \<exists>va. ptable_lift (cur_thread s) s va = Some pa \<and> AllowRead \<in> ptable_rights (cur_thread s) s va})). \<forall>m. \<forall>x\<in>fst (user_memory_update ((fst (snd (snd x)) |` {pa. \<exists>va. ptable_lift (cur_thread s) s va = Some pa \<and> AllowWrite \<in> ptable_rights (cur_thread s) s va} \<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 b m p x2 va. \<lbrakk>(a, aa, ab, b) \<in> fst (f (cur_thread s) (\<lambda>x. if ptable_rights (cur_thread s) s x \<noteq> {} then ptable_lift (cur_thread s) s x else None) (ptable_rights (cur_thread s) s) (tc, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then device_state (machine_state s) (ptrFromPAddr x) else None)); valid_state s; tcb_at (cur_thread s) s; ct_running s; ab (addrFromPPtr p) = Some x2; ptable_lift (cur_thread s) s va = Some (addrFromPPtr p); AllowWrite \<in> ptable_rights (cur_thread s) s va; device_state (machine_state s) p = None; x2 \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> in_user_frame p s proof (prove)
goal (3 subgoals):
 1. \<And>s a aa ab b m p x2 va. \<lbrakk>(a, aa, ab, b) \<in> fst (f (cur_thread s) (\<lambda>x. if ptable_rights (cur_thread s) s x \<noteq> {} then ptable_lift (cur_thread s) s x else None) (ptable_rights (cur_thread s) s) (tc, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then device_state (machine_state s) (ptrFromPAddr x) else None)); valid_state s; tcb_at (cur_thread s) s; ct_running s; ab (addrFromPPtr p) = Some x2; ptable_lift (cur_thread s) s va = Some (addrFromPPtr p); AllowWrite \<in> ptable_rights (cur_thread s) s va; device_state (machine_state s) p = None; x2 \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> ptable_rights (?t117 s a aa ab b m p x2 va) s (?x117 s a aa ab b m p x2 va) \<noteq> {}
 2. \<And>s a aa ab b m p x2 va. \<lbrakk>(a, aa, ab, b) \<in> fst (f (cur_thread s) (\<lambda>x. if ptable_rights (cur_thread s) s x \<noteq> {} then ptable_lift (cur_thread s) s x else None) (ptable_rights (cur_thread s) s) (tc, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then device_state (machine_state s) (ptrFromPAddr x) else None)); valid_state s; tcb_at (cur_thread s) s; ct_running s; ab (addrFromPPtr p) = Some x2; ptable_lift (cur_thread s) s va = Some (addrFromPPtr p); AllowWrite \<in> ptable_rights (cur_thread s) s va; device_state (machine_state s) p = None; x2 \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> ptable_lift (?t117 s a aa ab b m p x2 va) s (?x117 s a aa ab b m p x2 va) = Some (addrFromPPtr (?y117 s a aa ab b m p x2 va))
 3. \<And>s a aa ab b m p x2 va. \<lbrakk>(a, aa, ab, b) \<in> fst (f (cur_thread s) (\<lambda>x. if ptable_rights (cur_thread s) s x \<noteq> {} then ptable_lift (cur_thread s) s x else None) (ptable_rights (cur_thread s) s) (tc, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then device_state (machine_state s) (ptrFromPAddr x) else None)); valid_state s; tcb_at (cur_thread s) s; ct_running s; ab (addrFromPPtr p) = Some x2; ptable_lift (cur_thread s) s va = Some (addrFromPPtr p); AllowWrite \<in> ptable_rights (cur_thread s) s va; device_state (machine_state s) p = None; x2 \<noteq> underlying_memory m p; in_user_frame (?y117 s a aa ab b m p x2 va) s \<or> in_device_frame (?y117 s a aa ab b m p x2 va) s\<rbrakk> \<Longrightarrow> in_user_frame p s proof (prove)
goal (1 subgoal):
 1. \<And>s a aa ab b m p x2 va. \<lbrakk>(a, aa, ab, b) \<in> fst (f (cur_thread s) (\<lambda>x. if ptable_rights (cur_thread s) s x \<noteq> {} then ptable_lift (cur_thread s) s x else None) (ptable_rights (cur_thread s) s) (tc, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then user_mem s (ptrFromPAddr x) else None, \<lambda>x. if \<exists>va. ptable_lift (cur_thread s) s va = Some x \<and> AllowRead \<in> ptable_rights (cur_thread s) s va then device_state (machine_state s) (ptrFromPAddr x) else None)); valid_state s; tcb_at (cur_thread s) s; ct_running s; ab (addrFromPPtr p) = Some x2; ptable_lift (cur_thread s) s va = Some (addrFromPPtr p); AllowWrite \<in> ptable_rights (cur_thread s) s va; device_state (machine_state s) p = None; x2 \<noteq> underlying_memory m p; in_user_frame p s \<or> in_device_frame p s\<rbrakk> \<Longrightarrow> in_user_frame p s proof (prove)
goal:
No subgoals!