Merge branch 'sail2' into mappings

(involved some manual tinkering with gitignore, type_check, riscv)

8 files changed, 118 insertions, 160 deletions

diff --git a/mips/.gitignore b/mips/.gitignore
new file mode 100644
index 00000000..2ee9fde0
--- /dev/null
+++ b/mips/.gitignore
@@ -0,0 +1,5 @@
+mips.lem
+mips_types.lem
+mipsScript.sml
+mips_typesScript.sml
+mips_extrasScript.sml
\ No newline at end of file
diff --git a/mips/Holmakefile b/mips/Holmakefile
new file mode 100644
index 00000000..a31bfd4f
--- /dev/null
+++ b/mips/Holmakefile
@@ -0,0 +1,11 @@
+LEMDIR=../../lem/hol-lib
+
+INCLUDES = $(LEMDIR) ../lib/hol
+
+all: mipsTheory.uo
+.PHONY: all
+
+ifdef POLY
+BASE_HEAP = ../lib/hol/sail-heap
+
+endif
diff --git a/mips/Makefile b/mips/Makefile
index 6d605d60..6abf1848 100644
--- a/mips/Makefile
+++ b/mips/Makefile
@@ -12,24 +12,37 @@ MIPS_TLB_STUB:=$(MIPS_SAIL_DIR)/mips_tlb_stub.sail
 MIPS_SAILS:=$(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_ast_decl.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
 MIPS_MAIN:=$(MIPS_SAIL_DIR)/main.sail
 
-mips: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN)
-	$(SAIL) -ocaml -o mips -memo_z3 $^
+mips: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN) ../sail
+	$(SAIL) -ocaml -o mips -memo_z3 $(filter %.sail, $^)
+
+mips.c: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN) Makefile ../sail
+	$(SAIL) -O -memo_z3 -c $(filter %.sail, $^) 1> $@
+
+mips_c: mips.c ../lib/sail.h Makefile
+	gcc -O2 -g -I ../lib $< -l gmp -o $@
 
 mips_no_tlb.lem: $(MIPS_PRE) $(MIPS_TLB_STUB) $(MIPS_SAILS)
 	$(SAIL) -lem -o mips_no_tlb -lem_mwords -lem_lib Mips_extras -undefined_gen -memo_z3 $^
 mips_no_tlb_types.lem: mips_no_tlb.lem
 
-# TODO: Use monomorphisation so that we can switch to machine words
-mips.lem: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS)
-	$(SAIL) -lem -o mips -lem_lib Mips_extras -undefined_gen -memo_z3 $^
+mips.lem: $(MIPS_PRE) $(SAIL_LIB_DIR)/mono_rewrites.sail $(MIPS_TLB) $(MIPS_SAILS)
+	$(SAIL) -lem -o mips -auto_mono -mono_rewrites -lem_mwords -lem_lib Mips_extras -undefined_gen -memo_z3 $^
 mips_types.lem: mips.lem
 
 M%.thy: m%.lem m%_types.lem mips_extras.lem
 	lem -isa -outdir . -lib $(SAIL_DIR)/src/gen_lib -lib $(SAIL_DIR)/src/lem_interp $^
 	sed -i 's/datatype ast/datatype (plugins only: size) ast/' M$*_types.thy
 
+%Script.sml: %.lem %_types.lem $(MIPS_SAIL_DIR)/mips_extras.lem
+	lem -hol -outdir . -lib $(SAIL_DIR)/lib/hol -lib $(SAIL_DIR)/src/gen_lib -lib $(SAIL_DIR)/src/lem_interp $^
+
+%Theory.uo: %Script.sml
+	Holmake $@
+
 LOC_FILES:=$(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN)
 include ../etc/loc.mk
 
 clean:
-	rm -rf mips Mips.thy mips.lem _sbuild
+	rm -rf mips Mips.thy mips.lem mips_types.lem _sbuild mips.c mips_c
+	rm -f mipsScript.sml mips_typesScript.sml mips_extrasScript.sml
+	-Holmake cleanAll
diff --git a/mips/main.sail b/mips/main.sail
index 8ec91ba6..8b1e01d7 100644
--- a/mips/main.sail
+++ b/mips/main.sail
@@ -1,39 +1,44 @@
 
 register instCount : int
 
