Modified MIPS model so it typechecks with the new typechecker

7 files changed, 317 insertions, 234 deletions

diff --git a/lib/prelude.sail b/lib/prelude.sail
index 350c6c20..9a52e5fb 100644
--- a/lib/prelude.sail
+++ b/lib/prelude.sail
@@ -1,32 +1,34 @@
 
-val cast forall Nat 'n, Nat 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0:2**'m - 1|] effect pure unsigned
+val cast forall Num 'n, Num 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0:2**'m - 1|] effect pure unsigned
 
-val forall Nat 'n, Nat 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0 - (2**('m - 1)):2**('m - 1) - 1|] effect pure signed
+val forall Num 'n, Num 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0 - (2**('m - 1)):2**('m - 1) - 1|] effect pure signed
 
-val forall Nat 'n, Nat 'm. [|0:'n|] -> vector<'m - 1,'m,dec,bit> effect pure to_vec
+val forall Num 'n, Num 'm. [|0:'n|] -> vector<'m - 1,'m,dec,bit> effect pure to_vec
+
+val forall Num 'm. int -> vector<'m - 1,'m,dec,bit> effect pure to_svec
 
 (* Vector access can't actually be properly polymorphic on vector
    direction because of the ranges being different for each type, so
    we overload it instead *)
-val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec
-val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc
+val forall Num 'n, Num 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec
+val forall Num 'n, Num 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc
 
 overload vector_access [vector_access_inc; vector_access_dec]
 
 (* Type safe vector subrange *)
-val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l.
+val forall Num 'n, Num 'l, Num 'm, Num 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l.
   (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,'o - 'm,inc,'a> effect pure vector_subrange_inc
 
-val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1.
+val forall Num 'n, Num 'l, Num 'm, Num 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1.
   (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - ('o - 1),dec,'a> effect pure vector_subrange_dec
 
-val forall Nat 'n, Nat 'l, Order 'ord.
+val forall Num 'n, Num 'l, Order 'ord.
   (vector<'n,'l,'ord,bit>, int, int) -> list<bit> effect pure vector_subrange_bl
 
 overload vector_subrange [vector_subrange_inc; vector_subrange_dec; vector_subrange_bl]
 
 (* Type safe vector append *)
-val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0.
+val forall Num 'n1, Num 'l1, Num 'n2, Num 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0.
   (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'l1 + 'l2 - 1,'l1 + 'l2,'o,'a> effect pure vec_append
 
 val (list<bit>, list<bit>) -> list<bit> effect pure list_append
@@ -37,89 +39,98 @@ overload vector_append [vec_append; list_append]
 val cast forall Type 'a. register<'a> -> 'a effect {rreg} reg_deref
 
 (* Bitvector duplication *)
-val forall Nat 'n. (bit, [:'n:]) -> vector<'n - 1,'n,dec,bit> effect pure duplicate
+val forall Num 'n. (bit, [:'n:]) -> vector<'n - 1,'n,dec,bit> effect pure duplicate
 
 val (bit, int) -> list<bit> effect pure duplicate_to_list
 
-val forall Nat 'n, Nat 'm, Nat 'o, Order 'ord.
+val forall Num 'n, Num 'm, Num 'o, Order 'ord.
   (vector<'o,'n,'ord,bit>, [:'m:]) -> vector<'o,'m*'n,'ord,bit> effect pure duplicate_bits
 
-val forall Nat 'n, Nat 'o, Order 'ord.
+val forall Num 'n, Num 'o, Order 'ord.
   (vector<'o,'n,'ord,bit>, int) -> list<bit> effect pure duplicate_bits_to_list
 
 overload (deinfix ^^) [duplicate; duplicate_bits; duplicate_to_list; duplicate_bits_to_list]
 
 (* Bitvector extension *)
-val forall Nat 'n, Nat 'm, Nat 'o, Nat 'p, Order 'ord.
+val forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord.
     vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure extz
 
-val forall Nat 'm, Nat 'p, Order 'ord.
+val forall Num 'm, Num 'p, Order 'ord.
     list<bit> -> vector<'p, 'm, 'ord, bit> effect pure extz_bl
 
-val forall Nat 'n, Nat 'm, Nat 'o, Nat 'p, Order 'ord.
+val forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord.
     vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure exts
 
-val forall Nat 'm, Nat 'p, Order 'ord.
+val forall Num 'm, Num 'p, Order 'ord.
     list<bit> -> vector<'p, 'm, 'ord, bit> effect pure exts_bl
 
+val cast forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord, 'm >= 'n.
+    vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure extzi
+
 overload EXTZ [extz; extz_bl]
 overload EXTS [exts; exts_bl]
 
-val forall Type 'a, Nat 'n, Nat 'm, Nat 'o, Nat 'p, Order 'ord, 'm >= 'o.
+val forall Type 'a, Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord, 'm >= 'o.
     vector<'n, 'm, 'ord, 'a> -> vector<'p, 'o, 'ord, 'a> effect pure mask
 
 (* Adjust the start index of a decreasing bitvector *)
-val cast forall Nat 'n, Nat 'm, 'n >= 'm - 1.
+val cast forall Num 'n, Num 'm, 'n >= 'm - 1.
   vector<'n,'m,dec,bit> -> vector<'m - 1,'m,dec,bit>
   effect pure norm_dec
 
-val cast forall Nat 'n, Nat 'm, Nat 'o, 'n >= 'm - 1, 'o >= 'm - 1.
+val cast forall Num 'n, Num 'm, Num 'o, 'n >= 'm - 1, 'o >= 'm - 1.
   vector<'n,'m,dec,bit> -> vector<'o,'m,dec,bit>
   effect pure adjust_dec
 
 (* Various casts from 0 and 1 to bitvectors *)
-val cast forall Nat 'n, Nat 'l, Order 'ord. [:0:] -> vector<'n,'l,'ord,bit> effect pure cast_0_vec
-val cast forall Nat 'n, Nat 'l, Order 'ord. [:1:] -> vector<'n,'l,'ord,bit> effect pure cast_1_vec
-val cast forall Nat 'n, Nat 'l, Order 'ord. [|0:1|] -> vector<'n,'l,'ord,bit> effect pure cast_01_vec
+val cast forall Num 'n, Num 'l, Order 'ord. [:0:] -> vector<'n,'l,'ord,bit> effect pure cast_0_vec
+val cast forall Num 'n, Num 'l, Order 'ord. [:1:] -> vector<'n,'l,'ord,bit> effect pure cast_1_vec
+val cast forall Num 'n, Num 'l, Order 'ord. [|0:1|] -> vector<'n,'l,'ord,bit> effect pure cast_01_vec
 
-val cast forall Nat 'n, Order 'ord. vector<'n,1,'ord,bit> -> bool effect pure cast_vec_bool
+val cast forall Num 'n, Order 'ord. vector<'n,1,'ord,bit> -> bool effect pure cast_vec_bool
 val cast bit -> bool effect pure cast_bit_bool
 
+val cast forall Num 'n, Num 'm, 'n >= 'm - 1, 'm >= 1. bit -> vector<'n,'m,dec,bit> effect pure cast_bit_vec
+
 (* MSB *)
-val forall Nat 'n, Nat 'm, Order 'ord. vector<'n, 'm, 'ord, bit> -> bit effect pure most_significant
+val forall Num 'n, Num 'm, Order 'ord. vector<'n, 'm, 'ord, bit> -> bit effect pure most_significant
 
 (* Arithmetic *)
 
-val forall Nat 'n, Nat 'm, Nat 'o, Nat 'p.
+val forall Num 'n, Num 'm, Num 'o, Num 'p.
     ([|'n:'m|], [|'o:'p|]) -> [|'n + 'o:'m + 'p|] effect pure add
 
 val (nat, nat) -> nat effect pure add_nat
 
 val (int, int) -> int effect pure add_int
 
-val forall Nat 'n, Nat 'o, Order 'ord.
+val forall Num 'n, Num 'o, Order 'ord.
     (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure add_vec
 
-val forall Nat 'n, Nat 'o, Order 'ord.
+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.
     (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> (vector<'o, 'n, 'ord, bit>, bit, bit) effect pure add_overflow_vec
 
-val forall Nat 'n, Nat 'm, Nat 'o, Nat 'p.
+val forall Num 'n, Num 'm, Num 'o, Num 'p.
     ([|'n:'m|], [|'o:'p|]) -> [|'n - 'p:'m - 'o|] effect pure sub
 
 val (int, int) -> int effect pure sub_int
 
-val forall Nat 'n, Nat 'm, Order 'ord.
+val forall Num 'n, Num 'm, Order 'ord.
     (vector<'n,'m,'ord,bit>, int) -> vector<'n,'m,'ord,bit> effect pure sub_vec_int
 
-val forall Nat 'n, Nat 'o, Order 'ord.
+val forall Num 'n, Num 'o, Order 'ord.
     (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure sub_vec
 
-val forall Nat 'n, Nat 'o, Order 'ord.
+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 sub_underflow_vec
 
 overload (deinfix +) [
   add_vec;
   add_overflow_vec;
+  add_vec_int;
   add;
   add_nat;
   add_int
@@ -133,21 +144,35 @@ overload (deinfix -) [
   sub_int
 ]
 
-val forall Nat 'n, Nat 'o, Order 'ord.
-    (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure add_svec
+val bool -> bit effect pure bool_to_bit
+
+val (int, int) -> int effect pure mul_int
+val forall Num 'n, Num 'o, Order 'ord.
+    (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure mul_vec
+
+overload (deinfix * ) [
+  mul_vec;
+  mul_int
+]
+
+val forall Num 'n, Num 'o, Order 'ord.
+    (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure mul_svec
 
 overload (deinfix *_s) [
-  add_svec
+  mul_svec
 ]
 
-val forall Nat 'n, Nat 'o, Order 'ord.
+val (bool, bool) -> bool effect pure bool_xor
+
+val forall Num 'n, Num 'o, Order 'ord.
     (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure xor_vec
 
 overload (deinfix ^) [
+  bool_xor;
   xor_vec
 ]
 
-val forall Nat 'n, Nat 'o, Order 'ord.
+val forall Num 'n, Num 'o, Order 'ord.
     (vector<'o, 'n, 'ord, bit>, int) -> vector<'o, 'n, 'ord, bit> effect pure shiftl
 
 overload (deinfix <<) [
@@ -230,6 +255,10 @@ val (int, int) -> int effect pure quotient
 
 overload (deinfix quot) [quotient]
 
+val (int, int) -> int effect pure modulus
+
+overload (deinfix mod) [modulus]
+
 val forall Num 'n, Num 'm, Order 'ord, Type 'a. vector<'n,'m,'ord,'a> -> [:'m:] effect pure length
 
 val cast forall Num 'n. [:'n:] -> [|'n|] effect pure upper
diff --git a/mips_new_tc/mips_epilogue.sail b/mips_new_tc/mips_epilogue.sail
index 50993949..09ce7688 100644
--- a/mips_new_tc/mips_epilogue.sail
+++ b/mips_new_tc/mips_epilogue.sail
@@ -38,4 +38,4 @@ end decode
 end execute
 end ast
 
-function option<ast> supported_instructions (instr) = Some(instr)
+function option<ast> supported_instructions (ast) instr = Some(instr)
diff --git a/mips_new_tc/mips_insts.sail b/mips_new_tc/mips_insts.sail
index 19176c72..88c78e80 100644
--- a/mips_new_tc/mips_insts.sail
+++ b/mips_new_tc/mips_insts.sail
@@ -32,12 +32,12 @@
 (*  SUCH DAMAGE.                                                          *)
 (*========================================================================*)
 
-(* misp_insts.sail: mips instruction decode and execute clauses and AST node 
+(* misp_insts.sail: mips instruction decode and execute clauses and AST node
    declarations *)
 
 scattered typedef ast = const union
 
-val ast -> unit effect pure execute
+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
@@ -47,13 +47,13 @@ scattered function option<ast> decode
 (* [D]ADD[I][U] various forms of ADD                                                  *)
 (**************************************************************************************)
 
-(* DADDIU Doubleword Add Immediate Unsigned -- 
-   the simplest possible instruction, no undefined behaviour or exceptions 
+(* DADDIU Doubleword Add Immediate Unsigned --
+   the simplest possible instruction, no undefined behaviour or exceptions
    reg, reg, immediate *)
 
 union ast member regregimm16 DADDIU
 
-function clause decode (0b011001 : (regno) rs : (regno) rt : (imm16) imm) = 
+function clause decode (0b011001 : (regno) rs : (regno) rt : (imm16) imm) =
   Some(DADDIU(rs, rt, imm))
 
 function clause execute (DADDIU (rs, rt, imm)) =
@@ -66,7 +66,7 @@ function clause execute (DADDIU (rs, rt, imm)) =
 
 union ast member regregreg DADDU
 
-function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101101) = 
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101101) =
   Some(DADDU(rs, rt, rd))
 
 function clause execute (DADDU (rs, rt, rd)) =
@@ -79,7 +79,7 @@ function clause execute (DADDU (rs, rt, rd)) =
 
 union ast member regregimm16 DADDI
 
-function clause decode (0b011000 : (regno) rs : (regno) rt : (imm16) imm) = 
+function clause decode (0b011000 : (regno) rs : (regno) rt : (imm16) imm) =
   Some(DADDI(rs, rt, imm))
 
 function clause execute (DADDI (rs, rt, imm)) =
@@ -98,7 +98,7 @@ function clause execute (DADDI (rs, rt, imm)) =
 
 union ast member regregreg DADD
 
-function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101100) = 
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101100) =
   Some(DADD(rs, rt, rd))
 
 function clause execute (DADD (rs, rt, rd)) =
@@ -140,7 +140,7 @@ union ast member regregimm16 ADDI
 function clause decode (0b001000 : (regno) rs : (regno) rt : (imm16) imm) =
   Some(ADDI(rs, rt, imm))
 
-function clause execute (ADDI(rs, rt, imm)) = 
+function clause execute (ADDI(rs, rt, imm)) =
   {
     (bit[64]) opA := rGPR(rs);
     if NotWordVal(opA) then
@@ -160,7 +160,7 @@ union ast member regregreg ADDU
 function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100001) =
   Some(ADDU(rs, rt, rd))
 
-function clause execute (ADDU(rs, rt, rd)) = 
+function clause execute (ADDU(rs, rt, rd)) =
   {
     (bit[64]) opA := rGPR(rs);
     (bit[64]) opB := rGPR(rt);
@@ -178,7 +178,7 @@ union ast member regregimm16 ADDIU
 function clause decode (0b001001 : (regno) rs : (regno) rt : (imm16) imm) =
   Some(ADDIU(rs, rt, imm))
 
-function clause execute (ADDIU(rs, rt, imm)) = 
+function clause execute (ADDIU(rs, rt, imm)) =
   {
     (bit[64]) opA := rGPR(rs);
     if NotWordVal(opA) then
@@ -195,7 +195,7 @@ function clause execute (ADDIU(rs, rt, imm)) =
 
 union ast member regregreg DSUBU
 
-function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101111) = 
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101111) =
   Some(DSUBU(rs, rt, rd))
 
 function clause execute (DSUBU (rs, rt, rd)) =
@@ -207,7 +207,7 @@ function clause execute (DSUBU (rs, rt, rd)) =
 
 union ast member regregreg DSUB
 
-function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101110) = 
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101110) =
   Some(DSUB(rs, rt, rd))
 
 function clause execute (DSUB (rs, rt, rd)) =
@@ -248,7 +248,7 @@ union ast member regregreg SUBU
 function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100011) =
     Some(SUBU(rs, rt, rd))
 
-function clause execute (SUBU(rs, rt, rd)) = 
+function clause execute (SUBU(rs, rt, rd)) =
   {
     (bit[64]) opA := rGPR(rs);
     (bit[64]) opB := rGPR(rt);
@@ -265,7 +265,7 @@ function clause execute (SUBU(rs, rt, rd)) =
 (* AND reg, reg, reg *)
 
 union ast member regregreg AND
-function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100100) = 
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100100) =
     Some(AND(rs, rt, rd))
 
 function clause execute (AND (rs, rt, rd)) =
@@ -276,7 +276,7 @@ function clause execute (AND (rs, rt, rd)) =
 (* ANDI reg, reg, imm *)
 
 union ast member regregimm16 ANDI
-function clause decode (0b001100 : (regno) rs : (regno) rt : (imm16) imm) = 
+function clause decode (0b001100 : (regno) rs : (regno) rt : (imm16) imm) =
   Some(ANDI(rs, rt, imm))
 function clause execute (ANDI (rs, rt, imm)) =
   {
@@ -286,7 +286,7 @@ function clause execute (ANDI (rs, rt, imm)) =
 (* OR reg, reg, reg *)
 
 union ast member regregreg OR
-function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100101) = 
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100101) =
   Some(OR(rs, rt, rd))
 function clause execute (OR (rs, rt, rd)) =
   {
@@ -296,7 +296,7 @@ function clause execute (OR (rs, rt, rd)) =
 (* ORI reg, reg, imm *)
 
 union ast member regregimm16 ORI
-function clause decode (0b001101 : (regno) rs : (regno) rt : (imm16) imm) = 
+function clause decode (0b001101 : (regno) rs : (regno) rt : (imm16) imm) =
   Some(ORI(rs, rt, imm))
 function clause execute (ORI (rs, rt, imm)) =
   {
@@ -306,7 +306,7 @@ function clause execute (ORI (rs, rt, imm)) =
 (* NOR reg, reg, reg *)
 
 union ast member regregreg NOR
-function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100111) = 
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100111) =
   Some(NOR(rs, rt, rd))
 function clause execute (NOR (rs, rt, rd)) =
   {
@@ -316,7 +316,7 @@ function clause execute (NOR (rs, rt, rd)) =
 (* XOR reg, reg, reg *)
 
 union ast member regregreg XOR
-function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100110) = 
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100110) =
   Some(XOR(rs, rt, rd))
 function clause execute (XOR (rs, rt, rd)) =
   {
@@ -325,7 +325,7 @@ function clause execute (XOR (rs, rt, rd)) =
 
 (* XORI reg, reg, imm *)
 union ast member regregimm16 XORI
-function clause decode (0b001110 : (regno) rs : (regno) rt : (imm16) imm) = 
+function clause decode (0b001110 : (regno) rs : (regno) rt : (imm16) imm) =
   Some(XORI(rs, rt, imm))
 function clause execute (XORI (rs, rt, imm)) =
   {
@@ -333,8 +333,8 @@ function clause execute (XORI (rs, rt, imm)) =
   }
 
 (* LUI reg, imm 32-bit load immediate into upper 16 bits *)
-union ast member (regno, imm16) LUI 
-function clause decode (0b001111 : 0b00000 : (regno) rt : (imm16) imm) = 
+union ast member (regno, imm16) LUI
+function clause decode (0b001111 : 0b00000 : (regno) rt : (imm16) imm) =
   Some(LUI(rt, imm))
 function clause execute (LUI (rt, imm)) =
   {
@@ -348,18 +348,18 @@ function clause execute (LUI (rt, imm)) =
 (* DSLL reg, reg, imm5 *)
 
 union ast member regregreg DSLL
-function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111000) = 
+function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111000) =
   Some(DSLL(rt, rd, sa))
 function clause execute (DSLL (rt, rd, sa)) =
   {
-    
+
     wGPR(rd) := (rGPR(rt) << sa) (* make tuareg mode less blue >> *)
   }
 
 (* DSLL32 reg, reg, imm5 *)
 
 union ast member regregreg DSLL32
-function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111100) = 
+function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111100) =
   Some(DSLL32(rt, rd, sa))
 function clause execute (DSLL32 (rt, rd, sa)) =
   {
@@ -369,12 +369,12 @@ function clause execute (DSLL32 (rt, rd, sa)) =
 (* DSLLV reg, reg, reg *)
 
 union ast member regregreg DSLLV
-function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b010100) = 
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b010100) =
   Some(DSLLV(rs, rt, rd))
 function clause execute (DSLLV (rs, rt, rd)) =
   {
     wGPR(rd) := (rGPR(rt) << ((rGPR(rs))[5 .. 0])) (* make tuareg mode less blue >> *)
-    (* alternative slicing based version of above 
+    (* alternative slicing based version of above
     sa       := (rGPR(rt))[5 .. 0];
     v        := rGPR(rs);
     wGPR(rd) := v[(63-sa) .. 0] : (0b0 ^^ sa)  *)
@@ -383,24 +383,24 @@ function clause execute (DSLLV (rs, rt, rd)) =
 (* DSRA arithmetic shift duplicating sign bit - reg, reg, imm5 *)
 
 union ast member regregreg DSRA
-function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111011) = 
+function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111011) =
   Some(DSRA(rt, rd, sa))
 function clause execute (DSRA (rt, rd, sa)) =
   {
     temp     := rGPR(rt);
-    wGPR(rd) := EXTS((temp[63] ^^ sa) : (temp[63 .. sa]))
+    wGPR(rd) := EXTZ((temp[63] ^^ sa) : (temp[63 .. sa]))
   }
 
 (* DSRA32 reg, reg, imm5 *)
 
 union ast member regregreg DSRA32
-function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111111) = 
+function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111111) =
   Some(DSRA32(rt, rd, sa))
 function clause execute (DSRA32 (rt, rd, sa)) =
   {
     temp     := rGPR(rt);
     sa32     := (0b1 : sa); (* sa+32 *)
-    wGPR(rd) := EXTS((temp[63] ^^ sa32) : (temp[63 .. sa32]))
+    wGPR(rd) := EXTZ((temp[63] ^^ sa32) : (temp[63 .. sa32]))
   }
 
 (* DSRAV reg, reg, reg *)
@@ -411,42 +411,42 @@ function clause execute (DSRAV (rs, rt, rd)) =
   {
     temp     := rGPR(rt);
     sa       := (rGPR(rs)) [5..0];
-    wGPR(rd) := EXTS((temp[63] ^^ sa) : temp[63 .. sa])
+    wGPR(rd) := EXTZ((temp[63] ^^ sa) : temp[63 .. sa])
   }
 
 (* DSRL shift right logical - reg, reg, imm5 *)
 
 union ast member regregreg DSRL
-function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111010) = 
+function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111010) =
   Some(DSRL(rt, rd, sa))
 function clause execute (DSRL (rt, rd, sa)) =
   {
     temp     := rGPR(rt);
-    wGPR(rd) := EXTS((bitzero ^^ sa) : (temp[63 .. sa]))
+    wGPR(rd) := EXTZ((bitzero ^^ sa) : (temp[63 .. sa]))
   }
 
 (* DSRL32 reg, reg, imm5 *)
 
 union ast member regregreg DSRL32
-function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111110) = 
+function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111110) =
   Some(DSRL32(rt, rd, sa))
 function clause execute (DSRL32 (rt, rd, sa)) =
   {
     temp     := rGPR(rt);
     sa32     := (0b1 : sa); (* sa+32 *)
-    wGPR(rd) := EXTS((bitzero ^^ sa32) : (temp[63 .. sa32]))
+    wGPR(rd) := EXTZ((bitzero ^^ sa32) : (temp[63 .. sa32]))
   }
 
 (* DSRLV reg, reg, reg *)
 
 union ast member regregreg DSRLV
