4 files changed, 24 insertions, 34 deletions
diff --git a/riscv/Makefile b/riscv/Makefile
index 20ff8160..a3079148 100644
--- a/riscv/Makefile
+++ b/riscv/Makefile
@@ -32,11 +32,11 @@ coverage: _sbuild/coverage.native
 	mkdir bisect && mv bisect*.out bisect/
 	mkdir coverage && bisect-ppx-report -html coverage/ -I _sbuild/ bisect/bisect*.out
 
-riscv.c: $(SAIL_SRCS) main.sail Makefile riscv_prelude.h
-	$(SAIL) -O -memo_z3 -c -c_include "riscv_prelude.h" $(SAIL_SRCS) main.sail 1> $@
+riscv.c: $(SAIL_SRCS) main.sail Makefile
+	$(SAIL) -O -memo_z3 -c -c_include riscv_prelude.h $(SAIL_SRCS) main.sail 1> $@
 
-riscv_c: riscv.c Makefile
-	gcc -O2 riscv.c ../lib/*.c -lgmp -lz -I ../lib -o riscv_c
+riscv_c: riscv.c riscv_prelude.h riscv_prelude.c Makefile
+	gcc -O2 riscv.c riscv_prelude.c ../lib/*.c -lgmp -lz -I ../lib -o riscv_c
 
 latex: $(SAIL_SRCS) Makefile
 	$(SAIL) -latex -latex_prefix sail -o sail_ltx $(SAIL_SRCS)
diff --git a/riscv/prelude.sail b/riscv/prelude.sail
index 88bc00fb..8d56a756 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -70,21 +70,20 @@ val gteq_atom = {coq: "Z.geb", _: "gteq"} : forall 'n 'm. (atom('n), atom('m)) -
 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"} : (int, int) -> 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"} : forall 'n. (bits('n), bits('n)) -> 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 = {ocaml: "eq_string", lem: "eq", coq: "generic_eq"} : (string, string) -> bool
+val eq_string = {c: "eq_string", ocaml: "eq_string", lem: "eq", coq: "generic_eq"} : (string, string) -> bool
 val string_startswith = "string_startswith" : (string, string) -> bool
 val string_drop = "string_drop" : (string, nat) -> string
 val string_length = "string_length" : string -> nat
-val string_append = "string_append" : (string, string) -> string
+val string_append = {c: "concat_str", _: "string_append"} : (string, string) -> string
 val maybe_int_of_prefix = "maybe_int_of_prefix" : string -> option((int, nat))
 val maybe_nat_of_prefix = "maybe_nat_of_prefix" : string -> option((nat, nat))
 val maybe_int_of_string = "maybe_int_of_string" : string -> option(int)
 
-
 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
@@ -104,7 +103,7 @@ overload operator == = {eq_atom, eq_int, eq_bit, eq_vec, eq_string, eq_real, eq_
 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 = {ocaml: "access", lem: "access_vec_dec", coq: "access_vec_dec"} : forall ('n : Int) ('m : Int), 0 <= 'm < 'n.
+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.
@@ -136,7 +135,7 @@ overload append = {bitvector_concat, vector_concat}
 
 val not_bool = {coq: "negb", _: "not"} : bool -> bool
 
-val not_vec = "not_vec" : forall 'n. bits('n) -> bits('n)
+val not_vec = {c: "not_bits", _: "not_vec"} : forall 'n. bits('n) -> bits('n)
 
 overload ~ = {not_bool, not_vec}
 
@@ -160,7 +159,7 @@ overload operator != = {neq_atom, neq_int, neq_vec, neq_anything}
 
 val and_bool = {coq: "andb", _: "and_bool"} : (bool, bool) -> bool
 
-val builtin_and_vec = {ocaml: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+val builtin_and_vec = {c: "and_bits", ocaml: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
 val and_vec = {lem: "and_vec", coq: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
@@ -178,9 +177,9 @@ function or_vec (xs, ys) = builtin_or_vec(xs, ys)
 
 overload operator | = {or_bool, or_vec}
 
-val unsigned = {ocaml: "uint", lem: "uint", coq: "uint"} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1)
+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"} : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 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)
 
@@ -231,7 +230,7 @@ val HexStr : int -> string
 
 val BitStr = "string_of_bits" : forall 'n. bits('n) -> string
 
-val xor_vec = "xor_vec" : forall 'n. (bits('n), bits('n)) -> bits('n)
+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"} : (int, int) -> int
 
@@ -244,9 +243,9 @@ val add_range = {ocaml: "add_int", lem: "integerAdd", coq: "add_range"} : forall
 
 val add_int = {ocaml: "add_int", lem: "integerAdd", coq: "Z.add"} : (int, int) -> int
 
-val add_vec = "add_vec" : forall 'n. (bits('n), bits('n)) -> bits('n)
+val add_vec = {c: "add_bits", _: "add_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
-val add_vec_int = "add_vec_int" : forall 'n. (bits('n), int) -> 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
 
@@ -260,9 +259,9 @@ val sub_nat = {ocaml: "(fun (x,y) -> let n = sub_int (x,y) in if Big_int.less_eq
                lem: "integerMinus", coq: "sub_nat"}
             : (nat, nat) -> nat
 
-val "sub_vec" : forall 'n. (bits('n), bits('n)) -> bits('n)
+val sub_vec = {c: "sub_bits", _: "sub_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
-val "sub_vec_int" : forall 'n. (bits('n), int) -> 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
 
diff --git a/riscv/riscv_prelude.c b/riscv/riscv_prelude.c
new file mode 100644
index 00000000..a1f06b4d
--- /dev/null
+++ b/riscv/riscv_prelude.c
@@ -0,0 +1,6 @@
+#include "riscv_prelude.h"
+
+unit print_string(sail_string prefix, sail_string msg)
+{
+  printf("%s%s\n", prefix, msg);
+}
diff --git a/riscv/riscv_prelude.h b/riscv/riscv_prelude.h
index 94f02b83..a0686086 100644
--- a/riscv/riscv_prelude.h
+++ b/riscv/riscv_prelude.h
@@ -1,19 +1,4 @@
 #include "sail.h"
 #include "rts.h"
 
-void string_append(sail_string *dst, sail_string s1, sail_string s2);
-bool string_startswith(sail_string s, sail_string prefix);
-void string_length(sail_int *len, sail_string s);
-void string_drop(sail_string *dst, sail_string s, sail_int len);
 unit print_string(sail_string prefix, sail_string msg);
-
-void add_vec(sail_bits *dst, sail_bits s1, sail_bits s2);
-void add_vec_int(sail_bits *dst, sail_bits src, sail_int i);
-
-void sub_vec(sail_bits *dst, sail_bits s1, sail_bits s2);
-void sub_vec_int(sail_bits *dst, sail_bits src, sail_int i);
-
-void not_vec(sail_bits *dst, sail_bits src);
-void xor_vec(sail_bits *dst, sail_bits s1, sail_bits s2);
-
-