Add some lemmas about bitvectors

Also clean up some library functions a bit, and add some missing failure
handling variants of division operations on bitvectors.

6 files changed, 161 insertions, 43 deletions

diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 8214bf49..de683047 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -67,6 +67,11 @@ let of_bits_oracle bits =
 val of_bits_fail : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monad 'rv 'a 'e
 let of_bits_fail bits = maybe_fail "of_bits" (of_bits bits)
 
+val mword_oracle : forall 'rv 'a 'e. Size 'a => unit -> monad 'rv (mword 'a) 'e
+let mword_oracle () =
+  bools_of_bits_oracle (repeat [BU] (integerFromNat size)) >>= (fun bs ->
+  return (wordFromBitlist bs))
+
 val whileM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
                 ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
 let rec whileM vars cond body =
diff --git a/src/gen_lib/prompt_monad.lem b/src/gen_lib/prompt_monad.lem
index b1dd59c4..9eb59319 100644
--- a/src/gen_lib/prompt_monad.lem
+++ b/src/gen_lib/prompt_monad.lem
@@ -34,10 +34,8 @@ type monad 'regval 'a 'e =
   | Print of string * monad 'regval 'a 'e
   (*Result of a failed assert with possible error message to report*)
   | Fail of string
-  | Error of string
   (* Exception of type 'e *)
   | Exception of 'e
-  (* TODO: Reading/writing tags *)
 
 val return : forall 'rv 'a 'e. 'a -> monad 'rv 'a 'e
 let return a = Done a
@@ -58,7 +56,6 @@ let rec bind m f = match m with
   | Write_reg r v k ->    Write_reg r v    (bind k f)
   | Print msg k ->        Print msg        (bind k f)
   | Fail descr ->         Fail descr
-  | Error descr ->        Error descr
   | Exception e ->        Exception e
 end
 
@@ -90,7 +87,6 @@ let rec try_catch m h = match m with
   | Write_reg r v k ->    Write_reg r v    (try_catch k h)
   | Print msg k ->        Print msg        (try_catch k h)
   | Fail descr ->         Fail descr
-  | Error descr ->        Error descr
   | Exception e ->        h e
 end
 
@@ -165,7 +161,7 @@ let read_reg reg =
   let k v =
     match reg.of_regval v with
       | Just v -> Done v
-      | Nothing -> Error "read_reg: unrecognised value"
+      | Nothing -> Fail "read_reg: unrecognised value"
     end
   in
   Read_reg reg.name k
diff --git a/src/gen_lib/sail_operators_bitlists.lem b/src/gen_lib/sail_operators_bitlists.lem
index 18c90c66..132ea84f 100644
--- a/src/gen_lib/sail_operators_bitlists.lem
+++ b/src/gen_lib/sail_operators_bitlists.lem
@@ -129,39 +129,46 @@ let arith_op_double_bl op sign l r =
 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 subs_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   = arith_op_bv integerAdd false
 let adds_vec  = arith_op_bv integerAdd true
 let sub_vec   = arith_op_bv integerMinus false
+let subs_vec  = arith_op_bv integerMinus true
 let mult_vec  = arith_op_double_bl integerMult false
 let mults_vec = arith_op_double_bl integerMult true
 
 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 subs_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   l r = arith_op_bv_int integerAdd false l r
 let adds_vec_int  l r = arith_op_bv_int integerAdd true l r
 let sub_vec_int   l r = arith_op_bv_int integerMinus false l r
+let subs_vec_int  l r = arith_op_bv_int integerMinus true l r
 let mult_vec_int  l r = arith_op_double_bl integerMult false l (of_int (length l) r)
 let mults_vec_int l r = arith_op_double_bl integerMult true l (of_int (length l) r)
 
 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 subs_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   l r = arith_op_int_bv integerAdd false l r
 let adds_int_vec  l r = arith_op_int_bv integerAdd true l r
 let sub_int_vec   l r = arith_op_int_bv integerMinus false l r
+let subs_int_vec  l r = arith_op_int_bv integerMinus true l r
 let mult_int_vec  l r = arith_op_double_bl integerMult false (of_int (length r) l) r
 let mults_int_vec l r = arith_op_double_bl integerMult true (of_int (length r) l) r
 
 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
+val subs_vec_bit     : list bitU -> bitU -> list bitU
 
 let add_vec_bool       l r = arith_op_bv_bool integerAdd false l r
 let add_vec_bit_maybe  l r = arith_op_bv_bit integerAdd false l r
@@ -181,6 +188,12 @@ let sub_vec_bit_fail    l r = maybe_fail "sub_vec_bit" (sub_vec_bit_maybe l r)
 let sub_vec_bit_oracle  l r = bool_of_bitU_oracle r >>= (fun r -> return (sub_vec_bool l r))
 let sub_vec_bit         l r = fromMaybe (repeat [BU] (length l)) (sub_vec_bit_maybe l r)
 
+let subs_vec_bool       l r = arith_op_bv_bool integerMinus true l r
+let subs_vec_bit_maybe  l r = arith_op_bv_bit integerMinus true l r
+let subs_vec_bit_fail   l r = maybe_fail "sub_vec_bit" (subs_vec_bit_maybe l r)
+let subs_vec_bit_oracle l r = bool_of_bitU_oracle r >>= (fun r -> return (subs_vec_bool l r))
+let subs_vec_bit        l r = fromMaybe (repeat [BU] (length l)) (subs_vec_bit_maybe l r)
+
 (*val add_overflow_vec         : list bitU -> list bitU -> (list bitU * bitU * bitU)
 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)
@@ -214,17 +227,50 @@ 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 quots_vec     : list bitU -> list bitU -> list bitU
-let mod_vec   l r = fromMaybe (repeat [BU] (length l)) (mod_bv l r)
-let quot_vec  l r = fromMaybe (repeat [BU] (length l)) (quot_bv l r)
-let quots_vec l r = fromMaybe (repeat [BU] (length l)) (quots_bv l r)
-
-val mod_vec_int      : list bitU -> integer -> list bitU
-val quot_vec_int     : list bitU -> integer -> list bitU
-let mod_vec_int  l r = fromMaybe (repeat [BU] (length l)) (mod_bv_int l r)
-let quot_vec_int l r = fromMaybe (repeat [BU] (length l)) (quot_bv_int l r)
+val mod_vec        : list bitU -> list bitU -> list bitU
+val mod_vec_maybe  : list bitU -> list bitU -> maybe (list bitU)
+val mod_vec_fail   : forall 'rv 'e. list bitU -> list bitU -> monad 'rv (list bitU) 'e
+val mod_vec_oracle : forall 'rv 'e. list bitU -> list bitU -> monad 'rv (list bitU) 'e
+let mod_vec        l r = fromMaybe (repeat [BU] (length l)) (mod_bv l r)
+let mod_vec_maybe  l r = mod_bv l r
+let mod_vec_fail   l r = maybe_fail "mod_vec" (mod_bv l r)
+let mod_vec_oracle l r = of_bits_oracle (mod_vec l r)
+
+val quot_vec        : list bitU -> list bitU -> list bitU
+val quot_vec_maybe  : list bitU -> list bitU -> maybe (list bitU)
+val quot_vec_fail   : forall 'rv 'e. list bitU -> list bitU -> monad 'rv (list bitU) 'e
+val quot_vec_oracle : forall 'rv 'e. list bitU -> list bitU -> monad 'rv (list bitU) 'e
+let quot_vec        l r = fromMaybe (repeat [BU] (length l)) (quot_bv l r)
+let quot_vec_maybe  l r = quot_bv l r
+let quot_vec_fail   l r = maybe_fail "quot_vec" (quot_bv l r)
+let quot_vec_oracle l r = of_bits_oracle (quot_vec l r)
+
+val quots_vec        : list bitU -> list bitU -> list bitU
+val quots_vec_maybe  : list bitU -> list bitU -> maybe (list bitU)
+val quots_vec_fail   : forall 'rv 'e. list bitU -> list bitU -> monad 'rv (list bitU) 'e
+val quots_vec_oracle : forall 'rv 'e. list bitU -> list bitU -> monad 'rv (list bitU) 'e
+let quots_vec        l r = fromMaybe (repeat [BU] (length l)) (quots_bv l r)
+let quots_vec_maybe  l r = quots_bv l r
+let quots_vec_fail   l r = maybe_fail "quots_vec" (quots_bv l r)
+let quots_vec_oracle l r = of_bits_oracle (quots_vec l r)
+
+val mod_vec_int        : list bitU -> integer -> list bitU
+val mod_vec_int_maybe  : list bitU -> integer -> maybe (list bitU)
+val mod_vec_int_fail   : forall 'rv 'e. list bitU -> integer -> monad 'rv (list bitU) 'e
+val mod_vec_int_oracle : forall 'rv 'e. list bitU -> integer -> monad 'rv (list bitU) 'e
+let mod_vec_int        l r = fromMaybe (repeat [BU] (length l)) (mod_bv_int l r)
+let mod_vec_int_maybe  l r = mod_bv_int l r
+let mod_vec_int_fail   l r = maybe_fail "mod_vec_int" (mod_bv_int l r)
+let mod_vec_int_oracle l r = of_bits_oracle (mod_vec_int l r)
+
+val quot_vec_int        : list bitU -> integer -> list bitU
+val quot_vec_int_maybe  : list bitU -> integer -> maybe (list bitU)
+val quot_vec_int_fail   : forall 'rv 'e. list bitU -> integer -> monad 'rv (list bitU) 'e
+val quot_vec_int_oracle : forall 'rv 'e. list bitU -> integer -> monad 'rv (list bitU) 'e
+let quot_vec_int        l r = fromMaybe (repeat [BU] (length l)) (quot_bv_int l r)
+let quot_vec_int_maybe  l r = quot_bv_int l r
+let quot_vec_int_fail   l r = maybe_fail "quot_vec_int" (quot_bv_int l r)
+let quot_vec_int_oracle l r = of_bits_oracle (quot_vec_int l r)
 
 val replicate_bits : list bitU -> integer -> list bitU
 let replicate_bits = replicate_bits_bv
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index e3e1151a..55e6ff51 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -126,39 +126,46 @@ let not_vec = Machine_word.lNot
 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 subs_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   l r = arith_op_bv integerAdd   false l r
 let adds_vec  l r = arith_op_bv integerAdd   true  l r
-let sub_vec   l r = arith_op_bv integerMinus true  l r
+let sub_vec   l r = arith_op_bv integerMinus false l r
+let subs_vec  l r = arith_op_bv integerMinus true  l r
 let mult_vec  l r = arith_op_bv integerMult  false (zeroExtend l : mword 'b) (zeroExtend r : mword 'b)
 let mults_vec l r = arith_op_bv integerMult  true  (signExtend l : mword 'b) (signExtend r : mword 'b)
 
 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 subs_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   l r = arith_op_bv_int integerAdd   false l r
 let adds_vec_int  l r = arith_op_bv_int integerAdd   true  l r
-let sub_vec_int   l r = arith_op_bv_int integerMinus true  l r
+let sub_vec_int   l r = arith_op_bv_int integerMinus false l r
+let subs_vec_int  l r = arith_op_bv_int integerMinus true  l r
 let mult_vec_int  l r = arith_op_bv_int integerMult  false (zeroExtend l : mword 'b) r
 let mults_vec_int l r = arith_op_bv_int integerMult  true  (signExtend l : mword 'b) r
 
 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 subs_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   l r = arith_op_int_bv integerAdd   false l r
 let adds_int_vec  l r = arith_op_int_bv integerAdd   true  l r
-let sub_int_vec   l r = arith_op_int_bv integerMinus true  l r
+let sub_int_vec   l r = arith_op_int_bv integerMinus false l r
+let subs_int_vec  l r = arith_op_int_bv integerMinus true  l r
 let mult_int_vec  l r = arith_op_int_bv integerMult  false l (zeroExtend r : mword 'b)
 let mults_int_vec l r = arith_op_int_bv integerMult  true  l (signExtend r : mword 'b)
 
 val add_vec_bool  : forall 'a. Size 'a => mword 'a -> bool -> mword 'a
 val adds_vec_bool : forall 'a. Size 'a => mword 'a -> bool -> mword 'a
 val sub_vec_bool  : forall 'a. Size 'a => mword 'a -> bool -> mword 'a
+val subs_vec_bool : forall 'a. Size 'a => mword 'a -> bool -> mword 'a
 
 let add_vec_bool        l r = arith_op_bv_bool integerAdd false l r
 let add_vec_bit_maybe   l r = Maybe.map (add_vec_bool l) (bool_of_bitU r)
@@ -172,12 +179,18 @@ let adds_vec_bit_fail   l r = bool_of_bitU_fail r >>= (fun r -> return (adds_vec
 let adds_vec_bit_oracle l r = bool_of_bitU_oracle r >>= (fun r -> return (adds_vec_bool l r))
 let adds_vec_bit        l r = maybe_failwith (adds_vec_bit_maybe l r)
 
-let sub_vec_bool        l r = arith_op_bv_bool integerMinus true  l r
+let sub_vec_bool        l r = arith_op_bv_bool integerMinus false l r
 let sub_vec_bit_maybe   l r = Maybe.map (sub_vec_bool l) (bool_of_bitU r)
 let sub_vec_bit_fail    l r = bool_of_bitU_fail r >>= (fun r -> return (sub_vec_bool l r))
 let sub_vec_bit_oracle  l r = bool_of_bitU_oracle r >>= (fun r -> return (sub_vec_bool l r))
 let sub_vec_bit         l r = maybe_failwith (sub_vec_bit_maybe  l r)
 
+let subs_vec_bool       l r = arith_op_bv_bool integerMinus true  l r
+let subs_vec_bit_maybe  l r = Maybe.map (subs_vec_bool l) (bool_of_bitU r)
+let subs_vec_bit_fail   l r = bool_of_bitU_fail r >>= (fun r -> return (subs_vec_bool l r))
+let subs_vec_bit_oracle l r = bool_of_bitU_oracle r >>= (fun r -> return (subs_vec_bool l r))
+let subs_vec_bit        l r = maybe_failwith (subs_vec_bit_maybe  l r)
+
 (* TODO
 val maybe_mword_of_bits_overflow : forall 'a. Size 'a => (list bitU * bitU * bitU) -> maybe (mword 'a * bitU * bitU)
 let maybe_mword_of_bits_overflow (bits, overflow, carry) =
@@ -216,17 +229,70 @@ let arith_shiftr = arith_shiftr_mword
 let rotl         = rotl_mword
 let rotr         = rotr_mword
 
-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 quots_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
-let mod_vec   = mod_mword
-let quot_vec  = quot_mword
-let quots_vec = quots_mword
-
-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_mword_int
-let quot_vec_int = quot_mword_int
+val mod_vec        : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
+val mod_vec_maybe  : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a)
+val mod_vec_fail   : forall 'rv 'a 'e. Size 'a => mword 'a -> mword 'a -> monad 'rv (mword 'a) 'e
+val mod_vec_oracle : forall 'rv 'a 'e. Size 'a => mword 'a -> mword 'a -> monad 'rv (mword 'a) 'e
+let mod_vec        l r = mod_mword l r
+let mod_vec_maybe  l r = mod_bv l r
+let mod_vec_fail   l r = maybe_fail "mod_vec" (mod_bv l r)
+let mod_vec_oracle l r =
+  match (mod_bv l r) with
+    | Just w -> return w
+    | Nothing -> mword_oracle ()
+  end
+
+val quot_vec        : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
+val quot_vec_maybe  : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a)
+val quot_vec_fail   : forall 'rv 'a 'e. Size 'a => mword 'a -> mword 'a -> monad 'rv (mword 'a) 'e
+val quot_vec_oracle : forall 'rv 'a 'e. Size 'a => mword 'a -> mword 'a -> monad 'rv (mword 'a) 'e
+let quot_vec        l r = quot_mword l r
+let quot_vec_maybe  l r = quot_bv l r
+let quot_vec_fail   l r = maybe_fail "quot_vec" (quot_bv l r)
+let quot_vec_oracle l r =
+  match (quot_bv l r) with
+    | Just w -> return w
+    | Nothing -> mword_oracle ()
+  end
+
+val quots_vec        : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
+val quots_vec_maybe  : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a)
+val quots_vec_fail   : forall 'rv 'a 'e. Size 'a => mword 'a -> mword 'a -> monad 'rv (mword 'a) 'e
+val quots_vec_oracle : forall 'rv 'a 'e. Size 'a => mword 'a -> mword 'a -> monad 'rv (mword 'a) 'e
+let quots_vec        l r = quots_mword l r
+let quots_vec_maybe  l r = quots_bv l r
+let quots_vec_fail   l r = maybe_fail "quots_vec" (quots_bv l r)
+let quots_vec_oracle l r =
+  match (quots_bv l r) with
+    | Just w -> return w
+    | Nothing -> mword_oracle ()
+  end
+
+val mod_vec_int        : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+val mod_vec_int_maybe  : forall 'a. Size 'a => mword 'a -> integer -> maybe (mword 'a)
+val mod_vec_int_fail   : forall 'rv 'a 'e. Size 'a => mword 'a -> integer -> monad 'rv (mword 'a) 'e
+val mod_vec_int_oracle : forall 'rv 'a 'e. Size 'a => mword 'a -> integer -> monad 'rv (mword 'a) 'e
+let mod_vec_int        l r = mod_mword_int l r
+let mod_vec_int_maybe  l r = mod_bv_int l r
+let mod_vec_int_fail   l r = maybe_fail "mod_vec_int" (mod_bv_int l r)
+let mod_vec_int_oracle l r =
+  match (mod_bv_int l r) with
+    | Just w -> return w
+    | Nothing -> mword_oracle ()
+  end
+
+val quot_vec_int        : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+val quot_vec_int_maybe  : forall 'a. Size 'a => mword 'a -> integer -> maybe (mword 'a)
+val quot_vec_int_fail   : forall 'rv 'a 'e. Size 'a => mword 'a -> integer -> monad 'rv (mword 'a) 'e
+val quot_vec_int_oracle : forall 'rv 'a 'e. Size 'a => mword 'a -> integer -> monad 'rv (mword 'a) 'e
+let quot_vec_int        l r = quot_mword_int l r
+let quot_vec_int_maybe  l r = quot_bv_int l r
+let quot_vec_int_fail   l r = maybe_fail "quot_vec_int" (quot_bv_int l r)
+let quot_vec_int_oracle l r =
+  match (quot_bv_int l r) with
+    | Just w -> return w
+    | Nothing -> mword_oracle ()
+  end
 
 val replicate_bits : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
 let replicate_bits v count = wordFromBitlist (repeat (bitlistFromWord v) count)
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 819c11c5..2d9eda9c 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -253,12 +253,13 @@ let inline (+.) x y = xor_bit x y
 
 (*** Bool lists ***)
 
-val bools_of_nat_aux : natural -> list bool
-let rec bools_of_nat_aux x =
-  if x = 0 then []
-  else (if x mod 2 = 1 then true else false) :: bools_of_nat_aux (x / 2)
+val bools_of_nat_aux : integer -> natural -> list bool -> list bool
+let rec bools_of_nat_aux len x acc =
+  if len <= 0 then acc
+  else bools_of_nat_aux (len - 1) (x / 2) ((if x mod 2 = 1 then true else false) :: acc)
+  (*else (if x mod 2 = 1 then true else false) :: bools_of_nat_aux (x / 2)*)
 declare {isabelle} termination_argument bools_of_nat_aux = automatic
-let bools_of_nat n = List.reverse (bools_of_nat_aux n)
+let bools_of_nat len n = bools_of_nat_aux len n [] (*List.reverse (bools_of_nat_aux n)*)
 
 val nat_of_bools_aux : natural -> list bool -> natural
 let rec nat_of_bools_aux acc bs = match bs with
@@ -310,18 +311,22 @@ declare {isabelle} termination_argument add_one_bool_ignore_overflow_aux = autom
 let add_one_bool_ignore_overflow bits =
   List.reverse (add_one_bool_ignore_overflow_aux (List.reverse bits))
 
-let bool_list_of_int n =
+(*let bool_list_of_int n =
   let bs_abs = false :: bools_of_nat (naturalFromInteger (abs n)) in
   if n >= (0 : integer) then bs_abs
   else add_one_bool_ignore_overflow (List.map not bs_abs)
-let bools_of_int len n = exts_bools len (bool_list_of_int n)
+let bools_of_int len n = exts_bools len (bool_list_of_int n)*)
+let bools_of_int len n =
+  let bs_abs = bools_of_nat len (naturalFromInteger (abs n)) in
+  if n >= (0 : integer) then bs_abs
+  else add_one_bool_ignore_overflow (List.map not bs_abs)
 
 (*** Bit lists ***)
 
 val has_undefined_bits : list bitU -> bool
 let has_undefined_bits bs = List.any (function BU -> true | _ -> false end) bs
 
-let bits_of_nat n = List.map bitU_of_bool (bools_of_nat n)
+let bits_of_nat len n = List.map bitU_of_bool (bools_of_nat len n)
 
 let nat_of_bits bits =
   match (just_list (List.map bool_of_bitU bits)) with
@@ -369,8 +374,9 @@ declare {isabelle} termination_argument add_one_bit_ignore_overflow_aux = automa
 let add_one_bit_ignore_overflow bits =
   List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits))
 
-let bit_list_of_int n = List.map bitU_of_bool (bool_list_of_int n)
-let bits_of_int len n = exts_bits len (bit_list_of_int n)
+(*let bit_list_of_int n = List.map bitU_of_bool (bool_list_of_int n)
+let bits_of_int len n = exts_bits len (bit_list_of_int n)*)
+let bits_of_int len n = List.map bitU_of_bool (bools_of_int len n)
 
 val arith_op_bits :
   (integer -> integer -> integer) -> bool -> list bitU -> list bitU -> list bitU
@@ -628,7 +634,7 @@ declare {isabelle} termination_argument byte_chunks = automatic
 val bytes_of_bits : forall 'a. Bitvector 'a => 'a -> maybe (list memory_byte)
 let bytes_of_bits bs = byte_chunks (bits_of bs)
 
-val bits_of_bytes : forall 'a. Bitvector 'a => list memory_byte -> list bitU
+val bits_of_bytes : list memory_byte -> list bitU
 let bits_of_bytes bs = List.concat (List.map bits_of bs)
 
 let mem_bytes_of_bits bs = Maybe.map List.reverse (bytes_of_bits bs)
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 222cd715..61477258 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -24,7 +24,6 @@ let rec liftState ra s = match s with
   | (Barrier _ k)        -> liftState ra k
   | (Print _ k)          -> liftState ra k (* TODO *)
   | (Fail descr)         -> failS descr
-  | (Error descr)        -> failS descr
   | (Exception e)        -> throwS e
 end