Improve formatting of latex export of mips spec: wrap lines, remove dollars in comments. No functional change.

4 files changed, 131 insertions, 67 deletions

diff --git a/mips/mips_epilogue.sail b/mips/mips_epilogue.sail
index 710c277b..6b789639 100644
--- a/mips/mips_epilogue.sail
+++ b/mips/mips_epilogue.sail
@@ -32,6 +32,8 @@
 (*  SUCH DAMAGE.                                                          *)
 (*========================================================================*)
 
+(* mips_epilogue.sail: end of decode, execute and AST definitions. *)
+
 union ast member unit RI
 function clause decode _ = Some(RI)
 function clause execute (RI) =
diff --git a/mips/mips_insts.sail b/mips/mips_insts.sail
index 97a280d4..a6cef9ca 100644
--- a/mips/mips_insts.sail
+++ b/mips/mips_insts.sail
@@ -32,6 +32,9 @@
 (*  SUCH DAMAGE.                                                          *)
 (*========================================================================*)
 
+(* misp_insts.sail: mips instruction decode and execute clauses and AST node 
+   declarations *)
+
 scattered function unit execute
 scattered typedef ast = const union
 
@@ -920,10 +923,14 @@ 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) =  Some(BEQ(rs, rt, imm, false, false))  (* BEQ  *)
-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) =  Some(BEQ(rs, rt, imm, true , false))  (* BNE  *)
-function clause decode (0b010101 : (regno) rs : (regno) rt : (imm16) imm) =  Some(BEQ(rs, rt, imm, true , true))   (* BNEL *)
+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) = 
+  Some(BEQ(rs, rt, imm, false, true))   (* BEQL *)
+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) = 
+  Some(BEQ(rs, rt, imm, true , true))   (* BNEL *)
 function clause execute (BEQ(rs, rd, imm, ne, likely)) =
   {
     if ((rGPR(rs) == rGPR(rd)) ^ ne) then
@@ -950,21 +957,33 @@ 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) = Some(BCMPZ(rs, imm, LT, false, false)) (* BLTZ *)
-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) = Some(BCMPZ(rs, imm, LT, false, true))  (* BLTZL *)
-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) = Some(BCMPZ(rs, imm, GE, false, false)) (* BGEZ *)
-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) = Some(BCMPZ(rs, imm, GE, false, true))  (* BGEZL *)
-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) = Some(BCMPZ(rs, imm, GT, false, false)) (* BGTZ *)
-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) = Some(BCMPZ(rs, imm, LE, false, false)) (* BLEZ *)
-function clause decode (0b010110 : (regno) rs : 0b00000 : (imm16) imm) = Some(BCMPZ(rs, imm, LE, false, true))  (* BLEZL *)
+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) = 
+  Some(BCMPZ(rs, imm, LT, true, false))  (* BLTZAL *)
+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) = 
+  Some(BCMPZ(rs, imm, LT, true, true))   (* BLTZALL *)
+
+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) = 
+  Some(BCMPZ(rs, imm, GE, true, false))  (* BGEZAL *)
+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) = 
+  Some(BCMPZ(rs, imm, GE, true, true))   (* BGEZALL *)
+
+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) = 
+  Some(BCMPZ(rs, imm, GT, false, true))  (* BGTZL *)
+
+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) = 
+  Some(BCMPZ(rs, imm, LE, false, true))  (* BLEZL *)
 
 function clause execute (BCMPZ(rs, imm, cmp, link, likely)) =
   {
@@ -1016,12 +1035,18 @@ 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) = Some(TRAPREG(rs, rt, GE)) (* TGE *)
-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) = Some(TRAPREG(rs, rt, LT)) (* TLT *)
-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) = Some(TRAPREG(rs, rt, EQ)) (* TEQ *)
-function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110110) = Some(TRAPREG(rs, rt, NE)) (* TNE *)
+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) = 
+  Some(TRAPREG(rs, rt, GEU)) (* TGEU *)
+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) = 
+  Some(TRAPREG(rs, rt, LTU)) (* TLTU *)
+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) = 
+  Some(TRAPREG(rs, rt, NE)) (* TNE *)
 function clause execute (TRAPREG(rs, rt, cmp)) =
   {
     rs_val := rGPR(rs);
@@ -1034,12 +1059,18 @@ 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) = Some(TRAPIMM(rs, imm, EQ)) (* TEQI *)
-function clause decode (0b000001 : (regno) rs : 0b01110 : (imm16) imm) = Some(TRAPIMM(rs, imm, NE)) (* TNEI *)
-function clause decode (0b000001 : (regno) rs : 0b01000 : (imm16) imm) = Some(TRAPIMM(rs, imm, GE)) (* TGEI *)
-function clause decode (0b000001 : (regno) rs : 0b01001 : (imm16) imm) = Some(TRAPIMM(rs, imm, GEU)) (* TGEIU *)
-function clause decode (0b000001 : (regno) rs : 0b01010 : (imm16) imm) = Some(TRAPIMM(rs, imm, LT))  (* TLTI *)
-function clause decode (0b000001 : (regno) rs : 0b01011 : (imm16) imm) = Some(TRAPIMM(rs, imm, LTU))  (* TLTIU *)
+function clause decode (0b000001 : (regno) rs : 0b01100 : (imm16) imm) = 
+  Some(TRAPIMM(rs, imm, EQ)) (* TEQI *)
+function clause decode (0b000001 : (regno) rs : 0b01110 : (imm16) imm) = 
+  Some(TRAPIMM(rs, imm, NE)) (* TNEI *)
+function clause decode (0b000001 : (regno) rs : 0b01000 : (imm16) imm) = 
+  Some(TRAPIMM(rs, imm, GE)) (* TGEI *)
+function clause decode (0b000001 : (regno) rs : 0b01001 : (imm16) imm) = 
+  Some(TRAPIMM(rs, imm, GEU)) (* TGEIU *)
+function clause decode (0b000001 : (regno) rs : 0b01010 : (imm16) imm) = 
+  Some(TRAPIMM(rs, imm, LT))  (* TLTI *)
+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);
@@ -1054,15 +1085,24 @@ 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) = Some(Load(B, true,  false, base, rt, offset)) (* LB *)
-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) = Some(Load(H, true,  false, base, rt, offset)) (* LH *)
-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) = Some(Load(W, true,  false, base, rt, offset)) (* LW *)
-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) = Some(Load(D, false, false, base, rt, offset)) (* LD *)
-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) = Some(Load(D, false, true, base, rt, offset))  (* LLD *)
+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) = 
+  Some(Load(B, false, false, base, rt, offset)) (* LBU *)
+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) = 
+  Some(Load(H, false, false, base, rt, offset)) (* LHU *)
+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) = 
+  Some(Load(W, false, false, base, rt, offset)) (* LWU *)
+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) = 
+  Some(Load(W, true,  true, base, rt, offset))  (* LL *)
+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)) =
   {
     (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), LoadData, width);
