Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into mono-experiments

38 files changed, 1652 insertions, 482 deletions

diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail
index 0a286070..101414f8 100644
--- a/cheri/cheri_insts.sail
+++ b/cheri/cheri_insts.sail
@@ -73,7 +73,7 @@ function clause execute (CGetType(rd, cb)) =
     let capVal = readCapReg(cb) in
     wGPR(rd) := if (capVal.sealed)
       then EXTZ(capVal.otype)
-      else -1
+      else (bitone ^^ 64)
   (* END_CGetType *)
 }
 
@@ -110,8 +110,9 @@ function clause execute (CGetLen(rd, cb)) =
   else
     let capVal = readCapReg(cb) in
     let len65  = getCapLength(capVal) in
-    let len64  = (if len65 > MAX_U64 then MAX_U64 else len65) in
-    wGPR(rd) := (bit[64]) len64;
+    wGPR(rd) := (if len65 > MAX_U64 then MAX_U64 else len65);
+    (*let (uint64) len64 = (if len65 > MAX_U64 then MAX_U64 else len65) in
+    wGPR(rd) := (bit[64]) len64;*)
   (* END_CGetLen *)
 }
 
@@ -123,7 +124,7 @@ function clause execute (CGetTag(rd, cb)) =
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
   else
     let capVal = readCapReg(cb) in
-    wGPR(rd) := EXTZ(capVal.tag);
+    wGPR(rd) := EXTZ([capVal.tag]);
   (* END_CGetTag *)
 }
 
@@ -135,7 +136,7 @@ function clause execute (CGetSealed(rd, cb)) =
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
   else
     let capVal = readCapReg(cb) in
-    wGPR(rd) := EXTZ(capVal.sealed);
+    wGPR(rd) := EXTZ([capVal.sealed]);
   (* END_CGetSealed *)
 }
 
@@ -150,7 +151,7 @@ function clause execute (CGetPCC(cd)) =
   else
     let pcc = (capRegToCapStruct(PCC)) in
     let (success, pcc2) = setCapOffset(pcc, PC) in
-    {assert (success, None); (* guaranteed to be in-bounds *)
+    {assert (success, ""); (* guaranteed to be in-bounds *)
     writeCapReg(cd, pcc2)};
   (* END_CGetPCC *)
 }
@@ -279,7 +280,7 @@ function clause execute(CSub(rd, cb, ct)) =
     raise_c2_exception(CapEx_AccessSystemRegsViolation, ct)
   else 
     {
-      wGPR(rd) := (bit[64])(getCapCursor(cb_val) - getCapCursor(ct_val))
+      wGPR(rd) := (bit[64])(to_svec(getCapCursor(cb_val) - getCapCursor(ct_val)))
     }
   (* END_CSub *)
 }
@@ -325,7 +326,7 @@ function clause execute(CPtrCmp(rd, cb, ct, op)) =
           ltu     := (cursor1 < cursor2);
           lts     := (((bit[64])cursor1) <_s ((bit[64])cursor2));
         };
-      wGPR(rd) := EXTZ(switch (op) {
+      wGPR(rd) := EXTZ ((bool[1]) (switch (op) {
         case CEQ   -> [equal]
         case CNE   -> [not (equal)]
         case CLT   -> [lts]
@@ -334,7 +335,7 @@ function clause execute(CPtrCmp(rd, cb, ct, op)) =
         case CLEU  -> [ltu | equal]
         case CEXEQ -> [cb_val == ct_val]
         case CNEXEQ -> [cb_val != ct_val]
-      })
+      }))
     }
   (* END_CPtrCmp *)
 }
@@ -574,8 +575,8 @@ function clause execute (CBuildCap(cd, cb, ct)) =
     let (representable, cd2) = setCapOffset(cd1, (bit[64]) ct_offset) in
     let cd3 = setCapPerms(cd2, ct_perms) in
     {
-      assert(exact, None);         (* base and top came from ct originally so will be exact *)
-      assert(representable, None); (* similarly offset should be representable XXX except for fastRepCheck *)
+      assert(exact, "");         (* base and top came from ct originally so will be exact *)
+      assert(representable, ""); (* similarly offset should be representable XXX except for fastRepCheck *)
       writeCapReg(cd, cd3);
     }
   (* END_CBuildCap *)
@@ -609,11 +610,11 @@ function clause execute (CCopyType(cd, cb, ct)) =
       raise_c2_exception(CapEx_LengthViolation, cb)
     else
       let (success, cap) = setCapOffset(cb_val, (bit[64]) (ct_otype - cb_base)) in {
-        assert(success, None); (* offset is in bounds so must succeed *)
+        assert(success, ""); (* offset is in bounds so must succeed *)
         writeCapReg(cd, cap);
       }
   } else
-    writeCapReg(cd, int_to_cap(-1))
+    writeCapReg(cd, int_to_cap(bitone ^^ 64))
   (* END_CCopyType *)
 }
 
@@ -624,7 +625,7 @@ function clause execute (CCheckPerm(cs, rt)) =
   (* START_CCheckPerm *)
   checkCP2usable();
   cs_val := readCapReg(cs);
-  cs_perms := EXTZ(getCapPerms(cs_val));
+  cs_perms := (bit[64]) (EXTZ(getCapPerms(cs_val)));
   rt_perms := rGPR(rt);
   if (register_inaccessible(cs)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cs)
@@ -725,7 +726,7 @@ function clause execute (CCSeal(cd, cs, ct)) =
     raise_c2_exception(CapEx_AccessSystemRegsViolation, ct)
   else if not (cs_val.tag) then
     raise_c2_exception(CapEx_TagViolation, cs)
-  else if (not (ct_val.tag)) | (getCapCursor(ct_val) == -1) then
+  else if (not (ct_val.tag)) | (getCapCursor(ct_val) == unsigned(bitone ^^ 64)) then
     writeCapReg(cd, cs_val)
   else if (cs_val.sealed) then
     raise_c2_exception(CapEx_SealViolation, cs)
@@ -939,7 +940,7 @@ function clause execute(CJALR(cd, cb, link)) =
         if (success) then
             writeCapReg(cd, linkCap)
         else
-            assert(false, None);
+            assert(false, "");
       delayedPC :=  (bit[64]) (getCapOffset(cb_val));
       delayedPCC := capStructToCapReg(cb_val);
       branchPending := 1;
@@ -982,7 +983,7 @@ function clause execute (CLoad(rd, cb, rt, offset, signext, width, linked)) =
       size   := wordWidthBytes(width);
       cursor := getCapCursor(cb_val);
       vAddr  := cursor + unsigned(rGPR(rt)) + (size*signed(offset));
-      vAddr64:= (bit[64]) vAddr;
+      vAddr64:= (bit[64]) (to_svec(vAddr));
       if ((vAddr + size) > getCapTop(cb_val)) then
         raise_c2_exception(CapEx_LengthViolation, cb)
       else if (vAddr < getCapBase(cb_val)) then
@@ -993,18 +994,23 @@ function clause execute (CLoad(rd, cb, rt, offset, signext, width, linked)) =
         {
           pAddr      := (TLBTranslate(vAddr64, LoadData));
           widthBytes := wordWidthBytes(width);
-          memResult  := if (linked) then
+          (bit[64]) memResult := if (linked) then
               {
                 CP0LLBit  := 0b1;
                 CP0LLAddr := pAddr;
-                MEMr_reserve_wrapper(pAddr, widthBytes);
+                if widthBytes == 1 then extendLoad(MEMr_reserve_wrapper(pAddr, 1), signext)
+                else if widthBytes == 2 then extendLoad(MEMr_reserve_wrapper(pAddr, 2), signext)
+                else if widthBytes == 4 then extendLoad(MEMr_reserve_wrapper(pAddr, 4), signext)
+                else extendLoad(MEMr_reserve_wrapper(pAddr, 8), signext)
               }
             else
-              MEMr_wrapper(pAddr, widthBytes);
-          if (signext) then
-            wGPR(rd) := EXTS(memResult)
-          else
-            wGPR(rd) := EXTZ(memResult)
+              {
+                if widthBytes == 1 then extendLoad(MEMr_wrapper(pAddr, 1), signext)
+                else if widthBytes == 2 then extendLoad(MEMr_wrapper(pAddr, 2), signext)
+                else if widthBytes == 4 then extendLoad(MEMr_wrapper(pAddr, 4), signext)
+                else extendLoad(MEMr_wrapper(pAddr, 8), signext)
+              };
+          wGPR(rd) := memResult;
         }
     }
   (* END_CLoad *)
@@ -1039,7 +1045,7 @@ function clause execute (CStore(rs, cb, rt, rd, offset, width, conditional)) =
       size   := wordWidthBytes(width);
       cursor := getCapCursor(cb_val);
       vAddr  := cursor + unsigned(rGPR(rt)) + (size * signed(offset));
-      vAddr64:= (bit[64]) vAddr;
+      vAddr64:= (bit[64]) (to_svec(vAddr));
       if ((vAddr + size) > getCapTop(cb_val)) then
         raise_c2_exception(CapEx_LengthViolation, cb)
       else if (vAddr < getCapBase(cb_val)) then
