Merge changes to type_check.ml

8 files changed, 1014 insertions, 1266 deletions

diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 5019c2f7..d398ab52 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -1,172 +1,8 @@
 open import Pervasives_extra
 open import Sail_impl_base
 open import Sail_values
-
-type M 'a 'e = outcome 'a 'e
-
-val return : forall 'a 'e. 'a -> M 'a 'e
-let return a = Done a
-
-val bind : forall 'a 'b 'e. M 'a 'e -> ('a -> M 'b 'e) -> M 'b 'e
-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))
-  | Read_reg descr k ->    Read_reg descr   (fun v -> let (o,opt) = k v in (bind o f,opt))
-  | Write_memv descr k ->  Write_memv descr (fun v -> let (o,opt) = k v in (bind o f,opt))
-  | Excl_res k ->          Excl_res         (fun v -> let (o,opt) = k v in (bind o f,opt))
-  | Write_ea descr o_s ->  Write_ea descr   (let (o,opt) = o_s in (bind o f,opt))
-  | Barrier descr o_s ->   Barrier descr    (let (o,opt) = o_s in (bind o f,opt))
-  | Footprint o_s ->       Footprint        (let (o,opt) = o_s in (bind o f,opt))
-  | Write_reg descr o_s -> Write_reg descr  (let (o,opt) = o_s in (bind o f,opt))
-  | Escape descr ->        Escape descr
-  | Fail descr ->          Fail descr
-  | Error descr ->         Error descr
-  | Exception e ->         Exception e
-  | Internal descr o_s ->  Internal descr   (let (o,opt) = o_s in (bind o f ,opt))
-end
-
-let inline (>>=) = bind
-val (>>) : forall 'b 'e. M unit 'e -> M 'b 'e -> M 'b 'e
-let inline (>>) m n = m >>= fun (_ : unit) -> n
-
-val exit : forall 'a 'e. unit -> M 'a 'e
-let exit () = Fail Nothing
-
-val assert_exp : forall 'e. bool -> string -> M unit 'e
-let assert_exp exp msg = if exp then Done () else Fail (Just msg)
-
-val throw : forall 'a 'e. 'e -> M 'a 'e
-let throw e = Exception e
-
-val try_catch : forall 'a 'e1 'e2. M 'a 'e1 -> ('e1 -> M 'a 'e2) ->  M 'a 'e2
-let rec try_catch m h = match m with
-  | Done a ->              Done a
-  | Read_mem descr k ->    Read_mem descr   (fun v -> let (o,opt) = k v in (try_catch o h,opt))
-  | Read_reg descr k ->    Read_reg descr   (fun v -> let (o,opt) = k v in (try_catch o h,opt))
-  | Write_memv descr k ->  Write_memv descr (fun v -> let (o,opt) = k v in (try_catch o h,opt))
-  | Excl_res k ->          Excl_res         (fun v -> let (o,opt) = k v in (try_catch o h,opt))
-  | Write_ea descr o_s ->  Write_ea descr   (let (o,opt) = o_s in (try_catch o h,opt))
-  | Barrier descr o_s ->   Barrier descr    (let (o,opt) = o_s in (try_catch o h,opt))
-  | Footprint o_s ->       Footprint        (let (o,opt) = o_s in (try_catch o h,opt))
-  | Write_reg descr o_s -> Write_reg descr  (let (o,opt) = o_s in (try_catch o h,opt))
-  | Escape descr ->        Escape descr
-  | Fail descr ->          Fail descr
-  | Error descr ->         Error descr
-  | Exception e ->         h e
-  | Internal descr o_s ->  Internal descr   (let (o,opt) = o_s in (try_catch o h ,opt))
-end
-
-(* For early return, we abuse exceptions by throwing and catching
-   the return value. The exception type is "either 'r 'e", where "Right e"
-   represents a proper exception and "Left r" an early return of value "r". *)
-type MR 'a 'r 'e = M 'a (either 'r 'e)
-
-val early_return : forall 'a 'r 'e. 'r -> MR 'a 'r 'e
-let early_return r = throw (Left r)
-
-val catch_early_return : forall 'a 'e. MR 'a 'a 'e -> M 'a 'e
-let catch_early_return m =
-  try_catch m
-    (function
-      | Left a -> return a
-      | Right e -> throw e
-     end)
-
-(* Lift to monad with early return by wrapping exceptions *)
-val liftR : forall 'a 'r 'e. M 'a 'e -> MR 'a 'r 'e
-let liftR m = try_catch m (fun e -> throw (Right e))
-
-(* Catch exceptions in the presence of early returns *)
-val try_catchR : forall 'a 'r 'e1 'e2. MR 'a 'r 'e1 -> ('e1 -> MR 'a 'r 'e2) ->  MR 'a 'r 'e2
-let try_catchR m h =
-  try_catch m
-    (function
-      | Left r -> throw (Left r)
-      | Right e -> h e
-     end)
-
-
-val read_mem : forall 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> M 'b 'e
-let read_mem rk addr sz =
-  let addr = address_lifted_of_bitv (bits_of addr) in
-  let sz = natFromInteger sz in
-  let k memory_value =
-    let bitv = of_bits (internal_mem_value memory_value) in
-    (Done bitv,Nothing) in
-  Read_mem (rk,addr,sz) k
-
-val excl_result : forall 'e. unit -> M bool 'e
-let excl_result () =
-  let k successful = (return successful,Nothing) in
-  Excl_res k
-
-val write_mem_ea : forall 'a 'e. Bitvector 'a => write_kind -> 'a -> integer -> M unit 'e
-let write_mem_ea wk addr sz =
-  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 : forall 'a 'e. Bitvector 'a => 'a -> M bool 'e
-let write_mem_val v =
-  let v = external_mem_value (bits_of v) in
-  let k successful = (return successful,Nothing) in
-  Write_memv v k
-
-val read_reg_aux : forall 'a 'e. Bitvector 'a => reg_name -> M 'a 'e
-let read_reg_aux reg = 
-  let k reg_value =
-    let v = of_bits (internal_reg_value reg_value) in
-    (Done v,Nothing) in
-  Read_reg reg k
-
-let read_reg reg =
-  read_reg_aux (external_reg_whole reg)
-let read_reg_range reg i j =
-  read_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger j))
-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.field_name)
-let read_reg_bitfield reg regfield =
-  read_reg_aux (external_reg_field_whole reg regfield.field_name) >>= fun v ->
-  return (extract_only_element v)
-
-let reg_deref = read_reg
-
-val write_reg_aux : forall 'a 'e. Bitvector 'a => reg_name -> 'a -> M unit 'e
-let write_reg_aux reg_name v =
-  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_pos reg i v =
-  let iN = natFromInteger i in
-  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_field_bit reg regfield bit =
-  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.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
-
-let write_reg_ref (reg, v) = write_reg reg v
-
-val barrier : forall 'e. barrier_kind -> M unit 'e
-let barrier bk = Barrier bk (Done (), Nothing)
-
-
-val footprint : forall 'e. M unit 'e
-let footprint = Footprint (Done (),Nothing)
-
+open import Prompt_monad
+open import {isabelle} `Prompt_monad_extras`
 
 val iter_aux : forall 'a 'e. integer -> (integer -> 'a -> M unit 'e) -> list 'a -> M unit 'e
 let rec iter_aux i f xs = match xs with
diff --git a/src/gen_lib/prompt_monad.lem b/src/gen_lib/prompt_monad.lem
new file mode 100644
index 00000000..45733caa
--- /dev/null
+++ b/src/gen_lib/prompt_monad.lem
@@ -0,0 +1,168 @@
+open import Pervasives_extra
+open import Sail_impl_base
+open import Sail_values
+
+type M 'a 'e = outcome 'a 'e
+
+val return : forall 'a 'e. 'a -> M 'a 'e
+let return a = Done a
+
+val bind : forall 'a 'b 'e. M 'a 'e -> ('a -> M 'b 'e) -> M 'b 'e
+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))
+  | Read_reg descr k ->    Read_reg descr   (fun v -> let (o,opt) = k v in (bind o f,opt))
+  | Write_memv descr k ->  Write_memv descr (fun v -> let (o,opt) = k v in (bind o f,opt))
+  | Excl_res k ->          Excl_res         (fun v -> let (o,opt) = k v in (bind o f,opt))
+  | Write_ea descr o_s ->  Write_ea descr   (let (o,opt) = o_s in (bind o f,opt))
+  | Barrier descr o_s ->   Barrier descr    (let (o,opt) = o_s in (bind o f,opt))
+  | Footprint o_s ->       Footprint        (let (o,opt) = o_s in (bind o f,opt))
+  | Write_reg descr o_s -> Write_reg descr  (let (o,opt) = o_s in (bind o f,opt))
+  | Escape descr ->        Escape descr
+  | Fail descr ->          Fail descr
+  | Error descr ->         Error descr
+  | Exception e ->         Exception e
+  | Internal descr o_s ->  Internal descr   (let (o,opt) = o_s in (bind o f ,opt))
+end
+
+let inline (>>=) = bind
+val (>>) : forall 'b 'e. M unit 'e -> M 'b 'e -> M 'b 'e
+let inline (>>) m n = m >>= fun (_ : unit) -> n
+
+val exit : forall 'a 'e. unit -> M 'a 'e
+let exit () = Fail Nothing
+
+val assert_exp : forall 'e. bool -> string -> M unit 'e
+let assert_exp exp msg = if exp then Done () else Fail (Just msg)
+
+val throw : forall 'a 'e. 'e -> M 'a 'e
+let throw e = Exception e
+
+val try_catch : forall 'a 'e1 'e2. M 'a 'e1 -> ('e1 -> M 'a 'e2) ->  M 'a 'e2
+let rec try_catch m h = match m with
+  | Done a ->              Done a
+  | Read_mem descr k ->    Read_mem descr   (fun v -> let (o,opt) = k v in (try_catch o h,opt))
+  | Read_reg descr k ->    Read_reg descr   (fun v -> let (o,opt) = k v in (try_catch o h,opt))
+  | Write_memv descr k ->  Write_memv descr (fun v -> let (o,opt) = k v in (try_catch o h,opt))
+  | Excl_res k ->          Excl_res         (fun v -> let (o,opt) = k v in (try_catch o h,opt))
+  | Write_ea descr o_s ->  Write_ea descr   (let (o,opt) = o_s in (try_catch o h,opt))
+  | Barrier descr o_s ->   Barrier descr    (let (o,opt) = o_s in (try_catch o h,opt))
+  | Footprint o_s ->       Footprint        (let (o,opt) = o_s in (try_catch o h,opt))
+  | Write_reg descr o_s -> Write_reg descr  (let (o,opt) = o_s in (try_catch o h,opt))
+  | Escape descr ->        Escape descr
+  | Fail descr ->          Fail descr
+  | Error descr ->         Error descr
+  | Exception e ->         h e
+  | Internal descr o_s ->  Internal descr   (let (o,opt) = o_s in (try_catch o h ,opt))
+end
+
+(* For early return, we abuse exceptions by throwing and catching
+   the return value. The exception type is "either 'r 'e", where "Right e"
+   represents a proper exception and "Left r" an early return of value "r". *)
+type MR 'a 'r 'e = M 'a (either 'r 'e)
+
+val early_return : forall 'a 'r 'e. 'r -> MR 'a 'r 'e
+let early_return r = throw (Left r)
+
+val catch_early_return : forall 'a 'e. MR 'a 'a 'e -> M 'a 'e
+let catch_early_return m =
+  try_catch m
+    (function
+      | Left a -> return a
+      | Right e -> throw e
+     end)
+
+(* Lift to monad with early return by wrapping exceptions *)
+val liftR : forall 'a 'r 'e. M 'a 'e -> MR 'a 'r 'e
+let liftR m = try_catch m (fun e -> throw (Right e))
+
+(* Catch exceptions in the presence of early returns *)
+val try_catchR : forall 'a 'r 'e1 'e2. MR 'a 'r 'e1 -> ('e1 -> MR 'a 'r 'e2) ->  MR 'a 'r 'e2
+let try_catchR m h =
+  try_catch m
+    (function
+      | Left r -> throw (Left r)
+      | Right e -> h e
+     end)
+
+
+val read_mem : forall 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> M 'b 'e
+let read_mem rk addr sz =
+  let addr = address_lifted_of_bitv (bits_of addr) in
+  let sz = natFromInteger sz in
+  let k memory_value =
+    let bitv = of_bits (internal_mem_value memory_value) in
+    (Done bitv,Nothing) in
+  Read_mem (rk,addr,sz) k
+
+val excl_result : forall 'e. unit -> M bool 'e
+let excl_result () =
+  let k successful = (return successful,Nothing) in
+  Excl_res k
+
+val write_mem_ea : forall 'a 'e. Bitvector 'a => write_kind -> 'a -> integer -> M unit 'e
+let write_mem_ea wk addr sz =
+  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 : forall 'a 'e. Bitvector 'a => 'a -> M bool 'e
+let write_mem_val v =
+  let v = external_mem_value (bits_of v) in
+  let k successful = (return successful,Nothing) in
+  Write_memv v k
+
+val read_reg_aux : forall 'a 'e. Bitvector 'a => reg_name -> M 'a 'e
+let read_reg_aux reg =
+  let k reg_value =
+    let v = of_bits (internal_reg_value reg_value) in
+    (Done v,Nothing) in
+  Read_reg reg k
+
+let read_reg reg =
+  read_reg_aux (external_reg_whole reg)
+let read_reg_range reg i j =
+  read_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger j))
+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.field_name)
+let read_reg_bitfield reg regfield =
+  read_reg_aux (external_reg_field_whole reg regfield.field_name) >>= fun v ->
+  return (extract_only_element v)
+
+let reg_deref = read_reg
+
+val write_reg_aux : forall 'a 'e. Bitvector 'a => reg_name -> 'a -> M unit 'e
+let write_reg_aux reg_name v =
+  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_pos reg i v =
+  let iN = natFromInteger i in
+  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_field_bit reg regfield bit =
+  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.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
+
+let write_reg_ref (reg, v) = write_reg reg v
+
+val barrier : forall 'e. barrier_kind -> M unit 'e
+let barrier bk = Barrier bk (Done (), Nothing)
+
+
+val footprint : forall 'e. M unit 'e
+let footprint = Footprint (Done (),Nothing)
diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index 230ab84e..ada91bd0 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail_operators.lem
@@ -5,53 +5,22 @@ open import Sail_values
 
 (*** Bit vector operations *)
 
