Fix implicits in v8.2 public ARM spec

2 files changed, 85 insertions, 86 deletions

diff --git a/aarch64/no_vector/spec.sail b/aarch64/no_vector/spec.sail
index fc53e03e..c91da297 100644
--- a/aarch64/no_vector/spec.sail
+++ b/aarch64/no_vector/spec.sail
@@ -564,9 +564,9 @@ val UndefinedFault : unit -> unit effect {escape}
 
 function UndefinedFault () = assert(false, "Undefined fault")
 
-val ThisInstrAddr : forall ('N : Int), 'N >= 0. unit -> bits('N) effect {rreg}
+val ThisInstrAddr : forall ('N : Int), 'N >= 0. (implicit('N), unit) -> bits('N) effect {rreg}
 
-function ThisInstrAddr () = return(slice(_PC, 0, 'N))
+function ThisInstrAddr(N, _) = slice(_PC, 0, N)
 
 val ThisInstr : unit -> bits(32) effect {rreg}
 
@@ -1521,9 +1521,9 @@ val AArch32_CurrentCond : unit -> bits(4) effect {rreg}
 function AArch32_CurrentCond () = return(__currentCond)
 
 val aget_SP : forall ('width : Int), 'width >= 0.
-  unit -> bits('width) effect {escape, rreg}
+  (implicit('width), unit) -> bits('width) effect {escape, rreg}
 
-function aget_SP () = {
+function aget_SP(width, _) = {
   assert('width == 8 | 'width == 16 | 'width == 32 | 'width == 64, "((width == 8) || ((width == 16) || ((width == 32) || (width == 64))))");
   if PSTATE.SP == 0b0 then return(slice(SP_EL0, 0, 'width)) else match PSTATE.EL {
     ? if ? == EL0 => return(slice(SP_EL0, 0, 'width)),
@@ -1762,9 +1762,9 @@ function AArch64_InstructionDevice (addrdesc__arg, vaddress, ipaddress, 'level,
 }
 
 val aget_Vpart : forall ('width : Int), 'width >= 0.
-  (int, int) -> bits('width) effect {escape, rreg}
+  (implicit('width), int, int) -> bits('width) effect {escape, rreg}
 
-function aget_Vpart ('n, 'part) = {
+function aget_Vpart (width, 'n, 'part) = {
   assert(n >= 0 & n <= 31, "((n >= 0) && (n <= 31))");
   assert(part == 0 | part == 1, "((part == 0) || (part == 1))");
   if part == 0 then {
@@ -1777,12 +1777,12 @@ function aget_Vpart ('n, 'part) = {
 }
 
 val aget_V : forall ('width : Int), 'width >= 0.
-  int -> bits('width) effect {escape, rreg}
+  (implicit('width), int) -> bits('width) effect {escape, rreg}
 
-function aget_V 'n = {
+function aget_V(width, n) = {
   assert(n >= 0 & n <= 31, "((n >= 0) && (n <= 31))");
-  assert('width == 8 | 'width == 16 | 'width == 32 | 'width == 64 | 'width == 128, "((width == 8) || ((width == 16) || ((width == 32) || ((width == 64) || (width == 128)))))");
-  return(slice(_V[n], 0, 'width))
+  assert(width == 8 | width == 16 | width == 32 | width == 64 | width == 128);
+  return(slice(_V[n], 0, width))
 }
 
 val LookUpRIndex : (int, bits(5)) -> int effect {escape, undef}
@@ -1829,9 +1829,9 @@ function BitReverse data = {
   return(result)
 }
 
-val NextInstrAddr : forall ('N : Int), 'N >= 0. unit -> bits('N) effect {rreg}
+val NextInstrAddr : forall ('N : Int), 'N >= 0. (implicit('N), unit) -> bits('N) effect {rreg}
 
-function NextInstrAddr () = return(slice(_PC + ThisInstrLength() / 8, 0, 'N))
+function NextInstrAddr(N, _) = slice(_PC + ThisInstrLength() / 8, 0, N)
 
 val AArch32_ExceptionClass : Exception -> (int, bits(1)) effect {escape, rreg, undef}
 
@@ -2000,7 +2000,7 @@ val aget_Elem__0 : forall ('N : Int) ('size : Int), 'N >= 0 & 'size >= 0.
   (bits('N), int, atom('size)) -> bits('size) effect {escape}
 
 val aget_Elem__1 : forall ('N : Int) ('size : Int), 'N >= 0 & 'size >= 0.
-  (bits('N), int) -> bits('size) effect {escape}
+  (implicit('size), bits('N), int) -> bits('size) effect {escape}
 
 overload aget_Elem = {aget_Elem__0, aget_Elem__1}
 
@@ -2009,7 +2009,7 @@ function aget_Elem__0 (vector_name, 'e, size) = {
   return(slice(vector_name, e * 'size, 'size))
 }
 
-function aget_Elem__1 (vector_name, 'e) = return(aget_Elem(vector_name, e, 'size))
+function aget_Elem__1 (size, vector_name, 'e) = return(aget_Elem(vector_name, e, size))
 
 val UnsignedSatQ : forall ('N : Int), 'N >= 0.
   (int, atom('N)) -> (bits('N), bool) effect {undef}
@@ -2060,24 +2060,24 @@ function SatQ ('i, N, unsigned) = {
 }
 
 val Replicate : forall ('M : Int) ('N : Int), 'M >= 0 & 'N >= 0.
-  bits('M) -> bits('N) effect {escape}
+  (implicit('N), bits('M)) -> bits('N) effect {escape}
 
-function Replicate x = {
-  assert('N % 'M == 0, "((N MOD M) == 0)");
-  let 'O = 'N / 'M;
+function Replicate(N, x) = {
+  assert(N % 'M == 0, "((N MOD M) == 0)");
+  let 'O = N / 'M;
   assert(constraint('O * 'M == 'N));
-  return(replicate_bits(x, 'N / 'M))
+  return(replicate_bits(x, N / 'M))
 }
 
 val Zeros__0  = {c: "zeros"} : forall ('N : Int), 'N >= 0. atom('N) -> bits('N)
 
-val Zeros__1 : forall ('N : Int), 'N >= 0. unit -> bits('N)
+val Zeros__1 : forall ('N : Int), 'N >= 0. (implicit('N), unit) -> bits('N)
 
 overload Zeros = {Zeros__0, Zeros__1}
 
-function Zeros__0 N = return(replicate_bits(0b0, 'N))
+function Zeros__0(N) = replicate_bits(0b0, N)
 
-function Zeros__1 () = return(Zeros('N))
+function Zeros__1(N, _) = Zeros__0(N)
 
 val __ResetMemoryState : unit -> unit effect {rreg, wreg}
 
@@ -2090,16 +2090,16 @@ val ZeroExtend__0 = {c: "zero_extend"} : forall ('M : Int) ('N : Int), 'M >= 0 &
   (bits('M), atom('N)) -> bits('N) effect {escape}
 
 val ZeroExtend__1 : forall ('M : Int) ('N : Int), 'M >= 0 & 'N >= 0.
-  bits('M) -> bits('N) effect {escape}
+  (implicit('N), bits('M)) -> bits('N) effect {escape}
 
 overload ZeroExtend = {ZeroExtend__0, ZeroExtend__1}
 
-function ZeroExtend__0 (x, N) = {
-  assert('N >= 'M);
-  return(Zeros('N - 'M) @ x)
+function ZeroExtend__0(x, N) = {
+  assert(N >= 'M);
+  Zeros(N - 'M) @ x
 }
 
-function ZeroExtend__1 x = return(ZeroExtend(x, 'N))
+function ZeroExtend__1(N, x) = ZeroExtend__0(x, N)
 
 val aset_Vpart : forall ('width : Int), 'width >= 0.
   (int, int, bits('width)) -> unit effect {escape, wreg, rreg}
@@ -2278,10 +2278,10 @@ function GetPSRFromPSTATE () = {
   return(spsr)
 }
 
-val FPZero : forall ('N : Int), 1 >= 0 & 'N >= 0.
-  bits(1) -> bits('N) effect {escape}
+val FPZero : forall ('N : Int), 'N >= 0.
+  (implicit('N), bits(1)) -> bits('N) effect {escape}
 
-function FPZero sign = {
+function FPZero(N, sign) = {
   assert('N == 16 | 'N == 32 | 'N == 64, "((N == 16) || ((N == 32) || (N == 64)))");
   let 'E = (if 'N == 16 then 5 else if 'N == 32 then 8 else 11) : {|5, 8, 11|};
   F : atom('N - 'E - 1) = ('N - E) - 1;
@@ -2303,9 +2303,9 @@ function ExceptionSyndrome typ = {
 }
 
 val ConstrainUnpredictableBits : forall ('width : Int), 'width >= 0.
-  Unpredictable -> (Constraint, bits('width)) effect {undef}
+  (implicit('width), Unpredictable) -> (Constraint, bits('width)) effect {undef}
 
-function ConstrainUnpredictableBits which = {
+function ConstrainUnpredictableBits(width, which) = {
   c : Constraint = ConstrainUnpredictable(which);
   if c == Constraint_UNKNOWN then return((c, Zeros('width))) else return((c, undefined))
 }
@@ -2335,9 +2335,9 @@ function AArch32_PhysicalSErrorSyndrome () = {
 }
 
 val VFPExpandImm : forall ('N : Int), 8 >= 0 & 'N >= 0.
-  bits(8) -> bits('N) effect {escape}
+  (implicit('N), bits(8)) -> bits('N) effect {escape}
 
-function VFPExpandImm imm8 = {
+function VFPExpandImm(N, imm8) = {
   assert('N == 16 | 'N == 32 | 'N == 64, "((N == 16) || ((N == 32) || (N == 64)))");
   let 'E = (if 'N == 16 then 5 else if 'N == 32 then 8 else 11) : {|5, 8, 11|};
   F : atom('N - 'E - 1) = ('N - E) - 1;
@@ -2351,28 +2351,28 @@ val SignExtend__0 : forall ('M : Int) ('N : Int), 'M >= 0 & 'N >= 0.
   (bits('M), atom('N)) -> bits('N) effect {escape}
 
 val SignExtend__1 : forall ('M : Int) ('N : Int), 'M >= 0 & 'N >= 0.
-  bits('M) -> bits('N) effect {escape}
+  (implicit('N), bits('M)) -> bits('N) effect {escape}
 
 overload SignExtend = {SignExtend__0, SignExtend__1}
 
-function SignExtend__0 (x, N) = {
+function SignExtend__0(x, N) = {
   assert('N >= 'M);
-  return(replicate_bits([x['M - 1]], 'N - 'M) @ x)
+  replicate_bits([x['M - 1]], 'N - 'M) @ x
 }
 
-function SignExtend__1 x = return(SignExtend(x, 'N))
+function SignExtend__1(N, x) = SignExtend__0(x, N)
 
 val Extend__0 : forall ('M : Int) ('N : Int), 'M >= 0 & 'N >= 0.
   (bits('M), atom('N), bool) -> bits('N) effect {escape}
 
 val Extend__1 : forall ('M : Int) ('N : Int), 'M >= 0 & 'N >= 0.
-  (bits('M), bool) -> bits('N) effect {escape}
+  (implicit('N), bits('M), bool) -> bits('N) effect {escape}
 
 overload Extend = {Extend__0, Extend__1}
 
-function Extend__0 (x, N, unsigned) = return(if unsigned then ZeroExtend(x, 'N) else SignExtend(x, 'N))
+function Extend__0(x, N, unsigned) = if unsigned then ZeroExtend(x, N) else SignExtend(x, N)
 
-function Extend__1 (x, unsigned) = return(Extend(x, 'N, unsigned))
+function Extend__1(N, x, unsigned) = Extend__0(x, N, unsigned)
 
 val ASR_C : forall ('N : Int), 'N >= 0 & 'N >= 0 & 1 >= 0.
   (bits('N), int) -> (bits('N), bits(1)) effect {escape}
@@ -2398,22 +2398,22 @@ function ASR (x, 'shift) = {
 
 val Ones__0 : forall ('N : Int), 'N >= 0. atom('N) -> bits('N)
 
-val Ones__1 : forall ('N : Int), 'N >= 0. unit -> bits('N)
+val Ones__1 : forall ('N : Int), 'N >= 0. (implicit('N), unit) -> bits('N)
 
 overload Ones = {Ones__0, Ones__1}
 
-function Ones__0 N = return(replicate_bits(0b1, 'N))
+function Ones__0(N) = replicate_bits(0b1, N)
 
-function Ones__1 () = return(Ones('N))
+function Ones__1(N, _) = Ones(N)
 
 val IsOnes : forall ('N : Int), 'N >= 0. bits('N) -> bool
 
 function IsOnes x = return(x == Ones('N))
 
 val FPMaxNormal : forall ('N : Int), 1 >= 0 & 'N >= 0.
-  bits(1) -> bits('N) effect {escape}
+  (implicit('N), bits(1)) -> bits('N) effect {escape}
 
-function FPMaxNormal sign = {
+function FPMaxNormal(N, sign) = {
   assert('N == 16 | 'N == 32 | 'N == 64, "((N == 16) || ((N == 32) || (N == 64)))");
   let 'E = (if 'N == 16 then 5 else if 'N == 32 then 8 else 11) : {|5, 8, 11|};
   F : atom('N - 'E - 1) = ('N - E) - 1;
@@ -2423,9 +2423,9 @@ function FPMaxNormal sign = {
 }
 
 val FPInfinity : forall ('N : Int), 1 >= 0 & 'N >= 0.
-  bits(1) -> bits('N) effect {escape}
+  (implicit('N), bits(1)) -> bits('N) effect {escape}
 
-function FPInfinity sign = {
+function FPInfinity(N, sign) = {
   assert('N == 16 | 'N == 32 | 'N == 64, "((N == 16) || ((N == 32) || (N == 64)))");
   let 'E = (if 'N == 16 then 5 else if 'N == 32 then 8 else 11) : {|5, 8, 11|};
   F : atom('N - 'E - 1) = ('N - E) - 1;
@@ -2434,9 +2434,9 @@ function FPInfinity sign = {
   return(append(append(sign, exp), frac))
 }
 
-val FPDefaultNaN : forall ('N : Int), 'N >= 0. unit -> bits('N) effect {escape}
+val FPDefaultNaN : forall ('N : Int), 'N >= 0. (implicit('N), unit) -> bits('N) effect {escape}
 
-function FPDefaultNaN () = {
+function FPDefaultNaN(N, _)= {
   assert('N == 16 | 'N == 32 | 'N == 64, "((N == 16) || ((N == 32) || (N == 64)))");
   let 'E = (if 'N == 16 then 5 else if 'N == 32 then 8 else 11) : {|5, 8, 11|};
   F : atom('N - 'E - 1) = ('N - E) - 1;
@@ -2447,9 +2447,9 @@ function FPDefaultNaN () = {
 }
 
 val FPConvertNaN : forall ('N : Int) ('M : Int), 'N >= 0 & 'M >= 0.
-  bits('N) -> bits('M) effect {escape, undef}
+  (implicit('M), bits('N)) -> bits('M) effect {escape, undef}
 
-function FPConvertNaN op = {
+function FPConvertNaN(M, op) = {
   assert('N == 16 | 'N == 32 | 'N == 64, "((N == 16) || ((N == 32) || (N == 64)))");
   assert('M == 16 | 'M == 32 | 'M == 64, "((M == 16) || ((M == 32) || (M == 64)))");
   result : bits('M) = undefined;
@@ -2701,9 +2701,9 @@ function aset_ELR__1 value_name = {
 }
 
 val aget_X : forall ('width : Int), 'width >= 0.
-  int -> bits('width) effect {escape, rreg}
+  (implicit('width), int) -> bits('width) effect {escape, rreg}
 
-function aget_X 'n = {
+function aget_X(width, 'n) = {
   assert(n >= 0 & n <= 31, "((n >= 0) && (n <= 31))");
   assert('width == 8 | 'width == 16 | 'width == 32 | 'width == 64, "((width == 8) || ((width == 16) || ((width == 32) || (width == 64))))");
   if n != 31 then return(slice(_R[n], 0, 'width)) else return(Zeros('width))
@@ -2945,9 +2945,9 @@ function integer_arithmetic_addsub_carry_decode (sf, op, S, Rm, opcode2, Rn, Rd)
 }
 
 val ExtendReg : forall ('N : Int), 'N >= 0.
-  (int, ExtendType, int) -> bits('N) effect {escape, rreg, undef}
+  (implicit('N), int, ExtendType, int) -> bits('N) effect {escape, rreg, undef}
 
-function ExtendReg (reg, typ, shift) = {
+function ExtendReg (N, reg, typ, shift) = {
   assert(shift >= 0 & shift <= 4, "((shift >= 0) && (shift <= 4))");
   val_name : bits('N) = aget_X(reg);
   unsigned : bool = undefined;
@@ -3051,9 +3051,9 @@ function aarch64_integer_bitfield ('R, 'S, 'd, datasize, extend, inzero, 'n, tma
 }
 
 val ShiftReg : forall ('N : Int), 'N >= 0.
-  (int, ShiftType, int) -> bits('N) effect {escape, rreg, undef}
+  (implicit('N), int, ShiftType, int) -> bits('N) effect {escape, rreg, undef}
 
-function ShiftReg ('reg, typ, 'amount) = {
+function ShiftReg (N, 'reg, typ, 'amount) = {
   result : bits('N) = aget_X(reg);
   match typ {
     ShiftType_LSL => result = LSL(result, amount),
@@ -3482,9 +3482,9 @@ function FPProcessException (exception, fpcr) = {
 }
 
 val FPRoundBase : forall ('N : Int), 32 >= 0 & 'N >= 0.
-  (real, bits(32), FPRounding) -> bits('N) effect {escape, wreg, rreg, undef}
+  (implicit('N), real, bits(32), FPRounding) -> bits('N) effect {escape, wreg, rreg, undef}
 
-function FPRoundBase (op, fpcr, rounding) = {
+function FPRoundBase (N, op, fpcr, rounding) = {
   assert('N == 16 | 'N == 32 | 'N == 64);
   assert(op != 0.0);
   assert(rounding != FPRounding_TIEAWAY);
@@ -3591,34 +3591,34 @@ function FPRoundBase (op, fpcr, rounding) = {
 }
 
 val FPRoundCV : forall ('N : Int), 32 >= 0 & 'N >= 0.
-  (real, bits(32), FPRounding) -> bits('N) effect {escape, rreg, undef, wreg}
+  (implicit('N), real, bits(32), FPRounding) -> bits('N) effect {escape, rreg, undef, wreg}
 
-function FPRoundCV (op, fpcr__arg, rounding) = {
+function FPRoundCV (N, op, fpcr__arg, rounding) = {
   fpcr = fpcr__arg;
   fpcr = __SetSlice_bits(32, 1, fpcr, 19, 0b0);
   return(FPRoundBase(op, fpcr, rounding))
 }
 
-val FPRound__0 : forall ('N : Int), 32 >= 0 & 'N >= 0.
-  (real, bits(32), FPRounding) -> bits('N) effect {escape, rreg, undef, wreg}
+val FPRound__0 : forall ('N : Int), 'N >= 0.
+  (implicit('N), real, bits(32), FPRounding) -> bits('N) effect {escape, rreg, undef, wreg}
 
-val FPRound__1 : forall ('N : Int), 32 >= 0 & 'N >= 0.
-  (real, bits(32)) -> bits('N) effect {escape, rreg, undef, wreg}
+val FPRound__1 : forall ('N : Int), 'N >= 0.
+  (implicit('N), real, bits(32)) -> bits('N) effect {escape, rreg, undef, wreg}
 
 overload FPRound = {FPRound__0, FPRound__1}
 
-function FPRound__0 (op, fpcr__arg, rounding) = {
+function FPRound__0 (N, op, fpcr__arg, rounding) = {
   fpcr = fpcr__arg;
   fpcr = __SetSlice_bits(32, 1, fpcr, 26, 0b0);
   return(FPRoundBase(op, fpcr, rounding))
 }
 
-function FPRound__1 (op, fpcr) = return(FPRound(op, fpcr, FPRoundingMode(fpcr)))
+function FPRound__1 (N, op, fpcr) = return(FPRound(op, fpcr, FPRoundingMode(fpcr)))
 
 val FixedToFP : forall ('M : Int) ('N : Int), 'M >= 0 & 32 >= 0 & 'N >= 0.
-  (bits('M), int, bool, bits(32), FPRounding) -> bits('N) effect {escape, undef, wreg, rreg}
+  (implicit('N), bits('M), int, bool, bits(32), FPRounding) -> bits('N) effect {escape, undef, wreg, rreg}
 
-function FixedToFP (op, 'fbits, unsigned, fpcr, rounding) = {
+function FixedToFP (N, op, 'fbits, unsigned, fpcr, rounding) = {
   assert('N == 16 | 'N == 32 | 'N == 64);
   assert('M == 16 | 'M == 32 | 'M == 64);
   result : bits('N) = undefined;
@@ -3896,14 +3896,14 @@ function FPUnpackCV (fpval, fpcr__arg) = {
 }
 
 val FPConvert__0 : forall ('N : Int) ('M : Int), 'N >= 0 & 32 >= 0 & 'M >= 0.
-  (bits('N), bits(32), FPRounding) -> bits('M) effect {escape, rreg, undef, wreg}
+  (implicit('M), bits('N), bits(32), FPRounding) -> bits('M) effect {escape, rreg, undef, wreg}
 
 val FPConvert__1 : forall ('N : Int) ('M : Int), 'N >= 0 & 32 >= 0 & 'M >= 0.
-  (bits('N), bits(32)) -> bits('M) effect {escape, rreg, undef, wreg}
+  (implicit('M), bits('N), bits(32)) -> bits('M) effect {escape, rreg, undef, wreg}
 
 overload FPConvert = {FPConvert__0, FPConvert__1}
 
-function FPConvert__0 (op, fpcr, rounding) = {
+function FPConvert__0 (M, op, fpcr, rounding) = {
   assert('M == 16 | 'M == 32 | 'M == 64);
   assert('N == 16 | 'N == 32 | 'N == 64);
   result : bits('M) = undefined;
@@ -3927,7 +3927,7 @@ function FPConvert__0 (op, fpcr, rounding) = {
   return(result)
 }
 
-function FPConvert__1 (op, fpcr) = return(FPConvert(op, fpcr, FPRoundingMode(fpcr)))
+function FPConvert__1 (M, op, fpcr) = return(FPConvert(op, fpcr, FPRoundingMode(fpcr)))
 
 val FPUnpack : forall ('N : Int), 'N >= 0 & 32 >= 0 & 1 >= 0.
   (bits('N), bits(32)) -> (FPType, bits(1), real) effect {escape, rreg, undef, wreg}
@@ -3943,9 +3943,9 @@ function FPUnpack (fpval, fpcr__arg) = {
 }
 
 val FPToFixedJS : forall ('M : Int) ('N : Int), 'M >= 0 & 32 >= 0 & 'N >= 0.
-  (bits('M), bits(32), bool) -> bits('N) effect {escape, rreg, undef, wreg}
+  (implicit('N), bits('M), bits(32), bool) -> bits('N) effect {escape, rreg, undef, wreg}
 
-function FPToFixedJS (op, fpcr, Is64) = {
+function FPToFixedJS (N, op, fpcr, Is64) = {
   assert('M == 64 & 'N == 32, "((M == 64) && (N == 32))");
   value_name : real = undefined;
   sign : bits(1) = undefined;
@@ -3976,9 +3976,9 @@ function FPToFixedJS (op, fpcr, Is64) = {
 }
 
 val FPToFixed : forall ('N : Int) ('M : Int), 'N >= 0 & 32 >= 0 & 'M >= 0.
-  (bits('N), int, bool, bits(32), FPRounding) -> bits('M) effect {escape, rreg, undef, wreg}
+  (implicit('M), bits('N), int, bool, bits(32), FPRounding) -> bits('M) effect {escape, rreg, undef, wreg}
 
-function FPToFixed (op, 'fbits, unsigned, fpcr, rounding) = {
+function FPToFixed (M, op, 'fbits, unsigned, fpcr, rounding) = {
   assert('N == 16 | 'N == 32 | 'N == 64, "((N == 16) || ((N == 32) || (N == 64)))");
   assert('M == 16 | 'M == 32 | 'M == 64, "((M == 16) || ((M == 32) || (M == 64)))");
   assert(fbits >= 0, "(fbits >= 0)");
@@ -5273,9 +5273,9 @@ function IsOnes_slice (xs, i, 'l) = {
 }
 
 val ZeroExtend_slice_append : forall 'n 'm 'o, 'n >= 0 & 'm >= 0 & 'o >= 0.
-  (bits('n), int, int, bits('m)) -> bits('o) effect {escape}
+  (implicit('o), bits('n), int, int, bits('m)) -> bits('o) effect {escape}
 
-function ZeroExtend_slice_append (xs, i, 'l, ys) = {
+function ZeroExtend_slice_append (o, xs, i, 'l, ys) = {
   assert(constraint('l >= 0));
   ZeroExtend(slice(xs, i, l) @ ys)
 }
@@ -11573,9 +11573,9 @@ function integer_arithmetic_addsub_extendedreg_decode (sf, op, S, opt, Rm, optio
 }
 
 val DecodeBitMasks : forall ('M : Int), 1 >= 0 & 6 >= 0 & 6 >= 0 & 'M >= 0 & 'M >= 0.
-  (bits(1), bits(6), bits(6), bool) -> (bits('M), bits('M)) effect {escape, rreg, undef, wreg}
+  (implicit('M), bits(1), bits(6), bits(6), bool) -> (bits('M), bits('M)) effect {escape, rreg, undef, wreg}
 
-function DecodeBitMasks (immN, imms, immr, immediate) = {
+function DecodeBitMasks (M, immN, imms, immr, immediate) = {
   tmask : bits(64) = undefined;
   wmask : bits(64) = undefined;
   tmask_and : bits(6) = undefined;
diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail
index 98318dd4..f4f7dc75 100755
--- a/aarch64/prelude.sail
+++ b/aarch64/prelude.sail
@@ -6,8 +6,6 @@ $include <arith.sail>
 
 type bits ('n : Int) = vector('n, dec, bit)
 
-val eq_bit = {ocaml: "(fun (x, y) -> x = y)", lem: "eq", interpreter: "eq_anything", c: "eq_bit", coq: "eq_bit"} : (bit, bit) -> bool
-
 val eq_vec = {ocaml: "eq_list", lem: "eq_vec", c: "eq_bits", coq: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
 
 val eq_string = {ocaml: "eq_string", lem: "eq", c: "eq_string", coq: "generic_eq"} : (string, string) -> bool
@@ -28,7 +26,7 @@ val list_length = {ocaml: "length", lem: "length_list", c: "length", coq: "lengt
 
 overload length = {bitvector_length, vector_length, list_length}
 
-overload operator == = {eq_bit, eq_vec, eq_string, eq_real, eq_anything}
+overload operator == = {eq_vec, eq_string, eq_real, eq_anything}
 
 val vector_subrange_A = {
   ocaml: "subrange",
@@ -135,7 +133,7 @@ val or_vec = {lem: "or_vec", c: "or_bits", coq: "or_vec"}: forall 'n. (bits('n),
 
 function or_vec (xs, ys) = builtin_or_vec(xs, ys)
 
-overload operator | = {or_bool, or_vec}
+overload operator | = {or_vec}
 
 val UInt = {
   ocaml: "uint",
@@ -373,3 +371,4 @@ val __GetVerbosity = {c: "sail_get_verbosity"}: unit -> bits(64) effect {rreg, u
 
 val get_cycle_count = { c: "get_cycle_count" } : unit -> int effect {undef, wreg, rreg, rmem, wmem}
 
+overload __size = {length}