@@ -1052,7 +1058,7 @@ function clause execute (CStore(rs, cb, rt, rd, offset, width, conditional)) =
           rs_val := rGPR(rs);
           if (conditional) then
             {
-              success := if (CP0LLBit[0]) then
+              (bool) success := if (CP0LLBit[0]) then
                   switch(width)
                     {
                       case B -> MEMw_conditional_wrapper(pAddr, 1, rs_val[7..0])
@@ -1102,7 +1108,7 @@ function clause execute (CSC(cs, cb, rt, rd, offset, conditional)) =
     {
       cursor := getCapCursor(cb_val);
       vAddr  := cursor + unsigned(rGPR(rt)) + (((int) 16) * signed(offset));
-      vAddr64:= (bit[64]) vAddr;
+      vAddr64:= (bit[64]) (to_svec(vAddr));
       if ((vAddr + cap_size) > getCapTop(cb_val)) then
         raise_c2_exception(CapEx_LengthViolation, cb)
       else if (vAddr < getCapBase(cb_val)) then
@@ -1149,7 +1155,7 @@ function clause execute (CLC(cd, cb, rt, offset, linked)) =
     {
       cursor := getCapCursor(cb_val);
       vAddr  := cursor + unsigned(rGPR(rt)) + (((int) 16) * signed(offset));
-      vAddr64:= (bit[64]) vAddr;
+      vAddr64:= (bit[64]) (to_svec(vAddr));
       if ((vAddr + cap_size) > getCapTop(cb_val)) then
         raise_c2_exception(CapEx_LengthViolation, cb)
       else if (vAddr < getCapBase(cb_val)) then
@@ -1159,17 +1165,18 @@ function clause execute (CLC(cd, cb, rt, offset, linked)) =
       else
         {
           let (pAddr, suppressTag) = (TLBTranslateC(vAddr64, LoadData)) in
-          let (tag, mem) = (if (linked) 
-            then
-              {
-                CP0LLBit  := 0b1;
-                CP0LLAddr := pAddr;
-                MEMr_tagged_reserve(pAddr);
-              }
-            else 
-              (MEMr_tagged(pAddr)))
-          in
-          (CapRegs[cd]) := memBitsToCapBits(tag & (cb_val.permit_load_cap) & not (suppressTag), mem);
+          if (linked) then
+            {
+              CP0LLBit  := 0b1;
+              CP0LLAddr := pAddr;
+              let (tag, mem) = MEMr_tagged_reserve(pAddr) in
+              (CapRegs[cd]) := memBitsToCapBits(tag & (cb_val.permit_load_cap) & (not (suppressTag)), mem);
+            }
+          else
+            {
+              let (tag, mem) = MEMr_tagged(pAddr) in
+              (CapRegs[cd]) := memBitsToCapBits(tag & (cb_val.permit_load_cap) & (not (suppressTag)), mem);
+            }
         }
     }
   (* END_CLC *)
diff --git a/cheri/cheri_prelude_128.sail b/cheri/cheri_prelude_128.sail
index 98b0a40c..f1f33a56 100644
--- a/cheri/cheri_prelude_128.sail
+++ b/cheri/cheri_prelude_128.sail
@@ -35,6 +35,14 @@
 (* 128 bit cap + tag *)
 typedef CapReg = bit[129]
 
+val cast bool -> bit effect pure cast_bool_bit
+val cast forall 'n, 'm. vector<'n,'m,dec,bool> -> vector<'n,'m,dec,bit> effect pure cast_boolvec_bitvec
+val cast forall 'm. [|0:2**'m - 1|] -> vector<'m - 1,'m,dec,bit> effect pure cast_range_bitvec
+function vector<'m - 1,'m,dec,bit> cast_range_bitvec (v) = to_vec (v)
+val extern bool -> bool effect pure not
+
+typedef uint64 = range<0, (2** 64) - 1>
+
 typedef CapStruct = const struct {
   bool    tag;
   bit[4]  uperms;
@@ -85,9 +93,9 @@ def Nat cap_size_t  = 16 (* cap size in bytes *)
 let ([:cap_size_t:]) cap_size = 16
 
 function CapStruct capRegToCapStruct((CapReg) c) =
-  let (bool)    s = c[104] in
-  let (bit[20]) B = if s then c[103..96] : 0x000 else c[103..84] in
-  let (bit[20]) T = if s then c[83..76] : 0x000 else c[83..64] in
+  let (bool)    s  = c[104] in
+  let (bit[20]) Bc = if s then c[103..96] : 0x000 else c[103..84] in
+  let (bit[20]) Tc = if s then c[83..76] : 0x000 else c[83..64] in
   let (bit[24]) otype = if s then c[95..84] : c[75..64] else 0 in
   {
     tag                    = c[128];
@@ -106,8 +114,8 @@ function CapStruct capRegToCapStruct((CapReg) c) =
     reserved               = c[112..111];
     E                      = c[110..105] ^ 0b110000;
     sealed                 = s;
-    B                      = B;
-    T                      = T;
+    B                      = Bc;
+    T                      = Tc;
     otype                  = otype;
     address                = c[63..0];
   }
@@ -175,30 +183,30 @@ function (bool, CapStruct) sealCap((CapStruct) cap, (bit[24]) otype) =
         (false, cap (* was undefined but ocaml shallow embedding can't handle it *) )
 
 function [|-1:1|] a_top_correction((bit[20]) a_mid, (bit[20]) R, (bit[20]) bound) =
-    switch (a_mid <_u R, bound <_u R) {
-      case (bitzero, bitzero) -> 0
-      case (bitzero, bitone)  -> 1
-      case (bitone, bitzero)  -> -1
-      case (bitone, bitone)   -> 0
+    switch (a_mid < R, bound < R) {
+      case (false, false) -> 0
+      case (false, true)  -> 1
+      case (true, false)  -> -1
+      case (true, true)   -> 0
     }
 
 function uint64 getCapBase((CapStruct) c)  = 
     let ([|45|])  E = min(unsigned(c.E), 45) in
-    let (bit[20]) B = c.B in
+    let (bit[20]) Bc = c.B in
     let (bit[65]) a = EXTZ(c.address) in
-    let (bit[20]) R = B - 0x01000 in (* wraps *)
+    let (bit[20]) R = Bc - 0x01000 in (* wraps *)
     let (bit[20]) a_mid = a[(E + 19)..E] in
-    let correction = a_top_correction(a_mid, R, B) in
+    let correction = a_top_correction(a_mid, R, Bc) in
     let a_top = a >> (E+20) in
-    let (bit[64]) base = EXTZ((a_top + correction) : B) << E in
+    let (bit[64]) base = EXTZ((a_top + correction) : Bc) << E in
     unsigned(base)
 
 function CapLen getCapTop ((CapStruct) c)  = 
     let ([|45|])  E = min(unsigned(c.E), 45) in
-    let (bit[20]) B = c.B in
+    let (bit[20]) Bc = c.B in
     let (bit[20]) T = c.T in
     let (bit[65]) a = EXTZ(c.address)  in
-    let (bit[20]) R = B - 0x01000 in (* wraps *)
+    let (bit[20]) R = Bc - 0x01000 in (* wraps *)
     let (bit[20]) a_mid = a[(E + 19)..E] in
     let correction = a_top_correction(a_mid, R, T) in
     let a_top = a >> (E+20) in
@@ -283,10 +291,10 @@ function [|48|] computeE ((bit[65]) rlength) =
 function (bool, CapStruct) setCapBounds((CapStruct) cap, (bit[64]) base, (bit[65]) top) =
     (* {cap with base=base; length=(bit[64]) length; offset=0} *)
     let ([|48|])  e = computeE(top - (0b0 : base)) in
-    let (bit[20]) B = base[(19+e)..e] in
-    let (bit[20]) T = top[(19+e)..e] in
+    let (bit[20]) Bc = base[19+e..e] in
+    let (bit[20]) T = top[19+e..e] in
     let (bit[20]) T2 = T + if (top[(e - 1)..0] == 0) then 0 else 1 in
-    let newCap  = {cap with E=(bit[6]) e; B=B; T=T2} in
+    let newCap  = {cap with E=(bit[6]) e; B=Bc; T=T2} in
     let newBase = getCapBase(newCap) in
     let newTop  = getCapTop(newCap) in
     let exact   = (base == newBase) & (top == newTop) in
diff --git a/cheri/cheri_prelude_256.sail b/cheri/cheri_prelude_256.sail
index ee9a91ac..7cf3d69c 100644
--- a/cheri/cheri_prelude_256.sail
+++ b/cheri/cheri_prelude_256.sail
@@ -36,7 +36,10 @@
 typedef CapReg = bit[257]
 
 val cast bool -> bit effect pure cast_bool_bit
-val cast forall 'n, 'm. vector<'n,'m,dec,bool> -> vector<'n,'m,dec,bit> effect pure cast_bool_vec
+val cast forall 'n, 'm. vector<'n,'m,dec,bool> -> vector<'n,'m,dec,bit> effect pure cast_boolvec_bitvec
+val cast forall 'm. [|0:2**'m - 1|] -> vector<'m - 1,'m,dec,bit> effect pure cast_range_bitvec
+function vector<'m - 1,'m,dec,bit> cast_range_bitvec (v) = to_vec (v)
+val extern bool -> bool effect pure not
 
 typedef uint64 = range<0, (2** 64) - 1>
 
@@ -188,13 +191,13 @@ function CapStruct setCapPerms((CapStruct) cap, (bit[31]) perms) =
 function (bool, CapStruct) sealCap((CapStruct) cap, (bit[24]) otype) =
     (true, {cap with sealed=true; otype=otype})
 
-function uint64 getCapBase((CapStruct) c)   = unsigned(c.base)
-function CapLen getCapTop((CapStruct) c)    = unsigned(c.base) + unsigned(c.length)
-function uint64 getCapOffset((CapStruct) c) = unsigned(c.offset)
-function CapLen getCapLength((CapStruct) c) = unsigned(c.length)
+function bit[64] getCapBase((CapStruct) c)        = c.base
+function [|0:2**65 - 2|] getCapTop((CapStruct) c) = unsigned(c.base) + unsigned(c.length)
+function bit[64] getCapOffset((CapStruct) c)      = c.offset
+function CapLen  getCapLength((CapStruct) c)      = unsigned(c.length)
 
 function uint64 getCapCursor((CapStruct) cap) = 
-  (unsigned(cap.base) + unsigned(cap.offset)) mod (2 ** 64)
+  (unsigned(cap.base) + unsigned(cap.offset)) mod (pow2(64))
 
 function (bool, CapStruct) setCapOffset((CapStruct) c, (bit[64]) offset) = 
     (true, {c with offset=offset})
diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail
index dcb56d01..f5fcd095 100644
--- a/cheri/cheri_prelude_common.sail
+++ b/cheri/cheri_prelude_common.sail
@@ -32,6 +32,16 @@
 (*  SUCH DAMAGE.                                                          *)
 (*========================================================================*)
 
+
+scattered typedef ast = const union
+
+val ast -> unit effect {barr, eamem, escape, rmem, rmemt, rreg, undef, wmvt, wreg} execute
+scattered function unit execute
+
+val bit[32] -> option<ast> effect pure decode
+scattered function option<ast> decode
+
+
 register CapReg PCC
 register CapReg nextPCC
 register CapReg delayedPCC
@@ -74,7 +84,7 @@ let (vector <0, 32, inc, (register<CapReg>)>) CapRegs =
   C21, C22, C23, C24, C25, C26, C27, C28, C29, C30, C31
   ]
 
-let (nat) max_otype = 0xffffff
+let max_otype = MAX(24) (*0xffffff*)
 let have_cp2 = true
 
 function (CapStruct) readCapReg((regno) n) =
@@ -204,7 +214,7 @@ function bool pcc_access_system_regs () =
       (pcc.access_system_regs)
 
 function bool register_inaccessible((regno) r) = 
-  let is_sys_reg = switch(r) {
+  let (bool) is_sys_reg = switch(r) {
     case 0b11011 -> true
     case 0b11100 -> true
     case 0b11101 -> true
@@ -249,7 +259,8 @@ function bool MEMw_tagged_conditional((bit[64]) addr, (bool) tag, (bit[cap_size_
   MEMval_tag_conditional(addr, cap_size, tag, reverse_endianness(data));
 }
 
-function unit effect {wmem} MEMw_wrapper(addr, size, data) =
+val forall Nat 'n, 'n >= 1. (bit[64], [:'n:], bit[8 * 'n]) -> unit effect {wmvt, wreg, eamem} MEMw_wrapper
+function unit effect {wmvt, wreg, eamem} MEMw_wrapper(addr, size, data) =
   let ledata = reverse_endianness(data) in
   if (addr == 0x000000007f000000) then
   {
@@ -263,7 +274,8 @@ function unit effect {wmem} MEMw_wrapper(addr, size, data) =
     MEMval_tag(addr, size, false, ledata);
   }
 
-function bool effect {wmem} MEMw_conditional_wrapper(addr, size, data) =
+val forall Nat 'n, 'n >= 1. (bit[64], [:'n:], bit[8 * 'n]) -> bool effect {wmvt, eamem} MEMw_conditional_wrapper
+function bool effect {wmvt, eamem} MEMw_conditional_wrapper(addr, size, data) =
   {
     (* On cheri non-capability writes must clear the corresponding tag*)
     MEMea_conditional(addr, size);
@@ -293,7 +305,7 @@ function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordTy
     else if (vAddr < (base)) then
       (raise_c2_exception(CapEx_LengthViolation, capno))
     else
-      (bit[64]) vAddr; (* XXX vAddr not truncated because top <= 2^64 and size > 0 *)
+      (bit[64]) (to_vec(vAddr)); (* XXX vAddr not truncated because top <= 2^64 and size > 0 *)
   }
 
 function (bit[64]) TranslatePC ((bit[64]) vAddr) = {
@@ -311,7 +323,7 @@ function (bit[64]) TranslatePC ((bit[64]) vAddr) = {
 }
 
 function unit checkCP2usable () =
-  if not ((CP0Status.CU)[2]) then
+  if not ((norm_dec (CP0Status.CU))[2]) then
     {
       (CP0Cause.CE) := 0b10;
       (SignalException(CpU));
diff --git a/lib/prelude.sail b/lib/prelude.sail
index fe5d7d5b..b211def1 100644
--- a/lib/prelude.sail
+++ b/lib/prelude.sail
@@ -129,6 +129,9 @@ val forall Num 'n, Num 'o, Order 'ord.
     (vector<'o, 'n, 'ord, bit>, int) -> vector<'o, 'n, 'ord, bit> effect pure add_vec_int
 
 val forall Num 'n, Num 'o, Order 'ord.
+    (int, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure add_int_vec
+
+val forall Num 'n, Num 'o, Order 'ord.
     (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> (vector<'o, 'n, 'ord, bit>, bit, bit) effect pure add_overflow_vec
 
 val extern forall Num 'n, Num 'm, Num 'o, Num 'p.
@@ -149,6 +152,7 @@ overload (deinfix +) [
   add_vec;
   add_overflow_vec;
   add_vec_int;
+  add_int_vec;
   add_range;
   add_nat;
   add_int
@@ -264,9 +268,9 @@ val extern forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> bool effect pure lt_atom_a
 val extern forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> bool effect pure gt_atom_atom = "gt"
 
 overload (deinfix >=) [gteq_atom_atom; gteq_range_atom; gteq_atom_range; gteq_vec; gteq_int]
-overload (deinfix >) [gt_atom_atom; gt_vec; gt_int]
+overload (deinfix >) [gt_atom_atom; gt_range_atom; gt_vec; gt_int]
 overload (deinfix <=) [lteq_atom_atom; lteq_range_atom; lteq_atom_range; lteq_vec; lteq_int]
-overload (deinfix <) [lt_atom_atom; lt_vec; lt_int]
+overload (deinfix <) [lt_atom_atom; lt_range_atom; lt_vec; lt_int]
 
 val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure gteq_svec
 val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure gt_svec
@@ -278,13 +282,21 @@ overload (deinfix <=_s) [lteq_svec]
 overload (deinfix >_s) [gt_svec]
 overload (deinfix >=_s) [gteq_svec]
 
+val extern forall Num 'n, Num 'm, Num 'o, 'o >= 'n. ([|'n:'m|], [:'o:]) -> [|'n:'o|] effect pure min_range_atom = "min"
+val extern (int, int) -> int effect pure min_int = "min"
+
+overload min [min_range_atom; min_int]
+
 val (int, int) -> int effect pure quotient
 
 overload (deinfix quot) [quotient]
 
 val (int, int) -> int effect pure modulo
+val extern forall Num 'm. (int, [:'m:]) -> [|0:'m - 1|] effect pure modulo_atom = "modulo"
+
+overload (deinfix mod) [modulo_atom; modulo]
 
-overload (deinfix mod) [modulo]
+val extern forall Num 'n. [:'n:] -> [:2** 'n:] effect pure pow2
 
 val extern forall Num 'n, Num 'm, Order 'ord, Type 'a. vector<'n,'m,'ord,'a> -> [:'m:] effect pure vector_length = "length"
 val forall Type 'a. list<'a> -> nat effect pure list_length
diff --git a/mips_new_tc/mips_ast_decl.sail b/mips_new_tc/mips_ast_decl.sail
new file mode 100644
index 00000000..68e0558b
--- /dev/null
+++ b/mips_new_tc/mips_ast_decl.sail
@@ -0,0 +1,44 @@
+(*========================================================================*)
+(*                                                                        *)
+(*  Copyright (c) 2015-2017 Robert M. Norton                              *)
+(*  Copyright (c) 2015-2017 Kathyrn Gray                                  *)
+(*  All rights reserved.                                                  *)
+(*                                                                        *)
+(*  This software was developed by the University of Cambridge Computer   *)
+(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
+(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*     notice, this list of conditions and the following disclaimer.      *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*     notice, this list of conditions and the following disclaimer in    *)
+(*     the documentation and/or other materials provided with the         *)
+(*     distribution.                                                      *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
+(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
+(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
+(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
+(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
+(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
+(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
+(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
+(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
+(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
+(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
+(*  SUCH DAMAGE.                                                          *)
+(*========================================================================*)
+
+(* misp_insts.sail: mips instruction decode and execute clauses and AST node
+   declarations *)
+
+scattered typedef ast = const union
+
+val ast -> unit effect {barr, eamem, escape, rmem, rreg, undef, wmv, wreg} execute
+scattered function unit execute
+
+val bit[32] -> option<ast> effect pure decode
+scattered function option<ast> decode
diff --git a/mips_new_tc/mips_extras_embed_sequential.lem b/mips_new_tc/mips_extras_embed_sequential.lem
index f9c6c92c..4f690e5b 100644
--- a/mips_new_tc/mips_extras_embed_sequential.lem
+++ b/mips_new_tc/mips_extras_embed_sequential.lem
@@ -2,25 +2,26 @@ open import Pervasives
 open import Pervasives_extra
 open import Sail_impl_base
 open import Sail_values
+open import Sail_operators_mwords
 open import State
 
-val MEMr             : forall 'regs 'a 'b. Size 'b => (bitvector 'a * integer) -> M 'regs (bitvector 'b)
-val MEMr_reserve     : forall 'regs 'a 'b. Size 'b => (bitvector 'a * integer) -> M 'regs (bitvector 'b)
-val MEMr_tag         : forall 'regs 'a 'b. Size 'b => (bitvector 'a * integer) -> M 'regs (bitU * bitvector 'b)
-val MEMr_tag_reserve : forall 'regs 'a 'b. Size 'b => (bitvector 'a * integer) -> M 'regs (bitU * bitvector 'b)
+val MEMr             : forall 'regs 'a 'b. Size 'a, Size 'b => (bitvector 'a * integer) -> M 'regs (bitvector 'b)
+val MEMr_reserve     : forall 'regs 'a 'b. Size 'a, Size 'b => (bitvector 'a * integer) -> M 'regs (bitvector 'b)
+val MEMr_tag         : forall 'regs 'a 'b. Size 'a, Size 'b => (bitvector 'a * integer) -> M 'regs (bool * bitvector 'b)
+val MEMr_tag_reserve : forall 'regs 'a 'b. Size 'a, Size 'b => (bitvector 'a * integer) -> M 'regs (bool * bitvector 'b)
 
-let MEMr (addr,size)             = read_mem false Read_plain addr size
-let MEMr_reserve (addr,size)     = read_mem false Read_reserve addr size
+let MEMr (addr,size)             = read_mem false Read_plain (unsigned addr) size >>= fun v -> return (vec_to_bvec v)
+let MEMr_reserve (addr,size)     = read_mem false Read_reserve (unsigned addr) size >>= fun v -> return (vec_to_bvec v)
 
 let MEMr_tag (addr,size) =
-  read_mem false Read_plain addr size >>= fun v ->
-  read_tag false Read_plain addr >>= fun t ->
-  return (t, v)
+  read_mem false Read_plain (unsigned addr) size >>= fun v ->
+  read_tag false Read_plain (unsigned addr) >>= fun t ->
+  return (bitU_to_bool t, vec_to_bvec v)
 
 let MEMr_tag_reserve (addr,size) =
-  read_mem false Read_plain addr size >>= fun v ->
-  read_tag false Read_plain addr >>= fun t ->
-  return (t, v)
+  read_mem false Read_plain (unsigned addr) size >>= fun v ->
+  read_tag false Read_plain (unsigned addr) >>= fun t ->
+  return (bitU_to_bool t, vec_to_bvec v)
 
 
 val MEMea                 : forall 'regs 'a. (bitvector 'a * integer) -> M 'regs unit
@@ -28,22 +29,22 @@ val MEMea_conditional     : forall 'regs 'a. (bitvector 'a * integer) -> M 'regs
 val MEMea_tag             : forall 'regs 'a. (bitvector 'a * integer) -> M 'regs unit
 val MEMea_tag_conditional : forall 'regs 'a. (bitvector 'a * integer) -> M 'regs unit
 
-let MEMea (addr,size)                 = write_mem_ea Write_plain addr size
-let MEMea_conditional (addr,size)     = write_mem_ea Write_conditional addr size
+let MEMea (addr,size)                 = write_mem_ea Write_plain (unsigned addr) size
+let MEMea_conditional (addr,size)     = write_mem_ea Write_conditional (unsigned addr) size
 
-let MEMea_tag (addr,size)             = write_mem_ea Write_plain addr size
-let MEMea_tag_conditional (addr,size) = write_mem_ea Write_conditional addr size
+let MEMea_tag (addr,size)             = write_mem_ea Write_plain (unsigned addr) size
+let MEMea_tag_conditional (addr,size) = write_mem_ea Write_conditional (unsigned addr) size
 
 
 val MEMval                 : forall 'regs 'a 'b. (bitvector 'a * integer * bitvector 'b) -> M 'regs unit
 val MEMval_conditional     : forall 'regs 'a 'b. (bitvector 'a * integer * bitvector 'b) -> M 'regs bool
-val MEMval_tag             : forall 'regs 'a 'b. (bitvector 'a * integer * bitU * bitvector 'b) -> M 'regs unit
-val MEMval_tag_conditional : forall 'regs 'a 'b. (bitvector 'a * integer * bitU * bitvector 'b) -> M 'regs bool
+val MEMval_tag             : forall 'regs 'a 'b. (bitvector 'a * integer * bool * bitvector 'b) -> M 'regs unit
+val MEMval_tag_conditional : forall 'regs 'a 'b. (bitvector 'a * integer * bool * bitvector 'b) -> M 'regs bool
 
-let MEMval (_,_,v)                   = write_mem_val v >>= fun _ -> return ()
-let MEMval_conditional (_,_,v)       = write_mem_val v >>= fun b -> return (if b then true else false)
-let MEMval_tag (_,_,t,v)             = write_mem_val v >>= fun _ -> write_tag t >>= fun _ -> return ()
-let MEMval_tag_conditional (_,_,t,v) = write_mem_val v >>= fun b -> write_tag t >>= fun _ -> return (if b then true else false)
+let MEMval (_,_,v)                   = write_mem_val (bvec_to_vec v) >>= fun _ -> return ()
+let MEMval_conditional (_,_,v)       = write_mem_val (bvec_to_vec v) >>= fun b -> return (if b then true else false)
+let MEMval_tag (_,_,t,v)             = write_mem_val (bvec_to_vec v) >>= fun _ -> write_tag (bool_to_bitU t) >>= fun _ -> return ()
+let MEMval_tag_conditional (_,_,t,v) = write_mem_val (bvec_to_vec v) >>= fun b -> write_tag (bool_to_bitU t) >>= fun _ -> return (if b then true else false)
 
 val MEM_sync  : forall 'regs. unit -> M 'regs unit
 
diff --git a/mips_new_tc/mips_insts.sail b/mips_new_tc/mips_insts.sail
index 96826dae..51ef65a6 100644
--- a/mips_new_tc/mips_insts.sail
+++ b/mips_new_tc/mips_insts.sail
@@ -35,14 +35,6 @@
 (* misp_insts.sail: mips instruction decode and execute clauses and AST node
    declarations *)
 
-scattered typedef ast = const union
-
-val ast -> unit effect {barr, eamem, escape, rmem, rreg, undef, wmv, wreg} execute
-scattered function unit execute
-
-val bit[32] -> option<ast> effect pure decode
-scattered function option<ast> decode
-
 (**************************************************************************************)
 (* [D]ADD[I][U] various forms of ADD                                                  *)
 (**************************************************************************************)
diff --git a/mips_new_tc/mips_prelude.sail b/mips_new_tc/mips_prelude.sail
index 6792f546..128c63d8 100644
--- a/mips_new_tc/mips_prelude.sail
+++ b/mips_new_tc/mips_prelude.sail
@@ -89,9 +89,12 @@ let ([:64:]) TLBNumEntries = 64
 typedef TLBIndexT = (bit[6])
 let (TLBIndexT) TLBIndexMax = 0b111111
 
-let MAX_U64 = unsigned(0xffffffffffffffff)
-let MAX_VA  = unsigned(0xffffffffff)
-let MAX_PA  = unsigned(0xfffffffff)
+val forall 'n. [:'n:] -> [:2**'n - 1:] effect pure MAX
+function MAX(n) = pow2(n) - 1
+
+let MAX_U64 = MAX(64) (*unsigned(0xffffffffffffffff)*)
+let MAX_VA  = MAX(40) (*unsigned(0xffffffffff)*)
+let MAX_PA  = MAX(36) (*unsigned(0xfffffffff)*)
 
 typedef TLBEntry = register bits [116 : 0] {
   116 ..  101: pagemask;
diff --git a/src/Makefile b/src/Makefile
index 53acec6a..6cfcf874 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -78,11 +78,11 @@ ZARITH_LIB=$(ZARITH_DIR)/zarith.cmxa
 SAIL_LIB_DIR:=$(SAIL_DIR)/lib
 MIPS_SAIL_DIR:=$(SAIL_DIR)/mips_new_tc
 
-MIPS_SAILS_PRE:=$(SAIL_LIB_DIR)/prelude.sail $(SAIL_LIB_DIR)/prelude_wrappers.sail $(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
+MIPS_SAILS_PRE:=$(SAIL_LIB_DIR)/prelude.sail $(SAIL_LIB_DIR)/prelude_wrappers.sail $(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(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_SAILS:=$(MIPS_SAILS_PRE) $(SAIL_DIR)/etc/regfp.sail $(MIPS_SAIL_DIR)/mips_regfp.sail
 
-MIPS_NOTLB_SAILS_PRE:=$(SAIL_LIB_DIR)/prelude.sail $(SAIL_LIB_DIR)/prelude_wrappers.sail $(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb_stub.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
+MIPS_NOTLB_SAILS_PRE:=$(SAIL_LIB_DIR)/prelude.sail $(SAIL_LIB_DIR)/prelude_wrappers.sail $(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb_stub.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_ast_decl.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
 
 MIPS_NOTLB_SAILS:=$(MIPS_NOTLB_SAILS_PRE) $(SAIL_DIR)/etc/regfp.sail $(MIPS_SAIL_DIR)/mips_regfp.sail
 
@@ -170,14 +170,14 @@ _build/cheri_notlb.lem: $(CHERI_NOTLB_SAILS) ./sail.native
 	cd _build ;\
 	../sail.native -lem_ast -o cheri_notlb $(CHERI_NOTLB_SAILS)
 
-_build/cheri_embed_types.lem: $(CHERI_SAILS) ./sail.native
+_build/cheri_embed_types_sequential.lem: $(CHERI_SAILS) ./sail.native
 	mkdir -p _build
 	cd _build ;\
-	../sail.native -lem_lib "Mips_extras_embed" -lem -o cheri $(CHERI_SAILS)
+	../sail.native -lem_lib "Mips_extras_embed" -lem -lem_sequential -lem_mwords -o cheri $(CHERI_SAILS)
 
-_build/Cheri_embed_sequential.thy: _build/cheri_embed_types.lem
+_build/Cheri_embed_sequential.thy: _build/cheri_embed_types_sequential.lem
 	cd _build ;\
-	lem -isa -outdir . ../lem_interp/sail_impl_base.lem ../gen_lib/state.lem ../../mips/mips_extras_embed_sequential.lem cheri_embed_types.lem cheri_embed_sequential.lem
+	lem -isa -outdir . ../lem_interp/sail_impl_base.lem ../gen_lib/state.lem $(MIPS_SAIL_DIR)/mips_extras_embed_sequential.lem cheri_embed_types_sequential.lem cheri_embed_sequential.lem
 
 _build/mips_all.sail: $(MIPS_SAILS)
 	cat $(MIPS_SAILS) > $@
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 7d8797f9..aef1a05d 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -51,6 +51,8 @@ let no_annot = (Parse_ast.Unknown, ())
 let inc_ord = Ord_aux (Ord_inc, Parse_ast.Unknown)
 let dec_ord = Ord_aux (Ord_dec, Parse_ast.Unknown)
 
+let mk_id str = Id_aux (Id str, Parse_ast.Unknown)
+
 let mk_nc nc_aux = NC_aux (nc_aux, Parse_ast.Unknown)
 
 let mk_nexp nexp_aux = Nexp_aux (nexp_aux, Parse_ast.Unknown)
@@ -60,6 +62,8 @@ let unaux_exp (E_aux (exp_aux, _)) = exp_aux
 
 let mk_pat pat_aux = P_aux (pat_aux, no_annot)
 
+let mk_lexp lexp_aux = LEXP_aux (lexp_aux, no_annot)
+
 let mk_lit lit_aux = L_aux (lit_aux, Parse_ast.Unknown)
 
 let mk_lit_exp lit_aux = mk_exp (E_lit (mk_lit lit_aux))
@@ -73,9 +77,127 @@ let mk_fundef funcls =
   DEF_fundef
    (FD_aux (FD_function (rec_opt, tannot_opt, effect_opt, funcls), no_annot))
 
+let mk_letbind pat exp = LB_aux (LB_val_implicit (pat, exp), no_annot)
+
 let mk_val_spec vs_aux =
   DEF_spec (VS_aux (vs_aux, no_annot))
 
+let kopt_kid (KOpt_aux (kopt_aux, _)) =
+  match kopt_aux with
+  | KOpt_none kid | KOpt_kind (_, kid) -> kid
+
+let is_nat_kopt = function
+  | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_nat, _)], _), _), _) -> true
+  | KOpt_aux (KOpt_none _, _) -> true
+  | _ -> false
+
+let is_order_kopt = function
+  | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_order, _)], _), _), _) -> true
+  | _ -> false
+
+let is_typ_kopt = function
+  | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_type, _)], _), _), _) -> true
+  | _ -> false
+
+let rec nexp_simp (Nexp_aux (nexp, l)) = Nexp_aux (nexp_simp_aux nexp, l)
+and nexp_simp_aux = function
+  | Nexp_minus (Nexp_aux (Nexp_sum (Nexp_aux (n1, _), Nexp_aux (Nexp_constant c1, _)), _), Nexp_aux (Nexp_constant c2, _)) when c1 = c2 ->
+     nexp_simp_aux n1
+  | Nexp_sum (Nexp_aux (Nexp_minus (Nexp_aux (n1, _), Nexp_aux (Nexp_constant c1, _)), _), Nexp_aux (Nexp_constant c2, _)) when c1 = c2 ->
+     nexp_simp_aux n1
+  | Nexp_sum (n1, n2) ->
+     begin
+       let (Nexp_aux (n1_simp, _) as n1) = nexp_simp n1 in
+       let (Nexp_aux (n2_simp, _) as n2) = nexp_simp n2 in
+       match n1_simp, n2_simp with
+       | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (c1 + c2)
+       | _, Nexp_neg n2 -> Nexp_minus (n1, n2)
+       | _, _ -> Nexp_sum (n1, n2)
+     end
+  | Nexp_times (n1, n2) ->
+     begin
+       let (Nexp_aux (n1_simp, _) as n1) = nexp_simp n1 in
+       let (Nexp_aux (n2_simp, _) as n2) = nexp_simp n2 in
+       match n1_simp, n2_simp with
+       | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (c1 * c2)
+       | _, _ -> Nexp_times (n1, n2)
+     end
+  | Nexp_minus (n1, n2) ->
+     begin
+       let (Nexp_aux (n1_simp, _) as n1) = nexp_simp n1 in
+       let (Nexp_aux (n2_simp, _) as n2) = nexp_simp n2 in
+       match n1_simp, n2_simp with
+       | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (c1 - c2)
+       | _, _ -> Nexp_minus (n1, n2)
+     end
+  | nexp -> nexp
+
+let mk_typ typ = Typ_aux (typ, Parse_ast.Unknown)
+let mk_typ_arg arg = Typ_arg_aux (arg, Parse_ast.Unknown)
+let mk_kid str = Kid_aux (Var ("'" ^ str), Parse_ast.Unknown)
+let mk_infix_id str = Id_aux (DeIid str, Parse_ast.Unknown)
+
+let mk_id_typ id = Typ_aux (Typ_id id, Parse_ast.Unknown)
+
+let mk_ord ord_aux = Ord_aux (ord_aux, Parse_ast.Unknown)
+
+let int_typ = mk_id_typ (mk_id "int")
+let nat_typ = mk_id_typ (mk_id "nat")
+let unit_typ = mk_id_typ (mk_id "unit")
+let bit_typ = mk_id_typ (mk_id "bit")
+let real_typ = mk_id_typ (mk_id "real")
+let app_typ id args = mk_typ (Typ_app (id, args))
+let atom_typ nexp =
+  mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (Typ_arg_nexp (nexp_simp nexp))]))
+let range_typ nexp1 nexp2 =
+  mk_typ (Typ_app (mk_id "range", [mk_typ_arg (Typ_arg_nexp (nexp_simp nexp1));
+                                   mk_typ_arg (Typ_arg_nexp (nexp_simp nexp2))]))
+let bool_typ = mk_id_typ (mk_id "bool")
+let string_typ = mk_id_typ (mk_id "string")
+let list_typ typ = mk_typ (Typ_app (mk_id "list", [mk_typ_arg (Typ_arg_typ typ)]))
+
+let vector_typ n m ord typ =
+  mk_typ (Typ_app (mk_id "vector",
+                   [mk_typ_arg (Typ_arg_nexp (nexp_simp n));
+                    mk_typ_arg (Typ_arg_nexp (nexp_simp m));
+                    mk_typ_arg (Typ_arg_order ord);
+                    mk_typ_arg (Typ_arg_typ typ)]))
+
+let exc_typ = mk_id_typ (mk_id "exception")
+
+let nconstant c = Nexp_aux (Nexp_constant c, Parse_ast.Unknown)
+let nminus n1 n2 = Nexp_aux (Nexp_minus (n1, n2), Parse_ast.Unknown)
+let nsum n1 n2 = Nexp_aux (Nexp_sum (n1, n2), Parse_ast.Unknown)
+let ntimes n1 n2 = Nexp_aux (Nexp_times (n1, n2), Parse_ast.Unknown)
+let npow2 n = Nexp_aux (Nexp_exp n, Parse_ast.Unknown)
+let nvar kid = Nexp_aux (Nexp_var kid, Parse_ast.Unknown)
+let nid id = Nexp_aux (Nexp_id id, Parse_ast.Unknown)
+
+let nc_eq n1 n2 = mk_nc (NC_fixed (n1, n2))
+let nc_neq n1 n2 = mk_nc (NC_not_equal (n1, n2))
+let nc_lteq n1 n2 = NC_aux (NC_bounded_le (n1, n2), Parse_ast.Unknown)
+let nc_gteq n1 n2 = NC_aux (NC_bounded_ge (n1, n2), Parse_ast.Unknown)
+let nc_lt n1 n2 = nc_lteq n1 (nsum n2 (nconstant 1))
+let nc_gt n1 n2 = nc_gteq n1 (nsum n2 (nconstant 1))
+let nc_and nc1 nc2 = mk_nc (NC_and (nc1, nc2))
+let nc_or nc1 nc2 = mk_nc (NC_or (nc1, nc2))
+let nc_true = mk_nc NC_true
+let nc_false = mk_nc NC_false
+
+let mk_typschm typq typ = TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown)
+
+let mk_fexp id exp = FE_aux (FE_Fexp (id, exp), no_annot)
+let mk_fexps fexps = FES_aux (FES_Fexps (fexps, false), no_annot)
+
+let mk_effect effs =
+  Effect_aux (Effect_set (List.map (fun be_aux -> BE_aux (be_aux, Parse_ast.Unknown)) effs), Parse_ast.Unknown)
+
+let no_effect = mk_effect []
+
+let quant_items : typquant -> quant_item list = function
+  | TypQ_aux (TypQ_tq qis, _) -> qis
+  | TypQ_aux (TypQ_no_forall, _) -> []
+
 let rec map_exp_annot f (E_aux (exp, annot)) = E_aux (map_exp_annot_aux f exp, f annot)
 and map_exp_annot_aux f = function
   | E_block xs -> E_block (List.map (map_exp_annot f) xs)
@@ -270,6 +392,11 @@ and string_of_n_constraint = function
   | NC_aux (NC_true, _) -> "true"
   | NC_aux (NC_false, _) -> "false"
 
+let string_of_annot = function
+  | Some (_, typ, eff) ->
+     "Some (_, " ^ string_of_typ typ ^ ", " ^ string_of_effect eff ^ ")"
+  | None -> "None"
+
 let string_of_quant_item_aux = function
   | QI_id (KOpt_aux (KOpt_none kid, _)) -> string_of_kid kid
   | QI_id (KOpt_aux (KOpt_kind (k, kid), _)) -> string_of_kind k ^ " " ^ string_of_kid kid
@@ -321,6 +448,8 @@ let rec string_of_exp (E_aux (exp, _)) =
   | E_cast (typ, exp) -> "(" ^ string_of_typ typ ^ ") " ^ string_of_exp exp
   | E_vector vec -> "[" ^ string_of_list ", " string_of_exp vec ^ "]"
   | E_vector_access (v, n) -> string_of_exp v ^ "[" ^ string_of_exp n ^ "]"
+  | E_vector_update (v, n, exp) -> "[" ^ string_of_exp v ^ " with " ^ string_of_exp n ^ " = " ^ string_of_exp exp ^ "]"
+  | E_vector_update_subrange (v, n, m, exp) -> "[" ^ string_of_exp v ^ " with " ^ string_of_exp n ^ " .. " ^ string_of_exp m ^ " = " ^ string_of_exp exp ^ "]"
   | E_vector_subrange (v, n1, n2) -> string_of_exp v ^ "[" ^ string_of_exp n1 ^ " .. " ^ string_of_exp n2 ^ "]"
   | E_vector_append (v1, v2) -> string_of_exp v1 ^ " : " ^ string_of_exp v2
   | E_if (cond, then_branch, else_branch) ->
@@ -348,6 +477,8 @@ let rec string_of_exp (E_aux (exp, _)) =
   | E_comment _ -> "INTERNAL COMMENT"
   | E_comment_struc _ -> "INTERNAL COMMENT STRUC"
   | E_internal_let _ -> "INTERNAL LET"
+  | E_internal_return _ -> "INTERNAL RETURN"
+  | E_internal_plet _ -> "INTERNAL PLET"
   | _ -> "INTERNAL"
 and string_of_fexp (FE_aux (FE_Fexp (field, exp), _)) =
   string_of_id field ^ " = " ^ string_of_exp exp
@@ -471,11 +602,11 @@ let rec simplify_nexp (Nexp_aux (nexp, l)) =
   | Nexp_times (n1, n2) -> try_binop ( * ) n1 n2 (fun n1 n2 -> Nexp_times (n1, n2))
   | Nexp_sum (n1, n2) -> try_binop ( + ) n1 n2 (fun n1 n2 -> Nexp_sum (n1, n2))
   | Nexp_minus (n1, n2) -> try_binop ( - ) n1 n2 (fun n1 n2 -> Nexp_minus (n1, n2))
-  | Nexp_exp n ->
+  (* | Nexp_exp n ->
     (match simplify_nexp n with
       | Nexp_aux (Nexp_constant i, _) ->
         rewrap (Nexp_constant (power 2 i))
-      | n -> rewrap (Nexp_exp n))
+      | n -> rewrap (Nexp_exp n)) *)
   | Nexp_neg n ->
     (match simplify_nexp n with
       | Nexp_aux (Nexp_constant i, _) ->
@@ -503,13 +634,17 @@ let rec is_vector_typ = function
 let typ_app_args_of = function
   | Typ_aux (Typ_app (Id_aux (Id c,_), targs), l) ->
     (c, List.map (fun (Typ_arg_aux (a,_)) -> a) targs, l)
-  | Typ_aux (_, l) -> raise (Reporting_basic.err_typ l "typ_app_args_of called on non-app type")
+  | Typ_aux (_, l) as typ ->
+     raise (Reporting_basic.err_typ l
+       ("typ_app_args_of called on non-app type " ^ string_of_typ typ))
 
 let rec vector_typ_args_of typ = match typ_app_args_of typ with
   | ("vector", [Typ_arg_nexp start; Typ_arg_nexp len; Typ_arg_order ord; Typ_arg_typ etyp], _) ->
-    (start, len, ord, etyp)
+    (simplify_nexp start, simplify_nexp len, ord, etyp)
   | ("register", [Typ_arg_typ rtyp], _) -> vector_typ_args_of rtyp
-  | (_, _, l) -> raise (Reporting_basic.err_typ l "vector_typ_args_of called on non-vector type")
+  | (_, _, l) ->
+     raise (Reporting_basic.err_typ l
+       ("vector_typ_args_of called on non-vector type " ^ string_of_typ typ))
 
 let is_order_inc = function
   | Ord_aux (Ord_inc, _) -> true
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 7580404d..e6823ee9 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -44,21 +44,83 @@
 
 open Ast
 
+val mk_id : string -> id
+val mk_kid : string -> kid
+val mk_ord : order_aux -> order
 val mk_nc : n_constraint_aux -> n_constraint
 val mk_nexp : nexp_aux -> nexp
 val mk_exp : unit exp_aux -> unit exp
 val mk_pat : unit pat_aux -> unit pat
+val mk_lexp : unit lexp_aux -> unit lexp
 val mk_lit : lit_aux -> lit
 val mk_lit_exp : lit_aux -> unit exp
 val mk_funcl : id -> unit pat -> unit exp -> unit funcl
 val mk_fundef : (unit funcl) list -> unit def
 val mk_val_spec : val_spec_aux -> unit def
+val mk_typschm : typquant -> typ -> typschm
+val mk_fexp : id -> unit exp -> unit fexp
+val mk_fexps : (unit fexp) list -> unit fexps
+val mk_letbind : unit pat -> unit exp -> unit letbind
 
 val unaux_exp : 'a exp -> 'a exp_aux
 
 val inc_ord : order
 val dec_ord : order
 
+(* Utilites for working with kinded_ids *)
+val kopt_kid : kinded_id -> kid
+val is_nat_kopt : kinded_id -> bool
+val is_order_kopt : kinded_id -> bool
+val is_typ_kopt : kinded_id -> bool
+
+(* Some handy utility functions for constructing types. *)
+val mk_typ : typ_aux -> typ
+val mk_typ_arg : typ_arg_aux -> typ_arg
+val mk_id_typ : id -> typ
+
+(* Sail builtin types. *)
+val int_typ : typ
+val nat_typ : typ
+val atom_typ : nexp -> typ
+val range_typ : nexp -> nexp -> typ
+val bit_typ : typ
+val bool_typ : typ
+val app_typ : id -> typ_arg list -> typ
+val unit_typ : typ
+val string_typ : typ
+val real_typ : typ
+val vector_typ : nexp -> nexp -> order -> typ -> typ
+val list_typ : typ -> typ
+val exc_typ : typ
+
+val no_effect : effect
+val mk_effect : base_effect_aux list -> effect
+
+val nexp_simp : nexp -> nexp
+
+(* Utilities for building n-expressions *)
+val nconstant : int -> nexp
+val nminus : nexp -> nexp -> nexp
+val nsum : nexp -> nexp -> nexp
+val ntimes : nexp -> nexp -> nexp
+val npow2 : nexp -> nexp
+val nvar : kid -> nexp
+val nid : id -> nexp (* NOTE: Nexp_id's don't do anything currently *)
+
+(* Numeric constraint builders *)
+val nc_eq : nexp -> nexp -> n_constraint
+val nc_neq : nexp -> nexp -> n_constraint
+val nc_lteq : nexp -> nexp -> n_constraint
+val nc_gteq : nexp -> nexp -> n_constraint
+val nc_lt : nexp -> nexp -> n_constraint
+val nc_gt : nexp -> nexp -> n_constraint
+val nc_and : n_constraint -> n_constraint -> n_constraint
+val nc_or : n_constraint -> n_constraint -> n_constraint
+val nc_true : n_constraint
+val nc_false : n_constraint
+
+val quant_items : typquant -> quant_item list
+
 (* Functions to map over the annotations in sub-expressions *)
 val map_exp_annot : ('a annot -> 'b annot) -> 'a exp -> 'b exp
 val map_pat_annot : ('a annot -> 'b annot) -> 'a pat -> 'b pat
@@ -84,6 +146,7 @@ val string_of_order : order -> string
 val string_of_nexp : nexp -> string
 val string_of_typ : typ -> string
 val string_of_typ_arg : typ_arg -> string
+val string_of_annot : ('a * typ * effect) option -> string
 val string_of_n_constraint : n_constraint -> string
 val string_of_quant_item : quant_item -> string
 val string_of_typquant : typquant -> string
diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index 3919d540..a760fb42 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail_operators.lem
@@ -34,6 +34,8 @@ let adjust_start_index (start, v) = set_vector_start (start, v)
 
 let cast_vec_bool v = bitU_to_bool (extract_only_element v)
 let cast_bit_vec (start, len, b) = Vector (repeat [b] len) start false
+let cast_boolvec_bitvec (Vector bs start inc) =
+  Vector (List.map bool_to_bitU bs) start inc
 
 let pp_bitu_vector (Vector elems start inc) =
   let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in
@@ -203,6 +205,7 @@ let modulo (l,r) = hardware_mod l r
 let quot = hardware_quot
 let power (l,r) = integerPow l r
 
+let add_int = add
 let sub_int = sub
 let mult_int = mult
 
@@ -450,6 +453,9 @@ let rec repeat xs n =
 let duplicate (bit, length) =
   Vector (repeat [bit] length) (length - 1) false
 
+let replicate_bits (v, count) =
+  Vector (repeat (get_elems v) count) ((length v * count) - 1) false
+
 let compare_op op (l,r) = (op l r)
 
 let lt = compare_op (<)
@@ -529,3 +535,17 @@ let make_bitvector_undef length =
 let mask' (start, n, Vector bits _ dir) =
   let current_size = List.length bits in
   Vector (drop (current_size - (natFromInteger n)) bits) start dir
+
+
+(* Register operations *)
+
+let update_reg_range i j reg_val new_val = update reg_val i j new_val
+let update_reg_bit i reg_val bit = update_pos reg_val i bit
+let update_reg_field_range regfield i j reg_val new_val =
+  let current_field_value = regfield.get_field reg_val in
+  let new_field_value = update current_field_value i j new_val in
+  regfield.set_field reg_val new_field_value
+let write_reg_field_bit regfield i reg_val bit =
+  let current_field_value = regfield.get_field reg_val in
+  let new_field_value = update_pos current_field_value i bit in
+  regfield.set_field reg_val new_field_value
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index 8f44b2b5..f10ed9f7 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -96,6 +96,8 @@ let adjust_start_index (start, v) = set_bitvector_start (start, v)
 
 let cast_vec_bool v = bitU_to_bool (extract_only_bit v)
 let cast_bit_vec (start, len, b) = vec_to_bvec (Vector [b] start false)
+let cast_boolvec_bitvec (Vector bs start inc) =
+  vec_to_bvec (Vector (List.map bool_to_bitU bs) start inc)
 
 let pp_bitu_vector (Vector elems start inc) =
   let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in
@@ -243,6 +245,7 @@ let modulo (l,r) = hardware_mod l r
 let quot = hardware_quot
 let power (l,r) = integerPow l r
 
+let add_int = add
 let sub_int = sub
 let mult_int = mult
 
@@ -572,3 +575,16 @@ let make_bitvector_undef length =
 (* TODO *)
 val mask : forall 'a 'b. Size 'b => (integer * integer * bitvector 'a) -> bitvector 'b
 let mask (start, _, Bitvector w _ dir) = (Bitvector (zeroExtend w) start dir)
+
+(* Register operations *)
+
+let update_reg_range i j reg_val new_val = bvupdate reg_val i j new_val
+let update_reg_bit i reg_val bit = bvupdate_pos reg_val i bit
+let update_reg_field_range regfield i j reg_val new_val =
+  let current_field_value = regfield.get_field reg_val in
+  let new_field_value = bvupdate current_field_value i j new_val in
+  regfield.set_field reg_val new_field_value
+let write_reg_field_bit regfield i reg_val bit =
+  let current_field_value = regfield.get_field reg_val in
+  let new_field_value = bvupdate_pos current_field_value i bit in
+  regfield.set_field reg_val new_field_value
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index b7b87b97..4d3ddbce 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -11,6 +11,8 @@ type nn = natural
 val pow : integer -> integer -> integer
 let pow m n = m ** (natFromInteger n)
 
+let pow2 n = pow 2 n
+
 let bool_or (l, r) = (l || r)
 let bool_and (l, r) = (l && r)
 let bool_xor (l, r) = xor l r
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 879b092f..0ea65551 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -1,7 +1,6 @@
 open import Pervasives_extra
 open import Sail_impl_base
 open import Sail_values
-open import Sail_operators_mwords
 
 (* 'a is result type *)
 
@@ -51,7 +50,7 @@ let inline (>>) m n = m >>= fun _ -> n
 val exit : forall 'regs 'e 'a. 'e -> M 'regs 'a
 let exit _ s = [(Right (), s)]
 
-val early_return : forall 'regs 'r. 'r -> MR 'regs unit 'r
+val early_return : forall 'regs 'a 'r. 'r -> MR 'regs 'a 'r
 let early_return r s = [(Right (Just r), s)]
 
 val catch_early_return : forall 'regs 'a. MR 'regs 'a 'a -> M 'regs 'a
@@ -76,12 +75,11 @@ let set_reg state reg v =
   <| state with regstate = reg.write_to state.regstate v |>
 
 
-val read_mem : forall 'regs 'a 'b. Size 'b => bool -> read_kind -> bitvector 'a -> integer -> M 'regs (bitvector 'b)
+val read_mem : forall 'regs 'a 'b. Size 'b => bool -> read_kind -> integer -> integer -> M 'regs (vector bitU)
 let read_mem dir read_kind addr sz state =
-  let addr = unsigned addr in
   let addrs = range addr (addr+sz-1) in
   let memory_value = List.map (fun addr -> Map_extra.find addr state.memstate) addrs in
-  let value = vec_to_bvec (Sail_values.internal_mem_value dir memory_value) in
+  let value = Sail_values.internal_mem_value dir memory_value in
   let is_exclusive = match read_kind with
     | Sail_impl_base.Read_plain -> false
     | Sail_impl_base.Read_reserve -> true
@@ -98,9 +96,9 @@ let read_mem dir read_kind addr sz state =
 (* caps are aligned at 32 bytes *)
 let cap_alignment = (32 : integer)
 
-val read_tag : forall 'regs 'a. bool -> read_kind -> bitvector 'a -> M 'regs bitU
+val read_tag : forall 'regs 'a. bool -> read_kind -> integer -> M 'regs bitU
 let read_tag dir read_kind addr state =
-  let addr = (unsigned addr) / cap_alignment in
+  let addr = addr / cap_alignment in
   let tag = match (Map.lookup addr state.tagstate) with
     | Just t -> t
     | Nothing -> B0
@@ -125,18 +123,17 @@ let excl_result () state =
     (Left true,  <| state with last_exclusive_operation_was_load = false |>) in
   (Left false, state) :: if state.last_exclusive_operation_was_load then [success] else []
 
-val write_mem_ea : forall 'regs 'a. write_kind -> bitvector 'a -> integer -> M 'regs unit
+val write_mem_ea : forall 'regs 'a. write_kind -> integer -> integer -> M 'regs unit
 let write_mem_ea write_kind addr sz state = 
-  let addr = unsigned addr in
   [(Left (), <| state with write_ea = Just (write_kind,addr,sz) |>)]
 
-val write_mem_val : forall 'regs 'b. bitvector 'b -> M 'regs bool
+val write_mem_val : forall 'regs 'b. vector bitU -> M 'regs bool
 let write_mem_val v state =
   let (write_kind,addr,sz) = match state.write_ea with
     | Nothing -> failwith "write ea has not been announced yet"
     | Just write_ea -> write_ea end in
   let addrs = range addr (addr+sz-1) in
-  let v = external_mem_value (bvec_to_vec v) in
+  let v = external_mem_value v in
   let addresses_with_value = List.zip addrs v in
   let memstate = List.foldl (fun mem (addr,v) -> Map.insert addr v mem)
                             state.memstate addresses_with_value in
@@ -178,28 +175,6 @@ let update_reg reg f v state =
   let current_value = get_reg state reg in
   let new_value = f current_value v in
   [(Left (), set_reg state reg new_value)]
-let write_reg_range reg i j v state =
-  let current_value = get_reg state reg in
-  let new_value = bvupdate current_value i j v in
-  [(Left (), set_reg state reg new_value)]
-let write_reg_bit reg i bit state =
-  let current_value = get_reg state reg in
-  let new_value = bvupdate_pos current_value i bit in
-  [(Left (), set_reg state reg new_value)]
-let write_reg_field reg regfield =
-  update_reg reg regfield.set_field
-let write_reg_field_range reg regfield i j =
-  let upd regval v =
-    let current_field_value = regfield.get_field regval in
-    let new_field_value = bvupdate current_field_value i j v in
-    regfield.set_field regval new_field_value in
-  update_reg reg upd
-let write_reg_field_bit reg regfield i =
-  let upd regval v =
-    let current_field_value = regfield.get_field regval in
-    let new_field_value = bvupdate_pos current_field_value i v in
-    regfield.set_field regval new_field_value in
-  update_reg reg upd
 
 
 val barrier : forall 'regs. barrier_kind -> M 'regs unit
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 8e5fd35f..74faba25 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -1012,6 +1012,8 @@ let typschm_of_string order str =
   let (typschm, _, _) = to_ast_typschm initial_kind_env order typschm in
   typschm
 
+let val_spec_of_string order id str = mk_val_spec (VS_extern_no_rename (typschm_of_string order str, id))
+
 let val_spec_ids (Defs defs) =
   let val_spec_id (VS_aux (vs_aux, _)) =
     match vs_aux with
@@ -1027,14 +1029,56 @@ let val_spec_ids (Defs defs) =
   in
   IdSet.of_list (vs_ids defs)
 
+let quant_item_param = function
+  | QI_aux (QI_id kopt, _) when is_nat_kopt kopt -> [prepend_id "atom_" (id_of_kid (kopt_kid kopt))]
+  | QI_aux (QI_id kopt, _) when is_typ_kopt kopt -> [prepend_id "typ_" (id_of_kid (kopt_kid kopt))]
+  | _ -> []
+let quant_item_typ = function
+  | QI_aux (QI_id kopt, _) when is_nat_kopt kopt -> [atom_typ (nvar (kopt_kid kopt))]
+  | QI_aux (QI_id kopt, _) when is_typ_kopt kopt -> [mk_typ (Typ_var (kopt_kid kopt))]
+  | _ -> []
+let quant_item_arg = function
+  | QI_aux (QI_id kopt, _) when is_nat_kopt kopt -> [mk_typ_arg (Typ_arg_nexp (nvar (kopt_kid kopt)))]
+  | QI_aux (QI_id kopt, _) when is_typ_kopt kopt -> [mk_typ_arg (Typ_arg_typ (mk_typ (Typ_var (kopt_kid kopt))))]
+  | _ -> []
+let undefined_typschm id typq =
+  let qis = quant_items typq in
+  if qis = [] then
+    mk_typschm typq (mk_typ (Typ_fn (unit_typ, mk_typ (Typ_id id), mk_effect [BE_undef])))
+  else
+    let arg_typ = mk_typ (Typ_tup (List.concat (List.map quant_item_typ qis))) in
+    let ret_typ = app_typ id (List.concat (List.map quant_item_arg qis)) in
+    mk_typschm typq (mk_typ (Typ_fn (arg_typ, ret_typ, mk_effect [BE_undef])))
+
 let generate_undefineds vs_ids (Defs defs) =
+  let gen_vs id str =
+    if (IdSet.mem id vs_ids) then [] else [val_spec_of_string dec_ord id str]
+  in
+  let undefined_builtins = List.concat
+    [gen_vs (mk_id "internal_pick") "forall 'a:Type. list('a) -> 'a effect {undef}";
+     gen_vs (mk_id "undefined_bool") "unit -> bool effect {undef}";
+     gen_vs (mk_id "undefined_bit") "unit -> bit effect {undef}";
+     gen_vs (mk_id "undefined_int") "unit -> int effect {undef}";
+     gen_vs (mk_id "undefined_string") "unit -> string effect {undef}";
+     gen_vs (mk_id "undefined_range") "forall 'n 'm. (atom('n), atom('m)) -> range('n,'m) effect {undef}";
+     (* FIXME: How to handle inc/dec order correctly? *)
+     gen_vs (mk_id "undefined_vector") "forall 'n 'm 'a:Type. (atom('n), atom('m), 'a) -> vector('n, 'm, dec,'a) effect {undef}";
+     gen_vs (mk_id "undefined_unit") "unit -> unit effect {undef}"]
+  in
   let undefined_td = function
     | TD_enum (id, _, ids, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
        let typschm = typschm_of_string dec_ord ("unit -> " ^ string_of_id id ^ " effect {undef}") in
        [mk_val_spec (VS_val_spec (typschm, prepend_id "undefined_" id));
         mk_fundef [mk_funcl (prepend_id "undefined_" id)
                             (mk_pat (P_lit (mk_lit L_unit)))
-                            (mk_exp (E_lit (mk_lit L_undef)))]]
+                            (mk_exp (E_app (mk_id "internal_pick",
+                                            [mk_exp (E_list (List.map (fun id -> mk_exp (E_id id)) ids))])))]]
+    | TD_record (id, _, typq, fields, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
+       let pat = mk_pat (P_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id)))) in
+       [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id));
+        mk_fundef [mk_funcl (prepend_id "undefined_" id)
+                            pat
+                            (mk_exp (E_record (mk_fexps (List.map (fun (_, id) -> mk_fexp id (mk_lit_exp L_undef)) fields))))]]
     | _ -> []
   in
   let rec undefined_defs = function
@@ -1044,9 +1088,28 @@ let generate_undefineds vs_ids (Defs defs) =
        def :: undefined_defs defs
     | [] -> []
   in
-  Defs (undefined_defs defs)
+  Defs (undefined_builtins @ undefined_defs defs)
+
+let rec get_registers = function
+  | DEF_reg_dec (DEC_aux (DEC_reg (typ, id), _)) :: defs -> (typ, id) :: get_registers defs
+  | def :: defs -> get_registers defs
+  | [] -> []
+
+let generate_initialize_registers vs_ids (Defs defs) =
+  let regs = get_registers defs in
+  let initialize_registers =
+    if IdSet.mem (mk_id "initialize_registers") vs_ids || regs = [] then []
+    else
+      [val_spec_of_string dec_ord (mk_id "initialize_registers") "unit -> unit effect {undef, wreg}";
+       mk_fundef [mk_funcl (mk_id "initialize_registers")
+                           (mk_pat (P_lit (mk_lit L_unit)))
+                           (mk_exp (E_block (List.map (fun (typ, id) -> mk_exp (E_assign (mk_lexp (LEXP_cast (typ, id)), mk_lit_exp L_undef))) regs)))]]
+  in
+  Defs (defs @ initialize_registers)
+
 
 let process_ast order defs =
   let (ast, _, _) = to_ast Nameset.empty initial_kind_env order defs in
   let vs_ids = val_spec_ids ast in
-  generate_undefineds vs_ids ast
+  let ast = generate_undefineds vs_ids ast in
+  generate_initialize_registers vs_ids ast
diff --git a/src/initial_check.mli b/src/initial_check.mli
index ed4eb0bf..86b5ca3b 100644
--- a/src/initial_check.mli
+++ b/src/initial_check.mli
@@ -41,6 +41,8 @@
 (**************************************************************************)
 
 open Ast
+open Ast_util
 
 val process_ast : order -> Parse_ast.defs -> unit defs
 
+val val_spec_ids : 'a defs -> IdSet.t
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
new file mode 100644
index 00000000..8b88a07e
--- /dev/null
+++ b/src/ocaml_backend.ml
@@ -0,0 +1,347 @@
+open Ast
+open Ast_util
+open PPrint
+open Type_check
+
+type ctx =
+  { register_inits : tannot exp list;
+    externs : id Bindings.t
+  }
+
+let empty_ctx =
+  { register_inits = [];
+    externs = Bindings.empty
+  }
+
+let zchar c =
+  let zc c = "z" ^ String.make 1 c in
+  if Char.code c <= 41 then zc (Char.chr (Char.code c + 16))
+  else if Char.code c <= 47 then zc (Char.chr (Char.code c + 23))
+  else if Char.code c <= 57 then String.make 1 c
+  else if Char.code c <= 64 then zc (Char.chr (Char.code c + 13))
+  else if Char.code c <= 90 then String.make 1 c
+  else if Char.code c <= 94 then zc (Char.chr (Char.code c - 13))
+  else if Char.code c <= 95 then "_"
+  else if Char.code c <= 96 then zc (Char.chr (Char.code c - 13))
+  else if Char.code c <= 121 then String.make 1 c
+  else if Char.code c <= 122 then "zz"
+  else if Char.code c <= 126 then zc (Char.chr (Char.code c - 39))
+  else raise (Invalid_argument "zchar")
+
+let zencode_string str = "z" ^ List.fold_left (fun s1 s2 -> s1 ^ s2) "" (List.map zchar (Util.string_to_list str))
+
+let zencode_upper_string str = "Z" ^ List.fold_left (fun s1 s2 -> s1 ^ s2) "" (List.map zchar (Util.string_to_list str))
+
+let zencode ctx id =
+  try string (string_of_id (Bindings.find id ctx.externs)) with
+  | Not_found -> string (zencode_string (string_of_id id))
+
+let zencode_upper ctx id =
+  try string (string_of_id (Bindings.find id ctx.externs)) with
+  | Not_found -> string (zencode_upper_string (string_of_id id))
+
+let zencode_kid kid = string ("'" ^ zencode_string (string_of_id (id_of_kid kid)))
+
+let ocaml_typ_id ctx = function
+  | id when Id.compare id (mk_id "string") = 0 -> string "string"
+  | id when Id.compare id (mk_id "list") = 0 -> string "list"
+  | id when Id.compare id (mk_id "bit") = 0 -> string "bit"
+  | id when Id.compare id (mk_id "int") = 0 -> string "big_int"
+  | id when Id.compare id (mk_id "bool") = 0 -> string "bool"
+  | id -> zencode ctx id
+
+let rec ocaml_typ ctx (Typ_aux (typ_aux, _)) =
+  match typ_aux with
+  | Typ_id id -> ocaml_typ_id ctx id
+  | Typ_app (id, []) -> ocaml_typ_id ctx id
+  | Typ_app (id, typs) -> parens (separate_map (string " * ") (ocaml_typ_arg ctx) typs) ^^ space ^^ ocaml_typ_id ctx id
+  | Typ_tup typs -> parens (separate_map (string " * ") (ocaml_typ ctx) typs)
+  | Typ_fn (typ1, typ2, _) -> separate space [ocaml_typ ctx typ1; string "->"; ocaml_typ ctx typ2]
+  | Typ_var kid -> zencode_kid kid
+  | Typ_exist _ | Typ_wild -> assert false
+and ocaml_typ_arg ctx (Typ_arg_aux (typ_arg_aux, _) as typ_arg) =
+  match typ_arg_aux with
+  | Typ_arg_typ typ -> ocaml_typ ctx typ
+  | _ -> failwith ("OCaml: unexpected type argument " ^ string_of_typ_arg typ_arg)
+
+let ocaml_typquant typq =
+  let ocaml_qi = function
+    | QI_aux (QI_id kopt, _) -> zencode_kid (kopt_kid kopt)
+    | QI_aux (QI_const _, _) -> failwith "Ocaml type quantifiers should no longer contain constraints"
+  in
+  match quant_items typq with
+  | [] -> empty
+  | [qi] -> ocaml_qi qi
+  | qis -> parens (separate_map (string " * ") ocaml_qi qis)
+
+let ocaml_lit (L_aux (lit_aux, _)) =
+  match lit_aux with
+  | L_unit -> string "()"
+  | L_zero -> string "B0"
+  | L_one -> string "B1"
+  | L_true -> string "true"
+  | L_false -> string "false"
+  | L_num n -> parens (string "big_int_of_int" ^^ space ^^ string (string_of_int n))
+  | L_undef -> failwith "undefined should have been re-written prior to ocaml backend"
+  | L_string str -> dquotes (string (String.escaped str))
+  | _ -> string "LIT"
+
+let rec ocaml_pat ctx (P_aux (pat_aux, _) as pat) =
+  match pat_aux with
+  | P_id id -> zencode ctx id
+  | P_lit lit -> ocaml_lit lit
+  | P_typ (_, pat) -> ocaml_pat ctx pat
+  | P_tup pats -> parens (separate_map (comma ^^ space) (ocaml_pat ctx) pats)
+  | P_list pats -> brackets (separate_map (semi ^^ space) (ocaml_pat ctx) pats)
+  | P_wild -> string "_"
+  | P_as (pat, id) -> separate space [ocaml_pat ctx pat; string "as"; zencode ctx id]
+  | _ -> string ("PAT<" ^ string_of_pat pat ^ ">")
+
+let begin_end doc = group (string "begin" ^^ nest 2 (break 1 ^^ doc) ^/^ string "end")
+
+let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) =
+  match exp_aux with
+  | E_app (f, [x]) -> zencode ctx f ^^ space ^^ ocaml_atomic_exp ctx x
+  | E_app (f, xs) -> zencode ctx f ^^ space ^^ parens (separate_map (comma ^^ space) (ocaml_exp ctx) xs)
+  | E_return exp -> separate space [string "r.return"; ocaml_atomic_exp ctx exp]
+  | E_assert (exp, _) -> separate space [string "assert"; ocaml_atomic_exp ctx exp]
+  | E_cast (_, exp) -> ocaml_exp ctx exp
+  | E_block [exp] -> ocaml_exp ctx exp
+  | E_block [] -> string "()"
+  | E_block exps -> begin_end (ocaml_block ctx exps)
+  | E_field (exp, id) -> ocaml_atomic_exp ctx exp ^^ dot ^^ zencode ctx id
+  | E_exit exp -> string "failwith" ^^ space ^^ dquotes (string (String.escaped (string_of_exp exp)))
+  | E_case (exp, pexps) ->
+     begin_end (separate space [string "match"; ocaml_atomic_exp ctx exp; string "with"]
+                ^/^ ocaml_pexps ctx pexps)
+  | E_assign (lexp, exp) -> separate space [ocaml_lexp ctx lexp; string ":="; ocaml_exp ctx exp]
+  | E_if (c, t, e) -> separate space [string "if"; ocaml_atomic_exp ctx c;
+                                      string "then"; ocaml_atomic_exp ctx t;
+                                      string "else"; ocaml_atomic_exp ctx e]
+  | E_record (FES_aux (FES_Fexps (fexps, _), _)) ->
+     enclose lbrace rbrace (group (separate_map (semi ^^ break 1) (ocaml_fexp ctx) fexps))
+  | E_record_update (exp, FES_aux (FES_Fexps (fexps, _), _)) ->
+     enclose lbrace rbrace (separate space [ocaml_atomic_exp ctx exp;
+                                            string "with";
+                                            separate_map (semi ^^ space) (ocaml_fexp ctx) fexps])
+  | E_let (lb, exp) ->
+     separate space [string "let"; ocaml_letbind ctx lb; string "in"]
+     ^/^ ocaml_exp ctx exp
+  | E_internal_let (lexp, exp1, exp2) ->
+     separate space [string "let"; ocaml_atomic_lexp ctx lexp;
+                     equals; string "ref"; ocaml_atomic_exp ctx exp1; string "in"]
+     ^/^ ocaml_exp ctx exp2
+  | E_lit _ | E_list _ | E_id _ | E_tuple _ -> ocaml_atomic_exp ctx exp
+  | _ -> string ("EXP(" ^ string_of_exp exp ^ ")")
+and ocaml_letbind ctx (LB_aux (lb_aux, _)) =
+  match lb_aux with
+  | LB_val_implicit (pat, exp) -> separate space [ocaml_pat ctx pat; equals; ocaml_atomic_exp ctx exp]
+  | _ -> failwith "Ocaml: Explicit letbind found"
+and ocaml_pexps ctx = function
+  | [pexp] -> ocaml_pexp ctx pexp
+  | pexp :: pexps -> ocaml_pexp ctx pexp ^/^ ocaml_pexps ctx pexps
+  | [] -> empty
+and ocaml_pexp ctx = function
+  | Pat_aux (Pat_exp (pat, exp), _) ->
+     separate space [bar; ocaml_pat ctx pat; string "->"]
+     ^//^ group (ocaml_exp ctx exp)
+  | Pat_aux (Pat_when (pat, wh, exp), _) ->
+     separate space [bar; ocaml_pat ctx pat; string "when"; ocaml_atomic_exp ctx exp; string "->"]
+     ^//^ group (ocaml_exp ctx exp)
+and ocaml_block ctx = function
+  | [exp] -> ocaml_exp ctx exp
+  | exp :: exps -> ocaml_exp ctx exp ^^ semi ^/^ ocaml_block ctx exps
+  | _ -> assert false
+and ocaml_fexp ctx (FE_aux (FE_Fexp (id, exp), _)) =
+  separate space [zencode ctx id; equals; ocaml_exp ctx exp]
+and ocaml_atomic_exp ctx (E_aux (exp_aux, _) as exp) =
+  match exp_aux with
+  | E_lit lit -> ocaml_lit lit
+  | E_id id ->
+     begin
+       match Env.lookup_id id (env_of exp) with
+       | Local (Immutable, _) | Unbound -> zencode ctx id
+       | Enum _ -> zencode_upper ctx id
+       | Register _ | Local (Mutable, _) -> bang ^^ zencode ctx id
+       | _ -> failwith ("Union constructor: " ^ zencode_string (string_of_id id))
+     end
+  | E_list exps -> enclose lbracket rbracket (separate_map (semi ^^ space) (ocaml_exp ctx) exps)
+  | E_tuple exps -> parens (separate_map (comma ^^ space) (ocaml_exp ctx) exps)
+  | _ -> parens (ocaml_exp ctx exp)
+and ocaml_lexp ctx (LEXP_aux (lexp_aux, _) as lexp) =
+  match lexp_aux with
+  | LEXP_cast _ | LEXP_id _ -> ocaml_atomic_lexp ctx lexp
+  | _ -> string ("LEXP<" ^ string_of_lexp lexp ^ ">")
+and ocaml_atomic_lexp ctx (LEXP_aux (lexp_aux, _) as lexp) =
+  match lexp_aux with
+  | LEXP_cast (_, id) -> zencode ctx id
+  | LEXP_id id -> zencode ctx id
+  | _ -> parens (ocaml_lexp ctx lexp)
+
+let rec get_initialize_registers = function
+  | DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, _, E_aux (E_block inits, _)), _)]), _)) :: defs
+       when Id.compare id (mk_id "initialize_registers") = 0 ->
+     inits
+  | _ :: defs -> get_initialize_registers defs
+  | [] -> []
+
+let initial_value_for id inits =
+  let find_reg = function
+    | E_aux (E_assign (LEXP_aux (LEXP_cast (_, reg_id), _), init), _) when Id.compare id reg_id = 0 -> Some init
+    | _ -> None
+  in
+  match Util.option_first find_reg inits with
+  | Some init -> init
+  | None -> failwith ("No assignment to register ^ " ^ string_of_id id ^ " in initialize_registers")
+
+let ocaml_dec_spec ctx (DEC_aux (reg, _)) =
+  match reg with
+  | DEC_reg (typ, id) ->
+     separate space [string "let"; zencode ctx id; colon;
+                     parens (ocaml_typ ctx typ); string "ref"; equals;
+                     string "ref"; parens (ocaml_exp ctx (initial_value_for id ctx.register_inits))]
+  | _ -> failwith "Unsupported register declaration"
+
+let funcls_id = function
+  | [] -> failwith "Ocaml: empty function"
+  | FCL_aux (FCL_Funcl (id, pat, exp),_) :: _ -> id
+
+let ocaml_funcl_match ctx (FCL_aux (FCL_Funcl (id, pat, exp), _)) =
+  separate space [bar; ocaml_pat ctx pat; string "->"]
+  ^//^ group (string "with_return (fun r ->" ^//^ ocaml_exp ctx exp ^^ rparen)
+
+let rec ocaml_funcl_matches ctx = function
+  | [] -> failwith "Ocaml: empty function"
+  | [clause] -> ocaml_funcl_match ctx clause
+  | (clause :: clauses) -> ocaml_funcl_match ctx clause ^/^ ocaml_funcl_matches ctx clauses
+
+let ocaml_funcls ctx = function
+  | [] -> failwith "Ocaml: empty function"
+  | [FCL_aux (FCL_Funcl (id, pat, exp),_)] ->
+     separate space [string "let"; zencode ctx id; ocaml_pat ctx pat; equals; string "with_return (fun r ->"]
+     ^//^ ocaml_exp ctx exp
+     ^^ rparen
+  | funcls ->
+     let id = funcls_id funcls in
+     separate space [string "let"; zencode ctx id; equals; string "function"]
+     ^//^ ocaml_funcl_matches ctx funcls
+
+let ocaml_fundef ctx (FD_aux (FD_function (_, _, _, funcls), _)) =
+  ocaml_funcls ctx funcls
+
+let rec ocaml_fields ctx =
+  let ocaml_field typ id =
+    separate space [zencode ctx id; colon; ocaml_typ ctx typ]
+  in
+  function
+  | [(typ, id)] -> ocaml_field typ id
+  | (typ, id) :: fields -> ocaml_field typ id ^^ semi ^/^ ocaml_fields ctx fields
+  | [] -> empty
+
+let rec ocaml_cases ctx =
+  let ocaml_case = function
+    | Tu_aux (Tu_id id, _) -> separate space [bar; zencode ctx id]
+    | Tu_aux (Tu_ty_id (typ, id), _) -> separate space [bar; zencode ctx id; string "of"; ocaml_typ ctx typ]
+  in
+  function
+  | [tu] -> ocaml_case tu
+  | tu :: tus -> ocaml_case tu ^/^ ocaml_cases ctx tus
+  | [] -> empty
+
+let rec ocaml_enum ctx = function
+  | [id] -> zencode_upper ctx id
+  | id :: ids -> zencode_upper ctx id ^/^ (bar ^^ space ^^ ocaml_enum ctx ids)
+  | [] -> empty
+
+let ocaml_typedef ctx (TD_aux (td_aux, _)) =
+  match td_aux with
+  | TD_record (id, _, typq, fields, _) ->
+     (separate space [string "type"; ocaml_typquant typq; zencode ctx id; equals; lbrace]
+      ^//^ ocaml_fields ctx fields)
+     ^/^ rbrace
+  | TD_variant (id, _, typq, cases, _) ->
+     separate space [string "type"; ocaml_typquant typq; zencode ctx id; equals]
+     ^//^ ocaml_cases ctx cases
+  | TD_enum (id, _, ids, _) ->
+     separate space [string "type"; zencode ctx id; equals]
+     ^//^ (bar ^^ space ^^ ocaml_enum ctx ids)
+  | TD_abbrev (id, _, TypSchm_aux (TypSchm_ts (typq, typ), _)) ->
+     separate space [string "type"; ocaml_typquant typq; zencode ctx id; equals; ocaml_typ ctx typ]
+  | _ -> failwith "Unsupported typedef"
+
+let get_externs (Defs defs) =
+  let extern_id (VS_aux (vs_aux, _)) =
+    match vs_aux with
+    | VS_val_spec (typschm, id) -> []
+    | VS_extern_no_rename (typschm, id) -> [(id, id)]
+    | VS_extern_spec (typschm, id, name) -> [(id, mk_id name)]
+    | VS_cast_spec (typschm, id) -> []
+  in
+  let rec extern_ids = function
+    | DEF_spec vs :: defs -> extern_id vs :: extern_ids defs
+    | def :: defs -> extern_ids defs
+    | [] -> []
+  in
+  List.fold_left (fun exts (id, name) -> Bindings.add id name exts) Bindings.empty (List.concat (extern_ids defs))
+
+let ocaml_def_end = string ";;" ^^ twice hardline
+
+let ocaml_def ctx def = match def with
+  | DEF_reg_dec ds -> group (ocaml_dec_spec ctx ds) ^^ ocaml_def_end
+  | DEF_fundef fd -> group (ocaml_fundef ctx fd) ^^ ocaml_def_end
+  | DEF_type td -> group (ocaml_typedef ctx td) ^^ ocaml_def_end
+  | _ -> empty
+
+let ocaml_defs (Defs defs) =
+  let ctx = { register_inits = get_initialize_registers defs;
+              externs = get_externs (Defs defs)
+            }
+  in
+  let empty_reg_init =
+    if ctx.register_inits = []
+    then
+      separate space [string "let"; string "initialize_registers"; string "()"; equals; string "()"]
+      ^^ ocaml_def_end
+    else empty
+  in
+  (string "open Sail_lib;;" ^^ hardline)
+  ^^ (string "open Big_int" ^^ ocaml_def_end)
+  ^^ concat (List.map (ocaml_def ctx) defs)
+  ^^ empty_reg_init
+
+let ocaml_main spec =
+  concat [separate space [string "open"; string (String.capitalize spec)] ^^ ocaml_def_end;
+          separate space [string "let"; string "()"; equals]
+          ^//^ (string "Random.self_init ();"
+                ^/^ string "initialize_registers ();"
+                ^/^ string "zmain ()")
+         ]
+
+let ocaml_pp_defs f defs =
+  ToChannel.pretty 1. 80 f (ocaml_defs defs)
+
+let ocaml_compile spec defs =
+  let sail_lib_dir =
+    try Sys.getenv "SAILLIBDIR" with
+    | Not_found -> failwith "Environment variable SAILLIBDIR needs to be set"
+  in
+  if Sys.file_exists "_sbuild" then () else Unix.mkdir "_sbuild" 0o775;
+  let cwd = Unix.getcwd () in
+  Unix.chdir "_sbuild";
+  let _ = Unix.system ("cp " ^ sail_lib_dir ^ "/sail_lib.ml .") in
+  let out_chan = open_out (spec ^ ".ml") in
+  ocaml_pp_defs out_chan defs;
+  close_out out_chan;
+  if IdSet.mem (mk_id "main") (Initial_check.val_spec_ids defs)
+  then
+    let out_chan = open_out "main.ml" in
+    ToChannel.pretty 1. 80 out_chan (ocaml_main spec);
+    close_out out_chan;
+    let _ = Unix.system "ocamlbuild -lib nums main.native" in
+    let _ = Unix.system ("cp main.native " ^ cwd ^ "/" ^ spec) in
+    ()
+  else
+    let _ = Unix.system ("ocamlbuild -lib nums " ^ spec ^ ".cmo") in
+    ();
+  Unix.chdir cwd
+
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 3951ab51..b259611d 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -288,6 +288,7 @@ exp_aux =  (* Expression *)
  | E_try of exp * pexp list
  | E_return of exp
  | E_assert of exp * exp
+ | E_internal_let of exp * exp * exp
 
 and exp = 
    E_aux of exp_aux * l
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 7671c26b..5e0d39a0 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -58,7 +58,11 @@ let langlebar = string "<|"
 let ranglebar = string "|>"
 let anglebars = enclose langlebar ranglebar
 
-let fix_id name = match name with
+let is_number_char c =
+  c = '0' || c = '1' || c = '2' || c = '3' || c = '4' || c = '5' ||
+  c = '6' || c = '7' || c = '8' || c = '9'
+
+let fix_id remove_tick name = match name with
   | "assert"
   | "lsl"
   | "lsr"
@@ -76,22 +80,17 @@ let fix_id name = match name with
   | "EQ"
   | "integer"
     -> name ^ "'"
-  | _ -> name
-
-let is_number char =
-  char = '0' || char = '1' || char = '2' || char = '3' || char = '4' || char = '5' ||
-  char = '6' || char = '7' || char = '8' || char = '9'
+  | _ ->
+     if name.[0] = '\'' then
+       let var = String.sub name 1 (String.length name - 1) in
+       if remove_tick then var else (var ^ "'")
+     else if is_number_char(name.[0]) then
+       ("v" ^ name ^ "'")
+     else name
 
 let doc_id_lem (Id_aux(i,_)) =
   match i with
-  | Id i ->
-     (* this not the right place to do this, just a workaround *)
-     if i.[0] = '\'' then
-       string ((String.sub i 1 (String.length i - 1)) ^ "'")
-     else if is_number(i.[0]) then
-       string ("v" ^ i ^ "'")
-     else
-       string (fix_id i)
+  | Id i -> string (fix_id false i)
   | DeIid x ->
      (* add an extra space through empty to avoid a closing-comment
       * token in case of x ending with star. *)
@@ -102,7 +101,7 @@ let doc_id_lem_type (Id_aux(i,_)) =
   | Id("int") -> string "ii"
   | Id("nat") -> string "ii"
   | Id("option") -> string "maybe"
-  | Id i -> string (fix_id i)
+  | Id i -> string (fix_id false i)
   | DeIid x ->
      (* add an extra space through empty to avoid a closing-comment
       * token in case of x ending with star. *)
@@ -115,12 +114,14 @@ let doc_id_lem_ctor (Id_aux(i,_)) =
   | Id("nat") -> string "integer"
   | Id("Some") -> string "Just"
   | Id("None") -> string "Nothing"
-  | Id i -> string (fix_id (String.capitalize i))
+  | Id i -> string (fix_id false (String.capitalize i))
   | DeIid x ->
      (* add an extra space through empty to avoid a closing-comment
       * token in case of x ending with star. *)
      separate space [colon; string (String.capitalize x); empty]
 
+let doc_var_lem kid = string (fix_id true (string_of_kid kid))
+
 let effectful_set =
   List.exists
     (fun (BE_aux (eff,_)) ->
@@ -230,6 +231,7 @@ let rec contains_t_pp_var (Typ_aux (t,a) as typ) = match t with
   | Typ_wild -> true
   | Typ_id _ -> false
   | Typ_var _ -> true
+  | Typ_exist _ -> true
   | Typ_fn (t1,t2,_) -> contains_t_pp_var t1 || contains_t_pp_var t2
   | Typ_tup ts -> List.exists contains_t_pp_var ts
   | Typ_app (c,targs) ->
@@ -321,6 +323,7 @@ let rec doc_pat_lem sequential mwords apat_needed (P_aux (p,(l,annot)) as pa) =
      begin match id with
      | Id_aux (Id "None",_) -> string "Nothing" (* workaround temporary issue *)
      | _ -> doc_id_lem id end
+  | P_var kid -> doc_var_lem kid
   | P_as(p,id) -> parens (separate space [doc_pat_lem sequential mwords true p; string "as"; doc_id_lem id])
   | P_typ(typ,p) ->
     let doc_p = doc_pat_lem sequential mwords true p in
@@ -391,15 +394,16 @@ let doc_exp_lem, doc_let_lem =
                    underscore ^^
                    doc_id_lem id in
                  liftR ((prefix 2 1)
-                   (string "write_reg_field_range")
+                   (string "update_reg")
                    (align (doc_lexp_deref_lem sequential mwords early_ret le ^^ space^^
-                             field_ref ^/^ expY e2 ^/^ expY e3 ^/^ expY e)))
+                      parens (string "update_reg_field_range" ^/^ field_ref ^/^ expY e2 ^/^ expY e3) ^/^ expY e)))
             | _ ->
                liftR ((prefix 2 1)
-                 (string "write_reg_range")
-                 (align (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^ expY e2 ^/^ expY e3 ^/^ expY e)))
+                 (string "update_reg")
+                 (align (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^
+                   parens (string "update_reg_range" ^/^ expY e2 ^/^ expY e3) ^/^ expY e)))
            )
-        | LEXP_vector (le,e2) when is_bit_typ t ->
+        | LEXP_vector (le,e2) ->
            (match le with
             | LEXP_aux (LEXP_field ((LEXP_aux (_, lannot) as le),id), fannot) ->
                if is_bit_typ (typ_of_annot fannot) then
@@ -410,12 +414,14 @@ let doc_exp_lem, doc_let_lem =
                    underscore ^^
                    doc_id_lem id in
                  liftR ((prefix 2 1)
-                   (string "write_reg_field_bit")
-                   (align (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^ field_ref ^/^ expY e2 ^/^ expY e)))
+                   (string "update_reg")
+                   (align (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^
+                     parens (string "update_reg_field_bit" ^/^ field_ref ^/^ expY e2) ^/^ expY e)))
             | _ ->
                liftR ((prefix 2 1)
-                 (string "write_reg_bit")
-                 (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^ expY e2 ^/^ expY e))
+                 (string "update_reg")
+                 (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^
+                   parens (string "update_reg_bit" ^/^ expY e2) ^/^ expY e))
            )
         (* | LEXP_field (le,id) when is_bit_typ t ->
            liftR ((prefix 2 1)
@@ -425,9 +431,11 @@ let doc_exp_lem, doc_let_lem =
           let field_ref =
             doc_id_lem (typ_id_of (typ_of_annot lannot)) ^^
             underscore ^^
-            doc_id_lem id in
+            doc_id_lem id ^^
+            dot ^^
+            string "set_field" in
            liftR ((prefix 2 1)
-             (string "write_reg_field")
+             (string "update_reg")
              (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^
                 field_ref ^/^ expY e))
         (* | (LEXP_id id | LEXP_cast (_,id)), t, Alias alias_info ->
@@ -692,7 +700,7 @@ let doc_exp_lem, doc_let_lem =
        let recordtyp = match annot with
          | Some (env, Typ_aux (Typ_id tid,_), _) when Env.is_record tid env ->
            tid
-         | _ ->  raise (report l "cannot get record type") in
+         | _ ->  raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in
        let epp = anglebars (space ^^ (align (separate_map
                                           (semi_sp ^^ break 1)
                                           (doc_fexp sequential mwords early_ret recordtyp) fexps)) ^^ space) in
@@ -702,7 +710,7 @@ let doc_exp_lem, doc_let_lem =
        let recordtyp = match eannot with
          | Some (env, Typ_aux (Typ_id tid,_), _) when Env.is_record tid env ->
            tid
-         | _ ->  raise (report l "cannot get record type") in
+         | _ ->  raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in
        anglebars (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp sequential mwords early_ret recordtyp) fexps))
     | E_vector exps ->
        let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
@@ -801,21 +809,26 @@ let doc_exp_lem, doc_let_lem =
        if aexp_needed then parens (align bepp) else bepp
     | E_vector_update(v,e1,e2) ->
        let t = typ_of full_exp in
+       let (_, _, ord, _) = vector_typ_args_of (Env.base_typ_of (env_of full_exp) t) in
+       let ord_suffix = if is_order_inc ord then "_inc" else "_dec" in
        let call =
          if is_bitvector_typ t (*&& mwords*)
-         then "bitvector_update_pos"
-         else "update_pos" in
-       let epp = separate space [string call;expY v;expY e1;expY e2] in
+         then "bitvector_update_pos" ^ ord_suffix
+         else "update_pos" ^ ord_suffix in
+       let epp = string call ^^ space ^^ parens (separate comma_sp [expY v;expY e1;expY e2]) in
        if aexp_needed then parens (align epp) else epp
     | E_vector_update_subrange(v,e1,e2,e3) ->
        let t = typ_of full_exp in
+       let (_, _, ord, _) = vector_typ_args_of (Env.base_typ_of (env_of full_exp) t) in
+       let ord_suffix = if is_order_inc ord then "_inc" else "_dec" in
        let call =
          if is_bitvector_typ t (*&& mwords*)
-         then "bitvector_update"
-         else "update" in
-       let epp = align (string call ^//^
-                          group (group (expY v) ^/^ group (expY e1) ^/^ group (expY e2)) ^/^
-                            group (expY e3)) in
+         then "bitvector_update" ^ ord_suffix
+         else "update" ^ ord_suffix in
+       let epp =
+         align (string call ^//^
+           parens (separate comma_sp
+             [group (expY v); group (expY e1); group (expY e2); group (expY e3)])) in
        if aexp_needed then parens (align epp) else epp
     | E_list exps ->
        brackets (separate_map semi (expN) exps)
@@ -843,8 +856,10 @@ let doc_exp_lem, doc_let_lem =
        if aexp_needed then parens (align epp) else align epp
     | E_exit e -> liftR (separate space [string "exit"; expY e;])
     | E_assert (e1,e2) ->
-       let epp = separate space [string "assert'"; expY e1; expY e2] in
-       if aexp_needed then parens (align epp) else align epp
+       (* FIXME needs pretty-printing of E_constraint; ignore for now *)
+       string "()"
+       (* let epp = separate space [string "assert'"; expY e1; expY e2] in
+       if aexp_needed then parens (align epp) else align epp *)
     | E_app_infix (e1,id,e2) ->
        (* TODO: Should have been removed by the new type checker; check with Alasdair *)
        raise (Reporting_basic.err_unreachable l
@@ -999,6 +1014,7 @@ let doc_exp_lem, doc_let_lem =
                                  top_exp sequential mwords early_ret true e])
     | LEXP_id id -> doc_id_lem id
     | LEXP_cast (typ,id) -> doc_id_lem id