-val concat_vec : forall 'a 'b 'c. Bitvector 'a, Bitvector 'b, Bitvector 'c => 'a -> 'b -> 'c
-let concat_vec l r = of_bits (bits_of l ++ bits_of r)
+val concat_bv : forall 'a 'b 'c. Bitvector 'a, Bitvector 'b, Bitvector 'c => 'a -> 'b -> 'c
+let concat_bv l r = of_bits (bits_of l ++ bits_of r)
 
-val cons_vec : forall 'a 'b 'c. Bitvector 'a, Bitvector 'b => bitU -> 'a -> 'b
-let cons_vec b v = of_bits (b :: bits_of v)
+val cons_bv : forall 'a 'b 'c. Bitvector 'a, Bitvector 'b => bitU -> 'a -> 'b
+let cons_bv b v = of_bits (b :: bits_of v)
 
-let bool_of_vec v = extract_only_element (bits_of v)
-let vec_of_bit len b = of_bits (extz_bits len [b])
-let cast_unit_vec b = of_bits [b]
+let bool_of_bv v = extract_only_element (bits_of v)
+let cast_unit_bv b = of_bits [b]
+let bv_of_bit len b = of_bits (extz_bits len [b])
+let int_of_bv sign = if sign then signed else unsigned
 
 let most_significant v = match bits_of v with
   | b :: _ -> b
   | _ -> failwith "most_significant applied to empty vector"
   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 int_of_vec sign = if sign then signed else unsigned
-let vec_of_int len n = of_bits (bits_of_int len n)
-
-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
@@ -68,106 +37,106 @@ let get_min_representable_in _ (n : integer) : integer =
   else if n = 5 then min_5
   else 0 - (integerPow 2 (natFromInteger n))
 
-val bitwise_binop_vec : forall 'a. Bitvector 'a =>
+val bitwise_binop_bv : forall 'a. Bitvector 'a =>
   (bool -> bool -> bool) -> 'a -> 'a -> 'a
-let bitwise_binop_vec op l r = of_bits (binop_bits op (bits_of l) (bits_of r))
+let bitwise_binop_bv op l r = of_bits (binop_bits op (bits_of l) (bits_of r))
 
-let and_vec = bitwise_binop_vec (&&)
-let or_vec = bitwise_binop_vec (||)
-let xor_vec = bitwise_binop_vec xor
-let not_vec v = of_bits (not_bits (bits_of v))
+let and_bv = bitwise_binop_bv (&&)
+let or_bv = bitwise_binop_bv (||)
+let xor_bv = bitwise_binop_bv xor
+let not_bv v = of_bits (not_bits (bits_of v))
 
