Merge remote-tracking branch 'origin/asl_flow2' into sail2

4 files changed, 112 insertions, 107 deletions

diff --git a/aarch64/Makefile b/aarch64/Makefile
index aa4d5301..365e23bd 100644
--- a/aarch64/Makefile
+++ b/aarch64/Makefile
@@ -5,13 +5,13 @@ SAIL_LIB_DIR:=$(SAIL_DIR)/lib
 SAIL:=$(SAIL_DIR)/sail
 
 aarch64.c: no_vector.sail
-	$(SAIL) $^ -c -O -undefined_gen -no_lexp_bounds_check -memo_z3 1> aarch64.c
+	$(SAIL) $(SAIL_FLAGS) $^ -c -O -undefined_gen -no_lexp_bounds_check -memo_z3 1> aarch64.c
 
 aarch64_c: aarch64.c
 	gcc -O2 $^ -o aarch64_c -lgmp -I $(SAIL_DIR)/lib
 
 aarch64: no_vector.sail
-	$(SAIL) $^ -o aarch64 -ocaml -undefined_gen -no_lexp_bounds_check -memo_z3
+	$(SAIL) $(SAIL_FLAGS) $^ -o aarch64 -ocaml -undefined_gen -no_lexp_bounds_check -memo_z3
 
 aarch64_full: full.sail
 	$(SAIL) $^ -o aarch64_full -ocaml -undefined_gen -no_lexp_bounds_check -memo_z3
@@ -23,5 +23,11 @@ aarch64_types.lem: aarch64.lem
 Aarch64.thy: aarch64_extras.lem aarch64_types.lem aarch64.lem
 	lem -isa -outdir . -lib Sail=$(SAIL_DIR)/src/gen_lib -lib Sail=$(SAIL_DIR)/src/lem_interp $^
 
+clean:
+	rm -rf _sbuild/
+	rm -f aarch64
+	rm -f aarch64.c
+	rm -f aarch64.lem
+
 LOC_FILES:=prelude.sail full/spec.sail decode_start.sail full/decode.sail decode_end.sail main.sail
 include ../etc/loc.mk
