Merge branch 'experiments' into mono-experiments

9 files changed, 449 insertions, 243 deletions

diff --git a/src/Makefile b/src/Makefile
index 1bac0b71..d0001868 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -125,10 +125,14 @@ _build/mips.lem: $(MIPS_SAILS) ./sail.native
 	cd _build ;\
 	../sail.native -lem_ast -o mips $(MIPS_SAILS)
 
-_build/mips_embed_types.lem: $(MIPS_SAILS) ./sail.native
+_build/mips_embed_types.lem: $(MIPS_NOTLB_SAILS) ./sail.native
 	mkdir -p _build
 	cd _build ;\
-	../sail.native -lem_lib "Mips_extras_embed" -lem -o mips $(MIPS_NOTLB_SAILS)
+	../sail.native -lem_lib "Mips_extras_embed" -lem -lem_mwords -o mips $(MIPS_NOTLB_SAILS)
+
+_build/Mips_embed.thy: _build/mips_embed_types.lem
+	cd _build ;\
+	lem -isa -outdir . -lib ../lem_interp -lib ../gen_lib $(MIPS_SAIL_DIR)/mips_extras_embed.lem mips_embed_types.lem mips_embed.lem
 
 _build/mips_notlb.lem: $(MIPS_NOTLB_SAILS) ./sail.native
 	mkdir -p _build
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 8e04bd30..f5ac8fc5 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -73,12 +73,12 @@ let rec catch_early_return m = match m with
   | Return a ->            Done a
 end
 
-val read_mem : bool -> read_kind -> vector bitU -> integer -> M (vector bitU)
+val read_mem : forall 'a 'b. Bitvector 'a, Bitvector 'b => bool -> read_kind -> 'a -> integer -> M 'b
 let read_mem dir rk addr sz =
-  let addr = address_lifted_of_bitv addr in
+  let addr = address_lifted_of_bitv (bits_of addr) in
   let sz = natFromInteger sz in
   let k memory_value =
-    let bitv = internal_mem_value dir memory_value in
+    let bitv = of_bits (internal_mem_value dir memory_value) in
     (Done bitv,Nothing) in
   Read_mem (rk,addr,sz) k
 
@@ -87,22 +87,22 @@ let excl_result () =
   let k successful = (return successful,Nothing) in
   Excl_res k
 
-val write_mem_ea : write_kind -> vector bitU -> integer -> M unit
+val write_mem_ea : forall 'a. Bitvector 'a => write_kind -> 'a -> integer -> M unit
 let write_mem_ea wk addr sz =
-  let addr = address_lifted_of_bitv addr in
+  let addr = address_lifted_of_bitv (bits_of addr) in
   let sz = natFromInteger sz in
   Write_ea (wk,addr,sz) (Done (),Nothing)
 
-val write_mem_val : vector bitU -> M bool
+val write_mem_val : forall 'a. Bitvector 'a => 'a -> M bool
 let write_mem_val v =
-  let v = external_mem_value v in
+  let v = external_mem_value (bits_of v) in
   let k successful = (return successful,Nothing) in
   Write_memv v k
 
-val read_reg_aux : reg_name -> M (vector bitU)
+val read_reg_aux : forall 'a. Bitvector 'a => reg_name -> M 'a
 let read_reg_aux reg = 
   let k reg_value =
-    let v = internal_reg_value reg_value in
+    let v = of_bits (internal_reg_value reg_value) in
     (Done v,Nothing) in
   Read_reg reg k
 
@@ -121,25 +121,29 @@ let read_reg_bitfield reg regfield =
 
 let reg_deref = read_reg
 
-val write_reg_aux : reg_name -> vector bitU -> M unit
+val write_reg_aux : forall 'a. Bitvector 'a => reg_name -> 'a -> M unit
 let write_reg_aux reg_name v =
-  let regval = external_reg_value reg_name v in
+  let regval = external_reg_value reg_name (bits_of v) in
   Write_reg (reg_name,regval) (Done (), Nothing)
 
 let write_reg reg v =
   write_reg_aux (external_reg_whole reg) v
 let write_reg_range reg i j v =
   write_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger j)) v
-let write_reg_bit reg i bit =
+let write_reg_pos reg i v =
   let iN = natFromInteger i in
-  write_reg_aux (external_reg_slice reg (iN,iN)) (Vector [bit] i (is_inc_of_reg reg))
+  write_reg_aux (external_reg_slice reg (iN,iN)) [v]
+let write_reg_bit = write_reg_pos
 let write_reg_field reg regfield v =
   write_reg_aux (external_reg_field_whole reg regfield.field_name) v