@@ -1091,12 +1131,18 @@ 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) = Some(Store(B, false, base, rt, offset)) (* SB *)
-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) = Some(Store(W, false, base, rt, offset)) (* SW *)
-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) = Some(Store(W, true, base, rt, offset))  (* SC *)
-function clause decode (0b111100 : (regno) base : (regno) rt : (imm16) offset) = Some(Store(D, true, base, rt, offset))  (* SCD *)
+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) = 
+  Some(Store(H, false, base, rt, offset)) (* SH *)
+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) = 
+  Some(Store(D, false, base, rt, offset)) (* SD *)
+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) = 
+  Some(Store(D, true, base, rt, offset))  (* SCD *)
 function clause execute (Store(width, conditional, base, rt, offset)) =
       {
         (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), StoreData, width);
@@ -1341,13 +1387,6 @@ function clause decode (0b000000 : 0b00000 : 0b00000 : 0b00000 : (regno) stype :
 function clause execute(SYNC) =
   MEM_sync()
 
-union ast member unit HCF
-function clause decode (0b010000 : 0b00100 : (regno) rt : 0b10111 : 0b00000000000) =
-  Some(HCF()) (* simulator halt instruction "MTC0 rt, $23" (cheri specific behaviour) *)
-
-function clause decode (0b010000 : 0b00100 : (regno) rt : 0b11010 : 0b00000000000) =
-  Some(HCF()) (* simulator halt instruction "MTC0 rt, $26" (cheri specific behaviour) *)
-
 union ast member (regno, regno, bit[3], bool) MFC0
 function clause decode (0b010000 : 0b00000 : (regno) rt : (regno) rd : 0b00000000 : (bit[3]) sel) =
   Some(MFC0(rt, rd, sel, false)) (* MFC0 *)
@@ -1570,7 +1609,8 @@ function clause execute ((TLBP)) = {
 }
 
 union ast member (regno, regno) RDHWR
-function clause decode (0b011111 : 0b00000 : (regno) rt : (regno) rd : 0b00000 : 0b111011) = Some(RDHWR(rt, rd))
+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
@@ -1606,5 +1646,13 @@ function clause execute (ERET) =
           }
       }
 