+    | LEXP_tup lexps -> parens (separate_map comma_sp (doc_lexp_deref_lem sequential mwords early_ret) lexps)
     | _ ->
        raise (Reporting_basic.err_unreachable l ("doc_lexp_deref_lem: Shouldn't happen"))
              (* expose doc_exp_lem and doc_let *)
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index adddcee6..5edf9d12 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -221,6 +221,8 @@ and pp_format_nexp_constraint_lem (NC_aux(nc,l)) =
   | NC_not_equal(n1,n2) -> "(NC_not_equal " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")"
   | NC_or(nc1,nc2) -> "(NC_or " ^ pp_format_nexp_constraint_lem nc1 ^ " " ^ pp_format_nexp_constraint_lem nc2 ^ ")"
   | NC_and(nc1,nc2) -> "(NC_and " ^ pp_format_nexp_constraint_lem nc1 ^ " " ^ pp_format_nexp_constraint_lem nc2 ^ ")"
+  | NC_true -> "NC_true"
+  | NC_false -> "NC_false"
   | NC_nat_set_bounded(id,bounds) -> "(NC_nat_set_bounded " ^
     pp_format_var_lem id ^
       " [" ^
@@ -326,6 +328,7 @@ let rec pp_format_pat_lem (P_aux(p,(l,annot))) =
   | P_lit(lit) -> "(P_lit " ^ pp_format_lit_lem lit ^ ")"
   | P_wild -> "P_wild"
   | P_id(id) -> "(P_id " ^ pp_format_id_lem id ^ ")"
