theory ArchADT_IF_Refine

lemma doUserOp_if_no_interrupt[ADT_IF_Refine_assms]:
  "\<lbrace>K (uop_sane uop)\<rbrace>
   doUserOp_if uop tc
   \<lbrace>\<lambda>r s. (fst r) \<noteq> Some Interrupt\<rbrace>" apply (simp add: doUserOp_if_def del: split_paired_All) apply (wp | wpc)+ apply (clarsimp simp: uop_sane_def simp del: split_paired_All) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (uop_sane uop)\<rbrace> doUserOp_if uop tc \<lbrace>\<lambda>r s. fst r \<noteq> Some Interrupt\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>y. uop_sane uop\<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 (uop 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> {});
(e, tc', um', ds', es') <- select (uop 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 ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- doMachineOp (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- doMachineOp (setExMonitor es');
return (e, tc')
od \<lbrace>\<lambda>r s. fst r \<noteq> Some Interrupt\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. uop_sane uop \<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> uop (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>uop (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)). \<forall>xa xb. x = (xa, xb) \<longrightarrow> (\<forall>x xc. xb = (x, xc) \<longrightarrow> (\<forall>xb xd. xc = (xb, xd) \<longrightarrow> (\<forall>xb xc. xd = (xb, xc) \<longrightarrow> fst (xa, x) \<noteq> Some Interrupt)))) proof (prove)
goal:
No subgoals!