-function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b010110) = 
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b010110) =
   Some(DSRLV(rs, rt, rd))
 function clause execute (DSRLV (rs, rt, rd)) =
   {
     temp     := rGPR(rt);
     sa       := (rGPR(rs)) [5..0];
-    wGPR(rd) := EXTS((bitzero ^^ sa) : temp[63 .. sa])
+    wGPR(rd) := EXTZ((bitzero ^^ sa) : temp[63 .. sa])
   }
 
 (**************************************************************************************)
@@ -456,28 +456,28 @@ function clause execute (DSRLV (rs, rt, rd)) =
 (* SLL 32-bit shift left *)
 
 union ast member regregreg SLL
-function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (regno) sa : 0b000000) = 
+function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (regno) sa : 0b000000) =
   Some(SLL(rt, rd, sa))
 function clause execute (SLL(rt, rd, sa)) =
   {
-    wGPR(rd) := EXTS((rGPR(rt)) [31 - sa .. 0] : (bitzero ^^ sa))
+    wGPR(rd) := EXTZ((rGPR(rt)) [31 - sa .. 0] : (bitzero ^^ sa))
   }
 
 (* SLLV 32-bit shift left variable *)
 
 union ast member regregreg SLLV
-function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b000100) = 
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b000100) =
   Some(SLLV(rs, rt, rd))
 function clause execute (SLLV(rs, rt, rd)) =
   {
     sa       := (rGPR(rs))[4..0];
-    wGPR(rd) := EXTS((rGPR(rt)) [31 - sa .. 0] : (bitzero ^^ sa))
+    wGPR(rd) := EXTZ((rGPR(rt)) [31 - sa .. 0] : (bitzero ^^ sa))
   }
 
 (* SRA 32-bit arithmetic shift right *)
 
 union ast member regregreg SRA