+  | P_var(kid) -> "(P_var " ^ pp_format_var_lem kid ^ ")"
   | P_as(pat,id) -> "(P_as " ^ pp_format_pat_lem pat ^ " " ^ pp_format_id_lem id ^ ")"
   | P_typ(typ,pat) -> "(P_typ " ^ pp_format_typ_lem typ ^ " " ^ pp_format_pat_lem pat ^ ")"
   | P_app(id,pats) -> "(P_app " ^ pp_format_id_lem id ^ " [" ^
diff --git a/src/process_file.ml b/src/process_file.ml
index b91f6e70..22f25f6e 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -41,6 +41,8 @@
 (**************************************************************************)
 
 let opt_new_parser = ref false
+let opt_lem_sequential = ref false
+let opt_lem_mwords = ref false
 
 type out_type =
   | Lem_ast_out
@@ -139,31 +141,28 @@ let generated_line f =
 
 let output_lem filename libs defs =
   let generated_line = generated_line filename in
-  let types_module = (filename ^ "_embed_types") in
-  let types_module_seq = (filename ^ "_embed_types_sequential") in
-  let libs_seq = List.map (fun lib -> lib ^ "_sequential") libs in
+  let seq_suffix = if !opt_lem_sequential then "_sequential" else "" in
+  let types_module = (filename ^ "_embed_types" ^ seq_suffix) in
+  let monad_module = if !opt_lem_sequential then "State" else "Prompt" in
+  let operators_module = if !opt_lem_mwords then "Sail_operators_mwords" else "Sail_operators" in
+  let libs = List.map (fun lib -> lib ^ seq_suffix) libs in
+  let base_imports = [
+      "Pervasives_extra";
+      "Sail_impl_base";
+      "Sail_values";
+      operators_module;
+      monad_module
+    ] in
   let ((ot,_, _) as ext_ot) =