+(* simulator halt instruction "MTC0 rt, r23" (cheri specific behaviour) *)
+union ast member unit HCF
+function clause decode (0b010000 : 0b00100 : (regno) rt : 0b10111 : 0b00000000000) =
+  Some(HCF()) 
+
+function clause decode (0b010000 : 0b00100 : (regno) rt : 0b11010 : 0b00000000000) =
+  Some(HCF())
+
 function clause execute (HCF) =
   () (* halt instruction actually executed by interpreter framework *)
diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail
index 5847cecb..e498d354 100644
--- a/mips/mips_prelude.sail
+++ b/mips/mips_prelude.sail
@@ -32,13 +32,12 @@
 (*  SUCH DAMAGE.                                                          *)
 (*========================================================================*)
 
+(* mips_prelude.sail: declarations of mips registers, and functions common 
+   to mips instructions (e.g. address translation) *)
+
 (* bit vectors have indices decreasing from left i.e. msb is highest index *)
 default Order dec
 
-(*(* external functions *)
-val extern forall Nat 'm, Nat 'n. (implicit<'m>,bit['n]) -> bit['m] effect pure EXTS (* Sign extend *)
-val extern forall Nat 'n, Nat 'm. (implicit<'m>,bit['n]) -> bit['m] effect pure EXTZ (* Zero extend *)
-*)
 register (bit[64]) PC
 register (bit[64]) nextPC
 
@@ -228,13 +227,13 @@ val bit[64] -> bool effect pure NotWordVal
 function bool NotWordVal (word) = 
     (word[31] ^^ 32) != word[63..32]
 
-(* Read numbered GP reg. ($0 always zero) *)
+(* Read numbered GP reg. (r0 is always zero) *)
 val bit[5] -> bit[64] effect {rreg} rGPR
 function bit[64] rGPR idx = {
          if idx == 0 then 0 else GPR[idx]
 }
 
-(* Write numbered GP reg. (writes to $0 ignored) *)
+(* Write numbered GP reg. (writes to r0 ignored) *)
 val (bit[5], bit[64]) -> unit effect {wreg} wGPR
 function unit wGPR (idx, v) = {
          if idx == 0 then () else GPR[idx] := v
@@ -442,8 +441,10 @@ function (bit[64], bool) TLBTranslate2 ((bit[64]) vAddr, (MemAccessType) accessT
     else if ((accessType == StoreData) & ~(d)) then
       exit (SignalExceptionTLB(TLBMod, vAddr))
     else
-      (EXTZ(pfn[23..((evenOddBit)-(12))] : vAddr[((evenOddBit)-(1)) .. 0]), if (accessType == StoreData) then caps else capl)
-    case None -> exit (SignalExceptionTLB(if (accessType == StoreData) then XTLBRefillS else XTLBRefillL, vAddr))
+      (EXTZ(pfn[23..((evenOddBit)-(12))] : vAddr[((evenOddBit)-(1)) .. 0]), 
+       if (accessType == StoreData) then caps else capl)
+    case None -> exit (SignalExceptionTLB(
+      if (accessType == StoreData) then XTLBRefillS else XTLBRefillL, vAddr))
   }
 }
 