-function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (regno) sa : 0b000011) = 
+function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (regno) sa : 0b000011) =
   Some(SRA(rt, rd, sa))
 function clause execute (SRA(rt, rd, sa)) =
   {
@@ -485,13 +485,13 @@ function clause execute (SRA(rt, rd, sa)) =
     if (NotWordVal(temp)) then
       wGPR(rd) := undefined
     else
-      wGPR(rd) := EXTS((temp[31] ^^ (sa+32)) : temp [31..sa])
+      wGPR(rd) := EXTZ((temp[31] ^^ (sa+32)) : temp [31..sa])
   }
 
 (* SRAV 32-bit arithmetic shift right variable *)
 
 union ast member regregreg SRAV
-function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b000111) = 
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b000111) =
   Some(SRAV(rs, rt, rd))
 function clause execute (SRAV(rs, rt, rd)) =
   {
@@ -500,13 +500,13 @@ function clause execute (SRAV(rs, rt, rd)) =
     if (NotWordVal(temp)) then
       wGPR(rd) := undefined
     else
-      wGPR(rd) := EXTS((temp[31] ^^ (sa+32)) : temp [31..sa])
+      wGPR(rd) := EXTZ((temp[31] ^^ (sa+32)) : temp [31..sa])
   }
 
 (* SRL 32-bit shift right *)
 
 union ast member regregreg SRL
-function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (regno) sa : 0b000010) = 
+function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (regno) sa : 0b000010) =
   Some(SRL(rt, rd, sa))
 function clause execute (SRL(rt, rd, sa)) =
   {
@@ -514,13 +514,13 @@ function clause execute (SRL(rt, rd, sa)) =
     if (NotWordVal(temp)) then
       wGPR(rd) := undefined
     else
-      wGPR(rd) := EXTS((bitzero ^^ sa) : (temp [31..sa]))
+      wGPR(rd) := EXTZ((bitzero ^^ sa) : (temp [31..sa]))
   }
 
 (* SRLV 32-bit shift right variable *)
 
 union ast member regregreg SRLV
-function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b000110) = 
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b000110) =
   Some(SRLV(rs, rt, rd))
 function clause execute (SRLV(rs, rt, rd)) =
   {
@@ -529,7 +529,7 @@ function clause execute (SRLV(rs, rt, rd)) =
     if (NotWordVal(temp)) then
       wGPR(rd) := undefined
     else
-      wGPR(rd) := EXTS((bitzero ^^ sa) : (temp [31..sa]))
+      wGPR(rd) := EXTZ((bitzero ^^ sa) : (temp [31..sa]))
   }
 
 (**************************************************************************************)
@@ -539,7 +539,7 @@ function clause execute (SRLV(rs, rt, rd)) =
 (* SLT set if less than (signed) *)
 
 union ast member regregreg SLT
-function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101010) = 
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101010) =
   Some(SLT(rs, rt, rd))
 function clause execute (SLT(rs, rt, rd)) =
   {
@@ -549,7 +549,7 @@ function clause execute (SLT(rs, rt, rd)) =
 (* SLT set if less than immediate (signed) *)
 
 union ast member regregimm16 SLTI
-function clause decode (0b001010 : (regno) rs : (regno) rt : (imm16) imm) = 
+function clause decode (0b001010 : (regno) rs : (regno) rt : (imm16) imm) =
   Some(SLTI(rs, rt, imm))
 function clause execute (SLTI(rs, rt, imm)) =
   {
@@ -561,7 +561,7 @@ function clause execute (SLTI(rs, rt, imm)) =
 (* SLTU set if less than unsigned *)
 
 union ast member regregreg SLTU
-function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101011) = 
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101011) =
   Some(SLTU(rs, rt, rd))
 function clause execute (SLTU(rs, rt, rd)) =
   {
@@ -573,7 +573,7 @@ function clause execute (SLTU(rs, rt, rd)) =
 (* SLTIU set if less than immediate unsigned *)
 
 union ast member regregimm16 SLTIU
-function clause decode (0b001011 : (regno) rs : (regno) rt : (imm16) imm) = 
+function clause decode (0b001011 : (regno) rs : (regno) rt : (imm16) imm) =
   Some(SLTIU(rs, rt, imm))
 function clause execute (SLTIU(rs, rt, imm)) =
   {
@@ -585,22 +585,22 @@ function clause execute (SLTIU(rs, rt, imm)) =
 (* MOVN move if non-zero *)
 
 union ast member regregreg MOVN
-function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b001011) = 
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b001011) =
   Some(MOVN(rs, rt, rd))
 function clause execute (MOVN(rs, rt, rd)) =
   {
-    if (rGPR(rt) != 0x0000000000000000) then 
+    if (rGPR(rt) != 0x0000000000000000) then
       wGPR(rd) := rGPR(rs)
   }
 
 (* MOVZ move if zero *)
 
 union ast member regregreg MOVZ
