Make partiality more explicit in library functions of Lem shallow embedding

Some functions are partial, e.g. converting a bitvector to an integer, which
might fail for the bit list representation due to undefined bits.  Undefined
cases can be handled in different ways:

- call Lem's failwith, which maps to undefined/ARB in Isabelle and HOL (the
  default so far),
- return an option type,
- raise a failure  in the monad, or
- use a bitstream oracle to resolve undefined bits.

This patch adds different versions of partial functions corresponding to those
options.  The desired behaviour can be selected by choosing a binding in the
Sail prelude.  The naming scheme is that the failwith version is the default,
while the other versions have the suffixes _maybe, _fail, and _oracle,
respectively.

1 files changed, 243 insertions, 185 deletions

diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index edb8da88..238ebe58 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -1,5 +1,3 @@
-(* Version of sail_values.lem that uses Lem's machine words library *)
-
 open import Pervasives_extra
 open import Machine_word
 (*open import Sail_impl_base*)
@@ -8,8 +6,11 @@ open import Machine_word
 type ii = integer
 type nn = natural
 
+val nat_of_int : integer -> nat
+let nat_of_int i = if i < 0 then 0 else natFromInteger i
+
 val pow : integer -> integer -> integer
-let pow m n = m ** (natFromInteger n)
+let pow m n = m ** (nat_of_int n)
 
 let pow2 n = pow 2 n
 
@@ -31,7 +32,7 @@ let mult_int l r = integerMult l r
 let div_int l r = integerDiv l r
 let div_nat l r = natDiv l r
 let power_int_nat l r = integerPow l r
-let power_int_int l r = integerPow l (natFromInteger r)
+let power_int_int l r = integerPow l (nat_of_int r)
 let negate_int i = integerNegate i
 let min_int l r = integerMin l r
 let max_int l r = integerMax l r
@@ -50,8 +51,8 @@ let xor_bool l r = xor l r
 
 let append_list l r = l ++ r
 let length_list xs = integerFromNat (List.length xs)
-let take_list n xs = List.take (natFromInteger n) xs
-let drop_list n xs = List.drop (natFromInteger n) xs
+let take_list n xs = List.take (nat_of_int n) xs
+let drop_list n xs = List.drop (nat_of_int n) xs
 
 val repeat : forall 'a. list 'a -> integer -> list 'a
 let rec repeat xs n =
@@ -99,6 +100,29 @@ let min_8   = (0 - 128 : integer)
 let max_5   = (31 : integer)
 let min_5   = (0 - 32 : integer)
 
+(* just_list takes a list of maybes and returns Just xs if all elements have
+   a value, and Nothing if one of the elements is Nothing. *)
+val just_list : forall 'a. list (maybe 'a) -> maybe (list 'a)
+let rec just_list l = match l with
+  | [] -> Just []
+  | (x :: xs) ->
+    match (x, just_list xs) with
+      | (Just x, Just xs) -> Just (x :: xs)
+      | (_, _) -> Nothing
+    end
+  end
+declare {isabelle} termination_argument just_list = automatic
+
+lemma just_list_spec:
+  ((forall xs. (just_list xs = Nothing) <-> List.elem Nothing xs) &&
+   (forall xs es. (just_list xs = Just es) <-> (xs = List.map Just es)))
+
+val maybe_failwith : forall 'a. maybe 'a -> 'a
+let maybe_failwith = function
+  | Just a -> a
+  | Nothing -> failwith "maybe_failwith"
+end
+
 (*** Bits *)
 type bitU = B0 | B1 | BU
 
@@ -118,6 +142,25 @@ instance (Show bitU)
   let show = showBitU
 end
 
+val compare_bitU : bitU -> bitU -> ordering
+let compare_bitU l r = match (l, r) with
+  | (BU, BU) -> EQ
+  | (B0, B0) -> EQ
+  | (B1, B1) -> EQ
+  | (BU, _)  -> LT
+  | (_, BU)  -> GT
+  | (B0, _)  -> LT
+  | (_, _)   -> GT
+end
+
+instance (Ord bitU)
+  let compare = compare_bitU
+  let (<)  l r = (compare_bitU l r) = LT
+  let (<=) l r = (compare_bitU l r) <> GT
+  let (>)  l r = (compare_bitU l r) = GT
+  let (>=) l r = (compare_bitU l r) <> LT
+end
+
 class (BitU 'a)
   val to_bitU : 'a -> bitU
   val of_bitU : bitU -> 'a
@@ -129,44 +172,20 @@ instance (BitU bitU)
 end
 
 let bool_of_bitU = function
-  | B0 -> false
-  | B1 -> true
-  | BU -> failwith "bool_of_bitU applied to BU"
+  | B0 -> Just false
+  | B1 -> Just true
+  | BU -> Nothing
   end
 
 let bitU_of_bool b = if b then B1 else B0
 
-instance (BitU bool)
+(*instance (BitU bool)
   let to_bitU = bitU_of_bool
   let of_bitU = bool_of_bitU
-end
+end*)
 
 let cast_bit_bool = bool_of_bitU
 
-(*let bit_lifted_of_bitU = function
-  | B0 -> Bitl_zero
-  | B1 -> Bitl_one
-  | BU -> Bitl_undef
-  end
-
-let bitU_of_bit = function
-  | Bitc_zero -> B0
-  | Bitc_one  -> B1
-  end
-
-let bit_of_bitU = function
-  | B0 -> Bitc_zero
-  | B1 -> Bitc_one
-  | BU -> failwith "bit_of_bitU: BU"
-  end
-
-let bitU_of_bit_lifted = function
-  | Bitl_zero -> B0
-  | Bitl_one  -> B1
-  | Bitl_undef -> BU
-  | Bitl_unknown -> failwith "bitU_of_bit_lifted Bitl_unknown"
-  end*)
-
 let not_bit = function
   | B1 -> B0
   | B0 -> B1
@@ -177,20 +196,33 @@ val is_one : integer -> bitU
 let is_one i =
   if i = 1 then B1 else B0
 
-let binop_bit op x y = match (x, y) with
-  | (BU,_) -> BU (*Do we want to do this or to respect | of I and & of B0 rules?*)
-  | (_,BU) -> BU (*Do we want to do this or to respect | of I and & of B0 rules?*)
-  | (x,y) -> bitU_of_bool (op (bool_of_bitU x) (bool_of_bitU y))
-  end
-
 val and_bit : bitU -> bitU -> bitU
-let and_bit = binop_bit (&&)
+let and_bit x y =
+  match (x, y) with
+    | (B0, _) -> B0
+    | (_, B0) -> B0
+    | (B1, B1) -> B1
+    | (_, _) -> BU
+  end
 
 val or_bit : bitU -> bitU -> bitU
-let or_bit = binop_bit (||)
+let or_bit x y =
+  match (x, y) with
+    | (B1, _) -> B1
+    | (_, B1) -> B1
+    | (B0, B0) -> B0
+    | (_, _) -> BU
+  end
 
 val xor_bit : bitU -> bitU -> bitU
-let xor_bit = binop_bit xor
+let xor_bit x y=
+  match (x, y) with
+    | (B0, B0) -> B0
+    | (B0, B1) -> B1
+    | (B1, B0) -> B1
+    | (B1, B1) -> B0
+    | (_, _) -> BU
+  end
 
 val (&.) : bitU -> bitU -> bitU
 let inline (&.) x y = and_bit x y
@@ -202,81 +234,134 @@ val (+.) : bitU -> bitU -> bitU
 let inline (+.) x y = xor_bit x y
 
 
-(*** Bit lists ***)
+(*** Bool lists ***)
 
-val bits_of_nat_aux : natural -> list bitU
-let rec bits_of_nat_aux x =
+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 B1 else B0) :: bits_of_nat_aux (x / 2)
-declare {isabelle} termination_argument bits_of_nat_aux = automatic
-let bits_of_nat n = List.reverse (bits_of_nat_aux n)
+  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)
 
