diff options
| -rw-r--r-- | lib/isabelle/State_lemmas.thy | 8 | ||||
| -rw-r--r-- | lib/isabelle/State_monad_lemmas.thy | 200 | ||||
| -rw-r--r-- | src/gen_lib/state_monad.lem | 32 |
3 files changed, 195 insertions, 45 deletions
diff --git a/lib/isabelle/State_lemmas.thy b/lib/isabelle/State_lemmas.thy index 9c5dd8af..d8ab5db9 100644 --- a/lib/isabelle/State_lemmas.thy +++ b/lib/isabelle/State_lemmas.thy @@ -13,7 +13,7 @@ lemma liftState_bind[simp]: lemma liftState_return[simp]: "liftState r (return a) = returnS a" by (auto simp: return_def) lemma Value_liftState_Run: - assumes "(Value a, s') \<in> set (liftState r m s)" + assumes "(Value a, s') \<in> liftState r m s" obtains t where "Run m t a" by (use assms in \<open>induction r m arbitrary: s s' rule: liftState.induct\<close>; auto simp add: failS_def throwS_def returnS_def simp del: read_regvalS.simps; @@ -101,8 +101,8 @@ lemma liftState_foreachM[simp]: lemma whileS_dom_step: assumes "whileS_dom (vars, cond, body, s)" - and "(Value True, s') \<in> set (cond vars s)" - and "(Value vars', s'') \<in> set (body vars s')" + and "(Value True, s') \<in> cond vars s" + and "(Value vars', s'') \<in> body vars s'" shows "whileS_dom (vars', cond, body, s'')" by (use assms in \<open>induction vars cond body s arbitrary: vars' s' s'' rule: whileS.pinduct\<close>) (auto intro: whileS.domintros) @@ -143,7 +143,7 @@ proof (use assms in \<open>induction vars "liftState r \<circ> cond" "liftState show "\<exists>t. Run (cond vars) t True" using while that by (auto elim: Value_liftState_Run) show "\<exists>t'. Run (body vars) t' vars'" using while' that by (auto elim: Value_liftState_Run) qed - then show ?case using while while' that by (auto intro: IH) + then show ?case using while while' that IH by auto qed auto then show ?case by auto qed auto diff --git a/lib/isabelle/State_monad_lemmas.thy b/lib/isabelle/State_monad_lemmas.thy index d8730421..746fd315 100644 --- a/lib/isabelle/State_monad_lemmas.thy +++ b/lib/isabelle/State_monad_lemmas.thy @@ -8,34 +8,36 @@ context notes returnS_def[simp] and failS_def[simp] and throwS_def[simp] and readS_def[simp] and updateS_def[simp] begin -abbreviation "bindS_aux f \<equiv> (\<lambda>r. case r of (Value a, s') \<Rightarrow> f a s' | (Ex e, s') \<Rightarrow> [(Ex e, s')])" -abbreviation "bindS_app ms f \<equiv> List.concat (List.map (bindS_aux f) ms)" +abbreviation "bindS_aux f \<equiv> (\<lambda>r. case r of (Value a, s') \<Rightarrow> f a s' | (Ex e, s') \<Rightarrow> {(Ex e, s')})" +abbreviation "bindS_app ms f \<equiv> \<Union>(bindS_aux f ` ms)" lemma bindS_ext_cong[fundef_cong]: assumes m: "m1 s = m2 s" - and f: "\<And>a s'. (Value a, s') \<in> set (m2 s) \<Longrightarrow> f1 a s' = f2 a s'" + and f: "\<And>a s'. (Value a, s') \<in> (m2 s) \<Longrightarrow> f1 a s' = f2 a s'" shows "bindS m1 f1 s = bindS m2 f2 s" -proof - + using assms unfolding bindS_def by (auto split: result.splits) +(* proof - have "bindS_app (m2 s) f1 = bindS_app (m2 s) f2" - using f by (intro arg_cong[where f = List.concat]) (auto intro: map_ext split: result.splits) + using f by (auto split: result.splits) then show ?thesis using m by (auto simp: bindS_def) -qed +qed *) lemma bindS_cong[fundef_cong]: assumes m: "m1 = m2" - and f: "\<And>s a s'. (Value a, s') \<in> set (m2 s) \<Longrightarrow> f1 a s' = f2 a s'" + and f: "\<And>s a s'. (Value a, s') \<in> (m2 s) \<Longrightarrow> f1 a s' = f2 a s'" shows "bindS m1 f1 = bindS m2 f2" - using assms by (blast intro: bindS_ext_cong) + using assms by (intro ext bindS_ext_cong; blast) lemma bindS_returnS_left[simp]: "bindS (returnS x) f = f x" by (auto simp add: bindS_def) lemma bindS_returnS_right[simp]: "bindS m returnS = (m :: ('regs, 'a, 'e) monadS)" -proof - + by (intro ext) (auto simp: bindS_def split: result.splits) +(* proof - have "List.concat (map (bindS_aux returnS) ms) = ms" for ms :: "(('a, 'e) result \<times> 'regs sequential_state) list" by (induction ms) (auto split: result.splits) then show ?thesis unfolding bindS_def by blast -qed +qed *) lemma bindS_readS: "bindS (readS f) m = (\<lambda>s. m (f s) s)" by (auto simp: bindS_def) @@ -43,30 +45,100 @@ lemma bindS_readS: "bindS (readS f) m = (\<lambda>s. m (f s) s)" lemma bindS_updateS: "bindS (updateS f) m = (\<lambda>s. m () (f s))" by (auto simp: bindS_def) -lemma bindS_assoc[simp]: "bindS (bindS m f) g = bindS m (\<lambda>x. bindS (f x) g)" + +lemma result_cases: + fixes r :: "('a, 'e) result" + obtains (Value) a where "r = Value a" + | (Throw) e where "r = Ex (Throw e)" + | (Failure) msg where "r = Ex (Failure msg)" +proof (cases r) + case (Ex ex) then show ?thesis by (cases ex; auto intro: that) +qed + +lemma result_state_cases: + fixes rs :: "('a, 'e) result \<times> 's" + obtains (Value) a s where "rs = (Value a, s)" + | (Throw) e s where "rs = (Ex (Throw e), s)" + | (Failure) msg s where "rs = (Ex (Failure msg), s)" proof - + obtain r s where rs: "rs = (r, s)" by (cases rs) + then show thesis by (cases r rule: result_cases) (auto intro: that) +qed + +lemma monadS_ext_eqI: + fixes m m' :: "('regs, 'a, 'e) monadS" + assumes "\<And>a s'. (Value a, s') \<in> m s \<longleftrightarrow> (Value a, s') \<in> m' s" + and "\<And>e s'. (Ex (Throw e), s') \<in> m s \<longleftrightarrow> (Ex (Throw e), s') \<in> m' s" + and "\<And>msg s'. (Ex (Failure msg), s') \<in> m s \<longleftrightarrow> (Ex (Failure msg), s') \<in> m' s" + shows "m s = m' s" +proof (intro set_eqI) + fix x + show "x \<in> m s \<longleftrightarrow> x \<in> m' s" using assms by (cases x rule: result_state_cases) auto +qed + +lemma monadS_eqI: + fixes m m' :: "('regs, 'a, 'e) monadS" + assumes "\<And>s a s'. (Value a, s') \<in> m s \<longleftrightarrow> (Value a, s') \<in> m' s" + and "\<And>s e s'. (Ex (Throw e), s') \<in> m s \<longleftrightarrow> (Ex (Throw e), s') \<in> m' s" + and "\<And>s msg s'. (Ex (Failure msg), s') \<in> m s \<longleftrightarrow> (Ex (Failure msg), s') \<in> m' s" + shows "m = m'" + using assms by (intro ext monadS_ext_eqI) + +lemma + assumes "(Value a, s') \<in> bindS m f s" + obtains a' s'' where "(Value a', s'') \<in> m s" and "(Value a, s') \<in> f a' s''" + using assms by (auto simp: bindS_def split: result.splits) + +lemma + assumes "(Ex e, s') \<in> bindS m f s" + obtains (Left) "(Ex e, s') \<in> m s" + | (Right) a s'' where "(Value a, s'') \<in> m s" and "(Ex e, s') \<in> f a s''" + using assms by (auto simp: bindS_def split: result.splits) + +lemma bindS_cases: + assumes "(r, s') \<in> bindS m f s" + obtains (Value) a a' s'' where "r = Value a" and "(Value a', s'') \<in> m s" and "(Value a, s') \<in> f a' s''" + | (Ex_Left) e where "r = Ex e" and "(Ex e, s') \<in> m s" + | (Ex_Right) e a s'' where "r = Ex e" and "(Value a, s'') \<in> m s" and "(Ex e, s') \<in> f a s''" + using assms by (cases r; auto simp: bindS_def split: result.splits) + +lemma bindS_intros: + "\<And>m f s a s' a' s''. (Value a', s'') \<in> m s \<Longrightarrow> (Value a, s') \<in> f a' s'' \<Longrightarrow> (Value a, s') \<in> bindS m f s" + "\<And>m f s e s'. (Ex e, s') \<in> m s \<Longrightarrow> (Ex e, s') \<in> bindS m f s" + "\<And>m f s e s' a s''. (Ex e, s') \<in> f a s'' \<Longrightarrow> (Value a, s'') \<in> m s \<Longrightarrow> (Ex e, s') \<in> bindS m f s" + by (auto simp: bindS_def intro: bexI[rotated]) + +lemma bindS_assoc[simp]: "bindS (bindS m f) g = bindS m (\<lambda>x. bindS (f x) g)" + by (auto elim!: bindS_cases intro: bindS_intros monadS_eqI) +(*proof - have "List.concat (map (bindS_aux g) (List.concat (map (bindS_aux f) xs))) = List.concat (map (bindS_aux (\<lambda>x s. List.concat (map (bindS_aux g) (f x s)))) xs)" for xs by (induction xs) (auto split: result.splits) then show ?thesis unfolding bindS_def by auto -qed +qed*) lemma bindS_failS[simp]: "bindS (failS msg) f = failS msg" by (auto simp: bindS_def) lemma bindS_throwS[simp]: "bindS (throwS e) f = throwS e" by (auto simp: bindS_def) declare seqS_def[simp] lemma Value_bindS_elim: - assumes "(Value a, s') \<in> set (bindS m f s)" - obtains s'' a' where "(Value a', s'') \<in> set (m s)" and "(Value a, s') \<in> set (f a' s'')" - using assms by (auto simp: bindS_def; split result.splits; auto) + assumes "(Value a, s') \<in> bindS m f s" + obtains s'' a' where "(Value a', s'') \<in> m s" and "(Value a, s') \<in> f a' s''" + using assms by (auto elim: bindS_cases) + +lemma Ex_bindS_elim: + assumes "(Ex e, s') \<in> bindS m f s" + obtains (Left) "(Ex e, s') \<in> m s" + | (Right) s'' a' where "(Value a', s'') \<in> m s" and "(Ex e, s') \<in> f a' s''" + using assms by (auto elim: bindS_cases) abbreviation "try_catchS_aux h r \<equiv> (case r of (Value a, s') => returnS a s' | (Ex (Throw e), s') => h e s' - | (Ex (Failure msg), s') => [(Ex (Failure msg), s')])" -abbreviation "try_catchS_app ms h \<equiv> List.concat (List.map (try_catchS_aux h) ms)" + | (Ex (Failure msg), s') => {(Ex (Failure msg), s')})" +abbreviation "try_catchS_app ms h \<equiv> \<Union>(try_catchS_aux h ` ms)" lemma try_catchS_returnS[simp]: "try_catchS (returnS a) h = returnS a" and try_catchS_failS[simp]: "try_catchS (failS msg) h = failS msg" @@ -78,6 +150,31 @@ lemma try_catchS_cong[cong]: shows "try_catchS m1 h1 = try_catchS m2 h2" using assms by (intro arg_cong2[where f = try_catchS] ext) auto +lemma try_catchS_cases: + assumes "(r, s') \<in> try_catchS m h s" + obtains (Value) a where "r = Value a" and "(Value a, s') \<in> m s" + | (Fail) msg where "r = Ex (Failure msg)" and "(Ex (Failure msg), s') \<in> m s" + | (h) e s'' where "(Ex (Throw e), s'') \<in> m s" and "(r, s') \<in> h e s''" + using assms by (cases r rule: result_cases) (auto simp: try_catchS_def split: result.splits ex.splits) + +lemma try_catchS_intros: + "\<And>m h s a s'. (Value a, s') \<in> m s \<Longrightarrow> (Value a, s') \<in> try_catchS m h s" + "\<And>m h s msg s'. (Ex (Failure msg), s') \<in> m s \<Longrightarrow> (Ex (Failure msg), s') \<in> try_catchS m h s" + "\<And>m h s e s'' r s'. (Ex (Throw e), s'') \<in> m s \<Longrightarrow> (r, s') \<in> h e s'' \<Longrightarrow> (r, s') \<in> try_catchS m h s" + by (auto simp: try_catchS_def intro: bexI[rotated]) + +fun ignore_throw_aux :: "(('a, 'e1) result \<times> 's) \<Rightarrow> (('a, 'e2) result \<times> 's) set" where + "ignore_throw_aux (Value a, s') = {(Value a, s')}" +| "ignore_throw_aux (Ex (Throw e), s') = {}" +| "ignore_throw_aux (Ex (Failure msg), s') = {(Ex (Failure msg), s')}" +definition "ignore_throw m s \<equiv> \<Union>(ignore_throw_aux ` m s)" + +(*fun ignore_throw_aux :: "(('a, 'e1) result \<times> 's) \<Rightarrow> (('a, 'e2) result \<times> 's) list" where + "ignore_throw_aux r \<equiv> + (case r of + (Value a, s') => returnS a s' + | (Ex (Throw e), s') => h e s' + | (Ex (Failure msg), s') => {(Ex (Failure msg), s')})" fun ignore_throw_app :: "(('a, 'e1) result \<times> 's) list \<Rightarrow> (('a, 'e2) result \<times> 's) list" where "ignore_throw_app [] = []" | "ignore_throw_app ((Value a, s) # ms) = (Value a, s) # ignore_throw_app ms" @@ -95,12 +192,31 @@ lemma ignore_throw_app_append[simp]: lemma ignore_throw_app_bindS_app[simp]: "ignore_throw_app (bindS_app ms f) = bindS_app (ignore_throw_app ms) (ignore_throw \<circ> f)" - by (induction ms rule: ignore_throw_app.induct) (auto split: result.splits) + by (induction ms rule: ignore_throw_app.induct) (auto split: result.splits)*) + +lemma [simp]: + "(Value a, s') \<in> ignore_throw_aux ms \<longleftrightarrow> ms = (Value a, s')" + "(Ex (Throw e), s') \<in> ignore_throw_aux ms \<longleftrightarrow> False" + "(Ex (Failure msg), s') \<in> ignore_throw_aux ms \<longleftrightarrow> ms = (Ex (Failure msg), s')" + by (cases ms rule: result_state_cases; auto)+ + +(*lemma [simp]: "(Value a, s') \<in> ignore_throw m s \<longleftrightarrow> (Value a, s') \<in> m s" + "(Value a, s') \<in> ignore_throw m s \<longleftrightarrow> (Value a, s') \<in> m s" + "(Ex (Throw e), s') \<in> ignore_throw m s \<longleftrightarrow> False" + "(Ex (Failure msg), s') \<in> ignore_throw_aux ms \<longleftrightarrow> ms = (Ex (Failure msg), s')" + by (auto simp: ignore_throw_def)*) + +lemma ignore_throw_cases: + assumes no_throw: "ignore_throw m s = m s" + and r: "(r, s') \<in> m s" + obtains (Value) a where "r = Value a" + | (Failure) msg where "r = Ex (Failure msg)" + using r unfolding no_throw[symmetric] + by (cases r rule: result_cases) (auto simp: ignore_throw_def) lemma ignore_throw_bindS[simp]: "ignore_throw (bindS m f) = bindS (ignore_throw m) (ignore_throw \<circ> f)" - "ignore_throw (bindS m f) s = bindS (ignore_throw m) (ignore_throw \<circ> f) s" - unfolding bindS_def by auto + by (intro monadS_eqI) (auto simp: ignore_throw_def elim!: bindS_cases intro: bindS_intros) lemma try_catchS_bindS_no_throw: fixes m1 :: "('r, 'a, 'e1) monadS" and m2 :: "('r, 'a, 'e2) monadS" @@ -109,13 +225,47 @@ lemma try_catchS_bindS_no_throw: shows "try_catchS (bindS m1 f) h = bindS m2 (\<lambda>a. try_catchS (f a) h)" proof fix s + have "try_catchS (bindS m1 f) h s = bindS (ignore_throw m1) (\<lambda>a. try_catchS (f a) h) s" + by (intro monadS_ext_eqI; + auto elim!: bindS_cases try_catchS_cases elim: ignore_throw_cases[OF m1]; + auto simp: ignore_throw_def intro: bindS_intros try_catchS_intros) + also have "\<dots> = bindS m2 (\<lambda>a. try_catchS (f a) h) s" using m2 by (intro bindS_ext_cong) auto + finally show "try_catchS (bindS m1 f) h s = bindS m2 (\<lambda>a. try_catchS (f a) h) s" . +qed +(*proof + fix s have 1: "try_catchS_app (bindS_app ms f) h = bindS_app (ignore_throw_app ms) (\<lambda>a s'. try_catchS_app (f a s') h)" if "ignore_throw_app ms = ms" for ms using that by (induction ms rule: ignore_throw_app.induct) auto then show "try_catchS (bindS m1 f) h s = bindS m2 (\<lambda>a. try_catchS (f a) h) s" using m1 unfolding try_catchS_def bindS_def m2[symmetric] by blast -qed +qed*) + +(*lemma no_throwI: + fixes m1 :: "('regs, 'a, 'e1) monadS" and m2 :: "('regs, 'a, 'e2) monadS" + assumes "\<And>a s'. (Value a, s') \<in> m1 s \<longleftrightarrow> (Value a, s') \<in> m2 s" + and "\<And>msg s'. (Ex (Failure msg), s') \<in> m1 s \<longleftrightarrow> (Ex (Failure msg), s') \<in> m2 s" + and "\<And>e s'. (Ex (Throw e), s') \<notin> m1 s" + and "\<And>e s'. (Ex (Throw e), s') \<notin> m2 s" + shows "ignore_throw m1 s = m2 s" + using assms by (intro monadS_ext_eqI) (auto simp: ignore_throw_def)*) + +(*lemma no_throw_bindSI: + assumes "ignore_throw m1 s = m2 s" +and "\<And>a s'. (Value a, s') \<in> m2 s \<Longrightarrow> ignore_throw (f1 a) s' = f2 a s'" +shows "ignore_throw (bindS m1 f1) s = bindS m2 f2 s" + using assms unfolding ignore_throw_bindS apply (intro monadS_ext_eqI) apply auto apply (auto elim!: bindS_cases intro: bindS_intros) + defer thm bindS_intros + apply (intro bindS_intros(3)) apply auto + apply (intro bindS_intros(3)) apply auto + done + +lemma + "\<And>BC rk a sz s. ignore_throw (read_mem_bytesS BC rk a sz) s = read_mem_bytesS BC rk a sz s" + unfolding read_mem_bytesS_def Let_def seqS_def + apply (intro no_throw_bindSI) + oops*) lemma no_throw_mem_builtins: "\<And>a. ignore_throw (returnS a) = returnS a" @@ -130,16 +280,16 @@ lemma no_throw_mem_builtins: unfolding read_mem_bytesS_def read_memS_def read_tagS_def write_mem_eaS_def unfolding write_mem_valS_def write_mem_bytesS_def write_tagS_def unfolding excl_resultS_def undefined_boolS_def - by (auto simp: bindS_def chooseS_def Let_def split: option.splits prod.splits)+ + by (auto simp: ignore_throw_def bindS_def chooseS_def Let_def split: option.splits prod.splits) lemma no_throw_read_memS: "ignore_throw (read_memS BCa BCb rk a sz) s = read_memS BCa BCb rk a sz s" - by (auto simp: read_memS_def no_throw_mem_builtins cong: bindS_cong) + by (auto simp: read_memS_def no_throw_mem_builtins cong: bindS_ext_cong) lemma no_throw_read_regvalS: "ignore_throw (read_regvalS r reg_name) s = read_regvalS r reg_name s" - by (cases r) (auto simp: bindS_def split: option.splits) + by (cases r) (auto simp: ignore_throw_def bindS_def split: option.splits) lemma no_throw_write_regvalS: "ignore_throw (write_regvalS r reg_name v) s = write_regvalS r reg_name v s" - by (cases r) (auto simp: bindS_def split: option.splits) + by (cases r) (auto simp: ignore_throw_def bindS_def split: option.splits) lemmas no_throw_builtins[simp, intro] = no_throw_mem_builtins no_throw_read_regvalS no_throw_write_regvalS no_throw_read_memS diff --git a/src/gen_lib/state_monad.lem b/src/gen_lib/state_monad.lem index 26179244..26f912fd 100644 --- a/src/gen_lib/state_monad.lem +++ b/src/gen_lib/state_monad.lem @@ -38,17 +38,17 @@ type result 'a 'e = (* State, nondeterminism and exception monad with result value type 'a and exception type 'e. *) -type monadS 'regs 'a 'e = sequential_state 'regs -> list (result 'a 'e * sequential_state 'regs) +type monadS 'regs 'a 'e = sequential_state 'regs -> set (result 'a 'e * sequential_state 'regs) val returnS : forall 'regs 'a 'e. 'a -> monadS 'regs 'a 'e -let returnS a s = [(Value a,s)] +let returnS a s = {(Value a,s)} val bindS : forall 'regs 'a 'b 'e. monadS 'regs 'a 'e -> ('a -> monadS 'regs 'b 'e) -> monadS 'regs 'b 'e let bindS m f (s : sequential_state 'regs) = - List.concatMap (function - | (Value a, s') -> f a s' - | (Ex e, s') -> [(Ex e, s')] - end) (m s) + Set.bigunion (Set.map (function + | (Value a, s') -> f a s' + | (Ex e, s') -> {(Ex e, s')} + end) (m s)) val seqS: forall 'regs 'b 'e. monadS 'regs unit 'e -> monadS 'regs 'b 'e -> monadS 'regs 'b 'e let seqS m n = bindS m (fun (_ : unit) -> n) @@ -56,8 +56,8 @@ let seqS m n = bindS m (fun (_ : unit) -> n) let inline (>>$=) = bindS let inline (>>$) = seqS -val chooseS : forall 'regs 'a 'e. list 'a -> monadS 'regs 'a 'e -let chooseS xs s = List.map (fun x -> (Value x, s)) xs +val chooseS : forall 'regs 'a 'e. SetType 'a => set 'a -> monadS 'regs 'a 'e +let chooseS xs s = Set.map (fun x -> (Value x, s)) xs val readS : forall 'regs 'a 'e. (sequential_state 'regs -> 'a) -> monadS 'regs 'a 'e let readS f = (fun s -> returnS (f s) s) @@ -66,7 +66,7 @@ val updateS : forall 'regs 'e. (sequential_state 'regs -> sequential_state 'regs let updateS f = (fun s -> returnS () (f s)) val failS : forall 'regs 'a 'e. string -> monadS 'regs 'a 'e -let failS msg s = [(Ex (Failure msg), s)] +let failS msg s = {(Ex (Failure msg), s)} val undefined_boolS : forall 'regval 'regs 'a 'e. unit -> monadS 'regs bool 'e let undefined_boolS () = @@ -78,15 +78,15 @@ val exitS : forall 'regs 'e 'a. unit -> monadS 'regs 'a 'e let exitS () = failS "exit" val throwS : forall 'regs 'a 'e. 'e -> monadS 'regs 'a 'e -let throwS e s = [(Ex (Throw e), s)] +let throwS e s = {(Ex (Throw e), s)} val try_catchS : forall 'regs 'a 'e1 'e2. monadS 'regs 'a 'e1 -> ('e1 -> monadS 'regs 'a 'e2) -> monadS 'regs 'a 'e2 let try_catchS m h s = - List.concatMap (function - | (Value a, s') -> returnS a s' - | (Ex (Throw e), s') -> h e s' - | (Ex (Failure msg), s') -> [(Ex (Failure msg), s')] - end) (m s) + Set.bigunion (Set.map (function + | (Value a, s') -> returnS a s' + | (Ex (Throw e), s') -> h e s' + | (Ex (Failure msg), s') -> {(Ex (Failure msg), s')} + end) (m s)) val assert_expS : forall 'regs 'e. bool -> string -> monadS 'regs unit 'e let assert_expS exp msg = if exp then returnS () else failS msg @@ -150,7 +150,7 @@ val excl_resultS : forall 'regs 'e. unit -> monadS 'regs bool 'e let excl_resultS () = readS (fun s -> s.last_exclusive_operation_was_load) >>$= (fun excl_load -> updateS (fun s -> <| s with last_exclusive_operation_was_load = false |>) >>$ - chooseS (if excl_load then [false; true] else [false])) + chooseS (if excl_load then {false; true} else {false})) val write_mem_eaS : forall 'regs 'e 'a. Bitvector 'a => write_kind -> 'a -> nat -> monadS 'regs unit 'e let write_mem_eaS write_kind addr sz = |