-    open_output_with_check_unformatted (filename ^ "_embed_types.lem") in
-  let ((ots,_, _) as ext_ots) =
-    open_output_with_check_unformatted (filename ^ "_embed_types_sequential.lem") in
+    open_output_with_check_unformatted (filename ^ "_embed_types" ^ seq_suffix ^ ".lem") in
   let ((o,_, _) as ext_o) =
-    open_output_with_check_unformatted (filename ^ "_embed.lem") in
-  let ((os,_, _) as ext_os) =
-    open_output_with_check_unformatted (filename ^ "_embed_sequential.lem") in
-  (Pretty_print.pp_defs_lem false false
-     (ot,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Sail_operators";"Prompt"])
-     (o,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Sail_operators";"Prompt";
-       String.capitalize types_module] @ libs)
-     defs generated_line);
-  (Pretty_print.pp_defs_lem true true
-     (ots,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Sail_operators_mwords";"State"])
-     (os,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Sail_operators_mwords";"State";
-       String.capitalize types_module_seq] @ libs_seq)
+    open_output_with_check_unformatted (filename ^ "_embed" ^ seq_suffix ^ ".lem") in
+  (Pretty_print.pp_defs_lem !opt_lem_sequential !opt_lem_mwords
+     (ot, base_imports)
+     (o, base_imports @ (String.capitalize types_module :: libs))
      defs generated_line);
   close_output_with_check ext_ot;
-  close_output_with_check ext_ots;
-  close_output_with_check ext_o;
-  close_output_with_check ext_os
+  close_output_with_check ext_o
 
 let output1 libpath out_arg filename defs  =
   let f' = Filename.basename (Filename.chop_extension filename) in
diff --git a/src/process_file.mli b/src/process_file.mli
index 5bcd9e03..c477d185 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -52,6 +52,8 @@ val load_file_no_check : Ast.order -> string -> unit Ast.defs
 val load_file : Ast.order -> Type_check.Env.t -> string -> Type_check.tannot Ast.defs * Type_check.Env.t
 
 val opt_new_parser : bool ref
+val opt_lem_sequential : bool ref
+val opt_lem_mwords : bool ref
 val opt_just_check : bool ref
 val opt_ddump_tc_ast : bool ref
 val opt_ddump_rewrite_ast : ((string * int) option) ref
@@ -74,4 +76,3 @@ val output :
     files existed before. If it is set to [false] and an output file already exists,
     the output file is only updated, if its content really changes. *)
 val always_replace_files : bool ref
-
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 79519af6..2b096609 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -1029,6 +1029,14 @@ let rewrite_trivial_sizeof, rewrite_trivial_sizeof_exp =
     | Nexp_neg nexp -> mk_exp (E_app (mk_id "negate_range", [split_nexp nexp]))
     | _ -> mk_exp (E_sizeof nexp)
   in
+  let rec rewrite_nexp_ids env (Nexp_aux (nexp, l) as nexp_aux) = match nexp with
+    | Nexp_id id -> rewrite_nexp_ids env (Env.get_num_def id env)
+    | Nexp_times (nexp1, nexp2) -> Nexp_aux (Nexp_times (rewrite_nexp_ids env nexp1, rewrite_nexp_ids env nexp2), l)
+    | Nexp_sum (nexp1, nexp2) -> Nexp_aux (Nexp_sum (rewrite_nexp_ids env nexp1, rewrite_nexp_ids env nexp2), l)
+    | Nexp_minus (nexp1, nexp2) -> Nexp_aux (Nexp_minus (rewrite_nexp_ids env nexp1, rewrite_nexp_ids env nexp2), l)
+    | Nexp_exp nexp -> Nexp_aux (Nexp_exp (rewrite_nexp_ids env nexp), l)
+    | Nexp_neg nexp -> Nexp_aux (Nexp_neg (rewrite_nexp_ids env nexp), l)
+    | _ -> nexp_aux in
   let rec rewrite_e_aux split_sizeof (E_aux (e_aux, (l, _)) as orig_exp) =
     let env = env_of orig_exp in
     match e_aux with
@@ -1036,17 +1044,21 @@ let rewrite_trivial_sizeof, rewrite_trivial_sizeof_exp =
        E_aux (E_lit (L_aux (L_num c, l)), (l, Some (env, atom_typ nexp, no_effect)))
     | E_sizeof nexp ->
        begin
-         let locals = Env.get_locals env in
-         let exps = Bindings.bindings locals
-                    |> List.map (extract_typ_var l env nexp)
-                    |> List.map (fun opt -> match opt with Some x -> [x] | None -> [])
-                    |> List.concat
-         in
-         match exps with
-         | (exp :: _) -> exp
-         | [] when split_sizeof ->
-            fold_exp (rewrite_e_sizeof false) (check_exp env (split_nexp nexp) (typ_of orig_exp))
-         | [] -> orig_exp
+         match simplify_nexp (rewrite_nexp_ids (env_of orig_exp) nexp) with
+         | Nexp_aux (Nexp_constant c, _) ->
+            E_aux (E_lit (L_aux (L_num c, l)), (l, Some (env, atom_typ nexp, no_effect)))
+         | _ ->
+            let locals = Env.get_locals env in
+            let exps = Bindings.bindings locals
+                       |> List.map (extract_typ_var l env nexp)
+                       |> List.map (fun opt -> match opt with Some x -> [x] | None -> [])
+                       |> List.concat
+            in
+            match exps with
+            | (exp :: _) -> exp
+            | [] when split_sizeof ->
+               fold_exp (rewrite_e_sizeof false) (check_exp env (split_nexp nexp) (typ_of orig_exp))
+            | [] -> orig_exp
        end
     | _ -> orig_exp
   and rewrite_e_sizeof split_sizeof =
@@ -1274,7 +1286,7 @@ let rewrite_sizeof (Defs defs) =
     let funcls = List.map rewrite_funcl_params funcls in
     (nvars, FD_aux (FD_function (rec_opt,tannot,eff,funcls),annot)) in
 