-let write_reg_bitfield reg regfield bit =
+(*let write_reg_field_bit reg regfield bit =
   write_reg_aux (external_reg_field_whole reg regfield.field_name)
-                (Vector [bit] 0 (is_inc_of_reg reg))
+                (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.field_name (natFromInteger i,natFromInteger j)) v
+let write_reg_field_pos reg regfield i v =
+  write_reg_field_range reg regfield i i [v]
+let write_reg_field_bit = write_reg_field_pos
 
 
 
@@ -199,7 +203,7 @@ let rec while_MM is_while vars cond body =
   then body vars >>= fun vars -> while_MM is_while vars cond body
   else return vars
 
-let write_two_regs r1 r2 vec =
+(*let write_two_regs r1 r2 vec =
   let is_inc =
     let is_inc_r1 = is_inc_of_reg r1 in
     let is_inc_r2 = is_inc_of_reg r2 in
@@ -218,4 +222,4 @@ let write_two_regs r1 r2 vec =
     if is_inc
     then slice vec (size_r1 - start_vec) (size_vec - start_vec)
     else slice vec (start_vec - size_r1) (start_vec - size_vec) in
-  write_reg r1 r1_v >> write_reg r2 r2_v
+  write_reg r1 r1_v >> write_reg r2 r2_v*)
diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index a760fb42..7b117726 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail_operators.lem
@@ -18,14 +18,15 @@ 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 vector_subrange_bl (start, v, i, j) =
   let v' = slice v i j in
   get_elems v'
+let vector_subrange_bl_dec = vector_subrange_bl
 
 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 bitvector_update_subrange_dec = vector_update_dec
 
 let extract_only_bit = extract_only_element
 
@@ -60,7 +61,7 @@ let bitwise_and = bitwise_binop (&&)
 let bitwise_or = bitwise_binop (||)
 let bitwise_xor = bitwise_binop xor
 
-let unsigned (Vector bs _ _) : integer =
+(*let unsigned (Vector bs _ _) : integer =
   let (sum,_) =
     List.foldr
       (fun b (acc,exp) ->
@@ -70,7 +71,7 @@ let unsigned (Vector bs _ _) : integer =
         | BU -> failwith "unsigned: vector has undefined bits"
         end)
       (0,0) bs in
-  sum
+  sum*)
 
 let unsigned_big = unsigned
 
@@ -155,7 +156,7 @@ 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 to_norm_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
@@ -168,12 +169,12 @@ let to_vec is_inc ((len : integer),(n : integer)) =
   else Vector (add_one_bit_ignore_overflow (bitwise_not_bitlist bits'))
               start is_inc
 
-let to_vec_big = to_vec
+let to_vec_big = to_norm_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 to_vec_inc (start, len, n) = set_vector_start (start, to_norm_vec true (len, n))
+let to_vec_norm_inc (len, n) = to_norm_vec true (len, n)
+let to_vec_dec (start, len, n) = set_vector_start (start, to_norm_vec false (len, n))
+let to_vec_norm_dec (len, n) = to_norm_vec false (len, n)
 
 let cast_0_vec = to_vec_dec
 let cast_1_vec = to_vec_dec
@@ -185,8 +186,8 @@ let to_vec_undef is_inc (len : integer) =
 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 (start, len, vec) = set_vector_start (start, to_norm_vec (get_dir vec) (len,signed vec))
+let extz (start, len, vec) = set_vector_start (start, to_norm_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))
@@ -212,7 +213,7 @@ 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)
+  to_norm_vec is_inc (size * (length l),n)
 
 
 (* add_vec
@@ -234,7 +235,7 @@ 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))
+  arith_op_vec op sign size l (to_norm_vec is_inc (length l,r))
 
 (* add_vec_range
  * add_vec_range_signed
@@ -252,7 +253,7 @@ 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
+  arith_op_vec op sign size (to_norm_vec is_inc (length r, l)) r
 
 (* add_range_vec
  * add_range_vec_signed
@@ -301,7 +302,7 @@ 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)
+  to_norm_vec is_inc (length l * size,n)
 
 (* add_vec_bit
  * add_vec_bit_signed
@@ -318,8 +319,8 @@ let rec arith_op_overflow_vec (op : integer -> integer -> integer) sign size (Ve
   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 correct_size_num = to_norm_vec is_inc (act_size,n) in
+  let one_more_size_u = to_norm_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
@@ -352,8 +353,8 @@ let rec arith_op_overflow_vec_bit (op : integer -> integer -> integer) sign (siz
     | 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 correct_size_num = to_norm_vec is_inc (act_size,n) in
+  let one_larger = to_norm_vec is_inc (act_size + 1,nu) in
   let overflow =
     if changed
     then
@@ -406,7 +407,7 @@ let rec arith_op_vec_no0 (op : integer -> integer -> integer) sign size ((Vector
     | _ -> (false,0)
     end in
   if representable
-  then to_vec is_inc (act_size,n')
+  then to_norm_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
@@ -429,7 +430,7 @@ let arith_op_overflow_no0_vec op sign size ((Vector _ start is_inc) as l) r =
     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'))
+      (to_norm_vec is_inc (act_size,n'),to_norm_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
@@ -440,7 +441,7 @@ 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))
+  arith_op_vec_no0 op sign size l (to_norm_vec is_inc (length l,r))
 
 let mod_VIV = arith_op_vec_range_no0 hardware_mod false 1
 
@@ -514,7 +515,8 @@ 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 (l,r) = not (eq_vec (l,r))
+let neq_vec_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))
 
@@ -532,20 +534,20 @@ let make_bitvector_undef length =
 
 (* let bitwise_not_range_bit n = bitwise_not (to_vec defaultDir n) *)
 
-let mask' (start, n, Vector bits _ dir) =
+let mask (start, n, Vector bits _ dir) =
   let current_size = List.length bits in
   Vector (drop (current_size - (natFromInteger n)) bits) start dir
 
 
 (* Register operations *)
 
-let update_reg_range i j reg_val new_val = update reg_val i j new_val
-let update_reg_bit i reg_val bit = update_pos reg_val i bit
+(*let update_reg_range i j reg_val new_val = update reg_val i j new_val
+let update_reg_pos i reg_val bit = update_pos reg_val i bit
 let update_reg_field_range regfield i j reg_val new_val =
   let current_field_value = regfield.get_field reg_val in
   let new_field_value = update current_field_value i j new_val in
   regfield.set_field reg_val new_field_value
-let write_reg_field_bit regfield i reg_val bit =
+(*let write_reg_field_pos regfield i reg_val bit =
   let current_field_value = regfield.get_field reg_val in
   let new_field_value = update_pos current_field_value i bit in
-  regfield.set_field reg_val new_field_value
+  regfield.set_field reg_val new_field_value*)*)
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index f10ed9f7..63c9bfcc 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -5,9 +5,9 @@ open import Sail_values
 
 (*** Bit vector operations *)
 
-let bvlength (Bitvector bs _ _) = integerFromNat (word_length bs)
+let bvlength bs = integerFromNat (word_length bs)
 
-val set_bitvector_start : forall 'a. (integer * bitvector 'a) -> bitvector 'a
+(*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
 
@@ -18,25 +18,26 @@ 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
+  Bitvector (word_concat bs bs') start is_inc*)
+
+let bitvector_concat (bs, bs') = word_concat bs bs'
 
 let inline (^^^) = bitvector_concat
 
-val bvslice : forall 'a 'b. Size 'a => bitvector 'a -> integer -> integer -> bitvector 'b
-let bvslice (Bitvector bs start is_inc) i j =
+val bvslice : forall 'a 'b. Size 'a => bool -> integer -> bitvector 'a -> integer -> integer -> bitvector 'b
+let bvslice is_inc start bs i j =
   let iN = natFromInteger i in
   let jN = natFromInteger j in
   let startN = natFromInteger start in
   let top = word_length bs - 1 in
   let (hi,lo) = if is_inc then (top+startN-iN,top+startN-jN) else (top-startN+iN,top-startN+jN) in
-  let subvector_bits = word_extract lo hi bs in
-  Bitvector subvector_bits i is_inc
+  word_extract lo hi bs
 
-let bitvector_subrange_inc (v, i, j) = bvslice v i j
-let bitvector_subrange_dec (v, i, j) = bvslice v i j
+let bitvector_subrange_inc (start, v, i, j) = bvslice true start v i j
+let bitvector_subrange_dec (start, v, i, j) = bvslice false start v i j
 
-let vector_subrange_bl (v, i, j) =
-  let v' = slice (bvec_to_vec v) i j in
+let vector_subrange_bl_dec (start, v, i, j) =
+  let v' = slice (bvec_to_vec false start v) i j in
   get_elems v'
 
 (* this is for the vector slicing introduced in vector-concat patterns: i and j
@@ -44,55 +45,56 @@ 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 bvslice_raw bs i j =
   let iN = natFromInteger i in
   let jN = natFromInteger j in
-  let bits = word_extract iN jN bs 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
+  Bitvector bits (if is_inc then 0 else len - 1) is_inc*)
 
-val bvupdate_aux : forall 'a 'b. Size 'a => bitvector 'a -> integer -> integer -> mword 'b -> bitvector 'a
-let bvupdate_aux (Bitvector bs start is_inc) i j bs' =
-  let iN = natFromInteger i in
+val bvupdate_aux : forall 'a 'b. Size 'a => bool -> integer -> bitvector 'a -> integer -> integer -> list bitU -> bitvector 'a
+let bvupdate_aux is_inc start bs i j bs' =
+  let bits = update_aux is_inc start (List.map to_bitU (bitlistFromWord bs)) i j bs' in
+  wordFromBitlist (List.map from_bitU bits)
+  (*let iN = natFromInteger i in
   let jN = natFromInteger j in
   let startN = natFromInteger start in
   let top = word_length bs - 1 in
   let (hi,lo) = if is_inc then (top+startN-iN,top+startN-jN) else (top-startN+iN,top-startN+jN) in
-  let bits = word_update bs lo hi bs' in
-  Bitvector bits start is_inc
+  word_update bs lo hi bs'*)
 
-val bvupdate : forall 'a 'b. Size 'a => bitvector 'a -> integer -> integer -> bitvector 'b -> bitvector 'a
-let bvupdate v i j (Bitvector bs' _ _) =
-  bvupdate_aux v i j bs'
+val bvupdate : forall 'a 'b. Size 'a => bool -> integer -> bitvector 'a -> integer -> integer -> bitvector 'b -> bitvector 'a
+let bvupdate is_inc start bs i j bs' =
+  bvupdate_aux is_inc start bs i j (List.map to_bitU (bitlistFromWord bs'))
 
-val bvaccess : forall 'a. Size 'a => bitvector 'a -> integer -> bitU
-let bvaccess (Bitvector bs start is_inc) n = bool_to_bitU (
+val bvaccess : forall 'a. Size 'a => bool -> integer -> bitvector 'a -> integer -> bitU
+let bvaccess is_inc start bs n = bool_to_bitU (
   let top = integerFromNat (word_length bs) - 1 in
   if is_inc then getBit bs (natFromInteger (top + start - n))
   else getBit bs (natFromInteger (top + n - start)))
 
-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)
+val bvupdate_pos : forall 'a. Size 'a => bool -> integer -> bitvector 'a -> integer -> bitU -> bitvector 'a
+let bvupdate_pos is_inc start v n b =
+  bvupdate_aux is_inc start v n n [b]
 
-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'
+let bitvector_access_inc (start, v, i) = bvaccess true start v i
+let bitvector_access_dec (start, v, i) = bvaccess false start v i
+let bitvector_update_pos_dec (start, v, i, b) = bvupdate_pos false start v i b
+let bitvector_update_subrange_dec (start, v, i, j, v') = bvupdate false start 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*)
+let extract_only_bit elems =
+  let l = word_length elems in
+  if l = 1 then
     bool_to_bitU (msb elems)
-  (*else if l = 0 then
+  else if l = 0 then
     failwith "extract_single_bit called for empty vector"
   else
-    failwith "extract_single_bit called for vector with more bits"*)
+    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 norm_dec v = v (*reset_bitvector_start*)
+let adjust_start_index (start, v) = 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)
@@ -104,7 +106,7 @@ let pp_bitu_vector (Vector elems start inc) =
   "Vector [" ^ elems_pp ^ "] " ^ show start ^ " " ^ show inc
 
 
-let most_significant (Bitvector v _ _) =
+let most_significant v =
   if word_length v = 0 then
     failwith "most_significant applied to empty vector"
   else
@@ -112,20 +114,18 @@ let most_significant (Bitvector 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_not bs = lNot bs
 
-let bitwise_binop op (Bitvector bsl start is_inc, Bitvector bsr _ _) =
-  Bitvector (op bsl bsr) start is_inc
+let bitwise_binop op (bsl, bsr) = (op bsl bsr)
 
 let bitwise_and x = bitwise_binop lAnd x
 let bitwise_or x = bitwise_binop lOr x
 let bitwise_xor x = bitwise_binop lXor x
 
-let unsigned (Bitvector bs _ _) : integer = unsignedIntegerFromWord bs
+(*let unsigned bs : integer = unsignedIntegerFromWord bs*)
 let unsigned_big = unsigned
 
-let signed (Bitvector v _ _) : integer = signedIntegerFromWord v
+let signed v : integer = signedIntegerFromWord v
 
 let hardware_mod (a: integer) (b:integer) : integer = 
  if a < 0 && b < 0
@@ -200,8 +200,9 @@ 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)) =
+val to_norm_vec : forall 'a. Size 'a => integer -> bitvector 'a
+let to_norm_vec (n : integer) = wordFromInteger n
+(*
   (* Bitvector length is determined by return type *)
   let bits = wordFromInteger n in
   let len = integerFromNat (word_length bits) in
@@ -210,31 +211,34 @@ let to_vec_ord is_inc ((len : integer), (n : integer)) =
     Bitvector bits start is_inc
   (*else
     failwith "Vector length mismatch in to_vec"*)
+*)
 
-let to_vec_big = to_vec_ord
+let to_vec_big = to_norm_vec
 
-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)
+let to_vec_inc (start, len, n) = to_norm_vec n
+let to_vec_norm_inc (len, n) = to_norm_vec n
+let to_vec_dec (start, len, n) = to_norm_vec n
+let to_vec_norm_dec (len, n) = to_norm_vec 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
+  (* 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 (start, len, vec) = to_norm_vec (signed vec)
+val extz : forall 'a 'b. Size 'a, Size 'b => (integer * integer * bitvector 'a) -> bitvector 'b
+let extz (start, len, vec) = to_norm_vec (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))
+let exts_big (start, len, vec) = to_vec_big (signed_big vec)
+let extz_big (start, len, vec) = to_vec_big (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 extz_bl (start, len, bits) = vec_to_bvec (Vector bits (integerFromNat (List.length bits - 1)) false)
+let exts_bl (start, len, 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
@@ -252,10 +256,10 @@ 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 arith_op_vec op sign (size : integer) 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)
+  to_norm_vec n
 
 
 (* add_vec
@@ -277,8 +281,8 @@ 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)
+let arith_op_vec_range op sign size l r =
+  arith_op_vec op sign size l ((to_norm_vec r) : bitvector 'a)
 
 (* add_vec_range
  * add_vec_range_signed
@@ -296,8 +300,8 @@ 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
+let arith_op_range_vec op sign size l r =
+  arith_op_vec op sign size ((to_norm_vec l) : bitvector 'a) r
 
 (* add_range_vec
  * add_range_vec_signed
@@ -343,10 +347,10 @@ let arith_op_vec_vec_range op sign l r =
 let add_VVI x = arith_op_vec_vec_range integerAdd false x
 let addS_VVI x = arith_op_vec_vec_range integerAdd true x
 
-let arith_op_vec_bit op sign (size : integer) (Bitvector _ _ is_inc as l) r =
+let arith_op_vec_bit op sign (size : integer) 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)
+  to_norm_vec n
 
 (* add_vec_bit
  * add_vec_bit_signed
@@ -421,15 +425,15 @@ 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 shift_op_vec op (bs, (n : integer)) =
   let n = natFromInteger n in
   match op with
   | LL_shift (*"<<"*) ->
-     Bitvector (shiftLeft bs n) start is_inc
+     shiftLeft bs n
   | RR_shift (*">>"*) ->
-     Bitvector (shiftRight bs n) start is_inc
+     shiftRight bs n
   | LLL_shift (*"<<<"*) ->
-     Bitvector (rotateLeft n bs) start is_inc
+     rotateLeft n bs
   end
 
 let bitwise_leftshift x = shift_op_vec LL_shift x (*"<<"*)
@@ -544,17 +548,18 @@ 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 (Bitvector l _ _,Bitvector r _ _) = (l = r)
-let eq_bit (l,r) = (l = r)
+val eq_vec : forall 'a. Size 'a => bitvector 'a * bitvector 'a -> bool
+let eq_vec (l,r) = eq (to_num false l, to_num false r)
+let eq_bit (l,r) = eq (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 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 (l,r) = not (eq_vec (l,r))
+(*let neq_vec_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))
 
@@ -574,17 +579,17 @@ let make_bitvector_undef length =
 
 (* 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)
+let mask (start, _, w) = (zeroExtend w)
 
 (* Register operations *)
 
-let update_reg_range i j reg_val new_val = bvupdate reg_val i j new_val
-let update_reg_bit i reg_val bit = bvupdate_pos reg_val i bit
+(*let update_reg_range reg i j reg_val new_val = bvupdate (reg.reg_is_inc) (reg.reg_start) reg_val i j new_val
+let update_reg_pos reg i reg_val bit = bvupdate_pos (reg.reg_is_inc) (reg.reg_start) reg_val i bit
 let update_reg_field_range regfield i j reg_val new_val =
   let current_field_value = regfield.get_field reg_val in
-  let new_field_value = bvupdate current_field_value i j new_val in
+  let new_field_value = bvupdate (regfield.field_is_inc) (regfield.field_start) current_field_value i j new_val in
   regfield.set_field reg_val new_field_value
-let write_reg_field_bit regfield i reg_val bit =
+(*let write_reg_field_pos regfield i reg_val bit =
   let current_field_value = regfield.get_field reg_val in
-  let new_field_value = bvupdate_pos current_field_value i bit in
-  regfield.set_field reg_val new_field_value
+  let new_field_value = bvupdate_pos (regfield.field_is_inc) (regfield.field_start) current_field_value i bit in
+  regfield.set_field reg_val new_field_value*)*)
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 4d3ddbce..ae8a0a5b 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -48,6 +48,15 @@ instance (Show bitU)
   let show = showBitU
 end
 
+class (BitU 'a)
+  val to_bitU : 'a -> bitU
+  val from_bitU : bitU -> 'a
+end
+
+instance (BitU bitU)
+  let to_bitU b = b
+  let from_bitU b = b
+end
 
 let bitU_to_bool = function
   | B0 -> false
@@ -55,6 +64,13 @@ let bitU_to_bool = function
   | BU -> failwith "to_bool applied to BU"
   end
 
+let bool_to_bitU b = if b then B1 else B0
+
+instance (BitU bool)
+  let to_bitU = bool_to_bitU
+  let from_bitU = bitU_to_bool
+end
+
 let cast_bit_bool = bitU_to_bool
 
 let bit_lifted_of_bitU = function
@@ -93,8 +109,6 @@ 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?*)
@@ -173,17 +187,19 @@ let update_sublist xs (i,j) xs' =
   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 =
+val slice_aux : forall 'a. bool -> integer -> list 'a -> integer -> integer -> list 'a
+let slice_aux is_inc start bs 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
+  sublist bs (if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN))
+
+val slice : forall 'a. vector 'a -> integer -> integer -> vector 'a
+let slice (Vector bs start is_inc) i j =
+  Vector (slice_aux is_inc start bs i j) 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
+let vector_subrange_inc (start, v, i, j) = slice v i j
+let vector_subrange_dec (start, 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
@@ -198,34 +214,35 @@ let slice_raw (Vector bs start is_inc) i j =
   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' =
+val update_aux : forall 'a. bool -> integer -> list 'a -> integer -> integer -> list 'a -> list 'a
+let update_aux is_inc start bs 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
+  update_sublist bs
+      (if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN)) bs'
 
 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'
+let update (Vector bs start is_inc) i j (Vector bs' _ _) =
+  Vector (update_aux is_inc start bs i j bs') start is_inc
 
-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'
+let vector_update_inc (start, v, i, j, v') = update v i j v'
+let vector_update_dec (start, v, i, j, v') = update v i j v'
+
+val access_aux : forall 'a. bool -> integer -> list 'a -> integer -> 'a
+let access_aux is_inc start xs n =
+  if is_inc then List_extra.nth xs (natFromInteger (n - start))
+  else List_extra.nth xs (natFromInteger (start - n))
 
 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))
+let access (Vector bs start is_inc) n = access_aux is_inc start bs n
 
-let vector_access_inc (v, i) = access v i
-let vector_access_dec (v, i) = access v i
+let vector_access_inc (start, v, i) = access v i
+let vector_access_dec (start, v, i) = access v i
 
 val update_pos : forall 'a. vector 'a -> integer -> 'a -> vector 'a
 let update_pos v n b =
-  update_aux v n n [b]
+  update v n n (Vector [b] 0 false)
 
 let extract_only_element (Vector elems _ _) = match elems with
   | [] -> failwith "extract_only_element called for empty vector"
@@ -236,10 +253,65 @@ end
 (*** Bitvectors *)
 
 (* element list * start * has increasing direction *)
-type bitvector 'a = Bitvector of mword 'a * integer * bool
+type bitvector 'a = mword 'a (* Bitvector of mword 'a * integer * bool *)
 declare isabelle target_sorts bitvector = `len`
 
-let showBitvector (Bitvector elems start inc) =
+class (Bitvector 'a)
+  val bits_of : 'a -> list bitU
+  val of_bits : list bitU -> 'a
+  val unsigned : 'a -> integer
+  (* The first two parameters of the following specify indexing:
+     indexing order and start index *)
+  val get_bit : bool -> integer -> 'a -> integer -> bitU
+  val set_bit : bool -> integer -> 'a -> integer -> bitU -> 'a
+  val get_bits : bool -> integer -> 'a -> integer -> integer -> list bitU
+  val set_bits : bool -> integer -> 'a -> integer -> integer -> list bitU -> 'a
+end
+
+val bitlist_to_integer : list bitU -> integer
+let bitlist_to_integer bs =
+  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
+
+instance forall 'a. BitU 'a => (Bitvector (list 'a))
+  let bits_of v = List.map to_bitU v
+  let of_bits v = List.map from_bitU v
+  let unsigned v = bitlist_to_integer (List.map to_bitU v)
+  let get_bit is_inc start v n = to_bitU (access_aux is_inc start v n)
+  let set_bit is_inc start v n b = update_aux is_inc start v n n [from_bitU b]
+  let get_bits is_inc start v i j = List.map to_bitU (slice_aux is_inc start v i j)
+  let set_bits is_inc start v i j v' = update_aux is_inc start v i j (List.map from_bitU v')
+end
+
+instance forall 'a. BitU 'a => (Bitvector (vector 'a))
+  let bits_of v = List.map to_bitU (get_elems v)
+  let of_bits v = Vector (List.map from_bitU v) (integerFromNat (List.length v) - 1) false
+  let unsigned v = unsigned (get_elems v)
+  let get_bit is_inc start v n = to_bitU (access v n)
+  let set_bit is_inc start v n b = update_pos v n (from_bitU b)
+  let get_bits is_inc start v i j = List.map to_bitU (get_elems (slice v i j))
+  let set_bits is_inc start v i j v' = update v i j (Vector (List.map from_bitU v') (integerFromNat (List.length v') - 1) false)
+end
+
+instance forall 'a. Size 'a => (Bitvector (mword 'a))
+  let bits_of v = List.map to_bitU (bitlistFromWord v)
+  let of_bits v = wordFromBitlist (List.map from_bitU v)
+  let unsigned v = unsignedIntegerFromWord v
+  let get_bit is_inc start v n = to_bitU (access_aux is_inc start (bitlistFromWord v) n)
+  let set_bit is_inc start v n b = wordFromBitlist (update_aux is_inc start (bitlistFromWord v) n n [from_bitU b])
+  let get_bits is_inc start v i j = slice_aux is_inc start (List.map to_bitU (bitlistFromWord v)) i j
+  let set_bits is_inc start v i j v' = wordFromBitlist (update_aux is_inc start (bitlistFromWord v) i j (List.map from_bitU v'))
+end
+
+(*let showBitvector (Bitvector elems start inc) =
   "Bitvector " ^ show elems ^ " " ^ show start ^ " " ^ show inc
 
 let bvget_dir (Bitvector _ _ ord) = ord
@@ -248,15 +320,15 @@ let bvget_elems (Bitvector elems _ _) = elems
 
 instance forall 'a. (Show (bitvector 'a))
   let show = showBitvector
-end
+end*)
 
-let bvec_to_vec (Bitvector bs start is_inc) =
+let bvec_to_vec is_inc start bs =
   let bits = List.map bool_to_bitU (bitlistFromWord bs) in
   Vector bits start is_inc
 
 let vec_to_bvec (Vector elems start is_inc) =
-  let word = wordFromBitlist (List.map bitU_to_bool elems) in
-  Bitvector word start is_inc
+  (*let word =*) wordFromBitlist (List.map bitU_to_bool elems) (*in
+  Bitvector word start is_inc*)
 
 (*** Vector operations *)
 
@@ -269,37 +341,37 @@ let rec byte_chunks n list = match (n,list) with
   | _ -> failwith "byte_chunks not given enough bits"
 end
 
-val bitv_of_byte_lifteds : bool -> list Sail_impl_base.byte_lifted -> vector bitU
+val bitv_of_byte_lifteds : bool -> list Sail_impl_base.byte_lifted -> list 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
+  bits (*Vector bits (if dir then 0 else len - 1) dir*)
 
-val bitv_of_bytes : bool -> list Sail_impl_base.byte -> vector bitU
+val bitv_of_bytes : bool -> list Sail_impl_base.byte -> list 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
+  bits (*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) =
+val byte_lifteds_of_bitv : list bitU -> list byte_lifted
+let byte_lifteds_of_bitv bits =
   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) =
+val bytes_of_bitv : list bitU -> list byte
+let bytes_of_bitv bits =
   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 bit_lifteds_of_bitv : list bitU -> list bit_lifted
+let bit_lifteds_of_bitv v = bit_lifteds_of_bitUs v
 
 
-val address_lifted_of_bitv : vector bitU -> address_lifted
+val address_lifted_of_bitv : list bitU -> address_lifted
 let address_lifted_of_bitv v =
   let byte_lifteds = byte_lifteds_of_bitv v in
   let maybe_address_integer =
@@ -309,7 +381,7 @@ let address_lifted_of_bitv v =
     end in
   Address_lifted byte_lifteds maybe_address_integer
 
-val address_of_bitv : vector bitU -> address
+val address_of_bitv : list bitU -> address
 let address_of_bitv v =
   let bytes = bytes_of_bitv v in
   address_of_byte_list bytes
@@ -332,11 +404,15 @@ type register =
 
 type register_ref 'regstate 'a =
   <| reg_name : string;
+     reg_start : integer;
+     reg_is_inc : bool;
      read_from : 'regstate -> 'a;
      write_to : 'regstate -> 'a -> 'regstate |>
 
 type field_ref 'regtype 'a =
   <| field_name : string;
+     field_start : integer;
+     field_is_inc : bool;
      get_field : 'regtype -> 'a;
      set_field : 'regtype -> 'a -> 'regtype |>
 
@@ -415,11 +491,11 @@ let rec external_reg_value reg_name v =
      rv_start          = external_start;
      rv_start_internal = internal_start |>
 
-val internal_reg_value : register_value -> vector bitU
+val internal_reg_value : register_value -> list 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)
+  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)) =
@@ -502,8 +578,9 @@ let toNaturalFiveTup (n1,n2,n3,n4,n5) =
    toNatural n4,
    toNatural n5)
 
-
-type regfp =
+(* Let the following types be generated by Sail per spec, using either bitlists
+   or machine words as bitvector representation *)
+(*type regfp =
   | RFull of (string)
   | RSlice of (string * integer * integer)
   | RSliceBit of (string * integer)
@@ -545,7 +622,7 @@ end
 
 let niafp_to_nia reginfo = function
   | NIAFP_successor -> NIA_successor
-  | NIAFP_concrete_address v -> NIA_concrete_address (address_of_bitv v)
+  | NIAFP_concrete_address v -> NIA_concrete_address (address_of_bitv (bits_of v))
   | NIAFP_LR -> NIA_LR
   | NIAFP_CTR -> NIA_CTR
   | NIAFP_register r -> NIA_register (regfp_to_reg reginfo r)
@@ -553,6 +630,7 @@ end
 
 let diafp_to_dia reginfo = function
   | DIAFP_none -> DIA_none
-  | DIAFP_concrete v -> DIA_concrete_address (address_of_bitv v)
+  | DIAFP_concrete v -> DIA_concrete_address (address_of_bitv (bits_of 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 fa6515fb..1b03c81e 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -75,11 +75,12 @@ let set_reg state reg v =
   <| state with regstate = reg.write_to state.regstate v |>
 
 
-val read_mem : forall 'regs 'a 'b. Size 'b => bool -> read_kind -> integer -> integer -> M 'regs (vector bitU)
+val read_mem : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => bool -> read_kind -> 'a -> integer -> M 'regs 'b
 let read_mem dir read_kind addr sz state =
+  let addr = unsigned addr in
   let addrs = range addr (addr+sz-1) in
   let memory_value = List.map (fun addr -> Map_extra.find addr state.memstate) addrs in
-  let value = Sail_values.internal_mem_value dir memory_value in
+  let value = of_bits (Sail_values.internal_mem_value dir memory_value) in
   let is_exclusive = match read_kind with
     | Sail_impl_base.Read_plain -> false
     | Sail_impl_base.Read_reserve -> true
@@ -96,9 +97,9 @@ let read_mem dir read_kind addr sz state =
 (* caps are aligned at 32 bytes *)
 let cap_alignment = (32 : integer)
 
-val read_tag : forall 'regs 'a. bool -> read_kind -> integer -> M 'regs bitU
+val read_tag : forall 'regs 'a. Bitvector 'a => bool -> read_kind -> 'a -> M 'regs bitU
 let read_tag dir read_kind addr state =
-  let addr = addr / cap_alignment in
+  let addr = (unsigned addr) / cap_alignment in
   let tag = match (Map.lookup addr state.tagstate) with
     | Just t -> t
     | Nothing -> B0
@@ -123,17 +124,17 @@ let excl_result () state =
     (Left true,  <| state with last_exclusive_operation_was_load = false |>) in
   (Left false, state) :: if state.last_exclusive_operation_was_load then [success] else []
 
-val write_mem_ea : forall 'regs 'a. write_kind -> integer -> integer -> M 'regs unit
+val write_mem_ea : forall 'regs 'a. Bitvector 'a => write_kind -> 'a -> integer -> M 'regs unit
 let write_mem_ea write_kind addr sz state = 
-  [(Left (), <| state with write_ea = Just (write_kind,addr,sz) |>)]
+  [(Left (), <| state with write_ea = Just (write_kind,unsigned addr,sz) |>)]
 
-val write_mem_val : forall 'regs 'b. vector bitU -> M 'regs bool
+val write_mem_val : forall 'a 'regs 'b. Bitvector 'a => 'a -> M 'regs bool
 let write_mem_val v state =
   let (write_kind,addr,sz) = match state.write_ea with
     | Nothing -> failwith "write ea has not been announced yet"
     | Just write_ea -> write_ea end in
   let addrs = range addr (addr+sz-1) in
-  let v = external_mem_value v in
+  let v = external_mem_value (bits_of v) in
   let addresses_with_value = List.zip addrs v in
   let memstate = List.foldl (fun mem (addr,v) -> Map.insert addr v mem)
                             state.memstate addresses_with_value in
@@ -170,12 +171,42 @@ let reg_deref = read_reg
 val write_reg : forall 'regs 'a. register_ref 'regs 'a -> 'a -> M 'regs unit
 let write_reg reg v state =
   [(Left (), <| state with regstate = reg.write_to state.regstate v |>)]
+
 val update_reg : forall 'regs 'a 'b. register_ref 'regs 'a -> ('a -> 'b -> 'a) -> 'b -> M 'regs unit
 let update_reg reg f v state =
   let current_value = get_reg state reg in
   let new_value = f current_value v in
   [(Left (), set_reg state reg new_value)]
 
+let write_reg_field reg regfield = update_reg reg regfield.set_field
+
+val update_reg_range : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => register_ref 'regs 'a -> integer -> integer -> 'a -> 'b -> 'a
+let update_reg_range reg i j reg_val new_val = set_bits (reg.reg_is_inc) (reg.reg_start) reg_val i j (bits_of new_val)
+let write_reg_range reg i j = update_reg reg (update_reg_range reg i j)
+
+let update_reg_pos reg i reg_val x = update_pos reg_val i x
+let write_reg_pos reg i = update_reg reg (update_reg_pos reg i)
+
+let update_reg_bit reg i reg_val bit = set_bit (reg.reg_is_inc) (reg.reg_start) reg_val i (to_bitU bit)
+let write_reg_bit reg i = update_reg reg (update_reg_bit reg i)
+
+let update_reg_field_range regfield i j reg_val new_val =
+  let current_field_value = regfield.get_field reg_val in
+  let new_field_value = set_bits (regfield.field_is_inc) (regfield.field_start) current_field_value i j (bits_of new_val) in
+  regfield.set_field reg_val new_field_value
+let write_reg_field_range reg regfield i j = update_reg reg (update_reg_field_range regfield i j)
+
+let update_reg_field_pos regfield i reg_val x =
+  let current_field_value = regfield.get_field reg_val in
+  let new_field_value = update_pos current_field_value i x in
+  regfield.set_field reg_val new_field_value
+let write_reg_field_pos reg regfield i = update_reg reg (update_reg_field_pos regfield i)
+
+let update_reg_field_bit regfield i reg_val bit =
+  let current_field_value = regfield.get_field reg_val in
+  let new_field_value = set_bit (regfield.field_is_inc) (regfield.field_start) current_field_value i (to_bitU bit) in
+  regfield.set_field reg_val new_field_value
+let write_reg_field_bit reg regfield i = update_reg reg (update_reg_field_bit regfield i)
 
 val barrier : forall 'regs. barrier_kind -> M 'regs unit
 let barrier _ = return ()
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index f981297d..f6fec143 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -122,6 +122,12 @@ let doc_id_lem_ctor (Id_aux(i,_)) =
 
 let doc_var_lem kid = string (fix_id true (string_of_kid kid))
 
+let simple_annot l typ = (Parse_ast.Generated l, Some (Env.empty, typ, no_effect))
+let simple_num l n = E_aux (
+  E_lit (L_aux (L_num n, Parse_ast.Generated l)),
+  simple_annot (Parse_ast.Generated l)
+    (atom_typ (Nexp_aux (Nexp_constant n, Parse_ast.Generated l))))
+
 let effectful_set =
   List.exists
     (fun (BE_aux (eff,_)) ->
@@ -394,15 +400,14 @@ let doc_exp_lem, doc_let_lem =
                    underscore ^^
                    doc_id_lem id in
                  liftR ((prefix 2 1)
-                   (string "update_reg")
-                   (align (doc_lexp_deref_lem sequential mwords early_ret le ^^ space^^
-                      parens (string "update_reg_field_range" ^/^ field_ref ^/^ expY e2 ^/^ expY e3) ^/^ expY e)))
+                   (string "write_reg_field_range")
+                   (align (doc_lexp_deref_lem sequential mwords early_ret le ^/^
+                      field_ref ^/^ expY e2 ^/^ expY e3 ^/^ expY e)))
             | _ ->
+               let deref = doc_lexp_deref_lem sequential mwords early_ret le in
                liftR ((prefix 2 1)
-                 (string "update_reg")
-                 (align (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^
-                   parens (string "update_reg_range" ^/^ expY e2 ^/^ expY e3) ^/^ expY e)))
-           )
+                 (string "write_reg_range")
+                 (align (deref ^/^ expY e2 ^/^ expY e3) ^/^ expY e)))
         | LEXP_vector (le,e2) ->
            (match le with
             | LEXP_aux (LEXP_field ((LEXP_aux (_, lannot) as le),id), fannot) ->
@@ -413,11 +418,12 @@ let doc_exp_lem, doc_let_lem =
                    doc_id_lem (typ_id_of (typ_of_annot lannot)) ^^
                    underscore ^^
                    doc_id_lem id in
+                 let call = if is_bitvector_typ (Env.base_typ_of (env_of full_exp) (typ_of_annot fannot)) then "write_reg_field_bit" else "write_reg_field_pos" in
                  liftR ((prefix 2 1)
-                   (string "update_reg")
-                   (align (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^
-                     parens (string "update_reg_field_bit" ^/^ field_ref ^/^ expY e2) ^/^ expY e)))
-            | _ ->
+                   (string call)
+                   (align (doc_lexp_deref_lem sequential mwords early_ret le ^/^
+                     field_ref ^/^ expY e2 ^/^ expY e)))
+            | LEXP_aux (_, lannot) ->
                (match le with
                  | LEXP_aux (_, (_, Some (_, Typ_aux (Typ_app (vector, [_; _; _; Typ_arg_aux (Typ_arg_typ etyp, _)]), _), _)))
                    when is_reftyp etyp && string_of_id vector = "vector" ->
@@ -430,9 +436,10 @@ let doc_exp_lem, doc_let_lem =
                        ]) in
                    liftR ((prefix 2 1) (string "write_reg") (deref ^/^ expY e))
                  | _ ->
-                   liftR ((prefix 2 1) (string "update_reg")
-                   (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^
-                     parens (string "update_reg_bit" ^/^ expY e2) ^/^ expY e)))
+                   let deref = doc_lexp_deref_lem sequential mwords early_ret le in
+                   let call = if is_bitvector_typ (Env.base_typ_of (env_of full_exp) (typ_of_annot lannot)) then "write_reg_bit" else "write_reg_pos" in
+                   liftR ((prefix 2 1) (string call)
+                   (deref ^/^ expY e2 ^/^ expY e)))
            )
         (* | LEXP_field (le,id) when is_bit_typ t ->
            liftR ((prefix 2 1)
@@ -442,11 +449,11 @@ let doc_exp_lem, doc_let_lem =
           let field_ref =
             doc_id_lem (typ_id_of (typ_of_annot lannot)) ^^
             underscore ^^
-            doc_id_lem id ^^
+            doc_id_lem id (*^^
             dot ^^
-            string "set_field" in
+            string "set_field"*) in
            liftR ((prefix 2 1)
-             (string "update_reg")
+             (string "write_reg_field")
              (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^
                 field_ref ^/^ expY e))
         (* | (LEXP_id id | LEXP_cast (_,id)), t, Alias alias_info ->
@@ -597,8 +604,22 @@ let doc_exp_lem, doc_let_lem =
           end
        end
     | E_vector_access (v,e) ->
-      raise (Reporting_basic.err_unreachable l
-        "E_vector_access should have been rewritten before pretty-printing")
+      let vtyp = Env.base_typ_of (env_of v) (typ_of v) in
+      let (start, _, ord, etyp) = vector_typ_args_of vtyp in
+      let ord_suffix = if is_order_inc ord then "_inc" else "_dec" in
+      let call =
+        if is_bitvector_typ vtyp (*&& mwords*)
+        then "bitvector_access" ^ ord_suffix
+        else "vector_access" ^ ord_suffix in
+      let start_idx = match simplify_nexp (start) with
+        | Nexp_aux (Nexp_constant i, _) -> expN (simple_num l i)
+        | _ ->
+          raise (Reporting_basic.err_unreachable l
+            ("cannot pretty print expression " ^ (string_of_exp full_exp) ^ " with non-constant start index")) in
+      let epp = string call ^^ space ^^ parens (separate comma_sp [start_idx;expY v;expY e]) in
+      if aexp_needed then parens (align epp) else epp
+      (* raise (Reporting_basic.err_unreachable l
+        "E_vector_access should have been rewritten before pretty-printing") *)
        (* let eff = effect_of full_exp in
        let epp =
          if has_effect eff BE_rreg then
@@ -609,8 +630,22 @@ let doc_exp_lem, doc_let_lem =
            separate space [string call;expY v;expY e] in
        if aexp_needed then parens (align epp) else epp*)
     | E_vector_subrange (v,e1,e2) ->
-      raise (Reporting_basic.err_unreachable l
-        "E_vector_subrange should have been rewritten before pretty-printing")
+      let vtyp = Env.base_typ_of (env_of v) (typ_of v) in
+      let (start, _, ord, etyp) = vector_typ_args_of vtyp in
+      let ord_suffix = if is_order_inc ord then "_inc" else "_dec" in
+      let call =
+        if is_bitvector_typ vtyp (*&& mwords*)
+        then "bitvector_subrange" ^ ord_suffix
+        else "vector_subrange" ^ ord_suffix in
+      let start_idx = match simplify_nexp (start) with
+        | Nexp_aux (Nexp_constant i, _) -> expN (simple_num l i)
+        | _ ->
+          raise (Reporting_basic.err_unreachable l
+            ("cannot pretty print expression " ^ (string_of_exp full_exp) ^ " with non-constant start index")) in
+      let epp = string call ^^ space ^^ parens (separate comma_sp [start_idx;expY v;expY e1;expY e2]) in
+      if aexp_needed then parens (align epp) else epp
+      (* raise (Reporting_basic.err_unreachable l
+        "E_vector_subrange should have been rewritten before pretty-printing") *)
        (* let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
        let eff = effect_of full_exp in
        let (epp,aexp_needed) =
@@ -849,26 +884,36 @@ let doc_exp_lem, doc_let_lem =
        if aexp_needed then parens (align bepp) else bepp
     | E_vector_update(v,e1,e2) ->
        let t = typ_of full_exp in
-       let (_, _, ord, _) = vector_typ_args_of (Env.base_typ_of (env_of full_exp) t) in
+       let (start, _, ord, _) = vector_typ_args_of (Env.base_typ_of (env_of full_exp) t) in
        let ord_suffix = if is_order_inc ord then "_inc" else "_dec" in
        let call =
          if is_bitvector_typ t (*&& mwords*)
          then "bitvector_update_pos" ^ ord_suffix
-         else "update_pos" ^ ord_suffix in
-       let epp = string call ^^ space ^^ parens (separate comma_sp [expY v;expY e1;expY e2]) in
+         else "vector_update_pos" ^ ord_suffix in
+       let start_idx = match simplify_nexp (start) with
+         | Nexp_aux (Nexp_constant i, _) -> expN (simple_num l i)
+         | _ ->
+           raise (Reporting_basic.err_unreachable l
+             ("cannot pretty print expression " ^ (string_of_exp full_exp) ^ " with non-constant start index")) in
+       let epp = string call ^^ space ^^ parens (separate comma_sp [start_idx;expY v;expY e1;expY e2]) in
        if aexp_needed then parens (align epp) else epp
     | E_vector_update_subrange(v,e1,e2,e3) ->
        let t = typ_of full_exp in
-       let (_, _, ord, _) = vector_typ_args_of (Env.base_typ_of (env_of full_exp) t) in
+       let (start, _, ord, _) = vector_typ_args_of (Env.base_typ_of (env_of full_exp) t) in
        let ord_suffix = if is_order_inc ord then "_inc" else "_dec" in
        let call =
          if is_bitvector_typ t (*&& mwords*)
-         then "bitvector_update" ^ ord_suffix
-         else "update" ^ ord_suffix in
+         then "bitvector_update_subrange" ^ ord_suffix
+         else "vector_update_subrange" ^ ord_suffix in
+       let start_idx = match simplify_nexp (start) with
+         | Nexp_aux (Nexp_constant i, _) -> expN (simple_num l i)
+         | _ ->
+           raise (Reporting_basic.err_unreachable l
+             ("cannot pretty print expression " ^ (string_of_exp full_exp) ^ " with non-constant start index")) in
        let epp =
          align (string call ^//^
            parens (separate comma_sp
-             [group (expY v); group (expY e1); group (expY e2); group (expY e3)])) in
+             [start_idx; group (expY v); group (expY e1); group (expY e2); group (expY e3)])) in
        if aexp_needed then parens (align epp) else epp
     | E_list exps ->
        brackets (separate_map semi (expN) exps)
@@ -1071,7 +1116,7 @@ let rec doc_range_lem (BF_aux(r,_)) = match r with
   | BF_range(i1,i2) -> parens (doc_op comma (doc_int i1) (doc_int i2))
   | BF_concat(ir1,ir2) -> (doc_range ir1) ^^ comma ^^ (doc_range ir2)
 
-let doc_typdef_lem sequential mwords (TD_aux(td, (l, _))) = match td with
+let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with
   | TD_abbrev(id,nm,typschm) ->
      doc_op equals (concat [string "type"; space; doc_id_lem_type id])
             (doc_typschm_lem sequential mwords false typschm)
@@ -1102,10 +1147,25 @@ let doc_typdef_lem sequential mwords (TD_aux(td, (l, _))) = match td with
         string "rec_val" ^^ dot ^^ fname fid,
         anglebars (space ^^ string "rec_val with " ^^
           (doc_op equals (fname fid) (string "v")) ^^ space) in
+      let base_ftyp = match annot with
+        | Some (env, _, _) -> Env.base_typ_of env ftyp
+        | _ -> ftyp in
+      let (start, is_inc) =
+        try
+          let (start, _, ord, _) = vector_typ_args_of base_ftyp in
+          match simplify_nexp start with
+          | Nexp_aux (Nexp_constant i, _) -> (i, is_order_inc ord)
+          | _ ->
+            raise (Reporting_basic.err_unreachable Parse_ast.Unknown
+              ("register " ^ string_of_id id ^ " has non-constant start index " ^ string_of_nexp start))
+        with
+        | _ -> (0, true) in
       doc_op equals
         (concat [string "let "; parens (concat [doc_id_lem id; underscore; doc_id_lem fid; rfannot])])
         (anglebars (concat [space;
           doc_op equals (string "field_name") (string_lit (doc_id_lem fid)); semi_sp;
+          doc_op equals (string "field_start") (string (string_of_int start)); semi_sp;
+          doc_op equals (string "field_is_inc") (string (if is_inc then "true" else "false")); semi_sp;
           doc_op equals (string "get_field") (parens (doc_op arrow (string "fun rec_val") get)); semi_sp;
           doc_op equals (string "set_field") (parens (doc_op arrow (string "fun rec_val v") set)); space])) in
     doc_op equals
@@ -1120,9 +1180,9 @@ let doc_typdef_lem sequential mwords (TD_aux(td, (l, _))) = match td with
       | Id_aux ((Id "barrier_kind"),_) -> empty
       | Id_aux ((Id "trans_kind"),_) -> empty
       | Id_aux ((Id "instruction_kind"),_) -> empty
-      | Id_aux ((Id "regfp"),_) -> empty
+      (* | Id_aux ((Id "regfp"),_) -> empty
       | Id_aux ((Id "niafp"),_) -> empty
-      | Id_aux ((Id "diafp"),_) -> empty
+      | Id_aux ((Id "diafp"),_) -> empty *)
       | Id_aux ((Id "option"),_) -> empty
       | _ ->
          let ar_doc = group (separate_map (break 1) (doc_type_union_lem sequential mwords) ar) in
@@ -1298,7 +1358,7 @@ let doc_typdef_lem sequential mwords (TD_aux(td, (l, _))) = match td with
     match n1, n2 with
     | Nexp_aux(Nexp_constant i1,_),Nexp_aux(Nexp_constant i2,_) ->
        let dir_b = i1 < i2 in
-       let dir = string (if dir_b then "true" else "false") in
+       let dir = (if dir_b then "true" else "false") in
        let dir_suffix = (if dir_b then "_inc" else "_dec") in
        let ord = Ord_aux ((if dir_b then Ord_inc else Ord_dec), Parse_ast.Unknown) in
        let size = if dir_b then i2-i1 +1 else i1-i2 + 1 in
@@ -1319,15 +1379,20 @@ let doc_typdef_lem sequential mwords (TD_aux(td, (l, _))) = match td with
              [mk_typ_arg (Typ_arg_typ (mk_id_typ id));
               mk_typ_arg (Typ_arg_typ ftyp)])) in
          let rfannot = doc_tannot_lem sequential mwords false reftyp in
+         let id_exp id = E_aux (E_id (mk_id id), simple_annot l vtyp) in
          let get, set =
-           "bitvector_subrange" ^ dir_suffix ^ " (reg, " ^ string_of_int i ^ ", " ^ string_of_int j ^ ")",
-           "bitvector_update" ^ dir_suffix ^ " (reg, " ^ string_of_int i ^ ", " ^ string_of_int j ^ ", v)" in
+           E_aux (E_vector_subrange (id_exp "reg", simple_num l i, simple_num l j), simple_annot l ftyp),
+           E_aux (E_vector_update_subrange (id_exp "reg", simple_num l i, simple_num l j, id_exp "v"), simple_annot l ftyp) in
+           (* "bitvector_subrange" ^ dir_suffix ^ " (" ^ string_of_int i1 ^ ", reg, " ^ string_of_int i ^ ", " ^ string_of_int j ^ ")",
+           "bitvector_update_subrange" ^ dir_suffix ^ " (" ^ string_of_int i1 ^ ", reg, " ^ string_of_int i ^ ", " ^ string_of_int j ^ ", v)" in *)
          doc_op equals
            (concat [string "let "; parens (concat [doc_id_lem id; underscore; doc_id_lem fid; rfannot])])
            (concat [
              space; langlebar; string " field_name = \"" ^^ doc_id_lem fid ^^ string "\";"; hardline;
-             space; space; space; string (" get_field = (fun reg -> " ^ get ^ ");"); hardline;
-             space; space; space; string (" set_field = (fun reg v -> " ^ set ^ ") "); ranglebar])
+             space; space; space; string (" field_start = " ^ string_of_int i ^ ";"); hardline;
+             space; space; space; string (" field_is_inc = " ^ dir ^ ";"); hardline;
+             space; space; space; string " get_field = (fun reg -> " ^^ doc_exp_lem sequential mwords false false get ^^ string ");"; hardline;
+             space; space; space; string " set_field = (fun reg v -> " ^^ doc_exp_lem sequential mwords false false set ^^ string ") "; ranglebar])
        in
        doc_op equals
          (concat [string "type";space;doc_id_lem id])
@@ -1365,7 +1430,7 @@ let doc_typdef_lem sequential mwords (TD_aux(td, (l, _))) = match td with
          doc_op equals
            (concat [string "let";space;string "build_";doc_id_lem id;space;string "regname"])
            (string "Register" ^^ space ^^
-              align (separate space [string "regname"; doc_int size; doc_int i1; dir;
+              align (separate space [string "regname"; doc_int size; doc_int i1; string dir;
                                      break 0 ^^ brackets (align doc_rids)]))
          (*^^ hardline ^^
            separate_map hardline doc_field rs*)
@@ -1550,7 +1615,11 @@ let find_registers (Defs defs) =
   List.fold_left
     (fun acc def ->
       match def with
-      | DEF_reg_dec (DEC_aux(DEC_reg (typ, id),_)) -> (typ, id) :: acc
+      | DEF_reg_dec (DEC_aux(DEC_reg (typ, id), annot)) ->
+        let env = match annot with
+          | (_, Some (env, _, _)) -> env
+          | _ -> Env.empty in
+        (typ, id, env) :: acc
       | _ -> acc
     ) [] defs
 
@@ -1568,7 +1637,7 @@ let doc_regstate_lem mwords registers =
         Id_aux (Id "regstate", l),
         Name_sect_aux (Name_sect_none, l),
         TypQ_aux (TypQ_tq [], l),
-        registers,
+        List.map (fun (typ, id, env) -> (typ, id)) registers,
         false) in
   concat [
     doc_typdef_lem true mwords (TD_aux (regstate, annot)); hardline;
@@ -1577,11 +1646,24 @@ let doc_regstate_lem mwords registers =
   ]
 
 let doc_register_refs_lem registers =
-  let doc_register_ref (typ, id) =
+  let doc_register_ref (typ, id, env) =
     let idd = doc_id_lem id in
     let field = if prefix_recordtype then string "regstate_" ^^ idd else idd in
+    let base_typ = Env.base_typ_of env typ in
+    let (start, is_inc) =
+      try
+        let (start, _, ord, _) = vector_typ_args_of base_typ in
+        match simplify_nexp start with
+        | Nexp_aux (Nexp_constant i, _) -> (i, is_order_inc ord)
+        | _ ->
+          raise (Reporting_basic.err_unreachable Parse_ast.Unknown
+            ("register " ^ string_of_id id ^ " has non-constant start index " ^ string_of_nexp start))
+      with
+      | _ -> (0, true) in
     concat [string "let "; idd; string " = <|"; hardline;
       string "  reg_name = \""; idd; string "\";"; hardline;
+      string "  reg_start = "; string (string_of_int start); string ";"; hardline;
+      string "  reg_is_inc = "; string (if is_inc then "true" else "false"); string ";"; hardline;
       string "  read_from = (fun s -> s."; field; string ");"; hardline;
       string "  write_to = (fun s v -> (<| s with "; field; string " = v |>)) |>"] in
   separate_map hardline doc_register_ref registers
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 5cf1a6b9..c2b8e618 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -1452,10 +1452,10 @@ let remove_vector_concat_pat pat =
       let index_j = simple_num l j in
 
       (* FIXME *)
-      (* let subv = fix_eff_exp (E_aux (E_vector_subrange (root, index_i, index_j), cannot)) in *)
-      let (_, _, ord, _) = vector_typ_args_of (Env.base_typ_of (env_of root) (typ_of root)) in
+      let subv = fix_eff_exp (E_aux (E_vector_subrange (root, index_i, index_j), cannot)) in
+      (* let (_, _, ord, _) = vector_typ_args_of (Env.base_typ_of (env_of root) (typ_of root)) in
       let subrange_id = if is_order_inc ord then "bitvector_subrange_inc" else "bitvector_subrange_dec" in
-      let subv = fix_eff_exp (E_aux (E_app (mk_id subrange_id, [root; index_i; index_j]), cannot)) in
+      let subv = fix_eff_exp (E_aux (E_app (mk_id subrange_id, [root; index_i; index_j]), cannot)) in *)
 
       let id_pat =
         match typ_opt with
@@ -1920,12 +1920,12 @@ let remove_bitvector_pat pat =
   let access_bit_exp (rootid,rannot) l idx =
     let root : tannot exp = E_aux (E_id rootid,rannot) in
     (* FIXME *)
-    (* E_aux (E_vector_access (root,simple_num l idx), simple_annot l bit_typ) in *)
-    let env = env_of_annot rannot in
+    E_aux (E_vector_access (root,simple_num l idx), simple_annot l bit_typ) in
+    (*let env = env_of_annot rannot in
     let t = Env.base_typ_of env (typ_of_annot rannot) in
     let (_, _, ord, _) = vector_typ_args_of t in
     let access_id = if is_order_inc ord then "bitvector_access_inc" else "bitvector_access_dec" in
-    E_aux (E_app (mk_id access_id, [root; simple_num l idx]), simple_annot l bit_typ) in
+    E_aux (E_app (mk_id access_id, [root; simple_num l idx]), simple_annot l bit_typ) in*)
 
   let test_bit_exp rootid l t idx exp =
     let rannot = simple_annot l t in
@@ -1951,12 +1951,12 @@ let remove_bitvector_pat pat =
       (*if vec_start t = i && vec_length t = List.length lits
       then E_id rootid
       else*)
-          (* E_vector_subrange (
+          E_vector_subrange (
              E_aux (E_id rootid, simple_annot l typ),
              simple_num l i,
-             simple_num l j) in *)
-          let subrange_id = if is_order_inc ord then "bitvector_subrange_inc" else "bitvector_subrange_dec" in
-          E_app (mk_id subrange_id, [E_aux (E_id rootid, simple_annot l typ); simple_num l i; simple_num l j]) in
+             simple_num l j) in
+          (* let subrange_id = if is_order_inc ord then "bitvector_subrange_inc" else "bitvector_subrange_dec" in
+          E_app (mk_id subrange_id, [E_aux (E_id rootid, simple_annot l typ); simple_num l i; simple_num l j]) in *)
     E_aux (E_app(
       Id_aux (Id "eq_vec", Parse_ast.Generated l),
       [E_aux (subvec_exp, simple_annot l typ');
diff --git a/src/type_check.ml b/src/type_check.ml
index 5a98704c..8dabbd30 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1647,8 +1647,8 @@ let destruct_atom_nexp env typ =
   match Env.expand_synonyms env typ with
   | Typ_aux (Typ_app (f, [Typ_arg_aux (Typ_arg_nexp n, _)]), _)
        when string_of_id f = "atom" -> Some n
-  | Typ_aux (Typ_app (f, [Typ_arg_aux (Typ_arg_nexp n, _); Typ_arg_aux (Typ_arg_nexp _, _)]), _)
-       when string_of_id f = "range" -> Some n
+  | Typ_aux (Typ_app (f, [Typ_arg_aux (Typ_arg_nexp n, _); Typ_arg_aux (Typ_arg_nexp m, _)]), _)
+       when string_of_id f = "range" && nexp_identical n m -> Some n
   | _ -> None
 
 exception Not_a_constraint;;