diff --git a/aarch64/elfmain.sail b/aarch64/elfmain.sail
index ad564108..2fdb471b 100644
--- a/aarch64/elfmain.sail
+++ b/aarch64/elfmain.sail
@@ -23,7 +23,7 @@ function Step_CPU() = {
   interrupt_req.take_IRQ = true; interrupt_req.take_vIRQ = true;
   interrupt_req.take_FIQ = true; interrupt_req.take_vFIQ = true;
   try {
-      var interrupted = false;
+      var interrupted : bool = false;
       interrupted = TakePendingInterrupts(interrupt_req);
       if interrupted then {
           print("Pending interrupt taken\n");
@@ -34,7 +34,7 @@ function Step_CPU() = {
       }
   };
 
-  var fetch_ok = false;
+  var fetch_ok : bool = false;
   try {
       if PSTATE.nRW != bitzero then {
         print("UNIMPLEMENTED: AArch32 support\n");
@@ -247,7 +247,7 @@ function Step_System () = {
                    PSTATE.EL);
       };
       if prevI != PSTATE.I then {
-	prerr_bits("[Sail] PSTATE.I changed to: ", PSTATE.I);
+        prerr_bits("[Sail] PSTATE.I changed to: ", PSTATE.I);
         print(concat_str("   at PC=",
               concat_str(HexStr(UInt(aget_PC())),
               concat_str(" in cycle=",
@@ -263,7 +263,7 @@ function Step_System () = {
 
     } catch {
       Error_ExceptionTaken(_) => {
-	// enable_tracing()
+        // enable_tracing()
         print(concat_str("Exception taken during Step_System.  PC=",
               concat_str(HexStr(UInt(aget_PC())),
               concat_str(" cycle=",
diff --git a/aarch64/no_vector/spec.sail b/aarch64/no_vector/spec.sail
index 610884a4..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)
 }
@@ -6336,7 +6336,7 @@ function AArch64_CheckS2Permission (perms, vaddress, ipaddress, 'level, acctype,
 }
 
 function AArch64_CheckAndUpdateDescriptor_SecondStage (result, fault, vaddress, acctype, iswrite, s2fs1walk, hwupdatewalk__arg) = {
-  hwupdatewalk = hwupdatewalk__arg;
+  hwupdatewalk : bool = hwupdatewalk__arg;
   hw_update_AF : bool = undefined;
   if result.AF then
     if fault.typ == Fault_None then hw_update_AF = true
@@ -6703,7 +6703,7 @@ function AArch64_SecondStageTranslate (S1, vaddress, acctype, iswrite, wasaligne
 }
 
 function AArch64_CheckAndUpdateDescriptor (result, fault, secondstage, vaddress, acctype, iswrite, s2fs1walk, hwupdatewalk__arg) = {
-  hwupdatewalk = hwupdatewalk__arg;
+  hwupdatewalk : bool = hwupdatewalk__arg;
   hw_update_AF : bool = undefined;
   if result.AF then if fault.typ == Fault_None then hw_update_AF = true else if ConstrainUnpredictable(Unpredictable_AFUPDATE) == Constraint_TRUE then hw_update_AF = true else hw_update_AF = false else ();
   hw_update_AP : bool = undefined;
@@ -6740,7 +6740,7 @@ function AArch64_StateMatch (SSC__arg, HMC__arg, PxC__arg, linked__arg, LBN, isb
   HMC = HMC__arg;
   PxC = PxC__arg;
   SSC = SSC__arg;
-  linked = linked__arg;
+  linked : bool = linked__arg;
   c : Constraint = undefined;
   if (((((((HMC @ SSC) @ PxC) & 0b11100) == 0b01100 | (((HMC @ SSC) @ PxC) & 0b11101) == 0b10000 | (((HMC @ SSC) @ PxC) & 0b11101) == 0b10100 | ((HMC @ SSC) @ PxC) == 0b11010 | ((HMC @ SSC) @ PxC) == 0b11101 | (((HMC @ SSC) @ PxC) & 0b11110) == 0b11110) | (HMC == 0b0 & PxC == 0b00) & (~(isbreakpnt) | ~(HaveAArch32EL(EL1)))) | (SSC == 0b01 | SSC == 0b10) & ~(HaveEL(EL3))) | (((HMC @ SSC) != 0b000 & (HMC @ SSC) != 0b111) & ~(HaveEL(EL3))) & ~(HaveEL(EL2))) | ((HMC @ SSC) @ PxC) == 0b11100 & ~(HaveEL(EL2)) then {
     __tmp_5 : bits(5) = undefined;
@@ -9202,7 +9202,7 @@ function aarch64_memory_single_general_register (acctype, 'datasize, extend_type
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
   assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
-  wback = wback__arg;
+  wback : bool = wback__arg;
   offset : bits(64) = ExtendReg(m, extend_type, shift);
   address : bits(64) = undefined;
   data : bits('datasize) = undefined;
@@ -9258,7 +9258,7 @@ function aarch64_memory_single_general_immediate_unsigned (acctype, 'datasize, m
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
   assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
-  wback = wback__arg;
+  wback : bool = wback__arg;
   address : bits(64) = undefined;
   data : bits('datasize) = undefined;
   wb_unknown : bool = false;
@@ -9313,7 +9313,7 @@ function aarch64_memory_single_general_immediate_signed_postidx (acctype, 'datas
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
   assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
-  wback = wback__arg;
+  wback : bool = wback__arg;
   address : bits(64) = undefined;
   data : bits('datasize) = undefined;
   wb_unknown : bool = false;
@@ -9364,7 +9364,7 @@ function aarch64_memory_single_general_immediate_signed_postidx (acctype, 'datas
 val aarch64_memory_single_general_immediate_signed_pac : (int, bits(64), int, bool, bool) -> unit effect {escape, rmem, rreg, undef, wmem, wreg}
 
 function aarch64_memory_single_general_immediate_signed_pac ('n, offset, 't, use_key_a, wback__arg) = {
-  wback = wback__arg;
+  wback : bool = wback__arg;
   address : bits(64) = undefined;
   data : bits(64) = undefined;
   wb_unknown : bool = false;
@@ -9400,7 +9400,7 @@ function aarch64_memory_single_general_immediate_signed_offset_unpriv (acctype,
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
   assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
-  wback = wback__arg;
+  wback : bool = wback__arg;
   address : bits(64) = undefined;
   data : bits('datasize) = undefined;
   wb_unknown : bool = false;
@@ -9455,7 +9455,7 @@ function aarch64_memory_single_general_immediate_signed_offset_normal (acctype,
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
   assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
-  wback = wback__arg;
+  wback : bool = wback__arg;
   address : bits(64) = undefined;
   data : bits('datasize) = undefined;
   wb_unknown : bool = false;
@@ -9611,7 +9611,7 @@ val aarch64_memory_pair_general_postidx : forall ('datasize : Int).
 function aarch64_memory_pair_general_postidx (acctype, datasize, memop, n, offset, postindex, signed, t, t2, wback__arg) = let 'dbytes = ex_int(datasize / 8) in {
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
   assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
-  wback = wback__arg;
+  wback : bool = wback__arg;
   address : bits(64) = undefined;
   data1 : bits('datasize) = undefined;
   data2 : bits('datasize) = undefined;
@@ -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 505ca7b6..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",
@@ -127,7 +125,7 @@ val and_vec = {lem: "and_vec", c: "and_bits", coq: "and_vec"} : forall 'n. (bits
 
 function and_vec (xs, ys) = builtin_and_vec(xs, ys)
 
-overload operator & = {and_bool, and_vec}
+overload operator & = {and_vec}
 
 val builtin_or_vec = {ocaml: "or_vec", c: "or_bits"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
@@ -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",
@@ -264,19 +262,19 @@ val Sqrt = {ocaml: "sqrt_real", lem: "realSqrt", c: "sqrt_real", coq: "sqrt"} :
 
 val gteq_real = {ocaml: "gteq_real", lem: "gteq", c: "gteq_real", coq: "gteq_real"} : (real, real) -> bool
 
-overload operator >= = {gteq_atom, gteq_int, gteq_real}
+overload operator >= = {gteq_real}
 
 val lteq_real = {ocaml: "lteq_real", lem: "lteq", c: "lteq_real", coq: "lteq_real"} : (real, real) -> bool
 
-overload operator <= = {lteq_atom, lteq_int, lteq_real}
+overload operator <= = {lteq_real}
 
 val gt_real = {ocaml: "gt_real", lem: "gt", c: "gt_real", coq: "gt_real"} : (real, real) -> bool
 
-overload operator > = {gt_atom, gt_int, gt_real}
+overload operator > = {gt_real}
 
 val lt_real = {ocaml: "lt_real", lem: "lt", c: "lt_real", coq: "lt_real"} : (real, real) -> bool
 
-overload operator < = {lt_atom, lt_int, lt_real}
+overload operator < = {lt_real}
 
 val RoundDown = {ocaml: "round_down", lem: "realFloor", c: "round_down", coq: "Zfloor"} : real -> int
 
@@ -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}