-function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b001010) = 
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b001010) =
   Some(MOVZ(rs, rt, rd))
 function clause execute (MOVZ(rs, rt, rd)) =
   {
-    if (rGPR(rt) == 0x0000000000000000) then 
+    if (rGPR(rt) == 0x0000000000000000) then
       wGPR(rd) := rGPR(rs)
   }
 
@@ -610,7 +610,7 @@ function clause execute (MOVZ(rs, rt, rd)) =
 
 (* MFHI move from HI register *)
 union ast member regno MFHI
-function clause decode (0b000000 : 0b0000000000 : (regno) rd : 0b00000 : 0b010000) = 
+function clause decode (0b000000 : 0b0000000000 : (regno) rd : 0b00000 : 0b010000) =
   Some(MFHI(rd))
 function clause execute (MFHI(rd)) =
   {
@@ -619,7 +619,7 @@ function clause execute (MFHI(rd)) =
 
 (* MFLO move from LO register *)
 union ast member regno MFLO
-function clause decode (0b000000 : 0b0000000000 : (regno) rd : 0b00000 : 0b010010) = 
+function clause decode (0b000000 : 0b0000000000 : (regno) rd : 0b00000 : 0b010010) =
   Some(MFLO(rd))
 function clause execute (MFLO(rd)) =
   {
@@ -628,7 +628,7 @@ function clause execute (MFLO(rd)) =
 
 (* MTHI move to HI register *)
 union ast member regno MTHI
-function clause decode (0b000000 : (regno) rs : 0b000000000000000 : 0b010001) = 
+function clause decode (0b000000 : (regno) rs : 0b000000000000000 : 0b010001) =
   Some(MTHI(rs))
 function clause execute (MTHI(rs)) =
   {
@@ -637,7 +637,7 @@ function clause execute (MTHI(rs)) =
 
 (* MTLO move to LO register *)
 union ast member regno MTLO
-function clause decode (0b000000 : (regno) rs : 0b000000000000000 : 0b010011) = 
+function clause decode (0b000000 : (regno) rs : 0b000000000000000 : 0b010011) =
   Some(MTLO(rs))
 function clause execute (MTLO(rs)) =
   {
@@ -657,7 +657,7 @@ function clause execute (MUL(rs, rt, rd)) =
         undefined
       else
         EXTS(result[31..0]);
-    (* HI and LO are technically undefined after MUL, but this causes problems with tests and 
+    (* HI and LO are technically undefined after MUL, but this causes problems with tests and
        (potentially) context switch so just leave them alone
     HI := undefined;
     LO := undefined;
@@ -691,7 +691,7 @@ function clause execute (MULTU(rs, rt)) =
     (bit[64]) result := if (NotWordVal(rsVal) | NotWordVal(rtVal)) then
         undefined
       else
-        (rsVal[31..0]) * (rtVal[31..0]);
+	EXTS((rsVal[31..0]) * (rtVal[31..0]));
     HI := EXTS(result[63..32]);
     LO := EXTS(result[31..0]);
   }
@@ -796,13 +796,13 @@ function clause execute (DIV(rs, rt)) =
     rtVal := rGPR(rt);
     let ((bit[32]) q, (bit[32])r) = (
       if (NotWordVal(rsVal) | NotWordVal(rtVal) | (rtVal == 0)) then
-        (undefined, undefined)
+	((bit[32]) undefined, (bit[32]) undefined)
       else
         let si = (signed((rsVal[31..0]))) in
         let ti = (signed((rtVal[31..0]))) in
         let qi = (si quot ti)  in
         let ri = (si - (ti*qi))   in
-        ((bit[32]) qi, (bit[32]) ri))
+	((bit[32]) (to_svec(qi)), (bit[32]) (to_svec(ri))))
     in
     {
       HI := EXTS(r);
@@ -820,13 +820,13 @@ function clause execute (DIVU(rs, rt)) =
     rtVal := rGPR(rt);
     let ((bit[32]) q, (bit[32])r) = (
       if (NotWordVal(rsVal) | NotWordVal(rtVal) | rtVal == 0) then
-        (undefined, undefined)
+	((bit[32]) undefined, (bit[32]) undefined)
       else
         let si = unsigned(rsVal[31..0]) in
         let ti = unsigned(rtVal[31..0]) in
         let qi = (si quot ti)  in
         let ri = (si mod ti)   in
-        ((bit[32]) qi, (bit[32]) ri))
+	((bit[32]) (to_svec(qi)), (bit[32]) (to_svec(ri))))
     in
     {
       HI := EXTS(r);
@@ -843,11 +843,11 @@ function clause execute (DDIV(rs, rt)) =
     rsVal := signed(rGPR(rs));
     rtVal := signed(rGPR(rt));
     let ((bit[64])q, (bit[64])r) = (if (rtVal == 0)
-      then (undefined, undefined) 
-      else 
+      then ((bit[64]) undefined, (bit[64]) undefined)
+      else
            let qi = (rsVal quot rtVal) in
            let ri = (rsVal - (qi * rtVal)) in
-           ((bit[64]) qi, (bit[64]) ri)) in
+	   ((bit[64]) (to_svec(qi)), (bit[64]) (to_svec(ri)))) in
     {
       LO    := q;
       HI    := r;
@@ -863,10 +863,10 @@ function clause execute (DDIVU(rs, rt)) =
     (int) rsVal := rGPR(rs);
     (int) rtVal := rGPR(rt);
     let ((bit[64])q, (bit[64])r) = (if (rtVal == 0)
-      then (undefined, undefined) 
+      then ((bit[64]) undefined, (bit[64]) undefined)
       else let qi = (rsVal quot rtVal) in
            let ri = (rsVal mod rtVal) in
-           ((bit[64]) qi, (bit[64]) ri)) in
+	   ((bit[64]) (to_svec(qi)), (bit[64]) (to_svec(ri)))) in
     {
       LO    := q;
       HI    := r;
@@ -881,7 +881,7 @@ function clause execute (DDIVU(rs, rt)) =
 union ast member (bit[26]) J
 function clause decode (0b000010 : (bit[26]) offset) =
   Some(J(offset))
-function clause execute (J(offset)) = 
+function clause execute (J(offset)) =
   {
     delayedPC     := (PC + 4)[63..28] : offset : 0b00;
     branchPending := 1
@@ -891,11 +891,11 @@ function clause execute (J(offset)) =
 union ast member (bit[26]) JAL
 function clause decode (0b000011 : (bit[26]) offset) =
   Some(JAL(offset))
-function clause execute (JAL(offset)) = 
+function clause execute (JAL(offset)) =
   {
     delayedPC     := (PC + 4)[63..28] : offset : 0b00;
     branchPending := 1;
-    wGPR(31)      := PC + 8;
+    wGPR(0b11111) := PC + 8;
   }
 
 (* JR -- jump via register *)
@@ -925,13 +925,13 @@ function clause execute (JALR(rs, rd)) =
 (**************************************************************************************)
 
 union ast member (regno, regno, imm16, bool, bool) BEQ
-function clause decode (0b000100 : (regno) rs : (regno) rt : (imm16) imm) = 
+function clause decode (0b000100 : (regno) rs : (regno) rt : (imm16) imm) =
   Some(BEQ(rs, rt, imm, false, false))  (* BEQ  *)
-function clause decode (0b010100 : (regno) rs : (regno) rt : (imm16) imm) = 
+function clause decode (0b010100 : (regno) rs : (regno) rt : (imm16) imm) =
   Some(BEQ(rs, rt, imm, false, true))   (* BEQL *)
-function clause decode (0b000101 : (regno) rs : (regno) rt : (imm16) imm) = 
+function clause decode (0b000101 : (regno) rs : (regno) rt : (imm16) imm) =
   Some(BEQ(rs, rt, imm, true , false))  (* BNE  *)
-function clause decode (0b010101 : (regno) rs : (regno) rt : (imm16) imm) = 
+function clause decode (0b010101 : (regno) rs : (regno) rt : (imm16) imm) =
   Some(BEQ(rs, rt, imm, true , true))   (* BNEL *)
 function clause execute (BEQ(rs, rd, imm, ne, likely)) =
   {
@@ -948,8 +948,8 @@ function clause execute (BEQ(rs, rd, imm, ne, likely)) =
       }
   }
 
-(* 
-   
+(*
+
    Branches comparing with zero (single register operand, possible link in r31)
 *)
 
@@ -959,32 +959,32 @@ function clause execute (BEQ(rs, rd, imm, ne, likely)) =
 (**************************************************************************************)
 
 union ast member (regno, imm16, Comparison, bool, bool) BCMPZ
-function clause decode (0b000001 : (regno) rs : 0b00000 : (imm16) imm) = 
+function clause decode (0b000001 : (regno) rs : 0b00000 : (imm16) imm) =
   Some(BCMPZ(rs, imm, LT, false, false)) (* BLTZ *)
-function clause decode (0b000001 : (regno) rs : 0b10000 : (imm16) imm) = 
+function clause decode (0b000001 : (regno) rs : 0b10000 : (imm16) imm) =
   Some(BCMPZ(rs, imm, LT, true, false))  (* BLTZAL *)
-function clause decode (0b000001 : (regno) rs : 0b00010 : (imm16) imm) = 
+function clause decode (0b000001 : (regno) rs : 0b00010 : (imm16) imm) =
   Some(BCMPZ(rs, imm, LT, false, true))  (* BLTZL *)
-function clause decode (0b000001 : (regno) rs : 0b10010 : (imm16) imm) = 
+function clause decode (0b000001 : (regno) rs : 0b10010 : (imm16) imm) =
   Some(BCMPZ(rs, imm, LT, true, true))   (* BLTZALL *)
 
-function clause decode (0b000001 : (regno) rs : 0b00001 : (imm16) imm) = 
+function clause decode (0b000001 : (regno) rs : 0b00001 : (imm16) imm) =
   Some(BCMPZ(rs, imm, GE, false, false)) (* BGEZ *)
-function clause decode (0b000001 : (regno) rs : 0b10001 : (imm16) imm) = 
+function clause decode (0b000001 : (regno) rs : 0b10001 : (imm16) imm) =
   Some(BCMPZ(rs, imm, GE, true, false))  (* BGEZAL *)
-function clause decode (0b000001 : (regno) rs : 0b00011 : (imm16) imm) = 
+function clause decode (0b000001 : (regno) rs : 0b00011 : (imm16) imm) =
   Some(BCMPZ(rs, imm, GE, false, true))  (* BGEZL *)
-function clause decode (0b000001 : (regno) rs : 0b10011 : (imm16) imm) = 
+function clause decode (0b000001 : (regno) rs : 0b10011 : (imm16) imm) =
   Some(BCMPZ(rs, imm, GE, true, true))   (* BGEZALL *)
 
-function clause decode (0b000111 : (regno) rs : 0b00000 : (imm16) imm) = 
+function clause decode (0b000111 : (regno) rs : 0b00000 : (imm16) imm) =
   Some(BCMPZ(rs, imm, GT, false, false)) (* BGTZ *)
-function clause decode (0b010111 : (regno) rs : 0b00000 : (imm16) imm) = 
+function clause decode (0b010111 : (regno) rs : 0b00000 : (imm16) imm) =
   Some(BCMPZ(rs, imm, GT, false, true))  (* BGTZL *)
 
-function clause decode (0b000110 : (regno) rs : 0b00000 : (imm16) imm) = 
+function clause decode (0b000110 : (regno) rs : 0b00000 : (imm16) imm) =
   Some(BCMPZ(rs, imm, LE, false, false)) (* BLEZ *)
-function clause decode (0b010110 : (regno) rs : 0b00000 : (imm16) imm) = 
+function clause decode (0b010110 : (regno) rs : 0b00000 : (imm16) imm) =
   Some(BCMPZ(rs, imm, LE, false, true))  (* BLEZL *)
 
 function clause execute (BCMPZ(rs, imm, cmp, link, likely)) =
@@ -1003,7 +1003,7 @@ function clause execute (BCMPZ(rs, imm, cmp, link, likely)) =
         nextPC := PC + 8  (* skip branch delay *)
       };
     if (link) then
-      wGPR(31) := linkVal
+      wGPR(0b11111) := linkVal
   }
 
 (**************************************************************************************)
@@ -1051,17 +1051,17 @@ function clause execute (WAIT) = {
 
 (* Trap instructions with two register operands *)
 union ast member (regno, regno, Comparison) TRAPREG
-function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110000) = 
+function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110000) =
   Some(TRAPREG(rs, rt, GE)) (* TGE *)
-function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110001) = 
+function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110001) =
   Some(TRAPREG(rs, rt, GEU)) (* TGEU *)
-function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110010) = 
+function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110010) =
   Some(TRAPREG(rs, rt, LT)) (* TLT *)