-val nat_of_bits_aux : natural -> list bitU -> natural
-let rec nat_of_bits_aux acc bs = match bs with
+val nat_of_bools_aux : natural -> list bool -> natural
+let rec nat_of_bools_aux acc bs = match bs with
   | [] -> acc
-  | B1 :: bs -> nat_of_bits_aux ((2 * acc) + 1) bs
-  | B0 :: bs -> nat_of_bits_aux (2 * acc) bs
-  | BU :: _ -> failwith "nat_of_bits_aux: bit list has undefined bits"
+  | true :: bs -> nat_of_bools_aux ((2 * acc) + 1) bs
+  | false :: bs -> nat_of_bools_aux (2 * acc) bs
 end
-declare {isabelle} termination_argument nat_of_bits_aux = automatic
-let nat_of_bits bits = nat_of_bits_aux 0 bits
+declare {isabelle} termination_argument nat_of_bools_aux = automatic
+let nat_of_bools bs = nat_of_bools_aux 0 bs
+
+val unsigned_of_bools : list bool -> integer
+let unsigned_of_bools bs = integerFromNatural (nat_of_bools bs)
+
+val signed_of_bools : list bool -> integer
+let signed_of_bools bs =
+  match bs with
+    | true :: _  -> 0 - (1 + (unsigned_of_bools (List.map not bs)))
+    | false :: _ -> unsigned_of_bools bs
+    | [] -> 0 (* Treat empty list as all zeros *)
+  end
 