-  let rewrite_sizeof_fundef (params_map, defs) = function
+  let rewrite_sizeof_def (params_map, defs) = function
     | DEF_fundef fd as def ->
        let (nvars, fd') = rewrite_sizeof_fun params_map fd in
        let id = id_of_fundef fd in
@@ -1282,6 +1294,17 @@ let rewrite_sizeof (Defs defs) =
          if KidSet.is_empty nvars then params_map
          else Bindings.add id nvars params_map in
        (params_map', defs @ [DEF_fundef fd'])
+    | DEF_val (LB_aux (lb, annot)) ->
+       begin
+         let lb' = match lb with
+         | LB_val_explicit (typschm, pat, exp) ->
+           let exp' = fst (fold_exp { copy_exp_alg with e_aux = e_app_aux params_map } exp) in
+           LB_val_explicit (typschm, pat, exp')
+         | LB_val_implicit (pat, exp) ->
+           let exp' = fst (fold_exp { copy_exp_alg with e_aux = e_app_aux params_map } exp) in
+           LB_val_implicit (pat, exp') in
+         (params_map, defs @ [DEF_val (LB_aux (lb', annot))])
+       end
     | def ->
        (params_map, defs @ [def]) in
 
@@ -1314,7 +1337,7 @@ let rewrite_sizeof (Defs defs) =
        DEF_spec (VS_aux (VS_cast_spec (rewrite_typschm typschm id, id), a))
     | _ -> def in
 
-  let (params_map, defs) = List.fold_left rewrite_sizeof_fundef
+  let (params_map, defs) = List.fold_left rewrite_sizeof_def
                                           (Bindings.empty, []) defs in
   let defs = List.map (rewrite_sizeof_valspec params_map) defs in
   Defs defs
@@ -1941,7 +1964,12 @@ let remove_bitvector_pat pat =
     (letexp, letbind) in
 
   let compose_guards guards =
-    List.fold_right (Util.option_binop bitwise_and_exp) guards None in
+    let conj g1 g2 = match g1, g2 with
+      | Some g1, Some g2 -> Some (bitwise_and_exp g1 g2)
+      | Some g1, None -> Some g1
+      | None, Some g2 -> Some g2
+      | None, None -> None in
+    List.fold_right conj guards None in
 
   let flatten_guards_decls gd =
     let (guards,decls,letbinds) = Util.split3 gd in
@@ -2152,7 +2180,7 @@ let rewrite_defs_guarded_pats =
 
 
 let id_is_local_var id env = match Env.lookup_id id env with
-  | Local _ | Unbound -> true
+  | Local _ -> true
   | _ -> false
 
 let rec lexp_is_local (LEXP_aux (lexp, _)) env = match lexp with
@@ -2164,6 +2192,19 @@ let rec lexp_is_local (LEXP_aux (lexp, _)) env = match lexp with
   | LEXP_vector_range (lexp,_,_)
   | LEXP_field (lexp,_) -> lexp_is_local lexp env
 
+let id_is_unbound id env = match Env.lookup_id id env with
+  | Unbound -> true
+  | _ -> false
+
+let rec lexp_is_local_intro (LEXP_aux (lexp, _)) env = match lexp with
+  | LEXP_memory _ -> false
+  | LEXP_id id
+  | LEXP_cast (_, id) -> id_is_unbound id env
+  | LEXP_tup lexps -> List.for_all (fun lexp -> lexp_is_local_intro lexp env) lexps
+  | LEXP_vector (lexp,_)
+  | LEXP_vector_range (lexp,_,_)
+  | LEXP_field (lexp,_) -> lexp_is_local_intro lexp env
+
 let lexp_is_effectful (LEXP_aux (_, (_, annot))) = match annot with
   | Some (_, _, eff) -> effectful_effs eff
   | _ -> false
@@ -2171,6 +2212,13 @@ let lexp_is_effectful (LEXP_aux (_, (_, annot))) = match annot with
 let rec rewrite_local_lexp ((LEXP_aux(lexp,((l,_) as annot))) as le) = match lexp with
   | LEXP_id id | LEXP_cast (_, id) ->
     (le, E_aux (E_id id, annot), (fun exp -> exp))
+  | LEXP_tup les ->
+    let get_id (LEXP_aux(lexp,((l,_) as annot)) as le) = match lexp with
+      | LEXP_id id | LEXP_cast (_, id) -> E_aux (E_id id, annot)
+      | _ ->
+        raise (Reporting_basic.err_unreachable l
+          ("Unsupported sub-lexp " ^ string_of_lexp le ^ " in tuple")) in
+    (le, E_aux (E_tuple (List.map get_id les), annot), (fun exp -> exp))
   | LEXP_vector (lexp, e) ->
     let (lexp, access, rexp) = rewrite_local_lexp lexp in
     (lexp, E_aux (E_vector_access (access, e), annot),
@@ -2184,7 +2232,7 @@ let rec rewrite_local_lexp ((LEXP_aux(lexp,((l,_) as annot))) as le) = match lex
     let field_update exp = FES_aux (FES_Fexps ([FE_aux (FE_Fexp (id, exp), annot)], false), annot) in
     (lexp, E_aux (E_field (access, id), annot),
     (fun exp -> rexp (E_aux (E_record_update (access, field_update exp), annot))))
-  | _ -> raise (Reporting_basic.err_unreachable l "unsupported lexp")
+  | _ -> raise (Reporting_basic.err_unreachable l ("Unsupported lexp: " ^ string_of_lexp le))
 
 (*Expects to be called after rewrite_defs; thus the following should not appear:
   internal_exp of any form
@@ -2201,7 +2249,7 @@ let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as f
     let rec walker exps = match exps with
       | [] -> []
       | (E_aux(E_assign(le,e), ((l, Some (env,typ,eff)) as annot)) as exp)::exps
-        when lexp_is_local le env && not (lexp_is_effectful le)->
+        when lexp_is_local_intro le env && not (lexp_is_effectful le) ->
         let (le', _, re') = rewrite_local_lexp le in
         let e' = re' (rewrite_base e) in
         let exps' = walker exps in
@@ -2254,7 +2302,7 @@ let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as f
     in
     rewrap (E_block (walker exps))
   | E_assign(le,e)
-    when lexp_is_local le (env_of full_exp) && not (lexp_is_effectful le) ->
+    when lexp_is_local_intro le (env_of full_exp) && not (lexp_is_effectful le) ->
     let (le', _, re') = rewrite_local_lexp le in
     let e' = re' (rewrite_base e) in
     let block = E_aux (E_block [], simple_annot l unit_typ) in
@@ -2339,12 +2387,11 @@ let rewrite_defs_early_return =
   | _ -> exp in
 
   let e_block es =
-    (* let rec walker = function
-    | e :: es -> if is_return e then [e] else e :: walker es
-    | [] -> [] in
-    let es = walker es in *)
     match es with
     | [E_aux (e, _)] -> e
+    | _ :: _ when is_return (Util.last es) ->
+       let (E_aux (_, annot) as e) = Util.last es in
+       E_return (E_aux (E_block (Util.butlast es @ [get_return e]), annot))
     | _ -> E_block es in
 
   let e_if (e1, e2, e3) =
@@ -2372,14 +2419,19 @@ let rewrite_defs_early_return =
     | _ -> full_exp in
 
   let rewrite_funcl_early_return _ (FCL_aux (FCL_Funcl (id, pat, exp), a)) =
-    let exp = fold_exp
-      { id_exp_alg with e_block = e_block; e_if = e_if; e_case = e_case;
-        e_aux = e_aux } exp in
+    let exp =
+      exp
+      (* Pull early returns out as far as possible *)
+      |> fold_exp { id_exp_alg with e_block = e_block; e_if = e_if; e_case = e_case }
+      (* Remove singleton E_return *)
+      |> get_return
+      (* Fix effect annotations *)
+      |> fold_exp { id_exp_alg with e_aux = e_aux } in
     let a = match a with
     | (l, Some (env, typ, eff)) ->
       (l, Some (env, typ, union_effects eff (effect_of exp)))
     | _ -> a in
-    FCL_aux (FCL_Funcl (id, pat, get_return exp), a) in
+    FCL_aux (FCL_Funcl (id, pat, exp), a) in
 
   let rewrite_fun_early_return rewriters
     (FD_aux (FD_function (rec_opt, tannot_opt, effect_opt, funcls), a)) =
@@ -2441,7 +2493,7 @@ let rewrite_overload_cast (Defs defs) =
   let remove_cast_vs (VS_aux (vs_aux, annot)) =
     match vs_aux with
     | VS_val_spec (typschm, id) -> VS_aux (VS_val_spec (typschm, id), annot)
-    | VS_extern_no_rename (typschm, id) -> VS_aux (VS_val_spec (typschm, id), annot)
+    | VS_extern_no_rename (typschm, id) -> VS_aux (VS_extern_no_rename (typschm, id), annot)
     | VS_extern_spec (typschm, id, e) -> VS_aux (VS_extern_spec (typschm, id, e), annot)
     | VS_cast_spec (typschm, id) -> VS_aux (VS_val_spec (typschm, id), annot)
   in
@@ -2463,6 +2515,11 @@ let rewrite_undefined =
        mk_exp (E_app (prepend_id "undefined_" id, [mk_lit_exp L_unit]))
     | Typ_app (id, args) ->
        mk_exp (E_app (prepend_id "undefined_" id, List.concat (List.map undefined_of_typ_args args)))
+    | Typ_var kid ->
+       (* FIXME: bit of a hack, need to add a restriction to how
+          polymorphic undefined can be in the type checker to
+          guarantee this always works. *)
+       mk_exp (E_id (prepend_id "typ_" (id_of_kid kid)))
     | Typ_fn _ -> assert false
   and undefined_of_typ_args (Typ_arg_aux (typ_arg_aux, _) as typ_arg) =
     match typ_arg_aux with
@@ -2473,7 +2530,6 @@ let rewrite_undefined =
   let rewrite_e_aux (E_aux (e_aux, _) as exp) =
     match e_aux with
     | E_lit (L_aux (L_undef, l)) ->
-       print_endline ("Undefined: " ^ string_of_typ (typ_of exp));
        check_exp (env_of exp) (undefined_of_typ (typ_of exp)) (typ_of exp)
     | _ -> exp
   in
@@ -2501,10 +2557,15 @@ let rewrite_simple_types (Defs defs) =
        Typ_id (mk_id "int")
     | Typ_app (id, [_; _]) when Id.compare id (mk_id "range") = 0 ->
        Typ_id (mk_id "int")
+    | Typ_app (id, args) -> Typ_app (id, List.concat (List.map simple_typ_arg args))
     | Typ_fn (typ1, typ2, effs) -> Typ_fn (simple_typ typ1, simple_typ typ2, effs)
     | Typ_tup typs -> Typ_tup (List.map simple_typ typs)
     | Typ_exist (_, _, Typ_aux (typ, l)) -> simple_typ_aux typ
     | typ_aux -> typ_aux
+  and simple_typ_arg (Typ_arg_aux (typ_arg_aux, l)) =
+    match typ_arg_aux with
+    | Typ_arg_typ typ -> [Typ_arg_aux (Typ_arg_typ (simple_typ typ), l)]
+    | _ -> []
   in
   let simple_typschm (TypSchm_aux (TypSchm_ts (typq, typ), annot)) =
     TypSchm_aux (TypSchm_ts (simple_typquant typq, simple_typ typ), annot)
@@ -2512,7 +2573,7 @@ let rewrite_simple_types (Defs defs) =
   let simple_vs (VS_aux (vs_aux, annot)) =
     match vs_aux with
     | VS_val_spec (typschm, id) -> VS_aux (VS_val_spec (simple_typschm typschm, id), annot)
-    | VS_extern_no_rename (typschm, id) -> VS_aux (VS_val_spec (simple_typschm typschm, id), annot)
+    | VS_extern_no_rename (typschm, id) -> VS_aux (VS_extern_no_rename (simple_typschm typschm, id), annot)
     | VS_extern_spec (typschm, id, e) -> VS_aux (VS_extern_spec (simple_typschm typschm, id, e), annot)
     | VS_cast_spec (typschm, id) -> VS_aux (VS_cast_spec (simple_typschm typschm, id), annot)
   in
@@ -2549,6 +2610,43 @@ let rewrite_simple_types (Defs defs) =
   let defs = Defs (List.map simple_def defs) in
   rewrite_defs_base simple_defs defs
 
+let rewrite_tuple_assignments defs =
+  let assign_tuple e_aux annot =
+    let env = env_of_annot annot in
+    match e_aux with
+    | E_assign (LEXP_aux (LEXP_tup lexps, _), exp) ->
+       let (_, ids) = List.fold_left (fun (n, ids) _ -> (n + 1, ids @ [mk_id ("tup__" ^ string_of_int n)])) (0, []) lexps in
+       let block_assign i lexp = mk_exp (E_assign (strip_lexp lexp, mk_exp (E_id (mk_id ("tup__" ^ string_of_int i))))) in
+       let block = mk_exp (E_block (List.mapi block_assign lexps)) in
+       let letbind = mk_letbind (mk_pat (P_tup (List.map (fun id -> mk_pat (P_id id)) ids))) (strip_exp exp) in
+       let let_exp = mk_exp (E_let (letbind, block)) in
+       check_exp env let_exp unit_typ
+    | _ -> E_aux (e_aux, annot)
+  in
+  let assign_exp = {
+      id_exp_alg with
+      e_aux = (fun (e_aux, annot) -> assign_tuple e_aux annot)
+    } in
+  let assign_defs = { rewriters_base with rewrite_exp = (fun _ -> fold_exp assign_exp) } in
+  rewrite_defs_base assign_defs defs
+
+let rewrite_simple_assignments defs =
+  let assign_e_aux e_aux annot =
+    let env = env_of_annot annot in
+    match e_aux with
+    | E_assign (lexp, exp) ->
+       let (lexp, _, rhs) = rewrite_local_lexp lexp in
+       let assign = mk_exp (E_assign (strip_lexp lexp, strip_exp (rhs exp))) in
+       check_exp env assign unit_typ
+    | _ -> E_aux (e_aux, annot)
+  in
+  let assign_exp = {
+      id_exp_alg with
+      e_aux = (fun (e_aux, annot) -> assign_e_aux e_aux annot)
+    } in
+  let assign_defs = { rewriters_base with rewrite_exp = (fun _ -> fold_exp assign_exp) } in
+  rewrite_defs_base assign_defs defs
+
 let rewrite_defs_remove_blocks =
   let letbind_wild v body =
     let (E_aux (_,(l,tannot))) = v in
@@ -2814,7 +2912,8 @@ let rewrite_defs_letbind_effects  =
        rewrap (E_let (lb,n_exp body k)))
     | E_sizeof nexp ->
        k (rewrap (E_sizeof nexp))
-    | E_constraint nc -> failwith "E_constraint should have been removed till now"
+    | E_constraint nc ->
+       k (rewrap (E_constraint nc))
     | E_sizeof_internal annot ->
        k (rewrap (E_sizeof_internal annot))
     | E_assign (lexp,exp1) ->
@@ -2869,14 +2968,25 @@ let rewrite_defs_letbind_effects  =
 
 let rewrite_defs_effectful_let_expressions =
 
-  let e_let (lb,body) = 
+  let rec pat_of_local_lexp (LEXP_aux (lexp, ((l, _) as annot))) = match lexp with
+    | LEXP_id id -> P_aux (P_id id, annot)
+    | LEXP_cast (typ, id) -> P_aux (P_typ (typ, P_aux (P_id id, annot)), annot)
+    | LEXP_tup lexps -> P_aux (P_tup (List.map pat_of_local_lexp lexps), annot)
+    | _ -> raise (Reporting_basic.err_unreachable l "unexpected local lexp") in
+
+  let e_let (lb,body) =
     match lb with
+    | LB_aux (LB_val_implicit (P_aux (P_wild, _), E_aux (E_assign ((LEXP_aux (_, annot) as le), exp), _)), _)
+      when lexp_is_local le (env_of_annot annot) ->
+      (* Rewrite assignments to local variables into let bindings *)
+      let (lhs, _, rhs) = rewrite_local_lexp le in
+      E_let (LB_aux (LB_val_implicit (pat_of_local_lexp lhs, rhs exp), annot), body)
     | LB_aux (LB_val_explicit (_,pat,exp'),annot')
     | LB_aux (LB_val_implicit (pat,exp'),annot') ->
        if effectful exp'
        then E_internal_plet (pat,exp',body)
        else E_let (lb,body) in
-                             
+
   let e_internal_let = fun (lexp,exp1,exp2) ->
     match lexp with
     | LEXP_aux (LEXP_id id,annot)
@@ -2890,7 +3000,7 @@ let rewrite_defs_effectful_let_expressions =
 
   let alg = { id_exp_alg with e_let = e_let; e_internal_let = e_internal_let } in
   rewrite_defs_base
-    {rewrite_exp = (fun _ -> fold_exp alg)
+    { rewrite_exp = (fun _ -> fold_exp alg)
     ; rewrite_pat = rewrite_pat
     ; rewrite_let = rewrite_let
     ; rewrite_lexp = rewrite_lexp
@@ -2912,13 +3022,25 @@ let eqidtyp (id1,_) (id2,_) =
   let name2 = match id2 with Id_aux ((Id name | DeIid name),_) -> name in
   name1 = name2
 
+let find_introduced_vars exp =
+  let lEXP_aux ((ids,lexp),annot) =
+    let ids = match lexp, annot with
+    | LEXP_id id, (_, Some (env, _, _))
+    | LEXP_cast (_, id), (_, Some (env, _, _))
+      when id_is_unbound id env -> IdSet.add id ids
+    | _ -> ids in
+    (ids, LEXP_aux (lexp, annot)) in
+  fst (fold_exp
+    { (compute_exp_alg IdSet.empty IdSet.union) with lEXP_aux = lEXP_aux } exp)
+
 let find_updated_vars exp =
+  let intros = find_introduced_vars exp in
   let lEXP_aux ((ids,lexp),annot) =
     let ids = match lexp, annot with
-    | LEXP_id id, (_, Some (env, _, _)) ->
-      (match Env.lookup_id id env with
-      | Local (Mutable, _) -> (id, annot) :: ids
-      | _ -> ids)
+    | LEXP_id id, (_, Some (env, _, _))
+    | LEXP_cast (_, id), (_, Some (env, _, _))
+      when id_is_local_var id env && not (IdSet.mem id intros) ->
+      (id, annot) :: ids
     | _ -> ids in
     (ids, LEXP_aux (lexp, annot)) in
   dedup eqidtyp (fst (fold_exp
@@ -3170,7 +3292,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
      "tail-position": check the definition nexp_term and where it is used. *)
   | _ -> exp
 
-let replace_memwrite_e_assign exp = 
+let replace_memwrite_e_assign exp =
   let e_aux = fun (expaux,annot) ->
     match expaux with
     | E_assign (LEXP_aux (LEXP_memory (id,args),_),v) -> E_aux (E_app (id,args @ [v]),annot)
@@ -3278,7 +3400,7 @@ let rewrite_defs_remove_superfluous_returns =
 
   let alg = { id_exp_alg with e_aux = e_aux } in
   rewrite_defs_base
-    {rewrite_exp = (fun _ -> fold_exp alg)
+    { rewrite_exp = (fun _ -> fold_exp alg)
     ; rewrite_pat = rewrite_pat
     ; rewrite_let = rewrite_let
     ; rewrite_lexp = rewrite_lexp
@@ -3304,7 +3426,8 @@ let rewrite_defs_remove_e_assign =
 let recheck_defs defs = fst (check initial_env defs)
 
 let rewrite_defs_lem =[
-  top_sort_defs;
+  (* top_sort_defs; *)
+  rewrite_trivial_sizeof;
   rewrite_sizeof;
   rewrite_defs_remove_vector_concat;
   rewrite_defs_remove_bitvector_pats;
@@ -3323,13 +3446,15 @@ let rewrite_defs_lem =[
 let rewrite_defs_ocaml = [
     (* top_sort_defs; *)
   rewrite_undefined;
+  rewrite_tuple_assignments;
+  rewrite_simple_assignments;
   rewrite_defs_remove_vector_concat;
   rewrite_constraint;
   rewrite_trivial_sizeof;
-  (* rewrite_sizeof; *)
-  (* rewrite_simple_types; *)
-  (* rewrite_overload_cast; *)
-  (* rewrite_defs_exp_lift_assign; *)
+  rewrite_sizeof;
+  rewrite_simple_types;
+  rewrite_overload_cast;
+  rewrite_defs_exp_lift_assign;
   (* rewrite_defs_exp_lift_assign *)
   (* rewrite_defs_separate_numbs *)
   ]
diff --git a/src/sail.ml b/src/sail.ml
index 2f1e5c4a..04e1a6fd 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -73,6 +73,12 @@ let options = Arg.align ([
   ( "-ocaml_lib",
     Arg.String (fun l -> opt_libs_ocaml := l::!opt_libs_ocaml),
     "<filename> provide additional library to open in OCaml output");
+  ( "-lem_sequential",
+    Arg.Set Process_file.opt_lem_sequential,
+    " use sequential state monad for Lem output");
+  ( "-lem_mwords",
+    Arg.Set Process_file.opt_lem_mwords,
+    " use native machine word library for Lem output");
 (*
   ( "-i",
     Arg.String (fun l -> lib := l::!lib),
@@ -160,11 +166,10 @@ let main() =
        then output "" Lem_ast_out [out_name,ast]
        else ());
       (if !(opt_print_ocaml)
-       then let ast_ocaml = rewrite_ast_ocaml ast in
-         Pretty_print_sail.pp_defs stdout ast_ocaml;
-         if !(opt_libs_ocaml) = []
-         then output "" (Ocaml_out None) [out_name,ast_ocaml]
-         else output "" (Ocaml_out (Some (List.hd !opt_libs_ocaml))) [out_name,ast_ocaml]
+       then
+         let ast_ocaml = rewrite_ast_ocaml ast in
+         let out = match !opt_file_out with None -> "out" | Some s -> s in
+         Ocaml_backend.ocaml_compile out ast_ocaml
        else ());
       (if !(opt_print_lem)
        then let ast_lem = rewrite_ast_lem ast in
diff --git a/src/type_check.ml b/src/type_check.ml
index a3c4f767..4eb0688b 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -91,74 +91,6 @@ let orig_kid (Kid_aux (Var v, l) as kid) =
   with
   | Not_found -> kid
 
-let mk_typ typ = Typ_aux (typ, Parse_ast.Unknown)
-let mk_typ_arg arg = Typ_arg_aux (arg, Parse_ast.Unknown)
-let mk_id str = Id_aux (Id str, Parse_ast.Unknown)
-let mk_kid str = Kid_aux (Var ("'" ^ str), Parse_ast.Unknown)
-let mk_infix_id str = Id_aux (DeIid str, Parse_ast.Unknown)
-
-let mk_id_typ id = Typ_aux (Typ_id id, Parse_ast.Unknown)
-
-let mk_ord ord_aux = Ord_aux (ord_aux, Parse_ast.Unknown)
-
-let rec nexp_simp (Nexp_aux (nexp, l)) = Nexp_aux (nexp_simp_aux nexp, l)
-and nexp_simp_aux = function
-  | Nexp_minus (Nexp_aux (Nexp_sum (Nexp_aux (n1, _), Nexp_aux (Nexp_constant c1, _)), _), Nexp_aux (Nexp_constant c2, _)) when c1 = c2 ->
-     nexp_simp_aux n1
-  | Nexp_sum (Nexp_aux (Nexp_minus (Nexp_aux (n1, _), Nexp_aux (Nexp_constant c1, _)), _), Nexp_aux (Nexp_constant c2, _)) when c1 = c2 ->
-     nexp_simp_aux n1
-  | Nexp_sum (n1, n2) ->
-     begin
-       let (Nexp_aux (n1_simp, _) as n1) = nexp_simp n1 in
-       let (Nexp_aux (n2_simp, _) as n2) = nexp_simp n2 in
-       match n1_simp, n2_simp with
-       | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (c1 + c2)
-       | _, Nexp_neg n2 -> Nexp_minus (n1, n2)
-       | _, _ -> Nexp_sum (n1, n2)
-     end
-  | Nexp_times (n1, n2) ->
-     begin
-       let (Nexp_aux (n1_simp, _) as n1) = nexp_simp n1 in
-       let (Nexp_aux (n2_simp, _) as n2) = nexp_simp n2 in
-       match n1_simp, n2_simp with
-       | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (c1 * c2)
-       | _, _ -> Nexp_times (n1, n2)
-     end
-  | Nexp_minus (n1, n2) ->
-     begin
-       let (Nexp_aux (n1_simp, _) as n1) = nexp_simp n1 in
-       let (Nexp_aux (n2_simp, _) as n2) = nexp_simp n2 in
-       typ_debug ("SIMP: " ^ string_of_nexp n1 ^ " - " ^ string_of_nexp n2);
-       match n1_simp, n2_simp with
-       | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (c1 - c2)
-       | _, _ -> Nexp_minus (n1, n2)
-     end
-  | nexp -> nexp
-
-let int_typ = mk_id_typ (mk_id "int")
-let nat_typ = mk_id_typ (mk_id "nat")
-let unit_typ = mk_id_typ (mk_id "unit")
-let bit_typ = mk_id_typ (mk_id "bit")
-let real_typ = mk_id_typ (mk_id "real")
-let app_typ id args = mk_typ (Typ_app (id, args))
-let atom_typ nexp =
-  mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (Typ_arg_nexp (nexp_simp nexp))]))
-let range_typ nexp1 nexp2 =
-  mk_typ (Typ_app (mk_id "range", [mk_typ_arg (Typ_arg_nexp (nexp_simp nexp1));
-                                   mk_typ_arg (Typ_arg_nexp (nexp_simp nexp2))]))
-let bool_typ = mk_id_typ (mk_id "bool")
-let string_typ = mk_id_typ (mk_id "string")
-let list_typ typ = mk_typ (Typ_app (mk_id "list", [mk_typ_arg (Typ_arg_typ typ)]))
-
-let vector_typ n m ord typ =
-  mk_typ (Typ_app (mk_id "vector",
-                   [mk_typ_arg (Typ_arg_nexp (nexp_simp n));
-                    mk_typ_arg (Typ_arg_nexp (nexp_simp m));
-                    mk_typ_arg (Typ_arg_order ord);
-                    mk_typ_arg (Typ_arg_typ typ)]))
-
-let exc_typ = mk_id_typ (mk_id "exception")
-
 let is_range (Typ_aux (typ_aux, _)) =
   match typ_aux with
   | Typ_app (f, [Typ_arg_aux (Typ_arg_nexp n, _)])
@@ -173,25 +105,6 @@ let is_list (Typ_aux (typ_aux, _)) =
        when string_of_id f = "list" -> Some typ
   | _ -> None
 
-let nconstant c = Nexp_aux (Nexp_constant c, Parse_ast.Unknown)
-let nminus n1 n2 = Nexp_aux (Nexp_minus (n1, n2), Parse_ast.Unknown)
-let nsum n1 n2 = Nexp_aux (Nexp_sum (n1, n2), Parse_ast.Unknown)
-let ntimes n1 n2 = Nexp_aux (Nexp_times (n1, n2), Parse_ast.Unknown)
-let npow2 n = Nexp_aux (Nexp_exp n, Parse_ast.Unknown)
-let nvar kid = Nexp_aux (Nexp_var kid, Parse_ast.Unknown)
-let nid id = Nexp_aux (Nexp_id id, Parse_ast.Unknown)
-
-let nc_eq n1 n2 = mk_nc (NC_fixed (n1, n2))
-let nc_neq n1 n2 = mk_nc (NC_not_equal (n1, n2))
-let nc_lteq n1 n2 = NC_aux (NC_bounded_le (n1, n2), Parse_ast.Unknown)
-let nc_gteq n1 n2 = NC_aux (NC_bounded_ge (n1, n2), Parse_ast.Unknown)
-let nc_lt n1 n2 = nc_lteq n1 (nsum n2 (nconstant 1))
-let nc_gt n1 n2 = nc_gteq n1 (nsum n2 (nconstant 1))
-let nc_and nc1 nc2 = mk_nc (NC_and (nc1, nc2))
-let nc_or nc1 nc2 = mk_nc (NC_or (nc1, nc2))
-let nc_true = mk_nc NC_true
-let nc_false = mk_nc NC_false
-
 let mk_lit l = E_aux (E_lit (L_aux (l, Parse_ast.Unknown)), (Parse_ast.Unknown, ()))
 
 let rec nc_negate (NC_aux (nc, _)) =
@@ -211,10 +124,6 @@ let rec nc_negate (NC_aux (nc, _)) =
 
 (* Utilities for constructing effect sets *)
 
-let mk_effect effs =
-  Effect_aux (Effect_set (List.map (fun be_aux -> BE_aux (be_aux, Parse_ast.Unknown)) effs), Parse_ast.Unknown)
-
-let no_effect = mk_effect []
 
 module BESet = Set.Make(BE)
 
@@ -246,10 +155,6 @@ let string_of_index_sort = function
      ^ string_of_list " & " (fun (x, y) -> string_of_nexp x ^ " <= " ^ string_of_nexp y) constraints
      ^ "}"
 
-let quant_items : typquant -> quant_item list = function
-  | TypQ_aux (TypQ_tq qis, _) -> qis
-  | TypQ_aux (TypQ_no_forall, _) -> []
-
 let quant_split typq =
   let qi_kopt = function
     | QI_aux (QI_id kopt, _) -> [kopt]
@@ -262,23 +167,6 @@ let quant_split typq =
   let qis = quant_items typq in
   List.concat (List.map qi_kopt qis), List.concat (List.map qi_nc qis)
 
-let kopt_kid (KOpt_aux (kopt_aux, _)) =
-  match kopt_aux with
-  | KOpt_none kid | KOpt_kind (_, kid) -> kid
-
-let is_nat_kopt = function
-  | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_nat, _)], _), _), _) -> true
-  | KOpt_aux (KOpt_none _, _) -> true
-  | _ -> false
-
-let is_order_kopt = function
-  | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_order, _)], _), _), _) -> true
-  | _ -> false
-
-let is_typ_kopt = function
-  | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_type, _)], _), _), _) -> true
-  | _ -> false
-
 (**************************************************************************)
 (* 1. Substitutions                                                       *)
 (**************************************************************************)
@@ -768,6 +656,7 @@ end = struct
          end
 
   let add_register id typ env =
+    wf_typ env typ;
     if Bindings.mem id env.registers
     then typ_error (id_loc id) ("Register " ^ string_of_id id ^ " is already bound")
     else
@@ -1686,13 +1575,31 @@ let pat_typ_of (P_aux (_, (l, tannot))) = typ_of_annot (l, tannot)
 
 (* Flow typing *)
 
+let rec big_int_of_nexp (Nexp_aux (nexp, _)) = match nexp with
+  | Nexp_constant c -> Some (big_int_of_int c)
+  | Nexp_times (n1, n2) ->
+     Util.option_binop add_big_int (big_int_of_nexp n1) (big_int_of_nexp n2)
+  | Nexp_sum (n1, n2) ->
+     Util.option_binop add_big_int (big_int_of_nexp n1) (big_int_of_nexp n2)
+  | Nexp_minus (n1, n2) ->
+     Util.option_binop add_big_int (big_int_of_nexp n1) (big_int_of_nexp n2)
+  | Nexp_exp n ->
+     Util.option_map (power_int_positive_big_int 2) (big_int_of_nexp n)
+  | _ -> None
+
 let destruct_atom (Typ_aux (typ_aux, _)) =
   match typ_aux with
-  | Typ_app (f, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_constant c, _)), _)])
-       when string_of_id f = "atom" -> c
-  | Typ_app (f, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_constant c1, _)), _); Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_constant c2, _)), _)])
-       when string_of_id f = "range" && c1 = c2 -> c1
-  | _ -> assert false
+  | Typ_app (f, [Typ_arg_aux (Typ_arg_nexp nexp, _)])
+       when string_of_id f = "atom" ->
+     Util.option_map (fun c -> (c, nexp)) (big_int_of_nexp nexp)
+  | Typ_app (f, [Typ_arg_aux (Typ_arg_nexp nexp1, _); Typ_arg_aux (Typ_arg_nexp nexp2, _)])
+       when string_of_id f = "range" ->
+     begin
+       match big_int_of_nexp nexp1, big_int_of_nexp nexp2 with
+       | Some c1, Some c2 -> if eq_big_int c1 c2 then Some (c1, nexp1) else None
+       | _ -> None
+     end
+  | _ -> None
 
 let destruct_atom_nexp env typ =
   match Env.expand_synonyms env typ with
