Simplify treating of undefined_bool in Lem library

Use nondeterministic choice by default instead of a deterministic bitstream
generator in the state, which is slightly awkward to reason about, because
every use of undefined_boolS changes the state.  The previous behaviour can be
implemented as Sail code, if desired.

Also add a default implementation of internal_pick that nondeterministically
chooses an element from a list.

6 files changed, 107 insertions, 94 deletions

diff --git a/src/gen_lib/sail2_operators_bitlists.lem b/src/gen_lib/sail2_operators_bitlists.lem
index 3f8b7510..0c833e90 100644
--- a/src/gen_lib/sail2_operators_bitlists.lem
+++ b/src/gen_lib/sail2_operators_bitlists.lem
@@ -10,16 +10,16 @@ open import Sail2_prompt
 val uint_maybe : list bitU -> maybe integer
 let uint_maybe v = unsigned v
 let uint_fail v = maybe_fail "uint" (unsigned v)
-let uint_oracle v =
-  bools_of_bits_oracle v >>= (fun bs ->
+let uint_nondet v =
+  bools_of_bits_nondet v >>= (fun bs ->
   return (int_of_bools false bs))
 let uint v = maybe_failwith (uint_maybe v)
 
 val sint_maybe : list bitU -> maybe integer
 let sint_maybe v = signed v
 let sint_fail v = maybe_fail "sint" (signed v)
-let sint_oracle v =
-  bools_of_bits_oracle v >>= (fun bs ->
+let sint_nondet v =
+  bools_of_bits_nondet v >>= (fun bs ->
   return (int_of_bools true bs))
 let sint v = maybe_failwith (sint_maybe v)
 
@@ -43,13 +43,13 @@ let vector_truncate bs len = extz_bv len bs
 
 val vec_of_bits_maybe    : list bitU -> maybe (list bitU)
 val vec_of_bits_fail     : forall 'rv 'e. list bitU -> monad 'rv (list bitU) 'e
-val vec_of_bits_oracle   : forall 'rv 'e. list bitU -> monad 'rv (list bitU) 'e
+val vec_of_bits_nondet   : forall 'rv 'e. list bitU -> monad 'rv (list bitU) 'e
 val vec_of_bits_failwith : list bitU -> list bitU
 val vec_of_bits          : list bitU -> list bitU
 let inline vec_of_bits bits = bits
 let inline vec_of_bits_maybe bits = Just bits
 let inline vec_of_bits_fail bits = return bits
-let inline vec_of_bits_oracle bits = return bits
+let inline vec_of_bits_nondet bits = return bits
 let inline vec_of_bits_failwith bits = bits
 
 val access_vec_inc : list bitU -> integer -> bitU
@@ -62,13 +62,13 @@ val update_vec_inc : list bitU -> integer -> bitU -> list bitU
 let update_vec_inc = update_bv_inc
 let update_vec_inc_maybe v i b = Just (update_vec_inc v i b)
 let update_vec_inc_fail v i b = return (update_vec_inc v i b)
-let update_vec_inc_oracle v i b = return (update_vec_inc v i b)
+let update_vec_inc_nondet v i b = return (update_vec_inc v i b)
 
 val update_vec_dec : list bitU -> integer -> bitU -> list bitU
 let update_vec_dec = update_bv_dec
 let update_vec_dec_maybe v i b = Just (update_vec_dec v i b)
 let update_vec_dec_fail v i b = return (update_vec_dec v i b)
-let update_vec_dec_oracle v i b = return (update_vec_dec v i b)
+let update_vec_dec_nondet v i b = return (update_vec_dec v i b)
 
 val subrange_vec_inc : list bitU -> integer -> integer -> list bitU
 let subrange_vec_inc = subrange_bv_inc
@@ -89,19 +89,19 @@ val cons_vec : bitU -> list bitU -> list bitU
 let cons_vec = cons_bv
 let cons_vec_maybe b v = Just (cons_vec b v)
 let cons_vec_fail b v = return (cons_vec b v)
-let cons_vec_oracle b v = return (cons_vec b v)
+let cons_vec_nondet b v = return (cons_vec b v)
 
 val cast_unit_vec : bitU -> list bitU
 let cast_unit_vec = cast_unit_bv
 let cast_unit_vec_maybe b = Just (cast_unit_vec b)
 let cast_unit_vec_fail b = return (cast_unit_vec b)
-let cast_unit_vec_oracle b = return (cast_unit_vec b)
+let cast_unit_vec_nondet b = return (cast_unit_vec b)
 
 val vec_of_bit : integer -> bitU -> list bitU
 let vec_of_bit = bv_of_bit
 let vec_of_bit_maybe len b = Just (vec_of_bit len b)
 let vec_of_bit_fail len b = return (vec_of_bit len b)
-let vec_of_bit_oracle len b = return (vec_of_bit len b)
+let vec_of_bit_nondet len b = return (vec_of_bit len b)
 
 val msb : list bitU -> bitU
 let msb = most_significant
@@ -109,7 +109,7 @@ let msb = most_significant
 val int_of_vec_maybe : bool -> list bitU -> maybe integer
 let int_of_vec_maybe = int_of_bv
 let int_of_vec_fail sign v = maybe_fail "int_of_vec" (int_of_vec_maybe sign v)
-let int_of_vec_oracle sign v = bools_of_bits_oracle v >>= (fun v -> return (int_of_bools sign v))
+let int_of_vec_nondet sign v = bools_of_bits_nondet v >>= (fun v -> return (int_of_bools sign v))
 let int_of_vec sign v = maybe_failwith (int_of_vec_maybe sign v)
 
 val string_of_bits : list bitU -> string
@@ -179,25 +179,25 @@ val subs_vec_bit     : list bitU -> bitU -> list bitU
 let add_vec_bool       l r = arith_op_bv_bool integerAdd false l r
 let add_vec_bit_maybe  l r = arith_op_bv_bit integerAdd false l r
 let add_vec_bit_fail   l r = maybe_fail "add_vec_bit" (add_vec_bit_maybe l r)
-let add_vec_bit_oracle l r = bool_of_bitU_oracle r >>= (fun r -> return (add_vec_bool l r))
+let add_vec_bit_nondet l r = bool_of_bitU_nondet r >>= (fun r -> return (add_vec_bool l r))
 let add_vec_bit        l r = fromMaybe (repeat [BU] (length l)) (add_vec_bit_maybe l r)
 
 let adds_vec_bool       l r = arith_op_bv_bool integerAdd true l r
 let adds_vec_bit_maybe  l r = arith_op_bv_bit integerAdd true l r
 let adds_vec_bit_fail   l r = maybe_fail "adds_vec_bit" (adds_vec_bit_maybe l r)
-let adds_vec_bit_oracle l r = bool_of_bitU_oracle r >>= (fun r -> return (adds_vec_bool l r))
+let adds_vec_bit_nondet l r = bool_of_bitU_nondet r >>= (fun r -> return (adds_vec_bool l r))
 let adds_vec_bit        l r = fromMaybe (repeat [BU] (length l)) (adds_vec_bit_maybe l r)
 
 let sub_vec_bool        l r = arith_op_bv_bool integerMinus false l r
 let sub_vec_bit_maybe   l r = arith_op_bv_bit integerMinus false l r
 let sub_vec_bit_fail    l r = maybe_fail "sub_vec_bit" (sub_vec_bit_maybe l r)
-let sub_vec_bit_oracle  l r = bool_of_bitU_oracle r >>= (fun r -> return (sub_vec_bool l r))
+let sub_vec_bit_nondet  l r = bool_of_bitU_nondet r >>= (fun r -> return (sub_vec_bool l r))
 let sub_vec_bit         l r = fromMaybe (repeat [BU] (length l)) (sub_vec_bit_maybe l r)
 
 let subs_vec_bool       l r = arith_op_bv_bool integerMinus true l r
 let subs_vec_bit_maybe  l r = arith_op_bv_bit integerMinus true l r
 let subs_vec_bit_fail   l r = maybe_fail "sub_vec_bit" (subs_vec_bit_maybe l r)
-let subs_vec_bit_oracle l r = bool_of_bitU_oracle r >>= (fun r -> return (subs_vec_bool l r))
+let subs_vec_bit_nondet l r = bool_of_bitU_nondet r >>= (fun r -> return (subs_vec_bool l r))
 let subs_vec_bit        l r = fromMaybe (repeat [BU] (length l)) (subs_vec_bit_maybe l r)
 
 (*val add_overflow_vec         : list bitU -> list bitU -> (list bitU * bitU * bitU)
@@ -236,47 +236,47 @@ let rotr         = rotr_bv
 val mod_vec        : list bitU -> list bitU -> list bitU
 val mod_vec_maybe  : list bitU -> list bitU -> maybe (list bitU)
 val mod_vec_fail   : forall 'rv 'e. list bitU -> list bitU -> monad 'rv (list bitU) 'e
-val mod_vec_oracle : forall 'rv 'e. list bitU -> list bitU -> monad 'rv (list bitU) 'e
+val mod_vec_nondet : forall 'rv 'e. list bitU -> list bitU -> monad 'rv (list bitU) 'e
 let mod_vec        l r = fromMaybe (repeat [BU] (length l)) (mod_bv l r)
 let mod_vec_maybe  l r = mod_bv l r
 let mod_vec_fail   l r = maybe_fail "mod_vec" (mod_bv l r)
-let mod_vec_oracle l r = of_bits_oracle (mod_vec l r)
+let mod_vec_nondet l r = of_bits_nondet (mod_vec l r)
 
 val quot_vec        : list bitU -> list bitU -> list bitU
 val quot_vec_maybe  : list bitU -> list bitU -> maybe (list bitU)
 val quot_vec_fail   : forall 'rv 'e. list bitU -> list bitU -> monad 'rv (list bitU) 'e
-val quot_vec_oracle : forall 'rv 'e. list bitU -> list bitU -> monad 'rv (list bitU) 'e
+val quot_vec_nondet : forall 'rv 'e. list bitU -> list bitU -> monad 'rv (list bitU) 'e
 let quot_vec        l r = fromMaybe (repeat [BU] (length l)) (quot_bv l r)
 let quot_vec_maybe  l r = quot_bv l r
 let quot_vec_fail   l r = maybe_fail "quot_vec" (quot_bv l r)
-let quot_vec_oracle l r = of_bits_oracle (quot_vec l r)
+let quot_vec_nondet l r = of_bits_nondet (quot_vec l r)
 
 val quots_vec        : list bitU -> list bitU -> list bitU
 val quots_vec_maybe  : list bitU -> list bitU -> maybe (list bitU)
 val quots_vec_fail   : forall 'rv 'e. list bitU -> list bitU -> monad 'rv (list bitU) 'e
-val quots_vec_oracle : forall 'rv 'e. list bitU -> list bitU -> monad 'rv (list bitU) 'e
+val quots_vec_nondet : forall 'rv 'e. list bitU -> list bitU -> monad 'rv (list bitU) 'e
 let quots_vec        l r = fromMaybe (repeat [BU] (length l)) (quots_bv l r)
 let quots_vec_maybe  l r = quots_bv l r
 let quots_vec_fail   l r = maybe_fail "quots_vec" (quots_bv l r)
-let quots_vec_oracle l r = of_bits_oracle (quots_vec l r)
+let quots_vec_nondet l r = of_bits_nondet (quots_vec l r)
 
 val mod_vec_int        : list bitU -> integer -> list bitU
 val mod_vec_int_maybe  : list bitU -> integer -> maybe (list bitU)
 val mod_vec_int_fail   : forall 'rv 'e. list bitU -> integer -> monad 'rv (list bitU) 'e
-val mod_vec_int_oracle : forall 'rv 'e. list bitU -> integer -> monad 'rv (list bitU) 'e
+val mod_vec_int_nondet : forall 'rv 'e. list bitU -> integer -> monad 'rv (list bitU) 'e
 let mod_vec_int        l r = fromMaybe (repeat [BU] (length l)) (mod_bv_int l r)
 let mod_vec_int_maybe  l r = mod_bv_int l r
 let mod_vec_int_fail   l r = maybe_fail "mod_vec_int" (mod_bv_int l r)
-let mod_vec_int_oracle l r = of_bits_oracle (mod_vec_int l r)
+let mod_vec_int_nondet l r = of_bits_nondet (mod_vec_int l r)
 
 val quot_vec_int        : list bitU -> integer -> list bitU
 val quot_vec_int_maybe  : list bitU -> integer -> maybe (list bitU)
 val quot_vec_int_fail   : forall 'rv 'e. list bitU -> integer -> monad 'rv (list bitU) 'e
-val quot_vec_int_oracle : forall 'rv 'e. list bitU -> integer -> monad 'rv (list bitU) 'e
+val quot_vec_int_nondet : forall 'rv 'e. list bitU -> integer -> monad 'rv (list bitU) 'e
 let quot_vec_int        l r = fromMaybe (repeat [BU] (length l)) (quot_bv_int l r)
 let quot_vec_int_maybe  l r = quot_bv_int l r
 let quot_vec_int_fail   l r = maybe_fail "quot_vec_int" (quot_bv_int l r)
-let quot_vec_int_oracle l r = of_bits_oracle (quot_vec_int l r)
+let quot_vec_int_nondet l r = of_bits_nondet (quot_vec_int l r)
 
 val replicate_bits : list bitU -> integer -> list bitU
 let replicate_bits = replicate_bits_bv
@@ -285,8 +285,8 @@ val duplicate : bitU -> integer -> list bitU
 let duplicate = duplicate_bit_bv
 let duplicate_maybe b n = Just (duplicate b n)
 let duplicate_fail b n = return (duplicate b n)
-let duplicate_oracle b n =
-  bool_of_bitU_oracle b >>= (fun b ->
+let duplicate_nondet b n =
+  bool_of_bitU_nondet b >>= (fun b ->
   return (duplicate (bitU_of_bool b) n))
 
 val reverse_endianness : list bitU -> list bitU
diff --git a/src/gen_lib/sail2_operators_mwords.lem b/src/gen_lib/sail2_operators_mwords.lem
index 1e4d63ba..61048ac5 100644
--- a/src/gen_lib/sail2_operators_mwords.lem
+++ b/src/gen_lib/sail2_operators_mwords.lem
@@ -10,21 +10,21 @@ open import Sail2_prompt
 let inline uint v = unsignedIntegerFromWord v
 let uint_maybe v = Just (uint v)
 let uint_fail v = return (uint v)
-let uint_oracle v = return (uint v)
+let uint_nondet v = return (uint v)
 
 let inline sint v = signedIntegerFromWord v
 let sint_maybe v = Just (sint v)
 let sint_fail v = return (sint v)
-let sint_oracle v = return (sint v)
+let sint_nondet v = return (sint v)
 
 val vec_of_bits_maybe    : forall 'a. Size 'a => list bitU -> maybe (mword 'a)
 val vec_of_bits_fail     : forall 'rv 'a 'e. Size 'a => list bitU -> monad 'rv (mword 'a) 'e
-val vec_of_bits_oracle   : forall 'rv 'a 'e. Size 'a => list bitU -> monad 'rv (mword 'a) 'e
+val vec_of_bits_nondet   : forall 'rv 'a 'e. Size 'a => list bitU -> monad 'rv (mword 'a) 'e
 val vec_of_bits_failwith : forall 'a. Size 'a => list bitU -> mword 'a
 val vec_of_bits          : forall 'a. Size 'a => list bitU -> mword 'a
 let vec_of_bits_maybe bits = of_bits bits
 let vec_of_bits_fail bits = of_bits_fail bits
-let vec_of_bits_oracle bits = of_bits_oracle bits
+let vec_of_bits_nondet bits = of_bits_nondet bits
 let vec_of_bits_failwith bits = of_bits_failwith bits
 let vec_of_bits bits = of_bits_failwith bits
 
@@ -38,8 +38,8 @@ let update_vec_dec_maybe w i b = update_mword_dec w i b
 let update_vec_dec_fail w i b =
   bool_of_bitU_fail b >>= (fun b ->
   return (update_mword_bool_dec w i b))
-let update_vec_dec_oracle w i b =
-  bool_of_bitU_oracle b >>= (fun b ->
+let update_vec_dec_nondet w i b =
+  bool_of_bitU_nondet b >>= (fun b ->
   return (update_mword_bool_dec w i b))
 let update_vec_dec w i b = maybe_failwith (update_vec_dec_maybe w i b)
 
@@ -47,8 +47,8 @@ let update_vec_inc_maybe w i b = update_mword_inc w i b
 let update_vec_inc_fail w i b =
   bool_of_bitU_fail b >>= (fun b ->
   return (update_mword_bool_inc w i b))
-let update_vec_inc_oracle w i b =
-  bool_of_bitU_oracle b >>= (fun b ->
+let update_vec_inc_nondet w i b =
+  bool_of_bitU_nondet b >>= (fun b ->
   return (update_mword_bool_inc w i b))
 let update_vec_inc w i b = maybe_failwith (update_vec_inc_maybe w i b)
 
@@ -89,21 +89,21 @@ val cons_vec_bool : forall 'a 'b 'c. Size 'a, Size 'b => bool -> mword 'a -> mwo
 let cons_vec_bool b w = wordFromBitlist (b :: bitlistFromWord w)
 let cons_vec_maybe b w = Maybe.map (fun b -> cons_vec_bool b w) (bool_of_bitU b)
 let cons_vec_fail b w = bool_of_bitU_fail b >>= (fun b -> return (cons_vec_bool b w))
-let cons_vec_oracle b w = bool_of_bitU_oracle b >>= (fun b -> return (cons_vec_bool b w))
+let cons_vec_nondet b w = bool_of_bitU_nondet b >>= (fun b -> return (cons_vec_bool b w))
 let cons_vec b w = maybe_failwith (cons_vec_maybe b w)
 
 val vec_of_bool : forall 'a. Size 'a => integer -> bool -> mword 'a
 let vec_of_bool _ b = wordFromBitlist [b]
 let vec_of_bit_maybe len b = Maybe.map (vec_of_bool len) (bool_of_bitU b)
 let vec_of_bit_fail len b = bool_of_bitU_fail b >>= (fun b -> return (vec_of_bool len b))
-let vec_of_bit_oracle len b = bool_of_bitU_oracle b >>= (fun b -> return (vec_of_bool len b))
+let vec_of_bit_nondet len b = bool_of_bitU_nondet b >>= (fun b -> return (vec_of_bool len b))
 let vec_of_bit len b = maybe_failwith (vec_of_bit_maybe len b)
 
 val cast_bool_vec : bool -> mword ty1
 let cast_bool_vec b = vec_of_bool 1 b
 let cast_unit_vec_maybe b = vec_of_bit_maybe 1 b
 let cast_unit_vec_fail b = bool_of_bitU_fail b >>= (fun b -> return (cast_bool_vec b))
-let cast_unit_vec_oracle b = bool_of_bitU_oracle b >>= (fun b -> return (cast_bool_vec b))
+let cast_unit_vec_nondet b = bool_of_bitU_nondet b >>= (fun b -> return (cast_bool_vec b))
 let cast_unit_vec b = maybe_failwith (cast_unit_vec_maybe b)
 
 val msb : forall 'a. Size 'a => mword 'a -> bitU
@@ -176,25 +176,25 @@ val subs_vec_bool : forall 'a. Size 'a => mword 'a -> bool -> mword 'a
 let add_vec_bool        l r = arith_op_bv_bool integerAdd false l r
 let add_vec_bit_maybe   l r = Maybe.map (add_vec_bool l) (bool_of_bitU r)
 let add_vec_bit_fail    l r = bool_of_bitU_fail r >>= (fun r -> return (add_vec_bool l r))
-let add_vec_bit_oracle  l r = bool_of_bitU_oracle r >>= (fun r -> return (add_vec_bool l r))
+let add_vec_bit_nondet  l r = bool_of_bitU_nondet r >>= (fun r -> return (add_vec_bool l r))
 let add_vec_bit         l r = maybe_failwith (add_vec_bit_maybe  l r)
 
 let adds_vec_bool       l r = arith_op_bv_bool integerAdd true  l r
 let adds_vec_bit_maybe  l r = Maybe.map (adds_vec_bool l) (bool_of_bitU r)
 let adds_vec_bit_fail   l r = bool_of_bitU_fail r >>= (fun r -> return (adds_vec_bool l r))
-let adds_vec_bit_oracle l r = bool_of_bitU_oracle r >>= (fun r -> return (adds_vec_bool l r))
+let adds_vec_bit_nondet l r = bool_of_bitU_nondet r >>= (fun r -> return (adds_vec_bool l r))
 let adds_vec_bit        l r = maybe_failwith (adds_vec_bit_maybe l r)
 
 let sub_vec_bool        l r = arith_op_bv_bool integerMinus false l r
 let sub_vec_bit_maybe   l r = Maybe.map (sub_vec_bool l) (bool_of_bitU r)
 let sub_vec_bit_fail    l r = bool_of_bitU_fail r >>= (fun r -> return (sub_vec_bool l r))
-let sub_vec_bit_oracle  l r = bool_of_bitU_oracle r >>= (fun r -> return (sub_vec_bool l r))
+let sub_vec_bit_nondet  l r = bool_of_bitU_nondet r >>= (fun r -> return (sub_vec_bool l r))
 let sub_vec_bit         l r = maybe_failwith (sub_vec_bit_maybe  l r)
 
 let subs_vec_bool       l r = arith_op_bv_bool integerMinus true  l r
 let subs_vec_bit_maybe  l r = Maybe.map (subs_vec_bool l) (bool_of_bitU r)
 let subs_vec_bit_fail   l r = bool_of_bitU_fail r >>= (fun r -> return (subs_vec_bool l r))
-let subs_vec_bit_oracle l r = bool_of_bitU_oracle r >>= (fun r -> return (subs_vec_bool l r))
+let subs_vec_bit_nondet l r = bool_of_bitU_nondet r >>= (fun r -> return (subs_vec_bool l r))
 let subs_vec_bit        l r = maybe_failwith (subs_vec_bit_maybe  l r)
 
 (* TODO
@@ -238,66 +238,66 @@ let rotr         = rotr_mword
 val mod_vec        : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
 val mod_vec_maybe  : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a)
 val mod_vec_fail   : forall 'rv 'a 'e. Size 'a => mword 'a -> mword 'a -> monad 'rv (mword 'a) 'e
-val mod_vec_oracle : forall 'rv 'a 'e. Size 'a => mword 'a -> mword 'a -> monad 'rv (mword 'a) 'e
+val mod_vec_nondet : forall 'rv 'a 'e. Size 'a => mword 'a -> mword 'a -> monad 'rv (mword 'a) 'e
 let mod_vec        l r = mod_mword l r
 let mod_vec_maybe  l r = mod_bv l r
 let mod_vec_fail   l r = maybe_fail "mod_vec" (mod_bv l r)
-let mod_vec_oracle l r =
+let mod_vec_nondet l r =
   match (mod_bv l r) with
     | Just w -> return w
-    | Nothing -> mword_oracle ()
+    | Nothing -> mword_nondet ()
   end
 
 val quot_vec        : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
 val quot_vec_maybe  : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a)
 val quot_vec_fail   : forall 'rv 'a 'e. Size 'a => mword 'a -> mword 'a -> monad 'rv (mword 'a) 'e