@@ -459,7 +460,7 @@ function (bit[64], bool) TLBTranslateC ((bit[64]) vAddr, (MemAccessType) accessT
         case (true, 0b00) -> (Kernel, Some(EXTZ(vAddr[28..0]))) (* kseg0 unmapped cached 32-bit compat *)
         case (_, _) -> (Kernel, None) (* xkseg mapped *)
       }
-      case 0b10 -> (Kernel, Some(EXTZ(vAddr[58..0])))       (* xkphys bits 61-59 are cache mode which we ignore *)
+      case 0b10 -> (Kernel, Some(EXTZ(vAddr[58..0])))       (* xkphys bits 61-59 are cache mode (ignored) *)
       case 0b01 -> (Supervisor, None)                       (* xsseg - supervisor mapped *)
       case 0b00 -> (User, None) (* xuseg - user mapped *)
     } in
@@ -484,9 +485,18 @@ function (bit[64]) TLBTranslate ((bit[64]) vAddr, (MemAccessType) accessType) =
 
 typedef regno = bit[5]                      (* a register number *)
 typedef imm16 = bit[16]                     (* 16-bit immediate *)
-typedef regregreg   = (regno, regno, regno) (* a commonly used instruction format with three register operands *)
-typedef regregimm16 = (regno, regno, imm16) (* a commonly used instruction format with two register operands and 16-bit immediate *)
-typedef decode_failure = enumerate { no_matching_pattern; unsupported_instruction; illegal_instruction; internal_error }
+(* a commonly used instruction format with three register operands *)
+typedef regregreg   = (regno, regno, regno)
+(* a commonly used instruction format with two register operands and 16-bit immediate *)
+typedef regregimm16 = (regno, regno, imm16)
+
+typedef decode_failure = enumerate { 
+  no_matching_pattern; 
+  unsupported_instruction; 
+  illegal_instruction; 
+  internal_error 
+}
+
 (* Used by branch and trap instructions *)
 typedef Comparison = enumerate { 
   EQ; (* equal *)
@@ -499,7 +509,8 @@ typedef Comparison = enumerate {
   LTU;(* unsigned less than or qual *) 
 }
 function bool compare ((Comparison)cmp, (bit[64]) valA, (bit[64]) valB) =
-  let valA65 = (0b0 : valA) in (* sail comparisons are signed so extend to 65 bits for unsigned comparisons *)
+   (* sail comparisons are signed so extend to 65 bits for unsigned comparisons *)
+  let valA65 = (0b0 : valA) in
   let valB65 = (0b0 : valB) in
   switch(cmp) {
     case EQ  -> valA ==   valB
diff --git a/mips/mips_wrappers.sail b/mips/mips_wrappers.sail
index 36495de2..36cbe0d4 100644
--- a/mips/mips_wrappers.sail
+++ b/mips/mips_wrappers.sail
@@ -32,6 +32,9 @@
 (*  SUCH DAMAGE.                                                          *)
 (*========================================================================*)
 
+(* mips_wrappers.sail: wrappers functions and hooks for CHERI extensibility 
+   (mostly identity functions here) *)
+
 function unit effect {wmem} MEMw_wrapper(addr, size, data) = MEMw(addr, size, data)
 function bool effect {wmem} MEMw_conditional_wrapper(addr, size, data) =
   MEMw_conditional(addr, size, data)