@@ -1702,20 +1609,6 @@ let destruct_atom_nexp env typ =
        when string_of_id f = "range" -> Some n
   | _ -> None
 
-let restrict_range_upper c1 (Typ_aux (typ_aux, l) as typ) =
-  match typ_aux with
-  | Typ_app (f, [Typ_arg_aux (Typ_arg_nexp nexp, _); Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_constant c2, _)), _)])
-     when string_of_id f = "range" ->
-     range_typ nexp (nconstant (min c1 c2))
-  | _ -> typ
-
-let restrict_range_lower c1 (Typ_aux (typ_aux, l) as typ) =
-  match typ_aux with
-  | Typ_app (f, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_constant c2, _)), _); Typ_arg_aux (Typ_arg_nexp nexp, _)])
-     when string_of_id f = "range" ->
-     range_typ (nconstant (max c1 c2)) nexp
-  | _ -> typ
-
 exception Not_a_constraint;;
 
 let rec assert_nexp (E_aux (exp_aux, l)) =
@@ -1737,12 +1630,42 @@ let rec assert_constraint (E_aux (exp_aux, l)) =
   | _ -> nc_true
 
 type flow_constraint =
-  | Flow_lteq of int
-  | Flow_gteq of int
+  | Flow_lteq of big_int * nexp
+  | Flow_gteq of big_int * nexp
+
+let restrict_range_upper c1 nexp1 (Typ_aux (typ_aux, l) as typ) =
+  match typ_aux with
+  | Typ_app (f, [Typ_arg_aux (Typ_arg_nexp nexp, _); Typ_arg_aux (Typ_arg_nexp nexp2, _)])
+     when string_of_id f = "range" ->
+     begin
+       match big_int_of_nexp nexp2 with
+       | Some c2 ->
+          let upper = if (lt_big_int c1 c2) then nexp1 else nexp2 in
+          range_typ nexp upper
+       | _ -> typ
+     end
+  | _ -> typ
+
+let restrict_range_lower c1 nexp1 (Typ_aux (typ_aux, l) as typ) =
+  match typ_aux with
+  | Typ_app (f, [Typ_arg_aux (Typ_arg_nexp nexp2, _); Typ_arg_aux (Typ_arg_nexp nexp, _)])
+     when string_of_id f = "range" ->
+     begin
+       match big_int_of_nexp nexp2 with
+       | Some c2 ->
+          let lower = if (gt_big_int c1 c2) then nexp1 else nexp2 in
+          range_typ lower nexp
+       | _ -> typ
+     end
+  | _ -> typ
 
 let apply_flow_constraint = function
-  | Flow_lteq c -> (restrict_range_upper c, restrict_range_lower (c + 1))
-  | Flow_gteq c -> (restrict_range_lower c, restrict_range_upper (c - 1))
+  | Flow_lteq (c, nexp) ->
+     (restrict_range_upper c nexp,
+      restrict_range_lower (succ_big_int c) (nexp_simp (nsum nexp (nconstant 1))))
+  | Flow_gteq (c, nexp) ->
+     (restrict_range_lower c nexp,
+      restrict_range_upper (pred_big_int c) (nexp_simp (nminus nexp (nconstant 1))))
 
 let rec infer_flow env (E_aux (exp_aux, (l, _))) =
   match exp_aux with
@@ -1764,20 +1687,34 @@ let rec infer_flow env (E_aux (exp_aux, (l, _))) =
      [], [nc_gt n1 n2]
   | E_app (f, [E_aux (E_id v, _); y]) when string_of_id f = "lt_range_atom" ->
      let kid = Env.fresh_kid env in
-     let c = destruct_atom (typ_of y) in
-     [(v, Flow_lteq (c - 1))], []
+     begin
+       match destruct_atom (typ_of y) with
+       | Some (c, nexp) ->
+          [(v, Flow_lteq (pred_big_int c, nexp_simp (nminus nexp (nconstant 1))))], []
+       | _ -> [], []
+     end
   | E_app (f, [E_aux (E_id v, _); y]) when string_of_id f = "lteq_range_atom" ->
      let kid = Env.fresh_kid env in
-     let c = destruct_atom (typ_of y) in
-     [(v, Flow_lteq c)], []
+     begin
+       match destruct_atom (typ_of y) with
+       | Some (c, nexp) -> [(v, Flow_lteq (c, nexp))], []
+       | _ -> [], []
+     end
   | E_app (f, [E_aux (E_id v, _); y]) when string_of_id f = "gt_range_atom" ->
      let kid = Env.fresh_kid env in
-     let c = destruct_atom (typ_of y) in
-     [(v, Flow_gteq (c + 1))], []
+     begin
+       match destruct_atom (typ_of y) with
+       | Some (c, nexp) ->
+          [(v, Flow_gteq (succ_big_int c, nexp_simp (nsum nexp (nconstant 1))))], []
+       | _ -> [], []
+     end
   | E_app (f, [E_aux (E_id v, _); y]) when string_of_id f = "gteq_range_atom" ->
      let kid = Env.fresh_kid env in
-     let c = destruct_atom (typ_of y) in
-     [(v, Flow_gteq c)], []
+     begin
+       match destruct_atom (typ_of y) with
+       | Some (c, nexp) -> [(v, Flow_gteq (c, nexp))], []
+       | _ -> [], []
+     end
   | _ -> [], []
 
 let rec add_flows b flows env =
@@ -1857,6 +1794,7 @@ let irule r env exp =
 
 let strip_exp : 'a exp -> unit exp = function exp -> map_exp_annot (fun (l, _) -> (l, ())) exp
 let strip_pat : 'a pat -> unit pat = function pat -> map_pat_annot (fun (l, _) -> (l, ())) pat
+let strip_lexp : 'a lexp -> unit lexp = function lexp -> map_lexp_annot (fun (l, _) -> (l, ())) lexp
 
 let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ_aux, _) as typ) : tannot exp =
   let annot_exp_effect exp typ eff = E_aux (exp, (l, Some (env, typ, eff))) in
@@ -2599,6 +2537,8 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
      let else_branch' = crule check_exp (add_constraints (List.map nc_negate constrs) (add_flows false flows env)) else_branch (typ_of then_branch') in
      annot_exp (E_if (cond', then_branch', else_branch')) (typ_of then_branch')
   | E_vector_access (v, n) -> infer_exp env (E_aux (E_app (mk_id "vector_access", [v; n]), (l, ())))
+  | E_vector_update (v, n, exp) -> infer_exp env (E_aux (E_app (mk_id "vector_update", [v; n; exp]), (l, ())))
+  | E_vector_update_subrange (v, n, m, exp) -> infer_exp env (E_aux (E_app (mk_id "vector_update_subrange", [v; n; m; exp]), (l, ())))
   | E_vector_append (v1, v2) -> infer_exp env (E_aux (E_app (mk_id "append", [v1; v2]), (l, ())))
   | E_vector_subrange (v, n, m) -> infer_exp env (E_aux (E_app (mk_id "vector_subrange", [v; n; m]), (l, ())))
   | E_vector [] -> typ_error l "Cannot infer type of empty vector"
diff --git a/src/type_check.mli b/src/type_check.mli
index e3b9b81b..857e0019 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -103,6 +103,8 @@ module Env : sig
 
   val get_overloads : id -> t -> id list
 
+  val get_num_def : id -> t -> nexp
+
   val is_extern : id -> t -> bool
 
   val get_extern : id -> t -> string
@@ -151,73 +153,28 @@ val add_typquant : typquant -> Env.t -> Env.t
    not of this form. *)
 val orig_kid : kid -> kid
 
-(* Some handy utility functions for constructing types. *)
-val mk_typ : typ_aux -> typ
-val mk_typ_arg : typ_arg_aux -> typ_arg
-val mk_id : string -> id
-val mk_id_typ : id -> typ
-
-val no_effect : effect
-val mk_effect : base_effect_aux list -> effect
-
 val union_effects : effect -> effect -> effect
 val equal_effects : effect -> effect -> bool
 
-val nconstant : int -> nexp
-val nminus : nexp -> nexp -> nexp
-val nsum : nexp -> nexp -> nexp
-val ntimes : nexp -> nexp -> nexp
-val npow2 : nexp -> nexp
-val nvar : kid -> nexp
-val nid : id -> nexp (* NOTE: Nexp_id's don't do anything currently *)
-
-(* Numeric constraint builders *)
-val nc_eq : nexp -> nexp -> n_constraint
-val nc_neq : nexp -> nexp -> n_constraint
-val nc_lteq : nexp -> nexp -> n_constraint
-val nc_gteq : nexp -> nexp -> n_constraint
-val nc_lt : nexp -> nexp -> n_constraint
-val nc_gt : nexp -> nexp -> n_constraint
-val nc_and : n_constraint -> n_constraint -> n_constraint
-val nc_or : n_constraint -> n_constraint -> n_constraint
-val nc_true : n_constraint
-val nc_false : n_constraint
-
 (* Negate a n_constraint. Note that there's no NC_not constructor, so
    this flips all the inequalites a the n_constraint leaves and uses
    de-morgans to switch and to or and vice versa. *)
 val nc_negate : n_constraint -> n_constraint
 
-val is_nat_kopt : kinded_id -> bool
-val is_order_kopt : kinded_id -> bool
-val is_typ_kopt : kinded_id -> bool
-
-(* Sail builtin types. *)
-val int_typ : typ
-val nat_typ : typ
-val atom_typ : nexp -> typ
-val range_typ : nexp -> nexp -> typ
-val bit_typ : typ
-val bool_typ : typ
-val unit_typ : typ
-val string_typ : typ
-val real_typ : typ
-val vector_typ : nexp -> nexp -> order -> typ -> typ
-val list_typ : typ -> typ
-val exist_typ : (kid -> n_constraint) -> (kid -> typ) -> typ
-val exc_typ : typ
-
 (* Vector with default order. *)
 val dvector_typ : Env.t -> nexp -> nexp -> typ -> typ
 
 (* Vector of specific length with default order, i.e. lvector_typ env n bit_typ = bit[n]. *)
 val lvector_typ : Env.t -> nexp -> typ -> typ
 
+val exist_typ : (kid -> n_constraint) -> (kid -> typ) -> typ
+
 type tannot = (Env.t * typ * effect) option
 
 (* Strip the type annotations from an expression. *)
 val strip_exp : 'a exp -> unit exp
 val strip_pat : 'a pat -> unit pat
+val strip_lexp : 'a lexp -> unit lexp
 
 (* Check an expression has some type. Returns a fully annotated
    version of the expression, where each subexpression is annotated
diff --git a/src/util.ml b/src/util.ml
index 75732376..335fd36f 100644
--- a/src/util.ml
+++ b/src/util.ml
@@ -86,6 +86,15 @@
 (*  IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.                         *)
 (**************************************************************************)
 
+let rec last = function
+  | [x] -> x
+  | _ :: xs -> last xs
+  | [] -> raise (Failure "last")
+
+let rec butlast = function
+  | [x] -> []
+  | x :: xs -> x :: butlast xs
+  | [] -> []
 
 module Duplicate(S : Set.S) = struct
 
@@ -204,10 +213,8 @@ let option_bind f = function
   | Some(o) -> f o
 
 let rec option_binop f x y = match x, y with
-  | None, None -> None
-  | Some x, None -> Some x
-  | None, Some y -> Some y
   | Some x, Some y -> Some (f x y)
+  | _ -> None
 
 let changed2 f g x h y =
   match (g x, h y) with
diff --git a/src/util.mli b/src/util.mli
index aa442ada..11588de2 100644
--- a/src/util.mli
+++ b/src/util.mli
@@ -40,6 +40,11 @@
 (*  SUCH DAMAGE.                                                          *)
 (**************************************************************************)
 
+(* Last element of a list *)
+val last : 'a list -> 'a
+
+val butlast : 'a list -> 'a list
+
 (** Mixed useful things *)
 module Duplicate(S : Set.S) : sig 
   type dups = 
@@ -77,10 +82,8 @@ val option_bind : ('a -> 'b option) -> 'a option -> 'b option
     whereas [option_default d (Some x)] returns [x]. *)
 val option_default : 'a -> 'a option -> 'a
 