-val arith_op_vec : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
+val arith_op_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
   (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> 'b
-let arith_op_vec op sign size l r =
-  let (l',r') = (int_of_vec sign l, int_of_vec sign r) in
+let arith_op_bv op sign size l r =
+  let (l',r') = (int_of_bv sign l, int_of_bv sign r) in
   let n = op l' r' in
-  of_bits (bits_of_int (size * length l) n)
+  of_int (size * length l) n
 
 
-let add_vec = arith_op_vec integerAdd false 1
-let addS_vec = arith_op_vec integerAdd true 1
-let sub_vec = arith_op_vec integerMinus false 1
-let mult_vec = arith_op_vec integerMult false 2
-let multS_vec = arith_op_vec integerMult true 2
+let add_bv   = arith_op_bv integerAdd false 1
+let addS_bv  = arith_op_bv integerAdd true 1
+let sub_bv   = arith_op_bv integerMinus false 1
+let mult_bv  = arith_op_bv integerMult false 2
+let multS_bv = arith_op_bv integerMult true 2
 
 let inline add_mword = Machine_word.plus
 let inline sub_mword = Machine_word.minus
 val mult_mword : forall 'a 'b. Size 'b => mword 'a -> mword 'a -> mword 'b
 let mult_mword l r = times (zeroExtend l) (zeroExtend r)
 
-val arith_op_vec_int : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
+val arith_op_bv_int : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
   (integer -> integer -> integer) -> bool -> integer -> 'a -> integer -> 'b
-let arith_op_vec_int op sign size l r =
-  let l' = int_of_vec sign l in
+let arith_op_bv_int op sign size l r =
+  let l' = int_of_bv sign l in
   let n = op l' r in
-  of_bits (bits_of_int (size * length l) n)
+  of_int (size * length l) n
 
-let add_vec_int = arith_op_vec_int integerAdd false 1
-let addS_vec_int = arith_op_vec_int integerAdd true 1
-let sub_vec_int = arith_op_vec_int integerMinus false 1
-let mult_vec_int = arith_op_vec_int integerMult false 2
-let multS_vec_int = arith_op_vec_int integerMult true 2
+let add_bv_int = arith_op_bv_int integerAdd false 1
+let addS_bv_int = arith_op_bv_int integerAdd true 1
+let sub_bv_int = arith_op_bv_int integerMinus false 1
+let mult_bv_int = arith_op_bv_int integerMult false 2
+let multS_bv_int = arith_op_bv_int integerMult true 2
 
-val arith_op_int_vec : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
+val arith_op_int_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
   (integer -> integer -> integer) -> bool -> integer -> integer -> 'a -> 'b
-let arith_op_int_vec op sign size l r =
-  let r' = int_of_vec sign r in
+let arith_op_int_bv op sign size l r =
+  let r' = int_of_bv sign r in
   let n = op l r' in
-  of_bits (bits_of_int (size * length r) n)
+  of_int (size * length r) n
 
-let add_int_vec = arith_op_int_vec integerAdd false 1
-let addS_int_vec = arith_op_int_vec integerAdd true 1
-let sub_int_vec = arith_op_int_vec integerMinus false 1
-let mult_int_vec = arith_op_int_vec integerMult false 2
-let multS_int_vec = arith_op_int_vec integerMult true 2
+let add_int_bv = arith_op_int_bv integerAdd false 1
+let addS_int_bv = arith_op_int_bv integerAdd true 1
+let sub_int_bv = arith_op_int_bv integerMinus false 1
+let mult_int_bv = arith_op_int_bv integerMult false 2
+let multS_int_bv = arith_op_int_bv integerMult true 2
 
-let arith_op_vec_bit op sign (size : integer) l r =
-  let l' = int_of_vec sign l in
+let arith_op_bv_bit op sign (size : integer) l r =
+  let l' = int_of_bv sign l in
   let n = op l' (match r with | B1 -> (1 : integer) | _ -> 0 end) in
-  of_bits (bits_of_int (size * length l) n)
+  of_int (size * length l) n
 
-let add_vec_bit = arith_op_vec_bit integerAdd false 1
-let addS_vec_bit = arith_op_vec_bit integerAdd true 1
-let sub_vec_bit = arith_op_vec_bit integerMinus true 1
+let add_bv_bit = arith_op_bv_bit integerAdd false 1
+let addS_bv_bit = arith_op_bv_bit integerAdd true 1
+let sub_bv_bit = arith_op_bv_bit integerMinus true 1
 
-val arith_op_overflow_vec : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
+val arith_op_overflow_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
   (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> ('b * bitU * bitU)
-let arith_op_overflow_vec op sign size l r =
+let arith_op_overflow_bv op sign size l r =
   let len = length l in
   let act_size = len * size in
-  let (l_sign,r_sign) = (int_of_vec sign l,int_of_vec sign r) in
-  let (l_unsign,r_unsign) = (int_of_vec false l,int_of_vec false r) in
+  let (l_sign,r_sign) = (int_of_bv sign l,int_of_bv sign r) in
+  let (l_unsign,r_unsign) = (int_of_bv false l,int_of_bv false r) in
   let n = op l_sign r_sign in
   let n_unsign = op l_unsign r_unsign in
-  let correct_size = bits_of_int act_size n in
+  let correct_size = of_int act_size n in
   let one_more_size_u = bits_of_int (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
-  (of_bits correct_size,overflow,c_out)
+  (correct_size,overflow,c_out)
 
-let add_overflow_vec = arith_op_overflow_vec integerAdd false 1
-let add_overflow_vec_signed = arith_op_overflow_vec integerAdd true 1
-let sub_overflow_vec = arith_op_overflow_vec integerMinus false 1
-let sub_overflow_vec_signed = arith_op_overflow_vec integerMinus true 1
-let mult_overflow_vec = arith_op_overflow_vec integerMult false 2
-let mult_overflow_vec_signed = arith_op_overflow_vec integerMult true 2
+let add_overflow_bv = arith_op_overflow_bv integerAdd false 1
+let add_overflow_bv_signed = arith_op_overflow_bv integerAdd true 1
+let sub_overflow_bv = arith_op_overflow_bv integerMinus false 1
+let sub_overflow_bv_signed = arith_op_overflow_bv integerMinus true 1
+let mult_overflow_bv = arith_op_overflow_bv integerMult false 2
+let mult_overflow_bv_signed = arith_op_overflow_bv integerMult true 2
 
-val arith_op_overflow_vec_bit : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
+val arith_op_overflow_bv_bit : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
   (integer -> integer -> integer) -> bool -> integer -> 'a -> bitU -> ('b * bitU * bitU)
-let arith_op_overflow_vec_bit op sign size l r_bit =
+let arith_op_overflow_bv_bit op sign size l r_bit =
   let act_size = length l * size in
-  let l' = int_of_vec sign l in
-  let l_u = int_of_vec false l in
+  let l' = int_of_bv sign l in
+  let l_u = int_of_bv 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"
+    | BU -> failwith "arith_op_overflow_bv_bit applied to undefined bit"
     end in
-  let correct_size = bits_of_int act_size n in
+  let correct_size = of_int act_size n in
   let one_larger = bits_of_int (act_size + 1) nu in
   let overflow =
     if changed
@@ -175,32 +144,35 @@ let arith_op_overflow_vec_bit op sign size l r_bit =
       if n <= get_max_representable_in sign act_size && n >= get_min_representable_in sign act_size
       then B0 else B1
     else B0 in
-  (of_bits correct_size,overflow,most_significant one_larger)
+  (correct_size,overflow,most_significant one_larger)
 
-let add_overflow_vec_bit = arith_op_overflow_vec_bit integerAdd false 1
-let add_overflow_vec_bit_signed = arith_op_overflow_vec_bit integerAdd true 1
-let sub_overflow_vec_bit = arith_op_overflow_vec_bit integerMinus false 1
-let sub_overflow_vec_bit_signed = arith_op_overflow_vec_bit integerMinus true 1
+let add_overflow_bv_bit = arith_op_overflow_bv_bit integerAdd false 1
+let add_overflow_bv_bit_signed = arith_op_overflow_bv_bit integerAdd true 1
+let sub_overflow_bv_bit = arith_op_overflow_bv_bit integerMinus false 1
+let sub_overflow_bv_bit_signed = arith_op_overflow_bv_bit integerMinus true 1
 
-type shift = LL_shift | RR_shift | LL_rot | RR_rot
+type shift = LL_shift | RR_shift | RR_shift_arith | LL_rot | RR_rot
 
-val shift_op_vec : forall 'a. Bitvector 'a => shift -> 'a -> integer -> 'a
-let shift_op_vec op v n =
+val shift_op_bv : forall 'a. Bitvector 'a => shift -> 'a -> integer -> 'a
+let shift_op_bv op v n =
   match op with
   | LL_shift ->
      of_bits (get_bits true v n (length v - 1) ++ repeat [B0] n)
   | RR_shift ->
      of_bits (repeat [B0] n ++ get_bits true v 0 (length v - n - 1))
+  | RR_shift_arith ->
+     of_bits (repeat [most_significant v] n ++ get_bits true v 0 (length v - n - 1))
   | LL_rot ->
      of_bits (get_bits true v n (length v - 1) ++ get_bits true v 0 (n - 1))
   | RR_rot ->
      of_bits (get_bits false v 0 (n - 1) ++ get_bits false v n (length v - 1))
   end
 
-let shiftl = shift_op_vec LL_shift (*"<<"*)
-let shiftr = shift_op_vec RR_shift (*">>"*)
-let rotl = shift_op_vec LL_rot (*"<<<"*)
-let rotr = shift_op_vec LL_rot (*">>>"*)
+let shiftl_bv = shift_op_bv LL_shift (*"<<"*)
+let shiftr_bv = shift_op_bv RR_shift (*">>"*)
+let arith_shiftr_bv = shift_op_bv RR_shift_arith
+let rotl_bv = shift_op_bv LL_rot (*"<<<"*)
+let rotr_bv = shift_op_bv LL_rot (*">>>"*)
 
 let shiftl_mword w n = Machine_word.shiftLeft w (natFromInteger n)
 let shiftr_mword w n = Machine_word.shiftRight w (natFromInteger n)
@@ -212,11 +184,11 @@ let rec arith_op_no0 (op : integer -> integer -> integer) l r =
   then Nothing
   else Just (op l r)
 
-val arith_op_vec_no0 : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
+val arith_op_bv_no0 : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
   (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> 'b
-let arith_op_vec_no0 op sign size l r =
+let arith_op_bv_no0 op sign size l r =
   let act_size = length l * size in
-  let (l',r') = (int_of_vec sign l,int_of_vec sign r) in
+  let (l',r') = (int_of_bv sign l,int_of_bv sign r) in
   let n = arith_op_no0 op l' r' in
   let (representable,n') =
     match n with
@@ -225,80 +197,42 @@ let arith_op_vec_no0 op sign size l r =
          n' >= get_min_representable_in sign act_size, n')
     | _ -> (false,0)
     end in
-  of_bits (if representable then bits_of_int act_size n' else repeat [BU] act_size)
+  if representable then (of_int act_size n') else (of_bits (repeat [BU] act_size))
 
-let mod_vec = arith_op_vec_no0 hardware_mod false 1
-let quot_vec = arith_op_vec_no0 hardware_quot false 1
-let quot_vec_signed = arith_op_vec_no0 hardware_quot true 1
+let mod_bv = arith_op_bv_no0 hardware_mod false 1
+let quot_bv = arith_op_bv_no0 hardware_quot false 1
+let quot_bv_signed = arith_op_bv_no0 hardware_quot true 1
 
 let mod_mword = Machine_word.modulo
 let quot_mword = Machine_word.unsignedDivide
 let quot_mword_signed = Machine_word.signedDivide
 
-val arith_op_overflow_vec_no0 : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
-  (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> ('b * bitU * bitU)
-let arith_op_overflow_vec_no0 op sign size l r =
-  let rep_size = length r * size in
-  let act_size = length l * size in
-  let (l',r') = (int_of_vec sign l,int_of_vec sign r) in
-  let (l_u,r_u) = (int_of_vec false l,int_of_vec 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,one_more) =
-    if representable then
-      (bits_of_int act_size n', bits_of_int (act_size + 1) n_u')
-    else
-      (repeat [BU] act_size, repeat [BU] (act_size + 1)) in
-  let overflow = if representable then B0 else B1 in
-  (of_bits correct_size,overflow,most_significant one_more)
-
-let quot_overflow_vec = arith_op_overflow_vec_no0 hardware_quot false 1
-let quot_overflow_vec_signed = arith_op_overflow_vec_no0 hardware_quot true 1
-
-let arith_op_vec_int_no0 op sign size l r =
-  arith_op_vec_no0 op sign size l (of_bits (bits_of_int (length l) r))
-
-let quot_vec_int = arith_op_vec_int_no0 hardware_quot false 1
-let mod_vec_int = arith_op_vec_int_no0 hardware_mod false 1
-
-let replicate_bits v count = of_bits (repeat v count)
-let duplicate bit len = replicate_bits [bit] len
-
-let lt = (<)
-let gt = (>)
-let lteq = (<=)
-let gteq = (>=)
+let arith_op_bv_int_no0 op sign size l r =
+  arith_op_bv_no0 op sign size l (of_int (length l) r)
 
-val eq : forall 'a. Eq 'a => 'a -> 'a -> bool
-let eq l r = (l = r)
+let quot_bv_int = arith_op_bv_int_no0 hardware_quot false 1
+let mod_bv_int = arith_op_bv_int_no0 hardware_mod false 1
 
-val eq_vec : forall 'a. Bitvector 'a => 'a -> 'a -> bool
-let eq_vec l r = (unsigned l = unsigned r)
+let replicate_bits_bv v count = of_bits (repeat (bits_of v) count)
+let duplicate_bit_bv bit len = replicate_bits_bv [bit] len
 
-val neq : forall 'a. Eq 'a => 'a -> 'a -> bool
-let neq l r = (l <> r)
+val eq_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool
+let eq_bv l r = (unsigned l = unsigned r)
 
-val neq_vec : forall 'a. Bitvector 'a => 'a -> 'a -> bool
-let neq_vec l r = (unsigned l <> unsigned r)
+val neq_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool
+let neq_bv l r = (unsigned l <> unsigned r)
 
-val ucmp_vec : forall 'a. Bitvector 'a => (integer -> integer -> bool) -> 'a -> 'a -> bool
-let ucmp_vec cmp l r = cmp (unsigned l) (unsigned r)
+val ucmp_bv : forall 'a. Bitvector 'a => (integer -> integer -> bool) -> 'a -> 'a -> bool
+let ucmp_bv cmp l r = cmp (unsigned l) (unsigned r)
 
-val scmp_vec : forall 'a. Bitvector 'a => (integer -> integer -> bool) -> 'a -> 'a -> bool
-let scmp_vec cmp l r = cmp (signed l) (signed r)
+val scmp_bv : forall 'a. Bitvector 'a => (integer -> integer -> bool) -> 'a -> 'a -> bool
+let scmp_bv cmp l r = cmp (signed l) (signed r)
 
-let ult_vec = ucmp_vec (<)
-let slt_vec = scmp_vec (<)
-let ugt_vec = ucmp_vec (>)
-let sgt_vec = scmp_vec (>)
-let ulteq_vec = ucmp_vec (<=)
-let slteq_vec = scmp_vec (<=)
-let ugteq_vec = ucmp_vec (>=)
-let sgteq_vec = scmp_vec (>=)
+let ult_bv = ucmp_bv (<)
+let slt_bv = scmp_bv (<)
+let ugt_bv = ucmp_bv (>)
+let sgt_bv = scmp_bv (>)
+let ulteq_bv = ucmp_bv (<=)
+let slteq_bv = scmp_bv (<=)
+let ugteq_bv = ucmp_bv (>=)
+let sgteq_bv = scmp_bv (>=)
diff --git a/src/gen_lib/sail_operators_bitlists.lem b/src/gen_lib/sail_operators_bitlists.lem
new file mode 100644
index 00000000..374628a4
--- /dev/null
+++ b/src/gen_lib/sail_operators_bitlists.lem
@@ -0,0 +1,179 @@
+open import Pervasives_extra
+open import Machine_word
+open import Sail_impl_base
+open import Sail_values
+open import Sail_operators
+
+(* Specialisation of operators to bit lists *)
+
+val access_vec_inc : list bitU -> integer -> bitU
+let access_vec_inc = access_bv_inc
+
+val access_vec_dec : list bitU -> integer -> bitU
+let access_vec_dec = access_bv_dec
+
+val update_vec_inc : list bitU -> integer -> bitU -> list bitU
+let update_vec_inc = update_bv_inc
+
+val update_vec_dec : list bitU -> integer -> bitU -> list bitU
+let update_vec_dec = update_bv_dec
+
+val subrange_vec_inc : list bitU -> integer -> integer -> list bitU
+let subrange_vec_inc = subrange_bv_inc
+
+val subrange_vec_dec : list bitU -> integer -> integer -> list bitU
+let subrange_vec_dec = subrange_bv_dec
+
+val update_subrange_vec_inc : list bitU -> integer -> integer -> list bitU -> list bitU
+let update_subrange_vec_inc = update_subrange_bv_inc
+
+val update_subrange_vec_dec : list bitU -> integer -> integer -> list bitU -> list bitU
+let update_subrange_vec_dec = update_subrange_bv_dec
+
+val extz_vec : integer -> list bitU -> list bitU
+let extz_vec = extz_bv
+
+val exts_vec : integer -> list bitU -> list bitU
+let exts_vec = exts_bv
+
+val concat_vec : list bitU -> list bitU -> list bitU
+let concat_vec = concat_bv
+
+val cons_vec : bitU -> list bitU -> list bitU
+let cons_vec = cons_bv
+
+val bool_of_vec : mword ty1 -> bitU
+let bool_of_vec = bool_of_bv
+
+val cast_unit_vec : bitU -> mword ty1
+let cast_unit_vec = cast_unit_bv
+
+val vec_of_bit : integer -> bitU -> list bitU
+let vec_of_bit = bv_of_bit
+
+val msb : list bitU -> bitU
+let msb = most_significant
+
+val int_of_vec : bool -> list bitU -> integer
+let int_of_vec = int_of_bv
+
+val and_vec : list bitU -> list bitU -> list bitU
+val or_vec  : list bitU -> list bitU -> list bitU
+val xor_vec : list bitU -> list bitU -> list bitU
+val not_vec : list bitU -> list bitU
+let and_vec = and_bv
+let or_vec  = or_bv
+let xor_vec = xor_bv
+let not_vec = not_bv
+
+val add_vec   : list bitU -> list bitU -> list bitU
+val addS_vec  : list bitU -> list bitU -> list bitU
+val sub_vec   : list bitU -> list bitU -> list bitU
+val mult_vec  : list bitU -> list bitU -> list bitU
+val multS_vec : list bitU -> list bitU -> list bitU
+let add_vec   = add_bv
+let addS_vec  = addS_bv
+let sub_vec   = sub_bv
+let mult_vec  = mult_bv
+let multS_vec = multS_bv
+
+val add_vec_int   : list bitU -> integer -> list bitU
+val addS_vec_int  : list bitU -> integer -> list bitU
+val sub_vec_int   : list bitU -> integer -> list bitU
+val mult_vec_int  : list bitU -> integer -> list bitU
+val multS_vec_int : list bitU -> integer -> list bitU
+let add_vec_int   = add_bv_int
+let addS_vec_int  = addS_bv_int
+let sub_vec_int   = sub_bv_int
+let mult_vec_int  = mult_bv_int
+let multS_vec_int = multS_bv_int
+
+val add_int_vec   : integer -> list bitU -> list bitU
+val addS_int_vec  : integer -> list bitU -> list bitU
+val sub_int_vec   : integer -> list bitU -> list bitU
+val mult_int_vec  : integer -> list bitU -> list bitU
+val multS_int_vec : integer -> list bitU -> list bitU
+let add_int_vec   = add_int_bv
+let addS_int_vec  = addS_int_bv
+let sub_int_vec   = sub_int_bv
+let mult_int_vec  = mult_int_bv
+let multS_int_vec = multS_int_bv
+
+val add_vec_bit  : list bitU -> bitU -> list bitU
+val addS_vec_bit : list bitU -> bitU -> list bitU
+val sub_vec_bit  : list bitU -> bitU -> list bitU
+let add_vec_bit  = add_bv_bit
+let addS_vec_bit = addS_bv_bit
+let sub_vec_bit  = sub_bv_bit
+
+val add_overflow_vec         : list bitU -> list bitU -> (list bitU * bitU * bitU)
+val add_overflow_vec_signed  : list bitU -> list bitU -> (list bitU * bitU * bitU)
+val sub_overflow_vec         : list bitU -> list bitU -> (list bitU * bitU * bitU)
+val sub_overflow_vec_signed  : list bitU -> list bitU -> (list bitU * bitU * bitU)
+val mult_overflow_vec        : list bitU -> list bitU -> (list bitU * bitU * bitU)
+val mult_overflow_vec_signed : list bitU -> list bitU -> (list bitU * bitU * bitU)
+let add_overflow_vec         = add_overflow_bv
+let add_overflow_vec_signed  = add_overflow_bv_signed
+let sub_overflow_vec         = sub_overflow_bv
+let sub_overflow_vec_signed  = sub_overflow_bv_signed
+let mult_overflow_vec        = mult_overflow_bv
+let mult_overflow_vec_signed = mult_overflow_bv_signed
+
+val add_overflow_vec_bit         : list bitU -> bitU -> (list bitU * bitU * bitU)
+val add_overflow_vec_bit_signed  : list bitU -> bitU -> (list bitU * bitU * bitU)
+val sub_overflow_vec_bit         : list bitU -> bitU -> (list bitU * bitU * bitU)
+val sub_overflow_vec_bit_signed  : list bitU -> bitU -> (list bitU * bitU * bitU)
+let add_overflow_vec_bit         = add_overflow_bv_bit
+let add_overflow_vec_bit_signed  = add_overflow_bv_bit_signed
+let sub_overflow_vec_bit         = sub_overflow_bv_bit
+let sub_overflow_vec_bit_signed  = sub_overflow_bv_bit_signed
+
+val shiftl       : list bitU -> integer -> list bitU
+val shiftr       : list bitU -> integer -> list bitU
+val arith_shiftr : list bitU -> integer -> list bitU
+val rotl         : list bitU -> integer -> list bitU
+val rotr         : list bitU -> integer -> list bitU
+let shiftl       = shiftl_bv
+let shiftr       = shiftr_bv
+let arith_shiftr = arith_shiftr_bv
+let rotl         = rotl_bv
+let rotr         = rotr_bv
+
+val mod_vec         : list bitU -> list bitU -> list bitU
+val quot_vec        : list bitU -> list bitU -> list bitU
+val quot_vec_signed : list bitU -> list bitU -> list bitU
+let mod_vec         = mod_bv
+let quot_vec        = quot_bv
+let quot_vec_signed = quot_bv_signed
+
+val mod_vec_int  : list bitU -> integer -> list bitU
+val quot_vec_int : list bitU -> integer -> list bitU
+let mod_vec_int  = mod_bv_int
+let quot_vec_int = quot_bv_int
+
+val replicate_bits : list bitU -> integer -> list bitU
+let replicate_bits = replicate_bits_bv
+
+val duplicate : bitU -> integer -> list bitU
+let duplicate = duplicate_bit_bv
+
+val eq_vec    : list bitU -> list bitU -> bool
+val neq_vec   : list bitU -> list bitU -> bool
+val ult_vec   : list bitU -> list bitU -> bool
+val slt_vec   : list bitU -> list bitU -> bool
+val ugt_vec   : list bitU -> list bitU -> bool
+val sgt_vec   : list bitU -> list bitU -> bool
+val ulteq_vec : list bitU -> list bitU -> bool
+val slteq_vec : list bitU -> list bitU -> bool
+val ugteq_vec : list bitU -> list bitU -> bool
+val sgteq_vec : list bitU -> list bitU -> bool
+let eq_vec    = eq_bv
+let neq_vec   = neq_bv
+let ult_vec   = ult_bv
+let slt_vec   = slt_bv
+let ugt_vec   = ugt_bv
+let sgt_vec   = sgt_bv
+let ulteq_vec = ulteq_bv
+let slteq_vec = slteq_bv
+let ugteq_vec = ugteq_bv
+let sgteq_vec = sgteq_bv
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index ff25c37b..7fa09b9b 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -2,600 +2,178 @@ open import Pervasives_extra
 open import Machine_word
 open import Sail_impl_base
 open import Sail_values
-
-(* Translating between a type level number (itself 'n) and an integer *)
-
-let size_itself_int x = integerFromNat (size_itself x)
-
-(* NB: the corresponding sail type is forall 'n. atom('n) -> itself('n),
-   the actual integer is ignored. *)
-
-val make_the_value : forall 'n. integer -> itself 'n
-let inline make_the_value x = the_value
-
-(*** Bit vector operations *)
-
-let bitvector_length 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 bitvector_concat (bs, bs') = word_concat bs bs'
-
-let inline (^^^) = bitvector_concat
-
-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
-  word_extract lo hi bs
-
-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_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
-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 bs 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. 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 of_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
-  word_update bs lo hi 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 => 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 => 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 (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 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 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_basic (start, len, b) = vec_to_bvec (Vector [b] start false)
-let cast_boolvec_bitvec (Vector bs start inc) =
-  vec_to_bvec (Vector (List.map bool_to_bitU bs) start inc)
-let cast_vec_bl v = List.map bool_to_bitU (bitlistFromWord v)
-let cast_int_vec n = wordFromInteger n
-let cast_bl_vec (start, len, bs) = wordFromBitlist (List.map bitU_to_bool bs)
-let cast_bl_svec (start, len, bs) = cast_int_vec (bitlist_to_signed bs)
-
-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 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 bs = lNot bs
-
-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 bs : integer = unsignedIntegerFromWord bs*)
-let unsigned_big = unsigned
-
-let signed 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_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
-  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_norm_vec
-
-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 *)
-
-let to_vec_inc_undef = to_vec_undef true
-let to_vec_dec_undef = to_vec_undef false
-
-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) = to_vec_big (signed_big vec)
-let extz_big (start, len, vec) = to_vec_big (unsigned_big vec)
-
-let quot = hardware_quot
-let modulo (l,r) = hardware_mod l r
-
-(* 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) l r =
-  let (l',r') = (to_num sign l, to_num sign r) in
-  let n = op l' r' in
-  to_norm_vec 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 l r =
-  arith_op_vec op sign size l ((to_norm_vec 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 r =
-  arith_op_vec op sign size ((to_norm_vec 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 x = arith_op_range_vec_range integerAdd false x
-let addS_IVI x = arith_op_range_vec_range integerAdd true x
-let minus_IVI x = arith_op_range_vec_range integerMinus false x
-
-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 x = arith_op_vec_range_range integerAdd false x
-let addS_VII x = arith_op_vec_range_range integerAdd true x
-let minus_VII x = arith_op_vec_range_range integerMinus false x
-
-
-
-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 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) l r =
-  let l' = to_num sign l in
-  let n = op l' (match r with | B1 -> (1 : integer) | _ -> 0 end) in
-  to_norm_vec n
-
-(* add_vec_bit
- * add_vec_bit_signed
- * minus_vec_bit_signed
- *)
-let add_VBV x = arith_op_vec_bit integerAdd false 1 x
-let addS_VBV x = arith_op_vec_bit integerAdd true 1 x
-let minus_VBV x = arith_op_vec_bit integerMinus true 1 x
-
-(* 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 (bs, (n : integer)) =
-  let n = natFromInteger n in
-  match op with
-  | LL_shift (*"<<"*) ->
-     shiftLeft bs n
-  | RR_shift (*">>"*) ->
-     shiftRight bs n
-  | LLL_shift (*"<<<"*) ->
-     rotateLeft n bs
-  end
-
-let bitwise_leftshift x = shift_op_vec LL_shift x (*"<<"*)
-let bitwise_rightshift x = shift_op_vec RR_shift x (*">>"*)
-let bitwise_rotate x = shift_op_vec LLL_shift x (*"<<<"*)
-
-let shiftl = bitwise_leftshift
-let shiftr = bitwise_rightshift
-
-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)
-
-(* TODO: replace with better native versions *)
-let replicate_bits (v, count) =
-  let v = bvec_to_vec true 0 v in
-  vec_to_bvec (Vector (repeat (get_elems v) count) ((length v * count) - 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 x = compare_op_vec (<) true x
-let gt_vec x = compare_op_vec (>) true x
-let lteq_vec x = compare_op_vec (<=) true x
-let gteq_vec x = compare_op_vec (>=) true x
-
-let lt_vec_signed x = compare_op_vec (<) true x
-let gt_vec_signed x = compare_op_vec (>) true x
-let lteq_vec_signed x = compare_op_vec (<=) true x
-let gteq_vec_signed x = compare_op_vec (>=) true x
-let lt_vec_unsigned x = compare_op_vec (<) false x
-let gt_vec_unsigned x = compare_op_vec (>) false x
-let lteq_vec_unsigned x = compare_op_vec (<=) false x
-let gteq_vec_unsigned x = compare_op_vec (>=) false x
-
-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 x = compare_op_vec_range (<) true x
-let gt_vec_range x = compare_op_vec_range (>) true x
-let lteq_vec_range x = compare_op_vec_range (<=) true x
-let gteq_vec_range x = compare_op_vec_range (>=) true x
-
-let compare_op_range_vec op sign (l,r) =
-  compare_op op (l, (to_num sign r))
-
-let lt_range_vec x = compare_op_range_vec (<) true x
-let gt_range_vec x = compare_op_range_vec (>) true x
-let lteq_range_vec x = compare_op_range_vec (<=) true x
-let gteq_range_vec x = compare_op_range_vec (>=) true x
-
-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. 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 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 (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))
-
-
-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, _, w) = (zeroExtend w)
-
-(* Register operations *)
-
-(*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 (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_pos regfield i reg_val bit =
-  let current_field_value = regfield.get_field reg_val in
-  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*)*)
+open import Sail_operators
+
+(* Specialisation of operators to machine words *)
+
+val access_vec_inc : forall 'a. Size 'a => mword 'a -> integer -> bitU
+let access_vec_inc = access_bv_inc
+
+val access_vec_dec : forall 'a. Size 'a => mword 'a -> integer -> bitU
+let access_vec_dec = access_bv_dec
+
+val update_vec_inc : forall 'a. Size 'a => mword 'a -> integer -> bitU -> mword 'a
+let update_vec_inc = update_bv_inc
+
+val update_vec_dec : forall 'a. Size 'a => mword 'a -> integer -> bitU -> mword 'a
+let update_vec_dec = update_bv_dec
+
+val subrange_vec_inc : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b
+let subrange_vec_inc = subrange_bv_inc
+
+val subrange_vec_dec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b
+let subrange_vec_dec = subrange_bv_dec
+
+val update_subrange_vec_inc : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b -> mword 'a
+let update_subrange_vec_inc = update_subrange_bv_inc
+
+val update_subrange_vec_dec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b -> mword 'a
+let update_subrange_vec_dec = update_subrange_bv_dec
+
+val extz_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b
+let extz_vec = extz_bv
+
+val exts_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b
+let exts_vec = exts_bv
+
+val concat_vec : forall 'a 'b 'c. Size 'a, Size 'b, Size 'c => mword 'a -> mword 'b -> mword 'c
+let concat_vec = concat_bv
+
+val cons_vec : forall 'a 'b 'c. Size 'a, Size 'b => bitU -> mword 'a -> mword 'b
+let cons_vec = cons_bv
+
+val bool_of_vec : mword ty1 -> bitU
+let bool_of_vec = bool_of_bv
+
+val cast_unit_vec : bitU -> mword ty1
+let cast_unit_vec = cast_unit_bv
+
+val vec_of_bit : forall 'a. Size 'a => integer -> bitU -> mword 'a
+let vec_of_bit = bv_of_bit
+
+val msb : forall 'a. Size 'a => mword 'a -> bitU
+let msb = most_significant
+
+val int_of_vec : forall 'a. Size 'a => bool -> mword 'a -> integer
+let int_of_vec = int_of_bv
+
+val and_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
+val or_vec  : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
+val xor_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
+val not_vec : forall 'a. Size 'a => mword 'a -> mword 'a
+let and_vec = and_bv
+let or_vec  = or_bv
+let xor_vec = xor_bv
+let not_vec = not_bv
+
+val add_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
+val addS_vec  : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
+val sub_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
+val mult_vec  : forall 'a 'b. Size 'a, Size 'b => mword 'a -> mword 'a -> mword 'b
+val multS_vec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> mword 'a -> mword 'b
+let add_vec   = add_bv
+let addS_vec  = addS_bv
+let sub_vec   = sub_bv
+let mult_vec  = mult_bv
+let multS_vec = multS_bv
+
+val add_vec_int   : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+val addS_vec_int  : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+val sub_vec_int   : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+val mult_vec_int  : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
+val multS_vec_int : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
+let add_vec_int   = add_bv_int
+let addS_vec_int  = addS_bv_int
+let sub_vec_int   = sub_bv_int
+let mult_vec_int  = mult_bv_int
+let multS_vec_int = multS_bv_int
+
+val add_int_vec   : forall 'a. Size 'a => integer -> mword 'a -> mword 'a
+val addS_int_vec  : forall 'a. Size 'a => integer -> mword 'a -> mword 'a
+val sub_int_vec   : forall 'a. Size 'a => integer -> mword 'a -> mword 'a
+val mult_int_vec  : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b
+val multS_int_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b
+let add_int_vec   = add_int_bv
+let addS_int_vec  = addS_int_bv
+let sub_int_vec   = sub_int_bv
+let mult_int_vec  = mult_int_bv
+let multS_int_vec = multS_int_bv
+
+val add_vec_bit  : forall 'a. Size 'a => mword 'a -> bitU -> mword 'a
+val addS_vec_bit : forall 'a. Size 'a => mword 'a -> bitU -> mword 'a
+val sub_vec_bit  : forall 'a. Size 'a => mword 'a -> bitU -> mword 'a
+let add_vec_bit  = add_bv_bit
+let addS_vec_bit = addS_bv_bit
+let sub_vec_bit  = sub_bv_bit
+
+val add_overflow_vec         : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU)
+val add_overflow_vec_signed  : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU)
+val sub_overflow_vec         : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU)
+val sub_overflow_vec_signed  : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU)
+val mult_overflow_vec        : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU)
+val mult_overflow_vec_signed : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU)
+let add_overflow_vec         = add_overflow_bv
+let add_overflow_vec_signed  = add_overflow_bv_signed
+let sub_overflow_vec         = sub_overflow_bv
+let sub_overflow_vec_signed  = sub_overflow_bv_signed
+let mult_overflow_vec        = mult_overflow_bv
+let mult_overflow_vec_signed = mult_overflow_bv_signed
+
+val add_overflow_vec_bit         : forall 'a. Size 'a => mword 'a -> bitU -> (mword 'a * bitU * bitU)
+val add_overflow_vec_bit_signed  : forall 'a. Size 'a => mword 'a -> bitU -> (mword 'a * bitU * bitU)
+val sub_overflow_vec_bit         : forall 'a. Size 'a => mword 'a -> bitU -> (mword 'a * bitU * bitU)
+val sub_overflow_vec_bit_signed  : forall 'a. Size 'a => mword 'a -> bitU -> (mword 'a * bitU * bitU)
+let add_overflow_vec_bit         = add_overflow_bv_bit
+let add_overflow_vec_bit_signed  = add_overflow_bv_bit_signed
+let sub_overflow_vec_bit         = sub_overflow_bv_bit
+let sub_overflow_vec_bit_signed  = sub_overflow_bv_bit_signed
+
+val shiftl       : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+val shiftr       : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+val arith_shiftr : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+val rotl         : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+val rotr         : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+let shiftl       = shiftl_bv
+let shiftr       = shiftr_bv
+let arith_shiftr = arith_shiftr_bv
+let rotl         = rotl_bv
+let rotr         = rotr_bv
+
+val mod_vec         : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
+val quot_vec        : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
+val quot_vec_signed : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
+let mod_vec         = mod_bv
+let quot_vec        = quot_bv
+let quot_vec_signed = quot_bv_signed
+
+val mod_vec_int  : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+val quot_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+let mod_vec_int  = mod_bv_int
+let quot_vec_int = quot_bv_int
+
+val replicate_bits : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
+let replicate_bits = replicate_bits_bv
+
+val duplicate : forall 'a. Size 'a => bitU -> integer -> mword 'a
+let duplicate = duplicate_bit_bv
+
+val eq_vec    : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
+val neq_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
+val ult_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
+val slt_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
+val ugt_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
+val sgt_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
+val ulteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
+val slteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
+val ugteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
+val sgteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
+let eq_vec    = eq_bv
+let neq_vec   = neq_bv
+let ult_vec   = ult_bv
+let slt_vec   = slt_bv
+let ugt_vec   = ugt_bv
+let sgt_vec   = sgt_bv
+let ulteq_vec = ulteq_bv
+let slteq_vec = slteq_bv
+let ugteq_vec = ugteq_bv
+let sgteq_vec = sgteq_bv
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 8aee556d..50dacf5e 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -13,6 +13,17 @@ let pow m n = m ** (natFromInteger n)
 
 let pow2 n = pow 2 n
 
+let inline lt = (<)
+let inline gt = (>)
+let inline lteq = (<=)
+let inline gteq = (>=)
+
+val eq : forall 'a. Eq 'a => 'a -> 'a -> bool
+let inline eq l r = (l = r)
+
+val neq : forall 'a. Eq 'a => 'a -> 'a -> bool
+let inline neq l r = (l <> r)
+
 (*let add_int l r = integerAdd l r
 let add_signed l r = integerAdd l r
 let sub_int l r = integerMinus l r
@@ -58,6 +69,34 @@ let rec replace bs (n : integer) b' = match bs with
 
 let upper n = n
 
+(* Modulus operation corresponding to quot below -- result
+   has sign of dividend. *)
+let hardware_mod (a: integer) (b:integer) : integer =
+  let m = (abs a) mod (abs b) in
+  if a < 0 then ~m else m
+
+(* 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 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)
+
 (*** Bits *)
 type bitU = B0 | B1 | BU
 
@@ -83,7 +122,7 @@ end
 
 let bool_of_bitU = function
   | B0 -> false
-  | B1  -> true
+  | B1 -> true
   | BU -> failwith "bool_of_bitU applied to BU"
   end
 
@@ -272,34 +311,34 @@ let show_bitlist bs =
 
 let inline (^^) = append_list
 
-val slice_list_inc : forall 'a. list 'a -> integer -> integer -> list 'a
-let slice_list_inc xs i j =
+val subrange_list_inc : forall 'a. list 'a -> integer -> integer -> list 'a
+let subrange_list_inc xs i j =
   let (toJ,_suffix) = List.splitAt (natFromInteger j + 1) xs in
   let (_prefix,fromItoJ) = List.splitAt (natFromInteger i) toJ in
   fromItoJ
 
-val slice_list_dec : forall 'a. list 'a -> integer -> integer -> list 'a
-let slice_list_dec xs i j =
+val subrange_list_dec : forall 'a. list 'a -> integer -> integer -> list 'a
+let subrange_list_dec xs i j =
   let top = (length_list xs) - 1 in
-  slice_list_inc xs (top - i) (top - j)
+  subrange_list_inc xs (top - i) (top - j)
 
-val slice_list : forall 'a. bool -> list 'a -> integer -> integer -> list 'a
-let slice_list is_inc xs i j = if is_inc then slice_list_inc xs i j else slice_list_dec xs i j
+val subrange_list : forall 'a. bool -> list 'a -> integer -> integer -> list 'a
+let subrange_list is_inc xs i j = if is_inc then subrange_list_inc xs i j else subrange_list_dec xs i j
 
-val update_slice_list_inc : forall 'a. list 'a -> integer -> integer -> list 'a -> list 'a
-let update_slice_list_inc xs i j xs' =
+val update_subrange_list_inc : forall 'a. list 'a -> integer -> integer -> list 'a -> list 'a
+let update_subrange_list_inc xs i j xs' =
   let (toJ,suffix) = List.splitAt (natFromInteger j + 1) xs in
   let (prefix,_fromItoJ) = List.splitAt (natFromInteger i) toJ in
   prefix ++ xs' ++ suffix
 
-val update_slice_list_dec : forall 'a. list 'a -> integer -> integer -> list 'a -> list 'a
-let update_slice_list_dec xs i j xs' =
+val update_subrange_list_dec : forall 'a. list 'a -> integer -> integer -> list 'a -> list 'a
+let update_subrange_list_dec xs i j xs' =
   let top = (length_list xs) - 1 in
-  update_slice_list_inc xs (top - i) (top - j) xs'
+  update_subrange_list_inc xs (top - i) (top - j) xs'
 
-val update_slice_list : forall 'a. bool -> list 'a -> integer -> integer -> list 'a -> list 'a
-let update_slice_list is_inc xs i j xs' =
-  if is_inc then update_slice_list_inc xs i j xs' else update_slice_list_dec xs i j xs'
+val update_subrange_list : forall 'a. bool -> list 'a -> integer -> integer -> list 'a -> list 'a
+let update_subrange_list is_inc xs i j xs' =
+  if is_inc then update_subrange_list_inc xs i j xs' else update_subrange_list_dec xs i j xs'
 
 val access_list_inc : forall 'a. list 'a -> integer -> 'a
 let access_list_inc xs n = List_extra.nth xs (natFromInteger n)
@@ -383,11 +422,28 @@ val update_mword : forall 'a. bool -> mword 'a -> integer -> bitU -> mword 'a
 let update_mword is_inc w n b =
   if is_inc then update_mword_inc w n b else update_mword_dec w n b
 
+val mword_of_int : forall 'a. Size 'a => integer -> integer -> mword 'a
+let mword_of_int len n =
+  let w = wordFromInteger n in
+  if (length_mword w = len) then w else failwith "unexpected word length"
+
+(* Translating between a type level number (itself 'n) and an integer *)
+
+let size_itself_int x = integerFromNat (size_itself x)
+
+(* NB: the corresponding sail type is forall 'n. atom('n) -> itself('n),
+   the actual integer is ignored. *)
+
+val make_the_value : forall 'n. integer -> itself 'n
+let inline make_the_value x = the_value
+
 (*** Bitvectors *)
 
 class (Bitvector 'a)
   val bits_of : 'a -> list bitU
   val of_bits : list bitU -> 'a
+  (* The first parameter specifies the desired length of the bitvector *)
+  val of_int : integer -> integer -> 'a
   val length : 'a -> integer
   val unsigned : 'a -> integer
   val signed : 'a -> integer
@@ -401,44 +457,46 @@ end
 instance forall 'a. BitU 'a => (Bitvector (list 'a))
   let bits_of v = List.map to_bitU v
   let of_bits v = List.map of_bitU v
-  let length v = length_list v
+  let of_int len n = List.map of_bitU (bits_of_int len n)
+  let length = length_list
   let unsigned v = unsigned_of_bits (List.map to_bitU v)
   let signed v = signed_of_bits (List.map to_bitU v)
   let get_bit is_inc v n = to_bitU (access_list is_inc v n)
   let set_bit is_inc v n b = update_list is_inc v n (of_bitU b)
-  let get_bits is_inc v i j = List.map to_bitU (slice_list is_inc v i j)
-  let set_bits is_inc v i j v' = update_slice_list is_inc v i j (List.map of_bitU v')
+  let get_bits is_inc v i j = List.map to_bitU (subrange_list is_inc v i j)
+  let set_bits is_inc v i j v' = update_subrange_list is_inc v i j (List.map of_bitU v')
 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 of_bitU v)
+  let of_int = mword_of_int
   let length v = integerFromNat (word_length v)
-  let unsigned v = unsignedIntegerFromWord v
-  let signed v = signedIntegerFromWord v
+  let unsigned = unsignedIntegerFromWord
+  let signed = signedIntegerFromWord
   let get_bit = access_mword
   let set_bit = update_mword
   let get_bits is_inc v i j = get_bits is_inc (bitlistFromWord v) i j
   let set_bits is_inc v i j v' = wordFromBitlist (set_bits is_inc (bitlistFromWord v) i j v')
 end
 
-let access_vec_inc v n = get_bit true  v n
-let access_vec_dec v n = get_bit false v n
+let access_bv_inc v n = get_bit true  v n
+let access_bv_dec v n = get_bit false v n
 
-let update_vec_inc v n b = set_bit true  v n b
-let update_vec_dec v n b = set_bit false v n b
+let update_bv_inc v n b = set_bit true  v n b
+let update_bv_dec v n b = set_bit false v n b
 
-let subrange_vec_inc v i j = of_bits (get_bits true  v i j)
-let subrange_vec_dec v i j = of_bits (get_bits false v i j)
+let subrange_bv_inc v i j = of_bits (get_bits true  v i j)
+let subrange_bv_dec v i j = of_bits (get_bits false v i j)
 
-let update_subrange_vec_inc v i j v' = set_bits true  v i j (bits_of v')
-let update_subrange_vec_dec v i j v' = set_bits false v i j (bits_of v')
+let update_subrange_bv_inc v i j v' = set_bits true  v i j (bits_of v')
+let update_subrange_bv_dec v i j v' = set_bits false v i j (bits_of v')
 