-val quot_vec_oracle : forall 'rv 'a 'e. Size 'a => mword 'a -> mword 'a -> monad 'rv (mword 'a) 'e
+val quot_vec_nondet : forall 'rv 'a 'e. Size 'a => mword 'a -> mword 'a -> monad 'rv (mword 'a) 'e
 let quot_vec        l r = quot_mword l r
 let quot_vec_maybe  l r = quot_bv l r
 let quot_vec_fail   l r = maybe_fail "quot_vec" (quot_bv l r)
-let quot_vec_oracle l r =
+let quot_vec_nondet l r =
   match (quot_bv l r) with
     | Just w -> return w
-    | Nothing -> mword_oracle ()
+    | Nothing -> mword_nondet ()
   end
 
 val quots_vec        : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
 val quots_vec_maybe  : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a)
 val quots_vec_fail   : forall 'rv 'a 'e. Size 'a => mword 'a -> mword 'a -> monad 'rv (mword 'a) 'e
-val quots_vec_oracle : forall 'rv 'a 'e. Size 'a => mword 'a -> mword 'a -> monad 'rv (mword 'a) 'e
+val quots_vec_nondet : forall 'rv 'a 'e. Size 'a => mword 'a -> mword 'a -> monad 'rv (mword 'a) 'e
 let quots_vec        l r = quots_mword l r
 let quots_vec_maybe  l r = quots_bv l r
 let quots_vec_fail   l r = maybe_fail "quots_vec" (quots_bv l r)