-(** [option_binop f None None] returns [None], while
-    [option_binop f (Some x) None] and [option_binop f None (Some x)]
-    return [Some x], and [option_binop f (Some x) (Some y)] returns
-    [Some (f x y)] *)
+(** [option_binop f (Some x) (Some y)] returns [Some (f x y)],
+    and in all other cases, [option_binop] returns [None]. *)
 val option_binop : ('a -> 'a -> 'a) -> 'a option -> 'a option -> 'a option
 
 (** [option_get_exn exn None] throws the exception [exn],
diff --git a/test/ocaml/hello_world/expect b/test/ocaml/hello_world/expect
new file mode 100644
index 00000000..3df47a31
--- /dev/null
+++ b/test/ocaml/hello_world/expect
@@ -0,0 +1,2 @@
+Hello, Sail!
+Hello, World!
diff --git a/test/ocaml/hello_world/hello_world.sail b/test/ocaml/hello_world/hello_world.sail
new file mode 100644
index 00000000..d96429f2
--- /dev/null
+++ b/test/ocaml/hello_world/hello_world.sail
@@ -0,0 +1,19 @@
+
+val unit -> string effect pure hello_world
+
+function hello_world () = {
+  return "Hello, World!";
+  "Unreachable"
+}
+
+val unit -> unit effect {wreg, rreg} main
+
+register string REG
+
+function main () = {
+  REG := "Hello, Sail!";
+  print(REG);
+  REG := hello_world ();
+  print(REG);
+  return ()
+}
diff --git a/test/ocaml/prelude.sail b/test/ocaml/prelude.sail
new file mode 100644
index 00000000..2526d109
--- /dev/null
+++ b/test/ocaml/prelude.sail
@@ -0,0 +1,138 @@
+
+default Order dec
+
+val extern (int, int) -> bool effect pure eq_int = "eq_int"
+val extern forall 'n. (bit['n], bit['n]) -> bool effect pure eq_vec = "eq_list"
+val extern (string, string) -> bool effect pure eq_string = "eq_string"
+val (real, real) -> bool effect pure eq_real
+
+val extern forall Type 'a. ('a, 'a) -> bool effect pure eq_anything = "(fun (x, y) -> x == y)"
+
+overload (deinfix ==) [eq_int; eq_vec; eq_string; eq_real; eq_anything]
+
+val extern forall Type 'a, Num 'n. vector<'n - 1, 'n, dec, 'a> -> [:'n:] effect pure length = "length"
+
+val extern forall Num 'n, Num 'm, Num 'o (* , 'm >= 'o, 'o >= 0, 'n >= 'm + 1 *).
+  (bit['n], [:'m:], [:'o:]) -> bit['m - ('o - 1)] effect pure vector_subrange = "subrange"
+
+val extern forall Num 'n, Type 'a. (vector<'n - 1, 'n, dec, 'a>, int) -> 'a effect pure vector_access = "access"
+
+val extern forall Num 'n, Type 'a. (vector<'n - 1, 'n, dec, 'a>, int, 'a) -> vector<'n - 1, 'n, dec, 'a> effect pure vector_update = "update"
+
+val extern forall Num 'n, Num 'm, Num 'o.
+  (bit['n], [:'m:], [:'o:], bit['m - ('o - 1)]) -> bit['n]
+  effect pure vector_update_subrange = "update_subrange"
+
+val forall Num 'n, Type 'a. ('a, vector<'n - 1, 'n, dec, 'a>) -> vector<'n, 'n + 1, dec, 'a> effect pure vcons
+
+val extern forall Num 'n, Num 'm, Type 'a. (vector<'n - 1, 'n, dec, 'a>, vector<'m - 1, 'm, dec, 'a>) -> vector<('n + 'm) - 1, 'n + 'm, dec, 'a> effect pure append = "append"
+
+val extern bool -> bool effect pure not_bool = "not"
+val extern forall 'n. bit['n] -> bit['n] effect pure not_vec = "not_vec"
+
+overload ~ [not_bool; not_vec]
+
+val forall Type 'a. ('a, 'a) -> bool effect pure neq_anything
+
+function neq_anything (x, y) = not_bool (x == y)
+
+overload (deinfix !=) [neq_anything]
+
+val extern (bool, bool) -> bool effect pure and_bool = "and_bool"
+val extern forall 'n. (bit['n], bit['n]) -> bit['n] effect pure and_vec = "and_vec"
+
+overload (deinfix &) [and_bool; and_vec]
+
+val extern (bool, bool) -> bool effect pure or_bool = "or_bool"
+val extern forall 'n. (bit['n], bit['n]) -> bit['n] effect pure or_vec = "or_vec"
+
+overload (deinfix |) [or_bool; or_vec]
+
+val extern forall 'n. bit['n] -> [|0:2**'n - 1|] effect pure UInt = "uint"
+
+val extern forall 'n. bit['n] -> [|- 2**('n - 1):2**('n - 1) - 1|] effect pure SInt = "sint"
+
+val extern string -> unit effect pure print = "print_endline"
+val extern (string, string) -> string effect pure concat_str = "concat_string"
+val int -> string effect pure DecStr
+val int -> string effect pure HexStr
+
+val forall 'n. (bit['n], bit['n]) -> bit['n] effect pure xor_vec
+val (int, int) -> int effect pure int_exp
+
+overload (deinfix ^) [xor_vec; int_exp]
+
+val extern forall 'n, 'm, 'o, 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range = "add"
+val extern (int, int) -> int effect pure add_int = "add"
+val extern forall 'n. (bit['n], bit['n]) -> bit['n] effect pure add_vec = "add_vec"
+val forall 'n. (bit['n], int) -> bit['n] effect pure add_vec_int
+
+overload (deinfix +) [add_range; add_int; add_vec; add_vec_int]
+
+val extern forall 'n, 'm, 'o, 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range = "sub"
+val extern (int, int) -> int effect pure sub_int = "sub"
+val forall 'n. (bit['n], bit['n]) -> bit['n] effect pure sub_vec
+val forall 'n. (bit['n], int) -> bit ['n] effect pure sub_vec_int
+
+val forall 'n. [|'n:'m|] -> [|-'m:-'n|] effect pure negate_range
+val int -> int effect pure negate_int
+
+overload (deinfix -) [sub_range; sub_int; sub_vec; sub_vec_int]
+overload negate [negate_range; negate_int]
+
+val extern forall 'n, 'm, 'o, 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n * 'o : 'm * 'p|] effect pure mult_range = "mult"
+val extern (int, int) -> int effect pure mult_int = "mult"
+
+overload (deinfix * ) [mult_range; mult_int]
+
+val (int, int) -> bool effect pure gteq_int
+val (real, real) -> bool effect pure gteq_real
+
+overload (deinfix >=) [gteq_int; gteq_real]
+
+val (int, int) -> bool effect pure lteq_int
+val (real, real) -> bool effect pure lteq_real
+
+overload (deinfix <=) [lteq_int; lteq_real]
+
+val (int, int) -> bool effect pure gt_int
+val (real, real) -> bool effect pure gt_real
+
+overload (deinfix >) [gt_int; gt_real]
+
+val (int, int) -> bool effect pure lt_int
+val (real, real) -> bool effect pure lt_real
+
+overload (deinfix <) [lt_int; lt_real]
+
+val real -> int effect pure RoundDown
+val real -> int effect pure RoundUp
+
+val extern (int, int) -> int effect pure quotient = "quotient"
+
+overload (deinfix quot) [quotient]
+
+val extern (int, int) -> int effect pure modulus = "modulus"
+
+overload (deinfix mod) [modulus]
+
+val extern (int, int) -> int effect pure shl_int
+val extern (int, int) -> int effect pure shr_int
+
+val (nat, nat) -> nat effect pure min_nat
+val (int, int) -> int effect pure min_int
+val (nat, nat) -> nat effect pure max_nat
+val (int, int) -> int effect pure max_int
+
+overload min [min_nat; min_int]
+overload max [max_nat; max_int]
+
+val extern forall 'n, 'm. ([:'m:], [:'n:], bit['m], bit['m], bit[8 * 'n]) -> unit effect {wmem} __WriteRAM = "write_ram"
+val extern forall 'n, 'm. ([:'m:], [:'n:], bit['m], bit['m]) -> bit[8 * 'n] effect {rmem} __ReadRAM = "read_ram"
+
+val extern forall 'n, 'm. (bit['n], [:'m:]) -> bit['n * 'm] effect pure replicate_bits
+
+val extern nat -> exist 'n, 'n >= 0. [:'n:] effect pure ex_nat = "identity"
+val extern int -> exist 'n. [:'n:] effect pure ex_int = "identity"
+val extern forall 'n, 'm. [|'n:'m|] -> exist 'o, 'n <= 'o & 'o <= 'm. [:'o:] effect pure ex_range = "identity"
+
diff --git a/test/ocaml/run_tests.sh b/test/ocaml/run_tests.sh
new file mode 100755
index 00000000..d01535b6
--- /dev/null
+++ b/test/ocaml/run_tests.sh
@@ -0,0 +1,69 @@
+#!/usr/bin/env bash
+set -e
+
+DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
+SAILDIR="$DIR/../.."
+
+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"
+    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
+}
+
+SAILLIBDIR="$DIR"
+
+printf "<testsuites>\n" >> $DIR/tests.xml
+
+for i in `ls -d */`;
+do
+    cd $DIR/$i;
+    if $SAILDIR/sail -o out -ocaml ../prelude.sail `ls *.sail`;
+    then
+	./out > result;
+	if diff expect result;
+	then
+	    green "built $i" "ok"
+	else
+	    yellow "bad output $i" "fail"
+	fi;
+	rm out;
+	rm result;
+	rm -r _sbuild
+    else
+	red "building $i" "fail"
+    fi
+done
+
+printf "</testsuites>\n" >> $DIR/tests.xml
diff --git a/test/ocaml/sail_lib.ml b/test/ocaml/sail_lib.ml
new file mode 100644
index 00000000..e287eadb
--- /dev/null
+++ b/test/ocaml/sail_lib.ml
@@ -0,0 +1,169 @@
+open Big_int
+
+type 'a return = { return : 'b . 'a -> 'b }
+
+let with_return (type t) (f : _ -> t) =
+  let module M =
+    struct exception Return of t end
+  in
+  let return = { return = (fun x -> raise (M.Return x)); } in
+  try f return with M.Return x -> x
+
+type bit = B0 | B1
+
+let and_bit = function
+  | B1, B1 -> B1
+  | _, _ -> B0
+
+let or_bit = function
+  | B0, B0 -> B0
+  | _, _ -> B1
+
+let and_vec (xs, ys) =
+  assert (List.length xs = List.length ys);
+  List.map2 (fun x y -> and_bit (x, y)) xs ys
+
+let and_bool (b1, b2) = b1 && b2
+
+let or_vec (xs, ys) =
+  assert (List.length xs = List.length ys);
+  List.map2 (fun x y -> or_bit (x, y)) xs ys
+
+let or_bool (b1, b2) = b1 || b2
+
+let undefined_bit () =
+  if Random.bool () then B0 else B1
+
+let undefined_bool () = Random.bool ()
+
+let rec undefined_vector (start_index, len, item) =
+  if eq_big_int len zero_big_int
+  then []
+  else item :: undefined_vector (start_index, sub_big_int len unit_big_int, item)
+
+let undefined_string () = ""
+
+let undefined_unit () = ()
+
+let undefined_int () =
+  big_int_of_int (Random.int 0xFFFF)
+
+let internal_pick list =
+  List.nth list (Random.int (List.length list))
+
+let eq_int (n, m) = eq_big_int n m
+
+let eq_string (str1, str2) = String.compare str1 str2 = 0
+
+let concat_string (str1, str2) = str1 ^ str2
+
+let rec drop n xs =
+  match n, xs with
+  | 0, xs -> xs
+  | n, [] -> []
+  | n, (x :: xs) -> drop (n -1) xs
+
+let rec take n xs =
+  match n, xs with
+  | 0, xs -> []
+  | n, (x :: xs) -> x :: take (n - 1) xs
+  | n, [] -> []
+
+let subrange (list, n, m) =
+  let n = int_of_big_int n in
+  let m = int_of_big_int m in
+  List.rev (take (n - (m - 1)) (drop m (List.rev list)))
+
+let eq_list (xs, ys) = List.for_all2 (fun x y -> x == y) xs ys
+
+let access (xs, n) = List.nth (List.rev xs) (int_of_big_int n)
+
+let append (xs, ys) = xs @ ys
+
+let update (xs, n, x) =
+  let n = int_of_big_int n in
+  take n xs @ [x] @ drop (n + 1) xs
+
+let update_subrange (xs, n, m, ys) =
+  let n = int_of_big_int n in
+  let m = int_of_big_int m in
+  assert false
+
+let length xs = big_int_of_int (List.length xs)
+
+let big_int_of_bit = function
+  | B0 -> zero_big_int
+  | B1 -> unit_big_int
+
+let uint xs =
+  let uint_bit x (n, pos) =
+    add_big_int n (mult_big_int (power_int_positive_int 2 pos) (big_int_of_bit x)), pos + 1
+  in
+  fst (List.fold_right uint_bit xs (zero_big_int, 0))
+
+let sint = function
+  | [] -> zero_big_int
+  | [msb] -> minus_big_int (big_int_of_bit msb)
+  | msb :: xs ->
+     let msb_pos = List.length xs in
+     let complement =
+       minus_big_int (mult_big_int (power_int_positive_int 2 msb_pos) (big_int_of_bit msb))
+     in
+     add_big_int complement (uint xs)
+
+let add (x, y) = add_big_int x y
+let sub (x, y) = sub_big_int x y
+let mult (x, y) = mult_big_int x y
+let quotient (x, y) = fst (quomod_big_int x y)
+let modulus (x, y) = snd (quomod_big_int x y)
+
+let add_bit_with_carry (x, y, carry) =
+  match x, y, carry with
+  | B0, B0, B0 -> B0, B0
+  | B0, B1, B0 -> B1, B0
+  | B1, B0, B0 -> B1, B0
+  | B1, B1, B0 -> B0, B1
+  | B0, B0, B1 -> B1, B0
+  | B0, B1, B1 -> B0, B1
+  | B1, B0, B1 -> B0, B1
+  | B1, B1, B1 -> B1, B1
+
+let not_bit = function
+  | B0 -> B1
+  | B1 -> B0
+
+let not_vec xs = List.map not_bit xs
+
+let add_vec_carry (xs, ys) =
+  assert (List.length xs = List.length ys);
+  let (carry, result) =
+    List.fold_right2 (fun x y (c, result) -> let (z, c) = add_bit_with_carry (x, y, c) in (c, z :: result)) xs ys (B0, [])
+  in
+  carry, result
+
+let add_vec (xs, ys) = snd (add_vec_carry (xs, ys))
+
+let rec replicate_bits (bits, n) =
+  if eq_big_int n zero_big_int
+  then []
+  else bits @ replicate_bits (bits, sub_big_int n unit_big_int)
+
+let identity x = x
+
+let get_slice_int (n, m, o) = assert false
+
+let hex_slice (str, n, m) = assert false
+
+let putchar n = print_endline (string_of_big_int n)
+
+let write_ram (addr_size, data_size, hex_ram, addr, data) =
+  assert false
+
+let read_ram (addr_size, data_size, hex_ram, addr) =
+  assert false
+
+(* FIXME: Casts can't be externed *)
+let zcast_unit_vec x = [x]
+
+let shl_int (n, m) = assert false
+let shr_int (n, m) = assert false
diff --git a/test/ocaml/string_equality/expect b/test/ocaml/string_equality/expect
new file mode 100644
index 00000000..27ba77dd
--- /dev/null
+++ b/test/ocaml/string_equality/expect
@@ -0,0 +1 @@
+true
diff --git a/test/ocaml/string_equality/string_equality.sail b/test/ocaml/string_equality/string_equality.sail
new file mode 100644
index 00000000..68629862
--- /dev/null
+++ b/test/ocaml/string_equality/string_equality.sail
@@ -0,0 +1,10 @@
+
+val unit -> unit effect pure main
+
+function main () = {
+  if ("test" == "test") then {
+    print("true")
+  } else {
+    print("false")
+  }
+}
diff --git a/test/typecheck/run_tests.sh b/test/typecheck/run_tests.sh
index 24f20d1f..eaa268a6 100755
--- a/test/typecheck/run_tests.sh
+++ b/test/typecheck/run_tests.sh
@@ -21,8 +21,8 @@ MIPS="$SAILDIR/mips_new_tc"
 cat $SAILDIR/lib/prelude.sail $SAILDIR/lib/prelude_wrappers.sail $MIPS/mips_prelude.sail > $DIR/pass/mips_prelude.sail
 cat $SAILDIR/lib/prelude.sail $SAILDIR/lib/prelude_wrappers.sail $MIPS/mips_prelude.sail $MIPS/mips_tlb.sail > $DIR/pass/mips_tlb.sail
 cat $SAILDIR/lib/prelude.sail $SAILDIR/lib/prelude_wrappers.sail $MIPS/mips_prelude.sail $MIPS/mips_tlb.sail $MIPS/mips_wrappers.sail > $DIR/pass/mips_wrappers.sail
-cat $SAILDIR/lib/prelude.sail $SAILDIR/lib/prelude_wrappers.sail $MIPS/mips_prelude.sail $MIPS/mips_tlb.sail $MIPS/mips_wrappers.sail $MIPS/mips_insts.sail $MIPS/mips_epilogue.sail > $DIR/pass/mips_insts.sail
-cat $SAILDIR/lib/prelude.sail $SAILDIR/lib/prelude_wrappers.sail $MIPS/mips_prelude.sail $MIPS/mips_tlb_stub.sail $MIPS/mips_wrappers.sail $MIPS/mips_insts.sail $MIPS/mips_epilogue.sail > $DIR/pass/mips_notlb.sail
+cat $SAILDIR/lib/prelude.sail $SAILDIR/lib/prelude_wrappers.sail $MIPS/mips_prelude.sail $MIPS/mips_tlb.sail $MIPS/mips_wrappers.sail $MIPS/mips_ast_decl.sail $MIPS/mips_insts.sail $MIPS/mips_epilogue.sail > $DIR/pass/mips_insts.sail
+cat $SAILDIR/lib/prelude.sail $SAILDIR/lib/prelude_wrappers.sail $MIPS/mips_prelude.sail $MIPS/mips_tlb_stub.sail $MIPS/mips_wrappers.sail $MIPS/mips_ast_decl.sail $MIPS/mips_insts.sail $MIPS/mips_epilogue.sail > $DIR/pass/mips_notlb.sail
 
 pass=0
 fail=0
@@ -103,14 +103,14 @@ function test_lem {
 	# MIPS requires an additional library, Mips_extras_embed.
 	# It might be useful to allow adding options for specific test cases.
 	# For now, include the library for all test cases, which doesn't seem to hurt.
-	if $SAILDIR/sail -lem -lem_lib Mips_extras_embed $DIR/$1/$i 2> /dev/null
+	if $SAILDIR/sail -lem -lem_lib Mips_extras_embed -lem_sequential -lem_mwords $DIR/$1/$i 2> /dev/null
 	then
 	    green "generated lem for $1/$i" "pass"
 
 	    cp $MIPS/mips_extras_embed_sequential.lem $DIR/lem/
-	    mv $SAILDIR/${i%%.*}_embed_types.lem $DIR/lem/
+	    # mv $SAILDIR/${i%%.*}_embed_types.lem $DIR/lem/
 	    mv $SAILDIR/${i%%.*}_embed_types_sequential.lem $DIR/lem/
-	    mv $SAILDIR/${i%%.*}_embed.lem $DIR/lem/
+	    # mv $SAILDIR/${i%%.*}_embed.lem $DIR/lem/
 	    mv $SAILDIR/${i%%.*}_embed_sequential.lem $DIR/lem/
 	    # Test sequential embedding for now
 	    # TODO: Add tests for the free monad
@@ -135,26 +135,26 @@ test_lem rtpass
 
 finish_suite "Lem generation 2"
 
-function test_ocaml {
-    for i in `ls $DIR/pass/`;
-    do
-	if $SAILDIR/sail -ocaml $DIR/$1/$i 2> /dev/null
-	then
-	    green "generated ocaml for $1/$i" "pass"
+# function test_ocaml {
+#     for i in `ls $DIR/pass/`;
+#     do
+# 	if $SAILDIR/sail -ocaml $DIR/$1/$i 2> /dev/null
+# 	then
+# 	    green "generated ocaml for $1/$i" "pass"
 
-	    rm $SAILDIR/${i%%.*}.ml
-	else
-	    red "generated ocaml for $1/$i" "fail"
-	fi
-    done
-}
+# 	    rm $SAILDIR/${i%%.*}.ml
+# 	else
+# 	    red "generated ocaml for $1/$i" "fail"
+# 	fi
+#     done
+# }
 
-test_ocaml pass
+# test_ocaml pass
 
-finish_suite "Ocaml generation 1"
+# finish_suite "Ocaml generation 1"
 
-test_ocaml rtpass
+# test_ocaml rtpass
 
-finish_suite "Ocaml generation 2"
+# finish_suite "Ocaml generation 2"
 
 printf "</testsuites>\n" >> $DIR/tests.xml