-val fetch_and_execute : unit -> unit effect {barr, eamem, escape, rmem, rreg, wmv, wreg, undef, wmvt, rmemt}
+val fetch_and_execute : unit -> bool effect {barr, eamem, escape, rmem, rreg, wmv, wreg, undef, wmvt, rmemt}
 function fetch_and_execute () = {
-  while true do {
-    PC = nextPC;
-    inBranchDelay = branchPending;
-    branchPending = 0b0;
-    nextPC = if inBranchDelay then delayedPC else PC + 4;
-    cp2_next_pc();
-    instCount = instCount + 1;
-    print_bits("PC: ", PC);
-    try {
-      let pc_pa = TranslatePC(PC);
-      /*print_bits("pa: ", pc_pa);*/
-      let instr = MEMr_wrapper(pc_pa, 4);
-      /*print_bits("hex: ", instr);*/
-      let instr_ast = decode(instr);
-      match instr_ast {
-        Some(HCF()) => {
-                       print("simulation stopped due to halt instruction.");
-                       return ();
-                     },
-        Some(ast) => execute(ast),
-        None()    => {print("Decode failed"); exit (())} /* Never expect this -- unknown instruction should actually result in reserved instruction ISA-level exception (see mips_ri.sail). */
-      }
-    } catch {
-      ISAException() => print("EXCEPTION")
-      /* ISA-level exception occurrred either during TranslatePC or execute --
-         just continue from nextPC, which should have been set to the appropriate
-         exception vector (along with clearing branchPending etc.) . */
-    };
+  PC = nextPC;
+  inBranchDelay = branchPending;
+  branchPending = 0b0;
+  nextPC = if inBranchDelay then delayedPC else PC + 4;
+  cp2_next_pc();
+  instCount = instCount + 1;
+  if UART_WRITTEN then {
+    putchar(unsigned(UART_WDATA));
+    UART_WRITTEN = 0b0;
   };
+  /* the following skips are required on mips to fake the tag effects otherwise type checker complains  */
   skip_rmemt();
   skip_wmvt();
+  prerr_bits("PC: ", PC);
+  loop_again = true;
+  try {
+    let pc_pa = TranslatePC(PC);
+    /*print_bits("pa: ", pc_pa);*/
+    let instr = MEMr_wrapper(pc_pa, 4);
+    /*print_bits("hex: ", instr);*/
+    let instr_ast = decode(instr);
+    match instr_ast {
+      Some(HCF()) => {
+                     print("simulation stopped due to halt instruction.");
+                     loop_again = false
+                   },
+      Some(ast) => execute(ast),
+      None()    => { print("Decode failed"); loop_again=false } /* Never expect this -- unknown instruction should actually result in reserved instruction ISA-level exception (see mips_ri.sail). */
+    }
+  } catch {
+    ISAException() => prerr_endline("EXCEPTION")
+    /* ISA-level exception occurrred either during TranslatePC or execute --
+       just continue from nextPC, which should have been set to the appropriate
+       exception vector (along with clearing branchPending etc.) . */
+  };
+  loop_again;
 }
 
 val elf_entry = {
@@ -42,7 +47,13 @@ val elf_entry = {
   c: "elf_entry"
 } : unit -> int
 
-val main : unit -> unit effect {barr, eamem, escape, rmem, rreg, undef, wmv, wreg, rmemt, wmvt}
+val init_registers : bits(64) -> unit effect {wreg}
+
+function init_registers (initialPC) = {
+  init_cp0_state();
+  init_cp2_state();
+  nextPC = initialPC;
+}
 
 function dump_mips_state () : unit -> unit = {
   print_bits("DEBUG MIPS PC ", PC);
@@ -51,12 +62,12 @@ function dump_mips_state () : unit -> unit = {
   }
 }
 
+val main : unit -> unit effect {barr, eamem, escape, rmem, rreg, undef, wmv, wreg, rmemt, wmvt}
+
 function main () = {
-  init_cp0_state();
-  init_cp2_state();
-  nextPC = to_bits(64, elf_entry());
+  init_registers(to_bits(64, elf_entry()));
   startTime = get_time_ns();
-  fetch_and_execute();
+  while (fetch_and_execute()) do ();
   endTime = get_time_ns();
   elapsed = endTime - startTime;
   inst_1e9 = instCount * 1000000000;
diff --git a/mips/mips_insts.sail b/mips/mips_insts.sail
index a3781426..db494224 100644
--- a/mips/mips_insts.sail
+++ b/mips/mips_insts.sail
@@ -1455,7 +1455,7 @@ function clause execute (MFC0(rt, rd, sel, double)) = {
                                  @ 0b000             /* AR */
                                  @ 0b001             /* MT standard TLB */
                                  @ 0b0000            /* zero */
-                                 @ 0b000),
+                                 @ CP0ConfigK0),
           (0b10000,0b001) => zero_extend( /* 16, sel 1: Config1 */
                                           0b1      /* M */
                                         @ TLBIndexMax /* MMU size-1 */
@@ -1556,7 +1556,7 @@ function clause execute (MTC0(rt, rd, sel, double)) = {
         CP0Cause->IP() = ((ip[7..2]) @ (reg_val[9..8]));
       },
       (0b01110,0b000) => CP0EPC = reg_val, /* 14, EPC */
-      (0b10000,0b000) => (), /* XXX ignore K0 cache config  16: Config0 */
+      (0b10000,0b000) => CP0ConfigK0 = reg_val[2..0], /*  K0 cache config 16: Config0 */
       (0b10100,0b000) => TLBXContext->XPTEBase() = reg_val[63..33],
       (0b11110,0b000) => CP0ErrorEPC = reg_val, /* 30, ErrorEPC */
       _               => (SignalException(ResI))
diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail
index f9049b5d..b5931a45 100644
--- a/mips/mips_prelude.sail
+++ b/mips/mips_prelude.sail
@@ -267,6 +267,7 @@ register CP0BadVAddr : bits(64)
 register CP0Count : bits(32)
 register CP0HWREna : bits(32)
 register CP0UserLocal : bits(64)
+register CP0ConfigK0 : bits(3)
 
 bitfield StatusReg : bits(32) = {
   CU : 31.. 28,  /* co-processor enable bits */
@@ -614,22 +615,20 @@ function rec forall Nat 'W, 'W >= 1. bits(8 * 'W) reverse_endianness ((bits(8 *
     reverse_endianness'(sizeof 'W, value)
 }*/
 
-val MEMr_wrapper : forall 'n, 1 <= 'n <=8 . (bits(64), atom('n)) -> bits(8*'n) effect {rmem}
-function MEMr_wrapper (addr, size) = reverse_endianness(MEMr (addr, size))
-/* TODO
+val MEMr_wrapper : forall 'n, 1 <= 'n <=8 . (bits(64), atom('n)) -> bits(8*'n) effect {rmem, rreg, wreg}
+function MEMr_wrapper (addr, size) = 
     if (addr == 0x000000007f000000) then
       {
         let rvalid = UART_RVALID in
-	let rdata = (bits(8 * 'n)) (mask(0x00000000 : UART_RDATA : rvalid : 0b0000000 : 0x0000)) in
         {
           UART_RVALID = [bitzero];
-          rdata
+          mask(0x00000000 @ UART_RDATA @ rvalid @ 0b0000000 @ 0x0000)
         }
       }
     else if (addr == 0x000000007f000004) then
       mask(0x000000000004ffff) /* Always plenty of write space available and jtag activity */
     else
-      reverse_endianness(MEMr(addr, size)) /* MEMr assumes little endian */ */
+      reverse_endianness(MEMr(addr, size)) /* MEMr assumes little endian */
 
 val MEMr_reserve_wrapper : forall 'n, 1 <= 'n <= 8 . ( bits(64) , atom('n) ) -> (bits(8 * 'n)) effect { rmem }
 function MEMr_reserve_wrapper (addr , size) =
diff --git a/mips/mips_wrappers.sail b/mips/mips_wrappers.sail
index 70e6fa83..0cc098a5 100644
--- a/mips/mips_wrappers.sail
+++ b/mips/mips_wrappers.sail
@@ -42,7 +42,7 @@ function MEMw_wrapper(addr, size, data) =
     if (addr == 0x000000007f000000) then
       {
         UART_WDATA   = ledata[7..0];
-	UART_WRITTEN = bitone;
+        UART_WRITTEN = bitone;
       } else {
         MEMea(addr, size);
         MEMval(addr, size, ledata);
diff --git a/mips/prelude.sail b/mips/prelude.sail
index e0bcd8cf..b2c2931b 100644
--- a/mips/prelude.sail
+++ b/mips/prelude.sail
@@ -1,103 +1,44 @@
 default Order dec
 
-type bits ('n : Int) = vector('n, dec, bit)
-union option ('a : Type) = {None : unit, Some : 'a}
-
-val eq_bit = {ocaml: "(fun (x, y) -> x = y)", lem: "eq", interpreter: "eq_anything", c: "eq_bit"} : (bit, bit) -> bool
-
-val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
-
-val eq_string = {ocaml: "eq_string", lem: "eq"} : (string, string) -> bool
-
-val eq_anything = {ocaml: "(fun (x, y) -> x = y)", lem: "eq"} : forall ('a : Type). ('a, 'a) -> bool
-
-val bitvector_length = {ocaml: "length", lem: "length"} : forall 'n. bits('n) -> atom('n)
-val vector_length = {ocaml: "length", lem: "length_list"} : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n)
-val list_length = {ocaml: "length", lem: "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_bit}
+/* this is here because if we don't have it before including vector_dec 
+   we get infinite loops caused by interaction with bool/bit casts */
+val eq_bit2 = "eq_bit" : (bit, bit) -> bool
+overload operator == = {eq_bit2}
 
+$include <smt.sail>
 $include <flow.sail>
+$include <arith.sail>
+$include <option.sail>
+$include <vector_dec.sail>
 
-overload operator == = {eq_vec, eq_string, eq_anything}
-
-val vector_subrange = {ocaml: "subrange", lem: "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"} : forall ('n : Int) ('m : Int), 0 <= 'm < 'n.
-  (bits('n), atom('m)) -> bit
-
-val any_vector_access = {ocaml: "access", lem: "access_list_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 eq_anything = {ocaml: "(fun (x, y) -> x = y)", lem: "eq", _:"eq_anything"} : forall ('a : Type). ('a, 'a) -> bool
+overload operator == = {eq_anything}
 
-val bitvector_update = {ocaml: "update", lem: "update_vec_dec"} : forall 'n.
-  (bits('n), int, bit) -> bits('n)
-
-val any_vector_update = {ocaml: "update", lem: "update_list_dec"} : 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"} : forall 'n 'm 'o.
-  (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
-
-val bitvector_concat = {ocaml: "append", lem: "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_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}
 
 val not = "not" : bool -> bool
 
 val neq_vec = {lem: "neq"} : forall 'n. (bits('n), bits('n)) -> bool
-function neq_vec (x, y) = not_bool(eq_vec(x, y))
+function neq_vec (x, y) = not_bool(eq_bits(x, y))
 
 val neq_anything = {lem: "neq"} : forall ('a : Type). ('a, 'a) -> bool
 function neq_anything (x, y) = not_bool(x == y)
 
 overload operator != = {neq_atom, neq_int, neq_vec, neq_anything}
 
-val builtin_and_vec = {ocaml: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
-
-val and_vec = {lem: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
-
-function and_vec (xs, ys) = builtin_and_vec(xs, ys)
-
-overload operator & = {and_bool, and_vec}
+val and_bits = {c:"and_bits", _: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
-val builtin_or_vec = {ocaml: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+overload operator & = {and_bool, and_bits}
 
-val or_vec = {lem: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+val or_bits = {c: "or_bits", _: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
-function or_vec (xs, ys) = builtin_or_vec(xs, ys)
-
-overload operator | = {or_bool, or_vec}
-
-/*!
-The \function{unsigned} function converts a bit vector to an integer assuming an unsigned representation:
-*/
-val unsigned = {ocaml: "uint", lem: "uint"} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1)
-
-/*!
-The \function{signed} function converts a bit vector to an integer assuming a signed twos-complement representation:
-*/
-val signed = {ocaml: "sint", lem: "sint"} : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1)
-
-val "get_slice_int" : forall 'w. (atom('w), int, int) -> bits('w)
+overload operator | = {or_bool, or_bits}
 
 val cast cast_unit_vec : bit -> bits(1)
 
@@ -106,11 +47,14 @@ function cast_unit_vec b = match b {
   bitone => 0b1
 }
 
-val print = "prerr_endline" : string -> unit
+val print = "print_endline" : string -> unit
+
+val "prerr_endline" : string -> unit
+
 
-val putchar = "putchar" : forall ('a : Type). 'a -> unit
+val putchar = {c:"sail_putchar", _:"putchar"} : forall ('a : Type). 'a -> unit
 
-val concat_str = {ocaml: "concat_str", lem: "stringAppend"} : (string, string) -> string
+val concat_str = {lem: "stringAppend", _: "concat_str"} : (string, string) -> string
 
 val string_of_int = "string_of_int" : int -> string
 
@@ -120,7 +64,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"} : (int, int) -> int
 
@@ -129,8 +73,6 @@ overload operator ^ = {xor_vec, int_power}
 val add_range = {ocaml: "add_int", lem: "integerAdd"} : forall 'n 'm 'o 'p.
   (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
 
-val add_int = {ocaml: "add_int", lem: "integerAdd"} : (int, int) -> int
-
 val add_vec = "add_vec" : forall 'n. (bits('n), bits('n)) -> bits('n)
 
 val add_vec_int = "add_vec_int" : forall 'n. (bits('n), int) -> bits('n)
@@ -140,16 +82,12 @@ overload operator + = {add_range, add_int, add_vec, add_vec_int}
 val sub_range = {ocaml: "sub_int", lem: "integerMinus"} : forall 'n 'm 'o 'p.
   (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o)
 
-val sub_int = {ocaml: "sub_int", lem: "integerMinus"} : (int, int) -> int
-
-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 negate_range = {ocaml: "minus_big_int", lem: "integerNegate"} : forall 'n 'm. range('n, 'm) -> range(- 'm, - 'n)
 
-val negate_int = {ocaml: "minus_big_int", lem: "integerNegate"} : int -> int
-
 overload operator - = {sub_range, sub_int, sub_vec, sub_vec_int}
 
 overload negate = {negate_range, negate_int}
@@ -157,8 +95,6 @@ overload negate = {negate_range, negate_int}
 val mult_range = {ocaml: "mult", lem: "integerMult"} : forall 'n 'm 'o 'p.
   (range('n, 'm), range('o, 'p)) -> range('n * 'o, 'm * 'p)
 
-val mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int
-
 overload operator * = {mult_range, mult_int}
 
 val quotient_nat = {ocaml: "quotient", lem: "integerDiv"} : (nat, nat) -> nat
@@ -167,10 +103,10 @@ val quotient = {ocaml: "quotient", lem: "integerDiv"} : (int, int) -> int
 
 overload operator / = {quotient_nat, quotient}
 
-val quot_round_zero = {ocaml: "quot_round_zero", lem: "hardware_quot"} : (int, int) -> int
-val rem_round_zero = {ocaml: "rem_round_zero", lem: "hardware_mod"} : (int, int) -> int
+val quot_round_zero = {ocaml: "quot_round_zero", lem: "hardware_quot", _ : "div_int"} : (int, int) -> int
+val rem_round_zero = {ocaml: "rem_round_zero", lem: "hardware_mod", _ : "mod_int"} : (int, int) -> int
 
-val modulus = {ocaml: "modulus", lem: "hardware_mod"} : forall 'n, 'n > 0 .  (int, atom('n)) -> range(0, 'n - 1)
+val modulus = {ocaml: "modulus", lem: "hardware_mod", _ : "mod_int"} : forall 'n, 'n > 0 .  (int, atom('n)) -> range(0, 'n - 1)
 
 overload operator % = {modulus}
 
@@ -202,18 +138,12 @@ val __ReadRAM = "read_ram" : forall 'n 'm.
 val __MIPS_read : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem}
 function __MIPS_read (addr, width) = __ReadRAM(64, width, 0x0000_0000_0000_0000, addr)
 
-val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
-
 infix 8 ^^
 val operator ^^ = {lem: "replicate_bits"} : forall 'n 'm . (bits('n), atom('m)) -> bits('n * 'm)
 function operator ^^ (bs, n) = replicate_bits (bs, 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
-
 union exception = {
   ISAException : unit,
   Error_not_implemented : string,
@@ -222,14 +152,11 @@ union exception = {
   Error_internal_error : unit
 }
 
-val _sign_extend = {ocaml: "sign_extend", lem: "_sign_extend"} : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
-val _zero_extend = {ocaml: "zero_extend", lem: "_zero_extend"} : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
-
 val sign_extend : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m)
 val zero_extend : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m)
 
-function sign_extend v = _sign_extend(v, sizeof('m))
-function zero_extend v = _zero_extend(v, sizeof('m))
+function sign_extend v = sail_sign_extend(v, sizeof('m))
+function zero_extend v = sail_zero_extend(v, sizeof('m))
 
 val zeros : forall 'n, 'n >= 0 . unit -> bits('n)
 function zeros() = replicate_bits (0b0,'n)
@@ -289,14 +216,6 @@ val operator *_u = "mult_vec" : forall 'n . (bits('n), bits('n)) -> bits(2 * 'n)
 val to_bits : forall 'l.(atom('l), int) -> bits('l)
 function to_bits (l, n) = get_slice_int(l, n, 0)
 
-val vector_update_subrange_dec = {ocaml: "update_subrange", lem: "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}
-
 val mask : forall 'm 'n , 'm >= 'n > 0 . bits('m) -> bits('n)
 function mask bs = bs['n - 1 .. 0]