-let quots_vec_oracle l r =
+let quots_vec_nondet l r =
   match (quots_bv l r) with
     | Just w -> return w
-    | Nothing -> mword_oracle ()
+    | Nothing -> mword_nondet ()
   end
 
 val mod_vec_int        : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
 val mod_vec_int_maybe  : forall 'a. Size 'a => mword 'a -> integer -> maybe (mword 'a)
 val mod_vec_int_fail   : forall 'rv 'a 'e. Size 'a => mword 'a -> integer -> monad 'rv (mword 'a) 'e
-val mod_vec_int_oracle : forall 'rv 'a 'e. Size 'a => mword 'a -> integer -> monad 'rv (mword 'a) 'e
+val mod_vec_int_nondet : forall 'rv 'a 'e. Size 'a => mword 'a -> integer -> monad 'rv (mword 'a) 'e
 let mod_vec_int        l r = mod_mword_int l r
 let mod_vec_int_maybe  l r = mod_bv_int l r
 let mod_vec_int_fail   l r = maybe_fail "mod_vec_int" (mod_bv_int l r)
-let mod_vec_int_oracle l r =
+let mod_vec_int_nondet l r =
   match (mod_bv_int l r) with
     | Just w -> return w
-    | Nothing -> mword_oracle ()
+    | Nothing -> mword_nondet ()
   end
 
 val quot_vec_int        : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
 val quot_vec_int_maybe  : forall 'a. Size 'a => mword 'a -> integer -> maybe (mword 'a)
 val quot_vec_int_fail   : forall 'rv 'a 'e. Size 'a => mword 'a -> integer -> monad 'rv (mword 'a) 'e
-val quot_vec_int_oracle : forall 'rv 'a 'e. Size 'a => mword 'a -> integer -> monad 'rv (mword 'a) 'e
+val quot_vec_int_nondet : forall 'rv 'a 'e. Size 'a => mword 'a -> integer -> monad 'rv (mword 'a) 'e
 let quot_vec_int        l r = quot_mword_int l r
 let quot_vec_int_maybe  l r = quot_bv_int l r
 let quot_vec_int_fail   l r = maybe_fail "quot_vec_int" (quot_bv_int l r)
-let quot_vec_int_oracle l r =
+let quot_vec_int_nondet l r =
   match (quot_bv_int l r) with
     | Just w -> return w
-    | Nothing -> mword_oracle ()
+    | Nothing -> mword_nondet ()
   end
 
 val replicate_bits : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
@@ -307,7 +307,7 @@ val duplicate_bool : forall 'a. Size 'a => bool -> integer -> mword 'a
 let duplicate_bool   b n = wordFromBitlist (repeat [b] n)
 let duplicate_maybe  b n = Maybe.map (fun b -> duplicate_bool b n) (bool_of_bitU b)
 let duplicate_fail   b n = bool_of_bitU_fail b >>= (fun b -> return (duplicate_bool b n))
-let duplicate_oracle b n = bool_of_bitU_oracle b >>= (fun b -> return (duplicate_bool b n))
+let duplicate_nondet b n = bool_of_bitU_nondet b >>= (fun b -> return (duplicate_bool b n))
 let duplicate        b n = maybe_failwith (duplicate_maybe b n)
 
 val reverse_endianness : forall 'a. Size 'a => mword 'a -> mword 'a
diff --git a/src/gen_lib/sail2_prompt.lem b/src/gen_lib/sail2_prompt.lem
index 08a47052..e01cc051 100644
--- a/src/gen_lib/sail2_prompt.lem
+++ b/src/gen_lib/sail2_prompt.lem
@@ -51,31 +51,31 @@ let bool_of_bitU_fail = function
   | BU -> Fail "bool_of_bitU"
 end
 
-val bool_of_bitU_oracle : forall 'rv 'e. bitU -> monad 'rv bool 'e
-let bool_of_bitU_oracle = function
+val bool_of_bitU_nondet : forall 'rv 'e. bitU -> monad 'rv bool 'e
+let bool_of_bitU_nondet = function
   | B0 -> return false
   | B1 -> return true
   | BU -> undefined_bool ()
 end
 
-val bools_of_bits_oracle : forall 'rv 'e. list bitU -> monad 'rv (list bool) 'e
-let bools_of_bits_oracle bits =
+val bools_of_bits_nondet : forall 'rv 'e. list bitU -> monad 'rv (list bool) 'e
+let bools_of_bits_nondet bits =
   foreachM bits []
     (fun b bools ->
-      bool_of_bitU_oracle b >>= (fun b ->
+      bool_of_bitU_nondet b >>= (fun b ->
       return (bools ++ [b])))
 
-val of_bits_oracle : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monad 'rv 'a 'e
-let of_bits_oracle bits =
-  bools_of_bits_oracle bits >>= (fun bs ->
+val of_bits_nondet : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monad 'rv 'a 'e
+let of_bits_nondet bits =
+  bools_of_bits_nondet bits >>= (fun bs ->
   return (of_bools bs))
 
 val of_bits_fail : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monad 'rv 'a 'e
 let of_bits_fail bits = maybe_fail "of_bits" (of_bits bits)
 
-val mword_oracle : forall 'rv 'a 'e. Size 'a => unit -> monad 'rv (mword 'a) 'e
-let mword_oracle () =
-  bools_of_bits_oracle (repeat [BU] (integerFromNat size)) >>= (fun bs ->
+val mword_nondet : forall 'rv 'a 'e. Size 'a => unit -> monad 'rv (mword 'a) 'e
+let mword_nondet () =
+  bools_of_bits_nondet (repeat [BU] (integerFromNat size)) >>= (fun bs ->
   return (wordFromBitlist bs))
 
 val whileM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
@@ -93,6 +93,16 @@ let rec untilM vars cond body =
   cond vars >>= fun cond_val ->
   if cond_val then return vars else untilM vars cond body
 
+val internal_pick : forall 'rv 'a 'e. list 'a -> monad 'rv 'a 'e
+let internal_pick xs =
+  (* Use sufficiently many undefined bits and convert into an index into the list *)
+  bools_of_bits_nondet (repeat [BU] (length_list xs)) >>= fun bs ->
+  let idx = (natFromNatural (nat_of_bools bs)) mod List.length xs in
+  match index xs idx with
+    | Just x -> return x
+    | Nothing -> Fail "internal_pick"
+  end
+
 (*let write_two_regs r1 r2 vec =
   let is_inc =
     let is_inc_r1 = is_inc_of_reg r1 in
diff --git a/src/gen_lib/sail2_prompt_monad.lem b/src/gen_lib/sail2_prompt_monad.lem
index 745589e2..78b1615e 100644
--- a/src/gen_lib/sail2_prompt_monad.lem
+++ b/src/gen_lib/sail2_prompt_monad.lem
@@ -29,6 +29,7 @@ type monad 'regval 'a 'e =
   | Read_reg of register_name * ('regval -> monad 'regval 'a 'e)
   (* Request to write register *)
   | Write_reg of register_name * 'regval * monad 'regval 'a 'e
+  (* Request to choose a Boolean, e.g. to resolve an undefined bit *)
   | Undefined of (bool -> monad 'regval 'a 'e)
   (* Print debugging or tracing information *)
   | Print of string * monad 'regval 'a 'e
diff --git a/src/gen_lib/sail2_state.lem b/src/gen_lib/sail2_state.lem
index 82ac35d8..f703dead 100644
--- a/src/gen_lib/sail2_state.lem
+++ b/src/gen_lib/sail2_state.lem
@@ -41,31 +41,31 @@ let bool_of_bitU_fail = function
   | BU -> failS "bool_of_bitU"
 end
 
-val bool_of_bitU_oracleS : forall 'rv 'e. bitU -> monadS 'rv bool 'e
-let bool_of_bitU_oracleS = function
+val bool_of_bitU_nondetS : forall 'rv 'e. bitU -> monadS 'rv bool 'e
+let bool_of_bitU_nondetS = function
   | B0 -> returnS false
   | B1 -> returnS true
   | BU -> undefined_boolS ()
 end
 
-val bools_of_bits_oracleS : forall 'rv 'e. list bitU -> monadS 'rv (list bool) 'e
-let bools_of_bits_oracleS bits =
+val bools_of_bits_nondetS : forall 'rv 'e. list bitU -> monadS 'rv (list bool) 'e
+let bools_of_bits_nondetS bits =
   foreachS bits []
     (fun b bools ->
-      bool_of_bitU_oracleS b >>$= (fun b ->
+      bool_of_bitU_nondetS b >>$= (fun b ->
       returnS (bools ++ [b])))
 
-val of_bits_oracleS : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monadS 'rv 'a 'e
-let of_bits_oracleS bits =
-  bools_of_bits_oracleS bits >>$= (fun bs ->
+val of_bits_nondetS : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monadS 'rv 'a 'e
+let of_bits_nondetS bits =
+  bools_of_bits_nondetS bits >>$= (fun bs ->
   returnS (of_bools bs))
 
 val of_bits_failS : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monadS 'rv 'a 'e
 let of_bits_failS bits = maybe_failS "of_bits" (of_bits bits)
 
-val mword_oracleS : forall 'rv 'a 'e. Size 'a => unit -> monadS 'rv (mword 'a) 'e
-let mword_oracleS () =
-  bools_of_bits_oracleS (repeat [BU] (integerFromNat size)) >>$= (fun bs ->
+val mword_nondetS : forall 'rv 'a 'e. Size 'a => unit -> monadS 'rv (mword 'a) 'e
+let mword_nondetS () =
+  bools_of_bits_nondetS (repeat [BU] (integerFromNat size)) >>$= (fun bs ->
   returnS (wordFromBitlist bs))
 
 
@@ -83,3 +83,13 @@ let rec untilS vars cond body s =
   (body vars >>$= (fun vars s' ->
   (cond vars >>$= (fun cond_val s'' ->
   if cond_val then returnS vars s'' else untilS vars cond body s'')) s')) s
+
+val internal_pickS : forall 'rv 'a 'e. list 'a -> monadS 'rv 'a 'e
+let internal_pickS xs =
+  (* Use sufficiently many undefined bits and convert into an index into the list *)
+  bools_of_bits_nondetS (repeat [BU] (length_list xs)) >>$= fun bs ->
+  let idx = (natFromNatural (nat_of_bools bs)) mod List.length xs in
+  match index xs idx with
+    | Just x -> returnS x
+    | Nothing -> failS "internal_pick"
+  end
diff --git a/src/gen_lib/sail2_state_monad.lem b/src/gen_lib/sail2_state_monad.lem
index f207699f..30b296cc 100644
--- a/src/gen_lib/sail2_state_monad.lem
+++ b/src/gen_lib/sail2_state_monad.lem
@@ -13,20 +13,15 @@ type sequential_state 'regs =
      memstate : memstate;
      tagstate : tagstate;
      write_ea : maybe (write_kind * integer * integer);
-     last_exclusive_operation_was_load : bool;
-     (* Random bool generator for use as an undefined bit oracle *)
-     next_bool : nat -> (bool * nat);
-     seed : nat |>
+     last_exclusive_operation_was_load : bool |>
 
-val init_state : forall 'regs. 'regs -> (nat -> (bool* nat)) -> nat -> sequential_state 'regs
-let init_state regs o s =
+val init_state : forall 'regs. 'regs -> sequential_state 'regs
+let init_state regs =
   <| regstate = regs;
      memstate = Map.empty;
      tagstate = Map.empty;
      write_ea = Nothing;
-     last_exclusive_operation_was_load = false;
-     next_bool = o;
-     seed = s |>
+     last_exclusive_operation_was_load = false |>
 
 type ex 'e =
   | Failure of string
@@ -69,10 +64,7 @@ val failS : forall 'regs 'a 'e. string -> monadS 'regs 'a 'e
 let failS msg s = {(Ex (Failure msg), s)}
 
 val undefined_boolS : forall 'regval 'regs 'a 'e. unit -> monadS 'regs bool 'e
-let undefined_boolS () =
-  readS (fun s -> s.next_bool (s.seed)) >>$= (fun (b, seed) ->
-  updateS (fun s -> <| s with seed = seed |>) >>$
-  returnS b)
+let undefined_boolS () = chooseS {false; true}
 
 val exitS : forall 'regs 'e 'a. unit -> monadS 'regs 'a 'e
 let exitS () = failS "exit"