-function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110011) = 
+function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110011) =
   Some(TRAPREG(rs, rt, LTU)) (* TLTU *)
-function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110100) = 
+function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110100) =
   Some(TRAPREG(rs, rt, EQ)) (* TEQ *)
-function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110110) = 
+function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110110) =
   Some(TRAPREG(rs, rt, NE)) (* TNE *)
 function clause execute (TRAPREG(rs, rt, cmp)) =
   {
@@ -1075,22 +1075,22 @@ function clause execute (TRAPREG(rs, rt, cmp)) =
 
 (* Trap instructions with one register and one immediate operand *)
 union ast member (regno, imm16, Comparison) TRAPIMM
-function clause decode (0b000001 : (regno) rs : 0b01100 : (imm16) imm) = 
+function clause decode (0b000001 : (regno) rs : 0b01100 : (imm16) imm) =
   Some(TRAPIMM(rs, imm, EQ)) (* TEQI *)
-function clause decode (0b000001 : (regno) rs : 0b01110 : (imm16) imm) = 
+function clause decode (0b000001 : (regno) rs : 0b01110 : (imm16) imm) =
   Some(TRAPIMM(rs, imm, NE)) (* TNEI *)
-function clause decode (0b000001 : (regno) rs : 0b01000 : (imm16) imm) = 
+function clause decode (0b000001 : (regno) rs : 0b01000 : (imm16) imm) =
   Some(TRAPIMM(rs, imm, GE)) (* TGEI *)
-function clause decode (0b000001 : (regno) rs : 0b01001 : (imm16) imm) = 
+function clause decode (0b000001 : (regno) rs : 0b01001 : (imm16) imm) =
   Some(TRAPIMM(rs, imm, GEU)) (* TGEIU *)
-function clause decode (0b000001 : (regno) rs : 0b01010 : (imm16) imm) = 
+function clause decode (0b000001 : (regno) rs : 0b01010 : (imm16) imm) =
   Some(TRAPIMM(rs, imm, LT))  (* TLTI *)
-function clause decode (0b000001 : (regno) rs : 0b01011 : (imm16) imm) = 
+function clause decode (0b000001 : (regno) rs : 0b01011 : (imm16) imm) =
   Some(TRAPIMM(rs, imm, LTU)) (* TLTIU *)
 function clause execute (TRAPIMM(rs, imm, cmp)) =
   {
     rs_val := rGPR(rs);
-    imm_val := EXTS(imm);
+    (bit[64]) imm_val := EXTS(imm);
     condition := compare(cmp, rs_val, imm_val);
     if (condition) then
       (SignalException(Tr))
@@ -1101,23 +1101,23 @@ function clause execute (TRAPIMM(rs, imm, cmp)) =
 (**************************************************************************************)
 
 union ast member (WordType, bool, bool, regno, regno, imm16) Load
-function clause decode (0b100000 : (regno) base : (regno) rt : (imm16) offset) = 
+function clause decode (0b100000 : (regno) base : (regno) rt : (imm16) offset) =
   Some(Load(B, true,  false, base, rt, offset)) (* LB *)
-function clause decode (0b100100 : (regno) base : (regno) rt : (imm16) offset) = 
+function clause decode (0b100100 : (regno) base : (regno) rt : (imm16) offset) =
   Some(Load(B, false, false, base, rt, offset)) (* LBU *)
-function clause decode (0b100001 : (regno) base : (regno) rt : (imm16) offset) = 
+function clause decode (0b100001 : (regno) base : (regno) rt : (imm16) offset) =
   Some(Load(H, true,  false, base, rt, offset)) (* LH *)
-function clause decode (0b100101 : (regno) base : (regno) rt : (imm16) offset) = 
+function clause decode (0b100101 : (regno) base : (regno) rt : (imm16) offset) =
   Some(Load(H, false, false, base, rt, offset)) (* LHU *)
-function clause decode (0b100011 : (regno) base : (regno) rt : (imm16) offset) = 
+function clause decode (0b100011 : (regno) base : (regno) rt : (imm16) offset) =
   Some(Load(W, true,  false, base, rt, offset)) (* LW *)
-function clause decode (0b100111 : (regno) base : (regno) rt : (imm16) offset) = 
+function clause decode (0b100111 : (regno) base : (regno) rt : (imm16) offset) =
   Some(Load(W, false, false, base, rt, offset)) (* LWU *)
-function clause decode (0b110111 : (regno) base : (regno) rt : (imm16) offset) = 
+function clause decode (0b110111 : (regno) base : (regno) rt : (imm16) offset) =
   Some(Load(D, false, false, base, rt, offset)) (* LD *)
-function clause decode (0b110000 : (regno) base : (regno) rt : (imm16) offset) = 
+function clause decode (0b110000 : (regno) base : (regno) rt : (imm16) offset) =
   Some(Load(W, true,  true, base, rt, offset))  (* LL *)
-function clause decode (0b110100 : (regno) base : (regno) rt : (imm16) offset) = 
+function clause decode (0b110100 : (regno) base : (regno) rt : (imm16) offset) =
   Some(Load(D, false, true, base, rt, offset))  (* LLD *)
 function clause execute (Load(width, signed, linked, base, rt, offset)) =
   {
@@ -1127,15 +1127,25 @@ function clause execute (Load(width, signed, linked, base, rt, offset)) =
     else
       let pAddr = (TLBTranslate(vAddr, LoadData)) in
           {
-            memResult := if (linked) then
+	    (bit[64]) memResult := if (linked) then
                 {
                   CP0LLBit  := 0b1;
-                  CP0LLAddr := pAddr;
-                  MEMr_reserve_wrapper(pAddr, wordWidthBytes(width));
+		  CP0LLAddr := pAddr;
+		  switch wordWidthBytes(width) {
+		    case ([:1:]) w -> MEMr_reserve_wrapper(pAddr, w)
+		    case ([:2:]) w -> MEMr_reserve_wrapper(pAddr, w)
+		    case ([:4:]) w -> MEMr_reserve_wrapper(pAddr, w)
+		    case ([:8:]) w -> MEMr_reserve_wrapper(pAddr, w)
+		  }
                 }
               else
-                MEMr_wrapper(pAddr, wordWidthBytes(width));
-            if (signed) then
+		switch wordWidthBytes(width) {
+		  case ([:1:]) w -> MEMr_reserve_wrapper(pAddr, w)
+		  case ([:2:]) w -> MEMr_reserve_wrapper(pAddr, w)
+		  case ([:4:]) w -> MEMr_reserve_wrapper(pAddr, w)
+		  case ([:8:]) w -> MEMr_reserve_wrapper(pAddr, w)
+		};
+	    if (signed) then
               wGPR(rt) := EXTS(memResult)
             else
               wGPR(rt) := EXTZ(memResult)
@@ -1147,17 +1157,17 @@ function clause execute (Load(width, signed, linked, base, rt, offset)) =
 (**************************************************************************************)
 
 union ast member (WordType, bool, regno, regno, imm16) Store
-function clause decode (0b101000 : (regno) base : (regno) rt : (imm16) offset) = 
+function clause decode (0b101000 : (regno) base : (regno) rt : (imm16) offset) =
   Some(Store(B, false, base, rt, offset)) (* SB *)
-function clause decode (0b101001 : (regno) base : (regno) rt : (imm16) offset) = 
+function clause decode (0b101001 : (regno) base : (regno) rt : (imm16) offset) =
   Some(Store(H, false, base, rt, offset)) (* SH *)
-function clause decode (0b101011 : (regno) base : (regno) rt : (imm16) offset) = 
+function clause decode (0b101011 : (regno) base : (regno) rt : (imm16) offset) =
   Some(Store(W, false, base, rt, offset)) (* SW *)
-function clause decode (0b111111 : (regno) base : (regno) rt : (imm16) offset) = 
+function clause decode (0b111111 : (regno) base : (regno) rt : (imm16) offset) =
   Some(Store(D, false, base, rt, offset)) (* SD *)
-function clause decode (0b111000 : (regno) base : (regno) rt : (imm16) offset) = 
+function clause decode (0b111000 : (regno) base : (regno) rt : (imm16) offset) =
   Some(Store(W, true, base, rt, offset))  (* SC *)
-function clause decode (0b111100 : (regno) base : (regno) rt : (imm16) offset) = 
+function clause decode (0b111100 : (regno) base : (regno) rt : (imm16) offset) =
   Some(Store(D, true, base, rt, offset))  (* SCD *)
 function clause execute (Store(width, conditional, base, rt, offset)) =
       {
@@ -1170,14 +1180,14 @@ function clause execute (Store(width, conditional, base, rt, offset)) =
           {
                 if (conditional) then
                   {
-                    success := if (CP0LLBit[0]) then switch(width)
+		    success := if (CP0LLBit[0]) then (bool) switch(width)
                     {
                       case B -> MEMw_conditional_wrapper(pAddr, 1, rt_val[7..0])
                       case H -> MEMw_conditional_wrapper(pAddr, 2, rt_val[15..0])
                       case W -> MEMw_conditional_wrapper(pAddr, 4, rt_val[31..0])
                       case D -> MEMw_conditional_wrapper(pAddr, 8, rt_val)
                     } else false;
-                    wGPR(rt) := EXTZ([success])
+		    wGPR(rt) := EXTZ([bool_to_bit(success)])
                   }
                 else
                   switch(width)
@@ -1195,7 +1205,7 @@ function clause execute (Store(width, conditional, base, rt, offset)) =
 union ast member regregimm16 LWL
 function clause decode(0b100010 : (regno) base : (regno) rt : (imm16) offset) =
       Some(LWL(base, rt, offset))
-function clause execute(LWL(base, rt, offset)) = 
+function clause execute(LWL(base, rt, offset)) =
       {
         (* XXX length check not quite right, but conservative *)
         (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), LoadData, W);
@@ -1203,19 +1213,19 @@ function clause execute(LWL(base, rt, offset)) =
           {
             mem_val   := MEMr_wrapper (pAddr[63..2] : 0b00, 4); (* read word of interest *)
             reg_val   := rGPR(rt);
-            wGPR(rt)  := EXTS(switch(vAddr[1..0])
+	    wGPR(rt)  := EXTS((bit[32]) switch(vAddr[1..0])
               {
                 case 0b00 -> mem_val
                 case 0b01 -> mem_val[23..0] : reg_val[07..0]
                 case 0b10 -> mem_val[15..0] : reg_val[15..0]
                 case 0b11 -> mem_val[07..0] : reg_val[23..0]
-              });
+	      });
           }
       }
 union ast member regregimm16 LWR
 function clause decode(0b100110 : (regno) base : (regno) rt : (imm16) offset) =
       Some(LWR(base, rt, offset))
-function clause execute(LWR(base, rt, offset)) = 
+function clause execute(LWR(base, rt, offset)) =
       {
         (* XXX length check not quite right, but conservative *)
         (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), LoadData, W);
@@ -1223,7 +1233,7 @@ function clause execute(LWR(base, rt, offset)) =
           {
             mem_val   := MEMr_wrapper (pAddr[63..2] : 0b00, 4); (* read word of interest *)
             reg_val   := rGPR(rt);
-            wGPR(rt)  := EXTS(switch(vAddr[1..0]) (* it is acceptable to sign extend in all cases *)
+	    wGPR(rt)  := EXTS((bit[32]) switch(vAddr[1..0]) (* it is acceptable to sign extend in all cases *)
               {
                 case 0b00 -> reg_val[31..8]  : mem_val[31..24]
                 case 0b01 -> reg_val[31..16] : mem_val[31..16]
@@ -1237,7 +1247,7 @@ function clause execute(LWR(base, rt, offset)) =
 union ast member regregimm16 SWL
 function clause decode(0b101010 : (regno) base : (regno) rt : (imm16) offset) =
       Some(SWL(base, rt, offset))
-function clause execute(SWL(base, rt, offset)) = 
+function clause execute(SWL(base, rt, offset)) =
       {
         (* XXX length check not quite right, but conservative *)
         (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), StoreData, W);
@@ -1257,7 +1267,7 @@ function clause execute(SWL(base, rt, offset)) =
 union ast member regregimm16 SWR
 function clause decode(0b101110 : (regno) base : (regno) rt : (imm16) offset) =
       Some(SWR(base, rt, offset))
-function clause execute(SWR(base, rt, offset)) = 
+function clause execute(SWR(base, rt, offset)) =
       {
         (* XXX length check not quite right, but conservative *)
         (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), StoreData, W);
@@ -1279,7 +1289,7 @@ function clause execute(SWR(base, rt, offset)) =
 union ast member regregimm16 LDL
 function clause decode(0b011010 : (regno) base : (regno) rt : (imm16) offset) =
   Some(LDL(base, rt, offset))
-function clause execute(LDL(base, rt, offset)) = 
+function clause execute(LDL(base, rt, offset)) =
   {
     (* XXX length check not quite right, but conservative *)
     (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), LoadData, D);
@@ -1305,7 +1315,7 @@ function clause execute(LDL(base, rt, offset)) =
 union ast member regregimm16 LDR
 function clause decode(0b011011 : (regno) base : (regno) rt : (imm16) offset) =
   Some(LDR(base, rt, offset))
-function clause execute(LDR(base, rt, offset)) = 
+function clause execute(LDR(base, rt, offset)) =
   {
     (* XXX length check not quite right, but conservative *)
     (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), LoadData, D);
@@ -1331,7 +1341,7 @@ function clause execute(LDR(base, rt, offset)) =
 union ast member regregimm16 SDL
 function clause decode(0b101100 : (regno) base : (regno) rt : (imm16) offset) =
       Some(SDL(base, rt, offset))
-function clause execute(SDL(base, rt, offset)) = 
+function clause execute(SDL(base, rt, offset)) =
       {
         (* XXX length check not quite right, but conservative *)
         (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), StoreData, D);
@@ -1357,7 +1367,7 @@ function clause execute(SDL(base, rt, offset)) =
 union ast member regregimm16 SDR
 function clause decode(0b101101 : (regno) base : (regno) rt : (imm16) offset) =
       Some(SDR(base, rt, offset))
-function clause execute(SDR(base, rt, offset)) = 
+function clause execute(SDR(base, rt, offset)) =
   {
         (* XXX length check not quite right, but conservative *)
         (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), StoreData, D);
@@ -1384,7 +1394,7 @@ function clause execute(SDR(base, rt, offset)) =
 union ast member regregimm16 CACHE
 function clause decode (0b101111 : (regno) base : (regno) op : (imm16) imm) =
   Some(CACHE(base, op, imm))
-function clause execute (CACHE(base, op, imm)) = 
+function clause execute (CACHE(base, op, imm)) =
   checkCP0Access () (* pretty much a NOP because no caches *)
 
 (* PREF - prefetching into (non-existent) caches *)
@@ -1398,7 +1408,7 @@ function clause execute (PREF(base, op, imm)) =
 
 (* SYNC  - Memory barrier *)
 union ast member unit SYNC
-function clause decode (0b000000 : 0b00000 : 0b00000 : 0b00000 : (regno) stype : 0b001111) = 
+function clause decode (0b000000 : 0b00000 : 0b00000 : 0b00000 : (regno) stype : 0b001111) =
   Some((ast) SYNC) (* stype is currently ignored *)
 function clause execute(SYNC) =
   MEM_sync()
@@ -1413,7 +1423,7 @@ function clause execute (MFC0(rt, rd, sel, double)) = {
   let (bit[64]) result = switch (rd, sel)
         {
           case (0b00000,0b000) -> let (bit[31]) idx = EXTZ(TLBIndex) in
-                                  (0x00000000 : [TLBProbe] : idx)  (* 0, TLB Index *)
+				  (0x00000000 : TLBProbe : idx)  (* 0, TLB Index *)
           case (0b00001,0b000) -> EXTZ(TLBRandom)  (* 1, TLB Random *)
           case (0b00010,0b000) -> TLBEntryLo0      (* 2, TLB EntryLo0 *)
           case (0b00011,0b000) -> TLBEntryLo1      (* 3, TLB EntryLo1 *)
@@ -1433,9 +1443,9 @@ function clause execute (MFC0(rt, rd, sel, double)) = {
           case (0b01111,0b110) -> 0                (* 15, sel 6: CHERI core ID *)
           case (0b01111,0b111) -> 0                (* 15, sel 7: CHERI thread ID *)
           case (0b10000,0b000) -> EXTZ(0b1 (* M *)      (* 16, sel 0: Config0 *)
-                                  : 0b000000000000000 (* Impl *) 
-                                  : 0b1               (* BE *) 
-                                  : 0b10              (* AT *) 
+                                  : 0b000000000000000 (* Impl *)
+                                  : 0b1               (* BE *)
+                                  : 0b10              (* AT *)
                                   : 0b000             (* AR *)
                                   : 0b001             (* MT standard TLB *)
                                   : 0b0000            (* zero *)
@@ -1449,7 +1459,7 @@ function clause execute (MFC0(rt, rd, sel, double)) = {
                                          : 0b000    (* DS dcache sets *)
                                          : 0b000    (* DL dcache lines *)
                                          : 0b000    (* DA dcache assoc. *)
-                                         : [have_cp2] (* C2 CP2 presence *)
+					 : [bool_to_bit(have_cp2)] (* C2 CP2 presence *)
                                          : 0b0      (* MD MDMX implemented *)
                                          : 0b0      (* PC performance counters *)
                                          : 0b0      (* WR watch registers *)
@@ -1476,7 +1486,7 @@ function clause execute (MFC0(rt, rd, sel, double)) = {
           case _               -> (SignalException(ResI))
         } in
   wGPR(rt) := if (double) then result else EXTS(result[31..0])
-}  
+}
 
 (* simulator halt instruction "MTC0 rt, r23" (cheri specific behaviour) *)
 union ast member unit HCF
@@ -1519,7 +1529,7 @@ function clause execute (MTC0(rt, rd, sel, double)) = {
         (TLBEntryHi.ASID) := (reg_val[7..0]);
       }
       case (0b01011,0b000) -> {  (* 11, sel 0: Compare reg *)
-        CP0Compare := reg_val[31..0]; 
+	CP0Compare := reg_val[31..0];
         (CP0Cause[15]) := bitzero;
       }
       case (0b01100,0b000) -> {  (* 12 Status *)
@@ -1546,7 +1556,7 @@ function clause execute (MTC0(rt, rd, sel, double)) = {
       case _               -> (SignalException(ResI))
     }
 }
-(*
+
 function unit TLBWriteEntry((TLBIndexT) idx) = {
   pagemask := (bit[16]) (EXTZ(TLBPageMask)); (* XXX EXTZ here forces register read in ocaml shallow embedding *)
   switch(pagemask) {
@@ -1561,26 +1571,28 @@ function unit TLBWriteEntry((TLBIndexT) idx) = {
       case 0xffff -> ()
       case _      -> (SignalException(MCheck))
   };
-  ((TLBEntries[idx]).pagemask) := pagemask;
-  ((TLBEntries[idx]).r       ) := TLBEntryHi.R;
-  ((TLBEntries[idx]).vpn2    ) := TLBEntryHi.VPN2;
-  ((TLBEntries[idx]).asid    ) := TLBEntryHi.ASID;
-  ((TLBEntries[idx]).g       ) := ((TLBEntryLo0.G) & (TLBEntryLo1.G));
-  ((TLBEntries[idx]).valid   ) := bitone;
-  ((TLBEntries[idx]).caps0   ) := TLBEntryLo0.CapS;
-  ((TLBEntries[idx]).capl0   ) := TLBEntryLo0.CapL;
-  ((TLBEntries[idx]).pfn0    ) := TLBEntryLo0.PFN;
-  ((TLBEntries[idx]).c0      ) := TLBEntryLo0.C;
-  ((TLBEntries[idx]).d0      ) := TLBEntryLo0.D;
-  ((TLBEntries[idx]).v0      ) := TLBEntryLo0.V;
-  ((TLBEntries[idx]).caps1   ) := TLBEntryLo1.CapS;
-  ((TLBEntries[idx]).capl1   ) := TLBEntryLo1.CapL;
-  ((TLBEntries[idx]).pfn1    ) := TLBEntryLo1.PFN;
-  ((TLBEntries[idx]).c1      ) := TLBEntryLo1.C;
-  ((TLBEntries[idx]).d1      ) := TLBEntryLo1.D;
-  ((TLBEntries[idx]).v1      ) := TLBEntryLo1.V;
+  let idxr = unsigned(idx) in {
+  ((TLBEntries[idxr]).pagemask) := pagemask;
+  ((TLBEntries[idxr]).r       ) := TLBEntryHi.R;
+  ((TLBEntries[idxr]).vpn2    ) := TLBEntryHi.VPN2;
+  ((TLBEntries[idxr]).asid    ) := TLBEntryHi.ASID;
+  ((TLBEntries[idxr]).g       ) := ((TLBEntryLo0.G) & (TLBEntryLo1.G));
+  ((TLBEntries[idxr]).valid   ) := bitone;
+  ((TLBEntries[idxr]).caps0   ) := TLBEntryLo0.CapS;
+  ((TLBEntries[idxr]).capl0   ) := TLBEntryLo0.CapL;
+  ((TLBEntries[idxr]).pfn0    ) := TLBEntryLo0.PFN;
+  ((TLBEntries[idxr]).c0      ) := TLBEntryLo0.C;
+  ((TLBEntries[idxr]).d0      ) := TLBEntryLo0.D;
+  ((TLBEntries[idxr]).v0      ) := TLBEntryLo0.V;
+  ((TLBEntries[idxr]).caps1   ) := TLBEntryLo1.CapS;
+  ((TLBEntries[idxr]).capl1   ) := TLBEntryLo1.CapL;
+  ((TLBEntries[idxr]).pfn1    ) := TLBEntryLo1.PFN;
+  ((TLBEntries[idxr]).c1      ) := TLBEntryLo1.C;
+  ((TLBEntries[idxr]).d1      ) := TLBEntryLo1.D;
+  ((TLBEntries[idxr]).v1      ) := TLBEntryLo1.V;
+  }
 }
-*)
+
 union ast member TLBWI
 function clause decode (0b010000 : 0b10000000000000000000 : 0b000010) = Some((ast) TLBWI)
 function clause execute (TLBWI) = {
@@ -1599,7 +1611,7 @@ union ast member TLBR
 function clause decode (0b010000 : 0b10000000000000000000 : 0b000001) = Some((ast) TLBR)
 function clause execute (TLBR) = {
   checkCP0Access();
-  let entry = TLBEntries[TLBIndex] in {
+  let entry = TLBEntries[unsigned(TLBIndex)] in {
     TLBPageMask     := entry.pagemask;
     TLBEntryHi.R    := entry.r;
     TLBEntryHi.VPN2 := entry.vpn2;
@@ -1633,17 +1645,17 @@ function clause execute ((TLBP)) = {
     }
     case None -> {
       TLBProbe := [bitone];
-      TLBIndex := 0;
+      TLBIndex := 0b000000;
     }
   }
 }
 
 union ast member (regno, regno) RDHWR
-function clause decode (0b011111 : 0b00000 : (regno) rt : (regno) rd : 0b00000 : 0b111011) = 
+function clause decode (0b011111 : 0b00000 : (regno) rt : (regno) rd : 0b00000 : 0b111011) =
   Some(RDHWR(rt, rd))
 function clause execute (RDHWR(rt, rd)) = {
   let accessLevel = getAccessLevel() in
-  if ((accessLevel != Kernel) & (~((CP0Status.CU)[0])) & ~(CP0HWREna[rd])) then
+  if ((accessLevel != Kernel) & (~((CP0Status.CU)[28])) & ~(CP0HWREna[rd])) then
     (SignalException(ResI));
   let (bit[64]) temp = switch (rd) {
     case 0b00000 -> EXTZ([bitzero])  (* CPUNum *)
diff --git a/mips_new_tc/mips_wrappers.sail b/mips_new_tc/mips_wrappers.sail
index cdb4316c..5b36983d 100644
--- a/mips_new_tc/mips_wrappers.sail
+++ b/mips_new_tc/mips_wrappers.sail
@@ -35,8 +35,10 @@
 (* mips_wrappers.sail: wrappers functions and hooks for CHERI extensibility 
    (mostly identity functions here) *)
 
-function unit effect {wmem} MEMw_wrapper((bit[64]) addr, ([:8:]) size, (bit[64]) data) =
-    let ledata = reverse_endianness'(8, data) in
+val forall Nat 'n, 'n >= 1, 'n <= 8. (bit[64], [:'n:], bit[8 * 'n]) -> unit effect {eamem, wmv, wreg} MEMw_wrapper
+
+function unit MEMw_wrapper((bit[64]) addr, ([:'n:]) size, (bit[8 * 'n]) data) =
+    let ledata = reverse_endianness'(sizeof 'n, data) in
     if (addr == 0x000000007f000000) then
       {
         UART_WDATA   := ledata[7..0];
@@ -46,10 +48,12 @@ function unit effect {wmem} MEMw_wrapper((bit[64]) addr, ([:8:]) size, (bit[64])
         MEMval(addr, size, ledata);
       }
 
-function bool effect {wmem} MEMw_conditional_wrapper((bit[64]) addr, ([:8:]) size, (bit[64]) data) =
+val forall Nat 'n, 'n >= 1, 'n <= 8. (bit[64], [:'n:], bit[8 * 'n]) -> bool effect {eamem, wmv} MEMw_conditional_wrapper
+
+function bool MEMw_conditional_wrapper(addr, size, data) =
     {
       MEMea_conditional(addr, size);
-      MEMval_conditional(addr, size, reverse_endianness'(8, data))
+      MEMval_conditional(addr, size, reverse_endianness'(sizeof 'n, data))
     }
 
 function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordType) width) =
diff --git a/src/ast_util.ml b/src/ast_util.ml
index d41ef180..22746ed1 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -294,6 +294,7 @@ and string_of_lexp (LEXP_aux (lexp, _)) =
   | LEXP_tup lexps -> "(" ^ string_of_list ", " string_of_lexp lexps ^ ")"
   | LEXP_vector (lexp, exp) -> string_of_lexp lexp ^ "[" ^ string_of_exp exp ^ "]"
   | LEXP_field (lexp, id) -> string_of_lexp lexp ^ "." ^ string_of_id id
+  | LEXP_memory (f, xs) -> string_of_id f ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")"
   | _ -> "LEXP"
 and string_of_letbind (LB_aux (lb, l)) =
   match lb with
diff --git a/src/type_check_new.ml b/src/type_check_new.ml
index 5be2cd43..b696e6d2 100644
--- a/src/type_check_new.ml
+++ b/src/type_check_new.ml
@@ -723,13 +723,13 @@ end = struct
     then typ_error (id_loc id) ("Type synonym " ^ string_of_id id ^ " already exists")
     else
       begin
-        typ_debug ("Adding type synonym " ^ string_of_id id);
+        typ_print ("Adding type synonym " ^ string_of_id id);
         { env with typ_synonyms = Bindings.add id synonym env.typ_synonyms }
       end
 
   let get_typ_synonym id env = Bindings.find id env.typ_synonyms
 
-  let rec expand_synonyms env (Typ_aux (typ, l)) =
+  let rec expand_synonyms env (Typ_aux (typ, l) as t) =
     match typ with
     | Typ_tup typs -> Typ_aux (Typ_tup (List.map (expand_synonyms env) typs), l)
     | Typ_fn (typ1, typ2, effs) -> Typ_aux (Typ_fn (expand_synonyms env typ1, expand_synonyms env typ2, effs), l)
@@ -1773,13 +1773,35 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as
   let annot_assign lexp exp = E_aux (E_assign (lexp, exp), (l, Some (env, mk_typ (Typ_id (mk_id "unit")), no_effect))) in
   let annot_lexp_effect lexp typ eff = LEXP_aux (lexp, (l, Some (env, typ, eff))) in
   let annot_lexp lexp typ = annot_lexp_effect lexp typ no_effect in
+  let has_typ v env =
+    match Env.lookup_id v env with
+    | Local (Mutable, _) | Register _ -> true
+    | _ -> false
+  in
   match lexp_aux with
-  | LEXP_field (LEXP_aux (LEXP_id v, _), field) ->
+  | LEXP_field (LEXP_aux (flexp, _), field) ->
      begin
-       let regtyp = match Env.lookup_id v env with
-         | Register typ -> typ
-         | _ -> typ_error l "l-expression field is not a register"
+       let infer_flexp = function
+         | LEXP_id v ->
+            begin match Env.lookup_id v env with
+            | Register typ -> typ, LEXP_id v
+            | _ -> typ_error l "l-expression field is not a register"
+            end
+         | LEXP_vector (LEXP_aux (LEXP_id v, _), exp) ->
+            begin
+              (* Check: is this ok if the vector is immutable? *)
+              let is_immutable, vtyp = match Env.lookup_id v env with
+                | Unbound -> typ_error l "Cannot assign to element of unbound vector"
+                | Enum _ -> typ_error l "Cannot vector assign to enumeration element"
+                | Local (Immutable, vtyp) -> true, vtyp
+                | Local (Mutable, vtyp) | Register vtyp -> false, vtyp
+              in
+              let access = infer_exp (Env.enable_casts env) (E_aux (E_app (mk_id "vector_access", [E_aux (E_id v, (l, ())); exp]), (l, ()))) in
+              let E_aux (E_app (_, [_; inferred_exp]), _) = access in
+              typ_of access, LEXP_vector (annot_lexp (LEXP_id v) vtyp, inferred_exp)
+            end
        in
+       let regtyp, inferred_flexp = infer_flexp flexp in
        match Env.expand_synonyms env regtyp with
        | Typ_aux (Typ_id regtyp_id, _) when Env.is_regtyp regtyp_id env ->
           let base, top, ranges = Env.get_regtyp regtyp_id env in
@@ -1795,7 +1817,7 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as
             | _, _ -> typ_error l "Not implemented this register field type yet..."
           in
           let checked_exp = crule check_exp env exp vec_typ in
-          annot_assign (annot_lexp (LEXP_field (annot_lexp_effect (LEXP_id v) regtyp (mk_effect [BE_wreg]), field)) vec_typ) checked_exp, env
+          annot_assign (annot_lexp (LEXP_field (annot_lexp_effect inferred_flexp regtyp (mk_effect [BE_wreg]), field)) vec_typ) checked_exp, env
        | _ ->  typ_error l "Field l-expression has invalid type"
      end
   | LEXP_memory (f, xs) ->
@@ -1804,6 +1826,14 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as
      let checked_exp = crule check_exp env exp typ_annot in
      let tlexp, env' = bind_lexp env lexp (typ_of checked_exp) in
      annot_assign tlexp checked_exp, env'
+  | LEXP_id v when has_typ v env ->
+     begin match Env.lookup_id v env with
+     | Local (Mutable, vtyp) | Register vtyp ->
+        let checked_exp = crule check_exp env exp vtyp in
+        let tlexp, env' = bind_lexp env lexp (typ_of checked_exp) in
+        annot_assign tlexp checked_exp, env'
+     | _ -> assert false
+     end
   | _ ->
      let inferred_exp = irule infer_exp env exp in
      let tlexp, env' = bind_lexp env lexp (typ_of inferred_exp) in
@@ -1814,13 +1844,12 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
   let annot_lexp lexp typ = annot_lexp_effect lexp typ no_effect in
   match lexp_aux with
   | LEXP_id v ->
-     begin
-       match Env.lookup_id v env with
-       | Local (Immutable, _) | Enum _ ->
-          typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v)
-       | Local (Mutable, vtyp) -> subtyp l env typ vtyp; annot_lexp (LEXP_id v) typ, env
-       | Register vtyp -> subtyp l env typ vtyp; annot_lexp_effect (LEXP_id v) typ (mk_effect [BE_wreg]), env
-       | Unbound -> annot_lexp (LEXP_id v) typ, Env.add_local v (Mutable, typ) env
+     begin match Env.lookup_id v env with
+     | Local (Immutable, _) | Enum _ ->
+        typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v)
+     | Local (Mutable, vtyp) -> subtyp l env typ vtyp; annot_lexp (LEXP_id v) typ, env
+     | Register vtyp -> subtyp l env typ vtyp; annot_lexp_effect (LEXP_id v) typ (mk_effect [BE_wreg]), env
+     | Unbound -> annot_lexp (LEXP_id v) typ, Env.add_local v (Mutable, typ) env
      end
   | LEXP_cast (typ_annot, v) ->
      begin
@@ -2423,11 +2452,16 @@ let check_register env id base top ranges =
   | Nexp_aux (Nexp_constant basec, _), Nexp_aux (Nexp_constant topc, _) ->
      let no_typq = TypQ_aux (TypQ_tq [], Parse_ast.Unknown) (* Maybe could be TypQ_no_forall? *) in
      (* FIXME: wrong for default Order inc? *)
-     let cast_typ = mk_typ (Typ_fn (mk_id_typ id, dvector_typ env base (nconstant ((basec - topc) + 1)) bit_typ, no_effect)) in
+     let vec_typ = dvector_typ env base (nconstant ((basec - topc) + 1)) bit_typ in
+     let cast_typ = mk_typ (Typ_fn (mk_id_typ id, vec_typ, no_effect)) in
+     let cast_to_typ = mk_typ (Typ_fn (vec_typ, mk_id_typ id, no_effect)) in
      env
      |> Env.add_regtyp id basec topc ranges
+  (* |> Env.add_typ_synonym id (fun _ -> vec_typ) *)
      |> Env.add_val_spec (mk_id ("cast_" ^ string_of_id id)) (no_typq, cast_typ)
      |> Env.add_cast (mk_id ("cast_" ^ string_of_id id))
+     |> Env.add_val_spec (mk_id ("cast_to_" ^ string_of_id id)) (no_typq, cast_to_typ)
+     |> Env.add_cast (mk_id ("cast_to_" ^ string_of_id id))
   | _, _ -> typ_error (id_loc id) "Num expressions in register type declaration do not evaluate to constants"
 
 let kinded_id_arg kind_id =
diff --git a/test/typecheck/run_tests.sh b/test/typecheck/run_tests.sh
index 5172142d..6ce2d5c8 100755
--- a/test/typecheck/run_tests.sh
+++ b/test/typecheck/run_tests.sh
@@ -15,9 +15,12 @@ mkdir -p $DIR/rtfail
 
 rm -f $DIR/tests.xml
 
-cat $SAILDIR/lib/prelude.sail $SAILDIR/mips_new_tc/mips_prelude.sail > $DIR/pass/mips_prelude.sail
-cat $SAILDIR/lib/prelude.sail $SAILDIR/mips_new_tc/mips_prelude.sail $SAILDIR/mips_new_tc/mips_tlb.sail > $DIR/pass/mips_tlb.sail
-cat $SAILDIR/lib/prelude.sail $SAILDIR/mips_new_tc/mips_prelude.sail $SAILDIR/mips_new_tc/mips_tlb.sail $SAILDIR/mips_new_tc/mips_wrappers.sail > $DIR/pass/mips_wrappers.sail
+MIPS="$SAILDIR/mips_new_tc"
+
+cat $SAILDIR/lib/prelude.sail $MIPS/mips_prelude.sail > $DIR/pass/mips_prelude.sail
+cat $SAILDIR/lib/prelude.sail $MIPS/mips_prelude.sail $MIPS/mips_tlb.sail > $DIR/pass/mips_tlb.sail
+cat $SAILDIR/lib/prelude.sail $MIPS/mips_prelude.sail $MIPS/mips_tlb.sail $MIPS/mips_wrappers.sail > $DIR/pass/mips_wrappers.sail
+cat $SAILDIR/lib/prelude.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
 
 pass=0
 fail=0