-let not_bits = List.map not_bit
+val int_of_bools : bool -> list bool -> integer
+let int_of_bools sign bs = if sign then signed_of_bools bs else unsigned_of_bools bs
 
-let binop_bits op bsl bsr =
-  foldr (fun (bl, br) acc -> binop_bit op bl br :: acc) [] (zip bsl bsr)
+val pad_list : forall 'a. 'a -> list 'a -> integer -> list 'a
+let rec pad_list x xs n =
+  if n <= 0 then xs else pad_list x (x :: xs) (n - 1)
+declare {isabelle} termination_argument pad_list = automatic
 
-let and_bits = binop_bits (&&)
-let or_bits = binop_bits (||)
-let xor_bits = binop_bits xor
+let ext_list pad len xs =
+  let longer = len - (integerFromNat (List.length xs)) in
+  if longer < 0 then drop (nat_of_int (abs (longer))) xs
+  else pad_list pad xs longer
 
-val unsigned_of_bits : list bitU -> integer
-let unsigned_of_bits bs = integerFromNatural (nat_of_bits bs)
+let extz_bools len bs = ext_list false len bs
+let exts_bools len bs =
+  match bs with
+    | true :: _ -> ext_list true len bs
+    | _ -> ext_list false len bs
+  end
 
-val signed_of_bits : list bitU -> integer
-let signed_of_bits bits =
-  match bits with
-  | B1 :: _ -> 0 - (1 + (unsigned_of_bits (not_bits bits)))
-  | B0 :: _ -> unsigned_of_bits bits
-  | BU :: _ -> failwith "signed_of_bits applied to list with undefined bits"
-  | [] -> failwith "signed_of_bits applied to empty list"
+let rec add_one_bool_ignore_overflow_aux bits = match bits with
+  | [] -> []
+  | false :: bits -> true :: bits
+  | true :: bits -> false :: add_one_bool_ignore_overflow_aux bits
+end
+declare {isabelle} termination_argument add_one_bool_ignore_overflow_aux = automatic
+
+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 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)
+
+(*** 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 nat_of_bits bits =
+  match (just_list (List.map bool_of_bitU bits)) with
+    | Just bs -> Just (nat_of_bools bs)
+    | Nothing -> Nothing
+  end
+
+let not_bits = List.map not_bit
+
+val binop_list : forall 'a. ('a -> 'a -> 'a) -> list 'a -> list 'a -> list 'a
+let binop_list op xs ys =
+  foldr (fun (x, y) acc -> op x y :: acc) [] (zip xs ys)
+
+let unsigned_of_bits bits =
+  match (just_list (List.map bool_of_bitU bits)) with
+    | Just bs -> Just (unsigned_of_bools bs)
+    | Nothing -> Nothing
   end
 
-val pad_bitlist : bitU -> list bitU -> integer -> list bitU
-let rec pad_bitlist b bits n =
-  if n <= 0 then bits else pad_bitlist b (b :: bits) (n - 1)
-declare {isabelle} termination_argument pad_bitlist = automatic
+let signed_of_bits bits =
+  match (just_list (List.map bool_of_bitU bits)) with
+    | Just bs -> Just (signed_of_bools bs)
+    | Nothing -> Nothing
+  end
 
-let ext_bits pad len bits =
-  let longer = len - (integerFromNat (List.length bits)) in
-  if longer < 0 then drop (natFromInteger (abs (longer))) bits
-  else pad_bitlist pad bits longer
+val int_of_bits : bool -> list bitU -> maybe integer
+let int_of_bits sign bs = if sign then signed_of_bits bs else unsigned_of_bits bs
 
-let extz_bits len bits = ext_bits B0 len bits
+let extz_bits len bits = ext_list B0 len bits
 let exts_bits len bits =
   match bits with
