Make Lem export of CHERI(-256) typecheck

Note: The effect annotations of the execute function differ between CHERI and
MIPS, so I split out a new file mips_ast_decl.sail for MIPS with just the
initial declarations of ast, decode, and execute (with the right effects for
MIPS).

15 files changed, 190 insertions, 101 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..8425c110 100644
--- a/mips_new_tc/mips_extras_embed_sequential.lem
+++ b/mips_new_tc/mips_extras_embed_sequential.lem
@@ -6,8 +6,8 @@ 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_tag         : forall 'regs 'a 'b. Size 'b => (bitvector 'a * integer) -> M 'regs (bool * bitvector 'b)
+val MEMr_tag_reserve : forall 'regs 'a 'b. 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
@@ -15,12 +15,12 @@ let MEMr_reserve (addr,size)     = read_mem false Read_reserve addr size
 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)
+  return (bitU_to_bool t, 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)
+  return (bitU_to_bool t, v)
 
 
 val MEMea                 : forall 'regs 'a. (bitvector 'a * integer) -> M 'regs unit
@@ -37,13 +37,13 @@ let MEMea_tag_conditional (addr,size) = write_mem_ea Write_conditional 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_tag (_,_,t,v)             = write_mem_val v >>= fun _ -> write_tag (bool_to_bitU t) >>= fun _ -> return ()
+let MEMval_tag_conditional (_,_,t,v) = write_mem_val 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..4147b10c 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)
 
-_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/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index 3919d540..fbe096c9 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
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index 10a56ad5..9bc81b3e 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
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index eeec7440..e2cbb98a 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/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 7671c26b..3d4f3083 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -843,8 +843,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
diff --git a/test/typecheck/run_tests.sh b/test/typecheck/run_tests.sh
index 24f20d1f..8e21eca0 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