Revert "Need to separate out the 0.10 lem library from upcoming 0.11"

This reverts commit 3fb4cf236c0d4b15831576faa45c763853632568.

14 files changed, 56 insertions, 5670 deletions

diff --git a/src/gen_lib/0.11/sail2_deep_shallow_convert.lem b/src/gen_lib/0.11/sail2_deep_shallow_convert.lem
deleted file mode 100644
index 2e3543b4..00000000
--- a/src/gen_lib/0.11/sail2_deep_shallow_convert.lem
+++ /dev/null
@@ -1,623 +0,0 @@
-open import Pervasives_extra
-open import Sail2_impl_base
-open import Sail2_interp
-open import Sail2_interp_ast
-open import Sail2_values
-
-
-class (ToFromInterpValue 'a)
-  val toInterpValue : 'a -> Interp_ast.value
-  val fromInterpValue : Interp_ast.value -> 'a
-end
-
-let toInterValueBool = function
-  | true -> Interp_ast.V_lit (L_aux (L_one) Unknown)
-  | false -> Interp_ast.V_lit (L_aux (L_zero) Unknown)
-end
-let rec fromInterpValueBool v = match v with
-  | Interp_ast.V_lit (L_aux (L_one) _)  -> true
-  | Interp_ast.V_lit (L_aux (L_true) _)  ->  true
-  | Interp_ast.V_lit (L_aux (L_zero) _) -> false
-  | Interp_ast.V_lit (L_aux (L_false) _) -> false
-  | Interp_ast.V_tuple [v] -> fromInterpValueBool v
-  | v -> failwith ("fromInterpValue bool: unexpected value. " ^
-                     Interp.debug_print_value v)
-end
-instance (ToFromInterpValue bool)
-  let toInterpValue = toInterValueBool
-  let fromInterpValue = fromInterpValueBool
-end
-
-
-let toInterpValueUnit () = Interp_ast.V_lit (L_aux (L_unit) Unknown)
-let rec fromInterpValueUnit v = match v with
-  | Interp_ast.V_lit (L_aux (L_unit) _) -> ()
-  | Interp_ast.V_tuple [v] -> fromInterpValueUnit v
-  | v -> failwith ("fromInterpValue unit: unexpected value. " ^
-                     Interp.debug_print_value v)
-end
-instance (ToFromInterpValue unit)
-  let toInterpValue = toInterpValueUnit
-  let fromInterpValue = fromInterpValueUnit
-end
-
-
-let toInterpValueInteger i = V_lit (L_aux (L_num i) Unknown)
-let rec fromInterpValueInteger v = match v with
-  | Interp_ast.V_lit (L_aux (L_num i) _) -> i
-  | Interp_ast.V_tuple [v] -> fromInterpValueInteger v
-  | v -> failwith ("fromInterpValue integer: unexpected value. " ^
-                     Interp.debug_print_value v)
-end
-instance (ToFromInterpValue integer)
-  let toInterpValue = toInterpValueInteger
-  let fromInterpValue = fromInterpValueInteger
-end
-
-
-let toInterpValueString s = V_lit (L_aux (L_string s) Unknown)
-let rec fromInterpValueString v = match v with
-  | Interp_ast.V_lit (L_aux (L_string s) _) -> s
-  | Interp_ast.V_tuple [v] -> fromInterpValueString v
-  | v -> failwith ("fromInterpValue integer: unexpected value. " ^
-                     Interp.debug_print_value v)
-end
-instance (ToFromInterpValue string)
-  let toInterpValue = toInterpValueString
-  let fromInterpValue = fromInterpValueString
-end
-
-
-let toInterpValueBitU = function
-  | B1 -> Interp_ast.V_lit (L_aux (L_one) Unknown)
-  | B0 -> Interp_ast.V_lit (L_aux (L_zero) Unknown)
-  | BU -> Interp_ast.V_lit (L_aux (L_undef) Unknown)
-end
-let rec fromInterpValueBitU v = match v with
-  | Interp_ast.V_lit (L_aux (L_one) _)   -> B1
-  | Interp_ast.V_lit (L_aux (L_zero) _)  -> B0
-  | Interp_ast.V_lit (L_aux (L_undef) _) -> BU
-  | Interp_ast.V_lit (L_aux (L_true) _)   -> B1
-  | Interp_ast.V_lit (L_aux (L_false) _)  -> B0 
-  | Interp_ast.V_tuple [v] -> fromInterpValueBitU v
-  | v -> failwith ("fromInterpValue bitU: unexpected value. " ^
-                     Interp.debug_print_value v)
-end
-instance (ToFromInterpValue bitU)
-  let toInterpValue = toInterpValueBitU
-  let fromInterpValue = fromInterpValueBitU
-end
-
-
-let tuple2ToInterpValue (a,b) =
-  V_tuple [toInterpValue a;toInterpValue b]
-let rec tuple2FromInterpValue v = match v with
-  | V_tuple [a;b] -> (fromInterpValue a,fromInterpValue b)
-  | V_tuple [v] -> tuple2FromInterpValue v
-  | v -> failwith ("fromInterpValue a*b: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-instance forall 'a 'b. ToFromInterpValue 'a, ToFromInterpValue 'b => (ToFromInterpValue ('a * 'b))
-  let toInterpValue = tuple2ToInterpValue
-  let fromInterpValue = tuple2FromInterpValue
-end
-
-
-let tuple3ToInterpValue (a,b,c) =
-  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c]
-let rec tuple3FromInterpValue v = match v with
-  | V_tuple [a;b;c] -> (fromInterpValue a,fromInterpValue b,fromInterpValue c)
-  | V_tuple [v] -> tuple3FromInterpValue v
-  | v -> failwith ("fromInterpValue a*b*c: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-instance forall 'a 'b 'c. ToFromInterpValue 'a, ToFromInterpValue 'b, ToFromInterpValue 'c =>
-    (ToFromInterpValue ('a * 'b * 'c))
-  let toInterpValue = tuple3ToInterpValue
-  let fromInterpValue = tuple3FromInterpValue
-end
-
-
-let tuple4ToInterpValue (a,b,c,d) =
-  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d]
-let rec tuple4FromInterpValue v = match v with
-  | V_tuple [a;b;c;d] -> (fromInterpValue a,fromInterpValue b,
-                          fromInterpValue c,fromInterpValue d)
-  | V_tuple [v] -> tuple4FromInterpValue v
-  | v -> failwith ("fromInterpValue a*b*c*d: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-instance forall 'a 'b 'c 'd. ToFromInterpValue 'a, ToFromInterpValue 'b,
-                             ToFromInterpValue 'c, ToFromInterpValue 'd =>
-    (ToFromInterpValue ('a * 'b * 'c * 'd))
-  let toInterpValue = tuple4ToInterpValue
-  let fromInterpValue = tuple4FromInterpValue
-end
-
-
-let tuple5ToInterpValue (a,b,c,d,e) =
-  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d;toInterpValue e]
-let rec tuple5FromInterpValue v = match v with
-  | V_tuple [a;b;c;d;e] ->
-     (fromInterpValue a,fromInterpValue b,fromInterpValue c,
-      fromInterpValue d,fromInterpValue e)
-  | V_tuple [v] -> tuple5FromInterpValue v
-  | v -> failwith ("fromInterpValue a*b*c*d*e: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-instance forall 'a 'b 'c 'd 'e.
-    ToFromInterpValue 'a, ToFromInterpValue 'b,
-    ToFromInterpValue 'c, ToFromInterpValue 'd,
-    ToFromInterpValue 'e =>
-    (ToFromInterpValue ('a * 'b * 'c * 'd * 'e))
-  let toInterpValue = tuple5ToInterpValue
-  let fromInterpValue = tuple5FromInterpValue
-end
-
-
-let tuple6ToInterpValue (a,b,c,d,e,f) =
-  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d;
-           toInterpValue e;toInterpValue f]
-let rec tuple6FromInterpValue v = match v with
-  | V_tuple [a;b;c;d;e;f] ->
-     (fromInterpValue a,fromInterpValue b,fromInterpValue c,
-      fromInterpValue d,fromInterpValue e,fromInterpValue f)
-  | V_tuple [v] -> tuple6FromInterpValue v
-  | v -> failwith ("fromInterpValue a*b*c*d*e*f: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-instance forall 'a 'b 'c 'd 'e 'f.
-    ToFromInterpValue 'a, ToFromInterpValue 'b,
-    ToFromInterpValue 'c, ToFromInterpValue 'd,
-    ToFromInterpValue 'e, ToFromInterpValue 'f =>
-    (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f))
-  let toInterpValue = tuple6ToInterpValue
-  let fromInterpValue = tuple6FromInterpValue
-end
-
-
-let tuple7ToInterpValue (a,b,c,d,e,f,g) =
-  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d;
-           toInterpValue e;toInterpValue f;toInterpValue g]
-let rec tuple7FromInterpValue v = match v with
-  | V_tuple [a;b;c;d;e;f;g] ->
-     (fromInterpValue a,fromInterpValue b,fromInterpValue c,
-      fromInterpValue d,fromInterpValue e,fromInterpValue f,
-      fromInterpValue g)
-  | V_tuple [v] -> tuple7FromInterpValue v
-  | v -> failwith ("fromInterpValue a*b*c*d*e*f*g: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-instance forall 'a 'b 'c 'd 'e 'f 'g.
-    ToFromInterpValue 'a, ToFromInterpValue 'b,
-    ToFromInterpValue 'c, ToFromInterpValue 'd,
-    ToFromInterpValue 'e, ToFromInterpValue 'f,
-    ToFromInterpValue 'g =>
-    (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f * 'g))
-  let toInterpValue = tuple7ToInterpValue
-  let fromInterpValue = tuple7FromInterpValue
-end
-
-
-let tuple8ToInterpValue (a,b,c,d,e,f,g,h) =
-  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d;
-           toInterpValue e;toInterpValue f;toInterpValue g;toInterpValue h]
-let rec tuple8FromInterpValue v = match v with
-  | V_tuple [a;b;c;d;e;f;g;h] ->
-     (fromInterpValue a,fromInterpValue b,fromInterpValue c,
-      fromInterpValue d,fromInterpValue e,fromInterpValue f,
-      fromInterpValue g,fromInterpValue h)
-  | V_tuple [v] -> tuple8FromInterpValue v
-  | v -> failwith ("fromInterpValue a*b*c*d*e*f*g*h: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-instance forall 'a 'b 'c 'd 'e 'f 'g 'h.
-    ToFromInterpValue 'a, ToFromInterpValue 'b,
-    ToFromInterpValue 'c, ToFromInterpValue 'd,
-    ToFromInterpValue 'e, ToFromInterpValue 'f,
-    ToFromInterpValue 'g, ToFromInterpValue 'h =>
-    (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h))
-  let toInterpValue = tuple8ToInterpValue
-  let fromInterpValue = tuple8FromInterpValue
-end
-
-
-let tuple9ToInterpValue (a,b,c,d,e,f,g,h,i) =
-  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d;
-           toInterpValue e;toInterpValue f;toInterpValue g;toInterpValue h;
-           toInterpValue i]
-let rec tuple9FromInterpValue v = match v with
-  | V_tuple [a;b;c;d;e;f;g;h;i] ->
-     (fromInterpValue a,fromInterpValue b,fromInterpValue c,
-      fromInterpValue d,fromInterpValue e,fromInterpValue f,
-      fromInterpValue g,fromInterpValue h,fromInterpValue i)
-  | V_tuple [v] -> tuple9FromInterpValue v
-  | v -> failwith ("fromInterpValue a*b*c*d*e*f*g*h*i: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-instance forall 'a 'b 'c 'd 'e 'f 'g 'h 'i.
-    ToFromInterpValue 'a, ToFromInterpValue 'b,
-    ToFromInterpValue 'c, ToFromInterpValue 'd,
-    ToFromInterpValue 'e, ToFromInterpValue 'f,
-    ToFromInterpValue 'g, ToFromInterpValue 'h,
-    ToFromInterpValue 'i =>
-    (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i))
-  let toInterpValue = tuple9ToInterpValue
-  let fromInterpValue = tuple9FromInterpValue
-end
-
-
-let tuple10ToInterpValue (a,b,c,d,e,f,g,h,i,j) =
-  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d;
-           toInterpValue e;toInterpValue f;toInterpValue g;toInterpValue h;
-           toInterpValue i;toInterpValue j;]
-let rec tuple10FromInterpValue v = match v with
-  | V_tuple [a;b;c;d;e;f;g;h;i;j] ->
-     (fromInterpValue a,fromInterpValue b,fromInterpValue c,
-      fromInterpValue d,fromInterpValue e,fromInterpValue f,
-      fromInterpValue g,fromInterpValue h,fromInterpValue i,
-      fromInterpValue j)
-  | V_tuple [v] -> tuple10FromInterpValue v
-  | v -> failwith ("fromInterpValue a*b*c*d*e*f*g*h*i*j: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-instance forall 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j.
-    ToFromInterpValue 'a, ToFromInterpValue 'b,
-    ToFromInterpValue 'c, ToFromInterpValue 'd,
-    ToFromInterpValue 'e, ToFromInterpValue 'f,
-    ToFromInterpValue 'g, ToFromInterpValue 'h,
-    ToFromInterpValue 'i, ToFromInterpValue 'j =>
-    (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j))
-  let toInterpValue = tuple10ToInterpValue
-  let fromInterpValue = tuple10FromInterpValue
-end
-
-
-let tuple11ToInterpValue (a,b,c,d,e,f,g,h,i,j,k) =
-  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d;
-           toInterpValue e;toInterpValue f;toInterpValue g;toInterpValue h;
-           toInterpValue i;toInterpValue j;toInterpValue k;]
-let rec tuple11FromInterpValue v = match v with
-  | V_tuple [a;b;c;d;e;f;g;h;i;j;k] ->
-     (fromInterpValue a,fromInterpValue b,fromInterpValue c,
-      fromInterpValue d,fromInterpValue e,fromInterpValue f,
-      fromInterpValue g,fromInterpValue h,fromInterpValue i,
-      fromInterpValue j,fromInterpValue k)
-  | V_tuple [v] -> tuple11FromInterpValue v
-  | v -> failwith ("fromInterpValue a*b*c*d*e*f*g*h*i*j*k: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-instance forall 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j 'k.
-    ToFromInterpValue 'a, ToFromInterpValue 'b,
-    ToFromInterpValue 'c, ToFromInterpValue 'd,
-    ToFromInterpValue 'e, ToFromInterpValue 'f,
-    ToFromInterpValue 'g, ToFromInterpValue 'h,
-    ToFromInterpValue 'i, ToFromInterpValue 'j,
-    ToFromInterpValue 'k =>
-    (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k))
-  let toInterpValue = tuple11ToInterpValue
-  let fromInterpValue = tuple11FromInterpValue
-end
-
-
-let tuple12ToInterpValue (a,b,c,d,e,f,g,h,i,j,k,l) =
-  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d;
-           toInterpValue e;toInterpValue f;toInterpValue g;toInterpValue h;
-           toInterpValue i;toInterpValue j;toInterpValue k;toInterpValue l;]
-let rec tuple12FromInterpValue v = match v with
-  | V_tuple [a;b;c;d;e;f;g;h;i;j;k;l] ->
-     (fromInterpValue a,fromInterpValue b,fromInterpValue c,
-      fromInterpValue d,fromInterpValue e,fromInterpValue f,
-      fromInterpValue g,fromInterpValue h,fromInterpValue i,
-      fromInterpValue j,fromInterpValue k,fromInterpValue l)
-  | V_tuple [v] -> tuple12FromInterpValue v
-  | v -> failwith ("fromInterpValue a*b*c*d*e*f*g*h*i*j*k*l: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-instance forall 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j 'k 'l.
-    ToFromInterpValue 'a, ToFromInterpValue 'b,
-    ToFromInterpValue 'c, ToFromInterpValue 'd,
-    ToFromInterpValue 'e, ToFromInterpValue 'f,
-    ToFromInterpValue 'g, ToFromInterpValue 'h,
-    ToFromInterpValue 'i, ToFromInterpValue 'j,
-    ToFromInterpValue 'k, ToFromInterpValue 'l =>
-    (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k * 'l))
-  let toInterpValue = tuple12ToInterpValue
-  let fromInterpValue = tuple12FromInterpValue
-end
-
-
-let listToInterpValue l = V_list (List.map toInterpValue l)
-let rec listFromInterpValue v = match v with
-  | V_list l -> List.map fromInterpValue l
-  | V_tuple [v] -> listFromInterpValue v
-  | v -> failwith ("fromInterpValue list 'a: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-instance forall 'a. ToFromInterpValue 'a => (ToFromInterpValue (list 'a))
-  let toInterpValue = listToInterpValue
-  let fromInterpValue = listFromInterpValue
-end
-
-
-let vectorToInterpValue (Vector vs start direction) =
-  V_vector (natFromInteger start) (if direction then IInc else IDec) (List.map toInterpValue vs)
-let rec vectorFromInterpValue v = match v with
-  | V_vector start direction vs ->
-     Vector (List.map fromInterpValue vs) (integerFromNat start)
-            (match direction with | IInc -> true | IDec -> false end)
-  | V_vector_sparse start length direction valuemap defaultval ->
-     make_indexed_vector
-       (List.map (fun (i,v) -> (integerFromNat i,fromInterpValue v)) valuemap)
-       (fromInterpValue defaultval)
-       (integerFromNat start) (integerFromNat length)
-       (match direction with | IInc -> true | IDec -> false end)
-  | V_tuple [v] -> vectorFromInterpValue v
-  | v -> failwith ("fromInterpValue vector 'a: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-instance forall 'a. ToFromInterpValue 'a => (ToFromInterpValue (vector 'a))
-  let toInterpValue = vectorToInterpValue
-  let fromInterpValue = vectorFromInterpValue
-end
-
-(* Here the type information is not accurate: instead of T_id "option" it should
-   be T_app (T_id "option") (...), but temporarily we'll do it like this. The
-   same thing has to be fixed in pretty_print.ml when we're generating the
-   type-class instances. *)
-let maybeToInterpValue = function
-  | Nothing -> V_ctor (Id_aux (Id "None") Unknown) (T_id "option") C_Union (V_lit (L_aux L_unit Unknown))
-  | Just a  -> V_ctor (Id_aux (Id "Some") Unknown) (T_id "option") C_Union (toInterpValue a)
-  end
-let rec maybeFromInterpValue v = match v with
-  | V_ctor (Id_aux (Id "None") _) _ _ _ -> Nothing
-  | V_ctor (Id_aux (Id "Some") _) _ _ v -> Just (fromInterpValue v)
-  | V_tuple [v] -> maybeFromInterpValue v
-  | v -> failwith ("fromInterpValue maybe 'a: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-
-instance forall 'a. ToFromInterpValue 'a => (ToFromInterpValue (maybe 'a))
-  let toInterpValue = maybeToInterpValue
-  let fromInterpValue = maybeFromInterpValue
-end
-
-
-let read_kindToInterpValue = function
-  | Read_plain -> V_ctor (Id_aux (Id "Read_plain") Unknown) (T_id "read_kind") (C_Enum 0) (toInterpValue ())
-  | Read_reserve -> V_ctor (Id_aux (Id "Read_reserve") Unknown) (T_id "read_kind") (C_Enum 1) (toInterpValue ())
-  | Read_acquire -> V_ctor (Id_aux (Id "Read_acquire") Unknown) (T_id "read_kind") (C_Enum 2) (toInterpValue ())
-  | Read_exclusive -> V_ctor (Id_aux (Id "Read_exclusive") Unknown) (T_id "read_kind") (C_Enum 3) (toInterpValue ())
-  | Read_exclusive_acquire -> V_ctor (Id_aux (Id "Read_exclusive_acquire") Unknown) (T_id "read_kind") (C_Enum 4) (toInterpValue ())
-  | Read_stream -> V_ctor (Id_aux (Id "Read_stream") Unknown) (T_id "read_kind") (C_Enum 5) (toInterpValue ())
-  | Read_RISCV_acquire -> V_ctor (Id_aux (Id "Read_RISCV_acquire") Unknown) (T_id "read_kind") (C_Enum 6) (toInterpValue ())
-  | Read_RISCV_strong_acquire -> V_ctor (Id_aux (Id "Read_RISCV_strong_acquire") Unknown) (T_id "read_kind") (C_Enum 7) (toInterpValue ())
-  | Read_RISCV_reserved -> V_ctor (Id_aux (Id "Read_RISCV_reserved") Unknown) (T_id "read_kind") (C_Enum 8) (toInterpValue ())
-  | Read_RISCV_reserved_acquire -> V_ctor (Id_aux (Id "Read_RISCV_reserved_acquire") Unknown) (T_id "read_kind") (C_Enum 9) (toInterpValue ())
-  | Read_RISCV_reserved_strong_acquire -> V_ctor (Id_aux (Id "Read_RISCV_reserved_strong_acquire") Unknown) (T_id "read_kind") (C_Enum 10) (toInterpValue ())
-  | Read_X86_locked -> V_ctor (Id_aux (Id "Read_X86_locked") Unknown) (T_id "read_kind") (C_Enum 11) (toInterpValue ())
-  end
-let rec read_kindFromInterpValue v = match v with
-  | V_ctor (Id_aux (Id "Read_plain") _) _ _ v -> Read_plain
-  | V_ctor (Id_aux (Id "Read_reserve") _) _ _ v -> Read_reserve
-  | V_ctor (Id_aux (Id "Read_acquire") _) _ _ v -> Read_acquire
-  | V_ctor (Id_aux (Id "Read_exclusive") _) _ _ v -> Read_exclusive
-  | V_ctor (Id_aux (Id "Read_exclusive_acquire") _) _ _ v -> Read_exclusive_acquire
-  | V_ctor (Id_aux (Id "Read_stream") _) _ _ v -> Read_stream
-  | V_ctor (Id_aux (Id "Read_RISCV_acquire") _) _ _ v -> Read_RISCV_acquire
-  | V_ctor (Id_aux (Id "Read_RISCV_strong_acquire") _) _ _ v -> Read_RISCV_strong_acquire
-  | V_ctor (Id_aux (Id "Read_RISCV_reserved") _) _ _ v -> Read_RISCV_reserved
-  | V_ctor (Id_aux (Id "Read_RISCV_reserved_acquire") _) _ _ v -> Read_RISCV_reserved_acquire
-  | V_ctor (Id_aux (Id "Read_RISCV_reserved_strong_acquire") _) _ _ v -> Read_RISCV_reserved_strong_acquire
-  | V_ctor (Id_aux (Id "Read_X86_locked") _) _ _ v -> Read_X86_locked
-  | V_tuple [v] -> read_kindFromInterpValue v
-  | v -> failwith ("fromInterpValue read_kind: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-instance (ToFromInterpValue read_kind)
-  let toInterpValue = read_kindToInterpValue
-  let fromInterpValue = read_kindFromInterpValue
-end
-
-
-let write_kindToInterpValue = function
-  | Write_plain -> V_ctor (Id_aux (Id "Write_plain") Unknown) (T_id "write_kind") (C_Enum 0) (toInterpValue ())
-  | Write_conditional -> V_ctor (Id_aux (Id "Write_conditional") Unknown) (T_id "write_kind") (C_Enum 1) (toInterpValue ())
-  | Write_release -> V_ctor (Id_aux (Id "Write_release") Unknown) (T_id "write_kind") (C_Enum 2) (toInterpValue ())
-  | Write_exclusive -> V_ctor (Id_aux (Id "Write_exclusive") Unknown) (T_id "write_kind") (C_Enum 3) (toInterpValue ())
-  | Write_exclusive_release -> V_ctor (Id_aux (Id "Write_exclusive_release") Unknown) (T_id "write_kind") (C_Enum 4) (toInterpValue ())
-  | Write_RISCV_release -> V_ctor (Id_aux (Id "Write_RISCV_release") Unknown) (T_id "write_kind") (C_Enum 5) (toInterpValue ())
-  | Write_RISCV_strong_release -> V_ctor (Id_aux (Id "Write_RISCV_strong_release") Unknown) (T_id "write_kind") (C_Enum 6) (toInterpValue ())
-  | Write_RISCV_conditional -> V_ctor (Id_aux (Id "Write_RISCV_conditional") Unknown) (T_id "write_kind") (C_Enum 7) (toInterpValue ())
-  | Write_RISCV_conditional_release -> V_ctor (Id_aux (Id "Write_RISCV_conditional_release") Unknown) (T_id "write_kind") (C_Enum 8) (toInterpValue ())
-  | Write_RISCV_conditional_strong_release -> V_ctor (Id_aux (Id "Write_RISCV_conditional_strong_release") Unknown) (T_id "write_kind") (C_Enum 9) (toInterpValue ())
-  | Write_X86_locked -> V_ctor (Id_aux (Id "Write_X86_locked") Unknown) (T_id "write_kind") (C_Enum 10) (toInterpValue ())
-  end
-let rec write_kindFromInterpValue v = match v with
-  | V_ctor (Id_aux (Id "Write_plain") _) _ _ v -> Write_plain
-  | V_ctor (Id_aux (Id "Write_conditional") _) _ _ v -> Write_conditional
-  | V_ctor (Id_aux (Id "Write_release") _) _ _ v -> Write_release
-  | V_ctor (Id_aux (Id "Write_exclusive") _) _ _ v -> Write_exclusive
-  | V_ctor (Id_aux (Id "Write_exclusive_release") _) _ _ v -> Write_exclusive_release
-  | V_ctor (Id_aux (Id "Write_RISCV_release") _) _ _ v -> Write_RISCV_release
-  | V_ctor (Id_aux (Id "Write_RISCV_strong_release") _) _ _ v -> Write_RISCV_strong_release
-  | V_ctor (Id_aux (Id "Write_RISCV_conditional") _) _ _ v -> Write_RISCV_conditional
-  | V_ctor (Id_aux (Id "Write_RISCV_conditional_release") _) _ _ v -> Write_RISCV_conditional_release
-  | V_ctor (Id_aux (Id "Write_RISCV_conditional_strong_release") _) _ _ v -> Write_RISCV_conditional_strong_release
-  | V_ctor (Id_aux (Id "Write_X86_locked") _) _ _ v -> Write_X86_locked
-  | V_tuple [v] -> write_kindFromInterpValue v
-  | v -> failwith ("fromInterpValue write_kind: unexpected value " ^
-                     Interp.debug_print_value v)
-  end
-instance (ToFromInterpValue write_kind)
-  let toInterpValue = write_kindToInterpValue
-  let fromInterpValue = write_kindFromInterpValue
-end
-
-
-let a64_barrier_domainToInterpValue = function
-  | A64_FullShare ->
-    V_ctor (Id_aux (Id "A64_FullShare") Unknown) (T_id "a64_barrier_domain") (C_Enum 0) (toInterpValue ())
-  | A64_InnerShare ->
-    V_ctor (Id_aux (Id "A64_InnerShare") Unknown) (T_id "a64_barrier_domain") (C_Enum 1) (toInterpValue ())
-  | A64_OuterShare ->
-    V_ctor (Id_aux (Id "A64_OuterShare") Unknown) (T_id "a64_barrier_domain") (C_Enum 2) (toInterpValue ())
-  | A64_NonShare ->
-    V_ctor (Id_aux (Id "A64_NonShare") Unknown) (T_id "a64_barrier_domain") (C_Enum 3) (toInterpValue ())
-end
-let rec a64_barrier_domainFromInterpValue v = match v with
-  | V_ctor (Id_aux (Id "A64_FullShare") _) _ _ v -> A64_FullShare
-  | V_ctor (Id_aux (Id "A64_InnerShare") _) _ _ v -> A64_InnerShare
-  | V_ctor (Id_aux (Id "A64_OuterShare") _) _ _ v -> A64_OuterShare
-  | V_ctor (Id_aux (Id "A64_NonShare") _) _ _ v -> A64_NonShare
-  | V_tuple [v] -> a64_barrier_domainFromInterpValue v
-  | v -> failwith ("fromInterpValue a64_barrier_domain: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-instance (ToFromInterpValue a64_barrier_domain)
-  let toInterpValue = a64_barrier_domainToInterpValue
-  let fromInterpValue = a64_barrier_domainFromInterpValue
-end
-
-let a64_barrier_typeToInterpValue = function
-  | A64_barrier_all ->
-    V_ctor (Id_aux (Id "A64_barrier_all") Unknown) (T_id "a64_barrier_type") (C_Enum 0) (toInterpValue ())
-  | A64_barrier_LD ->
-    V_ctor (Id_aux (Id "A64_barrier_LD") Unknown) (T_id "a64_barrier_type") (C_Enum 1) (toInterpValue ())
-  | A64_barrier_ST ->
-    V_ctor (Id_aux (Id "A64_barrier_ST") Unknown) (T_id "a64_barrier_type") (C_Enum 2) (toInterpValue ())
-end
-let rec a64_barrier_typeFromInterpValue v = match v with
-  | V_ctor (Id_aux (Id "A64_barrier_all") _) _ _ v -> A64_barrier_all
-  | V_ctor (Id_aux (Id "A64_barrier_LD") _) _ _ v -> A64_barrier_LD
-  | V_ctor (Id_aux (Id "A64_barrier_ST") _) _ _ v -> A64_barrier_ST
-  | V_tuple [v] -> a64_barrier_typeFromInterpValue v
-  | v -> failwith ("fromInterpValue a64_barrier_type: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-instance (ToFromInterpValue a64_barrier_type)
-  let toInterpValue = a64_barrier_typeToInterpValue
-  let fromInterpValue = a64_barrier_typeFromInterpValue
-end
-
-
-let barrier_kindToInterpValue = function
-  | Barrier_Sync -> V_ctor (Id_aux (Id "Barrier_Sync") Unknown) (T_id "barrier_kind") (C_Enum 0) (toInterpValue ())
-  | Barrier_LwSync -> V_ctor (Id_aux (Id "Barrier_LwSync") Unknown) (T_id "barrier_kind") (C_Enum 1) (toInterpValue ())
-  | Barrier_Eieio -> V_ctor (Id_aux (Id "Barrier_Eieio") Unknown) (T_id "barrier_kind") (C_Enum 2) (toInterpValue ())
-  | Barrier_Isync -> V_ctor (Id_aux (Id "Barrier_Isync") Unknown) (T_id "barrier_kind") (C_Enum 3) (toInterpValue ())
-  | Barrier_DMB (dom,typ) ->
-      V_ctor (Id_aux (Id "Barrier_DMB") Unknown) (T_id "barrier_kind") C_Union (toInterpValue (dom, typ))
-  | Barrier_DSB (dom,typ) ->
-      V_ctor (Id_aux (Id "Barrier_DSB") Unknown) (T_id "barrier_kind") C_Union (toInterpValue (dom, typ))
-  | Barrier_ISB -> V_ctor (Id_aux (Id "Barrier_ISB") Unknown) (T_id "barrier_kind") (C_Enum 10) (toInterpValue ())
-  | Barrier_TM_COMMIT -> V_ctor (Id_aux (Id "Barrier_TM_COMMIT") Unknown) (T_id "barrier_kind") (C_Enum 11) (toInterpValue ())
-  | Barrier_MIPS_SYNC -> V_ctor (Id_aux (Id "Barrier_MIPS_SYNC") Unknown) (T_id "barrier_kind") (C_Enum 12) (toInterpValue ())
-  | Barrier_RISCV_rw_rw -> V_ctor (Id_aux (Id "Barrier_RISCV_rw_rw") Unknown) (T_id "barrier_kind") (C_Enum 13) (toInterpValue ())
-  | Barrier_RISCV_r_rw -> V_ctor (Id_aux (Id "Barrier_RISCV_r_rw") Unknown) (T_id "barrier_kind") (C_Enum 14) (toInterpValue ())
-  | Barrier_RISCV_r_r -> V_ctor (Id_aux (Id "Barrier_RISCV_r_r") Unknown) (T_id "barrier_kind") (C_Enum 15) (toInterpValue ())
-  | Barrier_RISCV_rw_w -> V_ctor (Id_aux (Id "Barrier_RISCV_rw_w") Unknown) (T_id "barrier_kind") (C_Enum 16) (toInterpValue ())
-  | Barrier_RISCV_w_w -> V_ctor (Id_aux (Id "Barrier_RISCV_w_w") Unknown) (T_id "barrier_kind") (C_Enum 17) (toInterpValue ())
-  | Barrier_RISCV_i -> V_ctor (Id_aux (Id "Barrier_RISCV_i") Unknown) (T_id "barrier_kind") (C_Enum 18) (toInterpValue ())
-  | Barrier_x86_MFENCE -> V_ctor (Id_aux (Id "Barrier_x86_MFENCE") Unknown) (T_id "barrier_kind") (C_Enum 19) (toInterpValue ())
-  end
-let rec barrier_kindFromInterpValue v = match v with
-  | V_ctor (Id_aux (Id "Barrier_Sync") _) _ _ v -> Barrier_Sync
-  | V_ctor (Id_aux (Id "Barrier_LwSync") _) _ _ v -> Barrier_LwSync
-  | V_ctor (Id_aux (Id "Barrier_Eieio") _) _ _ v -> Barrier_Eieio
-  | V_ctor (Id_aux (Id "Barrier_Isync") _) _ _ v -> Barrier_Isync
-  | V_ctor (Id_aux (Id "Barrier_DMB") _) _ _ v ->
-      let (dom, typ) = fromInterpValue v in
-      Barrier_DMB (dom,typ)
-  | V_ctor (Id_aux (Id "Barrier_DSB") _) _ _ v ->
-      let (dom, typ) = fromInterpValue v in
-      Barrier_DSB (dom,typ)
-  | V_ctor (Id_aux (Id "Barrier_ISB") _) _ _ v -> Barrier_ISB
-  | V_ctor (Id_aux (Id "Barrier_TM_COMMIT") _) _ _ v -> Barrier_TM_COMMIT
-  | V_ctor (Id_aux (Id "Barrier_MIPS_SYNC") _) _ _ v -> Barrier_MIPS_SYNC
-  | V_ctor (Id_aux (Id "Barrier_RISCV_rw_rw") _) _ _ v -> Barrier_RISCV_rw_rw
-  | V_ctor (Id_aux (Id "Barrier_RISCV_r_rw") _) _ _ v -> Barrier_RISCV_r_rw
-  | V_ctor (Id_aux (Id "Barrier_RISCV_r_r") _) _ _ v -> Barrier_RISCV_r_r
-  | V_ctor (Id_aux (Id "Barrier_RISCV_rw_w") _) _ _ v -> Barrier_RISCV_rw_w
-  | V_ctor (Id_aux (Id "Barrier_RISCV_w_w") _) _ _ v -> Barrier_RISCV_w_w
-  | V_ctor (Id_aux (Id "Barrier_RISCV_i") _) _ _ v -> Barrier_RISCV_i
-  | V_ctor (Id_aux (Id "Barrier_x86_MFENCE") _) _ _ v -> Barrier_x86_MFENCE
-  | V_tuple [v] -> barrier_kindFromInterpValue v
-  | v -> failwith ("fromInterpValue barrier_kind: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-instance (ToFromInterpValue barrier_kind)
-  let toInterpValue = barrier_kindToInterpValue
-  let fromInterpValue = barrier_kindFromInterpValue
-end
-
-
-let trans_kindToInterpValue = function
-  | Transaction_start -> V_ctor (Id_aux (Id "Transaction_start") Unknown) (T_id "trans_kind") (C_Enum 0) (toInterpValue ())
-  | Transaction_commit -> V_ctor (Id_aux (Id "Transaction_commit") Unknown) (T_id "trans_kind") (C_Enum 1) (toInterpValue ())
-  | Transaction_abort -> V_ctor (Id_aux (Id "Transaction_abort") Unknown) (T_id "trans_kind") (C_Enum 2) (toInterpValue ())
-  end
-let rec trans_kindFromInterpValue v = match v with
-  | V_ctor (Id_aux (Id "Transaction_start") _) _ _ v -> Transaction_start
-  | V_ctor (Id_aux (Id "Transaction_commit") _) _ _ v -> Transaction_commit
-  | V_ctor (Id_aux (Id "Transaction_abort") _) _ _ v -> Transaction_abort
-  | V_tuple [v] -> trans_kindFromInterpValue v
-  | v -> failwith ("fromInterpValue trans_kind: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-instance (ToFromInterpValue trans_kind)
-  let toInterpValue = trans_kindToInterpValue
-  let fromInterpValue = trans_kindFromInterpValue
-end
-
-
-let instruction_kindToInterpValue = function
-  | IK_barrier v -> V_ctor (Id_aux (Id "IK_barrier") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v)
-  | IK_mem_read v -> V_ctor (Id_aux (Id "IK_mem_read") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v)
-  | IK_mem_write v -> V_ctor (Id_aux (Id "IK_mem_write") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v)
-  | IK_mem_rmw v -> V_ctor (Id_aux (Id "IK_mem_rmw") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v)
-  | IK_branch -> V_ctor (Id_aux (Id "IK_branch") Unknown) (T_id "instruction_kind") C_Union (toInterpValue ())
-  | IK_trans v -> V_ctor (Id_aux (Id "IK_trans") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v)
-  | IK_simple -> V_ctor (Id_aux (Id "IK_simple") Unknown) (T_id "instruction_kind") C_Union (toInterpValue ())
-  end
-let rec instruction_kindFromInterpValue v = match v with
-  | V_ctor (Id_aux (Id "IK_barrier") _) _ _ v -> IK_barrier (fromInterpValue v)
-  | V_ctor (Id_aux (Id "IK_mem_read") _) _ _ v -> IK_mem_read (fromInterpValue v)
-  | V_ctor (Id_aux (Id "IK_mem_write") _) _ _ v -> IK_mem_write (fromInterpValue v)
-  | V_ctor (Id_aux (Id "IK_mem_rmw") _) _ _ v -> IK_mem_rmw (fromInterpValue v)
-  | V_ctor (Id_aux (Id "IK_branch") _) _ _ v -> IK_branch
-  | V_ctor (Id_aux (Id "IK_trans") _) _ _ v -> IK_trans (fromInterpValue v)
-  | V_ctor (Id_aux (Id "IK_simple") _) _ _ v -> IK_simple
-  | V_tuple [v] -> instruction_kindFromInterpValue v
-  | v -> failwith ("fromInterpValue instruction_kind: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-instance (ToFromInterpValue instruction_kind)
-  let toInterpValue = instruction_kindToInterpValue
-  let fromInterpValue = instruction_kindFromInterpValue
-end
-
-let regfpToInterpValue = function
-  | RFull v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RFull") Interp_ast.Unknown) (Interp_ast.T_id "regfp") Interp_ast.C_Union (toInterpValue v)
-  | RSlice v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RSlice") Interp_ast.Unknown) (Interp_ast.T_id "regfp") Interp_ast.C_Union (toInterpValue v)
-  | RSliceBit v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RSliceBit") Interp_ast.Unknown) (Interp_ast.T_id "regfp") Interp_ast.C_Union (toInterpValue v)
-  | RField v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RField") Interp_ast.Unknown) (Interp_ast.T_id "regfp") Interp_ast.C_Union (toInterpValue v)
-  end
-
-let rec regfpFromInterpValue v = match v with
-  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RFull") _) _ _ v -> RFull (fromInterpValue v)
-  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RSlice") _) _ _ v -> RSlice (fromInterpValue v)
-  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RSliceBit") _) _ _ v -> RSliceBit (fromInterpValue v)
-  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RField") _) _ _ v -> RField (fromInterpValue v)
-  | Interp_ast.V_tuple [v] -> regfpFromInterpValue v
-  | v -> failwith ("fromInterpValue regfp: unexpected value. " ^ Interp.debug_print_value v)
-  end
-
-instance (ToFromInterpValue regfp)
-  let toInterpValue = regfpToInterpValue
-  let fromInterpValue = regfpFromInterpValue
-end
-
-
-
-
diff --git a/src/gen_lib/0.11/sail2_instr_kinds.lem b/src/gen_lib/0.11/sail2_instr_kinds.lem
deleted file mode 100644
index 3d238676..00000000
--- a/src/gen_lib/0.11/sail2_instr_kinds.lem
+++ /dev/null
@@ -1,306 +0,0 @@
-(*========================================================================*)
-(*     Sail                                                               *)
-(*                                                                        *)
-(*  Copyright (c) 2013-2017                                               *)
-(*    Kathyrn Gray                                                        *)
-(*    Shaked Flur                                                         *)
-(*    Stephen Kell                                                        *)
-(*    Gabriel Kerneis                                                     *)
-(*    Robert Norton-Wright                                                *)
-(*    Christopher Pulte                                                   *)
-(*    Peter Sewell                                                        *)
-(*    Alasdair Armstrong                                                  *)
-(*    Brian Campbell                                                      *)
-(*    Thomas Bauereiss                                                    *)
-(*    Anthony Fox                                                         *)
-(*    Jon French                                                          *)
-(*    Dominic Mulligan                                                    *)
-(*    Stephen Kell                                                        *)
-(*    Mark Wassell                                                        *)
-(*                                                                        *)
-(*  All rights reserved.                                                  *)
-(*                                                                        *)
-(*  This software was developed by the University of Cambridge Computer   *)
-(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
-(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
-(*                                                                        *)
-(*  Redistribution and use in source and binary forms, with or without    *)
-(*  modification, are permitted provided that the following conditions    *)
-(*  are met:                                                              *)
-(*  1. Redistributions of source code must retain the above copyright     *)
-(*     notice, this list of conditions and the following disclaimer.      *)
-(*  2. Redistributions in binary form must reproduce the above copyright  *)
-(*     notice, this list of conditions and the following disclaimer in    *)
-(*     the documentation and/or other materials provided with the         *)
-(*     distribution.                                                      *)
-(*                                                                        *)
-(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
-(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
-(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
-(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
-(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
-(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
-(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
-(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
-(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
-(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
-(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
-(*  SUCH DAMAGE.                                                          *)
-(*========================================================================*)
-
-open import Pervasives_extra
-
-
-class ( EnumerationType 'a )
-  val toNat : 'a -> nat
-end
-
-
-val enumeration_typeCompare : forall 'a. EnumerationType 'a => 'a -> 'a -> ordering
-let ~{ocaml} enumeration_typeCompare e1 e2 =
-  compare (toNat e1) (toNat e2)
-let inline {ocaml} enumeration_typeCompare = defaultCompare
-
-
-default_instance forall 'a. EnumerationType 'a => (Ord 'a)
-  let compare = enumeration_typeCompare
-  let (<)  r1 r2 = (enumeration_typeCompare r1 r2) = LT
-  let (<=) r1 r2 = (enumeration_typeCompare r1 r2) <> GT
-  let (>)  r1 r2 = (enumeration_typeCompare r1 r2) = GT
-  let (>=) r1 r2 = (enumeration_typeCompare r1 r2) <> LT
-end
-
-
-(* Data structures for building up instructions *)
-
-(* careful: changes in the read/write/barrier kinds have to be
-   reflected in deep_shallow_convert *)
-type read_kind =
-  (* common reads *)
-  | Read_plain
-  (* Power reads *)
-  | Read_reserve
-  (* AArch64 reads *)
-  | Read_acquire | Read_exclusive | Read_exclusive_acquire | Read_stream
-  (* RISC-V reads *)
-  | Read_RISCV_acquire  | Read_RISCV_strong_acquire
-  | Read_RISCV_reserved | Read_RISCV_reserved_acquire
-  | Read_RISCV_reserved_strong_acquire
-  (* x86 reads *)
-  | Read_X86_locked (* the read part of a lock'd instruction (rmw) *)
-
-instance (Show read_kind)
-  let show = function
-    | Read_plain -> "Read_plain"
-    | Read_reserve -> "Read_reserve"
-    | Read_acquire -> "Read_acquire"
-    | Read_exclusive -> "Read_exclusive"
-    | Read_exclusive_acquire -> "Read_exclusive_acquire"
-    | Read_stream -> "Read_stream"
-    | Read_RISCV_acquire -> "Read_RISCV_acquire"
-    | Read_RISCV_strong_acquire -> "Read_RISCV_strong_acquire"
-    | Read_RISCV_reserved -> "Read_RISCV_reserved"
-    | Read_RISCV_reserved_acquire -> "Read_RISCV_reserved_acquire"
-    | Read_RISCV_reserved_strong_acquire -> "Read_RISCV_reserved_strong_acquire"
-    | Read_X86_locked -> "Read_X86_locked"
-  end
-end
-
-type write_kind =
-  (* common writes *)
-  | Write_plain
-  (* Power writes *)
-  | Write_conditional
-  (* AArch64 writes *)
-  | Write_release | Write_exclusive | Write_exclusive_release
-  (* RISC-V *)
-  | Write_RISCV_release     | Write_RISCV_strong_release
-  | Write_RISCV_conditional | Write_RISCV_conditional_release
-  | Write_RISCV_conditional_strong_release
-  (* x86 writes *)
-  | Write_X86_locked (* the write part of a lock'd instruction (rmw) *)
-
-instance (Show write_kind)
-  let show = function
-    | Write_plain -> "Write_plain"
-    | Write_conditional -> "Write_conditional"
-    | Write_release -> "Write_release"
-    | Write_exclusive -> "Write_exclusive"
-    | Write_exclusive_release -> "Write_exclusive_release"
-    | Write_RISCV_release -> "Write_RISCV_release"
-    | Write_RISCV_strong_release -> "Write_RISCV_strong_release"
-    | Write_RISCV_conditional -> "Write_RISCV_conditional"
-    | Write_RISCV_conditional_release -> "Write_RISCV_conditional_release"
-    | Write_RISCV_conditional_strong_release -> "Write_RISCV_conditional_strong_release"
-    | Write_X86_locked -> "Write_X86_locked"
-  end
-end
-
-type barrier_kind =
-  (* Power barriers *)
-  Barrier_Sync | Barrier_LwSync | Barrier_Eieio | Barrier_Isync
-  (* AArch64 barriers *)
-  | Barrier_DMB | Barrier_DMB_ST | Barrier_DMB_LD | Barrier_DSB
-  | Barrier_DSB_ST | Barrier_DSB_LD | Barrier_ISB
-  | Barrier_TM_COMMIT
-  (* MIPS barriers *)
-  | Barrier_MIPS_SYNC
-  (* RISC-V barriers *)
-  | Barrier_RISCV_rw_rw
-  | Barrier_RISCV_r_rw
-  | Barrier_RISCV_r_r
-  | Barrier_RISCV_rw_w
-  | Barrier_RISCV_w_w
-  | Barrier_RISCV_w_rw
-  | Barrier_RISCV_rw_r
-  | Barrier_RISCV_r_w
-  | Barrier_RISCV_w_r
-  | Barrier_RISCV_i
-  (* X86 *)
-  | Barrier_x86_MFENCE
-
-
-instance (Show barrier_kind)
-  let show = function
-    | Barrier_Sync -> "Barrier_Sync"
-    | Barrier_LwSync -> "Barrier_LwSync"
-    | Barrier_Eieio -> "Barrier_Eieio"
-    | Barrier_Isync -> "Barrier_Isync"
-    | Barrier_DMB -> "Barrier_DMB"
-    | Barrier_DMB_ST -> "Barrier_DMB_ST"
-    | Barrier_DMB_LD -> "Barrier_DMB_LD"
-    | Barrier_DSB -> "Barrier_DSB"
-    | Barrier_DSB_ST -> "Barrier_DSB_ST"
-    | Barrier_DSB_LD -> "Barrier_DSB_LD"
-    | Barrier_ISB -> "Barrier_ISB"
-    | Barrier_TM_COMMIT -> "Barrier_TM_COMMIT"
-    | Barrier_MIPS_SYNC -> "Barrier_MIPS_SYNC"
-    | Barrier_RISCV_rw_rw -> "Barrier_RISCV_rw_rw"
-    | Barrier_RISCV_r_rw  -> "Barrier_RISCV_r_rw"
-    | Barrier_RISCV_r_r   -> "Barrier_RISCV_r_r"
-    | Barrier_RISCV_rw_w  -> "Barrier_RISCV_rw_w"
-    | Barrier_RISCV_w_w   -> "Barrier_RISCV_w_w"
-    | Barrier_RISCV_w_rw  -> "Barrier_RISCV_w_rw"
-    | Barrier_RISCV_rw_r  -> "Barrier_RISCV_rw_r"
-    | Barrier_RISCV_r_w   -> "Barrier_RISCV_r_w"
-    | Barrier_RISCV_w_r   -> "Barrier_RISCV_w_r"
-    | Barrier_RISCV_i     -> "Barrier_RISCV_i"
-    | Barrier_x86_MFENCE  -> "Barrier_x86_MFENCE"
-  end
-end
-
-type trans_kind =
-  (* AArch64 *)
-  | Transaction_start | Transaction_commit | Transaction_abort
-
-instance (Show trans_kind)
-  let show = function
-  | Transaction_start  -> "Transaction_start"
-  | Transaction_commit -> "Transaction_commit"
-  | Transaction_abort  -> "Transaction_abort"
-  end
-end
-
-type instruction_kind =
-  | IK_barrier   of barrier_kind
-  | IK_mem_read  of read_kind
-  | IK_mem_write of write_kind
-  | IK_mem_rmw   of (read_kind * write_kind)
-  | IK_branch    of unit(* this includes conditional-branch (multiple nias, none of which is NIA_indirect_address),
-  indirect/computed-branch (single nia of kind NIA_indirect_address)
-  and branch/jump (single nia of kind NIA_concrete_address) *)
-  | IK_trans     of trans_kind
-  | IK_simple    of unit
-
-
-instance (Show instruction_kind)
-  let show = function
-    | IK_barrier barrier_kind -> "IK_barrier " ^ (show barrier_kind)
-    | IK_mem_read read_kind   -> "IK_mem_read " ^ (show read_kind)
-    | IK_mem_write write_kind -> "IK_mem_write " ^ (show write_kind)
-    | IK_mem_rmw (r, w)       -> "IK_mem_rmw " ^ (show r) ^ " " ^ (show w)
-    | IK_branch ()            -> "IK_branch"
-    | IK_trans trans_kind     -> "IK_trans " ^ (show trans_kind)
-    | IK_simple ()            -> "IK_simple"
-  end
-end
-
-
-let read_is_exclusive = function
-  | Read_plain -> false
-  | Read_reserve -> true
-  | Read_acquire -> false
-  | Read_exclusive -> true
-  | Read_exclusive_acquire -> true
-  | Read_stream -> false
-  | Read_RISCV_acquire -> false
-  | Read_RISCV_strong_acquire -> false
-  | Read_RISCV_reserved -> true
-  | Read_RISCV_reserved_acquire -> true
-  | Read_RISCV_reserved_strong_acquire -> true
-  | Read_X86_locked -> true
-end
-
-
-
-instance (EnumerationType read_kind)
-  let toNat = function
-    | Read_plain -> 0
-    | Read_reserve -> 1
-    | Read_acquire -> 2
-    | Read_exclusive -> 3
-    | Read_exclusive_acquire -> 4
-    | Read_stream -> 5
-    | Read_RISCV_acquire -> 6
-    | Read_RISCV_strong_acquire -> 7
-    | Read_RISCV_reserved -> 8
-    | Read_RISCV_reserved_acquire -> 9
-    | Read_RISCV_reserved_strong_acquire -> 10
-    | Read_X86_locked -> 11
-  end
-end
-
-instance (EnumerationType write_kind)
-  let toNat = function
-    | Write_plain -> 0
-    | Write_conditional -> 1
-    | Write_release -> 2
-    | Write_exclusive -> 3
-    | Write_exclusive_release -> 4
-    | Write_RISCV_release -> 5
-    | Write_RISCV_strong_release -> 6
-    | Write_RISCV_conditional -> 7
-    | Write_RISCV_conditional_release -> 8
-    | Write_RISCV_conditional_strong_release -> 9
-    | Write_X86_locked -> 10
-  end
-end
-
-instance (EnumerationType barrier_kind)
-  let toNat = function
-    | Barrier_Sync -> 0
-    | Barrier_LwSync -> 1
-    | Barrier_Eieio ->2
-    | Barrier_Isync -> 3
-    | Barrier_DMB -> 4
-    | Barrier_DMB_ST -> 5
-    | Barrier_DMB_LD -> 6
-    | Barrier_DSB -> 7
-    | Barrier_DSB_ST -> 8
-    | Barrier_DSB_LD -> 9
-    | Barrier_ISB -> 10
-    | Barrier_TM_COMMIT -> 11
-    | Barrier_MIPS_SYNC -> 12
-    | Barrier_RISCV_rw_rw -> 13
-    | Barrier_RISCV_r_rw -> 14
-    | Barrier_RISCV_r_r -> 15
-    | Barrier_RISCV_rw_w -> 16
-    | Barrier_RISCV_w_w -> 17
-    | Barrier_RISCV_w_rw -> 18
-    | Barrier_RISCV_rw_r -> 19
-    | Barrier_RISCV_r_w -> 20
-    | Barrier_RISCV_w_r -> 21
-    | Barrier_RISCV_i -> 22
-    | Barrier_x86_MFENCE -> 23
-  end
-end
diff --git a/src/gen_lib/0.11/sail2_operators.lem b/src/gen_lib/0.11/sail2_operators.lem
deleted file mode 100644
index 43a9812e..00000000
--- a/src/gen_lib/0.11/sail2_operators.lem
+++ /dev/null
@@ -1,207 +0,0 @@
-open import Pervasives_extra
-open import Machine_word
-open import Sail2_values
-
-(*** Bit vector operations *)
-
-val concat_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b => 'a -> 'b -> list bitU
-let concat_bv l r = (bits_of l ++ bits_of r)
-
-val cons_bv : forall 'a. Bitvector 'a => bitU -> 'a -> list bitU
-let cons_bv b v = b :: bits_of v
-
-val cast_unit_bv : bitU -> list bitU
-let cast_unit_bv b = [b]
-
-val bv_of_bit : integer -> bitU -> list bitU
-let bv_of_bit len b = extz_bits len [b]
-
-let most_significant v = match bits_of v with
-  | b :: _ -> b
-  | _ -> B0 (* Treat empty bitvector as all zeros *)
-  end
-
-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 arith_op_bv_int : forall 'a 'b. Bitvector 'a =>
-  (integer -> integer -> integer) -> bool -> 'a -> integer -> 'a
-let arith_op_bv_int op sign l r =
-  let r' = of_int (length l) r in
-  arith_op_bv op sign l r'
-
-val arith_op_int_bv : forall 'a 'b. Bitvector 'a =>
-  (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a
-let arith_op_int_bv op sign l r =
-  let l' = of_int (length r) l in
-  arith_op_bv op sign l' r
-
-let arith_op_bv_bool op sign l r = arith_op_bv_int op sign l (if r then 1 else 0)
-let arith_op_bv_bit op sign l r = Maybe.map (arith_op_bv_bool op sign l) (bool_of_bitU r)
-
-(* TODO (or just omit and define it per spec if needed)
-val arith_op_overflow_bv : forall 'a. Bitvector 'a =>
-  (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> (list bitU * bitU * bitU)
-let arith_op_overflow_bv op sign size l r =
-  let len = length l in
-  let act_size = len * size in
-  match (int_of_bv sign l, int_of_bv sign r, int_of_bv false l, int_of_bv false r) with
-    | (Just l_sign, Just r_sign, Just l_unsign, Just r_unsign) ->
-       let n = op l_sign r_sign in
-       let n_unsign = op l_unsign r_unsign 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
-       (correct_size,overflow,c_out)
-    | (_, _, _, _) ->
-       (repeat [BU] act_size, BU, BU)
-  end
-
-let add_overflow_bv = arith_op_overflow_bv integerAdd false 1
-let adds_overflow_bv = arith_op_overflow_bv integerAdd true 1
-let sub_overflow_bv = arith_op_overflow_bv integerMinus false 1
-let subs_overflow_bv = arith_op_overflow_bv integerMinus true 1
-let mult_overflow_bv = arith_op_overflow_bv integerMult false 2
-let mults_overflow_bv = arith_op_overflow_bv integerMult true 2
-
-val arith_op_overflow_bv_bit : forall 'a. Bitvector 'a =>
-  (integer -> integer -> integer) -> bool -> integer -> 'a -> bitU -> (list bitU * bitU * bitU)
-let arith_op_overflow_bv_bit op sign size l r_bit =
-  let act_size = length l * size in
-  match (int_of_bv sign l, int_of_bv false l, r_bit = BU) with
-    | (Just l', Just l_u, false) ->
-       let (n, nu, changed) = match r_bit with
-         | B1 -> (op l' 1, op l_u 1, true)
-         | B0 -> (l', l_u, false)
-         | BU -> (* unreachable due to check above *)
-            failwith "arith_op_overflow_bv_bit applied to undefined bit"
-         end 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
-         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, overflow, most_significant one_larger)
-    | (_, _, _) ->
-       (repeat [BU] act_size, BU, BU)
-  end
-
-let add_overflow_bv_bit = arith_op_overflow_bv_bit integerAdd false 1
-let adds_overflow_bv_bit = arith_op_overflow_bv_bit integerAdd true 1
-let sub_overflow_bv_bit = arith_op_overflow_bv_bit integerMinus false 1
-let subs_overflow_bv_bit = arith_op_overflow_bv_bit integerMinus true 1*)
-
-type shift = LL_shift | RR_shift | RR_shift_arith | LL_rot | RR_rot
-
-let invert_shift = function
-  | LL_shift -> RR_shift
-  | RR_shift -> LL_shift
-  | RR_shift_arith -> LL_shift
-  | LL_rot -> RR_rot
-  | RR_rot -> LL_rot
-end
-
-val shift_op_bv : forall 'a. Bitvector 'a => shift -> 'a -> integer -> list bitU
-let shift_op_bv op v n =
-  let v = bits_of v in
-  if n = 0 then v else
-  let (op, n) = if n > 0 then (op, n) else (invert_shift op, ~n) in
-  match op with
-  | LL_shift ->
-     subrange_list true v n (length v - 1) ++ repeat [B0] n
-  | RR_shift ->
-     repeat [B0] n ++ subrange_list true v 0 (length v - n - 1)
-  | RR_shift_arith ->
-     repeat [most_significant v] n ++ subrange_list true v 0 (length v - n - 1)
-  | LL_rot ->
-     subrange_list true v n (length v - 1) ++ subrange_list true v 0 (n - 1)
-  | RR_rot ->
-     subrange_list false v 0 (n - 1) ++ subrange_list false v n (length v - 1)
-  end
-
-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 (nat_of_int n)
-let shiftr_mword w n = Machine_word.shiftRight w (nat_of_int n)
-let arith_shiftr_mword w n = Machine_word.arithShiftRight w (nat_of_int n)
-let rotl_mword w n = Machine_word.rotateLeft (nat_of_int n) w
-let rotr_mword w n = Machine_word.rotateRight (nat_of_int n) w
-
-let rec arith_op_no0 (op : integer -> integer -> integer) l r =
-  if r = 0
-  then Nothing
-  else Just (op l r)
-
-val arith_op_bv_no0 : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
-  (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> maybe 'b
-let arith_op_bv_no0 op sign size l r =
-  Maybe.bind (int_of_bv sign l) (fun l' ->
-  Maybe.bind (int_of_bv sign r) (fun r' ->
-  if r' = 0 then Nothing else Just (of_int (length l * size) (op l' r'))))
-
-let mod_bv = arith_op_bv_no0 tmod_int false 1
-let quot_bv = arith_op_bv_no0 tdiv_int false 1
-let quots_bv = arith_op_bv_no0 tdiv_int true 1
-
-let mod_mword = Machine_word.modulo
-let quot_mword = Machine_word.unsignedDivide
-let quots_mword = Machine_word.signedDivide
-
-let arith_op_bv_int_no0 op sign size l r =
-  arith_op_bv_no0 op sign size l (of_int (length l) r)
-
-let quot_bv_int = arith_op_bv_int_no0 tdiv_int false 1
-let mod_bv_int = arith_op_bv_int_no0 tmod_int false 1
-
-let mod_mword_int l r = Machine_word.modulo l (wordFromInteger r)
-let quot_mword_int l r = Machine_word.unsignedDivide l (wordFromInteger r)
-let quots_mword_int l r = Machine_word.signedDivide l (wordFromInteger r)
-
-let replicate_bits_bv v count = repeat (bits_of v) count
-let duplicate_bit_bv bit len = replicate_bits_bv [bit] len
-
-val eq_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool
-let eq_bv l r = (bits_of l = bits_of r)
-
-let inline eq_mword l r = (l = r)
-
-val neq_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool
-let neq_bv l r = not (eq_bv l r)
-
-let inline neq_mword l r = (l <> r)
-
-val get_slice_int_bv : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a
-let get_slice_int_bv len n lo =
-  let hi = lo + len - 1 in
-  let bs = bools_of_int (hi + 1) n in
-  of_bools (subrange_list false bs hi lo)
-
-val set_slice_int_bv : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a -> integer
-let set_slice_int_bv len n lo v =
-  let hi = lo + len - 1 in
-  let bs = bits_of_int (hi + 1) n in
-  maybe_failwith (signed_of_bits (update_subrange_list false bs hi lo (bits_of v)))
diff --git a/src/gen_lib/0.11/sail2_operators_bitlists.lem b/src/gen_lib/0.11/sail2_operators_bitlists.lem
deleted file mode 100644
index c9892e4c..00000000
--- a/src/gen_lib/0.11/sail2_operators_bitlists.lem
+++ /dev/null
@@ -1,308 +0,0 @@
-open import Pervasives_extra
-open import Machine_word
-open import Sail2_values
-open import Sail2_operators
-open import Sail2_prompt_monad
-open import Sail2_prompt
-
-(* Specialisation of operators to bit lists *)
-
-val uint_maybe : list bitU -> maybe integer
-let uint_maybe v = unsigned v
-let uint_fail v = maybe_fail "uint" (unsigned v)
-let uint_nondet v =
-  bools_of_bits_nondet v >>= (fun bs ->
-  return (int_of_bools false bs))
-let uint v = maybe_failwith (uint_maybe v)
-
-val sint_maybe : list bitU -> maybe integer
-let sint_maybe v = signed v
-let sint_fail v = maybe_fail "sint" (signed v)
-let sint_nondet v =
-  bools_of_bits_nondet v >>= (fun bs ->
-  return (int_of_bools true bs))
-let sint v = maybe_failwith (sint_maybe v)
-
-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 zero_extend : list bitU -> integer -> list bitU
-let zero_extend bits len = extz_bits len bits
-
-val sign_extend : list bitU -> integer -> list bitU
-let sign_extend bits len = exts_bits len bits
-
-val zeros : integer -> list bitU
-let zeros len = repeat [B0] len
-
-val vector_truncate : list bitU -> integer -> list bitU
-let vector_truncate bs len = extz_bv len bs
-
-val vector_truncateLSB : list bitU -> integer -> list bitU
-let vector_truncateLSB bs len = take_list len bs
-
-val vec_of_bits_maybe    : list bitU -> maybe (list bitU)
-val vec_of_bits_fail     : forall 'rv 'e. list bitU -> monad 'rv (list bitU) 'e
-val vec_of_bits_nondet   : forall 'rv 'e. list bitU -> monad 'rv (list bitU) 'e
-val vec_of_bits_failwith : list bitU -> list bitU
-val vec_of_bits          : list bitU -> list bitU
-let inline vec_of_bits bits = bits
-let inline vec_of_bits_maybe bits = Just bits
-let inline vec_of_bits_fail bits = return bits
-let inline vec_of_bits_nondet bits = return bits
-let inline vec_of_bits_failwith bits = bits
-
-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
-let update_vec_inc_maybe v i b = Just (update_vec_inc v i b)
-let update_vec_inc_fail v i b = return (update_vec_inc v i b)
-let update_vec_inc_nondet v i b = return (update_vec_inc v i b)
-
-val update_vec_dec : list bitU -> integer -> bitU -> list bitU
-let update_vec_dec = update_bv_dec
-let update_vec_dec_maybe v i b = Just (update_vec_dec v i b)
-let update_vec_dec_fail v i b = return (update_vec_dec v i b)
-let update_vec_dec_nondet v i b = return (update_vec_dec v i b)
-
-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 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
-let cons_vec_maybe b v = Just (cons_vec b v)
-let cons_vec_fail b v = return (cons_vec b v)
-let cons_vec_nondet b v = return (cons_vec b v)
-
-val cast_unit_vec : bitU -> list bitU
-let cast_unit_vec = cast_unit_bv
-let cast_unit_vec_maybe b = Just (cast_unit_vec b)
-let cast_unit_vec_fail b = return (cast_unit_vec b)
-let cast_unit_vec_nondet b = return (cast_unit_vec b)
-
-val vec_of_bit : integer -> bitU -> list bitU
-let vec_of_bit = bv_of_bit
-let vec_of_bit_maybe len b = Just (vec_of_bit len b)
-let vec_of_bit_fail len b = return (vec_of_bit len b)
-let vec_of_bit_nondet len b = return (vec_of_bit len b)
-
-val msb : list bitU -> bitU
-let msb = most_significant
-
-val int_of_vec_maybe : bool -> list bitU -> maybe integer
-let int_of_vec_maybe = int_of_bv
-let int_of_vec_fail sign v = maybe_fail "int_of_vec" (int_of_vec_maybe sign v)
-let int_of_vec_nondet sign v = bools_of_bits_nondet v >>= (fun v -> return (int_of_bools sign v))
-let int_of_vec sign v = maybe_failwith (int_of_vec_maybe sign v)
-
-val string_of_bits : list bitU -> string
-let string_of_bits = string_of_bv
-
-val decimal_string_of_bits : list bitU -> string
-let decimal_string_of_bits = decimal_string_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 = binop_list and_bit
-let or_vec  = binop_list or_bit
-let xor_vec = binop_list xor_bit
-let not_vec = List.map not_bit
-
-val arith_op_double_bl : forall 'a 'b. Bitvector 'a =>
-  (integer -> integer -> integer) -> bool -> 'a -> 'a -> list bitU
-let arith_op_double_bl op sign l r =
-  let len = 2 * length l in
-  let l' = if sign then exts_bv len l else extz_bv len l in
-  let r' = if sign then exts_bv len r else extz_bv len r in
-  arith_op_bv 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 sub_vec_int       : list bitU -> integer -> list bitU
-val mult_vec_int      : list bitU -> integer -> list bitU
-let add_vec_int   l r = arith_op_bv_int integerAdd false l r
-let sub_vec_int   l r = arith_op_bv_int integerMinus false l r
-let mult_vec_int  l r = arith_op_double_bl integerMult false l (of_int (length l) r)
-
-val add_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
-let add_int_vec   l r = arith_op_int_bv integerAdd false l r
-let sub_int_vec   l r = arith_op_int_bv integerMinus false l r
-let mult_int_vec  l r = arith_op_double_bl integerMult false (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
-let add_vec_bit_fail   l r = maybe_fail "add_vec_bit" (add_vec_bit_maybe l r)
-let add_vec_bit_nondet l r = bool_of_bitU_nondet r >>= (fun r -> return (add_vec_bool l r))
-let add_vec_bit        l r = fromMaybe (repeat [BU] (length l)) (add_vec_bit_maybe l r)
-
-let adds_vec_bool       l r = arith_op_bv_bool integerAdd true l r
-let adds_vec_bit_maybe  l r = arith_op_bv_bit integerAdd true l r
-let adds_vec_bit_fail   l r = maybe_fail "adds_vec_bit" (adds_vec_bit_maybe l r)
-let adds_vec_bit_nondet l r = bool_of_bitU_nondet r >>= (fun r -> return (adds_vec_bool l r))
-let adds_vec_bit        l r = fromMaybe (repeat [BU] (length l)) (adds_vec_bit_maybe l r)
-
-let sub_vec_bool        l r = arith_op_bv_bool integerMinus false l r
-let sub_vec_bit_maybe   l r = arith_op_bv_bit integerMinus false l r
-let sub_vec_bit_fail    l r = maybe_fail "sub_vec_bit" (sub_vec_bit_maybe l r)
-let sub_vec_bit_nondet  l r = bool_of_bitU_nondet 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_nondet l r = bool_of_bitU_nondet 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)
-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 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_nondet : 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_nondet l r = of_bits_nondet (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_nondet : 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_nondet l r = of_bits_nondet (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_nondet : 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_nondet l r = of_bits_nondet (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_nondet : 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_nondet l r = of_bits_nondet (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_nondet : 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_nondet l r = of_bits_nondet (quot_vec_int l r)
-
-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
-let duplicate_maybe b n = Just (duplicate b n)
-let duplicate_fail b n = return (duplicate b n)
-let duplicate_nondet b n =
-  bool_of_bitU_nondet b >>= (fun b ->
-  return (duplicate (bitU_of_bool b) n))
-
-val reverse_endianness : list bitU -> list bitU
-let reverse_endianness v = reverse_endianness_list v
-
-val get_slice_int : integer -> integer -> integer -> list bitU
-let get_slice_int = get_slice_int_bv
-
-val set_slice_int : integer -> integer -> integer -> list bitU -> integer
-let set_slice_int = set_slice_int_bv
-
-val slice : list bitU -> integer -> integer -> list bitU
-let slice v lo len =
-  subrange_vec_dec v (lo + len - 1) lo
-
-val set_slice : integer -> integer -> list bitU -> integer -> list bitU -> list bitU
-let set_slice (out_len:ii) (slice_len:ii) out (n:ii) v =
-  update_subrange_vec_dec out (n + slice_len - 1) n v
-
-val eq_vec    : list bitU -> list bitU -> bool
-val neq_vec   : list bitU -> list bitU -> bool
-let eq_vec    = eq_bv
-let neq_vec   = neq_bv
-
-let inline count_leading_zeros v = count_leading_zero_bits v
diff --git a/src/gen_lib/0.11/sail2_operators_mwords.lem b/src/gen_lib/0.11/sail2_operators_mwords.lem
deleted file mode 100644
index c8524e16..00000000
--- a/src/gen_lib/0.11/sail2_operators_mwords.lem
+++ /dev/null
@@ -1,334 +0,0 @@
-open import Pervasives_extra
-open import Machine_word
-open import Sail2_values
-open import Sail2_operators
-open import Sail2_prompt_monad
-open import Sail2_prompt
-
-(* Specialisation of operators to machine words *)
-
-let inline uint v = unsignedIntegerFromWord v
-let uint_maybe v = Just (uint v)
-let uint_fail v = return (uint v)
-let uint_nondet v = return (uint v)
-
-let inline sint v = signedIntegerFromWord v
-let sint_maybe v = Just (sint v)
-let sint_fail v = return (sint v)
-let sint_nondet v = return (sint v)
-
-val vec_of_bits_maybe    : forall 'a. Size 'a => list bitU -> maybe (mword 'a)
-val vec_of_bits_fail     : forall 'rv 'a 'e. Size 'a => list bitU -> monad 'rv (mword 'a) 'e
-val vec_of_bits_nondet   : forall 'rv 'a 'e. Size 'a => list bitU -> monad 'rv (mword 'a) 'e
-val vec_of_bits_failwith : forall 'a. Size 'a => list bitU -> mword 'a
-val vec_of_bits          : forall 'a. Size 'a => list bitU -> mword 'a
-let vec_of_bits_maybe bits = of_bits bits
-let vec_of_bits_fail bits = of_bits_fail bits
-let vec_of_bits_nondet bits = of_bits_nondet bits
-let vec_of_bits_failwith bits = of_bits_failwith bits
-let vec_of_bits bits = of_bits_failwith bits
-
-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
-
-let update_vec_dec_maybe w i b = update_mword_dec w i b
-let update_vec_dec_fail w i b =
-  bool_of_bitU_fail b >>= (fun b ->
-  return (update_mword_bool_dec w i b))
-let update_vec_dec_nondet w i b =
-  bool_of_bitU_nondet b >>= (fun b ->
-  return (update_mword_bool_dec w i b))
-let update_vec_dec w i b = maybe_failwith (update_vec_dec_maybe w i b)
-
-let update_vec_inc_maybe w i b = update_mword_inc w i b
-let update_vec_inc_fail w i b =
-  bool_of_bitU_fail b >>= (fun b ->
-  return (update_mword_bool_inc w i b))
-let update_vec_inc_nondet w i b =
-  bool_of_bitU_nondet b >>= (fun b ->
-  return (update_mword_bool_inc w i b))
-let update_vec_inc w i b = maybe_failwith (update_vec_inc_maybe w i b)
-
-val subrange_vec_dec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b
-let subrange_vec_dec w i j = Machine_word.word_extract (nat_of_int j) (nat_of_int i) w
-
-val subrange_vec_inc : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b
-let subrange_vec_inc w i j = subrange_vec_dec w (length w - 1 - i) (length w - 1 - j)
-
-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 w i j w' = Machine_word.word_update w (nat_of_int j) (nat_of_int i) w'
-
-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 w i j w' = update_subrange_vec_dec w (length w - 1 - i) (length w - 1 - j) w'
-
-val extz_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b
-let extz_vec _ w = Machine_word.zeroExtend w
-
-val exts_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b
-let exts_vec _ w = Machine_word.signExtend w
-
-val zero_extend : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
-let zero_extend w _ = Machine_word.zeroExtend w
-
-val sign_extend : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
-let sign_extend w _ = Machine_word.signExtend w
-
-val zeros : forall 'a. Size 'a => integer -> mword 'a
-let zeros _ = Machine_word.wordFromNatural 0
-
-val vector_truncate : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
-let vector_truncate w _ = Machine_word.zeroExtend w
-
-val vector_truncateLSB : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
-let vector_truncateLSB w len =
-  let len = nat_of_int len in
-  let lo = Machine_word.word_length w - len in
-  let hi = lo + len - 1 in
-  Machine_word.word_extract lo hi w
-
-val concat_vec : forall 'a 'b 'c. Size 'a, Size 'b, Size 'c => mword 'a -> mword 'b -> mword 'c
-let concat_vec = Machine_word.word_concat
-
-val cons_vec_bool : forall 'a 'b 'c. Size 'a, Size 'b => bool -> mword 'a -> mword 'b
-let cons_vec_bool b w = wordFromBitlist (b :: bitlistFromWord w)
-let cons_vec_maybe b w = Maybe.map (fun b -> cons_vec_bool b w) (bool_of_bitU b)
-let cons_vec_fail b w = bool_of_bitU_fail b >>= (fun b -> return (cons_vec_bool b w))
-let cons_vec_nondet b w = bool_of_bitU_nondet b >>= (fun b -> return (cons_vec_bool b w))
-let cons_vec b w = maybe_failwith (cons_vec_maybe b w)
-
-val vec_of_bool : forall 'a. Size 'a => integer -> bool -> mword 'a
-let vec_of_bool _ b = wordFromBitlist [b]
-let vec_of_bit_maybe len b = Maybe.map (vec_of_bool len) (bool_of_bitU b)
-let vec_of_bit_fail len b = bool_of_bitU_fail b >>= (fun b -> return (vec_of_bool len b))
-let vec_of_bit_nondet len b = bool_of_bitU_nondet b >>= (fun b -> return (vec_of_bool len b))
-let vec_of_bit len b = maybe_failwith (vec_of_bit_maybe len b)
-
-val cast_bool_vec : bool -> mword ty1
-let cast_bool_vec b = vec_of_bool 1 b
-let cast_unit_vec_maybe b = vec_of_bit_maybe 1 b
-let cast_unit_vec_fail b = bool_of_bitU_fail b >>= (fun b -> return (cast_bool_vec b))
-let cast_unit_vec_nondet b = bool_of_bitU_nondet b >>= (fun b -> return (cast_bool_vec b))
-let cast_unit_vec b = maybe_failwith (cast_unit_vec_maybe b)
-
-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 sign w =
-  if sign
-  then signedIntegerFromWord w
-  else unsignedIntegerFromWord w
-let int_of_vec_maybe sign w = Just (int_of_vec sign w)
-let int_of_vec_fail sign w = return (int_of_vec sign w)
-
-val string_of_bits : forall 'a. Size 'a => mword 'a -> string
-let string_of_bits = string_of_bv
-
-val decimal_string_of_bits : forall 'a. Size 'a => mword 'a -> string
-let decimal_string_of_bits = decimal_string_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 = Machine_word.lAnd
-let or_vec  = Machine_word.lOr
-let xor_vec = Machine_word.lXor
-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 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 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
-let add_vec_int   l r = arith_op_bv_int integerAdd   false l r
-let sub_vec_int   l r = arith_op_bv_int integerMinus false l r
-let mult_vec_int  l r = arith_op_bv_int integerMult  false (zeroExtend l : mword 'b) r
-
-val add_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
-let add_int_vec   l r = arith_op_int_bv integerAdd   false l r
-let sub_int_vec   l r = arith_op_int_bv integerMinus false l r
-let mult_int_vec  l r = arith_op_int_bv integerMult  false l (zeroExtend 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)
-let add_vec_bit_fail    l r = bool_of_bitU_fail r >>= (fun r -> return (add_vec_bool l r))
-let add_vec_bit_nondet  l r = bool_of_bitU_nondet r >>= (fun r -> return (add_vec_bool l r))
-let add_vec_bit         l r = maybe_failwith (add_vec_bit_maybe  l r)
-
-let adds_vec_bool       l r = arith_op_bv_bool integerAdd true  l r
-let adds_vec_bit_maybe  l r = Maybe.map (adds_vec_bool l) (bool_of_bitU r)
-let adds_vec_bit_fail   l r = bool_of_bitU_fail r >>= (fun r -> return (adds_vec_bool l r))
-let adds_vec_bit_nondet l r = bool_of_bitU_nondet 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 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_nondet  l r = bool_of_bitU_nondet 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_nondet l r = bool_of_bitU_nondet 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) =
-  Maybe.map (fun w -> (w, overflow, carry)) (of_bits bits)
-
-val add_overflow_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a * bitU * bitU)
-val adds_overflow_vec  : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a * bitU * bitU)
-val sub_overflow_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a * bitU * bitU)
-val subs_overflow_vec  : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a * bitU * bitU)
-val mult_overflow_vec  : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a * bitU * bitU)
-val mults_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a * bitU * bitU)
-let add_overflow_vec   l r = maybe_mword_of_bits_overflow (add_overflow_bv l r)
-let adds_overflow_vec  l r = maybe_mword_of_bits_overflow (adds_overflow_bv l r)
-let sub_overflow_vec   l r = maybe_mword_of_bits_overflow (sub_overflow_bv l r)
-let subs_overflow_vec  l r = maybe_mword_of_bits_overflow (subs_overflow_bv l r)
-let mult_overflow_vec  l r = maybe_mword_of_bits_overflow (mult_overflow_bv l r)
-let mults_overflow_vec l r = maybe_mword_of_bits_overflow (mults_overflow_bv l r)
-
-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_mword
-let shiftr       = shiftr_mword
-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 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_nondet : 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_nondet l r =
-  match (mod_bv l r) with
-    | Just w -> return w
-    | Nothing -> mword_nondet ()
-  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_nondet : 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_nondet l r =
-  match (quot_bv l r) with
-    | Just w -> return w
-    | Nothing -> mword_nondet ()
-  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_nondet : 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_nondet l r =
-  match (quots_bv l r) with
-    | Just w -> return w
-    | Nothing -> mword_nondet ()
-  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_nondet : 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_nondet l r =
-  match (mod_bv_int l r) with
-    | Just w -> return w
-    | Nothing -> mword_nondet ()
-  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_nondet : 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_nondet l r =
-  match (quot_bv_int l r) with
-    | Just w -> return w
-    | Nothing -> mword_nondet ()
-  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)
-
-val duplicate_bool : forall 'a. Size 'a => bool -> integer -> mword 'a
-let duplicate_bool   b n = wordFromBitlist (repeat [b] n)
-let duplicate_maybe  b n = Maybe.map (fun b -> duplicate_bool b n) (bool_of_bitU b)
-let duplicate_fail   b n = bool_of_bitU_fail b >>= (fun b -> return (duplicate_bool b n))
-let duplicate_nondet b n = bool_of_bitU_nondet b >>= (fun b -> return (duplicate_bool b n))
-let duplicate        b n = maybe_failwith (duplicate_maybe b n)
-
-val reverse_endianness : forall 'a. Size 'a => mword 'a -> mword 'a
-let reverse_endianness v = wordFromBitlist (reverse_endianness_list (bitlistFromWord v))
-
-val get_slice_int : forall 'a. Size 'a => integer -> integer -> integer -> mword 'a
-let get_slice_int = get_slice_int_bv
-
-val set_slice_int : forall 'a. Size 'a => integer -> integer -> integer -> mword 'a -> integer
-let set_slice_int = set_slice_int_bv
-
-val slice : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b
-let slice v lo len =
-  subrange_vec_dec v (lo + len - 1) lo
-
-val set_slice : forall 'a 'b. Size 'a, Size 'b => integer -> integer -> mword 'a -> integer -> mword 'b -> mword 'a
-let set_slice (out_len:ii) (slice_len:ii) out (n:ii) v =
-  update_subrange_vec_dec out (n + slice_len - 1) n v
-
-val eq_vec    : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-val neq_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-let inline eq_vec    = eq_mword
-let inline neq_vec   = neq_mword
-
-val count_leading_zeros : forall 'a. Size 'a => mword 'a -> integer
-let count_leading_zeros v = count_leading_zeros_bv v
diff --git a/src/gen_lib/0.11/sail2_prompt.lem b/src/gen_lib/0.11/sail2_prompt.lem
deleted file mode 100644
index 3cde7ade..00000000
--- a/src/gen_lib/0.11/sail2_prompt.lem
+++ /dev/null
@@ -1,139 +0,0 @@
-open import Pervasives_extra
-(*open import Sail_impl_base*)
-open import Sail2_values
-open import Sail2_prompt_monad
-open import {isabelle} `Sail2_prompt_monad_lemmas`
-
-val (>>=) : forall 'rv 'a 'b 'e. monad 'rv 'a 'e -> ('a -> monad 'rv 'b 'e) -> monad 'rv 'b 'e
-declare isabelle target_rep function (>>=) = infix `\<bind>`
-let inline ~{isabelle} (>>=) = bind
-
-val (>>) : forall 'rv 'b 'e. monad 'rv unit 'e -> monad 'rv 'b 'e -> monad 'rv 'b 'e
-declare isabelle target_rep function (>>) = infix `\<then>`
-let inline ~{isabelle} (>>) m n = m >>= fun (_ : unit) -> n
-
-val iter_aux : forall 'rv 'a 'e. integer -> (integer -> 'a -> monad 'rv unit 'e) -> list 'a -> monad 'rv unit 'e
-let rec iter_aux i f xs = match xs with
-  | x :: xs -> f i x >> iter_aux (i + 1) f xs
-  | [] -> return ()
-  end
-
-declare {isabelle} termination_argument iter_aux = automatic
-
-val iteri : forall 'rv 'a 'e. (integer -> 'a -> monad 'rv unit 'e) -> list 'a -> monad 'rv unit 'e
-let iteri f xs = iter_aux 0 f xs
-
-val iter : forall 'rv 'a 'e. ('a -> monad 'rv unit 'e) -> list 'a -> monad 'rv unit 'e
-let iter f xs = iteri (fun _ x -> f x) xs
-
-val foreachM : forall 'a 'rv 'vars 'e.
-  list 'a -> 'vars -> ('a -> 'vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
-let rec foreachM l vars body =
-match l with
-| [] -> return vars
-| (x :: xs) ->
-  body x vars >>= fun vars ->
-  foreachM xs vars body
-end
-
-declare {isabelle} termination_argument foreachM = automatic
-
-val genlistM : forall 'a 'rv 'e. (nat -> monad 'rv 'a 'e) -> nat -> monad 'rv (list 'a) 'e
-let genlistM f n =
-  let indices = genlist (fun n -> n) n in
-  foreachM indices [] (fun n xs -> (f n >>= (fun x -> return (xs ++ [x]))))
-
-val and_boolM : forall 'rv 'e. monad 'rv bool 'e -> monad 'rv bool 'e -> monad 'rv bool 'e
-let and_boolM l r = l >>= (fun l -> if l then r else return false)
-
-val or_boolM : forall 'rv 'e. monad 'rv bool 'e -> monad 'rv bool 'e -> monad 'rv bool 'e
-let or_boolM l r = l >>= (fun l -> if l then return true else r)
-
-val bool_of_bitU_fail : forall 'rv 'e. bitU -> monad 'rv bool 'e
-let bool_of_bitU_fail = function
-  | B0 -> return false
-  | B1 -> return true
-  | BU -> Fail "bool_of_bitU"
-end
-
-val bool_of_bitU_nondet : forall 'rv 'e. bitU -> monad 'rv bool 'e
-let bool_of_bitU_nondet = function
-  | B0 -> return false
-  | B1 -> return true
-  | BU -> choose_bool "bool_of_bitU"
-end
-
-val bools_of_bits_nondet : forall 'rv 'e. list bitU -> monad 'rv (list bool) 'e
-let bools_of_bits_nondet bits =
-  foreachM bits []
-    (fun b bools ->
-      bool_of_bitU_nondet b >>= (fun b ->
-      return (bools ++ [b])))
-
-val of_bits_nondet : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monad 'rv 'a 'e
-let of_bits_nondet bits =
-  bools_of_bits_nondet bits >>= (fun bs ->
-  return (of_bools bs))
-
-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_nondet : forall 'rv 'a 'e. Size 'a => unit -> monad 'rv (mword 'a) 'e
-let mword_nondet () =
-  bools_of_bits_nondet (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 =
-  cond vars >>= fun cond_val ->
-  if cond_val then
-    body vars >>= fun vars -> whileM vars cond body
-  else return vars
-
-val untilM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
-                ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
-let rec untilM vars cond body =
-  body vars >>= fun vars ->
-  cond vars >>= fun cond_val ->
-  if cond_val then return vars else untilM vars cond body
-
-val choose_bools : forall 'rv 'e. string -> nat -> monad 'rv (list bool) 'e
-let choose_bools descr n = genlistM (fun _ -> choose_bool descr) n
-
-val choose : forall 'rv 'a 'e. string -> list 'a -> monad 'rv 'a 'e
-let choose descr xs =
-  (* Use sufficiently many nondeterministically chosen bits and convert into an
-     index into the list *)
-  choose_bools descr (List.length xs) >>= fun bs ->
-  let idx = (natFromNatural (nat_of_bools bs)) mod List.length xs in
-  match index xs idx with
-    | Just x -> return x
-    | Nothing -> Fail ("choose " ^ descr)
-  end
-
-declare {isabelle} rename function choose = chooseM
-
-val internal_pick : forall 'rv 'a 'e. list 'a -> monad 'rv 'a 'e
-let internal_pick xs = choose "internal_pick" xs
-
-(*let write_two_regs r1 r2 vec =
-  let is_inc =
-    let is_inc_r1 = is_inc_of_reg r1 in
-    let is_inc_r2 = is_inc_of_reg r2 in
-    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
-  write_reg r1 r1_v >> write_reg r2 r2_v*)
diff --git a/src/gen_lib/0.11/sail2_prompt_monad.lem b/src/gen_lib/0.11/sail2_prompt_monad.lem
deleted file mode 100644
index 28c0a27e..00000000
--- a/src/gen_lib/0.11/sail2_prompt_monad.lem
+++ /dev/null
@@ -1,336 +0,0 @@
-open import Pervasives_extra
-(*open import Sail_impl_base*)
-open import Sail2_instr_kinds
-open import Sail2_values
-
-type register_name = string
-type address = list bitU
-
-type monad 'regval 'a 'e =
-  | Done of 'a
-  (* Read a number of bytes from memory, returned in little endian order,
-     with or without a tag.  The first nat specifies the address, the second
-     the number of bytes. *)
-  | Read_mem of read_kind * nat * nat * (list memory_byte -> monad 'regval 'a 'e)
-  | Read_memt of read_kind * nat * nat * ((list memory_byte * bitU) -> monad 'regval 'a 'e)
-  (* Tell the system a write is imminent, at the given address and with the
-     given size. *)
-  | Write_ea of write_kind * nat * nat * monad 'regval 'a 'e
-  (* Request the result of store-exclusive *)
-  | Excl_res of (bool -> monad 'regval 'a 'e)
-  (* Request to write a memory value of the given size at the given address,
-     with or without a tag. *)
-  | Write_mem of write_kind * nat * nat * list memory_byte * (bool -> monad 'regval 'a 'e)
-  | Write_memt of write_kind * nat * nat * list memory_byte * bitU * (bool -> monad 'regval 'a 'e)
-  (* Tell the system to dynamically recalculate dependency footprint *)
-  | Footprint of monad 'regval 'a 'e
-  (* Request a memory barrier *)
-  | Barrier of barrier_kind * monad 'regval 'a 'e
-  (* Request to read register, will track dependency when mode.track_values *)
-  | Read_reg of register_name * ('regval -> monad 'regval 'a 'e)
-  (* Request to write register *)
-  | Write_reg of register_name * 'regval * monad 'regval 'a 'e
-  (* Request to choose a Boolean, e.g. to resolve an undefined bit. The string
-     argument may be used to provide information to the system about what the
-     Boolean is going to be used for. *)
-  | Choose of string * (bool -> monad 'regval 'a 'e)
-  (* Print debugging or tracing information *)
-  | Print of string * monad 'regval 'a 'e
-  (*Result of a failed assert with possible error message to report*)
-  | Fail of string
-  (* Exception of type 'e *)
-  | Exception of 'e
-
-type event 'regval =
-  | E_read_mem of read_kind * nat * nat * list memory_byte
-  | E_read_memt of read_kind * nat * nat * (list memory_byte * bitU)
-  | E_write_mem of write_kind * nat * nat * list memory_byte * bool
-  | E_write_memt of write_kind * nat * nat * list memory_byte * bitU * bool
-  | E_write_ea of write_kind * nat * nat
-  | E_excl_res of bool
-  | E_barrier of barrier_kind
-  | E_footprint
-  | E_read_reg of register_name * 'regval
-  | E_write_reg of register_name * 'regval
-  | E_choose of string * bool
-  | E_print of string
-
-type trace 'regval = list (event 'regval)
-
-val return : forall 'rv 'a 'e. 'a -> monad 'rv 'a 'e
-let return a = Done a
-
-val bind : forall 'rv 'a 'b 'e. monad 'rv 'a 'e -> ('a -> monad 'rv 'b 'e) -> monad 'rv 'b 'e
-let rec bind m f = match m with
-  | Done a -> f a
-  | Read_mem rk a sz k ->       Read_mem rk a sz       (fun v -> bind (k v) f)
-  | Read_memt rk a sz k ->      Read_memt rk a sz      (fun v -> bind (k v) f)
-  | Write_mem wk a sz v k ->    Write_mem wk a sz v    (fun v -> bind (k v) f)
-  | Write_memt wk a sz v t k -> Write_memt wk a sz v t (fun v -> bind (k v) f)
-  | Read_reg descr k ->         Read_reg descr         (fun v -> bind (k v) f)
-  | Excl_res k ->               Excl_res               (fun v -> bind (k v) f)
-  | Choose descr k ->           Choose descr           (fun v -> bind (k v) f)
-  | Write_ea wk a sz k ->       Write_ea wk a sz       (bind k f)
-  | Footprint k ->              Footprint              (bind k f)
-  | Barrier bk k ->             Barrier bk             (bind k f)
-  | Write_reg r v k ->          Write_reg r v          (bind k f)
-  | Print msg k ->              Print msg              (bind k f)
-  | Fail descr ->               Fail descr
-  | Exception e ->              Exception e
-end
-
-val exit : forall 'rv 'a 'e. unit -> monad 'rv 'a 'e
-let exit () = Fail "exit"
-
-val choose_bool : forall 'rv 'e. string -> monad 'rv bool 'e
-let choose_bool descr = Choose descr return
-
-val undefined_bool : forall 'rv 'e. unit -> monad 'rv bool 'e
-let undefined_bool () = choose_bool "undefined_bool"
-
-val assert_exp : forall 'rv 'e. bool -> string -> monad 'rv unit 'e
-let assert_exp exp msg = if exp then Done () else Fail msg
-
-val throw : forall 'rv 'a 'e. 'e -> monad 'rv 'a 'e
-let throw e = Exception e
-
-val try_catch : forall 'rv 'a 'e1 'e2. monad 'rv 'a 'e1 -> ('e1 -> monad 'rv 'a 'e2) -> monad 'rv 'a 'e2
-let rec try_catch m h = match m with
-  | Done a -> Done a
-  | Read_mem rk a sz k ->       Read_mem rk a sz       (fun v -> try_catch (k v) h)
-  | Read_memt rk a sz k ->      Read_memt rk a sz      (fun v -> try_catch (k v) h)
-  | Write_mem wk a sz v k ->    Write_mem wk a sz v    (fun v -> try_catch (k v) h)
-  | Write_memt wk a sz v t k -> Write_memt wk a sz v t (fun v -> try_catch (k v) h)
-  | Read_reg descr k ->         Read_reg descr         (fun v -> try_catch (k v) h)
-  | Excl_res k ->               Excl_res               (fun v -> try_catch (k v) h)
-  | Choose descr k ->           Choose descr           (fun v -> try_catch (k v) h)
-  | Write_ea wk a sz k ->       Write_ea wk a sz       (try_catch k h)
-  | Footprint k ->              Footprint              (try_catch k h)
-  | Barrier bk k ->             Barrier bk             (try_catch k h)
-  | 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
-  | Exception e ->              h e
-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 monadR 'rv 'a 'r 'e = monad 'rv 'a (either 'r 'e)
-
-val early_return : forall 'rv 'a 'r 'e. 'r -> monadR 'rv 'a 'r 'e
-let early_return r = throw (Left r)
-
-val catch_early_return : forall 'rv 'a 'e. monadR 'rv 'a 'a 'e -> monad 'rv '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 'rv 'a 'r 'e. monad 'rv 'a 'e -> monadR 'rv '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 'rv 'a 'r 'e1 'e2. monadR 'rv 'a 'r 'e1 -> ('e1 -> monadR 'rv 'a 'r 'e2) ->  monadR 'rv 'a 'r 'e2
-let try_catchR m h =
-  try_catch m
-    (function
-      | Left r -> throw (Left r)
-      | Right e -> h e
-     end)
-
-val maybe_fail : forall 'rv 'a 'e. string -> maybe 'a -> monad 'rv 'a 'e
-let maybe_fail msg = function
-  | Just a -> return a
-  | Nothing -> Fail msg
-end
-
-val read_memt_bytes : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv (list memory_byte * bitU) 'e
-let read_memt_bytes rk addr sz =
-  bind
-    (maybe_fail "nat_of_bv" (nat_of_bv addr))
-    (fun addr -> Read_memt rk addr (nat_of_int sz) return)
-
-val read_memt : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv ('b * bitU) 'e
-let read_memt rk addr sz =
-  bind
-    (read_memt_bytes rk addr sz)
-    (fun (bytes, tag) ->
-       match of_bits (bits_of_mem_bytes bytes) with
-         | Just v -> return (v, tag)
-         | Nothing -> Fail "bits_of_mem_bytes"
-       end)
-
-val read_mem_bytes : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv (list memory_byte) 'e
-let read_mem_bytes rk addr sz =
-  bind
-    (maybe_fail "nat_of_bv" (nat_of_bv addr))
-    (fun addr -> Read_mem rk addr (nat_of_int sz) return)
-
-val read_mem : forall 'rv 'a 'b 'e 'addrsize. Bitvector 'a, Bitvector 'b => read_kind -> 'addrsize -> 'a -> integer -> monad 'rv 'b 'e
-let read_mem rk addr_sz addr sz =
-  bind
-    (read_mem_bytes rk addr sz)
-    (fun bytes ->
-       match of_bits (bits_of_mem_bytes bytes) with
-         | Just v -> return v
-         | Nothing -> Fail "bits_of_mem_bytes"
-       end)
-
-val excl_result : forall 'rv 'e. unit -> monad 'rv bool 'e
-let excl_result () =
-  let k successful = (return successful) in
-  Excl_res k
-
-val write_mem_ea : forall 'rv 'a 'e 'addrsize. Bitvector 'a => write_kind -> 'addrsize -> 'a -> integer -> monad 'rv unit 'e
-let write_mem_ea wk addr_size addr sz =
-  bind
-    (maybe_fail "nat_of_bv" (nat_of_bv addr))
-    (fun addr -> Write_ea wk addr (nat_of_int sz) (Done ()))
-
-val write_mem : forall 'rv 'a 'b 'e 'addrsize. Bitvector 'a, Bitvector 'b =>
-  write_kind -> 'addrsize -> 'a -> integer -> 'b -> monad 'rv bool 'e
-let write_mem wk addr_size addr sz v =
-  match (mem_bytes_of_bits v, nat_of_bv addr) with
-    | (Just v, Just addr) ->
-       Write_mem wk addr (nat_of_int sz) v return
-    | _ -> Fail "write_mem"
-  end
-
-val write_memt : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b =>
-  write_kind -> 'a -> integer -> 'b -> bitU -> monad 'rv bool 'e
-let write_memt wk addr sz v tag =
-  match (mem_bytes_of_bits v, nat_of_bv addr) with
-    | (Just v, Just addr) ->
-       Write_memt wk addr (nat_of_int sz) v tag return
-    | _ -> Fail "write_mem"
-  end
-
-val read_reg : forall 's 'rv 'a 'e. register_ref 's 'rv 'a -> monad 'rv 'a 'e
-let read_reg reg =
-  let k v =
-    match reg.of_regval v with
-      | Just v -> Done v
-      | Nothing -> Fail "read_reg: unrecognised value"
-    end
-  in
-  Read_reg reg.name k
-
-(* TODO
-val read_reg_range : forall 's 'r 'rv 'a 'e. Bitvector 'a => register_ref 's 'rv 'r -> integer -> integer -> monad 'rv 'a 'e
-let read_reg_range reg i j =
-  read_reg_aux of_bits (external_reg_slice reg (nat_of_int i,nat_of_int j))
-
-let read_reg_bit reg i =
-  read_reg_aux (fun v -> v) (external_reg_slice reg (nat_of_int i,nat_of_int i)) >>= fun v ->
-  return (extract_only_element v)
-
-let read_reg_field reg regfield =
-  read_reg_aux (external_reg_field_whole reg regfield)
-
-let read_reg_bitfield reg regfield =
-  read_reg_aux (external_reg_field_whole reg regfield) >>= fun v ->
-  return (extract_only_element v)*)
-
-let reg_deref = read_reg
-
-val write_reg : forall 's 'rv 'a 'e. register_ref 's 'rv 'a -> 'a -> monad 'rv unit 'e
-let write_reg reg v = Write_reg reg.name (reg.regval_of v) (Done ())
-
-(* TODO
-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 (nat_of_int i,nat_of_int j)) v
-let write_reg_pos reg i v =
-  let iN = nat_of_int 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 (nat_of_int i,nat_of_int 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*)
-
-val barrier : forall 'rv 'e. barrier_kind -> monad 'rv unit 'e
-let barrier bk = Barrier bk (Done ())
-
-val footprint : forall 'rv 'e. unit -> monad 'rv unit 'e
-let footprint _ = Footprint (Done ())
-
-(* Event traces *)
-
-val emitEvent : forall 'regval 'a 'e. Eq 'regval => monad 'regval 'a 'e -> event 'regval -> maybe (monad 'regval 'a 'e)
-let emitEvent m e = match (e, m) with
-  | (E_read_mem rk a sz v, Read_mem rk' a' sz' k) ->
-     if rk' = rk && a' = a && sz' = sz then Just (k v) else Nothing
-  | (E_read_memt rk a sz vt, Read_memt rk' a' sz' k) ->
-     if rk' = rk && a' = a && sz' = sz then Just (k vt) else Nothing
-  | (E_write_mem wk a sz v r, Write_mem wk' a' sz' v' k) ->
-     if wk' = wk && a' = a && sz' = sz && v' = v then Just (k r) else Nothing
-  | (E_write_memt wk a sz v tag r, Write_memt wk' a' sz' v' tag' k) ->
-     if wk' = wk && a' = a && sz' = sz && v' = v && tag' = tag then Just (k r) else Nothing
-  | (E_read_reg r v, Read_reg r' k) ->
-     if r' = r then Just (k v) else Nothing
-  | (E_write_reg r v, Write_reg r' v' k) ->
-     if r' = r && v' = v then Just k else Nothing
-  | (E_write_ea wk a sz, Write_ea wk' a' sz' k) ->
-     if wk' = wk && a' = a && sz' = sz then Just k else Nothing
-  | (E_barrier bk, Barrier bk' k) ->
-     if bk' = bk then Just k else Nothing
-  | (E_print m, Print m' k) ->
-     if m' = m then Just k else Nothing
-  | (E_excl_res v, Excl_res k) -> Just (k v)
-  | (E_choose descr v, Choose descr' k) -> if descr' = descr then Just (k v) else Nothing
-  | (E_footprint, Footprint k) -> Just k
-  | _ -> Nothing
-end
-
-val runTrace : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> maybe (monad 'regval 'a 'e)
-let rec runTrace t m = match t with
-  | [] -> Just m
-  | e :: t' -> Maybe.bind (emitEvent m e) (runTrace t')
-end
-
-declare {isabelle} termination_argument runTrace = automatic
-
-val final : forall 'regval 'a 'e. monad 'regval 'a 'e -> bool
-let final = function
-  | Done _ -> true
-  | Fail _ -> true
-  | Exception _ -> true
-  | _ -> false
-end
-
-val hasTrace : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> bool
-let hasTrace t m = match runTrace t m with
-  | Just m -> final m
-  | Nothing -> false
-end
-
-val hasException : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> bool
-let hasException t m = match runTrace t m with
-  | Just (Exception _) -> true
-  | _ -> false
-end
-
-val hasFailure : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> bool
-let hasFailure t m = match runTrace t m with
-  | Just (Fail _) -> true
-  | _ -> false
-end
-
-(* Define a type synonym that also takes the register state as a type parameter,
-   in order to make switching to the state monad without changing generated
-   definitions easier, see also lib/hol/prompt_monad.lem. *)
-
-type base_monad 'regval 'regstate 'a 'e = monad 'regval 'a 'e
-type base_monadR 'regval 'regstate 'a 'r 'e = monadR 'regval 'a 'r 'e
diff --git a/src/gen_lib/0.11/sail2_state.lem b/src/gen_lib/0.11/sail2_state.lem
deleted file mode 100644
index ec787764..00000000
--- a/src/gen_lib/0.11/sail2_state.lem
+++ /dev/null
@@ -1,105 +0,0 @@
-open import Pervasives_extra
-open import Sail2_values
-open import Sail2_state_monad
-open import {isabelle} `Sail2_state_monad_lemmas`
-
-val iterS_aux : forall 'rv 'a 'e. integer -> (integer -> 'a -> monadS 'rv unit 'e) -> list 'a -> monadS 'rv unit 'e
-let rec iterS_aux i f xs = match xs with
-  | x :: xs -> f i x >>$ iterS_aux (i + 1) f xs
-  | [] -> returnS ()
-  end
-
-declare {isabelle} termination_argument iterS_aux = automatic
-
-val iteriS : forall 'rv 'a 'e. (integer -> 'a -> monadS 'rv unit 'e) -> list 'a -> monadS 'rv unit 'e
-let iteriS f xs = iterS_aux 0 f xs
-
-val iterS : forall 'rv 'a 'e. ('a -> monadS 'rv unit 'e) -> list 'a -> monadS 'rv unit 'e
-let iterS f xs = iteriS (fun _ x -> f x) xs
-
-val foreachS : forall 'a 'rv 'vars 'e.
-  list 'a -> 'vars -> ('a -> 'vars -> monadS 'rv 'vars 'e) -> monadS 'rv 'vars 'e
-let rec foreachS xs vars body = match xs with
-  | [] -> returnS vars
-  | x :: xs ->
-     body x vars >>$= fun vars ->
-     foreachS xs vars body
-end
-
-declare {isabelle} termination_argument foreachS = automatic
-
-val genlistS : forall 'a 'rv 'e. (nat -> monadS 'rv 'a 'e) -> nat -> monadS 'rv (list 'a) 'e
-let genlistS f n =
-  let indices = genlist (fun n -> n) n in
-  foreachS indices [] (fun n xs -> (f n >>$= (fun x -> returnS (xs ++ [x]))))
-
-val and_boolS : forall 'rv 'e. monadS 'rv bool 'e -> monadS 'rv bool 'e -> monadS 'rv bool 'e
-let and_boolS l r = l >>$= (fun l -> if l then r else returnS false)
-
-val or_boolS : forall 'rv 'e. monadS 'rv bool 'e -> monadS 'rv bool 'e -> monadS 'rv bool 'e
-let or_boolS l r = l >>$= (fun l -> if l then returnS true else r)
-
-val bool_of_bitU_fail : forall 'rv 'e. bitU -> monadS 'rv bool 'e
-let bool_of_bitU_fail = function
-  | B0 -> returnS false
-  | B1 -> returnS true
-  | BU -> failS "bool_of_bitU"
-end
-
-val bool_of_bitU_nondetS : forall 'rv 'e. bitU -> monadS 'rv bool 'e
-let bool_of_bitU_nondetS = function
-  | B0 -> returnS false
-  | B1 -> returnS true
-  | BU -> undefined_boolS ()
-end
-
-val bools_of_bits_nondetS : forall 'rv 'e. list bitU -> monadS 'rv (list bool) 'e
-let bools_of_bits_nondetS bits =
-  foreachS bits []
-    (fun b bools ->
-      bool_of_bitU_nondetS b >>$= (fun b ->
-      returnS (bools ++ [b])))
-
-val of_bits_nondetS : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monadS 'rv 'a 'e
-let of_bits_nondetS bits =
-  bools_of_bits_nondetS bits >>$= (fun bs ->
-  returnS (of_bools bs))
-
-val of_bits_failS : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monadS 'rv 'a 'e
-let of_bits_failS bits = maybe_failS "of_bits" (of_bits bits)
-
-val mword_nondetS : forall 'rv 'a 'e. Size 'a => unit -> monadS 'rv (mword 'a) 'e
-let mword_nondetS () =
-  bools_of_bits_nondetS (repeat [BU] (integerFromNat size)) >>$= (fun bs ->
-  returnS (wordFromBitlist bs))
-
-
-val whileS : forall 'rv 'vars 'e. 'vars -> ('vars -> monadS 'rv bool 'e) ->
-                ('vars -> monadS 'rv 'vars 'e) -> monadS 'rv 'vars 'e
-let rec whileS vars cond body s =
-  (cond vars >>$= (fun cond_val s' ->
-  if cond_val then
-    (body vars >>$= (fun vars s'' -> whileS vars cond body s'')) s'
-  else returnS vars s')) s
-
-val untilS : forall 'rv 'vars 'e. 'vars -> ('vars -> monadS 'rv bool 'e) ->
-                ('vars -> monadS 'rv 'vars 'e) -> monadS 'rv 'vars 'e
-let rec untilS vars cond body s =
-  (body vars >>$= (fun vars s' ->
-  (cond vars >>$= (fun cond_val s'' ->
-  if cond_val then returnS vars s'' else untilS vars cond body s'')) s')) s
-
-val choose_boolsS : forall 'rv 'e. nat -> monadS 'rv (list bool) 'e
-let choose_boolsS n = genlistS (fun _ -> choose_boolS ()) n
-
-(* TODO: Replace by chooseS and prove equivalence to prompt monad version *)
-val internal_pickS : forall 'rv 'a 'e. list 'a -> monadS 'rv 'a 'e
-let internal_pickS xs =
-  (* Use sufficiently many nondeterministically chosen bits and convert into an
-     index into the list *)
-  choose_boolsS (List.length xs) >>$= fun bs ->
-  let idx = (natFromNatural (nat_of_bools bs)) mod List.length xs in
-  match index xs idx with
-    | Just x -> returnS x
-    | Nothing -> failS "choose internal_pick"
-  end
diff --git a/src/gen_lib/0.11/sail2_state_lifting.lem b/src/gen_lib/0.11/sail2_state_lifting.lem
deleted file mode 100644
index 98a5390d..00000000
--- a/src/gen_lib/0.11/sail2_state_lifting.lem
+++ /dev/null
@@ -1,57 +0,0 @@
-open import Pervasives_extra
-open import Sail2_values
-open import Sail2_prompt_monad
-open import Sail2_prompt
-open import Sail2_state_monad
-open import {isabelle} `Sail2_state_monad_lemmas`
-
-(* Lifting from prompt monad to state monad *)
-val liftState : forall 'regval 'regs 'a 'e. register_accessors 'regs 'regval -> monad 'regval 'a 'e -> monadS 'regs 'a 'e
-let rec liftState ra m = match m with
-  | (Done a)                   -> returnS a
-  | (Read_mem rk a sz k)       -> bindS (read_mem_bytesS rk a sz)       (fun v -> liftState ra (k v))
-  | (Read_memt rk a sz k)      -> bindS (read_memt_bytesS rk a sz)      (fun v -> liftState ra (k v))
-  | (Write_mem wk a sz v k)    -> bindS (write_mem_bytesS wk a sz v)    (fun v -> liftState ra (k v))
-  | (Write_memt wk a sz v t k) -> bindS (write_memt_bytesS wk a sz v t) (fun v -> liftState ra (k v))
-  | (Read_reg r k)             -> bindS (read_regvalS ra r)             (fun v -> liftState ra (k v))
-  | (Excl_res k)               -> bindS (excl_resultS ())               (fun v -> liftState ra (k v))
-  | (Choose _ k)               -> bindS (choose_boolS ())               (fun v -> liftState ra (k v))
-  | (Write_reg r v k)          -> seqS (write_regvalS ra r v)           (liftState ra k)
-  | (Write_ea _ _ _ k)         -> liftState ra k
-  | (Footprint k)              -> liftState ra k
-  | (Barrier _ k)              -> liftState ra k
-  | (Print _ k)                -> liftState ra k (* TODO *)
-  | (Fail descr)               -> failS descr
-  | (Exception e)              -> throwS e
-end
-
-val emitEventS : forall 'regval 'regs 'a 'e. Eq 'regval => register_accessors 'regs 'regval -> event 'regval -> sequential_state 'regs -> maybe (sequential_state 'regs)
-let emitEventS ra e s = match e with
-  | E_read_mem _ addr sz v ->
-     Maybe.bind (get_mem_bytes addr sz s) (fun (v', _) ->
-     if v' = v then Just s else Nothing)
-  | E_read_memt _ addr sz (v, tag) ->
-     Maybe.bind (get_mem_bytes addr sz s) (fun (v', tag') ->
-     if v' = v && tag' = tag then Just s else Nothing)
-  | E_write_mem _ addr sz v success ->
-     if success then Just (put_mem_bytes addr sz v B0 s) else Nothing
-  | E_write_memt _ addr sz v tag success ->
-     if success then Just (put_mem_bytes addr sz v tag s) else Nothing
-  | E_read_reg r v ->
-     let (read_reg, _) = ra in
-     Maybe.bind (read_reg r s.regstate) (fun v' ->
-     if v' = v then Just s else Nothing)
-  | E_write_reg r v ->
-     let (_, write_reg) = ra in
-     Maybe.bind (write_reg r v s.regstate) (fun rs' ->
-     Just <| s with regstate = rs' |>)
-  | _ -> Just s
-end
-
-val runTraceS : forall 'regval 'regs 'a 'e. Eq 'regval => register_accessors 'regs 'regval -> trace 'regval -> sequential_state 'regs -> maybe (sequential_state 'regs)
-let rec runTraceS ra t s = match t with
-  | [] -> Just s
-  | e :: t' -> Maybe.bind (emitEventS ra e s) (runTraceS ra t')
-end
-
-declare {isabelle} termination_argument runTraceS = automatic
diff --git a/src/gen_lib/0.11/sail2_state_monad.lem b/src/gen_lib/0.11/sail2_state_monad.lem
deleted file mode 100644
index 8ea919f9..00000000
--- a/src/gen_lib/0.11/sail2_state_monad.lem
+++ /dev/null
@@ -1,278 +0,0 @@
-open import Pervasives_extra
-open import Sail2_instr_kinds
-open import Sail2_values
-
-(* 'a is result type *)
-
-type memstate = map nat memory_byte
-type tagstate = map nat bitU
-(* type regstate = map string (vector bitU) *)
-
-type sequential_state 'regs =
-  <| regstate : 'regs;
-     memstate : memstate;
-     tagstate : tagstate |>
-
-val init_state : forall 'regs. 'regs -> sequential_state 'regs
-let init_state regs =
-  <| regstate = regs;
-     memstate = Map.empty;
-     tagstate = Map.empty |>
-
-type ex 'e =
-  | Failure of string
-  | Throw of 'e
-
-type result 'a 'e =
-  | Value of 'a
-  | Ex of (ex 'e)
-
-(* State, nondeterminism and exception monad with result value type 'a
-   and exception type 'e. *)
-type monadS 'regs 'a 'e = sequential_state 'regs -> set (result 'a 'e * sequential_state 'regs)
-
-val returnS : forall 'regs 'a 'e. 'a -> monadS 'regs 'a 'e
-let returnS a s = {(Value a,s)}
-
-val bindS : forall 'regs 'a 'b 'e. monadS 'regs 'a 'e -> ('a -> monadS 'regs 'b 'e) -> monadS 'regs 'b 'e
-let bindS m f (s : sequential_state 'regs) =
-  Set.bigunion (Set.map (function
-                | (Value a, s') -> f a s'
-                | (Ex e, s') -> {(Ex e, s')}
-                end) (m s))
-
-val seqS: forall 'regs 'b 'e. monadS 'regs unit 'e -> monadS 'regs 'b 'e -> monadS 'regs 'b 'e
-let seqS m n = bindS m (fun (_ : unit) -> n)
-
-let inline (>>$=) = bindS
-let inline (>>$) = seqS
-
-val chooseS : forall 'regs 'a 'e. SetType 'a => list 'a -> monadS 'regs 'a 'e
-let chooseS xs s = Set.fromList (List.map (fun x -> (Value x, s)) xs)
-
-val readS : forall 'regs 'a 'e. (sequential_state 'regs -> 'a) -> monadS 'regs 'a 'e
-let readS f = (fun s -> returnS (f s) s)
-
-val updateS : forall 'regs 'e. (sequential_state 'regs -> sequential_state 'regs) -> monadS 'regs unit 'e
-let updateS f = (fun s -> returnS () (f s))
-
-val failS : forall 'regs 'a 'e. string -> monadS 'regs 'a 'e
-let failS msg s = {(Ex (Failure msg), s)}
-
-val choose_boolS : forall 'regval 'regs 'a 'e. unit -> monadS 'regs bool 'e
-let choose_boolS () = chooseS [false; true]
-let undefined_boolS = choose_boolS
-
-val exitS : forall 'regs 'e 'a. unit -> monadS 'regs 'a 'e
-let exitS () = failS "exit"
-
-val throwS : forall 'regs 'a 'e. 'e -> monadS 'regs 'a 'e
-let throwS e s = {(Ex (Throw e), s)}
-
-val try_catchS : forall 'regs 'a 'e1 'e2. monadS 'regs 'a 'e1 -> ('e1 -> monadS 'regs 'a 'e2) ->  monadS 'regs 'a 'e2
-let try_catchS m h s =
-  Set.bigunion (Set.map (function
-                | (Value a, s') -> returnS a s'
-                | (Ex (Throw e), s') -> h e s'
-                | (Ex (Failure msg), s') -> {(Ex (Failure msg), s')}
-                end) (m s))
-
-val assert_expS : forall 'regs 'e. bool -> string -> monadS 'regs unit 'e
-let assert_expS exp msg = if exp then returnS () else failS msg
-
-(* 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 monadRS 'regs 'a 'r 'e = monadS 'regs 'a (either 'r 'e)
-
-val early_returnS : forall 'regs 'a 'r 'e. 'r -> monadRS 'regs 'a 'r 'e
-let early_returnS r = throwS (Left r)
-
-val catch_early_returnS : forall 'regs 'a 'e. monadRS 'regs 'a 'a 'e -> monadS 'regs 'a 'e
-let catch_early_returnS m =
-  try_catchS m
-    (function
-      | Left a -> returnS a
-      | Right e -> throwS e
-     end)
-
-(* Lift to monad with early return by wrapping exceptions *)
-val liftRS : forall 'a 'r 'regs 'e. monadS 'regs 'a 'e -> monadRS 'regs 'a 'r 'e
-let liftRS m = try_catchS m (fun e -> throwS (Right e))
-
-(* Catch exceptions in the presence of early returns *)
-val try_catchRS : forall 'regs 'a 'r 'e1 'e2. monadRS 'regs 'a 'r 'e1 -> ('e1 -> monadRS 'regs 'a 'r 'e2) ->  monadRS 'regs 'a 'r 'e2
-let try_catchRS m h =
-  try_catchS m
-    (function
-      | Left r -> throwS (Left r)
-      | Right e -> h e
-     end)
-
-val maybe_failS : forall 'regs 'a 'e. string -> maybe 'a -> monadS 'regs 'a 'e
-let maybe_failS msg = function
-  | Just a  -> returnS a
-  | Nothing -> failS msg
-end
-
-val read_tagS : forall 'regs 'a 'e. Bitvector 'a => 'a -> monadS 'regs bitU 'e
-let read_tagS addr =
-  maybe_failS "nat_of_bv" (nat_of_bv addr) >>$= (fun addr ->
-  readS (fun s -> fromMaybe B0 (Map.lookup addr s.tagstate)))
-
-(* Read bytes from memory and return in little endian order *)
-val get_mem_bytes : forall 'regs. nat -> nat -> sequential_state 'regs -> maybe (list memory_byte * bitU)
-let get_mem_bytes addr sz s =
-  let addrs = genlist (fun n -> addr + n) sz in
-  let read_byte s addr = Map.lookup addr s.memstate in
-  let read_tag s addr = Map.findWithDefault addr B0 s.tagstate in
-  Maybe.map
-    (fun mem_val -> (mem_val, List.foldl and_bit B1 (List.map (read_tag s) addrs)))
-    (just_list (List.map (read_byte s) addrs))
-
-val read_memt_bytesS : forall 'regs 'e. read_kind -> nat -> nat -> monadS 'regs (list memory_byte * bitU) 'e
-let read_memt_bytesS _ addr sz =
-  readS (get_mem_bytes addr sz) >>$=
-  maybe_failS "read_memS"
-
-val read_mem_bytesS : forall 'regs 'e. read_kind -> nat -> nat -> monadS 'regs (list memory_byte) 'e
-let read_mem_bytesS rk addr sz =
-  read_memt_bytesS rk addr sz >>$= (fun (bytes, _) ->
-  returnS bytes)
-
-val read_memtS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs ('b * bitU) 'e
-let read_memtS rk a sz =
-  maybe_failS "nat_of_bv" (nat_of_bv a) >>$= (fun a ->
-  read_memt_bytesS rk a (nat_of_int sz) >>$= (fun (bytes, tag) ->
-  maybe_failS "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes)) >>$= (fun mem_val ->
-  returnS (mem_val, tag))))
-
-val read_memS : forall 'regs 'e 'a 'b 'addrsize. Bitvector 'a, Bitvector 'b => read_kind -> 'addrsize -> 'a -> integer -> monadS 'regs 'b 'e
-let read_memS rk addr_size a sz =
-  read_memtS rk a sz >>$= (fun (bytes, _) ->
-  returnS bytes)
-
-val excl_resultS : forall 'regs 'e. unit -> monadS 'regs bool 'e
-let excl_resultS =
-  (* TODO: This used to be more deterministic, checking a flag in the state
-     whether an exclusive load has occurred before.  However, this does not
-     seem very precise; it might be safer to overapproximate the possible
-     behaviours by always making a nondeterministic choice. *)
-  undefined_boolS
-
-(* Write little-endian list of bytes to given address *)
-val put_mem_bytes : forall 'regs. nat -> nat -> list memory_byte -> bitU -> sequential_state 'regs -> sequential_state 'regs
-let put_mem_bytes addr sz v tag s =
-  let addrs = genlist (fun n -> addr + n) sz in
-  let a_v = List.zip addrs v in
-  let write_byte mem (addr, v) = Map.insert addr v mem in
-  let write_tag mem addr = Map.insert addr tag mem in
-  <| s with memstate = List.foldl write_byte s.memstate a_v;
-            tagstate = List.foldl write_tag s.tagstate addrs |>
-
-val write_memt_bytesS : forall 'regs 'e. write_kind -> nat -> nat -> list memory_byte -> bitU -> monadS 'regs bool 'e
-let write_memt_bytesS _ addr sz v t =
-  updateS (put_mem_bytes addr sz v t) >>$
-  returnS true
-
-val write_mem_bytesS : forall 'regs 'e. write_kind -> nat -> nat -> list memory_byte -> monadS 'regs bool 'e
-let write_mem_bytesS wk addr sz v = write_memt_bytesS wk addr sz v B0
-
-val write_memtS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b =>
-  write_kind -> 'a -> integer -> 'b -> bitU -> monadS 'regs bool 'e
-let write_memtS wk addr sz v t =
-  match (nat_of_bv addr, mem_bytes_of_bits v) with
-    | (Just addr, Just v) -> write_memt_bytesS wk addr (nat_of_int sz) v t
-    | _ -> failS "write_mem"
-  end
-
-val write_memS : forall 'regs 'e 'a 'b 'addrsize. Bitvector 'a, Bitvector 'b =>
-  write_kind -> 'addrsize -> 'a -> integer -> 'b -> monadS 'regs bool 'e
-let write_memS wk addr_size addr sz v = write_memtS wk addr sz v B0
-
-val read_regS : forall 'regs 'rv 'a 'e. register_ref 'regs 'rv 'a -> monadS 'regs 'a 'e
-let read_regS reg = readS (fun s -> reg.read_from s.regstate)
-
-(* TODO
-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 *)
-
-val read_regvalS : forall 'regs 'rv 'e.
-  register_accessors 'regs 'rv -> string -> monadS 'regs 'rv 'e
-let read_regvalS (read, _) reg =
-  readS (fun s -> read reg s.regstate) >>$= (function
-      | Just v ->  returnS v
-      | Nothing -> failS ("read_regvalS " ^ reg)
-    end)
-
-val write_regvalS : forall 'regs 'rv 'e.
-  register_accessors 'regs 'rv -> string -> 'rv -> monadS 'regs unit 'e
-let write_regvalS (_, write) reg v =
-  readS (fun s -> write reg v s.regstate) >>$= (function
-      | Just rs' -> updateS (fun s -> <| s with regstate = rs' |>)
-      | Nothing ->  failS ("write_regvalS " ^ reg)
-    end)
-
-val write_regS : forall 'regs 'rv 'a 'e. register_ref 'regs 'rv 'a -> 'a -> monadS 'regs unit 'e
-let write_regS reg v =
-  updateS (fun s -> <| s with regstate = reg.write_to v s.regstate |>)
-
-(* TODO
-val update_reg : forall 'regs 'rv 'a 'b 'e. register_ref 'regs 'rv 'a -> ('a -> 'b -> 'a) -> 'b -> monadS '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 'rv 'a 'b. Bitvector 'a, Bitvector 'b => register_ref 'regs 'rv 'a -> integer -> integer -> 'a -> 'b -> 'a
-let update_reg_range reg i j reg_val new_val = set_bits (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.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.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)*)
-
-(* TODO Add Show typeclass for value and exception type *)
-val show_result : forall 'a 'e. result 'a 'e -> string
-let show_result = function
-  | Value _ -> "Value ()"
-  | Ex (Failure msg) -> "Failure " ^ msg
-  | Ex (Throw _) -> "Throw"
-end
-
-val prerr_results : forall 'a 'e 's. SetType 's => set (result 'a 'e * 's) -> unit
-let prerr_results rs =
-  let _ = Set.map (fun (r, _) -> let _ = prerr_endline (show_result r) in ()) rs in
-  ()
diff --git a/src/gen_lib/0.11/sail2_string.lem b/src/gen_lib/0.11/sail2_string.lem
deleted file mode 100644
index 33a665a0..00000000
--- a/src/gen_lib/0.11/sail2_string.lem
+++ /dev/null
@@ -1,448 +0,0 @@
-open import Pervasives
-open import List
-open import List_extra
-open import String
-open import String_extra
-
-open import Sail2_operators
-open import Sail2_values
-
-val string_sub : string -> ii -> ii -> string
-let string_sub str start len =
-  toString (take (natFromInteger len) (drop (natFromInteger start) (toCharList str)))
-
-val string_startswith : string -> string -> bool
-let string_startswith str1 str2 =
-  let prefix = string_sub str1 0 (integerFromNat (stringLength str2)) in
-  (prefix = str2)
-
-val string_drop : string -> ii -> string
-let string_drop str n =
-  toString (drop (natFromInteger n) (toCharList str))
-
-val string_take : string -> ii -> string
-let string_take str n =
-  toString (take (natFromInteger n) (toCharList str))
-
-val string_length : string -> ii
-let string_length s = integerFromNat (stringLength s)
-
-let string_append = stringAppend
-
-(***********************************************
- * Begin stuff that should be in Lem Num_extra *
- ***********************************************)
-
-val maybeIntegerOfString : string -> maybe integer
-let maybeIntegerOfString _ = Nothing (* TODO FIXME *)
-declare ocaml target_rep function maybeIntegerOfString = `(fun s -> match int_of_string s with i -> Some (Nat_big_num.of_int i) | exception Failure _ -> None )`
-
-(***********************************************
- * end stuff that should be in Lem Num_extra   *
- ***********************************************)
-
-let rec maybe_int_of_prefix s =
-  match s with
-  | "" -> Nothing
-  | str ->
-     let len = string_length str in
-     match maybeIntegerOfString str with
-     | Just n -> Just (n, len)
-     | Nothing -> maybe_int_of_prefix (string_sub str 0 (len - 1))
-     end
-  end
-
-let maybe_int_of_string = maybeIntegerOfString
-
-val n_leading_spaces : string -> ii
-let rec n_leading_spaces s =
-  let len = string_length s in
-  if len = 0 then 0 else
-    if len = 1 then
-      match s with
-         | " " -> 1
-         | _ -> 0
-      end
-    else
-           (* Isabelle generation for pattern matching on characters
-              is currently broken, so use an if-expression *)
-           if nth s 0 = #' '
-           then 1 + (n_leading_spaces (string_sub s 1 (len - 1)))
-           else 0
-  (* end *)
-
-let opt_spc_matches_prefix s =
-  Just ((), n_leading_spaces s)
-
-let spc_matches_prefix s =
-  let n = n_leading_spaces s in
-  (* match n with *)
-(* | 0 -> Nothing *)
-  if n = 0 then Nothing else
-  (* | n -> *) Just ((), n)
-  (* end *)
-
-(* Python:
-f = """let hex_bits_{0}_matches_prefix s =
-  match maybe_int_of_prefix s with
-  | Nothing -> Nothing
-  | Just (n, len) ->
-    if 0 <= n && n < (2 ** {0}) then
-      Just ((of_int {0} n, len))
-    else
-      Nothing
-  end
-"""
-
-for i in list(range(1, 34)) + [48, 64]:
-  print(f.format(i))
-*)
-let hex_bits_1_matches_prefix s =
-  match maybe_int_of_prefix s with
-  | Nothing -> Nothing
-  | Just (n, len) ->
-    if 0 <= n && n < (2 ** 1) then
-      Just ((of_int 1 n, len))
-    else
-      Nothing
-  end
-
-let hex_bits_2_matches_prefix s =
-  match maybe_int_of_prefix s with
-  | Nothing -> Nothing
-  | Just (n, len) ->
-    if 0 <= n && n < (2 ** 2) then
-      Just ((of_int 2 n, len))
-    else
-      Nothing
-  end
-
-let hex_bits_3_matches_prefix s =
-  match maybe_int_of_prefix s with
-  | Nothing -> Nothing
-  | Just (n, len) ->
-    if 0 <= n && n < (2 ** 3) then
-      Just ((of_int 3 n, len))
-    else
-      Nothing
-  end
-
-let hex_bits_4_matches_prefix s =
-  match maybe_int_of_prefix s with
-  | Nothing -> Nothing
-  | Just (n, len) ->
-    if 0 <= n && n < (2 ** 4) then
-      Just ((of_int 4 n, len))
-    else
-      Nothing
-  end
-
-let hex_bits_5_matches_prefix s =
-  match maybe_int_of_prefix s with
-  | Nothing -> Nothing
-  | Just (n, len) ->
-    if 0 <= n && n < (2 ** 5) then
-      Just ((of_int 5 n, len))
-    else
-      Nothing
-  end
-
-let hex_bits_6_matches_prefix s =
-  match maybe_int_of_prefix s with
-  | Nothing -> Nothing
-  | Just (n, len) ->
-    if 0 <= n && n < (2 ** 6) then
-      Just ((of_int 6 n, len))
-    else
-      Nothing
-  end
-
-let hex_bits_7_matches_prefix s =
-  match maybe_int_of_prefix s with
-  | Nothing -> Nothing
-  | Just (n, len) ->
-    if 0 <= n && n < (2 ** 7) then
-      Just ((of_int 7 n, len))
-    else
-      Nothing
-  end
-
-let hex_bits_8_matches_prefix s =
-  match maybe_int_of_prefix s with
-  | Nothing -> Nothing
-  | Just (n, len) ->
-    if 0 <= n && n < (2 ** 8) then
-      Just ((of_int 8 n, len))
-    else
-      Nothing
-  end
-
-let hex_bits_9_matches_prefix s =
-  match maybe_int_of_prefix s with
-  | Nothing -> Nothing
-  | Just (n, len) ->
-    if 0 <= n && n < (2 ** 9) then
-      Just ((of_int 9 n, len))
-    else
-      Nothing
-  end
-
-let hex_bits_10_matches_prefix s =
-  match maybe_int_of_prefix s with
-  | Nothing -> Nothing
-  | Just (n, len) ->
-    if 0 <= n && n < (2 ** 10) then
-      Just ((of_int 10 n, len))
-    else
-      Nothing
-  end
-
-let hex_bits_11_matches_prefix s =
-  match maybe_int_of_prefix s with
-  | Nothing -> Nothing
-  | Just (n, len) ->
-    if 0 <= n && n < (2 ** 11) then
-      Just ((of_int 11 n, len))
-    else
-      Nothing
-  end
-
-let hex_bits_12_matches_prefix s =
-  match maybe_int_of_prefix s with
-  | Nothing -> Nothing
-  | Just (n, len) ->
-    if 0 <= n && n < (2 ** 12) then
-      Just ((of_int 12 n, len))
-    else
-      Nothing
-  end
-
-let hex_bits_13_matches_prefix s =
-  match maybe_int_of_prefix s with
-  | Nothing -> Nothing
-  | Just (n, len) ->
-    if 0 <= n && n < (2 ** 13) then
-      Just ((of_int 13 n, len))
-    else
-      Nothing
-  end
-
-let hex_bits_14_matches_prefix s =
-  match maybe_int_of_prefix s with
-  | Nothing -> Nothing
-  | Just (n, len) ->
-    if 0 <= n && n < (2 ** 14) then
-      Just ((of_int 14 n, len))
-    else
-      Nothing
-  end
-
-let hex_bits_15_matches_prefix s =
-  match maybe_int_of_prefix s with
-  | Nothing -> Nothing
-  | Just (n, len) ->
-    if 0 <= n && n < (2 ** 15) then
-      Just ((of_int 15 n, len))
-    else
-      Nothing
-  end
-
-let hex_bits_16_matches_prefix s =
-  match maybe_int_of_prefix s with
-  | Nothing -> Nothing
-  | Just (n, len) ->
-    if 0 <= n && n < (2 ** 16) then
-      Just ((of_int 16 n, len))
-    else
-      Nothing
-  end
-
-let hex_bits_17_matches_prefix s =
-  match maybe_int_of_prefix s with
-  | Nothing -> Nothing
-  | Just (n, len) ->
-    if 0 <= n && n < (2 ** 17) then
-      Just ((of_int 17 n, len))
-    else
-      Nothing
-  end
-
-let hex_bits_18_matches_prefix s =
-  match maybe_int_of_prefix s with
-  | Nothing -> Nothing
-  | Just (n, len) ->
-    if 0 <= n && n < (2 ** 18) then
-      Just ((of_int 18 n, len))
-    else
-      Nothing
-  end
-
-let hex_bits_19_matches_prefix s =
-  match maybe_int_of_prefix s with
-  | Nothing -> Nothing
-  | Just (n, len) ->
-    if 0 <= n && n < (2 ** 19) then
-      Just ((of_int 19 n, len))
-    else
-      Nothing
-  end
-
-let hex_bits_20_matches_prefix s =
-  match maybe_int_of_prefix s with
-  | Nothing -> Nothing
-  | Just (n, len) ->
-    if 0 <= n && n < (2 ** 20) then
-      Just ((of_int 20 n, len))
-    else
-      Nothing
-  end
-
-let hex_bits_21_matches_prefix s =
-  match maybe_int_of_prefix s with
-  | Nothing -> Nothing
-  | Just (n, len) ->
-    if 0 <= n && n < (2 ** 21) then
-      Just ((of_int 21 n, len))
-    else
-      Nothing
-  end
-
-let hex_bits_22_matches_prefix s =
-  match maybe_int_of_prefix s with
-  | Nothing -> Nothing
-  | Just (n, len) ->
-    if 0 <= n && n < (2 ** 22) then
-      Just ((of_int 22 n, len))
-    else
-      Nothing
-  end
-
-let hex_bits_23_matches_prefix s =
-  match maybe_int_of_prefix s with
-  | Nothing -> Nothing
-  | Just (n, len) ->
-    if 0 <= n && n < (2 ** 23) then
-      Just ((of_int 23 n, len))
-    else
-      Nothing
-  end
-
-let hex_bits_24_matches_prefix s =
-  match maybe_int_of_prefix s with
-  | Nothing -> Nothing
-  | Just (n, len) ->
-    if 0 <= n && n < (2 ** 24) then
-      Just ((of_int 24 n, len))
-    else
-      Nothing
-  end
-
-let hex_bits_25_matches_prefix s =
-  match maybe_int_of_prefix s with
-  | Nothing -> Nothing
-  | Just (n, len) ->
-    if 0 <= n && n < (2 ** 25) then
-      Just ((of_int 25 n, len))
-    else
-      Nothing
-  end
-
-let hex_bits_26_matches_prefix s =
-  match maybe_int_of_prefix s with
-  | Nothing -> Nothing
-  | Just (n, len) ->
-    if 0 <= n && n < (2 ** 26) then
-      Just ((of_int 26 n, len))
-    else
-      Nothing
-  end
-
-let hex_bits_27_matches_prefix s =
-  match maybe_int_of_prefix s with
-  | Nothing -> Nothing
-  | Just (n, len) ->
-    if 0 <= n && n < (2 ** 27) then
-      Just ((of_int 27 n, len))
-    else
-      Nothing
-  end
-
-let hex_bits_28_matches_prefix s =
-  match maybe_int_of_prefix s with
-  | Nothing -> Nothing
-  | Just (n, len) ->
-    if 0 <= n && n < (2 ** 28) then
-      Just ((of_int 28 n, len))
-    else
-      Nothing
-  end
-
-let hex_bits_29_matches_prefix s =
-  match maybe_int_of_prefix s with
-  | Nothing -> Nothing
-  | Just (n, len) ->
-    if 0 <= n && n < (2 ** 29) then
-      Just ((of_int 29 n, len))
-    else
-      Nothing
-  end
-
-let hex_bits_30_matches_prefix s =
-  match maybe_int_of_prefix s with
-  | Nothing -> Nothing
-  | Just (n, len) ->
-    if 0 <= n && n < (2 ** 30) then
-      Just ((of_int 30 n, len))
-    else
-      Nothing
-  end
-
-let hex_bits_31_matches_prefix s =
-  match maybe_int_of_prefix s with
-  | Nothing -> Nothing
-  | Just (n, len) ->
-    if 0 <= n && n < (2 ** 31) then
-      Just ((of_int 31 n, len))
-    else
-      Nothing
-  end
-
-let hex_bits_32_matches_prefix s =
-  match maybe_int_of_prefix s with
-  | Nothing -> Nothing
-  | Just (n, len) ->
-    if 0 <= n && n < (2 ** 32) then
-      Just ((of_int 32 n, len))
-    else
-      Nothing
-  end
-
-let hex_bits_33_matches_prefix s =
-  match maybe_int_of_prefix s with
-  | Nothing -> Nothing
-  | Just (n, len) ->
-    if 0 <= n && n < (2 ** 33) then
-      Just ((of_int 33 n, len))
-    else
-      Nothing
-  end
-
-let hex_bits_48_matches_prefix s =
-  match maybe_int_of_prefix s with
-  | Nothing -> Nothing
-  | Just (n, len) ->
-    if 0 <= n && n < (2 ** 48) then
-      Just ((of_int 48 n, len))
-    else
-      Nothing
-  end
-
-let hex_bits_64_matches_prefix s =
-  match maybe_int_of_prefix s with
-  | Nothing -> Nothing
-  | Just (n, len) ->
-    if 0 <= n && n < (2 ** 64) then
-      Just ((of_int 64 n, len))
-    else
-      Nothing
-  end
diff --git a/src/gen_lib/0.11/sail2_values.lem b/src/gen_lib/0.11/sail2_values.lem
deleted file mode 100644
index f657803f..00000000
--- a/src/gen_lib/0.11/sail2_values.lem
+++ /dev/null
@@ -1,999 +0,0 @@
-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
-*)
diff --git a/src/gen_lib/0.11/sail_impl_base.lem b/src/gen_lib/0.11/sail_impl_base.lem
deleted file mode 100644
index 421219da..00000000
--- a/src/gen_lib/0.11/sail_impl_base.lem
+++ /dev/null
@@ -1,1518 +0,0 @@
-(*========================================================================*)
-(*     Sail                                                               *)
-(*                                                                        *)
-(*  Copyright (c) 2013-2017                                               *)
-(*    Kathyrn Gray                                                        *)
-(*    Shaked Flur                                                         *)
-(*    Stephen Kell                                                        *)
-(*    Gabriel Kerneis                                                     *)
-(*    Robert Norton-Wright                                                *)
-(*    Christopher Pulte                                                   *)
-(*    Peter Sewell                                                        *)
-(*    Alasdair Armstrong                                                  *)
-(*    Brian Campbell                                                      *)
-(*    Thomas Bauereiss                                                    *)
-(*    Anthony Fox                                                         *)
-(*    Jon French                                                          *)
-(*    Dominic Mulligan                                                    *)
-(*    Stephen Kell                                                        *)
-(*    Mark Wassell                                                        *)
-(*                                                                        *)
-(*  All rights reserved.                                                  *)
-(*                                                                        *)
-(*  This software was developed by the University of Cambridge Computer   *)
-(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
-(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
-(*                                                                        *)
-(*  Redistribution and use in source and binary forms, with or without    *)
-(*  modification, are permitted provided that the following conditions    *)
-(*  are met:                                                              *)
-(*  1. Redistributions of source code must retain the above copyright     *)
-(*     notice, this list of conditions and the following disclaimer.      *)
-(*  2. Redistributions in binary form must reproduce the above copyright  *)
-(*     notice, this list of conditions and the following disclaimer in    *)
-(*     the documentation and/or other materials provided with the         *)
-(*     distribution.                                                      *)
-(*                                                                        *)
-(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
-(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
-(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
-(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
-(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
-(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
-(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
-(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
-(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
-(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
-(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
-(*  SUCH DAMAGE.                                                          *)
-(*========================================================================*)
-
-open import Pervasives_extra
-
-
-
-class ( EnumerationType 'a ) 
-  val toNat : 'a -> nat
-end
-
-
-val enumeration_typeCompare : forall 'a. EnumerationType 'a => 'a -> 'a -> ordering
-let ~{ocaml} enumeration_typeCompare e1 e2 =
-  compare (toNat e1) (toNat e2)
-let inline {ocaml} enumeration_typeCompare = defaultCompare
-
- 
-default_instance forall 'a. EnumerationType 'a => (Ord 'a)
-  let compare = enumeration_typeCompare
-  let (<)  r1 r2 = (enumeration_typeCompare r1 r2) = LT
-  let (<=) r1 r2 = (enumeration_typeCompare r1 r2) <> GT
-  let (>)  r1 r2 = (enumeration_typeCompare r1 r2) = GT
-  let (>=) r1 r2 = (enumeration_typeCompare r1 r2) <> LT
-end
-
-
-
-(* maybe isn't a member of type Ord - this should be in the Lem standard library*)
-instance forall 'a. Ord 'a => (Ord (maybe 'a))
-  let compare = maybeCompare compare
-  let (<)  r1 r2 = (maybeCompare compare r1 r2) = LT
-  let (<=) r1 r2 = (maybeCompare compare r1 r2) <> GT
-  let (>)  r1 r2 = (maybeCompare compare r1 r2) = GT
-  let (>=) r1 r2 = (maybeCompare compare r1 r2) <> LT
-end
-
-type word8 = nat (* bounded at a byte, for when lem supports it*)
-
-type end_flag =
-  | E_big_endian
-  | E_little_endian
-
-type bit =
-  | Bitc_zero
-  | Bitc_one
-
-type bit_lifted = 
-  | Bitl_zero
-  | Bitl_one
-  | Bitl_undef    (* used for modelling h/w arch unspecified bits *)
-  | Bitl_unknown  (* used for interpreter analysis exhaustive execution *)
-
-type direction = 
-  | D_increasing
-  | D_decreasing
-
-(* at some point this should probably not mention bit_lifted anymore *)
-type register_value = <| 
-    rv_bits: list bit_lifted (* MSB first, smallest index number *); 
-    rv_dir: direction; 
-    rv_start: nat ;
-    rv_start_internal: nat; 
-    (*when dir is increasing, rv_start = rv_start_internal. 
-      Otherwise, tells interpreter how to reconstruct a proper decreasing value*)
-    |>
-
-type byte_lifted = Byte_lifted of list bit_lifted (* of length 8 *) (*MSB first everywhere*)
-
-type instruction_field_value = list bit
-
-type byte = Byte of list bit (* of length 8 *)  (*MSB first everywhere*) 
-
-type address_lifted = Address_lifted of list byte_lifted (* of length 8 for 64bit machines*) * maybe integer
-(* for both values of end_flag, MSBy first *)
-
-type memory_byte = byte_lifted (* of length 8 *) (*MSB first everywhere*)
-
-type memory_value = list memory_byte
-(* the list is of length >=1 *)
-(* the head of the list is the byte stored at the lowest address;
-when calling a Sail function with a wmv effect, the least significant 8
-bits of the bit vector passed to the function will be interpreted as
-the lowest address byte; similarly, when calling a Sail function with
-rmem effect, the lowest address byte will be placed in the least
-significant 8 bits of the bit vector returned by the function; this
-behaviour is consistent with little-endian. *)
-
-
-(* not sure which of these is more handy yet *)
-type address = Address of list byte (* of length 8 *) * integer
-(* type address = Address of integer *)
-
-type opcode = Opcode of list byte (* of length 4 *)
-
-(** typeclass instantiations *)
-
-let ~{ocaml} bitCompare (b1:bit) (b2:bit) =
-  match (b1,b2) with
-  | (Bitc_zero, Bitc_zero) -> EQ
-  | (Bitc_one, Bitc_one) -> EQ
-  | (Bitc_zero, _) -> LT
-  | (_,_) -> GT
-  end
-let inline {ocaml} bitCompare = defaultCompare
-
-let ~{ocaml} bitLess b1 b2      = bitCompare b1 b2 =  LT
-let ~{ocaml} bitLessEq b1 b2    = bitCompare b1 b2 <> GT
-let ~{ocaml} bitGreater b1 b2   = bitCompare b1 b2 =  GT
-let ~{ocaml} bitGreaterEq b1 b2 = bitCompare b1 b2 <> LT
-
-let inline {ocaml} bitLess      = defaultLess
-let inline {ocaml} bitLessEq    = defaultLessEq
-let inline {ocaml} bitGreater   = defaultGreater
-let inline {ocaml} bitGreaterEq = defaultGreaterEq
-
-instance (Ord bit)
-  let compare = bitCompare
-  let (<)  = bitLess
-  let (<=) = bitLessEq
-  let (>)  = bitGreater
-  let (>=) = bitGreaterEq
-end
-
-let ~{ocaml} bit_liftedCompare (bl1:bit_lifted) (bl2:bit_lifted) =
-  match (bl1,bl2) with
-  | (Bitl_zero, Bitl_zero) -> EQ
-  | (Bitl_zero,_) -> LT
-  | (Bitl_one, Bitl_zero) -> GT
-  | (Bitl_one, Bitl_one) -> EQ
-  | (Bitl_one, _) -> LT
-  | (Bitl_undef,Bitl_zero) -> GT
-  | (Bitl_undef,Bitl_one) -> GT
-  | (Bitl_undef,Bitl_undef) -> EQ
-  | (Bitl_undef,_) -> LT
-  | (Bitl_unknown,Bitl_unknown) -> EQ
-  | (Bitl_unknown,_) -> GT
-  end
-let inline {ocaml} bit_liftedCompare = defaultCompare
-
-let ~{ocaml} bit_liftedLess b1 b2      = bit_liftedCompare b1 b2 =  LT
-let ~{ocaml} bit_liftedLessEq b1 b2    = bit_liftedCompare b1 b2 <> GT
-let ~{ocaml} bit_liftedGreater b1 b2   = bit_liftedCompare b1 b2 =  GT
-let ~{ocaml} bit_liftedGreaterEq b1 b2 = bit_liftedCompare b1 b2 <> LT
-
-let inline {ocaml} bit_liftedLess      = defaultLess
-let inline {ocaml} bit_liftedLessEq    = defaultLessEq
-let inline {ocaml} bit_liftedGreater   = defaultGreater
-let inline {ocaml} bit_liftedGreaterEq = defaultGreaterEq
-
-instance (Ord bit_lifted)
-  let compare = bit_liftedCompare
-  let (<)  = bit_liftedLess
-  let (<=) = bit_liftedLessEq
-  let (>)  = bit_liftedGreater
-  let (>=) = bit_liftedGreaterEq
-end
-
-let ~{ocaml} byte_liftedCompare (Byte_lifted b1) (Byte_lifted b2) = compare b1 b2
-let inline {ocaml} byte_liftedCompare = defaultCompare
-
-let ~{ocaml} byte_liftedLess b1 b2      = byte_liftedCompare b1 b2 =  LT
-let ~{ocaml} byte_liftedLessEq b1 b2    = byte_liftedCompare b1 b2 <> GT
-let ~{ocaml} byte_liftedGreater b1 b2   = byte_liftedCompare b1 b2 =  GT
-let ~{ocaml} byte_liftedGreaterEq b1 b2 = byte_liftedCompare b1 b2 <> LT
-
-let inline {ocaml} byte_liftedLess      = defaultLess
-let inline {ocaml} byte_liftedLessEq    = defaultLessEq
-let inline {ocaml} byte_liftedGreater   = defaultGreater
-let inline {ocaml} byte_liftedGreaterEq = defaultGreaterEq
-
-instance (Ord byte_lifted)
-  let compare = byte_liftedCompare
-  let (<)  = byte_liftedLess
-  let (<=) = byte_liftedLessEq
-  let (>)  = byte_liftedGreater
-  let (>=) = byte_liftedGreaterEq
-end
-
-let ~{ocaml} byteCompare (Byte b1) (Byte b2) = compare b1 b2
-let inline {ocaml} byteCompare = defaultCompare
-
-let ~{ocaml} byteLess b1 b2      = byteCompare b1 b2 =  LT
-let ~{ocaml} byteLessEq b1 b2    = byteCompare b1 b2 <> GT
-let ~{ocaml} byteGreater b1 b2   = byteCompare b1 b2 =  GT
-let ~{ocaml} byteGreaterEq b1 b2 = byteCompare b1 b2 <> LT
-
-let inline {ocaml} byteLess      = defaultLess
-let inline {ocaml} byteLessEq    = defaultLessEq
-let inline {ocaml} byteGreater   = defaultGreater
-let inline {ocaml} byteGreaterEq = defaultGreaterEq
-
-instance (Ord byte)
-  let compare = byteCompare
-  let (<)  = byteLess
-  let (<=) = byteLessEq
-  let (>)  = byteGreater
-  let (>=) = byteGreaterEq
-end
-
-let ~{ocaml} opcodeCompare (Opcode o1) (Opcode o2) =
-  compare o1 o2
-let {ocaml} opcodeCompare = defaultCompare
-
-let ~{ocaml} opcodeLess b1 b2      = opcodeCompare b1 b2 =  LT
-let ~{ocaml} opcodeLessEq b1 b2    = opcodeCompare b1 b2 <> GT
-let ~{ocaml} opcodeGreater b1 b2   = opcodeCompare b1 b2 =  GT
-let ~{ocaml} opcodeGreaterEq b1 b2 = opcodeCompare b1 b2 <> LT
-
-let inline {ocaml} opcodeLess      = defaultLess
-let inline {ocaml} opcodeLessEq    = defaultLessEq
-let inline {ocaml} opcodeGreater   = defaultGreater
-let inline {ocaml} opcodeGreaterEq = defaultGreaterEq
-
-instance (Ord opcode)
-  let compare = opcodeCompare
-  let (<)  = opcodeLess
-  let (<=) = opcodeLessEq
-  let (>)  = opcodeGreater
-  let (>=) = opcodeGreaterEq
-end
-
-let addressCompare (Address b1 i1) (Address b2 i2) = compare i1 i2
-(* this cannot be defaultCompare for OCaml because addresses contain big ints *)
-
-let addressLess b1 b2      = addressCompare b1 b2 =  LT
-let addressLessEq b1 b2    = addressCompare b1 b2 <> GT
-let addressGreater b1 b2   = addressCompare b1 b2 =  GT
-let addressGreaterEq b1 b2 = addressCompare b1 b2 <> LT
-
-instance (SetType address)
-  let setElemCompare = addressCompare
-end
-
-instance (Ord address)
-  let compare = addressCompare
-  let (<)  = addressLess
-  let (<=) = addressLessEq
-  let (>)  = addressGreater
-  let (>=) = addressGreaterEq
-end
-
-let {coq; ocaml} addressEqual a1 a2 = (addressCompare a1 a2) = EQ
-let inline {hol; isabelle} addressEqual = unsafe_structural_equality
-
-let {coq; ocaml} addressInequal a1 a2 = not (addressEqual a1 a2)
-let inline {hol; isabelle} addressInequal = unsafe_structural_inequality
-
-instance  (Eq address)
-  let (=)  = addressEqual
-  let (<>) = addressInequal
-end
-
-let ~{ocaml} directionCompare d1 d2 =
-  match (d1, d2) with
-  | (D_decreasing, D_increasing) -> GT
-  | (D_increasing, D_decreasing) -> LT
-  | _ -> EQ
-  end
-let inline {ocaml} directionCompare = defaultCompare
-
-let ~{ocaml} directionLess b1 b2      = directionCompare b1 b2 =  LT
-let ~{ocaml} directionLessEq b1 b2    = directionCompare b1 b2 <> GT
-let ~{ocaml} directionGreater b1 b2   = directionCompare b1 b2 =  GT
-let ~{ocaml} directionGreaterEq b1 b2 = directionCompare b1 b2 <> LT
-
-let inline {ocaml} directionLess      = defaultLess
-let inline {ocaml} directionLessEq    = defaultLessEq
-let inline {ocaml} directionGreater   = defaultGreater
-let inline {ocaml} directionGreaterEq = defaultGreaterEq
-
-instance (Ord direction)
-  let compare = directionCompare
-  let (<)  = directionLess
-  let (<=) = directionLessEq
-  let (>)  = directionGreater
-  let (>=) = directionGreaterEq
-end
-
-instance (Show direction)
-  let show = function D_increasing -> "D_increasing" | D_decreasing  -> "D_decreasing" end
-end
-
-let ~{ocaml} register_valueCompare rv1 rv2 =
-  compare (rv1.rv_bits, rv1.rv_dir, rv1.rv_start, rv1.rv_start_internal)
-          (rv2.rv_bits, rv2.rv_dir, rv2.rv_start, rv2.rv_start_internal)
-let inline {ocaml} register_valueCompare = defaultCompare
-
-let ~{ocaml} register_valueLess b1 b2      = register_valueCompare b1 b2 =  LT
-let ~{ocaml} register_valueLessEq b1 b2    = register_valueCompare b1 b2 <> GT
-let ~{ocaml} register_valueGreater b1 b2   = register_valueCompare b1 b2 =  GT
-let ~{ocaml} register_valueGreaterEq b1 b2 = register_valueCompare b1 b2 <> LT
-
-let inline {ocaml} register_valueLess      = defaultLess
-let inline {ocaml} register_valueLessEq    = defaultLessEq
-let inline {ocaml} register_valueGreater   = defaultGreater
-let inline {ocaml} register_valueGreaterEq = defaultGreaterEq
-
-instance (Ord register_value)
-  let compare = register_valueCompare
-  let (<)  = register_valueLess
-  let (<=) = register_valueLessEq
-  let (>)  = register_valueGreater
-  let (>=) = register_valueGreaterEq
-end
-
-let address_liftedCompare (Address_lifted b1 i1) (Address_lifted b2 i2) =
-  compare (i1,b1) (i2,b2)
-(* this cannot be defaultCompare for OCaml because address_lifteds contain big
-   ints *)
-
-let address_liftedLess b1 b2      = address_liftedCompare b1 b2 =  LT
-let address_liftedLessEq b1 b2    = address_liftedCompare b1 b2 <> GT
-let address_liftedGreater b1 b2   = address_liftedCompare b1 b2 =  GT
-let address_liftedGreaterEq b1 b2 = address_liftedCompare b1 b2 <> LT
-
-instance (Ord address_lifted)
-  let compare = address_liftedCompare
-  let (<)  = address_liftedLess
-  let (<=) = address_liftedLessEq
-  let (>)  = address_liftedGreater
-  let (>=) = address_liftedGreaterEq
-end
-
-(* Registers *)
-type slice = (nat * nat)
-
-type reg_name = 
-  (* do we really need this here if ppcmem already has this information by itself? *)
-| Reg of string * nat * nat * direction
-(*Name of the register, accessing the entire register, the start and size of this register, and its direction *)
-
-| Reg_slice of string * nat * direction * slice 
-(* Name of the register, accessing from the bit indexed by the first
-to the bit indexed by the second integer of the slice, inclusive. For
-machineDef* the first is a smaller number or equal to the second, adjusted
-to reflect the correct span direction in the interpreter side.  *)
-
-| Reg_field of string * nat * direction * string * slice 
-(*Name of the register, start and direction, and name of the field of the register
-accessed. The slice specifies where this field is in the register*)
-
-| Reg_f_slice of string * nat * direction * string * slice * slice 
-(* The first four components are as in Reg_field; the final slice
-specifies a part of the field, indexed w.r.t. the register as a whole *)
-
-let register_base_name : reg_name -> string = function
-  | Reg s _ _ _             -> s
-  | Reg_slice s _ _ _       -> s
-  | Reg_field s _ _ _ _     -> s
-  | Reg_f_slice s _ _ _ _ _ -> s
-  end
-
-let slice_of_reg_name : reg_name -> slice = function
-  | Reg _ start width D_increasing -> (start, start + width -1)
-  | Reg _ start width D_decreasing -> (start - width - 1, start)
-  | Reg_slice _ _ _ sl             -> sl
-  | Reg_field _ _ _ _ sl           -> sl
-  | Reg_f_slice _ _ _ _ _ sl       -> sl
-  end
-
-let width_of_reg_name (r: reg_name) : nat =
-  let width_of_slice (i, j) = (* j - i + 1 in *)
-
-    (integerFromNat j) - (integerFromNat i) + 1
-    $> abs $> natFromInteger
-  in
-  match r with
-  | Reg _ _ width _          -> width
-  | Reg_slice _ _ _ sl       -> width_of_slice sl
-  | Reg_field _ _ _ _ sl     -> width_of_slice sl
-  | Reg_f_slice _ _ _ _ _ sl -> width_of_slice sl
-  end
-
-let reg_name_non_empty_intersection (r: reg_name) (r': reg_name) : bool = 
-  register_base_name r = register_base_name r' &&
-  let (i1,  i2)  = slice_of_reg_name r in
-  let (i1', i2') = slice_of_reg_name r' in
-  i1' <= i2 && i2' >= i1
-
-let reg_nameCompare r1 r2 = 
-  compare (register_base_name r1,slice_of_reg_name r1)
-          (register_base_name r2,slice_of_reg_name r2)
-
-let reg_nameLess b1 b2      = reg_nameCompare b1 b2 =  LT
-let reg_nameLessEq b1 b2    = reg_nameCompare b1 b2 <> GT
-let reg_nameGreater b1 b2   = reg_nameCompare b1 b2 =  GT
-let reg_nameGreaterEq b1 b2 = reg_nameCompare b1 b2 <> LT
-
-instance (Ord reg_name)
-  let compare = reg_nameCompare
-  let (<)  = reg_nameLess
-  let (<=) = reg_nameLessEq
-  let (>)  = reg_nameGreater
-  let (>=) = reg_nameGreaterEq
-end
-
-let {coq;ocaml} reg_nameEqual a1 a2 = (reg_nameCompare a1 a2) = EQ
-let {hol;isabelle} reg_nameEqual = unsafe_structural_equality
-let {coq;ocaml} reg_nameInequal a1 a2 = not (reg_nameEqual a1 a2)
-let {hol;isabelle} reg_nameInequal = unsafe_structural_inequality
-
-instance (Eq reg_name)
-  let (=)  = reg_nameEqual
-  let (<>) = reg_nameInequal
-end
-
-instance (SetType reg_name)
-  let setElemCompare = reg_nameCompare
-end
-
-let direction_of_reg_name r = match r with
-  | Reg _ _ _ d -> d
-  | Reg_slice _ _ d _ -> d
-  | Reg_field _ _ d _ _ -> d
-  | Reg_f_slice _ _ d _ _ _ -> d
- end
-
-let start_of_reg_name r = match r with
-  | Reg _ start _ _ -> start
-  | Reg_slice _ start _ _ -> start
-  | Reg_field _ start _ _ _ -> start
-  | Reg_f_slice _ start _ _ _ _ -> start
-end
-
-(* Data structures for building up instructions *)
-
-(* careful: changes in the read/write/barrier kinds have to be
-   reflected in deep_shallow_convert *)
-type read_kind =
-  (* common reads *)
-  | Read_plain
-  (* Power reads *)
-  | Read_reserve
-  (* AArch64 reads *)
-  | Read_acquire | Read_exclusive | Read_exclusive_acquire | Read_stream
-  (* RISC-V reads *)
-  | Read_RISCV_acquire  | Read_RISCV_strong_acquire
-  | Read_RISCV_reserved | Read_RISCV_reserved_acquire
-  | Read_RISCV_reserved_strong_acquire
-  (* x86 reads *)
-  | Read_X86_locked (* the read part of a lock'd instruction (rmw) *)
-
-instance (Show read_kind)
-  let show = function
-    | Read_plain -> "Read_plain"
-    | Read_reserve -> "Read_reserve"
-    | Read_acquire -> "Read_acquire"
-    | Read_exclusive -> "Read_exclusive"
-    | Read_exclusive_acquire -> "Read_exclusive_acquire"
-    | Read_stream -> "Read_stream"
-    | Read_RISCV_acquire -> "Read_RISCV_acquire"
-    | Read_RISCV_strong_acquire -> "Read_RISCV_strong_acquire"
-    | Read_RISCV_reserved -> "Read_RISCV_reserved"
-    | Read_RISCV_reserved_acquire -> "Read_RISCV_reserved_acquire"
-    | Read_RISCV_reserved_strong_acquire -> "Read_RISCV_reserved_strong_acquire"
-    | Read_X86_locked -> "Read_X86_locked"
-  end
-end
-
-type write_kind =
-  (* common writes *)
-  | Write_plain
-  (* Power writes *)
-  | Write_conditional
-  (* AArch64 writes *)
-  | Write_release | Write_exclusive | Write_exclusive_release
-  (* RISC-V *)
-  | Write_RISCV_release     | Write_RISCV_strong_release
-  | Write_RISCV_conditional | Write_RISCV_conditional_release
-  | Write_RISCV_conditional_strong_release
-  (* x86 writes *)
-  | Write_X86_locked (* the write part of a lock'd instruction (rmw) *)
-
-instance (Show write_kind)
-  let show = function
-    | Write_plain -> "Write_plain"
-    | Write_conditional -> "Write_conditional"
-    | Write_release -> "Write_release"
-    | Write_exclusive -> "Write_exclusive"
-    | Write_exclusive_release -> "Write_exclusive_release"
-    | Write_RISCV_release -> "Write_RISCV_release"
-    | Write_RISCV_strong_release -> "Write_RISCV_strong_release"
-    | Write_RISCV_conditional -> "Write_RISCV_conditional"
-    | Write_RISCV_conditional_release -> "Write_RISCV_conditional_release"
-    | Write_RISCV_conditional_strong_release -> "Write_RISCV_conditional_strong_release"
-    | Write_X86_locked -> "Write_X86_locked"
-  end
-end
-
-type barrier_kind =
-  (* Power barriers *)
-  Barrier_Sync | Barrier_LwSync | Barrier_Eieio | Barrier_Isync
-  (* AArch64 barriers *)
-  | Barrier_DMB | Barrier_DMB_ST | Barrier_DMB_LD | Barrier_DSB
-  | Barrier_DSB_ST | Barrier_DSB_LD | Barrier_ISB
-  | Barrier_TM_COMMIT
-  (* MIPS barriers *)
-  | Barrier_MIPS_SYNC
-  (* RISC-V barriers *)
-  | Barrier_RISCV_rw_rw
-  | Barrier_RISCV_r_rw
-  | Barrier_RISCV_r_r
-  | Barrier_RISCV_rw_w
-  | Barrier_RISCV_w_w
-  | Barrier_RISCV_i
-  (* X86 *)
-  | Barrier_x86_MFENCE
-
-
-instance (Show barrier_kind)
-  let show = function
-    | Barrier_Sync -> "Barrier_Sync"
-    | Barrier_LwSync -> "Barrier_LwSync"
-    | Barrier_Eieio -> "Barrier_Eieio"
-    | Barrier_Isync -> "Barrier_Isync"
-    | Barrier_DMB -> "Barrier_DMB"
-    | Barrier_DMB_ST -> "Barrier_DMB_ST"
-    | Barrier_DMB_LD -> "Barrier_DMB_LD"
-    | Barrier_DSB -> "Barrier_DSB"
-    | Barrier_DSB_ST -> "Barrier_DSB_ST"
-    | Barrier_DSB_LD -> "Barrier_DSB_LD"
-    | Barrier_ISB -> "Barrier_ISB"
-    | Barrier_TM_COMMIT -> "Barrier_TM_COMMIT"
-    | Barrier_MIPS_SYNC -> "Barrier_MIPS_SYNC"
-    | Barrier_RISCV_rw_rw -> "Barrier_RISCV_rw_rw"
-    | Barrier_RISCV_r_rw  -> "Barrier_RISCV_r_rw"
-    | Barrier_RISCV_r_r   -> "Barrier_RISCV_r_r"
-    | Barrier_RISCV_rw_w  -> "Barrier_RISCV_rw_w"
-    | Barrier_RISCV_w_w   -> "Barrier_RISCV_w_w"
-    | Barrier_RISCV_i     -> "Barrier_RISCV_i"
-    | Barrier_x86_MFENCE  -> "Barrier_x86_MFENCE"
-  end
-end
-
-type trans_kind =
-  (* AArch64 *)
-  | Transaction_start | Transaction_commit | Transaction_abort
-
-instance (Show trans_kind)
-  let show = function
-  | Transaction_start  -> "Transaction_start"
-  | Transaction_commit -> "Transaction_commit"
-  | Transaction_abort  -> "Transaction_abort"
-  end
-end
-
-type instruction_kind = 
-  | IK_barrier   of barrier_kind
-  | IK_mem_read  of read_kind
-  | IK_mem_write of write_kind
-  | IK_mem_rmw   of (read_kind * write_kind)
-  | IK_cond_branch
-  (* unconditional branches are not distinguished in the instruction_kind;
-  they just have particular nias (and will be IK_simple *)
-  (* | IK_uncond_branch *)
-  | IK_trans     of trans_kind
-  | IK_simple
-
-
-instance (Show instruction_kind)
-  let show = function
-    | IK_barrier barrier_kind -> "IK_barrier " ^ (show barrier_kind)
-    | IK_mem_read read_kind -> "IK_mem_read " ^ (show read_kind)
-    | IK_mem_write write_kind -> "IK_mem_write " ^ (show write_kind)
-    | IK_cond_branch -> "IK_cond_branch"
-    | IK_trans trans_kind -> "IK_trans " ^ (show trans_kind)
-    | IK_simple -> "IK_simple"
-  end
-end
-
-
-
-let ~{ocaml} read_kindCompare rk1 rk2 =
-  match (rk1, rk2) with
-  | (Read_plain, Read_plain)             -> EQ
-  | (Read_plain, Read_reserve)           -> LT
-  | (Read_plain, Read_acquire)           -> LT
-  | (Read_plain, Read_exclusive)         -> LT
-  | (Read_plain, Read_exclusive_acquire) -> LT
-  | (Read_plain, Read_stream)            -> LT
-
-  | (Read_reserve, Read_plain)             -> GT
-  | (Read_reserve, Read_reserve)           -> EQ
-  | (Read_reserve, Read_acquire)           -> LT
-  | (Read_reserve, Read_exclusive)         -> LT
-  | (Read_reserve, Read_exclusive_acquire) -> LT
-  | (Read_reserve, Read_stream)            -> LT
-
-  | (Read_acquire, Read_plain)             -> GT
-  | (Read_acquire, Read_reserve)           -> GT
-  | (Read_acquire, Read_acquire)           -> EQ
-  | (Read_acquire, Read_exclusive)         -> LT
-  | (Read_acquire, Read_exclusive_acquire) -> LT
-  | (Read_acquire, Read_stream)            -> LT
-
-  | (Read_exclusive, Read_plain)             -> GT
-  | (Read_exclusive, Read_reserve)           -> GT
-  | (Read_exclusive, Read_acquire)           -> GT
-  | (Read_exclusive, Read_exclusive)         -> EQ
-  | (Read_exclusive, Read_exclusive_acquire) -> LT
-  | (Read_exclusive, Read_stream)            -> LT
-
-  | (Read_exclusive_acquire, Read_plain)             -> GT
-  | (Read_exclusive_acquire, Read_reserve)           -> GT
-  | (Read_exclusive_acquire, Read_acquire)           -> GT
-  | (Read_exclusive_acquire, Read_exclusive)         -> GT
-  | (Read_exclusive_acquire, Read_exclusive_acquire) -> EQ
-  | (Read_exclusive_acquire, Read_stream)            -> GT
-
-  | (Read_stream, Read_plain)             -> GT
-  | (Read_stream, Read_reserve)           -> GT
-  | (Read_stream, Read_acquire)           -> GT
-  | (Read_stream, Read_exclusive)         -> GT
-  | (Read_stream, Read_exclusive_acquire) -> GT
-  | (Read_stream, Read_stream)            -> EQ
-end
-let inline {ocaml} read_kindCompare = defaultCompare
-
-let ~{ocaml} read_kindLess b1 b2      = read_kindCompare b1 b2 =  LT
-let ~{ocaml} read_kindLessEq b1 b2    = read_kindCompare b1 b2 <> GT
-let ~{ocaml} read_kindGreater b1 b2   = read_kindCompare b1 b2 =  GT
-let ~{ocaml} read_kindGreaterEq b1 b2 = read_kindCompare b1 b2 <> LT
-
-let inline {ocaml} read_kindLess      = defaultLess
-let inline {ocaml} read_kindLessEq    = defaultLessEq
-let inline {ocaml} read_kindGreater   = defaultGreater
-let inline {ocaml} read_kindGreaterEq = defaultGreaterEq
-
-instance (Ord read_kind)
-  let compare = read_kindCompare
-  let (<)  = read_kindLess
-  let (<=) = read_kindLessEq
-  let (>)  = read_kindGreater
-  let (>=) = read_kindGreaterEq
-end
-
-let ~{ocaml} write_kindCompare wk1 wk2 =
-  match (wk1, wk2) with
-  | (Write_plain, Write_plain)             -> EQ
-  | (Write_plain, Write_conditional)       -> LT
-  | (Write_plain, Write_release)           -> LT
-  | (Write_plain, Write_exclusive)         -> LT
-  | (Write_plain, Write_exclusive_release) -> LT
-
-  | (Write_conditional, Write_plain)             -> GT
-  | (Write_conditional, Write_conditional)       -> EQ
-  | (Write_conditional, Write_release)           -> LT
-  | (Write_conditional, Write_exclusive)         -> LT
-  | (Write_conditional, Write_exclusive_release) -> LT
-
-  | (Write_release, Write_plain)             -> GT
-  | (Write_release, Write_conditional)       -> GT
-  | (Write_release, Write_release)           -> EQ
-  | (Write_release, Write_exclusive)         -> LT
-  | (Write_release, Write_exclusive_release) -> LT
-
-  | (Write_exclusive, Write_plain)             -> GT
-  | (Write_exclusive, Write_conditional)       -> GT
-  | (Write_exclusive, Write_release)           -> GT
-  | (Write_exclusive, Write_exclusive)         -> EQ
-  | (Write_exclusive, Write_exclusive_release) -> LT
-
-  | (Write_exclusive_release, Write_plain)             -> GT
-  | (Write_exclusive_release, Write_conditional)       -> GT
-  | (Write_exclusive_release, Write_release)           -> GT
-  | (Write_exclusive_release, Write_exclusive)         -> GT
-  | (Write_exclusive_release, Write_exclusive_release) -> EQ
-end
-let inline {ocaml} write_kindCompare = defaultCompare
-
-let ~{ocaml} write_kindLess b1 b2      = write_kindCompare b1 b2 =  LT
-let ~{ocaml} write_kindLessEq b1 b2    = write_kindCompare b1 b2 <> GT
-let ~{ocaml} write_kindGreater b1 b2   = write_kindCompare b1 b2 =  GT
-let ~{ocaml} write_kindGreaterEq b1 b2 = write_kindCompare b1 b2 <> LT
-
-let inline {ocaml} write_kindLess      = defaultLess
-let inline {ocaml} write_kindLessEq    = defaultLessEq
-let inline {ocaml} write_kindGreater   = defaultGreater
-let inline {ocaml} write_kindGreaterEq = defaultGreaterEq
-
-instance (Ord write_kind)
-  let compare = write_kindCompare
-  let (<)  = write_kindLess
-  let (<=) = write_kindLessEq
-  let (>)  = write_kindGreater
-  let (>=) = write_kindGreaterEq
-end
-
-(* Barrier comparison that uses less memory in Isabelle/HOL *)
-let ~{ocaml} barrier_number = function
-    | Barrier_Sync -> (0 : natural)
-    | Barrier_LwSync -> 1
-    | Barrier_Eieio -> 2
-    | Barrier_Isync -> 3
-    | Barrier_DMB -> 4
-    | Barrier_DMB_ST -> 5
-    | Barrier_DMB_LD -> 6
-    | Barrier_DSB -> 7
-    | Barrier_DSB_ST -> 8
-    | Barrier_DSB_LD -> 9
-    | Barrier_ISB -> 10
-    | Barrier_TM_COMMIT -> 11
-    | Barrier_MIPS_SYNC -> 12
-    | Barrier_RISCV_rw_rw -> 13
-    | Barrier_RISCV_r_rw -> 14
-    | Barrier_RISCV_r_r -> 15
-    | Barrier_RISCV_rw_w -> 16
-    | Barrier_RISCV_w_w -> 17
-    | Barrier_RISCV_i -> 18
-    | Barrier_x86_MFENCE -> 19
-  end
-
-let ~{ocaml} barrier_kindCompare bk1 bk2 =
-  let n1 = barrier_number bk1 in
-  let n2 = barrier_number bk2 in
-  if n1 < n2 then LT
-  else if n1 = n2 then EQ
-  else GT
-let inline {ocaml} barrier_kindCompare = defaultCompare
-
-(*let ~{ocaml} barrier_kindCompare bk1 bk2 =
-  match (bk1, bk2) with
-  | (Barrier_Sync, Barrier_Sync) -> EQ
-  | (Barrier_Sync, _) -> LT
-  | (_, Barrier_Sync) -> GT
-
-  | (Barrier_LwSync, Barrier_LwSync) -> EQ
-  | (Barrier_LwSync, _) -> LT
-  | (_, Barrier_LwSync) -> GT
-
-  | (Barrier_Eieio, Barrier_Eieio) -> EQ
-  | (Barrier_Eieio, _) -> LT
-  | (_, Barrier_Eieio) -> GT
-
-  | (Barrier_Isync, Barrier_Isync) -> EQ
-  | (Barrier_Isync, _) -> LT
-  | (_, Barrier_Isync) -> GT
-
-  | (Barrier_DMB, Barrier_DMB) -> EQ
-  | (Barrier_DMB, _) -> LT
-  | (_, Barrier_DMB) -> GT
-
-  | (Barrier_DMB_ST, Barrier_DMB_ST) -> EQ
-  | (Barrier_DMB_ST, _) -> LT
-  | (_, Barrier_DMB_ST) -> GT
-
-  | (Barrier_DMB_LD, Barrier_DMB_LD) -> EQ
-  | (Barrier_DMB_LD, _) -> LT
-  | (_, Barrier_DMB_LD) -> GT
-
-  | (Barrier_DSB, Barrier_DSB) -> EQ
-  | (Barrier_DSB, _) -> LT
-  | (_, Barrier_DSB) -> GT
-
-  | (Barrier_DSB_ST, Barrier_DSB_ST) -> EQ
-  | (Barrier_DSB_ST, _) -> LT
-  | (_, Barrier_DSB_ST) -> GT
-
-  | (Barrier_DSB_LD, Barrier_DSB_LD) -> EQ
-  | (Barrier_DSB_LD, _) -> LT
-  | (_, Barrier_DSB_LD) -> GT
-                          
-  | (Barrier_ISB, Barrier_ISB) -> EQ
-  | (Barrier_ISB, _) -> LT
-  | (_, Barrier_ISB) -> GT
-
-  | (Barrier_TM_COMMIT, Barrier_TM_COMMIT) -> EQ
-  | (Barrier_TM_COMMIT, _) -> LT
-  | (_, Barrier_TM_COMMIT) -> GT
-
-  | (Barrier_MIPS_SYNC, Barrier_MIPS_SYNC) -> EQ
-  (* | (Barrier_MIPS_SYNC, _) -> LT
-  | (_, Barrier_MIPS_SYNC) -> GT *)
-
-  end*)
-
-let ~{ocaml} barrier_kindLess b1 b2      = barrier_kindCompare b1 b2 =  LT
-let ~{ocaml} barrier_kindLessEq b1 b2    = barrier_kindCompare b1 b2 <> GT
-let ~{ocaml} barrier_kindGreater b1 b2   = barrier_kindCompare b1 b2 =  GT
-let ~{ocaml} barrier_kindGreaterEq b1 b2 = barrier_kindCompare b1 b2 <> LT
-
-let inline {ocaml} barrier_kindLess      = defaultLess
-let inline {ocaml} barrier_kindLessEq    = defaultLessEq
-let inline {ocaml} barrier_kindGreater   = defaultGreater
-let inline {ocaml} barrier_kindGreaterEq = defaultGreaterEq
-
-instance (Ord barrier_kind)
-  let compare = barrier_kindCompare
-  let (<)  = barrier_kindLess
-  let (<=) = barrier_kindLessEq
-  let (>)  = barrier_kindGreater
-  let (>=) = barrier_kindGreaterEq
-end
-
-type event = 
-  | E_read_mem of read_kind * address_lifted * nat * maybe (list reg_name)
-  | E_read_memt of read_kind * address_lifted * nat * maybe (list reg_name)
-  | E_write_mem of write_kind * address_lifted * nat * maybe (list reg_name) * memory_value * maybe (list reg_name)
-  | E_write_ea of write_kind * address_lifted * nat * maybe (list reg_name)
-  | E_excl_res
-  | E_write_memv of maybe address_lifted * memory_value * maybe (list reg_name)
-  | E_write_memvt of maybe address_lifted * (bit_lifted * memory_value) * maybe (list reg_name)
-  | E_barrier of barrier_kind
-  | E_footprint 
-  | E_read_reg of reg_name
-  | E_write_reg of reg_name * register_value
-  | E_escape
-  | E_error of string 
-
-
-let eventCompare e1 e2 = 
-  match (e1,e2) with
-  | (E_read_mem rk1 v1 i1 tr1, E_read_mem rk2 v2 i2 tr2) ->
-     compare (rk1, (v1,i1,tr1)) (rk2,(v2, i2, tr2)) 
-  | (E_read_memt rk1 v1 i1 tr1, E_read_memt rk2 v2 i2 tr2) ->
-     compare (rk1, (v1,i1,tr1)) (rk2,(v2, i2, tr2)) 
-  | (E_write_mem wk1 v1 i1 tr1 v1' tr1', E_write_mem wk2 v2 i2 tr2 v2' tr2') -> 
-    compare ((wk1,v1,i1),(tr1,v1',tr1'))  ((wk2,v2,i2),(tr2,v2',tr2')) 
-  | (E_write_ea wk1 a1 i1 tr1, E_write_ea wk2 a2 i2 tr2) ->
-    compare (wk1, (a1, i1, tr1)) (wk2, (a2, i2, tr2))
-  | (E_excl_res, E_excl_res) -> EQ
-  | (E_write_memv _ mv1 tr1, E_write_memv _ mv2 tr2) -> compare (mv1,tr1) (mv2,tr2)
-  | (E_write_memvt _ mv1 tr1, E_write_memvt _ mv2 tr2) -> compare (mv1,tr1) (mv2,tr2)
-  | (E_barrier bk1, E_barrier bk2) -> compare bk1 bk2
-  | (E_read_reg r1, E_read_reg r2) -> compare r1 r2
-  | (E_write_reg r1 v1, E_write_reg r2 v2) -> compare (r1,v1) (r2,v2)
-  | (E_error s1, E_error s2) -> compare s1 s2
-  | (E_escape,E_escape) -> EQ
-  | (E_read_mem _ _ _ _, _) -> LT
-  | (E_write_mem _ _ _ _ _ _, _) -> LT
-  | (E_write_ea _ _ _ _, _) -> LT
-  | (E_excl_res, _) -> LT
-  | (E_write_memv _ _ _, _) -> LT
-  | (E_barrier _, _) -> LT
-  | (E_read_reg _, _) -> LT
-  | (E_write_reg _ _, _) -> LT
-  | _ -> GT
-  end
-
-let eventLess b1 b2      = eventCompare b1 b2 =  LT
-let eventLessEq b1 b2    = eventCompare b1 b2 <> GT
-let eventGreater b1 b2   = eventCompare b1 b2 =  GT
-let eventGreaterEq b1 b2 = eventCompare b1 b2 <> LT
-
-instance (Ord event)
-  let compare = eventCompare
-  let (<)  = eventLess
-  let (<=) = eventLessEq
-  let (>)  = eventGreater
-  let (>=) = eventGreaterEq
-end
-
-instance (SetType event)
-  let setElemCompare = compare
-end
-
-
-(* the address_lifted types should go away here and be replaced by address *)
-type with_aux 'o = 'o * maybe ((unit -> (string * string)) * ((list (reg_name * register_value)) -> list event))
-type outcome_r 'a 'r =
-  (* Request to read memory, value is location to read, integer is size to read,
-     followed by registers that were used in computing that size *)
-  | Read_mem of (read_kind * address_lifted * nat) * (memory_value -> with_aux (outcome_r 'a 'r))
-  (* Tell the system a write is imminent, at address lifted, of size nat *)
-  | Write_ea of (write_kind * address_lifted * nat) * (with_aux (outcome_r 'a 'r))
-  (* Request the result of store-exclusive *)
-  | Excl_res of (bool -> with_aux (outcome_r 'a 'r))
-  (* Request to write memory at last signalled address. Memory value should be 8
-     times the size given in ea signal *)
-  | Write_memv of memory_value * (bool -> with_aux (outcome_r 'a 'r))
-  (* Request a memory barrier *)
-  | Barrier of barrier_kind * with_aux (outcome_r 'a 'r)
-  (* Tell the system to dynamically recalculate dependency footprint *)
-  | Footprint of with_aux (outcome_r 'a 'r)
-  (* Request to read register, will track dependency when mode.track_values *)
-  | Read_reg of reg_name * (register_value -> with_aux (outcome_r 'a 'r))
-  (* Request to write register *)
-  | Write_reg of (reg_name * register_value) * with_aux (outcome_r 'a 'r)
-  | Escape of maybe string
-  (*Result of a failed assert with possible error message to report*)
-  | Fail of maybe string
-  (* Early return with value of type 'r *)
-  | Return of 'r
-  | Internal of (maybe string * maybe (unit -> string)) * with_aux (outcome_r 'a 'r)
-  | Done of 'a
-  | Error of string
-
-type outcome 'a = outcome_r 'a unit
-type outcome_s 'a = with_aux (outcome 'a)
-(* first string : output of instruction_stack_to_string
-   second string: output of local_variables_to_string *)
-
-(** operations and coercions on basic values *)
-
-val word8_to_bitls : word8 -> list bit_lifted
-val bitls_to_word8 : list bit_lifted -> word8
-
-val integer_of_word8_list : list word8 -> integer
-val word8_list_of_integer : integer -> integer -> list word8 
-
-val concretizable_bitl : bit_lifted -> bool
-val concretizable_bytl : byte_lifted -> bool
-val concretizable_bytls : list byte_lifted -> bool
-
-let concretizable_bitl = function
-  | Bitl_zero -> true
-  | Bitl_one -> true
-  | Bitl_undef -> false
-  | Bitl_unknown -> false
-end 
-
-let concretizable_bytl (Byte_lifted bs) = List.all concretizable_bitl bs
-let concretizable_bytls = List.all concretizable_bytl
-
-(* constructing values *)
-
-val build_register_value : list bit_lifted -> direction -> nat -> nat -> register_value
-let build_register_value bs dir width start_index =
-  <| rv_bits = bs;
-     rv_dir = dir; (* D_increasing for Power, D_decreasing for ARM *)
-     rv_start_internal = start_index; 
-     rv_start = if dir = D_increasing
-       then start_index
-       else (start_index+1) - width; (* Smaller index, as in Power, for external interaction *)
-  |>
-
-val register_value : bit_lifted -> direction -> nat -> nat -> register_value
-let register_value b dir width start_index = 
-  build_register_value (List.replicate width b) dir width start_index
-
-val register_value_zeros : direction -> nat -> nat -> register_value
-let register_value_zeros dir width start_index = 
-  register_value Bitl_zero dir width start_index
-
-val register_value_ones : direction -> nat -> nat -> register_value
-let register_value_ones dir width start_index = 
-  register_value Bitl_one dir width start_index
-
-val register_value_for_reg : reg_name -> list bit_lifted -> register_value
-let register_value_for_reg r bs : register_value =
-  let () = ensure (width_of_reg_name r = List.length bs)
-      ("register_value_for_reg (\"" ^ show (register_base_name r) ^ "\") length mismatch: "
-          ^ show (width_of_reg_name r) ^ " vs " ^ show (List.length bs))
-  in
-  let (j1, j2) = slice_of_reg_name r in
-  let d = direction_of_reg_name r in
-  <|  rv_bits = bs;
-      rv_dir = d;
-      rv_start_internal = if d = D_increasing then j1 else (start_of_reg_name r) - j1;
-      rv_start = j1;
-  |>
-
-val byte_lifted_undef : byte_lifted
-let byte_lifted_undef = Byte_lifted (List.replicate 8 Bitl_undef)
-
-val byte_lifted_unknown : byte_lifted
-let byte_lifted_unknown = Byte_lifted (List.replicate 8 Bitl_unknown)
-  
-val memory_value_unknown : nat (*the number of bytes*) -> memory_value
-let memory_value_unknown (width:nat) : memory_value = 
-  List.replicate width byte_lifted_unknown 
-
-val memory_value_undef : nat (*the number of bytes*) -> memory_value
-let memory_value_undef (width:nat) : memory_value = 
-  List.replicate width byte_lifted_undef 
-
-val match_endianness : forall 'a. end_flag -> list 'a -> list 'a
-let match_endianness endian l =
-  match endian with
-  | E_little_endian -> List.reverse l
-  | E_big_endian    -> l
-  end
-
-(* lengths *)  
-
-val memory_value_length : memory_value -> nat
-let memory_value_length (mv:memory_value) = List.length mv
-
-
-(* aux fns *)
-
-val maybe_all : forall 'a.  list (maybe 'a) -> maybe (list 'a)
-let rec maybe_all' xs acc = 
-  match xs with
-  | [] -> Just (List.reverse acc)
-  | Nothing :: _ -> Nothing
-  | (Just y)::xs' -> maybe_all' xs' (y::acc)
-  end
-let maybe_all xs = maybe_all' xs [] 
-
-(** coercions *)
-
-(* bits and bytes *)
-
-let bit_to_bool = function (* TODO: rename bool_of_bit *)
-  | Bitc_zero -> false
-  | Bitc_one -> true
-end
-
-
-val bit_lifted_of_bit : bit -> bit_lifted
-let bit_lifted_of_bit b = 
-  match b with
-  | Bitc_zero -> Bitl_zero
-  | Bitc_one -> Bitl_one
-  end
-
-val bit_of_bit_lifted : bit_lifted -> maybe bit
-let bit_of_bit_lifted bl =
-  match bl with
-  | Bitl_zero -> Just Bitc_zero
-  | Bitl_one -> Just Bitc_one
-  | Bitl_undef -> Nothing
-  | Bitl_unknown -> Nothing
-  end
-
-
-val byte_lifted_of_byte : byte -> byte_lifted
-let byte_lifted_of_byte (Byte bs) : byte_lifted = Byte_lifted (List.map bit_lifted_of_bit bs)
-
-val byte_of_byte_lifted : byte_lifted -> maybe byte
-let byte_of_byte_lifted bl = 
-  match bl with
-  | Byte_lifted bls -> 
-      match maybe_all (List.map bit_of_bit_lifted bls) with
-      | Nothing -> Nothing
-      | Just bs -> Just (Byte bs)
-      end
-  end
-
-
-val bytes_of_bits : list bit -> list byte (*assumes (length bits) mod 8 = 0*)
-let rec bytes_of_bits bits = match bits with
-  | [] -> []
-  | b0::b1::b2::b3::b4::b5::b6::b7::bits -> 
-    (Byte [b0;b1;b2;b3;b4;b5;b6;b7])::(bytes_of_bits bits)
-  | _ -> failwith "bytes_of_bits not given bits divisible by 8"
-end
-
-val byte_lifteds_of_bit_lifteds : list bit_lifted -> list byte_lifted (*assumes (length bits) mod 8 = 0*)
-let rec byte_lifteds_of_bit_lifteds bits = match bits with
-  | [] -> []
-  | b0::b1::b2::b3::b4::b5::b6::b7::bits -> 
-    (Byte_lifted [b0;b1;b2;b3;b4;b5;b6;b7])::(byte_lifteds_of_bit_lifteds bits)
-  | _ -> failwith "byte_lifteds of bit_lifteds not given bits divisible by 8"
-end
-
-
-val byte_of_memory_byte : memory_byte -> maybe byte
-let byte_of_memory_byte = byte_of_byte_lifted
-
-val memory_byte_of_byte : byte -> memory_byte
-let memory_byte_of_byte = byte_lifted_of_byte
-
-
-(* to and from nat *)
-
-(* this natFromBoolList could move to the Lem word.lem library *)
-val natFromBoolList : list bool -> nat
-let rec natFromBoolListAux (acc : nat) (bl : list bool) = 
-  match bl with 
-    | [] -> acc
-    | (true :: bl') -> natFromBoolListAux ((acc * 2) + 1) bl'
-    | (false :: bl') -> natFromBoolListAux (acc * 2) bl'
-  end
-let natFromBoolList bl = 
-  natFromBoolListAux 0 (List.reverse bl)
-
-
-val nat_of_bit_list : list bit -> nat 
-let nat_of_bit_list b =
-  natFromBoolList (List.reverse (List.map bit_to_bool b))
-  (* natFromBoolList takes a list with LSB first, for consistency with rest of Lem word library, so we reverse it. twice. *)
-
-
-(* to and from integer *)
-
-val integer_of_bit_list : list bit -> integer 
-let integer_of_bit_list b =
-  integerFromBoolList (false,(List.reverse (List.map bit_to_bool b)))
-  (* integerFromBoolList takes a list with LSB first, so we reverse it *)
-
-val bit_list_of_integer : nat -> integer -> list bit 
-let bit_list_of_integer len b = 
-  List.map (fun b -> if b then Bitc_one else Bitc_zero) 
-    (reverse (boolListFrombitSeq len (bitSeqFromInteger Nothing b)))
-
-val integer_of_byte_list : list byte -> integer 
-let integer_of_byte_list bytes = integer_of_bit_list (List.concatMap (fun (Byte bs) -> bs) bytes)
-
-val byte_list_of_integer : nat -> integer -> list byte 
-let byte_list_of_integer (len:nat) (a:integer):list byte = 
-  let bits = bit_list_of_integer (len * 8) a in bytes_of_bits bits
-
-
-val integer_of_address : address -> integer 
-let integer_of_address (a:address):integer = 
-  match a with
-  | Address bs i -> i 
-  end
-
-val address_of_integer : integer -> address 
-let address_of_integer (i:integer):address =
-  Address (byte_list_of_integer 8 i) i
-
-(* to and from signed-integer *)
-
-val signed_integer_of_bit_list : list bit -> integer
-let signed_integer_of_bit_list b =
-  match b with
-  | [] -> failwith "empty bit list"
-  | Bitc_zero :: b' ->
-      integerFromBoolList (false,(List.reverse (List.map bit_to_bool b)))
-  | Bitc_one :: b' ->
-      let b'_val = integerFromBoolList (false,(List.reverse (List.map bit_to_bool b'))) in
-      (* integerFromBoolList takes a list with LSB first, so we reverse it *)
-      let msb_val = integerPow 2 ((List.length b) - 1) in
-      b'_val - msb_val
-  end
-
-
-(* regarding a list of int as a list of bytes in memory, MSB lowest-address first, convert to an integer *)
-val integer_address_of_int_list : list int -> integer
-let rec integerFromIntListAux (acc: integer) (is: list int) = 
-  match is with 
-  | [] -> acc
-  | (i :: is') -> integerFromIntListAux ((acc * 256) + integerFromInt i) is'
-  end
-let integer_address_of_int_list (is: list int) =
-  integerFromIntListAux 0 is
-
-val address_of_byte_list : list byte -> address 
-let address_of_byte_list bs = 
-  if List.length bs <> 8 then failwith "address_of_byte_list given list not of length 8" else 
-  Address bs (integer_of_byte_list bs)
-
-let address_of_byte_lifted_list bls =
-  match maybe_all (List.map byte_of_byte_lifted bls) with
-  | Nothing -> Nothing
-  | Just bs -> Just (address_of_byte_list bs)
-  end
-
-(* operations on addresses *)
-
-val add_address_nat : address -> nat -> address 
-let add_address_nat (a:address) (i:nat) : address = 
-  address_of_integer ((integer_of_address a) + (integerFromNat i))
-
-val clear_low_order_bits_of_address : address -> address 
-let clear_low_order_bits_of_address a = 
-  match a with 
-  | Address [b0;b1;b2;b3;b4;b5;b6;b7] i -> 
-      match b7 with
-      | Byte [bt0;bt1;bt2;bt3;bt4;bt5;bt6;bt7] -> 
-          let b7' = Byte [bt0;bt1;bt2;bt3;bt4;bt5;Bitc_zero;Bitc_zero] in
-	  let bytes = [b0;b1;b2;b3;b4;b5;b6;b7'] in
-          Address bytes (integer_of_byte_list bytes)
-      | _ -> failwith "Byte does not contain 8 bits"
-      end
-  | _ -> failwith "Address does not contain 8 bytes"
-  end
-
-
-
-val byte_list_of_memory_value : end_flag -> memory_value -> maybe (list byte)
-let byte_list_of_memory_value endian mv =
-  match_endianness endian mv
-  $> List.map byte_of_memory_byte
-  $> maybe_all
-
-
-val integer_of_memory_value : end_flag -> memory_value -> maybe integer
-let integer_of_memory_value endian (mv:memory_value):maybe integer =
-  match byte_list_of_memory_value endian mv with
-  | Just bs -> Just (integer_of_byte_list bs)
-  | Nothing -> Nothing 
-  end
-
-val memory_value_of_integer : end_flag  -> nat -> integer -> memory_value
-let memory_value_of_integer endian (len:nat) (i:integer):memory_value =
-  List.map byte_lifted_of_byte (byte_list_of_integer len i)
-  $> match_endianness endian
-
-
-val integer_of_register_value : register_value -> maybe integer 
-let integer_of_register_value (rv:register_value):maybe integer = 
-  match maybe_all (List.map bit_of_bit_lifted rv.rv_bits) with
-  | Nothing -> Nothing
-  | Just bs -> Just (integer_of_bit_list bs)
-  end
-
-(* NOTE: register_value_for_reg_of_integer might be easier to use *)
-val register_value_of_integer : nat -> nat -> direction -> integer -> register_value 
-let register_value_of_integer (len:nat) (start:nat) (dir:direction) (i:integer):register_value =
-  let bs = bit_list_of_integer len i in
-  build_register_value (List.map bit_lifted_of_bit bs) dir len start
-
-val register_value_for_reg_of_integer : reg_name -> integer -> register_value
-let register_value_for_reg_of_integer (r: reg_name) (i:integer) : register_value =
-  register_value_of_integer (width_of_reg_name r) (start_of_reg_name r) (direction_of_reg_name r) i
-
-(* *)
-
-val opcode_of_bytes : byte -> byte -> byte -> byte -> opcode
-let opcode_of_bytes b0 b1 b2 b3 : opcode = Opcode [b0;b1;b2;b3]
-
-val register_value_of_address : address -> direction -> register_value   
-let register_value_of_address (Address bytes _) dir : register_value = 
-  let bits = List.concatMap (fun (Byte bs) -> List.map bit_lifted_of_bit bs) bytes in
-   <| rv_bits = bits;
-      rv_dir = dir;
-      rv_start = 0; 
-      rv_start_internal = if dir = D_increasing then 0 else (List.length bits) - 1
-   |>
-
-val register_value_of_memory_value : memory_value -> direction -> register_value
-let register_value_of_memory_value bytes dir : register_value =
-  let bitls = List.concatMap (fun (Byte_lifted bs) -> bs) bytes in
-  <| rv_bits = bitls;
-     rv_dir = dir;
-     rv_start = 0;
-     rv_start_internal = if dir = D_increasing then 0 else (List.length bitls) - 1
-   |>                                                     
-
-val memory_value_of_register_value: register_value -> memory_value
-let memory_value_of_register_value r =
-  (byte_lifteds_of_bit_lifteds r.rv_bits)
-   
-val address_lifted_of_register_value : register_value -> maybe address_lifted
-(* returning Nothing iff the register value is not 64 bits wide, but
-allowing Bitl_undef and Bitl_unknown *)
-let address_lifted_of_register_value (rv:register_value) : maybe address_lifted = 
-  if List.length rv.rv_bits <> 64 then Nothing
-  else 
-    Just (Address_lifted (byte_lifteds_of_bit_lifteds rv.rv_bits)
-                         (if List.all concretizable_bitl rv.rv_bits 
-			  then match (maybe_all (List.map bit_of_bit_lifted rv.rv_bits)) with
-                              | (Just(bits)) -> Just (integer_of_bit_list bits)
-                              | Nothing -> Nothing end
-			  else Nothing))
-
-val address_of_address_lifted : address_lifted -> maybe address
-(* returning Nothing iff the address contains any Bitl_undef or Bitl_unknown *)
-let address_of_address_lifted (al:address_lifted): maybe address =
-  match al with
-  | Address_lifted bls (Just i)-> 
-      match maybe_all ((List.map byte_of_byte_lifted) bls) with
-      | Nothing -> Nothing
-      | Just bs -> Just (Address bs i)
-      end
-  | _ -> Nothing
-end
-
-val address_of_register_value : register_value -> maybe address
-(* returning Nothing iff the register value is not 64 bits wide, or contains Bitl_undef or Bitl_unknown *)
-let address_of_register_value (rv:register_value) : maybe address = 
-  match address_lifted_of_register_value rv with
-  | Nothing -> Nothing
-  | Just al -> 
-      match address_of_address_lifted al with
-      | Nothing -> Nothing
-      | Just a -> Just a
-      end
-  end
-
-let address_of_memory_value (endian: end_flag) (mv:memory_value) : maybe address =
-  match byte_list_of_memory_value endian mv with
-  | Nothing -> Nothing
-  | Just bs -> 
-      if List.length bs <> 8 then Nothing else
-      Just (address_of_byte_list bs)
-  end 
-
-val byte_of_int : int -> byte
-let byte_of_int (i:int) : byte = 
-  Byte (bit_list_of_integer 8 (integerFromInt i))
-
-val memory_byte_of_int : int -> memory_byte
-let memory_byte_of_int (i:int) : memory_byte = 
-  memory_byte_of_byte (byte_of_int i)
-
-(*
-val int_of_memory_byte : int -> maybe memory_byte
-let int_of_memory_byte (mb:memory_byte) : int = 
-  failwith "TODO"
-*)
-
-
-
-val memory_value_of_address_lifted : end_flag -> address_lifted -> memory_value
-let memory_value_of_address_lifted endian (Address_lifted bs _ :address_lifted) =
-  match_endianness endian bs
-
-val byte_list_of_address : address -> list byte
-let byte_list_of_address (Address bs _) : list byte = bs
-
-val memory_value_of_address : end_flag -> address -> memory_value
-let memory_value_of_address endian (Address bs _) =
-  match_endianness endian bs
-  $> List.map byte_lifted_of_byte
-
-val byte_list_of_opcode : opcode -> list byte
-let byte_list_of_opcode (Opcode bs) : list byte = bs
-
-(** ****************************************** *)
-(** show type class instantiations             *)
-(** ****************************************** *)
-
-(* matching printing_functions.ml *)
-val stringFromReg_name : reg_name -> string
-let stringFromReg_name r =
-  let norm_sl start dir (first,second) = (first,second)
-    (* match dir with
-      | D_increasing -> (first,second)
-      | D_decreasing -> (start - first, start - second)
-    end *)
-  in
-  match r with
-  | Reg s start size dir -> s
-  | Reg_slice s start dir sl ->
-      let (first,second) = norm_sl start dir sl in
-      s ^ "[" ^ show first ^ (if (first = second) then "" else ".." ^ (show second)) ^ "]"
-  | Reg_field s start dir f sl ->
-      let (first,second) = norm_sl start dir sl in
-      s ^ "." ^ f ^ " (" ^ (show start) ^ ", " ^ (show dir) ^ ", " ^ (show first) ^ ", " ^ (show second) ^ ")"
-  | Reg_f_slice s start dir f (first1,second1) (first,second) ->
-      let (first,second) =
-        match dir with
-        | D_increasing -> (first,second)
-        | D_decreasing -> (start - first, start - second)
-        end in
-      s ^ "." ^ f ^ "]" ^ show first ^ (if (first = second) then "" else ".." ^ (show second)) ^ "]"
-  end
-
-instance (Show reg_name)
-  let show = stringFromReg_name
-end
-
-
-(* hex pp of integers, adapting the Lem string_extra.lem code *)
-val stringFromNaturalHexHelper : natural -> list char -> list char
-let rec stringFromNaturalHexHelper n acc =
-  if n = 0 then
-    acc
-  else
-    stringFromNaturalHexHelper (n / 16) (String_extra.chr (natFromNatural (let nd = n mod 16 in if nd <=9 then nd + 48 else nd - 10 + 97)) :: acc)
-
-val stringFromNaturalHex : natural -> string
-let (*~{ocaml;hol}*) stringFromNaturalHex n = 
-  if n = 0 then "0" else toString (stringFromNaturalHexHelper n [])
-
-val stringFromIntegerHex : integer -> string
-let (*~{ocaml}*) stringFromIntegerHex i = 
-  if i < 0 then 
-    "-" ^ stringFromNaturalHex (naturalFromInteger i)
-  else
-    stringFromNaturalHex (naturalFromInteger i)
-
-
-let stringFromAddress (Address bs i) = 
-  let i' = integer_of_byte_list bs in
-  if i=i' then
-(*TODO: ideally this should be made to match the src/pp.ml pp_address; the following very roughly matches what's used in the ppcmem UI, enough to make exceptions readable *)
-    if i < 65535 then 
-      show i 
-    else
-      stringFromIntegerHex i
-  else
-    "stringFromAddress bytes and integer mismatch"
-
-instance (Show address)
-  let show = stringFromAddress
-end
-
-let stringFromByte_lifted bl =
-  match byte_of_byte_lifted bl with
-  | Nothing -> "u?"  
-  | Just (Byte bits) -> 
-      let i = integer_of_bit_list bits in
-      show i
-  end
-
-instance (Show byte_lifted)
-  let show = stringFromByte_lifted
-end
-
-(* possible next instruction address options *)
-type nia = 
-  | NIA_successor
-  | NIA_concrete_address of address
-  | NIA_LR   (* "LR0:61 || 0b00" in Power pseudocode *)
-  | NIA_CTR  (* "CTR0:61 || 0b00" in Power pseudocode *)
-  | NIA_register of reg_name (* the address will be in a register,
-                                corresponds to AArch64 BLR, BR, RET
-                                instructions *)
-
-let niaCompare n1 n2 = match (n1,n2) with
-  | (NIA_successor, NIA_successor) -> EQ
-  | (NIA_successor, _) -> LT
-  | (NIA_concrete_address _, NIA_successor) -> GT
-  | (NIA_concrete_address a1, NIA_concrete_address a2) -> compare a1 a2
-  | (NIA_concrete_address _, _) -> LT
-  | (NIA_LR, NIA_successor) -> GT
-  | (NIA_LR, NIA_concrete_address _) -> GT
-  | (NIA_LR, NIA_LR) -> EQ
-  | (NIA_LR, _) -> LT
-  | (NIA_CTR, NIA_successor) -> GT
-  | (NIA_CTR, NIA_concrete_address _) -> GT
-  | (NIA_CTR, NIA_LR) -> GT
-  | (NIA_CTR, NIA_CTR) -> EQ
-  | (NIA_CTR, NIA_register _) -> LT
-  | (NIA_register _, NIA_successor) -> GT
-  | (NIA_register _, NIA_concrete_address _) -> GT
-  | (NIA_register _, NIA_LR) -> GT
-  | (NIA_register _, NIA_CTR) -> GT
-  | (NIA_register r1, NIA_register r2) -> compare r1 r2
-  end
-
-instance (Ord nia)
-  let compare = niaCompare
-  let (<)  n1 n2 = (niaCompare n1 n2) = LT
-  let (<=) n1 n2 = (niaCompare n1 n2) <> GT
-  let (>)  n1 n2 = (niaCompare n1 n2) = GT
-  let (>=) n1 n2 = (niaCompare n1 n2) <> LT
-end
-
-let stringFromNia = function
-  | NIA_successor -> "NIA_successor"
-  | NIA_concrete_address a -> "NIA_concrete_address " ^ show a
-  | NIA_LR -> "NIA_LR"
-  | NIA_CTR -> "NIA_CTR"
-  | NIA_register r -> "NIA_register " ^ show r
-end
-
-instance (Show nia)
-  let show = stringFromNia
-end
-
-type dia =
-  | DIA_none
-  | DIA_concrete_address of address
-  | DIA_register of reg_name
-
-let diaCompare d1 d2 = match (d1, d2) with
-  | (DIA_none, DIA_none) -> EQ
-  | (DIA_none, _) -> LT
-  | (DIA_concrete_address a1, DIA_none) -> GT
-  | (DIA_concrete_address a1, DIA_concrete_address a2) -> compare a1 a2
-  | (DIA_concrete_address a1, _) -> LT
-  | (DIA_register r1, DIA_register r2) -> compare r1 r2
-  | (DIA_register _, _) -> GT
-end
-
-instance (Ord dia)
-  let compare = diaCompare
-  let (<)  n1 n2 = (diaCompare n1 n2) = LT
-  let (<=) n1 n2 = (diaCompare n1 n2) <> GT
-  let (>)  n1 n2 = (diaCompare n1 n2) = GT
-  let (>=) n1 n2 = (diaCompare n1 n2) <> LT
-end
-
-let stringFromDia = function
-  | DIA_none               ->  "DIA_none"
-  | DIA_concrete_address a ->  "DIA_concrete_address " ^ show a
-  | DIA_register r ->  "DIA_delayed_register " ^ show r
-end
-
-instance (Show dia)
-  let show = stringFromDia
-end
diff --git a/src/gen_lib/sail2_deep_shallow_convert.lem b/src/gen_lib/sail2_deep_shallow_convert.lem
index b963e537..2e3543b4 100644
--- a/src/gen_lib/sail2_deep_shallow_convert.lem
+++ b/src/gen_lib/sail2_deep_shallow_convert.lem
@@ -455,17 +455,61 @@ instance (ToFromInterpValue write_kind)
 end
 
 
+let a64_barrier_domainToInterpValue = function
+  | A64_FullShare ->
+    V_ctor (Id_aux (Id "A64_FullShare") Unknown) (T_id "a64_barrier_domain") (C_Enum 0) (toInterpValue ())
+  | A64_InnerShare ->
+    V_ctor (Id_aux (Id "A64_InnerShare") Unknown) (T_id "a64_barrier_domain") (C_Enum 1) (toInterpValue ())
+  | A64_OuterShare ->
+    V_ctor (Id_aux (Id "A64_OuterShare") Unknown) (T_id "a64_barrier_domain") (C_Enum 2) (toInterpValue ())
+  | A64_NonShare ->
+    V_ctor (Id_aux (Id "A64_NonShare") Unknown) (T_id "a64_barrier_domain") (C_Enum 3) (toInterpValue ())
+end
+let rec a64_barrier_domainFromInterpValue v = match v with
+  | V_ctor (Id_aux (Id "A64_FullShare") _) _ _ v -> A64_FullShare
+  | V_ctor (Id_aux (Id "A64_InnerShare") _) _ _ v -> A64_InnerShare
+  | V_ctor (Id_aux (Id "A64_OuterShare") _) _ _ v -> A64_OuterShare
+  | V_ctor (Id_aux (Id "A64_NonShare") _) _ _ v -> A64_NonShare
+  | V_tuple [v] -> a64_barrier_domainFromInterpValue v
+  | v -> failwith ("fromInterpValue a64_barrier_domain: unexpected value. " ^
+                     Interp.debug_print_value v)
+  end
+instance (ToFromInterpValue a64_barrier_domain)
+  let toInterpValue = a64_barrier_domainToInterpValue
+  let fromInterpValue = a64_barrier_domainFromInterpValue
+end
+
+let a64_barrier_typeToInterpValue = function
+  | A64_barrier_all ->
+    V_ctor (Id_aux (Id "A64_barrier_all") Unknown) (T_id "a64_barrier_type") (C_Enum 0) (toInterpValue ())
+  | A64_barrier_LD ->
+    V_ctor (Id_aux (Id "A64_barrier_LD") Unknown) (T_id "a64_barrier_type") (C_Enum 1) (toInterpValue ())
+  | A64_barrier_ST ->
+    V_ctor (Id_aux (Id "A64_barrier_ST") Unknown) (T_id "a64_barrier_type") (C_Enum 2) (toInterpValue ())
+end
+let rec a64_barrier_typeFromInterpValue v = match v with
+  | V_ctor (Id_aux (Id "A64_barrier_all") _) _ _ v -> A64_barrier_all
+  | V_ctor (Id_aux (Id "A64_barrier_LD") _) _ _ v -> A64_barrier_LD
+  | V_ctor (Id_aux (Id "A64_barrier_ST") _) _ _ v -> A64_barrier_ST
+  | V_tuple [v] -> a64_barrier_typeFromInterpValue v
+  | v -> failwith ("fromInterpValue a64_barrier_type: unexpected value. " ^
+                     Interp.debug_print_value v)
+  end
+instance (ToFromInterpValue a64_barrier_type)
+  let toInterpValue = a64_barrier_typeToInterpValue
+  let fromInterpValue = a64_barrier_typeFromInterpValue
+end
+
+
 let barrier_kindToInterpValue = function
   | Barrier_Sync -> V_ctor (Id_aux (Id "Barrier_Sync") Unknown) (T_id "barrier_kind") (C_Enum 0) (toInterpValue ())
   | Barrier_LwSync -> V_ctor (Id_aux (Id "Barrier_LwSync") Unknown) (T_id "barrier_kind") (C_Enum 1) (toInterpValue ())
   | Barrier_Eieio -> V_ctor (Id_aux (Id "Barrier_Eieio") Unknown) (T_id "barrier_kind") (C_Enum 2) (toInterpValue ())
   | Barrier_Isync -> V_ctor (Id_aux (Id "Barrier_Isync") Unknown) (T_id "barrier_kind") (C_Enum 3) (toInterpValue ())
-  | Barrier_DMB -> V_ctor (Id_aux (Id "Barrier_DMB") Unknown) (T_id "barrier_kind") (C_Enum 4) (toInterpValue ())
-  | Barrier_DMB_ST -> V_ctor (Id_aux (Id "Barrier_DMB_ST") Unknown) (T_id "barrier_kind") (C_Enum 5) (toInterpValue ())
-  | Barrier_DMB_LD -> V_ctor (Id_aux (Id "Barrier_DMB_LD") Unknown) (T_id "barrier_kind") (C_Enum 6) (toInterpValue ())
-  | Barrier_DSB -> V_ctor (Id_aux (Id "Barrier_DSB") Unknown) (T_id "barrier_kind") (C_Enum 7) (toInterpValue ())
-  | Barrier_DSB_ST -> V_ctor (Id_aux (Id "Barrier_DSB_ST") Unknown) (T_id "barrier_kind") (C_Enum 8) (toInterpValue ())
-  | Barrier_DSB_LD -> V_ctor (Id_aux (Id "Barrier_DSB_LD") Unknown) (T_id "barrier_kind") (C_Enum 9) (toInterpValue ())
+  | Barrier_DMB (dom,typ) ->
+      V_ctor (Id_aux (Id "Barrier_DMB") Unknown) (T_id "barrier_kind") C_Union (toInterpValue (dom, typ))
+  | Barrier_DSB (dom,typ) ->
+      V_ctor (Id_aux (Id "Barrier_DSB") Unknown) (T_id "barrier_kind") C_Union (toInterpValue (dom, typ))
   | Barrier_ISB -> V_ctor (Id_aux (Id "Barrier_ISB") Unknown) (T_id "barrier_kind") (C_Enum 10) (toInterpValue ())
   | Barrier_TM_COMMIT -> V_ctor (Id_aux (Id "Barrier_TM_COMMIT") Unknown) (T_id "barrier_kind") (C_Enum 11) (toInterpValue ())
   | Barrier_MIPS_SYNC -> V_ctor (Id_aux (Id "Barrier_MIPS_SYNC") Unknown) (T_id "barrier_kind") (C_Enum 12) (toInterpValue ())
@@ -482,12 +526,12 @@ let rec barrier_kindFromInterpValue v = match v with
   | V_ctor (Id_aux (Id "Barrier_LwSync") _) _ _ v -> Barrier_LwSync
   | V_ctor (Id_aux (Id "Barrier_Eieio") _) _ _ v -> Barrier_Eieio
   | V_ctor (Id_aux (Id "Barrier_Isync") _) _ _ v -> Barrier_Isync
-  | V_ctor (Id_aux (Id "Barrier_DMB") _) _ _ v -> Barrier_DMB
-  | V_ctor (Id_aux (Id "Barrier_DMB_ST") _) _ _ v -> Barrier_DMB_ST
-  | V_ctor (Id_aux (Id "Barrier_DMB_LD") _) _ _ v -> Barrier_DMB_LD
-  | V_ctor (Id_aux (Id "Barrier_DSB") _) _ _ v -> Barrier_DSB
-  | V_ctor (Id_aux (Id "Barrier_DSB_ST") _) _ _ v -> Barrier_DSB_ST
-  | V_ctor (Id_aux (Id "Barrier_DSB_LD") _) _ _ v -> Barrier_DSB_LD
+  | V_ctor (Id_aux (Id "Barrier_DMB") _) _ _ v ->
+      let (dom, typ) = fromInterpValue v in
+      Barrier_DMB (dom,typ)
+  | V_ctor (Id_aux (Id "Barrier_DSB") _) _ _ v ->
+      let (dom, typ) = fromInterpValue v in
+      Barrier_DSB (dom,typ)
   | V_ctor (Id_aux (Id "Barrier_ISB") _) _ _ v -> Barrier_ISB
   | V_ctor (Id_aux (Id "Barrier_TM_COMMIT") _) _ _ v -> Barrier_TM_COMMIT
   | V_ctor (Id_aux (Id "Barrier_MIPS_SYNC") _) _ _ v -> Barrier_MIPS_SYNC