3 files changed, 36 insertions, 0 deletions
diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v
index 5ab93cbc..68d097fb 100644
--- a/lib/coq/Sail2_prompt.v
+++ b/lib/coq/Sail2_prompt.v
@@ -181,6 +181,37 @@ Definition untilMT {RV Vars E} limit (vars : Vars) (cond : Vars -> monad RV bool
     else slice vec (start_vec - size_r1) (start_vec - size_vec) in
   write_reg r1 r1_v >> write_reg r2 r2_v*)
 
+Fixpoint pick_bit_list {rv e} (n:nat) : monad rv (list bool) e :=
+  match n with
+  | O => returnm []
+  | S m => choose_bool "pick_bit_list" >>= fun b =>
+           pick_bit_list m >>= fun t =>
+           returnm (b::t)
+  end%list.
+
+Definition internal_pick {rv a e} (xs : list a) : monad rv a e :=
+  let n := length xs in
+  match xs with
+  | h::_ =>
+    pick_bit_list (2 + n) >>= fun bs =>
+    let i := (Word.wordToNat (wordFromBitlist bs) mod n)%nat in
+    returnm (List.nth i xs h)
+  | [] => Fail "internal_pick called on empty list"
+  end.
+
+Fixpoint undefined_word_nat {rv e} n : monad rv (Word.word n) e :=
+  match n with
+  | O => returnm Word.WO
+  | S m =>
+    choose_bool "undefined_word_nat" >>= fun b =>
+    undefined_word_nat m >>= fun t =>
+    returnm (Word.WS b t)
+  end.
+
+Definition undefined_bitvector {rv e} n `{ArithFact (n >= 0)} : monad rv (mword n) e :=
+  undefined_word_nat (Z.to_nat n) >>= fun w =>
+  returnm (word_to_mword w).
+
 (* If we need to build an existential after a monadic operation, assume that
    we can do it entirely from the type. *)
 
diff --git a/lib/coq/Sail2_prompt_monad.v b/lib/coq/Sail2_prompt_monad.v
index f95e4b6c..b26a2ff3 100644
--- a/lib/coq/Sail2_prompt_monad.v
+++ b/lib/coq/Sail2_prompt_monad.v
@@ -113,6 +113,8 @@ Definition choose_bool {rv E} descr : monad rv bool E := Choose descr returnm.
 (*val undefined_bool : forall 'rv 'e. unit -> monad 'rv bool 'e*)
 Definition undefined_bool {rv e} (_:unit) : monad rv bool e := choose_bool "undefined_bool".
 
+Definition undefined_unit {rv e} (_:unit) : monad rv unit e := returnm tt.
+
 (*val assert_exp : forall rv e. bool -> string -> monad rv unit e*)
 Definition assert_exp {rv E} (exp :bool) msg : monad rv unit E :=
  if exp then Done tt else Fail msg.
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 1ddc3f22..4bfc9125 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -873,6 +873,9 @@ Program Definition to_word {n} : n >= 0 -> word (Z.to_nat n) -> mword n :=
   | Zpos _ => fun _ w => w
   end.
 
+Definition word_to_mword {n} (w : word (Z.to_nat n)) `{H:ArithFact (n >= 0)} : mword n :=
+  to_word (match H with Build_ArithFact _ H' => H' end) w.
+
 (*val length_mword : forall a. mword a -> Z*)
 Definition length_mword {n} (w : mword n) := n.