Need to separate out the 0.10 lem library from upcoming 0.11

Unlike the prompt-monad change I don't see a way to do this easily
purely on the model side

Make sure a64_barrier_type and domain aren't visible for RISC-V
isabelle build

1 files changed, 999 insertions, 0 deletions

diff --git a/src/gen_lib/0.11/sail2_values.lem b/src/gen_lib/0.11/sail2_values.lem
new file mode 100644
index 00000000..f657803f
--- /dev/null
+++ b/src/gen_lib/0.11/sail2_values.lem
@@ -0,0 +1,999 @@
+open import Pervasives_extra
+open import Machine_word
+(*open import Sail_impl_base*)
+
+
+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 ** (nat_of_int 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
+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 (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
+
+let add_real l r = realAdd l r
+let sub_real l r = realMinus l r
+let mult_real l r = realMult l r
+let div_real l r = realDiv l r
+let negate_real r = realNegate r
+let abs_real r = realAbs r
+let power_real b e = realPowInteger b e*)
+
+val print_endline : string -> unit
+let print_endline _ = ()
+declare ocaml target_rep function print_endline = `print_endline`
+
+val print : string -> unit
+let print _ = ()
+declare ocaml target_rep function print = `print_string`
+
+val prerr_endline : string -> unit
+let prerr_endline _ = ()
+declare ocaml target_rep function prerr_endline = `prerr_endline`
+
+let prerr x = prerr_endline x
+
+val print_int : string -> integer -> unit
+let print_int msg i = print_endline (msg ^ (stringFromInteger i))
+
+val prerr_int : string -> integer -> unit
+let prerr_int msg i = prerr_endline (msg ^ (stringFromInteger i))
+
+val putchar : integer -> unit
+let putchar _ = ()
+declare ocaml target_rep function putchar i = (`print_char` (`char_of_int` (`Nat_big_num.to_int` i)))
+
+val shr_int : ii -> ii -> ii
+let rec shr_int x s = if s > 0 then shr_int (x / 2) (s - 1) else x
+
+val shl_int : integer -> integer -> integer
+let rec shl_int i shift = if shift > 0 then 2 * shl_int i (shift - 1) else i
+
+let inline or_bool l r = (l || r)
+let inline and_bool l r = (l && r)
+let inline xor_bool l r = xor l r
+
+let inline append_list l r = l ++ r
+let inline length_list xs = integerFromNat (List.length 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 =
+  if n <= 0 then []
+  else xs ++ repeat xs (n-1)
+declare {isabelle} termination_argument repeat = automatic
+
+let duplicate_to_list bit length = repeat [bit] length
+
+let rec replace bs (n : integer) b' = match bs with
+  | [] -> []
+  | b :: bs ->
+     if n = 0 then b' :: bs
+              else b :: replace bs (n - 1) b'
+  end
+declare {isabelle; hol} termination_argument replace = automatic
+
+let upper n = n
+
+(* Modulus operation corresponding to quot below -- result
+   has sign of dividend. *)
+let tmod_int (a: integer) (b:integer) : integer =
+  let m = (abs a) mod (abs b) in
+  if a < 0 then ~m else m
+
+let hardware_mod = tmod_int
+
+(* 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 tdiv_int (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 hardware_quot = tdiv_int
+
+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)
+
+(* 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; hol} 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
+
+let showBitU = function
+  | B0 -> "O"
+  | B1 -> "I"
+  | BU -> "U"
+end
+
+let bitU_char = function
+  | B0 -> #'0'
+  | B1 -> #'1'
+  | BU -> #'?'
+end
+
+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
+end
+
+instance (BitU bitU)
+  let to_bitU b = b
+  let of_bitU b = b
+end
+
+let bool_of_bitU = function
+  | B0 -> Just false
+  | B1 -> Just true
+  | BU -> Nothing
+  end
+
+let bitU_of_bool b = if b then B1 else B0
+
+(*instance (BitU bool)
+  let to_bitU = bitU_of_bool
+  let of_bitU = bool_of_bitU
+end*)
+
+let cast_bit_bool = bool_of_bitU
+
+let not_bit = function
+  | B1 -> B0
+  | B0 -> B1
+  | BU -> BU
+  end
+
+val is_one : integer -> bitU
+let is_one i =
+  if i = 1 then B1 else B0
+
+val and_bit : bitU -> bitU -> bitU
+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 x y =
+  match (x, y) with
+    | (B1, _) -> B1
+    | (_, B1) -> B1
+    | (B0, B0) -> B0
+    | (_, _) -> BU
+  end
+
+val xor_bit : bitU -> bitU -> bitU
+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
+
+val (|.) : bitU -> bitU -> bitU
+let inline (|.) x y = or_bit x y
+
+val (+.) : bitU -> bitU -> bitU
+let inline (+.) x y = xor_bit x y
+
+
+(*** Bool lists ***)
+
+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 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
+  | [] -> acc
+  | true :: bs -> nat_of_bools_aux ((2 * acc) + 1) bs
+  | false :: bs -> nat_of_bools_aux (2 * acc) bs
+end
+declare {isabelle; hol} 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
+
+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
+
+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 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
+
+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
+
+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; hol} 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)*)
+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 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
+    | 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
+
+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
+
+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_list B0 len bits
+let exts_bits len bits =
+  match bits with
+  | 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 :: bits -> BU :: List.map (fun _ -> BU) bits
+end
+declare {isabelle; hol} 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 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
+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'
+  | (B0, B0, B0, B1) -> Just #'1'
+  | (B0, B0, B1, B0) -> Just #'2'
+  | (B0, B0, B1, B1) -> Just #'3'
+  | (B0, B1, B0, B0) -> Just #'4'
+  | (B0, B1, B0, B1) -> Just #'5'
+  | (B0, B1, B1, B0) -> Just #'6'
+  | (B0, B1, B1, B1) -> Just #'7'
+  | (B1, B0, B0, B0) -> Just #'8'
+  | (B1, B0, B0, B1) -> Just #'9'
+  | (B1, B0, B1, B0) -> Just #'A'
+  | (B1, B0, B1, B1) -> Just #'B'
+  | (B1, B1, B0, B0) -> Just #'C'
+  | (B1, B1, B0, B1) -> Just #'D'
+  | (B1, B1, B1, B0) -> Just #'E'
+  | (B1, B1, B1, B1) -> Just #'F'
+  | _ -> Nothing
+  end
+
+let rec hexstring_of_bits bs = match bs with
+  | b1 :: b2 :: b3 :: b4 :: bs ->
+     let n = char_of_nibble (b1, b2, b3, b4) in
+     let s = hexstring_of_bits bs in
+     match (n, s) with
+     | (Just n, Just s) -> Just (n :: s)
+     | _ -> Nothing
+     end
+  | [] -> Just []
+  | _ -> Nothing
+  end
+declare {isabelle; hol} termination_argument hexstring_of_bits = automatic
+
+let show_bitlist bs =
+  match hexstring_of_bits bs with
+  | Just s -> toString (#'0' :: #'x' :: s)
+  | Nothing -> toString (#'0' :: #'b' :: map bitU_char bs)
+  end
+
+(*** List operations *)
+
+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 (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
+let subrange_list_dec xs i j =
+  let top = (length_list xs) - 1 in
+  subrange_list_inc xs (top - i) (top - 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_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 (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
+let update_subrange_list_dec xs i j xs' =
+  let top = (length_list xs) - 1 in
+  update_subrange_list_inc xs (top - i) (top - 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 (nat_of_int n)
+
+val access_list_dec : forall 'a. list 'a -> integer -> 'a
+let access_list_dec xs n =
+  let top = (length_list xs) - 1 in
+  access_list_inc xs (top - n)
+
+val access_list : forall 'a. bool -> list 'a -> integer -> 'a
+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 (nat_of_int n) x
+
+val update_list_dec : forall 'a. list 'a -> integer -> 'a -> list 'a
+let update_list_dec xs n x =
+  let top = (length_list xs) - 1 in
+  update_list_inc xs (top - n) x
+
+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_bit = function
+  | [] ->  BU
+  | [e] -> e
+  | _ ->   BU
+end
+
+(*** Machine words *)
+
+val length_mword : forall 'a. mword 'a -> integer
+let inline 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 (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 =
+  let top = (length_mword w) - 1 in
+  slice_mword_dec w (top - i) (top - j)
+
+val slice_mword : forall 'a 'b. bool -> mword 'a -> integer -> integer -> mword 'b
+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 (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' =
+  let top = (length_mword w) - 1 in
+  update_slice_mword_dec w (top - i) (top - j) w'
+
+val update_slice_mword : forall 'a 'b. bool -> mword 'a -> integer -> integer -> mword 'b -> mword 'a
+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 (nat_of_int n))
+
+val access_mword_inc : forall 'a. mword 'a -> integer -> bitU
+let access_mword_inc w n =
+  let top = (length_mword w) - 1 in
+  access_mword_dec w (top - n)
+
+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_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_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_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 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 *)
+
+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 make_the_value _ = the_value
+
+(*** Bitvectors *)
+
+class (Bitvector 'a)
+  val bits_of : 'a -> list bitU
+  (* 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
+  (* 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 = 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 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 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 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 = 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 = 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 = 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' = 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. Bitvector 'a => integer -> 'a -> list bitU
+let extz_bv n v = extz_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 nat_of_bv : forall 'a. Bitvector 'a => 'a -> maybe nat
+let nat_of_bv v = Maybe.map nat_of_int (unsigned v)
+
+val string_of_bv : forall 'a. Bitvector 'a => 'a -> string
+let string_of_bv v = show_bitlist (bits_of v)
+
+val print_bits : forall 'a. Bitvector 'a => string -> 'a -> unit
+let print_bits str v = print_endline (str ^ string_of_bv v)
+
+val dec_str : integer -> string
+let dec_str bv = show bv
+
+val concat_str : string -> string -> string
+let concat_str str1 str2 = str1 ^ str2
+
+val int_of_bit : bitU -> integer
+let int_of_bit b =
+  match b with
+  | B0 -> 0
+  | B1 -> 1
+  | _ -> failwith "int_of_bit saw unknown"
+  end
+
+val count_leading_zero_bits : list bitU -> integer
+let rec count_leading_zero_bits v =
+  match v with
+  | B0 :: v' -> count_leading_zero_bits v' + 1
+  | _ -> 0
+  end
+
+val count_leading_zeros_bv : forall 'a. Bitvector 'a => 'a -> integer
+let count_leading_zeros_bv v = count_leading_zero_bits (bits_of v)
+
+val decimal_string_of_bv : forall 'a. Bitvector 'a => 'a -> string
+let decimal_string_of_bv bv =
+  let place_values =
+    List.mapi
+      (fun i b -> (int_of_bit b) * (2 ** i))
+      (List.reverse (bits_of bv))
+  in
+  let sum = List.foldl (+) 0 place_values in
+  show sum
+
+(*** Bytes and addresses *)
+
+type memory_byte = list bitU
+
+val byte_chunks : forall 'a. list 'a -> maybe (list (list 'a))
+let rec byte_chunks bs = match bs with
+  | [] -> Just []
+  | a::b::c::d::e::f::g::h::rest ->
+     Maybe.bind (byte_chunks rest) (fun rest -> Just ([a;b;c;d;e;f;g;h] :: rest))
+  | _ -> Nothing
+end
+declare {isabelle; hol} 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 : 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)
+
+(*val bitv_of_byte_lifteds : list Sail_impl_base.byte_lifted -> list bitU
+let bitv_of_byte_lifteds v =
+  foldl (fun x (Byte_lifted y) -> x ++ (List.map bitU_of_bit_lifted y)) [] v
+
+val bitv_of_bytes : list Sail_impl_base.byte -> list bitU
+let bitv_of_bytes v =
+  foldl (fun x (Byte y) -> x ++ (List.map bitU_of_bit y)) [] v
+
+val byte_lifteds_of_bitv : list bitU -> list byte_lifted
+let byte_lifteds_of_bitv bits =
+  let bits = List.map bit_lifted_of_bitU bits in
+  byte_lifteds_of_bit_lifteds bits
+
+val bytes_of_bitv : list bitU -> list byte
+let bytes_of_bitv bits =
+  let bits = List.map bit_of_bitU bits in
+  bytes_of_bits bits
+
+val bit_lifteds_of_bitUs : list bitU -> list bit_lifted
+let bit_lifteds_of_bitUs bits = List.map bit_lifted_of_bitU bits
+
+val bit_lifteds_of_bitv : list bitU -> list bit_lifted
+let bit_lifteds_of_bitv v = bit_lifteds_of_bitUs v
+
+
+val address_lifted_of_bitv : list bitU -> address_lifted
+let address_lifted_of_bitv v =
+  let byte_lifteds = byte_lifteds_of_bitv v in
+  let maybe_address_integer =
+    match (maybe_all (List.map byte_of_byte_lifted byte_lifteds)) with
+    | Just bs -> Just (integer_of_byte_list bs)
+    | _ -> Nothing
+    end in
+  Address_lifted byte_lifteds maybe_address_integer
+
+val bitv_of_address_lifted : address_lifted -> list bitU
+let bitv_of_address_lifted (Address_lifted bs _) = bitv_of_byte_lifteds bs
+
+val address_of_bitv : list bitU -> address
+let address_of_bitv v =
+  let bytes = bytes_of_bitv v in
+  address_of_byte_list bytes*)
+
+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
+
+
+(*** Registers *)
+
+(*type register_field = string
+type register_field_index = string * (integer * integer) (* name, start and end *)
+
+type register =
+  | Register of string * (* name *)
+                integer * (* length *)
+                integer * (* start index *)
+                bool * (* is increasing *)
+                  list register_field_index
+  | UndefinedRegister of integer (* length *)
+  | RegisterPair of register * register*)
+
+type register_ref 'regstate 'regval 'a =
+  <| name : string;
+     (*is_inc : bool;*)
+     read_from : 'regstate -> 'a;
+     write_to : 'a -> 'regstate -> 'regstate;
+     of_regval : 'regval -> maybe 'a;
+     regval_of : 'a -> 'regval |>
+
+(* Register accessors: pair of functions for reading and writing register values *)
+type register_accessors 'regstate 'regval =
+  ((string -> 'regstate -> maybe 'regval) *
+   (string -> 'regval -> 'regstate -> maybe 'regstate))
+
+type field_ref 'regtype 'a =
+  <| field_name : string;
+     field_start : integer;
+     field_is_inc : bool;
+     get_field : 'regtype -> 'a;
+     set_field : 'regtype -> 'a -> 'regtype |>
+
+(*let name_of_reg = function
+  | Register name _ _ _ _ -> name
+  | UndefinedRegister _ -> failwith "name_of_reg UndefinedRegister"
+  | RegisterPair _ _ -> failwith "name_of_reg RegisterPair"
+end
+
+let size_of_reg = function
+  | Register _ size _ _ _ -> size
+  | UndefinedRegister size -> size
+  | RegisterPair _ _ -> failwith "size_of_reg RegisterPair"
+end
+
+let start_of_reg = function
+  | Register _ _ start _ _ -> start
+  | UndefinedRegister _ -> failwith "start_of_reg UndefinedRegister"
+  | RegisterPair _ _ -> failwith "start_of_reg RegisterPair"
+end
+
+let is_inc_of_reg = function
+  | Register _ _ _ is_inc _ -> is_inc
+  | UndefinedRegister _ -> failwith "is_inc_of_reg UndefinedRegister"
+  | RegisterPair _ _ -> failwith "in_inc_of_reg RegisterPair"
+end
+
+let dir_of_reg = function
+  | Register _ _ _ is_inc _ -> dir_of_bool is_inc
+  | UndefinedRegister _ -> failwith "dir_of_reg UndefinedRegister"
+  | RegisterPair _ _ -> failwith "dir_of_reg RegisterPair"
+end
+
+let size_of_reg_nat reg = natFromInteger (size_of_reg reg)
+let start_of_reg_nat reg = natFromInteger (start_of_reg reg)
+
+val register_field_indices_aux : register -> register_field -> maybe (integer * integer)
+let rec register_field_indices_aux register rfield =
+  match register with
+  | Register _ _ _ _ rfields -> List.lookup rfield rfields
+  | RegisterPair r1 r2 ->
+      let m_indices = register_field_indices_aux r1 rfield in
+      if isJust m_indices then m_indices else register_field_indices_aux r2 rfield
+  | UndefinedRegister _ -> Nothing
+  end
+
+val register_field_indices : register -> register_field -> integer * integer
+let register_field_indices register rfield =
+  match register_field_indices_aux register rfield with
+  | Just indices -> indices
+  | Nothing -> failwith "Invalid register/register-field combination"
+  end
+
+let register_field_indices_nat reg regfield=
+  let (i,j) = register_field_indices reg regfield in
+  (natFromInteger i,natFromInteger j)*)
+
+(*let rec external_reg_value reg_name v =
+  let (internal_start, external_start, direction) =
+    match reg_name with
+     | Reg _ start size dir ->
+        (start, (if dir = D_increasing then start else (start - (size +1))), dir)
+     | Reg_slice _ reg_start dir (slice_start, _) ->
+        ((if dir = D_increasing then slice_start else (reg_start - slice_start)),
+         slice_start, dir)
+     | 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, _) ->
+        ((if dir = D_increasing then slice_start else (reg_start - slice_start)),
+         slice_start, dir)
+     end in
+  let bits = bit_lifteds_of_bitv v in
+  <| rv_bits           = bits;
+     rv_dir            = direction;
+     rv_start          = external_start;
+     rv_start_internal = internal_start |>
+
+val internal_reg_value : register_value -> list bitU
+let internal_reg_value v =
+  List.map bitU_of_bit_lifted v.rv_bits
+         (*(integerFromNat v.rv_start_internal)
+         (v.rv_dir = D_increasing)*)
+
+
+let external_slice (d:direction) (start:nat) ((i,j):(nat*nat)) =
+  match d with
+  (*This is the case the thread/concurrecny model expects, so no change needed*)
+  | D_increasing -> (i,j)
+  | D_decreasing -> let slice_i = start - i in
+                    let slice_j = (i - j) + slice_i in
+                    (slice_i,slice_j)
+  end *)
+
+(* TODO
+let external_reg_whole r =
+  Reg (r.name) (natFromInteger r.start) (natFromInteger r.size) (dir_of_bool r.is_inc)
+
+let external_reg_slice r (i,j) =
+  let start = natFromInteger r.start in
+  let dir = dir_of_bool r.is_inc in
+  Reg_slice (r.name) start dir (external_slice dir start (i,j))
+
+let external_reg_field_whole reg rfield =
+  let (m,n) = register_field_indices_nat reg rfield in
+  let start = start_of_reg_nat reg in
+  let dir = dir_of_reg reg in
+  Reg_field (name_of_reg reg) start dir rfield (external_slice dir start (m,n))
+
+let external_reg_field_slice reg rfield (i,j) =
+  let (m,n) = register_field_indices_nat reg rfield in
+  let start = start_of_reg_nat reg in
+  let dir = dir_of_reg reg in
+  Reg_f_slice (name_of_reg reg) start dir rfield
+              (external_slice dir start (m,n))
+              (external_slice dir start (i,j))*)
+
+(*val external_mem_value : list bitU -> memory_value
+let external_mem_value v =
+  byte_lifteds_of_bitv v $> List.reverse
+
+val internal_mem_value : memory_value -> list bitU
+let internal_mem_value bytes =
+  List.reverse bytes $> bitv_of_byte_lifteds*)
+
+
+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
+
+declare {isabelle; hol} termination_argument foreach = automatic
+
+val index_list : integer -> integer -> integer -> list integer
+let rec index_list from to step =
+  if (step > 0 && from <= to) || (step < 0 && to <= from) then
+    from :: index_list (from + step) to step
+  else []
+
+val while : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
+let rec while vars cond body =
+  if cond vars then while (body vars) cond body else vars
+
+val until : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
+let rec until vars cond body =
+  let vars = body vars in
+  if cond vars then vars else until (body vars) cond body
+
+
+(* convert numbers unsafely to naturals *)
+
+class (ToNatural 'a) val toNatural : 'a -> natural end
+(* eta-expanded for Isabelle output, otherwise it breaks *)
+instance (ToNatural integer) let toNatural = (fun n -> naturalFromInteger n) end
+instance (ToNatural int)     let toNatural = (fun n -> naturalFromInt n)     end
+instance (ToNatural nat)     let toNatural = (fun n -> naturalFromNat n)     end
+instance (ToNatural natural) let toNatural = (fun n -> n)                    end
+
+let toNaturalFiveTup (n1,n2,n3,n4,n5) =
+  (toNatural n1,
+   toNatural n2,
+   toNatural n3,
+   toNatural n4,
+   toNatural n5)
+
+(* Let the following types be generated by Sail per spec, using either bitlists
+   or machine words as bitvector representation *)
+(*type regfp =
+  | RFull of (string)
+  | RSlice of (string * integer * integer)
+  | RSliceBit of (string * integer)
+  | RField of (string * string)
+
+type niafp =
+  | NIAFP_successor
+  | NIAFP_concrete_address of vector bitU
+  | NIAFP_indirect_address
+
+(* only for MIPS *)
+type diafp =
+  | DIAFP_none
+  | DIAFP_concrete of vector bitU
+  | DIAFP_reg of regfp
+
+let regfp_to_reg (reg_info : string -> maybe string -> (nat * nat * direction * (nat * nat))) = function
+  | RFull name ->
+     let (start,length,direction,_) = reg_info name Nothing in
+     Reg name start length direction
+  | RSlice (name,i,j) ->
+     let i = natFromInteger i in
+     let j = natFromInteger j in
+     let (start,length,direction,_) = reg_info name Nothing in
+     let slice = external_slice direction start (i,j) in
+     Reg_slice name start direction slice
+  | RSliceBit (name,i) ->
+     let i = natFromInteger i in
+     let (start,length,direction,_) = reg_info name Nothing in
+     let slice = external_slice direction start (i,i) in
+     Reg_slice name start direction slice
+  | RField (name,field_name) ->
+     let (start,length,direction,span) = reg_info name (Just field_name) in
+     let slice = external_slice direction start span in
+     Reg_field name start direction field_name slice
+end
+
+let niafp_to_nia reginfo = function
+  | NIAFP_successor -> NIA_successor
+  | NIAFP_concrete_address v -> NIA_concrete_address (address_of_bitv v)
+  | NIAFP_indirect_address -> NIA_indirect_address
+end
+
+let diafp_to_dia reginfo = function
+  | DIAFP_none -> DIA_none
+  | DIAFP_concrete v -> DIA_concrete_address (address_of_bitv v)
+  | DIAFP_reg r -> DIA_register (regfp_to_reg reginfo r)
+end
+*)