diff options
| -rw-r--r-- | lib/isabelle/Sail2_prompt_monad_lemmas.thy | 6 | ||||
| -rw-r--r-- | lib/isabelle/Sail2_state_lemmas.thy | 27 | ||||
| -rw-r--r-- | lib/isabelle/Sail2_state_monad_lemmas.thy | 14 | ||||
| -rw-r--r-- | src/gen_lib/sail2_prompt_monad.lem | 82 | ||||
| -rw-r--r-- | src/gen_lib/sail2_state_lifting.lem | 36 | ||||
| -rw-r--r-- | src/gen_lib/sail2_state_monad.lem | 20 |
6 files changed, 113 insertions, 72 deletions
diff --git a/lib/isabelle/Sail2_prompt_monad_lemmas.thy b/lib/isabelle/Sail2_prompt_monad_lemmas.thy index 406b5871..c59fc62f 100644 --- a/lib/isabelle/Sail2_prompt_monad_lemmas.thy +++ b/lib/isabelle/Sail2_prompt_monad_lemmas.thy @@ -32,6 +32,7 @@ lemmas try_catch_induct[case_names Done Read_mem Write_memv Read_reg Excl_res Wr inductive_set T :: "(('rv, 'a, 'e) monad \<times> 'rv event \<times> ('rv, 'a, 'e) monad) set" where Read_mem: "((Read_mem rk addr sz k), E_read_mem rk addr sz v, k v) \<in> T" +| Read_tagged_mem: "((Read_tagged_mem rk addr sz k), E_read_tagged_mem rk addr sz v, k v) \<in> T" | Write_ea: "((Write_ea wk addr sz k), E_write_ea wk addr sz, k) \<in> T" | Excl_res: "((Excl_res k), E_excl_res r, k r) \<in> T" | Write_mem: "((Write_mem wk addr sz v t k), E_write_mem wk addr sz v t r, k r) \<in> T" @@ -60,7 +61,8 @@ lemma Traces_cases: fixes m :: "('rv, 'a, 'e) monad" assumes Run: "(m, t, m') \<in> Traces" obtains (Nil) a where "m = m'" and "t = []" - | (Read_mem) rk addr s k t' v tag where "m = Read_mem rk addr s k" and "t = E_read_mem rk addr s (v, tag) # t'" and "(k (v, tag), t', m') \<in> Traces" + | (Read_mem) rk addr s k t' v where "m = Read_mem rk addr s k" and "t = E_read_mem rk addr s v # t'" and "(k v, t', m') \<in> Traces" + | (Read_tagged_mem) rk addr s k t' v tag where "m = Read_tagged_mem rk addr s k" and "t = E_read_tagged_mem rk addr s (v, tag) # t'" and "(k (v, tag), t', m') \<in> Traces" | (Write_mem) wk addr sz val tag k t' v where "m = Write_mem wk addr sz val tag k" and "t = E_write_mem wk addr sz val tag v # t'" and "(k v, t', m') \<in> Traces" | (Barrier) bk k t' v where "m = Barrier bk k" and "t = E_barrier bk # t'" and "(k, t', m') \<in> Traces" | (Read_reg) reg k t' v where "m = Read_reg reg k" and "t = E_read_reg reg v # t'" and "(k v, t', m') \<in> Traces" @@ -79,7 +81,7 @@ next note m' = \<open>(m'', t', m') \<in> Traces\<close> from \<open>(m, e, m'') \<in> T\<close> and t and m' show ?thesis proof (cases m e m'' rule: T.cases) - case (Read_mem rk addr sz k v) + case (Read_tagged_mem rk addr sz k v) then show ?thesis using t m' by (cases v; elim that; blast) qed (elim that; blast)+ qed diff --git a/lib/isabelle/Sail2_state_lemmas.thy b/lib/isabelle/Sail2_state_lemmas.thy index c7d55d31..77f4ac5a 100644 --- a/lib/isabelle/Sail2_state_lemmas.thy +++ b/lib/isabelle/Sail2_state_lemmas.thy @@ -80,19 +80,20 @@ lemma liftState_bool_of_bitU_nondet[liftState_simp]: "liftState r (bool_of_bitU_nondet b) = bool_of_bitU_nondetS b" by (cases b; auto simp: bool_of_bitU_nondet_def bool_of_bitU_nondetS_def liftState_simp) -lemma liftState_read_mem_BC: - assumes "unsigned_method BC_bitU_list (bits_of_method BCa a) = unsigned_method BCa a" - shows "liftState r (read_mem BCa BCb rk a sz) = read_memS BCa BCb rk a sz" - using assms - by (auto simp: read_mem_def read_mem_bytes_def read_memS_def read_mem_bytesS_def maybe_failS_def +lemma liftState_read_tagged_mem[liftState_simp]: + shows "liftState r (read_tagged_mem BCa BCb rk a sz) = read_tagged_memS BCa BCb rk a sz" + by (auto simp: read_tagged_mem_def read_tagged_mem_bytes_def maybe_failS_def read_tagged_memS_def prod.case_distrib option.case_distrib[where h = "liftState r"] option.case_distrib[where h = "\<lambda>c. c \<bind>\<^sub>S f" for f] liftState_simp - cong: option.case_cong) + split: option.splits intro: bindS_cong) lemma liftState_read_mem[liftState_simp]: - "\<And>a. liftState r (read_mem BC_mword BC_mword rk a sz) = read_memS BC_mword BC_mword rk a sz" - "\<And>a. liftState r (read_mem BC_bitU_list BC_bitU_list rk a sz) = read_memS BC_bitU_list BC_bitU_list rk a sz" - by (auto simp: liftState_read_mem_BC) + shows "liftState r (read_mem BCa BCb rk a sz) = read_memS BCa BCb rk a sz" + by (auto simp: read_mem_def read_mem_bytes_def read_memS_def read_mem_bytesS_def maybe_failS_def + read_tagged_memS_def + prod.case_distrib option.case_distrib[where h = "liftState r"] + option.case_distrib[where h = "\<lambda>c. c \<bind>\<^sub>S f" for f] liftState_simp + split: option.splits intro: bindS_cong) lemma liftState_write_mem_ea_BC: assumes "unsigned_method BCa a = Some a'" @@ -399,7 +400,10 @@ text \<open>Event traces\<close> lemma Some_eq_bind_conv: "Some x = Option.bind f g \<longleftrightarrow> (\<exists>y. f = Some y \<and> g y = Some x)" unfolding bind_eq_Some_conv[symmetric] by auto -lemma if_then_Some_eq_Some: "((if b then Some x else None) = Some y) \<longleftrightarrow> (b \<and> y = x)" +lemma if_then_Some_eq_Some_iff: "((if b then Some x else None) = Some y) \<longleftrightarrow> (b \<and> y = x)" + by auto + +lemma Some_eq_if_then_Some_iff: "(Some y = (if b then Some x else None)) \<longleftrightarrow> (b \<and> y = x)" by auto lemma emitEventS_update_cases: @@ -413,7 +417,8 @@ lemma emitEventS_update_cases: and "s' = s\<lparr>regstate := rs'\<rparr>" | (Read) "s' = s" using assms - by (elim emitEventS.elims) (auto simp: Some_eq_bind_conv bind_eq_Some_conv if_then_Some_eq_Some) + by (elim emitEventS.elims) + (auto simp: Some_eq_bind_conv bind_eq_Some_conv if_then_Some_eq_Some_iff Some_eq_if_then_Some_iff) lemma runTraceS_singleton[simp]: "runTraceS ra [e] s = emitEventS ra e s" by (cases "emitEventS ra e s"; auto) diff --git a/lib/isabelle/Sail2_state_monad_lemmas.thy b/lib/isabelle/Sail2_state_monad_lemmas.thy index 6fb5e7ef..12452ca4 100644 --- a/lib/isabelle/Sail2_state_monad_lemmas.thy +++ b/lib/isabelle/Sail2_state_monad_lemmas.thy @@ -211,22 +211,22 @@ lemma ignore_throw_let_distrib: "ignore_throw (let x = y in f x) = (let x = y in by auto lemma no_throw_mem_builtins: - "\<And>BC rk a sz s. ignore_throw (read_mem_bytesS rk a sz) s = read_mem_bytesS rk a sz s" + "\<And>rk a sz s. ignore_throw (read_mem_bytesS rk a sz) s = read_mem_bytesS rk a sz s" + "\<And>rk a sz s. ignore_throw (read_tagged_mem_bytesS rk a sz) s = read_tagged_mem_bytesS rk a sz s" "\<And>BC a s. ignore_throw (read_tagS BC a) s = read_tagS BC a s" + "\<And>BCa BCv rk a sz s. ignore_throw (read_memS BCa BCv rk a sz) s = read_memS BCa BCv rk a sz s" + "\<And>BCa BCv rk a sz s. ignore_throw (read_tagged_memS BCa BCv rk a sz) s = read_tagged_memS BCa BCv rk a sz s" "\<And>BC wk addr sz v t s. ignore_throw (write_mem_bytesS wk addr sz v t) s = write_mem_bytesS wk addr sz v t s" - "\<And>BC_a BC_v wk addr sz v t s. ignore_throw (write_memS BC_a BC_v wk addr sz v t) s = write_memS BC_a BC_v wk addr sz v t s" + "\<And>BCa BCv wk addr sz v t s. ignore_throw (write_memS BCa BCv wk addr sz v t) s = write_memS BCa BCv wk addr sz v t s" "\<And>s. ignore_throw (excl_resultS ()) s = excl_resultS () s" "\<And>s. ignore_throw (undefined_boolS ()) s = undefined_boolS () s" - unfolding read_mem_bytesS_def read_memS_def read_tagS_def write_memS_def + unfolding read_mem_bytesS_def read_tagged_mem_bytesS_def read_tagged_memS_def read_memS_def read_tagS_def write_memS_def unfolding write_mem_bytesS_def unfolding excl_resultS_def undefined_boolS_def maybe_failS_def unfolding ignore_throw_bindS by (auto cong: bindS_cong bindS_ext_cong ignore_throw_cong option.case_cong simp: prod.case_distrib ignore_throw_option_case_distrib ignore_throw_let_distrib comp_def) -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 prod.case_distrib comp_def 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: option.case_distrib cong: bindS_cong option.case_cong) @@ -234,7 +234,7 @@ lemma no_throw_write_regvalS: "ignore_throw (write_regvalS r reg_name v) s = wri by (cases r) (auto simp: option.case_distrib cong: bindS_cong option.case_cong) lemmas no_throw_builtins[simp] = - no_throw_mem_builtins no_throw_read_regvalS no_throw_write_regvalS no_throw_read_memS + no_throw_mem_builtins no_throw_read_regvalS no_throw_write_regvalS (* end *) diff --git a/src/gen_lib/sail2_prompt_monad.lem b/src/gen_lib/sail2_prompt_monad.lem index 7503ca22..079375a3 100644 --- a/src/gen_lib/sail2_prompt_monad.lem +++ b/src/gen_lib/sail2_prompt_monad.lem @@ -9,9 +9,10 @@ type address = list bitU type monad 'regval 'a 'e = | Done of 'a (* Read a number of bytes from memory, returned in little endian order, - together with a tag. The first nat specifies the address, the second + with or without a tag. The first nat specifies the address, the second the number of bytes. *) - | Read_mem of read_kind * nat * nat * ((list memory_byte * bitU) -> monad 'regval 'a 'e) + | Read_mem of read_kind * nat * nat * (list memory_byte -> monad 'regval 'a 'e) + | Read_tagged_mem of read_kind * nat * nat * ((list memory_byte * bitU) -> monad 'regval 'a 'e) (* Tell the system a write is imminent, at the given address and with the given size. *) | Write_ea of write_kind * nat * nat * monad 'regval 'a 'e @@ -38,7 +39,8 @@ type monad 'regval 'a 'e = | Exception of 'e type event 'regval = - | E_read_mem of read_kind * nat * nat * (list memory_byte * bitU) + | E_read_mem of read_kind * nat * nat * list memory_byte + | E_read_tagged_mem of read_kind * nat * nat * (list memory_byte * bitU) | E_write_mem of write_kind * nat * nat * list memory_byte * bitU * bool | E_write_ea of write_kind * nat * nat | E_excl_res of bool @@ -57,18 +59,19 @@ let return a = Done a val bind : forall 'rv 'a 'b 'e. monad 'rv 'a 'e -> ('a -> monad 'rv 'b 'e) -> monad 'rv 'b 'e let rec bind m f = match m with | Done a -> f a - | Read_mem rk a sz k -> Read_mem rk a sz (fun v -> bind (k v) f) - | Write_mem wk a sz v t k -> Write_mem wk a sz v t (fun v -> bind (k v) f) - | Read_reg descr k -> Read_reg descr (fun v -> bind (k v) f) - | Excl_res k -> Excl_res (fun v -> bind (k v) f) - | Undefined k -> Undefined (fun v -> bind (k v) f) - | Write_ea wk a sz k -> Write_ea wk a sz (bind k f) - | Footprint k -> Footprint (bind k f) - | Barrier bk k -> Barrier bk (bind k f) - | Write_reg r v k -> Write_reg r v (bind k f) - | Print msg k -> Print msg (bind k f) - | Fail descr -> Fail descr - | Exception e -> Exception e + | Read_mem rk a sz k -> Read_mem rk a sz (fun v -> bind (k v) f) + | Read_tagged_mem rk a sz k -> Read_tagged_mem rk a sz (fun v -> bind (k v) f) + | Write_mem wk a sz v t k -> Write_mem wk a sz v t (fun v -> bind (k v) f) + | Read_reg descr k -> Read_reg descr (fun v -> bind (k v) f) + | Excl_res k -> Excl_res (fun v -> bind (k v) f) + | Undefined k -> Undefined (fun v -> bind (k v) f) + | Write_ea wk a sz k -> Write_ea wk a sz (bind k f) + | Footprint k -> Footprint (bind k f) + | Barrier bk k -> Barrier bk (bind k f) + | Write_reg r v k -> Write_reg r v (bind k f) + | Print msg k -> Print msg (bind k f) + | Fail descr -> Fail descr + | Exception e -> Exception e end val exit : forall 'rv 'a 'e. unit -> monad 'rv 'a 'e @@ -86,18 +89,19 @@ let throw e = Exception e val try_catch : forall 'rv 'a 'e1 'e2. monad 'rv 'a 'e1 -> ('e1 -> monad 'rv 'a 'e2) -> monad 'rv 'a 'e2 let rec try_catch m h = match m with | Done a -> Done a - | Read_mem rk a sz k -> Read_mem rk a sz (fun v -> try_catch (k v) h) - | Write_mem wk a sz v t k -> Write_mem wk a sz v t (fun v -> try_catch (k v) h) - | Read_reg descr k -> Read_reg descr (fun v -> try_catch (k v) h) - | Excl_res k -> Excl_res (fun v -> try_catch (k v) h) - | Undefined k -> Undefined (fun v -> try_catch (k v) h) - | Write_ea wk a sz k -> Write_ea wk a sz (try_catch k h) - | Footprint k -> Footprint (try_catch k h) - | Barrier bk k -> Barrier bk (try_catch k h) - | Write_reg r v k -> Write_reg r v (try_catch k h) - | Print msg k -> Print msg (try_catch k h) - | Fail descr -> Fail descr - | Exception e -> h e + | Read_mem rk a sz k -> Read_mem rk a sz (fun v -> try_catch (k v) h) + | Read_tagged_mem rk a sz k -> Read_tagged_mem rk a sz (fun v -> try_catch (k v) h) + | Write_mem wk a sz v t k -> Write_mem wk a sz v t (fun v -> try_catch (k v) h) + | Read_reg descr k -> Read_reg descr (fun v -> try_catch (k v) h) + | Excl_res k -> Excl_res (fun v -> try_catch (k v) h) + | Undefined k -> Undefined (fun v -> try_catch (k v) h) + | Write_ea wk a sz k -> Write_ea wk a sz (try_catch k h) + | Footprint k -> Footprint (try_catch k h) + | Barrier bk k -> Barrier bk (try_catch k h) + | Write_reg r v k -> Write_reg r v (try_catch k h) + | Print msg k -> Print msg (try_catch k h) + | Fail descr -> Fail descr + | Exception e -> h e end (* For early return, we abuse exceptions by throwing and catching @@ -135,19 +139,35 @@ let maybe_fail msg = function | Nothing -> Fail msg end -val read_mem_bytes : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv (list memory_byte * bitU) 'e +val read_tagged_mem_bytes : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv (list memory_byte * bitU) 'e +let read_tagged_mem_bytes rk addr sz = + bind + (maybe_fail "nat_of_bv" (nat_of_bv addr)) + (fun addr -> Read_tagged_mem rk addr (nat_of_int sz) return) + +val read_tagged_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv ('b * bitU) 'e +let read_tagged_mem rk addr sz = + bind + (read_tagged_mem_bytes rk addr sz) + (fun (bytes, tag) -> + match of_bits (bits_of_mem_bytes bytes) with + | Just v -> return (v, tag) + | Nothing -> Fail "bits_of_mem_bytes" + end) + +val read_mem_bytes : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv (list memory_byte) 'e let read_mem_bytes rk addr sz = bind (maybe_fail "nat_of_bv" (nat_of_bv addr)) (fun addr -> Read_mem rk addr (nat_of_int sz) return) -val read_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv ('b * bitU) 'e +val read_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv 'b 'e let read_mem rk addr sz = bind (read_mem_bytes rk addr sz) - (fun (bytes, tag) -> + (fun bytes -> match of_bits (bits_of_mem_bytes bytes) with - | Just v -> return (v, tag) + | Just v -> return v | Nothing -> Fail "bits_of_mem_bytes" end) diff --git a/src/gen_lib/sail2_state_lifting.lem b/src/gen_lib/sail2_state_lifting.lem index 0e7addbb..07a6215b 100644 --- a/src/gen_lib/sail2_state_lifting.lem +++ b/src/gen_lib/sail2_state_lifting.lem @@ -8,28 +8,32 @@ open import {isabelle} `Sail2_state_monad_lemmas` (* Lifting from prompt monad to state monad *) val liftState : forall 'regval 'regs 'a 'e. register_accessors 'regs 'regval -> monad 'regval 'a 'e -> monadS 'regs 'a 'e let rec liftState ra m = match m with - | (Done a) -> returnS a - | (Read_mem rk a sz k) -> bindS (read_mem_bytesS rk a sz) (fun v -> liftState ra (k v)) - | (Write_mem wk a sz v t k) -> bindS (write_mem_bytesS wk a sz v t) (fun v -> liftState ra (k v)) - | (Read_reg r k) -> bindS (read_regvalS ra r) (fun v -> liftState ra (k v)) - | (Excl_res k) -> bindS (excl_resultS ()) (fun v -> liftState ra (k v)) - | (Undefined k) -> bindS (undefined_boolS ()) (fun v -> liftState ra (k v)) - | (Write_reg r v k) -> seqS (write_regvalS ra r v) (liftState ra k) - | (Write_ea _ _ _ k) -> liftState ra k - | (Footprint k) -> liftState ra k - | (Barrier _ k) -> liftState ra k - | (Print _ k) -> liftState ra k (* TODO *) - | (Fail descr) -> failS descr - | (Exception e) -> throwS e + | (Done a) -> returnS a + | (Read_mem rk a sz k) -> bindS (read_mem_bytesS rk a sz) (fun v -> liftState ra (k v)) + | (Read_tagged_mem rk a sz k) -> bindS (read_tagged_mem_bytesS rk a sz) (fun v -> liftState ra (k v)) + | (Write_mem wk a sz v t k) -> bindS (write_mem_bytesS wk a sz v t) (fun v -> liftState ra (k v)) + | (Read_reg r k) -> bindS (read_regvalS ra r) (fun v -> liftState ra (k v)) + | (Excl_res k) -> bindS (excl_resultS ()) (fun v -> liftState ra (k v)) + | (Undefined k) -> bindS (undefined_boolS ()) (fun v -> liftState ra (k v)) + | (Write_reg r v k) -> seqS (write_regvalS ra r v) (liftState ra k) + | (Write_ea _ _ _ k) -> liftState ra k + | (Footprint k) -> liftState ra k + | (Barrier _ k) -> liftState ra k + | (Print _ k) -> liftState ra k (* TODO *) + | (Fail descr) -> failS descr + | (Exception e) -> throwS e end val emitEventS : forall 'regval 'regs 'a 'e. Eq 'regval => register_accessors 'regs 'regval -> event 'regval -> sequential_state 'regs -> maybe (sequential_state 'regs) let emitEventS ra e s = match e with - | E_read_mem _ addr sz (v, tag) -> + | E_read_mem _ addr sz v -> + Maybe.bind (get_mem_bytes addr sz s) (fun (v', _) -> + if v' = v then Just s else Nothing) + | E_read_tagged_mem _ addr sz (v, tag) -> Maybe.bind (get_mem_bytes addr sz s) (fun (v', tag') -> if v' = v && tag' = tag then Just s else Nothing) - | E_write_mem _ addr sz v tag _ -> - Just (put_mem_bytes addr sz v tag s) + | E_write_mem _ addr sz v tag success -> + if success then Just (put_mem_bytes addr sz v tag s) else Nothing | E_read_reg r v -> let (read_reg, _) = ra in Maybe.bind (read_reg r s.regstate) (fun v' -> diff --git a/src/gen_lib/sail2_state_monad.lem b/src/gen_lib/sail2_state_monad.lem index 6c1cd4bd..8626052f 100644 --- a/src/gen_lib/sail2_state_monad.lem +++ b/src/gen_lib/sail2_state_monad.lem @@ -129,18 +129,28 @@ let get_mem_bytes addr sz s = (fun mem_val -> (mem_val, List.foldl and_bit B1 (List.map (read_tag s) addrs))) (just_list (List.map (read_byte s) addrs)) -val read_mem_bytesS : forall 'regs 'e. read_kind -> nat -> nat -> monadS 'regs (list memory_byte * bitU) 'e -let read_mem_bytesS _ addr sz = +val read_tagged_mem_bytesS : forall 'regs 'e. read_kind -> nat -> nat -> monadS 'regs (list memory_byte * bitU) 'e +let read_tagged_mem_bytesS _ addr sz = readS (get_mem_bytes addr sz) >>$= maybe_failS "read_memS" -val read_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs ('b * bitU) 'e -let read_memS rk a sz = +val read_mem_bytesS : forall 'regs 'e. read_kind -> nat -> nat -> monadS 'regs (list memory_byte) 'e +let read_mem_bytesS rk addr sz = + read_tagged_mem_bytesS rk addr sz >>$= (fun (bytes, _) -> + returnS bytes) + +val read_tagged_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs ('b * bitU) 'e +let read_tagged_memS rk a sz = maybe_failS "nat_of_bv" (nat_of_bv a) >>$= (fun a -> - read_mem_bytesS rk a (nat_of_int sz) >>$= (fun (bytes, tag) -> + read_tagged_mem_bytesS rk a (nat_of_int sz) >>$= (fun (bytes, tag) -> maybe_failS "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes)) >>$= (fun mem_val -> returnS (mem_val, tag)))) +val read_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs 'b 'e +let read_memS rk a sz = + read_tagged_memS rk a sz >>$= (fun (bytes, _) -> + returnS bytes) + val excl_resultS : forall 'regs 'e. unit -> monadS 'regs bool 'e let excl_resultS = (* TODO: This used to be more deterministic, checking a flag in the state |