Add bitvector size constraints in MIPS

1 files changed, 2 insertions, 2 deletions

diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail
index b5931a45..7ec4fdfe 100644
--- a/mips/mips_prelude.sail
+++ b/mips/mips_prelude.sail
@@ -331,9 +331,9 @@ function wGPR (idx, v) = {
          if i == 0 then () else GPR[i] = v
 }
 
-val MEMr = {lem: "MEMr"} : forall 'n.
+val MEMr = {lem: "MEMr"} : forall 'n, 'n >= 0.
   ( bits(64) , atom('n) ) -> (bits(8 * 'n)) effect { rmem }
-val MEMr_reserve = {lem: "MEMr_reserve"} : forall 'n.
+val MEMr_reserve = {lem: "MEMr_reserve"} : forall 'n, 'n >= 0.
   ( bits(64) , atom('n) ) -> (bits(8 * 'n)) effect { rmem }
 val MEM_sync = {lem: "MEM_sync"} :
   unit -> unit effect { barr }