Begin refactoring Sail library

- Add back support for bit list representation of bit vectors, for backwards
  compatibility in order to ease integration with the interpreter.  For this
purpose, split out a file sail_operators.lem from sail_values.lem, and add a
variant sail_operators_mwords.lem for the machine word representation of
bitvectors.  Currently, Sail is hardcoded to use machine words for the
sequential state monad, and bit lists for the free monad, but this could be
turned into a command line flag.

- Add a prelude_wrappers.sail file for glueing the Sail prelude to the Lem
  library.  The wrappers make use of sizeof expressions to extract type
information from bitvectors (length, start index) in order to pass it to the
Lem functions.

- Add early return support to the free monad, using a new constructor "Return
  of 'r".  As with the sequential monad, functions with early return are
wrapped into "catch_early_return", which extracts the return value at the end
of the function execution.

6 files changed, 1187 insertions, 1626 deletions

diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 0944f42b..5c539354 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -2,10 +2,13 @@ open import Pervasives_extra
 open import Sail_impl_base
 open import Sail_values
 
-val return : forall 'a. 'a -> outcome 'a
+type MR 'a 'r = outcome_r 'a 'r
+type M 'a = outcome 'a
+
+val return : forall 'a 'r. 'a -> MR 'a 'r
 let return a = Done a
 
-val bind : forall 'a 'b. outcome 'a -> ('a -> outcome 'b) -> outcome 'b
+val bind : forall 'a 'b 'r. MR 'a 'r -> ('a -> MR 'b 'r) -> MR 'b 'r
 let rec bind m f = match m with
   | Done a ->              f a
   | Read_mem descr k ->    Read_mem descr   (fun v -> let (o,opt) = k v in (bind o f,opt))
@@ -19,19 +22,57 @@ let rec bind m f = match m with
   | Escape descr ->        Escape descr
   | Fail descr ->          Fail descr
   | Error descr ->         Error descr
+  | Return a ->            Return a
   | Internal descr o_s ->  Internal descr   (let (o,opt) = o_s in (bind o f ,opt))
 end
 
 
-type M 'a = outcome 'a
-
 let inline (>>=) = bind
-val (>>) : forall 'b. M unit -> M 'b -> M 'b
+val (>>) : forall 'b 'r. MR unit 'r -> MR 'b 'r -> MR 'b 'r
 let inline (>>) m n = m >>= fun _ -> n
 
 val exit : forall 'a 'b. 'b -> M 'a
 let exit s = Fail Nothing
 
+val early_return : forall 'r. 'r -> MR unit 'r
+let early_return r = Return r
+
+val liftR : forall 'a 'r. M 'a -> MR 'a 'r
+let rec liftR m = match m with
+  | Done a ->              Done a
+  | Read_mem descr k ->    Read_mem descr   (fun v -> let (o,opt) = k v in (liftR o,opt))
+  | Read_reg descr k ->    Read_reg descr   (fun v -> let (o,opt) = k v in (liftR o,opt))
+  | Write_memv descr k ->  Write_memv descr (fun v -> let (o,opt) = k v in (liftR o,opt))
+  | Excl_res k ->          Excl_res         (fun v -> let (o,opt) = k v in (liftR o,opt))
+  | Write_ea descr o_s ->  Write_ea descr   (let (o,opt) = o_s in (liftR o,opt))
+  | Barrier descr o_s ->   Barrier descr    (let (o,opt) = o_s in (liftR o,opt))
+  | Footprint o_s ->       Footprint        (let (o,opt) = o_s in (liftR o,opt))
+  | Write_reg descr o_s -> Write_reg descr  (let (o,opt) = o_s in (liftR o,opt))
+  | Internal descr o_s ->  Internal descr   (let (o,opt) = o_s in (liftR o,opt))
+  | Escape descr ->        Escape descr
+  | Fail descr ->          Fail descr
+  | Error descr ->         Error descr
+  | Return _ ->            Error "uncaught early return"
+end
+
+val catch_early_return : forall 'a 'r. MR 'a 'a -> M 'a
+let rec catch_early_return m = match m with
+  | Done a ->              Done a
+  | Read_mem descr k ->    Read_mem descr   (fun v -> let (o,opt) = k v in (catch_early_return o,opt))
+  | Read_reg descr k ->    Read_reg descr   (fun v -> let (o,opt) = k v in (catch_early_return o,opt))
+  | Write_memv descr k ->  Write_memv descr (fun v -> let (o,opt) = k v in (catch_early_return o,opt))
+  | Excl_res k ->          Excl_res         (fun v -> let (o,opt) = k v in (catch_early_return o,opt))
+  | Write_ea descr o_s ->  Write_ea descr   (let (o,opt) = o_s in (catch_early_return o,opt))
+  | Barrier descr o_s ->   Barrier descr    (let (o,opt) = o_s in (catch_early_return o,opt))
+  | Footprint o_s ->       Footprint        (let (o,opt) = o_s in (catch_early_return o,opt))
+  | Write_reg descr o_s -> Write_reg descr  (let (o,opt) = o_s in (catch_early_return o,opt))
+  | Internal descr o_s ->  Internal descr   (let (o,opt) = o_s in (catch_early_return o,opt))
+  | Escape descr ->        Escape descr
+  | Fail descr ->          Fail descr
+  | Error descr ->         Error descr
+  | Return a ->            Done a
+end
+
 val read_mem : bool -> read_kind -> vector bitU -> integer -> M (vector bitU)
 let read_mem dir rk addr sz =
   let addr = address_lifted_of_bitv addr in
@@ -73,9 +114,9 @@ let read_reg_bit reg i =
   read_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger i)) >>= fun v ->
   return (extract_only_element v)
 let read_reg_field reg regfield =
-  read_reg_aux (external_reg_field_whole reg regfield)
+  read_reg_aux (external_reg_field_whole reg regfield.field_name)
 let read_reg_bitfield reg regfield =
-  read_reg_aux (external_reg_field_whole reg regfield) >>= fun v ->
+  read_reg_aux (external_reg_field_whole reg regfield.field_name) >>= fun v ->
   return (extract_only_element v)
 
 let reg_deref = read_reg
@@ -93,12 +134,12 @@ let write_reg_bit reg i bit =
   let iN = natFromInteger i in
   write_reg_aux (external_reg_slice reg (iN,iN)) (Vector [bit] i (is_inc_of_reg reg))
 let write_reg_field reg regfield v =
-  write_reg_aux (external_reg_field_whole reg regfield) v
+  write_reg_aux (external_reg_field_whole reg regfield.field_name) v
 let write_reg_bitfield reg regfield bit =
-  write_reg_aux (external_reg_field_whole reg regfield)
+  write_reg_aux (external_reg_field_whole reg regfield.field_name)
                 (Vector [bit] 0 (is_inc_of_reg reg))
 let write_reg_field_range reg regfield i j v =
-  write_reg_aux (external_reg_field_slice reg regfield (natFromInteger i,natFromInteger j)) v
+  write_reg_aux (external_reg_field_slice reg regfield.field_name (natFromInteger i,natFromInteger j)) v
 
 
 
@@ -110,8 +151,8 @@ val footprint : M unit
 let footprint = Footprint (Done (),Nothing)
 
 
