Merge branch 'sail2' of github.com:rems-project/sail into sail2

43 files changed, 881 insertions, 271 deletions

diff --git a/test/c/sail.h b/test/c/sail.h
index 880f5a57..92127a1b 100644
--- a/test/c/sail.h
+++ b/test/c/sail.h
@@ -38,7 +38,7 @@ unit sail_exit(const unit u) {
 }
 
 void elf_entry(mpz_t *rop, const unit u) {
-  mpz_set_ui(*rop, 0x8000ul);
+  mpz_set_ui(*rop, 0x400130ul);
 }
 
 // Sail bits are mapped to ints where bitzero = 0 and bitone = 1
@@ -240,6 +240,11 @@ void pow2(mpz_t *rop, mpz_t exp) {
 
 // ***** Sail bitvectors *****
 
+unit print_bits(const sail_string str, const bv_t op) {
+  fputs(str, stdout);
+  gmp_printf("%d'0x%ZX\n", op.len, op.bits);
+}
+
 void length_bv_t(mpz_t *rop, const bv_t op) {
   mpz_set_ui(*rop, op.len);
 }
@@ -278,13 +283,22 @@ void replicate_bits(bv_t *rop, const bv_t op1, const mpz_t op2) {
   rop->len = op1.len * op2_ui;
   mpz_set(*rop->bits, *op1.bits);
   for (int i = 1; i < op2_ui; i++) {
-    mpz_mul_2exp(*rop->bits, *rop->bits, op2_ui);
-    mpz_add(*rop->bits, *rop->bits, *op1.bits);
+    mpz_mul_2exp(*rop->bits, *rop->bits, op1.len);
+    mpz_ior(*rop->bits, *rop->bits, *op1.bits);
   }
 }
 
-void slice(bv_t *rop, const bv_t op, const mpz_t i, const mpz_t len) {
-  // TODO
+void slice(bv_t *rop, const bv_t op, const mpz_t start_mpz, const mpz_t len_mpz)
+{
+  uint64_t start = mpz_get_ui(start_mpz);
+  uint64_t len = mpz_get_ui(len_mpz);
+
+  mpz_set_ui(*rop->bits, 0ul);
+  rop->len = len;
+
+  for (uint64_t i = 0; i < len; i++) {
+    if (mpz_tstbit(*op.bits, i + start)) mpz_setbit(*rop->bits, i);
+  }
 }
 
 uint64_t convert_uint64_t_of_bv_t(const bv_t op) {
@@ -321,6 +335,12 @@ void mask(bv_t *rop) {
   }
 }
 
+void truncate(bv_t *rop, const bv_t op, const mpz_t len) {
+  rop->len = mpz_get_ui(len);
+  mpz_set(*rop->bits, *op.bits);
+  mask(rop);
+}
+
 void and_bits(bv_t *rop, const bv_t op1, const bv_t op2) {
   rop->len = op1.len;
   mpz_and(*rop->bits, *op1.bits, *op2.bits);
@@ -341,8 +361,11 @@ void xor_bits(bv_t *rop, const bv_t op1, const bv_t op2) {
   mpz_xor(*rop->bits, *op1.bits, *op2.bits);
 }
 
+mpz_t eq_bits_test;
+
 bool eq_bits(const bv_t op1, const bv_t op2) {
-  return mpz_cmp(*op1.bits, *op2.bits) == 0;
+  mpz_xor(eq_bits_test, *op1.bits, *op2.bits);
+  return mpz_popcount(eq_bits_test) == 0;
 }
 
 void sail_uint(mpz_t *rop, const bv_t op) {
@@ -382,37 +405,122 @@ void sub_bits_int(bv_t *rop, const bv_t op1, const mpz_t op2) {
   mask(rop);
 }
 
-void get_slice_int(bv_t *rop, const mpz_t n, const mpz_t m, const mpz_t o) {
-  // TODO
+// Takes a slice of the (two's complement) binary representation of
+// integer n, starting at bit start, and of length len. With the
+// argument in the following order:
+//
+// get_slice_int(len, n, start)
+//
+// For example:
+//
+// get_slice_int(8, 1680, 4) =
+//
+//                    11           0
+//                    V            V
+// get_slice_int(8, 0b0110_1001_0000, 4) = 0b0110_1001
+//                    <-------^
+//                    (8 bit) 4
+//
+void get_slice_int(bv_t *rop, const mpz_t len_mpz, const mpz_t n, const mpz_t start_mpz)
+{
+  uint64_t start = mpz_get_ui(start_mpz);
+  uint64_t len = mpz_get_ui(len_mpz);
+
+  mpz_set_ui(*rop->bits, 0ul);
+  rop->len = len;
+
+  for (uint64_t i = 0; i < len; i++) {
+    if (mpz_tstbit(n, i + start)) mpz_setbit(*rop->bits, i);
+  }
 }
 
-void set_slice_int(mpz_t *rop, const mpz_t n, const mpz_t m, const mpz_t o, const bv_t op) {
-  // TODO
+// Set slice uses the same indexing scheme as get_slice_int, but it
+// puts a bitvector slice into an integer rather than returning it.
+void set_slice_int(mpz_t *rop,
+		   const mpz_t len_mpz,
+		   const mpz_t n,
+		   const mpz_t start_mpz,
+		   const bv_t slice)
+{
+  uint64_t start = mpz_get_ui(start_mpz);
+
+  mpz_set(*rop, n);
+
+  for (uint64_t i = 0; i < slice.len; i++) {
+    if (mpz_tstbit(*slice.bits, i)) {
+      mpz_setbit(*rop, i + start);
+    } else {
+      mpz_clrbit(*rop, i + start);
+    }
+  }
 }
 
-void vector_update_subrange_bv_t(bv_t *rop, const bv_t op, const mpz_t n, const mpz_t m, const bv_t slice) {
-  // TODO
+void vector_update_subrange_bv_t(bv_t *rop,
+				 const bv_t op,
+				 const mpz_t n_mpz,
+				 const mpz_t m_mpz,
+				 const bv_t slice)
+{
+  uint64_t n = mpz_get_ui(n_mpz);
+  uint64_t m = mpz_get_ui(m_mpz);
+
+  mpz_set(*rop->bits, *op.bits);
+
+  for (uint64_t i = 0; i < n - (m - 1ul); i++) {
+    if (mpz_tstbit(*slice.bits, i)) {
+      mpz_setbit(*rop->bits, i + m);
+    } else {
+      mpz_clrbit(*rop->bits, i + m);
+    }
+  }
 }
 
-void vector_subrange_bv_t(bv_t *rop, const bv_t op, const mpz_t n, const mpz_t m) {
-  // TODO
+void vector_subrange_bv_t(bv_t *rop, const bv_t op, const mpz_t n_mpz, const mpz_t m_mpz)
+{
+  uint64_t n = mpz_get_ui(n_mpz);
+  uint64_t m = mpz_get_ui(m_mpz);
+
+  mpz_set_ui(*rop->bits, 0ul);
+  rop->len = n - (m - 1ul);
+
+  for (uint64_t i = 0; i < rop->len; i++) {
+    if (mpz_tstbit(*op.bits, i + m)) {
+      mpz_setbit(*rop->bits, i);
+    } else {
+      mpz_clrbit(*rop->bits, i);
+    }
+  }
 }
 
-int bitvector_access(const bv_t op, const mpz_t n) {
-  return 0; // TODO
+int bitvector_access(const bv_t op, const mpz_t n_mpz) {
+  uint64_t n = mpz_get_ui(n_mpz);
+  return mpz_tstbit(*op.bits, n);
 }
 
 void hex_slice (bv_t *rop, const sail_string hex, const mpz_t n, const mpz_t m) {
-  // TODO
+  fprintf(stderr, "hex_slice unimplemented");
+  exit(1);
 }
 
-void set_slice (bv_t *rop, const mpz_t len, const mpz_t slen, const bv_t op, const mpz_t i, const bv_t slice) {
-  // TODO
-}
+void set_slice (bv_t *rop,
+		const mpz_t len_mpz,
+		const mpz_t slen_mpz,
+		const bv_t op,
+		const mpz_t start_mpz,
+		const bv_t slice)
+{
+  uint64_t start = mpz_get_ui(start_mpz);
 
-unit print_bits(const sail_string str, const bv_t op) {
-  fputs(str, stdout);
-  gmp_printf("%d'0x%ZX\n", op.len, op.bits);
+  mpz_set(*rop->bits, *op.bits);
+  rop->len = op.len;
+
+  for (uint64_t i = 0; i < slice.len; i++) {
+    if (mpz_tstbit(*slice.bits, i)) {
+      mpz_setbit(*rop->bits, i + start);
+    } else {
+      mpz_clrbit(*rop->bits, i + start);
+    }
+  }
 }
 
 // ***** Real number implementation *****
@@ -425,10 +533,6 @@ typedef mpf_t real;
 
 #define FLOAT_PRECISION 255
 
-void setup_real(void) {
-  mpf_set_default_prec(FLOAT_PRECISION);
-}
-
 void init_real(real *rop) {
   mpf_init(*rop);
 }
@@ -528,9 +632,67 @@ void init_real_of_sail_string(real *rop, const sail_string op) {
 // ***** Memory *****
 
 unit write_ram(const mpz_t m, const mpz_t n, const bv_t x, const bv_t y, const bv_t data) {
-  return UNIT;
+  fprintf(stderr, "write_ram unimplemented");
+  exit(1);
+}
+
+void read_ram(bv_t *data, const mpz_t m, const mpz_t n, const bv_t x, const bv_t addr_bv) {
+  uint64_t addr = mpz_get_ui(*addr_bv.bits);
+  uint32_t instr;
+  switch (addr) {
+    // print_char
+  case 0x400110: instr = 0xd10043ffu; break;
+  case 0x400114: instr = 0x39003fe0u; break;
+  case 0x400118: instr = 0x39403fe0u; break;
+  case 0x40011c: instr = 0x580003e1u; break;
+  case 0x400120: instr = 0x39000020u; break;
+  case 0x400124: instr = 0xd503201fu; break;
+  case 0x400128: instr = 0x910043ffu; break;
+  case 0x40012c: instr = 0xd65f03c0u; break;
+    // _start
+  case 0x400130: instr = 0xa9be7bfdu; break;
+  case 0x400134: instr = 0x910003fdu; break;
+  case 0x400138: instr = 0x94000007u; break;
+  case 0x40013c: instr = 0xb9001fa0u; break;
+  case 0x400140: instr = 0x52800080u; break;
+  case 0x400144: instr = 0x97fffff3u; break;
+  case 0x400148: instr = 0xd503201fu; break;
+  case 0x40014c: instr = 0xa8c27bfdu; break;
+  case 0x400150: instr = 0xd65f03c0u; break;
+    // main
+  case 0x400154: instr = 0xd10043ffu; break;
+  case 0x400158: instr = 0xb9000fffu; break;
+  case 0x40015c: instr = 0xb9000bffu; break;
+  case 0x400160: instr = 0x14000007u; break;
+  case 0x400164: instr = 0xb9400fe0u; break;
+  case 0x400168: instr = 0x11000400u; break;
+  case 0x40016c: instr = 0xb9000fe0u; break;
+  case 0x400170: instr = 0xb9400be0u; break;
+  case 0x400174: instr = 0x11000400u; break;
+  case 0x400178: instr = 0xb9000be0u; break;
+  case 0x40017c: instr = 0xb9400be0u; break;
+  case 0x400180: instr = 0x710fa01fu; break;
+  case 0x400184: instr = 0x54ffff0du; break;
+  case 0x400188: instr = 0xb9400fe0u; break;
+  case 0x40018c: instr = 0x910043ffu; break;
+  case 0x400190: instr = 0xd65f03c0u; break;
+  case 0x400194: instr = 0x00000000u; break;
+  case 0x400198: instr = 0x13000000u; break;
+  case 0x40019c: instr = 0x00000000u; break;
+  }
+
+  mpz_set_ui(*data->bits, instr);
+  data->len = 32;
+  print_bits("instruction = ", *data);
+}
+
+// ***** Setup and cleanup functions for library code *****
+
+void setup_library(void) {
+  mpf_set_default_prec(FLOAT_PRECISION);
+  mpz_init(eq_bits_test);
 }
 
-void read_ram(bv_t *data, const mpz_t m, const mpz_t n, const bv_t x, const bv_t y) {
-  // TODO
+void cleanup_library(void) {
+  mpz_clear(eq_bits_test);
 }
diff --git a/test/c/short_circuit.expect b/test/c/short_circuit.expect
new file mode 100644
index 00000000..9766475a
--- /dev/null
+++ b/test/c/short_circuit.expect
@@ -0,0 +1 @@
+ok
diff --git a/test/c/short_circuit.sail b/test/c/short_circuit.sail
new file mode 100644
index 00000000..8289efa6
--- /dev/null
+++ b/test/c/short_circuit.sail
@@ -0,0 +1,22 @@
+
+$include <exception_basic.sail>
+$include <flow.sail>
+
+val print = "print_endline" : string -> unit
+
+val test : unit -> bool effect {escape}
+
+function test () = {
+  assert(false);
+  false
+}
+
+val main : unit -> unit effect {escape}
+
+function main () = {
+  if false & test() then {
+    print("unreachable");
+  } else {
+    print("ok");
+  }
+}
\ No newline at end of file
diff --git a/test/mono/.gitignore b/test/mono/.gitignore
index 2dd3daa3..bb7f92e1 100644
--- a/test/mono/.gitignore
+++ b/test/mono/.gitignore
@@ -1 +1 @@
-test-out
\ No newline at end of file
+test-output
\ No newline at end of file
diff --git a/test/mono/addsubexist.sail b/test/mono/addsubexist.sail
deleted file mode 100644
index f59f596e..00000000
--- a/test/mono/addsubexist.sail
+++ /dev/null
@@ -1,75 +0,0 @@
-(* Adapted from hand-written ARM model *)
-
-default Order dec
-typedef boolean = bit
-typedef reg_size   = bit[5]
-typedef reg_index = [|31|]
-
-val reg_size -> reg_index effect pure UInt_reg
-val unit -> unit effect pure (* probably not pure *) ReservedValue
-function forall Nat 'N. bit['N] NOT((bit['N]) x) = ~(x)
-val forall Nat 'M, Nat 'N. bit['M] -> bit['N] effect pure ZeroExtend
-val forall Nat 'N. (bit['N], bit['N], bit) -> (bit['N],bit[4]) effect pure AddWithCarry
-val forall Nat 'N, 'N IN {8,16,32,64}. (*broken? implicit<'N>*)unit -> bit['N] effect {rreg} rSP
-val forall Nat 'N, 'N IN {8,16,32,64}. ((*ditto implicit<'N>,*)reg_index) -> bit['N] effect {rreg}rX
-val (unit, bit[4]) -> unit effect {wreg} wPSTATE_NZCV
-val forall Nat 'N, 'N IN {32,64}. (unit, bit['N]) -> unit effect {rreg,wreg} wSP
-val forall Nat 'N, 'N IN {32,64}. (reg_index,bit['N]) -> unit effect {wreg} wX
-
-typedef ast = const union
-{
-  (exist 'R, 'R in {32,64}. (reg_index,reg_index,[:'R:],boolean,boolean,bit['R])) AddSubImmediate;
-}
-
-val ast -> unit effect {rreg,wreg(*,rmem,barr,eamem,wmv,escape*)} execute
-scattered function unit execute
-
-val bit[32] -> option<(ast)> effect pure decodeAddSubtractImmediate
-
-(* ADD/ADDS (immediate) *)
-(* SUB/SUBS (immediate) *)
-function option<(ast)> effect pure decodeAddSubtractImmediate ([sf]:[op]:[S]:0b10001:(bit[2]) shift:(bit[12]) imm12:(reg_size) Rn:(reg_size) Rd) =
-{
-  (reg_index) d := UInt_reg(Rd);
-  (reg_index) n := UInt_reg(Rn);
-  let (exist 'R, 'R in {32,64}. [:'R:]) 'datasize = if sf then 64 else 32 in {
-  (boolean) sub_op := op;
-  (boolean) setflags := S;
-  (bit['datasize]) imm := 0; (* ARM: uninitialized *)
-
-  switch shift {
-    case 0b00 -> imm := ZeroExtend(imm12)
-    case 0b01 -> imm := ZeroExtend(imm12 : (0b0 ^^ 12))
-    case [bitone,_] -> ReservedValue()
-  };
-
-  Some(AddSubImmediate( (d,n,datasize,sub_op,setflags,imm) ));
-}}
-
-function clause execute (AddSubImmediate('datasize)) = {
-switch datasize {
-case (d,n,datasize,sub_op,setflags,imm) ->
-{
-  (bit['datasize]) operand1 := if n == 31 then rSP() else rX(n);
-  (bit['datasize]) operand2 := imm;
-  (bit) carry_in := bitzero; (* ARM: uninitialized *)
-
-  if sub_op then {
-    operand2 := NOT(operand2);
-    carry_in := bitone;
-  }
-  else
-    carry_in := bitzero;
-
-  let (result,nzcv) = (AddWithCarry(operand1, operand2, carry_in)) in {
-
-    if setflags then
-      wPSTATE_NZCV() := nzcv;
-
-    if (d == 31 & ~(setflags)) then
-      wSP() := result
-    else
-      wX(d) := result;
-  }
-}}}
-end execute
diff --git a/test/mono/assert.sail b/test/mono/assert.sail
index 5b4a013a..91826822 100644
--- a/test/mono/assert.sail
+++ b/test/mono/assert.sail
@@ -1,7 +1,21 @@
+$include <smt.sail>
+$include <flow.sail>
+default Order dec
+type bits ('n : Int) = vector('n, dec, bit)
+val operator & = "and_bool" : (bool, bool) -> bool
+val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
+overload operator == = {eq_int, eq_vec}
+val mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int
+overload operator * = {mult_range, mult_int, mult_real}
+val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
+overload operator < = {lt_atom, lt_int}
+
+/* Tests set constraints in different constraints */
+
 val f : forall 'n 'm. (atom('n), atom('m)) -> unit effect {escape}
 
 function f(n,m) = {
-    assert(constraint('n in {8,16} & 'm < 'n));
+    assert(constraint('n in {8,16} & 'm < 'n), "nconstraint");
     let 'p = 2 * n in
     let x : bits('p) = replicate_bits(0b0,'p) in
     ()
@@ -10,7 +24,7 @@ function f(n,m) = {
 val g : forall 'n 'm. (atom('n), atom('m)) -> unit effect {escape}
 
 function g(n,m) = {
-    assert(constraint('n in {8,16}) & 'm < 'n);
+    assert(constraint('n in {8,16}) & 'm < 'n, "set and exp");
     let 'p = 2 * n in
     let x : bits('p) = replicate_bits(0b0,'p) in
     ()
@@ -18,8 +32,16 @@ function g(n,m) = {
 val h : forall 'n 'm. (atom('n), atom('m)) -> unit effect {escape}
 
 function h(n,m) = {
-    assert(('n == 8 | 'n == 16) & 'm < 'n);
+    assert(('n == 8 | 'n == 16) & 'm < 'n, "all exp");
     let 'p = 2 * n in
     let x : bits('p) = replicate_bits(0b0,'p) in
     ()
 }
+
+val run : unit -> unit effect {escape}
+
+function run () = {
+    f(8,3);
+    g(16,3);
+    h(8,3);
+}
\ No newline at end of file
diff --git a/test/mono/assert2.sail b/test/mono/assert2.sail
index 67e18f76..edf92710 100644
--- a/test/mono/assert2.sail
+++ b/test/mono/assert2.sail
@@ -1,3 +1,17 @@
+$include <smt.sail>
+$include <flow.sail>
+default Order dec
+type bits ('n : Int) = vector('n, dec, bit)
+val operator & = "and_bool" : (bool, bool) -> bool
+val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
+overload operator == = {eq_int, eq_vec}
+val mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int
+overload operator * = {mult_range, mult_int, mult_real}
+val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
+overload operator < = {lt_atom, lt_int}
+
+/* Should find a set constraint below the let */
+
 val f : forall 'n. atom('n) -> unit effect {escape}
 
 function f(n) = {
@@ -7,3 +21,11 @@ function f(n) = {
       ()
     }
 }
+
+
+val run : unit -> unit effect {escape}
+
+function run () = {
+    f(8);
+    f(16);
+}
\ No newline at end of file
diff --git a/test/mono/atomsplit.sail b/test/mono/atomsplit.sail
new file mode 100644
index 00000000..6e5d3e3b
--- /dev/null
+++ b/test/mono/atomsplit.sail
@@ -0,0 +1,30 @@
+$include <smt.sail>
+$include <flow.sail>
+default Order dec
+type bits ('n : Int) = vector('n, dec, bit)
+val operator & = "and_bool" : (bool, bool) -> bool
+val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
+overload operator == = {eq_int, eq_vec}
+val mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int
+overload operator * = {mult_range, mult_int, mult_real}
+val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
+overload operator < = {lt_atom, lt_int}
+
+/* Test splitting required because there's a size calculation in the function */
+
+val foo : forall 'n. atom('n) -> unit effect {escape}
+
+function foo(n) = {
+  assert(constraint('n in {2,4}));
+  let 'm = 8 * n in
+  let x : bits('m) = replicate_bits(0b0,m) in
+  let y : bits('n) = replicate_bits(0b0,n) in
+  ()
+}
+
+val run : unit -> unit effect {escape}
+
+function run () = {
+    foo(2);
+    foo(4);
+}
\ No newline at end of file
diff --git a/test/mono/castreq.sail b/test/mono/castreq.sail
index 3c03c452..5b155aa9 100644
--- a/test/mono/castreq.sail
+++ b/test/mono/castreq.sail
@@ -1,3 +1,25 @@
+$include <smt.sail>
+$include <flow.sail>
+default Order dec
+type bits ('n : Int) = vector('n, dec, bit)
+val operator & = "and_bool" : (bool, bool) -> bool
+val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
+overload operator == = {eq_int, eq_vec}
+val mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int
+overload operator * = {mult_range, mult_int, mult_real}
+val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
+overload operator < = {lt_atom, lt_int}
+val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+val extzv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure
+function extzv(v) = extz_vec(sizeof('m),v)
+val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append"} : forall ('n : Int) ('m : Int).
+  (bits('n), bits('m)) -> bits('n + 'm)
+overload append = {bitvector_concat}
+val bitvector_cast = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
+val bitvector_length = "length" : forall 'n. bits('n) -> atom('n)
+overload length = {bitvector_length}
+
+/* Test generation of casts across case splits (e.g., going from bits('m) to bits(32)) */
 
 val foo : forall 'm 'n, 'm in {8,16} & 'n in {32,64}. bits('m) -> bits('n) effect pure
 
@@ -41,6 +63,7 @@ function assign(x) = {
   r
 }
 
+/* Adding casts for top-level pattern matches is not yet supported
 
 val foo2 : forall 'm 'n, 'm in {8,16} & 'n in {32,64}. (atom('n), bits('m)) -> bits('n) effect pure
 
@@ -58,4 +81,19 @@ function bar2(8,x) =
 and bar2(16,x) =
   use(x)
 
-
+*/
+
+val run : unit -> unit effect {escape,undef}
+
+function run () = {
+    bar(0x12);
+    bar(0x3456);
+    assert((ret(0x34) : bits(32)) == 0x00340034);
+    assert((ret(0x34) : bits(64)) == 0x0034003400340034);
+    assert((ret(0x3456) : bits(32)) == 0x34563456);
+    assert((ret(0x3456) : bits(64)) == 0x3456345634563456);
+    assert((assign(0x12) : bits(32)) == 0x00120012);
+    assert((assign(0x1234) : bits(32)) == 0x12341234);
+    assert((assign(0x12) : bits(64)) == 0x0012001200120012);
+    assert((assign(0x1234) : bits(64)) == 0x1234123412341234);
+}
\ No newline at end of file
diff --git a/test/mono/control_deps.sail b/test/mono/control_deps.sail
index eaefd129..b94ffe2f 100644
--- a/test/mono/control_deps.sail
+++ b/test/mono/control_deps.sail
@@ -1,44 +1,76 @@
-(* Test monomorphisation control dependencies *)
-
+$include <smt.sail>
+$include <flow.sail>
 default Order dec
+type bits ('n : Int) = vector('n, dec, bit)
+val operator & = "and_bool" : (bool, bool) -> bool
+val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
+overload operator == = {eq_int, eq_vec}
+val mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int
+overload operator * = {mult_range, mult_int, mult_real}
+val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
+overload operator < = {lt_atom, lt_int}
+val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+val extz : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure
+function extz(v) = extz_vec(sizeof('m),v)
+val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append"} : forall ('n : Int) ('m : Int).
+  (bits('n), bits('m)) -> bits('n + 'm)
+overload append = {bitvector_concat}
+val bitvector_cast = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
+val bitvector_length = "length" : forall 'n. bits('n) -> atom('n)
+overload length = {bitvector_length}
+
+/* Test monomorphisation control dependencies */
 
-val (bool,bool) -> unit effect pure f
+val f : (bool,bool) -> unit
 
 function f(nosplit,split) = {
   if nosplit then {
-    let (exist 'x, true. [:'x:]) 'x = if split then 16 else 32 in
-    let (bit['x]) v = extz(0b0) in
+    let 'x : {'x, true. atom('x)} = if split then 16 else 32 in
+    let v : bits('x) = extz(0b0) in
     ()
   } else ()
 }
 
-val (bool,bool) -> unit effect pure g
+val g : (bool,bool) -> unit
 
 function g(split,nosplit) = {
-  (exist 'x, true. [:'x:]) x := 16;
-  (exist 'y, true. [:'y:]) y := 16;
+  x : {'x, true. atom('x)} = 16;
+  y : {'y, true. atom('y)} = 16;
   if split then
-    x := 32
+    x = 32
   else
     ();
   if nosplit then
-    y := 32
+    y = 32
   else
     ();
-  let (exist 'z, true. [:'z:]) 'z = x in
-  let (bit['z]) v = extz(0b0) in
+  let 'z : {'z, true. atom('z)} = x in
+  let v : bits('z)= extz(0b0) in
   ()
 }
 
-typedef exception = unit
+type exception = unit
 
-val bool -> unit effect {escape} h
+val h : bool -> unit effect {escape}
 
-(* Note: we don't really need to split on b, but it's awkward to avoid.
-   The important bit is not to overreact to the exception. *)
+/* Note: we don't really need to split on b, but it's awkward to avoid.
+   The important bit is not to overreact to the exception. */
+/* While the case splitting currently works, it doesn't yet generate a fake size
+   for 'x or remove the dead code that needs one
 function h(b) = {
-  let (exist 'x, true. [:'x:]) 'x =
+  let 'x : {'x, true. atom('x)} =
     if b then 16 else throw () in
-  let (bit['x]) v = extz(0b0) in
+  let v : bits('x) = extz(0b0) in
   ()
 }
+*/
+
+val run : unit -> unit /*effect {escape}*/
+
+function run () = {
+  f(false,false);
+  f(false,true);
+  g(false,false);
+  g(false,true);
+/*  h(true);*/
+}
\ No newline at end of file
diff --git a/test/mono/exint.sail b/test/mono/exint.sail
new file mode 100644
index 00000000..65589fb8
--- /dev/null
+++ b/test/mono/exint.sail
@@ -0,0 +1,57 @@
+$include <smt.sail>
+$include <flow.sail>
+default Order dec
+type bits ('n : Int) = vector('n, dec, bit)
+val operator & = "and_bool" : (bool, bool) -> bool
+val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
+overload operator == = {eq_int, eq_vec}
+val mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int
+overload operator * = {mult_range, mult_int, mult_real}
+val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
+overload operator < = {lt_atom, lt_int}
+val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+val extzv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure
+function extzv(v) = extz_vec(sizeof('m),v)
+val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append"} : forall ('n : Int) ('m : Int).
+  (bits('n), bits('m)) -> bits('n + 'm)
+overload append = {bitvector_concat}
+val bitvector_cast = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
+val bitvector_length = "length" : forall 'n. bits('n) -> atom('n)
+overload length = {bitvector_length}
+val cast ex_int : int -> {'n, true. atom('n)}
+function ex_int 'n = n
+
+
+/* Decode -> int -> existential test */
+
+val needssize : forall 'n, 'n >= 0. atom('n) -> unit effect pure
+
+function needssize(n) = {
+  let x : bits('n) = replicate_bits(0b0,n) in
+  ()
+}
+
+val test : bits(2) -> unit effect {undef,escape}
+
+function test(x) = {
+  n : int = undefined;
+  match x {
+    0b00 => n = 1,
+    0b01 => n = 2,
+    0b10 => n = 4,
+    0b11 => ()
+  };
+  let 'n2 = ex_int(n) in {
+    assert(constraint('n2 >= 0));
+    needssize(n2)
+  }
+}
+
+val run : unit -> unit effect {undef,escape}
+
+function run () = {
+  test(0b00);
+  test(0b01);
+  test(0b10);
+  test(0b11);
+}
\ No newline at end of file
diff --git a/test/mono/feature.sail b/test/mono/feature.sail
new file mode 100644
index 00000000..c7e13e11
--- /dev/null
+++ b/test/mono/feature.sail
@@ -0,0 +1,49 @@
+$include <smt.sail>
+$include <flow.sail>
+default Order dec
+type bits ('n : Int) = vector('n, dec, bit)
+val operator & = "and_bool" : (bool, bool) -> bool
+val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
+overload operator == = {eq_int, eq_vec}
+val mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int
+overload operator * = {mult_range, mult_int, mult_real}
+val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
+overload operator < = {lt_atom, lt_int}
+val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+val extzv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure
+function extzv(v) = extz_vec(sizeof('m),v)
+val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append"} : forall ('n : Int) ('m : Int).
+  (bits('n), bits('m)) -> bits('n + 'm)
+overload append = {bitvector_concat}
+val bitvector_cast = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
+val bitvector_length = "length" : forall 'n. bits('n) -> atom('n)
+overload length = {bitvector_length}
+
+/* Inlining feature test functions, as in aarch64 */
+
+val HaveSomeFeature : unit -> bool
+
+function HaveSomeFeature () = return(true)
+
+val foo : bits(1) -> unit effect {escape, undef}
+
+function foo(x) = {
+  let i : int =
+    match x {
+    0b0 => 8,
+    0b1 => if HaveSomeFeature() then 16 else undefined
+    }
+  in
+  let 'n = i in {
+    assert(constraint('n >= 0));
+    let y : bits('n) = replicate_bits(0b0, n) in
+    ()
+  }
+}
+
+val run : unit -> unit effect {escape, undef}
+
+function run () = {
+    foo(0b0);
+    foo(0b1);
+}
\ No newline at end of file
diff --git a/test/mono/fnreduce.sail b/test/mono/fnreduce.sail
index f39fb87d..cd58e71a 100644
--- a/test/mono/fnreduce.sail
+++ b/test/mono/fnreduce.sail
@@ -1,69 +1,86 @@
-(* Test constant propagation part of monomorphisation involving
+val add_int = {ocaml: "add_int", lem: "integerAdd"} : (int, int) -> int
+overload operator + = {add_int}
+val eq_int = {ocaml: "eq_int", lem: "eq"} : (int, int) -> bool
+val eq_anything = {ocaml: "(fun (x, y) -> x = y)", lem: "eq"} : forall ('a : Type). ('a, 'a) -> bool
+overload operator == = {eq_int, eq_anything}
+
+
+/* Test constant propagation part of monomorphisation involving
    functions.  We should reduce a function application when the
    arguments are suitable values, the function is pure and the result
    is a value.
- *)
+ */
 
-typedef AnEnum = enumerate { One; Two; Three }
+enum AnEnum = One | Two | Three
 
-typedef EnumlikeUnion = const union { First; Second }
+union EnumlikeUnion = { First, Second }
 
-typedef ProperUnion = const union {
-  (AnEnum) Stuff;
-  (EnumlikeUnion) Nonsense;
+union ProperUnion = {
+  Stuff : AnEnum,
+  Nonsense : EnumLikeUnion
 }
 
-function AnEnum canReduce ((AnEnum) x) = {
-  switch (x) {
-  case One -> Two
-  case x -> x
+val canReduce : AnEnum -> AnEnum
+
+function canReduce (x) = {
+  match (x) {
+  One => Two,
+  x => x
   }
 }
 
-function nat cannotReduce ((AnEnum) x) = {
-  let (nat) y = switch (x) { case One -> 1 case _ -> 5 } in
+val cannotReduce : AnEnum -> int
+
+function cannotReduce (x) = {
+  let y : int = match (x) { One => 1, _ => 5 } in
   2 + y
 }
 
-function AnEnum effect {rreg} fakeUnpure ((AnEnum) x) = {
-  switch (x) {
-  case One -> Two
-  case x -> x
+register whatever : int
+
+val impure : AnEnum -> AnEnum effect {rreg}
+
+function impure (x) = {
+  match (x) {
+  One => Two,
+  x => let _ = whatever in x
   }
 }
 
-function EnumlikeUnion canReduceUnion ((AnEnum) x) = {
-  switch (x) {
-  case One -> First
-  case _ -> Second
+val canReduceUnion : AnEnum -> EnumlikeUnion
+
+function canReduceUnion (x) = {
+  match (x) {
+  One => First,
+  _ => Second
   }
 }
 
-function ProperUnion canReduceUnion2 ((AnEnum) x) = {
-  switch (x) {
-  case One -> Nonsense(First)
-  case y -> Stuff(y)
+val canReduceUnion2 : AnEnum -> ProperUnion
+
+function canReduceUnion2 (x) = {
+  match (x) {
+  One => Nonsense(First),
+  y => Stuff(y)
   }
 }
 
-(* FIXME LATER: once effect handling is in place we should get an error
-   because this isn't pure *)
 
-val AnEnum -> (AnEnum,nat,AnEnum,EnumlikeUnion,ProperUnion) effect pure test
+val test : AnEnum -> (AnEnum,int,AnEnum,EnumlikeUnion,ProperUnion) effect {rreg}
 
 function test (x) = {
   let a = canReduce(x) in
   let b = cannotReduce(x) in
-  let c = fakeUnpure(x) in
+  let c = impure(x) in
   let d = canReduceUnion(x) in
   let e = canReduceUnion2(x) in
   (a,b,c,d,e)
 }
 
-val unit -> bool effect pure run
+val run : unit -> unit effect {rreg,escape}
 
 function run () = {
-  test(One) == (Two,3,Two,First,Nonsense(First)) &
-  test(Two) == (Two,7,Two,Second,Stuff(Two)) &
-  test(Three) == (Three,7,Three,Second,Stuff(Three))
+  assert(test(One) == (Two,3,Two,First,Nonsense(First)));
+  assert(test(Two) == (Two,7,Two,Second,Stuff(Two)));
+  assert(test(Three) == (Three,7,Three,Second,Stuff(Three)));
 }
diff --git a/test/mono/pass/assert b/test/mono/pass/assert
new file mode 100644
index 00000000..f24b885a
--- /dev/null
+++ b/test/mono/pass/assert
@@ -0,0 +1 @@
+assert.sail -auto_mono
\ No newline at end of file
diff --git a/test/mono/pass/assert2 b/test/mono/pass/assert2
new file mode 100644
index 00000000..491a98b6
--- /dev/null
+++ b/test/mono/pass/assert2
@@ -0,0 +1 @@
+assert2.sail -auto_mono
\ No newline at end of file
diff --git a/test/mono/pass/atomsplit b/test/mono/pass/atomsplit
new file mode 100644
index 00000000..d224fcfd
--- /dev/null
+++ b/test/mono/pass/atomsplit
@@ -0,0 +1 @@
+atomsplit.sail -auto_mono
\ No newline at end of file
diff --git a/test/mono/pass/castreq b/test/mono/pass/castreq
new file mode 100644
index 00000000..e2fc1d55
--- /dev/null
+++ b/test/mono/pass/castreq
@@ -0,0 +1 @@
+castreq.sail -auto_mono -undefined_gen
\ No newline at end of file
diff --git a/test/mono/pass/control_deps b/test/mono/pass/control_deps
new file mode 100644
index 00000000..e173c42f
--- /dev/null
+++ b/test/mono/pass/control_deps
@@ -0,0 +1 @@
+control_deps.sail -auto_mono
\ No newline at end of file
diff --git a/test/mono/pass/exint b/test/mono/pass/exint
new file mode 100644
index 00000000..8de7c0bf
--- /dev/null
+++ b/test/mono/pass/exint
@@ -0,0 +1 @@
+exint.sail -auto_mono -undefined_gen
\ No newline at end of file
diff --git a/test/mono/pass/feature b/test/mono/pass/feature
new file mode 100644
index 00000000..9363dd68
--- /dev/null
+++ b/test/mono/pass/feature
@@ -0,0 +1 @@
+feature -auto_mono -undefined_gen
\ No newline at end of file
diff --git a/test/mono/pass/feature_no_effects b/test/mono/pass/feature_no_effects
new file mode 100644
index 00000000..098d7f94
--- /dev/null
+++ b/test/mono/pass/feature_no_effects
@@ -0,0 +1 @@
+feature.sail -auto_mono -undefined_gen -no_effects
diff --git a/test/mono/pass/fnreduce b/test/mono/pass/fnreduce
new file mode 100644
index 00000000..4237c34a
--- /dev/null
+++ b/test/mono/pass/fnreduce
@@ -0,0 +1 @@
+fnreduce.sail -auto_mono
\ No newline at end of file
diff --git a/test/mono/pass/fnreduce_manual b/test/mono/pass/fnreduce_manual
new file mode 100644
index 00000000..25d8256c
--- /dev/null
+++ b/test/mono/pass/fnreduce_manual
@@ -0,0 +1 @@
+fnreduce.sail -mono_split fnreduce.sail:43:x
\ No newline at end of file
diff --git a/test/mono/pass/set b/test/mono/pass/set
new file mode 100644
index 00000000..700d1752
--- /dev/null
+++ b/test/mono/pass/set
@@ -0,0 +1 @@
+set.sail -auto_mono
diff --git a/test/mono/pass/time8_continue b/test/mono/pass/time8_continue
new file mode 100644
index 00000000..eb8d043b
--- /dev/null
+++ b/test/mono/pass/time8_continue
@@ -0,0 +1 @@
+times8.sail -auto_mono -dmono_continue -dall_split_errors
\ No newline at end of file
diff --git a/test/mono/pass/times8 b/test/mono/pass/times8
new file mode 100644
index 00000000..1315855d
--- /dev/null
+++ b/test/mono/pass/times8
@@ -0,0 +1 @@
+times8.sail -auto_mono
\ No newline at end of file
diff --git a/test/mono/pass/times8div8 b/test/mono/pass/times8div8
new file mode 100644
index 00000000..5f3a973f
--- /dev/null
+++ b/test/mono/pass/times8div8
@@ -0,0 +1 @@
+times8div8.sail -auto_mono -undefined_gen
diff --git a/test/mono/pass/union-exist b/test/mono/pass/union-exist
new file mode 100644
index 00000000..ebb89267
--- /dev/null
+++ b/test/mono/pass/union-exist
@@ -0,0 +1 @@
+union-exist.sail -auto_mono
diff --git a/test/mono/pass/union-exist_manual b/test/mono/pass/union-exist_manual
new file mode 100644
index 00000000..d35c3d48
--- /dev/null
+++ b/test/mono/pass/union-exist_manual
@@ -0,0 +1 @@
+union-exist.sail -mono_split union-exist.sail:9:v
\ No newline at end of file
diff --git a/test/mono/pass/varmatch b/test/mono/pass/varmatch
new file mode 100644
index 00000000..e1402863
--- /dev/null
+++ b/test/mono/pass/varmatch
@@ -0,0 +1 @@
+varmatch.sail -auto_mono
diff --git a/test/mono/pass/varmatch_manual b/test/mono/pass/varmatch_manual
new file mode 100644
index 00000000..f2870060
--- /dev/null
+++ b/test/mono/pass/varmatch_manual
@@ -0,0 +1 @@
+varmatch.sail -mono_split varmatch.sail:7:x
\ No newline at end of file
diff --git a/test/mono/pass/vector b/test/mono/pass/vector
new file mode 100644
index 00000000..82435ef5
--- /dev/null
+++ b/test/mono/pass/vector
@@ -0,0 +1 @@
+vector.sail -auto_mono
diff --git a/test/mono/pass/vector_manual b/test/mono/pass/vector_manual
new file mode 100644
index 00000000..d0712dbc
--- /dev/null
+++ b/test/mono/pass/vector_manual
@@ -0,0 +1 @@
+vector.sail -mono_split vector.sail:7:sel
\ No newline at end of file
diff --git a/test/mono/run_tests.sh b/test/mono/run_tests.sh
new file mode 100755
index 00000000..4be1f434
--- /dev/null
+++ b/test/mono/run_tests.sh
@@ -0,0 +1,103 @@
+#!/usr/bin/env bash
+set -e
+
+DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
+SAILDIR="$DIR/../.."
+TESTSDIR="$DIR"
+OUTPUTDIR="$DIR/test-output"
+
+RED='\033[0;31m'
+GREEN='\033[0;32m'
+YELLOW='\033[0;33m'
+NC='\033[0m'
+
+rm -f $DIR/tests.xml
+
+pass=0
+fail=0
+
+XML=""
+
+function green {
+    (( pass += 1 ))
+    printf "$1: ${GREEN}$2${NC}\n"
+    XML+="    <testcase name=\"$1\"/>\n"
+}
+
+function yellow {
+    (( fail += 1 ))
+    printf "$1: ${YELLOW}$2${NC}\n"
+    XML+="    <testcase name=\"$1\">\n      <error message=\"$2\">$2</error>\n    </testcase>\n"
+}
+
+function red {
+    (( fail += 1 ))
+    printf "$1: ${RED}$2${NC}\n"
+    XML+="    <testcase name=\"$1\">\n      <error message=\"$2\">$2</error>\n    </testcase>\n"
+}
+
+function finish_suite {
+    printf "$1: Passed ${pass} out of $(( pass + fail ))\n\n"
+    XML="  <testsuite name=\"$1\" tests=\"$(( pass + fail ))\" failures=\"${fail}\" timestamp=\"$(date)\">\n$XML  </testsuite>\n"
+    printf "$XML" >> "$DIR/tests.xml"
+    XML=""
+    pass=0
+    fail=0
+}
+
+printf "<testsuites>\n" >> "$DIR/tests.xml"
+
+cd "$DIR"
+mkdir -p "$OUTPUTDIR"
+
+echo > log
+
+for i in `ls $TESTSDIR/pass`;
+do
+    echo "Running test $i" >> log
+    cd "$DIR"
+    if "$SAILDIR/sail" -lem -lem_mwords -lem_lib Test_extra -o out $(< "$TESTSDIR/pass/$i") &>>log;
+    then
+        mv out.lem out_types.lem "$OUTPUTDIR"
+	if lem -ocaml -lib "$SAILDIR/src/lem_interp" \
+               -outdir "$OUTPUTDIR" \
+               "$SAILDIR/src/gen_lib/sail_values.lem" \
+               "$SAILDIR/src/gen_lib/sail_operators.lem" \
+               "$SAILDIR/src/gen_lib/sail_operators_mwords.lem" \
+               "$SAILDIR/src/lem_interp/sail_instr_kinds.lem" \
+               "$SAILDIR/src/gen_lib/prompt.lem" \
+               "$SAILDIR/src/gen_lib/state_monad.lem" \
+               "$SAILDIR/src/gen_lib/state.lem" \
+               "$SAILDIR/src/gen_lib/prompt_monad.lem" \
+               "$DIR/test_extra.lem" \
+               "$OUTPUTDIR/out_types.lem" "$OUTPUTDIR/out.lem" &>>log;
+	then
+            cd "$OUTPUTDIR"
+            if ocamlfind ocamlc -linkpkg -package zarith -package lem \
+                         sail_values.ml sail_operators.ml \
+                         sail_operators_mwords.ml sail_instr_kinds.ml \
+                         prompt_monad.ml prompt.ml state_monad.ml state.ml \
+                         test_extra.ml out_types.ml out.ml ../test.ml \
+                         -o test &>>log
+            then
+                if ./test &>>log
+                then
+	            green "tested $i expecting pass" "pass"
+                else
+	            red "tested $i expecting pass" "running generated test failed"
+                fi
+            else
+	        red "tested $i expecting pass" "compiling generated OCaml failed"
+            fi
+	else
+	    red "tested $i expecting pass" "failed to generate OCaml from Lem"
+	fi
+    else
+	red "tested $i expecting pass" "failed to generate Lem"
+    fi
+    echo >> log
+done
+
+finish_suite "monomorphisation tests"
+
+printf "</testsuites>\n" >> $DIR/tests.xml
diff --git a/test/mono/set.sail b/test/mono/set.sail
index ecc06137..b7cf4862 100644
--- a/test/mono/set.sail
+++ b/test/mono/set.sail
@@ -1,29 +1,45 @@
 default Order dec
-
-(* A function which is merely parametrised by a size does not need to be
-   monomorphised *)
-
-val forall 'n, 'n in {32,64}. [:'n:] -> bit[64] effect pure parametric
+type bits ('n : Int) = vector('n, dec, bit)
+val operator & = "and_bool" : (bool, bool) -> bool
+val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
+val eq_int = {ocaml: "eq_int", lem: "eq"} : (int, int) -> bool
+overload operator == = {eq_int, eq_vec}
+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 mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int
+overload operator * = {mult_range, mult_int, mult_real}
+val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+val extz : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure
+function extz(v) = extz_vec(sizeof('m),v)
+val "exts_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+val exts : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure
+function exts(v) = exts_vec(sizeof('m),v)
+
+/* A function which is merely parametrised by a size does not need to be
+   monomorphised */
+
+val parametric : forall 'n, 'n in {32,64}. atom('n) -> bits(64)
 
 function parametric(n) = {
-  let (bit['n]) x = exts(0x80000000) in
+  let x : bits('n) = exts(0x80000000) in
   extz(x)
 }
 
-(* But if we do a calculation on the size then we'll need to case split *)
+/* But if we do a calculation on the size then we'll need to case split */
 
-val forall 'n, 'n in {16,32}. [:'n:] -> bit[64] effect pure depends
+val depends : forall 'n, 'n in {16,32}. atom('n) -> bits(64)
 
 function depends(n) = {
   let 'm = 2 * n in
-  let (bit['m]) x = exts(0x80000000) in
+  let x : bits('m) = exts(0x80000000) in
   extz(x)
 }
 
-val unit -> bool effect pure run
+val run : unit -> unit effect {escape}
 
-function run () =
-  parametric(32) == 0x0000000080000000 &
-  parametric(64) == 0xffffffff80000000 &
-  depends(16) == 0x0000000080000000 &
-  depends(32) == 0xffffffff80000000
+function run () = {
+  assert(parametric(32) == 0x0000000080000000);
+  assert(parametric(64) == 0xffffffff80000000);
+  assert(depends(16) == 0x0000000080000000);
+  assert(depends(32) == 0xffffffff80000000);
+}
diff --git a/test/mono/test.ml b/test/mono/test.ml
index f99abfb8..32d3b2ed 100644
--- a/test/mono/test.ml
+++ b/test/mono/test.ml
@@ -1 +1,3 @@
-if Testout_embed_sequential.run() then print_endline "OK" else print_endline "Failed";;
+match Out.run() with
+| Done _ -> exit 0
+| _ -> exit 1
diff --git a/test/mono/test.sh b/test/mono/test.sh
deleted file mode 100755
index 2a5aa80b..00000000
--- a/test/mono/test.sh
+++ /dev/null
@@ -1,44 +0,0 @@
-#!/bin/bash
-
-set -e
-
-DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
-SAILDIR="$DIR/../.."
-LEMDIR="$DIR/../../../lem"
-OUTDIR="$DIR/test-out"
-ZARITH="$LEMDIR/ocaml-lib/dependencies/zarith"
-
-if [ ! -d "$OUTDIR" ]; then
-  mkdir -- "$OUTDIR"
-fi
-cd "$OUTDIR"
-
-TESTONLY="$1"
-if [ -n "$TESTONLY" ]; then shift; fi
-
-LOG="$DIR/log"
-date > "$LOG"
-
-exec 3< "$DIR/tests"
-set +e
-
-while read -u 3 TEST ARGS; do
-  if [ -z "$TESTONLY" -o "$TEST" = "$TESTONLY" ]; then
-#    echo "$TEST ocaml"
-#    rm -f -- "$OUTDIR"/*
-#    "$SAILDIR/sail" -ocaml "$SAILDIR/lib/prelude.sail" "$SAILDIR/lib/prelude_wrappers.sail" "$DIR/$TEST" -o "$OUTDIR/testout" $ARGS
-#    cp -- "$SAILDIR"/src/gen_lib/sail_values.ml .
-#    cp -- "$DIR"/test.ml .
-#    ocamlc -I "$ZARITH" "$ZARITH/zarith.cma" -dllpath "$ZARITH" -I "$LEMDIR/ocaml-lib" "$LEMDIR/ocaml-lib/extract.cma" -I "$SAILDIR/src/_build/lem_interp" "$SAILDIR/src/_build/lem_interp/extract.cma" sail_values.ml testout.ml test.ml -o test
-#    ./test
-   
-    echo "$TEST lem - ocaml" | tee -a -- "$LOG"
-    rm -f -- "$OUTDIR"/*
-    "$SAILDIR/sail" -lem -lem_sequential -lem_mwords "$SAILDIR/lib/prelude.sail" "$SAILDIR/lib/prelude_wrappers.sail" "$DIR/$TEST".sail -o "$OUTDIR/testout" $ARGS $@ &>> "$LOG" && \
-    "$LEMDIR/bin/lem" -ocaml -lib "$SAILDIR/src/lem_interp" "$SAILDIR/src/gen_lib/sail_values.lem" "$SAILDIR/src/gen_lib/sail_operators_mwords.lem" "$SAILDIR/src/gen_lib/state.lem" testout_embed_types_sequential.lem testout_embed_sequential.lem -outdir "$OUTDIR" &>> "$LOG" && \
-    cp -- "$DIR"/test.ml "$OUTDIR" && \
-    ocamlc -I "$ZARITH" "$ZARITH/zarith.cma" -dllpath "$ZARITH" -I "$LEMDIR/ocaml-lib" "$LEMDIR/ocaml-lib/extract.cma" -I "$SAILDIR/src/_build/lem_interp" "$SAILDIR/src/_build/lem_interp/extract.cma" sail_values.ml sail_operators_mwords.ml state.ml testout_embed_types_sequential.ml testout_embed_sequential.ml test.ml -o test &>> "$LOG" && \
-    ./test |& tee -a -- "$LOG" || \
-      (echo "Failed:"; echo; tail -- "$LOG"; echo; echo)
-  fi
-done
diff --git a/test/mono/tests b/test/mono/tests
index 27e161cf..f5d5306b 100644
--- a/test/mono/tests
+++ b/test/mono/tests
@@ -1,9 +1,20 @@
-fnreduce -mono-split fnreduce.sail:43:x
-varmatch -mono-split varmatch.sail:7:x
-vector -mono-split vector.sail:7:sel
-union-exist -mono-split union-exist.sail:9:v
+fnreduce -mono_split fnreduce.sail:43:x
+varmatch -mono_split varmatch.sail:7:x
+vector -mono_split vector.sail:7:sel
+union-exist -mono_split union-exist.sail:9:v
 fnreduce -auto_mono
 varmatch -auto_mono
 vector -auto_mono
 union-exist -auto_mono
 set -auto_mono
+assert -auto_mono
+assert2 -auto_mono
+atomsplit -auto_mono
+castreq -auto_mono -undefined_gen
+control_deps -auto_mono
+exint -auto_mono -undefined_gen
+feature -auto_mono -undefined_gen -no_effects
+feature -auto_mono -undefined_gen
+times8div8 -auto_mono -undefined_gen
+times8 -auto_mono
+times8 -auto_mono -dmono_continue -dall_split_errors
diff --git a/test/mono/times8.sail b/test/mono/times8.sail
new file mode 100644
index 00000000..56b1d209
--- /dev/null
+++ b/test/mono/times8.sail
@@ -0,0 +1,42 @@
+$include <smt.sail>
+$include <flow.sail>
+default Order dec
+type bits ('n : Int) = vector('n, dec, bit)
+val operator & = "and_bool" : (bool, bool) -> bool
+val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
+overload operator == = {eq_int, eq_vec}
+val mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int
+overload operator * = {mult_range, mult_int, mult_real}
+val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
+overload operator < = {lt_atom, lt_int}
+val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+val extzv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure
+function extzv(v) = extz_vec(sizeof('m),v)
+val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append"} : forall ('n : Int) ('m : Int).
+  (bits('n), bits('m)) -> bits('n + 'm)
+overload append = {bitvector_concat}
+val bitvector_cast = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
+val bitvector_length = "length" : forall 'n. bits('n) -> atom('n)
+overload length = {bitvector_length}
+val cast ex_int : int -> {'n, true. atom('n)}
+function ex_int 'n = n
+
+/* Another byte/bit size conversion */
+
+val bar : forall 'n. atom('n) -> bits(8 * 'n) effect pure
+
+function bar (n) = replicate_bits(0x12,n)
+
+val foo : forall 'size, 8 * 'size >= 0. atom('size) -> bits(8 * 'size) effect {escape}
+
+function foo(size) = {
+  assert('size == 1 | 'size == 2, "size");
+  return bar('size)
+}
+
+val run : unit -> unit effect {escape}
+
+function run () = {
+  assert(foo(1) == 0x12);
+  assert(foo(2) == 0x1212);
+}
\ No newline at end of file
diff --git a/test/mono/times8div8.sail b/test/mono/times8div8.sail
new file mode 100644
index 00000000..240bbfc6
--- /dev/null
+++ b/test/mono/times8div8.sail
@@ -0,0 +1,66 @@
+$include <smt.sail>
+$include <flow.sail>
+default Order dec
+type bits ('n : Int) = vector('n, dec, bit)
+val operator & = "and_bool" : (bool, bool) -> bool
+val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
+overload operator == = {eq_int, eq_vec}
+val mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int
+overload operator * = {mult_range, mult_int, mult_real}
+val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
+overload operator < = {lt_atom, lt_int}
+val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+val extzv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure
+function extzv(v) = extz_vec(sizeof('m),v)
+val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append"} : forall ('n : Int) ('m : Int).
+  (bits('n), bits('m)) -> bits('n + 'm)
+overload append = {bitvector_concat}
+val bitvector_cast = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
+val bitvector_length = "length" : forall 'n. bits('n) -> atom('n)
+overload length = {bitvector_length}
+val cast ex_int : int -> {'n, true. atom('n)}
+function ex_int 'n = n
+val quotient = {ocaml: "quotient", lem: "integerDiv", c: "div_int"} : (int, int) -> int
+overload operator / = {quotient}
+
+/* Byte/bits size conversions are a pain */
+
+val accept : forall 'n. (atom('n), bits(8 * 'n)) -> unit
+
+function accept (_,_) = ()
+
+val f : forall 'n. atom('n) -> unit effect {escape,undef}
+
+function f(n) = {
+    assert(constraint('n in {8,16}));
+    x : bits('n) = undefined;
+    let 'm : {'o, true. atom('o)} = ex_int(n / 8) in {
+        assert(constraint(8 * 'm = 'n));
+        x = replicate_bits(0b00000000,'m);
+        accept(m,x);
+        accept(m,replicate_bits(0b00000000,'m));
+    }
+}
+
+val accept2 : forall 'n. bits('n) -> unit
+
+function accept2 (_) = ()
+
+val g : forall 'm 'n. (atom('m), atom('n), bits('n)) -> unit effect {escape}
+
+function g(m,n,v) = {
+  assert(constraint('m >= 0 & 'n >= 0));
+  let 'o : {'p, true. atom('p)} = ex_int(m / n) in {
+    assert(constraint('o * 'n = 'm));
+    accept2(replicate_bits(v,o))
+  }
+}
+
+val run : unit -> unit effect {escape, undef}
+
+function run () = {
+    f(8);
+    f(16);
+    g(16,8,0x12);
+    g(32,32,0x12345678);
+}
diff --git a/test/mono/union-exist.sail b/test/mono/union-exist.sail
index 74ab429a..f1e01e75 100644
--- a/test/mono/union-exist.sail
+++ b/test/mono/union-exist.sail
@@ -1,33 +1,38 @@
 default Order dec
+type bits ('n : Int) = vector('n, dec, bit)
+val operator & = "and_bool" : (bool, bool) -> bool
+val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
+val eq_int = {ocaml: "eq_int", lem: "eq"} : (int, int) -> bool
+overload operator == = {eq_int, eq_vec}
+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))
 
-typedef myunion = const union {
-  (exist 'n, 'n in {8,16}. ([:'n:],bit['n])) MyConstr;
+
+union myunion = {
+  MyConstr : {'n, 'n in {8,16}. (atom('n),bits('n))}
 }
 
-val bit[2] -> myunion effect pure make
+val make : bits(2) -> myunion
 
 function make(v) =
-  (* Can't mention these below without running into exp/nexp parsing conflict! *)
+  /* Can't mention these below without running into exp/nexp parsing conflict! */
   let eight = 8 in let sixteen = 16 in
-  switch v {
-    case 0b00 -> MyConstr( (  eight,  0x12) )
-    case 0b01 -> MyConstr( (sixteen,0x1234) )
-    case 0b10 -> MyConstr( (  eight,  0x56) )
-    case 0b11 -> MyConstr( (sixteen,0x5678) )
-  }
-
-val myunion -> bit[32] effect pure use
-
-function use(MyConstr('n)) = {
-  switch n {
-    case (n,v) -> extz(v)
-  }
-}
-val unit -> bool effect pure run
+  let r : {'n, 'n in {8,16}. (atom('n),bits('n))} = match v {
+    0b00 => (  eight,  0x12),
+    0b01 => (sixteen,0x1234),
+    0b10 => (  eight,  0x56),
+    0b11 => (sixteen,0x5678)
+  } in MyConstr(r)
+
+val use : myunion -> bits(32)
+
+function use(MyConstr((n,v) as (atom('n),bits('n)))) = extz(v)
+
+val run : unit -> unit effect {escape}
 
 function run () = {
-  use(make(0b00)) == 0x00000012 &
-  use(make(0b01)) == 0x00001234 &
-  use(make(0b10)) == 0x00000056 &
-  use(make(0b11)) == 0x00005678
+  assert(use(make(0b00)) == 0x00000012);
+  assert(use(make(0b01)) == 0x00001234);
+  assert(use(make(0b10)) == 0x00000056);
+  assert(use(make(0b11)) == 0x00005678);
 }
diff --git a/test/mono/varmatch.sail b/test/mono/varmatch.sail
index 7d2b9b73..c3c2994d 100644
--- a/test/mono/varmatch.sail
+++ b/test/mono/varmatch.sail
@@ -1,19 +1,24 @@
-(* Check that when we case split on a variable that the constant propagation
-   handles the default case correctly. *)
+val operator & = "and_bool" : (bool, bool) -> bool
+val operator == = {ocaml: "(fun (x, y) -> x = y)", lem: "eq"} : forall ('a : Type). ('a, 'a) -> bool
 
-typedef AnEnum = enumerate { One; Two; Three }
+/* Check that when we case split on a variable that the constant propagation
+   handles the default case correctly. */
 
-function AnEnum foo((AnEnum) x) = {
-  switch (x) {
-  case One -> Two
-  case y -> y
+enum AnEnum = One | Two | Three
+
+val foo : AnEnum -> AnEnum
+
+function foo(x) = {
+  match (x) {
+  One => Two,
+  y => y
   }
 }
 
-val unit -> bool effect pure run
+val run : unit -> unit effect {escape}
 
 function run () = {
-  foo(One) == Two &
-  foo(Two) == Two &
-  foo(Three) == Three
+  assert(foo(One) == Two);
+  assert(foo(Two) == Two);
+  assert(foo(Three) == Three);
 }
diff --git a/test/mono/vector.sail b/test/mono/vector.sail
index 03f36da5..93cc2d41 100644
--- a/test/mono/vector.sail
+++ b/test/mono/vector.sail
@@ -1,21 +1,28 @@
-(* Check case splitting on a vector *)
-
 default Order dec
+type bits ('n : Int) = vector('n, dec, bit)
+val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
+val eq_int = {ocaml: "eq_int", lem: "eq"} : (int, int) -> bool
+overload operator == = {eq_int, eq_vec}
+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))
+
+
+/* Check case splitting on a vector */
 
-val bit[32] -> nat effect pure test
+val test : bits(32) -> nat
 
-function nat test((bit[2]) sel : (bit[30]) _) = {
-  switch (sel) {
-    case 0b00 -> 5
-    case 0b10 -> 1
-    case _ -> 0
+function test((sel : bits(2)) @ (_ : bits(30))) = {
+  match (sel) {
+    0b00 => 5,
+    0b10 => 1,
+    _ => 0
   }
 }
 
-val unit -> bool effect pure run
+val run : unit -> unit effect {escape}
 
 function run () = {
-  test(0x0f353533) == 5 &
-  test(0x84534656) == 1 &
-  test(0xf3463903) == 0
+  assert(test(0x0f353533) == 5);
+  assert(test(0x84534656) == 1);
+  assert(test(0xf3463903) == 0);
 }