-  | BU :: _ -> failwith "exts_bits: undefined bit"
-  | B1 :: _ -> ext_bits B1 len bits
-  | _ -> ext_bits B0 len bits
+  | BU :: _ -> ext_list BU len bits
+  | B1 :: _ -> ext_list B1 len bits
+  | _ -> ext_list B0 len bits
   end
 
 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"
+  | BU :: bits -> BU :: List.map (fun _ -> BU) bits
 end
 declare {isabelle} termination_argument add_one_bit_ignore_overflow_aux = automatic
 
 let add_one_bit_ignore_overflow bits =
   List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits))
 
-let bitlist_of_int n =
-  let bits_abs = B0 :: bits_of_nat (naturalFromInteger (abs n)) in
-  if n >= (0 : integer) then bits_abs
-  else add_one_bit_ignore_overflow (not_bits bits_abs)
+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 = exts_bits len (bitlist_of_int n)
+val arith_op_bits :
+  (integer -> integer -> integer) -> bool -> list bitU -> list bitU -> list bitU
+let arith_op_bits op sign l r =
+  match (int_of_bits sign l, int_of_bits sign r) with
+    | (Just li, Just ri) -> bits_of_int (length_list l) (op li ri)
+    | (_, _) -> repeat [BU] (length_list l)
+  end
 
 let char_of_nibble = function
   | (B0, B0, B0, B0) -> Just #'0'
@@ -322,8 +407,8 @@ let inline (^^) = append_list
 
 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
+  let (toJ,_suffix) = List.splitAt (nat_of_int (j + 1)) xs in
+  let (_prefix,fromItoJ) = List.splitAt (nat_of_int i) toJ in
   fromItoJ
 
 val subrange_list_dec : forall 'a. list 'a -> integer -> integer -> list 'a
@@ -336,8 +421,8 @@ let subrange_list is_inc xs i j = if is_inc then subrange_list_inc xs i j else s
 
 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
+  let (toJ,suffix) = List.splitAt (nat_of_int (j + 1)) xs in
+  let (prefix,_fromItoJ) = List.splitAt (nat_of_int i) toJ in
   prefix ++ xs' ++ suffix
 
 val update_subrange_list_dec : forall 'a. list 'a -> integer -> integer -> list 'a -> list 'a
@@ -350,7 +435,7 @@ 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)
+let access_list_inc xs n = List_extra.nth xs (nat_of_int n)
 
 val access_list_dec : forall 'a. list 'a -> integer -> 'a
 let access_list_dec xs n =
@@ -362,7 +447,7 @@ let access_list is_inc xs n =
   if is_inc then access_list_inc xs n else access_list_dec xs n
 
 val update_list_inc : forall 'a. list 'a -> integer -> 'a -> list 'a
-let update_list_inc xs n x = List.update xs (natFromInteger n) x
+let update_list_inc xs n x = List.update xs (nat_of_int n) x
 
 val update_list_dec : forall 'a. list 'a -> integer -> 'a -> list 'a
 let update_list_dec xs n x =
@@ -373,36 +458,19 @@ val update_list : forall 'a. bool -> list 'a -> integer -> 'a -> list 'a
 let update_list is_inc xs n x =
   if is_inc then update_list_inc xs n x else update_list_dec xs n x
 
-let extract_only_element = function
-  | [] -> failwith "extract_only_element called for empty list"
+let extract_only_bit = function
+  | [] ->  BU
   | [e] -> e
-  | _ -> failwith "extract_only_element called for list with more elements"
+  | _ ->   BU
 end
 