-val foreachM_inc : forall 'vars. (integer * integer * integer) -> 'vars ->
-                  (integer -> 'vars -> M 'vars) -> M 'vars
+val foreachM_inc : forall 'vars 'r. (integer * integer * integer) -> 'vars ->
+                  (integer -> 'vars -> MR 'vars 'r) -> MR 'vars 'r
 let rec foreachM_inc (i,stop,by) vars body =
   if i <= stop
   then
@@ -120,8 +161,8 @@ let rec foreachM_inc (i,stop,by) vars body =
   else return vars
 
 
-val foreachM_dec : forall 'vars. (integer * integer * integer) -> 'vars ->
-                  (integer -> 'vars -> M 'vars) -> M 'vars
+val foreachM_dec : forall 'vars 'r. (integer * integer * integer) -> 'vars ->
+                  (integer -> 'vars -> MR 'vars 'r) -> MR 'vars 'r
 let rec foreachM_dec (i,stop,by) vars body =
   if i >= stop
   then
diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
new file mode 100644
index 00000000..3919d540
--- /dev/null
+++ b/src/gen_lib/sail_operators.lem
@@ -0,0 +1,531 @@
+open import Pervasives_extra
+open import Machine_word
+open import Sail_impl_base
+open import Sail_values
+
+(*** Bit vector operations *)
+
+let bvlength = length
+
+let set_bitvector_start = set_vector_start
+let reset_bitvector_start = reset_vector_start
+
+let set_bitvector_start_to_length = set_vector_start_to_length
+
+let bitvector_concat = vector_concat
+let inline (^^^) = bitvector_concat
+
+let bitvector_subrange_inc = vector_subrange_inc
+let bitvector_subrange_dec = vector_subrange_dec
+
+let vector_subrange_bl (v, i, j) =
+  let v' = slice v i j in
+  get_elems v'
+
+let bitvector_access_inc = vector_access_inc
+let bitvector_access_dec = vector_access_dec
+let bitvector_update_pos_dec = update_pos
+let bitvector_update_dec = vector_update_dec
+
+let extract_only_bit = extract_only_element
+
+let norm_dec = reset_vector_start
+let adjust_start_index (start, v) = set_vector_start (start, v)
+
+let cast_vec_bool v = bitU_to_bool (extract_only_element v)
+let cast_bit_vec (start, len, b) = Vector (repeat [b] len) start false
+
+let pp_bitu_vector (Vector elems start inc) =
+  let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in
+  "Vector [" ^ elems_pp ^ "] " ^ show start ^ " " ^ show inc
+
+
+let most_significant = function
+  | (Vector (b :: _) _ _) -> b
+  | _ -> failwith "most_significant applied to empty vector"
+  end
+
+let bitwise_not_bitlist = List.map bitwise_not_bit
+
+let bitwise_not (Vector bs start is_inc) =
+  Vector (bitwise_not_bitlist bs) start is_inc
+
+let bitwise_binop op (Vector bsl start is_inc, Vector bsr _ _) =
+  let revbs = foldl (fun acc pair -> bitwise_binop_bit op pair :: acc) [] (zip bsl bsr) in
+  Vector (reverse revbs) start is_inc
+
+let bitwise_and = bitwise_binop (&&)
+let bitwise_or = bitwise_binop (||)
+let bitwise_xor = bitwise_binop xor
+
+let unsigned (Vector bs _ _) : integer =
+  let (sum,_) =
+    List.foldr
+      (fun b (acc,exp) ->
+        match b with
+        | B1 -> (acc + integerPow 2 exp,exp + 1)
+        | B0 -> (acc, exp + 1)
+        | BU -> failwith "unsigned: vector has undefined bits"
+        end)
+      (0,0) bs in
+  sum
+
+let unsigned_big = unsigned
+
+let signed v : integer =
+  match most_significant v with
+  | B1 -> 0 - (1 + (unsigned (bitwise_not v)))
+  | B0 -> unsigned v
+  | BU -> failwith "signed applied to vector with undefined bits"
+  end
+
+let hardware_mod (a: integer) (b:integer) : integer = 
+ if a < 0 && b < 0
+ then (abs a) mod (abs b)
+ else if (a < 0 && b >= 0) 
+ then (a mod b) - b
+ else a mod b
+
+(* There are different possible answers for integer divide regarding
+rounding behaviour on negative operands. Positive operands always
+round down so derive the one we want (trucation towards zero) from
+that *)
+let hardware_quot (a:integer) (b:integer) : integer = 
+  let q = (abs a) / (abs b) in
+  if ((a<0) = (b<0)) then
+    q  (* same sign -- result positive *)
+  else
+    ~q (* different sign -- result negative *)
+
+let quot_signed = hardware_quot
+
+
+let signed_big = signed
+
+let to_num sign = if sign then signed else unsigned
+
+let max_64u = (integerPow 2 64) - 1
+let max_64  = (integerPow 2 63) - 1
+let min_64  = 0 - (integerPow 2 63)
+let max_32u = (4294967295 : integer)
+let max_32  = (2147483647 : integer)
+let min_32  = (0 - 2147483648 : integer)
+let max_8   = (127 : integer)
+let min_8   = (0 - 128 : integer)
+let max_5   = (31 : integer)
+let min_5   = (0 - 32 : integer)
+
+let get_max_representable_in sign (n : integer) : integer =
+  if (n = 64) then match sign with | true -> max_64 | false -> max_64u end
+  else if (n=32) then match sign with | true -> max_32 | false -> max_32u end
+  else if (n=8) then max_8
+  else if (n=5) then max_5
+  else match sign with | true -> integerPow 2 ((natFromInteger n) -1)
+                       | false -> integerPow 2 (natFromInteger n)
+       end
+
+let get_min_representable_in _ (n : integer) : integer =
+  if n = 64 then min_64
+  else if n = 32 then min_32
+  else if n = 8 then min_8
+  else if n = 5 then min_5
+  else 0 - (integerPow 2 (natFromInteger n))
+
+val to_bin_aux : natural -> list bitU
+let rec to_bin_aux x =
+  if x = 0 then []
+  else (if x mod 2 = 1 then B1 else B0) :: to_bin_aux (x / 2)
+let to_bin n = List.reverse (to_bin_aux n)
+
+val pad_zero : list bitU -> integer -> list bitU
+let rec pad_zero bits n =
+  if n = 0 then bits else pad_zero (B0 :: bits) (n -1)
+
+
+let rec add_one_bit_ignore_overflow_aux bits = match bits with
+  | [] -> []
+  | B0 :: bits -> B1 :: bits
+  | B1 :: bits -> B0 :: add_one_bit_ignore_overflow_aux bits
+  | BU :: _ -> failwith "add_one_bit_ignore_overflow: undefined bit"
+end
+
+let add_one_bit_ignore_overflow bits =
+  List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits))
+  
+
+let to_vec is_inc ((len : integer),(n : integer)) =
+  let start = if is_inc then 0 else len - 1 in
+  let bits = to_bin (naturalFromInteger (abs n)) in
+  let len_bits = integerFromNat (List.length bits) in
+  let longer = len - len_bits in
+  let bits' =
+    if longer < 0 then drop (natFromInteger (abs (longer))) bits
+    else pad_zero bits longer in
+  if n > (0 : integer)
+  then Vector bits' start is_inc
+  else Vector (add_one_bit_ignore_overflow (bitwise_not_bitlist bits'))
+              start is_inc
+
+let to_vec_big = to_vec
+
+let to_vec_inc (start, len, n) = set_vector_start (start, to_vec true (len, n))
+let to_vec_norm_inc (len, n) = to_vec true (len, n)
+let to_vec_dec (start, len, n) = set_vector_start (start, to_vec false (len, n))
+let to_vec_norm_dec (len, n) = to_vec false (len, n)
+
+let cast_0_vec = to_vec_dec
+let cast_1_vec = to_vec_dec
+let cast_01_vec = to_vec_dec
+
+let to_vec_undef is_inc (len : integer) =
+  Vector (replicate (natFromInteger len) BU) (if is_inc then 0 else len-1) is_inc
+
+let to_vec_inc_undef = to_vec_undef true
+let to_vec_dec_undef = to_vec_undef false
+
+let exts (start, len, vec) = set_vector_start (start, to_vec (get_dir vec) (len,signed vec))
+let extz (start, len, vec) = set_vector_start (start, to_vec (get_dir vec) (len,unsigned vec))
+
+let exts_big (start, len, vec) = set_vector_start (start, to_vec_big (get_dir vec) (len, signed_big vec))
+let extz_big (start, len, vec) = set_vector_start (start, to_vec_big (get_dir vec) (len, unsigned_big vec))
+
+(* TODO *)
+let extz_bl (start, len, bits) = Vector bits start false
+let exts_bl (start, len, bits) = Vector bits start false
+
+
+let add (l,r) = integerAdd l r
+let add_signed (l,r) = integerAdd l r
+let sub (l,r) = integerMinus l r
+let mult (l,r) = integerMult l r
+let quotient (l,r) = integerDiv l r
+let modulo (l,r) = hardware_mod l r
+let quot = hardware_quot
+let power (l,r) = integerPow l r
+
+let sub_int = sub
+let mult_int = mult
+
+let arith_op_vec op sign (size : integer) (Vector _ _ is_inc as l) r =
+  let (l',r') = (to_num sign l, to_num sign r) in
+  let n = op l' r' in
+  to_vec is_inc (size * (length l),n)
+
+
+(* add_vec
+ * add_vec_signed
+ * minus_vec
+ * multiply_vec
+ * multiply_vec_signed
+ *)
+let add_VVV = arith_op_vec integerAdd false 1
+let addS_VVV = arith_op_vec integerAdd true 1
+let minus_VVV = arith_op_vec integerMinus false 1
+let mult_VVV = arith_op_vec integerMult false 2
+let multS_VVV = arith_op_vec integerMult true 2
+
+let mult_vec (l, r) = mult_VVV l r
+let mult_svec (l, r) = multS_VVV l r
+
+let add_vec (l, r) = add_VVV l r
+let sub_vec (l, r) = minus_VVV l r
+
+let arith_op_vec_range op sign size (Vector _ _ is_inc as l) r =
+  arith_op_vec op sign size l (to_vec is_inc (length l,r))
+
+(* add_vec_range
+ * add_vec_range_signed
+ * minus_vec_range
+ * mult_vec_range
+ * mult_vec_range_signed
+ *)
+let add_VIV = arith_op_vec_range integerAdd false 1
+let addS_VIV = arith_op_vec_range integerAdd true 1
+let minus_VIV = arith_op_vec_range integerMinus false 1
+let mult_VIV = arith_op_vec_range integerMult false 2
+let multS_VIV = arith_op_vec_range integerMult true 2
+
+let add_vec_int (l, r) = add_VIV l r
+let sub_vec_int (l, r) = minus_VIV l r
+
+let arith_op_range_vec op sign size l (Vector _ _ is_inc as r) =
+  arith_op_vec op sign size (to_vec is_inc (length r, l)) r
+
+(* add_range_vec
+ * add_range_vec_signed
+ * minus_range_vec
+ * mult_range_vec
+ * mult_range_vec_signed
+ *)
+let add_IVV = arith_op_range_vec integerAdd false 1
+let addS_IVV = arith_op_range_vec integerAdd true 1
+let minus_IVV = arith_op_range_vec integerMinus false 1
+let mult_IVV = arith_op_range_vec integerMult false 2
+let multS_IVV = arith_op_range_vec integerMult true 2
+
+let arith_op_range_vec_range op sign l r = op l (to_num sign r)
+
+(* add_range_vec_range
+ * add_range_vec_range_signed
+ * minus_range_vec_range
+ *)
+let add_IVI = arith_op_range_vec_range integerAdd false
+let addS_IVI = arith_op_range_vec_range integerAdd true
+let minus_IVI = arith_op_range_vec_range integerMinus false
+
+let arith_op_vec_range_range op sign l r = op (to_num sign l) r
+
+(* add_vec_range_range
+ * add_vec_range_range_signed
+ * minus_vec_range_range
+ *)
+let add_VII = arith_op_vec_range_range integerAdd false
+let addS_VII = arith_op_vec_range_range integerAdd true
+let minus_VII = arith_op_vec_range_range integerMinus false
+
+
+
+let arith_op_vec_vec_range op sign l r =
+  let (l',r') = (to_num sign l,to_num sign r) in
+  op l' r'
+
+(* add_vec_vec_range
+ * add_vec_vec_range_signed
+ *)
+let add_VVI = arith_op_vec_vec_range integerAdd false
+let addS_VVI = arith_op_vec_vec_range integerAdd true
+
+let arith_op_vec_bit op sign (size : integer) (Vector _ _ is_inc as l)r =
+  let l' = to_num sign l in
+  let n = op l' (match r with | B1 -> (1 : integer) | _ -> 0 end) in
+  to_vec is_inc (length l * size,n)
+
+(* add_vec_bit
+ * add_vec_bit_signed
+ * minus_vec_bit_signed
+ *)
+let add_VBV = arith_op_vec_bit integerAdd false 1
+let addS_VBV = arith_op_vec_bit integerAdd true 1
+let minus_VBV = arith_op_vec_bit integerMinus true 1
+
+let rec arith_op_overflow_vec (op : integer -> integer -> integer) sign size (Vector _ _ is_inc as l) r =
+  let len = length l in
+  let act_size = len * size in
+  let (l_sign,r_sign) = (to_num sign l,to_num sign r) in
+  let (l_unsign,r_unsign) = (to_num false l,to_num false r) in
+  let n = op l_sign r_sign in
+  let n_unsign = op l_unsign r_unsign in
+  let correct_size_num = to_vec is_inc (act_size,n) in
+  let one_more_size_u = to_vec is_inc (act_size + 1,n_unsign) in
+  let overflow =
+    if n <= get_max_representable_in sign len &&
+         n >= get_min_representable_in sign len
+    then B0 else B1 in
+  let c_out = most_significant one_more_size_u in
+  (correct_size_num,overflow,c_out)
+
+(* add_overflow_vec
+ * add_overflow_vec_signed
+ * minus_overflow_vec
+ * minus_overflow_vec_signed
+ * mult_overflow_vec
+ * mult_overflow_vec_signed
+ *)
+let addO_VVV = arith_op_overflow_vec integerAdd false 1
+let addSO_VVV = arith_op_overflow_vec integerAdd true 1
+let minusO_VVV = arith_op_overflow_vec integerMinus false 1
+let minusSO_VVV = arith_op_overflow_vec integerMinus true 1
+let multO_VVV = arith_op_overflow_vec integerMult false 2
+let multSO_VVV = arith_op_overflow_vec integerMult true 2
+
+let rec arith_op_overflow_vec_bit (op : integer -> integer -> integer) sign (size : integer)
+                                  (Vector _ _ is_inc as l) r_bit =
+  let act_size = length l * size in
+  let l' = to_num sign l in
+  let l_u = to_num false l in
+  let (n,nu,changed) = match r_bit with
+    | B1 -> (op l' 1, op l_u 1, true)
+    | B0 -> (l',l_u,false)
+    | BU -> failwith "arith_op_overflow_vec_bit applied to undefined bit"
+    end in
+(*    | _ -> assert false *)
+  let correct_size_num = to_vec is_inc (act_size,n) in
+  let one_larger = to_vec is_inc (act_size + 1,nu) in
+  let overflow =
+    if changed
+    then
+      if n <= get_max_representable_in sign act_size && n >= get_min_representable_in sign act_size
+      then B0 else B1
+    else B0 in
+  (correct_size_num,overflow,most_significant one_larger)
+
+(* add_overflow_vec_bit_signed
+ * minus_overflow_vec_bit
+ * minus_overflow_vec_bit_signed
+ *)
+let addSO_VBV = arith_op_overflow_vec_bit integerAdd true 1
+let minusO_VBV = arith_op_overflow_vec_bit integerMinus false 1
+let minusSO_VBV = arith_op_overflow_vec_bit integerMinus true 1
+
+type shift = LL_shift | RR_shift | LLL_shift
+
+let shift_op_vec op (Vector bs start is_inc,(n : integer)) =
+  let n = natFromInteger n in
+  match op with
+  | LL_shift (*"<<"*) ->
+     Vector (sublist bs (n,List.length bs -1) ++ List.replicate n B0) start is_inc
+  | RR_shift (*">>"*) ->
+     Vector (List.replicate n B0 ++ sublist bs (0,n-1)) start is_inc
+  | LLL_shift (*"<<<"*) ->
+     Vector (sublist bs (n,List.length bs - 1) ++ sublist bs (0,n-1)) start is_inc
+  end
+
+let bitwise_leftshift = shift_op_vec LL_shift (*"<<"*)
+let bitwise_rightshift = shift_op_vec RR_shift (*">>"*)
+let bitwise_rotate = shift_op_vec LLL_shift (*"<<<"*)
+
+let shiftl = bitwise_leftshift
+
+let rec arith_op_no0 (op : integer -> integer -> integer) l r =
+  if r = 0
+  then Nothing
+  else Just (op l r)
+
+let rec arith_op_vec_no0 (op : integer -> integer -> integer) sign size ((Vector _ start is_inc) as l) r =
+  let act_size = length l * size in
+  let (l',r') = (to_num sign l,to_num sign r) in
+  let n = arith_op_no0 op l' r' in
+  let (representable,n') =
+    match n with
+    | Just n' ->
+      (n' <= get_max_representable_in sign act_size &&
+         n' >= get_min_representable_in sign act_size, n')
+    | _ -> (false,0)
+    end in
+  if representable
+  then to_vec is_inc (act_size,n')
+  else Vector (List.replicate (natFromInteger act_size) BU) start is_inc
+
+let mod_VVV = arith_op_vec_no0 hardware_mod false 1
+let quot_VVV = arith_op_vec_no0 hardware_quot false 1
+let quotS_VVV = arith_op_vec_no0 hardware_quot true 1
+
+let arith_op_overflow_no0_vec op sign size ((Vector _ start is_inc) as l) r =
+  let rep_size = length r * size in
+  let act_size = length l * size in
+  let (l',r') = (to_num sign l,to_num sign r) in
+  let (l_u,r_u) = (to_num false l,to_num false r) in
+  let n = arith_op_no0 op l' r' in
+  let n_u = arith_op_no0 op l_u r_u in
+  let (representable,n',n_u') =
+    match (n, n_u) with
+    | (Just n',Just n_u') ->
+       ((n' <= get_max_representable_in sign rep_size &&
+           n' >= (get_min_representable_in sign rep_size)), n', n_u')
+    | _ -> (true,0,0)
+    end in
+  let (correct_size_num,one_more) =
+    if representable then
+      (to_vec is_inc (act_size,n'),to_vec is_inc (act_size + 1,n_u'))
+    else
+      (Vector (List.replicate (natFromInteger act_size) BU) start is_inc,
+       Vector (List.replicate (natFromInteger (act_size + 1)) BU) start is_inc) in
+  let overflow = if representable then B0 else B1 in
+  (correct_size_num,overflow,most_significant one_more)
+
+let quotO_VVV = arith_op_overflow_no0_vec hardware_quot false 1
+let quotSO_VVV = arith_op_overflow_no0_vec hardware_quot true 1
+
+let arith_op_vec_range_no0 op sign size (Vector _ _ is_inc as l) r =
+  arith_op_vec_no0 op sign size l (to_vec is_inc (length l,r))
+
+let mod_VIV = arith_op_vec_range_no0 hardware_mod false 1
+
+val repeat : forall 'a. list 'a -> integer -> list 'a
+let rec repeat xs n =
+  if n = 0 then []
+  else xs ++ repeat xs (n-1)
+
+(* Assumes decreasing bit vectors *)
+let duplicate (bit, length) =
+  Vector (repeat [bit] length) (length - 1) false
+
+let compare_op op (l,r) = (op l r)
+
+let lt = compare_op (<)
+let gt = compare_op (>)
+let lteq = compare_op (<=)
+let gteq = compare_op (>=)
+
+
+let compare_op_vec op sign (l,r) =
+  let (l',r') = (to_num sign l, to_num sign r) in
+  compare_op op (l',r')
+
+let lt_vec = compare_op_vec (<) true
+let gt_vec = compare_op_vec (>) true
+let lteq_vec = compare_op_vec (<=) true
+let gteq_vec = compare_op_vec (>=) true
+
+let lt_vec_signed = compare_op_vec (<) true
+let gt_vec_signed = compare_op_vec (>) true
+let lteq_vec_signed = compare_op_vec (<=) true
+let gteq_vec_signed = compare_op_vec (>=) true
+let lt_vec_unsigned = compare_op_vec (<) false
+let gt_vec_unsigned = compare_op_vec (>) false
+let lteq_vec_unsigned = compare_op_vec (<=) false
+let gteq_vec_unsigned = compare_op_vec (>=) false
+
+let lt_svec = lt_vec_signed
+
+let compare_op_vec_range op sign (l,r) =
+  compare_op op ((to_num sign l),r)
+
+let lt_vec_range = compare_op_vec_range (<) true
+let gt_vec_range = compare_op_vec_range (>) true
+let lteq_vec_range = compare_op_vec_range (<=) true
+let gteq_vec_range = compare_op_vec_range (>=) true
+
+let compare_op_range_vec op sign (l,r) =
+  compare_op op (l, (to_num sign r))
+
+let lt_range_vec = compare_op_range_vec (<) true
+let gt_range_vec = compare_op_range_vec (>) true
+let lteq_range_vec = compare_op_range_vec (<=) true
+let gteq_range_vec = compare_op_range_vec (>=) true
+
+val eq : forall 'a. Eq 'a => 'a * 'a -> bool
+let eq (l,r) = (l = r)
+let eq_range (l,r) = (l = r)
+
+val eq_vec : forall 'a. vector 'a * vector 'a -> bool
+let eq_vec (l,r) = (l = r)
+let eq_bit (l,r) = (l = r)
+let eq_vec_range (l,r) = eq (to_num false l,r)
+let eq_range_vec (l,r) = eq (l, to_num false r)
+let eq_vec_vec (l,r) = eq (to_num true l, to_num true r)
+
+let neq (l,r) = not (eq (l,r))
+let neq_bit (l,r) = not (eq_bit (l,r))
+let neq_range (l,r) = not (eq_range (l,r))
+let neq_vec (l,r) = not (eq_vec_vec (l,r))
+let neq_vec_range (l,r) = not (eq_vec_range (l,r))
+let neq_range_vec (l,r) = not (eq_range_vec (l,r))
+
+
+val make_indexed_vector : forall 'a. list (integer * 'a) -> 'a -> integer -> integer -> bool -> vector 'a
+let make_indexed_vector entries default start length dir =
+  let length = natFromInteger length in
+  Vector (List.foldl replace (replicate length default) entries) start dir
+
+(*
+val make_bit_vector_undef : integer -> vector bitU
+let make_bitvector_undef length =
+  Vector (replicate (natFromInteger length) BU) 0 true
+ *)
+
+(* let bitwise_not_range_bit n = bitwise_not (to_vec defaultDir n) *)
+
+let mask' (start, n, Vector bits _ dir) =
+  let current_size = List.length bits in
+  Vector (drop (current_size - (natFromInteger n)) bits) start dir
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
new file mode 100644
index 00000000..87d805f6
--- /dev/null
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -0,0 +1,571 @@
+open import Pervasives_extra
+open import Machine_word
+open import Sail_impl_base
+open import Sail_values
+
+(*** Bit vector operations *)
+
+let bvlength (Bitvector bs _ _) = integerFromNat (word_length bs)
+
+val set_bitvector_start : forall 'a. (integer * bitvector 'a) -> bitvector 'a
+let set_bitvector_start (new_start, Bitvector bs _ is_inc) =
+  Bitvector bs new_start is_inc
+
+let reset_bitvector_start v =
+  set_bitvector_start (if (bvget_dir v) then 0 else (bvlength v - 1), v)
+
+let set_bitvector_start_to_length v =
+  set_bitvector_start (bvlength v - 1, v)
+
+let bitvector_concat (Bitvector bs start is_inc, Bitvector bs' _ _) =
+  Bitvector (word_concat bs bs') start is_inc
+
+let inline (^^^) = bitvector_concat
+
+val bvslice : forall 'a 'b. bitvector 'a -> integer -> integer -> bitvector 'b
+let bvslice (Bitvector bs start is_inc) i j =
+  let iN = natFromInteger i in
+  let jN = natFromInteger j in
+  let startN = natFromInteger start in
+  let (lo,hi) = if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN) in
+  let subvector_bits = word_extract lo hi bs in
+  Bitvector subvector_bits i is_inc
+
+let bitvector_subrange_inc (v, i, j) = bvslice v i j
+let bitvector_subrange_dec (v, i, j) = bvslice v i j
+
+let vector_subrange_bl (v, i, j) =
+  let v' = slice (bvec_to_vec v) i j in
+  get_elems v'
+
+(* this is for the vector slicing introduced in vector-concat patterns: i and j
+index into the "raw data", the list of bits. Therefore getting the bit list is
+easy, but the start index has to be transformed to match the old vector start
+and the direction. *)
+val bvslice_raw : forall 'a 'b. Size 'b => bitvector 'a -> integer -> integer -> bitvector 'b
+let bvslice_raw (Bitvector bs start is_inc) i j =
+  let iN = natFromInteger i in
+  let jN = natFromInteger j in
+  let bits = word_extract iN jN bs in
+  let len = integerFromNat (word_length bits) in
+  Bitvector bits (if is_inc then 0 else len - 1) is_inc
+
+val bvupdate_aux : forall 'a 'b. bitvector 'a -> integer -> integer -> mword 'b -> bitvector 'a
+let bvupdate_aux (Bitvector bs start is_inc) i j bs' =
+  let iN = natFromInteger i in
+  let jN = natFromInteger j in
+  let startN = natFromInteger start in
+  let (lo,hi) = if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN) in
+  let bits = word_update bs lo hi bs' in
+  Bitvector bits start is_inc
+
+val bvupdate : forall 'a 'b. bitvector 'a -> integer -> integer -> bitvector 'b -> bitvector 'a
+let bvupdate v i j (Bitvector bs' _ _) =
+  bvupdate_aux v i j bs'
+
+val bvaccess : forall 'a. bitvector 'a -> integer -> bitU
+let bvaccess (Bitvector bs start is_inc) n = bool_to_bitU (
+  if is_inc then getBit bs (natFromInteger (n - start))
+  else getBit bs (natFromInteger (start - n)))
+
+val bvupdate_pos : forall 'a. Size 'a => bitvector 'a -> integer -> bitU -> bitvector 'a
+let bvupdate_pos v n b =
+  bvupdate_aux v n n ((wordFromNatural (if bitU_to_bool b then 1 else 0)) : mword ty1)
+
+let bitvector_access_inc (v, i) = bvaccess v i
+let bitvector_access_dec (v, i) = bvaccess v i
+let bitvector_update_pos_dec (v, i, b) = bvupdate_pos v i b
+let bitvector_update_dec (v, i, j, v') = bvupdate v i j v'
+
+val extract_only_bit : bitvector ty1 -> bitU
+let extract_only_bit (Bitvector elems _ _) =
+  (*let l = word_length elems in
+  if l = 1 then*)
+    bool_to_bitU (msb elems)
+  (*else if l = 0 then
+    failwith "extract_single_bit called for empty vector"
+  else
+    failwith "extract_single_bit called for vector with more bits"*)
+
+
+let norm_dec = reset_bitvector_start
+let adjust_start_index (start, v) = set_bitvector_start (start, v)
+
+let cast_vec_bool v = bitU_to_bool (extract_only_bit v)
+let cast_bit_vec (start, len, b) = vec_to_bvec (Vector [b] start false)
+
+let pp_bitu_vector (Vector elems start inc) =
+  let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in
+  "Vector [" ^ elems_pp ^ "] " ^ show start ^ " " ^ show inc
+
+
+let most_significant (Bitvector v _ _) =
+  if word_length v = 0 then
+    failwith "most_significant applied to empty vector"
+  else
+    bool_to_bitU (msb v)
+
+let bitwise_not_bitlist = List.map bitwise_not_bit
+
+let bitwise_not (Bitvector bs start is_inc) =
+  Bitvector (lNot bs) start is_inc
+
+let bitwise_binop op (Bitvector bsl start is_inc, Bitvector bsr _ _) =
+  Bitvector (op bsl bsr) start is_inc
+
+let bitwise_and = bitwise_binop lAnd
+let bitwise_or = bitwise_binop lOr
+let bitwise_xor = bitwise_binop lXor
+
+let unsigned (Bitvector bs _ _) : integer = unsignedIntegerFromWord bs
+let unsigned_big = unsigned
+
+let signed (Bitvector v _ _) : integer = signedIntegerFromWord v
+
+let hardware_mod (a: integer) (b:integer) : integer = 
+ if a < 0 && b < 0
+ then (abs a) mod (abs b)
+ else if (a < 0 && b >= 0) 
+ then (a mod b) - b
+ else a mod b
+
+(* There are different possible answers for integer divide regarding
+rounding behaviour on negative operands. Positive operands always
+round down so derive the one we want (trucation towards zero) from
+that *)
+let hardware_quot (a:integer) (b:integer) : integer = 
+  let q = (abs a) / (abs b) in
+  if ((a<0) = (b<0)) then
+    q  (* same sign -- result positive *)
+  else
+    ~q (* different sign -- result negative *)
+
+let quot_signed = hardware_quot
+
+
+let signed_big = signed
+
+let to_num sign = if sign then signed else unsigned
+
+let max_64u = (integerPow 2 64) - 1
+let max_64  = (integerPow 2 63) - 1
+let min_64  = 0 - (integerPow 2 63)
+let max_32u = (4294967295 : integer)
+let max_32  = (2147483647 : integer)
+let min_32  = (0 - 2147483648 : integer)
+let max_8   = (127 : integer)
+let min_8   = (0 - 128 : integer)
+let max_5   = (31 : integer)
+let min_5   = (0 - 32 : integer)
+
+let get_max_representable_in sign (n : integer) : integer =
+  if (n = 64) then match sign with | true -> max_64 | false -> max_64u end
+  else if (n=32) then match sign with | true -> max_32 | false -> max_32u end
+  else if (n=8) then max_8
+  else if (n=5) then max_5
+  else match sign with | true -> integerPow 2 ((natFromInteger n) -1)
+                       | false -> integerPow 2 (natFromInteger n)
+       end
+
+let get_min_representable_in _ (n : integer) : integer =
+  if n = 64 then min_64
+  else if n = 32 then min_32
+  else if n = 8 then min_8
+  else if n = 5 then min_5
+  else 0 - (integerPow 2 (natFromInteger n))
+
+val to_bin_aux : natural -> list bitU
+let rec to_bin_aux x =
+  if x = 0 then []
+  else (if x mod 2 = 1 then B1 else B0) :: to_bin_aux (x / 2)
+let to_bin n = List.reverse (to_bin_aux n)
+
+val pad_zero : list bitU -> integer -> list bitU
+let rec pad_zero bits n =
+  if n = 0 then bits else pad_zero (B0 :: bits) (n -1)
+
+
+let rec add_one_bit_ignore_overflow_aux bits = match bits with
+  | [] -> []
+  | B0 :: bits -> B1 :: bits
+  | B1 :: bits -> B0 :: add_one_bit_ignore_overflow_aux bits
+  | BU :: _ -> failwith "add_one_bit_ignore_overflow: undefined bit"
+end
+
+let add_one_bit_ignore_overflow bits =
+  List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits))
+  
+val to_vec_ord : forall 'a. Size 'a => bool -> (integer * integer) -> bitvector 'a
+let to_vec_ord is_inc ((len : integer), (n : integer)) =
+  (* Bitvector length is determined by return type *)
+  let bits = wordFromInteger n in
+  let len = integerFromNat (word_length bits) in
+  let start = if is_inc then 0 else len - 1 in
+  (*if integerFromNat (word_length bits) = len then*)
+    Bitvector bits start is_inc
+  (*else
+    failwith "Vector length mismatch in to_vec"*)
+
+let to_vec_big = to_vec_ord
+
+let to_vec_inc (start, len, n) = set_bitvector_start (start, to_vec_ord true (len, n))
+let to_vec_norm_inc (len, n) = to_vec_ord true (len, n)
+let to_vec_dec (start, len, n) = set_bitvector_start (start, to_vec_ord false (len, n))
+let to_vec_norm_dec (len, n) = to_vec_ord false (len, n)
+
+(* TODO: Think about undefined bit(vector)s *)
+let to_vec_undef is_inc (len : integer) =
+  Bitvector (failwith "undefined bitvector") (if is_inc then 0 else len-1) is_inc
+
+let to_vec_inc_undef = to_vec_undef true
+let to_vec_dec_undef = to_vec_undef false
+
+let exts (start, len, vec) = set_bitvector_start (start, to_vec_ord (bvget_dir vec) (len, signed vec))
+val extz : forall 'a 'b. Size 'b => (integer * integer * bitvector 'a) -> bitvector 'b
+let extz (start, len, vec) = set_bitvector_start (start, to_vec_ord (bvget_dir vec) (len, unsigned vec))
+
+let exts_big (start, len, vec) = set_bitvector_start (start, to_vec_big (bvget_dir vec) (len, signed_big vec))
+let extz_big (start, len, vec) = set_bitvector_start (start, to_vec_big (bvget_dir vec) (len, unsigned_big vec))
+
+(* TODO *)
+let extz_bl (start, len, bits) = set_bitvector_start (start, vec_to_bvec (Vector bits (integerFromNat (List.length bits - 1)) false))
+let exts_bl (start, len, bits) = set_bitvector_start (start, vec_to_bvec (Vector bits (integerFromNat (List.length bits - 1)) false))
+
+let add (l,r) = integerAdd l r
+let add_signed (l,r) = integerAdd l r
+let sub (l,r) = integerMinus l r
+let mult (l,r) = integerMult l r
+let quotient (l,r) = integerDiv l r
+let modulo (l,r) = hardware_mod l r
+let quot = hardware_quot
+let power (l,r) = integerPow l r
+
+let sub_int = sub
+let mult_int = mult
+
+(* TODO: this, and the definitions that use it, currently require Size for
+   to_vec, which I'd rather avoid in favour of library versions; the
+   double-size results for multiplication may be a problem *)
+let arith_op_vec op sign (size : integer) (Bitvector _ _ is_inc as l) r =
+  let (l',r') = (to_num sign l, to_num sign r) in
+  let n = op l' r' in
+  to_vec_ord is_inc (size, n)
+
+
+(* add_vec
+ * add_vec_signed
+ * minus_vec
+ * multiply_vec
+ * multiply_vec_signed
+ *)
+let add_VVV = arith_op_vec integerAdd false 1
+let addS_VVV = arith_op_vec integerAdd true 1
+let minus_VVV = arith_op_vec integerMinus false 1
+let mult_VVV = arith_op_vec integerMult false 2
+let multS_VVV = arith_op_vec integerMult true 2
+
+let mult_vec (l, r) = mult_VVV l r
+let mult_svec (l, r) = multS_VVV l r
+
+let add_vec (l, r) = add_VVV l r
+let sub_vec (l, r) = minus_VVV l r
+
+val arith_op_vec_range : forall 'a 'b. Size 'a, Size 'b => (integer -> integer -> integer) -> bool -> integer -> bitvector 'a -> integer -> bitvector 'b
+let arith_op_vec_range op sign size (Bitvector _ _ is_inc as l) r =
+  arith_op_vec op sign size l ((to_vec_ord is_inc (size, r)) : bitvector 'a)
+
+(* add_vec_range
+ * add_vec_range_signed
+ * minus_vec_range
+ * mult_vec_range
+ * mult_vec_range_signed
+ *)
+let add_VIV = arith_op_vec_range integerAdd false 1
+let addS_VIV = arith_op_vec_range integerAdd true 1
+let minus_VIV = arith_op_vec_range integerMinus false 1
+let mult_VIV = arith_op_vec_range integerMult false 2
+let multS_VIV = arith_op_vec_range integerMult true 2
+
+let add_vec_int (l, r) = add_VIV l r
+let sub_vec_int (l, r) = minus_VIV l r
+
+val arith_op_range_vec : forall 'a 'b. Size 'a, Size 'b => (integer -> integer -> integer) -> bool -> integer -> integer -> bitvector 'a -> bitvector 'b
+let arith_op_range_vec op sign size l (Bitvector _ _ is_inc as r) =
+  arith_op_vec op sign size ((to_vec_ord is_inc (size, l)) : bitvector 'a) r
+
+(* add_range_vec
+ * add_range_vec_signed
+ * minus_range_vec
+ * mult_range_vec
+ * mult_range_vec_signed
+ *)
+let add_IVV = arith_op_range_vec integerAdd false 1
+let addS_IVV = arith_op_range_vec integerAdd true 1
+let minus_IVV = arith_op_range_vec integerMinus false 1
+let mult_IVV = arith_op_range_vec integerMult false 2
+let multS_IVV = arith_op_range_vec integerMult true 2
+
+let arith_op_range_vec_range op sign l r = op l (to_num sign r)
+
+(* add_range_vec_range
+ * add_range_vec_range_signed
+ * minus_range_vec_range
+ *)
+let add_IVI = arith_op_range_vec_range integerAdd false
+let addS_IVI = arith_op_range_vec_range integerAdd true
+let minus_IVI = arith_op_range_vec_range integerMinus false
+
+let arith_op_vec_range_range op sign l r = op (to_num sign l) r
+
+(* add_vec_range_range
+ * add_vec_range_range_signed
+ * minus_vec_range_range
+ *)
+let add_VII = arith_op_vec_range_range integerAdd false
+let addS_VII = arith_op_vec_range_range integerAdd true
+let minus_VII = arith_op_vec_range_range integerMinus false
+
+
+
+let arith_op_vec_vec_range op sign l r =
+  let (l',r') = (to_num sign l,to_num sign r) in
+  op l' r'
+
+(* add_vec_vec_range
+ * add_vec_vec_range_signed
+ *)
+let add_VVI = arith_op_vec_vec_range integerAdd false
+let addS_VVI = arith_op_vec_vec_range integerAdd true
+
+let arith_op_vec_bit op sign (size : integer) (Bitvector _ _ is_inc as l) r =
+  let l' = to_num sign l in
+  let n = op l' (match r with | B1 -> (1 : integer) | _ -> 0 end) in
+  to_vec_ord is_inc (size, n)
+
+(* add_vec_bit
+ * add_vec_bit_signed
+ * minus_vec_bit_signed
+ *)
+let add_VBV = arith_op_vec_bit integerAdd false 1
+let addS_VBV = arith_op_vec_bit integerAdd true 1
+let minus_VBV = arith_op_vec_bit integerMinus true 1
+
+(* TODO: these can't be done directly in Lem because of the one_more size calculation
+val arith_op_overflow_vec : forall 'a 'b. Size 'a, Size 'b => (integer -> integer -> integer) -> bool -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b * bitU * bool
+let rec arith_op_overflow_vec op sign size (Bitvector _ _ is_inc as l) r =
+  let len = bvlength l in
+  let act_size = len * size in
+  let (l_sign,r_sign) = (to_num sign l,to_num sign r) in
+  let (l_unsign,r_unsign) = (to_num false l,to_num false r) in
+  let n = op l_sign r_sign in
+  let n_unsign = op l_unsign r_unsign in
+  let correct_size_num = to_vec_ord is_inc (act_size,n) in
+  let one_more_size_u = to_vec_ord is_inc (act_size + 1,n_unsign) in
+  let overflow =
+    if n <= get_max_representable_in sign len &&
+         n >= get_min_representable_in sign len
+    then B0 else B1 in
+  let c_out = most_significant one_more_size_u in
+  (correct_size_num,overflow,c_out)
+
+(* add_overflow_vec
+ * add_overflow_vec_signed
+ * minus_overflow_vec
+ * minus_overflow_vec_signed
+ * mult_overflow_vec
+ * mult_overflow_vec_signed
+ *)
+let addO_VVV = arith_op_overflow_vec integerAdd false 1
+let addSO_VVV = arith_op_overflow_vec integerAdd true 1
+let minusO_VVV = arith_op_overflow_vec integerMinus false 1
+let minusSO_VVV = arith_op_overflow_vec integerMinus true 1
+let multO_VVV = arith_op_overflow_vec integerMult false 2
+let multSO_VVV = arith_op_overflow_vec integerMult true 2
+
+val arith_op_overflow_vec_bit : forall 'a 'b. Size 'a, Size 'b => (integer -> integer -> integer) -> bool -> integer ->
+                                bitvector 'a -> bitU -> bitvector 'b * bitU * bool
+let rec arith_op_overflow_vec_bit (op : integer -> integer -> integer) sign (size : integer)
+                                  (Bitvector _ _ is_inc as l) r_bit =
+  let act_size = bvlength l * size in
+  let l' = to_num sign l in
+  let l_u = to_num false l in
+  let (n,nu,changed) = match r_bit with
+    | B1 -> (op l' 1, op l_u 1, true)
+    | B0 -> (l',l_u,false)
+    | BU -> failwith "arith_op_overflow_vec_bit applied to undefined bit"
+    end in
+(*    | _ -> assert false *)
+  let correct_size_num = to_vec_ord is_inc (act_size,n) in
+  let one_larger = to_vec_ord is_inc (act_size + 1,nu) in
+  let overflow =
+    if changed
+    then
+      if n <= get_max_representable_in sign act_size && n >= get_min_representable_in sign act_size
+      then B0 else B1
+    else B0 in
+  (correct_size_num,overflow,most_significant one_larger)
+
+(* add_overflow_vec_bit_signed
+ * minus_overflow_vec_bit
+ * minus_overflow_vec_bit_signed
+ *)
+let addSO_VBV = arith_op_overflow_vec_bit integerAdd true 1
+let minusO_VBV = arith_op_overflow_vec_bit integerMinus false 1
+let minusSO_VBV = arith_op_overflow_vec_bit integerMinus true 1
+*)
+type shift = LL_shift | RR_shift | LLL_shift
+
+let shift_op_vec op (Bitvector bs start is_inc,(n : integer)) =
+  let n = natFromInteger n in
+  match op with
+  | LL_shift (*"<<"*) ->
+     Bitvector (shiftLeft bs n) start is_inc
+  | RR_shift (*">>"*) ->
+     Bitvector (shiftRight bs n) start is_inc
+  | LLL_shift (*"<<<"*) ->
+     Bitvector (rotateLeft n bs) start is_inc
+  end
+
+let bitwise_leftshift = shift_op_vec LL_shift (*"<<"*)
+let bitwise_rightshift = shift_op_vec RR_shift (*">>"*)
+let bitwise_rotate = shift_op_vec LLL_shift (*"<<<"*)
+
+let shiftl = bitwise_leftshift
+
+let rec arith_op_no0 (op : integer -> integer -> integer) l r =
+  if r = 0
+  then Nothing
+  else Just (op l r)
+(* TODO
+let rec arith_op_vec_no0 (op : integer -> integer -> integer) sign size ((Bitvector _ start is_inc) as l) r =
+  let act_size = bvlength l * size in
+  let (l',r') = (to_num sign l,to_num sign r) in
+  let n = arith_op_no0 op l' r' in
+  let (representable,n') =
+    match n with
+    | Just n' ->
+      (n' <= get_max_representable_in sign act_size &&
+         n' >= get_min_representable_in sign act_size, n')
+    | _ -> (false,0)
+    end in
+  if representable
+  then to_vec_ord is_inc (act_size,n')
+  else Vector (List.replicate (natFromInteger act_size) BU) start is_inc
+
+let mod_VVV = arith_op_vec_no0 hardware_mod false 1
+let quot_VVV = arith_op_vec_no0 hardware_quot false 1
+let quotS_VVV = arith_op_vec_no0 hardware_quot true 1
+
+let arith_op_overflow_no0_vec op sign size ((Vector _ start is_inc) as l) r =
+  let rep_size = length r * size in
+  let act_size = length l * size in
+  let (l',r') = (to_num sign l,to_num sign r) in
+  let (l_u,r_u) = (to_num false l,to_num false r) in
+  let n = arith_op_no0 op l' r' in
+  let n_u = arith_op_no0 op l_u r_u in
+  let (representable,n',n_u') =
+    match (n, n_u) with
+    | (Just n',Just n_u') ->
+       ((n' <= get_max_representable_in sign rep_size &&
+           n' >= (get_min_representable_in sign rep_size)), n', n_u')
+    | _ -> (true,0,0)
+    end in
+  let (correct_size_num,one_more) =
+    if representable then
+      (to_vec_ord is_inc (act_size,n'),to_vec_ord is_inc (act_size + 1,n_u'))
+    else
+      (Vector (List.replicate (natFromInteger act_size) BU) start is_inc,
+       Vector (List.replicate (natFromInteger (act_size + 1)) BU) start is_inc) in
+  let overflow = if representable then B0 else B1 in
+  (correct_size_num,overflow,most_significant one_more)
+
+let quotO_VVV = arith_op_overflow_no0_vec hardware_quot false 1
+let quotSO_VVV = arith_op_overflow_no0_vec hardware_quot true 1
+
+let arith_op_vec_range_no0 op sign size (Vector _ _ is_inc as l) r =
+  arith_op_vec_no0 op sign size l (to_vec_ord is_inc (length l,r))
+
+let mod_VIV = arith_op_vec_range_no0 hardware_mod false 1
+*)
+
+let duplicate (bit, length) =
+  vec_to_bvec (Vector (repeat [bit] length) (length - 1) false)
+
+let compare_op op (l,r) = (op l r)
+
+let lt = compare_op (<)
+let gt = compare_op (>)
+let lteq = compare_op (<=)
+let gteq = compare_op (>=)
+
+let compare_op_vec op sign (l,r) =
+  let (l',r') = (to_num sign l, to_num sign r) in
+  compare_op op (l',r')
+
+let lt_vec = compare_op_vec (<) true
+let gt_vec = compare_op_vec (>) true
+let lteq_vec = compare_op_vec (<=) true
+let gteq_vec = compare_op_vec (>=) true
+
+let lt_vec_signed = compare_op_vec (<) true
+let gt_vec_signed = compare_op_vec (>) true
+let lteq_vec_signed = compare_op_vec (<=) true
+let gteq_vec_signed = compare_op_vec (>=) true
+let lt_vec_unsigned = compare_op_vec (<) false
+let gt_vec_unsigned = compare_op_vec (>) false
+let lteq_vec_unsigned = compare_op_vec (<=) false
+let gteq_vec_unsigned = compare_op_vec (>=) false
+
+let lt_svec = lt_vec_signed
+
+let compare_op_vec_range op sign (l,r) =
+  compare_op op ((to_num sign l),r)
+
+let lt_vec_range = compare_op_vec_range (<) true
+let gt_vec_range = compare_op_vec_range (>) true
+let lteq_vec_range = compare_op_vec_range (<=) true
+let gteq_vec_range = compare_op_vec_range (>=) true
+
+let compare_op_range_vec op sign (l,r) =
+  compare_op op (l, (to_num sign r))
+
+let lt_range_vec = compare_op_range_vec (<) true
+let gt_range_vec = compare_op_range_vec (>) true
+let lteq_range_vec = compare_op_range_vec (<=) true
+let gteq_range_vec = compare_op_range_vec (>=) true
+
+val eq : forall 'a. Eq 'a => 'a * 'a -> bool
+let eq (l,r) = (l = r)
+let eq_range (l,r) = (l = r)
+
+val eq_vec : forall 'a. bitvector 'a * bitvector 'a -> bool
+let eq_vec (l,r) = (l = r)
+let eq_bit (l,r) = (l = r)
+let eq_vec_range (l,r) = eq (to_num false l,r)
+let eq_range_vec (l,r) = eq (l, to_num false r)
+let eq_vec_vec (l,r) = eq (to_num true l, to_num true r)
+
+let neq (l,r) = not (eq (l,r))
+let neq_bit (l,r) = not (eq_bit (l,r))
+let neq_range (l,r) = not (eq_range (l,r))
+let neq_vec (l,r) = not (eq_vec_vec (l,r))
+let neq_vec_range (l,r) = not (eq_vec_range (l,r))
+let neq_range_vec (l,r) = not (eq_range_vec (l,r))
+
+
+val make_indexed_vector : forall 'a. list (integer * 'a) -> 'a -> integer -> integer -> bool -> vector 'a
+let make_indexed_vector entries default start length dir =
+  let length = natFromInteger length in
+  Vector (List.foldl replace (replicate length default) entries) start dir
+
+(*
+val make_bit_vector_undef : integer -> vector bitU
+let make_bitvector_undef length =
+  Vector (replicate (natFromInteger length) BU) 0 true
+ *)
+
+(* let bitwise_not_range_bit n = bitwise_not (to_vec_ord defaultDir n) *)
+
+(* TODO *)
+val mask : forall 'a 'b. Size 'b => (integer * integer * bitvector 'a) -> bitvector 'b
+let mask (start, _, Bitvector w _ dir) = (Bitvector (zeroExtend w) start dir)
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index eb5cdef5..eeec7440 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -17,6 +17,13 @@ let bool_xor (l, r) = xor l r
 
 let list_append (l, r) = l ++ r
 
+val repeat : forall 'a. list 'a -> integer -> list 'a
+let rec repeat xs n =
+  if n = 0 then []
+  else xs ++ repeat xs (n-1)
+
+let duplicate_to_list (bit, length) = repeat [bit] length
+
 let rec replace bs ((n : integer),b') = match bs with
   | [] -> []
   | b :: bs ->
@@ -137,17 +144,17 @@ let bool_of_dir = function
 
 (*** Vector operations *)
 
-val set_vector_start : forall 'a. integer -> vector 'a -> vector 'a
-let set_vector_start new_start (Vector bs _ is_inc) =
+val set_vector_start : forall 'a. (integer * vector 'a) -> vector 'a
+let set_vector_start (new_start, Vector bs _ is_inc) =
   Vector bs new_start is_inc
 
 let reset_vector_start v =
-  set_vector_start (if (get_dir v) then 0 else (length v - 1)) v
+  set_vector_start (if (get_dir v) then 0 else (length v - 1), v)
 
 let set_vector_start_to_length v =
-  set_vector_start (length v - 1) v
+  set_vector_start (length v - 1, v)
 
-let vector_concat (Vector bs start is_inc) (Vector bs' _ _) =
+let vector_concat (Vector bs start is_inc, Vector bs' _ _) =
   Vector (bs ++ bs') start is_inc
 
 let inline (^^) = vector_concat
@@ -173,6 +180,9 @@ let slice (Vector bs start is_inc) i j =
     sublist bs (if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN)) in
   Vector subvector_bits i is_inc
 
+let vector_subrange_inc (v, i, j) = slice v i j
+let vector_subrange_dec (v, i, j) = slice v i j
+
 (* this is for the vector slicing introduced in vector-concat patterns: i and j
 index into the "raw data", the list of bits. Therefore getting the bit list is
 easy, but the start index has to be transformed to match the old vector start
@@ -200,6 +210,9 @@ val update : forall 'a. vector 'a -> integer -> integer -> vector 'a -> vector '
 let update v i j (Vector bs' _ _) =
   update_aux v i j bs'
 
+let vector_update_inc (v, i, j, v') = update v i j v'
+let vector_update_dec (v, i, j, v') = update v i j v'
+
 val access : forall 'a. vector 'a -> integer -> 'a
 let access (Vector bs start is_inc) n =
   if is_inc then List_extra.nth bs (natFromInteger (n - start))
@@ -212,6 +225,12 @@ val update_pos : forall 'a. vector 'a -> integer -> 'a -> vector 'a
 let update_pos v n b =
   update_aux v n n [b]
 
+let extract_only_element (Vector elems _ _) = match elems with
+  | [] -> failwith "extract_only_element called for empty vector"
+  | [e] -> e
+  | _ -> failwith "extract_only_element called for vector with more elements"
+end
+
 (*** Bitvectors *)
 
 (* element list * start * has increasing direction *)
@@ -224,7 +243,6 @@ let showBitvector (Bitvector elems start inc) =
 let bvget_dir (Bitvector _ _ ord) = ord
 let bvget_start (Bitvector _ s _) = s
 let bvget_elems (Bitvector elems _ _) = elems
-let bvlength (Bitvector bs _ _) = integerFromNat (word_length bs)
 
 instance forall 'a. (Show (bitvector 'a))
   let show = showBitvector
@@ -240,581 +258,8 @@ let vec_to_bvec (Vector elems start is_inc) =
 
 (*** Vector operations *)
 
-val set_bitvector_start : forall 'a. integer -> bitvector 'a -> bitvector 'a
-let set_bitvector_start new_start (Bitvector bs _ is_inc) =
-  Bitvector bs new_start is_inc
-
-let reset_bitvector_start v =
-  set_bitvector_start (if (bvget_dir v) then 0 else (bvlength v - 1)) v
-
-let set_bitvector_start_to_length v =
-  set_bitvector_start (bvlength v - 1) v
-
-let bitvector_concat (Bitvector bs start is_inc, Bitvector bs' _ _) =
-  Bitvector (word_concat bs bs') start is_inc
-
-let norm_dec = reset_bitvector_start
-let adjust_dec = reset_bitvector_start
-
-let inline (^^^) = bitvector_concat
-
-val bvslice : forall 'a 'b. bitvector 'a -> integer -> integer -> bitvector 'b
-let bvslice (Bitvector bs start is_inc) i j =
-  let iN = natFromInteger i in
-  let jN = natFromInteger j in
-  let startN = natFromInteger start in
-  let (lo,hi) = if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN) in
-  let subvector_bits = word_extract lo hi bs in
-  Bitvector subvector_bits i is_inc
-
-let bitvector_subrange_inc (v, i, j) = bvslice v i j
-let bitvector_subrange_dec (v, i, j) = bvslice v i j
-
-let vector_subrange_bl (v, i, j) =
-  let v' = slice (bvec_to_vec v) i j in
-  get_elems v'
-
-(* this is for the vector slicing introduced in vector-concat patterns: i and j
-index into the "raw data", the list of bits. Therefore getting the bit list is
-easy, but the start index has to be transformed to match the old vector start
-and the direction. *)
-val bvslice_raw : forall 'a 'b. Size 'b => bitvector 'a -> integer -> integer -> bitvector 'b
-let bvslice_raw (Bitvector bs start is_inc) i j =
-  let iN = natFromInteger i in
-  let jN = natFromInteger j in
-  let bits = word_extract iN jN bs in
-  let len = integerFromNat (word_length bits) in
-  Bitvector bits (if is_inc then 0 else len - 1) is_inc
-
-val bvupdate_aux : forall 'a 'b. bitvector 'a -> integer -> integer -> mword 'b -> bitvector 'a
-let bvupdate_aux (Bitvector bs start is_inc) i j bs' =
-  let iN = natFromInteger i in
-  let jN = natFromInteger j in
-  let startN = natFromInteger start in
-  let (lo,hi) = if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN) in
-  let bits = word_update bs lo hi bs' in
-  Bitvector bits start is_inc
-
-val bvupdate : forall 'a 'b. bitvector 'a -> integer -> integer -> bitvector 'b -> bitvector 'a
-let bvupdate v i j (Bitvector bs' _ _) =
-  bvupdate_aux v i j bs'
-
-val bvaccess : forall 'a. bitvector 'a -> integer -> bitU
-let bvaccess (Bitvector bs start is_inc) n = bool_to_bitU (
-  if is_inc then getBit bs (natFromInteger (n - start))
-  else getBit bs (natFromInteger (start - n)))
-
-val bvupdate_pos : forall 'a. Size 'a => bitvector 'a -> integer -> bitU -> bitvector 'a
-let bvupdate_pos v n b =
-  bvupdate_aux v n n ((wordFromNatural (if bitU_to_bool b then 1 else 0)) : mword ty1)
-
-let bitvector_access_inc (v, i) = bvaccess v i
-let bitvector_access_dec (v, i) = bvaccess v i
-let bitvector_update_pos_dec (v, i, b) = bvupdate_pos v i b
-let bitvector_update_dec (v, i, j, v') = bvupdate v i j v'
-
-(*** Bit vector operations *)
-
-let extract_only_element (Vector elems _ _) = match elems with
-  | [] -> failwith "extract_only_element called for empty vector"
-  | [e] -> e
-  | _ -> failwith "extract_only_element called for vector with more elements"
-end
-
-val extract_only_bit : bitvector ty1 -> bitU
-let extract_only_bit (Bitvector elems _ _) =
-  (*let l = word_length elems in
-  if l = 1 then*)
-    bool_to_bitU (msb elems)
-  (*else if l = 0 then
-    failwith "extract_single_bit called for empty vector"
-  else
-    failwith "extract_single_bit called for vector with more bits"*)
-
-let cast_vec_bool v = bitU_to_bool (extract_only_bit v)
-let cast_bit_vec b = vec_to_bvec (Vector [b] 0 false)
-
-let pp_bitu_vector (Vector elems start inc) =
-  let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in
-  "Vector [" ^ elems_pp ^ "] " ^ show start ^ " " ^ show inc
-
-
-let most_significant (Bitvector v _ _) =
-  if word_length v = 0 then
-    failwith "most_significant applied to empty vector"
-  else
-    bool_to_bitU (msb v)
-
-let bitwise_not_bitlist = List.map bitwise_not_bit
-
-let bitwise_not (Bitvector bs start is_inc) =
-  Bitvector (lNot bs) start is_inc
-
-let bitwise_binop op (Bitvector bsl start is_inc, Bitvector bsr _ _) =
-  Bitvector (op bsl bsr) start is_inc
-
-let bitwise_and = bitwise_binop lAnd
-let bitwise_or = bitwise_binop lOr
-let bitwise_xor = bitwise_binop lXor
-
-let unsigned (Bitvector bs _ _) : integer = unsignedIntegerFromWord bs
-let unsigned_big = unsigned
-
-let signed (Bitvector v _ _) : integer = signedIntegerFromWord v
-
-let hardware_mod (a: integer) (b:integer) : integer = 
- if a < 0 && b < 0
- then (abs a) mod (abs b)
- else if (a < 0 && b >= 0) 
- then (a mod b) - b
- else a mod b
-
-(* There are different possible answers for integer divide regarding
-rounding behaviour on negative operands. Positive operands always
-round down so derive the one we want (trucation towards zero) from
-that *)
-let hardware_quot (a:integer) (b:integer) : integer = 
-  let q = (abs a) / (abs b) in
-  if ((a<0) = (b<0)) then
-    q  (* same sign -- result positive *)
-  else
-    integerNegate q (* different sign -- result negative *)
-
-let quot_signed = hardware_quot
-
-
-let signed_big = signed
-
-let to_num sign = if sign then signed else unsigned
-
-let max_64u = (integerPow 2 64) - 1
-let max_64  = (integerPow 2 63) - 1
-let min_64  = 0 - (integerPow 2 63)
-let max_32u = (4294967295 : integer)
-let max_32  = (2147483647 : integer)
-let min_32  = (0 - 2147483648 : integer)
-let max_8   = (127 : integer)
-let min_8   = (0 - 128 : integer)
-let max_5   = (31 : integer)
-let min_5   = (0 - 32 : integer)
-
-let get_max_representable_in sign (n : integer) : integer =
-  if (n = 64) then match sign with | true -> max_64 | false -> max_64u end
-  else if (n=32) then match sign with | true -> max_32 | false -> max_32u end
-  else if (n=8) then max_8
-  else if (n=5) then max_5
-  else match sign with | true -> integerPow 2 ((natFromInteger n) -1)
-                       | false -> integerPow 2 (natFromInteger n)
-       end
-
-let get_min_representable_in _ (n : integer) : integer =
-  if n = 64 then min_64
-  else if n = 32 then min_32
-  else if n = 8 then min_8
-  else if n = 5 then min_5
-  else 0 - (integerPow 2 (natFromInteger n))
-
-val to_bin_aux : natural -> list bitU
-let rec to_bin_aux x =
-  if x = 0 then []
-  else (if x mod 2 = 1 then B1 else B0) :: to_bin_aux (x / 2)
-let to_bin n = List.reverse (to_bin_aux n)
-
-val pad_zero : list bitU -> integer -> list bitU
-let rec pad_zero bits n =
-  if n = 0 then bits else pad_zero (B0 :: bits) (n -1)
-
-
-let rec add_one_bit_ignore_overflow_aux bits = match bits with
-  | [] -> []
-  | B0 :: bits -> B1 :: bits
-  | B1 :: bits -> B0 :: add_one_bit_ignore_overflow_aux bits
-  | BU :: _ -> failwith "add_one_bit_ignore_overflow: undefined bit"
-end
-
-let add_one_bit_ignore_overflow bits =
-  List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits))
-  
-let to_vec is_inc ((n : integer)) =
-  (* Bitvector length is determined by return type *)
-  let bits = wordFromInteger n in
-  let len = integerFromNat (word_length bits) in
-  let start = if is_inc then 0 else len - 1 in
-  (*if integerFromNat (word_length bits) = len then*)
-    Bitvector bits start is_inc
-  (*else
-    failwith "Vector length mismatch in to_vec"*)
-
-let to_vec_big = to_vec
-
-let to_vec_inc = to_vec true
-let to_vec_dec = to_vec false
-
-let cast_0_vec = to_vec_dec
-let cast_1_vec = to_vec_dec
-let cast_01_vec = to_vec_dec
-
-(* TODO: Think about undefined bit(vector)s *)
-let to_vec_undef is_inc (len : integer) =
-  Bitvector (failwith "undefined bitvector") (if is_inc then 0 else len-1) is_inc
-
-let to_vec_inc_undef = to_vec_undef true
-let to_vec_dec_undef = to_vec_undef false
-
-let exts (vec) = to_vec (bvget_dir vec) (signed vec)
-let extz (vec) = to_vec (bvget_dir vec) (unsigned vec)
-
-let exts_big (vec) = to_vec_big (bvget_dir vec) (signed_big vec)
-let extz_big (vec) = to_vec_big (bvget_dir vec) (unsigned_big vec)
-
-let extz_bl (bits) = vec_to_bvec (Vector bits (integerFromNat (List.length bits - 1)) false)
-
-let add (l,r) = integerAdd l r
-let add_signed (l,r) = integerAdd l r
-let sub (l,r) = integerMinus l r
-let multiply (l,r) = integerMult l r
-let quotient (l,r) = integerDiv l r
-let modulo (l,r) = hardware_mod l r
-let quot = hardware_quot
-let power (l,r) = integerPow l r
-
-let sub_int = sub
-let mul_int = multiply
-
-(* TODO: this, and the definitions that use it, currently require Size for
-   to_vec, which I'd rather avoid in favour of library versions; the
-   double-size results for multiplication may be a problem *)
-let arith_op_vec op sign (size : integer) (Bitvector _ _ is_inc as l) r =
-  let (l',r') = (to_num sign l, to_num sign r) in
-  let n = op l' r' in
-  to_vec is_inc (n)
-
-
-(* add_vec
- * add_vec_signed
- * minus_vec
- * multiply_vec
- * multiply_vec_signed
- *)
-let add_VVV = arith_op_vec integerAdd false 1
-let addS_VVV = arith_op_vec integerAdd true 1
-let minus_VVV = arith_op_vec integerMinus false 1
-let mult_VVV = arith_op_vec integerMult false 2
-let multS_VVV = arith_op_vec integerMult true 2
-
-let mul_vec (l, r) = mult_VVV l r
-let mul_svec (l, r) = multS_VVV l r
-
-let add_vec (l, r) = add_VVV l r
-let sub_vec (l, r) = minus_VVV l r
-
-val arith_op_vec_range : forall 'a 'b. Size 'a, Size 'b => (integer -> integer -> integer) -> bool -> integer -> bitvector 'a -> integer -> bitvector 'b
-let arith_op_vec_range op sign size (Bitvector _ _ is_inc as l) r =
-  arith_op_vec op sign size l ((to_vec is_inc (r)) : bitvector 'a)
-
-(* add_vec_range
- * add_vec_range_signed
- * minus_vec_range
- * mult_vec_range
- * mult_vec_range_signed
- *)
-let add_VIV = arith_op_vec_range integerAdd false 1
-let addS_VIV = arith_op_vec_range integerAdd true 1
-let minus_VIV = arith_op_vec_range integerMinus false 1
-let mult_VIV = arith_op_vec_range integerMult false 2
-let multS_VIV = arith_op_vec_range integerMult true 2
-
-let add_vec_int (l, r) = add_VIV l r
-let sub_vec_int (l, r) = minus_VIV l r
-
-val arith_op_range_vec : forall 'a 'b. Size 'a, Size 'b => (integer -> integer -> integer) -> bool -> integer -> integer -> bitvector 'a -> bitvector 'b
-let arith_op_range_vec op sign size l (Bitvector _ _ is_inc as r) =
-  arith_op_vec op sign size ((to_vec is_inc (l)) : bitvector 'a) r
-
-(* add_range_vec
- * add_range_vec_signed
- * minus_range_vec
- * mult_range_vec
- * mult_range_vec_signed
- *)
-let add_IVV = arith_op_range_vec integerAdd false 1
-let addS_IVV = arith_op_range_vec integerAdd true 1
-let minus_IVV = arith_op_range_vec integerMinus false 1
-let mult_IVV = arith_op_range_vec integerMult false 2
-let multS_IVV = arith_op_range_vec integerMult true 2
-
-let arith_op_range_vec_range op sign l r = op l (to_num sign r)
-
-(* add_range_vec_range
- * add_range_vec_range_signed
- * minus_range_vec_range
- *)
-let add_IVI = arith_op_range_vec_range integerAdd false
-let addS_IVI = arith_op_range_vec_range integerAdd true
-let minus_IVI = arith_op_range_vec_range integerMinus false
-
-let arith_op_vec_range_range op sign l r = op (to_num sign l) r
-
-(* add_vec_range_range
- * add_vec_range_range_signed
- * minus_vec_range_range
- *)
-let add_VII = arith_op_vec_range_range integerAdd false
-let addS_VII = arith_op_vec_range_range integerAdd true
-let minus_VII = arith_op_vec_range_range integerMinus false
-
-
-
-let arith_op_vec_vec_range op sign l r =
-  let (l',r') = (to_num sign l,to_num sign r) in
-  op l' r'
-
-(* add_vec_vec_range
- * add_vec_vec_range_signed
- *)
-let add_VVI = arith_op_vec_vec_range integerAdd false
-let addS_VVI = arith_op_vec_vec_range integerAdd true
-
-let arith_op_vec_bit op sign (size : integer) (Bitvector _ _ is_inc as l) r =
-  let l' = to_num sign l in
-  let n = op l' (match r with | B1 -> (1 : integer) | _ -> 0 end) in
-  to_vec is_inc (n)
-
-(* add_vec_bit
- * add_vec_bit_signed
- * minus_vec_bit_signed
- *)
-let add_VBV = arith_op_vec_bit integerAdd false 1
-let addS_VBV = arith_op_vec_bit integerAdd true 1
-let minus_VBV = arith_op_vec_bit integerMinus true 1
-
-(* TODO: these can't be done directly in Lem because of the one_more size calculation
-val arith_op_overflow_vec : forall 'a 'b. Size 'a, Size 'b => (integer -> integer -> integer) -> bool -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b * bitU * bool
-let rec arith_op_overflow_vec op sign size (Bitvector _ _ is_inc as l) r =
-  let len = bvlength l in
-  let act_size = len * size in
-  let (l_sign,r_sign) = (to_num sign l,to_num sign r) in
-  let (l_unsign,r_unsign) = (to_num false l,to_num false r) in
-  let n = op l_sign r_sign in
-  let n_unsign = op l_unsign r_unsign in
-  let correct_size_num = to_vec is_inc (act_size,n) in
-  let one_more_size_u = to_vec is_inc (act_size + 1,n_unsign) in
-  let overflow =
-    if n <= get_max_representable_in sign len &&
-         n >= get_min_representable_in sign len
-    then B0 else B1 in
-  let c_out = most_significant one_more_size_u in
-  (correct_size_num,overflow,c_out)
-
-(* add_overflow_vec
- * add_overflow_vec_signed
- * minus_overflow_vec
- * minus_overflow_vec_signed
- * mult_overflow_vec
- * mult_overflow_vec_signed
- *)
-let addO_VVV = arith_op_overflow_vec integerAdd false 1
-let addSO_VVV = arith_op_overflow_vec integerAdd true 1
-let minusO_VVV = arith_op_overflow_vec integerMinus false 1
-let minusSO_VVV = arith_op_overflow_vec integerMinus true 1
-let multO_VVV = arith_op_overflow_vec integerMult false 2
-let multSO_VVV = arith_op_overflow_vec integerMult true 2
-
-val arith_op_overflow_vec_bit : forall 'a 'b. Size 'a, Size 'b => (integer -> integer -> integer) -> bool -> integer ->
-                                bitvector 'a -> bitU -> bitvector 'b * bitU * bool
-let rec arith_op_overflow_vec_bit (op : integer -> integer -> integer) sign (size : integer)
-                                  (Bitvector _ _ is_inc as l) r_bit =
-  let act_size = bvlength l * size in
-  let l' = to_num sign l in
-  let l_u = to_num false l in
-  let (n,nu,changed) = match r_bit with
-    | B1 -> (op l' 1, op l_u 1, true)
-    | B0 -> (l',l_u,false)
-    | BU -> failwith "arith_op_overflow_vec_bit applied to undefined bit"
-    end in
-(*    | _ -> assert false *)
-  let correct_size_num = to_vec is_inc (act_size,n) in
-  let one_larger = to_vec is_inc (act_size + 1,nu) in
-  let overflow =
-    if changed
-    then
-      if n <= get_max_representable_in sign act_size && n >= get_min_representable_in sign act_size
-      then B0 else B1
-    else B0 in
-  (correct_size_num,overflow,most_significant one_larger)
-
-(* add_overflow_vec_bit_signed
- * minus_overflow_vec_bit
- * minus_overflow_vec_bit_signed
- *)
-let addSO_VBV = arith_op_overflow_vec_bit integerAdd true 1
-let minusO_VBV = arith_op_overflow_vec_bit integerMinus false 1
-let minusSO_VBV = arith_op_overflow_vec_bit integerMinus true 1
-*)
-type shift = LL_shift | RR_shift | LLL_shift
-
-let shift_op_vec op (Bitvector bs start is_inc,(n : integer)) =
-  let n = natFromInteger n in
-  match op with
-  | LL_shift (*"<<"*) ->
-     Bitvector (shiftLeft bs n) start is_inc
-  | RR_shift (*">>"*) ->
-     Bitvector (shiftRight bs n) start is_inc
-  | LLL_shift (*"<<<"*) ->
-     Bitvector (rotateLeft n bs) start is_inc
-  end
-
-let bitwise_leftshift = shift_op_vec LL_shift (*"<<"*)
-let bitwise_rightshift = shift_op_vec RR_shift (*">>"*)
-let bitwise_rotate = shift_op_vec LLL_shift (*"<<<"*)
-
-let shiftl = bitwise_leftshift
-
-let rec arith_op_no0 (op : integer -> integer -> integer) l r =
-  if r = 0
-  then Nothing
-  else Just (op l r)
-(* TODO
-let rec arith_op_vec_no0 (op : integer -> integer -> integer) sign size ((Bitvector _ start is_inc) as l) r =
-  let act_size = bvlength l * size in
-  let (l',r') = (to_num sign l,to_num sign r) in
-  let n = arith_op_no0 op l' r' in
-  let (representable,n') =
-    match n with
-    | Just n' ->
-      (n' <= get_max_representable_in sign act_size &&
-         n' >= get_min_representable_in sign act_size, n')
-    | _ -> (false,0)
-    end in
-  if representable
-  then to_vec is_inc (act_size,n')
-  else Vector (List.replicate (natFromInteger act_size) BU) start is_inc
-
-let mod_VVV = arith_op_vec_no0 hardware_mod false 1
-let quot_VVV = arith_op_vec_no0 hardware_quot false 1
-let quotS_VVV = arith_op_vec_no0 hardware_quot true 1
-
-let arith_op_overflow_no0_vec op sign size ((Vector _ start is_inc) as l) r =
-  let rep_size = length r * size in
-  let act_size = length l * size in
-  let (l',r') = (to_num sign l,to_num sign r) in
-  let (l_u,r_u) = (to_num false l,to_num false r) in
-  let n = arith_op_no0 op l' r' in
-  let n_u = arith_op_no0 op l_u r_u in
-  let (representable,n',n_u') =
-    match (n, n_u) with
-    | (Just n',Just n_u') ->
-       ((n' <= get_max_representable_in sign rep_size &&
-           n' >= (get_min_representable_in sign rep_size)), n', n_u')
-    | _ -> (true,0,0)
-    end in
-  let (correct_size_num,one_more) =
-    if representable then
-      (to_vec is_inc (act_size,n'),to_vec is_inc (act_size + 1,n_u'))
-    else
-      (Vector (List.replicate (natFromInteger act_size) BU) start is_inc,
-       Vector (List.replicate (natFromInteger (act_size + 1)) BU) start is_inc) in
-  let overflow = if representable then B0 else B1 in
-  (correct_size_num,overflow,most_significant one_more)
-
-let quotO_VVV = arith_op_overflow_no0_vec hardware_quot false 1
-let quotSO_VVV = arith_op_overflow_no0_vec hardware_quot true 1
-
-let arith_op_vec_range_no0 op sign size (Vector _ _ is_inc as l) r =
-  arith_op_vec_no0 op sign size l (to_vec is_inc (length l,r))
-
-let mod_VIV = arith_op_vec_range_no0 hardware_mod false 1
-*)
-val repeat : forall 'a. list 'a -> integer -> list 'a
-let rec repeat xs n =
-  if n = 0 then []
-  else xs ++ repeat xs (n-1)
-
-
-let duplicate (bit, length) =
-  vec_to_bvec (Vector (repeat [bit] length) (length - 1) false)
-
-let duplicate_to_list (bit, length) = repeat [bit] length
-
-let compare_op op (l,r) = (op l r)
-
-let lt = compare_op (<)
-let gt = compare_op (>)
-let lteq = compare_op (<=)
-let gteq = compare_op (>=)
-
-let compare_op_vec op sign (l,r) =
-  let (l',r') = (to_num sign l, to_num sign r) in
-  compare_op op (l',r')
-
-let lt_vec = compare_op_vec (<) true
-let gt_vec = compare_op_vec (>) true
-let lteq_vec = compare_op_vec (<=) true
-let gteq_vec = compare_op_vec (>=) true
-
-let lt_vec_signed = compare_op_vec (<) true
-let gt_vec_signed = compare_op_vec (>) true
-let lteq_vec_signed = compare_op_vec (<=) true
-let gteq_vec_signed = compare_op_vec (>=) true
-let lt_vec_unsigned = compare_op_vec (<) false
-let gt_vec_unsigned = compare_op_vec (>) false
-let lteq_vec_unsigned = compare_op_vec (<=) false
-let gteq_vec_unsigned = compare_op_vec (>=) false
-
-let lt_svec = lt_vec_signed
-
-let compare_op_vec_range op sign (l,r) =
-  compare_op op ((to_num sign l),r)
-
-let lt_vec_range = compare_op_vec_range (<) true
-let gt_vec_range = compare_op_vec_range (>) true
-let lteq_vec_range = compare_op_vec_range (<=) true
-let gteq_vec_range = compare_op_vec_range (>=) true
-
-let compare_op_range_vec op sign (l,r) =
-  compare_op op (l, (to_num sign r))
-
-let lt_range_vec = compare_op_range_vec (<) true
-let gt_range_vec = compare_op_range_vec (>) true
-let lteq_range_vec = compare_op_range_vec (<=) true
-let gteq_range_vec = compare_op_range_vec (>=) true
-
-val eq : forall 'a. Eq 'a => 'a * 'a -> bool
-let eq (l,r) = (l = r)
-let eq_range (l,r) = (l = r)
-
-val eq_vec : forall 'a. bitvector 'a * bitvector 'a -> bool
-let eq_vec (l,r) = (l = r)
-let eq_bit (l,r) = (l = r)
-let eq_vec_range (l,r) = eq (to_num false l,r)
-let eq_range_vec (l,r) = eq (l, to_num false r)
-let eq_vec_vec (l,r) = eq (to_num true l, to_num true r)
-
-let neq (l,r) = not (eq (l,r))
-let neq_bit (l,r) = not (eq_bit (l,r))
-let neq_range (l,r) = not (eq_range (l,r))
-let neq_vec (l,r) = not (eq_vec_vec (l,r))
-let neq_vec_range (l,r) = not (eq_vec_range (l,r))
-let neq_range_vec (l,r) = not (eq_range_vec (l,r))
-
-
-val make_indexed_vector : forall 'a. list (integer * 'a) -> 'a -> integer -> integer -> bool -> vector 'a
-let make_indexed_vector entries default start length dir =
-  let length = natFromInteger length in
-  Vector (List.foldl replace (replicate length default) entries) start dir
-
-(*
-val make_bit_vector_undef : integer -> vector bitU
-let make_bitvector_undef length =
-  Vector (replicate (natFromInteger length) BU) 0 true
- *)
-
-(* let bitwise_not_range_bit n = bitwise_not (to_vec defaultDir n) *)
-
-(* TODO *)
-val mask : forall 'a 'b. Size 'b => bitvector 'a -> bitvector 'b
-let mask (Bitvector w i dir) = (Bitvector (zeroExtend w) i dir)
 
+(* Bytes and addresses *)
 
 val byte_chunks : forall 'a. nat -> list 'a -> list (list 'a)
 let rec byte_chunks n list = match (n,list) with
@@ -885,11 +330,13 @@ type register =
   | RegisterPair of register * register
 
 type register_ref 'regstate 'a =
-  <| read_from : 'regstate -> 'a;
+  <| reg_name : string;
+     read_from : 'regstate -> 'a;
      write_to : 'regstate -> 'a -> 'regstate |>
 
 type field_ref 'regtype 'a =
-  <| get_field : 'regtype -> 'a;
+  <| field_name : string;
+     get_field : 'regtype -> 'a;
      set_field : 'regtype -> 'a -> 'regtype |>
 
 let name_of_reg = function
diff --git a/src/gen_lib/sail_values_word.lem b/src/gen_lib/sail_values_word.lem
deleted file mode 100644
index 048bf30a..00000000
--- a/src/gen_lib/sail_values_word.lem
+++ /dev/null
@@ -1,1030 +0,0 @@
-(* Version of sail_values.lem that uses Lem's machine words library *)
-
-open import Pervasives_extra
-open import Machine_word
-open import Sail_impl_base
-
-
-type ii = integer
-type nn = natural
-
-val pow : integer -> integer -> integer
-let pow m n = m ** (natFromInteger n)
-
-let rec replace bs ((n : integer),b') = match bs with
-  | [] -> []
-  | b :: bs ->
-     if n = 0 then b' :: bs
-              else b :: replace bs (n - 1,b')
-  end
-
-
-(*** Bits *)
-type bitU = B0 | B1 | BU
-
-let showBitU = function
-  | B0 -> "O"
-  | B1 -> "I"
-  | BU -> "U"
-end
-
-instance (Show bitU)
-  let show = showBitU
-end
-
-
-let bitU_to_bool = function
-  | B0 -> false
-  | B1  -> true
-  | BU -> failwith "to_bool applied to BU"
-  end
-
-let bit_lifted_of_bitU = function
-  | B0 -> Bitl_zero
-  | B1 -> Bitl_one
-  | BU -> Bitl_undef
-  end
-
-let bitU_of_bit = function
-  | Bitc_zero -> B0
-  | Bitc_one  -> B1
-  end
-
-let bit_of_bitU = function
-  | B0 -> Bitc_zero
-  | B1 -> Bitc_one
-  | BU -> failwith "bit_of_bitU: BU"
-  end
-
-let bitU_of_bit_lifted = function
-  | Bitl_zero -> B0
-  | Bitl_one  -> B1
-  | Bitl_undef -> BU
-  | Bitl_unknown -> failwith "bitU_of_bit_lifted Bitl_unknown"
-  end
-
-let bitwise_not_bit = function
-  | B1 -> B0
-  | B0 -> B1
-  | BU -> BU
-  end
-
-let inline (~) = bitwise_not_bit
-
-val is_one : integer -> bitU
-let is_one i =
-  if i = 1 then B1 else B0
-
-let bool_to_bitU b = if b then B1 else B0
-
-let bitwise_binop_bit op = function
-  | (BU,_) -> BU (*Do we want to do this or to respect | of I and & of B0 rules?*)
-  | (_,BU) -> BU (*Do we want to do this or to respect | of I and & of B0 rules?*)
-  | (x,y) -> bool_to_bitU (op (bitU_to_bool x) (bitU_to_bool y))
-  end
-
-val bitwise_and_bit : bitU * bitU -> bitU
-let bitwise_and_bit = bitwise_binop_bit (&&)
-
-val bitwise_or_bit : bitU * bitU -> bitU
-let bitwise_or_bit = bitwise_binop_bit (||)
-
-val bitwise_xor_bit : bitU * bitU -> bitU
-let bitwise_xor_bit = bitwise_binop_bit xor
-
-val (&.) : bitU -> bitU -> bitU
-let inline (&.) x y = bitwise_and_bit (x,y)
-
-val (|.) : bitU -> bitU -> bitU
-let inline (|.) x y = bitwise_or_bit (x,y)
-
-val (+.) : bitU -> bitU -> bitU
-let inline (+.) x y = bitwise_xor_bit (x,y)
-
-
-
-(*** Vectors *)
-
-(* element list * start * has increasing direction *)
-type vector 'a = Vector of list 'a * integer * bool
-
-let showVector (Vector elems start inc) =
-  "Vector " ^ show elems ^ " " ^ show start ^ " " ^ show inc
-
-let get_dir (Vector _ _ ord) = ord
-let get_start (Vector _ s _) = s
-let get_elems (Vector elems _ _) = elems
-let length (Vector bs _ _) = integerFromNat (length bs)
-
-instance forall 'a. Show 'a => (Show (vector 'a))
-  let show = showVector
-end
-
-let dir is_inc = if is_inc then D_increasing else D_decreasing
-let bool_of_dir = function
-  | D_increasing -> true
-  | D_decreasing -> false
-  end
-
-(*** Vector operations *)
-
-val set_vector_start : forall 'a. integer -> vector 'a -> vector 'a
-let set_vector_start new_start (Vector bs _ is_inc) =
-  Vector bs new_start is_inc
-
-let reset_vector_start v =
-  set_vector_start (if (get_dir v) then 0 else (length v - 1)) v
-
-let set_vector_start_to_length v =
-  set_vector_start (length v - 1) v
-
-let vector_concat (Vector bs start is_inc) (Vector bs' _ _) =
-  Vector (bs ++ bs') start is_inc
-
-let inline (^^) = vector_concat
-
-val sublist : forall 'a. list 'a -> (nat * nat) -> list 'a
-let sublist xs (i,j) =
-  let (toJ,_suffix) = List.splitAt (j+1) xs in
-  let (_prefix,fromItoJ) = List.splitAt i toJ in
-  fromItoJ
-
-val update_sublist : forall 'a. list 'a -> (nat * nat) -> list 'a -> list 'a
-let update_sublist xs (i,j) xs' =
-  let (toJ,suffix) = List.splitAt (j+1) xs in
-  let (prefix,_fromItoJ) = List.splitAt i toJ in
-  prefix ++ xs' ++ suffix
-
-val slice : forall 'a. vector 'a -> integer -> integer -> vector 'a
-let slice (Vector bs start is_inc) i j =
-  let iN = natFromInteger i in
-  let jN = natFromInteger j in
-  let startN = natFromInteger start in
-  let subvector_bits =
-    sublist bs (if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN)) in
-  Vector subvector_bits i is_inc
-
-(* this is for the vector slicing introduced in vector-concat patterns: i and j
-index into the "raw data", the list of bits. Therefore getting the bit list is
-easy, but the start index has to be transformed to match the old vector start
-and the direction. *)
-val slice_raw : forall 'a. vector 'a -> integer -> integer -> vector 'a
-let slice_raw (Vector bs start is_inc) i j =
-  let iN = natFromInteger i in
-  let jN = natFromInteger j in
-  let bits = sublist bs (iN,jN) in
-  let len = integerFromNat (List.length bits) in
-  Vector bits (if is_inc then 0 else len - 1) is_inc
-
-
-val update_aux : forall 'a. vector 'a -> integer -> integer -> list 'a -> vector 'a
-let update_aux (Vector bs start is_inc) i j bs' =
-  let iN = natFromInteger i in
-  let jN = natFromInteger j in
-  let startN = natFromInteger start in
-  let bits =
-    (update_sublist bs)
-      (if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN)) bs' in
-  Vector bits start is_inc
-
-val update : forall 'a. vector 'a -> integer -> integer -> vector 'a -> vector 'a
-let update v i j (Vector bs' _ _) =
-  update_aux v i j bs'
-
-val access : forall 'a. vector 'a -> integer -> 'a
-let access (Vector bs start is_inc) n =
-  if is_inc then List_extra.nth bs (natFromInteger (n - start))
-  else List_extra.nth bs (natFromInteger (start - n))
-
-val update_pos : forall 'a. vector 'a -> integer -> 'a -> vector 'a
-let update_pos v n b =
-  update_aux v n n [b]
-
-(*** Bitvectors *)
-
-(* element list * start * has increasing direction *)
-type bitvector 'a = Bitvector of mword 'a * integer * bool
-
-let showBitvector (Bitvector elems start inc) =
-  "Bitvector " ^ show elems ^ " " ^ show start ^ " " ^ show inc
-
-let bvget_dir (Bitvector _ _ ord) = ord
-let bvget_start (Bitvector _ s _) = s
-let bvget_elems (Bitvector elems _ _) = elems
-let bvlength (Bitvector bs _ _) = integerFromNat (word_length bs)
-
-instance forall 'a. Show 'a => (Show (bitvector 'a))
-  let show = showBitvector
-end
-
-(*** Vector operations *)
-
-val set_bitvector_start : forall 'a. integer -> bitvector 'a -> bitvector 'a
-let set_bitvector_start new_start (Bitvector bs _ is_inc) =
-  Bitvector bs new_start is_inc
-
-let reset_bitvector_start v =
-  set_bitvector_start (if (bvget_dir v) then 0 else (bvlength v - 1)) v
-
-let set_bitvector_start_to_length v =
-  set_bitvector_start (bvlength v - 1) v
-
-let bitvector_concat (Bitvector bs start is_inc) (Bitvector bs' _ _) =
-  Bitvector (word_concat bs bs') start is_inc
-
-let inline (^^^) = bitvector_concat
-
-val bvslice : forall 'a 'b. bitvector 'a -> integer -> integer -> bitvector 'b
-let bvslice (Bitvector bs start is_inc) i j =
-  let iN = natFromInteger i in
-  let jN = natFromInteger j in
-  let startN = natFromInteger start in
-  let (lo,hi) = if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN) in
-  let subvector_bits = word_extract lo hi bs in
-  Bitvector subvector_bits i is_inc
-
-(* this is for the vector slicing introduced in vector-concat patterns: i and j
-index into the "raw data", the list of bits. Therefore getting the bit list is
-easy, but the start index has to be transformed to match the old vector start
-and the direction. *)
-val bvslice_raw : forall 'a 'b. Size 'b => bitvector 'a -> integer -> integer -> bitvector 'b
-let bvslice_raw (Bitvector bs start is_inc) i j =
-  let iN = natFromInteger i in
-  let jN = natFromInteger j in
-  let bits = word_extract iN jN bs in
-  let len = integerFromNat (word_length bits) in
-  Bitvector bits (if is_inc then 0 else len - 1) is_inc
-
-val bvupdate_aux : forall 'a 'b. bitvector 'a -> integer -> integer -> mword 'b -> bitvector 'a
-let bvupdate_aux (Bitvector bs start is_inc) i j bs' =
-  let iN = natFromInteger i in
-  let jN = natFromInteger j in
-  let startN = natFromInteger start in
-  let (lo,hi) = if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN) in
-  let bits = word_update bs lo hi bs' in
-  Bitvector bits start is_inc
-
-val bvupdate : forall 'a. bitvector 'a -> integer -> integer -> bitvector 'a -> bitvector 'a
-let bvupdate v i j (Bitvector bs' _ _) =
-  bvupdate_aux v i j bs'
-
-(* TODO: decide between nat/natural, change either here or in machine_word *)
-val getBit' : forall 'a. mword 'a -> nat -> bool
-let getBit' w n = getBit w (naturalFromNat n)
-
-val bvaccess : forall 'a. bitvector 'a -> integer -> bool
-let bvaccess (Bitvector bs start is_inc) n =
-  if is_inc then getBit' bs (natFromInteger (n - start))
-  else getBit' bs (natFromInteger (start - n))
-
-val bvupdate_pos : forall 'a. Size 'a => bitvector 'a -> integer -> bool -> bitvector 'a
-let bvupdate_pos v n b =
-  bvupdate_aux v n n (wordFromNatural (if b then 1 else 0))
-
-(*** Bit vector operations *)
-
-let extract_only_bit (Bitvector elems _ _) =
-  let l = word_length elems in
-  if l = 1 then
-    msb elems
-  else if l = 0 then
-    failwith "extract_single_bit called for empty vector"
-  else
-    failwith "extract_single_bit called for vector with more bits"
-
-let pp_bitu_vector (Vector elems start inc) =
-  let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in
-  "Vector [" ^ elems_pp ^ "] " ^ show start ^ " " ^ show inc
-
-
-let most_significant (Bitvector v _ _) =
-  if word_length v = 0 then
-    failwith "most_significant applied to empty vector"
-  else
-    msb v
-
-let bitwise_not_bitlist = List.map bitwise_not_bit
-
-let bitwise_not (Bitvector bs start is_inc) =
-  Bitvector (lNot bs) start is_inc
-
-let bitwise_binop op (Bitvector bsl start is_inc, Bitvector bsr _ _) =
-  Bitvector (op bsl bsr) start is_inc
-
-let bitwise_and = bitwise_binop lAnd
-let bitwise_or = bitwise_binop lOr
-let bitwise_xor = bitwise_binop lXor
-
-let unsigned (Bitvector bs _ _) : integer = unsignedIntegerFromWord bs
-let unsigned_big = unsigned
-
-let signed (Bitvector v _ _) : integer = signedIntegerFromWord v
-
-let hardware_mod (a: integer) (b:integer) : integer = 
- if a < 0 && b < 0
- then (abs a) mod (abs b)
- else if (a < 0 && b >= 0) 
- then (a mod b) - b
- else a mod b
-
-(* There are different possible answers for integer divide regarding
-rounding behaviour on negative operands. Positive operands always
-round down so derive the one we want (trucation towards zero) from
-that *)
-let hardware_quot (a:integer) (b:integer) : integer = 
-  let q = (abs a) / (abs b) in
-  if ((a<0) = (b<0)) then
-    q  (* same sign -- result positive *)
-  else
-    ~q (* different sign -- result negative *)
-
-let quot_signed = hardware_quot
-
-
-let signed_big = signed
-
-let to_num sign = if sign then signed else unsigned
-
-let max_64u = (integerPow 2 64) - 1
-let max_64  = (integerPow 2 63) - 1
-let min_64  = 0 - (integerPow 2 63)
-let max_32u = (4294967295 : integer)
-let max_32  = (2147483647 : integer)
-let min_32  = (0 - 2147483648 : integer)
-let max_8   = (127 : integer)
-let min_8   = (0 - 128 : integer)
-let max_5   = (31 : integer)
-let min_5   = (0 - 32 : integer)
-
-let get_max_representable_in sign (n : integer) : integer =
-  if (n = 64) then match sign with | true -> max_64 | false -> max_64u end
-  else if (n=32) then match sign with | true -> max_32 | false -> max_32u end
-  else if (n=8) then max_8
-  else if (n=5) then max_5
-  else match sign with | true -> integerPow 2 ((natFromInteger n) -1)
-                       | false -> integerPow 2 (natFromInteger n)
-       end
-
-let get_min_representable_in _ (n : integer) : integer =
-  if n = 64 then min_64
-  else if n = 32 then min_32
-  else if n = 8 then min_8
-  else if n = 5 then min_5
-  else 0 - (integerPow 2 (natFromInteger n))
-
-val to_bin_aux : natural -> list bitU
-let rec to_bin_aux x =
-  if x = 0 then []
-  else (if x mod 2 = 1 then B1 else B0) :: to_bin_aux (x / 2)
-let to_bin n = List.reverse (to_bin_aux n)
-
-val pad_zero : list bitU -> integer -> list bitU
-let rec pad_zero bits n =
-  if n = 0 then bits else pad_zero (B0 :: bits) (n -1)
-
-
-let rec add_one_bit_ignore_overflow_aux bits = match bits with
-  | [] -> []
-  | B0 :: bits -> B1 :: bits
-  | B1 :: bits -> B0 :: add_one_bit_ignore_overflow_aux bits
-  | BU :: _ -> failwith "add_one_bit_ignore_overflow: undefined bit"
-end
-
-let add_one_bit_ignore_overflow bits =
-  List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits))
-  
-let to_vec is_inc ((len : integer),(n : integer)) =
-  let start = if is_inc then 0 else len - 1 in
-  let bits = wordFromInteger n in
-  if integerFromNat (word_length bits) = len then
-    Bitvector bits start is_inc
-  else
-    failwith "Vector length mismatch in to_vec"
-
-let to_vec_big = to_vec
-
-let to_vec_inc = to_vec true
-let to_vec_dec = to_vec false
-(* TODO??
-let to_vec_undef is_inc (len : integer) =
-  Vector (replicate (natFromInteger len) BU) (if is_inc then 0 else len-1) is_inc
-
-let to_vec_inc_undef = to_vec_undef true
-let to_vec_dec_undef = to_vec_undef false
-*)
-let exts (len, vec) = to_vec (bvget_dir vec) (len,signed vec)
-let extz (len, vec) = to_vec (bvget_dir vec) (len,unsigned vec)
-
-let exts_big (len, vec) = to_vec_big (bvget_dir vec) (len, signed_big vec)
-let extz_big (len, vec) = to_vec_big (bvget_dir vec) (len, unsigned_big vec)
-
-let add = integerAdd
-let add_signed = integerAdd
-let minus = integerMinus
-let multiply = integerMult
-let modulo = hardware_mod
-let quot = hardware_quot
-let power = integerPow
-
-(* TODO: this, and the definitions that use it, currently requires Size for
-   to_vec, which I'd rather avoid *)
-let arith_op_vec op sign (size : integer) (Bitvector _ _ is_inc as l) r =
-  let (l',r') = (to_num sign l, to_num sign r) in
-  let n = op l' r' in
-  to_vec is_inc (size * (bvlength l),n)
-
-
-(* add_vec
- * add_vec_signed
- * minus_vec
- * multiply_vec
- * multiply_vec_signed
- *)
-let add_VVV = arith_op_vec integerAdd false 1
-let addS_VVV = arith_op_vec integerAdd true 1
-let minus_VVV = arith_op_vec integerMinus false 1
-let mult_VVV = arith_op_vec integerMult false 2
-let multS_VVV = arith_op_vec integerMult true 2
-
-val arith_op_vec_range : forall 'a. Size 'a => (integer -> integer -> integer) -> bool -> integer -> bitvector 'a -> integer -> bitvector 'a
-let arith_op_vec_range op sign size (Bitvector _ _ is_inc as l) r =
-  arith_op_vec op sign size l (to_vec is_inc (bvlength l,r))
-
-(* add_vec_range
- * add_vec_range_signed
- * minus_vec_range
- * mult_vec_range
- * mult_vec_range_signed
- *)
-let add_VIV = arith_op_vec_range integerAdd false 1
-let addS_VIV = arith_op_vec_range integerAdd true 1
-let minus_VIV = arith_op_vec_range integerMinus false 1
-let mult_VIV = arith_op_vec_range integerMult false 2
-let multS_VIV = arith_op_vec_range integerMult true 2
-
-val arith_op_range_vec : forall 'a. Size 'a => (integer -> integer -> integer) -> bool -> integer -> integer -> bitvector 'a -> bitvector 'a
-let arith_op_range_vec op sign size l (Bitvector _ _ is_inc as r) =
-  arith_op_vec op sign size (to_vec is_inc (bvlength r, l)) r
-
-(* add_range_vec
- * add_range_vec_signed
- * minus_range_vec
- * mult_range_vec
- * mult_range_vec_signed
- *)
-let add_IVV = arith_op_range_vec integerAdd false 1
-let addS_IVV = arith_op_range_vec integerAdd true 1
-let minus_IVV = arith_op_range_vec integerMinus false 1
-let mult_IVV = arith_op_range_vec integerMult false 2
-let multS_IVV = arith_op_range_vec integerMult true 2
-
-let arith_op_range_vec_range op sign l r = op l (to_num sign r)
-
-(* add_range_vec_range
- * add_range_vec_range_signed
- * minus_range_vec_range
- *)
-let add_IVI = arith_op_range_vec_range integerAdd false
-let addS_IVI = arith_op_range_vec_range integerAdd true
-let minus_IVI = arith_op_range_vec_range integerMinus false
-
-let arith_op_vec_range_range op sign l r = op (to_num sign l) r
-
-(* add_vec_range_range
- * add_vec_range_range_signed
- * minus_vec_range_range
- *)
-let add_VII = arith_op_vec_range_range integerAdd false
-let addS_VII = arith_op_vec_range_range integerAdd true
-let minus_VII = arith_op_vec_range_range integerMinus false
-
-
-
-let arith_op_vec_vec_range op sign l r =
-  let (l',r') = (to_num sign l,to_num sign r) in
-  op l' r'
-
-(* add_vec_vec_range
- * add_vec_vec_range_signed
- *)
-let add_VVI = arith_op_vec_vec_range integerAdd false
-let addS_VVI = arith_op_vec_vec_range integerAdd true
-
-let arith_op_vec_bit op sign (size : integer) (Bitvector _ _ is_inc as l)r =
-  let l' = to_num sign l in
-  let n = op l' (match r with | B1 -> (1 : integer) | _ -> 0 end) in
-  to_vec is_inc (bvlength l * size,n)
-
-(* add_vec_bit
- * add_vec_bit_signed
- * minus_vec_bit_signed
- *)
-let add_VBV = arith_op_vec_bit integerAdd false 1
-let addS_VBV = arith_op_vec_bit integerAdd true 1
-let minus_VBV = arith_op_vec_bit integerMinus true 1
-
-val arith_op_overflow_vec : forall 'a. Size 'a => (integer -> integer -> integer) -> bool -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'a * bitU * bool
-let rec arith_op_overflow_vec op sign size (Bitvector _ _ is_inc as l) r =
-  let len = bvlength l in
-  let act_size = len * size in
-  let (l_sign,r_sign) = (to_num sign l,to_num sign r) in
-  let (l_unsign,r_unsign) = (to_num false l,to_num false r) in
-  let n = op l_sign r_sign in
-  let n_unsign = op l_unsign r_unsign in
-  let correct_size_num = to_vec is_inc (act_size,n) in
-  let one_more_size_u = to_vec is_inc (act_size + 1,n_unsign) in
-  let overflow =
-    if n <= get_max_representable_in sign len &&
-         n >= get_min_representable_in sign len
-    then B0 else B1 in
-  let c_out = most_significant one_more_size_u in
-  (correct_size_num,overflow,c_out)
-
-(* add_overflow_vec
- * add_overflow_vec_signed
- * minus_overflow_vec
- * minus_overflow_vec_signed
- * mult_overflow_vec
- * mult_overflow_vec_signed
- *)
-let addO_VVV = arith_op_overflow_vec integerAdd false 1
-let addSO_VVV = arith_op_overflow_vec integerAdd true 1
-let minusO_VVV = arith_op_overflow_vec integerMinus false 1
-let minusSO_VVV = arith_op_overflow_vec integerMinus true 1
-let multO_VVV = arith_op_overflow_vec integerMult false 2
-let multSO_VVV = arith_op_overflow_vec integerMult true 2
-
-val arith_op_overflow_vec_bit : forall 'a. Size 'a => (integer -> integer -> integer) -> bool -> integer ->
-                                bitvector 'a -> bitU -> bitvector 'a * bitU * bool
-let rec arith_op_overflow_vec_bit (op : integer -> integer -> integer) sign (size : integer)
-                                  (Bitvector _ _ is_inc as l) r_bit =
-  let act_size = bvlength l * size in
-  let l' = to_num sign l in
-  let l_u = to_num false l in
-  let (n,nu,changed) = match r_bit with
-    | B1 -> (op l' 1, op l_u 1, true)
-    | B0 -> (l',l_u,false)
-    | BU -> failwith "arith_op_overflow_vec_bit applied to undefined bit"
-    end in
-(*    | _ -> assert false *)
-  let correct_size_num = to_vec is_inc (act_size,n) in
-  let one_larger = to_vec is_inc (act_size + 1,nu) in
-  let overflow =
-    if changed
-    then
-      if n <= get_max_representable_in sign act_size && n >= get_min_representable_in sign act_size
-      then B0 else B1
-    else B0 in
-  (correct_size_num,overflow,most_significant one_larger)
-
-(* add_overflow_vec_bit_signed
- * minus_overflow_vec_bit
- * minus_overflow_vec_bit_signed
- *)
-let addSO_VBV = arith_op_overflow_vec_bit integerAdd true 1
-let minusO_VBV = arith_op_overflow_vec_bit integerMinus false 1
-let minusSO_VBV = arith_op_overflow_vec_bit integerMinus true 1
-
-type shift = LL_shift | RR_shift | LLL_shift
-
-let shift_op_vec op (Bitvector bs start is_inc,(n : integer)) =
-  let n = natFromInteger n in
-  match op with
-  | LL_shift (*"<<"*) ->
-     Bitvector (shiftLeft bs (naturalFromNat n)) start is_inc
-  | RR_shift (*">>"*) ->
-     Bitvector (shiftRight bs (naturalFromNat n)) start is_inc
-  | LLL_shift (*"<<<"*) ->
-     Bitvector (rotateLeft (naturalFromNat n) bs) start is_inc
-  end
-
-let bitwise_leftshift = shift_op_vec LL_shift (*"<<"*)
-let bitwise_rightshift = shift_op_vec RR_shift (*">>"*)
-let bitwise_rotate = shift_op_vec LLL_shift (*"<<<"*)
-
-let rec arith_op_no0 (op : integer -> integer -> integer) l r =
-  if r = 0
-  then Nothing
-  else Just (op l r)
-(* TODO
-let rec arith_op_vec_no0 (op : integer -> integer -> integer) sign size ((Bitvector _ start is_inc) as l) r =
-  let act_size = bvlength l * size in
-  let (l',r') = (to_num sign l,to_num sign r) in
-  let n = arith_op_no0 op l' r' in
-  let (representable,n') =
-    match n with
-    | Just n' ->
-      (n' <= get_max_representable_in sign act_size &&
-         n' >= get_min_representable_in sign act_size, n')
-    | _ -> (false,0)
-    end in
-  if representable
-  then to_vec is_inc (act_size,n')
-  else Vector (List.replicate (natFromInteger act_size) BU) start is_inc
-
-let mod_VVV = arith_op_vec_no0 hardware_mod false 1
-let quot_VVV = arith_op_vec_no0 hardware_quot false 1
-let quotS_VVV = arith_op_vec_no0 hardware_quot true 1
-
-let arith_op_overflow_no0_vec op sign size ((Vector _ start is_inc) as l) r =
-  let rep_size = length r * size in
-  let act_size = length l * size in
-  let (l',r') = (to_num sign l,to_num sign r) in
-  let (l_u,r_u) = (to_num false l,to_num false r) in
-  let n = arith_op_no0 op l' r' in
-  let n_u = arith_op_no0 op l_u r_u in
-  let (representable,n',n_u') =
-    match (n, n_u) with
-    | (Just n',Just n_u') ->
-       ((n' <= get_max_representable_in sign rep_size &&
-           n' >= (get_min_representable_in sign rep_size)), n', n_u')
-    | _ -> (true,0,0)
-    end in
-  let (correct_size_num,one_more) =
-    if representable then
-      (to_vec is_inc (act_size,n'),to_vec is_inc (act_size + 1,n_u'))
-    else
-      (Vector (List.replicate (natFromInteger act_size) BU) start is_inc,
-       Vector (List.replicate (natFromInteger (act_size + 1)) BU) start is_inc) in
-  let overflow = if representable then B0 else B1 in
-  (correct_size_num,overflow,most_significant one_more)
-
-let quotO_VVV = arith_op_overflow_no0_vec hardware_quot false 1
-let quotSO_VVV = arith_op_overflow_no0_vec hardware_quot true 1
-
-let arith_op_vec_range_no0 op sign size (Vector _ _ is_inc as l) r =
-  arith_op_vec_no0 op sign size l (to_vec is_inc (length l,r))
-
-let mod_VIV = arith_op_vec_range_no0 hardware_mod false 1
-*)
-val repeat : forall 'a. list 'a -> integer -> list 'a
-let rec repeat xs n =
-  if n = 0 then []
-  else xs ++ repeat xs (n-1)
-
-(*
-let duplicate bit length =
-  Vector (repeat [bit] length) (if dir then 0 else length - 1) dir
- *)
-
-let compare_op op (l,r) = bool_to_bitU (op l r)
-
-let lt = compare_op (<)
-let gt = compare_op (>)
-let lteq = compare_op (<=)
-let gteq = compare_op (>=)
-
-
-let compare_op_vec op sign (l,r) =
-  let (l',r') = (to_num sign l, to_num sign r) in
-  compare_op op (l',r')
-
-let lt_vec = compare_op_vec (<) true
-let gt_vec = compare_op_vec (>) true
-let lteq_vec = compare_op_vec (<=) true
-let gteq_vec = compare_op_vec (>=) true
-
-let lt_vec_signed = compare_op_vec (<) true
-let gt_vec_signed = compare_op_vec (>) true
-let lteq_vec_signed = compare_op_vec (<=) true
-let gteq_vec_signed = compare_op_vec (>=) true
-let lt_vec_unsigned = compare_op_vec (<) false
-let gt_vec_unsigned = compare_op_vec (>) false
-let lteq_vec_unsigned = compare_op_vec (<=) false
-let gteq_vec_unsigned = compare_op_vec (>=) false
-
-let compare_op_vec_range op sign (l,r) =
-  compare_op op ((to_num sign l),r)
-
-let lt_vec_range = compare_op_vec_range (<) true
-let gt_vec_range = compare_op_vec_range (>) true
-let lteq_vec_range = compare_op_vec_range (<=) true
-let gteq_vec_range = compare_op_vec_range (>=) true
-
-let compare_op_range_vec op sign (l,r) =
-  compare_op op (l, (to_num sign r))
-
-let lt_range_vec = compare_op_range_vec (<) true
-let gt_range_vec = compare_op_range_vec (>) true
-let lteq_range_vec = compare_op_range_vec (<=) true
-let gteq_range_vec = compare_op_range_vec (>=) true
-
-let eq (l,r) = bool_to_bitU (l = r)
-let eq_range (l,r) = bool_to_bitU (l = r)
-let eq_vec (l,r) = bool_to_bitU (l = r)
-let eq_bit (l,r) = bool_to_bitU (l = r)
-let eq_vec_range (l,r) = eq (to_num false l,r)
-let eq_range_vec (l,r) = eq (l, to_num false r)
-let eq_vec_vec (l,r) = eq (to_num true l, to_num true r)
-
-let neq (l,r) = bitwise_not_bit (eq (l,r))
-let neq_bit (l,r) = bitwise_not_bit (eq_bit (l,r))
-let neq_range (l,r) = bitwise_not_bit (eq_range (l,r))
-let neq_vec (l,r) = bitwise_not_bit (eq_vec_vec (l,r))
-let neq_vec_range (l,r) = bitwise_not_bit (eq_vec_range (l,r))
-let neq_range_vec (l,r) = bitwise_not_bit (eq_range_vec (l,r))
-
-
-val make_indexed_vector : forall 'a. list (integer * 'a) -> 'a -> integer -> integer -> bool -> vector 'a
-let make_indexed_vector entries default start length dir =
-  let length = natFromInteger length in
-  Vector (List.foldl replace (replicate length default) entries) start dir
-
-(*
-val make_bit_vector_undef : integer -> vector bitU
-let make_bitvector_undef length =
-  Vector (replicate (natFromInteger length) BU) 0 true
- *)
-
-(* let bitwise_not_range_bit n = bitwise_not (to_vec defaultDir n) *)
-
-let mask (n,Vector bits start dir) =
-  let current_size = List.length bits in
-  Vector (drop (current_size - (natFromInteger n)) bits) (if dir then 0 else (n-1)) dir
-
-
-val byte_chunks : forall 'a. nat -> list 'a -> list (list 'a)
-let rec byte_chunks n list = match (n,list) with
-  | (0,_) -> []
-  | (n+1, a::b::c::d::e::f::g::h::rest) -> [a;b;c;d;e;f;g;h] :: byte_chunks n rest
-  | _ -> failwith "byte_chunks not given enough bits"
-end
-
-val bitv_of_byte_lifteds : bool -> list Sail_impl_base.byte_lifted -> vector bitU
-let bitv_of_byte_lifteds dir v =
-  let bits = foldl (fun x (Byte_lifted y) -> x ++ (List.map bitU_of_bit_lifted y)) [] v in
-  let len = integerFromNat (List.length bits) in
-  Vector bits (if dir then 0 else len - 1) dir
-
-val bitv_of_bytes : bool -> list Sail_impl_base.byte -> vector bitU
-let bitv_of_bytes dir v =
-  let bits = foldl (fun x (Byte y) -> x ++ (List.map bitU_of_bit y)) [] v in
-  let len = integerFromNat (List.length bits) in
-  Vector bits (if dir then 0 else len - 1) dir
-
-
-val byte_lifteds_of_bitv : vector bitU -> list byte_lifted
-let byte_lifteds_of_bitv (Vector bits length is_inc) =
-  let bits = List.map bit_lifted_of_bitU bits in
-  byte_lifteds_of_bit_lifteds bits
-
-val bytes_of_bitv : vector bitU -> list byte
-let bytes_of_bitv (Vector bits length is_inc) =
-  let bits = List.map bit_of_bitU bits in
-  bytes_of_bits bits
-
-val bit_lifteds_of_bitUs : list bitU -> list bit_lifted
-let bit_lifteds_of_bitUs bits = List.map bit_lifted_of_bitU bits
-
-val bit_lifteds_of_bitv : vector bitU -> list bit_lifted
-let bit_lifteds_of_bitv v = bit_lifteds_of_bitUs (get_elems v)
-
-
-val address_lifted_of_bitv : vector bitU -> address_lifted
-let address_lifted_of_bitv v =
-  let byte_lifteds = byte_lifteds_of_bitv v in
-  let maybe_address_integer =
-    match (maybe_all (List.map byte_of_byte_lifted byte_lifteds)) with
-    | Just bs -> Just (integer_of_byte_list bs)
-    | _ -> Nothing
-    end in
-  Address_lifted byte_lifteds maybe_address_integer
-
-val address_of_bitv : vector bitU -> address
-let address_of_bitv v =
-  let bytes = bytes_of_bitv v in
-  address_of_byte_list bytes
-
-
-
-(*** Registers *)
-
-type register_field = string
-type register_field_index = string * (integer * integer) (* name, start and end *)
-
-type register =
-  | Register of string * (* name *)
-                integer * (* length *)
-                integer * (* start index *)
-                bool * (* is increasing *)
-                  list register_field_index
-  | UndefinedRegister of integer (* length *)
-  | RegisterPair of register * register
-
-let name_of_reg = function
-  | Register name _ _ _ _ -> name
-  | UndefinedRegister _ -> failwith "name_of_reg UndefinedRegister"
-  | RegisterPair _ _ -> failwith "name_of_reg RegisterPair"
-end
-
-let size_of_reg = function
-  | Register _ size _ _ _ -> size
-  | UndefinedRegister size -> size
-  | RegisterPair _ _ -> failwith "size_of_reg RegisterPair"
-end
-                              
-let start_of_reg = function
-  | Register _ _ start _ _ -> start
-  | UndefinedRegister _ -> failwith "start_of_reg UndefinedRegister"
-  | RegisterPair _ _ -> failwith "start_of_reg RegisterPair"
-end
-
-let is_inc_of_reg = function
-  | Register _ _ _ is_inc _ -> is_inc
-  | UndefinedRegister _ -> failwith "is_inc_of_reg UndefinedRegister"
-  | RegisterPair _ _ -> failwith "in_inc_of_reg RegisterPair"
-end
-
-let dir_of_reg = function
-  | Register _ _ _ is_inc _ -> dir is_inc
-  | UndefinedRegister _ -> failwith "dir_of_reg UndefinedRegister"
-  | RegisterPair _ _ -> failwith "dir_of_reg RegisterPair"
-end
-
-let size_of_reg_nat reg = natFromInteger (size_of_reg reg)
-let start_of_reg_nat reg = natFromInteger (start_of_reg reg)
-
-val register_field_indices_aux : register -> register_field -> maybe (integer * integer)
-let rec register_field_indices_aux register rfield =
-  match register with
-  | Register _ _ _ _ rfields -> List.lookup rfield rfields
-  | RegisterPair r1 r2 ->
-      let m_indices = register_field_indices_aux r1 rfield in
-      if isJust m_indices then m_indices else register_field_indices_aux r2 rfield
-  | UndefinedRegister _ -> Nothing
-  end
-
-val register_field_indices : register -> register_field -> integer * integer
-let register_field_indices register rfield =
-  match register_field_indices_aux register rfield with
-  | Just indices -> indices
-  | Nothing -> failwith "Invalid register/register-field combination"
-  end
-
-let register_field_indices_nat reg regfield=
-  let (i,j) = register_field_indices reg regfield in
-  (natFromInteger i,natFromInteger j)
-
-let rec external_reg_value reg_name v = 
-  let (internal_start, external_start, direction) =
-    match reg_name with 
-     | Reg _ start size dir ->
-        (start, (if dir = D_increasing then start else (start - (size +1))), dir)
-     | Reg_slice _ reg_start dir (slice_start, slice_end) ->
-        ((if dir = D_increasing then slice_start else (reg_start - slice_start)),
-         slice_start, dir)
-     | Reg_field _ reg_start dir _ (slice_start, slice_end) ->
-        ((if dir = D_increasing then slice_start else (reg_start - slice_start)),
-         slice_start, dir)
-     | Reg_f_slice _ reg_start dir _ _ (slice_start, slice_end) ->
-        ((if dir = D_increasing then slice_start else (reg_start - slice_start)),
-         slice_start, dir) 
-     end in
-  let bits = bit_lifteds_of_bitv v in
-  <| rv_bits           = bits; 
-     rv_dir            = direction;
-     rv_start          = external_start;
-     rv_start_internal = internal_start |>
-
-val internal_reg_value : register_value -> vector bitU
-let internal_reg_value v =
-  Vector (List.map bitU_of_bit_lifted v.rv_bits)
-         (integerFromNat v.rv_start_internal)
-         (v.rv_dir = D_increasing)
-
-
-let external_slice (d:direction) (start:nat) ((i,j):(nat*nat)) =
-  match d with
-  (*This is the case the thread/concurrecny model expects, so no change needed*)
-  | D_increasing -> (i,j)
-  | D_decreasing -> let slice_i = start - i in 
-                    let slice_j = (i - j) + slice_i in
-                    (slice_i,slice_j)
-  end 
-
-let external_reg_whole reg =
-  Reg (name_of_reg reg) (start_of_reg_nat reg) (size_of_reg_nat reg) (dir_of_reg reg)
-      
-let external_reg_slice reg (i,j) =
-  let start = start_of_reg_nat reg in
-  let dir = dir_of_reg reg in
-  Reg_slice (name_of_reg reg) start dir (external_slice dir start (i,j))
-
-let external_reg_field_whole reg rfield = 
-  let (m,n) = register_field_indices_nat reg rfield in
-  let start = start_of_reg_nat reg in
-  let dir = dir_of_reg reg in
-  Reg_field (name_of_reg reg) start dir rfield (external_slice dir start (m,n))
-            
-let external_reg_field_slice reg rfield (i,j) = 
-  let (m,n) = register_field_indices_nat reg rfield in
-  let start = start_of_reg_nat reg in
-  let dir = dir_of_reg reg in
-  Reg_f_slice (name_of_reg reg) start dir rfield
-              (external_slice dir start (m,n))
-              (external_slice dir start (i,j))
-
-let external_mem_value v =
-  byte_lifteds_of_bitv v $> List.reverse
-
-let internal_mem_value direction bytes =
-  List.reverse bytes $> bitv_of_byte_lifteds direction
-
-
-
-                       
-
-val foreach_inc :  forall 'vars. (integer * integer * integer) -> 'vars ->
-                   (integer -> 'vars -> 'vars) -> 'vars
-let rec foreach_inc (i,stop,by) vars body =
-  if i <= stop
-  then let vars = body i vars in
-       foreach_inc (i + by,stop,by) vars body
-  else vars
-
-val foreach_dec : forall 'vars. (integer * integer * integer) -> 'vars ->
-                  (integer -> 'vars -> 'vars) -> 'vars
-let rec foreach_dec (i,stop,by) vars body =
-  if i >= stop
-  then let vars = body i vars in
-       foreach_dec (i - by,stop,by) vars body
-  else vars
-
-let assert' b msg_opt =
-  let msg = match msg_opt with
-  | Just msg -> msg
-  | Nothing  -> "unspecified error"
-  end in
-  if bitU_to_bool b then () else failwith msg
-
-(* convert numbers unsafely to naturals *)
-
-class (ToNatural 'a) val toNatural : 'a -> natural end
-(* eta-expanded for Isabelle output, otherwise it breaks *)
-instance (ToNatural integer) let toNatural = (fun n -> naturalFromInteger n) end
-instance (ToNatural int)     let toNatural = (fun n -> naturalFromInt n)     end
-instance (ToNatural nat)     let toNatural = (fun n -> naturalFromNat n)     end
-instance (ToNatural natural) let toNatural = (fun n -> n)                    end
-
-let toNaturalFiveTup (n1,n2,n3,n4,n5) =
-  (toNatural n1,
-   toNatural n2,
-   toNatural n3,
-   toNatural n4,
-   toNatural n5)
-
-
-type regfp =
-  | RFull of (string)
-  | RSlice of (string * integer * integer)
-  | RSliceBit of (string * integer)
-  | RField of (string * string)
-
-type niafp = 
-  | NIAFP_successor
-  | NIAFP_concrete_address of vector bitU
-  | NIAFP_LR
-  | NIAFP_CTR
-  | NIAFP_register of regfp
-
-(* only for MIPS *)
-type diafp = 
-  | DIAFP_none
-  | DIAFP_concrete of vector bitU
-  | DIAFP_reg of regfp
-
-let regfp_to_reg (reg_info : string -> maybe string -> (nat * nat * direction * (nat * nat))) = function
-  | RFull name -> 
-     let (start,length,direction,_) = reg_info name Nothing in
-     Reg name start length direction
-  | RSlice (name,i,j) ->
-     let i = natFromInteger i in
-     let j = natFromInteger j in
-     let (start,length,direction,_) = reg_info name Nothing in
-     let slice = external_slice direction start (i,j) in
-     Reg_slice name start direction slice
-  | RSliceBit (name,i) ->
-     let i = natFromInteger i in
-     let (start,length,direction,_) = reg_info name Nothing in
-     let slice = external_slice direction start (i,i) in
-     Reg_slice name start direction slice
-  | RField (name,field_name) ->
-     let (start,length,direction,span) = reg_info name (Just field_name) in
-     let slice = external_slice direction start span in
-     Reg_field name start direction field_name slice
-end
-
-let niafp_to_nia reginfo = function
-  | NIAFP_successor -> NIA_successor
-  | NIAFP_concrete_address v -> NIA_concrete_address (address_of_bitv v)
-  | NIAFP_LR -> NIA_LR
-  | NIAFP_CTR -> NIA_CTR
-  | NIAFP_register r -> NIA_register (regfp_to_reg reginfo r)
-end
-
-let diafp_to_dia reginfo = function
-  | DIAFP_none -> DIA_none
-  | DIAFP_concrete v -> DIA_concrete_address (address_of_bitv v)
-  | DIAFP_reg r -> DIA_register (regfp_to_reg reginfo r)
-end
-
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 3cbcd4c8..4543bbcf 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -1,6 +1,7 @@
 open import Pervasives_extra
 open import Sail_impl_base
 open import Sail_values
+open import Sail_operators_mwords
 
 (* 'a is result type *)