Interpreter: don't silently use OCaml externs, only interpreter externs

(Adds 'interpreter' externs as appropriate.)

9 files changed, 486 insertions, 435 deletions

diff --git a/lib/arith.sail b/lib/arith.sail
index 61a1ff76..3a1b0927 100644
--- a/lib/arith.sail
+++ b/lib/arith.sail
@@ -5,19 +5,19 @@ $include <flow.sail>
 
 // ***** Addition *****
 
-val add_atom = {ocaml: "add_int", lem: "integerAdd", c: "add_int", coq: "Z.add"} : forall 'n 'm.
+val add_atom = {ocaml: "add_int", interpreter: "add_int", lem: "integerAdd", c: "add_int", coq: "Z.add"} : forall 'n 'm.
   (int('n), int('m)) -> int('n + 'm)
 
-val add_int = {ocaml: "add_int", lem: "integerAdd", c: "add_int", coq: "Z.add"} : (int, int) -> int
+val add_int = {ocaml: "add_int", interpreter: "add_int", lem: "integerAdd", c: "add_int", coq: "Z.add"} : (int, int) -> int
 
 overload operator + = {add_atom, add_int}
 
 // ***** Subtraction *****
 
-val sub_atom = {ocaml: "sub_int", lem: "integerMinus", c: "sub_int", coq: "Z.sub"} : forall 'n 'm.
+val sub_atom = {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", c: "sub_int", coq: "Z.sub"} : forall 'n 'm.
   (int('n), int('m)) -> int('n - 'm)
 
-val sub_int = {ocaml: "sub_int", lem: "integerMinus", c: "sub_int", coq: "Z.sub"} : (int, int) -> int
+val sub_int = {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", c: "sub_int", coq: "Z.sub"} : (int, int) -> int
 
 overload operator - = {sub_atom, sub_int}
 
@@ -29,18 +29,18 @@ val sub_nat = {
 
 // ***** Negation *****
 
-val negate_atom = {ocaml: "negate", lem: "integerNegate", c: "neg_int", coq: "Z.opp"} : forall 'n. int('n) -> int(- 'n)
+val negate_atom = {ocaml: "negate", interpreter: "negate", lem: "integerNegate", c: "neg_int", coq: "Z.opp"} : forall 'n. int('n) -> int(- 'n)
 
-val negate_int = {ocaml: "negate", lem: "integerNegate", c: "neg_int", coq: "Z.opp"} : int -> int
+val negate_int = {ocaml: "negate", interpreter: "negate", lem: "integerNegate", c: "neg_int", coq: "Z.opp"} : int -> int
 
 overload negate = {negate_atom, negate_int}
 
 // ***** Multiplication *****
 
-val mult_atom = {ocaml: "mult", lem: "integerMult", c: "mult_int", coq: "Z.mul"} : forall 'n 'm.
+val mult_atom = {ocaml: "mult", interpreter: "mult", lem: "integerMult", c: "mult_int", coq: "Z.mul"} : forall 'n 'm.
   (int('n), int('m)) -> int('n * 'm)
 
-val mult_int = {ocaml: "mult", lem: "integerMult", c: "mult_int", coq: "Z.mul"} : (int, int) -> int
+val mult_int = {ocaml: "mult", interpreter: "mult", lem: "integerMult", c: "mult_int", coq: "Z.mul"} : (int, int) -> int
 
 overload operator * = {mult_atom, mult_int}
 
@@ -59,6 +59,7 @@ val shr_int = "shr_int" : (int, int) -> int
 val div_int = {
   smt: "div",
   ocaml: "quotient",
+  interpreter: "quotient",
   lem: "integerDiv",
   c: "tdiv_int",
   coq: "Z.quot"
@@ -69,6 +70,7 @@ overload operator / = {div_int}
 val mod_int = {
   smt: "mod",
   ocaml: "modulus",
+  interpreter: "modulus",
   lem: "integerMod",
   c: "tmod_int",
   coq: "Z.rem"
@@ -79,6 +81,7 @@ overload operator % = {mod_int}
 val abs_int = {
   smt : "abs",
   ocaml: "abs_int",
+  interpreter: "abs_int",
   lem: "abs_int",
   coq: "Z.abs"
 } : (int, int) -> int
diff --git a/lib/elf.sail b/lib/elf.sail
index 2d799d4d..6ea5de19 100644
--- a/lib/elf.sail
+++ b/lib/elf.sail
@@ -3,12 +3,14 @@ $define _ELF
 
 val elf_entry = {
   ocaml: "Elf_loader.elf_entry",
+  interpreter: "Elf_loader.elf_entry",
   lem: "elf_entry",
   c: "elf_entry"
 } : unit -> int
 
 val elf_tohost = {
   ocaml: "Elf_loader.elf_tohost",
+  interpreter: "Elf_loader.elf_tohost",
   lem: "elf_tohost",
   c: "elf_tohost"
 } : unit -> int
diff --git a/lib/flow.sail b/lib/flow.sail
index 5ee9a74a..7c6f1ebb 100644
--- a/lib/flow.sail
+++ b/lib/flow.sail
@@ -21,7 +21,7 @@ val not_bool = {coq: "negb", _: "not"} : bool -> bool
 val and_bool = {coq: "andb", _: "and_bool"} : (bool, bool) -> bool
 val or_bool = {coq: "orb", _: "or_bool"} : (bool, bool) -> bool
 
-val eq_atom = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : forall 'n 'm. (atom('n), atom('m)) -> bool
+val eq_atom = {ocaml: "eq_int", interpreter: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : forall 'n 'm. (atom('n), atom('m)) -> bool
 
 val neq_atom = {lem: "neq", coq: "neq_atom"} : forall 'n 'm. (atom('n), atom('m)) -> bool
 
@@ -41,9 +41,9 @@ val lteq_atom_range = {coq: "leb_range_r", _: "lteq"} : forall 'n 'm 'o. (atom('
 val gt_atom_range = {coq: "gtb_range_r", _: "gt"}     : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool
 val gteq_atom_range = {coq: "geb_range_r", _: "gteq"} : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool
 
-val eq_range = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "eq_range"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> bool
-val eq_int = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : (int, int) -> bool
-val eq_bool = {ocaml: "eq_bool", lem: "eq", c: "eq_bool", coq: "Bool.eqb"} : (bool, bool) -> bool
+val eq_range = {ocaml: "eq_int", interpreter: "eq_int", lem: "eq", c: "eq_int", coq: "eq_range"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> bool
+val eq_int = {ocaml: "eq_int", interpreter: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : (int, int) -> bool
+val eq_bool = {ocaml: "eq_bool", interpreter: "eq_bool", lem: "eq", c: "eq_bool", coq: "Bool.eqb"} : (bool, bool) -> bool
 
 val neq_range = {lem: "neq"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> bool
 function neq_range (x, y) = not_bool(eq_range(x, y))
diff --git a/lib/instr_kinds.sail b/lib/instr_kinds.sail
new file mode 100644
index 00000000..66ef90c6
--- /dev/null
+++ b/lib/instr_kinds.sail
@@ -0,0 +1,28 @@
+union read_kind = {
+  Read_plain : unit,
+  Read_reserve : unit,
+  Read_acquire : unit,
+  Read_exclusive : unit,
+  Read_exclusive_acquire : unit,
+  Read_stream : unit,
+  Read_RISCV_acquire : unit,
+  Read_RISCV_strong_acquire : unit,
+  Read_RISCV_reserved : unit,
+  Read_RISCV_reserved_acquire : unit,
+  Read_RISCV_reserved_strong_acquire : unit,
+  Read_X86_locked : unit
+}
+
+union write_kind = {
+  Write_plain  : unit
+  Write_conditional : unit
+  Write_release : unit
+  Write_exclusive : unit
+  Write_exclusive_release : unit
+  Write_RISCV_release : unit
+  Write_RISCV_strong_release : unit
+  Write_RISCV_conditional : unit
+  Write_RISCV_conditional_release : unit
+  Write_RISCV_conditional_strong_release : unit
+  Write_X86_locked : unit
+}
\ No newline at end of file
diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index 8abcd218..9ac4d1a5 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -9,6 +9,7 @@ val eq_bit = { lem : "eq", _ : "eq_bit" } : (bit, bit) -> bool
 
 val eq_bits = {
   ocaml: "eq_list",
+  interpreter: "eq_list",
   lem: "eq_vec",
   c: "eq_bits",
   coq: "eq_vec"
@@ -20,6 +21,7 @@ val bitvector_length = {coq: "length_mword", _:"length"} : forall 'n. bits('n) -
 
 val vector_length = {
   ocaml: "length",
+  interpreter: "length",
   lem: "length_list",
   c: "length",
   coq: "vec_length"
@@ -39,6 +41,7 @@ val sail_zero_extend = "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('
 
 val truncate = {
   ocaml: "vector_truncate",
+  interpreter: "vector_truncate",
   lem: "vector_truncate",
   coq: "vector_truncate",
   c: "sail_truncate"
@@ -50,7 +53,7 @@ function sail_mask(len, v) = if len <= length(v) then truncate(v, len) else sail
 
 overload operator ^ = {sail_mask}
 
-val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append", coq: "concat_vec"} : forall ('n : Int) ('m : Int).
+val bitvector_concat = {ocaml: "append", interpreter: "append", lem: "concat_vec", c: "append", coq: "concat_vec"} : forall ('n : Int) ('m : Int).
   (bits('n), bits('m)) -> bits('n + 'm)
 
 overload append = {bitvector_concat}
@@ -60,6 +63,7 @@ val "append_64" : forall 'n. (bits('n), bits(64)) -> bits('n + 64)
 
 val bitvector_access = {
   ocaml: "access",
+  interpreter: "access",
   lem: "access_vec_dec",
   coq: "access_vec_dec",
   c: "vector_access"
@@ -67,6 +71,7 @@ val bitvector_access = {
 
 val plain_vector_access = {
   ocaml: "access",
+  interpreter: "access",
   lem: "access_list_dec",
   coq: "vec_access_dec",
   c: "vector_access"
@@ -76,6 +81,7 @@ overload vector_access = {bitvector_access, plain_vector_access}
 
 val bitvector_update = {
   ocaml: "update",
+  interpreter: "update",
   lem: "update_vec_dec",
   coq: "update_vec_dec",
   c: "vector_update"
@@ -83,6 +89,7 @@ val bitvector_update = {
 
 val plain_vector_update = {
   ocaml: "update",
+  interpreter: "update",
   lem: "update_list_dec",
   coq: "vec_update_dec",
   c: "vector_update"
@@ -92,6 +99,7 @@ overload vector_update = {bitvector_update, plain_vector_update}
 
 val add_bits = {
   ocaml: "add_vec",
+  interpreter: "add_vec",
   lem: "add_vec",
   c: "add_bits",
   coq: "add_vec"
@@ -99,6 +107,7 @@ val add_bits = {
 
 val add_bits_int = {
   ocaml: "add_vec_int",
+  interpreter: "add_vec_int",
   lem: "add_vec_int",
   c: "add_bits_int",
   coq: "add_vec_int"
@@ -108,6 +117,7 @@ overload operator + = {add_bits, add_bits_int}
 
 val vector_subrange = {
   ocaml: "subrange",
+  interpreter: "subrange",
   lem: "subrange_vec_dec",
   c: "vector_subrange",
   coq: "subrange_vec_dec"
@@ -116,6 +126,7 @@ val vector_subrange = {
 
 val vector_update_subrange = {
   ocaml: "update_subrange",
+  interpreter: "update_subrange",
   lem: "update_subrange_vec_dec",
   c: "vector_update_subrange",
   coq: "update_subrange_vec_dec"
diff --git a/lib/vector_inc.sail b/lib/vector_inc.sail
index b295c92c..b8e1b91f 100644
--- a/lib/vector_inc.sail
+++ b/lib/vector_inc.sail
@@ -9,6 +9,7 @@ val "eq_bit" : (bit, bit) -> bool
 
 val eq_bits = {
   ocaml: "eq_list",
+  interpreter: "eq_list",
   lem: "eq_vec",
   c: "eq_bits",
   coq: "eq_vec"
@@ -20,6 +21,7 @@ val bitvector_length = {coq: "length_mword", _:"length"} : forall 'n. bits('n) -
 
 val vector_length = {
   ocaml: "length",
+  interpreter: "length",
   lem: "length_list",
   c: "length",
   coq: "length_list"
@@ -37,6 +39,7 @@ val "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
 
 val truncate = {
   ocaml: "vector_truncate",
+  interpreter: "vector_truncate",
   lem: "vector_truncate",
   coq: "vector_truncate",
   c: "truncate"
@@ -48,7 +51,7 @@ function mask(len, v) = if len <= length(v) then truncate(v, len) else zero_exte
 
 overload operator ^ = {mask}
 
-val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append", coq: "concat_vec"} : forall ('n : Int) ('m : Int).
+val bitvector_concat = {ocaml: "append", interpreter: "append", lem: "concat_vec", c: "append", coq: "concat_vec"} : forall ('n : Int) ('m : Int).
   (bits('n), bits('m)) -> bits('n + 'm)
 
 overload append = {bitvector_concat}
@@ -58,6 +61,7 @@ val "append_64" : forall 'n. (bits('n), bits(64)) -> bits('n + 64)
 
 val bitvector_access = {
   ocaml: "access",
+  interpreter: "access",
   lem: "access_vec_inc",
   coq: "access_vec_inc",
   c: "vector_access"
@@ -65,6 +69,7 @@ val bitvector_access = {
 
 val plain_vector_access = {
   ocaml: "access",
+  interpreter: "access",
   lem: "access_list_inc",
   coq: "access_list_inc",
   c: "vector_access"
@@ -74,6 +79,7 @@ overload vector_access = {bitvector_access, plain_vector_access}
 
 val bitvector_update = {
   ocaml: "update",
+  interpreter: "update",
   lem: "update_vec_inc",
   coq: "update_vec_inc",
   c: "vector_update"
@@ -81,6 +87,7 @@ val bitvector_update = {
 
 val plain_vector_update = {
   ocaml: "update",
+  interpreter: "update",
   lem: "update_list_inc",
   coq: "update_list_inc",
   c: "vector_update"
@@ -90,11 +97,12 @@ overload vector_update = {bitvector_update, plain_vector_update}
 
 val add_bits = {
   ocaml: "add_vec",
+  interpreter: "add_vec",
   c: "add_bits"
 } : forall 'n. (bits('n), bits('n)) -> bits('n)
 
 val add_bits_int = {
-  ocaml: "add_vec_int",
+  ocaml: "add_vec_int", interpreter: "add_vec_int",
   c: "add_bits_int"
 } : forall 'n. (bits('n), int) -> bits('n)
 
@@ -102,6 +110,7 @@ overload operator + = {add_bits, add_bits_int}
 
 val vector_subrange = {
   ocaml: "subrange",
+  interpreter: "subrange",
   lem: "subrange_vec_inc",
   c: "vector_subrange",
   coq: "subrange_vec_inc"
@@ -110,6 +119,7 @@ val vector_subrange = {
 
 val vector_update_subrange = {
   ocaml: "update_subrange",
+  interpreter: "update_subrange",
   lem: "update_subrange_vec_inc",
   c: "vector_update_subrange",
   coq: "update_subrange_vec_inc"
diff --git a/riscv/prelude.sail b/riscv/prelude.sail
index 24913719..36f361ea 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -5,6 +5,390 @@ $include <flow.sail>
 type bits ('n : Int) = vector('n, dec, bit)
 union option ('a : Type) = {None : unit, Some : 'a}
 
+$include <regfp.sail>
+
+val eq_atom = {ocaml: "eq_int", interpreter: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : forall 'n 'm. (atom('n), atom('m)) -> bool
+val lteq_atom = {coq: "Z.leb", _: "lteq"} : forall 'n 'm. (atom('n), atom('m)) -> bool
+val gteq_atom = {coq: "Z.geb", _: "gteq"} : forall 'n 'm. (atom('n), atom('m)) -> bool
+val lt_atom = {coq: "Z.ltb", _: "lt"} : forall 'n 'm. (atom('n), atom('m)) -> bool
+val gt_atom = {coq: "Z.gtb", _: "gt"} : forall 'n 'm. (atom('n), atom('m)) -> bool
+
+val eq_int = {ocaml: "eq_int", interpreter: "eq_int", lem: "eq", coq: "Z.eqb", c: "eq_int"} : (int, int) -> bool
+val eq_bit = {ocaml: "eq_bit", lem: "eq", interpreter: "eq_anything", c: "eq_bit", coq: "eq_bit"} : (bit, bit) -> bool
+
+val eq_vec = {ocaml: "eq_list", interpreter: "eq_list", lem: "eq_vec", coq: "eq_vec", c: "eq_bits"} : forall 'n. (bits('n), bits('n)) -> bool
+
+val eq_string = {c: "eq_string", ocaml: "eq_string", interpreter: "eq_string", lem: "eq", coq: "generic_eq"} : (string, string) -> bool
+
+val eq_real = {ocaml: "eq_real", interpreter: "eq_real", lem: "eq"} : (real, real) -> bool
+
+val eq_anything = {ocaml: "(fun (x, y) -> x = y)", interpreter: "eq_anything", lem: "eq", coq: "generic_eq"} : forall ('a : Type). ('a, 'a) -> bool
+
+val bitvector_length = {ocaml: "length", interpreter: "length", lem: "length", coq: "length_mword"} : forall 'n. bits('n) -> atom('n)
+val vector_length = {ocaml: "length", interpreter: "length", lem: "length_list", coq: "vec_length"} : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n)
+val list_length = {ocaml: "length", interpreter: "length", lem: "length_list", coq: "length_list"} : forall ('a : Type). list('a) -> int
+
+overload length = {bitvector_length, vector_length, list_length}
+
+val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
+/* sneaky deref with no effect necessary for bitfield writes */
+val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a
+
+overload operator == = {eq_atom, eq_int, eq_bit, eq_vec, eq_string, eq_real, eq_anything}
+
+val vector_subrange = {
+  ocaml: "subrange", interpreter: "subrange",
+  lem: "subrange_vec_dec",
+  c: "vector_subrange",
+  coq: "subrange_vec_dec"
+} : forall ('n : Int) ('m : Int) ('o : Int), 0 <= 'o <= 'm < 'n.
+  (bits('n), atom('m), atom('o)) -> bits('m - 'o + 1)
+/*
+val vector_subrange = {ocaml: "subrange", interpreter: "subrange", lem: "subrange_vec_dec", coq: "subrange_vec_dec"} : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n.
+  (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1))
+*/
+
+val bitvector_access = {c: "bitvector_access", ocaml: "access", interpreter: "access", lem: "access_vec_dec", coq: "access_vec_dec"} : forall ('n : Int) ('m : Int), 0 <= 'm < 'n.
+  (bits('n), atom('m)) -> bit
+
+val any_vector_access = {ocaml: "access", interpreter: "access", lem: "access_list_dec", coq: "vec_access_dec"} : forall ('n : Int) ('m : Int) ('a : Type), 0 <= 'm < 'n.
+  (vector('n, dec, 'a), atom('m)) -> 'a
+
+overload vector_access = {bitvector_access, any_vector_access}
+
+val bitvector_update = {ocaml: "update", interpreter: "update", lem: "update_vec_dec", coq: "update_vec_dec"} : forall 'n.
+  (bits('n), int, bit) -> bits('n)
+
+val any_vector_update = {ocaml: "update", interpreter: "update", lem: "update_list_dec", coq: "vector_update"} : forall 'n ('a : Type).
+  (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a)
+
+overload vector_update = {bitvector_update, any_vector_update}
+
+val update_subrange = {ocaml: "update_subrange", interpreter: "update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o.
+  (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
+
+val vcons = {lem: "cons_vec"} : forall ('n : Int) ('a : Type).
+  ('a, vector('n, dec, 'a)) -> vector('n + 1, dec, 'a)
+
+val bitvector_concat = {c: "append", ocaml: "append", interpreter: "append", lem: "concat_vec", coq: "concat_vec"} : forall ('n : Int) ('m : Int).
+  (bits('n), bits('m)) -> bits('n + 'm)
+
+val vector_concat = {ocaml: "append", interpreter: "append", lem: "append_list"} : forall ('n : Int) ('m : Int) ('a : Type).
+  (vector('n, dec, 'a), vector('m, dec, 'a)) -> vector('n + 'm, dec, 'a)
+
+overload append = {bitvector_concat, vector_concat}
+
+val not_bool = {coq: "negb", _: "not"} : bool -> bool
+
+val not_vec = {c: "not_bits", _: "not_vec"} : forall 'n. bits('n) -> bits('n)
+
+overload ~ = {not_bool, not_vec}
+
+val neq_vec = {lem: "neq"} : forall 'n. (bits('n), bits('n)) -> bool
+
+function neq_vec (x, y) = not_bool(eq_vec(x, y))
+
+val neq_anything = {lem: "neq", coq: "generic_neq"} : forall ('a : Type). ('a, 'a) -> bool
+
+function neq_anything (x, y) = not_bool(x == y)
+
+overload operator != = {neq_vec, neq_anything}
+
+val and_vec = {lem: "and_vec", c: "and_bits", coq: "and_vec", ocaml: "and_vec", interpreter: "and_vec" } : forall 'n. (bits('n), bits('n)) -> bits('n)
+
+overload operator & = {and_vec}
+
+val or_vec = {lem: "or_vec", c: "or_bits", coq: "or_vec", ocaml: "or_vec", interpreter: "or_vec" } : forall 'n. (bits('n), bits('n)) -> bits('n)
+
+overload operator | = {or_vec}
+
+val unsigned = {ocaml: "uint", interpreter: "uint", lem: "uint", coq: "uint", c: "sail_unsigned"} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1)
+
+val signed = {ocaml: "sint", interpreter: "sint", lem: "sint", coq: "sint", c: "sail_signed"} : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1)
+
+val hex_slice = "hex_slice" : forall 'n 'm, 'n >= 'm. (string, atom('n), atom('m)) -> bits('n - 'm)
+
+val __SetSlice_bits = "set_slice" : forall 'n 'm.
+  (atom('n), atom('m), bits('n), int, bits('m)) -> bits('n)
+
+val __SetSlice_int = "set_slice_int" : forall 'w. (atom('w), int, int, bits('w)) -> int
+
+val __raw_SetSlice_int : forall 'w. (atom('w), int, int, bits('w)) -> int
+
+val __raw_GetSlice_int = "get_slice_int" : forall 'w, 'w >= 0. (atom('w), int, int) -> bits('w)
+
+val __GetSlice_int : forall 'n, 'n >= 0. (atom('n), int, int) -> bits('n)
+
+function __GetSlice_int (n, m, o) = __raw_GetSlice_int(n, m, o)
+
+val __raw_SetSlice_bits : forall 'n 'w.
+  (atom('n), atom('w), bits('n), int, bits('w)) -> bits('n)
+
+val __raw_GetSlice_bits : forall 'n 'w, 'w >= 0.
+  (atom('n), atom('w), bits('n), int) -> bits('w)
+
+val "shiftl" : forall 'm. (bits('m), int) -> bits('m)
+val "shiftr" : forall 'm. (bits('m), int) -> bits('m)
+
+val __SignExtendSlice = {lem: "exts_slice"} : forall 'm. (bits('m), int, int) -> bits('m)
+
+val __ZeroExtendSlice = {lem: "extz_slice"} : forall 'm. (bits('m), int, int) -> bits('m)
+
+val cast cast_unit_vec : bit -> bits(1)
+
+function cast_unit_vec b = match b {
+  bitzero => 0b0,
+  bitone  => 0b1
+}
+
+val print = "print_endline" : string -> unit
+
+val putchar = "putchar" : forall ('a : Type). 'a -> unit
+
+val concat_str = {c: "concat_str", ocaml: "concat_str", interpreter: "concat_str", lem: "stringAppend", coq: "String.append"} : (string, string) -> string
+
+val string_of_int = {c: "string_of_int", ocaml: "string_of_int", interpreter: "string_of_int", lem: "stringFromInteger", coq: "string_of_int"} : int -> string
+
+val DecStr : int -> string
+
+val HexStr : int -> string
+
+val BitStr = "string_of_bits" : forall 'n. bits('n) -> string
+val "decimal_string_of_bits" : forall 'n. bits('n) -> string
+
+val xor_vec = {c: "xor_bits", _: "xor_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+
+val int_power = {ocaml: "int_power", interpreter: "int_power", lem: "pow", coq: "pow", c: "pow_int"} : (int, int) -> int
+
+val real_power = {ocaml: "real_power", interpreter: "real_power", lem: "realPowInteger"} : (real, int) -> real
+
+overload operator ^ = {xor_vec, int_power, real_power, concat_str}
+
+val add_range = {ocaml: "add_int", interpreter: "add_int", c: "add_int", lem: "integerAdd", coq: "add_range"} : forall 'n 'm 'o 'p.
+  (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
+
+val add_int = {ocaml: "add_int", interpreter: "add_int", c: "add_int", lem: "integerAdd", coq: "Z.add"} : (int, int) -> int
+
+val add_vec = {c: "add_bits", _: "add_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+
+val add_vec_int = {c: "add_bits_int", _: "add_vec_int"} : forall 'n. (bits('n), int) -> bits('n)
+
+val add_real = {ocaml: "add_real", interpreter: "add_real", lem: "realAdd"} : (real, real) -> real
+
+overload operator + = {add_range, add_int, add_vec, add_vec_int, add_real}
+
+val sub_range = {ocaml: "sub_int", interpreter: "sub_int", c: "sub_int", lem: "integerMinus", coq: "sub_range"} : forall 'n 'm 'o 'p.
+  (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o)
+
+val sub_int = {ocaml: "sub_int", interpreter: "sub_int", c: "sub_int", lem: "integerMinus", coq: "Z.sub"} : (int, int) -> int
+val sub_nat = {ocaml: "(fun (x,y) -> let n = sub_int (x,y) in if Big_int.less_equal n Big_int.zero then Big_int.zero else n)", interpreter: "(fun (x,y) -> let n = sub_int (x,y) in if Big_int.less_equal n Big_int.zero then Big_int.zero else n)",
+	       lem: "integerMinus", coq: "sub_nat", c: "sub_nat"}
+            : (nat, nat) -> nat
+
+val sub_vec = {c: "sub_bits", _: "sub_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+
+val sub_vec_int = {c: "sub_bits_int", _: "sub_vec_int"} : forall 'n. (bits('n), int) -> bits('n)
+
+val sub_real = {ocaml: "sub_real", interpreter: "sub_real", lem: "realMinus"} : (real, real) -> real
+
+val negate_range = {ocaml: "negate", interpreter: "negate", lem: "integerNegate", coq: "negate_range"} : forall 'n 'm. range('n, 'm) -> range(- 'm, - 'n)
+
+val negate_int = {ocaml: "negate", interpreter: "negate", lem: "integerNegate", coq: "Z.opp"} : int -> int
+
+val negate_real = {ocaml: "Num.minus_num", interpreter: "Num.minus_num", lem: "realNegate"} : real -> real
+
+overload operator - = {sub_range, sub_int, sub_vec, sub_vec_int, sub_real}
+
+overload negate = {negate_range, negate_int, negate_real}
+
+val mult_atom = {ocaml: "mult", interpreter: "mult", lem: "integerMult", c: "mult_int", coq: "Z.mul"} : forall 'n 'm.
+  (atom('n), atom('m)) -> atom('n * 'm)
+
+val mult_int = {ocaml: "mult", interpreter: "mult", lem: "integerMult", coq: "Z.mul"} : (int, int) -> int
+
+val mult_real = {ocaml: "mult_real", interpreter: "mult_real", lem: "realMult"} : (real, real) -> real
+
+overload operator * = {mult_atom, mult_int, mult_real}
+
+val Sqrt = {ocaml: "sqrt_real", interpreter: "sqrt_real", lem: "realSqrt"} : real -> real
+
+val gteq_int = {coq: "Z.geb", _: "gteq"} : (int, int) -> bool
+
+val gteq_real = {ocaml: "gteq_real", interpreter: "gteq_real", lem: "gteq"} : (real, real) -> bool
+
+overload operator >= = {gteq_atom, gteq_int, gteq_real}
+
+val lteq_int = {coq: "Z.leb", _: "lteq"} : (int, int) -> bool
+
+val lteq_real = {ocaml: "lteq_real", interpreter: "lteq_real", lem: "lteq"} : (real, real) -> bool
+
+overload operator <= = {lteq_atom, lteq_int, lteq_real}
+
+val gt_int = {coq: "Z.gtb", _: "gt"} : (int, int) -> bool
+
+val gt_real = {ocaml: "gt_real", interpreter: "gt_real", lem: "gt"} : (real, real) -> bool
+
+overload operator > = {gt_atom, gt_int, gt_real}
+
+val lt_int = {coq: "Z.ltb", _: "lt"} : (int, int) -> bool
+
+val lt_real = {ocaml: "lt_real", interpreter: "lt_real", lem: "lt"} : (real, real) -> bool
+
+overload operator < = {lt_atom, lt_int, lt_real}
+
+val RoundDown = {ocaml: "round_down", interpreter: "round_down", lem: "realFloor"} : real -> int
+
+val RoundUp = {ocaml: "round_up", interpreter: "round_up", lem: "realCeiling"} : real -> int
+
+val abs_int = {ocaml: "abs_int", interpreter: "abs_int", lem: "abs", coq: "Z.abs"} : int -> int
+
+val abs_real = {ocaml: "abs_real", interpreter: "abs_real", lem: "abs"} : real -> real
+
+overload abs = {abs_int, abs_real}
+
+val quotient_nat = {ocaml: "quotient", interpreter: "quotient", lem: "integerDiv"} : (nat, nat) -> nat
+
+val quotient_real = {ocaml: "quotient_real", interpreter: "quotient_real", lem: "realDiv"} : (real, real) -> real
+
+val quotient = {ocaml: "quotient", interpreter: "quotient", lem: "integerDiv"} : (int, int) -> int
+
+overload operator / = {quotient_nat, quotient, quotient_real}
+
+val quot_round_zero = {ocaml: "quot_round_zero", interpreter: "quot_round_zero", lem: "hardware_quot", c: "tdiv_int"} : (int, int) -> int
+val rem_round_zero = {ocaml: "rem_round_zero", interpreter: "rem_round_zero", lem: "hardware_mod", c: "tmod_int"} : (int, int) -> int
+
+val modulus = {ocaml: "modulus", interpreter: "modulus", lem: "hardware_mod", c: "tmod_int"} : (int, int) -> int
+
+overload operator % = {modulus}
+
+val Real = {ocaml: "Num.num_of_big_int", interpreter: "Num.num_of_big_int", lem: "realFromInteger"} : int -> real
+
+val shl_int = "shl_int" : (int, int) -> int
+val shr_int = "shr_int" : (int, int) -> int
+val lor_int = "lor_int" : (int, int) -> int
+val land_int = "land_int" : (int, int) -> int
+val lxor_int = "lxor_int" : (int, int) -> int
+
+val min_nat = {ocaml: "min_int", interpreter: "min_int", lem: "min", c: "min_int"} : (nat, nat) -> nat
+
+val min_int = {ocaml: "min_int", interpreter: "min_int", lem: "min", coq: "Z.min", c: "min_int"} : (int, int) -> int
+
+val max_nat = {ocaml: "max_int", interpreter: "max_int", lem: "max", c: "max_int"} : (nat, nat) -> nat
+
+val max_int = {ocaml: "max_int", interpreter: "max_int", lem: "max", coq: "Z.max", c: "max_int"} : (int, int) -> int
+
+overload min = {min_nat, min_int}
+
+overload max = {max_nat, max_int}
+
+val __TraceMemoryWrite : forall 'n 'm.
+  (atom('n), bits('m), bits(8 * 'n)) -> unit
+
+val __TraceMemoryRead : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit
+
+val replicate_bits = "replicate_bits" : forall 'n 'm, 'm >= 0. (bits('n), atom('m)) -> bits('n * 'm)
+
+val cast ex_nat : nat -> {'n, 'n >= 0. atom('n)}
+
+function ex_nat 'n = n
+
+val cast ex_int : int -> {'n, true. atom('n)}
+
+function ex_int 'n = n
+
+/*
+val cast ex_range : forall 'n 'm. range('n, 'm) -> {'o, 'n <= 'o <= 'm. atom('o)}
+
+function ex_range (n as 'N) = n
+*/
+
+val coerce_int_nat : int -> nat effect {escape}
+
+function coerce_int_nat 'x = {
+  assert(constraint('x >= 0));
+  x
+}
+
+val slice = "slice" : forall ('n : Int) ('m : Int), 'm >= 0 & 'n >= 0.
+  (bits('m), int, atom('n)) -> bits('n)
+
+val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n)
+
+val print_int = "print_int" : (string, int) -> unit
+val print_bits = "print_bits" : forall 'n. (string, bits('n)) -> unit
+val print_string = "print_string" : (string, string) -> unit
+
+val "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
+val "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
+
+val EXTS : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m)
+val EXTZ : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m)
+
+function EXTS v = sign_extend(v, sizeof('m))
+function EXTZ v = zero_extend(v, sizeof('m))
+
+infix 4 <_s
+infix 4 >=_s
+infix 4 <_u
+infix 4 >=_u
+infix 4 <=_u
+
+val operator <_s  : forall 'n, 'n > 0. (bits('n), bits('n)) -> bool
+val operator >=_s : forall 'n, 'n > 0. (bits('n), bits('n)) -> bool
+val operator <_u  : forall 'n. (bits('n), bits('n)) -> bool
+val operator >=_u : forall 'n. (bits('n), bits('n)) -> bool
+val operator <=_u : forall 'n. (bits('n), bits('n)) -> bool
+
+function operator <_s  (x, y) = signed(x) < signed(y)
+function operator >=_s (x, y) = signed(x) >= signed(y)
+function operator <_u  (x, y) = unsigned(x) < unsigned(y)
+function operator >=_u (x, y) = unsigned(x) >= unsigned(y)
+function operator <=_u (x, y) = unsigned(x) <= unsigned(y)
+
+val cast bool_to_bits : bool -> bits(1)
+function bool_to_bits x = if x then 0b1 else 0b0
+
+val cast bit_to_bool : bit -> bool
+function bit_to_bool b = match b {
+  bitone  => true,
+  bitzero => false
+}
+
+infix 7 >>
+infix 7 <<
+
+val operator >> = "shift_bits_right" : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
+val operator << = "shift_bits_left" : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
+
+val vector64 : int -> bits(64)
+
+function vector64 n = __raw_GetSlice_int(64, n, 0)
+
+val to_bits : forall 'l, 'l >= 0.(atom('l), int) -> bits('l)
+function to_bits (l, n) = __raw_GetSlice_int(l, n, 0)
+
+val vector_update_subrange_dec = {ocaml: "update_subrange", interpreter: "update_subrange", c: "vector_update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o.
+  (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
+
+val vector_update_subrange_inc = {ocaml: "update_subrange", interpreter: "update_subrange", lem: "update_subrange_vec_inc"} : forall 'n 'm 'o.
+  (vector('n, inc, bit), atom('m), atom('o), vector('o - ('m - 1), inc, bit)) -> vector('n, inc, bit)
+
+overload vector_update_subrange = {vector_update_subrange_dec, vector_update_subrange_inc}
+
+/* Ideally these would be sail builtin */
+
+function shift_right_arith64 (v : bits(64), shift : bits(6)) -> bits(64) =
+    let v128 : bits(128) = EXTS(v) in
+    (v128 >> shift)[63..0]
+
+function shift_right_arith32 (v : bits(32), shift : bits(5)) -> bits(32) =
+    let v64 : bits(64) = EXTS(v) in
+    (v64 >> shift)[31..0]
+
+/* Special version of zero_extend that the Lem back-end knows will be at a
+   case split on 'm and uses a more generic type for.  (Temporary hack, honest) */
+val zero_extend_type_hack = "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
+
 val spc : unit <-> string
 val opt_spc : unit <-> string
 val def_spc : unit <-> string
@@ -711,423 +1095,6 @@ function hex_bits_64_backwards s =
   }
 
 
-val eq_atom = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : forall 'n 'm. (atom('n), atom('m)) -> bool
-val lteq_atom = {coq: "Z.leb", _: "lteq"} : forall 'n 'm. (atom('n), atom('m)) -> bool
-val gteq_atom = {coq: "Z.geb", _: "gteq"} : forall 'n 'm. (atom('n), atom('m)) -> bool
-val lt_atom = {coq: "Z.ltb", _: "lt"} : forall 'n 'm. (atom('n), atom('m)) -> bool
-val gt_atom = {coq: "Z.gtb", _: "gt"} : forall 'n 'm. (atom('n), atom('m)) -> bool
-
-val eq_int = {ocaml: "eq_int", lem: "eq", coq: "Z.eqb", c: "eq_int"} : (int, int) -> bool
-val eq_bit = {ocaml: "eq_bit", lem: "eq", interpreter: "eq_anything", c: "eq_bit", coq: "eq_bit"} : (bit, bit) -> bool
-
-val eq_vec = {ocaml: "eq_list", lem: "eq_vec", coq: "eq_vec", c: "eq_bits"} : forall 'n. (bits('n), bits('n)) -> bool
-
-val eq_string = {c: "eq_string", ocaml: "eq_string", lem: "eq", coq: "generic_eq"} : (string, string) -> bool
-
-val eq_real = {ocaml: "eq_real", lem: "eq"} : (real, real) -> bool
-
-val eq_anything = {ocaml: "(fun (x, y) -> x = y)", lem: "eq", coq: "generic_eq"} : forall ('a : Type). ('a, 'a) -> bool
-
-val bitvector_length = {ocaml: "length", lem: "length", coq: "length_mword"} : forall 'n. bits('n) -> atom('n)
-val vector_length = {ocaml: "length", lem: "length_list", coq: "vec_length"} : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n)
-val list_length = {ocaml: "length", lem: "length_list", coq: "length_list"} : forall ('a : Type). list('a) -> int
-
-overload length = {bitvector_length, vector_length, list_length}
-
-val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
-/* sneaky deref with no effect necessary for bitfield writes */
-val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a
-
-overload operator == = {eq_atom, eq_int, eq_bit, eq_vec, eq_string, eq_real, eq_anything}
-
-val vector_subrange = {
-  ocaml: "subrange",
-  lem: "subrange_vec_dec",
-  c: "vector_subrange",
-  coq: "subrange_vec_dec"
-} : forall ('n : Int) ('m : Int) ('o : Int), 0 <= 'o <= 'm < 'n.
-  (bits('n), atom('m), atom('o)) -> bits('m - 'o + 1)
-/*
-val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec", coq: "subrange_vec_dec"} : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n.
-  (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1))
-*/
-
-val bitvector_access = {c: "bitvector_access", ocaml: "access", lem: "access_vec_dec", coq: "access_vec_dec"} : forall ('n : Int) ('m : Int), 0 <= 'm < 'n.
-  (bits('n), atom('m)) -> bit
-
-val any_vector_access = {ocaml: "access", lem: "access_list_dec", coq: "vec_access_dec"} : forall ('n : Int) ('m : Int) ('a : Type), 0 <= 'm < 'n.
-  (vector('n, dec, 'a), atom('m)) -> 'a
-
-overload vector_access = {bitvector_access, any_vector_access}
-
-val bitvector_update = {ocaml: "update", lem: "update_vec_dec", coq: "update_vec_dec"} : forall 'n.
-  (bits('n), int, bit) -> bits('n)
-
-val any_vector_update = {ocaml: "update", lem: "update_list_dec", coq: "vector_update"} : forall 'n ('a : Type).
-  (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a)
-
-overload vector_update = {bitvector_update, any_vector_update}
-
-val update_subrange = {ocaml: "update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o.
-  (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
-
-val vcons = {lem: "cons_vec"} : forall ('n : Int) ('a : Type).
-  ('a, vector('n, dec, 'a)) -> vector('n + 1, dec, 'a)
-
-val bitvector_concat = {c: "append", ocaml: "append", lem: "concat_vec", coq: "concat_vec"} : forall ('n : Int) ('m : Int).
-  (bits('n), bits('m)) -> bits('n + 'm)
-
-val vector_concat = {ocaml: "append", lem: "append_list"} : forall ('n : Int) ('m : Int) ('a : Type).
-  (vector('n, dec, 'a), vector('m, dec, 'a)) -> vector('n + 'm, dec, 'a)
-
-overload append = {bitvector_concat, vector_concat}
-
-val not_bool = {coq: "negb", _: "not"} : bool -> bool
-
-val not_vec = {c: "not_bits", _: "not_vec"} : forall 'n. bits('n) -> bits('n)
-
-overload ~ = {not_bool, not_vec}
-
-val neq_vec = {lem: "neq"} : forall 'n. (bits('n), bits('n)) -> bool
-
-function neq_vec (x, y) = not_bool(eq_vec(x, y))
-
-val neq_anything = {lem: "neq", coq: "generic_neq"} : forall ('a : Type). ('a, 'a) -> bool
-
-function neq_anything (x, y) = not_bool(x == y)
-
-overload operator != = {neq_vec, neq_anything}
-
-val and_vec = {lem: "and_vec", c: "and_bits", coq: "and_vec", ocaml: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
-
-overload operator & = {and_vec}
-
-val or_vec = {lem: "or_vec", c: "or_bits", coq: "or_vec", ocaml: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
-
-overload operator | = {or_vec}
-
-val unsigned = {ocaml: "uint", lem: "uint", coq: "uint", c: "sail_unsigned"} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1)
-
-val signed = {ocaml: "sint", lem: "sint", coq: "sint", c: "sail_signed"} : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1)
-
-val hex_slice = "hex_slice" : forall 'n 'm, 'n >= 'm. (string, atom('n), atom('m)) -> bits('n - 'm)
-
-val __SetSlice_bits = "set_slice" : forall 'n 'm.
-  (atom('n), atom('m), bits('n), int, bits('m)) -> bits('n)
-
-val __SetSlice_int = "set_slice_int" : forall 'w. (atom('w), int, int, bits('w)) -> int
-
-val __raw_SetSlice_int : forall 'w. (atom('w), int, int, bits('w)) -> int
-
-val __raw_GetSlice_int = "get_slice_int" : forall 'w, 'w >= 0. (atom('w), int, int) -> bits('w)
-
-val __GetSlice_int : forall 'n, 'n >= 0. (atom('n), int, int) -> bits('n)
-
-function __GetSlice_int (n, m, o) = __raw_GetSlice_int(n, m, o)
-
-val __raw_SetSlice_bits : forall 'n 'w.
-  (atom('n), atom('w), bits('n), int, bits('w)) -> bits('n)
-
-val __raw_GetSlice_bits : forall 'n 'w, 'w >= 0.
-  (atom('n), atom('w), bits('n), int) -> bits('w)
-
-val "shiftl" : forall 'm. (bits('m), int) -> bits('m)
-val "shiftr" : forall 'm. (bits('m), int) -> bits('m)
-
-val __SignExtendSlice = {lem: "exts_slice"} : forall 'm. (bits('m), int, int) -> bits('m)
-
-val __ZeroExtendSlice = {lem: "extz_slice"} : forall 'm. (bits('m), int, int) -> bits('m)
-
-val cast cast_unit_vec : bit -> bits(1)
-
-function cast_unit_vec b = match b {
-  bitzero => 0b0,
-  bitone  => 0b1
-}
-
-val print = "print_endline" : string -> unit
-
-val putchar = "putchar" : forall ('a : Type). 'a -> unit
-
-val concat_str = {c: "concat_str", ocaml: "concat_str", lem: "stringAppend", coq: "String.append"} : (string, string) -> string
-
-val string_of_int = {c: "string_of_int", ocaml: "string_of_int", lem: "stringFromInteger", coq: "string_of_int"} : int -> string
-
-val DecStr : int -> string
-
-val HexStr : int -> string
-
-val BitStr = "string_of_bits" : forall 'n. bits('n) -> string
-val "decimal_string_of_bits" : forall 'n. bits('n) -> string
-
-val xor_vec = {c: "xor_bits", _: "xor_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
-
-val int_power = {ocaml: "int_power", lem: "pow", coq: "pow", c: "pow_int"} : (int, int) -> int
-
-val real_power = {ocaml: "real_power", lem: "realPowInteger"} : (real, int) -> real
-
-overload operator ^ = {xor_vec, int_power, real_power, concat_str}
-
-val add_range = {ocaml: "add_int", c: "add_int", lem: "integerAdd", coq: "add_range"} : forall 'n 'm 'o 'p.
-  (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
-
-val add_int = {ocaml: "add_int", c: "add_int", lem: "integerAdd", coq: "Z.add"} : (int, int) -> int
-
-val add_vec = {c: "add_bits", _: "add_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
-
-val add_vec_int = {c: "add_bits_int", _: "add_vec_int"} : forall 'n. (bits('n), int) -> bits('n)
-
-val add_real = {ocaml: "add_real", lem: "realAdd"} : (real, real) -> real
-
-overload operator + = {add_range, add_int, add_vec, add_vec_int, add_real}
-
-val sub_range = {ocaml: "sub_int", c: "sub_int", lem: "integerMinus", coq: "sub_range"} : forall 'n 'm 'o 'p.
-  (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o)
-
-val sub_int = {ocaml: "sub_int", c: "sub_int", lem: "integerMinus", coq: "Z.sub"} : (int, int) -> int
-val sub_nat = {ocaml: "(fun (x,y) -> let n = sub_int (x,y) in if Big_int.less_equal n Big_int.zero then Big_int.zero else n)",
-	       lem: "integerMinus", coq: "sub_nat", c: "sub_nat"}
-            : (nat, nat) -> nat
-
-val sub_vec = {c: "sub_bits", _: "sub_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
-
-val sub_vec_int = {c: "sub_bits_int", _: "sub_vec_int"} : forall 'n. (bits('n), int) -> bits('n)
-
-val sub_real = {ocaml: "sub_real", lem: "realMinus"} : (real, real) -> real
-
-val negate_range = {ocaml: "negate", lem: "integerNegate", coq: "negate_range"} : forall 'n 'm. range('n, 'm) -> range(- 'm, - 'n)
-
-val negate_int = {ocaml: "negate", lem: "integerNegate", coq: "Z.opp"} : int -> int
-
-val negate_real = {ocaml: "Num.minus_num", lem: "realNegate"} : real -> real
-
-overload operator - = {sub_range, sub_int, sub_vec, sub_vec_int, sub_real}
-
-overload negate = {negate_range, negate_int, negate_real}
-
-val mult_atom = {ocaml: "mult", lem: "integerMult", c: "mult_int", coq: "Z.mul"} : forall 'n 'm.
-  (atom('n), atom('m)) -> atom('n * 'm)
-
-val mult_int = {ocaml: "mult", lem: "integerMult", coq: "Z.mul"} : (int, int) -> int
-
-val mult_real = {ocaml: "mult_real", lem: "realMult"} : (real, real) -> real
-
-overload operator * = {mult_atom, mult_int, mult_real}
-
-val Sqrt = {ocaml: "sqrt_real", lem: "realSqrt"} : real -> real
-
-val gteq_int = {coq: "Z.geb", _: "gteq"} : (int, int) -> bool
-
-val gteq_real = {ocaml: "gteq_real", lem: "gteq"} : (real, real) -> bool
-
-overload operator >= = {gteq_atom, gteq_int, gteq_real}
-
-val lteq_int = {coq: "Z.leb", _: "lteq"} : (int, int) -> bool
-
-val lteq_real = {ocaml: "lteq_real", lem: "lteq"} : (real, real) -> bool
-
-overload operator <= = {lteq_atom, lteq_int, lteq_real}
-
-val gt_int = {coq: "Z.gtb", _: "gt"} : (int, int) -> bool
-
-val gt_real = {ocaml: "gt_real", lem: "gt"} : (real, real) -> bool
-
-overload operator > = {gt_atom, gt_int, gt_real}
-
-val lt_int = {coq: "Z.ltb", _: "lt"} : (int, int) -> bool
-
-val lt_real = {ocaml: "lt_real", lem: "lt"} : (real, real) -> bool
-
-overload operator < = {lt_atom, lt_int, lt_real}
-
-val RoundDown = {ocaml: "round_down", lem: "realFloor"} : real -> int
-
-val RoundUp = {ocaml: "round_up", lem: "realCeiling"} : real -> int
-
-val abs_int = {ocaml: "abs_int", lem: "abs", coq: "Z.abs"} : int -> int
-
-val abs_real = {ocaml: "abs_real", lem: "abs"} : real -> real
-
-overload abs = {abs_int, abs_real}
-
-val quotient_nat = {ocaml: "quotient", lem: "integerDiv"} : (nat, nat) -> nat
-
-val quotient_real = {ocaml: "quotient_real", lem: "realDiv"} : (real, real) -> real
-
-val quotient = {ocaml: "quotient", lem: "integerDiv"} : (int, int) -> int
-
-overload operator / = {quotient_nat, quotient, quotient_real}
-
-val quot_round_zero = {ocaml: "quot_round_zero", lem: "hardware_quot", c: "tdiv_int"} : (int, int) -> int
-val rem_round_zero = {ocaml: "rem_round_zero", lem: "hardware_mod", c: "tmod_int"} : (int, int) -> int
-
-val modulus = {ocaml: "modulus", lem: "hardware_mod", c: "tmod_int"} : (int, int) -> int
-
-overload operator % = {modulus}
-
-val Real = {ocaml: "Num.num_of_big_int", lem: "realFromInteger"} : int -> real
-
-val shl_int = "shl_int" : (int, int) -> int
-val shr_int = "shr_int" : (int, int) -> int
-val lor_int = "lor_int" : (int, int) -> int
-val land_int = "land_int" : (int, int) -> int
-val lxor_int = "lxor_int" : (int, int) -> int
-
-val min_nat = {ocaml: "min_int", lem: "min", c: "min_int"} : (nat, nat) -> nat
-
-val min_int = {ocaml: "min_int", lem: "min", coq: "Z.min", c: "min_int"} : (int, int) -> int
-
-val max_nat = {ocaml: "max_int", lem: "max", c: "max_int"} : (nat, nat) -> nat
-
-val max_int = {ocaml: "max_int", lem: "max", coq: "Z.max", c: "max_int"} : (int, int) -> int
-
-overload min = {min_nat, min_int}
-
-overload max = {max_nat, max_int}
-
-val __WriteRAM = "write_ram" : forall 'n 'm.
-  (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
-
-val __RISCV_write : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> bool effect {wmv}
-function __RISCV_write (addr, width, data) = {
-  __WriteRAM(64, width, 0x0000_0000_0000_0000, addr, data)
-}
-
-val __TraceMemoryWrite : forall 'n 'm.
-  (atom('n), bits('m), bits(8 * 'n)) -> unit
-
-val __ReadRAM = { lem: "MEMr", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
-  (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
-
-val __ReadRAM_acquire = { lem: "MEMr_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
-  (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
-
-val __ReadRAM_strong_acquire = { lem: "MEMr_strong_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
-  (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
-
-val __ReadRAM_reserved = { lem: "MEMr_reserved", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
-  (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
-
-val __ReadRAM_reserved_acquire = { lem: "MEMr_reserved_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
-  (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
-
-val __ReadRAM_reserved_strong_acquire = { lem: "MEMr_reserved_strong_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
-  (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
-
-val __RISCV_read : forall 'n, 'n >= 0. (bits(64), atom('n), bool, bool, bool) -> option(bits(8 * 'n)) effect {rmem}
-function __RISCV_read (addr, width, aq, rl, res) =
-  match (aq, rl, res) {
-    (false, false, false) => Some(__ReadRAM(64, width, 0x0000_0000_0000_0000, addr)),
-    (true,  false, false) => Some(__ReadRAM_acquire(64, width, 0x0000_0000_0000_0000, addr)),
-    (true,  true,  false) => Some(__ReadRAM_strong_acquire(64, width, 0x0000_0000_0000_0000, addr)),
-    (false, false, true)  => Some(__ReadRAM_reserved(64, width, 0x0000_0000_0000_0000, addr)),
-    (true,  false, true)  => Some(__ReadRAM_reserved_acquire(64, width, 0x0000_0000_0000_0000, addr)),
-    (true,  true,  true)  => Some(__ReadRAM_reserved_strong_acquire(64, width, 0x0000_0000_0000_0000, addr)),
-    (false, true,  false) => None(),
-    (false, true,  true)  => None()
-  }
-
-val __TraceMemoryRead : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit
-
-val replicate_bits = "replicate_bits" : forall 'n 'm, 'm >= 0. (bits('n), atom('m)) -> bits('n * 'm)
-
-val cast ex_nat : nat -> {'n, 'n >= 0. atom('n)}
-
-function ex_nat 'n = n
-
-val cast ex_int : int -> {'n, true. atom('n)}
-
-function ex_int 'n = n
-
-/*
-val cast ex_range : forall 'n 'm. range('n, 'm) -> {'o, 'n <= 'o <= 'm. atom('o)}
-
-function ex_range (n as 'N) = n
-*/
-
-val coerce_int_nat : int -> nat effect {escape}
-
-function coerce_int_nat 'x = {
-  assert(constraint('x >= 0));
-  x
-}
-
-val slice = "slice" : forall ('n : Int) ('m : Int), 'm >= 0 & 'n >= 0.
-  (bits('m), int, atom('n)) -> bits('n)
-
-val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n)
-
-val print_int = "print_int" : (string, int) -> unit
-val print_bits = "print_bits" : forall 'n. (string, bits('n)) -> unit
-val print_string = "print_string" : (string, string) -> unit
-
-val "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
-val "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
-
-val EXTS : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m)
-val EXTZ : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m)
-
-function EXTS v = sign_extend(v, sizeof('m))
-function EXTZ v = zero_extend(v, sizeof('m))
-
-infix 4 <_s
-infix 4 >=_s
-infix 4 <_u
-infix 4 >=_u
-infix 4 <=_u
-
-val operator <_s  : forall 'n, 'n > 0. (bits('n), bits('n)) -> bool
-val operator >=_s : forall 'n, 'n > 0. (bits('n), bits('n)) -> bool
-val operator <_u  : forall 'n. (bits('n), bits('n)) -> bool
-val operator >=_u : forall 'n. (bits('n), bits('n)) -> bool
-val operator <=_u : forall 'n. (bits('n), bits('n)) -> bool
-
-function operator <_s  (x, y) = signed(x) < signed(y)
-function operator >=_s (x, y) = signed(x) >= signed(y)
-function operator <_u  (x, y) = unsigned(x) < unsigned(y)
-function operator >=_u (x, y) = unsigned(x) >= unsigned(y)
-function operator <=_u (x, y) = unsigned(x) <= unsigned(y)
-
-val cast bool_to_bits : bool -> bits(1)
-function bool_to_bits x = if x then 0b1 else 0b0
-
-val cast bit_to_bool : bit -> bool
-function bit_to_bool b = match b {
-  bitone  => true,
-  bitzero => false
-}
-
-infix 7 >>
-infix 7 <<
-
-val operator >> = "shift_bits_right" : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
-val operator << = "shift_bits_left" : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
-
-val vector64 : int -> bits(64)
-
-function vector64 n = __raw_GetSlice_int(64, n, 0)
-
-val to_bits : forall 'l, 'l >= 0.(atom('l), int) -> bits('l)
-function to_bits (l, n) = __raw_GetSlice_int(l, n, 0)
-
-val vector_update_subrange_dec = {ocaml: "update_subrange", c: "vector_update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o.
-  (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
-
-val vector_update_subrange_inc = {ocaml: "update_subrange", lem: "update_subrange_vec_inc"} : forall 'n 'm 'o.
-  (vector('n, inc, bit), atom('m), atom('o), vector('o - ('m - 1), inc, bit)) -> vector('n, inc, bit)
-
-overload vector_update_subrange = {vector_update_subrange_dec, vector_update_subrange_inc}
-
-/* Ideally these would be sail builtin */
-
-function shift_right_arith64 (v : bits(64), shift : bits(6)) -> bits(64) =
-    let v128 : bits(128) = EXTS(v) in
-    (v128 >> shift)[63..0]
-
-function shift_right_arith32 (v : bits(32), shift : bits(5)) -> bits(32) =
-    let v64 : bits(64) = EXTS(v) in
-    (v64 >> shift)[31..0]
-
 /* Special version of zero_extend that the Lem back-end knows will be at a
    case split on 'm and uses a more generic type for.  (Temporary hack, honest) */
 val zero_extend_type_hack = "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
diff --git a/src/interpreter.ml b/src/interpreter.ml
index 407f512a..e355b6d3 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -266,12 +266,11 @@ let rec build_letchain id lbs (E_aux (_, annot) as exp) =
 
 let is_interpreter_extern id env =
   let open Type_check in
-  Env.is_extern id env "interpreter" || Env.is_extern id env "ocaml"
+  Env.is_extern id env "interpreter"
 
 let get_interpreter_extern id env =
   let open Type_check in
-  try Env.get_extern id env "interpreter" with
-  | Type_error _ -> Env.get_extern id env "ocaml"
+  Env.get_extern id env "interpreter"
 
 let rec step (E_aux (e_aux, annot) as orig_exp) =
   let wrap e_aux' = return (E_aux (e_aux', annot)) in
diff --git a/src/value.ml b/src/value.ml
index 157c16fc..90f6d947 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -274,6 +274,10 @@ let value_or_vec = function
   | [v1; v2] -> mk_vector (Sail_lib.or_vec (coerce_bv v1, coerce_bv v2))
   | _ -> failwith "value not_vec"
 
+let value_xor_vec = function
+  | [v1; v2] -> mk_vector (Sail_lib.xor_vec (coerce_bv v1, coerce_bv v2))
+  | _ -> failwith "value xor_vec"
+
 let value_uint = function
   | [v] -> V_int (Sail_lib.uint (coerce_bv v))
   | _ -> failwith "value uint"
@@ -407,6 +411,14 @@ let value_shiftr = function
   | [v1; v2] -> mk_vector (Sail_lib.shiftr (coerce_bv v1, coerce_int v2))
   | _ -> failwith "value shiftr"
 
+let value_shift_bits_left = function
+  | [v1; v2] -> mk_vector (Sail_lib.shift_bits_left (coerce_bv v1, coerce_bv v2))
+  | _ -> failwith "value shift_bits_left"
+
+let value_shift_bits_right = function
+  | [v1; v2] -> mk_vector (Sail_lib.shift_bits_right (coerce_bv v1, coerce_bv v2))
+  | _ -> failwith "value shift_bits_right"
+
 let value_vector_truncate = function
   | [v1; v2] -> mk_vector (Sail_lib.vector_truncate (coerce_bv v1, coerce_int v2))
   | _ -> failwith "value vector_truncate"
@@ -498,6 +510,14 @@ let value_round_down = function
   | [v] -> V_int (Sail_lib.round_down (coerce_real v))
   | _ -> failwith "value round_down"
 
+let value_quot_round_zero = function
+  | [v1; v2] -> V_int (Sail_lib.quot_round_zero (coerce_int v1, coerce_int v2))
+  | _ -> failwith "value quot_round_zero"
+
+let value_rem_round_zero = function
+  | [v1; v2] -> V_int (Sail_lib.rem_round_zero (coerce_int v1, coerce_int v2))
+  | _ -> failwith "value rem_round_zero"
+
 let value_eq_real = function
   | [v1; v2] -> V_bool (Sail_lib.eq_real (coerce_real v1, coerce_real v2))
   | _ -> failwith "value eq_real"
@@ -522,6 +542,10 @@ let value_string_append = function
   | [v1; v2] -> V_string (Sail_lib.string_append (coerce_string v1, coerce_string v2))
   | _ -> failwith "value string_append"
 
+let value_decimal_string_of_bits = function
+  | [v] -> V_string (Sail_lib.decimal_string_of_bits (coerce_bv v))
+  | _ -> failwith "value decimal_string_of_bits"
+       
 let primops =
   List.fold_left
     (fun r (x, y) -> StringMap.add x y r)
@@ -536,6 +560,7 @@ let primops =
       ("putchar", value_putchar);
       ("string_of_int", fun vs -> V_string (string_of_value (List.hd vs)));
       ("string_of_bits", fun vs -> V_string (string_of_value (List.hd vs)));
+      ("decimal_string_of_bits", value_decimal_string_of_bits);
       ("print_bits", value_print_bits);
       ("print_int", value_print_int);
       ("print_string", value_print_string);
@@ -568,6 +593,7 @@ let primops =
       ("not_vec", value_not_vec);
       ("and_vec", value_and_vec);
       ("or_vec", value_or_vec);
+      ("xor_vec", value_xor_vec);
       ("uint", value_uint);
       ("sint", value_sint);
       ("get_slice_int", value_get_slice_int);
@@ -579,6 +605,8 @@ let primops =
       ("zeros", value_zeros);
       ("shiftr", value_shiftr);
       ("shiftl", value_shiftl);
+      ("shift_bits_left", value_shift_bits_left);
+      ("shift_bits_right", value_shift_bits_right);
       ("add_int", value_add_int);
       ("sub_int", value_sub_int);
       ("div_int", value_quotient);
@@ -610,6 +638,8 @@ let primops =
       ("gteq_real", value_gt_real);
       ("round_up", value_round_up);
       ("round_down", value_round_down);
+      ("quot_round_zero", value_quot_round_zero);
+      ("rem_round_zero", value_rem_round_zero);
       ("quotient_real", value_quotient_real);
       ("undefined_unit", fun _ -> V_unit);
       ("undefined_bit", fun _ -> V_bit Sail_lib.B0);
@@ -625,4 +655,5 @@ let primops =
       ("string_length", value_string_length);
       ("string_startswith", value_string_startswith);
       ("string_drop", value_string_drop);
+      ("skip", fun _ -> V_unit);
     ]