-(* just_list takes a list of maybes and returns Just xs if all elements have
-   a value, and Nothing if one of the elements is Nothing. *)
-val just_list : forall 'a. list (maybe 'a) -> maybe (list 'a)
-let rec just_list l = match l with
-  | [] -> Just []
-  | (x :: xs) ->
-    match (x, just_list xs) with
-      | (Just x, Just xs) -> Just (x :: xs)
-      | (_, _) -> Nothing
-    end
-  end
-declare {isabelle} termination_argument just_list = automatic
-
-lemma just_list_spec:
-  ((forall xs. (just_list xs = Nothing) <-> List.elem Nothing xs) &&
-   (forall xs es. (just_list xs = Just es) <-> (xs = List.map Just es)))
-
 (*** Machine words *)
 
 val length_mword : forall 'a. mword 'a -> integer
 let length_mword w = integerFromNat (word_length w)
 
 val slice_mword_dec : forall 'a 'b. mword 'a -> integer -> integer -> mword 'b
-let slice_mword_dec w i j = word_extract (natFromInteger i) (natFromInteger j) w
+let slice_mword_dec w i j = word_extract (nat_of_int i) (nat_of_int j) w
 
 val slice_mword_inc : forall 'a 'b. mword 'a -> integer -> integer -> mword 'b
 let slice_mword_inc w i j =
@@ -413,7 +481,7 @@ val slice_mword : forall 'a 'b. bool -> mword 'a -> integer -> integer -> mword
 let slice_mword is_inc w i j = if is_inc then slice_mword_inc w i j else slice_mword_dec w i j
 
 val update_slice_mword_dec : forall 'a 'b. mword 'a -> integer -> integer -> mword 'b -> mword 'a
-let update_slice_mword_dec w i j w' = word_update w (natFromInteger i) (natFromInteger j) w'
+let update_slice_mword_dec w i j w' = word_update w (nat_of_int i) (nat_of_int j) w'
 
 val update_slice_mword_inc : forall 'a 'b. mword 'a -> integer -> integer -> mword 'b -> mword 'a
 let update_slice_mword_inc w i j w' =
@@ -425,7 +493,7 @@ let update_slice_mword is_inc w i j w' =
   if is_inc then update_slice_mword_inc w i j w' else update_slice_mword_dec w i j w'
 
 val access_mword_dec : forall 'a. mword 'a -> integer -> bitU
-let access_mword_dec w n = bitU_of_bool (getBit w (natFromInteger n))
+let access_mword_dec w n = bitU_of_bool (getBit w (nat_of_int n))
 
 val access_mword_inc : forall 'a. mword 'a -> integer -> bitU
 let access_mword_inc w n =
@@ -436,22 +504,19 @@ val access_mword : forall 'a. bool -> mword 'a -> integer -> bitU
 let access_mword is_inc w n =
   if is_inc then access_mword_inc w n else access_mword_dec w n
 
-val update_mword_dec : forall 'a. mword 'a -> integer -> bitU -> mword 'a
-let update_mword_dec w n b = setBit w (natFromInteger n) (bool_of_bitU b)
+val update_mword_bool_dec : forall 'a. mword 'a -> integer -> bool -> mword 'a
+let update_mword_bool_dec w n b = setBit w (nat_of_int n) b
+let update_mword_dec w n b = Maybe.map (update_mword_bool_dec w n) (bool_of_bitU b)
 
-val update_mword_inc : forall 'a. mword 'a -> integer -> bitU -> mword 'a
-let update_mword_inc w n b =
+val update_mword_bool_inc : forall 'a. mword 'a -> integer -> bool -> mword 'a
+let update_mword_bool_inc w n b =
   let top = (length_mword w) - 1 in
-  update_mword_dec w (top - n) b
-
-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
+  update_mword_bool_dec w (top - n) b
+let update_mword_inc w n b = Maybe.map (update_mword_bool_inc w n) (bool_of_bitU 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"
+val int_of_mword : forall 'a. bool -> mword 'a -> integer
+let int_of_mword sign w =
+  if sign then signedIntegerFromWord w else unsignedIntegerFromWord w
 
 (* Translating between a type level number (itself 'n) and an integer *)
 
@@ -461,68 +526,71 @@ let size_itself_int x = integerFromNat (size_itself x)
    the actual integer is ignored. *)
 
 val make_the_value : forall 'n. integer -> itself 'n
-let inline make_the_value x = the_value
+let inline make_the_value = (fun _ -> 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
+  (* We allow of_bits to be partial, as not all bitvector representations
+     support undefined bits *)
+  val of_bits : list bitU -> maybe 'a
+  val of_bools : list bool -> 'a
   val length : 'a -> integer
-  val unsigned : 'a -> integer
-  val signed : 'a -> integer
-  (* The first parameter specifies the indexing order (true is increasing) *)
-  val get_bit : bool -> 'a -> integer -> bitU
-  val set_bit : bool -> 'a -> integer -> bitU -> 'a
-  val get_bits : bool -> 'a -> integer -> integer -> list bitU
-  val set_bits : bool -> 'a -> integer -> integer -> list bitU -> 'a
+  (* of_int: the first parameter specifies the desired length of the bitvector *)
+  val of_int : integer -> integer -> 'a
+  (* Conversion to integers is undefined if any bit is undefined *)
+  val unsigned : 'a -> maybe integer
+  val signed : 'a -> maybe integer
+  (* Lifting of integer operations to bitvectors:  The boolean flag indicates
+     whether to treat the bitvectors as signed (true) or not (false). *)
+  val arith_op_bv : (integer -> integer -> integer) -> bool -> 'a -> 'a -> 'a
 end
 
+val of_bits_failwith : forall 'a. Bitvector 'a => list bitU -> 'a
+let of_bits_failwith bits = maybe_failwith (of_bits bits)
+
+let int_of_bv sign = if sign then signed else unsigned
+
 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 of_bits v = Just (List.map of_bitU v)
+  let of_bools v = List.map of_bitU (List.map bitU_of_bool 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 (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')
+  let arith_op_bv op sign l r = List.map of_bitU (arith_op_bits op sign (List.map to_bitU l) (List.map to_bitU r))
 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 bits_of v = List.map bitU_of_bool (bitlistFromWord v)
+  let of_bits v = Maybe.map wordFromBitlist (just_list (List.map bool_of_bitU v))
+  let of_bools v = wordFromBitlist v
+  let of_int = (fun _ n -> wordFromInteger n)
   let length v = integerFromNat (word_length 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')
+  let unsigned v = Just (unsignedIntegerFromWord v)
+  let signed v = Just (signedIntegerFromWord v)
+  let arith_op_bv op sign l r = wordFromInteger (op (int_of_mword sign l) (int_of_mword sign r))
 end
 
-let access_bv_inc v n = get_bit true  v n
-let access_bv_dec v n = get_bit false v n
+let access_bv_inc v n = access_list true  (bits_of v) n
+let access_bv_dec v n = access_list false (bits_of v) n
 
-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 update_bv_inc v n b = update_list true  (bits_of v) n b
+let update_bv_dec v n b = update_list false (bits_of v) n b
 
-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 subrange_bv_inc v i j = subrange_list true  (bits_of v) i j
+let subrange_bv_dec v i j = subrange_list false (bits_of v) i j
 
-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')
+let update_subrange_bv_inc v i j v' = update_subrange_list true  (bits_of v) i j (bits_of v')
+let update_subrange_bv_dec v i j v' = update_subrange_list false (bits_of v) i j (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 extz_bv : forall 'a. Bitvector 'a => integer -> 'a -> list bitU
+let extz_bv n v = extz_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))
+val exts_bv : forall 'a. Bitvector 'a => integer -> 'a -> list bitU
+let exts_bv n v = exts_bits n (bits_of v)
 
 val string_of_bv : forall 'a. Bitvector 'a => 'a -> string
 let string_of_bv v = show_bitlist (bits_of v)
@@ -543,8 +611,8 @@ 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 -> 'a
-let bits_of_bytes bs = of_bits (List.concat (List.map bits_of bs))
+val bits_of_bytes : forall 'a. Bitvector 'a => 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)
 let bits_of_mem_bytes bs = bits_of_bytes (List.reverse bs)
@@ -596,9 +664,6 @@ let rec reverse_endianness_list bits =
   if List.length bits <= 8 then bits else
     reverse_endianness_list (drop_list 8 bits) ++ take_list 8 bits
 
-val reverse_endianness : forall 'a. Bitvector 'a => 'a -> 'a
-let reverse_endianness v = of_bits (reverse_endianness_list (bits_of v))
-
 
 (*** Registers *)
 
@@ -760,10 +825,10 @@ let internal_mem_value bytes =
 val foreach : forall 'a 'vars.
   (list 'a) -> 'vars -> ('a -> 'vars -> 'vars) -> 'vars
 let rec foreach l vars body =
-match l with
-| [] -> vars
-| (x :: xs) -> foreach xs (body x vars) body
-end
+  match l with
+    | [] -> vars
+    | (x :: xs) -> foreach xs (body x vars) body
+  end
 
 declare {isabelle} termination_argument foreach = automatic
 
@@ -783,13 +848,6 @@ let rec until vars cond body =
   if cond vars then vars else until (body vars) cond body
 
 
-let assert' b msg_opt =
-  let msg = match msg_opt with
-  | Just msg -> msg
-  | Nothing  -> "unspecified error"
-  end in
-  if b then () else failwith msg
-
 (* convert numbers unsafely to naturals *)
 
 class (ToNatural 'a) val toNatural : 'a -> natural end