-val extz_vec : forall 'a 'b. Bitvector 'a, Bitvector 'b => integer -> 'a -> 'b
-let extz_vec n v = of_bits (extz_bits n (bits_of v))
+val extz_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b => integer -> 'a -> 'b
+let extz_bv n v = of_bits (extz_bits n (bits_of v))
 
-val exts_vec : forall 'a 'b. Bitvector 'a, Bitvector 'b => integer -> 'a -> 'b
-let exts_vec n v = of_bits (exts_bits n (bits_of v))
+val exts_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b => integer -> 'a -> 'b
+let exts_bv n v = of_bits (exts_bits n (bits_of v))
 
 (*** Bytes and addresses *)
 
@@ -584,13 +642,13 @@ let rec external_reg_value reg_name v =
     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) ->
+     | Reg_slice _ reg_start dir (slice_start, _) ->
         ((if dir = D_increasing then slice_start else (reg_start - slice_start)),
          slice_start, dir)
-     | Reg_field _ reg_start dir _ (slice_start, slice_end) ->
+     | Reg_field _ reg_start dir _ (slice_start, _) ->
         ((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) ->
+     | Reg_f_slice _ reg_start dir _ _ (slice_start, _) ->
         ((if dir = D_increasing then slice_start else (reg_start - slice_start)),
          slice_start, dir) 
      end in
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index b6852aaf..ac6d55b5 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -1,253 +1,8 @@
 open import Pervasives_extra
 open import Sail_impl_base
 open import Sail_values
-
-(* 'a is result type *)
-
-type memstate = map integer memory_byte
-type tagstate = map integer bitU
-(* type regstate = map string (vector bitU) *)
-
-type sequential_state 'regs =
-  <| regstate : 'regs;
-     memstate : memstate;
-     tagstate : tagstate;
-     write_ea : maybe (write_kind * integer * integer);
-     last_exclusive_operation_was_load : bool|>
-
-val init_state : forall 'regs. 'regs -> sequential_state 'regs
-let init_state regs =
-  <| regstate = regs;
-     memstate = Map.empty;
-     tagstate = Map.empty;
-     write_ea = Nothing;
-     last_exclusive_operation_was_load = false |>
-
-type ex 'e =
-  | Exit
-  | Assert of string
-  | Throw of 'e
-
-type result 'a 'e =
-  | Value of 'a
-  | Exception of (ex 'e)
-
-(* State, nondeterminism and exception monad with result value type 'a
-   and exception type 'e. *)
-type M 'regs 'a 'e = sequential_state 'regs -> list (result 'a 'e * sequential_state 'regs)
-
-val return : forall 'regs 'a 'e. 'a -> M 'regs 'a 'e
-let return a s = [(Value a,s)]
-
-val bind : forall 'regs 'a 'b 'e. M 'regs 'a 'e -> ('a -> M 'regs 'b 'e) -> M 'regs 'b 'e
-let bind m f (s : sequential_state 'regs) =
-  List.concatMap (function
-                  | (Value a, s') -> f a s'
-                  | (Exception e, s') -> [(Exception e, s')]
-                  end) (m s)
-
-let inline (>>=) = bind
-val (>>): forall 'regs 'b 'e. M 'regs unit 'e -> M 'regs 'b 'e -> M 'regs 'b 'e
-let inline (>>) m n = m >>= fun (_ : unit) -> n
-
-val throw : forall 'regs 'a 'e. 'e -> M 'regs 'a 'e
-let throw e s = [(Exception (Throw e), s)]
-
-val try_catch : forall 'regs 'a 'e1 'e2. M 'regs 'a 'e1 -> ('e1 -> M 'regs 'a 'e2) ->  M 'regs 'a 'e2
-let try_catch m h s =
-  List.concatMap (function
-                  | (Value a, s') -> return a s'
-                  | (Exception (Throw e), s') -> h e s'
-                  | (Exception Exit, s') -> [(Exception Exit, s')]
-                  | (Exception (Assert msg), s') -> [(Exception (Assert msg), s')]
-                  end) (m s)
-
-val exit : forall 'regs 'e 'a. unit -> M 'regs 'a 'e
-let exit () s = [(Exception Exit, s)]
-
-val assert_exp : forall 'regs 'e. bool -> string -> M 'regs unit 'e
-let assert_exp exp msg s = if exp then [(Value (), s)] else [(Exception (Assert msg), s)]
-
-(* For early return, we abuse exceptions by throwing and catching
-   the return value. The exception type is "either 'r 'e", where "Right e"
-   represents a proper exception and "Left r" an early return of value "r". *)
-type MR 'regs 'a 'r 'e = M 'regs 'a (either 'r 'e)
-
-val early_return : forall 'regs 'a 'r 'e. 'r -> MR 'regs 'a 'r 'e
-let early_return r = throw (Left r)
-
-val catch_early_return : forall 'regs 'a 'e. MR 'regs 'a 'a 'e -> M 'regs 'a 'e
-let catch_early_return m =
-  try_catch m
-    (function
-      | Left a -> return a
-      | Right e -> throw e
-     end)
-
-(* Lift to monad with early return by wrapping exceptions *)
-val liftR : forall 'a 'r 'regs 'e. M 'regs 'a 'e -> MR 'regs 'a 'r 'e
-let liftR m = try_catch m (fun e -> throw (Right e))
-
-(* Catch exceptions in the presence of early returns *)
-val try_catchR : forall 'regs 'a 'r 'e1 'e2. MR 'regs 'a 'r 'e1 -> ('e1 -> MR 'regs 'a 'r 'e2) ->  MR 'regs 'a 'r 'e2
-let try_catchR m h =
-  try_catch m
-    (function
-      | Left r -> throw (Left r)
-      | Right e -> h e
-     end)
-
-val range : integer -> integer -> list integer
-let rec range i j =
-  if j < i then []
-  else if i = j then [i]
-  else i :: range (i+1) j
-
-val get_reg : forall 'regs 'a. sequential_state 'regs -> register_ref 'regs 'a -> 'a
-let get_reg state reg = reg.read_from state.regstate
-
-val set_reg : forall 'regs 'a. sequential_state 'regs -> register_ref 'regs 'a -> 'a -> sequential_state 'regs
-let set_reg state reg v =
-  <| state with regstate = reg.write_to state.regstate v |>
-
-
-let is_exclusive = function
-  | Sail_impl_base.Read_plain -> false
-  | Sail_impl_base.Read_reserve -> true
-  | Sail_impl_base.Read_acquire -> false
-  | Sail_impl_base.Read_exclusive -> true
-  | Sail_impl_base.Read_exclusive_acquire -> true
-  | Sail_impl_base.Read_stream -> false
-  | Sail_impl_base.Read_RISCV_acquire -> false
-  | Sail_impl_base.Read_RISCV_strong_acquire -> false
-  | Sail_impl_base.Read_RISCV_reserved -> true
-  | Sail_impl_base.Read_RISCV_reserved_acquire -> true
-  | Sail_impl_base.Read_RISCV_reserved_strong_acquire -> true
-  | Sail_impl_base.Read_X86_locked -> true
-end
-
-
-val read_mem : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> M 'regs 'b 'e
-let read_mem 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 = of_bits (Sail_values.internal_mem_value memory_value) in
-  if is_exclusive read_kind
-  then [(Value value, <| state with last_exclusive_operation_was_load = true |>)]
-  else [(Value value, state)]
-
-(* caps are aligned at 32 bytes *)
-let cap_alignment = (32 : integer)
-
-val read_tag : forall 'regs 'a 'e. Bitvector 'a => read_kind -> 'a -> M 'regs bitU 'e
-let read_tag read_kind addr state =
-  let addr = (unsigned addr) / cap_alignment in
-  let tag = match (Map.lookup addr state.tagstate) with
-    | Just t -> t
-    | Nothing -> B0
-  end in
-  if is_exclusive read_kind
-  then [(Value tag, <| state with last_exclusive_operation_was_load = true |>)]
-  else [(Value tag, state)]
-
-val excl_result : forall 'regs 'e. unit -> M 'regs bool 'e
-let excl_result () state =
-  let success =
-    (Value true,  <| state with last_exclusive_operation_was_load = false |>) in
-  (Value false, state) :: if state.last_exclusive_operation_was_load then [success] else []
-
-val write_mem_ea : forall 'regs 'a 'e. Bitvector 'a => write_kind -> 'a -> integer -> M 'regs unit 'e
-let write_mem_ea write_kind addr sz state = 
-  [(Value (), <| state with write_ea = Just (write_kind,unsigned addr,sz) |>)]
-
-val write_mem_val : forall 'a 'regs 'b 'e. Bitvector 'a => 'a -> M 'regs bool 'e
-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 (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
-  [(Value true,  <| state with memstate = memstate |>)]
-
-val write_tag : forall 'regs 'e. bitU -> M 'regs bool 'e
-let write_tag t 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 taddr = addr / cap_alignment in
-  let tagstate = Map.insert taddr t state.tagstate in
-  [(Value true,  <| state with tagstate = tagstate |>)]
-
-val read_reg : forall 'regs 'a 'e. register_ref 'regs 'a -> M 'regs 'a 'e
-let read_reg reg state =
-  let v = reg.read_from state.regstate in
-  [(Value v,state)]
-(*let read_reg_range reg i j state =
-  let v = slice (get_reg state (name_of_reg reg)) i j in
-  [(Value (vec_to_bvec v),state)]
-let read_reg_bit reg i state =
-  let v = access (get_reg state (name_of_reg reg)) i in
-  [(Value v,state)]
-let read_reg_field reg regfield =
-  let (i,j) = register_field_indices reg regfield in
-  read_reg_range reg i j
-let read_reg_bitfield reg regfield =
-  let (i,_) = register_field_indices reg regfield in
-  read_reg_bit reg i *)
-
-let reg_deref = read_reg
-
-val write_reg : forall 'regs 'a 'e. register_ref 'regs 'a -> 'a -> M 'regs unit 'e
-let write_reg reg v state =
-  [(Value (), <| state with regstate = reg.write_to state.regstate v |>)]
-
-let write_reg_ref (reg, v) = write_reg reg v
-
-val update_reg : forall 'regs 'a 'b 'e. register_ref 'regs 'a -> ('a -> 'b -> 'a) -> 'b -> M 'regs unit 'e
-let update_reg reg f v state =
-  let current_value = get_reg state reg in
-  let new_value = f current_value v in
-  [(Value (), 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_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_list reg.reg_is_inc 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_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) 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_list regfield.field_is_inc 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) 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 'e. barrier_kind -> M 'regs unit 'e
-let barrier _ = return ()
-
-val footprint : forall 'regs 'e. M 'regs unit 'e
-let footprint s = return () s
+open import State_monad
+open import {isabelle} `State_monad_extras`
 
 val iter_aux : forall 'regs 'e 'a. integer -> (integer -> 'a -> M 'regs unit 'e) -> list 'a -> M 'regs unit 'e
 let rec iter_aux i f xs = match xs with
@@ -286,24 +41,30 @@ let rec while_PP vars cond body =
 
 val while_PM : forall 'regs 'vars 'e. 'vars -> ('vars -> bool) ->
                 ('vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e
-let rec while_PM vars cond body =
+let rec while_PM vars cond body s =
   if cond vars then
-    body vars >>= fun vars -> while_PM vars cond body
-  else return vars
+    bind (body vars) (fun vars s' -> while_PM vars cond body s') s
+  else return vars s
 
 val while_MP : forall 'regs 'vars 'e. 'vars -> ('vars -> M 'regs bool 'e) ->
                 ('vars -> 'vars) -> M 'regs 'vars 'e
-let rec while_MP vars cond body =
-  cond vars >>= fun cond_val ->
-  if cond_val then while_MP (body vars) cond body else return vars
+let rec while_MP vars cond body s =
+  bind
+    (cond vars)
+    (fun cond_val s' ->
+      if cond_val then while_MP (body vars) cond body s' else return vars s') s
 
 val while_MM : forall 'regs 'vars 'e. 'vars -> ('vars -> M 'regs bool 'e) ->
                 ('vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e
-let rec while_MM vars cond body =
-  cond vars >>= fun cond_val ->
-  if cond_val then
-    body vars >>= fun vars -> while_MM vars cond body
-  else return vars
+let rec while_MM vars cond body s =
+  bind
+    (cond vars)
+    (fun cond_val s' ->
+      if cond_val then
+        bind
+          (body vars)
+          (fun vars s'' -> while_MM vars cond body s'') s'
+      else return vars s') s
 
 val until_PP : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
 let rec until_PP vars cond body =
@@ -312,44 +73,28 @@ let rec until_PP vars cond body =
 
 val until_PM : forall 'regs 'vars 'e. 'vars -> ('vars -> bool) ->
                 ('vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e
-let rec until_PM vars cond body =
-  body vars >>= fun vars ->
-  if (cond vars) then return vars else until_PM vars cond body
+let rec until_PM vars cond body s =
+  bind
+    (body vars)
+    (fun vars s' ->
+      if (cond vars) then return vars s' else until_PM vars cond body s') s
 
 val until_MP : forall 'regs 'vars 'e. 'vars -> ('vars -> M 'regs bool 'e) ->
                 ('vars -> 'vars) -> M 'regs 'vars 'e
-let rec until_MP vars cond body =
+let rec until_MP vars cond body s =
   let vars = body vars in
-  cond vars >>= fun cond_val ->
-  if cond_val then return vars else until_MP vars cond body
+  bind
+    (cond vars)
+    (fun cond_val s' ->
+      if cond_val then return vars s' else until_MP vars cond body s') s
 
 val until_MM : forall 'regs 'vars 'e. 'vars -> ('vars -> M 'regs bool 'e) ->
                 ('vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e
-let rec until_MM vars cond body =
-  body vars >>= fun vars ->
-  cond vars >>= fun cond_val ->
-  if cond_val then return vars else until_MM vars cond body
-
-(*let write_two_regs r1 r2 bvec state =
-  let vec = bvec_to_vec bvec in
-  let is_inc =
-    let is_inc_r1 = is_inc_of_reg r1 in
-    let is_inc_r2 = is_inc_of_reg r2 in
-    let () = ensure (is_inc_r1 = is_inc_r2)
-                    "write_two_regs called with vectors of different direction" in
-    is_inc_r1 in
-
-  let (size_r1 : integer) = size_of_reg r1 in
-  let (start_vec : integer) = get_start vec in
-  let size_vec = length vec in
-  let r1_v =
-    if is_inc
-    then slice vec start_vec (size_r1 - start_vec - 1)
-    else slice vec start_vec (start_vec - size_r1 - 1) in
-  let r2_v =
-    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
-  let state1 = set_reg state (name_of_reg r1) r1_v in
-  let state2 = set_reg state1 (name_of_reg r2) r2_v in
-  [(Left (), state2)]*)
+let rec until_MM vars cond body s =
+  bind
+    (body vars)
+    (fun vars s' ->
+      bind
+        (cond vars)
+        (fun cond_val s''->
+          if cond_val then return vars s'' else until_MM vars cond body s'') s') s
diff --git a/src/gen_lib/state_monad.lem b/src/gen_lib/state_monad.lem
new file mode 100644
index 00000000..2d8e412e
--- /dev/null
+++ b/src/gen_lib/state_monad.lem
@@ -0,0 +1,250 @@
+open import Pervasives_extra
+open import Sail_impl_base
+open import Sail_values
+
+(* 'a is result type *)
+
+type memstate = map integer memory_byte
+type tagstate = map integer bitU
+(* type regstate = map string (vector bitU) *)
+
+type sequential_state 'regs =
+  <| regstate : 'regs;
+     memstate : memstate;
+     tagstate : tagstate;
+     write_ea : maybe (write_kind * integer * integer);
+     last_exclusive_operation_was_load : bool|>
+
+val init_state : forall 'regs. 'regs -> sequential_state 'regs
+let init_state regs =
+  <| regstate = regs;
+     memstate = Map.empty;
+     tagstate = Map.empty;
+     write_ea = Nothing;
+     last_exclusive_operation_was_load = false |>
+
+type ex 'e =
+  | Exit
+  | Assert of string
+  | Throw of 'e
+
+type result 'a 'e =
+  | Value of 'a
+  | Exception of (ex 'e)
+
+(* State, nondeterminism and exception monad with result value type 'a
+   and exception type 'e. *)
+type M 'regs 'a 'e = sequential_state 'regs -> list (result 'a 'e * sequential_state 'regs)
+
+val return : forall 'regs 'a 'e. 'a -> M 'regs 'a 'e
+let return a s = [(Value a,s)]
+
+val bind : forall 'regs 'a 'b 'e. M 'regs 'a 'e -> ('a -> M 'regs 'b 'e) -> M 'regs 'b 'e
+let bind m f (s : sequential_state 'regs) =
+  List.concatMap (function
+                  | (Value a, s') -> f a s'
+                  | (Exception e, s') -> [(Exception e, s')]
+                  end) (m s)
+
+let inline (>>=) = bind
+val (>>): forall 'regs 'b 'e. M 'regs unit 'e -> M 'regs 'b 'e -> M 'regs 'b 'e
+let inline (>>) m n = m >>= fun (_ : unit) -> n
+
+val throw : forall 'regs 'a 'e. 'e -> M 'regs 'a 'e
+let throw e s = [(Exception (Throw e), s)]
+
+val try_catch : forall 'regs 'a 'e1 'e2. M 'regs 'a 'e1 -> ('e1 -> M 'regs 'a 'e2) ->  M 'regs 'a 'e2
+let try_catch m h s =
+  List.concatMap (function
+                  | (Value a, s') -> return a s'
+                  | (Exception (Throw e), s') -> h e s'
+                  | (Exception Exit, s') -> [(Exception Exit, s')]
+                  | (Exception (Assert msg), s') -> [(Exception (Assert msg), s')]
+                  end) (m s)
+
+val exit : forall 'regs 'e 'a. unit -> M 'regs 'a 'e
+let exit () s = [(Exception Exit, s)]
+
+val assert_exp : forall 'regs 'e. bool -> string -> M 'regs unit 'e
+let assert_exp exp msg s = if exp then [(Value (), s)] else [(Exception (Assert msg), s)]
+
+(* For early return, we abuse exceptions by throwing and catching
+   the return value. The exception type is "either 'r 'e", where "Right e"
+   represents a proper exception and "Left r" an early return of value "r". *)
+type MR 'regs 'a 'r 'e = M 'regs 'a (either 'r 'e)
+
+val early_return : forall 'regs 'a 'r 'e. 'r -> MR 'regs 'a 'r 'e
+let early_return r = throw (Left r)
+
+val catch_early_return : forall 'regs 'a 'e. MR 'regs 'a 'a 'e -> M 'regs 'a 'e
+let catch_early_return m =
+  try_catch m
+    (function
+      | Left a -> return a
+      | Right e -> throw e
+     end)
+
+(* Lift to monad with early return by wrapping exceptions *)
+val liftR : forall 'a 'r 'regs 'e. M 'regs 'a 'e -> MR 'regs 'a 'r 'e
+let liftR m = try_catch m (fun e -> throw (Right e))
+
+(* Catch exceptions in the presence of early returns *)
+val try_catchR : forall 'regs 'a 'r 'e1 'e2. MR 'regs 'a 'r 'e1 -> ('e1 -> MR 'regs 'a 'r 'e2) ->  MR 'regs 'a 'r 'e2
+let try_catchR m h =
+  try_catch m
+    (function
+      | Left r -> throw (Left r)
+      | Right e -> h e
+     end)
+
+val range : integer -> integer -> list integer
+let rec range i j =
+  if j < i then []
+  else if i = j then [i]
+  else i :: range (i+1) j
+
+val get_reg : forall 'regs 'a. sequential_state 'regs -> register_ref 'regs 'a -> 'a
+let get_reg state reg = reg.read_from state.regstate
+
+val set_reg : forall 'regs 'a. sequential_state 'regs -> register_ref 'regs 'a -> 'a -> sequential_state 'regs
+let set_reg state reg v =
+  <| state with regstate = reg.write_to state.regstate v |>
+
+
+let is_exclusive = function
+  | Sail_impl_base.Read_plain -> false
+  | Sail_impl_base.Read_reserve -> true
+  | Sail_impl_base.Read_acquire -> false
+  | Sail_impl_base.Read_exclusive -> true
+  | Sail_impl_base.Read_exclusive_acquire -> true
+  | Sail_impl_base.Read_stream -> false
+  | Sail_impl_base.Read_RISCV_acquire -> false
+  | Sail_impl_base.Read_RISCV_strong_acquire -> false
+  | Sail_impl_base.Read_RISCV_reserved -> true
+  | Sail_impl_base.Read_RISCV_reserved_acquire -> true
+  | Sail_impl_base.Read_RISCV_reserved_strong_acquire -> true
+  | Sail_impl_base.Read_X86_locked -> true
+end
+
+
+val read_mem : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> M 'regs 'b 'e
+let read_mem 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 = of_bits (Sail_values.internal_mem_value memory_value) in
+  if is_exclusive read_kind
+  then [(Value value, <| state with last_exclusive_operation_was_load = true |>)]
+  else [(Value value, state)]
+
+(* caps are aligned at 32 bytes *)
+let cap_alignment = (32 : integer)
+
+val read_tag : forall 'regs 'a 'e. Bitvector 'a => read_kind -> 'a -> M 'regs bitU 'e
+let read_tag read_kind addr state =
+  let addr = (unsigned addr) / cap_alignment in
+  let tag = match (Map.lookup addr state.tagstate) with
+    | Just t -> t
+    | Nothing -> B0
+  end in
+  if is_exclusive read_kind
+  then [(Value tag, <| state with last_exclusive_operation_was_load = true |>)]
+  else [(Value tag, state)]
+
+val excl_result : forall 'regs 'e. unit -> M 'regs bool 'e
+let excl_result () state =
+  let success =
+    (Value true,  <| state with last_exclusive_operation_was_load = false |>) in
+  (Value false, state) :: if state.last_exclusive_operation_was_load then [success] else []
+
+val write_mem_ea : forall 'regs 'a 'e. Bitvector 'a => write_kind -> 'a -> integer -> M 'regs unit 'e
+let write_mem_ea write_kind addr sz state =
+  [(Value (), <| state with write_ea = Just (write_kind,unsigned addr,sz) |>)]
+
+val write_mem_val : forall 'a 'regs 'b 'e. Bitvector 'a => 'a -> M 'regs bool 'e
+let write_mem_val v state =
+  let (_,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 (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
+  [(Value true,  <| state with memstate = memstate |>)]
+
+val write_tag : forall 'regs 'e. bitU -> M 'regs bool 'e
+let write_tag t state =
+  let (_,addr,_) = match state.write_ea with
+    | Nothing -> failwith "write ea has not been announced yet"
+    | Just write_ea -> write_ea end in
+  let taddr = addr / cap_alignment in
+  let tagstate = Map.insert taddr t state.tagstate in
+  [(Value true,  <| state with tagstate = tagstate |>)]
+
+val read_reg : forall 'regs 'a 'e. register_ref 'regs 'a -> M 'regs 'a 'e
+let read_reg reg state =
+  let v = reg.read_from state.regstate in
+  [(Value v,state)]
+(*let read_reg_range reg i j state =
+  let v = slice (get_reg state (name_of_reg reg)) i j in
+  [(Value (vec_to_bvec v),state)]
+let read_reg_bit reg i state =
+  let v = access (get_reg state (name_of_reg reg)) i in
+  [(Value v,state)]
+let read_reg_field reg regfield =
+  let (i,j) = register_field_indices reg regfield in
+  read_reg_range reg i j
+let read_reg_bitfield reg regfield =
+  let (i,_) = register_field_indices reg regfield in
+  read_reg_bit reg i *)
+
+let reg_deref = read_reg
+
+val write_reg : forall 'regs 'a 'e. register_ref 'regs 'a -> 'a -> M 'regs unit 'e
+let write_reg reg v state =
+  [(Value (), <| state with regstate = reg.write_to state.regstate v |>)]
+
+let write_reg_ref (reg, v) = write_reg reg v
+
+val update_reg : forall 'regs 'a 'b 'e. register_ref 'regs 'a -> ('a -> 'b -> 'a) -> 'b -> M 'regs unit 'e
+let update_reg reg f v state =
+  let current_value = get_reg state reg in
+  let new_value = f current_value v in
+  [(Value (), 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_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_list reg.reg_is_inc 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_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) 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_list regfield.field_is_inc 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) 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 'e. barrier_kind -> M 'regs unit 'e
+let barrier _ = return ()
+
+val footprint : forall 'regs 'e. M 'regs unit 'e
+let footprint s = return () s